🦥 Lazy_storage_kind.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.

Require TezosOfOCaml.Proto_alpha.Lazy_storage_kind.
Require TezosOfOCaml.Proto_alpha.Proofs.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_repr.

Module ID.
  Module Valid.
    Import TezosOfOCaml.Proto_alpha.Lazy_storage_kind.ID.

    Record t {a : Set} (I : Lazy_storage_kind.ID (t := a)): Prop := {
      encoding : Data_encoding.Valid.t (fun _ ⇒ True) I.(encoding);
    }.
  End Valid.
End ID.

Lemma encoding_is_valid (y : Lazy_storage_kind.MakeId.FArgs) :
  Data_encoding.Valid.t (fun _ ⇒ True) Lazy_storage_kind.MakeId.Id.encoding.
Proof. Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

[compare] function is valid

Lemma compare_is_valid (args : Lazy_storage_kind.MakeId.FArgs) :
  Compare.Valid.t (fun _ ⇒ True) id Lazy_storage_kind.MakeId.Id.compare.
Proof. Compare.valid_auto. Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.

Lemma big_map_alloc_encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Lazy_storage_kind.Big_map.alloc_encoding.
Proof. Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve big_map_alloc_encoding_is_valid : Data_encoding_db.

Lemma update_encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Lazy_storage_kind.Big_map.update_encoding.
Proof. Data_encoding.Valid.data_encoding_auto.
       hauto l: on.
Qed.
#[global] Hint Resolve update_encoding_is_valid : Data_encoding_db.

Lemma updates_encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Lazy_storage_kind.Big_map.updates_encoding.
Proof. Data_encoding.Valid.data_encoding_auto. sfirstorder.
Qed.
#[global] Hint Resolve updates_encoding_is_valid : Data_encoding_db.

Module Sapling_state_alloc.
  Module Valid.
    Definition t (x : Lazy_storage_kind.Sapling_state.alloc) : Prop :=
      Sapling_repr.Memo_size.Valid.t
         x.(Lazy_storage_kind.Sapling_state.alloc.memo_size).
  End Valid.
End Sapling_state_alloc.

Lemma sapling_state_alloc_encoding_is_valid :
  Data_encoding.Valid.t
    Sapling_state_alloc.Valid.t
    Lazy_storage_kind.Sapling_state.alloc_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve sapling_state_alloc_encoding_is_valid : Data_encoding_db.

Lemma sapling_state_updates_encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True)
    Lazy_storage_kind.Sapling_state.updates_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve sapling_state_updates_encoding_is_valid :
  Data_encoding_db.