:set iteSolver=on is unsound

[LeventErkok]

@atomb @brianhuffman @acfoltzer

[This is a direct consequence of a bug in SBV: https://github.com/LeventErkok/sbv/issues/180. So, no immediate action is needed on the Crytpol side; but see below for a discussion.]

Consider this Cryptol program:

foo : [8] -> [8]
foo x = if x == 0 then y else y+1
  where y = if x == 0 then x else x+1

property bad x = foo x == if x == 0 then x else x+1

We have:

Main> :prove bad
bad 0xfe = False

which is correct. But:

Main> :set iteSolver=on
Main> :prove bad
Q.E.D.

Oops.. But Cryptol isn't to blame; as I mentioned, this is an SBV bug. See LeventErkok/sbv#180 for details.

I've outlined a proposed solution in the above ticket. Unfortunately, Cryptol can't just take advantage of it by a simple recompile. It'll have to pass a special configuration parameter to SBV if iteSolver is turned on. It should be a simple tweak, but will require a new release obviously. (Both for SBV and Cryptol.)

I don't want to make a big fuss about this either: Neither sBranch in SBV, nor iteSolver in Cryptol are heavily used; so we can have some discussion around how to best address the issue, and I'm open to hearing ideas on how to proceed. But strictly speaking, this is a soundness issue and thus needs to be dealt with; it's not just a matter of some programs not working, but rather Cryptol/SBV just plain lying about properties when iteSolver is turned on.

[LeventErkok]

After some consideration, it boils down to the fact that it's not just SBV's sharing, but also Haskell's own sharing that's getting into play here. I've put some comments in LeventErkok/sbv#180. Bottom line, sBranch/sAssert are not sound, and thus I removed them in: LeventErkok/sbv@d04fa40

There is now the following function, however:

isSatisfiableInCurrentPath :: SBool -> Symbolic Bool

You might still be able to implement iteSolver using this function, though it's not going to be as simple as before, since the Symbolic type is now exposed in this call. Let me know how you decide to proceed and once things settle down, I'll make a new SBV release.

[acfoltzer]

This is now removed both from the 2.2 maintenance branch and master. When we eventually do a refactoring of the evaluator to permit a monadic context, we'll try to reintroduce this feature.