Skip to main content

🐆 Tx_rollup_state_repr.v


See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_repr.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
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 xInterval.Valid.t x
      | Tx_rollup_state_repr.Empty xEmpty.Valid.t x
  End Valid.
End range.

Lemma range_encoding_is_valid : Data_encoding.Valid.t range.Valid.t
  intros [] []; dtauto.
#[global] Hint Resolve range_encoding_is_valid : Data_encoding_db.

Module Watermark.
The validity condition for [watermark].
The encoding [encoding] is valid.
  intros [] []; qauto l: on.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Verification of no internal errors below

Import and Abreviations for shortening [oldest] and [newest] names in the proofs.
Import Tx_rollup_state_repr.t.
#[local] Notation oldest :=
#[local] Notation newest :=

Lemma initial_state_is_valid (pre_allocated_storage : Z.t) :
  0 pre_allocated_storage
  Valid.t (Tx_rollup_state_repr.initial_state pre_allocated_storage).
  intros Hpre.
  unfold_after Valid.t; simpl.

Lemma adjust_storage_allocation_is_valid
  (state_value : Tx_rollup_state_repr.t) (delta_ : Z.t) :
  state_value.(occupied_storage) +Z delta_ 0
  Valid.t state_value
  letP? '(state_value', _) := Tx_rollup_state_repr.adjust_storage_allocation
                                state_value delta_ in
    Valid.t state_value'.
  intros Hdelta Hvalid.
  unfold Tx_rollup_state_repr.adjust_storage_allocation.
  step; [easy|]; simpl.
  step; [easy|].
  step; simpl;
  unfold with_occupied_storage; simpl;
  destruct Hvalid;
  constructor; simpl; try (easy || lia).

(* @TODO *)
Lemma update_burn_per_byte_helper_is_valid
      (state_value : Tx_rollup_state_repr.t)
      (a b c : int) :
  Valid.t state_value
  Valid.t (Tx_rollup_state_repr.update_burn_per_byte_helper
             state_value a b c).
  intros Hvalid.
  unfold_after Valid.t.
  destruct Hvalid; simpl.
  step; simpl.
  { constructor; simpl; try easy.

(* @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 xx.(oldest) level x.(newest)
  | Tx_rollup_state_repr.Empty _False

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)
    | NoneTrue
End Valid_belongs_to.

Definition Rollup_state_consisitent
  (state_value : Tx_rollup_state_repr.t) : Prop :=
  state_value.(tezos_head_level) None
    state_value.(uncommitted_inboxes) = None
    state_value.(uncommitted_inboxes) = None)
    state_value.(uncommitted_inboxes) None
    state_value.(uncommitted_inboxes) None)).

[shrink] does not return [Internal_error] as long as the [range] argument is [Internval _]
[right_cut] does not return [Internal_error]
Lemma right_cut_no_internal_error
  (range : Tx_rollup_state_repr.range)
  (level : Tx_rollup_level_repr.level) :
  right_cut_valid_range range level
    (Tx_rollup_state_repr.right_cut range level).
  unfold right_cut_valid_range in H.
  unfold Tx_rollup_state_repr.right_cut.
  destruct Tx_rollup_level_repr.pred eqn:?; [|easy]; simpl.
  destruct range; [|easy].
  destruct H as [H1 H2].
  apply Zle_imp_le_bool in H1.
  apply Zle_imp_le_bool in H2.
  simpl. unfold Tx_rollup_level_repr.op_lteq; simpl.
  simpl in ×.
  set (cond1 := _ <=? level).
  set (cond2 := level <=? _).
  assert (Hcond1 : cond1 = true)
    by (cbv; cbv in H1; now rewrite H1).
  assert (Hcond2 : cond2 = true)
    by (cbv; cbv in H2; now rewrite H2).
  rewrite Hcond1, Hcond2. simpl.
  now destruct (_ <=? i) eqn:?.

