sbv-5.9: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Examples.BitPrecise.PrefixSum

Contents

- Formalizing power-lists
- Reference prefix-sum implementation
- The Ladner-Fischer parallel version
- Sample proofs for concrete operators
- Inspecting symbolic traces

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

- type PowerList a = [a]
- tiePL :: PowerList a -> PowerList a -> PowerList a
- zipPL :: PowerList a -> PowerList a -> PowerList a
- unzipPL :: PowerList a -> (PowerList a, PowerList a)
- ps :: (a, a -> a -> a) -> PowerList a -> PowerList a
- lf :: (a, a -> a -> a) -> PowerList a -> PowerList a
- flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Num a, Bits a) => (a, a -> a -> a)) -> Symbolic SBool
- thm1 :: IO ThmResult
- thm2 :: IO ThmResult
- ladnerFischerTrace :: Int -> IO ()
- scanlTrace :: Int -> IO ()

# 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 a Source

The tie operator, concatenation.

zipPL :: PowerList a -> PowerList a -> PowerList a Source

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 a Source

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

# The Ladner-Fischer parallel version

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

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.

# Sample proofs for concrete operators

flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Num a, Bits a) => (a, a -> a -> a)) -> Symbolic SBool Source

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

thm1 :: IO ThmResult Source

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

thm2 :: IO ThmResult Source

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

# Inspecting symbolic traces

ladnerFischerTrace :: Int -> IO () Source

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 :: Bool
      s_1 = True :: Bool
    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
    ASSERTIONS
    OUTPUTS
      s0
      s8
      s9
      s11
      s12
      s14
      s15
      s18

scanlTrace :: Int -> IO () Source

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 :: Bool
      s_1 = True :: Bool
    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
    ASSERTIONS
    OUTPUTS
      s0
      s8
      s9
      s10
      s11
      s12
      s13
      s14