Symbolic Identity Unit Test Michelson

identity-symbolic.tzt

// Symbolic Unit Test for Identity Function
// lines 3 and 24 represent our input and expected output stack respectively
input { Stack_elt nat $N } ;
code { DUP ;
       PUSH nat 0 ;
       SWAP ;
       INT ;
       GT ;
       // Loop assigned name @I
       LOOP @I {
           PUSH nat 1 ;
           ADD ;
           DUP ;
           DIG 2 ;
           DUP ;
           DUG 3 ;
           SWAP ;
           COMPARE ;
           LT
       } ;
       DIP { DROP }
} ;
// Output stack is an arbitrary number $N_OUT which must equal $N by line 25
output { Stack_elt nat $N_OUT } ;
postcondition { { PUSH nat $N_OUT ; PUSH nat $N ; COMPARE ; EQ } } ;
// invariant composed of:
// Line  30:    Stack shape
// Lines 31-32: Predicate blocks --- blocks of Michelson that take an empty
//              stack must return a stack of the form Stack_elt bool $B
invariant @I { Stack_elt bool $GUARD ; Stack_elt nat $C ; Stack_elt nat $N 
               { { PUSH nat $N ; PUSH nat $C ; COMPARE ; LE }
               ; { PUSH nat $N ; PUSH nat $C ; COMPARE ; LT ; PUSH bool $GUARD ; COMPARE ; EQ }
             }