## [Math][Python][Z3] Bit reverse function verification

This is quite popular function. Unfortunately, such a hackish code is error-prone, an unnoticed typo can easily creep in.

While you can check all possible 32-bit values in brute-force manner, this is infeasible for 64-bit function(s).

As before, I'm not proving here the function is "correct" in some sense, but I'm proving equivalence of two functions: bitrev64() and bitrev64_unoptimized(), which uses bitrev32(), which in turn uses bitrev16(), etc...

#!/usr/bin/python

from z3 import *

# from Henry Warren's "Hacker's Delight", Chapter 7
# Or: https://github.com/torvalds/linux/blob/master/include/linux/bitrev.h

# default right shift in Z3 is arithmetical, so I'm using Z3's LShR() function here, which is logical shift right

def bitrev8(x):
x = LShR(x, 4) | (x << 4)
x = LShR(x & 0xCC, 2) | ((x & 0x33) << 2)
x = LShR(x & 0xAA, 1) | ((x & 0x55) << 1)
return x

# these "unoptimized" versions are constructed like a Russian doll...

def bitrev16_unoptimized(x):
return (bitrev8(x & 0xff) << 8) | (bitrev8(LShR(x, 8)))

def bitrev32_unoptimized(x):
return (bitrev16_unoptimized(x & 0xffff) << 16) | (bitrev16_unoptimized(LShR(x, 16)))

def bitrev32(x):
x = LShR(x, 16) | (x << 16)
x = LShR(x & 0xFF00FF00, 8) | ((x & 0x00FF00FF) << 8)
x = LShR(x & 0xF0F0F0F0, 4) | ((x & 0x0F0F0F0F) << 4)
x = LShR(x & 0xCCCCCCCC, 2) | ((x & 0x33333333) << 2)
x = LShR(x & 0xAAAAAAAA, 1) | ((x & 0x55555555) << 1)
return x

def bitrev64_unoptimized(x):
# both versions must work:
return (bitrev32_unoptimized(x & 0xffffffff) << 32) | bitrev32_unoptimized(LShR(x, 32))
#return (bitrev32(x & 0xffffffff) << 32) | bitrev32(LShR(x, 32))

def bitrev64 (a):
a = LShR(a, 32) ^ (a << 32)
m = 0x0000ffff0000ffff
a = (LShR(a, 16) & m) ^ ((a << 16) & ~m)
m = 0x00ff00ff00ff00ff
a = (LShR(a, 8) & m) ^ ((a << 8) & ~m)
m = 0x0f0f0f0f0f0f0f0f
a = (LShR(a, 4) & m) ^ ((a << 4) & ~m)
m = 0x3333333333333333
a = (LShR(a, 2) & m) ^ ((a << 2) & ~m)
m = 0x5555555555555555
a = (LShR(a, 1) & m) ^ ((a << 1) & ~m)
return a

s=Solver()

x=BitVec('x', 64)

# tests.
# uncomment any.
# must be "unsat" in each case.

# these are involutory functions, i.e., f(f(x))=x

# must be "unsat", no counterexample found
print s.check()



The problem is easy enough to be solved using my toy MK85 bitblaster, with only tiny modifications:

#!/usr/bin/python

from MK85 import *

# MK85 uses logical shift right for Python operator >>, so here is it as is...

def bitrev32(x):
x = (x >> 16) | (x << 16)
x = ((x & 0xFF00FF00) >> 8) | ((x & 0x00FF00FF) << 8)
x = ((x & 0xF0F0F0F0) >> 4) | ((x & 0x0F0F0F0F) << 4)
x = ((x & 0xCCCCCCCC) >> 2) | ((x & 0x33333333) << 2)
x = ((x & 0xAAAAAAAA) >> 1) | ((x & 0x55555555) << 1)
return x

def bitrev64_unoptimized(x):
return (bitrev32(x & 0xffffffff) << 32) | bitrev32(x >> 32)

s=MK85(verbose=0)

def bitrev64 (a):
a = (a >> 32) ^ (a << 32)
m = 0x0000ffff0000ffff
a = ((a >> 16) & m) ^ ((a << 16) & ~m)
m = 0x00ff00ff00ff00ff
a = ((a >> 8) & m) ^ ((a << 8) & ~m)
m = 0x0f0f0f0f0f0f0f0f
a = ((a >> 4) & m) ^ ((a << 4) & ~m)
m = 0x3333333333333333
a = ((a >> 2) & m) ^ ((a << 2) & ~m)
m = 0x5555555555555555
a = ((a >> 1) & m) ^ ((a << 1) & ~m)
return a

x=s.BitVec('x', 64)
y=s.BitVec('y', 64)

# tests.

# check this: