🦏 Sc_rollup_metadata_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_metadata_repr.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_repr.

Module Valid.

Validity predicate for the type [Sc_rollup_metadata_repr.t].

  Record t (x : Sc_rollup_metadata_repr.t) : Prop := {
    origination_level :
        Raw_level_repr.Valid.t x.(Sc_rollup_metadata_repr.t.origination_level) ;
  }.

@TODO see if there is/should be a validity predicate for the field [address : Sc_rollup_repr.Address.t]

End Valid.

Propositional equality and [equal] are equivalent on [Sc_rollup_metada_repr.t].

Lemma equal_is_valid :
  Compare.Equal.Valid.t (fun _ ⇒ True) Sc_rollup_metadata_repr.equal.
Proof.
  unfold Compare.Equal.Valid.t.
  intros meta1 meta2 _ _.
  destruct meta1 as [add1 or_lev1], meta2 as [add2 or_lev2].
  unfold Sc_rollup_metadata_repr.equal. simpl in ×.
  split ; intro H.
  { inversion H. subst add2 or_lev2.
    apply Bool.andb_true_iff. split.
    { apply Sc_rollup_repr.Address.equal_is_valid ; try constructor. }
    { apply Raw_level_repr.equal_is_valid ; try constructor. }
  }
  { apply Bool.andb_true_iff in H. destruct H as [Hadd Hlev].
    apply Sc_rollup_repr.Address.equal_is_valid in Hadd ; try constructor.
    apply Raw_level_repr.equal_is_valid in Hlev ; try constructor.
    subst. reflexivity.
  }
Qed.

The [encoding] is valid.

Lemma encoding_is_valid :
  Data_encoding.Valid.t Valid.t
    Sc_rollup_metadata_repr.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.