(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 = 64 :: Word8

And similarly, sat finds a satisfying instance. The types involved are:

    prove :: Provable a => a -> IO ThmResult
    sat   :: Satisfiable a => a -> IO SatResult

The classes Provable and Satisfiable come 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.

Symbolic Types

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.
• SRational: Rationals. (Ratio of two symbolic integers.)
• SFloatingPoint: Generalized IEEE-754 floating point values, with user specified exponent and mantissa widths.
• 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: 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.
• Ability to define SMTLib functions, generated directly from Haskell versions, including support for recursive and mutually recursive functions.
• Express quantified formulas (both universals and existentials, including alternating quantifiers), covering first-order logic.
• 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.

Solvers

The sbv library uses third-party SMT solvers via the standard SMT-Lib interface: https://smt-lib.org

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, and CVC5 from Stanford University and the University of Iowa. https://cvc4.github.io/ and https://cvc5.github.io
• Boolector from Johannes Kepler University: https://boolector.github.io and its successor Bitwuzla from Stanford university: https://bitwuzla.github.io
• MathSAT from Fondazione Bruno Kessler and DISI-University of Trento: http://mathsat.fbk.eu/
• Yices from SRI: http://yices.csl.sri.com/
• DReal from CMU: http://dreal.github.io/
• OpenSMT from Università della Svizzera italiana https://verify.inf.usi.ch/opensmt
• 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.

Semi-automated theorem proving

While SMT solvers are quite powerful, there is a certain class of problems that they are just not well suited for. In particular, SMT solvers are not good at proofs that require induction, or those that require complex chains of reasoning. Induction is necessary to reason about any recursive algorithm, and most such proofs require carefully constructed equational steps. SBV allows for a style of semi-automated theorem proving, called KnuckleDragger, that can be used to construct such proofs. The documentation includes example proofs for many list functions, and even inductive proofs for the familiar insertion and merge-sort algorithms, along with a proof that the square-root of 2 is irrational. While a proper theorem prover (such as Lean, Isabelle etc.) is a more appropriate choice for such proofs, with some guidance (and acceptance of a much larger trusted code base!), SBV can be used to establish correctness of various mathematical claims and algorithms that are usually beyond the scope of SMT solvers alone. See Data.SBV.Tools.KnuckleDragger for the API, and

• Documentation.SBV.Examples.KnuckleDragger.InsertionSort
• Documentation.SBV.Examples.KnuckleDragger.MergeSort
• Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational
• Documentation.SBV.Examples.KnuckleDragger.ShefferStroke
• Documentation.SBV.Examples.KnuckleDragger.Lists

for various proofs performed in this style.

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.