Skip to main content

🐆 Tx_rollup_commitment_repr.v

Proofs

See code, Gitlab , OCaml

[Tx_rollup_commitment_repr.Hash.compare] is valid.
Definition is by [Blake2B.Make], for which we have proof, so, just use it.
  Lemma compare_is_valid :
    Compare.Valid.t (fun _True) id Tx_rollup_commitment_repr.Hash.compare.
  Proof.
    apply Blake2B.Make_is_valid.
  Qed.
End Hash.

Module Merkle_hash.
  Lemma encoding_is_valid :
    Data_encoding.Valid.t (fun _True)
      Tx_rollup_commitment_repr.Merkle_hash.encoding.
  Proof.
    apply Blake2B.Make_is_valid.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.

[Tx_rollup_commitment_repr.Merkle_hash.compare] is valid.
Definition is by [Blake2B.Make], for which we have proof, so, just use it.
  Lemma compare_is_valid :
    Compare.Valid.t (fun _True) id Tx_rollup_commitment_repr.Merkle_hash.compare.
  Proof.
    apply Blake2B.Make_is_valid.
  Qed.
End Merkle_hash.

This is a generic template to model Valid.t
Module Template.
  Module Valid.
    Import Proto_alpha.Tx_rollup_commitment_repr.template.

    Record t {a : Set} (domain: a Prop) (r : Tx_rollup_commitment_repr.template a ) : Prop := {
        level : Raw_level_repr.Valid.t r.(level);
        messages : domain r.(messages);
      }.
  End Valid.
End Template.

Module Compact.
Valid module for the excerpt record in Compact Module
  Module Excerpt.
    Module Valid.
      Import Proto_alpha.Tx_rollup_commitment_repr.Compact.excerpt.
      Record t (r : Tx_rollup_commitment_repr.Compact.excerpt) : Prop := {
        
Proof of validity for count field
        count : Pervasives.Int31.Valid.t r.(count)
      }.
    End Valid.
  End Excerpt.

  Module Valid.
Definition used to prove validity of Compact using Template
    Definition t (x : Tx_rollup_commitment_repr.Compact.t) : Prop :=
      Template.Valid.t Excerpt.Valid.t x.
  End Valid.

  Lemma encoding_is_valid :
    Data_encoding.Valid.t Valid.t Tx_rollup_commitment_repr.Compact.encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
    sauto.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Compact.

Module Full.
  Module Valid.
Valid Definition for Full Module
    Definition t (x : Tx_rollup_commitment_repr.Full.t) : Prop :=
      Template.Valid.t (fun _True) x.
  End Valid.

  Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t
    Tx_rollup_commitment_repr.Full.encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
      sauto l: on.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Full.

Module Index.
Lemma requires no extra Valid function because Index is a Hash type and it has it's Valid Definition which can be resolved using the Hint provided
  Lemma encoding_is_valid : Data_encoding.Valid.t (fun _True)
    Tx_rollup_commitment_repr.Index.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.

[Tx_rollup_commitment_repr.Index.compare] is valid.
Definition is just [Hash.compare], for which we already have a proof, so, just use it.
  Lemma compare_is_valid :
    Compare.Valid.t (fun _True) id Tx_rollup_commitment_repr.Index.compare.
  Proof.
    apply Hash.compare_is_valid.
  Qed.
End Index.

Module Submitted_commitment.
  Module Valid.
Record with Valid Definitions for the Lemma to use this Valid Module
    Import Proto_alpha.Tx_rollup_commitment_repr.Submitted_commitment.t.
    Record t (x : Tx_rollup_commitment_repr.Submitted_commitment.t) : Prop := {
      commitment : Compact.Valid.t x.(commitment);
      submitted_at : Raw_level_repr.Valid.t x.(submitted_at);
      finalized_at : Option.Forall Raw_level_repr.Valid.t x.(finalized_at)
    }.
  End Valid.
  Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t
    Tx_rollup_commitment_repr.Submitted_commitment.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Submitted_commitment.