sbv-2.0: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Portability portable experimental erkokl@gmail.com Safe-Infered

Data.SBV.Examples.Uninterpreted.AUF

Description

Formalizes and proves the following theorem, about arithmetic, uninterpreted functions, and arrays. (For reference, see http://research.microsoft.com/en-us/um/redmond/projects/z3/fmcad06-slides.pdf slide number 24):

```    x + 2 = y  implies  f (read (write (a, x, 3), y - 2)) = f (y - x + 1)
```

We interpret the types as follows (other interpretations certainly possible):

x
`SWord32` (32-bit unsigned address)
y
`SWord32` (32-bit unsigned address)
a
An array, indexed by 32-bit addresses, returning 32-bit unsigned integers
f
An uninterpreted function of type `SWord32 -> SWord64`

The function `read` and `write` are usual array operations.

Synopsis

# Model using functional arrays

The array type, takes symbolic 32-bit unsigned indexes and stores 32-bit unsigned symbolic values. These are functional arrays where reading before writing a cell throws an exception.

Uninterpreted function in the theorem

thm1 :: SWord32 -> SWord32 -> A -> SWord32 -> SBoolSource

Correctness theorem. We state it for all values of `x`, `y`, and the array `a`. We also take an arbitrary initializer for the array.

Prints Q.E.D. when run, as expected

````>>> ````proveThm1
```Q.E.D.
```

# Model using SMT arrays

This version directly uses SMT-arrays and hence does not need an initializer. Reading an element before writing to it returns an arbitrary value.

thm2 :: SWord32 -> SWord32 -> B -> SBoolSource

Same as `thm1`, except we don't need an initializer with the `SArray` model.

Prints Q.E.D. when run, as expected:

````>>> ````proveThm2
```Q.E.D.
```