:prove with yices fails for properties involving (^^) with large exponents

[brianhuffman]

Interestingly, for odd bitvectors x, x ^^ -1 calculates the multiplicative inverse! Try it, it's cool!

Cryptol> 0x35 * 0x35 ^^ -1
0x01

Anyway, yices seems to be pretty good at proving this fact for bit-widths less than 32. But at type [32], we get such an unexpected error that cryptol exits the REPL. If yices can't handle proofs like this, that's OK, but we should at least try to handle the error message gracefully, and stay in the REPL.

Cryptol> :set prover=yices
Cryptol> :prove \(x:[16]) -> x!0 ==> x * (x ^^ -1) == 1
Q.E.D.
(Total Elapsed Time: 0.004s, using Yices)
Cryptol> :prove \(x:[24]) -> x!0 ==> x * (x ^^ -1) == 1
Q.E.D.
(Total Elapsed Time: 0.006s, using Yices)
Cryptol> :prove \(x:[32]) -> x!0 ==> x * (x ^^ -1) == 1
cryptol: 
*** Data.SBV: Unexpected non-success response from Yices:
***
***    Sent      : (define-fun s64 () (_ BitVec 32) (bvmul s63 s63))
***    Expected  : success
***    Received  : (error "at line 71, column 35: in bvmul: maximal polynomial degree exceeded")
***    Exit code : ExitSuccess
***
***    Executable: /Users/huffman/.bin/yices-smt2
***    Options   : --incremental
***
*** Failed to establish solver context. Running in debug mode might provide
*** more information. Please report this as an issue!

CallStack (from HasCallStack):
  error, called at ./Data/SBV/SMT/SMT.hs:722:61 in sbv-7.1-GWUBwRjB6reL6wJl5cixpT:Data.SBV.SMT.SMT

With z3 we also see problems for large bit-widths (>25), but here the message is caught and reported properly, and we stay in the REPL.

Cryptol> :set prover=z3
Cryptol> :prove \(x:[16]) -> x!0 ==> x * (x ^^ -1) == 1
Q.E.D.
(Total Elapsed Time: 0.054s, using Z3)
Cryptol> :prove \(x:[26]) -> x!0 ==> x * (x ^^ -1) == 1
Unknown.
  Reason: Overflow encountered when expanding vector
(Total Elapsed Time: 27.468s, using Z3)

[brianhuffman]

As of revision 8f94daf (a fix for #479), this error no longer causes the REPL to exit. We should file this as an issue with SBV.

[brianhuffman]

This example once again causes the Cryptol REPL to exit, probably because (since SBV version 7.5, when the fix for LeventErkok/sbv#335 was published) SBV now throws a different IOException instead of calling error.

Here's another example I just found that causes the Cryptol REPL to exit with a very similar error message:

Cryptol> :set prover=yices
Cryptol> :prove \(x:Integer) y -> y > 0 ==> -x / -y == x / y
cryptol:
*** Data.SBV: Unexpected non-success response from Yices:
***
***    Sent      : (assert (not s10))
***    Expected  : success
***    Received  : (error "non-linear arithmetic is not allowed in logic ALL")
***
***    Exit code : ExitFailure (-15)
***    Executable: /Users/huffman/.bin/yices-smt2
***    Options   : --incremental
***
***    Reason    : Check solver response for further information. If your code is correct,
***                please report this as an issue either with SBV or the solver itself!