Skip to main content

🐆 Tx_rollup_inbox_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_errors_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_gas.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_hash_builder.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_repr.

Definition find
  (ctxt : Raw_context.t) (level : Tx_rollup_level_repr.t)
  (tx_rollup : Tx_rollup_repr.t)
  : M? (Raw_context.t × option Tx_rollup_inbox_repr.t) :=
  Storage.Tx_rollup.Inbox.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
    (ctxt, tx_rollup) level.

Definition get
  (ctxt : Raw_context.t) (level : Tx_rollup_level_repr.t)
  (tx_rollup : Tx_rollup_repr.t)
  : M? (Raw_context.t × Tx_rollup_inbox_repr.t) :=
  let? function_parameter := find ctxt level tx_rollup in
  match function_parameter with
  | (_, None)
    Error_monad.tzfail
      (Build_extensible "Inbox_does_not_exist"
        (Tx_rollup_repr.t × Tx_rollup_level_repr.t) (tx_rollup, level))
  | (ctxt, Some inbox_value)return? (ctxt, inbox_value)
  end.

[prepare_inbox ctxt rollup state level] prepares the metadata for an inbox at [level], which may imply creating it if it does not already exist.
Definition prepare_inbox
  (ctxt : Raw_context.t) (rollup : Tx_rollup_repr.t)
  (state_value : Tx_rollup_state_repr.t) (level : Raw_level_repr.t)
  : M?
    (Raw_context.t × Tx_rollup_state_repr.t × Tx_rollup_level_repr.t ×
      Tx_rollup_inbox_repr.t × Z.t) :=
  let? '_ :=
    Error_monad.fail_when
      ((Constants_storage.tx_rollup_max_inboxes_count ctxt) i
      (Tx_rollup_state_repr.inboxes_count state_value))
      (Build_extensible "Too_many_inboxes" unit tt) in
  let current_levels := Tx_rollup_state_repr.head_levels state_value in
  match
    (current_levels,
      match current_levels with
      | Some (_, tezos_lvl)Raw_level_repr.op_lt level tezos_lvl
      | _false
      end,
      match current_levels with
      | Some (tx_lvl, tezos_lvl)Raw_level_repr.op_eq tezos_lvl level
      | _false
      end) with
  | (Some (_, tezos_lvl), true, _)
    Error_monad.tzfail
      (Build_extensible "Internal_error" string
        "Trying to write into an inbox from the past")
  | (Some (tx_lvl, tezos_lvl), _, true)
    let? '(ctxt, metadata) :=
      Storage.Tx_rollup.Inbox.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
        (ctxt, rollup) tx_lvl in
    return? (ctxt, state_value, tx_lvl, metadata, Z.zero)
  | (_, _, _)
    let pred_level_and_tx_level :=
      Option.bind current_levels
        (fun (function_parameter : Tx_rollup_level_repr.t × Raw_level_repr.t) ⇒
          let '(tx_level, tezos_level) := function_parameter in
          Option.map
            (fun (pred : Tx_rollup_level_repr.level) ⇒ (pred, tezos_level))
            (Tx_rollup_level_repr.pred tx_level)) in
    let? '(ctxt, state_value) :=
      match pred_level_and_tx_level with
      | Nonereturn? (ctxt, state_value)
      | Some (tx_level, tezos_level)
        let? '(ctxt, minbox) := find ctxt tx_level rollup in
        let final_size :=
          match minbox with
          | Some inbox_value
            inbox_value.(Tx_rollup_inbox_repr.t.cumulated_size)
          | None ⇒ 0
          end in
        let hard_limit :=
          Constants_storage.tx_rollup_hard_size_limit_per_inbox ctxt in
        let factor := Constants_storage.tx_rollup_cost_per_byte_ema_factor ctxt
          in
        let diff_value := Raw_level_repr.diff_value level tezos_level in
        let elapsed :=
          if diff_value i32 Int32.one then
            0
          else
            Int32.to_int diff_value in
        let state_value :=
          Tx_rollup_state_repr.update_burn_per_byte state_value elapsed factor
            final_size hard_limit in
        let? '(ctxt, _, _) :=
          Storage.Tx_rollup.State.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
            ctxt rollup state_value in
        return? (ctxt, state_value)
      end in
    let? '(state_value, tx_level, paid_storage_space_diff) :=
      Tx_rollup_state_repr.record_inbox_creation state_value level in
    let inbox_value := Tx_rollup_inbox_repr.empty in
    let? '(ctxt, _inbox_size_alloc) :=
      Storage.Tx_rollup.Inbox.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
        (ctxt, rollup) tx_level inbox_value in
    return? (ctxt, state_value, tx_level, inbox_value, paid_storage_space_diff)
  end.

