🐆 Tx_rollup_inbox_storage.v
Translated 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.
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
| None ⇒ return? (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.
(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
| None ⇒ return? (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.
(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.