Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
ChrisHughes24 authored May 30, 2023
1 parent 73e8e62 commit 2c18de3
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,4 @@

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\And 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/vs/tests.lean`. This second algorithm does not yet have a Lean proof of correctness.
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.

0 comments on commit 2c18de3

Please sign in to comment.