----------------------------------------------------------------------------- -- | -- Module : Data.SBV.Examples.BitPrecise.PrefixSum -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer : erkokl@gmail.com -- Stability : experimental -- -- The PrefixSum algorithm over power-lists and proof of -- the Ladner-Fischer implementation. -- See -- and . ----------------------------------------------------------------------------- {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} module Data.SBV.Examples.BitPrecise.PrefixSum where import Data.SBV import qualified Data.SBV.Provers.Yices as Yices import Data.SBV.Internals(runSymbolic) ---------------------------------------------------------------------- -- * Formalizing power-lists ---------------------------------------------------------------------- -- | A poor man's representation of powerlists and -- basic operations on them: . -- We merely represent power-lists by ordinary lists. type PowerList a = [a] -- | The tie operator, concatenation. tiePL :: PowerList a -> PowerList a -> PowerList a tiePL = (++) -- | The zip operator, zips the power-lists of the same size, returns -- a powerlist of double the size. zipPL :: PowerList a -> PowerList a -> PowerList a zipPL [] [] = [] zipPL (x:xs) (y:ys) = x : y : zipPL xs ys zipPL _ _ = error "zipPL: nonsimilar powerlists received" -- | Inverse of zipping. unzipPL :: PowerList a -> (PowerList a, PowerList a) unzipPL = unzip . chunk2 where chunk2 [] = [] chunk2 (x:y:xs) = (x,y) : chunk2 xs chunk2 _ = error "unzipPL: malformed powerlist" ---------------------------------------------------------------------- -- * Reference prefix-sum implementation ---------------------------------------------------------------------- -- | Reference prefix sum (@ps@) is simply Haskell's @scanl1@ function. ps :: (a, a -> a -> a) -> PowerList a -> PowerList a ps (_, f) = scanl1 f ---------------------------------------------------------------------- -- * The Ladner-Fischer parallel version ---------------------------------------------------------------------- -- | The Ladner-Fischer (@lf@) implementation of prefix-sum. See -- or pg. 16 of . lf :: (a, a -> a -> a) -> PowerList a -> PowerList a lf _ [] = error "lf: malformed (empty) powerlist" lf _ [x] = [x] lf (zero, f) pl = zipPL (zipWith f (rsh lfpq) p) lfpq where (p, q) = unzipPL pl pq = zipWith f p q lfpq = lf (zero, f) pq rsh xs = zero : init xs ---------------------------------------------------------------------- -- * Sample proofs for concrete operators ---------------------------------------------------------------------- -- | Correctness theorem, for a powerlist of given size, an associative operator, and its left-unit element. flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Num a, Bits a) => (a, a -> a -> a)) -> Symbolic SBool flIsCorrect n zf = do args :: PowerList SWord32 <- mkForallVars 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 = 1073741824 :: SWord32 -- s5 = 0 :: SWord32 -- s6 = 0 :: SWord32 -- s7 = 0 :: SWord32 -- -- uninterpreted: u -- u = 0 -- -- uninterpreted: flOp -- flOp 0 0 = 2147483648 -- flOp 0 1073741824 = 3221225472 -- flOp 2147483648 0 = 3221225472 -- flOp 2147483648 1073741824 = 1073741824 -- flOp _ _ = 0 -- -- You can verify that the function @flOp@ is indeed not associative: -- -- @ -- ghci> flOp 3221225472 (flOp 2147483648 1073741824) -- 0 -- ghci> flOp (flOp 3221225472 2147483648) 1073741824 -- 3221225472 -- @ -- -- Also, the unit @0@ is clearly not a left-unit for @flOp@, as the last -- equation for @flOp@ will simply map many elements to @0@. -- (NB. We need to use yices for this proof as the uninterpreted function -- examples are only supported through the yices interface currently.) thm3 :: IO ThmResult thm3 = proveWith yicesSMT09 $ do args :: PowerList SWord32 <- mkForallVars 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 <- mkForallVars n addAxiom "flOp is associative" assocAxiom addAxiom "u is left-unit for flOp" leftUnitAxiom return $ ps (u, op) args .== lf (u, op) args where op :: SWord32 -> SWord32 -> SWord32 op = uninterpret "flOp" u :: SWord32 u = uninterpret "u" -- axioms.. These are a bit brittle. Note that we have to -- refer to the uninterpreted symbols with the prefix "uninterpreted_" when -- used with the SMTLib1 interface to avoid any collision. This is admittedly -- ugly, but it'll do till we get a sub-DSL for writing proper axioms (if ever) assocAxiom :: [String] assocAxiom = [ ":assumption (forall (?x BitVec[32]) (?y BitVec[32]) (?z BitVec[32])" , " (= (uninterpreted_flOp ?x (uninterpreted_flOp ?y ?z))" , " (uninterpreted_flOp (uninterpreted_flOp ?x ?y) ?z)" , " )" , " )" ] leftUnitAxiom :: [String] leftUnitAxiom = [ ":assumption (forall (?x BitVec[32]) (= (uninterpreted_flOp uninterpreted_u ?x) ?x))" ] -- | Prove the generic problem for powerlists of given sizes. Note that -- this will only work for Yices-1. This is due to the fact that Yices-2 -- follows the SMT-Lib standard and does not accept bit-vector problems with -- quantified axioms in them, while Yices-1 did allow for that. The crux of -- the problem is that there are no SMT-Lib logics that combine BV's and -- quantifiers, see: . So we -- are stuck until new powerful logics are added to SMT-Lib. -- -- Here, we explicitly tell SBV to use Yices-1 that did not have that limitation. -- Tweak the executable location accordingly below for your platform.. -- -- We have: -- -- >>> prefixSum 2 -- Q.E.D. -- -- >>> prefixSum 4 -- Q.E.D. -- -- Note that these proofs tend to run long. Also, Yices ran out of memory -- and crashed on my box when I tried for size @8@, after running for about 2.5 minutes.. prefixSum :: Int -> IO ThmResult prefixSum i -- Fast way of checking whether a number is a power of two, see: | i <= 1 || (i .&. (i-1)) /= 0 = error $ "prefixSum: input must be a power of 2 larger than 2, received: " ++ show i | True = proveWith yices1029 $ genPrefixSumInstance i -- | Old version of Yices that supports quantified axioms in SMT-Lib1 yices1029 :: SMTConfig yices1029 = yices {solver = yices'} where yices' = Yices.yices { options = ["-tc", "-smt", "-e"] , executable = "yices-1.0.29" } -- | Another old version of yices, suitable for the non-axiom based problem yicesSMT09 :: SMTConfig yicesSMT09 = yices {solver = yices'} where yices' = Yices.yices { options = ["-m"] , executable = "yices-SMT09" } ---------------------------------------------------------------------- -- * 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 -- USER GIVEN CODE SEGMENTS -- 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 -- CONSTRAINTS -- OUTPUTS -- s0 -- s8 -- s9 -- s11 -- s12 -- s14 -- s15 -- s18 ladnerFischerTrace :: Int -> IO () ladnerFischerTrace n = gen >>= print where gen = runSymbolic (True, Nothing) $ do args :: [SWord8] <- mkForallVars 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 -- USER GIVEN CODE SEGMENTS -- 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 -- CONSTRAINTS -- OUTPUTS -- s0 -- s8 -- s9 -- s10 -- s11 -- s12 -- s13 -- s14 -- scanlTrace :: Int -> IO () scanlTrace n = gen >>= print where gen = runSymbolic (True, Nothing) $ do args :: [SWord8] <- mkForallVars n mapM_ output $ ps (0, (+)) args {-# ANN module "HLint: ignore Reduce duplication" #-}