diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -102,6 +102,8 @@ , SInt8, SInt16, SInt32, SInt64 -- *** Arrays of symbolic values , SymArray(..), SArray, SFunArray, mkSFunArray + -- *** Full binary trees + , STree, readSTree, writeSTree, mkSTree -- ** Operations on symbolic words -- *** Word level , bitValue, setBitTo, oneIf, lsb, msb @@ -111,6 +113,8 @@ , blastBE, blastLE, FromBits(..) -- *** Splitting, joining, and extending , Splittable(..) + -- *** Sign-casting + , SignCast(..) -- ** Polynomial arithmetic , Polynomial(..) -- ** Conditionals: Mergeable values @@ -197,7 +201,9 @@ import Data.SBV.BitVectors.Model import Data.SBV.BitVectors.PrettyNum import Data.SBV.BitVectors.Polynomial +import Data.SBV.BitVectors.SignCast import Data.SBV.BitVectors.Splittable +import Data.SBV.BitVectors.STree import Data.SBV.Compilers.C import Data.SBV.Compilers.CodeGen import Data.SBV.Provers.Prover diff --git a/Data/SBV/BitVectors/Data.hs b/Data/SBV/BitVectors/Data.hs --- a/Data/SBV/BitVectors/Data.hs +++ b/Data/SBV/BitVectors/Data.hs @@ -698,10 +698,9 @@ instance (HasSignAndSize a, HasSignAndSize b) => Show (SFunArray a b) where show (SFunArray _) = "SFunArray<" ++ showType (undefined :: a) ++ ":" ++ showType (undefined :: b) ++ ">" --- | Make a constant fun-array always returning a fixed value. --- Useful for creating arrays in a pure context. (Otherwise use `newArray`.) -mkSFunArray :: SBV b -> SFunArray a b -mkSFunArray i = SFunArray (const i) +-- | 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 +mkSFunArray = SFunArray --------------------------------------------------------------------------------- -- * Cached values @@ -753,6 +752,10 @@ instance NFData SW instance NFData SBVType instance NFData UnintKind +instance NFData a => NFData (Cached a) where + rnf (Cached f) = f `seq` () +instance NFData a => NFData (SBV a) where + rnf (SBV x y) = rnf x `seq` rnf y `seq` () -- Quickcheck interface on symbolic-booleans.. instance Testable SBool where diff --git a/Data/SBV/BitVectors/Model.hs b/Data/SBV/BitVectors/Model.hs --- a/Data/SBV/BitVectors/Model.hs +++ b/Data/SBV/BitVectors/Model.hs @@ -414,11 +414,11 @@ rotateL x y | y < 0 = rotateR x (-y) | y == 0 = x - | True = liftSym1 (mkSymOp1 (Rol y)) (rot True (bitSize x) y) x + | True = let sz = bitSize x in liftSym1 (mkSymOp1 (Rol (y `mod` sz))) (rot True sz y) x rotateR x y | y < 0 = rotateL x (-y) | y == 0 = x - | True = liftSym1 (mkSymOp1 (Ror y)) (rot False (bitSize x) y) x + | True = let sz = bitSize x in liftSym1 (mkSymOp1 (Ror (y `mod` sz))) (rot False sz y) x -- Since the underlying representation is just Integers, rotations has to be careful on the bit-size rot :: Bool -> Int -> Int -> Integer -> Integer diff --git a/Data/SBV/BitVectors/STree.hs b/Data/SBV/BitVectors/STree.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/BitVectors/STree.hs @@ -0,0 +1,70 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.BitVectors.STree +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- Portability : portable +-- +-- Implementation of full-binary symbolic trees, providing logarithmic +-- time access to elements. Both reads and writes are supported. +----------------------------------------------------------------------------- + +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE FlexibleContexts #-} + +module Data.SBV.BitVectors.STree (STree, readSTree, writeSTree, mkSTree) where + +import Data.Bits (Bits(..)) + +import Data.SBV.BitVectors.Data +import Data.SBV.BitVectors.Model + +-- | 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) + +-- Internal representation, not exposed to the user +data STreeInternal i e = SLeaf e -- NB. parameter 'i' is phantom + | SBin (STreeInternal i e) (STreeInternal i e) + deriving Show + +instance (SymWord e, Mergeable (SBV e)) => Mergeable (STree i e) where + symbolicMerge b (SLeaf i) (SLeaf j) = SLeaf (ite b i j) + symbolicMerge b (SBin l r) (SBin l' r') = SBin (ite b l l') (ite b r r') + symbolicMerge _ _ _ = error $ "SBV.STree.symbolicMerge: Impossible happened while merging states" + +-- | 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 +readSTree s i = walk (blastBE i) s + where walk [] (SLeaf v) = v + walk (b:bs) (SBin l r) = ite b (walk bs r) (walk bs l) + walk _ _ = error $ "SBV.STree.readSTree: Impossible happened while reading: " ++ show i + +-- | 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 +writeSTree s i j = walk (blastBE i) s + where walk [] _ = SLeaf j + walk (b:bs) (SBin l r) = SBin (ite b l (walk bs l)) (ite b (walk bs r) r) + walk _ _ = error $ "SBV.STree.writeSTree: Impossible happened while reading: " ++ show i + +-- | Construct the fully balanced initial tree using the given values +mkSTree :: forall i e. HasSignAndSize i => [SBV e] -> STree i e +mkSTree ivals + | reqd /= given = error $ "SBV.STree.mkSTree: Required " ++ show reqd ++ " elements, received: " ++ show given + | True = go ivals + where reqd = 2 ^ (sizeOf (undefined :: i)) + given = length ivals + go [] = error $ "SBV.STree.mkSTree: Impossible happened, ran out of elements" + go [l] = SLeaf l + go ns = let (l, r) = splitAt (length ns `div` 2) ns in SBin (go l) (go r) diff --git a/Data/SBV/BitVectors/SignCast.hs b/Data/SBV/BitVectors/SignCast.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/BitVectors/SignCast.hs @@ -0,0 +1,111 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.BitVectors.SignCast +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- Portability : portable +-- +-- Implementation of casting between signed/unsigned variants of the +-- same type. +----------------------------------------------------------------------------- + +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE PatternGuards #-} + +module Data.SBV.BitVectors.SignCast (SignCast(..)) where + +import Data.Word (Word8, Word16, Word32, Word64) +import Data.Int (Int8, Int16, Int32, Int64) + +import Data.SBV.BitVectors.Data +import Data.SBV.BitVectors.Model() -- instances only + +-- | 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 where + -- | Interpret as a signed word + signCast :: a -> b + -- | Interpret as an unsigned word + unsignCast :: b -> a + +-- concrete instances +instance SignCast Word64 Int64 where + signCast = fromIntegral + unsignCast = fromIntegral + +instance SignCast Word32 Int32 where + signCast = fromIntegral + unsignCast = fromIntegral + +instance SignCast Word16 Int16 where + signCast = fromIntegral + unsignCast = fromIntegral + +instance SignCast Word8 Int8 where + signCast = fromIntegral + unsignCast = fromIntegral + +-- A generic implementation can be along the following lines: +-- fromBitsLE . blastLE +-- However, we prefer this version as the above will generate +-- a ton more code during compilation to SMT-Lib and C +genericSign :: (Integral a, SymWord a, Num b, SymWord b) => SBV a -> SBV b +genericSign x + | Just c <- unliteral x = literal $ fromIntegral c + | True = SBV sgsz (Right (cache y)) + where sgsz@(_, sz) = (True, sizeOf x) + y st = do xsw <- sbvToSW st x + newExpr st sgsz (SBVApp (Extract (sz-1) 0) [xsw]) + +-- Same comments as above, regarding the implementation. +genericUnsign :: (Integral a, SymWord a, Num b, SymWord b) => SBV a -> SBV b +genericUnsign x + | Just c <- unliteral x = literal $ fromIntegral c + | True = SBV sgsz (Right (cache y)) + where sgsz@(_, sz) = (False, sizeOf x) + y st = do xsw <- sbvToSW st x + newExpr st sgsz (SBVApp (Extract (sz-1) 0) [xsw]) + +-- symbolic instances +instance SignCast SWord8 SInt8 where + signCast = genericSign + unsignCast = genericUnsign + +instance SignCast SWord16 SInt16 where + signCast = genericSign + unsignCast = genericUnsign + +instance SignCast SWord32 SInt32 where + signCast = genericSign + unsignCast = genericUnsign + +instance SignCast SWord64 SInt64 where + signCast = genericSign + unsignCast = genericUnsign diff --git a/Data/SBV/BitVectors/Splittable.hs b/Data/SBV/BitVectors/Splittable.hs --- a/Data/SBV/BitVectors/Splittable.hs +++ b/Data/SBV/BitVectors/Splittable.hs @@ -72,7 +72,7 @@ -- symbolic instances instance Splittable SWord64 SWord32 where split (SBV _ (Left z)) = cwSplit z - split z = (SBV (False, 32) (Right (cache x)), SBV (False, 32) (Right (cache y))) + split z = (SBV (False, 32) (Right (cache x)), SBV (False, 32) (Right (cache y))) where x st = do zsw <- sbvToSW st z newExpr st (False, 32) (SBVApp (Extract 63 32) [zsw]) y st = do zsw <- sbvToSW st z @@ -86,7 +86,7 @@ instance Splittable SWord32 SWord16 where split (SBV _ (Left z)) = cwSplit z - split z = (SBV (False, 16) (Right (cache x)), SBV (False, 16) (Right (cache y))) + split z = (SBV (False, 16) (Right (cache x)), SBV (False, 16) (Right (cache y))) where x st = do zsw <- sbvToSW st z newExpr st (False, 16) (SBVApp (Extract 31 16) [zsw]) y st = do zsw <- sbvToSW st z diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs --- a/Data/SBV/Compilers/C.hs +++ b/Data/SBV/Compilers/C.hs @@ -461,6 +461,15 @@ extract 15 0 (False, 32) a = text "(SWord16)" <+> a extract 15 8 (False, 16) a = text "(SWord8)" <+> (parens (a <+> text ">> 8")) extract 7 0 (False, 16) a = text "(SWord8)" <+> a + -- the followings are used by sign-conversions. (Check instances in Data/SBV/BitVectors/SignCast.hs). + extract 63 0 (False, 64) a = text "(SInt64)" <+> a + extract 63 0 (True, 64) a = text "(SWord64)" <+> a + extract 31 0 (False, 32) a = text "(SInt32)" <+> a + extract 31 0 (True, 32) a = text "(SWord32)" <+> a + extract 15 0 (False, 16) a = text "(SInt16)" <+> a + extract 15 0 (True, 16) a = text "(SWord16)" <+> a + extract 7 0 (False, 8) a = text "(SInt8)" <+> a + extract 7 0 (True, 8) a = text "(SWord8)" <+> a extract i j (sg, sz) _ = tbd $ "extract with " ++ show (i, j, (sg, sz)) -- TBD: ditto here for join, just like extract above join ((False, 8), (False, 8), a, b) = parens ((parens (text "(SWord16)" <+> a)) <+> text "<< 8") <+> text "|" <+> parens (text "(SWord16)" <+> b) @@ -531,7 +540,7 @@ libh = libName ++ ".h" libd = libName ++ "_driver" os = map (flip replaceExtension ".o") fs - mkObj o f = text o <> text (":" ++ unwords [f, libh]) + mkObj o f = text o <> text (": " ++ unwords [f, libh]) $$ text "\t${CC} ${CCFLAGS} -c $< -o $@" $$ text "" diff --git a/Data/SBV/Examples/BitPrecise/Legato.hs b/Data/SBV/Examples/BitPrecise/Legato.hs --- a/Data/SBV/Examples/BitPrecise/Legato.hs +++ b/Data/SBV/Examples/BitPrecise/Legato.hs @@ -298,6 +298,6 @@ legatoInC = compileToC Nothing "runLegato" $ do x <- cgInput "x" y <- cgInput "y" - let (hi, lo) = runLegato (0, x) (1, y) 2 (initMachine (mkSFunArray 0) (0, 0, 0, false, false)) + let (hi, lo) = runLegato (0, x) (1, y) 2 (initMachine (mkSFunArray (const 0)) (0, 0, 0, false, false)) cgOutput "hi" hi cgOutput "lo" lo diff --git a/Data/SBV/Examples/BitPrecise/PrefixSum.hs b/Data/SBV/Examples/BitPrecise/PrefixSum.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Examples/BitPrecise/PrefixSum.hs @@ -0,0 +1,304 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Examples.BitPrecise.PrefixSum +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- Portability : portable +-- +-- The PrefixSum algorithm over power-lists and proof of +-- the Ladner-Fischer implementation. +-- See +-- and . +----------------------------------------------------------------------------- + +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Data.SBV.Examples.BitPrecise.PrefixSum where + +import Data.SBV +import Data.SBV.Internals(runSymbolic) + +---------------------------------------------------------------------- +-- * Formalizing power-lists +---------------------------------------------------------------------- + +-- | A poor man's representation of powerlists and +-- basic operations on them: . +-- We merely represent power-lists by ordinary lists. +type PowerList a = [a] + +-- | The tie operator, concatenation. +tiePL :: PowerList a -> PowerList a -> PowerList a +tiePL = (++) + +-- | 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 +zipPL [] [] = [] +zipPL (x:xs) (y:ys) = x : y : zipPL xs ys +zipPL _ _ = error "zipPL: nonsimilar powerlists received" + +-- | Inverse of zipping. +unzipPL :: PowerList a -> (PowerList a, PowerList a) +unzipPL = unzip . chunk2 + where chunk2 [] = [] + chunk2 (x:y:xs) = (x,y) : chunk2 xs + chunk2 _ = error "unzipPL: malformed powerlist" + +---------------------------------------------------------------------- +-- * Reference prefix-sum implementation +---------------------------------------------------------------------- + +-- | Reference prefix sum (@ps@) is simply Haskell's @scanl1@ function. +ps :: (a, a -> a -> a) -> PowerList a -> PowerList a +ps (_, f) = scanl1 f + +---------------------------------------------------------------------- +-- * The Ladner-Fischer parallel version +---------------------------------------------------------------------- + +-- | The Ladner-Fischer (@lf@) implementation of prefix-sum. See +-- or pg. 16 of . +lf :: (a, a -> a -> a) -> PowerList a -> PowerList a +lf _ [] = error "lf: malformed (empty) powerlist" +lf _ [x] = [x] +lf (zero, f) pl = zipPL (zipWith f (rsh lfpq) p) lfpq + where (p, q) = unzipPL pl + pq = zipWith f p q + lfpq = lf (zero, f) pq + rsh xs = zero : init xs + + +---------------------------------------------------------------------- +-- * Sample proofs for concrete operators +---------------------------------------------------------------------- + +-- | 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 +flIsCorrect n zf = do + args :: PowerList SWord32 <- mkFreeVars n + return $ ps zf args .== lf zf args + +-- | 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 +thm1 = prove $ flIsCorrect 8 (0, (+)) + +-- | 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 +thm2 = prove $ flIsCorrect 16 (0, smax) + +---------------------------------------------------------------------- +-- * Attempt at proving for arbitrary operators +---------------------------------------------------------------------- +-- | 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 +thm3 = prove $ do args :: PowerList SWord32 <- mkFreeVars 8 + return $ ps (u, op) args .== lf (u, op) args + where op :: SWord32 -> SWord32 -> SWord32 + op = uninterpret "flOp" + u :: SWord32 + u = uninterpret "u" + +---------------------------------------------------------------------- +-- * Proving for arbitrary operators using axioms +---------------------------------------------------------------------- +-- | 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 +genPrefixSumInstance n = do + args :: PowerList SWord32 <- mkFreeVars n + addAxiom "flOp is associative" $ assocAxiom (sbvUFName opH) + addAxiom "u is left-unit for flOp" $ leftUnitAxiom (sbvUFName opH) (sbvUFName uH) + return $ ps (u, op) args .== lf (u, op) args + where op :: SWord32 -> SWord32 -> SWord32 + opH :: SBVUF + (opH, op) = uninterpretWithHandle "flOp" + u :: SWord32 + uH :: SBVUF + (uH, u) = uninterpretWithHandle "u" + -- this is the brittle part; but it'll have to do until we get a proper + -- DSL for expressing SMT-axioms.. + mkCall :: String -> String -> String -> String + mkCall o x y = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")" + assocAxiom :: String -> [String] + assocAxiom o = [ + ":assumption (forall (?x BitVec[32]) (?y BitVec[32]) (?z BitVec[32])" + , " (= " ++ lhs + , " " ++ rhs + , " )" + , " )" + ] + where lhs = mkCall o (mkCall o "?x" "?y") "?z" + rhs = mkCall o "?x" (mkCall o "?y" "?z") + leftUnitAxiom :: String -> String -> [String] + leftUnitAxiom o ue = [ + ":assumption (forall (?x BitVec[32])" + , " (= " ++ lhs + , " " ++ rhs + , " )" + , " )" + ] + where lhs = "(" ++ o ++ " " ++ ue ++ " " ++ "?x" ++ ")" + rhs = "?x" + +-- | 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: . 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 +prefixSum i + -- Fast way of checking whether a number is a power of two, see: + | i <= 1 || (i .&. (i-1)) /= 0 + = error $ "prefixSum: input must be a power of 2 larger than 2, received: " ++ show i + | True + = proveWith cfg $ genPrefixSumInstance i + where cfg = defaultSMTCfg { solver = yices' } + yices' = yices { options = ["-tc", "-smt", "-e"] + , executable = "/usr/local/yices-1.0.29/bin/yices" + } + +---------------------------------------------------------------------- +-- * Inspecting symbolic traces +---------------------------------------------------------------------- + +-- | 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 () +ladnerFischerTrace n = gen >>= print + where gen = runSymbolic $ do args :: [SWord8] <- mkFreeVars n + mapM_ output $ lf (0, (+)) args + +-- | 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 () +scanlTrace n = gen >>= print + where gen = runSymbolic $ do args :: [SWord8] <- mkFreeVars n + mapM_ output $ ps (0, (+)) args diff --git a/Data/SBV/Examples/CodeGeneration/Fibonacci.hs b/Data/SBV/Examples/CodeGeneration/Fibonacci.hs --- a/Data/SBV/Examples/CodeGeneration/Fibonacci.hs +++ b/Data/SBV/Examples/CodeGeneration/Fibonacci.hs @@ -25,7 +25,7 @@ -- for concrete inputs: -- -- >>> map fib0 [0..6] --- [0 :: SWord32,1 :: SWord32,1 :: SWord32,2 :: SWord32,3 :: SWord32,5 :: SWord32,8 :: SWord32] +-- [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 @@ -34,7 +34,7 @@ -- 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 :: SWord32 -> SWord32 +fib0 :: SWord64 -> SWord64 fib0 n = ite (n .== 0 ||| n .== 1) n (fib0 (n-1) + fib0 (n-2)) @@ -53,14 +53,17 @@ -- | The recursion-depth limited version of fibonacci. Limiting the maximum number to be 20, we can say: -- -- >>> map (fib1 20) [0..6] --- [0 :: SWord32,1 :: SWord32,1 :: SWord32,2 :: SWord32,3 :: SWord32,5 :: SWord32,8 :: SWord32] +-- [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. -fib1 :: SWord32 -> SWord32 -> SWord32 +-- +-- 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 fib1 top n = fib' 0 1 0 - where fib' :: SWord32 -> SWord32 -> SWord32 -> SWord32 + where fib' :: SWord64 -> SWord64 -> SWord64 -> SWord64 fib' prev' prev m = ite (m .== top ||| m .== n) -- did we reach recursion depth, or the index we're looking for prev' -- stop and return the result (fib' prev (prev' + prev) (m+1)) -- otherwise recurse @@ -71,33 +74,33 @@ -- from the code generated for the call @genFib1 10@, where the code will work correctly -- for indexes up to 10: -- --- > SWord32 fib1(const SWord32 x) +-- > SWord64 fib1(const SWord64 x) -- > { --- > const SWord32 s0 = x; --- > const SBool s2 = s0 == 0x00000000UL; --- > const SBool s4 = s0 == 0x00000001UL; --- > const SBool s6 = s0 == 0x00000002UL; --- > const SBool s8 = s0 == 0x00000003UL; --- > const SBool s10 = s0 == 0x00000004UL; --- > const SBool s12 = s0 == 0x00000005UL; --- > const SBool s14 = s0 == 0x00000006UL; --- > const SBool s17 = s0 == 0x00000007UL; --- > const SBool s19 = s0 == 0x00000008UL; --- > const SBool s22 = s0 == 0x00000009UL; --- > const SWord32 s25 = s22 ? 0x00000022UL : 0x00000037UL; --- > const SWord32 s26 = s19 ? 0x00000015UL : s25; --- > const SWord32 s27 = s17 ? 0x0000000dUL : s26; --- > const SWord32 s28 = s14 ? 0x00000008UL : s27; --- > const SWord32 s29 = s12 ? 0x00000005UL : s28; --- > const SWord32 s30 = s10 ? 0x00000003UL : s29; --- > const SWord32 s31 = s8 ? 0x00000002UL : s30; --- > const SWord32 s32 = s6 ? 0x00000001UL : s31; --- > const SWord32 s33 = s4 ? 0x00000001UL : s32; --- > const SWord32 s34 = s2 ? 0x00000000UL : s33; +-- > 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 :: SWord32 -> IO () +genFib1 :: SWord64 -> IO () genFib1 top = compileToC Nothing "fib1" $ do x <- cgInput "x" cgReturn $ fib1 top x @@ -114,7 +117,7 @@ -- | Compute the fibonacci numbers statically at /code-generation/ time and -- put them in a table, accessed by the 'select' call. -fib2 :: SWord32 -> SWord32 -> SWord32 +fib2 :: SWord64 -> SWord64 -> SWord64 fib2 top n = select table 0 n where table = map (fib1 top) [0 .. top] @@ -125,33 +128,48 @@ -- naturally. (Note that this function returns @0@ if the index is larger -- than 64, as specified by the call to 'select' with default @0@.) -- --- > SWord32 fibLookup(const SWord32 x) +-- > SWord64 fibLookup(const SWord64 x) -- > { --- > const SWord32 s0 = x; --- > static const SWord32 table0[] = { --- > 0x00000000UL, 0x00000001UL, 0x00000001UL, 0x00000002UL, --- > 0x00000003UL, 0x00000005UL, 0x00000008UL, 0x0000000dUL, --- > 0x00000015UL, 0x00000022UL, 0x00000037UL, 0x00000059UL, --- > 0x00000090UL, 0x000000e9UL, 0x00000179UL, 0x00000262UL, --- > 0x000003dbUL, 0x0000063dUL, 0x00000a18UL, 0x00001055UL, --- > 0x00001a6dUL, 0x00002ac2UL, 0x0000452fUL, 0x00006ff1UL, --- > 0x0000b520UL, 0x00012511UL, 0x0001da31UL, 0x0002ff42UL, --- > 0x0004d973UL, 0x0007d8b5UL, 0x000cb228UL, 0x00148addUL, --- > 0x00213d05UL, 0x0035c7e2UL, 0x005704e7UL, 0x008cccc9UL, --- > 0x00e3d1b0UL, 0x01709e79UL, 0x02547029UL, 0x03c50ea2UL, --- > 0x06197ecbUL, 0x09de8d6dUL, 0x0ff80c38UL, 0x19d699a5UL, --- > 0x29cea5ddUL, 0x43a53f82UL, 0x6d73e55fUL, 0xb11924e1UL, --- > 0x1e8d0a40UL, 0xcfa62f21UL, 0xee333961UL, 0xbdd96882UL, --- > 0xac0ca1e3UL, 0x69e60a65UL, 0x15f2ac48UL, 0x7fd8b6adUL, --- > 0x95cb62f5UL, 0x15a419a2UL, 0xab6f7c97UL, 0xc1139639UL, --- > 0x6c8312d0UL, 0x2d96a909UL, 0x9a19bbd9UL, 0xc7b064e2UL, --- > 0x61ca20bbUL +-- > 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 SWord32 s65 = s0 >= 65 ? 0x00000000UL : table0[s0]; +-- > const SWord64 s65 = s0 >= 65 ? 0x0000000000000000ULL : table0[s0]; -- > -- > return s65; -- > } -genFib2 :: SWord32 -> IO () +genFib2 :: SWord64 -> IO () genFib2 top = compileToC Nothing "fibLookup" $ do cgPerformRTCs True -- protect against potential overflow, our table is not big enough x <- cgInput "x" diff --git a/Data/SBV/Examples/Crypto/AES.hs b/Data/SBV/Examples/Crypto/AES.hs --- a/Data/SBV/Examples/Crypto/AES.hs +++ b/Data/SBV/Examples/Crypto/AES.hs @@ -217,7 +217,7 @@ -- ** Tables for T-Box encryption ----------------------------------------------------------------------------- --- | T-box table generation function.for encryption +-- | T-box table generation function for encryption t0Func :: GF28 -> [GF28] t0Func a = [s `gf28Mult` 2, s, s, s `gf28Mult` 3] where s = sbox a diff --git a/Data/SBV/Examples/Crypto/RC4.hs b/Data/SBV/Examples/Crypto/RC4.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Examples/Crypto/RC4.hs @@ -0,0 +1,145 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Examples.Crypto.RC4 +-- Copyright : (c) Austin Seipp +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- Portability : portable +-- +-- An implementation of RC4 (AKA Rivest Cipher 4 or Alleged RC4/ARC4), +-- using SBV. For information on RC4, see: . +-- +-- 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. +----------------------------------------------------------------------------- + +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE PatternGuards #-} + +module Data.SBV.Examples.Crypto.RC4 where + +import Data.Char (ord, chr) +import Data.List (genericIndex) +import Data.Maybe (fromJust) +import Data.SBV + +----------------------------------------------------------------------------- +-- * Types +----------------------------------------------------------------------------- + +-- | 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 +initS = mkSTree (map literal [0 .. 255]) + +-- | 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) + +----------------------------------------------------------------------------- +-- * The PRGA +----------------------------------------------------------------------------- + +-- | Swaps two elements in the RC4 array. +swap :: SWord8 -> SWord8 -> S -> S +swap i j st = writeSTree (writeSTree st i stj) j sti + where sti = readSTree st i + stj = readSTree st j + +-- | Implements the PRGA used in RC4. We return the new state and the next key value generated. +prga :: RC4 -> (SWord8, RC4) +prga (st', i', j') = (readSTree st kInd, (st, i, j)) + where i = i' + 1 + j = j' + readSTree st' i + st = swap i j st' + kInd = readSTree st i + readSTree st j + +----------------------------------------------------------------------------- +-- * Key schedule +----------------------------------------------------------------------------- + +-- | Constructs the state to be used by the PRGA using the given key. +initRC4 :: Key -> S +initRC4 key + | keyLength < 1 || keyLength > 256 + = error $ "RC4 requires a key of length between 1 and 256, received: " ++ show keyLength + | True + = snd $ foldl mix (0, initS) [0..255] + where keyLength = length key + mix :: (SWord8, S) -> SWord8 -> (SWord8, S) + mix (j', s) i = let j = j' + readSTree s i + genericIndex key (fromJust (unliteral i) `mod` fromIntegral keyLength) + in (j, swap i j s) + +-- | The key-schedule. Note that this function returns an infinite list. +keySchedule :: Key -> [SWord8] +keySchedule key = genKeys (initRC4 key, 0, 0) + where genKeys :: RC4 -> [SWord8] + genKeys st = let (k, st') = prga st in k : genKeys st' + +-- | Generate a key-schedule from a given key-string. +keyScheduleString :: String -> [SWord8] +keyScheduleString = keySchedule . map (literal . fromIntegral . ord) + +----------------------------------------------------------------------------- +-- * Encryption and Decryption +----------------------------------------------------------------------------- + +-- | RC4 encryption. We generate key-words and xor it with the input. The +-- following test-vectors are from Wikipedia : +-- +-- >>> concatMap hex $ encrypt "Key" "Plaintext" +-- "bbf316e8d940af0ad3" +-- +-- >>> concatMap hex $ encrypt "Wiki" "pedia" +-- "1021bf0420" +-- +-- >>> concatMap hex $ encrypt "Secret" "Attack at dawn" +-- "45a01f645fc35b383552544b9bf5" +encrypt :: String -> String -> [SWord8] +encrypt key pt = zipWith xor (keyScheduleString key) (map cvt pt) + where cvt = literal . fromIntegral . ord + +-- | 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 +decrypt key ct = map cvt $ zipWith xor (keyScheduleString key) ct + where cvt = chr . fromIntegral . fromJust . unliteral + +----------------------------------------------------------------------------- +-- * Verification +----------------------------------------------------------------------------- + +-- | 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 +rc4IsCorrect = prove $ do + key <- mkFreeVars 5 + pt <- mkFreeVars 5 + let ks = keySchedule key + ct = zipWith xor ks pt + pt' = zipWith xor ks ct + return $ pt .== pt' diff --git a/Data/SBV/Examples/PrefixSum/PrefixSum.hs b/Data/SBV/Examples/PrefixSum/PrefixSum.hs deleted file mode 100644 --- a/Data/SBV/Examples/PrefixSum/PrefixSum.hs +++ /dev/null @@ -1,304 +0,0 @@ ------------------------------------------------------------------------------ --- | --- Module : Data.SBV.Examples.PrefixSum.PrefixSum --- Copyright : (c) Levent Erkok --- License : BSD3 --- Maintainer : erkokl@gmail.com --- Stability : experimental --- Portability : portable --- --- The PrefixSum algorithm over power-lists and proof of --- the Ladner-Fischer implementation. --- See --- and . ------------------------------------------------------------------------------ - -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE ScopedTypeVariables #-} - -module Data.SBV.Examples.PrefixSum.PrefixSum where - -import Data.SBV -import Data.SBV.Internals(runSymbolic) - ----------------------------------------------------------------------- --- * Formalizing power-lists ----------------------------------------------------------------------- - --- | A poor man's representation of powerlists and --- basic operations on them: . --- We merely represent power-lists by ordinary lists. -type PowerList a = [a] - --- | The tie operator, concatenation -tiePL :: PowerList a -> PowerList a -> PowerList a -tiePL = (++) - --- | 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 -zipPL [] [] = [] -zipPL (x:xs) (y:ys) = x : y : zipPL xs ys -zipPL _ _ = error "zipPL: nonsimilar powerlists received" - --- | Inverse of zipping -unzipPL :: PowerList a -> (PowerList a, PowerList a) -unzipPL = unzip . chunk2 - where chunk2 [] = [] - chunk2 (x:y:xs) = (x,y) : chunk2 xs - chunk2 _ = error "unzipPL: malformed powerlist" - ----------------------------------------------------------------------- --- * Reference prefix-sum implementation ----------------------------------------------------------------------- - --- | Reference prefix sum (@ps@) is simply Haskell's @scanl1@ function -ps :: (a, a -> a -> a) -> PowerList a -> PowerList a -ps (_, f) = scanl1 f - ----------------------------------------------------------------------- --- * The Ladner-Fischer parallel version ----------------------------------------------------------------------- - --- | The Ladner-Fischer (@lf@) implementation of prefix-sum. See --- or pg. 16 of . -lf :: (a, a -> a -> a) -> PowerList a -> PowerList a -lf _ [] = error "lf: malformed (empty) powerlist" -lf _ [x] = [x] -lf (zero, f) pl = zipPL (zipWith f (rsh lfpq) p) lfpq - where (p, q) = unzipPL pl - pq = zipWith f p q - lfpq = lf (zero, f) pq - rsh xs = zero : init xs - - ----------------------------------------------------------------------- --- * Sample proofs for concrete operators ----------------------------------------------------------------------- - --- | 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 -flIsCorrect n zf = do - args :: PowerList SWord32 <- mkFreeVars n - return $ ps zf args .== lf zf args - --- | 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 -thm1 = prove $ flIsCorrect 8 (0, (+)) - --- | 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 -thm2 = prove $ flIsCorrect 16 (0, smax) - ----------------------------------------------------------------------- --- * Attempt at proving for arbitrary operators ----------------------------------------------------------------------- --- | 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 --- --- >>> 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 -thm3 = prove $ do args :: PowerList SWord32 <- mkFreeVars 8 - return $ ps (u, op) args .== lf (u, op) args - where op :: SWord32 -> SWord32 -> SWord32 - op = uninterpret "flOp" - u :: SWord32 - u = uninterpret "u" - ----------------------------------------------------------------------- --- * Proving for arbitrary operators using axioms ----------------------------------------------------------------------- --- | 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 -genPrefixSumInstance n = do - args :: PowerList SWord32 <- mkFreeVars n - addAxiom "flOp is associative" $ assocAxiom (sbvUFName opH) - addAxiom "u is left-unit for flOp" $ leftUnitAxiom (sbvUFName opH) (sbvUFName uH) - return $ ps (u, op) args .== lf (u, op) args - where op :: SWord32 -> SWord32 -> SWord32 - opH :: SBVUF - (opH, op) = uninterpretWithHandle "flOp" - u :: SWord32 - uH :: SBVUF - (uH, u) = uninterpretWithHandle "u" - -- this is the brittle part; but it'll have to do until we get a proper - -- DSL for expressing SMT-axioms.. - mkCall :: String -> String -> String -> String - mkCall o x y = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")" - assocAxiom :: String -> [String] - assocAxiom o = [ - ":assumption (forall (?x BitVec[32]) (?y BitVec[32]) (?z BitVec[32])" - , " (= " ++ lhs - , " " ++ rhs - , " )" - , " )" - ] - where lhs = mkCall o (mkCall o "?x" "?y") "?z" - rhs = mkCall o "?x" (mkCall o "?y" "?z") - leftUnitAxiom :: String -> String -> [String] - leftUnitAxiom o ue = [ - ":assumption (forall (?x BitVec[32])" - , " (= " ++ lhs - , " " ++ rhs - , " )" - , " )" - ] - where lhs = "(" ++ o ++ " " ++ ue ++ " " ++ "?x" ++ ")" - rhs = "?x" - --- | 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: . 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-1.0.28 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 -prefixSum i - -- Fast way of checking whether a number is a power of two, see: - | i <= 1 || (i .&. (i-1)) /= 0 - = error $ "prefixSum: input must be a power of 2 larger than 2, received: " ++ show i - | True - = proveWith cfg $ genPrefixSumInstance i - where cfg = defaultSMTCfg { solver = yices' } - yices' = yices { options = ["-tc", "-smt", "-e"] - , executable = "/usr/local/yices-1.0.28/bin/yices" - } - ----------------------------------------------------------------------- --- * Inspecting symbolic traces ----------------------------------------------------------------------- - --- | 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 () -ladnerFischerTrace n = gen >>= print - where gen = runSymbolic $ do args :: [SWord8] <- mkFreeVars n - mapM_ output $ lf (0, (+)) args - --- | 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 () -scanlTrace n = gen >>= print - where gen = runSymbolic $ do args :: [SWord8] <- mkFreeVars n - mapM_ output $ ps (0, (+)) args diff --git a/Data/SBV/Examples/Puzzles/Counts.hs b/Data/SBV/Examples/Puzzles/Counts.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Examples/Puzzles/Counts.hs @@ -0,0 +1,84 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Examples.Puzzles.Counts +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- Portability : portable +-- +-- 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: +-- +-- * Douglas Hofstadter, Metamagical Themes, pg. 27. +-- +-- * +-- +----------------------------------------------------------------------------- + +module Data.SBV.Examples.Puzzles.Counts where + +import Data.SBV + +-- | 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 +count n cnts = ite (n .< 10) + (upd n cnts) -- only one digit + (ite (n .< 100) + (upd d1 (upd d2 cnts)) -- two digits + (upd d1 (upd d2 (upd d3 cnts)))) -- three digits + where (r1, d1) = n `bvQuotRem` 10 + (d3, d2) = r1 `bvQuotRem` 10 + upd d vals = zipWith inc [0..] vals + where inc i c = ite (i .== d) (c+1) c + +-- | 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 +puzzle cnt = cnt .== last css + where ones = replicate 10 1 -- all digits occur once to start with + css = [ones] ++ zipWith count cnt css + +-- | 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 () +solve = do res <- allSat $ mkFreeVars 10 >>= return . puzzle + cnt <- displayModels disp res + putStrLn $ "Found: " ++ show cnt ++ " solution(s)." + where disp n s = do putStrLn $ "Solution #" ++ show n + dispSolution s + dispSolution :: [Word8] -> IO () + dispSolution ns = putStrLn soln + where soln = "In this sentence, the number of occurrences" + ++ " of 0 is " ++ show (ns !! 0) + ++ ", of 1 is " ++ show (ns !! 1) + ++ ", of 2 is " ++ show (ns !! 2) + ++ ", of 3 is " ++ show (ns !! 3) + ++ ", of 4 is " ++ show (ns !! 4) + ++ ", of 5 is " ++ show (ns !! 5) + ++ ", of 6 is " ++ show (ns !! 6) + ++ ", of 7 is " ++ show (ns !! 7) + ++ ", of 8 is " ++ show (ns !! 8) + ++ ", of 9 is " ++ show (ns !! 9) + ++ "." diff --git a/Data/SBV/Internals.hs b/Data/SBV/Internals.hs --- a/Data/SBV/Internals.hs +++ b/Data/SBV/Internals.hs @@ -16,7 +16,7 @@ -- * Running symbolic programs /manually/ Result, runSymbolic -- * Other internal structures useful for low-level programming - , SBV(..), CW, mkConstCW, genFree, genFree_ + , SBV(..), HasSignAndSize(..), CW, mkConstCW, genFree, genFree_ -- * Compilation to C , compileToC', compileToCLib', CgPgmBundle(..), CgPgmKind(..) -- * Integrating with the test framework @@ -24,7 +24,7 @@ , module Data.SBV.Utils.SBVTest ) where -import Data.SBV.BitVectors.Data (Result, runSymbolic, SBV(..), CW, mkConstCW) +import Data.SBV.BitVectors.Data (Result, runSymbolic, SBV(..), HasSignAndSize(..), CW, mkConstCW) import Data.SBV.BitVectors.Model (genFree, genFree_) import Data.SBV.Compilers.C (compileToC', compileToCLib') import Data.SBV.Compilers.CodeGen (CgPgmBundle(..), CgPgmKind(..)) diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -303,7 +303,13 @@ Result is consts tbls arrs uis axs pgm [o@(SW (False, 1) _)] | sizeOf o == 1 -> timeIf isTiming "translation" $ let uiMap = catMaybes (map arrayUIKind arrs) ++ map unintFnUIKind uis in return (is, uiMap, toSMTLib isSat comments is consts tbls arrs uis axs pgm o) - _ -> error $ "SBVProver.generateTrace: Impossible happened:\n" ++ show res + Result _is _consts _tbls _arrs _uis _axs _pgm os -> case length os of + 0 -> error $ "Impossible happened, unexpected non-outputting result\n" ++ show res + 1 -> error $ "Impossible happened, non-boolean output in " ++ show os + ++ "\nDetected while generating the trace:\n" ++ show res + _ -> error $ "User error: Multiple output values detected: " ++ show os + ++ "\nDetected while generating the trace:\n" ++ show res + ++ "\n*** Check calls to \"output\", they are typically not needed!" -- | Equality as a proof method. Allows for -- very concise construction of equivalence proofs, which is very typical in diff --git a/Data/SBV/TestSuite/Basics/Arithmetic.hs b/Data/SBV/TestSuite/Basics/Arithmetic.hs --- a/Data/SBV/TestSuite/Basics/Arithmetic.hs +++ b/Data/SBV/TestSuite/Basics/Arithmetic.hs @@ -40,6 +40,7 @@ ++ genIntTest "rotateL" rotateL ++ genIntTest "rotateR" rotateR ++ genBlasts + ++ genCasts genBinTest :: String -> (forall a. Bits a => a -> a -> a) -> [Test] genBinTest nm op = map mkTest $ @@ -87,19 +88,41 @@ ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw8s ] ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si8s ] ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si8s ] - ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw16s ] - ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw16s ] - ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si16s ] - ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si16s ] - ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw32s ] - ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw32s ] - ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si32s ] - ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si32s ] - ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw64s ] - ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw64s ] - ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si64s ] - ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si64s ] + ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw16s] + ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw16s] + ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si16s] + ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si16s] + ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw32s] + ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw32s] + ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si32s] + ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si32s] + ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw64s] + ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw64s] + ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si64s] + ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si64s] where mkTest (x, r) = "blast-" ++ show x ~: r `showsAs` "True" + +genCasts :: [Test] +genCasts = map mkTest $ + [(show x, unsignCast (signCast x) .== x) | x <- sw8s ] + ++ [(show x, unsignCast (signCast x) .== x) | x <- sw16s] + ++ [(show x, unsignCast (signCast x) .== x) | x <- sw32s] + ++ [(show x, unsignCast (signCast x) .== x) | x <- sw64s] + ++ [(show x, signCast (unsignCast x) .== x) | x <- si8s ] + ++ [(show x, signCast (unsignCast x) .== x) | x <- si16s] + ++ [(show x, signCast (unsignCast x) .== x) | x <- si8s ] + ++ [(show x, signCast (unsignCast x) .== x) | x <- si16s] + ++ [(show x, signCast (unsignCast x) .== x) | x <- si32s] + ++ [(show x, signCast (unsignCast x) .== x) | x <- si64s] + ++ [(show x, signCast x .== fromBitsLE (blastLE x)) | x <- sw8s ] + ++ [(show x, signCast x .== fromBitsLE (blastLE x)) | x <- sw16s] + ++ [(show x, signCast x .== fromBitsLE (blastLE x)) | x <- sw32s] + ++ [(show x, signCast x .== fromBitsLE (blastLE x)) | x <- sw64s] + ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si8s ] + ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si16s] + ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si32s] + ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si64s] + where mkTest (x, r) = "cast-" ++ show x ~: r `showsAs` "True" -- Concrete test data xsSigned, xsUnsigned :: (Num a, Enum a, Bounded a) => [a] diff --git a/Data/SBV/TestSuite/BitPrecise/Legato.hs b/Data/SBV/TestSuite/BitPrecise/Legato.hs --- a/Data/SBV/TestSuite/BitPrecise/Legato.hs +++ b/Data/SBV/TestSuite/BitPrecise/Legato.hs @@ -29,6 +29,6 @@ cgPerformRTCs True x <- cgInput "x" y <- cgInput "y" - let (hi, lo) = runLegato (0, x) (1, y) 2 (initMachine (mkSFunArray 0) (0, 0, 0, false, false)) + let (hi, lo) = runLegato (0, x) (1, y) 2 (initMachine (mkSFunArray (const 0)) (0, 0, 0, false, false)) cgOutput "hi" hi cgOutput "lo" lo diff --git a/Data/SBV/TestSuite/BitPrecise/PrefixSum.hs b/Data/SBV/TestSuite/BitPrecise/PrefixSum.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/TestSuite/BitPrecise/PrefixSum.hs @@ -0,0 +1,25 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.TestSuite.BitPrecise.PrefixSum +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- Portability : portable +-- +-- Test suite for Data.SBV.Examples.PrefixSum.PrefixSum +----------------------------------------------------------------------------- + +module Data.SBV.TestSuite.BitPrecise.PrefixSum(testSuite) where + +import Data.SBV +import Data.SBV.Internals +import Data.SBV.Examples.BitPrecise.PrefixSum + +-- Test suite +testSuite :: SBVTestSuite +testSuite = mkTestSuite $ \goldCheck -> test [ + "prefixSum1" ~: assert =<< isTheorem (flIsCorrect 8 (0, (+))) + , "prefixSum2" ~: assert =<< isTheorem (flIsCorrect 16 (0, smax)) + , "prefixSum3" ~: runSymbolic (genPrefixSumInstance 16 >>= output) `goldCheck` "prefixSum_16.gold" + ] diff --git a/Data/SBV/TestSuite/Crypto/AES.hs b/Data/SBV/TestSuite/Crypto/AES.hs --- a/Data/SBV/TestSuite/Crypto/AES.hs +++ b/Data/SBV/TestSuite/Crypto/AES.hs @@ -7,7 +7,7 @@ -- Stability : experimental -- Portability : portable -- --- Test suite for Data.SBV.Examples.CodeGeneration.AES +-- Test suite for Data.SBV.Examples.Crypto.AES ----------------------------------------------------------------------------- module Data.SBV.TestSuite.Crypto.AES(testSuite) where diff --git a/Data/SBV/TestSuite/Crypto/RC4.hs b/Data/SBV/TestSuite/Crypto/RC4.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/TestSuite/Crypto/RC4.hs @@ -0,0 +1,24 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.TestSuite.Crypto.RC4 +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- Portability : portable +-- +-- Test suite for Data.SBV.Examples.Crypto.RC4 +----------------------------------------------------------------------------- + +module Data.SBV.TestSuite.Crypto.RC4(testSuite) where + +import Data.SBV +import Data.SBV.Internals +import Data.SBV.Examples.Crypto.RC4 + +-- Test suite +testSuite :: SBVTestSuite +testSuite = mkTestSuite $ \_ -> test [ + "rc4swap" ~: assert =<< isTheorem readWrite + ] + where readWrite i j = readSTree (writeSTree initS i j) i .== j diff --git a/Data/SBV/TestSuite/PrefixSum/PrefixSum.hs b/Data/SBV/TestSuite/PrefixSum/PrefixSum.hs deleted file mode 100644 --- a/Data/SBV/TestSuite/PrefixSum/PrefixSum.hs +++ /dev/null @@ -1,25 +0,0 @@ ------------------------------------------------------------------------------ --- | --- Module : Data.SBV.TestSuite.PrefixSum.PrefixSum --- Copyright : (c) Levent Erkok --- License : BSD3 --- Maintainer : erkokl@gmail.com --- Stability : experimental --- Portability : portable --- --- Test suite for Data.SBV.Examples.PrefixSum.PrefixSum ------------------------------------------------------------------------------ - -module Data.SBV.TestSuite.PrefixSum.PrefixSum(testSuite) where - -import Data.SBV -import Data.SBV.Internals -import Data.SBV.Examples.PrefixSum.PrefixSum - --- Test suite -testSuite :: SBVTestSuite -testSuite = mkTestSuite $ \goldCheck -> test [ - "prefixSum1" ~: assert =<< isTheorem (flIsCorrect 8 (0, (+))) - , "prefixSum2" ~: assert =<< isTheorem (flIsCorrect 16 (0, smax)) - , "prefixSum3" ~: runSymbolic (genPrefixSumInstance 16 >>= output) `goldCheck` "prefixSum_16.gold" - ] diff --git a/README b/README --- a/README +++ b/README @@ -62,8 +62,7 @@ all satisfying assignments, lazily. The SBV library can also compile Haskell functions that manipulate symbolic -values directly to C, rendering them as straight-line C programs that can be -executed in, say, embedded platforms. +values directly to C, rendering them as straight-line C programs. Use of SMT solvers ================== @@ -120,4 +119,4 @@ by providing time and computing machinery. The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways: -Ian Blumenfeld, Iavor Diatchki, Lee Pike, Austin Seipp, Don Stewart, and Josef Svenningsson. +Ian Blumenfeld, Ian Calvert, Iavor Diatchki, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann. diff --git a/SBVUnitTest/GoldFiles/aes128Lib.gold b/SBVUnitTest/GoldFiles/aes128Lib.gold --- a/SBVUnitTest/GoldFiles/aes128Lib.gold +++ b/SBVUnitTest/GoldFiles/aes128Lib.gold @@ -3746,13 +3746,13 @@ aes128Lib_driver: aes128Lib_driver.c aes128Lib.h ${CC} ${CCFLAGS} $< -o $@ aes128Lib.a -aes128KeySchedule.o:aes128KeySchedule.c aes128Lib.h +aes128KeySchedule.o: aes128KeySchedule.c aes128Lib.h ${CC} ${CCFLAGS} -c $< -o $@ -aes128BlockEncrypt.o:aes128BlockEncrypt.c aes128Lib.h +aes128BlockEncrypt.o: aes128BlockEncrypt.c aes128Lib.h ${CC} ${CCFLAGS} -c $< -o $@ -aes128BlockDecrypt.o:aes128BlockDecrypt.c aes128Lib.h +aes128BlockDecrypt.o: aes128BlockDecrypt.c aes128Lib.h ${CC} ${CCFLAGS} -c $< -o $@ clean: diff --git a/SBVUnitTest/GoldFiles/counts.gold b/SBVUnitTest/GoldFiles/counts.gold new file mode 100644 --- /dev/null +++ b/SBVUnitTest/GoldFiles/counts.gold @@ -0,0 +1,1702 @@ +INPUTS + s0 :: SWord8 + s1 :: SWord8 + s2 :: SWord8 + s3 :: SWord8 + s4 :: SWord8 + s5 :: SWord8 + s6 :: SWord8 + s7 :: SWord8 + s8 :: SWord8 + s9 :: SWord8 +CONSTANTS + s_2 = False + s_1 = True + s10 = 10 :: SWord8 + s12 = 0 :: SWord8 + s32 = 2 :: SWord8 + s33 = 1 :: SWord8 + s35 = 100 :: SWord8 + s555 = 3 :: SWord8 + s716 = 4 :: SWord8 + s877 = 5 :: SWord8 + s1038 = 6 :: SWord8 + s1199 = 7 :: SWord8 + s1360 = 8 :: SWord8 + s1521 = 9 :: SWord8 +TABLES +ARRAYS +UNINTERPRETED CONSTANTS +AXIOMS +DEFINE + s11 :: SBool = s9 < s10 + s13 :: SBool = s9 == s12 + s14 :: SBool = s8 < s10 + s15 :: SBool = s8 == s12 + s16 :: SBool = s7 < s10 + s17 :: SBool = s7 == s12 + s18 :: SBool = s6 < s10 + s19 :: SBool = s6 == s12 + s20 :: SBool = s5 < s10 + s21 :: SBool = s5 == s12 + s22 :: SBool = s4 < s10 + s23 :: SBool = s4 == s12 + s24 :: SBool = s3 < s10 + s25 :: SBool = s3 == s12 + s26 :: SBool = s2 < s10 + s27 :: SBool = s2 == s12 + s28 :: SBool = s1 < s10 + s29 :: SBool = s1 == s12 + s30 :: SBool = s0 < s10 + s31 :: SBool = s0 == s12 + s34 :: SWord8 = if s31 then s32 else s33 + s36 :: SBool = s0 < s35 + s37 :: SWord8 = s0 rem s10 + s38 :: SBool = s12 == s37 + s39 :: SWord8 = s0 quot s10 + s40 :: SWord8 = s39 rem s10 + s41 :: SBool = s12 == s40 + s42 :: SWord8 = if s41 then s32 else s33 + s43 :: SWord8 = s33 + s42 + s44 :: SWord8 = if s38 then s43 else s42 + s45 :: SWord8 = s39 quot s10 + s46 :: SBool = s12 == s45 + s47 :: SWord8 = if s46 then s32 else s33 + s48 :: SWord8 = s33 + s47 + s49 :: SWord8 = if s41 then s48 else s47 + s50 :: SWord8 = s33 + s49 + s51 :: SWord8 = if s38 then s50 else s49 + s52 :: SWord8 = if s36 then s44 else s51 + s53 :: SWord8 = if s30 then s34 else s52 + s54 :: SWord8 = s33 + s53 + s55 :: SWord8 = if s29 then s54 else s53 + s56 :: SBool = s1 < s35 + s57 :: SWord8 = s1 rem s10 + s58 :: SBool = s12 == s57 + s59 :: SWord8 = s1 quot s10 + s60 :: SWord8 = s59 rem s10 + s61 :: SBool = s12 == s60 + s62 :: SWord8 = if s61 then s54 else s53 + s63 :: SWord8 = s33 + s62 + s64 :: SWord8 = if s58 then s63 else s62 + s65 :: SWord8 = s59 quot s10 + s66 :: SBool = s12 == s65 + s67 :: SWord8 = if s66 then s54 else s53 + s68 :: SWord8 = s33 + s67 + s69 :: SWord8 = if s61 then s68 else s67 + s70 :: SWord8 = s33 + s69 + s71 :: SWord8 = if s58 then s70 else s69 + s72 :: SWord8 = if s56 then s64 else s71 + s73 :: SWord8 = if s28 then s55 else s72 + s74 :: SWord8 = s33 + s73 + s75 :: SWord8 = if s27 then s74 else s73 + s76 :: SBool = s2 < s35 + s77 :: SWord8 = s2 rem s10 + s78 :: SBool = s12 == s77 + s79 :: SWord8 = s2 quot s10 + s80 :: SWord8 = s79 rem s10 + s81 :: SBool = s12 == s80 + s82 :: SWord8 = if s81 then s74 else s73 + s83 :: SWord8 = s33 + s82 + s84 :: SWord8 = if s78 then s83 else s82 + s85 :: SWord8 = s79 quot s10 + s86 :: SBool = s12 == s85 + s87 :: SWord8 = if s86 then s74 else s73 + s88 :: SWord8 = s33 + s87 + s89 :: SWord8 = if s81 then s88 else s87 + s90 :: SWord8 = s33 + s89 + s91 :: SWord8 = if s78 then s90 else s89 + s92 :: SWord8 = if s76 then s84 else s91 + s93 :: SWord8 = if s26 then s75 else s92 + s94 :: SWord8 = s33 + s93 + s95 :: SWord8 = if s25 then s94 else s93 + s96 :: SBool = s3 < s35 + s97 :: SWord8 = s3 rem s10 + s98 :: SBool = s12 == s97 + s99 :: SWord8 = s3 quot s10 + s100 :: SWord8 = s99 rem s10 + s101 :: SBool = s12 == s100 + s102 :: SWord8 = if s101 then s94 else s93 + s103 :: SWord8 = s33 + s102 + s104 :: SWord8 = if s98 then s103 else s102 + s105 :: SWord8 = s99 quot s10 + s106 :: SBool = s12 == s105 + s107 :: SWord8 = if s106 then s94 else s93 + s108 :: SWord8 = s33 + s107 + s109 :: SWord8 = if s101 then s108 else s107 + s110 :: SWord8 = s33 + s109 + s111 :: SWord8 = if s98 then s110 else s109 + s112 :: SWord8 = if s96 then s104 else s111 + s113 :: SWord8 = if s24 then s95 else s112 + s114 :: SWord8 = s33 + s113 + s115 :: SWord8 = if s23 then s114 else s113 + s116 :: SBool = s4 < s35 + s117 :: SWord8 = s4 rem s10 + s118 :: SBool = s12 == s117 + s119 :: SWord8 = s4 quot s10 + s120 :: SWord8 = s119 rem s10 + s121 :: SBool = s12 == s120 + s122 :: SWord8 = if s121 then s114 else s113 + s123 :: SWord8 = s33 + s122 + s124 :: SWord8 = if s118 then s123 else s122 + s125 :: SWord8 = s119 quot s10 + s126 :: SBool = s12 == s125 + s127 :: SWord8 = if s126 then s114 else s113 + s128 :: SWord8 = s33 + s127 + s129 :: SWord8 = if s121 then s128 else s127 + s130 :: SWord8 = s33 + s129 + s131 :: SWord8 = if s118 then s130 else s129 + s132 :: SWord8 = if s116 then s124 else s131 + s133 :: SWord8 = if s22 then s115 else s132 + s134 :: SWord8 = s33 + s133 + s135 :: SWord8 = if s21 then s134 else s133 + s136 :: SBool = s5 < s35 + s137 :: SWord8 = s5 rem s10 + s138 :: SBool = s12 == s137 + s139 :: SWord8 = s5 quot s10 + s140 :: SWord8 = s139 rem s10 + s141 :: SBool = s12 == s140 + s142 :: SWord8 = if s141 then s134 else s133 + s143 :: SWord8 = s33 + s142 + s144 :: SWord8 = if s138 then s143 else s142 + s145 :: SWord8 = s139 quot s10 + s146 :: SBool = s12 == s145 + s147 :: SWord8 = if s146 then s134 else s133 + s148 :: SWord8 = s33 + s147 + s149 :: SWord8 = if s141 then s148 else s147 + s150 :: SWord8 = s33 + s149 + s151 :: SWord8 = if s138 then s150 else s149 + s152 :: SWord8 = if s136 then s144 else s151 + s153 :: SWord8 = if s20 then s135 else s152 + s154 :: SWord8 = s33 + s153 + s155 :: SWord8 = if s19 then s154 else s153 + s156 :: SBool = s6 < s35 + s157 :: SWord8 = s6 rem s10 + s158 :: SBool = s12 == s157 + s159 :: SWord8 = s6 quot s10 + s160 :: SWord8 = s159 rem s10 + s161 :: SBool = s12 == s160 + s162 :: SWord8 = if s161 then s154 else s153 + s163 :: SWord8 = s33 + s162 + s164 :: SWord8 = if s158 then s163 else s162 + s165 :: SWord8 = s159 quot s10 + s166 :: SBool = s12 == s165 + s167 :: SWord8 = if s166 then s154 else s153 + s168 :: SWord8 = s33 + s167 + s169 :: SWord8 = if s161 then s168 else s167 + s170 :: SWord8 = s33 + s169 + s171 :: SWord8 = if s158 then s170 else s169 + s172 :: SWord8 = if s156 then s164 else s171 + s173 :: SWord8 = if s18 then s155 else s172 + s174 :: SWord8 = s33 + s173 + s175 :: SWord8 = if s17 then s174 else s173 + s176 :: SBool = s7 < s35 + s177 :: SWord8 = s7 rem s10 + s178 :: SBool = s12 == s177 + s179 :: SWord8 = s7 quot s10 + s180 :: SWord8 = s179 rem s10 + s181 :: SBool = s12 == s180 + s182 :: SWord8 = if s181 then s174 else s173 + s183 :: SWord8 = s33 + s182 + s184 :: SWord8 = if s178 then s183 else s182 + s185 :: SWord8 = s179 quot s10 + s186 :: SBool = s12 == s185 + s187 :: SWord8 = if s186 then s174 else s173 + s188 :: SWord8 = s33 + s187 + s189 :: SWord8 = if s181 then s188 else s187 + s190 :: SWord8 = s33 + s189 + s191 :: SWord8 = if s178 then s190 else s189 + s192 :: SWord8 = if s176 then s184 else s191 + s193 :: SWord8 = if s16 then s175 else s192 + s194 :: SWord8 = s33 + s193 + s195 :: SWord8 = if s15 then s194 else s193 + s196 :: SBool = s8 < s35 + s197 :: SWord8 = s8 rem s10 + s198 :: SBool = s12 == s197 + s199 :: SWord8 = s8 quot s10 + s200 :: SWord8 = s199 rem s10 + s201 :: SBool = s12 == s200 + s202 :: SWord8 = if s201 then s194 else s193 + s203 :: SWord8 = s33 + s202 + s204 :: SWord8 = if s198 then s203 else s202 + s205 :: SWord8 = s199 quot s10 + s206 :: SBool = s12 == s205 + s207 :: SWord8 = if s206 then s194 else s193 + s208 :: SWord8 = s33 + s207 + s209 :: SWord8 = if s201 then s208 else s207 + s210 :: SWord8 = s33 + s209 + s211 :: SWord8 = if s198 then s210 else s209 + s212 :: SWord8 = if s196 then s204 else s211 + s213 :: SWord8 = if s14 then s195 else s212 + s214 :: SWord8 = s33 + s213 + s215 :: SWord8 = if s13 then s214 else s213 + s216 :: SBool = s9 < s35 + s217 :: SWord8 = s9 rem s10 + s218 :: SBool = s12 == s217 + s219 :: SWord8 = s9 quot s10 + s220 :: SWord8 = s219 rem s10 + s221 :: SBool = s12 == s220 + s222 :: SWord8 = if s221 then s214 else s213 + s223 :: SWord8 = s33 + s222 + s224 :: SWord8 = if s218 then s223 else s222 + s225 :: SWord8 = s219 quot s10 + s226 :: SBool = s12 == s225 + s227 :: SWord8 = if s226 then s214 else s213 + s228 :: SWord8 = s33 + s227 + s229 :: SWord8 = if s221 then s228 else s227 + s230 :: SWord8 = s33 + s229 + s231 :: SWord8 = if s218 then s230 else s229 + s232 :: SWord8 = if s216 then s224 else s231 + s233 :: SWord8 = if s11 then s215 else s232 + s234 :: SBool = s0 == s233 + s235 :: SBool = s9 == s33 + s236 :: SBool = s8 == s33 + s237 :: SBool = s7 == s33 + s238 :: SBool = s6 == s33 + s239 :: SBool = s5 == s33 + s240 :: SBool = s4 == s33 + s241 :: SBool = s3 == s33 + s242 :: SBool = s2 == s33 + s243 :: SBool = s1 == s33 + s244 :: SBool = s0 == s33 + s245 :: SWord8 = if s244 then s32 else s33 + s246 :: SBool = s33 == s37 + s247 :: SBool = s33 == s40 + s248 :: SWord8 = if s247 then s32 else s33 + s249 :: SWord8 = s33 + s248 + s250 :: SWord8 = if s246 then s249 else s248 + s251 :: SBool = s33 == s45 + s252 :: SWord8 = if s251 then s32 else s33 + s253 :: SWord8 = s33 + s252 + s254 :: SWord8 = if s247 then s253 else s252 + s255 :: SWord8 = s33 + s254 + s256 :: SWord8 = if s246 then s255 else s254 + s257 :: SWord8 = if s36 then s250 else s256 + s258 :: SWord8 = if s30 then s245 else s257 + s259 :: SWord8 = s33 + s258 + s260 :: SWord8 = if s243 then s259 else s258 + s261 :: SBool = s33 == s57 + s262 :: SBool = s33 == s60 + s263 :: SWord8 = if s262 then s259 else s258 + s264 :: SWord8 = s33 + s263 + s265 :: SWord8 = if s261 then s264 else s263 + s266 :: SBool = s33 == s65 + s267 :: SWord8 = if s266 then s259 else s258 + s268 :: SWord8 = s33 + s267 + s269 :: SWord8 = if s262 then s268 else s267 + s270 :: SWord8 = s33 + s269 + s271 :: SWord8 = if s261 then s270 else s269 + s272 :: SWord8 = if s56 then s265 else s271 + s273 :: SWord8 = if s28 then s260 else s272 + s274 :: SWord8 = s33 + s273 + s275 :: SWord8 = if s242 then s274 else s273 + s276 :: SBool = s33 == s77 + s277 :: SBool = s33 == s80 + s278 :: SWord8 = if s277 then s274 else s273 + s279 :: SWord8 = s33 + s278 + s280 :: SWord8 = if s276 then s279 else s278 + s281 :: SBool = s33 == s85 + s282 :: SWord8 = if s281 then s274 else s273 + s283 :: SWord8 = s33 + s282 + s284 :: SWord8 = if s277 then s283 else s282 + s285 :: SWord8 = s33 + s284 + s286 :: SWord8 = if s276 then s285 else s284 + s287 :: SWord8 = if s76 then s280 else s286 + s288 :: SWord8 = if s26 then s275 else s287 + s289 :: SWord8 = s33 + s288 + s290 :: SWord8 = if s241 then s289 else s288 + s291 :: SBool = s33 == s97 + s292 :: SBool = s33 == s100 + s293 :: SWord8 = if s292 then s289 else s288 + s294 :: SWord8 = s33 + s293 + s295 :: SWord8 = if s291 then s294 else s293 + s296 :: SBool = s33 == s105 + s297 :: SWord8 = if s296 then s289 else s288 + s298 :: SWord8 = s33 + s297 + s299 :: SWord8 = if s292 then s298 else s297 + s300 :: SWord8 = s33 + s299 + s301 :: SWord8 = if s291 then s300 else s299 + s302 :: SWord8 = if s96 then s295 else s301 + s303 :: SWord8 = if s24 then s290 else s302 + s304 :: SWord8 = s33 + s303 + s305 :: SWord8 = if s240 then s304 else s303 + s306 :: SBool = s33 == s117 + s307 :: SBool = s33 == s120 + s308 :: SWord8 = if s307 then s304 else s303 + s309 :: SWord8 = s33 + s308 + s310 :: SWord8 = if s306 then s309 else s308 + s311 :: SBool = s33 == s125 + s312 :: SWord8 = if s311 then s304 else s303 + s313 :: SWord8 = s33 + s312 + s314 :: SWord8 = if s307 then s313 else s312 + s315 :: SWord8 = s33 + s314 + s316 :: SWord8 = if s306 then s315 else s314 + s317 :: SWord8 = if s116 then s310 else s316 + s318 :: SWord8 = if s22 then s305 else s317 + s319 :: SWord8 = s33 + s318 + s320 :: SWord8 = if s239 then s319 else s318 + s321 :: SBool = s33 == s137 + s322 :: SBool = s33 == s140 + s323 :: SWord8 = if s322 then s319 else s318 + s324 :: SWord8 = s33 + s323 + s325 :: SWord8 = if s321 then s324 else s323 + s326 :: SBool = s33 == s145 + s327 :: SWord8 = if s326 then s319 else s318 + s328 :: SWord8 = s33 + s327 + s329 :: SWord8 = if s322 then s328 else s327 + s330 :: SWord8 = s33 + s329 + s331 :: SWord8 = if s321 then s330 else s329 + s332 :: SWord8 = if s136 then s325 else s331 + s333 :: SWord8 = if s20 then s320 else s332 + s334 :: SWord8 = s33 + s333 + s335 :: SWord8 = if s238 then s334 else s333 + s336 :: SBool = s33 == s157 + s337 :: SBool = s33 == s160 + s338 :: SWord8 = if s337 then s334 else s333 + s339 :: SWord8 = s33 + s338 + s340 :: SWord8 = if s336 then s339 else s338 + s341 :: SBool = s33 == s165 + s342 :: SWord8 = if s341 then s334 else s333 + s343 :: SWord8 = s33 + s342 + s344 :: SWord8 = if s337 then s343 else s342 + s345 :: SWord8 = s33 + s344 + s346 :: SWord8 = if s336 then s345 else s344 + s347 :: SWord8 = if s156 then s340 else s346 + s348 :: SWord8 = if s18 then s335 else s347 + s349 :: SWord8 = s33 + s348 + s350 :: SWord8 = if s237 then s349 else s348 + s351 :: SBool = s33 == s177 + s352 :: SBool = s33 == s180 + s353 :: SWord8 = if s352 then s349 else s348 + s354 :: SWord8 = s33 + s353 + s355 :: SWord8 = if s351 then s354 else s353 + s356 :: SBool = s33 == s185 + s357 :: SWord8 = if s356 then s349 else s348 + s358 :: SWord8 = s33 + s357 + s359 :: SWord8 = if s352 then s358 else s357 + s360 :: SWord8 = s33 + s359 + s361 :: SWord8 = if s351 then s360 else s359 + s362 :: SWord8 = if s176 then s355 else s361 + s363 :: SWord8 = if s16 then s350 else s362 + s364 :: SWord8 = s33 + s363 + s365 :: SWord8 = if s236 then s364 else s363 + s366 :: SBool = s33 == s197 + s367 :: SBool = s33 == s200 + s368 :: SWord8 = if s367 then s364 else s363 + s369 :: SWord8 = s33 + s368 + s370 :: SWord8 = if s366 then s369 else s368 + s371 :: SBool = s33 == s205 + s372 :: SWord8 = if s371 then s364 else s363 + s373 :: SWord8 = s33 + s372 + s374 :: SWord8 = if s367 then s373 else s372 + s375 :: SWord8 = s33 + s374 + s376 :: SWord8 = if s366 then s375 else s374 + s377 :: SWord8 = if s196 then s370 else s376 + s378 :: SWord8 = if s14 then s365 else s377 + s379 :: SWord8 = s33 + s378 + s380 :: SWord8 = if s235 then s379 else s378 + s381 :: SBool = s33 == s217 + s382 :: SBool = s33 == s220 + s383 :: SWord8 = if s382 then s379 else s378 + s384 :: SWord8 = s33 + s383 + s385 :: SWord8 = if s381 then s384 else s383 + s386 :: SBool = s33 == s225 + s387 :: SWord8 = if s386 then s379 else s378 + s388 :: SWord8 = s33 + s387 + s389 :: SWord8 = if s382 then s388 else s387 + s390 :: SWord8 = s33 + s389 + s391 :: SWord8 = if s381 then s390 else s389 + s392 :: SWord8 = if s216 then s385 else s391 + s393 :: SWord8 = if s11 then s380 else s392 + s394 :: SBool = s1 == s393 + s395 :: SBool = s9 == s32 + s396 :: SBool = s8 == s32 + s397 :: SBool = s7 == s32 + s398 :: SBool = s6 == s32 + s399 :: SBool = s5 == s32 + s400 :: SBool = s4 == s32 + s401 :: SBool = s3 == s32 + s402 :: SBool = s2 == s32 + s403 :: SBool = s1 == s32 + s404 :: SBool = s0 == s32 + s405 :: SWord8 = if s404 then s32 else s33 + s406 :: SBool = s32 == s37 + s407 :: SBool = s32 == s40 + s408 :: SWord8 = if s407 then s32 else s33 + s409 :: SWord8 = s33 + s408 + s410 :: SWord8 = if s406 then s409 else s408 + s411 :: SBool = s32 == s45 + s412 :: SWord8 = if s411 then s32 else s33 + s413 :: SWord8 = s33 + s412 + s414 :: SWord8 = if s407 then s413 else s412 + s415 :: SWord8 = s33 + s414 + s416 :: SWord8 = if s406 then s415 else s414 + s417 :: SWord8 = if s36 then s410 else s416 + s418 :: SWord8 = if s30 then s405 else s417 + s419 :: SWord8 = s33 + s418 + s420 :: SWord8 = if s403 then s419 else s418 + s421 :: SBool = s32 == s57 + s422 :: SBool = s32 == s60 + s423 :: SWord8 = if s422 then s419 else s418 + s424 :: SWord8 = s33 + s423 + s425 :: SWord8 = if s421 then s424 else s423 + s426 :: SBool = s32 == s65 + s427 :: SWord8 = if s426 then s419 else s418 + s428 :: SWord8 = s33 + s427 + s429 :: SWord8 = if s422 then s428 else s427 + s430 :: SWord8 = s33 + s429 + s431 :: SWord8 = if s421 then s430 else s429 + s432 :: SWord8 = if s56 then s425 else s431 + s433 :: SWord8 = if s28 then s420 else s432 + s434 :: SWord8 = s33 + s433 + s435 :: SWord8 = if s402 then s434 else s433 + s436 :: SBool = s32 == s77 + s437 :: SBool = s32 == s80 + s438 :: SWord8 = if s437 then s434 else s433 + s439 :: SWord8 = s33 + s438 + s440 :: SWord8 = if s436 then s439 else s438 + s441 :: SBool = s32 == s85 + s442 :: SWord8 = if s441 then s434 else s433 + s443 :: SWord8 = s33 + s442 + s444 :: SWord8 = if s437 then s443 else s442 + s445 :: SWord8 = s33 + s444 + s446 :: SWord8 = if s436 then s445 else s444 + s447 :: SWord8 = if s76 then s440 else s446 + s448 :: SWord8 = if s26 then s435 else s447 + s449 :: SWord8 = s33 + s448 + s450 :: SWord8 = if s401 then s449 else s448 + s451 :: SBool = s32 == s97 + s452 :: SBool = s32 == s100 + s453 :: SWord8 = if s452 then s449 else s448 + s454 :: SWord8 = s33 + s453 + s455 :: SWord8 = if s451 then s454 else s453 + s456 :: SBool = s32 == s105 + s457 :: SWord8 = if s456 then s449 else s448 + s458 :: SWord8 = s33 + s457 + s459 :: SWord8 = if s452 then s458 else s457 + s460 :: SWord8 = s33 + s459 + s461 :: SWord8 = if s451 then s460 else s459 + s462 :: SWord8 = if s96 then s455 else s461 + s463 :: SWord8 = if s24 then s450 else s462 + s464 :: SWord8 = s33 + s463 + s465 :: SWord8 = if s400 then s464 else s463 + s466 :: SBool = s32 == s117 + s467 :: SBool = s32 == s120 + s468 :: SWord8 = if s467 then s464 else s463 + s469 :: SWord8 = s33 + s468 + s470 :: SWord8 = if s466 then s469 else s468 + s471 :: SBool = s32 == s125 + s472 :: SWord8 = if s471 then s464 else s463 + s473 :: SWord8 = s33 + s472 + s474 :: SWord8 = if s467 then s473 else s472 + s475 :: SWord8 = s33 + s474 + s476 :: SWord8 = if s466 then s475 else s474 + s477 :: SWord8 = if s116 then s470 else s476 + s478 :: SWord8 = if s22 then s465 else s477 + s479 :: SWord8 = s33 + s478 + s480 :: SWord8 = if s399 then s479 else s478 + s481 :: SBool = s32 == s137 + s482 :: SBool = s32 == s140 + s483 :: SWord8 = if s482 then s479 else s478 + s484 :: SWord8 = s33 + s483 + s485 :: SWord8 = if s481 then s484 else s483 + s486 :: SBool = s32 == s145 + s487 :: SWord8 = if s486 then s479 else s478 + s488 :: SWord8 = s33 + s487 + s489 :: SWord8 = if s482 then s488 else s487 + s490 :: SWord8 = s33 + s489 + s491 :: SWord8 = if s481 then s490 else s489 + s492 :: SWord8 = if s136 then s485 else s491 + s493 :: SWord8 = if s20 then s480 else s492 + s494 :: SWord8 = s33 + s493 + s495 :: SWord8 = if s398 then s494 else s493 + s496 :: SBool = s32 == s157 + s497 :: SBool = s32 == s160 + s498 :: SWord8 = if s497 then s494 else s493 + s499 :: SWord8 = s33 + s498 + s500 :: SWord8 = if s496 then s499 else s498 + s501 :: SBool = s32 == s165 + s502 :: SWord8 = if s501 then s494 else s493 + s503 :: SWord8 = s33 + s502 + s504 :: SWord8 = if s497 then s503 else s502 + s505 :: SWord8 = s33 + s504 + s506 :: SWord8 = if s496 then s505 else s504 + s507 :: SWord8 = if s156 then s500 else s506 + s508 :: SWord8 = if s18 then s495 else s507 + s509 :: SWord8 = s33 + s508 + s510 :: SWord8 = if s397 then s509 else s508 + s511 :: SBool = s32 == s177 + s512 :: SBool = s32 == s180 + s513 :: SWord8 = if s512 then s509 else s508 + s514 :: SWord8 = s33 + s513 + s515 :: SWord8 = if s511 then s514 else s513 + s516 :: SBool = s32 == s185 + s517 :: SWord8 = if s516 then s509 else s508 + s518 :: SWord8 = s33 + s517 + s519 :: SWord8 = if s512 then s518 else s517 + s520 :: SWord8 = s33 + s519 + s521 :: SWord8 = if s511 then s520 else s519 + s522 :: SWord8 = if s176 then s515 else s521 + s523 :: SWord8 = if s16 then s510 else s522 + s524 :: SWord8 = s33 + s523 + s525 :: SWord8 = if s396 then s524 else s523 + s526 :: SBool = s32 == s197 + s527 :: SBool = s32 == s200 + s528 :: SWord8 = if s527 then s524 else s523 + s529 :: SWord8 = s33 + s528 + s530 :: SWord8 = if s526 then s529 else s528 + s531 :: SBool = s32 == s205 + s532 :: SWord8 = if s531 then s524 else s523 + s533 :: SWord8 = s33 + s532 + s534 :: SWord8 = if s527 then s533 else s532 + s535 :: SWord8 = s33 + s534 + s536 :: SWord8 = if s526 then s535 else s534 + s537 :: SWord8 = if s196 then s530 else s536 + s538 :: SWord8 = if s14 then s525 else s537 + s539 :: SWord8 = s33 + s538 + s540 :: SWord8 = if s395 then s539 else s538 + s541 :: SBool = s32 == s217 + s542 :: SBool = s32 == s220 + s543 :: SWord8 = if s542 then s539 else s538 + s544 :: SWord8 = s33 + s543 + s545 :: SWord8 = if s541 then s544 else s543 + s546 :: SBool = s32 == s225 + s547 :: SWord8 = if s546 then s539 else s538 + s548 :: SWord8 = s33 + s547 + s549 :: SWord8 = if s542 then s548 else s547 + s550 :: SWord8 = s33 + s549 + s551 :: SWord8 = if s541 then s550 else s549 + s552 :: SWord8 = if s216 then s545 else s551 + s553 :: SWord8 = if s11 then s540 else s552 + s554 :: SBool = s2 == s553 + s556 :: SBool = s9 == s555 + s557 :: SBool = s8 == s555 + s558 :: SBool = s7 == s555 + s559 :: SBool = s6 == s555 + s560 :: SBool = s5 == s555 + s561 :: SBool = s4 == s555 + s562 :: SBool = s3 == s555 + s563 :: SBool = s2 == s555 + s564 :: SBool = s1 == s555 + s565 :: SBool = s0 == s555 + s566 :: SWord8 = if s565 then s32 else s33 + s567 :: SBool = s37 == s555 + s568 :: SBool = s40 == s555 + s569 :: SWord8 = if s568 then s32 else s33 + s570 :: SWord8 = s33 + s569 + s571 :: SWord8 = if s567 then s570 else s569 + s572 :: SBool = s45 == s555 + s573 :: SWord8 = if s572 then s32 else s33 + s574 :: SWord8 = s33 + s573 + s575 :: SWord8 = if s568 then s574 else s573 + s576 :: SWord8 = s33 + s575 + s577 :: SWord8 = if s567 then s576 else s575 + s578 :: SWord8 = if s36 then s571 else s577 + s579 :: SWord8 = if s30 then s566 else s578 + s580 :: SWord8 = s33 + s579 + s581 :: SWord8 = if s564 then s580 else s579 + s582 :: SBool = s57 == s555 + s583 :: SBool = s60 == s555 + s584 :: SWord8 = if s583 then s580 else s579 + s585 :: SWord8 = s33 + s584 + s586 :: SWord8 = if s582 then s585 else s584 + s587 :: SBool = s65 == s555 + s588 :: SWord8 = if s587 then s580 else s579 + s589 :: SWord8 = s33 + s588 + s590 :: SWord8 = if s583 then s589 else s588 + s591 :: SWord8 = s33 + s590 + s592 :: SWord8 = if s582 then s591 else s590 + s593 :: SWord8 = if s56 then s586 else s592 + s594 :: SWord8 = if s28 then s581 else s593 + s595 :: SWord8 = s33 + s594 + s596 :: SWord8 = if s563 then s595 else s594 + s597 :: SBool = s77 == s555 + s598 :: SBool = s80 == s555 + s599 :: SWord8 = if s598 then s595 else s594 + s600 :: SWord8 = s33 + s599 + s601 :: SWord8 = if s597 then s600 else s599 + s602 :: SBool = s85 == s555 + s603 :: SWord8 = if s602 then s595 else s594 + s604 :: SWord8 = s33 + s603 + s605 :: SWord8 = if s598 then s604 else s603 + s606 :: SWord8 = s33 + s605 + s607 :: SWord8 = if s597 then s606 else s605 + s608 :: SWord8 = if s76 then s601 else s607 + s609 :: SWord8 = if s26 then s596 else s608 + s610 :: SWord8 = s33 + s609 + s611 :: SWord8 = if s562 then s610 else s609 + s612 :: SBool = s97 == s555 + s613 :: SBool = s100 == s555 + s614 :: SWord8 = if s613 then s610 else s609 + s615 :: SWord8 = s33 + s614 + s616 :: SWord8 = if s612 then s615 else s614 + s617 :: SBool = s105 == s555 + s618 :: SWord8 = if s617 then s610 else s609 + s619 :: SWord8 = s33 + s618 + s620 :: SWord8 = if s613 then s619 else s618 + s621 :: SWord8 = s33 + s620 + s622 :: SWord8 = if s612 then s621 else s620 + s623 :: SWord8 = if s96 then s616 else s622 + s624 :: SWord8 = if s24 then s611 else s623 + s625 :: SWord8 = s33 + s624 + s626 :: SWord8 = if s561 then s625 else s624 + s627 :: SBool = s117 == s555 + s628 :: SBool = s120 == s555 + s629 :: SWord8 = if s628 then s625 else s624 + s630 :: SWord8 = s33 + s629 + s631 :: SWord8 = if s627 then s630 else s629 + s632 :: SBool = s125 == s555 + s633 :: SWord8 = if s632 then s625 else s624 + s634 :: SWord8 = s33 + s633 + s635 :: SWord8 = if s628 then s634 else s633 + s636 :: SWord8 = s33 + s635 + s637 :: SWord8 = if s627 then s636 else s635 + s638 :: SWord8 = if s116 then s631 else s637 + s639 :: SWord8 = if s22 then s626 else s638 + s640 :: SWord8 = s33 + s639 + s641 :: SWord8 = if s560 then s640 else s639 + s642 :: SBool = s137 == s555 + s643 :: SBool = s140 == s555 + s644 :: SWord8 = if s643 then s640 else s639 + s645 :: SWord8 = s33 + s644 + s646 :: SWord8 = if s642 then s645 else s644 + s647 :: SBool = s145 == s555 + s648 :: SWord8 = if s647 then s640 else s639 + s649 :: SWord8 = s33 + s648 + s650 :: SWord8 = if s643 then s649 else s648 + s651 :: SWord8 = s33 + s650 + s652 :: SWord8 = if s642 then s651 else s650 + s653 :: SWord8 = if s136 then s646 else s652 + s654 :: SWord8 = if s20 then s641 else s653 + s655 :: SWord8 = s33 + s654 + s656 :: SWord8 = if s559 then s655 else s654 + s657 :: SBool = s157 == s555 + s658 :: SBool = s160 == s555 + s659 :: SWord8 = if s658 then s655 else s654 + s660 :: SWord8 = s33 + s659 + s661 :: SWord8 = if s657 then s660 else s659 + s662 :: SBool = s165 == s555 + s663 :: SWord8 = if s662 then s655 else s654 + s664 :: SWord8 = s33 + s663 + s665 :: SWord8 = if s658 then s664 else s663 + s666 :: SWord8 = s33 + s665 + s667 :: SWord8 = if s657 then s666 else s665 + s668 :: SWord8 = if s156 then s661 else s667 + s669 :: SWord8 = if s18 then s656 else s668 + s670 :: SWord8 = s33 + s669 + s671 :: SWord8 = if s558 then s670 else s669 + s672 :: SBool = s177 == s555 + s673 :: SBool = s180 == s555 + s674 :: SWord8 = if s673 then s670 else s669 + s675 :: SWord8 = s33 + s674 + s676 :: SWord8 = if s672 then s675 else s674 + s677 :: SBool = s185 == s555 + s678 :: SWord8 = if s677 then s670 else s669 + s679 :: SWord8 = s33 + s678 + s680 :: SWord8 = if s673 then s679 else s678 + s681 :: SWord8 = s33 + s680 + s682 :: SWord8 = if s672 then s681 else s680 + s683 :: SWord8 = if s176 then s676 else s682 + s684 :: SWord8 = if s16 then s671 else s683 + s685 :: SWord8 = s33 + s684 + s686 :: SWord8 = if s557 then s685 else s684 + s687 :: SBool = s197 == s555 + s688 :: SBool = s200 == s555 + s689 :: SWord8 = if s688 then s685 else s684 + s690 :: SWord8 = s33 + s689 + s691 :: SWord8 = if s687 then s690 else s689 + s692 :: SBool = s205 == s555 + s693 :: SWord8 = if s692 then s685 else s684 + s694 :: SWord8 = s33 + s693 + s695 :: SWord8 = if s688 then s694 else s693 + s696 :: SWord8 = s33 + s695 + s697 :: SWord8 = if s687 then s696 else s695 + s698 :: SWord8 = if s196 then s691 else s697 + s699 :: SWord8 = if s14 then s686 else s698 + s700 :: SWord8 = s33 + s699 + s701 :: SWord8 = if s556 then s700 else s699 + s702 :: SBool = s217 == s555 + s703 :: SBool = s220 == s555 + s704 :: SWord8 = if s703 then s700 else s699 + s705 :: SWord8 = s33 + s704 + s706 :: SWord8 = if s702 then s705 else s704 + s707 :: SBool = s225 == s555 + s708 :: SWord8 = if s707 then s700 else s699 + s709 :: SWord8 = s33 + s708 + s710 :: SWord8 = if s703 then s709 else s708 + s711 :: SWord8 = s33 + s710 + s712 :: SWord8 = if s702 then s711 else s710 + s713 :: SWord8 = if s216 then s706 else s712 + s714 :: SWord8 = if s11 then s701 else s713 + s715 :: SBool = s3 == s714 + s717 :: SBool = s9 == s716 + s718 :: SBool = s8 == s716 + s719 :: SBool = s7 == s716 + s720 :: SBool = s6 == s716 + s721 :: SBool = s5 == s716 + s722 :: SBool = s4 == s716 + s723 :: SBool = s3 == s716 + s724 :: SBool = s2 == s716 + s725 :: SBool = s1 == s716 + s726 :: SBool = s0 == s716 + s727 :: SWord8 = if s726 then s32 else s33 + s728 :: SBool = s37 == s716 + s729 :: SBool = s40 == s716 + s730 :: SWord8 = if s729 then s32 else s33 + s731 :: SWord8 = s33 + s730 + s732 :: SWord8 = if s728 then s731 else s730 + s733 :: SBool = s45 == s716 + s734 :: SWord8 = if s733 then s32 else s33 + s735 :: SWord8 = s33 + s734 + s736 :: SWord8 = if s729 then s735 else s734 + s737 :: SWord8 = s33 + s736 + s738 :: SWord8 = if s728 then s737 else s736 + s739 :: SWord8 = if s36 then s732 else s738 + s740 :: SWord8 = if s30 then s727 else s739 + s741 :: SWord8 = s33 + s740 + s742 :: SWord8 = if s725 then s741 else s740 + s743 :: SBool = s57 == s716 + s744 :: SBool = s60 == s716 + s745 :: SWord8 = if s744 then s741 else s740 + s746 :: SWord8 = s33 + s745 + s747 :: SWord8 = if s743 then s746 else s745 + s748 :: SBool = s65 == s716 + s749 :: SWord8 = if s748 then s741 else s740 + s750 :: SWord8 = s33 + s749 + s751 :: SWord8 = if s744 then s750 else s749 + s752 :: SWord8 = s33 + s751 + s753 :: SWord8 = if s743 then s752 else s751 + s754 :: SWord8 = if s56 then s747 else s753 + s755 :: SWord8 = if s28 then s742 else s754 + s756 :: SWord8 = s33 + s755 + s757 :: SWord8 = if s724 then s756 else s755 + s758 :: SBool = s77 == s716 + s759 :: SBool = s80 == s716 + s760 :: SWord8 = if s759 then s756 else s755 + s761 :: SWord8 = s33 + s760 + s762 :: SWord8 = if s758 then s761 else s760 + s763 :: SBool = s85 == s716 + s764 :: SWord8 = if s763 then s756 else s755 + s765 :: SWord8 = s33 + s764 + s766 :: SWord8 = if s759 then s765 else s764 + s767 :: SWord8 = s33 + s766 + s768 :: SWord8 = if s758 then s767 else s766 + s769 :: SWord8 = if s76 then s762 else s768 + s770 :: SWord8 = if s26 then s757 else s769 + s771 :: SWord8 = s33 + s770 + s772 :: SWord8 = if s723 then s771 else s770 + s773 :: SBool = s97 == s716 + s774 :: SBool = s100 == s716 + s775 :: SWord8 = if s774 then s771 else s770 + s776 :: SWord8 = s33 + s775 + s777 :: SWord8 = if s773 then s776 else s775 + s778 :: SBool = s105 == s716 + s779 :: SWord8 = if s778 then s771 else s770 + s780 :: SWord8 = s33 + s779 + s781 :: SWord8 = if s774 then s780 else s779 + s782 :: SWord8 = s33 + s781 + s783 :: SWord8 = if s773 then s782 else s781 + s784 :: SWord8 = if s96 then s777 else s783 + s785 :: SWord8 = if s24 then s772 else s784 + s786 :: SWord8 = s33 + s785 + s787 :: SWord8 = if s722 then s786 else s785 + s788 :: SBool = s117 == s716 + s789 :: SBool = s120 == s716 + s790 :: SWord8 = if s789 then s786 else s785 + s791 :: SWord8 = s33 + s790 + s792 :: SWord8 = if s788 then s791 else s790 + s793 :: SBool = s125 == s716 + s794 :: SWord8 = if s793 then s786 else s785 + s795 :: SWord8 = s33 + s794 + s796 :: SWord8 = if s789 then s795 else s794 + s797 :: SWord8 = s33 + s796 + s798 :: SWord8 = if s788 then s797 else s796 + s799 :: SWord8 = if s116 then s792 else s798 + s800 :: SWord8 = if s22 then s787 else s799 + s801 :: SWord8 = s33 + s800 + s802 :: SWord8 = if s721 then s801 else s800 + s803 :: SBool = s137 == s716 + s804 :: SBool = s140 == s716 + s805 :: SWord8 = if s804 then s801 else s800 + s806 :: SWord8 = s33 + s805 + s807 :: SWord8 = if s803 then s806 else s805 + s808 :: SBool = s145 == s716 + s809 :: SWord8 = if s808 then s801 else s800 + s810 :: SWord8 = s33 + s809 + s811 :: SWord8 = if s804 then s810 else s809 + s812 :: SWord8 = s33 + s811 + s813 :: SWord8 = if s803 then s812 else s811 + s814 :: SWord8 = if s136 then s807 else s813 + s815 :: SWord8 = if s20 then s802 else s814 + s816 :: SWord8 = s33 + s815 + s817 :: SWord8 = if s720 then s816 else s815 + s818 :: SBool = s157 == s716 + s819 :: SBool = s160 == s716 + s820 :: SWord8 = if s819 then s816 else s815 + s821 :: SWord8 = s33 + s820 + s822 :: SWord8 = if s818 then s821 else s820 + s823 :: SBool = s165 == s716 + s824 :: SWord8 = if s823 then s816 else s815 + s825 :: SWord8 = s33 + s824 + s826 :: SWord8 = if s819 then s825 else s824 + s827 :: SWord8 = s33 + s826 + s828 :: SWord8 = if s818 then s827 else s826 + s829 :: SWord8 = if s156 then s822 else s828 + s830 :: SWord8 = if s18 then s817 else s829 + s831 :: SWord8 = s33 + s830 + s832 :: SWord8 = if s719 then s831 else s830 + s833 :: SBool = s177 == s716 + s834 :: SBool = s180 == s716 + s835 :: SWord8 = if s834 then s831 else s830 + s836 :: SWord8 = s33 + s835 + s837 :: SWord8 = if s833 then s836 else s835 + s838 :: SBool = s185 == s716 + s839 :: SWord8 = if s838 then s831 else s830 + s840 :: SWord8 = s33 + s839 + s841 :: SWord8 = if s834 then s840 else s839 + s842 :: SWord8 = s33 + s841 + s843 :: SWord8 = if s833 then s842 else s841 + s844 :: SWord8 = if s176 then s837 else s843 + s845 :: SWord8 = if s16 then s832 else s844 + s846 :: SWord8 = s33 + s845 + s847 :: SWord8 = if s718 then s846 else s845 + s848 :: SBool = s197 == s716 + s849 :: SBool = s200 == s716 + s850 :: SWord8 = if s849 then s846 else s845 + s851 :: SWord8 = s33 + s850 + s852 :: SWord8 = if s848 then s851 else s850 + s853 :: SBool = s205 == s716 + s854 :: SWord8 = if s853 then s846 else s845 + s855 :: SWord8 = s33 + s854 + s856 :: SWord8 = if s849 then s855 else s854 + s857 :: SWord8 = s33 + s856 + s858 :: SWord8 = if s848 then s857 else s856 + s859 :: SWord8 = if s196 then s852 else s858 + s860 :: SWord8 = if s14 then s847 else s859 + s861 :: SWord8 = s33 + s860 + s862 :: SWord8 = if s717 then s861 else s860 + s863 :: SBool = s217 == s716 + s864 :: SBool = s220 == s716 + s865 :: SWord8 = if s864 then s861 else s860 + s866 :: SWord8 = s33 + s865 + s867 :: SWord8 = if s863 then s866 else s865 + s868 :: SBool = s225 == s716 + s869 :: SWord8 = if s868 then s861 else s860 + s870 :: SWord8 = s33 + s869 + s871 :: SWord8 = if s864 then s870 else s869 + s872 :: SWord8 = s33 + s871 + s873 :: SWord8 = if s863 then s872 else s871 + s874 :: SWord8 = if s216 then s867 else s873 + s875 :: SWord8 = if s11 then s862 else s874 + s876 :: SBool = s4 == s875 + s878 :: SBool = s9 == s877 + s879 :: SBool = s8 == s877 + s880 :: SBool = s7 == s877 + s881 :: SBool = s6 == s877 + s882 :: SBool = s5 == s877 + s883 :: SBool = s4 == s877 + s884 :: SBool = s3 == s877 + s885 :: SBool = s2 == s877 + s886 :: SBool = s1 == s877 + s887 :: SBool = s0 == s877 + s888 :: SWord8 = if s887 then s32 else s33 + s889 :: SBool = s37 == s877 + s890 :: SBool = s40 == s877 + s891 :: SWord8 = if s890 then s32 else s33 + s892 :: SWord8 = s33 + s891 + s893 :: SWord8 = if s889 then s892 else s891 + s894 :: SBool = s45 == s877 + s895 :: SWord8 = if s894 then s32 else s33 + s896 :: SWord8 = s33 + s895 + s897 :: SWord8 = if s890 then s896 else s895 + s898 :: SWord8 = s33 + s897 + s899 :: SWord8 = if s889 then s898 else s897 + s900 :: SWord8 = if s36 then s893 else s899 + s901 :: SWord8 = if s30 then s888 else s900 + s902 :: SWord8 = s33 + s901 + s903 :: SWord8 = if s886 then s902 else s901 + s904 :: SBool = s57 == s877 + s905 :: SBool = s60 == s877 + s906 :: SWord8 = if s905 then s902 else s901 + s907 :: SWord8 = s33 + s906 + s908 :: SWord8 = if s904 then s907 else s906 + s909 :: SBool = s65 == s877 + s910 :: SWord8 = if s909 then s902 else s901 + s911 :: SWord8 = s33 + s910 + s912 :: SWord8 = if s905 then s911 else s910 + s913 :: SWord8 = s33 + s912 + s914 :: SWord8 = if s904 then s913 else s912 + s915 :: SWord8 = if s56 then s908 else s914 + s916 :: SWord8 = if s28 then s903 else s915 + s917 :: SWord8 = s33 + s916 + s918 :: SWord8 = if s885 then s917 else s916 + s919 :: SBool = s77 == s877 + s920 :: SBool = s80 == s877 + s921 :: SWord8 = if s920 then s917 else s916 + s922 :: SWord8 = s33 + s921 + s923 :: SWord8 = if s919 then s922 else s921 + s924 :: SBool = s85 == s877 + s925 :: SWord8 = if s924 then s917 else s916 + s926 :: SWord8 = s33 + s925 + s927 :: SWord8 = if s920 then s926 else s925 + s928 :: SWord8 = s33 + s927 + s929 :: SWord8 = if s919 then s928 else s927 + s930 :: SWord8 = if s76 then s923 else s929 + s931 :: SWord8 = if s26 then s918 else s930 + s932 :: SWord8 = s33 + s931 + s933 :: SWord8 = if s884 then s932 else s931 + s934 :: SBool = s97 == s877 + s935 :: SBool = s100 == s877 + s936 :: SWord8 = if s935 then s932 else s931 + s937 :: SWord8 = s33 + s936 + s938 :: SWord8 = if s934 then s937 else s936 + s939 :: SBool = s105 == s877 + s940 :: SWord8 = if s939 then s932 else s931 + s941 :: SWord8 = s33 + s940 + s942 :: SWord8 = if s935 then s941 else s940 + s943 :: SWord8 = s33 + s942 + s944 :: SWord8 = if s934 then s943 else s942 + s945 :: SWord8 = if s96 then s938 else s944 + s946 :: SWord8 = if s24 then s933 else s945 + s947 :: SWord8 = s33 + s946 + s948 :: SWord8 = if s883 then s947 else s946 + s949 :: SBool = s117 == s877 + s950 :: SBool = s120 == s877 + s951 :: SWord8 = if s950 then s947 else s946 + s952 :: SWord8 = s33 + s951 + s953 :: SWord8 = if s949 then s952 else s951 + s954 :: SBool = s125 == s877 + s955 :: SWord8 = if s954 then s947 else s946 + s956 :: SWord8 = s33 + s955 + s957 :: SWord8 = if s950 then s956 else s955 + s958 :: SWord8 = s33 + s957 + s959 :: SWord8 = if s949 then s958 else s957 + s960 :: SWord8 = if s116 then s953 else s959 + s961 :: SWord8 = if s22 then s948 else s960 + s962 :: SWord8 = s33 + s961 + s963 :: SWord8 = if s882 then s962 else s961 + s964 :: SBool = s137 == s877 + s965 :: SBool = s140 == s877 + s966 :: SWord8 = if s965 then s962 else s961 + s967 :: SWord8 = s33 + s966 + s968 :: SWord8 = if s964 then s967 else s966 + s969 :: SBool = s145 == s877 + s970 :: SWord8 = if s969 then s962 else s961 + s971 :: SWord8 = s33 + s970 + s972 :: SWord8 = if s965 then s971 else s970 + s973 :: SWord8 = s33 + s972 + s974 :: SWord8 = if s964 then s973 else s972 + s975 :: SWord8 = if s136 then s968 else s974 + s976 :: SWord8 = if s20 then s963 else s975 + s977 :: SWord8 = s33 + s976 + s978 :: SWord8 = if s881 then s977 else s976 + s979 :: SBool = s157 == s877 + s980 :: SBool = s160 == s877 + s981 :: SWord8 = if s980 then s977 else s976 + s982 :: SWord8 = s33 + s981 + s983 :: SWord8 = if s979 then s982 else s981 + s984 :: SBool = s165 == s877 + s985 :: SWord8 = if s984 then s977 else s976 + s986 :: SWord8 = s33 + s985 + s987 :: SWord8 = if s980 then s986 else s985 + s988 :: SWord8 = s33 + s987 + s989 :: SWord8 = if s979 then s988 else s987 + s990 :: SWord8 = if s156 then s983 else s989 + s991 :: SWord8 = if s18 then s978 else s990 + s992 :: SWord8 = s33 + s991 + s993 :: SWord8 = if s880 then s992 else s991 + s994 :: SBool = s177 == s877 + s995 :: SBool = s180 == s877 + s996 :: SWord8 = if s995 then s992 else s991 + s997 :: SWord8 = s33 + s996 + s998 :: SWord8 = if s994 then s997 else s996 + s999 :: SBool = s185 == s877 + s1000 :: SWord8 = if s999 then s992 else s991 + s1001 :: SWord8 = s33 + s1000 + s1002 :: SWord8 = if s995 then s1001 else s1000 + s1003 :: SWord8 = s33 + s1002 + s1004 :: SWord8 = if s994 then s1003 else s1002 + s1005 :: SWord8 = if s176 then s998 else s1004 + s1006 :: SWord8 = if s16 then s993 else s1005 + s1007 :: SWord8 = s33 + s1006 + s1008 :: SWord8 = if s879 then s1007 else s1006 + s1009 :: SBool = s197 == s877 + s1010 :: SBool = s200 == s877 + s1011 :: SWord8 = if s1010 then s1007 else s1006 + s1012 :: SWord8 = s33 + s1011 + s1013 :: SWord8 = if s1009 then s1012 else s1011 + s1014 :: SBool = s205 == s877 + s1015 :: SWord8 = if s1014 then s1007 else s1006 + s1016 :: SWord8 = s33 + s1015 + s1017 :: SWord8 = if s1010 then s1016 else s1015 + s1018 :: SWord8 = s33 + s1017 + s1019 :: SWord8 = if s1009 then s1018 else s1017 + s1020 :: SWord8 = if s196 then s1013 else s1019 + s1021 :: SWord8 = if s14 then s1008 else s1020 + s1022 :: SWord8 = s33 + s1021 + s1023 :: SWord8 = if s878 then s1022 else s1021 + s1024 :: SBool = s217 == s877 + s1025 :: SBool = s220 == s877 + s1026 :: SWord8 = if s1025 then s1022 else s1021 + s1027 :: SWord8 = s33 + s1026 + s1028 :: SWord8 = if s1024 then s1027 else s1026 + s1029 :: SBool = s225 == s877 + s1030 :: SWord8 = if s1029 then s1022 else s1021 + s1031 :: SWord8 = s33 + s1030 + s1032 :: SWord8 = if s1025 then s1031 else s1030 + s1033 :: SWord8 = s33 + s1032 + s1034 :: SWord8 = if s1024 then s1033 else s1032 + s1035 :: SWord8 = if s216 then s1028 else s1034 + s1036 :: SWord8 = if s11 then s1023 else s1035 + s1037 :: SBool = s5 == s1036 + s1039 :: SBool = s9 == s1038 + s1040 :: SBool = s8 == s1038 + s1041 :: SBool = s7 == s1038 + s1042 :: SBool = s6 == s1038 + s1043 :: SBool = s5 == s1038 + s1044 :: SBool = s4 == s1038 + s1045 :: SBool = s3 == s1038 + s1046 :: SBool = s2 == s1038 + s1047 :: SBool = s1 == s1038 + s1048 :: SBool = s0 == s1038 + s1049 :: SWord8 = if s1048 then s32 else s33 + s1050 :: SBool = s37 == s1038 + s1051 :: SBool = s40 == s1038 + s1052 :: SWord8 = if s1051 then s32 else s33 + s1053 :: SWord8 = s33 + s1052 + s1054 :: SWord8 = if s1050 then s1053 else s1052 + s1055 :: SBool = s45 == s1038 + s1056 :: SWord8 = if s1055 then s32 else s33 + s1057 :: SWord8 = s33 + s1056 + s1058 :: SWord8 = if s1051 then s1057 else s1056 + s1059 :: SWord8 = s33 + s1058 + s1060 :: SWord8 = if s1050 then s1059 else s1058 + s1061 :: SWord8 = if s36 then s1054 else s1060 + s1062 :: SWord8 = if s30 then s1049 else s1061 + s1063 :: SWord8 = s33 + s1062 + s1064 :: SWord8 = if s1047 then s1063 else s1062 + s1065 :: SBool = s57 == s1038 + s1066 :: SBool = s60 == s1038 + s1067 :: SWord8 = if s1066 then s1063 else s1062 + s1068 :: SWord8 = s33 + s1067 + s1069 :: SWord8 = if s1065 then s1068 else s1067 + s1070 :: SBool = s65 == s1038 + s1071 :: SWord8 = if s1070 then s1063 else s1062 + s1072 :: SWord8 = s33 + s1071 + s1073 :: SWord8 = if s1066 then s1072 else s1071 + s1074 :: SWord8 = s33 + s1073 + s1075 :: SWord8 = if s1065 then s1074 else s1073 + s1076 :: SWord8 = if s56 then s1069 else s1075 + s1077 :: SWord8 = if s28 then s1064 else s1076 + s1078 :: SWord8 = s33 + s1077 + s1079 :: SWord8 = if s1046 then s1078 else s1077 + s1080 :: SBool = s77 == s1038 + s1081 :: SBool = s80 == s1038 + s1082 :: SWord8 = if s1081 then s1078 else s1077 + s1083 :: SWord8 = s33 + s1082 + s1084 :: SWord8 = if s1080 then s1083 else s1082 + s1085 :: SBool = s85 == s1038 + s1086 :: SWord8 = if s1085 then s1078 else s1077 + s1087 :: SWord8 = s33 + s1086 + s1088 :: SWord8 = if s1081 then s1087 else s1086 + s1089 :: SWord8 = s33 + s1088 + s1090 :: SWord8 = if s1080 then s1089 else s1088 + s1091 :: SWord8 = if s76 then s1084 else s1090 + s1092 :: SWord8 = if s26 then s1079 else s1091 + s1093 :: SWord8 = s33 + s1092 + s1094 :: SWord8 = if s1045 then s1093 else s1092 + s1095 :: SBool = s97 == s1038 + s1096 :: SBool = s100 == s1038 + s1097 :: SWord8 = if s1096 then s1093 else s1092 + s1098 :: SWord8 = s33 + s1097 + s1099 :: SWord8 = if s1095 then s1098 else s1097 + s1100 :: SBool = s105 == s1038 + s1101 :: SWord8 = if s1100 then s1093 else s1092 + s1102 :: SWord8 = s33 + s1101 + s1103 :: SWord8 = if s1096 then s1102 else s1101 + s1104 :: SWord8 = s33 + s1103 + s1105 :: SWord8 = if s1095 then s1104 else s1103 + s1106 :: SWord8 = if s96 then s1099 else s1105 + s1107 :: SWord8 = if s24 then s1094 else s1106 + s1108 :: SWord8 = s33 + s1107 + s1109 :: SWord8 = if s1044 then s1108 else s1107 + s1110 :: SBool = s117 == s1038 + s1111 :: SBool = s120 == s1038 + s1112 :: SWord8 = if s1111 then s1108 else s1107 + s1113 :: SWord8 = s33 + s1112 + s1114 :: SWord8 = if s1110 then s1113 else s1112 + s1115 :: SBool = s125 == s1038 + s1116 :: SWord8 = if s1115 then s1108 else s1107 + s1117 :: SWord8 = s33 + s1116 + s1118 :: SWord8 = if s1111 then s1117 else s1116 + s1119 :: SWord8 = s33 + s1118 + s1120 :: SWord8 = if s1110 then s1119 else s1118 + s1121 :: SWord8 = if s116 then s1114 else s1120 + s1122 :: SWord8 = if s22 then s1109 else s1121 + s1123 :: SWord8 = s33 + s1122 + s1124 :: SWord8 = if s1043 then s1123 else s1122 + s1125 :: SBool = s137 == s1038 + s1126 :: SBool = s140 == s1038 + s1127 :: SWord8 = if s1126 then s1123 else s1122 + s1128 :: SWord8 = s33 + s1127 + s1129 :: SWord8 = if s1125 then s1128 else s1127 + s1130 :: SBool = s145 == s1038 + s1131 :: SWord8 = if s1130 then s1123 else s1122 + s1132 :: SWord8 = s33 + s1131 + s1133 :: SWord8 = if s1126 then s1132 else s1131 + s1134 :: SWord8 = s33 + s1133 + s1135 :: SWord8 = if s1125 then s1134 else s1133 + s1136 :: SWord8 = if s136 then s1129 else s1135 + s1137 :: SWord8 = if s20 then s1124 else s1136 + s1138 :: SWord8 = s33 + s1137 + s1139 :: SWord8 = if s1042 then s1138 else s1137 + s1140 :: SBool = s157 == s1038 + s1141 :: SBool = s160 == s1038 + s1142 :: SWord8 = if s1141 then s1138 else s1137 + s1143 :: SWord8 = s33 + s1142 + s1144 :: SWord8 = if s1140 then s1143 else s1142 + s1145 :: SBool = s165 == s1038 + s1146 :: SWord8 = if s1145 then s1138 else s1137 + s1147 :: SWord8 = s33 + s1146 + s1148 :: SWord8 = if s1141 then s1147 else s1146 + s1149 :: SWord8 = s33 + s1148 + s1150 :: SWord8 = if s1140 then s1149 else s1148 + s1151 :: SWord8 = if s156 then s1144 else s1150 + s1152 :: SWord8 = if s18 then s1139 else s1151 + s1153 :: SWord8 = s33 + s1152 + s1154 :: SWord8 = if s1041 then s1153 else s1152 + s1155 :: SBool = s177 == s1038 + s1156 :: SBool = s180 == s1038 + s1157 :: SWord8 = if s1156 then s1153 else s1152 + s1158 :: SWord8 = s33 + s1157 + s1159 :: SWord8 = if s1155 then s1158 else s1157 + s1160 :: SBool = s185 == s1038 + s1161 :: SWord8 = if s1160 then s1153 else s1152 + s1162 :: SWord8 = s33 + s1161 + s1163 :: SWord8 = if s1156 then s1162 else s1161 + s1164 :: SWord8 = s33 + s1163 + s1165 :: SWord8 = if s1155 then s1164 else s1163 + s1166 :: SWord8 = if s176 then s1159 else s1165 + s1167 :: SWord8 = if s16 then s1154 else s1166 + s1168 :: SWord8 = s33 + s1167 + s1169 :: SWord8 = if s1040 then s1168 else s1167 + s1170 :: SBool = s197 == s1038 + s1171 :: SBool = s200 == s1038 + s1172 :: SWord8 = if s1171 then s1168 else s1167 + s1173 :: SWord8 = s33 + s1172 + s1174 :: SWord8 = if s1170 then s1173 else s1172 + s1175 :: SBool = s205 == s1038 + s1176 :: SWord8 = if s1175 then s1168 else s1167 + s1177 :: SWord8 = s33 + s1176 + s1178 :: SWord8 = if s1171 then s1177 else s1176 + s1179 :: SWord8 = s33 + s1178 + s1180 :: SWord8 = if s1170 then s1179 else s1178 + s1181 :: SWord8 = if s196 then s1174 else s1180 + s1182 :: SWord8 = if s14 then s1169 else s1181 + s1183 :: SWord8 = s33 + s1182 + s1184 :: SWord8 = if s1039 then s1183 else s1182 + s1185 :: SBool = s217 == s1038 + s1186 :: SBool = s220 == s1038 + s1187 :: SWord8 = if s1186 then s1183 else s1182 + s1188 :: SWord8 = s33 + s1187 + s1189 :: SWord8 = if s1185 then s1188 else s1187 + s1190 :: SBool = s225 == s1038 + s1191 :: SWord8 = if s1190 then s1183 else s1182 + s1192 :: SWord8 = s33 + s1191 + s1193 :: SWord8 = if s1186 then s1192 else s1191 + s1194 :: SWord8 = s33 + s1193 + s1195 :: SWord8 = if s1185 then s1194 else s1193 + s1196 :: SWord8 = if s216 then s1189 else s1195 + s1197 :: SWord8 = if s11 then s1184 else s1196 + s1198 :: SBool = s6 == s1197 + s1200 :: SBool = s9 == s1199 + s1201 :: SBool = s8 == s1199 + s1202 :: SBool = s7 == s1199 + s1203 :: SBool = s6 == s1199 + s1204 :: SBool = s5 == s1199 + s1205 :: SBool = s4 == s1199 + s1206 :: SBool = s3 == s1199 + s1207 :: SBool = s2 == s1199 + s1208 :: SBool = s1 == s1199 + s1209 :: SBool = s0 == s1199 + s1210 :: SWord8 = if s1209 then s32 else s33 + s1211 :: SBool = s37 == s1199 + s1212 :: SBool = s40 == s1199 + s1213 :: SWord8 = if s1212 then s32 else s33 + s1214 :: SWord8 = s33 + s1213 + s1215 :: SWord8 = if s1211 then s1214 else s1213 + s1216 :: SBool = s45 == s1199 + s1217 :: SWord8 = if s1216 then s32 else s33 + s1218 :: SWord8 = s33 + s1217 + s1219 :: SWord8 = if s1212 then s1218 else s1217 + s1220 :: SWord8 = s33 + s1219 + s1221 :: SWord8 = if s1211 then s1220 else s1219 + s1222 :: SWord8 = if s36 then s1215 else s1221 + s1223 :: SWord8 = if s30 then s1210 else s1222 + s1224 :: SWord8 = s33 + s1223 + s1225 :: SWord8 = if s1208 then s1224 else s1223 + s1226 :: SBool = s57 == s1199 + s1227 :: SBool = s60 == s1199 + s1228 :: SWord8 = if s1227 then s1224 else s1223 + s1229 :: SWord8 = s33 + s1228 + s1230 :: SWord8 = if s1226 then s1229 else s1228 + s1231 :: SBool = s65 == s1199 + s1232 :: SWord8 = if s1231 then s1224 else s1223 + s1233 :: SWord8 = s33 + s1232 + s1234 :: SWord8 = if s1227 then s1233 else s1232 + s1235 :: SWord8 = s33 + s1234 + s1236 :: SWord8 = if s1226 then s1235 else s1234 + s1237 :: SWord8 = if s56 then s1230 else s1236 + s1238 :: SWord8 = if s28 then s1225 else s1237 + s1239 :: SWord8 = s33 + s1238 + s1240 :: SWord8 = if s1207 then s1239 else s1238 + s1241 :: SBool = s77 == s1199 + s1242 :: SBool = s80 == s1199 + s1243 :: SWord8 = if s1242 then s1239 else s1238 + s1244 :: SWord8 = s33 + s1243 + s1245 :: SWord8 = if s1241 then s1244 else s1243 + s1246 :: SBool = s85 == s1199 + s1247 :: SWord8 = if s1246 then s1239 else s1238 + s1248 :: SWord8 = s33 + s1247 + s1249 :: SWord8 = if s1242 then s1248 else s1247 + s1250 :: SWord8 = s33 + s1249 + s1251 :: SWord8 = if s1241 then s1250 else s1249 + s1252 :: SWord8 = if s76 then s1245 else s1251 + s1253 :: SWord8 = if s26 then s1240 else s1252 + s1254 :: SWord8 = s33 + s1253 + s1255 :: SWord8 = if s1206 then s1254 else s1253 + s1256 :: SBool = s97 == s1199 + s1257 :: SBool = s100 == s1199 + s1258 :: SWord8 = if s1257 then s1254 else s1253 + s1259 :: SWord8 = s33 + s1258 + s1260 :: SWord8 = if s1256 then s1259 else s1258 + s1261 :: SBool = s105 == s1199 + s1262 :: SWord8 = if s1261 then s1254 else s1253 + s1263 :: SWord8 = s33 + s1262 + s1264 :: SWord8 = if s1257 then s1263 else s1262 + s1265 :: SWord8 = s33 + s1264 + s1266 :: SWord8 = if s1256 then s1265 else s1264 + s1267 :: SWord8 = if s96 then s1260 else s1266 + s1268 :: SWord8 = if s24 then s1255 else s1267 + s1269 :: SWord8 = s33 + s1268 + s1270 :: SWord8 = if s1205 then s1269 else s1268 + s1271 :: SBool = s117 == s1199 + s1272 :: SBool = s120 == s1199 + s1273 :: SWord8 = if s1272 then s1269 else s1268 + s1274 :: SWord8 = s33 + s1273 + s1275 :: SWord8 = if s1271 then s1274 else s1273 + s1276 :: SBool = s125 == s1199 + s1277 :: SWord8 = if s1276 then s1269 else s1268 + s1278 :: SWord8 = s33 + s1277 + s1279 :: SWord8 = if s1272 then s1278 else s1277 + s1280 :: SWord8 = s33 + s1279 + s1281 :: SWord8 = if s1271 then s1280 else s1279 + s1282 :: SWord8 = if s116 then s1275 else s1281 + s1283 :: SWord8 = if s22 then s1270 else s1282 + s1284 :: SWord8 = s33 + s1283 + s1285 :: SWord8 = if s1204 then s1284 else s1283 + s1286 :: SBool = s137 == s1199 + s1287 :: SBool = s140 == s1199 + s1288 :: SWord8 = if s1287 then s1284 else s1283 + s1289 :: SWord8 = s33 + s1288 + s1290 :: SWord8 = if s1286 then s1289 else s1288 + s1291 :: SBool = s145 == s1199 + s1292 :: SWord8 = if s1291 then s1284 else s1283 + s1293 :: SWord8 = s33 + s1292 + s1294 :: SWord8 = if s1287 then s1293 else s1292 + s1295 :: SWord8 = s33 + s1294 + s1296 :: SWord8 = if s1286 then s1295 else s1294 + s1297 :: SWord8 = if s136 then s1290 else s1296 + s1298 :: SWord8 = if s20 then s1285 else s1297 + s1299 :: SWord8 = s33 + s1298 + s1300 :: SWord8 = if s1203 then s1299 else s1298 + s1301 :: SBool = s157 == s1199 + s1302 :: SBool = s160 == s1199 + s1303 :: SWord8 = if s1302 then s1299 else s1298 + s1304 :: SWord8 = s33 + s1303 + s1305 :: SWord8 = if s1301 then s1304 else s1303 + s1306 :: SBool = s165 == s1199 + s1307 :: SWord8 = if s1306 then s1299 else s1298 + s1308 :: SWord8 = s33 + s1307 + s1309 :: SWord8 = if s1302 then s1308 else s1307 + s1310 :: SWord8 = s33 + s1309 + s1311 :: SWord8 = if s1301 then s1310 else s1309 + s1312 :: SWord8 = if s156 then s1305 else s1311 + s1313 :: SWord8 = if s18 then s1300 else s1312 + s1314 :: SWord8 = s33 + s1313 + s1315 :: SWord8 = if s1202 then s1314 else s1313 + s1316 :: SBool = s177 == s1199 + s1317 :: SBool = s180 == s1199 + s1318 :: SWord8 = if s1317 then s1314 else s1313 + s1319 :: SWord8 = s33 + s1318 + s1320 :: SWord8 = if s1316 then s1319 else s1318 + s1321 :: SBool = s185 == s1199 + s1322 :: SWord8 = if s1321 then s1314 else s1313 + s1323 :: SWord8 = s33 + s1322 + s1324 :: SWord8 = if s1317 then s1323 else s1322 + s1325 :: SWord8 = s33 + s1324 + s1326 :: SWord8 = if s1316 then s1325 else s1324 + s1327 :: SWord8 = if s176 then s1320 else s1326 + s1328 :: SWord8 = if s16 then s1315 else s1327 + s1329 :: SWord8 = s33 + s1328 + s1330 :: SWord8 = if s1201 then s1329 else s1328 + s1331 :: SBool = s197 == s1199 + s1332 :: SBool = s200 == s1199 + s1333 :: SWord8 = if s1332 then s1329 else s1328 + s1334 :: SWord8 = s33 + s1333 + s1335 :: SWord8 = if s1331 then s1334 else s1333 + s1336 :: SBool = s205 == s1199 + s1337 :: SWord8 = if s1336 then s1329 else s1328 + s1338 :: SWord8 = s33 + s1337 + s1339 :: SWord8 = if s1332 then s1338 else s1337 + s1340 :: SWord8 = s33 + s1339 + s1341 :: SWord8 = if s1331 then s1340 else s1339 + s1342 :: SWord8 = if s196 then s1335 else s1341 + s1343 :: SWord8 = if s14 then s1330 else s1342 + s1344 :: SWord8 = s33 + s1343 + s1345 :: SWord8 = if s1200 then s1344 else s1343 + s1346 :: SBool = s217 == s1199 + s1347 :: SBool = s220 == s1199 + s1348 :: SWord8 = if s1347 then s1344 else s1343 + s1349 :: SWord8 = s33 + s1348 + s1350 :: SWord8 = if s1346 then s1349 else s1348 + s1351 :: SBool = s225 == s1199 + s1352 :: SWord8 = if s1351 then s1344 else s1343 + s1353 :: SWord8 = s33 + s1352 + s1354 :: SWord8 = if s1347 then s1353 else s1352 + s1355 :: SWord8 = s33 + s1354 + s1356 :: SWord8 = if s1346 then s1355 else s1354 + s1357 :: SWord8 = if s216 then s1350 else s1356 + s1358 :: SWord8 = if s11 then s1345 else s1357 + s1359 :: SBool = s7 == s1358 + s1361 :: SBool = s9 == s1360 + s1362 :: SBool = s8 == s1360 + s1363 :: SBool = s7 == s1360 + s1364 :: SBool = s6 == s1360 + s1365 :: SBool = s5 == s1360 + s1366 :: SBool = s4 == s1360 + s1367 :: SBool = s3 == s1360 + s1368 :: SBool = s2 == s1360 + s1369 :: SBool = s1 == s1360 + s1370 :: SBool = s0 == s1360 + s1371 :: SWord8 = if s1370 then s32 else s33 + s1372 :: SBool = s37 == s1360 + s1373 :: SBool = s40 == s1360 + s1374 :: SWord8 = if s1373 then s32 else s33 + s1375 :: SWord8 = s33 + s1374 + s1376 :: SWord8 = if s1372 then s1375 else s1374 + s1377 :: SBool = s45 == s1360 + s1378 :: SWord8 = if s1377 then s32 else s33 + s1379 :: SWord8 = s33 + s1378 + s1380 :: SWord8 = if s1373 then s1379 else s1378 + s1381 :: SWord8 = s33 + s1380 + s1382 :: SWord8 = if s1372 then s1381 else s1380 + s1383 :: SWord8 = if s36 then s1376 else s1382 + s1384 :: SWord8 = if s30 then s1371 else s1383 + s1385 :: SWord8 = s33 + s1384 + s1386 :: SWord8 = if s1369 then s1385 else s1384 + s1387 :: SBool = s57 == s1360 + s1388 :: SBool = s60 == s1360 + s1389 :: SWord8 = if s1388 then s1385 else s1384 + s1390 :: SWord8 = s33 + s1389 + s1391 :: SWord8 = if s1387 then s1390 else s1389 + s1392 :: SBool = s65 == s1360 + s1393 :: SWord8 = if s1392 then s1385 else s1384 + s1394 :: SWord8 = s33 + s1393 + s1395 :: SWord8 = if s1388 then s1394 else s1393 + s1396 :: SWord8 = s33 + s1395 + s1397 :: SWord8 = if s1387 then s1396 else s1395 + s1398 :: SWord8 = if s56 then s1391 else s1397 + s1399 :: SWord8 = if s28 then s1386 else s1398 + s1400 :: SWord8 = s33 + s1399 + s1401 :: SWord8 = if s1368 then s1400 else s1399 + s1402 :: SBool = s77 == s1360 + s1403 :: SBool = s80 == s1360 + s1404 :: SWord8 = if s1403 then s1400 else s1399 + s1405 :: SWord8 = s33 + s1404 + s1406 :: SWord8 = if s1402 then s1405 else s1404 + s1407 :: SBool = s85 == s1360 + s1408 :: SWord8 = if s1407 then s1400 else s1399 + s1409 :: SWord8 = s33 + s1408 + s1410 :: SWord8 = if s1403 then s1409 else s1408 + s1411 :: SWord8 = s33 + s1410 + s1412 :: SWord8 = if s1402 then s1411 else s1410 + s1413 :: SWord8 = if s76 then s1406 else s1412 + s1414 :: SWord8 = if s26 then s1401 else s1413 + s1415 :: SWord8 = s33 + s1414 + s1416 :: SWord8 = if s1367 then s1415 else s1414 + s1417 :: SBool = s97 == s1360 + s1418 :: SBool = s100 == s1360 + s1419 :: SWord8 = if s1418 then s1415 else s1414 + s1420 :: SWord8 = s33 + s1419 + s1421 :: SWord8 = if s1417 then s1420 else s1419 + s1422 :: SBool = s105 == s1360 + s1423 :: SWord8 = if s1422 then s1415 else s1414 + s1424 :: SWord8 = s33 + s1423 + s1425 :: SWord8 = if s1418 then s1424 else s1423 + s1426 :: SWord8 = s33 + s1425 + s1427 :: SWord8 = if s1417 then s1426 else s1425 + s1428 :: SWord8 = if s96 then s1421 else s1427 + s1429 :: SWord8 = if s24 then s1416 else s1428 + s1430 :: SWord8 = s33 + s1429 + s1431 :: SWord8 = if s1366 then s1430 else s1429 + s1432 :: SBool = s117 == s1360 + s1433 :: SBool = s120 == s1360 + s1434 :: SWord8 = if s1433 then s1430 else s1429 + s1435 :: SWord8 = s33 + s1434 + s1436 :: SWord8 = if s1432 then s1435 else s1434 + s1437 :: SBool = s125 == s1360 + s1438 :: SWord8 = if s1437 then s1430 else s1429 + s1439 :: SWord8 = s33 + s1438 + s1440 :: SWord8 = if s1433 then s1439 else s1438 + s1441 :: SWord8 = s33 + s1440 + s1442 :: SWord8 = if s1432 then s1441 else s1440 + s1443 :: SWord8 = if s116 then s1436 else s1442 + s1444 :: SWord8 = if s22 then s1431 else s1443 + s1445 :: SWord8 = s33 + s1444 + s1446 :: SWord8 = if s1365 then s1445 else s1444 + s1447 :: SBool = s137 == s1360 + s1448 :: SBool = s140 == s1360 + s1449 :: SWord8 = if s1448 then s1445 else s1444 + s1450 :: SWord8 = s33 + s1449 + s1451 :: SWord8 = if s1447 then s1450 else s1449 + s1452 :: SBool = s145 == s1360 + s1453 :: SWord8 = if s1452 then s1445 else s1444 + s1454 :: SWord8 = s33 + s1453 + s1455 :: SWord8 = if s1448 then s1454 else s1453 + s1456 :: SWord8 = s33 + s1455 + s1457 :: SWord8 = if s1447 then s1456 else s1455 + s1458 :: SWord8 = if s136 then s1451 else s1457 + s1459 :: SWord8 = if s20 then s1446 else s1458 + s1460 :: SWord8 = s33 + s1459 + s1461 :: SWord8 = if s1364 then s1460 else s1459 + s1462 :: SBool = s157 == s1360 + s1463 :: SBool = s160 == s1360 + s1464 :: SWord8 = if s1463 then s1460 else s1459 + s1465 :: SWord8 = s33 + s1464 + s1466 :: SWord8 = if s1462 then s1465 else s1464 + s1467 :: SBool = s165 == s1360 + s1468 :: SWord8 = if s1467 then s1460 else s1459 + s1469 :: SWord8 = s33 + s1468 + s1470 :: SWord8 = if s1463 then s1469 else s1468 + s1471 :: SWord8 = s33 + s1470 + s1472 :: SWord8 = if s1462 then s1471 else s1470 + s1473 :: SWord8 = if s156 then s1466 else s1472 + s1474 :: SWord8 = if s18 then s1461 else s1473 + s1475 :: SWord8 = s33 + s1474 + s1476 :: SWord8 = if s1363 then s1475 else s1474 + s1477 :: SBool = s177 == s1360 + s1478 :: SBool = s180 == s1360 + s1479 :: SWord8 = if s1478 then s1475 else s1474 + s1480 :: SWord8 = s33 + s1479 + s1481 :: SWord8 = if s1477 then s1480 else s1479 + s1482 :: SBool = s185 == s1360 + s1483 :: SWord8 = if s1482 then s1475 else s1474 + s1484 :: SWord8 = s33 + s1483 + s1485 :: SWord8 = if s1478 then s1484 else s1483 + s1486 :: SWord8 = s33 + s1485 + s1487 :: SWord8 = if s1477 then s1486 else s1485 + s1488 :: SWord8 = if s176 then s1481 else s1487 + s1489 :: SWord8 = if s16 then s1476 else s1488 + s1490 :: SWord8 = s33 + s1489 + s1491 :: SWord8 = if s1362 then s1490 else s1489 + s1492 :: SBool = s197 == s1360 + s1493 :: SBool = s200 == s1360 + s1494 :: SWord8 = if s1493 then s1490 else s1489 + s1495 :: SWord8 = s33 + s1494 + s1496 :: SWord8 = if s1492 then s1495 else s1494 + s1497 :: SBool = s205 == s1360 + s1498 :: SWord8 = if s1497 then s1490 else s1489 + s1499 :: SWord8 = s33 + s1498 + s1500 :: SWord8 = if s1493 then s1499 else s1498 + s1501 :: SWord8 = s33 + s1500 + s1502 :: SWord8 = if s1492 then s1501 else s1500 + s1503 :: SWord8 = if s196 then s1496 else s1502 + s1504 :: SWord8 = if s14 then s1491 else s1503 + s1505 :: SWord8 = s33 + s1504 + s1506 :: SWord8 = if s1361 then s1505 else s1504 + s1507 :: SBool = s217 == s1360 + s1508 :: SBool = s220 == s1360 + s1509 :: SWord8 = if s1508 then s1505 else s1504 + s1510 :: SWord8 = s33 + s1509 + s1511 :: SWord8 = if s1507 then s1510 else s1509 + s1512 :: SBool = s225 == s1360 + s1513 :: SWord8 = if s1512 then s1505 else s1504 + s1514 :: SWord8 = s33 + s1513 + s1515 :: SWord8 = if s1508 then s1514 else s1513 + s1516 :: SWord8 = s33 + s1515 + s1517 :: SWord8 = if s1507 then s1516 else s1515 + s1518 :: SWord8 = if s216 then s1511 else s1517 + s1519 :: SWord8 = if s11 then s1506 else s1518 + s1520 :: SBool = s8 == s1519 + s1522 :: SBool = s9 == s1521 + s1523 :: SBool = s8 == s1521 + s1524 :: SBool = s7 == s1521 + s1525 :: SBool = s6 == s1521 + s1526 :: SBool = s5 == s1521 + s1527 :: SBool = s4 == s1521 + s1528 :: SBool = s3 == s1521 + s1529 :: SBool = s2 == s1521 + s1530 :: SBool = s1 == s1521 + s1531 :: SBool = s0 == s1521 + s1532 :: SWord8 = if s1531 then s32 else s33 + s1533 :: SBool = s37 == s1521 + s1534 :: SBool = s40 == s1521 + s1535 :: SWord8 = if s1534 then s32 else s33 + s1536 :: SWord8 = s33 + s1535 + s1537 :: SWord8 = if s1533 then s1536 else s1535 + s1538 :: SBool = s45 == s1521 + s1539 :: SWord8 = if s1538 then s32 else s33 + s1540 :: SWord8 = s33 + s1539 + s1541 :: SWord8 = if s1534 then s1540 else s1539 + s1542 :: SWord8 = s33 + s1541 + s1543 :: SWord8 = if s1533 then s1542 else s1541 + s1544 :: SWord8 = if s36 then s1537 else s1543 + s1545 :: SWord8 = if s30 then s1532 else s1544 + s1546 :: SWord8 = s33 + s1545 + s1547 :: SWord8 = if s1530 then s1546 else s1545 + s1548 :: SBool = s57 == s1521 + s1549 :: SBool = s60 == s1521 + s1550 :: SWord8 = if s1549 then s1546 else s1545 + s1551 :: SWord8 = s33 + s1550 + s1552 :: SWord8 = if s1548 then s1551 else s1550 + s1553 :: SBool = s65 == s1521 + s1554 :: SWord8 = if s1553 then s1546 else s1545 + s1555 :: SWord8 = s33 + s1554 + s1556 :: SWord8 = if s1549 then s1555 else s1554 + s1557 :: SWord8 = s33 + s1556 + s1558 :: SWord8 = if s1548 then s1557 else s1556 + s1559 :: SWord8 = if s56 then s1552 else s1558 + s1560 :: SWord8 = if s28 then s1547 else s1559 + s1561 :: SWord8 = s33 + s1560 + s1562 :: SWord8 = if s1529 then s1561 else s1560 + s1563 :: SBool = s77 == s1521 + s1564 :: SBool = s80 == s1521 + s1565 :: SWord8 = if s1564 then s1561 else s1560 + s1566 :: SWord8 = s33 + s1565 + s1567 :: SWord8 = if s1563 then s1566 else s1565 + s1568 :: SBool = s85 == s1521 + s1569 :: SWord8 = if s1568 then s1561 else s1560 + s1570 :: SWord8 = s33 + s1569 + s1571 :: SWord8 = if s1564 then s1570 else s1569 + s1572 :: SWord8 = s33 + s1571 + s1573 :: SWord8 = if s1563 then s1572 else s1571 + s1574 :: SWord8 = if s76 then s1567 else s1573 + s1575 :: SWord8 = if s26 then s1562 else s1574 + s1576 :: SWord8 = s33 + s1575 + s1577 :: SWord8 = if s1528 then s1576 else s1575 + s1578 :: SBool = s97 == s1521 + s1579 :: SBool = s100 == s1521 + s1580 :: SWord8 = if s1579 then s1576 else s1575 + s1581 :: SWord8 = s33 + s1580 + s1582 :: SWord8 = if s1578 then s1581 else s1580 + s1583 :: SBool = s105 == s1521 + s1584 :: SWord8 = if s1583 then s1576 else s1575 + s1585 :: SWord8 = s33 + s1584 + s1586 :: SWord8 = if s1579 then s1585 else s1584 + s1587 :: SWord8 = s33 + s1586 + s1588 :: SWord8 = if s1578 then s1587 else s1586 + s1589 :: SWord8 = if s96 then s1582 else s1588 + s1590 :: SWord8 = if s24 then s1577 else s1589 + s1591 :: SWord8 = s33 + s1590 + s1592 :: SWord8 = if s1527 then s1591 else s1590 + s1593 :: SBool = s117 == s1521 + s1594 :: SBool = s120 == s1521 + s1595 :: SWord8 = if s1594 then s1591 else s1590 + s1596 :: SWord8 = s33 + s1595 + s1597 :: SWord8 = if s1593 then s1596 else s1595 + s1598 :: SBool = s125 == s1521 + s1599 :: SWord8 = if s1598 then s1591 else s1590 + s1600 :: SWord8 = s33 + s1599 + s1601 :: SWord8 = if s1594 then s1600 else s1599 + s1602 :: SWord8 = s33 + s1601 + s1603 :: SWord8 = if s1593 then s1602 else s1601 + s1604 :: SWord8 = if s116 then s1597 else s1603 + s1605 :: SWord8 = if s22 then s1592 else s1604 + s1606 :: SWord8 = s33 + s1605 + s1607 :: SWord8 = if s1526 then s1606 else s1605 + s1608 :: SBool = s137 == s1521 + s1609 :: SBool = s140 == s1521 + s1610 :: SWord8 = if s1609 then s1606 else s1605 + s1611 :: SWord8 = s33 + s1610 + s1612 :: SWord8 = if s1608 then s1611 else s1610 + s1613 :: SBool = s145 == s1521 + s1614 :: SWord8 = if s1613 then s1606 else s1605 + s1615 :: SWord8 = s33 + s1614 + s1616 :: SWord8 = if s1609 then s1615 else s1614 + s1617 :: SWord8 = s33 + s1616 + s1618 :: SWord8 = if s1608 then s1617 else s1616 + s1619 :: SWord8 = if s136 then s1612 else s1618 + s1620 :: SWord8 = if s20 then s1607 else s1619 + s1621 :: SWord8 = s33 + s1620 + s1622 :: SWord8 = if s1525 then s1621 else s1620 + s1623 :: SBool = s157 == s1521 + s1624 :: SBool = s160 == s1521 + s1625 :: SWord8 = if s1624 then s1621 else s1620 + s1626 :: SWord8 = s33 + s1625 + s1627 :: SWord8 = if s1623 then s1626 else s1625 + s1628 :: SBool = s165 == s1521 + s1629 :: SWord8 = if s1628 then s1621 else s1620 + s1630 :: SWord8 = s33 + s1629 + s1631 :: SWord8 = if s1624 then s1630 else s1629 + s1632 :: SWord8 = s33 + s1631 + s1633 :: SWord8 = if s1623 then s1632 else s1631 + s1634 :: SWord8 = if s156 then s1627 else s1633 + s1635 :: SWord8 = if s18 then s1622 else s1634 + s1636 :: SWord8 = s33 + s1635 + s1637 :: SWord8 = if s1524 then s1636 else s1635 + s1638 :: SBool = s177 == s1521 + s1639 :: SBool = s180 == s1521 + s1640 :: SWord8 = if s1639 then s1636 else s1635 + s1641 :: SWord8 = s33 + s1640 + s1642 :: SWord8 = if s1638 then s1641 else s1640 + s1643 :: SBool = s185 == s1521 + s1644 :: SWord8 = if s1643 then s1636 else s1635 + s1645 :: SWord8 = s33 + s1644 + s1646 :: SWord8 = if s1639 then s1645 else s1644 + s1647 :: SWord8 = s33 + s1646 + s1648 :: SWord8 = if s1638 then s1647 else s1646 + s1649 :: SWord8 = if s176 then s1642 else s1648 + s1650 :: SWord8 = if s16 then s1637 else s1649 + s1651 :: SWord8 = s33 + s1650 + s1652 :: SWord8 = if s1523 then s1651 else s1650 + s1653 :: SBool = s197 == s1521 + s1654 :: SBool = s200 == s1521 + s1655 :: SWord8 = if s1654 then s1651 else s1650 + s1656 :: SWord8 = s33 + s1655 + s1657 :: SWord8 = if s1653 then s1656 else s1655 + s1658 :: SBool = s205 == s1521 + s1659 :: SWord8 = if s1658 then s1651 else s1650 + s1660 :: SWord8 = s33 + s1659 + s1661 :: SWord8 = if s1654 then s1660 else s1659 + s1662 :: SWord8 = s33 + s1661 + s1663 :: SWord8 = if s1653 then s1662 else s1661 + s1664 :: SWord8 = if s196 then s1657 else s1663 + s1665 :: SWord8 = if s14 then s1652 else s1664 + s1666 :: SWord8 = s33 + s1665 + s1667 :: SWord8 = if s1522 then s1666 else s1665 + s1668 :: SBool = s217 == s1521 + s1669 :: SBool = s220 == s1521 + s1670 :: SWord8 = if s1669 then s1666 else s1665 + s1671 :: SWord8 = s33 + s1670 + s1672 :: SWord8 = if s1668 then s1671 else s1670 + s1673 :: SBool = s225 == s1521 + s1674 :: SWord8 = if s1673 then s1666 else s1665 + s1675 :: SWord8 = s33 + s1674 + s1676 :: SWord8 = if s1669 then s1675 else s1674 + s1677 :: SWord8 = s33 + s1676 + s1678 :: SWord8 = if s1668 then s1677 else s1676 + s1679 :: SWord8 = if s216 then s1672 else s1678 + s1680 :: SWord8 = if s11 then s1667 else s1679 + s1681 :: SBool = s9 == s1680 + s1682 :: SBool = s1520 & s1681 + s1683 :: SBool = s1359 & s1682 + s1684 :: SBool = s1198 & s1683 + s1685 :: SBool = s1037 & s1684 + s1686 :: SBool = s876 & s1685 + s1687 :: SBool = s715 & s1686 + s1688 :: SBool = s554 & s1687 + s1689 :: SBool = s394 & s1688 + s1690 :: SBool = s234 & s1689 +OUTPUTS + s1690 diff --git a/SBVUnitTest/GoldFiles/fib1.gold b/SBVUnitTest/GoldFiles/fib1.gold --- a/SBVUnitTest/GoldFiles/fib1.gold +++ b/SBVUnitTest/GoldFiles/fib1.gold @@ -44,7 +44,7 @@ typedef int64_t SInt64; /* Entry point prototype: */ -SWord32 fib1(const SWord32 n); +SWord64 fib1(const SWord64 n); #endif /* __fib1__HEADER_INCLUDED__ */ == END: "fib1.h" ================== @@ -59,9 +59,9 @@ int main(void) { - const SWord32 __result = fib1(0x0000000cUL); + const SWord64 __result = fib1(0x000000000000000cULL); - printf("fib1(0x0000000cUL) = 0x%08"PRIx32"UL\n", __result); + printf("fib1(0x000000000000000cULL) = 0x%016"PRIx64"ULL\n", __result); return 0; } @@ -73,137 +73,137 @@ #include #include "fib1.h" -SWord32 fib1(const SWord32 n) +SWord64 fib1(const SWord64 n) { - const SWord32 s0 = n; - const SBool s2 = s0 == 0x00000000UL; - const SBool s4 = s0 == 0x00000001UL; - const SBool s6 = s0 == 0x00000002UL; - const SBool s8 = s0 == 0x00000003UL; - const SBool s10 = s0 == 0x00000004UL; - const SBool s12 = s0 == 0x00000005UL; - const SBool s14 = s0 == 0x00000006UL; - const SBool s17 = s0 == 0x00000007UL; - const SBool s19 = s0 == 0x00000008UL; - const SBool s22 = s0 == 0x00000009UL; - const SBool s25 = s0 == 0x0000000aUL; - const SBool s28 = s0 == 0x0000000bUL; - const SBool s31 = s0 == 0x0000000cUL; - const SBool s33 = s0 == 0x0000000dUL; - const SBool s36 = s0 == 0x0000000eUL; - const SBool s39 = s0 == 0x0000000fUL; - const SBool s42 = s0 == 0x00000010UL; - const SBool s45 = s0 == 0x00000011UL; - const SBool s48 = s0 == 0x00000012UL; - const SBool s51 = s0 == 0x00000013UL; - const SBool s54 = s0 == 0x00000014UL; - const SBool s56 = s0 == 0x00000015UL; - const SBool s59 = s0 == 0x00000016UL; - const SBool s62 = s0 == 0x00000017UL; - const SBool s65 = s0 == 0x00000018UL; - const SBool s68 = s0 == 0x00000019UL; - const SBool s71 = s0 == 0x0000001aUL; - const SBool s74 = s0 == 0x0000001bUL; - const SBool s77 = s0 == 0x0000001cUL; - const SBool s80 = s0 == 0x0000001dUL; - const SBool s83 = s0 == 0x0000001eUL; - const SBool s86 = s0 == 0x0000001fUL; - const SBool s89 = s0 == 0x00000020UL; - const SBool s92 = s0 == 0x00000021UL; - const SBool s94 = s0 == 0x00000022UL; - const SBool s97 = s0 == 0x00000023UL; - const SBool s100 = s0 == 0x00000024UL; - const SBool s103 = s0 == 0x00000025UL; - const SBool s106 = s0 == 0x00000026UL; - const SBool s109 = s0 == 0x00000027UL; - const SBool s112 = s0 == 0x00000028UL; - const SBool s115 = s0 == 0x00000029UL; - const SBool s118 = s0 == 0x0000002aUL; - const SBool s121 = s0 == 0x0000002bUL; - const SBool s124 = s0 == 0x0000002cUL; - const SBool s127 = s0 == 0x0000002dUL; - const SBool s130 = s0 == 0x0000002eUL; - const SBool s133 = s0 == 0x0000002fUL; - const SBool s136 = s0 == 0x00000030UL; - const SBool s139 = s0 == 0x00000031UL; - const SBool s142 = s0 == 0x00000032UL; - const SBool s145 = s0 == 0x00000033UL; - const SBool s148 = s0 == 0x00000034UL; - const SBool s151 = s0 == 0x00000035UL; - const SBool s154 = s0 == 0x00000036UL; - const SBool s156 = s0 == 0x00000037UL; - const SBool s159 = s0 == 0x00000038UL; - const SBool s162 = s0 == 0x00000039UL; - const SBool s165 = s0 == 0x0000003aUL; - const SBool s168 = s0 == 0x0000003bUL; - const SBool s171 = s0 == 0x0000003cUL; - const SBool s174 = s0 == 0x0000003dUL; - const SBool s177 = s0 == 0x0000003eUL; - const SBool s180 = s0 == 0x0000003fUL; - const SWord32 s183 = s180 ? 0xc7b064e2UL : 0x61ca20bbUL; - const SWord32 s184 = s177 ? 0x9a19bbd9UL : s183; - const SWord32 s185 = s174 ? 0x2d96a909UL : s184; - const SWord32 s186 = s171 ? 0x6c8312d0UL : s185; - const SWord32 s187 = s168 ? 0xc1139639UL : s186; - const SWord32 s188 = s165 ? 0xab6f7c97UL : s187; - const SWord32 s189 = s162 ? 0x15a419a2UL : s188; - const SWord32 s190 = s159 ? 0x95cb62f5UL : s189; - const SWord32 s191 = s156 ? 0x7fd8b6adUL : s190; - const SWord32 s192 = s154 ? 0x15f2ac48UL : s191; - const SWord32 s193 = s151 ? 0x69e60a65UL : s192; - const SWord32 s194 = s148 ? 0xac0ca1e3UL : s193; - const SWord32 s195 = s145 ? 0xbdd96882UL : s194; - const SWord32 s196 = s142 ? 0xee333961UL : s195; - const SWord32 s197 = s139 ? 0xcfa62f21UL : s196; - const SWord32 s198 = s136 ? 0x1e8d0a40UL : s197; - const SWord32 s199 = s133 ? 0xb11924e1UL : s198; - const SWord32 s200 = s130 ? 0x6d73e55fUL : s199; - const SWord32 s201 = s127 ? 0x43a53f82UL : s200; - const SWord32 s202 = s124 ? 0x29cea5ddUL : s201; - const SWord32 s203 = s121 ? 0x19d699a5UL : s202; - const SWord32 s204 = s118 ? 0x0ff80c38UL : s203; - const SWord32 s205 = s115 ? 0x09de8d6dUL : s204; - const SWord32 s206 = s112 ? 0x06197ecbUL : s205; - const SWord32 s207 = s109 ? 0x03c50ea2UL : s206; - const SWord32 s208 = s106 ? 0x02547029UL : s207; - const SWord32 s209 = s103 ? 0x01709e79UL : s208; - const SWord32 s210 = s100 ? 0x00e3d1b0UL : s209; - const SWord32 s211 = s97 ? 0x008cccc9UL : s210; - const SWord32 s212 = s94 ? 0x005704e7UL : s211; - const SWord32 s213 = s92 ? 0x0035c7e2UL : s212; - const SWord32 s214 = s89 ? 0x00213d05UL : s213; - const SWord32 s215 = s86 ? 0x00148addUL : s214; - const SWord32 s216 = s83 ? 0x000cb228UL : s215; - const SWord32 s217 = s80 ? 0x0007d8b5UL : s216; - const SWord32 s218 = s77 ? 0x0004d973UL : s217; - const SWord32 s219 = s74 ? 0x0002ff42UL : s218; - const SWord32 s220 = s71 ? 0x0001da31UL : s219; - const SWord32 s221 = s68 ? 0x00012511UL : s220; - const SWord32 s222 = s65 ? 0x0000b520UL : s221; - const SWord32 s223 = s62 ? 0x00006ff1UL : s222; - const SWord32 s224 = s59 ? 0x0000452fUL : s223; - const SWord32 s225 = s56 ? 0x00002ac2UL : s224; - const SWord32 s226 = s54 ? 0x00001a6dUL : s225; - const SWord32 s227 = s51 ? 0x00001055UL : s226; - const SWord32 s228 = s48 ? 0x00000a18UL : s227; - const SWord32 s229 = s45 ? 0x0000063dUL : s228; - const SWord32 s230 = s42 ? 0x000003dbUL : s229; - const SWord32 s231 = s39 ? 0x00000262UL : s230; - const SWord32 s232 = s36 ? 0x00000179UL : s231; - const SWord32 s233 = s33 ? 0x000000e9UL : s232; - const SWord32 s234 = s31 ? 0x00000090UL : s233; - const SWord32 s235 = s28 ? 0x00000059UL : s234; - const SWord32 s236 = s25 ? 0x00000037UL : s235; - const SWord32 s237 = s22 ? 0x00000022UL : s236; - const SWord32 s238 = s19 ? 0x00000015UL : s237; - const SWord32 s239 = s17 ? 0x0000000dUL : s238; - const SWord32 s240 = s14 ? 0x00000008UL : s239; - const SWord32 s241 = s12 ? 0x00000005UL : s240; - const SWord32 s242 = s10 ? 0x00000003UL : s241; - const SWord32 s243 = s8 ? 0x00000002UL : s242; - const SWord32 s244 = s6 ? 0x00000001UL : s243; - const SWord32 s245 = s4 ? 0x00000001UL : s244; - const SWord32 s246 = s2 ? 0x00000000UL : s245; + const SWord64 s0 = n; + 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 SBool s25 = s0 == 0x000000000000000aULL; + const SBool s28 = s0 == 0x000000000000000bULL; + const SBool s31 = s0 == 0x000000000000000cULL; + const SBool s33 = s0 == 0x000000000000000dULL; + const SBool s36 = s0 == 0x000000000000000eULL; + const SBool s39 = s0 == 0x000000000000000fULL; + const SBool s42 = s0 == 0x0000000000000010ULL; + const SBool s45 = s0 == 0x0000000000000011ULL; + const SBool s48 = s0 == 0x0000000000000012ULL; + const SBool s51 = s0 == 0x0000000000000013ULL; + const SBool s54 = s0 == 0x0000000000000014ULL; + const SBool s56 = s0 == 0x0000000000000015ULL; + const SBool s59 = s0 == 0x0000000000000016ULL; + const SBool s62 = s0 == 0x0000000000000017ULL; + const SBool s65 = s0 == 0x0000000000000018ULL; + const SBool s68 = s0 == 0x0000000000000019ULL; + const SBool s71 = s0 == 0x000000000000001aULL; + const SBool s74 = s0 == 0x000000000000001bULL; + const SBool s77 = s0 == 0x000000000000001cULL; + const SBool s80 = s0 == 0x000000000000001dULL; + const SBool s83 = s0 == 0x000000000000001eULL; + const SBool s86 = s0 == 0x000000000000001fULL; + const SBool s89 = s0 == 0x0000000000000020ULL; + const SBool s92 = s0 == 0x0000000000000021ULL; + const SBool s94 = s0 == 0x0000000000000022ULL; + const SBool s97 = s0 == 0x0000000000000023ULL; + const SBool s100 = s0 == 0x0000000000000024ULL; + const SBool s103 = s0 == 0x0000000000000025ULL; + const SBool s106 = s0 == 0x0000000000000026ULL; + const SBool s109 = s0 == 0x0000000000000027ULL; + const SBool s112 = s0 == 0x0000000000000028ULL; + const SBool s115 = s0 == 0x0000000000000029ULL; + const SBool s118 = s0 == 0x000000000000002aULL; + const SBool s121 = s0 == 0x000000000000002bULL; + const SBool s124 = s0 == 0x000000000000002cULL; + const SBool s127 = s0 == 0x000000000000002dULL; + const SBool s130 = s0 == 0x000000000000002eULL; + const SBool s133 = s0 == 0x000000000000002fULL; + const SBool s136 = s0 == 0x0000000000000030ULL; + const SBool s139 = s0 == 0x0000000000000031ULL; + const SBool s142 = s0 == 0x0000000000000032ULL; + const SBool s145 = s0 == 0x0000000000000033ULL; + const SBool s148 = s0 == 0x0000000000000034ULL; + const SBool s151 = s0 == 0x0000000000000035ULL; + const SBool s154 = s0 == 0x0000000000000036ULL; + const SBool s156 = s0 == 0x0000000000000037ULL; + const SBool s159 = s0 == 0x0000000000000038ULL; + const SBool s162 = s0 == 0x0000000000000039ULL; + const SBool s165 = s0 == 0x000000000000003aULL; + const SBool s168 = s0 == 0x000000000000003bULL; + const SBool s171 = s0 == 0x000000000000003cULL; + const SBool s174 = s0 == 0x000000000000003dULL; + const SBool s177 = s0 == 0x000000000000003eULL; + const SBool s180 = s0 == 0x000000000000003fULL; + const SWord64 s183 = s180 ? 0x000005f6c7b064e2ULL : 0x000009a661ca20bbULL; + const SWord64 s184 = s177 ? 0x000003af9a19bbd9ULL : s183; + const SWord64 s185 = s174 ? 0x000002472d96a909ULL : s184; + const SWord64 s186 = s171 ? 0x000001686c8312d0ULL : s185; + const SWord64 s187 = s168 ? 0x000000dec1139639ULL : s186; + const SWord64 s188 = s165 ? 0x00000089ab6f7c97ULL : s187; + const SWord64 s189 = s162 ? 0x0000005515a419a2ULL : s188; + const SWord64 s190 = s159 ? 0x0000003495cb62f5ULL : s189; + const SWord64 s191 = s156 ? 0x000000207fd8b6adULL : s190; + const SWord64 s192 = s154 ? 0x0000001415f2ac48ULL : s191; + const SWord64 s193 = s151 ? 0x0000000c69e60a65ULL : s192; + const SWord64 s194 = s148 ? 0x00000007ac0ca1e3ULL : s193; + const SWord64 s195 = s145 ? 0x00000004bdd96882ULL : s194; + const SWord64 s196 = s142 ? 0x00000002ee333961ULL : s195; + const SWord64 s197 = s139 ? 0x00000001cfa62f21ULL : s196; + const SWord64 s198 = s136 ? 0x000000011e8d0a40ULL : s197; + const SWord64 s199 = s133 ? 0x00000000b11924e1ULL : s198; + const SWord64 s200 = s130 ? 0x000000006d73e55fULL : s199; + const SWord64 s201 = s127 ? 0x0000000043a53f82ULL : s200; + const SWord64 s202 = s124 ? 0x0000000029cea5ddULL : s201; + const SWord64 s203 = s121 ? 0x0000000019d699a5ULL : s202; + const SWord64 s204 = s118 ? 0x000000000ff80c38ULL : s203; + const SWord64 s205 = s115 ? 0x0000000009de8d6dULL : s204; + const SWord64 s206 = s112 ? 0x0000000006197ecbULL : s205; + const SWord64 s207 = s109 ? 0x0000000003c50ea2ULL : s206; + const SWord64 s208 = s106 ? 0x0000000002547029ULL : s207; + const SWord64 s209 = s103 ? 0x0000000001709e79ULL : s208; + const SWord64 s210 = s100 ? 0x0000000000e3d1b0ULL : s209; + const SWord64 s211 = s97 ? 0x00000000008cccc9ULL : s210; + const SWord64 s212 = s94 ? 0x00000000005704e7ULL : s211; + const SWord64 s213 = s92 ? 0x000000000035c7e2ULL : s212; + const SWord64 s214 = s89 ? 0x0000000000213d05ULL : s213; + const SWord64 s215 = s86 ? 0x0000000000148addULL : s214; + const SWord64 s216 = s83 ? 0x00000000000cb228ULL : s215; + const SWord64 s217 = s80 ? 0x000000000007d8b5ULL : s216; + const SWord64 s218 = s77 ? 0x000000000004d973ULL : s217; + const SWord64 s219 = s74 ? 0x000000000002ff42ULL : s218; + const SWord64 s220 = s71 ? 0x000000000001da31ULL : s219; + const SWord64 s221 = s68 ? 0x0000000000012511ULL : s220; + const SWord64 s222 = s65 ? 0x000000000000b520ULL : s221; + const SWord64 s223 = s62 ? 0x0000000000006ff1ULL : s222; + const SWord64 s224 = s59 ? 0x000000000000452fULL : s223; + const SWord64 s225 = s56 ? 0x0000000000002ac2ULL : s224; + const SWord64 s226 = s54 ? 0x0000000000001a6dULL : s225; + const SWord64 s227 = s51 ? 0x0000000000001055ULL : s226; + const SWord64 s228 = s48 ? 0x0000000000000a18ULL : s227; + const SWord64 s229 = s45 ? 0x000000000000063dULL : s228; + const SWord64 s230 = s42 ? 0x00000000000003dbULL : s229; + const SWord64 s231 = s39 ? 0x0000000000000262ULL : s230; + const SWord64 s232 = s36 ? 0x0000000000000179ULL : s231; + const SWord64 s233 = s33 ? 0x00000000000000e9ULL : s232; + const SWord64 s234 = s31 ? 0x0000000000000090ULL : s233; + const SWord64 s235 = s28 ? 0x0000000000000059ULL : s234; + const SWord64 s236 = s25 ? 0x0000000000000037ULL : s235; + const SWord64 s237 = s22 ? 0x0000000000000022ULL : s236; + const SWord64 s238 = s19 ? 0x0000000000000015ULL : s237; + const SWord64 s239 = s17 ? 0x000000000000000dULL : s238; + const SWord64 s240 = s14 ? 0x0000000000000008ULL : s239; + const SWord64 s241 = s12 ? 0x0000000000000005ULL : s240; + const SWord64 s242 = s10 ? 0x0000000000000003ULL : s241; + const SWord64 s243 = s8 ? 0x0000000000000002ULL : s242; + const SWord64 s244 = s6 ? 0x0000000000000001ULL : s243; + const SWord64 s245 = s4 ? 0x0000000000000001ULL : s244; + const SWord64 s246 = s2 ? 0x0000000000000000ULL : s245; return s246; } diff --git a/SBVUnitTest/GoldFiles/fib2.gold b/SBVUnitTest/GoldFiles/fib2.gold --- a/SBVUnitTest/GoldFiles/fib2.gold +++ b/SBVUnitTest/GoldFiles/fib2.gold @@ -44,7 +44,7 @@ typedef int64_t SInt64; /* Entry point prototype: */ -SWord32 fib2(const SWord32 n); +SWord64 fib2(const SWord64 n); #endif /* __fib2__HEADER_INCLUDED__ */ == END: "fib2.h" ================== @@ -59,9 +59,9 @@ int main(void) { - const SWord32 __result = fib2(0x00000014UL); + const SWord64 __result = fib2(0x0000000000000014ULL); - printf("fib2(0x00000014UL) = 0x%08"PRIx32"UL\n", __result); + printf("fib2(0x0000000000000014ULL) = 0x%016"PRIx64"ULL\n", __result); return 0; } @@ -73,29 +73,44 @@ #include #include "fib2.h" -SWord32 fib2(const SWord32 n) +SWord64 fib2(const SWord64 n) { - const SWord32 s0 = n; - static const SWord32 table0[] = { - 0x00000000UL, 0x00000001UL, 0x00000001UL, 0x00000002UL, - 0x00000003UL, 0x00000005UL, 0x00000008UL, 0x0000000dUL, - 0x00000015UL, 0x00000022UL, 0x00000037UL, 0x00000059UL, - 0x00000090UL, 0x000000e9UL, 0x00000179UL, 0x00000262UL, - 0x000003dbUL, 0x0000063dUL, 0x00000a18UL, 0x00001055UL, - 0x00001a6dUL, 0x00002ac2UL, 0x0000452fUL, 0x00006ff1UL, - 0x0000b520UL, 0x00012511UL, 0x0001da31UL, 0x0002ff42UL, - 0x0004d973UL, 0x0007d8b5UL, 0x000cb228UL, 0x00148addUL, - 0x00213d05UL, 0x0035c7e2UL, 0x005704e7UL, 0x008cccc9UL, - 0x00e3d1b0UL, 0x01709e79UL, 0x02547029UL, 0x03c50ea2UL, - 0x06197ecbUL, 0x09de8d6dUL, 0x0ff80c38UL, 0x19d699a5UL, - 0x29cea5ddUL, 0x43a53f82UL, 0x6d73e55fUL, 0xb11924e1UL, - 0x1e8d0a40UL, 0xcfa62f21UL, 0xee333961UL, 0xbdd96882UL, - 0xac0ca1e3UL, 0x69e60a65UL, 0x15f2ac48UL, 0x7fd8b6adUL, - 0x95cb62f5UL, 0x15a419a2UL, 0xab6f7c97UL, 0xc1139639UL, - 0x6c8312d0UL, 0x2d96a909UL, 0x9a19bbd9UL, 0xc7b064e2UL, - 0x61ca20bbUL + const SWord64 s0 = n; + 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 SWord32 s65 = s0 >= 65 ? 0x00000000UL : table0[s0]; + const SWord64 s65 = s0 >= 65 ? 0x0000000000000000ULL : table0[s0]; return s65; } diff --git a/SBVUnitTest/SBVUnitTest.hs b/SBVUnitTest/SBVUnitTest.hs --- a/SBVUnitTest/SBVUnitTest.hs +++ b/SBVUnitTest/SBVUnitTest.hs @@ -34,6 +34,7 @@ import qualified Data.SBV.TestSuite.Basics.QRem as T02_06(testSuite) import qualified Data.SBV.TestSuite.BitPrecise.BitTricks as T03_01(testSuite) import qualified Data.SBV.TestSuite.BitPrecise.Legato as T03_02(testSuite) +import qualified Data.SBV.TestSuite.BitPrecise.PrefixSum as T03_03(testSuite) import qualified Data.SBV.TestSuite.CRC.CCITT as T04_01(testSuite) import qualified Data.SBV.TestSuite.CRC.CCITT_Unidir as T04_02(testSuite) import qualified Data.SBV.TestSuite.CRC.GenPoly as T04_03(testSuite) @@ -45,19 +46,20 @@ import qualified Data.SBV.TestSuite.CodeGeneration.GCD as T05_04(testSuite) import qualified Data.SBV.TestSuite.CodeGeneration.PopulationCount as T05_05(testSuite) import qualified Data.SBV.TestSuite.Crypto.AES as T06_01(testSuite) +import qualified Data.SBV.TestSuite.Crypto.RC4 as T06_02(testSuite) import qualified Data.SBV.TestSuite.Polynomials.Polynomials as T07_01(testSuite) -import qualified Data.SBV.TestSuite.PrefixSum.PrefixSum as T08_01(testSuite) -import qualified Data.SBV.TestSuite.Puzzles.DogCatMouse as T09_01(testSuite) -import qualified Data.SBV.TestSuite.Puzzles.Euler185 as T09_02(testSuite) -import qualified Data.SBV.TestSuite.Puzzles.MagicSquare as T09_03(testSuite) -import qualified Data.SBV.TestSuite.Puzzles.NQueens as T09_04(testSuite) -import qualified Data.SBV.TestSuite.Puzzles.PowerSet as T09_05(testSuite) -import qualified Data.SBV.TestSuite.Puzzles.Sudoku as T09_06(testSuite) -import qualified Data.SBV.TestSuite.Puzzles.Temperature as T09_07(testSuite) -import qualified Data.SBV.TestSuite.Puzzles.U2Bridge as T09_08(testSuite) -import qualified Data.SBV.TestSuite.Uninterpreted.AUF as T10_01(testSuite) -import qualified Data.SBV.TestSuite.Uninterpreted.Function as T10_02(testSuite) -import qualified Data.SBV.TestSuite.Uninterpreted.Uninterpreted as T10_03(testSuite) +import qualified Data.SBV.TestSuite.Puzzles.Counts as T08_01(testSuite) +import qualified Data.SBV.TestSuite.Puzzles.DogCatMouse as T08_02(testSuite) +import qualified Data.SBV.TestSuite.Puzzles.Euler185 as T08_03(testSuite) +import qualified Data.SBV.TestSuite.Puzzles.MagicSquare as T08_04(testSuite) +import qualified Data.SBV.TestSuite.Puzzles.NQueens as T08_05(testSuite) +import qualified Data.SBV.TestSuite.Puzzles.PowerSet as T08_06(testSuite) +import qualified Data.SBV.TestSuite.Puzzles.Sudoku as T08_07(testSuite) +import qualified Data.SBV.TestSuite.Puzzles.Temperature as T08_08(testSuite) +import qualified Data.SBV.TestSuite.Puzzles.U2Bridge as T08_09(testSuite) +import qualified Data.SBV.TestSuite.Uninterpreted.AUF as T09_01(testSuite) +import qualified Data.SBV.TestSuite.Uninterpreted.Function as T09_02(testSuite) +import qualified Data.SBV.TestSuite.Uninterpreted.Uninterpreted as T09_03(testSuite) testCollection :: [(String, SBVTestSuite)] testCollection = [ @@ -70,6 +72,7 @@ , ("qrem", T02_06.testSuite) , ("bitTricks", T03_01.testSuite) , ("legato", T03_02.testSuite) + , ("prefixSum", T03_03.testSuite) , ("ccitt", T04_01.testSuite) , ("ccitt2", T04_02.testSuite) , ("genPoly", T04_03.testSuite) @@ -81,19 +84,20 @@ , ("gcd", T05_04.testSuite) , ("popCount", T05_05.testSuite) , ("aes", T06_01.testSuite) + , ("rc4", T06_02.testSuite) , ("poly", T07_01.testSuite) - , ("prefixSum", T08_01.testSuite) - , ("dogCatMouse", T09_01.testSuite) - , ("euler185", T09_02.testSuite) - , ("magicSquare", T09_03.testSuite) - , ("nQueens", T09_04.testSuite) - , ("powerset", T09_05.testSuite) - , ("sudoku", T09_06.testSuite) - , ("temperature", T09_07.testSuite) - , ("u2bridge", T09_08.testSuite) - , ("auf1", T10_01.testSuite) - , ("auf2", T10_02.testSuite) - , ("unint", T10_03.testSuite) + , ("counts", T08_01.testSuite) + , ("dogCatMouse", T08_02.testSuite) + , ("euler185", T08_03.testSuite) + , ("magicSquare", T08_04.testSuite) + , ("nQueens", T08_05.testSuite) + , ("powerset", T08_06.testSuite) + , ("sudoku", T08_07.testSuite) + , ("temperature", T08_08.testSuite) + , ("u2bridge", T08_09.testSuite) + , ("auf1", T09_01.testSuite) + , ("auf2", T09_02.testSuite) + , ("unint", T09_03.testSuite) ] -- No user serviceable parts below.. diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,7 +1,7 @@ Name: sbv -Version: 0.9.18 +Version: 0.9.19 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math -Synopsis: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers. +Synopsis: Symbolic bit vectors: Bit-precise verification and automatic C-code generation. Description: 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 @@ -25,6 +25,8 @@ . * '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 @@ -40,8 +42,7 @@ * quick-checked . The SBV library can also compile Haskell functions that manipulate symbolic - values directly to C, rendering them as straight-line C programs that can be - executed in, say, embedded platforms. + 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, @@ -53,7 +54,7 @@ Galois, Inc. () has contributed to the development of SBV, by providing time and computing machinery. The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways: - Ian Blumenfeld, Iavor Diatchki, Lee Pike, Austin Seipp, Don Stewart, and Josef Svenningsson. + Ian Blumenfeld, Ian Calvert, Iavor Diatchki, Lee Pike, Austin Seipp, Don Stewart, and Josef Svenningsson. Copyright: Levent Erkok, 2010-2011 License: BSD3 @@ -93,13 +94,15 @@ , Data.SBV.Internals , Data.SBV.Examples.BitPrecise.BitTricks , Data.SBV.Examples.BitPrecise.Legato + , Data.SBV.Examples.BitPrecise.PrefixSum , Data.SBV.Examples.CodeGeneration.AddSub , Data.SBV.Examples.CodeGeneration.Fibonacci , Data.SBV.Examples.CodeGeneration.GCD , Data.SBV.Examples.CodeGeneration.PopulationCount , Data.SBV.Examples.Crypto.AES + , Data.SBV.Examples.Crypto.RC4 , Data.SBV.Examples.Polynomials.Polynomials - , Data.SBV.Examples.PrefixSum.PrefixSum + , Data.SBV.Examples.Puzzles.Counts , Data.SBV.Examples.Puzzles.DogCatMouse , Data.SBV.Examples.Puzzles.Euler185 , Data.SBV.Examples.Puzzles.MagicSquare @@ -110,9 +113,11 @@ , Data.SBV.Examples.Uninterpreted.Function Other-modules : Data.SBV.BitVectors.Data , Data.SBV.BitVectors.Model - , Data.SBV.BitVectors.Splittable , Data.SBV.BitVectors.Polynomial , Data.SBV.BitVectors.PrettyNum + , Data.SBV.BitVectors.SignCast + , Data.SBV.BitVectors.Splittable + , Data.SBV.BitVectors.STree , Data.SBV.Compilers.C , Data.SBV.Compilers.CodeGen , Data.SBV.SMT.SMT @@ -147,18 +152,19 @@ , Data.SBV.TestSuite.Basics.QRem , Data.SBV.TestSuite.BitPrecise.BitTricks , Data.SBV.TestSuite.BitPrecise.Legato + , Data.SBV.TestSuite.BitPrecise.PrefixSum , Data.SBV.TestSuite.CodeGeneration.AddSub , Data.SBV.TestSuite.CodeGeneration.CgTests , Data.SBV.TestSuite.CodeGeneration.Fibonacci , Data.SBV.TestSuite.CodeGeneration.GCD , Data.SBV.TestSuite.CodeGeneration.PopulationCount , Data.SBV.TestSuite.Crypto.AES + , Data.SBV.TestSuite.Crypto.RC4 , Data.SBV.TestSuite.CRC.CCITT , Data.SBV.TestSuite.CRC.CCITT_Unidir , Data.SBV.TestSuite.CRC.GenPoly , Data.SBV.TestSuite.CRC.Parity , Data.SBV.TestSuite.CRC.USB5 - , Data.SBV.TestSuite.PrefixSum.PrefixSum , Data.SBV.TestSuite.Polynomials.Polynomials , Data.SBV.TestSuite.Puzzles.DogCatMouse , Data.SBV.TestSuite.Puzzles.Euler185