`:prove` incorrectly throws a runtime error when evaluating `fpToRational` using What4-based provers

[RyanGlScott]

fpToRational (0 : Float32) should be equal to (ratio 0 1). Cryptol's native and reference evaluators confirm this:

Cryptol> :m Float
Loading module Cryptol
Loading module Float
Float> fpToRational (0 : Float32) == (ratio 0 1)
True
Float> :eval fpToRational (0 : Float32) == (ratio 0 1)
True

If you ask the :prove command with a What4-based prover, however, it claims that evaluating this query will result in a runtime error:

Float> :set prover=w4-z3
Float> :prove fpToRational (0 : Float32) == (ratio 0 1)
Counterexample
(fpToRational (0 : Float32) == (ratio 0 1)) ~> ERROR
(Total Elapsed Time: 0.018s, using "Z3")

As far as I can tell, this is a bug. Strangely, this issue doesn't arise if you try the following, very similar :sat command:

Float> :sat \x -> fpToRational (0 : Float32) == x
Satisfiable
(\x -> fpToRational (0 : Float32) == x) (ratio 0 1) = True
(Total Elapsed Time: 0.021s, using "Z3")

[RyanGlScott]

I suspect the culprit is the implementation of fpToRational in What4.SFloat:

{- | Returns a predicate and two integers, @x@ and @y@.
If the the predicate holds, then @x / y@ is a rational representing
the floating point number. Assumes the FP number is not one of the
special ones that has no real representation. -}
fpToRational ::
  IsSymExprBuilder sym =>
  sym ->
  SFloat sym ->
  IO (Pred sym, SymInteger sym, SymInteger sym)
fpToRational sym fp =
  do r    <- fpToReal sym fp
     x    <- freshConstant sym emptySymbol BaseIntegerRepr
     y    <- freshConstant sym emptySymbol BaseIntegerRepr
     num  <- integerToReal sym x
     den  <- integerToReal sym y
     res  <- realDiv sym num den
     same <- realEq sym r res
     pure (same, x, y)

Given a floating-point value fp, this "converts" it to a rational value by creating two symbolic integers (x and y) and asserting that integerToReal x / integerToReal y is equal to fpToReal fp. Note, however, that y is completely unconstrained, which means that it is entirely possible that it could take on the value 0, leading to a division-by-zero error.

The following what4 patch (which enforces that the denominator must be positive) appears to fix the issue:

diff --git a/what4/src/What4/SFloat.hs b/what4/src/What4/SFloat.hs
index 8e76e671..a1ea005e 100644
--- a/what4/src/What4/SFloat.hs
+++ b/what4/src/What4/SFloat.hs
@@ -426,7 +426,7 @@ fpToRational ::
 fpToRational sym fp =
   do r    <- fpToReal sym fp
      x    <- freshConstant sym emptySymbol BaseIntegerRepr
-     y    <- freshConstant sym emptySymbol BaseIntegerRepr
+     y    <- freshBoundedInt sym emptySymbol (Just 1) Nothing
      num  <- integerToReal sym x
      den  <- integerToReal sym y
      res  <- realDiv sym num den

[RyanGlScott]

Better yet, fpToRational already returns a predicate that must be assumed in order for the overall rational to be valid. As such, we can add an additional assumption to this predicate that the denominator is non-zero. This should work just as well as using freshBoundedInt, and it should also be compatible with a future in which freshBoundedInt is reworked (or even removed), as discussed in GaloisInc/what4#360.

[RyanGlScott]

The underlying problem has been addressed on the what4 side in GaloisInc/what4#399. Once we upload a new what4 Hackage release with those changes and incorporate it into Cryptol, we should add a regression test using the program above and close this issue.