Skip to main content

🐆 Tx_rollup_gas.v

Translated OCaml

See proofs, See simulations, Gitlab , OCaml

File generated by coq-of-ocaml
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).

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.

As generated by the model [inbox_add_message_codegen] in [lib_benchmarks_proto/tx_rollup_benchmarks.ml].
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.

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).