Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

Bounded fixed-point unrolling.

# Documentation

bfix :: (SymVal a, Uninterpreted (SBV a -> r)) => Int -> String -> ((SBV a -> r) -> SBV a -> r) -> SBV a -> r Source #

Bounded fixed-point operation. The call `bfix bnd nm f`

unrolls the recursion in `f`

at most
`bnd`

times, and uninterprets the function (with the name `nm`

) after the bound is reached.

This combinator is handy for dealing with recursive definitions that are not symbolically terminating and when the property we are interested in does not require an infinite unrolling, or when we are happy with a bounded proof. In particular, this operator can be used as a basis of software-bounded model checking algorithms built on top of SBV. The bound can be successively refined in a CEGAR like loop as necessary, by analyzing the counter-examples and rejecting them if they are false-negatives.

For instance, we can define the factorial function using the bounded fixed-point operator like this:

bfac :: SInteger -> SInteger bfac = bfix 10 "fac" fact where fact f n = ite (n .== 0) 1 (n * f (n-1))

This definition unrolls the recursion in factorial at most 10 times before uninterpreting the result. We can now prove:

`>>>`

Q.E.D.`prove $ \n -> n .>= 1 .&& n .<= 9 .=> bfac n .== n * bfac (n-1)`

And we would get a bogus counter-example if the proof of our property needs a larger bound:

`>>>`

Falsifiable. Counter-example: s0 = 10 :: Integer fac :: Integer -> Integer fac _ = 2`prove $ \n -> n .== 10 .=> bfac n .== 3628800`

The counter-example is telling us how it instantiated the function `fac`

when the recursion
bottomed out: It simply made it return `2`

for all arguments at that point, which provides
the (unintended) counter-example.

By design, if a function defined via `bfix`

is given a concrete argument, it will unroll
the recursion as much as necessary to complete the call (which can of course diverge). The bound
only applies if the given argument is symbolic. This fact can be used to observe concrete
values to see where the bounded-model-checking approach fails:

`>>>`

Falsifiable. Counter-example: bfac_10 = 3628800 :: Integer bfac_n = 7257600 :: Integer s0 = 10 :: Integer fac :: Integer -> Integer fac _ = 2`prove $ \n -> n .== 10 .=> observe "bfac_n" (bfac n) .== observe "bfac_10" (bfac 10)`

Here, we see further evidence that the SMT solver must have decided to assign the
value `2`

in the final call just as it was reaching the base case, and thus got the
final result incorrect. (Note that `7257600 = 2 * 3628800`

.) A wrapper algorithm can
then assert the actual value of `bfac 10`

here as an extra constraint and can
search for "deeper bugs."