Introducing the [V] Specification Language

In a previous blog post, we looked at how formal verification can be used to prove that a program is free of logical bugs. However, in order to use a formal verification tool, the developer needs to provide a specification describing the intended behavior of the program in a mathematically precise way. In this blog post, we will examine Veridise’s specification language called [V] by illustrating how it can be used to specify various properties over the following simple Wallet contract:

contract Wallet {     
    mapping(address => uint) balances;
    function balanceOf(address addr) public view returns (uint) {
        return balances[addr];
    }
    function deposit() payable external {
        balances[msg.sender] += msg.value;
   }
   function withdraw(uint amt) external {
       require(amt <= balanceOf(msg.sender));
       payable(msg.sender).transfer(amt);
   }
}

[V] Statements

At the core of the [V] specification language are [V] statements, which are building blocks from which all [V] specifications are composed. In a nutshell, [V] statements allow the user to specify properties that should hold when some transaction occurs. For instance, consider the deposit method of the Wallet contract, and suppose that we want to express that calling deposit always successfully completes in state wherein the user’s wallet balance is updated by the amount deposited. This can be expressed using the following [V] statement:

finished(Wallet.deposit(), this.balanceOf(sender) =
         old(this.balanceOf(sender)) + value)

This statement is of the form finished(transaction, property) expressing that transaction should always finish successfully (without reverting) in a state satisfying property. Hence, the [V] statement shown above specifies two important pieces of information:

1. Invoking Wallet.deposit() should never result in an exception
2. When the execution of Wallet.deposit() terminates, the balance of the user (i.e., sender) should increase by the amount sent (i.e., value).

Here, note that the construct old(t) refers to the value of t before the transaction started, and any integers used in the specification are assumed to be mathematical integers (i.e., no overflows).

As another example, suppose that we want to express that a wallet should not allow withdrawing more money than the user possesses. This property can be expressed using the following [V] statement:

reverted(Wallet.withdraw(amt), amt > this.balanceOf(sender))

This specification uses another predicate called reverted of the form reverted(transaction, property) expressing that transaction should revert when it is invoked in a state satisfying property. Hence, it expresses that withdrawing amt results in a failed a transaction when the balance of the message’s sender is less than the amount specified.

More generally, all [V] statements have the following shape:

predicate ( transaction, property )

where:

• predicate constrains the outcome of a transaction’s execution on the blockchain. The three most common predicates used in [V] are started, finished, and reverted.
• transaction is an expression of the form contract.methodName(arguments) describing the invocation of some contact method.
• property is a boolean expression which can refer to the method arguments, contract variables, contract functions, implicit blockchain variables and [V] built-ins. Some of the most common built-ins are old(t) and sum(t), where old(t) returns the value of t evaluated at the beginning of the transaction and sum(t) returns the sum of all values stored in the collection t.

Contract Invariants

In many cases, we wish to express that some property should hold before and after every transaction. We refer to such properties as contract invariants. Intuitively, a contract invariant expresses that a property should hold before and after every execution of every contract method.

For instance, a key property of the wallet contract above is that the contract’s balance should be equal to the sum of all balances across the different accounts. This property can be expressed using the following contract invariant in [V]:

inv: started(Wallet.*, balance(this) = sum(this.balances))

where * matches any method of the contract. Such an annotation tells the verifier to check that the contract invariant is obeyed throughout the contract’s execution.

Method Contracts

In addition to specifying contract invariants, we also often wish to express individual properties of each method. Such properties are captured using method contracts of the form Pre |=> Post, where Pre is a property that should hold when the method is called and Post is property that should hold after the method is done executing. For instance, going back to our Wallet example, we would naturally expect that after a successful execution of the withdraw method, the balance of the user should be reduced by the amount withdrawn. This property can be expressed using the following method contract in [V]:

spec: finished(Wallet.withdraw(amt), this.balanceOf(sender) >= amt
               |=> balance(this) = old(balance(this)) - amt)

