🍬 Script_typed_ir_size_costs.v
Translated 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.
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)).
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)).