Incorrect encoding of binary subnormal floats

[robdockins]

Consider

> :m Float
Loading module Cryptol
Loading module Float
Float> fpFromBits (zero#0x1) : Float32
0x8.0p-152

This, I believe, correctly represents the smallest positive 32-bit subnormal floating-point value. However, if we encode this back into bits, we get something else entirely.

Float> fpToBits (0x8.0p-152 : Float32)
0xf5000000
Float> fpToBits (fpFromBits (zero#0x1) : Float32)
0xf5000000

[weaversa]

Since it’s only 32-bits, it’s entirely possible to do an exhaustive comparison against a trusted floating point implementation. Might be a worthwhile thing to do with all these operations...

[brianhuffman]

So fpToBits should always be the inverse of fpFromBits, but it appears that isn't always the case. Here's an example testing all possible values for a 12-bit float type. If it was implemented correctly, the output would consist of all 1 bits:

Float> groupBy`{32} [ fpToBits (fpFromBits`{5,7} x) == x | x <- [0..0xfff] ]
[0x80000000, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0x80000000, 0x80000000, 0x80000000,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff,
 0xffffffff, 0x80000000, 0x00000000]

[robdockins]

I'm pretty sure I have a fix.

You have to be careful, though. The property you've stated isn't quite correct because NaNs are always round-tripped to a canonical quiet NaN.

[brianhuffman]

Yeah, I just realized that all of the non-subnormal mismatches are for NaN values; I wasn't sure whether or not those were supposed to be all mapped to the same value.

I guess the real property you want to test is whether those two functions are inverses when you compose them the other way around.

[robdockins]

I'm currently running the following before I check in a fix.

:exhaust (\x -> (y != y \/ x == fpToBits y  where y = fpFromBits x : Float32))

So far it's about 10% in, no failures yet.