\myheading{Bit reverse function}
\label{bitrev}

\renewcommand{\CURPATH}{proofs/bitrev}

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

\begin{lstlisting}
#define __constant_bitrev32(x)	\
({					\
	u32 ___x = x;			\
	___x = (___x >> 16) | (___x << 16);	\
	___x = ((___x & (u32)0xFF00FF00UL) >> 8) | ((___x & (u32)0x00FF00FFUL) << 8);	\
	___x = ((___x & (u32)0xF0F0F0F0UL) >> 4) | ((___x & (u32)0x0F0F0F0FUL) << 4);	\
	___x = ((___x & (u32)0xCCCCCCCCUL) >> 2) | ((___x & (u32)0x33333333UL) << 2);	\
	___x = ((___x & (u32)0xAAAAAAAAUL) >> 1) | ((___x & (u32)0x55555555UL) << 1);	\
	___x;								\
})
\end{lstlisting}
( \url{https://github.com/torvalds/linux/blob/master/include/linux/bitrev.h} )

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: \verb|bitrev64()|
and \verb|bitrev64_unoptimized()|, which uses \verb|bitrev32()|, which in turn uses \verb|bitrev16()|, etc...

\lstinputlisting[style=custompy]{\CURPATH/bitrev_Z3.py}

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

\lstinputlisting[style=custompy]{\CURPATH/bitrev_MK85.py}