{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Core.Sized (
SWord, WordN, sWord, sWord_, sWords
, SInt, IntN, sInt, sInt_, sInts
, bvExtract, (#), zeroExtend, signExtend, bvDrop, bvTake
, 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
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
Ord)
type SWord (n :: Nat) = SBV (WordN n)
instance Show (WordN n) where
show :: WordN n -> String
show (WordN Integer
v) = Integer -> String
forall a. Show a => a -> String
show Integer
v
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))
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 :: forall (m :: * -> *).
MonadSymbolic m =>
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
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
Ord)
type SInt (n :: Nat) = SBV (IntN n)
instance Show (IntN n) where
show :: IntN n -> String
show (IntN Integer
v) = Integer -> String
forall a. Show a => a -> String
show Integer
v
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))
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 :: forall (m :: * -> *).
MonadSymbolic m =>
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
lift1 :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> SVal) -> bv n -> bv n
lift1 :: 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
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)
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 :: 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
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)
lift2I :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I :: 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
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)
lift2IB :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
lift2IB :: 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
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)
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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
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))
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))
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
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
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
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
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)
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)
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))
bitSize :: WordN n -> Int
bitSize WordN n
_ = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))
bitSize :: IntN n -> Int
bitSize IntN n
_ = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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
instance (KnownNat n, BVIsNonZero n) => SIntegral (WordN n)
instance (KnownNat n, BVIsNonZero n) => SIntegral (IntN n)
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
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
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
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
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n)
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n)
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))
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))
instance (KnownNat n, BVIsNonZero n) => Metric (WordN n)
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
sWord :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => String -> m (SWord n)
sWord :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
String -> m (SWord n)
sWord = String -> m (SBV (WordN n))
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic
sWord_ :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => m (SWord n)
sWord_ :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
m (SWord n)
sWord_ = m (SBV (WordN n))
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_
sWords :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => [String] -> m [SWord n]
sWords :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
[String] -> m [SWord n]
sWords = [String] -> m [SBV (WordN n)]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics
sInt :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => String -> m (SInt n)
sInt :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
String -> m (SInt n)
sInt = String -> m (SBV (IntN n))
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic
sInt_ :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => m (SInt n)
sInt_ :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
m (SInt n)
sInt_ = m (SBV (IntN n))
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_
sInts :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => [String] -> m [SInt n]
sInts :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
[String] -> m [SInt n]
sInts = [String] -> m [SBV (IntN n)]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics
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
-> proxy j
-> SBV (bv n)
-> SBV (bv (i - j + 1))
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)
(#) :: ( KnownNat n, BVIsNonZero n, SymVal (bv n)
, KnownNat m, BVIsNonZero m, SymVal (bv m)
) => SBV (bv n)
-> SBV (bv m)
-> SBV (bv (n + m))
SBV (bv n)
n # :: 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))
# 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 #
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)
-> SBV (bv m)
zeroExtend :: forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(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) -> 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
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)
-> SBV (bv m)
signExtend :: forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(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) -> 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
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
-> SBV (bv n)
-> SBV (bv m)
bvDrop :: forall (i :: Nat) (n :: Nat) (m :: Nat) (bv :: Nat -> *)
(proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, KnownNat i, (i + 1) <= n,
((i + m) - n) <= 0, BVIsNonZero (n - i)) =>
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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
bvTake :: forall i n bv proxy. ( KnownNat n, BVIsNonZero n
, KnownNat i, BVIsNonZero i
, i <= n
) => proxy i
-> SBV (bv n)
-> SBV (bv i)
bvTake :: forall (i :: Nat) (n :: Nat) (bv :: Nat -> *) (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, KnownNat i, BVIsNonZero i, i <= n) =>
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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
class ByteConverter a where
toBytes :: a -> [SWord 8]
fromBytes :: [SWord 8] -> a
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)
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @15) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @7) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @31) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @23) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @15) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @7) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @63) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @55) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @47) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @39) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @31) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @23) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @15) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @7) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @127) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @119) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @111) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @103) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @95) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @87) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @79) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @71) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @63) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @55) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @47) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @39) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @31) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @23) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @15) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @7) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @255) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @247) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @239) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @231) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @223) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @215) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @207) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @199) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @191) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @183) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @175) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @167) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @159) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @151) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @143) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @135) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @127) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @119) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @111) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @103) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @95) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @87) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @79) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @71) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @63) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @55) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @47) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @39) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @31) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @23) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @15) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @7) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @511) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @503) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @495) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @487) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @479) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @471) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @463) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @455) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @447) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @439) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @431) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @423) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @415) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @407) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @399) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @391) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @383) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @375) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @367) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @359) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @351) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @343) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @335) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @327) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @319) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @311) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @303) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @295) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @287) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @279) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @271) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @263) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @255) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @247) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @239) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @231) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @223) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @215) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @207) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @199) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @191) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @183) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @175) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @167) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @159) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @151) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @143) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @135) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @127) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @119) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @111) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @103) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @95) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @87) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @79) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @71) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @63) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @55) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @47) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @39) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @31) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @23) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @15) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @7) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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
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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @1023) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @1015) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @1007) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @999) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @991) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @983) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @975) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @967) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @959) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @951) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @943) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @935) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @927) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @919) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @911) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @903) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @895) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @887) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @879) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @871) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @863) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @855) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @847) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @839) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @831) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @823) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @815) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @807) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @799) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @791) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @783) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @775) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @767) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @759) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @751) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @743) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @735) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @727) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @719) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @711) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @703) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @695) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @687) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @679) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @671) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @663) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @655) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @647) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @639) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @631) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @623) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @615) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @607) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @599) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @591) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @583) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @575) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @567) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @559) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @551) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @543) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @535) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @527) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @519) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @511) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @503) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @495) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @487) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @479) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @471) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @463) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @455) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @447) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @439) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @431) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @423) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @415) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @407) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @399) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @391) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @383) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @375) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @367) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @359) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @351) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @343) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @335) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @327) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @319) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @311) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @303) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @295) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @287) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @279) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @271) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @263) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @255) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @247) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @239) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @231) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @223) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @215) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @207) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @199) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @191) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @183) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @175) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @167) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @159) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @151) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @143) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @135) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @127) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @119) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @111) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @103) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @95) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @87) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @79) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @71) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @63) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @55) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @47) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @39) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @31) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @23) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @15) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @7) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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