content: {-# LANGUAGE BinaryLiterals #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE NegativeLiterals #-}
  {-# LANGUAGE PatternSynonyms #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  
  module Grisette.SymPrim.BVTests (bvTests) where
  
  import Control.DeepSeq (NFData (rnf), deepseq, force)
  import Control.Exception
    ( ArithException,
      SomeException,
      catch,
      evaluate,
    )
  import Control.Monad (when)
  import Data.Bifunctor (Bifunctor (bimap))
  import Data.Bits
    ( Bits
        ( bit,
          bitSizeMaybe,
          clearBit,
          complement,
          complementBit,
          isSigned,
          popCount,
          rotate,
          rotateL,
          rotateR,
          setBit,
          shift,
          shiftL,
          shiftR,
          testBit,
          xor,
          zeroBits,
          (.&.),
          (.|.)
        ),
      FiniteBits (countLeadingZeros, countTrailingZeros, finiteBitSize),
    )
  import Data.Int (Int8)
  import Data.Proxy (Proxy (Proxy))
  import Data.Serialize (decode, encode)
  import Data.Typeable (Typeable, typeRep)
  import Data.Word (Word8)
  import GHC.Stack (HasCallStack)
  import Grisette
    ( BV (bv),
      SizedBV
        ( sizedBVConcat,
          sizedBVExt,
          sizedBVSelect,
          sizedBVSext,
          sizedBVZext
        ),
      SomeIntN,
      SomeWordN,
      pattern SomeIntN,
      pattern SomeWordN,
    )
  import Grisette.Internal.SymPrim.BV
    ( IntN (IntN),
      WordN (unWordN),
    )
  import Test.Framework (Test, TestName, testGroup)
  import Test.Framework.Providers.HUnit (testCase)
  import Test.Framework.Providers.QuickCheck2 (testProperty)
  import Test.HUnit (Assertion, assertFailure, (@=?), (@?=))
  import Test.QuickCheck (Arbitrary, Property, ioProperty)
  
  unaryConform :: forall a b c d. (Show c, Eq c, HasCallStack) => (a -> b) -> (d -> c) -> (a -> c) -> (b -> d) -> a -> Property
  unaryConform a2b d2c f g x = ioProperty $ f x @=? d2c (g (a2b x))
  
  binaryConform ::
    forall a b c d e f.
    (Show e, Eq e, HasCallStack) =>
    (a -> b) ->
    (c -> d) ->
    (f -> e) ->
    (a -> c -> e) ->
    (b -> d -> f) ->
    a ->
    c ->
    Property
  binaryConform a2b c2d f2e f g x y = ioProperty $ f x y @=? f2e (g (a2b x) (c2d y))
  
  wordUnaryConform :: (HasCallStack) => (WordN 8 -> WordN 8) -> (Word8 -> Word8) -> Word8 -> Assertion
  wordUnaryConform f g x = unWordN (f (fromIntegral x)) @=? toInteger (g x)
  
  wordUnaryNonNegIntConform :: (HasCallStack) => (Int -> WordN 8) -> (Int -> Word8) -> Int -> Assertion
  wordUnaryNonNegIntConform f g y = when (y >= 0) $ unWordN (f y) @=? toInteger (g y)
  
  wordBinIntConform :: (HasCallStack) => (WordN 8 -> Int -> WordN 8) -> (Word8 -> Int -> Word8) -> Word8 -> Int -> Assertion
  wordBinIntConform f g x y = unWordN (f (fromIntegral x) y) @=? toInteger (g x y)
  
  wordBinNonNegIntConform :: (HasCallStack) => (WordN 8 -> Int -> WordN 8) -> (Word8 -> Int -> Word8) -> Word8 -> Int -> Assertion
  wordBinNonNegIntConform f g x y = when (y >= 0) $ unWordN (f (fromIntegral x) y) @=? toInteger (g x y)
  
  wordBinConform :: (HasCallStack) => (WordN 8 -> WordN 8 -> WordN 8) -> (Word8 -> Word8 -> Word8) -> Word8 -> Word8 -> Assertion
  wordBinConform f g x y = unWordN (f (fromIntegral x) (fromIntegral y)) @=? toInteger (g x y)
  
  intN8eqint8 :: IntN 8 -> Int8 -> Assertion
  intN8eqint8 (IntN v) i
    | v < 0 = assertFailure "Bad IntN"
    | v <= 127 = v @=? fromIntegral i
    | v == 128 = i @=? -128
    | otherwise = 256 - v @=? fromIntegral (-i)
  
  intUnaryConform :: (IntN 8 -> IntN 8) -> (Int8 -> Int8) -> Int8 -> Assertion
  intUnaryConform f g x = intN8eqint8 (f (fromIntegral x)) (g x)
  
  intUnaryNonNegIntConform :: (Int -> IntN 8) -> (Int -> Int8) -> Int -> Assertion
  intUnaryNonNegIntConform f g y = when (y >= 0) $ intN8eqint8 (f y) (g y)
  
  intBinIntConform :: (IntN 8 -> Int -> IntN 8) -> (Int8 -> Int -> Int8) -> Int8 -> Int -> Assertion
  intBinIntConform f g x y = intN8eqint8 (f (fromIntegral x) y) (g x y)
  
  intBinNonNegIntConform :: (IntN 8 -> Int -> IntN 8) -> (Int8 -> Int -> Int8) -> Int8 -> Int -> Assertion
  intBinNonNegIntConform f g x y = when (y >= 0) $ intN8eqint8 (f (fromIntegral x) y) (g x y)
  
  intBinConform :: (IntN 8 -> IntN 8 -> IntN 8) -> (Int8 -> Int8 -> Int8) -> Int8 -> Int8 -> Assertion
  intBinConform f g x y = intN8eqint8 (f (fromIntegral x) (fromIntegral y)) (g x y)
  
  finiteBitsConformTest ::
    forall ref typ.
    ( Arbitrary ref,
      Typeable ref,
      Typeable typ,
      Show ref,
      FiniteBits ref,
      FiniteBits typ,
      Integral ref,
      Integral typ
    ) =>
    Proxy ref ->
    Proxy typ ->
    Int ->
    Test
  finiteBitsConformTest pref ptyp numBits =
    testGroup
      (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for FiniteBits instances")
      [ testCase "finiteBitSize" $ finiteBitSize (0 :: typ) @=? numBits,
        testProperty "countLeadingZeros" $ unaryConform @ref @typ fromIntegral id countLeadingZeros countLeadingZeros,
        testProperty "countTrailingZeros" $ unaryConform @ref @typ fromIntegral id countTrailingZeros countTrailingZeros
      ]
  
  boundedConformTest ::
    forall ref typ.
    (Typeable ref, Typeable typ, Bounded typ, Bounded ref, Integral ref, Num typ, Eq typ, Show typ) =>
    Proxy ref ->
    Proxy typ ->
    Test
  boundedConformTest pref ptyp =
    testGroup
      (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for Bounded instances")
      [ testCase "minBound" $ (minBound :: typ) @=? fromIntegral (minBound :: ref),
        testCase "maxBound" $ (maxBound :: typ) @=? fromIntegral (maxBound :: ref)
      ]
  
  shouldThrow :: (NFData a) => String -> a -> IO ()
  shouldThrow name x = do
    errored <- catch (evaluate $ x `deepseq` True) (\(_ :: SomeException) -> return False)
    when errored $ assertFailure $ name ++ " should throw an exception"
  
  succPredLikeTest ::
    forall a b.
    (Arbitrary a, Eq a, Eq b, Show a, Show b, NFData b) =>
    TestName ->
    String ->
    (a -> b) ->
    (a -> a) ->
    (b -> b) ->
    a ->
    b ->
    Test
  succPredLikeTest name boundName a2b fa fb bounda boundb =
    testGroup
      name
      [ testProperty (name ++ " non " ++ boundName) $
          ioProperty . \(x :: a) ->
            if x == bounda then return () else a2b (fa x) @=? fb (a2b x),
        testCase (name ++ " " ++ boundName) $ shouldThrow (name ++ " " ++ boundName) $ fb boundb
      ]
  
  enumConformTest ::
    forall ref typ.
    ( Arbitrary ref,
      Typeable ref,
      Typeable typ,
      Show ref,
      Show typ,
      NFData typ,
      Integral ref,
      Integral typ,
      Bounded ref,
      Bounded typ
    ) =>
    Proxy ref ->
    Proxy typ ->
    Test
  enumConformTest pref ptyp =
    testGroup
      (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for Enum instances")
      [ succPredLikeTest @ref @typ "succ" "maxBound" fromIntegral succ succ maxBound maxBound,
        succPredLikeTest @ref @typ "pred" "minBound" fromIntegral pred pred minBound minBound,
        testGroup
          "toEnum"
          [ testProperty "toEnum in bounds" $
              ioProperty . \(x :: ref) ->
                toInteger (toEnum (fromIntegral x) :: ref) @=? toInteger (toEnum (fromIntegral x) :: typ),
            testCase "toEnum (fromIntegral minBound - 1)" $
              shouldThrow "toEnum (fromIntegral minBound - 1)" (toEnum (fromIntegral (minBound :: typ) - 1) :: typ),
            testCase "toEnum (fromIntegral maxBound + 1)" $
              shouldThrow "toEnum (fromIntegral maxBound + 1)" (toEnum (fromIntegral (maxBound :: typ) + 1) :: typ)
          ],
        testProperty "fromEnum" $ unaryConform @ref @typ fromIntegral id fromEnum fromEnum,
        testProperty "enumFrom" $ unaryConform @ref @typ fromIntegral (fromIntegral <$>) enumFrom enumFrom,
        testProperty "enumFromThen" $ \(x :: ref) y ->
          ioProperty $ do
            if x == y
              then return ()
              else do
                (fromIntegral <$> enumFromThen x y) @=? enumFromThen (fromIntegral x :: typ) (fromIntegral y),
        testProperty "enumFromTo" $ binaryConform @ref @typ fromIntegral fromIntegral (fromIntegral <$>) enumFromTo enumFromTo,
        testProperty "enumFromThenTo" $ \(x :: ref) y z ->
          ioProperty $
            if x == y
              then return ()
              else (fromIntegral <$> enumFromThenTo x y z) @=? enumFromThenTo (fromIntegral x :: typ) (fromIntegral y) (fromIntegral z)
      ]
  
  newtype AEWrapper = AEWrapper ArithException deriving (Eq)
  
  instance Show AEWrapper where
    show (AEWrapper x) = show x
  
  instance NFData AEWrapper where
    rnf (AEWrapper x) = x `seq` ()
  
  sameDiv :: (NFData a, NFData b, Eq b, Show b) => a -> a -> (a -> b) -> (a -> a -> a) -> (b -> b -> b) -> IO ()
  sameDiv x y a2b fa fb = do
    xa <- evaluate (force $ Right $ fa x y) `catch` \(e :: ArithException) -> return $ Left $ AEWrapper e
    xb <- evaluate (force $ Right $ fb (a2b x) (a2b y)) `catch` \(e :: ArithException) -> return $ Left $ AEWrapper e
    xb @=? a2b <$> xa
  
  sameDivMod :: (NFData a, NFData b, Eq b, Show b) => a -> a -> (a -> b) -> (a -> a -> (a, a)) -> (b -> b -> (b, b)) -> IO ()
  sameDivMod x y a2b fa fb = do
    xa <- evaluate (force $ Right $ fa x y) `catch` \(e :: ArithException) -> return $ Left $ AEWrapper e
    xb <- evaluate (force $ Right $ fb (a2b x) (a2b y)) `catch` \(e :: ArithException) -> return $ Left $ AEWrapper e
    xb @=? bimap a2b a2b <$> xa
  
  divLikeTest ::
    forall a b.
    (Arbitrary a, Eq b, Num a, Show a, Bounded a, Show b, NFData b, NFData a) =>
    TestName ->
    (a -> b) ->
    (a -> a -> a) ->
    (b -> b -> b) ->
    Test
  divLikeTest name a2b fa fb =
    testGroup
      name
      [ testCase "divided by zero" $ do
          sameDiv 1 0 a2b fa fb
          sameDiv 0 0 a2b fa fb
          sameDiv (-1) 0 a2b fa fb
          sameDiv minBound 0 a2b fa fb
          sameDiv maxBound 0 a2b fa fb,
        testCase "min divided by -1" $ do
          sameDiv minBound (-1) a2b fa fb,
        testProperty "prop" $ \(x :: a) y -> ioProperty $ sameDiv x y a2b fa fb
      ]
  
  divModLikeTest ::
    forall a b.
    (Arbitrary a, Eq b, Num a, NFData a, Show a, Bounded a, Show b, NFData b) =>
    TestName ->
    (a -> b) ->
    (a -> a -> (a, a)) ->
    (b -> b -> (b, b)) ->
    Test
  divModLikeTest name a2b fa fb =
    testGroup
      name
      [ testCase "divided by zero" $ do
          sameDivMod 1 0 a2b fa fb
          sameDivMod 0 0 a2b fa fb
          sameDivMod (-1) 0 a2b fa fb
          sameDivMod minBound 0 a2b fa fb
          sameDivMod maxBound 0 a2b fa fb,
        testCase "min divided by -1" $ do
          sameDivMod minBound (-1) a2b fa fb,
        testProperty "prop" $ \(x :: a) y -> ioProperty $ sameDivMod x y a2b fa fb
      ]
  
  realConformTest ::
    forall proxy ref typ.
    (Typeable ref, Typeable typ, Integral ref, Arbitrary ref, Real typ, Show ref) =>
    proxy ref ->
    proxy typ ->
    Test
  realConformTest pref ptyp =
    testGroup
      (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for Real instances")
      [ testProperty "toRational" $ unaryConform @ref @typ fromIntegral id toRational toRational
      ]
  
  integralConformTest ::
    forall ref typ.
    ( Arbitrary ref,
      Typeable ref,
      Typeable typ,
      Show ref,
      Show typ,
      Integral ref,
      Integral typ,
      Bounded ref,
      NFData typ,
      NFData ref
    ) =>
    Proxy ref ->
    Proxy typ ->
    Test
  integralConformTest pref ptyp =
    testGroup
      (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for Integral instances")
      [ divLikeTest @ref @typ "quot" fromIntegral quot quot,
        divLikeTest @ref @typ "rem" fromIntegral rem rem,
        divModLikeTest @ref @typ "quotRem" fromIntegral quotRem quotRem,
        divLikeTest @ref @typ "div" fromIntegral div div,
        divLikeTest @ref @typ "mod" fromIntegral mod mod,
        divModLikeTest @ref @typ "divMod" fromIntegral divMod divMod,
        testProperty "toInteger" $ unaryConform @ref @typ fromIntegral id toInteger toInteger
      ]
  
  sizedBVTests :: Test
  sizedBVTests =
    testGroup
      "sizedBV"
      [ testGroup
          "WordN 8 conform to Word8 for Bits instances"
          [ testProperty "(.&.)" $ \x y -> ioProperty $ wordBinConform (.&.) (.&.) x y,
            testProperty "(.|.)" $ \x y -> ioProperty $ wordBinConform (.|.) (.|.) x y,
            testProperty "xor" $ \x y -> ioProperty $ wordBinConform xor xor x y,
            testProperty "complement" $ ioProperty . wordUnaryConform complement complement,
            testProperty "shift" $ \x y -> ioProperty $ wordBinIntConform shift shift x y,
            testProperty "rotate" $ \x y -> ioProperty $ wordBinIntConform rotate rotate x y,
            testCase "zeroBits" $ (zeroBits :: WordN 8) @=? 0,
            testProperty "bit" $ ioProperty . wordUnaryNonNegIntConform bit bit,
            testProperty "setBit" $ \x y -> ioProperty $ wordBinNonNegIntConform setBit setBit x y,
            testProperty "clearBit" $ \x y -> ioProperty $ wordBinNonNegIntConform clearBit clearBit x y,
            testProperty "complementBit" $ \x y -> ioProperty $ wordBinNonNegIntConform complementBit complementBit x y,
            testProperty "testBit" $ \(x :: Word8) i -> i < 0 || testBit x i == testBit (fromIntegral x :: WordN 8) i,
            testCase "bitSizeMaybe" $ bitSizeMaybe (0 :: WordN 8) @=? Just 8,
            testCase "isSigned" $ isSigned (0 :: WordN 8) @=? False,
            testProperty "shiftL" $ \x y -> ioProperty $ wordBinNonNegIntConform shiftL shiftL x y,
            testProperty "shiftR" $ \x y -> ioProperty $ wordBinNonNegIntConform shiftR shiftR x y,
            testProperty "rotateL" $ \x y -> ioProperty $ wordBinNonNegIntConform rotateL rotateL x y,
            testProperty "rotateR" $ \x y -> ioProperty $ wordBinNonNegIntConform rotateR rotateR x y,
            testProperty "popCount" $ ioProperty . \(x :: Word8) -> popCount x @=? popCount (fromIntegral x :: WordN 8)
          ],
        finiteBitsConformTest (Proxy @Word8) (Proxy @(WordN 8)) 8,
        boundedConformTest (Proxy @Word8) (Proxy @(WordN 8)),
        enumConformTest (Proxy @Word8) (Proxy @(WordN 8)),
        realConformTest (Proxy @Word8) (Proxy @(WordN 8)),
        integralConformTest (Proxy @Word8) (Proxy @(WordN 8)),
        testGroup
          "WordN 8 conform to Word8 for Num instances"
          [ testProperty "(+)" $ \x y -> ioProperty $ wordBinConform (+) (+) x y,
            testProperty "(*)" $ \x y -> ioProperty $ wordBinConform (*) (*) x y,
            testProperty "(-)" $ \x y -> ioProperty $ wordBinConform (-) (-) x y,
            testProperty "negate" $ ioProperty . wordUnaryConform negate negate,
            testProperty "abs" $ ioProperty . wordUnaryConform abs abs,
            testProperty "signum" $ ioProperty . wordUnaryConform signum signum,
            testProperty "fromInteger" $
              ioProperty . \(x :: Integer) ->
                unWordN (fromInteger x :: WordN 8) @=? toInteger (fromInteger x :: Word8)
          ],
        testGroup
          "WordN 8 conform to Word8 for Ord instances"
          [ testProperty "(<=)" $ \(x :: Word8) y -> ioProperty $ x <= y @=? (fromIntegral x :: WordN 8) <= (fromIntegral y :: WordN 8)
          ],
        testGroup
          "IntN 8 conform to Int8 for Bits instances"
          [ testProperty "(.&.)" $ \x y -> ioProperty $ intBinConform (.&.) (.&.) x y,
            testProperty "(.|.)" $ \x y -> ioProperty $ intBinConform (.|.) (.|.) x y,
            testProperty "xor" $ \x y -> ioProperty $ intBinConform xor xor x y,
            testProperty "complement" $ ioProperty . intUnaryConform complement complement,
            testProperty "shift" $ \x y -> ioProperty $ intBinIntConform shift shift x y,
            testProperty "rotate" $ \x y -> ioProperty $ intBinIntConform rotate rotate x y,
            testCase "zeroBits" $ (zeroBits :: IntN 8) @=? 0,
            testProperty "bit" $ ioProperty . intUnaryNonNegIntConform bit bit,
            testProperty "setBit" $ \x y -> ioProperty $ intBinNonNegIntConform setBit setBit x y,
            testProperty "clearBit" $ \x y -> ioProperty $ intBinNonNegIntConform clearBit clearBit x y,
            testProperty "complementBit" $ \x y -> ioProperty $ intBinNonNegIntConform complementBit complementBit x y,
            testProperty "testBit" $ \(x :: Int8) i -> i < 0 || testBit x i == testBit (fromIntegral x :: IntN 8) i,
            testCase "bitSizeMaybe" $ bitSizeMaybe (0 :: IntN 8) @=? Just 8,
            testCase "isSigned" $ isSigned (0 :: IntN 8) @=? True,
            testProperty "shiftL" $ \x y -> ioProperty $ intBinNonNegIntConform shiftL shiftL x y,
            testProperty "shiftR" $ \x y -> ioProperty $ intBinNonNegIntConform shiftR shiftR x y,
            testProperty "rotateL" $ \x y -> ioProperty $ intBinNonNegIntConform rotateL rotateL x y,
            testProperty "rotateR" $ \x y -> ioProperty $ intBinNonNegIntConform rotateR rotateR x y,
            testProperty "popCount" $ ioProperty . \(x :: Int8) -> popCount x @=? popCount (fromIntegral x :: IntN 8)
          ],
        finiteBitsConformTest (Proxy @Int8) (Proxy @(IntN 8)) 8,
        boundedConformTest (Proxy @Int8) (Proxy @(IntN 8)),
        enumConformTest (Proxy @Int8) (Proxy @(IntN 8)),
        realConformTest (Proxy @Int8) (Proxy @(IntN 8)),
        integralConformTest (Proxy @Int8) (Proxy @(IntN 8)),
        testGroup
          "IntN 8 conform to Int8 for Num instances"
          [ testProperty "(+)" $ \x y -> ioProperty $ intBinConform (+) (+) x y,
            testProperty "(*)" $ \x y -> ioProperty $ intBinConform (*) (*) x y,
            testProperty "(-)" $ \x y -> ioProperty $ intBinConform (-) (-) x y,
            testProperty "negate" $ ioProperty . wordUnaryConform negate negate,
            testProperty "abs" $ ioProperty . wordUnaryConform abs abs,
            testProperty "signum" $ ioProperty . wordUnaryConform signum signum,
            testProperty "fromInteger" $
              ioProperty . \(x :: Integer) ->
                intN8eqint8 (fromInteger x :: IntN 8) (fromInteger x :: Int8)
          ],
        testGroup
          "IntN 8 conform to IntN for Ord instances"
          [ testProperty "(<=)" $ \(x :: Int8) y -> ioProperty $ (fromIntegral x :: IntN 8) <= (fromIntegral y :: IntN 8) @=? x <= y
          ],
        testGroup
          "WordN bvops"
          [ testProperty "sizedBVConcat" $ \(x :: Integer) (y :: Integer) ->
              ioProperty $
                sizedBVConcat (fromInteger x :: WordN 5) (fromInteger y :: WordN 7) @=? fromInteger (x * 128 + y `mod` 128),
            testProperty "sizedBVZext" $ ioProperty . \(x :: Integer) -> sizedBVZext (Proxy :: Proxy 12) (fromInteger x :: WordN 7) @=? fromInteger (x `mod` 128),
            testCase "sizedBVSext" $ do
              sizedBVSext (Proxy :: Proxy 12) (0 :: WordN 8) @=? 0
              sizedBVSext (Proxy :: Proxy 12) (1 :: WordN 8) @=? 1
              sizedBVSext (Proxy :: Proxy 12) (127 :: WordN 8) @=? 127
              sizedBVSext (Proxy :: Proxy 12) (128 :: WordN 8) @=? 3968
              sizedBVSext (Proxy :: Proxy 12) (255 :: WordN 8) @=? 4095,
            testProperty "sizedBVExt is sizedBVZext" $
              ioProperty . \(x :: Integer) ->
                sizedBVExt (Proxy :: Proxy 12) (fromInteger x :: WordN 8) @=? sizedBVZext (Proxy :: Proxy 12) (fromInteger x :: WordN 8),
            testCase "sizedBVSelect" $ do
              sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b11100 :: WordN 8) @=? 0b11
              sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b111000 :: WordN 8) @=? 0b111
              sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b101000 :: WordN 8) @=? 0b101
              sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b1010000 :: WordN 8) @=? 0b10
          ],
        testGroup
          "IntN bvops"
          [ testProperty "sizedBVConcat" $ \(x :: Integer) (y :: Integer) ->
              ioProperty $
                sizedBVConcat (fromInteger x :: IntN 5) (fromInteger y :: IntN 7) @=? fromInteger (x * 128 + y `mod` 128),
            testProperty "sizedBVZext" $ ioProperty . \(x :: Integer) -> sizedBVZext (Proxy :: Proxy 12) (fromInteger x :: IntN 7) @=? fromInteger (x `mod` 128),
            testCase "sizedBVSext" $ do
              sizedBVSext (Proxy :: Proxy 12) (0 :: WordN 8) @=? 0
              sizedBVSext (Proxy :: Proxy 12) (1 :: WordN 8) @=? 1
              sizedBVSext (Proxy :: Proxy 12) (127 :: WordN 8) @=? 127
              sizedBVSext (Proxy :: Proxy 12) (128 :: WordN 8) @=? 3968
              sizedBVSext (Proxy :: Proxy 12) (255 :: WordN 8) @=? 4095,
            testProperty "sizedBVExt is sizedBVSext" $
              ioProperty . \(x :: Integer) ->
                sizedBVExt (Proxy :: Proxy 12) (fromInteger x :: IntN 8) @=? sizedBVSext (Proxy :: Proxy 12) (fromInteger x :: IntN 8),
            testCase "sizedBVSelect" $ do
              sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b11100 :: IntN 8) @=? 0b11
              sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b111000 :: IntN 8) @=? 0b111
              sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b101000 :: IntN 8) @=? 0b101
              sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b1010000 :: IntN 8) @=? 0b10
          ],
        testGroup
          "read"
          [ testProperty "read . show" $ \(x :: IntN 8) -> read (show x) == x,
            testProperty "read . show" $ \(x :: WordN 8) -> read (show x) == x,
            testProperty "read . show" $ \(x :: IntN 9) -> read (show x) == x,
            testProperty "read . show" $ \(x :: WordN 9) -> read (show x) == x
          ],
        testGroup
          "Regression"
          [ testCase "division of min bound and minus one for signed bit vector should throw" $ do
              shouldThrow "divMod" $ divMod (minBound :: IntN 8) (-1 :: IntN 8)
              shouldThrow "div" $ div (minBound :: IntN 8) (-1 :: IntN 8)
              shouldThrow "quotRem" $ quotRem (minBound :: IntN 8) (-1 :: IntN 8)
              shouldThrow "quot" $ quot (minBound :: IntN 8) (-1 :: IntN 8),
            testCase "toInteger for IntN 1" $ do
              toInteger (0 :: IntN 1) @=? 0
              toInteger (1 :: IntN 1) @=? (-1),
            testProperty "WordN shiftL by large amount" $ \(x :: WordN 128) ->
              ioProperty $ shiftL x maxBound @=? 0,
            testProperty "IntN shiftL by large amount" $ \(x :: IntN 128) ->
              ioProperty $ shiftL x maxBound @=? 0
          ],
        testGroup
          "Serialize"
          [ testProperty "WordN 8" $
              \(x :: WordN 8) -> Right x == (decode . encode) x,
            testProperty "IntN 8" $
              \(x :: IntN 8) -> Right x == (decode . encode) x
          ]
      ]
  
  someWordNTests :: Test
  someWordNTests =
    testGroup
      "SomeWordN"
      [ testGroup
          "BV"
          [ testGroup
              "bv"
              [ testCase "bv 12 21" $
                  (bv 12 21 :: SomeWordN) @?= SomeWordN (0x015 :: WordN 12)
              ]
          ]
      ]
  
  someIntNTests :: Test
  someIntNTests =
    testGroup
      "SomeIntN"
      [ testGroup
          "BV"
          [ testGroup
              "bv"
              [ testCase "bv 12 21" $
                  (bv 12 21 :: SomeIntN) @?= SomeIntN (0x015 :: IntN 12)
              ]
          ]
      ]
  
  bvTests :: Test
  bvTests = testGroup "BV" [sizedBVTests, someWordNTests, someIntNTests]
  