🐆 Tx_rollup_state_repr.v

Proofs

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

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.

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 :=
  Tx_rollup_state_repr.ConstructorRecords_range.range.Interval.oldest.
#[local] Notation newest :=
  Tx_rollup_state_repr.ConstructorRecords_range.range.Interval.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).
Proof.
  intros Hpre.
  unfold_after Valid.t; simpl.
  easy.
Qed.

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'.
Proof.
  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).
Qed.

(* @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).
Proof.
  intros Hvalid.
  unfold_after 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)).

[shrink] does not return [Internal_error] as long as the [range] argument is [Internval _]

Lemma shrink_no_internal_error
  (x : Tx_rollup_state_repr.ConstructorRecords_range.range.Interval_skeleton
         Tx_rollup_level_repr.t Tx_rollup_level_repr.t) :
  Error.No_internal_errors.t
    (Tx_rollup_state_repr.shrink (Tx_rollup_state_repr.Interval x)).
Proof.
  intros.
  unfold Tx_rollup_state_repr.shrink.
  now step.
Qed.

[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 →
  Error.No_internal_errors.t
    (Tx_rollup_state_repr.right_cut range level).
Proof.
  intros.
  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:?.
Qed.

[adjust_storage_allocation] does not return [Internal_error]

Lemma adjust_storage_allocation_no_internal_error (state_value : Tx_rollup_state_repr.t) (delta : Z.t) :
  state_value.(Tx_rollup_state_repr.t.occupied_storage) +Z delta > 0 →
  Error.No_internal_errors.t
    (Tx_rollup_state_repr.adjust_storage_allocation state_value delta).
Proof.
  intros.
  unfold Tx_rollup_state_repr.adjust_storage_allocation.
  destruct Z.equal; [easy|].
  replace (state_value.(Tx_rollup_state_repr.t.occupied_storage) +Z delta <Z Z.zero) with false by lia.
  now step.
Qed.

[left_extend] does not return [Internal_error]

Lemma left_extend_no_intenral_error range level :
  Error.No_internal_errors.t (Tx_rollup_state_repr.left_extend range level).
Proof.
  unfold Tx_rollup_state_repr.left_extend.
  now step.
Qed.

[record_inbox_creation] does not return [Internal_error]

Lemma record_inbox_creation_no_internal_error
  (t_value : Tx_rollup_state_repr.t) (level : Raw_level_repr.raw_level) (delta : Z.t) :
  t_value.(Tx_rollup_state_repr.t.occupied_storage) +Z Tx_rollup_inbox_repr.size_value > 0 →
  t_value.(Tx_rollup_state_repr.t.tezos_head_level) = None →
  Error.No_internal_errors.t (Tx_rollup_state_repr.record_inbox_creation t_value level).
Proof.
  intros Hzero HNone.
  unfold Tx_rollup_state_repr.record_inbox_creation.
  rewrite HNone. simpl.
  destruct Tx_rollup_state_repr.extend; try easy.
  unfold Tx_rollup_state_repr.adjust_storage_allocation.
  step; [easy|].
  replace (_ +Z _ <? Z.zero) with false by lia.
  now step.
Qed.

[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 →
  Error.No_internal_errors.t
    (Tx_rollup_state_repr.record_commitment_rejection
       state_value level predecessor_hash).
Proof.
  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.
Qed.

[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 →
  Error.No_internal_errors.t
    (Tx_rollup_state_repr.next_commitment_level
      state_value current_level).
Proof.
  intros.
  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.
Qed.

[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) →
  Error.No_internal_errors.t
    (Tx_rollup_state_repr.record_inbox_deletion state_value
       candidate).
Proof.
  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.
Qed.

[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 →
  Error.No_internal_errors.t
     (Tx_rollup_state_repr.record_commitment_creation state_value
         level hash_value).
Proof.
  intros Hvalid Huinb Hlevel Hocc Hsize_value.
  unfold Tx_rollup_state_repr.record_commitment_creation,
    Tx_rollup_state_repr.range_oldest,
    error_unless,
    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_outer.
  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.
Qed.

[record_commitment_deletion] does not return [Internal_error]

Lemma record_commitment_deletion_no_internal_error
  (state_value : Tx_rollup_state_repr.t)
  (level : Tx_rollup_level_repr.t)
  (hash_value : Tx_rollup_commitment_repr.Hash.t)
  (message_hash : Tx_rollup_message_result_hash_repr.t)
  (i : Tx_rollup_state_repr.ConstructorRecords_range.range.Interval_skeleton Tx_rollup_level_repr.t
        Tx_rollup_level_repr.t) :
  state_value.(finalized_commitments) =
    Tx_rollup_state_repr.Interval i →
  level = oldest i →
  Error.No_internal_errors.t
    (Tx_rollup_state_repr.record_commitment_deletion
       state_value level hash_value message_hash).
Proof.
  intros Hfin Hlevel.
  unfold Tx_rollup_state_repr.record_commitment_deletion.
  rewrite Hfin; simpl.
  unfold_match; simpl.
  rewrite Hlevel, Z.eqb_refl; simpl.
  unfold op_gtgtquestion.
  pose proof shrink_no_internal_error as Hshrink.
  specialize (Hshrink i).
  now step.
Qed.