Skip to main content

🦥 Lazy_storage_diff.v


See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.

Require TezosOfOCaml.Proto_alpha.Lazy_storage_diff.
Require TezosOfOCaml.Proto_alpha.Proofs.Lazy_storage_kind.

Module OPS.
  Module Valid.
  Import TezosOfOCaml.Proto_alpha.Lazy_storage_diff.OPS.
[t] is used to validate [Ops]
  Record t {Id_t alloc updates : Set}
    (O : Lazy_storage_diff.OPS
      (Id_t := Id_t) (alloc := alloc) (updates := updates)) : Prop := {
        Id : Lazy_storage_kind.ID.Valid.t O.(Id);
        alloc_encoding :
          Data_encoding.Valid.t (fun _True) O.(alloc_encoding);
        updates_encoding :
          Data_encoding.Valid.t (fun _True) O.(updates_encoding);
  End Valid.
End OPS.

Module Ops.
  Module Valid.
[t] pattern matches [Lazy_storage_diff.ops] to generate a valid prop
    Inductive t {i a u} : Lazy_storage_diff.ops i a u Prop :=
    | Intro OPS : OPS.Valid.t OPS t (existS _ tt OPS).
  End Valid.
End Ops.

[diff_encoding] is valid by using the valid proposition generated by [Ops.Valid.t] constructor [Intro OPS]
Lemma diff_encoding_is_valid {i a u} (OPS : Lazy_storage_diff.ops i a u) :
  Ops.Valid.t OPS
  Data_encoding.Valid.t (fun _True) (Lazy_storage_diff.diff_encoding OPS).
  destruct H.
  all : sauto.

Module diffs_item.
  Module Valid.
Validity predicate for a [diffs_item].
    Inductive t : Lazy_storage_diff.diffs_item Prop :=
    | Big_map
        (id : Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t))
        (diff :
        ) :
      t (Lazy_storage_diff.Item Lazy_storage_kind.Big_map id diff)
    | Sapling_state
        (id : Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t))
        (diff :
        ) :
      t (Lazy_storage_diff.Item Lazy_storage_kind.Sapling_state id diff).
  End Valid.
End diffs_item.

The encoding [item_encoding] is valid.
Lemma item_encoding_is_valid :
  Data_encoding.Valid.t diffs_item.Valid.t Lazy_storage_diff.item_encoding.
  (* Admitted as there are cast axioms in the encoding. *)
#[global] Hint Resolve item_encoding_is_valid : Data_encoding_db.

[encoding] is valid for [Lazy_storage_diff] using [diff_encoding_is_valid] and [item_encoding_is_valid]
Lemma encoding_is_valid :
  Data_encoding.Valid.t (List.Forall diffs_item.Valid.t)
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.