Skip to main content

🦏 Sc_rollup_metadata_repr.v


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].
@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.
  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.

The [encoding] is valid.
Lemma encoding_is_valid :
  Data_encoding.Valid.t Valid.t
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.