Fix handling of special Float values. Refs #697.

copilot-bluespec/CHANGELOG

@@ -1,3 +1,6 @@
+2026-03-31
+        * Fix translation of special Float values to Bluespec. (#697)
+
 2026-03-07
         * Version bump (4.7). (#714)
 

copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs

@@ -18,7 +18,7 @@ import Data.String (IsString (..))
 import qualified Language.Bluespec.Classic.AST as BS
 import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS
 import Numeric.Floating.IEEE.NaN (isSignaling, setPayloadSignaling, setPayload, getPayload)
-import GHC.Float (double2Float, castFloatToWord32, castDoubleToWord64)
+import GHC.Float (double2Float, castFloatToWord32, castDoubleToWord64, float2Double)
 
 -- Internal imports: Copilot
 import Copilot.Core
@@ -535,7 +535,7 @@ constTy ty =
     Word16    -> constInt ty . toInteger
     Word32    -> constInt ty . toInteger
     Word64    -> constInt ty . toInteger
-    Float     -> constFP ty . realToFrac
+    Float     -> constFP ty . nanSafeFloat2Double
     Double    -> constFP ty
 
     -- Translating a Copilot array literal to a Bluespec Vector is somewhat
@@ -563,6 +563,20 @@ constTy ty =
                , constTy ty'' val
                ))
              (toValues v))
+  where
+    -- Convert a Float to a Double. This function takes care to preserve
+    -- special floating-point values, such as negative zero, infinity, and NaN
+    -- values.
+    nanSafeFloat2Double :: Float -> Double
+    nanSafeFloat2Double x
+        -- float2Double does not preserve the payloads of NaN values, so we
+        -- include special cases for translating NaNs.
+        | isNaN x && isSignaling x = setPayloadSignaling payload
+        | isNaN x                  = setPayload payload
+        | otherwise                = float2Double x
+      where
+        payload :: Double
+        payload = float2Double $ getPayload x
 
 -- | Transform a list of Copilot Core expressions of a given 'Type' into a
 -- Bluespec @Vector@ expression.

copilot-theorem/CHANGELOG

@@ -1,3 +1,6 @@
+2026-03-31
+        * Handle special Float values correctly for counterexamples. (#697)
+
 2026-03-07
         * Version bump (4.7). (#714)
 

copilot-theorem/copilot-theorem.cabal

@@ -51,6 +51,7 @@ library
                           , containers            >= 0.4 && < 0.9
                           , data-default          >= 0.7 && < 0.9
                           , directory             >= 1.3 && < 1.4
+                          , fp-ieee               >= 0.1 && < 0.2
                           , libBF                 >= 0.6.2 && < 0.7
                           , mtl                   >= 2.0 && < 2.4
                           , panic                 >= 0.4.0 && < 0.5

copilot-theorem/src/Copilot/Theorem/What4.hs

@@ -77,8 +77,9 @@ import Data.Parameterized.NatRepr
 import Data.Parameterized.Nonce
 import Data.Parameterized.Some
 import qualified Data.Parameterized.Vector as V
-import GHC.Float (castWord32ToFloat, castWord64ToDouble)
+import GHC.Float (castWord32ToFloat, castWord64ToDouble, double2Float)
 import LibBF (BigFloat, bfToDouble, pattern NearEven)
+import Numeric.Floating.IEEE.NaN (getPayload, isSignaling, setPayload, setPayloadSignaling)
 import qualified Panic as Panic
 
 import Copilot.Theorem.What4.Translate
@@ -707,7 +708,7 @@ valFromExpr ge xe = case xe of
   XFloat e ->
     Some . CopilotValue CT.Float <$>
       iFloatGroundEval WFP.SingleFloatRepr e
-                       (realToFrac . fst . bfToDouble NearEven)
+                       (nanSafeDoubleToFloat . fst . bfToDouble NearEven)
                        fromRational
                        (castWord32ToFloat . fromInteger . BV.asUnsigned)
   XDouble e ->
@@ -757,3 +758,17 @@ valFromExpr ge xe = case xe of
         WB.FloatIEEERepr          -> ieeeK <$> WG.groundEval ge e
         WB.FloatRealRepr          -> realK <$> WG.groundEval ge e
         WB.FloatUninterpretedRepr -> uninterpK <$> WG.groundEval ge e
+
+    -- Convert a Double to a Float. This function takes care to preserve
+    -- special floating-point values, such as negative zero, infinity, and NaN
+    -- values.
+    nanSafeDoubleToFloat :: Double -> Float
+    nanSafeDoubleToFloat x
+        -- double2Float does not preserve the payloads of NaN values, so we
+        -- include a special case for translating NaNs.
+        | isNaN x && isSignaling x = setPayloadSignaling payload
+        | isNaN x                  = setPayload payload
+        | otherwise                = double2Float x
+      where
+        payload :: Float
+        payload = double2Float $ getPayload x