packages feed

grisette-0.11.0.0: test/Grisette/SymPrim/FPTests.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# HLINT ignore "Unused LANGUAGE pragma" #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

module Grisette.SymPrim.FPTests (fpTests) where

import Data.Foldable (traverse_)
import Data.Kind (Type)
import Data.Ratio ((%))
import Data.SBV (SMTResult (Satisfiable, Unsatisfiable))
import qualified Data.SBV as SBV
import Data.Serialize (decode, encode)
import Data.Word (Word32, Word64)
import GHC.TypeLits (KnownNat, Nat, type (<=))
import Grisette
  ( AlgReal (AlgExactRational),
    FP,
    FPRoundingMode (RTP),
    IEEEFPConstants
      ( fpMaxNormalized,
        fpMaxSubnormal,
        fpMinNormalized,
        fpMinSubnormal
      ),
    IEEEFPOp
      ( fpAbs,
        fpMaximum,
        fpMaximumNumber,
        fpMinimum,
        fpMinimumNumber,
        fpNeg,
        fpRem
      ),
    IEEEFPRoundingMode (rna, rne, rtn, rtp, rtz),
    IEEEFPRoundingOp
      ( fpAdd,
        fpDiv,
        fpFMA,
        fpMul,
        fpRoundToIntegral,
        fpSqrt,
        fpSub
      ),
    WordN,
    bitCastOrCanonical,
  )
import Grisette.Internal.Core.Data.Class.BitCast (BitCast (bitCast))
import Grisette.Internal.Core.Data.Class.IEEEFP
  ( IEEEFPConstants
      ( fpNaN,
        fpNegativeInfinite,
        fpNegativeZero,
        fpPositiveInfinite,
        fpPositiveZero
      ),
    IEEEFPConvertible (fromFPOr, toFP),
    fpIsNaN,
    fpIsNegativeInfinite,
    fpIsNegativeZero,
    fpIsPositiveInfinite,
    fpIsPositiveZero,
  )
import Grisette.Internal.Core.Data.Class.SafeFromFP (SafeFromFP (safeFromFP))
import Grisette.Internal.Core.Data.Class.SymIEEEFP
  ( SymIEEEFPTraits
      ( symFpIsInfinite,
        symFpIsNaN,
        symFpIsNegative,
        symFpIsNegativeInfinite,
        symFpIsNegativeZero,
        symFpIsNormal,
        symFpIsPoint,
        symFpIsPositive,
        symFpIsPositiveInfinite,
        symFpIsPositiveZero,
        symFpIsSubnormal,
        symFpIsZero
      ),
  )
