Revision 322c73366a9198d5bd6be08e91b729c775761821 authored by Diane Gallois-Wong on 31 August 2022, 15:57:02 UTC, committed by Marge Bot on 06 September 2022, 08:21:04 UTC
Notably, remove plugin tests on 1M, since the plugin is no longer responsible for enforcing 1M. Similar tests on 1M already exist in tezt, and will be extended in the next commit to cover all the cases of the removed tests.
1 parent 995112f
script_typed_ir.mli
(*****************************************************************************)
(* *)
(* Open Source License *)
(* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. <contact@tezos.com> *)
(* Copyright (c) 2020 Metastate AG <hello@metastate.dev> *)
(* Copyright (c) 2021-2022 Nomadic Labs <contact@nomadic-labs.com> *)
(* *)
(* 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_int
open Dependent_bool
type step_constants = {
source : Contract.t;
payer : Contract.t;
self : Contract.t;
amount : Tez.t;
balance : Tez.t;
chain_id : Chain_id.t;
now : Script_timestamp.t;
level : Script_int.n Script_int.num;
}
(* Preliminary definitions. *)
type never = |
type address = {destination : Destination.t; entrypoint : Entrypoint.t}
module Script_signature : sig
(** [t] is made algebraic in order to distinguish it from the other type
parameters of [Script_typed_ir.ty]. *)
type t = Signature_tag of signature [@@ocaml.unboxed]
val make : signature -> t
val get : t -> signature
val encoding : t Data_encoding.t
val of_b58check_opt : string -> t option
val check :
?watermark:Signature.watermark ->
Signature.Public_key.t ->
t ->
Bytes.t ->
bool
val compare : t -> t -> int
val size : int
end
type signature = Script_signature.t
type tx_rollup_l2_address = Tx_rollup_l2_address.Indexable.value
type ('a, 'b) pair = 'a * 'b
type ('a, 'b) union = L of 'a | R of 'b
module Script_chain_id : sig
(** [t] is made algebraic in order to distinguish it from the other type
parameters of [Script_typed_ir.ty]. *)
type t = Chain_id_tag of Chain_id.t [@@ocaml.unboxed]
val make : Chain_id.t -> t
val compare : t -> t -> int
val size : int
val encoding : t Data_encoding.t
val to_b58check : t -> string
val of_b58check_opt : string -> t option
end
module Script_bls : sig
module type S = sig
type t
type fr
val add : t -> t -> t
val mul : t -> fr -> t
val negate : t -> t
val of_bytes_opt : Bytes.t -> t option
val to_bytes : t -> Bytes.t
end
module Fr : sig
(** [t] is made algebraic in order to distinguish it from the other type
parameters of [Script_typed_ir.ty]. *)
type t = Fr_tag of Bls12_381.Fr.t [@@ocaml.unboxed]
include S with type t := t and type fr := t
val of_z : Z.t -> t
val to_z : t -> Z.t
end
module G1 : sig
(** [t] is made algebraic in order to distinguish it from the other type
parameters of [Script_typed_ir.ty]. *)
type t = G1_tag of Bls12_381.G1.t [@@ocaml.unboxed]
include S with type t := t and type fr := Fr.t
end
module G2 : sig
(** [t] is made algebraic in order to distinguish it from the other type
parameters of [Script_typed_ir.ty]. *)
type t = G2_tag of Bls12_381.G2.t [@@ocaml.unboxed]
include S with type t := t and type fr := Fr.t
end
val pairing_check : (G1.t * G2.t) list -> bool
end
module Script_timelock : sig
(** [chest_key] is made algebraic in order to distinguish it from the other
type parameters of [Script_typed_ir.ty]. *)
type chest_key = Chest_key_tag of Timelock.chest_key [@@ocaml.unboxed]
val make_chest_key : Timelock.chest_key -> chest_key
val chest_key_encoding : chest_key Data_encoding.t
(** [chest] is made algebraic in order to distinguish it from the other type
parameters of [Script_typed_ir.ty]. *)
type chest = Chest_tag of Timelock.chest [@@ocaml.unboxed]
val make_chest : Timelock.chest -> chest
val chest_encoding : chest Data_encoding.t
val open_chest : chest -> chest_key -> time:int -> Timelock.opening_result
val get_plaintext_size : chest -> int
end
type 'a ticket = {ticketer : Contract.t; contents : 'a; amount : n num}
type empty_cell = EmptyCell
type end_of_stack = empty_cell * empty_cell
module Type_size : sig
type 'a t
val check_eq :
error_details:'error_trace Script_tc_errors.error_details ->
'a t ->
'b t ->
(unit, 'error_trace) result
val to_int : 'a t -> Saturation_repr.mul_safe Saturation_repr.t
end
type 'a ty_metadata = {size : 'a Type_size.t} [@@unboxed]
module type Boxed_set_OPS = sig
type t
type elt
val elt_size : elt -> int (* Gas_input_size.t *)
val empty : t
val add : elt -> t -> t
val mem : elt -> t -> bool
val remove : elt -> t -> t
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
end
module type Boxed_set = sig
type elt
module OPS : Boxed_set_OPS with type elt = elt
val boxed : OPS.t
val size : int
end
(** [set] is made algebraic in order to distinguish it from the other type
parameters of [ty]. *)
type 'elt set = Set_tag of (module Boxed_set with type elt = 'elt)
[@@ocaml.unboxed]
module type Boxed_map_OPS = sig
type 'a t
type key
val key_size : key -> int (* Gas_input_size.t *)
val empty : 'value t
val add : key -> 'value -> 'value t -> 'value t
val remove : key -> 'value t -> 'value t
val find : key -> 'value t -> 'value option
val fold : (key -> 'value -> 'a -> 'a) -> 'value t -> 'a -> 'a
val fold_es :
(key -> 'value -> 'a -> 'a tzresult Lwt.t) ->
'value t ->
'a ->
'a tzresult Lwt.t
end
module type Boxed_map = sig
type key
type value
module OPS : Boxed_map_OPS with type key = key
val boxed : value OPS.t
val size : int
end
(** [map] is made algebraic in order to distinguish it from the other type
parameters of [ty]. *)
type ('key, 'value) map =
| Map_tag of (module Boxed_map with type key = 'key and type value = 'value)
[@@ocaml.unboxed]
module Big_map_overlay : Map.S with type key = Script_expr_hash.t
type ('key, 'value) big_map_overlay = {
map : ('key * 'value option) Big_map_overlay.t;
size : int;
}
type 'elt boxed_list = {elements : 'elt list; length : int}
type view = {
input_ty : Script.node;
output_ty : Script.node;
view_code : Script.node;
}
type view_map = (Script_string.t, view) map
type entrypoint_info = {name : Entrypoint.t; original_type_expr : Script.node}
(** ['arg entrypoints] represents the tree of entrypoints of a parameter type
['arg].
[at_node] are entrypoint details at that node if it is not [None].
[nested] are the entrypoints below the node in the tree.
It is always [Entrypoints_None] for non-union nodes.
But it is also ok to have [Entrypoints_None] for a union node, it just
means that there are no entrypoints below that node in the tree.
*)
type 'arg entrypoints_node = {
at_node : entrypoint_info option;
nested : 'arg nested_entrypoints;
}
and 'arg nested_entrypoints =
| Entrypoints_Union : {
left : 'l entrypoints_node;
right : 'r entrypoints_node;
}
-> ('l, 'r) union nested_entrypoints
| Entrypoints_None : _ nested_entrypoints
(** [no_entrypoints] is [{at_node = None; nested = Entrypoints_None}] *)
val no_entrypoints : _ entrypoints_node
type 'arg entrypoints = {
root : 'arg entrypoints_node;
original_type_expr : Script.node;
}
type ('arg, 'storage) script =
| Script : {
code :
(('arg, 'storage) pair, (operation boxed_list, 'storage) pair) lambda;
arg_type : ('arg, _) ty;
storage : 'storage;
storage_type : ('storage, _) ty;
views : view_map;
entrypoints : 'arg entrypoints;
code_size : Cache_memory_helpers.sint;
}
-> ('arg, 'storage) script
(* ---- Instructions --------------------------------------------------------*)
(*
The instructions of Michelson are represented in the following
Generalized Algebraic Datatypes.
There are three important aspects in that type declaration.
First, we follow a tagless approach for values: they are directly
represented as OCaml values. This reduces the computational cost of
interpretation because there is no need to check the shape of a
value before applying an operation to it. To achieve that, the GADT
encodes the typing rules of the Michelson programming
language. This static information is sufficient for the typechecker
to justify the absence of runtime checks. As a bonus, it also
ensures that well-typed Michelson programs cannot go wrong: if the
interpreter typechecks then we have the static guarantee that no
stack underflow or type error can occur at runtime.
Second, we maintain the invariant that the stack type always has a
distinguished topmost element. This invariant is important to
implement the stack as an accumulator followed by a linked list of
cells, a so-called A-Stack. This representation is considered in
the literature[1] as an efficient representation of the stack for a
stack-based abstract machine, mainly because this opens the
opportunity for the accumulator to be stored in a hardware
register. In the GADT, this invariant is encoded by representing
the stack type using two parameters instead of one: the first one
is the type of the accumulator while the second is the type of the
rest of the stack.
Third, in this representation, each instruction embeds its
potential successor instructions in the control flow. This design
choice permits an efficient implementation of the continuation
stack in the interpreter. Assigning a precise type to this kind of
instruction which is a cell in a linked list of instructions is
similar to the typing of delimited continuations: we need to give a
type to the stack ['before] the execution of the instruction, a
type to the stack ['after] the execution of the instruction and
before the execution of the next, and a type for the [`result]ing
stack type after the execution of the whole chain of instructions.
Combining these three aspects, the type [kinstr] needs four
parameters:
('before_top, 'before, 'result_top, 'result) kinstr
Notice that we could have chosen to only give two parameters to
[kinstr] by manually enforcing each argument to be a pair but this
is error-prone: with four parameters, this constraint is enforced
by the arity of the type constructor itself.
Hence, an instruction which has a successor instruction enjoys a
type of the form:
... * ('after_top, 'after, 'result_top, 'result) kinstr * ... ->
('before_top, 'before, 'result_top, 'result) kinstr
where ['before_top] and ['before] are the types of the stack top
and rest before the instruction chain, ['after_top] and ['after]
are the types of the stack top and rest after the instruction
chain, and ['result_top] and ['result] are the types of the stack
top and rest after the instruction chain. The [IHalt] instruction
ends a sequence of instructions and has no successor, as shown by
its type:
IHalt : ('a, 's) kinfo -> ('a, 's, 'a, 's) kinstr
Each instruction is decorated by some metadata (typically to hold
locations). The type for these metadata is [kinfo]: such a value is
only used for logging and error reporting and has no impact on the
operational semantics.
Notations:
----------
In the following declaration, we use 'a, 'b, 'c, 'd, ... to assign
types to stack cell contents while we use 's, 't, 'u, 'v, ... to
assign types to stacks.
The types for the final result and stack rest of a whole sequence
of instructions are written 'r and 'f (standing for "result" and
"final stack rest", respectively).
Instructions for internal execution steps
=========================================
Some instructions encoded in the following type are not present in the
source language. They only appear during evaluation to account for
intermediate execution steps. Indeed, since the interpreter follows
a small-step style, it is sometimes necessary to decompose a
source-level instruction (e.g. List_map) into several instructions
with smaller steps. This technique seems required to get an
efficient tail-recursive interpreter.
References
==========
[1]: http://www.complang.tuwien.ac.at/projects/interpreters.html
*)
and ('before_top, 'before, 'result_top, 'result) kinstr =
(*
Stack
-----
*)
| IDrop :
('a, 'b * 's) kinfo * ('b, 's, 'r, 'f) kinstr
-> ('a, 'b * 's, 'r, 'f) kinstr
| IDup :
('a, 's) kinfo * ('a, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| ISwap :
('a, 'b * 's) kinfo * ('b, 'a * 's, 'r, 'f) kinstr
-> ('a, 'b * 's, 'r, 'f) kinstr
| IConst :
('a, 's) kinfo * 'ty * ('ty, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
(*
Pairs
-----
*)
| ICons_pair :
('a, 'b * 's) kinfo * ('a * 'b, 's, 'r, 'f) kinstr
-> ('a, 'b * 's, 'r, 'f) kinstr
| ICar :
('a * 'b, 's) kinfo * ('a, 's, 'r, 'f) kinstr
-> ('a * 'b, 's, 'r, 'f) kinstr
| ICdr :
('a * 'b, 's) kinfo * ('b, 's, 'r, 'f) kinstr
-> ('a * 'b, 's, 'r, 'f) kinstr
| IUnpair :
('a * 'b, 's) kinfo * ('a, 'b * 's, 'r, 'f) kinstr
-> ('a * 'b, 's, 'r, 'f) kinstr
(*
Options
-------
*)
| ICons_some :
('v, 's) kinfo * ('v option, 's, 'r, 'f) kinstr
-> ('v, 's, 'r, 'f) kinstr
| ICons_none :
('a, 's) kinfo * ('b option, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| IIf_none : {
kinfo : ('a option, 'b * 's) kinfo;
branch_if_none : ('b, 's, 'c, 't) kinstr;
branch_if_some : ('a, 'b * 's, 'c, 't) kinstr;
k : ('c, 't, 'r, 'f) kinstr;
}
-> ('a option, 'b * 's, 'r, 'f) kinstr
| IOpt_map : {
kinfo : ('a option, 's) kinfo;
body : ('a, 's, 'b, 's) kinstr;
k : ('b option, 's, 'c, 't) kinstr;
}
-> ('a option, 's, 'c, 't) kinstr
(*
Unions
------
*)
| ICons_left :
('a, 's) kinfo * (('a, 'b) union, 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| ICons_right :
('b, 's) kinfo * (('a, 'b) union, 's, 'r, 'f) kinstr
-> ('b, 's, 'r, 'f) kinstr
| IIf_left : {
kinfo : (('a, 'b) union, 's) kinfo;
branch_if_left : ('a, 's, 'c, 't) kinstr;
branch_if_right : ('b, 's, 'c, 't) kinstr;
k : ('c, 't, 'r, 'f) kinstr;
}
-> (('a, 'b) union, 's, 'r, 'f) kinstr
(*
Lists
-----
*)
| ICons_list :
('a, 'a boxed_list * 's) kinfo * ('a boxed_list, 's, 'r, 'f) kinstr
-> ('a, 'a boxed_list * 's, 'r, 'f) kinstr
| INil :
('a, 's) kinfo * ('b boxed_list, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| IIf_cons : {
kinfo : ('a boxed_list, 'b * 's) kinfo;
branch_if_cons : ('a, 'a boxed_list * ('b * 's), 'c, 't) kinstr;
branch_if_nil : ('b, 's, 'c, 't) kinstr;
k : ('c, 't, 'r, 'f) kinstr;
}
-> ('a boxed_list, 'b * 's, 'r, 'f) kinstr
| IList_map :
('a boxed_list, 'c * 's) kinfo
* ('a, 'c * 's, 'b, 'c * 's) kinstr
* ('b boxed_list, 'c * 's, 'r, 'f) kinstr
-> ('a boxed_list, 'c * 's, 'r, 'f) kinstr
| IList_iter :
('a boxed_list, 'b * 's) kinfo
* ('a, 'b * 's, 'b, 's) kinstr
* ('b, 's, 'r, 'f) kinstr
-> ('a boxed_list, 'b * 's, 'r, 'f) kinstr
| IList_size :
('a boxed_list, 's) kinfo * (n num, 's, 'r, 'f) kinstr
-> ('a boxed_list, 's, 'r, 'f) kinstr
(*
Sets
----
*)
| IEmpty_set :
('a, 's) kinfo * 'b comparable_ty * ('b set, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| ISet_iter :
('a set, 'b * 's) kinfo
* ('a, 'b * 's, 'b, 's) kinstr
* ('b, 's, 'r, 'f) kinstr
-> ('a set, 'b * 's, 'r, 'f) kinstr
| ISet_mem :
('a, 'a set * 's) kinfo * (bool, 's, 'r, 'f) kinstr
-> ('a, 'a set * 's, 'r, 'f) kinstr
| ISet_update :
('a, bool * ('a set * 's)) kinfo * ('a set, 's, 'r, 'f) kinstr
-> ('a, bool * ('a set * 's), 'r, 'f) kinstr
| ISet_size :
('a set, 's) kinfo * (n num, 's, 'r, 'f) kinstr
-> ('a set, 's, 'r, 'f) kinstr
(*
Maps
----
*)
| IEmpty_map :
('a, 's) kinfo * 'b comparable_ty * (('b, 'c) map, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| IMap_map :
(('a, 'b) map, 'd * 's) kinfo
* ('a * 'b, 'd * 's, 'c, 'd * 's) kinstr
* (('a, 'c) map, 'd * 's, 'r, 'f) kinstr
-> (('a, 'b) map, 'd * 's, 'r, 'f) kinstr
| IMap_iter :
(('a, 'b) map, 'c * 's) kinfo
* ('a * 'b, 'c * 's, 'c, 's) kinstr
* ('c, 's, 'r, 'f) kinstr
-> (('a, 'b) map, 'c * 's, 'r, 'f) kinstr
| IMap_mem :
('a, ('a, 'b) map * 's) kinfo * (bool, 's, 'r, 'f) kinstr
-> ('a, ('a, 'b) map * 's, 'r, 'f) kinstr
| IMap_get :
('a, ('a, 'b) map * 's) kinfo * ('b option, 's, 'r, 'f) kinstr
-> ('a, ('a, 'b) map * 's, 'r, 'f) kinstr
| IMap_update :
('a, 'b option * (('a, 'b) map * 's)) kinfo
* (('a, 'b) map, 's, 'r, 'f) kinstr
-> ('a, 'b option * (('a, 'b) map * 's), 'r, 'f) kinstr
| IMap_get_and_update :
('a, 'b option * (('a, 'b) map * 's)) kinfo
* ('b option, ('a, 'b) map * 's, 'r, 'f) kinstr
-> ('a, 'b option * (('a, 'b) map * 's), 'r, 'f) kinstr
| IMap_size :
(('a, 'b) map, 's) kinfo * (n num, 's, 'r, 'f) kinstr
-> (('a, 'b) map, 's, 'r, 'f) kinstr
(*
Big maps
--------
*)
| IEmpty_big_map :
('a, 's) kinfo
* 'b comparable_ty
* ('c, _) ty
* (('b, 'c) big_map, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| IBig_map_mem :
('a, ('a, 'b) big_map * 's) kinfo * (bool, 's, 'r, 'f) kinstr
-> ('a, ('a, 'b) big_map * 's, 'r, 'f) kinstr
| IBig_map_get :
('a, ('a, 'b) big_map * 's) kinfo * ('b option, 's, 'r, 'f) kinstr
-> ('a, ('a, 'b) big_map * 's, 'r, 'f) kinstr
| IBig_map_update :
('a, 'b option * (('a, 'b) big_map * 's)) kinfo
* (('a, 'b) big_map, 's, 'r, 'f) kinstr
-> ('a, 'b option * (('a, 'b) big_map * 's), 'r, 'f) kinstr
| IBig_map_get_and_update :
('a, 'b option * (('a, 'b) big_map * 's)) kinfo
* ('b option, ('a, 'b) big_map * 's, 'r, 'f) kinstr
-> ('a, 'b option * (('a, 'b) big_map * 's), 'r, 'f) kinstr
(*
Strings
-------
*)
| IConcat_string :
(Script_string.t boxed_list, 's) kinfo
* (Script_string.t, 's, 'r, 'f) kinstr
-> (Script_string.t boxed_list, 's, 'r, 'f) kinstr
| IConcat_string_pair :
(Script_string.t, Script_string.t * 's) kinfo
* (Script_string.t, 's, 'r, 'f) kinstr
-> (Script_string.t, Script_string.t * 's, 'r, 'f) kinstr
| ISlice_string :
(n num, n num * (Script_string.t * 's)) kinfo
* (Script_string.t option, 's, 'r, 'f) kinstr
-> (n num, n num * (Script_string.t * 's), 'r, 'f) kinstr
| IString_size :
(Script_string.t, 's) kinfo * (n num, 's, 'r, 'f) kinstr
-> (Script_string.t, 's, 'r, 'f) kinstr
(*
Bytes
-----
*)
| IConcat_bytes :
(bytes boxed_list, 's) kinfo * (bytes, 's, 'r, 'f) kinstr
-> (bytes boxed_list, 's, 'r, 'f) kinstr
| IConcat_bytes_pair :
(bytes, bytes * 's) kinfo * (bytes, 's, 'r, 'f) kinstr
-> (bytes, bytes * 's, 'r, 'f) kinstr
| ISlice_bytes :
(n num, n num * (bytes * 's)) kinfo * (bytes option, 's, 'r, 'f) kinstr
-> (n num, n num * (bytes * 's), 'r, 'f) kinstr
| IBytes_size :
(bytes, 's) kinfo * (n num, 's, 'r, 'f) kinstr
-> (bytes, 's, 'r, 'f) kinstr
(*
Timestamps
----------
*)
| IAdd_seconds_to_timestamp :
(z num, Script_timestamp.t * 's) kinfo
* (Script_timestamp.t, 's, 'r, 'f) kinstr
-> (z num, Script_timestamp.t * 's, 'r, 'f) kinstr
| IAdd_timestamp_to_seconds :
(Script_timestamp.t, z num * 's) kinfo
* (Script_timestamp.t, 's, 'r, 'f) kinstr
-> (Script_timestamp.t, z num * 's, 'r, 'f) kinstr
| ISub_timestamp_seconds :
(Script_timestamp.t, z num * 's) kinfo
* (Script_timestamp.t, 's, 'r, 'f) kinstr
-> (Script_timestamp.t, z num * 's, 'r, 'f) kinstr
| IDiff_timestamps :
(Script_timestamp.t, Script_timestamp.t * 's) kinfo
* (z num, 's, 'r, 'f) kinstr
-> (Script_timestamp.t, Script_timestamp.t * 's, 'r, 'f) kinstr
(*
Tez
---
*)
| IAdd_tez :
(Tez.t, Tez.t * 's) kinfo * (Tez.t, 's, 'r, 'f) kinstr
-> (Tez.t, Tez.t * 's, 'r, 'f) kinstr
| ISub_tez :
(Tez.t, Tez.t * 's) kinfo * (Tez.t option, 's, 'r, 'f) kinstr
-> (Tez.t, Tez.t * 's, 'r, 'f) kinstr
| ISub_tez_legacy :
(Tez.t, Tez.t * 's) kinfo * (Tez.t, 's, 'r, 'f) kinstr
-> (Tez.t, Tez.t * 's, 'r, 'f) kinstr
| IMul_teznat :
(Tez.t, n num * 's) kinfo * (Tez.t, 's, 'r, 'f) kinstr
-> (Tez.t, n num * 's, 'r, 'f) kinstr
| IMul_nattez :
(n num, Tez.t * 's) kinfo * (Tez.t, 's, 'r, 'f) kinstr
-> (n num, Tez.t * 's, 'r, 'f) kinstr
| IEdiv_teznat :
(Tez.t, n num * 's) kinfo
* ((Tez.t, Tez.t) pair option, 's, 'r, 'f) kinstr
-> (Tez.t, n num * 's, 'r, 'f) kinstr
| IEdiv_tez :
(Tez.t, Tez.t * 's) kinfo
* ((n num, Tez.t) pair option, 's, 'r, 'f) kinstr
-> (Tez.t, Tez.t * 's, 'r, 'f) kinstr
(*
Booleans
--------
*)
| IOr :
(bool, bool * 's) kinfo * (bool, 's, 'r, 'f) kinstr
-> (bool, bool * 's, 'r, 'f) kinstr
| IAnd :
(bool, bool * 's) kinfo * (bool, 's, 'r, 'f) kinstr
-> (bool, bool * 's, 'r, 'f) kinstr
| IXor :
(bool, bool * 's) kinfo * (bool, 's, 'r, 'f) kinstr
-> (bool, bool * 's, 'r, 'f) kinstr
| INot :
(bool, 's) kinfo * (bool, 's, 'r, 'f) kinstr
-> (bool, 's, 'r, 'f) kinstr
(*
Integers
--------
*)
| IIs_nat :
(z num, 's) kinfo * (n num option, 's, 'r, 'f) kinstr
-> (z num, 's, 'r, 'f) kinstr
| INeg :
('a num, 's) kinfo * (z num, 's, 'r, 'f) kinstr
-> ('a num, 's, 'r, 'f) kinstr
| IAbs_int :
(z num, 's) kinfo * (n num, 's, 'r, 'f) kinstr
-> (z num, 's, 'r, 'f) kinstr
| IInt_nat :
(n num, 's) kinfo * (z num, 's, 'r, 'f) kinstr
-> (n num, 's, 'r, 'f) kinstr
| IAdd_int :
('a num, 'b num * 's) kinfo * (z num, 's, 'r, 'f) kinstr
-> ('a num, 'b num * 's, 'r, 'f) kinstr
| IAdd_nat :
(n num, n num * 's) kinfo * (n num, 's, 'r, 'f) kinstr
-> (n num, n num * 's, 'r, 'f) kinstr
| ISub_int :
('a num, 'b num * 's) kinfo * (z num, 's, 'r, 'f) kinstr
-> ('a num, 'b num * 's, 'r, 'f) kinstr
| IMul_int :
('a num, 'b num * 's) kinfo * (z num, 's, 'r, 'f) kinstr
-> ('a num, 'b num * 's, 'r, 'f) kinstr
| IMul_nat :
(n num, 'a num * 's) kinfo * ('a num, 's, 'r, 'f) kinstr
-> (n num, 'a num * 's, 'r, 'f) kinstr
| IEdiv_int :
('a num, 'b num * 's) kinfo
* ((z num, n num) pair option, 's, 'r, 'f) kinstr
-> ('a num, 'b num * 's, 'r, 'f) kinstr
| IEdiv_nat :
(n num, 'a num * 's) kinfo
* (('a num, n num) pair option, 's, 'r, 'f) kinstr
-> (n num, 'a num * 's, 'r, 'f) kinstr
| ILsl_nat :
(n num, n num * 's) kinfo * (n num, 's, 'r, 'f) kinstr
-> (n num, n num * 's, 'r, 'f) kinstr
| ILsr_nat :
(n num, n num * 's) kinfo * (n num, 's, 'r, 'f) kinstr
-> (n num, n num * 's, 'r, 'f) kinstr
| IOr_nat :
(n num, n num * 's) kinfo * (n num, 's, 'r, 'f) kinstr
-> (n num, n num * 's, 'r, 'f) kinstr
| IAnd_nat :
(n num, n num * 's) kinfo * (n num, 's, 'r, 'f) kinstr
-> (n num, n num * 's, 'r, 'f) kinstr
| IAnd_int_nat :
(z num, n num * 's) kinfo * (n num, 's, 'r, 'f) kinstr
-> (z num, n num * 's, 'r, 'f) kinstr
| IXor_nat :
(n num, n num * 's) kinfo * (n num, 's, 'r, 'f) kinstr
-> (n num, n num * 's, 'r, 'f) kinstr
| INot_int :
('a num, 's) kinfo * (z num, 's, 'r, 'f) kinstr
-> ('a num, 's, 'r, 'f) kinstr
(*
Control
-------
*)
| IIf : {
kinfo : (bool, 'a * 's) kinfo;
branch_if_true : ('a, 's, 'b, 'u) kinstr;
branch_if_false : ('a, 's, 'b, 'u) kinstr;
k : ('b, 'u, 'r, 'f) kinstr;
}
-> (bool, 'a * 's, 'r, 'f) kinstr
| ILoop :
(bool, 'a * 's) kinfo
* ('a, 's, bool, 'a * 's) kinstr
* ('a, 's, 'r, 'f) kinstr
-> (bool, 'a * 's, 'r, 'f) kinstr
| ILoop_left :
(('a, 'b) union, 's) kinfo
* ('a, 's, ('a, 'b) union, 's) kinstr
* ('b, 's, 'r, 'f) kinstr
-> (('a, 'b) union, 's, 'r, 'f) kinstr
| IDip :
('a, 'b * 's) kinfo
* ('b, 's, 'c, 't) kinstr
* ('a, 'c * 't, 'r, 'f) kinstr
-> ('a, 'b * 's, 'r, 'f) kinstr
| IExec :
('a, ('a, 'b) lambda * 's) kinfo * ('b, 's, 'r, 'f) kinstr
-> ('a, ('a, 'b) lambda * 's, 'r, 'f) kinstr
| IApply :
('a, ('a * 'b, 'c) lambda * 's) kinfo
* ('a, _) ty
* (('b, 'c) lambda, 's, 'r, 'f) kinstr
-> ('a, ('a * 'b, 'c) lambda * 's, 'r, 'f) kinstr
| ILambda :
('a, 's) kinfo
* ('b, 'c) lambda
* (('b, 'c) lambda, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| IFailwith :
('a, 's) kinfo * Script.location * ('a, _) ty
-> ('a, 's, 'r, 'f) kinstr
(*
Comparison
----------
*)
| ICompare :
('a, 'a * 's) kinfo * 'a comparable_ty * (z num, 's, 'r, 'f) kinstr
-> ('a, 'a * 's, 'r, 'f) kinstr
(*
Comparators
-----------
*)
| IEq :
(z num, 's) kinfo * (bool, 's, 'r, 'f) kinstr
-> (z num, 's, 'r, 'f) kinstr
| INeq :
(z num, 's) kinfo * (bool, 's, 'r, 'f) kinstr
-> (z num, 's, 'r, 'f) kinstr
| ILt :
(z num, 's) kinfo * (bool, 's, 'r, 'f) kinstr
-> (z num, 's, 'r, 'f) kinstr
| IGt :
(z num, 's) kinfo * (bool, 's, 'r, 'f) kinstr
-> (z num, 's, 'r, 'f) kinstr
| ILe :
(z num, 's) kinfo * (bool, 's, 'r, 'f) kinstr
-> (z num, 's, 'r, 'f) kinstr
| IGe :
(z num, 's) kinfo * (bool, 's, 'r, 'f) kinstr
-> (z num, 's, 'r, 'f) kinstr
(*
Protocol
--------
*)
| IAddress :
('a typed_contract, 's) kinfo * (address, 's, 'r, 'f) kinstr
-> ('a typed_contract, 's, 'r, 'f) kinstr
| IContract :
(address, 's) kinfo
* ('a, _) ty
* Entrypoint.t
* ('a typed_contract option, 's, 'r, 'f) kinstr
-> (address, 's, 'r, 'f) kinstr
| IView :
('a, address * 's) kinfo
* ('a, 'b) view_signature
* ('b option, 's, 'r, 'f) kinstr
-> ('a, address * 's, 'r, 'f) kinstr
| ITransfer_tokens :
('a, Tez.t * ('a typed_contract * 's)) kinfo
* (operation, 's, 'r, 'f) kinstr
-> ('a, Tez.t * ('a typed_contract * 's), 'r, 'f) kinstr
| IImplicit_account :
(public_key_hash, 's) kinfo * (unit typed_contract, 's, 'r, 'f) kinstr
-> (public_key_hash, 's, 'r, 'f) kinstr
| ICreate_contract : {
kinfo : (public_key_hash option, Tez.t * ('a * 's)) kinfo;
storage_type : ('a, _) ty;
code : Script.expr;
k : (operation, address * 's, 'r, 'f) kinstr;
}
-> (public_key_hash option, Tez.t * ('a * 's), 'r, 'f) kinstr
| ISet_delegate :
(public_key_hash option, 's) kinfo * (operation, 's, 'r, 'f) kinstr
-> (public_key_hash option, 's, 'r, 'f) kinstr
| INow :
('a, 's) kinfo * (Script_timestamp.t, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| IMin_block_time :
('a, 's) kinfo * (n num, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| IBalance :
('a, 's) kinfo * (Tez.t, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| ILevel :
('a, 's) kinfo * (n num, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| ICheck_signature :
(public_key, signature * (bytes * 's)) kinfo * (bool, 's, 'r, 'f) kinstr
-> (public_key, signature * (bytes * 's), 'r, 'f) kinstr
| IHash_key :
(public_key, 's) kinfo * (public_key_hash, 's, 'r, 'f) kinstr
-> (public_key, 's, 'r, 'f) kinstr
| IPack :
('a, 's) kinfo * ('a, _) ty * (bytes, 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| IUnpack :
(bytes, 's) kinfo * ('a, _) ty * ('a option, 's, 'r, 'f) kinstr
-> (bytes, 's, 'r, 'f) kinstr
| IBlake2b :
(bytes, 's) kinfo * (bytes, 's, 'r, 'f) kinstr
-> (bytes, 's, 'r, 'f) kinstr
| ISha256 :
(bytes, 's) kinfo * (bytes, 's, 'r, 'f) kinstr
-> (bytes, 's, 'r, 'f) kinstr
| ISha512 :
(bytes, 's) kinfo * (bytes, 's, 'r, 'f) kinstr
-> (bytes, 's, 'r, 'f) kinstr
| ISource :
('a, 's) kinfo * (address, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| ISender :
('a, 's) kinfo * (address, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| ISelf :
('a, 's) kinfo
* ('b, _) ty
* Entrypoint.t
* ('b typed_contract, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| ISelf_address :
('a, 's) kinfo * (address, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| IAmount :
('a, 's) kinfo * (Tez.t, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| ISapling_empty_state :
('a, 's) kinfo
* Sapling.Memo_size.t
* (Sapling.state, 'a * 's, 'b, 'f) kinstr
-> ('a, 's, 'b, 'f) kinstr
| ISapling_verify_update :
(Sapling.transaction, Sapling.state * 's) kinfo
* ((bytes, (z num, Sapling.state) pair) pair option, 's, 'r, 'f) kinstr
-> (Sapling.transaction, Sapling.state * 's, 'r, 'f) kinstr
| ISapling_verify_update_deprecated :
(* legacy introduced in J *)
(Sapling.Legacy.transaction, Sapling.state * 's) kinfo
* ((z num, Sapling.state) pair option, 's, 'r, 'f) kinstr
-> (Sapling.Legacy.transaction, Sapling.state * 's, 'r, 'f) kinstr
| IDig :
('a, 's) kinfo
(*
There is a prefix of length [n] common to the input stack
of type ['a * 's] and an intermediary stack of type ['d * 'u].
*)
* int
(*
Under this common prefix, the input stack has type ['b * 'c * 't] and
the intermediary stack type ['c * 't] because we removed the ['b] from
the input stack. This value of type ['b] is pushed on top of the
stack passed to the continuation.
*)
* ('b, 'c * 't, 'c, 't, 'a, 's, 'd, 'u) stack_prefix_preservation_witness
* ('b, 'd * 'u, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| IDug :
('a, 'b * 's) kinfo
(*
The input stack has type ['a * 'b * 's].
There is a prefix of length [n] common to its substack
of type ['b * 's] and the output stack of type ['d * 'u].
*)
* int
(*
Under this common prefix, the first stack has type ['c * 't]
and the second has type ['a * 'c * 't] because we have pushed
the topmost element of this input stack under the common prefix.
*)
* ('c, 't, 'a, 'c * 't, 'b, 's, 'd, 'u) stack_prefix_preservation_witness
* ('d, 'u, 'r, 'f) kinstr
-> ('a, 'b * 's, 'r, 'f) kinstr
| IDipn :
('a, 's) kinfo
(*
The body of Dipn is applied under a prefix of size [n]...
*)
* int
(*
... the relation between the types of the input and output stacks
is characterized by the following witness.
(See forthcoming comments about [stack_prefix_preservation_witness].)
*)
* ('c, 't, 'd, 'v, 'a, 's, 'b, 'u) stack_prefix_preservation_witness
* ('c, 't, 'd, 'v) kinstr
* ('b, 'u, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| IDropn :
('a, 's) kinfo
(*
The input stack enjoys a prefix of length [n]...
*)
* int
(*
... and the following value witnesses that under this prefix
the stack has type ['b * 'u].
*)
* ('b, 'u, 'b, 'u, 'a, 's, 'a, 's) stack_prefix_preservation_witness
(*
This stack is passed to the continuation since we drop the
entire prefix.
*)
* ('b, 'u, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| IChainId :
('a, 's) kinfo * (Script_chain_id.t, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| INever : (never, 's) kinfo -> (never, 's, 'r, 'f) kinstr
| IVoting_power :
(public_key_hash, 's) kinfo * (n num, 's, 'r, 'f) kinstr
-> (public_key_hash, 's, 'r, 'f) kinstr
| ITotal_voting_power :
('a, 's) kinfo * (n num, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| IKeccak :
(bytes, 's) kinfo * (bytes, 's, 'r, 'f) kinstr
-> (bytes, 's, 'r, 'f) kinstr
| ISha3 :
(bytes, 's) kinfo * (bytes, 's, 'r, 'f) kinstr
-> (bytes, 's, 'r, 'f) kinstr
| IAdd_bls12_381_g1 :
(Script_bls.G1.t, Script_bls.G1.t * 's) kinfo
* (Script_bls.G1.t, 's, 'r, 'f) kinstr
-> (Script_bls.G1.t, Script_bls.G1.t * 's, 'r, 'f) kinstr
| IAdd_bls12_381_g2 :
(Script_bls.G2.t, Script_bls.G2.t * 's) kinfo
* (Script_bls.G2.t, 's, 'r, 'f) kinstr
-> (Script_bls.G2.t, Script_bls.G2.t * 's, 'r, 'f) kinstr
| IAdd_bls12_381_fr :
(Script_bls.Fr.t, Script_bls.Fr.t * 's) kinfo
* (Script_bls.Fr.t, 's, 'r, 'f) kinstr
-> (Script_bls.Fr.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr
| IMul_bls12_381_g1 :
(Script_bls.G1.t, Script_bls.Fr.t * 's) kinfo
* (Script_bls.G1.t, 's, 'r, 'f) kinstr
-> (Script_bls.G1.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr
| IMul_bls12_381_g2 :
(Script_bls.G2.t, Script_bls.Fr.t * 's) kinfo
* (Script_bls.G2.t, 's, 'r, 'f) kinstr
-> (Script_bls.G2.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr
| IMul_bls12_381_fr :
(Script_bls.Fr.t, Script_bls.Fr.t * 's) kinfo
* (Script_bls.Fr.t, 's, 'r, 'f) kinstr
-> (Script_bls.Fr.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr
| IMul_bls12_381_z_fr :
(Script_bls.Fr.t, 'a num * 's) kinfo
* (Script_bls.Fr.t, 's, 'r, 'f) kinstr
-> (Script_bls.Fr.t, 'a num * 's, 'r, 'f) kinstr
| IMul_bls12_381_fr_z :
('a num, Script_bls.Fr.t * 's) kinfo
* (Script_bls.Fr.t, 's, 'r, 'f) kinstr
-> ('a num, Script_bls.Fr.t * 's, 'r, 'f) kinstr
| IInt_bls12_381_fr :
(Script_bls.Fr.t, 's) kinfo * (z num, 's, 'r, 'f) kinstr
-> (Script_bls.Fr.t, 's, 'r, 'f) kinstr
| INeg_bls12_381_g1 :
(Script_bls.G1.t, 's) kinfo * (Script_bls.G1.t, 's, 'r, 'f) kinstr
-> (Script_bls.G1.t, 's, 'r, 'f) kinstr
| INeg_bls12_381_g2 :
(Script_bls.G2.t, 's) kinfo * (Script_bls.G2.t, 's, 'r, 'f) kinstr
-> (Script_bls.G2.t, 's, 'r, 'f) kinstr
| INeg_bls12_381_fr :
(Script_bls.Fr.t, 's) kinfo * (Script_bls.Fr.t, 's, 'r, 'f) kinstr
-> (Script_bls.Fr.t, 's, 'r, 'f) kinstr
| IPairing_check_bls12_381 :
((Script_bls.G1.t, Script_bls.G2.t) pair boxed_list, 's) kinfo
* (bool, 's, 'r, 'f) kinstr
-> ((Script_bls.G1.t, Script_bls.G2.t) pair boxed_list, 's, 'r, 'f) kinstr
| IComb :
('a, 's) kinfo
* int
* ('a * 's, 'b * 'u) comb_gadt_witness
* ('b, 'u, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| IUncomb :
('a, 's) kinfo
* int
* ('a * 's, 'b * 'u) uncomb_gadt_witness
* ('b, 'u, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| IComb_get :
('t, 's) kinfo
* int
* ('t, 'v) comb_get_gadt_witness
* ('v, 's, 'r, 'f) kinstr
-> ('t, 's, 'r, 'f) kinstr
| IComb_set :
('a, 'b * 's) kinfo
* int
* ('a, 'b, 'c) comb_set_gadt_witness
* ('c, 's, 'r, 'f) kinstr
-> ('a, 'b * 's, 'r, 'f) kinstr
| IDup_n :
('a, 's) kinfo
* int
* ('a * 's, 't) dup_n_gadt_witness
* ('t, 'a * 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
| ITicket :
('a, n num * 's) kinfo * ('a ticket, 's, 'r, 'f) kinstr
-> ('a, n num * 's, 'r, 'f) kinstr
| IRead_ticket :
('a ticket, 's) kinfo
* (address * ('a * n num), 'a ticket * 's, 'r, 'f) kinstr
-> ('a ticket, 's, 'r, 'f) kinstr
| ISplit_ticket :
('a ticket, (n num * n num) * 's) kinfo
* (('a ticket * 'a ticket) option, 's, 'r, 'f) kinstr
-> ('a ticket, (n num * n num) * 's, 'r, 'f) kinstr
| IJoin_tickets :
('a ticket * 'a ticket, 's) kinfo
* 'a comparable_ty
* ('a ticket option, 's, 'r, 'f) kinstr
-> ('a ticket * 'a ticket, 's, 'r, 'f) kinstr
| IOpen_chest :
(Script_timelock.chest_key, Script_timelock.chest * (n num * 's)) kinfo
* ((bytes, bool) union, 's, 'r, 'f) kinstr
-> ( Script_timelock.chest_key,
Script_timelock.chest * (n num * 's),
'r,
'f )
kinstr
(*
Internal control instructions
=============================
The following instructions are not available in the source language.
They are used by the internals of the interpreter.
*)
| IHalt : ('a, 's) kinfo -> ('a, 's, 'a, 's) kinstr
| ILog :
('a, 's) kinfo * logging_event * logger * ('a, 's, 'r, 'f) kinstr
-> ('a, 's, 'r, 'f) kinstr
and logging_event =
| LogEntry : logging_event
| LogExit : ('b, 'u) kinfo -> logging_event
and ('arg, 'ret) lambda =
| Lam :
('arg, end_of_stack, 'ret, end_of_stack) kdescr * Script.node
-> ('arg, 'ret) lambda
[@@coq_force_gadt]
and 'arg typed_contract =
| Typed_contract : {
arg_ty : ('arg, _) ty;
address : address;
}
-> 'arg typed_contract
(*
Control stack
=============
The control stack is a list of [kinstr].
Since [kinstr] denotes a list of instructions, the control stack
can be seen as a list of instruction sequences, each representing a
form of delimited continuation (i.e. a control stack fragment). The
[continuation] GADT ensures that the input and output stack types of the
continuations are consistent.
Loops have a special treatment because their control stack is reused
as is for the next iteration. This avoids the reallocation of a
control stack cell at each iteration.
To implement [step] as a tail-recursive function, we implement
higher-order iterators (i.e. MAPs and ITERs) using internal instructions
. Roughly speaking, these instructions help in decomposing the execution
of [I f c] (where [I] is an higher-order iterator over a container [c])
into three phases: to start the iteration, to execute [f] if there are
elements to be processed in [c], and to loop.
Dip also has a dedicated constructor in the control stack. This
allows the stack prefix to be restored after the execution of the
[Dip]'s body.
Following the same style as in [kinstr], [continuation] has four
arguments, two for each stack types. More precisely, with
[('bef_top, 'bef, 'aft_top, 'aft) continuation]
we encode the fact that the stack before executing the continuation
has type [('bef_top * 'bef)] and that the stack after this execution
has type [('aft_top * 'aft)].
*)
and (_, _, _, _) continuation =
(* This continuation returns immediately. *)
| KNil : ('r, 'f, 'r, 'f) continuation
(* This continuation starts with the next instruction to execute. *)
| KCons :
('a, 's, 'b, 't) kinstr * ('b, 't, 'r, 'f) continuation
-> ('a, 's, 'r, 'f) continuation
(* This continuation represents a call frame: it stores the caller's
stack of type ['s] and the continuation which expects the callee's
result on top of the stack. *)
| KReturn :
's * ('a, 's, 'r, 'f) continuation
-> ('a, end_of_stack, 'r, 'f) continuation
(* This continuation is useful when stack head requires some wrapping or
unwrapping before it can be passed forward. For instance this continuation
is used after a [MAP] instruction applied to an option in order to wrap the
result back in a [Some] constructor.
/!\ When using it, make sure the function runs in constant time or that gas
has been properly charged beforehand.
Also make sure it runs with a small, bounded stack.
*)
| KMap_head :
('a -> 'b) * ('b, 's, 'r, 'f) continuation
-> ('a, 's, 'r, 'f) continuation
(* This continuation comes right after a [Dip i] to restore the topmost
element ['b] of the stack after having executed [i] in the substack
of type ['a * 's]. *)
| KUndip :
'b * ('b, 'a * 's, 'r, 'f) continuation
-> ('a, 's, 'r, 'f) continuation
(* This continuation is executed at each iteration of a loop with
a Boolean condition. *)
| KLoop_in :
('a, 's, bool, 'a * 's) kinstr * ('a, 's, 'r, 'f) continuation
-> (bool, 'a * 's, 'r, 'f) continuation
(* This continuation is executed at each iteration of a loop with
a condition encoded by a sum type. *)
| KLoop_in_left :
('a, 's, ('a, 'b) union, 's) kinstr * ('b, 's, 'r, 'f) continuation
-> (('a, 'b) union, 's, 'r, 'f) continuation
(* This continuation is executed at each iteration of a traversal.
(Used in List, Map and Set.) *)
| KIter :
('a, 'b * 's, 'b, 's) kinstr * 'a list * ('b, 's, 'r, 'f) continuation
-> ('b, 's, 'r, 'f) continuation
(* This continuation represents each step of a List.map. *)
| KList_enter_body :
('a, 'c * 's, 'b, 'c * 's) kinstr
* 'a list
* 'b list
* int
* ('b boxed_list, 'c * 's, 'r, 'f) continuation
-> ('c, 's, 'r, 'f) continuation
(* This continuation represents what is done after each step of a List.map. *)
| KList_exit_body :
('a, 'c * 's, 'b, 'c * 's) kinstr
* 'a list
* 'b list
* int
* ('b boxed_list, 'c * 's, 'r, 'f) continuation
-> ('b, 'c * 's, 'r, 'f) continuation
(* This continuation represents each step of a Map.map. *)
| KMap_enter_body :
('a * 'b, 'd * 's, 'c, 'd * 's) kinstr
* ('a * 'b) list
* ('a, 'c) map
* (('a, 'c) map, 'd * 's, 'r, 'f) continuation
-> ('d, 's, 'r, 'f) continuation
(* This continuation represents what is done after each step of a Map.map. *)
| KMap_exit_body :
('a * 'b, 'd * 's, 'c, 'd * 's) kinstr
* ('a * 'b) list
* ('a, 'c) map
* 'a
* (('a, 'c) map, 'd * 's, 'r, 'f) continuation
-> ('c, 'd * 's, 'r, 'f) continuation
(* This continuation represents what is done after returning from a view.
It holds the original step constants value prior to entering the view. *)
| KView_exit :
step_constants * ('a, 's, 'r, 'f) continuation
-> ('a, 's, 'r, 'f) continuation
(* This continuation instruments the execution with a [logger]. *)
| KLog :
('a, 's, 'r, 'f) continuation * logger
-> ('a, 's, 'r, 'f) continuation
(*
Execution instrumentation
=========================
One can observe the context and the stack at some specific points
of an execution step. This feature is implemented by calling back
some [logging_function]s defined in a record of type [logger]
passed as argument to the step function.
A [logger] is typically embedded in an [KLog] continuation by the
client to trigger an evaluation instrumented with some logging. The
logger is then automatically propagated to the logging instruction
[ILog] as well as to any instructions that need to generate a
backtrace when it fails (e.g., [IFailwith], [IMul_teznat], ...).
*)
and ('a, 's, 'b, 'f, 'c, 'u) logging_function =
('a, 's, 'b, 'f) kinstr ->
context ->
Script.location ->
('c, 'u) stack_ty ->
'c * 'u ->
unit
and execution_trace = (Script.location * Gas.t * Script.expr list) list
and logger = {
log_interp : 'a 's 'b 'f 'c 'u. ('a, 's, 'b, 'f, 'c, 'u) logging_function;
(** [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. *)
}
(* ---- Auxiliary types -----------------------------------------------------*)
and ('ty, 'comparable) ty =
| Unit_t : (unit, yes) ty
| Int_t : (z num, yes) ty
| Nat_t : (n num, yes) ty
| Signature_t : (signature, yes) ty
| String_t : (Script_string.t, yes) ty
| Bytes_t : (bytes, yes) ty
| Mutez_t : (Tez.t, yes) ty
| Key_hash_t : (public_key_hash, yes) ty
| Key_t : (public_key, yes) ty
| Timestamp_t : (Script_timestamp.t, yes) ty
| Address_t : (address, yes) ty
| Tx_rollup_l2_address_t : (tx_rollup_l2_address, yes) ty
| Bool_t : (bool, yes) ty
| Pair_t :
('a, 'ac) ty
* ('b, 'bc) ty
* ('a, 'b) pair ty_metadata
* ('ac, 'bc, 'rc) dand
-> (('a, 'b) pair, 'rc) ty
| Union_t :
('a, 'ac) ty
* ('b, 'bc) ty
* ('a, 'b) union ty_metadata
* ('ac, 'bc, 'rc) dand
-> (('a, 'b) union, 'rc) ty
| Lambda_t :
('arg, _) ty * ('ret, _) ty * ('arg, 'ret) lambda ty_metadata
-> (('arg, 'ret) lambda, no) ty
| Option_t :
('v, 'c) ty * 'v option ty_metadata * 'c dbool
-> ('v option, 'c) ty
| List_t : ('v, _) ty * 'v boxed_list ty_metadata -> ('v boxed_list, no) ty
| Set_t : 'v comparable_ty * 'v set ty_metadata -> ('v set, no) ty
| Map_t :
'k comparable_ty * ('v, _) ty * ('k, 'v) map ty_metadata
-> (('k, 'v) map, no) ty
| Big_map_t :
'k comparable_ty * ('v, _) ty * ('k, 'v) big_map ty_metadata
-> (('k, 'v) big_map, no) ty
| Contract_t :
('arg, _) ty * 'arg typed_contract ty_metadata
-> ('arg typed_contract, no) ty
| Sapling_transaction_t : Sapling.Memo_size.t -> (Sapling.transaction, no) ty
| Sapling_transaction_deprecated_t :
Sapling.Memo_size.t
-> (Sapling.Legacy.transaction, no) ty
| Sapling_state_t : Sapling.Memo_size.t -> (Sapling.state, no) ty
| Operation_t : (operation, no) ty
| Chain_id_t : (Script_chain_id.t, yes) ty
| Never_t : (never, yes) ty
| Bls12_381_g1_t : (Script_bls.G1.t, no) ty
| Bls12_381_g2_t : (Script_bls.G2.t, no) ty
| Bls12_381_fr_t : (Script_bls.Fr.t, no) ty
| Ticket_t : 'a comparable_ty * 'a ticket ty_metadata -> ('a ticket, no) ty
| Chest_key_t : (Script_timelock.chest_key, no) ty
| Chest_t : (Script_timelock.chest, no) ty
and 'ty comparable_ty = ('ty, yes) ty
and ('top_ty, 'resty) stack_ty =
| Item_t :
('ty, _) ty * ('ty2, 'rest) stack_ty
-> ('ty, 'ty2 * 'rest) stack_ty
| Bot_t : (empty_cell, empty_cell) stack_ty
and ('key, 'value) big_map =
| Big_map : {
id : Big_map.Id.t option;
diff : ('key, 'value) big_map_overlay;
key_type : 'key comparable_ty;
value_type : ('value, _) ty;
}
-> ('key, 'value) big_map
and ('a, 's, 'r, 'f) kdescr = {
kloc : Script.location;
kbef : ('a, 's) stack_ty;
kaft : ('r, 'f) stack_ty;
kinstr : ('a, 's, 'r, 'f) kinstr;
}
and ('a, 's) kinfo = {iloc : Script.location; kstack_ty : ('a, 's) stack_ty}
(*
Several instructions work under an arbitrary deep stack prefix
(e.g, IDipn, IDropn, etc). To convince the typechecker that
these instructions are well-typed, we must provide a witness
to statically characterize the relationship between the input
and the output stacks. The inhabitants of the following GADT
act as such witnesses.
More precisely, a value [w] of type
[(c, t, d, v, a, s, b, u) stack_prefix_preservation_witness]
proves that there is a common prefix between an input stack
of type [a * s] and an output stack of type [b * u]. This prefix
is as deep as the number of [KPrefix] application in [w]. When
used with an operation parameterized by a natural number [n]
characterizing the depth at which the operation must be applied,
[w] is the Peano encoding of [n].
When this prefix is removed from the two stacks, the input stack
has type [c * t] while the output stack has type [d * v].
*)
and (_, _, _, _, _, _, _, _) stack_prefix_preservation_witness =
| KPrefix :
('y, 'u) kinfo
* ('c, 'v, 'd, 'w, 'x, 's, 'y, 'u) stack_prefix_preservation_witness
-> ( 'c,
'v,
'd,
'w,
'a,
'x * 's,
'a,
'y * 'u )
stack_prefix_preservation_witness
| KRest : ('a, 's, 'b, 'u, 'a, 's, 'b, 'u) stack_prefix_preservation_witness
and ('before, 'after) comb_gadt_witness =
| Comb_one : ('a * ('x * 'before), 'a * ('x * 'before)) comb_gadt_witness
| Comb_succ :
('before, 'b * 'after) comb_gadt_witness
-> ('a * 'before, ('a * 'b) * 'after) comb_gadt_witness
and ('before, 'after) uncomb_gadt_witness =
| Uncomb_one : ('rest, 'rest) uncomb_gadt_witness
| Uncomb_succ :
('b * 'before, 'after) uncomb_gadt_witness
-> (('a * 'b) * 'before, 'a * 'after) uncomb_gadt_witness
and ('before, 'after) comb_get_gadt_witness =
| Comb_get_zero : ('b, 'b) comb_get_gadt_witness
| Comb_get_one : ('a * 'b, 'a) comb_get_gadt_witness
| Comb_get_plus_two :
('before, 'after) comb_get_gadt_witness
-> ('a * 'before, 'after) comb_get_gadt_witness
and ('value, 'before, 'after) comb_set_gadt_witness =
| Comb_set_zero : ('value, _, 'value) comb_set_gadt_witness
| Comb_set_one : ('value, 'hd * 'tl, 'value * 'tl) comb_set_gadt_witness
| Comb_set_plus_two :
('value, 'before, 'after) comb_set_gadt_witness
-> ('value, 'a * 'before, 'a * 'after) comb_set_gadt_witness
[@@coq_force_gadt]
(*
[dup_n_gadt_witness ('s, 't)] ensures that there exists at least
[n] elements in ['s] and that the [n]-th element of ['s] is of type
['t]. Here [n] follows Peano's encoding (0 and successor).
Besides, [0] corresponds to the topmost element of ['s].
This relational predicate is defined by induction on [n].
*)
and (_, _) dup_n_gadt_witness =
| Dup_n_zero : ('a * 'rest, 'a) dup_n_gadt_witness
| Dup_n_succ :
('stack, 'b) dup_n_gadt_witness
-> ('a * 'stack, 'b) dup_n_gadt_witness
and ('input, 'output) view_signature =
| View_signature : {
name : Script_string.t;
input_ty : ('input, _) ty;
output_ty : ('output, _) ty;
}
-> ('input, 'output) view_signature
and 'kind manager_operation =
| Transaction : {
(* The [transaction.parameters] field may seem useless since we have
access to a typed version of the field (with [parameters_ty] and
[parameters]), but we keep it so that we do not have to unparse the
typed version in order to produce the receipt
([Apply_results.internal_manager_operation]). *)
transaction : Alpha_context.transaction;
location : Script.location;
parameters_ty : ('a, _) ty;
parameters : 'a;
}
-> Kind.transaction manager_operation
| Origination : {
origination : Alpha_context.origination;
preorigination : Contract.t;
storage_type : ('storage, _) ty;
storage : 'storage;
}
-> Kind.origination manager_operation
| Delegation :
Signature.Public_key_hash.t option
-> Kind.delegation manager_operation
and 'kind internal_operation = {
source : Contract.contract;
operation : 'kind manager_operation;
nonce : int;
}
and packed_internal_operation =
| Internal_operation : 'kind internal_operation -> packed_internal_operation
[@@ocaml.unboxed]
and operation = {
piop : packed_internal_operation;
lazy_storage_diff : Lazy_storage.diffs option;
}
type packed_manager_operation =
| Manager : 'kind manager_operation -> packed_manager_operation
[@@ocaml.unboxed]
val manager_kind : 'kind manager_operation -> 'kind Kind.manager
val kinfo_of_kinstr : ('a, 's, 'b, 'f) kinstr -> ('a, 's) kinfo
type kinstr_rewritek = {
apply : 'b 'u 'r 'f. ('b, 'u, 'r, 'f) kinstr -> ('b, 'u, 'r, 'f) kinstr;
}
val kinstr_rewritek :
('a, 's, 'r, 'f) kinstr -> kinstr_rewritek -> ('a, 's, 'r, 'f) kinstr
val ty_size : ('a, _) ty -> 'a Type_size.t
val comparable_ty_size : 'a comparable_ty -> 'a Type_size.t
val is_comparable : ('v, 'c) ty -> 'c dbool
type 'v ty_ex_c = Ty_ex_c : ('v, _) ty -> 'v ty_ex_c [@@ocaml.unboxed]
val unit_key : unit comparable_ty
val never_key : never comparable_ty
val int_key : z num comparable_ty
val nat_key : n num comparable_ty
val signature_key : signature comparable_ty
val string_key : Script_string.t comparable_ty
val bytes_key : Bytes.t comparable_ty
val mutez_key : Tez.t comparable_ty
val bool_key : bool comparable_ty
val key_hash_key : public_key_hash comparable_ty
val key_key : public_key comparable_ty
val timestamp_key : Script_timestamp.t comparable_ty
val chain_id_key : Script_chain_id.t comparable_ty
val address_key : address comparable_ty
val tx_rollup_l2_address_key : tx_rollup_l2_address comparable_ty
val pair_key :
Script.location ->
'a comparable_ty ->
'b comparable_ty ->
('a, 'b) pair comparable_ty tzresult
val pair_3_key :
Script.location ->
'a comparable_ty ->
'b comparable_ty ->
'c comparable_ty ->
('a, ('b, 'c) pair) pair comparable_ty tzresult
val union_key :
Script.location ->
'a comparable_ty ->
'b comparable_ty ->
('a, 'b) union comparable_ty tzresult
val option_key :
Script.location -> 'v comparable_ty -> 'v option comparable_ty tzresult
val unit_t : unit comparable_ty
val int_t : z num comparable_ty
val nat_t : n num comparable_ty
val signature_t : signature comparable_ty
val string_t : Script_string.t comparable_ty
val bytes_t : Bytes.t comparable_ty
val mutez_t : Tez.t comparable_ty
val key_hash_t : public_key_hash comparable_ty
val key_t : public_key comparable_ty
val timestamp_t : Script_timestamp.t comparable_ty
val address_t : address comparable_ty
val tx_rollup_l2_address_t : tx_rollup_l2_address comparable_ty
val bool_t : bool comparable_ty
val pair_t :
Script.location -> ('a, _) ty -> ('b, _) ty -> ('a, 'b) pair ty_ex_c tzresult
val comparable_pair_t :
Script.location ->
('a, yes) ty ->
('b, yes) ty ->
(('a, 'b) pair, yes) ty tzresult
val union_t :
Script.location -> ('a, _) ty -> ('b, _) ty -> ('a, 'b) union ty_ex_c tzresult
val comparable_union_t :
Script.location ->
('a, yes) ty ->
('b, yes) ty ->
('a, 'b) union comparable_ty tzresult
val union_bytes_bool_t : (Bytes.t, bool) union comparable_ty
val lambda_t :
Script.location ->
('arg, _) ty ->
('ret, _) ty ->
(('arg, 'ret) lambda, no) ty tzresult
val option_t : Script.location -> ('v, 'c) ty -> ('v option, 'c) ty tzresult
val option_mutez_t : Tez.t option comparable_ty
val option_string_t : Script_string.t option comparable_ty
val option_bytes_t : Bytes.t option comparable_ty
val option_nat_t : n num option comparable_ty
val option_pair_nat_nat_t : (n num, n num) pair option comparable_ty
val option_pair_nat_mutez_t : (n num, Tez.t) pair option comparable_ty
val option_pair_mutez_mutez_t : (Tez.t, Tez.t) pair option comparable_ty
val option_pair_int_nat_t : (z num, n num) pair option comparable_ty
val list_t : Script.location -> ('v, _) ty -> ('v boxed_list, no) ty tzresult
val list_operation_t : (operation boxed_list, no) ty
val set_t : Script.location -> 'v comparable_ty -> ('v set, no) ty tzresult
val map_t :
Script.location ->
'k comparable_ty ->
('v, _) ty ->
(('k, 'v) map, no) ty tzresult
val big_map_t :
Script.location ->
'k comparable_ty ->
('v, _) ty ->
(('k, 'v) big_map, no) ty tzresult
val contract_t :
Script.location -> ('arg, _) ty -> ('arg typed_contract, no) ty tzresult
val contract_unit_t : (unit typed_contract, no) ty
val sapling_transaction_t :
memo_size:Sapling.Memo_size.t -> (Sapling.transaction, no) ty
val sapling_transaction_deprecated_t :
memo_size:Sapling.Memo_size.t -> (Sapling.Legacy.transaction, no) ty
val sapling_state_t : memo_size:Sapling.Memo_size.t -> (Sapling.state, no) ty
val operation_t : (operation, no) ty
val chain_id_t : Script_chain_id.t comparable_ty
val never_t : never comparable_ty
val bls12_381_g1_t : (Script_bls.G1.t, no) ty
val bls12_381_g2_t : (Script_bls.G2.t, no) ty
val bls12_381_fr_t : (Script_bls.Fr.t, no) ty
val ticket_t :
Script.location -> 'a comparable_ty -> ('a ticket, no) ty tzresult
val chest_key_t : (Script_timelock.chest_key, no) ty
val chest_t : (Script_timelock.chest, no) ty
(**
The following functions named `X_traverse` for X in
[{ kinstr, ty, comparable_ty, value }] provide tail recursive top down
traversals over the values of these types.
The traversal goes through a value and rewrites an accumulator
along the way starting from some [init]ial value for the
accumulator.
All these traversals follow the same recursion scheme: the
user-provided function is first called on the toplevel value, then
the traversal recurses on the direct subvalues of the same type.
Hence, the user-provided function must only compute the
contribution of the value on the accumulator minus the contribution
of its subvalues of the same type.
*)
type 'a kinstr_traverse = {
apply : 'b 'u 'r 'f. 'a -> ('b, 'u, 'r, 'f) kinstr -> 'a;
}
val kinstr_traverse :
('a, 'b, 'c, 'd) kinstr -> 'ret -> 'ret kinstr_traverse -> 'ret
type 'a ty_traverse = {
apply : 't 'tc. 'a -> ('t, 'tc) ty -> 'a;
apply_comparable : 't. 'a -> 't comparable_ty -> 'a;
}
val comparable_ty_traverse : 'a comparable_ty -> 'r -> 'r ty_traverse -> 'r
val ty_traverse : ('a, _) ty -> 'r -> 'r ty_traverse -> 'r
type 'accu stack_ty_traverse = {
apply : 'ty 's. 'accu -> ('ty, 's) stack_ty -> 'accu;
}
val stack_ty_traverse : ('a, 's) stack_ty -> 'r -> 'r stack_ty_traverse -> 'r
type 'a value_traverse = {
apply : 't 'tc. 'a -> ('t, 'tc) ty -> 't -> 'a;
apply_comparable : 't. 'a -> 't comparable_ty -> 't -> 'a;
}
val value_traverse :
(('t, _) ty, 't comparable_ty) union -> 't -> 'r -> 'r value_traverse -> 'r
val stack_top_ty : ('a, 'b * 's) stack_ty -> 'a ty_ex_c
Computing file changes ...
