Michelson: check (field) annotations of field accesses

src/bin_client/test/contracts/and.tz

@@ -1,3 +1,3 @@
 parameter (pair :param (bool %first) (bool %second));
 storage (option bool);
-code { CAR ; UNPAIR; AND @and; SOME @res; NIL @noop operation; PAIR };
+code { CAR ; UNPAIR; AND @and; SOME @res; NIL @noop operation; PAIR; UNPAIR @x @y; PAIR %a %b };

src/bin_client/test/contracts/weather_insurance.tz

@@ -1,18 +1,18 @@
-# (pair signed_weather_data actual_level)
+parameter (pair (signature %signed_weather_data) (nat :rain %actual_level));
-parameter (pair (signature @sig) (nat @nat));
 # (pair (under_key over_key) (pair weather_service_key (pair rain_level days_in_future)))
-storage (pair (pair (contract @lt unit)
+storage (pair (pair (contract %under_key unit)
-                    (contract @geq unit))
+                    (contract %over_key unit))
-              (pair nat key));
+              (pair (nat :rain %rain_level) (key %weather_service_key)));
 code { DUP; DUP;
        CAR; MAP_CDR{H};
-       SWAP; CDDDR; DIP {UNPAIR} ; CHECK_SIGNATURE; # Check if the data has been correctly signed
+       SWAP; CDDDR %weather_service_key;
+       DIP {UNPAIR} ; CHECK_SIGNATURE @sigok; # Check if the data has been correctly signed
        ASSERT; # If signature is not correct, end the execution
-       DUP; DUP; DUP; DIIIP{CDR}; # Place storage type on bottom of stack
+       DUP; DUP; DUP; DIIIP{CDR %storage}; # Place storage type on bottom of stack
        DIIP{CDAR};                # Place contracts below numbers
-       DIP{CADR};                # Get actual rain
+       DIP{CADR %actual_level};   # Get actual rain
-       CDDAR;                     # Get rain threshold
+       CDDAR %rain_level;         # Get rain threshold
-       CMPLT; IF {CAR @winner} {CDR @winner};     # Select contract to receive tokens
+       CMPLT; IF {CAR %under_key} {CDR %over_key};     # Select contract to receive tokens
-       BALANCE; UNIT ; TRANSFER_TOKENS; # Setup and execute transfer
+       BALANCE; UNIT ; TRANSFER_TOKENS @trans_op; # Setup and execute transfer
        NIL operation ; SWAP ; CONS ;
        PAIR };

src/proto_alpha/lib_client/michelson_v1_error_reporter.ml

@@ -368,6 +368,13 @@ let report_errors ~details ~show_source ?parsed ppf errs =
                  - @[<v>%s@]@]"
                 annot1
                 annot2
+          | Inconsistent_field_annotations (annot1, annot2) ->
+              Format.fprintf ppf
+                "@[<v 2>The field access annotation does not match:@,\
+                 - @[<v>%s@]@,\
+                 - @[<v>%s@]@]"
+                annot1
+                annot2
           | Inconsistent_type_annotations (loc, ty1, ty2) ->
               Format.fprintf ppf
                 "@[<v 2>%athe two types contain incompatible annotations:@,\

src/proto_alpha/lib_protocol/src/script_ir_translator.ml

@@ -1009,7 +1009,6 @@ let parse_field_annot
     | [ `Field_annot _ as a ] -> ok (Some a)
     | _ -> error (Unexpected_annotation loc) (* (Invalid_var_annotation (loc, annot)) *)
 
-
 let extract_field_annot
   : Script.node -> (Script.node * field_annot option) tzresult
   = function
@@ -1024,6 +1023,14 @@ let extract_field_annot
         Prim (loc, prim, args, annot), field_annot
     | expr -> ok (expr, None)
 
+let check_correct_field
+  : field_annot option -> field_annot option -> unit tzresult
+  = fun f1 f2 ->
+    match f1, f2 with
+    | None, _ | _, None -> ok ()
+    | Some `Field_annot s1, Some `Field_annot s2 ->
+        if String.equal s1 s2 then ok ()
+        else error (Inconsistent_field_annotations ("%" ^ s1, "%" ^ s2))
 
 let rec parse_comparable_ty
   : Script.node -> ex_comparable_ty tzresult
@@ -1773,14 +1780,16 @@ and parse_instr
         typed ctxt loc Cons_pair
           (Item_t (Pair_t((a, l_field), (b, r_field), ty_name), rest, annot))
     | Prim (loc, I_CAR, [], annot),
-      Item_t (Pair_t ((a, field_annot), _, _), rest, pair_annot) ->
+      Item_t (Pair_t ((a, expected_field_annot), _, _), rest, pair_annot) ->
-        parse_var_annot loc annot ~default:(access_annot pair_annot field_annot)
+        parse_var_field_annot loc annot >>=? fun (annot, field_annot) ->
-        >>=? fun annot ->
+        let annot = default_annot annot ~default:(access_annot pair_annot expected_field_annot) in
+        Lwt.return (check_correct_field field_annot expected_field_annot) >>=? fun () ->
         typed ctxt loc Car (Item_t (a, rest, annot))
     | Prim (loc, I_CDR, [], annot),
-      Item_t (Pair_t (_, (b, field_annot), _), rest, pair_annot) ->
+      Item_t (Pair_t (_, (b, expected_field_annot), _), rest, pair_annot) ->
-        parse_var_annot loc annot ~default:(access_annot pair_annot field_annot)
+        parse_var_field_annot loc annot >>=? fun (annot, field_annot) ->
-        >>=? fun annot ->
+        let annot = default_annot annot ~default:(access_annot pair_annot expected_field_annot) in
+        Lwt.return (check_correct_field field_annot expected_field_annot) >>=? fun () ->
         typed ctxt loc Cdr (Item_t (b, rest, annot))
     (* unions *)
     | Prim (loc, I_LEFT, [ tr ], annot),

src/proto_alpha/lib_protocol/src/script_tc_errors.ml

@@ -43,6 +43,7 @@ type error += Inconsistent_annotations of string * string
 type error += Inconsistent_type_annotations : Script.location * _ ty * _ ty -> error
 type error += Invalid_type_annotation : Script.location * annot list -> error
 type error += Invalid_var_annotation : Script.location * annot list -> error
+type error += Inconsistent_field_annotations of string * string
 type error += Unexpected_annotation of Script.location
 type error += Invalid_map_body : Script.location * _ stack_ty -> error
 type error += Invalid_map_block_fail of Script.location

src/proto_alpha/lib_protocol/src/script_tc_errors_registration.ml

@@ -335,6 +335,18 @@ let () =
     (function Inconsistent_annotations (annot1, annot2) -> Some (annot1, annot2)
             | _ -> None)
     (fun (annot1, annot2) -> Inconsistent_annotations (annot1, annot2)) ;
+  (* Inconsistent field annotations *)
+  register_error_kind
+    `Permanent
+    ~id:"inconsistentFieldAnnotations"
+    ~title:"Annotations for field accesses is inconsistent"
+    ~description:"The specified field does not match the field annotation in the type"
+    (obj2
+       (req "annot1" string)
+       (req "annot2" string))
+    (function Inconsistent_field_annotations (annot1, annot2) -> Some (annot1, annot2)
+            | _ -> None)
+    (fun (annot1, annot2) -> Inconsistent_field_annotations (annot1, annot2)) ;
   (* Inconsistent type annotations *)
   register_error_kind
     `Permanent