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.

The tie operator, concatenation.

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

Inverse of zipping.

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

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.

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.

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

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 ran out of memory and crashed on my box when I tried for size 8, after running for about 2.5 minutes..

Old version of Yices that supports quantified axioms in SMT-Lib1

Another old version of yices, suitable for the non-axiom based problem

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

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