Floating points are nice and all. You can get pretty far pretending they are actually numbers. But they don’t obey some mathematical properties that feel pretty obvious. A classic to glance through is “What Every Computer Scientist Should Know About Floating-Point Arithmetic” https://docs.oracle.com/cd/E19957-01/806-3568/ncg_goldberg.html
We can check some properties with z3py. Here are a couple simple properties that succeed for mathematical integers and reals, but fail for floating point
I recently saw on twitter a reference to a Sylvie Boldo paper https://hal.archives-ouvertes.fr/hal-01148409/ “Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number”.
In it, she uses FlocQ and Coq to prove a somewhat surprising result that the naive formula actually is correct for the right rounding mode of floating point, something I wouldn’t have guessed.
Z3 confirms for
Float16. I can’t get
Float32 to come back after even a day on a fairly beefy computer. If I use
FPSort(ebits,sbits) rather than a standard size, it just comes back unknown, so i can’t really see where the cutoff size is. This does not bode well for checking properties of floating point in z3 in general. I think a brute force for loop check of 32 bit float properties is feasible. I might even be pretty fast. To some degree, if z3 is taking forever to find a counterexample, I wonder to what to degree the property is probably true.
If anyone has suggestions, I’m all ears.