sbv-0.9.2: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.

Portability portable experimental erkokl@gmail.com

Data.SBV

Description

(The sbv library is hosted at http://github.com/LeventErkok/sbv. Comments, bug reports, and patches are always welcome.)

SBV: Symbolic Bit Vectors in Haskell

Express properties about bit-precise Haskell programs and automatically prove them using SMT solvers.

```   \$ ghci -XScopedTypeVariables
Prelude> :m Data.SBV
Prelude Data.SBV> prove \$ \(x::SWord8) -> x `shiftL` 2 .== 4*x
Q.E.D.
Prelude Data.SBV> prove \$ forAll ["x"] \$ \(x::SWord8) -> x `shiftL` 2 .== x
Falsifiable. Counter-example:
x = 128 :: SWord8
```

The function `prove` has the following type:

```     `prove` :: `Provable` a => a -> `IO` `ThmResult`
```

The class `Provable` comes with instances for n-ary predicates, for arbitrary n. The predicates are just regular Haskell functions over symbolic signed and unsigned bit-vectors. Functions for checking satisfiability (`sat` and `allSat`) are also provided.

In particular, the sbv library introduces the types:

• `SBool`: Symbolic Booleans (bits)
• `SWord8`, `SWord16`, `SWord32`, `SWord64`: Symbolic Words (unsigned)
• `SInt8`, `SInt16`, `SInt32`, `SInt64`: Symbolic Ints (signed)
• `SArray`, `SFunArray`: Flat arrays of symbolic values
• Symbolic polynomials over GF(2^n), and polynomial arithmetic

The user can construct ordinary Haskell programs using these types, which behave very similar to their concrete counterparts. In particular these types belong to the standard classes `Num`, `Bits`, custom versions of `Eq` (`EqSymbolic`) and `Ord` (`OrdSymbolic`), along with several other custom classes for simplifying bit-precise programming with symbolic values. The framework takes full advantage of Haskell's type inference to avoid many common mistakes.

Furthermore, predicates (i.e., functions that return `SBool`) built out of these types can also be:

• proven correct via an external SMT solver (the `prove` function)
• checked for satisfiability (the `sat` and `allSat` functions)
• quick-checked

If a predicate is not valid, `prove` will return a counterexample: An assignment to inputs such that the predicate fails. The `sat` function will return a satisfying assignment, if there is one. The `allSat` function returns all satisfying assignments, lazily.

The sbv library uses third-party SMT solvers via the standard SMT-Lib interface: http://goedel.cs.uiowa.edu/smtlib/.

While the library is designed to work with any SMT-Lib compliant SMT-solver, solver specific support is required for parsing counter-example/model data since there is currently no agreed upon format for getting models from arbitrary SMT solvers. (The SMT-Lib2 initiative will potentially address this issue in the future, at which point the sbv library can be generalized as well.) Currently, we only support the Yices SMT solver from SRI as far as the counter-example and model generation support is concerned: http://yices.csl.sri.com/. However, other solvers can be hooked up with relative ease.

You should download and install Yices on your machine, and make sure the `yices` executable is in your path before using the sbv library, as it is the current default solver. Alternatively, you can specify the location of yices executable in the environment variable `SBV_YICES` and the options to yices in `SBV_YICES_OPTIONS`. (The default for the latter is '"-m -f"'.)

Synopsis

# Programming with symbolic values

The SBV library is really two things:

• A framework for writing bit-precise programs in Haskell
• A framework for proving properties of such programs using SMT solvers

In this first section we will look at the constructs that will let us construct such programs in Haskell. The goal is to have a seamless experience, i.e., program in the usual Haskell style without distractions of symbolic coding. While Haskell helps in some aspects (the `Num` and `Bits` classes simplify coding), it makes life harder in others. For instance, `if-then-else` only takes `Bool` as a test in Haskell, and comparisons (`>` etc.) only return `Bool`s. Clearly we would like these values to be symbolic (i.e., `SBool`), thus stopping us from using some native Haskell constructs. When symbolic versions of operators are needed, they are typically obtained by prepending a dot, for instance `==` becomes `.==`. Care has been taken to make the transition painless. In particular, any Haskell program you build out of symbolic components is fully concretely executable within Haskell, without the need for any custom interpreters. (They are truly Haskell programs, not AST's built out of pieces of syntax.) This provides for an integrated feel of the system, one of the original design goals for SBV.

## Symbolic types

### Symbolic bit

type SBool = SBV BoolSource

A symbolic boolean/bit

### Unsigned symbolic bit-vectors

type SWord8 = SBV Word8Source

8-bit unsigned symbolic value

16-bit unsigned symbolic value

32-bit unsigned symbolic value

64-bit unsigned symbolic value

### Signed symbolic bit-vectors

type SInt8 = SBV Int8Source

8-bit signed symbolic value, 2's complement representation

type SInt16 = SBV Int16Source

16-bit signed symbolic value, 2's complement representation

type SInt32 = SBV Int32Source

32-bit signed symbolic value, 2's complement representation

type SInt64 = SBV Int64Source

64-bit signed symbolic value, 2's complement representation

### Arrays of symbolic values

class SymArray array whereSource

Flat arrays of symbolic values An `array a b` is an array indexed by the type `SBV a`, with elements of type `SBV b` If an initial value is not provided in `newArray_` and `newArray` methods, then the elements are left unspecified, i.e., the solver is free to choose any value. This is the right thing to do if arrays are used as inputs to functions to be verified, typically. Reading an uninitilized entry is an error. While it's certainly possible for user to create instances of `SymArray`, the `SArray` and `SFunArray` instances already provided should cover most use cases in practice.

Minimal complete definition: All methods are required, no defaults.

Methods

newArray_ :: (HasSignAndSize a, HasSignAndSize b) => Maybe (SBV b) -> Symbolic (array a b)Source

Create a new array, with an optional initial value

newArray :: (HasSignAndSize a, HasSignAndSize b) => String -> Maybe (SBV b) -> Symbolic (array a b)Source

Create a named new array with, with an optional initial value

readArray :: array a b -> SBV a -> SBV bSource

Read the array element at `a`

resetArray :: SymWord b => array a b -> SBV b -> array a bSource

Reset all the elements of the array to the value `b`

writeArray :: SymWord b => array a b -> SBV a -> SBV b -> array a bSource

Update the element at `a` to be `b`

mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a bSource

Merge two given arrays on the symbolic condition Intuitively: `mergeArrays cond a b = if cond then a else b`. Merging pushes the if-then-else choice down on to elements

Instances

 SymArray SFunArray SymArray SArray

data SArray a b Source

Arrays implemented in terms of SMT-arrays: http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2

Instances

 SymArray SArray (HasSignAndSize a, HasSignAndSize b) => Show (SArray a b) SymWord b => Mergeable (SArray a b) EqSymbolic (SArray a b)

data SFunArray a b Source

Arrays implemented internally as functions, and rendered as SMT-Lib functions

Instances

 SymArray SFunArray (HasSignAndSize a, HasSignAndSize b) => Show (SFunArray a b) (SymWord b, Arbitrary b) => Arbitrary (SFunArray a b) SymWord b => Mergeable (SFunArray a b)

## Operations on symbolic words

### Word level

bitValue :: (Bits a, SymWord a) => SBV a -> Int -> SBoolSource

Replacement for `testBit`. Since `testBit` requires a `Bool` to be returned, we cannot implement it for symbolic words. Index 0 is the least-significant bit.

setBitTo :: (Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV aSource

Generalization of `setBit` based on a symbolic boolean. Note that `setBit` and `clearBit` are still available on Symbolic words, this operation comes handy when the condition to set/clear happens to be symbolic

oneIf :: (Num a, SymWord a) => SBool -> SBV aSource

Returns 1 if the boolean is true, otherwise 0

lsb :: (Bits a, SymWord a) => SBV a -> SBoolSource

Least significant bit of a word, always stored at index 0

msb :: (Bits a, SymWord a) => SBV a -> SBoolSource

Most significant bit of a word, always stored at the last position

### List level

allEqual :: (Eq a, SymWord a) => [SBV a] -> SBoolSource

Returns (symbolic) true if all the elements of the given list are the same

allDifferent :: (Eq a, SymWord a) => [SBV a] -> SBoolSource

Returns (symbolic) true if all the elements of the given list are different

### Blasting/Unblasting

blastBE :: (Bits a, SymWord a) => SBV a -> [SBool]Source

Big-endian blasting of a word into its bits. Also see the `FromBits` class

blastLE :: (Bits a, SymWord a) => SBV a -> [SBool]Source

Little-endian blasting of a word into its bits. Also see the `FromBits` class

class FromBits a whereSource

Unblasting a value from symbolic-bits. The bits can be given little-endian or big-endian. For a signed number in little-endian, we assume the very last bit is the sign digit. This is a bit awkward, but it is more consistent with the reverse view of little-big-endian representations

Minimal complete definiton: `fromBitsLE`

Methods

fromBitsLE :: [SBool] -> aSource

fromBitsBE :: [SBool] -> aSource

### Splitting, joining, and extending

class Splittable a b | b -> a whereSource

Splitting an `a` into two `b`'s and joining back. Intuitively, `a` is a larger bit-size word than `b`, typically double. The `extend` operation captures embedding of a `b` value into an `a` without changing its semantic value.

Minimal complete definition: All, no defaults.

Methods

split :: a -> (b, b)Source

(#) :: b -> b -> aSource

extend :: b -> aSource

## Polynomial arithmetic

class Bits a => Polynomial a whereSource

Implements polynomial addition, multiplication, division, and modulus operations over GF(2^n). NB. Similar to `bvQuotRem`, division by `0` is interpreted as follows:

`x `pDivMod` 0 = (0, x)`

for all `x` (including `0`)

Minimal complete definiton: `pMult`, `pDivMod`, `showPoly`

Methods

polynomial :: [Int] -> aSource

Given bit-positions to be set, create a polynomial For instance

`polynomial [0, 1, 3] :: SWord8`

will evaluate to `11`, since it sets the bits `0`, `1`, and `3`. Mathematicans would write this polynomial as `x^3 + x + 1`. And in fact, `showPoly` will show it like that.

pAdd :: a -> a -> aSource

Add two polynomials in GF(2^n)

pMult :: (a, a, [Int]) -> aSource

Multiply two polynomials in GF(2^n), and reduce it by the irreducible specified by the polynomial as specified by coefficients of the third argument. Note that the third argument is specifically left in this form as it is usally in GF(2^(n+1)), which is not available in our formalism. (That is, we would need SWord9 for SWord8 multiplication, etc.) Also note that we do not support symbolic irreducibles, which is a minor shortcoming. (Most GF's will come with fixed irreducibles, so this should not be a problem in practice.)

Passing [] for the third argument will multiply the polynomials and then ignore the higher bits that won't fit into the resulting size.

pDiv :: a -> a -> aSource

Divide two polynomials in GF(2^n), see above note for division by 0

pMod :: a -> a -> aSource

Compute modulus of two polynomials in GF(2^n), see above note for modulus by 0

pDivMod :: a -> a -> (a, a)Source

Division and modulus packed together

showPoly :: a -> StringSource

Display a polynomial like a mathematician would (over the monomial `x`)

## Conditionals: Mergeable values

class Mergeable a whereSource

Symbolic choice operator, parameterized via a class `select` is a total-indexing function, with the default.

Minimal complete definition: `symbolicMerge`

Methods

symbolicMerge :: SBool -> a -> a -> aSource

Merge two values based on the condition

ite :: SBool -> a -> a -> aSource

Choose one or the other element, based on the condition. This is similar to `symbolicMerge`, but it has a default implementation that makes sure it's short-cut if the condition is concrete

select :: (Bits b, SymWord b, Integral b) => [a] -> a -> SBV b -> aSource

Total indexing operation. `select xs default index` is intuitively the same as `xs !! index`, except it evaluates to `default` if `index` overflows

Instances

 Mergeable () Mergeable Mostek Mergeable Status Mergeable a => Mergeable [a] Mergeable a => Mergeable (Maybe a) SymWord a => Mergeable (SBV a) Mergeable a => Mergeable (Move a) Mergeable b => Mergeable (a -> b) (Mergeable a, Mergeable b) => Mergeable (Either a b) (Mergeable a, Mergeable b) => Mergeable (a, b) (Ix a, Mergeable b) => Mergeable (Array a b) SymWord b => Mergeable (SFunArray a b) SymWord b => Mergeable (SArray a b) (Mergeable a, Mergeable b, Mergeable c) => Mergeable (a, b, c) (Mergeable a, Mergeable b, Mergeable c, Mergeable d) => Mergeable (a, b, c, d) (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e) => Mergeable (a, b, c, d, e) (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f) => Mergeable (a, b, c, d, e, f) (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f, Mergeable g) => Mergeable (a, b, c, d, e, f, g)

## Symbolic equality

class EqSymbolic a whereSource

Symbolic Equality. Note that we can't use Haskell's `Eq` class since Haskell insists on returning Bool Comparing symbolic values will necessarily return a symbolic value.

Minimal complete definition: `.==`

Methods

(.==) :: a -> a -> SBoolSource

(./=) :: a -> a -> SBoolSource

Instances

 EqSymbolic Bool EqSymbolic SWord11 EqSymbolic a => EqSymbolic [a] EqSymbolic a => EqSymbolic (Maybe a) EqSymbolic (SBV a) (EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b) (EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b) EqSymbolic (SArray a b) (EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c) (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d) (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e) (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f) => EqSymbolic (a, b, c, d, e, f) (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f, EqSymbolic g) => EqSymbolic (a, b, c, d, e, f, g)

## Symbolic ordering

class (Mergeable a, EqSymbolic a) => OrdSymbolic a whereSource

Symbolic Comparisons. Similar to `Eq`, we cannot implement Haskell's `Ord` class since there is no way to return an `Ordering` value from a symbolic comparison. Furthermore, `OrdSymbolic` requires `Mergeable` to implement if-then-else, for the benefit of implementing symbolic versions of `max` and `min` functions.

Minimal complete definition: `.<`

Methods

(.<) :: a -> a -> SBoolSource

(.>=) :: a -> a -> SBoolSource

(.>) :: a -> a -> SBoolSource

(.<=) :: a -> a -> SBoolSource

smin :: a -> a -> aSource

smax :: a -> a -> aSource

Instances

 OrdSymbolic a => OrdSymbolic [a] OrdSymbolic a => OrdSymbolic (Maybe a) SymWord a => OrdSymbolic (SBV a) (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b) (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b) (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c) (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d) (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e) (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f) => OrdSymbolic (a, b, c, d, e, f) (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f, OrdSymbolic g) => OrdSymbolic (a, b, c, d, e, f, g)

## Division

class BVDivisible a whereSource

The `BVDivisible` class captures the essence of division of words. Unfortunately we cannot use Haskell's `Integral` class since the `Real` and `Enum` superclasses are not implementable for symbolic bit-vectors. However, `quotRem` makes perfect sense, and the `BVDivisible` class captures this operation. One issue is how division by 0 behaves. The verification technology requires total functions, and there are several design choices here. We follow Isabelle/HOL approach of assigning the value 0 for division by 0. Therefore, we impose the following law:

` x `bvQuotRem` 0 = (0, x)`

Note that our instances implement this law even when `x` is `0` itself.

Minimal complete definition: `bvQuotRem`

Methods

bvQuotRem :: a -> a -> (a, a)Source

## The Boolean class

class Boolean b whereSource

The `Boolean` class: a generalization of Haskell's `Bool` type Haskell `Bool` and SBV's `SBool` are instances of this class, unifying the treatment of boolean values.

Minimal complete definition: `true`, `bnot`, `&&&` However, it's advisable to define `false`, and `|||` as well (typically), for clarity.

Methods

true :: bSource

logical true

false :: bSource

logical false

bnot :: b -> bSource

complement

(&&&) :: b -> b -> bSource

and

(|||) :: b -> b -> bSource

or

(~&) :: b -> b -> bSource

nand

(~|) :: b -> b -> bSource

nor

(<+>) :: b -> b -> bSource

xor

(==>) :: b -> b -> bSource

implies

(<=>) :: b -> b -> bSource

equivalence

fromBool :: Bool -> bSource

cast from Bool

Instances

 Boolean Bool Boolean SBool

### Generalizations of boolean operations

bAnd :: Boolean b => [b] -> bSource

Generalization of `and`

bOr :: Boolean b => [b] -> bSource

Generalization of `or`

bAny :: Boolean b => (a -> b) -> [a] -> bSource

Generalization of `any`

bAll :: Boolean b => (a -> b) -> [a] -> bSource

Generalization of `all`

## Pretty-printing and reading numbers in Hex & Binary

class PrettyNum a whereSource

PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers.

Minimal complete definition: `hexS` and `binS`

Methods

hexS :: a -> StringSource

Show a number in hexadecimal (starting with `0x`)

binS :: a -> StringSource

Show a number in binary (starting with `0b`)

hex :: a -> IO ()Source

IO version of `hexS`

bin :: a -> IO ()Source

IO version of `binS`

Instances

 PrettyNum Bool PrettyNum Int8 PrettyNum Int16 PrettyNum Int32 PrettyNum Int64 PrettyNum Word8 PrettyNum Word16 PrettyNum Word32 PrettyNum Word64 PrettyNum Bit PrettyNum CW (SymWord a, PrettyNum a) => PrettyNum (SBV a)

readBin :: Num a => String -> aSource

A more convenient interface for reading binary numbers, also supports negative numbers

# Proving properties

The SBV library provides a push-button verification system via automated SMT solving. The design goal is to let SMT solvers be used without any knowledge of how SMT solvers work or how different logics operate. The details are hidden behind the SBV framework, providing Haskell programmers with a clean API that is unencumbered by the details of individual solvers. To that end, we use the SMT-Lib standard (http://goedel.cs.uiowa.edu/smtlib/) to communicate with arbitrary SMT solvers. Unfortunately, the SMT-Lib version 1.X does not standardize how models are communicated back from solvers, so there is some work in parsing individual SMT solver output. The 2.X version of the SMT-Lib standard (not yet implemented by SMT solvers widely, unfortunately) will bring new standard features for getting models; at which time the SBV framework can be modified into a truly plug-and-play system where arbitrary SMT solvers can be used.

## Predicates

A predicate is a symbolic program that returns a (symbolic) boolean value. For all intents and purposes, it can be treated as an n-ary function from symbolic-values to a boolean. The `Symbolic` monad captures the underlying representation, and can/should be ignored by the users of the library, unless you are building further utilities on top of SBV itself. Instead, simply use the `Predicate` type when necessary.

class Provable a whereSource

A type `a` is provable if we can turn it into a predicate. Note that a predicate can be made from a curried function of arbitrary arity, where each element is either a symbolic type or up-to a 7-tuple of symbolic-types. So predicates can be constructed from almost arbitrary Haskell functions that have arbitrary shapes. (See the instance declarations below.)

Methods

forAll_ :: a -> PredicateSource

Turns a value into a predicate, internally naming the inputs. In this case the sbv library will use names of the form `s1, s2`, etc. to name these variables Example:

```  forAll_ \$ \(x::SWord8) y -> x `shiftL` 2 .== y
```

is a predicate with two arguments, captured using an ordinary Haskell function. Internally, `x` will be named `s0` and `y` will be named `s1`.

forAll :: [String] -> a -> PredicateSource

Turns a value into a predicate, allowing users to provide names for the inputs. If the user does not provide enough number of names for the free variables, the remaining ones will be internally generated. Note that the names are only used for printing models and has no other significance; in particular, we do not check that they are unique. Example:

```  forAll ["x", "y"] \$ \(x::SWord8) y -> x `shiftL` 2 .== y
```

This is the same as above, except the variables will be named `x` and `y` respectively, simplifying the counter-examples when they are printed.

Instances

 Provable SBool Provable Predicate (SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) -> p) (SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) -> p) (SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) -> p) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) (HasSignAndSize a, HasSignAndSize b, SymArray array, Provable p) => Provable (array a b -> p) (SymWord a, Provable p) => Provable (SBV a -> p)

class Equality a whereSource

Equality as a proof method. Allows for very concise construction of equivalence proofs, which is very typical in bit-precise proofs.

Methods

(===) :: a -> a -> IO ThmResultSource

Instances

 (SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) (SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) (SymWord a, EqSymbolic z) => Equality (SBV a -> z)

## Proving properties

prove :: Provable a => a -> IO ThmResultSource

Prove a predicate, equivalent to `proveWith defaultSMTCfg`

proveWith :: Provable a => SMTConfig -> a -> IO ThmResultSource

Proves the predicate using the given SMT-solver

isTheorem :: Provable a => a -> IO BoolSource

Checks theoremhood

isTheoremWithin :: Provable a => Int -> a -> IO (Maybe Bool)Source

Checks theoremhood within the given time limit of `i` seconds. Returns `Nothing` if times out, or the result wrapped in a `Just` otherwise.

## Checking satisfiability

sat :: Provable a => a -> IO SatResultSource

Find a satisfying assignment for a predicate, equivalent to `satWith defaultSMTCfg`

satWith :: Provable a => SMTConfig -> a -> IO SatResultSource

Find a satisfying assignment using the given SMT-solver

isSatisfiable :: Provable a => a -> IO BoolSource

Checks satisfiability

isSatisfiableWithin :: Provable a => Int -> a -> IO (Maybe Bool)Source

Checks satisfiability within the given time limit of `i` seconds. Returns `Nothing` if times out, or the result wrapped in a `Just` otherwise.

## Finding all satisfying assignments

allSat :: Provable a => a -> IO AllSatResultSource

Return all satisfying assignments for a predicate, equivalent to `allSatWith defaultSMTCfg`. Satisfying assignments are constructed lazily, so they will be available as returned by the solver and on demand.

allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResultSource

Find all satisfying assignments using the given SMT-solver

numberOfModels :: Provable a => a -> IO IntSource

Returns the number of models that satisfy the predicate, as it would be returned by `allSat`. Note that the number of models is always a finite number, and hence this will always return a result. Of course, computing it might take quite long, as it literally generates and counts the number of satisfying models.

# Model extraction

The default `Show` instances for prover calls provide all the counter-example information in a human-readable form and should be sufficient for most casual uses of sbv. However, tools built on top of sbv will inevitably need to look into the constructed models more deeply, programmatically extracting their results and performing actions based on them. The API provided in this section aims at simplifying this task.

## Inspecting proof results

`ThmResult`, `SatResult`, and `AllSatResult` are simple newtype wrappers over `SMTResult`. Their main purpose is so that we can provide custom `Show` instances to print results accordingly.

newtype ThmResult Source

A `prove` call results in a `ThmResult`

Constructors

 ThmResult SMTResult

Instances

 Show ThmResult

newtype SatResult Source

A `sat` call results in a `SatResult` The reason for having a separate `SatResult` is to have a more meaningful `Show` instance.

Constructors

 SatResult SMTResult

Instances

 Show SatResult

newtype AllSatResult Source

An `allSat` call results in a `AllSatResult`

Constructors

 AllSatResult [SMTResult]

Instances

 Show AllSatResult

data SMTResult Source

The result of an SMT solver call. Each constructor is tagged with the `SMTConfig` that created it so that further tools can inspect it and build layers of results, if needed. For ordinary uses of the library, this type should not be needed, instead use the accessor functions on it. (Custom Show instances and model extractors.)

Constructors

 Unsatisfiable SMTConfig Unsatisfiable Satisfiable SMTConfig [(String, CW)] Satisfiable with model Unknown SMTConfig [(String, CW)] Prover returned unknown, with a potential (possibly bogus) model ProofError SMTConfig [String] Prover errored out TimeOut SMTConfig Computation timed out (see the `timeout` combinator)

Instances

 NFData SMTResult

## Programmable model extraction

While default `Show` instances are sufficient for most use cases, it is sometimes desirable (especially for library construction) that the SMT-models are reinterpreted in terms of domain types. Programmable extraction allows getting arbitrarily typed models out of SMT models.

class SatModel a whereSource

Instances of `SatModel` can be automatically extracted from models returned by the solvers. The idea is that the sbv infrastructure provides a stream of `CW'`s (constant-words) coming from the solver, and the type `a` is interpreted based on these constants. Many typical instances are already provided, so new instances can be declared with relative ease.

Minimum complete definition: `parseCWs`

Methods

parseCWs :: [CW] -> Maybe (a, [CW])Source

Given a sequence of constant-words, extract one instance of the type `a`, returning the remaining elements untouched. If the next element is not what's expected for this type you should return `Nothing`

cvtModel :: (a -> Maybe b) -> Maybe (a, [CW]) -> Maybe (b, [CW])Source

Given a parsed model instance, transform it using `f`, and return the result. The default definition for this method should be sufficient in most use cases.

Instances

 SatModel Bool SatModel Int8 SatModel Int16 SatModel Int32 SatModel Int64 SatModel Word8 SatModel Word16 SatModel Word32 SatModel Word64 SatModel U2Member SatModel a => SatModel [a] (SatModel a, SatModel b) => SatModel (a, b) (SatModel a, SatModel b, SatModel c) => SatModel (a, b, c) (SatModel a, SatModel b, SatModel c, SatModel d) => SatModel (a, b, c, d) (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e) => SatModel (a, b, c, d, e) (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f) => SatModel (a, b, c, d, e, f) (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f, SatModel g) => SatModel (a, b, c, d, e, f, g)

getModel :: SatModel a => SMTResult -> aSource

Given an `SMTResult`, extract an arbitrarily typed model from it, given a `SatModel` instance

displayModels :: SatModel a => (Int -> a -> IO ()) -> AllSatResult -> IO IntSource

Given an `allSat` call, we typically want to iterate over it and print the results in sequence. The `displayModels` function automates this task by calling `disp` on each result, consecutively. The first `Int` argument to `disp` 'is the current model number.

# SMT Interface: Configurations and solvers

data SMTConfig Source

Solver configuration

Constructors

 SMTConfig Fieldsverbose :: BoolDebug mode timing :: BoolPrint timing information on how long different phases took (construction, solving, etc.) printBase :: IntPrint literals in this base solver :: SMTSolverThe actual SMT solver

data SMTSolver Source

An SMT solver

Constructors

 SMTSolver Fieldsname :: StringPrintable name of the solver executable :: StringThe path to its executable options :: [String]Options to provide to the solver engine :: SMTEngineThe solver engine, responsible for interpreting solver output

Default configuration for the SMT solver. Non-verbose, non-timing, prints results in base 10, and uses the Yices SMT solver.

Same as `defaultSMTCfg`, except verbose

Same as `defaultSMTCfg`, except prints timing info

Same as `defaultSMTCfg`, except both verbose and timing info

Adds a time out of `n` seconds to a given solver configuration

The description of the Yices SMT solver The default executable is `"yices"`, which must be in your path. You can use the `SBV_YICES` environment variable to point to the executable on your system. The default options are `"-m -f"`, which is valid for Yices 2 series. You can use the `SBV_YICES_OPTIONS` environment variable to override the options.

# Symbolic computations

data Symbolic a Source

A Symbolic computation. Represented by a reader monad carrying the state of the computation, layered on top of IO for creating unique references to hold onto intermediate results.

Instances

 Monad Symbolic MonadIO Symbolic MonadReader State Symbolic

output :: SBV a -> Symbolic (SBV a)Source

Mark an interim result as an output. Useful when constructing Symbolic programs that return multiple values, or when the result is programmatically computed.

class Ord a => SymWord a whereSource

A `SymWord` is a potential symbolic bitvector that can be created instances of to be fed to a symbolic program. Note that these methods are typically not needed in casual uses with `prove`, `sat`, `allSat` etc, as default instances automatically provide the necessary bits.

Methods

free :: String -> Symbolic (SBV a)Source

Create a user named input

Create an automatically named input

literal :: a -> SBV aSource

Turn a literal constant to symbolic

unliteral :: SBV a -> Maybe aSource

Extract a literal, if the value is concrete

fromCW :: CW -> aSource

Extract a literal, from a CW representation

isConcrete :: SBV a -> BoolSource

Is the symbolic word concrete?

isSymbolic :: SBV a -> BoolSource

Is the symbolic word really symbolic?

# Module exports

The SBV library exports the following modules wholesale, as user programs will have to import these three modules to make any sensible use of the SBV functionality.

module Data.Bits

module Data.Word

module Data.Int