💎 Origination_nonce.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Origination_nonce.

Require TezosOfOCaml.Environment.V7.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V7.Proofs.Operation_hash.

Module Valid.
  Import Origination_nonce.t.

Validity predicate for [t].

  Record t (x : Origination_nonce.t) : Prop := {
    origination_index : Int32.Valid.t x.(origination_index);
  }.
End Valid.

The encoding [encoding] is valid.

Lemma encoding_is_valid
  : Data_encoding.Valid.t Valid.t Origination_nonce.encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

The function [initial] is valid.

Lemma initial_is_valid operation_hash :
  Valid.t (Origination_nonce.initial operation_hash).
Proof.
  easy.
Qed.

The function [incr] is valid.

Lemma incr_is_valid noce_value :
  Valid.t (Origination_nonce.incr noce_value).
Proof.
  constructor; simpl.
  lia.
Qed.