{-|
Module      : What4.Utils.BVDomain.Bitwise
Copyright   : (c) Galois Inc, 2020
License     : BSD3
Maintainer  : huffman@galois.com

Provides a bitwise implementation of bitvector abstract domains.
-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

module What4.Utils.BVDomain.Bitwise
  ( Domain(..)
  , bitle
  , proper
  , bvdMask
  , member
  , pmember
  , size
  , asSingleton
  , nonempty
  , eq
  , domainsOverlap
  , bitbounds
  -- * Operations
  , any
  , singleton
  , range
  , interval
  , union
  , intersection
  , concat
  , select
  , zext
  , sext
  , testBit
  -- ** shifts and rotates
  , shl
  , lshr
  , ashr
  , rol
  , ror
  -- ** bitwise logical
  , and
  , or
  , xor
  , not

  -- * Correctness properties
  , genDomain
  , genElement
  , genPair
  , correct_any
  , correct_singleton
  , correct_overlap
  , correct_union
  , correct_intersection
  , correct_zero_ext
  , correct_sign_ext
  , correct_concat
  , correct_shrink
  , correct_trunc
  , correct_select
  , correct_shl
  , correct_lshr
  , correct_ashr
  , correct_rol
  , correct_ror
  , correct_eq
  , correct_and
  , correct_or
  , correct_not
  , correct_xor
  , correct_testBit
  ) where

import           Data.Bits hiding (testBit, xor)
import qualified Data.Bits as Bits
import           Data.Parameterized.NatRepr
import           Numeric.Natural
import           GHC.TypeNats
import           Test.Verification (Property, property, (==>), Gen, chooseInteger)

import qualified Prelude
import           Prelude hiding (any, concat, negate, and, or, not)

import qualified What4.Utils.Arithmetic as Arith

-- | A bitwise interval domain, defined via a
--   bitwise upper and lower bound.  The ordering
--   used here to construct the interval is the pointwise
--   ordering on bits.  In particular @x [= y iff x .|. y == y@,
--   and a value @x@ is in the set defined by the pair @(lo,hi)@
--   just when @lo [= x && x [= hi@.
data Domain (w :: Nat) =
  BVBitInterval !Integer !Integer !Integer
  -- ^ @BVDBitInterval mask lo hi@.
  --  @mask@ caches the value of @2^w - 1@
 deriving (Int -> Domain w -> ShowS
[Domain w] -> ShowS
Domain w -> String
(Int -> Domain w -> ShowS)
-> (Domain w -> String) -> ([Domain w] -> ShowS) -> Show (Domain w)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (w :: Nat). Int -> Domain w -> ShowS
forall (w :: Nat). [Domain w] -> ShowS
forall (w :: Nat). Domain w -> String
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)

-- | Test if the domain satisfies its invariants
proper :: NatRepr w -> Domain w -> Bool
proper :: NatRepr w -> Domain w -> Bool
proper NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) =
  Integer
mask Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w Bool -> Bool -> Bool
&&
  Integer -> Integer -> Bool
bitle Integer
lo Integer
mask Bool -> Bool -> Bool
&&
  Integer -> Integer -> Bool
bitle Integer
hi Integer
mask Bool -> Bool -> Bool
&&
  Integer -> Integer -> Bool
bitle Integer
lo Integer
hi

-- | Test if the given integer value is a member of the abstract domain
member :: Domain w -> Integer -> Bool
member :: Domain w -> Integer -> Bool
member (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
x = Integer -> Integer -> Bool
bitle Integer
lo Integer
x' Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
bitle Integer
x' Integer
hi
  where x' :: Integer
x' = Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask

-- | Compute how many concrete elements are in the abstract domain
size :: Domain w -> Integer
size :: Domain w -> Integer
size (BVBitInterval Integer
_ Integer
lo Integer
hi)
  | Integer -> Integer -> Bool
bitle Integer
lo Integer
hi = Int -> Integer
forall a. Bits a => Int -> a
Bits.bit Int
p
  | Bool
otherwise   = Integer
0
 where
 u :: Integer
u = Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
Bits.xor Integer
lo Integer
hi
 p :: Int
p = Integer -> Int
forall a. Bits a => a -> Int
Bits.popCount Integer
u

bitle :: Integer -> Integer -> Bool
bitle :: Integer -> Integer -> Bool
bitle Integer
x Integer
y = (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
y) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y

-- | Return the bitvector mask value from this domain
bvdMask :: Domain w -> Integer
bvdMask :: Domain w -> Integer
bvdMask (BVBitInterval Integer
mask Integer
_ Integer
_) = Integer
mask

-- | Random generator for domain values.  We always generate
--   nonempty domain values.
genDomain :: NatRepr w -> Gen (Domain w)
genDomain :: NatRepr w -> Gen (Domain w)
genDomain NatRepr w
w =
  do let mask :: Integer
mask = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w
     Integer
lo <- (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, Integer
mask)
     Integer
hi <- (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, Integer
mask)
     Domain w -> Gen (Domain w)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Domain w -> Gen (Domain w)) -> Domain w -> Gen (Domain w)
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
lo (Integer
lo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
hi)

-- This generator goes to some pains to try
-- to generate a good statistical distribution
-- of the values in the domain.  It only choses
-- random bits for the "unknown" values of
-- the domain, then stripes them out among
-- the unknown bit positions.
genElement :: Domain w -> Gen Integer
genElement :: Domain w -> Gen Integer
genElement (BVBitInterval Integer
_mask Integer
lo Integer
hi) =
  do Integer
x <- (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, Int -> Integer
forall a. Bits a => Int -> a
bit Int
bs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
     Integer -> Gen Integer
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Integer -> Gen Integer) -> Integer -> Gen Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Int -> Integer
stripe Integer
lo Integer
x Int
0

 where
 u :: Integer
u = Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
Bits.xor Integer
lo Integer
hi
 bs :: Int
bs = Integer -> Int
forall a. Bits a => a -> Int
Bits.popCount Integer
u
 stripe :: Integer -> Integer -> Int -> Integer
stripe Integer
val Integer
x Int
i
   | Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Integer
val
   | Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
u Int
i =
       let val' :: Integer
val' = if Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
x Int
0 then Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
setBit Integer
val Int
i else Integer
val in
       Integer -> Integer -> Int -> Integer
stripe Integer
val' (Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
1) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
   | Bool
otherwise = Integer -> Integer -> Int -> Integer
stripe Integer
val Integer
x (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)

{- A faster generator, but I worry that it
   doesn't have very good statistical properties...

genElement :: Domain w -> Gen Integer
genElement (BVBitInterval mask lo hi) =
  do let u = Bits.xor lo hi
     x <- chooseInteger (0, mask)
     pure ((x .&. u) .|. lo)
-}

-- | Generate a random nonempty domain and an element
--   contained in that domain.
genPair :: NatRepr w -> Gen (Domain w, Integer)
genPair :: NatRepr w -> Gen (Domain w, Integer)
genPair NatRepr w
w =
  do Domain w
a <- NatRepr w -> Gen (Domain w)
forall (w :: Nat). NatRepr w -> Gen (Domain w)
genDomain NatRepr w
w
     Integer
x <- Domain w -> Gen Integer
forall (w :: Nat). Domain w -> Gen Integer
genElement Domain w
a
     (Domain w, Integer) -> Gen (Domain w, Integer)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Domain w
a,Integer
x)

-- | Unsafe constructor for internal use.
interval :: Integer -> Integer -> Integer -> Domain w
interval :: Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
lo Integer
hi = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
lo Integer
hi

-- | Construct a domain from bitwise lower and upper bounds
range :: NatRepr w -> Integer -> Integer -> Domain w
range :: NatRepr w -> Integer -> Integer -> Domain w
range NatRepr w
w Integer
lo Integer
hi = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w) Integer
lo' Integer
hi'
  where
  lo' :: Integer
