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

SBV: SMT Based Verification

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

>>> prove $ \x -> x `shiftL` 2 .== 4 * (x :: SWord8)
Q.E.D.

>>> prove $ \x -> x `shiftL` 2 .== 2 * (x :: SWord8)
Falsifiable. Counter-example:
  s0 = 32 :: Word8

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 types listed below. Functions for checking satisfiability (sat and allSat) are also provided.

The sbv library introduces the following symbolic types:

• SBool: Symbolic Booleans (bits).
• SWord8, SWord16, SWord32, SWord64: Symbolic Words (unsigned).
• SInt8, SInt16, SInt32, SInt64: Symbolic Ints (signed).
• 'SWord n': Generalized symbolic words of arbitrary bit-size.
• 'SInt n': Generalized symbolic ints of arbitrary bit-size.
• SInteger: Unbounded signed integers.
• SReal: Algebraic-real numbers
• SFloat: IEEE-754 single-precision floating point values
• SDouble: IEEE-754 double-precision floating point values
• SChar, SString, RegExp: Characters, strings and regular expressions
• SList: Symbolic lists (which can be nested)
• STuple, STuple2, STuple3, .., STuple8 : Symbolic tuples (upto 8-tuples, can be nested)
• SEither: Symbolic sums
• SMaybe: Symbolic optional values
• SSet: Symbolic sets
• SArray, SFunArray: Flat arrays of symbolic values.
• Symbolic polynomials over GF(2^n), polynomial arithmetic, and CRCs.
• Uninterpreted constants and functions over symbolic values, with user defined SMT-Lib axioms.
• Uninterpreted sorts, and proofs over such sorts, potentially with axioms.
• Model validation: SBV can validate models returned by solvers, which allows for protection against bugs in SMT solvers and SBV itself. (See the validateModel parameter.)

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 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, allSat functions)
• used in synthesis (the sat function with existentials)
• 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.

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

The SBV library is designed to work with any SMT-Lib compliant SMT-solver. Currently, we support the following SMT-Solvers out-of-the box:

• ABC from University of Berkeley: http://www.eecs.berkeley.edu/~alanmi/abc/
• CVC4 from Stanford: http://cvc4.cs.stanford.edu/web/
• Boolector from Johannes Kepler University: http://fmv.jku.at/boolector/
• MathSAT from Fondazione Bruno Kessler and DISI-University of Trento: http://mathsat.fbk.eu/
• Yices from SRI: http://yices.csl.sri.com/
• Z3 from Microsoft: http://github.com/Z3Prover/z3/wiki

SBV requires recent versions of these solvers; please see the file SMTSolverVersions.md in the source distribution for specifics.

SBV also allows calling these solvers in parallel, either getting results from multiple solvers or returning the fastest one. (See proveWithAll, proveWithAny, etc.)

Support for other compliant solvers can be added relatively easily, please get in touch if there is a solver you'd like to see included.

The SBV library is really two things:

• A framework for writing symbolic programs in Haskell, i.e., programs operating on symbolic values along with the usual concrete counterparts.
• A framework for proving properties of such programs using SMT solvers.

The programming goal of SBV is to provide a seamless experience, i.e., let people 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 Bools. 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.

Incremental query mode: SBV provides a wide variety of ways to utilize SMT-solvers, without requiring the user to deal with the solvers themselves. While this mode is convenient, advanced users might need access to the underlying solver at a lower level. For such use cases, SBV allows users to have an interactive session: The user can issue commands to the solver, inspect the values/results, and formulate new constraints. This advanced feature is available through the Data.SBV.Control module, where most SMTLib features are made available via a typed-API.

The SBV library supports unbounded signed integers with the type SInteger, which are not subject to overflow/underflow as it is the case with the bounded types, such as SWord8, SInt16, etc. However, some bit-vector based operations are not supported for the SInteger type while in the verification mode. That is, you can use these operations on SInteger values during normal programming/simulation. but the SMT translation will not support these operations since there corresponding operations are not supported in SMT-Lib. Note that this should rarely be a problem in practice, as these operations are mostly meaningful on fixed-size bit-vectors. The operations that are restricted to bounded word/int sizes are:

• Rotations and shifts: rotateL, rotateR, shiftL, shiftR
• Bitwise logical ops: .&., .|., xor, complement
• Extraction and concatenation: bvExtract, #, zeroExtend, signExtend, bvDrop, and bvTake

Usual arithmetic (+, -, *, sQuotRem, sQuot, sRem, sDivMod, sDiv, sMod) and logical operations (.<, .<=, .>, .>=, .==, ./=) operations are supported for SInteger fully, both in programming and verification modes.

Floating point numbers are defined by the IEEE-754 standard; and correspond to Haskell's Float and Double types. For SMT support with floating-point numbers, see the paper by Rummer and Wahl: http://www.philipp.ruemmer.org/publications/smt-fpa.pdf.

Algebraic reals are roots of single-variable polynomials with rational coefficients. (See http://en.wikipedia.org/wiki/Algebraic_number.) Note that algebraic reals are infinite precision numbers, but they do not cover all real numbers. (In particular, they cannot represent transcendentals.) Some irrational numbers are algebraic (such as sqrt 2), while others are not (such as pi and e).

SBV can deal with real numbers just fine, since the theory of reals is decidable. (See http://smtlib.cs.uiowa.edu/theories-Reals.shtml.) In addition, by leveraging backend solver capabilities, SBV can also represent and solve non-linear equations involving real-variables. (For instance, the Z3 SMT solver, supports polynomial constraints on reals starting with v4.0.)

Support for characters, strings, and regular expressions (intial version contributed by Joel Burget) adds support for QF_S logic, described here: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml and here: http://rise4fun.com/z3/tutorialcontent/sequences. Note that this logic is still not part of official SMTLib (as of March 2018), so it should be considered experimental.

See Data.SBV.Char, Data.SBV.String, Data.SBV.RegExp for related functions.

Support for symbolic lists (intial version contributed by Joel Burget) adds support for sequence support, described here: http://rise4fun.com/z3/tutorialcontent/sequences. Note that this logic is still not part of official SMTLib (as of March 2018), so it should be considered experimental.

See Data.SBV.List for related functions.

Tuples can be used as symbolic values. This is useful in combination with lists, for example SBV [(Integer, String)] is a valid type. These types can be arbitrarily nested, eg SBV [(Integer, [(Char, (Integer, String))])]. Instances of upto 8-tuples are provided.