💾 Storage_costs.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
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))).