lo'  = Integer
lo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask
  hi' :: Integer
hi'  = Integer
hi Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask
  mask :: Integer
mask = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w

-- | Bitwise lower and upper bounds
bitbounds :: Domain w -> (Integer, Integer)
bitbounds :: Domain w -> (Integer, Integer)
bitbounds (BVBitInterval Integer
_ Integer
lo Integer
hi) = (Integer
lo, Integer
hi)

-- | Test if this domain contains a single value, and return it if so
asSingleton :: Domain w -> Maybe Integer
asSingleton :: Domain w -> Maybe Integer
asSingleton (BVBitInterval Integer
_ Integer
lo Integer
hi) = if Integer
lo Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
hi then Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
lo else Maybe Integer
forall a. Maybe a
Nothing

-- | Returns true iff there is at least on element
--   in this bitwise domain.
nonempty :: Domain w -> Bool
nonempty :: Domain w -> Bool
nonempty (BVBitInterval Integer
_mask Integer
lo Integer
hi) = Integer -> Integer -> Bool
bitle Integer
lo Integer
hi

-- | Return a domain containing just the given value
singleton :: NatRepr w -> Integer -> Domain w
singleton :: NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
x = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
x' Integer
x'
  where
  x' :: Integer
x' = Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask
  mask :: Integer
