{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module What4.Utils.BVDomain.Bitwise
( Domain(..)
, bitle
, proper
, bvdMask
, member
, pmember
, size
, asSingleton
, nonempty
, eq
, domainsOverlap
, bitbounds
, any
, singleton
, range
, interval
, union
, intersection
, concat
, select
, zext
, sext
, testBit
, shl
, lshr
, ashr
, rol
, ror
, and
, or
, xor
, not
, genDomain
, genElement
, genPair
, correct_any
, correct_singleton
, correct_overlap
, correct_union
, correct_intersection
, correct_zero_ext
, correct_sign_ext
, correct_concat
, correct_shrink
, correct_trunc
, correct_select
, correct_shl
, correct_lshr
, correct_ashr
, correct_rol
, correct_ror
, correct_eq
, correct_and
, correct_or
, correct_not
, correct_xor
, correct_testBit
) where
import Data.Bits hiding (testBit, xor)
import qualified Data.Bits as Bits
import Data.Parameterized.NatRepr
import Numeric.Natural
import GHC.TypeNats
import Test.Verification (Property, property, (==>), Gen, chooseInteger)
import qualified Prelude
import Prelude hiding (any, concat, negate, and, or, not)
import qualified What4.Utils.Arithmetic as Arith
data Domain (w :: Nat) =
BVBitInterval !Integer !Integer !Integer
deriving (Int -> Domain w -> ShowS
forall (w :: Nat). Int -> Domain w -> ShowS
forall (w :: Nat). [Domain w] -> ShowS
forall (w :: Nat). Domain w -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Domain w] -> ShowS
$cshowList :: forall (w :: Nat). [Domain w] -> ShowS
show :: Domain w -> String
$cshow :: forall (w :: Nat). Domain w -> String
showsPrec :: Int -> Domain w -> ShowS
$cshowsPrec :: forall (w :: Nat). Int -> Domain w -> ShowS
Show)
proper :: NatRepr w -> Domain w -> Bool
proper :: forall (w :: Nat). NatRepr w -> Domain w -> Bool
proper NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) =
Integer
mask forall a. Eq a => a -> a -> Bool
== forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w Bool -> Bool -> Bool
&&
Integer -> Integer -> Bool
bitle Integer
lo Integer
mask Bool -> Bool -> Bool
&&
Integer -> Integer -> Bool
bitle Integer
hi Integer
mask Bool -> Bool -> Bool
&&
Integer -> Integer -> Bool
bitle Integer
lo Integer
hi
member :: Domain w -> Integer -> Bool
member :: forall (w :: Nat). Domain w -> Integer -> Bool
member (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
x = Integer -> Integer -> Bool
bitle Integer
lo Integer
x' Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
bitle Integer
x' Integer
hi
where x' :: Integer
x' = Integer
x forall a. Bits a => a -> a -> a
.&. Integer
mask
size :: Domain w -> Integer
size :: forall (w :: Nat). Domain w -> Integer
size (BVBitInterval Integer
_ Integer
lo Integer
hi)
| Integer -> Integer -> Bool
bitle Integer
lo Integer
hi = forall a. Bits a => Int -> a
Bits.bit Int
p
| Bool
otherwise = Integer
0
where
u :: Integer
u = forall a. Bits a => a -> a -> a
Bits.xor Integer
lo Integer
hi
p :: Int
p = forall a. Bits a => a -> Int
Bits.popCount Integer
u
bitle :: Integer -> Integer -> Bool
bitle :: Integer -> Integer -> Bool
bitle Integer
x Integer
y = (Integer
x forall a. Bits a => a -> a -> a
.|. Integer
y) forall a. Eq a => a -> a -> Bool
== Integer
y
bvdMask :: Domain w -> Integer
bvdMask :: forall (w :: Nat). Domain w -> Integer
bvdMask (BVBitInterval Integer
mask Integer
_ Integer
_) = Integer
mask
genDomain :: NatRepr w -> Gen (Domain w)
genDomain :: forall (w :: Nat). NatRepr w -> Gen (Domain w)
genDomain NatRepr w
w =
do let mask :: Integer
mask = forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w
Integer
lo <- (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, Integer
mask)
Integer
hi <- (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, Integer
mask)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
lo (Integer
lo forall a. Bits a => a -> a -> a
.|. Integer
hi)
genElement :: Domain w -> Gen Integer
genElement :: forall (w :: Nat). Domain w -> Gen Integer
genElement (BVBitInterval Integer
_mask Integer
lo Integer
hi) =
do Integer
x <- (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, forall a. Bits a => Int -> a
bit Int
bs forall a. Num a => a -> a -> a
- Integer
1)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Int -> Integer
stripe Integer
lo Integer
x Int
0
where
u :: Integer
u = forall a. Bits a => a -> a -> a
Bits.xor Integer
lo Integer
hi
bs :: Int
bs = forall a. Bits a => a -> Int
Bits.popCount Integer
u
stripe :: Integer -> Integer -> Int -> Integer
stripe Integer
val Integer
x Int
i
| Integer
x forall a. Eq a => a -> a -> Bool
== Integer
0 = Integer
val
| forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
u Int
i =
let val' :: Integer
val' = if forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
x Int
0 then forall a. Bits a => a -> Int -> a
setBit Integer
val Int
i else Integer
val in
Integer -> Integer -> Int -> Integer
stripe Integer
val' (Integer
x forall a. Bits a => a -> Int -> a
`shiftR` Int
1) (Int
iforall a. Num a => a -> a -> a
+Int
1)
| Bool
otherwise = Integer -> Integer -> Int -> Integer
stripe Integer
val Integer
x (Int
iforall a. Num a => a -> a -> a
+Int
1)
genPair :: NatRepr w -> Gen (Domain w, Integer)
genPair :: forall (w :: Nat). NatRepr w -> Gen (Domain w, Integer)
genPair NatRepr w
w =
do Domain w
a <- forall (w :: Nat). NatRepr w -> Gen (Domain w)
genDomain NatRepr w
w
Integer
x <- forall (w :: Nat). Domain w -> Gen Integer
genElement Domain w
a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Domain w
a,Integer
x)
interval :: Integer -> Integer -> Integer -> Domain w
interval :: forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
lo Integer
hi = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
lo Integer
hi
range :: NatRepr w -> Integer -> Integer -> Domain w
range :: forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr w
w Integer
lo Integer
hi = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval (forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w) Integer
lo' Integer
hi'
where
lo' :: Integer
lo' = Integer
lo forall a. Bits a => a -> a -> a
.&. Integer
mask
hi' :: Integer
hi' = Integer
hi forall a. Bits a => a -> a -> a
.&. Integer
mask
mask :: Integer
mask = forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w
bitbounds :: Domain w -> (Integer, Integer)
bitbounds :: forall (w :: Nat). Domain w -> (Integer, Integer)
bitbounds (BVBitInterval Integer
_ Integer
lo Integer
hi) = (Integer
lo, Integer
hi)
asSingleton :: Domain w -> Maybe Integer
asSingleton :: forall (w :: Nat). Domain w -> Maybe Integer
asSingleton (BVBitInterval Integer
_ Integer
lo Integer
hi) = if Integer
lo forall a. Eq a => a -> a -> Bool
== Integer
hi then forall a. a -> Maybe a
Just Integer
lo else forall a. Maybe a
Nothing
nonempty :: Domain w -> Bool
nonempty :: forall (w :: Nat). Domain w -> Bool
nonempty (BVBitInterval Integer
_mask Integer
lo Integer
hi) = Integer -> Integer -> Bool
bitle Integer
lo Integer
hi
singleton :: NatRepr w -> Integer -> Domain w
singleton :: forall (w :: Nat). NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
x = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
x' Integer
x'
where
x' :: Integer
x' = Integer
x forall a. Bits a => a -> a -> a
.&. Integer
mask
mask :: Integer
mask = forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w
any :: NatRepr w -> Domain w
any :: forall (w :: Nat). NatRepr w -> Domain w
any NatRepr w
w = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
0 Integer
mask
where
mask :: Integer
mask = forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w
domainsOverlap :: Domain w -> Domain w -> Bool
domainsOverlap :: forall (w :: Nat). Domain w -> Domain w -> Bool
domainsOverlap Domain w
a Domain w
b = forall (w :: Nat). Domain w -> Bool
nonempty (forall (w :: Nat). Domain w -> Domain w -> Domain w
intersection Domain w
a Domain w
b)
eq :: Domain w -> Domain w -> Maybe Bool
eq :: forall (w :: Nat). Domain w -> Domain w -> Maybe Bool
eq Domain w
a Domain w
b
| Just Integer
x <- forall (w :: Nat). Domain w -> Maybe Integer
asSingleton Domain w
a
, Just Integer
y <- forall (w :: Nat). Domain w -> Maybe Integer
asSingleton Domain w
b
= forall a. a -> Maybe a
Just (Integer
x forall a. Eq a => a -> a -> Bool
== Integer
y)
| Bool -> Bool
Prelude.not (forall (w :: Nat). Domain w -> Domain w -> Bool
domainsOverlap Domain w
a Domain w
b) = forall a. a -> Maybe a
Just Bool
False
| Bool
otherwise = forall a. Maybe a
Nothing
intersection :: Domain w -> Domain w -> Domain w
intersection :: forall (w :: Nat). Domain w -> Domain w -> Domain w
intersection (BVBitInterval Integer
mask Integer
alo Integer
ahi) (BVBitInterval Integer
_ Integer
blo Integer
bhi) =
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer
alo forall a. Bits a => a -> a -> a
.|. Integer
blo) (Integer
ahi forall a. Bits a => a -> a -> a
.&. Integer
bhi)
union :: Domain w -> Domain w -> Domain w
union :: forall (w :: Nat). Domain w -> Domain w -> Domain w
union (BVBitInterval Integer
mask Integer
alo Integer
ahi) (BVBitInterval Integer
_ Integer
blo Integer
bhi) =
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer
alo forall a. Bits a => a -> a -> a
.&. Integer
blo) (Integer
ahi forall a. Bits a => a -> a -> a
.|. Integer
bhi)
concat :: NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
concat :: forall (u :: Nat) (v :: Nat).
NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
concat NatRepr u
u (BVBitInterval Integer
_ Integer
alo Integer
ahi) NatRepr v
v (BVBitInterval Integer
_ Integer
blo Integer
bhi) =
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer -> Integer -> Integer
cat Integer
alo Integer
blo) (Integer -> Integer -> Integer
cat Integer
ahi Integer
bhi)
where
cat :: Integer -> Integer -> Integer
cat Integer
i Integer
j = (Integer
i forall a. Bits a => a -> Int -> a
`shiftL` forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr v
v) forall a. Num a => a -> a -> a
+ Integer
j
mask :: Integer
mask = forall (w :: Nat). NatRepr w -> Integer
maxUnsigned (forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr u
u NatRepr v
v)
shrink ::
NatRepr i ->
Domain (i + n) -> Domain n
shrink :: forall (i :: Nat) (n :: Nat).
NatRepr i -> Domain (i + n) -> Domain n
shrink NatRepr i
i (BVBitInterval Integer
mask Integer
lo Integer
hi) = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval (Integer -> Integer
shr Integer
mask) (Integer -> Integer
shr Integer
lo) (Integer -> Integer
shr Integer
hi)
where
shr :: Integer -> Integer
shr Integer
x = Integer
x forall a. Bits a => a -> Int -> a
`shiftR` forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr i
i
trunc ::
(n <= w) =>
NatRepr n ->
Domain w ->
Domain n
trunc :: forall (n :: Nat) (w :: Nat).
(n <= w) =>
NatRepr n -> Domain w -> Domain n
trunc NatRepr n
n (BVBitInterval Integer
_ Integer
lo Integer
hi) = forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr n
n Integer
lo Integer
hi
select ::
(1 <= n, i + n <= w) =>
NatRepr i ->
NatRepr n ->
Domain w -> Domain n
select :: forall (n :: Nat) (i :: Nat) (w :: Nat).
(1 <= n, (i + n) <= w) =>
NatRepr i -> NatRepr n -> Domain w -> Domain n
select NatRepr i
i NatRepr n
n Domain w
a = forall (i :: Nat) (n :: Nat).
NatRepr i -> Domain (i + n) -> Domain n
shrink NatRepr i
i (forall (n :: Nat) (w :: Nat).
(n <= w) =>
NatRepr n -> Domain w -> Domain n
trunc (forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr i
i NatRepr n
n) Domain w
a)
zext :: (1 <= w, w+1 <= u) => Domain w -> NatRepr u -> Domain u
zext :: forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
Domain w -> NatRepr u -> Domain u
zext (BVBitInterval Integer
_ Integer
lo Integer
hi) NatRepr u
u = forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr u
u Integer
lo Integer
hi
sext :: (1 <= w, w+1 <= u) => NatRepr w -> Domain w -> NatRepr u -> Domain u
sext :: forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> Domain w -> NatRepr u -> Domain u
sext NatRepr w
w (BVBitInterval Integer
_ Integer
lo Integer
hi) NatRepr u
u = forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr u
u Integer
lo' Integer
hi'
where
lo' :: Integer
lo' = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr w
w Integer
lo
hi' :: Integer
hi' = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr w
w Integer
hi
testBit :: Domain w -> Natural -> Maybe Bool
testBit :: forall (w :: Nat). Domain w -> Nat -> Maybe Bool
testBit (BVBitInterval Integer
_mask Integer
lo Integer
hi) Nat
i = if Bool
lob forall a. Eq a => a -> a -> Bool
== Bool
hib then forall a. a -> Maybe a
Just Bool
lob else forall a. Maybe a
Nothing
where
lob :: Bool
lob = forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
lo Int
j
hib :: Bool
hib = forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
hi Int
j
j :: Int
j = forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
i
shl :: NatRepr w -> Domain w -> Integer -> Domain w
shl :: forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
shl NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
y = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer -> Integer
shleft Integer
lo) (Integer -> Integer
shleft Integer
hi)
where
y' :: Int
y' = forall a. Num a => Integer -> a
fromInteger (forall a. Ord a => a -> a -> a
min Integer
y (forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w))
shleft :: Integer -> Integer
shleft Integer
x = (Integer
x forall a. Bits a => a -> Int -> a
`shiftL` Int
y') forall a. Bits a => a -> a -> a
.&. Integer
mask
rol :: NatRepr w -> Domain w -> Integer -> Domain w
rol :: forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
rol NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
y =
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateLeft NatRepr w
w Integer
lo Integer
y) (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateLeft NatRepr w
w Integer
hi Integer
y)
ror :: NatRepr w -> Domain w -> Integer -> Domain w
ror :: forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
ror NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
y =
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateRight NatRepr w
w Integer
lo Integer
y) (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateRight NatRepr w
w Integer
hi Integer
y)
lshr :: NatRepr w -> Domain w -> Integer -> Domain w
lshr :: forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
lshr NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
y = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer -> Integer
shr Integer
lo) (Integer -> Integer
shr Integer
hi)
where
y' :: Int
y' = forall a. Num a => Integer -> a
fromInteger (forall a. Ord a => a -> a -> a
min Integer
y (forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w))
shr :: Integer -> Integer
shr Integer
x = Integer
x forall a. Bits a => a -> Int -> a
`shiftR` Int
y'
ashr :: (1 <= w) => NatRepr w -> Domain w -> Integer -> Domain w
ashr :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Integer -> Domain w
ashr NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
y = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer -> Integer
shr Integer
lo) (Integer -> Integer
shr Integer
hi)
where
y' :: Int
y' = forall a. Num a => Integer -> a
fromInteger (forall a. Ord a => a -> a -> a
min Integer
y (forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w))
shr :: Integer -> Integer
shr Integer
x = ((forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr w
w Integer
x) forall a. Bits a => a -> Int -> a
`shiftR` Int
y') forall a. Bits a => a -> a -> a
.&. Integer
mask
not :: Domain w -> Domain w
not :: forall (w :: Nat). Domain w -> Domain w
not (BVBitInterval Integer
mask Integer
alo Integer
ahi) =
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer
ahi forall a. Bits a => a -> a -> a
`Bits.xor` Integer
mask) (Integer
alo forall a. Bits a => a -> a -> a
`Bits.xor` Integer
mask)
and :: Domain w -> Domain w -> Domain w
and :: forall (w :: Nat). Domain w -> Domain w -> Domain w
and (BVBitInterval Integer
mask Integer
alo Integer
ahi) (BVBitInterval Integer
_ Integer
blo Integer
bhi) =
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer
alo forall a. Bits a => a -> a -> a
.&. Integer
blo) (Integer
ahi forall a. Bits a => a -> a -> a
.&. Integer
bhi)
or :: Domain w -> Domain w -> Domain w
or :: forall (w :: Nat). Domain w -> Domain w -> Domain w
or (BVBitInterval Integer
mask Integer
alo Integer
ahi) (BVBitInterval Integer
_ Integer
blo Integer
bhi) =
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer
alo forall a. Bits a => a -> a -> a
.|. Integer
blo) (Integer
ahi forall a. Bits a => a -> a -> a
.|. Integer
bhi)
xor :: Domain w -> Domain w -> Domain w
xor :: forall (w :: Nat). Domain w -> Domain w -> Domain w
xor (BVBitInterval Integer
mask Integer
alo Integer
ahi) (BVBitInterval Integer
_ Integer
blo Integer
bhi) = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
clo Integer
chi
where
au :: Integer
au = Integer
alo forall a. Bits a => a -> a -> a
`Bits.xor` Integer
ahi
bu :: Integer
bu = Integer
blo forall a. Bits a => a -> a -> a
`Bits.xor` Integer
bhi
c :: Integer
c = Integer
alo forall a. Bits a => a -> a -> a
`Bits.xor` Integer
blo
cu :: Integer
cu = Integer
au forall a. Bits a => a -> a -> a
.|. Integer
bu
chi :: Integer
chi = Integer
c forall a. Bits a => a -> a -> a
.|. Integer
cu
clo :: Integer
clo = Integer
chi forall a. Bits a => a -> a -> a
`Bits.xor` Integer
cu
pmember :: NatRepr n -> Domain n -> Integer -> Bool
pmember :: forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n Domain n
a Integer
x = forall (w :: Nat). NatRepr w -> Domain w -> Bool
proper NatRepr n
n Domain n
a Bool -> Bool -> Bool
&& forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x
correct_any :: (1 <= n) => NatRepr n -> Integer -> Property
correct_any :: forall (n :: Nat). (1 <= n) => NatRepr n -> Integer -> Property
correct_any NatRepr n
n Integer
x = Bool -> Property
property (forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). NatRepr w -> Domain w
any NatRepr n
n) Integer
x)
correct_singleton :: (1 <= n) => NatRepr n -> Integer -> Integer -> Property
correct_singleton :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Integer -> Integer -> Property
correct_singleton NatRepr n
n Integer
x Integer
y = Bool -> Property
property (forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). NatRepr w -> Integer -> Domain w
singleton NatRepr n
n Integer
x') Integer
y' forall a. Eq a => a -> a -> Bool
== (Integer
x' forall a. Eq a => a -> a -> Bool
== Integer
y'))
where
x' :: Integer
x' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x
y' :: Integer
y' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y
correct_overlap :: Domain n -> Domain n -> Integer -> Property
correct_overlap :: forall (n :: Nat). Domain n -> Domain n -> Integer -> Property
correct_overlap Domain n
a Domain n
b Integer
x =
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Bool -> Bool
&& forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). Domain w -> Domain w -> Bool
domainsOverlap Domain n
a Domain n
b
correct_union :: (1 <= n) => NatRepr n -> Domain n -> Domain n -> Integer -> Property
correct_union :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Domain n -> Domain n -> Integer -> Property
correct_union NatRepr n
n Domain n
a Domain n
b Integer
x =
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Bool -> Bool
|| forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w -> Domain w
union Domain n
a Domain n
b) Integer
x
correct_intersection :: (1 <= n) => Domain n -> Domain n -> Integer -> Property
correct_intersection :: forall (n :: Nat).
(1 <= n) =>
Domain n -> Domain n -> Integer -> Property
correct_intersection Domain n
a Domain n
b Integer
x =
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Bool -> Bool
&& forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). Domain w -> Integer -> Bool
member (forall (w :: Nat). Domain w -> Domain w -> Domain w
intersection Domain n
a Domain n
b) Integer
x
correct_zero_ext :: (1 <= w, w+1 <= u) => NatRepr w -> Domain w -> NatRepr u -> Integer -> Property
correct_zero_ext :: forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> Domain w -> NatRepr u -> Integer -> Property
correct_zero_ext NatRepr w
w Domain w
a NatRepr u
u Integer
x = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain w
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr u
u (forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
Domain w -> NatRepr u -> Domain u
zext Domain w
a NatRepr u
u) Integer
x'
where
x' :: Integer
x' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr w
w Integer
x
correct_sign_ext :: (1 <= w, w+1 <= u) => NatRepr w -> Domain w -> NatRepr u -> Integer -> Property
correct_sign_ext :: forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> Domain w -> NatRepr u -> Integer -> Property
correct_sign_ext NatRepr w
w Domain w
a NatRepr u
u Integer
x = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain w
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr u
u (forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> Domain w -> NatRepr u -> Domain u
sext NatRepr w
w Domain w
a NatRepr u
u) Integer
x'
where
x' :: Integer
x' = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr w
w Integer
x
correct_concat :: NatRepr m -> (Domain m,Integer) -> NatRepr n -> (Domain n,Integer) -> Property
correct_concat :: forall (m :: Nat) (n :: Nat).
NatRepr m
-> (Domain m, Integer)
-> NatRepr n
-> (Domain n, Integer)
-> Property
correct_concat NatRepr m
m (Domain m
a,Integer
x) NatRepr n
n (Domain n
b,Integer
y) = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain m
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
y' forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember (forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr m
m NatRepr n
n) (forall (u :: Nat) (v :: Nat).
NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
concat NatRepr m
m Domain m
a NatRepr n
n Domain n
b) Integer
z
where
x' :: Integer
x' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr m
m Integer
x
y' :: Integer
y' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y
z :: Integer
z = Integer
x' forall a. Bits a => a -> Int -> a
`shiftL` (forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr n
n) forall a. Bits a => a -> a -> a
.|. Integer
y'
correct_shrink :: NatRepr i -> NatRepr n -> (Domain (i + n), Integer) -> Property
correct_shrink :: forall (i :: Nat) (n :: Nat).
NatRepr i -> NatRepr n -> (Domain (i + n), Integer) -> Property
correct_shrink NatRepr i
i NatRepr n
n (Domain (i + n)
a,Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain (i + n)
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (i :: Nat) (n :: Nat).
NatRepr i -> Domain (i + n) -> Domain n
shrink NatRepr i
i Domain (i + n)
a) (Integer
x' forall a. Bits a => a -> Int -> a
`shiftR` forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr i
i)
where
x' :: Integer
x' = Integer
x forall a. Bits a => a -> a -> a
.&. forall (w :: Nat). Domain w -> Integer
bvdMask Domain (i + n)
a
correct_trunc :: (n <= w) => NatRepr n -> (Domain w, Integer) -> Property
correct_trunc :: forall (n :: Nat) (w :: Nat).
(n <= w) =>
NatRepr n -> (Domain w, Integer) -> Property
correct_trunc NatRepr n
n (Domain w
a,Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain w
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (n :: Nat) (w :: Nat).
(n <= w) =>
NatRepr n -> Domain w -> Domain n
trunc NatRepr n
n Domain w
a) (forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x')
where
x' :: Integer
x' = Integer
x forall a. Bits a => a -> a -> a
.&. forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
correct_select :: (1 <= n, i + n <= w) =>
NatRepr i -> NatRepr n -> (Domain w, Integer) -> Property
correct_select :: forall (n :: Nat) (i :: Nat) (w :: Nat).
(1 <= n, (i + n) <= w) =>
NatRepr i -> NatRepr n -> (Domain w, Integer) -> Property
correct_select NatRepr i
i NatRepr n
n (Domain w
a, Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain w
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (n :: Nat) (i :: Nat) (w :: Nat).
(1 <= n, (i + n) <= w) =>
NatRepr i -> NatRepr n -> Domain w -> Domain n
select NatRepr i
i NatRepr n
n Domain w
a) Integer
y
where
y :: Integer
y = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n ((Integer
x forall a. Bits a => a -> a -> a
.&. forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a) forall a. Bits a => a -> Int -> a
`shiftR` (forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr i
i))
correct_eq :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_eq :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_eq NatRepr n
n (Domain n
a,Integer
x) (Domain n
b,Integer
y) =
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==>
case forall (w :: Nat). Domain w -> Domain w -> Maybe Bool
eq Domain n
a Domain n
b of
Just Bool
True -> forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x forall a. Eq a => a -> a -> Bool
== forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y
Just Bool
False -> forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x forall a. Eq a => a -> a -> Bool
/= forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y
Maybe Bool
Nothing -> Bool
True
correct_shl :: (1 <= n) => NatRepr n -> (Domain n,Integer) -> Integer -> Property
correct_shl :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_shl NatRepr n
n (Domain n
a,Integer
x) Integer
y = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
shl NatRepr n
n Domain n
a Integer
y) Integer
z
where
z :: Integer
z = (forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x) forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => Integer -> a
fromInteger (forall a. Ord a => a -> a -> a
min (forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr n
n) Integer
y)
correct_lshr :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_lshr :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_lshr NatRepr n
n (Domain n
a,Integer
x) Integer
y = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
lshr NatRepr n
n Domain n
a Integer
y) Integer
z
where
z :: Integer
z = (forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x) forall a. Bits a => a -> Int -> a
`shiftR` forall a. Num a => Integer -> a
fromInteger (forall a. Ord a => a -> a -> a
min (forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr n
n) Integer
y)
correct_ashr :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_ashr :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_ashr NatRepr n
n (Domain n
a,Integer
x) Integer
y = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Integer -> Domain w
ashr NatRepr n
n Domain n
a Integer
y) Integer
z
where
z :: Integer
z = (forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x) forall a. Bits a => a -> Int -> a
`shiftR` forall a. Num a => Integer -> a
fromInteger (forall a. Ord a => a -> a -> a
min (forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr n
n) Integer
y)
correct_rol :: (1 <= n) => NatRepr n -> (Domain n,Integer) -> Integer -> Property
correct_rol :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_rol NatRepr n
n (Domain n
a,Integer
x) Integer
y = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
rol NatRepr n
n Domain n
a Integer
y) (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateLeft NatRepr n
n Integer
x Integer
y)
correct_ror :: (1 <= n) => NatRepr n -> (Domain n,Integer) -> Integer -> Property
correct_ror :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_ror NatRepr n
n (Domain n
a,Integer
x) Integer
y = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
ror NatRepr n
n Domain n
a Integer
y) (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateRight NatRepr n
n Integer
x Integer
y)
correct_not :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Property
correct_not :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> Property
correct_not NatRepr n
n (Domain n
a,Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w
not Domain n
a) (forall a. Bits a => a -> a
complement Integer
x)
correct_and :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_and :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_and NatRepr n
n (Domain n
a,Integer
x) (Domain n
b,Integer
y) = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w -> Domain w
and Domain n
a Domain n
b) (Integer
x forall a. Bits a => a -> a -> a
.&. Integer
y)
correct_or :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_or :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_or NatRepr n
n (Domain n
a,Integer
x) (Domain n
b,Integer
y) = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w -> Domain w
or Domain n
a Domain n
b) (Integer
x forall a. Bits a => a -> a -> a
.|. Integer
y)
correct_xor :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_xor :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_xor NatRepr n
n (Domain n
a,Integer
x) (Domain n
b,Integer
y) = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w -> Domain w
xor Domain n
a Domain n
b) (Integer
x forall a. Bits a => a -> a -> a
`Bits.xor` Integer
y)
correct_testBit :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Natural -> Property
correct_testBit :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> Nat -> Property
correct_testBit NatRepr n
n (Domain n
a,Integer
x) Nat
i =
Nat
i forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr n
n forall t. Verifiable t => Bool -> t -> Property
==>
case forall (w :: Nat). Domain w -> Nat -> Maybe Bool
testBit Domain n
a Nat
i of
Just Bool
True -> forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
x (forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
i)
Just Bool
False -> Bool -> Bool
Prelude.not (forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
x (forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
i))
Maybe Bool
Nothing -> Bool
True