{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module What4.Utils.BVDomain
(
BVDomain(..)
, proper
, member
, size
, asArithDomain
, asBitwiseDomain
, asXorDomain
, fromXorDomain
, arithToXorDomain
, bitwiseToXorDomain
, xorToBitwiseDomain
, asSingleton
, eq
, slt
, ult
, testBit
, domainsOverlap
, ubounds
, sbounds
, isUltSumCommonEquiv
, A.arithDomainData
, B.bitbounds
, any
, singleton
, range
, fromAscEltList
, union
, concat
, select
, zext
, sext
, shl
, lshr
, ashr
, rol
, ror
, add
, negate
, scale
, mul
, udiv
, urem
, sdiv
, srem
, What4.Utils.BVDomain.not
, and
, or
, xor
, popcnt
, clz
, ctz
, bitwiseRoundAbove
, bitwiseRoundBetween
, genDomain
, genElement
, genPair
, correct_arithToBitwise
, correct_bitwiseToArith
, correct_bitwiseToXorDomain
, correct_arithToXorDomain
, correct_xorToBitwiseDomain
, correct_asXorDomain
, correct_fromXorDomain
, correct_bra1
, correct_bra2
, correct_brb1
, correct_brb2
, correct_any
, correct_ubounds
, correct_sbounds
, correct_singleton
, correct_overlap
, precise_overlap
, correct_union
, correct_zero_ext
, correct_sign_ext
, correct_concat
, correct_select
, correct_add
, correct_neg
, correct_mul
, correct_scale
, correct_udiv
, correct_urem
, correct_sdiv
, correct_srem
, correct_shl
, correct_lshr
, correct_ashr
, correct_rol
, correct_ror
, correct_eq
, correct_ult
, correct_slt
, correct_and
, correct_or
, correct_not
, correct_xor
, correct_testBit
, correct_popcnt
, correct_clz
, correct_ctz
) where
import qualified Data.Bits as Bits
import Data.Bits hiding (testBit, xor)
import qualified Data.List as List
import Data.Parameterized.NatRepr
import Numeric.Natural
import GHC.TypeNats
import GHC.Stack
import qualified Prelude
import Prelude hiding (any, concat, negate, and, or, not)
import qualified What4.Utils.Arithmetic as Arith
import qualified What4.Utils.BVDomain.Arith as A
import qualified What4.Utils.BVDomain.Bitwise as B
import qualified What4.Utils.BVDomain.XOR as X
import Test.Verification ( Property, property, (==>), Gen, chooseBool )
arithToBitwiseDomain :: A.Domain w -> B.Domain w
arithToBitwiseDomain :: forall (w :: Nat). Domain w -> Domain w
arithToBitwiseDomain Domain w
a =
let mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
A.bvdMask Domain w
a in
case forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
A.arithDomainData Domain w
a of
Maybe (Integer, Integer)
Nothing -> forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
B.interval Integer
mask Integer
0 Integer
mask
Just (Integer
alo,Integer
_) -> forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
B.interval Integer
mask Integer
lo Integer
hi
where
u :: Integer
u = forall (w :: Nat). Domain w -> Integer
A.unknowns Domain w
a
hi :: Integer
hi = Integer
alo forall a. Bits a => a -> a -> a
.|. Integer
u
lo :: Integer
lo = Integer
hi forall a. Bits a => a -> a -> a
`Bits.xor` Integer
u
bitwiseToArithDomain :: B.Domain w -> A.Domain w
bitwiseToArithDomain :: forall (w :: Nat). Domain w -> Domain w
bitwiseToArithDomain Domain w
b = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
A.interval Integer
mask Integer
lo ((Integer
hi forall a. Num a => a -> a -> a
- Integer
lo) forall a. Bits a => a -> a -> a
.&. Integer
mask)
where
mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
B.bvdMask Domain w
b
(Integer
lo,Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b
bitwiseToXorDomain :: B.Domain w -> X.Domain w
bitwiseToXorDomain :: forall (w :: Nat). Domain w -> Domain w
bitwiseToXorDomain Domain w
b = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
X.interval Integer
mask Integer
lo Integer
hi
where
mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
B.bvdMask Domain w
b
(Integer
lo,Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b
arithToXorDomain :: A.Domain w -> X.Domain w
arithToXorDomain :: forall (w :: Nat). Domain w -> Domain w
arithToXorDomain Domain w
a =
let mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
A.bvdMask Domain w
a in
case forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
A.arithDomainData Domain w
a of
Maybe (Integer, Integer)
Nothing -> forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
X.BVDXor Integer
mask Integer
mask Integer
mask
Just (Integer
alo,Integer
_) -> forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
X.BVDXor Integer
mask Integer
hi Integer
u
where
u :: Integer
u = forall (w :: Nat). Domain w -> Integer
A.unknowns Domain w
a
hi :: Integer
hi = Integer
alo forall a. Bits a => a -> a -> a
.|. Integer
u
xorToBitwiseDomain :: X.Domain w -> B.Domain w
xorToBitwiseDomain :: forall (w :: Nat). Domain w -> Domain w
xorToBitwiseDomain Domain w
x = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
B.interval Integer
mask Integer
lo Integer
hi
where
mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
X.bvdMask Domain w
x
(Integer
lo, Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
X.bitbounds Domain w
x
asXorDomain :: BVDomain w -> X.Domain w
asXorDomain :: forall (w :: Nat). BVDomain w -> Domain w
asXorDomain (BVDArith Domain w
a) = forall (w :: Nat). Domain w -> Domain w
arithToXorDomain Domain w
a
asXorDomain (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> Domain w
bitwiseToXorDomain Domain w
b
fromXorDomain :: X.Domain w -> BVDomain w
fromXorDomain :: forall (w :: Nat). Domain w -> BVDomain w
fromXorDomain Domain w
x = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat). Domain w -> Domain w
xorToBitwiseDomain Domain w
x)
asArithDomain :: BVDomain w -> A.Domain w
asArithDomain :: forall (w :: Nat). BVDomain w -> Domain w
asArithDomain (BVDArith Domain w
a) = Domain w
a
asArithDomain (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> Domain w
bitwiseToArithDomain Domain w
b
asBitwiseDomain :: BVDomain w -> B.Domain w
asBitwiseDomain :: forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain (BVDArith Domain w
a) = forall (w :: Nat). Domain w -> Domain w
arithToBitwiseDomain Domain w
a
asBitwiseDomain (BVDBitwise Domain w
b) = Domain w
b
data BVDomain (w :: Nat)
= BVDArith !(A.Domain w)
| BVDBitwise !(B.Domain w)
deriving Int -> BVDomain w -> ShowS
forall (w :: Nat). Int -> BVDomain w -> ShowS
forall (w :: Nat). [BVDomain w] -> ShowS
forall (w :: Nat). BVDomain w -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BVDomain w] -> ShowS
$cshowList :: forall (w :: Nat). [BVDomain w] -> ShowS
show :: BVDomain w -> String
$cshow :: forall (w :: Nat). BVDomain w -> String
showsPrec :: Int -> BVDomain w -> ShowS
$cshowsPrec :: forall (w :: Nat). Int -> BVDomain w -> ShowS
Show
bvdMask :: BVDomain w -> Integer
bvdMask :: forall (w :: Nat). BVDomain w -> Integer
bvdMask BVDomain w
x =
case BVDomain w
x of
BVDArith Domain w
a -> forall (w :: Nat). Domain w -> Integer
A.bvdMask Domain w
a
BVDBitwise Domain w
b -> forall (w :: Nat). Domain w -> Integer
B.bvdMask Domain w
b
proper :: NatRepr w -> BVDomain w -> Bool
proper :: forall (w :: Nat). NatRepr w -> BVDomain w -> Bool
proper NatRepr w
w (BVDArith Domain w
a) = forall (w :: Nat). NatRepr w -> Domain w -> Bool
A.proper NatRepr w
w Domain w
a
proper NatRepr w
w (BVDBitwise Domain w
b) = forall (w :: Nat). NatRepr w -> Domain w -> Bool
B.proper NatRepr w
w Domain w
b
member :: BVDomain w -> Integer -> Bool
member :: forall (w :: Nat). BVDomain w -> Integer -> Bool
member (BVDArith Domain w
a) Integer
x = forall (w :: Nat). Domain w -> Integer -> Bool
A.member Domain w
a Integer
x
member (BVDBitwise Domain w
a) Integer
x = forall (w :: Nat). Domain w -> Integer -> Bool
B.member Domain w
a Integer
x
size :: BVDomain w -> Integer
size :: forall (w :: Nat). BVDomain w -> Integer
size (BVDArith Domain w
a) = forall (w :: Nat). Domain w -> Integer
A.size Domain w
a
size (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> Integer
B.size Domain w
b
genDomain :: NatRepr w -> Gen (BVDomain w)
genDomain :: forall (w :: Nat). NatRepr w -> Gen (BVDomain w)
genDomain NatRepr w
w =
do Bool
b <- Gen Bool
chooseBool
if Bool
b then
forall (w :: Nat). Domain w -> BVDomain w
BVDArith forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Nat). NatRepr w -> Gen (Domain w)
A.genDomain NatRepr w
w
else
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Nat). NatRepr w -> Gen (Domain w)
B.genDomain NatRepr w
w
genElement :: BVDomain w -> Gen Integer
genElement :: forall (w :: Nat). BVDomain w -> Gen Integer
genElement (BVDArith Domain w
a) = forall (w :: Nat). Domain w -> Gen Integer
A.genElement Domain w
a
genElement (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> Gen Integer
B.genElement Domain w
b
genPair :: NatRepr w -> Gen (BVDomain w, Integer)
genPair :: forall (w :: Nat). NatRepr w -> Gen (BVDomain w, Integer)
genPair NatRepr w
w =
do BVDomain w
a <- forall (w :: Nat). NatRepr w -> Gen (BVDomain w)
genDomain NatRepr w
w
Integer
x <- forall (w :: Nat). BVDomain w -> Gen Integer
genElement BVDomain w
a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BVDomain w
a,Integer
x)
asSingleton :: BVDomain w -> Maybe Integer
asSingleton :: forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton (BVDArith Domain w
a) = forall (w :: Nat). Domain w -> Maybe Integer
A.asSingleton Domain w
a
asSingleton (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> Maybe Integer
B.asSingleton Domain w
b
bitwiseRoundAbove ::
Integer ->
Integer ->
Integer ->
Integer
bitwiseRoundAbove :: Integer -> Integer -> Integer -> Integer
bitwiseRoundAbove Integer
bvmask Integer
x Integer
lomask = Integer
upperbits forall a. Bits a => a -> a -> a
.|. Integer
lowerbits
where
upperbits :: Integer
upperbits = Integer
x forall a. Bits a => a -> a -> a
.&. (Integer
bvmask forall a. Bits a => a -> a -> a
`Bits.xor` Integer
fillmask)
lowerbits :: Integer
lowerbits = Integer
lomask forall a. Bits a => a -> a -> a
.&. Integer
fillmask
fillmask :: Integer
fillmask = Integer -> Integer
A.fillright ((Integer
x forall a. Bits a => a -> a -> a
.|. Integer
lomask) forall a. Bits a => a -> a -> a
`Bits.xor` Integer
x)
bitwiseRoundBetween ::
Integer ->
Integer ->
Integer ->
Integer ->
Integer
bitwiseRoundBetween :: Integer -> Integer -> Integer -> Integer -> Integer
bitwiseRoundBetween Integer
bvmask Integer
x Integer
lomask Integer
himask = Integer
final
where
final :: Integer
final = (Integer
upper forall a. Bits a => a -> a -> a
.&. (Integer
lobits forall a. Bits a => a -> a -> a
`Bits.xor` Integer
bvmask)) forall a. Bits a => a -> a -> a
.|. Integer
lomask
upper :: Integer
upper = (Integer
z forall a. Num a => a -> a -> a
+ Integer
highbit) forall a. Bits a => a -> a -> a
.&. Integer
himask
z :: Integer
z = Integer
loup forall a. Bits a => a -> a -> a
.|. Integer
himask'
highbit :: Integer
highbit = Integer
rmask forall a. Bits a => a -> a -> a
`Bits.xor` Integer
lobits
lobits :: Integer
lobits = Integer
rmask forall a. Bits a => a -> Int -> a
`shiftR` Int
1
rmask :: Integer
rmask = Integer -> Integer
A.fillright Integer
r
r :: Integer
r = Integer
loup forall a. Bits a => a -> a -> a
.&. Integer
himask'
himask' :: Integer
himask' = Integer
himask forall a. Bits a => a -> a -> a
`Bits.xor` Integer
bvmask
loup :: Integer
loup = Integer -> Integer -> Integer -> Integer
bitwiseRoundAbove Integer
bvmask Integer
x Integer
lomask
mixedDomainsOverlap :: A.Domain a -> B.Domain b -> Bool
mixedDomainsOverlap :: forall (a :: Nat) (b :: Nat). Domain a -> Domain b -> Bool
mixedDomainsOverlap Domain a
a Domain b
b =
case forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
A.arithDomainData Domain a
a of
Maybe (Integer, Integer)
Nothing -> forall (w :: Nat). Domain w -> Bool
B.nonempty Domain b
b
Just (Integer
alo,Integer
_) ->
let (Integer
lomask,Integer
himask) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain b
b
brb :: Integer
brb = Integer -> Integer -> Integer -> Integer -> Integer
bitwiseRoundBetween (forall (w :: Nat). Domain w -> Integer
A.bvdMask Domain a
a) Integer
alo Integer
lomask Integer
himask
in forall (w :: Nat). Domain w -> Bool
B.nonempty Domain b
b Bool -> Bool -> Bool
&& (forall (w :: Nat). Domain w -> Integer -> Bool
A.member Domain a
a Integer
lomask Bool -> Bool -> Bool
|| forall (w :: Nat). Domain w -> Integer -> Bool
A.member Domain a
a Integer
himask Bool -> Bool -> Bool
|| forall (w :: Nat). Domain w -> Integer -> Bool
A.member Domain a
a Integer
brb)
domainsOverlap :: BVDomain w -> BVDomain w -> Bool
domainsOverlap :: forall (w :: Nat). BVDomain w -> BVDomain w -> Bool
domainsOverlap (BVDBitwise Domain w
a) (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> Domain w -> Bool
B.domainsOverlap Domain w
a Domain w
b
domainsOverlap (BVDArith Domain w
a) (BVDArith Domain w
b) = forall (w :: Nat). Domain w -> Domain w -> Bool
A.domainsOverlap Domain w
a Domain w
b
domainsOverlap (BVDArith Domain w
a) (BVDBitwise Domain w
b) = forall (a :: Nat) (b :: Nat). Domain a -> Domain b -> Bool
mixedDomainsOverlap Domain w
a Domain w
b
domainsOverlap (BVDBitwise Domain w
b) (BVDArith Domain w
a) = forall (a :: Nat) (b :: Nat). Domain a -> Domain b -> Bool
mixedDomainsOverlap Domain w
a Domain w
b
arithDomainLo :: A.Domain w -> Integer
arithDomainLo :: forall (w :: Nat). Domain w -> Integer
arithDomainLo Domain w
a =
case forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
A.arithDomainData Domain w
a of
Maybe (Integer, Integer)
Nothing -> Integer
0
Just (Integer
lo,Integer
_) -> Integer
lo
mixedCandidates :: A.Domain w -> B.Domain w -> [Integer]
mixedCandidates :: forall (w :: Nat). Domain w -> Domain w -> [Integer]
mixedCandidates Domain w
a Domain w
b =
case forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
A.arithDomainData Domain w
a of
Maybe (Integer, Integer)
Nothing -> [ Integer
lomask ]
Just (Integer
alo,Integer
_) -> [ Integer
lomask, Integer
himask, Integer -> Integer -> Integer -> Integer -> Integer
bitwiseRoundBetween (forall (w :: Nat). Domain w -> Integer
A.bvdMask Domain w
a) Integer
alo Integer
lomask Integer
himask ]
where
(Integer
lomask,Integer
himask) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b
overlapCandidates :: BVDomain w -> BVDomain w -> [Integer]
overlapCandidates :: forall (w :: Nat). BVDomain w -> BVDomain w -> [Integer]
overlapCandidates (BVDArith Domain w
a) (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> Domain w -> [Integer]
mixedCandidates Domain w
a Domain w
b
overlapCandidates (BVDBitwise Domain w
b) (BVDArith Domain w
a) = forall (w :: Nat). Domain w -> Domain w -> [Integer]
mixedCandidates Domain w
a Domain w
b
overlapCandidates (BVDArith Domain w
a) (BVDArith Domain w
b) = [ forall (w :: Nat). Domain w -> Integer
arithDomainLo Domain w
a, forall (w :: Nat). Domain w -> Integer
arithDomainLo Domain w
b ]
overlapCandidates (BVDBitwise Domain w
a) (BVDBitwise Domain w
b) = [ Integer
loa forall a. Bits a => a -> a -> a
.|. Integer
lob ]
where
(Integer
loa,Integer
_) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
a
(Integer
lob,Integer
_) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b
eq :: BVDomain w -> BVDomain w -> Maybe Bool
eq :: forall (w :: Nat). BVDomain w -> BVDomain w -> Maybe Bool
eq BVDomain w
a BVDomain w
b
| Just Integer
x <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a
, Just Integer
y <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b = forall a. a -> Maybe a
Just (Integer
x forall a. Eq a => a -> a -> Bool
== Integer
y)
| forall (w :: Nat). BVDomain w -> BVDomain w -> Bool
domainsOverlap BVDomain w
a BVDomain w
b forall a. Eq a => a -> a -> Bool
== Bool
False = forall a. a -> Maybe a
Just Bool
False
| Bool
otherwise = forall a. Maybe a
Nothing
slt :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> Maybe Bool
slt :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> Maybe Bool
slt NatRepr w
w BVDomain w
a BVDomain w
b = forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Maybe Bool
A.slt NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
b)
ult :: (1 <= w) => BVDomain w -> BVDomain w -> Maybe Bool
ult :: forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> Maybe Bool
ult BVDomain w
a BVDomain w
b = forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Maybe Bool
A.ult (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
b)
testBit ::
NatRepr w ->
BVDomain w ->
Natural ->
Maybe Bool
testBit :: forall (w :: Nat). NatRepr w -> BVDomain w -> Nat -> Maybe Bool
testBit NatRepr w
_w BVDomain w
a Nat
i = forall (w :: Nat). Domain w -> Nat -> Maybe Bool
B.testBit (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
a) Nat
i
ubounds :: BVDomain w -> (Integer, Integer)
ubounds :: forall (w :: Nat). BVDomain w -> (Integer, Integer)
ubounds BVDomain w
a = forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a)
sbounds :: (1 <= w) => NatRepr w -> BVDomain w -> (Integer, Integer)
sbounds :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> (Integer, Integer)
sbounds NatRepr w
w BVDomain w
a = forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> (Integer, Integer)
A.sbounds NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a)
isUltSumCommonEquiv :: BVDomain w -> BVDomain w -> BVDomain w -> Bool
isUltSumCommonEquiv :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w -> Bool
isUltSumCommonEquiv BVDomain w
a BVDomain w
b BVDomain w
c =
forall (w :: Nat). Domain w -> Domain w -> Domain w -> Bool
A.isUltSumCommonEquiv (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
b) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
c)
any :: (1 <= w) => NatRepr w -> BVDomain w
any :: forall (w :: Nat). (1 <= w) => NatRepr w -> BVDomain w
any NatRepr w
w = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat). NatRepr w -> Domain w
B.any NatRepr w
w)
singleton :: (HasCallStack, 1 <= w) => NatRepr w -> Integer -> BVDomain w
singleton :: forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> BVDomain w
singleton NatRepr w
w Integer
x = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
A.singleton NatRepr w
w Integer
x)
range :: NatRepr w -> Integer -> Integer -> BVDomain w
range :: forall (w :: Nat). NatRepr w -> Integer -> Integer -> BVDomain w
range NatRepr w
w Integer
al Integer
ah = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
A.range NatRepr w
w Integer
al Integer
ah)
fromAscEltList :: (1 <= w) => NatRepr w -> [Integer] -> BVDomain w
fromAscEltList :: forall (w :: Nat). (1 <= w) => NatRepr w -> [Integer] -> BVDomain w
fromAscEltList NatRepr w
w [Integer]
xs = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => NatRepr w -> [Integer] -> Domain w
A.fromAscEltList NatRepr w
w [Integer]
xs)
union :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w
union :: forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
union (BVDBitwise Domain w
a) (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union Domain w
a Domain w
b)
union (BVDArith Domain w
a) (BVDArith Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.union Domain w
a Domain w
b)
union (BVDBitwise Domain w
a) (BVDArith Domain w
b) = forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> BVDomain w
mixedUnion Domain w
b Domain w
a
union (BVDArith Domain w
a) (BVDBitwise Domain w
b) = forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> BVDomain w
mixedUnion Domain w
a Domain w
b
mixedUnion :: (1 <= w) => A.Domain w -> B.Domain w -> BVDomain w
mixedUnion :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> BVDomain w
mixedUnion Domain w
a Domain w
b
| Just Integer
_ <- forall (w :: Nat). Domain w -> Maybe Integer
A.asSingleton Domain w
a = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union (forall (w :: Nat). Domain w -> Domain w
arithToBitwiseDomain Domain w
a) Domain w
b)
| Bool
otherwise = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.union Domain w
a (forall (w :: Nat). Domain w -> Domain w
bitwiseToArithDomain Domain w
b))
concat :: NatRepr u -> BVDomain u -> NatRepr v -> BVDomain v -> BVDomain (u + v)
concat :: forall (u :: Nat) (v :: Nat).
NatRepr u
-> BVDomain u -> NatRepr v -> BVDomain v -> BVDomain (u + v)
concat NatRepr u
u (BVDArith Domain u
a) NatRepr v
v (BVDArith Domain v
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (u :: Nat) (v :: Nat).
NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
A.concat NatRepr u
u Domain u
a NatRepr v
v Domain v
b)
concat NatRepr u
u (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain u
a) NatRepr v
v (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain v
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (u :: Nat) (v :: Nat).
NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
B.concat NatRepr u
u Domain u
a NatRepr v
v Domain v
b)
select ::
(1 <= n, i + n <= w) =>
NatRepr i ->
NatRepr n ->
BVDomain w -> BVDomain n
select :: forall (n :: Nat) (i :: Nat) (w :: Nat).
(1 <= n, (i + n) <= w) =>
NatRepr i -> NatRepr n -> BVDomain w -> BVDomain n
select NatRepr i
i NatRepr n
n (BVDArith Domain w
a) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (n :: Nat) (i :: Nat) (w :: Nat).
(1 <= n, (i + n) <= w) =>
NatRepr i -> NatRepr n -> Domain w -> Domain n
A.select NatRepr i
i NatRepr n
n Domain w
a)
select NatRepr i
i NatRepr n
n (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (n :: Nat) (i :: Nat) (w :: Nat).
(1 <= n, (i + n) <= w) =>
NatRepr i -> NatRepr n -> Domain w -> Domain n
B.select NatRepr i
i NatRepr n
n Domain w
b)
zext :: (1 <= w, w+1 <= u) => BVDomain w -> NatRepr u -> BVDomain u
zext :: forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
BVDomain w -> NatRepr u -> BVDomain u
zext (BVDArith Domain w
a) NatRepr u
u = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
Domain w -> NatRepr u -> Domain u
A.zext Domain w
a NatRepr u
u)
zext (BVDBitwise Domain w
b) NatRepr u
u = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
Domain w -> NatRepr u -> Domain u
B.zext Domain w
b NatRepr u
u)
sext ::
forall w u. (1 <= w, w + 1 <= u) =>
NatRepr w ->
BVDomain w ->
NatRepr u ->
BVDomain u
sext :: forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> BVDomain w -> NatRepr u -> BVDomain u
sext NatRepr w
w (BVDArith Domain w
a) NatRepr u
u = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> Domain w -> NatRepr u -> Domain u
A.sext NatRepr w
w Domain w
a NatRepr u
u)
sext NatRepr w
w (BVDBitwise Domain w
b) NatRepr u
u = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> Domain w -> NatRepr u -> Domain u
B.sext NatRepr w
w Domain w
b NatRepr u
u)
shiftBound :: Integer
shiftBound :: Integer
shiftBound = Integer
16
shl :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
shl :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
shl NatRepr w
w (BVDBitwise Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b)
| Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
hi' Bool -> Bool -> Bool
&& Integer
hi' forall a. Num a => a -> a -> a
- Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
shiftBound =
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union [ forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
B.shl NatRepr w
w Domain w
a Integer
y | Integer
y <- [Integer
lo .. Integer
hi'] ]
where
(Integer
lo, Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds Domain w
b
hi' :: Integer
hi' = forall a. Ord a => a -> a -> a
max Integer
hi (forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w)
shl NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
A.shl NatRepr w
w Domain w
a Domain w
b)
lshr :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
lshr :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
lshr NatRepr w
w (BVDBitwise Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b)
| Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
hi' Bool -> Bool -> Bool
&& Integer
hi' forall a. Num a => a -> a -> a
- Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
shiftBound =
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union [ forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
B.lshr NatRepr w
w Domain w
a Integer
y | Integer
y <- [Integer
lo .. Integer
hi'] ]
where
(Integer
lo, Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds Domain w
b
hi' :: Integer
hi' = forall a. Ord a => a -> a -> a
max Integer
hi (forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w)
lshr NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
A.lshr NatRepr w
w Domain w
a Domain w
b)
ashr :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
ashr :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
ashr NatRepr w
w (BVDBitwise Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b)
| Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
hi' Bool -> Bool -> Bool
&& Integer
hi' forall a. Num a => a -> a -> a
- Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
shiftBound =
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union [ forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Integer -> Domain w
B.ashr NatRepr w
w Domain w
a Integer
y | Integer
y <- [Integer
lo .. Integer
hi'] ]
where
(Integer
lo, Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds Domain w
b
hi' :: Integer
hi' = forall a. Ord a => a -> a -> a
max Integer
hi (forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w)
ashr NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
A.ashr NatRepr w
w Domain w
a Domain w
b)
rol :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
rol :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
rol NatRepr w
_w a :: BVDomain w
a@(forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton -> Just Integer
x) BVDomain w
_
| Integer
x forall a. Eq a => a -> a -> Bool
== Integer
0 = BVDomain w
a
| Integer
x forall a. Eq a => a -> a -> Bool
== forall (w :: Nat). BVDomain w -> Integer
bvdMask BVDomain w
a = BVDomain w
a
rol NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) =
if (Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
hi Bool -> Bool -> Bool
&& Integer
hi forall a. Num a => a -> a -> a
- Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
shiftBound) then
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union [ forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
B.rol NatRepr w
w Domain w
a Integer
y | Integer
y <- [Integer
lo .. Integer
hi] ]
else
forall (w :: Nat). (1 <= w) => NatRepr w -> BVDomain w
any NatRepr w
w
where
(Integer
lo, Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.urem Domain w
b (forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
A.singleton NatRepr w
w (forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w)))
ror :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
ror :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
ror NatRepr w
_w a :: BVDomain w
a@(forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton -> Just Integer
x) BVDomain w
_
| Integer
x forall a. Eq a => a -> a -> Bool
== Integer
0 = BVDomain w
a
| Integer
x forall a. Eq a => a -> a -> Bool
== forall (w :: Nat). BVDomain w -> Integer
bvdMask BVDomain w
a = BVDomain w
a
ror NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) =
if (Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
hi Bool -> Bool -> Bool
&& Integer
hi forall a. Num a => a -> a -> a
- Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
shiftBound) then
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union [ forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
B.ror NatRepr w
w Domain w
a Integer
y | Integer
y <- [Integer
lo .. Integer
hi] ]
else
forall (w :: Nat). (1 <= w) => NatRepr w -> BVDomain w
any NatRepr w
w
where
(Integer
lo, Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.urem Domain w
b (forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
A.singleton NatRepr w
w (forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w)))
add :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w
add :: forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
add BVDomain w
a BVDomain w
b
| Just Integer
0 <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a = BVDomain w
b
| Just Integer
0 <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b = BVDomain w
a
| Bool
otherwise = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.add (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
b))
negate :: (1 <= w) => BVDomain w -> BVDomain w
negate :: forall (w :: Nat). (1 <= w) => BVDomain w -> BVDomain w
negate (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => Domain w -> Domain w
A.negate Domain w
a)
scale :: (1 <= w) => Integer -> BVDomain w -> BVDomain w
scale :: forall (w :: Nat). (1 <= w) => Integer -> BVDomain w -> BVDomain w
scale Integer
k BVDomain w
a
| Integer
k forall a. Eq a => a -> a -> Bool
== Integer
1 = BVDomain w
a
| Bool
otherwise = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => Integer -> Domain w -> Domain w
A.scale Integer
k (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a))
mul :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w
mul :: forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
mul BVDomain w
a BVDomain w
b
| Just Integer
1 <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a = BVDomain w
b
| Just Integer
1 <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b = BVDomain w
a
| Bool
otherwise = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.mul (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
b))
udiv :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w
udiv :: forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
udiv (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.udiv Domain w
a Domain w
b)
urem :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w
urem :: forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
urem (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.urem Domain w
a Domain w
b)
sdiv :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
sdiv :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
sdiv NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
A.sdiv NatRepr w
w Domain w
a Domain w
b)
srem :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
srem :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
srem NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
A.srem NatRepr w
w Domain w
a Domain w
b)
not :: BVDomain w -> BVDomain w
not :: forall (w :: Nat). BVDomain w -> BVDomain w
not (BVDArith Domain w
a) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). Domain w -> Domain w
A.not Domain w
a)
not (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat). Domain w -> Domain w
B.not Domain w
b)
and :: BVDomain w -> BVDomain w -> BVDomain w
and :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
and BVDomain w
a BVDomain w
b
| Just Integer
x <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a, Integer
x forall a. Eq a => a -> a -> Bool
== Integer
mask = BVDomain w
b
| Just Integer
x <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b, Integer
x forall a. Eq a => a -> a -> Bool
== Integer
mask = BVDomain w
a
| Bool
otherwise = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat). Domain w -> Domain w -> Domain w
B.and (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
b))
where
mask :: Integer
mask = forall (w :: Nat). BVDomain w -> Integer
bvdMask BVDomain w
a
or :: BVDomain w -> BVDomain w -> BVDomain w
or :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
or BVDomain w
a BVDomain w
b
| Just Integer
0 <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a = BVDomain w
b
| Just Integer
0 <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b = BVDomain w
a
| Bool
otherwise = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat). Domain w -> Domain w -> Domain w
B.or (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
b))
xor :: BVDomain w -> BVDomain w -> BVDomain w
xor :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
xor BVDomain w
a BVDomain w
b
| Just Integer
0 <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a = BVDomain w
b
| Just Integer
0 <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b = BVDomain w
a
| Bool
otherwise = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat). Domain w -> Domain w -> Domain w
B.xor (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
b))
popcnt :: NatRepr w -> BVDomain w -> BVDomain w
popcnt :: forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
popcnt NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
A.range NatRepr w
w Integer
lo Integer
hi)
where
(Integer
bitlo, Integer
bithi) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b
lo :: Integer
lo = forall a. Integral a => a -> Integer
toInteger (forall a. Bits a => a -> Int
Bits.popCount Integer
bitlo)
hi :: Integer
hi = forall a. Integral a => a -> Integer
toInteger (forall a. Bits a => a -> Int
Bits.popCount Integer
bithi)
clz :: NatRepr w -> BVDomain w -> BVDomain w
clz :: forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
clz NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
A.range NatRepr w
w Integer
lo Integer
hi)
where
(Integer
bitlo, Integer
bithi) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b
lo :: Integer
lo = forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.clz NatRepr w
w Integer
bithi
hi :: Integer
hi = forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.clz NatRepr w
w Integer
bitlo
ctz :: NatRepr w -> BVDomain w -> BVDomain w
ctz :: forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
ctz NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
A.range NatRepr w
w Integer
lo Integer
hi)
where
(Integer
bitlo, Integer
bithi) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b
lo :: Integer
lo = forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.ctz NatRepr w
w Integer
bithi
hi :: Integer
hi = forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.ctz NatRepr w
w Integer
bitlo
pmember :: NatRepr n -> BVDomain n -> Integer -> Bool
pmember :: forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n BVDomain n
a Integer
x = forall (w :: Nat). NatRepr w -> BVDomain w -> Bool
proper NatRepr n
n BVDomain n
a Bool -> Bool -> Bool
&& forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x
correct_arithToBitwise :: NatRepr n -> (A.Domain n, Integer) -> Property
correct_arithToBitwise :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
correct_arithToBitwise NatRepr n
n (Domain n
a,Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
A.member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
B.pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w
arithToBitwiseDomain Domain n
a) Integer
x
correct_bitwiseToArith :: NatRepr n -> (B.Domain n, Integer) -> Property
correct_bitwiseToArith :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
correct_bitwiseToArith NatRepr n
n (Domain n
b,Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
B.member Domain n
b Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
A.pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w
bitwiseToArithDomain Domain n
b) Integer
x
correct_bitwiseToXorDomain :: NatRepr n -> (B.Domain n, Integer) -> Property
correct_bitwiseToXorDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
correct_bitwiseToXorDomain NatRepr n
n (Domain n
b,Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
B.member Domain n
b Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
X.pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w
bitwiseToXorDomain Domain n
b) Integer
x
correct_arithToXorDomain :: NatRepr n -> (A.Domain n, Integer) -> Property
correct_arithToXorDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
correct_arithToXorDomain NatRepr n
n (Domain n
a,Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
A.member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
X.pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w
arithToXorDomain Domain n
a) Integer
x
correct_xorToBitwiseDomain :: NatRepr n -> (X.Domain n, Integer) -> Property
correct_xorToBitwiseDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
correct_xorToBitwiseDomain NatRepr n
n (Domain n
a,Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
X.member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
B.pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w
xorToBitwiseDomain Domain n
a) Integer
x
correct_asXorDomain :: NatRepr n -> (BVDomain n, Integer) -> Property
correct_asXorDomain :: forall (n :: Nat). NatRepr n -> (BVDomain n, Integer) -> Property
correct_asXorDomain NatRepr n
n (BVDomain n
a, Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
X.pmember NatRepr n
n (forall (w :: Nat). BVDomain w -> Domain w
asXorDomain BVDomain n
a) Integer
x
correct_fromXorDomain :: NatRepr n -> (X.Domain n, Integer) -> Property
correct_fromXorDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
correct_fromXorDomain NatRepr n
n (Domain n
a, Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
X.member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). Domain w -> BVDomain w
fromXorDomain Domain n
a) Integer
x
correct_bra1 :: NatRepr n -> Integer -> Integer -> Property
correct_bra1 :: forall (n :: Nat). NatRepr n -> Integer -> Integer -> Property
correct_bra1 NatRepr n
n Integer
x Integer
lomask = Integer
lomask forall a. Ord a => a -> a -> Bool
<= Integer
x forall t. Verifiable t => Bool -> t -> Property
==> (Integer
x forall a. Ord a => a -> a -> Bool
<= Integer
q Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
lomask Integer
q)
where
q :: Integer
q = Integer -> Integer -> Integer -> Integer
bitwiseRoundAbove (forall (n :: Nat). NatRepr n -> Integer
maxUnsigned NatRepr n
n) Integer
x Integer
lomask
correct_bra2 :: NatRepr n -> Integer -> Integer -> Integer -> Property
correct_bra2 :: forall (n :: Nat).
NatRepr n -> Integer -> Integer -> Integer -> Property
correct_bra2 NatRepr n
n Integer
x Integer
lomask Integer
q' = (Integer
x forall a. Ord a => a -> a -> Bool
<= Integer
q' Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
lomask Integer
q') forall t. Verifiable t => Bool -> t -> Property
==> Integer
q forall a. Ord a => a -> a -> Bool
<= Integer
q'
where
q :: Integer
q = Integer -> Integer -> Integer -> Integer
bitwiseRoundAbove (forall (n :: Nat). NatRepr n -> Integer
maxUnsigned NatRepr n
n) Integer
x Integer
lomask
correct_brb1 :: NatRepr n -> Integer -> Integer -> Integer -> Property
correct_brb1 :: forall (n :: Nat).
NatRepr n -> Integer -> Integer -> Integer -> Property
correct_brb1 NatRepr n
n Integer
x Integer
lomask Integer
himask =
(Integer -> Integer -> Bool
B.bitle Integer
lomask Integer
himask Bool -> Bool -> Bool
&& Integer
lomask forall a. Ord a => a -> a -> Bool
<= Integer
x Bool -> Bool -> Bool
&& Integer
x forall a. Ord a => a -> a -> Bool
<= Integer
himask) forall t. Verifiable t => Bool -> t -> Property
==>
(Integer
x forall a. Ord a => a -> a -> Bool
<= Integer
q Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
lomask Integer
q Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
q Integer
himask)
where
q :: Integer
q = Integer -> Integer -> Integer -> Integer -> Integer
bitwiseRoundBetween (forall (n :: Nat). NatRepr n -> Integer
maxUnsigned NatRepr n
n) Integer
x Integer
lomask Integer
himask
correct_brb2 :: NatRepr n -> Integer -> Integer -> Integer -> Integer -> Property
correct_brb2 :: forall (n :: Nat).
NatRepr n -> Integer -> Integer -> Integer -> Integer -> Property
correct_brb2 NatRepr n
n Integer
x Integer
lomask Integer
himask Integer
q' =
(Integer
x forall a. Ord a => a -> a -> Bool
<= Integer
q' Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
lomask Integer
q' Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
q' Integer
himask) forall t. Verifiable t => Bool -> t -> Property
==> Integer
q forall a. Ord a => a -> a -> Bool
<= Integer
q'
where
q :: Integer
q = Integer -> Integer -> Integer -> Integer -> Integer
bitwiseRoundBetween (forall (n :: Nat). NatRepr n -> Integer
maxUnsigned NatRepr n
n) Integer
x Integer
lomask Integer
himask
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 -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). (1 <= w) => NatRepr w -> BVDomain w
any NatRepr n
n) Integer
x)
correct_ubounds :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_ubounds :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (BVDomain n, Integer) -> Property
correct_ubounds NatRepr n
n (BVDomain n
a,Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
x' Bool -> Bool -> Bool
&& Integer
x' forall a. Ord a => a -> a -> Bool
<= Integer
hi
where
x' :: Integer
x' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x
(Integer
lo,Integer
hi) = forall (w :: Nat). BVDomain w -> (Integer, Integer)
ubounds BVDomain n
a
correct_sbounds :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_sbounds :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (BVDomain n, Integer) -> Property
correct_sbounds NatRepr n
n (BVDomain n
a,Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
x' Bool -> Bool -> Bool
&& Integer
x' forall a. Ord a => a -> a -> Bool
<= Integer
hi
where
x' :: Integer
x' = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x
(Integer
lo,Integer
hi) = forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> (Integer, Integer)
sbounds NatRepr n
n BVDomain n
a
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 (w :: Nat). BVDomain w -> Integer -> Bool
member (forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> BVDomain 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 :: BVDomain n -> BVDomain n -> Integer -> Property
correct_overlap :: forall (n :: Nat). BVDomain n -> BVDomain n -> Integer -> Property
correct_overlap BVDomain n
a BVDomain n
b Integer
x =
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Bool -> Bool
&& forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> BVDomain w -> Bool
domainsOverlap BVDomain n
a BVDomain n
b
precise_overlap :: BVDomain n -> BVDomain n -> Property
precise_overlap :: forall (n :: Nat). BVDomain n -> BVDomain n -> Property
precise_overlap BVDomain n
a BVDomain n
b =
forall (w :: Nat). BVDomain w -> BVDomain w -> Bool
domainsOverlap BVDomain n
a BVDomain n
b forall t. Verifiable t => Bool -> t -> Property
==> forall (t :: Type -> Type). Foldable t => t Bool -> Bool
List.or [ forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Bool -> Bool
&& forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
x | Integer
x <- forall (w :: Nat). BVDomain w -> BVDomain w -> [Integer]
overlapCandidates BVDomain n
a BVDomain n
b ]
correct_union :: (1 <= n) => NatRepr n -> BVDomain n -> BVDomain n -> Integer -> Property
correct_union :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> BVDomain n -> BVDomain n -> Integer -> Property
correct_union NatRepr n
n BVDomain n
a BVDomain n
b Integer
x =
(forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Bool -> Bool
|| forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
x) forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
union BVDomain n
a BVDomain n
b) Integer
x
correct_zero_ext :: (1 <= w, w+1 <= u) => NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property
correct_zero_ext :: forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property
correct_zero_ext NatRepr w
w BVDomain w
a NatRepr u
u Integer
x = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain w
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr u
u (forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
BVDomain w -> NatRepr u -> BVDomain u
zext BVDomain 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 -> BVDomain w -> NatRepr u -> Integer -> Property
correct_sign_ext :: forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property
correct_sign_ext NatRepr w
w BVDomain w
a NatRepr u
u Integer
x = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain w
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr u
u (forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> BVDomain w -> NatRepr u -> BVDomain u
sext NatRepr w
w BVDomain 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 -> (BVDomain m,Integer) -> NatRepr n -> (BVDomain n,Integer) -> Property
correct_concat :: forall (m :: Nat) (n :: Nat).
NatRepr m
-> (BVDomain m, Integer)
-> NatRepr n
-> (BVDomain n, Integer)
-> Property
correct_concat NatRepr m
m (BVDomain m
a,Integer
x) NatRepr n
n (BVDomain n
b,Integer
y) =
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain m
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain 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
-> BVDomain u -> NatRepr v -> BVDomain v -> BVDomain (u + v)
concat NatRepr m
m BVDomain m
a NatRepr n
n BVDomain n
b) Integer
z
where
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_select :: (1 <= n, i + n <= w) =>
NatRepr i -> NatRepr n -> (BVDomain w, Integer) -> Property
correct_select :: forall (n :: Nat) (i :: Nat) (w :: Nat).
(1 <= n, (i + n) <= w) =>
NatRepr i -> NatRepr n -> (BVDomain w, Integer) -> Property
correct_select NatRepr i
i NatRepr n
n (BVDomain w
a, Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain w
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (n :: Nat) (i :: Nat) (w :: Nat).
(1 <= n, (i + n) <= w) =>
NatRepr i -> NatRepr n -> BVDomain w -> BVDomain n
select NatRepr i
i NatRepr n
n BVDomain 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). BVDomain w -> Integer
bvdMask BVDomain w
a) forall a. Bits a => a -> Int -> a
`shiftR` (forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr i
i))
correct_add :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_add :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_add NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
add BVDomain n
a BVDomain n
b) (Integer
x forall a. Num a => a -> a -> a
+ Integer
y)
correct_neg :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_neg :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (BVDomain n, Integer) -> Property
correct_neg NatRepr n
n (BVDomain n
a,Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). (1 <= w) => BVDomain w -> BVDomain w
negate BVDomain n
a) (forall a. Num a => a -> a
Prelude.negate Integer
x)
correct_mul :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_mul :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_mul NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
mul BVDomain n
a BVDomain n
b) (Integer
x forall a. Num a => a -> a -> a
* Integer
y)
correct_scale :: (1 <= n) => NatRepr n -> Integer -> (BVDomain n, Integer) -> Property
correct_scale :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Integer -> (BVDomain n, Integer) -> Property
correct_scale NatRepr n
n Integer
k (BVDomain n
a,Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). (1 <= w) => Integer -> BVDomain w -> BVDomain w
scale Integer
k' BVDomain n
a) (Integer
k' forall a. Num a => a -> a -> a
* Integer
x)
where
k' :: Integer
k' = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
k
correct_udiv :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_udiv :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_udiv NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y' forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' forall a. Eq a => a -> a -> Bool
/= Integer
0 forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
udiv BVDomain n
a BVDomain n
b) (Integer
x' forall a. Integral a => a -> a -> a
`quot` 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_urem :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_urem :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_urem NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y' forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' forall a. Eq a => a -> a -> Bool
/= Integer
0 forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
urem BVDomain n
a BVDomain n
b) (Integer
x' forall a. Integral a => a -> a -> a
`rem` 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_sdiv :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_sdiv :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_sdiv NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) =
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y' forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' forall a. Eq a => a -> a -> Bool
/= Integer
0 forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
sdiv NatRepr n
n BVDomain n
a BVDomain n
b) (Integer
x' forall a. Integral a => a -> a -> a
`quot` Integer
y')
where
x' :: Integer
x' = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x
y' :: Integer
y' = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y
correct_srem :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_srem :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_srem NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) =
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y' forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' forall a. Eq a => a -> a -> Bool
/= Integer
0 forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
srem NatRepr n
n BVDomain n
a BVDomain n
b) (Integer
x' forall a. Integral a => a -> a -> a
`rem` Integer
y')
where
x' :: Integer
x' = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x
y' :: Integer
y' = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y
correct_shl :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_shl :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_shl NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
shl NatRepr n
n BVDomain n
a BVDomain n
b) 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 (n :: Nat). NatRepr n -> Integer
intValue NatRepr n
n) Integer
y)
correct_lshr :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_lshr :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_lshr NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
lshr NatRepr n
n BVDomain n
a BVDomain n
b) 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 (n :: Nat). NatRepr n -> Integer
intValue NatRepr n
n) Integer
y)
correct_ashr :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_ashr :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_ashr NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
ashr NatRepr n
n BVDomain n
a BVDomain n
b) 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 (n :: Nat). NatRepr n -> Integer
intValue NatRepr n
n) Integer
y)
correct_rol :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_rol :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_rol NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
rol NatRepr n
n BVDomain n
a BVDomain n
b) (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateLeft NatRepr n
n Integer
x Integer
y)
correct_ror :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_ror :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_ror NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
ror NatRepr n
n BVDomain n
a BVDomain n
b) (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateRight NatRepr n
n Integer
x Integer
y)
correct_eq :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_eq :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_eq NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) =
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==>
case forall (w :: Nat). BVDomain w -> BVDomain w -> Maybe Bool
eq BVDomain n
a BVDomain 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_ult :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_ult :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_ult NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) =
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==>
case forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> Maybe Bool
ult BVDomain n
a BVDomain n
b of
Just Bool
True -> forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x forall a. Ord 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. Ord a => a -> a -> Bool
>= forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y
Maybe Bool
Nothing -> Bool
True
correct_slt :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_slt :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_slt NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) =
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==>
case forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> Maybe Bool
slt NatRepr n
n BVDomain n
a BVDomain n
b of
Just Bool
True -> forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x forall a. Ord a => a -> a -> Bool
< forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y
Just Bool
False -> forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x forall a. Ord a => a -> a -> Bool
>= forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y
Maybe Bool
Nothing -> Bool
True
correct_not :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_not :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (BVDomain n, Integer) -> Property
correct_not NatRepr n
n (BVDomain n
a,Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). BVDomain w -> BVDomain w
not BVDomain n
a) (forall a. Bits a => a -> a
complement Integer
x)
correct_and :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_and :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_and NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
and BVDomain n
a BVDomain n
b) (Integer
x forall a. Bits a => a -> a -> a
.&. Integer
y)
correct_or :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_or :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_or NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
or BVDomain n
a BVDomain n
b) (Integer
x forall a. Bits a => a -> a -> a
.|. Integer
y)
correct_xor :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_xor :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_xor NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
xor BVDomain n
a BVDomain n
b) (Integer
x forall a. Bits a => a -> a -> a
`Bits.xor` Integer
y)
correct_testBit :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Natural -> Property
correct_testBit :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (BVDomain n, Integer) -> Nat -> Property
correct_testBit NatRepr n
n (BVDomain 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). NatRepr w -> BVDomain w -> Nat -> Maybe Bool
testBit NatRepr n
n BVDomain 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
correct_popcnt :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_popcnt :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (BVDomain n, Integer) -> Property
correct_popcnt NatRepr n
n (BVDomain n
a,Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
popcnt NatRepr n
n BVDomain n
a) (forall a. Integral a => a -> Integer
toInteger (forall a. Bits a => a -> Int
Bits.popCount Integer
x))
correct_ctz :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_ctz :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (BVDomain n, Integer) -> Property
correct_ctz NatRepr n
n (BVDomain n
a,Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
ctz NatRepr n
n BVDomain n
a) (forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.ctz NatRepr n
n Integer
x)
correct_clz :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_clz :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (BVDomain n, Integer) -> Property
correct_clz NatRepr n
n (BVDomain n
a,Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
clz NatRepr n
n BVDomain n
a) (forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.clz NatRepr n
n Integer
x)