🍬 Script_interpreter_defs.v

Translated 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 __0 ⇒ Script_list.t __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 __3 ⇒ Script_list.t __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 __6 ⇒ Script_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 __28 ⇒ Script_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 __30 ⇒ Script_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_list.t 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_list.t 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 __42 ⇒ 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 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.ILsl_bytes _ _, accu_value, stack_value) ⇒
    let 'existT _ __65 [stack_value, accu_value] :=
      cast_exists (Es := Set) (fun __65 ⇒ [Script_int.num × __65 ** bytes])
        [stack_value, accu_value] in
    let x_value := accu_value in
    let '(y_value, _) := stack_value in
    Interp_costs.lsl_bytes x_value y_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.ILsr_bytes _ _, accu_value, stack_value) ⇒
    let 'existT _ __67 [stack_value, accu_value] :=
      cast_exists (Es := Set) (fun __67 ⇒ [Script_int.num × __67 ** bytes])
        [stack_value, accu_value] in
    let x_value := accu_value in
    let '(y_value, _) := stack_value in
    Interp_costs.lsr_bytes x_value y_value
  | (Script_typed_ir.IOr_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.or_nat x_value y_value
  | (Script_typed_ir.IOr_bytes _ _, accu_value, stack_value) ⇒
    let 'existT _ __69 [stack_value, accu_value] :=
      cast_exists (Es := Set) (fun __69 ⇒ [bytes × __69 ** bytes])
        [stack_value, accu_value] in
    let x_value := accu_value in
    let '(y_value, _) := stack_value in
    Interp_costs.or_bytes x_value y_value
  | (Script_typed_ir.IAnd_nat _ _, x_value, stack_value) ⇒
    let 'existT _ __70 [stack_value, x_value] :=
      cast_exists (Es := Set)
        (fun __70 ⇒ [Script_int.num × __70 ** 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 _ __71 [stack_value, x_value] :=
      cast_exists (Es := Set)
        (fun __71 ⇒ [Script_int.num × __71 ** 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.IAnd_bytes _ _, accu_value, stack_value) ⇒
    let 'existT _ __72 [stack_value, accu_value] :=
      cast_exists (Es := Set) (fun __72 ⇒ [bytes × __72 ** bytes])
        [stack_value, accu_value] in
    let x_value := accu_value in
    let '(y_value, _) := stack_value in
    Interp_costs.and_bytes x_value y_value
  | (Script_typed_ir.IXor_nat _ _, x_value, stack_value) ⇒
    let 'existT _ __73 [stack_value, x_value] :=
      cast_exists (Es := Set)
        (fun __73 ⇒ [Script_int.num × __73 ** 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.IXor_bytes _ _, accu_value, stack_value) ⇒
    let 'existT _ __74 [stack_value, accu_value] :=
      cast_exists (Es := Set) (fun __74 ⇒ [bytes × __74 ** bytes])
        [stack_value, accu_value] in
    let x_value := accu_value in
    let '(y_value, _) := stack_value in
    Interp_costs.xor_bytes 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.INot_bytes _ _, accu_value, _) ⇒
    let accu_value := cast bytes accu_value in
    let x_value := accu_value in
    Interp_costs.not_bytes x_value
  | (Script_typed_ir.ICompare _ ty_value _, a_value, stack_value) ⇒
    let 'existT _ [__76, __77] [stack_value, a_value, ty_value] :=
      cast_exists (Es := [Set ** Set])
        (fun '[__76 , __77 ] ⇒
          [a × (__76 × __77) ** 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 _ __78 [stack_value, key_value] :=
      cast_exists (Es := Set)
        (fun __78 ⇒
          [Script_typed_ir.signature × (bytes × __78) **
            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_list.t
          (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 _ _, _, stack_value) ⇒
    let 'existT _ __82 stack_value :=
      cast_exists (Es := Set)
        (fun __82 ⇒ (Script_int.num × Script_int.num) × __82) stack_value in
    let '((amount_a, amount_b), _) := stack_value in
    Interp_costs.split_ticket amount_a amount_b
  | (Script_typed_ir.IJoin_tickets _ ty_value _, accu_value, _) ⇒
    let 'existT _ __83 [accu_value, ty_value] :=
      cast_exists (Es := Set)
        (fun __83 ⇒
          [Script_typed_ir.ticket __83 × Script_typed_ir.ticket __83 **
            Script_typed_ir.comparable_ty]) [accu_value, ty_value] in
    let '(ticket_a, ticket_b) := accu_value 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 _ __139 stack_value :=
      cast_exists (Es := Set) (fun __139 ⇒ Script_typed_ir.lambda × __139)
        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 _ __160 stack_value :=
      cast_exists (Es := Set) (fun __160 ⇒ Script_int.num × __160) 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 _ __175 stack_value :=
      cast_exists (Es := Set)
        (fun __175 ⇒
          Script_typed_ir.Script_timelock.chest × (Script_int.num × __175))
        stack_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.KNil ⇒ Interp_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
  | None ⇒ Pervasives.Ok None
  | Some logger ⇒ logger.(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].