💾 Storage_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.
Definition read_access (path_length : int) (read_bytes : int)
: Gas_limit_repr.cost :=
let base_cost := Saturation_repr.safe_int (200000 +i (5000 ×i path_length)) in
Gas_limit_repr.atomic_step_cost
(Saturation_repr.add base_cost
(Saturation_repr.mul (Saturation_repr.safe_int 2)
(Saturation_repr.safe_int read_bytes))).
Definition write_access (written_bytes : int) : Gas_limit_repr.cost :=
Gas_limit_repr.atomic_step_cost
(Saturation_repr.add (Saturation_repr.safe_int 200000)
(Saturation_repr.mul (Saturation_repr.safe_int 4)
(Saturation_repr.safe_int written_bytes))).
Definition list_key_values_step_cost : Saturation_repr.t :=
Saturation_repr.safe_int 117.
Definition list_key_values_intercept : Saturation_repr.t :=
Saturation_repr.safe_int 470.
Definition list_key_values_traverse (size_value : int) : Saturation_repr.t :=
Saturation_repr.add list_key_values_intercept
(Saturation_repr.mul (Saturation_repr.safe_int size_value)
list_key_values_step_cost).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Definition read_access (path_length : int) (read_bytes : int)
: Gas_limit_repr.cost :=
let base_cost := Saturation_repr.safe_int (200000 +i (5000 ×i path_length)) in
Gas_limit_repr.atomic_step_cost
(Saturation_repr.add base_cost
(Saturation_repr.mul (Saturation_repr.safe_int 2)
(Saturation_repr.safe_int read_bytes))).
Definition write_access (written_bytes : int) : Gas_limit_repr.cost :=
Gas_limit_repr.atomic_step_cost
(Saturation_repr.add (Saturation_repr.safe_int 200000)
(Saturation_repr.mul (Saturation_repr.safe_int 4)
(Saturation_repr.safe_int written_bytes))).
Definition list_key_values_step_cost : Saturation_repr.t :=
Saturation_repr.safe_int 117.
Definition list_key_values_intercept : Saturation_repr.t :=
Saturation_repr.safe_int 470.
Definition list_key_values_traverse (size_value : int) : Saturation_repr.t :=
Saturation_repr.add list_key_values_intercept
(Saturation_repr.mul (Saturation_repr.safe_int size_value)
list_key_values_step_cost).