A symbolic boolean/bit

8-bit unsigned symbolic value

16-bit unsigned symbolic value

32-bit unsigned symbolic value

64-bit unsigned symbolic value

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

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

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

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

Infinite precision signed symbolic value

IEEE-754 single-precision floating point numbers

IEEE-754 double-precision floating point numbers

Rounding mode to be used for the IEEE floating-point operations. Note that Haskell's default is RoundNearestTiesToEven. If you use a different rounding mode, then the counter-examples you get may not match what you observe in Haskell.

Not-A-Number for Double and Float. Surprisingly, Haskell Prelude doesn't have this value defined, so we provide it here.

Infinity for Double and Float. Surprisingly, Haskell Prelude doesn't have this value defined, so we provide it here.

Symbolic variant of Not-A-Number. This value will inhabit both SDouble and SFloat.

Symbolic variant of infinity. This value will inhabit both SDouble and SFloat.

Fused-multiply add. fusedMA a b c = a * b + c, for double and floating point values. Note that a fusedMA call will *never* be concrete, even if all the arguments are constants; since we cannot guarantee the precision requirements, which is the whole reason why fusedMA exists in the first place. (NB. fusedMA only rounds once, even though it does two operations, and hence the extra precision.)

Note that the floating point value NaN does not compare equal to itself, so we need a special recognizer for that. Haskell provides the isNaN predicate with the RealFrac class, which unfortunately is not currently implementable for symbolic cases. (Requires trigonometric functions etc.) Thus, we provide this recognizer separately. Note that the definition simply tests equality against itself, which fails for NaN. Who said equality for floating point was reflexive?

We call a FP number FPPoint if it is neither NaN, nor +/- infinity.

Infinite precision symbolic algebraic real value

Algebraic reals. Note that the representation is left abstract. We represent rational results explicitly, while the roots-of-polynomials are represented implicitly by their defining equation

Promote an SInteger to an SReal

Declare an SBool

Declare an SWord8

Declare an SWord16

Declare an SWord32

Declare an SWord64

Declare an SInt8

Declare an SInt16

Declare an SInt32

Declare an SInt64

Declare an SInteger

Declare an SReal

Declare an SFloat

Declare an SDouble

Declare a list of SBools

Declare a list of SWord8s

Declare a list of SWord16s

Declare a list of SWord32s

Declare a list of SWord64s

Declare a list of SInt8s

Declare a list of SInt16s

Declare a list of SInt32s

Declare a list of SInt64s

Declare a list of SIntegers

Declare a list of SReals

Declare a list of SFloats

Declare a list of SDoubles

The Symbolic value. Either a constant (Left) or a symbolic value (Right Cached). Note that caching is essential for making sure sharing is preserved. The parameter a is phantom, but is extremely important in keeping the user interface strongly typed.

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.

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. (There are some differences between these models, however, see the corresponding declaration.)

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

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

• Maps directly to SMT-lib arrays
• Reading from an unintialized value is OK and yields an uninterpreted result
• Can check for equality of these arrays
• Cannot quick-check theorems using SArray values
• Typically slower as it heavily relies on SMT-solving for the array theory

Arrays implemented internally as functions

• Internally handled by the library and not mapped to SMT-Lib
  • Reading an uninitialized value is considered an error (will throw exception)
  • Cannot check for equality (internally represented as functions)
  • Can quick-check
  • Typically faster as it gets compiled away during translation

Lift a function to an array. Useful for creating arrays in a pure context. (Otherwise use newArray.)

A symbolic tree containing values of type e, indexed by elements of type i. Note that these are full-trees, and their their shapes remain constant. There is no API provided that can change the shape of the tree. These structures are useful when dealing with data-structures that are indexed with symbolic values where access time is important. STree structures provide logarithmic time reads and writes.

Reading a value. We bit-blast the index and descend down the full tree according to bit-values.

Writing a value, similar to how reads are done. The important thing is that the tree representation keeps updates to a minimum.

Construct the fully balanced initial tree using the given values.

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.

Replacement for popCount. Since popCount returns an Int, we cannot implement it for symbolic words. Here, we return an SWord8, which can overflow when used on quantities that have more than 255 bits. Currently, that's only the SInteger type that SBV supports, all other types are safe. Even with SInteger, this will only overflow if there are at least 256-bits set in the number, and the smallest such number is 2^256-1, which is a pretty darn big number to worry about for practical purposes. In any case, we do not support sbvPopCount for unbounded symbolic integers, as the only possible implementation wouldn't symbolically terminate. So the only overflow issue is with really-really large concrete SInteger values.

