-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Core.Sized
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Type-level sized bit-vectors. Thanks to Ben Blaxill for providing an
-- initial implementation of this idea.
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Core.Sized (
        -- * Type-sized unsigned bit-vectors
          SWord, WordN, sWord, sWord_, sWords
        -- * Type-sized signed bit-vectors
        , SInt, IntN, sInt, sInt_, sInts
        -- * Bit-vector operations
        , bvExtract, (#), zeroExtend, signExtend, bvDrop, bvTake
        -- * Splitting and reconstructing from bytes
        , ByteConverter(..)
       ) where

import Data.Bits
import Data.Maybe (fromJust)
import Data.Proxy (Proxy(..))

import GHC.TypeLits

import Data.SBV.Core.Data
import Data.SBV.Core.Kind
import Data.SBV.Core.Model
import Data.SBV.Core.Operations
import Data.SBV.Core.Symbolic

import Data.SBV.SMT.SMT

-- Doctest only
-- $setup
-- >>> :set -XTypeApplications
-- >>> :set -XDataKinds
-- >>> import Data.SBV.Provers.Prover (prove)

-- | An unsigned bit-vector carrying its size info
newtype WordN (n :: Nat) = WordN Integer deriving (WordN n -> WordN n -> Bool
(WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool) -> Eq (WordN n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (n :: Nat). WordN n -> WordN n -> Bool
/= :: WordN n -> WordN n -> Bool
$c/= :: forall (n :: Nat). WordN n -> WordN n -> Bool
== :: WordN n -> WordN n -> Bool
$c== :: forall (n :: Nat). WordN n -> WordN n -> Bool
Eq, Eq (WordN n)
Eq (WordN n)
-> (WordN n -> WordN n -> Ordering)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> WordN n)
-> (WordN n -> WordN n -> WordN n)
-> Ord (WordN n)
WordN n -> WordN n -> Bool
WordN n -> WordN n -> Ordering
WordN n -> WordN n -> WordN n
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (n :: Nat). Eq (WordN n)
forall (n :: Nat). WordN n -> WordN n -> Bool
forall (n :: Nat). WordN n -> WordN n -> Ordering
forall (n :: Nat). WordN n -> WordN n -> WordN n
min :: WordN n -> WordN n -> WordN n
$cmin :: forall (n :: Nat). WordN n -> WordN n -> WordN n
max :: WordN n -> WordN n -> WordN n
$cmax :: forall (n :: Nat). WordN n -> WordN n -> WordN n
>= :: WordN n -> WordN n -> Bool
$c>= :: forall (n :: Nat). WordN n -> WordN n -> Bool
> :: WordN n -> WordN n -> Bool
$c> :: forall (n :: Nat). WordN n -> WordN n -> Bool
<= :: WordN n -> WordN n -> Bool
$c<= :: forall (n :: Nat). WordN n -> WordN n -> Bool
< :: WordN n -> WordN n -> Bool
$c< :: forall (n :: Nat). WordN n -> WordN n -> Bool
compare :: WordN n -> WordN n -> Ordering
$ccompare :: forall (n :: Nat). WordN n -> WordN n -> Ordering
$cp1Ord :: forall (n :: Nat). Eq (WordN n)
Ord)

-- | A symbolic unsigned bit-vector carrying its size info
type SWord (n :: Nat) = SBV (WordN n)

-- | Show instance for 'WordN'
instance Show (WordN n) where
  show :: WordN n -> String
show (WordN Integer
v) = Integer -> String
forall a. Show a => a -> String
show Integer
v

-- | 'WordN' has a kind
instance (KnownNat n, BVIsNonZero n) => HasKind (WordN n) where
  kindOf :: WordN n -> Kind
kindOf WordN n
_ = Bool -> Int -> Kind
KBounded Bool
False (Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n))

-- | 'SymVal' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => SymVal (WordN n) where
   literal :: WordN n -> SBV (WordN n)
literal  WordN n
x = Kind -> WordN n -> SBV (WordN n)
forall a b. Integral a => Kind -> a -> SBV b
genLiteral  (WordN n -> Kind
forall a. HasKind a => a -> Kind
kindOf WordN n
x) WordN n
x
   mkSymVal :: VarContext -> Maybe String -> m (SBV (WordN n))
mkSymVal   = Kind -> VarContext -> Maybe String -> m (SBV (WordN n))
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (WordN n -> Kind
forall a. HasKind a => a -> Kind
kindOf (WordN n
forall a. HasCallStack => a
undefined :: WordN n))
   fromCV :: CV -> WordN n
fromCV     = CV -> WordN n
forall a. Integral a => CV -> a
genFromCV

-- | A signed bit-vector carrying its size info
newtype IntN (n :: Nat) = IntN Integer deriving (IntN n -> IntN n -> Bool
(IntN n -> IntN n -> Bool)
-> (IntN n -> IntN n -> Bool) -> Eq (IntN n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (n :: Nat). IntN n -> IntN n -> Bool
/= :: IntN n -> IntN n -> Bool
$c/= :: forall (n :: Nat). IntN n -> IntN n -> Bool
== :: IntN n -> IntN n -> Bool
$c== :: forall (n :: Nat). IntN n -> IntN n -> Bool
Eq, Eq (IntN n)
Eq (IntN n)
-> (IntN n -> IntN n -> Ordering)
-> (IntN n -> IntN n -> Bool)
-> (IntN n -> IntN n -> Bool)
-> (IntN n -> IntN n -> Bool)
-> (IntN n -> IntN n -> Bool)
-> (IntN n -> IntN n -> IntN n)
-> (IntN n -> IntN n -> IntN n)
-> Ord (IntN n)
IntN n -> IntN n -> Bool
IntN n -> IntN n -> Ordering
IntN n -> IntN n -> IntN n
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (n :: Nat). Eq (IntN n)
forall (n :: Nat). IntN n -> IntN n -> Bool
forall (n :: Nat). IntN n -> IntN n -> Ordering
forall (n :: Nat). IntN n -> IntN n -> IntN n
min :: IntN n -> IntN n -> IntN n
$cmin :: forall (n :: Nat). IntN n -> IntN n -> IntN n
max :: IntN n -> IntN n -> IntN n
$cmax :: forall (n :: Nat). IntN n -> IntN n -> IntN n
>= :: IntN n -> IntN n -> Bool
$c>= :: forall (n :: Nat). IntN n -> IntN n -> Bool
> :: IntN n -> IntN n -> Bool
$c> :: forall (n :: Nat). IntN n -> IntN n -> Bool
<= :: IntN n -> IntN n -> Bool
$c<= :: forall (n :: Nat). IntN n -> IntN n -> Bool
< :: IntN n -> IntN n -> Bool
$c< :: forall (n :: Nat). IntN n -> IntN n -> Bool
compare :: IntN n -> IntN n -> Ordering
$ccompare :: forall (n :: Nat). IntN n -> IntN n -> Ordering
$cp1Ord :: forall (n :: Nat). Eq (IntN n)
Ord)

-- | A symbolic signed bit-vector carrying its size info
type SInt (n :: Nat) = SBV (IntN n)

-- | Show instance for 'IntN'
instance Show (IntN n) where
  show :: IntN n -> String
show (IntN Integer
v) = Integer -> String
forall a. Show a => a -> String
show Integer
v

-- | 'IntN' has a kind
instance (KnownNat n, BVIsNonZero n) => HasKind (IntN n) where
  kindOf :: IntN n -> Kind
kindOf IntN n
_ = Bool -> Int -> Kind
KBounded Bool
True (Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n))

-- | 'SymVal' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => SymVal (IntN n) where
   literal :: IntN n -> SBV (IntN n)
literal  IntN n
x = Kind -> IntN n -> SBV (IntN n)
forall a b. Integral a => Kind -> a -> SBV b
genLiteral  (IntN n -> Kind
forall a. HasKind a => a -> Kind
kindOf IntN n
x) IntN n
x
   mkSymVal :: VarContext -> Maybe String -> m (SBV (IntN n))
mkSymVal   = Kind -> VarContext -> Maybe String -> m (SBV (IntN n))
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (IntN n -> Kind
forall a. HasKind a => a -> Kind
kindOf (IntN n
forall a. HasCallStack => a
undefined :: IntN n))
   fromCV :: CV -> IntN n
fromCV     = CV -> IntN n
forall a. Integral a => CV -> a
genFromCV

-- Lift a unary operation via SVal
lift1 :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> SVal) -> bv n -> bv n
lift1 :: String -> (SVal -> SVal) -> bv n -> bv n
lift1 String
nm SVal -> SVal
op bv n
x = SVal -> bv n
uc (SVal -> bv n) -> SVal -> bv n
forall a b. (a -> b) -> a -> b
$ SVal -> SVal
op (bv n -> SVal
c bv n
x)
  where k :: Kind
k = bv n -> Kind
forall a. HasKind a => a -> Kind
kindOf bv n
x
        c :: bv n -> SVal
c = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal)
-> (bv n -> Either CV (Cached SV)) -> bv n -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (bv n -> CV) -> bv n -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> (bv n -> CVal) -> bv n -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CVal
CInteger (Integer -> CVal) -> (bv n -> Integer) -> bv n -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. bv n -> Integer
forall a. Integral a => a -> Integer
toInteger
        uc :: SVal -> bv n
uc (SVal Kind
_ (Left (CV Kind
_ (CInteger Integer
v)))) = Integer -> bv n
forall a. Num a => Integer -> a
fromInteger Integer
v
        uc SVal
r                                   = String -> bv n
forall a. HasCallStack => String -> a
error (String -> bv n) -> String -> bv n
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened while lifting " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" over " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Kind, bv n, SVal) -> String
forall a. Show a => a -> String
show (Kind
k, bv n
x, SVal
r)

-- Lift a binary operation via SVal
lift2 :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2 :: String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2 String
nm SVal -> SVal -> SVal
op bv n
x bv n
y = SVal -> bv n
uc (SVal -> bv n) -> SVal -> bv n
forall a b. (a -> b) -> a -> b
$ bv n -> SVal
c bv n
x SVal -> SVal -> SVal
`op` bv n -> SVal
c bv n
y
  where k :: Kind
k = bv n -> Kind
forall a. HasKind a => a -> Kind
kindOf bv n
x
        c :: bv n -> SVal
c = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal)
-> (bv n -> Either CV (Cached SV)) -> bv n -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (bv n -> CV) -> bv n -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> (bv n -> CVal) -> bv n -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CVal
CInteger (Integer -> CVal) -> (bv n -> Integer) -> bv n -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. bv n -> Integer
forall a. Integral a => a -> Integer
toInteger
        uc :: SVal -> bv n
uc (SVal Kind
_ (Left (CV Kind
_ (CInteger Integer
v)))) = Integer -> bv n
forall a. Num a => Integer -> a
fromInteger Integer
v
        uc SVal
r                                   = String -> bv n
forall a. HasCallStack => String -> a
error (String -> bv n) -> String -> bv n
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened while lifting " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" over " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Kind, bv n, bv n, SVal) -> String
forall a. Show a => a -> String
show (Kind
k, bv n
x, bv n
y, SVal
r)

-- Lift a binary operation via SVal where second argument is an Int
lift2I :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I :: String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I String
nm SVal -> Int -> SVal
op bv n
x Int
i = SVal -> bv n
uc (SVal -> bv n) -> SVal -> bv n
forall a b. (a -> b) -> a -> b
$ bv n -> SVal
c bv n
x SVal -> Int -> SVal
`op` Int
i
  where k :: Kind
k = bv n -> Kind
forall a. HasKind a => a -> Kind
kindOf bv n
x
        c :: bv n -> SVal
c = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal)
-> (bv n -> Either CV (Cached SV)) -> bv n -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (bv n -> CV) -> bv n -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> (bv n -> CVal) -> bv n -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CVal
CInteger (Integer -> CVal) -> (bv n -> Integer) -> bv n -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. bv n -> Integer
forall a. Integral a => a -> Integer
toInteger
        uc :: SVal -> bv n
uc (SVal Kind
_ (Left (CV Kind
_ (CInteger Integer
v)))) = Integer -> bv n
forall a. Num a => Integer -> a
fromInteger Integer
v
        uc SVal
r                                   = String -> bv n
forall a. HasCallStack => String -> a
error (String -> bv n) -> String -> bv n
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened while lifting " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" over " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Kind, bv n, Int, SVal) -> String
forall a. Show a => a -> String
show (Kind
k, bv n
x, Int
i, SVal
r)

-- Lift a binary operation via SVal where second argument is an Int and returning a Bool
lift2IB :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
lift2IB :: String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
lift2IB String
nm SVal -> Int -> SVal
op bv n
x Int
i = SVal -> Bool
uc (SVal -> Bool) -> SVal -> Bool
forall a b. (a -> b) -> a -> b
$ bv n -> SVal
c bv n
x SVal -> Int -> SVal
`op` Int
i
  where k :: Kind
k = bv n -> Kind
forall a. HasKind a => a -> Kind
kindOf bv n
x
        c :: bv n -> SVal
c = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal)
-> (bv n -> Either CV (Cached SV)) -> bv n -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (bv n -> CV) -> bv n -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> (bv n -> CVal) -> bv n -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CVal
CInteger (Integer -> CVal) -> (bv n -> Integer) -> bv n -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. bv n -> Integer
forall a. Integral a => a -> Integer
toInteger
        uc :: SVal -> Bool
uc (SVal Kind
_ (Left CV
v)) = CV -> Bool
cvToBool CV
v
        uc SVal
r                 = String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened while lifting " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" over " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Kind, bv n, Int, SVal) -> String
forall a. Show a => a -> String
show (Kind
k, bv n
x, Int
i, SVal
r)

-- | 'Bounded' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => Bounded (WordN n) where
   minBound :: WordN n
minBound = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
0
   maxBound :: WordN n
maxBound = let sz :: Int
sz = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n) in Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer -> WordN n) -> Integer -> WordN n
forall a b. (a -> b) -> a -> b
$ Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
sz Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1

-- | 'Bounded' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => Bounded (IntN n) where
   minBound :: IntN n
minBound = let sz1 :: Int
sz1 = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 in Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> Integer -> IntN n
forall a b. (a -> b) -> a -> b
$ - (Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
sz1)
   maxBound :: IntN n
maxBound = let sz1 :: Int
sz1 = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 in Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> Integer -> IntN n
forall a b. (a -> b) -> a -> b
$ Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
sz1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1

-- | 'Num' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => Num (WordN n) where
   + :: WordN n -> WordN n -> WordN n
