Skip to main content

🐆 Tx_rollup_state_repr.v


See code, Gitlab , OCaml

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

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

Require TezosOfOCaml.Environment.V7.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 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.

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

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

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

The function [burn_cost] is valid.