Why3: State-based Development

A deductive verification tool like Why3 can be used to check the behavior of a collection of functions working on a shared state, such as classes in object-oriented programming (sharing instance variables), smart contracts in blockchain development, or multi-threaded concurrent programming (based on shared memory).

We will illustrate this by means of an example where we model functions operating on a bank account.

The global shared state stores the balance of each account, identified by a number.

module Accounts_MapImp
  use int.Int
  type accNumber = int 
  type amount    = int

  val open (n :accNumber) : ()
  val deposit (n :accNumber) (x :amount) : () 
  val withdraw (n :accNumber) (x :amount) : () 
  val transfer (from :accNumber) (to_ :accNumber) (x :amount) : () 

We need a way to associate balances with account numbers. We will use a Why3 finite map (or dictionary) type for this purpose. The Why3 library https://why3.lri.fr/stdlib/fmap.html makes available different logic and programming types for finite maps.

We will use a programming type of imperative maps. The read, write, and key membership functions on this type are specified in the library with the following prototypes:

  val find (k: key) (m: t 'v) : 'v

  val add  (k: key) (v: 'v) (m: t 'v) : unit

  val mem (k: key) (m: t 'v) : bool

Programming types are used by cloning the respective module into our own. In this concrete case we will instantiate the type of the map keys:

  clone fmap.MapImp with type key = accNumber
  type mapAccAmount = t amount 

The type of maps with accNumber as keys is available with name t; we then define mapAccAmount as the concrete type of maps from accNumber to amount. The following declares the state variable accounts as such a map:

  val accounts : mapAccAmount

We wish to write functions to do the following tasks:

• open a new account with a given account number
• deposit funds into a given account
• withdraw funds from an account
• transfer funds internally from an account to another

As a first step let us consider a natural language specification of their behavior. For instance:

• given an account number n , the call open n will insert the pair (n →0) in the accounts dictionary

• given an account number n and an amount x, the call deposit n x will add x to the current balance of account n

• . . .

Preconditions and Implementation

An important step is to discuss what the functions should do in case they receive unexpected argument values. What should happen if

• in a call open n, the account number n already exists, i.e. it is already present in the domain of accounts ?

• in a call deposit n x,

  • the number n is not a valid account number (i.e. it is not in the domain of accounts,
  • or x is a negative number ?

We will choose not to program defensively : the functions will take for granted, without checking, that unsafe calls do not occur.

In the absence of defensive programming it is the caller’s responsibility to make sure that all calls satisfy the desired conditions, which should be included in the contracts of the callee functions as preconditions.

The four desired functions can be promptly written, including preconditions, as follows, using the dictionary functions add and find :

  let open (n :accNumber) : ()
    requires { not mem n accounts }
  = add n 0 accounts

  let deposit (n :accNumber) (x :amount) : () 
    requires { mem n accounts /\ x > 0 }
  = let bal = find n accounts in 
    add n (bal+x) accounts 

  let withdraw (n :accNumber) (x :amount) : () 
    requires { mem n accounts /\ 0 < x <= accounts n }
  = let bal = find n accounts in 
    add n (bal-x) accounts 
 
  let transfer (from :accNumber) (to_ :accNumber) (x :amount) : () 
    requires { mem from accounts /\ mem to_ accounts }
    requires { from <> to_ }
    requires { 0 < x <= accounts from }
  = let balfrom = find from accounts in 
    let balto   = find to_  accounts in 
    add to_  (balto  +x) accounts ;
    add from (balfrom-x) accounts 

Why3 generates verification conditions for find operations, to guarantee that the keys being read are actually in the domain of the dictionary (finite map). The preconditions ensure that they actually are, so all VCs are proved valid.

State Invariants

[permalink]

We may wish to prove that certain properties of the global state always hold, i.e. they are invariants of all the state-changing functions.

For instance:

The balance of every account is non-negative

This can be written as a predicate on maps (from accounts to amounts) as follows:

  predicate inv (accs : mapAccAmount) = 
    forall a :accNumber. mem a accs -> accs a >= 0 

Such properties may be treated by simply including them simultaneously as pre- and postconditions in all functions:

    requires { inv accounts }   
    ensures  { inv accounts }

The set of verification conditions for the resulting module (permalink) now contains additional VCs, ensuring that the invariant is preserved by every function.

Postconditions and “Complete” Specs

[permalink]

The specifications in the previous module contain safety preconditions, and can be see as adequate for reasoning about the state invariant described above. However, they are not sufficient for reasoning about programs using the functions, such as:

  let main ()
    requires { accounts = empty }
    ensures  { accounts 3333 = 200 }
  = open 1111 ;
    open 2222 ;
    open 3333 ;
    deposit 1111 100 ; 
    deposit 2222 100 ; 
    transfer 1111 3333 100 ;
    transfer 2222 3333 100 

The reason for this is that the code of the functions is not visible at the logic level, so there is no way to establish the postcondition of the main function.

Moreover, each of the above function calls will generate safety VCs regarding the presence of the different account numbers in the dictionary, and for the same reason these cannot be proved.

The way to solve this problem is to write more complete specifications for the functions, including postconditions describing exactly what the functions do, in particular:

• which account numbers are in the dictionary after a call to the function;
• and what the balance of each account is

For instance a complete spec for open can be given as follows:

  let open (n :accNumber) : ()
    requires { not mem n accounts }
    ensures  { forall a:accNumber. mem a accounts <-> mem a (old accounts) \/ a = n}
    ensures  { accounts n = 0 }
    ensures  { forall a :accNumber. mem a accounts /\ a <> n -> 
                 accounts a = old accounts a }     
  = add n 0 accounts

Note that:

• The first postcondition relates the keysets (domains) of the mapping before and after execution of each function
• The second postcondition specifies the balance of account n
• The third one expresses an obvious fact that is implicit in the natural language spec, but must be stated explicitly in the contract: with the exception of account n, all balances are preserved

The complete module [permalink] , including the above main function, can be entirely proved with TryWhy3.

Record types and type invariants

[permalink]

Why3 provides a more convenient way to verify state invariants such as the inv predicate given above. It suffices to encapsulate the state variable(s) inside a record type, and attach a type invariant to it:

module Accounts_MapImp_Record
  use int.Int
  type accNumber = int 
  type amount    = int
  clone fmap.MapImp with type key = accNumber

  type state = { mutable bal: t amount }
    invariant  { forall a :accNumber. mem a bal -> find a bal >= 0 }
    by { bal = create() }

  val accounts :state

Declaring the state using a record type allows us to include the state invariant directly in the type definition. Verification conditions will be automatically created for all state-changing functions, ensuring the preservation of the type invariant.

Note that:

• The by clause is mandatory. Its role is to provide a witness satisfying the type invariant. We simply provide the empty mapping as example (it is returned by the create function)
• Record fields are by default immutable (as in functional programming). Mutable fields must be explicitly identified as above

Both in the code and the spec, the balance value will have to be referred using record field notation, for instance:

  let open (n :accNumber) : ()
    requires { not mem n accounts.bal }
    ensures  { forall a:accNumber. mem a accounts.bal <-> 
                  mem a (old accounts.bal) \/ a = n } 
    ensures  { accounts.bal n = 0 }
    ensures  { forall a :accNumber. mem a accounts.bal /\ a <> n -> 
                 accounts.bal a = old accounts.bal a }    
  = add n 0 accounts.bal 

The complete module [permalink] can be fully verified using Try Why3.