Special annotations can lead to invalid field annotations

Environment (Mainnet, test network, build from source, ...)

• https://testnet-tezos.giganode.io

Summary

When PAIR is used with the special annotation %@, it will take the variable annotations of both values and, if they have a dot ., they will be split.

E.g. if the two values are annotated with @p.a and @p.b, these annotations will be split into @p, %a and %b.

/* [ @p.a int : @p.b int ] */ ;
PAIR %@ %@
/* [ @p pair (int %a @p.a) (int %a @p.b) ] */ ;

However, if one of the values is annotated with, say, @p.@@@@ (which is a valid var annotation), PAIR %@ will split it into @p and %@@@@.

According to the docs, %@@@@ is not a valid annotation, because it does not match the regex @%|@%%|%@|[@:%][_0-9a-zA-Z][_0-9a-zA-Z\.%@]*.

Expected behavior

Expected the typechecker to fail.

Actual behavior

The typechecker succeeds, and creates an invalid annotation.

Steps to reproduce

split_anns.tz

parameter unit;
storage   unit;

code {
      DROP;

      PUSH @p.@@@@ int 1;
      PUSH @p.a int 2;
      PAIR %@ %@;

      DROP; UNIT; NIL operation; PAIR 2;
     };

$ tezos-client -E https://testnet-tezos.giganode.io typecheck script split_anns.tz -v

Well typed
Gas remaining: 1039992.050 units remaining
{ parameter unit ;
  storage unit ;
  code { /* [ pair (unit @parameter) (unit @storage) ] */
         DROP
         /* [] */ ;
         PUSH @p.@@@@ int 1
         /* [ @p.@@@@ int ] */ ;
         PUSH @p.a int 2
         /* [ @p.a int : @p.@@@@ int ] */ ;
         PAIR %@ %@
         /* [ @p pair (int %a @p.a) (int %@@@@ @p.@@@@) ] */ ;
         DROP
         /* [] */ ;
         UNIT
         /* [ unit ] */ ;
         NIL operation
         /* [ list operation : unit ] */ ;
         PAIR 2
         /* [ pair (list operation) unit ] */ } }