mask = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w

-- | Bitwise domain containing every bitvector value
any :: NatRepr w -> Domain w
any :: NatRepr w -> Domain w
any NatRepr w
w = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
0 Integer
mask
  where
  mask :: Integer
mask = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w

-- | Returns true iff the domains have some value in common
domainsOverlap :: Domain w -> Domain w -> Bool
domainsOverlap :: Domain w -> Domain w -> Bool
domainsOverlap Domain w
a Domain w
b = Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
nonempty (Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
intersection Domain w
a Domain w
b)

eq :: Domain w -> Domain w -> Maybe Bool
eq :: Domain w -> Domain w -> Maybe Bool
eq Domain w
a Domain w
b
  | Just Integer
x <- Domain w -> Maybe Integer
forall (w :: Nat). Domain w -> Maybe Integer
asSingleton Domain w
a
  , Just Integer
y <- Domain w -> Maybe Integer
forall (w :: Nat). Domain w -> Maybe Integer
asSingleton Domain w
b
  = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y)

  | Bool -> Bool
Prelude.not (Domain w -> Domain w -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
domainsOverlap Domain w
a Domain w
b) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
  | Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing

intersection :: Domain w -> Domain w -> Domain w
intersection :: Domain w -> Domain w -> Domain w
intersection (BVBitInterval Integer
mask Integer
alo Integer
ahi) (BVBitInterval Integer
_ Integer
blo Integer
bhi) =
  Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer
alo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
blo) (Integer
ahi Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bhi)

union :: Domain w -> Domain w -> Domain w
union :: Domain w -> Domain w -> Domain w
union (BVBitInterval Integer
mask Integer
alo Integer
ahi) (BVBitInterval Integer
_ Integer
blo Integer
bhi) =
  Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer
alo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
blo) (Integer
ahi Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
bhi)

-- | @concat a y@ returns domain where each element in @a@ has been
-- concatenated with an element in @y@.  The most-significant bits
-- are @a@, and the least significant bits are @y@.
concat :: NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
concat :: NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
concat NatRepr u
u (BVBitInterval Integer
_ Integer
alo Integer
ahi) NatRepr v
v (BVBitInterval Integer
_ Integer
blo Integer
bhi) =
    Integer -> Integer -> Integer -> Domain (u + v)
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer -> Integer -> Integer
cat Integer
alo Integer
blo) (Integer -> Integer -> Integer
cat Integer
ahi Integer
bhi)
  where
    cat :: Integer -> Integer -> Integer
