Skip to main content

🦏 Sc_rollup_costs.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.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_levelSaturation_repr.zero
  | Sc_rollup_inbox_message_repr.End_of_levelSaturation_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.