script_ir_translator.mli
(*****************************************************************************)
(* *)
(* Open Source License *)
(* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. <contact@tezos.com> *)
(* Copyright (c) 2021-2022 Nomadic Labs <contact@nomadic-labs.com> *)
(* Copyright (c) 2022 Trili Tech <contact@trili.tech> *)
(* *)
(* 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. *)
(* *)
(*****************************************************************************)
(* Overview:
This mli is organized into roughly three parts:
1. A set of new types prefixed with "ex_"
Michelson is encoded in a GADT that preserves certain properties about its
type system. If you haven't read about GADT's, check out the relevant section
in the Tezos docs:
https://tezos.gitlab.io/developer/gadt.html#generalized-algebraic-data-types-gadts
The idea is that type representing a Michelson type, ['a ty], is parameterized
by a type 'a. But that 'a can't be just _any_ type; it must be valid according
to the definition of ['a ty]. Thus, if I give you a value of type ['a ty],
all you know is that "there exists some 'a such that 'a ty exists". You must be
careful not to accidentally quantify 'a universally, that is "for all 'a,
'a ty exists", otherwise you'll get an annoying error about 'a trying to escape
it's scope. We do this by hiding 'a in an existential type. This is what
ex_comparable_ty, ex_ty, ex_stack_ty, etc. do.
2. A set of functions dealing with high-level Michelson types:
This module also provides functions for interacting with the list, map,
set, and big_map Michelson types.
3. A set of functions for parsing and typechecking Michelson.
Finally, and what you likely came for, the module provides many functions prefixed
with "parse_" that convert untyped Micheline (which is essentially S-expressions
with a few primitive atom types) into the GADT encoding well-typed Michelson. Likewise
there is a number of functions prefixed "unparse_" that do the reverse. These functions
consume gas, and thus are parameterized by an [Alpha_context.t].
The variety of functions reflects the variety of things one might want to parse,
from [parse_data] for arbitrary Micheline expressions to [parse_contract_data] for
well-formed Michelson contracts.
*)
(** {1 Michelson Existential Witness types} *)
open Alpha_context
open Script_typed_ir
open Script_tc_errors
type ('ta, 'tb) eq = Eq : ('same, 'same) eq
type ex_comparable_ty =
| Ex_comparable_ty : 'a Script_typed_ir.comparable_ty -> ex_comparable_ty
type ex_parameter_ty_and_entrypoints =
| Ex_parameter_ty_and_entrypoints : {
arg_type : ('a, _) Script_typed_ir.ty;
entrypoints : 'a Script_typed_ir.entrypoints;
}
-> ex_parameter_ty_and_entrypoints
type ex_stack_ty =
| Ex_stack_ty : ('a, 's) Script_typed_ir.stack_ty -> ex_stack_ty
type ex_script = Ex_script : ('a, 'b) Script_typed_ir.script -> ex_script
type toplevel = {
code_field : Script.node;
arg_type : Script.node;
storage_type : Script.node;
views : Script_typed_ir.view_map;
}
type ('arg, 'storage) code =
| Code : {
code :
( ('arg, 'storage) Script_typed_ir.pair,
( Script_typed_ir.operation Script_typed_ir.boxed_list,
'storage )
Script_typed_ir.pair )
Script_typed_ir.lambda;
arg_type : ('arg, _) Script_typed_ir.ty;
storage_type : ('storage, _) Script_typed_ir.ty;
views : Script_typed_ir.view_map;
entrypoints : 'arg Script_typed_ir.entrypoints;
code_size : Cache_memory_helpers.sint;
(** This is an over-approximation of the value size in memory, in
bytes, of the contract's static part, that is its source
code. This includes the code of the contract as well as the code
of the views. The storage size is not taken into account by this
field as it has a dynamic size. *)
}
-> ('arg, 'storage) code
type ex_code = Ex_code : ('a, 'c) code -> ex_code
type 'storage typed_view =
| Typed_view : {
input_ty : ('input, _) Script_typed_ir.ty;
output_ty : ('output, _) Script_typed_ir.ty;
kinstr :
( 'input * 'storage,
Script_typed_ir.end_of_stack,
'output,
Script_typed_ir.end_of_stack )
Script_typed_ir.kinstr;
original_code_expr : Script.node;
}
-> 'storage typed_view
type 'storage typed_view_map =
(Script_string.t, 'storage typed_view) Script_typed_ir.map
type ('a, 's, 'b, 'u) cinstr = {
apply :
'r 'f.
('b, 'u, 'r, 'f) Script_typed_ir.kinstr ->
('a, 's, 'r, 'f) Script_typed_ir.kinstr;
}
[@@ocaml.unboxed]
type ('a, 's, 'b, 'u) descr = {
loc : Script.location;
bef : ('a, 's) Script_typed_ir.stack_ty;
aft : ('b, 'u) Script_typed_ir.stack_ty;
instr : ('a, 's, 'b, 'u) cinstr;
}
type tc_context = Script_tc_context.t
type ('a, 's) judgement =
| Typed : ('a, 's, 'b, 'u) descr -> ('a, 's) judgement
| Failed : {
descr : 'b 'u. ('b, 'u) Script_typed_ir.stack_ty -> ('a, 's, 'b, 'u) descr;
}
-> ('a, 's) judgement
val close_descr :
('a, 'b, 'c, 'd) descr -> ('a, 'b, 'c, 'd) Script_typed_ir.kdescr
(* ---- Lists, Sets and Maps ----------------------------------------------- *)
(** {2 High-level Michelson Data Types} *)
val ty_eq :
error_details:(Script.location, 'error_trace) error_details ->
('a, 'ac) Script_typed_ir.ty ->
('b, 'bc) Script_typed_ir.ty ->
( (('a, 'ac) Script_typed_ir.ty, ('b, 'bc) Script_typed_ir.ty) eq,
'error_trace )
Gas_monad.t
(** {3 Parsing and Typechecking Michelson} *)
val parse_comparable_data :
?type_logger:Script_ir_translator_config.type_logger ->
context ->
'a Script_typed_ir.comparable_ty ->
Script.node ->
('a * context) tzresult Lwt.t
(* Parsing a Micheline node data into an IR-typed data. *)
val parse_data :
elab_conf:Script_ir_translator_config.elab_config ->
context ->
allow_forged:bool ->
('a, _) Script_typed_ir.ty ->
Script.node ->
('a * context) tzresult Lwt.t
(* Unparsing an IR-typed data back into a Micheline node data *)
val unparse_data :
context ->
Script_ir_unparser.unparsing_mode ->
('a, _) Script_typed_ir.ty ->
'a ->
(Script.expr * context) tzresult Lwt.t
val unparse_code :
context ->
Script_ir_unparser.unparsing_mode ->
Script.node ->
(Script.expr * context) tzresult Lwt.t
(** For benchmarking purpose, we also export versions of the unparsing
functions which don't call location stripping. These functions are
not carbonated and should not be called directly from the protocol. *)
module Internal_for_benchmarking : sig
val unparse_data :
context ->
stack_depth:int ->
Script_ir_unparser.unparsing_mode ->
('a, 'ac) ty ->
'a ->
(Script.node * context) tzresult Lwt.t
val unparse_code :
context ->
stack_depth:int ->
Script_ir_unparser.unparsing_mode ->
Script.node ->
(Script.node * context) tzresult Lwt.t
end
val parse_instr :
elab_conf:Script_ir_translator_config.elab_config ->
tc_context ->
context ->
Script.node ->
('a, 's) Script_typed_ir.stack_ty ->
(('a, 's) judgement * context) tzresult Lwt.t
(**
[parse_ty] specialized for the right-hand side part of a big map type, i.e.
the `value` in `big_map key value`.
*)
val parse_big_map_value_ty :
context -> legacy:bool -> Script.node -> (ex_ty * context) tzresult
val parse_packable_ty :
context -> legacy:bool -> Script.node -> (ex_ty * context) tzresult
val parse_passable_ty :
context -> legacy:bool -> Script.node -> (ex_ty * context) tzresult
val parse_comparable_ty :
context -> Script.node -> (ex_comparable_ty * context) tzresult
val parse_parameter_ty_and_entrypoints :
context ->
legacy:bool ->
Script.node ->
(ex_parameter_ty_and_entrypoints * context) tzresult
val parse_view_input_ty :
context ->
stack_depth:int ->
legacy:bool ->
Script.node ->
(ex_ty * context) tzresult
val parse_view_output_ty :
context ->
stack_depth:int ->
legacy:bool ->
Script.node ->
(ex_ty * context) tzresult
val parse_view :
elab_conf:Script_ir_translator_config.elab_config ->
context ->
('storage, _) Script_typed_ir.ty ->
Script_typed_ir.view ->
('storage typed_view * context) tzresult Lwt.t
val parse_views :
elab_conf:Script_ir_translator_config.elab_config ->
context ->
('storage, _) Script_typed_ir.ty ->
Script_typed_ir.view_map ->
('storage typed_view_map * context) tzresult Lwt.t
(**
[parse_ty] allowing big_map values, operations, contract and tickets.
*)
val parse_any_ty :
context -> legacy:bool -> Script.node -> (ex_ty * context) tzresult
(** We expose [parse_ty] for convenience to external tools. Please use
specialized versions such as [parse_packable_ty], [parse_passable_ty],
[parse_comparable_ty], or [parse_big_map_value_ty] if possible. *)
val parse_ty :
context ->
legacy:bool ->
allow_lazy_storage:bool ->
allow_operation:bool ->
allow_contract:bool ->
allow_ticket:bool ->
Script.node ->
(ex_ty * context) tzresult
val parse_toplevel :
context -> legacy:bool -> Script.expr -> (toplevel * context) tzresult Lwt.t
(** High-level function to typecheck a Michelson script. This function is not
used for validating operations but only for the [typecheck_code] RPC.
If [show_types] is set to [true], details of the typechecking are returned
in the [type_map], otherwise the returned [type_map] is empty. *)
val typecheck_code :
legacy:bool ->
show_types:bool ->
context ->
Script.expr ->
(type_map * context) tzresult Lwt.t
val parse_code :
elab_conf:Script_ir_translator_config.elab_config ->
context ->
code:Script.lazy_expr ->
(ex_code * context) tzresult Lwt.t
val parse_storage :
elab_conf:Script_ir_translator_config.elab_config ->
context ->
allow_forged:bool ->
('storage, _) Script_typed_ir.ty ->
storage:Script.lazy_expr ->
('storage * context) tzresult Lwt.t
(** Combines [parse_code] and [parse_storage] *)
val parse_script :
elab_conf:Script_ir_translator_config.elab_config ->
context ->
allow_forged_in_storage:bool ->
Script.t ->
(ex_script * context) tzresult Lwt.t
(* Gas accounting may not be perfect in this function, as it is only called by RPCs. *)
val parse_and_unparse_script_unaccounted :
context ->
legacy:bool ->
allow_forged_in_storage:bool ->
Script_ir_unparser.unparsing_mode ->
normalize_types:bool ->
Script.t ->
(Script.t * context) tzresult Lwt.t
val parse_contract_data :
context ->
Script.location ->
('a, _) Script_typed_ir.ty ->
Destination.t ->
entrypoint:Entrypoint.t ->
(context * 'a Script_typed_ir.typed_contract) tzresult Lwt.t
val parse_contract_for_script :
context ->
Script.location ->
('a, _) Script_typed_ir.ty ->
Destination.t ->
entrypoint:Entrypoint.t ->
(context * 'a Script_typed_ir.typed_contract option) tzresult Lwt.t
(** ['a ex_ty_cstr] is like [ex_ty], but also adds to the existential a function
used to reconstruct a value of type ['a] from the internal type of the
existential. Typically, it will be used to go from the type of an
entry-point to the full type of a contract. *)
type 'a ex_ty_cstr =
| Ex_ty_cstr : {
ty : ('b, _) Script_typed_ir.ty;
construct : 'b -> 'a;
original_type_expr : Script.node;
}
-> 'a ex_ty_cstr
val find_entrypoint :
error_details:(_, 'error_trace) error_details ->
('t, _) Script_typed_ir.ty ->
't Script_typed_ir.entrypoints ->
Entrypoint.t ->
('t ex_ty_cstr, 'error_trace) Gas_monad.t
val list_entrypoints_uncarbonated :
('t, _) Script_typed_ir.ty ->
't Script_typed_ir.entrypoints ->
Michelson_v1_primitives.prim list list
* (ex_ty * Script.node) Entrypoint.Map.t
val pack_data :
context ->
('a, _) Script_typed_ir.ty ->
'a ->
(bytes * context) tzresult Lwt.t
val hash_comparable_data :
context ->
'a Script_typed_ir.comparable_ty ->
'a ->
(Script_expr_hash.t * context) tzresult Lwt.t
val hash_data :
context ->
('a, _) Script_typed_ir.ty ->
'a ->
(Script_expr_hash.t * context) tzresult Lwt.t
type lazy_storage_ids
val no_lazy_storage_id : lazy_storage_ids
(** Traverse the given type, producing a {!lazy_storage_ids} for
use with {!extract_lazy_storage_diff}.
*)
val collect_lazy_storage :
context ->
('a, _) Script_typed_ir.ty ->
'a ->
(lazy_storage_ids * context) tzresult
val list_of_big_map_ids : lazy_storage_ids -> Big_map.Id.t list
(** Produce a lazy storage diff, containing in-memory writes to
lazy data structures such as big_maps yet to be committed.
The resulting diff can be committed to the underlying storage
(context) using [Lazy_storage_diff.apply].
@param to_duplicate
Lazy data structure reference produced via {!collect_lazy_storage}
that can not be reused. Typically collected via traversing
the parameters to a smart contract.
@param to_update
Lazy data structure reference produced via {!collect_lazy_storage}
that can be reused. Typically collected via traversing the previous
storage of a smart contract.
*)
val extract_lazy_storage_diff :
context ->
Script_ir_unparser.unparsing_mode ->
temporary:bool ->
to_duplicate:lazy_storage_ids ->
to_update:lazy_storage_ids ->
('a, _) Script_typed_ir.ty ->
'a ->
('a * Lazy_storage.diffs option * context) tzresult Lwt.t
(* return [None] if none or more than one found *)
val get_single_sapling_state :
context ->
('a, _) Script_typed_ir.ty ->
'a ->
(Sapling.Id.t option * context) tzresult
(** [code_size ctxt code views] returns an overapproximation of the size of
the in-memory representation of [code] and [views] in bytes in the
context [ctxt]. *)
val code_size :
context ->
('a, 'b) Script_typed_ir.lambda ->
Script_typed_ir.view_map ->
(Cache_memory_helpers.sint * context) tzresult
(** [script_size script] returns an overapproximation of the size of
the in-memory representation of [script] in bytes as well as the cost
associated to computing that overapproximation. *)
val script_size : ex_script -> int * Gas_limit_repr.cost
