🐆 Tx_rollup_gas.v
Translated OCaml
See proofs, See simulations, 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.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Merkle_list.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_prefixes.
Module S := Saturation_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Merkle_list.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_prefixes.
Module S := Saturation_repr.
The model in {!Michelson_v1_gas.N_IBlake2b}, plus the allocation
of bytes from {!Storage_functor}.
Definition hash_cost (input_size : int) : M? S.t :=
let? '_ :=
Error_monad.error_unless (0 ≤i input_size)
(Build_extensible "Tx_rollup_negative_input_size" unit tt) in
let op_plus := S.add in
let cost_serialization := Gas_limit_repr.alloc_mbytes_cost input_size in
let v0 := Saturation_repr.safe_int input_size in
let cost_N_IBlake2b :=
op_plus (op_plus (S.safe_int 430) v0) (S.shift_right v0 3) in
let cost_blake2b := Gas_limit_repr.atomic_step_cost cost_N_IBlake2b in
return? (op_plus cost_serialization cost_blake2b).
let? '_ :=
Error_monad.error_unless (0 ≤i input_size)
(Build_extensible "Tx_rollup_negative_input_size" unit tt) in
let op_plus := S.add in
let cost_serialization := Gas_limit_repr.alloc_mbytes_cost input_size in
let v0 := Saturation_repr.safe_int input_size in
let cost_N_IBlake2b :=
op_plus (op_plus (S.safe_int 430) v0) (S.shift_right v0 3) in
let cost_blake2b := Gas_limit_repr.atomic_step_cost cost_N_IBlake2b in
return? (op_plus cost_serialization cost_blake2b).
Model from {!Ticket_costs.Constants.cost_compare_ticket_hash} since they are
Blake2B hashes too.
Definition compare_blake2b_hash : S.t := S.safe_int 10.
#[bypass_check(guard)]
Definition check_path_cost (element_size : int) (path_depth : int) : M? S.t :=
let op_plus := S.add in
let? '_ :=
Error_monad.error_unless (0 ≤i path_depth)
(Build_extensible "Tx_rollup_negative_input_size" unit tt) in
let? element_hash_cost := hash_cost element_size in
let? hash_cost := hash_cost 64 in
let fix acc_hash_cost (acc_value : S.t) (i_value : int) {struct i_value}
: S.t :=
if i_value ≤i 0 then
acc_value
else
acc_hash_cost (op_plus hash_cost acc_value) (i_value -i 1) in
return?
(op_plus element_hash_cost (acc_hash_cost compare_blake2b_hash path_depth)).
Definition consume_check_path_inbox_cost (ctxt : Raw_context.t)
: M? Raw_context.t :=
let count_limit := Constants_storage.tx_rollup_max_messages_per_inbox ctxt in
let max_depth := Merkle_list.max_depth count_limit in
let? cost :=
check_path_cost
Tx_rollup_prefixes.message_hash.(Tx_rollup_prefixes.t.hash_size) max_depth
in
Raw_context.consume_gas ctxt cost.
Definition consume_check_path_commitment_cost (ctxt : Raw_context.t)
: M? Raw_context.t :=
let count_limit := Constants_storage.tx_rollup_max_messages_per_inbox ctxt in
let max_depth := Merkle_list.max_depth count_limit in
let? cost :=
check_path_cost
Tx_rollup_prefixes.message_result_hash.(Tx_rollup_prefixes.t.hash_size)
max_depth in
Raw_context.consume_gas ctxt cost.
#[bypass_check(guard)]
Definition check_path_cost (element_size : int) (path_depth : int) : M? S.t :=
let op_plus := S.add in
let? '_ :=
Error_monad.error_unless (0 ≤i path_depth)
(Build_extensible "Tx_rollup_negative_input_size" unit tt) in
let? element_hash_cost := hash_cost element_size in
let? hash_cost := hash_cost 64 in
let fix acc_hash_cost (acc_value : S.t) (i_value : int) {struct i_value}
: S.t :=
if i_value ≤i 0 then
acc_value
else
acc_hash_cost (op_plus hash_cost acc_value) (i_value -i 1) in
return?
(op_plus element_hash_cost (acc_hash_cost compare_blake2b_hash path_depth)).
Definition consume_check_path_inbox_cost (ctxt : Raw_context.t)
: M? Raw_context.t :=
let count_limit := Constants_storage.tx_rollup_max_messages_per_inbox ctxt in
let max_depth := Merkle_list.max_depth count_limit in
let? cost :=
check_path_cost
Tx_rollup_prefixes.message_hash.(Tx_rollup_prefixes.t.hash_size) max_depth
in
Raw_context.consume_gas ctxt cost.
Definition consume_check_path_commitment_cost (ctxt : Raw_context.t)
: M? Raw_context.t :=
let count_limit := Constants_storage.tx_rollup_max_messages_per_inbox ctxt in
let max_depth := Merkle_list.max_depth count_limit in
let? cost :=
check_path_cost
Tx_rollup_prefixes.message_result_hash.(Tx_rollup_prefixes.t.hash_size)
max_depth in
Raw_context.consume_gas ctxt cost.
As generated by the model [inbox_add_message_codegen] in
[lib_benchmarks_proto/tx_rollup_benchmarks.ml].
Definition model_inbox_add_message_codegen (inbox_length : int) : S.t :=
let log2 (n_value : S.t) : S.t :=
S.safe_int (1 +i (S.numbits n_value)) in
S.mul (S.safe_int 445) (log2 (S.safe_int inbox_length)).
Definition consume_add_message_cost (ctxt : Raw_context.t) : M? Raw_context.t :=
let max_messages_per_inbox :=
Constants_storage.tx_rollup_max_messages_per_inbox ctxt in
let cost := model_inbox_add_message_codegen max_messages_per_inbox in
Raw_context.consume_gas ctxt cost.
let log2 (n_value : S.t) : S.t :=
S.safe_int (1 +i (S.numbits n_value)) in
S.mul (S.safe_int 445) (log2 (S.safe_int inbox_length)).
Definition consume_add_message_cost (ctxt : Raw_context.t) : M? Raw_context.t :=
let max_messages_per_inbox :=
Constants_storage.tx_rollup_max_messages_per_inbox ctxt in
let cost := model_inbox_add_message_codegen max_messages_per_inbox in
Raw_context.consume_gas ctxt cost.
As generated by the model [model_commitment_full_compact] in
[lib_benchmarks_proto/tx_rollup_benchmarks.ml]. We add one to
[inbox_length] so that the cost is never zero.
Definition model_commitment_full_compact (inbox_length : int) : S.t :=
S.mul (S.safe_int 915) (S.safe_int (1 +i inbox_length)).
Definition consume_compact_commitment_cost
(ctxt : Raw_context.t) (inbox_length : int) : M? Raw_context.t :=
let cost := model_commitment_full_compact inbox_length in
Raw_context.consume_gas ctxt cost.
Definition hash_value {A B : Set}
(hash_f : list bytes → A) (ctxt : Raw_context.t)
(encoding : Data_encoding.encoding B) (input : B) : M? (Raw_context.t × A) :=
match Data_encoding.Binary.to_bytes_opt None encoding input with
| Some buffer ⇒
let len := Bytes.length buffer in
let? cost := hash_cost len in
let? ctxt := Raw_context.consume_gas ctxt cost in
return? (ctxt, (hash_f [ buffer ]))
| None ⇒
Error_monad.error_value
(Build_extensible "Internal_error" string
"Cannot serialize input to hash function")
end.
S.mul (S.safe_int 915) (S.safe_int (1 +i inbox_length)).
Definition consume_compact_commitment_cost
(ctxt : Raw_context.t) (inbox_length : int) : M? Raw_context.t :=
let cost := model_commitment_full_compact inbox_length in
Raw_context.consume_gas ctxt cost.
Definition hash_value {A B : Set}
(hash_f : list bytes → A) (ctxt : Raw_context.t)
(encoding : Data_encoding.encoding B) (input : B) : M? (Raw_context.t × A) :=
match Data_encoding.Binary.to_bytes_opt None encoding input with
| Some buffer ⇒
let len := Bytes.length buffer in
let? cost := hash_cost len in
let? ctxt := Raw_context.consume_gas ctxt cost in
return? (ctxt, (hash_f [ buffer ]))
| None ⇒
Error_monad.error_value
(Build_extensible "Internal_error" string
"Cannot serialize input to hash function")
end.
Init function; without side-effects in Coq
Definition init_module : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"tx_rollup_negative_input_size"
"The protocol has computed a negative size for the input of a hash function"
"The protocol has computed a negative size for the input of a hash function. This is an internal error, and denotes a bug in the protocol implementation."
None Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Tx_rollup_negative_input_size" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Tx_rollup_negative_input_size" unit tt).
Error_monad.register_error_kind Error_monad.Permanent
"tx_rollup_negative_input_size"
"The protocol has computed a negative size for the input of a hash function"
"The protocol has computed a negative size for the input of a hash function. This is an internal error, and denotes a bug in the protocol implementation."
None Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Tx_rollup_negative_input_size" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Tx_rollup_negative_input_size" unit tt).