----------------------------------------------------------------------------- -- | -- Module : Documentation.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 Documentation.SBV.Examples.BitPrecise.PrefixSum where import Data.SBV ---------------------------------------------------------------------- -- * 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@. We have: -- -- >>> thm1 -- Q.E.D. 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@. We have: -- -- >>> thm2 -- Q.E.D. thm2 :: IO ThmResult thm2 = prove \$ flIsCorrect 16 (0, smax)