[adjust_storage_allocation] does not return [Internal_error]
[left_extend] does not return [Internal_error]
[record_inbox_creation] does not return [Internal_error]
[record_commitment_rejection_creation] does not return [Internal_error]
Lemma record_commitment_rejection_no_internal_error
  (state_value : Tx_rollup_state_repr.t) (level : Tx_rollup_level_repr.t)
  (predecessor_hash : option Tx_rollup_commitment_repr.Hash.t) :
  Valid.t state_value
  right_cut_valid_range state_value.(unfinalized_commitments) level
  Valid_belongs_to.t state_value level predecessor_hash
  state_value.(last_removed_commitment_hashes) None
       state_value level predecessor_hash).
  intros HValid Hright_cut Hbelongs_to Hlast.
  unfold Tx_rollup_state_repr.record_commitment_rejection.
  unfold op_gtgtquestion.
  pose proof left_extend_no_intenral_error as Hleft.
  specialize (Hleft state_value.(uncommitted_inboxes) level).
  step; [|assumption].
  unfold with_uncommitted_inboxes; simpl.
  clear Hleft Heqr.
  step; [|
    pose proof right_cut_no_internal_error as Hright;
    specialize (Hright state_value.(unfinalized_commitments) level);
    rewrite Heqt in Hright; now apply Hright].
  step; [|easy].
  unfold Valid_belongs_to.t in Hbelongs_to.
  rewrite Heqo in Hbelongs_to;
    destruct Hbelongs_to as [[Hb Hb'] | [Hb Hb']];
    [step; [now destruct predecessor_hash|easy]|].
  step; [now destruct predecessor_hash|].
  destruct predecessor_hash; [easy|]; simpl.
  destruct HValid; simpl.
  destruct state_value; simpl.
  destruct last_removed_commitment_hashes0; [|easy]; simpl.
  now destruct p.

[next_commitment_level] does not return [Internal_error]
Lemma next_commitment_level_no_internal_error
  (state_value : Tx_rollup_state_repr.t)
  (current_level : Raw_level_repr.raw_level) :
  Rollup_state_consisitent state_value
      state_value current_level).
  unfold Tx_rollup_state_repr.next_commitment_level.
  destruct H as [Hhead [[Hnewest Holdest] | [Hnewest Holdest]]];
  do 2 step; simpl; try easy.
  step; [easy|].
  step; [|easy].
  unfold error_when.
  now step.

[record_inbox_deletion] does not return [Internal_error]
Lemma record_inbox_deletion_no_internal_error
  (state_value : Tx_rollup_state_repr.t)
  (candidate : Tx_rollup_level_repr.level)
  (i : Tx_rollup_state_repr.ConstructorRecords_range.range.Interval_skeleton
       Tx_rollup_level_repr.t Tx_rollup_level_repr.t) :
  state_value.(unfinalized_commitments) =
    Tx_rollup_state_repr.Interval i
  candidate = (oldest i)
    (Tx_rollup_state_repr.record_inbox_deletion state_value
  intros Hinter Hcand.
  unfold Tx_rollup_state_repr.record_inbox_deletion.
  unfold Tx_rollup_state_repr.range_oldest in ×.
  rewrite Hinter, Hcand.
  unfold Tx_rollup_level_repr.op_eq; simpl.
  rewrite <- Hcand.
  rewrite <- Hcand at 1.
  rewrite Z.eqb_refl.
  pose proof shrink_no_internal_error as Hshrink.
  specialize (Hshrink i).
  unfold op_gtgtquestion.
  step; [|easy].
  unfold Tx_rollup_state_repr.extend.
  now step.

[record_commitment_creation] does not return [Internal_error]
Lemma record_commitment_creation_no_internal_error
  (state_value : Tx_rollup_state_repr.t)
  (level : Tx_rollup_level_repr.level)
  (hash_value : Tx_rollup_commitment_repr.Hash.t)
  (i : Tx_rollup_state_repr.ConstructorRecords_range.range.Interval_skeleton
         Tx_rollup_level_repr.t Tx_rollup_level_repr.t) :
  Valid.t state_value
  state_value.(uncommitted_inboxes) =
    Tx_rollup_state_repr.Interval i
  level = (oldest i)
  state_value.(occupied_storage) > Tx_rollup_inbox_repr.size_value
  0 Tx_rollup_inbox_repr.size_value
     (Tx_rollup_state_repr.record_commitment_creation state_value
         level hash_value).
  intros Hvalid Huinb Hlevel Hocc Hsize_value.
  unfold Tx_rollup_state_repr.record_commitment_creation,
    Tx_rollup_level_repr.op_eq; simpl.
  rewrite Huinb, Hlevel.
  rewrite <- Hlevel.
  rewrite <- Hlevel at 1.
  rewrite Z.eqb_refl.
  pose proof shrink_no_internal_error as Hshrink.
  specialize (Hshrink i).
  unfold op_gtgtquestion; simpl.
  step; [|easy].
  unfold Tx_rollup_state_repr.extend.
  step; [|easy].
  pose proof adjust_storage_allocation_no_internal_error
    as Hadjust.
  set (state_value' := with_commitment_newest_hash _ _).
  set (level' := neg _).
  specialize (Hadjust state_value' level').
  step; [|
    apply Hadjust; destruct Hvalid;
    subst state_value'; simpl; lia].
  now destruct p.

[record_commitment_deletion] does not return [Internal_error]