🍬 Michelson_v1_gas.v
Translated 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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Gas_input_size.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_map.
Require TezosOfOCaml.Proto_alpha.Script_set.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Storage_costs.
Module S := Saturation_repr.
Module Size := Gas_input_size.
Module Cost_of.
Module S_syntax.
Definition log2 (x_value : S.t) : S.t :=
S.safe_int (1 +i (S.numbits x_value)).
Definition op_plus : S.t → S.t → S.t := S.add.
Definition op_star : S.t → S.t → S.t := S.mul.
Definition lsr : S.t → int → S.t := S.shift_right.
End S_syntax.
Definition z_bytes (z_value : Z.t) : int :=
let bits := Z.numbits z_value in
(7 +i bits) /i 8.
Definition int_bytes (z_value : Alpha_context.Script_int.num) : int :=
z_bytes (Alpha_context.Script_int.to_zint z_value).
Definition manager_operation : Alpha_context.Gas.cost :=
Alpha_context.Gas.step_cost (S.safe_int 1000).
Module Generated_costs.
Definition cost_N_IAbs_int (size_value : int) : S.t :=
S.safe_int (20 +i (Pervasives.lsr size_value 4)).
Definition cost_N_IAdd_bls12_381_fr : S.t := S.safe_int 30.
Definition cost_N_IAdd_bls12_381_g1 : S.t := S.safe_int 900.
Definition cost_N_IAdd_bls12_381_g2 : S.t := S.safe_int 2470.
Definition cost_linear_op_int (size1 : int) (size2 : int) : S.t :=
let v0 := S.safe_int (Compare.Int.max size1 size2) in
S_syntax.op_plus (S.safe_int 35)
(S_syntax.op_plus (S_syntax.lsr v0 4) (S_syntax.lsr v0 7)).
Definition cost_N_IAdd_int : int → int → S.t := cost_linear_op_int.
Definition cost_N_IAdd_nat : int → int → S.t := cost_linear_op_int.
Definition cost_N_IAdd_seconds_to_timestamp : int → int → S.t :=
cost_linear_op_int.
Definition cost_N_IAdd_tez : S.t := S.safe_int 20.
Definition cost_N_IAdd_timestamp_to_seconds : int → int → S.t :=
cost_linear_op_int.
Definition cost_N_IAddress : S.t := S.safe_int 10.
Definition cost_N_IAmount : S.t := S.safe_int 10.
Definition cost_N_IAnd : S.t := S.safe_int 10.
Definition cost_N_IAnd_int_nat (size1 : int) (size2 : int) : S.t :=
let v0 := S.safe_int (Compare.Int.min size1 size2) in
S_syntax.op_plus (S.safe_int 35)
(S_syntax.op_plus (S_syntax.lsr v0 3) (S_syntax.lsr v0 6)).
Definition cost_N_IAnd_nat (size1 : int) (size2 : int) : S.t :=
let v0 := S.safe_int (Compare.Int.min size1 size2) in
S_syntax.op_plus (S.safe_int 35)
(S_syntax.op_plus (S_syntax.lsr v0 4) (S_syntax.lsr v0 7)).
Definition cost_N_IApply : S.t := S.safe_int 140.
Definition cost_N_IBlake2b (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 430) v0)
(S_syntax.lsr v0 3).
Definition cost_N_IBytes_size : S.t := S.safe_int 10.
Definition cost_N_ICar : S.t := S.safe_int 10.
Definition cost_N_ICdr : S.t := S.safe_int 10.
Definition cost_N_IChainId : S.t := S.safe_int 15.
Definition cost_N_ICheck_signature_ed25519 (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 65800)
(S_syntax.op_plus v0 (S_syntax.lsr v0 3)).
Definition cost_N_ICheck_signature_p256 (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 990000)
(S_syntax.op_plus v0 (S_syntax.lsr v0 3)).
Definition cost_N_ICheck_signature_secp256k1 (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 51600)
(S_syntax.op_plus v0 (S_syntax.lsr v0 3)).
Definition cost_N_IComb (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus
(S_syntax.op_plus (S_syntax.op_star (S.safe_int 3) v0)
(S_syntax.lsr v0 1)) (S_syntax.lsr v0 5).
Definition cost_N_IComb_get (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 20) (S_syntax.lsr v0 1))
(S_syntax.lsr v0 4).
Definition cost_N_IComb_set (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 20)
(S_syntax.op_plus (S_syntax.op_plus v0 (S_syntax.lsr v0 2))
(S_syntax.lsr v0 5)).
Definition cost_N_ICompare (size1 : int) (size2 : int) : S.t :=
let v0 := S.safe_int (Compare.Int.min size1 size2) in
S_syntax.op_plus (S.safe_int 35)
(S_syntax.op_plus (S_syntax.lsr v0 6) (S_syntax.lsr v0 7)).
Definition cost_N_IConcat_bytes_pair (size1 : int) (size2 : int) : S.t :=
let v0 := S_syntax.op_plus (S.safe_int size1) (S.safe_int size2) in
S_syntax.op_plus (S.safe_int 45) (S_syntax.lsr v0 4).
Definition cost_N_IConcat_string_pair (size1 : int) (size2 : int) : S.t :=
let v0 := S_syntax.op_plus (S.safe_int size1) (S.safe_int size2) in
S_syntax.op_plus (S.safe_int 45) (S_syntax.lsr v0 4).
Definition cost_N_ICons_list : S.t := S.safe_int 10.
Definition cost_N_ICons_none : S.t := S.safe_int 10.
Definition cost_N_ICons_pair : S.t := S.safe_int 10.
Definition cost_N_ICons_some : S.t := S.safe_int 10.
Definition cost_N_IConst : S.t := S.safe_int 10.
Definition cost_N_IContract : S.t := S.safe_int 30.
Definition cost_N_ICreate_contract : S.t := S.safe_int 30.
Definition cost_N_IDiff_timestamps : int → int → S.t :=
cost_linear_op_int.
Definition cost_N_IDig (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 30)
(S_syntax.op_plus
(S_syntax.op_plus (S_syntax.op_star (S.safe_int 6) v0)
(S_syntax.lsr v0 1)) (S_syntax.lsr v0 2)).
Definition cost_N_IDip : S.t := S.safe_int 10.
Definition cost_N_IDipN (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 30)
(S_syntax.op_plus
(S_syntax.op_plus (S_syntax.op_star (S.safe_int 2) v0)
(S_syntax.lsr v0 1)) (S_syntax.lsr v0 3)).
Definition cost_N_IView : S.t := S.safe_int 1460.
Definition cost_N_IDrop : S.t := S.safe_int 10.
Definition cost_N_IDropN (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus
(S_syntax.op_plus
(S_syntax.op_plus (S.safe_int 30) (S_syntax.op_star (S.safe_int 2) v0))
(S_syntax.lsr v0 1)) (S_syntax.lsr v0 3).
Definition cost_N_IDug (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 35)
(S_syntax.op_plus
(S_syntax.op_plus (S_syntax.op_star (S.safe_int 6) v0)
(S_syntax.lsr v0 1)) (S_syntax.lsr v0 2)).
Definition cost_N_IDup : S.t := S.safe_int 10.
Definition cost_N_IDupN (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 20) v0) (S_syntax.lsr v0 3).
Definition cost_div_int (size1 : int) (size2 : int) : S.t :=
let q_value := size1 -i size2 in
if q_value <i 0 then
S.safe_int 105
else
let v0 := S_syntax.op_star (S.safe_int q_value) (S.safe_int size2) in
S_syntax.op_plus
(S_syntax.op_plus
(S_syntax.op_plus (S.safe_int 105) (S_syntax.lsr v0 10))
(S_syntax.lsr v0 11)) (S_syntax.lsr v0 13).
Definition cost_N_IEdiv_int : int → int → S.t := cost_div_int.
Definition cost_N_IEdiv_nat : int → int → S.t := cost_div_int.
Definition cost_N_IEdiv_tez : S.t := S.safe_int 80.
Definition cost_N_IEdiv_teznat : S.t := S.safe_int 70.
Definition cost_N_IEmpty_big_map : S.t := S.safe_int 10.
Definition cost_N_IEmpty_map : S.t := S.safe_int 220.
Definition cost_N_IEmpty_set : S.t := S.safe_int 220.
Definition cost_N_IEq : S.t := S.safe_int 10.
Definition cost_N_IExec : S.t := S.safe_int 10.
Definition cost_N_IGe : S.t := S.safe_int 10.
Definition cost_N_IGt : S.t := S.safe_int 10.
Definition cost_N_IHalt : S.t := S.safe_int 10.
Definition cost_N_IHash_key : S.t := S.safe_int 605.
Definition cost_N_IIf : S.t := S.safe_int 10.
Definition cost_N_IIf_cons : S.t := S.safe_int 10.
Definition cost_N_IIf_left : S.t := S.safe_int 10.
Definition cost_N_IIf_none : S.t := S.safe_int 10.
Definition cost_opt_map : S.t := S.safe_int 10.
Definition cost_N_IImplicit_account : S.t := S.safe_int 10.
Definition cost_N_IInt_bls12_381_z_fr : S.t := S.safe_int 115.
Definition cost_N_IInt_nat : S.t := S.safe_int 10.
Definition cost_N_IIs_nat : S.t := S.safe_int 10.
Definition cost_N_IKeccak (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 1350)
(S_syntax.op_plus (S_syntax.op_star (S.safe_int 8) v0)
(S_syntax.lsr v0 2)).
Definition cost_N_ILambda : S.t := S.safe_int 10.
Definition cost_N_ILe : S.t := S.safe_int 10.
Definition cost_N_ILeft : S.t := S.safe_int 10.
Definition cost_N_ILevel : S.t := S.safe_int 10.
Definition cost_N_IList_iter {A : Set} (function_parameter : A) : S.t :=
let '_ := function_parameter in
S.safe_int 20.
Definition cost_N_IList_map {A : Set} (function_parameter : A) : S.t :=
let '_ := function_parameter in
S.safe_int 20.
Definition cost_N_IList_size : S.t := S.safe_int 10.
Definition cost_N_ILoop : S.t := S.safe_int 10.
Definition cost_N_ILoop_left : S.t := S.safe_int 10.
Definition cost_N_ILsl_nat (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 40)
(S_syntax.op_plus
(S_syntax.op_plus (S_syntax.lsr v0 4) (S_syntax.lsr v0 5))
(S_syntax.lsr v0 6)).
Definition cost_N_ILsr_nat (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 45)
(S_syntax.op_plus
(S_syntax.op_plus (S_syntax.lsr v0 4) (S_syntax.lsr v0 5))
(S_syntax.lsr v0 6)).
Definition cost_N_ILt : S.t := S.safe_int 10.
Definition cost_N_IMap_get (size1 : S.t) (size2 : S.t) : S.t :=
let v0 := S_syntax.op_star size1 (S_syntax.log2 size2) in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 45) (S_syntax.lsr v0 5))
(S_syntax.lsr v0 6).
Definition cost_N_IMap_get_and_update (size1 : S.t) (size2 : S.t) : S.t :=
let v0 := S_syntax.op_star size1 (S_syntax.log2 size2) in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 75) (S_syntax.lsr v0 3))
(S_syntax.lsr v0 6).
Definition cost_N_IMap_iter (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus
(S_syntax.op_plus
(S_syntax.op_plus (S.safe_int 50) (S_syntax.op_star (S.safe_int 7) v0))
(S_syntax.lsr v0 1)) (S_syntax.lsr v0 3).
Definition cost_N_IMap_map (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 50)
(S_syntax.op_plus (S_syntax.op_star (S.safe_int 7) v0)
(S_syntax.lsr v0 1)).
Definition cost_N_IMap_mem (size1 : S.t) (size2 : S.t) : S.t :=
let v0 := S_syntax.op_star size1 (S_syntax.log2 size2) in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 45) (S_syntax.lsr v0 5))
(S_syntax.lsr v0 6).
Definition cost_N_IMap_size : S.t := S.safe_int 10.
Definition cost_N_IMap_update (size1 : S.t) (size2 : S.t) : S.t :=
let v0 := S_syntax.op_star size1 (S_syntax.log2 size2) in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 55) (S_syntax.lsr v0 4))
(S_syntax.lsr v0 5).
Definition cost_N_IMul_bls12_381_fr : S.t := S.safe_int 45.
Definition cost_N_IMul_bls12_381_fr_z (size1 : int) : S.t :=
let v0 := S.safe_int size1 in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 265) v0)
(S_syntax.lsr v0 4).
Definition cost_N_IMul_bls12_381_g1 : S.t := S.safe_int 103000.
Definition cost_N_IMul_bls12_381_g2 : S.t := S.safe_int 220000.
Definition cost_N_IMul_bls12_381_z_fr (size1 : int) : S.t :=
let v0 := S.safe_int size1 in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 265) v0)
(S_syntax.lsr v0 4).
Definition cost_mul (size1 : int) (size2 : int) : S.t :=
let a_value := S.add (S.safe_int size1) (S.safe_int size2) in
let v0 := S_syntax.op_star a_value (S_syntax.log2 a_value) in
S_syntax.op_plus
(S_syntax.op_plus (S_syntax.op_plus (S.safe_int 55) (S_syntax.lsr v0 1))
(S_syntax.lsr v0 2)) (S_syntax.lsr v0 4).
Definition cost_N_IMul_int : int → int → S.t := cost_mul.
Definition cost_N_IMul_nat : int → int → S.t := cost_mul.
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_INeg_bls12_381_fr : S.t := S.safe_int 25.
Definition cost_N_INeg_bls12_381_g1 : S.t := S.safe_int 50.
Definition cost_N_INeg_bls12_381_g2 : S.t := S.safe_int 70.
Definition cost_N_INeg (size_value : int) : S.t :=
S_syntax.op_plus (S.safe_int 25) (S_syntax.lsr (S.safe_int size_value) 4).
Definition cost_N_INeq : S.t := S.safe_int 10.
Definition cost_N_INil : S.t := S.safe_int 10.
Definition cost_N_INot : S.t := S.safe_int 10.
Definition cost_N_INot_int (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 25)
(S_syntax.op_plus (S_syntax.lsr v0 4) (S_syntax.lsr v0 7)).
Definition cost_N_INow : S.t := S.safe_int 10.
Definition cost_N_IMin_block_time : S.t := S.safe_int 20.
Definition cost_N_IOpen_chest (chest_value : int) (time : int) : S.t :=
let v0 := S.safe_int chest_value in
let v1 := S.safe_int time in
S_syntax.op_plus
(S_syntax.op_plus (S.safe_int 612000)
(S_syntax.op_star (S.safe_int 19) v0))
(S_syntax.op_star (S.safe_int 19050) v1).
Definition cost_N_IOr : S.t := S.safe_int 10.
Definition cost_N_IOr_nat : int → int → S.t := cost_linear_op_int.
Definition cost_N_IPairing_check_bls12_381 (size_value : int) : S.t :=
S.add (S.safe_int 450000)
(S.mul (S.safe_int 342500) (S.safe_int size_value)).
Definition cost_N_IRead_ticket : S.t := S.safe_int 10.
Definition cost_N_IRight : S.t := S.safe_int 10.
Definition cost_N_ISapling_empty_state : S.t := S.safe_int 10.
Definition cost_N_ISapling_verify_update
(size1 : int) (size2 : int) (bound_data : int) : S.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_ISelf_address : S.t := S.safe_int 10.
Definition cost_N_ISelf : S.t := S.safe_int 10.
Definition cost_N_ISender : S.t := S.safe_int 10.
Definition cost_N_ISet_delegate : S.t := S.safe_int 30.
Definition cost_N_ISet_iter (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus
(S_syntax.op_plus
(S_syntax.op_plus (S.safe_int 50) (S_syntax.op_star (S.safe_int 7) v0))
(S_syntax.lsr v0 1)) (S_syntax.lsr v0 3).
Definition cost_N_ISet_size : S.t := S.safe_int 10.
Definition cost_N_ISha256 (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 600)
(S_syntax.op_plus
(S_syntax.op_plus (S_syntax.op_star (S.safe_int 4) v0)
(S_syntax.lsr v0 1)) (S_syntax.lsr v0 2)).
Definition cost_N_ISha3 : int → S.t := cost_N_IKeccak.
Definition cost_N_ISha512 (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 680) (S_syntax.op_star (S.safe_int 3) v0).
Definition cost_N_ISlice_bytes (size_value : int) : S.t :=
S_syntax.op_plus (S.safe_int 25) (S_syntax.lsr (S.safe_int size_value) 4).
Definition cost_N_ISlice_string (size_value : int) : S.t :=
S_syntax.op_plus (S.safe_int 25) (S_syntax.lsr (S.safe_int size_value) 4).
Definition cost_N_ISource : S.t := S.safe_int 10.
Definition cost_N_ISplit_ticket (size1 : int) (size2 : int) : S.t :=
let v1 := S.safe_int (Compare.Int.max size1 size2) in
S_syntax.op_plus (S.safe_int 40) (S_syntax.lsr v1 3).
Definition cost_N_IString_size : S.t := S.safe_int 15.
Definition cost_N_ISub_int : int → int → S.t := cost_linear_op_int.
Definition cost_N_ISub_tez : S.t := S.safe_int 15.
Definition cost_N_ISub_tez_legacy : S.t := S.safe_int 20.
Definition cost_N_ISub_timestamp_seconds : int → int → S.t :=
cost_linear_op_int.
Definition cost_N_ISwap : S.t := S.safe_int 10.
Definition cost_N_ITicket : S.t := S.safe_int 10.
Definition cost_N_ITotal_voting_power : S.t := S.safe_int 370.
Definition cost_N_ITransfer_tokens : S.t := S.safe_int 30.
Definition cost_N_IUncomb (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 25) (S_syntax.op_star (S.safe_int 4) v0).
Definition cost_N_IUnpair : S.t := S.safe_int 10.
Definition cost_N_IVoting_power : S.t := S.safe_int 530.
Definition cost_N_IXor : S.t := S.safe_int 15.
Definition cost_N_IXor_nat : int → int → S.t := cost_linear_op_int.
Definition cost_N_KCons : S.t := S.safe_int 10.
Definition cost_N_KIter : S.t := S.safe_int 10.
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_N_KList_exit_body : S.t := S.safe_int 10.
Definition cost_N_KLoop_in : S.t := S.safe_int 10.
Definition cost_N_KLoop_in_left : S.t := S.safe_int 10.
Definition cost_N_KMap_enter_body : S.t := S.safe_int 80.
Definition cost_N_KNil : S.t := S.safe_int 10.
Definition cost_N_KReturn : S.t := S.safe_int 10.
Definition cost_N_KView_exit : S.t := S.safe_int 20.
Definition cost_N_KMap_head : S.t := S.safe_int 20.
Definition cost_N_KUndip : S.t := S.safe_int 10.
Definition cost_DECODING_BLS_FR : S.t := S.safe_int 120.
Definition cost_DECODING_BLS_G1 : S.t := S.safe_int 54600.
Definition cost_DECODING_BLS_G2 : S.t := S.safe_int 69000.
Definition cost_B58CHECK_DECODING_CHAIN_ID : S.t := S.safe_int 1600.
Definition cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_ed25519 : S.t :=
S.safe_int 3300.
Definition cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_p256 : S.t :=
S.safe_int 3300.
Definition cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_secp256k1 : S.t :=
S.safe_int 3300.
Definition cost_B58CHECK_DECODING_PUBLIC_KEY_ed25519 : S.t :=
S.safe_int 4200.
Definition cost_B58CHECK_DECODING_PUBLIC_KEY_p256 : S.t :=
S.safe_int 325000.
Definition cost_B58CHECK_DECODING_PUBLIC_KEY_secp256k1 : S.t :=
S.safe_int 9000.
Definition cost_B58CHECK_DECODING_SIGNATURE_ed25519 : S.t :=
S.safe_int 6400.
Definition cost_B58CHECK_DECODING_SIGNATURE_p256 : S.t := S.safe_int 6400.
Definition cost_B58CHECK_DECODING_SIGNATURE_secp256k1 : S.t :=
S.safe_int 6400.
Definition cost_ENCODING_BLS_FR : S.t := S.safe_int 80.
Definition cost_ENCODING_BLS_G1 : S.t := S.safe_int 3200.
Definition cost_ENCODING_BLS_G2 : S.t := S.safe_int 3900.
Definition cost_B58CHECK_ENCODING_CHAIN_ID : S.t := S.safe_int 1800.
Definition cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_ed25519 : S.t :=
S.safe_int 3200.
Definition cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_p256 : S.t :=
S.safe_int 3200.
Definition cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_secp256k1 : S.t :=
S.safe_int 3200.
Definition cost_B58CHECK_ENCODING_PUBLIC_KEY_ed25519 : S.t :=
S.safe_int 4500.
Definition cost_B58CHECK_ENCODING_PUBLIC_KEY_p256 : S.t := S.safe_int 4550.
Definition cost_B58CHECK_ENCODING_PUBLIC_KEY_secp256k1 : S.t :=
S.safe_int 4950.
Definition cost_B58CHECK_ENCODING_SIGNATURE_ed25519 : S.t :=
S.safe_int 8300.
Definition cost_B58CHECK_ENCODING_SIGNATURE_p256 : S.t := S.safe_int 8300.
Definition cost_B58CHECK_ENCODING_SIGNATURE_secp256k1 : S.t :=
S.safe_int 8300.
Definition cost_DECODING_CHAIN_ID : S.t := S.safe_int 50.
Definition cost_DECODING_PUBLIC_KEY_HASH_ed25519 : S.t := S.safe_int 50.
Definition cost_DECODING_PUBLIC_KEY_HASH_p256 : S.t := S.safe_int 50.
Definition cost_DECODING_PUBLIC_KEY_HASH_secp256k1 : S.t := S.safe_int 50.
Definition cost_DECODING_PUBLIC_KEY_ed25519 : S.t := S.safe_int 60.
Definition cost_DECODING_PUBLIC_KEY_p256 : S.t := S.safe_int 320000.
Definition cost_DECODING_PUBLIC_KEY_secp256k1 : S.t := S.safe_int 4900.
Definition cost_DECODING_SIGNATURE_ed25519 : S.t := S.safe_int 35.
Definition cost_DECODING_SIGNATURE_p256 : S.t := S.safe_int 35.
Definition cost_DECODING_SIGNATURE_secp256k1 : S.t := S.safe_int 35.
Definition cost_DECODING_Chest_key : S.t := S.safe_int 5900.
Definition cost_DECODING_Chest (bytes_value : int) : S.t :=
let v0 := S.safe_int bytes_value in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 7400) (S_syntax.lsr v0 5))
(S_syntax.lsr v0 7).
Definition cost_ENCODING_CHAIN_ID : S.t := S.safe_int 50.
Definition cost_ENCODING_PUBLIC_KEY_HASH_ed25519 : S.t := S.safe_int 70.
Definition cost_ENCODING_PUBLIC_KEY_HASH_p256 : S.t := S.safe_int 70.
Definition cost_ENCODING_PUBLIC_KEY_HASH_secp256k1 : S.t := S.safe_int 70.
Definition cost_ENCODING_PUBLIC_KEY_ed25519 : S.t := S.safe_int 80.
Definition cost_ENCODING_PUBLIC_KEY_p256 : S.t := S.safe_int 90.
Definition cost_ENCODING_PUBLIC_KEY_secp256k1 : S.t := S.safe_int 455.
Definition cost_ENCODING_SIGNATURE_ed25519 : S.t := S.safe_int 45.
Definition cost_ENCODING_SIGNATURE_p256 : S.t := S.safe_int 45.
Definition cost_ENCODING_SIGNATURE_secp256k1 : S.t := S.safe_int 45.
Definition cost_ENCODING_Chest_key : S.t := S.safe_int 13500.
Definition cost_ENCODING_Chest (plaintext_size : int) : S.t :=
let v0 := S.safe_int plaintext_size in
S_syntax.op_plus (S.safe_int 16630) (S_syntax.lsr v0 3).
Definition cost_TIMESTAMP_READABLE_DECODING (bytes_value : int) : S.t :=
let b_value := S.safe_int bytes_value in
let v0 := S.mul (S.sqrt b_value) b_value in
S_syntax.op_plus (S.safe_int 800)
(S_syntax.op_plus (S_syntax.lsr v0 2) (S_syntax.lsr v0 3)).
Definition cost_TIMESTAMP_READABLE_ENCODING : S.t := S.safe_int 100.
Definition cost_CHECK_PRINTABLE (size_value : int) : S.t :=
S_syntax.op_plus (S.safe_int 14)
(S_syntax.op_star (S.safe_int 10) (S.safe_int size_value)).
Definition cost_TY_EQ : S.t := S.safe_int 60.
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 45.
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_UNPARSE_COMPARABLE_TYPE (type_size : S.t) : S.t :=
S.mul (S.safe_int 20) type_size.
Definition cost_COMPARABLE_TY_OF_TY : S.t := S.safe_int 120.
Definition cost_FIND_ENTRYPOINT : S.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)).
End Generated_costs.
Module Interpreter.
Definition drop : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IDrop.
Definition dup : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IDup.
Definition swap : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISwap.
Definition cons_some : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ICons_some.
Definition cons_none : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ICons_none.
Definition if_none : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IIf_none.
Definition opt_map : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_opt_map.
Definition cons_pair : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ICons_pair.
Definition unpair : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IUnpair.
Definition car : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ICar.
Definition cdr : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ICdr.
Definition cons_left : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ILeft.
Definition cons_right : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IRight.
Definition if_left : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IIf_left.
Definition cons_list : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ICons_list.
Definition nil : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_INil.
Definition if_cons : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IIf_cons.
Definition list_map {a : Set}
(function_parameter : Script_typed_ir.boxed_list a)
: Alpha_context.Gas.cost :=
let '{| Script_typed_ir.boxed_list.length := length |} :=
function_parameter in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IList_map length).
Definition list_size : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IList_size.
Definition list_iter {a : Set}
(function_parameter : Script_typed_ir.boxed_list a)
: Alpha_context.Gas.cost :=
let '{| Script_typed_ir.boxed_list.length := length |} :=
function_parameter in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IList_iter length).
Definition empty_set : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IEmpty_set.
Definition set_iter {a : Set} (set : Script_typed_ir.set a)
: Alpha_context.Gas.cost :=
let Box := Script_set.get set in
let 'existS _ _ Box := Box in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISet_iter
Box.(Script_typed_ir.Boxed_set.size_value)).
Definition set_size : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISet_size.
Definition empty_map : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IEmpty_map.
Definition map_map {k v : Set} (map : Script_typed_ir.map k v)
: Alpha_context.Gas.cost :=
let Box := Script_map.get_module map in
let 'existS _ _ Box := Box in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMap_map
Box.(Script_typed_ir.Boxed_map.size_value)).
Definition map_iter {k v : Set} (map : Script_typed_ir.map k v)
: Alpha_context.Gas.cost :=
let Box := Script_map.get_module map in
let 'existS _ _ Box := Box in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMap_iter
Box.(Script_typed_ir.Boxed_map.size_value)).
Definition map_size : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IMap_size.
Definition big_map_elt_size : S.t := S.safe_int Script_expr_hash.size_value.
Definition big_map_mem {A B : Set}
(function_parameter : Script_typed_ir.big_map_overlay A B)
: Alpha_context.Gas.cost :=
let '{| Script_typed_ir.big_map_overlay.size := size_value |} :=
function_parameter in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMap_mem big_map_elt_size
(S.safe_int size_value)).
Definition big_map_get {A B : Set}
(function_parameter : Script_typed_ir.big_map_overlay A B)
: Alpha_context.Gas.cost :=
let '{| Script_typed_ir.big_map_overlay.size := size_value |} :=
function_parameter in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMap_get big_map_elt_size
(S.safe_int size_value)).
Definition big_map_update {A B : Set}
(function_parameter : Script_typed_ir.big_map_overlay A B)
: Alpha_context.Gas.cost :=
let '{| Script_typed_ir.big_map_overlay.size := size_value |} :=
function_parameter in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMap_update big_map_elt_size
(S.safe_int size_value)).
Definition big_map_get_and_update {A B : Set}
(function_parameter : Script_typed_ir.big_map_overlay A B)
: Alpha_context.Gas.cost :=
let '{| Script_typed_ir.big_map_overlay.size := size_value |} :=
function_parameter in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMap_get_and_update big_map_elt_size
(S.safe_int size_value)).
Definition add_seconds_timestamp
(seconds : Alpha_context.Script_int.num)
(timestamp : Alpha_context.Script_timestamp.t) : Alpha_context.Gas.cost :=
let seconds_bytes := int_bytes seconds in
let timestamp_bytes :=
z_bytes (Alpha_context.Script_timestamp.to_zint timestamp) in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IAdd_seconds_to_timestamp seconds_bytes
timestamp_bytes).
Definition add_timestamp_seconds
(timestamp : Alpha_context.Script_timestamp.t)
(seconds : Alpha_context.Script_int.num) : Alpha_context.Gas.cost :=
let seconds_bytes := int_bytes seconds in
let timestamp_bytes :=
z_bytes (Alpha_context.Script_timestamp.to_zint timestamp) in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IAdd_timestamp_to_seconds timestamp_bytes
seconds_bytes).
Definition sub_timestamp_seconds
(timestamp : Alpha_context.Script_timestamp.t)
(seconds : Alpha_context.Script_int.num) : Alpha_context.Gas.cost :=
let seconds_bytes := int_bytes seconds in
let timestamp_bytes :=
z_bytes (Alpha_context.Script_timestamp.to_zint timestamp) in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISub_timestamp_seconds timestamp_bytes
seconds_bytes).
Definition diff_timestamps
(t1 : Alpha_context.Script_timestamp.t)
(t2 : Alpha_context.Script_timestamp.t) : Alpha_context.Gas.cost :=
let t1_bytes := z_bytes (Alpha_context.Script_timestamp.to_zint t1) in
let t2_bytes := z_bytes (Alpha_context.Script_timestamp.to_zint t2) in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IDiff_timestamps t1_bytes t2_bytes).
Definition concat_string_pair
(s1 : Alpha_context.Script_string.t) (s2 : Alpha_context.Script_string.t)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IConcat_string_pair
(Alpha_context.Script_string.length s1)
(Alpha_context.Script_string.length s2)).
Definition slice_string (s_value : Alpha_context.Script_string.t)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISlice_string
(Alpha_context.Script_string.length s_value)).
Definition string_size : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IString_size.
Definition concat_bytes_pair (b1 : bytes) (b2 : bytes)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IConcat_bytes_pair (Bytes.length b1)
(Bytes.length b2)).
Definition slice_bytes (b_value : bytes) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISlice_bytes (Bytes.length b_value)).
Definition bytes_size : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IBytes_size.
Definition add_tez : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IAdd_tez.
Definition sub_tez : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISub_tez.
Definition sub_tez_legacy : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISub_tez_legacy.
Definition mul_teznat : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IMul_teznat.
Definition mul_nattez : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IMul_nattez.
Definition bool_or : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IOr.
Definition bool_and : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IAnd.
Definition bool_xor : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IXor.
Definition bool_not : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_INot.
Definition is_nat : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IIs_nat.
Definition abs_int (i_value : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IAbs_int (int_bytes i_value)).
Definition int_nat : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IInt_nat.
Definition neg (i_value : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_INeg (int_bytes i_value)).
Definition add_int
(i1 : Alpha_context.Script_int.num) (i2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IAdd_int (int_bytes i1) (int_bytes i2)).
Definition add_nat
(i1 : Alpha_context.Script_int.num) (i2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IAdd_nat (int_bytes i1) (int_bytes i2)).
Definition sub_int
(i1 : Alpha_context.Script_int.num) (i2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISub_int (int_bytes i1) (int_bytes i2)).
Definition mul_int
(i1 : Alpha_context.Script_int.num) (i2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMul_int (int_bytes i1) (int_bytes i2)).
Definition mul_nat
(i1 : Alpha_context.Script_int.num) (i2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMul_nat (int_bytes i1) (int_bytes i2)).
Definition ediv_teznat {A B : Set} (_tez : A) (_n : B)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IEdiv_teznat.
Definition ediv_tez : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IEdiv_tez.
Definition ediv_int
(i1 : Alpha_context.Script_int.num) (i2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IEdiv_int (int_bytes i1) (int_bytes i2)).
Definition ediv_nat
(i1 : Alpha_context.Script_int.num) (i2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IEdiv_nat (int_bytes i1) (int_bytes i2)).
Definition eq_value : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IEq.
Definition lsl_nat (shifted : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ILsl_nat (int_bytes shifted)).
Definition lsr_nat (shifted : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ILsr_nat (int_bytes shifted)).
Definition or_nat
(n1 : Alpha_context.Script_int.num) (n2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IOr_nat (int_bytes n1) (int_bytes n2)).
Definition and_nat
(n1 : Alpha_context.Script_int.num) (n2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IAnd_nat (int_bytes n1) (int_bytes n2)).
Definition and_int_nat
(n1 : Alpha_context.Script_int.num) (n2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IAnd_int_nat (int_bytes n1) (int_bytes n2)).
Definition xor_nat
(n1 : Alpha_context.Script_int.num) (n2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IXor_nat (int_bytes n1) (int_bytes n2)).
Definition not_int (i_value : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_INot_int (int_bytes i_value)).
Definition if_ : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IIf.
Definition loop : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ILoop.
Definition loop_left : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ILoop_left.
Definition dip : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IDip.
Definition view : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IView.
Definition check_signature (pkey : Signature.public_key) (b_value : bytes)
: Alpha_context.Gas.cost :=
let cost :=
match pkey with
| Signature.Ed25519 _ ⇒
Generated_costs.cost_N_ICheck_signature_ed25519 (Bytes.length b_value)
| Signature.Secp256k1 _ ⇒
Generated_costs.cost_N_ICheck_signature_secp256k1
(Bytes.length b_value)
| Signature.P256 _ ⇒
Generated_costs.cost_N_ICheck_signature_p256 (Bytes.length b_value)
end in
Alpha_context.Gas.atomic_step_cost cost.
Definition blake2b (b_value : bytes) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IBlake2b (Bytes.length b_value)).
Definition sha256 (b_value : bytes) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISha256 (Bytes.length b_value)).
Definition sha512 (b_value : bytes) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISha512 (Bytes.length b_value)).
Definition dign (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_IDig n_value).
Definition dugn (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_IDug n_value).
Definition dipn (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_IDipN n_value).
Definition dropn (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_IDropN n_value).
Definition voting_power : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IVoting_power.
Definition total_voting_power : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_ITotal_voting_power.
Definition keccak (b_value : bytes) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IKeccak (Bytes.length b_value)).
Definition sha3 (b_value : bytes) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISha3 (Bytes.length b_value)).
Definition add_bls12_381_g1 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_IAdd_bls12_381_g1.
Definition add_bls12_381_g2 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_IAdd_bls12_381_g2.
Definition add_bls12_381_fr : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_IAdd_bls12_381_fr.
Definition mul_bls12_381_g1 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_IMul_bls12_381_g1.
Definition mul_bls12_381_g2 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_IMul_bls12_381_g2.
Definition mul_bls12_381_fr : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_IMul_bls12_381_fr.
Definition mul_bls12_381_fr_z (z_value : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMul_bls12_381_fr_z (int_bytes z_value)).
Definition mul_bls12_381_z_fr (z_value : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMul_bls12_381_z_fr (int_bytes z_value)).
Definition int_bls12_381_fr : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_IInt_bls12_381_z_fr.
Definition neg_bls12_381_g1 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_INeg_bls12_381_g1.
Definition neg_bls12_381_g2 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_INeg_bls12_381_g2.
Definition neg_bls12_381_fr : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_INeg_bls12_381_fr.
Definition neq : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_INeq.
Definition pairing_check_bls12_381 {a : Set}
(l_value : Script_typed_ir.boxed_list a) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IPairing_check_bls12_381
l_value.(Script_typed_ir.boxed_list.length)).
Definition comb (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_IComb n_value).
Definition uncomb (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IUncomb n_value).
Definition comb_get (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IComb_get n_value).
Definition comb_set (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IComb_set n_value).
Definition dupn (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_IDupN n_value).
Definition sapling_verify_update
(inputs : int) (outputs : int) (bound_data : int)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISapling_verify_update inputs outputs bound_data).
Definition sapling_verify_update_deprecated (inputs : int) (outputs : int)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISapling_verify_update inputs outputs 0).
Definition sapling_empty_state : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_ISapling_empty_state.
Definition halt : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IHalt.
Definition const : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IConst.
Definition empty_big_map : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IEmpty_big_map.
Definition lt : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ILt.
Definition le : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ILe.
Definition gt : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IGt.
Definition ge : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IGe.
Definition exec : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IExec.
Definition apply : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IApply.
Definition lambda : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ILambda.
Definition address : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IAddress.
Definition contract : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IContract.
Definition transfer_tokens : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ITransfer_tokens.
Definition implicit_account : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_IImplicit_account.
Definition create_contract : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ICreate_contract.
Definition set_delegate : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISet_delegate.
Definition level : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ILevel.
Definition now : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_INow.
Definition min_block_time : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IMin_block_time.
Definition source : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISource.
Definition sender : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISender.
Definition self : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISelf.
Definition self_address : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISelf_address.
Definition amount : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IAmount.
Definition chain_id : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IChainId.
Definition ticket : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ITicket.
Definition read_ticket : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IRead_ticket.
Definition hash_key {A : Set} (function_parameter : A)
: Alpha_context.Gas.cost :=
let '_ := function_parameter in
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IHash_key.
Definition split_ticket {A : Set} (function_parameter : A)
: Alpha_context.Script_int.num → Alpha_context.Script_int.num →
Alpha_context.Gas.cost :=
let '_ := function_parameter in
fun (amount_a : Alpha_context.Script_int.num) ⇒
fun (amount_b : Alpha_context.Script_int.num) ⇒
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISplit_ticket (int_bytes amount_a)
(int_bytes amount_b)).
Definition open_chest
(chest_value : Script_typed_ir.Script_timelock.chest) (time : Z.t)
: Alpha_context.Gas.cost :=
let plaintext :=
Script_typed_ir.Script_timelock.get_plaintext_size chest_value in
let log_time := Z.log2 (Z.one +Z time) in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IOpen_chest plaintext log_time).
Definition compare_unit : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (S.safe_int 10).
Definition compare_pair_tag : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (S.safe_int 10).
Definition compare_union_tag : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (S.safe_int 10).
Definition compare_option_tag : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (S.safe_int 10).
Definition compare_bool : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_ICompare 1 1).
Definition compare_signature : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (S.safe_int 92).
Definition compare_string
(s1 : Alpha_context.Script_string.t) (s2 : Alpha_context.Script_string.t)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ICompare (Alpha_context.Script_string.length s1)
(Alpha_context.Script_string.length s2)).
Definition compare_bytes (b1 : bytes) (b2 : bytes)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ICompare (Bytes.length b1) (Bytes.length b2)).
Definition compare_mutez : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_ICompare 8 8).
Definition compare_int
(i1 : Alpha_context.Script_int.num) (i2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ICompare (int_bytes i1) (int_bytes i2)).
Definition compare_nat
(n1 : Alpha_context.Script_int.num) (n2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ICompare (int_bytes n1) (int_bytes n2)).
Definition compare_key_hash : Alpha_context.Gas.cost :=
let sz :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value) in
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_ICompare sz sz).
Definition compare_key : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (S.safe_int 92).
Definition compare_timestamp
(t1 : Alpha_context.Script_timestamp.t)
(t2 : Alpha_context.Script_timestamp.t) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ICompare
(z_bytes (Alpha_context.Script_timestamp.to_zint t1))
(z_bytes (Alpha_context.Script_timestamp.to_zint t2))).
Definition entrypoint_size : int := 31.
Definition compare_address : Alpha_context.Gas.cost :=
let sz :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value) +i
entrypoint_size in
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_ICompare sz sz).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Gas_input_size.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_map.
Require TezosOfOCaml.Proto_alpha.Script_set.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Storage_costs.
Module S := Saturation_repr.
Module Size := Gas_input_size.
Module Cost_of.
Module S_syntax.
Definition log2 (x_value : S.t) : S.t :=
S.safe_int (1 +i (S.numbits x_value)).
Definition op_plus : S.t → S.t → S.t := S.add.
Definition op_star : S.t → S.t → S.t := S.mul.
Definition lsr : S.t → int → S.t := S.shift_right.
End S_syntax.
Definition z_bytes (z_value : Z.t) : int :=
let bits := Z.numbits z_value in
(7 +i bits) /i 8.
Definition int_bytes (z_value : Alpha_context.Script_int.num) : int :=
z_bytes (Alpha_context.Script_int.to_zint z_value).
Definition manager_operation : Alpha_context.Gas.cost :=
Alpha_context.Gas.step_cost (S.safe_int 1000).
Module Generated_costs.
Definition cost_N_IAbs_int (size_value : int) : S.t :=
S.safe_int (20 +i (Pervasives.lsr size_value 4)).
Definition cost_N_IAdd_bls12_381_fr : S.t := S.safe_int 30.
Definition cost_N_IAdd_bls12_381_g1 : S.t := S.safe_int 900.
Definition cost_N_IAdd_bls12_381_g2 : S.t := S.safe_int 2470.
Definition cost_linear_op_int (size1 : int) (size2 : int) : S.t :=
let v0 := S.safe_int (Compare.Int.max size1 size2) in
S_syntax.op_plus (S.safe_int 35)
(S_syntax.op_plus (S_syntax.lsr v0 4) (S_syntax.lsr v0 7)).
Definition cost_N_IAdd_int : int → int → S.t := cost_linear_op_int.
Definition cost_N_IAdd_nat : int → int → S.t := cost_linear_op_int.
Definition cost_N_IAdd_seconds_to_timestamp : int → int → S.t :=
cost_linear_op_int.
Definition cost_N_IAdd_tez : S.t := S.safe_int 20.
Definition cost_N_IAdd_timestamp_to_seconds : int → int → S.t :=
cost_linear_op_int.
Definition cost_N_IAddress : S.t := S.safe_int 10.
Definition cost_N_IAmount : S.t := S.safe_int 10.
Definition cost_N_IAnd : S.t := S.safe_int 10.
Definition cost_N_IAnd_int_nat (size1 : int) (size2 : int) : S.t :=
let v0 := S.safe_int (Compare.Int.min size1 size2) in
S_syntax.op_plus (S.safe_int 35)
(S_syntax.op_plus (S_syntax.lsr v0 3) (S_syntax.lsr v0 6)).
Definition cost_N_IAnd_nat (size1 : int) (size2 : int) : S.t :=
let v0 := S.safe_int (Compare.Int.min size1 size2) in
S_syntax.op_plus (S.safe_int 35)
(S_syntax.op_plus (S_syntax.lsr v0 4) (S_syntax.lsr v0 7)).
Definition cost_N_IApply : S.t := S.safe_int 140.
Definition cost_N_IBlake2b (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 430) v0)
(S_syntax.lsr v0 3).
Definition cost_N_IBytes_size : S.t := S.safe_int 10.
Definition cost_N_ICar : S.t := S.safe_int 10.
Definition cost_N_ICdr : S.t := S.safe_int 10.
Definition cost_N_IChainId : S.t := S.safe_int 15.
Definition cost_N_ICheck_signature_ed25519 (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 65800)
(S_syntax.op_plus v0 (S_syntax.lsr v0 3)).
Definition cost_N_ICheck_signature_p256 (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 990000)
(S_syntax.op_plus v0 (S_syntax.lsr v0 3)).
Definition cost_N_ICheck_signature_secp256k1 (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 51600)
(S_syntax.op_plus v0 (S_syntax.lsr v0 3)).
Definition cost_N_IComb (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus
(S_syntax.op_plus (S_syntax.op_star (S.safe_int 3) v0)
(S_syntax.lsr v0 1)) (S_syntax.lsr v0 5).
Definition cost_N_IComb_get (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 20) (S_syntax.lsr v0 1))
(S_syntax.lsr v0 4).
Definition cost_N_IComb_set (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 20)
(S_syntax.op_plus (S_syntax.op_plus v0 (S_syntax.lsr v0 2))
(S_syntax.lsr v0 5)).
Definition cost_N_ICompare (size1 : int) (size2 : int) : S.t :=
let v0 := S.safe_int (Compare.Int.min size1 size2) in
S_syntax.op_plus (S.safe_int 35)
(S_syntax.op_plus (S_syntax.lsr v0 6) (S_syntax.lsr v0 7)).
Definition cost_N_IConcat_bytes_pair (size1 : int) (size2 : int) : S.t :=
let v0 := S_syntax.op_plus (S.safe_int size1) (S.safe_int size2) in
S_syntax.op_plus (S.safe_int 45) (S_syntax.lsr v0 4).
Definition cost_N_IConcat_string_pair (size1 : int) (size2 : int) : S.t :=
let v0 := S_syntax.op_plus (S.safe_int size1) (S.safe_int size2) in
S_syntax.op_plus (S.safe_int 45) (S_syntax.lsr v0 4).
Definition cost_N_ICons_list : S.t := S.safe_int 10.
Definition cost_N_ICons_none : S.t := S.safe_int 10.
Definition cost_N_ICons_pair : S.t := S.safe_int 10.
Definition cost_N_ICons_some : S.t := S.safe_int 10.
Definition cost_N_IConst : S.t := S.safe_int 10.
Definition cost_N_IContract : S.t := S.safe_int 30.
Definition cost_N_ICreate_contract : S.t := S.safe_int 30.
Definition cost_N_IDiff_timestamps : int → int → S.t :=
cost_linear_op_int.
Definition cost_N_IDig (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 30)
(S_syntax.op_plus
(S_syntax.op_plus (S_syntax.op_star (S.safe_int 6) v0)
(S_syntax.lsr v0 1)) (S_syntax.lsr v0 2)).
Definition cost_N_IDip : S.t := S.safe_int 10.
Definition cost_N_IDipN (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 30)
(S_syntax.op_plus
(S_syntax.op_plus (S_syntax.op_star (S.safe_int 2) v0)
(S_syntax.lsr v0 1)) (S_syntax.lsr v0 3)).
Definition cost_N_IView : S.t := S.safe_int 1460.
Definition cost_N_IDrop : S.t := S.safe_int 10.
Definition cost_N_IDropN (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus
(S_syntax.op_plus
(S_syntax.op_plus (S.safe_int 30) (S_syntax.op_star (S.safe_int 2) v0))
(S_syntax.lsr v0 1)) (S_syntax.lsr v0 3).
Definition cost_N_IDug (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 35)
(S_syntax.op_plus
(S_syntax.op_plus (S_syntax.op_star (S.safe_int 6) v0)
(S_syntax.lsr v0 1)) (S_syntax.lsr v0 2)).
Definition cost_N_IDup : S.t := S.safe_int 10.
Definition cost_N_IDupN (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 20) v0) (S_syntax.lsr v0 3).
Definition cost_div_int (size1 : int) (size2 : int) : S.t :=
let q_value := size1 -i size2 in
if q_value <i 0 then
S.safe_int 105
else
let v0 := S_syntax.op_star (S.safe_int q_value) (S.safe_int size2) in
S_syntax.op_plus
(S_syntax.op_plus
(S_syntax.op_plus (S.safe_int 105) (S_syntax.lsr v0 10))
(S_syntax.lsr v0 11)) (S_syntax.lsr v0 13).
Definition cost_N_IEdiv_int : int → int → S.t := cost_div_int.
Definition cost_N_IEdiv_nat : int → int → S.t := cost_div_int.
Definition cost_N_IEdiv_tez : S.t := S.safe_int 80.
Definition cost_N_IEdiv_teznat : S.t := S.safe_int 70.
Definition cost_N_IEmpty_big_map : S.t := S.safe_int 10.
Definition cost_N_IEmpty_map : S.t := S.safe_int 220.
Definition cost_N_IEmpty_set : S.t := S.safe_int 220.
Definition cost_N_IEq : S.t := S.safe_int 10.
Definition cost_N_IExec : S.t := S.safe_int 10.
Definition cost_N_IGe : S.t := S.safe_int 10.
Definition cost_N_IGt : S.t := S.safe_int 10.
Definition cost_N_IHalt : S.t := S.safe_int 10.
Definition cost_N_IHash_key : S.t := S.safe_int 605.
Definition cost_N_IIf : S.t := S.safe_int 10.
Definition cost_N_IIf_cons : S.t := S.safe_int 10.
Definition cost_N_IIf_left : S.t := S.safe_int 10.
Definition cost_N_IIf_none : S.t := S.safe_int 10.
Definition cost_opt_map : S.t := S.safe_int 10.
Definition cost_N_IImplicit_account : S.t := S.safe_int 10.
Definition cost_N_IInt_bls12_381_z_fr : S.t := S.safe_int 115.
Definition cost_N_IInt_nat : S.t := S.safe_int 10.
Definition cost_N_IIs_nat : S.t := S.safe_int 10.
Definition cost_N_IKeccak (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 1350)
(S_syntax.op_plus (S_syntax.op_star (S.safe_int 8) v0)
(S_syntax.lsr v0 2)).
Definition cost_N_ILambda : S.t := S.safe_int 10.
Definition cost_N_ILe : S.t := S.safe_int 10.
Definition cost_N_ILeft : S.t := S.safe_int 10.
Definition cost_N_ILevel : S.t := S.safe_int 10.
Definition cost_N_IList_iter {A : Set} (function_parameter : A) : S.t :=
let '_ := function_parameter in
S.safe_int 20.
Definition cost_N_IList_map {A : Set} (function_parameter : A) : S.t :=
let '_ := function_parameter in
S.safe_int 20.
Definition cost_N_IList_size : S.t := S.safe_int 10.
Definition cost_N_ILoop : S.t := S.safe_int 10.
Definition cost_N_ILoop_left : S.t := S.safe_int 10.
Definition cost_N_ILsl_nat (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 40)
(S_syntax.op_plus
(S_syntax.op_plus (S_syntax.lsr v0 4) (S_syntax.lsr v0 5))
(S_syntax.lsr v0 6)).
Definition cost_N_ILsr_nat (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 45)
(S_syntax.op_plus
(S_syntax.op_plus (S_syntax.lsr v0 4) (S_syntax.lsr v0 5))
(S_syntax.lsr v0 6)).
Definition cost_N_ILt : S.t := S.safe_int 10.
Definition cost_N_IMap_get (size1 : S.t) (size2 : S.t) : S.t :=
let v0 := S_syntax.op_star size1 (S_syntax.log2 size2) in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 45) (S_syntax.lsr v0 5))
(S_syntax.lsr v0 6).
Definition cost_N_IMap_get_and_update (size1 : S.t) (size2 : S.t) : S.t :=
let v0 := S_syntax.op_star size1 (S_syntax.log2 size2) in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 75) (S_syntax.lsr v0 3))
(S_syntax.lsr v0 6).
Definition cost_N_IMap_iter (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus
(S_syntax.op_plus
(S_syntax.op_plus (S.safe_int 50) (S_syntax.op_star (S.safe_int 7) v0))
(S_syntax.lsr v0 1)) (S_syntax.lsr v0 3).
Definition cost_N_IMap_map (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 50)
(S_syntax.op_plus (S_syntax.op_star (S.safe_int 7) v0)
(S_syntax.lsr v0 1)).
Definition cost_N_IMap_mem (size1 : S.t) (size2 : S.t) : S.t :=
let v0 := S_syntax.op_star size1 (S_syntax.log2 size2) in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 45) (S_syntax.lsr v0 5))
(S_syntax.lsr v0 6).
Definition cost_N_IMap_size : S.t := S.safe_int 10.
Definition cost_N_IMap_update (size1 : S.t) (size2 : S.t) : S.t :=
let v0 := S_syntax.op_star size1 (S_syntax.log2 size2) in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 55) (S_syntax.lsr v0 4))
(S_syntax.lsr v0 5).
Definition cost_N_IMul_bls12_381_fr : S.t := S.safe_int 45.
Definition cost_N_IMul_bls12_381_fr_z (size1 : int) : S.t :=
let v0 := S.safe_int size1 in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 265) v0)
(S_syntax.lsr v0 4).
Definition cost_N_IMul_bls12_381_g1 : S.t := S.safe_int 103000.
Definition cost_N_IMul_bls12_381_g2 : S.t := S.safe_int 220000.
Definition cost_N_IMul_bls12_381_z_fr (size1 : int) : S.t :=
let v0 := S.safe_int size1 in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 265) v0)
(S_syntax.lsr v0 4).
Definition cost_mul (size1 : int) (size2 : int) : S.t :=
let a_value := S.add (S.safe_int size1) (S.safe_int size2) in
let v0 := S_syntax.op_star a_value (S_syntax.log2 a_value) in
S_syntax.op_plus
(S_syntax.op_plus (S_syntax.op_plus (S.safe_int 55) (S_syntax.lsr v0 1))
(S_syntax.lsr v0 2)) (S_syntax.lsr v0 4).
Definition cost_N_IMul_int : int → int → S.t := cost_mul.
Definition cost_N_IMul_nat : int → int → S.t := cost_mul.
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_INeg_bls12_381_fr : S.t := S.safe_int 25.
Definition cost_N_INeg_bls12_381_g1 : S.t := S.safe_int 50.
Definition cost_N_INeg_bls12_381_g2 : S.t := S.safe_int 70.
Definition cost_N_INeg (size_value : int) : S.t :=
S_syntax.op_plus (S.safe_int 25) (S_syntax.lsr (S.safe_int size_value) 4).
Definition cost_N_INeq : S.t := S.safe_int 10.
Definition cost_N_INil : S.t := S.safe_int 10.
Definition cost_N_INot : S.t := S.safe_int 10.
Definition cost_N_INot_int (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 25)
(S_syntax.op_plus (S_syntax.lsr v0 4) (S_syntax.lsr v0 7)).
Definition cost_N_INow : S.t := S.safe_int 10.
Definition cost_N_IMin_block_time : S.t := S.safe_int 20.
Definition cost_N_IOpen_chest (chest_value : int) (time : int) : S.t :=
let v0 := S.safe_int chest_value in
let v1 := S.safe_int time in
S_syntax.op_plus
(S_syntax.op_plus (S.safe_int 612000)
(S_syntax.op_star (S.safe_int 19) v0))
(S_syntax.op_star (S.safe_int 19050) v1).
Definition cost_N_IOr : S.t := S.safe_int 10.
Definition cost_N_IOr_nat : int → int → S.t := cost_linear_op_int.
Definition cost_N_IPairing_check_bls12_381 (size_value : int) : S.t :=
S.add (S.safe_int 450000)
(S.mul (S.safe_int 342500) (S.safe_int size_value)).
Definition cost_N_IRead_ticket : S.t := S.safe_int 10.
Definition cost_N_IRight : S.t := S.safe_int 10.
Definition cost_N_ISapling_empty_state : S.t := S.safe_int 10.
Definition cost_N_ISapling_verify_update
(size1 : int) (size2 : int) (bound_data : int) : S.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_ISelf_address : S.t := S.safe_int 10.
Definition cost_N_ISelf : S.t := S.safe_int 10.
Definition cost_N_ISender : S.t := S.safe_int 10.
Definition cost_N_ISet_delegate : S.t := S.safe_int 30.
Definition cost_N_ISet_iter (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus
(S_syntax.op_plus
(S_syntax.op_plus (S.safe_int 50) (S_syntax.op_star (S.safe_int 7) v0))
(S_syntax.lsr v0 1)) (S_syntax.lsr v0 3).
Definition cost_N_ISet_size : S.t := S.safe_int 10.
Definition cost_N_ISha256 (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 600)
(S_syntax.op_plus
(S_syntax.op_plus (S_syntax.op_star (S.safe_int 4) v0)
(S_syntax.lsr v0 1)) (S_syntax.lsr v0 2)).
Definition cost_N_ISha3 : int → S.t := cost_N_IKeccak.
Definition cost_N_ISha512 (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 680) (S_syntax.op_star (S.safe_int 3) v0).
Definition cost_N_ISlice_bytes (size_value : int) : S.t :=
S_syntax.op_plus (S.safe_int 25) (S_syntax.lsr (S.safe_int size_value) 4).
Definition cost_N_ISlice_string (size_value : int) : S.t :=
S_syntax.op_plus (S.safe_int 25) (S_syntax.lsr (S.safe_int size_value) 4).
Definition cost_N_ISource : S.t := S.safe_int 10.
Definition cost_N_ISplit_ticket (size1 : int) (size2 : int) : S.t :=
let v1 := S.safe_int (Compare.Int.max size1 size2) in
S_syntax.op_plus (S.safe_int 40) (S_syntax.lsr v1 3).
Definition cost_N_IString_size : S.t := S.safe_int 15.
Definition cost_N_ISub_int : int → int → S.t := cost_linear_op_int.
Definition cost_N_ISub_tez : S.t := S.safe_int 15.
Definition cost_N_ISub_tez_legacy : S.t := S.safe_int 20.
Definition cost_N_ISub_timestamp_seconds : int → int → S.t :=
cost_linear_op_int.
Definition cost_N_ISwap : S.t := S.safe_int 10.
Definition cost_N_ITicket : S.t := S.safe_int 10.
Definition cost_N_ITotal_voting_power : S.t := S.safe_int 370.
Definition cost_N_ITransfer_tokens : S.t := S.safe_int 30.
Definition cost_N_IUncomb (size_value : int) : S.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 25) (S_syntax.op_star (S.safe_int 4) v0).
Definition cost_N_IUnpair : S.t := S.safe_int 10.
Definition cost_N_IVoting_power : S.t := S.safe_int 530.
Definition cost_N_IXor : S.t := S.safe_int 15.
Definition cost_N_IXor_nat : int → int → S.t := cost_linear_op_int.
Definition cost_N_KCons : S.t := S.safe_int 10.
Definition cost_N_KIter : S.t := S.safe_int 10.
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_N_KList_exit_body : S.t := S.safe_int 10.
Definition cost_N_KLoop_in : S.t := S.safe_int 10.
Definition cost_N_KLoop_in_left : S.t := S.safe_int 10.
Definition cost_N_KMap_enter_body : S.t := S.safe_int 80.
Definition cost_N_KNil : S.t := S.safe_int 10.
Definition cost_N_KReturn : S.t := S.safe_int 10.
Definition cost_N_KView_exit : S.t := S.safe_int 20.
Definition cost_N_KMap_head : S.t := S.safe_int 20.
Definition cost_N_KUndip : S.t := S.safe_int 10.
Definition cost_DECODING_BLS_FR : S.t := S.safe_int 120.
Definition cost_DECODING_BLS_G1 : S.t := S.safe_int 54600.
Definition cost_DECODING_BLS_G2 : S.t := S.safe_int 69000.
Definition cost_B58CHECK_DECODING_CHAIN_ID : S.t := S.safe_int 1600.
Definition cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_ed25519 : S.t :=
S.safe_int 3300.
Definition cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_p256 : S.t :=
S.safe_int 3300.
Definition cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_secp256k1 : S.t :=
S.safe_int 3300.
Definition cost_B58CHECK_DECODING_PUBLIC_KEY_ed25519 : S.t :=
S.safe_int 4200.
Definition cost_B58CHECK_DECODING_PUBLIC_KEY_p256 : S.t :=
S.safe_int 325000.
Definition cost_B58CHECK_DECODING_PUBLIC_KEY_secp256k1 : S.t :=
S.safe_int 9000.
Definition cost_B58CHECK_DECODING_SIGNATURE_ed25519 : S.t :=
S.safe_int 6400.
Definition cost_B58CHECK_DECODING_SIGNATURE_p256 : S.t := S.safe_int 6400.
Definition cost_B58CHECK_DECODING_SIGNATURE_secp256k1 : S.t :=
S.safe_int 6400.
Definition cost_ENCODING_BLS_FR : S.t := S.safe_int 80.
Definition cost_ENCODING_BLS_G1 : S.t := S.safe_int 3200.
Definition cost_ENCODING_BLS_G2 : S.t := S.safe_int 3900.
Definition cost_B58CHECK_ENCODING_CHAIN_ID : S.t := S.safe_int 1800.
Definition cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_ed25519 : S.t :=
S.safe_int 3200.
Definition cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_p256 : S.t :=
S.safe_int 3200.
Definition cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_secp256k1 : S.t :=
S.safe_int 3200.
Definition cost_B58CHECK_ENCODING_PUBLIC_KEY_ed25519 : S.t :=
S.safe_int 4500.
Definition cost_B58CHECK_ENCODING_PUBLIC_KEY_p256 : S.t := S.safe_int 4550.
Definition cost_B58CHECK_ENCODING_PUBLIC_KEY_secp256k1 : S.t :=
S.safe_int 4950.
Definition cost_B58CHECK_ENCODING_SIGNATURE_ed25519 : S.t :=
S.safe_int 8300.
Definition cost_B58CHECK_ENCODING_SIGNATURE_p256 : S.t := S.safe_int 8300.
Definition cost_B58CHECK_ENCODING_SIGNATURE_secp256k1 : S.t :=
S.safe_int 8300.
Definition cost_DECODING_CHAIN_ID : S.t := S.safe_int 50.
Definition cost_DECODING_PUBLIC_KEY_HASH_ed25519 : S.t := S.safe_int 50.
Definition cost_DECODING_PUBLIC_KEY_HASH_p256 : S.t := S.safe_int 50.
Definition cost_DECODING_PUBLIC_KEY_HASH_secp256k1 : S.t := S.safe_int 50.
Definition cost_DECODING_PUBLIC_KEY_ed25519 : S.t := S.safe_int 60.
Definition cost_DECODING_PUBLIC_KEY_p256 : S.t := S.safe_int 320000.
Definition cost_DECODING_PUBLIC_KEY_secp256k1 : S.t := S.safe_int 4900.
Definition cost_DECODING_SIGNATURE_ed25519 : S.t := S.safe_int 35.
Definition cost_DECODING_SIGNATURE_p256 : S.t := S.safe_int 35.
Definition cost_DECODING_SIGNATURE_secp256k1 : S.t := S.safe_int 35.
Definition cost_DECODING_Chest_key : S.t := S.safe_int 5900.
Definition cost_DECODING_Chest (bytes_value : int) : S.t :=
let v0 := S.safe_int bytes_value in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 7400) (S_syntax.lsr v0 5))
(S_syntax.lsr v0 7).
Definition cost_ENCODING_CHAIN_ID : S.t := S.safe_int 50.
Definition cost_ENCODING_PUBLIC_KEY_HASH_ed25519 : S.t := S.safe_int 70.
Definition cost_ENCODING_PUBLIC_KEY_HASH_p256 : S.t := S.safe_int 70.
Definition cost_ENCODING_PUBLIC_KEY_HASH_secp256k1 : S.t := S.safe_int 70.
Definition cost_ENCODING_PUBLIC_KEY_ed25519 : S.t := S.safe_int 80.
Definition cost_ENCODING_PUBLIC_KEY_p256 : S.t := S.safe_int 90.
Definition cost_ENCODING_PUBLIC_KEY_secp256k1 : S.t := S.safe_int 455.
Definition cost_ENCODING_SIGNATURE_ed25519 : S.t := S.safe_int 45.
Definition cost_ENCODING_SIGNATURE_p256 : S.t := S.safe_int 45.
Definition cost_ENCODING_SIGNATURE_secp256k1 : S.t := S.safe_int 45.
Definition cost_ENCODING_Chest_key : S.t := S.safe_int 13500.
Definition cost_ENCODING_Chest (plaintext_size : int) : S.t :=
let v0 := S.safe_int plaintext_size in
S_syntax.op_plus (S.safe_int 16630) (S_syntax.lsr v0 3).
Definition cost_TIMESTAMP_READABLE_DECODING (bytes_value : int) : S.t :=
let b_value := S.safe_int bytes_value in
let v0 := S.mul (S.sqrt b_value) b_value in
S_syntax.op_plus (S.safe_int 800)
(S_syntax.op_plus (S_syntax.lsr v0 2) (S_syntax.lsr v0 3)).
Definition cost_TIMESTAMP_READABLE_ENCODING : S.t := S.safe_int 100.
Definition cost_CHECK_PRINTABLE (size_value : int) : S.t :=
S_syntax.op_plus (S.safe_int 14)
(S_syntax.op_star (S.safe_int 10) (S.safe_int size_value)).
Definition cost_TY_EQ : S.t := S.safe_int 60.
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 45.
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_UNPARSE_COMPARABLE_TYPE (type_size : S.t) : S.t :=
S.mul (S.safe_int 20) type_size.
Definition cost_COMPARABLE_TY_OF_TY : S.t := S.safe_int 120.
Definition cost_FIND_ENTRYPOINT : S.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)).
End Generated_costs.
Module Interpreter.
Definition drop : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IDrop.
Definition dup : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IDup.
Definition swap : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISwap.
Definition cons_some : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ICons_some.
Definition cons_none : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ICons_none.
Definition if_none : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IIf_none.
Definition opt_map : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_opt_map.
Definition cons_pair : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ICons_pair.
Definition unpair : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IUnpair.
Definition car : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ICar.
Definition cdr : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ICdr.
Definition cons_left : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ILeft.
Definition cons_right : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IRight.
Definition if_left : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IIf_left.
Definition cons_list : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ICons_list.
Definition nil : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_INil.
Definition if_cons : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IIf_cons.
Definition list_map {a : Set}
(function_parameter : Script_typed_ir.boxed_list a)
: Alpha_context.Gas.cost :=
let '{| Script_typed_ir.boxed_list.length := length |} :=
function_parameter in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IList_map length).
Definition list_size : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IList_size.
Definition list_iter {a : Set}
(function_parameter : Script_typed_ir.boxed_list a)
: Alpha_context.Gas.cost :=
let '{| Script_typed_ir.boxed_list.length := length |} :=
function_parameter in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IList_iter length).
Definition empty_set : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IEmpty_set.
Definition set_iter {a : Set} (set : Script_typed_ir.set a)
: Alpha_context.Gas.cost :=
let Box := Script_set.get set in
let 'existS _ _ Box := Box in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISet_iter
Box.(Script_typed_ir.Boxed_set.size_value)).
Definition set_size : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISet_size.
Definition empty_map : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IEmpty_map.
Definition map_map {k v : Set} (map : Script_typed_ir.map k v)
: Alpha_context.Gas.cost :=
let Box := Script_map.get_module map in
let 'existS _ _ Box := Box in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMap_map
Box.(Script_typed_ir.Boxed_map.size_value)).
Definition map_iter {k v : Set} (map : Script_typed_ir.map k v)
: Alpha_context.Gas.cost :=
let Box := Script_map.get_module map in
let 'existS _ _ Box := Box in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMap_iter
Box.(Script_typed_ir.Boxed_map.size_value)).
Definition map_size : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IMap_size.
Definition big_map_elt_size : S.t := S.safe_int Script_expr_hash.size_value.
Definition big_map_mem {A B : Set}
(function_parameter : Script_typed_ir.big_map_overlay A B)
: Alpha_context.Gas.cost :=
let '{| Script_typed_ir.big_map_overlay.size := size_value |} :=
function_parameter in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMap_mem big_map_elt_size
(S.safe_int size_value)).
Definition big_map_get {A B : Set}
(function_parameter : Script_typed_ir.big_map_overlay A B)
: Alpha_context.Gas.cost :=
let '{| Script_typed_ir.big_map_overlay.size := size_value |} :=
function_parameter in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMap_get big_map_elt_size
(S.safe_int size_value)).
Definition big_map_update {A B : Set}
(function_parameter : Script_typed_ir.big_map_overlay A B)
: Alpha_context.Gas.cost :=
let '{| Script_typed_ir.big_map_overlay.size := size_value |} :=
function_parameter in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMap_update big_map_elt_size
(S.safe_int size_value)).
Definition big_map_get_and_update {A B : Set}
(function_parameter : Script_typed_ir.big_map_overlay A B)
: Alpha_context.Gas.cost :=
let '{| Script_typed_ir.big_map_overlay.size := size_value |} :=
function_parameter in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMap_get_and_update big_map_elt_size
(S.safe_int size_value)).
Definition add_seconds_timestamp
(seconds : Alpha_context.Script_int.num)
(timestamp : Alpha_context.Script_timestamp.t) : Alpha_context.Gas.cost :=
let seconds_bytes := int_bytes seconds in
let timestamp_bytes :=
z_bytes (Alpha_context.Script_timestamp.to_zint timestamp) in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IAdd_seconds_to_timestamp seconds_bytes
timestamp_bytes).
Definition add_timestamp_seconds
(timestamp : Alpha_context.Script_timestamp.t)
(seconds : Alpha_context.Script_int.num) : Alpha_context.Gas.cost :=
let seconds_bytes := int_bytes seconds in
let timestamp_bytes :=
z_bytes (Alpha_context.Script_timestamp.to_zint timestamp) in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IAdd_timestamp_to_seconds timestamp_bytes
seconds_bytes).
Definition sub_timestamp_seconds
(timestamp : Alpha_context.Script_timestamp.t)
(seconds : Alpha_context.Script_int.num) : Alpha_context.Gas.cost :=
let seconds_bytes := int_bytes seconds in
let timestamp_bytes :=
z_bytes (Alpha_context.Script_timestamp.to_zint timestamp) in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISub_timestamp_seconds timestamp_bytes
seconds_bytes).
Definition diff_timestamps
(t1 : Alpha_context.Script_timestamp.t)
(t2 : Alpha_context.Script_timestamp.t) : Alpha_context.Gas.cost :=
let t1_bytes := z_bytes (Alpha_context.Script_timestamp.to_zint t1) in
let t2_bytes := z_bytes (Alpha_context.Script_timestamp.to_zint t2) in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IDiff_timestamps t1_bytes t2_bytes).
Definition concat_string_pair
(s1 : Alpha_context.Script_string.t) (s2 : Alpha_context.Script_string.t)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IConcat_string_pair
(Alpha_context.Script_string.length s1)
(Alpha_context.Script_string.length s2)).
Definition slice_string (s_value : Alpha_context.Script_string.t)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISlice_string
(Alpha_context.Script_string.length s_value)).
Definition string_size : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IString_size.
Definition concat_bytes_pair (b1 : bytes) (b2 : bytes)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IConcat_bytes_pair (Bytes.length b1)
(Bytes.length b2)).
Definition slice_bytes (b_value : bytes) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISlice_bytes (Bytes.length b_value)).
Definition bytes_size : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IBytes_size.
Definition add_tez : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IAdd_tez.
Definition sub_tez : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISub_tez.
Definition sub_tez_legacy : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISub_tez_legacy.
Definition mul_teznat : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IMul_teznat.
Definition mul_nattez : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IMul_nattez.
Definition bool_or : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IOr.
Definition bool_and : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IAnd.
Definition bool_xor : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IXor.
Definition bool_not : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_INot.
Definition is_nat : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IIs_nat.
Definition abs_int (i_value : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IAbs_int (int_bytes i_value)).
Definition int_nat : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IInt_nat.
Definition neg (i_value : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_INeg (int_bytes i_value)).
Definition add_int
(i1 : Alpha_context.Script_int.num) (i2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IAdd_int (int_bytes i1) (int_bytes i2)).
Definition add_nat
(i1 : Alpha_context.Script_int.num) (i2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IAdd_nat (int_bytes i1) (int_bytes i2)).
Definition sub_int
(i1 : Alpha_context.Script_int.num) (i2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISub_int (int_bytes i1) (int_bytes i2)).
Definition mul_int
(i1 : Alpha_context.Script_int.num) (i2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMul_int (int_bytes i1) (int_bytes i2)).
Definition mul_nat
(i1 : Alpha_context.Script_int.num) (i2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMul_nat (int_bytes i1) (int_bytes i2)).
Definition ediv_teznat {A B : Set} (_tez : A) (_n : B)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IEdiv_teznat.
Definition ediv_tez : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IEdiv_tez.
Definition ediv_int
(i1 : Alpha_context.Script_int.num) (i2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IEdiv_int (int_bytes i1) (int_bytes i2)).
Definition ediv_nat
(i1 : Alpha_context.Script_int.num) (i2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IEdiv_nat (int_bytes i1) (int_bytes i2)).
Definition eq_value : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IEq.
Definition lsl_nat (shifted : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ILsl_nat (int_bytes shifted)).
Definition lsr_nat (shifted : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ILsr_nat (int_bytes shifted)).
Definition or_nat
(n1 : Alpha_context.Script_int.num) (n2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IOr_nat (int_bytes n1) (int_bytes n2)).
Definition and_nat
(n1 : Alpha_context.Script_int.num) (n2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IAnd_nat (int_bytes n1) (int_bytes n2)).
Definition and_int_nat
(n1 : Alpha_context.Script_int.num) (n2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IAnd_int_nat (int_bytes n1) (int_bytes n2)).
Definition xor_nat
(n1 : Alpha_context.Script_int.num) (n2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IXor_nat (int_bytes n1) (int_bytes n2)).
Definition not_int (i_value : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_INot_int (int_bytes i_value)).
Definition if_ : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IIf.
Definition loop : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ILoop.
Definition loop_left : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ILoop_left.
Definition dip : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IDip.
Definition view : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IView.
Definition check_signature (pkey : Signature.public_key) (b_value : bytes)
: Alpha_context.Gas.cost :=
let cost :=
match pkey with
| Signature.Ed25519 _ ⇒
Generated_costs.cost_N_ICheck_signature_ed25519 (Bytes.length b_value)
| Signature.Secp256k1 _ ⇒
Generated_costs.cost_N_ICheck_signature_secp256k1
(Bytes.length b_value)
| Signature.P256 _ ⇒
Generated_costs.cost_N_ICheck_signature_p256 (Bytes.length b_value)
end in
Alpha_context.Gas.atomic_step_cost cost.
Definition blake2b (b_value : bytes) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IBlake2b (Bytes.length b_value)).
Definition sha256 (b_value : bytes) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISha256 (Bytes.length b_value)).
Definition sha512 (b_value : bytes) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISha512 (Bytes.length b_value)).
Definition dign (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_IDig n_value).
Definition dugn (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_IDug n_value).
Definition dipn (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_IDipN n_value).
Definition dropn (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_IDropN n_value).
Definition voting_power : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IVoting_power.
Definition total_voting_power : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_ITotal_voting_power.
Definition keccak (b_value : bytes) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IKeccak (Bytes.length b_value)).
Definition sha3 (b_value : bytes) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISha3 (Bytes.length b_value)).
Definition add_bls12_381_g1 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_IAdd_bls12_381_g1.
Definition add_bls12_381_g2 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_IAdd_bls12_381_g2.
Definition add_bls12_381_fr : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_IAdd_bls12_381_fr.
Definition mul_bls12_381_g1 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_IMul_bls12_381_g1.
Definition mul_bls12_381_g2 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_IMul_bls12_381_g2.
Definition mul_bls12_381_fr : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_IMul_bls12_381_fr.
Definition mul_bls12_381_fr_z (z_value : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMul_bls12_381_fr_z (int_bytes z_value)).
Definition mul_bls12_381_z_fr (z_value : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IMul_bls12_381_z_fr (int_bytes z_value)).
Definition int_bls12_381_fr : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_IInt_bls12_381_z_fr.
Definition neg_bls12_381_g1 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_INeg_bls12_381_g1.
Definition neg_bls12_381_g2 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_INeg_bls12_381_g2.
Definition neg_bls12_381_fr : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_INeg_bls12_381_fr.
Definition neq : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_INeq.
Definition pairing_check_bls12_381 {a : Set}
(l_value : Script_typed_ir.boxed_list a) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IPairing_check_bls12_381
l_value.(Script_typed_ir.boxed_list.length)).
Definition comb (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_IComb n_value).
Definition uncomb (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IUncomb n_value).
Definition comb_get (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IComb_get n_value).
Definition comb_set (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IComb_set n_value).
Definition dupn (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_IDupN n_value).
Definition sapling_verify_update
(inputs : int) (outputs : int) (bound_data : int)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISapling_verify_update inputs outputs bound_data).
Definition sapling_verify_update_deprecated (inputs : int) (outputs : int)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISapling_verify_update inputs outputs 0).
Definition sapling_empty_state : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_ISapling_empty_state.
Definition halt : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IHalt.
Definition const : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IConst.
Definition empty_big_map : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IEmpty_big_map.
Definition lt : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ILt.
Definition le : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ILe.
Definition gt : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IGt.
Definition ge : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IGe.
Definition exec : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IExec.
Definition apply : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IApply.
Definition lambda : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ILambda.
Definition address : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IAddress.
Definition contract : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IContract.
Definition transfer_tokens : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ITransfer_tokens.
Definition implicit_account : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_IImplicit_account.
Definition create_contract : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ICreate_contract.
Definition set_delegate : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISet_delegate.
Definition level : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ILevel.
Definition now : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_INow.
Definition min_block_time : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IMin_block_time.
Definition source : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISource.
Definition sender : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISender.
Definition self : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISelf.
Definition self_address : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ISelf_address.
Definition amount : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IAmount.
Definition chain_id : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IChainId.
Definition ticket : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_ITicket.
Definition read_ticket : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IRead_ticket.
Definition hash_key {A : Set} (function_parameter : A)
: Alpha_context.Gas.cost :=
let '_ := function_parameter in
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_IHash_key.
Definition split_ticket {A : Set} (function_parameter : A)
: Alpha_context.Script_int.num → Alpha_context.Script_int.num →
Alpha_context.Gas.cost :=
let '_ := function_parameter in
fun (amount_a : Alpha_context.Script_int.num) ⇒
fun (amount_b : Alpha_context.Script_int.num) ⇒
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ISplit_ticket (int_bytes amount_a)
(int_bytes amount_b)).
Definition open_chest
(chest_value : Script_typed_ir.Script_timelock.chest) (time : Z.t)
: Alpha_context.Gas.cost :=
let plaintext :=
Script_typed_ir.Script_timelock.get_plaintext_size chest_value in
let log_time := Z.log2 (Z.one +Z time) in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_IOpen_chest plaintext log_time).
Definition compare_unit : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (S.safe_int 10).
Definition compare_pair_tag : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (S.safe_int 10).
Definition compare_union_tag : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (S.safe_int 10).
Definition compare_option_tag : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (S.safe_int 10).
Definition compare_bool : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_ICompare 1 1).
Definition compare_signature : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (S.safe_int 92).
Definition compare_string
(s1 : Alpha_context.Script_string.t) (s2 : Alpha_context.Script_string.t)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ICompare (Alpha_context.Script_string.length s1)
(Alpha_context.Script_string.length s2)).
Definition compare_bytes (b1 : bytes) (b2 : bytes)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ICompare (Bytes.length b1) (Bytes.length b2)).
Definition compare_mutez : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_ICompare 8 8).
Definition compare_int
(i1 : Alpha_context.Script_int.num) (i2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ICompare (int_bytes i1) (int_bytes i2)).
Definition compare_nat
(n1 : Alpha_context.Script_int.num) (n2 : Alpha_context.Script_int.num)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ICompare (int_bytes n1) (int_bytes n2)).
Definition compare_key_hash : Alpha_context.Gas.cost :=
let sz :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value) in
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_ICompare sz sz).
Definition compare_key : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (S.safe_int 92).
Definition compare_timestamp
(t1 : Alpha_context.Script_timestamp.t)
(t2 : Alpha_context.Script_timestamp.t) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_ICompare
(z_bytes (Alpha_context.Script_timestamp.to_zint t1))
(z_bytes (Alpha_context.Script_timestamp.to_zint t2))).
Definition entrypoint_size : int := 31.
Definition compare_address : Alpha_context.Gas.cost :=
let sz :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value) +i
entrypoint_size in
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_ICompare sz sz).
TODO: https://gitlab.com/tezos/tezos/-/issues/2340
Refine the gas model
Definition compare_tx_rollup_l2_address : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_ICompare 48 48).
Definition compare_chain_id : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (S.safe_int 30).
Inductive cont : Set :=
| Compare : ∀ {a : Set},
Script_typed_ir.comparable_ty → a → a → cont → cont
| Return : cont.
Axiom compare : ∀ {a : Set},
Script_typed_ir.comparable_ty → a → a → Alpha_context.Gas.cost.
Definition set_mem {a : Set} (elt_value : a) (set : Script_typed_ir.set a)
: Alpha_context.Gas.cost :=
let Box := Script_set.get set in
let 'existS _ _ Box := Box in
let per_elt_cost :=
S.safe_int
(Size.to_int
(Box.(Script_typed_ir.Boxed_set.OPS).(Script_typed_ir.Boxed_set_OPS.elt_size)
elt_value)) in
let size_value := S.safe_int Box.(Script_typed_ir.Boxed_set.size_value) in
let intercept := Alpha_context.Gas.atomic_step_cost (S.safe_int 115) in
Alpha_context.Gas.op_plusat intercept
(Alpha_context.Gas.op_starat (S_syntax.log2 size_value) per_elt_cost).
Definition set_update {a : Set}
(elt_value : a) (set : Script_typed_ir.set a) : Alpha_context.Gas.cost :=
let Box := Script_set.get set in
let 'existS _ _ Box := Box in
let per_elt_cost :=
S.safe_int
(Size.to_int
(Box.(Script_typed_ir.Boxed_set.OPS).(Script_typed_ir.Boxed_set_OPS.elt_size)
elt_value)) in
let size_value := S.safe_int Box.(Script_typed_ir.Boxed_set.size_value) in
let intercept := Alpha_context.Gas.atomic_step_cost (S.safe_int 130) in
Alpha_context.Gas.op_plusat intercept
(Alpha_context.Gas.op_starat
(S_syntax.op_star (S.safe_int 2) (S_syntax.log2 size_value))
per_elt_cost).
Definition map_mem {k v : Set}
(elt_value : k) (map : Script_typed_ir.map k v)
: Alpha_context.Gas.cost :=
let Box := Script_map.get_module map in
let 'existS _ _ Box := Box in
let per_elt_cost :=
S.safe_int
(Size.to_int
(Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.key_size)
elt_value)) in
let size_value := S.safe_int Box.(Script_typed_ir.Boxed_map.size_value) in
let intercept := Alpha_context.Gas.atomic_step_cost (S.safe_int 80) in
Alpha_context.Gas.op_plusat intercept
(Alpha_context.Gas.op_starat (S_syntax.log2 size_value) per_elt_cost).
Definition map_get {A B : Set}
: A → Script_typed_ir.map A B → Alpha_context.Gas.cost := map_mem.
Definition map_update {k v : Set}
(elt_value : k) (map : Script_typed_ir.map k v)
: Alpha_context.Gas.cost :=
let Box := Script_map.get_module map in
let 'existS _ _ Box := Box in
let per_elt_cost :=
S.safe_int
(Size.to_int
(Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.key_size)
elt_value)) in
let size_value := S.safe_int Box.(Script_typed_ir.Boxed_map.size_value) in
let intercept := Alpha_context.Gas.atomic_step_cost (S.safe_int 80) in
Alpha_context.Gas.op_plusat intercept
(Alpha_context.Gas.op_starat
(S_syntax.op_star (S.safe_int 2) (S_syntax.log2 size_value))
per_elt_cost).
Definition map_get_and_update {k v : Set}
(elt_value : k) (map : Script_typed_ir.map k v)
: Alpha_context.Gas.cost :=
let Box := Script_map.get_module map in
let 'existS _ _ Box := Box in
let per_elt_cost :=
S.safe_int
(Size.to_int
(Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.key_size)
elt_value)) in
let size_value := S.safe_int Box.(Script_typed_ir.Boxed_map.size_value) in
let intercept := Alpha_context.Gas.atomic_step_cost (S.safe_int 80) in
Alpha_context.Gas.op_plusat intercept
(Alpha_context.Gas.op_starat
(S_syntax.op_star (S.safe_int 3) (S_syntax.log2 size_value))
per_elt_cost).
Definition view_get
(elt_value : Alpha_context.Script_string.t)
(m_value : Script_typed_ir.view_map) : Alpha_context.Gas.cost :=
map_get elt_value m_value.
Definition view_update
(elt_value : Alpha_context.Script_string.t)
(m_value : Script_typed_ir.view_map) : Alpha_context.Gas.cost :=
map_update elt_value m_value.
Definition join_tickets {a : Set}
(ty : Script_typed_ir.comparable_ty) (ticket_a : Script_typed_ir.ticket a)
(ticket_b : Script_typed_ir.ticket a) : Alpha_context.Gas.cost :=
let contents_comparison :=
compare ty ticket_a.(Script_typed_ir.ticket.contents)
ticket_b.(Script_typed_ir.ticket.contents) in
Alpha_context.Gas.op_plusat
(Alpha_context.Gas.op_plusat contents_comparison compare_address)
(add_nat ticket_a.(Script_typed_ir.ticket.amount)
ticket_b.(Script_typed_ir.ticket.amount)).
Module Control.
Definition nil : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KNil.
Definition cons_value : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KCons.
Definition _return : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KReturn.
Definition view_exit : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KView_exit.
Definition map_head : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KMap_head.
Definition undip : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KUndip.
Definition loop_in : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KLoop_in.
Definition loop_in_left : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KLoop_in_left.
Definition iter : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KIter.
Definition list_enter_body {A : Set} (xs : list A) (ys_len : int)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_KList_enter_body xs ys_len).
Definition list_exit_body : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_KList_exit_body.
Definition map_enter_body : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_KMap_enter_body.
Definition map_exit_body {k v : Set}
(key_value : k) (map : Script_typed_ir.map k v)
: Alpha_context.Gas.cost := map_update key_value map.
End Control.
Definition concat_string_precheck {a : Set}
(l_value : Script_typed_ir.boxed_list a) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.mul (S.safe_int l_value.(Script_typed_ir.boxed_list.length))
(S.safe_int 10)).
Definition concat_string (total_bytes : S.t) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.add (S.safe_int 100) (S.ediv total_bytes (S.safe_int 10))).
Definition concat_bytes (total_bytes : S.t) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.add (S.safe_int 100) (S.ediv total_bytes (S.safe_int 10))).
Definition balance : Alpha_context.Gas.cost := Alpha_context.Gas.free.
Definition unpack (bytes_value : bytes) : Alpha_context.Gas.cost :=
let blen := Bytes.length bytes_value in
Alpha_context.Gas.atomic_step_cost
(S_syntax.op_plus (S.safe_int 260) (S_syntax.lsr (S.safe_int blen) 3)).
Definition unpack_failed (bytes_value : string) : Alpha_context.Gas.cost :=
let blen := String.length bytes_value in
let len := S.safe_int blen in
let d_value := Z.numbits (Z.of_int blen) in
Alpha_context.Gas.op_plusat
(Alpha_context.Gas.op_starat len (Alpha_context.Gas.alloc_mbytes_cost 1))
(Alpha_context.Gas.op_starat len
(Alpha_context.Gas.op_starat (S.safe_int d_value)
(Alpha_context.Gas.op_plusat
(Alpha_context.Gas.alloc_cost (S.safe_int 3))
(Alpha_context.Gas.step_cost S.one)))).
End Interpreter.
Module Typechecking.
Definition public_key_optimized : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_DECODING_PUBLIC_KEY_ed25519
(S.max Generated_costs.cost_DECODING_PUBLIC_KEY_secp256k1
Generated_costs.cost_DECODING_PUBLIC_KEY_p256)).
Definition public_key_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_ed25519
(S.max Generated_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_secp256k1
Generated_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_p256)).
Definition key_hash_optimized : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_DECODING_PUBLIC_KEY_HASH_ed25519
(S.max Generated_costs.cost_DECODING_PUBLIC_KEY_HASH_secp256k1
Generated_costs.cost_DECODING_PUBLIC_KEY_HASH_p256)).
Definition key_hash_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_ed25519
(S.max
Generated_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_secp256k1
Generated_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_p256)).
Definition signature_optimized : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_DECODING_SIGNATURE_ed25519
(S.max Generated_costs.cost_DECODING_SIGNATURE_secp256k1
Generated_costs.cost_DECODING_SIGNATURE_p256)).
Definition signature_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_B58CHECK_DECODING_SIGNATURE_ed25519
(S.max Generated_costs.cost_B58CHECK_DECODING_SIGNATURE_secp256k1
Generated_costs.cost_B58CHECK_DECODING_SIGNATURE_p256)).
Definition chain_id_optimized : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_DECODING_CHAIN_ID.
Definition chain_id_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_B58CHECK_DECODING_CHAIN_ID.
Definition address_optimized : Alpha_context.Gas.cost := key_hash_optimized.
Definition contract_optimized : Alpha_context.Gas.cost :=
key_hash_optimized.
Definition contract_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.op_starat (S.safe_int 2) key_hash_readable.
Definition bls12_381_g1 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_DECODING_BLS_G1.
Definition bls12_381_g2 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_DECODING_BLS_G2.
Definition bls12_381_fr : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_DECODING_BLS_FR.
Definition check_printable (s_value : string) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_CHECK_PRINTABLE (String.length s_value)).
Definition merge_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_TY_EQ.
Definition parse_type_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_PARSE_TYPE.
Definition parse_instr_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_TYPECHECKING_CODE.
Definition parse_data_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_TYPECHECKING_DATA.
Definition comparable_ty_of_ty_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_COMPARABLE_TY_OF_TY.
Definition check_dupable_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_TYPECHECKING_DATA.
Definition find_entrypoint_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_FIND_ENTRYPOINT.
Definition bool_value : Alpha_context.Gas.cost := Alpha_context.Gas.free.
Definition unit_value : Alpha_context.Gas.cost := Alpha_context.Gas.free.
Definition timestamp_readable (s_value : string) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_TIMESTAMP_READABLE_DECODING
(String.length s_value)).
Alpha_context.Gas.atomic_step_cost (Generated_costs.cost_N_ICompare 48 48).
Definition compare_chain_id : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost (S.safe_int 30).
Inductive cont : Set :=
| Compare : ∀ {a : Set},
Script_typed_ir.comparable_ty → a → a → cont → cont
| Return : cont.
Axiom compare : ∀ {a : Set},
Script_typed_ir.comparable_ty → a → a → Alpha_context.Gas.cost.
Definition set_mem {a : Set} (elt_value : a) (set : Script_typed_ir.set a)
: Alpha_context.Gas.cost :=
let Box := Script_set.get set in
let 'existS _ _ Box := Box in
let per_elt_cost :=
S.safe_int
(Size.to_int
(Box.(Script_typed_ir.Boxed_set.OPS).(Script_typed_ir.Boxed_set_OPS.elt_size)
elt_value)) in
let size_value := S.safe_int Box.(Script_typed_ir.Boxed_set.size_value) in
let intercept := Alpha_context.Gas.atomic_step_cost (S.safe_int 115) in
Alpha_context.Gas.op_plusat intercept
(Alpha_context.Gas.op_starat (S_syntax.log2 size_value) per_elt_cost).
Definition set_update {a : Set}
(elt_value : a) (set : Script_typed_ir.set a) : Alpha_context.Gas.cost :=
let Box := Script_set.get set in
let 'existS _ _ Box := Box in
let per_elt_cost :=
S.safe_int
(Size.to_int
(Box.(Script_typed_ir.Boxed_set.OPS).(Script_typed_ir.Boxed_set_OPS.elt_size)
elt_value)) in
let size_value := S.safe_int Box.(Script_typed_ir.Boxed_set.size_value) in
let intercept := Alpha_context.Gas.atomic_step_cost (S.safe_int 130) in
Alpha_context.Gas.op_plusat intercept
(Alpha_context.Gas.op_starat
(S_syntax.op_star (S.safe_int 2) (S_syntax.log2 size_value))
per_elt_cost).
Definition map_mem {k v : Set}
(elt_value : k) (map : Script_typed_ir.map k v)
: Alpha_context.Gas.cost :=
let Box := Script_map.get_module map in
let 'existS _ _ Box := Box in
let per_elt_cost :=
S.safe_int
(Size.to_int
(Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.key_size)
elt_value)) in
let size_value := S.safe_int Box.(Script_typed_ir.Boxed_map.size_value) in
let intercept := Alpha_context.Gas.atomic_step_cost (S.safe_int 80) in
Alpha_context.Gas.op_plusat intercept
(Alpha_context.Gas.op_starat (S_syntax.log2 size_value) per_elt_cost).
Definition map_get {A B : Set}
: A → Script_typed_ir.map A B → Alpha_context.Gas.cost := map_mem.
Definition map_update {k v : Set}
(elt_value : k) (map : Script_typed_ir.map k v)
: Alpha_context.Gas.cost :=
let Box := Script_map.get_module map in
let 'existS _ _ Box := Box in
let per_elt_cost :=
S.safe_int
(Size.to_int
(Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.key_size)
elt_value)) in
let size_value := S.safe_int Box.(Script_typed_ir.Boxed_map.size_value) in
let intercept := Alpha_context.Gas.atomic_step_cost (S.safe_int 80) in
Alpha_context.Gas.op_plusat intercept
(Alpha_context.Gas.op_starat
(S_syntax.op_star (S.safe_int 2) (S_syntax.log2 size_value))
per_elt_cost).
Definition map_get_and_update {k v : Set}
(elt_value : k) (map : Script_typed_ir.map k v)
: Alpha_context.Gas.cost :=
let Box := Script_map.get_module map in
let 'existS _ _ Box := Box in
let per_elt_cost :=
S.safe_int
(Size.to_int
(Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.key_size)
elt_value)) in
let size_value := S.safe_int Box.(Script_typed_ir.Boxed_map.size_value) in
let intercept := Alpha_context.Gas.atomic_step_cost (S.safe_int 80) in
Alpha_context.Gas.op_plusat intercept
(Alpha_context.Gas.op_starat
(S_syntax.op_star (S.safe_int 3) (S_syntax.log2 size_value))
per_elt_cost).
Definition view_get
(elt_value : Alpha_context.Script_string.t)
(m_value : Script_typed_ir.view_map) : Alpha_context.Gas.cost :=
map_get elt_value m_value.
Definition view_update
(elt_value : Alpha_context.Script_string.t)
(m_value : Script_typed_ir.view_map) : Alpha_context.Gas.cost :=
map_update elt_value m_value.
Definition join_tickets {a : Set}
(ty : Script_typed_ir.comparable_ty) (ticket_a : Script_typed_ir.ticket a)
(ticket_b : Script_typed_ir.ticket a) : Alpha_context.Gas.cost :=
let contents_comparison :=
compare ty ticket_a.(Script_typed_ir.ticket.contents)
ticket_b.(Script_typed_ir.ticket.contents) in
Alpha_context.Gas.op_plusat
(Alpha_context.Gas.op_plusat contents_comparison compare_address)
(add_nat ticket_a.(Script_typed_ir.ticket.amount)
ticket_b.(Script_typed_ir.ticket.amount)).
Module Control.
Definition nil : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KNil.
Definition cons_value : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KCons.
Definition _return : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KReturn.
Definition view_exit : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KView_exit.
Definition map_head : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KMap_head.
Definition undip : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KUndip.
Definition loop_in : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KLoop_in.
Definition loop_in_left : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KLoop_in_left.
Definition iter : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_N_KIter.
Definition list_enter_body {A : Set} (xs : list A) (ys_len : int)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_N_KList_enter_body xs ys_len).
Definition list_exit_body : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_KList_exit_body.
Definition map_enter_body : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_N_KMap_enter_body.
Definition map_exit_body {k v : Set}
(key_value : k) (map : Script_typed_ir.map k v)
: Alpha_context.Gas.cost := map_update key_value map.
End Control.
Definition concat_string_precheck {a : Set}
(l_value : Script_typed_ir.boxed_list a) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.mul (S.safe_int l_value.(Script_typed_ir.boxed_list.length))
(S.safe_int 10)).
Definition concat_string (total_bytes : S.t) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.add (S.safe_int 100) (S.ediv total_bytes (S.safe_int 10))).
Definition concat_bytes (total_bytes : S.t) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.add (S.safe_int 100) (S.ediv total_bytes (S.safe_int 10))).
Definition balance : Alpha_context.Gas.cost := Alpha_context.Gas.free.
Definition unpack (bytes_value : bytes) : Alpha_context.Gas.cost :=
let blen := Bytes.length bytes_value in
Alpha_context.Gas.atomic_step_cost
(S_syntax.op_plus (S.safe_int 260) (S_syntax.lsr (S.safe_int blen) 3)).
Definition unpack_failed (bytes_value : string) : Alpha_context.Gas.cost :=
let blen := String.length bytes_value in
let len := S.safe_int blen in
let d_value := Z.numbits (Z.of_int blen) in
Alpha_context.Gas.op_plusat
(Alpha_context.Gas.op_starat len (Alpha_context.Gas.alloc_mbytes_cost 1))
(Alpha_context.Gas.op_starat len
(Alpha_context.Gas.op_starat (S.safe_int d_value)
(Alpha_context.Gas.op_plusat
(Alpha_context.Gas.alloc_cost (S.safe_int 3))
(Alpha_context.Gas.step_cost S.one)))).
End Interpreter.
Module Typechecking.
Definition public_key_optimized : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_DECODING_PUBLIC_KEY_ed25519
(S.max Generated_costs.cost_DECODING_PUBLIC_KEY_secp256k1
Generated_costs.cost_DECODING_PUBLIC_KEY_p256)).
Definition public_key_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_ed25519
(S.max Generated_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_secp256k1
Generated_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_p256)).
Definition key_hash_optimized : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_DECODING_PUBLIC_KEY_HASH_ed25519
(S.max Generated_costs.cost_DECODING_PUBLIC_KEY_HASH_secp256k1
Generated_costs.cost_DECODING_PUBLIC_KEY_HASH_p256)).
Definition key_hash_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_ed25519
(S.max
Generated_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_secp256k1
Generated_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_p256)).
Definition signature_optimized : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_DECODING_SIGNATURE_ed25519
(S.max Generated_costs.cost_DECODING_SIGNATURE_secp256k1
Generated_costs.cost_DECODING_SIGNATURE_p256)).
Definition signature_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_B58CHECK_DECODING_SIGNATURE_ed25519
(S.max Generated_costs.cost_B58CHECK_DECODING_SIGNATURE_secp256k1
Generated_costs.cost_B58CHECK_DECODING_SIGNATURE_p256)).
Definition chain_id_optimized : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_DECODING_CHAIN_ID.
Definition chain_id_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_B58CHECK_DECODING_CHAIN_ID.
Definition address_optimized : Alpha_context.Gas.cost := key_hash_optimized.
Definition contract_optimized : Alpha_context.Gas.cost :=
key_hash_optimized.
Definition contract_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.op_starat (S.safe_int 2) key_hash_readable.
Definition bls12_381_g1 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_DECODING_BLS_G1.
Definition bls12_381_g2 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_DECODING_BLS_G2.
Definition bls12_381_fr : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_DECODING_BLS_FR.
Definition check_printable (s_value : string) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_CHECK_PRINTABLE (String.length s_value)).
Definition merge_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_TY_EQ.
Definition parse_type_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_PARSE_TYPE.
Definition parse_instr_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_TYPECHECKING_CODE.
Definition parse_data_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_TYPECHECKING_DATA.
Definition comparable_ty_of_ty_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_COMPARABLE_TY_OF_TY.
Definition check_dupable_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_TYPECHECKING_DATA.
Definition find_entrypoint_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_FIND_ENTRYPOINT.
Definition bool_value : Alpha_context.Gas.cost := Alpha_context.Gas.free.
Definition unit_value : Alpha_context.Gas.cost := Alpha_context.Gas.free.
Definition timestamp_readable (s_value : string) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_TIMESTAMP_READABLE_DECODING
(String.length s_value)).
TODO: https://gitlab.com/tezos/tezos/-/issues/2340
Refine the gas model
Definition tx_rollup_l2_address : Alpha_context.Gas.cost := bls12_381_g1.
Definition contract_exists : Alpha_context.Gas.cost :=
Alpha_context.Gas.cost_of_repr (Storage_costs.read_access 4 8).
Definition proof_argument (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.mul (S.safe_int n_value) (S.safe_int 50)).
Definition chest_key_value : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_DECODING_Chest_key.
Definition chest_value (bytes_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_DECODING_Chest bytes_value).
End Typechecking.
Module Unparsing.
Definition public_key_optimized : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_ENCODING_PUBLIC_KEY_ed25519
(S.max Generated_costs.cost_ENCODING_PUBLIC_KEY_secp256k1
Generated_costs.cost_ENCODING_PUBLIC_KEY_p256)).
Definition public_key_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_ed25519
(S.max Generated_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_secp256k1
Generated_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_p256)).
Definition key_hash_optimized : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_ENCODING_PUBLIC_KEY_HASH_ed25519
(S.max Generated_costs.cost_ENCODING_PUBLIC_KEY_HASH_secp256k1
Generated_costs.cost_ENCODING_PUBLIC_KEY_HASH_p256)).
Definition key_hash_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_ed25519
(S.max
Generated_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_secp256k1
Generated_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_p256)).
Definition signature_optimized : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_ENCODING_SIGNATURE_ed25519
(S.max Generated_costs.cost_ENCODING_SIGNATURE_secp256k1
Generated_costs.cost_ENCODING_SIGNATURE_p256)).
Definition signature_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_B58CHECK_ENCODING_SIGNATURE_ed25519
(S.max Generated_costs.cost_B58CHECK_ENCODING_SIGNATURE_secp256k1
Generated_costs.cost_B58CHECK_ENCODING_SIGNATURE_p256)).
Definition chain_id_optimized : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_ENCODING_CHAIN_ID.
Definition chain_id_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_B58CHECK_ENCODING_CHAIN_ID.
Definition timestamp_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_TIMESTAMP_READABLE_ENCODING.
Definition address_optimized : Alpha_context.Gas.cost := key_hash_optimized.
Definition contract_optimized : Alpha_context.Gas.cost :=
key_hash_optimized.
Definition contract_readable : Alpha_context.Gas.cost := key_hash_readable.
Definition bls12_381_g1 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_ENCODING_BLS_G1.
Definition bls12_381_g2 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_ENCODING_BLS_G2.
Definition bls12_381_fr : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_ENCODING_BLS_FR.
Definition unparse_type (ty : Script_typed_ir.ty)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_UNPARSE_TYPE
(Script_typed_ir.Type_size.to_int (Script_typed_ir.ty_size ty))).
Definition unparse_comparable_type (comp_ty : Script_typed_ir.comparable_ty)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_UNPARSE_COMPARABLE_TYPE
(Script_typed_ir.Type_size.to_int
(Script_typed_ir.comparable_ty_size comp_ty))).
Definition unparse_instr_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_UNPARSING_CODE.
Definition unparse_data_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_UNPARSING_DATA.
Definition unit_value : Alpha_context.Gas.cost := Alpha_context.Gas.free.
Definition contract_exists : Alpha_context.Gas.cost :=
Alpha_context.Gas.cost_of_repr (Storage_costs.read_access 4 8).
Definition proof_argument (n_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.mul (S.safe_int n_value) (S.safe_int 50)).
Definition chest_key_value : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_DECODING_Chest_key.
Definition chest_value (bytes_value : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_DECODING_Chest bytes_value).
End Typechecking.
Module Unparsing.
Definition public_key_optimized : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_ENCODING_PUBLIC_KEY_ed25519
(S.max Generated_costs.cost_ENCODING_PUBLIC_KEY_secp256k1
Generated_costs.cost_ENCODING_PUBLIC_KEY_p256)).
Definition public_key_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_ed25519
(S.max Generated_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_secp256k1
Generated_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_p256)).
Definition key_hash_optimized : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_ENCODING_PUBLIC_KEY_HASH_ed25519
(S.max Generated_costs.cost_ENCODING_PUBLIC_KEY_HASH_secp256k1
Generated_costs.cost_ENCODING_PUBLIC_KEY_HASH_p256)).
Definition key_hash_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_ed25519
(S.max
Generated_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_secp256k1
Generated_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_p256)).
Definition signature_optimized : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_ENCODING_SIGNATURE_ed25519
(S.max Generated_costs.cost_ENCODING_SIGNATURE_secp256k1
Generated_costs.cost_ENCODING_SIGNATURE_p256)).
Definition signature_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(S.max Generated_costs.cost_B58CHECK_ENCODING_SIGNATURE_ed25519
(S.max Generated_costs.cost_B58CHECK_ENCODING_SIGNATURE_secp256k1
Generated_costs.cost_B58CHECK_ENCODING_SIGNATURE_p256)).
Definition chain_id_optimized : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_ENCODING_CHAIN_ID.
Definition chain_id_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_B58CHECK_ENCODING_CHAIN_ID.
Definition timestamp_readable : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
Generated_costs.cost_TIMESTAMP_READABLE_ENCODING.
Definition address_optimized : Alpha_context.Gas.cost := key_hash_optimized.
Definition contract_optimized : Alpha_context.Gas.cost :=
key_hash_optimized.
Definition contract_readable : Alpha_context.Gas.cost := key_hash_readable.
Definition bls12_381_g1 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_ENCODING_BLS_G1.
Definition bls12_381_g2 : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_ENCODING_BLS_G2.
Definition bls12_381_fr : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_ENCODING_BLS_FR.
Definition unparse_type (ty : Script_typed_ir.ty)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_UNPARSE_TYPE
(Script_typed_ir.Type_size.to_int (Script_typed_ir.ty_size ty))).
Definition unparse_comparable_type (comp_ty : Script_typed_ir.comparable_ty)
: Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_UNPARSE_COMPARABLE_TYPE
(Script_typed_ir.Type_size.to_int
(Script_typed_ir.comparable_ty_size comp_ty))).
Definition unparse_instr_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_UNPARSING_CODE.
Definition unparse_data_cycle : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_UNPARSING_DATA.
Definition unit_value : Alpha_context.Gas.cost := Alpha_context.Gas.free.
TODO: https://gitlab.com/tezos/tezos/-/issues/2340
Refine the gas model
Definition tx_rollup_l2_address : Alpha_context.Gas.cost := bls12_381_g1.
Definition operation (bytes_value : bytes) : Alpha_context.Gas.cost :=
Alpha_context.Script.bytes_node_cost bytes_value.
Definition sapling_transaction (t_value : Alpha_context.Sapling.transaction)
: Alpha_context.Gas.cost :=
let inputs := Size.sapling_transaction_inputs t_value in
let outputs := Size.sapling_transaction_outputs t_value in
let bound_data := Size.sapling_transaction_bound_data t_value in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_SAPLING_TRANSACTION_ENCODING inputs outputs
bound_data).
Definition sapling_transaction_deprecated
(t_value : Alpha_context.Sapling.Legacy.transaction)
: Alpha_context.Gas.cost :=
let inputs := List.length t_value.(Sapling.UTXO.Legacy.transaction.inputs)
in
let outputs :=
List.length t_value.(Sapling.UTXO.Legacy.transaction.outputs) in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_SAPLING_TRANSACTION_ENCODING inputs outputs 0).
Definition sapling_diff (d_value : Alpha_context.Sapling.diff)
: Alpha_context.Gas.cost :=
let nfs := List.length d_value.(Alpha_context.Sapling.diff.nullifiers) in
let cms :=
List.length
d_value.(Alpha_context.Sapling.diff.commitments_and_ciphertexts) in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_SAPLING_DIFF_ENCODING nfs cms).
Definition chest_key_value : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_ENCODING_Chest_key.
Definition chest_value (plaintext_size : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_ENCODING_Chest plaintext_size).
End Unparsing.
End Cost_of.
Definition operation (bytes_value : bytes) : Alpha_context.Gas.cost :=
Alpha_context.Script.bytes_node_cost bytes_value.
Definition sapling_transaction (t_value : Alpha_context.Sapling.transaction)
: Alpha_context.Gas.cost :=
let inputs := Size.sapling_transaction_inputs t_value in
let outputs := Size.sapling_transaction_outputs t_value in
let bound_data := Size.sapling_transaction_bound_data t_value in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_SAPLING_TRANSACTION_ENCODING inputs outputs
bound_data).
Definition sapling_transaction_deprecated
(t_value : Alpha_context.Sapling.Legacy.transaction)
: Alpha_context.Gas.cost :=
let inputs := List.length t_value.(Sapling.UTXO.Legacy.transaction.inputs)
in
let outputs :=
List.length t_value.(Sapling.UTXO.Legacy.transaction.outputs) in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_SAPLING_TRANSACTION_ENCODING inputs outputs 0).
Definition sapling_diff (d_value : Alpha_context.Sapling.diff)
: Alpha_context.Gas.cost :=
let nfs := List.length d_value.(Alpha_context.Sapling.diff.nullifiers) in
let cms :=
List.length
d_value.(Alpha_context.Sapling.diff.commitments_and_ciphertexts) in
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_SAPLING_DIFF_ENCODING nfs cms).
Definition chest_key_value : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost Generated_costs.cost_ENCODING_Chest_key.
Definition chest_value (plaintext_size : int) : Alpha_context.Gas.cost :=
Alpha_context.Gas.atomic_step_cost
(Generated_costs.cost_ENCODING_Chest plaintext_size).
End Unparsing.
End Cost_of.