[update_inbox inbox msg_size] updates [metadata] to account for a new message of [msg_size] bytes.
Definition update_inbox
  (metadata : Tx_rollup_inbox_repr.t) (msg_size : int)
  (merkle_root : Tx_rollup_inbox_repr.Merkle.root) : Tx_rollup_inbox_repr.t :=
  {|
    Tx_rollup_inbox_repr.t.inbox_length :=
      1 +i metadata.(Tx_rollup_inbox_repr.t.inbox_length);
    Tx_rollup_inbox_repr.t.cumulated_size :=
      msg_size +i metadata.(Tx_rollup_inbox_repr.t.cumulated_size);
    Tx_rollup_inbox_repr.t.merkle_root := merkle_root; |}.

Definition append_message
  (ctxt : Raw_context.t) (rollup : Tx_rollup_repr.t)
  (state_value : Tx_rollup_state_repr.t) (message : Tx_rollup_message_repr.t)
  : M? (Raw_context.t × Tx_rollup_state_repr.t × Z.t) :=
  let level := (Raw_context.current_level ctxt).(Level_repr.t.level) in
  let message_size := Tx_rollup_message_repr.size_value message in
  let?
    '(ctxt, new_state, tx_level, inbox_value,
      paid_storage_space_diff_for_init_inbox) :=
    prepare_inbox ctxt rollup state_value level in
  let? '_ :=
    Error_monad.fail_when
      (inbox_value.(Tx_rollup_inbox_repr.t.inbox_length) i
      (Constants_storage.tx_rollup_max_messages_per_inbox ctxt))
      (Build_extensible "Inbox_count_would_exceed_limit" Tx_rollup_repr.t rollup)
    in
  let? '(ctxt, message_hash) := Tx_rollup_hash_builder.message ctxt message in
  let? ctxt := Tx_rollup_gas.consume_add_message_cost ctxt in
  let '(ctxt, inbox_merkle_root) :=
    Raw_context.Tx_rollup.add_message ctxt rollup message_hash in
  let new_inbox := update_inbox inbox_value message_size inbox_merkle_root in
  let new_size := new_inbox.(Tx_rollup_inbox_repr.t.cumulated_size) in
  let inbox_limit := Constants_storage.tx_rollup_hard_size_limit_per_inbox ctxt
    in
  let? '_ :=
    Error_monad.fail_unless (new_size i inbox_limit)
      (Build_extensible "Inbox_size_would_exceed_limit" Tx_rollup_repr.t rollup)
    in
  let? '(ctxt, new_inbox_size_alloc, _) :=
    Storage.Tx_rollup.Inbox.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
      (ctxt, rollup) tx_level new_inbox in
  let? '(new_state, paid_storage_space_diff) :=
    Tx_rollup_state_repr.adjust_storage_allocation new_state
      (Z.of_int new_inbox_size_alloc) in
  return?
    (ctxt, new_state,
      (paid_storage_space_diff_for_init_inbox +Z paid_storage_space_diff)).

Definition remove
  (ctxt : Raw_context.t) (level : Tx_rollup_level_repr.t)
  (rollup : Tx_rollup_repr.t) : M? Raw_context.t :=
  let? '(ctxt, _freed, _) :=
    Storage.Tx_rollup.Inbox.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove)
      (ctxt, rollup) level in
  return? ctxt.

Definition check_message_hash
  (ctxt : Raw_context.t) (level : Tx_rollup_level_repr.t)
  (tx_rollup : Tx_rollup_repr.t) (position : int)
  (message : Tx_rollup_message_repr.t) (path : Tx_rollup_inbox_repr.Merkle.path)
  : M? Raw_context.t :=
  let? '(ctxt, inbox_value) :=
    Storage.Tx_rollup.Inbox.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
      (ctxt, tx_rollup) level in
  let? '(ctxt, message_hash) := Tx_rollup_hash_builder.message ctxt message in
  let? ctxt := Tx_rollup_gas.consume_check_path_inbox_cost ctxt in
  let? b_value :=
    Tx_rollup_inbox_repr.Merkle.check_path path position message_hash
      inbox_value.(Tx_rollup_inbox_repr.t.merkle_root) in
  let? '_ :=
    Error_monad.fail_unless b_value
      (Build_extensible "Wrong_message_path"
        Tx_rollup_errors_repr.Wrong_message_path
        {|
          Tx_rollup_errors_repr.Wrong_message_path.expected :=
            inbox_value.(Tx_rollup_inbox_repr.t.merkle_root); |}) in
  return? ctxt.