sbv 0.9.18 → 0.9.19
raw patch · 29 files changed
+2828/−603 lines, 29 files
Files
- Data/SBV.hs +6/−0
- Data/SBV/BitVectors/Data.hs +7/−4
- Data/SBV/BitVectors/Model.hs +2/−2
- Data/SBV/BitVectors/STree.hs +70/−0
- Data/SBV/BitVectors/SignCast.hs +111/−0
- Data/SBV/BitVectors/Splittable.hs +2/−2
- Data/SBV/Compilers/C.hs +10/−1
- Data/SBV/Examples/BitPrecise/Legato.hs +1/−1
- Data/SBV/Examples/BitPrecise/PrefixSum.hs +304/−0
- Data/SBV/Examples/CodeGeneration/Fibonacci.hs +69/−51
- Data/SBV/Examples/Crypto/AES.hs +1/−1
- Data/SBV/Examples/Crypto/RC4.hs +145/−0
- Data/SBV/Examples/PrefixSum/PrefixSum.hs +0/−304
- Data/SBV/Examples/Puzzles/Counts.hs +84/−0
- Data/SBV/Internals.hs +2/−2
- Data/SBV/Provers/Prover.hs +7/−1
- Data/SBV/TestSuite/Basics/Arithmetic.hs +35/−12
- Data/SBV/TestSuite/BitPrecise/Legato.hs +1/−1
- Data/SBV/TestSuite/BitPrecise/PrefixSum.hs +25/−0
- Data/SBV/TestSuite/Crypto/AES.hs +1/−1
- Data/SBV/TestSuite/Crypto/RC4.hs +24/−0
- Data/SBV/TestSuite/PrefixSum/PrefixSum.hs +0/−25
- README +2/−3
- SBVUnitTest/GoldFiles/aes128Lib.gold +3/−3
- SBVUnitTest/GoldFiles/counts.gold +1702/−0
- SBVUnitTest/GoldFiles/fib1.gold +133/−133
- SBVUnitTest/GoldFiles/fib2.gold +39/−24
- SBVUnitTest/SBVUnitTest.hs +28/−24
- sbv.cabal +14/−8
Data/SBV.hs view
@@ -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
Data/SBV/BitVectors/Data.hs view
@@ -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
Data/SBV/BitVectors/Model.hs view
@@ -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
+ Data/SBV/BitVectors/STree.hs view
@@ -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)
+ Data/SBV/BitVectors/SignCast.hs view
@@ -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
Data/SBV/BitVectors/Splittable.hs view
@@ -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
Data/SBV/Compilers/C.hs view
@@ -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 ""
Data/SBV/Examples/BitPrecise/Legato.hs view
@@ -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
+ Data/SBV/Examples/BitPrecise/PrefixSum.hs view
@@ -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 <http://www.cs.utexas.edu/users/psp/powerlist.pdf>+-- and <http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf>.+-----------------------------------------------------------------------------++{-# 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: <http://www.cs.utexas.edu/users/psp/powerlist.pdf>.+-- We merely represent power-lists by ordinary lists.+type PowerList a = [a]++-- | The tie operator, concatenation.+tiePL :: PowerList a -> PowerList a -> PowerList a+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 <http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf>+-- or pg. 16 of <http://www.cs.utexas.edu/users/psp/powerlist.pdf>.+lf :: (a, a -> a -> a) -> PowerList a -> PowerList a+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: <http://goedel.cs.uiowa.edu/smtlib/logics.html>. So we+-- are stuck until new powerful logics are added to SMT-Lib.+--+-- Here, we explicitly tell SBV to use Yices-1 that did not have that limitation.+-- Tweak the executable location accordingly below for your platform..+--+-- We have:+--+-- >>> prefixSum 2+-- Q.E.D.+--+-- >>> prefixSum 4+-- Q.E.D.+--+-- Note that these proofs tend to run long. Also, Yices ran out of memory+-- and crashed on my box when I tried for size @8@, after running for about 2.5 minutes..+prefixSum :: Int -> IO ThmResult+prefixSum i+ -- Fast way of checking whether a number is a power of two, see: <http://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2>+ | 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
Data/SBV/Examples/CodeGeneration/Fibonacci.hs view
@@ -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"
Data/SBV/Examples/Crypto/AES.hs view
@@ -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
+ Data/SBV/Examples/Crypto/RC4.hs view
@@ -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: <http://en.wikipedia.org/wiki/RC4>.+--+-- We make no effort to optimize the code, and instead focus on a clear+-- implementation. In fact, the RC4 algorithm relies on in-place update of+-- its state heavily for efficiency, and is therefore unsuitable for a purely+-- functional implementation.+-----------------------------------------------------------------------------++{-# 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 <http://en.wikipedia.org/wiki/RC4>:+--+-- >>> concatMap hex $ encrypt "Key" "Plaintext"+-- "bbf316e8d940af0ad3"+--+-- >>> concatMap hex $ encrypt "Wiki" "pedia"+-- "1021bf0420"+--+-- >>> concatMap hex $ encrypt "Secret" "Attack at dawn"+-- "45a01f645fc35b383552544b9bf5"+encrypt :: String -> String -> [SWord8]+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'
− Data/SBV/Examples/PrefixSum/PrefixSum.hs
@@ -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 <http://www.cs.utexas.edu/users/psp/powerlist.pdf>--- and <http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf>.--------------------------------------------------------------------------------{-# 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: <http://www.cs.utexas.edu/users/psp/powerlist.pdf>.--- We merely represent power-lists by ordinary lists.-type PowerList a = [a]---- | The tie operator, concatenation-tiePL :: PowerList a -> PowerList a -> PowerList a-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 <http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf>--- or pg. 16 of <http://www.cs.utexas.edu/users/psp/powerlist.pdf>.-lf :: (a, a -> a -> a) -> PowerList a -> PowerList a-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: <http://goedel.cs.uiowa.edu/smtlib/logics.html>. So we--- are stuck until new powerful logics are added to SMT-Lib.------ Here, we explicitly tell SBV to use Yices-1 that did not have that limitation.--- Tweak the executable location accordingly below for your platform..------ We have:------ >>> prefixSum 2--- Q.E.D.------ >>> prefixSum 4--- Q.E.D.------ Note that these proofs tend to run long. Also, Yices-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: <http://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2>- | 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
+ Data/SBV/Examples/Puzzles/Counts.hs view
@@ -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.+--+-- * <http://www.lboro.ac.uk/departments/ma/gallery/selfref/index.html>+--+-----------------------------------------------------------------------------++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)+ ++ "."
Data/SBV/Internals.hs view
@@ -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(..))
Data/SBV/Provers/Prover.hs view
@@ -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
Data/SBV/TestSuite/Basics/Arithmetic.hs view
@@ -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]
Data/SBV/TestSuite/BitPrecise/Legato.hs view
@@ -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
+ Data/SBV/TestSuite/BitPrecise/PrefixSum.hs view
@@ -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"+ ]
Data/SBV/TestSuite/Crypto/AES.hs view
@@ -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
+ Data/SBV/TestSuite/Crypto/RC4.hs view
@@ -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
− Data/SBV/TestSuite/PrefixSum/PrefixSum.hs
@@ -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"- ]
README view
@@ -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.
SBVUnitTest/GoldFiles/aes128Lib.gold view
@@ -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:
+ SBVUnitTest/GoldFiles/counts.gold view
@@ -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
SBVUnitTest/GoldFiles/fib1.gold view
@@ -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 <stdint.h> #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; }
SBVUnitTest/GoldFiles/fib2.gold view
@@ -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 <stdint.h> #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; }
SBVUnitTest/SBVUnitTest.hs view
@@ -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..
sbv.cabal view
@@ -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. (<http://www.galois.com>) 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