# Stupid is as Stupid Does: Floating Point in Z3Py

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

 from z3 import * def numbery_proofs(sort): x = Const("x", sort) y = Const("y", sort) z = Const("z", sort) print("Commutativity") prove(x + y == y + x) #Commutativity print("Associativity") prove(((x + y) + z) == ((x + (y + z)))) #associativity print("Additive Identity") prove(x + 0 == x) # 0 additive identity print("Multiplicative Identity") prove(1 * x == x) print("Trichotomy") prove(Or(x > 0, x < 0, x == 0)) #trichotomy print("Distributivity") prove(x * (y + z) == x * y + x * z) print("Square positive") prove(x * x >= 0) print("Ints -----------------") numbery_proofs(IntSort()) print("Reals ---------------") numbery_proofs(RealSort()) print("Float----------------") numbery_proofs(Float16()) ''' Output Ints ----------------- Commutativity proved Associativity proved Additive Identity proved Multiplicative Identity proved Trichotomy proved Distributivity proved Square positive proved Reals --------------- Commutativity proved Associativity proved Additive Identity proved Multiplicative Identity proved Trichotomy proved Distributivity proved Square positive proved Float---------------- Commutativity proved Associativity counterexample [z = -1.9375*(2**8), y = 1.0009765625*(2**14), x = 1.5224609375*(2**4)] Additive Identity counterexample [x = -0.0] Multiplicative Identity proved Trichotomy counterexample [x = NaN] Distributivity counterexample [z = -1.0029296875*(2**-2), y = 1.01171875*(2**-10), x = -1.4833984375*(2**8)] Square positive counterexample [x = NaN] '''
view raw numbery.py hosted with ❤ by GitHub

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 $\sqrt{x^2} = |x|$ 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.

 from z3 import * x = FP("x", Float16()) rm = RNE() # Rounding Nearest Ties to Even x2 = fpMul(rm, x, x) absx1 = fpSqrt(rm, x2) absx2 = fpAbs(x) s = Solver() s.add( 0.01 <= x, x <= 100) s.add( absx1 != absx2) res = s.check() print(res) if res == sat: m = s.model() print(m.eval(absx1)) print(m.eval(absx2))
view raw stupid.py hosted with ❤ by GitHub