cat Integer
i Integer
j = (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` NatRepr v -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr v
v) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j
    mask :: Integer
mask = NatRepr (u + v) -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned (NatRepr u -> NatRepr v -> NatRepr (u + v)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr u
u NatRepr v
v)

-- | @shrink i a@ drops the @i@ least significant bits from @a@.
shrink ::
  NatRepr i ->
  Domain (i + n) -> Domain n
shrink :: NatRepr i -> Domain (i + n) -> Domain n
shrink NatRepr i
i (BVBitInterval Integer
mask Integer
lo Integer
hi) = Integer -> Integer -> Integer -> Domain n
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval (Integer -> Integer
shr Integer
mask) (Integer -> Integer
shr Integer
lo) (Integer -> Integer
shr Integer
hi)
  where
  shr :: Integer -> Integer
shr Integer
x = Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` NatRepr i -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr i
i

-- | @trunc n d@ selects the @n@ least significant bits from @d@.
trunc ::
  (n <= w) =>
  NatRepr n ->
  Domain w ->
  Domain n
trunc :: NatRepr n -> Domain w -> Domain n
trunc NatRepr n
n (BVBitInterval Integer
_ Integer
lo Integer
hi) = NatRepr n -> Integer -> Integer -> Domain n
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr n
n Integer
lo Integer
hi

-- | @select i n a@ selects @n@ bits starting from index @i@ from @a@.
select ::
  (1 <= n, i + n <= w) =>
  NatRepr i ->
  NatRepr n ->
  Domain w -> Domain n
select :: NatRepr i -> NatRepr n -> Domain w -> Domain n
select NatRepr i
i NatRepr n
n Domain w
a = NatRepr i -> Domain (i + n) -> Domain n
forall (i :: Nat) (n :: Nat).
NatRepr i -> Domain (i + n) -> Domain n
shrink NatRepr i
i (NatRepr (i + n) -> Domain w -> Domain (i + n)
forall (n :: Nat) (w :: Nat).
(n <= w) =>
NatRepr n -> Domain w -> Domain n
trunc (NatRepr i -> NatRepr n -> NatRepr (i + n)
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 :: Domain w -> NatRepr u -> Domain u
zext (BVBitInterval Integer
_ Integer
lo Integer
hi) NatRepr u
u = NatRepr u -> Integer -> Integer -> Domain u
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr u
u Integer
lo Integer
hi

sext :: (1 <= w, w+1 <= u) => NatRepr w -> Domain w -> NatRepr u -> Domain u
sext :: NatRepr w -> Domain w -> NatRepr u -> Domain u
sext NatRepr w
w (BVBitInterval Integer
_ Integer
lo Integer
hi) NatRepr u
u = NatRepr u -> Integer -> Integer -> Domain u
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr u
u Integer
lo' Integer
hi'
  where
  lo' :: Integer
lo' = NatRepr w -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr w
w Integer
lo
  hi' :: Integer
hi' = NatRepr w -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr w
w Integer
hi

testBit :: Domain w -> Natural -> Maybe Bool
testBit :: Domain w -> Natural -> Maybe Bool
testBit (BVBitInterval Integer
_mask Integer
lo Integer
hi) Natural
i = if Bool
lob Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
hib then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
lob else Maybe Bool
forall a. Maybe a
Nothing
  where
  lob :: Bool
lob = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
lo Int
j
  hib :: Bool
hib = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
hi Int
j
  j :: Int
j = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
i

shl :: NatRepr w -> Domain w -> Integer -> Domain w
shl :: NatRepr w -> Domain w -> Integer -> Domain w
shl NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
y = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer -> Integer
shleft Integer
lo) (Integer -> Integer
shleft Integer
hi)
  where
  y' :: Int
y' = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
y (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w))
  shleft :: Integer -> Integer
shleft Integer
x = (Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
y') Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask

rol :: NatRepr w -> Domain w -> Integer -> Domain w
rol :: NatRepr w -> Domain w -> Integer -> Domain w
rol NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
y =
  Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (NatRepr w -> Integer -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateLeft NatRepr w
w Integer
lo Integer
y) (NatRepr w -> Integer -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateLeft NatRepr w
w Integer
hi Integer
y)

ror :: NatRepr w -> Domain w -> Integer -> Domain w
ror :: NatRepr w -> Domain w -> Integer -> Domain w
ror NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
y =
  Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (NatRepr w -> Integer -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateRight NatRepr w
w Integer
lo Integer
y) (NatRepr w -> Integer -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateRight NatRepr w
w Integer
hi Integer
y)

lshr :: NatRepr w -> Domain w -> Integer -> Domain w
lshr :: NatRepr w -> Domain w -> Integer -> Domain w
lshr NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
y = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer -> Integer
shr Integer
lo) (Integer -> Integer
shr Integer
hi)
  where
  y' :: Int
y' = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
y (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w))
  shr :: Integer -> Integer
