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
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.