(+)         = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2 String
"(+)"    SVal -> SVal -> SVal
svPlus
   (-)         = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2 String
"(*)"    SVal -> SVal -> SVal
svMinus
   * :: WordN n -> WordN n -> WordN n
(*)         = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2 String
"(*)"    SVal -> SVal -> SVal
svTimes
   negate :: WordN n -> WordN n
negate      = String -> (SVal -> SVal) -> WordN n -> WordN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal) -> bv n -> bv n
lift1 String
"signum" SVal -> SVal
svUNeg
   abs :: WordN n -> WordN n
abs         = String -> (SVal -> SVal) -> WordN n -> WordN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal) -> bv n -> bv n
lift1 String
"abs"    SVal -> SVal
svAbs
   signum :: WordN n -> WordN n
signum      = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer -> WordN n) -> (WordN n -> Integer) -> WordN n -> WordN n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
signum   (Integer -> Integer) -> (WordN n -> Integer) -> WordN n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordN n -> Integer
forall a. Integral a => a -> Integer
toInteger
   fromInteger :: Integer -> WordN n
fromInteger = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer -> WordN n) -> (Integer -> Integer) -> Integer -> WordN n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Integer -> Integer
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Integer -> Integer)
-> (Integer -> Maybe Integer) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> Maybe Integer
svAsInteger (SVal -> Maybe Integer)
-> (Integer -> SVal) -> Integer -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Integer -> SVal
svInteger (WordN n -> Kind
forall a. HasKind a => a -> Kind
kindOf (WordN n
forall a. HasCallStack => a
undefined :: WordN n))

-- | 'Num' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => Num (IntN n) where
   + :: IntN n -> IntN n -> IntN n
(+)         = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2 String
"(+)"    SVal -> SVal -> SVal
svPlus
   (-)         = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2 String
"(*)"    SVal -> SVal -> SVal
svMinus
   * :: IntN n -> IntN n -> IntN n
(*)         = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2 String
"(*)"    SVal -> SVal -> SVal
svTimes
   negate :: IntN n -> IntN n
negate      = String -> (SVal -> SVal) -> IntN n -> IntN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal) -> bv n -> bv n
lift1 String
"signum" SVal -> SVal
svUNeg
   abs :: IntN n -> IntN n
abs         = String -> (SVal -> SVal) -> IntN n -> IntN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal) -> bv n -> bv n
lift1 String
"abs"    SVal -> SVal
svAbs
   signum :: IntN n -> IntN n
signum      = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> (IntN n -> Integer) -> IntN n -> IntN n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
signum   (Integer -> Integer) -> (IntN n -> Integer) -> IntN n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger
   fromInteger :: Integer -> IntN n
fromInteger = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> (Integer -> Integer) -> Integer -> IntN n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Integer -> Integer
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Integer -> Integer)
-> (Integer -> Maybe Integer) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> Maybe Integer
svAsInteger (SVal -> Maybe Integer)
-> (Integer -> SVal) -> Integer -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Integer -> SVal
svInteger (IntN n -> Kind
forall a. HasKind a => a -> Kind
kindOf (IntN n
forall a. HasCallStack => a
undefined :: IntN n))

-- | 'Enum' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => Enum (WordN n) where
   toEnum :: Int -> WordN n
toEnum   = Integer -> WordN n
forall a. Num a => Integer -> a
fromInteger  (Integer -> WordN n) -> (Int -> Integer) -> Int -> WordN n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger
   fromEnum :: WordN n -> Int
fromEnum = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> (WordN n -> Integer) -> WordN n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordN n -> Integer
forall a. Integral a => a -> Integer
toInteger

-- | 'Enum' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => Enum (IntN n) where
   toEnum :: Int -> IntN n
toEnum   = Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger  (Integer -> IntN n) -> (Int -> Integer) -> Int -> IntN n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger
   fromEnum :: IntN n -> Int
fromEnum = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> (IntN n -> Integer) -> IntN n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger

-- | 'Real' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => Real (WordN n) where
   toRational :: WordN n -> Rational
toRational (WordN Integer
x) = Integer -> Rational
forall a. Real a => a -> Rational
toRational Integer
x

-- | 'Real' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => Real (IntN n) where
   toRational :: IntN n -> Rational
toRational (IntN Integer
x) = Integer -> Rational
forall a. Real a => a -> Rational
toRational Integer
x

-- | 'Integral' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => Integral (WordN n) where
   toInteger :: WordN n -> Integer
toInteger (WordN Integer
x)           = Integer
x
   quotRem :: WordN n -> WordN n -> (WordN n, WordN n)
quotRem   (WordN Integer
x) (WordN Integer
y) = let (Integer
q, Integer
r) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
quotRem Integer
x Integer
y in (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
q, Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
r)

-- | 'Integral' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => Integral (IntN n) where
   toInteger :: IntN n -> Integer
toInteger (IntN Integer
x)          = Integer
x
   quotRem :: IntN n -> IntN n -> (IntN n, IntN n)
quotRem   (IntN Integer
x) (IntN Integer
y) = let (Integer
q, Integer
r) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
quotRem Integer
x Integer
y in (Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
q, Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
r)

--  'Bits' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => Bits (WordN n) where
   .&. :: WordN n -> WordN n -> WordN n
(.&.)        = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2   String
"(.&.)"      SVal -> SVal -> SVal
svAnd
   .|. :: WordN n -> WordN n -> WordN n
(.|.)        = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2   String
"(.|.)"      SVal -> SVal -> SVal
svOr
   xor :: WordN n -> WordN n -> WordN n
xor          = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2   String
"xor"        SVal -> SVal -> SVal
svXOr
   complement :: WordN n -> WordN n
complement   = String -> (SVal -> SVal) -> WordN n -> WordN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal) -> bv n -> bv n
lift1   String
"complement" SVal -> SVal
svNot
   shiftL :: WordN n -> Int -> WordN n
shiftL       = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> WordN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I  String
"shiftL"     SVal -> Int -> SVal
svShl
   shiftR :: WordN n -> Int -> WordN n
shiftR       = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> WordN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I  String
"shiftR"     SVal -> Int -> SVal
svShr
   rotateL :: WordN n -> Int -> WordN n
rotateL      = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> WordN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I  String
"rotateL"    SVal -> Int -> SVal
svRol
   rotateR :: WordN n -> Int -> WordN n
rotateR      = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> WordN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I  String
"rotateR"    SVal -> Int -> SVal
svRor
   testBit :: WordN n -> Int -> Bool
testBit      = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> Bool
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
lift2IB String
"svTestBit"  SVal -> Int -> SVal
svTestBit
   bitSizeMaybe :: WordN n -> Maybe Int
bitSizeMaybe = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (WordN n -> Int) -> WordN n -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> WordN n -> Int
forall a b. a -> b -> a
const (Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
   bitSize :: WordN n -> Int
bitSize WordN n
_    = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
   isSigned :: WordN n -> Bool
isSigned     = Kind -> Bool
forall a. HasKind a => a -> Bool
hasSign (Kind -> Bool) -> (WordN n -> Kind) -> WordN n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordN n -> Kind
forall a. HasKind a => a -> Kind
kindOf
   bit :: Int -> WordN n
bit Int
i        = WordN n
1 WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
`shiftL` Int
i
   popCount :: WordN n -> Int
popCount     = Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int) -> (WordN n -> Int) -> WordN n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a. Bits a => a -> Int
popCount (Integer -> Int) -> (WordN n -> Integer) -> WordN n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordN n -> Integer
forall a. Integral a => a -> Integer
toInteger

--  'Bits' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => Bits (IntN n) where
   .&. :: IntN n -> IntN n -> IntN n
(.&.)        = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2   String
"(.&.)"      SVal -> SVal -> SVal
svAnd
   .|. :: IntN n -> IntN n -> IntN n
(.|.)        = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2   String
"(.|.)"      SVal -> SVal -> SVal
svOr
   xor :: IntN n -> IntN n -> IntN n
xor          = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2   String
"xor"        SVal -> SVal -> SVal
svXOr
   complement :: IntN n -> IntN n
complement   = String -> (SVal -> SVal) -> IntN n -> IntN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal) -> bv n -> bv n
lift1   String
"complement" SVal -> SVal
svNot
   shiftL :: IntN n -> Int -> IntN n
shiftL       = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> IntN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I  String
"shiftL"     SVal -> Int -> SVal
svShl
   shiftR :: IntN n -> Int -> IntN n
shiftR       = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> IntN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I  String
"shiftR"     SVal -> Int -> SVal
svShr
   rotateL :: IntN n -> Int -> IntN n
rotateL      = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> IntN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I  String
"rotateL"    SVal -> Int -> SVal
svRol
   rotateR :: IntN n -> Int -> IntN n
rotateR      = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> IntN n
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I  String
"rotateR"    SVal -> Int -> SVal
svRor
   testBit :: IntN n -> Int -> Bool
testBit      = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> Bool
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
lift2IB String
"svTestBit"  SVal -> Int -> SVal
svTestBit
   bitSizeMaybe :: IntN n -> Maybe Int
bitSizeMaybe = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (IntN n -> Int) -> IntN n -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> IntN n -> Int
forall a b. a -> b -> a
const (Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
   bitSize :: IntN n -> Int
bitSize IntN n
_    = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
   isSigned :: IntN n -> Bool
isSigned     = Kind -> Bool
forall a. HasKind a => a -> Bool
hasSign (Kind -> Bool) -> (IntN n -> Kind) -> IntN n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntN n -> Kind
forall a. HasKind a => a -> Kind
kindOf
   bit :: Int -> IntN n
bit Int
i        = IntN n
1 IntN n -> Int -> IntN n
forall a. Bits a => a -> Int -> a
`shiftL` Int
i
   popCount :: IntN n -> Int
popCount     = Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int) -> (IntN n -> Int) -> IntN n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a. Bits a => a -> Int
popCount (Integer -> Int) -> (IntN n -> Integer) -> IntN n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger

-- | 'SIntegral' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => SIntegral (WordN n)

-- | 'SIntegral' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => SIntegral (IntN n)

-- | 'SDivisible' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => SDivisible (WordN n) where
  sQuotRem :: WordN n -> WordN n -> (WordN n, WordN n)
sQuotRem WordN n
x WordN n
0 = (WordN n
0, WordN n
x)
  sQuotRem WordN n
x WordN n
y = WordN n
x WordN n -> WordN n -> (WordN n, WordN n)
forall a. Integral a => a -> a -> (a, a)
`quotRem` WordN n
y
  sDivMod :: WordN n -> WordN n -> (WordN n, WordN n)
sDivMod  WordN n
x WordN n
0 = (WordN n
0, WordN n
x)
  sDivMod  WordN n
x WordN n
y = WordN n
x WordN n -> WordN n -> (WordN n, WordN n)
forall a. Integral a => a -> a -> (a, a)
`divMod` WordN n
y

-- | 'SDivisible' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => SDivisible (IntN n) where
  sQuotRem :: IntN n -> IntN n -> (IntN n, IntN n)
sQuotRem IntN n
x IntN n
0 = (IntN n
0, IntN n
x)
  sQuotRem IntN n
x IntN n
y = IntN n
x IntN n -> IntN n -> (IntN n, IntN n)
forall a. Integral a => a -> a -> (a, a)
`quotRem` IntN n
y
  sDivMod :: IntN n -> IntN n -> (IntN n, IntN n)
sDivMod  IntN n
x IntN n
0 = (IntN n
0, IntN n
x)
  sDivMod  IntN n
x IntN n
y = IntN n
x IntN n -> IntN n -> (IntN n, IntN n)
forall a. Integral a => a -> a -> (a, a)
`divMod` IntN n
y

-- | 'SDivisible' instance for 'SWord'
instance (KnownNat n, BVIsNonZero n) => SDivisible (SWord n) where
  sQuotRem :: SWord n -> SWord n -> (SWord n, SWord n)
sQuotRem = SWord n -> SWord n -> (SWord n, SWord n)
forall a. (Eq a, SymVal a) => SBV a -> SBV a -> (SBV a, SBV a)
liftQRem
  sDivMod :: SWord n -> SWord n -> (SWord n, SWord n)
sDivMod  = SWord n -> SWord n -> (SWord n, SWord n)
forall a.
(Ord a, SymVal a, Num a, SDivisible (SBV a)) =>
SBV a -> SBV a -> (SBV a, SBV a)
liftDMod

-- | 'SDivisible' instance for 'SInt'
instance (KnownNat n, BVIsNonZero n) => SDivisible (SInt n) where
  sQuotRem :: SInt n -> SInt n -> (SInt n, SInt n)
sQuotRem = SInt n -> SInt n -> (SInt n, SInt n)
forall a. (Eq a, SymVal a) => SBV a -> SBV a -> (SBV a, SBV a)
liftQRem
  sDivMod :: SInt n -> SInt n -> (SInt n, SInt n)
sDivMod  = SInt n -> SInt n -> (SInt n, SInt n)
forall a.
(Ord a, SymVal a, Num a, SDivisible (SBV a)) =>
SBV a -> SBV a -> (SBV a, SBV a)
liftDMod

-- | 'SFiniteBits' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => SFiniteBits (WordN n) where
   sFiniteBitSize :: SBV (WordN n) -> Int
sFiniteBitSize SBV (WordN n)
_ = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n)

-- | 'SFiniteBits' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => SFiniteBits (IntN n) where
   sFiniteBitSize :: SBV (IntN n) -> Int
sFiniteBitSize SBV (IntN n)
_ = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n)

-- | Constructing models for 'WordN'
instance (KnownNat n, BVIsNonZero n) => SatModel (WordN n) where
  parseCVs :: [CV] -> Maybe (WordN n, [CV])
