💎 Origination_nonce.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Origination_nonce.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Operation_hash.
Module Valid.
Import Origination_nonce.t.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Origination_nonce.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.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.
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.
: 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.
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.
Valid.t (Origination_nonce.incr noce_value).
Proof.
constructor; simpl.
lia.
Qed.