🦏 Sc_rollup_inbox_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_repr.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Context_hash.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_repr.

Module Valid.
  Import Sc_rollup_inbox_repr.t.

  Record t (x : Sc_rollup_inbox_repr.t) : Prop := {
    level : Raw_level_repr.Valid.t x.(level);
    nb_available_messages : Int64.Valid.t x.(nb_available_messages);
    message_counter : 0 ≤ x.(message_counter);
  }.
End Valid.

Lemma old_levels_messages_encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True)
    Sc_rollup_inbox_repr.old_levels_messages_encoding.
Proof.
Admitted.
#[global] Hint Resolve old_levels_messages_encoding_is_valid : Data_encoding_db.

Axiom functional_extentionality_unit : ∀ {a : Set} (f1 f2 : unit → a),
  f1 tt = f2 tt → f1 = f2.

Lemma encoding_is_valid :
  Data_encoding.Valid.t Valid.t Sc_rollup_inbox_repr.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  repeat (split; try dtauto).
  destruct_all Sc_rollup_inbox_repr.t; f_equal.
  now apply functional_extentionality_unit.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.