Skip to main content

🍬 Script_interpreter_defs.v

Translated OCaml

See proofs, See simulations, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Gas_input_size.
Require TezosOfOCaml.Proto_alpha.Local_gas_counter.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_gas.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.

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_mem _ _, _, 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_mem map.(Script_typed_ir.big_map.Big_map.diff)
  | (Script_typed_ir.IBig_map_get _ _, _, 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_get 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
          [Alpha_context.Script_timestamp.t × __35 **
            Alpha_context.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
          [Alpha_context.Script_int.num × __36 **
            Alpha_context.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
          [Alpha_context.Script_int.num × __37 **
            Alpha_context.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
          [Alpha_context.Script_timestamp.t × __38 **
            Alpha_context.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
          [Alpha_context.Script_string.t × __39 **
            Alpha_context.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 Alpha_context.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
          [Alpha_context.Script_int.num × (Alpha_context.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 __42Alpha_context.Script_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 Alpha_context.Script_int.num x_value in
    Interp_costs.abs_int x_value
  | (Script_typed_ir.INeg _ _, x_value, _)
    let x_value := cast Alpha_context.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
          [Alpha_context.Script_int.num × __48 ** Alpha_context.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
          [Alpha_context.Script_int.num × __49 ** Alpha_context.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
          [Alpha_context.Script_int.num × __52 ** Alpha_context.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
          [Alpha_context.Script_int.num × __55 ** Alpha_context.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
          [Alpha_context.Script_int.num × __57 ** Alpha_context.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[Alpha_context.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
          [Alpha_context.Script_int.num × __61 ** Alpha_context.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
          [Alpha_context.Script_int.num × __63 ** Alpha_context.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 Alpha_context.Script_int.num x_value in
    Interp_costs.lsl_nat x_value
  | (Script_typed_ir.ILsr_nat _ _, x_value, _)
    let x_value := cast Alpha_context.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
          [Alpha_context.Script_int.num × __66 ** Alpha_context.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
          [Alpha_context.Script_int.num × __67 ** Alpha_context.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
          [Alpha_context.Script_int.num × __68 ** Alpha_context.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
          [Alpha_context.Script_int.num × __69 ** Alpha_context.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 Alpha_context.Script_int.num x_value in
    Interp_costs.not_int x_value
  | (Script_typed_ir.ICompare _ ty _, a_value, stack_value)
    let 'existT _ __71 [stack_value, a_value, ty] :=
      cast_exists (Es := Set)
        (fun __71[a × __71 ** a ** Script_typed_ir.comparable_ty])
        [stack_value, a_value, ty] in
    let '(b_value, _) := stack_value in
    Interp_costs.compare ty a_value b_value
  | (Script_typed_ir.ICheck_signature _ _, key_value, stack_value)
    let 'existT _ __72 [stack_value, key_value] :=
      cast_exists (Es := Set)
        (fun __72
          [Script_typed_ir.signature × (bytes × __72) **
            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 _ [__76, __75] [stack_value, accu_value] :=
      cast_exists (Es := [Set ** Set])
        (fun '[__76, __75]
          [(Alpha_context.Script_int.num × Alpha_context.Script_int.num) × __76
            ** Script_typed_ir.ticket __75]) [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 _, ticket_a_b, _)
    let 'existT _ __77 [ticket_a_b, ty] :=
      cast_exists (Es := Set)
        (fun __77
          [Script_typed_ir.ticket __77 × Script_typed_ir.ticket __77 **
            Script_typed_ir.comparable_ty]) [ticket_a_b, ty] in
    let '(ticket_a, ticket_b) := ticket_a_b in
    Interp_costs.join_tickets ty 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 _ _ _, _, _)Interp_costs.apply
  | (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 Alpha_context.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 _ __140 stack_value :=
      cast_exists (Es := Set)
        (fun __140Alpha_context.Script_int.num × __140) 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 _ _, _, _)Interp_costs.ticket
  | (Script_typed_ir.IRead_ticket _ _, _, _)Interp_costs.read_ticket
  | (Script_typed_ir.IOpen_chest _ _, _chest_key, stack_value)
    let 'existT _ __145 [stack_value, _chest_key] :=
      cast_exists (Es := Set)
        (fun __145
          [Script_typed_ir.Script_timelock.chest ×
            (Alpha_context.Script_int.num × __145) ** a])
        [stack_value, _chest_key] in
    let '(chest_value, (time, _)) := stack_value in
    Interp_costs.open_chest chest_value (Alpha_context.Script_int.to_zint time)
  | (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 log_entry {A B : Set}
  (logger : Script_typed_ir.logger) (ctxt : Local_gas_counter.outdated_context)
  (gas : Local_gas_counter.local_gas_counter) (k_value : Script_typed_ir.kinstr)
  (accu_value : A) (stack_value : B) : unit :=
  let kinfo_value := Script_typed_ir.kinfo_of_kinstr k_value in
  let ctxt := Local_gas_counter.update_context gas ctxt in
  logger.(Script_typed_ir.logger.log_entry) _ _ k_value ctxt
    kinfo_value.(Script_typed_ir.kinfo.iloc)
    kinfo_value.(Script_typed_ir.kinfo.kstack_ty) (accu_value, stack_value).

Definition log_exit {A B : Set}
  (logger : Script_typed_ir.logger) (ctxt : Local_gas_counter.outdated_context)
  (gas : Local_gas_counter.local_gas_counter)
  (kinfo_prev : Script_typed_ir.kinfo) (k_value : Script_typed_ir.kinstr)
  (accu_value : A) (stack_value : B) : unit :=
  let kinfo_value := Script_typed_ir.kinfo_of_kinstr k_value in
  let ctxt := Local_gas_counter.update_context gas ctxt in
  logger.(Script_typed_ir.logger.log_exit) _ _ k_value ctxt
    kinfo_prev.(Script_typed_ir.kinfo.iloc)
    kinfo_value.(Script_typed_ir.kinfo.kstack_ty) (accu_value, stack_value).

Definition log_control
  (logger : Script_typed_ir.logger) (ks : Script_typed_ir.continuation)
  : unit := logger.(Script_typed_ir.logger.log_control) ks.

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.

Definition log_kinstr
  (logger : Script_typed_ir.logger) (i_value : Script_typed_ir.kinstr)
  : Script_typed_ir.kinstr :=
  Script_typed_ir.ILog (Script_typed_ir.kinfo_of_kinstr i_value)
    Script_typed_ir.LogEntry logger i_value.

Definition log_next_kinstr
  (logger : Script_typed_ir.logger) (i_value : Script_typed_ir.kinstr)
  : Script_typed_ir.kinstr :=
  let apply (k_value : Script_typed_ir.kinstr) : Script_typed_ir.kinstr :=
    Script_typed_ir.ILog (Script_typed_ir.kinfo_of_kinstr k_value)
      (Script_typed_ir.LogExit (Script_typed_ir.kinfo_of_kinstr i_value)) logger
      (log_kinstr logger k_value) in
  Script_typed_ir.kinstr_rewritek_value i_value
    {| Script_typed_ir.kinstr_rewritek.apply := apply; |}.

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

#[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 kinfo_value w_value, _, stack_value)
    let 'existT _ [__0, __1] [stack_value, w_value, kinfo_value] :=
      cast_exists (Es := [Set ** Set])
        (fun '[__0, __1]
          [__0 × __1 ** Script_typed_ir.stack_prefix_preservation_witness **
            Script_typed_ir.kinfo]) [stack_value, w_value, kinfo_value] in
    let k_value := Script_typed_ir.IConst kinfo_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 'Script_typed_ir.Lam descr_value expr := lam in
  match descr_value.(Script_typed_ir.kdescr.kbef) with
  | Script_typed_ir.Item_t full_arg_ty _
    let ctxt := Local_gas_counter.update_context gas ctxt in
    let? '(const_expr, ctxt) :=
      Script_ir_translator.unparse_data ctxt Script_ir_translator.Optimized
        capture_ty capture in
    let loc_value := Micheline.dummy_location in
    let? '(ty_expr, ctxt) :=
      Script_ir_translator.unparse_ty loc_value ctxt capture_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 :=
            let kinfo_const :=
              {|
                Script_typed_ir.kinfo.iloc :=
                  descr_value.(Script_typed_ir.kdescr.kloc);
                Script_typed_ir.kinfo.kstack_ty := arg_stack_ty; |} in
            let kinfo_pair :=
              {|
                Script_typed_ir.kinfo.iloc :=
                  descr_value.(Script_typed_ir.kdescr.kloc);
                Script_typed_ir.kinfo.kstack_ty :=
                  Script_typed_ir.Item_t capture_ty arg_stack_ty; |} in
            Script_typed_ir.IConst kinfo_const capture
              (Script_typed_ir.ICons_pair kinfo_pair
                descr_value.(Script_typed_ir.kdescr.kinstr)); |} in
      let full_expr :=
        Micheline.Seq loc_value
          [
            Micheline.Prim loc_value Michelson_v1_primitives.I_PUSH
              [ ty_expr; const_expr ] nil;
            Micheline.Prim loc_value Michelson_v1_primitives.I_PAIR nil nil;
            expr
          ] in
      let lam' := Script_typed_ir.Lam full_descr full_expr in
      let '(gas, ctxt) :=
        Local_gas_counter.local_gas_counter_and_outdated_context ctxt in
      return? (lam', ctxt, gas)
    | _unreachable_gadt_branch
    end
  | _unreachable_gadt_branch
  end.

Definition transfer {A : 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.ty A
  Alpha_context.Destination.t Alpha_context.Entrypoint.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 (parameters_ty : Script_typed_ir.ty) ⇒
          fun (parameters : A) ⇒
            fun (destination : Alpha_context.Destination.t) ⇒
              fun (entrypoint : Alpha_context.Entrypoint.t) ⇒
                let craft_transfer_parameters
                  (ctxt : Alpha_context.context) (tp : Script_typed_ir.ty)
                  (p_value :
                    Micheline.node Alpha_context.Script.location
                      Alpha_context.Script.prim)
                  (function_parameter : Alpha_context.Destination.t)
                  : M?
                    (Micheline.node Alpha_context.Script.location
                      Alpha_context.Script.prim × Alpha_context.context) :=
                  match function_parameter with
                  | Alpha_context.Destination.Contract _
                    return? (p_value, ctxt)
                  | Alpha_context.Destination.Tx_rollup _
                    match tp with
                    |
                      Script_typed_ir.Pair_t (Script_typed_ir.Ticket_t tp _) _ _
                        _
                      let? '(ty, ctxt) :=
                        Script_ir_translator.unparse_comparable_ty
                          Micheline.dummy_location ctxt tp in
                      return?
                        ((Micheline.Seq Micheline.dummy_location [ p_value; ty ]),
                          ctxt)
                    | _
                      (* ❌ Assert instruction is not handled. *)
                      assert
                        (M?
                          (Micheline.node Alpha_context.Script.location
                            Alpha_context.Script.prim × Alpha_context.context))
                        false
                    end
                  end in
                let ctxt := Local_gas_counter.update_context gas ctxt 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_translator.Optimized true to_duplicate to_update
                    parameters_ty parameters in
                let? '(unparsed_parameters, ctxt) :=
                  Script_ir_translator.unparse_data ctxt
                    Script_ir_translator.Optimized parameters_ty parameters in
                let? '(unparsed_parameters, ctxt) :=
                  craft_transfer_parameters ctxt parameters_ty
                    unparsed_parameters destination in
                let? ctxt :=
                  Alpha_context.Gas.consume ctxt
                    (Alpha_context.Script.strip_locations_cost
                      unparsed_parameters) in
                let transaction :=
                  let parameters :=
                    Alpha_context.Script.lazy_expr_value
                      (Micheline.strip_locations unparsed_parameters) in
                  {| Alpha_context.transaction.amount := amount;
                    Alpha_context.transaction.parameters := parameters;
                    Alpha_context.transaction.entrypoint := entrypoint;
                    Alpha_context.transaction.destination := destination; |} in
                let operation :=
                  Script_typed_ir.Transaction
                    {|
                      Script_typed_ir.manager_operation.Transaction.transaction
                        := transaction;
                      Script_typed_ir.manager_operation.Transaction.location :=
                        location;
                      Script_typed_ir.manager_operation.Transaction.parameters_ty
                        := parameters_ty;
                      Script_typed_ir.manager_operation.Transaction.parameters
                        := parameters; |} in
                let? '(ctxt, nonce_value) :=
                  Alpha_context.fresh_internal_nonce ctxt in
                let iop :=
                  {|
                    Script_typed_ir.internal_operation.source :=
                      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 × Alpha_context.Contract.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_translator.Optimized true to_duplicate to_update
                  storage_type init_value in
              let? '(storage_value, ctxt) :=
                Script_ir_translator.unparse_data ctxt
                  Script_ir_translator.Optimized storage_type init_value in
              let? ctxt :=
                Alpha_context.Gas.consume ctxt
                  (Alpha_context.Script.strip_locations_cost storage_value) in
              let storage_value := Micheline.strip_locations storage_value in
              let? '(ctxt, contract) :=
                Alpha_context.Contract.fresh_contract_from_current_nonce ctxt in
              let origination :=
                {| Alpha_context.origination.delegate := delegate;
                  Alpha_context.origination.script :=
                    {|
                      Alpha_context.Script.t.code :=
                        Alpha_context.Script.lazy_expr_value code;
                      Alpha_context.Script.t.storage :=
                        Alpha_context.Script.lazy_expr_value storage_value; |};
                  Alpha_context.origination.credit := credit; |} in
              let operation :=
                Script_typed_ir.Origination
                  {|
                    Script_typed_ir.manager_operation.Origination.origination :=
                      origination;
                    Script_typed_ir.manager_operation.Origination.preorigination
                      := contract;
                    Script_typed_ir.manager_operation.Origination.storage_type
                      := storage_type;
                    Script_typed_ir.manager_operation.Origination.storage :=
                      init_value; |} in
              let? '(ctxt, nonce_value) :=
                Alpha_context.fresh_internal_nonce ctxt in
              let piop :=
                Script_typed_ir.Internal_operation
                  {|
                    Script_typed_ir.internal_operation.source :=
                      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 := 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, contract, ctxt, gas).

Definition unpack {A : Set}
  (ctxt : Alpha_context.context) (ty : 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 None ctxt false false ty
          (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 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 g h m n o : Set) : Set :=
  (Script_typed_ir.continuation Script_typed_ir.continuation)
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter
  Script_typed_ir.kinstr × list (m × n) × Script_typed_ir.map m o × m
  Script_typed_ir.continuation o a × b
  M?
    (g × h × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Definition kmap_enter_type (a b c d e j k : Set) : Set :=
  (Script_typed_ir.continuation Script_typed_ir.continuation)
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter
  Script_typed_ir.kinstr × list (j × k) × 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 :=
  (Script_typed_ir.continuation Script_typed_ir.continuation)
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter
  Script_typed_ir.kinstr × list i × list j × 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 :=
  (Script_typed_ir.continuation Script_typed_ir.continuation)
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter
  Script_typed_ir.kinstr × list j × list b × 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 :=
  (Script_typed_ir.continuation Script_typed_ir.continuation)
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter Script_typed_ir.kinstr × 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 :=
  (Script_typed_ir.continuation Script_typed_ir.continuation)
  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 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 :=
  (Script_typed_ir.continuation Script_typed_ir.continuation)
  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 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 :=
  (Script_typed_ir.continuation Script_typed_ir.continuation)
  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 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 :=
  (Script_typed_ir.continuation Script_typed_ir.continuation)
  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 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 :=
  (Script_typed_ir.continuation Script_typed_ir.continuation)
  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 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
  Script_typed_ir.kinfo × Script_typed_ir.kinstr
  Script_typed_ir.continuation Alpha_context.Tez.t
  Alpha_context.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
  Script_typed_ir.kinfo × Script_typed_ir.kinstr
  Script_typed_ir.continuation Alpha_context.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
  Script_typed_ir.kinfo × Script_typed_ir.kinstr
  Script_typed_ir.continuation Alpha_context.Script_int.num
  Alpha_context.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
  Script_typed_ir.kinfo × Script_typed_ir.kinstr
  Script_typed_ir.continuation Alpha_context.Script_int.num
  Alpha_context.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 :=
  option Script_typed_ir.logger
  Local_gas_counter.outdated_context × Script_typed_ir.step_constants
  Local_gas_counter.local_gas_counter 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).