parseCVs = Kind -> [CV] -> Maybe (WordN n, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (WordN n -> Kind
forall a. HasKind a => a -> Kind
kindOf (WordN n
forall a. HasCallStack => a
undefined :: WordN n))

-- | Constructing models for 'IntN'
instance (KnownNat n, BVIsNonZero n) => SatModel (IntN n) where
  parseCVs :: [CV] -> Maybe (IntN n, [CV])
parseCVs = Kind -> [CV] -> Maybe (IntN n, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (IntN n -> Kind
forall a. HasKind a => a -> Kind
kindOf (IntN n
forall a. HasCallStack => a
undefined :: IntN n))

-- | Optimizing 'WordN'
instance (KnownNat n, BVIsNonZero n) => Metric (WordN n)

-- | Optimizing 'IntN'
instance (KnownNat n, BVIsNonZero n) => Metric (IntN n) where
  type MetricSpace (IntN n) = WordN n
  toMetricSpace :: SBV (IntN n) -> SBV (MetricSpace (IntN n))
toMetricSpace    SBV (IntN n)
x        = SBV (IntN n) -> SBV (WordN n)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SBV (IntN n)
x SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
forall a. Num a => a -> a -> a
+ SBV (WordN n)
2 SBV (WordN n) -> Int -> SBV (WordN n)
forall a b. (Num a, Integral b) => a -> b -> a
^ (Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
  fromMetricSpace :: SBV (MetricSpace (IntN n)) -> SBV (IntN n)
fromMetricSpace  SBV (MetricSpace (IntN n))
x        = SBV (WordN n) -> SBV (IntN n)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SBV (MetricSpace (IntN n))
SBV (WordN n)
x SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
forall a. Num a => a -> a -> a
- SBV (IntN n)
2 SBV (IntN n) -> Int -> SBV (IntN n)
forall a b. (Num a, Integral b) => a -> b -> a
^ (Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

-- | Generalization of 'Data.SBV.sWord'
sWord :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => String -> m (SWord n)
sWord :: String -> m (SWord n)
sWord = String -> m (SWord n)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sWord_'
sWord_ :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => m (SWord n)
sWord_ :: m (SWord n)
sWord_ = m (SWord n)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sWord64s'
sWords :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => [String] -> m [SWord n]
sWords :: [String] -> m [SWord n]
sWords = [String] -> m [SWord n]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sInt'
sInt :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => String -> m (SInt n)
sInt :: String -> m (SInt n)
sInt = String -> m (SInt n)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sInt_'
sInt_ :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => m (SInt n)
sInt_ :: m (SInt n)
sInt_ = m (SInt n)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sInts'
sInts :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => [String] -> m [SInt n]
sInts :: [String] -> m [SInt n]
sInts = [String] -> m [SInt n]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Extract a portion of bits to form a smaller bit-vector.
--
-- >>> prove $ \x -> bvExtract (Proxy @7) (Proxy @3) (x :: SWord 12) .== bvDrop (Proxy @4) (bvTake (Proxy @9) x)
-- Q.E.D.
bvExtract :: forall i j n bv proxy. ( KnownNat n, BVIsNonZero n, SymVal (bv n)
                                    , KnownNat i
                                    , KnownNat j
                                    , i + 1 <= n
                                    , j <= i
                                    , BVIsNonZero (i - j + 1)
                                    ) => proxy i                -- ^ @i@: Start position, numbered from @n-1@ to @0@
                                      -> proxy j                -- ^ @j@: End position, numbered from @n-1@ to @0@, @j <= i@ must hold
                                      -> SBV (bv n)             -- ^ Input bit vector of size @n@
                                      -> SBV (bv (i - j + 1))   -- ^ Output is of size @i - j + 1@
bvExtract :: proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract proxy i
start proxy j
end = SVal -> SBV (bv ((i - j) + 1))
forall a. SVal -> SBV a
SBV (SVal -> SBV (bv ((i - j) + 1)))
-> (SBV (bv n) -> SVal) -> SBV (bv n) -> SBV (bv ((i - j) + 1))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> SVal -> SVal
svExtract Int
i Int
j (SVal -> SVal) -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV (bv n) -> SVal
forall a. SBV a -> SVal
unSBV
   where i :: Int
i  = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (proxy i -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy i
start)
         j :: Int
j  = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (proxy j -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy j
end)

-- | Join two bitvectors.
--
-- >>> prove $ \x y -> x .== bvExtract (Proxy @79) (Proxy @71) ((x :: SWord 9) # (y :: SWord 71))
-- Q.E.D.
(#) :: ( KnownNat n, BVIsNonZero n, SymVal (bv n)
       , KnownNat m, BVIsNonZero m, SymVal (bv m)
       ) => SBV (bv n)                     -- ^ First input, of size @n@, becomes the left side
         -> SBV (bv m)                     -- ^ Second input, of size @m@, becomes the right side
         -> SBV (bv (n + m))               -- ^ Concatenation, of size @n+m@
SBV (bv n)
n # :: SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SBV (bv m)
m = SVal -> SBV (bv (n + m))
forall a. SVal -> SBV a
SBV (SVal -> SBV (bv (n + m))) -> SVal -> SBV (bv (n + m))
forall a b. (a -> b) -> a -> b
$ SVal -> SVal -> SVal
svJoin (SBV (bv n) -> SVal
forall a. SBV a -> SVal
unSBV SBV (bv n)
n) (SBV (bv m) -> SVal
forall a. SBV a -> SVal
unSBV SBV (bv m)
m)
infixr 5 #

-- | Zero extend a bit-vector.
--
-- >>> prove $ \x -> bvExtract (Proxy @20) (Proxy @12) (zeroExtend (x :: SInt 12) :: SInt 21) .== 0
-- Q.E.D.
zeroExtend :: forall n m bv. ( KnownNat n, BVIsNonZero n, SymVal (bv n)
                             , KnownNat m, BVIsNonZero m, SymVal (bv m)
                             , n + 1 <= m
                             , SIntegral (bv (m - n))
                             , BVIsNonZero (m - n)
                             ) => SBV (bv n)    -- ^ Input, of size @n@
                               -> SBV (bv m)    -- ^ Output, of size @m@. @n < m@ must hold
zeroExtend :: SBV (bv n) -> SBV (bv m)
zeroExtend SBV (bv n)
n = SVal -> SBV (bv m)
forall a. SVal -> SBV a
SBV (SVal -> SBV (bv m)) -> SVal -> SBV (bv m)
forall a b. (a -> b) -> a -> b
$ SVal -> SVal -> SVal
svJoin (SBV (bv (m - n)) -> SVal
forall a. SBV a -> SVal
unSBV SBV (bv (m - n))
zero) (SBV (bv n) -> SVal
forall a. SBV a -> SVal
unSBV SBV (bv n)
n)
  where zero :: SBV (bv (m - n))
        zero :: SBV (bv (m - n))
zero = bv (m - n) -> SBV (bv (m - n))
forall a. SymVal a => a -> SBV a
literal bv (m - n)
0

-- | Sign extend a bit-vector.
--
-- >>> prove $ \x -> sNot (msb x) .=> bvExtract (Proxy @20) (Proxy @12) (signExtend (x :: SInt 12) :: SInt 21) .== 0
-- Q.E.D.
-- >>> prove $ \x ->       msb x  .=> bvExtract (Proxy @20) (Proxy @12) (signExtend (x :: SInt 12) :: SInt 21) .== complement 0
-- Q.E.D.
signExtend :: forall n m bv. ( KnownNat n, BVIsNonZero n, SymVal (bv n)
                             , KnownNat m, BVIsNonZero m, SymVal (bv m)
                             , n + 1 <= m
                             , SFiniteBits (bv n)
                             , SIntegral   (bv (m - n))
                             , BVIsNonZero   (m - n)
                             ) => SBV (bv n)  -- ^ Input, of size @n@
                               -> SBV (bv m)  -- ^ Output, of size @m@. @n < m@ must hold
signExtend :: SBV (bv n) -> SBV (bv m)
signExtend SBV (bv n)
n = SVal -> SBV (bv m)
forall a. SVal -> SBV a
SBV (SVal -> SBV (bv m)) -> SVal -> SBV (bv m)
forall a b. (a -> b) -> a -> b
$ SVal -> SVal -> SVal
svJoin (SBV (bv (m - n)) -> SVal
forall a. SBV a -> SVal
unSBV SBV (bv (m - n))
ext) (SBV (bv n) -> SVal
forall a. SBV a -> SVal
unSBV SBV (bv n)
n)
  where zero, ones, ext :: SBV (bv (m - n))
        zero :: SBV (bv (m - n))
zero = bv (m - n) -> SBV (bv (m - n))
forall a. SymVal a => a -> SBV a
literal bv (m - n)
0
        ones :: SBV (bv (m - n))
ones = SBV (bv (m - n)) -> SBV (bv (m - n))
forall a. Bits a => a -> a
complement SBV (bv (m - n))
zero
        ext :: SBV (bv (m - n))
ext  = SBool -> SBV (bv (m - n)) -> SBV (bv (m - n)) -> SBV (bv (m - n))
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV (bv n) -> SBool
forall a. SFiniteBits a => SBV a -> SBool
msb SBV (bv n)
n) SBV (bv (m - n))
ones SBV (bv (m - n))
zero

-- | Drop bits from the top of a bit-vector.
--
-- >>> prove $ \x -> bvDrop (Proxy @0) (x :: SWord 43) .== x
-- Q.E.D.
-- >>> prove $ \x -> bvDrop (Proxy @20) (x :: SWord 21) .== ite (lsb x) 1 0
-- Q.E.D.
bvDrop :: forall i n m bv proxy. ( KnownNat n, BVIsNonZero n
                                 , KnownNat i
                                 , i + 1 <= n
                                 , i + m - n <= 0
                                 , BVIsNonZero (n - i)
                                 ) => proxy i                    -- ^ @i@: Number of bits to drop. @i < n@ must hold.
                                   -> SBV (bv n)                 -- ^ Input, of size @n@
                                   -> SBV (bv m)                 -- ^ Output, of size @m@. @m = n - i@ holds.
bvDrop :: proxy i -> SBV (bv n) -> SBV (bv m)
bvDrop proxy i
i = SVal -> SBV (bv m)
forall a. SVal -> SBV a
SBV (SVal -> SBV (bv m))
-> (SBV (bv n) -> SVal) -> SBV (bv n) -> SBV (bv m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> SVal -> SVal
svExtract Int
start Int
0 (SVal -> SVal) -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV (bv n) -> SVal
forall a. SBV a -> SVal
unSBV
  where nv :: Int
nv    = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
        start :: Int
start = Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
- Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (proxy i -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy i
i) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

-- | Take bits from the top of a bit-vector.
--
-- >>> prove $ \x -> bvTake (Proxy @13) (x :: SWord 13) .== x
-- Q.E.D.
-- >>> prove $ \x -> bvTake (Proxy @1) (x :: SWord 13) .== ite (msb x) 1 0
-- Q.E.D.
-- >>> prove $ \x -> bvTake (Proxy @4) x # bvDrop (Proxy @4) x .== (x :: SWord 23)
-- Q.E.D.
bvTake :: forall i n bv proxy. ( KnownNat n, BVIsNonZero n
                               , KnownNat i, BVIsNonZero i
                               , i <= n
                               ) => proxy i                  -- ^ @i@: Number of bits to take. @0 < i <= n@ must hold.
                                 -> SBV (bv n)               -- ^ Input, of size @n@
                                 -> SBV (bv i)               -- ^ Output, of size @i@
bvTake :: proxy i -> SBV (bv n) -> SBV (bv i)
bvTake proxy i
i = SVal -> SBV (bv i)
forall a. SVal -> SBV a
SBV (SVal -> SBV (bv i))
-> (SBV (bv n) -> SVal) -> SBV (bv n) -> SBV (bv i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> SVal -> SVal
svExtract Int
start Int
end (SVal -> SVal) -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV (bv n) -> SVal
forall a. SBV a -> SVal
unSBV
  where nv :: Int
nv    = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
        start :: Int
start = Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
        end :: Int
end   = Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
- Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (proxy i -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy i
i) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1

-- | A helper class to convert sized bit-vectors to/from bytes.
class ByteConverter a where
   -- | Convert to a sequence of bytes
   --
   -- >>> prove $ \a b c d -> toBytes ((fromBytes [a, b, c, d]) :: SWord 32) .== [a, b, c, d]
   -- Q.E.D.
   toBytes   :: a -> [SWord 8]

   -- | Convert from a sequence of bytes
   --
   -- >>> prove $ \r -> fromBytes (toBytes r) .== (r :: SWord 64)
   -- Q.E.D.
   fromBytes :: [SWord 8] -> a

-- NB. The following instances are automatically generated by buildUtils/genByteConverter.hs
-- It is possible to write these more compactly indeed, but this explicit form generates
-- better C code, and hence we allow the verbosity here.

-- | 'SWord' 8 instance for 'ByteConverter'
instance ByteConverter (SWord 8) where
   toBytes :: SWord 8 -> [SWord 8]
toBytes SWord 8
a = [SWord 8
a]

   fromBytes :: [SWord 8] -> SWord 8
fromBytes [SWord 8
x] = SWord 8
x
   fromBytes [SWord 8]
as  = String -> SWord 8
forall a. HasCallStack => String -> a
error (String -> SWord 8) -> String -> SWord 8
forall a b. (a -> b) -> a -> b
$ String
"fromBytes:SWord 8: Incorrect number of bytes: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([SWord 8] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
as)

-- | 'SWord' 16 instance for 'ByteConverter'
instance ByteConverter (SWord 16) where
   toBytes :: SWord 16 -> [SWord 8]
toBytes SWord 16
a = [ Proxy 15 -> Proxy 8 -> SWord 16 -> SBV (WordN ((15 - 8) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 15
forall k (t :: k). Proxy t
Proxy @15) (Proxy 8
forall k (t :: k). Proxy t
Proxy  @8) SWord 16
a
               , Proxy 7 -> Proxy 0 -> SWord 16 -> SBV (WordN ((7 - 0) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 7
forall k (t :: k). Proxy t
Proxy  @7) (Proxy 0
forall k (t :: k). Proxy t
Proxy  @0) SWord 16
a
               ]

   fromBytes :: [SWord 8] -> SWord 16
fromBytes [SWord 8]
as
     | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2
     = ([SWord 8] -> SWord 8
forall a. ByteConverter a => [SWord 8] -> a
fromBytes :: [SWord 8] -> SWord 8) (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
take Int
1 [SWord 8]
as) SWord 8 -> SWord 8 -> SBV (WordN (8 + 8))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# [SWord 8] -> SWord 8
forall a. ByteConverter a => [SWord 8] -> a
fromBytes (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
1 [SWord 8]
as)
     | Bool
True
     = String -> SWord 16
forall a. HasCallStack => String -> a
error (String -> SWord 16) -> String -> SWord 16
forall a b. (a -> b) -> a -> b
$ String
"fromBytes:SWord 16: Incorrect number of bytes: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l
     where l :: Int
l = [SWord 8] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
as

-- | 'SWord' 32 instance for 'ByteConverter'
instance ByteConverter (SWord 32) where
   toBytes :: SWord 32 -> [SWord 8]
toBytes SWord 32
a = [ Proxy 31 -> Proxy 24 -> SWord 32 -> SBV (WordN ((31 - 24) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 31
forall k (t :: k). Proxy t
Proxy @31) (Proxy 24
forall k (t :: k). Proxy t
Proxy @24) SWord 32
a, Proxy 23 -> Proxy 16 -> SWord 32 -> SBV (WordN ((23 - 16) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 23
forall k (t :: k). Proxy t
Proxy @23) (Proxy 16
forall k (t :: k). Proxy t
Proxy @16) SWord 32
a, Proxy 15 -> Proxy 8 -> SWord 32 -> SBV (WordN ((15 - 8) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 15
forall k (t :: k). Proxy t
Proxy @15) (Proxy 8
forall k (t :: k). Proxy t
Proxy  @8) SWord 32
a, Proxy 7 -> Proxy 0 -> SWord 32 -> SBV (WordN ((7 - 0) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 7
forall k (t :: k). Proxy t
Proxy  @7) (Proxy 0
forall k (t :: k). Proxy t
Proxy  @0) SWord 32
a
               ]

   fromBytes :: [SWord 8] -> SWord 32
fromBytes [SWord 8]
as
     | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4
     = ([SWord 8] -> SWord 16
forall a. ByteConverter a => [SWord 8] -> a
fromBytes :: [SWord 8] -> SWord 16) (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
take Int
2 [SWord 8]
as) SWord 16 -> SWord 16 -> SBV (WordN (16 + 16))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# [SWord 8] -> SWord 16
forall a. ByteConverter a => [SWord 8] -> a
fromBytes (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
2 [SWord 8]
as)
     | Bool
True
     = String -> SWord 32
forall a. HasCallStack => String -> a
error (String -> SWord 32) -> String -> SWord 32
forall a b. (a -> b) -> a -> b
$ String
"fromBytes:SWord 32: Incorrect number of bytes: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l
     where l :: Int
l = [SWord 8] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
as

-- | 'SWord' 64 instance for 'ByteConverter'
instance ByteConverter (SWord 64) where
   toBytes :: SWord 64 -> [SWord 8]
toBytes SWord 64
a = [ Proxy 63 -> Proxy 56 -> SWord 64 -> SBV (WordN ((63 - 56) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 63
forall k (t :: k). Proxy t
Proxy @63) (Proxy 56
forall k (t :: k). Proxy t
Proxy @56) SWord 64
a, Proxy 55 -> Proxy 48 -> SWord 64 -> SBV (WordN ((55 - 48) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 55
forall k (t :: k). Proxy t
Proxy @55) (Proxy 48
forall k (t :: k). Proxy t
Proxy @48) SWord 64
a, Proxy 47 -> Proxy 40 -> SWord 64 -> SBV (WordN ((47 - 40) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 47
forall k (t :: k). Proxy t
Proxy @47) (Proxy 40
forall k (t :: k). Proxy t
Proxy @40) SWord 64
a, Proxy 39 -> Proxy 32 -> SWord 64 -> SBV (WordN ((39 - 32) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 39
forall k (t :: k). Proxy t
Proxy @39) (Proxy 32
forall k (t :: k). Proxy t
Proxy @32) SWord 64
a
               , Proxy 31 -> Proxy 24 -> SWord 64 -> SBV (WordN ((31 - 24) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 31
forall k (t :: k). Proxy t
Proxy @31) (Proxy 24
forall k (t :: k). Proxy t
Proxy @24) SWord 64
a, Proxy 23 -> Proxy 16 -> SWord 64 -> SBV (WordN ((23 - 16) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 23
forall k (t :: k). Proxy t
Proxy @23) (Proxy 16
forall k (t :: k). Proxy t
Proxy @16) SWord 64
a, Proxy 15 -> Proxy 8 -> SWord 64 -> SBV (WordN ((15 - 8) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 15
forall k (t :: k). Proxy t
Proxy @15) (Proxy 8
forall k (t :: k). Proxy t
Proxy  @8) SWord 64
a, Proxy 7 -> Proxy 0 -> SWord 64 -> SBV (WordN ((7 - 0) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 7
forall k (t :: k). Proxy t
Proxy  @7) (Proxy 0
forall k (t :: k). Proxy t
Proxy  @0) SWord 64
a
               ]

   fromBytes :: [SWord 8] -> SWord 64
fromBytes [SWord 8]
as
     | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
8
     = ([SWord 8] -> SWord 32
forall a. ByteConverter a => [SWord 8] -> a
fromBytes :: [SWord 8] -> SWord 32) (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
take Int
4 [SWord 8]
as) SWord 32 -> SWord 32 -> SBV (WordN (32 + 32))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# [SWord 8] -> SWord 32
forall a. ByteConverter a => [SWord 8] -> a
fromBytes (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
4 [SWord 8]
as)
     | Bool
True
     = String -> SWord 64
forall a. HasCallStack => String -> a
error (String -> SWord 64) -> String -> SWord 64
forall a b. (a -> b) -> a -> b
$ String
"fromBytes:SWord 64: Incorrect number of bytes: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l
     where l :: Int
l = [SWord 8] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
as

-- | 'SWord' 128 instance for 'ByteConverter'
instance ByteConverter (SWord 128) where
   toBytes :: SWord 128 -> [SWord 8]
toBytes SWord 128
a = [ Proxy 127
-> Proxy 120 -> SWord 128 -> SBV (WordN ((127 - 120) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 127
forall k (t :: k). Proxy t
Proxy @127) (Proxy 120
forall k (t :: k). Proxy t
Proxy @120) SWord 128
a, Proxy 119
-> Proxy 112 -> SWord 128 -> SBV (WordN ((119 - 112) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 119
forall k (t :: k). Proxy t
Proxy @119) (Proxy 112
forall k (t :: k). Proxy t
Proxy @112) SWord 128
a, Proxy 111
-> Proxy 104 -> SWord 128 -> SBV (WordN ((111 - 104) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 111
forall k (t :: k). Proxy t
Proxy @111) (Proxy 104
forall k (t :: k). Proxy t
Proxy @104) SWord 128
a, Proxy 103 -> Proxy 96 -> SWord 128 -> SBV (WordN ((103 - 96) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 103
forall k (t :: k). Proxy t
Proxy @103) (Proxy 96
forall k (t :: k). Proxy t
Proxy  @96) SWord 128
a
               , Proxy 95 -> Proxy 88 -> SWord 128 -> SBV (WordN ((95 - 88) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 95
forall k (t :: k). Proxy t
Proxy  @95) (Proxy 88
forall k (t :: k). Proxy t
Proxy  @88) SWord 128
a, Proxy 87 -> Proxy 80 -> SWord 128 -> SBV (WordN ((87 - 80) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 87
forall k (t :: k). Proxy t
Proxy  @87) (Proxy 80
forall k (t :: k). Proxy t
Proxy  @80) SWord 128
a, Proxy 79 -> Proxy 72 -> SWord 128 -> SBV (WordN ((79 - 72) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 79
forall k (t :: k). Proxy t
Proxy  @79) (Proxy 72
forall k (t :: k). Proxy t
Proxy  @72) SWord 128
a, Proxy 71 -> Proxy 64 -> SWord 128 -> SBV (WordN ((71 - 64) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 71
forall k (t :: k). Proxy t
Proxy  @71) (Proxy 64
forall k (t :: k). Proxy t
Proxy  @64) SWord 128
a
               , Proxy 63 -> Proxy 56 -> SWord 128 -> SBV (WordN ((63 - 56) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 63
forall k (t :: k). Proxy t
Proxy  @63) (Proxy 56
forall k (t :: k). Proxy t
Proxy  @56) SWord 128
a, Proxy 55 -> Proxy 48 -> SWord 128 -> SBV (WordN ((55 - 48) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 55
forall k (t :: k). Proxy t
Proxy  @55) (Proxy 48
forall k (t :: k). Proxy t
Proxy  @48) SWord 128
a, Proxy 47 -> Proxy 40 -> SWord 128 -> SBV (WordN ((47 - 40) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 47
forall k (t :: k). Proxy t
Proxy  @47) (Proxy 40
forall k (t :: k). Proxy t
Proxy  @40) SWord 128
a, Proxy 39 -> Proxy 32 -> SWord 128 -> SBV (WordN ((39 - 32) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 39
forall k (t :: k). Proxy t
Proxy  @39) (Proxy 32
forall k (t :: k). Proxy t
Proxy  @32) SWord 128
a
               , Proxy 31 -> Proxy 24 -> SWord 128 -> SBV (WordN ((31 - 24) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 31
forall k (t :: k). Proxy t
Proxy  @31) (Proxy 24
forall k (t :: k). Proxy t
Proxy  @24) SWord 128
a, Proxy 23 -> Proxy 16 -> SWord 128 -> SBV (WordN ((23 - 16) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 23
forall k (t :: k). Proxy t
Proxy  @23) (Proxy 16
forall k (t :: k). Proxy t
Proxy  @16) SWord 128
a, Proxy 15 -> Proxy 8 -> SWord 128 -> SBV (WordN ((15 - 8) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 15
forall k (t :: k). Proxy t
Proxy  @15) (Proxy 8
forall k (t :: k). Proxy t
Proxy   @8) SWord 128
a, Proxy 7 -> Proxy 0 -> SWord 128 -> SBV (WordN ((7 - 0) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 7
forall k (t :: k). Proxy t
Proxy   @7) (Proxy 0
forall k (t :: k). Proxy t
Proxy   @0) SWord 128
a
               ]

   fromBytes :: [SWord 8] -> SWord 128
fromBytes [SWord 8]
as
     | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
16
     = ([SWord 8] -> SWord 64
forall a. ByteConverter a => [SWord 8] -> a
fromBytes :: [SWord 8] -> SWord 64) (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
take Int
8 [SWord 8]
as) SWord 64 -> SWord 64 -> SBV (WordN (64 + 64))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# [SWord 8] -> SWord 64
forall a. ByteConverter a => [SWord 8] -> a
fromBytes (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
8 [SWord 8]
as)
     | Bool
True
     = String -> SWord 128
forall a. HasCallStack => String -> a
error (String -> SWord 128) -> String -> SWord 128
forall a b. (a -> b) -> a -> b
$ String
"fromBytes:SWord 128: Incorrect number of bytes: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l
     where l :: Int
l = [SWord 8] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
as

-- | 'SWord' 256 instance for 'ByteConverter'
instance ByteConverter (SWord 256) where
   toBytes :: SWord 256 -> [SWord 8]
toBytes SWord 256
a = [ Proxy 255
-> Proxy 248 -> SWord 256 -> SBV (WordN ((255 - 248) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 255
forall k (t :: k). Proxy t
Proxy @255) (Proxy 248
forall k (t :: k). Proxy t
Proxy @248) SWord 256
a, Proxy 247
-> Proxy 240 -> SWord 256 -> SBV (WordN ((247 - 240) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 247
forall k (t :: k). Proxy t
Proxy @247) (Proxy 240
forall k (t :: k). Proxy t
Proxy @240) SWord 256
a, Proxy 239
-> Proxy 232 -> SWord 256 -> SBV (WordN ((239 - 232) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 239
forall k (t :: k). Proxy t
Proxy @239) (Proxy 232
forall k (t :: k). Proxy t
Proxy @232) SWord 256
a, Proxy 231
-> Proxy 224 -> SWord 256 -> SBV (WordN ((231 - 224) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 231
forall k (t :: k). Proxy t
Proxy @231) (Proxy 224
forall k (t :: k). Proxy t
Proxy @224) SWord 256
a
               , Proxy 223
-> Proxy 216 -> SWord 256 -> SBV (WordN ((223 - 216) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 223
forall k (t :: k). Proxy t
Proxy @223) (Proxy 216
forall k (t :: k). Proxy t
Proxy @216) SWord 256
a, Proxy 215
-> Proxy 208 -> SWord 256 -> SBV (WordN ((215 - 208) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 215
forall k (t :: k). Proxy t
Proxy @215) (Proxy 208
forall k (t :: k). Proxy t
Proxy @208) SWord 256
a, Proxy 207
-> Proxy 200 -> SWord 256 -> SBV (WordN ((207 - 200) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 207
forall k (t :: k). Proxy t
Proxy @207) (Proxy 200
forall k (t :: k). Proxy t
Proxy @200) SWord 256
a, Proxy 199
-> Proxy 192 -> SWord 256 -> SBV (WordN ((199 - 192) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 199
forall k (t :: k). Proxy t
Proxy @199) (Proxy 192
forall k (t :: k). Proxy t
Proxy @192) SWord 256
a
               , Proxy 191
-> Proxy 184 -> SWord 256 -> SBV (WordN ((191 - 184) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 191
forall k (t :: k). Proxy t
Proxy @191) (Proxy 184
forall k (t :: k). Proxy t
Proxy @184) SWord 256
a, Proxy 183
-> Proxy 176 -> SWord 256 -> SBV (WordN ((183 - 176) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 183
forall k (t :: k). Proxy t
Proxy @183) (Proxy 176
forall k (t :: k). Proxy t
Proxy @176) SWord 256
a, Proxy 175
-> Proxy 168 -> SWord 256 -> SBV (WordN ((175 - 168) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 175
forall k (t :: k). Proxy t
Proxy @175) (Proxy 168
forall k (t :: k). Proxy t
Proxy @168) SWord 256
a, Proxy 167
-> Proxy 160 -> SWord 256 -> SBV (WordN ((167 - 160) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 167
forall k (t :: k). Proxy t
Proxy @167) (Proxy 160
forall k (t :: k). Proxy t
Proxy @160) SWord 256
a
               , Proxy 159
-> Proxy 152 -> SWord 256 -> SBV (WordN ((159 - 152) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 159
forall k (t :: k). Proxy t
Proxy @159) (Proxy 152
forall k (t :: k). Proxy t
Proxy @152) SWord 256
a, Proxy 151
-> Proxy 144 -> SWord 256 -> SBV (WordN ((151 - 144) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 151
forall k (t :: k). Proxy t
Proxy @151) (Proxy 144
forall k (t :: k). Proxy t
Proxy @144) SWord 256
a, Proxy 143
-> Proxy 136 -> SWord 256 -> SBV (WordN ((143 - 136) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 143
forall k (t :: k). Proxy t
Proxy @143) (Proxy 136
forall k (t :: k). Proxy t
Proxy @136) SWord 256
a, Proxy 135
-> Proxy 128 -> SWord 256 -> SBV (WordN ((135 - 128) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 135
forall k (t :: k). Proxy t
Proxy @135) (Proxy 128
forall k (t :: k). Proxy t
Proxy @128) SWord 256
a
               , Proxy 127
-> Proxy 120 -> SWord 256 -> SBV (WordN ((127 - 120) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 127
forall k (t :: k). Proxy t
Proxy @127) (Proxy 120
forall k (t :: k). Proxy t
Proxy @120) SWord 256
a, Proxy 119
-> Proxy 112 -> SWord 256 -> SBV (WordN ((119 - 112) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 119
forall k (t :: k). Proxy t
Proxy @119) (Proxy 112
forall k (t :: k). Proxy t
Proxy @112) SWord 256
a, Proxy 111
-> Proxy 104 -> SWord 256 -> SBV (WordN ((111 - 104) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 111
forall k (t :: k). Proxy t
Proxy @111) (Proxy 104
forall k (t :: k). Proxy t
Proxy @104) SWord 256
a, Proxy 103 -> Proxy 96 -> SWord 256 -> SBV (WordN ((103 - 96) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 103
forall k (t :: k). Proxy t
Proxy @103) (Proxy 96
forall k (t :: k). Proxy t
Proxy  @96) SWord 256
a
               , Proxy 95 -> Proxy 88 -> SWord 256 -> SBV (WordN ((95 - 88) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 95
forall k (t :: k). Proxy t
Proxy  @95) (Proxy 88
forall k (t :: k). Proxy t
Proxy  @88) SWord 256
a, Proxy 87 -> Proxy 80 -> SWord 256 -> SBV (WordN ((87 - 80) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 87
forall k (t :: k). Proxy t
Proxy  @87) (Proxy 80
forall k (t :: k). Proxy t
Proxy  @80) SWord 256
a, Proxy 79 -> Proxy 72 -> SWord 256 -> SBV (WordN ((79 - 72) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 79
forall k (t :: k). Proxy t
Proxy  @79) (Proxy 72
forall k (t :: k). Proxy t
Proxy  @72) SWord 256
a, Proxy 71 -> Proxy 64 -> SWord 256 -> SBV (WordN ((71 - 64) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 71
forall k (t :: k). Proxy t
Proxy  @71) (Proxy 64
forall k (t :: k). Proxy t
Proxy  @64) SWord 256
a
               , Proxy 63 -> Proxy 56 -> SWord 256 -> SBV (WordN ((63 - 56) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 63
forall k (t :: k). Proxy t
Proxy  @63) (Proxy 56
forall k (t :: k). Proxy t
Proxy  @56) SWord 256
a, Proxy 55 -> Proxy 48 -> SWord 256 -> SBV (WordN ((55 - 48) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 55
forall k (t :: k). Proxy t
Proxy  @55) (Proxy 48
forall k (t :: k). Proxy t
Proxy  @48) SWord 256
a, Proxy 47 -> Proxy 40 -> SWord 256 -> SBV (WordN ((47 - 40) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 47
forall k (t :: k). Proxy t
Proxy  @47) (Proxy 40
forall k (t :: k). Proxy t
Proxy  @40) SWord 256
a, Proxy 39 -> Proxy 32 -> SWord 256 -> SBV (WordN ((39 - 32) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 39
forall k (t :: k). Proxy t
Proxy  @39) (Proxy 32
forall k (t :: k). Proxy t
Proxy  @32) SWord 256
a
               , Proxy 31 -> Proxy 24 -> SWord 256 -> SBV (WordN ((31 - 24) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 31
forall k (t :: k). Proxy t
Proxy  @31) (Proxy 24
forall k (t :: k). Proxy t
Proxy  @24) SWord 256
a, Proxy 23 -> Proxy 16 -> SWord 256 -> SBV (WordN ((23 - 16) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 23
forall k (t :: k). Proxy t
Proxy  @23) (Proxy 16
forall k (t :: k). Proxy t
Proxy  @16) SWord 256
a, Proxy 15 -> Proxy 8 -> SWord 256 -> SBV (WordN ((15 - 8) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 15
forall k (t :: k). Proxy t
Proxy  @15) (Proxy 8
forall k (t :: k). Proxy t
Proxy   @8) SWord 256
a, Proxy 7 -> Proxy 0 -> SWord 256 -> SBV (WordN ((7 - 0) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 7
forall k (t :: k). Proxy t
Proxy   @7) (Proxy 0
forall k (t :: k). Proxy t
Proxy   @0) SWord 256
a
               ]

   fromBytes :: [SWord 8] -> SWord 256
fromBytes [SWord 8]
as
     | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
32
     = ([SWord 8] -> SWord 128
forall a. ByteConverter a => [SWord 8] -> a
fromBytes :: [SWord 8] -> SWord 128) (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
take Int
16 [SWord 8]
as) SWord 128 -> SWord 128 -> SBV (WordN (128 + 128))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# [SWord 8] -> SWord 128
forall a. ByteConverter a => [SWord 8] -> a
fromBytes (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
16 [SWord 8]
as)
     | Bool
True
     = String -> SWord 256
forall a. HasCallStack => String -> a
error (String -> SWord 256) -> String -> SWord 256
forall a b. (a -> b) -> a -> b
$ String
"fromBytes:SWord 256: Incorrect number of bytes: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l
     where l :: Int
l = [SWord 8] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
as

-- | 'SWord' 512 instance for 'ByteConverter'
instance ByteConverter (SWord 512) where
   toBytes :: SWord 512 -> [SWord 8]
toBytes SWord 512
a = [ Proxy 511
-> Proxy 504 -> SWord 512 -> SBV (WordN ((511 - 504) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 511
forall k (t :: k). Proxy t
Proxy @511) (Proxy 504
forall k (t :: k). Proxy t
Proxy @504) SWord 512
a, Proxy 503
-> Proxy 496 -> SWord 512 -> SBV (WordN ((503 - 496) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 503
forall k (t :: k). Proxy t
Proxy @503) (Proxy 496
forall k (t :: k). Proxy t
Proxy @496) SWord 512
a, Proxy 495
-> Proxy 488 -> SWord 512 -> SBV (WordN ((495 - 488) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 495
forall k (t :: k). Proxy t
Proxy @495) (Proxy 488
forall k (t :: k). Proxy t
Proxy @488) SWord 512
a, Proxy 487
-> Proxy 480 -> SWord 512 -> SBV (WordN ((487 - 480) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 487
forall k (t :: k). Proxy t
Proxy @487) (Proxy 480
forall k (t :: k). Proxy t
Proxy @480) SWord 512
a
               , Proxy 479
-> Proxy 472 -> SWord 512 -> SBV (WordN ((479 - 472) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 479
forall k (t :: k). Proxy t
Proxy @479) (Proxy 472
forall k (t :: k). Proxy t
Proxy @472) SWord 512
a, Proxy 471
-> Proxy 464 -> SWord 512 -> SBV (WordN ((471 - 464) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 471
forall k (t :: k). Proxy t
Proxy @471) (Proxy 464
forall k (t :: k). Proxy t
Proxy @464) SWord 512
a, Proxy 463
-> Proxy 456 -> SWord 512 -> SBV (WordN ((463 - 456) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 463
forall k (t :: k). Proxy t
Proxy @463) (Proxy 456
forall k (t :: k). Proxy t
Proxy @456) SWord 512
a, Proxy 455
-> Proxy 448 -> SWord 512 -> SBV (WordN ((455 - 448) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 455
forall k (t :: k). Proxy t
Proxy @455) (Proxy 448
forall k (t :: k). Proxy t
Proxy @448) SWord 512
a
               , Proxy 447
-> Proxy 440 -> SWord 512 -> SBV (WordN ((447 - 440) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 447
forall k (t :: k). Proxy t
Proxy @447) (Proxy 440
forall k (t :: k). Proxy t
Proxy @440) SWord 512
a, Proxy 439
-> Proxy 432 -> SWord 512 -> SBV (WordN ((439 - 432) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 439
forall k (t :: k). Proxy t
Proxy @439) (Proxy 432
forall k (t :: k). Proxy t
Proxy @432) SWord 512
a, Proxy 431
-> Proxy 424 -> SWord 512 -> SBV (WordN ((431 - 424) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 431
forall k (t :: k). Proxy t
Proxy @431) (Proxy 424
forall k (t :: k). Proxy t
Proxy @424) SWord 512
a, Proxy 423
-> Proxy 416 -> SWord 512 -> SBV (WordN ((423 - 416) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 423
forall k (t :: k). Proxy t
Proxy @423) (Proxy 416
forall k (t :: k). Proxy t
Proxy @416) SWord 512
a
               , Proxy 415
-> Proxy 408 -> SWord 512 -> SBV (WordN ((415 - 408) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 415
forall k (t :: k). Proxy t
Proxy @415) (Proxy 408
forall k (t :: k). Proxy t
Proxy @408) SWord 512
a, Proxy 407
-> Proxy 400 -> SWord 512 -> SBV (WordN ((407 - 400) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 407
forall k (t :: k). Proxy t
Proxy @407) (Proxy 400
forall k (t :: k). Proxy t
Proxy @400) SWord 512
a, Proxy 399
-> Proxy 392 -> SWord 512 -> SBV (WordN ((399 - 392) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 399
forall k (t :: k). Proxy t
Proxy @399) (Proxy 392
forall k (t :: k). Proxy t
Proxy @392) SWord 512
a, Proxy 391
-> Proxy 384 -> SWord 512 -> SBV (WordN ((391 - 384) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 391
forall k (t :: k). Proxy t
Proxy @391) (Proxy 384
forall k (t :: k). Proxy t
Proxy @384) SWord 512
a
               , Proxy 383
-> Proxy 376 -> SWord 512 -> SBV (WordN ((383 - 376) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 383
forall k (t :: k). Proxy t
Proxy @383) (Proxy 376
forall k (t :: k). Proxy t
Proxy @376) SWord 512
a, Proxy 375
-> Proxy 368 -> SWord 512 -> SBV (WordN ((375 - 368) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 375
forall k (t :: k). Proxy t
Proxy @375) (Proxy 368
forall k (t :: k). Proxy t
Proxy @368) SWord 512
a, Proxy 367
-> Proxy 360 -> SWord 512 -> SBV (WordN ((367 - 360) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 367
forall k (t :: k). Proxy t
Proxy @367) (Proxy 360
forall k (t :: k). Proxy t
Proxy @360) SWord 512
a, Proxy 359
-> Proxy 352 -> SWord 512 -> SBV (WordN ((359 - 352) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 359
forall k (t :: k). Proxy t
Proxy @359) (Proxy 352
forall k (t :: k). Proxy t
Proxy @352) SWord 512
a
               , Proxy 351
-> Proxy 344 -> SWord 512 -> SBV (WordN ((351 - 344) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 351
forall k (t :: k). Proxy t
Proxy @351) (Proxy 344
forall k (t :: k). Proxy t
Proxy @344) SWord 512
a, Proxy 343
-> Proxy 336 -> SWord 512 -> SBV (WordN ((343 - 336) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 343
forall k (t :: k). Proxy t
Proxy @343) (Proxy 336
forall k (t :: k). Proxy t
Proxy @336) SWord 512
a, Proxy 335
-> Proxy 328 -> SWord 512 -> SBV (WordN ((335 - 328) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 335
forall k (t :: k). Proxy t
Proxy @335) (Proxy 328
forall k (t :: k). Proxy t
Proxy @328) SWord 512
a, Proxy 327
-> Proxy 320 -> SWord 512 -> SBV (WordN ((327 - 320) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 327
forall k (t :: k). Proxy t
Proxy @327) (Proxy 320
forall k (t :: k). Proxy t
Proxy @320) SWord 512
a
               , Proxy 319
-> Proxy 312 -> SWord 512 -> SBV (WordN ((319 - 312) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 319
forall k (t :: k). Proxy t
Proxy @319) (Proxy 312
forall k (t :: k). Proxy t
Proxy @312) SWord 512
a, Proxy 311
-> Proxy 304 -> SWord 512 -> SBV (WordN ((311 - 304) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 311
forall k (t :: k). Proxy t
Proxy @311) (Proxy 304
forall k (t :: k). Proxy t
Proxy @304) SWord 512
a, Proxy 303
-> Proxy 296 -> SWord 512 -> SBV (WordN ((303 - 296) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 303
forall k (t :: k). Proxy t
Proxy @303) (Proxy 296
forall k (t :: k). Proxy t
Proxy @296) SWord 512
a, Proxy 295
-> Proxy 288 -> SWord 512 -> SBV (WordN ((295 - 288) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 295
forall k (t :: k). Proxy t
Proxy @295) (Proxy 288
forall k (t :: k). Proxy t
Proxy @288) SWord 512
a
               , Proxy 287
-> Proxy 280 -> SWord 512 -> SBV (WordN ((287 - 280) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 287
forall k (t :: k). Proxy t
Proxy @287) (Proxy 280
forall k (t :: k). Proxy t
Proxy @280) SWord 512
a, Proxy 279
-> Proxy 272 -> SWord 512 -> SBV (WordN ((279 - 272) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 279
forall k (t :: k). Proxy t
Proxy @279) (Proxy 272
forall k (t :: k). Proxy t
Proxy @272) SWord 512
a, Proxy 271
-> Proxy 264 -> SWord 512 -> SBV (WordN ((271 - 264) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 271
forall k (t :: k). Proxy t
Proxy @271) (Proxy 264
forall k (t :: k). Proxy t
Proxy @264) SWord 512
a, Proxy 263
-> Proxy 256 -> SWord 512 -> SBV (WordN ((263 - 256) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 263
forall k (t :: k). Proxy t
Proxy @263) (Proxy 256
forall k (t :: k). Proxy t
Proxy @256) SWord 512
a
               , Proxy 255
-> Proxy 248 -> SWord 512 -> SBV (WordN ((255 - 248) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 255
forall k (t :: k). Proxy t
Proxy @255) (Proxy 248
forall k (t :: k). Proxy t
Proxy @248) SWord 512
a, Proxy 247
-> Proxy 240 -> SWord 512 -> SBV (WordN ((247 - 240) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 247
forall k (t :: k). Proxy t
Proxy @247) (Proxy 240
forall k (t :: k). Proxy t
Proxy @240) SWord 512
a, Proxy 239
-> Proxy 232 -> SWord 512 -> SBV (WordN ((239 - 232) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 239
forall k (t :: k). Proxy t
Proxy @239) (Proxy 232
forall k (t :: k). Proxy t
Proxy @232) SWord 512
a, Proxy 231
-> Proxy 224 -> SWord 512 -> SBV (WordN ((231 - 224) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 231
forall k (t :: k). Proxy t
Proxy @231) (Proxy 224
forall k (t :: k). Proxy t
Proxy @224) SWord 512
a
               , Proxy 223
-> Proxy 216 -> SWord 512 -> SBV (WordN ((223 - 216) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 223
forall k (t :: k). Proxy t
Proxy @223) (Proxy 216
forall k (t :: k). Proxy t
Proxy @216) SWord 512
a, Proxy 215
-> Proxy 208 -> SWord 512 -> SBV (WordN ((215 - 208) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 215
forall k (t :: k). Proxy t
Proxy @215) (Proxy 208
forall k (t :: k). Proxy t
Proxy @208) SWord 512
a, Proxy 207
-> Proxy 200 -> SWord 512 -> SBV (WordN ((207 - 200) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 207
forall k (t :: k). Proxy t
Proxy @207) (Proxy 200
forall k (t :: k). Proxy t
Proxy @200) SWord 512
a, Proxy 199
-> Proxy 192 -> SWord 512 -> SBV (WordN ((199 - 192) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 199
forall k (t :: k). Proxy t
Proxy @199) (Proxy 192
forall k (t :: k). Proxy t
Proxy @192) SWord 512
a
               , Proxy 191
-> Proxy 184 -> SWord 512 -> SBV (WordN ((191 - 184) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 191
forall k (t :: k). Proxy t
Proxy @191) (Proxy 184
forall k (t :: k). Proxy t
Proxy @184) SWord 512
a, Proxy 183
-> Proxy 176 -> SWord 512 -> SBV (WordN ((183 - 176) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 183
forall k (t :: k). Proxy t
Proxy @183) (Proxy 176
forall k (t :: k). Proxy t
Proxy @176) SWord 512
a, Proxy 175
-> Proxy 168 -> SWord 512 -> SBV (WordN ((175 - 168) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 175
forall k (t :: k). Proxy t
Proxy @175) (Proxy 168
forall k (t :: k). Proxy t
Proxy @168) SWord 512
a, Proxy 167
-> Proxy 160 -> SWord 512 -> SBV (WordN ((167 - 160) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 167
forall k (t :: k). Proxy t
Proxy @167) (Proxy 160
forall k (t :: k). Proxy t
Proxy @160) SWord 512
a
               , Proxy 159
-> Proxy 152 -> SWord 512 -> SBV (WordN ((159 - 152) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 159
forall k (t :: k). Proxy t
Proxy @159) (Proxy 152
forall k (t :: k). Proxy t
Proxy @152) SWord 512
a, Proxy 151
-> Proxy 144 -> SWord 512 -> SBV (WordN ((151 - 144) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 151
forall k (t :: k). Proxy t
Proxy @151) (Proxy 144
forall k (t :: k). Proxy t
Proxy @144) SWord 512
a, Proxy 143
-> Proxy 136 -> SWord 512 -> SBV (WordN ((143 - 136) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 143
forall k (t :: k). Proxy t
Proxy @143) (Proxy 136
forall k (t :: k). Proxy t
Proxy @136) SWord 512
a, Proxy 135
-> Proxy 128 -> SWord 512 -> SBV (WordN ((135 - 128) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 135
forall k (t :: k). Proxy t
Proxy @135) (Proxy 128
forall k (t :: k). Proxy t
Proxy @128) SWord 512
a
               , Proxy 127
-> Proxy 120 -> SWord 512 -> SBV (WordN ((127 - 120) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 127
forall k (t :: k). Proxy t
Proxy @127) (Proxy 120
forall k (t :: k). Proxy t
Proxy @120) SWord 512
a, Proxy 119
-> Proxy 112 -> SWord 512 -> SBV (WordN ((119 - 112) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 119
forall k (t :: k). Proxy t
Proxy @119) (Proxy 112
forall k (t :: k). Proxy t
Proxy @112) SWord 512
a, Proxy 111
-> Proxy 104 -> SWord 512 -> SBV (WordN ((111 - 104) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 111
forall k (t :: k). Proxy t
Proxy @111) (Proxy 104
forall k (t :: k). Proxy t
Proxy @104) SWord 512
a, Proxy 103 -> Proxy 96 -> SWord 512 -> SBV (WordN ((103 - 96) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 103
forall k (t :: k). Proxy t
Proxy @103) (Proxy 96
forall k (t :: k). Proxy t
Proxy  @96) SWord 512
a
               , Proxy 95 -> Proxy 88 -> SWord 512 -> SBV (WordN ((95 - 88) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 95
forall k (t :: k). Proxy t
Proxy  @95) (Proxy 88
forall k (t :: k). Proxy t
Proxy  @88) SWord 512
a, Proxy 87 -> Proxy 80 -> SWord 512 -> SBV (WordN ((87 - 80) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 87
forall k (t :: k). Proxy t
Proxy  @87) (Proxy 80
forall k (t :: k). Proxy t
Proxy  @80) SWord 512
a, Proxy 79 -> Proxy 72 -> SWord 512 -> SBV (WordN ((79 - 72) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 79
forall k (t :: k). Proxy t
Proxy  @79) (Proxy 72
forall k (t :: k). Proxy t
Proxy  @72) SWord 512
a, Proxy 71 -> Proxy 64 -> SWord 512 -> SBV (WordN ((71 - 64) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 71
forall k (t :: k). Proxy t
Proxy  @71) (Proxy 64
forall k (t :: k). Proxy t
Proxy  @64) SWord 512
a
               , Proxy 63 -> Proxy 56 -> SWord 512 -> SBV (WordN ((63 - 56) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 63
forall k (t :: k). Proxy t
Proxy  @63) (Proxy 56
forall k (t :: k). Proxy t
Proxy  @56) SWord 512
a, Proxy 55 -> Proxy 48 -> SWord 512 -> SBV (WordN ((55 - 48) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 55
forall k (t :: k). Proxy t
Proxy  @55) (Proxy 48
forall k (t :: k). Proxy t
Proxy  @48) SWord 512
a, Proxy 47 -> Proxy 40 -> SWord 512 -> SBV (WordN ((47 - 40) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 47
forall k (t :: k). Proxy t
Proxy  @47) (Proxy 40
forall k (t :: k). Proxy t
Proxy  @40) SWord 512
a, Proxy 39 -> Proxy 32 -> SWord 512 -> SBV (WordN ((39 - 32) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 39
forall k (t :: k). Proxy t
Proxy  @39) (Proxy 32
forall k (t :: k). Proxy t
Proxy  @32) SWord 512
a
               , Proxy 31 -> Proxy 24 -> SWord 512 -> SBV (WordN ((31 - 24) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 31
forall k (t :: k). Proxy t
Proxy  @31) (Proxy 24
forall k (t :: k). Proxy t
Proxy  @24) SWord 512
a, Proxy 23 -> Proxy 16 -> SWord 512 -> SBV (WordN ((23 - 16) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 23
forall k (t :: k). Proxy t
Proxy  @23) (Proxy 16
forall k (t :: k). Proxy t
Proxy  @16) SWord 512
a, Proxy 15 -> Proxy 8 -> SWord 512 -> SBV (WordN ((15 - 8) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 15
forall k (t :: k). Proxy t
Proxy  @15) (Proxy 8
forall k (t :: k). Proxy t
Proxy   @8) SWord 512
a, Proxy 7 -> Proxy 0 -> SWord 512 -> SBV (WordN ((7 - 0) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 7
forall k (t :: k). Proxy t
Proxy   @7) (Proxy 0
forall k (t :: k). Proxy t
Proxy   @0) SWord 512
a
               ]

   fromBytes :: [SWord 8] -> SWord 512
fromBytes [SWord 8]
as
     | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
64
     = ([SWord 8] -> SWord 256
forall a. ByteConverter a => [SWord 8] -> a
fromBytes :: [SWord 8] -> SWord 256) (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
take Int
32 [SWord 8]
as) SWord 256 -> SWord 256 -> SBV (WordN (256 + 256))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# [SWord 8] -> SWord 256
forall a. ByteConverter a => [SWord 8] -> a
fromBytes (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
32 [SWord 8]
as)
     | Bool
True
     = String -> SWord 512
forall a. HasCallStack => String -> a
error (String -> SWord 512) -> String -> SWord 512
forall a b. (a -> b) -> a -> b
$ String
"fromBytes:SWord 512: Incorrect number of bytes: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l
     where l :: Int
l = [SWord 8] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
as

-- | 'SWord' 1024 instance for 'ByteConverter'
instance ByteConverter (SWord 1024) where
   toBytes :: SWord 1024 -> [SWord 8]
toBytes SWord 1024
a = [ Proxy 1023
-> Proxy 1016 -> SWord 1024 -> SBV (WordN ((1023 - 1016) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 1023
forall k (t :: k). Proxy t
Proxy @1023) (Proxy 1016
forall k (t :: k). Proxy t
Proxy @1016) SWord 1024
a, Proxy 1015
-> Proxy 1008 -> SWord 1024 -> SBV (WordN ((1015 - 1008) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 1015
forall k (t :: k). Proxy t
Proxy @1015) (Proxy 1008
forall k (t :: k). Proxy t
Proxy @1008) SWord 1024
a, Proxy 1007
-> Proxy 1000 -> SWord 1024 -> SBV (WordN ((1007 - 1000) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 1007
forall k (t :: k). Proxy t
Proxy @1007) (Proxy 1000
forall k (t :: k). Proxy t
Proxy @1000) SWord 1024
a, Proxy 999
-> Proxy 992 -> SWord 1024 -> SBV (WordN ((999 - 992) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 999
forall k (t :: k). Proxy t
Proxy  @999) (Proxy 992
forall k (t :: k). Proxy t
Proxy  @992) SWord 1024
a
               , Proxy 991
-> Proxy 984 -> SWord 1024 -> SBV (WordN ((991 - 984) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 991
forall k (t :: k). Proxy t
Proxy  @991) (Proxy 984
forall k (t :: k). Proxy t
Proxy  @984) SWord 1024
a, Proxy 983
-> Proxy 976 -> SWord 1024 -> SBV (WordN ((983 - 976) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 983
forall k (t :: k). Proxy t
Proxy  @983) (Proxy 976
forall k (t :: k). Proxy t
Proxy  @976) SWord 1024
a, Proxy 975
-> Proxy 968 -> SWord 1024 -> SBV (WordN ((975 - 968) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 975
forall k (t :: k). Proxy t
Proxy  @975) (Proxy 968
forall k (t :: k). Proxy t
Proxy  @968) SWord 1024
a, Proxy 967
-> Proxy 960 -> SWord 1024 -> SBV (WordN ((967 - 960) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 967
forall k (t :: k). Proxy t
Proxy  @967) (Proxy 960
forall k (t :: k). Proxy t
Proxy  @960) SWord 1024
a
               , Proxy 959
-> Proxy 952 -> SWord 1024 -> SBV (WordN ((959 - 952) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 959
forall k (t :: k). Proxy t
Proxy  @959) (Proxy 952
forall k (t :: k). Proxy t
Proxy  @952) SWord 1024
a, Proxy 951
-> Proxy 944 -> SWord 1024 -> SBV (WordN ((951 - 944) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 951
forall k (t :: k). Proxy t
Proxy  @951) (Proxy 944
forall k (t :: k). Proxy t
Proxy  @944) SWord 1024
a, Proxy 943
-> Proxy 936 -> SWord 1024 -> SBV (WordN ((943 - 936) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 943
forall k (t :: k). Proxy t
Proxy  @943) (Proxy 936
forall k (t :: k). Proxy t
Proxy  @936) SWord 1024
a, Proxy 935
-> Proxy 928 -> SWord 1024 -> SBV (WordN ((935 - 928) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 935
forall k (t :: k). Proxy t
Proxy  @935) (Proxy 928
forall k (t :: k). Proxy t
Proxy  @928) SWord 1024
a
               , Proxy 927
-> Proxy 920 -> SWord 1024 -> SBV (WordN ((927 - 920) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 927
forall k (t :: k). Proxy t
Proxy  @927) (Proxy 920
forall k (t :: k). Proxy t
Proxy  @920) SWord 1024
a, Proxy 919
-> Proxy 912 -> SWord 1024 -> SBV (WordN ((919 - 912) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 919
forall k (t :: k). Proxy t
Proxy  @919) (Proxy 912
forall k (t :: k). Proxy t
Proxy  @912) SWord 1024
a, Proxy 911
-> Proxy 904 -> SWord 1024 -> SBV (WordN ((911 - 904) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 911
forall k (t :: k). Proxy t
Proxy  @911) (Proxy 904
forall k (t :: k). Proxy t
Proxy  @904) SWord 1024
a, Proxy 903
-> Proxy 896 -> SWord 1024 -> SBV (WordN ((903 - 896) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 903
forall k (t :: k). Proxy t
Proxy  @903) (Proxy 896
forall k (t :: k). Proxy t
Proxy  @896) SWord 1024
a
               , Proxy 895
-> Proxy 888 -> SWord 1024 -> SBV (WordN ((895 - 888) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 895
forall k (t :: k). Proxy t
Proxy  @895) (Proxy 888
forall k (t :: k). Proxy t
Proxy  @888) SWord 1024
a, Proxy 887
-> Proxy 880 -> SWord 1024 -> SBV (WordN ((887 - 880) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 887
forall k (t :: k). Proxy t
Proxy  @887) (Proxy 880
forall k (t :: k). Proxy t
Proxy  @880) SWord 1024
a, Proxy 879
-> Proxy 872 -> SWord 1024 -> SBV (WordN ((879 - 872) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 879
forall k (t :: k). Proxy t
Proxy  @879) (Proxy 872
forall k (t :: k). Proxy t
Proxy  @872) SWord 1024
a, Proxy 871
-> Proxy 864 -> SWord 1024 -> SBV (WordN ((871 - 864) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 871
forall k (t :: k). Proxy t
Proxy  @871) (Proxy 864
forall k (t :: k). Proxy t
Proxy  @864) SWord 1024
a
               , Proxy 863
-> Proxy 856 -> SWord 1024 -> SBV (WordN ((863 - 856) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 863
forall k (t :: k). Proxy t
Proxy  @863) (Proxy 856
forall k (t :: k). Proxy t
Proxy  @856) SWord 1024
a, Proxy 855
-> Proxy 848 -> SWord 1024 -> SBV (WordN ((855 - 848) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 855
forall k (t :: k). Proxy t
Proxy  @855) (Proxy 848
forall k (t :: k). Proxy t
Proxy  @848) SWord 1024
a, Proxy 847
-> Proxy 840 -> SWord 1024 -> SBV (WordN ((847 - 840) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 847
forall k (t :: k). Proxy t
Proxy  @847) (Proxy 840
forall k (t :: k). Proxy t
Proxy  @840) SWord 1024
a, Proxy 839
-> Proxy 832 -> SWord 1024 -> SBV (WordN ((839 - 832) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 839
forall k (t :: k). Proxy t
Proxy  @839) (Proxy 832
forall k (t :: k). Proxy t
Proxy  @832) SWord 1024
a
               , Proxy 831
-> Proxy 824 -> SWord 1024 -> SBV (WordN ((831 - 824) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 831
forall k (t :: k). Proxy t
Proxy  @831) (Proxy 824
forall k (t :: k). Proxy t
Proxy  @824) SWord 1024
a, Proxy 823
-> Proxy 816 -> SWord 1024 -> SBV (WordN ((823 - 816) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 823
forall k (t :: k). Proxy t
Proxy  @823) (Proxy 816
forall k (t :: k). Proxy t
Proxy  @816) SWord 1024
a, Proxy 815
-> Proxy 808 -> SWord 1024 -> SBV (WordN ((815 - 808) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 815
forall k (t :: k). Proxy t
Proxy  @815) (Proxy 808
forall k (t :: k). Proxy t
Proxy  @808) SWord 1024
a, Proxy 807
-> Proxy 800 -> SWord 1024 -> SBV (WordN ((807 - 800) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 807
forall k (t :: k). Proxy t
Proxy  @807) (Proxy 800
forall k (t :: k). Proxy t
Proxy  @800) SWord 1024
a
               , Proxy 799
-> Proxy 792 -> SWord 1024 -> SBV (WordN ((799 - 792) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 799
forall k (t :: k). Proxy t
Proxy  @799) (Proxy 792
forall k (t :: k). Proxy t
Proxy  @792) SWord 1024
a, Proxy 791
-> Proxy 784 -> SWord 1024 -> SBV (WordN ((791 - 784) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 791
forall k (t :: k). Proxy t
Proxy  @791) (Proxy 784
forall k (t :: k). Proxy t
Proxy  @784) SWord 1024
a, Proxy 783
-> Proxy 776 -> SWord 1024 -> SBV (WordN ((783 - 776) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 783
forall k (t :: k). Proxy t
Proxy  @783) (Proxy 776
forall k (t :: k). Proxy t
Proxy  @776) SWord 1024
a, Proxy 775
-> Proxy 768 -> SWord 1024 -> SBV (WordN ((775 - 768) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 775
forall k (t :: k). Proxy t
Proxy  @775) (Proxy 768
forall k (t :: k). Proxy t
Proxy  @768) SWord 1024
a
               , Proxy 767
-> Proxy 760 -> SWord 1024 -> SBV (WordN ((767 - 760) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 767
forall k (t :: k). Proxy t
Proxy  @767) (Proxy 760
forall k (t :: k). Proxy t
Proxy  @760) SWord 1024
a, Proxy 759
-> Proxy 752 -> SWord 1024 -> SBV (WordN ((759 - 752) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 759
forall k (t :: k). Proxy t
Proxy  @759) (Proxy 752
forall k (t :: k). Proxy t
Proxy  @752) SWord 1024
a, Proxy 751
-> Proxy 744 -> SWord 1024 -> SBV (WordN ((751 - 744) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 751
forall k (t :: k). Proxy t
Proxy  @751) (Proxy 744
forall k (t :: k). Proxy t
Proxy  @744) SWord 1024
a, Proxy 743
-> Proxy 736 -> SWord 1024 -> SBV (WordN ((743 - 736) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 743
forall k (t :: k). Proxy t
Proxy  @743) (Proxy 736
forall k (t :: k). Proxy t
Proxy  @736) SWord 1024
a
               , Proxy 735
-> Proxy 728 -> SWord 1024 -> SBV (WordN ((735 - 728) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 735
forall k (t :: k). Proxy t
Proxy  @735) (Proxy 728
forall k (t :: k). Proxy t
Proxy  @728) SWord 1024
a, Proxy 727
-> Proxy 720 -> SWord 1024 -> SBV (WordN ((727 - 720) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 727
forall k (t :: k). Proxy t
Proxy  @727) (Proxy 720
forall k (t :: k). Proxy t
Proxy  @720) SWord 1024
a, Proxy 719
-> Proxy 712 -> SWord 1024 -> SBV (WordN ((719 - 712) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 719
forall k (t :: k). Proxy t
Proxy  @719) (Proxy 712
forall k (t :: k). Proxy t
Proxy  @712) SWord 1024
a, Proxy 711
-> Proxy 704 -> SWord 1024 -> SBV (WordN ((711 - 704) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 711
forall k (t :: k). Proxy t
Proxy  @711) (Proxy 704
forall k (t :: k). Proxy t
Proxy  @704) SWord 1024
a
               , Proxy 703
-> Proxy 696 -> SWord 1024 -> SBV (WordN ((703 - 696) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 703
forall k (t :: k). Proxy t
Proxy  @703) (Proxy 696
forall k (t :: k). Proxy t
Proxy  @696) SWord 1024
a, Proxy 695
-> Proxy 688 -> SWord 1024 -> SBV (WordN ((695 - 688) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 695
forall k (t :: k). Proxy t
Proxy  @695) (Proxy 688
forall k (t :: k). Proxy t
Proxy  @688) SWord 1024
a, Proxy 687
-> Proxy 680 -> SWord 1024 -> SBV (WordN ((687 - 680) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 687
forall k (t :: k). Proxy t
Proxy  @687) (Proxy 680
forall k (t :: k). Proxy t
Proxy  @680) SWord 1024
a, Proxy 679
-> Proxy 672 -> SWord 1024 -> SBV (WordN ((679 - 672) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 679
forall k (t :: k). Proxy t
Proxy  @679) (Proxy 672
forall k (t :: k). Proxy t
Proxy  @672) SWord 1024
a
               , Proxy 671
-> Proxy 664 -> SWord 1024 -> SBV (WordN ((671 - 664) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 671
forall k (t :: k). Proxy t
Proxy  @671) (Proxy 664
forall k (t :: k). Proxy t
Proxy  @664) SWord 1024
a, Proxy 663
-> Proxy 656 -> SWord 1024 -> SBV (WordN ((663 - 656) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 663
forall k (t :: k). Proxy t
Proxy  @663) (Proxy 656
forall k (t :: k). Proxy t
Proxy  @656) SWord 1024
a, Proxy 655
-> Proxy 648 -> SWord 1024 -> SBV (WordN ((655 - 648) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 655
forall k (t :: k). Proxy t
Proxy  @655) (Proxy 648
forall k (t :: k). Proxy t
Proxy  @648) SWord 1024
a, Proxy 647
-> Proxy 640 -> SWord 1024 -> SBV (WordN ((647 - 640) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 647
forall k (t :: k). Proxy t
Proxy  @647) (Proxy 640
forall k (t :: k). Proxy t
Proxy  @640) SWord 1024
a
               , Proxy 639
-> Proxy 632 -> SWord 1024 -> SBV (WordN ((639 - 632) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 639
forall k (t :: k). Proxy t
Proxy  @639) (Proxy 632
forall k (t :: k). Proxy t
Proxy  @632) SWord 1024
a, Proxy 631
-> Proxy 624 -> SWord 1024 -> SBV (WordN ((631 - 624) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 631
forall k (t :: k). Proxy t
Proxy  @631) (Proxy 624
forall k (t :: k). Proxy t
Proxy  @624) SWord 1024
a, Proxy 623
-> Proxy 616 -> SWord 1024 -> SBV (WordN ((623 - 616) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 623
forall k (t :: k). Proxy t
Proxy  @623) (Proxy 616
forall k (t :: k). Proxy t
Proxy  @616) SWord 1024
a, Proxy 615
-> Proxy 608 -> SWord 1024 -> SBV (WordN ((615 - 608) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 615
forall k (t :: k). Proxy t
Proxy  @615) (Proxy 608
forall k (t :: k). Proxy t
Proxy  @608) SWord 1024
a
               , Proxy 607
-> Proxy 600 -> SWord 1024 -> SBV (WordN ((607 - 600) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 607
forall k (t :: k). Proxy t
Proxy  @607) (Proxy 600
forall k (t :: k). Proxy t
Proxy  @600) SWord 1024
a, Proxy 599
-> Proxy 592 -> SWord 1024 -> SBV (WordN ((599 - 592) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 599
forall k (t :: k). Proxy t
Proxy  @599) (Proxy 592
forall k (t :: k). Proxy t
Proxy  @592) SWord 1024
a, Proxy 591
-> Proxy 584 -> SWord 1024 -> SBV (WordN ((591 - 584) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 591
forall k (t :: k). Proxy t
Proxy  @591) (Proxy 584
forall k (t :: k). Proxy t
Proxy  @584) SWord 1024
a, Proxy 583
-> Proxy 576 -> SWord 1024 -> SBV (WordN ((583 - 576) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 583
forall k (t :: k). Proxy t
Proxy  @583) (Proxy 576
forall k (t :: k). Proxy t
Proxy  @576) SWord 1024
a
               , Proxy 575
-> Proxy 568 -> SWord 1024 -> SBV (WordN ((575 - 568) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 575
forall k (t :: k). Proxy t
Proxy  @575) (Proxy 568
forall k (t :: k). Proxy t
Proxy  @568) SWord 1024
a, Proxy 567
-> Proxy 560 -> SWord 1024 -> SBV (WordN ((567 - 560) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 567
forall k (t :: k). Proxy t
Proxy  @567) (Proxy 560
forall k (t :: k). Proxy t
Proxy  @560) SWord 1024
a, Proxy 559
-> Proxy 552 -> SWord 1024 -> SBV (WordN ((559 - 552) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 559
forall k (t :: k). Proxy t
Proxy  @559) (Proxy 552
forall k (t :: k). Proxy t
Proxy  @552) SWord 1024
a, Proxy 551
-> Proxy 544 -> SWord 1024 -> SBV (WordN ((551 - 544) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 551
forall k (t :: k). Proxy t
Proxy  @551) (Proxy 544
forall k (t :: k). Proxy t
Proxy  @544) SWord 1024
a
               , Proxy 543
-> Proxy 536 -> SWord 1024 -> SBV (WordN ((543 - 536) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 543
forall k (t :: k). Proxy t
Proxy  @543) (Proxy 536
forall k (t :: k). Proxy t
Proxy  @536) SWord 1024
a, Proxy 535
-> Proxy 528 -> SWord 1024 -> SBV (WordN ((535 - 528) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 535
forall k (t :: k). Proxy t
Proxy  @535) (Proxy 528
forall k (t :: k). Proxy t
Proxy  @528) SWord 1024
a, Proxy 527
-> Proxy 520 -> SWord 1024 -> SBV (WordN ((527 - 520) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 527
forall k (t :: k). Proxy t
Proxy  @527) (Proxy 520
forall k (t :: k). Proxy t
Proxy  @520) SWord 1024
a, Proxy 519
-> Proxy 512 -> SWord 1024 -> SBV (WordN ((519 - 512) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 519
forall k (t :: k). Proxy t
Proxy  @519) (Proxy 512
forall k (t :: k). Proxy t
Proxy  @512) SWord 1024
a
               , Proxy 511
-> Proxy 504 -> SWord 1024 -> SBV (WordN ((511 - 504) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 511
forall k (t :: k). Proxy t
Proxy  @511) (Proxy 504
forall k (t :: k). Proxy t
Proxy  @504) SWord 1024
a, Proxy 503
-> Proxy 496 -> SWord 1024 -> SBV (WordN ((503 - 496) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 503
forall k (t :: k). Proxy t
Proxy  @503) (Proxy 496
forall k (t :: k). Proxy t
Proxy  @496) SWord 1024
a, Proxy 495
-> Proxy 488 -> SWord 1024 -> SBV (WordN ((495 - 488) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 495
forall k (t :: k). Proxy t
Proxy  @495) (Proxy 488
forall k (t :: k). Proxy t
Proxy  @488) SWord 1024
a, Proxy 487
-> Proxy 480 -> SWord 1024 -> SBV (WordN ((487 - 480) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 487
forall k (t :: k). Proxy t
Proxy  @487) (Proxy 480
forall k (t :: k). Proxy t
Proxy  @480) SWord 1024
a
               , Proxy 479
-> Proxy 472 -> SWord 1024 -> SBV (WordN ((479 - 472) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 479
forall k (t :: k). Proxy t
Proxy  @479) (Proxy 472
forall k (t :: k). Proxy t
Proxy  @472) SWord 1024
a, Proxy 471
-> Proxy 464 -> SWord 1024 -> SBV (WordN ((471 - 464) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 471
forall k (t :: k). Proxy t
Proxy  @471) (Proxy 464
forall k (t :: k). Proxy t
Proxy  @464) SWord 1024
a, Proxy 463
-> Proxy 456 -> SWord 1024 -> SBV (WordN ((463 - 456) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 463
forall k (t :: k). Proxy t
Proxy  @463) (Proxy 456
forall k (t :: k). Proxy t
Proxy  @456) SWord 1024
a, Proxy 455
-> Proxy 448 -> SWord 1024 -> SBV (WordN ((455 - 448) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 455
forall k (t :: k). Proxy t
Proxy  @455) (Proxy 448
forall k (t :: k). Proxy t
Proxy  @448) SWord 1024
a
               , Proxy 447
-> Proxy 440 -> SWord 1024 -> SBV (WordN ((447 - 440) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 447
forall k (t :: k). Proxy t
Proxy  @447) (Proxy 440
forall k (t :: k). Proxy t
Proxy  @440) SWord 1024
a, Proxy 439
-> Proxy 432 -> SWord 1024 -> SBV (WordN ((439 - 432) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 439
forall k (t :: k). Proxy t
Proxy  @439) (Proxy 432
forall k (t :: k). Proxy t
Proxy  @432) SWord 1024
a, Proxy 431
-> Proxy 424 -> SWord 1024 -> SBV (WordN ((431 - 424) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 431
forall k (t :: k). Proxy t
Proxy  @431) (Proxy 424
forall k (t :: k). Proxy t
Proxy  @424) SWord 1024
a, Proxy 423
-> Proxy 416 -> SWord 1024 -> SBV (WordN ((423 - 416) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 423
forall k (t :: k). Proxy t
Proxy  @423) (Proxy 416
forall k (t :: k). Proxy t
Proxy  @416) SWord 1024
a
               , Proxy 415
-> Proxy 408 -> SWord 1024 -> SBV (WordN ((415 - 408) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 415
forall k (t :: k). Proxy t
Proxy  @415) (Proxy 408
forall k (t :: k). Proxy t
Proxy  @408) SWord 1024
a, Proxy 407
-> Proxy 400 -> SWord 1024 -> SBV (WordN ((407 - 400) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 407
forall k (t :: k). Proxy t
Proxy  @407) (Proxy 400
forall k (t :: k). Proxy t
Proxy  @400) SWord 1024
a, Proxy 399
-> Proxy 392 -> SWord 1024 -> SBV (WordN ((399 - 392) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 399
forall k (t :: k). Proxy t
Proxy  @399) (Proxy 392
forall k (t :: k). Proxy t
Proxy  @392) SWord 1024
a, Proxy 391
-> Proxy 384 -> SWord 1024 -> SBV (WordN ((391 - 384) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 391
forall k (t :: k). Proxy t
Proxy  @391) (Proxy 384
forall k (t :: k). Proxy t
Proxy  @384) SWord 1024
a
               , Proxy 383
-> Proxy 376 -> SWord 1024 -> SBV (WordN ((383 - 376) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 383
forall k (t :: k). Proxy t
Proxy  @383) (Proxy 376
forall k (t :: k). Proxy t
Proxy  @376) SWord 1024
a, Proxy 375
-> Proxy 368 -> SWord 1024 -> SBV (WordN ((375 - 368) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 375
forall k (t :: k). Proxy t
Proxy  @375) (Proxy 368
forall k (t :: k). Proxy t
Proxy  @368) SWord 1024
a, Proxy 367
-> Proxy 360 -> SWord 1024 -> SBV (WordN ((367 - 360) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 367
forall k (t :: k). Proxy t
Proxy  @367) (Proxy 360
forall k (t :: k). Proxy t
Proxy  @360) SWord 1024
a, Proxy 359
-> Proxy 352 -> SWord 1024 -> SBV (WordN ((359 - 352) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 359
forall k (t :: k). Proxy t
Proxy  @359) (Proxy 352
forall k (t :: k). Proxy t
Proxy  @352) SWord 1024
a
               , Proxy 351
-> Proxy 344 -> SWord 1024 -> SBV (WordN ((351 - 344) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 351
forall k (t :: k). Proxy t
Proxy  @351) (Proxy 344
forall k (t :: k). Proxy t
Proxy  @344) SWord 1024
a, Proxy 343
-> Proxy 336 -> SWord 1024 -> SBV (WordN ((343 - 336) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 343
forall k (t :: k). Proxy t
Proxy  @343) (Proxy 336
forall k (t :: k). Proxy t
Proxy  @336) SWord 1024
a, Proxy 335
-> Proxy 328 -> SWord 1024 -> SBV (WordN ((335 - 328) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 335
forall k (t :: k). Proxy t
Proxy  @335) (Proxy 328
forall k (t :: k). Proxy t
Proxy  @328) SWord 1024
a, Proxy 327
-> Proxy 320 -> SWord 1024 -> SBV (WordN ((327 - 320) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 327
forall k (t :: k). Proxy t
Proxy  @327) (Proxy 320
forall k (t :: k). Proxy t
Proxy  @320) SWord 1024
a
               , Proxy 319
-> Proxy 312 -> SWord 1024 -> SBV (WordN ((319 - 312) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 319
forall k (t :: k). Proxy t
Proxy  @319) (Proxy 312
forall k (t :: k). Proxy t
Proxy  @312) SWord 1024
a, Proxy 311
-> Proxy 304 -> SWord 1024 -> SBV (WordN ((311 - 304) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 311
forall k (t :: k). Proxy t
Proxy  @311) (Proxy 304
forall k (t :: k). Proxy t
Proxy  @304) SWord 1024
a, Proxy 303
-> Proxy 296 -> SWord 1024 -> SBV (WordN ((303 - 296) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 303
forall k (t :: k). Proxy t
Proxy  @303) (Proxy 296
forall k (t :: k). Proxy t
Proxy  @296) SWord 1024
a, Proxy 295
-> Proxy 288 -> SWord 1024 -> SBV (WordN ((295 - 288) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 295
forall k (t :: k). Proxy t
Proxy  @295) (Proxy 288
forall k (t :: k). Proxy t
Proxy  @288) SWord 1024
a
               , Proxy 287
-> Proxy 280 -> SWord 1024 -> SBV (WordN ((287 - 280) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 287
forall k (t :: k). Proxy t
Proxy  @287) (Proxy 280
forall k (t :: k). Proxy t
Proxy  @280) SWord 1024
a, Proxy 279
-> Proxy 272 -> SWord 1024 -> SBV (WordN ((279 - 272) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 279
forall k (t :: k). Proxy t
Proxy  @279) (Proxy 272
forall k (t :: k). Proxy t
Proxy  @272) SWord 1024
a, Proxy 271
-> Proxy 264 -> SWord 1024 -> SBV (WordN ((271 - 264) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 271
forall k (t :: k). Proxy t
Proxy  @271) (Proxy 264
forall k (t :: k). Proxy t
Proxy  @264) SWord 1024
a, Proxy 263
-> Proxy 256 -> SWord 1024 -> SBV (WordN ((263 - 256) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 263
forall k (t :: k). Proxy t
Proxy  @263) (Proxy 256
forall k (t :: k). Proxy t
Proxy  @256) SWord 1024
a
               , Proxy 255
-> Proxy 248 -> SWord 1024 -> SBV (WordN ((255 - 248) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 255
forall k (t :: k). Proxy t
Proxy  @255) (Proxy 248
forall k (t :: k). Proxy t
Proxy  @248) SWord 1024
a, Proxy 247
-> Proxy 240 -> SWord 1024 -> SBV (WordN ((247 - 240) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 247
forall k (t :: k). Proxy t
Proxy  @247) (Proxy 240
forall k (t :: k). Proxy t
Proxy  @240) SWord 1024
a, Proxy 239
-> Proxy 232 -> SWord 1024 -> SBV (WordN ((239 - 232) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 239
forall k (t :: k). Proxy t
Proxy  @239) (Proxy 232
forall k (t :: k). Proxy t
Proxy  @232) SWord 1024
a, Proxy 231
-> Proxy 224 -> SWord 1024 -> SBV (WordN ((231 - 224) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 231
forall k (t :: k). Proxy t
Proxy  @231) (Proxy 224
forall k (t :: k). Proxy t
Proxy  @224) SWord 1024
a
               , Proxy 223
-> Proxy 216 -> SWord 1024 -> SBV (WordN ((223 - 216) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 223
forall k (t :: k). Proxy t
Proxy  @223) (Proxy 216
forall k (t :: k). Proxy t
Proxy  @216) SWord 1024
a, Proxy 215
-> Proxy 208 -> SWord 1024 -> SBV (WordN ((215 - 208) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 215
forall k (t :: k). Proxy t
Proxy  @215) (Proxy 208
forall k (t :: k). Proxy t
Proxy  @208) SWord 1024
a, Proxy 207
-> Proxy 200 -> SWord 1024 -> SBV (WordN ((207 - 200) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 207
forall k (t :: k). Proxy t
Proxy  @207) (Proxy 200
forall k (t :: k). Proxy t
Proxy  @200) SWord 1024
a, Proxy 199
-> Proxy 192 -> SWord 1024 -> SBV (WordN ((199 - 192) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 199
forall k (t :: k). Proxy t
Proxy  @199) (Proxy 192
forall k (t :: k). Proxy t
Proxy  @192) SWord 1024
a
               , Proxy 191
-> Proxy 184 -> SWord 1024 -> SBV (WordN ((191 - 184) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 191
forall k (t :: k). Proxy t
Proxy  @191) (Proxy 184
forall k (t :: k). Proxy t
Proxy  @184) SWord 1024
a, Proxy 183
-> Proxy 176 -> SWord 1024 -> SBV (WordN ((183 - 176) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 183
forall k (t :: k). Proxy t
Proxy  @183) (Proxy 176
forall k (t :: k). Proxy t
Proxy  @176) SWord 1024
a, Proxy 175
-> Proxy 168 -> SWord 1024 -> SBV (WordN ((175 - 168) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 175
forall k (t :: k). Proxy t
Proxy  @175) (Proxy 168
forall k (t :: k). Proxy t
Proxy  @168) SWord 1024
a, Proxy 167
-> Proxy 160 -> SWord 1024 -> SBV (WordN ((167 - 160) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 167
forall k (t :: k). Proxy t
Proxy  @167) (Proxy 160
forall k (t :: k). Proxy t
Proxy  @160) SWord 1024
a
               , Proxy 159
-> Proxy 152 -> SWord 1024 -> SBV (WordN ((159 - 152) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 159
forall k (t :: k). Proxy t
Proxy  @159) (Proxy 152
forall k (t :: k). Proxy t
Proxy  @152) SWord 1024
a, Proxy 151
-> Proxy 144 -> SWord 1024 -> SBV (WordN ((151 - 144) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 151
forall k (t :: k). Proxy t
Proxy  @151) (Proxy 144
forall k (t :: k). Proxy t
Proxy  @144) SWord 1024
a, Proxy 143
-> Proxy 136 -> SWord 1024 -> SBV (WordN ((143 - 136) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 143
forall k (t :: k). Proxy t
Proxy  @143) (Proxy 136
forall k (t :: k). Proxy t
Proxy  @136) SWord 1024
a, Proxy 135
-> Proxy 128 -> SWord 1024 -> SBV (WordN ((135 - 128) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 135
forall k (t :: k). Proxy t
Proxy  @135) (Proxy 128
forall k (t :: k). Proxy t
Proxy  @128) SWord 1024
a
               , Proxy 127
-> Proxy 120 -> SWord 1024 -> SBV (WordN ((127 - 120) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 127
forall k (t :: k). Proxy t
Proxy  @127) (Proxy 120
forall k (t :: k). Proxy t
Proxy  @120) SWord 1024
a, Proxy 119
-> Proxy 112 -> SWord 1024 -> SBV (WordN ((119 - 112) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 119
forall k (t :: k). Proxy t
Proxy  @119) (Proxy 112
forall k (t :: k). Proxy t
Proxy  @112) SWord 1024
a, Proxy 111
-> Proxy 104 -> SWord 1024 -> SBV (WordN ((111 - 104) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 111
forall k (t :: k). Proxy t
Proxy  @111) (Proxy 104
forall k (t :: k). Proxy t
Proxy  @104) SWord 1024
a, Proxy 103 -> Proxy 96 -> SWord 1024 -> SBV (WordN ((103 - 96) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 103
forall k (t :: k). Proxy t
Proxy  @103) (Proxy 96
forall k (t :: k). Proxy t
Proxy   @96) SWord 1024
a
               , Proxy 95 -> Proxy 88 -> SWord 1024 -> SBV (WordN ((95 - 88) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 95
forall k (t :: k). Proxy t
Proxy   @95) (Proxy 88
forall k (t :: k). Proxy t
Proxy   @88) SWord 1024
a, Proxy 87 -> Proxy 80 -> SWord 1024 -> SBV (WordN ((87 - 80) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 87
forall k (t :: k). Proxy t
Proxy   @87) (Proxy 80
forall k (t :: k). Proxy t
Proxy   @80) SWord 1024
a, Proxy 79 -> Proxy 72 -> SWord 1024 -> SBV (WordN ((79 - 72) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 79
forall k (t :: k). Proxy t
Proxy   @79) (Proxy 72
forall k (t :: k). Proxy t
Proxy   @72) SWord 1024
a, Proxy 71 -> Proxy 64 -> SWord 1024 -> SBV (WordN ((71 - 64) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 71
forall k (t :: k). Proxy t
Proxy   @71) (Proxy 64
forall k (t :: k). Proxy t
Proxy   @64) SWord 1024
a
               , Proxy 63 -> Proxy 56 -> SWord 1024 -> SBV (WordN ((63 - 56) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 63
forall k (t :: k). Proxy t
Proxy   @63) (Proxy 56
forall k (t :: k). Proxy t
Proxy   @56) SWord 1024
a, Proxy 55 -> Proxy 48 -> SWord 1024 -> SBV (WordN ((55 - 48) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 55
forall k (t :: k). Proxy t
Proxy   @55) (Proxy 48
forall k (t :: k). Proxy t
Proxy   @48) SWord 1024
a, Proxy 47 -> Proxy 40 -> SWord 1024 -> SBV (WordN ((47 - 40) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 47
forall k (t :: k). Proxy t
Proxy   @47) (Proxy 40
forall k (t :: k). Proxy t
Proxy   @40) SWord 1024
a, Proxy 39 -> Proxy 32 -> SWord 1024 -> SBV (WordN ((39 - 32) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 39
forall k (t :: k). Proxy t
Proxy   @39) (Proxy 32
forall k (t :: k). Proxy t
Proxy   @32) SWord 1024
a
               , Proxy 31 -> Proxy 24 -> SWord 1024 -> SBV (WordN ((31 - 24) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 31
forall k (t :: k). Proxy t
Proxy   @31) (Proxy 24
forall k (t :: k). Proxy t
Proxy   @24) SWord 1024
a, Proxy 23 -> Proxy 16 -> SWord 1024 -> SBV (WordN ((23 - 16) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 23
forall k (t :: k). Proxy t
Proxy   @23) (Proxy 16
forall k (t :: k). Proxy t
Proxy   @16) SWord 1024
a, Proxy 15 -> Proxy 8 -> SWord 1024 -> SBV (WordN ((15 - 8) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 15
forall k (t :: k). Proxy t
Proxy   @15) (Proxy 8
forall k (t :: k). Proxy t
Proxy    @8) SWord 1024
a, Proxy 7 -> Proxy 0 -> SWord 1024 -> SBV (WordN ((7 - 0) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 7
forall k (t :: k). Proxy t
Proxy    @7) (Proxy 0
forall k (t :: k). Proxy t
Proxy    @0) SWord 1024
a
               ]

   fromBytes :: [SWord 8] -> SWord 1024
fromBytes [SWord 8]
as
     | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
128
     = ([SWord 8] -> SWord 512
forall a. ByteConverter a => [SWord 8] -> a
fromBytes :: [SWord 8] -> SWord 512) (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
take Int
64 [SWord 8]
as) SWord 512 -> SWord 512 -> SBV (WordN (512 + 512))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# [SWord 8] -> SWord 512
forall a. ByteConverter a => [SWord 8] -> a
fromBytes (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
64 [SWord 8]
as)
     | Bool
True
     = String -> SWord 1024
forall a. HasCallStack => String -> a
error (String -> SWord 1024) -> String -> SWord 1024
forall a b. (a -> b) -> a -> b
$ String
"fromBytes:SWord 1024: Incorrect number of bytes: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l
     where l :: Int
l = [SWord 8] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
as