{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module What4.Utils.BVDomain.Arith
( Domain(..)
, proper
, bvdMask
, member
, pmember
, interval
, size
, asSingleton
, ubounds
, sbounds
, eq
, slt
, ult
, isUltSumCommonEquiv
, domainsOverlap
, arithDomainData
, bitbounds
, unknowns
, fillright
, any
, singleton
, range
, fromAscEltList
, union
, concat
, select
, zext
, sext
, shl
, lshr
, ashr
, add
, negate
, scale
, mul
, udiv
, urem
, sdiv
, srem
, What4.Utils.BVDomain.Arith.not
, genDomain
, genElement
, genPair
, correct_any
, correct_ubounds
, correct_sbounds
, correct_singleton
, correct_overlap
, correct_union
, correct_zero_ext
, correct_sign_ext
, correct_concat
, correct_shrink
, correct_trunc
, correct_select
, correct_add
, correct_neg
, correct_mul
, correct_scale
, correct_scale_eq
, correct_udiv
, correct_urem
, correct_sdivRange
, correct_sdiv
, correct_srem
, correct_not
, correct_shl
, correct_lshr
, correct_ashr
, correct_eq
, correct_ult
, correct_slt
, correct_isUltSumCommonEquiv
, correct_unknowns
, correct_bitbounds
) where
import qualified Data.Bits as Bits
import Data.Bits hiding (testBit, xor)
import Data.Parameterized.NatRepr
import GHC.TypeNats
import GHC.Stack
import qualified Prelude
import Prelude hiding (any, concat, negate, and, or, not)
import Test.Verification ( Property, property, (==>), Gen, chooseInteger )
data Domain (w :: Nat)
= BVDAny !Integer
| BVDInterval !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
sameDomain :: Domain w -> Domain w -> Bool
sameDomain :: forall (w :: Nat). Domain w -> Domain w -> Bool
sameDomain (BVDAny Integer
_) (BVDAny Integer
_) = Bool
True
sameDomain (BVDInterval Integer
_ Integer
x Integer
w) (BVDInterval Integer
_ Integer
x' Integer
w') = Integer
x forall a. Eq a => a -> a -> Bool
== Integer
x' Bool -> Bool -> Bool
&& Integer
w forall a. Eq a => a -> a -> Bool
== Integer
w'
sameDomain Domain w
_ Domain w
_ = Bool
False
size :: Domain w -> Integer
size :: forall (w :: Nat). Domain w -> Integer
size (BVDAny Integer
mask) = Integer
mask forall a. Num a => a -> a -> a
+ Integer
1
size (BVDInterval Integer
_ Integer
_ Integer
sz) = Integer
sz forall a. Num a => a -> a -> a
+ Integer
1
member :: Domain w -> Integer -> Bool
member :: forall (w :: Nat). Domain w -> Integer -> Bool
member (BVDAny Integer
_) Integer
_ = Bool
True
member (BVDInterval Integer
mask Integer
lo Integer
sz) Integer
x = ((Integer
x' forall a. Num a => a -> a -> a
- Integer
lo) forall a. Bits a => a -> a -> a
.&. Integer
mask) forall a. Ord a => a -> a -> Bool
<= Integer
sz
where x' :: Integer
x' = Integer
x forall a. Bits a => a -> a -> a
.&. Integer
mask
proper :: NatRepr w -> Domain w -> Bool
proper :: forall (w :: Nat). NatRepr w -> Domain w -> Bool
proper NatRepr w
w (BVDAny Integer
mask) = Integer
mask forall a. Eq a => a -> a -> Bool
== forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w
proper NatRepr w
w (BVDInterval Integer
mask Integer
lo Integer
sz) =
Integer
mask forall a. Eq a => a -> a -> Bool
== forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w Bool -> Bool -> Bool
&&
Integer
lo forall a. Bits a => a -> a -> a
.|. Integer
mask forall a. Eq a => a -> a -> Bool
== Integer
mask Bool -> Bool -> Bool
&&
Integer
sz forall a. Bits a => a -> a -> a
.|. Integer
mask forall a. Eq a => a -> a -> Bool
== Integer
mask Bool -> Bool -> Bool
&&
Integer
sz forall a. Ord a => a -> a -> Bool
< Integer
mask
bvdMask :: Domain w -> Integer
bvdMask :: forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
x =
case Domain w
x of
BVDAny Integer
mask -> Integer
mask
BVDInterval 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
sz <- (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
sz
genElement :: Domain w -> Gen Integer
genElement :: forall (w :: Nat). Domain w -> Gen Integer
genElement (BVDAny Integer
mask) = (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, Integer
mask)
genElement (BVDInterval Integer
mask Integer
lo Integer
sz) =
do Integer
x <- (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, Integer
sz)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((Integer
xforall a. Num a => a -> a -> a
+Integer
lo) forall a. Bits a => a -> a -> a
.&. Integer
mask)
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)
halfRange :: (1 <= w) => NatRepr w -> Integer
halfRange :: forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
halfRange NatRepr w
w = forall a. Bits a => Int -> a
bit (forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr w
w forall a. Num a => a -> a -> a
- Int
1)
asSingleton :: Domain w -> Maybe Integer
asSingleton :: forall (w :: Nat). Domain w -> Maybe Integer
asSingleton Domain w
x =
case Domain w
x of
BVDAny Integer
_ -> forall a. Maybe a
Nothing
BVDInterval Integer
_ Integer
xl Integer
xd
| Integer
xd forall a. Eq a => a -> a -> Bool
== Integer
0 -> forall a. a -> Maybe a
Just Integer
xl
| Bool
otherwise -> forall a. Maybe a
Nothing
isSingletonZero :: Domain w -> Bool
isSingletonZero :: forall (w :: Nat). Domain w -> Bool
isSingletonZero Domain w
x =
case Domain w
x of
BVDInterval Integer
_ Integer
0 Integer
0 -> Bool
True
Domain w
_ -> Bool
False
isBVDAny :: Domain w -> Bool
isBVDAny :: forall (w :: Nat). Domain w -> Bool
isBVDAny Domain w
x =
case Domain w
x of
BVDAny {} -> Bool
True
BVDInterval {} -> Bool
False
ubounds :: Domain w -> (Integer, Integer)
ubounds :: forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
a =
case Domain w
a of
BVDAny Integer
mask -> (Integer
0, Integer
mask)
BVDInterval Integer
mask Integer
al Integer
aw
| Integer
ah forall a. Ord a => a -> a -> Bool
> Integer
mask -> (Integer
0, Integer
mask)
| Bool
otherwise -> (Integer
al, Integer
ah)
where ah :: Integer
ah = Integer
al forall a. Num a => a -> a -> a
+ Integer
aw
sbounds :: (1 <= w) => NatRepr w -> Domain w -> (Integer, Integer)
sbounds :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> (Integer, Integer)
sbounds NatRepr w
w Domain w
a = (Integer
lo forall a. Num a => a -> a -> a
- Integer
delta, Integer
hi forall a. Num a => a -> a -> a
- Integer
delta)
where
delta :: Integer
delta = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
halfRange NatRepr w
w
(Integer
lo, Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
add Domain w
a (forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDInterval (forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a) Integer
delta Integer
0))
arithDomainData :: Domain w -> Maybe (Integer, Integer)
arithDomainData :: forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
arithDomainData (BVDAny Integer
_) = forall a. Maybe a
Nothing
arithDomainData (BVDInterval Integer
_ Integer
al Integer
aw) = forall a. a -> Maybe a
Just (Integer
al, Integer
aw)
domainsOverlap :: Domain w -> Domain w -> Bool
domainsOverlap :: forall (w :: Nat). Domain w -> Domain w -> Bool
domainsOverlap Domain w
a Domain w
b =
case Domain w
a of
BVDAny Integer
_ -> Bool
True
BVDInterval Integer
_ Integer
al Integer
aw ->
case Domain w
b of
BVDAny Integer
_ -> Bool
True
BVDInterval Integer
mask Integer
bl Integer
bw ->
Integer
diff forall a. Ord a => a -> a -> Bool
<= Integer
bw Bool -> Bool -> Bool
|| Integer
diff forall a. Num a => a -> a -> a
+ Integer
aw forall a. Ord a => a -> a -> Bool
> Integer
mask
where diff :: Integer
diff = (Integer
al forall a. Num a => a -> a -> a
- Integer
bl) forall a. Bits a => a -> a -> a
.&. Integer
mask
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)
| forall (w :: Nat). Domain w -> Domain w -> Bool
domainsOverlap Domain w
a Domain 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 -> Domain w -> Domain w -> Maybe Bool
slt :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Maybe Bool
slt NatRepr w
w Domain w
a Domain w
b
| Integer
a_max forall a. Ord a => a -> a -> Bool
< Integer
b_min = forall a. a -> Maybe a
Just Bool
True
| Integer
a_min forall a. Ord a => a -> a -> Bool
>= Integer
b_max = forall a. a -> Maybe a
Just Bool
False
| Bool
otherwise = forall a. Maybe a
Nothing
where
(Integer
a_min, Integer
a_max) = forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> (Integer, Integer)
sbounds NatRepr w
w Domain w
a
(Integer
b_min, Integer
b_max) = forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> (Integer, Integer)
sbounds NatRepr w
w Domain w
b
ult :: (1 <= w) => Domain w -> Domain w -> Maybe Bool
ult :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Maybe Bool
ult Domain w
a Domain w
b
| Integer
a_max forall a. Ord a => a -> a -> Bool
< Integer
b_min = forall a. a -> Maybe a
Just Bool
True
| Integer
a_min forall a. Ord a => a -> a -> Bool
>= Integer
b_max = forall a. a -> Maybe a
Just Bool
False
| Bool
otherwise = forall a. Maybe a
Nothing
where
(Integer
a_min, Integer
a_max) = forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
a
(Integer
b_min, Integer
b_max) = forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
b
isUltSumCommonEquiv :: Domain w -> Domain w -> Domain w -> Bool
isUltSumCommonEquiv :: forall (w :: Nat). Domain w -> Domain w -> Domain w -> Bool
isUltSumCommonEquiv Domain w
a Domain w
b Domain w
c = if Integer
al forall a. Eq a => a -> a -> Bool
== Integer
ah Bool -> Bool -> Bool
&& Integer
bl forall a. Eq a => a -> a -> Bool
== Integer
bh Bool -> Bool -> Bool
&& Integer
al forall a. Eq a => a -> a -> Bool
== Integer
bl
then Bool
True
else if Integer
cl forall a. Num a => a -> a -> a
+ Integer
cw forall a. Eq a => a -> a -> Bool
== Integer
ch
then Integer -> Integer -> Bool
checkSameWrapInterval Integer
cl Integer
ch
else Integer -> Integer -> Bool
checkSameWrapInterval Integer
cl Integer
mask Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
checkSameWrapInterval Integer
0 Integer
ch
where
(Integer
mask, Integer
cl, Integer
cw) = case Domain w
c of
BVDInterval Integer
mask' Integer
cl' Integer
cw' -> (Integer
mask', Integer
cl', Integer
cw')
BVDAny Integer
mask' -> (Integer
mask', Integer
0, Integer
mask')
ch :: Integer
ch = (Integer
cl forall a. Num a => a -> a -> a
+ Integer
cw) forall a. Bits a => a -> a -> a
.&. Integer
mask
(Integer
al, Integer
ah) = forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
a
(Integer
bl, Integer
bh) = forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
b
checkSameWrapInterval :: Integer -> Integer -> Bool
checkSameWrapInterval Integer
lo Integer
hi =
Integer
ah forall a. Num a => a -> a -> a
+ Integer
hi forall a. Ord a => a -> a -> Bool
<= Integer
mask Bool -> Bool -> Bool
&& Integer
bh forall a. Num a => a -> a -> a
+ Integer
hi forall a. Ord a => a -> a -> Bool
<= Integer
mask Bool -> Bool -> Bool
|| Integer
mask forall a. Ord a => a -> a -> Bool
< Integer
al forall a. Num a => a -> a -> a
+ Integer
lo Bool -> Bool -> Bool
&& Integer
mask forall a. Ord a => a -> a -> Bool
< Integer
bl forall a. Num a => a -> a -> a
+ Integer
lo
any :: (1 <= w) => NatRepr w -> Domain w
any :: forall (w :: Nat). (1 <= w) => NatRepr w -> Domain w
any NatRepr w
w = forall (w :: Nat). Integer -> Domain w
BVDAny (forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w)
singleton :: (HasCallStack, 1 <= w) => NatRepr w -> Integer -> Domain w
singleton :: forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
x = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDInterval Integer
mask (Integer
x forall a. Bits a => a -> a -> a
.&. Integer
mask) Integer
0
where mask :: Integer
mask = forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w
range :: NatRepr w -> Integer -> Integer -> Domain w
range :: forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr w
w Integer
al Integer
ah = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
al ((Integer
ah forall a. Num a => a -> a -> a
- Integer
al) forall a. Bits a => a -> a -> a
.&. Integer
mask)
where mask :: Integer
mask = forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w
interval :: Integer -> Integer -> Integer -> Domain w
interval :: forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
al Integer
aw =
if Integer
aw forall a. Ord a => a -> a -> Bool
>= Integer
mask then forall (w :: Nat). Integer -> Domain w
BVDAny Integer
mask else forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDInterval Integer
mask (Integer
al forall a. Bits a => a -> a -> a
.&. Integer
mask) Integer
aw
fromAscEltList :: (1 <= w) => NatRepr w -> [Integer] -> Domain w
fromAscEltList :: forall (w :: Nat). (1 <= w) => NatRepr w -> [Integer] -> Domain w
fromAscEltList NatRepr w
w [] = forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
0
fromAscEltList NatRepr w
w [Integer
x] = forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
x
fromAscEltList NatRepr w
w (Integer
x0 : Integer
x1 : [Integer]
xs) = (Integer, Integer) -> (Integer, Integer) -> [Integer] -> Domain w
go (Integer
x0, Integer
x0) (Integer
x1, Integer
x1) [Integer]
xs
where
go :: (Integer, Integer) -> (Integer, Integer) -> [Integer] -> Domain w
go (Integer
a, Integer
b) (Integer
c, Integer
d) [] = forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
union (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr w
w Integer
a Integer
b) (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr w
w Integer
c Integer
d)
go (Integer
a, Integer
b) (Integer
c, Integer
d) (Integer
e : [Integer]
rest)
| Integer
e forall a. Num a => a -> a -> a
- Integer
d forall a. Ord a => a -> a -> Bool
> Integer
c forall a. Num a => a -> a -> a
- Integer
b = (Integer, Integer) -> (Integer, Integer) -> [Integer] -> Domain w
go (Integer
a, Integer
d) (Integer
e, Integer
e) [Integer]
rest
| Bool
otherwise = (Integer, Integer) -> (Integer, Integer) -> [Integer] -> Domain w
go (Integer
a, Integer
b) (Integer
c, Integer
e) [Integer]
rest
union :: (1 <= w) => Domain w -> Domain w -> Domain w
union :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
union Domain w
a Domain w
b =
case Domain w
a of
BVDAny Integer
_ -> Domain w
a
BVDInterval Integer
_ Integer
al Integer
aw ->
case Domain w
b of
BVDAny Integer
_ -> Domain w
b
BVDInterval Integer
mask Integer
bl Integer
bw ->
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
cl (Integer
ch forall a. Num a => a -> a -> a
- Integer
cl)
where
sz :: Integer
sz = Integer
mask forall a. Num a => a -> a -> a
+ Integer
1
ac :: Integer
ac = Integer
2 forall a. Num a => a -> a -> a
* Integer
al forall a. Num a => a -> a -> a
+ Integer
aw
bc :: Integer
bc = Integer
2 forall a. Num a => a -> a -> a
* Integer
bl forall a. Num a => a -> a -> a
+ Integer
bw
al' :: Integer
al' = if Integer
ac forall a. Num a => a -> a -> a
+ Integer
mask forall a. Ord a => a -> a -> Bool
< Integer
bc then Integer
al forall a. Num a => a -> a -> a
+ Integer
sz else Integer
al
bl' :: Integer
bl' = if Integer
bc forall a. Num a => a -> a -> a
+ Integer
mask forall a. Ord a => a -> a -> Bool
< Integer
ac then Integer
bl forall a. Num a => a -> a -> a
+ Integer
sz else Integer
bl
ah' :: Integer
ah' = Integer
al' forall a. Num a => a -> a -> a
+ Integer
aw
bh' :: Integer
bh' = Integer
bl' forall a. Num a => a -> a -> a
+ Integer
bw
cl :: Integer
cl = forall a. Ord a => a -> a -> a
min Integer
al' Integer
bl'
ch :: Integer
ch = forall a. Ord a => a -> a -> a
max Integer
ah' Integer
bh'
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 Domain u
a NatRepr v
v Domain v
b =
case Domain u
a of
BVDAny Integer
_ -> forall (w :: Nat). Integer -> Domain w
BVDAny Integer
mask
BVDInterval Integer
_ Integer
al Integer
aw -> forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask (Integer -> Integer -> Integer
cat Integer
al Integer
bl) (Integer -> Integer -> Integer
cat Integer
aw Integer
bw)
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)
(Integer
bl, Integer
bh) = forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain v
b
bw :: Integer
bw = Integer
bh forall a. Num a => a -> a -> a
- Integer
bl
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 Domain (i + n)
a =
case Domain (i + n)
a of
BVDAny Integer
mask -> forall (w :: Nat). Integer -> Domain w
BVDAny (Integer -> Integer
shr Integer
mask)
BVDInterval Integer
mask Integer
al Integer
aw ->
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval (Integer -> Integer
shr Integer
mask) Integer
bl (Integer
bh forall a. Num a => a -> a -> a
- Integer
bl)
where
bl :: Integer
bl = Integer -> Integer
shr Integer
al
bh :: Integer
bh = Integer -> Integer
shr (Integer
al forall a. Num a => a -> a -> a
+ Integer
aw)
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 Domain w
a =
case Domain w
a of
BVDAny Integer
_ -> forall (w :: Nat). Integer -> Domain w
BVDAny Integer
mask
BVDInterval Integer
_ Integer
al Integer
aw -> forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
al Integer
aw
where
mask :: Integer
mask = forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr n
n
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 Domain w
a NatRepr u
u = forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr u
u Integer
al Integer
ah
where (Integer
al, Integer
ah) = forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
a
sext ::
forall w u. (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 Domain w
a NatRepr u
u =
case LeqProof 1 u
fProof of
LeqProof 1 u
LeqProof ->
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr u
u Integer
al Integer
ah
where (Integer
al, Integer
ah) = forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> (Integer, Integer)
sbounds NatRepr w
w Domain w
a
where
wProof :: LeqProof 1 w
wProof :: LeqProof 1 w
wProof = forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof
uProof :: LeqProof (w+1) u
uProof :: LeqProof (w + 1) u
uProof = forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof
fProof :: LeqProof 1 u
fProof :: LeqProof 1 u
fProof = forall (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans (forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 w
wProof (forall (n :: Nat). KnownNat n => NatRepr n
knownNat :: NatRepr 1)) LeqProof (w + 1) u
uProof
shl :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
shl :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
shl NatRepr w
w Domain w
a Domain w
b
| forall (w :: Nat). Domain w -> Bool
isBVDAny Domain w
a = Domain w
a
| forall (w :: Nat). Domain w -> Bool
isSingletonZero Domain w
a = Domain w
a
| forall (w :: Nat). Domain w -> Bool
isSingletonZero Domain w
b = Domain w
a
| Bool
otherwise = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
lo (Integer
hi forall a. Num a => a -> a -> a
- Integer
lo)
where
mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
sz :: Integer
sz = Integer
mask forall a. Num a => a -> a -> a
+ Integer
1
(Integer
bl, Integer
bh) = forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
b
bl' :: Int
bl' = forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
bl
bh' :: Int
bh' = forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
bh
cl :: Integer
cl = if (Integer
mask forall a. Bits a => a -> Int -> a
`shiftR` Int
bl' forall a. Eq a => a -> a -> Bool
== Integer
0) then Integer
sz else forall a. Bits a => Int -> a
bit Int
bl'
ch :: Integer
ch = if (Integer
mask forall a. Bits a => a -> Int -> a
`shiftR` Int
bh' forall a. Eq a => a -> a -> Bool
== Integer
0) then Integer
sz else forall a. Bits a => Int -> a
bit Int
bh'
(Integer
lo, Integer
hi) = (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer)
mulRange (forall (w :: Nat). Domain w -> (Integer, Integer)
zbounds Domain w
a) (Integer
cl, Integer
ch)
lshr :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
lshr :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
lshr NatRepr w
w Domain w
a Domain w
b = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
cl (Integer
ch forall a. Num a => a -> a -> a
- Integer
cl)
where
mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
(Integer
al, Integer
ah) = forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
a
(Integer
bl, Integer
bh) = forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
b
cl :: Integer
cl = Integer
al forall a. Bits a => a -> Int -> a
`shiftR` forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
bh
ch :: Integer
ch = Integer
ah forall a. Bits a => a -> Int -> a
`shiftR` forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
bl
ashr :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
ashr :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
ashr NatRepr w
w Domain w
a Domain w
b = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
cl (Integer
ch forall a. Num a => a -> a -> a
- Integer
cl)
where
mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
(Integer
al, Integer
ah) = forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> (Integer, Integer)
sbounds NatRepr w
w Domain w
a
(Integer
bl, Integer
bh) = forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
b
cl :: Integer
cl = Integer
al forall a. Bits a => a -> Int -> a
`shiftR` (if Integer
al forall a. Ord a => a -> a -> Bool
< Integer
0 then forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
bl else forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
bh)
ch :: Integer
ch = Integer
ah forall a. Bits a => a -> Int -> a
`shiftR` (if Integer
ah forall a. Ord a => a -> a -> Bool
< Integer
0 then forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
bh else forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
bl)
clamp :: NatRepr w -> Integer -> Int
clamp :: forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
x = forall a. Num a => Integer -> a
fromInteger (forall a. Ord a => a -> a -> a
min (forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w) Integer
x)
add :: (1 <= w) => Domain w -> Domain w -> Domain w
add :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
add Domain w
a Domain w
b =
case Domain w
a of
BVDAny Integer
_ -> Domain w
a
BVDInterval Integer
_ Integer
al Integer
aw ->
case Domain w
b of
BVDAny Integer
_ -> Domain w
b
BVDInterval Integer
mask Integer
bl Integer
bw ->
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask (Integer
al forall a. Num a => a -> a -> a
+ Integer
bl) (Integer
aw forall a. Num a => a -> a -> a
+ Integer
bw)
negate :: (1 <= w) => Domain w -> Domain w
negate :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w
negate Domain w
a =
case Domain w
a of
BVDAny Integer
_ -> Domain w
a
BVDInterval Integer
mask Integer
al Integer
aw -> forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDInterval Integer
mask ((-Integer
ah) forall a. Bits a => a -> a -> a
.&. Integer
mask) Integer
aw
where ah :: Integer
ah = Integer
al forall a. Num a => a -> a -> a
+ Integer
aw
scale :: (1 <= w) => Integer -> Domain w -> Domain w
scale :: forall (w :: Nat). (1 <= w) => Integer -> Domain w -> Domain w
scale Integer
k Domain w
a
| Integer
k forall a. Eq a => a -> a -> Bool
== Integer
0 = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDInterval (forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a) Integer
0 Integer
0
| Integer
k forall a. Eq a => a -> a -> Bool
== Integer
1 = Domain w
a
| Bool
otherwise =
case Domain w
a of
BVDAny Integer
_ -> Domain w
a
BVDInterval Integer
mask Integer
al Integer
aw
| Integer
k forall a. Ord a => a -> a -> Bool
>= Integer
0 -> forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask (Integer
k forall a. Num a => a -> a -> a
* Integer
al) (Integer
k forall a. Num a => a -> a -> a
* Integer
aw)
| Bool
otherwise -> forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask (Integer
k forall a. Num a => a -> a -> a
* Integer
ah) (forall a. Num a => a -> a
abs Integer
k forall a. Num a => a -> a -> a
* Integer
aw)
where ah :: Integer
ah = Integer
al forall a. Num a => a -> a -> a
+ Integer
aw
mul :: (1 <= w) => Domain w -> Domain w -> Domain w
mul :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
mul Domain w
a Domain w
b
| forall (w :: Nat). Domain w -> Bool
isSingletonZero Domain w
a = Domain w
a
| forall (w :: Nat). Domain w -> Bool
isSingletonZero Domain w
b = Domain w
b
| forall (w :: Nat). Domain w -> Bool
isBVDAny Domain w
a = Domain w
a
| forall (w :: Nat). Domain w -> Bool
isBVDAny Domain w
b = Domain w
b
| Bool
otherwise = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
cl (Integer
ch forall a. Num a => a -> a -> a
- Integer
cl)
where
mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
(Integer
cl, Integer
ch) = (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer)
mulRange (forall (w :: Nat). Domain w -> (Integer, Integer)
zbounds Domain w
a) (forall (w :: Nat). Domain w -> (Integer, Integer)
zbounds Domain w
b)
zbounds :: Domain w -> (Integer, Integer)
zbounds :: forall (w :: Nat). Domain w -> (Integer, Integer)
zbounds Domain w
a =
case Domain w
a of
BVDAny Integer
mask -> (Integer
0, Integer
mask)
BVDInterval Integer
mask Integer
lo Integer
sz -> (Integer
lo', Integer
lo' forall a. Num a => a -> a -> a
+ Integer
sz)
where lo' :: Integer
lo' = if Integer
2forall a. Num a => a -> a -> a
*Integer
lo forall a. Num a => a -> a -> a
+ Integer
sz forall a. Ord a => a -> a -> Bool
> Integer
mask then Integer
lo forall a. Num a => a -> a -> a
- (Integer
mask forall a. Num a => a -> a -> a
+ Integer
1) else Integer
lo
mulRange :: (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer)
mulRange :: (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer)
mulRange (Integer
al, Integer
ah) (Integer
bl, Integer
bh) = (Integer
cl, Integer
ch)
where
(Integer
albl, Integer
albh) = Integer -> (Integer, Integer) -> (Integer, Integer)
scaleRange Integer
al (Integer
bl, Integer
bh)
(Integer
ahbl, Integer
ahbh) = Integer -> (Integer, Integer) -> (Integer, Integer)
scaleRange Integer
ah (Integer
bl, Integer
bh)
cl :: Integer
cl = forall a. Ord a => a -> a -> a
min Integer
albl Integer
ahbl
ch :: Integer
ch = forall a. Ord a => a -> a -> a
max Integer
albh Integer
ahbh
scaleRange :: Integer -> (Integer, Integer) -> (Integer, Integer)
scaleRange :: Integer -> (Integer, Integer) -> (Integer, Integer)
scaleRange Integer
k (Integer
lo, Integer
hi)
| Integer
k forall a. Ord a => a -> a -> Bool
< Integer
0 = (Integer
k forall a. Num a => a -> a -> a
* Integer
hi, Integer
k forall a. Num a => a -> a -> a
* Integer
lo)
| Bool
otherwise = (Integer
k forall a. Num a => a -> a -> a
* Integer
lo, Integer
k forall a. Num a => a -> a -> a
* Integer
hi)
udiv :: (1 <= w) => Domain w -> Domain w -> Domain w
udiv :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
udiv Domain w
a Domain w
b = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
ql (Integer
qh forall a. Num a => a -> a -> a
- Integer
ql)
where
mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
(Integer
al, Integer
ah) = forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
a
(Integer
bl, Integer
bh) = forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
b
ql :: Integer
ql = Integer
al forall a. Integral a => a -> a -> a
`div` forall a. Ord a => a -> a -> a
max Integer
1 Integer
bh
qh :: Integer
qh = Integer
ah forall a. Integral a => a -> a -> a
`div` forall a. Ord a => a -> a -> a
max Integer
1 Integer
bl
urem :: (1 <= w) => Domain w -> Domain w -> Domain w
urem :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
urem Domain w
a Domain w
b
| Integer
qh forall a. Eq a => a -> a -> Bool
== Integer
ql = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
rl (Integer
rh forall a. Num a => a -> a -> a
- Integer
rl)
| Bool
otherwise = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
0 (Integer
bh forall a. Num a => a -> a -> a
- Integer
1)
where
mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
(Integer
al, Integer
ah) = forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
a
(Integer
bl, Integer
bh) = forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
b
(Integer
ql, Integer
rl) = Integer
al forall a. Integral a => a -> a -> (a, a)
`divMod` forall a. Ord a => a -> a -> a
max Integer
1 Integer
bh
(Integer
qh, Integer
rh) = Integer
ah forall a. Integral a => a -> a -> (a, a)
`divMod` forall a. Ord a => a -> a -> a
max Integer
1 Integer
bl
data ReciprocalRange = ReciprocalRange Integer Integer
rbounds :: (1 <= w) => NatRepr w -> Domain w -> ReciprocalRange
rbounds :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> ReciprocalRange
rbounds NatRepr w
w Domain w
a =
case Domain w
a of
BVDAny Integer
_ -> Integer -> Integer -> ReciprocalRange
ReciprocalRange (-Integer
1) Integer
1
BVDInterval Integer
mask Integer
al Integer
aw
| Integer
ah forall a. Ord a => a -> a -> Bool
> Integer
mask forall a. Num a => a -> a -> a
+ Integer
1 -> Integer -> Integer -> ReciprocalRange
ReciprocalRange (-Integer
1) Integer
1
| Bool
otherwise -> Integer -> Integer -> ReciprocalRange
ReciprocalRange (Integer -> Integer
signed (forall a. Ord a => a -> a -> a
min Integer
mask Integer
ah)) (Integer -> Integer
signed (forall a. Ord a => a -> a -> a
max Integer
1 Integer
al))
where
ah :: Integer
ah = Integer
al forall a. Num a => a -> a -> a
+ Integer
aw
signed :: Integer -> Integer
signed Integer
x = if Integer
x forall a. Ord a => a -> a -> Bool
< forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
halfRange NatRepr w
w then Integer
x else Integer
x forall a. Num a => a -> a -> a
- (Integer
mask forall a. Num a => a -> a -> a
+ Integer
1)
sdivRange :: (Integer, Integer) -> ReciprocalRange -> (Integer, Integer)
sdivRange :: (Integer, Integer) -> ReciprocalRange -> (Integer, Integer)
sdivRange (Integer
al, Integer
ah) (ReciprocalRange Integer
bl Integer
bh) = (Integer
ql, Integer
qh)
where
(Integer
ql1, Integer
qh1) = (Integer, Integer) -> Integer -> (Integer, Integer)
scaleDownRange (Integer
al, Integer
ah) Integer
bh
(Integer
ql2, Integer
qh2) = (Integer, Integer) -> Integer -> (Integer, Integer)
scaleDownRange (Integer
al, Integer
ah) Integer
bl
ql :: Integer
ql = forall a. Ord a => a -> a -> a
min Integer
ql1 Integer
ql2
qh :: Integer
qh = forall a. Ord a => a -> a -> a
max Integer
qh1 Integer
qh2
scaleDownRange :: (Integer, Integer) -> Integer -> (Integer, Integer)
scaleDownRange :: (Integer, Integer) -> Integer -> (Integer, Integer)
scaleDownRange (Integer
lo, Integer
hi) Integer
k
| Integer
k forall a. Ord a => a -> a -> Bool
> Integer
0 = (Integer
lo forall a. Integral a => a -> a -> a
`quot` Integer
k, Integer
hi forall a. Integral a => a -> a -> a
`quot` Integer
k)
| Integer
k forall a. Ord a => a -> a -> Bool
< Integer
0 = (Integer
hi forall a. Integral a => a -> a -> a
`quot` Integer
k, Integer
lo forall a. Integral a => a -> a -> a
`quot` Integer
k)
| Bool
otherwise = (Integer
lo, Integer
hi)
sdiv :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
sdiv :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
sdiv NatRepr w
w Domain w
a Domain w
b = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
ql (Integer
qh forall a. Num a => a -> a -> a
- Integer
ql)
where
mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
(Integer
ql, Integer
qh) = (Integer, Integer) -> ReciprocalRange -> (Integer, Integer)
sdivRange (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> (Integer, Integer)
sbounds NatRepr w
w Domain w
a) (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> ReciprocalRange
rbounds NatRepr w
w Domain w
b)
srem :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
srem :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
srem NatRepr w
w Domain w
a Domain w
b =
if Integer
ql forall a. Eq a => a -> a -> Bool
== Integer
qh then
(if Integer
ql forall a. Ord a => a -> a -> Bool
< Integer
0
then forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask (Integer
al forall a. Num a => a -> a -> a
- Integer
ql forall a. Num a => a -> a -> a
* Integer
bl) (Integer
aw forall a. Num a => a -> a -> a
- Integer
ql forall a. Num a => a -> a -> a
* Integer
bw)
else forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask (Integer
al forall a. Num a => a -> a -> a
- Integer
ql forall a. Num a => a -> a -> a
* Integer
bh) (Integer
aw forall a. Num a => a -> a -> a
+ Integer
ql forall a. Num a => a -> a -> a
* Integer
bw))
else forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
rl (Integer
rh forall a. Num a => a -> a -> a
- Integer
rl)
where
mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
(Integer
al, Integer
ah) = forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> (Integer, Integer)
sbounds NatRepr w
w Domain w
a
(Integer
bl, Integer
bh) = forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> (Integer, Integer)
sbounds NatRepr w
w Domain w
b
(Integer
ql, Integer
qh) = (Integer, Integer) -> ReciprocalRange -> (Integer, Integer)
sdivRange (Integer
al, Integer
ah) (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> ReciprocalRange
rbounds NatRepr w
w Domain w
b)
rl :: Integer
rl = if Integer
al forall a. Ord a => a -> a -> Bool
< Integer
0 then forall a. Ord a => a -> a -> a
min (Integer
blforall a. Num a => a -> a -> a
+Integer
1) (-Integer
bhforall a. Num a => a -> a -> a
+Integer
1) else Integer
0
rh :: Integer
rh = if Integer
ah forall a. Ord a => a -> a -> Bool
> Integer
0 then forall a. Ord a => a -> a -> a
max (-Integer
blforall a. Num a => a -> a -> a
-Integer
1) (Integer
bhforall a. Num a => a -> a -> a
-Integer
1) else Integer
0
aw :: Integer
aw = Integer
ah forall a. Num a => a -> a -> a
- Integer
al
bw :: Integer
bw = Integer
bh forall a. Num a => a -> a -> a
- Integer
bl
not :: Domain w -> Domain w
not :: forall (w :: Nat). Domain w -> Domain w
not Domain w
a =
case Domain w
a of
BVDAny Integer
_ -> Domain w
a
BVDInterval Integer
mask Integer
al Integer
aw ->
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDInterval Integer
mask (forall a. Bits a => a -> a
complement Integer
ah forall a. Bits a => a -> a -> a
.&. Integer
mask) Integer
aw
where ah :: Integer
ah = Integer
al forall a. Num a => a -> a -> a
+ Integer
aw
bitbounds :: Domain w -> (Integer, Integer)
bitbounds :: forall (w :: Nat). Domain w -> (Integer, Integer)
bitbounds Domain w
a =
case Domain w
a of
BVDAny Integer
mask -> (Integer
0, Integer
mask)
BVDInterval Integer
mask Integer
al Integer
aw
| Integer
al forall a. Num a => a -> a -> a
+ Integer
aw forall a. Ord a => a -> a -> Bool
> Integer
mask -> (Integer
0, Integer
mask)
| Bool
otherwise -> (Integer
lo, Integer
hi)
where
au :: Integer
au = forall (w :: Nat). Domain w -> Integer
unknowns Domain w
a
hi :: Integer
hi = Integer
al forall a. Bits a => a -> a -> a
.|. Integer
au
lo :: Integer
lo = Integer
hi forall a. Bits a => a -> a -> a
`Bits.xor` Integer
au
unknowns :: Domain w -> Integer
unknowns :: forall (w :: Nat). Domain w -> Integer
unknowns (BVDAny Integer
mask) = Integer
mask
unknowns (BVDInterval Integer
mask Integer
al Integer
aw) = Integer
mask forall a. Bits a => a -> a -> a
.&. (Integer -> Integer
fillright (Integer
al forall a. Bits a => a -> a -> a
`Bits.xor` (Integer
alforall a. Num a => a -> a -> a
+Integer
aw)))
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
fillright :: Integer -> Integer
fillright :: Integer -> Integer
fillright = Int -> Integer -> Integer
go Int
1
where
go :: Int -> Integer -> Integer
go :: Int -> Integer -> Integer
go Int
i Integer
x
| Integer
x' forall a. Eq a => a -> a -> Bool
== Integer
x = Integer
x
| Bool
otherwise = Int -> Integer -> Integer
go (Int
2 forall a. Num a => a -> a -> a
* Int
i) Integer
x'
where x' :: Integer
x' = Integer
x forall a. Bits a => a -> a -> a
.|. (Integer
x forall a. Bits a => a -> Int -> a
`shiftR` Int
i)
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
w Integer
x = Bool -> Property
property (forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
w (forall (w :: Nat). (1 <= w) => NatRepr w -> Domain w
any NatRepr n
w) Integer
x)
correct_ubounds :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Property
correct_ubounds :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> Property
correct_ubounds NatRepr n
n (Domain n
a,Integer
x) = forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n Domain 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). Domain w -> (Integer, Integer)
ubounds Domain n
a
correct_sbounds :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Property
correct_sbounds :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> Property
correct_sbounds NatRepr n
n (Domain n
a,Integer
x) = forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n Domain 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 -> Domain w -> (Integer, Integer)
sbounds NatRepr n
n Domain 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 (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(HasCallStack, 1 <= w) =>
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). (1 <= w) => Domain w -> Domain w -> Domain w
union 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_add :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_add :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_add 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). (1 <= w) => Domain w -> Domain w -> Domain w
add Domain n
a Domain n
b) (Integer
x forall a. Num a => a -> a -> a
+ Integer
y)
correct_neg :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Property
correct_neg :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> Property
correct_neg 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). (1 <= w) => Domain w -> Domain w
negate Domain n
a) (forall a. Num a => a -> a
Prelude.negate Integer
x)
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_mul :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_mul :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_mul 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). (1 <= w) => Domain w -> Domain w -> Domain w
mul Domain n
a Domain n
b) (Integer
x forall a. Num a => a -> a -> a
* Integer
y)
correct_scale :: (1 <= n) => NatRepr n -> Integer -> (Domain n, Integer) -> Property
correct_scale :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Integer -> (Domain n, Integer) -> Property
correct_scale NatRepr n
n Integer
k (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). (1 <= w) => Integer -> Domain w -> Domain w
scale Integer
k' Domain 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_scale_eq :: (1 <= n) => NatRepr n -> Integer -> Domain n -> Property
correct_scale_eq :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Integer -> Domain n -> Property
correct_scale_eq NatRepr n
n Integer
k Domain n
a = Bool -> Property
property forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). Domain w -> Domain w -> Bool
sameDomain (forall (w :: Nat). (1 <= w) => Integer -> Domain w -> Domain w
scale Integer
k' Domain n
a) (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
mul (forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
singleton NatRepr n
n Integer
k) Domain n
a)
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 -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_udiv :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_udiv 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
==> Integer
y' forall a. Eq a => a -> a -> Bool
/= Integer
0 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) => Domain w -> Domain w -> Domain w
udiv Domain n
a Domain 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 -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_urem :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_urem 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
==> Integer
y' forall a. Eq a => a -> a -> Bool
/= Integer
0 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) => Domain w -> Domain w -> Domain w
urem Domain n
a Domain 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_sdivRange :: (Integer, Integer) -> (Integer, Integer) -> Integer -> Integer -> Property
correct_sdivRange :: (Integer, Integer)
-> (Integer, Integer) -> Integer -> Integer -> Property
correct_sdivRange (Integer, Integer)
a (Integer, Integer)
b Integer
x Integer
y =
forall {a}. Ord a => (a, a) -> a -> Bool
mem (Integer, Integer)
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall {a}. Ord a => (a, a) -> a -> Bool
mem (Integer, Integer)
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 {a}. Ord a => (a, a) -> a -> Bool
mem ((Integer, Integer) -> ReciprocalRange -> (Integer, Integer)
sdivRange (Integer, Integer)
a ReciprocalRange
b') (Integer
x forall a. Integral a => a -> a -> a
`quot` Integer
y)
where
b' :: ReciprocalRange
b' = Integer -> Integer -> ReciprocalRange
ReciprocalRange (forall a b. (a, b) -> b
snd (Integer, Integer)
b) (forall a b. (a, b) -> a
fst (Integer, Integer)
b)
mem :: (a, a) -> a -> Bool
mem (a
lo,a
hi) a
v = a
lo forall a. Ord a => a -> a -> Bool
<= a
v Bool -> Bool -> Bool
&& a
v forall a. Ord a => a -> a -> Bool
<= a
hi
correct_sdiv :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_sdiv :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_sdiv 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
==> Integer
y forall a. Eq a => a -> a -> Bool
/= Integer
0 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 -> Domain w -> Domain w
sdiv NatRepr n
n Domain n
a Domain 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 -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_srem :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_srem 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
==> Integer
y forall a. Eq a => a -> a -> Bool
/= Integer
0 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 -> Domain w -> Domain w
srem NatRepr n
n Domain n
a Domain 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 -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_shl :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_shl 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).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
shl NatRepr n
n Domain n
a Domain 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 (w :: Nat). NatRepr w -> Integer
intValue NatRepr n
n) Integer
y)
correct_lshr :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_lshr :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_lshr 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).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
lshr NatRepr n
n Domain n
a Domain 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 (w :: Nat). NatRepr w -> Integer
intValue NatRepr n
n) Integer
y)
correct_ashr :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_ashr :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_ashr 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).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
ashr NatRepr n
n Domain n
a Domain 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 (w :: Nat). NatRepr w -> Integer
intValue NatRepr n
n) Integer
y)
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_ult :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_ult :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_ult 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). (1 <= w) => Domain w -> Domain w -> Maybe Bool
ult 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. 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 -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_slt :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_slt 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).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Maybe Bool
slt NatRepr n
n Domain n
a Domain 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_isUltSumCommonEquiv ::
(1 <= n) =>
NatRepr n ->
(Domain n, Integer) ->
(Domain n, Integer) ->
(Domain n, Integer) ->
Property
correct_isUltSumCommonEquiv :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (Domain n, Integer)
-> (Domain n, Integer)
-> (Domain n, Integer)
-> Property
correct_isUltSumCommonEquiv NatRepr n
n (Domain n
a, Integer
x) (Domain n
b, Integer
y) (Domain n
c, Integer
z) =
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 (w :: Nat). Domain w -> Integer -> Bool
member Domain n
c Integer
z forall t. Verifiable t => Bool -> t -> Property
==>
forall (w :: Nat). Domain w -> Domain w -> Domain w -> Bool
isUltSumCommonEquiv Domain n
a Domain n
b Domain n
c forall t. Verifiable t => Bool -> t -> Property
==>
((forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n (Integer
x forall a. Num a => a -> a -> a
+ Integer
z) forall a. Ord a => a -> a -> Bool
< forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n (Integer
y forall a. Num a => a -> a -> a
+ Integer
z)) forall a. Eq a => a -> a -> Bool
== (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))
correct_unknowns :: (1 <= n) => Domain n -> Integer -> Integer -> Property
correct_unknowns :: forall (n :: Nat).
(1 <= n) =>
Domain n -> Integer -> Integer -> Property
correct_unknowns 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 (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
y forall t. Verifiable t => Bool -> t -> Property
==> ((Integer
x forall a. Bits a => a -> a -> a
.|. Integer
u) forall a. Eq a => a -> a -> Bool
== (Integer
y forall a. Bits a => a -> a -> a
.|. Integer
u)) Bool -> Bool -> Bool
&& (Integer
u forall a. Bits a => a -> a -> a
.|. Integer
mask forall a. Eq a => a -> a -> Bool
== Integer
mask)
where
u :: Integer
u = forall (w :: Nat). Domain w -> Integer
unknowns Domain n
a
mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
bvdMask Domain n
a
correct_bitbounds :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Property
correct_bitbounds :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> Property
correct_bitbounds 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
==> (Integer -> Integer -> Bool
bitle Integer
lo Integer
x' Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
bitle Integer
x' Integer
hi Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
bitle Integer
hi (forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr n
n))
where
x' :: Integer
x' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x
(Integer
lo, Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
bitbounds Domain n
a