Symbolic Integer exponentiation not caught

[weaversa]

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.

Main> :prove \(a:[5], b:[5], p:[5]) -> p > 0 ==> 10 == fromInteger (toInteger a ^^ toInteger b)
[warning] at <interactive>:1:43--1:54:
  Defaulting type argument 'a' of 'fromInteger' to [4]
Q.E.D.
(Total Elapsed Time: 0.009s, using "Z3")
Main> :check \(a:[5], b:[5], p:[5]) -> p > 0 ==> 10 == fromInteger (toInteger a ^^ toInteger b)
[warning] at <interactive>:1:43--1:54:
  Defaulting type argument 'a' of 'fromInteger' to [4]
Using random testing.
(\(a : [5], b : [5],
   p : [5]) -> p > 0 ==> 10 == fromInteger (toInteger a ^^ toInteger b))
  (11, 17, 28) = False
Main> :prove \(a:[5], b:[5]) -> 10 == fromInteger (toInteger a ^^ toInteger b)
[warning] at <interactive>:1:26--1:37:
  Defaulting type argument 'a' of 'fromInteger' to [4]

operation can not be supported on symbolic values: integer exponentation

[brianhuffman]

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 :-)

[LeventErkok]

@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.

[brianhuffman]

Bisection shows that the first bad commit is ffdf11d by @robdockins, dated March 26, which has the commit message "Minor style and bugfixes".

[brianhuffman]

Changeset ffdf11d introduced the current definition of intExp for the SBV backend; this must be the source of the problem:

cryptol/src/Cryptol/Eval/SBV.hs

Lines 300 to 305 in 1c38465

	intExp sym a b
	| Just e <- svAsInteger b =
	do unless (0 <= e) (raiseError sym NegativeExponent)
	pure $! SBV.svExp a b
	| otherwise =
	raiseError sym (UnsupportedSymbolicOp "integer exponentation")

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")

[brianhuffman]

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.)

[LeventErkok]

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."

[brianhuffman]

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.

[robdockins]

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.

[robdockins]

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.