balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Alpha: consume typechecking gas in type equality for expansion

Browse Source
This commit is contained in:
Alain Mebsout 2018-06-28 16:58:29 +02:00 committed by Benjamin Canou
parent 589bb54abe
commit b1515dc376
3 changed files with 223 additions and 212 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/bin_client/test/test_contracts.sh
View File

@ -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'

431
src/proto_alpha/lib_protocol/src/script_ir_translator.ml
View File

@ -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))

2
src/proto_alpha/lib_protocol/src/script_ir_translator.mli
View File

@ -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 ->