script_ir_translator.ml
(*****************************************************************************)
(* *)
(* 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> *)
(* 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. *)
(* *)
(*****************************************************************************)
open Alpha_context
open Micheline
open Script
open Script_tc_errors
open Script_ir_annot
open Script_typed_ir
open Script_ir_unparser
module Typecheck_costs = Michelson_v1_gas.Cost_of.Typechecking
module Unparse_costs = Michelson_v1_gas.Cost_of.Unparsing
module Tc_context = Script_tc_context
type elab_conf = Script_ir_translator_config.elab_config
type ex_stack_ty = Ex_stack_ty : ('a, 's) stack_ty -> ex_stack_ty
(* Equality witnesses *)
type ('ta, 'tb) eq = Eq : ('same, 'same) eq
(*
The following type represents an instruction parameterized by its
continuation. During the elaboration of the typed term, a sequence
of instructions in Micheline is read from left to right: hence, the
elaboration needs to wait for the next instruction to be elaborated
to be able to construct the current instruction.
*)
type ('a, 's, 'b, 'u) cinstr = {
apply : 'r 'f. ('b, 'u, 'r, 'f) kinstr -> ('a, 's, 'r, 'f) kinstr;
}
[@@ocaml.unboxed]
(*
While a [Script_typed_ir.descr] contains a fully defined
instruction, [descr] contains a [cinstr], that is an instruction
parameterized by the next instruction, as explained in the previous
comment.
*)
type ('a, 's, 'b, 'u) descr = {
loc : Script.location;
bef : ('a, 's) stack_ty;
aft : ('b, 'u) stack_ty;
instr : ('a, 's, 'b, 'u) cinstr;
}
let close_descr {loc; bef; aft; instr} =
let kinstr = instr.apply (IHalt loc) in
{kloc = loc; kbef = bef; kaft = aft; kinstr}
let compose_descr :
type a s b u c v.
Script.location ->
(a, s, b, u) descr ->
(b, u, c, v) descr ->
(a, s, c, v) descr =
fun loc d1 d2 ->
{
loc;
bef = d1.bef;
aft = d2.aft;
instr = {apply = (fun k -> d1.instr.apply (d2.instr.apply k))};
}
type tc_context = Tc_context.t
(* ---- Error helpers -------------------------------------------------------*)
let location = function
| Prim (loc, _, _, _)
| Int (loc, _)
| String (loc, _)
| Bytes (loc, _)
| Seq (loc, _) ->
loc
let kind_equal a b =
match (a, b) with
| Int_kind, Int_kind
| String_kind, String_kind
| Bytes_kind, Bytes_kind
| Prim_kind, Prim_kind
| Seq_kind, Seq_kind ->
true
| _ -> false
let kind = function
| Int _ -> Int_kind
| String _ -> String_kind
| Bytes _ -> Bytes_kind
| Prim _ -> Prim_kind
| Seq _ -> Seq_kind
let unexpected expr exp_kinds exp_ns exp_prims =
match expr with
| Int (loc, _) -> Invalid_kind (loc, Prim_kind :: exp_kinds, Int_kind)
| String (loc, _) -> Invalid_kind (loc, Prim_kind :: exp_kinds, String_kind)
| Bytes (loc, _) -> Invalid_kind (loc, Prim_kind :: exp_kinds, Bytes_kind)
| Seq (loc, _) -> Invalid_kind (loc, Prim_kind :: exp_kinds, Seq_kind)
| Prim (loc, name, _, _) -> (
let open Michelson_v1_primitives in
match (namespace name, exp_ns) with
| Type_namespace, Type_namespace
| Instr_namespace, Instr_namespace
| Constant_namespace, Constant_namespace ->
Invalid_primitive (loc, exp_prims, name)
| ns, _ -> Invalid_namespace (loc, name, exp_ns, ns))
let check_kind kinds expr =
let kind = kind expr in
if List.exists (kind_equal kind) kinds then Result.return_unit
else
let loc = location expr in
error (Invalid_kind (loc, kinds, kind))
let check_comparable :
type a ac.
Script.location -> (a, ac) ty -> (ac, Dependent_bool.yes) eq tzresult =
fun loc ty ->
match is_comparable ty with
| Yes -> ok Eq
| No ->
let t = Script_ir_unparser.serialize_ty_for_error ty in
error (Comparable_type_expected (loc, t))
let pack_node unparsed ctxt =
Gas.consume ctxt (Script.strip_locations_cost unparsed) >>? fun ctxt ->
let bytes =
Data_encoding.Binary.to_bytes_exn
expr_encoding
(Micheline.strip_locations unparsed)
in
Gas.consume ctxt (Script.serialized_cost bytes) >|? fun ctxt ->
let bytes = Bytes.cat (Bytes.of_string "\005") bytes in
(bytes, ctxt)
let pack_comparable_data ctxt ty data =
unparse_comparable_data ~loc:() ctxt Optimized_legacy ty data
>>=? fun (unparsed, ctxt) -> Lwt.return @@ pack_node unparsed ctxt
let hash_bytes ctxt bytes =
Gas.consume ctxt (Michelson_v1_gas.Cost_of.Interpreter.blake2b bytes)
>|? fun ctxt -> (Script_expr_hash.(hash_bytes [bytes]), ctxt)
let hash_comparable_data ctxt ty data =
pack_comparable_data ctxt ty data >>=? fun (bytes, ctxt) ->
Lwt.return @@ hash_bytes ctxt bytes
(* ---- Tickets ------------------------------------------------------------ *)
(*
All comparable types are dupable, this function exists only to not forget
checking this property when adding new types.
*)
let check_dupable_comparable_ty : type a. a comparable_ty -> unit = function
| Unit_t | Never_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t
| Mutez_t | Bool_t | Key_hash_t | Key_t | Timestamp_t | Chain_id_t | Address_t
| Tx_rollup_l2_address_t | Pair_t _ | Union_t _ | Option_t _ ->
()
let check_dupable_ty ctxt loc ty =
let rec aux : type a ac. location -> (a, ac) ty -> (unit, error) Gas_monad.t =
fun loc ty ->
let open Gas_monad.Syntax in
let* () = Gas_monad.consume_gas Typecheck_costs.check_dupable_cycle in
match ty with
| Unit_t -> return_unit
| Int_t -> return_unit
| Nat_t -> return_unit
| Signature_t -> return_unit
| String_t -> return_unit
| Bytes_t -> return_unit
| Mutez_t -> return_unit
| Key_hash_t -> return_unit
| Key_t -> return_unit
| Timestamp_t -> return_unit
| Address_t -> return_unit
| Tx_rollup_l2_address_t -> return_unit
| Bool_t -> return_unit
| Contract_t _ -> return_unit
| Operation_t -> return_unit
| Chain_id_t -> return_unit
| Never_t -> return_unit
| Bls12_381_g1_t -> return_unit
| Bls12_381_g2_t -> return_unit
| Bls12_381_fr_t -> return_unit
| Sapling_state_t _ -> return_unit
| Sapling_transaction_t _ -> return_unit
| Sapling_transaction_deprecated_t _ -> return_unit
| Chest_t -> return_unit
| Chest_key_t -> return_unit
| Ticket_t _ -> fail @@ Unexpected_ticket loc
| Pair_t (ty_a, ty_b, _, _) ->
let* () = aux loc ty_a in
aux loc ty_b
| Union_t (ty_a, ty_b, _, _) ->
let* () = aux loc ty_a in
aux loc ty_b
| Lambda_t (_, _, _) ->
(*
Lambda are dupable as long as:
- they don't contain non-dupable values, e.g. in `PUSH`
(mostly non-dupable values should probably be considered forged)
- they are not the result of a partial application on a non-dupable
value. `APPLY` rejects non-packable types (because of `PUSH`).
Hence non-dupable should imply non-packable.
*)
return_unit
| Option_t (ty, _, _) -> aux loc ty
| List_t (ty, _) -> aux loc ty
| Set_t (key_ty, _) ->
let () = check_dupable_comparable_ty key_ty in
return_unit
| Map_t (key_ty, val_ty, _) ->
let () = check_dupable_comparable_ty key_ty in
aux loc val_ty
| Big_map_t (key_ty, val_ty, _) ->
let () = check_dupable_comparable_ty key_ty in
aux loc val_ty
in
let gas = aux loc ty in
Gas_monad.run ctxt gas >>? fun (res, ctxt) ->
match res with Ok () -> ok ctxt | Error e -> error e
let type_metadata_eq :
type error_trace.
error_details:(_, error_trace) error_details ->
'a ty_metadata ->
'b ty_metadata ->
(unit, error_trace) result =
fun ~error_details {size = size_a} {size = size_b} ->
Type_size.check_eq ~error_details size_a size_b
let default_ty_eq_error loc ty1 ty2 =
let ty1 = serialize_ty_for_error ty1 in
let ty2 = serialize_ty_for_error ty2 in
Inconsistent_types (loc, ty1, ty2)
let memo_size_eq :
type error_trace.
error_details:(_, error_trace) error_details ->
Sapling.Memo_size.t ->
Sapling.Memo_size.t ->
(unit, error_trace) result =
fun ~error_details ms1 ms2 ->
if Sapling.Memo_size.equal ms1 ms2 then Result.return_unit
else
Error
(match error_details with
| Fast -> Inconsistent_types_fast
| Informative _ -> trace_of_error @@ Inconsistent_memo_sizes (ms1, ms2))
(* Check that two types are equal.
The result is an equality witness between the types of the two inputs within
the gas monad (for gas consumption).
*)
let rec ty_eq :
type a ac b bc error_trace.
error_details:(Script.location, error_trace) error_details ->
(a, ac) ty ->
(b, bc) ty ->
(((a, ac) ty, (b, bc) ty) eq, error_trace) Gas_monad.t =
fun ~error_details ty1 ty2 ->
let type_metadata_eq meta1 meta2 =
Gas_monad.of_result (type_metadata_eq ~error_details meta1 meta2)
|> Gas_monad.record_trace_eval ~error_details (fun loc ->
default_ty_eq_error loc ty1 ty2)
in
let memo_size_eq ms1 ms2 =
Gas_monad.of_result (memo_size_eq ~error_details ms1 ms2)
in
let rec help :
type ta tac tb tbc.
(ta, tac) ty ->
(tb, tbc) ty ->
(((ta, tac) ty, (tb, tbc) ty) eq, error_trace) Gas_monad.t =
fun ty1 ty2 ->
help0 ty1 ty2
|> Gas_monad.record_trace_eval ~error_details (fun loc ->
default_ty_eq_error loc ty1 ty2)
and help0 :
type ta tac tb tbc.
(ta, tac) ty ->
(tb, tbc) ty ->
(((ta, tac) ty, (tb, tbc) ty) eq, error_trace) Gas_monad.t =
fun ty1 ty2 ->
let open Gas_monad.Syntax in
let* () = Gas_monad.consume_gas Typecheck_costs.merge_cycle in
let not_equal () =
Gas_monad.of_result
@@ Error
(match error_details with
| Fast -> (Inconsistent_types_fast : error_trace)
| Informative loc ->
trace_of_error @@ default_ty_eq_error loc ty1 ty2)
in
match (ty1, ty2) with
| Unit_t, Unit_t -> return (Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
| Unit_t, _ -> not_equal ()
| Int_t, Int_t -> return Eq
| Int_t, _ -> not_equal ()
| Nat_t, Nat_t -> return Eq
| Nat_t, _ -> not_equal ()
| Key_t, Key_t -> return Eq
| Key_t, _ -> not_equal ()
| Key_hash_t, Key_hash_t -> return Eq
| Key_hash_t, _ -> not_equal ()
| String_t, String_t -> return Eq
| String_t, _ -> not_equal ()
| Bytes_t, Bytes_t -> return Eq
| Bytes_t, _ -> not_equal ()
| Signature_t, Signature_t -> return Eq
| Signature_t, _ -> not_equal ()
| Mutez_t, Mutez_t -> return Eq
| Mutez_t, _ -> not_equal ()
| Timestamp_t, Timestamp_t -> return Eq
| Timestamp_t, _ -> not_equal ()
| Address_t, Address_t -> return Eq
| Address_t, _ -> not_equal ()
| Tx_rollup_l2_address_t, Tx_rollup_l2_address_t -> return Eq
| Tx_rollup_l2_address_t, _ -> not_equal ()
| Bool_t, Bool_t -> return Eq
| Bool_t, _ -> not_equal ()
| Chain_id_t, Chain_id_t -> return Eq
| Chain_id_t, _ -> not_equal ()
| Never_t, Never_t -> return Eq
| Never_t, _ -> not_equal ()
| Operation_t, Operation_t -> return Eq
| Operation_t, _ -> not_equal ()
| Bls12_381_g1_t, Bls12_381_g1_t -> return Eq
| Bls12_381_g1_t, _ -> not_equal ()
| Bls12_381_g2_t, Bls12_381_g2_t -> return Eq
| Bls12_381_g2_t, _ -> not_equal ()
| Bls12_381_fr_t, Bls12_381_fr_t -> return Eq
| Bls12_381_fr_t, _ -> not_equal ()
| Map_t (tal, tar, meta1), Map_t (tbl, tbr, meta2) ->
let* () = type_metadata_eq meta1 meta2 in
let* Eq = help tar tbr in
let+ Eq = ty_eq ~error_details tal tbl in
(Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
| Map_t _, _ -> not_equal ()
| Big_map_t (tal, tar, meta1), Big_map_t (tbl, tbr, meta2) ->
let* () = type_metadata_eq meta1 meta2 in
let* Eq = help tar tbr in
let+ Eq = ty_eq ~error_details tal tbl in
(Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
| Big_map_t _, _ -> not_equal ()
| Set_t (ea, meta1), Set_t (eb, meta2) ->
let* () = type_metadata_eq meta1 meta2 in
let+ Eq = ty_eq ~error_details ea eb in
(Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
| Set_t _, _ -> not_equal ()
| Ticket_t (ea, meta1), Ticket_t (eb, meta2) ->
let* () = type_metadata_eq meta1 meta2 in
let+ Eq = ty_eq ~error_details ea eb in
(Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
| Ticket_t _, _ -> not_equal ()
| Pair_t (tal, tar, meta1, cmp1), Pair_t (tbl, tbr, meta2, cmp2) ->
let* () = type_metadata_eq meta1 meta2 in
let* Eq = help tal tbl in
let+ Eq = help tar tbr in
let Eq = Dependent_bool.merge_dand cmp1 cmp2 in
(Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
| Pair_t _, _ -> not_equal ()
| Union_t (tal, tar, meta1, cmp1), Union_t (tbl, tbr, meta2, cmp2) ->
let* () = type_metadata_eq meta1 meta2 in
let* Eq = help tal tbl in
let+ Eq = help tar tbr in
let Eq = Dependent_bool.merge_dand cmp1 cmp2 in
(Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
| Union_t _, _ -> not_equal ()
| Lambda_t (tal, tar, meta1), Lambda_t (tbl, tbr, meta2) ->
let* () = type_metadata_eq meta1 meta2 in
let* Eq = help tal tbl in
let+ Eq = help tar tbr in
(Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
| Lambda_t _, _ -> not_equal ()
| Contract_t (tal, meta1), Contract_t (tbl, meta2) ->
let* () = type_metadata_eq meta1 meta2 in
let+ Eq = help tal tbl in
(Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
| Contract_t _, _ -> not_equal ()
| Option_t (tva, meta1, _), Option_t (tvb, meta2, _) ->
let* () = type_metadata_eq meta1 meta2 in
let+ Eq = help tva tvb in
(Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
| Option_t _, _ -> not_equal ()
| List_t (tva, meta1), List_t (tvb, meta2) ->
let* () = type_metadata_eq meta1 meta2 in
let+ Eq = help tva tvb in
(Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
| List_t _, _ -> not_equal ()
| Sapling_state_t ms1, Sapling_state_t ms2 ->
let+ () = memo_size_eq ms1 ms2 in
Eq
| Sapling_state_t _, _ -> not_equal ()
| Sapling_transaction_t ms1, Sapling_transaction_t ms2 ->
let+ () = memo_size_eq ms1 ms2 in
Eq
| Sapling_transaction_t _, _ -> not_equal ()
| Sapling_transaction_deprecated_t ms1, Sapling_transaction_deprecated_t ms2
->
let+ () = memo_size_eq ms1 ms2 in
Eq
| Sapling_transaction_deprecated_t _, _ -> not_equal ()
| Chest_t, Chest_t -> return Eq
| Chest_t, _ -> not_equal ()
| Chest_key_t, Chest_key_t -> return Eq
| Chest_key_t, _ -> not_equal ()
in
help ty1 ty2
(* Same as ty_eq but for stacks.
A single error monad is used here because there is no need to
recover from stack merging errors. *)
let rec stack_eq :
type ta tb ts tu.
Script.location ->
context ->
int ->
(ta, ts) stack_ty ->
(tb, tu) stack_ty ->
(((ta, ts) stack_ty, (tb, tu) stack_ty) eq * context) tzresult =
fun loc ctxt lvl stack1 stack2 ->
match (stack1, stack2) with
| Bot_t, Bot_t -> ok (Eq, ctxt)
| Item_t (ty1, rest1), Item_t (ty2, rest2) ->
Gas_monad.run ctxt @@ ty_eq ~error_details:(Informative loc) ty1 ty2
|> record_trace (Bad_stack_item lvl)
>>? fun (eq, ctxt) ->
eq >>? fun Eq ->
stack_eq loc ctxt (lvl + 1) rest1 rest2 >|? fun (Eq, ctxt) ->
((Eq : ((ta, ts) stack_ty, (tb, tu) stack_ty) eq), ctxt)
| _, _ -> error Bad_stack_length
(* ---- Type checker results -------------------------------------------------*)
type ('a, 's) judgement =
| Typed : ('a, 's, 'b, 'u) descr -> ('a, 's) judgement
| Failed : {
descr : 'b 'u. ('b, 'u) stack_ty -> ('a, 's, 'b, 'u) descr;
}
-> ('a, 's) judgement
(* ---- Type checker (Untyped expressions -> Typed IR) ----------------------*)
type ('a, 's, 'b, 'u, 'c, 'v) branch = {
branch :
'r 'f.
('a, 's, 'r, 'f) descr -> ('b, 'u, 'r, 'f) descr -> ('c, 'v, 'r, 'f) descr;
}
[@@unboxed]
let merge_branches :
type a s b u c v.
context ->
Script.location ->
(a, s) judgement ->
(b, u) judgement ->
(a, s, b, u, c, v) branch ->
((c, v) judgement * context) tzresult =
fun ctxt loc btr bfr {branch} ->
match (btr, bfr) with
| Typed ({aft = aftbt; _} as dbt), Typed ({aft = aftbf; _} as dbf) ->
let unmatched_branches () =
let aftbt = serialize_stack_for_error ctxt aftbt in
let aftbf = serialize_stack_for_error ctxt aftbf in
Unmatched_branches (loc, aftbt, aftbf)
in
record_trace_eval
unmatched_branches
( stack_eq loc ctxt 1 aftbt aftbf >|? fun (Eq, ctxt) ->
(Typed (branch dbt dbf), ctxt) )
| Failed {descr = descrt}, Failed {descr = descrf} ->
let descr ret = branch (descrt ret) (descrf ret) in
ok (Failed {descr}, ctxt)
| Typed dbt, Failed {descr = descrf} ->
ok (Typed (branch dbt (descrf dbt.aft)), ctxt)
| Failed {descr = descrt}, Typed dbf ->
ok (Typed (branch (descrt dbf.aft) dbf), ctxt)
let parse_memo_size (n : (location, _) Micheline.node) :
Sapling.Memo_size.t tzresult =
match n with
| Int (_, z) -> (
match Sapling.Memo_size.parse_z z with
| Ok _ as ok_memo_size -> ok_memo_size
| Error msg ->
error
@@ Invalid_syntactic_constant (location n, strip_locations n, msg))
| _ -> error @@ Invalid_kind (location n, [Int_kind], kind n)
type ex_comparable_ty =
| Ex_comparable_ty : 'a comparable_ty -> ex_comparable_ty
type ex_parameter_ty_and_entrypoints_node =
| Ex_parameter_ty_and_entrypoints_node : {
arg_type : ('a, _) ty;
entrypoints : 'a entrypoints_node;
}
-> ex_parameter_ty_and_entrypoints_node
(** [parse_ty] can be used to parse regular types as well as parameter types
together with their entrypoints.
In the first case, use [~ret:Don't_parse_entrypoints], [parse_ty] will
return an [ex_ty].
In the second case, use [~ret:Parse_entrypoints], [parse_ty] will return
an [ex_parameter_ty_and_entrypoints_node].
*)
type ('ret, 'name) parse_ty_ret =
| Don't_parse_entrypoints : (ex_ty, unit) parse_ty_ret
| Parse_entrypoints
: (ex_parameter_ty_and_entrypoints_node, Entrypoint.t option) parse_ty_ret
let rec parse_ty :
type ret name.
context ->
stack_depth:int ->
legacy:bool ->
allow_lazy_storage:bool ->
allow_operation:bool ->
allow_contract:bool ->
allow_ticket:bool ->
ret:(ret, name) parse_ty_ret ->
Script.node ->
(ret * context) tzresult =
fun ctxt
~stack_depth
~legacy
~allow_lazy_storage
~allow_operation
~allow_contract
~allow_ticket
~ret
node ->
Gas.consume ctxt Typecheck_costs.parse_type_cycle >>? fun ctxt ->
if Compare.Int.(stack_depth > 10000) then
error Typechecking_too_many_recursive_calls
else
(match ret with
| Don't_parse_entrypoints -> ok (node, (() : name))
| Parse_entrypoints -> extract_entrypoint_annot node)
>>? fun (node, name) ->
let return ctxt ty : ret * context =
match ret with
| Don't_parse_entrypoints -> (Ex_ty ty, ctxt)
| Parse_entrypoints ->
let at_node =
Option.map (fun name -> {name; original_type_expr = node}) name
in
( Ex_parameter_ty_and_entrypoints_node
{
arg_type = ty;
entrypoints = {at_node; nested = Entrypoints_None};
},
ctxt )
in
match node with
| Prim (loc, T_unit, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt unit_t
| Prim (loc, T_int, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt int_t
| Prim (loc, T_nat, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt nat_t
| Prim (loc, T_string, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt string_t
| Prim (loc, T_bytes, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt bytes_t
| Prim (loc, T_mutez, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt mutez_t
| Prim (loc, T_bool, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt bool_t
| Prim (loc, T_key, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt key_t
| Prim (loc, T_key_hash, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt key_hash_t
| Prim (loc, T_chest_key, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt chest_key_t
| Prim (loc, T_chest, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt chest_t
| Prim (loc, T_timestamp, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt timestamp_t
| Prim (loc, T_address, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt address_t
| Prim (loc, T_tx_rollup_l2_address, [], annot) ->
if Constants.tx_rollup_enable ctxt then
check_type_annot loc annot >|? fun () ->
return ctxt tx_rollup_l2_address_t
else error @@ Tx_rollup_addresses_disabled loc
| Prim (loc, T_signature, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt signature_t
| Prim (loc, T_operation, [], annot) ->
if allow_operation then
check_type_annot loc annot >|? fun () -> return ctxt operation_t
else error (Unexpected_operation loc)
| Prim (loc, T_chain_id, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt chain_id_t
| Prim (loc, T_never, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt never_t
| Prim (loc, T_bls12_381_g1, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt bls12_381_g1_t
| Prim (loc, T_bls12_381_g2, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt bls12_381_g2_t
| Prim (loc, T_bls12_381_fr, [], annot) ->
check_type_annot loc annot >|? fun () -> return ctxt bls12_381_fr_t
| Prim (loc, T_contract, [utl], annot) ->
if allow_contract then
parse_passable_ty
ctxt
~stack_depth:(stack_depth + 1)
~legacy
utl
~ret:Don't_parse_entrypoints
>>? fun (Ex_ty tl, ctxt) ->
check_type_annot loc annot >>? fun () ->
contract_t loc tl >|? fun ty -> return ctxt ty
else error (Unexpected_contract loc)
| Prim (loc, T_pair, utl :: utr, annot) ->
remove_field_annot utl >>? fun utl ->
parse_ty
ctxt
~stack_depth:(stack_depth + 1)
~legacy
~allow_lazy_storage
~allow_operation
~allow_contract
~allow_ticket
~ret:Don't_parse_entrypoints
utl
>>? fun (Ex_ty tl, ctxt) ->
(match utr with
| [utr] -> remove_field_annot utr
| utr ->
(* Unfold [pair t1 ... tn] as [pair t1 (... (pair tn-1 tn))] *)
ok (Prim (loc, T_pair, utr, [])))
>>? fun utr ->
parse_ty
ctxt
~stack_depth:(stack_depth + 1)
~legacy
~allow_lazy_storage
~allow_operation
~allow_contract
~allow_ticket
~ret:Don't_parse_entrypoints
utr
>>? fun (Ex_ty tr, ctxt) ->
check_type_annot loc annot >>? fun () ->
pair_t loc tl tr >|? fun (Ty_ex_c ty) -> return ctxt ty
| Prim (loc, T_or, [utl; utr], annot) -> (
(match ret with
| Don't_parse_entrypoints ->
remove_field_annot utl >>? fun utl ->
remove_field_annot utr >|? fun utr -> (utl, utr)
| Parse_entrypoints -> ok (utl, utr))
>>? fun (utl, utr) ->
parse_ty
ctxt
~stack_depth:(stack_depth + 1)
~legacy
~allow_lazy_storage
~allow_operation
~allow_contract
~allow_ticket
~ret
utl
>>? fun (parsed_l, ctxt) ->
parse_ty
ctxt
~stack_depth:(stack_depth + 1)
~legacy
~allow_lazy_storage
~allow_operation
~allow_contract
~allow_ticket
~ret
utr
>>? fun (parsed_r, ctxt) ->
check_type_annot loc annot >>? fun () ->
match ret with
| Don't_parse_entrypoints ->
let (Ex_ty tl) = parsed_l in
let (Ex_ty tr) = parsed_r in
union_t loc tl tr >|? fun (Ty_ex_c ty) -> ((Ex_ty ty : ret), ctxt)
| Parse_entrypoints ->
let (Ex_parameter_ty_and_entrypoints_node
{arg_type = tl; entrypoints = left}) =
parsed_l
in
let (Ex_parameter_ty_and_entrypoints_node
{arg_type = tr; entrypoints = right}) =
parsed_r
in
union_t loc tl tr >|? fun (Ty_ex_c arg_type) ->
let entrypoints =
let at_node =
Option.map (fun name -> {name; original_type_expr = node}) name
in
{at_node; nested = Entrypoints_Union {left; right}}
in
(Ex_parameter_ty_and_entrypoints_node {arg_type; entrypoints}, ctxt)
)
| Prim (loc, T_lambda, [uta; utr], annot) ->
parse_any_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy uta
>>? fun (Ex_ty ta, ctxt) ->
parse_any_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy utr
>>? fun (Ex_ty tr, ctxt) ->
check_type_annot loc annot >>? fun () ->
lambda_t loc ta tr >|? fun ty -> return ctxt ty
| Prim (loc, T_option, [ut], annot) ->
(if legacy then
(* legacy semantics with (broken) field annotations *)
remove_field_annot ut >>? fun ut ->
check_composed_type_annot loc annot >>? fun () -> ok ut
else check_type_annot loc annot >>? fun () -> ok ut)
>>? fun ut ->
parse_ty
ctxt
~stack_depth:(stack_depth + 1)
~legacy
~allow_lazy_storage
~allow_operation
~allow_contract
~allow_ticket
~ret:Don't_parse_entrypoints
ut
>>? fun (Ex_ty t, ctxt) ->
option_t loc t >|? fun ty -> return ctxt ty
| Prim (loc, T_list, [ut], annot) ->
parse_ty
ctxt
~stack_depth:(stack_depth + 1)
~legacy
~allow_lazy_storage
~allow_operation
~allow_contract
~allow_ticket
~ret:Don't_parse_entrypoints
ut
>>? fun (Ex_ty t, ctxt) ->
check_type_annot loc annot >>? fun () ->
list_t loc t >|? fun ty -> return ctxt ty
| Prim (loc, T_ticket, [ut], annot) ->
if allow_ticket then
parse_comparable_ty ~stack_depth:(stack_depth + 1) ctxt ut
>>? fun (Ex_comparable_ty t, ctxt) ->
check_type_annot loc annot >>? fun () ->
ticket_t loc t >|? fun ty -> return ctxt ty
else error (Unexpected_ticket loc)
| Prim (loc, T_set, [ut], annot) ->
parse_comparable_ty ~stack_depth:(stack_depth + 1) ctxt ut
>>? fun (Ex_comparable_ty t, ctxt) ->
check_type_annot loc annot >>? fun () ->
set_t loc t >|? fun ty -> return ctxt ty
| Prim (loc, T_map, [uta; utr], annot) ->
parse_comparable_ty ~stack_depth:(stack_depth + 1) ctxt uta
>>? fun (Ex_comparable_ty ta, ctxt) ->
parse_ty
ctxt
~stack_depth:(stack_depth + 1)
~legacy
~allow_lazy_storage
~allow_operation
~allow_contract
~allow_ticket
~ret:Don't_parse_entrypoints
utr
>>? fun (Ex_ty tr, ctxt) ->
check_type_annot loc annot >>? fun () ->
map_t loc ta tr >|? fun ty -> return ctxt ty
| Prim (loc, T_sapling_transaction, [memo_size], annot) ->
check_type_annot loc annot >>? fun () ->
parse_memo_size memo_size >|? fun memo_size ->
return ctxt (sapling_transaction_t ~memo_size)
| Prim (loc, T_sapling_transaction_deprecated, [memo_size], annot) ->
if legacy then
check_type_annot loc annot >>? fun () ->
parse_memo_size memo_size >|? fun memo_size ->
return ctxt (sapling_transaction_deprecated_t ~memo_size)
else error (Deprecated_instruction T_sapling_transaction_deprecated)
(*
/!\ When adding new lazy storage kinds, be careful to use
[when allow_lazy_storage] /!\
Lazy storage should not be packable to avoid stealing a lazy storage
from another contract with `PUSH t id` or `UNPACK`.
*)
| Prim (loc, T_big_map, args, annot) when allow_lazy_storage ->
parse_big_map_ty
ctxt
~stack_depth:(stack_depth + 1)
~legacy
loc
args
annot
>|? fun (Ex_ty ty, ctxt) -> return ctxt ty
| Prim (loc, T_sapling_state, [memo_size], annot) when allow_lazy_storage ->
check_type_annot loc annot >>? fun () ->
parse_memo_size memo_size >|? fun memo_size ->
return ctxt (sapling_state_t ~memo_size)
| Prim (loc, (T_big_map | T_sapling_state), _, _) ->
error (Unexpected_lazy_storage loc)
| Prim
( loc,
(( T_unit | T_signature | T_int | T_nat | T_string | T_bytes | T_mutez
| T_bool | T_key | T_key_hash | T_timestamp | T_address
| T_tx_rollup_l2_address | T_chain_id | T_operation | T_never ) as
prim),
l,
_ ) ->
error (Invalid_arity (loc, prim, 0, List.length l))
| Prim
( loc,
((T_set | T_list | T_option | T_contract | T_ticket) as prim),
l,
_ ) ->
error (Invalid_arity (loc, prim, 1, List.length l))
| Prim (loc, ((T_pair | T_or | T_map | T_lambda) as prim), l, _) ->
error (Invalid_arity (loc, prim, 2, List.length l))
| expr ->
error
@@ unexpected
expr
[]
Type_namespace
[
T_bls12_381_fr;
T_bls12_381_g1;
T_bls12_381_g2;
T_bool;
T_bytes;
T_chain_id;
T_contract;
T_int;
T_key;
T_key_hash;
T_lambda;
T_list;
T_map;
T_mutez;
T_nat;
T_never;
T_operation;
T_option;
T_or;
T_pair;
T_set;
T_signature;
T_string;
T_ticket;
T_timestamp;
T_tx_rollup_l2_address;
T_unit;
]
and parse_comparable_ty :
context ->
stack_depth:int ->
Script.node ->
(ex_comparable_ty * context) tzresult =
fun ctxt ~stack_depth node ->
parse_ty
~ret:Don't_parse_entrypoints
ctxt
~stack_depth:(stack_depth + 1)
~legacy:false
~allow_lazy_storage:false
~allow_operation:false
~allow_contract:false
~allow_ticket:false
node
>>? fun (Ex_ty t, ctxt) ->
match is_comparable t with
| Yes -> ok (Ex_comparable_ty t, ctxt)
| No ->
error
(Comparable_type_expected (location node, Micheline.strip_locations node))
and parse_passable_ty :
type ret name.
context ->
stack_depth:int ->
legacy:bool ->
ret:(ret, name) parse_ty_ret ->
Script.node ->
(ret * context) tzresult =
fun ctxt ~stack_depth ~legacy ->
(parse_ty [@tailcall])
ctxt
~stack_depth
~legacy
~allow_lazy_storage:true
~allow_operation:false
~allow_contract:true
~allow_ticket:true
and parse_any_ty :
context ->
stack_depth:int ->
legacy:bool ->
Script.node ->
(ex_ty * context) tzresult =
fun ctxt ~stack_depth ~legacy ->
(parse_ty [@tailcall])
ctxt
~stack_depth
~legacy
~allow_lazy_storage:true
~allow_operation:true
~allow_contract:true
~allow_ticket:true
~ret:Don't_parse_entrypoints
and parse_big_map_ty ctxt ~stack_depth ~legacy big_map_loc args map_annot =
Gas.consume ctxt Typecheck_costs.parse_type_cycle >>? fun ctxt ->
match args with
| [key_ty; value_ty] ->
parse_comparable_ty ~stack_depth:(stack_depth + 1) ctxt key_ty
>>? fun (Ex_comparable_ty key_ty, ctxt) ->
parse_big_map_value_ty
ctxt
~stack_depth:(stack_depth + 1)
~legacy
value_ty
>>? fun (Ex_ty value_ty, ctxt) ->
check_type_annot big_map_loc map_annot >>? fun () ->
big_map_t big_map_loc key_ty value_ty >|? fun big_map_ty ->
(Ex_ty big_map_ty, ctxt)
| args -> error @@ Invalid_arity (big_map_loc, T_big_map, 2, List.length args)
and parse_big_map_value_ty ctxt ~stack_depth ~legacy value_ty =
(parse_ty [@tailcall])
ctxt
~stack_depth
~legacy
~allow_lazy_storage:false
~allow_operation:false
~allow_contract:legacy
~allow_ticket:true
~ret:Don't_parse_entrypoints
value_ty
let parse_packable_ty ctxt ~stack_depth ~legacy node =
(parse_ty [@tailcall])
ctxt
~stack_depth
~legacy
~allow_lazy_storage:false
~allow_operation:false
~allow_contract:legacy
(* type contract is forbidden in UNPACK because of
https://gitlab.com/tezos/tezos/-/issues/301 *)
~allow_ticket:false
~ret:Don't_parse_entrypoints
node
let parse_view_input_ty ctxt ~stack_depth ~legacy node =
(parse_ty [@tailcall])
ctxt
~stack_depth
~legacy
~allow_lazy_storage:false
~allow_operation:false
~allow_contract:true
~allow_ticket:false
~ret:Don't_parse_entrypoints
node
let parse_view_output_ty ctxt ~stack_depth ~legacy node =
(parse_ty [@tailcall])
ctxt
~stack_depth
~legacy
~allow_lazy_storage:false
~allow_operation:false
~allow_contract:true
~allow_ticket:false
~ret:Don't_parse_entrypoints
node
let parse_normal_storage_ty ctxt ~stack_depth ~legacy node =
(parse_ty [@tailcall])
ctxt
~stack_depth
~legacy
~allow_lazy_storage:true
~allow_operation:false
~allow_contract:legacy
~allow_ticket:true
~ret:Don't_parse_entrypoints
node
let parse_storage_ty :
context ->
stack_depth:int ->
legacy:bool ->
Script.node ->
(ex_ty * context) tzresult =
fun ctxt ~stack_depth ~legacy node ->
match node with
| Prim
( loc,
T_pair,
[Prim (big_map_loc, T_big_map, args, map_annot); remaining_storage],
storage_annot )
when legacy -> (
match storage_annot with
| [] ->
(parse_normal_storage_ty [@tailcall]) ctxt ~stack_depth ~legacy node
| [single]
when Compare.Int.(String.length single > 0)
&& Compare.Char.(single.[0] = '%') ->
(parse_normal_storage_ty [@tailcall]) ctxt ~stack_depth ~legacy node
| _ ->
(* legacy semantics of big maps used the wrong annotation parser *)
Gas.consume ctxt Typecheck_costs.parse_type_cycle >>? fun ctxt ->
parse_big_map_ty
ctxt
~stack_depth:(stack_depth + 1)
~legacy
big_map_loc
args
map_annot
>>? fun (Ex_ty big_map_ty, ctxt) ->
parse_normal_storage_ty
ctxt
~stack_depth:(stack_depth + 1)
~legacy
remaining_storage
>>? fun (Ex_ty remaining_storage, ctxt) ->
check_composed_type_annot loc storage_annot >>? fun () ->
pair_t loc big_map_ty remaining_storage >|? fun (Ty_ex_c ty) ->
(Ex_ty ty, ctxt))
| _ -> (parse_normal_storage_ty [@tailcall]) ctxt ~stack_depth ~legacy node
(* check_packable: determine if a `ty` is packable into Michelson *)
let check_packable ~legacy loc root =
let rec check : type t tc. (t, tc) ty -> unit tzresult = function
(* /!\ When adding new lazy storage kinds, be sure to return an error. /!\
Lazy storage should not be packable. *)
| Big_map_t _ -> error (Unexpected_lazy_storage loc)
| Sapling_state_t _ -> error (Unexpected_lazy_storage loc)
| Operation_t -> error (Unexpected_operation loc)
| Unit_t -> Result.return_unit
| Int_t -> Result.return_unit
| Nat_t -> Result.return_unit
| Signature_t -> Result.return_unit
| String_t -> Result.return_unit
| Bytes_t -> Result.return_unit
| Mutez_t -> Result.return_unit
| Key_hash_t -> Result.return_unit
| Key_t -> Result.return_unit
| Timestamp_t -> Result.return_unit
| Address_t -> Result.return_unit
| Tx_rollup_l2_address_t -> Result.return_unit
| Bool_t -> Result.return_unit
| Chain_id_t -> Result.return_unit
| Never_t -> Result.return_unit
| Set_t (_, _) -> Result.return_unit
| Ticket_t _ -> error (Unexpected_ticket loc)
| Lambda_t (_, _, _) -> Result.return_unit
| Bls12_381_g1_t -> Result.return_unit
| Bls12_381_g2_t -> Result.return_unit
| Bls12_381_fr_t -> Result.return_unit
| Pair_t (l_ty, r_ty, _, _) -> check l_ty >>? fun () -> check r_ty
| Union_t (l_ty, r_ty, _, _) -> check l_ty >>? fun () -> check r_ty
| Option_t (v_ty, _, _) -> check v_ty
| List_t (elt_ty, _) -> check elt_ty
| Map_t (_, elt_ty, _) -> check elt_ty
| Contract_t (_, _) when legacy -> Result.return_unit
| Contract_t (_, _) -> error (Unexpected_contract loc)
| Sapling_transaction_t _ -> ok ()
| Sapling_transaction_deprecated_t _ -> ok ()
| Chest_key_t -> Result.return_unit
| Chest_t -> Result.return_unit
in
check root
type toplevel = {
code_field : Script.node;
arg_type : Script.node;
storage_type : Script.node;
views : view_map;
}
type ('arg, 'storage) code =
| Code : {
code :
(('arg, 'storage) pair, (operation boxed_list, 'storage) pair) lambda;
arg_type : ('arg, _) ty;
storage_type : ('storage, _) ty;
views : view_map;
entrypoints : 'arg entrypoints;
code_size : Cache_memory_helpers.sint;
}
-> ('arg, 'storage) code
type ex_script = Ex_script : ('a, 'c) Script_typed_ir.script -> ex_script
type ex_code = Ex_code : ('a, 'c) code -> ex_code
type 'storage typed_view =
| Typed_view : {
input_ty : ('input, _) ty;
output_ty : ('output, _) ty;
kinstr : ('input * 'storage, end_of_stack, 'output, end_of_stack) kinstr;
original_code_expr : Script.node;
}
-> 'storage typed_view
type 'storage typed_view_map = (Script_string.t, 'storage typed_view) map
type (_, _) dig_proof_argument =
| Dig_proof_argument :
('x, 'a * 's, 'a, 's, 'b, 't, 'c, 'u) stack_prefix_preservation_witness
* ('x, _) ty
* ('c, 'u) stack_ty
-> ('b, 't) dig_proof_argument
type (_, _, _) dug_proof_argument =
| Dug_proof_argument :
(('a, 's, 'x, 'a * 's, 'b, 't, 'c, 'u) stack_prefix_preservation_witness
* ('c, 'u) stack_ty)
-> ('b, 't, 'x) dug_proof_argument
type (_, _) dipn_proof_argument =
| Dipn_proof_argument :
('fa, 'fs, 'fb, 'fu, 'a, 's, 'b, 'u) stack_prefix_preservation_witness
* context
* ('fa, 'fs, 'fb, 'fu) descr
* ('b, 'u) stack_ty
-> ('a, 's) dipn_proof_argument
type (_, _) dropn_proof_argument =
| Dropn_proof_argument :
('fa, 'fs, 'fa, 'fs, 'a, 's, 'a, 's) stack_prefix_preservation_witness
* ('fa, 'fs) stack_ty
-> ('a, 's) dropn_proof_argument
type (_, _, _) comb_proof_argument =
| Comb_proof_argument :
('a, 'b, 's, 'c, 'd, 't) comb_gadt_witness * ('c, 'd * 't) stack_ty
-> ('a, 'b, 's) comb_proof_argument
type (_, _, _) uncomb_proof_argument =
| Uncomb_proof_argument :
('a, 'b, 's, 'c, 'd, 't) uncomb_gadt_witness * ('c, 'd * 't) stack_ty
-> ('a, 'b, 's) uncomb_proof_argument
type 'before comb_get_proof_argument =
| Comb_get_proof_argument :
('before, 'after) comb_get_gadt_witness * ('after, _) ty
-> 'before comb_get_proof_argument
type ('rest, 'before) comb_set_proof_argument =
| Comb_set_proof_argument :
('rest, 'before, 'after) comb_set_gadt_witness * ('after, _) ty
-> ('rest, 'before) comb_set_proof_argument
type (_, _, _) dup_n_proof_argument =
| Dup_n_proof_argument :
('a, 'b, 's, 't) dup_n_gadt_witness * ('t, _) ty
-> ('a, 'b, 's) dup_n_proof_argument
let rec make_dug_proof_argument :
type a s x xc.
location ->
int ->
(x, xc) ty ->
(a, s) stack_ty ->
(a, s, x) dug_proof_argument option =
fun loc n x stk ->
match (n, stk) with
| 0, rest -> Some (Dug_proof_argument (KRest, Item_t (x, rest)))
| n, Item_t (v, rest) ->
make_dug_proof_argument loc (n - 1) x rest
|> Option.map @@ fun (Dug_proof_argument (n', aft')) ->
Dug_proof_argument (KPrefix (loc, v, n'), Item_t (v, aft'))
| _, _ -> None
let rec make_comb_get_proof_argument :
type b bc. int -> (b, bc) ty -> b comb_get_proof_argument option =
fun n ty ->
match (n, ty) with
| 0, value_ty -> Some (Comb_get_proof_argument (Comb_get_zero, value_ty))
| 1, Pair_t (hd_ty, _, _annot, _) ->
Some (Comb_get_proof_argument (Comb_get_one, hd_ty))
| n, Pair_t (_, tl_ty, _annot, _) ->
make_comb_get_proof_argument (n - 2) tl_ty
|> Option.map
@@ fun (Comb_get_proof_argument (comb_get_left_witness, ty')) ->
Comb_get_proof_argument (Comb_get_plus_two comb_get_left_witness, ty')
| _ -> None
let rec make_comb_set_proof_argument :
type value valuec before beforec a s.
context ->
(a, s) stack_ty ->
location ->
int ->
(value, valuec) ty ->
(before, beforec) ty ->
(value, before) comb_set_proof_argument tzresult =
fun ctxt stack_ty loc n value_ty ty ->
match (n, ty) with
| 0, _ -> ok @@ Comb_set_proof_argument (Comb_set_zero, value_ty)
| 1, Pair_t (_hd_ty, tl_ty, _, _) ->
pair_t loc value_ty tl_ty >|? fun (Ty_ex_c after_ty) ->
Comb_set_proof_argument (Comb_set_one, after_ty)
| n, Pair_t (hd_ty, tl_ty, _, _) ->
make_comb_set_proof_argument ctxt stack_ty loc (n - 2) value_ty tl_ty
>>? fun (Comb_set_proof_argument (comb_set_left_witness, tl_ty')) ->
pair_t loc hd_ty tl_ty' >|? fun (Ty_ex_c after_ty) ->
Comb_set_proof_argument (Comb_set_plus_two comb_set_left_witness, after_ty)
| _ ->
let whole_stack = serialize_stack_for_error ctxt stack_ty in
error (Bad_stack (loc, I_UPDATE, 2, whole_stack))
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
let find_entrypoint (type full fullc error_context error_trace)
~(error_details : (error_context, error_trace) error_details)
(full : (full, fullc) ty) (entrypoints : full entrypoints) entrypoint :
(full ex_ty_cstr, error_trace) Gas_monad.t =
let open Gas_monad.Syntax in
let rec find_entrypoint :
type t tc.
(t, tc) ty ->
t entrypoints_node ->
Entrypoint.t ->
(t ex_ty_cstr, unit) Gas_monad.t =
fun ty entrypoints entrypoint ->
let* () = Gas_monad.consume_gas Typecheck_costs.find_entrypoint_cycle in
match (ty, entrypoints) with
| _, {at_node = Some {name; original_type_expr}; _}
when Entrypoint.(name = entrypoint) ->
return (Ex_ty_cstr {ty; construct = (fun e -> e); original_type_expr})
| Union_t (tl, tr, _, _), {nested = Entrypoints_Union {left; right}; _} -> (
Gas_monad.bind_recover (find_entrypoint tl left entrypoint) @@ function
| Ok (Ex_ty_cstr {ty; construct; original_type_expr}) ->
return
(Ex_ty_cstr
{
ty;
construct = (fun e -> L (construct e));
original_type_expr;
})
| Error () ->
let+ (Ex_ty_cstr {ty; construct; original_type_expr}) =
find_entrypoint tr right entrypoint
in
Ex_ty_cstr
{ty; construct = (fun e -> R (construct e)); original_type_expr})
| _, {nested = Entrypoints_None; _} -> Gas_monad.of_result (Error ())
in
let {root; original_type_expr} = entrypoints in
Gas_monad.bind_recover (find_entrypoint full root entrypoint) @@ function
| Ok f_t -> return f_t
| Error () ->
if Entrypoint.is_default entrypoint then
return
(Ex_ty_cstr {ty = full; construct = (fun e -> e); original_type_expr})
else
Gas_monad.of_result
@@ Error
(match error_details with
| Fast -> (Inconsistent_types_fast : error_trace)
| Informative _ -> trace_of_error @@ No_such_entrypoint entrypoint)
let find_entrypoint_for_type (type full fullc exp expc error_trace)
~error_details ~(full : (full, fullc) ty) ~(expected : (exp, expc) ty)
entrypoints entrypoint :
(Entrypoint.t * (exp, expc) ty, error_trace) Gas_monad.t =
let open Gas_monad.Syntax in
let* res = find_entrypoint ~error_details full entrypoints entrypoint in
match res with
| Ex_ty_cstr {ty; _} -> (
match entrypoints.root.at_node with
| Some {name; original_type_expr = _}
when Entrypoint.is_root name && Entrypoint.is_default entrypoint ->
Gas_monad.bind_recover
(ty_eq ~error_details:Fast ty expected)
(function
| Ok Eq -> return (Entrypoint.default, (ty : (exp, expc) ty))
| Error Inconsistent_types_fast ->
let+ Eq = ty_eq ~error_details full expected in
(Entrypoint.root, (full : (exp, expc) ty)))
| _ ->
let+ Eq = ty_eq ~error_details ty expected in
(entrypoint, (ty : (exp, expc) ty)))
let well_formed_entrypoints (type full fullc) (full : (full, fullc) ty)
entrypoints =
let merge path (type t tc) (ty : (t, tc) ty)
(entrypoints : t entrypoints_node) reachable
((first_unreachable, all) as acc) =
match entrypoints.at_node with
| None ->
ok
( (if reachable then acc
else
match ty with
| Union_t _ -> acc
| _ -> (
match first_unreachable with
| None -> (Some (List.rev path), all)
| Some _ -> acc)),
reachable )
| Some {name; original_type_expr = _} ->
if Entrypoint.Set.mem name all then error (Duplicate_entrypoint name)
else ok ((first_unreachable, Entrypoint.Set.add name all), true)
in
let rec check :
type t tc.
(t, tc) ty ->
t entrypoints_node ->
prim list ->
bool ->
prim list option * Entrypoint.Set.t ->
(prim list option * Entrypoint.Set.t) tzresult =
fun t entrypoints path reachable acc ->
match (t, entrypoints) with
| Union_t (tl, tr, _, _), {nested = Entrypoints_Union {left; right}; _} ->
merge (D_Left :: path) tl left reachable acc
>>? fun (acc, l_reachable) ->
merge (D_Right :: path) tr right reachable acc
>>? fun (acc, r_reachable) ->
check tl left (D_Left :: path) l_reachable acc >>? fun acc ->
check tr right (D_Right :: path) r_reachable acc
| _ -> ok acc
in
let init, reachable =
match entrypoints.at_node with
| None -> (Entrypoint.Set.empty, false)
| Some {name; original_type_expr = _} ->
(Entrypoint.Set.singleton name, true)
in
check full entrypoints [] reachable (None, init)
>>? fun (first_unreachable, all) ->
if not (Entrypoint.Set.mem Entrypoint.default all) then Result.return_unit
else
match first_unreachable with
| None -> Result.return_unit
| Some path -> error (Unreachable_entrypoint path)
type ex_parameter_ty_and_entrypoints =
| Ex_parameter_ty_and_entrypoints : {
arg_type : ('a, _) ty;
entrypoints : 'a entrypoints;
}
-> ex_parameter_ty_and_entrypoints
let parse_parameter_ty_and_entrypoints :
context ->
stack_depth:int ->
legacy:bool ->
Script.node ->
(ex_parameter_ty_and_entrypoints * context) tzresult =
fun ctxt ~stack_depth ~legacy node ->
parse_passable_ty
ctxt
~stack_depth:(stack_depth + 1)
~legacy
node
~ret:Parse_entrypoints
>>? fun (Ex_parameter_ty_and_entrypoints_node {arg_type; entrypoints}, ctxt)
->
(if legacy then Result.return_unit
else well_formed_entrypoints arg_type entrypoints)
>|? fun () ->
let entrypoints = {root = entrypoints; original_type_expr = node} in
(Ex_parameter_ty_and_entrypoints {arg_type; entrypoints}, ctxt)
let parse_passable_ty = parse_passable_ty ~ret:Don't_parse_entrypoints
let parse_uint ~nb_bits =
assert (Compare.Int.(nb_bits >= 0 && nb_bits <= 30)) ;
let max_int = (1 lsl nb_bits) - 1 in
let max_z = Z.of_int max_int in
function
| Micheline.Int (_, n) when Compare.Z.(Z.zero <= n) && Compare.Z.(n <= max_z)
->
ok (Z.to_int n)
| node ->
error
@@ Invalid_syntactic_constant
( location node,
strip_locations node,
"a positive " ^ string_of_int nb_bits
^ "-bit integer (between 0 and " ^ string_of_int max_int ^ ")" )
let parse_uint10 = parse_uint ~nb_bits:10
let parse_uint11 = parse_uint ~nb_bits:11
(* The type returned by this function is used to:
- serialize and deserialize tickets when they are stored or transferred,
- type the READ_TICKET instruction. *)
let opened_ticket_type loc ty = comparable_pair_3_t loc address_t ty nat_t
(* -- parse data of primitive types -- *)
let parse_unit ctxt ~legacy = function
| Prim (loc, D_Unit, [], annot) ->
(if legacy then Result.return_unit else error_unexpected_annot loc annot)
>>? fun () ->
Gas.consume ctxt Typecheck_costs.unit >|? fun ctxt -> ((), ctxt)
| Prim (loc, D_Unit, l, _) ->
error @@ Invalid_arity (loc, D_Unit, 0, List.length l)
| expr -> error @@ unexpected expr [] Constant_namespace [D_Unit]
let parse_bool ctxt ~legacy = function
| Prim (loc, D_True, [], annot) ->
(if legacy then Result.return_unit else error_unexpected_annot loc annot)
>>? fun () ->
Gas.consume ctxt Typecheck_costs.bool >|? fun ctxt -> (true, ctxt)
| Prim (loc, D_False, [], annot) ->
(if legacy then Result.return_unit else error_unexpected_annot loc annot)
>>? fun () ->
Gas.consume ctxt Typecheck_costs.bool >|? fun ctxt -> (false, ctxt)
| Prim (loc, ((D_True | D_False) as c), l, _) ->
error @@ Invalid_arity (loc, c, 0, List.length l)
| expr -> error @@ unexpected expr [] Constant_namespace [D_True; D_False]
let parse_string ctxt : Script.node -> (Script_string.t * context) tzresult =
function
| String (loc, v) as expr ->
Gas.consume ctxt (Typecheck_costs.check_printable v) >>? fun ctxt ->
record_trace
(Invalid_syntactic_constant
(loc, strip_locations expr, "a printable ascii string"))
(Script_string.of_string v >|? fun s -> (s, ctxt))
| expr -> error @@ Invalid_kind (location expr, [String_kind], kind expr)
let parse_bytes ctxt = function
| Bytes (_, v) -> ok (v, ctxt)
| expr -> error @@ Invalid_kind (location expr, [Bytes_kind], kind expr)
let parse_int ctxt = function
| Int (_, v) -> ok (Script_int.of_zint v, ctxt)
| expr -> error @@ Invalid_kind (location expr, [Int_kind], kind expr)
let parse_nat ctxt :
Script.node -> (Script_int.n Script_int.num * context) tzresult = function
| Int (loc, v) as expr -> (
let v = Script_int.of_zint v in
match Script_int.is_nat v with
| Some nat -> ok (nat, ctxt)
| None ->
error
@@ Invalid_syntactic_constant
(loc, strip_locations expr, "a non-negative integer"))
| expr -> error @@ Invalid_kind (location expr, [Int_kind], kind expr)
let parse_mutez ctxt : Script.node -> (Tez.t * context) tzresult = function
| Int (loc, v) as expr -> (
match
let open Option in
bind (catch (fun () -> Z.to_int64 v)) Tez.of_mutez
with
| Some tez -> Ok (tez, ctxt)
| None ->
error
@@ Invalid_syntactic_constant
(loc, strip_locations expr, "a valid mutez amount"))
| expr -> error @@ Invalid_kind (location expr, [Int_kind], kind expr)
let parse_timestamp ctxt :
Script.node -> (Script_timestamp.t * context) tzresult = function
| Int (_, v) (* As unparsed with [Optimized] or out of bounds [Readable]. *)
->
ok (Script_timestamp.of_zint v, ctxt)
| String (loc, s) as expr (* As unparsed with [Readable]. *) -> (
Gas.consume ctxt (Typecheck_costs.timestamp_readable s) >>? fun ctxt ->
match Script_timestamp.of_string s with
| Some v -> ok (v, ctxt)
| None ->
error
@@ Invalid_syntactic_constant
(loc, strip_locations expr, "a valid timestamp"))
| expr ->
error @@ Invalid_kind (location expr, [String_kind; Int_kind], kind expr)
let parse_key ctxt : Script.node -> (public_key * context) tzresult = function
| Bytes (loc, bytes) as expr -> (
(* As unparsed with [Optimized]. *)
Gas.consume ctxt Typecheck_costs.public_key_optimized
>>? fun ctxt ->
match
Data_encoding.Binary.of_bytes_opt Signature.Public_key.encoding bytes
with
| Some k -> ok (k, ctxt)
| None ->
error
@@ Invalid_syntactic_constant
(loc, strip_locations expr, "a valid public key"))
| String (loc, s) as expr -> (
(* As unparsed with [Readable]. *)
Gas.consume ctxt Typecheck_costs.public_key_readable
>>? fun ctxt ->
match Signature.Public_key.of_b58check_opt s with
| Some k -> ok (k, ctxt)
| None ->
error
@@ Invalid_syntactic_constant
(loc, strip_locations expr, "a valid public key"))
| expr ->
error @@ Invalid_kind (location expr, [String_kind; Bytes_kind], kind expr)
let parse_key_hash ctxt : Script.node -> (public_key_hash * context) tzresult =
function
| Bytes (loc, bytes) as expr -> (
(* As unparsed with [Optimized]. *)
Gas.consume ctxt Typecheck_costs.key_hash_optimized
>>? fun ctxt ->
match
Data_encoding.Binary.of_bytes_opt
Signature.Public_key_hash.encoding
bytes
with
| Some k -> ok (k, ctxt)
| None ->
error
@@ Invalid_syntactic_constant
(loc, strip_locations expr, "a valid key hash"))
| String (loc, s) as expr (* As unparsed with [Readable]. *) -> (
Gas.consume ctxt Typecheck_costs.key_hash_readable >>? fun ctxt ->
match Signature.Public_key_hash.of_b58check_opt s with
| Some k -> ok (k, ctxt)
| None ->
error
@@ Invalid_syntactic_constant
(loc, strip_locations expr, "a valid key hash"))
| expr ->
error @@ Invalid_kind (location expr, [String_kind; Bytes_kind], kind expr)
let parse_signature ctxt : Script.node -> (signature * context) tzresult =
function
| Bytes (loc, bytes) as expr (* As unparsed with [Optimized]. *) -> (
Gas.consume ctxt Typecheck_costs.signature_optimized >>? fun ctxt ->
match
Data_encoding.Binary.of_bytes_opt Script_signature.encoding bytes
with
| Some k -> ok (k, ctxt)
| None ->
error
@@ Invalid_syntactic_constant
(loc, strip_locations expr, "a valid signature"))
| String (loc, s) as expr (* As unparsed with [Readable]. *) -> (
Gas.consume ctxt Typecheck_costs.signature_readable >>? fun ctxt ->
match Script_signature.of_b58check_opt s with
| Some s -> ok (s, ctxt)
| None ->
error
@@ Invalid_syntactic_constant
(loc, strip_locations expr, "a valid signature"))
| expr ->
error @@ Invalid_kind (location expr, [String_kind; Bytes_kind], kind expr)
let parse_chain_id ctxt : Script.node -> (Script_chain_id.t * context) tzresult
= function
| Bytes (loc, bytes) as expr -> (
Gas.consume ctxt Typecheck_costs.chain_id_optimized >>? fun ctxt ->
match
Data_encoding.Binary.of_bytes_opt Script_chain_id.encoding bytes
with
| Some k -> ok (k, ctxt)
| None ->
error
@@ Invalid_syntactic_constant
(loc, strip_locations expr, "a valid chain id"))
| String (loc, s) as expr -> (
Gas.consume ctxt Typecheck_costs.chain_id_readable >>? fun ctxt ->
match Script_chain_id.of_b58check_opt s with
| Some s -> ok (s, ctxt)
| None ->
error
@@ Invalid_syntactic_constant
(loc, strip_locations expr, "a valid chain id"))
| expr ->
error @@ Invalid_kind (location expr, [String_kind; Bytes_kind], kind expr)
let parse_address ctxt : Script.node -> (address * context) tzresult =
let destination_allowed loc {destination; entrypoint} ctxt =
match destination with
| Destination.Tx_rollup _ when not (Constants.tx_rollup_enable ctxt) ->
error @@ Tx_rollup_addresses_disabled loc
| Destination.Sc_rollup _ when not (Constants.sc_rollup_enable ctxt) ->
error @@ Sc_rollup_disabled loc
| _ -> Ok ({destination; entrypoint}, ctxt)
in
function
| Bytes (loc, bytes) as expr (* As unparsed with [Optimized]. *) -> (
Gas.consume ctxt Typecheck_costs.contract_optimized >>? fun ctxt ->
match
Data_encoding.Binary.of_bytes_opt
Data_encoding.(tup2 Destination.encoding Entrypoint.value_encoding)
bytes
with
| Some (destination, entrypoint) ->
destination_allowed loc {destination; entrypoint} ctxt
| None ->
error
@@ Invalid_syntactic_constant
(loc, strip_locations expr, "a valid address"))
| String (loc, s) (* As unparsed with [Readable]. *) ->
Gas.consume ctxt Typecheck_costs.contract_readable >>? fun ctxt ->
(match String.index_opt s '%' with
| None -> ok (s, Entrypoint.default)
| Some pos ->
let len = String.length s - pos - 1 in
let name = String.sub s (pos + 1) len in
Entrypoint.of_string_strict ~loc name >|? fun entrypoint ->
(String.sub s 0 pos, entrypoint))
>>? fun (addr, entrypoint) ->
Destination.of_b58check addr >>? fun destination ->
destination_allowed loc {destination; entrypoint} ctxt
| expr ->
error @@ Invalid_kind (location expr, [String_kind; Bytes_kind], kind expr)
let parse_tx_rollup_l2_address ctxt :
Script.node -> (tx_rollup_l2_address * context) tzresult = function
| Bytes (loc, bytes) as expr (* As unparsed with [Optimized]. *) -> (
Gas.consume ctxt Typecheck_costs.tx_rollup_l2_address >>? fun ctxt ->
match Tx_rollup_l2_address.of_bytes_opt bytes with
| Some txa -> ok (Tx_rollup_l2_address.Indexable.value txa, ctxt)
| None ->
error
@@ Invalid_syntactic_constant
( loc,
strip_locations expr,
"a valid transaction rollup L2 address" ))
| String (loc, str) as expr (* As unparsed with [Readable]. *) -> (
Gas.consume ctxt Typecheck_costs.tx_rollup_l2_address >>? fun ctxt ->
match Tx_rollup_l2_address.of_b58check_opt str with
| Some txa -> ok (Tx_rollup_l2_address.Indexable.value txa, ctxt)
| None ->
error
@@ Invalid_syntactic_constant
( loc,
strip_locations expr,
"a valid transaction rollup L2 address" ))
| expr ->
error @@ Invalid_kind (location expr, [String_kind; Bytes_kind], kind expr)
let parse_never expr : (never * context) tzresult =
error @@ Invalid_never_expr (location expr)
(* -- parse data of complex types -- *)
let parse_pair (type r) parse_l parse_r ctxt ~legacy
(r_comb_witness : (r, unit -> _) comb_witness) expr =
let parse_comb loc l rs =
parse_l ctxt l >>=? fun (l, ctxt) ->
(match (rs, r_comb_witness) with
| [r], _ -> ok r
| [], _ -> error @@ Invalid_arity (loc, D_Pair, 2, 1)
| _ :: _, Comb_Pair _ ->
(* Unfold [Pair x1 ... xn] as [Pair x1 (Pair x2 ... xn-1 xn))]
for type [pair ta (pair tb1 tb2)] and n >= 3 only *)
ok (Prim (loc, D_Pair, rs, []))
| _ -> error @@ Invalid_arity (loc, D_Pair, 2, 1 + List.length rs))
>>?= fun r ->
parse_r ctxt r >|=? fun (r, ctxt) -> ((l, r), ctxt)
in
match expr with
| Prim (loc, D_Pair, l :: rs, annot) ->
(if legacy then Result.return_unit else error_unexpected_annot loc annot)
>>?= fun () -> parse_comb loc l rs
| Prim (loc, D_Pair, l, _) ->
fail @@ Invalid_arity (loc, D_Pair, 2, List.length l)
(* Unfold [{x1; ...; xn}] as [Pair x1 x2 ... xn-1 xn] for n >= 2 *)
| Seq (loc, l :: (_ :: _ as rs)) -> parse_comb loc l rs
| Seq (loc, l) -> fail @@ Invalid_seq_arity (loc, 2, List.length l)
| expr -> fail @@ unexpected expr [] Constant_namespace [D_Pair]
let parse_union parse_l parse_r ctxt ~legacy = function
| Prim (loc, D_Left, [v], annot) ->
(if legacy then Result.return_unit else error_unexpected_annot loc annot)
>>?= fun () ->
parse_l ctxt v >|=? fun (v, ctxt) -> (L v, ctxt)
| Prim (loc, D_Left, l, _) ->
fail @@ Invalid_arity (loc, D_Left, 1, List.length l)
| Prim (loc, D_Right, [v], annot) ->
(if legacy then Result.return_unit else error_unexpected_annot loc annot)
>>?= fun () ->
parse_r ctxt v >|=? fun (v, ctxt) -> (R v, ctxt)
| Prim (loc, D_Right, l, _) ->
fail @@ Invalid_arity (loc, D_Right, 1, List.length l)
| expr -> fail @@ unexpected expr [] Constant_namespace [D_Left; D_Right]
let parse_option parse_v ctxt ~legacy = function
| Prim (loc, D_Some, [v], annot) ->
(if legacy then Result.return_unit else error_unexpected_annot loc annot)
>>?= fun () ->
parse_v ctxt v >|=? fun (v, ctxt) -> (Some v, ctxt)
| Prim (loc, D_Some, l, _) ->
fail @@ Invalid_arity (loc, D_Some, 1, List.length l)
| Prim (loc, D_None, [], annot) ->
Lwt.return
( (if legacy then Result.return_unit
else error_unexpected_annot loc annot)
>|? fun () -> (None, ctxt) )
| Prim (loc, D_None, l, _) ->
fail @@ Invalid_arity (loc, D_None, 0, List.length l)
| expr -> fail @@ unexpected expr [] Constant_namespace [D_Some; D_None]
let comb_witness1 : type t tc. (t, tc) ty -> (t, unit -> unit) comb_witness =
function
| Pair_t _ -> Comb_Pair Comb_Any
| _ -> Comb_Any
let parse_view_name ctxt : Script.node -> (Script_string.t * context) tzresult =
function
| String (loc, v) as expr ->
(* The limitation of length of string is same as entrypoint *)
if Compare.Int.(String.length v > 31) then error (View_name_too_long v)
else
let rec check_char i =
if Compare.Int.(i < 0) then ok v
else if Script_ir_annot.is_allowed_char v.[i] then check_char (i - 1)
else error (Bad_view_name loc)
in
Gas.consume ctxt (Typecheck_costs.check_printable v) >>? fun ctxt ->
record_trace
(Invalid_syntactic_constant
( loc,
strip_locations expr,
"string [a-zA-Z0-9_.%@] and the maximum string length of 31 \
characters" ))
( check_char (String.length v - 1) >>? fun v ->
Script_string.of_string v >|? fun s -> (s, ctxt) )
| expr -> error @@ Invalid_kind (location expr, [String_kind], kind expr)
let parse_toplevel :
context -> legacy:bool -> Script.expr -> (toplevel * context) tzresult =
fun ctxt ~legacy toplevel ->
record_trace (Ill_typed_contract (toplevel, []))
@@
match root toplevel with
| Int (loc, _) -> error (Invalid_kind (loc, [Seq_kind], Int_kind))
| String (loc, _) -> error (Invalid_kind (loc, [Seq_kind], String_kind))
| Bytes (loc, _) -> error (Invalid_kind (loc, [Seq_kind], Bytes_kind))
| Prim (loc, _, _, _) -> error (Invalid_kind (loc, [Seq_kind], Prim_kind))
| Seq (_, fields) -> (
let rec find_fields ctxt p s c views fields =
match fields with
| [] -> ok (ctxt, (p, s, c, views))
| Int (loc, _) :: _ -> error (Invalid_kind (loc, [Prim_kind], Int_kind))
| String (loc, _) :: _ ->
error (Invalid_kind (loc, [Prim_kind], String_kind))
| Bytes (loc, _) :: _ ->
error (Invalid_kind (loc, [Prim_kind], Bytes_kind))
| Seq (loc, _) :: _ -> error (Invalid_kind (loc, [Prim_kind], Seq_kind))
| Prim (loc, K_parameter, [arg], annot) :: rest -> (
match p with
| None -> find_fields ctxt (Some (arg, loc, annot)) s c views rest
| Some _ -> error (Duplicate_field (loc, K_parameter)))
| Prim (loc, K_storage, [arg], annot) :: rest -> (
match s with
| None -> find_fields ctxt p (Some (arg, loc, annot)) c views rest
| Some _ -> error (Duplicate_field (loc, K_storage)))
| Prim (loc, K_code, [arg], annot) :: rest -> (
match c with
| None -> find_fields ctxt p s (Some (arg, loc, annot)) views rest
| Some _ -> error (Duplicate_field (loc, K_code)))
| Prim (loc, ((K_parameter | K_storage | K_code) as name), args, _) :: _
->
error (Invalid_arity (loc, name, 1, List.length args))
| Prim (loc, K_view, [name; input_ty; output_ty; view_code], _) :: rest
->
parse_view_name ctxt name >>? fun (str, ctxt) ->
Gas.consume
ctxt
(Michelson_v1_gas.Cost_of.Interpreter.view_update str views)
>>? fun ctxt ->
if Script_map.mem str views then error (Duplicated_view_name loc)
else
let views' =
Script_map.update
str
(Some {input_ty; output_ty; view_code})
views
in
find_fields ctxt p s c views' rest
| Prim (loc, K_view, args, _) :: _ ->
error (Invalid_arity (loc, K_view, 4, List.length args))
| Prim (loc, name, _, _) :: _ ->
let allowed = [K_parameter; K_storage; K_code; K_view] in
error (Invalid_primitive (loc, allowed, name))
in
find_fields ctxt None None None (Script_map.empty string_t) fields
>>? fun (ctxt, toplevel) ->
match toplevel with
| None, _, _, _ -> error (Missing_field K_parameter)
| Some _, None, _, _ -> error (Missing_field K_storage)
| Some _, Some _, None, _ -> error (Missing_field K_code)
| ( Some (p, ploc, pannot),
Some (s, sloc, sannot),
Some (c, cloc, cannot),
views ) ->
let p_pannot =
(* root name can be attached to either the parameter
primitive or the toplevel constructor (legacy only).
In the latter case we move it to the parameter type.
*)
Script_ir_annot.has_field_annot p >>? function
| true -> ok (p, pannot)
| false -> (
match pannot with
| [single] when legacy -> (
is_field_annot ploc single >|? fun is_field_annot ->
match (is_field_annot, p) with
| true, Prim (loc, prim, args, annots) ->
(Prim (loc, prim, args, single :: annots), [])
| _ -> (p, []))
| _ -> ok (p, pannot))
in
(* only one field annot is allowed to set the root entrypoint name *)
p_pannot >>? fun (arg_type, pannot) ->
Script_ir_annot.error_unexpected_annot ploc pannot >>? fun () ->
Script_ir_annot.error_unexpected_annot cloc cannot >>? fun () ->
Script_ir_annot.error_unexpected_annot sloc sannot >|? fun () ->
({code_field = c; arg_type; views; storage_type = s}, ctxt))
(* -- parse data of any type -- *)
(*
Some values, such as operations, tickets, or big map ids, are used only
internally and are not allowed to be forged by users.
In [parse_data], [allow_forged] should be [false] for:
- PUSH
- UNPACK
- user-provided script parameters
- storage on origination
And [true] for:
- internal calls parameters
- storage after origination
*)
let rec parse_data :
type a ac.
elab_conf:elab_conf ->
stack_depth:int ->
context ->
allow_forged:bool ->
(a, ac) ty ->
Script.node ->
(a * context) tzresult Lwt.t =
fun ~elab_conf ~stack_depth ctxt ~allow_forged ty script_data ->
Gas.consume ctxt Typecheck_costs.parse_data_cycle >>?= fun ctxt ->
let non_terminal_recursion ctxt ty script_data =
if Compare.Int.(stack_depth > 10_000) then
fail Typechecking_too_many_recursive_calls
else
parse_data
~elab_conf
~stack_depth:(stack_depth + 1)
ctxt
~allow_forged
ty
script_data
in
let parse_data_error () =
let ty = serialize_ty_for_error ty in
Invalid_constant (location script_data, strip_locations script_data, ty)
in
let fail_parse_data () = fail (parse_data_error ()) in
let traced_no_lwt body = record_trace_eval parse_data_error body in
let traced body = trace_eval parse_data_error body in
let traced_fail err = Lwt.return @@ traced_no_lwt (error err) in
let parse_items ctxt expr key_type value_type items item_wrapper =
List.fold_left_es
(fun (last_value, map, ctxt) item ->
match item with
| Prim (loc, D_Elt, [k; v], annot) ->
(if elab_conf.legacy then Result.return_unit
else error_unexpected_annot loc annot)
>>?= fun () ->
non_terminal_recursion ctxt key_type k >>=? fun (k, ctxt) ->
non_terminal_recursion ctxt value_type v >>=? fun (v, ctxt) ->
Lwt.return
( (match last_value with
| Some value ->
Gas.consume
ctxt
(Michelson_v1_gas.Cost_of.Interpreter.compare
key_type
value
k)
>>? fun ctxt ->
let c =
Script_comparable.compare_comparable key_type value k
in
if Compare.Int.(0 <= c) then
if Compare.Int.(0 = c) then
error (Duplicate_map_keys (loc, strip_locations expr))
else
error (Unordered_map_keys (loc, strip_locations expr))
else ok ctxt
| None -> ok ctxt)
>>? fun ctxt ->
Gas.consume
ctxt
(Michelson_v1_gas.Cost_of.Interpreter.map_update k map)
>|? fun ctxt ->
(Some k, Script_map.update k (Some (item_wrapper v)) map, ctxt)
)
| Prim (loc, D_Elt, l, _) ->
fail @@ Invalid_arity (loc, D_Elt, 2, List.length l)
| Prim (loc, name, _, _) ->
fail @@ Invalid_primitive (loc, [D_Elt], name)
| Int _ | String _ | Bytes _ | Seq _ -> fail_parse_data ())
(None, Script_map.empty key_type, ctxt)
items
|> traced
>|=? fun (_, items, ctxt) -> (items, ctxt)
in
let parse_big_map_items (type t) ctxt expr (key_type : t comparable_ty)
value_type items item_wrapper =
List.fold_left_es
(fun (last_key, {map; size}, ctxt) item ->
match item with
| Prim (loc, D_Elt, [k; v], annot) ->
(if elab_conf.legacy then Result.return_unit
else error_unexpected_annot loc annot)
>>?= fun () ->
non_terminal_recursion ctxt key_type k >>=? fun (k, ctxt) ->
hash_comparable_data ctxt key_type k >>=? fun (key_hash, ctxt) ->
non_terminal_recursion ctxt value_type v >>=? fun (v, ctxt) ->
Lwt.return
( (match last_key with
| Some last_key ->
Gas.consume
ctxt
(Michelson_v1_gas.Cost_of.Interpreter.compare
key_type
last_key
k)
>>? fun ctxt ->
let c =
Script_comparable.compare_comparable key_type last_key k
in
if Compare.Int.(0 <= c) then
if Compare.Int.(0 = c) then
error (Duplicate_map_keys (loc, strip_locations expr))
else
error (Unordered_map_keys (loc, strip_locations expr))
else ok ctxt
| None -> ok ctxt)
>>? fun ctxt ->
Gas.consume
ctxt
(Michelson_v1_gas.Cost_of.Interpreter.big_map_update
{map; size})
>>? fun ctxt ->
if Big_map_overlay.mem key_hash map then
error (Duplicate_map_keys (loc, strip_locations expr))
else
ok
( Some k,
{
map =
Big_map_overlay.add key_hash (k, item_wrapper v) map;
size = size + 1;
},
ctxt ) )
| Prim (loc, D_Elt, l, _) ->
fail @@ Invalid_arity (loc, D_Elt, 2, List.length l)
| Prim (loc, name, _, _) ->
fail @@ Invalid_primitive (loc, [D_Elt], name)
| Int _ | String _ | Bytes _ | Seq _ -> fail_parse_data ())
(None, {map = Big_map_overlay.empty; size = 0}, ctxt)
items
|> traced
>|=? fun (_, map, ctxt) -> (map, ctxt)
in
let legacy = elab_conf.legacy in
match (ty, script_data) with
| Unit_t, expr ->
Lwt.return @@ traced_no_lwt
@@ (parse_unit ctxt ~legacy expr : (a * context) tzresult)
| Bool_t, expr -> Lwt.return @@ traced_no_lwt @@ parse_bool ctxt ~legacy expr
| String_t, expr -> Lwt.return @@ traced_no_lwt @@ parse_string ctxt expr
| Bytes_t, expr -> Lwt.return @@ traced_no_lwt @@ parse_bytes ctxt expr
| Int_t, expr -> Lwt.return @@ traced_no_lwt @@ parse_int ctxt expr
| Nat_t, expr -> Lwt.return @@ traced_no_lwt @@ parse_nat ctxt expr
| Mutez_t, expr -> Lwt.return @@ traced_no_lwt @@ parse_mutez ctxt expr
| Timestamp_t, expr ->
Lwt.return @@ traced_no_lwt @@ parse_timestamp ctxt expr
| Key_t, expr -> Lwt.return @@ traced_no_lwt @@ parse_key ctxt expr
| Key_hash_t, expr -> Lwt.return @@ traced_no_lwt @@ parse_key_hash ctxt expr
| Signature_t, expr ->
Lwt.return @@ traced_no_lwt @@ parse_signature ctxt expr
| Operation_t, _ ->
(* operations cannot appear in parameters or storage,
the protocol should never parse the bytes of an operation *)
assert false
| Chain_id_t, expr -> Lwt.return @@ traced_no_lwt @@ parse_chain_id ctxt expr
| Address_t, expr -> Lwt.return @@ traced_no_lwt @@ parse_address ctxt expr
| Tx_rollup_l2_address_t, expr ->
Lwt.return @@ traced_no_lwt @@ parse_tx_rollup_l2_address ctxt expr
| Contract_t (arg_ty, _), expr ->
traced
( parse_address ctxt expr >>?= fun (address, ctxt) ->
let loc = location expr in
parse_contract_data
~stack_depth:(stack_depth + 1)
ctxt
loc
arg_ty
address.destination
~entrypoint:address.entrypoint
>|=? fun (ctxt, typed_contract) -> (typed_contract, ctxt) )
(* Pairs *)
| Pair_t (tl, tr, _, _), expr ->
let r_witness = comb_witness1 tr in
let parse_l ctxt v = non_terminal_recursion ctxt tl v in
let parse_r ctxt v = non_terminal_recursion ctxt tr v in
traced @@ parse_pair parse_l parse_r ctxt ~legacy r_witness expr
(* Unions *)
| Union_t (tl, tr, _, _), expr ->
let parse_l ctxt v = non_terminal_recursion ctxt tl v in
let parse_r ctxt v = non_terminal_recursion ctxt tr v in
traced @@ parse_union parse_l parse_r ctxt ~legacy expr
(* Lambdas *)
| Lambda_t (ta, tr, _ty_name), (Seq (_loc, _) as script_instr) ->
traced
@@ parse_kdescr
Tc_context.data
~elab_conf
~stack_depth:(stack_depth + 1)
ctxt
ta
tr
script_instr
>|=? fun (kdescr, ctxt) -> (Lam (kdescr, script_instr), ctxt)
| ( Lambda_t (ta, tr, _ty_name),
Prim (loc, D_Lambda_rec, [(Seq (_loc, _) as script_instr)], []) ) ->
traced
@@ ( lambda_t loc ta tr >>?= fun lambda_rec_ty ->
parse_lam_rec
Tc_context.(add_lambda data)
~elab_conf
~stack_depth:(stack_depth + 1)
ctxt
ta
tr
lambda_rec_ty
script_instr )
| Lambda_t _, expr ->
traced_fail (Invalid_kind (location expr, [Seq_kind], kind expr))
(* Options *)
| Option_t (t, _, _), expr ->
let parse_v ctxt v = non_terminal_recursion ctxt t v in
traced @@ parse_option parse_v ctxt ~legacy expr
(* Lists *)
| List_t (t, _ty_name), Seq (_loc, items) ->
traced
@@ List.fold_right_es
(fun v (rest, ctxt) ->
non_terminal_recursion ctxt t v >|=? fun (v, ctxt) ->
(Script_list.cons v rest, ctxt))
items
(Script_list.empty, ctxt)
| List_t _, expr ->
traced_fail (Invalid_kind (location expr, [Seq_kind], kind expr))
(* Tickets *)
| Ticket_t (t, _ty_name), expr ->
if allow_forged then
opened_ticket_type (location expr) t >>?= fun ty ->
non_terminal_recursion ctxt ty expr
>>=? fun (({destination; entrypoint = _}, (contents, amount)), ctxt) ->
match destination with
| Contract ticketer -> return ({ticketer; contents; amount}, ctxt)
| Tx_rollup _ | Sc_rollup _ ->
fail (Unexpected_ticket_owner destination)
else traced_fail (Unexpected_forged_value (location expr))
(* Sets *)
| Set_t (t, _ty_name), (Seq (loc, vs) as expr) ->
traced
@@ List.fold_left_es
(fun (last_value, set, ctxt) v ->
non_terminal_recursion ctxt t v >>=? fun (v, ctxt) ->
Lwt.return
( (match last_value with
| Some value ->
Gas.consume
ctxt
(Michelson_v1_gas.Cost_of.Interpreter.compare t value v)
>>? fun ctxt ->
let c = Script_comparable.compare_comparable t value v in
if Compare.Int.(0 <= c) then
if Compare.Int.(0 = c) then
error
(Duplicate_set_values (loc, strip_locations expr))
else
error
(Unordered_set_values (loc, strip_locations expr))
else ok ctxt
| None -> ok ctxt)
>>? fun ctxt ->
Gas.consume
ctxt
(Michelson_v1_gas.Cost_of.Interpreter.set_update v set)
>|? fun ctxt -> (Some v, Script_set.update v true set, ctxt) ))
(None, Script_set.empty t, ctxt)
vs
>|=? fun (_, set, ctxt) -> (set, ctxt)
| Set_t _, expr ->
traced_fail (Invalid_kind (location expr, [Seq_kind], kind expr))
(* Maps *)
| Map_t (tk, tv, _ty_name), (Seq (_, vs) as expr) ->
parse_items ctxt expr tk tv vs (fun x -> x)
| Map_t _, expr ->
traced_fail (Invalid_kind (location expr, [Seq_kind], kind expr))
| Big_map_t (tk, tv, _ty_name), expr ->
(match expr with
| Int (loc, id) ->
return (Some (id, loc), {map = Big_map_overlay.empty; size = 0}, ctxt)
| Seq (_, vs) ->
parse_big_map_items ctxt expr tk tv vs (fun x -> Some x)
>|=? fun (diff, ctxt) -> (None, diff, ctxt)
| Prim (loc, D_Pair, [Int (loc_id, id); Seq (_, vs)], annot) ->
error_unexpected_annot loc annot >>?= fun () ->
option_t loc tv >>?= fun tv_opt ->
parse_big_map_items ctxt expr tk tv_opt vs (fun x -> x)
>|=? fun (diff, ctxt) -> (Some (id, loc_id), diff, ctxt)
| Prim (_, D_Pair, [Int _; expr], _) ->
traced_fail (Invalid_kind (location expr, [Seq_kind], kind expr))
| Prim (_, D_Pair, [expr; _], _) ->
traced_fail (Invalid_kind (location expr, [Int_kind], kind expr))
| Prim (loc, D_Pair, l, _) ->
traced_fail @@ Invalid_arity (loc, D_Pair, 2, List.length l)
| _ ->
traced_fail
(unexpected expr [Seq_kind; Int_kind] Constant_namespace [D_Pair]))
>>=? fun (id_opt, diff, ctxt) ->
(match id_opt with
| None -> return @@ (None, ctxt)
| Some (id, loc) ->
if allow_forged then
let id = Big_map.Id.parse_z id in
Big_map.exists ctxt id >>=? function
| _, None -> traced_fail (Invalid_big_map (loc, id))
| ctxt, Some (btk, btv) ->
Lwt.return
( parse_comparable_ty
~stack_depth:(stack_depth + 1)
ctxt
(Micheline.root btk)
>>? fun (Ex_comparable_ty btk, ctxt) ->
parse_big_map_value_ty
ctxt
~stack_depth:(stack_depth + 1)
~legacy
(Micheline.root btv)
>>? fun (Ex_ty btv, ctxt) ->
(Gas_monad.run ctxt
@@
let open Gas_monad.Syntax in
let error_details = Informative loc in
let* Eq = ty_eq ~error_details tk btk in
ty_eq ~error_details tv btv)
>>? fun (eq, ctxt) ->
eq >|? fun Eq -> (Some id, ctxt) )
else traced_fail (Unexpected_forged_value loc))
>|=? fun (id, ctxt) ->
(Big_map {id; diff; key_type = tk; value_type = tv}, ctxt)
| Never_t, expr -> Lwt.return @@ traced_no_lwt @@ parse_never expr
(* Bls12_381 types *)
| Bls12_381_g1_t, Bytes (_, bs) -> (
Gas.consume ctxt Typecheck_costs.bls12_381_g1 >>?= fun ctxt ->
match Script_bls.G1.of_bytes_opt bs with
| Some pt -> return (pt, ctxt)
| None -> fail_parse_data ())
| Bls12_381_g1_t, expr ->
traced_fail (Invalid_kind (location expr, [Bytes_kind], kind expr))
| Bls12_381_g2_t, Bytes (_, bs) -> (
Gas.consume ctxt Typecheck_costs.bls12_381_g2 >>?= fun ctxt ->
match Script_bls.G2.of_bytes_opt bs with
| Some pt -> return (pt, ctxt)
| None -> fail_parse_data ())
| Bls12_381_g2_t, expr ->
traced_fail (Invalid_kind (location expr, [Bytes_kind], kind expr))
| Bls12_381_fr_t, Bytes (_, bs) -> (
Gas.consume ctxt Typecheck_costs.bls12_381_fr >>?= fun ctxt ->
match Script_bls.Fr.of_bytes_opt bs with
| Some pt -> return (pt, ctxt)
| None -> fail_parse_data ())
| Bls12_381_fr_t, Int (_, v) ->
Gas.consume ctxt Typecheck_costs.bls12_381_fr >>?= fun ctxt ->
return (Script_bls.Fr.of_z v, ctxt)
| Bls12_381_fr_t, expr ->
traced_fail (Invalid_kind (location expr, [Bytes_kind], kind expr))
(*
/!\ When adding new lazy storage kinds, you may want to guard the parsing
of identifiers with [allow_forged].
*)
(* Sapling *)
| Sapling_transaction_t memo_size, Bytes (_, bytes) -> (
match
Data_encoding.Binary.of_bytes_opt Sapling.transaction_encoding bytes
with
| Some transaction -> (
match Sapling.transaction_get_memo_size transaction with
| None -> return (transaction, ctxt)
| Some transac_memo_size ->
Lwt.return
( memo_size_eq
~error_details:(Informative ())
memo_size
transac_memo_size
>|? fun () -> (transaction, ctxt) ))
| None -> fail_parse_data ())
| Sapling_transaction_t _, expr ->
traced_fail (Invalid_kind (location expr, [Bytes_kind], kind expr))
| Sapling_transaction_deprecated_t memo_size, Bytes (_, bytes) -> (
match
Data_encoding.Binary.of_bytes_opt
Sapling.Legacy.transaction_encoding
bytes
with
| Some transaction -> (
match Sapling.Legacy.transaction_get_memo_size transaction with
| None -> return (transaction, ctxt)
| Some transac_memo_size ->
Lwt.return
( memo_size_eq
~error_details:(Informative ())
memo_size
transac_memo_size
>|? fun () -> (transaction, ctxt) ))
| None -> fail_parse_data ())
| Sapling_transaction_deprecated_t _, expr ->
traced_fail (Invalid_kind (location expr, [Bytes_kind], kind expr))
| Sapling_state_t memo_size, Int (loc, id) ->
if allow_forged then
let id = Sapling.Id.parse_z id in
Sapling.state_from_id ctxt id >>=? fun (state, ctxt) ->
Lwt.return
( traced_no_lwt
@@ memo_size_eq
~error_details:(Informative ())
memo_size
state.Sapling.memo_size
>|? fun () -> (state, ctxt) )
else traced_fail (Unexpected_forged_value loc)
| Sapling_state_t memo_size, Seq (_, []) ->
return (Sapling.empty_state ~memo_size (), ctxt)
| Sapling_state_t _, expr ->
(* Do not allow to input diffs as they are untrusted and may not be the
result of a verify_update. *)
traced_fail
(Invalid_kind (location expr, [Int_kind; Seq_kind], kind expr))
(* Time lock*)
| Chest_key_t, Bytes (_, bytes) -> (
Gas.consume ctxt Typecheck_costs.chest_key >>?= fun ctxt ->
match
Data_encoding.Binary.of_bytes_opt
Script_timelock.chest_key_encoding
bytes
with
| Some chest_key -> return (chest_key, ctxt)
| None -> fail_parse_data ())
| Chest_key_t, expr ->
traced_fail (Invalid_kind (location expr, [Bytes_kind], kind expr))
| Chest_t, Bytes (_, bytes) -> (
Gas.consume ctxt (Typecheck_costs.chest ~bytes:(Bytes.length bytes))
>>?= fun ctxt ->
match
Data_encoding.Binary.of_bytes_opt Script_timelock.chest_encoding bytes
with
| Some chest -> return (chest, ctxt)
| None -> fail_parse_data ())
| Chest_t, expr ->
traced_fail (Invalid_kind (location expr, [Bytes_kind], kind expr))
and parse_view :
type storage storagec.
elab_conf:elab_conf ->
context ->
(storage, storagec) ty ->
view ->
(storage typed_view * context) tzresult Lwt.t =
fun ~elab_conf ctxt storage_type {input_ty; output_ty; view_code} ->
let legacy = elab_conf.legacy in
let input_ty_loc = location input_ty in
record_trace_eval
(fun () ->
Ill_formed_type
(Some "arg of view", strip_locations input_ty, input_ty_loc))
(parse_view_input_ty ctxt ~stack_depth:0 ~legacy input_ty)
>>?= fun (Ex_ty input_ty, ctxt) ->
let output_ty_loc = location output_ty in
record_trace_eval
(fun () ->
Ill_formed_type
(Some "return of view", strip_locations output_ty, output_ty_loc))
(parse_view_output_ty ctxt ~stack_depth:0 ~legacy output_ty)
>>?= fun (Ex_ty output_ty, ctxt) ->
pair_t input_ty_loc input_ty storage_type >>?= fun (Ty_ex_c pair_ty) ->
parse_instr
~elab_conf
~stack_depth:0
Tc_context.view
ctxt
view_code
(Item_t (pair_ty, Bot_t))
>>=? fun (judgement, ctxt) ->
Lwt.return
@@
match judgement with
| Failed {descr} ->
let {kinstr; _} = close_descr (descr (Item_t (output_ty, Bot_t))) in
ok
( Typed_view
{input_ty; output_ty; kinstr; original_code_expr = view_code},
ctxt )
| Typed ({loc; aft; _} as descr) -> (
let ill_type_view stack_ty loc =
let actual = serialize_stack_for_error ctxt stack_ty in
let expected_stack = Item_t (output_ty, Bot_t) in
let expected = serialize_stack_for_error ctxt expected_stack in
Ill_typed_view {loc; actual; expected}
in
match aft with
| Item_t (ty, Bot_t) ->
let error_details = Informative loc in
Gas_monad.run ctxt
@@ Gas_monad.record_trace_eval ~error_details (fun loc ->
ill_type_view aft loc)
@@ ty_eq ~error_details ty output_ty
>>? fun (eq, ctxt) ->
eq >|? fun Eq ->
let {kinstr; _} = close_descr descr in
( Typed_view
{input_ty; output_ty; kinstr; original_code_expr = view_code},
ctxt )
| _ -> error (ill_type_view aft loc))
and parse_views :
type storage storagec.
elab_conf:elab_conf ->
context ->
(storage, storagec) ty ->
view_map ->
(storage typed_view_map * context) tzresult Lwt.t =
fun ~elab_conf ctxt storage_type views ->
let aux ctxt name cur_view =
Gas.consume
ctxt
(Michelson_v1_gas.Cost_of.Interpreter.view_update name views)
>>?= fun ctxt -> parse_view ~elab_conf ctxt storage_type cur_view
in
Script_map.map_es_in_context aux ctxt views
and parse_kdescr :
type arg argc ret retc.
elab_conf:elab_conf ->
stack_depth:int ->
tc_context ->
context ->
(arg, argc) ty ->
(ret, retc) ty ->
Script.node ->
((arg, end_of_stack, ret, end_of_stack) kdescr * context) tzresult Lwt.t =
fun ~elab_conf ~stack_depth tc_context ctxt arg ret script_instr ->
parse_instr
~elab_conf
tc_context
ctxt
~stack_depth:(stack_depth + 1)
script_instr
(Item_t (arg, Bot_t))
>>=? function
| Typed ({loc; aft = Item_t (ty, Bot_t) as stack_ty; _} as descr), ctxt ->
Lwt.return
(let error_details = Informative loc in
Gas_monad.run ctxt
@@ Gas_monad.record_trace_eval ~error_details (fun loc ->
let ret = serialize_ty_for_error ret in
let stack_ty = serialize_stack_for_error ctxt stack_ty in
Bad_return (loc, stack_ty, ret))
@@ ty_eq ~error_details ty ret
>>? fun (eq, ctxt) ->
eq >|? fun Eq ->
( (close_descr descr : (arg, end_of_stack, ret, end_of_stack) kdescr),
ctxt ))
| Typed {loc; aft = stack_ty; _}, ctxt ->
let ret = serialize_ty_for_error ret in
let stack_ty = serialize_stack_for_error ctxt stack_ty in
fail @@ Bad_return (loc, stack_ty, ret)
| Failed {descr}, ctxt ->
return
( (close_descr (descr (Item_t (ret, Bot_t)))
: (arg, end_of_stack, ret, end_of_stack) kdescr),
ctxt )
and parse_lam_rec :
type arg argc ret retc.
elab_conf:elab_conf ->
stack_depth:int ->
tc_context ->
context ->
(arg, argc) ty ->
(ret, retc) ty ->
((arg, ret) lambda, _) ty ->
Script.node ->
((arg, ret) lambda * context) tzresult Lwt.t =
fun ~elab_conf ~stack_depth tc_context ctxt arg ret lambda_rec_ty script_instr ->
parse_instr
~elab_conf
tc_context
ctxt
~stack_depth:(stack_depth + 1)
script_instr
(Item_t (arg, Item_t (lambda_rec_ty, Bot_t)))
>>=? function
| Typed ({loc; aft = Item_t (ty, Bot_t) as stack_ty; _} as descr), ctxt ->
Lwt.return
(let error_details = Informative loc in
Gas_monad.run ctxt
@@ Gas_monad.record_trace_eval ~error_details (fun loc ->
let ret = serialize_ty_for_error ret in
let stack_ty = serialize_stack_for_error ctxt stack_ty in
Bad_return (loc, stack_ty, ret))
@@ ty_eq ~error_details ty ret
>>? fun (eq, ctxt) ->
eq >|? fun Eq ->
((LamRec (close_descr descr, script_instr) : (arg, ret) lambda), ctxt))
| Typed {loc; aft = stack_ty; _}, ctxt ->
let ret = serialize_ty_for_error ret in
let stack_ty = serialize_stack_for_error ctxt stack_ty in
fail @@ Bad_return (loc, stack_ty, ret)
| Failed {descr}, ctxt ->
return
( (LamRec (close_descr (descr (Item_t (ret, Bot_t))), script_instr)
: (arg, ret) lambda),
ctxt )
and parse_instr :
type a s.
elab_conf:elab_conf ->
stack_depth:int ->
tc_context ->
context ->
Script.node ->
(a, s) stack_ty ->
((a, s) judgement * context) tzresult Lwt.t =
fun ~elab_conf ~stack_depth tc_context ctxt script_instr stack_ty ->
let for_logging_only x =
if elab_conf.keep_extra_types_for_interpreter_logging then Some x else None
in
let check_item_ty (type a ac b bc) ctxt (exp : (a, ac) ty) (got : (b, bc) ty)
loc name n m : ((a, b) eq * context) tzresult =
record_trace_eval (fun () ->
let stack_ty = serialize_stack_for_error ctxt stack_ty in
Bad_stack (loc, name, m, stack_ty))
@@ record_trace
(Bad_stack_item n)
( Gas_monad.run ctxt @@ ty_eq ~error_details:(Informative loc) exp got
>>? fun (eq, ctxt) ->
eq >|? fun Eq -> ((Eq : (a, b) eq), ctxt) )
in
let log_stack loc stack_ty aft =
match (elab_conf.type_logger, script_instr) with
| None, _ | Some _, (Int _ | String _ | Bytes _) -> ()
| Some log, (Prim _ | Seq _) ->
(* Unparsing for logging is not carbonated as this
is used only by the client and not the protocol *)
let stack_ty_before = unparse_stack_uncarbonated stack_ty in
let stack_ty_after = unparse_stack_uncarbonated aft in
log loc ~stack_ty_before ~stack_ty_after
in
let typed_no_lwt ctxt loc instr aft =
log_stack loc stack_ty aft ;
let j = Typed {loc; instr; bef = stack_ty; aft} in
Ok (j, ctxt)
in
let typed ctxt loc instr aft =
Lwt.return @@ typed_no_lwt ctxt loc instr aft
in
Gas.consume ctxt Typecheck_costs.parse_instr_cycle >>?= fun ctxt ->
let non_terminal_recursion tc_context ctxt script_instr stack_ty =
if Compare.Int.(stack_depth > 10000) then
fail Typechecking_too_many_recursive_calls
else
parse_instr
~elab_conf
tc_context
ctxt
~stack_depth:(stack_depth + 1)
script_instr
stack_ty
in
let bad_stack_error ctxt loc prim relevant_stack_portion =
let whole_stack = serialize_stack_for_error ctxt stack_ty in
error (Bad_stack (loc, prim, relevant_stack_portion, whole_stack))
in
let legacy = elab_conf.legacy in
match (script_instr, stack_ty) with
(* stack ops *)
| Prim (loc, I_DROP, [], annot), Item_t (_, rest) ->
(error_unexpected_annot loc annot >>?= fun () ->
typed ctxt loc {apply = (fun k -> IDrop (loc, k))} rest
: ((a, s) judgement * context) tzresult Lwt.t)
| Prim (loc, I_DROP, [n], result_annot), whole_stack ->
parse_uint10 n >>?= fun whole_n ->
Gas.consume ctxt (Typecheck_costs.proof_argument whole_n) >>?= fun ctxt ->
let rec make_proof_argument :
type a s.
int -> (a, s) stack_ty -> (a, s) dropn_proof_argument tzresult =
fun n stk ->
match (Compare.Int.(n = 0), stk) with
| true, rest -> ok @@ Dropn_proof_argument (KRest, rest)
| false, Item_t (a, rest) ->
make_proof_argument (n - 1) rest
>|? fun (Dropn_proof_argument (n', stack_after_drops)) ->
Dropn_proof_argument (KPrefix (loc, a, n'), stack_after_drops)
| _, _ ->
let whole_stack = serialize_stack_for_error ctxt whole_stack in
error (Bad_stack (loc, I_DROP, whole_n, whole_stack))
in
error_unexpected_annot loc result_annot >>?= fun () ->
make_proof_argument whole_n whole_stack
>>?= fun (Dropn_proof_argument (n', stack_after_drops)) ->
let kdropn k = IDropn (loc, whole_n, n', k) in
typed ctxt loc {apply = kdropn} stack_after_drops
| Prim (loc, I_DROP, (_ :: _ :: _ as l), _), _ ->
(* Technically, the arities 0 and 1 are allowed but the error only mentions 1.
However, DROP is equivalent to DROP 1 so hinting at an arity of 1 makes sense. *)
fail (Invalid_arity (loc, I_DROP, 1, List.length l))
| Prim (loc, I_DUP, [], annot), (Item_t (v, _) as stack) ->
check_var_annot loc annot >>?= fun () ->
record_trace_eval
(fun () ->
let t = serialize_ty_for_error v in
Non_dupable_type (loc, t))
(check_dupable_ty ctxt loc v)
>>?= fun ctxt ->
let dup = {apply = (fun k -> IDup (loc, k))} in
typed ctxt loc dup (Item_t (v, stack))
| Prim (loc, I_DUP, [n], v_annot), (Item_t _ as stack_ty) ->
check_var_annot loc v_annot >>?= fun () ->
let rec make_proof_argument :
type a b s.
int -> (a, b * s) stack_ty -> (a, b, s) dup_n_proof_argument tzresult
=
fun n (stack_ty : (a, b * s) stack_ty) ->
match (n, stack_ty) with
| 1, Item_t (hd_ty, _) -> ok @@ Dup_n_proof_argument (Dup_n_zero, hd_ty)
| n, Item_t (_, (Item_t (_, _) as tl_ty)) ->
make_proof_argument (n - 1) tl_ty
>|? fun (Dup_n_proof_argument (dup_n_witness, b_ty)) ->
Dup_n_proof_argument (Dup_n_succ dup_n_witness, b_ty)
| _ -> bad_stack_error ctxt loc I_DUP 1
in
parse_uint10 n >>?= fun n ->
Gas.consume ctxt (Typecheck_costs.proof_argument n) >>?= fun ctxt ->
error_unless (Compare.Int.( > ) n 0) (Dup_n_bad_argument loc)
>>?= fun () ->
record_trace (Dup_n_bad_stack loc) (make_proof_argument n stack_ty)
>>?= fun (Dup_n_proof_argument (witness, after_ty)) ->
record_trace_eval
(fun () ->
let t = serialize_ty_for_error after_ty in
Non_dupable_type (loc, t))
(check_dupable_ty ctxt loc after_ty)
>>?= fun ctxt ->
let dupn = {apply = (fun k -> IDup_n (loc, n, witness, k))} in
typed ctxt loc dupn (Item_t (after_ty, stack_ty))
| Prim (loc, I_DIG, [n], result_annot), stack ->
let rec make_proof_argument :
type a s. int -> (a, s) stack_ty -> (a, s) dig_proof_argument tzresult
=
fun n stk ->
match (Compare.Int.(n = 0), stk) with
| true, Item_t (v, rest) -> ok @@ Dig_proof_argument (KRest, v, rest)
| false, Item_t (v, rest) ->
make_proof_argument (n - 1) rest
>|? fun (Dig_proof_argument (n', x, aft')) ->
Dig_proof_argument (KPrefix (loc, v, n'), x, Item_t (v, aft'))
| _, _ ->
let whole_stack = serialize_stack_for_error ctxt stack in
error (Bad_stack (loc, I_DIG, 3, whole_stack))
in
parse_uint10 n >>?= fun n ->
Gas.consume ctxt (Typecheck_costs.proof_argument n) >>?= fun ctxt ->
error_unexpected_annot loc result_annot >>?= fun () ->
make_proof_argument n stack >>?= fun (Dig_proof_argument (n', x, aft)) ->
let dig = {apply = (fun k -> IDig (loc, n, n', k))} in
typed ctxt loc dig (Item_t (x, aft))
| Prim (loc, I_DIG, (([] | _ :: _ :: _) as l), _), _ ->
fail (Invalid_arity (loc, I_DIG, 1, List.length l))
| Prim (loc, I_DUG, [n], result_annot), Item_t (x, whole_stack) -> (
parse_uint10 n >>?= fun whole_n ->
Gas.consume ctxt (Typecheck_costs.proof_argument whole_n) >>?= fun ctxt ->
error_unexpected_annot loc result_annot >>?= fun () ->
match make_dug_proof_argument loc whole_n x whole_stack with
| None ->
let whole_stack = serialize_stack_for_error ctxt whole_stack in
fail (Bad_stack (loc, I_DUG, whole_n, whole_stack))
| Some (Dug_proof_argument (n', aft)) ->
let dug = {apply = (fun k -> IDug (loc, whole_n, n', k))} in
typed ctxt loc dug aft)
| Prim (loc, I_DUG, [_], result_annot), stack ->
Lwt.return
( error_unexpected_annot loc result_annot >>? fun () ->
let stack = serialize_stack_for_error ctxt stack in
error (Bad_stack (loc, I_DUG, 1, stack)) )
| Prim (loc, I_DUG, (([] | _ :: _ :: _) as l), _), _ ->
fail (Invalid_arity (loc, I_DUG, 1, List.length l))
| Prim (loc, I_SWAP, [], annot), Item_t (v, Item_t (w, rest)) ->
error_unexpected_annot loc annot >>?= fun () ->
let swap = {apply = (fun k -> ISwap (loc, k))} in
let stack_ty = Item_t (w, Item_t (v, rest)) in
typed ctxt loc swap stack_ty
| Prim (loc, I_PUSH, [t; d], annot), stack ->
check_var_annot loc annot >>?= fun () ->
parse_packable_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy t
>>?= fun (Ex_ty t, ctxt) ->
parse_data
~elab_conf
~stack_depth:(stack_depth + 1)
ctxt
~allow_forged:false
t
d
>>=? fun (v, ctxt) ->
let const = {apply = (fun k -> IConst (loc, t, v, k))} in
typed ctxt loc const (Item_t (t, stack))
| Prim (loc, I_UNIT, [], annot), stack ->
check_var_type_annot loc annot >>?= fun () ->
let const = {apply = (fun k -> IConst (loc, unit_t, (), k))} in
typed ctxt loc const (Item_t (unit_t, stack))
(* options *)
| Prim (loc, I_SOME, [], annot), Item_t (t, rest) ->
check_var_type_annot loc annot >>?= fun () ->
let cons_some = {apply = (fun k -> ICons_some (loc, k))} in
option_t loc t >>?= fun ty -> typed ctxt loc cons_some (Item_t (ty, rest))
| Prim (loc, I_NONE, [t], annot), stack ->
parse_any_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy t
>>?= fun (Ex_ty t, ctxt) ->
check_var_type_annot loc annot >>?= fun () ->
let cons_none = {apply = (fun k -> ICons_none (loc, t, k))} in
option_t loc t >>?= fun ty ->
let stack_ty = Item_t (ty, stack) in
typed ctxt loc cons_none stack_ty
| Prim (loc, I_MAP, [body], annot), Item_t (Option_t (t, _, _), rest) -> (
check_kind [Seq_kind] body >>?= fun () ->
check_var_type_annot loc annot >>?= fun () ->
non_terminal_recursion tc_context ctxt body (Item_t (t, rest))
>>=? fun (judgement, ctxt) ->
Lwt.return
@@
match judgement with
| Typed ({loc; aft = Item_t (ret, aft_rest); _} as kibody) ->
let invalid_map_body () =
let aft = serialize_stack_for_error ctxt kibody.aft in
Invalid_map_body (loc, aft)
in
record_trace_eval
invalid_map_body
( stack_eq loc ctxt 1 aft_rest rest >>? fun (Eq, ctxt) ->
option_t loc ret >>? fun opt_ty ->
let final_stack = Item_t (opt_ty, rest) in
let body = kibody.instr.apply (IHalt loc) in
let apply k = IOpt_map {loc; body; k} in
typed_no_lwt ctxt loc {apply} final_stack )
| Typed {aft = Bot_t; _} ->
let aft = serialize_stack_for_error ctxt Bot_t in
error (Invalid_map_body (loc, aft))
| Failed _ -> error (Invalid_map_block_fail loc))
| ( Prim (loc, I_IF_NONE, [bt; bf], annot),
(Item_t (Option_t (t, _, _), rest) as bef) ) ->
check_kind [Seq_kind] bt >>?= fun () ->
check_kind [Seq_kind] bf >>?= fun () ->
error_unexpected_annot loc annot >>?= fun () ->
non_terminal_recursion tc_context ctxt bt rest >>=? fun (btr, ctxt) ->
let stack_ty = Item_t (t, rest) in
non_terminal_recursion tc_context ctxt bf stack_ty >>=? fun (bfr, ctxt) ->
let branch ibt ibf =
let ifnone =
{
apply =
(fun k ->
let hloc = kinstr_location k in
let branch_if_none = ibt.instr.apply (IHalt hloc)
and branch_if_some = ibf.instr.apply (IHalt hloc) in
IIf_none {loc; branch_if_none; branch_if_some; k});
}
in
{loc; instr = ifnone; bef; aft = ibt.aft}
in
Lwt.return @@ merge_branches ctxt loc btr bfr {branch}
(* pairs *)
| Prim (loc, I_PAIR, [], annot), Item_t (a, Item_t (b, rest)) ->
check_constr_annot loc annot >>?= fun () ->
pair_t loc a b >>?= fun (Ty_ex_c ty) ->
let stack_ty = Item_t (ty, rest) in
let cons_pair = {apply = (fun k -> ICons_pair (loc, k))} in
typed ctxt loc cons_pair stack_ty
| Prim (loc, I_PAIR, [n], annot), (Item_t _ as stack_ty) ->
check_var_annot loc annot >>?= fun () ->
let rec make_proof_argument :
type a b s.
int -> (a, b * s) stack_ty -> (a, b, s) comb_proof_argument tzresult =
fun n stack_ty ->
match (n, stack_ty) with
| 1, Item_t _ -> ok (Comb_proof_argument (Comb_one, stack_ty))
| n, Item_t (a_ty, (Item_t _ as tl_ty)) ->
make_proof_argument (n - 1) tl_ty
>>? fun (Comb_proof_argument (comb_witness, Item_t (b_ty, tl_ty')))
->
pair_t loc a_ty b_ty >|? fun (Ty_ex_c pair_t) ->
Comb_proof_argument (Comb_succ comb_witness, Item_t (pair_t, tl_ty'))
| _ -> bad_stack_error ctxt loc I_PAIR 1
in
parse_uint10 n >>?= fun n ->
Gas.consume ctxt (Typecheck_costs.proof_argument n) >>?= fun ctxt ->
error_unless (Compare.Int.( > ) n 1) (Pair_bad_argument loc)
>>?= fun () ->
make_proof_argument n stack_ty
>>?= fun (Comb_proof_argument (witness, after_ty)) ->
let comb = {apply = (fun k -> IComb (loc, n, witness, k))} in
typed ctxt loc comb after_ty
| Prim (loc, I_UNPAIR, [n], annot), (Item_t _ as stack_ty) ->
error_unexpected_annot loc annot >>?= fun () ->
let rec make_proof_argument :
type a b s.
int -> (a, b * s) stack_ty -> (a, b, s) uncomb_proof_argument tzresult
=
fun n stack_ty ->
match (n, stack_ty) with
| 1, (Item_t _ as stack) ->
ok @@ Uncomb_proof_argument (Uncomb_one, stack)
| n, Item_t (Pair_t (a_ty, b_ty, _, _), tl_ty) ->
make_proof_argument (n - 1) (Item_t (b_ty, tl_ty))
>|? fun (Uncomb_proof_argument (uncomb_witness, after_ty)) ->
Uncomb_proof_argument
(Uncomb_succ uncomb_witness, Item_t (a_ty, after_ty))
| _ -> bad_stack_error ctxt loc I_UNPAIR 1
in
parse_uint10 n >>?= fun n ->
Gas.consume ctxt (Typecheck_costs.proof_argument n) >>?= fun ctxt ->
error_unless (Compare.Int.( > ) n 1) (Unpair_bad_argument loc)
>>?= fun () ->
make_proof_argument n stack_ty
>>?= fun (Uncomb_proof_argument (witness, after_ty)) ->
let uncomb = {apply = (fun k -> IUncomb (loc, n, witness, k))} in
typed ctxt loc uncomb after_ty
| Prim (loc, I_GET, [n], annot), Item_t (comb_ty, rest_ty) -> (
check_var_annot loc annot >>?= fun () ->
parse_uint11 n >>?= fun n ->
Gas.consume ctxt (Typecheck_costs.proof_argument n) >>?= fun ctxt ->
match make_comb_get_proof_argument n comb_ty with
| None ->
let whole_stack = serialize_stack_for_error ctxt stack_ty in
fail (Bad_stack (loc, I_GET, 1, whole_stack))
| Some (Comb_get_proof_argument (witness, ty')) ->
let after_stack_ty = Item_t (ty', rest_ty) in
let comb_get = {apply = (fun k -> IComb_get (loc, n, witness, k))} in
typed ctxt loc comb_get after_stack_ty)
| ( Prim (loc, I_UPDATE, [n], annot),
Item_t (value_ty, Item_t (comb_ty, rest_ty)) ) ->
check_var_annot loc annot >>?= fun () ->
parse_uint11 n >>?= fun n ->
Gas.consume ctxt (Typecheck_costs.proof_argument n) >>?= fun ctxt ->
make_comb_set_proof_argument ctxt stack_ty loc n value_ty comb_ty
>>?= fun (Comb_set_proof_argument (witness, after_ty)) ->
let after_stack_ty = Item_t (after_ty, rest_ty) in
let comb_set = {apply = (fun k -> IComb_set (loc, n, witness, k))} in
typed ctxt loc comb_set after_stack_ty
| Prim (loc, I_UNPAIR, [], annot), Item_t (Pair_t (a, b, _, _), rest) ->
check_unpair_annot loc annot >>?= fun () ->
let unpair = {apply = (fun k -> IUnpair (loc, k))} in
typed ctxt loc unpair (Item_t (a, Item_t (b, rest)))
| Prim (loc, I_CAR, [], annot), Item_t (Pair_t (a, _, _, _), rest) ->
check_destr_annot loc annot >>?= fun () ->
let car = {apply = (fun k -> ICar (loc, k))} in
typed ctxt loc car (Item_t (a, rest))
| Prim (loc, I_CDR, [], annot), Item_t (Pair_t (_, b, _, _), rest) ->
check_destr_annot loc annot >>?= fun () ->
let cdr = {apply = (fun k -> ICdr (loc, k))} in
typed ctxt loc cdr (Item_t (b, rest))
(* unions *)
| Prim (loc, I_LEFT, [tr], annot), Item_t (tl, rest) ->
parse_any_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy tr
>>?= fun (Ex_ty tr, ctxt) ->
check_constr_annot loc annot >>?= fun () ->
let cons_left = {apply = (fun k -> ICons_left (loc, tr, k))} in
union_t loc tl tr >>?= fun (Ty_ex_c ty) ->
let stack_ty = Item_t (ty, rest) in
typed ctxt loc cons_left stack_ty
| Prim (loc, I_RIGHT, [tl], annot), Item_t (tr, rest) ->
parse_any_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy tl
>>?= fun (Ex_ty tl, ctxt) ->
check_constr_annot loc annot >>?= fun () ->
let cons_right = {apply = (fun k -> ICons_right (loc, tl, k))} in
union_t loc tl tr >>?= fun (Ty_ex_c ty) ->
let stack_ty = Item_t (ty, rest) in
typed ctxt loc cons_right stack_ty
| ( Prim (loc, I_IF_LEFT, [bt; bf], annot),
(Item_t (Union_t (tl, tr, _, _), rest) as bef) ) ->
check_kind [Seq_kind] bt >>?= fun () ->
check_kind [Seq_kind] bf >>?= fun () ->
error_unexpected_annot loc annot >>?= fun () ->
non_terminal_recursion tc_context ctxt bt (Item_t (tl, rest))
>>=? fun (btr, ctxt) ->
non_terminal_recursion tc_context ctxt bf (Item_t (tr, rest))
>>=? fun (bfr, ctxt) ->
let branch ibt ibf =
let instr =
{
apply =
(fun k ->
let hloc = kinstr_location k in
let branch_if_left = ibt.instr.apply (IHalt hloc)
and branch_if_right = ibf.instr.apply (IHalt hloc) in
IIf_left {loc; branch_if_left; branch_if_right; k});
}
in
{loc; instr; bef; aft = ibt.aft}
in
Lwt.return @@ merge_branches ctxt loc btr bfr {branch}
(* lists *)
| Prim (loc, I_NIL, [t], annot), stack ->
parse_any_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy t
>>?= fun (Ex_ty t, ctxt) ->
check_var_type_annot loc annot >>?= fun () ->
let nil = {apply = (fun k -> INil (loc, t, k))} in
list_t loc t >>?= fun ty -> typed ctxt loc nil (Item_t (ty, stack))
| ( Prim (loc, I_CONS, [], annot),
Item_t (tv, (Item_t (List_t (t, _), _) as stack)) ) ->
check_item_ty ctxt tv t loc I_CONS 1 2 >>?= fun (Eq, ctxt) ->
check_var_annot loc annot >>?= fun () ->
let cons_list = {apply = (fun k -> ICons_list (loc, k))} in
(typed ctxt loc cons_list stack
: ((a, s) judgement * context) tzresult Lwt.t)
| ( Prim (loc, I_IF_CONS, [bt; bf], annot),
(Item_t (List_t (t, _), rest) as bef) ) ->
check_kind [Seq_kind] bt >>?= fun () ->
check_kind [Seq_kind] bf >>?= fun () ->
error_unexpected_annot loc annot >>?= fun () ->
non_terminal_recursion tc_context ctxt bt (Item_t (t, bef))
>>=? fun (btr, ctxt) ->
non_terminal_recursion tc_context ctxt bf rest >>=? fun (bfr, ctxt) ->
let branch ibt ibf =
let instr =
{
apply =
(fun k ->
let hloc = kinstr_location k in
let branch_if_cons = ibt.instr.apply (IHalt hloc)
and branch_if_nil = ibf.instr.apply (IHalt hloc) in
IIf_cons {loc; branch_if_nil; branch_if_cons; k});
}
in
{loc; instr; bef; aft = ibt.aft}
in
Lwt.return @@ merge_branches ctxt loc btr bfr {branch}
| Prim (loc, I_SIZE, [], annot), Item_t (List_t _, rest) ->
check_var_type_annot loc annot >>?= fun () ->
let list_size = {apply = (fun k -> IList_size (loc, k))} in
typed ctxt loc list_size (Item_t (nat_t, rest))
| Prim (loc, I_MAP, [body], annot), Item_t (List_t (elt, _), starting_rest)
-> (
check_kind [Seq_kind] body >>?= fun () ->
check_var_type_annot loc annot >>?= fun () ->
non_terminal_recursion tc_context ctxt body (Item_t (elt, starting_rest))
>>=? fun (judgement, ctxt) ->
Lwt.return
@@
match judgement with
| Typed ({aft = Item_t (ret, rest) as aft; _} as kibody) ->
let invalid_map_body () =
let aft = serialize_stack_for_error ctxt aft in
Invalid_map_body (loc, aft)
in
record_trace_eval
invalid_map_body
( stack_eq loc ctxt 1 rest starting_rest >>? fun (Eq, ctxt) ->
let hloc = loc in
let ibody = kibody.instr.apply (IHalt hloc) in
list_t loc ret >>? fun ty ->
let list_map =
{
apply =
(fun k -> IList_map (loc, ibody, for_logging_only ty, k));
}
in
let stack = Item_t (ty, rest) in
typed_no_lwt ctxt loc list_map stack )
| Typed {aft; _} ->
let aft = serialize_stack_for_error ctxt aft in
error (Invalid_map_body (loc, aft))
| Failed _ -> error (Invalid_map_block_fail loc))
| Prim (loc, I_ITER, [body], annot), Item_t (List_t (elt, _), rest) -> (
check_kind [Seq_kind] body >>?= fun () ->
error_unexpected_annot loc annot >>?= fun () ->
non_terminal_recursion tc_context ctxt body (Item_t (elt, rest))
>>=? fun (judgement, ctxt) ->
let mk_list_iter ibody =
{
apply =
(fun k ->
let hinfo = loc in
let ibody = ibody.instr.apply (IHalt hinfo) in
IList_iter (loc, for_logging_only elt, ibody, k));
}
in
Lwt.return
@@
match judgement with
| Typed ({aft; _} as ibody) ->
let invalid_iter_body () =
let aft = serialize_stack_for_error ctxt ibody.aft in
let rest = serialize_stack_for_error ctxt rest in
Invalid_iter_body (loc, rest, aft)
in
record_trace_eval
invalid_iter_body
( stack_eq loc ctxt 1 aft rest
>>? fun (Eq, ctxt) : ((a, s) judgement * context) tzresult ->
typed_no_lwt ctxt loc (mk_list_iter ibody) rest )
| Failed {descr} -> typed_no_lwt ctxt loc (mk_list_iter (descr rest)) rest
)
(* sets *)
| Prim (loc, I_EMPTY_SET, [t], annot), rest ->
parse_comparable_ty ~stack_depth:(stack_depth + 1) ctxt t
>>?= fun (Ex_comparable_ty t, ctxt) ->
check_var_type_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IEmpty_set (loc, t, k))} in
set_t loc t >>?= fun ty -> typed ctxt loc instr (Item_t (ty, rest))
| Prim (loc, I_ITER, [body], annot), Item_t (Set_t (elt, _), rest) -> (
check_kind [Seq_kind] body >>?= fun () ->
error_unexpected_annot loc annot >>?= fun () ->
non_terminal_recursion tc_context ctxt body (Item_t (elt, rest))
>>=? fun (judgement, ctxt) ->
let mk_iset_iter ibody =
{
apply =
(fun k ->
let hinfo = loc in
let ibody = ibody.instr.apply (IHalt hinfo) in
ISet_iter (loc, for_logging_only elt, ibody, k));
}
in
Lwt.return
@@
match judgement with
| Typed ({aft; _} as ibody) ->
let invalid_iter_body () =
let aft = serialize_stack_for_error ctxt ibody.aft in
let rest = serialize_stack_for_error ctxt rest in
Invalid_iter_body (loc, rest, aft)
in
record_trace_eval
invalid_iter_body
( stack_eq loc ctxt 1 aft rest
>>? fun (Eq, ctxt) : ((a, s) judgement * context) tzresult ->
typed_no_lwt ctxt loc (mk_iset_iter ibody) rest )
| Failed {descr} -> typed_no_lwt ctxt loc (mk_iset_iter (descr rest)) rest
)
| Prim (loc, I_MEM, [], annot), Item_t (v, Item_t (Set_t (elt, _), rest)) ->
check_var_type_annot loc annot >>?= fun () ->
check_item_ty ctxt elt v loc I_MEM 1 2 >>?= fun (Eq, ctxt) ->
let instr = {apply = (fun k -> ISet_mem (loc, k))} in
(typed ctxt loc instr (Item_t (bool_t, rest))
: ((a, s) judgement * context) tzresult Lwt.t)
| ( Prim (loc, I_UPDATE, [], annot),
Item_t (v, Item_t (Bool_t, (Item_t (Set_t (elt, _), _) as stack))) ) ->
check_item_ty ctxt elt v loc I_UPDATE 1 3 >>?= fun (Eq, ctxt) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISet_update (loc, k))} in
(typed ctxt loc instr stack : ((a, s) judgement * context) tzresult Lwt.t)
| Prim (loc, I_SIZE, [], annot), Item_t (Set_t _, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISet_size (loc, k))} in
typed ctxt loc instr (Item_t (nat_t, rest))
(* maps *)
| Prim (loc, I_EMPTY_MAP, [tk; tv], annot), stack ->
parse_comparable_ty ~stack_depth:(stack_depth + 1) ctxt tk
>>?= fun (Ex_comparable_ty tk, ctxt) ->
parse_any_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy tv
>>?= fun (Ex_ty tv, ctxt) ->
check_var_type_annot loc annot >>?= fun () ->
let instr =
{apply = (fun k -> IEmpty_map (loc, tk, for_logging_only tv, k))}
in
map_t loc tk tv >>?= fun ty -> typed ctxt loc instr (Item_t (ty, stack))
| Prim (loc, I_MAP, [body], annot), Item_t (Map_t (kt, elt, _), starting_rest)
-> (
check_kind [Seq_kind] body >>?= fun () ->
check_var_type_annot loc annot >>?= fun () ->
pair_t loc kt elt >>?= fun (Ty_ex_c ty) ->
non_terminal_recursion tc_context ctxt body (Item_t (ty, starting_rest))
>>=? fun (judgement, ctxt) ->
Lwt.return
@@
match judgement with
| Typed ({aft = Item_t (ret, rest) as aft; _} as ibody) ->
let invalid_map_body () =
let aft = serialize_stack_for_error ctxt aft in
Invalid_map_body (loc, aft)
in
record_trace_eval
invalid_map_body
( stack_eq loc ctxt 1 rest starting_rest >>? fun (Eq, ctxt) ->
map_t loc kt ret >>? fun ty ->
let instr =
{
apply =
(fun k ->
let hinfo = loc in
let ibody = ibody.instr.apply (IHalt hinfo) in
IMap_map (loc, for_logging_only ty, ibody, k));
}
in
let stack = Item_t (ty, rest) in
typed_no_lwt ctxt loc instr stack )
| Typed {aft; _} ->
let aft = serialize_stack_for_error ctxt aft in
error (Invalid_map_body (loc, aft))
| Failed _ -> error (Invalid_map_block_fail loc))
| Prim (loc, I_ITER, [body], annot), Item_t (Map_t (key, element_ty, _), rest)
-> (
check_kind [Seq_kind] body >>?= fun () ->
error_unexpected_annot loc annot >>?= fun () ->
pair_t loc key element_ty >>?= fun (Ty_ex_c ty) ->
non_terminal_recursion tc_context ctxt body (Item_t (ty, rest))
>>=? fun (judgement, ctxt) ->
let make_instr ibody =
{
apply =
(fun k ->
let hinfo = loc in
let ibody = ibody.instr.apply (IHalt hinfo) in
IMap_iter (loc, for_logging_only ty, ibody, k));
}
in
Lwt.return
@@
match judgement with
| Typed ({aft; _} as ibody) ->
let invalid_iter_body () =
let aft = serialize_stack_for_error ctxt ibody.aft in
let rest = serialize_stack_for_error ctxt rest in
Invalid_iter_body (loc, rest, aft)
in
record_trace_eval
invalid_iter_body
( stack_eq loc ctxt 1 aft rest
>>? fun (Eq, ctxt) : ((a, s) judgement * context) tzresult ->
typed_no_lwt ctxt loc (make_instr ibody) rest )
| Failed {descr} -> typed_no_lwt ctxt loc (make_instr (descr rest)) rest)
| Prim (loc, I_MEM, [], annot), Item_t (vk, Item_t (Map_t (k, _, _), rest)) ->
check_item_ty ctxt vk k loc I_MEM 1 2 >>?= fun (Eq, ctxt) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMap_mem (loc, k))} in
(typed ctxt loc instr (Item_t (bool_t, rest))
: ((a, s) judgement * context) tzresult Lwt.t)
| Prim (loc, I_GET, [], annot), Item_t (vk, Item_t (Map_t (k, elt, _), rest))
->
check_item_ty ctxt vk k loc I_GET 1 2 >>?= fun (Eq, ctxt) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMap_get (loc, k))} in
option_t loc elt
>>?= fun ty : ((a, s) judgement * context) tzresult Lwt.t ->
typed ctxt loc instr (Item_t (ty, rest))
| ( Prim (loc, I_UPDATE, [], annot),
Item_t
( vk,
Item_t (Option_t (vv, _, _), (Item_t (Map_t (k, v, _), _) as stack))
) ) ->
check_item_ty ctxt vk k loc I_UPDATE 1 3 >>?= fun (Eq, ctxt) ->
check_item_ty ctxt vv v loc I_UPDATE 2 3 >>?= fun (Eq, ctxt) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMap_update (loc, k))} in
(typed ctxt loc instr stack : ((a, s) judgement * context) tzresult Lwt.t)
| ( Prim (loc, I_GET_AND_UPDATE, [], annot),
Item_t
( vk,
(Item_t (Option_t (vv, _, _), Item_t (Map_t (k, v, _), _)) as stack)
) ) ->
check_item_ty ctxt vk k loc I_GET_AND_UPDATE 1 3 >>?= fun (Eq, ctxt) ->
check_item_ty ctxt vv v loc I_GET_AND_UPDATE 2 3 >>?= fun (Eq, ctxt) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMap_get_and_update (loc, k))} in
(typed ctxt loc instr stack : ((a, s) judgement * context) tzresult Lwt.t)
| Prim (loc, I_SIZE, [], annot), Item_t (Map_t (_, _, _), rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMap_size (loc, k))} in
typed ctxt loc instr (Item_t (nat_t, rest))
(* big_map *)
| Prim (loc, I_EMPTY_BIG_MAP, [tk; tv], annot), stack ->
parse_comparable_ty ~stack_depth:(stack_depth + 1) ctxt tk
>>?= fun (Ex_comparable_ty tk, ctxt) ->
parse_big_map_value_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy tv
>>?= fun (Ex_ty tv, ctxt) ->
check_var_type_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IEmpty_big_map (loc, tk, tv, k))} in
big_map_t loc tk tv >>?= fun ty ->
let stack = Item_t (ty, stack) in
typed ctxt loc instr stack
| ( Prim (loc, I_MEM, [], annot),
Item_t (set_key, Item_t (Big_map_t (k, _, _), rest)) ) ->
check_item_ty ctxt set_key k loc I_MEM 1 2 >>?= fun (Eq, ctxt) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IBig_map_mem (loc, k))} in
let stack = Item_t (bool_t, rest) in
(typed ctxt loc instr stack : ((a, s) judgement * context) tzresult Lwt.t)
| ( Prim (loc, I_GET, [], annot),
Item_t (vk, Item_t (Big_map_t (k, elt, _), rest)) ) ->
check_item_ty ctxt vk k loc I_GET 1 2 >>?= fun (Eq, ctxt) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IBig_map_get (loc, k))} in
option_t loc elt >>?= fun ty ->
let stack = Item_t (ty, rest) in
(typed ctxt loc instr stack : ((a, s) judgement * context) tzresult Lwt.t)
| ( Prim (loc, I_UPDATE, [], annot),
Item_t
( set_key,
Item_t
( Option_t (set_value, _, _),
(Item_t (Big_map_t (map_key, map_value, _), _) as stack) ) ) ) ->
check_item_ty ctxt set_key map_key loc I_UPDATE 1 3 >>?= fun (Eq, ctxt) ->
check_item_ty ctxt set_value map_value loc I_UPDATE 2 3
>>?= fun (Eq, ctxt) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IBig_map_update (loc, k))} in
(typed ctxt loc instr stack : ((a, s) judgement * context) tzresult Lwt.t)
| ( Prim (loc, I_GET_AND_UPDATE, [], annot),
Item_t
( vk,
(Item_t (Option_t (vv, _, _), Item_t (Big_map_t (k, v, _), _)) as
stack) ) ) ->
check_item_ty ctxt vk k loc I_GET_AND_UPDATE 1 3 >>?= fun (Eq, ctxt) ->
check_item_ty ctxt vv v loc I_GET_AND_UPDATE 2 3 >>?= fun (Eq, ctxt) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IBig_map_get_and_update (loc, k))} in
(typed ctxt loc instr stack : ((a, s) judgement * context) tzresult Lwt.t)
(* Sapling *)
| Prim (loc, I_SAPLING_EMPTY_STATE, [memo_size], annot), rest ->
parse_memo_size memo_size >>?= fun memo_size ->
check_var_annot loc annot >>?= fun () ->
let instr =
{apply = (fun k -> ISapling_empty_state (loc, memo_size, k))}
in
let stack = Item_t (sapling_state_t ~memo_size, rest) in
typed ctxt loc instr stack
| ( Prim (loc, I_SAPLING_VERIFY_UPDATE, [], _),
Item_t
( Sapling_transaction_deprecated_t transaction_memo_size,
Item_t ((Sapling_state_t state_memo_size as state_ty), rest) ) ) ->
if legacy then
memo_size_eq
~error_details:(Informative ())
state_memo_size
transaction_memo_size
>>?= fun () ->
let instr =
{apply = (fun k -> ISapling_verify_update_deprecated (loc, k))}
in
pair_t loc int_t state_ty >>?= fun (Ty_ex_c pair_ty) ->
option_t loc pair_ty >>?= fun ty ->
let stack = Item_t (ty, rest) in
typed ctxt loc instr stack
else fail (Deprecated_instruction T_sapling_transaction_deprecated)
| ( Prim (loc, I_SAPLING_VERIFY_UPDATE, [], _),
Item_t
( Sapling_transaction_t transaction_memo_size,
Item_t ((Sapling_state_t state_memo_size as state_ty), rest) ) ) ->
memo_size_eq
~error_details:(Informative ())
state_memo_size
transaction_memo_size
>>?= fun () ->
let instr = {apply = (fun k -> ISapling_verify_update (loc, k))} in
pair_t loc int_t state_ty >>?= fun (Ty_ex_c pair_ty) ->
pair_t loc bytes_t pair_ty >>?= fun (Ty_ex_c pair_ty) ->
option_t loc pair_ty >>?= fun ty ->
let stack = Item_t (ty, rest) in
typed ctxt loc instr stack
(* control *)
| Seq (loc, []), stack ->
let instr = {apply = (fun k -> k)} in
typed ctxt loc instr stack
| Seq (_, [single]), stack ->
non_terminal_recursion tc_context ctxt single stack
| Seq (loc, hd :: tl), stack -> (
non_terminal_recursion tc_context ctxt hd stack
>>=? fun (judgement, ctxt) ->
match judgement with
| Failed _ -> fail (Fail_not_in_tail_position (Micheline.location hd))
| Typed ({aft = middle; _} as ihd) ->
non_terminal_recursion
tc_context
ctxt
(Seq (Micheline.dummy_location, tl))
middle
>|=? fun (judgement, ctxt) ->
let judgement =
match judgement with
| Failed {descr} ->
let descr ret = compose_descr loc ihd (descr ret) in
Failed {descr}
| Typed itl -> Typed (compose_descr loc ihd itl)
in
(judgement, ctxt))
| Prim (loc, I_IF, [bt; bf], annot), (Item_t (Bool_t, rest) as bef) ->
check_kind [Seq_kind] bt >>?= fun () ->
check_kind [Seq_kind] bf >>?= fun () ->
error_unexpected_annot loc annot >>?= fun () ->
non_terminal_recursion tc_context ctxt bt rest >>=? fun (btr, ctxt) ->
non_terminal_recursion tc_context ctxt bf rest >>=? fun (bfr, ctxt) ->
let branch ibt ibf =
let instr =
{
apply =
(fun k ->
let hloc = kinstr_location k in
let branch_if_true = ibt.instr.apply (IHalt hloc)
and branch_if_false = ibf.instr.apply (IHalt hloc) in
IIf {loc; branch_if_true; branch_if_false; k});
}
in
{loc; instr; bef; aft = ibt.aft}
in
Lwt.return @@ merge_branches ctxt loc btr bfr {branch}
| Prim (loc, I_LOOP, [body], annot), (Item_t (Bool_t, rest) as stack) -> (
check_kind [Seq_kind] body >>?= fun () ->
error_unexpected_annot loc annot >>?= fun () ->
non_terminal_recursion tc_context ctxt body rest
>>=? fun (judgement, ctxt) ->
Lwt.return
@@
match judgement with
| Typed ibody ->
let unmatched_branches () =
let aft = serialize_stack_for_error ctxt ibody.aft in
let stack = serialize_stack_for_error ctxt stack in
Unmatched_branches (loc, aft, stack)
in
record_trace_eval
unmatched_branches
( stack_eq loc ctxt 1 ibody.aft stack >>? fun (Eq, ctxt) ->
let instr =
{
apply =
(fun k ->
let loc = kinstr_location k in
let ibody = ibody.instr.apply (IHalt loc) in
ILoop (loc, ibody, k));
}
in
typed_no_lwt ctxt loc instr rest )
| Failed {descr} ->
let instr =
{
apply =
(fun k ->
let loc = kinstr_location k in
let ibody = descr stack in
let ibody = ibody.instr.apply (IHalt loc) in
ILoop (loc, ibody, k));
}
in
typed_no_lwt ctxt loc instr rest)
| ( Prim (loc, I_LOOP_LEFT, [body], annot),
(Item_t (Union_t (tl, tr, _, _), rest) as stack) ) -> (
check_kind [Seq_kind] body >>?= fun () ->
check_var_annot loc annot >>?= fun () ->
non_terminal_recursion tc_context ctxt body (Item_t (tl, rest))
>>=? fun (judgement, ctxt) ->
Lwt.return
@@
match judgement with
| Typed ibody ->
let unmatched_branches () =
let aft = serialize_stack_for_error ctxt ibody.aft in
let stack = serialize_stack_for_error ctxt stack in
Unmatched_branches (loc, aft, stack)
in
record_trace_eval
unmatched_branches
( stack_eq loc ctxt 1 ibody.aft stack >>? fun (Eq, ctxt) ->
let instr =
{
apply =
(fun k ->
let loc = kinstr_location k in
let ibody = ibody.instr.apply (IHalt loc) in
ILoop_left (loc, ibody, k));
}
in
let stack = Item_t (tr, rest) in
typed_no_lwt ctxt loc instr stack )
| Failed {descr} ->
let instr =
{
apply =
(fun k ->
let loc = kinstr_location k in
let ibody = descr stack in
let ibody = ibody.instr.apply (IHalt loc) in
ILoop_left (loc, ibody, k));
}
in
let stack = Item_t (tr, rest) in
typed_no_lwt ctxt loc instr stack)
| Prim (loc, I_LAMBDA, [arg; ret; code], annot), stack ->
parse_any_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy arg
>>?= fun (Ex_ty arg, ctxt) ->
parse_any_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy ret
>>?= fun (Ex_ty ret, ctxt) ->
check_kind [Seq_kind] code >>?= fun () ->
check_var_annot loc annot >>?= fun () ->
parse_kdescr
(Tc_context.add_lambda tc_context)
~elab_conf
~stack_depth:(stack_depth + 1)
ctxt
arg
ret
code
>>=? fun (kdescr, ctxt) ->
let instr = {apply = (fun k -> ILambda (loc, Lam (kdescr, code), k))} in
lambda_t loc arg ret >>?= fun ty ->
let stack = Item_t (ty, stack) in
typed ctxt loc instr stack
| ( Prim (loc, I_LAMBDA_REC, [arg_ty_expr; ret_ty_expr; lambda_expr], annot),
stack ) ->
parse_any_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy arg_ty_expr
>>?= fun (Ex_ty arg, ctxt) ->
parse_any_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy ret_ty_expr
>>?= fun (Ex_ty ret, ctxt) ->
check_kind [Seq_kind] lambda_expr >>?= fun () ->
check_var_annot loc annot >>?= fun () ->
lambda_t loc arg ret >>?= fun lambda_rec_ty ->
parse_lam_rec
Tc_context.(add_lambda tc_context)
~elab_conf
~stack_depth:(stack_depth + 1)
ctxt
arg
ret
lambda_rec_ty
lambda_expr
>>=? fun (code, ctxt) ->
let instr = {apply = (fun k -> ILambda (loc, code, k))} in
let stack = Item_t (lambda_rec_ty, stack) in
typed ctxt loc instr stack
| ( Prim (loc, I_EXEC, [], annot),
Item_t (arg, Item_t (Lambda_t (param, ret, _), rest)) ) ->
check_item_ty ctxt arg param loc I_EXEC 1 2 >>?= fun (Eq, ctxt) ->
check_var_annot loc annot >>?= fun () ->
let stack = Item_t (ret, rest) in
let instr = {apply = (fun k -> IExec (loc, for_logging_only stack, k))} in
(typed ctxt loc instr stack : ((a, s) judgement * context) tzresult Lwt.t)
| ( Prim (loc, I_APPLY, [], annot),
Item_t
( capture,
Item_t (Lambda_t (Pair_t (capture_ty, arg_ty, _, _), ret, _), rest) )
) ->
check_packable ~legacy:false loc capture_ty >>?= fun () ->
check_item_ty ctxt capture capture_ty loc I_APPLY 1 2
>>?= fun (Eq, ctxt) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IApply (loc, capture_ty, k))} in
lambda_t loc arg_ty ret
(* This cannot fail because the type [lambda 'arg 'ret] is always smaller than
the input type [lambda (pair 'arg 'capture) 'ret]. In an ideal world, there
would be a smart deconstructor to ensure this statically. *)
>>?=
fun res_ty ->
let stack = Item_t (res_ty, rest) in
(typed ctxt loc instr stack : ((a, s) judgement * context) tzresult Lwt.t)
| Prim (loc, I_DIP, [code], annot), Item_t (v, rest) -> (
error_unexpected_annot loc annot >>?= fun () ->
check_kind [Seq_kind] code >>?= fun () ->
non_terminal_recursion tc_context ctxt code rest
>>=? fun (judgement, ctxt) ->
match judgement with
| Typed descr ->
let instr =
{
apply =
(fun k ->
let b = descr.instr.apply (IHalt descr.loc) in
IDip (loc, b, for_logging_only v, k));
}
in
let stack = Item_t (v, descr.aft) in
typed ctxt loc instr stack
| Failed _ -> fail (Fail_not_in_tail_position loc))
| Prim (loc, I_DIP, [n; code], result_annot), stack ->
parse_uint10 n >>?= fun n ->
Gas.consume ctxt (Typecheck_costs.proof_argument n) >>?= fun ctxt ->
let rec make_proof_argument :
type a s.
int -> (a, s) stack_ty -> (a, s) dipn_proof_argument tzresult Lwt.t =
fun n stk ->
match (Compare.Int.(n = 0), stk) with
| true, rest -> (
non_terminal_recursion tc_context ctxt code rest
>>=? fun (judgement, ctxt) ->
Lwt.return
@@
match judgement with
| Typed descr ->
ok
(Dipn_proof_argument (KRest, ctxt, descr, descr.aft)
: (a, s) dipn_proof_argument)
| Failed _ -> error (Fail_not_in_tail_position loc))
| false, Item_t (v, rest) ->
make_proof_argument (n - 1) rest
>|=? fun (Dipn_proof_argument (n', ctxt, descr, aft')) ->
let w = KPrefix (loc, v, n') in
Dipn_proof_argument (w, ctxt, descr, Item_t (v, aft'))
| _, _ ->
Lwt.return
(let whole_stack = serialize_stack_for_error ctxt stack in
error (Bad_stack (loc, I_DIP, 1, whole_stack)))
in
error_unexpected_annot loc result_annot >>?= fun () ->
make_proof_argument n stack
>>=? fun (Dipn_proof_argument (n', ctxt, descr, aft)) ->
let b = descr.instr.apply (IHalt descr.loc) in
let res = {apply = (fun k -> IDipn (loc, n, n', b, k))} in
typed ctxt loc res aft
| Prim (loc, I_DIP, (([] | _ :: _ :: _ :: _) as l), _), _ ->
(* Technically, the arities 1 and 2 are allowed but the error only mentions 2.
However, DIP {code} is equivalent to DIP 1 {code} so hinting at an arity of 2 makes sense. *)
fail (Invalid_arity (loc, I_DIP, 2, List.length l))
| Prim (loc, I_FAILWITH, [], annot), Item_t (v, _rest) ->
Lwt.return
( error_unexpected_annot loc annot >>? fun () ->
(if legacy then Result.return_unit
else check_packable ~legacy:false loc v)
>|? fun () ->
let instr = {apply = (fun _k -> IFailwith (loc, v))} in
let descr aft = {loc; instr; bef = stack_ty; aft} in
log_stack loc stack_ty Bot_t ;
(Failed {descr}, ctxt) )
| Prim (loc, I_NEVER, [], annot), Item_t (Never_t, _rest) ->
Lwt.return
( error_unexpected_annot loc annot >|? fun () ->
let instr = {apply = (fun _k -> INever loc)} in
let descr aft = {loc; instr; bef = stack_ty; aft} in
log_stack loc stack_ty Bot_t ;
(Failed {descr}, ctxt) )
(* timestamp operations *)
| Prim (loc, I_ADD, [], annot), Item_t (Timestamp_t, Item_t (Int_t, rest)) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IAdd_timestamp_to_seconds (loc, k))} in
typed ctxt loc instr (Item_t (Timestamp_t, rest))
| ( Prim (loc, I_ADD, [], annot),
Item_t (Int_t, (Item_t (Timestamp_t, _) as stack)) ) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IAdd_seconds_to_timestamp (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_SUB, [], annot), Item_t (Timestamp_t, Item_t (Int_t, rest)) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISub_timestamp_seconds (loc, k))} in
let stack = Item_t (Timestamp_t, rest) in
typed ctxt loc instr stack
| ( Prim (loc, I_SUB, [], annot),
Item_t (Timestamp_t, Item_t (Timestamp_t, rest)) ) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IDiff_timestamps (loc, k))} in
let stack = Item_t (int_t, rest) in
typed ctxt loc instr stack
(* string operations *)
| ( Prim (loc, I_CONCAT, [], annot),
Item_t (String_t, (Item_t (String_t, _) as stack)) ) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IConcat_string_pair (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_CONCAT, [], annot), Item_t (List_t (String_t, _), rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IConcat_string (loc, k))} in
typed ctxt loc instr (Item_t (String_t, rest))
| ( Prim (loc, I_SLICE, [], annot),
Item_t (Nat_t, Item_t (Nat_t, Item_t (String_t, rest))) ) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISlice_string (loc, k))} in
let stack = Item_t (option_string_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_SIZE, [], annot), Item_t (String_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IString_size (loc, k))} in
let stack = Item_t (nat_t, rest) in
typed ctxt loc instr stack
(* bytes operations *)
| ( Prim (loc, I_CONCAT, [], annot),
Item_t (Bytes_t, (Item_t (Bytes_t, _) as stack)) ) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IConcat_bytes_pair (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_CONCAT, [], annot), Item_t (List_t (Bytes_t, _), rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IConcat_bytes (loc, k))} in
let stack = Item_t (Bytes_t, rest) in
typed ctxt loc instr stack
| ( Prim (loc, I_SLICE, [], annot),
Item_t (Nat_t, Item_t (Nat_t, Item_t (Bytes_t, rest))) ) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISlice_bytes (loc, k))} in
let stack = Item_t (option_bytes_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_SIZE, [], annot), Item_t (Bytes_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IBytes_size (loc, k))} in
let stack = Item_t (nat_t, rest) in
typed ctxt loc instr stack
(* currency operations *)
| ( Prim (loc, I_ADD, [], annot),
Item_t (Mutez_t, (Item_t (Mutez_t, _) as stack)) ) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IAdd_tez (loc, k))} in
typed ctxt loc instr stack
| ( Prim (loc, I_SUB, [], annot),
Item_t (Mutez_t, (Item_t (Mutez_t, _) as stack)) ) ->
if legacy then
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISub_tez_legacy (loc, k))} in
typed ctxt loc instr stack
else fail (Deprecated_instruction I_SUB)
| Prim (loc, I_SUB_MUTEZ, [], annot), Item_t (Mutez_t, Item_t (Mutez_t, rest))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISub_tez (loc, k))} in
let stack = Item_t (option_mutez_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_MUL, [], annot), Item_t (Mutez_t, Item_t (Nat_t, rest)) ->
(* no type name check *)
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMul_teznat (loc, k))} in
let stack = Item_t (Mutez_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_MUL, [], annot), Item_t (Nat_t, (Item_t (Mutez_t, _) as stack))
->
(* no type name check *)
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMul_nattez (loc, k))} in
typed ctxt loc instr stack
(* boolean operations *)
| Prim (loc, I_OR, [], annot), Item_t (Bool_t, (Item_t (Bool_t, _) as stack))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IOr (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_AND, [], annot), Item_t (Bool_t, (Item_t (Bool_t, _) as stack))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IAnd (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_XOR, [], annot), Item_t (Bool_t, (Item_t (Bool_t, _) as stack))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IXor (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_NOT, [], annot), (Item_t (Bool_t, _) as stack) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> INot (loc, k))} in
typed ctxt loc instr stack
(* integer operations *)
| Prim (loc, I_ABS, [], annot), Item_t (Int_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IAbs_int (loc, k))} in
let stack = Item_t (nat_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_ISNAT, [], annot), Item_t (Int_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IIs_nat (loc, k))} in
let stack = Item_t (option_nat_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_INT, [], annot), Item_t (Nat_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IInt_nat (loc, k))} in
let stack = Item_t (int_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_NEG, [], annot), (Item_t (Int_t, _) as stack) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> INeg (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_NEG, [], annot), Item_t (Nat_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> INeg (loc, k))} in
let stack = Item_t (int_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_ADD, [], annot), Item_t (Int_t, (Item_t (Int_t, _) as stack))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IAdd_int (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_ADD, [], annot), Item_t (Int_t, Item_t (Nat_t, rest)) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IAdd_int (loc, k))} in
let stack = Item_t (Int_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_ADD, [], annot), Item_t (Nat_t, (Item_t (Int_t, _) as stack))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IAdd_int (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_ADD, [], annot), Item_t (Nat_t, (Item_t (Nat_t, _) as stack))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IAdd_nat (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_SUB, [], annot), Item_t (Int_t, (Item_t (Int_t, _) as stack))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISub_int (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_SUB, [], annot), Item_t (Int_t, Item_t (Nat_t, rest)) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISub_int (loc, k))} in
let stack = Item_t (Int_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_SUB, [], annot), Item_t (Nat_t, (Item_t (Int_t, _) as stack))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISub_int (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_SUB, [], annot), Item_t (Nat_t, Item_t (Nat_t, rest)) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISub_int (loc, k))} in
let stack = Item_t (int_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_MUL, [], annot), Item_t (Int_t, (Item_t (Int_t, _) as stack))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMul_int (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_MUL, [], annot), Item_t (Int_t, Item_t (Nat_t, rest)) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMul_int (loc, k))} in
let stack = Item_t (Int_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_MUL, [], annot), Item_t (Nat_t, (Item_t (Int_t, _) as stack))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMul_nat (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_MUL, [], annot), Item_t (Nat_t, (Item_t (Nat_t, _) as stack))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMul_nat (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_EDIV, [], annot), Item_t (Mutez_t, Item_t (Nat_t, rest)) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IEdiv_teznat (loc, k))} in
let stack = Item_t (option_pair_mutez_mutez_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_EDIV, [], annot), Item_t (Mutez_t, Item_t (Mutez_t, rest)) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IEdiv_tez (loc, k))} in
let stack = Item_t (option_pair_nat_mutez_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_EDIV, [], annot), Item_t (Int_t, Item_t (Int_t, rest)) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IEdiv_int (loc, k))} in
let stack = Item_t (option_pair_int_nat_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_EDIV, [], annot), Item_t (Int_t, Item_t (Nat_t, rest)) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IEdiv_int (loc, k))} in
let stack = Item_t (option_pair_int_nat_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_EDIV, [], annot), Item_t (Nat_t, Item_t (Int_t, rest)) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IEdiv_nat (loc, k))} in
let stack = Item_t (option_pair_int_nat_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_EDIV, [], annot), Item_t (Nat_t, Item_t (Nat_t, rest)) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IEdiv_nat (loc, k))} in
let stack = Item_t (option_pair_nat_nat_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_LSL, [], annot), Item_t (Nat_t, (Item_t (Nat_t, _) as stack))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ILsl_nat (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_LSR, [], annot), Item_t (Nat_t, (Item_t (Nat_t, _) as stack))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ILsr_nat (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_OR, [], annot), Item_t (Nat_t, (Item_t (Nat_t, _) as stack)) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IOr_nat (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_AND, [], annot), Item_t (Nat_t, (Item_t (Nat_t, _) as stack))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IAnd_nat (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_AND, [], annot), Item_t (Int_t, (Item_t (Nat_t, _) as stack))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IAnd_int_nat (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_XOR, [], annot), Item_t (Nat_t, (Item_t (Nat_t, _) as stack))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IXor_nat (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_NOT, [], annot), (Item_t (Int_t, _) as stack) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> INot_int (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_NOT, [], annot), Item_t (Nat_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> INot_int (loc, k))} in
let stack = Item_t (int_t, rest) in
typed ctxt loc instr stack
(* comparison *)
| Prim (loc, I_COMPARE, [], annot), Item_t (t1, Item_t (t2, rest)) ->
check_var_annot loc annot >>?= fun () ->
check_item_ty ctxt t1 t2 loc I_COMPARE 1 2 >>?= fun (Eq, ctxt) ->
check_comparable loc t1 >>?= fun Eq ->
let instr = {apply = (fun k -> ICompare (loc, t1, k))} in
let stack = Item_t (int_t, rest) in
(typed ctxt loc instr stack : ((a, s) judgement * context) tzresult Lwt.t)
(* comparators *)
| Prim (loc, I_EQ, [], annot), Item_t (Int_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IEq (loc, k))} in
let stack = Item_t (bool_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_NEQ, [], annot), Item_t (Int_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> INeq (loc, k))} in
let stack = Item_t (bool_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_LT, [], annot), Item_t (Int_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ILt (loc, k))} in
let stack = Item_t (bool_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_GT, [], annot), Item_t (Int_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IGt (loc, k))} in
let stack = Item_t (bool_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_LE, [], annot), Item_t (Int_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ILe (loc, k))} in
let stack = Item_t (bool_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_GE, [], annot), Item_t (Int_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IGe (loc, k))} in
let stack = Item_t (bool_t, rest) in
typed ctxt loc instr stack
(* annotations *)
| Prim (loc, I_CAST, [cast_t], annot), (Item_t (t, _) as stack) ->
check_var_annot loc annot >>?= fun () ->
parse_any_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy cast_t
>>?= fun (Ex_ty cast_t, ctxt) ->
Gas_monad.run ctxt @@ ty_eq ~error_details:(Informative loc) cast_t t
>>?= fun (eq, ctxt) ->
eq >>?= fun Eq ->
(* We can reuse [stack] because [a ty = b ty] means [a = b]. *)
let instr = {apply = (fun k -> k)} in
(typed ctxt loc instr stack : ((a, s) judgement * context) tzresult Lwt.t)
| Prim (loc, I_RENAME, [], annot), (Item_t _ as stack) ->
check_var_annot loc annot >>?= fun () ->
(* can erase annot *)
let instr = {apply = (fun k -> k)} in
typed ctxt loc instr stack
(* packing *)
| Prim (loc, I_PACK, [], annot), Item_t (t, rest) ->
check_packable
~legacy:true
(* allow to pack contracts for hash/signature checks *) loc
t
>>?= fun () ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IPack (loc, t, k))} in
let stack = Item_t (bytes_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_UNPACK, [ty], annot), Item_t (Bytes_t, rest) ->
parse_packable_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy ty
>>?= fun (Ex_ty t, ctxt) ->
check_var_type_annot loc annot >>?= fun () ->
option_t loc t >>?= fun res_ty ->
let instr = {apply = (fun k -> IUnpack (loc, t, k))} in
let stack = Item_t (res_ty, rest) in
typed ctxt loc instr stack
(* protocol *)
| Prim (loc, I_ADDRESS, [], annot), Item_t (Contract_t _, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IAddress (loc, k))} in
let stack = Item_t (address_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_CONTRACT, [ty], annot), Item_t (Address_t, rest) ->
parse_passable_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy ty
>>?= fun (Ex_ty t, ctxt) ->
contract_t loc t >>?= fun contract_ty ->
option_t loc contract_ty >>?= fun res_ty ->
parse_entrypoint_annot_strict loc annot >>?= fun entrypoint ->
let instr = {apply = (fun k -> IContract (loc, t, entrypoint, k))} in
let stack = Item_t (res_ty, rest) in
typed ctxt loc instr stack
| ( Prim (loc, I_VIEW, [name; output_ty], annot),
Item_t (input_ty, Item_t (Address_t, rest)) ) ->
let output_ty_loc = location output_ty in
parse_view_name ctxt name >>?= fun (name, ctxt) ->
parse_view_output_ty ctxt ~stack_depth:0 ~legacy output_ty
>>?= fun (Ex_ty output_ty, ctxt) ->
option_t output_ty_loc output_ty >>?= fun res_ty ->
check_var_annot loc annot >>?= fun () ->
let instr =
{
apply =
(fun k ->
IView
( loc,
View_signature {name; input_ty; output_ty},
for_logging_only rest,
k ));
}
in
let stack = Item_t (res_ty, rest) in
typed ctxt loc instr stack
| ( Prim (loc, (I_TRANSFER_TOKENS as prim), [], annot),
Item_t (p, Item_t (Mutez_t, Item_t (Contract_t (cp, _), rest))) ) ->
Tc_context.check_not_in_view loc ~legacy tc_context prim >>?= fun () ->
check_item_ty ctxt p cp loc prim 1 4 >>?= fun (Eq, ctxt) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ITransfer_tokens (loc, k))} in
let stack = Item_t (operation_t, rest) in
(typed ctxt loc instr stack : ((a, s) judgement * context) tzresult Lwt.t)
| ( Prim (loc, (I_SET_DELEGATE as prim), [], annot),
Item_t (Option_t (Key_hash_t, _, _), rest) ) ->
Tc_context.check_not_in_view loc ~legacy tc_context prim >>?= fun () ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISet_delegate (loc, k))} in
let stack = Item_t (operation_t, rest) in
typed ctxt loc instr stack
| Prim (_, I_CREATE_ACCOUNT, _, _), _ ->
fail (Deprecated_instruction I_CREATE_ACCOUNT)
| Prim (loc, I_IMPLICIT_ACCOUNT, [], annot), Item_t (Key_hash_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IImplicit_account (loc, k))} in
let stack = Item_t (contract_unit_t, rest) in
typed ctxt loc instr stack
| ( Prim (loc, (I_CREATE_CONTRACT as prim), [(Seq _ as code)], annot),
Item_t
(Option_t (Key_hash_t, _, _), Item_t (Mutez_t, Item_t (ginit, rest))) )
-> (
Tc_context.check_not_in_view ~legacy loc tc_context prim >>?= fun () ->
check_two_var_annot loc annot >>?= fun () ->
(* We typecheck the script to make sure we will originate only well-typed
contracts but then we throw away the typed version, except for the
storage type which is kept for efficiency in the ticket scanner. *)
let canonical_code = Micheline.strip_locations code in
parse_toplevel ctxt ~legacy canonical_code
>>?= fun ({arg_type; storage_type; code_field; views}, ctxt) ->
record_trace
(Ill_formed_type (Some "parameter", canonical_code, location arg_type))
(parse_parameter_ty_and_entrypoints
ctxt
~stack_depth:(stack_depth + 1)
~legacy
arg_type)
>>?= fun (Ex_parameter_ty_and_entrypoints {arg_type; entrypoints}, ctxt)
->
record_trace
(Ill_formed_type (Some "storage", canonical_code, location storage_type))
(parse_storage_ty
ctxt
~stack_depth:(stack_depth + 1)
~legacy
storage_type)
>>?= fun (Ex_ty storage_type, ctxt) ->
pair_t loc arg_type storage_type >>?= fun (Ty_ex_c arg_type_full) ->
pair_t loc list_operation_t storage_type
>>?= fun (Ty_ex_c ret_type_full) ->
trace
(Ill_typed_contract (canonical_code, []))
(parse_kdescr
(Tc_context.toplevel ~storage_type ~param_type:arg_type ~entrypoints)
ctxt
~elab_conf
~stack_depth:(stack_depth + 1)
arg_type_full
ret_type_full
code_field)
>>=? function
| {kbef = Item_t (arg, Bot_t); kaft = Item_t (ret, Bot_t); _}, ctxt ->
let views_result = parse_views ctxt ~elab_conf storage_type views in
trace (Ill_typed_contract (canonical_code, [])) views_result
>>=? fun (_typed_views, ctxt) ->
(let error_details = Informative loc in
Gas_monad.run ctxt
@@
let open Gas_monad.Syntax in
let* Eq = ty_eq ~error_details arg arg_type_full in
let* Eq = ty_eq ~error_details ret ret_type_full in
ty_eq ~error_details storage_type ginit)
>>?= fun (storage_eq, ctxt) ->
storage_eq >>?= fun Eq ->
let instr =
{
apply =
(fun k ->
ICreate_contract {loc; storage_type; code = canonical_code; k});
}
in
let stack = Item_t (operation_t, Item_t (address_t, rest)) in
typed ctxt loc instr stack)
| Prim (loc, I_NOW, [], annot), stack ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> INow (loc, k))} in
let stack = Item_t (timestamp_t, stack) in
typed ctxt loc instr stack
| Prim (loc, I_MIN_BLOCK_TIME, [], _), stack ->
typed
ctxt
loc
{apply = (fun k -> IMin_block_time (loc, k))}
(Item_t (nat_t, stack))
| Prim (loc, I_AMOUNT, [], annot), stack ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IAmount (loc, k))} in
let stack = Item_t (mutez_t, stack) in
typed ctxt loc instr stack
| Prim (loc, I_CHAIN_ID, [], annot), stack ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IChainId (loc, k))} in
let stack = Item_t (chain_id_t, stack) in
typed ctxt loc instr stack
| Prim (loc, I_BALANCE, [], annot), stack ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IBalance (loc, k))} in
let stack = Item_t (mutez_t, stack) in
typed ctxt loc instr stack
| Prim (loc, I_LEVEL, [], annot), stack ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ILevel (loc, k))} in
let stack = Item_t (nat_t, stack) in
typed ctxt loc instr stack
| Prim (loc, I_VOTING_POWER, [], annot), Item_t (Key_hash_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IVoting_power (loc, k))} in
let stack = Item_t (nat_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_TOTAL_VOTING_POWER, [], annot), stack ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ITotal_voting_power (loc, k))} in
let stack = Item_t (nat_t, stack) in
typed ctxt loc instr stack
| Prim (_, I_STEPS_TO_QUOTA, _, _), _ ->
fail (Deprecated_instruction I_STEPS_TO_QUOTA)
| Prim (loc, I_SOURCE, [], annot), stack ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISource (loc, k))} in
let stack = Item_t (address_t, stack) in
typed ctxt loc instr stack
| Prim (loc, I_SENDER, [], annot), stack ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISender (loc, k))} in
let stack = Item_t (address_t, stack) in
typed ctxt loc instr stack
| Prim (loc, (I_SELF as prim), [], annot), stack ->
Lwt.return
( parse_entrypoint_annot_lax loc annot >>? fun entrypoint ->
let open Tc_context in
match tc_context.callsite with
| _ when is_in_lambda tc_context ->
error
(Forbidden_instr_in_context (loc, Script_tc_errors.Lambda, prim))
(* [Data] is for pushed instructions of lambda type. *)
| Data ->
error
(Forbidden_instr_in_context (loc, Script_tc_errors.Lambda, prim))
| View ->
error
(Forbidden_instr_in_context (loc, Script_tc_errors.View, prim))
| Toplevel {param_type; entrypoints; storage_type = _} ->
Gas_monad.run ctxt
@@ find_entrypoint
~error_details:(Informative ())
param_type
entrypoints
entrypoint
>>? fun (r, ctxt) ->
r >>? fun (Ex_ty_cstr {ty = param_type; _}) ->
contract_t loc param_type >>? fun res_ty ->
let instr =
{apply = (fun k -> ISelf (loc, param_type, entrypoint, k))}
in
let stack = Item_t (res_ty, stack) in
typed_no_lwt ctxt loc instr stack )
| Prim (loc, I_SELF_ADDRESS, [], annot), stack ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISelf_address (loc, k))} in
let stack = Item_t (address_t, stack) in
typed ctxt loc instr stack
(* cryptography *)
| Prim (loc, I_HASH_KEY, [], annot), Item_t (Key_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IHash_key (loc, k))} in
let stack = Item_t (key_hash_t, rest) in
typed ctxt loc instr stack
| ( Prim (loc, I_CHECK_SIGNATURE, [], annot),
Item_t (Key_t, Item_t (Signature_t, Item_t (Bytes_t, rest))) ) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ICheck_signature (loc, k))} in
let stack = Item_t (bool_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_BLAKE2B, [], annot), (Item_t (Bytes_t, _) as stack) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IBlake2b (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_SHA256, [], annot), (Item_t (Bytes_t, _) as stack) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISha256 (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_SHA512, [], annot), (Item_t (Bytes_t, _) as stack) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISha512 (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_KECCAK, [], annot), (Item_t (Bytes_t, _) as stack) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IKeccak (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_SHA3, [], annot), (Item_t (Bytes_t, _) as stack) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> ISha3 (loc, k))} in
typed ctxt loc instr stack
| ( Prim (loc, I_ADD, [], annot),
Item_t (Bls12_381_g1_t, (Item_t (Bls12_381_g1_t, _) as stack)) ) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IAdd_bls12_381_g1 (loc, k))} in
typed ctxt loc instr stack
| ( Prim (loc, I_ADD, [], annot),
Item_t (Bls12_381_g2_t, (Item_t (Bls12_381_g2_t, _) as stack)) ) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IAdd_bls12_381_g2 (loc, k))} in
typed ctxt loc instr stack
| ( Prim (loc, I_ADD, [], annot),
Item_t (Bls12_381_fr_t, (Item_t (Bls12_381_fr_t, _) as stack)) ) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IAdd_bls12_381_fr (loc, k))} in
typed ctxt loc instr stack
| ( Prim (loc, I_MUL, [], annot),
Item_t (Bls12_381_g1_t, Item_t (Bls12_381_fr_t, rest)) ) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMul_bls12_381_g1 (loc, k))} in
let stack = Item_t (Bls12_381_g1_t, rest) in
typed ctxt loc instr stack
| ( Prim (loc, I_MUL, [], annot),
Item_t (Bls12_381_g2_t, Item_t (Bls12_381_fr_t, rest)) ) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMul_bls12_381_g2 (loc, k))} in
let stack = Item_t (Bls12_381_g2_t, rest) in
typed ctxt loc instr stack
| ( Prim (loc, I_MUL, [], annot),
Item_t (Bls12_381_fr_t, (Item_t (Bls12_381_fr_t, _) as stack)) ) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMul_bls12_381_fr (loc, k))} in
typed ctxt loc instr stack
| ( Prim (loc, I_MUL, [], annot),
Item_t (Nat_t, (Item_t (Bls12_381_fr_t, _) as stack)) ) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMul_bls12_381_fr_z (loc, k))} in
typed ctxt loc instr stack
| ( Prim (loc, I_MUL, [], annot),
Item_t (Int_t, (Item_t (Bls12_381_fr_t, _) as stack)) ) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMul_bls12_381_fr_z (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_MUL, [], annot), Item_t (Bls12_381_fr_t, Item_t (Int_t, rest))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMul_bls12_381_z_fr (loc, k))} in
let stack = Item_t (Bls12_381_fr_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_MUL, [], annot), Item_t (Bls12_381_fr_t, Item_t (Nat_t, rest))
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IMul_bls12_381_z_fr (loc, k))} in
let stack = Item_t (Bls12_381_fr_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_INT, [], annot), Item_t (Bls12_381_fr_t, rest) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IInt_bls12_381_fr (loc, k))} in
let stack = Item_t (int_t, rest) in
typed ctxt loc instr stack
| Prim (loc, I_NEG, [], annot), (Item_t (Bls12_381_g1_t, _) as stack) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> INeg_bls12_381_g1 (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_NEG, [], annot), (Item_t (Bls12_381_g2_t, _) as stack) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> INeg_bls12_381_g2 (loc, k))} in
typed ctxt loc instr stack
| Prim (loc, I_NEG, [], annot), (Item_t (Bls12_381_fr_t, _) as stack) ->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> INeg_bls12_381_fr (loc, k))} in
typed ctxt loc instr stack
| ( Prim (loc, I_PAIRING_CHECK, [], annot),
Item_t (List_t (Pair_t (Bls12_381_g1_t, Bls12_381_g2_t, _, _), _), rest) )
->
check_var_annot loc annot >>?= fun () ->
let instr = {apply = (fun k -> IPairing_check_bls12_381 (loc, k))} in
let stack = Item_t (bool_t, rest) in
typed ctxt loc instr stack
(* Tickets *)
| Prim (loc, I_TICKET, [], annot), Item_t (t, Item_t (Nat_t, rest)) ->
check_var_annot loc annot >>?= fun () ->
check_comparable loc t >>?= fun Eq ->
ticket_t loc t >>?= fun res_ty ->
let instr = {apply = (fun k -> ITicket (loc, for_logging_only t, k))} in
let stack = Item_t (res_ty, rest) in
typed ctxt loc instr stack
| ( Prim (loc, I_READ_TICKET, [], annot),
(Item_t (Ticket_t (t, _), _) as full_stack) ) ->
check_var_annot loc annot >>?= fun () ->
let () = check_dupable_comparable_ty t in
opened_ticket_type loc t >>?= fun result ->
let instr =
{apply = (fun k -> IRead_ticket (loc, for_logging_only t, k))}
in
let stack = Item_t (result, full_stack) in
typed ctxt loc instr stack
| ( Prim (loc, I_SPLIT_TICKET, [], annot),
Item_t
( (Ticket_t (t, _) as ticket_t),
Item_t (Pair_t (Nat_t, Nat_t, _, _), rest) ) ) ->
check_var_annot loc annot >>?= fun () ->
let () = check_dupable_comparable_ty t in
pair_t loc ticket_t ticket_t >>?= fun (Ty_ex_c pair_tickets_ty) ->
option_t loc pair_tickets_ty >>?= fun res_ty ->
let instr = {apply = (fun k -> ISplit_ticket (loc, k))} in
let stack = Item_t (res_ty, rest) in
typed ctxt loc instr stack
| ( Prim (loc, I_JOIN_TICKETS, [], annot),
Item_t
( Pair_t
( (Ticket_t (contents_ty_a, _) as ty_a),
Ticket_t (contents_ty_b, _),
_,
_ ),
rest ) ) ->
check_var_annot loc annot >>?= fun () ->
Gas_monad.run ctxt
@@ ty_eq ~error_details:(Informative loc) contents_ty_a contents_ty_b
>>?= fun (eq, ctxt) ->
eq >>?= fun Eq ->
option_t loc ty_a >>?= fun res_ty ->
let instr = {apply = (fun k -> IJoin_tickets (loc, contents_ty_a, k))} in
let stack = Item_t (res_ty, rest) in
typed ctxt loc instr stack
(* Timelocks *)
| ( Prim (loc, I_OPEN_CHEST, [], _),
Item_t (Chest_key_t, Item_t (Chest_t, Item_t (Nat_t, rest))) ) ->
let instr = {apply = (fun k -> IOpen_chest (loc, k))} in
typed ctxt loc instr (Item_t (union_bytes_bool_t, rest))
(* Events *)
| Prim (loc, I_EMIT, [], annot), Item_t (data, rest) ->
check_packable ~legacy loc data >>?= fun () ->
parse_entrypoint_annot_strict loc annot >>?= fun tag ->
unparse_ty ~loc:() ctxt data >>?= fun (unparsed_ty, ctxt) ->
Gas.consume ctxt (Script.strip_locations_cost unparsed_ty)
>>?= fun ctxt ->
let unparsed_ty = Micheline.strip_locations unparsed_ty in
let instr =
{apply = (fun k -> IEmit {loc; tag; ty = data; unparsed_ty; k})}
in
typed ctxt loc instr (Item_t (Operation_t, rest))
| Prim (loc, I_EMIT, [ty_node], annot), Item_t (data, rest) ->
parse_packable_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy ty_node
>>?= fun (Ex_ty ty, ctxt) ->
check_item_ty ctxt ty data loc I_EMIT 1 2 >>?= fun (Eq, ctxt) ->
parse_entrypoint_annot_strict loc annot >>?= fun tag ->
Gas.consume ctxt (Script.strip_locations_cost ty_node) >>?= fun ctxt ->
let unparsed_ty = Micheline.strip_locations ty_node in
let instr =
{apply = (fun k -> IEmit {loc; tag; ty = data; unparsed_ty; k})}
in
typed ctxt loc instr (Item_t (Operation_t, rest))
(* Primitive parsing errors *)
| ( Prim
( loc,
(( I_DUP | I_SWAP | I_SOME | I_UNIT | I_PAIR | I_UNPAIR | I_CAR
| I_CDR | I_CONS | I_CONCAT | I_SLICE | I_MEM | I_UPDATE | I_GET
| I_EXEC | I_FAILWITH | I_SIZE | I_ADD | I_SUB | I_SUB_MUTEZ | I_MUL
| I_EDIV | I_OR | I_AND | I_XOR | I_NOT | I_ABS | I_NEG | I_LSL
| I_LSR | I_COMPARE | I_EQ | I_NEQ | I_LT | I_GT | I_LE | I_GE
| I_TRANSFER_TOKENS | I_SET_DELEGATE | I_NOW | I_MIN_BLOCK_TIME
| I_IMPLICIT_ACCOUNT | I_AMOUNT | I_BALANCE | I_LEVEL
| I_CHECK_SIGNATURE | I_HASH_KEY | I_SOURCE | I_SENDER | I_BLAKE2B
| I_SHA256 | I_SHA512 | I_ADDRESS | I_RENAME | I_PACK | I_ISNAT
| I_INT | I_SELF | I_CHAIN_ID | I_NEVER | I_VOTING_POWER
| I_TOTAL_VOTING_POWER | I_KECCAK | I_SHA3 | I_PAIRING_CHECK
| I_TICKET | I_READ_TICKET | I_SPLIT_TICKET | I_JOIN_TICKETS
| I_OPEN_CHEST ) as name),
(_ :: _ as l),
_ ),
_ ) ->
fail (Invalid_arity (loc, name, 0, List.length l))
| ( Prim
( loc,
(( I_NONE | I_LEFT | I_RIGHT | I_NIL | I_MAP | I_ITER | I_EMPTY_SET
| I_LOOP | I_LOOP_LEFT | I_CONTRACT | I_CAST | I_UNPACK
| I_CREATE_CONTRACT | I_EMIT ) as name),
(([] | _ :: _ :: _) as l),
_ ),
_ ) ->
fail (Invalid_arity (loc, name, 1, List.length l))
| ( Prim
( loc,
(( I_PUSH | I_VIEW | I_IF_NONE | I_IF_LEFT | I_IF_CONS | I_EMPTY_MAP
| I_EMPTY_BIG_MAP | I_IF ) as name),
(([] | [_] | _ :: _ :: _ :: _) as l),
_ ),
_ ) ->
fail (Invalid_arity (loc, name, 2, List.length l))
| ( Prim (loc, I_LAMBDA, (([] | [_] | [_; _] | _ :: _ :: _ :: _ :: _) as l), _),
_ ) ->
fail (Invalid_arity (loc, I_LAMBDA, 3, List.length l))
(* Stack errors *)
| ( Prim
( loc,
(( I_ADD | I_SUB | I_SUB_MUTEZ | I_MUL | I_EDIV | I_AND | I_OR | I_XOR
| I_LSL | I_LSR | I_CONCAT | I_PAIRING_CHECK ) as name),
[],
_ ),
Item_t (ta, Item_t (tb, _)) ) ->
let ta = serialize_ty_for_error ta in
let tb = serialize_ty_for_error tb in
fail (Undefined_binop (loc, name, ta, tb))
| ( Prim
( loc,
(( I_NEG | I_ABS | I_NOT | I_SIZE | I_EQ | I_NEQ | I_LT | I_GT | I_LE
| I_GE
(* CONCAT is both unary and binary; this case can only be triggered
on a singleton stack *)
| I_CONCAT ) as name),
[],
_ ),
Item_t (t, _) ) ->
let t = serialize_ty_for_error t in
fail (Undefined_unop (loc, name, t))
| Prim (loc, ((I_UPDATE | I_SLICE | I_OPEN_CHEST) as name), [], _), stack ->
Lwt.return
(let stack = serialize_stack_for_error ctxt stack in
error (Bad_stack (loc, name, 3, stack)))
| Prim (loc, I_CREATE_CONTRACT, _, _), stack ->
let stack = serialize_stack_for_error ctxt stack in
fail (Bad_stack (loc, I_CREATE_CONTRACT, 7, stack))
| Prim (loc, I_TRANSFER_TOKENS, [], _), stack ->
Lwt.return
(let stack = serialize_stack_for_error ctxt stack in
error (Bad_stack (loc, I_TRANSFER_TOKENS, 4, stack)))
| ( Prim
( loc,
(( I_DROP | I_DUP | I_CAR | I_CDR | I_UNPAIR | I_SOME | I_BLAKE2B
| I_SHA256 | I_SHA512 | I_DIP | I_IF_NONE | I_LEFT | I_RIGHT
| I_IF_LEFT | I_IF | I_LOOP | I_IF_CONS | I_IMPLICIT_ACCOUNT | I_NEG
| I_ABS | I_INT | I_NOT | I_HASH_KEY | I_EQ | I_NEQ | I_LT | I_GT
| I_LE | I_GE | I_SIZE | I_FAILWITH | I_RENAME | I_PACK | I_ISNAT
| I_ADDRESS | I_SET_DELEGATE | I_CAST | I_MAP | I_ITER | I_LOOP_LEFT
| I_UNPACK | I_CONTRACT | I_NEVER | I_KECCAK | I_SHA3 | I_READ_TICKET
| I_JOIN_TICKETS ) as name),
_,
_ ),
stack ) ->
Lwt.return
(let stack = serialize_stack_for_error ctxt stack in
error (Bad_stack (loc, name, 1, stack)))
| ( Prim
( loc,
(( I_SWAP | I_PAIR | I_CONS | I_GET | I_MEM | I_EXEC
| I_CHECK_SIGNATURE | I_ADD | I_SUB | I_SUB_MUTEZ | I_MUL | I_EDIV
| I_AND | I_OR | I_XOR | I_LSL | I_LSR | I_COMPARE | I_PAIRING_CHECK
| I_TICKET | I_SPLIT_TICKET ) as name),
_,
_ ),
stack ) ->
Lwt.return
(let stack = serialize_stack_for_error ctxt stack in
error (Bad_stack (loc, name, 2, stack)))
(* Generic parsing errors *)
| expr, _ ->
fail
@@ unexpected
expr
[Seq_kind]
Instr_namespace
[
I_ABS;
I_ADD;
I_AMOUNT;
I_AND;
I_BALANCE;
I_BLAKE2B;
I_CAR;
I_CDR;
I_CHECK_SIGNATURE;
I_COMPARE;
I_CONCAT;
I_CONS;
I_CREATE_CONTRACT;
I_DIG;
I_DIP;
I_DROP;
I_DUG;
I_DUP;
I_EDIV;
I_EMPTY_BIG_MAP;
I_EMPTY_MAP;
I_EMPTY_SET;
I_EQ;
I_EXEC;
I_FAILWITH;
I_GE;
I_GET;
I_GET_AND_UPDATE;
I_GT;
I_HASH_KEY;
I_IF;
I_IF_CONS;
I_IF_LEFT;
I_IF_NONE;
I_IMPLICIT_ACCOUNT;
I_INT;
I_ITER;
I_JOIN_TICKETS;
I_KECCAK;
I_LAMBDA;
I_LE;
I_LEFT;
I_LEVEL;
I_LOOP;
I_LSL;
I_LSR;
I_LT;
I_MAP;
I_MEM;
I_MIN_BLOCK_TIME;
I_MUL;
I_NEG;
I_NEQ;
I_NEVER;
I_NIL;
I_NONE;
I_NOT;
I_NOW;
I_OPEN_CHEST;
I_OR;
I_PAIR;
I_PAIRING_CHECK;
I_PUSH;
I_READ_TICKET;
I_RIGHT;
I_SAPLING_EMPTY_STATE;
I_SAPLING_VERIFY_UPDATE;
I_SELF;
I_SELF_ADDRESS;
I_SENDER;
I_SHA256;
I_SHA3;
I_SHA512;
I_SIZE;
I_SOME;
I_SOURCE;
I_SPLIT_TICKET;
I_SUB;
I_SUB_MUTEZ;
I_SWAP;
I_TICKET;
I_TOTAL_VOTING_POWER;
I_TRANSFER_TOKENS;
I_UNIT;
I_UNPAIR;
I_UPDATE;
I_VIEW;
I_VOTING_POWER;
I_XOR;
]
and parse_contract_data :
type arg argc.
stack_depth:int ->
context ->
Script.location ->
(arg, argc) ty ->
Destination.t ->
entrypoint:Entrypoint.t ->
(context * arg typed_contract) tzresult Lwt.t =
fun ~stack_depth ctxt loc arg destination ~entrypoint ->
let error_details = Informative loc in
parse_contract
~stack_depth:(stack_depth + 1)
ctxt
~error_details
loc
arg
destination
~entrypoint
>>=? fun (ctxt, res) -> Lwt.return (res >|? fun res -> (ctxt, res))
(* [parse_contract] is used both to:
- parse contract data by [parse_data] ([parse_contract_data])
- to execute the [CONTRACT] instruction ([parse_contract_for_script]).
The return type resembles the [Gas_monad]:
- the outer [tzresult] is for gas exhaustion and internal errors
- the inner [result] is for other legitimate cases of failure.
The inner [result] is turned into an [option] by [parse_contract_for_script].
Both [tzresult] are merged by [parse_contract_data].
*)
and parse_contract :
type arg argc err.
stack_depth:int ->
context ->
error_details:(location, err) error_details ->
Script.location ->
(arg, argc) ty ->
Destination.t ->
entrypoint:Entrypoint.t ->
(context * (arg typed_contract, err) result) tzresult Lwt.t =
fun ~stack_depth ctxt ~error_details loc arg destination ~entrypoint ->
let error ctxt f_err : context * (_, err) result =
( ctxt,
Error
(match error_details with
| Fast -> (Inconsistent_types_fast : err)
| Informative loc -> trace_of_error @@ f_err loc) )
in
Gas.consume ctxt Typecheck_costs.parse_instr_cycle >>?= fun ctxt ->
match destination with
| Contract contract -> (
match contract with
| Implicit pkh ->
Lwt.return
(if Entrypoint.is_default entrypoint then
(* An implicit account on the "default" entrypoint always exists and has type unit. *)
Gas_monad.run ctxt @@ ty_eq ~error_details arg unit_t
>|? fun (eq, ctxt) ->
(ctxt, eq >|? fun Eq : arg typed_contract -> Typed_implicit pkh)
else
(* An implicit account on any other entrypoint is not a valid contract. *)
ok (error ctxt (fun _loc -> No_such_entrypoint entrypoint)))
| Originated contract_hash ->
trace
(Invalid_contract (loc, contract))
( Contract.get_script_code ctxt contract >>=? fun (ctxt, code) ->
Lwt.return
(match code with
| None ->
ok
(error ctxt (fun loc -> Invalid_contract (loc, contract)))
| Some code ->
Script.force_decode_in_context
~consume_deserialization_gas:When_needed
ctxt
code
>>? fun (code, ctxt) ->
(* can only fail because of gas *)
parse_toplevel ctxt ~legacy:true code
>>? fun ({arg_type; _}, ctxt) ->
parse_parameter_ty_and_entrypoints
ctxt
~stack_depth:(stack_depth + 1)
~legacy:true
arg_type
>>? fun ( Ex_parameter_ty_and_entrypoints
{arg_type = targ; entrypoints},
ctxt ) ->
Gas_monad.run ctxt
@@ find_entrypoint_for_type
~error_details
~full:targ
~expected:arg
entrypoints
entrypoint
>|? fun (entrypoint_arg, ctxt) ->
( ctxt,
entrypoint_arg >|? fun (entrypoint, arg_ty) ->
Typed_originated {arg_ty; contract_hash; entrypoint} )) ))
| Tx_rollup tx_rollup ->
Tx_rollup_state.assert_exist ctxt tx_rollup >|=? fun ctxt ->
if Entrypoint.(entrypoint = Tx_rollup.deposit_entrypoint) then
(* /!\ This pattern matching needs to remain in sync with
[parse_tx_rollup_deposit_parameters]. *)
match arg with
| Pair_t (Ticket_t (_, _), Tx_rollup_l2_address_t, _, _) ->
( ctxt,
ok
@@ (Typed_tx_rollup {arg_ty = arg; tx_rollup}
: arg typed_contract) )
| _ ->
error ctxt (fun loc ->
Tx_rollup_bad_deposit_parameter (loc, serialize_ty_for_error arg))
else error ctxt (fun _loc -> No_such_entrypoint entrypoint)
| Sc_rollup sc_rollup ->
Sc_rollup.parameters_type ctxt sc_rollup
>>=? fun (parameters_type, ctxt) ->
Lwt.return
(match parameters_type with
| None ->
ok
(error ctxt (fun _loc ->
Sc_rollup.Errors.Sc_rollup_does_not_exist sc_rollup))
| Some parameters_type ->
Script.force_decode_in_context
~consume_deserialization_gas:When_needed
ctxt
parameters_type
>>? fun (parameters_type, ctxt) ->
parse_parameter_ty_and_entrypoints
ctxt
~stack_depth:(stack_depth + 1)
~legacy:true
(root parameters_type)
>>? fun ( Ex_parameter_ty_and_entrypoints
{arg_type = full; entrypoints},
ctxt ) ->
Gas_monad.run ctxt
@@ find_entrypoint_for_type
~error_details
~full
~expected:arg
entrypoints
entrypoint
>|? fun (entrypoint_arg, ctxt) ->
( ctxt,
entrypoint_arg >|? fun (entrypoint, arg_ty) ->
Typed_sc_rollup {arg_ty; sc_rollup; entrypoint} ))
(* Same as [parse_contract], but does not fail when the contact is missing or
if the expected type doesn't match the actual one. In that case None is
returned and some overapproximation of the typechecking gas is consumed.
This can still fail on gas exhaustion. *)
let parse_contract_for_script :
type arg argc.
context ->
Script.location ->
(arg, argc) ty ->
Destination.t ->
entrypoint:Entrypoint.t ->
(context * arg typed_contract option) tzresult Lwt.t =
fun ctxt loc arg destination ~entrypoint ->
parse_contract
~stack_depth:0
ctxt
~error_details:Fast
loc
arg
destination
~entrypoint
>|=? fun (ctxt, res) ->
( ctxt,
match res with Ok res -> Some res | Error Inconsistent_types_fast -> None )
let view_size view =
let open Script_typed_ir_size in
node_size view.view_code ++ node_size view.input_ty
++ node_size view.output_ty
let code_size ctxt code views =
let open Script_typed_ir_size in
let views_size = Script_map.fold (fun _ v s -> view_size v ++ s) views zero in
(* The size of the storage_type and the arg_type is counted by
[lambda_size]. *)
let ir_size = lambda_size code in
let nodes, code_size = views_size ++ ir_size in
(* We consume gas after the fact in order to not have to instrument
[node_size] (for efficiency).
This is safe, as we already pay gas proportional to [views_size] and
[ir_size] during their typechecking. *)
Gas.consume ctxt (Script_typed_ir_size_costs.nodes_cost ~nodes)
>|? fun ctxt -> (code_size, ctxt)
let parse_code :
elab_conf:elab_conf ->
context ->
code:lazy_expr ->
(ex_code * context) tzresult Lwt.t =
fun ~elab_conf ctxt ~code ->
Script.force_decode_in_context
~consume_deserialization_gas:When_needed
ctxt
code
>>?= fun (code, ctxt) ->
let legacy = elab_conf.legacy in
Global_constants_storage.expand ctxt code >>=? fun (ctxt, code) ->
parse_toplevel ctxt ~legacy code
>>?= fun ({arg_type; storage_type; code_field; views}, ctxt) ->
let arg_type_loc = location arg_type in
record_trace
(Ill_formed_type (Some "parameter", code, arg_type_loc))
(parse_parameter_ty_and_entrypoints ctxt ~stack_depth:0 ~legacy arg_type)
>>?= fun (Ex_parameter_ty_and_entrypoints {arg_type; entrypoints}, ctxt) ->
let storage_type_loc = location storage_type in
record_trace
(Ill_formed_type (Some "storage", code, storage_type_loc))
(parse_storage_ty ctxt ~stack_depth:0 ~legacy storage_type)
>>?= fun (Ex_ty storage_type, ctxt) ->
pair_t storage_type_loc arg_type storage_type
>>?= fun (Ty_ex_c arg_type_full) ->
pair_t storage_type_loc list_operation_t storage_type
>>?= fun (Ty_ex_c ret_type_full) ->
trace
(Ill_typed_contract (code, []))
(parse_kdescr
Tc_context.(toplevel ~storage_type ~param_type:arg_type ~entrypoints)
~elab_conf
ctxt
~stack_depth:0
arg_type_full
ret_type_full
code_field)
>>=? fun (kdescr, ctxt) ->
let code = Lam (kdescr, code_field) in
Lwt.return
( code_size ctxt code views >>? fun (code_size, ctxt) ->
ok
( Ex_code
(Code {code; arg_type; storage_type; views; entrypoints; code_size}),
ctxt ) )
let parse_storage :
elab_conf:elab_conf ->
context ->
allow_forged:bool ->
('storage, _) ty ->
storage:lazy_expr ->
('storage * context) tzresult Lwt.t =
fun ~elab_conf ctxt ~allow_forged storage_type ~storage ->
Script.force_decode_in_context
~consume_deserialization_gas:When_needed
ctxt
storage
>>?= fun (storage, ctxt) ->
trace_eval
(fun () ->
let storage_type = serialize_ty_for_error storage_type in
Ill_typed_data (None, storage, storage_type))
(parse_data
~elab_conf
~stack_depth:0
ctxt
~allow_forged
storage_type
(root storage))
let parse_script :
elab_conf:elab_conf ->
context ->
allow_forged_in_storage:bool ->
Script.t ->
(ex_script * context) tzresult Lwt.t =
fun ~elab_conf ctxt ~allow_forged_in_storage {code; storage} ->
parse_code ~elab_conf ctxt ~code
>>=? fun ( Ex_code
(Code
{code; arg_type; storage_type; views; entrypoints; code_size}),
ctxt ) ->
parse_storage
~elab_conf
ctxt
~allow_forged:allow_forged_in_storage
storage_type
~storage
>|=? fun (storage, ctxt) ->
( Ex_script
(Script
{code_size; code; arg_type; storage; storage_type; views; entrypoints}),
ctxt )
type typechecked_code_internal =
| Typechecked_code_internal : {
toplevel : toplevel;
arg_type : ('arg, _) ty;
storage_type : ('storage, _) ty;
entrypoints : 'arg entrypoints;
typed_views : 'storage typed_view_map;
type_map : type_map;
}
-> typechecked_code_internal
let typecheck_code :
legacy:bool ->
show_types:bool ->
context ->
Script.expr ->
(typechecked_code_internal * context) tzresult Lwt.t =
fun ~legacy ~show_types ctxt code ->
(* Constants need to be expanded or [parse_toplevel] may fail. *)
Global_constants_storage.expand ctxt code >>=? fun (ctxt, code) ->
parse_toplevel ctxt ~legacy code >>?= fun (toplevel, ctxt) ->
let {arg_type; storage_type; code_field; views} = toplevel in
let type_map = ref [] in
let arg_type_loc = location arg_type in
record_trace
(Ill_formed_type (Some "parameter", code, arg_type_loc))
(parse_parameter_ty_and_entrypoints ctxt ~stack_depth:0 ~legacy arg_type)
>>?= fun (Ex_parameter_ty_and_entrypoints {arg_type; entrypoints}, ctxt) ->
let storage_type_loc = location storage_type in
record_trace
(Ill_formed_type (Some "storage", code, storage_type_loc))
(parse_storage_ty ctxt ~stack_depth:0 ~legacy storage_type)
>>?= fun (ex_storage_type, ctxt) ->
let (Ex_ty storage_type) = ex_storage_type in
pair_t storage_type_loc arg_type storage_type
>>?= fun (Ty_ex_c arg_type_full) ->
pair_t storage_type_loc list_operation_t storage_type
>>?= fun (Ty_ex_c ret_type_full) ->
let type_logger loc ~stack_ty_before ~stack_ty_after =
type_map := (loc, (stack_ty_before, stack_ty_after)) :: !type_map
in
let type_logger = if show_types then Some type_logger else None in
let elab_conf = Script_ir_translator_config.make ~legacy ?type_logger () in
let result =
parse_kdescr
(Tc_context.toplevel ~storage_type ~param_type:arg_type ~entrypoints)
ctxt
~elab_conf
~stack_depth:0
arg_type_full
ret_type_full
code_field
in
trace (Ill_typed_contract (code, !type_map)) result
>>=? fun ((_ : (_, _, _, _) kdescr), ctxt) ->
let views_result = parse_views ctxt ~elab_conf storage_type views in
trace (Ill_typed_contract (code, !type_map)) views_result
>|=? fun (typed_views, ctxt) ->
( Typechecked_code_internal
{
toplevel;
arg_type;
storage_type;
entrypoints;
typed_views;
type_map = !type_map;
},
ctxt )
(* Uncarbonated because used only in RPCs *)
let list_entrypoints_uncarbonated (type full fullc) (full : (full, fullc) ty)
(entrypoints : full entrypoints) =
let merge path (type t tc) (ty : (t, tc) ty)
(entrypoints : t entrypoints_node) reachable ((unreachables, all) as acc)
=
match entrypoints.at_node with
| None ->
( (if reachable then acc
else
match ty with
| Union_t _ -> acc
| _ -> (List.rev path :: unreachables, all)),
reachable )
| Some {name; original_type_expr} ->
( (if Entrypoint.Map.mem name all then
(List.rev path :: unreachables, all)
else
( unreachables,
Entrypoint.Map.add name (Ex_ty ty, original_type_expr) all )),
true )
in
let rec fold_tree :
type t tc.
(t, tc) ty ->
t entrypoints_node ->
prim list ->
bool ->
prim list list * (ex_ty * Script.node) Entrypoint.Map.t ->
prim list list * (ex_ty * Script.node) Entrypoint.Map.t =
fun t entrypoints path reachable acc ->
match (t, entrypoints) with
| Union_t (tl, tr, _, _), {nested = Entrypoints_Union {left; right}; _} ->
let acc, l_reachable = merge (D_Left :: path) tl left reachable acc in
let acc, r_reachable = merge (D_Right :: path) tr right reachable acc in
let acc = fold_tree tl left (D_Left :: path) l_reachable acc in
fold_tree tr right (D_Right :: path) r_reachable acc
| _ -> acc
in
let init, reachable =
match entrypoints.root.at_node with
| None -> (Entrypoint.Map.empty, false)
| Some {name; original_type_expr} ->
(Entrypoint.Map.singleton name (Ex_ty full, original_type_expr), true)
in
fold_tree full entrypoints.root [] reachable ([], init)
include Data_unparser (struct
let opened_ticket_type = opened_ticket_type
let parse_packable_ty = parse_packable_ty
let parse_data = parse_data
end)
let parse_and_unparse_script_unaccounted ctxt ~legacy ~allow_forged_in_storage
mode ~normalize_types {code; storage} =
Script.force_decode_in_context
~consume_deserialization_gas:When_needed
ctxt
code
>>?= fun (code, ctxt) ->
typecheck_code ~legacy ~show_types:false ctxt code
>>=? fun ( Typechecked_code_internal
{
toplevel =
{
code_field;
arg_type = original_arg_type_expr;
storage_type = original_storage_type_expr;
views;
};
arg_type;
storage_type;
entrypoints;
typed_views;
type_map = _;
},
ctxt ) ->
parse_storage
~elab_conf:(Script_ir_translator_config.make ~legacy ())
ctxt
~allow_forged:allow_forged_in_storage
storage_type
~storage
>>=? fun (storage, ctxt) ->
unparse_code ctxt ~stack_depth:0 mode code_field >>=? fun (code, ctxt) ->
unparse_data ctxt ~stack_depth:0 mode storage_type storage
>>=? fun (storage, ctxt) ->
let loc = Micheline.dummy_location in
(if normalize_types then
unparse_parameter_ty ~loc ctxt arg_type ~entrypoints
>>?= fun (arg_type, ctxt) ->
unparse_ty ~loc ctxt storage_type >>?= fun (storage_type, ctxt) ->
Script_map.map_es_in_context
(fun ctxt
_name
(Typed_view {input_ty; output_ty; kinstr = _; original_code_expr}) ->
Lwt.return
( unparse_ty ~loc ctxt input_ty >>? fun (input_ty, ctxt) ->
unparse_ty ~loc ctxt output_ty >|? fun (output_ty, ctxt) ->
({input_ty; output_ty; view_code = original_code_expr}, ctxt) ))
ctxt
typed_views
>|=? fun (views, ctxt) -> (arg_type, storage_type, views, ctxt)
else return (original_arg_type_expr, original_storage_type_expr, views, ctxt))
>>=? fun (arg_type, storage_type, views, ctxt) ->
Script_map.map_es_in_context
(fun ctxt _name {input_ty; output_ty; view_code} ->
unparse_code ctxt ~stack_depth:0 mode view_code
>|=? fun (view_code, ctxt) -> ({input_ty; output_ty; view_code}, ctxt))
ctxt
views
>>=? fun (views, ctxt) ->
let open Micheline in
let unparse_view_unaccounted name {input_ty; output_ty; view_code} views =
Prim
( loc,
K_view,
[
String (loc, Script_string.to_string name);
input_ty;
output_ty;
view_code;
],
[] )
:: views
in
let views = Script_map.fold unparse_view_unaccounted views [] |> List.rev in
let code =
Seq
( loc,
[
Prim (loc, K_parameter, [arg_type], []);
Prim (loc, K_storage, [storage_type], []);
Prim (loc, K_code, [code], []);
]
@ views )
in
return
( {
code = lazy_expr (strip_locations code);
storage = lazy_expr (strip_locations storage);
},
ctxt )
let pack_data_with_mode ctxt ty data ~mode =
unparse_data ~stack_depth:0 ctxt mode ty data >>=? fun (unparsed, ctxt) ->
Lwt.return @@ pack_node unparsed ctxt
let hash_data ctxt ty data =
pack_data_with_mode ctxt ty data ~mode:Optimized_legacy
>>=? fun (bytes, ctxt) -> Lwt.return @@ hash_bytes ctxt bytes
let pack_data ctxt ty data =
pack_data_with_mode ctxt ty data ~mode:Optimized_legacy
(* ---------------- Lazy storage---------------------------------------------*)
type lazy_storage_ids = Lazy_storage.IdSet.t
let no_lazy_storage_id = Lazy_storage.IdSet.empty
let diff_of_big_map ctxt mode ~temporary ~ids_to_copy
(Big_map {id; key_type; value_type; diff}) =
(match id with
| Some id ->
if Lazy_storage.IdSet.mem Big_map id ids_to_copy then
Big_map.fresh ~temporary ctxt >|=? fun (ctxt, duplicate) ->
(ctxt, Lazy_storage.Copy {src = id}, duplicate)
else
(* The first occurrence encountered of a big_map reuses the
ID. This way, the payer is only charged for the diff.
For this to work, this diff has to be put at the end of
the global diff, otherwise the duplicates will use the
updated version as a base. This is true because we add
this diff first in the accumulator of
`extract_lazy_storage_updates`, and this accumulator is not
reversed. *)
return (ctxt, Lazy_storage.Existing, id)
| None ->
Big_map.fresh ~temporary ctxt >>=? fun (ctxt, id) ->
Lwt.return
(let kt = unparse_comparable_ty_uncarbonated ~loc:() key_type in
Gas.consume ctxt (Script.strip_locations_cost kt) >>? fun ctxt ->
unparse_ty ~loc:() ctxt value_type >>? fun (kv, ctxt) ->
Gas.consume ctxt (Script.strip_locations_cost kv) >|? fun ctxt ->
let key_type = Micheline.strip_locations kt in
let value_type = Micheline.strip_locations kv in
(ctxt, Lazy_storage.(Alloc Big_map.{key_type; value_type}), id)))
>>=? fun (ctxt, init, id) ->
let pairs =
Big_map_overlay.fold
(fun key_hash (key, value) acc -> (key_hash, key, value) :: acc)
diff.map
[]
in
List.fold_left_es
(fun (acc, ctxt) (key_hash, key, value) ->
Gas.consume ctxt Typecheck_costs.parse_instr_cycle >>?= fun ctxt ->
unparse_comparable_data ~loc:() ctxt mode key_type key
>>=? fun (key_node, ctxt) ->
Gas.consume ctxt (Script.strip_locations_cost key_node) >>?= fun ctxt ->
let key = Micheline.strip_locations key_node in
(match value with
| None -> return (None, ctxt)
| Some x ->
unparse_data ~stack_depth:0 ctxt mode value_type x
>>=? fun (node, ctxt) ->
Lwt.return
( Gas.consume ctxt (Script.strip_locations_cost node) >|? fun ctxt ->
(Some (Micheline.strip_locations node), ctxt) ))
>|=? fun (value, ctxt) ->
let diff_item = Big_map.{key; key_hash; value} in
(diff_item :: acc, ctxt))
([], ctxt)
(List.rev pairs)
>|=? fun (updates, ctxt) -> (Lazy_storage.Update {init; updates}, id, ctxt)
let diff_of_sapling_state ctxt ~temporary ~ids_to_copy
({id; diff; memo_size} : Sapling.state) =
(match id with
| Some id ->
if Lazy_storage.IdSet.mem Sapling_state id ids_to_copy then
Sapling.fresh ~temporary ctxt >|=? fun (ctxt, duplicate) ->
(ctxt, Lazy_storage.Copy {src = id}, duplicate)
else return (ctxt, Lazy_storage.Existing, id)
| None ->
Sapling.fresh ~temporary ctxt >|=? fun (ctxt, id) ->
(ctxt, Lazy_storage.Alloc Sapling.{memo_size}, id))
>|=? fun (ctxt, init, id) ->
(Lazy_storage.Update {init; updates = diff}, id, ctxt)
(**
Witness flag for whether a type can be populated by a value containing a
lazy storage.
[False_f] must be used only when a value of the type cannot contain a lazy
storage.
This flag is built in [has_lazy_storage] and used only in
[extract_lazy_storage_updates] and [collect_lazy_storage].
This flag is necessary to avoid these two functions to have a quadratic
complexity in the size of the type.
Add new lazy storage kinds here.
Please keep the usage of this GADT local.
*)
type 'ty has_lazy_storage =
| Big_map_f : ('a, 'b) big_map has_lazy_storage
| Sapling_state_f : Sapling.state has_lazy_storage
| False_f : _ has_lazy_storage
| Pair_f :
'a has_lazy_storage * 'b has_lazy_storage
-> ('a, 'b) pair has_lazy_storage
| Union_f :
'a has_lazy_storage * 'b has_lazy_storage
-> ('a, 'b) union has_lazy_storage
| Option_f : 'a has_lazy_storage -> 'a option has_lazy_storage
| List_f : 'a has_lazy_storage -> 'a boxed_list has_lazy_storage
| Map_f : 'v has_lazy_storage -> (_, 'v) map has_lazy_storage
(**
This function is called only on storage and parameter types of contracts,
once per typechecked contract. It has a complexity linear in the size of
the types, which happen to be literally written types, so the gas for them
has already been paid.
*)
let rec has_lazy_storage : type t tc. (t, tc) ty -> t has_lazy_storage =
fun ty ->
let aux1 cons t =
match has_lazy_storage t with False_f -> False_f | h -> cons h
in
let aux2 cons t1 t2 =
match (has_lazy_storage t1, has_lazy_storage t2) with
| False_f, False_f -> False_f
| h1, h2 -> cons h1 h2
in
match ty with
| Big_map_t (_, _, _) -> Big_map_f
| Sapling_state_t _ -> Sapling_state_f
| Unit_t -> False_f
| Int_t -> False_f
| Nat_t -> False_f
| Signature_t -> False_f
| String_t -> False_f
| Bytes_t -> False_f
| Mutez_t -> False_f
| Key_hash_t -> False_f
| Key_t -> False_f
| Timestamp_t -> False_f
| Address_t -> False_f
| Tx_rollup_l2_address_t -> False_f
| Bool_t -> False_f
| Lambda_t (_, _, _) -> False_f
| Set_t (_, _) -> False_f
| Contract_t (_, _) -> False_f
| Operation_t -> False_f
| Chain_id_t -> False_f
| Never_t -> False_f
| Bls12_381_g1_t -> False_f
| Bls12_381_g2_t -> False_f
| Bls12_381_fr_t -> False_f
| Sapling_transaction_t _ -> False_f
| Sapling_transaction_deprecated_t _ -> False_f
| Ticket_t _ -> False_f
| Chest_key_t -> False_f
| Chest_t -> False_f
| Pair_t (l, r, _, _) -> aux2 (fun l r -> Pair_f (l, r)) l r
| Union_t (l, r, _, _) -> aux2 (fun l r -> Union_f (l, r)) l r
| Option_t (t, _, _) -> aux1 (fun h -> Option_f h) t
| List_t (t, _) -> aux1 (fun h -> List_f h) t
| Map_t (_, t, _) -> aux1 (fun h -> Map_f h) t
(**
Transforms a value potentially containing lazy storage in an intermediary
state to a value containing lazy storage only represented by identifiers.
Returns the updated value, the updated set of ids to copy, and the lazy
storage diff to show on the receipt and apply on the storage.
*)
let extract_lazy_storage_updates ctxt mode ~temporary ids_to_copy acc ty x =
let rec aux :
type a ac.
context ->
unparsing_mode ->
temporary:bool ->
Lazy_storage.IdSet.t ->
Lazy_storage.diffs ->
(a, ac) ty ->
a ->
has_lazy_storage:a has_lazy_storage ->
(context * a * Lazy_storage.IdSet.t * Lazy_storage.diffs) tzresult Lwt.t =
fun ctxt mode ~temporary ids_to_copy acc ty x ~has_lazy_storage ->
Gas.consume ctxt Typecheck_costs.parse_instr_cycle >>?= fun ctxt ->
match (has_lazy_storage, ty, x) with
| False_f, _, _ -> return (ctxt, x, ids_to_copy, acc)
| Big_map_f, Big_map_t (_, _, _), map ->
diff_of_big_map ctxt mode ~temporary ~ids_to_copy map
>|=? fun (diff, id, ctxt) ->
let map =
let (Big_map map) = map in
Big_map
{
map with
diff = {map = Big_map_overlay.empty; size = 0};
id = Some id;
}
in
let diff = Lazy_storage.make Big_map id diff in
let ids_to_copy = Lazy_storage.IdSet.add Big_map id ids_to_copy in
(ctxt, map, ids_to_copy, diff :: acc)
| Sapling_state_f, Sapling_state_t _, sapling_state ->
diff_of_sapling_state ctxt ~temporary ~ids_to_copy sapling_state
>|=? fun (diff, id, ctxt) ->
let sapling_state =
Sapling.empty_state ~id ~memo_size:sapling_state.memo_size ()
in
let diff = Lazy_storage.make Sapling_state id diff in
let ids_to_copy = Lazy_storage.IdSet.add Sapling_state id ids_to_copy in
(ctxt, sapling_state, ids_to_copy, diff :: acc)
| Pair_f (hl, hr), Pair_t (tyl, tyr, _, _), (xl, xr) ->
aux ctxt mode ~temporary ids_to_copy acc tyl xl ~has_lazy_storage:hl
>>=? fun (ctxt, xl, ids_to_copy, acc) ->
aux ctxt mode ~temporary ids_to_copy acc tyr xr ~has_lazy_storage:hr
>|=? fun (ctxt, xr, ids_to_copy, acc) ->
(ctxt, (xl, xr), ids_to_copy, acc)
| Union_f (has_lazy_storage, _), Union_t (ty, _, _, _), L x ->
aux ctxt mode ~temporary ids_to_copy acc ty x ~has_lazy_storage
>|=? fun (ctxt, x, ids_to_copy, acc) -> (ctxt, L x, ids_to_copy, acc)
| Union_f (_, has_lazy_storage), Union_t (_, ty, _, _), R x ->
aux ctxt mode ~temporary ids_to_copy acc ty x ~has_lazy_storage
>|=? fun (ctxt, x, ids_to_copy, acc) -> (ctxt, R x, ids_to_copy, acc)
| Option_f has_lazy_storage, Option_t (ty, _, _), Some x ->
aux ctxt mode ~temporary ids_to_copy acc ty x ~has_lazy_storage
>|=? fun (ctxt, x, ids_to_copy, acc) -> (ctxt, Some x, ids_to_copy, acc)
| List_f has_lazy_storage, List_t (ty, _), l ->
List.fold_left_es
(fun (ctxt, l, ids_to_copy, acc) x ->
aux ctxt mode ~temporary ids_to_copy acc ty x ~has_lazy_storage
>|=? fun (ctxt, x, ids_to_copy, acc) ->
(ctxt, Script_list.cons x l, ids_to_copy, acc))
(ctxt, Script_list.empty, ids_to_copy, acc)
l.elements
>|=? fun (ctxt, l, ids_to_copy, acc) ->
let reversed = {length = l.length; elements = List.rev l.elements} in
(ctxt, reversed, ids_to_copy, acc)
| Map_f has_lazy_storage, Map_t (_, ty, _), map ->
let (module M) = Script_map.get_module map in
let bindings m = M.OPS.fold (fun k v bs -> (k, v) :: bs) m [] in
List.fold_left_es
(fun (ctxt, m, ids_to_copy, acc) (k, x) ->
aux ctxt mode ~temporary ids_to_copy acc ty x ~has_lazy_storage
>|=? fun (ctxt, x, ids_to_copy, acc) ->
(ctxt, M.OPS.add k x m, ids_to_copy, acc))
(ctxt, M.OPS.empty, ids_to_copy, acc)
(bindings M.boxed)
>|=? fun (ctxt, m, ids_to_copy, acc) ->
let module M = struct
module OPS = M.OPS
type key = M.key
type value = M.value
let boxed = m
let size = M.size
end in
( ctxt,
Script_map.make
(module M : Boxed_map
with type key = M.key
and type value = M.value),
ids_to_copy,
acc )
| _, Option_t (_, _, _), None -> return (ctxt, None, ids_to_copy, acc)
in
let has_lazy_storage = has_lazy_storage ty in
aux ctxt mode ~temporary ids_to_copy acc ty x ~has_lazy_storage
(** We namespace an error type for [fold_lazy_storage]. The error case is only
available when the ['error] parameter is equal to unit. *)
module Fold_lazy_storage = struct
type ('acc, 'error) result =
| Ok : 'acc -> ('acc, 'error) result
| Error : ('acc, unit) result
end
(** Prematurely abort if [f] generates an error. Use this function without the
[unit] type for [error] if you are in a case where errors are impossible.
*)
let rec fold_lazy_storage :
type a ac error.
f:('acc, error) Fold_lazy_storage.result Lazy_storage.IdSet.fold_f ->
init:'acc ->
context ->
(a, ac) ty ->
a ->
has_lazy_storage:a has_lazy_storage ->
(('acc, error) Fold_lazy_storage.result * context) tzresult =
fun ~f ~init ctxt ty x ~has_lazy_storage ->
Gas.consume ctxt Typecheck_costs.parse_instr_cycle >>? fun ctxt ->
match (has_lazy_storage, ty, x) with
| Big_map_f, Big_map_t (_, _, _), Big_map {id = Some id; _} ->
Gas.consume ctxt Typecheck_costs.parse_instr_cycle >>? fun ctxt ->
ok (f.f Big_map id (Fold_lazy_storage.Ok init), ctxt)
| Sapling_state_f, Sapling_state_t _, {id = Some id; _} ->
Gas.consume ctxt Typecheck_costs.parse_instr_cycle >>? fun ctxt ->
ok (f.f Sapling_state id (Fold_lazy_storage.Ok init), ctxt)
| False_f, _, _ -> ok (Fold_lazy_storage.Ok init, ctxt)
| Big_map_f, Big_map_t (_, _, _), Big_map {id = None; _} ->
ok (Fold_lazy_storage.Ok init, ctxt)
| Sapling_state_f, Sapling_state_t _, {id = None; _} ->
ok (Fold_lazy_storage.Ok init, ctxt)
| Pair_f (hl, hr), Pair_t (tyl, tyr, _, _), (xl, xr) -> (
fold_lazy_storage ~f ~init ctxt tyl xl ~has_lazy_storage:hl
>>? fun (init, ctxt) ->
match init with
| Fold_lazy_storage.Ok init ->
fold_lazy_storage ~f ~init ctxt tyr xr ~has_lazy_storage:hr
| Fold_lazy_storage.Error -> ok (init, ctxt))
| Union_f (has_lazy_storage, _), Union_t (ty, _, _, _), L x ->
fold_lazy_storage ~f ~init ctxt ty x ~has_lazy_storage
| Union_f (_, has_lazy_storage), Union_t (_, ty, _, _), R x ->
fold_lazy_storage ~f ~init ctxt ty x ~has_lazy_storage
| _, Option_t (_, _, _), None -> ok (Fold_lazy_storage.Ok init, ctxt)
| Option_f has_lazy_storage, Option_t (ty, _, _), Some x ->
fold_lazy_storage ~f ~init ctxt ty x ~has_lazy_storage
| List_f has_lazy_storage, List_t (ty, _), l ->
List.fold_left_e
(fun ((init, ctxt) : ('acc, error) Fold_lazy_storage.result * context) x ->
match init with
| Fold_lazy_storage.Ok init ->
fold_lazy_storage ~f ~init ctxt ty x ~has_lazy_storage
| Fold_lazy_storage.Error -> ok (init, ctxt))
(Fold_lazy_storage.Ok init, ctxt)
l.elements
| Map_f has_lazy_storage, Map_t (_, ty, _), m ->
Script_map.fold
(fun _
v
(acc : (('acc, error) Fold_lazy_storage.result * context) tzresult) ->
acc >>? fun (init, ctxt) ->
match init with
| Fold_lazy_storage.Ok init ->
fold_lazy_storage ~f ~init ctxt ty v ~has_lazy_storage
| Fold_lazy_storage.Error -> ok (init, ctxt))
m
(ok (Fold_lazy_storage.Ok init, ctxt))
let collect_lazy_storage ctxt ty x =
let has_lazy_storage = has_lazy_storage ty in
let f kind id (acc : (_, never) Fold_lazy_storage.result) =
let acc = match acc with Fold_lazy_storage.Ok acc -> acc in
Fold_lazy_storage.Ok (Lazy_storage.IdSet.add kind id acc)
in
fold_lazy_storage ~f:{f} ~init:no_lazy_storage_id ctxt ty x ~has_lazy_storage
>>? fun (ids, ctxt) ->
match ids with Fold_lazy_storage.Ok ids -> ok (ids, ctxt)
let extract_lazy_storage_diff ctxt mode ~temporary ~to_duplicate ~to_update ty v
=
(*
Basically [to_duplicate] are ids from the argument and [to_update] are ids
from the storage before execution (i.e. it is safe to reuse them since they
will be owned by the same contract).
*)
let to_duplicate = Lazy_storage.IdSet.diff to_duplicate to_update in
extract_lazy_storage_updates ctxt mode ~temporary to_duplicate [] ty v
>|=? fun (ctxt, v, alive, diffs) ->
let diffs =
if temporary then diffs
else
let dead = Lazy_storage.IdSet.diff to_update alive in
Lazy_storage.IdSet.fold_all
{f = (fun kind id acc -> Lazy_storage.make kind id Remove :: acc)}
dead
diffs
in
match diffs with
| [] -> (v, None, ctxt)
| diffs -> (v, Some diffs (* do not reverse *), ctxt)
let list_of_big_map_ids ids =
Lazy_storage.IdSet.fold Big_map (fun id acc -> id :: acc) ids []
let parse_data = parse_data ~stack_depth:0
let parse_comparable_data ?type_logger =
parse_data
~elab_conf:Script_ir_translator_config.(make ~legacy:false ?type_logger ())
~allow_forged:false
let parse_instr :
type a s.
elab_conf:elab_conf ->
tc_context ->
context ->
Script.node ->
(a, s) stack_ty ->
((a, s) judgement * context) tzresult Lwt.t =
fun ~elab_conf tc_context ctxt script_instr stack_ty ->
parse_instr ~elab_conf ~stack_depth:0 tc_context ctxt script_instr stack_ty
let unparse_data = unparse_data ~stack_depth:0
let unparse_code ctxt mode code =
(* Constants need to be expanded or [unparse_code] may fail. *)
Global_constants_storage.expand ctxt (strip_locations code)
>>=? fun (ctxt, code) -> unparse_code ~stack_depth:0 ctxt mode (root code)
let parse_contract_data context loc arg_ty contract ~entrypoint =
parse_contract_data ~stack_depth:0 context loc arg_ty contract ~entrypoint
let parse_toplevel ctxt ~legacy toplevel =
Global_constants_storage.expand ctxt toplevel >>=? fun (ctxt, toplevel) ->
Lwt.return @@ parse_toplevel ctxt ~legacy toplevel
let parse_comparable_ty = parse_comparable_ty ~stack_depth:0
let parse_big_map_value_ty = parse_big_map_value_ty ~stack_depth:0
let parse_packable_ty = parse_packable_ty ~stack_depth:0
let parse_passable_ty = parse_passable_ty ~stack_depth:0
let parse_any_ty = parse_any_ty ~stack_depth:0
let parse_ty = parse_ty ~stack_depth:0 ~ret:Don't_parse_entrypoints
let parse_parameter_ty_and_entrypoints =
parse_parameter_ty_and_entrypoints ~stack_depth:0
let get_single_sapling_state ctxt ty x =
let has_lazy_storage = has_lazy_storage ty in
let f (type i a u) (kind : (i, a, u) Lazy_storage.Kind.t) (id : i)
single_id_opt : (Sapling.Id.t option, unit) Fold_lazy_storage.result =
match kind with
| Lazy_storage.Kind.Sapling_state -> (
match single_id_opt with
| Fold_lazy_storage.Ok None -> Fold_lazy_storage.Ok (Some id)
| Fold_lazy_storage.Ok (Some _) ->
Fold_lazy_storage.Error (* more than one *)
| Fold_lazy_storage.Error -> single_id_opt)
| _ -> single_id_opt
in
fold_lazy_storage ~f:{f} ~init:None ctxt ty x ~has_lazy_storage
>>? fun (id, ctxt) ->
match id with
| Fold_lazy_storage.Ok (Some id) -> ok (Some id, ctxt)
| Fold_lazy_storage.Ok None | Fold_lazy_storage.Error -> ok (None, ctxt)
(*
{!Script_cache} needs a measure of the script size in memory.
Determining this size is not easy in OCaml because of sharing.
Indeed, many values present in the script share the same memory
area. This is especially true for types and stack types: they are
heavily shared in every typed IR internal representation. As a
consequence, computing the size of the typed IR without taking
sharing into account leads to a size which is sometimes two order
of magnitude bigger than the actual size.
We could track down this sharing. Unfortunately, sharing is not
part of OCaml semantics: for this reason, a compiler can optimize
memory representation by adding more sharing. If two nodes use
different optimization flags or compilers, such a precise
computation of the memory footprint of scripts would lead to two
distinct sizes. As these sizes occur in the blockchain context,
this situation would lead to a fork.
For this reason, we introduce a *size model* for the script size.
This model provides an overapproximation of the actual size in
memory. The risk is to be too far from the actual size: the cache
would then be wrongly marked as full. This situation would make the
cache less useful but should present no security risk .
*)
let script_size
(Ex_script
(Script
{
code_size;
code = _;
arg_type = _;
storage;
storage_type;
entrypoints = _;
views = _;
})) =
let nodes, storage_size =
Script_typed_ir_size.value_size storage_type storage
in
let cost = Script_typed_ir_size_costs.nodes_cost ~nodes in
(Saturation_repr.(add code_size storage_size |> to_int), cost)
let typecheck_code ~legacy ~show_types ctxt code =
typecheck_code ~legacy ~show_types ctxt code
>|=? fun (Typechecked_code_internal {type_map; _}, ctxt) -> (type_map, ctxt)
