Closed weaversa closed 4 years ago
Wow, yeah, this is totally a bug. We can also prove even more ridiculous things like this:
Cryptol> :prove \(n:Integer, p : Bit) -> p ==> (x != x where x = 2 ^^ n)
Q.E.D.
(Total Elapsed Time: 0.031s, using "Z3")
I have a feeling that the problem might lie within the SBV library; maybe it's some weird interaction having to do with path conditions and partially-defined functions. With @robdockins' new what4
-based backend, we get the "operation not supported" message:
Cryptol> :set prover=w4-z3
Cryptol> :prove \(n:Integer, p : Bit) -> p ==> (x != x where x = 2 ^^ n)
operation can not be supported on symbolic values: integer exponentation
As for the wording of the error message, I guess we support neither "exponentation" nor exponentiation on symbolic integers, so it's technically correct :-)
@brianhuffman
This doesn't reproduce with Cryptol 2.8.0 from Hackage:
$ cryptol
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃ ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹ ╹ ┗━┛┗━╸
version 2.8.0
Loading module Cryptol
Cryptol> :prove \(n:Integer, p : Bit) -> p ==> (x != x where x = 2 ^^ n)
SBV error:
svExp: exponentiation only works with unsigned bounded symbolic exponents, kind: SInteger
(Also note that exponentiation
is correctly spelled, and I double-checked the above string directly comes from SBV itself.)
But this version also doesn't understand :set prover=w4-z3
, so I'm guessing you must've recently changed how power is compiled and it does something funky as it goes through the SBV backend.
Let me know what you find out; planning to have an SBV release soon, so it'd be good to have this incorporated if there's anything to be done on the SBV side.
Bisection shows that the first bad commit is ffdf11d202d687fa7a7249bfdfc0da7b6fe2763a by @robdockins, dated March 26, which has the commit message "Minor style and bugfixes".
Changeset ffdf11d introduced the current definition of intExp
for the SBV backend; this must be the source of the problem: https://github.com/GaloisInc/cryptol/blob/1c38465ca8f6c96e69c76c07d4186a501591de19/src/Cryptol/Eval/SBV.hs#L300-L305
I can also confirm that the first branch of that definition (with the svAsInteger
guard) is not the problem. I replaced pure $! SBV.svExp a b
with a call to error
and I get the same Q.E.D.
proof result as before. So it's totally not SBV's fault.
My best guess is that the real problem is some interaction between raiseError
and conditional expressions in the evaluation backend, or else :prove
is doing something wrong with the safety predicate that the evaluation backend is producing now.
Here's another instance of the same bug, which doesn't use integer exponentiation at all:
Cryptol> :prove \(p : Bit) -> p ==> undefined
Q.E.D.
(Total Elapsed Time: 0.009s, using "Z3")
An even more ridiculous example, this one showing :sat
also getting it wrong:
Cryptol> :prove \p -> if p then undefined else if p then True else undefined
Q.E.D.
(Total Elapsed Time: 0.008s, using "Z3")
Cryptol> :sat \p -> if p then undefined else if p then True else undefined
(\p -> if p then undefined else if p then True else undefined)
False = True
(Total Elapsed Time: 0.009s, using "Z3")
(Note that this predicate should always evaluate to undefined
.)
In Cryptol 1.X, our strategy was to symbolically substitute zero
for all partial functions when the value was undefined, and then make the meta-claim that :prove
and :sat
results are only valid provided :safe
says the input is safe indeed.
I think Cryptol 2.X has dropped :safe
and tried to do a better job of handing undetermined behavior directly within the evaluator. This is always a weak point, even for SBV, but I can see the allure of it. One sticking point is really trying to reconcile what SMTLib says for partiality and what your language does (division by 0 being the prime example). An SMT solver can simply produce "any value" when undefined behavior exists, given it's a logic of total functions. And it'll almost always pick something that makes the output confusing as it's trying to sat
or prove
the predicate.
I think the :safe
approach is the easiest to understand and implement, but from the end-users perspective, it's cognitive burden and yet another thing to "remember."
In Cryptol 2.x we (until recently) translated all partial functions to zero
in the symbolic backend wherever they were undefined. With the recent evaluator overhaul by @robdockins (#684), that has now changed, and I think that is the cause of all this surprising behavior. So where previously we had translated if p then q else undefined
into SMTLib as if p then q else False
we now translate it as just q
, along with a safety predicate of p
(which we then ignore). Ignoring the safety predicate in this situation leads to some pretty confusing behavior.
Yes, I'm pretty sure I understand what's happening here. The issue is that during the overhaul, I made sure we explicitly computed safety predicates, but pending some design decisions (CF #284), I left the safety predicates as ignored in the SBV backend. I think we've arrived at a consensus for how :safe
and safety predicates should work, so I'll go ahead and work on that shortly.
It's worth noting, also, that PR #724 will change the type of (^^)
so that this error cannot happen anymore.
Fixed in #724. We eventually decided to continue to allow exponents to be Integer, so this error can still occur. However, it's now upgraded in severity so it doesn't interact with safety predicates, and instead just throws an exception.
If I add a conditional in front of the Integer exponentiation, z3 proves an incorrect theorem. I gather that the check "operation can not be supported on symbolic values: integer exponentation" is being avoided somehow. Also, "exponentation" in the error message is spelled wrong.