Yeah, it was really hard to minimize the title within HN's limit. It comes from the following description in the "how" document (emphases on used words):
> 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.
> 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