SBV generates inputs ABC cannot handle

[robdockins]

With SBV 8.6

Prelude Data.SBV.Dynamic> proveWith abc (do { x <- sWordN 32 "x"; y <- sWordN 5 "y"; return (svEqual x ((x `svRotateLeft` y) `svRotateRight` y))})
*** Exception:
*** Data.SBV: fd:15: hGetLine: end of file:
***
***    Sent      : (check-sat)
***
***    Executable: /Users/rdockins/.local/bin/abc
***    Options   : -S "%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000"
***
***    Hint      : Solver process prematurely ended communication.
***                It is likely it was terminated because of a seg-fault.
***                Run with 'transcript=Just "bad.smt2"' option, and feed
***                the generated "bad.smt2" file directly to the solver
***                outside of SBV for further information.

Interestingly, the Data.SBV interface doesn't seem to have this problem, so maybe theres an easy solution?

Prelude Data.SBV> proveWith abc (forAll ["x","y"] (\ (x::SWord32) -> \(y::SWord8) -> (x `sRotateLeft` y) `sRotateRight` y .== x))
Q.E.D.

The suspicion from GaloisInc/cryptol#436 is that this is related to the use of SMT arrays.

[robdockins]

OK, well, this is a wrinkle I did not expect. I just wanted to absolutely verify that the size of y doesn't matter... and actually it does.

Prelude Data.SBV.Dynamic> proveWith abc (do { x <- sWordN 32 "x"; y <- sWordN 8 "y"; return (svEqual x ((x `svRotateLeft` y) `svRotateRight` y))})
Q.E.D.

[LeventErkok]

I'd hazard a guess that when you use a 5-bit word SBV generates code to "normalize" it, and ABC chokes on it. It probably doesn't support bvurem operation, or something similar. And indeed, you can make it crash from the regular interface as well, just use the proper sizes:

Prelude Data.SBV> :set -XDataKinds
Prelude Data.SBV> proveWith abc (forAll ["x","y"] (\ (x::SWord32) -> \(y::SWord 5) -> (x `sRotateLeft` y) `sRotateRight` y .== x))
*** Exception:
*** Data.SBV: fd:15: hGetLine: end of file:
***
***    Sent      : (check-sat)
***
***    Executable: /usr/local/bin/abc
***    Options   : -S "%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000"
***
***    Hint      : Solver process prematurely ended communication.
***                It is likely it was terminated because of a seg-fault.
***                Run with 'transcript=Just "bad.smt2"' option, and feed
***                the generated "bad.smt2" file directly to the solver
***                outside of SBV for further information.

Note the y :: SWord 5 vs y :: SWord8 above!

[LeventErkok]

Yeah, I wouldn't trust abc when bvurem is involved; it might crash if you're lucky, or produce something that's totally bogus:

Prelude Data.SBV> satWith abc{validateModel = True} $ \x y -> x `sMod` (y :: SWord 5) .== 0
*** Data.SBV: Model validation failure: Final output evaluated to False.
***
*** Assignment:
***
***       s0 = 31 :: WordN 5
***       s1 = 15 :: WordN 5
***
*** Backend solver returned a model that does not satisfy the constraints.
*** This could indicate a bug in the backend solver, or SBV itself. Please report.
***
*** Alleged model:
***
*** Satisfiable. Model:
***   s0 = 31 :: WordN 5
***   s1 = 15 :: WordN 5

Ugh.. That's really bad! You can (and probably should) report this to ABC folks; though I'm not sure if you'll get a better answer than bvurem isn't supported. (Though it's not clear what they really do with it.)

[LeventErkok]

Also relevant: https://bitbucket.org/alanmi/abc/issues/71/abc-fails-assertion-on-smt-file

We can make SBV should check if there are tables in the generated program and refuse to call ABC if that's the case. We already have a "capabilities" mechanism for doing so. But given this is such a "fundamental" SMTLib functionality, I'm not sure it has pay-off. ABC probably also doesn't support uninterpreted functions or any of the fancier BV methods either.

[robdockins]

Oh, yeah! That's a real bummer! Here's another bummer:

Prelude Data.SBV> proveWith yices (forAll ["x","y"] (\ (x::SWord32) -> \(y::SWord 8) -> (x `sRotateLeft` y) `sRotateRight` (y-3) .== x))
Falsifiable. Counter-example:
  x = 1073741824 :: Word32
  y =          1 :: Word8
Prelude Data.SBV> proveWith z3 (forAll ["x","y"] (\ (x::SWord32) -> \(y::SWord 8) -> (x `sRotateLeft` y) `sRotateRight` (y-3) .== x))
Falsifiable. Counter-example:
  x = 1094795585 :: Word32
  y =         31 :: Word8
Prelude Data.SBV> proveWith abc (forAll ["x","y"] (\ (x::SWord32) -> \(y::SWord 8) -> (x `sRotateLeft` y) `sRotateRight` (y-3) .== x))
Q.E.D.

So, I'm not sure what ABC is doing with these problems, but it seems like it's just wrong.

[LeventErkok]

To be fair, ABC is really not an SMT solver. It was used in early versions of Cryptol-1's symbolic back-end, when everything was bit-blasted, i.e., it was used as a SAT solver. (And in that case it worked really well.) When we created SMT backend for Cryptol, we (i.e., our customers!) asked Alan to add basic support for SMT, and he added support for a very limited subset of SMTLib, mainly the bit-vector logic with some niceties.

What's bad is ABC seems to be silently "ignoring" what it doesn't support and just plunging ahead and doing something. Perhaps you can ask Alan to fix those cases. (i.e., recognize and "reject", as opposed to ignore and continue.) Expecting him to support more of SMTLib, however, sounds like a non-starter. Sean should have a better handle on what Alan can provide here.

[LeventErkok]

There isn't really much SBV can do regarding this ticket. ABC will likely never support all the operations we generate.