Generalization of shiftL, when the shift-amount is symbolic. Since Haskell's shiftL only takes an Int as the shift amount, it cannot be used when we have a symbolic amount to shift with. The shift amount must be an unsigned quantity.

Generalization of shiftR, when the shift-amount is symbolic. Since Haskell's shiftR only takes an Int as the shift amount, it cannot be used when we have a symbolic amount to shift with. The shift amount must be an unsigned quantity.

NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical, following the usual Haskell convention. See sbvSignedShiftArithRight for a variant that explicitly uses the msb as the sign bit, even for unsigned underlying types.

Arithmetic shift-right with a symbolic unsigned shift amount. This is equivalent to sbvShiftRight when the argument is signed. However, if the argument is unsigned, then it explicitly treats its msb as a sign-bit, and uses it as the bit that gets shifted in. Useful when using the underlying unsigned bit representation to implement custom signed operations. Note that there is no direct Haskell analogue of this function.

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.

Returns 1 if the boolean is true, otherwise 0.

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

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

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

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

Returns (symbolic) true if the argument is in range

Symbolic membership test

Full adder. Returns the carry-out from the addition.

N.B. Only works for unsigned types. Signed arguments will be rejected.

Full multiplier: Returns both the high-order and the low-order bits in a tuple, thus fully accounting for the overflow.

N.B. Only works for unsigned types. Signed arguments will be rejected.

N.B. The higher-order bits are determined using a simple shift-add multiplier, thus involving bit-blasting. It'd be naive to expect SMT solvers to deal efficiently with properties involving this function, at least with the current state of the art.

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

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

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 definition: fromBitsLE

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.

Sign casting a value into another. This essentially means forgetting the sign bit and reinterpreting the bits accordingly when converting a signed value to an unsigned one. Similarly, when an unsigned quantity is converted to a signed one, the most significant bit is interpreted as the sign. We only define instances when the source and target types are precisely the same size. The idea is that signCast and unsignCast must form an isomorphism pair between the types a and b, i.e., we expect the following two properties to hold:

   signCast . unsignCast = id
   unsingCast . signCast = id

Note that one naive way to implement both these operations is simply to compute fromBitsLE . blastLE, i.e., first get all the bits of the word and then reconstruct in the target type. While this is semantically correct, it generates a lot of code (both during proofs via SMT-Lib, and when compiled to C). The goal of this class is to avoid that cost, so these operations can be compiled very efficiently, they will essentially become no-op's.

Minimal complete definition: All, no defaults.

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

x pDivMod 0 = (0, x)

for all x (including 0)

Minimal complete definition: pMult, pDivMod, showPolynomial

Compute CRCs over bit-vectors. The call crcBV n m p computes the CRC of the message m with respect to polynomial p. The inputs are assumed to be blasted big-endian. The number n specifies how many bits of CRC is needed. Note that n is actually the degree of the polynomial p, and thus it seems redundant to pass it in. However, in a typical proof context, the polynomial can be symbolic, so we cannot compute the degree easily. While this can be worked-around by generating code that accounts for all possible degrees, the resulting code would be unnecessarily big and complicated, and much harder to reason with. (Also note that a CRC is just the remainder from the polynomial division, but this routine is much faster in practice.)

NB. The nth bit of the polynomial p must be set for the CRC to be computed correctly. Note that the polynomial argument p will not even have this bit present most of the time, as it will typically contain bits 0 through n-1 as usual in the CRC literature. The higher order nth bit is simply assumed to be set, as it does not make sense to use a polynomial of a lesser degree. This is usually not a problem since CRC polynomials are designed and expressed this way.

