🍬 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.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Dependent_bool.
Require TezosOfOCaml.Proto_alpha.Gas_input_size.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_gas_costs.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_list.
Require TezosOfOCaml.Proto_alpha.Script_map.
Require TezosOfOCaml.Proto_alpha.Script_set.
Require TezosOfOCaml.Proto_alpha.Script_string.
Require TezosOfOCaml.Proto_alpha.Script_timestamp.
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.
  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 : Script_int.num) : int :=
    z_bytes (Script_int.to_zint z_value).

  Definition manager_operation_int : int := 1000.

  Definition manager_operation : Alpha_context.Gas.cost :=
    Alpha_context.Gas.step_cost (S.safe_int manager_operation_int).

  Module Interpreter.
    Definition drop : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IDrop.

    Definition dup : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IDup.

    Definition swap : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_ISwap.

    Definition cons_some : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_ICons_some.

    Definition cons_none : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_ICons_none.

    Definition if_none : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IIf_none.

    Definition opt_map : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IOpt_map.

    Definition cons_pair : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_ICons_pair.

    Definition unpair : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IUnpair.

    Definition car : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_ICar.

    Definition cdr : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_ICdr.

    Definition cons_left : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_ILeft.

    Definition cons_right : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IRight.

    Definition if_left : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IIf_left.

    Definition cons_list : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_ICons_list.

    Definition nil : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_INil.

    Definition if_cons : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IIf_cons.

    Definition list_map {a : Set} (function_parameter : Script_list.t a)
      : Alpha_context.Gas.cost :=
      let '_ := function_parameter in
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IList_map.

    Definition list_size : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_IList_size.

    Definition list_iter {a : Set} (function_parameter : Script_list.t a)
      : Alpha_context.Gas.cost :=
      let '_ := function_parameter in
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_IList_iter.

    Definition empty_set : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_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
        (Michelson_v1_gas_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 Michelson_v1_gas_costs.cost_N_ISet_size.

    Definition empty_map : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_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
        (Michelson_v1_gas_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
        (Michelson_v1_gas_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 Michelson_v1_gas_costs.cost_N_IMap_size.

    Definition big_map_elt_size : 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
        (Michelson_v1_gas_costs.cost_N_IMap_mem big_map_elt_size 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
        (Michelson_v1_gas_costs.cost_N_IMap_get big_map_elt_size 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
        (Michelson_v1_gas_costs.cost_N_IMap_update big_map_elt_size 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
        (Michelson_v1_gas_costs.cost_N_IMap_get_and_update big_map_elt_size
          size_value).

    Definition add_seconds_timestamp
      (seconds : Script_int.num) (timestamp : Script_timestamp.t)
      : Alpha_context.Gas.cost :=
      let seconds_bytes := int_bytes seconds in
      let timestamp_bytes := z_bytes (Script_timestamp.to_zint timestamp) in
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IAdd_seconds_to_timestamp seconds_bytes
          timestamp_bytes).

    Definition add_timestamp_seconds
      (timestamp : Script_timestamp.t) (seconds : Script_int.num)
      : Alpha_context.Gas.cost :=
      let seconds_bytes := int_bytes seconds in
      let timestamp_bytes := z_bytes (Script_timestamp.to_zint timestamp) in
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IAdd_timestamp_to_seconds timestamp_bytes
          seconds_bytes).

    Definition sub_timestamp_seconds
      (timestamp : Script_timestamp.t) (seconds : Script_int.num)
      : Alpha_context.Gas.cost :=
      let seconds_bytes := int_bytes seconds in
      let timestamp_bytes := z_bytes (Script_timestamp.to_zint timestamp) in
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_ISub_timestamp_seconds timestamp_bytes
          seconds_bytes).

    Definition diff_timestamps
      (t1 : Script_timestamp.t) (t2 : Script_timestamp.t)
      : Alpha_context.Gas.cost :=
      let t1_bytes := z_bytes (Script_timestamp.to_zint t1) in
      let t2_bytes := z_bytes (Script_timestamp.to_zint t2) in
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IDiff_timestamps t1_bytes t2_bytes).

    Definition concat_string_pair (s1 : Script_string.t) (s2 : Script_string.t)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IConcat_string_pair
          (Script_string.length s1) (Script_string.length s2)).

    Definition slice_string (s_value : Script_string.t)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_ISlice_string
          (Script_string.length s_value)).

    Definition string_size : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_IString_size.

    Definition concat_bytes_pair (b1 : bytes) (b2 : bytes)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_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
        (Michelson_v1_gas_costs.cost_N_ISlice_bytes (Bytes.length b_value)).

    Definition bytes_size : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_IBytes_size.

    Definition lsl_bytes (input : bytes) (nbits : Script_int.num)
      : Saturation_repr.t :=
      match Script_int.to_int nbits with
      | None ⇒ Saturation_repr.saturated
      | Some nbits ⇒
        Alpha_context.Gas.atomic_step_cost
          (Michelson_v1_gas_costs.cost_N_ILsl_bytes (Bytes.length input) nbits)
      end.

    Definition lsr_bytes (input : bytes) (nbits : Script_int.num)
      : Alpha_context.Gas.cost :=
      let input_nbytes := Bytes.length input in
      let nbits :=
        Option.value_value (Script_int.to_int nbits) (input_nbytes ×i 8) in
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_ILsr_bytes input_nbytes nbits).

    Definition or_bytes (b1 : bytes) (b2 : bytes) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IOr_bytes (Bytes.length b1)
          (Bytes.length b2)).

    Definition and_bytes (b1 : bytes) (b2 : bytes) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IAnd_bytes (Bytes.length b1)
          (Bytes.length b2)).

    Definition xor_bytes (b1 : bytes) (b2 : bytes) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IXor_bytes (Bytes.length b1)
          (Bytes.length b2)).

    Definition not_bytes (b_value : bytes) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_INot_bytes (Bytes.length b_value)).

    Definition add_tez : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IAdd_tez.

    Definition sub_tez : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_ISub_tez.

    Definition sub_tez_legacy : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_ISub_tez_legacy.

    Definition mul_teznat : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_IMul_teznat.

    Definition mul_nattez : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_IMul_nattez.

    Definition bool_or : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IOr.

    Definition bool_and : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IAnd.

    Definition bool_xor : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IXor.

    Definition bool_not : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_INot.

    Definition is_nat : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IIs_nat.

    Definition abs_int (i_value : Script_int.num) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IAbs_int (int_bytes i_value)).

    Definition int_nat : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IInt_nat.

    Definition neg (i_value : Script_int.num) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_INeg (int_bytes i_value)).

    Definition add_int (i1 : Script_int.num) (i2 : Script_int.num)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IAdd_int (int_bytes i1) (int_bytes i2)).

    Definition add_nat (i1 : Script_int.num) (i2 : Script_int.num)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IAdd_nat (int_bytes i1) (int_bytes i2)).

    Definition sub_int (i1 : Script_int.num) (i2 : Script_int.num)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_ISub_int (int_bytes i1) (int_bytes i2)).

    Definition mul_int (i1 : Script_int.num) (i2 : Script_int.num)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IMul_int (int_bytes i1) (int_bytes i2)).

    Definition mul_nat (i1 : Script_int.num) (i2 : Script_int.num)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_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
        Michelson_v1_gas_costs.cost_N_IEdiv_teznat.

    Definition ediv_tez : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IEdiv_tez.

    Definition ediv_int (i1 : Script_int.num) (i2 : Script_int.num)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IEdiv_int (int_bytes i1) (int_bytes i2)).

    Definition ediv_nat (i1 : Script_int.num) (i2 : Script_int.num)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IEdiv_nat (int_bytes i1) (int_bytes i2)).

    Definition eq_value : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IEq.

    Definition lsl_nat (shifted : Script_int.num) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_ILsl_nat (int_bytes shifted)).

    Definition lsr_nat (shifted : Script_int.num) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_ILsr_nat (int_bytes shifted)).

    Definition or_nat (n1 : Script_int.num) (n2 : Script_int.num)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IOr_nat (int_bytes n1) (int_bytes n2)).

    Definition and_nat (n1 : Script_int.num) (n2 : Script_int.num)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IAnd_nat (int_bytes n1) (int_bytes n2)).

    Definition and_int_nat (n1 : Script_int.num) (n2 : Script_int.num)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IAnd_int_nat (int_bytes n1)
          (int_bytes n2)).

    Definition xor_nat (n1 : Script_int.num) (n2 : Script_int.num)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IXor_nat (int_bytes n1) (int_bytes n2)).

    Definition not_int (i_value : Script_int.num) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_INot_int (int_bytes i_value)).

    Definition if_ : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IIf.

    Definition loop : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_ILoop.

    Definition loop_left : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_ILoop_left.

    Definition dip : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IDip.

    Definition view : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_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 _ ⇒
          Michelson_v1_gas_costs.cost_N_ICheck_signature_ed25519
            (Bytes.length b_value)
        | Signature.Secp256k1 _ ⇒
          Michelson_v1_gas_costs.cost_N_ICheck_signature_secp256k1
            (Bytes.length b_value)
        | Signature.P256 _ ⇒
          Michelson_v1_gas_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
        (Michelson_v1_gas_costs.cost_N_IBlake2b (Bytes.length b_value)).

    Definition sha256 (b_value : bytes) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_ISha256 (Bytes.length b_value)).

    Definition sha512 (b_value : bytes) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_ISha512 (Bytes.length b_value)).

    Definition dign (n_value : int) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IDig n_value).

    Definition dugn (n_value : int) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IDug n_value).

    Definition dipn (n_value : int) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IDipN n_value).

    Definition dropn (n_value : int) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IDropN n_value).

    Definition voting_power : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_IVoting_power.

    Definition total_voting_power : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_ITotal_voting_power.

    Definition keccak (b_value : bytes) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IKeccak (Bytes.length b_value)).

    Definition sha3 (b_value : bytes) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_ISha3 (Bytes.length b_value)).

    Definition add_bls12_381_g1 : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_IAdd_bls12_381_g1.

    Definition add_bls12_381_g2 : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_IAdd_bls12_381_g2.

    Definition add_bls12_381_fr : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_IAdd_bls12_381_fr.

    Definition mul_bls12_381_g1 : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_IMul_bls12_381_g1.

    Definition mul_bls12_381_g2 : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_IMul_bls12_381_g2.

    Definition mul_bls12_381_fr : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_IMul_bls12_381_fr.

    Definition mul_bls12_381_fr_z (z_value : Script_int.num)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IMul_bls12_381_fr_z (int_bytes z_value)).

    Definition mul_bls12_381_z_fr (z_value : Script_int.num)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_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
        Michelson_v1_gas_costs.cost_N_IInt_bls12_381_z_fr.

    Definition neg_bls12_381_g1 : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_INeg_bls12_381_g1.

    Definition neg_bls12_381_g2 : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_INeg_bls12_381_g2.

    Definition neg_bls12_381_fr : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_INeg_bls12_381_fr.

    Definition neq : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_INeq.

    Definition pairing_check_bls12_381 {a : Set} (l_value : Script_list.t a)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IPairing_check_bls12_381
          l_value.(Script_list.t.length)).

    Definition comb (n_value : int) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IComb n_value).

    Definition uncomb (n_value : int) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IUncomb n_value).

    Definition comb_get (n_value : int) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IComb_get n_value).

    Definition comb_set (n_value : int) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IComb_set n_value).

    Definition dupn (n_value : int) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_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
        (Michelson_v1_gas_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
        (Michelson_v1_gas_costs.cost_N_ISapling_verify_update inputs outputs 0).

    Definition sapling_empty_state : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_ISapling_empty_state.

    Definition halt : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IHalt.

    Definition const : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IConst.

    Definition empty_big_map : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_IEmpty_big_map.

    Definition lt : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_ILt.

    Definition le : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_ILe.

    Definition gt : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IGt.

    Definition ge : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IGe.

    Definition exec : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IExec.

    Definition apply (rec_flag : bool) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_IApply rec_flag).

    Definition lambda : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_ILambda.

    Definition address : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IAddress.

    Definition contract : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IContract.

    Definition transfer_tokens : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_ITransfer_tokens.

    Definition implicit_account : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_IImplicit_account.

    Definition create_contract : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_ICreate_contract.

    Definition set_delegate : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_ISet_delegate.

    Definition level : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_ILevel.

    Definition now : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_INow.

    Definition min_block_time : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_IMin_block_time.

    Definition source : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_ISource.

    Definition sender : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_ISender.

    Definition self : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_ISelf.

    Definition self_address : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_N_ISelf_address.

    Definition amount : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IAmount.

    Definition balance : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IBalance.

    Definition chain_id : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IChainId.

    Definition ticket : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_ITicket.

    Definition read_ticket : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_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 Michelson_v1_gas_costs.cost_N_IHash_key.

    Definition split_ticket
      (amount_a : Script_int.num) (amount_b : Script_int.num)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_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
        (Michelson_v1_gas_costs.cost_N_IOpen_chest log_time plaintext).

    Definition compare_unit : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost (Michelson_v1_gas_costs.S.safe_int 10).

    Definition compare_pair_tag : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost (Michelson_v1_gas_costs.S.safe_int 10).

    Definition compare_union_tag : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost (Michelson_v1_gas_costs.S.safe_int 10).

    Definition compare_option_tag : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost (Michelson_v1_gas_costs.S.safe_int 10).

    Definition compare_bool : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_ICompare 1 1).

    Definition compare_signature : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost (Michelson_v1_gas_costs.S.safe_int 92).

    Definition compare_string (s1 : Script_string.t) (s2 : Script_string.t)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_ICompare (Script_string.length s1)
          (Script_string.length s2)).

    Definition compare_bytes (b1 : bytes) (b2 : bytes)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_ICompare (Bytes.length b1)
          (Bytes.length b2)).

    Definition compare_mutez : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_ICompare 8 8).

    Definition compare_int (i1 : Script_int.num) (i2 : Script_int.num)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_ICompare (int_bytes i1) (int_bytes i2)).

    Definition compare_nat (n1 : Script_int.num) (n2 : Script_int.num)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_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
        (Michelson_v1_gas_costs.cost_N_ICompare sz sz).

    Definition compare_key : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost (Michelson_v1_gas_costs.S.safe_int 92).

    Definition compare_timestamp
      (t1 : Script_timestamp.t) (t2 : Script_timestamp.t)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_N_ICompare
          (z_bytes (Script_timestamp.to_zint t1))
          (z_bytes (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
        (Michelson_v1_gas_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
        (Michelson_v1_gas_costs.cost_N_ICompare 48 48).

    Definition compare_chain_id : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost (Michelson_v1_gas_costs.S.safe_int 30).

    Inductive cont : Set :=
    | Compare : ∀ {a : Set},
      Script_typed_ir.comparable_ty → a → a → cont → cont
    | Return : cont.

    Module Compare.
      Reserved Notation "'apply".

      #[bypass_check(guard)]
      Fixpoint compare {a : Set}
        (ty_value : Script_typed_ir.comparable_ty) (x_value : a) (y_value : a)
        (acc_value : Alpha_context.Gas.cost) (k_value : cont) {struct ty_value}
        : Alpha_context.Gas.cost :=
        let apply := 'apply in
        match (ty_value, x_value, y_value) with
        | (Script_typed_ir.Unit_t, _, _) ⇒
          apply (Alpha_context.Gas.op_plusat acc_value compare_unit) k_value
        | (Script_typed_ir.Bool_t, _, _) ⇒
          apply (Alpha_context.Gas.op_plusat acc_value compare_bool) k_value
        | (Script_typed_ir.String_t, x_value, y_value) ⇒
          let '[y_value, x_value] :=
            cast [Script_string.t ** Script_string.t] [y_value, x_value] in
          apply
            (Alpha_context.Gas.op_plusat acc_value
              (compare_string x_value y_value)) k_value
        | (Script_typed_ir.Signature_t, _, _) ⇒
          apply (Alpha_context.Gas.op_plusat acc_value compare_signature)
            k_value
        | (Script_typed_ir.Bytes_t, x_value, y_value) ⇒
          let '[y_value, x_value] := cast [bytes ** bytes] [y_value, x_value] in
          apply
            (Alpha_context.Gas.op_plusat acc_value
              (compare_bytes x_value y_value)) k_value
        | (Script_typed_ir.Mutez_t, _, _) ⇒
          apply (Alpha_context.Gas.op_plusat acc_value compare_mutez) k_value
        | (Script_typed_ir.Int_t, x_value, y_value) ⇒
          let '[y_value, x_value] :=
            cast [Script_int.num ** Script_int.num] [y_value, x_value] in
          apply
            (Alpha_context.Gas.op_plusat acc_value (compare_int x_value y_value))
            k_value
        | (Script_typed_ir.Nat_t, x_value, y_value) ⇒
          let '[y_value, x_value] :=
            cast [Script_int.num ** Script_int.num] [y_value, x_value] in
          apply
            (Alpha_context.Gas.op_plusat acc_value (compare_nat x_value y_value))
            k_value
        | (Script_typed_ir.Key_hash_t, _, _) ⇒
          apply (Alpha_context.Gas.op_plusat acc_value compare_key_hash) k_value
        | (Script_typed_ir.Key_t, _, _) ⇒
          apply (Alpha_context.Gas.op_plusat acc_value compare_key) k_value
        | (Script_typed_ir.Timestamp_t, x_value, y_value) ⇒
          let '[y_value, x_value] :=
            cast [Script_timestamp.t ** Script_timestamp.t] [y_value, x_value]
            in
          apply
            (Alpha_context.Gas.op_plusat acc_value
              (compare_timestamp x_value y_value)) k_value
        | (Script_typed_ir.Address_t, _, _) ⇒
          apply (Alpha_context.Gas.op_plusat acc_value compare_address) k_value
        | (Script_typed_ir.Tx_rollup_l2_address_t, _, _) ⇒
          apply
            (Alpha_context.Gas.op_plusat acc_value compare_tx_rollup_l2_address)
            k_value
        | (Script_typed_ir.Chain_id_t, _, _) ⇒
          apply (Alpha_context.Gas.op_plusat acc_value compare_chain_id) k_value
        |
          (Script_typed_ir.Pair_t tl tr _ Dependent_bool.YesYes, x_value,
            y_value) ⇒
          let 'existT _ [__0, __1] [y_value, x_value, tr, tl] :=
            cast_exists (Es := [Set ** Set])
              (fun '[__0, __1] ⇒
                [__0 × __1 ** __0 × __1 ** Script_typed_ir.ty **
                  Script_typed_ir.ty]) [y_value, x_value, tr, tl] in
          let '(xl, xr) := x_value in
          let '(yl, yr) := y_value in
          compare tl xl yl
            (Alpha_context.Gas.op_plusat acc_value compare_pair_tag)
            (Compare tr xr yr k_value)
        |
          (Script_typed_ir.Union_t tl tr _ Dependent_bool.YesYes, x_value,
            y_value) ⇒
          let 'existT _ [__2, __3] [y_value, x_value, tr, tl] :=
            cast_exists (Es := [Set ** Set])
              (fun '[__2, __3] ⇒
                [Script_typed_ir.union __2 __3 ** Script_typed_ir.union __2 __3
                  ** Script_typed_ir.ty ** Script_typed_ir.ty])
              [y_value, x_value, tr, tl] in
          match (x_value, y_value) with
          | (Script_typed_ir.L x_value, Script_typed_ir.L y_value) ⇒
            compare tl x_value y_value
              (Alpha_context.Gas.op_plusat acc_value compare_union_tag) k_value
          | (Script_typed_ir.L _, Script_typed_ir.R _) ⇒
            apply (Alpha_context.Gas.op_plusat acc_value compare_union_tag)
              k_value
          | (Script_typed_ir.R _, Script_typed_ir.L _) ⇒
            apply (Alpha_context.Gas.op_plusat acc_value compare_union_tag)
              k_value
          | (Script_typed_ir.R x_value, Script_typed_ir.R y_value) ⇒
            compare tr x_value y_value
              (Alpha_context.Gas.op_plusat acc_value compare_union_tag) k_value
          end
        |
          (Script_typed_ir.Option_t t_value _ Dependent_bool.Yes, x_value,
            y_value) ⇒
          let 'existT _ __4 [y_value, x_value, t_value] :=
            cast_exists (Es := Set)
              (fun __4 ⇒ [option __4 ** option __4 ** Script_typed_ir.ty])
              [y_value, x_value, t_value] in
          match (x_value, y_value) with
          | (None, None) ⇒
            apply (Alpha_context.Gas.op_plusat acc_value compare_option_tag)
              k_value
          | (None, Some _) ⇒
            apply (Alpha_context.Gas.op_plusat acc_value compare_option_tag)
              k_value
          | (Some _, None) ⇒
            apply (Alpha_context.Gas.op_plusat acc_value compare_option_tag)
              k_value
          | (Some x_value, Some y_value) ⇒
            compare t_value x_value y_value
              (Alpha_context.Gas.op_plusat acc_value compare_option_tag) k_value
          end
        | _ ⇒ unreachable_gadt_branch
        end
      
      where "'apply" :=
        (fun (cost : Alpha_context.Gas.cost) (k_value : cont) ⇒
          match k_value with
          | Compare ty_value x_value y_value k_value ⇒
            compare ty_value x_value y_value cost k_value
          | Return ⇒ cost
          end).

      Definition apply := 'apply.
    End Compare.

    Definition compare {a : Set}
      (ty_value : Script_typed_ir.comparable_ty) (x_value : a) (y_value : a)
      : Alpha_context.Gas.cost :=
      Compare.compare ty_value x_value y_value Alpha_context.Gas.free Return.

    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 :=
        Michelson_v1_gas_costs.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 :=
        Michelson_v1_gas_costs.S.safe_int
          Box.(Script_typed_ir.Boxed_set.size_value) in
      let intercept :=
        Alpha_context.Gas.atomic_step_cost
          (Michelson_v1_gas_costs.S.safe_int 115) in
      Alpha_context.Gas.op_plusat intercept
        (Alpha_context.Gas.op_starat
          (Michelson_v1_gas_costs.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 :=
        Michelson_v1_gas_costs.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 :=
        Michelson_v1_gas_costs.S.safe_int
          Box.(Script_typed_ir.Boxed_set.size_value) in
      let intercept :=
        Alpha_context.Gas.atomic_step_cost
          (Michelson_v1_gas_costs.S.safe_int 130) in
      Alpha_context.Gas.op_plusat intercept
        (Alpha_context.Gas.op_starat
          (Michelson_v1_gas_costs.S.Syntax.op_star
            (Michelson_v1_gas_costs.S.safe_int 2)
            (Michelson_v1_gas_costs.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 :=
        Michelson_v1_gas_costs.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 :=
        Michelson_v1_gas_costs.S.safe_int
          Box.(Script_typed_ir.Boxed_map.size_value) in
      let intercept :=
        Alpha_context.Gas.atomic_step_cost
          (Michelson_v1_gas_costs.S.safe_int 80) in
      Alpha_context.Gas.op_plusat intercept
        (Alpha_context.Gas.op_starat
          (Michelson_v1_gas_costs.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 :=
        Michelson_v1_gas_costs.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 :=
        Michelson_v1_gas_costs.S.safe_int
          Box.(Script_typed_ir.Boxed_map.size_value) in
      let intercept :=
        Alpha_context.Gas.atomic_step_cost
          (Michelson_v1_gas_costs.S.safe_int 80) in
      Alpha_context.Gas.op_plusat intercept
        (Alpha_context.Gas.op_starat
          (Michelson_v1_gas_costs.S.Syntax.op_star
            (Michelson_v1_gas_costs.S.safe_int 2)
            (Michelson_v1_gas_costs.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 :=
        Michelson_v1_gas_costs.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 :=
        Michelson_v1_gas_costs.S.safe_int
          Box.(Script_typed_ir.Boxed_map.size_value) in
      let intercept :=
        Alpha_context.Gas.atomic_step_cost
          (Michelson_v1_gas_costs.S.safe_int 80) in
      Alpha_context.Gas.op_plusat intercept
        (Alpha_context.Gas.op_starat
          (Michelson_v1_gas_costs.S.Syntax.op_star
            (Michelson_v1_gas_costs.S.safe_int 3)
            (Michelson_v1_gas_costs.S.Syntax.log2 size_value)) per_elt_cost).

    Definition view_get
      (elt_value : 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 : 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_value : 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_value 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)).

    Definition emit : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_IEmit.

    Module Control.
      Definition nil : Alpha_context.Gas.cost :=
        Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_KNil.

      Definition cons_value : Alpha_context.Gas.cost :=
        Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_KCons.

      Definition _return : Alpha_context.Gas.cost :=
        Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_KReturn.

      Definition view_exit : Alpha_context.Gas.cost :=
        Alpha_context.Gas.atomic_step_cost
          Michelson_v1_gas_costs.cost_N_KView_exit.

      Definition map_head : Alpha_context.Gas.cost :=
        Alpha_context.Gas.atomic_step_cost
          Michelson_v1_gas_costs.cost_N_KMap_head.

      Definition undip : Alpha_context.Gas.cost :=
        Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_N_KUndip.

      Definition loop_in : Alpha_context.Gas.cost :=
        Alpha_context.Gas.atomic_step_cost
          Michelson_v1_gas_costs.cost_N_KLoop_in.

      Definition loop_in_left : Alpha_context.Gas.cost :=
        Alpha_context.Gas.atomic_step_cost
          Michelson_v1_gas_costs.cost_N_KLoop_in_left.

      Definition iter : Alpha_context.Gas.cost :=
        Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_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
          (Michelson_v1_gas_costs.cost_N_KList_enter_body xs ys_len).

      Definition list_exit_body : Alpha_context.Gas.cost :=
        Alpha_context.Gas.atomic_step_cost
          Michelson_v1_gas_costs.cost_N_KList_exit_body.

      Definition map_enter_body : Alpha_context.Gas.cost :=
        Alpha_context.Gas.atomic_step_cost
          Michelson_v1_gas_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_list.t a)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.S.mul
          (Michelson_v1_gas_costs.S.safe_int l_value.(Script_list.t.length))
          (Michelson_v1_gas_costs.S.safe_int 10)).

    Definition concat_string (total_bytes : Michelson_v1_gas_costs.S.t)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.S.add (Michelson_v1_gas_costs.S.safe_int 100)
          (Michelson_v1_gas_costs.S.shift_right total_bytes 1)).

    Definition concat_bytes (total_bytes : Michelson_v1_gas_costs.S.t)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.S.add (Michelson_v1_gas_costs.S.safe_int 100)
          (Michelson_v1_gas_costs.S.shift_right total_bytes 1)).

    Definition unpack (bytes_value : bytes) : Alpha_context.Gas.cost :=
      let blen := Bytes.length bytes_value in
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.S.Syntax.op_plus
          (Michelson_v1_gas_costs.S.safe_int 260)
          (Michelson_v1_gas_costs.S.Syntax.lsr
            (Michelson_v1_gas_costs.S.safe_int blen) 1)).

    Definition unpack_failed (bytes_value : string) : Alpha_context.Gas.cost :=
      let blen := String.length bytes_value in
      let len := Michelson_v1_gas_costs.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
            (Michelson_v1_gas_costs.S.safe_int d_value)
            (Alpha_context.Gas.op_plusat
              (Alpha_context.Gas.alloc_cost
                (Michelson_v1_gas_costs.S.safe_int 3))
              (Alpha_context.Gas.step_cost Michelson_v1_gas_costs.S.one)))).
  End Interpreter.

  Module Typechecking.
    Definition public_key_optimized : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.S.max
          Michelson_v1_gas_costs.cost_DECODING_PUBLIC_KEY_ed25519
          (Michelson_v1_gas_costs.S.max
            Michelson_v1_gas_costs.cost_DECODING_PUBLIC_KEY_secp256k1
            Michelson_v1_gas_costs.cost_DECODING_PUBLIC_KEY_p256)).

    Definition public_key_readable : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.S.max
          Michelson_v1_gas_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_ed25519
          (Michelson_v1_gas_costs.S.max
            Michelson_v1_gas_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_secp256k1
            Michelson_v1_gas_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_p256)).

    Definition key_hash_optimized : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.S.max
          Michelson_v1_gas_costs.cost_DECODING_PUBLIC_KEY_HASH_ed25519
          (Michelson_v1_gas_costs.S.max
            Michelson_v1_gas_costs.cost_DECODING_PUBLIC_KEY_HASH_secp256k1
            Michelson_v1_gas_costs.cost_DECODING_PUBLIC_KEY_HASH_p256)).

    Definition key_hash_readable : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.S.max
          Michelson_v1_gas_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_ed25519
          (Michelson_v1_gas_costs.S.max
            Michelson_v1_gas_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_secp256k1
            Michelson_v1_gas_costs.cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_p256)).

    Definition signature_optimized : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.S.max
          Michelson_v1_gas_costs.cost_DECODING_SIGNATURE_ed25519
          (Michelson_v1_gas_costs.S.max
            Michelson_v1_gas_costs.cost_DECODING_SIGNATURE_secp256k1
            Michelson_v1_gas_costs.cost_DECODING_SIGNATURE_p256)).

    Definition signature_readable : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.S.max
          Michelson_v1_gas_costs.cost_B58CHECK_DECODING_SIGNATURE_ed25519
          (Michelson_v1_gas_costs.S.max
            Michelson_v1_gas_costs.cost_B58CHECK_DECODING_SIGNATURE_secp256k1
            Michelson_v1_gas_costs.cost_B58CHECK_DECODING_SIGNATURE_p256)).

    Definition chain_id_optimized : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_DECODING_CHAIN_ID.

    Definition chain_id_readable : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_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 := key_hash_readable.

    Definition bls12_381_g1 : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_DECODING_BLS_G1.

    Definition bls12_381_g2 : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_DECODING_BLS_G2.

    Definition bls12_381_fr : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_DECODING_BLS_FR.

    Definition check_printable (s_value : string) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_CHECK_PRINTABLE (String.length s_value)).

    Definition merge_cycle : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_TY_EQ.

    Definition parse_type_cycle : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost Michelson_v1_gas_costs.cost_PARSE_TYPE.

    Definition parse_instr_cycle : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_TYPECHECKING_CODE.

    Definition parse_data_cycle : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_TYPECHECKING_DATA.

    Definition check_dupable_cycle : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_TYPECHECKING_DATA.

    Definition find_entrypoint_cycle : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_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
        (Michelson_v1_gas_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
        (Michelson_v1_gas_costs.S.mul
          (Michelson_v1_gas_costs.S.safe_int n_value)
          (Michelson_v1_gas_costs.S.safe_int 50)).

    Definition chest_key_value : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_DECODING_Chest_key.

    Definition chest_value (bytes_value : int) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_DECODING_Chest bytes_value).
  End Typechecking.

  Module Unparsing.
    Definition public_key_optimized : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.S.max
          Michelson_v1_gas_costs.cost_ENCODING_PUBLIC_KEY_ed25519
          (Michelson_v1_gas_costs.S.max
            Michelson_v1_gas_costs.cost_ENCODING_PUBLIC_KEY_secp256k1
            Michelson_v1_gas_costs.cost_ENCODING_PUBLIC_KEY_p256)).

    Definition public_key_readable : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.S.max
          Michelson_v1_gas_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_ed25519
          (Michelson_v1_gas_costs.S.max
            Michelson_v1_gas_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_secp256k1
            Michelson_v1_gas_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_p256)).

    Definition key_hash_optimized : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.S.max
          Michelson_v1_gas_costs.cost_ENCODING_PUBLIC_KEY_HASH_ed25519
          (Michelson_v1_gas_costs.S.max
            Michelson_v1_gas_costs.cost_ENCODING_PUBLIC_KEY_HASH_secp256k1
            Michelson_v1_gas_costs.cost_ENCODING_PUBLIC_KEY_HASH_p256)).

    Definition key_hash_readable : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.S.max
          Michelson_v1_gas_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_ed25519
          (Michelson_v1_gas_costs.S.max
            Michelson_v1_gas_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_secp256k1
            Michelson_v1_gas_costs.cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_p256)).

    Definition signature_optimized : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.S.max
          Michelson_v1_gas_costs.cost_ENCODING_SIGNATURE_ed25519
          (Michelson_v1_gas_costs.S.max
            Michelson_v1_gas_costs.cost_ENCODING_SIGNATURE_secp256k1
            Michelson_v1_gas_costs.cost_ENCODING_SIGNATURE_p256)).

    Definition signature_readable : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.S.max
          Michelson_v1_gas_costs.cost_B58CHECK_ENCODING_SIGNATURE_ed25519
          (Michelson_v1_gas_costs.S.max
            Michelson_v1_gas_costs.cost_B58CHECK_ENCODING_SIGNATURE_secp256k1
            Michelson_v1_gas_costs.cost_B58CHECK_ENCODING_SIGNATURE_p256)).

    Definition chain_id_optimized : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_ENCODING_CHAIN_ID.

    Definition chain_id_readable : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_B58CHECK_ENCODING_CHAIN_ID.

    Definition timestamp_readable : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_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
        Michelson_v1_gas_costs.cost_ENCODING_BLS_G1.

    Definition bls12_381_g2 : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_ENCODING_BLS_G2.

    Definition bls12_381_fr : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_ENCODING_BLS_FR.

    Definition unparse_type (ty_value : Script_typed_ir.ty)
      : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_UNPARSE_TYPE
          (Script_typed_ir.Type_size.to_int (Script_typed_ir.ty_size ty_value))).

    Definition unparse_instr_cycle : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_UNPARSING_CODE.

    Definition unparse_data_cycle : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_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
        (Michelson_v1_gas_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
        (Michelson_v1_gas_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
        (Michelson_v1_gas_costs.cost_SAPLING_DIFF_ENCODING nfs cms).

    Definition chest_key_value : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        Michelson_v1_gas_costs.cost_ENCODING_Chest_key.

    Definition chest_value (plaintext_size : int) : Alpha_context.Gas.cost :=
      Alpha_context.Gas.atomic_step_cost
        (Michelson_v1_gas_costs.cost_ENCODING_Chest plaintext_size).
  End Unparsing.
End Cost_of.