Floating-point library

Stream: lean4

[Mohit Tekriwal]

Hello, I am trying to find a floating-point library in lean4, similar to the Flocq library in Coq. Could someone please point me to the library?

[Henrik Böving]

Such a library does not currently exist to my knowledge. We do have built-in floating point numbers for program development at docs#Float but not yet verified them.

[Mohit Tekriwal]

okay, thanks!

[Mohit Tekriwal]

Is someone in the LEAN community already working on it though?

[Henrik Böving]

I am at least not aware of anything being publicly announced on here but that doesn't mean it doesn't exist.

[Geoffrey Irving]

Not the same, but I’m working on fixed point intervals arithmetic based on UInt64 (so no new axioms). It would be better to have IEEE floating point for my purposes, though, so +1 to floats being a great thing to do.

[James Gallicchio]

(this is just me being ignorant, but are modern FPUs shown to be bug-free so we can actually assert that the hardware float instructions do always correspond with the IEEE definition?)

[Geoffrey Irving]

Hardware folk do a lot of verification these days, but (1) I don’t know if these extend to full formal SAT/SMT proofs or just lots of model checking and (2) unfortunately the circuit designs are proprietary so we don’t get to see those proofs. However, we would have a choice about what instructions to assume compliant: the safest would be to go with just ring operations and not trust even division, though it’s not very ergonomic.

One thing I find super annoying is that if one wants to do interval arithmetic, modern CPUs handle rounding modes via processor flags, and modern compilers proudly distain these flags and say they consider themselves free to reorder the flag changes across arithmetic operations. This means that doing interval arithmetic safely requires nasty hacks. Thus, if we ever want to use floats to do certified approximate computing, ball arithmetic using round-to-nearest is the better way to go.

Nvidia GPUs are better here: they provide sane “round up / round down” versions of instructions. But other GPUs including Apple’s do not, so there is no portability.

[Geoffrey Irving]

I think given the above the right compromise for most math proof purposes is UInt64 (thus what I am doing). But it would be nice to have the float theory for code that wants to be faster, and for program verification in float contexts.

[James Gallicchio]

That's brutal :/ thanks for the detailed response

[Geoffrey Irving]

The typical move is to set the flag uniformly to “round up”, and store [a,b] as the tuple (-a,b) so that both directions of rounding are handled with the same processor mode (held fixed for a long period of time). But this is not friendly at all for library code which has to interoperate with other stuff arbitrarily.

[Richard Copley]

I have some lemmas here. The main result is u + v = (u ⊝ (u ⊕ v)) ⊕ v[1][2][3]. The assumptions are probably not in a particularly useful form, and there was never any intention to be well-structured, complete or suitable for any particular purpose. Moreover everything is in ℕ, so the results have to be stated and proved in several forms. Still, it kept me busy.

[1] On Properties of Floating Point Arithmetics: Numerical Stability and the Cost of Accurate Computations, Douglas M. Priest, Ph.D. thesis, 1992 (pp. 14-19)
[2] A Floating-Point Technique for Extending the Available Precision, T. J. Dekker, Numerische Mathematik 18:224-242, 1971 (equation 4.4)
[3] The Art Of Computer Programming - Volume 2 (Seminumerical Algorithms), Donald E. Knuth, Third edition, 1997, Addison Wesley Longman (section 4.2.2)

Priest's thesis is great. My results are not as general as his (I assume that, e.g., u ⊕ v = f (u + v) for some unspecified function f satisfying certain assumptions, where Priest makes no such assumption). I think the assumption holds for IEEE (in any rounding mode).