🐆 Tx_rollup_state_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_level_repr.
Module range.
Module Interval.
Module Valid.
Import Proto_alpha.Tx_rollup_state_repr.range.Interval.
Record t (x : Tx_rollup_state_repr.range.Interval) : Prop := {
order : x.(oldest) ≤ x.(newest);
oldest : Tx_rollup_level_repr.Valid.t x.(oldest);
newest : Tx_rollup_level_repr.Valid.t x.(newest);
}.
End Valid.
End Interval.
Module Empty.
Module Valid.
Import Proto_alpha.Tx_rollup_state_repr.range.Empty.
Record t (x : Tx_rollup_state_repr.range.Empty) : Prop := {
next : Tx_rollup_level_repr.Valid.t x.(next);
}.
End Valid.
End Empty.
Module Valid.
Definition t (x : Tx_rollup_state_repr.range) : Prop :=
match x with
| Tx_rollup_state_repr.Interval x ⇒ Interval.Valid.t x
| Tx_rollup_state_repr.Empty x ⇒ Empty.Valid.t x
end.
End Valid.
End range.
Lemma range_encoding_is_valid : Data_encoding.Valid.t range.Valid.t
Tx_rollup_state_repr.range_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [] []; dtauto.
Qed.
#[global] Hint Resolve range_encoding_is_valid : Data_encoding_db.
Module Watermark.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_level_repr.
Module range.
Module Interval.
Module Valid.
Import Proto_alpha.Tx_rollup_state_repr.range.Interval.
Record t (x : Tx_rollup_state_repr.range.Interval) : Prop := {
order : x.(oldest) ≤ x.(newest);
oldest : Tx_rollup_level_repr.Valid.t x.(oldest);
newest : Tx_rollup_level_repr.Valid.t x.(newest);
}.
End Valid.
End Interval.
Module Empty.
Module Valid.
Import Proto_alpha.Tx_rollup_state_repr.range.Empty.
Record t (x : Tx_rollup_state_repr.range.Empty) : Prop := {
next : Tx_rollup_level_repr.Valid.t x.(next);
}.
End Valid.
End Empty.
Module Valid.
Definition t (x : Tx_rollup_state_repr.range) : Prop :=
match x with
| Tx_rollup_state_repr.Interval x ⇒ Interval.Valid.t x
| Tx_rollup_state_repr.Empty x ⇒ Empty.Valid.t x
end.
End Valid.
End range.
Lemma range_encoding_is_valid : Data_encoding.Valid.t range.Valid.t
Tx_rollup_state_repr.range_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [] []; dtauto.
Qed.
#[global] Hint Resolve range_encoding_is_valid : Data_encoding_db.
Module Watermark.
The validity condition for [watermark].
Module Valid.
Definition t (x : Tx_rollup_state_repr.watermark) : Prop :=
Option.Forall Tx_rollup_level_repr.Valid.t x.
End Valid.
End Watermark.
Module Valid.
Import Tx_rollup_state_repr.t.
Record t (x : Tx_rollup_state_repr.t) : Prop := {
finalized_commitments : range.Valid.t x.(finalized_commitments);
unfinalized_commitments : range.Valid.t x.(unfinalized_commitments);
uncommitted_inboxes : range.Valid.t x.(uncommitted_inboxes);
tezos_head_level :
Option.Forall Raw_level_repr.Valid.t x.(tezos_head_level);
burn_per_byte : Tez_repr.Valid.t x.(burn_per_byte);
inbox_ema : Pervasives.Int31.Valid.t x.(inbox_ema);
allocated_storage : 0 ≤ x.(allocated_storage);
occupied_storage : 0 ≤ x.(occupied_storage);
commitments_watermark : Watermark.Valid.t x.(commitments_watermark);
}.
End Valid.
Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t
Definition t (x : Tx_rollup_state_repr.watermark) : Prop :=
Option.Forall Tx_rollup_level_repr.Valid.t x.
End Valid.
End Watermark.
Module Valid.
Import Tx_rollup_state_repr.t.
Record t (x : Tx_rollup_state_repr.t) : Prop := {
finalized_commitments : range.Valid.t x.(finalized_commitments);
unfinalized_commitments : range.Valid.t x.(unfinalized_commitments);
uncommitted_inboxes : range.Valid.t x.(uncommitted_inboxes);
tezos_head_level :
Option.Forall Raw_level_repr.Valid.t x.(tezos_head_level);
burn_per_byte : Tez_repr.Valid.t x.(burn_per_byte);
inbox_ema : Pervasives.Int31.Valid.t x.(inbox_ema);
allocated_storage : 0 ≤ x.(allocated_storage);
occupied_storage : 0 ≤ x.(occupied_storage);
commitments_watermark : Watermark.Valid.t x.(commitments_watermark);
}.
End Valid.
Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t
The encoding [encoding] is valid.
Tx_rollup_state_repr.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [] []; qauto l: on.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Lemma initial_state_is_valid (pre_allocated_storage : Z.t) :
0 ≤ pre_allocated_storage →
Tx_rollup_state_repr.Valid.t
(Tx_rollup_state_repr.initial_state pre_allocated_storage).
Proof.
intros Hpre.
unfold_after Tx_rollup_state_repr.Valid.t; simpl.
easy.
Qed.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [] []; qauto l: on.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Lemma initial_state_is_valid (pre_allocated_storage : Z.t) :
0 ≤ pre_allocated_storage →
Tx_rollup_state_repr.Valid.t
(Tx_rollup_state_repr.initial_state pre_allocated_storage).
Proof.
intros Hpre.
unfold_after Tx_rollup_state_repr.Valid.t; simpl.
easy.
Qed.
Import and Abreviations for shortening [oldest] and [newest]
names in the proofs.
Import Tx_rollup_state_repr.t.
#[local] Notation oldest :=
Tx_rollup_state_repr.ConstructorRecords_range.range.Interval.oldest.
#[local] Notation newest :=
Tx_rollup_state_repr.ConstructorRecords_range.range.Interval.newest.
Lemma adjust_storage_allocation_is_valid
(state_value : Tx_rollup_state_repr.t) (delta_ : Z.t) :
state_value.(occupied_storage) +Z delta_ ≥ 0 →
Tx_rollup_state_repr.Valid.t state_value →
letP? '(state_value', _) := Tx_rollup_state_repr.adjust_storage_allocation
state_value delta_ in
Tx_rollup_state_repr.Valid.t state_value'.
Proof.
intros Hdelta Hvalid.
unfold Tx_rollup_state_repr.adjust_storage_allocation.
step; [easy|]; simpl.
step; [lia|].
step; simpl;
unfold with_occupied_storage; simpl;
destruct Hvalid;
constructor; simpl; try (easy || lia).
Qed.
(* @TODO *)
Lemma update_burn_per_byte_helper_is_valid
(state_value : Tx_rollup_state_repr.t)
(a b c : int) :
Tx_rollup_state_repr.Valid.t state_value →
Tx_rollup_state_repr.Valid.t (Tx_rollup_state_repr.update_burn_per_byte_helper
state_value a b c).
Proof.
intros Hvalid.
unfold_after Tx_rollup_state_repr.Valid.t.
destruct Hvalid; simpl.
step; simpl.
{ constructor; simpl; try easy.
Abort.
(* @TODO Finish the verfication of state transitions
each function that returns an [Tx_rollup_state_repr.t]
must be verified that it returns a valid state. The
functions remaining are listed below. *)
(* @TODO update_burn_per_byte_is_valid *)
(* @TODO record_inbox_creation_is_valid *)
(* @TODO record_inbox_deletion_is_valid *)
(* @TODO record_commitment_creation_is_valid *)
(* @TODO record_commitment_rejection_is_valid *)
(* @TODO record_commitment_deletion_is_valid *)
(* @TODO : Merge the above predicates in a single predicate about the
validy of rollup state and verify the state transitions *)
Definition right_cut_valid_range (r : Tx_rollup_state_repr.range)
(level : Tx_rollup_level_repr.level) : Prop :=
match r with
| Tx_rollup_state_repr.Interval x ⇒ x.(oldest) ≤ level ≤ x.(newest)
| Tx_rollup_state_repr.Empty _ ⇒ False
end.
Module Valid_belongs_to.
(* This comes from right_cut, but I didn't stop to better understand/formulate this *)
Definition t (state_value : Tx_rollup_state_repr.t)
(level : Tx_rollup_level_repr.level)
(predecessor_hash : option Tx_rollup_commitment_repr.Hash.t) : Prop :=
let pred_level := Tx_rollup_level_repr.pred level in
match pred_level with
| Some pred_level ⇒
(Tx_rollup_state_repr.belongs_to state_value.(unfinalized_commitments) pred_level ||
Tx_rollup_state_repr.belongs_to state_value.(finalized_commitments) pred_level = true ∧
predecessor_hash ≠ None ∨
Tx_rollup_state_repr.belongs_to state_value.(unfinalized_commitments) pred_level ||
Tx_rollup_state_repr.belongs_to state_value.(finalized_commitments) pred_level = false ∧
predecessor_hash = None)
| None ⇒ True
end.
End Valid_belongs_to.
Definition Rollup_state_consisitent
(state_value : Tx_rollup_state_repr.t) : Prop :=
state_value.(tezos_head_level) ≠ None
∧
((Tx_rollup_state_repr.range_newest
state_value.(uncommitted_inboxes) = None ∧
Tx_rollup_state_repr.range_oldest
state_value.(uncommitted_inboxes) = None)
∨
(Tx_rollup_state_repr.range_newest
state_value.(uncommitted_inboxes) ≠ None ∧
Tx_rollup_state_repr.range_oldest
state_value.(uncommitted_inboxes) ≠ None)).
#[local] Notation oldest :=
Tx_rollup_state_repr.ConstructorRecords_range.range.Interval.oldest.
#[local] Notation newest :=
Tx_rollup_state_repr.ConstructorRecords_range.range.Interval.newest.
Lemma adjust_storage_allocation_is_valid
(state_value : Tx_rollup_state_repr.t) (delta_ : Z.t) :
state_value.(occupied_storage) +Z delta_ ≥ 0 →
Tx_rollup_state_repr.Valid.t state_value →
letP? '(state_value', _) := Tx_rollup_state_repr.adjust_storage_allocation
state_value delta_ in
Tx_rollup_state_repr.Valid.t state_value'.
Proof.
intros Hdelta Hvalid.
unfold Tx_rollup_state_repr.adjust_storage_allocation.
step; [easy|]; simpl.
step; [lia|].
step; simpl;
unfold with_occupied_storage; simpl;
destruct Hvalid;
constructor; simpl; try (easy || lia).
Qed.
(* @TODO *)
Lemma update_burn_per_byte_helper_is_valid
(state_value : Tx_rollup_state_repr.t)
(a b c : int) :
Tx_rollup_state_repr.Valid.t state_value →
Tx_rollup_state_repr.Valid.t (Tx_rollup_state_repr.update_burn_per_byte_helper
state_value a b c).
Proof.
intros Hvalid.
unfold_after Tx_rollup_state_repr.Valid.t.
destruct Hvalid; simpl.
step; simpl.
{ constructor; simpl; try easy.
Abort.
(* @TODO Finish the verfication of state transitions
each function that returns an [Tx_rollup_state_repr.t]
must be verified that it returns a valid state. The
functions remaining are listed below. *)
(* @TODO update_burn_per_byte_is_valid *)
(* @TODO record_inbox_creation_is_valid *)
(* @TODO record_inbox_deletion_is_valid *)
(* @TODO record_commitment_creation_is_valid *)
(* @TODO record_commitment_rejection_is_valid *)
(* @TODO record_commitment_deletion_is_valid *)
(* @TODO : Merge the above predicates in a single predicate about the
validy of rollup state and verify the state transitions *)
Definition right_cut_valid_range (r : Tx_rollup_state_repr.range)
(level : Tx_rollup_level_repr.level) : Prop :=
match r with
| Tx_rollup_state_repr.Interval x ⇒ x.(oldest) ≤ level ≤ x.(newest)
| Tx_rollup_state_repr.Empty _ ⇒ False
end.
Module Valid_belongs_to.
(* This comes from right_cut, but I didn't stop to better understand/formulate this *)
Definition t (state_value : Tx_rollup_state_repr.t)
(level : Tx_rollup_level_repr.level)
(predecessor_hash : option Tx_rollup_commitment_repr.Hash.t) : Prop :=
let pred_level := Tx_rollup_level_repr.pred level in
match pred_level with
| Some pred_level ⇒
(Tx_rollup_state_repr.belongs_to state_value.(unfinalized_commitments) pred_level ||
Tx_rollup_state_repr.belongs_to state_value.(finalized_commitments) pred_level = true ∧
predecessor_hash ≠ None ∨
Tx_rollup_state_repr.belongs_to state_value.(unfinalized_commitments) pred_level ||
Tx_rollup_state_repr.belongs_to state_value.(finalized_commitments) pred_level = false ∧
predecessor_hash = None)
| None ⇒ True
end.
End Valid_belongs_to.
Definition Rollup_state_consisitent
(state_value : Tx_rollup_state_repr.t) : Prop :=
state_value.(tezos_head_level) ≠ None
∧
((Tx_rollup_state_repr.range_newest
state_value.(uncommitted_inboxes) = None ∧
Tx_rollup_state_repr.range_oldest
state_value.(uncommitted_inboxes) = None)
∨
(Tx_rollup_state_repr.range_newest
state_value.(uncommitted_inboxes) ≠ None ∧
Tx_rollup_state_repr.range_oldest
state_value.(uncommitted_inboxes) ≠ None)).
The function [burn_cost] is valid.
Lemma burn_cost_is_valid limit state_value size_value :
Option.Forall Tez_repr.Valid.t limit →
Valid.t state_value →
Pervasives.Int.Valid.t size_value →
letP? cost := Tx_rollup_state_repr.burn_cost limit state_value size_value in
Tez_repr.Valid.t cost.
Proof.
Admitted.
(* The function [check_level_can_be_rejected] is valid. *)
Lemma check_level_can_be_rejected_is_valid state_value level :
Tx_rollup_level_repr.Valid.t level →
letP? _ := Tx_rollup_state_repr.check_level_can_be_rejected
state_value level
in True.
Proof.
Admitted.
Option.Forall Tez_repr.Valid.t limit →
Valid.t state_value →
Pervasives.Int.Valid.t size_value →
letP? cost := Tx_rollup_state_repr.burn_cost limit state_value size_value in
Tez_repr.Valid.t cost.
Proof.
Admitted.
(* The function [check_level_can_be_rejected] is valid. *)
Lemma check_level_can_be_rejected_is_valid state_value level :
Tx_rollup_level_repr.Valid.t level →
letP? _ := Tx_rollup_state_repr.check_level_can_be_rejected
state_value level
in True.
Proof.
Admitted.