shr Integer
x = Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
y'

ashr :: (1 <= w) => NatRepr w -> Domain w -> Integer -> Domain w
ashr :: NatRepr w -> Domain w -> Integer -> Domain w
ashr NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
y = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer -> Integer
shr Integer
lo) (Integer -> Integer
shr Integer
hi)
  where
  y' :: Int
y' = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
y (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w))
  shr :: Integer -> Integer
shr Integer
x = ((NatRepr w -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr w
w Integer
x) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
y') Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask

not :: Domain w -> Domain w
not :: Domain w -> Domain w
not (BVBitInterval Integer
mask Integer
alo Integer
ahi) =
  Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer
ahi Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
mask) (Integer
alo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
mask)

and :: Domain w -> Domain w -> Domain w
and :: Domain w -> Domain w -> Domain w
and (BVBitInterval Integer
mask Integer
alo Integer
ahi) (BVBitInterval Integer
_ Integer
blo Integer
bhi) =
  Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer
alo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
blo) (Integer
ahi Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bhi)

or :: Domain w -> Domain w -> Domain w
or :: Domain w -> Domain w -> Domain w
or (BVBitInterval Integer
mask Integer
alo Integer
ahi) (BVBitInterval Integer
_ Integer
blo Integer
bhi) =
  Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer
alo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
blo) (Integer
ahi Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
bhi)

xor :: Domain w -> Domain w -> Domain w
xor :: Domain w -> Domain w -> Domain w
xor (BVBitInterval Integer
mask Integer
alo Integer
ahi) (BVBitInterval Integer
_ Integer
blo Integer
bhi) = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
clo Integer
chi
  where
  au :: Integer
au  = Integer
alo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
ahi
  bu :: Integer
bu  = Integer
blo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
bhi
  c :: Integer
c   = Integer
alo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
blo
  cu :: Integer
cu  = Integer
au Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
bu
  chi :: Integer
chi = Integer
c  Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
cu
  clo :: Integer
clo = Integer
chi Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
cu


---------------------------------------------------------------------------------------
-- Correctness properties

-- | Check that a domain is proper, and that
--   the given value is a member
pmember :: NatRepr n -> Domain n -> Integer -> Bool
pmember :: NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n Domain n
a Integer
x = NatRepr n -> Domain n -> Bool
forall (w :: Nat). NatRepr w -> Domain w -> Bool
proper NatRepr n
n Domain n
a Bool -> Bool -> Bool
&& Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x

correct_any :: (1 <= n) => NatRepr n -> Integer -> Property
correct_any :: NatRepr n -> Integer -> Property
correct_any NatRepr n
n Integer
x = Bool -> Property
property (NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w
any NatRepr n
n) Integer
x)

correct_singleton :: (1 <= n) => NatRepr n -> Integer -> Integer -> Property
correct_singleton :: NatRepr n -> Integer -> Integer -> Property
correct_singleton NatRepr n
n Integer
x Integer
y = Bool -> Property
property (NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> Integer -> Domain n
forall (w :: Nat). NatRepr w -> Integer -> Domain w
singleton NatRepr n
n Integer
x') Integer
y' Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== (Integer
x' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y'))
  where
  x' :: Integer
x' = NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x
  y' :: Integer
y' = NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y

correct_overlap :: Domain n -> Domain n -> Integer -> Property
correct_overlap :: Domain n -> Domain n -> Integer -> Property
correct_overlap Domain n
a Domain n
b Integer
x =
  Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Bool -> Bool
&& Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Domain n -> Domain n -> Bool
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 :: NatRepr n -> Domain n -> Domain n -> Integer -> Property
correct_union NatRepr n
n Domain n
a Domain n
b Integer
x =
  Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Bool -> Bool
|| Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
union Domain n
a Domain n
b) Integer
x

correct_intersection :: (1 <= n) => Domain n -> Domain n -> Integer -> Property
correct_intersection :: Domain n -> Domain n -> Integer -> Property
correct_intersection Domain n
a Domain n
b Integer
x = -- NB, intersection might not be proper
  Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Bool -> Bool
&& Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
intersection Domain n
a Domain n
b) Integer
x

correct_zero_ext :: (1 <= w, w+1 <= u) => NatRepr w -> Domain w -> NatRepr u -> Integer -> Property
correct_zero_ext :: NatRepr w -> Domain w -> NatRepr u -> Integer -> Property
correct_zero_ext NatRepr w
w Domain w
a NatRepr u
u Integer
x = Domain w -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain w
a Integer
x' Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr u -> Domain u -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr u
u (Domain w -> NatRepr u -> Domain 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' = NatRepr w -> Integer -> Integer
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 :: NatRepr w -> Domain w -> NatRepr u -> Integer -> Property
correct_sign_ext NatRepr w
w Domain w
a NatRepr u
u Integer
x = Domain w -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain w
a Integer
x' Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr u -> Domain u -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr u
u (NatRepr w -> Domain w -> NatRepr u -> Domain 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' = NatRepr w -> Integer -> Integer
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 :: 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) = Domain m -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain m
a Integer
x' Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
y' Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr (m + n) -> Domain (m + n) -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember (NatRepr m -> NatRepr n -> NatRepr (m + n)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr m
m NatRepr n
n) (NatRepr m -> Domain m -> NatRepr n -> Domain n -> Domain (m + 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' = NatRepr m -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr m
m Integer
x
  y' :: Integer
y' = NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y
  z :: Integer
z  = Integer
x' Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (NatRepr n -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr n
n) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
y'

correct_shrink :: NatRepr i -> NatRepr n -> (Domain (i + n), Integer) -> Property
correct_shrink :: NatRepr i -> NatRepr n -> (Domain (i + n), Integer) -> Property
correct_shrink NatRepr i
i NatRepr n
n (Domain (i + n)
a,Integer
x) = Domain (i + n) -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain (i + n)
a Integer
x' Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr i -> Domain (i + n) -> Domain n
forall (i :: Nat) (n :: Nat).
NatRepr i -> Domain (i + n) -> Domain n
shrink NatRepr i
i Domain (i + n)
a) (Integer
x' Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` NatRepr i -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr i
i)
  where
  x' :: Integer
x' = Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Domain (i + n) -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain (i + n)
a

