🦥 Lazy_storage_diff.v

Proofs

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).
Proof.
  intros.
  destruct H.
  Data_encoding.Valid.data_encoding_auto.
  all : sauto.
Qed.

Module diffs_item.
  Module Valid.

Validity predicate for a [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.
Proof.
(* Admitted as there are cast axioms in the encoding. *)
Admitted.
#[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)
    Lazy_storage_diff.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.