fp.lean

A library for bitblasting IEEE754 floating point.

-- 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

References

• We use circuits inspired from symfpu for bitblasting.

Trustworthiness: Exhaustive Enumeration

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.

• Berlekee TestFloat.
• Ulp plots. _ Kahan Floating Point Paranoia.
• IEEE floating point testing software.
• An Automatable Formal Semantics for IEEE 754

TODO

• Finish proofs for everything
• Remove Canonical_all axiom
• Add support for more FP formats (OCP, P3109)
• Bench better, setup namespace-bed benching.

References

• IEEE 754-2008 spec
• SMT-LIB floating point specification.
• BTRW15: An Automatable Formal Semantics for IEEE 754
• 2020-2021 Floating Point Course @ Cambridge
• Numerical Computing with IEEE Floating Point Arithmetic by Michael L. Overton.
• FLoPS: IEEE-P3109 in Lean