2

TL;DR looks like 1 bug in spec and one more in type checker for alphanet.

Someone please review and comment on this behavior :)

parameter unit;
storage string;
code { DROP;
       PUSH int 3;
       PUSH (option int) None;
       IF_NONE { DROP;
                 PUSH @x (string :tagX) "bt1";
                 PUSH @y string"bt2";
                 PUSH @z (string :tagZ) "bt3";
               }
               { DROP;
                 DROP;
                 PUSH string "bf1";
                 PUSH (string :tagY) "bf2";
                 PUSH string "bf3";
               };
       PUSH @after_if (string :newTag) "after_if";
       CONCAT;
       DROP; DROP; DROP;
       PUSH string "Hello Tezos!";
       NIL operation;
       PAIR;
      };

On alphanet this script type checks well.

There are two problems with it:

Problem one (potential bug in spec)

   iff   bt :: [ 'S -> 'b : 'S]
         bf :: [ 'a : 'S -> 'b : 'S]

according to spec, but code in the sample behaves differently: IF_NONE :: option 'a : [ int : (pair unit string) ] -> 'b : [ string : string : string : (pair unit string) ]

So perhaps there's a bug in spec and IF_NONE :: option 'a : 'X -> 'b : 'Y (which is OK)

Problem two (potential bug in type checker)

If you follow type annotations, it will be evident that different branches of if pushed string :tagX : string : string :tagZ while other pushed string : string :tagY : string .

But surprisingly in the output of type checker we see /* [ @after_if string :newTag : string : string : string ] */ which is well .. strange. Looks like a bug in type checker that it accidentally erases type annotations when they differ for various branches of if (or maybe just for branches of if disregard to one other).


Dump of type checker for the sample:

Well typed
Gas remaining: 399177 units remaining
{ parameter unit ;
  storage string ;
  code { /* [ pair (unit @parameter) (string @storage) ] */
         DROP
         /* [] */ ;
         PUSH int 3
         /* [ int ] */ ;
         PUSH (option int) None
         /* [ option int : int ] */ ;
         IF_NONE
           { /* [ int ] */
             DROP
             /* [] */ ;
             PUSH @x (string :tagX) "bt1"
             /* [ @x string :tagX ] */ ;
             PUSH @y string "bt2"
             /* [ @y string : @x string :tagX ] */ ;
             PUSH @z (string :tagZ) "bt3"
             /* [ @z string :tagZ : @y string : @x string :tagX ] */ }
           { /* [ int : int ] */
             DROP
             /* [ int ] */ ;
             DROP
             /* [] */ ;
             PUSH string "bf1"
             /* [ string ] */ ;
             PUSH (string :tagY) "bf2"
             /* [ string :tagY : string ] */ ;
             PUSH string "bf3"
             /* [ string : string :tagY : string ] */ } ;
         PUSH @after_if
           (string :newTag)
           "after_if"
         /* [ @after_if string :newTag : string : string : string ] */ ;
         CONCAT
         /* [ string : string : string ] */ ;
         DROP
         /* [ string : string ] */ ;
         DROP
         /* [ string ] */ ;
         DROP
         /* [] */ ;
         PUSH string "Hello Tezos!"
         /* [ string ] */ ;
         NIL operation
         /* [ list operation : string ] */ ;
         PAIR
         /* [ pair (list operation) string ] */ } }
1
  • Bug reports are better filed using the ticket system on Gitlab. StackExchange is for questions
    – Arthur B
    Feb 8 '19 at 8:24
2

Created: https://gitlab.com/tezos/tezos/issues/471

This ticket will be closed.

Not the answer you're looking for? Browse other questions tagged or ask your own question.