correct_trunc :: (n <= w) => NatRepr n -> (Domain w, Integer) -> Property
correct_trunc :: NatRepr n -> (Domain w, Integer) -> Property
correct_trunc NatRepr n
n (Domain w
a,Integer
x) = Domain w -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain w
a Integer
x' Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> Domain w -> Domain n
forall (n :: Nat) (w :: Nat).
(n <= w) =>
NatRepr n -> Domain w -> Domain n
trunc NatRepr n
n Domain w
a) (NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x')
  where
  x' :: Integer
x' = Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Domain w -> Integer
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 :: NatRepr i -> NatRepr n -> (Domain w, Integer) -> Property
correct_select NatRepr i
i NatRepr n
n (Domain w
a, Integer
x) = Domain w -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain w
a Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr i -> NatRepr n -> Domain w -> Domain 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 = NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n ((Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` (NatRepr i -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr i
i))

correct_eq :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_eq :: NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_eq NatRepr n
n (Domain n
a,Integer
x) (Domain n
b,Integer
y) =
  Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==>
    case Domain n -> Domain n -> Maybe Bool
forall (w :: Nat). Domain w -> Domain w -> Maybe Bool
eq Domain n
a Domain n
b of
      Just Bool
True  -> NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y
      Just Bool
False -> NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y
      Maybe Bool
Nothing    -> Bool
True

correct_shl :: (1 <= n) => NatRepr n -> (Domain n,Integer) -> Integer -> Property
correct_shl :: NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_shl NatRepr n
n (Domain n
a,Integer
x) Integer
y = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> Domain n -> Integer -> Domain n
forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
shl NatRepr n
n Domain n
a Integer
y) Integer
z
  where
  z :: Integer
z = (NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min (NatRepr n -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr n
n) Integer
y)

correct_lshr :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_lshr :: NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_lshr NatRepr n
n (Domain n
a,Integer
x) Integer
y = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> Domain n -> Integer -> Domain n
forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
lshr NatRepr n
n Domain n
a Integer
y) Integer
z
  where
  z :: Integer
z = (NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min (NatRepr n -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr n
n) Integer
y)

correct_ashr :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_ashr :: NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_ashr NatRepr n
n (Domain n
a,Integer
x) Integer
y = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> Domain n -> Integer -> Domain n
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Integer -> Domain w
ashr NatRepr n
n Domain n
a Integer
y) Integer
z
  where
  z :: Integer
z = (NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min (NatRepr n -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr n
n) Integer
y)

correct_rol :: (1 <= n) => NatRepr n -> (Domain n,Integer) -> Integer -> Property
correct_rol :: NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_rol NatRepr n
n (Domain n
a,Integer
x) Integer
y = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> Domain n -> Integer -> Domain n
forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
rol NatRepr n
n Domain n
a Integer
y) (NatRepr n -> Integer -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateLeft NatRepr n
n Integer
x Integer
y)

correct_ror :: (1 <= n) => NatRepr n -> (Domain n,Integer) -> Integer -> Property
correct_ror :: NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_ror NatRepr n
n (Domain n
a,Integer
x) Integer
y = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> Domain n -> Integer -> Domain n
forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
ror NatRepr n
n Domain n
a Integer
y) (NatRepr n -> Integer -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateRight NatRepr n
n Integer
x Integer
y)

correct_not :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Property
correct_not :: NatRepr n -> (Domain n, Integer) -> Property
correct_not NatRepr n
n (Domain n
a,Integer
x) = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w
not Domain n
a) (Integer -> Integer
forall a. Bits a => a -> a
complement Integer
x)

correct_and :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_and :: NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_and NatRepr n
n (Domain n
a,Integer
x) (Domain n
b,Integer
y) = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
and Domain n
a Domain n
b) (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
y)

correct_or :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_or :: NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_or NatRepr n
n (Domain n
a,Integer
x) (Domain n
b,Integer
y) = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
or Domain n
a Domain n
b) (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
y)

correct_xor :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_xor :: NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_xor NatRepr n
n (Domain n
a,Integer
x) (Domain n
b,Integer
y) = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
xor Domain n
a Domain n
b) (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
y)

correct_testBit :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Natural -> Property
correct_testBit :: NatRepr n -> (Domain n, Integer) -> Natural -> Property
correct_testBit NatRepr n
n (Domain n
a,Integer
x) Natural
i =
  Natural
i Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr n -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr n
n Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==>
    case Domain n -> Natural -> Maybe Bool
forall (w :: Nat). Domain w -> Natural -> Maybe Bool
testBit Domain n
a Natural
i of
      Just Bool
True  -> Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
x (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
i)
      Just Bool
False -> Bool -> Bool
Prelude.not (Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
x (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
i))
      Maybe Bool
Nothing    -> Bool
True