🍬 Michelson_v1_gas_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.Michelson_v1_gas_costs_generated.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Include Michelson_v1_gas_costs_generated.
Definition cost_N_IMul_nattez : S.t := S.safe_int 50.
Definition cost_N_IMul_teznat : S.t := S.safe_int 50.
Definition cost_N_IEdiv_teznat : S.t := S.safe_int 70.
Definition cost_N_ISapling_verify_update
(size1 : int) (size2 : int) (bound_data : int) : Saturation_repr.t :=
let v1 := S.safe_int size1 in
let v2 := S.safe_int size2 in
S.Syntax.op_plus
(S.Syntax.op_plus
(S.Syntax.op_plus (cost_N_IBlake2b bound_data) (S.safe_int 310000))
(S.Syntax.op_star (S.safe_int 5575000) v1))
(S.Syntax.op_star (S.safe_int 5075000) v2).
Definition cost_N_IApply (rec_flag : bool) : S.t :=
if rec_flag then
S.safe_int 220
else
S.safe_int 140.
Definition cost_N_KIter : S.t := S.safe_int 10.
Definition cost_N_KMap_enter_body : S.t := S.safe_int 80.
Definition cost_N_KList_enter_body {A : Set} (xs : list A) (size_ys : int)
: S.t :=
match xs with
| [] ⇒
let v0 := S.safe_int size_ys in
S.Syntax.op_plus (S.safe_int 25)
(S.Syntax.op_plus (S.Syntax.op_plus v0 (S.Syntax.lsr v0 1))
(S.Syntax.lsr v0 3))
| cons _ _ ⇒ S.safe_int 25
end.
Definition cost_TY_EQ : S.t := S.safe_int 60.
Definition cost_PARSE_TYPE : S.t := S.safe_int 60.
Definition cost_UNPARSE_TYPE (type_size : S.t) : S.t :=
S.mul (S.safe_int 20) type_size.
Definition cost_TYPECHECKING_CODE : S.t := S.safe_int 220.
Definition cost_UNPARSING_CODE : S.t := S.safe_int 115.
Definition cost_TYPECHECKING_DATA : S.t := S.safe_int 100.
Definition cost_UNPARSING_DATA : S.t := S.safe_int 65.
Definition cost_FIND_ENTRYPOINT : Saturation_repr.t := cost_N_ICompare 31 31.
Definition cost_SAPLING_TRANSACTION_ENCODING
(inputs : int) (outputs : int) (bound_data : int) : S.t :=
S.safe_int
(((1500 +i (inputs ×i 160)) +i (outputs ×i 320)) +i
(Pervasives.lsr bound_data 3)).
Definition cost_SAPLING_DIFF_ENCODING (nfs : int) (cms : int) : S.t :=
S.safe_int ((nfs ×i 22) +i (cms ×i 215)).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_gas_costs_generated.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Include Michelson_v1_gas_costs_generated.
Definition cost_N_IMul_nattez : S.t := S.safe_int 50.
Definition cost_N_IMul_teznat : S.t := S.safe_int 50.
Definition cost_N_IEdiv_teznat : S.t := S.safe_int 70.
Definition cost_N_ISapling_verify_update
(size1 : int) (size2 : int) (bound_data : int) : Saturation_repr.t :=
let v1 := S.safe_int size1 in
let v2 := S.safe_int size2 in
S.Syntax.op_plus
(S.Syntax.op_plus
(S.Syntax.op_plus (cost_N_IBlake2b bound_data) (S.safe_int 310000))
(S.Syntax.op_star (S.safe_int 5575000) v1))
(S.Syntax.op_star (S.safe_int 5075000) v2).
Definition cost_N_IApply (rec_flag : bool) : S.t :=
if rec_flag then
S.safe_int 220
else
S.safe_int 140.
Definition cost_N_KIter : S.t := S.safe_int 10.
Definition cost_N_KMap_enter_body : S.t := S.safe_int 80.
Definition cost_N_KList_enter_body {A : Set} (xs : list A) (size_ys : int)
: S.t :=
match xs with
| [] ⇒
let v0 := S.safe_int size_ys in
S.Syntax.op_plus (S.safe_int 25)
(S.Syntax.op_plus (S.Syntax.op_plus v0 (S.Syntax.lsr v0 1))
(S.Syntax.lsr v0 3))
| cons _ _ ⇒ S.safe_int 25
end.
Definition cost_TY_EQ : S.t := S.safe_int 60.
Definition cost_PARSE_TYPE : S.t := S.safe_int 60.
Definition cost_UNPARSE_TYPE (type_size : S.t) : S.t :=
S.mul (S.safe_int 20) type_size.
Definition cost_TYPECHECKING_CODE : S.t := S.safe_int 220.
Definition cost_UNPARSING_CODE : S.t := S.safe_int 115.
Definition cost_TYPECHECKING_DATA : S.t := S.safe_int 100.
Definition cost_UNPARSING_DATA : S.t := S.safe_int 65.
Definition cost_FIND_ENTRYPOINT : Saturation_repr.t := cost_N_ICompare 31 31.
Definition cost_SAPLING_TRANSACTION_ENCODING
(inputs : int) (outputs : int) (bound_data : int) : S.t :=
S.safe_int
(((1500 +i (inputs ×i 160)) +i (outputs ×i 320)) +i
(Pervasives.lsr bound_data 3)).
Definition cost_SAPLING_DIFF_ENCODING (nfs : int) (cms : int) : S.t :=
S.safe_int ((nfs ×i 22) +i (cms ×i 215)).