sbv-8.7: 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

Documentation.SBV.Examples.Uninterpreted.Multiply

Description

Demonstrates how to use uninterpreted function models to synthesize a simple two-bit multiplier.

Synopsis

- mul22 :: (SBool, SBool) -> (SBool, SBool) -> (SBool, SBool)
- synthMul22 :: Goal

# Documentation

mul22 :: (SBool, SBool) -> (SBool, SBool) -> (SBool, SBool) Source #

The uninterpreted implementation of our 2x2 multiplier. We simply receive two 2-bit values, and return the high and the low bit of the resulting multiplication via two uninterpreted functions that we called `mul22_hi` and `mul22_lo`. Note that there is absolutely no computation going on here, aside from simply passing the arguments to the uninterpreted functions and stitching it back together.

NB. While definining `mul22_lo` we used our domain knowledge that the low-bit of the multiplication only depends on the low bits of the inputs. However, this is merely a simplifying assumption; we could have passed all the arguments as well.

synthMul22 :: Goal Source #

Synthesize a 2x2 multiplier. We use 8-bit inputs merely because that is the lowest bit-size SBV supports but that is more or less irrelevant. (Larger sizes would work too.) We simply assert this for all input values, extract the bottom two bits, and assert that our "uninterpreted" implementation in `mul22` is precisely the same. We have:

    >>> sat synthMul22
    Satisfiable. Model:
      mul22_hi :: Bool -> Bool -> Bool -> Bool -> Bool
      mul22_hi False True  True  False = True
      mul22_hi False True  True  True  = True
      mul22_hi True  False False True  = True
      mul22_hi True  False True  True  = True
      mul22_hi True  True  False True  = True
      mul22_hi True  True  True  False = True
      mul22_hi _     _     _     _     = False

      mul22_lo :: Bool -> Bool -> Bool
      mul22_lo True True = True
      mul22_lo _    _    = False

It is easy to see that the low bit is simply the logical-and of the low bits. It takes a moment of staring, but you can see that the high bit is correct as well: The logical formula is `a1b xor a0b1`, and if you work out the truth-table presented, you'll see that it is exactly that. Of course, you can use SBV to prove this. First, define the model we were given to make it symbolic: