Tools for proving equalities of operations on bitvectors

This repository contains a program for deciding equalities of operations on bitvectors involving a combination of the group operations, unity and the bitwise operations. For example, it can verify the equality $x+y=(x\oplus y)/+2(x\mathrm{\&}y)$.

There is a proof of decidablity in src/v1/decide.lean. However this proof is a very slow algorithm. There is also a much faster algorithm demonstrated in src/v3/tests.lean. This second algorithm does not yet have a Lean proof of correctness.