🐆 Tx_rollup_commitment_repr.v

Proofs

[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.

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.

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.