Skip to main content

🍬 Michelson_v1_gas_costs_generated.v

Translated OCaml

Gitlab , 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.