Skip to main content

💎 Origination_nonce.v

Proofs

See code, Gitlab , OCaml

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

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

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Operation_hash.

Module Valid.
  Import Origination_nonce.t.

  Record t (x : Origination_nonce.t) : Prop := {
    origination_index : Int32.Valid.t x.(origination_index);
  }.
End 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.