Float exponent size seems to be unnecessarily restricted to start at 3

[LeventErkok]

Looks like Cryptol requires the exponent size to be at least 3:

Float> 0 : Float 3 2
0.0
Float> 0 : Float 2 2

[error] at <interactive>:1:1--1:2:
  Unsolved constraints:
    • Literal 0 (Float 2 2)
        arising from
        use of literal or demoted expression
        at <interactive>:1:1--1:2
[error] at <interactive>:1:1--1:14:
  Unsolved constraints:
    • ValidFloat 2 2
        arising from
        use of partial type function Float
        at <interactive>:1:1--1:14```

From the code, I see that this directly comes from libbf itself (i.e.,, the C implementation of libbf itself):

/* libbf.h */
65:#define BF_EXP_BITS_MIN 3

The Haskell LibBF package and Cryptol's ValidFloat predicate impose this minimum accordingly.

But I don't think this is really needed. It should really be 2. If you grep through the libBF code itself, I see no mentions of the constant BF_EXP_BITS_MIN anywhere else. And when I played around with it, everything seems just fine using an exponent bit size of 2.

The # of bits in the exponent is bounded above by 62 on a 64-bit system; which sounds reasonable, though not strictly required by anything floating-point. Note that SMTLib only requires eb/sb to be both > 1, allowing eb to start at 2:

; Floating point sort, indexed by the length of the exponent and significand ; components of the number :sorts_description "All nullary sort symbols of the form

(_ FloatingPoint eb sb),

where eb and sb are numerals greater than 1."

(From http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml).

I experimented directly with LibBF itself via SBV, and nothing broke when I tried it with eb set to 2.

Prelude Data.SBV> allSat $ \(x :: SFloatingPoint 2 2) -> sTrue
Solution #1:
  s0 = NaN :: FloatingPoint 2 2
Solution #2:
  s0 = 0.0 :: FloatingPoint 2 2
Solution #3:
  s0 = 2.0 :: FloatingPoint 2 2
Solution #4:
  s0 = Infinity :: FloatingPoint 2 2
Solution #5:
  s0 = -Infinity :: FloatingPoint 2 2
Solution #6:
  s0 = -1.5 :: FloatingPoint 2 2
Solution #7:
  s0 = -0.5 :: FloatingPoint 2 2
Solution #8:
  s0 = 0.5 :: FloatingPoint 2 2
Solution #9:
  s0 = -0.0 :: FloatingPoint 2 2
Solution #10:
  s0 = -2.0 :: FloatingPoint 2 2
Solution #11:
  s0 = -1.0 :: FloatingPoint 2 2
Solution #12:
  s0 = -3.0 :: FloatingPoint 2 2
Solution #13:
  s0 = 1.0 :: FloatingPoint 2 2
Solution #14:
  s0 = 3.0 :: FloatingPoint 2 2
Solution #15:
  s0 = 1.5 :: FloatingPoint 2 2
Found 15 different solutions.

Of course this is a very simple test, but indeed FloatingPoint 2 2 is inhabited exactly by 15 members in SMTLib semantics.

So, I'm curious if you know why the lower-limit is set to 3 in LibBF (and consequently in Cryptol), and if anything would break if we relax it to 2.

(Admittedly, this is more a curiosity than any real need; but it'd be nice if the support for floats corresponded to that of what's allowed in SMT-Lib; except of course for upper bounds on exponent/precision sizes which are mandated by implementation restrictions. So far, I see no reason to limit the exponent size to be at least 3, other than that on lone constant in libbf.h which seems to be otherwise unused.)

[yav]

I a not sure, might be better to reach out the author of libBF? The restriction in Cryptol came directly from the constant in the source of libBF. I just looked at the source and don't see anything obvious that would preclude a 2 bit exponent, but it's quite possible that the constant documents some assumptions in the operations, and those would require a much closer inspection to know if things will always work with 2 bits.

[LeventErkok]

Good idea. I sent him an e-mail; let's see if he responds.

[LeventErkok]

This is what he said:

I had no clear reason to use BF_EXP_BITS_MIN = 3. So if "2" is OK then why not. The important is that the basic operations are OK. It is likely there are tricky cases in the transcendental operations but even with large exponents libbf may have problems with them !

Based on this, I'm inclined to start at '2' for SBV; not sure if there's any ROI for Cryptol to do the same or not. (Your LibBF binding doesn't export the transcendentals anyhow. They'd be useful for constant folding, but not much more since SMTLib doesn't support them anyway.)

[robdockins]

Agreed, it would be nice to support everything supported by the SMTLib2 standard. However, I'll note that, as a practical concern, I was having problems with the solvers themselves crashing when using small exponent sizes (less than about 5 for CVC4, if I recall) when doing some testing.

[LeventErkok]

I haven't seen many crashes with floats, though I mainly stick to z3 for testing purposes. I did see many "incorrect" answers over the years, but they're good at fixing them once reported.

One limitation z3 has with floats is that not all operations are supported when eb > sb. For instance, floating-point addition isn''t supported in eb > sb case. (see: https://github.com/Z3Prover/z3/issues/5051) Unfortunately which cases are supported/which aren't really well-documented. Hopefully they cover everything for the more-or-less standard sizes of half-single-double and quad floats. (All of which satisfy eb < sb.)