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

Safe HaskellNone




Formalizes and proves the following theorem, about arithmetic, uninterpreted functions, and arrays. (For reference, see 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):

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

The function read and write are usual array operations.


Model using functional arrays

type A = SFunArray Word32 Word32Source

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.

f :: SWord32 -> SWord64Source

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.

proveThm1 :: IO ()Source

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

>>> proveThm1

Model using SMT arrays

type B = SArray Word32 Word32Source

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.

proveThm2 :: IO ()Source

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

>>> proveThm2