🦏 Sc_rollup_costs.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.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.State_hash.
Module S := Saturation_repr.
Module S_syntax.
Definition log2 (x_value : S.t) : S.t :=
S.safe_int (1 +i (S.numbits x_value)).
Definition op_plus : S.t → S.t → S.t := S.add.
Definition op_star : S.t → S.t → S.t := S.mul.
Definition lsr : S.t → int → S.t := S.shift_right.
End S_syntax.
Module Constants.
Definition cost_add_message_base : S.t := S.safe_int 430.
Definition cost_add_message_per_byte : S.t := S.safe_int 15.
Definition cost_add_inbox_per_level : S.t := S.safe_int 15.
Definition cost_update_num_and_size_of_messages : S.t := S.safe_int 15.
Definition cost_decoding_contract_optimized : S.t := S.safe_int 70.
Definition cost_decoding_key_hash_optimized : S.t := S.safe_int 50.
Definition cost_encode_string_per_byte : S.t := S.safe_int 2.
Definition cost_serialize_state_hash : S.t :=
let len := S.safe_int State_hash.size_value in
S_syntax.op_star cost_encode_string_per_byte len.
Definition cost_serialize_commitment_hash : S.t :=
let len := S.safe_int Sc_rollup_commitment_repr.Hash.size_value in
S_syntax.op_star cost_encode_string_per_byte len.
Definition cost_serialize_commitment : S.t :=
S_syntax.op_plus cost_serialize_state_hash cost_serialize_commitment_hash.
Definition cost_serialize_operation_hash : S.t :=
let len := S.safe_int Operation_hash.size_value in
S_syntax.op_star cost_encode_string_per_byte len.
Definition cost_serialize_nonce : S.t := cost_serialize_operation_hash.
End Constants.
Definition cost_add_serialized_messages
(num_messages : int) (total_messages_size : int) (l_value : Int32.t) : S.t :=
let log_level :=
if Int32.equal l_value Int32.zero then
Saturation_repr.safe_int 0
else
S_syntax.log2 (S.safe_int (Int32.to_int l_value)) in
let level_cost :=
S_syntax.op_star log_level Constants.cost_add_inbox_per_level in
S_syntax.op_plus
(S_syntax.op_plus
(S_syntax.op_star (S.safe_int num_messages)
Constants.cost_add_message_base) level_cost)
(S_syntax.op_star Constants.cost_add_message_per_byte
(S.safe_int total_messages_size)).
Definition is_valid_parameters_ty_cost (ty_size : S.t) : S.t :=
let fixed_cost := S.safe_int 10 in
let coeff := S.safe_int 6 in
S.add fixed_cost (S.mul coeff ty_size).
Definition cost_serialize_internal_inbox_message
(internal_inbox_message : Sc_rollup_inbox_message_repr.internal_inbox_message)
: S.t :=
match internal_inbox_message with
|
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 := _;
Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.source := _;
Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.destination
:= _
|} ⇒
let lexpr := Script_repr.lazy_expr_value payload in
let expr_cost := Script_repr.force_bytes_cost lexpr in
S_syntax.op_plus
(S_syntax.op_plus expr_cost Constants.cost_decoding_contract_optimized)
Constants.cost_decoding_key_hash_optimized
| Sc_rollup_inbox_message_repr.Start_of_level ⇒ Saturation_repr.zero
| Sc_rollup_inbox_message_repr.End_of_level ⇒ Saturation_repr.zero
| Sc_rollup_inbox_message_repr.Info_per_level _ ⇒ Saturation_repr.zero
end.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.State_hash.
Module S := Saturation_repr.
Module S_syntax.
Definition log2 (x_value : S.t) : S.t :=
S.safe_int (1 +i (S.numbits x_value)).
Definition op_plus : S.t → S.t → S.t := S.add.
Definition op_star : S.t → S.t → S.t := S.mul.
Definition lsr : S.t → int → S.t := S.shift_right.
End S_syntax.
Module Constants.
Definition cost_add_message_base : S.t := S.safe_int 430.
Definition cost_add_message_per_byte : S.t := S.safe_int 15.
Definition cost_add_inbox_per_level : S.t := S.safe_int 15.
Definition cost_update_num_and_size_of_messages : S.t := S.safe_int 15.
Definition cost_decoding_contract_optimized : S.t := S.safe_int 70.
Definition cost_decoding_key_hash_optimized : S.t := S.safe_int 50.
Definition cost_encode_string_per_byte : S.t := S.safe_int 2.
Definition cost_serialize_state_hash : S.t :=
let len := S.safe_int State_hash.size_value in
S_syntax.op_star cost_encode_string_per_byte len.
Definition cost_serialize_commitment_hash : S.t :=
let len := S.safe_int Sc_rollup_commitment_repr.Hash.size_value in
S_syntax.op_star cost_encode_string_per_byte len.
Definition cost_serialize_commitment : S.t :=
S_syntax.op_plus cost_serialize_state_hash cost_serialize_commitment_hash.
Definition cost_serialize_operation_hash : S.t :=
let len := S.safe_int Operation_hash.size_value in
S_syntax.op_star cost_encode_string_per_byte len.
Definition cost_serialize_nonce : S.t := cost_serialize_operation_hash.
End Constants.
Definition cost_add_serialized_messages
(num_messages : int) (total_messages_size : int) (l_value : Int32.t) : S.t :=
let log_level :=
if Int32.equal l_value Int32.zero then
Saturation_repr.safe_int 0
else
S_syntax.log2 (S.safe_int (Int32.to_int l_value)) in
let level_cost :=
S_syntax.op_star log_level Constants.cost_add_inbox_per_level in
S_syntax.op_plus
(S_syntax.op_plus
(S_syntax.op_star (S.safe_int num_messages)
Constants.cost_add_message_base) level_cost)
(S_syntax.op_star Constants.cost_add_message_per_byte
(S.safe_int total_messages_size)).
Definition is_valid_parameters_ty_cost (ty_size : S.t) : S.t :=
let fixed_cost := S.safe_int 10 in
let coeff := S.safe_int 6 in
S.add fixed_cost (S.mul coeff ty_size).
Definition cost_serialize_internal_inbox_message
(internal_inbox_message : Sc_rollup_inbox_message_repr.internal_inbox_message)
: S.t :=
match internal_inbox_message with
|
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 := _;
Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.source := _;
Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.destination
:= _
|} ⇒
let lexpr := Script_repr.lazy_expr_value payload in
let expr_cost := Script_repr.force_bytes_cost lexpr in
S_syntax.op_plus
(S_syntax.op_plus expr_cost Constants.cost_decoding_contract_optimized)
Constants.cost_decoding_key_hash_optimized
| Sc_rollup_inbox_message_repr.Start_of_level ⇒ Saturation_repr.zero
| Sc_rollup_inbox_message_repr.End_of_level ⇒ Saturation_repr.zero
| Sc_rollup_inbox_message_repr.Info_per_level _ ⇒ Saturation_repr.zero
end.
TODO: #3212
Confirm gas cost model.
We here assume that the cost of deserializing an expression of [bytes_len]
is proportional to deserializing a script expression of size [bytes_len].
This may not be the case and in particular, the cost depends on the specific
structure used for the PVM. We may thus need to split the cost function.
Definition cost_deserialize_output_proof (bytes_len : int)
: Gas_limit_repr.cost :=
Script_repr.deserialization_cost_estimated_from_bytes bytes_len.
Definition cost_serialize_external_inbox_message (bytes_len : int) : S.t :=
let len := S.safe_int bytes_len in
S_syntax.op_star Constants.cost_encode_string_per_byte len.
Definition cost_hash_bytes (bytes_len : int) : S.t :=
let v0 := S.safe_int bytes_len in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 430) v0) (S_syntax.lsr v0 3).
: Gas_limit_repr.cost :=
Script_repr.deserialization_cost_estimated_from_bytes bytes_len.
Definition cost_serialize_external_inbox_message (bytes_len : int) : S.t :=
let len := S.safe_int bytes_len in
S_syntax.op_star Constants.cost_encode_string_per_byte len.
Definition cost_hash_bytes (bytes_len : int) : S.t :=
let v0 := S.safe_int bytes_len in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 430) v0) (S_syntax.lsr v0 3).