:check for float types never produces subnormal numbers

[brianhuffman]

Even with a very large number of tests (like a million) we never come across any examples where the exponent is all 0 bits, except for 0.0.

Cryptol> :m Float
Loading module Cryptol
Loading module Float
Float> :set tests=1000000
Float> :check \x -> take`{6} (drop`{1} (fpToBits`{6,10} x)) != 0 \/ x == 0
Using random testing.
Passed 1000000 tests.

Note that this can't be tested with :exhaust, due to #1051.

[robdockins]

The random generator for floats is here:

cryptol/src/Cryptol/Testing/Random.hs

Line 257 in 9b9f452

randomFloat ::

I think it's technically possible to produce subnormal numbers, just quite unlikely, even for small float types.

[brianhuffman]

I can get :check to find subnormal numbers if the exponent is 5 or lower, but so far I have not come across one with an exponent of 6 or more bits after many millions of trials. Even if it is actually possible for the generator to produce them, I think we need to tweak the generator to produce them a bit more often.

[robdockins]

Agreed. I've been using a more sophosticated generator for some What4 testing I'll probably port here. It switches, with fixed probabilities, between selecting special numbers (NaN, Inf, zeros), selecting numbers "mathematically" (but better than here, I think), and selecting numbers based on their bitwise representation. The bitwise form can be tweaked to produce subnormals quite easily.

[brianhuffman]

If I understand the code correctly, it looks like floats are generated as rational numbers, where the numerator and denominator are chosen from uniform distributions of the same magnitude. This means that this distribution will be biased rather heavily towards numbers near 1. So not only will subnormals be rare, but also very large numbers will be quite rare as well.

[robdockins]

I believe that's correct, yes.

[brianhuffman]

Indeed, you have to do a lot of searching to find a Float32 that's bigger than a million:

Float> :check \(x : Float32) -> x < 1000000
Using random testing.
Passed 100000 tests.

(Doing a million tests was enough to find one, though.)

[robdockins]

Fixed via #1069