🦏 Sc_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.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_costs.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_merkelized_payload_hashes_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Module Store := Storage.Sc_rollup.
Definition update_num_and_size_of_messages
(num_messages : int) (total_messages_size : int)
(message : Sc_rollup_inbox_message_repr.serialized) : int × int :=
((num_messages +i 1), (total_messages_size +i (String.length message))).
Definition get_inbox (ctxt : Raw_context.t)
: M? (Sc_rollup_inbox_repr.V1.t × Raw_context.t) :=
let? inbox_value := Store.Inbox.(Storage_sigs.Single_data_storage.get) ctxt in
return? (inbox_value, ctxt).
Definition _assert_inbox_nb_messages_in_commitment_period
(ctxt : Raw_context.t) (inbox_value : Sc_rollup_inbox_repr.t)
(extra_messages : int) : M? unit :=
let nb_messages_in_commitment_period :=
(Sc_rollup_inbox_repr.number_of_messages_during_commitment_period
inbox_value) +i64 (Int64.of_int extra_messages) in
let limit :=
Int64.of_int
(Constants_storage.sc_rollup_max_number_of_messages_per_commitment_period
ctxt) in
Error_monad.fail_when (nb_messages_in_commitment_period >i64 limit)
(Build_extensible
"Sc_rollup_max_number_of_messages_reached_for_commitment_period" unit tt).
Definition add_messages_aux
(ctxt : Raw_context.t)
(messages : list Sc_rollup_inbox_message_repr.serialized)
: M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
let '{| Level_repr.t.level := level |} := Raw_context.current_level ctxt in
let? '(inbox_value, ctxt) := get_inbox ctxt in
let? '(num_messages, total_messages_size, ctxt) :=
List.fold_left_es
(fun (function_parameter : int × int × Raw_context.t) ⇒
let '(num_messages, total_messages_size, ctxt) := function_parameter in
fun (message : Sc_rollup_inbox_message_repr.serialized) ⇒
let? ctxt :=
Raw_context.consume_gas ctxt
Sc_rollup_costs.Constants.cost_update_num_and_size_of_messages in
let '(num_messages, total_messages_size) :=
update_num_and_size_of_messages num_messages total_messages_size
message in
return? (num_messages, total_messages_size, ctxt)) (0, 0, ctxt)
messages in
let cost_add_serialized_messages :=
Sc_rollup_costs.cost_add_serialized_messages num_messages
total_messages_size 0 in
let? ctxt := Raw_context.consume_gas ctxt cost_add_serialized_messages in
let current_messages :=
Raw_context.Sc_rollup_in_memory_inbox.current_messages ctxt in
let? '(current_messages, inbox_value) :=
Sc_rollup_inbox_repr.add_messages_no_history inbox_value level messages
current_messages in
let ctxt :=
Raw_context.Sc_rollup_in_memory_inbox.set_current_messages ctxt
current_messages in
let? ctxt :=
Store.Inbox.(Storage_sigs.Single_data_storage.update) ctxt inbox_value in
return? (inbox_value, Z.zero, ctxt).
Definition serialize_external_messages
(ctxt : Raw_context.t) (external_messages : list string)
: M? (Raw_context.t × list Sc_rollup_inbox_message_repr.serialized) :=
List.fold_left_map_e
(fun (ctxt : Raw_context.t) ⇒
fun (message : string) ⇒
let? ctxt :=
let bytes_len := String.length message in
Raw_context.consume_gas ctxt
(Sc_rollup_costs.cost_serialize_external_inbox_message bytes_len) in
let? serialized_message :=
Sc_rollup_inbox_message_repr.serialize
(Sc_rollup_inbox_message_repr.External message) in
return? (ctxt, serialized_message)) ctxt external_messages.
Definition serialize_internal_message
(ctxt : Raw_context.t)
(internal_message : Sc_rollup_inbox_message_repr.internal_inbox_message)
: M? (Sc_rollup_inbox_message_repr.serialized × Raw_context.t) :=
let? ctxt :=
Raw_context.consume_gas ctxt
(Sc_rollup_costs.cost_serialize_internal_inbox_message internal_message)
in
let? message :=
Sc_rollup_inbox_message_repr.serialize
(Sc_rollup_inbox_message_repr.Internal internal_message) in
return? (message, ctxt).
Definition add_external_messages
(ctxt : Raw_context.t) (external_messages : list string)
: M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
let? '(ctxt, messages) := serialize_external_messages ctxt external_messages
in
add_messages_aux ctxt messages.
Definition add_internal_message
(ctxt : Raw_context.t)
(internal_message : Sc_rollup_inbox_message_repr.internal_inbox_message)
: M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
let? '(message, ctxt) := serialize_internal_message ctxt internal_message in
add_messages_aux ctxt [ message ].
Definition add_deposit
(ctxt : Raw_context.t) (payload : Script_repr.expr) (sender : Contract_hash.t)
(source : Signature.public_key_hash) (destination : Sc_rollup_repr.Address.t)
: M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
let internal_message :=
Sc_rollup_inbox_message_repr.Transfer
{|
Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.payload :=
payload;
Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.sender :=
sender;
Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.source :=
source;
Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.destination
:= destination; |} in
add_internal_message ctxt internal_message.
Definition add_start_of_level (ctxt : Raw_context.t)
: M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
add_internal_message ctxt Sc_rollup_inbox_message_repr.Start_of_level.
Definition add_end_of_level (ctxt : Raw_context.t)
: M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
add_internal_message ctxt Sc_rollup_inbox_message_repr.End_of_level.
Definition add_info_per_level
(ctxt : Raw_context.t) (timestamp : Time.t) (predecessor : Block_hash.t)
: M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
add_internal_message ctxt
(Sc_rollup_inbox_message_repr.Info_per_level
{|
Sc_rollup_inbox_message_repr.internal_inbox_message.Info_per_level.timestamp
:= timestamp;
Sc_rollup_inbox_message_repr.internal_inbox_message.Info_per_level.predecessor
:= predecessor; |}).
Definition init_value
(timestamp : Time.t) (predecessor : Block_hash.t) (ctxt : Raw_context.t)
: M? Raw_context.t :=
let '{| Level_repr.t.level := level |} := Raw_context.current_level ctxt in
let inbox_value := Sc_rollup_inbox_repr.empty level in
let? ctxt :=
Store.Inbox.(Storage_sigs.Single_data_storage.init_value) ctxt inbox_value
in
let? '(_inbox, _diff, ctxt) := add_start_of_level ctxt in
let? '(_inbox, _diff, ctxt) := add_info_per_level ctxt timestamp predecessor
in
let? '(_inbox, _diff, ctxt) := add_end_of_level ctxt in
return? ctxt.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_costs.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_merkelized_payload_hashes_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Module Store := Storage.Sc_rollup.
Definition update_num_and_size_of_messages
(num_messages : int) (total_messages_size : int)
(message : Sc_rollup_inbox_message_repr.serialized) : int × int :=
((num_messages +i 1), (total_messages_size +i (String.length message))).
Definition get_inbox (ctxt : Raw_context.t)
: M? (Sc_rollup_inbox_repr.V1.t × Raw_context.t) :=
let? inbox_value := Store.Inbox.(Storage_sigs.Single_data_storage.get) ctxt in
return? (inbox_value, ctxt).
Definition _assert_inbox_nb_messages_in_commitment_period
(ctxt : Raw_context.t) (inbox_value : Sc_rollup_inbox_repr.t)
(extra_messages : int) : M? unit :=
let nb_messages_in_commitment_period :=
(Sc_rollup_inbox_repr.number_of_messages_during_commitment_period
inbox_value) +i64 (Int64.of_int extra_messages) in
let limit :=
Int64.of_int
(Constants_storage.sc_rollup_max_number_of_messages_per_commitment_period
ctxt) in
Error_monad.fail_when (nb_messages_in_commitment_period >i64 limit)
(Build_extensible
"Sc_rollup_max_number_of_messages_reached_for_commitment_period" unit tt).
Definition add_messages_aux
(ctxt : Raw_context.t)
(messages : list Sc_rollup_inbox_message_repr.serialized)
: M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
let '{| Level_repr.t.level := level |} := Raw_context.current_level ctxt in
let? '(inbox_value, ctxt) := get_inbox ctxt in
let? '(num_messages, total_messages_size, ctxt) :=
List.fold_left_es
(fun (function_parameter : int × int × Raw_context.t) ⇒
let '(num_messages, total_messages_size, ctxt) := function_parameter in
fun (message : Sc_rollup_inbox_message_repr.serialized) ⇒
let? ctxt :=
Raw_context.consume_gas ctxt
Sc_rollup_costs.Constants.cost_update_num_and_size_of_messages in
let '(num_messages, total_messages_size) :=
update_num_and_size_of_messages num_messages total_messages_size
message in
return? (num_messages, total_messages_size, ctxt)) (0, 0, ctxt)
messages in
let cost_add_serialized_messages :=
Sc_rollup_costs.cost_add_serialized_messages num_messages
total_messages_size 0 in
let? ctxt := Raw_context.consume_gas ctxt cost_add_serialized_messages in
let current_messages :=
Raw_context.Sc_rollup_in_memory_inbox.current_messages ctxt in
let? '(current_messages, inbox_value) :=
Sc_rollup_inbox_repr.add_messages_no_history inbox_value level messages
current_messages in
let ctxt :=
Raw_context.Sc_rollup_in_memory_inbox.set_current_messages ctxt
current_messages in
let? ctxt :=
Store.Inbox.(Storage_sigs.Single_data_storage.update) ctxt inbox_value in
return? (inbox_value, Z.zero, ctxt).
Definition serialize_external_messages
(ctxt : Raw_context.t) (external_messages : list string)
: M? (Raw_context.t × list Sc_rollup_inbox_message_repr.serialized) :=
List.fold_left_map_e
(fun (ctxt : Raw_context.t) ⇒
fun (message : string) ⇒
let? ctxt :=
let bytes_len := String.length message in
Raw_context.consume_gas ctxt
(Sc_rollup_costs.cost_serialize_external_inbox_message bytes_len) in
let? serialized_message :=
Sc_rollup_inbox_message_repr.serialize
(Sc_rollup_inbox_message_repr.External message) in
return? (ctxt, serialized_message)) ctxt external_messages.
Definition serialize_internal_message
(ctxt : Raw_context.t)
(internal_message : Sc_rollup_inbox_message_repr.internal_inbox_message)
: M? (Sc_rollup_inbox_message_repr.serialized × Raw_context.t) :=
let? ctxt :=
Raw_context.consume_gas ctxt
(Sc_rollup_costs.cost_serialize_internal_inbox_message internal_message)
in
let? message :=
Sc_rollup_inbox_message_repr.serialize
(Sc_rollup_inbox_message_repr.Internal internal_message) in
return? (message, ctxt).
Definition add_external_messages
(ctxt : Raw_context.t) (external_messages : list string)
: M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
let? '(ctxt, messages) := serialize_external_messages ctxt external_messages
in
add_messages_aux ctxt messages.
Definition add_internal_message
(ctxt : Raw_context.t)
(internal_message : Sc_rollup_inbox_message_repr.internal_inbox_message)
: M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
let? '(message, ctxt) := serialize_internal_message ctxt internal_message in
add_messages_aux ctxt [ message ].
Definition add_deposit
(ctxt : Raw_context.t) (payload : Script_repr.expr) (sender : Contract_hash.t)
(source : Signature.public_key_hash) (destination : Sc_rollup_repr.Address.t)
: M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
let internal_message :=
Sc_rollup_inbox_message_repr.Transfer
{|
Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.payload :=
payload;
Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.sender :=
sender;
Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.source :=
source;
Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.destination
:= destination; |} in
add_internal_message ctxt internal_message.
Definition add_start_of_level (ctxt : Raw_context.t)
: M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
add_internal_message ctxt Sc_rollup_inbox_message_repr.Start_of_level.
Definition add_end_of_level (ctxt : Raw_context.t)
: M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
add_internal_message ctxt Sc_rollup_inbox_message_repr.End_of_level.
Definition add_info_per_level
(ctxt : Raw_context.t) (timestamp : Time.t) (predecessor : Block_hash.t)
: M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
add_internal_message ctxt
(Sc_rollup_inbox_message_repr.Info_per_level
{|
Sc_rollup_inbox_message_repr.internal_inbox_message.Info_per_level.timestamp
:= timestamp;
Sc_rollup_inbox_message_repr.internal_inbox_message.Info_per_level.predecessor
:= predecessor; |}).
Definition init_value
(timestamp : Time.t) (predecessor : Block_hash.t) (ctxt : Raw_context.t)
: M? Raw_context.t :=
let '{| Level_repr.t.level := level |} := Raw_context.current_level ctxt in
let inbox_value := Sc_rollup_inbox_repr.empty level in
let? ctxt :=
Store.Inbox.(Storage_sigs.Single_data_storage.init_value) ctxt inbox_value
in
let? '(_inbox, _diff, ctxt) := add_start_of_level ctxt in
let? '(_inbox, _diff, ctxt) := add_info_per_level ctxt timestamp predecessor
in
let? '(_inbox, _diff, ctxt) := add_end_of_level ctxt in
return? ctxt.