import Grisette.Internal.SymPrim.BV (IntN)
import Grisette.Internal.SymPrim.FP
  ( ConvertibleBound (convertibleLowerBound, convertibleUpperBound),
    FP32,
    NotRepresentableFPError,
    ValidFP,
    nextFP,
    prevFP,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm
  ( genericFPCast,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( SupportedPrim (conSBVTerm),
  )
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.Framework.Providers.QuickCheck2 (testProperty)
import Test.HUnit (assertBool, (@?=))
import Test.QuickCheck (Arbitrary, ioProperty)
import Type.Reflection (Typeable, typeRep)

sameFP :: forall a b. (RealFloat a, RealFloat b) => a -> b -> Bool
sameFP x y
  | isNaN x && isNaN y = True
  | isInfinite x && isInfinite y =
      (x < 0 && y < 0) || (x > 0 && y > 0)
  -- \| GHC's floating point support doesn't conform to IEEE754.
  | otherwise = (uncurry encodeFloat (decodeFloat x) :: b) == y

fp32ConversionTest :: (Word32 -> IO ()) -> [Test]
fp32ConversionTest testFun =
  [ testProperty "property" $ ioProperty . testFun,
    testCase "NaN" $ testFun 0x7f800100,
    testCase "+inf" $ testFun 0x7f800000,
    testCase "-inf" $ testFun 0xFf800000,
    testCase "0" $ testFun 0,
    testCase "-0" $ testFun 0x80000000
  ]

fp64ConversionTest :: (Word64 -> IO ()) -> [Test]
fp64ConversionTest testFun =
  [ testProperty "property" $ ioProperty . testFun,
    testCase "NaN" $ testFun 0x7ff8000010000000,
    testCase "+inf" $ testFun 0x7FF0000000000000,
    testCase "-inf" $ testFun 0xFFF0000000000000,
    testCase "0" $ testFun 0,
    testCase "-0" $ testFun 0x8000000000000000
  ]

unaryOpComplianceWithFloat ::
  String ->
  (FP32 -> a) ->
  (Float -> b) ->
  (a -> b -> Bool) ->
  Test
unaryOpComplianceWithFloat name fpOp floatOp cmp =
  testProperty name $ \x ->
    let x' = bitCastOrCanonical x
        actual = fpOp x
        expected = floatOp x'
     in cmp actual expected

binOpComplianceWithFloat ::
  String ->
  (FP32 -> FP32 -> a) ->
  (Float -> Float -> b) ->
  (a -> b -> Bool) ->
  Test
binOpComplianceWithFloat name fpOp floatOp cmp =
  testProperty name $ \x y ->
    let x' = bitCastOrCanonical x
        y' = bitCastOrCanonical y
        actual = fpOp x y
        expected = floatOp x' y'
     in cmp actual expected

fpTests :: Test
fpTests =
  testGroup
    "FP"
    [ testGroup
        "bitcast"
        [ testGroup "WordN -> FP" $
            fp32ConversionTest $ \(x :: Word32) -> do
              let fp = bitCast x :: FP32
              let float = bitCast x :: Float
              assertBool "Must be the same FP" $ sameFP fp float,
          testGroup "FP -> WordN" $ do
            fp32ConversionTest $ \(x :: Word32) -> do
              let fp = bitCast x :: FP32
              let regulated =
                    if isNaN fp
                      then 0x7fc00000
                      else bitCastOrCanonical fp :: WordN 32
              let actual = bitCastOrCanonical (bitCast regulated :: FP32)
              actual @?= regulated
        ],
      testGroup
        "Eq"
        [ binOpComplianceWithFloat "==" (==) (==) (==),
          binOpComplianceWithFloat "/=" (/=) (/=) (==)
        ],
      testGroup
        "Ord"
        [ binOpComplianceWithFloat "<" (<) (<) (==),
          binOpComplianceWithFloat "<=" (<=) (<=) (==),
          binOpComplianceWithFloat ">" (>) (>) (==),
          binOpComplianceWithFloat ">=" (>=) (>=) (==)
        ],
      testGroup
        "Num"
        [ binOpComplianceWithFloat "+" (+) (+) sameFP,
          binOpComplianceWithFloat "-" (-) (-) sameFP,
          binOpComplianceWithFloat "*" (*) (*) sameFP,
          unaryOpComplianceWithFloat "negate" negate negate sameFP,
          unaryOpComplianceWithFloat "abs" abs abs sameFP,
          unaryOpComplianceWithFloat "signum" signum signum sameFP,
          testProperty "fromInteger" $ \x ->
            let fp = fromInteger x :: FP32
                float = fromInteger x :: Float
             in sameFP fp float
        ],
      testCase "Lift" $ do
        let x = bitCast (0x12345678 :: WordN 32) :: FP32
        $$([||x||]) @?= x,
      testGroup
        "Fractional"
        [ binOpComplianceWithFloat "/" (/) (/) sameFP,
          unaryOpComplianceWithFloat "recip" recip recip sameFP,
          testProperty "fromRational" $ \x ->
            let fp = fromRational x :: FP32
                float = fromRational x :: Float
             in sameFP fp float
        ],
      testGroup
        "Floating"
        [ -- Only the following operations are supported in SBV
          unaryOpComplianceWithFloat "sqrt" sqrt sqrt sameFP,
          binOpComplianceWithFloat "(**)" (**) (**) sameFP
        ],
      -- Real instantce is not compliant with Float.
      -- testGroup
      --   "Real"
      --   [ unaryOpComplianceWithFloat "toRational" toRational toRational (==)
      --   ]
      -- RealFrac instance is not compliant with Float.
      -- testGroup
      --   "RealFrac"
      --   [ unaryOpComplianceWithFloat
      --       "truncate"
      --       truncate
      --       truncate
      --       ((==) @Integer),
      --     unaryOpComplianceWithFloat "round" round round ((==) @Integer),
      --     unaryOpComplianceWithFloat "ceiling" ceiling ceiling ((==) @Integer),
      --     unaryOpComplianceWithFloat "floor" floor floor ((==) @Integer)
      --   ]
      testGroup
        "RealFloat"
        [ unaryOpComplianceWithFloat "floatRadix" floatRadix floatRadix (==),
          unaryOpComplianceWithFloat "floatDigits" floatDigits floatDigits (==),
          unaryOpComplianceWithFloat "floatRange" floatRange floatRange (==),
          -- decodeFloat is not compliant with Float
          -- unaryOpComplianceWithFloat "decodeFloat" decodeFloat decodeFloat (==)
          -- encodeFloat isn't tested
          -- exponent is not compliant with Float
          -- unaryOpComplianceWithFloat "exponent" exponent exponent (==)
          -- significand is not compliant with Float
          -- unaryOpComplianceWithFloat "significand" significand significand sameFP
          testProperty "scaleFloat" $ \i (x :: FP32) ->
            let x' = bitCastOrCanonical x :: Float
                actual = scaleFloat i x
                expected = scaleFloat i x'
             in sameFP actual expected,
          testProperty "isNaN" $ \(x :: FP32) ->
            let x' = bitCastOrCanonical x :: Float
             in isNaN x == isNaN x',
          unaryOpComplianceWithFloat "isInfinite" isInfinite isInfinite (==),
          unaryOpComplianceWithFloat
            "isDenormalized"
            isDenormalized
            isDenormalized
            (==),
          unaryOpComplianceWithFloat
            "isNegativeZero"
            isNegativeZero
            isNegativeZero
            (==),
          unaryOpComplianceWithFloat "isIEEE" isIEEE isIEEE (==) -- ,
          -- atan2 is not supported
          -- binOpComplianceWithFloat "atan2" atan2 atan2 sameFP
        ],
      testGroup
        "SymIEEEFPTraits"
        [ unaryOpComplianceWithFloat "symFpIsNaN" symFpIsNaN symFpIsNaN (==),
          unaryOpComplianceWithFloat
            "symFpIsPositive"
            symFpIsPositive
            symFpIsPositive
            (==),
          unaryOpComplianceWithFloat
            "symFpIsNegative"
            symFpIsNegative
            symFpIsNegative
            (==),
          unaryOpComplianceWithFloat
            "symFpIsPositiveInfinite"
            symFpIsPositiveInfinite
            symFpIsPositiveInfinite
            (==),
          unaryOpComplianceWithFloat
            "symFpIsNegativeInfinite"
            symFpIsNegativeInfinite
            symFpIsNegativeInfinite
            (==),
          unaryOpComplianceWithFloat
            "symFpIsInfinite"
            symFpIsInfinite
            symFpIsInfinite
            (==),
          unaryOpComplianceWithFloat
            "symFpIsPositiveZero"
            symFpIsPositiveZero
            symFpIsPositiveZero
            (==),
          unaryOpComplianceWithFloat
            "symFpIsNegativeZero"
            symFpIsNegativeZero
            symFpIsNegativeZero
            (==),
          unaryOpComplianceWithFloat "symFpIsZero" symFpIsZero symFpIsZero (==),
          unaryOpComplianceWithFloat
            "symFpIsNormal"
            symFpIsNormal
            symFpIsNormal
            (==),
          unaryOpComplianceWithFloat
            "symFpIsSubnormal"
            symFpIsSubnormal
            symFpIsSubnormal
            (==),
          unaryOpComplianceWithFloat
            "symFpIsPoint"
            symFpIsPoint
            symFpIsPoint
            (==)
        ],
      testGroup
        "IEEEFPConstants"
        [ testCase "fpPositiveInfinite" $
            fpIsPositiveInfinite (fpPositiveInfinite :: FP32) @?= True,
          testCase "fpNegativeInfinite" $
            fpIsNegativeInfinite (fpNegativeInfinite :: FP32) @?= True,
          testCase "fpNaN" $
            fpIsNaN (fpNaN :: FP32) @?= True,
          testCase "fpPositiveZero" $
            fpIsPositiveZero (fpPositiveZero :: FP32) @?= True,
          testCase "fpNegativeZero" $
            fpIsNegativeZero (fpNegativeZero :: FP32) @?= True,
          testCase "fpMinNormalized" $
            fpMinNormalized @?= (1.5625e-2 :: FP 4 4),
          testCase "fpMaxNormalized" $
            fpMaxNormalized @?= (2.4e2 :: FP 4 4),
          testCase "fpMinSubnormal" $
            fpMinSubnormal @?= (1.953125e-3 :: FP 4 4),
          testCase "fpMaxSubnormal" $
            fpMaxSubnormal @?= (1.3671875e-2 :: FP 4 4)
        ],
      testGroup
        "IEEEFPOp"
        [ testCase "fpAbs" $ do
            SameFPObj (fpAbs (0 :: FP32)) @?= 0
            SameFPObj (fpAbs (fpNegativeZero :: FP32)) @?= 0
            SameFPObj (fpAbs (fpPositiveInfinite :: FP32))
              @?= fpPositiveInfinite
            SameFPObj (fpAbs (fpNegativeInfinite :: FP32))
              @?= fpPositiveInfinite
            SameFPObj (fpAbs (1 :: FP32)) @?= 1
            SameFPObj (fpAbs (-1 :: FP32)) @?= 1
            SameFPObj (fpAbs (fpNaN :: FP32)) @?= fpNaN,
          testCase "fpNeg" $ do
            SameFPObj (fpNeg (0 :: FP32)) @?= -0
            SameFPObj (fpNeg (fpNegativeZero :: FP32)) @?= 0
            SameFPObj (fpNeg (fpPositiveInfinite :: FP32))
              @?= fpNegativeInfinite
            SameFPObj (fpNeg (fpNegativeInfinite :: FP32))
              @?= fpPositiveInfinite
            SameFPObj (fpNeg (1 :: FP32)) @?= -1
            SameFPObj (fpNeg (-1 :: FP32)) @?= 1
            SameFPObj (fpNeg (fpNaN :: FP32)) @?= fpNaN,
          testGroup
            "fpRem"
            [ testCase "inf or nan / x" $ do
                let lhs =
                      [fpPositiveInfinite :: FP32, fpNegativeInfinite, fpNaN]
                let rhs =
                      [ 0,
                        -0,
                        1,
                        -1,
                        fpPositiveInfinite,
                        fpNegativeInfinite,
                        fpNaN
                      ]
                traverse_ (\(l, r) -> SameFPObj (fpRem l r) @?= fpNaN) $
                  zip lhs rhs,
              testCase "0 / neither 0 nor nan" $ do
                let lhs = [fpPositiveZero :: FP32, fpNegativeZero]
                let rhs =
                      [1, -1, fpPositiveInfinite, fpNegativeInfinite]
                traverse_ (\(l, r) -> SameFPObj (fpRem l r) @?= SameFPObj l) $
                  [(l, r) | l <- lhs, r <- rhs],
              testCase "0 / 0 or nan" $ do
                let lhs = [fpPositiveZero :: FP32, fpNegativeZero]
                let rhs = [fpPositiveZero, fpNegativeZero, fpNaN]
                traverse_ (\(l, r) -> SameFPObj (fpRem l r) @?= fpNaN) $
                  [(l, r) | l <- lhs, r <- rhs],
              testCase "normal" $ do
                SameFPObj (fpRem (5 :: FP32) 4) @?= 1
                SameFPObj (fpRem (6 :: FP32) 4) @?= -2
                SameFPObj (fpRem (7 :: FP32) 4) @?= -1
                SameFPObj (fpRem (8 :: FP32) 4) @?= 0
                SameFPObj (fpRem (9 :: FP32) 4) @?= 1
                SameFPObj (fpRem (10 :: FP32) 4) @?= 2
            ],
          testCase "fpMinimum" $ do
            SameFPObj (fpMinimum (0 :: FP32) 0) @?= 0
            SameFPObj (fpMinimum (0 :: FP32) (-0)) @?= -0
            SameFPObj (fpMinimum (-0 :: FP32) 0) @?= -0
            SameFPObj (fpMinimum (-0 :: FP32) (-0)) @?= -0
            SameFPObj (fpMinimum (fpNaN :: FP32) fpNaN) @?= fpNaN
            SameFPObj (fpMinimum (fpNaN :: FP32) 1) @?= fpNaN
            SameFPObj (fpMinimum (1 :: FP32) fpNaN) @?= fpNaN
            SameFPObj (fpMinimum (fpNaN :: FP32) fpPositiveInfinite) @?= fpNaN
            SameFPObj (fpMinimum (fpNegativeInfinite :: FP32) fpNaN) @?= fpNaN
            SameFPObj (fpMinimum (1 :: FP32) 2) @?= 1,
          testCase "fpMinimumNumber" $ do
            SameFPObj (fpMinimumNumber (0 :: FP32) 0) @?= 0
            SameFPObj (fpMinimumNumber (0 :: FP32) (-0)) @?= -0
            SameFPObj (fpMinimumNumber (-0 :: FP32) 0) @?= -0
            SameFPObj (fpMinimumNumber (-0 :: FP32) (-0)) @?= -0
            SameFPObj (fpMinimumNumber (fpNaN :: FP32) fpNaN) @?= fpNaN
            SameFPObj (fpMinimumNumber (fpNaN :: FP32) 1) @?= 1
            SameFPObj (fpMinimumNumber (1 :: FP32) fpNaN) @?= 1
            SameFPObj (fpMinimumNumber (fpNaN :: FP32) fpPositiveInfinite)
              @?= fpPositiveInfinite
            SameFPObj (fpMinimumNumber (fpNegativeInfinite :: FP32) fpNaN)
              @?= fpNegativeInfinite
            SameFPObj (fpMinimumNumber (1 :: FP32) 2) @?= 1,
          testCase "fpMaximum" $ do
            SameFPObj (fpMaximum (0 :: FP32) 0) @?= 0
            SameFPObj (fpMaximum (0 :: FP32) (-0)) @?= 0
            SameFPObj (fpMaximum (-0 :: FP32) 0) @?= 0
            SameFPObj (fpMaximum (-0 :: FP32) (-0)) @?= -0
            SameFPObj (fpMaximum (fpNaN :: FP32) fpNaN) @?= fpNaN
            SameFPObj (fpMaximum (fpNaN :: FP32) 1) @?= fpNaN
            SameFPObj (fpMaximum (1 :: FP32) fpNaN) @?= fpNaN
            SameFPObj (fpMaximum (fpNaN :: FP32) fpPositiveInfinite) @?= fpNaN
            SameFPObj (fpMaximum (fpNegativeInfinite :: FP32) fpNaN) @?= fpNaN
            SameFPObj (fpMaximum (1 :: FP32) 2) @?= 2,
          testCase "fpMaximumNumber" $ do
            SameFPObj (fpMaximumNumber (0 :: FP32) 0) @?= 0
            SameFPObj (fpMaximumNumber (0 :: FP32) (-0)) @?= 0
            SameFPObj (fpMaximumNumber (-0 :: FP32) 0) @?= 0
            SameFPObj (fpMaximumNumber (-0 :: FP32) (-0)) @?= -0
            SameFPObj (fpMaximumNumber (fpNaN :: FP32) fpNaN) @?= fpNaN
            SameFPObj (fpMaximumNumber (fpNaN :: FP32) 1) @?= 1
            SameFPObj (fpMaximumNumber (1 :: FP32) fpNaN) @?= 1
            SameFPObj (fpMaximumNumber (fpNaN :: FP32) fpPositiveInfinite)
              @?= fpPositiveInfinite
            SameFPObj (fpMaximumNumber (fpNegativeInfinite :: FP32) fpNaN)
              @?= fpNegativeInfinite
            SameFPObj (fpMaximumNumber (1 :: FP32) 2) @?= 2
        ],
      testGroup
        "IEEEFPRoundingOp"
        [ testCase "unop nan" $ do
            let op = [fpRoundToIntegral, fpSqrt]
            let roundingMode = [rne, rna, rtz, rtn, rtp]
            traverse_ (\(o, rd) -> SameFPObj (o rd fpNaN) @?= fpNaN) $
              [(op, rd) | op <- op, rd <- roundingMode],
          testCase "binop nan" $ do
            let op = [fpAdd, fpSub, fpMul, fpDiv]
            let roundingMode = [rne, rna, rtz, rtn, rtp]
            let operands =
                  [(fpNaN :: FP32, 1 :: FP32), (1, fpNaN), (fpNaN, fpNaN)]
            traverse_ (\(o, r, (a, b)) -> SameFPObj (o r a b) @?= fpNaN) $
              [(o, r, (a, b)) | o <- op, r <- roundingMode, (a, b) <- operands],
          testCase "ternop nan" $ do
            let op = [fpFMA]
            let roundingMode = [rne, rna, rtz, rtn, rtp]
            let operand = [fpNaN :: FP32, 1]
            let operands =
                  [ (a, b, c)
                    | a <- operand,
                      b <- operand,
                      c <- operand,
                      fpIsNaN a || fpIsNaN b || fpIsNaN c
                  ]
            traverse_ (\(o, r, (a, b, c)) -> SameFPObj (o r a b c) @?= fpNaN) $
              [ (o, r, (a, b, c))
                | o <- op,
                  r <- roundingMode,
                  (a, b, c) <- operands
              ],
          testCase "fpAdd" $ do
            let v = 60 :: FP 4 4
            fpAdd rne 2 v @?= 64
            fpAdd rna 2 v @?= 64
            fpAdd rne (-2) v @?= 56
            fpAdd rna (-2) v @?= 60
            fpAdd rtz 2 v @?= 60
            fpAdd rtn 2 v @?= 60
            fpAdd rtp 2 v @?= 64
            fpAdd rne (-2) (-v) @?= -64
            fpAdd rna (-2) (-v) @?= -64
            fpAdd rtz (-2) (-v) @?= -60
            fpAdd rtn (-2) (-v) @?= -64
            fpAdd rtp (-2) (-v) @?= -60
            fpAdd rne 1 v @?= 60
            fpAdd rna 1 v @?= 60
            fpAdd rtz 1 v @?= 60
            fpAdd rtn 1 v @?= 60
            fpAdd rtp 1 v @?= 64
            fpAdd rne (-1) (-v) @?= -60
            fpAdd rna (-1) (-v) @?= -60
            fpAdd rtz (-1) (-v) @?= -60
            fpAdd rtn (-1) (-v) @?= -64
            fpAdd rtp (-1) (-v) @?= -60
            fpAdd rne 3 v @?= 64
            fpAdd rna 3 v @?= 64
            fpAdd rtz 3 v @?= 60
            fpAdd rtn 3 v @?= 60
            fpAdd rtp 3 v @?= 64
            fpAdd rne (-3) (-v) @?= -64
            fpAdd rna (-3) (-v) @?= -64
            fpAdd rtz (-3) (-v) @?= -60
            fpAdd rtn (-3) (-v) @?= -64
            fpAdd rtp (-3) (-v) @?= -60
        ],
      testGroup "ConvertibleBound" $ do
        let test ::
              forall n eb sb.
              ( ValidFP eb sb,
                KnownNat n,
                1 <= n,
                SBV.BVIsNonZero n
              ) =>
              Test
            test =
              testGroup
                ( "n="
                    <> show (typeRep @n)
                    <> ",eb="
                    <> show (typeRep @eb)
                    <> ",sb="
                    <> show (typeRep @sb)
                )
                $ do
                  let tcase ::
                        forall (bv :: Nat -> Type) (sbvbv :: Nat -> Type).
                        ( ConvertibleBound bv,
                          Num (bv n),
                          SBV.SymVal (sbvbv n),
                          Num (SBV.SBV (sbvbv n)),
                          Typeable bv
                        ) =>
                        Test
                      tcase = testCase (show $ typeRep @bv) $ do
                        let lb =
                              convertibleLowerBound (0 :: bv n) RTP :: FP eb sb
                        let rb =
                              convertibleUpperBound (0 :: bv n) RTP :: FP eb sb
                        let lbad = prevFP lb
                        let rbad = nextFP rb
                        let sbvlb = conSBVTerm lb
                        let sbvrb = conSBVTerm rb
                        let sbvlbad = conSBVTerm lbad
                        let sbvrbad = conSBVTerm rbad
                        let sbvlbbv =
                              genericFPCast SBV.sRTP sbvlb :: SBV.SBV (sbvbv n)
                        let sbvrbbv =
                              genericFPCast SBV.sRTP sbvrb :: SBV.SBV (sbvbv n)
                        let sbvlbadbv =
                              genericFPCast
                                SBV.sRTP
                                sbvlbad ::
                                SBV.SBV (sbvbv n)
                        let sbvrbadbv =
                              genericFPCast
                                SBV.sRTP
                                sbvrbad ::
                                SBV.SBV (sbvbv n)
                        SBV.SatResult (Unsatisfiable {}) <-
                          SBV.sat (sbvlbbv SBV..== 1)
                        SBV.SatResult (Unsatisfiable {}) <-
                          SBV.sat (sbvrbbv SBV..== 1)
                        SBV.SatResult (Satisfiable {}) <-
                          SBV.sat (sbvlbadbv SBV..== 1)
                        SBV.SatResult (Satisfiable {}) <-
                          SBV.sat (sbvrbadbv SBV..== 1)
                        return ()
                  [tcase @IntN @SBV.IntN, tcase @WordN @SBV.WordN]
        [ test @12 @4 @16,
          test @12 @4 @14,
          test @12 @4 @13,
          test @12 @4 @12,
          test @12 @4 @11,
          test @12 @4 @10,
          test @12 @4 @9,
          test @12 @4 @2,
          test @10 @4 @16,
          test @10 @4 @12,
          test @10 @4 @11,
          test @10 @4 @10,
          test @10 @4 @9,
          test @10 @4 @8,
          test @10 @4 @7,
          test @10 @4 @2,
          test @9 @4 @16,
          test @9 @4 @11,
          test @9 @4 @10,
          test @9 @4 @9,
          test @9 @4 @8,
          test @9 @4 @7,
          test @9 @4 @6,
          test @9 @4 @2,
          test @8 @4 @16,
          test @8 @4 @10,
          test @8 @4 @9,
          test @8 @4 @8,
          test @8 @4 @7,
          test @8 @4 @6,
          test @8 @4 @5,
          test @8 @4 @2,
          test @7 @4 @16,
          test @7 @4 @9,
          test @7 @4 @8,
          test @7 @4 @7,
          test @7 @4 @6,
          test @7 @4 @5,
          test @7 @4 @3,
          test @7 @4 @2,
          test @6 @4 @16,
          test @6 @4 @8,
          test @6 @4 @7,
          test @6 @4 @6,
          test @6 @4 @5,
          test @6 @4 @3,
          test @6 @4 @2,
          test @5 @4 @16,
          test @5 @4 @7,
          test @5 @4 @6,
          test @5 @4 @5,
          test @5 @4 @3,
          test @5 @4 @2
          ],
      testGroup "IEEEFPConvertible" $ do
        let safeFromFPComplianceTest ::
              forall v.
              ( Show v,
                Eq v,
                Arbitrary v,
                SafeFromFP
                  NotRepresentableFPError
                  v
                  (FP 4 4)
                  FPRoundingMode
                  (Either NotRepresentableFPError)
              ) =>
              Test
            safeFromFPComplianceTest = testProperty "safeFromFP" $
              \(d :: v) (md :: FPRoundingMode) (v :: FP 4 4) -> do
                let s = safeFromFP md v :: Either NotRepresentableFPError v
                case s of
                  Left _ -> fromFPOr d md v == d
                  Right r -> fromFPOr d md v == r
        [ testGroup
            "AlgReal"
            [ testCase "fromFPOr" $ do
                fromFPOr (1 :: AlgReal) rne (fpPositiveZero :: FP 4 4) @?= 0
                fromFPOr (1 :: AlgReal) rne (fpNegativeZero :: FP 4 4) @?= 0
                fromFPOr (1 :: AlgReal) rne (fpPositiveInfinite :: FP 4 4) @?= 1
                fromFPOr (1 :: AlgReal) rne (fpNegativeInfinite :: FP 4 4) @?= 1
                fromFPOr (1 :: AlgReal) rne (fpNaN :: FP 4 4) @?= 1
                fromFPOr (1 :: AlgReal) rne (3.75 :: FP 4 4)
                  @?= AlgExactRational (15 % 4),
              safeFromFPComplianceTest @AlgReal,
              testCase "toFP" $ do
                toFP rne (AlgExactRational (15 % 4)) @?= (3.75 :: FP 4 4)
                toFP rne (AlgExactRational (15 % 8)) @?= (1.875 :: FP 4 4)
                toFP rne (AlgExactRational (17 % 8)) @?= (2 :: FP 4 4)
                toFP rna (AlgExactRational (17 % 8)) @?= (2.25 :: FP 4 4)
                toFP rtz (AlgExactRational (17 % 8)) @?= (2 :: FP 4 4)
                toFP rtp (AlgExactRational (17 % 8)) @?= (2.25 :: FP 4 4)
                toFP rtn (AlgExactRational (17 % 8)) @?= (2 :: FP 4 4)

                toFP rne (AlgExactRational (-(17 % 8))) @?= (-2 :: FP 4 4)
                toFP rna (AlgExactRational (-(17 % 8))) @?= (-2.25 :: FP 4 4)
                toFP rtz (AlgExactRational (-(17 % 8))) @?= (-2 :: FP 4 4)
                toFP rtp (AlgExactRational (-(17 % 8))) @?= (-2 :: FP 4 4)
                toFP rtn (AlgExactRational (-(17 % 8))) @?= (-2.25 :: FP 4 4)
            ],
          testGroup "FP" $ do
            let tcase name func = testCase name $ do
                  mapM_
                    ( \rm -> do
                        assertBool "+0" $
                          fpIsPositiveZero
                            (func rm (fpPositiveZero :: FP 6 6) :: FP 4 4)
                        assertBool "-0" $
                          fpIsNegativeZero (func rm (fpNegativeZero :: FP 6 6))
                        assertBool "+oo" $
                          fpIsPositiveInfinite
                            (func rm (fpPositiveInfinite :: FP 6 6))
                        assertBool "-oo" $
                          fpIsNegativeInfinite
                            (func rm (fpNegativeInfinite :: FP 6 6))
                        assertBool "nan" $
                          fpIsNaN (func rm (fpNaN :: FP 6 6))
                    )
                    [rna, rne, rtz, rtn, rtp]
                  let posfps = (/ 16) . fromIntegral <$> [48 .. 56] :: [FP 6 6]
                  let fps = (negate <$> posfps) <> posfps
                  let rnaExpected =
                        [3, 3, 3.25, 3.25, 3.25, 3.25, 3.5, 3.5, 3.5]
                  func rna <$> fps @?= (negate <$> rnaExpected) <> rnaExpected
                  let rneExpected =
                        [3, 3, 3, 3.25, 3.25, 3.25, 3.5, 3.5, 3.5]
                  func rne <$> fps @?= (negate <$> rneExpected) <> rneExpected
                  let rtzExpected =
                        [3, 3, 3, 3, 3.25, 3.25, 3.25, 3.25, 3.5]
                  func rtz <$> fps @?= (negate <$> rtzExpected) <> rtzExpected
                  let rtnExpected =
                        [3, 3, 3, 3, 3.25, 3.25, 3.25, 3.25, 3.5]
                  let rtpExpected =
                        [3, 3.25, 3.25, 3.25, 3.25, 3.5, 3.5, 3.5, 3.5]
                  func rtn <$> fps @?= (negate <$> rtpExpected) <> rtnExpected
                  func rtp <$> fps @?= (negate <$> rtnExpected) <> rtpExpected
            [ tcase "fromFPOr" (fromFPOr 2),
              tcase "toFP" toFP
              ],
          testGroup "Integrals" $ do
            let fps = (/ 4) . fromIntegral <$> [-7 .. 7] :: [FP 4 4]
            let rneFromExpected :: (Num a) => [a]
                rneFromExpected =
                  [-2, -2, -1, -1, -1, 0, 0, 0, 0, 0, 1, 1, 1, 2, 2]
                rnaFromExpected :: (Num a) => [a]
                rnaFromExpected =
                  [-2, -2, -1, -1, -1, -1, 0, 0, 0, 1, 1, 1, 1, 2, 2]
                rtpFromExpected :: (Num a) => [a]
                rtpFromExpected =
                  [-1, -1, -1, -1, 0, 0, 0, 0, 1, 1, 1, 1, 2, 2, 2]
                rtnFromExpected :: (Num a) => [a]
                rtnFromExpected =
                  [-2, -2, -2, -1, -1, -1, -1, 0, 0, 0, 0, 1, 1, 1, 1]
                rtzFromExpected :: (Num a) => [a]
                rtzFromExpected =
                  [-1, -1, -1, -1, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1]
            let posints :: (Num a, Enum a) => [a]
                posints = [30 .. 40]
                ints :: (Num a, Enum a) => [a]
                ints = (negate <$> posints) <> posints
            let rnePosToFPExpected =
                  [30 :: FP 4 4, 32, 32, 32, 32, 36, 36, 36, 40, 40, 40]
            let rnaPosToFPExpected =
                  [30 :: FP 4 4, 32, 32, 32, 36, 36, 36, 36, 40, 40, 40]
            let rtzPosToFPExpected =
                  [30 :: FP 4 4, 30, 32, 32, 32, 32, 36, 36, 36, 36, 40]
            let rtnPosToFPExpected =
                  [30 :: FP 4 4, 30, 32, 32, 32, 32, 36, 36, 36, 36, 40]
            let rtpPosToFPExpected =
                  [30 :: FP 4 4, 32, 32, 36, 36, 36, 36, 40, 40, 40, 40]
            let rneToFPExpected =
                  fmap negate rnePosToFPExpected <> rnePosToFPExpected
            let rnaToFPExpected =
                  fmap negate rnaPosToFPExpected <> rnaPosToFPExpected
            let rtzToFPExpected =
                  fmap negate rtzPosToFPExpected <> rtzPosToFPExpected
            let rtnToFPExpected =
                  fmap negate rtpPosToFPExpected <> rtnPosToFPExpected
            let rtpToFPExpected =
                  fmap negate rtnPosToFPExpected <> rtpPosToFPExpected

            let boundTest0 ::
                  forall bv n eb sb.
                  ( ValidFP eb sb,
                    KnownNat n,
                    1 <= n,
                    ConvertibleBound bv,
                    IEEEFPConvertible (bv n) (FP eb sb) FPRoundingMode,
                    Eq (bv n),
                    Show (bv n)
                  ) =>
                  String ->
                  bv n ->
                  [bv n] ->
                  [bv n] ->
                  Test
                boundTest0 name d lbvs rbvs = testGroup name $ do
                  (rm, lbv, rbv) <- zip3 [rne, rna, rtz, rtn, rtp] lbvs rbvs
                  return $ testCase (show rm) $ do
                    let (lb :: FP eb sb) = convertibleLowerBound d rm
                    let (rb :: FP eb sb) = convertibleUpperBound d rm
                    let lbad = prevFP lb
                    let rbad = nextFP rb
                    fromFPOr d rm lbad @?= d
                    fromFPOr d rm rbad @?= d
                    fromFPOr d rm lb @?= lbv
                    fromFPOr d rm rb @?= rbv
            let boundTest ::
                  forall bv n eb sb.
                  ( ValidFP eb sb,
                    KnownNat n,
                    1 <= n,
                    ConvertibleBound bv,
                    IEEEFPConvertible (bv n) (FP eb sb) FPRoundingMode,
                    Eq (bv n),
                    Show (bv n)
                  ) =>
                  String ->
                  bv n ->
                  bv n ->
                  bv n ->
                  Test
                boundTest name d lbv rbv =
                  boundTest0 @bv @n @eb @sb
                    name
                    d
                    (replicate 5 lbv)
                    (replicate 5 rbv)

            [ testGroup
                "Integer"
                [ testCase "fromFPOr" $ do
                    fromFPOr (1 :: Integer) rne (fpPositiveZero :: FP 4 4) @?= 0
                    fromFPOr (1 :: Integer) rne (fpNegativeZero :: FP 4 4) @?= 0
                    fromFPOr (1 :: Integer) rne (fpPositiveInfinite :: FP 4 4)
                      @?= 1
                    fromFPOr (1 :: Integer) rne (fpNegativeInfinite :: FP 4 4)
                      @?= 1
                    fromFPOr (1 :: Integer) rne (fpNaN :: FP 4 4) @?= 1
                    fromFPOr (100 :: Integer) rne <$> fps @?= rneFromExpected
                    fromFPOr (100 :: Integer) rna <$> fps @?= rnaFromExpected
                    fromFPOr (100 :: Integer) rtp <$> fps @?= rtpFromExpected
                    fromFPOr (100 :: Integer) rtn <$> fps @?= rtnFromExpected
                    fromFPOr (100 :: Integer) rtz <$> fps @?= rtzFromExpected,
                  safeFromFPComplianceTest @Integer,
                  testCase "toFP" $ do
                    toFP rne (15 :: Integer) @?= (15 :: FP 4 4)
                    toFP rne <$> (ints :: [Integer]) @?= rneToFPExpected
                    toFP rna <$> (ints :: [Integer]) @?= rnaToFPExpected
                    toFP rtz <$> (ints :: [Integer]) @?= rtzToFPExpected
                    toFP rtn <$> (ints :: [Integer]) @?= rtnToFPExpected
                    toFP rtp <$> (ints :: [Integer]) @?= rtpToFPExpected
                ],
              testGroup
                "IntN"
                [ testCase "fromFPOr" $ do
                    fromFPOr (1 :: IntN 32) rne (fpPositiveZero :: FP 4 4) @?= 0
                    fromFPOr (1 :: IntN 32) rne (fpNegativeZero :: FP 4 4) @?= 0
                    fromFPOr (1 :: IntN 32) rne (fpPositiveInfinite :: FP 4 4)
                      @?= 1
                    fromFPOr (1 :: IntN 32) rne (fpNegativeInfinite :: FP 4 4)
                      @?= 1
                    fromFPOr (1 :: IntN 32) rne (fpNaN :: FP 4 4) @?= 1
                    fromFPOr (100 :: IntN 32) rne <$> fps @?= rneFromExpected
                    fromFPOr (100 :: IntN 32) rna <$> fps @?= rnaFromExpected
                    fromFPOr (100 :: IntN 32) rtp <$> fps @?= rtpFromExpected
                    fromFPOr (100 :: IntN 32) rtn <$> fps @?= rtnFromExpected
                    fromFPOr (100 :: IntN 32) rtz <$> fps @?= rtzFromExpected
                    fromFPOr (0 :: IntN 3) rne (-3.5 :: FP 4 4) @?= -4
                    fromFPOr (0 :: IntN 3) rne (3.5 :: FP 4 4) @?= 0
                    fromFPOr (0 :: IntN 3) rna (-3.5 :: FP 4 4) @?= -4
                    fromFPOr (0 :: IntN 3) rna (3.5 :: FP 4 4) @?= 0
                    fromFPOr (0 :: IntN 3) rne (-4.5 :: FP 4 4) @?= -4
                    fromFPOr (0 :: IntN 3) rne (4.5 :: FP 4 4) @?= 0
                    fromFPOr (0 :: IntN 3) rna (-4.5 :: FP 4 4) @?= 0
                    fromFPOr (0 :: IntN 3) rna (4.5 :: FP 4 4) @?= 0,
                  safeFromFPComplianceTest @(IntN 3),
                  testGroup "ConvertibleBound" $ do
                    [ boundTest0 @IntN @12 @4 @16
                        "ebn<n-1&&sb>n-1,12/4/16"
                        100
                        [-256, -256, -255, -256, -255]
                        [256, 256, 255, 255, 256],
                      boundTest0 @IntN @12 @4 @12
                        "ebn<n-1&&sb>n-1,12/4/12"
                        100
                        [-256, -256, -255, -256, -255]
                        [256, 256, 255, 255, 256],
                      boundTest0 @IntN @12 @4 @11
                        "ebn<n-1&&sb==n-1,12/4/11"
                        100
                        [-256, -256, -255, -256, -255]
                        [256, 256, 255, 255, 256],
                      boundTest0 @IntN @12 @4 @10
                        "ebn<n-1&&sb<n-1,12/4/10"
                        100
                        [-256, -256, -255, -256, -255]
                        [256, 256, 255, 255, 256],
                      boundTest0 @IntN @12 @4 @9
                        "ebn<n-1&&sb<n-1,12/4/9"
                        100
                        [-256, -256, -255, -256, -255]
                        [256, 256, 255, 255, 256],
                      boundTest @IntN @12 @4 @2
                        "ebn<n-1&&sb<n-1,12/4/2"
                        100
                        (-192)
                        192,
                      boundTest0 @IntN @10 @4 @16
                        "ebn<n-1&&sb>n-1,10/4/16"
                        100
                        [-256, -256, -255, -256, -255]
                        [256, 256, 255, 255, 256],
                      boundTest0 @IntN @10 @4 @11
                        "ebn<n-1&&sb>n-1,10/4/10"
                        100
                        [-256, -256, -255, -256, -255]
                        [256, 256, 255, 255, 256],
                      boundTest0 @IntN @10 @4 @10
                        "ebn<n-1&&sb==n-1,10/4/9"
                        100
                        [-256, -256, -255, -256, -255]
                        [256, 256, 255, 255, 256],
                      boundTest @IntN @10 @4 @8
                        "ebn<n-1&&sb<n-1,10/4/8"
                        100
                        (-255)
                        255,
                      boundTest @IntN @10 @4 @7
                        "ebn<n-1&&sb<n-1,10/4/7"
                        100
                        (-254)
                        254,
                      boundTest @IntN @10 @4 @2
                        "ebn<n-1&&sb<n-1,10/4/2"
                        100
                        (-192)
                        192,
                      boundTest0 @IntN @9 @4 @16
                        "ebn==n-1&&sb>n-1,9/4/16"
                        100
                        [-256, -256, -255, -256, -255]
                        [255, 255, 255, 255, 255],
                      boundTest0 @IntN @9 @4 @9
                        "ebn==n-1&&sb>n-1,9/4/9"
                        100
                        [-256, -256, -255, -256, -255]
                        [255, 255, 255, 255, 255],
                      boundTest @IntN @9 @4 @8
                        "ebn==n-1&&sb==n-1,9/4/8"
                        100
                        (-255)
                        255,
                      boundTest @IntN @9 @4 @7
                        "ebn==n-1&&sb<n-1,9/4/7"
                        100
                        (-254)
                        254,
                      boundTest @IntN @9 @4 @2
                        "ebn==n-1&&sb<n-1,9/4/2"
                        100
                        (-192)
                        192,
                      boundTest @IntN @8 @4 @16
                        "ebn>n-1&&sb>n-1,8/4/16"
                        100
                        (-128)
                        127,
                      boundTest @IntN @8 @4 @8
                        "ebn>n-1&&sb>n-1,8/4/8"
                        100
                        (-128)
                        127,
                      boundTest @IntN @8 @4 @7
                        "ebn>n-1&&sb==n-1,8/4/7"
                        100
                        (-128)
                        127,
                      boundTest @IntN @8 @4 @6
                        "ebn>n-1&&sb<n-1,8/4/6"
                        100
                        (-128)
                        126,
                      boundTest @IntN @8 @4 @5
                        "ebn>n-1&&sb<n-1,8/4/5"
                        100
                        (-128)
                        124,
                      boundTest @IntN @8 @4 @2
                        "ebn>n-1&&sb<n-1,8/4/2"
                        100
                        (-128)
                        96,
                      boundTest @IntN @7 @4 @16
                        "ebn>n-1&&sb>n-1,7/4/16"
                        100
                        (-64)
                        63,
                      boundTest @IntN @7 @4 @7
                        "ebn>n-1&&sb>n-1,7/4/7"
                        100
                        (-64)
                        63,
                      boundTest @IntN @7 @4 @6
                        "ebn>n-1&&sb==n-1,7/4/6"
                        100
                        (-64)
                        63,
                      boundTest @IntN @7 @4 @5
                        "ebn>n-1&&sb<n-1,7/4/5"
                        100
                        (-64)
                        62,
                      boundTest @IntN @7 @4 @4
                        "ebn>n-1&&sb<n-1,7/4/4"
                        100
                        (-64)
                        60,
                      boundTest @IntN @7 @4 @2
                        "ebn>n-1&&sb<n-1,7/4/2"
                        100
                        (-64)
                        48,
                      boundTest @IntN @5 @4 @16
                        "ebn>n-1&&sb>n-1,5/4/16"
                        100
                        (-16)
                        15,
                      boundTest @IntN @5 @4 @5
                        "ebn>n-1&&sb>n-1,5/4/5"
                        100
                        (-16)
                        15,
                      boundTest @IntN @5 @4 @4
                        "ebn>n-1&&sb==n-1,5/4/4"
                        100
                        (-16)
                        15,
                      boundTest @IntN @5 @4 @3
                        "ebn>n-1&&sb<n-1,5/4/3"
                        100
                        (-16)
                        14,
                      boundTest @IntN @5 @4 @2
                        "ebn>n-1&&sb<n-1,5/4/2"
                        100
                        (-16)
                        12
                      ],
                  testCase "toFP" $ do
                    toFP rne (15 :: IntN 32) @?= (15 :: FP 4 4)
                    toFP rne <$> (ints :: [IntN 32]) @?= rneToFPExpected
                    toFP rna <$> (ints :: [IntN 32]) @?= rnaToFPExpected
                    toFP rtz <$> (ints :: [IntN 32]) @?= rtzToFPExpected
                    toFP rtn <$> (ints :: [IntN 32]) @?= rtnToFPExpected
                    toFP rtp <$> (ints :: [IntN 32]) @?= rtpToFPExpected
                ],
              testGroup
                "WordN"
                [ testCase "fromFPOr" $ do
                    fromFPOr (1 :: WordN 32) rne (fpPositiveZero :: FP 4 4)
                      @?= 0
                    fromFPOr (1 :: WordN 32) rne (fpNegativeZero :: FP 4 4)
                      @?= 0
                    fromFPOr (1 :: WordN 32) rne (fpPositiveInfinite :: FP 4 4)
                      @?= 1
                    fromFPOr (1 :: WordN 32) rne (fpNegativeInfinite :: FP 4 4)
                      @?= 1
                    fromFPOr (1 :: WordN 32) rne (fpNaN :: FP 4 4) @?= 1
                    let m = fmap (min 100)
                    fromFPOr (100 :: WordN 32) rne <$> fps @?= m rneFromExpected
                    fromFPOr (100 :: WordN 32) rna <$> fps @?= m rnaFromExpected
                    fromFPOr (100 :: WordN 32) rtp <$> fps @?= m rtpFromExpected
                    fromFPOr (100 :: WordN 32) rtn <$> fps @?= m rtnFromExpected
                    fromFPOr (100 :: WordN 32) rtz
                      <$> fps
                        @?= m rtzFromExpected
                    fromFPOr (4 :: WordN 3) rne (-0.5 :: FP 4 4) @?= 0
                    fromFPOr (4 :: WordN 3) rne (0.5 :: FP 4 4) @?= 0
                    fromFPOr (4 :: WordN 3) rna (-0.5 :: FP 4 4) @?= 4
                    fromFPOr (4 :: WordN 3) rna (0.5 :: FP 4 4) @?= 1
                    fromFPOr (4 :: WordN 3) rne (6.5 :: FP 4 4) @?= 6
                    fromFPOr (4 :: WordN 3) rne (7.5 :: FP 4 4) @?= 4
                    fromFPOr (4 :: WordN 3) rna (6.5 :: FP 4 4) @?= 7
                    fromFPOr (4 :: WordN 3) rna (7.5 :: FP 4 4) @?= 4,
                  safeFromFPComplianceTest @(WordN 3),
                  testGroup "ConvertibleBound" $ do
                    [ boundTest0 @WordN @12 @4 @16
                        "ebn<n&&sb>n,12/4/16"
                        100
                        [0, 0, 0, 0, 0]
                        [256, 256, 255, 255, 256],
                      boundTest0 @WordN @12 @4 @13
                        "ebn<n&&sb>n,12/4/13"
                        100
                        [0, 0, 0, 0, 0]
                        [256, 256, 255, 255, 256],
                      boundTest0 @WordN @12 @4 @12
                        "ebn<n&&sb==n,12/4/12"
                        100
                        [0, 0, 0, 0, 0]
                        [256, 256, 255, 255, 256],
                      boundTest0 @WordN @12 @4 @11
                        "ebn<n&&sb<n,12/4/11"
                        100
                        [0, 0, 0, 0, 0]
                        [256, 256, 255, 255, 256],
                      boundTest @WordN @12 @4 @2 "ebn<n&&sb<n,12/4/2" 100 0 192,
                      boundTest0 @WordN @9 @4 @16
                        "ebn<n&&sb>n,9/4/16"
                        100
                        [0, 0, 0, 0, 0]
                        [256, 256, 255, 255, 256],
                      boundTest0 @WordN @9 @4 @10
                        "ebn<n&&sb>n,9/4/10"
                        100
                        [0, 0, 0, 0, 0]
                        [256, 256, 255, 255, 256],
                      boundTest0 @WordN @9 @4 @9
                        "ebn<n&&sb==n,9/4/9"
                        100
                        [0, 0, 0, 0, 0]
                        [256, 256, 255, 255, 256],
                      boundTest @WordN @9 @4 @8 "ebn<n&&sb<n,9/4/8" 100 0 255,
                      boundTest @WordN @9 @4 @2 "ebn<n&&sb<n,9/4/2" 100 0 192,
                      boundTest @WordN @8 @4 @16
                        "ebn==n&&sb>n,8/4/16"
                        100
                        0
                        255,
                      boundTest @WordN @8 @4 @9 "ebn==n&&sb>n,8/4/16" 100 0 255,
                      boundTest @WordN @8 @4 @9 "ebn==n&&sb>n,8/4/9" 100 0 255,
                      boundTest @WordN @8 @4 @8 "ebn==n&&sb==n,8/4/8" 100 0 255,
                      boundTest @WordN @8 @4 @7 "ebn==n&&sb<n,8/4/7" 100 0 254,
                      boundTest @WordN @8 @4 @2 "ebn==n&&sb<n,8/4/2" 100 0 192,
                      boundTest @WordN @7 @4 @16 "ebn>n&&sb>n,7/4/16" 100 0 127,
                      boundTest @WordN @7 @4 @8 "ebn>n&&sb>n,7/4/8" 100 0 127,
                      boundTest @WordN @7 @4 @7 "ebn>n&&sb==n,7/4/7" 100 0 127,
                      boundTest @WordN @7 @4 @6 "ebn>n&&sb<n,7/4/6" 100 0 126,
                      boundTest @WordN @7 @4 @2 "ebn>n&&sb<n,7/4/2" 100 0 96,
                      boundTest @WordN @5 @4 @16 "ebn>n&&sb>n,7/4/16" 100 0 31,
                      boundTest @WordN @5 @4 @6 "ebn>n&&sb>n,5/4/6" 100 0 31,
                      boundTest @WordN @5 @4 @5 "ebn>n&&sb==n,5/4/5" 100 0 31,
                      boundTest @WordN @5 @4 @4 "ebn>n&&sb<n,5/4/4" 100 0 30,
                      boundTest @WordN @5 @4 @2 "ebn>n&&sb<n,5/4/2" 100 0 24
                      ],
                  testCase "toFP" $ do
                    toFP rne (15 :: WordN 32) @?= (15 :: FP 4 4)
                    toFP rne <$> (posints :: [WordN 32]) @?= rnePosToFPExpected
                    toFP rna <$> (posints :: [WordN 32]) @?= rnaPosToFPExpected
                    toFP rtz <$> (posints :: [WordN 32]) @?= rtzPosToFPExpected
                    toFP rtn <$> (posints :: [WordN 32]) @?= rtnPosToFPExpected
                    toFP rtp <$> (posints :: [WordN 32]) @?= rtpPosToFPExpected
                ]
              ]
          ],
      testProperty "Serialize" $ \(x :: FP 8 24) ->
        ioProperty $
          if isNaN x
            then case (decode . encode) x of
              Right (v :: FP 8 24) -> assertBool "Should be NaN" $ fpIsNaN v
              Left err -> fail err
            else Right x @?= (decode . encode) x
    ]

newtype SameFPObj = SameFPObj FP32 deriving newtype (Show, Num, IEEEFPConstants)

instance Eq SameFPObj where
  SameFPObj a == SameFPObj b
    | a == 0 && b == 0 =
        fpIsPositiveZero a == fpIsPositiveZero b
  SameFPObj a == SameFPObj b | fpIsNaN a && fpIsNaN b = True
  SameFPObj a == SameFPObj b = a == b