NB. The literature on CRC's has many variants on how CRC's are computed. We follow the painless guide (http://www.ross.net/crc/download/crc_v3.txt) and compute the CRC as follows:

• Extend the message m by adding n 0 bits on the right
  • Divide the polynomial thus obtained by the p
  • The remainder is the CRC value.

There are many variants on final XOR's, reversed polynomials etc., so it is essential to double check you use the correct algorithm.

Compute CRC's over polynomials, i.e., symbolic words. The first Int argument plays the same role as the one in the crcBV function.

Symbolic conditionals are modeled by the Mergeable class, describing how to merge the results of an if-then-else call with a symbolic test. SBV provides all basic types as instances of this class, so users only need to declare instances for custom data-types of their programs as needed.

The function select is a total-indexing function out of a list of choices with a default value, simulating array/list indexing. It's an n-way generalization of the ite function.

Minimal complete definition: symbolicMerge

If-then-else. This is by definition symbolicMerge with both branches forced. This is typically the desired behavior, but also see iteLazy should you need more laziness.

A Lazy version of ite, which does not force its arguments. This might cause issues for symbolic simulation with large thunks around, so use with care.

Branch on a condition, much like ite. The exception is that SBV will check to make sure if the test condition is feasible by making an external call to the SMT solver. Note that this can be expensive, thus we shall use a time-out value (sBranchTimeOut). There might be zero, one, or two such external calls per sBranch call:

• If condition is statically known to be True/False: 0 calls
• In this case, we simply constant fold..
  • If condition is determined to be unsatisfiable : 1 call
  • In this case, we know then-branch is infeasible, so just take the else-branch
  • If condition is determined to be satisfable : 2 calls
  • In this case, we know then-branch is feasible, but we still have to check if the else-branch is

In summary, sBranch calls can be expensive, but they can help with the so-called symbolic-termination problem. See Data.SBV.Examples.Misc.SBranch for an example.

Symbolic assert. Check that the given boolean condition is always true in the given path. Otherwise symbolic simulation will stop with a run-time error.

Symbolic assert with a programmable continuation. Check that the given boolean condition is always true in the given path. Otherwise symbolic simulation will transfer the failing model to the given continuation. The continuation takes the SMTConfig, and a possible model: If it receives Nothing, then it means that the condition fails for all assignments to inputs. Otherwise, it'll receive Just a dictionary that maps the input variables to the appropriate CW values that exhibit the failure. Note that the continuation has no option but to display the result in some fashion and call error, due to its restricted type.

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: .==

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: .<

Symbolic Numbers. This is a simple class that simply incorporates all number like base types together, simplifying writing polymorphic type-signatures that work for all symbolic numbers, such as SWord8, SInt8 etc. For instance, we can write a generic list-minimum function as follows:

   mm :: SIntegral a => [SBV a] -> SBV a
   mm = foldr1 (a b -> ite (a .<= b) a b)

It is similar to the standard Integral class, except ranging over symbolic instances.

The SDivisible class captures the essence of division. Unfortunately we cannot use Haskell's Integral class since the Real and Enum superclasses are not implementable for symbolic bit-vectors. However, quotRem and divMod makes perfect sense, and the SDivisible 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 sQuotRem 0 = (0, x) x sDivMod 0 = (0, x)

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

NB. quot truncates toward zero, while div truncates toward negative infinity.

Minimal complete definition: sQuotRem, sDivMod

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.

Generalization of and

Generalization of or

Generalization of any

Generalization of all

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

Minimal complete definition: hexS and binS

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

Uninterpreted constants and functions. An uninterpreted constant is a value that is indexed by its name. The only property the prover assumes about these values are that they are equivalent to themselves; i.e., (for functions) they return the same results when applied to same arguments. We support uninterpreted-functions as a general means of black-box'ing operations that are irrelevant for the purposes of the proof; i.e., when the proofs can be performed without any knowledge about the function itself.

Minimal complete definition: sbvUninterpret. However, most instances in practice are already provided by SBV, so end-users should not need to define their own instances.

Add a user specified axiom to the generated SMT-Lib file. The first argument is a mere string, use for commenting purposes. The second argument is intended to hold the multiple-lines of the axiom text as expressed in SMT-Lib notation. Note that we perform no checks on the axiom itself, to see whether it's actually well-formed or is sensical by any means. A separate formalization of SMT-Lib would be very useful here.

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.

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.)

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

Prove a predicate, equivalent to proveWith defaultSMTCfg

Proves the predicate using the given SMT-solver

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

Check whether a given property is a theorem, with an optional time out and the given solver. Returns Nothing if times out, or the result wrapped in a Just otherwise.

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

Find a satisfying assignment using the given SMT-solver

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

Check whether a given property is satisfiable, with an optional time out and the given solver. Returns Nothing if times out, or the result wrapped in a Just otherwise.

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.

NB. Uninterpreted constant/function values and counter-examples for array values are ignored for the purposes of allSat. That is, only the satisfying assignments modulo uninterpreted functions and array inputs will be returned. This is due to the limitation of not having a robust means of getting a function counter-example back from the SMT solver.

Find all satisfying assignments using the given SMT-solver

Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing problems with constraints, like the following:

  do [x, y, z] <- sIntegers ["x", "y", "z"]
     solve [x .> 5, y + z .< x]

