sBranch is incompatible with sharing

[LeventErkok]

Current implementation of sBranch interacts badly with the stable-named based sharing. The current implementation is unsound. To wit, consider:

foo :: SWord8 -> SWord8
foo x = sBranch (x .== 0) y (y+1)
  where y = sBranch (x .== 0) x (x+1)

Note the nested sBranch calls here. A nested if-then-else structure is necessary to exhibit this bug. Here's what happens:

• First sBranch runs. SBV asks the solver whether x .== 0 is satisfiable. It of course is. Then it asks the solver whether it's negation is satisfiable, i.e., bnot (x .== 0) which also is satisfiable.
• SBV then proceeds computing the then branch, recording the path condition that x .== 0 holds. Under this assumption the value of y is determined correctly to be x. This value is returned; and is recorded as part of the regular sharing for the expression y.
• SBV then proceeds computing the else branch, i.e., y+1. When this computation needs the value of y, SBV looks up the shared value of y and incorrectly takes it to be x again. The else-branch of the second sBranch is skipped, and the else-branch of the first thus evaluates to x+1. This is a major bug, since sharing this value is only valid under the assumption x .== 0, which no longer holds.
• The final value of foo is then computed to be simply ite (x .== 0) x (x+1)
• So, we have:

*Main> prove $ \x -> foo x .== ite (x .== 0) x (x+1)
Q.E.D.

Which is plain wrong:

*Main> foo 5
7 :: SWord8

The funny thing is that I damn well knew sharing under branch conditions were unsound, and wrote a long commentary for it long time ago when ite was implemented: https://github.com/LeventErkok/sbv/blob/master/Data/SBV/BitVectors/Operations.hs#L371

But when Cryptol implemented the "smart" if-then-else and I implemented the same in SBV, I completely missed the point that the exact same problem is in sBranch as well.

Long story short; sharing without being careful about path-conditions is just unsound. While the sharing implementation can be changed to support path conditions, I'm wary of its more general implications for performance; as sBranch is not that often used.

sAssert suffers from the same problem, as it also does computations under path-assumption.

Proposed solution I'm leaning towards still supporting sBranch/sAssert but turning off all sharing if sBranch/sAssert are used. This will be a dynamic check; the types of these functions unfortunately don't allow state to be accessible at the time of use. So, we'll have a new parameter as part of SMTConfig:

• interactive, which will default to False
• If False we shall dynamically reject sBranch/sAssert calls
• If True we will support sBranch/sAssert but sharing will be turned-off to preserve soundness.

@brianhuffman I'd like to hear your thoughts on the proposed solution.

[LeventErkok]

Here's the sAssert related failure:

import Data.SBV

foo :: SWord8 -> SWord8
foo x = ite (x .== 0) y (y+1)
  where y = sAssert "x must be zero" (x .== 0) x

We get:

*Main> safe foo
No safety violations detected.
*Main> foo 0
0 :: SWord8
*Main> foo 1
*** Exception: Assertion failure: "x must be zero"
*** Fails in all assignments to inputs

for very much the same reasons. So; sharing must be turned off in the presence of sBranch and sAssert.

[LeventErkok]

Turns out the problem is actually much deeper. Consider this expression:

foo :: SWord8 -> SWord8
foo x = sBranch (x .== 0) y (y+1)
  where y = sBranch (x .== 0) x (x+1)

The problem here is not just the way SBV internally caches expressions. While that is indeed a problem, we also are facing the fact that the "Haskell" variable 'y' is cached as well! So, once the inner sBranch is reduced, GHC will not even attempt to re-evaluate it, and rightly so.

What this is saying is that sBranch is just not implementable with the current type signature we have. It cannot be a pure expression. It'll have to be lifted to the Symbolic-monad level; which will make it less useful, but at least sound; assuming we can do a decent implementation.

[LeventErkok]

After some more thought; there's just no easy way to implement sBranch with its current type, while preserving soundness. Thus, I'll be removing sBranch and sAssert shortly.

Instead, we shall add a function isSatisfiableInCurrentPath :: SBool -> Symbolic Bool.

Note that this is quite a different approach: The Symbolic monad is exposed, and thus it's not really a drop-in replacement for if-then-else. Harder to use perhaps, but (I do believe) it is sound.