🐆 Tx_rollup_commitment_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Blake2B.
Require TezosOfOCaml.Environment.V8.Proofs.Context_hash.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_message_result_hash_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_withdraw_repr.
Module Hash.
Lemma encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True)
Tx_rollup_commitment_repr.Hash.encoding.
Proof.
apply Blake2B.Make_is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Blake2B.
Require TezosOfOCaml.Environment.V8.Proofs.Context_hash.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_message_result_hash_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_withdraw_repr.
Module Hash.
Lemma encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True)
Tx_rollup_commitment_repr.Hash.encoding.
Proof.
apply Blake2B.Make_is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
[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.
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.
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.
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 := {
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
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.
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.
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.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.
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.
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.