I have recently had some contact with SMT/Z3, and am now working on the following task:
Two variables, x and y, of type ulong (64-bit unsigned integer type) are given.
Show that the following sequence of instructions: x = x xor y; y = y xor x; x = x xor y; will result in a value swap, i.e., after their execution, the initial value of x will be in the variable y, and the initial value of y will be in x.
I have come up with the following code:
from z3 import *
# Standard swap with temporary variable
def swap(x, y):
temp = x
x = y
y = temp
return x, y
# Swap using xor
def xor_swap(x, y):
x = x ^ y
y = y ^ x
x = x ^ y
return x, y
# Create two 64-bit unsigned variables (64-bit vectors)
X, Y = BitVecs('X Y', 64)
# Create xor-swapped variables
X1, Y1 = xor_swap(X, Y)
# Create swap-with-temporary-variable variables
X2, Y2 = swap(X, Y)
# Create solver
s = Solver()
# Add constraints
# "Are there any values X and Y, for which xor_swap(X,Y) != swap(X,Y)?"
s.add(Or(X1 != X2, Y1 != Y2))
# Check if solver can find a counterexample
# A counterexample is a pair of values X and Y, for which xor_swap(X,Y) != swap(X,Y)
result = s.check()
# No solution
if result == unsat:
print("unsat")
print("No counterexample found")
print("For each pair X,Y: xor_swap(X,Y) == swap(X,Y)")
# Solution found
elif result == sat:
print("sat")
model = s.model()
print("X = ", model[X])
print("Y = ", model[Y])
which returns 'unsat' (as expected, since we know that the XOR swap works).
My question is, how can we be sure that this proof is exhaustive and that it is definitive?
Does this solution cover all cases? Are we 100% sure that the xor swap algorithm works, based just on the code above, or is there any other check we need to perform (or maybe we have to specify the problem in a different way)?
What you did is just fine. For style purposes, you can shorten it to:
X, Y = BitVecs('X Y', 64)
prove(ForAll([X, Y], And([i == j for (i, j) in zip(swap(X, Y), xor_swap(X, Y))])))
but this doesn't really change the proof in any material way; just easier to read perhaps. What you did is just as valid, and might even be preferable as the way you coded can show the model better if there was a discrepancy.
How do you know this is complete? Well, your proof covers all the cases for all 64-bit pairs of two-vectors. How do I know that? That's a meta-level question: Why do you trust some other proof, done in some other system? It's the internal knowledge of the system (to some extent), and also what you accept to be in your trusted-code-base. We know how z3 works, we know how the Python interface to z3 works, and we trust all of that; so it's complete because we "believe" it's complete.
But perhaps all you're asking is if what you did is enough; and the answer is indeed yes. You've covered all the cases necessary.