Skip to main content

Examples

Boomerang#

# boomerang.tzparameter unit;storage unit;<< ContractAnnot   { (_, _) | True } ->   { (ops, _) | amount = 0 && ops = [] ||      amount <> 0  && (match contract_opt source with                         | Some c -> ops = [ TransferTokens Unit amount c ]                         | None -> False) } &   { _ | False } >>code  {    CDR;    NIL operation;    AMOUNT;    PUSH mutez 0;    IFCMPEQ      {      }      {        SOURCE;        CONTRACT unit;        ASSERT_SOME;        AMOUNT;        UNIT;        TRANSFER_TOKENS;        CONS;      };    PAIR;  }

The code above, which is the contents of boomerang.tz, is a Michelson program that transfers back all money recieved to the source account. The program comes with a mandatory annotation ContractAnnot surrounded by << and >>. This annotation gives the specification of contract to be verified. In the code, it states the following two properties.

  • The pair (ops, _), which is in the stack at the end of the program, satisfies ops = [TransferTokens Unit balance c] where c bound for the contract object pointed to by source; this operation means that this contract will send money amount balance to addr with argument Unit after this contract finishes.
  • No exceptions are raised from the instructions in this program; this is expressed by the part ... & { _ | False }. There is an ASSERT_SOME instruction in the program that may raise an exception when the stack top is None. Because of Michlson specification, the account pointed to by source should be a human-operated account, the CONTRACT unit should always return Some, so no exception will be raised.

If you verify this program, you will get VERIFIED.

Checksig#

# checksig.tzparameter (pair signature string);storage (pair address key);<< ContractAnnot  { ((sign, data), (addr, pubkey)) |     match contract_opt addr with     Some (Contract<string> _) -> True | _ -> False } ->  { ([op], new_store) |     (addr, pubkey) = new_store &&     sig pubkey sign (pack data) &&     match contract_opt addr with     | Some c -> op = Transfer data 1 c     | None -> False }  & { _ | not (sig pubkey sign (pack data)) } >>code  {    DUP; DUP; DUP;    DIP { CAR; UNPAIR; DIP { PACK } }; CDDR;    CHECK_SIGNATURE; ASSERT;
    UNPAIR; CDR; SWAP; CAR;    CONTRACT string; ASSERT_SOME; SWAP;    PUSH mutez 1; SWAP;    TRANSFER_TOKENS;
    NIL operation; SWAP;    CONS; DIP { CDR };    PAIR;  }

This program

  1. checks the signature, the first element of the parameter, is valid one of the string, the second element of the parameter, signed by the private key corresponding to the stored public key; and then, if valid,
  2. transfers the string to the contract pointed to by the stored address with 1 mutez.

This behavior is described in the post- and ab-postcondition parts of ContractAnnot. The postcondition describes a condition when the contract normally terminated, that is:

  • the storage does not change;
  • signature verification has succeeded; and
  • the operation issued is an intended one.

The ab-postcondition describes a condition when the contract abnormally terminated, that is:

  • if the contract raises an exception, it is always the case that signature verification has failed.

Furthermore, precondition specifies the assumption for the stored address that is the address is valid one as a transfer destination. Without the assumption, ASSERT_SOME instruction in the code will raise an exception even if signature verification has succeeded; and as a result, verification of the ab-postcondition fails.

Sumseq#

# sumseq.tzparameter (list int);storage int;<< Measure sumseq : (list int) -> int where Nil = 0 | Cons h t = (h + (sumseq t)) >><< ContractAnnot { (l, _) | True } ->  { ret | sumseq l = second ret } &  { exc | False } (l' : list int) >>code  {    CAR;    << Assume { x | x = l' } >>    DIP { PUSH int 0 };    << LoopInv { r:s | l = l' && s + sumseq r = sumseq l' } >>    ITER { ADD };    NIL operation;    PAIR;  }

This contract computes the sum of the integers in the list passed as a parameter. The ContractAnnot annotation uses the function sumseq, which is defined in the earlier Measure annotation. In the code section, the Assume annotation is used to specify that l', which is declared to be a ghost variable in the ContractAnnot, is the list passed as a parameter. LoopInv gives the loop-invariant for ITER. ITER { ADD } is an instruction that adds the head of the list to the second s from the top of the stack. The loop-invariant condition s + sumseq r = sumseq l' expresses that adding s to the sum of list r in process equals the sum of the list l'. The obvious invariant l = l' compensate the relation between l and l'. Without it, what we can know after the loop is s = sumseq l', which is not s = sumseq l that we want.

Actually, the annotations in the code is redundant because we want to show a use case of an Assume annotation. We can give more straightforward annotations to verify the same specification as follows.

# sumseq.tzparameter (list int);storage int;<< Measure sumseq : (list int) -> int where Nil = 0 | Cons h t = (h + (sumseq t)) >><< ContractAnnot { (l, _) | True } ->  { ret | sumseq l = second ret } &  { exc | False } >>code  {    CAR;    DIP { PUSH int 0 };    << LoopInv { r:s | s + sumseq r = sumseq l } >>    ITER { ADD };    NIL operation;    PAIR;  }

MapIncr#

parameter (list int);storage (list int);<< Measure add_one : list int -> list int where [] = [] | h :: t = (1 + h) :: add_one t >><< ContractAnnot  { (p, _) | True } ->  { (_, p') | p' = add_one p } &  { _ | False } >>code  {    CAR;    << MapInv (res : list int) { l | res @ add_one l = add_one p } >>    MAP      {        PUSH int 1;        ADD;      };    NIL operation;    PAIR;  }

This example shows verification involving the MAP instruction. The code just stores the list consisting of increment elements of the given list. The increment relation is described by using the add_one measure function, which should be straightforward.

The new point is that MAP demands MapInv annotation which is a variant of LoopInv instruction but can use an additional variable bound for processed list's elements. In the example res is the additional variable. So you can imagine that at the start of every iteration, the invariant res @ add_one l = add_one p holds. After the invariant checking, it reveals that the stack just after the MAP instruction satisfies the condition { res | res @ add_one l = add_one p && l = []}, from which Helmholtz can deduce the postcondition of the contract specification.