Why3: State-based Development

A deductive verification tool like Why3 can be used to check the behavior of a collection of functions working on some notion of 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 inspired by the Trash software concept. The state will consist of two lists containing respectively erased items (the trash) and accessible items that can be erased.

Mutable Variables

We start by creating a module where we import some list library modules and declare a new type item. We also declare an equality predicate to be used for this type in program functions. Note that:

the postcondition of (=) establishes the correspondence between this program predicate and the notion of logical equality;
the idea is that equality will be defined for this type when it is instantiated later (if this module is cloned).

module Trash_Refs use list.List use list.Mem
```
type item
val (=) (x y : item) : bool
  ensures { result <-> x = y }

val ref accessible : list item 
val ref trashed : list item 
```

The module also contains two references accessible and trashed. These are mutable variables where the state of our module is kept.

The create function adds a new item to the list of accessible items. Note the use of the <- assignment operator used with references:

  let create (i : item) 
    requires { not mem i accessible /\ not mem i trashed }
    ensures  { accessible = Cons i (old accessible) }
    ensures  { trashed = old trashed }
  =
    accessible <- Cons i accessible 

The postconditions are trivial enough, but they should still be included to enable reasoning about calls to this function.

The next two functions allow for items to erased or recovered from the trash:

  (* helper function *)
  val function deleteAll (x: item) (l:list item) : list item =
    ensures { forall i :item. mem i result <-> mem i l /\ i<>x } 

  let delete (i : item)
    requires { mem i accessible }
    ensures  { accessible = deleteAll i (old accessible) }
    ensures  { trashed = Cons i (old trashed) }
  =
    accessible <- deleteAll i accessible ;
    trashed <- Cons i trashed  

  let restore (i : item)
    requires { mem i trashed }
    ensures  { accessible = Cons i (old accessible) }
    ensures  { trashed = deleteAll i (old trashed) }
  =
    trashed <- deleteAll i trashed ;
    accessible <- Cons i accessible 

Note the use of a helper function for deletion in lists. It is declared with a contract; this is sufficient to enable reasoning about calls to it.

The last function empties the trash:

  let empty ()
    requires { not is_nil trashed }
    ensures  { accessible = old accessible }
    ensures  { trashed = Nil }
  =
    trashed <- Nil ;

We can express and prove state invariants of this implementation by including them as preconditions and postconditions in every function.

For instance, an invariant property of this implementation is the fact no item can be simultaneously included in the accessible and trash lists:

  predicate noCommon (l1 l2 :list item) =
       forall x :item. not (mem x l1 /\ mem x l2) 

  let delete (i : item)
    requires { mem i accessible }
    requires { noCommon accessible trashed }
    ensures  { accessible = deleteAll i (old accessible) }
    ensures  { trashed = Cons i (old trashed) }
    ensures  { noCommon accessible trashed }
  =
    accessible <- deleteAll i accessible ;
    trashed <- Cons i trashed  

(repeated for every other function)

[permalink]

Records and Type Invariants

Alternatively we can include both state variables as fields of a record type. This will have the advantage of allowing us to include the state invariant as a record type invariant, thus eliminating the need to include it as pre- and post-condition in every function:

module Trash_Record
  use list.List  use list.Mem

  type item 
  val (=) (x y : item) : bool    ensures { result <-> x = y }

  type stateT = { mutable accessible : list item ;
                  mutable trashed    : list item }

    invariant  { forall x :item. not (mem x accessible /\ mem x trashed) }

    by { accessible = Nil ; trashed = Nil }

  val state : stateT

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:

Record fields are by default immutable (as in functional programming). Mutable fields must be explicitly identified, as above.
The role of the by clause is to provide a witness satisfying the type invariant, thus showing that we are not creating an inconsistency by attaching the invariant to the type. The state consisting of two empty lists trivially satisfies the invariant.

Both in the code and in contracts, the balance value will subsequently have to be referred using record field notation.

The first two functions will now be written as follows:

  let create (i : item) 
    requires { not mem i state.accessible /\ not mem i state.trashed }
    ensures  { state.accessible = Cons i (old state.accessible) }
    ensures  { state.trashed = old state.trashed }
  =
    state.accessible <- Cons i state.accessible 

  let delete (i : item)
    requires { mem i state.accessible }
    ensures  { state.accessible = deleteAll i (old state.accessible) }
    ensures  { state.trashed = Cons i (old state.trashed) }
  =
    state.accessible <- deleteAll i state.accessible ;
    state.trashed <- Cons i state.trashed 

