Skip to main content

🍬 Script_interpreter_defs.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Init function; without side-effects in Coq
Definition init_module : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "operation.rollup_invalid_transaction_amount"
    "Transaction amount to a rollup must be zero"
    "Because rollups are outside of the delegation mechanism of Tezos, they cannot own Tez, and therefore transactions targeting a rollup must have its amount field set to zero."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.pp_print_string ppf
            "Transaction amount to a rollup must be zero."))
    Data_encoding.unit_value
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Rollup_invalid_transaction_amount" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Rollup_invalid_transaction_amount" unit tt).

Module Interp_costs := Michelson_v1_gas.Cost_of.Interpreter.

Definition cost_of_instr {a s : Set}
  (i_value : Script_typed_ir.kinstr) (accu_value : a) (stack_value : s)
  : Alpha_context.Gas.cost :=
  match (i_value, accu_value, stack_value) with
  | (Script_typed_ir.IList_map _ _ _ _, list_value, _)
    let 'existT _ __0 list_value :=
      cast_exists (Es := Set) (fun __0Script_typed_ir.boxed_list __0)
        list_value in
    Interp_costs.list_map list_value
  | (Script_typed_ir.IList_iter _ _ _ _, list_value, _)
    let 'existT _ __3 list_value :=
      cast_exists (Es := Set) (fun __3Script_typed_ir.boxed_list __3)
        list_value in
    Interp_costs.list_iter list_value
  | (Script_typed_ir.ISet_iter _ _ _ _, set, _)
    let 'existT _ __6 set :=
      cast_exists (Es := Set) (fun __6Script_typed_ir.set __6) set in
    Interp_costs.set_iter set
  | (Script_typed_ir.ISet_mem _ _, v_value, stack_value)
    let 'existT _ __9 [stack_value, v_value] :=
      cast_exists (Es := Set) (fun __9[Script_typed_ir.set a × __9 ** a])
        [stack_value, v_value] in
    let '(set, _) := stack_value in
    Interp_costs.set_mem v_value set
  | (Script_typed_ir.ISet_update _ _, v_value, stack_value)
    let 'existT _ __10 [stack_value, v_value] :=
      cast_exists (Es := Set)
        (fun __10[bool × (Script_typed_ir.set a × __10) ** a])
        [stack_value, v_value] in
    let '(_, (set, _)) := stack_value in
    Interp_costs.set_update v_value set
  | (Script_typed_ir.IMap_map _ _ _ _, map, _)
    let 'existT _ [__11, __12] map :=
      cast_exists (Es := [Set ** Set])
        (fun '[__11, __12]Script_typed_ir.map __11 __12) map in
    Interp_costs.map_map map
  | (Script_typed_ir.IMap_iter _ _ _ _, map, _)
    let 'existT _ [__15, __16] map :=
      cast_exists (Es := [Set ** Set])
        (fun '[__15, __16]Script_typed_ir.map __15 __16) map in
    Interp_costs.map_iter map
  | (Script_typed_ir.IMap_mem _ _, v_value, stack_value)
    let 'existT _ [__19, __20] [stack_value, v_value] :=
      cast_exists (Es := [Set ** Set])
        (fun '[__19, __20][Script_typed_ir.map a __19 × __20 ** a])
        [stack_value, v_value] in
    let '(map, _) := stack_value in
    Interp_costs.map_mem v_value map
  | (Script_typed_ir.IMap_get _ _, v_value, stack_value)
    let 'existT _ [__21, __22] [stack_value, v_value] :=
      cast_exists (Es := [Set ** Set])
        (fun '[__21, __22][Script_typed_ir.map a __21 × __22 ** a])
        [stack_value, v_value] in
    let '(map, _) := stack_value in
    Interp_costs.map_get v_value map
  | (Script_typed_ir.IMap_update _ _, k_value, stack_value)
    let 'existT _ [__23, __24] [stack_value, k_value] :=
      cast_exists (Es := [Set ** Set])
        (fun '[__23, __24]
          [option __23 × (Script_typed_ir.map a __23 × __24) ** a])
        [stack_value, k_value] in
    let '(_, (map, _)) := stack_value in
    Interp_costs.map_update k_value map
  | (Script_typed_ir.IMap_get_and_update _ _, k_value, stack_value)
    let 'existT _ [__25, __26] [stack_value, k_value] :=
      cast_exists (Es := [Set ** Set])
        (fun '[__25, __26]
          [option __25 × (Script_typed_ir.map a __25 × __26) ** a])
        [stack_value, k_value] in
    let '(_, (map, _)) := stack_value in
    Interp_costs.map_get_and_update k_value map
  | (Script_typed_ir.IBig_map_get _ _, _, stack_value)
    let 'existT _ __28 stack_value :=
      cast_exists (Es := Set) (fun __28Script_typed_ir.big_map × __28)
        stack_value in
    let '(Script_typed_ir.Big_map map, _) := stack_value in
    Interp_costs.big_map_get map.(Script_typed_ir.big_map.Big_map.diff)
  | (Script_typed_ir.IBig_map_mem _ _, _, stack_value)
    let 'existT _ __30 stack_value :=
      cast_exists (Es := Set) (fun __30Script_typed_ir.big_map × __30)
        stack_value in
    let '(Script_typed_ir.Big_map map, _) := stack_value in
    Interp_costs.big_map_mem map.(Script_typed_ir.big_map.Big_map.diff)
  | (Script_typed_ir.IBig_map_update _ _, _, stack_value)
    let 'existT _ [__31, __32] stack_value :=
      cast_exists (Es := [Set ** Set])
        (fun '[__31, __32]option __31 × (Script_typed_ir.big_map × __32))
        stack_value in
    let '(_, (Script_typed_ir.Big_map map, _)) := stack_value in
    Interp_costs.big_map_update map.(Script_typed_ir.big_map.Big_map.diff)
  | (Script_typed_ir.IBig_map_get_and_update _ _, _, stack_value)
    let 'existT _ [__33, __34] stack_value :=
      cast_exists (Es := [Set ** Set])
        (fun '[__33, __34]option __33 × (Script_typed_ir.big_map × __34))
        stack_value in
    let '(_, (Script_typed_ir.Big_map map, _)) := stack_value in
    Interp_costs.big_map_get_and_update
      map.(Script_typed_ir.big_map.Big_map.diff)
  | (Script_typed_ir.IAdd_seconds_to_timestamp _ _, n_value, stack_value)
    let 'existT _ __35 [stack_value, n_value] :=
      cast_exists (Es := Set)
        (fun __35[Script_timestamp.t × __35 ** Script_int.num])
        [stack_value, n_value] in
    let '(t_value, _) := stack_value in
    Interp_costs.add_seconds_timestamp n_value t_value
  | (Script_typed_ir.IAdd_timestamp_to_seconds _ _, t_value, stack_value)
    let 'existT _ __36 [stack_value, t_value] :=
      cast_exists (Es := Set)
        (fun __36[Script_int.num × __36 ** Script_timestamp.t])
        [stack_value, t_value] in
    let '(n_value, _) := stack_value in
    Interp_costs.add_timestamp_seconds t_value n_value
  | (Script_typed_ir.ISub_timestamp_seconds _ _, t_value, stack_value)
    let 'existT _ __37 [stack_value, t_value] :=
      cast_exists (Es := Set)
        (fun __37[Script_int.num × __37 ** Script_timestamp.t])
        [stack_value, t_value] in
    let '(n_value, _) := stack_value in
    Interp_costs.sub_timestamp_seconds t_value n_value
  | (Script_typed_ir.IDiff_timestamps _ _, t1, stack_value)
    let 'existT _ __38 [stack_value, t1] :=
      cast_exists (Es := Set)
        (fun __38[Script_timestamp.t × __38 ** Script_timestamp.t])
        [stack_value, t1] in
    let '(t2, _) := stack_value in
    Interp_costs.diff_timestamps t1 t2
  | (Script_typed_ir.IConcat_string_pair _ _, x_value, stack_value)
    let 'existT _ __39 [stack_value, x_value] :=
      cast_exists (Es := Set)
        (fun __39[Script_string.t × __39 ** Script_string.t])
        [stack_value, x_value] in
    let '(y_value, _) := stack_value in
    Interp_costs.concat_string_pair x_value y_value
  | (Script_typed_ir.IConcat_string _ _, ss, _)
    let ss := cast (Script_typed_ir.boxed_list Script_string.t) ss in
    Interp_costs.concat_string_precheck ss
  | (Script_typed_ir.ISlice_string _ _, _offset, stack_value)
    let 'existT _ __40 [stack_value, _offset] :=
      cast_exists (Es := Set)
        (fun __40[Script_int.num × (Script_string.t × __40) ** a])
        [stack_value, _offset] in
    let '(_length, (s_value, _)) := stack_value in
    Interp_costs.slice_string s_value
  | (Script_typed_ir.IConcat_bytes_pair _ _, x_value, stack_value)
    let 'existT _ __41 [stack_value, x_value] :=
      cast_exists (Es := Set) (fun __41[bytes × __41 ** bytes])
        [stack_value, x_value] in
    let '(y_value, _) := stack_value in
    Interp_costs.concat_bytes_pair x_value y_value
  | (Script_typed_ir.IConcat_bytes _ _, ss, _)
    let ss := cast (Script_typed_ir.boxed_list bytes) ss in
    Interp_costs.concat_string_precheck ss
  | (Script_typed_ir.ISlice_bytes _ _, _, stack_value)
    let 'existT _ __42 stack_value :=
      cast_exists (Es := Set) (fun __42Script_int.num × (bytes × __42))
        stack_value in
    let '(_, (s_value, _)) := stack_value in
    Interp_costs.slice_bytes s_value
  | (Script_typed_ir.IMul_teznat _ _, _, _)Interp_costs.mul_teznat
  | (Script_typed_ir.IMul_nattez _ _, _, _)Interp_costs.mul_nattez
  | (Script_typed_ir.IAbs_int _ _, x_value, _)
    let x_value := cast Script_int.num x_value in
    Interp_costs.abs_int x_value
  | (Script_typed_ir.INeg _ _, x_value, _)
    let x_value := cast Script_int.num x_value in
    Interp_costs.neg x_value
  | (Script_typed_ir.IAdd_int _ _, x_value, stack_value)
    let 'existT _ __48 [stack_value, x_value] :=
      cast_exists (Es := Set)
        (fun __48[Script_int.num × __48 ** Script_int.num])
        [stack_value, x_value] in
    let '(y_value, _) := stack_value in
    Interp_costs.add_int x_value y_value
  | (Script_typed_ir.IAdd_nat _ _, x_value, stack_value)
    let 'existT _ __49 [stack_value, x_value] :=
      cast_exists (Es := Set)
        (fun __49[Script_int.num × __49 ** Script_int.num])
        [stack_value, x_value] in
    let '(y_value, _) := stack_value in
    Interp_costs.add_nat x_value y_value
  | (Script_typed_ir.ISub_int _ _, x_value, stack_value)
    let 'existT _ __52 [stack_value, x_value] :=
      cast_exists (Es := Set)
        (fun __52[Script_int.num × __52 ** Script_int.num])
        [stack_value, x_value] in
    let '(y_value, _) := stack_value in
    Interp_costs.sub_int x_value y_value
  | (Script_typed_ir.IMul_int _ _, x_value, stack_value)
    let 'existT _ __55 [stack_value, x_value] :=
      cast_exists (Es := Set)
        (fun __55[Script_int.num × __55 ** Script_int.num])
        [stack_value, x_value] in
    let '(y_value, _) := stack_value in
    Interp_costs.mul_int x_value y_value
  | (Script_typed_ir.IMul_nat _ _, x_value, stack_value)
    let 'existT _ __57 [stack_value, x_value] :=
      cast_exists (Es := Set)
        (fun __57[Script_int.num × __57 ** Script_int.num])
        [stack_value, x_value] in
    let '(y_value, _) := stack_value in
    Interp_costs.mul_nat x_value y_value
  | (Script_typed_ir.IEdiv_teznat _ _, x_value, stack_value)
    let 'existT _ __58 [stack_value, x_value] :=
      cast_exists (Es := Set) (fun __58[Script_int.num × __58 ** a])
        [stack_value, x_value] in
    let '(y_value, _) := stack_value in
    Interp_costs.ediv_teznat x_value y_value
  | (Script_typed_ir.IEdiv_int _ _, x_value, stack_value)
    let 'existT _ __61 [stack_value, x_value] :=
      cast_exists (Es := Set)
        (fun __61[Script_int.num × __61 ** Script_int.num])
        [stack_value, x_value] in
    let '(y_value, _) := stack_value in
    Interp_costs.ediv_int x_value y_value
  | (Script_typed_ir.IEdiv_nat _ _, x_value, stack_value)
    let 'existT _ __63 [stack_value, x_value] :=
      cast_exists (Es := Set)
        (fun __63[Script_int.num × __63 ** Script_int.num])
        [stack_value, x_value] in
    let '(y_value, _) := stack_value in
    Interp_costs.ediv_nat x_value y_value
  | (Script_typed_ir.ILsl_nat _ _, x_value, _)
    let x_value := cast Script_int.num x_value in
    Interp_costs.lsl_nat x_value
  | (Script_typed_ir.ILsr_nat _ _, x_value, _)
    let x_value := cast Script_int.num x_value in
    Interp_costs.lsr_nat x_value
  | (Script_typed_ir.IOr_nat _ _, x_value, stack_value)
    let 'existT _ __66 [stack_value, x_value] :=
      cast_exists (Es := Set)
        (fun __66[Script_int.num × __66 ** Script_int.num])
        [stack_value, x_value] in
    let '(y_value, _) := stack_value in
    Interp_costs.or_nat x_value y_value
  | (Script_typed_ir.IAnd_nat _ _, x_value, stack_value)
    let 'existT _ __67 [stack_value, x_value] :=
      cast_exists (Es := Set)
        (fun __67[Script_int.num × __67 ** Script_int.num])
        [stack_value, x_value] in
    let '(y_value, _) := stack_value in
    Interp_costs.and_nat x_value y_value
  | (Script_typed_ir.IAnd_int_nat _ _, x_value, stack_value)
    let 'existT _ __68 [stack_value, x_value] :=
      cast_exists (Es := Set)
        (fun __68[Script_int.num × __68 ** Script_int.num])
        [stack_value, x_value] in
    let '(y_value, _) := stack_value in
    Interp_costs.and_int_nat x_value y_value
  | (Script_typed_ir.IXor_nat _ _, x_value, stack_value)
    let 'existT _ __69 [stack_value, x_value] :=
      cast_exists (Es := Set)
        (fun __69[Script_int.num × __69 ** Script_int.num])
        [stack_value, x_value] in
    let '(y_value, _) := stack_value in
    Interp_costs.xor_nat x_value y_value
  | (Script_typed_ir.INot_int _ _, x_value, _)
    let x_value := cast Script_int.num x_value in
    Interp_costs.not_int x_value
  | (Script_typed_ir.ICompare _ ty_value _, a_value, stack_value)
    let 'existT _ [__71, __72] [stack_value, a_value, ty_value] :=
      cast_exists (Es := [Set ** Set])
        (fun '[__71, __72]
          [a × (__71 × __72) ** a ** Script_typed_ir.comparable_ty])
        [stack_value, a_value, ty_value] in
    let '(b_value, _) := stack_value in
    Interp_costs.compare ty_value a_value b_value
  | (Script_typed_ir.ICheck_signature _ _, key_value, stack_value)
    let 'existT _ __73 [stack_value, key_value] :=
      cast_exists (Es := Set)
        (fun __73
          [Script_typed_ir.signature × (bytes × __73) **
            Alpha_context.public_key]) [stack_value, key_value] in
    let '(_, (message, _)) := stack_value in
    Interp_costs.check_signature key_value message
  | (Script_typed_ir.IHash_key _ _, pk, _)
    let pk := cast Alpha_context.public_key pk in
    Interp_costs.hash_key pk
  | (Script_typed_ir.IBlake2b _ _, bytes_value, _)
    let bytes_value := cast bytes bytes_value in
    Interp_costs.blake2b bytes_value
  | (Script_typed_ir.ISha256 _ _, bytes_value, _)
    let bytes_value := cast bytes bytes_value in
    Interp_costs.sha256 bytes_value
  | (Script_typed_ir.ISha512 _ _, bytes_value, _)
    let bytes_value := cast bytes bytes_value in
    Interp_costs.sha512 bytes_value
  | (Script_typed_ir.IKeccak _ _, bytes_value, _)
    let bytes_value := cast bytes bytes_value in
    Interp_costs.keccak bytes_value
  | (Script_typed_ir.ISha3 _ _, bytes_value, _)
    let bytes_value := cast bytes bytes_value in
    Interp_costs.sha3 bytes_value
  | (Script_typed_ir.IPairing_check_bls12_381 _ _, pairs, _)
    let pairs :=
      cast
        (Script_typed_ir.boxed_list
          (Script_typed_ir.pair
            Script_typed_ir.Script_bls.G1.(Script_typed_ir.Script_bls.S.t)
            Script_typed_ir.Script_bls.G2.(Script_typed_ir.Script_bls.S.t)))
        pairs in
    Interp_costs.pairing_check_bls12_381 pairs
  | (Script_typed_ir.ISapling_verify_update _ _, accu_value, _)
    let accu_value := cast Sapling_repr.transaction accu_value in
    let tx := accu_value in
    let inputs := Gas_input_size.sapling_transaction_inputs tx in
    let outputs := Gas_input_size.sapling_transaction_outputs tx in
    let bound_data := Gas_input_size.sapling_transaction_bound_data tx in
    Interp_costs.sapling_verify_update inputs outputs bound_data
  | (Script_typed_ir.ISapling_verify_update_deprecated _ _, accu_value, _)
    let accu_value := cast Sapling_repr.legacy_transaction accu_value in
    let tx := accu_value in
    let inputs := List.length tx.(Sapling.UTXO.Legacy.transaction.inputs) in
    let outputs := List.length tx.(Sapling.UTXO.Legacy.transaction.outputs) in
    Interp_costs.sapling_verify_update_deprecated inputs outputs
  | (Script_typed_ir.ISplit_ticket _ _, accu_value, stack_value)
    let 'existT _ [__77, __76] [stack_value, accu_value] :=
      cast_exists (Es := [Set ** Set])
        (fun '[__77, __76]
          [(Script_int.num × Script_int.num) × __77 **
            Script_typed_ir.ticket __76]) [stack_value, accu_value] in
    let ticket := accu_value in
    let '((amount_a, amount_b), _) := stack_value in
    Interp_costs.split_ticket ticket.(Script_typed_ir.ticket.amount) amount_a
      amount_b
  | (Script_typed_ir.IJoin_tickets _ ty_value _, ticket_a_b, _)
    let 'existT _ __78 [ticket_a_b, ty_value] :=
      cast_exists (Es := Set)
        (fun __78
          [Script_typed_ir.ticket __78 × Script_typed_ir.ticket __78 **
            Script_typed_ir.comparable_ty]) [ticket_a_b, ty_value] in
    let '(ticket_a, ticket_b) := ticket_a_b in
    Interp_costs.join_tickets ty_value ticket_a ticket_b
  | (Script_typed_ir.IHalt _, _, _)Interp_costs.halt
  | (Script_typed_ir.IDrop _ _, _, _)Interp_costs.drop
  | (Script_typed_ir.IDup _ _, _, _)Interp_costs.dup
  | (Script_typed_ir.ISwap _ _, _, _)Interp_costs.swap
  | (Script_typed_ir.IConst _ _ _ _, _, _)Interp_costs.const
  | (Script_typed_ir.ICons_some _ _, _, _)Interp_costs.cons_some
  | (Script_typed_ir.ICons_none _ _ _, _, _)Interp_costs.cons_none
  | (Script_typed_ir.IIf_none _, _, _)Interp_costs.if_none
  | (Script_typed_ir.IOpt_map _, _, _)Interp_costs.opt_map
  | (Script_typed_ir.ICons_pair _ _, _, _)Interp_costs.cons_pair
  | (Script_typed_ir.IUnpair _ _, _, _)Interp_costs.unpair
  | (Script_typed_ir.ICar _ _, _, _)Interp_costs.car
  | (Script_typed_ir.ICdr _ _, _, _)Interp_costs.cdr
  | (Script_typed_ir.ICons_left _ _ _, _, _)Interp_costs.cons_left
  | (Script_typed_ir.ICons_right _ _ _, _, _)Interp_costs.cons_right
  | (Script_typed_ir.IIf_left _, _, _)Interp_costs.if_left
  | (Script_typed_ir.ICons_list _ _, _, _)Interp_costs.cons_list
  | (Script_typed_ir.INil _ _ _, _, _)Interp_costs.nil
  | (Script_typed_ir.IIf_cons _, _, _)Interp_costs.if_cons
  | (Script_typed_ir.IList_size _ _, _, _)Interp_costs.list_size
  | (Script_typed_ir.IEmpty_set _ _ _, _, _)Interp_costs.empty_set
  | (Script_typed_ir.ISet_size _ _, _, _)Interp_costs.set_size
  | (Script_typed_ir.IEmpty_map _ _ _ _, _, _)Interp_costs.empty_map
  | (Script_typed_ir.IMap_size _ _, _, _)Interp_costs.map_size
  | (Script_typed_ir.IEmpty_big_map _ _ _ _, _, _)Interp_costs.empty_big_map
  | (Script_typed_ir.IString_size _ _, _, _)Interp_costs.string_size
  | (Script_typed_ir.IBytes_size _ _, _, _)Interp_costs.bytes_size
  | (Script_typed_ir.IAdd_tez _ _, _, _)Interp_costs.add_tez
  | (Script_typed_ir.ISub_tez _ _, _, _)Interp_costs.sub_tez
  | (Script_typed_ir.ISub_tez_legacy _ _, _, _)Interp_costs.sub_tez_legacy
  | (Script_typed_ir.IOr _ _, _, _)Interp_costs.bool_or
  | (Script_typed_ir.IAnd _ _, _, _)Interp_costs.bool_and
  | (Script_typed_ir.IXor _ _, _, _)Interp_costs.bool_xor
  | (Script_typed_ir.INot _ _, _, _)Interp_costs.bool_not
  | (Script_typed_ir.IIs_nat _ _, _, _)Interp_costs.is_nat
  | (Script_typed_ir.IInt_nat _ _, _, _)Interp_costs.int_nat
  | (Script_typed_ir.IInt_bls12_381_fr _ _, _, _)
    Interp_costs.int_bls12_381_fr
  | (Script_typed_ir.IEdiv_tez _ _, _, _)Interp_costs.ediv_tez
  | (Script_typed_ir.IIf _, _, _)Interp_costs.if_
  | (Script_typed_ir.ILoop _ _ _, _, _)Interp_costs.loop
  | (Script_typed_ir.ILoop_left _ _ _, _, _)Interp_costs.loop_left
  | (Script_typed_ir.IDip _ _ _ _, _, _)Interp_costs.dip
  | (Script_typed_ir.IExec _ _ _, _, _)Interp_costs.exec
  | (Script_typed_ir.IApply _ _ _, _, stack_value)
    let 'existT _ __134 stack_value :=
      cast_exists (Es := Set) (fun __134Script_typed_ir.lambda × __134)
        stack_value in
    let '(l_value, _) := stack_value in
    match l_value with
    | Script_typed_ir.Lam _ _Interp_costs.apply false
    | Script_typed_ir.LamRec _ _Interp_costs.apply true
    end
  | (Script_typed_ir.ILambda _ _ _, _, _)Interp_costs.lambda
  | (Script_typed_ir.IFailwith _ _, _, _)Alpha_context.Gas.free
  | (Script_typed_ir.IEq _ _, _, _)Interp_costs.eq_value
  | (Script_typed_ir.INeq _ _, _, _)Interp_costs.neq
  | (Script_typed_ir.ILt _ _, _, _)Interp_costs.lt
  | (Script_typed_ir.ILe _ _, _, _)Interp_costs.le
  | (Script_typed_ir.IGt _ _, _, _)Interp_costs.gt
  | (Script_typed_ir.IGe _ _, _, _)Interp_costs.ge
  | (Script_typed_ir.IPack _ _ _, _, _)Alpha_context.Gas.free
  | (Script_typed_ir.IUnpack _ _ _, accu_value, _)
    let accu_value := cast bytes accu_value in
    let b_value := accu_value in
    Interp_costs.unpack b_value
  | (Script_typed_ir.IAddress _ _, _, _)Interp_costs.address
  | (Script_typed_ir.IContract _ _ _ _, _, _)Interp_costs.contract
  | (Script_typed_ir.ITransfer_tokens _ _, _, _)Interp_costs.transfer_tokens
  | (Script_typed_ir.IView _ _ _ _, _, _)Interp_costs.view
  | (Script_typed_ir.IImplicit_account _ _, _, _)
    Interp_costs.implicit_account
  | (Script_typed_ir.ISet_delegate _ _, _, _)Interp_costs.set_delegate
  | (Script_typed_ir.IBalance _ _, _, _)Interp_costs.balance
  | (Script_typed_ir.ILevel _ _, _, _)Interp_costs.level
  | (Script_typed_ir.INow _ _, _, _)Interp_costs.now
  | (Script_typed_ir.IMin_block_time _ _, _, _)Interp_costs.min_block_time
  | (Script_typed_ir.ISapling_empty_state _ _ _, _, _)
    Interp_costs.sapling_empty_state
  | (Script_typed_ir.ISource _ _, _, _)Interp_costs.source
  | (Script_typed_ir.ISender _ _, _, _)Interp_costs.sender
  | (Script_typed_ir.ISelf _ _ _ _, _, _)Interp_costs.self
  | (Script_typed_ir.ISelf_address _ _, _, _)Interp_costs.self_address
  | (Script_typed_ir.IAmount _ _, _, _)Interp_costs.amount
  | (Script_typed_ir.IDig _ n_value _ _, _, _)
    let n_value := cast int n_value in
    Interp_costs.dign n_value
  | (Script_typed_ir.IDug _ n_value _ _, _, _)
    let n_value := cast int n_value in
    Interp_costs.dugn n_value
  | (Script_typed_ir.IDipn _ n_value _ _ _, _, _)
    let n_value := cast int n_value in
    Interp_costs.dipn n_value
  | (Script_typed_ir.IDropn _ n_value _ _, _, _)
    let n_value := cast int n_value in
    Interp_costs.dropn n_value
  | (Script_typed_ir.IChainId _ _, _, _)Interp_costs.chain_id
  | (Script_typed_ir.ICreate_contract _, _, _)Interp_costs.create_contract
  | (Script_typed_ir.IVoting_power _ _, _, _)Interp_costs.voting_power
  | (Script_typed_ir.ITotal_voting_power _ _, _, _)
    Interp_costs.total_voting_power
  | (Script_typed_ir.IAdd_bls12_381_g1 _ _, _, _)
    Interp_costs.add_bls12_381_g1
  | (Script_typed_ir.IAdd_bls12_381_g2 _ _, _, _)
    Interp_costs.add_bls12_381_g2
  | (Script_typed_ir.IAdd_bls12_381_fr _ _, _, _)
    Interp_costs.add_bls12_381_fr
  | (Script_typed_ir.IMul_bls12_381_g1 _ _, _, _)
    Interp_costs.mul_bls12_381_g1
  | (Script_typed_ir.IMul_bls12_381_g2 _ _, _, _)
    Interp_costs.mul_bls12_381_g2
  | (Script_typed_ir.IMul_bls12_381_fr _ _, _, _)
    Interp_costs.mul_bls12_381_fr
  | (Script_typed_ir.INeg_bls12_381_g1 _ _, _, _)
    Interp_costs.neg_bls12_381_g1
  | (Script_typed_ir.INeg_bls12_381_g2 _ _, _, _)
    Interp_costs.neg_bls12_381_g2
  | (Script_typed_ir.INeg_bls12_381_fr _ _, _, _)
    Interp_costs.neg_bls12_381_fr
  | (Script_typed_ir.IMul_bls12_381_fr_z _ _, accu_value, _)
    let accu_value := cast Script_int.num accu_value in
    let z_value := accu_value in
    Interp_costs.mul_bls12_381_fr_z z_value
  | (Script_typed_ir.IMul_bls12_381_z_fr _ _, _, stack_value)
    let 'existT _ __155 stack_value :=
      cast_exists (Es := Set) (fun __155Script_int.num × __155) stack_value
      in
    let '(z_value, _) := stack_value in
    Interp_costs.mul_bls12_381_z_fr z_value
  | (Script_typed_ir.IDup_n _ n_value _ _, _, _)
    let n_value := cast int n_value in
    Interp_costs.dupn n_value
  | (Script_typed_ir.IComb _ n_value _ _, _, _)
    let n_value := cast int n_value in
    Interp_costs.comb n_value
  | (Script_typed_ir.IUncomb _ n_value _ _, _, _)
    let n_value := cast int n_value in
    Interp_costs.uncomb n_value
  | (Script_typed_ir.IComb_get _ n_value _ _, _, _)
    let n_value := cast int n_value in
    Interp_costs.comb_get n_value
  | (Script_typed_ir.IComb_set _ n_value _ _, _, _)
    let n_value := cast int n_value in
    Interp_costs.comb_set n_value
  |
    ((Script_typed_ir.ITicket _ _ _ | Script_typed_ir.ITicket_deprecated _ _ _),
      _, _)Interp_costs.ticket
  | (Script_typed_ir.IRead_ticket _ _ _, _, _)Interp_costs.read_ticket
  | (Script_typed_ir.IOpen_chest _ _, _, stack_value)
    let 'existT _ __170 stack_value :=
      cast_exists (Es := Set)
        (fun __170
          Script_typed_ir.Script_timelock.chest × (Script_int.num × __170))
        stack_value in
    let _chest_key := accu_value in
    let '(chest_value, (time, _)) := stack_value in
    Interp_costs.open_chest chest_value (Script_int.to_zint time)
  | (Script_typed_ir.IEmit _, _, _)Interp_costs.emit
  | (Script_typed_ir.ILog _ _ _ _ _, _, _)Alpha_context.Gas.free
  | _unreachable_gadt_branch
  end.

Definition cost_of_control (ks : Script_typed_ir.continuation)
  : Alpha_context.Gas.cost :=
  match ks with
  | Script_typed_ir.KLog _ _ _Alpha_context.Gas.free
  | Script_typed_ir.KNilInterp_costs.Control.nil
  | Script_typed_ir.KCons _ _Interp_costs.Control.cons_value
  | Script_typed_ir.KReturn _ _ _Interp_costs.Control._return
  | Script_typed_ir.KMap_head _ _Interp_costs.Control.map_head
  | Script_typed_ir.KUndip _ _ _Interp_costs.Control.undip
  | Script_typed_ir.KLoop_in _ _Interp_costs.Control.loop_in
  | Script_typed_ir.KLoop_in_left _ _Interp_costs.Control.loop_in_left
  | Script_typed_ir.KIter _ _ _ _Interp_costs.Control.iter
  | Script_typed_ir.KList_enter_body _ xs _ _ len _
    Interp_costs.Control.list_enter_body xs len
  | Script_typed_ir.KList_exit_body _ _ _ _ _ _
    Interp_costs.Control.list_exit_body
  | Script_typed_ir.KMap_enter_body _ _ _ _ _
    Interp_costs.Control.map_enter_body
  | Script_typed_ir.KMap_exit_body _ _ map key_value _ _
    Interp_costs.Control.map_exit_body key_value map
  | Script_typed_ir.KView_exit _ _Interp_costs.Control.view_exit
  end.

Definition consume_instr {A B : Set}
  (local_gas_counter_value : Local_gas_counter.local_gas_counter)
  (k_value : Script_typed_ir.kinstr) (accu_value : A) (stack_value : B)
  : option Local_gas_counter.local_gas_counter :=
  let cost := cost_of_instr k_value accu_value stack_value in
  Local_gas_counter.consume_opt local_gas_counter_value cost.

Definition consume_control
  (local_gas_counter_value : Local_gas_counter.local_gas_counter)
  (ks : Script_typed_ir.continuation)
  : option Local_gas_counter.local_gas_counter :=
  let cost := cost_of_control ks in
  Local_gas_counter.consume_opt local_gas_counter_value cost.

Definition get_log (function_parameter : option Script_typed_ir.logger)
  : M? (option Script_typed_ir.execution_trace) :=
  match function_parameter with
  | NonePervasives.Ok None
  | Some loggerlogger.(Script_typed_ir.logger.get_log) tt
  end.

#[bypass_check(guard)]
Fixpoint kundip {c u a s : Set}
  (w_value : Script_typed_ir.stack_prefix_preservation_witness) (accu_value : c)
  (stack_value : u) (k_value : Script_typed_ir.kinstr) {struct w_value}
  : a × s × Script_typed_ir.kinstr :=
  match (w_value, accu_value, stack_value) with
  | (Script_typed_ir.KPrefix loc_value ty_value w_value, _, stack_value)
    let 'existT _ [__0, __1] [stack_value, w_value, ty_value, loc_value] :=
      cast_exists (Es := [Set ** Set])
        (fun '[__0, __1]
          [__0 × __1 ** Script_typed_ir.stack_prefix_preservation_witness **
            Script_typed_ir.ty ** Alpha_context.Script.location])
        [stack_value, w_value, ty_value, loc_value] in
    let k_value := Script_typed_ir.IConst loc_value ty_value accu_value k_value
      in
    let '(accu_value, stack_value) := stack_value in
    kundip w_value accu_value stack_value k_value
  | (Script_typed_ir.KRest, accu_value, stack_value)
    let '[stack_value, accu_value] := cast [s ** a] [stack_value, accu_value] in
    (accu_value, stack_value, k_value)
  end.

Definition apply {A : Set}
  (ctxt : Local_gas_counter.outdated_context)
  (gas : Local_gas_counter.local_gas_counter) (capture_ty : Script_typed_ir.ty)
  (capture : A) (lam : Script_typed_ir.lambda)
  : M?
    (Script_typed_ir.lambda × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter) :=
  let loc_value := Micheline.dummy_location in
  let ctxt := Local_gas_counter.update_context gas ctxt in
  let? '(ty_expr, ctxt) :=
    Script_ir_unparser.unparse_ty loc_value ctxt capture_ty in
  let? '(const_expr, ctxt) :=
    Script_ir_translator.unparse_data ctxt Script_ir_unparser.Optimized
      capture_ty capture in
  let make_expr
    (expr :
      list
        (Micheline.node Micheline.canonical_location Alpha_context.Script.prim))
    : Micheline.node Micheline.canonical_location Alpha_context.Script.prim :=
    Micheline.Seq loc_value
      (cons
        (Micheline.Prim loc_value Michelson_v1_primitives.I_PUSH
          [ ty_expr; Micheline.root_value const_expr ] nil)
        (cons (Micheline.Prim loc_value Michelson_v1_primitives.I_PAIR nil nil)
          expr)) in
  let lam' :=
    match lam with
    | Script_typed_ir.LamRec descr_value expr
      match
        (descr_value.(Script_typed_ir.kdescr.kbef),
          descr_value.(Script_typed_ir.kdescr.kaft)) with
      |
        (Script_typed_ir.Item_t full_arg_ty
          (Script_typed_ir.Item_t (Script_typed_ir.Lambda_t _ _ _)
            Script_typed_ir.Bot_t),
          Script_typed_ir.Item_t ret_ty Script_typed_ir.Bot_t)
        let? '(arg_ty_expr, ctxt) :=
          Script_ir_unparser.unparse_ty loc_value ctxt full_arg_ty in
        let? '(ret_ty_expr, ctxt) :=
          Script_ir_unparser.unparse_ty loc_value ctxt ret_ty in
        match full_arg_ty with
        | Script_typed_ir.Pair_t capture_ty arg_ty _ _
          let arg_stack_ty :=
            Script_typed_ir.Item_t arg_ty Script_typed_ir.Bot_t in
          let full_descr :=
            {|
              Script_typed_ir.kdescr.kloc :=
                descr_value.(Script_typed_ir.kdescr.kloc);
              Script_typed_ir.kdescr.kbef := arg_stack_ty;
              Script_typed_ir.kdescr.kaft :=
                descr_value.(Script_typed_ir.kdescr.kaft);
              Script_typed_ir.kdescr.kinstr :=
                Script_typed_ir.IConst descr_value.(Script_typed_ir.kdescr.kloc)
                  capture_ty capture
                  (Script_typed_ir.ICons_pair
                    descr_value.(Script_typed_ir.kdescr.kloc)
                    (Script_typed_ir.ILambda
                      descr_value.(Script_typed_ir.kdescr.kloc) lam
                      (Script_typed_ir.ISwap
                        descr_value.(Script_typed_ir.kdescr.kloc)
                        (Script_typed_ir.IExec
                          descr_value.(Script_typed_ir.kdescr.kloc)
                          (Some descr_value.(Script_typed_ir.kdescr.kaft))
                          (Script_typed_ir.IHalt
                            descr_value.(Script_typed_ir.kdescr.kloc)))))); |}
            in
          let full_expr :=
            make_expr
              [
                Micheline.Prim loc_value Michelson_v1_primitives.I_LAMBDA_REC
                  [ arg_ty_expr; ret_ty_expr; expr ] nil;
                Micheline.Prim loc_value Michelson_v1_primitives.I_SWAP nil nil;
                Micheline.Prim loc_value Michelson_v1_primitives.I_EXEC nil nil
              ] in
          return? ((Script_typed_ir.Lam full_descr full_expr), ctxt)
        | _unreachable_gadt_branch
        end
      | _unreachable_gadt_branch
      end
    | Script_typed_ir.Lam descr_value expr
      match descr_value.(Script_typed_ir.kdescr.kbef) with
      | Script_typed_ir.Item_t full_arg_ty Script_typed_ir.Bot_t
        match full_arg_ty with
        | Script_typed_ir.Pair_t capture_ty arg_ty _ _
          let arg_stack_ty :=
            Script_typed_ir.Item_t arg_ty Script_typed_ir.Bot_t in
          let full_descr :=
            {|
              Script_typed_ir.kdescr.kloc :=
                descr_value.(Script_typed_ir.kdescr.kloc);
              Script_typed_ir.kdescr.kbef := arg_stack_ty;
              Script_typed_ir.kdescr.kaft :=
                descr_value.(Script_typed_ir.kdescr.kaft);
              Script_typed_ir.kdescr.kinstr :=
                Script_typed_ir.IConst descr_value.(Script_typed_ir.kdescr.kloc)
                  capture_ty capture
                  (Script_typed_ir.ICons_pair
                    descr_value.(Script_typed_ir.kdescr.kloc)
                    descr_value.(Script_typed_ir.kdescr.kinstr)); |} in
          let full_expr := make_expr [ expr ] in
          return? ((Script_typed_ir.Lam full_descr full_expr), ctxt)
        | _unreachable_gadt_branch
        end
      | _unreachable_gadt_branch
      end
    end in
  let? '(lam', ctxt) := lam' in
  let '(gas, ctxt) :=
    Local_gas_counter.local_gas_counter_and_outdated_context ctxt in
  return? (lam', ctxt, gas).

Definition make_transaction_to_tx_rollup {t : Set}
  (ctxt : Alpha_context.context) (destination : Alpha_context.Tx_rollup.t)
  (amount : Alpha_context.Tez.t) (parameters_ty : Script_typed_ir.ty)
  (parameters :
    Script_typed_ir.pair (Script_typed_ir.ticket t)
      Script_typed_ir.tx_rollup_l2_address)
  : M? (Script_typed_ir.internal_operation_contents × Alpha_context.context) :=
  let? '_ :=
    Error_monad.error_unless
      (Alpha_context.Tez.op_eq amount Alpha_context.Tez.zero)
      (Build_extensible "Rollup_invalid_transaction_amount" unit tt) in
  match parameters_ty with
  | Script_typed_ir.Pair_t (Script_typed_ir.Ticket_t tp _) _ _ _
    let? '(unparsed_parameters, ctxt) :=
      Script_ir_translator.unparse_data ctxt Script_ir_unparser.Optimized
        parameters_ty parameters in
    let? '(ty_value, ctxt) :=
      Script_ir_unparser.unparse_ty Micheline.dummy_location ctxt tp in
    let unparsed_parameters :=
      Micheline.Seq Micheline.dummy_location
        [ Micheline.root_value unparsed_parameters; ty_value ] in
    let? ctxt :=
      Alpha_context.Gas.consume ctxt
        (Alpha_context.Script.strip_locations_cost unparsed_parameters) in
    let unparsed_parameters := Micheline.strip_locations unparsed_parameters in
    return?
      ((Script_typed_ir.Transaction_to_tx_rollup
        {|
          Script_typed_ir.internal_operation_contents.Transaction_to_tx_rollup.destination
            := destination;
          Script_typed_ir.internal_operation_contents.Transaction_to_tx_rollup.parameters_ty
            := parameters_ty;
          Script_typed_ir.internal_operation_contents.Transaction_to_tx_rollup.parameters
            := parameters;
          Script_typed_ir.internal_operation_contents.Transaction_to_tx_rollup.unparsed_parameters
            := unparsed_parameters; |}), ctxt)
  | _unreachable_gadt_branch
  end.

Definition make_transaction_to_sc_rollup {A : Set}
  (ctxt : Alpha_context.context) (destination : Alpha_context.Sc_rollup.t)
  (amount : Alpha_context.Tez.t) (entrypoint : Alpha_context.Entrypoint.t)
  (parameters_ty : Script_typed_ir.ty) (parameters : A)
  : M? (Script_typed_ir.internal_operation_contents × Alpha_context.context) :=
  let? '_ :=
    Error_monad.error_unless
      (Alpha_context.Tez.op_eq amount Alpha_context.Tez.zero)
      (Build_extensible "Rollup_invalid_transaction_amount" unit tt) in
  let? '(unparsed_parameters, ctxt) :=
    Script_ir_translator.unparse_data ctxt Script_ir_unparser.Optimized
      parameters_ty parameters in
  return?
    ((Script_typed_ir.Transaction_to_sc_rollup
      {|
        Script_typed_ir.internal_operation_contents.Transaction_to_sc_rollup.destination
          := destination;
        Script_typed_ir.internal_operation_contents.Transaction_to_sc_rollup.entrypoint
          := entrypoint;
        Script_typed_ir.internal_operation_contents.Transaction_to_sc_rollup.parameters_ty
          := parameters_ty;
        Script_typed_ir.internal_operation_contents.Transaction_to_sc_rollup.parameters
          := parameters;
        Script_typed_ir.internal_operation_contents.Transaction_to_sc_rollup.unparsed_parameters
          := unparsed_parameters; |}), ctxt).

[emit_event] generates an internal operation that will effect an event emission if the contract code returns this successfully.
Definition emit_event {t : Set}
  (function_parameter :
    Local_gas_counter.outdated_context × Script_typed_ir.step_constants)
  : Local_gas_counter.local_gas_counter Script_typed_ir.ty
  Alpha_context.Script.expr Alpha_context.Entrypoint.t t
  M?
    (Script_typed_ir.operation × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter) :=
  let '(ctxt, sc) := function_parameter in
  fun (gas : Local_gas_counter.local_gas_counter) ⇒
    fun (event_type : Script_typed_ir.ty) ⇒
      fun (unparsed_ty : Alpha_context.Script.expr) ⇒
        fun (tag : Alpha_context.Entrypoint.t) ⇒
          fun (event_data : t) ⇒
            let ctxt := Local_gas_counter.update_context gas ctxt in
            let lazy_storage_diff {B : Set} : option B :=
              None in
            let? '(unparsed_data, ctxt) :=
              Script_ir_translator.unparse_data ctxt
                Script_ir_unparser.Optimized event_type event_data in
            let? '(ctxt, nonce_value) := Alpha_context.fresh_internal_nonce ctxt
              in
            let operation :=
              Script_typed_ir.Event
                {|
                  Script_typed_ir.internal_operation_contents.Event.ty :=
                    unparsed_ty;
                  Script_typed_ir.internal_operation_contents.Event.tag := tag;
                  Script_typed_ir.internal_operation_contents.Event.unparsed_data
                    := unparsed_data; |} in
            let iop :=
              {|
                Script_typed_ir.internal_operation.source :=
                  Contract_repr.Originated
                    sc.(Script_typed_ir.step_constants.self);
                Script_typed_ir.internal_operation.operation := operation;
                Script_typed_ir.internal_operation.nonce := nonce_value; |} in
            let res :=
              {|
                Script_typed_ir.operation.piop :=
                  Script_typed_ir.Internal_operation iop;
                Script_typed_ir.operation.lazy_storage_diff :=
                  lazy_storage_diff; |} in
            let '(gas, ctxt) :=
              Local_gas_counter.local_gas_counter_and_outdated_context ctxt in
            return? (res, ctxt, gas).

Definition make_transaction_to_zk_rollup {t : Set}
  (ctxt : Alpha_context.context) (destination : Alpha_context.Zk_rollup.t)
  (amount : Alpha_context.Tez.t) (parameters_ty : Script_typed_ir.ty)
  (parameters : Script_typed_ir.pair (Script_typed_ir.ticket t) bytes)
  : M? (Script_typed_ir.internal_operation_contents × Alpha_context.context) :=
  let? '_ :=
    Error_monad.error_unless
      (Alpha_context.Tez.op_eq amount Alpha_context.Tez.zero)
      (Build_extensible "Rollup_invalid_transaction_amount" unit tt) in
  let? '(unparsed_parameters, ctxt) :=
    Script_ir_translator.unparse_data ctxt Script_ir_unparser.Optimized
      parameters_ty parameters in
  return?
    ((Script_typed_ir.Transaction_to_zk_rollup
      {|
        Script_typed_ir.internal_operation_contents.Transaction_to_zk_rollup.destination
          := destination;
        Script_typed_ir.internal_operation_contents.Transaction_to_zk_rollup.parameters_ty
          := parameters_ty;
        Script_typed_ir.internal_operation_contents.Transaction_to_zk_rollup.parameters
          := parameters;
        Script_typed_ir.internal_operation_contents.Transaction_to_zk_rollup.unparsed_parameters
          := unparsed_parameters; |}), ctxt).

Definition transfer {t : Set}
  (function_parameter :
    Local_gas_counter.outdated_context × Script_typed_ir.step_constants)
  : Local_gas_counter.local_gas_counter Alpha_context.Tez.tez
  Alpha_context.Script.location Script_typed_ir.typed_contract t
  M?
    (Script_typed_ir.operation × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter) :=
  let '(ctxt, sc) := function_parameter in
  fun (gas : Local_gas_counter.local_gas_counter) ⇒
    fun (amount : Alpha_context.Tez.tez) ⇒
      fun (location : Alpha_context.Script.location) ⇒
        fun (typed_contract : Script_typed_ir.typed_contract) ⇒
          fun (parameters : t) ⇒
            let ctxt := Local_gas_counter.update_context gas ctxt in
            let? '(operation, lazy_storage_diff, ctxt) :=
              match (typed_contract, parameters) with
              | (Script_typed_ir.Typed_implicit destination, parameters)
                let '[parameters, destination] :=
                  cast [unit ** Alpha_context.public_key_hash]
                    [parameters, destination] in
                let '_ := parameters in
                return?
                  ((Script_typed_ir.Transaction_to_implicit
                    {|
                      Script_typed_ir.internal_operation_contents.Transaction_to_implicit.destination
                        := destination;
                      Script_typed_ir.internal_operation_contents.Transaction_to_implicit.amount
                        := amount; |}), None, ctxt)
              |
                (Script_typed_ir.Typed_originated {|
                  Script_typed_ir.typed_contract.Typed_originated.arg_ty := parameters_ty;
                    Script_typed_ir.typed_contract.Typed_originated.contract_hash
                      := destination;
                    Script_typed_ir.typed_contract.Typed_originated.entrypoint
                      := entrypoint
                    |}, _)
                let '[entrypoint, destination, parameters_ty] :=
                  cast
                    [Alpha_context.Entrypoint.t ** Contract_hash.t **
                      Script_typed_ir.ty]
                    [entrypoint, destination, parameters_ty] in
                let? '(to_duplicate, ctxt) :=
                  Script_ir_translator.collect_lazy_storage ctxt parameters_ty
                    parameters in
                let to_update := Script_ir_translator.no_lazy_storage_id in
                let? '(parameters, lazy_storage_diff, ctxt) :=
                  Script_ir_translator.extract_lazy_storage_diff ctxt
                    Script_ir_unparser.Optimized true to_duplicate to_update
                    parameters_ty parameters in
                let? '(unparsed_parameters, ctxt) :=
                  Script_ir_translator.unparse_data ctxt
                    Script_ir_unparser.Optimized parameters_ty parameters in
                return?
                  ((Script_typed_ir.Transaction_to_smart_contract
                    {|
                      Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.destination
                        := destination;
                      Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.amount
                        := amount;
                      Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.entrypoint
                        := entrypoint;
                      Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.location
                        := location;
                      Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.parameters_ty
                        := parameters_ty;
                      Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.parameters
                        := parameters;
                      Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.unparsed_parameters
                        := unparsed_parameters; |}), lazy_storage_diff, ctxt)
              |
                (Script_typed_ir.Typed_tx_rollup {|
                  Script_typed_ir.typed_contract.Typed_tx_rollup.arg_ty := parameters_ty;
                    Script_typed_ir.typed_contract.Typed_tx_rollup.tx_rollup :=
                      destination
                    |}, parameters)
                let 'existT _ __0 [parameters, destination, parameters_ty] :=
                  cast_exists (Es := Set)
                    (fun __0
                      [Script_typed_ir.pair (Script_typed_ir.ticket __0)
                        Script_typed_ir.tx_rollup_l2_address **
                        Alpha_context.Tx_rollup.t ** Script_typed_ir.ty])
                    [parameters, destination, parameters_ty] in
                let? '(operation, ctxt) :=
                  make_transaction_to_tx_rollup ctxt destination amount
                    parameters_ty parameters in
                return? (operation, None, ctxt)
              |
                (Script_typed_ir.Typed_sc_rollup {|
                  Script_typed_ir.typed_contract.Typed_sc_rollup.arg_ty := parameters_ty;
                    Script_typed_ir.typed_contract.Typed_sc_rollup.sc_rollup :=
                      destination;
                    Script_typed_ir.typed_contract.Typed_sc_rollup.entrypoint :=
                      entrypoint
                    |}, _)
                let '[entrypoint, destination, parameters_ty] :=
                  cast
                    [Alpha_context.Entrypoint.t ** Alpha_context.Sc_rollup.t **
                      Script_typed_ir.ty]
                    [entrypoint, destination, parameters_ty] in
                let? '(operation, ctxt) :=
                  make_transaction_to_sc_rollup ctxt destination amount
                    entrypoint parameters_ty parameters in
                return? (operation, None, ctxt)
              |
                (Script_typed_ir.Typed_zk_rollup {|
                  Script_typed_ir.typed_contract.Typed_zk_rollup.arg_ty := parameters_ty;
                    Script_typed_ir.typed_contract.Typed_zk_rollup.zk_rollup :=
                      destination
                    |}, parameters)
                let 'existT _ __1 [parameters, destination, parameters_ty] :=
                  cast_exists (Es := Set)
                    (fun __1
                      [Script_typed_ir.ticket __1 × bytes **
                        Alpha_context.Zk_rollup.t ** Script_typed_ir.ty])
                    [parameters, destination, parameters_ty] in
                let? '(operation, ctxt) :=
                  make_transaction_to_zk_rollup ctxt destination amount
                    parameters_ty parameters in
                return? (operation, None, ctxt)
              end in
            let? '(ctxt, nonce_value) := Alpha_context.fresh_internal_nonce ctxt
              in
            let iop :=
              {|
                Script_typed_ir.internal_operation.source :=
                  Contract_repr.Originated
                    sc.(Script_typed_ir.step_constants.self);
                Script_typed_ir.internal_operation.operation := operation;
                Script_typed_ir.internal_operation.nonce := nonce_value; |} in
            let res :=
              {|
                Script_typed_ir.operation.piop :=
                  Script_typed_ir.Internal_operation iop;
                Script_typed_ir.operation.lazy_storage_diff :=
                  lazy_storage_diff; |} in
            let '(gas, ctxt) :=
              Local_gas_counter.local_gas_counter_and_outdated_context ctxt in
            return? (res, ctxt, gas).

[create_contract (ctxt, sc) gas storage_ty code delegate credit init] creates an origination operation for a contract represented by [code], some initial [credit] (withdrawn from the contract being executed), and an initial storage [init] of type [storage_ty].
Definition create_contract {A : Set}
  (function_parameter :
    Local_gas_counter.outdated_context × Script_typed_ir.step_constants)
  : Local_gas_counter.local_gas_counter Script_typed_ir.ty
  Alpha_context.Script.expr option Signature.public_key_hash
  Alpha_context.Tez.tez A
  M?
    (Script_typed_ir.operation × Contract_hash.t ×
      Local_gas_counter.outdated_context × Local_gas_counter.local_gas_counter) :=
  let '(ctxt, sc) := function_parameter in
  fun (gas : Local_gas_counter.local_gas_counter) ⇒
    fun (storage_type : Script_typed_ir.ty) ⇒
      fun (code : Alpha_context.Script.expr) ⇒
        fun (delegate : option Signature.public_key_hash) ⇒
          fun (credit : Alpha_context.Tez.tez) ⇒
            fun (init_value : A) ⇒
              let ctxt := Local_gas_counter.update_context gas ctxt in
              let? '(to_duplicate, ctxt) :=
                Script_ir_translator.collect_lazy_storage ctxt storage_type
                  init_value in
              let to_update := Script_ir_translator.no_lazy_storage_id in
              let? '(init_value, lazy_storage_diff, ctxt) :=
                Script_ir_translator.extract_lazy_storage_diff ctxt
                  Script_ir_unparser.Optimized true to_duplicate to_update
                  storage_type init_value in
              let? '(unparsed_storage, ctxt) :=
                Script_ir_translator.unparse_data ctxt
                  Script_ir_unparser.Optimized storage_type init_value in
              let? '(ctxt, preorigination) :=
                Alpha_context.Contract.fresh_contract_from_current_nonce ctxt in
              let operation :=
                Script_typed_ir.Origination
                  {|
                    Script_typed_ir.internal_operation_contents.Origination.delegate
                      := delegate;
                    Script_typed_ir.internal_operation_contents.Origination.code
                      := code;
                    Script_typed_ir.internal_operation_contents.Origination.unparsed_storage
                      := unparsed_storage;
                    Script_typed_ir.internal_operation_contents.Origination.credit
                      := credit;
                    Script_typed_ir.internal_operation_contents.Origination.preorigination
                      := preorigination;
                    Script_typed_ir.internal_operation_contents.Origination.storage_type
                      := storage_type;
                    Script_typed_ir.internal_operation_contents.Origination.storage
                      := init_value; |} in
              let? '(ctxt, nonce_value) :=
                Alpha_context.fresh_internal_nonce ctxt in
              let source :=
                Contract_repr.Originated
                  sc.(Script_typed_ir.step_constants.self) in
              let piop :=
                Script_typed_ir.Internal_operation
                  {| Script_typed_ir.internal_operation.source := source;
                    Script_typed_ir.internal_operation.operation := operation;
                    Script_typed_ir.internal_operation.nonce := nonce_value; |}
                in
              let res :=
                {| Script_typed_ir.operation.piop := piop;
                  Script_typed_ir.operation.lazy_storage_diff :=
                    lazy_storage_diff; |} in
              let '(gas, ctxt) :=
                Local_gas_counter.local_gas_counter_and_outdated_context ctxt in
              return? (res, preorigination, ctxt, gas).

Definition unpack {A : Set}
  (ctxt : Alpha_context.context) (ty_value : Script_typed_ir.ty)
  (bytes_value : bytes) : M? (option A × Alpha_context.context) :=
  let? ctxt :=
    Alpha_context.Gas.consume ctxt
      (Alpha_context.Script.deserialization_cost_estimated_from_bytes
        (Bytes.length bytes_value)) in
  if
    ((Bytes.length bytes_value) i 1) &&
    ((TzEndian.get_uint8 bytes_value 0) =i 5)
  then
    let str := Bytes.sub_string bytes_value 1 ((Bytes.length bytes_value) -i 1)
      in
    match
      Data_encoding.Binary.of_string_opt Alpha_context.Script.expr_encoding str
      with
    | None
      let? ctxt :=
        Alpha_context.Gas.consume ctxt (Interp_costs.unpack_failed str) in
      return? (None, ctxt)
    | Some expr
      let function_parameter :=
        Script_ir_translator.parse_data
          (Script_ir_translator_config.make None None false tt) ctxt false
          ty_value (Micheline.root_value expr) in
      match function_parameter with
      | Pervasives.Ok (value_value, ctxt)return? ((Some value_value), ctxt)
      | Pervasives.Error _ignored
        let? ctxt :=
          Alpha_context.Gas.consume ctxt (Interp_costs.unpack_failed str) in
        return? (None, ctxt)
      end
    end
  else
    return? (None, ctxt).

#[bypass_check(guard)]
Fixpoint interp_stack_prefix_preserving_operation {a s b t result c u d w : Set}
  (f_value : a s (b × t) × result)
  (n_value : Script_typed_ir.stack_prefix_preservation_witness) (accu_value : c)
  (stk : u) {struct n_value} : (d × w) × result :=
  match (n_value, accu_value, stk) with
  | (Script_typed_ir.KPrefix _ _ n_value, _, rest)
    let 'existT _ [__0, __1, __2, __3] [rest, n_value] :=
      cast_exists (Es := [Set ** Set ** Set ** Set])
        (fun '[__0, __1, __2, __3]
          [__0 × __1 ** Script_typed_ir.stack_prefix_preservation_witness])
        [rest, n_value] in
    cast ((d × w) × result)
    ((fun (function_parameter : (__2 × __3) × result) ⇒
      let '((v_value, rest'), result_value) := function_parameter in
      ((accu_value, (v_value, rest')), result_value))
      (interp_stack_prefix_preserving_operation f_value n_value
        (Pervasives.fst rest) (Pervasives.snd rest)))
  | (Script_typed_ir.KRest, accu_value, v_value)
    let '[v_value, accu_value] := cast [s ** a] [v_value, accu_value] in
    cast ((d × w) × result) (f_value accu_value v_value)
  end.

Definition cont_instrumentation : Set :=
  Script_typed_ir.continuation Script_typed_ir.continuation.

Definition id {A : Set} (x_value : A) : A := x_value.

Definition step_type (a s r f : Set) : Set :=
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Script_typed_ir.kinstr
  Script_typed_ir.continuation a s
  M?
    (r × f × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition kmap_exit_type (a b e f m n o : Set) : Set :=
  cont_instrumentation
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Script_typed_ir.kinstr
  list (m × n) option Script_typed_ir.ty Script_typed_ir.map m o m
  Script_typed_ir.continuation o a × b
  M?
    (e × f × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition kmap_enter_type (a b c d e j k : Set) : Set :=
  cont_instrumentation
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Script_typed_ir.kinstr
  list (j × k) option Script_typed_ir.ty Script_typed_ir.map j a
  Script_typed_ir.continuation b c
  M?
    (d × e × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition klist_exit_type (a b c d i j : Set) : Set :=
  cont_instrumentation
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Script_typed_ir.kinstr list i
  list j option Script_typed_ir.ty int Script_typed_ir.continuation
  j a × b
  M?
    (c × d × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition klist_enter_type (a b c d e j : Set) : Set :=
  cont_instrumentation
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Script_typed_ir.kinstr list j
  list b option Script_typed_ir.ty int Script_typed_ir.continuation
  a c
  M?
    (d × e × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition kloop_in_left_type (a b e f g : Set) : Set :=
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Script_typed_ir.continuation
  Script_typed_ir.kinstr Script_typed_ir.continuation
  Script_typed_ir.union a b g
  M?
    (e × f × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition kloop_in_type (a r f s : Set) : Set :=
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Script_typed_ir.continuation
  Script_typed_ir.kinstr Script_typed_ir.continuation bool a × s
  M?
    (r × f × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition kiter_type (a b s r f : Set) : Set :=
  cont_instrumentation
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Script_typed_ir.kinstr
  option Script_typed_ir.ty list b Script_typed_ir.continuation a
  s
  M?
    (r × f × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition ilist_map_type (a b c d e : Set) : Set :=
  cont_instrumentation
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Script_typed_ir.kinstr
  Script_typed_ir.kinstr Script_typed_ir.continuation
  option Script_typed_ir.ty Script_typed_ir.boxed_list e a × b
  M?
    (c × d × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition ilist_iter_type (a b c d e : Set) : Set :=
  cont_instrumentation
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Script_typed_ir.kinstr
  option Script_typed_ir.ty Script_typed_ir.kinstr
  Script_typed_ir.continuation Script_typed_ir.boxed_list e a × b
  M?
    (c × d × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition iset_iter_type (a b c d e : Set) : Set :=
  cont_instrumentation
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Script_typed_ir.kinstr
  option Script_typed_ir.comparable_ty Script_typed_ir.kinstr
  Script_typed_ir.continuation Script_typed_ir.set e a × b
  M?
    (c × d × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition imap_map_type (a b c d e f : Set) : Set :=
  cont_instrumentation
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Script_typed_ir.kinstr
  Script_typed_ir.kinstr Script_typed_ir.continuation
  option Script_typed_ir.ty Script_typed_ir.map e f a × b
  M?
    (c × d × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition imap_iter_type (a b c d e f : Set) : Set :=
  cont_instrumentation
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Script_typed_ir.kinstr
  option Script_typed_ir.ty Script_typed_ir.kinstr
  Script_typed_ir.continuation Script_typed_ir.map e f a × b
  M?
    (c × d × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition imul_teznat_type (b e f : Set) : Set :=
  option Script_typed_ir.logger
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Alpha_context.Script.location
  Script_typed_ir.kinstr Script_typed_ir.continuation
  Alpha_context.Tez.t Script_int.num × b
  M?
    (e × f × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition imul_nattez_type (b e f : Set) : Set :=
  option Script_typed_ir.logger
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Alpha_context.Script.location
  Script_typed_ir.kinstr Script_typed_ir.continuation Script_int.num
  Alpha_context.Tez.t × b
  M?
    (e × f × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition ilsl_nat_type (b e f : Set) : Set :=
  option Script_typed_ir.logger
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Alpha_context.Script.location
  Script_typed_ir.kinstr Script_typed_ir.continuation Script_int.num
  Script_int.num × b
  M?
    (e × f × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition ilsr_nat_type (b e f : Set) : Set :=
  option Script_typed_ir.logger
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Alpha_context.Script.location
  Script_typed_ir.kinstr Script_typed_ir.continuation Script_int.num
  Script_int.num × b
  M?
    (e × f × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Module ifailwith_type.
  Record record : Set := Build {
    ifailwith :
       {a b : Set},
      option Script_typed_ir.logger
      Local_gas_counter.outdated_context × Script_typed_ir.step_constants
      Local_gas_counter.local_gas_counter Alpha_context.Script.location
      Script_typed_ir.ty a M? b;
  }.
  Definition with_ifailwith ifailwith (r : record) :=
    Build ifailwith.
End ifailwith_type.
Definition ifailwith_type := ifailwith_type.record.

Definition iexec_type (b e f g : Set) : Set :=
  cont_instrumentation option Script_typed_ir.logger
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter option Script_typed_ir.stack_ty
  Script_typed_ir.kinstr Script_typed_ir.continuation g
  Script_typed_ir.lambda × b
  M?
    (e × f × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition iview_type (a b e f i : Set) : Set :=
  cont_instrumentation
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Script_typed_ir.view_signature
  option Script_typed_ir.stack_ty Script_typed_ir.kinstr
  Script_typed_ir.continuation i Script_typed_ir.address × (a × b)
  M?
    (e × f × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).