-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.
--
-- Adds support for symbolic bit vectors, allowing formal models of
-- bit-precise programs to be created. Supports symbolic arrays and
-- polynomials over GF(2^n). Supports uninterpreted constants and
-- functions. Aims to provide seamless integration with SMT solvers to
-- produce formal property proofs of theoremhood and satisfiability, with
-- counter-examples.
@package sbv
@version 0.9.3
-- | 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
-- | 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.
--
--
-- $ ghci -XScopedTypeVariables
-- Prelude> :m Data.SBV
-- Prelude Data.SBV> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x
-- Q.E.D.
-- Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x
-- Falsifiable. Counter-example:
-- x = 128 :: SWord8
--
--
-- The function prove has the following type:
--
--
-- prove :: Provable a => a -> IO ThmResult
--
--
-- The class Provable comes with instances for n-ary predicates,
-- for arbitrary n. The predicates are just regular Haskell functions
-- over symbolic signed and unsigned bit-vectors. Functions for checking
-- satisfiability (sat and allSat) are also provided.
--
-- In particular, the sbv library introduces the types:
--
--
--
-- 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. Reading an uninitilized entry is an error.
-- While it's certainly possible for user to create instances of
-- SymArray, the SArray and SFunArray instances
-- already provided should cover most use cases in practice.
--
-- Minimal complete definition: All methods are required, no defaults.
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
data SArray a b
-- | Arrays implemented internally as functions, and rendered as SMT-Lib
-- functions
data SFunArray a b
-- | 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
-- | 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 -> IO ()
bin :: PrettyNum a => a -> IO ()
-- | 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: uninterpret. 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
-- | 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.
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 -> [(String, CW)] -> SMTResult
-- | Prover returned unknown, with a potential (possibly bogus) model
Unknown :: SMTConfig -> [(String, CW)] -> 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
-- | Mark an interim result as an output. Useful when constructing Symbolic
-- programs that return multiple values, or when the result is
-- programmatically computed.
output :: SBV a -> Symbolic (SBV 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.
class Ord a => SymWord a
free :: SymWord a => String -> Symbolic (SBV a)
free_ :: SymWord a => 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
-- | 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 : CLC ; set C to 0
-- step4 : LOOP ROR F1 ; rotate F1 right circular through C
-- step5 : BCC ZCOEF ; branch to ZCOEF if C = 0
-- step6 : CLC ; set C to 0
-- step7 : ADC F2 ; set A to A+F2+C and C to the carry
-- step8 : ZCOEF ROR A ; rotate A right circular through C
-- step9 : ROR LOW ; rotate LOW right circular through C
-- step10: DEX ; set X to X-1
-- step11: BNE LOOP ; branch to LOOP if Z = 0
--
--
-- NB. The CLC in step3 was later added by Warren Hunt; the original spec
-- did not include this statement. However, without this addition, the
-- algorithm does not work correctly for all starting states, so we adopt
-- this change as well.
--
-- 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
-- | 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 30 seconds with SFunArray memory model above and about 30
-- minutes with the SArray memory model
correctnessTheorem :: IO ThmResult
instance Eq Flag
instance Ord Flag
instance Ix Flag
instance Bounded Flag
instance Enum Flag
instance Eq Register
instance Ord Register
instance Ix Register
instance Bounded Register
instance Enum Register
instance Mergeable Mostek
-- | 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:
--
--
-- dog = 3 :: SWord16
-- cat = 41 :: SWord16
-- mouse = 56 :: SWord16
--
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. This call prints:
--
--
-- 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
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.
thm :: SWord32 -> SWord32 -> A -> SWord32 -> SBool
-- | Prints Q.E.D. when run, as expected
proveThm :: IO ()