Adding arbitrary constraints. When adding constraints, one has to be careful about making sure they are not inconsistent. The function isVacuous can be use for this purpose. Here is an example. Consider the following predicate:

>>> let pred = do { x <- forall "x"; constrain $ x .< x; return $ x .>= (5 :: SWord8) }

This predicate asserts that all 8-bit values are larger than 5, subject to the constraint that the values considered satisfy x .< x, i.e., they are less than themselves. Since there are no values that satisfy this constraint, the proof will pass vacuously:

>>> prove pred
Q.E.D.

We can use isVacuous to make sure to see that the pass was vacuous:

>>> isVacuous pred
True

While the above example is trivial, things can get complicated if there are multiple constraints with non-straightforward relations; so if constraints are used one should make sure to check the predicate is not vacuously true. Here's an example that is not vacuous:

>>> let pred' = do { x <- forall "x"; constrain $ x .> 6; return $ x .>= (5 :: SWord8) }

This time the proof passes as expected:

>>> prove pred'
Q.E.D.

And the proof is not vacuous:

>>> isVacuous pred'
False

Adding a probabilistic constraint. The Double argument is the probability threshold. Probabilistic constraints are useful for genTest and quickCheck calls where we restrict our attention to interesting parts of the input domain.

Check if the given constraints are satisfiable, equivalent to isVacuousWith defaultSMTCfg. See the function constrain for an example use of isVacuous.

Determine if the constraints are vacuous using the given SMT-solver

Check if a given definition is safe; i.e., if all sAssert conditions can be proven to hold.

Check if a given definition is safe using the given solver configuration; i.e., if all sAssert conditions can be proven to hold.

Symbolically executable program fragments. This class is mainly used for safe calls, and is sufficently populated internally to cover most use cases. Users can extend it as they wish to allow safe checks for SBV programs that return/take types that are user-defined.

Prove a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.

Prove a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.

Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.

Find a satisfying assignment to a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.

Find all satisfying assignments to a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.

Find all satisfying assignments to a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.

Minimizes a cost function with respect to a constraint. Examples:

>>> minimize Quantified sum 3 (bAll (.> (10 :: SInteger)))
Just [11,11,11]

Maximizes a cost function with respect to a constraint. Examples:

>>> maximize Quantified sum 3 (bAll (.< (10 :: SInteger)))
Just [9,9,9]

Variant of optimizeWith using the default solver. See optimizeWith for parameter descriptions.

Variant of minimize allowing the use of a user specified solver. See optimizeWith for parameter descriptions.

Variant of maximize allowing the use of a user specified solver. See optimizeWith for parameter descriptions.

Symbolic optimization. Generalization on minimize and maximize that allows arbitrary cost functions and comparisons.

Given a symbolic computation that produces a value, compute the expected value that value would take if this computation is run with its free variables drawn from uniform distributions of its respective values, satisfying the given constraints specified by constrain and pConstrain calls. This is equivalent to calling expectedValueWith the following parameters: verbose, warm-up round count of 10000, no maximum iteration count, and with convergence margin 0.0001.

Generalized version of expectedValue, allowing the user to specify the warm-up count and the convergence factor. Maximum iteration count can also be specified, at which point convergence won't be sought. The boolean controls verbosity.

A prove call results in a ThmResult

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

An allSat call results in a AllSatResult. The boolean says whether we should warn the user about prefix-existentials.

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.)

The result of an sAssert call

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

Various SMT results that we can extract models out of.

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. The second argument is a tuple, where the first element indicates whether the model is alleged (i.e., if the solver is not sure, returing Unknown)

Return all the models from an allSat call, similar to extractModel but is suitable for the case of multiple results.

Get dictionaries from an all-sat call. Similar to getModelDictionary.

Extract value of a variable from an all-sat call. Similar to getModelValue.

Extract value of an uninterpreted variable from an all-sat call. Similar to getModelUninterpretedValue.

Solver configuration. See also z3, yices, cvc4, boolector, mathSAT, etc. which are instantiations of this type for those solvers, with reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as z3{verbose=True}.)

Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite precision value on the screen. The field printRealPrec controls the printing precision, by specifying the number of digits after the decimal point. The default value is 16, but it can be set to any positive integer.

When printing, SBV will add the suffix ... at the and of a real-value, if the given bound is not sufficient to represent the real-value exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation of the real value is not finite, i.e., if it is not rational.