-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Symbolic bit vectors: Bit-precise verification and automatic C-code generation.
--
-- Express properties about bit-precise Haskell programs and
-- automatically prove them using SMT solvers. Automatically generate C
-- programs from Haskell functions. The SBV library adds support for
-- symbolic bit vectors, allowing formal models of bit-precise programs
-- to be created.
--
--
-- $ 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 library introduces the following types and concepts:
--
--
-- - 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
-- - STree: Full binary trees of symbolic values (for fast
-- symbolic access)
-- - Symbolic polynomials over GF(2^n), and polynomial arithmetic
-- - Uninterpreted constants and functions over symbolic values, with
-- user defined SMT-Lib axioms
--
--
-- Predicates (i.e., functions that return SBool) built out of
-- these types can be:
--
--
-- - proven correct via an external SMT solver (the prove
-- function)
-- - checked for satisfiability (the sat and allSat
-- functions)
-- - quick-checked
--
--
-- The SBV library can also compile Haskell functions that manipulate
-- symbolic values directly to C, rendering them as straight-line C
-- programs.
--
-- In addition to the library, the installation will create the
-- executable SBVUnitTests. You should run it once the
-- installation is complete, to make sure the unit tests are run and all
-- is well.
--
-- SBV is hosted at GitHub: http://github.com/LeventErkok/sbv.
-- Comments, bug reports, and patches are always welcome.
--
-- The following people reported bugs, provided comments/feedback, or
-- contributed to the development of SBV in various ways: Ian Blumenfeld,
-- Ian Calvert, Iavor Diatchki, Lee Pike, Austin Seipp, Don Stewart,
-- Josef Svenningsson, and Nis Wegmann.
@package sbv
@version 0.9.21
-- | Low level functions to access the SBV infrastructure, for developers
-- who want to build further tools on top of SBV. End-users of the
-- library should not need to use this module.
module Data.SBV.Internals
-- | Result of running a symbolic computation
data Result
-- | Run a symbolic computation and return a Result
runSymbolic :: Symbolic a -> IO Result
-- | 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.
data SBV a
SBV :: !(Bool, Size) -> !Either CW (Cached SW) -> SBV a
class HasSignAndSize a
sizeOf :: HasSignAndSize a => a -> Size
hasSign :: HasSignAndSize a => a -> Bool
showType :: HasSignAndSize a => a -> String
-- | CW represents a concrete word of a fixed size: Endianness is
-- mostly irrelevant (see the FromBits class). For signed words,
-- the most significant digit is considered to be the sign
data CW
mkConstCW :: Integral a => (Bool, Size) -> a -> CW
genFree :: (Bool, Size) -> String -> Symbolic (SBV a)
genFree_ :: (Bool, Size) -> Symbolic (SBV a)
-- | Lower level version of compileToC, producing a
-- CgPgmBundle
compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle
-- | Lower level version of compileToCLib, producing a
-- CgPgmBundle
compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle
-- | Representation of a collection of generated programs.
newtype CgPgmBundle
CgPgmBundle :: [(FilePath, (CgPgmKind, [Doc]))] -> CgPgmBundle
-- | Different kinds of files we can produce. Currently this is
-- quite C specific.
data CgPgmKind
CgMakefile :: CgPgmKind
CgHeader :: [Doc] -> CgPgmKind
CgSource :: CgPgmKind
CgDriver :: CgPgmKind
-- | Create a gold file for the test case
generateGoldCheck :: FilePath -> Bool -> (forall a. Show a => IO a -> FilePath -> IO ())
-- | Checks that a particular result shows as s
showsAs :: Show a => a -> String -> Assertion
-- | Run an IO computation and check that it's result shows as s
ioShowsAs :: Show a => IO a -> String -> Assertion
-- | Wrap over SBVTestSuite, avoids exporting the constructor
mkTestSuite :: ((forall a. Show a => IO a -> FilePath -> IO ()) -> Test) -> SBVTestSuite
-- | A Test-suite, parameterized by the gold-check generator/checker
data SBVTestSuite
SBVTestSuite :: ((forall a. Show a => (IO a -> FilePath -> IO ())) -> Test) -> SBVTestSuite
-- | (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.
--
--
-- >>> prove $ \x -> x `shiftL` 2 .== 4 * (x :: SWord8)
-- Q.E.D.
--
--
--
-- >>> prove $ forAll ["x"] $ \x -> x `shiftL` 2 .== (x :: SWord8)
-- 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
-- - Uninterpreted constants and functions over symbolic values, with
-- user defined SMT-Lib axioms
--
--
-- 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"'.)
module Data.SBV
-- | A symbolic boolean/bit
type SBool = SBV Bool
-- | 8-bit unsigned symbolic value
type SWord8 = SBV Word8
-- | 16-bit unsigned symbolic value
type SWord16 = SBV Word16
-- | 32-bit unsigned symbolic value
type SWord32 = SBV Word32
-- | 64-bit unsigned symbolic value
type SWord64 = SBV Word64
-- | 8-bit signed symbolic value, 2's complement representation
type SInt8 = SBV Int8
-- | 16-bit signed symbolic value, 2's complement representation
type SInt16 = SBV Int16
-- | 32-bit signed symbolic value, 2's complement representation
type SInt32 = SBV Int32
-- | 64-bit signed symbolic value, 2's complement representation
type SInt64 = SBV Int64
-- | 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.
class SymArray array
newArray_ :: (SymArray array, HasSignAndSize a, HasSignAndSize b) => Maybe (SBV b) -> Symbolic (array a b)
newArray :: (SymArray array, HasSignAndSize a, HasSignAndSize b) => String -> Maybe (SBV b) -> Symbolic (array a b)
readArray :: SymArray array => array a b -> SBV a -> SBV b
resetArray :: (SymArray array, SymWord b) => array a b -> SBV b -> array a b
writeArray :: (SymArray array, SymWord b) => array a b -> SBV a -> SBV b -> array a b
mergeArrays :: (SymArray array, SymWord b) => SBV Bool -> array a b -> array a b -> array a b
-- | 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
--
data SArray a b
-- | 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
--
data SFunArray a b
-- | Lift a function to an array. Useful for creating arrays in a pure
-- context. (Otherwise use newArray.)
mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b
-- | 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.
type STree i e = STreeInternal (SBV i) (SBV e)
-- | Reading a value. We bit-blast the index and descend down the full tree
-- according to bit-values.
readSTree :: (Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e
-- | Writing a value, similar to how reads are done. The important thing is
-- that the tree representation keeps updates to a minimum.
writeSTree :: (Mergeable (SBV e), Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e
-- | Construct the fully balanced initial tree using the given values
mkSTree :: HasSignAndSize i => [SBV e] -> STree i e
-- | 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.
bitValue :: (Bits a, SymWord a) => SBV a -> Int -> SBool
-- | 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
setBitTo :: (Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV a
-- | Returns 1 if the boolean is true, otherwise 0
oneIf :: (Num a, SymWord a) => SBool -> SBV a
-- | Least significant bit of a word, always stored at index 0
lsb :: (Bits a, SymWord a) => SBV a -> SBool
-- | Most significant bit of a word, always stored at the last position
msb :: (Bits a, SymWord a) => SBV a -> SBool
-- | Returns (symbolic) true if all the elements of the given list are the
-- same
allEqual :: (Eq a, SymWord a) => [SBV a] -> SBool
-- | Returns (symbolic) true if all the elements of the given list are
-- different
allDifferent :: (Eq a, SymWord a) => [SBV a] -> SBool
-- | Big-endian blasting of a word into its bits. Also see the
-- FromBits class
blastBE :: (Bits a, SymWord a) => SBV a -> [SBool]
-- | Little-endian blasting of a word into its bits. Also see the
-- FromBits class
blastLE :: (Bits a, SymWord a) => SBV a -> [SBool]
-- | 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
class FromBits a
fromBitsLE :: FromBits a => [SBool] -> a
fromBitsBE :: FromBits a => [SBool] -> a
-- | 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.
class Splittable a b | b -> a
split :: Splittable a b => a -> (b, b)
(#) :: Splittable a b => b -> b -> a
extend :: Splittable a b => b -> a
-- | 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.
class SignCast a b | a -> b, b -> a
signCast :: SignCast a b => a -> b
unsignCast :: SignCast a b => b -> a
-- | 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
class Bits a => Polynomial a
polynomial :: Polynomial a => [Int] -> a
pAdd :: Polynomial a => a -> a -> a
pMult :: Polynomial a => (a, a, [Int]) -> a
pDiv :: Polynomial a => a -> a -> a
pMod :: Polynomial a => a -> a -> a
pDivMod :: Polynomial a => a -> a -> (a, a)
showPoly :: Polynomial a => a -> String
-- | Symbolic choice operator, parameterized via a class select is a
-- total-indexing function, with the default.
--
-- Minimal complete definition: symbolicMerge
class Mergeable a
symbolicMerge :: Mergeable a => SBool -> a -> a -> a
ite :: Mergeable a => SBool -> a -> a -> a
select :: (Mergeable a, Bits b, SymWord b, Integral b) => [a] -> a -> SBV b -> a
-- | 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: .==
class EqSymbolic a
(.==) :: EqSymbolic a => a -> a -> SBool
(./=) :: EqSymbolic a => a -> a -> SBool
-- | 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: .<
class (Mergeable a, EqSymbolic a) => OrdSymbolic a
(.<) :: OrdSymbolic a => a -> a -> SBool
(.>=) :: OrdSymbolic a => a -> a -> SBool
(.>) :: OrdSymbolic a => a -> a -> SBool
(.<=) :: OrdSymbolic a => a -> a -> SBool
smin :: OrdSymbolic a => a -> a -> a
smax :: OrdSymbolic a => a -> a -> a
-- | 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
class BVDivisible a
bvQuotRem :: BVDivisible a => a -> a -> (a, a)
-- | 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.
class Boolean b
true :: Boolean b => b
false :: Boolean b => b
bnot :: Boolean b => b -> b
(&&&) :: Boolean b => b -> b -> b
(|||) :: Boolean b => b -> b -> b
(~&) :: Boolean b => b -> b -> b
(~|) :: Boolean b => b -> b -> b
(<+>) :: Boolean b => b -> b -> b
(==>) :: Boolean b => b -> b -> b
(<=>) :: Boolean b => b -> b -> b
fromBool :: Boolean b => Bool -> b
-- | Generalization of and
bAnd :: Boolean b => [b] -> b
-- | Generalization of or
bOr :: Boolean b => [b] -> b
-- | Generalization of any
bAny :: Boolean b => (a -> b) -> [a] -> b
-- | Generalization of all
bAll :: Boolean b => (a -> b) -> [a] -> b
-- | PrettyNum class captures printing of numbers in hex and binary
-- formats; also supporting negative numbers.
--
-- Minimal complete definition: hexS and binS
class PrettyNum a
hexS :: PrettyNum a => a -> String
binS :: PrettyNum a => a -> String
hex :: PrettyNum a => a -> String
bin :: PrettyNum a => a -> String
-- | A more convenient interface for reading binary numbers, also supports
-- negative numbers
readBin :: Num a => String -> a
-- | 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: uninterpretWithHandle. However,
-- most instances in practice are already provided by SBV, so end-users
-- should not need to define their own instances.
class Uninterpreted a
uninterpret :: Uninterpreted a => String -> a
uninterpretWithHandle :: Uninterpreted a => String -> (SBVUF, a)
-- | An uninterpreted function handle. This is the handle to be used for
-- adding axioms about uninterpreted constants/functions. Note that we
-- will leave this abstract for safety purposes
data SBVUF
-- | Get the name associated with the uninterpreted-value; useful when
-- constructing axioms about this UI.
sbvUFName :: SBVUF -> String
-- | Add a user specified axiom to the generated SMT-Lib file. Note that
-- the input is a mere string; we perform no checking on the input that
-- it's well-formed or is sensical. A separate formalization of SMT-Lib
-- would be very useful here.
addAxiom :: String -> [String] -> Symbolic ()
-- | 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.
type Predicate = Symbolic SBool
-- | 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.)
class Provable a
forAll_ :: Provable a => a -> Predicate
forAll :: Provable a => [String] -> a -> Predicate
-- | Equality as a proof method. Allows for very concise construction of
-- equivalence proofs, which is very typical in bit-precise proofs.
class Equality a
(===) :: Equality a => a -> a -> IO ThmResult
-- | Prove a predicate, equivalent to proveWith
-- defaultSMTCfg
prove :: Provable a => a -> IO ThmResult
-- | Proves the predicate using the given SMT-solver
proveWith :: Provable a => SMTConfig -> a -> IO ThmResult
-- | Checks theoremhood
isTheorem :: Provable a => a -> IO Bool
-- | Checks theoremhood within the given time limit of i seconds.
-- Returns Nothing if times out, or the result wrapped in a
-- Just otherwise.
isTheoremWithin :: Provable a => Int -> a -> IO (Maybe Bool)
-- | Find a satisfying assignment for a predicate, equivalent to
-- satWith defaultSMTCfg
sat :: Provable a => a -> IO SatResult
-- | Find a satisfying assignment using the given SMT-solver
satWith :: Provable a => SMTConfig -> a -> IO SatResult
-- | Checks satisfiability
isSatisfiable :: Provable a => a -> IO Bool
-- | Checks satisfiability within the given time limit of i
-- seconds. Returns Nothing if times out, or the result wrapped
-- in a Just otherwise.
isSatisfiableWithin :: Provable a => Int -> a -> IO (Maybe Bool)
-- | 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.
allSat :: Provable a => a -> IO AllSatResult
-- | Find all satisfying assignments using the given SMT-solver
allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResult
-- | 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.
numberOfModels :: Provable a => a -> IO Int
-- | A prove call results in a ThmResult
newtype ThmResult
ThmResult :: SMTResult -> ThmResult
-- | A sat call results in a SatResult The reason for
-- having a separate SatResult is to have a more meaningful
-- Show instance.
newtype SatResult
SatResult :: SMTResult -> SatResult
-- | An allSat call results in a AllSatResult
newtype AllSatResult
AllSatResult :: [SMTResult] -> AllSatResult
-- | 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.)
data SMTResult
-- | Unsatisfiable
Unsatisfiable :: SMTConfig -> SMTResult
-- | Satisfiable with model
Satisfiable :: SMTConfig -> SMTModel -> SMTResult
-- | Prover returned unknown, with a potential (possibly bogus) model
Unknown :: SMTConfig -> SMTModel -> SMTResult
-- | Prover errored out
ProofError :: SMTConfig -> [String] -> SMTResult
-- | Computation timed out (see the timeout combinator)
TimeOut :: SMTConfig -> SMTResult
-- | 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
class SatModel a
parseCWs :: SatModel a => [CW] -> Maybe (a, [CW])
cvtModel :: SatModel a => (a -> Maybe b) -> Maybe (a, [CW]) -> Maybe (b, [CW])
-- | Given an SMTResult, extract an arbitrarily typed model from it,
-- given a SatModel instance
getModel :: SatModel a => SMTResult -> a
-- | 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.
displayModels :: SatModel a => (Int -> a -> IO ()) -> AllSatResult -> IO Int
-- | Solver configuration
data SMTConfig
SMTConfig :: Bool -> Bool -> Int -> SMTSolver -> SMTConfig
-- | Debug mode
verbose :: SMTConfig -> Bool
-- | Print timing information on how long different phases took
-- (construction, solving, etc.)
timing :: SMTConfig -> Bool
-- | Print literals in this base
printBase :: SMTConfig -> Int
-- | The actual SMT solver
solver :: SMTConfig -> SMTSolver
-- | An SMT solver
data SMTSolver
SMTSolver :: String -> String -> [String] -> SMTEngine -> SMTSolver
-- | Printable name of the solver
name :: SMTSolver -> String
-- | The path to its executable
executable :: SMTSolver -> String
-- | Options to provide to the solver
options :: SMTSolver -> [String]
-- | The solver engine, responsible for interpreting solver output
engine :: SMTSolver -> SMTEngine
-- | Default configuration for the SMT solver. Non-verbose, non-timing,
-- prints results in base 10, and uses the Yices SMT solver.
defaultSMTCfg :: SMTConfig
-- | Same as defaultSMTCfg, except verbose
verboseSMTCfg :: SMTConfig
-- | Same as defaultSMTCfg, except prints timing info
timingSMTCfg :: SMTConfig
-- | Same as defaultSMTCfg, except both verbose and timing info
verboseTimingSMTCfg :: SMTConfig
-- | Adds a time out of n seconds to a given solver configuration
timeout :: Int -> SMTConfig -> SMTConfig
-- | 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.
yices :: SMTSolver
-- | 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.
data Symbolic a
output :: Outputtable a => a -> Symbolic a
-- | 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.
--
-- Minimal complete definiton: free, free_, literal, fromCW
class (Bounded a, Ord a) => SymWord a
free :: SymWord a => String -> Symbolic (SBV a)
free_ :: SymWord a => Symbolic (SBV a)
mkFreeVars :: SymWord a => Int -> Symbolic [SBV a]
literal :: SymWord a => a -> SBV a
unliteral :: SymWord a => SBV a -> Maybe a
fromCW :: SymWord a => CW -> a
isConcrete :: SymWord a => SBV a -> Bool
isSymbolic :: SymWord a => SBV a -> Bool
isConcretely :: SymWord a => SBV a -> (a -> Bool) -> Bool
-- | Compiles to SMT-Lib and returns the resulting program as a string.
-- Useful for saving the result to a file for off-line analysis, for
-- instance if you have an SMT solver that's not natively supported
-- out-of-the box by the SBV library.
compileToSMTLib :: Provable a => a -> IO String
-- | The code-generation monad. Allows for precise layout of input values
-- reference parameters (for returning composite values in languages such
-- as C), and return values.
data SBVCodeGen a
-- | Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large
-- value etc. on/off.
cgPerformRTCs :: Bool -> SBVCodeGen ()
-- | Sets driver program run time values, useful for generating programs
-- with fixed drivers for testing.
cgSetDriverValues :: [Integer] -> SBVCodeGen ()
-- | Creates an atomic input in the generated code.
cgInput :: (HasSignAndSize a, SymWord a) => String -> SBVCodeGen (SBV a)
-- | Creates an array input in the generated code.
cgInputArr :: (HasSignAndSize a, SymWord a) => Int -> String -> SBVCodeGen [SBV a]
-- | Creates an atomic output in the generated code.
cgOutput :: (HasSignAndSize a, SymWord a) => String -> SBV a -> SBVCodeGen ()
-- | Creates an array output in the generated code.
cgOutputArr :: (HasSignAndSize a, SymWord a) => String -> [SBV a] -> SBVCodeGen ()
-- | Creates a returned (unnamed) value in the generated code.
cgReturn :: (HasSignAndSize a, SymWord a) => SBV a -> SBVCodeGen ()
-- | Creates a returned (unnamed) array value in the generated code.
cgReturnArr :: (HasSignAndSize a, SymWord a) => [SBV a] -> SBVCodeGen ()
-- | Given a symbolic computation, render it as an equivalent collection of
-- files that make up a C program:
--
--
-- - The first argument is the directory name under which the files
-- will be saved. To save files in the current directory pass
-- Just ".". Use Nothing for printing to
-- stdout.
-- - The second argument is the name of the C function to
-- generate.
-- - The final argument is the function to be compiled.
--
--
-- Compilation will also generate a Makefile, a header file, and
-- a driver (test) program, etc.
compileToC :: Maybe FilePath -> String -> SBVCodeGen () -> IO ()
-- | Create code to generate a library archive (.a) from given symbolic
-- functions. Useful when generating code from multiple functions that
-- work together as a library.
--
--
-- - The first argument is the directory name under which the files
-- will be saved. To save files in the current directory pass
-- Just ".". Use Nothing for printing to
-- stdout.
-- - The second argument is the name of the archive to generate.
-- - The third argument is the list of functions to include, in the
-- form of function-name/code pairs, similar to the second and third
-- arguments of compileToC, except in a list.
--
compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen ())] -> IO ()
-- | Checks the correctness of a few tricks from the large collection found
-- in: http://graphics.stanford.edu/~seander/bithacks.html
module Data.SBV.Examples.BitPrecise.BitTricks
-- | Formalizes
-- http://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax
fastMinCorrect :: SInt32 -> SInt32 -> SBool
-- | Formalizes
-- http://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax
fastMaxCorrect :: SInt32 -> SInt32 -> SBool
-- | Formalizes
-- http://graphics.stanford.edu/~seander/bithacks.html#DetectOppositeSigns
oppositeSignsCorrect :: SInt32 -> SInt32 -> SBool
-- | Formalizes
-- http://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching
conditionalSetClearCorrect :: SBool -> SWord32 -> SWord32 -> SBool
-- | Formalizes
-- http://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2
powerOfTwoCorrect :: SWord32 -> SBool
-- | Collection of queries
queries :: IO ()
-- | An encoding and correctness proof of Legato's multiplier in Haskell.
-- Bill Legato came up with an interesting way to multiply two 8-bit
-- numbers on Mostek, as described here:
-- http://www.cs.utexas.edu/~moore/acl2/workshop-2004/contrib/legato/Weakest-Preconditions-Report.pdf
--
-- Here's Legato's algorithm, as coded in Mostek assembly:
--
--
-- step1 : LDX #8 ; load X immediate with the integer 8
-- step2 : LDA #0 ; load A immediate with the integer 0
-- step3 : LOOP ROR F1 ; rotate F1 right circular through C
-- step4 : BCC ZCOEF ; branch to ZCOEF if C = 0
-- step5 : CLC ; set C to 0
-- step6 : ADC F2 ; set A to A+F2+C and C to the carry
-- step7 : ZCOEF ROR A ; rotate A right circular through C
-- step8 : ROR LOW ; rotate LOW right circular through C
-- step9 : DEX ; set X to X-1
-- step10: BNE LOOP ; branch to LOOP if Z = 0
--
--
-- This program came to be known as the Legato's challenge in the
-- community, where the challenge was to prove that it indeed does
-- perform multiplication. This file formalizes the Mostek architecture
-- in Haskell and proves that Legato's algorithm is indeed correct.
module Data.SBV.Examples.BitPrecise.Legato
-- | The memory is addressed by 32-bit words.
type Address = SWord32
-- | We model only two registers of Mostek that is used in the above
-- algorithm, can add more.
data Register
RegX :: Register
RegA :: Register
-- | The carry flag (FlagC) and the zero flag (FlagZ)
data Flag
FlagC :: Flag
FlagZ :: Flag
-- | Mostek was an 8-bit machine.
type Value = SWord8
-- | Convenient synonym for symbolic machine bits.
type Bit = SBool
-- | Register bank
type Registers = Array Register Value
-- | Flag bank
type Flags = Array Flag Bit
-- | The memory maps 32-bit words to 8-bit words. (The Model
-- data-type is defined later, depending on the verification model used.)
type Memory = Model Word32 Word8
-- | Abstraction of the machine: The CPU consists of memory, registers, and
-- flags. Unlike traditional hardware, we assume the program is stored in
-- some other memory area that we need not model. (No self modifying
-- programs!)
data Mostek
Mostek :: Memory -> Registers -> Flags -> Mostek
memory :: Mostek -> Memory
registers :: Mostek -> Registers
flags :: Mostek -> Flags
-- | Given a machine state, compute a value out of it
type Extract a = Mostek -> a
-- | Programs are essentially state transformers (on the machine state)
type Program = Mostek -> Mostek
-- | Get the value of a given register
getReg :: Register -> Extract Value
-- | Set the value of a given register
setReg :: Register -> Value -> Program
-- | Get the value of a flag
getFlag :: Flag -> Extract Bit
-- | Set the value of a flag
setFlag :: Flag -> Bit -> Program
-- | Read memory
peek :: Address -> Extract Value
-- | Write to memory
poke :: Address -> Value -> Program
-- | Checking overflow. In Legato's multipler the ADC instruction
-- needs to see if the expression x + y + c overflowed, as checked by
-- this function. Note that we verify the correctness of this check
-- separately below in checkOverflowCorrect.
checkOverflow :: SWord8 -> SWord8 -> SBool -> SBool
-- | Correctness theorem for our checkOverflow implementation.
--
-- We have:
--
--
-- >>> checkOverflowCorrect
-- Q.E.D.
--
checkOverflowCorrect :: IO ThmResult
-- | An instruction is modeled as a Program transformer. We model
-- mostek programs in direct continuation passing style.
type Instruction = Program -> Program
-- | LDX: Set register X to value v
ldx :: Value -> Instruction
-- | LDA: Set register A to value v
lda :: Value -> Instruction
-- | CLC: Clear the carry flag
clc :: Instruction
-- | ROR, memory version: Rotate the value at memory location a to
-- the right by 1 bit, using the carry flag as a transfer position. That
-- is, the final bit of the memory location becomes the new carry and the
-- carry moves over to the first bit. This very instruction is one of the
-- reasons why Legato's multiplier is quite hard to understand and is
-- typically presented as a verification challenge.
rorM :: Address -> Instruction
-- | ROR, register version: Same as rorM, except through register
-- r.
rorR :: Register -> Instruction
-- | BCC: branch to label l if the carry flag is false
bcc :: Program -> Instruction
-- | ADC: Increment the value of register A by the value of memory
-- contents at address a, using the carry-bit as the carry-in
-- for the addition.
adc :: Address -> Instruction
-- | DEX: Decrement the value of register X
dex :: Instruction
-- | BNE: Branch if the zero-flag is false
bne :: Program -> Instruction
-- | The end combinator stops our program, providing the
-- final continuation that does nothing.
end :: Program
-- | Parameterized by the addresses of locations of the factors
-- (F1 and F2), the following program multiplies them,
-- storing the low-byte of the result in the memory location
-- lowAddr, and the high-byte in register A. The
-- implementation is a direct transliteration of Legato's algorithm given
-- at the top, using our notation.
legato :: Address -> Address -> Address -> Program
-- | Given address/value pairs for F1 and F2, and the location of where the
-- low-byte of the result should go, runLegato takes an
-- arbitrary machine state m and returns the high and low bytes
-- of the multiplication.
runLegato :: (Address, Value) -> (Address, Value) -> Address -> Mostek -> (Value, Value)
-- | Helper synonym for capturing relevant bits of Mostek
type InitVals = (Value, Value, Value, Bit, Bit)
-- | Create an instance of the Mostek machine, initialized by the memory
-- and the relevant values of the registers and the flags
initMachine :: Memory -> InitVals -> Mostek
-- | The correctness theorem. For all possible memory configurations, the
-- factors (x and y below), the location of the
-- low-byte result and the initial-values of registers and the flags,
-- this function will return True only if running Legato's algorithm does
-- indeed compute the product of x and y correctly.
legatoIsCorrect :: Memory -> (Address, Value) -> (Address, Value) -> Address -> InitVals -> SBool
-- | Choose the appropriate array model to be used for modeling the memory.
-- (See Memory.) The SFunArray is the function based model.
-- SArray is the SMT-Lib array's based model.
type Model = SFunArray
-- | The correctness theorem. On a decent MacBook Pro, this proof takes
-- about 3 minutes with the SFunArray memory model and about 30
-- minutes with the SArray model.
correctnessTheorem :: IO ThmResult
-- | Generate a C program that implements Legato's algorithm automatically.
legatoInC :: IO ()
instance Eq Register
instance Ord Register
instance Ix Register
instance Bounded Register
instance Enum Register
instance Eq Flag
instance Ord Flag
instance Ix Flag
instance Bounded Flag
instance Enum Flag
instance Mergeable Mostek
-- | The PrefixSum algorithm over power-lists and proof of the
-- Ladner-Fischer implementation. See
-- http://www.cs.utexas.edu/users/psp/powerlist.pdf and
-- http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf.
module Data.SBV.Examples.BitPrecise.PrefixSum
-- | A poor man's representation of powerlists and basic operations on
-- them: http://www.cs.utexas.edu/users/psp/powerlist.pdf. We
-- merely represent power-lists by ordinary lists.
type PowerList a = [a]
-- | The tie operator, concatenation.
tiePL :: PowerList a -> PowerList a -> PowerList a
-- | The zip operator, zips the power-lists of the same size, returns a
-- powerlist of double the size.
zipPL :: PowerList a -> PowerList a -> PowerList a
-- | Inverse of zipping.
unzipPL :: PowerList a -> (PowerList a, PowerList a)
-- | Reference prefix sum (ps) is simply Haskell's scanl1
-- function.
ps :: (a, a -> a -> a) -> PowerList a -> PowerList a
-- | The Ladner-Fischer (lf) implementation of prefix-sum. See
-- http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf
-- or pg. 16 of http://www.cs.utexas.edu/users/psp/powerlist.pdf.
lf :: (a, a -> a -> a) -> PowerList a -> PowerList a
-- | Correctness theorem, for a powerlist of given size, an associative
-- operator, and its left-unit element.
flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Bits a) => (a, a -> a -> a)) -> Symbolic SBool
-- | Proves Ladner-Fischer is equivalent to reference specification for
-- addition. 0 is the left-unit element, and we use a power-list
-- of size 8.
thm1 :: IO ThmResult
-- | Proves Ladner-Fischer is equivalent to reference specification for the
-- function max. 0 is the left-unit element, and we use
-- a power-list of size 16.
thm2 :: IO ThmResult
-- | Try proving correctness for an arbitrary operator. This proof will
-- not go through since the SMT solver does not know that the
-- operator associative and has the given left-unit element. We have:
--
--
-- >>> thm3
-- Falsifiable. Counter-example:
-- s0 = 0 :: SWord32
-- s1 = 0 :: SWord32
-- s2 = 0 :: SWord32
-- s3 = 0 :: SWord32
-- s4 = 0 :: SWord32
-- s5 = 0 :: SWord32
-- s6 = 0 :: SWord32
-- s7 = 3221225472 :: SWord32
-- -- uninterpreted: u
-- u = 0
-- -- uninterpreted: flOp
-- flOp 0 3221225472 = 2147483648
-- flOp 0 2147483648 = 3758096384
-- flOp _ _ = 0
--
--
-- You can verify that the above function for flOp is not
-- associative:
--
--
-- ghci> flOp 3221225472 (flOp 2147483648 3221225472)
-- 0
-- ghci> flOp (flOp 3221225472 2147483648) 3221225472
-- 2147483648
--
--
-- Also, the unit 0 is clearly not a left-unit for
-- flOp, as the third equation for flOp will simply map
-- many elements to 0.
thm3 :: IO ThmResult
-- | Generate an instance of the prefix-sum problem for an arbitrary
-- operator, by telling the SMT solver the necessary axioms for
-- associativity and left-unit. The first argument states how wide the
-- power list should be.
genPrefixSumInstance :: Int -> Symbolic SBool
-- | Prove the generic problem for powerlists of given sizes. Note that
-- this will only work for Yices-1. This is due to the fact that Yices-2
-- follows the SMT-Lib standard and does not accept bit-vector problems
-- with quantified axioms in them, while Yices-1 did allow for that. The
-- crux of the problem is that there are no SMT-Lib logics that combine
-- BV's and quantifiers, see:
-- http://goedel.cs.uiowa.edu/smtlib/logics.html. So we are stuck
-- until new powerful logics are added to SMT-Lib.
--
-- Here, we explicitly tell SBV to use Yices-1 that did not have that
-- limitation. Tweak the executable location accordingly below for your
-- platform..
--
-- We have:
--
--
-- >>> prefixSum 2
-- Q.E.D.
--
--
--
-- >>> prefixSum 4
-- Q.E.D.
--
--
-- Note that these proofs tend to run long. Also, Yices ran out of memory
-- and crashed on my box when I tried for size 8, after running
-- for about 2.5 minutes..
prefixSum :: Int -> IO ThmResult
-- | A symbolic trace can help illustrate the action of Ladner-Fischer.
-- This generator produces the actions of Ladner-Fischer for addition,
-- showing how the computation proceeds:
--
--
-- >>> ladnerFischerTrace 8
-- INPUTS
-- s0 :: SWord8
-- s1 :: SWord8
-- s2 :: SWord8
-- s3 :: SWord8
-- s4 :: SWord8
-- s5 :: SWord8
-- s6 :: SWord8
-- s7 :: SWord8
-- CONSTANTS
-- s_2 = False
-- s_1 = True
-- TABLES
-- ARRAYS
-- UNINTERPRETED CONSTANTS
-- AXIOMS
-- DEFINE
-- s8 :: SWord8 = s0 + s1
-- s9 :: SWord8 = s2 + s8
-- s10 :: SWord8 = s2 + s3
-- s11 :: SWord8 = s8 + s10
-- s12 :: SWord8 = s4 + s11
-- s13 :: SWord8 = s4 + s5
-- s14 :: SWord8 = s11 + s13
-- s15 :: SWord8 = s6 + s14
-- s16 :: SWord8 = s6 + s7
-- s17 :: SWord8 = s13 + s16
-- s18 :: SWord8 = s11 + s17
-- OUTPUTS
-- s0
-- s8
-- s9
-- s11
-- s12
-- s14
-- s15
-- s18
--
ladnerFischerTrace :: Int -> IO ()
-- | Trace generator for the reference spec. It clearly demonstrates that
-- the reference implementation fewer operations, but is not
-- parallelizable at all:
--
--
-- >>> scanlTrace 8
-- INPUTS
-- s0 :: SWord8
-- s1 :: SWord8
-- s2 :: SWord8
-- s3 :: SWord8
-- s4 :: SWord8
-- s5 :: SWord8
-- s6 :: SWord8
-- s7 :: SWord8
-- CONSTANTS
-- s_2 = False
-- s_1 = True
-- TABLES
-- ARRAYS
-- UNINTERPRETED CONSTANTS
-- AXIOMS
-- DEFINE
-- s8 :: SWord8 = s0 + s1
-- s9 :: SWord8 = s2 + s8
-- s10 :: SWord8 = s3 + s9
-- s11 :: SWord8 = s4 + s10
-- s12 :: SWord8 = s5 + s11
-- s13 :: SWord8 = s6 + s12
-- s14 :: SWord8 = s7 + s13
-- OUTPUTS
-- s0
-- s8
-- s9
-- s10
-- s11
-- s12
-- s13
-- s14
--
scanlTrace :: Int -> IO ()
-- | Simple code generation example.
module Data.SBV.Examples.CodeGeneration.AddSub
-- | Simple function that returns add/sum of args
addSub :: SWord8 -> SWord8 -> (SWord8, SWord8)
-- | Generate C code for addSub. This will place the files in a directory
-- called genAddSub, generating the following files:
--
-- File: Makefile
--
--
-- # Makefile for addSub. Automatically generated by SBV. Do not edit!
--
-- # include any user-defined .mk file in the current directory.
-- -include *.mk
--
-- CC=gcc
-- CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
--
-- all: addSub_driver
--
-- addSub.o: addSub.c addSub.h
-- ${CC} ${CCFLAGS} -c $< -o $@
--
-- addSub_driver.o: addSub_driver.c
-- ${CC} ${CCFLAGS} -c $< -o $@
--
-- addSub_driver: addSub.o addSub_driver.o
-- ${CC} ${CCFLAGS} $^ -o $@
--
-- clean:
-- rm -f *.o
--
-- veryclean: clean
-- rm -f addSub_driver
--
--
-- File: addSub.h
--
--
-- /* Header file for addSub. Automatically generated by SBV. Do not edit! */
--
-- #ifndef __addSub__HEADER_INCLUDED__
-- #define __addSub__HEADER_INCLUDED__
--
-- #include <inttypes.h>
-- #include <stdint.h>
--
-- /* Unsigned bit-vectors */
-- typedef uint8_t SBool ;
-- typedef uint8_t SWord8 ;
-- typedef uint16_t SWord16;
-- typedef uint32_t SWord32;
-- typedef uint64_t SWord64;
--
-- /* Signed bit-vectors */
-- typedef int8_t SInt8 ;
-- typedef int16_t SInt16;
-- typedef int32_t SInt32;
-- typedef int64_t SInt64;
--
-- /* Entry point prototype: */
-- void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,
-- SWord8 *dif);
--
-- #endif /* __addSub__HEADER_INCLUDED__ */
--
--
-- File: addSub.c
--
--
-- /* File: "addSub.c". Automatically generated by SBV. Do not edit! */
--
-- #include <inttypes.h>
-- #include <stdint.h>
-- #include "addSub.h"
--
-- void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,
-- SWord8 *dif)
-- {
-- const SWord8 s0 = x;
-- const SWord8 s1 = y;
-- const SWord8 s2 = s0 + s1;
-- const SWord8 s3 = s0 - s1;
--
-- *sum = s2;
-- *dif = s3;
-- }
--
--
-- File: addSub_driver.c
--
--
-- /* Example driver program for addSub. */
-- /* Automatically generated by SBV. Edit as you see fit! */
--
-- #include <inttypes.h>
-- #include <stdint.h>
-- #include <stdio.h>
-- #include "addSub.h"
--
-- int main(void)
-- {
-- SWord8 sum;
-- SWord8 dif;
--
-- addSub(132, 241, &sum, &dif);
--
-- printf("addSub(132, 241, &sum, &dif) ->\n");
-- printf(" sum = %"PRIu8"\n", sum);
-- printf(" dif = %"PRIu8"\n", dif);
--
-- return 0;
-- }
--
genAddSub :: IO ()
-- | Computing Fibonacci numbers and generating C code. Inspired by Lee
-- Pike's original implementation, modified for inclusion in the package.
-- It illustrates symbolic termination issues one can have when working
-- with recursive algorithms and how to deal with such, eventually
-- generating good C code.
module Data.SBV.Examples.CodeGeneration.Fibonacci
-- | This is a naive implementation of fibonacci, and will work fine
-- (albeit slow) for concrete inputs:
--
--
-- >>> map fib0 [0..6]
-- [0 :: SWord64,1 :: SWord64,1 :: SWord64,2 :: SWord64,3 :: SWord64,5 :: SWord64,8 :: SWord64]
--
--
-- However, it is not suitable for doing proofs or generating code, as it
-- is not symbolically terminating when it is called with a symbolic
-- value n. When we recursively call fib0 on
-- n-1 (or n-2), the test against 0 will
-- always explore both branches since the result will be symbolic, hence
-- will not terminate. (An integrated theorem prover can establish
-- termination after a certain number of unrollings, but this would be
-- quite expensive to implement, and would be impractical.)
fib0 :: SWord64 -> SWord64
-- | The recursion-depth limited version of fibonacci. Limiting the maximum
-- number to be 20, we can say:
--
--
-- >>> map (fib1 20) [0..6]
-- [0 :: SWord64,1 :: SWord64,1 :: SWord64,2 :: SWord64,3 :: SWord64,5 :: SWord64,8 :: SWord64]
--
--
-- The function will work correctly, so long as the index we query is at
-- most top, and otherwise will return the value at
-- top. Note that we also use accumulating parameters here for
-- efficiency, although this is orthogonal to the termination concern.
--
-- A note on modular arithmetic: The 64-bit word we use to represent the
-- values will of course eventually overflow, beware! Fibonacci is a fast
-- growing function..
fib1 :: SWord64 -> SWord64 -> SWord64
-- | We can generate code for fib1 using the genFib1 action.
-- Note that the generated code will grow larger as we pick larger values
-- of top, but only linearly, thanks to the accumulating
-- parameter trick used by fib1. The following is an excerpt from
-- the code generated for the call genFib1 10, where the code
-- will work correctly for indexes up to 10:
--
--
-- SWord64 fib1(const SWord64 x)
-- {
-- const SWord64 s0 = x;
-- const SBool s2 = s0 == 0x0000000000000000ULL;
-- const SBool s4 = s0 == 0x0000000000000001ULL;
-- const SBool s6 = s0 == 0x0000000000000002ULL;
-- const SBool s8 = s0 == 0x0000000000000003ULL;
-- const SBool s10 = s0 == 0x0000000000000004ULL;
-- const SBool s12 = s0 == 0x0000000000000005ULL;
-- const SBool s14 = s0 == 0x0000000000000006ULL;
-- const SBool s17 = s0 == 0x0000000000000007ULL;
-- const SBool s19 = s0 == 0x0000000000000008ULL;
-- const SBool s22 = s0 == 0x0000000000000009ULL;
-- const SWord64 s25 = s22 ? 0x0000000000000022ULL : 0x0000000000000037ULL;
-- const SWord64 s26 = s19 ? 0x0000000000000015ULL : s25;
-- const SWord64 s27 = s17 ? 0x000000000000000dULL : s26;
-- const SWord64 s28 = s14 ? 0x0000000000000008ULL : s27;
-- const SWord64 s29 = s12 ? 0x0000000000000005ULL : s28;
-- const SWord64 s30 = s10 ? 0x0000000000000003ULL : s29;
-- const SWord64 s31 = s8 ? 0x0000000000000002ULL : s30;
-- const SWord64 s32 = s6 ? 0x0000000000000001ULL : s31;
-- const SWord64 s33 = s4 ? 0x0000000000000001ULL : s32;
-- const SWord64 s34 = s2 ? 0x0000000000000000ULL : s33;
--
-- return s34;
-- }
--
genFib1 :: SWord64 -> IO ()
-- | Compute the fibonacci numbers statically at code-generation
-- time and put them in a table, accessed by the select call.
fib2 :: SWord64 -> SWord64 -> SWord64
-- | Once we have fib2, we can generate the C code
-- straightforwardly. Below is an excerpt from the code that SBV
-- generates for the call genFib2 64. Note that this code is a
-- constant-time look-up table implementation of fibonacci, with no
-- run-time overhead. The index can be made arbitrarily large, naturally.
-- (Note that this function returns 0 if the index is larger
-- than 64, as specified by the call to select with default
-- 0.)
--
--
-- SWord64 fibLookup(const SWord64 x)
-- {
-- const SWord64 s0 = x;
-- static const SWord64 table0[] = {
-- 0x0000000000000000ULL, 0x0000000000000001ULL,
-- 0x0000000000000001ULL, 0x0000000000000002ULL,
-- 0x0000000000000003ULL, 0x0000000000000005ULL,
-- 0x0000000000000008ULL, 0x000000000000000dULL,
-- 0x0000000000000015ULL, 0x0000000000000022ULL,
-- 0x0000000000000037ULL, 0x0000000000000059ULL,
-- 0x0000000000000090ULL, 0x00000000000000e9ULL,
-- 0x0000000000000179ULL, 0x0000000000000262ULL,
-- 0x00000000000003dbULL, 0x000000000000063dULL,
-- 0x0000000000000a18ULL, 0x0000000000001055ULL,
-- 0x0000000000001a6dULL, 0x0000000000002ac2ULL,
-- 0x000000000000452fULL, 0x0000000000006ff1ULL,
-- 0x000000000000b520ULL, 0x0000000000012511ULL,
-- 0x000000000001da31ULL, 0x000000000002ff42ULL,
-- 0x000000000004d973ULL, 0x000000000007d8b5ULL,
-- 0x00000000000cb228ULL, 0x0000000000148addULL,
-- 0x0000000000213d05ULL, 0x000000000035c7e2ULL,
-- 0x00000000005704e7ULL, 0x00000000008cccc9ULL,
-- 0x0000000000e3d1b0ULL, 0x0000000001709e79ULL,
-- 0x0000000002547029ULL, 0x0000000003c50ea2ULL,
-- 0x0000000006197ecbULL, 0x0000000009de8d6dULL,
-- 0x000000000ff80c38ULL, 0x0000000019d699a5ULL,
-- 0x0000000029cea5ddULL, 0x0000000043a53f82ULL,
-- 0x000000006d73e55fULL, 0x00000000b11924e1ULL,
-- 0x000000011e8d0a40ULL, 0x00000001cfa62f21ULL,
-- 0x00000002ee333961ULL, 0x00000004bdd96882ULL,
-- 0x00000007ac0ca1e3ULL, 0x0000000c69e60a65ULL,
-- 0x0000001415f2ac48ULL, 0x000000207fd8b6adULL,
-- 0x0000003495cb62f5ULL, 0x0000005515a419a2ULL,
-- 0x00000089ab6f7c97ULL, 0x000000dec1139639ULL,
-- 0x000001686c8312d0ULL, 0x000002472d96a909ULL,
-- 0x000003af9a19bbd9ULL, 0x000005f6c7b064e2ULL, 0x000009a661ca20bbULL
-- };
-- const SWord64 s65 = s0 >= 65 ? 0x0000000000000000ULL : table0[s0];
--
-- return s65;
-- }
--
genFib2 :: SWord64 -> IO ()
-- | Computing GCD symbolically, and generating C code for it. This example
-- illustrates symbolic termination related issues when programming with
-- SBV, when the termination of a recursive algorithm crucially depends
-- on the value of a symbolic variable. The technique we use is to
-- statically enforce termination by using a recursion depth counter.
module Data.SBV.Examples.CodeGeneration.GCD
-- | The symbolic GCD algorithm, over two 8-bit numbers. We define sgcd
-- a 0 to be a for all a, which implies sgcd 0
-- 0 = 0. Note that this is essentially Euclid's algorithm, except
-- with a recursion depth counter. We need the depth counter since the
-- algorithm is not symbolically terminating, as we don't have a
-- means of determining that the second argument (b) will
-- eventually reach 0 in a symbolic context. Hence we stop after 12
-- iterations. Why 12? We've empirically determined that this algorithm
-- will recurse at most 12 times for arbitrary 8-bit numbers. Of course,
-- this is a claim that we shall prove below.
sgcd :: SWord8 -> SWord8 -> SWord8
-- | We have:
--
--
-- >>> prove sgcdIsCorrect
-- Q.E.D.
--
sgcdIsCorrect :: SWord8 -> SWord8 -> SWord8 -> SBool
-- | This call will generate the required C files. The following is the
-- function body generated for sgcd. (We are not showing the
-- generated header, Makefile, and the driver programs for
-- brevity.) Note that the generated function is a constant time
-- algorithm for GCD. It is not necessarily fastest, but it will take
-- precisely the same amount of time for all values of x and
-- y.
--
--
-- /* File: "sgcd.c". Automatically generated by SBV. Do not edit! */
--
-- #include <inttypes.h>
-- #include <stdint.h>
-- #include "sgcd.h"
--
-- SWord8 sgcd(const SWord8 x, const SWord8 y)
-- {
-- const SWord8 s0 = x;
-- const SWord8 s1 = y;
-- const SBool s3 = s1 == 0;
-- const SWord8 s4 = (s1 == 0) ? s0 : (s0 % s1);
-- const SWord8 s5 = s3 ? s0 : s4;
-- const SBool s6 = 0 == s5;
-- const SWord8 s7 = (s5 == 0) ? s1 : (s1 % s5);
-- const SWord8 s8 = s6 ? s1 : s7;
-- const SBool s9 = 0 == s8;
-- const SWord8 s10 = (s8 == 0) ? s5 : (s5 % s8);
-- const SWord8 s11 = s9 ? s5 : s10;
-- const SBool s12 = 0 == s11;
-- const SWord8 s13 = (s11 == 0) ? s8 : (s8 % s11);
-- const SWord8 s14 = s12 ? s8 : s13;
-- const SBool s15 = 0 == s14;
-- const SWord8 s16 = (s14 == 0) ? s11 : (s11 % s14);
-- const SWord8 s17 = s15 ? s11 : s16;
-- const SBool s18 = 0 == s17;
-- const SWord8 s19 = (s17 == 0) ? s14 : (s14 % s17);
-- const SWord8 s20 = s18 ? s14 : s19;
-- const SBool s21 = 0 == s20;
-- const SWord8 s22 = (s20 == 0) ? s17 : (s17 % s20);
-- const SWord8 s23 = s21 ? s17 : s22;
-- const SBool s24 = 0 == s23;
-- const SWord8 s25 = (s23 == 0) ? s20 : (s20 % s23);
-- const SWord8 s26 = s24 ? s20 : s25;
-- const SBool s27 = 0 == s26;
-- const SWord8 s28 = (s26 == 0) ? s23 : (s23 % s26);
-- const SWord8 s29 = s27 ? s23 : s28;
-- const SBool s30 = 0 == s29;
-- const SWord8 s31 = (s29 == 0) ? s26 : (s26 % s29);
-- const SWord8 s32 = s30 ? s26 : s31;
-- const SBool s33 = 0 == s32;
-- const SWord8 s34 = (s32 == 0) ? s29 : (s29 % s32);
-- const SWord8 s35 = s33 ? s29 : s34;
-- const SBool s36 = 0 == s35;
-- const SWord8 s37 = s36 ? s32 : s35;
-- const SWord8 s38 = s33 ? s29 : s37;
-- const SWord8 s39 = s30 ? s26 : s38;
-- const SWord8 s40 = s27 ? s23 : s39;
-- const SWord8 s41 = s24 ? s20 : s40;
-- const SWord8 s42 = s21 ? s17 : s41;
-- const SWord8 s43 = s18 ? s14 : s42;
-- const SWord8 s44 = s15 ? s11 : s43;
-- const SWord8 s45 = s12 ? s8 : s44;
-- const SWord8 s46 = s9 ? s5 : s45;
-- const SWord8 s47 = s6 ? s1 : s46;
-- const SWord8 s48 = s3 ? s0 : s47;
--
-- return s48;
-- }
--
genGCDInC :: IO ()
-- | Computing population-counts (number of set bits) and autimatically
-- generating C code.
module Data.SBV.Examples.CodeGeneration.PopulationCount
-- | Given a 64-bit quantity, the simplest (and obvious) way to count the
-- number of bits that are set in it is to simply walk through all the
-- bits and add 1 to a running count. This is slow, as it requires 64
-- iterations, but is simple and easy to convince yourself that it is
-- correct. For instance:
--
--
-- >>> popCount_Slow 0x0123456789ABCDEF
-- 32 :: SWord8
--
popCount_Slow :: SWord64 -> SWord8
-- | Faster version. This is essentially the same algorithm, except we go 8
-- bits at a time instead of one by one, by using a precomputed table of
-- population-count values for each byte. This algorithm loops
-- only 8 times, and hence is at least 8 times more efficient.
popCount :: SWord64 -> SWord8
-- | Look-up table, containing population counts for all possible 8-bit
-- value, from 0 to 255. Note that we do not "hard-code" the values, but
-- merely use the slow version to compute them.
pop8 :: [SWord8]
-- | States the correctness of faster population-count algorithm, with
-- respect to the reference slow version. We have:
--
--
-- >>> prove fastPopCountIsCorrect
-- Q.E.D.
--
fastPopCountIsCorrect :: SWord64 -> SBool
-- | Not only we can prove that faster version is correct, but we can also
-- automatically generate C code to compute population-counts for us.
-- This action will generate all the C files that you will need,
-- including a driver program for test purposes.
--
-- Below is the generated header file for popCount:
--
--
-- /* Header file for popCount. Automatically generated by SBV. Do not edit! */
--
-- #ifndef __popCount__HEADER_INCLUDED__
-- #define __popCount__HEADER_INCLUDED__
--
-- #include <inttypes.h>
-- #include <stdint.h>
--
-- /* Unsigned bit-vectors */
-- typedef uint8_t SBool ;
-- typedef uint8_t SWord8 ;
-- typedef uint16_t SWord16;
-- typedef uint32_t SWord32;
-- typedef uint64_t SWord64;
--
-- /* Signed bit-vectors */
-- typedef int8_t SInt8 ;
-- typedef int16_t SInt16;
-- typedef int32_t SInt32;
-- typedef int64_t SInt64;
--
-- /* Entry point prototype: */
-- SWord8 popCount(const SWord64 x);
--
-- #endif /* __popCount__HEADER_INCLUDED__ */
--
--
-- The generated C function. Note how the Haskell list pop8 is
-- turned into a look-up table automatically (see table0 below)
-- in the C code.
--
--
-- /* File: "popCount.c". Automatically generated by SBV. Do not edit! */
--
-- #include <inttypes.h>
-- #include <stdint.h>
-- #include "popCount.h"
--
-- SWord8 popCount(const SWord64 x)
-- {
-- const SWord64 s0 = x;
-- static const SWord8 table0[] = {
-- 0, 1, 1, 2, 1, 2, 2, 3, 1, 2, 2, 3, 2, 3, 3, 4, 1, 2, 2, 3, 2, 3,
-- 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4,
-- 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 1, 2,
-- 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5,
-- 3, 4, 4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5,
-- 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 1, 2, 2, 3,
-- 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4,
-- 4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,
-- 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 2, 3, 3, 4, 3, 4,
-- 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6,
-- 5, 6, 6, 7, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 4, 5,
-- 5, 6, 5, 6, 6, 7, 5, 6, 6, 7, 6, 7, 7, 8
-- };
-- const SWord64 s11 = s0 & 0x00000000000000ffULL;
-- const SWord8 s12 = table0[s11];
-- const SWord64 s13 = s0 >> 8;
-- const SWord64 s14 = 0x00000000000000ffULL & s13;
-- const SWord8 s15 = table0[s14];
-- const SWord8 s16 = s12 + s15;
-- const SWord64 s17 = s13 >> 8;
-- const SWord64 s18 = 0x00000000000000ffULL & s17;
-- const SWord8 s19 = table0[s18];
-- const SWord8 s20 = s16 + s19;
-- const SWord64 s21 = s17 >> 8;
-- const SWord64 s22 = 0x00000000000000ffULL & s21;
-- const SWord8 s23 = table0[s22];
-- const SWord8 s24 = s20 + s23;
-- const SWord64 s25 = s21 >> 8;
-- const SWord64 s26 = 0x00000000000000ffULL & s25;
-- const SWord8 s27 = table0[s26];
-- const SWord8 s28 = s24 + s27;
-- const SWord64 s29 = s25 >> 8;
-- const SWord64 s30 = 0x00000000000000ffULL & s29;
-- const SWord8 s31 = table0[s30];
-- const SWord8 s32 = s28 + s31;
-- const SWord64 s33 = s29 >> 8;
-- const SWord64 s34 = 0x00000000000000ffULL & s33;
-- const SWord8 s35 = table0[s34];
-- const SWord8 s36 = s32 + s35;
-- const SWord64 s37 = s33 >> 8;
-- const SWord64 s38 = 0x00000000000000ffULL & s37;
-- const SWord8 s39 = table0[s38];
-- const SWord8 s40 = s36 + s39;
--
-- return s40;
-- }
--
--
-- SBV will also generate a driver program for test purposes. The driver
-- will call the generated function with random values. (It is also
-- possible to instruct SBV to use prescribed values, see the function
-- compileToC'.)
--
--
-- /* Example driver program for popCount. */
-- /* Automatically generated by SBV. Edit as you see fit! */
--
-- #include <inttypes.h>
-- #include <stdint.h>
-- #include <stdio.h>
-- #include "popCount.h"
--
-- int main(void)
-- {
-- const SWord8 __result = popCount(0x000000007016b176ULL);
--
-- printf("popCount(0x000000007016b176ULL) = %"PRIu8"\n", __result);
--
-- return 0;
-- }
--
--
-- And a Makefile to simplify compilation:
--
--
-- # Makefile for popCount. Automatically generated by SBV. Do not edit!
--
-- # include any user-defined .mk file in the current directory.
-- -include *.mk
--
-- CC=gcc
-- CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
--
-- all: popCount_driver
--
-- popCount.o: popCount.c popCount.h
-- ${CC} ${CCFLAGS} -c $< -o $@
--
-- popCount_driver.o: popCount_driver.c
-- ${CC} ${CCFLAGS} -c $< -o $@
--
-- popCount_driver: popCount.o popCount_driver.o
-- ${CC} ${CCFLAGS} $^ -o $@
--
-- clean:
-- rm -f *.o
--
-- veryclean: clean
-- rm -f popCount_driver
--
genPopCountInC :: IO ()
-- | An implementation of AES (Advanced Encryption Standard), using SBV.
-- For details on AES, see FIPS-197:
-- http://csrc.nist.gov/publications/fips/fips197/fips-197.pdf.
--
-- We do a T-box implementation, which leads to good C code as we can
-- take advantage of look-up tables. Note that we make virtually no
-- attempt to optimize our Haskell code. The concern here is not with
-- getting Haskell running fast at all. The idea is to program the T-Box
-- implementation as naturally and clearly as possible in Haskell, and
-- have SBV's code-generator generate fast C code automatically.
-- Therefore, we merely use ordinary Haskell lists as our
-- data-structures, and do not bother with any unboxing or strictness
-- annotations. Thus, we achieve the separation of concerns: Correctness
-- via clairty and simplicity and proofs on the Haskell side, performance
-- by relying on SBV's code generator. If necessary, the generated code
-- can be FFI'd back into Haskell to complete the loop.
--
-- All 3 valid key sizes (128, 192, and 256) as required by the FIPS-197
-- standard are supported.
module Data.SBV.Examples.Crypto.AES
-- | An element of the Galois Field 2^8, which are essentially polynomials
-- with maximum degree 7. They are conveniently represented as values
-- between 0 and 255.
type GF28 = SWord8
-- | Multiplication in GF(2^8). This is simple polynomial multipliation,
-- followed by the irreducible polynomial x^8+x^5+x^3+x^1+1. We
-- simply use the pMult function exported by SBV to do the
-- operation.
gf28Mult :: GF28 -> GF28 -> GF28
-- | Exponentiation by a constant in GF(2^8). The implementation uses the
-- usual square-and-multiply trick to speed up the computation.
gf28Pow :: GF28 -> Int -> GF28
-- | Computing inverses in GF(2^8). By the mathematical properties of
-- GF(2^8) and the particular irreducible polynomial used
-- x^8+x^5+x^3+x^1+1, it turns out that raising to the 254 power
-- gives us the multiplicative inverse. Of course, we can prove this
-- using SBV:
--
--
-- >>> prove $ \x -> x ./= 0 ==> x `gf28Mult` gf28Inverse x .== 1
-- Q.E.D.
--
--
-- Note that we exclude 0 in our theorem, as it does not have a
-- multiplicative inverse.
gf28Inverse :: GF28 -> GF28
-- | AES state. The state consists of four 32-bit words, each of which is
-- in turn treated as four GF28's, i.e., 4 bytes. The T-Box
-- implementation keeps the four-bytes together for efficient
-- representation.
type State = [SWord32]
-- | The key, which can be 128, 192, or 256 bits. Represented as a sequence
-- of 32-bit words.
type Key = [SWord32]
-- | The key schedule. AES executes in rounds, and it treats first and last
-- round keys slightly differently than the middle ones. We reflect that
-- choice by being explicit about it in our type. The length of the
-- middle list of keys depends on the key-size, which in turn determines
-- the number of rounds.
type KS = (Key, [Key], Key)
-- | Conversion from 32-bit words to 4 constituent bytes.
toBytes :: SWord32 -> [GF28]
-- | Conversion from 4 bytes, back to a 32-bit row, inverse of
-- toBytes above. We have the following simple theorems stating
-- this relationship formally:
--
--
-- >>> prove $ \a b c d -> toBytes (fromBytes [a, b, c, d]) .== [a, b, c, d]
-- Q.E.D.
--
--
--
-- >>> prove $ \r -> fromBytes (toBytes r) .== r
-- Q.E.D.
--
fromBytes :: [GF28] -> SWord32
-- | Rotating a state row by a fixed amount to the right.
rotR :: [GF28] -> Int -> [GF28]
-- | Definition of round-constants, as specified in Section 5.2 of the AES
-- standard.
roundConstants :: [GF28]
-- | The InvMixColumns transformation, as described in Section
-- 5.3.3 of the standard. Note that this transformation is only used
-- explicitly during key-expansion in the T-Box implementation of AES.
invMixColumns :: State -> State
-- | Key expansion. Starting with the given key, returns an infinite
-- sequence of words, as described by the AES standard, Section 5.2,
-- Figure 11.
keyExpansion :: Int -> Key -> [Key]
-- | The values of the AES S-box table. Note that we describe the S-box
-- programmatically using the mathematical construction given in Section
-- 5.1.1 of the standard. However, the code-generation will turn this
-- into a mere look-up table, as it is just a constant table, all
-- computation being done at "compile-time".
sboxTable :: [GF28]
-- | The sbox transformation. We simply select from the sbox table. Note
-- that we are obliged to give a default value (here 0) to be
-- used if the index is out-of-bounds as required by SBV's select
-- function. However, that will never happen since the table has all 256
-- elements in it.
sbox :: GF28 -> GF28
-- | The values of the inverse S-box table. Again, the construction is
-- programmatic.
unSBoxTable :: [GF28]
-- | The inverse s-box transformation.
unSBox :: GF28 -> GF28
-- | Prove that the sbox and unSBox are inverses. We have:
--
--
-- >>> prove sboxInverseCorrect
-- Q.E.D.
--
sboxInverseCorrect :: GF28 -> SBool
-- | Adding the round-key to the current state. We simply exploit the fact
-- that addition is just xor in implementing this transformation.
addRoundKey :: Key -> State -> State
-- | T-box table generation function for encryption
t0Func :: GF28 -> [GF28]
-- | First look-up table used in encryption
t0 :: GF28 -> SWord32
-- | Second look-up table used in encryption
t1 :: GF28 -> SWord32
-- | Third look-up table used in encryption
t2 :: GF28 -> SWord32
-- | Fourth look-up table used in encryption
t3 :: GF28 -> SWord32
-- | T-box table generating function for decryption
u0Func :: GF28 -> [GF28]
-- | First look-up table used in decryption
u0 :: GF28 -> SWord32
-- | Second look-up table used in decryption
u1 :: GF28 -> SWord32
-- | Third look-up table used in decryption
u2 :: GF28 -> SWord32
-- | Fourth look-up table used in decryption
u3 :: GF28 -> SWord32
-- | Generic round function. Given the function to perform one round, a
-- key-schedule, and a starting state, it performs the AES rounds.
doRounds :: (Bool -> State -> Key -> State) -> KS -> State -> State
-- | One encryption round. The first argument indicates whether this is the
-- final round or not, in which case the construction is slightly
-- different.
aesRound :: Bool -> State -> Key -> State
-- | One decryption round. Similar to the encryption round, the first
-- argument indicates whether this is the final round or not.
aesInvRound :: Bool -> State -> Key -> State
-- | Key schedule. Given a 128, 192, or 256 bit key, expand it to get
-- key-schedules for encryption and decryption. The key is given as a
-- sequence of 32-bit words. (4 elements for 128-bits, 6 for 192, and 8
-- for 256.)
aesKeySchedule :: Key -> (KS, KS)
-- | Block encryption. The first argument is the plain-text, which must
-- have precisely 4 elements, for a total of 128-bits of input. The
-- second argument is the key-schedule to be used, obtained by a call to
-- aesKeySchedule. The output will always have 4 32-bit words,
-- which is the cipher-text.
aesEncrypt :: [SWord32] -> KS -> [SWord32]
-- | Block decryption. The arguments are the same as in aesEncrypt,
-- except the first argument is the cipher-text and the output is the
-- corresponding plain-text.
aesDecrypt :: [SWord32] -> KS -> [SWord32]
-- | 128-bit encryption test, from Appendix C.1 of the AES standard:
--
--
-- >>> map hex t128Enc
-- ["69c4e0d8","6a7b0430","d8cdb780","70b4c55a"]
--
t128Enc :: [SWord32]
-- | 128-bit decryption test, from Appendix C.1 of the AES standard:
--
--
-- >>> map hex t128Dec
-- ["00112233","44556677","8899aabb","ccddeeff"]
--
t128Dec :: [SWord32]
-- | 192-bit encryption test, from Appendix C.2 of the AES standard:
--
--
-- >>> map hex t192Enc
-- ["dda97ca4","864cdfe0","6eaf70a0","ec0d7191"]
--
t192Enc :: [SWord32]
-- | 192-bit decryption test, from Appendix C.2 of the AES standard:
--
--
-- >>> map hex t192Dec
-- ["00112233","44556677","8899aabb","ccddeeff"]
--
t192Dec :: [SWord32]
-- | 256-bit encryption, from Appendix C.3 of the AES standard:
--
--
-- >>> map hex t256Enc
-- ["8ea2b7ca","516745bf","eafc4990","4b496089"]
--
t256Enc :: [SWord32]
-- | 256-bit decryption, from Appendix C.3 of the AES standard:
--
--
-- >>> map hex t256Dec
-- ["00112233","44556677","8899aabb","ccddeeff"]
--
t256Dec :: [SWord32]
-- | Correctness theorem for 128-bit AES. Ideally, we would run:
--
--
-- prove aes128IsCorrect
--
--
-- to get a proof automatically. Unfortunately, while SBV will
-- successfully generate the proof obligation for this theorem and ship
-- it to the SMT solver, it would be naive to expect the SMT-solver to
-- finish that proof in any reasonable time with the currently available
-- SMT solving technologies. Instead, we can issue:
--
--
-- quickCheck aes128IsCorrect
--
--
-- and get some degree of confidence in our code. Similar predicates can
-- be easily constructed for 192, and 256 bit cases as well.
aes128IsCorrect :: (SWord32, SWord32, SWord32, SWord32) -> (SWord32, SWord32, SWord32, SWord32) -> SBool
-- | Code generation for 128-bit AES encryption.
--
-- The following sample from the generated code-lines show how T-Boxes
-- are rendered as C arrays:
--
--
-- static const SWord32 table1[] = {
-- 0xc66363a5UL, 0xf87c7c84UL, 0xee777799UL, 0xf67b7b8dUL,
-- 0xfff2f20dUL, 0xd66b6bbdUL, 0xde6f6fb1UL, 0x91c5c554UL,
-- 0x60303050UL, 0x02010103UL, 0xce6767a9UL, 0x562b2b7dUL,
-- 0xe7fefe19UL, 0xb5d7d762UL, 0x4dababe6UL, 0xec76769aUL,
-- ...
-- }
--
--
-- The generated program has 5 tables (one sbox table, and 4-Tboxes), all
-- converted to fast C arrays. Here is a sample of the generated
-- straightline C-code:
--
--
-- const SWord8 s1915 = (SWord8) s1912;
-- const SWord8 s1916 = table0[s1915];
-- const SWord16 s1917 = (((SWord16) s1914) << 8) | ((SWord16) s1916);
-- const SWord32 s1918 = (((SWord32) s1911) << 16) | ((SWord32) s1917);
-- const SWord32 s1919 = s1844 ^ s1918;
-- const SWord32 s1920 = s1903 ^ s1919;
--
--
-- The GNU C-compiler does a fine job of optimizing this straightline
-- code to generate a fairly efficient C implementation.
cgAES128BlockEncrypt :: IO ()
-- | Components of the AES-128 implementation that the library is generated
-- from
aes128LibComponents :: [(String, SBVCodeGen ())]
-- | Generate a C library, containing functions for performing 128-bit
-- encdeckey-expansion. A note on performance: In a very rough
-- speed test, the generated code was able to do 6.3 million block
-- encryptions per second on a decent MacBook Pro. On the same machine,
-- OpenSSL reports 8.2 million block encryptions per second. So, the
-- generated code is about 25% slower as compared to the highly optimized
-- OpenSSL implementation. (Note that the speed test was done somewhat
-- simplistically, so these numbers should be considered very rough
-- estimates.)
cgAES128Library :: IO ()
-- | An implementation of RC4 (AKA Rivest Cipher 4 or Alleged RC4/ARC4),
-- using SBV. For information on RC4, see:
-- http://en.wikipedia.org/wiki/RC4.
--
-- We make no effort to optimize the code, and instead focus on a clear
-- implementation. In fact, the RC4 algorithm relies on in-place update
-- of its state heavily for efficiency, and is therefore unsuitable for a
-- purely functional implementation.
module Data.SBV.Examples.Crypto.RC4
-- | RC4 State contains 256 8-bit values. We use the symbolically
-- accessible full-binary type STree to represent the state, since
-- RC4 needs access to the array via a symbolic index and it's important
-- to minimize access time.
type S = STree Word8 Word8
-- | Construct the fully balanced initial tree, where the leaves are simply
-- the numbers 0 through 255.
initS :: S
-- | The key is a stream of Word8 values.
type Key = [SWord8]
-- | Represents the current state of the RC4 stream: it is the S
-- array along with the i and j index values used by
-- the PRGA.
type RC4 = (S, SWord8, SWord8)
-- | Swaps two elements in the RC4 array.
swap :: SWord8 -> SWord8 -> S -> S
-- | Implements the PRGA used in RC4. We return the new state and the next
-- key value generated.
prga :: RC4 -> (SWord8, RC4)
-- | Constructs the state to be used by the PRGA using the given key.
initRC4 :: Key -> S
-- | The key-schedule. Note that this function returns an infinite list.
keySchedule :: Key -> [SWord8]
-- | Generate a key-schedule from a given key-string.
keyScheduleString :: String -> [SWord8]
-- | RC4 encryption. We generate key-words and xor it with the input. The
-- following test-vectors are from Wikipedia
-- http://en.wikipedia.org/wiki/RC4:
--
--
-- >>> concatMap hex $ encrypt "Key" "Plaintext"
-- "bbf316e8d940af0ad3"
--
--
--
-- >>> concatMap hex $ encrypt "Wiki" "pedia"
-- "1021bf0420"
--
--
--
-- >>> concatMap hex $ encrypt "Secret" "Attack at dawn"
-- "45a01f645fc35b383552544b9bf5"
--
encrypt :: String -> String -> [SWord8]
-- | RC4 decryption. Essentially the same as decryption. For the above test
-- vectors we have:
--
--
-- >>> decrypt "Key" [0xbb, 0xf3, 0x16, 0xe8, 0xd9, 0x40, 0xaf, 0x0a, 0xd3]
-- "Plaintext"
--
--
--
-- >>> decrypt "Wiki" [0x10, 0x21, 0xbf, 0x04, 0x20]
-- "pedia"
--
--
--
-- >>> decrypt "Secret" [0x45, 0xa0, 0x1f, 0x64, 0x5f, 0xc3, 0x5b, 0x38, 0x35, 0x52, 0x54, 0x4b, 0x9b, 0xf5]
-- "Attack at dawn"
--
decrypt :: String -> [SWord8] -> String
-- | Prove that round-trip encryption/decryption leaves the plain-text
-- unchanged. The theorem is stated parametrically over key and
-- plain-text sizes. The expression performs the proof for a 40-bit key
-- (5 bytes) and 40-bit plaintext (again 5 bytes).
--
-- Note that this theorem is trivial to prove, since it is essentially
-- establishing xor'in the same value twice leaves a word unchanged
-- (i.e., x xor y xor y = x). However, the proof
-- takes quite a while to complete, as it gives rise to a fairly large
-- symbolic trace.
rc4IsCorrect :: IO ThmResult
-- | Simple usage of polynomials over GF(2^n), using Rijndael's finite
-- field:
-- http://en.wikipedia.org/wiki/Finite_field_arithmetic#Rijndael.27s_finite_field
--
-- The functions available are:
--
--
-- - pMult GF(2^n) Multiplication
-- - pDiv GF(2^n) Division
-- - pMod GF(2^n) Modulus
-- - pDivMod GF(2^n) Division/Modulus, packed
-- together
--
--
-- Note that addition in GF(2^n) is simply xor, so no custom
-- function is provided.
module Data.SBV.Examples.Polynomials.Polynomials
-- | Helper synonym for representing GF(2^8); which are merely 8-bit
-- unsigned words. Largest term in such a polynomial has degree 7.
type GF28 = SWord8
-- | Multiplication in Rijndael's field; usual polynomial multiplication
-- followed by reduction by the irreducible polynomial. The irreducible
-- used by Rijndael's field is the polynomial x^8 + x^4 + x^3 + x +
-- 1, which we write by giving it's exponents in SBV. See:
-- http://en.wikipedia.org/wiki/Finite_field_arithmetic#Rijndael.27s_finite_field.
-- Note that the irreducible itself is not in GF28! It has a degree of 8.
--
-- NB. You can use the showPoly function to print polynomials
-- nicely, as a mathematician would write.
(<*>) :: GF28 -> GF28 -> GF28
-- | States that the unit polynomial 1, is the unit element
multUnit :: GF28 -> SBool
-- | States that multiplication is commutative
multComm :: GF28 -> GF28 -> SBool
-- | States that multiplication is associative, note that associativity
-- proofs are notoriously hard for SAT/SMT solvers
multAssoc :: GF28 -> GF28 -> GF28 -> SBool
-- | States that the usual multiplication rule holds over GF(2^n)
-- polynomials Checks:
--
--
-- if (a, b) = x pDivMod y then x = y pMult a + b
--
--
-- being careful about y = 0. When divisor is 0, then quotient
-- is defined to be 0 and the remainder is the numerator. (Note that
-- addition is simply xor in GF(2^8).)
polyDivMod :: GF28 -> GF28 -> SBool
-- | Queries
testGF28 :: IO ()
-- | Consider the sentence:
--
--
-- In this sentence, the number of occurrences of 0 is _, of 1 is _, of 2 is _,
-- of 3 is _, of 4 is _, of 5 is _, of 6 is _, of 7 is _, of 8 is _, and of 9 is _.
--
--
-- The puzzle is to fill the blanks with numbers, such that the sentence
-- will be correct. There are precisely two solutions to this puzzle,
-- both of which are found by SBV successfully.
--
-- References:
--
--
module Data.SBV.Examples.Puzzles.Counts
-- | We will assume each number can be represented by an 8-bit word, i.e.,
-- can be at most 128.
type Count = SWord8
type Counts = [Count]
-- | Given a number, increment the count array depending on the digits of
-- the number
count :: Count -> Counts -> Counts
-- | Encoding of the puzzle. The solution is a sequence of 10 numbers for
-- the occurrences of the digits such that if we count each digit, we
-- find these numbers.
puzzle :: Counts -> SBool
-- | Finds all two known solutions to this puzzle. We have:
--
--
-- >>> solve
-- Solution #1
-- In this sentence, the number of occurrences of 0 is 1, of 1 is 11, of 2 is 2, of 3 is 1, of 4 is 1, of 5 is 1, of 6 is 1, of 7 is 1, of 8 is 1, of 9 is 1.
-- Solution #2
-- In this sentence, the number of occurrences of 0 is 1, of 1 is 7, of 2 is 3, of 3 is 2, of 4 is 1, of 5 is 1, of 6 is 1, of 7 is 2, of 8 is 1, of 9 is 1.
-- Found: 2 solution(s).
--
solve :: IO ()
-- | Puzzle: Spend exactly 100 dollars and buy exactly 100 animals. Dogs
-- cost 15 dollars, cats cost 1 dollar, and mice cost 25 cents each. You
-- have to buy at least one of each. How many of each should you buy?
module Data.SBV.Examples.Puzzles.DogCatMouse
-- | Use 16-bit words to represent the counts, much larger than we actually
-- need, but no harm.
type Count = SWord16
-- | Codes the puzzle statement, more or less directly using SBV.
puzzle :: Count -> Count -> Count -> SBool
-- | Prints the only solution:
--
--
-- >>> solve
-- Only one solution found:
-- dog = 3 :: SWord16
-- cat = 41 :: SWord16
-- mouse = 56 :: SWord16
--
solve :: IO AllSatResult
-- | A solution to Project Euler problem #185:
-- http://projecteuler.net/index.php?section=problems&id=185
module Data.SBV.Examples.Puzzles.Euler185
-- | The given guesses and the correct digit counts, encoded as a simple
-- list.
guesses :: [(String, SWord8)]
-- | Encode the problem, note that we check digits are within 0-9 as we use
-- 8-bit words to represent them. Otherwise, the constraints are simply
-- generated by zipping the alleged solution with each guess, and making
-- sure the number of matching digits match what's given in the problem
-- statement.
euler185 :: Symbolic SBool
-- | Print out the solution nicely. We have:
--
--
-- >>> solve
-- 4640261571849533
-- Number of solutions: 1
--
solve :: IO ()
-- | Solves the magic-square puzzle. An NxN magic square is one where all
-- entries are filled with numbers from 1 to NxN such that sums of all
-- rows, columns and diagonals is the same.
module Data.SBV.Examples.Puzzles.MagicSquare
-- | Use 32-bit words for elements.
type Elem = SWord32
-- | A row is a list of elements
type Row = [Elem]
-- | The puzzle board is a list of rows
type Board = [Row]
-- | Checks that all elements in a list are within bounds
check :: Elem -> Elem -> [Elem] -> SBool
-- | Get the diagonal of a square matrix
diag :: [[a]] -> [a]
-- | Test if a given board is a magic square
isMagic :: Board -> SBool
-- | Group a list of elements in the sublists of length i
chunk :: Int -> [a] -> [[a]]
-- | Given n, magic n prints all solutions to the
-- nxn magic square problem
magic :: Int -> IO ()
-- | Solves the NQueens puzzle:
-- http://en.wikipedia.org/wiki/Eight_queens_puzzle
module Data.SBV.Examples.Puzzles.NQueens
-- | A solution is a sequence of row-numbers where queens should be placed
type Solution = [SWord8]
-- | Checks that a given solution of n-queens is valid, i.e., no
-- queen captures any other.
isValid :: Int -> Solution -> SBool
-- | Given n, it solves the n-queens puzzle, printing all
-- possible solutions.
nQueens :: Int -> IO ()
-- | The Sudoku solver, quintessential SMT solver example!
module Data.SBV.Examples.Puzzles.Sudoku
-- | A row is a sequence of 8-bit words, too large indeed for representing
-- 1-9, but does not harm
type Row = [SWord8]
-- | A Sudoku board is a sequence of 9 rows
type Board = [Row]
-- | Given a series of elements, make sure they are all different and they
-- all are numbers between 1 and 9
check :: [SWord8] -> SBool
-- | Given a full Sudoku board, check that it is valid
valid :: Board -> SBool
-- | A puzzle is a pair: First is the number of missing elements, second is
-- a function that given that many elements returns the final board.
type Puzzle = (Int, [SWord8] -> Board)
-- | Solve a given puzzle and print the results
solve :: Puzzle -> IO ()
-- | Helper function to display results nicely, not really needed, but
-- helps presentation
dispSolution :: Puzzle -> [Word8] -> IO ()
-- | Find all solutions to a puzzle
solveAll :: Puzzle -> IO ()
-- | Find an arbitrary good board
puzzle0 :: Puzzle
-- | A random puzzle, found on the internet..
puzzle1 :: Puzzle
-- | Another random puzzle, found on the internet..
puzzle2 :: Puzzle
-- | Another random puzzle, found on the internet..
puzzle3 :: Puzzle
-- | According to the web, this is the toughest sudoku puzzle ever.. It
-- even has a name: Al Escargot:
-- http://zonkedyak.blogspot.com/2006/11/worlds-hardest-sudoku-puzzle-al.html
puzzle4 :: Puzzle
-- | This one has been called diabolical, apparently
puzzle5 :: Puzzle
-- | The following is nefarious according to
-- http://haskell.org/haskellwiki/Sudoku
puzzle6 :: Puzzle
-- | Solve them all, this takes a fraction of a second to run for each case
allPuzzles :: IO ()
-- | The famous U2 bridge crossing puzzle:
-- http://www.brainj.net/puzzle.php?id=u2
module Data.SBV.Examples.Puzzles.U2Bridge
-- | U2 band members
data U2Member
Bono :: U2Member
Edge :: U2Member
Adam :: U2Member
Larry :: U2Member
-- | Model time using 32 bits
type Time = SWord32
-- | Each member gets an 8-bit id
type SU2Member = SWord8
-- | Bono's ID
bono :: SU2Member
-- | Edge's ID
edge :: SU2Member
-- | Adam's ID
adam :: SU2Member
-- | Larry's ID
larry :: SU2Member
-- | Is this a valid person?
isU2Member :: SU2Member -> SBool
-- | Crossing times for each member of the band
crossTime :: SU2Member -> Time
-- | Location of the flash
type Location = SBool
-- | We represent this side of the bridge as here, and arbitrarily
-- as false
here :: Location
-- | We represent other side of the bridge as there, and arbitrarily
-- as true
there :: Location
-- | The status of the puzzle after each move
data Status
Status :: Time -> Location -> Location -> Location -> Location -> Location -> Status
-- | elapsed time
time :: Status -> Time
-- | location of the flash
flash :: Status -> Location
-- | location of Bono
lBono :: Status -> Location
-- | location of Edge
lEdge :: Status -> Location
-- | location of Adam
lAdam :: Status -> Location
-- | location of Larry
lLarry :: Status -> Location
-- | Start configuration, time elapsed is 0 and everybody is here
start :: Status
-- | A puzzle move is modeled as a state-transformer
type Move a = State Status a
-- | Read the state via an accessor function
peek :: (Status -> a) -> Move a
-- | Given an arbitrary member, return his location
whereIs :: SU2Member -> Move SBool
-- | Transferring the flash to the other side
xferFlash :: Move ()
-- | Transferring a person to the other side
xferPerson :: SU2Member -> Move ()
-- | Increment the time, when only one person crosses
bumpTime1 :: SU2Member -> Move ()
-- | Increment the time, when two people cross together
bumpTime2 :: SU2Member -> SU2Member -> Move ()
-- | Symbolic version of when
whenS :: SBool -> Move () -> Move ()
-- | Move one member, remembering to take the flash
move1 :: SU2Member -> Move ()
-- | Move two members, again with the flash
move2 :: SU2Member -> SU2Member -> Move ()
-- | A move action is a sequence of triples. The first component is
-- symbolically True if only one member crosses. (In this case the third
-- element of the triple is irrelevant.) If the first component is
-- (symbolically) False, then both members move together
type Actions = [(SBool, SU2Member, SU2Member)]
-- | Run a sequence of given actions.
run :: Actions -> Move [Status]
-- | Check if a given sequence of actions is valid, i.e., they must all
-- cross the bridge according to the rules and in less than 17 seconds
isValid :: Actions -> SBool
-- | See if there is a solution that has precisely n steps
solveN :: Int -> IO Bool
-- | Solve the U2-bridge crossing puzzle, starting by testing solutions
-- with increasing number of steps, until we find one. We have:
--
--
-- >>> solveU2
-- Checking for solutions with 1 move.
-- Checking for solutions with 2 moves.
-- Checking for solutions with 3 moves.
-- Checking for solutions with 4 moves.
-- Checking for solutions with 5 moves.
-- Solution #1:
-- 0 --> Edge, Bono
-- 2 <-- Edge
-- 4 --> Larry, Adam
-- 14 <-- Bono
-- 15 --> Edge, Bono
-- Total time: 17
-- Solution #2:
-- 0 --> Edge, Bono
-- 2 <-- Bono
-- 3 --> Larry, Adam
-- 13 <-- Edge
-- 15 --> Edge, Bono
-- Total time: 17
-- Found: 2 solutions with 5 moves.
--
--
-- Finding the all 2 possible solutions to the puzzle.
solveU2 :: IO ()
instance Show U2Member
instance Enum U2Member
instance SatModel U2Member
instance Mergeable a => Mergeable (Move a)
instance Mergeable Status
-- | Formalizes and proves the following theorem, about arithmetic,
-- uninterpreted functions, and arrays. (For reference, see
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/fmcad06-slides.pdf
-- 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):
--
--
-- - x SWord32 (32-bit unsigned address)
-- - y SWord32 (32-bit unsigned address)
-- - a An array, indexed by 32-bit addresses, returning
-- 32-bit unsigned integers
-- - f An uninterpreted function of type
-- SWord32 -> SWord64
--
--
-- The function read and write are usual array
-- operations.
module Data.SBV.Examples.Uninterpreted.AUF
-- | 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.
type A = SFunArray Word32 Word32
-- | Uninterpreted function in the theorem
f :: SWord32 -> SWord64
-- | Correctness theorem. We state it for all values of x,
-- y, and the array a. We also take an arbitrary
-- initializer for the array.
thm1 :: SWord32 -> SWord32 -> A -> SWord32 -> SBool
-- | Prints Q.E.D. when run, as expected
--
--
-- >>> proveThm1
-- Q.E.D.
--
proveThm1 :: IO ()
-- | This version directly uses SMT-arrays and hence does not need an
-- initializer. Reading an element before writing to it returns an
-- arbitrary value.
type B = SArray Word32 Word32
-- | Same as thm1, except we don't need an initializer with the
-- SArray model.
thm2 :: SWord32 -> SWord32 -> B -> SBool
-- | Prints Q.E.D. when run, as expected:
--
--
-- >>> proveThm2
-- Q.E.D.
--
proveThm2 :: IO ()
-- | Demonstrates function counter-examples
module Data.SBV.Examples.Uninterpreted.Function
-- | An uninterpreted function
f :: SWord8 -> SWord8 -> SWord16
-- | Asserts that f x z == f (y+2) z whenever x == y+2.
-- Naturally correct:
--
--
-- >>> prove thmGood
-- Q.E.D.
--
thmGood :: SWord8 -> SWord8 -> SWord8 -> SBool
-- | Asserts that f is commutative; which is not necessarily true!
-- Indeed, the SMT solver (Yices in this case) returns a counter-example
-- function that is not commutative. We have:
--
--
-- >>> prove $ forAll ["x", "y"] thmBad
-- Falsifiable. Counter-example:
-- x = 0 :: SWord8
-- y = 128 :: SWord8
-- -- uninterpreted: f
-- f 128 0 = 32768
-- f _ _ = 0
--
--
-- Note how the counterexample function f returned by Yices
-- violates commutativity; thus providing evidence that the asserted
-- theorem is not valid.
thmBad :: SWord8 -> SWord8 -> SBool