🍬 Michelson_v1_gas_costs_generated.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Module S := Saturation_repr.
Module S_syntax := S.Syntax.
Definition cost_N_IAbs_int (size_value : int) : S.t :=
S.safe_int (20 +i (Pervasives.lsr size_value 1)).
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) : Saturation_repr.t :=
let v0 := S.safe_int (Compare.Int.max size1 size2) in
S_syntax.op_plus (S.safe_int 35) (S_syntax.lsr v0 1).
Definition cost_N_IAdd_int : int → int → Saturation_repr.t :=
cost_linear_op_int.
Definition cost_N_IAdd_nat : int → int → Saturation_repr.t :=
cost_linear_op_int.
Definition cost_N_IAdd_seconds_to_timestamp : int → int → Saturation_repr.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 → Saturation_repr.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)
: Saturation_repr.t :=
let v0 := S.safe_int (Compare.Int.min size1 size2) in
S_syntax.op_plus (S.safe_int 35) (S_syntax.lsr v0 1).
Definition cost_N_IAnd_nat (size1 : int) (size2 : int) : Saturation_repr.t :=
let v0 := S.safe_int (Compare.Int.min size1 size2) in
S_syntax.op_plus (S.safe_int 35) (S_syntax.lsr v0 1).
Definition cost_N_IAnd_bytes (size1 : int) (size2 : int) : Saturation_repr.t :=
let v0 := S.safe_int (Compare.Int.min size1 size2) in
S_syntax.op_plus (S.safe_int 30) (S_syntax.lsr v0 1).
Definition cost_N_IBalance : S.t := S.safe_int 10.
Definition cost_N_IBlake2b (size_value : int) : Saturation_repr.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)
: Saturation_repr.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)
: Saturation_repr.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)
: Saturation_repr.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) : Saturation_repr.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) : Saturation_repr.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) : Saturation_repr.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) : Saturation_repr.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)
: Saturation_repr.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 1).
Definition cost_N_IConcat_string_pair (size1 : int) (size2 : int)
: Saturation_repr.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 1).
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 60.
Definition cost_N_IDiff_timestamps : int → int → Saturation_repr.t :=
cost_linear_op_int.
Definition cost_N_IDig (size_value : int) : Saturation_repr.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) : Saturation_repr.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 15) (S_syntax.op_star (S.safe_int 4) v0).
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) : Saturation_repr.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) : Saturation_repr.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) : Saturation_repr.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 2).
Definition cost_div_int (size1 : int) (size2 : int) : Saturation_repr.t :=
let q_value := size1 -i size2 in
let v1 := S.safe_int size1 in
if q_value <i 0 then
S_syntax.op_plus (S.safe_int 105) (S_syntax.lsr v1 1)
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_syntax.op_plus (S.safe_int 105) (S_syntax.lsr v0 10))
(S_syntax.lsr v0 11)) (S_syntax.lsr v0 13)) (S_syntax.lsr v1 1).
Definition cost_N_IEdiv_int : int → int → Saturation_repr.t := cost_div_int.
Definition cost_N_IEdiv_nat : int → int → Saturation_repr.t := cost_div_int.
Definition cost_N_IEdiv_tez : S.t := S.safe_int 80.
Definition cost_N_IEmpty_big_map : S.t := S.safe_int 300.
Definition cost_N_IEmpty_map : S.t := S.safe_int 300.
Definition cost_N_IEmpty_set : S.t := S.safe_int 300.
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 15.
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_N_IOpt_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) : Saturation_repr.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 : S.t := S.safe_int 20.
Definition cost_N_IList_map : S.t := 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) : Saturation_repr.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 128) (S_syntax.lsr v0 1).
Definition cost_N_ILsr_nat (size_value : int) : Saturation_repr.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 45) (S_syntax.lsr v0 1).
Definition cost_N_ILsl_bytes (size_value : int) (shift : int)
: Saturation_repr.t :=
let v1 := S.safe_int size_value in
let v0 := S.safe_int shift in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 70) (S_syntax.lsr v1 1))
(S_syntax.lsr v0 4).
Definition cost_N_ILsr_bytes (size_value : int) (shift : int) : S.t :=
let q_value := size_value -i (Pervasives.lsr shift 3) in
if q_value <i 0 then
S.safe_int 70
else
let v0 := S.safe_int q_value in
S.Syntax.op_plus (S.safe_int 70) (S.Syntax.lsr v0 1).
Definition cost_N_ILt : S.t := S.safe_int 10.
Definition cost_N_IMap_get (size1 : int) (size2 : int) : Saturation_repr.t :=
let size1 := S.safe_int size1 in
let size2 := S.safe_int size2 in
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 : int) (size2 : int)
: Saturation_repr.t :=
let size1 := S.safe_int size1 in
let size2 := S.safe_int size2 in
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) : Saturation_repr.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) : Saturation_repr.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 40)
(S_syntax.op_plus (S_syntax.op_star (S.safe_int 8) v0) (S_syntax.lsr v0 1)).
Definition cost_N_IMap_mem (size1 : int) (size2 : int) : Saturation_repr.t :=
let size1 := S.safe_int size1 in
let size2 := S.safe_int size2 in
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 : int) (size2 : int) : Saturation_repr.t :=
let size1 := S.safe_int size1 in
let size2 := S.safe_int size2 in
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) : Saturation_repr.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) : Saturation_repr.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) : Saturation_repr.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 → Saturation_repr.t := cost_mul.
Definition cost_N_IMul_nat : int → int → Saturation_repr.t := cost_mul.
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) : Saturation_repr.t :=
S_syntax.op_plus (S.safe_int 25) (S_syntax.lsr (S.safe_int size_value) 1).
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) : Saturation_repr.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 25) (S_syntax.lsr v0 1).
Definition cost_N_INot_bytes (size_value : int) : Saturation_repr.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 30) (S_syntax.lsr v0 1).
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 (time : int) (chest_value : int)
: Saturation_repr.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 → Saturation_repr.t :=
cost_linear_op_int.
Definition cost_N_IOr_bytes (size1 : int) (size2 : int) : Saturation_repr.t :=
let v0 := S.safe_int (Compare.Int.max size1 size2) in
S_syntax.op_plus (S.safe_int 30) (S_syntax.lsr v0 1).
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 300.
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 60.
Definition cost_N_ISet_iter (size_value : int) : Saturation_repr.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) : Saturation_repr.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 → Saturation_repr.t := cost_N_IKeccak.
Definition cost_N_ISha512 (size_value : int) : Saturation_repr.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) : Saturation_repr.t :=
S_syntax.op_plus (S.safe_int 25) (S_syntax.lsr (S.safe_int size_value) 1).
Definition cost_N_ISlice_string (size_value : int) : Saturation_repr.t :=
S_syntax.op_plus (S.safe_int 25) (S_syntax.lsr (S.safe_int size_value) 1).
Definition cost_N_ISource : S.t := S.safe_int 10.
Definition cost_N_ISplit_ticket (size1 : int) (size2 : int)
: Saturation_repr.t :=
let v1 := S.safe_int (Compare.Int.max size1 size2) in
S_syntax.op_plus (S.safe_int 40) (S_syntax.lsr v1 1).
Definition cost_N_IString_size : S.t := S.safe_int 15.
Definition cost_N_ISub_int : int → int → Saturation_repr.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 → Saturation_repr.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 450.
Definition cost_N_ITransfer_tokens : S.t := S.safe_int 60.
Definition cost_N_IUncomb (size_value : int) : Saturation_repr.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 640.
Definition cost_N_IXor : S.t := S.safe_int 15.
Definition cost_N_IXor_nat : int → int → Saturation_repr.t :=
cost_linear_op_int.
Definition cost_N_IXor_bytes (size1 : int) (size2 : int) : Saturation_repr.t :=
let v0 := S.safe_int (Compare.Int.max size1 size2) in
S_syntax.op_plus (S.safe_int 30) (S_syntax.lsr v0 1).
Definition cost_N_KCons : S.t := S.safe_int 10.
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_KNil : S.t := S.safe_int 15.
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) : Saturation_repr.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 10000.
Definition cost_ENCODING_Chest (plaintext_size : int) : Saturation_repr.t :=
let v0 := S.safe_int plaintext_size in
S_syntax.op_plus (S.safe_int 12200) (S_syntax.lsr v0 3).
Definition cost_TIMESTAMP_READABLE_DECODING (bytes_value : int)
: Saturation_repr.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 105)
(S_syntax.op_plus (S_syntax.lsr v0 5) (S_syntax.lsr v0 6)).
Definition cost_TIMESTAMP_READABLE_ENCODING : S.t := S.safe_int 820.
Definition cost_CHECK_PRINTABLE (size_value : int) : Saturation_repr.t :=
S_syntax.op_plus (S.safe_int 14)
(S_syntax.op_star (S.safe_int 10) (S.safe_int size_value)).
Definition cost_N_IEmit : S.t := S.safe_int 30.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Module S := Saturation_repr.
Module S_syntax := S.Syntax.
Definition cost_N_IAbs_int (size_value : int) : S.t :=
S.safe_int (20 +i (Pervasives.lsr size_value 1)).
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) : Saturation_repr.t :=
let v0 := S.safe_int (Compare.Int.max size1 size2) in
S_syntax.op_plus (S.safe_int 35) (S_syntax.lsr v0 1).
Definition cost_N_IAdd_int : int → int → Saturation_repr.t :=
cost_linear_op_int.
Definition cost_N_IAdd_nat : int → int → Saturation_repr.t :=
cost_linear_op_int.
Definition cost_N_IAdd_seconds_to_timestamp : int → int → Saturation_repr.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 → Saturation_repr.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)
: Saturation_repr.t :=
let v0 := S.safe_int (Compare.Int.min size1 size2) in
S_syntax.op_plus (S.safe_int 35) (S_syntax.lsr v0 1).
Definition cost_N_IAnd_nat (size1 : int) (size2 : int) : Saturation_repr.t :=
let v0 := S.safe_int (Compare.Int.min size1 size2) in
S_syntax.op_plus (S.safe_int 35) (S_syntax.lsr v0 1).
Definition cost_N_IAnd_bytes (size1 : int) (size2 : int) : Saturation_repr.t :=
let v0 := S.safe_int (Compare.Int.min size1 size2) in
S_syntax.op_plus (S.safe_int 30) (S_syntax.lsr v0 1).
Definition cost_N_IBalance : S.t := S.safe_int 10.
Definition cost_N_IBlake2b (size_value : int) : Saturation_repr.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)
: Saturation_repr.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)
: Saturation_repr.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)
: Saturation_repr.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) : Saturation_repr.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) : Saturation_repr.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) : Saturation_repr.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) : Saturation_repr.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)
: Saturation_repr.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 1).
Definition cost_N_IConcat_string_pair (size1 : int) (size2 : int)
: Saturation_repr.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 1).
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 60.
Definition cost_N_IDiff_timestamps : int → int → Saturation_repr.t :=
cost_linear_op_int.
Definition cost_N_IDig (size_value : int) : Saturation_repr.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) : Saturation_repr.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 15) (S_syntax.op_star (S.safe_int 4) v0).
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) : Saturation_repr.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) : Saturation_repr.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) : Saturation_repr.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 2).
Definition cost_div_int (size1 : int) (size2 : int) : Saturation_repr.t :=
let q_value := size1 -i size2 in
let v1 := S.safe_int size1 in
if q_value <i 0 then
S_syntax.op_plus (S.safe_int 105) (S_syntax.lsr v1 1)
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_syntax.op_plus (S.safe_int 105) (S_syntax.lsr v0 10))
(S_syntax.lsr v0 11)) (S_syntax.lsr v0 13)) (S_syntax.lsr v1 1).
Definition cost_N_IEdiv_int : int → int → Saturation_repr.t := cost_div_int.
Definition cost_N_IEdiv_nat : int → int → Saturation_repr.t := cost_div_int.
Definition cost_N_IEdiv_tez : S.t := S.safe_int 80.
Definition cost_N_IEmpty_big_map : S.t := S.safe_int 300.
Definition cost_N_IEmpty_map : S.t := S.safe_int 300.
Definition cost_N_IEmpty_set : S.t := S.safe_int 300.
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 15.
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_N_IOpt_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) : Saturation_repr.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 : S.t := S.safe_int 20.
Definition cost_N_IList_map : S.t := 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) : Saturation_repr.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 128) (S_syntax.lsr v0 1).
Definition cost_N_ILsr_nat (size_value : int) : Saturation_repr.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 45) (S_syntax.lsr v0 1).
Definition cost_N_ILsl_bytes (size_value : int) (shift : int)
: Saturation_repr.t :=
let v1 := S.safe_int size_value in
let v0 := S.safe_int shift in
S_syntax.op_plus (S_syntax.op_plus (S.safe_int 70) (S_syntax.lsr v1 1))
(S_syntax.lsr v0 4).
Definition cost_N_ILsr_bytes (size_value : int) (shift : int) : S.t :=
let q_value := size_value -i (Pervasives.lsr shift 3) in
if q_value <i 0 then
S.safe_int 70
else
let v0 := S.safe_int q_value in
S.Syntax.op_plus (S.safe_int 70) (S.Syntax.lsr v0 1).
Definition cost_N_ILt : S.t := S.safe_int 10.
Definition cost_N_IMap_get (size1 : int) (size2 : int) : Saturation_repr.t :=
let size1 := S.safe_int size1 in
let size2 := S.safe_int size2 in
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 : int) (size2 : int)
: Saturation_repr.t :=
let size1 := S.safe_int size1 in
let size2 := S.safe_int size2 in
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) : Saturation_repr.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) : Saturation_repr.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 40)
(S_syntax.op_plus (S_syntax.op_star (S.safe_int 8) v0) (S_syntax.lsr v0 1)).
Definition cost_N_IMap_mem (size1 : int) (size2 : int) : Saturation_repr.t :=
let size1 := S.safe_int size1 in
let size2 := S.safe_int size2 in
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 : int) (size2 : int) : Saturation_repr.t :=
let size1 := S.safe_int size1 in
let size2 := S.safe_int size2 in
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) : Saturation_repr.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) : Saturation_repr.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) : Saturation_repr.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 → Saturation_repr.t := cost_mul.
Definition cost_N_IMul_nat : int → int → Saturation_repr.t := cost_mul.
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) : Saturation_repr.t :=
S_syntax.op_plus (S.safe_int 25) (S_syntax.lsr (S.safe_int size_value) 1).
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) : Saturation_repr.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 25) (S_syntax.lsr v0 1).
Definition cost_N_INot_bytes (size_value : int) : Saturation_repr.t :=
let v0 := S.safe_int size_value in
S_syntax.op_plus (S.safe_int 30) (S_syntax.lsr v0 1).
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 (time : int) (chest_value : int)
: Saturation_repr.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 → Saturation_repr.t :=
cost_linear_op_int.
Definition cost_N_IOr_bytes (size1 : int) (size2 : int) : Saturation_repr.t :=
let v0 := S.safe_int (Compare.Int.max size1 size2) in
S_syntax.op_plus (S.safe_int 30) (S_syntax.lsr v0 1).
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 300.
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 60.
Definition cost_N_ISet_iter (size_value : int) : Saturation_repr.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) : Saturation_repr.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 → Saturation_repr.t := cost_N_IKeccak.
Definition cost_N_ISha512 (size_value : int) : Saturation_repr.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) : Saturation_repr.t :=
S_syntax.op_plus (S.safe_int 25) (S_syntax.lsr (S.safe_int size_value) 1).
Definition cost_N_ISlice_string (size_value : int) : Saturation_repr.t :=
S_syntax.op_plus (S.safe_int 25) (S_syntax.lsr (S.safe_int size_value) 1).
Definition cost_N_ISource : S.t := S.safe_int 10.
Definition cost_N_ISplit_ticket (size1 : int) (size2 : int)
: Saturation_repr.t :=
let v1 := S.safe_int (Compare.Int.max size1 size2) in
S_syntax.op_plus (S.safe_int 40) (S_syntax.lsr v1 1).
Definition cost_N_IString_size : S.t := S.safe_int 15.
Definition cost_N_ISub_int : int → int → Saturation_repr.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 → Saturation_repr.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 450.
Definition cost_N_ITransfer_tokens : S.t := S.safe_int 60.
Definition cost_N_IUncomb (size_value : int) : Saturation_repr.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 640.
Definition cost_N_IXor : S.t := S.safe_int 15.
Definition cost_N_IXor_nat : int → int → Saturation_repr.t :=
cost_linear_op_int.
Definition cost_N_IXor_bytes (size1 : int) (size2 : int) : Saturation_repr.t :=
let v0 := S.safe_int (Compare.Int.max size1 size2) in
S_syntax.op_plus (S.safe_int 30) (S_syntax.lsr v0 1).
Definition cost_N_KCons : S.t := S.safe_int 10.
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_KNil : S.t := S.safe_int 15.
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) : Saturation_repr.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 10000.
Definition cost_ENCODING_Chest (plaintext_size : int) : Saturation_repr.t :=
let v0 := S.safe_int plaintext_size in
S_syntax.op_plus (S.safe_int 12200) (S_syntax.lsr v0 3).
Definition cost_TIMESTAMP_READABLE_DECODING (bytes_value : int)
: Saturation_repr.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 105)
(S_syntax.op_plus (S_syntax.lsr v0 5) (S_syntax.lsr v0 6)).
Definition cost_TIMESTAMP_READABLE_ENCODING : S.t := S.safe_int 820.
Definition cost_CHECK_PRINTABLE (size_value : int) : Saturation_repr.t :=
S_syntax.op_plus (S.safe_int 14)
(S_syntax.op_star (S.safe_int 10) (S.safe_int size_value)).
Definition cost_N_IEmit : S.t := S.safe_int 30.