A library for bitblasting IEEE754 floating point multiplication.
-- https://github.com/opencompl/fp.lean/blob/5e51278246ed86f5e772ee6697400c163b56d5e3/Fp/Multiplication.lean#L82
theorem mul_one_is_id (a : PackedFloat 5 2) (m : RoundingMode) (ha : ¬a.isNaN)
: (mul a oneE5M2 m) = a := by
apply PackedFloat.inj
simp at ha
simp [mul, round, BitVec.cons, oneE5M2, -BitVec.shiftLeft_eq', -BitVec.ushiftRight_eq']
bv_decide- We use circuits inspired from symfpu for bitblasting.
Our CI exhaustively enumerates against the FloatX and symfpu libraries for bit-for-bit compatibility.
We would appreciate pull requests that improve our testing. We audited several librares, but settled on our choices since they enable us to test all rounding modes for small bitwidths.