From b1515dc376d852c5cd964538772cc8fc113d46fd Mon Sep 17 00:00:00 2001 From: Alain Mebsout Date: Thu, 28 Jun 2018 16:58:29 +0200 Subject: [PATCH] Alpha: consume typechecking gas in type equality for expansion --- src/bin_client/test/test_contracts.sh | 2 +- .../lib_protocol/src/script_ir_translator.ml | 431 +++++++++--------- .../lib_protocol/src/script_ir_translator.mli | 2 +- 3 files changed, 223 insertions(+), 212 deletions(-) diff --git a/src/bin_client/test/test_contracts.sh b/src/bin_client/test/test_contracts.sh index e2c8c69c7..bb575787b 100755 --- a/src/bin_client/test/test_contracts.sh +++ b/src/bin_client/test/test_contracts.sh @@ -210,7 +210,7 @@ assert_storage $contract_dir/exec_concat.tz '"?"' '""' '"_abc"' assert_storage $contract_dir/exec_concat.tz '"?"' '"test"' '"test_abc"' # Get current steps to quota -assert_storage $contract_dir/steps_to_quota.tz 111 Unit 399849 +assert_storage $contract_dir/steps_to_quota.tz 111 Unit 399817 # Get the current balance of the contract assert_storage $contract_dir/balance.tz '111' Unit '4000000000000' diff --git a/src/proto_alpha/lib_protocol/src/script_ir_translator.ml b/src/proto_alpha/lib_protocol/src/script_ir_translator.ml index a3e3f51f9..caa98f144 100644 --- a/src/proto_alpha/lib_protocol/src/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/src/script_ir_translator.ml @@ -709,63 +709,68 @@ let record_inconsistent_type_annotations ctxt loc ta tb = Inconsistent_type_annotations (loc, ta, tb)) let rec ty_eq - : type ta tb. context -> ta ty -> tb ty -> (ta ty, tb ty) eq tzresult + : type ta tb. context -> ta ty -> tb ty -> ((ta ty, tb ty) eq * context) tzresult = fun ctxt ta tb -> + let ok (eq : (ta ty, tb ty) eq) ctxt nb_args : + ((ta ty, tb ty) eq * context) tzresult = + Gas.consume ctxt (Typecheck_costs.type_ (2 * nb_args)) >>? fun ctxt -> + Ok (eq, ctxt) in + Gas.consume ctxt Typecheck_costs.cycle >>? fun ctxt -> match ta, tb with - | Unit_t _, Unit_t _ -> Ok Eq - | Int_t _, Int_t _ -> Ok Eq - | Nat_t _, Nat_t _ -> Ok Eq - | Key_t _, Key_t _ -> Ok Eq - | Key_hash_t _, Key_hash_t _ -> Ok Eq - | String_t _, String_t _ -> Ok Eq - | Bytes_t _, Bytes_t _ -> Ok Eq - | Signature_t _, Signature_t _ -> Ok Eq - | Mutez_t _, Mutez_t _ -> Ok Eq - | Timestamp_t _, Timestamp_t _ -> Ok Eq - | Address_t _, Address_t _ -> Ok Eq - | Bool_t _, Bool_t _ -> Ok Eq - | Operation_t _, Operation_t _ -> Ok Eq + | Unit_t _, Unit_t _ -> ok Eq ctxt 0 + | Int_t _, Int_t _ -> ok Eq ctxt 0 + | Nat_t _, Nat_t _ -> ok Eq ctxt 0 + | Key_t _, Key_t _ -> ok Eq ctxt 0 + | Key_hash_t _, Key_hash_t _ -> ok Eq ctxt 0 + | String_t _, String_t _ -> ok Eq ctxt 0 + | Bytes_t _, Bytes_t _ -> ok Eq ctxt 0 + | Signature_t _, Signature_t _ -> ok Eq ctxt 0 + | Mutez_t _, Mutez_t _ -> ok Eq ctxt 0 + | Timestamp_t _, Timestamp_t _ -> ok Eq ctxt 0 + | Address_t _, Address_t _ -> ok Eq ctxt 0 + | Bool_t _, Bool_t _ -> ok Eq ctxt 0 + | Operation_t _, Operation_t _ -> ok Eq ctxt 0 | Map_t (tal, tar, _), Map_t (tbl, tbr, _) -> (comparable_ty_eq ctxt tal tbl >>? fun Eq -> - ty_eq ctxt tar tbr >>? fun Eq -> - (Ok Eq : (ta ty, tb ty) eq tzresult)) |> + ty_eq ctxt tar tbr >>? fun (Eq, ctxt) -> + (ok Eq ctxt 2)) |> record_inconsistent ctxt ta tb | Big_map_t (tal, tar, _), Big_map_t (tbl, tbr, _) -> (comparable_ty_eq ctxt tal tbl >>? fun Eq -> - ty_eq ctxt tar tbr >>? fun Eq -> - (Ok Eq : (ta ty, tb ty) eq tzresult)) |> + ty_eq ctxt tar tbr >>? fun (Eq, ctxt) -> + (ok Eq ctxt 2)) |> record_inconsistent ctxt ta tb | Set_t (ea, _), Set_t (eb, _) -> (comparable_ty_eq ctxt ea eb >>? fun Eq -> - (Ok Eq : (ta ty, tb ty) eq tzresult)) |> + (ok Eq ctxt 1)) |> record_inconsistent ctxt ta tb | Pair_t ((tal, _, _), (tar, _, _), _), Pair_t ((tbl, _, _), (tbr, _, _), _) -> - (ty_eq ctxt tal tbl >>? fun Eq -> - ty_eq ctxt tar tbr >>? fun Eq -> - (Ok Eq : (ta ty, tb ty) eq tzresult)) |> + (ty_eq ctxt tal tbl >>? fun (Eq, ctxt) -> + ty_eq ctxt tar tbr >>? fun (Eq, ctxt) -> + (ok Eq ctxt 2)) |> record_inconsistent ctxt ta tb | Union_t ((tal, _), (tar, _), _), Union_t ((tbl, _), (tbr, _), _) -> - (ty_eq ctxt tal tbl >>? fun Eq -> - ty_eq ctxt tar tbr >>? fun Eq -> - (Ok Eq : (ta ty, tb ty) eq tzresult)) |> + (ty_eq ctxt tal tbl >>? fun (Eq, ctxt) -> + ty_eq ctxt tar tbr >>? fun (Eq, ctxt) -> + (ok Eq ctxt 2)) |> record_inconsistent ctxt ta tb | Lambda_t (tal, tar, _), Lambda_t (tbl, tbr, _) -> - (ty_eq ctxt tal tbl >>? fun Eq -> - ty_eq ctxt tar tbr >>? fun Eq -> - (Ok Eq : (ta ty, tb ty) eq tzresult)) |> + (ty_eq ctxt tal tbl >>? fun (Eq, ctxt) -> + ty_eq ctxt tar tbr >>? fun (Eq, ctxt) -> + (ok Eq ctxt 2)) |> record_inconsistent ctxt ta tb | Contract_t (tal, _), Contract_t (tbl, _) -> - (ty_eq ctxt tal tbl >>? fun Eq -> - (Ok Eq : (ta ty, tb ty) eq tzresult)) |> + (ty_eq ctxt tal tbl >>? fun (Eq, ctxt) -> + (ok Eq ctxt 1)) |> record_inconsistent ctxt ta tb | Option_t ((tva, _), _, _), Option_t ((tvb, _), _, _) -> - (ty_eq ctxt tva tvb >>? fun Eq -> - (Ok Eq : (ta ty, tb ty) eq tzresult)) |> + (ty_eq ctxt tva tvb >>? fun (Eq, ctxt) -> + (ok Eq ctxt 1)) |> record_inconsistent ctxt ta tb | List_t (tva, _), List_t (tvb, _) -> - (ty_eq ctxt tva tvb >>? fun Eq -> - (Ok Eq : (ta ty, tb ty) eq tzresult)) |> + (ty_eq ctxt tva tvb >>? fun (Eq, ctxt) -> + (ok Eq ctxt 1)) |> record_inconsistent ctxt ta tb | _, _ -> serialize_ty_for_error ctxt ta >>? fun (ta, ctxt) -> @@ -774,15 +779,16 @@ let rec ty_eq let rec stack_ty_eq : type ta tb. context -> int -> ta stack_ty -> tb stack_ty -> - (ta stack_ty, tb stack_ty) eq tzresult = fun ctxt lvl ta tb -> - match ta, tb with - | Item_t (tva, ra, _), Item_t (tvb, rb, _) -> - ty_eq ctxt tva tvb |> - record_trace (fun () -> ok (Bad_stack_item lvl)) >>? fun Eq -> - stack_ty_eq ctxt (lvl + 1) ra rb >>? fun Eq -> - (Ok Eq : (ta stack_ty, tb stack_ty) eq tzresult) - | Empty_t, Empty_t -> Ok Eq - | _, _ -> error Bad_stack_length + ((ta stack_ty, tb stack_ty) eq * context) tzresult + = fun ctxt lvl ta tb -> + match ta, tb with + | Item_t (tva, ra, _), Item_t (tvb, rb, _) -> + ty_eq ctxt tva tvb |> + record_trace (fun () -> ok (Bad_stack_item lvl)) >>? fun (Eq, ctxt) -> + stack_ty_eq ctxt (lvl + 1) ra rb >>? fun (Eq, ctxt) -> + (Ok (Eq, ctxt) : ((ta stack_ty, tb stack_ty) eq * context) tzresult) + | Empty_t, Empty_t -> Ok (Eq, ctxt) + | _, _ -> error Bad_stack_length let merge_comparable_types : type ta. ta comparable_ty -> ta comparable_ty -> ta comparable_ty tzresult @@ -822,122 +828,125 @@ let rec strip_annotations = function | Seq (loc, items) -> Seq (loc, List.map strip_annotations items) let merge_types : - type b. context -> Script.location -> b ty -> b ty -> b ty tzresult = - fun ctxt -> - let rec help : type a. a ty -> a ty -> a ty tzresult - = fun ty1 ty2 -> - match ty1, ty2 with - | Unit_t tn1, Unit_t tn2 -> - merge_type_annot tn1 tn2 >|? fun tname -> - Unit_t tname - | Int_t tn1, Int_t tn2 -> - merge_type_annot tn1 tn2 >|? fun tname -> - Int_t tname - | Nat_t tn1, Nat_t tn2 -> - merge_type_annot tn1 tn2 >|? fun tname -> - Nat_t tname - | Key_t tn1, Key_t tn2 -> - merge_type_annot tn1 tn2 >|? fun tname -> - Key_t tname - | Key_hash_t tn1, Key_hash_t tn2 -> - merge_type_annot tn1 tn2 >|? fun tname -> - Key_hash_t tname - | String_t tn1, String_t tn2 -> - merge_type_annot tn1 tn2 >|? fun tname -> - String_t tname - | Bytes_t tn1, Bytes_t tn2 -> - merge_type_annot tn1 tn2 >|? fun tname -> - Bytes_t tname - | Signature_t tn1, Signature_t tn2 -> - merge_type_annot tn1 tn2 >|? fun tname -> - Signature_t tname - | Mutez_t tn1, Mutez_t tn2 -> - merge_type_annot tn1 tn2 >|? fun tname -> - Mutez_t tname - | Timestamp_t tn1, Timestamp_t tn2 -> - merge_type_annot tn1 tn2 >|? fun tname -> - Timestamp_t tname - | Address_t tn1, Address_t tn2 -> - merge_type_annot tn1 tn2 >|? fun tname -> - Address_t tname - | Bool_t tn1, Bool_t tn2 -> - merge_type_annot tn1 tn2 >|? fun tname -> - Bool_t tname - | Operation_t tn1, Operation_t tn2 -> - merge_type_annot tn1 tn2 >|? fun tname -> - Operation_t tname - | Map_t (tal, tar, tn1), Map_t (tbl, tbr, tn2) -> - merge_type_annot tn1 tn2 >>? fun tname -> - help tar tbr >>? fun value -> - ty_eq ctxt tar value >>? fun Eq -> - merge_comparable_types tal tbl >|? fun tk -> - Map_t (tk, value, tname) - | Big_map_t (tal, tar, tn1), Big_map_t (tbl, tbr, tn2) -> - merge_type_annot tn1 tn2 >>? fun tname -> - help tar tbr >>? fun value -> - ty_eq ctxt tar value >>? fun Eq -> - merge_comparable_types tal tbl >|? fun tk -> - Big_map_t (tk, value, tname) - | Set_t (ea, tn1), Set_t (eb, tn2) -> - merge_type_annot tn1 tn2 >>? fun tname -> - merge_comparable_types ea eb >|? fun e -> - Set_t (e, tname) - | Pair_t ((tal, l_field1, l_var1), (tar, r_field1, r_var1), tn1), - Pair_t ((tbl, l_field2, l_var2), (tbr, r_field2, r_var2), tn2) -> - merge_type_annot tn1 tn2 >>? fun tname -> - merge_field_annot l_field1 l_field2 >>? fun l_field -> - merge_field_annot r_field1 r_field2 >>? fun r_field -> - let l_var = merge_var_annot l_var1 l_var2 in - let r_var = merge_var_annot r_var1 r_var2 in - help tal tbl >>? fun left_ty -> - help tar tbr >|? fun right_ty -> - Pair_t ((left_ty, l_field, l_var), (right_ty, r_field, r_var), tname) - | Union_t ((tal, tal_annot), (tar, tar_annot), tn1), - Union_t ((tbl, tbl_annot), (tbr, tbr_annot), tn2) -> - merge_type_annot tn1 tn2 >>? fun tname -> - merge_field_annot tal_annot tbl_annot >>? fun left_annot -> - merge_field_annot tar_annot tbr_annot >>? fun right_annot -> - help tal tbl >>? fun left_ty -> - help tar tbr >|? fun right_ty -> - Union_t ((left_ty, left_annot), (right_ty, right_annot), tname) - | Lambda_t (tal, tar, tn1), Lambda_t (tbl, tbr, tn2) -> - merge_type_annot tn1 tn2 >>? fun tname -> - help tal tbl >>? fun left_ty -> - help tar tbr >|? fun right_ty -> - Lambda_t (left_ty, right_ty, tname) - | Contract_t (tal, tn1), Contract_t (tbl, tn2) -> - merge_type_annot tn1 tn2 >>? fun tname -> - help tal tbl >|? fun arg_ty -> - Contract_t (arg_ty, tname) - | Option_t ((tva, some_annot_a), none_annot_a, tn1), - Option_t ((tvb, some_annot_b), none_annot_b, tn2) -> - merge_type_annot tn1 tn2 >>? fun tname -> - merge_field_annot some_annot_a some_annot_b >>? fun some_annot -> - merge_field_annot none_annot_a none_annot_b >>? fun none_annot -> - help tva tvb >|? fun ty -> - Option_t ((ty, some_annot), none_annot, tname) - | List_t (tva, tn1), List_t (tvb, tn2) -> - merge_type_annot tn1 tn2 >>? fun tname -> - help tva tvb >|? fun ty -> - List_t (ty, tname) - | _, _ -> assert false - in (fun loc ty1 ty2 -> - record_inconsistent_type_annotations ctxt loc ty1 ty2 - (help ty1 ty2)) + type b. context -> Script.location -> b ty -> b ty -> (b ty * context) tzresult = + let rec help : type a. context -> a ty -> a ty -> (a ty * context) tzresult + = fun ctxt ty1 ty2 -> + match ty1, ty2 with + | Unit_t tn1, Unit_t tn2 -> + merge_type_annot tn1 tn2 >|? fun tname -> + Unit_t tname, ctxt + | Int_t tn1, Int_t tn2 -> + merge_type_annot tn1 tn2 >|? fun tname -> + Int_t tname, ctxt + | Nat_t tn1, Nat_t tn2 -> + merge_type_annot tn1 tn2 >|? fun tname -> + Nat_t tname, ctxt + | Key_t tn1, Key_t tn2 -> + merge_type_annot tn1 tn2 >|? fun tname -> + Key_t tname, ctxt + | Key_hash_t tn1, Key_hash_t tn2 -> + merge_type_annot tn1 tn2 >|? fun tname -> + Key_hash_t tname, ctxt + | String_t tn1, String_t tn2 -> + merge_type_annot tn1 tn2 >|? fun tname -> + String_t tname, ctxt + | Bytes_t tn1, Bytes_t tn2 -> + merge_type_annot tn1 tn2 >|? fun tname -> + Bytes_t tname, ctxt + | Signature_t tn1, Signature_t tn2 -> + merge_type_annot tn1 tn2 >|? fun tname -> + Signature_t tname, ctxt + | Mutez_t tn1, Mutez_t tn2 -> + merge_type_annot tn1 tn2 >|? fun tname -> + Mutez_t tname, ctxt + | Timestamp_t tn1, Timestamp_t tn2 -> + merge_type_annot tn1 tn2 >|? fun tname -> + Timestamp_t tname, ctxt + | Address_t tn1, Address_t tn2 -> + merge_type_annot tn1 tn2 >|? fun tname -> + Address_t tname, ctxt + | Bool_t tn1, Bool_t tn2 -> + merge_type_annot tn1 tn2 >|? fun tname -> + Bool_t tname, ctxt + | Operation_t tn1, Operation_t tn2 -> + merge_type_annot tn1 tn2 >|? fun tname -> + Operation_t tname, ctxt + | Map_t (tal, tar, tn1), Map_t (tbl, tbr, tn2) -> + merge_type_annot tn1 tn2 >>? fun tname -> + help ctxt tar tbr >>? fun (value, ctxt) -> + ty_eq ctxt tar value >>? fun (Eq, ctxt) -> + merge_comparable_types tal tbl >|? fun tk -> + Map_t (tk, value, tname), ctxt + | Big_map_t (tal, tar, tn1), Big_map_t (tbl, tbr, tn2) -> + merge_type_annot tn1 tn2 >>? fun tname -> + help ctxt tar tbr >>? fun (value, ctxt) -> + ty_eq ctxt tar value >>? fun (Eq, ctxt) -> + merge_comparable_types tal tbl >|? fun tk -> + Big_map_t (tk, value, tname), ctxt + | Set_t (ea, tn1), Set_t (eb, tn2) -> + merge_type_annot tn1 tn2 >>? fun tname -> + merge_comparable_types ea eb >|? fun e -> + Set_t (e, tname), ctxt + | Pair_t ((tal, l_field1, l_var1), (tar, r_field1, r_var1), tn1), + Pair_t ((tbl, l_field2, l_var2), (tbr, r_field2, r_var2), tn2) -> + merge_type_annot tn1 tn2 >>? fun tname -> + merge_field_annot l_field1 l_field2 >>? fun l_field -> + merge_field_annot r_field1 r_field2 >>? fun r_field -> + let l_var = merge_var_annot l_var1 l_var2 in + let r_var = merge_var_annot r_var1 r_var2 in + help ctxt tal tbl >>? fun (left_ty, ctxt) -> + help ctxt tar tbr >|? fun (right_ty, ctxt) -> + Pair_t ((left_ty, l_field, l_var), (right_ty, r_field, r_var), tname), + ctxt + | Union_t ((tal, tal_annot), (tar, tar_annot), tn1), + Union_t ((tbl, tbl_annot), (tbr, tbr_annot), tn2) -> + merge_type_annot tn1 tn2 >>? fun tname -> + merge_field_annot tal_annot tbl_annot >>? fun left_annot -> + merge_field_annot tar_annot tbr_annot >>? fun right_annot -> + help ctxt tal tbl >>? fun (left_ty, ctxt) -> + help ctxt tar tbr >|? fun (right_ty, ctxt) -> + Union_t ((left_ty, left_annot), (right_ty, right_annot), tname), + ctxt + | Lambda_t (tal, tar, tn1), Lambda_t (tbl, tbr, tn2) -> + merge_type_annot tn1 tn2 >>? fun tname -> + help ctxt tal tbl >>? fun (left_ty, ctxt) -> + help ctxt tar tbr >|? fun (right_ty, ctxt) -> + Lambda_t (left_ty, right_ty, tname), ctxt + | Contract_t (tal, tn1), Contract_t (tbl, tn2) -> + merge_type_annot tn1 tn2 >>? fun tname -> + help ctxt tal tbl >|? fun (arg_ty, ctxt) -> + Contract_t (arg_ty, tname), ctxt + | Option_t ((tva, some_annot_a), none_annot_a, tn1), + Option_t ((tvb, some_annot_b), none_annot_b, tn2) -> + merge_type_annot tn1 tn2 >>? fun tname -> + merge_field_annot some_annot_a some_annot_b >>? fun some_annot -> + merge_field_annot none_annot_a none_annot_b >>? fun none_annot -> + help ctxt tva tvb >|? fun (ty, ctxt) -> + Option_t ((ty, some_annot), none_annot, tname), ctxt + | List_t (tva, tn1), List_t (tvb, tn2) -> + merge_type_annot tn1 tn2 >>? fun tname -> + help ctxt tva tvb >|? fun (ty, ctxt) -> + List_t (ty, tname), ctxt + | _, _ -> assert false + in (fun ctxt loc ty1 ty2 -> + record_inconsistent_type_annotations ctxt loc ty1 ty2 + (help ctxt ty1 ty2)) let merge_stacks - : type ta. context -> Script.location -> ta stack_ty -> ta stack_ty -> ta stack_ty tzresult - = fun ctxt loc -> - let rec help : type a. a stack_ty -> a stack_ty -> a stack_ty tzresult - = fun stack1 stack2 -> + : type ta. Script.location -> context -> ta stack_ty -> ta stack_ty -> + (ta stack_ty * context) tzresult + = fun loc -> + let rec help : type a. context -> a stack_ty -> a stack_ty -> + (a stack_ty * context) tzresult + = fun ctxt stack1 stack2 -> match stack1, stack2 with - | Empty_t, Empty_t -> ok Empty_t + | Empty_t, Empty_t -> ok (Empty_t, ctxt) | Item_t (ty1, rest1, annot1), Item_t (ty2, rest2, annot2) -> let annot = merge_var_annot annot1 annot2 in - merge_types ctxt loc ty1 ty2 >>? fun ty -> - help rest1 rest2 >|? fun rest -> - Item_t (ty, rest, annot) + merge_types ctxt loc ty1 ty2 >>? fun (ty, ctxt) -> + help ctxt rest1 rest2 >|? fun (rest, ctxt) -> + Item_t (ty, rest, annot), ctxt in help (* ---- Type checker results -------------------------------------------------*) @@ -955,7 +964,7 @@ type ('t, 'f, 'b) branch = let merge_branches : type bef a b. context -> int -> a judgement -> b judgement -> (a, b, bef) branch -> - bef judgement tzresult Lwt.t + (bef judgement * context) tzresult Lwt.t = fun ctxt loc btr bfr { branch } -> match btr, bfr with | Typed ({ aft = aftbt ; _ } as dbt), Typed ({ aft = aftbf ; _ } as dbf) -> @@ -964,17 +973,19 @@ let merge_branches serialize_stack_for_error ctxt aftbf >>|? fun (aftbf, _ctxt) -> Unmatched_branches (loc, aftbt, aftbf) in trace unmatched_branches - (Lwt.return (stack_ty_eq ctxt 1 aftbt aftbf) >>=? fun Eq -> - Lwt.return (merge_stacks ctxt loc aftbt aftbf) >>=? fun merged_stack -> - return (Typed (branch {dbt with aft=merged_stack} {dbf with aft=merged_stack}))) + (Lwt.return (stack_ty_eq ctxt 1 aftbt aftbf) >>=? fun (Eq, ctxt) -> + Lwt.return (merge_stacks loc ctxt aftbt aftbf) >>=? fun (merged_stack, ctxt) -> + return ( + Typed (branch {dbt with aft=merged_stack} {dbf with aft=merged_stack}), + ctxt)) | Failed { descr = descrt }, Failed { descr = descrf } -> let descr ret = branch (descrt ret) (descrf ret) in - return (Failed { descr }) + return (Failed { descr }, ctxt) | Typed dbt, Failed { descr = descrf } -> - return (Typed (branch dbt (descrf dbt.aft))) + return (Typed (branch dbt (descrf dbt.aft)), ctxt) | Failed { descr = descrt }, Typed dbf -> - return (Typed (branch (descrt dbf.aft) dbf)) + return (Typed (branch (descrt dbf.aft) dbf), ctxt) let rec parse_comparable_ty : context -> Script.node -> (ex_comparable_ty * context) tzresult @@ -1535,22 +1546,22 @@ and parse_returning fun ?type_logger tc_context ctxt (arg, arg_annot) ret script_instr -> parse_instr ?type_logger tc_context ctxt script_instr (Item_t (arg, Empty_t, arg_annot)) >>=? function - | (Typed ({ loc ; aft = (Item_t (ty, Empty_t, _) as stack_ty) ; _ } as descr), gas) -> + | (Typed ({ loc ; aft = (Item_t (ty, Empty_t, _) as stack_ty) ; _ } as descr), ctxt) -> trace (fun () -> Lwt.return (serialize_ty_for_error ctxt ret) >>=? fun (ret, ctxt) -> serialize_stack_for_error ctxt stack_ty >>|? fun (stack_ty, _ctxt) -> Bad_return (loc, stack_ty, ret)) - (Lwt.return (ty_eq ctxt ty ret) >>=? fun Eq -> - Lwt.return (merge_types ctxt loc ty ret) >>=? fun _ret -> - return ((Lam (descr, strip_locations script_instr) : (arg, ret) lambda), gas)) - | (Typed { loc ; aft = stack_ty ; _ }, _gas) -> + (Lwt.return (ty_eq ctxt ty ret) >>=? fun (Eq, ctxt) -> + Lwt.return (merge_types ctxt loc ty ret) >>=? fun (_ret, ctxt) -> + return ((Lam (descr, strip_locations script_instr) : (arg, ret) lambda), ctxt)) + | (Typed { loc ; aft = stack_ty ; _ }, ctxt) -> Lwt.return (serialize_ty_for_error ctxt ret) >>=? fun (ret, ctxt) -> serialize_stack_for_error ctxt stack_ty >>=? fun (stack_ty, _ctxt) -> fail (Bad_return (loc, stack_ty, ret)) - | (Failed { descr }, gas) -> + | (Failed { descr }, ctxt) -> return ((Lam (descr (Item_t (ret, Empty_t, None)), strip_locations script_instr) - : (arg, ret) lambda), gas) + : (arg, ret) lambda), ctxt) and parse_instr : type bef. @@ -1564,7 +1575,7 @@ and parse_instr Bad_stack (loc, name, m, stack_ty)) @@ trace (fun () -> return (Bad_stack_item n)) @@ Lwt.return check in - let check_item_ty exp got loc n = + let check_item_ty ctxt exp got loc n = check_item (ty_eq ctxt exp got) loc n in let log_stack ctxt loc stack_ty aft = match type_logger, script_instr with @@ -1649,7 +1660,7 @@ and parse_instr parse_instr ?type_logger tc_context ctxt bf (Item_t (t, rest, annot)) >>=? fun (bfr, ctxt) -> let branch ibt ibf = { loc ; instr = If_none (ibt, ibf) ; bef ; aft = ibt.aft } in - merge_branches ctxt loc btr bfr { branch } >>=? fun judgement -> + merge_branches ctxt loc btr bfr { branch } >>=? fun (judgement, ctxt) -> return ctxt judgement (* pairs *) | Prim (loc, I_PAIR, [], annot), @@ -1706,7 +1717,7 @@ and parse_instr parse_instr ?type_logger tc_context ctxt bf (Item_t (tr, rest, right_annot)) >>=? fun (bfr, ctxt) -> let branch ibt ibf = { loc ; instr = If_left (ibt, ibf) ; bef ; aft = ibt.aft } in - merge_branches ctxt loc btr bfr { branch } >>=? fun judgement -> + merge_branches ctxt loc btr bfr { branch } >>=? fun (judgement, ctxt) -> return ctxt judgement (* lists *) | Prim (loc, I_NIL, [ t ], annot), @@ -1716,7 +1727,7 @@ and parse_instr typed ctxt loc Nil (Item_t (List_t (t, ty_name), stack, annot)) | Prim (loc, I_CONS, [], annot), Item_t (tv, Item_t (List_t (t, ty_name), rest, _), _) -> - check_item_ty tv t loc I_CONS 1 2 >>=? fun Eq -> + check_item_ty ctxt tv t loc I_CONS 1 2 >>=? fun (Eq, ctxt) -> parse_var_annot loc annot >>=? fun annot -> typed ctxt loc Cons_list (Item_t (List_t (t, ty_name), rest, annot)) | Prim (loc, I_IF_CONS, [ bt ; bf ], annot), @@ -1733,7 +1744,7 @@ and parse_instr rest >>=? fun (bfr, ctxt) -> let branch ibt ibf = { loc ; instr = If_cons (ibt, ibf) ; bef ; aft = ibt.aft } in - merge_branches ctxt loc btr bfr { branch } >>=? fun judgement -> + merge_branches ctxt loc btr bfr { branch } >>=? fun (judgement, ctxt) -> return ctxt judgement | Prim (loc, I_SIZE, [], annot), Item_t (List_t _, rest, _) -> @@ -1753,8 +1764,8 @@ and parse_instr serialize_stack_for_error ctxt ibody.aft >>|? fun (aft, _ctxt) -> Invalid_map_body (loc, aft) in trace invalid_map_body - (Lwt.return @@ stack_ty_eq ctxt 1 rest starting_rest >>=? fun Eq -> - Lwt.return @@ merge_stacks ctxt loc rest starting_rest >>=? fun rest -> + (Lwt.return @@ stack_ty_eq ctxt 1 rest starting_rest >>=? fun (Eq, ctxt) -> + Lwt.return @@ merge_stacks loc ctxt rest starting_rest >>=? fun (rest, ctxt) -> typed ctxt loc (List_map ibody) (Item_t (List_t (ret, list_ty_name), rest, ret_annot))) | Typed { aft ; _ } -> @@ -1776,8 +1787,8 @@ and parse_instr serialize_stack_for_error ctxt rest >>|? fun (rest, _ctxt) -> Invalid_iter_body (loc, rest, aft) in trace invalid_iter_body - (Lwt.return @@ stack_ty_eq ctxt 1 aft rest >>=? fun Eq -> - Lwt.return @@ merge_stacks ctxt loc aft rest >>=? fun rest -> + (Lwt.return @@ stack_ty_eq ctxt 1 aft rest >>=? fun (Eq, ctxt) -> + Lwt.return @@ merge_stacks loc ctxt aft rest >>=? fun (rest, ctxt) -> typed ctxt loc (List_iter ibody) rest) | Failed { descr } -> typed ctxt loc (List_iter (descr rest)) rest @@ -1803,8 +1814,8 @@ and parse_instr serialize_stack_for_error ctxt rest >>|? fun (rest, _ctxt) -> Invalid_iter_body (loc, rest, aft) in trace invalid_iter_body - (Lwt.return @@ stack_ty_eq ctxt 1 aft rest >>=? fun Eq -> - Lwt.return @@ merge_stacks ctxt loc aft rest >>=? fun rest -> + (Lwt.return @@ stack_ty_eq ctxt 1 aft rest >>=? fun (Eq, ctxt) -> + Lwt.return @@ merge_stacks loc ctxt aft rest >>=? fun (rest, ctxt) -> typed ctxt loc (Set_iter ibody) rest) | Failed { descr } -> typed ctxt loc (Set_iter (descr rest)) rest @@ -1813,13 +1824,13 @@ and parse_instr Item_t (v, Item_t (Set_t (elt, _), rest, _), _) -> let elt = ty_of_comparable_ty elt in parse_var_type_annot loc annot >>=? fun (annot, tname) -> - check_item_ty elt v loc I_MEM 1 2 >>=? fun Eq -> + check_item_ty ctxt elt v loc I_MEM 1 2 >>=? fun (Eq, ctxt) -> typed ctxt loc Set_mem (Item_t (Bool_t tname, rest, annot)) | Prim (loc, I_UPDATE, [], annot), Item_t (v, Item_t (Bool_t _, Item_t (Set_t (elt, tname), rest, set_annot), _), _) -> let ty = ty_of_comparable_ty elt in parse_var_annot loc annot ~default:set_annot >>=? fun annot -> - check_item_ty ty v loc I_UPDATE 1 3 >>=? fun Eq -> + check_item_ty ctxt ty v loc I_UPDATE 1 3 >>=? fun (Eq, ctxt) -> typed ctxt loc Set_update (Item_t (Set_t (elt, tname), rest, annot)) | Prim (loc, I_SIZE, [], annot), Item_t (Set_t _, rest, _) -> @@ -1848,8 +1859,8 @@ and parse_instr serialize_stack_for_error ctxt ibody.aft >>|? fun (aft, _ctxt) -> Invalid_map_body (loc, aft) in trace invalid_map_body - (Lwt.return @@ stack_ty_eq ctxt 1 rest starting_rest >>=? fun Eq -> - Lwt.return @@ merge_stacks ctxt loc rest starting_rest >>=? fun rest -> + (Lwt.return @@ stack_ty_eq ctxt 1 rest starting_rest >>=? fun (Eq, ctxt) -> + Lwt.return @@ merge_stacks loc ctxt rest starting_rest >>=? fun (rest, ctxt) -> typed ctxt loc (Map_map ibody) (Item_t (Map_t (ck, ret, ty_name), rest, ret_annot))) | Typed { aft ; _ } -> @@ -1874,8 +1885,8 @@ and parse_instr serialize_stack_for_error ctxt rest >>|? fun (rest, _ctxt) -> Invalid_iter_body (loc, rest, aft) in trace invalid_iter_body - (Lwt.return @@ stack_ty_eq ctxt 1 aft rest >>=? fun Eq -> - Lwt.return @@ merge_stacks ctxt loc aft rest >>=? fun rest -> + (Lwt.return @@ stack_ty_eq ctxt 1 aft rest >>=? fun (Eq, ctxt) -> + Lwt.return @@ merge_stacks loc ctxt aft rest >>=? fun (rest, ctxt) -> typed ctxt loc (Map_iter ibody) rest) | Failed { descr } -> typed ctxt loc (Map_iter (descr rest)) rest @@ -1883,21 +1894,21 @@ and parse_instr | Prim (loc, I_MEM, [], annot), Item_t (vk, Item_t (Map_t (ck, _, _), rest, _), _) -> let k = ty_of_comparable_ty ck in - check_item_ty vk k loc I_MEM 1 2 >>=? fun Eq -> + check_item_ty ctxt vk k loc I_MEM 1 2 >>=? fun (Eq, ctxt) -> parse_var_annot loc annot >>=? fun annot -> typed ctxt loc Map_mem (Item_t (Bool_t None, rest, annot)) | Prim (loc, I_GET, [], annot), Item_t (vk, Item_t (Map_t (ck, elt, _), rest, _), _) -> let k = ty_of_comparable_ty ck in - check_item_ty vk k loc I_GET 1 2 >>=? fun Eq -> + check_item_ty ctxt vk k loc I_GET 1 2 >>=? fun (Eq, ctxt) -> parse_var_annot loc annot >>=? fun annot -> typed ctxt loc Map_get (Item_t (Option_t ((elt, None), None, None), rest, annot)) | Prim (loc, I_UPDATE, [], annot), Item_t (vk, Item_t (Option_t ((vv, _), _, _), Item_t (Map_t (ck, v, map_name), rest, map_annot), _), _) -> let k = ty_of_comparable_ty ck in - check_item_ty vk k loc I_UPDATE 1 3 >>=? fun Eq -> - check_item_ty vv v loc I_UPDATE 2 3 >>=? fun Eq -> + 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) -> parse_var_annot loc annot ~default:map_annot >>=? fun annot -> typed ctxt loc Map_update (Item_t (Map_t (ck, v, map_name), rest, annot)) | Prim (loc, I_SIZE, [], annot), @@ -1908,13 +1919,13 @@ and parse_instr | Prim (loc, I_MEM, [], annot), Item_t (set_key, Item_t (Big_map_t (map_key, _, _), rest, _), _) -> let k = ty_of_comparable_ty map_key in - check_item_ty set_key k loc I_MEM 1 2 >>=? fun Eq -> + check_item_ty ctxt set_key k loc I_MEM 1 2 >>=? fun (Eq, ctxt) -> parse_var_annot loc annot >>=? fun annot -> typed ctxt loc Big_map_mem (Item_t (Bool_t None, rest, annot)) | Prim (loc, I_GET, [], annot), Item_t (vk, Item_t (Big_map_t (ck, elt, _), rest, _), _) -> let k = ty_of_comparable_ty ck in - check_item_ty vk k loc I_GET 1 2 >>=? fun Eq -> + check_item_ty ctxt vk k loc I_GET 1 2 >>=? fun (Eq, ctxt) -> parse_var_annot loc annot >>=? fun annot -> typed ctxt loc Big_map_get (Item_t (Option_t ((elt, None), None, None), rest, annot)) | Prim (loc, I_UPDATE, [], annot), @@ -1922,8 +1933,8 @@ and parse_instr Item_t (Option_t ((set_value, _), _, _), Item_t (Big_map_t (map_key, map_value, map_name), rest, map_annot), _), _) -> let k = ty_of_comparable_ty map_key in - check_item_ty set_key k loc I_UPDATE 1 3 >>=? fun Eq -> - check_item_ty set_value map_value loc I_UPDATE 2 3 >>=? fun Eq -> + check_item_ty ctxt set_key k loc I_UPDATE 1 3 >>=? fun (Eq, ctxt) -> + check_item_ty ctxt set_value map_value loc I_UPDATE 2 3 >>=? fun (Eq, ctxt) -> parse_var_annot loc annot ~default:map_annot >>=? fun annot -> typed ctxt loc Big_map_update (Item_t (Big_map_t (map_key, map_value, map_name), rest, annot)) (* control *) @@ -1973,7 +1984,7 @@ and parse_instr parse_instr ?type_logger tc_context ctxt bf rest >>=? fun (bfr, ctxt) -> let branch ibt ibf = { loc ; instr = If (ibt, ibf) ; bef ; aft = ibt.aft } in - merge_branches ctxt loc btr bfr { branch } >>=? fun judgement -> + merge_branches ctxt loc btr bfr { branch } >>=? fun (judgement, ctxt) -> return ctxt judgement | Prim (loc, I_LOOP, [ body ], annot), (Item_t (Bool_t _, rest, _stack_annot) as stack) -> @@ -1988,8 +1999,8 @@ and parse_instr serialize_stack_for_error ctxt stack >>|? fun (stack, _ctxt) -> Unmatched_branches (loc, aft, stack) in trace unmatched_branches - (Lwt.return @@ stack_ty_eq ctxt 1 ibody.aft stack >>=? fun Eq -> - Lwt.return @@ merge_stacks ctxt loc ibody.aft stack >>=? fun _stack -> + (Lwt.return @@ stack_ty_eq ctxt 1 ibody.aft stack >>=? fun (Eq, ctxt) -> + Lwt.return @@ merge_stacks loc ctxt ibody.aft stack >>=? fun (_stack, ctxt) -> typed ctxt loc (Loop ibody) rest) | Failed { descr } -> let ibody = descr stack in @@ -2008,8 +2019,8 @@ and parse_instr serialize_stack_for_error ctxt stack >>|? fun (stack, _ctxt) -> Unmatched_branches (loc, aft, stack) in trace unmatched_branches - (Lwt.return @@ stack_ty_eq ctxt 1 ibody.aft stack >>=? fun Eq -> - Lwt.return @@ merge_stacks ctxt loc ibody.aft stack >>=? fun _stack -> + (Lwt.return @@ stack_ty_eq ctxt 1 ibody.aft stack >>=? fun (Eq, ctxt) -> + Lwt.return @@ merge_stacks loc ctxt ibody.aft stack >>=? fun (_stack, ctxt) -> typed ctxt loc (Loop_left ibody) (Item_t (tr, rest, annot))) | Failed { descr } -> let ibody = descr stack in @@ -2028,7 +2039,7 @@ and parse_instr typed ctxt loc (Lambda lambda) (Item_t (Lambda_t (arg, ret, None), stack, annot)) | Prim (loc, I_EXEC, [], annot), Item_t (arg, Item_t (Lambda_t (param, ret, _), rest, _), _) -> - check_item_ty arg param loc I_EXEC 1 2 >>=? fun Eq -> + check_item_ty ctxt arg param loc I_EXEC 1 2 >>=? fun (Eq, ctxt) -> parse_var_annot loc annot >>=? fun annot -> typed ctxt loc Exec (Item_t (ret, rest, annot)) | Prim (loc, I_DIP, [ code ], annot), @@ -2404,8 +2415,8 @@ and parse_instr parse_var_annot loc annot ~default:item_annot >>=? fun annot -> (Lwt.return @@ parse_ty ctxt ~allow_big_map:true ~allow_operation:true cast_t) >>=? fun (Ex_ty cast_t, ctxt) -> - Lwt.return @@ ty_eq ctxt cast_t t >>=? fun Eq -> - Lwt.return @@ merge_types ctxt loc cast_t t >>=? fun _ -> + Lwt.return @@ ty_eq ctxt cast_t t >>=? fun (Eq, ctxt) -> + Lwt.return @@ merge_types ctxt loc cast_t t >>=? fun (_, ctxt) -> typed ctxt loc Nop (Item_t (cast_t, stack, annot)) | Prim (loc, I_RENAME, [], annot), Item_t (t, stack, _) -> @@ -2446,7 +2457,7 @@ and parse_instr Item_t (p, Item_t (Mutez_t _, Item_t (Contract_t (cp, _), rest, _), _), _) -> - check_item_ty p cp loc I_TRANSFER_TOKENS 1 4 >>=? fun Eq -> + check_item_ty ctxt p cp loc I_TRANSFER_TOKENS 1 4 >>=? fun (Eq, ctxt) -> parse_var_annot loc annot >>=? fun annot -> typed ctxt loc Transfer_tokens (Item_t (Operation_t None, rest, annot)) | Prim (loc, I_SET_DELEGATE, [], annot), @@ -2503,12 +2514,12 @@ and parse_instr ctxt ?type_logger (arg_type_full, None) ret_type_full code_field) >>=? fun (Lam ({ bef = Item_t (arg, Empty_t, _) ; aft = Item_t (ret, Empty_t, _) ; _ }, _) as lambda, ctxt) -> - Lwt.return @@ ty_eq ctxt arg arg_type_full >>=? fun Eq -> - Lwt.return @@ merge_types ctxt loc arg arg_type_full >>=? fun _ -> - Lwt.return @@ ty_eq ctxt ret ret_type_full >>=? fun Eq -> - Lwt.return @@ merge_types ctxt loc ret ret_type_full >>=? fun _ -> - Lwt.return @@ ty_eq ctxt storage_type ginit >>=? fun Eq -> - Lwt.return @@ merge_types ctxt loc storage_type ginit >>=? fun _ -> + Lwt.return @@ ty_eq ctxt arg arg_type_full >>=? fun (Eq, ctxt) -> + Lwt.return @@ merge_types ctxt loc arg arg_type_full >>=? fun (_, ctxt) -> + Lwt.return @@ ty_eq ctxt ret ret_type_full >>=? fun (Eq, ctxt) -> + Lwt.return @@ merge_types ctxt loc ret ret_type_full >>=? fun (_, ctxt) -> + Lwt.return @@ ty_eq ctxt storage_type ginit >>=? fun (Eq, ctxt) -> + Lwt.return @@ merge_types ctxt loc storage_type ginit >>=? fun (_, ctxt) -> typed ctxt loc (Create_contract (storage_type, arg_type, lambda)) (Item_t (Operation_t None, Item_t (Address_t None, rest, addr_annot), op_annot)) | Prim (loc, I_NOW, [], annot), @@ -2690,7 +2701,7 @@ and parse_contract Contract.get_script ctxt contract >>=? fun (ctxt, script) -> match script with | None -> Lwt.return - (ty_eq ctxt arg (Unit_t None) >>? fun Eq -> + (ty_eq ctxt arg (Unit_t None) >>? fun (Eq, ctxt) -> let contract : arg typed_contract = (arg, contract) in ok (ctxt, contract)) | Some { code ; _ } -> @@ -2699,8 +2710,8 @@ and parse_contract Gas.consume ctxt cost_code >>? fun ctxt -> parse_toplevel code >>? fun (arg_type, _, _) -> parse_ty ctxt ~allow_big_map:false ~allow_operation:false arg_type >>? fun (Ex_ty targ, ctxt) -> - ty_eq ctxt targ arg >>? fun Eq -> - merge_types ctxt loc targ arg >>? fun arg -> + ty_eq ctxt targ arg >>? fun (Eq, ctxt) -> + merge_types ctxt loc targ arg >>? fun (arg, ctxt) -> let contract : arg typed_contract = (arg, contract) in ok (ctxt, contract)) diff --git a/src/proto_alpha/lib_protocol/src/script_ir_translator.mli b/src/proto_alpha/lib_protocol/src/script_ir_translator.mli index a04657cbb..e221a3774 100644 --- a/src/proto_alpha/lib_protocol/src/script_ir_translator.mli +++ b/src/proto_alpha/lib_protocol/src/script_ir_translator.mli @@ -59,7 +59,7 @@ val big_map_update : val ty_eq : context -> 'ta Script_typed_ir.ty -> 'tb Script_typed_ir.ty -> - ('ta Script_typed_ir.ty, 'tb Script_typed_ir.ty) eq tzresult + (('ta Script_typed_ir.ty, 'tb Script_typed_ir.ty) eq * context) tzresult val parse_data : ?type_logger: type_logger ->