diff --git a/docs/protocols/alpha.rst b/docs/protocols/alpha.rst index 9c2667a6a3bb510a9470a18a0c74110cf86bb76f..9763321720bb5bfc3ee4e71d5900c227decfb87e 100644 --- a/docs/protocols/alpha.rst +++ b/docs/protocols/alpha.rst @@ -86,3 +86,5 @@ Internal - Make ``counter`` an abstract type instead of an alias of ``Z.t``. (MRs :gl:`!6647`, :gl:`!6648`) + +- Move interpreter logging to the plugin. (MR :gl:`!5778`) diff --git a/manifest/main.ml b/manifest/main.ml index 822abf3fbf0ef152f6b1afb90ddcad8c3a3da5bf..42e76679efb6cde2d52d98de48475d285018c4f7 100644 --- a/manifest/main.ml +++ b/manifest/main.ml @@ -3632,6 +3632,7 @@ end = struct octez_micheline |> open_; benchmark |> if_some |> open_; benchmark_type_inference |> if_some |> open_; + plugin |> if_some |> open_; parameters |> if_some |> if_ N.(number >= 013); ] in @@ -5044,6 +5045,7 @@ module Protocol = Protocol test_helpers |> open_; octez_sapling; client |> if_some |> open_; + plugin |> if_some |> open_; octez_protocol_environment; ] ~linkall:true diff --git a/opam/tezos-benchmarks-proto-014-PtKathma.opam b/opam/tezos-benchmarks-proto-014-PtKathma.opam index 91bf023fdc29a5e251d0622520dc1c41637902e8..791010e06cc73f21ae654a47be39bf259db25f85 100644 --- a/opam/tezos-benchmarks-proto-014-PtKathma.opam +++ b/opam/tezos-benchmarks-proto-014-PtKathma.opam @@ -22,6 +22,7 @@ depends: [ "tezos-014-PtKathma-test-helpers" "tezos-sapling" "tezos-client-014-PtKathma" + "tezos-protocol-plugin-014-PtKathma" "tezos-protocol-environment" ] build: [ diff --git a/opam/tezos-benchmarks-proto-015-PtLimaPt.opam b/opam/tezos-benchmarks-proto-015-PtLimaPt.opam index addd01cab2437be5c89a94f4fff5277a88f0b644..ab78f2b7082e77fa9c2be8fbe67bb2c1adcb77a7 100644 --- a/opam/tezos-benchmarks-proto-015-PtLimaPt.opam +++ b/opam/tezos-benchmarks-proto-015-PtLimaPt.opam @@ -22,6 +22,7 @@ depends: [ "tezos-015-PtLimaPt-test-helpers" "tezos-sapling" "tezos-client-015-PtLimaPt" + "tezos-protocol-plugin-015-PtLimaPt" "tezos-protocol-environment" ] build: [ diff --git a/opam/tezos-benchmarks-proto-alpha.opam b/opam/tezos-benchmarks-proto-alpha.opam index f994c9cb924586115cad7e57c927ca0d0c7cdc9b..594995c5f22a3882d5ae870be7b38c30ee7ddaf9 100644 --- a/opam/tezos-benchmarks-proto-alpha.opam +++ b/opam/tezos-benchmarks-proto-alpha.opam @@ -22,6 +22,7 @@ depends: [ "tezos-alpha-test-helpers" "tezos-sapling" "tezos-client-alpha" + "tezos-protocol-plugin-alpha" "tezos-protocol-environment" ] build: [ diff --git a/src/proto_014_PtKathma/lib_benchmarks_proto/dune b/src/proto_014_PtKathma/lib_benchmarks_proto/dune index e0d884826e8de6dc6b41c7e88d0a48d4fd53c745..bfc2a5d4013dd4501ebc74edba2146ce2e65cb24 100644 --- a/src/proto_014_PtKathma/lib_benchmarks_proto/dune +++ b/src/proto_014_PtKathma/lib_benchmarks_proto/dune @@ -21,6 +21,7 @@ tezos-014-PtKathma-test-helpers tezos-sapling tezos-client-014-PtKathma + tezos-protocol-plugin-014-PtKathma tezos-protocol-environment) (library_flags (:standard -linkall)) (flags @@ -39,4 +40,5 @@ -open Tezos_crypto -open Tezos_micheline -open Tezos_014_PtKathma_test_helpers - -open Tezos_client_014_PtKathma)) + -open Tezos_client_014_PtKathma + -open Tezos_protocol_plugin_014_PtKathma)) diff --git a/src/proto_014_PtKathma/lib_protocol/test/integration/michelson/dune b/src/proto_014_PtKathma/lib_protocol/test/integration/michelson/dune index c76337445db3e1270df7f78f658960280c24ce3d..7181e2718c45caf112eaa755f15b110a91c1b716 100644 --- a/src/proto_014_PtKathma/lib_protocol/test/integration/michelson/dune +++ b/src/proto_014_PtKathma/lib_protocol/test/integration/michelson/dune @@ -14,6 +14,7 @@ tezos-micheline tezos-benchmark-014-PtKathma tezos-benchmark-type-inference-014-PtKathma + tezos-protocol-plugin-014-PtKathma tezos-protocol-014-PtKathma.parameters) (flags (:standard) @@ -25,7 +26,8 @@ -open Tezos_client_014_PtKathma -open Tezos_micheline -open Tezos_benchmark_014_PtKathma - -open Tezos_benchmark_type_inference_014_PtKathma)) + -open Tezos_benchmark_type_inference_014_PtKathma + -open Tezos_protocol_plugin_014_PtKathma)) (rule (alias runtest) diff --git a/src/proto_015_PtLimaPt/lib_benchmarks_proto/dune b/src/proto_015_PtLimaPt/lib_benchmarks_proto/dune index 84b40912f635ed5733538afd40f30c305e115009..ad2a144280cc87562e591f03dbb9017388566c27 100644 --- a/src/proto_015_PtLimaPt/lib_benchmarks_proto/dune +++ b/src/proto_015_PtLimaPt/lib_benchmarks_proto/dune @@ -21,6 +21,7 @@ tezos-015-PtLimaPt-test-helpers tezos-sapling tezos-client-015-PtLimaPt + tezos-protocol-plugin-015-PtLimaPt tezos-protocol-environment) (library_flags (:standard -linkall)) (flags @@ -39,4 +40,5 @@ -open Tezos_crypto -open Tezos_micheline -open Tezos_015_PtLimaPt_test_helpers - -open Tezos_client_015_PtLimaPt)) + -open Tezos_client_015_PtLimaPt + -open Tezos_protocol_plugin_015_PtLimaPt)) diff --git a/src/proto_015_PtLimaPt/lib_protocol/test/integration/michelson/dune b/src/proto_015_PtLimaPt/lib_protocol/test/integration/michelson/dune index 14ad1267ac7b094bd288b6e22147b909c1bf9bbc..576884826a072223d836762511c984290857ef8b 100644 --- a/src/proto_015_PtLimaPt/lib_protocol/test/integration/michelson/dune +++ b/src/proto_015_PtLimaPt/lib_protocol/test/integration/michelson/dune @@ -14,6 +14,7 @@ tezos-micheline tezos-benchmark-015-PtLimaPt tezos-benchmark-type-inference-015-PtLimaPt + tezos-protocol-plugin-015-PtLimaPt tezos-protocol-015-PtLimaPt.parameters) (flags (:standard) @@ -25,7 +26,8 @@ -open Tezos_client_015_PtLimaPt -open Tezos_micheline -open Tezos_benchmark_015_PtLimaPt - -open Tezos_benchmark_type_inference_015_PtLimaPt)) + -open Tezos_benchmark_type_inference_015_PtLimaPt + -open Tezos_protocol_plugin_015_PtLimaPt)) (rule (alias runtest) diff --git a/src/proto_alpha/lib_benchmarks_proto/dune b/src/proto_alpha/lib_benchmarks_proto/dune index 0431bf92cca9e2597665d8d36e388ba00eed04fe..dfd091391e1e27aa9d156d9ab9fb460e644a7bbb 100644 --- a/src/proto_alpha/lib_benchmarks_proto/dune +++ b/src/proto_alpha/lib_benchmarks_proto/dune @@ -21,6 +21,7 @@ tezos-alpha-test-helpers tezos-sapling tezos-client-alpha + tezos-protocol-plugin-alpha tezos-protocol-environment) (library_flags (:standard -linkall)) (flags @@ -39,4 +40,5 @@ -open Tezos_crypto -open Tezos_micheline -open Tezos_alpha_test_helpers - -open Tezos_client_alpha)) + -open Tezos_client_alpha + -open Tezos_protocol_plugin_alpha)) diff --git a/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml b/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml index 221e1789050ab52ac1478a784226ffddf72766ce..462f4b534578cad57841de379846b8f7e3fa77c3 100644 --- a/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml +++ b/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml @@ -1482,17 +1482,24 @@ let extract_deps (type bef_top bef aft_top aft) ctxt step_constants (stack : bef_top * bef) = let trace = ref [] in (* Logger definition *) - let log_interp _instr _ctxt _log _stack_ty _stack = () in - let log_entry : - type a s b f. (a, s, b, f, a, s) Script_typed_ir.logging_function = - fun kinstr ctxt _loc _stack_ty stack -> - trace := extract_ir_sized_step ctxt kinstr stack :: !trace ; - match kinstr with IFailwith _ -> raise Stop_bench | _ -> () + let logger = + Script_interpreter_logging.make + (module struct + let log_interp _instr _ctxt _log _stack_ty _stack = () + + let log_entry : + type a s b f. (a, s, b, f, a, s) Script_typed_ir.logging_function = + fun kinstr ctxt _loc _stack_ty stack -> + trace := extract_ir_sized_step ctxt kinstr stack :: !trace ; + match kinstr with IFailwith _ -> raise Stop_bench | _ -> () + + let log_control kont = trace := extract_control_trace kont :: !trace + + let log_exit _instr _ctxt _log _stack_ty _stack = () + + let get_log () = Environment.Error_monad.return_none + end) in - let log_control kont = trace := extract_control_trace kont :: !trace in - let log_exit _instr _ctxt _log _stack_ty _stack = () in - let get_log () = Environment.Error_monad.return_none in - let logger = {log_interp; log_entry; log_control; log_exit; get_log} in try let res = Lwt_main.run @@ -1520,17 +1527,24 @@ let extract_deps_continuation (type bef_top bef aft_top aft) ctxt step_constants (stack : bef_top * bef) = let trace = ref [] in (* Logger definition *) - let log_interp _instr _ctxt _log _stack_ty _stack = () in - let log_entry : - type a s b f. (a, s, b, f, a, s) Script_typed_ir.logging_function = - fun kinstr ctxt _loc _stack_ty stack -> - trace := extract_ir_sized_step ctxt kinstr stack :: !trace ; - match kinstr with IFailwith _ -> raise Stop_bench | _ -> () + let logger = + Script_interpreter_logging.make + (module struct + let log_interp _instr _ctxt _log _stack_ty _stack = () + + let log_entry : + type a s b f. (a, s, b, f, a, s) Script_typed_ir.logging_function = + fun kinstr ctxt _loc _stack_ty stack -> + trace := extract_ir_sized_step ctxt kinstr stack :: !trace ; + match kinstr with IFailwith _ -> raise Stop_bench | _ -> () + + let log_control kont = trace := extract_control_trace kont :: !trace + + let log_exit _instr _ctxt _log _stack_ty _stack = () + + let get_log () = Environment.Error_monad.return_none + end) in - let log_control kont = trace := extract_control_trace kont :: !trace in - let log_exit _instr _ctxt _log _stack_ty _stack = () in - let get_log () = Environment.Error_monad.return_none in - let logger = {log_interp; log_entry; log_control; log_exit; get_log} in try let res = let _gas_counter, outdated_ctxt = diff --git a/src/proto_alpha/lib_plugin/RPC.ml b/src/proto_alpha/lib_plugin/RPC.ml index b72528e7698b6ab47f16a5f685bf999d7d421964..7ff7da7b146383ed4eac94144b9129b0703e57d3 100644 --- a/src/proto_alpha/lib_plugin/RPC.ml +++ b/src/proto_alpha/lib_plugin/RPC.ml @@ -499,28 +499,32 @@ module Scripts = struct unparse_stack (stack_ty, stack) let trace_logger ctxt : Script_typed_ir.logger = - let log : log_element list ref = ref [] in - let log_interp _ ctxt loc sty stack = - log := Log (ctxt, loc, stack, sty) :: !log - in - let log_entry _ _ctxt _loc _sty _stack = () in - let log_exit _ ctxt loc sty stack = - log := Log (ctxt, loc, stack, sty) :: !log - in - let log_control _ = () in - let get_log () = - List.fold_left_es - (fun (old_ctxt, l) (Log (ctxt, loc, stack, stack_ty)) -> - let consumed_gas = Gas.consumed ~since:old_ctxt ~until:ctxt in - trace - Plugin_errors.Cannot_serialize_log - (unparse_stack ctxt (stack, stack_ty)) - >>=? fun stack -> return (ctxt, (loc, consumed_gas, stack) :: l)) - (ctxt, []) - (List.rev !log) - >>=? fun (_ctxt, res) -> return (Some (List.rev res)) - in - {log_exit; log_entry; log_interp; get_log; log_control} + Script_interpreter_logging.make + (module struct + let log : log_element list ref = ref [] + + let log_interp _ ctxt loc sty stack = + log := Log (ctxt, loc, stack, sty) :: !log + + let log_entry _ _ctxt _loc _sty _stack = () + + let log_exit _ ctxt loc sty stack = + log := Log (ctxt, loc, stack, sty) :: !log + + let log_control _ = () + + let get_log () = + List.fold_left_es + (fun (old_ctxt, l) (Log (ctxt, loc, stack, stack_ty)) -> + let consumed_gas = Gas.consumed ~since:old_ctxt ~until:ctxt in + trace + Plugin_errors.Cannot_serialize_log + (unparse_stack ctxt (stack, stack_ty)) + >>=? fun stack -> return (ctxt, (loc, consumed_gas, stack) :: l)) + (ctxt, []) + (List.rev !log) + >>=? fun (_ctxt, res) -> return (Some (List.rev res)) + end) let execute ctxt step_constants ~script ~entrypoint ~parameter = let logger = trace_logger ctxt in diff --git a/src/proto_alpha/lib_plugin/plugin.ml b/src/proto_alpha/lib_plugin/plugin.ml index 224a977827cdfb831842683d61848024b9a12138..6cac7b1148120d896cfd6895408fcf411b873d6e 100644 --- a/src/proto_alpha/lib_plugin/plugin.ml +++ b/src/proto_alpha/lib_plugin/plugin.ml @@ -29,3 +29,4 @@ module Mempool = Mempool module View_helpers = View_helpers module RPC = RPC module Metrics = Metrics +module Script_interpreter_logging = Script_interpreter_logging diff --git a/src/proto_alpha/lib_plugin/script_interpreter_logging.ml b/src/proto_alpha/lib_plugin/script_interpreter_logging.ml new file mode 100644 index 0000000000000000000000000000000000000000..193926d2df90f6da7e42437ab185cd83a1e6c02f --- /dev/null +++ b/src/proto_alpha/lib_plugin/script_interpreter_logging.ml @@ -0,0 +1,2229 @@ +(*****************************************************************************) +(* *) +(* Open Source License *) +(* Copyright (c) 2022 Nomadic Labs *) +(* *) +(* Permission is hereby granted, free of charge, to any person obtaining a *) +(* copy of this software and associated documentation files (the "Software"),*) +(* to deal in the Software without restriction, including without limitation *) +(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *) +(* and/or sell copies of the Software, and to permit persons to whom the *) +(* Software is furnished to do so, subject to the following conditions: *) +(* *) +(* The above copyright notice and this permission notice shall be included *) +(* in all copies or substantial portions of the Software. *) +(* *) +(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*) +(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *) +(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *) +(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*) +(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *) +(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *) +(* DEALINGS IN THE SOFTWARE. *) +(* *) +(*****************************************************************************) + +open Protocol +open Environment +open Error_monad +open Alpha_context +open Script_typed_ir + +module Stack_utils = struct + type kinstr_rewritek = { + apply : + 'b 'u 'r 'f. + ('b, 'u) stack_ty -> ('b, 'u, 'r, 'f) kinstr -> ('b, 'u, 'r, 'f) kinstr; + } + [@@ocaml.unboxed] + + (* An existential wrapper around failed [kinstr], whose final stack type + is hidden as it is irrelevant. *) + type ('a, 's) failed_kinstr_cast = {cast : 'b 'u. ('a, 's, 'b, 'u) kinstr} + [@@ocaml.unboxed] + + (* This is a view on a deconstructed [kinstr]. Its type parameters refer to + the type of the viewed [kinstr], while existentials inside describe types of + [kinstr]'s components. The [reconstruct] field in each record stores a + function which reconstructs the original instruction from its components. *) + type ('a, 's, 'r, 'f) ex_split_kinstr = + | Ex_split_kinstr : { + cont_init_stack : ('b, 'u) stack_ty; + continuation : ('b, 'u, 'r, 'f) kinstr; + reconstruct : ('b, 'u, 'r, 'f) kinstr -> ('a, 's, 'r, 'f) kinstr; + } + -> ('a, 's, 'r, 'f) ex_split_kinstr + | Ex_split_log : { + stack : ('a, 's) stack_ty; + continuation : ('a, 's, 'r, 'f) kinstr; + reconstruct : ('a, 's, 'r, 'f) kinstr -> ('a, 's, 'r, 'f) kinstr; + } + -> ('a, 's, 'r, 'f) ex_split_kinstr + | Ex_split_loop_may_fail : { + body_init_stack : ('b, 'u) stack_ty; + body : ('b, 'u, 'r, 'f) kinstr; + cont_init_stack : ('c, 'v) stack_ty; + continuation : ('c, 'v, 't, 'g) kinstr; + reconstruct : + ('b, 'u, 'r, 'f) kinstr -> + ('c, 'v, 't, 'g) kinstr -> + ('a, 's, 't, 'g) kinstr; + } + -> ('a, 's, 't, 'g) ex_split_kinstr + | Ex_split_loop_may_not_fail : { + body_init_stack : ('b, 'u) stack_ty; + body : ('b, 'u, 'r, 'f) kinstr; + continuation : ('c, 'v, 't, 'g) kinstr; + aft_body_stack_transform : + ('r, 'f) stack_ty -> ('c, 'v) stack_ty tzresult; + reconstruct : + ('b, 'u, 'r, 'f) kinstr -> + ('c, 'v, 't, 'g) kinstr -> + ('a, 's, 't, 'g) kinstr; + } + -> ('a, 's, 't, 'g) ex_split_kinstr + | Ex_split_if : { + left_init_stack : ('b, 'u) stack_ty; + left_branch : ('b, 'u, 'r, 'f) kinstr; + right_init_stack : ('c, 'v) stack_ty; + right_branch : ('c, 'v, 'r, 'f) kinstr; + continuation : ('r, 'f, 't, 'g) kinstr; + reconstruct : + ('b, 'u, 'r, 'f) kinstr -> + ('c, 'v, 'r, 'f) kinstr -> + ('r, 'f, 't, 'g) kinstr -> + ('a, 's, 't, 'g) kinstr; + } + -> ('a, 's, 't, 'g) ex_split_kinstr + | Ex_split_halt : Script.location -> ('a, 's, 'a, 's) ex_split_kinstr + | Ex_split_failwith : { + location : Script.location; + arg_ty : ('a, _) ty; + cast : ('a, 's) failed_kinstr_cast; + } + -> ('a, 's, 'r, 'f) ex_split_kinstr + + (** An existential container for an instruction paired with its + initial stack type. This is used internally to pack together + execution branches with different initial stack types but + the same final stack type (which we want to compute). *) + type ('r, 'f) ex_init_stack_ty = + | Ex_init_stack_ty : + ('a, 's) stack_ty * ('a, 's, 'r, 'f) kinstr + -> ('r, 'f) ex_init_stack_ty + + let rec stack_prefix_preservation_witness_split_input : + type a s b t c u d v. + (b, t, c, u, a, s, d, v) stack_prefix_preservation_witness -> + (a, s) stack_ty -> + (b, t) stack_ty = + fun w s -> + match (w, s) with + | KPrefix (_, _, w), Item_t (_, s) -> + stack_prefix_preservation_witness_split_input w s + | KRest, s -> s + + let rec stack_prefix_preservation_witness_split_output : + type a s b t c u d v. + (b, t, c, u, a, s, d, v) stack_prefix_preservation_witness -> + (c, u) stack_ty -> + (d, v) stack_ty = + fun w s -> + match (w, s) with + | KPrefix (_, a, w), s -> + Item_t (a, stack_prefix_preservation_witness_split_output w s) + | KRest, s -> s + + (* We apply this function to optional type information which must be present + if functions from this module were called. Use with care. *) + let assert_some = function None -> assert false | Some x -> x + + let kinstr_split : + type a s r f. + (a, s) stack_ty -> + (a, s, r, f) kinstr -> + (a, s, r, f) ex_split_kinstr tzresult = + fun s i -> + let dummy = Micheline.dummy_location in + match (i, s) with + | IDrop (loc, k), Item_t (_a, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IDrop (loc, k)); + } + | IDup (loc, k), Item_t (a, s) -> + let s = Item_t (a, Item_t (a, s)) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IDup (loc, k)); + } + | ISwap (loc, k), Item_t (a, Item_t (b, s)) -> + let s = Item_t (b, Item_t (a, s)) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISwap (loc, k)); + } + | IConst (loc, a, x, k), s -> + let s = Item_t (a, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IConst (loc, a, x, k)); + } + | ICons_pair (loc, k), Item_t (a, Item_t (b, s)) -> + pair_t dummy a b >|? fun (Ty_ex_c c) -> + let s = Item_t (c, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ICons_pair (loc, k)); + } + | ICar (loc, k), Item_t (Pair_t (a, _b, _meta, _), s) -> + let s = Item_t (a, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ICar (loc, k)); + } + | ICdr (loc, k), Item_t (Pair_t (_a, b, _meta, _), s) -> + let s = Item_t (b, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ICdr (loc, k)); + } + | IUnpair (loc, k), Item_t (Pair_t (a, b, _meta, _), s) -> + let s = Item_t (a, Item_t (b, s)) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IUnpair (loc, k)); + } + | ICons_some (loc, k), Item_t (a, s) -> + option_t dummy a >|? fun o -> + let s = Item_t (o, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ICons_some (loc, k)); + } + | ICons_none (loc, a, k), s -> + option_t dummy a >|? fun o -> + let s = Item_t (o, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ICons_none (loc, a, k)); + } + | ( IIf_none {loc; branch_if_none; branch_if_some; k}, + Item_t (Option_t (a, _meta, _), s) ) -> + ok + @@ Ex_split_if + { + left_init_stack = s; + left_branch = branch_if_none; + right_init_stack = Item_t (a, s); + right_branch = branch_if_some; + continuation = k; + reconstruct = + (fun branch_if_none branch_if_some k -> + IIf_none {loc; branch_if_none; branch_if_some; k}); + } + | IOpt_map {loc; body; k}, Item_t (Option_t (a, _meta, _), s) -> + ok + @@ Ex_split_loop_may_not_fail + { + body_init_stack = Item_t (a, s); + body; + continuation = k; + aft_body_stack_transform = + (function + | Item_t (b, s) -> option_t dummy b >|? fun o -> Item_t (o, s)); + reconstruct = (fun body k -> IOpt_map {loc; body; k}); + } + | ICons_left (loc, b, k), Item_t (a, s) -> + union_t dummy a b >|? fun (Ty_ex_c c) -> + let s = Item_t (c, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ICons_left (loc, b, k)); + } + | ICons_right (loc, a, k), Item_t (b, s) -> + union_t dummy a b >|? fun (Ty_ex_c c) -> + let s = Item_t (c, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ICons_right (loc, a, k)); + } + | ( IIf_left {loc; branch_if_left; branch_if_right; k}, + Item_t (Union_t (a, b, _meta, _), s) ) -> + ok + @@ Ex_split_if + { + left_init_stack = Item_t (a, s); + left_branch = branch_if_left; + right_init_stack = Item_t (b, s); + right_branch = branch_if_right; + continuation = k; + reconstruct = + (fun branch_if_left branch_if_right k -> + IIf_left {loc; branch_if_left; branch_if_right; k}); + } + | ICons_list (loc, k), Item_t (_a, Item_t (l, s)) -> + let s = Item_t (l, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ICons_list (loc, k)); + } + | INil (loc, a, k), s -> + list_t dummy a >|? fun l -> + let s = Item_t (l, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> INil (loc, a, k)); + } + | ( IIf_cons {loc; branch_if_cons; branch_if_nil; k}, + Item_t ((List_t (a, _meta) as l), s) ) -> + ok + @@ Ex_split_if + { + left_init_stack = Item_t (a, Item_t (l, s)); + left_branch = branch_if_cons; + right_init_stack = s; + right_branch = branch_if_nil; + continuation = k; + reconstruct = + (fun branch_if_cons branch_if_nil k -> + IIf_cons {loc; branch_if_cons; branch_if_nil; k}); + } + | IList_map (loc, body, ty, k), Item_t (List_t (a, _meta), s) -> + let s = Item_t (a, s) in + ok + @@ Ex_split_loop_may_not_fail + { + body_init_stack = s; + body; + continuation = k; + aft_body_stack_transform = + (function + | Item_t (b, s) -> list_t dummy b >|? fun l -> Item_t (l, s)); + reconstruct = (fun body k -> IList_map (loc, body, ty, k)); + } + | IList_iter (loc, ty, body, k), Item_t (List_t (a, _meta), s) -> + ok + @@ Ex_split_loop_may_fail + { + body_init_stack = Item_t (a, s); + body; + cont_init_stack = s; + continuation = k; + reconstruct = (fun body k -> IList_iter (loc, ty, body, k)); + } + | IList_size (loc, k), Item_t (_l, s) -> + let s = Item_t (nat_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IList_size (loc, k)); + } + | IEmpty_set (loc, a, k), s -> + set_t dummy a >|? fun b -> + let s = Item_t (b, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IEmpty_set (loc, a, k)); + } + | ISet_iter (loc, a, body, k), Item_t (_b, s) -> + ok + @@ Ex_split_loop_may_fail + { + body_init_stack = Item_t (assert_some a, s); + body; + cont_init_stack = s; + continuation = k; + reconstruct = (fun body k -> ISet_iter (loc, a, body, k)); + } + | ISet_mem (loc, k), Item_t (_, Item_t (_, s)) -> + let s = Item_t (bool_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISet_mem (loc, k)); + } + | ISet_update (loc, k), Item_t (_, Item_t (_, s)) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISet_update (loc, k)); + } + | ISet_size (loc, k), Item_t (_, s) -> + let s = Item_t (nat_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISet_size (loc, k)); + } + | IEmpty_map (loc, cty, vty, k), s -> + map_t dummy cty (assert_some vty) >|? fun m -> + let s = Item_t (m, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IEmpty_map (loc, cty, vty, k)); + } + | IMap_map (loc, ty, body, k), Item_t (Map_t (kty, vty, _meta), s) -> + let (Map_t (key_ty, _, _)) = assert_some ty in + pair_t dummy key_ty vty >|? fun (Ty_ex_c p) -> + Ex_split_loop_may_not_fail + { + body_init_stack = Item_t (p, s); + body; + continuation = k; + aft_body_stack_transform = + (fun (Item_t (b, s)) -> + map_t dummy kty b >|? fun m -> Item_t (m, s)); + reconstruct = (fun body k -> IMap_map (loc, ty, body, k)); + } + | IMap_iter (loc, kvty, body, k), Item_t (_, stack) -> + ok + @@ Ex_split_loop_may_fail + { + body_init_stack = Item_t (assert_some kvty, stack); + body; + cont_init_stack = stack; + continuation = k; + reconstruct = (fun body k -> IMap_iter (loc, kvty, body, k)); + } + | IMap_mem (loc, k), Item_t (_, Item_t (_, s)) -> + let s = Item_t (bool_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IMap_mem (loc, k)); + } + | IMap_get (loc, k), Item_t (_, Item_t (Map_t (_kty, vty, _meta), s)) -> + option_t dummy vty >|? fun o -> + let s = Item_t (o, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IMap_get (loc, k)); + } + | IMap_update (loc, k), Item_t (_, Item_t (_, s)) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IMap_update (loc, k)); + } + | IMap_get_and_update (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IMap_get_and_update (loc, k)); + } + | IMap_size (loc, k), Item_t (_, s) -> + let s = Item_t (nat_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IMap_size (loc, k)); + } + | IEmpty_big_map (loc, cty, ty, k), s -> + big_map_t dummy cty ty >|? fun b -> + let s = Item_t (b, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IEmpty_big_map (loc, cty, ty, k)); + } + | IBig_map_mem (loc, k), Item_t (_, Item_t (_, s)) -> + let s = Item_t (bool_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IBig_map_mem (loc, k)); + } + | IBig_map_get (loc, k), Item_t (_, Item_t (Big_map_t (_kty, vty, _meta), s)) + -> + option_t dummy vty >|? fun o -> + let s = Item_t (o, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IBig_map_get (loc, k)); + } + | IBig_map_update (loc, k), Item_t (_, Item_t (_, s)) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IBig_map_update (loc, k)); + } + | IBig_map_get_and_update (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IBig_map_get_and_update (loc, k)); + } + | IConcat_string (loc, k), Item_t (_, s) -> + let s = Item_t (string_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IConcat_string (loc, k)); + } + | IConcat_string_pair (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IConcat_string_pair (loc, k)); + } + | ISlice_string (loc, k), Item_t (_, Item_t (_, Item_t (_, s))) -> + let s = Item_t (option_string_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISlice_string (loc, k)); + } + | IString_size (loc, k), Item_t (_, s) -> + let s = Item_t (nat_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IString_size (loc, k)); + } + | IConcat_bytes (loc, k), Item_t (_, s) -> + let s = Item_t (bytes_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IConcat_bytes (loc, k)); + } + | IConcat_bytes_pair (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IConcat_bytes_pair (loc, k)); + } + | ISlice_bytes (loc, k), Item_t (_, Item_t (_, Item_t (_, s))) -> + let s = Item_t (option_bytes_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISlice_bytes (loc, k)); + } + | IBytes_size (loc, k), Item_t (_, s) -> + let s = Item_t (nat_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IBytes_size (loc, k)); + } + | IAdd_seconds_to_timestamp (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IAdd_seconds_to_timestamp (loc, k)); + } + | IAdd_timestamp_to_seconds (loc, k), Item_t (_, Item_t (_, s)) -> + let s = Item_t (timestamp_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IAdd_timestamp_to_seconds (loc, k)); + } + | ISub_timestamp_seconds (loc, k), Item_t (_, Item_t (_, s)) -> + let s = Item_t (timestamp_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISub_timestamp_seconds (loc, k)); + } + | IDiff_timestamps (loc, k), Item_t (_, Item_t (_, s)) -> + let s = Item_t (int_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IDiff_timestamps (loc, k)); + } + | IAdd_tez (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IAdd_tez (loc, k)); + } + | ISub_tez (loc, k), Item_t (_, Item_t (_, s)) -> + let s = Item_t (option_mutez_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISub_tez (loc, k)); + } + | ISub_tez_legacy (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISub_tez_legacy (loc, k)); + } + | IMul_teznat (loc, k), Item_t (_, Item_t (_, s)) -> + let s = Item_t (mutez_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IMul_teznat (loc, k)); + } + | IMul_nattez (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IMul_nattez (loc, k)); + } + | IEdiv_teznat (loc, k), Item_t (_, Item_t (_, s)) -> + let s = Item_t (option_pair_mutez_mutez_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IEdiv_teznat (loc, k)); + } + | IEdiv_tez (loc, k), Item_t (_, Item_t (_, s)) -> + let s = Item_t (option_pair_nat_mutez_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IEdiv_tez (loc, k)); + } + | IOr (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IOr (loc, k)); + } + | IAnd (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IAnd (loc, k)); + } + | IXor (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IXor (loc, k)); + } + | INot (loc, k), s -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> INot (loc, k)); + } + | IIs_nat (loc, k), Item_t (_, s) -> + let s = Item_t (option_nat_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IIs_nat (loc, k)); + } + | INeg (loc, k), Item_t (_, s) -> + let s = Item_t (int_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> INeg (loc, k)); + } + | IAbs_int (loc, k), Item_t (_, s) -> + let s = Item_t (nat_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IAbs_int (loc, k)); + } + | IInt_nat (loc, k), Item_t (_, s) -> + let s = Item_t (int_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IInt_nat (loc, k)); + } + | IAdd_int (loc, k), Item_t (_, Item_t (_, s)) -> + let s = Item_t (int_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IAdd_int (loc, k)); + } + | IAdd_nat (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IAdd_nat (loc, k)); + } + | ISub_int (loc, k), Item_t (_, Item_t (_, s)) -> + let s = Item_t (int_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISub_int (loc, k)); + } + | IMul_int (loc, k), Item_t (_, Item_t (_, s)) -> + let s = Item_t (int_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IMul_int (loc, k)); + } + | IMul_nat (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IMul_nat (loc, k)); + } + | IEdiv_int (loc, k), Item_t (_, Item_t (_, s)) -> + let s = Item_t (option_pair_int_nat_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IEdiv_int (loc, k)); + } + | IEdiv_nat (loc, k), Item_t (_, Item_t (a, s)) -> + pair_t dummy a nat_t >>? fun (Ty_ex_c p) -> + option_t dummy p >|? fun o -> + let s = Item_t (o, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IEdiv_nat (loc, k)); + } + | ILsl_nat (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ILsl_nat (loc, k)); + } + | ILsr_nat (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ILsr_nat (loc, k)); + } + | IOr_nat (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IOr_nat (loc, k)); + } + | IAnd_nat (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IAnd_nat (loc, k)); + } + | IAnd_int_nat (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IAnd_int_nat (loc, k)); + } + | IXor_nat (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IXor_nat (loc, k)); + } + | INot_int (loc, k), Item_t (_, s) -> + let s = Item_t (int_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> INot_int (loc, k)); + } + | IIf {loc; branch_if_true; branch_if_false; k}, Item_t (_, s) -> + ok + @@ Ex_split_if + { + left_init_stack = s; + left_branch = branch_if_true; + right_init_stack = s; + right_branch = branch_if_false; + continuation = k; + reconstruct = + (fun branch_if_true branch_if_false k -> + IIf {loc; branch_if_true; branch_if_false; k}); + } + | ILoop (loc, body, k), Item_t (_, s) -> + ok + @@ Ex_split_loop_may_fail + { + body_init_stack = s; + body; + cont_init_stack = s; + continuation = k; + reconstruct = (fun body k -> ILoop (loc, body, k)); + } + | ILoop_left (loc, kl, kr), Item_t (Union_t (a, b, _meta, _), s) -> + ok + @@ Ex_split_loop_may_fail + { + body_init_stack = Item_t (a, s); + body = kl; + cont_init_stack = Item_t (b, s); + continuation = kr; + reconstruct = (fun kl kr -> ILoop_left (loc, kl, kr)); + } + | IDip (loc, body, ty, k), Item_t (a, s) -> + ok + @@ Ex_split_loop_may_not_fail + { + body_init_stack = s; + body; + continuation = k; + aft_body_stack_transform = (fun s -> ok @@ Item_t (a, s)); + reconstruct = (fun body k -> IDip (loc, body, ty, k)); + } + | IExec (loc, sty, k), Item_t (_, Item_t (Lambda_t (_, b, _meta), s)) -> + let s = Item_t (b, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IExec (loc, sty, k)); + } + | ( IApply (loc, ty, k), + Item_t (_, Item_t (Lambda_t (Pair_t (_, a, _, _), b, _), s)) ) -> + lambda_t dummy a b >|? fun l -> + let s = Item_t (l, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IApply (loc, ty, k)); + } + | ILambda (loc, (Lam (desc, _) as l), k), s -> + let (Item_t (a, Bot_t)) = desc.kbef in + let (Item_t (b, Bot_t)) = desc.kaft in + lambda_t dummy a b >|? fun lam -> + let s = Item_t (lam, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ILambda (loc, l, k)); + } + | ILambda (loc, (LamRec (desc, _) as l), k), s -> + let (Item_t (a, Item_t (Lambda_t _, Bot_t))) = desc.kbef in + let (Item_t (b, Bot_t)) = desc.kaft in + lambda_t dummy a b >|? fun lam -> + let s = Item_t (lam, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ILambda (loc, l, k)); + } + | IFailwith (location, arg_ty), _ -> + ok + @@ Ex_split_failwith + {location; arg_ty; cast = {cast = IFailwith (location, arg_ty)}} + | ICompare (loc, ty, k), Item_t (_, Item_t (_, s)) -> + let s = Item_t (int_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ICompare (loc, ty, k)); + } + | IEq (loc, k), Item_t (_, s) -> + let s = Item_t (bool_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IEq (loc, k)); + } + | INeq (loc, k), Item_t (_, s) -> + let s = Item_t (bool_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> INeq (loc, k)); + } + | ILt (loc, k), Item_t (_, s) -> + let s = Item_t (bool_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ILt (loc, k)); + } + | IGt (loc, k), Item_t (_, s) -> + let s = Item_t (bool_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IGt (loc, k)); + } + | ILe (loc, k), Item_t (_, s) -> + let s = Item_t (bool_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ILe (loc, k)); + } + | IGe (loc, k), Item_t (_, s) -> + let s = Item_t (bool_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IGe (loc, k)); + } + | IAddress (loc, k), Item_t (_, s) -> + let s = Item_t (address_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IAddress (loc, k)); + } + | IContract (loc, ty, code, k), Item_t (_, s) -> + contract_t dummy ty >>? fun c -> + option_t dummy c >|? fun o -> + let s = Item_t (o, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IContract (loc, ty, code, k)); + } + | ITransfer_tokens (loc, k), Item_t (_, Item_t (_, Item_t (_, s))) -> + let s = Item_t (operation_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ITransfer_tokens (loc, k)); + } + | ( IView (loc, (View_signature {output_ty; _} as view_signature), sty, k), + Item_t (_, Item_t (_, s)) ) -> + option_t dummy output_ty >|? fun b -> + let s = Item_t (b, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IView (loc, view_signature, sty, k)); + } + | IImplicit_account (loc, k), Item_t (_, s) -> + let s = Item_t (contract_unit_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IImplicit_account (loc, k)); + } + | ( ICreate_contract {loc; storage_type; code; k}, + Item_t (_, Item_t (_, Item_t (_, s))) ) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = Item_t (operation_t, Item_t (address_t, s)); + continuation = k; + reconstruct = + (fun k -> ICreate_contract {loc; storage_type; code; k}); + } + | ISet_delegate (loc, k), Item_t (_, s) -> + let s = Item_t (operation_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISet_delegate (loc, k)); + } + | INow (loc, k), s -> + let s = Item_t (timestamp_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> INow (loc, k)); + } + | IBalance (loc, k), s -> + let s = Item_t (mutez_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IBalance (loc, k)); + } + | ILevel (loc, k), s -> + let s = Item_t (nat_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ILevel (loc, k)); + } + | ICheck_signature (loc, k), Item_t (_, Item_t (_, Item_t (_, s))) -> + let s = Item_t (bool_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ICheck_signature (loc, k)); + } + | IHash_key (loc, k), Item_t (_, s) -> + let s = Item_t (key_hash_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IHash_key (loc, k)); + } + | IPack (loc, ty, k), Item_t (_, s) -> + let s = Item_t (bytes_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IPack (loc, ty, k)); + } + | IUnpack (loc, ty, k), Item_t (_, s) -> + option_t dummy ty >|? fun o -> + let s = Item_t (o, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IUnpack (loc, ty, k)); + } + | IBlake2b (loc, k), s -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IBlake2b (loc, k)); + } + | ISha256 (loc, k), s -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISha256 (loc, k)); + } + | ISha512 (loc, k), s -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISha512 (loc, k)); + } + | ISource (loc, k), s -> + let s = Item_t (address_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISource (loc, k)); + } + | ISender (loc, k), s -> + let s = Item_t (address_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISender (loc, k)); + } + | ISelf (loc, ty, ep, k), s -> + contract_t dummy ty >|? fun c -> + let s = Item_t (c, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISelf (loc, ty, ep, k)); + } + | ISelf_address (loc, k), s -> + let s = Item_t (address_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISelf_address (loc, k)); + } + | IAmount (loc, k), s -> + let s = Item_t (mutez_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IAmount (loc, k)); + } + | ISapling_empty_state (loc, memo_size, k), s -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = Item_t (sapling_state_t ~memo_size, s); + continuation = k; + reconstruct = (fun k -> ISapling_empty_state (loc, memo_size, k)); + } + | ( ISapling_verify_update_deprecated (loc, k), + Item_t (_, Item_t (state_ty, s)) ) -> + pair_t dummy int_t state_ty >>? fun (Ty_ex_c pair_ty) -> + option_t dummy pair_ty >|? fun ty -> + Ex_split_kinstr + { + cont_init_stack = Item_t (ty, s); + continuation = k; + reconstruct = (fun k -> ISapling_verify_update_deprecated (loc, k)); + } + | ISapling_verify_update (loc, k), Item_t (_, Item_t (state_ty, s)) -> + pair_t dummy int_t state_ty >>? fun (Ty_ex_c int_state_ty) -> + pair_t dummy bytes_t int_state_ty >>? fun (Ty_ex_c pair_ty) -> + option_t dummy pair_ty >|? fun ty -> + let s = Item_t (ty, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISapling_verify_update (loc, k)); + } + | IDig (loc, n, p, k), s -> + let (Item_t (b, s)) = + stack_prefix_preservation_witness_split_input p s + in + let s = stack_prefix_preservation_witness_split_output p s in + let s = Item_t (b, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IDig (loc, n, p, k)); + } + | IDug (loc, n, p, k), Item_t (a, s) -> + let s = stack_prefix_preservation_witness_split_input p s in + let s = Item_t (a, s) in + let s = stack_prefix_preservation_witness_split_output p s in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IDug (loc, n, p, k)); + } + | IDipn (loc, n, p, k1, k2), s -> + ok + @@ Ex_split_loop_may_not_fail + { + body_init_stack = + stack_prefix_preservation_witness_split_input p s; + body = k1; + continuation = k2; + aft_body_stack_transform = + (fun s -> + ok @@ stack_prefix_preservation_witness_split_output p s); + reconstruct = (fun k1 k2 -> IDipn (loc, n, p, k1, k2)); + } + | IDropn (loc, n, p, k), s -> + let s = stack_prefix_preservation_witness_split_input p s in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IDropn (loc, n, p, k)); + } + | IChainId (loc, k), s -> + let s = Item_t (chain_id_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IChainId (loc, k)); + } + | INever location, Item_t (arg_ty, _) -> + ok + @@ Ex_split_failwith {location; arg_ty; cast = {cast = INever location}} + | IVoting_power (loc, k), Item_t (_, s) -> + let s = Item_t (nat_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IVoting_power (loc, k)); + } + | ITotal_voting_power (loc, k), s -> + let s = Item_t (nat_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ITotal_voting_power (loc, k)); + } + | IKeccak (loc, k), s -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IKeccak (loc, k)); + } + | ISha3 (loc, k), s -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISha3 (loc, k)); + } + | IAdd_bls12_381_g1 (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IAdd_bls12_381_g1 (loc, k)); + } + | IAdd_bls12_381_g2 (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IAdd_bls12_381_g2 (loc, k)); + } + | IAdd_bls12_381_fr (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IAdd_bls12_381_fr (loc, k)); + } + | IMul_bls12_381_g1 (loc, k), Item_t (g1, Item_t (_, s)) -> + let s = Item_t (g1, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IMul_bls12_381_g1 (loc, k)); + } + | IMul_bls12_381_g2 (loc, k), Item_t (g2, Item_t (_, s)) -> + let s = Item_t (g2, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IMul_bls12_381_g2 (loc, k)); + } + | IMul_bls12_381_fr (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IMul_bls12_381_fr (loc, k)); + } + | IMul_bls12_381_z_fr (loc, k), Item_t (fr, Item_t (_, s)) -> + let s = Item_t (fr, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IMul_bls12_381_z_fr (loc, k)); + } + | IMul_bls12_381_fr_z (loc, k), Item_t (_, s) -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IMul_bls12_381_fr_z (loc, k)); + } + | IInt_bls12_381_fr (loc, k), Item_t (_, s) -> + let s = Item_t (int_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IInt_bls12_381_fr (loc, k)); + } + | INeg_bls12_381_g1 (loc, k), s -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> INeg_bls12_381_g1 (loc, k)); + } + | INeg_bls12_381_g2 (loc, k), s -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> INeg_bls12_381_g2 (loc, k)); + } + | INeg_bls12_381_fr (loc, k), s -> + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> INeg_bls12_381_fr (loc, k)); + } + | IPairing_check_bls12_381 (loc, k), Item_t (_, s) -> + let s = Item_t (bool_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IPairing_check_bls12_381 (loc, k)); + } + | IComb (loc, n, p, k), s -> + let rec aux : + type a b s c d t. + (a, b * s) stack_ty -> + (a, b, s, c, d, t) comb_gadt_witness -> + (c, d * t) stack_ty tzresult = + fun s w -> + match (w, s) with + | Comb_one, s -> ok s + | Comb_succ w, Item_t (a, s) -> + aux s w >>? fun (Item_t (c, t)) -> + pair_t dummy a c >|? fun (Ty_ex_c p) -> Item_t (p, t) + in + aux s p >|? fun s -> + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IComb (loc, n, p, k)); + } + | IUncomb (loc, n, p, k), s -> + let rec aux : + type a b s c d t. + (a, b * s) stack_ty -> + (a, b, s, c, d, t) uncomb_gadt_witness -> + (c, d * t) stack_ty = + fun s w -> + match (w, s) with + | Uncomb_one, s -> s + | Uncomb_succ w, Item_t (Pair_t (a, b, _meta, _), s) -> + let s = aux (Item_t (b, s)) w in + Item_t (a, s) + in + let s = aux s p in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IUncomb (loc, n, p, k)); + } + | IComb_get (loc, n, p, k), Item_t (c, s) -> + let rec aux : + type c cc a. (c, cc) ty -> (c, a) comb_get_gadt_witness -> a ty_ex_c + = + fun c w -> + match (w, c) with + | Comb_get_zero, c -> Ty_ex_c c + | Comb_get_one, Pair_t (hd, _tl, _meta, _) -> Ty_ex_c hd + | Comb_get_plus_two w, Pair_t (_hd, tl, _meta, _) -> aux tl w + in + let s = + let (Ty_ex_c ty) = aux c p in + Item_t (ty, s) + in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IComb_get (loc, n, p, k)); + } + | IComb_set (loc, n, p, k), Item_t (a, Item_t (b, s)) -> + let rec aux : + type a b c ca cb. + (a, ca) ty -> + (b, cb) ty -> + (a, b, c) comb_set_gadt_witness -> + c ty_ex_c tzresult = + fun a b w -> + match (w, b) with + | Comb_set_zero, _ -> ok (Ty_ex_c a) + | Comb_set_one, Pair_t (_hd, tl, _meta, _) -> pair_t dummy a tl + | Comb_set_plus_two w, Pair_t (hd, tl, _meta, _) -> + aux a tl w >>? fun (Ty_ex_c c) -> pair_t dummy hd c + in + aux a b p >|? fun (Ty_ex_c c) -> + let s = Item_t (c, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IComb_set (loc, n, p, k)); + } + | IDup_n (loc, n, p, k), s -> + let rec aux : + type a b s t. + (a, b * s) stack_ty -> (a, b, s, t) dup_n_gadt_witness -> t ty_ex_c + = + fun s w -> + match (w, s) with + | Dup_n_succ w, Item_t (_, s) -> aux s w + | Dup_n_zero, Item_t (a, _) -> Ty_ex_c a + in + let s = + let (Ty_ex_c ty) = aux s p in + Item_t (ty, s) + in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IDup_n (loc, n, p, k)); + } + | ITicket (loc, cty, k), Item_t (_, Item_t (_, s)) -> + ticket_t dummy (assert_some cty) >>? option_t loc >|? fun t -> + let s = Item_t (t, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ITicket (loc, cty, k)); + } + | ITicket_deprecated (loc, cty, k), Item_t (_, Item_t (_, s)) -> + ticket_t dummy (assert_some cty) >|? fun t -> + let s = Item_t (t, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ITicket_deprecated (loc, cty, k)); + } + | IRead_ticket (loc, a, k), s -> + pair_t dummy (assert_some a) nat_t >>? fun (Ty_ex_c p) -> + pair_t dummy address_t p >|? fun (Ty_ex_c t) -> + let s = Item_t (t, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IRead_ticket (loc, a, k)); + } + | ISplit_ticket (loc, k), Item_t (t, Item_t (_, s)) -> + pair_t dummy t t >>? fun (Ty_ex_c p) -> + option_t dummy p >|? fun o -> + let s = Item_t (o, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> ISplit_ticket (loc, k)); + } + | IJoin_tickets (loc, ty, k), Item_t (Pair_t (t, _t, _meta, _), s) -> + option_t dummy t >|? fun o -> + let s = Item_t (o, s) in + Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IJoin_tickets (loc, ty, k)); + } + | IOpen_chest (loc, k), Item_t (_, Item_t (_, Item_t (_, s))) -> + let s = Item_t (union_bytes_bool_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IOpen_chest (loc, k)); + } + | IMin_block_time (loc, k), s -> + let s = Item_t (nat_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IMin_block_time (loc, k)); + } + | IEmit {loc; ty; unparsed_ty; tag; k}, Item_t (_, s) -> + let s = Item_t (operation_t, s) in + ok + @@ Ex_split_kinstr + { + cont_init_stack = s; + continuation = k; + reconstruct = (fun k -> IEmit {loc; ty; unparsed_ty; tag; k}); + } + | IEmit _, Bot_t -> . + | IHalt loc, _s -> ok @@ Ex_split_halt loc + | ILog (loc, _stack_ty, event, logger, continuation), stack -> + ok + @@ Ex_split_log + { + stack; + continuation; + reconstruct = (fun k -> ILog (loc, s, event, logger, k)); + } + + (* [kinstr_final_stack_type sty instr] computes the stack type after + [instr] has been executed, assuming [sty] is the type of the stack + prior to execution. For the rare instructions which can return stacks + of any type ([FAILWITH] and [NEVER]), this function returns [None]. *) + let rec kinstr_final_stack_type : + type a s r f. + (a, s) stack_ty -> (a, s, r, f) kinstr -> (r, f) stack_ty option tzresult + = + fun s i -> + kinstr_split s i >>? function + | Ex_split_kinstr {cont_init_stack; continuation; _} -> + kinstr_final_stack_type cont_init_stack continuation + | Ex_split_log {stack; continuation; _} -> + kinstr_final_stack_type stack continuation + | Ex_split_loop_may_fail {cont_init_stack; continuation; _} -> + kinstr_final_stack_type cont_init_stack continuation + | Ex_split_loop_may_not_fail + {body_init_stack; body; continuation; aft_body_stack_transform; _} -> ( + kinstr_final_stack_type body_init_stack body >>? function + | Some after_body -> + aft_body_stack_transform after_body >>? fun before_k -> + kinstr_final_stack_type before_k continuation + | None -> ok None) + | Ex_split_if + { + left_init_stack; + left_branch; + right_init_stack; + right_branch; + continuation; + _; + } -> ( + kinstr_final_stack_type left_init_stack left_branch >>? function + | Some after_branch_a -> + kinstr_final_stack_type after_branch_a continuation + | None -> ( + kinstr_final_stack_type right_init_stack right_branch >>? function + | Some after_branch_b -> + kinstr_final_stack_type after_branch_b continuation + | None -> ok None)) + | Ex_split_halt _ -> ok @@ Some s + | Ex_split_failwith {cast = {cast = _}; _} -> ok None + + (* The same as [kinstr_final_stack_type], but selects from multiple + possible execution branches. If the first instr ends with FAILWITH, + it will try the next and so on. Note that all instructions must + result in the same stack type. *) + let rec branched_final_stack_type : + type r f. (r, f) ex_init_stack_ty list -> (r, f) stack_ty option tzresult + = function + | [] -> ok None + | Ex_init_stack_ty (init_sty, branch) :: bs -> ( + kinstr_final_stack_type init_sty branch >>? function + | Some _ as sty -> ok sty + | None -> branched_final_stack_type bs) + + let kinstr_rewritek : + type a s r f. + (a, s) stack_ty -> + (a, s, r, f) kinstr -> + kinstr_rewritek -> + (a, s, r, f) kinstr tzresult = + fun s i f -> + kinstr_split s i >>? function + | Ex_split_kinstr {cont_init_stack; continuation; reconstruct} -> + ok @@ reconstruct (f.apply cont_init_stack continuation) + | Ex_split_log {continuation; reconstruct; _} -> + ok @@ reconstruct continuation + | Ex_split_loop_may_fail + {body_init_stack; body; cont_init_stack; continuation; reconstruct} -> + ok + @@ reconstruct + (f.apply body_init_stack body) + (f.apply cont_init_stack continuation) + | Ex_split_loop_may_not_fail + { + body_init_stack; + body; + continuation; + aft_body_stack_transform; + reconstruct; + } -> + (kinstr_final_stack_type body_init_stack body >>? function + | Some after_body -> + aft_body_stack_transform after_body >|? fun before_k -> + f.apply before_k continuation + | None -> ok continuation) + >|? fun k -> reconstruct (f.apply body_init_stack body) k + | Ex_split_if + { + left_init_stack; + left_branch; + right_init_stack; + right_branch; + continuation; + reconstruct; + } -> + (kinstr_final_stack_type left_init_stack left_branch >>? function + | Some after_left_branch -> + ok @@ f.apply after_left_branch continuation + | None -> ( + kinstr_final_stack_type right_init_stack right_branch >>? function + | Some after_right_branch -> + ok @@ f.apply after_right_branch continuation + | None -> ok continuation)) + >|? fun k -> + reconstruct + (f.apply left_init_stack left_branch) + (f.apply right_init_stack right_branch) + k + | Ex_split_halt loc -> ok @@ IHalt loc + | Ex_split_failwith {location; arg_ty; _} -> + ok @@ IFailwith (location, arg_ty) + + (** [dipn_stack_ty witness stack_ty] returns the type of the stack + on which instructions inside dipped block will be operating. *) + let rec dipn_stack_ty : + type a s e z c u d w. + (a, s, e, z, c, u, d, w) stack_prefix_preservation_witness -> + (c, u) stack_ty -> + (a, s) stack_ty = + fun witness stack -> + match (witness, stack) with + | KPrefix (_, _, witness'), Item_t (_, sty) -> dipn_stack_ty witness' sty + | KRest, sty -> sty + + (** [instrument_cont logger sty] creates a function instrumenting + continuations starting from the stack type described by [sty]. + Instrumentation consists in wrapping inner continuations in + [KLog] continuation so that logging continues. *) + let instrument_cont : + type a b c d. + logger -> + (a, b) stack_ty -> + (a, b, c, d) continuation -> + (a, b, c, d) continuation = + fun logger sty -> function KLog _ as k -> k | k -> KLog (k, sty, logger) +end + +module type Logger_base = sig + val log_interp : ('a, 's, 'b, 'f, 'c, 'u) logging_function + + val log_entry : ('a, 's, 'b, 'f, 'a, 's) logging_function + + val log_control : ('a, 's, 'b, 'f) continuation -> unit + + val log_exit : ('a, 's, 'b, 'f, 'c, 'u) logging_function + + val get_log : unit -> execution_trace option tzresult Lwt.t +end + +module Logger (Base : Logger_base) = struct + open Stack_utils + open Local_gas_counter + open Script_interpreter_defs + open Script_interpreter.Internals.Raw + + (** [log_entry ctxt gas instr sty accu stack] simply calls the + [Base.log_entry] function with the appropriate arguments. *) + let log_entry ctxt gas k sty accu stack = + let ctxt = Local_gas_counter.update_context gas ctxt in + Base.log_entry k ctxt (kinstr_location k) sty (accu, stack) + + (** [log_exit ctxt gas loc instr sty accu stack] simply calls the + [Base.log_exit] function with the appropriate arguments. *) + let log_exit ctxt gas loc_prev k sty accu stack = + let ctxt = Local_gas_counter.update_context gas ctxt in + Base.log_exit k ctxt loc_prev sty (accu, stack) + + (** [log_control continuation] simply calls the [Base.log_control] + function with the appropriate arguments. *) + let log_control ks = Base.log_control ks + + (** [log_kinstr logger sty instr] returns [instr] prefixed by an + [ILog] instruction to log the first instruction in [instr]. *) + let log_kinstr logger sty i = + ILog (kinstr_location i, sty, LogEntry, logger, i) + + (* [log_next_kinstr logger i] instruments the next instruction of [i] + with [ILog] instructions to make sure it will be logged. + This instrumentation has a performance cost, but importantly, it is + only ever paid when logging is enabled. Otherwise, the possibility + to instrument the script is costless. + + Notice that the instrumentation breaks the sharing of continuations + that is normally enforced between branches of conditionals. This + has a performance cost. Anyway, the instrumentation allocates many + new [ILog] instructions and [KLog] continuations which makes + the execution of instrumented code significantly slower than + non-instrumented code. "Zero-cost logging" means that the normal + non-instrumented execution is not impacted by the ability to + instrument it, not that the logging itself has no cost. + *) + let log_next_kinstr logger sty i = + let apply sty k = + ILog + ( kinstr_location k, + sty, + LogExit (kinstr_location i), + logger, + log_kinstr logger sty k ) + in + kinstr_rewritek sty i {apply} + + (** [log_next_continuation logger sty cont] instruments the next + continuation in [cont] with [KLog] continuations to ensure + logging. + + This instrumentation has a performance cost, but importantly, it + is only ever paid when logging is enabled. Otherwise, the + possibility to instrument the script is costless. *) + let log_next_continuation : + type a b c d. + logger -> + (a, b) stack_ty -> + (a, b, c, d) continuation -> + (a, b, c, d) continuation tzresult = + fun logger stack_ty cont -> + let enable_log sty ki = log_kinstr logger sty ki in + match cont with + | KCons (ki, k) -> ( + let ki' = enable_log stack_ty ki in + kinstr_final_stack_type stack_ty ki >|? function + | None -> KCons (ki', k) + | Some sty -> KCons (ki', instrument_cont logger sty k)) + | KLoop_in (ki, k) -> + let (Item_t (Bool_t, sty)) = stack_ty in + ok @@ KLoop_in (enable_log sty ki, instrument_cont logger sty k) + | KReturn (stack, sty, k) -> + let k' = instrument_cont logger (assert_some sty) k in + ok @@ KReturn (stack, sty, k') + | KLoop_in_left (ki, k) -> + let (Item_t (Union_t (a_ty, b_ty, _, _), rest)) = stack_ty in + let ki' = enable_log (Item_t (a_ty, rest)) ki in + let k' = instrument_cont logger (Item_t (b_ty, rest)) k in + ok @@ KLoop_in_left (ki', k') + | KUndip (x, ty, k) -> + let k' = instrument_cont logger (Item_t (assert_some ty, stack_ty)) k in + ok @@ KUndip (x, ty, k') + | KIter (body, xty, xs, k) -> + let body' = enable_log (Item_t (assert_some xty, stack_ty)) body in + let k' = instrument_cont logger stack_ty k in + ok @@ KIter (body', xty, xs, k') + | KList_enter_body (body, xs, ys, ty, len, k) -> + let k' = instrument_cont logger (Item_t (assert_some ty, stack_ty)) k in + ok @@ KList_enter_body (body, xs, ys, ty, len, k') + | KList_exit_body (body, xs, ys, ty, len, k) -> + let (Item_t (_, sty)) = stack_ty in + let k' = instrument_cont logger (Item_t (assert_some ty, sty)) k in + ok @@ KList_exit_body (body, xs, ys, ty, len, k') + | KMap_enter_body (body, xs, ys, ty, k) -> + let k' = instrument_cont logger (Item_t (assert_some ty, stack_ty)) k in + ok @@ KMap_enter_body (body, xs, ys, ty, k') + | KMap_exit_body (body, xs, ys, yk, ty, k) -> + let (Item_t (_, sty)) = stack_ty in + let k' = instrument_cont logger (Item_t (assert_some ty, sty)) k in + ok @@ KMap_exit_body (body, xs, ys, yk, ty, k') + | KMap_head (_, _) + | KView_exit (_, _) + | KLog _ (* This case should never happen. *) | KNil -> + ok cont + + (* + + Zero-cost logging + ================= + + *) + + (* + + The following functions insert a logging instruction to continue + the logging process in the next execution steps. + + There is a special treatment of instructions that generate fresh + continuations: we pass a constructor as argument to their + evaluation rules so that they can instrument these fresh + continuations by themselves. Instructions that create continuations + without calling specialized functions have their branches from [step] + function duplicated and adjusted here. + + This on-the-fly instrumentation of the execution allows zero-cost + logging since logging instructions are only introduced if an + initial logging continuation is pushed in the initial continuation + that starts the evaluation. + + *) + let ilog : + type a s b t r f. + logger -> logging_event -> (a, s) stack_ty -> (a, s, b, t, r, f) step_type + = + fun logger event sty ((ctxt, _) as g) gas k ks accu stack -> + (match (k, event) with + | ILog _, LogEntry -> () + | _, LogEntry -> log_entry ctxt gas k sty accu stack + | _, LogExit prev_loc -> log_exit ctxt gas prev_loc k sty accu stack) ; + log_next_kinstr logger sty k >>?= fun k -> + (* We need to match on instructions that create continuations so + that we can instrument those continuations with [KLog] (see + comment above). For functions that don't do this, we simply call + [step], as they don't require any special treatment. *) + match k with + | IIf_none {branch_if_none; branch_if_some; k; _} -> ( + let (Item_t (Option_t (ty, _, _), rest)) = sty in + branched_final_stack_type + [ + Ex_init_stack_ty (rest, branch_if_none); + Ex_init_stack_ty (Item_t (ty, rest), branch_if_some); + ] + >>?= fun sty_opt -> + let ks' = + match sty_opt with + | None -> KCons (k, ks) + | Some sty' -> instrument_cont logger sty' @@ KCons (k, ks) + in + match accu with + | None -> + let accu, stack = stack in + (step [@ocaml.tailcall]) g gas branch_if_none ks' accu stack + | Some v -> (step [@ocaml.tailcall]) g gas branch_if_some ks' v stack) + | IOpt_map {body; k; loc = _} -> ( + match accu with + | None -> (step [@ocaml.tailcall]) g gas k ks None stack + | Some v -> + let (Item_t (Option_t (ty, _, _), rest)) = sty in + let bsty = Item_t (ty, rest) in + let kmap_head = KMap_head (Option.some, KCons (k, ks)) in + kinstr_final_stack_type bsty body >>?= fun sty_opt -> + let ks' = + match sty_opt with + | None -> kmap_head + | Some sty' -> instrument_cont logger sty' kmap_head + in + (step [@ocaml.tailcall]) g gas body ks' v stack) + | IIf_left {branch_if_left; branch_if_right; k; _} -> ( + let (Item_t (Union_t (lty, rty, _, _), rest)) = sty in + branched_final_stack_type + [ + Ex_init_stack_ty (Item_t (lty, rest), branch_if_left); + Ex_init_stack_ty (Item_t (rty, rest), branch_if_right); + ] + >>?= fun sty_opt -> + let k' = + match sty_opt with + | None -> KCons (k, ks) + | Some sty' -> instrument_cont logger sty' @@ KCons (k, ks) + in + match accu with + | L v -> (step [@ocaml.tailcall]) g gas branch_if_left k' v stack + | R v -> (step [@ocaml.tailcall]) g gas branch_if_right k' v stack) + | IIf_cons {branch_if_cons; branch_if_nil; k; _} -> ( + let (Item_t ((List_t (elty, _) as lty), rest)) = sty in + branched_final_stack_type + [ + Ex_init_stack_ty (rest, branch_if_nil); + Ex_init_stack_ty (Item_t (elty, Item_t (lty, rest)), branch_if_cons); + ] + >>?= fun sty' -> + let k' = + match sty' with + | None -> KCons (k, ks) + | Some sty' -> instrument_cont logger sty' @@ KCons (k, ks) + in + match Script_list.uncons accu with + | None -> + let accu, stack = stack in + (step [@ocaml.tailcall]) g gas branch_if_nil k' accu stack + | Some (hd, tl) -> + (step [@ocaml.tailcall]) g gas branch_if_cons k' hd (tl, stack)) + | IList_map (_, body, ty, k) -> + let (Item_t (_, sty')) = sty in + let instrument = instrument_cont logger sty' in + (ilist_map [@ocaml.tailcall]) instrument g gas body k ks ty accu stack + | IList_iter (_, ty, body, k) -> + let (Item_t (_, sty')) = sty in + let instrument = instrument_cont logger sty' in + (ilist_iter [@ocaml.tailcall]) instrument g gas body ty k ks accu stack + | ISet_iter (_, ty, body, k) -> + let (Item_t (_, rest)) = sty in + let instrument = instrument_cont logger rest in + (iset_iter [@ocaml.tailcall]) instrument g gas body ty k ks accu stack + | IMap_map (_, ty, body, k) -> + let (Item_t (_, rest)) = sty in + let instrument = instrument_cont logger rest in + (imap_map [@ocaml.tailcall]) instrument g gas body k ks ty accu stack + | IMap_iter (_, kvty, body, k) -> + let (Item_t (_, rest)) = sty in + let instrument = instrument_cont logger rest in + (imap_iter [@ocaml.tailcall]) instrument g gas body kvty k ks accu stack + | IMul_teznat (loc, k) -> + (imul_teznat [@ocaml.tailcall]) (Some logger) g gas loc k ks accu stack + | IMul_nattez (loc, k) -> + (imul_nattez [@ocaml.tailcall]) (Some logger) g gas loc k ks accu stack + | ILsl_nat (loc, k) -> + (ilsl_nat [@ocaml.tailcall]) (Some logger) g gas loc k ks accu stack + | ILsr_nat (loc, k) -> + (ilsr_nat [@ocaml.tailcall]) (Some logger) g gas loc k ks accu stack + | IIf {branch_if_true; branch_if_false; k; _} -> + let (Item_t (Bool_t, rest)) = sty in + branched_final_stack_type + [ + Ex_init_stack_ty (rest, branch_if_true); + Ex_init_stack_ty (rest, branch_if_false); + ] + >>?= fun sty' -> + let k' = + match sty' with + | None -> KCons (k, ks) + | Some sty' -> instrument_cont logger sty' @@ KCons (k, ks) + in + let res, stack = stack in + if accu then (step [@ocaml.tailcall]) g gas branch_if_true k' res stack + else (step [@ocaml.tailcall]) g gas branch_if_false k' res stack + | ILoop (_, body, k) -> + let ks = instrument_cont logger sty @@ KLoop_in (body, KCons (k, ks)) in + (next [@ocaml.tailcall]) g gas ks accu stack + | ILoop_left (_, bl, br) -> + let ks = + instrument_cont logger sty @@ KLoop_in_left (bl, KCons (br, ks)) + in + (next [@ocaml.tailcall]) g gas ks accu stack + | IDip (_, b, ty, k) -> + let (Item_t (_, rest)) = sty in + kinstr_final_stack_type rest b >>?= fun rest' -> + let ign = accu in + let ks = + match rest' with + | None -> KUndip (ign, ty, KCons (k, ks)) + | Some rest' -> + instrument_cont logger rest' (KUndip (ign, ty, KCons (k, ks))) + in + let accu, stack = stack in + (step [@ocaml.tailcall]) g gas b ks accu stack + | IExec (_, stack_ty, k) -> + let (Item_t (_, Item_t (Lambda_t (_, ret, _), _))) = sty in + let sty' = Item_t (ret, Bot_t) in + let instrument = instrument_cont logger sty' in + iexec instrument (Some logger) g gas stack_ty k ks accu stack + | IFailwith (kloc, tv) -> + let {ifailwith} = ifailwith in + (ifailwith [@ocaml.tailcall]) (Some logger) g gas kloc tv accu + | IDipn (_, _n, n', b, k) -> + let accu, stack, restore_prefix = kundip n' accu stack k in + let dipped_sty = dipn_stack_ty n' sty in + kinstr_final_stack_type dipped_sty b >>?= fun sty' -> + let ks = + match sty' with + | None -> KCons (restore_prefix, ks) + | Some sty' -> + instrument_cont logger sty' @@ KCons (restore_prefix, ks) + in + (step [@ocaml.tailcall]) g gas b ks accu stack + | IView (_, (View_signature {output_ty; _} as view_signature), stack_ty, k) + -> + let sty' = Item_t (output_ty, Bot_t) in + let instrument = instrument_cont logger sty' in + (iview [@ocaml.tailcall]) + instrument + g + gas + view_signature + stack_ty + k + ks + accu + stack + | _ -> (step [@ocaml.tailcall]) g gas k ks accu stack + [@@inline] + + let klog : + type a s r f. + logger -> + outdated_context * step_constants -> + local_gas_counter -> + (a, s) stack_ty -> + (a, s, r, f) continuation -> + (a, s, r, f) continuation -> + a -> + s -> + (r * f * outdated_context * local_gas_counter) tzresult Lwt.t = + fun logger g gas stack_ty k0 ks accu stack -> + let ty_for_logging_unsafe = function + (* This function is only called when logging is enabled. If + that's the case, the elaborator must have been called with + [logging_enabled] option, which ensures that this will not be + [None]. Realistically, it can happen that the [logging_enabled] + option was omitted, resulting in a crash here. But this is + acceptable, because logging is never enabled during block + validation, so the layer 1 is safe. *) + | None -> assert false + | Some ty -> ty + in + (match ks with KLog _ -> () | _ -> log_control ks) ; + log_next_continuation logger stack_ty ks >>?= function + | KCons (ki, k) -> (step [@ocaml.tailcall]) g gas ki k accu stack + | KLoop_in (ki, k) -> (kloop_in [@ocaml.tailcall]) g gas k0 ki k accu stack + | KReturn (_, _, _) as k -> (next [@ocaml.tailcall]) g gas k accu stack + | KLoop_in_left (ki, k) -> + (kloop_in_left [@ocaml.tailcall]) g gas k0 ki k accu stack + | KUndip (_, _, _) as k -> (next [@ocaml.tailcall]) g gas k accu stack + | KIter (body, xty, xs, k) -> + let instrument = instrument_cont logger stack_ty in + (kiter [@ocaml.tailcall]) instrument g gas body xty xs k accu stack + | KList_enter_body (body, xs, ys, ty_opt, len, k) -> + let instrument = + let ty = ty_for_logging_unsafe ty_opt in + let (List_t (vty, _)) = ty in + let sty = Item_t (vty, stack_ty) in + instrument_cont logger sty + in + (klist_enter [@ocaml.tailcall]) + instrument + g + gas + body + xs + ys + ty_opt + len + k + accu + stack + | KList_exit_body (body, xs, ys, ty_opt, len, k) -> + let (Item_t (_, rest)) = stack_ty in + let instrument = instrument_cont logger rest in + (klist_exit [@ocaml.tailcall]) + instrument + g + gas + body + xs + ys + ty_opt + len + k + accu + stack + | KMap_enter_body (body, xs, ys, ty_opt, k) -> + let instrument = + let ty = ty_for_logging_unsafe ty_opt in + let (Map_t (_, vty, _)) = ty in + let sty = Item_t (vty, stack_ty) in + instrument_cont logger sty + in + (kmap_enter [@ocaml.tailcall]) + instrument + g + gas + body + xs + ty_opt + ys + k + accu + stack + | KMap_exit_body (body, xs, ys, yk, ty_opt, k) -> + let (Item_t (_, rest)) = stack_ty in + let instrument = instrument_cont logger rest in + (kmap_exit [@ocaml.tailcall]) + instrument + g + gas + body + xs + ty_opt + ys + yk + k + accu + stack + | KMap_head (f, k) -> (next [@ocaml.taillcall]) g gas k (f accu) stack + | KView_exit (scs, k) -> + (next [@ocaml.tailcall]) (fst g, scs) gas k accu stack + | KLog _ as k -> + (* This case should never happen. *) + (next [@ocaml.tailcall]) g gas k accu stack + | KNil as k -> (next [@ocaml.tailcall]) g gas k accu stack + [@@inline] +end + +let make (module Base : Logger_base) = + let module Logger = Logger (Base) in + let open Logger in + let open Base in + {log_interp; get_log; log_kinstr; klog; ilog} diff --git a/src/proto_alpha/lib_plugin/script_interpreter_logging.mli b/src/proto_alpha/lib_plugin/script_interpreter_logging.mli new file mode 100644 index 0000000000000000000000000000000000000000..0492bab3c3120596ad16f9dea0ac0dbf48cad7d5 --- /dev/null +++ b/src/proto_alpha/lib_plugin/script_interpreter_logging.mli @@ -0,0 +1,43 @@ +(*****************************************************************************) +(* *) +(* Open Source License *) +(* Copyright (c) 2022 Nomadic Labs *) +(* *) +(* Permission is hereby granted, free of charge, to any person obtaining a *) +(* copy of this software and associated documentation files (the "Software"),*) +(* to deal in the Software without restriction, including without limitation *) +(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *) +(* and/or sell copies of the Software, and to permit persons to whom the *) +(* Software is furnished to do so, subject to the following conditions: *) +(* *) +(* The above copyright notice and this permission notice shall be included *) +(* in all copies or substantial portions of the Software. *) +(* *) +(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*) +(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *) +(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *) +(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*) +(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *) +(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *) +(* DEALINGS IN THE SOFTWARE. *) +(* *) +(*****************************************************************************) + +open Protocol +open Environment +open Error_monad +open Script_typed_ir + +module type Logger_base = sig + val log_interp : ('a, 's, 'b, 'f, 'c, 'u) logging_function + + val log_entry : ('a, 's, 'b, 'f, 'a, 's) logging_function + + val log_control : ('a, 's, 'b, 'f) continuation -> unit + + val log_exit : ('a, 's, 'b, 'f, 'c, 'u) logging_function + + val get_log : unit -> execution_trace option tzresult Lwt.t +end + +val make : (module Logger_base) -> logger diff --git a/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL b/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL index a8ae4f108e05072f1c21db480bc6d32ccc7f1fe9..69d336c8fb180de7c8de98d94d4284065429b33e 100644 --- a/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL +++ b/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL @@ -236,7 +236,6 @@ "Tx_rollup_ticket", "Script_interpreter_defs", - "Script_interpreter_logging", "Script_interpreter", "Sc_rollup_management_protocol", "Sc_rollup_operations", diff --git a/src/proto_alpha/lib_protocol/dune b/src/proto_alpha/lib_protocol/dune index 5ea086515edc06bfa8ddbf1d18fc2851ea3db18b..2caa12aa0a9a6df1d8662aef4a3f61c564ea2618 100644 --- a/src/proto_alpha/lib_protocol/dune +++ b/src/proto_alpha/lib_protocol/dune @@ -243,7 +243,6 @@ Ticket_accounting Tx_rollup_ticket Script_interpreter_defs - Script_interpreter_logging Script_interpreter Sc_rollup_management_protocol Sc_rollup_operations @@ -515,7 +514,6 @@ ticket_accounting.ml ticket_accounting.mli tx_rollup_ticket.ml tx_rollup_ticket.mli script_interpreter_defs.ml - script_interpreter_logging.ml script_interpreter_logging.mli script_interpreter.ml script_interpreter.mli sc_rollup_management_protocol.ml sc_rollup_management_protocol.mli sc_rollup_operations.ml sc_rollup_operations.mli @@ -767,7 +765,6 @@ ticket_accounting.ml ticket_accounting.mli tx_rollup_ticket.ml tx_rollup_ticket.mli script_interpreter_defs.ml - script_interpreter_logging.ml script_interpreter_logging.mli script_interpreter.ml script_interpreter.mli sc_rollup_management_protocol.ml sc_rollup_management_protocol.mli sc_rollup_operations.ml sc_rollup_operations.mli @@ -1024,7 +1021,6 @@ ticket_accounting.ml ticket_accounting.mli tx_rollup_ticket.ml tx_rollup_ticket.mli script_interpreter_defs.ml - script_interpreter_logging.ml script_interpreter_logging.mli script_interpreter.ml script_interpreter.mli sc_rollup_management_protocol.ml sc_rollup_management_protocol.mli sc_rollup_operations.ml sc_rollup_operations.mli diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml index 76b33e1c92914eb478e870180803cbcdc1d52a82..765a3ec876b987db4e495a2c26b68ad213b1c880 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter.ml @@ -234,7 +234,8 @@ let () = *) -(* +module Raw = struct + (* Evaluation of continuations =========================== @@ -251,131 +252,143 @@ let () = evaluation is logged. *) -let rec kmap_exit : - type a b c e f m n o. (a, b, c, e, f, m, n, o) kmap_exit_type = - fun instrument g gas body xs ty ys yk ks accu stack -> - let ys = Script_map.update yk (Some accu) ys in - let ks = instrument @@ KMap_enter_body (body, xs, ys, ty, ks) in - let accu, stack = stack in - (next [@ocaml.tailcall]) g gas ks accu stack - [@@inline] - -and kmap_enter : type a b c d f i j k. (a, b, c, d, f, i, j, k) kmap_enter_type - = - fun instrument g gas body xs ty ys ks accu stack -> - match xs with - | [] -> (next [@ocaml.tailcall]) g gas ks ys (accu, stack) - | (xk, xv) :: xs -> - let ks = instrument @@ KMap_exit_body (body, xs, ys, xk, ty, ks) in - let res = (xk, xv) in - let stack = (accu, stack) in - (step [@ocaml.tailcall]) g gas body ks res stack - [@@inline] - -and klist_exit : type a b c d e i j. (a, b, c, d, e, i, j) klist_exit_type = - fun instrument g gas body xs ys ty len ks accu stack -> - let ys = Script_list.cons accu ys in - let ks = instrument @@ KList_enter_body (body, xs, ys, ty, len, ks) in - let accu, stack = stack in - (next [@ocaml.tailcall]) g gas ks accu stack - [@@inline] - -and klist_enter : type a b c d e f j. (a, b, c, d, e, f, j) klist_enter_type = - fun instrument g gas body xs ys ty len ks' accu stack -> - match xs with - | [] -> - let ys = Script_list.rev ys in - (next [@ocaml.tailcall]) g gas ks' ys (accu, stack) - | x :: xs -> - let ks = instrument @@ KList_exit_body (body, xs, ys, ty, len, ks') in - (step [@ocaml.tailcall]) g gas body ks x (accu, stack) - [@@inline] - -and kloop_in_left : type a b c d e f g. (a, b, c, d, e, f, g) kloop_in_left_type - = - fun g gas ks0 ki ks' accu stack -> - match accu with - | L v -> (step [@ocaml.tailcall]) g gas ki ks0 v stack - | R v -> (next [@ocaml.tailcall]) g gas ks' v stack - [@@inline] - -and kloop_in : type a b c r f s. (a, b, c, r, f, s) kloop_in_type = - fun g gas ks0 ki ks' accu stack -> - let accu', stack' = stack in - if accu then (step [@ocaml.tailcall]) g gas ki ks0 accu' stack' - else (next [@ocaml.tailcall]) g gas ks' accu' stack' - [@@inline] - -and kiter : type a b s r f c. (a, b, s, r, f, c) kiter_type = - fun instrument g gas body ty xs ks accu stack -> - match xs with - | [] -> (next [@ocaml.tailcall]) g gas ks accu stack - | x :: xs -> - let ks = instrument @@ KIter (body, ty, xs, ks) in - (step [@ocaml.tailcall]) g gas body ks x (accu, stack) - [@@inline] - -and next : - type a s r f. - outdated_context * step_constants -> - local_gas_counter -> - (a, s, r, f) continuation -> - a -> - s -> - (r * f * outdated_context * local_gas_counter) tzresult Lwt.t = - fun ((ctxt, _) as g) gas ks0 accu stack -> - match consume_control gas ks0 with - | None -> fail Gas.Operation_quota_exceeded - | Some gas -> ( - match ks0 with - | KLog (ks, sty, logger) -> - (klog [@ocaml.tailcall]) logger g gas sty ks0 ks accu stack - | KNil -> Lwt.return (Ok (accu, stack, ctxt, gas)) - | KCons (k, ks) -> (step [@ocaml.tailcall]) g gas k ks accu stack - | KLoop_in (ki, ks') -> - (kloop_in [@ocaml.tailcall]) g gas ks0 ki ks' accu stack - | KReturn (stack', _, ks) -> (next [@ocaml.tailcall]) g gas ks accu stack' - | KMap_head (f, ks) -> (next [@ocaml.tailcall]) g gas ks (f accu) stack - | KLoop_in_left (ki, ks') -> - (kloop_in_left [@ocaml.tailcall]) g gas ks0 ki ks' accu stack - | KUndip (x, _, ks) -> (next [@ocaml.tailcall]) g gas ks x (accu, stack) - | KIter (body, ty, xs, ks) -> - (kiter [@ocaml.tailcall]) id g gas body ty xs ks accu stack - | KList_enter_body (body, xs, ys, ty, len, ks) -> - (klist_enter [@ocaml.tailcall]) - id - g - gas - body - xs - ys - ty - len - ks - accu - stack - | KList_exit_body (body, xs, ys, ty, len, ks) -> - (klist_exit [@ocaml.tailcall]) - id - g - gas - body - xs - ys - ty - len - ks - accu - stack - | KMap_enter_body (body, xs, ys, ty, ks) -> - (kmap_enter [@ocaml.tailcall]) id g gas body xs ty ys ks accu stack - | KMap_exit_body (body, xs, ys, yk, ty, ks) -> - (kmap_exit [@ocaml.tailcall]) id g gas body xs ty ys yk ks accu stack - | KView_exit (orig_step_constants, ks) -> - let g = (fst g, orig_step_constants) in - (next [@ocaml.tailcall]) g gas ks accu stack) + let rec kmap_exit : + type a b c e f m n o. (a, b, c, e, f, m, n, o) kmap_exit_type = + fun instrument g gas body xs ty ys yk ks accu stack -> + let ys = Script_map.update yk (Some accu) ys in + let ks = instrument @@ KMap_enter_body (body, xs, ys, ty, ks) in + let accu, stack = stack in + (next [@ocaml.tailcall]) g gas ks accu stack + [@@inline] + + and kmap_enter : + type a b c d f i j k. (a, b, c, d, f, i, j, k) kmap_enter_type = + fun instrument g gas body xs ty ys ks accu stack -> + match xs with + | [] -> (next [@ocaml.tailcall]) g gas ks ys (accu, stack) + | (xk, xv) :: xs -> + let ks = instrument @@ KMap_exit_body (body, xs, ys, xk, ty, ks) in + let res = (xk, xv) in + let stack = (accu, stack) in + (step [@ocaml.tailcall]) g gas body ks res stack + [@@inline] + + and klist_exit : type a b c d e i j. (a, b, c, d, e, i, j) klist_exit_type = + fun instrument g gas body xs ys ty len ks accu stack -> + let ys = Script_list.cons accu ys in + let ks = instrument @@ KList_enter_body (body, xs, ys, ty, len, ks) in + let accu, stack = stack in + (next [@ocaml.tailcall]) g gas ks accu stack + [@@inline] + + and klist_enter : type a b c d e f j. (a, b, c, d, e, f, j) klist_enter_type = + fun instrument g gas body xs ys ty len ks' accu stack -> + match xs with + | [] -> + let ys = Script_list.rev ys in + (next [@ocaml.tailcall]) g gas ks' ys (accu, stack) + | x :: xs -> + let ks = instrument @@ KList_exit_body (body, xs, ys, ty, len, ks') in + (step [@ocaml.tailcall]) g gas body ks x (accu, stack) + [@@inline] + + and kloop_in_left : + type a b c d e f g. (a, b, c, d, e, f, g) kloop_in_left_type = + fun g gas ks0 ki ks' accu stack -> + match accu with + | L v -> (step [@ocaml.tailcall]) g gas ki ks0 v stack + | R v -> (next [@ocaml.tailcall]) g gas ks' v stack + [@@inline] + + and kloop_in : type a b c r f s. (a, b, c, r, f, s) kloop_in_type = + fun g gas ks0 ki ks' accu stack -> + let accu', stack' = stack in + if accu then (step [@ocaml.tailcall]) g gas ki ks0 accu' stack' + else (next [@ocaml.tailcall]) g gas ks' accu' stack' + [@@inline] + + and kiter : type a b s r f c. (a, b, s, r, f, c) kiter_type = + fun instrument g gas body ty xs ks accu stack -> + match xs with + | [] -> (next [@ocaml.tailcall]) g gas ks accu stack + | x :: xs -> + let ks = instrument @@ KIter (body, ty, xs, ks) in + (step [@ocaml.tailcall]) g gas body ks x (accu, stack) + [@@inline] + + and next : + type a s r f. + outdated_context * step_constants -> + local_gas_counter -> + (a, s, r, f) continuation -> + a -> + s -> + (r * f * outdated_context * local_gas_counter) tzresult Lwt.t = + fun ((ctxt, _) as g) gas ks0 accu stack -> + match consume_control gas ks0 with + | None -> fail Gas.Operation_quota_exceeded + | Some gas -> ( + match ks0 with + | KLog (ks, sty, logger) -> + (logger.klog [@ocaml.tailcall]) logger g gas sty ks0 ks accu stack + | KNil -> Lwt.return (Ok (accu, stack, ctxt, gas)) + | KCons (k, ks) -> (step [@ocaml.tailcall]) g gas k ks accu stack + | KLoop_in (ki, ks') -> + (kloop_in [@ocaml.tailcall]) g gas ks0 ki ks' accu stack + | KReturn (stack', _, ks) -> + (next [@ocaml.tailcall]) g gas ks accu stack' + | KMap_head (f, ks) -> (next [@ocaml.tailcall]) g gas ks (f accu) stack + | KLoop_in_left (ki, ks') -> + (kloop_in_left [@ocaml.tailcall]) g gas ks0 ki ks' accu stack + | KUndip (x, _, ks) -> (next [@ocaml.tailcall]) g gas ks x (accu, stack) + | KIter (body, ty, xs, ks) -> + (kiter [@ocaml.tailcall]) id g gas body ty xs ks accu stack + | KList_enter_body (body, xs, ys, ty, len, ks) -> + (klist_enter [@ocaml.tailcall]) + id + g + gas + body + xs + ys + ty + len + ks + accu + stack + | KList_exit_body (body, xs, ys, ty, len, ks) -> + (klist_exit [@ocaml.tailcall]) + id + g + gas + body + xs + ys + ty + len + ks + accu + stack + | KMap_enter_body (body, xs, ys, ty, ks) -> + (kmap_enter [@ocaml.tailcall]) id g gas body xs ty ys ks accu stack + | KMap_exit_body (body, xs, ys, yk, ty, ks) -> + (kmap_exit [@ocaml.tailcall]) + id + g + gas + body + xs + ty + ys + yk + ks + accu + stack + | KView_exit (orig_step_constants, ks) -> + let g = (fst g, orig_step_constants) in + (next [@ocaml.tailcall]) g gas ks accu stack) -(* + (* Evaluation of instructions ========================== @@ -388,1531 +401,1208 @@ and next : instructions. *) -and ilist_map : - type a b c d e f g h i. (a, b, c, d, e, f, g, h, i) ilist_map_type = - fun instrument g gas body k ks ty accu stack -> - let xs = accu.elements in - let ys = Script_list.empty in - let len = accu.length in - let ks = - instrument @@ KList_enter_body (body, xs, ys, ty, len, KCons (k, ks)) - in - let accu, stack = stack in - (next [@ocaml.tailcall]) g gas ks accu stack - [@@inline] - -and ilist_iter : - type a b c d e f g cmp. (a, b, c, d, e, f, g, cmp) ilist_iter_type = - fun instrument g gas body ty k ks accu stack -> - let xs = accu.elements in - let ks = instrument @@ KIter (body, ty, xs, KCons (k, ks)) in - let accu, stack = stack in - (next [@ocaml.tailcall]) g gas ks accu stack - [@@inline] - -and iset_iter : type a b c d e f g. (a, b, c, d, e, f, g) iset_iter_type = - fun instrument g gas body ty k ks accu stack -> - let set = accu in - let l = List.rev (Script_set.fold (fun e acc -> e :: acc) set []) in - let ks = instrument @@ KIter (body, ty, l, KCons (k, ks)) in - let accu, stack = stack in - (next [@ocaml.tailcall]) g gas ks accu stack - [@@inline] - -and imap_map : - type a b c d e f g h i j. (a, b, c, d, e, f, g, h, i, j) imap_map_type = - fun instrument g gas body k ks ty accu stack -> - let map = accu in - let xs = List.rev (Script_map.fold (fun k v a -> (k, v) :: a) map []) in - let ys = Script_map.empty_from map in - let ks = instrument @@ KMap_enter_body (body, xs, ys, ty, KCons (k, ks)) in - let accu, stack = stack in - (next [@ocaml.tailcall]) g gas ks accu stack - [@@inline] - -and imap_iter : - type a b c d e f g h cmp. (a, b, c, d, e, f, g, h, cmp) imap_iter_type = - fun instrument g gas body ty k ks accu stack -> - let map = accu in - let l = List.rev (Script_map.fold (fun k v a -> (k, v) :: a) map []) in - let ks = instrument @@ KIter (body, ty, l, KCons (k, ks)) in - let accu, stack = stack in - (next [@ocaml.tailcall]) g gas ks accu stack - [@@inline] - -and imul_teznat : type a b c d e f. (a, b, c, d, e, f) imul_teznat_type = - fun logger g gas loc k ks accu stack -> - let x = accu in - let y, stack = stack in - match Script_int.to_int64 y with - | None -> get_log logger >>=? fun log -> fail (Overflow (loc, log)) - | Some y -> - Tez.(x *? y) >>?= fun res -> (step [@ocaml.tailcall]) g gas k ks res stack - -and imul_nattez : type a b c d e f. (a, b, c, d, e, f) imul_nattez_type = - fun logger g gas loc k ks accu stack -> - let y = accu in - let x, stack = stack in - match Script_int.to_int64 y with - | None -> get_log logger >>=? fun log -> fail (Overflow (loc, log)) - | Some y -> - Tez.(x *? y) >>?= fun res -> (step [@ocaml.tailcall]) g gas k ks res stack - -and ilsl_nat : type a b c d e f. (a, b, c, d, e, f) ilsl_nat_type = - fun logger g gas loc k ks accu stack -> - let x = accu and y, stack = stack in - match Script_int.shift_left_n x y with - | None -> get_log logger >>=? fun log -> fail (Overflow (loc, log)) - | Some x -> (step [@ocaml.tailcall]) g gas k ks x stack - -and ilsr_nat : type a b c d e f. (a, b, c, d, e, f) ilsr_nat_type = - fun logger g gas loc k ks accu stack -> - let x = accu and y, stack = stack in - match Script_int.shift_right_n x y with - | None -> get_log logger >>=? fun log -> fail (Overflow (loc, log)) - | Some r -> (step [@ocaml.tailcall]) g gas k ks r stack - -and ifailwith : ifailwith_type = - { - ifailwith = - (fun logger (ctxt, _) gas kloc tv accu -> - let v = accu in - let ctxt = update_context gas ctxt in - trace Cannot_serialize_failure (unparse_data ctxt Optimized tv v) - >>=? fun (v, _ctxt) -> - get_log logger >>=? fun log -> fail (Reject (kloc, v, log))); - } - -and iexec : type a b c d e f g. (a, b, c, d, e, f, g) iexec_type = - fun instrument logger g gas cont_sty k ks accu stack -> - let arg = accu and code, stack = stack in - let log_code b = - let body = - match logger with - | None -> b.kinstr - | Some logger -> - Script_interpreter_logging.log_kinstr logger b.kbef b.kinstr + and ilist_map : + type a b c d e f g h i. (a, b, c, d, e, f, g, h, i) ilist_map_type = + fun instrument g gas body k ks ty accu stack -> + let xs = accu.elements in + let ys = Script_list.empty in + let len = accu.length in + let ks = + instrument @@ KList_enter_body (body, xs, ys, ty, len, KCons (k, ks)) in - let ks = instrument @@ KReturn (stack, cont_sty, KCons (k, ks)) in - (body, ks) - in - match code with - | Lam (body, _) -> - let body, ks = log_code body in - (step [@ocaml.tailcall]) g gas body ks arg (EmptyCell, EmptyCell) - | LamRec (body, _) -> - let body, ks = log_code body in - (step [@ocaml.tailcall]) g gas body ks arg (code, (EmptyCell, EmptyCell)) - -and iview : type a b c d e f i o. (a, b, c, d, e, f, i, o) iview_type = - fun instrument - (ctxt, sc) - gas - (View_signature {name; input_ty; output_ty}) - stack_ty - k - ks - accu - stack -> - let input = accu in - let addr, stack = stack in - let ctxt = update_context gas ctxt in - let return_none ctxt = - let gas, ctxt = local_gas_counter_and_outdated_context ctxt in - (step [@ocaml.tailcall]) (ctxt, sc) gas k ks None stack - in - let legacy = Script_ir_translator_config.make ~legacy:true () in - match addr.destination with - | Contract (Implicit _) | Tx_rollup _ | Sc_rollup _ | Zk_rollup _ -> - (return_none [@ocaml.tailcall]) ctxt - | Contract (Originated contract_hash as c) -> ( - Contract.get_script ctxt contract_hash >>=? fun (ctxt, script_opt) -> - match script_opt with - | None -> (return_none [@ocaml.tailcall]) ctxt - | Some script -> ( - parse_script - ~elab_conf:legacy - ~allow_forged_in_storage:true - ctxt - script - >>=? fun (Ex_script (Script {storage; storage_type; views; _}), ctxt) - -> - Gas.consume ctxt (Interp_costs.view_get name views) >>?= fun ctxt -> - match Script_map.get name views with - | None -> (return_none [@ocaml.tailcall]) ctxt - | Some view -> ( - let view_result = - Script_ir_translator.parse_view - ctxt - ~elab_conf:legacy - storage_type - view - in - trace_eval - (fun () -> - Script_tc_errors.Ill_typed_contract - (Micheline.strip_locations view.view_code, [])) - view_result - >>=? fun ( Typed_view - { - input_ty = input_ty'; - output_ty = output_ty'; - kinstr; - original_code_expr = _; - }, - ctxt ) -> - let io_ty = - let open Gas_monad.Syntax in - let* out_eq = ty_eq ~error_details:Fast output_ty' output_ty in - let+ in_eq = ty_eq ~error_details:Fast input_ty input_ty' in - (out_eq, in_eq) - in - Gas_monad.run ctxt io_ty >>?= fun (eq, ctxt) -> - match eq with - | Error Inconsistent_types_fast -> - (return_none [@ocaml.tailcall]) ctxt - | Ok (Eq, Eq) -> - let kcons = KCons (ICons_some (kinstr_location k, k), ks) in - Contract.get_balance_carbonated ctxt c - >>=? fun (ctxt, balance) -> - let gas, ctxt = local_gas_counter_and_outdated_context ctxt in - let sty = - Option.map (fun t -> Item_t (output_ty, t)) stack_ty + let accu, stack = stack in + (next [@ocaml.tailcall]) g gas ks accu stack + [@@inline] + + and ilist_iter : + type a b c d e f g cmp. (a, b, c, d, e, f, g, cmp) ilist_iter_type = + fun instrument g gas body ty k ks accu stack -> + let xs = accu.elements in + let ks = instrument @@ KIter (body, ty, xs, KCons (k, ks)) in + let accu, stack = stack in + (next [@ocaml.tailcall]) g gas ks accu stack + [@@inline] + + and iset_iter : type a b c d e f g. (a, b, c, d, e, f, g) iset_iter_type = + fun instrument g gas body ty k ks accu stack -> + let set = accu in + let l = List.rev (Script_set.fold (fun e acc -> e :: acc) set []) in + let ks = instrument @@ KIter (body, ty, l, KCons (k, ks)) in + let accu, stack = stack in + (next [@ocaml.tailcall]) g gas ks accu stack + [@@inline] + + and imap_map : + type a b c d e f g h i j. (a, b, c, d, e, f, g, h, i, j) imap_map_type = + fun instrument g gas body k ks ty accu stack -> + let map = accu in + let xs = List.rev (Script_map.fold (fun k v a -> (k, v) :: a) map []) in + let ys = Script_map.empty_from map in + let ks = instrument @@ KMap_enter_body (body, xs, ys, ty, KCons (k, ks)) in + let accu, stack = stack in + (next [@ocaml.tailcall]) g gas ks accu stack + [@@inline] + + and imap_iter : + type a b c d e f g h cmp. (a, b, c, d, e, f, g, h, cmp) imap_iter_type = + fun instrument g gas body ty k ks accu stack -> + let map = accu in + let l = List.rev (Script_map.fold (fun k v a -> (k, v) :: a) map []) in + let ks = instrument @@ KIter (body, ty, l, KCons (k, ks)) in + let accu, stack = stack in + (next [@ocaml.tailcall]) g gas ks accu stack + [@@inline] + + and imul_teznat : type a b c d e f. (a, b, c, d, e, f) imul_teznat_type = + fun logger g gas loc k ks accu stack -> + let x = accu in + let y, stack = stack in + match Script_int.to_int64 y with + | None -> get_log logger >>=? fun log -> fail (Overflow (loc, log)) + | Some y -> + Tez.(x *? y) >>?= fun res -> + (step [@ocaml.tailcall]) g gas k ks res stack + + and imul_nattez : type a b c d e f. (a, b, c, d, e, f) imul_nattez_type = + fun logger g gas loc k ks accu stack -> + let y = accu in + let x, stack = stack in + match Script_int.to_int64 y with + | None -> get_log logger >>=? fun log -> fail (Overflow (loc, log)) + | Some y -> + Tez.(x *? y) >>?= fun res -> + (step [@ocaml.tailcall]) g gas k ks res stack + + and ilsl_nat : type a b c d e f. (a, b, c, d, e, f) ilsl_nat_type = + fun logger g gas loc k ks accu stack -> + let x = accu and y, stack = stack in + match Script_int.shift_left_n x y with + | None -> get_log logger >>=? fun log -> fail (Overflow (loc, log)) + | Some x -> (step [@ocaml.tailcall]) g gas k ks x stack + + and ilsr_nat : type a b c d e f. (a, b, c, d, e, f) ilsr_nat_type = + fun logger g gas loc k ks accu stack -> + let x = accu and y, stack = stack in + match Script_int.shift_right_n x y with + | None -> get_log logger >>=? fun log -> fail (Overflow (loc, log)) + | Some r -> (step [@ocaml.tailcall]) g gas k ks r stack + + and ifailwith : ifailwith_type = + { + ifailwith = + (fun logger (ctxt, _) gas kloc tv accu -> + let v = accu in + let ctxt = update_context gas ctxt in + trace Cannot_serialize_failure (unparse_data ctxt Optimized tv v) + >>=? fun (v, _ctxt) -> + get_log logger >>=? fun log -> fail (Reject (kloc, v, log))); + } + + and iexec : type a b c d e f g. (a, b, c, d, e, f, g) iexec_type = + fun instrument logger g gas cont_sty k ks accu stack -> + let arg = accu and code, stack = stack in + let log_code b = + let body = + match logger with + | None -> b.kinstr + | Some logger -> logger.log_kinstr logger b.kbef b.kinstr + in + let ks = instrument @@ KReturn (stack, cont_sty, KCons (k, ks)) in + (body, ks) + in + match code with + | Lam (body, _) -> + let body, ks = log_code body in + (step [@ocaml.tailcall]) g gas body ks arg (EmptyCell, EmptyCell) + | LamRec (body, _) -> + let body, ks = log_code body in + (step [@ocaml.tailcall]) g gas body ks arg (code, (EmptyCell, EmptyCell)) + + and iview : type a b c d e f i o. (a, b, c, d, e, f, i, o) iview_type = + fun instrument + (ctxt, sc) + gas + (View_signature {name; input_ty; output_ty}) + stack_ty + k + ks + accu + stack -> + let input = accu in + let addr, stack = stack in + let ctxt = update_context gas ctxt in + let return_none ctxt = + let gas, ctxt = local_gas_counter_and_outdated_context ctxt in + (step [@ocaml.tailcall]) (ctxt, sc) gas k ks None stack + in + let legacy = Script_ir_translator_config.make ~legacy:true () in + match addr.destination with + | Contract (Implicit _) | Tx_rollup _ | Sc_rollup _ | Zk_rollup _ -> + (return_none [@ocaml.tailcall]) ctxt + | Contract (Originated contract_hash as c) -> ( + Contract.get_script ctxt contract_hash >>=? fun (ctxt, script_opt) -> + match script_opt with + | None -> (return_none [@ocaml.tailcall]) ctxt + | Some script -> ( + parse_script + ~elab_conf:legacy + ~allow_forged_in_storage:true + ctxt + script + >>=? fun (Ex_script (Script {storage; storage_type; views; _}), ctxt) + -> + Gas.consume ctxt (Interp_costs.view_get name views) >>?= fun ctxt -> + match Script_map.get name views with + | None -> (return_none [@ocaml.tailcall]) ctxt + | Some view -> ( + let view_result = + Script_ir_translator.parse_view + ctxt + ~elab_conf:legacy + storage_type + view + in + trace_eval + (fun () -> + Script_tc_errors.Ill_typed_contract + (Micheline.strip_locations view.view_code, [])) + view_result + >>=? fun ( Typed_view + { + input_ty = input_ty'; + output_ty = output_ty'; + kinstr; + original_code_expr = _; + }, + ctxt ) -> + let io_ty = + let open Gas_monad.Syntax in + let* out_eq = + ty_eq ~error_details:Fast output_ty' output_ty in - (step [@ocaml.tailcall]) - ( ctxt, - { - source = Contract.Originated sc.self; - self = contract_hash; - amount = Tez.zero; - balance; - (* The following remain unchanged, but let's - list them anyway, so that we don't forget - to update something added later. *) - payer = sc.payer; - chain_id = sc.chain_id; - now = sc.now; - level = sc.level; - } ) - gas - kinstr - (instrument @@ KView_exit (sc, KReturn (stack, sty, kcons))) - (input, storage) - (EmptyCell, EmptyCell)))) - -and step : type a s b t r f. (a, s, b, t, r, f) step_type = - fun ((ctxt, sc) as g) gas i ks accu stack -> - match consume_instr gas i accu stack with - | None -> fail Gas.Operation_quota_exceeded - | Some gas -> ( - match i with - | ILog (_, sty, event, logger, k) -> - (log [@ocaml.tailcall]) (logger, event) sty g gas k ks accu stack - | IHalt _ -> (next [@ocaml.tailcall]) g gas ks accu stack - (* stack ops *) - | IDrop (_, k) -> - let accu, stack = stack in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IDup (_, k) -> (step [@ocaml.tailcall]) g gas k ks accu (accu, stack) - | ISwap (_, k) -> - let top, stack = stack in - (step [@ocaml.tailcall]) g gas k ks top (accu, stack) - | IConst (_, _ty, v, k) -> - (step [@ocaml.tailcall]) g gas k ks v (accu, stack) - (* options *) - | ICons_some (_, k) -> - (step [@ocaml.tailcall]) g gas k ks (Some accu) stack - | ICons_none (_, _ty, k) -> - (step [@ocaml.tailcall]) g gas k ks None (accu, stack) - | IIf_none {branch_if_none; branch_if_some; k; _} -> ( - match accu with - | None -> - let accu, stack = stack in - (step [@ocaml.tailcall]) - g - gas - branch_if_none - (KCons (k, ks)) - accu - stack - | Some v -> - (step [@ocaml.tailcall]) - g - gas - branch_if_some - (KCons (k, ks)) - v - stack) - | IOpt_map {body; k; loc = _} -> ( - match accu with - | None -> (step [@ocaml.tailcall]) g gas k ks None stack - | Some v -> - let ks' = KMap_head (Option.some, KCons (k, ks)) in - (step [@ocaml.tailcall]) g gas body ks' v stack) - (* pairs *) - | ICons_pair (_, k) -> - let b, stack = stack in - (step [@ocaml.tailcall]) g gas k ks (accu, b) stack - | IUnpair (_, k) -> - let a, b = accu in - (step [@ocaml.tailcall]) g gas k ks a (b, stack) - | ICar (_, k) -> - let a, _ = accu in - (step [@ocaml.tailcall]) g gas k ks a stack - | ICdr (_, k) -> - let _, b = accu in - (step [@ocaml.tailcall]) g gas k ks b stack - (* unions *) - | ICons_left (_, _tyb, k) -> - (step [@ocaml.tailcall]) g gas k ks (L accu) stack - | ICons_right (_, _tya, k) -> - (step [@ocaml.tailcall]) g gas k ks (R accu) stack - | IIf_left {branch_if_left; branch_if_right; k; _} -> ( - match accu with - | L v -> + let+ in_eq = ty_eq ~error_details:Fast input_ty input_ty' in + (out_eq, in_eq) + in + Gas_monad.run ctxt io_ty >>?= fun (eq, ctxt) -> + match eq with + | Error Inconsistent_types_fast -> + (return_none [@ocaml.tailcall]) ctxt + | Ok (Eq, Eq) -> + let kcons = KCons (ICons_some (kinstr_location k, k), ks) in + Contract.get_balance_carbonated ctxt c + >>=? fun (ctxt, balance) -> + let gas, ctxt = + local_gas_counter_and_outdated_context ctxt + in + let sty = + Option.map (fun t -> Item_t (output_ty, t)) stack_ty + in + (step [@ocaml.tailcall]) + ( ctxt, + { + source = Contract.Originated sc.self; + self = contract_hash; + amount = Tez.zero; + balance; + (* The following remain unchanged, but let's + list them anyway, so that we don't forget + to update something added later. *) + payer = sc.payer; + chain_id = sc.chain_id; + now = sc.now; + level = sc.level; + } ) + gas + kinstr + (instrument + @@ KView_exit (sc, KReturn (stack, sty, kcons))) + (input, storage) + (EmptyCell, EmptyCell)))) + + and step : type a s b t r f. (a, s, b, t, r, f) step_type = + fun ((ctxt, sc) as g) gas i ks accu stack -> + match consume_instr gas i accu stack with + | None -> fail Gas.Operation_quota_exceeded + | Some gas -> ( + match i with + | ILog (_, sty, event, logger, k) -> + (logger.ilog [@ocaml.tailcall]) + logger + event + sty + g + gas + k + ks + accu + stack + | IHalt _ -> (next [@ocaml.tailcall]) g gas ks accu stack + (* stack ops *) + | IDrop (_, k) -> + let accu, stack = stack in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IDup (_, k) -> (step [@ocaml.tailcall]) g gas k ks accu (accu, stack) + | ISwap (_, k) -> + let top, stack = stack in + (step [@ocaml.tailcall]) g gas k ks top (accu, stack) + | IConst (_, _ty, v, k) -> + (step [@ocaml.tailcall]) g gas k ks v (accu, stack) + (* options *) + | ICons_some (_, k) -> + (step [@ocaml.tailcall]) g gas k ks (Some accu) stack + | ICons_none (_, _ty, k) -> + (step [@ocaml.tailcall]) g gas k ks None (accu, stack) + | IIf_none {branch_if_none; branch_if_some; k; _} -> ( + match accu with + | None -> + let accu, stack = stack in + (step [@ocaml.tailcall]) + g + gas + branch_if_none + (KCons (k, ks)) + accu + stack + | Some v -> + (step [@ocaml.tailcall]) + g + gas + branch_if_some + (KCons (k, ks)) + v + stack) + | IOpt_map {body; k; loc = _} -> ( + match accu with + | None -> (step [@ocaml.tailcall]) g gas k ks None stack + | Some v -> + let ks' = KMap_head (Option.some, KCons (k, ks)) in + (step [@ocaml.tailcall]) g gas body ks' v stack) + (* pairs *) + | ICons_pair (_, k) -> + let b, stack = stack in + (step [@ocaml.tailcall]) g gas k ks (accu, b) stack + | IUnpair (_, k) -> + let a, b = accu in + (step [@ocaml.tailcall]) g gas k ks a (b, stack) + | ICar (_, k) -> + let a, _ = accu in + (step [@ocaml.tailcall]) g gas k ks a stack + | ICdr (_, k) -> + let _, b = accu in + (step [@ocaml.tailcall]) g gas k ks b stack + (* unions *) + | ICons_left (_, _tyb, k) -> + (step [@ocaml.tailcall]) g gas k ks (L accu) stack + | ICons_right (_, _tya, k) -> + (step [@ocaml.tailcall]) g gas k ks (R accu) stack + | IIf_left {branch_if_left; branch_if_right; k; _} -> ( + match accu with + | L v -> + (step [@ocaml.tailcall]) + g + gas + branch_if_left + (KCons (k, ks)) + v + stack + | R v -> + (step [@ocaml.tailcall]) + g + gas + branch_if_right + (KCons (k, ks)) + v + stack) + (* lists *) + | ICons_list (_, k) -> + let tl, stack = stack in + let accu = Script_list.cons accu tl in + (step [@ocaml.tailcall]) g gas k ks accu stack + | INil (_, _ty, k) -> + let stack = (accu, stack) in + let accu = Script_list.empty in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IIf_cons {branch_if_cons; branch_if_nil; k; _} -> ( + match Script_list.uncons accu with + | None -> + let accu, stack = stack in + (step [@ocaml.tailcall]) + g + gas + branch_if_nil + (KCons (k, ks)) + accu + stack + | Some (hd, tl) -> + (step [@ocaml.tailcall]) + g + gas + branch_if_cons + (KCons (k, ks)) + hd + (tl, stack)) + | IList_map (_, body, ty, k) -> + (ilist_map [@ocaml.tailcall]) id g gas body k ks ty accu stack + | IList_size (_, k) -> + let list = accu in + let len = Script_int.(abs (of_int list.length)) in + (step [@ocaml.tailcall]) g gas k ks len stack + | IList_iter (_, ty, body, k) -> + (ilist_iter [@ocaml.tailcall]) id g gas body ty k ks accu stack + (* sets *) + | IEmpty_set (_, ty, k) -> + let res = Script_set.empty ty in + let stack = (accu, stack) in + (step [@ocaml.tailcall]) g gas k ks res stack + | ISet_iter (_, ty, body, k) -> + (iset_iter [@ocaml.tailcall]) id g gas body ty k ks accu stack + | ISet_mem (_, k) -> + let set, stack = stack in + let res = Script_set.mem accu set in + (step [@ocaml.tailcall]) g gas k ks res stack + | ISet_update (_, k) -> + let presence, (set, stack) = stack in + let res = Script_set.update accu presence set in + (step [@ocaml.tailcall]) g gas k ks res stack + | ISet_size (_, k) -> + let res = Script_set.size accu in + (step [@ocaml.tailcall]) g gas k ks res stack + (* maps *) + | IEmpty_map (_, kty, _vty, k) -> + let res = Script_map.empty kty and stack = (accu, stack) in + (step [@ocaml.tailcall]) g gas k ks res stack + | IMap_map (_, ty, body, k) -> + (imap_map [@ocaml.tailcall]) id g gas body k ks ty accu stack + | IMap_iter (_, kvty, body, k) -> + (imap_iter [@ocaml.tailcall]) id g gas body kvty k ks accu stack + | IMap_mem (_, k) -> + let map, stack = stack in + let res = Script_map.mem accu map in + (step [@ocaml.tailcall]) g gas k ks res stack + | IMap_get (_, k) -> + let map, stack = stack in + let res = Script_map.get accu map in + (step [@ocaml.tailcall]) g gas k ks res stack + | IMap_update (_, k) -> + let v, (map, stack) = stack in + let key = accu in + let res = Script_map.update key v map in + (step [@ocaml.tailcall]) g gas k ks res stack + | IMap_get_and_update (_, k) -> + let key = accu in + let v, (map, rest) = stack in + let map' = Script_map.update key v map in + let v' = Script_map.get key map in + (step [@ocaml.tailcall]) g gas k ks v' (map', rest) + | IMap_size (_, k) -> + let res = Script_map.size accu in + (step [@ocaml.tailcall]) g gas k ks res stack + (* Big map operations *) + | IEmpty_big_map (_, tk, tv, k) -> + let ebm = Script_big_map.empty tk tv in + (step [@ocaml.tailcall]) g gas k ks ebm (accu, stack) + | IBig_map_mem (_, k) -> + let map, stack = stack in + let key = accu in + ( use_gas_counter_in_context ctxt gas @@ fun ctxt -> + Script_big_map.mem ctxt key map ) + >>=? fun (res, ctxt, gas) -> + (step [@ocaml.tailcall]) (ctxt, sc) gas k ks res stack + | IBig_map_get (_, k) -> + let map, stack = stack in + let key = accu in + ( use_gas_counter_in_context ctxt gas @@ fun ctxt -> + Script_big_map.get ctxt key map ) + >>=? fun (res, ctxt, gas) -> + (step [@ocaml.tailcall]) (ctxt, sc) gas k ks res stack + | IBig_map_update (_, k) -> + let key = accu in + let maybe_value, (map, stack) = stack in + ( use_gas_counter_in_context ctxt gas @@ fun ctxt -> + Script_big_map.update ctxt key maybe_value map ) + >>=? fun (big_map, ctxt, gas) -> + (step [@ocaml.tailcall]) (ctxt, sc) gas k ks big_map stack + | IBig_map_get_and_update (_, k) -> + let key = accu in + let v, (map, stack) = stack in + ( use_gas_counter_in_context ctxt gas @@ fun ctxt -> + Script_big_map.get_and_update ctxt key v map ) + >>=? fun ((v', map'), ctxt, gas) -> + (step [@ocaml.tailcall]) (ctxt, sc) gas k ks v' (map', stack) + (* timestamp operations *) + | IAdd_seconds_to_timestamp (_, k) -> + let n = accu in + let t, stack = stack in + let result = Script_timestamp.add_delta t n in + (step [@ocaml.tailcall]) g gas k ks result stack + | IAdd_timestamp_to_seconds (_, k) -> + let t = accu in + let n, stack = stack in + let result = Script_timestamp.add_delta t n in + (step [@ocaml.tailcall]) g gas k ks result stack + | ISub_timestamp_seconds (_, k) -> + let t = accu in + let s, stack = stack in + let result = Script_timestamp.sub_delta t s in + (step [@ocaml.tailcall]) g gas k ks result stack + | IDiff_timestamps (_, k) -> + let t1 = accu in + let t2, stack = stack in + let result = Script_timestamp.diff t1 t2 in + (step [@ocaml.tailcall]) g gas k ks result stack + (* string operations *) + | IConcat_string_pair (_, k) -> + let x = accu in + let y, stack = stack in + let s = Script_string.concat_pair x y in + (step [@ocaml.tailcall]) g gas k ks s stack + | IConcat_string (_, k) -> + let ss = accu in + (* The cost for this fold_left has been paid upfront *) + let total_length = + List.fold_left + (fun acc s -> S.add acc (S.safe_int (Script_string.length s))) + S.zero + ss.elements + in + consume gas (Interp_costs.concat_string total_length) + >>?= fun gas -> + let s = Script_string.concat ss.elements in + (step [@ocaml.tailcall]) g gas k ks s stack + | ISlice_string (_, k) -> + let offset = accu and length, (s, stack) = stack in + let s_length = Z.of_int (Script_string.length s) in + let offset = Script_int.to_zint offset in + let length = Script_int.to_zint length in + if Compare.Z.(offset < s_length && Z.add offset length <= s_length) + then + let s = Script_string.sub s (Z.to_int offset) (Z.to_int length) in + (step [@ocaml.tailcall]) g gas k ks (Some s) stack + else (step [@ocaml.tailcall]) g gas k ks None stack + | IString_size (_, k) -> + let s = accu in + let result = Script_int.(abs (of_int (Script_string.length s))) in + (step [@ocaml.tailcall]) g gas k ks result stack + (* bytes operations *) + | IConcat_bytes_pair (_, k) -> + let x = accu in + let y, stack = stack in + let s = Bytes.cat x y in + (step [@ocaml.tailcall]) g gas k ks s stack + | IConcat_bytes (_, k) -> + let ss = accu in + (* The cost for this fold_left has been paid upfront *) + let total_length = + List.fold_left + (fun acc s -> S.add acc (S.safe_int (Bytes.length s))) + S.zero + ss.elements + in + consume gas (Interp_costs.concat_string total_length) + >>?= fun gas -> + let s = Bytes.concat Bytes.empty ss.elements in + (step [@ocaml.tailcall]) g gas k ks s stack + | ISlice_bytes (_, k) -> + let offset = accu and length, (s, stack) = stack in + let s_length = Z.of_int (Bytes.length s) in + let offset = Script_int.to_zint offset in + let length = Script_int.to_zint length in + if Compare.Z.(offset < s_length && Z.add offset length <= s_length) + then + let s = Bytes.sub s (Z.to_int offset) (Z.to_int length) in + (step [@ocaml.tailcall]) g gas k ks (Some s) stack + else (step [@ocaml.tailcall]) g gas k ks None stack + | IBytes_size (_, k) -> + let s = accu in + let result = Script_int.(abs (of_int (Bytes.length s))) in + (step [@ocaml.tailcall]) g gas k ks result stack + (* currency operations *) + | IAdd_tez (_, k) -> + let x = accu in + let y, stack = stack in + Tez.(x +? y) >>?= fun res -> + (step [@ocaml.tailcall]) g gas k ks res stack + | ISub_tez (_, k) -> + let x = accu in + let y, stack = stack in + let res = Tez.sub_opt x y in + (step [@ocaml.tailcall]) g gas k ks res stack + | ISub_tez_legacy (_, k) -> + let x = accu in + let y, stack = stack in + Tez.(x -? y) >>?= fun res -> + (step [@ocaml.tailcall]) g gas k ks res stack + | IMul_teznat (loc, k) -> imul_teznat None g gas loc k ks accu stack + | IMul_nattez (loc, k) -> imul_nattez None g gas loc k ks accu stack + (* boolean operations *) + | IOr (_, k) -> + let x = accu in + let y, stack = stack in + (step [@ocaml.tailcall]) g gas k ks (x || y) stack + | IAnd (_, k) -> + let x = accu in + let y, stack = stack in + (step [@ocaml.tailcall]) g gas k ks (x && y) stack + | IXor (_, k) -> + let x = accu in + let y, stack = stack in + let res = Compare.Bool.(x <> y) in + (step [@ocaml.tailcall]) g gas k ks res stack + | INot (_, k) -> + let x = accu in + (step [@ocaml.tailcall]) g gas k ks (not x) stack + (* integer operations *) + | IIs_nat (_, k) -> + let x = accu in + let res = Script_int.is_nat x in + (step [@ocaml.tailcall]) g gas k ks res stack + | IAbs_int (_, k) -> + let x = accu in + let res = Script_int.abs x in + (step [@ocaml.tailcall]) g gas k ks res stack + | IInt_nat (_, k) -> + let x = accu in + let res = Script_int.int x in + (step [@ocaml.tailcall]) g gas k ks res stack + | INeg (_, k) -> + let x = accu in + let res = Script_int.neg x in + (step [@ocaml.tailcall]) g gas k ks res stack + | IAdd_int (_, k) -> + let x = accu and y, stack = stack in + let res = Script_int.add x y in + (step [@ocaml.tailcall]) g gas k ks res stack + | IAdd_nat (_, k) -> + let x = accu and y, stack = stack in + let res = Script_int.add_n x y in + (step [@ocaml.tailcall]) g gas k ks res stack + | ISub_int (_, k) -> + let x = accu and y, stack = stack in + let res = Script_int.sub x y in + (step [@ocaml.tailcall]) g gas k ks res stack + | IMul_int (_, k) -> + let x = accu and y, stack = stack in + let res = Script_int.mul x y in + (step [@ocaml.tailcall]) g gas k ks res stack + | IMul_nat (_, k) -> + let x = accu and y, stack = stack in + let res = Script_int.mul_n x y in + (step [@ocaml.tailcall]) g gas k ks res stack + | IEdiv_teznat (_, k) -> + let x = accu and y, stack = stack in + let x = Script_int.of_int64 (Tez.to_mutez x) in + let result = + match Script_int.ediv x y with + | None -> None + | Some (q, r) -> ( + match (Script_int.to_int64 q, Script_int.to_int64 r) with + | Some q, Some r -> ( + match (Tez.of_mutez q, Tez.of_mutez r) with + | Some q, Some r -> Some (q, r) + (* Cannot overflow *) + | _ -> assert false) + (* Cannot overflow *) + | _ -> assert false) + in + (step [@ocaml.tailcall]) g gas k ks result stack + | IEdiv_tez (_, k) -> + let x = accu and y, stack = stack in + let x = Script_int.abs (Script_int.of_int64 (Tez.to_mutez x)) in + let y = Script_int.abs (Script_int.of_int64 (Tez.to_mutez y)) in + let result = + match Script_int.ediv_n x y with + | None -> None + | Some (q, r) -> ( + match Script_int.to_int64 r with + | None -> assert false (* Cannot overflow *) + | Some r -> ( + match Tez.of_mutez r with + | None -> assert false (* Cannot overflow *) + | Some r -> Some (q, r))) + in + (step [@ocaml.tailcall]) g gas k ks result stack + | IEdiv_int (_, k) -> + let x = accu and y, stack = stack in + let res = Script_int.ediv x y in + (step [@ocaml.tailcall]) g gas k ks res stack + | IEdiv_nat (_, k) -> + let x = accu and y, stack = stack in + let res = Script_int.ediv_n x y in + (step [@ocaml.tailcall]) g gas k ks res stack + | ILsl_nat (loc, k) -> ilsl_nat None g gas loc k ks accu stack + | ILsr_nat (loc, k) -> ilsr_nat None g gas loc k ks accu stack + | IOr_nat (_, k) -> + let x = accu and y, stack = stack in + let res = Script_int.logor x y in + (step [@ocaml.tailcall]) g gas k ks res stack + | IAnd_nat (_, k) -> + let x = accu and y, stack = stack in + let res = Script_int.logand x y in + (step [@ocaml.tailcall]) g gas k ks res stack + | IAnd_int_nat (_, k) -> + let x = accu and y, stack = stack in + let res = Script_int.logand x y in + (step [@ocaml.tailcall]) g gas k ks res stack + | IXor_nat (_, k) -> + let x = accu and y, stack = stack in + let res = Script_int.logxor x y in + (step [@ocaml.tailcall]) g gas k ks res stack + | INot_int (_, k) -> + let x = accu in + let res = Script_int.lognot x in + (step [@ocaml.tailcall]) g gas k ks res stack + (* control *) + | IIf {branch_if_true; branch_if_false; k; _} -> + let res, stack = stack in + if accu then (step [@ocaml.tailcall]) g gas - branch_if_left + branch_if_true (KCons (k, ks)) - v + res stack - | R v -> + else (step [@ocaml.tailcall]) g gas - branch_if_right + branch_if_false (KCons (k, ks)) - v - stack) - (* lists *) - | ICons_list (_, k) -> - let tl, stack = stack in - let accu = Script_list.cons accu tl in - (step [@ocaml.tailcall]) g gas k ks accu stack - | INil (_, _ty, k) -> - let stack = (accu, stack) in - let accu = Script_list.empty in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IIf_cons {branch_if_cons; branch_if_nil; k; _} -> ( - match Script_list.uncons accu with - | None -> - let accu, stack = stack in - (step [@ocaml.tailcall]) - g - gas - branch_if_nil - (KCons (k, ks)) - accu + res stack - | Some (hd, tl) -> - (step [@ocaml.tailcall]) - g - gas - branch_if_cons - (KCons (k, ks)) - hd - (tl, stack)) - | IList_map (_, body, ty, k) -> - (ilist_map [@ocaml.tailcall]) id g gas body k ks ty accu stack - | IList_size (_, k) -> - let list = accu in - let len = Script_int.(abs (of_int list.length)) in - (step [@ocaml.tailcall]) g gas k ks len stack - | IList_iter (_, ty, body, k) -> - (ilist_iter [@ocaml.tailcall]) id g gas body ty k ks accu stack - (* sets *) - | IEmpty_set (_, ty, k) -> - let res = Script_set.empty ty in - let stack = (accu, stack) in - (step [@ocaml.tailcall]) g gas k ks res stack - | ISet_iter (_, ty, body, k) -> - (iset_iter [@ocaml.tailcall]) id g gas body ty k ks accu stack - | ISet_mem (_, k) -> - let set, stack = stack in - let res = Script_set.mem accu set in - (step [@ocaml.tailcall]) g gas k ks res stack - | ISet_update (_, k) -> - let presence, (set, stack) = stack in - let res = Script_set.update accu presence set in - (step [@ocaml.tailcall]) g gas k ks res stack - | ISet_size (_, k) -> - let res = Script_set.size accu in - (step [@ocaml.tailcall]) g gas k ks res stack - (* maps *) - | IEmpty_map (_, kty, _vty, k) -> - let res = Script_map.empty kty and stack = (accu, stack) in - (step [@ocaml.tailcall]) g gas k ks res stack - | IMap_map (_, ty, body, k) -> - (imap_map [@ocaml.tailcall]) id g gas body k ks ty accu stack - | IMap_iter (_, kvty, body, k) -> - (imap_iter [@ocaml.tailcall]) id g gas body kvty k ks accu stack - | IMap_mem (_, k) -> - let map, stack = stack in - let res = Script_map.mem accu map in - (step [@ocaml.tailcall]) g gas k ks res stack - | IMap_get (_, k) -> - let map, stack = stack in - let res = Script_map.get accu map in - (step [@ocaml.tailcall]) g gas k ks res stack - | IMap_update (_, k) -> - let v, (map, stack) = stack in - let key = accu in - let res = Script_map.update key v map in - (step [@ocaml.tailcall]) g gas k ks res stack - | IMap_get_and_update (_, k) -> - let key = accu in - let v, (map, rest) = stack in - let map' = Script_map.update key v map in - let v' = Script_map.get key map in - (step [@ocaml.tailcall]) g gas k ks v' (map', rest) - | IMap_size (_, k) -> - let res = Script_map.size accu in - (step [@ocaml.tailcall]) g gas k ks res stack - (* Big map operations *) - | IEmpty_big_map (_, tk, tv, k) -> - let ebm = Script_big_map.empty tk tv in - (step [@ocaml.tailcall]) g gas k ks ebm (accu, stack) - | IBig_map_mem (_, k) -> - let map, stack = stack in - let key = accu in - ( use_gas_counter_in_context ctxt gas @@ fun ctxt -> - Script_big_map.mem ctxt key map ) - >>=? fun (res, ctxt, gas) -> - (step [@ocaml.tailcall]) (ctxt, sc) gas k ks res stack - | IBig_map_get (_, k) -> - let map, stack = stack in - let key = accu in - ( use_gas_counter_in_context ctxt gas @@ fun ctxt -> - Script_big_map.get ctxt key map ) - >>=? fun (res, ctxt, gas) -> - (step [@ocaml.tailcall]) (ctxt, sc) gas k ks res stack - | IBig_map_update (_, k) -> - let key = accu in - let maybe_value, (map, stack) = stack in - ( use_gas_counter_in_context ctxt gas @@ fun ctxt -> - Script_big_map.update ctxt key maybe_value map ) - >>=? fun (big_map, ctxt, gas) -> - (step [@ocaml.tailcall]) (ctxt, sc) gas k ks big_map stack - | IBig_map_get_and_update (_, k) -> - let key = accu in - let v, (map, stack) = stack in - ( use_gas_counter_in_context ctxt gas @@ fun ctxt -> - Script_big_map.get_and_update ctxt key v map ) - >>=? fun ((v', map'), ctxt, gas) -> - (step [@ocaml.tailcall]) (ctxt, sc) gas k ks v' (map', stack) - (* timestamp operations *) - | IAdd_seconds_to_timestamp (_, k) -> - let n = accu in - let t, stack = stack in - let result = Script_timestamp.add_delta t n in - (step [@ocaml.tailcall]) g gas k ks result stack - | IAdd_timestamp_to_seconds (_, k) -> - let t = accu in - let n, stack = stack in - let result = Script_timestamp.add_delta t n in - (step [@ocaml.tailcall]) g gas k ks result stack - | ISub_timestamp_seconds (_, k) -> - let t = accu in - let s, stack = stack in - let result = Script_timestamp.sub_delta t s in - (step [@ocaml.tailcall]) g gas k ks result stack - | IDiff_timestamps (_, k) -> - let t1 = accu in - let t2, stack = stack in - let result = Script_timestamp.diff t1 t2 in - (step [@ocaml.tailcall]) g gas k ks result stack - (* string operations *) - | IConcat_string_pair (_, k) -> - let x = accu in - let y, stack = stack in - let s = Script_string.concat_pair x y in - (step [@ocaml.tailcall]) g gas k ks s stack - | IConcat_string (_, k) -> - let ss = accu in - (* The cost for this fold_left has been paid upfront *) - let total_length = - List.fold_left - (fun acc s -> S.add acc (S.safe_int (Script_string.length s))) - S.zero - ss.elements - in - consume gas (Interp_costs.concat_string total_length) >>?= fun gas -> - let s = Script_string.concat ss.elements in - (step [@ocaml.tailcall]) g gas k ks s stack - | ISlice_string (_, k) -> - let offset = accu and length, (s, stack) = stack in - let s_length = Z.of_int (Script_string.length s) in - let offset = Script_int.to_zint offset in - let length = Script_int.to_zint length in - if Compare.Z.(offset < s_length && Z.add offset length <= s_length) - then - let s = Script_string.sub s (Z.to_int offset) (Z.to_int length) in - (step [@ocaml.tailcall]) g gas k ks (Some s) stack - else (step [@ocaml.tailcall]) g gas k ks None stack - | IString_size (_, k) -> - let s = accu in - let result = Script_int.(abs (of_int (Script_string.length s))) in - (step [@ocaml.tailcall]) g gas k ks result stack - (* bytes operations *) - | IConcat_bytes_pair (_, k) -> - let x = accu in - let y, stack = stack in - let s = Bytes.cat x y in - (step [@ocaml.tailcall]) g gas k ks s stack - | IConcat_bytes (_, k) -> - let ss = accu in - (* The cost for this fold_left has been paid upfront *) - let total_length = - List.fold_left - (fun acc s -> S.add acc (S.safe_int (Bytes.length s))) - S.zero - ss.elements - in - consume gas (Interp_costs.concat_string total_length) >>?= fun gas -> - let s = Bytes.concat Bytes.empty ss.elements in - (step [@ocaml.tailcall]) g gas k ks s stack - | ISlice_bytes (_, k) -> - let offset = accu and length, (s, stack) = stack in - let s_length = Z.of_int (Bytes.length s) in - let offset = Script_int.to_zint offset in - let length = Script_int.to_zint length in - if Compare.Z.(offset < s_length && Z.add offset length <= s_length) - then - let s = Bytes.sub s (Z.to_int offset) (Z.to_int length) in - (step [@ocaml.tailcall]) g gas k ks (Some s) stack - else (step [@ocaml.tailcall]) g gas k ks None stack - | IBytes_size (_, k) -> - let s = accu in - let result = Script_int.(abs (of_int (Bytes.length s))) in - (step [@ocaml.tailcall]) g gas k ks result stack - (* currency operations *) - | IAdd_tez (_, k) -> - let x = accu in - let y, stack = stack in - Tez.(x +? y) >>?= fun res -> - (step [@ocaml.tailcall]) g gas k ks res stack - | ISub_tez (_, k) -> - let x = accu in - let y, stack = stack in - let res = Tez.sub_opt x y in - (step [@ocaml.tailcall]) g gas k ks res stack - | ISub_tez_legacy (_, k) -> - let x = accu in - let y, stack = stack in - Tez.(x -? y) >>?= fun res -> - (step [@ocaml.tailcall]) g gas k ks res stack - | IMul_teznat (loc, k) -> imul_teznat None g gas loc k ks accu stack - | IMul_nattez (loc, k) -> imul_nattez None g gas loc k ks accu stack - (* boolean operations *) - | IOr (_, k) -> - let x = accu in - let y, stack = stack in - (step [@ocaml.tailcall]) g gas k ks (x || y) stack - | IAnd (_, k) -> - let x = accu in - let y, stack = stack in - (step [@ocaml.tailcall]) g gas k ks (x && y) stack - | IXor (_, k) -> - let x = accu in - let y, stack = stack in - let res = Compare.Bool.(x <> y) in - (step [@ocaml.tailcall]) g gas k ks res stack - | INot (_, k) -> - let x = accu in - (step [@ocaml.tailcall]) g gas k ks (not x) stack - (* integer operations *) - | IIs_nat (_, k) -> - let x = accu in - let res = Script_int.is_nat x in - (step [@ocaml.tailcall]) g gas k ks res stack - | IAbs_int (_, k) -> - let x = accu in - let res = Script_int.abs x in - (step [@ocaml.tailcall]) g gas k ks res stack - | IInt_nat (_, k) -> - let x = accu in - let res = Script_int.int x in - (step [@ocaml.tailcall]) g gas k ks res stack - | INeg (_, k) -> - let x = accu in - let res = Script_int.neg x in - (step [@ocaml.tailcall]) g gas k ks res stack - | IAdd_int (_, k) -> - let x = accu and y, stack = stack in - let res = Script_int.add x y in - (step [@ocaml.tailcall]) g gas k ks res stack - | IAdd_nat (_, k) -> - let x = accu and y, stack = stack in - let res = Script_int.add_n x y in - (step [@ocaml.tailcall]) g gas k ks res stack - | ISub_int (_, k) -> - let x = accu and y, stack = stack in - let res = Script_int.sub x y in - (step [@ocaml.tailcall]) g gas k ks res stack - | IMul_int (_, k) -> - let x = accu and y, stack = stack in - let res = Script_int.mul x y in - (step [@ocaml.tailcall]) g gas k ks res stack - | IMul_nat (_, k) -> - let x = accu and y, stack = stack in - let res = Script_int.mul_n x y in - (step [@ocaml.tailcall]) g gas k ks res stack - | IEdiv_teznat (_, k) -> - let x = accu and y, stack = stack in - let x = Script_int.of_int64 (Tez.to_mutez x) in - let result = - match Script_int.ediv x y with - | None -> None - | Some (q, r) -> ( - match (Script_int.to_int64 q, Script_int.to_int64 r) with - | Some q, Some r -> ( - match (Tez.of_mutez q, Tez.of_mutez r) with - | Some q, Some r -> Some (q, r) - (* Cannot overflow *) - | _ -> assert false) - (* Cannot overflow *) - | _ -> assert false) - in - (step [@ocaml.tailcall]) g gas k ks result stack - | IEdiv_tez (_, k) -> - let x = accu and y, stack = stack in - let x = Script_int.abs (Script_int.of_int64 (Tez.to_mutez x)) in - let y = Script_int.abs (Script_int.of_int64 (Tez.to_mutez y)) in - let result = - match Script_int.ediv_n x y with - | None -> None - | Some (q, r) -> ( - match Script_int.to_int64 r with - | None -> assert false (* Cannot overflow *) - | Some r -> ( - match Tez.of_mutez r with - | None -> assert false (* Cannot overflow *) - | Some r -> Some (q, r))) - in - (step [@ocaml.tailcall]) g gas k ks result stack - | IEdiv_int (_, k) -> - let x = accu and y, stack = stack in - let res = Script_int.ediv x y in - (step [@ocaml.tailcall]) g gas k ks res stack - | IEdiv_nat (_, k) -> - let x = accu and y, stack = stack in - let res = Script_int.ediv_n x y in - (step [@ocaml.tailcall]) g gas k ks res stack - | ILsl_nat (loc, k) -> ilsl_nat None g gas loc k ks accu stack - | ILsr_nat (loc, k) -> ilsr_nat None g gas loc k ks accu stack - | IOr_nat (_, k) -> - let x = accu and y, stack = stack in - let res = Script_int.logor x y in - (step [@ocaml.tailcall]) g gas k ks res stack - | IAnd_nat (_, k) -> - let x = accu and y, stack = stack in - let res = Script_int.logand x y in - (step [@ocaml.tailcall]) g gas k ks res stack - | IAnd_int_nat (_, k) -> - let x = accu and y, stack = stack in - let res = Script_int.logand x y in - (step [@ocaml.tailcall]) g gas k ks res stack - | IXor_nat (_, k) -> - let x = accu and y, stack = stack in - let res = Script_int.logxor x y in - (step [@ocaml.tailcall]) g gas k ks res stack - | INot_int (_, k) -> - let x = accu in - let res = Script_int.lognot x in - (step [@ocaml.tailcall]) g gas k ks res stack - (* control *) - | IIf {branch_if_true; branch_if_false; k; _} -> - let res, stack = stack in - if accu then - (step [@ocaml.tailcall]) - g - gas - branch_if_true - (KCons (k, ks)) - res - stack - else - (step [@ocaml.tailcall]) + | ILoop (_, body, k) -> + let ks = KLoop_in (body, KCons (k, ks)) in + (next [@ocaml.tailcall]) g gas ks accu stack + | ILoop_left (_, bl, br) -> + let ks = KLoop_in_left (bl, KCons (br, ks)) in + (next [@ocaml.tailcall]) g gas ks accu stack + | IDip (_, b, ty, k) -> + let ign = accu in + let ks = KUndip (ign, ty, KCons (k, ks)) in + let accu, stack = stack in + (step [@ocaml.tailcall]) g gas b ks accu stack + | IExec (_, sty, k) -> iexec id None g gas sty k ks accu stack + | IApply (_, capture_ty, k) -> + let capture = accu in + let lam, stack = stack in + apply ctxt gas capture_ty capture lam >>=? fun (lam', ctxt, gas) -> + (step [@ocaml.tailcall]) (ctxt, sc) gas k ks lam' stack + | ILambda (_, lam, k) -> + (step [@ocaml.tailcall]) g gas k ks lam (accu, stack) + | IFailwith (kloc, tv) -> + let {ifailwith} = ifailwith in + ifailwith None g gas kloc tv accu + (* comparison *) + | ICompare (_, ty, k) -> + let a = accu in + let b, stack = stack in + let r = + Script_int.of_int @@ Script_comparable.compare_comparable ty a b + in + (step [@ocaml.tailcall]) g gas k ks r stack + (* comparators *) + | IEq (_, k) -> + let a = accu in + let a = Script_int.compare a Script_int.zero in + let a = Compare.Int.(a = 0) in + (step [@ocaml.tailcall]) g gas k ks a stack + | INeq (_, k) -> + let a = accu in + let a = Script_int.compare a Script_int.zero in + let a = Compare.Int.(a <> 0) in + (step [@ocaml.tailcall]) g gas k ks a stack + | ILt (_, k) -> + let a = accu in + let a = Script_int.compare a Script_int.zero in + let a = Compare.Int.(a < 0) in + (step [@ocaml.tailcall]) g gas k ks a stack + | ILe (_, k) -> + let a = accu in + let a = Script_int.compare a Script_int.zero in + let a = Compare.Int.(a <= 0) in + (step [@ocaml.tailcall]) g gas k ks a stack + | IGt (_, k) -> + let a = accu in + let a = Script_int.compare a Script_int.zero in + let a = Compare.Int.(a > 0) in + (step [@ocaml.tailcall]) g gas k ks a stack + | IGe (_, k) -> + let a = accu in + let a = Script_int.compare a Script_int.zero in + let a = Compare.Int.(a >= 0) in + (step [@ocaml.tailcall]) g gas k ks a stack + (* packing *) + | IPack (_, ty, k) -> + let value = accu in + ( use_gas_counter_in_context ctxt gas @@ fun ctxt -> + Script_ir_translator.pack_data ctxt ty value ) + >>=? fun (bytes, ctxt, gas) -> + (step [@ocaml.tailcall]) (ctxt, sc) gas k ks bytes stack + | IUnpack (_, ty, k) -> + let bytes = accu in + ( use_gas_counter_in_context ctxt gas @@ fun ctxt -> + unpack ctxt ~ty ~bytes ) + >>=? fun (opt, ctxt, gas) -> + (step [@ocaml.tailcall]) (ctxt, sc) gas k ks opt stack + | IAddress (_, k) -> + let typed_contract = accu in + let destination = Typed_contract.destination typed_contract in + let entrypoint = Typed_contract.entrypoint typed_contract in + let address = {destination; entrypoint} in + (step [@ocaml.tailcall]) g gas k ks address stack + | IContract (loc, t, entrypoint, k) -> ( + let addr = accu in + let entrypoint_opt = + if Entrypoint.is_default addr.entrypoint then Some entrypoint + else if Entrypoint.is_default entrypoint then Some addr.entrypoint + else (* both entrypoints are non-default *) None + in + match entrypoint_opt with + | Some entrypoint -> + let ctxt = update_context gas ctxt in + Script_ir_translator.parse_contract_for_script + ctxt + loc + t + addr.destination + ~entrypoint + >>=? fun (ctxt, maybe_contract) -> + let gas, ctxt = local_gas_counter_and_outdated_context ctxt in + let accu = maybe_contract in + (step [@ocaml.tailcall]) (ctxt, sc) gas k ks accu stack + | None -> (step [@ocaml.tailcall]) (ctxt, sc) gas k ks None stack) + | ITransfer_tokens (loc, k) -> + let p = accu in + let amount, (typed_contract, stack) = stack in + transfer (ctxt, sc) gas amount loc typed_contract p + >>=? fun (accu, ctxt, gas) -> + (step [@ocaml.tailcall]) (ctxt, sc) gas k ks accu stack + | IImplicit_account (_, k) -> + let key = accu in + let res = Typed_implicit key in + (step [@ocaml.tailcall]) g gas k ks res stack + | IView (_, view_signature, stack_ty, k) -> + (iview [@ocaml.tailcall]) + id g gas - branch_if_false - (KCons (k, ks)) - res - stack - | ILoop (_, body, k) -> - let ks = KLoop_in (body, KCons (k, ks)) in - (next [@ocaml.tailcall]) g gas ks accu stack - | ILoop_left (_, bl, br) -> - let ks = KLoop_in_left (bl, KCons (br, ks)) in - (next [@ocaml.tailcall]) g gas ks accu stack - | IDip (_, b, ty, k) -> - let ign = accu in - let ks = KUndip (ign, ty, KCons (k, ks)) in - let accu, stack = stack in - (step [@ocaml.tailcall]) g gas b ks accu stack - | IExec (_, sty, k) -> iexec id None g gas sty k ks accu stack - | IApply (_, capture_ty, k) -> - let capture = accu in - let lam, stack = stack in - apply ctxt gas capture_ty capture lam >>=? fun (lam', ctxt, gas) -> - (step [@ocaml.tailcall]) (ctxt, sc) gas k ks lam' stack - | ILambda (_, lam, k) -> - (step [@ocaml.tailcall]) g gas k ks lam (accu, stack) - | IFailwith (kloc, tv) -> - let {ifailwith} = ifailwith in - ifailwith None g gas kloc tv accu - (* comparison *) - | ICompare (_, ty, k) -> - let a = accu in - let b, stack = stack in - let r = - Script_int.of_int @@ Script_comparable.compare_comparable ty a b - in - (step [@ocaml.tailcall]) g gas k ks r stack - (* comparators *) - | IEq (_, k) -> - let a = accu in - let a = Script_int.compare a Script_int.zero in - let a = Compare.Int.(a = 0) in - (step [@ocaml.tailcall]) g gas k ks a stack - | INeq (_, k) -> - let a = accu in - let a = Script_int.compare a Script_int.zero in - let a = Compare.Int.(a <> 0) in - (step [@ocaml.tailcall]) g gas k ks a stack - | ILt (_, k) -> - let a = accu in - let a = Script_int.compare a Script_int.zero in - let a = Compare.Int.(a < 0) in - (step [@ocaml.tailcall]) g gas k ks a stack - | ILe (_, k) -> - let a = accu in - let a = Script_int.compare a Script_int.zero in - let a = Compare.Int.(a <= 0) in - (step [@ocaml.tailcall]) g gas k ks a stack - | IGt (_, k) -> - let a = accu in - let a = Script_int.compare a Script_int.zero in - let a = Compare.Int.(a > 0) in - (step [@ocaml.tailcall]) g gas k ks a stack - | IGe (_, k) -> - let a = accu in - let a = Script_int.compare a Script_int.zero in - let a = Compare.Int.(a >= 0) in - (step [@ocaml.tailcall]) g gas k ks a stack - (* packing *) - | IPack (_, ty, k) -> - let value = accu in - ( use_gas_counter_in_context ctxt gas @@ fun ctxt -> - Script_ir_translator.pack_data ctxt ty value ) - >>=? fun (bytes, ctxt, gas) -> - (step [@ocaml.tailcall]) (ctxt, sc) gas k ks bytes stack - | IUnpack (_, ty, k) -> - let bytes = accu in - ( use_gas_counter_in_context ctxt gas @@ fun ctxt -> - unpack ctxt ~ty ~bytes ) - >>=? fun (opt, ctxt, gas) -> - (step [@ocaml.tailcall]) (ctxt, sc) gas k ks opt stack - | IAddress (_, k) -> - let typed_contract = accu in - let destination = Typed_contract.destination typed_contract in - let entrypoint = Typed_contract.entrypoint typed_contract in - let address = {destination; entrypoint} in - (step [@ocaml.tailcall]) g gas k ks address stack - | IContract (loc, t, entrypoint, k) -> ( - let addr = accu in - let entrypoint_opt = - if Entrypoint.is_default addr.entrypoint then Some entrypoint - else if Entrypoint.is_default entrypoint then Some addr.entrypoint - else (* both entrypoints are non-default *) None - in - match entrypoint_opt with - | Some entrypoint -> - let ctxt = update_context gas ctxt in - Script_ir_translator.parse_contract_for_script - ctxt - loc - t - addr.destination - ~entrypoint - >>=? fun (ctxt, maybe_contract) -> - let gas, ctxt = local_gas_counter_and_outdated_context ctxt in - let accu = maybe_contract in - (step [@ocaml.tailcall]) (ctxt, sc) gas k ks accu stack - | None -> (step [@ocaml.tailcall]) (ctxt, sc) gas k ks None stack) - | ITransfer_tokens (loc, k) -> - let p = accu in - let amount, (typed_contract, stack) = stack in - transfer (ctxt, sc) gas amount loc typed_contract p - >>=? fun (accu, ctxt, gas) -> - (step [@ocaml.tailcall]) (ctxt, sc) gas k ks accu stack - | IImplicit_account (_, k) -> - let key = accu in - let res = Typed_implicit key in - (step [@ocaml.tailcall]) g gas k ks res stack - | IView (_, view_signature, stack_ty, k) -> - (iview [@ocaml.tailcall]) - id - g - gas - view_signature - stack_ty - k - ks - accu - stack - | ICreate_contract {storage_type; code; k; loc = _} -> - (* Removed the instruction's arguments manager, spendable and delegatable *) - let delegate = accu in - let credit, (init, stack) = stack in - create_contract g gas storage_type code delegate credit init - >>=? fun (res, contract, ctxt, gas) -> - let destination = Destination.Contract (Originated contract) in - let stack = ({destination; entrypoint = Entrypoint.default}, stack) in - (step [@ocaml.tailcall]) (ctxt, sc) gas k ks res stack - | ISet_delegate (_, k) -> - let delegate = accu in - let operation = Delegation delegate in - let ctxt = update_context gas ctxt in - fresh_internal_nonce ctxt >>?= fun (ctxt, nonce) -> - let piop = - Internal_operation - {source = Contract.Originated sc.self; operation; nonce} - in - let res = {piop; lazy_storage_diff = None} in - let gas, ctxt = local_gas_counter_and_outdated_context ctxt in - (step [@ocaml.tailcall]) (ctxt, sc) gas k ks res stack - | IBalance (_, k) -> - let ctxt = update_context gas ctxt in - let gas, ctxt = local_gas_counter_and_outdated_context ctxt in - let g = (ctxt, sc) in - (step [@ocaml.tailcall]) g gas k ks sc.balance (accu, stack) - | ILevel (_, k) -> - (step [@ocaml.tailcall]) g gas k ks sc.level (accu, stack) - | INow (_, k) -> (step [@ocaml.tailcall]) g gas k ks sc.now (accu, stack) - | IMin_block_time (_, k) -> - let ctxt = update_context gas ctxt in - let min_block_time = - Alpha_context.Constants.minimal_block_delay ctxt - |> Period.to_seconds |> Script_int.of_int64 - (* Realistically the block delay is never negative. *) - |> Script_int.abs - in - let new_stack = (accu, stack) in - (step [@ocaml.tailcall]) g gas k ks min_block_time new_stack - | ICheck_signature (_, k) -> - let key = accu and signature, (message, stack) = stack in - let res = Script_signature.check key signature message in - (step [@ocaml.tailcall]) g gas k ks res stack - | IHash_key (_, k) -> - let key = accu in - let res = Signature.Public_key.hash key in - (step [@ocaml.tailcall]) g gas k ks res stack - | IBlake2b (_, k) -> - let bytes = accu in - let hash = Raw_hashes.blake2b bytes in - (step [@ocaml.tailcall]) g gas k ks hash stack - | ISha256 (_, k) -> - let bytes = accu in - let hash = Raw_hashes.sha256 bytes in - (step [@ocaml.tailcall]) g gas k ks hash stack - | ISha512 (_, k) -> - let bytes = accu in - let hash = Raw_hashes.sha512 bytes in - (step [@ocaml.tailcall]) g gas k ks hash stack - | ISource (_, k) -> - let destination : Destination.t = Contract (Implicit sc.payer) in - let res = {destination; entrypoint = Entrypoint.default} in - (step [@ocaml.tailcall]) g gas k ks res (accu, stack) - | ISender (_, k) -> - let destination : Destination.t = Contract sc.source in - let res = {destination; entrypoint = Entrypoint.default} in - (step [@ocaml.tailcall]) g gas k ks res (accu, stack) - | ISelf (_, ty, entrypoint, k) -> - let res = - Typed_originated {arg_ty = ty; contract_hash = sc.self; entrypoint} - in - (step [@ocaml.tailcall]) g gas k ks res (accu, stack) - | ISelf_address (_, k) -> - let destination : Destination.t = Contract (Originated sc.self) in - let res = {destination; entrypoint = Entrypoint.default} in - (step [@ocaml.tailcall]) g gas k ks res (accu, stack) - | IAmount (_, k) -> - let accu = sc.amount and stack = (accu, stack) in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IDig (_, _n, n', k) -> - let (accu, stack), x = - interp_stack_prefix_preserving_operation - (fun v stack -> (stack, v)) - n' - accu - stack - in - let accu = x and stack = (accu, stack) in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IDug (_, _n, n', k) -> - let v = accu in - let accu, stack = stack in - let (accu, stack), () = - interp_stack_prefix_preserving_operation - (fun accu stack -> ((v, (accu, stack)), ())) - n' + view_signature + stack_ty + k + ks accu stack - in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IDipn (_, _n, n', b, k) -> - let accu, stack, restore_prefix = kundip n' accu stack k in - let ks = KCons (restore_prefix, ks) in - (step [@ocaml.tailcall]) g gas b ks accu stack - | IDropn (_, _n, n', k) -> - let stack = + | ICreate_contract {storage_type; code; k; loc = _} -> + (* Removed the instruction's arguments manager, spendable and delegatable *) + let delegate = accu in + let credit, (init, stack) = stack in + create_contract g gas storage_type code delegate credit init + >>=? fun (res, contract, ctxt, gas) -> + let destination = Destination.Contract (Originated contract) in + let stack = + ({destination; entrypoint = Entrypoint.default}, stack) + in + (step [@ocaml.tailcall]) (ctxt, sc) gas k ks res stack + | ISet_delegate (_, k) -> + let delegate = accu in + let operation = Delegation delegate in + let ctxt = update_context gas ctxt in + fresh_internal_nonce ctxt >>?= fun (ctxt, nonce) -> + let piop = + Internal_operation + {source = Contract.Originated sc.self; operation; nonce} + in + let res = {piop; lazy_storage_diff = None} in + let gas, ctxt = local_gas_counter_and_outdated_context ctxt in + (step [@ocaml.tailcall]) (ctxt, sc) gas k ks res stack + | IBalance (_, k) -> + let ctxt = update_context gas ctxt in + let gas, ctxt = local_gas_counter_and_outdated_context ctxt in + let g = (ctxt, sc) in + (step [@ocaml.tailcall]) g gas k ks sc.balance (accu, stack) + | ILevel (_, k) -> + (step [@ocaml.tailcall]) g gas k ks sc.level (accu, stack) + | INow (_, k) -> (step [@ocaml.tailcall]) g gas k ks sc.now (accu, stack) + | IMin_block_time (_, k) -> + let ctxt = update_context gas ctxt in + let min_block_time = + Alpha_context.Constants.minimal_block_delay ctxt + |> Period.to_seconds |> Script_int.of_int64 + (* Realistically the block delay is never negative. *) + |> Script_int.abs + in + let new_stack = (accu, stack) in + (step [@ocaml.tailcall]) g gas k ks min_block_time new_stack + | ICheck_signature (_, k) -> + let key = accu and signature, (message, stack) = stack in + let res = Script_signature.check key signature message in + (step [@ocaml.tailcall]) g gas k ks res stack + | IHash_key (_, k) -> + let key = accu in + let res = Signature.Public_key.hash key in + (step [@ocaml.tailcall]) g gas k ks res stack + | IBlake2b (_, k) -> + let bytes = accu in + let hash = Raw_hashes.blake2b bytes in + (step [@ocaml.tailcall]) g gas k ks hash stack + | ISha256 (_, k) -> + let bytes = accu in + let hash = Raw_hashes.sha256 bytes in + (step [@ocaml.tailcall]) g gas k ks hash stack + | ISha512 (_, k) -> + let bytes = accu in + let hash = Raw_hashes.sha512 bytes in + (step [@ocaml.tailcall]) g gas k ks hash stack + | ISource (_, k) -> + let destination : Destination.t = Contract (Implicit sc.payer) in + let res = {destination; entrypoint = Entrypoint.default} in + (step [@ocaml.tailcall]) g gas k ks res (accu, stack) + | ISender (_, k) -> + let destination : Destination.t = Contract sc.source in + let res = {destination; entrypoint = Entrypoint.default} in + (step [@ocaml.tailcall]) g gas k ks res (accu, stack) + | ISelf (_, ty, entrypoint, k) -> + let res = + Typed_originated + {arg_ty = ty; contract_hash = sc.self; entrypoint} + in + (step [@ocaml.tailcall]) g gas k ks res (accu, stack) + | ISelf_address (_, k) -> + let destination : Destination.t = Contract (Originated sc.self) in + let res = {destination; entrypoint = Entrypoint.default} in + (step [@ocaml.tailcall]) g gas k ks res (accu, stack) + | IAmount (_, k) -> + let accu = sc.amount and stack = (accu, stack) in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IDig (_, _n, n', k) -> + let (accu, stack), x = + interp_stack_prefix_preserving_operation + (fun v stack -> (stack, v)) + n' + accu + stack + in + let accu = x and stack = (accu, stack) in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IDug (_, _n, n', k) -> + let v = accu in + let accu, stack = stack in + let (accu, stack), () = + interp_stack_prefix_preserving_operation + (fun accu stack -> ((v, (accu, stack)), ())) + n' + accu + stack + in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IDipn (_, _n, n', b, k) -> + let accu, stack, restore_prefix = kundip n' accu stack k in + let ks = KCons (restore_prefix, ks) in + (step [@ocaml.tailcall]) g gas b ks accu stack + | IDropn (_, _n, n', k) -> + let stack = + let rec aux : + type a s b t. + (b, t, b, t, a, s, a, s) stack_prefix_preservation_witness -> + a -> + s -> + b * t = + fun w accu stack -> + match w with + | KRest -> (accu, stack) + | KPrefix (_, _ty, w) -> + let accu, stack = stack in + aux w accu stack + in + aux n' accu stack + in + let accu, stack = stack in + (step [@ocaml.tailcall]) g gas k ks accu stack + | ISapling_empty_state (_, memo_size, k) -> + let state = Sapling.empty_state ~memo_size () in + (step [@ocaml.tailcall]) g gas k ks state (accu, stack) + | ISapling_verify_update (_, k) -> ( + let transaction = accu in + let state, stack = stack in + let address = Contract_hash.to_b58check sc.self in + let sc_chain_id = Script_chain_id.make sc.chain_id in + let chain_id = Script_chain_id.to_b58check sc_chain_id in + let anti_replay = address ^ chain_id in + let ctxt = update_context gas ctxt in + Sapling.verify_update ctxt state transaction anti_replay + >>=? fun (ctxt, balance_state_opt) -> + let gas, ctxt = local_gas_counter_and_outdated_context ctxt in + match balance_state_opt with + | Some (balance, state) -> + let state = + Some + ( Bytes.of_string transaction.bound_data, + (Script_int.of_int64 balance, state) ) + in + (step [@ocaml.tailcall]) (ctxt, sc) gas k ks state stack + | None -> (step [@ocaml.tailcall]) (ctxt, sc) gas k ks None stack) + | ISapling_verify_update_deprecated (_, k) -> ( + let transaction = accu in + let state, stack = stack in + let address = Contract_hash.to_b58check sc.self in + let sc_chain_id = Script_chain_id.make sc.chain_id in + let chain_id = Script_chain_id.to_b58check sc_chain_id in + let anti_replay = address ^ chain_id in + let ctxt = update_context gas ctxt in + Sapling.Legacy.verify_update ctxt state transaction anti_replay + >>=? fun (ctxt, balance_state_opt) -> + let gas, ctxt = local_gas_counter_and_outdated_context ctxt in + match balance_state_opt with + | Some (balance, state) -> + let state = Some (Script_int.of_int64 balance, state) in + (step [@ocaml.tailcall]) (ctxt, sc) gas k ks state stack + | None -> (step [@ocaml.tailcall]) (ctxt, sc) gas k ks None stack) + | IChainId (_, k) -> + let accu = Script_chain_id.make sc.chain_id + and stack = (accu, stack) in + (step [@ocaml.tailcall]) g gas k ks accu stack + | INever _ -> ( match accu with _ -> .) + | IVoting_power (_, k) -> + let key_hash = accu in + let ctxt = update_context gas ctxt in + Vote.get_voting_power ctxt key_hash >>=? fun (ctxt, power) -> + let power = Script_int.(abs (of_int64 power)) in + let gas, ctxt = local_gas_counter_and_outdated_context ctxt in + (step [@ocaml.tailcall]) (ctxt, sc) gas k ks power stack + | ITotal_voting_power (_, k) -> + let ctxt = update_context gas ctxt in + Vote.get_total_voting_power ctxt >>=? fun (ctxt, power) -> + let power = Script_int.(abs (of_int64 power)) in + let gas, ctxt = local_gas_counter_and_outdated_context ctxt in + let g = (ctxt, sc) in + (step [@ocaml.tailcall]) g gas k ks power (accu, stack) + | IKeccak (_, k) -> + let bytes = accu in + let hash = Raw_hashes.keccak256 bytes in + (step [@ocaml.tailcall]) g gas k ks hash stack + | ISha3 (_, k) -> + let bytes = accu in + let hash = Raw_hashes.sha3_256 bytes in + (step [@ocaml.tailcall]) g gas k ks hash stack + | IAdd_bls12_381_g1 (_, k) -> + let x = accu and y, stack = stack in + let accu = Script_bls.G1.add x y in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IAdd_bls12_381_g2 (_, k) -> + let x = accu and y, stack = stack in + let accu = Script_bls.G2.add x y in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IAdd_bls12_381_fr (_, k) -> + let x = accu and y, stack = stack in + let accu = Script_bls.Fr.add x y in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IMul_bls12_381_g1 (_, k) -> + let x = accu and y, stack = stack in + let accu = Script_bls.G1.mul x y in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IMul_bls12_381_g2 (_, k) -> + let x = accu and y, stack = stack in + let accu = Script_bls.G2.mul x y in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IMul_bls12_381_fr (_, k) -> + let x = accu and y, stack = stack in + let accu = Script_bls.Fr.mul x y in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IMul_bls12_381_fr_z (_, k) -> + let x = accu and y, stack = stack in + let x = Script_bls.Fr.of_z (Script_int.to_zint x) in + let res = Script_bls.Fr.mul x y in + (step [@ocaml.tailcall]) g gas k ks res stack + | IMul_bls12_381_z_fr (_, k) -> + let y = accu and x, stack = stack in + let x = Script_bls.Fr.of_z (Script_int.to_zint x) in + let res = Script_bls.Fr.mul x y in + (step [@ocaml.tailcall]) g gas k ks res stack + | IInt_bls12_381_fr (_, k) -> + let x = accu in + let res = Script_int.of_zint (Script_bls.Fr.to_z x) in + (step [@ocaml.tailcall]) g gas k ks res stack + | INeg_bls12_381_g1 (_, k) -> + let x = accu in + let accu = Script_bls.G1.negate x in + (step [@ocaml.tailcall]) g gas k ks accu stack + | INeg_bls12_381_g2 (_, k) -> + let x = accu in + let accu = Script_bls.G2.negate x in + (step [@ocaml.tailcall]) g gas k ks accu stack + | INeg_bls12_381_fr (_, k) -> + let x = accu in + let accu = Script_bls.Fr.negate x in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IPairing_check_bls12_381 (_, k) -> + let pairs = accu in + let check = Script_bls.pairing_check pairs.elements in + (step [@ocaml.tailcall]) g gas k ks check stack + | IComb (_, _, witness, k) -> let rec aux : - type a s b t. - (b, t, b, t, a, s, a, s) stack_prefix_preservation_witness -> - a -> - s -> - b * t = - fun w accu stack -> - match w with - | KRest -> (accu, stack) - | KPrefix (_, _ty, w) -> - let accu, stack = stack in - aux w accu stack + type a b s c d t. + (a, b, s, c, d, t) comb_gadt_witness -> + a * (b * s) -> + c * (d * t) = + fun witness stack -> + match (witness, stack) with + | Comb_one, stack -> stack + | Comb_succ witness', (a, tl) -> + let b, tl' = aux witness' tl in + ((a, b), tl') in - aux n' accu stack - in - let accu, stack = stack in - (step [@ocaml.tailcall]) g gas k ks accu stack - | ISapling_empty_state (_, memo_size, k) -> - let state = Sapling.empty_state ~memo_size () in - (step [@ocaml.tailcall]) g gas k ks state (accu, stack) - | ISapling_verify_update (_, k) -> ( - let transaction = accu in - let state, stack = stack in - let address = Contract_hash.to_b58check sc.self in - let sc_chain_id = Script_chain_id.make sc.chain_id in - let chain_id = Script_chain_id.to_b58check sc_chain_id in - let anti_replay = address ^ chain_id in - let ctxt = update_context gas ctxt in - Sapling.verify_update ctxt state transaction anti_replay - >>=? fun (ctxt, balance_state_opt) -> - let gas, ctxt = local_gas_counter_and_outdated_context ctxt in - match balance_state_opt with - | Some (balance, state) -> - let state = + let stack = aux witness (accu, stack) in + let accu, stack = stack in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IUncomb (_, _, witness, k) -> + let rec aux : + type a b s c d t. + (a, b, s, c, d, t) uncomb_gadt_witness -> + a * (b * s) -> + c * (d * t) = + fun witness stack -> + match (witness, stack) with + | Uncomb_one, stack -> stack + | Uncomb_succ witness', ((a, b), tl) -> (a, aux witness' (b, tl)) + in + let stack = aux witness (accu, stack) in + let accu, stack = stack in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IComb_get (_, _, witness, k) -> + let comb = accu in + let rec aux : + type before after. + (before, after) comb_get_gadt_witness -> before -> after = + fun witness comb -> + match (witness, comb) with + | Comb_get_zero, v -> v + | Comb_get_one, (a, _) -> a + | Comb_get_plus_two witness', (_, b) -> aux witness' b + in + let accu = aux witness comb in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IComb_set (_, _, witness, k) -> + let value = accu and comb, stack = stack in + let rec aux : + type value before after. + (value, before, after) comb_set_gadt_witness -> + value -> + before -> + after = + fun witness value item -> + match (witness, item) with + | Comb_set_zero, _ -> value + | Comb_set_one, (_hd, tl) -> (value, tl) + | Comb_set_plus_two witness', (hd, tl) -> + (hd, aux witness' value tl) + in + let accu = aux witness value comb in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IDup_n (_, _, witness, k) -> + let rec aux : + type a b before after. + (a, b, before, after) dup_n_gadt_witness -> + a * (b * before) -> + after = + fun witness stack -> + match (witness, stack) with + | Dup_n_zero, (a, _) -> a + | Dup_n_succ witness', (_, tl) -> aux witness' tl + in + let stack = (accu, stack) in + let accu = aux witness stack in + (step [@ocaml.tailcall]) g gas k ks accu stack + (* Tickets *) + | ITicket_deprecated (_, _, k) -> ( + let contents = accu and amount, stack = stack in + match Ticket_amount.of_n amount with + | Some amount -> + let ticketer = Contract.Originated sc.self in + let accu = {ticketer; contents; amount} in + (step [@ocaml.tailcall]) g gas k ks accu stack + | None -> fail Script_tc_errors.Forbidden_zero_ticket_quantity) + | ITicket (_, _, k) -> ( + let contents = accu and amount, stack = stack in + match Ticket_amount.of_n amount with + | Some amount -> + let ticketer = Contract.Originated sc.self in + let accu = Some {ticketer; contents; amount} in + (step [@ocaml.tailcall]) g gas k ks accu stack + | None -> (step [@ocaml.tailcall]) g gas k ks None stack) + | IRead_ticket (_, _, k) -> + let {ticketer; contents; amount} = accu in + let stack = (accu, stack) in + let destination : Destination.t = Contract ticketer in + let addr = {destination; entrypoint = Entrypoint.default} in + let accu = + (addr, (contents, (amount :> Script_int.n Script_int.num))) + in + (step [@ocaml.tailcall]) g gas k ks accu stack + | ISplit_ticket (_, k) -> + let ticket = accu and (amount_a, amount_b), stack = stack in + let result = + Option.bind (Ticket_amount.of_n amount_a) @@ fun amount_a -> + Option.bind (Ticket_amount.of_n amount_b) @@ fun amount_b -> + let amount = Ticket_amount.add amount_a amount_b in + if + Compare.Int.( + Script_int.( + compare (amount :> n num) (ticket.amount :> n num)) + = 0) + then Some - ( Bytes.of_string transaction.bound_data, - (Script_int.of_int64 balance, state) ) - in - (step [@ocaml.tailcall]) (ctxt, sc) gas k ks state stack - | None -> (step [@ocaml.tailcall]) (ctxt, sc) gas k ks None stack) - | ISapling_verify_update_deprecated (_, k) -> ( - let transaction = accu in - let state, stack = stack in - let address = Contract_hash.to_b58check sc.self in - let sc_chain_id = Script_chain_id.make sc.chain_id in - let chain_id = Script_chain_id.to_b58check sc_chain_id in - let anti_replay = address ^ chain_id in - let ctxt = update_context gas ctxt in - Sapling.Legacy.verify_update ctxt state transaction anti_replay - >>=? fun (ctxt, balance_state_opt) -> - let gas, ctxt = local_gas_counter_and_outdated_context ctxt in - match balance_state_opt with - | Some (balance, state) -> - let state = Some (Script_int.of_int64 balance, state) in - (step [@ocaml.tailcall]) (ctxt, sc) gas k ks state stack - | None -> (step [@ocaml.tailcall]) (ctxt, sc) gas k ks None stack) - | IChainId (_, k) -> - let accu = Script_chain_id.make sc.chain_id - and stack = (accu, stack) in - (step [@ocaml.tailcall]) g gas k ks accu stack - | INever _ -> ( match accu with _ -> .) - | IVoting_power (_, k) -> - let key_hash = accu in - let ctxt = update_context gas ctxt in - Vote.get_voting_power ctxt key_hash >>=? fun (ctxt, power) -> - let power = Script_int.(abs (of_int64 power)) in - let gas, ctxt = local_gas_counter_and_outdated_context ctxt in - (step [@ocaml.tailcall]) (ctxt, sc) gas k ks power stack - | ITotal_voting_power (_, k) -> - let ctxt = update_context gas ctxt in - Vote.get_total_voting_power ctxt >>=? fun (ctxt, power) -> - let power = Script_int.(abs (of_int64 power)) in - let gas, ctxt = local_gas_counter_and_outdated_context ctxt in - let g = (ctxt, sc) in - (step [@ocaml.tailcall]) g gas k ks power (accu, stack) - | IKeccak (_, k) -> - let bytes = accu in - let hash = Raw_hashes.keccak256 bytes in - (step [@ocaml.tailcall]) g gas k ks hash stack - | ISha3 (_, k) -> - let bytes = accu in - let hash = Raw_hashes.sha3_256 bytes in - (step [@ocaml.tailcall]) g gas k ks hash stack - | IAdd_bls12_381_g1 (_, k) -> - let x = accu and y, stack = stack in - let accu = Script_bls.G1.add x y in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IAdd_bls12_381_g2 (_, k) -> - let x = accu and y, stack = stack in - let accu = Script_bls.G2.add x y in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IAdd_bls12_381_fr (_, k) -> - let x = accu and y, stack = stack in - let accu = Script_bls.Fr.add x y in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IMul_bls12_381_g1 (_, k) -> - let x = accu and y, stack = stack in - let accu = Script_bls.G1.mul x y in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IMul_bls12_381_g2 (_, k) -> - let x = accu and y, stack = stack in - let accu = Script_bls.G2.mul x y in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IMul_bls12_381_fr (_, k) -> - let x = accu and y, stack = stack in - let accu = Script_bls.Fr.mul x y in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IMul_bls12_381_fr_z (_, k) -> - let x = accu and y, stack = stack in - let x = Script_bls.Fr.of_z (Script_int.to_zint x) in - let res = Script_bls.Fr.mul x y in - (step [@ocaml.tailcall]) g gas k ks res stack - | IMul_bls12_381_z_fr (_, k) -> - let y = accu and x, stack = stack in - let x = Script_bls.Fr.of_z (Script_int.to_zint x) in - let res = Script_bls.Fr.mul x y in - (step [@ocaml.tailcall]) g gas k ks res stack - | IInt_bls12_381_fr (_, k) -> - let x = accu in - let res = Script_int.of_zint (Script_bls.Fr.to_z x) in - (step [@ocaml.tailcall]) g gas k ks res stack - | INeg_bls12_381_g1 (_, k) -> - let x = accu in - let accu = Script_bls.G1.negate x in - (step [@ocaml.tailcall]) g gas k ks accu stack - | INeg_bls12_381_g2 (_, k) -> - let x = accu in - let accu = Script_bls.G2.negate x in - (step [@ocaml.tailcall]) g gas k ks accu stack - | INeg_bls12_381_fr (_, k) -> - let x = accu in - let accu = Script_bls.Fr.negate x in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IPairing_check_bls12_381 (_, k) -> - let pairs = accu in - let check = Script_bls.pairing_check pairs.elements in - (step [@ocaml.tailcall]) g gas k ks check stack - | IComb (_, _, witness, k) -> - let rec aux : - type a b s c d t. - (a, b, s, c, d, t) comb_gadt_witness -> a * (b * s) -> c * (d * t) - = - fun witness stack -> - match (witness, stack) with - | Comb_one, stack -> stack - | Comb_succ witness', (a, tl) -> - let b, tl' = aux witness' tl in - ((a, b), tl') - in - let stack = aux witness (accu, stack) in - let accu, stack = stack in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IUncomb (_, _, witness, k) -> - let rec aux : - type a b s c d t. - (a, b, s, c, d, t) uncomb_gadt_witness -> - a * (b * s) -> - c * (d * t) = - fun witness stack -> - match (witness, stack) with - | Uncomb_one, stack -> stack - | Uncomb_succ witness', ((a, b), tl) -> (a, aux witness' (b, tl)) - in - let stack = aux witness (accu, stack) in - let accu, stack = stack in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IComb_get (_, _, witness, k) -> - let comb = accu in - let rec aux : - type before after. - (before, after) comb_get_gadt_witness -> before -> after = - fun witness comb -> - match (witness, comb) with - | Comb_get_zero, v -> v - | Comb_get_one, (a, _) -> a - | Comb_get_plus_two witness', (_, b) -> aux witness' b - in - let accu = aux witness comb in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IComb_set (_, _, witness, k) -> - let value = accu and comb, stack = stack in - let rec aux : - type value before after. - (value, before, after) comb_set_gadt_witness -> - value -> - before -> - after = - fun witness value item -> - match (witness, item) with - | Comb_set_zero, _ -> value - | Comb_set_one, (_hd, tl) -> (value, tl) - | Comb_set_plus_two witness', (hd, tl) -> (hd, aux witness' value tl) - in - let accu = aux witness value comb in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IDup_n (_, _, witness, k) -> - let rec aux : - type a b before after. - (a, b, before, after) dup_n_gadt_witness -> - a * (b * before) -> - after = - fun witness stack -> - match (witness, stack) with - | Dup_n_zero, (a, _) -> a - | Dup_n_succ witness', (_, tl) -> aux witness' tl - in - let stack = (accu, stack) in - let accu = aux witness stack in - (step [@ocaml.tailcall]) g gas k ks accu stack - (* Tickets *) - | ITicket_deprecated (_, _, k) -> ( - let contents = accu and amount, stack = stack in - match Ticket_amount.of_n amount with - | Some amount -> - let ticketer = Contract.Originated sc.self in - let accu = {ticketer; contents; amount} in - (step [@ocaml.tailcall]) g gas k ks accu stack - | None -> fail Script_tc_errors.Forbidden_zero_ticket_quantity) - | ITicket (_, _, k) -> ( - let contents = accu and amount, stack = stack in - match Ticket_amount.of_n amount with - | Some amount -> - let ticketer = Contract.Originated sc.self in - let accu = Some {ticketer; contents; amount} in - (step [@ocaml.tailcall]) g gas k ks accu stack - | None -> (step [@ocaml.tailcall]) g gas k ks None stack) - | IRead_ticket (_, _, k) -> - let {ticketer; contents; amount} = accu in - let stack = (accu, stack) in - let destination : Destination.t = Contract ticketer in - let addr = {destination; entrypoint = Entrypoint.default} in - let accu = - (addr, (contents, (amount :> Script_int.n Script_int.num))) - in - (step [@ocaml.tailcall]) g gas k ks accu stack - | ISplit_ticket (_, k) -> - let ticket = accu and (amount_a, amount_b), stack = stack in - let result = - Option.bind (Ticket_amount.of_n amount_a) @@ fun amount_a -> - Option.bind (Ticket_amount.of_n amount_b) @@ fun amount_b -> - let amount = Ticket_amount.add amount_a amount_b in - if - Compare.Int.( - Script_int.(compare (amount :> n num) (ticket.amount :> n num)) - = 0) - then - Some - ( {ticket with amount = amount_a}, - {ticket with amount = amount_b} ) - else None - in - (step [@ocaml.tailcall]) g gas k ks result stack - | IJoin_tickets (_, contents_ty, k) -> - let ticket_a, ticket_b = accu in - let result = - if - Compare.Int.( - Contract.compare ticket_a.ticketer ticket_b.ticketer = 0 - && Script_comparable.compare_comparable - contents_ty - ticket_a.contents - ticket_b.contents - = 0) - then - Some - { - ticketer = ticket_a.ticketer; - contents = ticket_a.contents; - amount = Ticket_amount.add ticket_a.amount ticket_b.amount; - } - else None - in - (step [@ocaml.tailcall]) g gas k ks result stack - | IOpen_chest (_, k) -> - let open Timelock in - let chest_key = accu in - let chest, (time_z, stack) = stack in - (* If the time is not an integer we then consider the proof as - incorrect. Indeed the verification asks for an integer for practical reasons. - Therefore no proof can be correct.*) - let accu = - match Script_int.to_int time_z with - | None -> R false - | Some time -> ( - match Script_timelock.open_chest chest chest_key ~time with - | Correct bytes -> L bytes - | Bogus_cipher -> R false - | Bogus_opening -> R true) - in - (step [@ocaml.tailcall]) g gas k ks accu stack - | IEmit {tag; ty = event_type; unparsed_ty; k; loc = _} -> - let event_data = accu in - emit_event (ctxt, sc) gas ~event_type ~unparsed_ty ~tag ~event_data - >>=? fun (accu, ctxt, gas) -> - (step [@ocaml.tailcall]) (ctxt, sc) gas k ks accu stack) - -(* - - Zero-cost logging - ================= - -*) - -(* - - The following functions insert a logging instruction to continue - the logging process in the next execution steps. - - There is a special treatment of instructions that generate fresh - continuations: we pass a constructor as argument to their - evaluation rules so that they can instrument these fresh - continuations by themselves. Instructions that create continuations - without calling specialised functions have their branches from [step] - function duplicated and adjusted here. + ( {ticket with amount = amount_a}, + {ticket with amount = amount_b} ) + else None + in + (step [@ocaml.tailcall]) g gas k ks result stack + | IJoin_tickets (_, contents_ty, k) -> + let ticket_a, ticket_b = accu in + let result = + if + Compare.Int.( + Contract.compare ticket_a.ticketer ticket_b.ticketer = 0 + && Script_comparable.compare_comparable + contents_ty + ticket_a.contents + ticket_b.contents + = 0) + then + Some + { + ticketer = ticket_a.ticketer; + contents = ticket_a.contents; + amount = Ticket_amount.add ticket_a.amount ticket_b.amount; + } + else None + in + (step [@ocaml.tailcall]) g gas k ks result stack + | IOpen_chest (_, k) -> + let open Timelock in + let chest_key = accu in + let chest, (time_z, stack) = stack in + (* If the time is not an integer we then consider the proof as + incorrect. Indeed the verification asks for an integer for practical reasons. + Therefore no proof can be correct.*) + let accu = + match Script_int.to_int time_z with + | None -> R false + | Some time -> ( + match Script_timelock.open_chest chest chest_key ~time with + | Correct bytes -> L bytes + | Bogus_cipher -> R false + | Bogus_opening -> R true) + in + (step [@ocaml.tailcall]) g gas k ks accu stack + | IEmit {tag; ty = event_type; unparsed_ty; k; loc = _} -> + let event_data = accu in + emit_event (ctxt, sc) gas ~event_type ~unparsed_ty ~tag ~event_data + >>=? fun (accu, ctxt, gas) -> + (step [@ocaml.tailcall]) (ctxt, sc) gas k ks accu stack) +end - This on-the-fly instrumentation of the execution allows zero-cost - logging since logging instructions are only introduced if an - initial logging continuation is pushed in the initial continuation - that starts the evaluation. +open Raw -*) -and log : - type a s b t r f. - logger * logging_event -> (a, s) stack_ty -> (a, s, b, t, r, f) step_type = - fun (logger, event) sty ((ctxt, _) as g) gas k ks accu stack -> - (match (k, event) with - | ILog _, LogEntry -> () - | _, LogEntry -> - Script_interpreter_logging.log_entry logger ctxt gas k sty accu stack - | _, LogExit prev_loc -> - Script_interpreter_logging.log_exit - logger - ctxt - gas - prev_loc - k - sty - accu - stack) ; - Script_interpreter_logging.log_next_kinstr logger sty k >>?= fun k -> - (* We need to match on instructions that create continuations so - that we can instrument those continuations with [KLog] (see - comment above). For functions that don't do this, we simply call - [step], as they don't require any special treatment. *) - match k with - | IIf_none {branch_if_none; branch_if_some; k; _} -> ( - let (Item_t (Option_t (ty, _, _), rest)) = sty in - Script_interpreter_logging.branched_final_stack_type - [ - Ex_init_stack_ty (rest, branch_if_none); - Ex_init_stack_ty (Item_t (ty, rest), branch_if_some); - ] - >>?= fun sty_opt -> - let ks' = - match sty_opt with - | None -> KCons (k, ks) - | Some sty' -> - Script_interpreter_logging.instrument_cont logger sty' - @@ KCons (k, ks) - in - match accu with - | None -> - let accu, stack = stack in - (step [@ocaml.tailcall]) g gas branch_if_none ks' accu stack - | Some v -> (step [@ocaml.tailcall]) g gas branch_if_some ks' v stack) - | IOpt_map {body; k; loc = _} -> ( - match accu with - | None -> (step [@ocaml.tailcall]) g gas k ks None stack - | Some v -> - let (Item_t (Option_t (ty, _, _), rest)) = sty in - let bsty = Item_t (ty, rest) in - let kmap_head = KMap_head (Option.some, KCons (k, ks)) in - Script_interpreter_logging.kinstr_final_stack_type bsty body - >>?= fun sty_opt -> - let ks' = - match sty_opt with - | None -> kmap_head - | Some sty' -> - Script_interpreter_logging.instrument_cont logger sty' kmap_head - in - (step [@ocaml.tailcall]) g gas body ks' v stack) - | IIf_left {branch_if_left; branch_if_right; k; _} -> ( - let (Item_t (Union_t (lty, rty, _, _), rest)) = sty in - Script_interpreter_logging.branched_final_stack_type - [ - Ex_init_stack_ty (Item_t (lty, rest), branch_if_left); - Ex_init_stack_ty (Item_t (rty, rest), branch_if_right); - ] - >>?= fun sty_opt -> - let k' = - match sty_opt with - | None -> KCons (k, ks) - | Some sty' -> - Script_interpreter_logging.instrument_cont logger sty' - @@ KCons (k, ks) - in - match accu with - | L v -> (step [@ocaml.tailcall]) g gas branch_if_left k' v stack - | R v -> (step [@ocaml.tailcall]) g gas branch_if_right k' v stack) - | IIf_cons {branch_if_cons; branch_if_nil; k; _} -> ( - let (Item_t ((List_t (elty, _) as lty), rest)) = sty in - Script_interpreter_logging.branched_final_stack_type - [ - Ex_init_stack_ty (rest, branch_if_nil); - Ex_init_stack_ty (Item_t (elty, Item_t (lty, rest)), branch_if_cons); - ] - >>?= fun sty' -> - let k' = - match sty' with - | None -> KCons (k, ks) - | Some sty' -> - Script_interpreter_logging.instrument_cont logger sty' - @@ KCons (k, ks) - in - match Script_list.uncons accu with - | None -> - let accu, stack = stack in - (step [@ocaml.tailcall]) g gas branch_if_nil k' accu stack - | Some (hd, tl) -> - (step [@ocaml.tailcall]) g gas branch_if_cons k' hd (tl, stack)) - | IList_map (_, body, ty, k) -> - let (Item_t (_, sty')) = sty in - let instrument = Script_interpreter_logging.instrument_cont logger sty' in - (ilist_map [@ocaml.tailcall]) instrument g gas body k ks ty accu stack - | IList_iter (_, ty, body, k) -> - let (Item_t (_, sty')) = sty in - let instrument = Script_interpreter_logging.instrument_cont logger sty' in - (ilist_iter [@ocaml.tailcall]) instrument g gas body ty k ks accu stack - | ISet_iter (_, ty, body, k) -> - let (Item_t (_, rest)) = sty in - let instrument = Script_interpreter_logging.instrument_cont logger rest in - (iset_iter [@ocaml.tailcall]) instrument g gas body ty k ks accu stack - | IMap_map (_, ty, body, k) -> - let (Item_t (_, rest)) = sty in - let instrument = Script_interpreter_logging.instrument_cont logger rest in - (imap_map [@ocaml.tailcall]) instrument g gas body k ks ty accu stack - | IMap_iter (_, kvty, body, k) -> - let (Item_t (_, rest)) = sty in - let instrument = Script_interpreter_logging.instrument_cont logger rest in - (imap_iter [@ocaml.tailcall]) instrument g gas body kvty k ks accu stack - | IMul_teznat (loc, k) -> - (imul_teznat [@ocaml.tailcall]) (Some logger) g gas loc k ks accu stack - | IMul_nattez (loc, k) -> - (imul_nattez [@ocaml.tailcall]) (Some logger) g gas loc k ks accu stack - | ILsl_nat (loc, k) -> - (ilsl_nat [@ocaml.tailcall]) (Some logger) g gas loc k ks accu stack - | ILsr_nat (loc, k) -> - (ilsr_nat [@ocaml.tailcall]) (Some logger) g gas loc k ks accu stack - | IIf {branch_if_true; branch_if_false; k; _} -> - let (Item_t (Bool_t, rest)) = sty in - Script_interpreter_logging.branched_final_stack_type - [ - Ex_init_stack_ty (rest, branch_if_true); - Ex_init_stack_ty (rest, branch_if_false); - ] - >>?= fun sty' -> - let k' = - match sty' with - | None -> KCons (k, ks) - | Some sty' -> - Script_interpreter_logging.instrument_cont logger sty' - @@ KCons (k, ks) - in - let res, stack = stack in - if accu then (step [@ocaml.tailcall]) g gas branch_if_true k' res stack - else (step [@ocaml.tailcall]) g gas branch_if_false k' res stack - | ILoop (_, body, k) -> - let ks = - Script_interpreter_logging.instrument_cont logger sty - @@ KLoop_in (body, KCons (k, ks)) - in - (next [@ocaml.tailcall]) g gas ks accu stack - | ILoop_left (_, bl, br) -> - let ks = - Script_interpreter_logging.instrument_cont logger sty - @@ KLoop_in_left (bl, KCons (br, ks)) - in - (next [@ocaml.tailcall]) g gas ks accu stack - | IDip (_, b, ty, k) -> - let (Item_t (_, rest)) = sty in - Script_interpreter_logging.kinstr_final_stack_type rest b - >>?= fun rest' -> - let ign = accu in - let ks = - match rest' with - | None -> KUndip (ign, ty, KCons (k, ks)) - | Some rest' -> - Script_interpreter_logging.instrument_cont - logger - rest' - (KUndip (ign, ty, KCons (k, ks))) - in - let accu, stack = stack in - (step [@ocaml.tailcall]) g gas b ks accu stack - | IExec (_, stack_ty, k) -> - let (Item_t (_, Item_t (Lambda_t (_, ret, _), _))) = sty in - let sty' = Item_t (ret, Bot_t) in - let instrument = Script_interpreter_logging.instrument_cont logger sty' in - iexec instrument (Some logger) g gas stack_ty k ks accu stack - | IFailwith (kloc, tv) -> - let {ifailwith} = ifailwith in - (ifailwith [@ocaml.tailcall]) (Some logger) g gas kloc tv accu - | IDipn (_, _n, n', b, k) -> - let accu, stack, restore_prefix = kundip n' accu stack k in - let dipped_sty = Script_interpreter_logging.dipn_stack_ty n' sty in - Script_interpreter_logging.kinstr_final_stack_type dipped_sty b - >>?= fun sty' -> - let ks = - match sty' with - | None -> KCons (restore_prefix, ks) - | Some sty' -> - Script_interpreter_logging.instrument_cont logger sty' - @@ KCons (restore_prefix, ks) - in - (step [@ocaml.tailcall]) g gas b ks accu stack - | IView (_, (View_signature {output_ty; _} as view_signature), stack_ty, k) -> - let sty' = Item_t (output_ty, Bot_t) in - let instrument = Script_interpreter_logging.instrument_cont logger sty' in - (iview [@ocaml.tailcall]) - instrument - g - gas - view_signature - stack_ty - k - ks - accu - stack - | _ -> (step [@ocaml.tailcall]) g gas k ks accu stack - [@@inline] - -and klog : - type a s r f. - logger -> - outdated_context * step_constants -> - local_gas_counter -> - (a, s) stack_ty -> - (a, s, r, f) continuation -> - (a, s, r, f) continuation -> - a -> - s -> - (r * f * outdated_context * local_gas_counter) tzresult Lwt.t = - fun logger g gas stack_ty k0 ks accu stack -> - let ty_for_logging_unsafe = function - (* This function is only called when logging is enabled. If - that's the case, the elaborator must have been called with - [logging_enabled] option, which ensures that this will not be - [None]. Realistically, it can happen that the [logging_enabled] - option was omitted, resulting in a crash here. But this is - acceptable, because logging is never enabled during block - validation, so the layer 1 is safe. *) - | None -> assert false - | Some ty -> ty - in - (match ks with - | KLog _ -> () - | _ -> Script_interpreter_logging.log_control logger ks) ; - Script_interpreter_logging.log_next_continuation logger stack_ty ks - >>?= function - | KCons (ki, k) -> (step [@ocaml.tailcall]) g gas ki k accu stack - | KLoop_in (ki, k) -> (kloop_in [@ocaml.tailcall]) g gas k0 ki k accu stack - | KReturn (_, _, _) as k -> (next [@ocaml.tailcall]) g gas k accu stack - | KLoop_in_left (ki, k) -> - (kloop_in_left [@ocaml.tailcall]) g gas k0 ki k accu stack - | KUndip (_, _, _) as k -> (next [@ocaml.tailcall]) g gas k accu stack - | KIter (body, xty, xs, k) -> - let instrument = - Script_interpreter_logging.instrument_cont logger stack_ty - in - (kiter [@ocaml.tailcall]) instrument g gas body xty xs k accu stack - | KList_enter_body (body, xs, ys, ty_opt, len, k) -> - let instrument = - let ty = ty_for_logging_unsafe ty_opt in - let (List_t (vty, _)) = ty in - let sty = Item_t (vty, stack_ty) in - Script_interpreter_logging.instrument_cont logger sty - in - (klist_enter [@ocaml.tailcall]) - instrument - g - gas - body - xs - ys - ty_opt - len - k - accu - stack - | KList_exit_body (body, xs, ys, ty_opt, len, k) -> - let (Item_t (_, rest)) = stack_ty in - let instrument = Script_interpreter_logging.instrument_cont logger rest in - (klist_exit [@ocaml.tailcall]) - instrument - g - gas - body - xs - ys - ty_opt - len - k - accu - stack - | KMap_enter_body (body, xs, ys, ty_opt, k) -> - let instrument = - let ty = ty_for_logging_unsafe ty_opt in - let (Map_t (_, vty, _)) = ty in - let sty = Item_t (vty, stack_ty) in - Script_interpreter_logging.instrument_cont logger sty - in - (kmap_enter [@ocaml.tailcall]) - instrument - g - gas - body - xs - ty_opt - ys - k - accu - stack - | KMap_exit_body (body, xs, ys, yk, ty_opt, k) -> - let (Item_t (_, rest)) = stack_ty in - let instrument = Script_interpreter_logging.instrument_cont logger rest in - (kmap_exit [@ocaml.tailcall]) - instrument - g - gas - body - xs - ty_opt - ys - yk - k - accu - stack - | KMap_head (f, k) -> (next [@ocaml.taillcall]) g gas k (f accu) stack - | KView_exit (scs, k) -> - (next [@ocaml.tailcall]) (fst g, scs) gas k accu stack - | KLog _ as k -> - (* This case should never happen. *) - (next [@ocaml.tailcall]) g gas k accu stack - | KNil as k -> (next [@ocaml.tailcall]) g gas k accu stack - [@@inline] (* Entrypoints @@ -2169,4 +1859,6 @@ module Internals = struct let step_descr logger ctxt step_constants descr stack = step_descr ~log_now:false logger (ctxt, step_constants) descr stack + + module Raw = Raw end diff --git a/src/proto_alpha/lib_protocol/script_interpreter.mli b/src/proto_alpha/lib_protocol/script_interpreter.mli index a34b6fda98ef222653ea06d990f58247cd658355..0a5a2903cb2b1e87cacc605afd480b252fd48fe6 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter.mli +++ b/src/proto_alpha/lib_protocol/script_interpreter.mli @@ -197,4 +197,57 @@ module Internals : sig 'a -> 's -> ('r * 'f * context) tzresult Lwt.t + + module Raw : sig + open Local_gas_counter + open Script_interpreter_defs + + val kmap_exit : ('a, 'b, 'c, 'e, 'f, 'm, 'n, 'o) kmap_exit_type + + val kmap_enter : ('a, 'b, 'c, 'd, 'f, 'i, 'j, 'k) kmap_enter_type + + val klist_exit : ('a, 'b, 'c, 'd, 'e, 'i, 'j) klist_exit_type + + val klist_enter : ('a, 'b, 'c, 'd, 'e, 'f, 'j) klist_enter_type + + val kloop_in_left : ('a, 'b, 'c, 'd, 'e, 'f, 'g) kloop_in_left_type + + val kloop_in : ('a, 'b, 'c, 'r, 'f, 's) kloop_in_type + + val kiter : ('a, 'b, 's, 'r, 'f, 'c) kiter_type + + val next : + outdated_context * step_constants -> + local_gas_counter -> + ('a, 's, 'r, 'f) continuation -> + 'a -> + 's -> + ('r * 'f * outdated_context * local_gas_counter) tzresult Lwt.t + + val ilist_map : ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i) ilist_map_type + + val ilist_iter : ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'cmp) ilist_iter_type + + val iset_iter : ('a, 'b, 'c, 'd, 'e, 'f, 'g) iset_iter_type + + val imap_map : ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j) imap_map_type + + val imap_iter : ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'cmp) imap_iter_type + + val imul_teznat : ('a, 'b, 'c, 'd, 'e, 'f) imul_teznat_type + + val imul_nattez : ('a, 'b, 'c, 'd, 'e, 'f) imul_nattez_type + + val ilsl_nat : ('a, 'b, 'c, 'd, 'e, 'f) ilsl_nat_type + + val ilsr_nat : ('a, 'b, 'c, 'd, 'e, 'f) ilsr_nat_type + + val ifailwith : ifailwith_type + + val iexec : ('a, 'b, 'c, 'd, 'e, 'f, 'g) iexec_type + + val iview : ('a, 'b, 'c, 'd, 'e, 'f, 'i, 'o) iview_type + + val step : ('a, 's, 'b, 't, 'r, 'f) step_type + end end diff --git a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml index fc13757c117a4e8c2f92667778de7f96db589851..7609b083ec3a66a9f8ef1706848b680e0671f0d4 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml @@ -769,15 +769,6 @@ type ('a, 'b, 'c, 'd) cont_instrumentation = let id x = x -type ('a, 's, 'b, 't, 'r, 'f) step_type = - outdated_context * step_constants -> - local_gas_counter -> - ('a, 's, 'b, 't) kinstr -> - ('b, 't, 'r, 'f) continuation -> - 'a -> - 's -> - ('r * 'f * outdated_context * local_gas_counter) tzresult Lwt.t - type ('a, 'b, 'c, 'e, 'f, 'm, 'n, 'o) kmap_exit_type = ('a, 'b, 'e, 'f) cont_instrumentation -> outdated_context * step_constants -> diff --git a/src/proto_alpha/lib_protocol/script_interpreter_logging.ml b/src/proto_alpha/lib_protocol/script_interpreter_logging.ml deleted file mode 100644 index 4822a9d5fb267e31dc38afb6ed2bc0e29ddb529e..0000000000000000000000000000000000000000 --- a/src/proto_alpha/lib_protocol/script_interpreter_logging.ml +++ /dev/null @@ -1,1839 +0,0 @@ -(*****************************************************************************) -(* *) -(* Open Source License *) -(* Copyright (c) 2022 Nomadic Labs *) -(* *) -(* Permission is hereby granted, free of charge, to any person obtaining a *) -(* copy of this software and associated documentation files (the "Software"),*) -(* to deal in the Software without restriction, including without limitation *) -(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *) -(* and/or sell copies of the Software, and to permit persons to whom the *) -(* Software is furnished to do so, subject to the following conditions: *) -(* *) -(* The above copyright notice and this permission notice shall be included *) -(* in all copies or substantial portions of the Software. *) -(* *) -(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*) -(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *) -(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *) -(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*) -(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *) -(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *) -(* DEALINGS IN THE SOFTWARE. *) -(* *) -(*****************************************************************************) - -open Alpha_context -open Script_typed_ir - -type kinstr_rewritek = { - apply : - 'b 'u 'r 'f. - ('b, 'u) stack_ty -> ('b, 'u, 'r, 'f) kinstr -> ('b, 'u, 'r, 'f) kinstr; -} -[@@ocaml.unboxed] - -(* An existential wrapper around failed [kinstr], whose final stack type - is hidden as it is irrelevant. *) -type ('a, 's) failed_kinstr_cast = {cast : 'b 'u. ('a, 's, 'b, 'u) kinstr} -[@@ocaml.unboxed] - -(* This is a view on a deconstructed [kinstr]. Its type parameters refer to - the type of the viewed [kinstr], while existentials inside describe types of - [kinstr]'s components. The [reconstruct] field in each record stores a - function which reconstructs the original instruction from its components. *) -type ('a, 's, 'r, 'f) ex_split_kinstr = - | Ex_split_kinstr : { - cont_init_stack : ('b, 'u) stack_ty; - continuation : ('b, 'u, 'r, 'f) kinstr; - reconstruct : ('b, 'u, 'r, 'f) kinstr -> ('a, 's, 'r, 'f) kinstr; - } - -> ('a, 's, 'r, 'f) ex_split_kinstr - | Ex_split_log : { - stack : ('a, 's) stack_ty; - continuation : ('a, 's, 'r, 'f) kinstr; - reconstruct : ('a, 's, 'r, 'f) kinstr -> ('a, 's, 'r, 'f) kinstr; - } - -> ('a, 's, 'r, 'f) ex_split_kinstr - | Ex_split_loop_may_fail : { - body_init_stack : ('b, 'u) stack_ty; - body : ('b, 'u, 'r, 'f) kinstr; - cont_init_stack : ('c, 'v) stack_ty; - continuation : ('c, 'v, 't, 'g) kinstr; - reconstruct : - ('b, 'u, 'r, 'f) kinstr -> - ('c, 'v, 't, 'g) kinstr -> - ('a, 's, 't, 'g) kinstr; - } - -> ('a, 's, 't, 'g) ex_split_kinstr - | Ex_split_loop_may_not_fail : { - body_init_stack : ('b, 'u) stack_ty; - body : ('b, 'u, 'r, 'f) kinstr; - continuation : ('c, 'v, 't, 'g) kinstr; - aft_body_stack_transform : - ('r, 'f) stack_ty -> ('c, 'v) stack_ty tzresult; - reconstruct : - ('b, 'u, 'r, 'f) kinstr -> - ('c, 'v, 't, 'g) kinstr -> - ('a, 's, 't, 'g) kinstr; - } - -> ('a, 's, 't, 'g) ex_split_kinstr - | Ex_split_if : { - left_init_stack : ('b, 'u) stack_ty; - left_branch : ('b, 'u, 'r, 'f) kinstr; - right_init_stack : ('c, 'v) stack_ty; - right_branch : ('c, 'v, 'r, 'f) kinstr; - continuation : ('r, 'f, 't, 'g) kinstr; - reconstruct : - ('b, 'u, 'r, 'f) kinstr -> - ('c, 'v, 'r, 'f) kinstr -> - ('r, 'f, 't, 'g) kinstr -> - ('a, 's, 't, 'g) kinstr; - } - -> ('a, 's, 't, 'g) ex_split_kinstr - | Ex_split_halt : Script.location -> ('a, 's, 'a, 's) ex_split_kinstr - | Ex_split_failwith : { - location : Script.location; - arg_ty : ('a, _) ty; - cast : ('a, 's) failed_kinstr_cast; - } - -> ('a, 's, 'r, 'f) ex_split_kinstr - -type ('r, 'f) ex_init_stack_ty = - | Ex_init_stack_ty : - ('a, 's) stack_ty * ('a, 's, 'r, 'f) kinstr - -> ('r, 'f) ex_init_stack_ty - -let rec stack_prefix_preservation_witness_split_input : - type a s b t c u d v. - (b, t, c, u, a, s, d, v) stack_prefix_preservation_witness -> - (a, s) stack_ty -> - (b, t) stack_ty = - fun w s -> - match (w, s) with - | KPrefix (_, _, w), Item_t (_, s) -> - stack_prefix_preservation_witness_split_input w s - | KRest, s -> s - -let rec stack_prefix_preservation_witness_split_output : - type a s b t c u d v. - (b, t, c, u, a, s, d, v) stack_prefix_preservation_witness -> - (c, u) stack_ty -> - (d, v) stack_ty = - fun w s -> - match (w, s) with - | KPrefix (_, a, w), s -> - Item_t (a, stack_prefix_preservation_witness_split_output w s) - | KRest, s -> s - -(* We apply this function to optional type information which must be present - if functions from this module were called. Use with care. *) -let assert_some = function None -> assert false | Some x -> x - -let kinstr_split : - type a s r f. - (a, s) stack_ty -> - (a, s, r, f) kinstr -> - (a, s, r, f) ex_split_kinstr tzresult = - fun s i -> - let dummy = Micheline.dummy_location in - match (i, s) with - | IDrop (loc, k), Item_t (_a, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IDrop (loc, k)); - } - | IDup (loc, k), Item_t (a, s) -> - let s = Item_t (a, Item_t (a, s)) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IDup (loc, k)); - } - | ISwap (loc, k), Item_t (a, Item_t (b, s)) -> - let s = Item_t (b, Item_t (a, s)) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISwap (loc, k)); - } - | IConst (loc, a, x, k), s -> - let s = Item_t (a, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IConst (loc, a, x, k)); - } - | ICons_pair (loc, k), Item_t (a, Item_t (b, s)) -> - pair_t dummy a b >|? fun (Ty_ex_c c) -> - let s = Item_t (c, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ICons_pair (loc, k)); - } - | ICar (loc, k), Item_t (Pair_t (a, _b, _meta, _), s) -> - let s = Item_t (a, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ICar (loc, k)); - } - | ICdr (loc, k), Item_t (Pair_t (_a, b, _meta, _), s) -> - let s = Item_t (b, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ICdr (loc, k)); - } - | IUnpair (loc, k), Item_t (Pair_t (a, b, _meta, _), s) -> - let s = Item_t (a, Item_t (b, s)) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IUnpair (loc, k)); - } - | ICons_some (loc, k), Item_t (a, s) -> - option_t dummy a >|? fun o -> - let s = Item_t (o, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ICons_some (loc, k)); - } - | ICons_none (loc, a, k), s -> - option_t dummy a >|? fun o -> - let s = Item_t (o, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ICons_none (loc, a, k)); - } - | ( IIf_none {loc; branch_if_none; branch_if_some; k}, - Item_t (Option_t (a, _meta, _), s) ) -> - ok - @@ Ex_split_if - { - left_init_stack = s; - left_branch = branch_if_none; - right_init_stack = Item_t (a, s); - right_branch = branch_if_some; - continuation = k; - reconstruct = - (fun branch_if_none branch_if_some k -> - IIf_none {loc; branch_if_none; branch_if_some; k}); - } - | IOpt_map {loc; body; k}, Item_t (Option_t (a, _meta, _), s) -> - ok - @@ Ex_split_loop_may_not_fail - { - body_init_stack = Item_t (a, s); - body; - continuation = k; - aft_body_stack_transform = - (function - | Item_t (b, s) -> option_t dummy b >|? fun o -> Item_t (o, s)); - reconstruct = (fun body k -> IOpt_map {loc; body; k}); - } - | ICons_left (loc, b, k), Item_t (a, s) -> - union_t dummy a b >|? fun (Ty_ex_c c) -> - let s = Item_t (c, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ICons_left (loc, b, k)); - } - | ICons_right (loc, a, k), Item_t (b, s) -> - union_t dummy a b >|? fun (Ty_ex_c c) -> - let s = Item_t (c, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ICons_right (loc, a, k)); - } - | ( IIf_left {loc; branch_if_left; branch_if_right; k}, - Item_t (Union_t (a, b, _meta, _), s) ) -> - ok - @@ Ex_split_if - { - left_init_stack = Item_t (a, s); - left_branch = branch_if_left; - right_init_stack = Item_t (b, s); - right_branch = branch_if_right; - continuation = k; - reconstruct = - (fun branch_if_left branch_if_right k -> - IIf_left {loc; branch_if_left; branch_if_right; k}); - } - | ICons_list (loc, k), Item_t (_a, Item_t (l, s)) -> - let s = Item_t (l, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ICons_list (loc, k)); - } - | INil (loc, a, k), s -> - list_t dummy a >|? fun l -> - let s = Item_t (l, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> INil (loc, a, k)); - } - | ( IIf_cons {loc; branch_if_cons; branch_if_nil; k}, - Item_t ((List_t (a, _meta) as l), s) ) -> - ok - @@ Ex_split_if - { - left_init_stack = Item_t (a, Item_t (l, s)); - left_branch = branch_if_cons; - right_init_stack = s; - right_branch = branch_if_nil; - continuation = k; - reconstruct = - (fun branch_if_cons branch_if_nil k -> - IIf_cons {loc; branch_if_cons; branch_if_nil; k}); - } - | IList_map (loc, body, ty, k), Item_t (List_t (a, _meta), s) -> - let s = Item_t (a, s) in - ok - @@ Ex_split_loop_may_not_fail - { - body_init_stack = s; - body; - continuation = k; - aft_body_stack_transform = - (function - | Item_t (b, s) -> list_t dummy b >|? fun l -> Item_t (l, s)); - reconstruct = (fun body k -> IList_map (loc, body, ty, k)); - } - | IList_iter (loc, ty, body, k), Item_t (List_t (a, _meta), s) -> - ok - @@ Ex_split_loop_may_fail - { - body_init_stack = Item_t (a, s); - body; - cont_init_stack = s; - continuation = k; - reconstruct = (fun body k -> IList_iter (loc, ty, body, k)); - } - | IList_size (loc, k), Item_t (_l, s) -> - let s = Item_t (nat_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IList_size (loc, k)); - } - | IEmpty_set (loc, a, k), s -> - set_t dummy a >|? fun b -> - let s = Item_t (b, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IEmpty_set (loc, a, k)); - } - | ISet_iter (loc, a, body, k), Item_t (_b, s) -> - ok - @@ Ex_split_loop_may_fail - { - body_init_stack = Item_t (assert_some a, s); - body; - cont_init_stack = s; - continuation = k; - reconstruct = (fun body k -> ISet_iter (loc, a, body, k)); - } - | ISet_mem (loc, k), Item_t (_, Item_t (_, s)) -> - let s = Item_t (bool_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISet_mem (loc, k)); - } - | ISet_update (loc, k), Item_t (_, Item_t (_, s)) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISet_update (loc, k)); - } - | ISet_size (loc, k), Item_t (_, s) -> - let s = Item_t (nat_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISet_size (loc, k)); - } - | IEmpty_map (loc, cty, vty, k), s -> - map_t dummy cty (assert_some vty) >|? fun m -> - let s = Item_t (m, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IEmpty_map (loc, cty, vty, k)); - } - | IMap_map (loc, ty, body, k), Item_t (Map_t (kty, vty, _meta), s) -> - let (Map_t (key_ty, _, _)) = assert_some ty in - pair_t dummy key_ty vty >|? fun (Ty_ex_c p) -> - Ex_split_loop_may_not_fail - { - body_init_stack = Item_t (p, s); - body; - continuation = k; - aft_body_stack_transform = - (fun (Item_t (b, s)) -> - map_t dummy kty b >|? fun m -> Item_t (m, s)); - reconstruct = (fun body k -> IMap_map (loc, ty, body, k)); - } - | IMap_iter (loc, kvty, body, k), Item_t (_, stack) -> - ok - @@ Ex_split_loop_may_fail - { - body_init_stack = Item_t (assert_some kvty, stack); - body; - cont_init_stack = stack; - continuation = k; - reconstruct = (fun body k -> IMap_iter (loc, kvty, body, k)); - } - | IMap_mem (loc, k), Item_t (_, Item_t (_, s)) -> - let s = Item_t (bool_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IMap_mem (loc, k)); - } - | IMap_get (loc, k), Item_t (_, Item_t (Map_t (_kty, vty, _meta), s)) -> - option_t dummy vty >|? fun o -> - let s = Item_t (o, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IMap_get (loc, k)); - } - | IMap_update (loc, k), Item_t (_, Item_t (_, s)) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IMap_update (loc, k)); - } - | IMap_get_and_update (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IMap_get_and_update (loc, k)); - } - | IMap_size (loc, k), Item_t (_, s) -> - let s = Item_t (nat_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IMap_size (loc, k)); - } - | IEmpty_big_map (loc, cty, ty, k), s -> - big_map_t dummy cty ty >|? fun b -> - let s = Item_t (b, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IEmpty_big_map (loc, cty, ty, k)); - } - | IBig_map_mem (loc, k), Item_t (_, Item_t (_, s)) -> - let s = Item_t (bool_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IBig_map_mem (loc, k)); - } - | IBig_map_get (loc, k), Item_t (_, Item_t (Big_map_t (_kty, vty, _meta), s)) - -> - option_t dummy vty >|? fun o -> - let s = Item_t (o, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IBig_map_get (loc, k)); - } - | IBig_map_update (loc, k), Item_t (_, Item_t (_, s)) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IBig_map_update (loc, k)); - } - | IBig_map_get_and_update (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IBig_map_get_and_update (loc, k)); - } - | IConcat_string (loc, k), Item_t (_, s) -> - let s = Item_t (string_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IConcat_string (loc, k)); - } - | IConcat_string_pair (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IConcat_string_pair (loc, k)); - } - | ISlice_string (loc, k), Item_t (_, Item_t (_, Item_t (_, s))) -> - let s = Item_t (option_string_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISlice_string (loc, k)); - } - | IString_size (loc, k), Item_t (_, s) -> - let s = Item_t (nat_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IString_size (loc, k)); - } - | IConcat_bytes (loc, k), Item_t (_, s) -> - let s = Item_t (bytes_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IConcat_bytes (loc, k)); - } - | IConcat_bytes_pair (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IConcat_bytes_pair (loc, k)); - } - | ISlice_bytes (loc, k), Item_t (_, Item_t (_, Item_t (_, s))) -> - let s = Item_t (option_bytes_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISlice_bytes (loc, k)); - } - | IBytes_size (loc, k), Item_t (_, s) -> - let s = Item_t (nat_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IBytes_size (loc, k)); - } - | IAdd_seconds_to_timestamp (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IAdd_seconds_to_timestamp (loc, k)); - } - | IAdd_timestamp_to_seconds (loc, k), Item_t (_, Item_t (_, s)) -> - let s = Item_t (timestamp_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IAdd_timestamp_to_seconds (loc, k)); - } - | ISub_timestamp_seconds (loc, k), Item_t (_, Item_t (_, s)) -> - let s = Item_t (timestamp_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISub_timestamp_seconds (loc, k)); - } - | IDiff_timestamps (loc, k), Item_t (_, Item_t (_, s)) -> - let s = Item_t (int_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IDiff_timestamps (loc, k)); - } - | IAdd_tez (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IAdd_tez (loc, k)); - } - | ISub_tez (loc, k), Item_t (_, Item_t (_, s)) -> - let s = Item_t (option_mutez_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISub_tez (loc, k)); - } - | ISub_tez_legacy (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISub_tez_legacy (loc, k)); - } - | IMul_teznat (loc, k), Item_t (_, Item_t (_, s)) -> - let s = Item_t (mutez_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IMul_teznat (loc, k)); - } - | IMul_nattez (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IMul_nattez (loc, k)); - } - | IEdiv_teznat (loc, k), Item_t (_, Item_t (_, s)) -> - let s = Item_t (option_pair_mutez_mutez_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IEdiv_teznat (loc, k)); - } - | IEdiv_tez (loc, k), Item_t (_, Item_t (_, s)) -> - let s = Item_t (option_pair_nat_mutez_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IEdiv_tez (loc, k)); - } - | IOr (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IOr (loc, k)); - } - | IAnd (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IAnd (loc, k)); - } - | IXor (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IXor (loc, k)); - } - | INot (loc, k), s -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> INot (loc, k)); - } - | IIs_nat (loc, k), Item_t (_, s) -> - let s = Item_t (option_nat_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IIs_nat (loc, k)); - } - | INeg (loc, k), Item_t (_, s) -> - let s = Item_t (int_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> INeg (loc, k)); - } - | IAbs_int (loc, k), Item_t (_, s) -> - let s = Item_t (nat_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IAbs_int (loc, k)); - } - | IInt_nat (loc, k), Item_t (_, s) -> - let s = Item_t (int_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IInt_nat (loc, k)); - } - | IAdd_int (loc, k), Item_t (_, Item_t (_, s)) -> - let s = Item_t (int_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IAdd_int (loc, k)); - } - | IAdd_nat (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IAdd_nat (loc, k)); - } - | ISub_int (loc, k), Item_t (_, Item_t (_, s)) -> - let s = Item_t (int_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISub_int (loc, k)); - } - | IMul_int (loc, k), Item_t (_, Item_t (_, s)) -> - let s = Item_t (int_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IMul_int (loc, k)); - } - | IMul_nat (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IMul_nat (loc, k)); - } - | IEdiv_int (loc, k), Item_t (_, Item_t (_, s)) -> - let s = Item_t (option_pair_int_nat_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IEdiv_int (loc, k)); - } - | IEdiv_nat (loc, k), Item_t (_, Item_t (a, s)) -> - pair_t dummy a nat_t >>? fun (Ty_ex_c p) -> - option_t dummy p >|? fun o -> - let s = Item_t (o, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IEdiv_nat (loc, k)); - } - | ILsl_nat (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ILsl_nat (loc, k)); - } - | ILsr_nat (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ILsr_nat (loc, k)); - } - | IOr_nat (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IOr_nat (loc, k)); - } - | IAnd_nat (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IAnd_nat (loc, k)); - } - | IAnd_int_nat (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IAnd_int_nat (loc, k)); - } - | IXor_nat (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IXor_nat (loc, k)); - } - | INot_int (loc, k), Item_t (_, s) -> - let s = Item_t (int_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> INot_int (loc, k)); - } - | IIf {loc; branch_if_true; branch_if_false; k}, Item_t (_, s) -> - ok - @@ Ex_split_if - { - left_init_stack = s; - left_branch = branch_if_true; - right_init_stack = s; - right_branch = branch_if_false; - continuation = k; - reconstruct = - (fun branch_if_true branch_if_false k -> - IIf {loc; branch_if_true; branch_if_false; k}); - } - | ILoop (loc, body, k), Item_t (_, s) -> - ok - @@ Ex_split_loop_may_fail - { - body_init_stack = s; - body; - cont_init_stack = s; - continuation = k; - reconstruct = (fun body k -> ILoop (loc, body, k)); - } - | ILoop_left (loc, kl, kr), Item_t (Union_t (a, b, _meta, _), s) -> - ok - @@ Ex_split_loop_may_fail - { - body_init_stack = Item_t (a, s); - body = kl; - cont_init_stack = Item_t (b, s); - continuation = kr; - reconstruct = (fun kl kr -> ILoop_left (loc, kl, kr)); - } - | IDip (loc, body, ty, k), Item_t (a, s) -> - ok - @@ Ex_split_loop_may_not_fail - { - body_init_stack = s; - body; - continuation = k; - aft_body_stack_transform = (fun s -> ok @@ Item_t (a, s)); - reconstruct = (fun body k -> IDip (loc, body, ty, k)); - } - | IExec (loc, sty, k), Item_t (_, Item_t (Lambda_t (_, b, _meta), s)) -> - let s = Item_t (b, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IExec (loc, sty, k)); - } - | ( IApply (loc, ty, k), - Item_t (_, Item_t (Lambda_t (Pair_t (_, a, _, _), b, _), s)) ) -> - lambda_t dummy a b >|? fun l -> - let s = Item_t (l, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IApply (loc, ty, k)); - } - | ILambda (loc, (Lam (desc, _) as l), k), s -> - let (Item_t (a, Bot_t)) = desc.kbef in - let (Item_t (b, Bot_t)) = desc.kaft in - lambda_t dummy a b >|? fun lam -> - let s = Item_t (lam, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ILambda (loc, l, k)); - } - | ILambda (loc, (LamRec (desc, _) as l), k), s -> - let (Item_t (a, Item_t (Lambda_t _, Bot_t))) = desc.kbef in - let (Item_t (b, Bot_t)) = desc.kaft in - lambda_t dummy a b >|? fun lam -> - let s = Item_t (lam, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ILambda (loc, l, k)); - } - | IFailwith (location, arg_ty), _ -> - ok - @@ Ex_split_failwith - {location; arg_ty; cast = {cast = IFailwith (location, arg_ty)}} - | ICompare (loc, ty, k), Item_t (_, Item_t (_, s)) -> - let s = Item_t (int_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ICompare (loc, ty, k)); - } - | IEq (loc, k), Item_t (_, s) -> - let s = Item_t (bool_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IEq (loc, k)); - } - | INeq (loc, k), Item_t (_, s) -> - let s = Item_t (bool_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> INeq (loc, k)); - } - | ILt (loc, k), Item_t (_, s) -> - let s = Item_t (bool_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ILt (loc, k)); - } - | IGt (loc, k), Item_t (_, s) -> - let s = Item_t (bool_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IGt (loc, k)); - } - | ILe (loc, k), Item_t (_, s) -> - let s = Item_t (bool_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ILe (loc, k)); - } - | IGe (loc, k), Item_t (_, s) -> - let s = Item_t (bool_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IGe (loc, k)); - } - | IAddress (loc, k), Item_t (_, s) -> - let s = Item_t (address_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IAddress (loc, k)); - } - | IContract (loc, ty, code, k), Item_t (_, s) -> - contract_t dummy ty >>? fun c -> - option_t dummy c >|? fun o -> - let s = Item_t (o, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IContract (loc, ty, code, k)); - } - | ITransfer_tokens (loc, k), Item_t (_, Item_t (_, Item_t (_, s))) -> - let s = Item_t (operation_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ITransfer_tokens (loc, k)); - } - | ( IView (loc, (View_signature {output_ty; _} as view_signature), sty, k), - Item_t (_, Item_t (_, s)) ) -> - option_t dummy output_ty >|? fun b -> - let s = Item_t (b, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IView (loc, view_signature, sty, k)); - } - | IImplicit_account (loc, k), Item_t (_, s) -> - let s = Item_t (contract_unit_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IImplicit_account (loc, k)); - } - | ( ICreate_contract {loc; storage_type; code; k}, - Item_t (_, Item_t (_, Item_t (_, s))) ) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = Item_t (operation_t, Item_t (address_t, s)); - continuation = k; - reconstruct = - (fun k -> ICreate_contract {loc; storage_type; code; k}); - } - | ISet_delegate (loc, k), Item_t (_, s) -> - let s = Item_t (operation_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISet_delegate (loc, k)); - } - | INow (loc, k), s -> - let s = Item_t (timestamp_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> INow (loc, k)); - } - | IBalance (loc, k), s -> - let s = Item_t (mutez_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IBalance (loc, k)); - } - | ILevel (loc, k), s -> - let s = Item_t (nat_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ILevel (loc, k)); - } - | ICheck_signature (loc, k), Item_t (_, Item_t (_, Item_t (_, s))) -> - let s = Item_t (bool_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ICheck_signature (loc, k)); - } - | IHash_key (loc, k), Item_t (_, s) -> - let s = Item_t (key_hash_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IHash_key (loc, k)); - } - | IPack (loc, ty, k), Item_t (_, s) -> - let s = Item_t (bytes_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IPack (loc, ty, k)); - } - | IUnpack (loc, ty, k), Item_t (_, s) -> - option_t dummy ty >|? fun o -> - let s = Item_t (o, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IUnpack (loc, ty, k)); - } - | IBlake2b (loc, k), s -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IBlake2b (loc, k)); - } - | ISha256 (loc, k), s -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISha256 (loc, k)); - } - | ISha512 (loc, k), s -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISha512 (loc, k)); - } - | ISource (loc, k), s -> - let s = Item_t (address_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISource (loc, k)); - } - | ISender (loc, k), s -> - let s = Item_t (address_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISender (loc, k)); - } - | ISelf (loc, ty, ep, k), s -> - contract_t dummy ty >|? fun c -> - let s = Item_t (c, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISelf (loc, ty, ep, k)); - } - | ISelf_address (loc, k), s -> - let s = Item_t (address_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISelf_address (loc, k)); - } - | IAmount (loc, k), s -> - let s = Item_t (mutez_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IAmount (loc, k)); - } - | ISapling_empty_state (loc, memo_size, k), s -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = Item_t (sapling_state_t ~memo_size, s); - continuation = k; - reconstruct = (fun k -> ISapling_empty_state (loc, memo_size, k)); - } - | ISapling_verify_update_deprecated (loc, k), Item_t (_, Item_t (state_ty, s)) - -> - pair_t dummy int_t state_ty >>? fun (Ty_ex_c pair_ty) -> - option_t dummy pair_ty >|? fun ty -> - Ex_split_kinstr - { - cont_init_stack = Item_t (ty, s); - continuation = k; - reconstruct = (fun k -> ISapling_verify_update_deprecated (loc, k)); - } - | ISapling_verify_update (loc, k), Item_t (_, Item_t (state_ty, s)) -> - pair_t dummy int_t state_ty >>? fun (Ty_ex_c int_state_ty) -> - pair_t dummy bytes_t int_state_ty >>? fun (Ty_ex_c pair_ty) -> - option_t dummy pair_ty >|? fun ty -> - let s = Item_t (ty, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISapling_verify_update (loc, k)); - } - | IDig (loc, n, p, k), s -> - let (Item_t (b, s)) = stack_prefix_preservation_witness_split_input p s in - let s = stack_prefix_preservation_witness_split_output p s in - let s = Item_t (b, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IDig (loc, n, p, k)); - } - | IDug (loc, n, p, k), Item_t (a, s) -> - let s = stack_prefix_preservation_witness_split_input p s in - let s = Item_t (a, s) in - let s = stack_prefix_preservation_witness_split_output p s in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IDug (loc, n, p, k)); - } - | IDipn (loc, n, p, k1, k2), s -> - ok - @@ Ex_split_loop_may_not_fail - { - body_init_stack = stack_prefix_preservation_witness_split_input p s; - body = k1; - continuation = k2; - aft_body_stack_transform = - (fun s -> - ok @@ stack_prefix_preservation_witness_split_output p s); - reconstruct = (fun k1 k2 -> IDipn (loc, n, p, k1, k2)); - } - | IDropn (loc, n, p, k), s -> - let s = stack_prefix_preservation_witness_split_input p s in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IDropn (loc, n, p, k)); - } - | IChainId (loc, k), s -> - let s = Item_t (chain_id_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IChainId (loc, k)); - } - | INever location, Item_t (arg_ty, _) -> - ok - @@ Ex_split_failwith {location; arg_ty; cast = {cast = INever location}} - | IVoting_power (loc, k), Item_t (_, s) -> - let s = Item_t (nat_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IVoting_power (loc, k)); - } - | ITotal_voting_power (loc, k), s -> - let s = Item_t (nat_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ITotal_voting_power (loc, k)); - } - | IKeccak (loc, k), s -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IKeccak (loc, k)); - } - | ISha3 (loc, k), s -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISha3 (loc, k)); - } - | IAdd_bls12_381_g1 (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IAdd_bls12_381_g1 (loc, k)); - } - | IAdd_bls12_381_g2 (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IAdd_bls12_381_g2 (loc, k)); - } - | IAdd_bls12_381_fr (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IAdd_bls12_381_fr (loc, k)); - } - | IMul_bls12_381_g1 (loc, k), Item_t (g1, Item_t (_, s)) -> - let s = Item_t (g1, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IMul_bls12_381_g1 (loc, k)); - } - | IMul_bls12_381_g2 (loc, k), Item_t (g2, Item_t (_, s)) -> - let s = Item_t (g2, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IMul_bls12_381_g2 (loc, k)); - } - | IMul_bls12_381_fr (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IMul_bls12_381_fr (loc, k)); - } - | IMul_bls12_381_z_fr (loc, k), Item_t (fr, Item_t (_, s)) -> - let s = Item_t (fr, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IMul_bls12_381_z_fr (loc, k)); - } - | IMul_bls12_381_fr_z (loc, k), Item_t (_, s) -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IMul_bls12_381_fr_z (loc, k)); - } - | IInt_bls12_381_fr (loc, k), Item_t (_, s) -> - let s = Item_t (int_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IInt_bls12_381_fr (loc, k)); - } - | INeg_bls12_381_g1 (loc, k), s -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> INeg_bls12_381_g1 (loc, k)); - } - | INeg_bls12_381_g2 (loc, k), s -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> INeg_bls12_381_g2 (loc, k)); - } - | INeg_bls12_381_fr (loc, k), s -> - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> INeg_bls12_381_fr (loc, k)); - } - | IPairing_check_bls12_381 (loc, k), Item_t (_, s) -> - let s = Item_t (bool_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IPairing_check_bls12_381 (loc, k)); - } - | IComb (loc, n, p, k), s -> - let rec aux : - type a b s c d t. - (a, b * s) stack_ty -> - (a, b, s, c, d, t) comb_gadt_witness -> - (c, d * t) stack_ty tzresult = - fun s w -> - match (w, s) with - | Comb_one, s -> ok s - | Comb_succ w, Item_t (a, s) -> - aux s w >>? fun (Item_t (c, t)) -> - pair_t dummy a c >|? fun (Ty_ex_c p) -> Item_t (p, t) - in - aux s p >|? fun s -> - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IComb (loc, n, p, k)); - } - | IUncomb (loc, n, p, k), s -> - let rec aux : - type a b s c d t. - (a, b * s) stack_ty -> - (a, b, s, c, d, t) uncomb_gadt_witness -> - (c, d * t) stack_ty = - fun s w -> - match (w, s) with - | Uncomb_one, s -> s - | Uncomb_succ w, Item_t (Pair_t (a, b, _meta, _), s) -> - let s = aux (Item_t (b, s)) w in - Item_t (a, s) - in - let s = aux s p in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IUncomb (loc, n, p, k)); - } - | IComb_get (loc, n, p, k), Item_t (c, s) -> - let rec aux : - type c cc a. (c, cc) ty -> (c, a) comb_get_gadt_witness -> a ty_ex_c = - fun c w -> - match (w, c) with - | Comb_get_zero, c -> Ty_ex_c c - | Comb_get_one, Pair_t (hd, _tl, _meta, _) -> Ty_ex_c hd - | Comb_get_plus_two w, Pair_t (_hd, tl, _meta, _) -> aux tl w - in - let s = - let (Ty_ex_c ty) = aux c p in - Item_t (ty, s) - in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IComb_get (loc, n, p, k)); - } - | IComb_set (loc, n, p, k), Item_t (a, Item_t (b, s)) -> - let rec aux : - type a b c ca cb. - (a, ca) ty -> - (b, cb) ty -> - (a, b, c) comb_set_gadt_witness -> - c ty_ex_c tzresult = - fun a b w -> - match (w, b) with - | Comb_set_zero, _ -> ok (Ty_ex_c a) - | Comb_set_one, Pair_t (_hd, tl, _meta, _) -> pair_t dummy a tl - | Comb_set_plus_two w, Pair_t (hd, tl, _meta, _) -> - aux a tl w >>? fun (Ty_ex_c c) -> pair_t dummy hd c - in - aux a b p >|? fun (Ty_ex_c c) -> - let s = Item_t (c, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IComb_set (loc, n, p, k)); - } - | IDup_n (loc, n, p, k), s -> - let rec aux : - type a b s t. - (a, b * s) stack_ty -> (a, b, s, t) dup_n_gadt_witness -> t ty_ex_c = - fun s w -> - match (w, s) with - | Dup_n_succ w, Item_t (_, s) -> aux s w - | Dup_n_zero, Item_t (a, _) -> Ty_ex_c a - in - let s = - let (Ty_ex_c ty) = aux s p in - Item_t (ty, s) - in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IDup_n (loc, n, p, k)); - } - | ITicket (loc, cty, k), Item_t (_, Item_t (_, s)) -> - ticket_t dummy (assert_some cty) >>? option_t loc >|? fun t -> - let s = Item_t (t, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ITicket (loc, cty, k)); - } - | ITicket_deprecated (loc, cty, k), Item_t (_, Item_t (_, s)) -> - ticket_t dummy (assert_some cty) >|? fun t -> - let s = Item_t (t, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ITicket_deprecated (loc, cty, k)); - } - | IRead_ticket (loc, a, k), s -> - pair_t dummy (assert_some a) nat_t >>? fun (Ty_ex_c p) -> - pair_t dummy address_t p >|? fun (Ty_ex_c t) -> - let s = Item_t (t, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IRead_ticket (loc, a, k)); - } - | ISplit_ticket (loc, k), Item_t (t, Item_t (_, s)) -> - pair_t dummy t t >>? fun (Ty_ex_c p) -> - option_t dummy p >|? fun o -> - let s = Item_t (o, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> ISplit_ticket (loc, k)); - } - | IJoin_tickets (loc, ty, k), Item_t (Pair_t (t, _t, _meta, _), s) -> - option_t dummy t >|? fun o -> - let s = Item_t (o, s) in - Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IJoin_tickets (loc, ty, k)); - } - | IOpen_chest (loc, k), Item_t (_, Item_t (_, Item_t (_, s))) -> - let s = Item_t (union_bytes_bool_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IOpen_chest (loc, k)); - } - | IMin_block_time (loc, k), s -> - let s = Item_t (nat_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IMin_block_time (loc, k)); - } - | IEmit {loc; ty; unparsed_ty; tag; k}, Item_t (_, s) -> - let s = Item_t (operation_t, s) in - ok - @@ Ex_split_kinstr - { - cont_init_stack = s; - continuation = k; - reconstruct = (fun k -> IEmit {loc; ty; unparsed_ty; tag; k}); - } - | IEmit _, Bot_t -> . - | IHalt loc, _s -> ok @@ Ex_split_halt loc - | ILog (loc, _stack_ty, event, logger, continuation), stack -> - ok - @@ Ex_split_log - { - stack; - continuation; - reconstruct = (fun k -> ILog (loc, s, event, logger, k)); - } - -let rec kinstr_final_stack_type : - type a s r f. - (a, s) stack_ty -> (a, s, r, f) kinstr -> (r, f) stack_ty option tzresult = - fun s i -> - kinstr_split s i >>? function - | Ex_split_kinstr {cont_init_stack; continuation; _} -> - kinstr_final_stack_type cont_init_stack continuation - | Ex_split_log {stack; continuation; _} -> - kinstr_final_stack_type stack continuation - | Ex_split_loop_may_fail {cont_init_stack; continuation; _} -> - kinstr_final_stack_type cont_init_stack continuation - | Ex_split_loop_may_not_fail - {body_init_stack; body; continuation; aft_body_stack_transform; _} -> ( - kinstr_final_stack_type body_init_stack body >>? function - | Some after_body -> - aft_body_stack_transform after_body >>? fun before_k -> - kinstr_final_stack_type before_k continuation - | None -> ok None) - | Ex_split_if - { - left_init_stack; - left_branch; - right_init_stack; - right_branch; - continuation; - _; - } -> ( - kinstr_final_stack_type left_init_stack left_branch >>? function - | Some after_branch_a -> - kinstr_final_stack_type after_branch_a continuation - | None -> ( - kinstr_final_stack_type right_init_stack right_branch >>? function - | Some after_branch_b -> - kinstr_final_stack_type after_branch_b continuation - | None -> ok None)) - | Ex_split_halt _ -> ok @@ Some s - | Ex_split_failwith {cast = {cast = _}; _} -> ok None - -let rec branched_final_stack_type : - type r f. (r, f) ex_init_stack_ty list -> (r, f) stack_ty option tzresult = - function - | [] -> ok None - | Ex_init_stack_ty (init_sty, branch) :: bs -> ( - kinstr_final_stack_type init_sty branch >>? function - | Some _ as sty -> ok sty - | None -> branched_final_stack_type bs) - -let kinstr_rewritek : - type a s r f. - (a, s) stack_ty -> - (a, s, r, f) kinstr -> - kinstr_rewritek -> - (a, s, r, f) kinstr tzresult = - fun s i f -> - kinstr_split s i >>? function - | Ex_split_kinstr {cont_init_stack; continuation; reconstruct} -> - ok @@ reconstruct (f.apply cont_init_stack continuation) - | Ex_split_log {continuation; reconstruct; _} -> - ok @@ reconstruct continuation - | Ex_split_loop_may_fail - {body_init_stack; body; cont_init_stack; continuation; reconstruct} -> - ok - @@ reconstruct - (f.apply body_init_stack body) - (f.apply cont_init_stack continuation) - | Ex_split_loop_may_not_fail - { - body_init_stack; - body; - continuation; - aft_body_stack_transform; - reconstruct; - } -> - (kinstr_final_stack_type body_init_stack body >>? function - | Some after_body -> - aft_body_stack_transform after_body >|? fun before_k -> - f.apply before_k continuation - | None -> ok continuation) - >|? fun k -> reconstruct (f.apply body_init_stack body) k - | Ex_split_if - { - left_init_stack; - left_branch; - right_init_stack; - right_branch; - continuation; - reconstruct; - } -> - (kinstr_final_stack_type left_init_stack left_branch >>? function - | Some after_left_branch -> ok @@ f.apply after_left_branch continuation - | None -> ( - kinstr_final_stack_type right_init_stack right_branch >>? function - | Some after_right_branch -> - ok @@ f.apply after_right_branch continuation - | None -> ok continuation)) - >|? fun k -> - reconstruct - (f.apply left_init_stack left_branch) - (f.apply right_init_stack right_branch) - k - | Ex_split_halt loc -> ok @@ IHalt loc - | Ex_split_failwith {location; arg_ty; _} -> ok @@ IFailwith (location, arg_ty) - -let log_entry logger ctxt gas k sty accu stack = - let ctxt = Local_gas_counter.update_context gas ctxt in - logger.log_entry k ctxt (kinstr_location k) sty (accu, stack) - -let log_exit logger ctxt gas loc_prev k sty accu stack = - let ctxt = Local_gas_counter.update_context gas ctxt in - logger.log_exit k ctxt loc_prev sty (accu, stack) - -let log_control logger ks = logger.log_control ks - -(* [log_kinstr logger i] emits an instruction to instrument the - execution of [i] with [logger]. *) -let log_kinstr logger sty i = ILog (kinstr_location i, sty, LogEntry, logger, i) - -(* [log_next_kinstr logger i] instruments the next instruction of [i] - with the [logger]. - - Notice that the instrumentation breaks the sharing of continuations - that is normally enforced between branches of conditionals. This - has a performance cost. Anyway, the instrumentation allocates many - new [ILog] instructions and [KLog] continuations which makes - the execution of instrumented code significantly slower than - non-instrumented code. "Zero-cost logging" means that the normal - non-instrumented execution is not impacted by the ability to - instrument it, not that the logging itself has no cost. -*) -let log_next_kinstr logger sty i = - let apply sty k = - ILog - ( kinstr_location k, - sty, - LogExit (kinstr_location i), - logger, - log_kinstr logger sty k ) - in - kinstr_rewritek sty i {apply} - -let instrument_cont : - type a b c d. - logger -> - (a, b) stack_ty -> - (a, b, c, d) continuation -> - (a, b, c, d) continuation = - fun logger sty -> function KLog _ as k -> k | k -> KLog (k, sty, logger) - -let log_next_continuation : - type a b c d. - logger -> - (a, b) stack_ty -> - (a, b, c, d) continuation -> - (a, b, c, d) continuation tzresult = - fun logger stack_ty cont -> - let enable_log sty ki = log_kinstr logger sty ki in - match cont with - | KCons (ki, k) -> ( - let ki' = enable_log stack_ty ki in - kinstr_final_stack_type stack_ty ki >|? function - | None -> KCons (ki', k) - | Some sty -> KCons (ki', instrument_cont logger sty k)) - | KLoop_in (ki, k) -> - let (Item_t (Bool_t, sty)) = stack_ty in - ok @@ KLoop_in (enable_log sty ki, instrument_cont logger sty k) - | KReturn (stack, sty, k) -> - let k' = instrument_cont logger (assert_some sty) k in - ok @@ KReturn (stack, sty, k') - | KLoop_in_left (ki, k) -> - let (Item_t (Union_t (a_ty, b_ty, _, _), rest)) = stack_ty in - let ki' = enable_log (Item_t (a_ty, rest)) ki in - let k' = instrument_cont logger (Item_t (b_ty, rest)) k in - ok @@ KLoop_in_left (ki', k') - | KUndip (x, ty, k) -> - let k' = instrument_cont logger (Item_t (assert_some ty, stack_ty)) k in - ok @@ KUndip (x, ty, k') - | KIter (body, xty, xs, k) -> - let body' = enable_log (Item_t (assert_some xty, stack_ty)) body in - let k' = instrument_cont logger stack_ty k in - ok @@ KIter (body', xty, xs, k') - | KList_enter_body (body, xs, ys, ty, len, k) -> - let k' = instrument_cont logger (Item_t (assert_some ty, stack_ty)) k in - ok @@ KList_enter_body (body, xs, ys, ty, len, k') - | KList_exit_body (body, xs, ys, ty, len, k) -> - let (Item_t (_, sty)) = stack_ty in - let k' = instrument_cont logger (Item_t (assert_some ty, sty)) k in - ok @@ KList_exit_body (body, xs, ys, ty, len, k') - | KMap_enter_body (body, xs, ys, ty, k) -> - let k' = instrument_cont logger (Item_t (assert_some ty, stack_ty)) k in - ok @@ KMap_enter_body (body, xs, ys, ty, k') - | KMap_exit_body (body, xs, ys, yk, ty, k) -> - let (Item_t (_, sty)) = stack_ty in - let k' = instrument_cont logger (Item_t (assert_some ty, sty)) k in - ok @@ KMap_exit_body (body, xs, ys, yk, ty, k') - | KMap_head (_, _) - | KView_exit (_, _) - | KLog _ (* This case should never happen. *) | KNil -> - ok cont - -let rec dipn_stack_ty : - type a s e z c u d w. - (a, s, e, z, c, u, d, w) stack_prefix_preservation_witness -> - (c, u) stack_ty -> - (a, s) stack_ty = - fun witness stack -> - match (witness, stack) with - | KPrefix (_, _, witness'), Item_t (_, sty) -> dipn_stack_ty witness' sty - | KRest, sty -> sty diff --git a/src/proto_alpha/lib_protocol/script_interpreter_logging.mli b/src/proto_alpha/lib_protocol/script_interpreter_logging.mli deleted file mode 100644 index f2e26a0cef56efc5bbe4b6bc0805feb28b638cef..0000000000000000000000000000000000000000 --- a/src/proto_alpha/lib_protocol/script_interpreter_logging.mli +++ /dev/null @@ -1,139 +0,0 @@ -(*****************************************************************************) -(* *) -(* Open Source License *) -(* Copyright (c) 2022 Nomadic Labs *) -(* *) -(* Permission is hereby granted, free of charge, to any person obtaining a *) -(* copy of this software and associated documentation files (the "Software"),*) -(* to deal in the Software without restriction, including without limitation *) -(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *) -(* and/or sell copies of the Software, and to permit persons to whom the *) -(* Software is furnished to do so, subject to the following conditions: *) -(* *) -(* The above copyright notice and this permission notice shall be included *) -(* in all copies or substantial portions of the Software. *) -(* *) -(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*) -(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *) -(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *) -(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*) -(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *) -(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *) -(* DEALINGS IN THE SOFTWARE. *) -(* *) -(*****************************************************************************) - -open Script_typed_ir - -(** An existential container for an instruction paired with its - initial stack type. This is used internally to pack together - execution branches with different initial stack types but - the same final stack type (which we want to compute). *) -type ('r, 'f) ex_init_stack_ty = - | Ex_init_stack_ty : - ('a, 's) stack_ty * ('a, 's, 'r, 'f) kinstr - -> ('r, 'f) ex_init_stack_ty - -(** [log_kinstr logger sty instr] returns [instr] prefixed by an - [ILog] instruction to log the first instruction in [instr]. Note - that [logger] value is only available when logging is enables, so - the type system protects us from calling this by mistake. *) -val log_kinstr : - logger -> - ('a, 'b) stack_ty -> - ('a, 'b, 'c, 'd) kinstr -> - ('a, 'b, 'c, 'd) kinstr - -(** [log_entry logger ctxt gas instr sty accu stack] simply calls - [logger.log_entry] function with the appropriate arguments. Note - that [logger] value is only available when logging is enables, so - the type system protects us from calling this by mistake.*) -val log_entry : - logger -> - Local_gas_counter.outdated_context -> - Local_gas_counter.local_gas_counter -> - ('a, 'b, 'c, 'd) kinstr -> - ('a, 'b) stack_ty -> - 'a -> - 'b -> - unit - -(** [log_exit logger ctxt gas loc instr sty accu stack] simply calls - [logger.log_exit] function with the appropriate arguments. Note - that [logger] value is only available when logging is enables, so - the type system protects us from calling this by mistake.*) -val log_exit : - logger -> - Local_gas_counter.outdated_context -> - Local_gas_counter.local_gas_counter -> - Alpha_context.Script.location -> - ('c, 'd, 'e, 'f) kinstr -> - ('g, 'h) stack_ty -> - 'g -> - 'h -> - unit - -(** [log_control logger continuation] simply calls [logger.log_control] - function with the appropriate arguments. Note that [logger] value - is only available when logging is enables, so the type system - protects us from calling this by mistake.*) -val log_control : logger -> ('a, 'b, 'c, 'd) continuation -> unit - -(** [instrument_cont logger sty] creates a function instrumenting - continuations starting from the stack type described by [sty]. - Instrumentation consists in wrapping inner continuations in - [KLog] continuation so that logging continues. *) -val instrument_cont : - logger -> - ('a, 'b) stack_ty -> - ('a, 'b, 'c, 'd) Script_interpreter_defs.cont_instrumentation - -(** [log_next_continuation logger sty cont] instruments the next - continuation in [cont] with [KLog] continuations to ensure - logging. - - This instrumentation has a performance cost, but importantly, it - is only ever paid when logging is enabled. Otherwise, the - possibility to instrument the script is costless. Note also that - [logger] value is only available when logging is enabled, so the - type system protects us from calling this by mistake. *) -val log_next_continuation : - logger -> - ('a, 'b) stack_ty -> - ('a, 'b, 'c, 'd) continuation -> - ('a, 'b, 'c, 'd) continuation tzresult - -(** [log_next_kinstr logger sty instr] instruments the next instruction - in [instr] with [ILog] instructions to make sure it will be logged. - This instrumentation has a performance cost, but importantly, it is - only ever paid when logging is enabled. Otherwise, the possibility - to instrument the script is costless. Note also that [logger] value - is only available when logging is enables, so the type system protects - us from calling this by mistake. *) -val log_next_kinstr : - logger -> - ('a, 'b) stack_ty -> - ('a, 'b, 'c, 'd) kinstr -> - ('a, 'b, 'c, 'd) kinstr tzresult - -(* [kinstr_final_stack_type sty instr] computes the stack type after - [instr] has been executed, assuming [sty] is the type of the stack - prior to execution. *) -val kinstr_final_stack_type : - ('a, 'b) stack_ty -> - ('a, 'b, 'c, 'd) kinstr -> - ('c, 'd) stack_ty option tzresult - -(* The same as [kinstr_final_stack_type], but selects from multiple - possible execution branches. If the first instr ends with FAILWITH, - it will try the next and so on. Note that all instructions must - result in the same stack type. *) -val branched_final_stack_type : - ('r, 'f) ex_init_stack_ty list -> ('r, 'f) stack_ty option tzresult - -(** [dipn_stack_ty witness stack_ty] returns the type of the stack - on which instructions inside dipped block will be operating. *) -val dipn_stack_ty : - ('a, 's, 'e, 'z, 'c, 'u, 'd, 'w) stack_prefix_preservation_witness -> - ('c, 'u) stack_ty -> - ('a, 's) stack_ty diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index 3c75ade275fa976d44a0cb3e8980f10fdfe3729a..e07f1e2914e0161d1feb5371b5ecf7f7c204c7ed 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -1223,12 +1223,54 @@ and execution_trace = (Script.location * Gas.Arith.fp * Script.expr list) list and logger = { log_interp : 'a 's 'b 'f 'c 'u. ('a, 's, 'b, 'f, 'c, 'u) logging_function; - log_entry : 'a 's 'b 'f. ('a, 's, 'b, 'f, 'a, 's) logging_function; - log_control : 'a 's 'b 'f. ('a, 's, 'b, 'f) continuation -> unit; - log_exit : 'a 's 'b 'f 'c 'u. ('a, 's, 'b, 'f, 'c, 'u) logging_function; get_log : unit -> execution_trace option tzresult Lwt.t; + klog : 'a 's 'r 'f. ('a, 's, 'r, 'f) klog; + ilog : 'a 's 'b 't 'r 'f. ('a, 's, 'b, 't, 'r, 'f) ilog; + log_kinstr : 'a 'b 'c 'd. ('a, 'b, 'c, 'd) log_kinstr; } +and ('a, 's, 'r, 'f) klog = + logger -> + Local_gas_counter.outdated_context * step_constants -> + Local_gas_counter.local_gas_counter -> + ('a, 's) stack_ty -> + ('a, 's, 'r, 'f) continuation -> + ('a, 's, 'r, 'f) continuation -> + 'a -> + 's -> + ('r + * 'f + * Local_gas_counter.outdated_context + * Local_gas_counter.local_gas_counter) + tzresult + Lwt.t + +and ('a, 's, 'b, 't, 'r, 'f) ilog = + logger -> + logging_event -> + ('a, 's) stack_ty -> + ('a, 's, 'b, 't, 'r, 'f) step_type + +and ('a, 's, 'b, 't, 'r, 'f) step_type = + Local_gas_counter.outdated_context * step_constants -> + Local_gas_counter.local_gas_counter -> + ('a, 's, 'b, 't) kinstr -> + ('b, 't, 'r, 'f) continuation -> + 'a -> + 's -> + ('r + * 'f + * Local_gas_counter.outdated_context + * Local_gas_counter.local_gas_counter) + tzresult + Lwt.t + +and ('a, 'b, 'c, 'd) log_kinstr = + logger -> + ('a, 'b) stack_ty -> + ('a, 'b, 'c, 'd) kinstr -> + ('a, 'b, 'c, 'd) kinstr + (* ---- Auxiliary types -----------------------------------------------------*) and ('ty, 'comparable) ty = | Unit_t : (unit, yes) ty diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index 874cb08556e870eabbb53d4812086fdaf773914e..7eeca18b1e3b8452af2e5a7b5f606e6abde4d705 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -1331,20 +1331,61 @@ and logger = { (** [log_interp] is called at each call of the internal function [interp]. [interp] is called when starting the interpretation of a script and subsequently at each [Exec] instruction. *) - log_entry : 'a 's 'b 'f. ('a, 's, 'b, 'f, 'a, 's) logging_function; - (** [log_entry] is called {i before} executing each instruction but - {i after} gas for this instruction has been successfully - consumed. *) - log_control : 'a 's 'b 'f. ('a, 's, 'b, 'f) continuation -> unit; - (** [log_control] is called {i before} the interpretation of the - current continuation. *) - log_exit : 'a 's 'b 'f 'c 'u. ('a, 's, 'b, 'f, 'c, 'u) logging_function; - (** [log_exit] is called {i after} executing each instruction. *) get_log : unit -> execution_trace option tzresult Lwt.t; (** [get_log] allows to obtain an execution trace, if any was produced. *) + klog : 'a 's 'r 'f. ('a, 's, 'r, 'f) klog; + (** [klog] is called on [KLog] inserted when instrumenting + continuations. *) + ilog : 'a 's 'b 't 'r 'f. ('a, 's, 'b, 't, 'r, 'f) ilog; + (** [ilog] is called on [ILog] inserted when instrumenting + instructions. *) + log_kinstr : 'a 'b 'c 'd. ('a, 'b, 'c, 'd) log_kinstr; + (** [log_kinstr] instruments an instruction with [ILog]. *) } +and ('a, 's, 'r, 'f) klog = + logger -> + Local_gas_counter.outdated_context * step_constants -> + Local_gas_counter.local_gas_counter -> + ('a, 's) stack_ty -> + ('a, 's, 'r, 'f) continuation -> + ('a, 's, 'r, 'f) continuation -> + 'a -> + 's -> + ('r + * 'f + * Local_gas_counter.outdated_context + * Local_gas_counter.local_gas_counter) + tzresult + Lwt.t + +and ('a, 's, 'b, 't, 'r, 'f) ilog = + logger -> + logging_event -> + ('a, 's) stack_ty -> + ('a, 's, 'b, 't, 'r, 'f) step_type + +and ('a, 's, 'b, 't, 'r, 'f) step_type = + Local_gas_counter.outdated_context * step_constants -> + Local_gas_counter.local_gas_counter -> + ('a, 's, 'b, 't) kinstr -> + ('b, 't, 'r, 'f) continuation -> + 'a -> + 's -> + ('r + * 'f + * Local_gas_counter.outdated_context + * Local_gas_counter.local_gas_counter) + tzresult + Lwt.t + +and ('a, 'b, 'c, 'd) log_kinstr = + logger -> + ('a, 'b) stack_ty -> + ('a, 'b, 'c, 'd) kinstr -> + ('a, 'b, 'c, 'd) kinstr + (* ---- Auxiliary types -----------------------------------------------------*) and ('ty, 'comparable) ty = | Unit_t : (unit, yes) ty diff --git a/src/proto_alpha/lib_protocol/test/integration/michelson/dune b/src/proto_alpha/lib_protocol/test/integration/michelson/dune index 7b2b2a1a6c31e43cd8ad27a2888ae288b965474c..2a07d5576e75c1b2737666cb2c3ff6d3d8b40254 100644 --- a/src/proto_alpha/lib_protocol/test/integration/michelson/dune +++ b/src/proto_alpha/lib_protocol/test/integration/michelson/dune @@ -14,6 +14,7 @@ tezos-micheline tezos-benchmark-alpha tezos-benchmark-type-inference-alpha + tezos-protocol-plugin-alpha tezos-protocol-alpha.parameters) (flags (:standard) @@ -25,7 +26,8 @@ -open Tezos_client_alpha -open Tezos_micheline -open Tezos_benchmark_alpha - -open Tezos_benchmark_type_inference_alpha)) + -open Tezos_benchmark_type_inference_alpha + -open Tezos_protocol_plugin_alpha)) (rule (alias runtest) diff --git a/src/proto_alpha/lib_protocol/test/integration/michelson/test_interpretation.ml b/src/proto_alpha/lib_protocol/test/integration/michelson/test_interpretation.ml index 4a4f86d4e63189918017663f50da3410e744c6ce..302eb4dcac7b63b32233cecea58622860170cc38 100644 --- a/src/proto_alpha/lib_protocol/test/integration/michelson/test_interpretation.ml +++ b/src/proto_alpha/lib_protocol/test/integration/michelson/test_interpretation.ml @@ -42,14 +42,18 @@ let test_context () = return (Incremental.alpha_ctxt v) let logger = - Script_typed_ir. - { - log_interp = (fun _ _ _ _ _ -> ()); - log_entry = (fun _ _ _ _ _ -> ()); - log_exit = (fun _ _ _ _ _ -> ()); - log_control = (fun _ -> ()); - get_log = (fun () -> Lwt.return (Ok None)); - } + Script_interpreter_logging.make + (module struct + let log_interp _ _ _ _ _ = () + + let log_entry _ _ _ _ _ = () + + let log_exit _ _ _ _ _ = () + + let log_control _ = () + + let get_log () = Lwt.return (Ok None) + end) let run_step ctxt code accu stack = let open Script_interpreter in diff --git a/src/proto_alpha/lib_protocol/test/regression/test_logging.ml b/src/proto_alpha/lib_protocol/test/regression/test_logging.ml index 6ab68e63171fca74a5eddab6160729a7a6539f86..a123f6d311ba9499e1c7a13b3a982ad0ec49f446 100644 --- a/src/proto_alpha/lib_protocol/test/regression/test_logging.ml +++ b/src/proto_alpha/lib_protocol/test/regression/test_logging.ml @@ -144,18 +144,24 @@ let logger () : (unit -> trace_element list tzresult Lwt.t) * Script_typed_ir.logger = let open Script_typed_ir in let log : log_element list ref = ref [] in - let log_interp : type a s b f c u. (a, s, b, f, c, u) logging_function = - fun instr ctxt loc sty stack -> - log := With_stack (ctxt, instr, loc, stack, sty, Interp) :: !log - in - let log_entry instr ctxt loc sty stack = - log := With_stack (ctxt, instr, loc, stack, sty, Entry) :: !log - in - let log_exit instr ctxt loc sty stack = - log := With_stack (ctxt, instr, loc, stack, sty, Exit) :: !log + let logger = + Script_interpreter_logging.make + (module struct + let log_interp : type a s b f c u. (a, s, b, f, c, u) logging_function = + fun instr ctxt loc sty stack -> + log := With_stack (ctxt, instr, loc, stack, sty, Interp) :: !log + + let log_entry instr ctxt loc sty stack = + log := With_stack (ctxt, instr, loc, stack, sty, Entry) :: !log + + let log_exit instr ctxt loc sty stack = + log := With_stack (ctxt, instr, loc, stack, sty, Exit) :: !log + + let log_control cont = log := Ctrl cont :: !log + + let get_log () = return_none + end) in - let log_control cont = log := Ctrl cont :: !log in - let get_log () = return_none in let assemble_log () = let open Environment.Error_monad in let+ l = @@ -172,7 +178,7 @@ let logger () : in List.rev l in - (assemble_log, {log_exit; log_entry; log_interp; get_log; log_control}) + (assemble_log, logger) (* [with_logger ~mask f] creates a fresh logger and passes it to [f]. After [f] finishes, logs are gathered and each occurrence of each