[permalink]

A Second Example, Using Maps

As a second example we will now model a basic bank account system.

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

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

  clone fmap.MapApp with type key = accNumber
 
  (* STATE VARIABLE: maps account numbers to balances  *) 
  val ref accounts : t amount 

Note the use of the applicative Map programming type from the finite maps library, corresponding to a declarative interface for a dictionary type (a partial function).
The clone operation creates the type of maps with domain type accNumber ; subsequently, t amount corresponds to the type of maps from accNumber to amount .

The most important map library functions are the following

  val create () : t 'v                         (* create empty map *)
  val mem (k: key) (m: t 'v) : bool            (* KEY membership predicate *)
  val is_empty (m: t 'v) : bool                
  val add (k: key) (v: 'v) (m: t 'v) : t 'v.   (* adds/assigns pair k -> v *)
  val find (k: key) (m: t 'v) : 'v             (* value associated with key k *)

Why3 generates verification conditions for find operations, to guarantee that the keys being read are actually in the domain of the dictionary (finite map). These are safety VCs, that have the goal of preventing the occurrence of runtime errors.

In fact, we will create a record type with a single field (a map), which will allow us to include a state invariant as a type invariant:

  val ref accounts : t amount 

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

  val accounts :state

The invariant states than

The balance of every account is non-negative

Note that “every account” means “every number in the domain of the bal map”. The by clause gives the empty map as an example of such a map.

We now wish to write functions to carry out 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

Let us start by considering the open operation.

Given an account number n , it creates an account with that number
The number should not correspond to an already existing account
In terms of the above state variables, the call open n will insert the pair (n →0) in the state.accounts dictionary

An important question to discuss is what the function should do in case it receives an unexpected argument value.

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 state.accounts ?

We 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, included as preconditions in the contracts of the callee functions

So the function open will not check if n is present in the domain of state.accounts. Instead, it is equipped with an appropriate precondition:

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

Similarly for the function deposit,

given an account number n and an amount x, the call deposit n x will add x to the current balance of account n
n should be a valid account number (i.e. it is in the domain of accounts)

x should be a positive number

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

We have not included postconditions describing what these functions do. One way to do this is of course to simply employ the applicative map operator, which can be used in the logic language:

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

Alternatively, we can opt for a more explicit (i.e. pointwise, and much more verbose) description of how the functions affect the dictionary’s domain and stored values:

  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 }
  = accounts.bal <- add n 0 accounts.bal 

  let deposit (n :accNumber) (x :amount)  
    requires { mem n accounts.bal /\ x > 0 }
    ensures  { forall a :accNumber. 
         mem a accounts.bal <-> mem a (old accounts.bal) } 
    ensures  { accounts.bal n = old accounts.bal n + x }
    ensures  { forall a :accNumber. 
         mem a accounts.bal /\ a <> n -> accounts.bal a = old accounts.bal a }
  = let baln = find n accounts.bal in
    accounts.bal <- add n (baln+x) accounts.bal 

Exercise: Complete the development of this module by writing the remaining functions; then verify it by proving all the generated goals.

As a test, the VCs generated for the following main program should all be proved.

  let withdraw (n :accNumber) (x :amount)  
  = ... 

  let transfer (from :accNumber) (to_ :accNumber) (x :amount)  
  = ...

  let main ()
    ensures { find 1111 accounts.bal = 50 }
    ensures { find 2222 accounts.bal = 0 }
    ensures { find 3333 accounts.bal = 200 }
  = accounts.bal <- create()  ;
    open 1111 ;
    open 2222 ;
    open 3333 ;
    deposit 1111 200 ; 
    deposit 2222 100 ; 
    transfer 1111 3333 100 ;
    transfer 2222 3333 100 ;
    withdraw 1111 50     

Try also the following modifications, which should result in unproved VCs:

Changing the last instruction to withdraw 1111 50
Changing the second postcondition to **find** 2222 accounts.bal = 0

[permalink]

Métodos Formais em Engenharia de Software

Mestrado em Engenharia Informática

Why3: State-based Development

Mutable Variables

Records and Type Invariants

A Second Example, Using Maps