🍬 Script_typed_ir_size_costs.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

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

Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.

Module S := Saturation_repr.

FIXME insert proper gas constants (the gas constant below was fitted on a non-standard machine)

Definition nodes_cost (nodes : int) : Gas_limit_repr.cost :=
  let nodes :=
    Cache_memory_helpers.Nodes.(Cache_memory_helpers.SNodes.to_int) nodes in
  let coeff := S.safe_int 45 in
  Gas_limit_repr.atomic_step_cost (S.mul coeff (S.safe_int nodes)).