This method contract states that if a user requests to withdraw amt ETH and balanceOf(msg.sender) is at least the amount of ETH to withdraw, then the transaction should not revert and the contract’s ETH balance should be reduced by the amount withdrawn. Note that the second argument of finished uses the Pre |=> Post construct where Pre specifies the pre-condition for withdraw to finish successfully, and Post specifies the condition that should hold upon successful termination of withdraw. Given such a contract, the verifier needs to check two conditions:

1. The withdraw method never reverts if the specified pre-conditions holds;
2. Under the assumption that the pre-condition is satisfied, withdraw terminates in a state satisfying the post-condition.

Behavioral Specifications

In addition to specifying properties of individual methods, we might also be interested in specifying how different methods of the same contract interact with each other. One can also express such more complicated specifications in the [V] language.

To illustrate such specifications, suppose that we wish to express that a Wallet’s withdraw function is the inverse of deposit. That is, if a user is able to successfully deposit some amount of ETH, they should then be able to successfully withdraw the same amount to undo the changes made by the deposit function. This can be expressed using the following [V] specification:

vars: Wallet wallet, uint ethBal, address u, uint uBal, uint a 
spec: finished(wallet.deposit(), value = a && u = sender && 
          ethBal = old(balance(this)) && 
          uBal = old(this.balanceOf(u)));
      finished(wallet.withdraw(amt), amt = a && u = sender              
          |=> ethBal = balance(this) && uBal = this.balanceOf(u))

Here ; refers to the sequence operator. In particular, the expression

predicate1( transaction1, property1 ) ; 
predicate2 ( transaction2, property2 )

has the following semantics: “In an execution where transaction2 is followed by transaction 1, both properties should hold”. Thus, the Wallet specification above expresses that depositing some amount amt and then withdrawing the same amount should end in a state where there is no overall change to the balance. Note that the variables ethBal, u, uBal and a used in this specification allow us to relate values across different transactions.

Now that we know how to relate transactions to each other, let’s also look at how to express properties over a set of accounts. As an example, consider the following [V] specification that expresses that users should only be able to withdraw their own funds:

vars: Wallet wallet, address u1, address u2, uint a 
init: finished(wallet.constructor()) ;
      finished(wallet.deposit(), sender = u1 && value = a) ;
      finished(wallet.deposit(), sender = u2 && u2 != u1) 
spec: reverted(wallet.withdraw(amt), sender = u1 && amt > a)

Such a specification is best thought of as a “symbolic unit test” where the “init” part of the specification sets up some desired blockchain state and the “spec” part asserts properties that should in that state. Specifically, this specification declares a Waller wallet and two users u1 and u2 of this wallet. The initialization phase considers a use case of the wallet where u1 deposits amount a followed by an (unknown) deposit by a different user u2. The specification asserts that, under such a use case of the contract, u1 should not be able to withdraw an amount larger than a. Such a specification is akin to a test case except that the users and deposit/withdraw amounts are symbolic. Hence, checking such a specification is like testing all possible instantiations of the deposit/withdraw amounts that satisfy the given constraint.

Looking Ahead

All of the specifications we looked at so far are instances of safety properties that express that something bad will never happen (i.e., an undesired state will not be reached). In some cases, we might also wish to express that something good will eventually happen. For example, as a participant of an auction, we might wish to express that I will eventually get my bid back if I am not the winner of the auction. Such a property is an example of a liveness property and can be expressed in [V] using temporal operators. We will leave the discussion of such temporal specifications to another blog post in our series.

Summary

[V] is a powerful specification language that provides users with many tools to express the properties they care about. It does so by allowing users to express many types of specifications, including method contracts, behavioral specifications and temporal specifications. All of these specifications make use of a common component, the [V] statement, allowing users to easily express new types of specifications without requiring much additional knowledge. [V] statements are declarative and allow users to concisely express properties of and relationships between transactions. For more information about [V], please see our documentation.