sbv-0.9.15: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.

Portability portable experimental erkokl@gmail.com

Data.SBV.Examples.PrefixSum.PrefixSum

Description

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.

Synopsis

Formalizing power-lists

type PowerList a = [a]Source

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.

tiePL :: PowerList a -> PowerList a -> PowerList aSource

The tie operator, concatenation

zipPL :: PowerList a -> PowerList a -> PowerList aSource

The zip operator, zips the power-lists of the same size, returns a powerlist of double the size.

unzipPL :: PowerList a -> (PowerList a, PowerList a)Source

Inverse of zipping

Reference prefix-sum implementation

ps :: (a, a -> a -> a) -> PowerList a -> PowerList aSource

Reference prefix sum (ps) is simply Haskell's scanl1 function

The Ladner-Fischer parallel version

lf :: (a, a -> a -> a) -> PowerList a -> PowerList aSource

Sample proofs for concrete operators

flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Bits a) => (a, a -> a -> a)) -> Symbolic SBoolSource

Correctness theorem, for a powerlist of given size, an associative operator, and its left-unit element

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.

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.

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.

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.

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..

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:

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

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