This PR implements the fast circuit for overflow detection in unsigned
multiplication used by Bitwuzla and proposed in:
https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=987767
The theorem is based on three definitions:
* `uppcRec`: the unsigned parallel prefix circuit for the bits until a
certain `i`
* `aandRec`: the conjunction between the parallel prefix circuit at of
the first operand until a certain `i` and the `i`-th bit in the second
operand
* `resRec`: the preliminary overflow flag computed with these two
definitions
To establish the correspondence between these definitiions and their
meaning in `Nat`, we rely on `clz` and `clzAuxRec` definitions.
Therefore, this PR contains the `clz`- and `clzAuxRec`-related
infrastructure that was necessary to get the proofs through.
An additional change this PR contains is the moving of `### Count
leading zeros` section in `BitVec.Lemmas` downwards. In fact, some of
the proofs I wrote required introducing `Bitvec.toNat_lt_iff` and
`BitVec.le_toNat_iff` which I believe should live in the `Inequalities`
section. Therefore, to put these in the appropriate section, I decided
to move the whole `clz` section downwards (while it's small and
relatively self contained. Specifically, the theorems I moved are:
`clzAuxRec_zero`, `clzAuxRec_succ`, `clzAuxRec_eq_clzAuxRec_of_le`,
`clzAuxRec_eq_clzAuxRec_of_getLsbD_false`.
The fast circuit is not yet the default one in the bitblaster, as it's
performance is not yet competitive due to some missing rewrites that
bitwuzla supports but are not in Lean yet.
co-authored-by: @bollu
---------
Co-authored-by: Tobias Grosser <tobias@grosser.es>
3e11f27ff4