🌍 Global_constants_costs.v

Translated OCaml

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

Module S := Saturation_repr.

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 lsr : S.t → int → S.t := S.shift_right.

Definition expr_to_address_in_context_cost (bytes_value : bytes)
  : Gas_limit_repr.cost :=
  let v0 := S.safe_int (Bytes.length bytes_value) in
  Gas_limit_repr.atomic_step_cost
    (op_plus (S.safe_int 200) (op_plus v0 (lsr v0 2))).

Definition expand_constants_branch_cost : Gas_limit_repr.cost :=
  Gas_limit_repr.atomic_step_cost (S.safe_int 4095).

Definition expand_no_constants_branch_cost (node_value : Script_repr.node)
  : Gas_limit_repr.cost :=
  let v0 := S.safe_int (Script_repr.micheline_nodes node_value) in
  let v0 := S.mul v0 (log2 v0) in
  Gas_limit_repr.atomic_step_cost
    (op_plus
      (op_plus (op_plus (S.safe_int 100) (S.mul (S.safe_int 4) v0)) (lsr v0 1))
      (lsr v0 3)).