Strengthen Symbolic Execution of %

[weaversa]

Consider gcd:

gcd : [8] -> [8] -> [8]
gcd a b = if(b == 0) then a
          else gcd b (a%b)

We can use :exhaust to prove the following property about gcd, but :prove never returns.

Main> :exhaust \x -> gcd 0 x == x
Using exhaustive testing.
passed 256 tests.
Q.E.D.
Main> :prove \x -> gcd 0 x == x
<break>

The termination condition of gcd is that b = 0. Since, for the above proof, b is symbolic, both branches of the if statement are followed because we can't determine whether or not b is 0. The second time through the recursion, a takes on the symbolic value of b, and now b takes on 0%b, which (as seen below) is 0, so the recursion should terminate.

Main> :prove \x -> 0%(x:[8]) == 0
Q.E.D.

I figure that the implementation of % in the symbolic execution engine could to be strengthened by ensuring that constant values are propagated when available, helping avoid symbolic termination problems.

[brianhuffman]

Note that this example works fine with :set iteSolver=on.

The SBV library implements various optimizations of this kind, e.g. 0 * x = 0, 0 + x = x. It should be a simple matter to add a special-case rule for sRem 0 x = 0 to the SBV library, and contribute the patch upstream.

[weaversa]

I don't know the list of rules SBV maintains, but it's also the case that sRem x 1 = 0.

[LeventErkok]

Added a few rules to SBV that should address these cases: LeventErkok/sbv@f2bb5a6

In reality, I find such "optimizations" to hardly ever pay off. As Brian mentioned, using 'iteSolver' (or sBranch in SBV parlance) is probably the right thing to do in such cases.

[brianhuffman]

Fixed in 80ec38f, which included SBV changes from LeventErkok/sbv@f2bb5a6.