Haroldbot, client-side tool that checks 32-bit bitvector arithmetic equivalence
haroldbot.nl
haroldbot.nl
That said, I wonder if it would make more sense to use an SMT prover as fallback rather than a SAT solver. The latter requires converting the 32-bit operations into boolean circuits, which might not be the most efficient way to solve the problem considering modern SMT solvers such as Z3 and CVC5 already have built-in efficient support for bit-vectors?
In fact, I believe that's what Alive2 [1] does, which is a similar tool (although with slightly different goals).
I think it might even be possible to make this work for 64-bit vectors with SMT (in most cases).
Just in case nobody else is far enough outside the industry to tell, this is a hilariously nonsensical post title for us ignorant laymen. It sounds like a fake product out of HBO’s Silicon Valley.
> Haroldbot is a tool that checks the equivalence of arithmetic expressions with 32-bit bitvector semantics, running entirely on the client. This task is mostly accomplished by encoding the expression as an array of 32 binary decision diagrams, one for each bit. Since for a given variable ordering a BDD of a boolean function is canonical, this representation offers and easy equivalence test, at the cost of having to build the BDD first.
You may get more information from the aforementioned document: http://haroldbot.nl/how.html