Skip to main content

🦥 Lazy_storage_diff.v


See code, Gitlab , OCaml

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

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

Require TezosOfOCaml.Proto_alpha.Environment.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.

TODO : [item_encoding] definition is not verified because it's using [coq_axiom_with_reason] for translation
Axiom item_encoding_is_valid :
  Data_encoding.Valid.t (fun _True) Lazy_storage_diff.item_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 (fun _True) Lazy_storage_diff.encoding.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.