Skip to main content

🍬 Michelson_v1_gas.v

Translated OCaml

See proofs, Gitlab , 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).

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)).

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.

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.