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

Provides a bitwise implementation of bitvector abstract domains.
-}

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

module What4.Domains.BV.Bitwise
  ( Domain(..)
  , bitle
  , proper
  , bvdMask
  , member
  , pmember
  , size
  , asSingleton
  , nonempty
  , eq
  , slt
  , ult
  , domainsOverlap
  , bitbounds
  , ubounds
  , sbounds
  -- * Lattice operations
  , top
  , any
  , bottom
  , isBottom
  , join
  , union
  , meet
  , intersection
  , leq
  -- * Operations
  , singleton
  , range
  , interval
  , concat
  , select
  , zext
  , sext
  , testBit
  -- ** shifts and rotates
  , shl
  , lshr
  , ashr
  , rol
  , ror
  , shlAbstract
  , lshrAbstract
  , ashrAbstract
  , rolAbstract
  , rorAbstract
  , shlAbstractSpec
  , lshrAbstractSpec
  , ashrAbstractSpec
  , rolAbstractSpec
  , rorAbstractSpec
  -- ** arithmetic
  , add
  , sub
  , negate
  , scale
  , mul
  , mulPrecise
  , udiv
  , urem
  , sdiv
  , srem
  , udivPrecise
  , uremPrecise
  -- ** arithmetic (SMT-LIB div-by-zero semantics)
  , udivSmtlib
  , uremSmtlib
  , sdivSmtlib
  , sremSmtlib
  -- ** bitwise logical
  , and
  , or
  , xor
  , not

  -- * Correctness properties
  , genDomain
  , genElement
  , genPair
  , correct_any
  , correct_singleton
  , correct_overlap
  , correct_overlap_inv
  , correct_asSingleton
  , correct_union
  , correct_intersection
  , correct_join
  , correct_meet
  , precise_meet
  , correct_leq
  -- ** Lattice laws
  , join_commutative
  , join_idempotent
  , meet_commutative
  , meet_idempotent
  , join_top
  , join_bottom
  , meet_top
  , meet_bottom
  , leq_reflexive
  , leq_transitive
  , meet_lower_bound
  , join_upper_bound
  , join_monotone
  , meet_monotone
  , join_associative
  , meet_associative
  , join_absorb
  , meet_absorb
  , join_proper
  , meet_proper
  , 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_shlAbstract
  , correct_lshrAbstract
  , correct_ashrAbstract
  , correct_rolAbstract
  , correct_rorAbstract
  , correct_equiv_shlAbstract
  , correct_equiv_lshrAbstract
  , correct_equiv_ashrAbstract
  , correct_equiv_rolAbstract
  , correct_equiv_rorAbstract
  , correct_eq
  , correct_ult
  , correct_slt
  , correct_ubounds
  , correct_sbounds
  , correct_add
  , correct_sub
  , correct_neg
  , correct_scale
  , correct_mul
  , correct_mulPrecise
  , correct_udiv
  , correct_urem
  , correct_sdiv
  , correct_srem
  , correct_udivPrecise
  , correct_uremPrecise
  , correct_udivSmtlib
  , correct_uremSmtlib
  , correct_sdivSmtlib
  , correct_sremSmtlib
  , 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           What4.Domains.BV.Bitwise.Tnum (Tnum)
import qualified What4.Domains.BV.Bitwise.Tnum as Tnum
import           What4.Domains.Verification (Property, property, (==>), Gen, chooseInteger)

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

import qualified What4.Domains.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 (Domain w -> Domain w -> Bool
(Domain w -> Domain w -> Bool)
-> (Domain w -> Domain w -> Bool) -> Eq (Domain w)
forall (w :: Nat). Domain w -> Domain w -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (w :: Nat). Domain w -> Domain w -> Bool
== :: Domain w -> Domain w -> Bool
$c/= :: forall (w :: Nat). Domain w -> Domain w -> Bool
/= :: Domain w -> Domain w -> Bool
Eq, Eq (Domain w)
Eq (Domain w) =>
(Domain w -> Domain w -> Ordering)
-> (Domain w -> Domain w -> Bool)
-> (Domain w -> Domain w -> Bool)
-> (Domain w -> Domain w -> Bool)
-> (Domain w -> Domain w -> Bool)
-> (Domain w -> Domain w -> Domain w)
-> (Domain w -> Domain w -> Domain w)
-> Ord (Domain w)
Domain w -> Domain w -> Bool
Domain w -> Domain w -> Ordering
Domain w -> Domain w -> Domain w
forall (w :: Nat). Eq (Domain w)
forall (w :: Nat). Domain w -> Domain w -> Bool
forall (w :: Nat). Domain w -> Domain w -> Ordering
forall (w :: Nat). Domain w -> Domain w -> Domain w
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: forall (w :: Nat). Domain w -> Domain w -> Ordering
compare :: Domain w -> Domain w -> Ordering
$c< :: forall (w :: Nat). Domain w -> Domain w -> Bool
< :: Domain w -> Domain w -> Bool
$c<= :: forall (w :: Nat). Domain w -> Domain w -> Bool
<= :: Domain w -> Domain w -> Bool
$c> :: forall (w :: Nat). Domain w -> Domain w -> Bool
> :: Domain w -> Domain w -> Bool
$c>= :: forall (w :: Nat). Domain w -> Domain w -> Bool
>= :: Domain w -> Domain w -> Bool
$cmax :: forall (w :: Nat). Domain w -> Domain w -> Domain w
max :: Domain w -> Domain w -> Domain w
$cmin :: forall (w :: Nat). Domain w -> Domain w -> Domain w
min :: Domain w -> Domain w -> Domain w
Ord, Int -> Domain w -> ShowS
[Domain w] -> ShowS
Domain w -> String
(Int -> Domain w -> ShowS)
-> (Domain w -> String) -> ([Domain w] -> ShowS) -> Show (Domain w)
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
$cshowsPrec :: forall (w :: Nat). Int -> Domain w -> ShowS
showsPrec :: Int -> Domain w -> ShowS
$cshow :: forall (w :: Nat). Domain w -> String
show :: Domain w -> String
$cshowList :: forall (w :: Nat). [Domain w] -> ShowS
showList :: [Domain w] -> ShowS
Show)

-- | /O(w)/. Test if the domain satisfies its invariants.
proper :: NatRepr w -> Domain w -> Bool
proper :: forall (w :: Nat). NatRepr w -> Domain w -> Bool
proper NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) =
  Integer
mask 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

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

-- | /O(w)/. Compute how many concrete elements are in the abstract domain.
size :: Domain w -> Integer
size :: forall (w :: Nat). Domain w -> Integer
size d :: Domain w
d@(BVBitInterval Integer
_ Integer
lo Integer
hi)
  | Integer -> Integer -> Bool
bitle Integer
lo Integer
hi = Int -> Integer
forall a. Bits a => Int -> a
Bits.bit (Integer -> Int
forall a. Bits a => a -> Int
Bits.popCount (Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
unknownBits Domain w
d))
  | Bool
otherwise   = Integer
0

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

-- | /O(1)/. The set of bit positions whose values are not constant
-- throughout the domain — i.e.\ the tristate-number mask. Bits set here
-- vary; bits clear here are determined (and equal in @lo@ and @hi@).
unknownBits :: Domain w -> Integer
unknownBits :: forall (w :: Nat). Domain w -> Integer
unknownBits (BVBitInterval Integer
_ Integer
lo Integer
hi) = Integer
lo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
hi
{-# INLINE unknownBits #-}

-- | /O(1)/. Return the bitvector mask value from this domain.
bvdMask :: Domain w -> Integer
bvdMask :: forall (w :: Nat). 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 :: forall (w :: Nat). 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 a. a -> Gen a
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 chooses
-- random bits for the "unknown" values of
-- the domain, then stripes them out among
-- the unknown bit positions.
genElement :: Domain w -> Gen Integer
genElement :: forall (w :: Nat). Domain w -> Gen Integer
genElement d :: Domain w
d@(BVBitInterval Integer
_mask Integer
lo Integer
_) =
  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 a. a -> Gen a
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 = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
unknownBits Domain w
d
 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
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
   | Bool
otherwise = Integer -> Integer -> Int -> Integer
stripe Integer
val Integer
x (Int
i Int -> 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 :: forall (w :: Nat). 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 a. a -> Gen a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Domain w
a,Integer
x)

-- | /O(1)/. Unsafe constructor for internal use.
interval :: Integer -> Integer -> Integer -> Domain w
interval :: forall (w :: Nat). 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

-- | /O(w)/. Construct a domain from bitwise lower and upper bounds.
range :: NatRepr w -> Integer -> Integer -> Domain w
range :: forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr w
w Integer
lo Integer
hi = 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

-- | /O(1)/. Bitwise lower and upper bounds.
bitbounds :: Domain w -> (Integer, Integer)
bitbounds :: forall (w :: Nat). Domain w -> (Integer, Integer)
bitbounds (BVBitInterval Integer
_ Integer
lo Integer
hi) = (Integer
lo, Integer
hi)

-- | /O(w)/. Test if this domain contains a single value, and return it if so.
asSingleton :: Domain w -> Maybe Integer
asSingleton :: forall (w :: Nat). 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

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

------------------------------------------------------------------------
-- Lattice operations

-- | /O(1)/. Top element of the lattice: represents all bitvectors of width @w@.
top :: NatRepr w -> Domain w
top :: forall (w :: Nat). NatRepr w -> Domain w
top 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
{-# INLINE top #-}

-- | /O(w)/. Bitwise domain containing every bitvector value.
{-# DEPRECATED any "Use 'top' instead" #-}
any :: NatRepr w -> Domain w
any :: forall (w :: Nat). NatRepr w -> Domain w
any = NatRepr w -> Domain w
forall (w :: Nat). NatRepr w -> Domain w
top
{-# INLINE any #-}

-- | /O(1)/. Bottom element of the lattice: represents the empty set of bitvectors.
-- This is an improper domain whose membership predicate is unsatisfiable.
bottom :: NatRepr w -> Domain w
bottom :: forall (w :: Nat). NatRepr w -> Domain w
bottom NatRepr w
w = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
mask Integer
0
  where
  mask :: Integer
mask = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w
{-# INLINE bottom #-}

-- | /O(1)/.
isBottom :: Domain w -> Bool
isBottom :: forall (w :: Nat). Domain w -> Bool
isBottom (BVBitInterval Integer
mask Integer
lo Integer
hi) = Integer
lo Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
mask Bool -> Bool -> Bool
&& Integer
hi Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0

-- | /O(w)/. Lattice join: pointwise least upper bound on the bit-level @bitle@ ordering.
join :: Domain w -> Domain w -> Domain w
join :: forall (w :: Nat). Domain w -> Domain w -> Domain w
join (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)

{-# DEPRECATED union "Use 'join' instead" #-}
union :: Domain w -> Domain w -> Domain w
union :: forall (w :: Nat). Domain w -> Domain w -> Domain w
union = Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
join
{-# INLINE union #-}

-- | /O(w)/. Lattice meet: pointwise greatest lower bound on the bit-level @bitle@ ordering.
-- If both inputs are proper (or bottom), so is the result.
meet :: Domain w -> Domain w -> Domain w
meet :: forall (w :: Nat). Domain w -> Domain w -> Domain w
meet (BVBitInterval Integer
mask Integer
alo Integer
ahi) (BVBitInterval Integer
_ Integer
blo Integer
bhi)
  | Integer -> Integer -> Bool
bitle Integer
lo Integer
hi = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
lo Integer
hi
  | Bool
otherwise   = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
mask Integer
0  -- canonical bottom
  where
    lo :: Integer
lo = Integer
alo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
blo
    hi :: Integer
hi = Integer
ahi Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bhi

{-# DEPRECATED intersection "Use 'meet' instead" #-}
intersection :: Domain w -> Domain w -> Domain w
intersection :: forall (w :: Nat). Domain w -> Domain w -> Domain w
intersection = Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
meet
{-# INLINE intersection #-}

-- | /O(w)/. Lattice ordering: @leq a b@ returns 'True' if every concrete value
-- represented by @a@ is also represented by @b@.
leq :: Domain w -> Domain w -> Bool
leq :: forall (w :: Nat). Domain w -> Domain w -> Bool
leq (BVBitInterval Integer
_ Integer
alo Integer
ahi) (BVBitInterval Integer
_ Integer
blo Integer
bhi) =
  Integer -> Integer -> Bool
bitle Integer
blo Integer
alo Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
bitle Integer
ahi Integer
bhi
{-# INLINE leq #-}

------------------------------------------------------------------------
-- Operations

-- | /O(w)/. Return a domain containing just the given value.
singleton :: NatRepr w -> Integer -> Domain w
singleton :: forall (w :: Nat). 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

-- | /O(w)/. Returns true iff the domains have some value in common.
domainsOverlap :: Domain w -> Domain w -> Bool
domainsOverlap :: forall (w :: Nat). 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
meet Domain w
a Domain w
b)

-- | /O(w)/. Decide equality of two domains: 'Just True' if both are the same
-- singleton, 'Just False' if they're disjoint, 'Nothing' otherwise.
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 <- 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

-- | /O(u + v)/. @concat a y@ returns a 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 :: forall (u :: Nat) (v :: Nat).
NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
concat NatRepr u
u (BVBitInterval Integer
_ Integer
alo Integer
ahi) NatRepr v
v (BVBitInterval Integer
_ Integer
blo Integer
bhi) =
    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)

-- | /O(w)/. @shrink i a@ drops the @i@ least significant bits from @a@.
shrink ::
  NatRepr i ->
  Domain (i + n) -> Domain n
shrink :: forall (i :: Nat) (n :: Nat).
NatRepr i -> Domain (i + n) -> Domain n
shrink NatRepr i
i (BVBitInterval Integer
mask Integer
lo Integer
hi) = 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

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

-- | /O(w)/. @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 :: 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 = 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)

-- | /O(w)/. Zero-extend a domain to a larger width.
zext :: (1 <= w, w + 1 <= u) => Domain w -> NatRepr u -> Domain u
zext :: forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
Domain w -> NatRepr u -> Domain u
zext (BVBitInterval Integer
_ Integer
lo Integer
hi) NatRepr u
u = NatRepr u -> Integer -> Integer -> Domain u
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr u
u Integer
lo Integer
hi

-- | /O(w)/. Sign-extend a domain to a larger width.
sext :: (1 <= w, w + 1 <= u) => NatRepr w -> Domain w -> NatRepr u -> Domain u
sext :: forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> Domain w -> NatRepr u -> Domain u
sext NatRepr w
w (BVBitInterval Integer
_ Integer
lo Integer
hi) NatRepr u
u = 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

-- | /O(w)/. Test bit @i@ of every value in the domain: 'Just True' if it is
-- set in every member, 'Just False' if clear in every member, 'Nothing' if
-- it varies.
testBit :: Domain w -> Natural -> Maybe Bool
testBit :: forall (w :: Nat). Domain w -> Nat -> Maybe Bool
testBit (BVBitInterval Integer
_mask Integer
lo Integer
hi) Nat
i = if Bool
lob 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 = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
i

-- | /O(w)/. Shift left by a known amount.
shl :: NatRepr w -> Domain w -> Integer -> Domain w
shl :: forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
shl NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
y = 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

-- | /O(w)/. Rotate left by a known amount.
rol :: NatRepr w -> Domain w -> Integer -> Domain w
rol :: forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
rol NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
y =
  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)

-- | /O(w)/. Rotate right by a known amount.
ror :: NatRepr w -> Domain w -> Integer -> Domain w
ror :: forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
ror NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
y =
  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)

-- | /O(w)/. Logical (zero-fill) shift right by a known amount.
lshr :: NatRepr w -> Domain w -> Integer -> Domain w
lshr :: forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
lshr NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
y = 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'

-- | /O(w)/. Arithmetic (sign-extending) shift right by a known amount.
ashr :: (1 <= w) => NatRepr w -> Domain w -> Integer -> Domain w
ashr :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Integer -> Domain w
ashr NatRepr w
w (BVBitInterval Integer
mask Integer
lo Integer
hi) Integer
y = 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

-- | Conflict ("empty") domain: invariant @lo [= hi@ is violated.
-- Used as the meet identity when intersecting per-shift contributions.
conflict :: Integer -> Domain w
conflict :: forall (w :: Nat). Integer -> Domain w
conflict Integer
mask = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
mask Integer
0

isConflict :: Domain w -> Bool
isConflict :: forall (w :: Nat). Domain w -> Bool
isConflict (BVBitInterval Integer
_ Integer
lo Integer
hi) = Bool -> Bool
Prelude.not (Integer -> Integer -> Bool
bitle Integer
lo Integer
hi)

-- | Is this the fully unknown domain, @[0, mask]@?
isAny :: Domain w -> Bool
isAny :: forall (w :: Nat). Domain w -> Bool
isAny (BVBitInterval Integer
mask Integer
lo Integer
hi) = Integer
lo Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 Bool -> Bool -> Bool
&& Integer
hi Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
mask

-- | Decompose @b@'s bounds into two bitmasks, @(zeros, ones)@:
--
-- * @zeros@ has a @1@ at every position where every member of @b@ has a @0@.
-- * @ones@ has a @1@ at every position where every member of @b@ has a @1@.
--
-- This is the same encoding LLVM's @KnownBits@ uses, and is paired with
-- 'memberMask' to check membership using bitwise operations alone.
knownZerosOnes :: Domain w -> (Integer, Integer)
knownZerosOnes :: forall (w :: Nat). Domain w -> (Integer, Integer)
knownZerosOnes (BVBitInterval Integer
mask Integer
lo Integer
hi) = (Integer
mask Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
hi, Integer
lo)

-- | Equivalent to 'member' @b@ @s@, given @(zeros, ones) = knownZerosOnes b@.
-- Cheaper than 'member' (no @[lo, hi]@ ordering check) and lets the inner
-- loop hoist @(zeros, ones)@ outside the iteration.
memberMask :: Integer -> Integer -> Integer -> Bool
memberMask :: Integer -> Integer -> Integer -> Bool
memberMask Integer
zeros Integer
ones Integer
s = (Integer
zeros Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
s) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 Bool -> Bool -> Bool
&& (Integer
ones Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
s) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
s

-- | Generic shift skeleton shared by 'shlAbstract', 'lshrAbstract', and
-- 'ashrAbstract'.
--
-- The idea: try every concrete shift amount @s@ that @b@ could be, apply
-- @op s@, and union the results. \"Union\" here means \"a result bit is
-- known to be 0 only if every per-shift result agrees it's 0, known to
-- be 1 only if every result agrees it's 1, otherwise unknown\".
--
-- Three optimizations make this fast:
--
-- * Don't iterate past the width. Every shift amount @>= w@ produces
--   the same result for a given @op@ (all zeros for @shl@/@lshr@, the
--   sign-extended pattern for @ashr@), so we iterate
--   @[bl, min bh w]@ and (if @bh > w@) collapse the rest into one
--   call @op w@.
-- * Skip impossible amounts. If @b@'s low bit is known to be 1, only
--   odd shift amounts are reachable; we use 'memberMask' to skip the
--   rest with a cheap pair of bitwise tests.
-- * Stop early. If the running union is already \"fully unknown\",
--   nothing more can be inferred.
--
-- Same iteration strategy as LLVM's @KnownBits::shl@, @KnownBits::lshr@,
-- and @KnownBits::ashr@.
{-# INLINE foldShifts #-}
foldShifts ::
  NatRepr w ->
  Domain w {- ^ shift-amount domain -} ->
  (Int -> Domain w) {- ^ per-shift transfer; @s@ ranges over @[0..w]@ -} ->
  Domain w
foldShifts :: forall (w :: Nat).
NatRepr w -> Domain w -> (Int -> Domain w) -> Domain w
foldShifts NatRepr w
w Domain w
b Int -> Domain w
op = Domain w -> Domain w
collapse (Integer -> Domain w -> Domain w
go Integer
bl (Integer -> Domain w
forall (w :: Nat). Integer -> Domain w
conflict Integer
mask))
  where
  mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
b
  wI :: Integer
wI = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w
  (Integer
bl, Integer
bh) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
b
  (Integer
zeros, Integer
ones) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
knownZerosOnes Domain w
b
  iterEnd :: Integer
iterEnd = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
bh Integer
wI
  go :: Integer -> Domain w -> Domain w
go !Integer
s !Domain w
acc
    | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isAny Domain w
acc = Domain w
acc
    | Integer
s Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
iterEnd =
        if Integer -> Integer -> Integer -> Bool
memberMask Integer
zeros Integer
ones Integer
s
          then Integer -> Domain w -> Domain w
go (Integer
s Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
union Domain w
acc (Int -> Domain w
op (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
s)))
          else Integer -> Domain w -> Domain w
go (Integer
s Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Domain w
acc
    | Integer
bh Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
wI =
        -- @b@'s high bound itself is a member of @b@ that exceeds @w@,
        -- so at least one shift amount falls in the saturated tail.
        Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
union Domain w
acc (Int -> Domain w
op (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
wI))
    | Bool
otherwise = Domain w
acc

  collapse :: Domain w -> Domain w
collapse Domain w
d
    | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isConflict Domain w
d = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
0 Integer
0
    | Bool
otherwise    = Domain w
d

-- | /O(w²)/. Shift left by an amount drawn from the domain @b@. See
-- 'foldShifts' for the algorithm.
--
-- More precisely, /O(n · w)/ where @w@ is the bitvector width and
-- @n = min(bh − bl + 1, w + 1)@ is the number of candidate shift amounts
-- considered, with @bl@ and @bh@ the unsigned bounds of @b@.
shlAbstract :: NatRepr w -> Domain w -> Domain w -> Domain w
shlAbstract :: forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
shlAbstract NatRepr w
w a :: Domain w
a@(BVBitInterval Integer
mask Integer
aLo Integer
aHi) Domain w
b
  -- Fast path: a fully unknown @a@ shifts in zeros at the bottom. Bits
  -- @[0..min bl w - 1]@ are forced to 0 because every concrete shift
  -- amount is at least @bl@ (and shift @>= w@ kills every bit).
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isAny Domain w
a =
      let k :: Int
k = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
bl (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w))
          lowZeros :: Integer
lowZeros = Int -> Integer
forall a. Bits a => Int -> a
bit Int
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
      in Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
0 (Integer
mask Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
lowZeros)
  | Bool
otherwise = NatRepr w -> Domain w -> (Int -> Domain w) -> Domain w
forall (w :: Nat).
NatRepr w -> Domain w -> (Int -> Domain w) -> Domain w
foldShifts NatRepr w
w Domain w
b Int -> Domain w
shiftBy
  where
  (Integer
bl, Integer
_) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
b
  shiftBy :: Int -> Domain w
shiftBy Int
s = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask ((Integer
aLo Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
s) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask)
                                 ((Integer
aHi Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
s) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask)

-- | /O(w²)/. Logical (zero-fill) shift right by an amount drawn from
-- the domain @b@. See 'foldShifts' for the algorithm.
--
-- More precisely, /O(n · w)/ where @w@ is the bitvector width and
-- @n = min(bh − bl + 1, w + 1)@ is the number of candidate shift amounts
-- considered, with @bl@ and @bh@ the unsigned bounds of @b@.
lshrAbstract :: NatRepr w -> Domain w -> Domain w -> Domain w
lshrAbstract :: forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
lshrAbstract NatRepr w
w a :: Domain w
a@(BVBitInterval Integer
mask Integer
aLo Integer
aHi) Domain w
b
  -- Fast path: every shift @>= bl@ forces the top @min bl w@ bits of
  -- the result to 0.
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isAny Domain w
a =
      let k :: Int
k = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
bl (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w))
          highMask :: Integer
highMask = Integer
mask Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
k
      in Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
0 Integer
highMask
  | Bool
otherwise = NatRepr w -> Domain w -> (Int -> Domain w) -> Domain w
forall (w :: Nat).
NatRepr w -> Domain w -> (Int -> Domain w) -> Domain w
foldShifts NatRepr w
w Domain w
b Int -> Domain w
shiftBy
  where
  (Integer
bl, Integer
_) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
b
  shiftBy :: Int -> Domain w
shiftBy Int
s = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer
aLo Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
s) (Integer
aHi Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
s)

-- | /O(w²)/. Arithmetic (sign-extending) shift right by an amount drawn
-- from the domain @b@. See 'foldShifts' for the algorithm.
--
-- More precisely, /O(n · w)/ where @w@ is the bitvector width and
-- @n = min(bh − bl + 1, w + 1)@ is the number of candidate shift amounts
-- considered, with @bl@ and @bh@ the unsigned bounds of @b@.
ashrAbstract :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
ashrAbstract :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
ashrAbstract NatRepr w
w (BVBitInterval Integer
mask Integer
aLo Integer
aHi) Domain w
b =
  NatRepr w -> Domain w -> (Int -> Domain w) -> Domain w
forall (w :: Nat).
NatRepr w -> Domain w -> (Int -> Domain w) -> Domain w
foldShifts NatRepr w
w Domain w
b Int -> Domain w
shiftBy
  where
  -- Sign-extending shift on the @lo@ and @hi@ bounds independently is
  -- sound: if every member of @a@ has a known-1 at position @i >= sign@,
  -- so does every member's @ashr s@; same for known-0.
  shiftBy :: Int -> Domain w
shiftBy Int
s = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask
                ((NatRepr w -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr w
w Integer
aLo Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
s) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask)
                ((NatRepr w -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr w
w Integer
aHi Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
s) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask)

-- | /O(w²)/. Rotate left by an amount drawn from the domain @b@. See
-- 'foldRotates' for the algorithm.
--
-- More precisely, /O(r · w)/ where @w@ is the bitvector width and @r@ is
-- the number of distinct residues mod @w@ that are reachable from @b@
-- (at most @w@).
rolAbstract :: NatRepr w -> Domain w -> Domain w -> Domain w
rolAbstract :: forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
rolAbstract NatRepr w
w (BVBitInterval Integer
mask Integer
aLo Integer
aHi) Domain w
b = NatRepr w -> Domain w -> (Int -> Domain w) -> Domain w -> Domain w
forall (w :: Nat).
NatRepr w -> Domain w -> (Int -> Domain w) -> Domain w -> Domain w
foldRotates NatRepr w
w Domain w
b Int -> Domain w
rotBy Domain w
fullDom
  where
  -- Fast path: if every residue in @[0, w-1]@ is reachable from @b@,
  -- every output bit could come from any input bit, so the answer is
  -- determined by @a@'s global structure alone.
  fullDom :: Domain w
fullDom = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
fullCoverage Integer
mask Integer
aLo Integer
aHi
  rotBy :: Int -> Domain w
rotBy Int
s = 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
aLo (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
s))
              (NatRepr w -> Integer -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateLeft NatRepr w
w Integer
aHi (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
s))

-- | /O(w²)/. Rotate right by an amount drawn from the domain @b@.
-- Mirrors 'rolAbstract'.
--
-- More precisely, /O(r · w)/ where @w@ is the bitvector width and @r@ is
-- the number of distinct residues mod @w@ that are reachable from @b@
-- (at most @w@).
rorAbstract :: NatRepr w -> Domain w -> Domain w -> Domain w
rorAbstract :: forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
rorAbstract NatRepr w
w (BVBitInterval Integer
mask Integer
aLo Integer
aHi) Domain w
b = NatRepr w -> Domain w -> (Int -> Domain w) -> Domain w -> Domain w
forall (w :: Nat).
NatRepr w -> Domain w -> (Int -> Domain w) -> Domain w -> Domain w
foldRotates NatRepr w
w Domain w
b Int -> Domain w
rotBy Domain w
fullDom
  where
  fullDom :: Domain w
fullDom = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
fullCoverage Integer
mask Integer
aLo Integer
aHi
  rotBy :: Int -> Domain w
rotBy Int
s = 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
aLo (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
s))
              (NatRepr w -> Integer -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateRight NatRepr w
w Integer
aHi (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
s))

-- | Generic rotate skeleton shared by 'rolAbstract' and 'rorAbstract'.
--
-- Rotating by @s@ is the same as rotating by @s `mod` w@, so we only
-- ever care about @w@ distinct rotation amounts. The trick is figuring
-- out which residues mod @w@ some member of @b@ can produce, then
-- unioning @op r@ over those residues. Two cases:
--
-- * Power-of-two width (the common case): @s `mod` w@ is just the low
--   @log2 w@ bits of @s@. So the reachable residues are exactly the
--   values consistent with @b@'s known bits restricted to those low
--   bits, and we use the same @KnownBits@-style mask check as
--   'foldShifts' to skip residues no member of @b@ can produce. This
--   gives the smallest sound result.
--
-- * Non-power-of-two width: there's no clean correspondence between
--   @b@'s bits and residues mod @w@. We fall back to bounds: the
--   residues reachable from @[bl, bh]@ form a (possibly wrapping)
--   range in @[0, w-1]@, which we iterate without further skipping.
--   Sound, sometimes loose.
--
-- Iteration is always at most @w@ steps, never over the (possibly
-- enormous) integer range @[bl, bh]@.
{-# INLINE foldRotates #-}
foldRotates ::
  NatRepr w ->
  Domain w {- ^ rotate-amount domain -} ->
  (Int -> Domain w) {- ^ per-amount transfer; argument is residue mod @w@ -} ->
  Domain w {- ^ result when all residues are reachable -} ->
  Domain w
foldRotates :: forall (w :: Nat).
NatRepr w -> Domain w -> (Int -> Domain w) -> Domain w -> Domain w
foldRotates NatRepr w
w Domain w
b Int -> Domain w
op Domain w
fullDom
  | Integer -> Bool
Arith.isPow2Integer Integer
wI =
      let residueMask :: Integer
residueMask = Integer
wI Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
          zerosLow :: Integer
zerosLow = Integer
zeros Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
residueMask
          onesLow :: Integer
onesLow = Integer
ones Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
residueMask
          allResiduesReachable :: Bool
allResiduesReachable = Integer
zerosLow Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 Bool -> Bool -> Bool
&& Integer
onesLow Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
          skip :: Int -> Bool
skip Int
r = Bool -> Bool
Prelude.not (Integer -> Integer -> Integer -> Bool
memberMask Integer
zerosLow Integer
onesLow (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
r))
      in if Bool
allResiduesReachable
           then Domain w
fullDom
           else (Int -> Bool) -> [(Int, Int)] -> Domain w -> Domain w
iterRanges Int -> Bool
skip [(Int
0, Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
wI Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)] (Integer -> Domain w
forall (w :: Nat). Integer -> Domain w
conflict Integer
mask)
  | Bool
otherwise =
      case Maybe [(Int, Int)]
residueRanges of
        Maybe [(Int, Int)]
Nothing     -> Domain w
fullDom
        Just [(Int, Int)]
ranges -> (Int -> Bool) -> [(Int, Int)] -> Domain w -> Domain w
iterRanges (\Int
_ -> Bool
False) [(Int, Int)]
ranges (Integer -> Domain w
forall (w :: Nat). Integer -> Domain w
conflict Integer
mask)
  where
  mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
b
  wI :: Integer
wI = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w
  (Integer
bl, Integer
bh) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
b
  (Integer
zeros, Integer
ones) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
knownZerosOnes Domain w
b

  -- Reduce @[bl, bh]@ mod @w@ to a list of residue ranges in @[0, w-1]@.
  -- @Nothing@ means every residue is reachable; otherwise the list has
  -- one or two ranges (two when the residue range wraps around @0@).
  residueRanges :: Maybe [(Int, Int)]
residueRanges
    | Integer
bh Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
bl Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
wI = Maybe [(Int, Int)]
forall a. Maybe a
Nothing
    | Bool
otherwise =
        let (Integer
ql, Integer
rl) = Integer
bl Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`divMod` Integer
wI
            (Integer
qh, Integer
rh) = Integer
bh Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`divMod` Integer
wI
        in if Integer
qh Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
ql
             then [(Int, Int)] -> Maybe [(Int, Int)]
forall a. a -> Maybe a
Just [(Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
rl, Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
rh)]
             else [(Int, Int)] -> Maybe [(Int, Int)]
forall a. a -> Maybe a
Just [(Int
0, Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
rh), (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
rl, Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
wI Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)]

  iterRanges :: (Int -> Bool) -> [(Int, Int)] -> Domain w -> Domain w
iterRanges Int -> Bool
_ [] Domain w
acc = Domain w
acc
  iterRanges Int -> Bool
skip ((Int
lo, Int
hi) : [(Int, Int)]
rest) Domain w
acc = (Int -> Bool) -> [(Int, Int)] -> Domain w -> Domain w
iterRanges Int -> Bool
skip [(Int, Int)]
rest ((Int -> Bool) -> Int -> Int -> Domain w -> Domain w
iter Int -> Bool
skip Int
lo Int
hi Domain w
acc)

  iter :: (Int -> Bool) -> Int -> Int -> Domain w -> Domain w
iter Int -> Bool
skip !Int
s !Int
hi !Domain w
acc
    | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isAny Domain w
acc = Domain w
acc
    | Int
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
hi    = Domain w
acc
    | Int -> Bool
skip Int
s    = (Int -> Bool) -> Int -> Int -> Domain w -> Domain w
iter Int -> Bool
skip (Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
hi Domain w
acc
    | Bool
otherwise = (Int -> Bool) -> Int -> Int -> Domain w -> Domain w
iter Int -> Bool
skip (Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
hi (Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
union Domain w
acc (Int -> Domain w
op Int
s))

-- | Declarative reference: union of @op s@ over every member @s@ of
-- @b@. /O(|b| · w / W)/, exponential in @w@, only suitable as a
-- correctness oracle, not for production.
foldShiftsSpec ::
  Integer  {- ^ mask -} ->
  Domain w {- ^ shift-amount domain -} ->
  (Integer -> Domain w) {- ^ per-amount transfer -} ->
  Domain w
foldShiftsSpec :: forall (w :: Nat).
Integer -> Domain w -> (Integer -> Domain w) -> Domain w
foldShiftsSpec Integer
mask Domain w
b Integer -> Domain w
op =
  (Integer -> Domain w -> Domain w)
-> Domain w -> [Integer] -> Domain w
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Prelude.foldr (\Integer
s Domain w
acc -> if Domain w -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain w
b Integer
s then Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
union Domain w
acc (Integer -> Domain w
op Integer
s) else Domain w
acc)
                (Integer -> Domain w
forall (w :: Nat). Integer -> Domain w
conflict Integer
mask)
                [Integer
0 .. Integer
mask]

-- | Declarative reference variant of 'shlAbstract': for every member
-- @y@ of the shift-amount domain, compute the per-shift result and
-- union them all. Strictly slower; used to validate 'shlAbstract'.
shlAbstractSpec :: NatRepr w -> Domain w -> Domain w -> Domain w
shlAbstractSpec :: forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
shlAbstractSpec NatRepr w
w Domain w
a Domain w
b = Integer -> Domain w -> (Integer -> Domain w) -> Domain w
forall (w :: Nat).
Integer -> Domain w -> (Integer -> Domain w) -> Domain w
foldShiftsSpec (Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a) Domain w
b (\Integer
y -> NatRepr w -> Domain w -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
shl NatRepr w
w Domain w
a Integer
y)

lshrAbstractSpec :: NatRepr w -> Domain w -> Domain w -> Domain w
lshrAbstractSpec :: forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
lshrAbstractSpec NatRepr w
w Domain w
a Domain w
b = Integer -> Domain w -> (Integer -> Domain w) -> Domain w
forall (w :: Nat).
Integer -> Domain w -> (Integer -> Domain w) -> Domain w
foldShiftsSpec (Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a) Domain w
b (\Integer
y -> NatRepr w -> Domain w -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
lshr NatRepr w
w Domain w
a Integer
y)

ashrAbstractSpec :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
ashrAbstractSpec :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
ashrAbstractSpec NatRepr w
w Domain w
a Domain w
b = Integer -> Domain w -> (Integer -> Domain w) -> Domain w
forall (w :: Nat).
Integer -> Domain w -> (Integer -> Domain w) -> Domain w
foldShiftsSpec (Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a) Domain w
b (\Integer
y -> NatRepr w -> Domain w -> Integer -> Domain w
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Integer -> Domain w
ashr NatRepr w
w Domain w
a Integer
y)

rolAbstractSpec :: NatRepr w -> Domain w -> Domain w -> Domain w
rolAbstractSpec :: forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
rolAbstractSpec NatRepr w
w Domain w
a Domain w
b = Integer -> Domain w -> (Integer -> Domain w) -> Domain w
forall (w :: Nat).
Integer -> Domain w -> (Integer -> Domain w) -> Domain w
foldShiftsSpec (Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a) Domain w
b (\Integer
y -> NatRepr w -> Domain w -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
rol NatRepr w
w Domain w
a Integer
y)

rorAbstractSpec :: NatRepr w -> Domain w -> Domain w -> Domain w
rorAbstractSpec :: forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
rorAbstractSpec NatRepr w
w Domain w
a Domain w
b = Integer -> Domain w -> (Integer -> Domain w) -> Domain w
forall (w :: Nat).
Integer -> Domain w -> (Integer -> Domain w) -> Domain w
foldShiftsSpec (Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a) Domain w
b (\Integer
y -> NatRepr w -> Domain w -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
ror NatRepr w
w Domain w
a Integer
y)

-- | The result of rotating @a@ by every position in @[0, w-1]@: each
-- output bit could come from any input bit, so the result is
-- determined by global properties of @a@. It's the all-zeros singleton
-- if @a = {0}@, the all-ones singleton if @a@ is the singleton mask,
-- and fully unknown otherwise.
fullCoverage :: Integer -> Integer -> Integer -> Domain w
fullCoverage :: forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
fullCoverage Integer
mask Integer
aLo Integer
aHi = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
outLo Integer
outHi
  where
  outHi :: Integer
outHi = if Integer
aHi Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Integer
0 else Integer
mask
  outLo :: Integer
outLo = if Integer
aLo Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
mask then Integer
mask else Integer
0

-- | /O(w)/. Bitwise complement.
not :: Domain w -> Domain w
not :: forall (w :: Nat). 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)

-- | /O(w)/. Bitwise AND of two domains.
and :: Domain w -> Domain w -> Domain w
and :: forall (w :: Nat). Domain w -> Domain w -> Domain w
and (BVBitInterval Integer
mask Integer
alo Integer
ahi) (BVBitInterval Integer
_ Integer
blo Integer
bhi) =
  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)

-- | /O(w)/. Bitwise OR of two domains.
or :: Domain w -> Domain w -> Domain w
or :: forall (w :: Nat). Domain w -> Domain w -> Domain w
or (BVBitInterval Integer
mask Integer
alo Integer
ahi) (BVBitInterval Integer
_ Integer
blo Integer
bhi) =
  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)

-- | /O(w)/. Bitwise XOR of two domains.
xor :: Domain w -> Domain w -> Domain w
xor :: forall (w :: Nat). Domain w -> Domain w -> Domain w
xor a :: Domain w
a@(BVBitInterval Integer
mask Integer
alo Integer
_) b :: Domain w
b@(BVBitInterval Integer
_ Integer
blo Integer
_) = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
clo Integer
chi
  where
  c :: Integer
c   = Integer
alo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
blo
  cu :: Integer
cu  = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
unknownBits Domain w
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
unknownBits Domain w
b
  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


---------------------------------------------------------------------------------------
-- Bounds and comparisons

-- | /O(1)/. Unsigned bounds for the domain. The low bit-pattern bound is
-- also the unsigned minimum, and the high bit-pattern bound is also the
-- unsigned maximum: setting unknown bits to 0 minimizes, setting them to
-- 1 maximizes.
ubounds :: Domain w -> (Integer, Integer)
ubounds :: forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
bitbounds

-- | /O(1)/. The mask with just the sign bit set: @bit (w - 1)@.
signBit :: (1 <= w) => NatRepr w -> Integer
signBit :: forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
signBit NatRepr w
w = Int -> Integer
forall a. Bits a => Int -> a
bit (NatRepr w -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr w
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
{-# INLINE signBit #-}

-- | /O(w)/. Signed bounds for the domain.
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 (BVBitInterval Integer
_ Integer
lo Integer
hi) = (NatRepr w -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr w
w Integer
lo', NatRepr w -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr w
w Integer
hi')
  where
  signbit :: Integer
signbit = NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
signBit NatRepr w
w
  -- If the sign bit is known (lo and hi agree on it), the bit-pattern
  -- bounds are also the signed bounds. If the sign bit is unknown, the
  -- most-negative value sets the sign bit and clears all other unknowns,
  -- and the most-positive clears the sign bit and sets all other unknowns.
  (Integer
lo', Integer
hi')
    | (Integer
lo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
signbit) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== (Integer
hi Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
signbit) = (Integer
lo, Integer
hi)
    | Bool
otherwise = (Integer
lo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
signbit, Integer
hi Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
signbit)

-- | /O(w)/. Check if all elements in one domain are unsigned-less-than all
-- elements in the other.
ult :: Domain w -> Domain w -> Maybe Bool
ult :: forall (w :: Nat). Domain w -> Domain w -> Maybe Bool
ult Domain w
a Domain w
b
  | Integer
ah Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
bl  = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
  | Integer
al Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
bh = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
  | Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing
  where
  (Integer
al, Integer
ah) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
a
  (Integer
bl, Integer
bh) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
b

-- | /O(w)/. Check if all elements in one domain are signed-less-than all
-- elements in the other.
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
ah Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
bl  = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
  | Integer
al Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
bh = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
  | Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing
  where
  (Integer
al, Integer
ah) = NatRepr w -> Domain w -> (Integer, Integer)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> (Integer, Integer)
sbounds NatRepr w
w Domain w
a
  (Integer
bl, Integer
bh) = NatRepr w -> Domain w -> (Integer, Integer)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> (Integer, Integer)
sbounds NatRepr w
w Domain w
b

---------------------------------------------------------------------------------------
-- Arithmetic

-- | Convert a domain into its tristate-number form.
toTnum :: Domain w -> Tnum
toTnum :: forall (w :: Nat). Domain w -> Tnum
toTnum d :: Domain w
d@(BVBitInterval Integer
_ Integer
lo Integer
_) = Integer -> Integer -> Tnum
Tnum.mk Integer
lo (Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
unknownBits Domain w
d)

-- | Convert a tristate-number back into a domain at the given @bvmask@.
fromTnum :: Integer -> Tnum -> Domain w
fromTnum :: forall (w :: Nat). Integer -> Tnum -> Domain w
fromTnum Integer
mask Tnum
t = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
v (Integer
v Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Tnum -> Integer
Tnum.tnumMask Tnum
t)
  where v :: Integer
v = Tnum -> Integer
Tnum.tnumValue Tnum
t

-- | Internal helper: build a singleton domain when only the mask is known.
mkSingleton :: Integer -> Integer -> Domain w
mkSingleton :: forall (w :: Nat). Integer -> Integer -> Domain w
mkSingleton Integer
mask 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

-- | /O(w)/. Add two bitwise domains.
add :: Domain w -> Domain w -> Domain w
add :: forall (w :: Nat). Domain w -> Domain w -> Domain w
add a :: Domain w
a@(BVBitInterval Integer
mask Integer
_ Integer
_) Domain w
b = Integer -> Tnum -> Domain w
forall (w :: Nat). Integer -> Tnum -> Domain w
fromTnum Integer
mask (Integer -> Tnum -> Tnum -> Tnum
Tnum.add Integer
mask (Domain w -> Tnum
forall (w :: Nat). Domain w -> Tnum
toTnum Domain w
a) (Domain w -> Tnum
forall (w :: Nat). Domain w -> Tnum
toTnum Domain w
b))

-- | /O(w)/. Two's complement negation: @negate a = not a + 1@.
negate :: Domain w -> Domain w
negate :: forall (w :: Nat). Domain w -> Domain w
negate Domain w
a = Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
add (Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w
not Domain w
a) (Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Domain w
mkSingleton (Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a) Integer
1)

-- | /O(w)/. Subtract: @sub a b = add a (negate b)@.
sub :: Domain w -> Domain w -> Domain w
sub :: forall (w :: Nat). Domain w -> Domain w -> Domain w
sub Domain w
a Domain w
b = Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
add Domain w
a (Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w
negate Domain w
b)

-- | /O(w²)/. Multiply by a constant. Uses 'mulPrecise' since the
-- shift-and-add algorithm gives bit-level precision when one operand
-- is concrete.
scale :: Integer -> Domain w -> Domain w
scale :: forall (w :: Nat). Integer -> Domain w -> Domain w
scale Integer
k Domain w
a = Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
mulPrecise (Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Domain w
mkSingleton (Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a) Integer
k) Domain w
a

-- | /O(w)/. Multiply two bitwise domains via interval and trailing-zero
-- analysis. Captures known leading bits (both 0s and 1s) derived from
-- @[aMin*bMin, aMax*bMax]@, plus known trailing zeros from the operands.
--
-- See 'Tnum.mul' for the algorithm. 'mulPrecise' is strictly more
-- precise; this is the cheaper alternative when middle-bit precision
-- doesn't matter.
mul :: Domain w -> Domain w -> Domain w
mul :: forall (w :: Nat). Domain w -> Domain w -> Domain w
mul a :: Domain w
a@(BVBitInterval Integer
mask Integer
_ Integer
_) Domain w
b =
  Integer -> Tnum -> Domain w
forall (w :: Nat). Integer -> Tnum -> Domain w
fromTnum Integer
mask (Integer -> Tnum -> Tnum -> Tnum
Tnum.mul Integer
mask (Domain w -> Tnum
forall (w :: Nat). Domain w -> Tnum
toTnum Domain w
a) (Domain w -> Tnum
forall (w :: Nat). Domain w -> Tnum
toTnum Domain w
b))

-- | /O(w²)/. Multiply two bitwise domains, combining the shift-and-add
-- tristate-number algorithm (BPF @tnum_mul@) with the interval and
-- trailing-zero analysis of 'mul'. Strictly at least as precise as 'mul'.
mulPrecise :: Domain w -> Domain w -> Domain w
mulPrecise :: forall (w :: Nat). Domain w -> Domain w -> Domain w
mulPrecise a :: Domain w
a@(BVBitInterval Integer
mask Integer
_ Integer
_) Domain w
b =
  Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
intersection
    (Integer -> Tnum -> Domain w
forall (w :: Nat). Integer -> Tnum -> Domain w
fromTnum Integer
mask (Integer -> Tnum -> Tnum -> Tnum
Tnum.mulPrecise Integer
mask (Domain w -> Tnum
forall (w :: Nat). Domain w -> Tnum
toTnum Domain w
a) (Domain w -> Tnum
forall (w :: Nat). Domain w -> Tnum
toTnum Domain w
b)))
    (Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
mul Domain w
a Domain w
b)

-- | /O(w)/. Unsigned division via interval analysis on the quotient bounds.
-- Assumes the divisor is nonzero.
--
-- Captures known leading bits (both 0s and 1s) derived from
-- @[aMin \`quot\` bMax, aMax \`quot\` bMin]@. When the divisor is a known
-- power of two, the result is exact (bit-level structure of the dividend
-- is preserved, e.g.\ @udiv (any w) (singleton w (2^k))@ has its top @k@
-- bits known zero). 'udivPrecise' is strictly more precise; this is the
-- cheaper alternative when middle-bit precision doesn't matter.
udiv :: Domain w -> Domain w -> Domain w
udiv :: forall (w :: Nat). Domain w -> Domain w -> Domain w
udiv a :: Domain w
a@(BVBitInterval Integer
mask Integer
_ Integer
_) Domain w
b =
  Integer -> Tnum -> Domain w
forall (w :: Nat). Integer -> Tnum -> Domain w
fromTnum Integer
mask (Integer -> Tnum -> Tnum -> Tnum
Tnum.udiv Integer
mask (Domain w -> Tnum
forall (w :: Nat). Domain w -> Tnum
toTnum Domain w
a) (Domain w -> Tnum
forall (w :: Nat). Domain w -> Tnum
toTnum Domain w
b))

-- | /O(w)/. Unsigned remainder via leading-zero analysis. Assumes the divisor
-- is nonzero.
--
-- The result is bounded above by @min(aMax, bMax - 1)@; bits above that are
-- known zero. (The remainder's lower bound is trivially 0, so the same
-- interval-agreement analysis used in 'udiv' would not yield additional
-- leading bits here.) When the divisor is a known power of two,
-- @urem a (singleton w (2^k))@ is exactly the low @k@ bits of @a@.
urem :: Domain w -> Domain w -> Domain w
urem :: forall (w :: Nat). Domain w -> Domain w -> Domain w
urem a :: Domain w
a@(BVBitInterval Integer
mask Integer
_ Integer
_) Domain w
b =
  Integer -> Tnum -> Domain w
forall (w :: Nat). Integer -> Tnum -> Domain w
fromTnum Integer
mask (Integer -> Tnum -> Tnum -> Tnum
Tnum.urem Integer
mask (Domain w -> Tnum
forall (w :: Nat). Domain w -> Tnum
toTnum Domain w
a) (Domain w -> Tnum
forall (w :: Nat). Domain w -> Tnum
toTnum Domain w
b))

-- | /O(w²)/. Unsigned division combining abstract schoolbook long division
-- with the interval analysis of 'udiv'. Assumes the divisor is nonzero.
-- Strictly at least as precise as 'udiv'.
--
-- The result is the 'intersection' of 'udiv' (interval analysis on the
-- quotient bounds, plus an exact path for power-of-two divisors) and the
-- schoolbook result (which captures middle-bit structure that interval
-- analysis can't see, but joins through any undetermined comparison and so
-- loses on power-of-two divisors).
udivPrecise :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
udivPrecise :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
udivPrecise NatRepr w
w Domain w
a Domain w
b = Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
intersection ((Domain w, Domain w) -> Domain w
forall a b. (a, b) -> a
fst (NatRepr w -> Domain w -> Domain w -> (Domain w, Domain w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> (Domain w, Domain w)
longDivision NatRepr w
w Domain w
a Domain w
b)) (Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
udiv Domain w
a Domain w
b)

-- | /O(w²)/. Unsigned remainder combining schoolbook long division with the
-- leading-zero analysis of 'urem'. Assumes the divisor is nonzero. Strictly
-- at least as precise as 'urem'.
uremPrecise :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
uremPrecise :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
uremPrecise NatRepr w
w Domain w
a Domain w
b = Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
intersection ((Domain w, Domain w) -> Domain w
forall a b. (a, b) -> b
snd (NatRepr w -> Domain w -> Domain w -> (Domain w, Domain w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> (Domain w, Domain w)
longDivision NatRepr w
w Domain w
a Domain w
b)) (Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
urem Domain w
a Domain w
b)

-- | Abstract schoolbook long division: simultaneously computes the
-- quotient and remainder by walking the bits of the dividend from MSB to
-- LSB, maintaining a running partial remainder @r@ as a 'Domain'.
--
-- At each step, @r@ is shifted left and the next bit of the dividend is
-- shifted in. If @r >= b@ definitely, we subtract and set the corresponding
-- bit of the quotient. If @r < b@ definitely, we leave it. If the
-- comparison is undetermined, we union both possibilities into @r@ and
-- leave the quotient bit unknown.
longDivision :: forall w. (1 <= w) => NatRepr w -> Domain w -> Domain w -> (Domain w, Domain w)
longDivision :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> (Domain w, Domain w)
longDivision NatRepr w
w Domain w
a Domain w
b = Int -> Domain w -> Domain w -> (Domain w, Domain w)
go (NatRepr w -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr w
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (NatRepr w -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
0) (NatRepr w -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
0)
  where
  -- Loop from bit (w-1) down to 0. @q@ accumulates the quotient,
  -- @r@ is the partial remainder.
  go :: Int -> Domain w -> Domain w -> (Domain w, Domain w)
  go :: Int -> Domain w -> Domain w -> (Domain w, Domain w)
go Int
i Domain w
q Domain w
r
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     = (Domain w
q, Domain w
r)
    | Bool
otherwise =
        let r' :: Domain w
r'        = Domain w -> Maybe Bool -> Domain w
injectBit Domain w
r (Domain w -> Nat -> Maybe Bool
forall (w :: Nat). Domain w -> Nat -> Maybe Bool
testBit Domain w
a (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i))
            r'MinusB :: Domain w
r'MinusB  = Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
sub Domain w
r' Domain w
b
            (Domain w
q'', Domain w
r'')= case Domain w -> Domain w -> Maybe Bool
forall (w :: Nat). Domain w -> Domain w -> Maybe Bool
ult Domain w
r' Domain w
b of
              Just Bool
True  -> (Domain w
q,                       Domain w
r')
              Just Bool
False -> (Domain w -> Int -> Domain w
setBitDom Domain w
q Int
i,           Domain w
r'MinusB)
              Maybe Bool
Nothing    -> (Domain w -> Int -> Domain w
unknownBitDom Domain w
q Int
i,       Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
union Domain w
r' Domain w
r'MinusB)
        in Int -> Domain w -> Domain w -> (Domain w, Domain w)
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Domain w
q'' Domain w
r''

  -- Shift @r@ left by 1 and OR in a fresh low bit, whose value is
  -- determined by the @testBit@ result on the dividend.
  injectBit :: Domain w -> Maybe Bool -> Domain w
  injectBit :: Domain w -> Maybe Bool -> Domain w
injectBit Domain w
r Maybe Bool
mb =
    let r1 :: Domain w
r1 = NatRepr w -> Domain w -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
shl NatRepr w
w Domain w
r Integer
1
        bit_dom :: Domain w
bit_dom = case Maybe Bool
mb of
          Just Bool
True  -> NatRepr w -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
1
          Just Bool
False -> NatRepr w -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
0
          Maybe Bool
Nothing    -> NatRepr w -> Integer -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr w
w Integer
0 Integer
1
    in Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
or Domain w
r1 Domain w
bit_dom

  -- Set bit @i@ of a domain that is known to have bit @i@ = 0 going in
  -- (q starts at 0 and we only ever set bits, so this is safe).
  setBitDom :: Domain w -> Int -> Domain w
  setBitDom :: Domain w -> Int -> Domain w
setBitDom (BVBitInterval Integer
mask Integer
lo Integer
hi) Int
i =
    Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
Bits.setBit Integer
lo Int
i) (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
Bits.setBit Integer
hi Int
i)

  -- Mark bit @i@ of a domain as unknown.
  unknownBitDom :: Domain w -> Int -> Domain w
  unknownBitDom :: Domain w -> Int -> Domain w
unknownBitDom (BVBitInterval Integer
mask Integer
lo Integer
hi) Int
i =
    Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
lo (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
Bits.setBit Integer
hi Int
i)

-- | /O(w)/. Signed division (rounds toward zero). Assumes the divisor is
-- nonzero.
--
-- Implemented by splitting each operand on its sign bit into a non-negative
-- \"zero circle\" and a negative \"one circle\", applying 'udiv' to the
-- absolute values, fixing up the sign, and joining the resulting subcases.
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 = NatRepr w
-> (Domain w -> Domain w -> Domain w)
-> (Sign -> Sign -> Domain w -> Domain w)
-> Domain w
-> Domain w
-> Domain w
forall (w :: Nat).
(1 <= w) =>
NatRepr w
-> (Domain w -> Domain w -> Domain w)
-> (Sign -> Sign -> Domain w -> Domain w)
-> Domain w
-> Domain w
-> Domain w
signedOp NatRepr w
w Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
udiv Sign -> Sign -> Domain w -> Domain w
forall {a} {w :: Nat}. Eq a => a -> a -> Domain w -> Domain w
flipDiff
  where
  -- For sdiv, the result is negated iff the input signs differ.
  flipDiff :: a -> a -> Domain w -> Domain w
flipDiff a
sa a
sb Domain w
d = if a
sa a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
sb then Domain w
d else Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w
negate Domain w
d

-- | /O(w)/. Signed remainder (sign of dividend). Assumes the divisor is
-- nonzero.
--
-- Implemented like 'sdiv', except the result takes the sign of the dividend
-- rather than the XOR of the input signs. Additionally, leading bits of the
-- result are refined using magnitude bounds: if the dividend is non-negative,
-- the result has leading zeros from both the dividend and divisor magnitude;
-- if negative and nonzero, it has leading ones similarly.
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 = Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
meet Domain w
base Domain w
signMagnitudeBound
  where
  base :: Domain w
base = NatRepr w
-> (Domain w -> Domain w -> Domain w)
-> (Sign -> Sign -> Domain w -> Domain w)
-> Domain w
-> Domain w
-> Domain w
forall (w :: Nat).
(1 <= w) =>
NatRepr w
-> (Domain w -> Domain w -> Domain w)
-> (Sign -> Sign -> Domain w -> Domain w)
-> Domain w
-> Domain w
-> Domain w
signedOp NatRepr w
w Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
urem Sign -> Sign -> Domain w -> Domain w
forall {p} {w :: Nat}. Sign -> p -> Domain w -> Domain w
flipByDividend Domain w
a Domain w
b
  flipByDividend :: Sign -> p -> Domain w -> Domain w
flipByDividend Sign
SNeg p
_ Domain w
d = Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w
negate Domain w
d
  flipByDividend Sign
SNonneg p
_ Domain w
d = Domain w
d
  -- Sign/magnitude refinement (LLVM KnownBits::srem approach):
  -- (1) srem has the sign of the dividend (or is zero):
  --     x >= 0  ==>  x %$ y >= 0           (lemma_srem_nonneg_leading_zeros)
  --     x <  0  ==>  x %$ y <= 0           (lemma_srem_neg_sign)
  -- (2) |x %$ y| < |y|, so if |y| < 2^(w-k) then the result has at least
  --     k sign bits (lemma_srem_magnitude_bound). Similarly |x %$ y| <= |x|
  --     bounds the result by the dividend's magnitude.
  -- We take the max of both bounds to get the tightest leading-bit constraint.
  -- See @lemma_srem_*@ properties in bitsdomain.cry.
  mask :: Integer
mask = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w
  (Integer
alo, Integer
ahi) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
bitbounds Domain w
a
  (Integer
blo, Integer
bhi) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
bitbounds Domain w
b
  clzOf :: Integer -> Int
clzOf Integer
x = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (NatRepr w -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.clz NatRepr w
w Integer
x)
  -- countMinSignBits: minimum number of identical sign bits guaranteed in b.
  -- Non-negative: leading zeros come from hi (upper bound on set bits).
  -- Negative: leading ones come from lo (lower bound on set bits).
  bSignBits :: Int
bSignBits = case NatRepr w -> Domain w -> Maybe Sign
forall (w :: Nat). (1 <= w) => NatRepr w -> Domain w -> Maybe Sign
signOf NatRepr w
w Domain w
b of
    Just Sign
SNonneg -> Integer -> Int
clzOf Integer
bhi
    Just Sign
SNeg    -> Integer -> Int
clzOf (Integer
mask Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
blo)
    Maybe Sign
Nothing      -> Int
1
  signMagnitudeBound :: Domain w
signMagnitudeBound = case NatRepr w -> Domain w -> Maybe Sign
forall (w :: Nat). (1 <= w) => NatRepr w -> Domain w -> Maybe Sign
signOf NatRepr w
w Domain w
a of
    Just Sign
SNonneg ->
      let leadZ :: Int
leadZ = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Integer -> Int
clzOf Integer
ahi) Int
bSignBits
          hi' :: Integer
hi' = Integer
mask Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
leadZ
      in Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
0 Integer
hi'
    Just Sign
SNeg
      | Bool -> Bool
Prelude.not (Domain w -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain w
base Integer
0) ->
          let leadO :: Int
leadO = Integer -> Int
clzOf (Integer
mask Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
alo)
              leading :: Int
leading = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
leadO Int
bSignBits
              lo' :: Integer
lo' = Integer -> Integer
forall a. Bits a => a -> a
complement (Integer
mask Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
leading) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask
          in Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
lo' Integer
mask
    Maybe Sign
_ -> Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
0 Integer
mask

-- | Helper for signed div/rem: split each operand on its sign bit,
--   call the unsigned operation on the absolute values, fix up the
--   result's sign per the operation's rule, and union all subcases.
signedOp ::
  (1 <= w) =>
  NatRepr w ->
  (Domain w -> Domain w -> Domain w) {- ^ unsigned op on absolute values -} ->
  (Sign -> Sign -> Domain w -> Domain w) {- ^ result fix-up given signs -} ->
  Domain w -> Domain w ->
  Domain w
signedOp :: forall (w :: Nat).
(1 <= w) =>
NatRepr w
-> (Domain w -> Domain w -> Domain w)
-> (Sign -> Sign -> Domain w -> Domain w)
-> Domain w
-> Domain w
-> Domain w
signedOp NatRepr w
w Domain w -> Domain w -> Domain w
uop Sign -> Sign -> Domain w -> Domain w
fixup Domain w
a Domain w
b =
  (Domain w -> Domain w -> Domain w) -> [Domain w] -> Domain w
forall a. (a -> a -> a) -> [a] -> a
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
Prelude.foldr1 Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
union
    [ Sign -> Sign -> Domain w -> Domain w
fixup Sign
sa Sign
sb (Domain w -> Domain w -> Domain w
uop (Sign -> Domain w -> Domain w
forall {w :: Nat}. Sign -> Domain w -> Domain w
absVal Sign
sa Domain w
a') (Sign -> Domain w -> Domain w
forall {w :: Nat}. Sign -> Domain w -> Domain w
absVal Sign
sb Domain w
b'))
    | (Sign
sa, Domain w
a') <- NatRepr w -> Domain w -> [(Sign, Domain w)]
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> [(Sign, Domain w)]
splitSign NatRepr w
w Domain w
a
    , (Sign
sb, Domain w
b') <- NatRepr w -> Domain w -> [(Sign, Domain w)]
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> [(Sign, Domain w)]
splitSign NatRepr w
w Domain w
b
    ]
  where
  absVal :: Sign -> Domain w -> Domain w
absVal Sign
SNonneg Domain w
d = Domain w
d
  absVal Sign
SNeg    Domain w
d = Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w
negate Domain w
d

data Sign = SNonneg | SNeg
  deriving Sign -> Sign -> Bool
(Sign -> Sign -> Bool) -> (Sign -> Sign -> Bool) -> Eq Sign
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Sign -> Sign -> Bool
== :: Sign -> Sign -> Bool
$c/= :: Sign -> Sign -> Bool
/= :: Sign -> Sign -> Bool
Eq

-- | If the sign bit is known, return its value; otherwise 'Nothing'.
signOf :: (1 <= w) => NatRepr w -> Domain w -> Maybe Sign
signOf :: forall (w :: Nat). (1 <= w) => NatRepr w -> Domain w -> Maybe Sign
signOf NatRepr w
w Domain w
d =
  case Domain w -> Nat -> Maybe Bool
forall (w :: Nat). Domain w -> Nat -> Maybe Bool
testBit Domain w
d (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral (NatRepr w -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr w
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)) of
    Just Bool
True  -> Sign -> Maybe Sign
forall a. a -> Maybe a
Just Sign
SNeg
    Just Bool
False -> Sign -> Maybe Sign
forall a. a -> Maybe a
Just Sign
SNonneg
    Maybe Bool
Nothing    -> Maybe Sign
forall a. Maybe a
Nothing

-- | Split a domain on its sign bit, returning each restriction tagged with
--   its sign. If the sign bit is already known, returns a singleton list.
splitSign :: (1 <= w) => NatRepr w -> Domain w -> [(Sign, Domain w)]
splitSign :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> [(Sign, Domain w)]
splitSign NatRepr w
w d :: Domain w
d@(BVBitInterval Integer
mask Integer
lo Integer
hi) =
  case NatRepr w -> Domain w -> Maybe Sign
forall (w :: Nat). (1 <= w) => NatRepr w -> Domain w -> Maybe Sign
signOf NatRepr w
w Domain w
d of
    Just Sign
s  -> [(Sign
s, Domain w
d)]
    Maybe Sign
Nothing -> [ (Sign
SNonneg, Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask Integer
lo (Integer
hi Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
signbit))
               , (Sign
SNeg,    Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVBitInterval Integer
mask (Integer
lo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
signbit) Integer
hi)
               ]
  where
  signbit :: Integer
signbit = NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
signBit NatRepr w
w

-- | /O(w)/. Like 'udiv', but using the SMT-LIB @FixedSizeBitVectors@ theory's
-- div-by-zero semantics: @bvudiv s 0@ is the all-ones bitvector. See @Note
-- [SMT-LIB division]@ in "What4.Interface" for the design rationale.
udivSmtlib :: (1 <= w) => Domain w -> Domain w -> Domain w
udivSmtlib :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
udivSmtlib Domain w
a Domain w
b
  | Just Integer
0 <- Domain w -> Maybe Integer
forall (w :: Nat). Domain w -> Maybe Integer
asSingleton Domain w
b = Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Domain w
mkSingleton Integer
mask Integer
mask
  | Domain w -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain w
b Integer
0              = Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
union (Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
udiv Domain w
a Domain w
b) (Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Domain w
mkSingleton Integer
mask Integer
mask)
  | Bool
otherwise               = Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
udiv Domain w
a Domain w
b
  where
  mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a

-- | /O(w)/. Like 'urem', but using the SMT-LIB @FixedSizeBitVectors@ theory's
-- div-by-zero semantics: @bvurem s 0@ is the dividend itself (@s@). See @Note
-- [SMT-LIB division]@ in "What4.Interface" for the design rationale.
uremSmtlib :: (1 <= w) => Domain w -> Domain w -> Domain w
uremSmtlib :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
uremSmtlib Domain w
a Domain w
b
  | Just Integer
0 <- Domain w -> Maybe Integer
forall (w :: Nat). Domain w -> Maybe Integer
asSingleton Domain w
b = Domain w
a
  | Domain w -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain w
b Integer
0              = Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
union (Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
urem Domain w
a Domain w
b) Domain w
a
  | Bool
otherwise               = Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
urem Domain w
a Domain w
b

-- | /O(w)/. Like 'sdiv', but using the SMT-LIB QF_BV logic's div-by-zero
-- convention: @bvsdiv s 0@ is all-ones when @s@ is non-negative and @1@ when
-- @s@ is negative. See @Note [SMT-LIB division]@ in "What4.Interface" for the
-- design rationale.
sdivSmtlib :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
sdivSmtlib :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
sdivSmtlib NatRepr w
w Domain w
a Domain w
b
  | Just Integer
0 <- Domain w -> Maybe Integer
forall (w :: Nat). Domain w -> Maybe Integer
asSingleton Domain w
b = NatRepr w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => NatRepr w -> Domain w -> Domain w
sdivByZero NatRepr w
w Domain w
a
  | Domain w -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain w
b Integer
0              = Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
union (NatRepr w -> Domain w -> Domain w -> Domain w
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
sdiv NatRepr w
w Domain w
a Domain w
b) (NatRepr w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => NatRepr w -> Domain w -> Domain w
sdivByZero NatRepr w
w Domain w
a)
  | Bool
otherwise               = NatRepr w -> Domain w -> Domain w -> Domain w
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
sdiv NatRepr w
w Domain w
a Domain w
b

-- | The result of @bvsdiv s 0@ as a function of @s@'s sign: all-ones when @s >=
--   0@, @1@ when @s < 0@.
sdivByZero :: (1 <= w) => NatRepr w -> Domain w -> Domain w
sdivByZero :: forall (w :: Nat). (1 <= w) => NatRepr w -> Domain w -> Domain w
sdivByZero NatRepr w
w Domain w
a =
  case NatRepr w -> Domain w -> Maybe Sign
forall (w :: Nat). (1 <= w) => NatRepr w -> Domain w -> Maybe Sign
signOf NatRepr w
w Domain w
a of
    Just Sign
SNonneg -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Domain w
mkSingleton Integer
mask Integer
mask
    Just Sign
SNeg    -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Domain w
mkSingleton Integer
mask Integer
1
    Maybe Sign
Nothing      -> Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
union (Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Domain w
mkSingleton Integer
mask Integer
1) (Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Domain w
mkSingleton Integer
mask Integer
mask)
  where
  mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a

-- | /O(w)/. Like 'srem', but using the SMT-LIB QF_BV logic's div-by-zero
-- convention: @bvsrem s 0@ is the dividend itself (@s@). See @Note [SMT-LIB
-- division]@ in "What4.Interface" for the design rationale.
sremSmtlib :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
sremSmtlib :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
sremSmtlib NatRepr w
w Domain w
a Domain w
b
  | Just Integer
0 <- Domain w -> Maybe Integer
forall (w :: Nat). Domain w -> Maybe Integer
asSingleton Domain w
b = Domain w
a
  | Domain w -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain w
b Integer
0              = Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
union (NatRepr w -> Domain w -> Domain w -> Domain w
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
srem NatRepr w
w Domain w
a Domain w
b) Domain w
a
  | Bool
otherwise               = NatRepr w -> Domain w -> Domain w -> Domain w
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
srem NatRepr w
w Domain w
a Domain w
b


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

-- | Check that a domain is proper, and that
--   the given value is a member
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 = 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 :: forall (n :: Nat). (1 <= n) => 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 :: forall (n :: Nat).
(1 <= n) =>
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 :: forall (n :: Nat). 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

-- | If 'domainsOverlap' returns 'True', then a shared witness exists
-- at the bitwise OR of the two low masks.
correct_overlap_inv :: Domain n -> Domain n -> Property
correct_overlap_inv :: forall (n :: Nat). Domain n -> Domain n -> Property
correct_overlap_inv Domain n
a Domain n
b =
  Domain n -> Domain n -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
domainsOverlap Domain n
a Domain n
b Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> (Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
witness Bool -> Bool -> Bool
&& Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
witness)
  where
    (Integer
alo, Integer
_) = Domain n -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
bitbounds Domain n
a
    (Integer
blo, Integer
_) = Domain n -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
bitbounds Domain n
b
    witness :: Integer
witness  = Integer
alo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
Bits..|. Integer
blo

correct_asSingleton :: (1 <= n) => NatRepr n -> Domain n -> Property
correct_asSingleton :: forall (n :: Nat). (1 <= n) => NatRepr n -> Domain n -> Property
correct_asSingleton NatRepr n
n Domain n
a =
  case Domain n -> Maybe Integer
forall (w :: Nat). Domain w -> Maybe Integer
asSingleton Domain n
a of
    Just Integer
x -> Bool -> Property
property (Domain n
a Domain n -> Domain n -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Integer -> Domain n
forall (w :: Nat). NatRepr w -> Integer -> Domain w
singleton NatRepr n
n Integer
x)
    Maybe Integer
Nothing -> Bool -> Property
property Bool
True

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 =
  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 :: forall (n :: Nat).
(1 <= n) =>
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_join :: (1 <= n) => NatRepr n -> Domain n -> Domain n -> Integer -> Property
correct_join :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Domain n -> Domain n -> Integer -> Property
correct_join 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
join Domain n
a Domain n
b) Integer
x

correct_meet :: (1 <= n) => Domain n -> Domain n -> Integer -> Property
correct_meet :: forall (n :: Nat).
(1 <= n) =>
Domain n -> Domain n -> Integer -> Property
correct_meet 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 -> 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
meet Domain n
a Domain n
b) Integer
x

-- | Precision of meet: if @x@ is a member of @meet a b@, then @x@ is
-- a member of both @a@ and @b@.
precise_meet :: (1 <= n) => Domain n -> Domain n -> Integer -> Property
precise_meet :: forall (n :: Nat).
(1 <= n) =>
Domain n -> Domain n -> Integer -> Property
precise_meet Domain n
a Domain n
b Integer
x =
  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
meet Domain n
a 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
a Integer
x Bool -> Bool -> Bool
&& Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
x)

correct_leq :: Domain n -> Domain n -> Integer -> Property
correct_leq :: forall (n :: Nat). Domain n -> Domain n -> Integer -> Property
correct_leq Domain n
a Domain n
b Integer
x =
  (Domain n -> Domain n -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
leq Domain n
a Domain n
b Bool -> Bool -> Bool
&& 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
==> Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
x

------------------------------------------------------------------------
-- Lattice law properties (semantic, i.e. same set of members)

join_commutative :: Domain n -> Domain n -> Integer -> Property
join_commutative :: forall (n :: Nat). Domain n -> Domain n -> Integer -> Property
join_commutative Domain n
a Domain n
b Integer
x =
  Bool -> Property
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
join Domain n
a Domain n
b) Integer
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== 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
join Domain n
b Domain n
a) Integer
x)

join_idempotent :: Domain n -> Integer -> Property
join_idempotent :: forall (n :: Nat). Domain n -> Integer -> Property
join_idempotent Domain n
a Integer
x =
  Bool -> Property
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
join Domain n
a Domain n
a) Integer
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x)

meet_commutative :: Domain n -> Domain n -> Integer -> Property
meet_commutative :: forall (n :: Nat). Domain n -> Domain n -> Integer -> Property
meet_commutative Domain n
a Domain n
b Integer
x =
  Bool -> Property
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
meet Domain n
a Domain n
b) Integer
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== 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
meet Domain n
b Domain n
a) Integer
x)

meet_idempotent :: Domain n -> Integer -> Property
meet_idempotent :: forall (n :: Nat). Domain n -> Integer -> Property
meet_idempotent Domain n
a Integer
x =
  Bool -> Property
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
meet Domain n
a Domain n
a) Integer
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x)

join_top :: NatRepr n -> Domain n -> Integer -> Property
join_top :: forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Property
join_top NatRepr n
n Domain n
a Integer
x =
  Bool -> Property
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
join Domain n
a (NatRepr n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w
top NatRepr n
n)) Integer
x)

join_bottom :: NatRepr n -> Domain n -> Integer -> Property
join_bottom :: forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Property
join_bottom NatRepr n
n Domain n
a Integer
x =
  Bool -> Property
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
join Domain n
a (NatRepr n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w
bottom NatRepr n
n)) Integer
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x)

meet_top :: NatRepr n -> Domain n -> Integer -> Property
meet_top :: forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Property
meet_top NatRepr n
n Domain n
a Integer
x =
  Bool -> Property
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
meet Domain n
a (NatRepr n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w
top NatRepr n
n)) Integer
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x)

meet_bottom :: NatRepr n -> Domain n -> Integer -> Property
meet_bottom :: forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Property
meet_bottom NatRepr n
n Domain n
a Integer
x =
  Bool -> Property
property (Bool -> Bool
Prelude.not (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
meet Domain n
a (NatRepr n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w
bottom NatRepr n
n)) Integer
x))

leq_reflexive :: Domain n -> Property
leq_reflexive :: forall (n :: Nat). Domain n -> Property
leq_reflexive Domain n
a = Bool -> Property
property (Domain n -> Domain n -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
leq Domain n
a Domain n
a)

leq_transitive :: Domain n -> Domain n -> Domain n -> Property
leq_transitive :: forall (n :: Nat). Domain n -> Domain n -> Domain n -> Property
leq_transitive Domain n
a Domain n
b Domain n
c =
  (Domain n -> Domain n -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
leq Domain n
a Domain n
b Bool -> Bool -> Bool
&& Domain n -> Domain n -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
leq Domain n
b Domain n
c) Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Domain n -> Domain n -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
leq Domain n
a Domain n
c

meet_lower_bound :: Domain n -> Domain n -> Property
meet_lower_bound :: forall (n :: Nat). Domain n -> Domain n -> Property
meet_lower_bound Domain n
a Domain n
b = Bool -> Property
property (Domain n -> Domain n -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
leq (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
meet Domain n
a Domain n
b) Domain n
a)

join_upper_bound :: Domain n -> Domain n -> Property
join_upper_bound :: forall (n :: Nat). Domain n -> Domain n -> Property
join_upper_bound Domain n
a Domain n
b = Bool -> Property
property (Domain n -> Domain n -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
leq Domain n
a (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
join Domain n
a Domain n
b))

join_monotone :: Domain n -> Domain n -> Domain n -> Property
join_monotone :: forall (n :: Nat). Domain n -> Domain n -> Domain n -> Property
join_monotone Domain n
a Domain n
b Domain n
c =
  Domain n -> Domain n -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
leq Domain n
a Domain n
b Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Domain n -> Domain n -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
leq (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
join Domain n
a Domain n
c) (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
join Domain n
b Domain n
c)

meet_monotone :: Domain n -> Domain n -> Domain n -> Property
meet_monotone :: forall (n :: Nat). Domain n -> Domain n -> Domain n -> Property
meet_monotone Domain n
a Domain n
b Domain n
c =
  Domain n -> Domain n -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
leq Domain n
a Domain n
b Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Domain n -> Domain n -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
leq (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
meet Domain n
a Domain n
c) (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
meet Domain n
b Domain n
c)

join_associative :: Domain n -> Domain n -> Domain n -> Integer -> Property
join_associative :: forall (n :: Nat).
Domain n -> Domain n -> Domain n -> Integer -> Property
join_associative Domain n
a Domain n
b Domain n
c Integer
x =
  Bool -> Property
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
join (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
join Domain n
a Domain n
b) Domain n
c) Integer
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== 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
join Domain n
a (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
join Domain n
b Domain n
c)) Integer
x)

meet_associative :: Domain n -> Domain n -> Domain n -> Integer -> Property
meet_associative :: forall (n :: Nat).
Domain n -> Domain n -> Domain n -> Integer -> Property
meet_associative Domain n
a Domain n
b Domain n
c Integer
x =
  Bool -> Property
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
meet (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
meet Domain n
a Domain n
b) Domain n
c) Integer
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== 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
meet Domain n
a (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
meet Domain n
b Domain n
c)) Integer
x)

join_absorb :: Domain n -> Domain n -> Integer -> Property
join_absorb :: forall (n :: Nat). Domain n -> Domain n -> Integer -> Property
join_absorb Domain n
a Domain n
b Integer
x =
  Bool -> Property
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
join Domain n
a (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
meet Domain n
a Domain n
b)) Integer
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x)

meet_absorb :: Domain n -> Domain n -> Integer -> Property
meet_absorb :: forall (n :: Nat). Domain n -> Domain n -> Integer -> Property
meet_absorb Domain n
a Domain n
b Integer
x =
  Bool -> Property
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
meet Domain n
a (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
join Domain n
a Domain n
b)) Integer
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x)

join_proper :: (1 <= n) => NatRepr n -> Domain n -> Domain n -> Property
join_proper :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Domain n -> Domain n -> Property
join_proper NatRepr n
n Domain n
a Domain n
b = Bool -> Property
property (NatRepr n -> Domain n -> Bool
forall (w :: Nat). NatRepr w -> Domain w -> Bool
proper NatRepr n
n (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
join Domain n
a Domain n
b))

meet_proper :: (1 <= n) => NatRepr n -> Domain n -> Domain n -> Property
meet_proper :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Domain n -> Domain n -> Property
meet_proper NatRepr n
n Domain n
a Domain n
b = Bool -> Property
property (NatRepr n -> Domain n -> Bool
forall (w :: Nat). NatRepr w -> Domain w -> Bool
proper NatRepr n
n Domain n
c Bool -> Bool -> Bool
|| Domain n -> Bool
forall (w :: Nat). Domain w -> Bool
isBottom Domain n
c)
  where c :: Domain n
c = Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
meet Domain n
a Domain n
b

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 = 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 :: 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 = 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 :: 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) = 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 :: 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) = 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 :: forall (n :: Nat) (w :: Nat).
(n <= w) =>
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 :: 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) = 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 :: 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) =
  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 :: forall (n :: Nat).
(1 <= n) =>
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 :: forall (n :: Nat).
(1 <= n) =>
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 :: forall (n :: Nat).
(1 <= n) =>
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 :: forall (n :: Nat).
(1 <= n) =>
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 :: forall (n :: Nat).
(1 <= n) =>
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_shlAbstract ::
  (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_shlAbstract :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_shlAbstract 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 (NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
shlAbstract NatRepr n
n Domain n
a Domain n
b) 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) (NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y))

correct_lshrAbstract ::
  (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_lshrAbstract :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_lshrAbstract 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 (NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
lshrAbstract NatRepr n
n Domain n
a Domain n
b) 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) (NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y))

correct_ashrAbstract ::
  (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_ashrAbstract :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_ashrAbstract 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 (NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
ashrAbstract NatRepr n
n Domain n
a Domain n
b) 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) (NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y))

correct_rolAbstract ::
  (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_rolAbstract :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_rolAbstract 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 (NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
rolAbstract NatRepr n
n Domain n
a Domain n
b) (NatRepr n -> Integer -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateLeft NatRepr n
n Integer
x (NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y))

correct_rorAbstract ::
  (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_rorAbstract :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_rorAbstract 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 (NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
rorAbstract NatRepr n
n Domain n
a Domain n
b) (NatRepr n -> Integer -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateRight NatRepr n
n Integer
x (NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y))

-- | The optimized 'shlAbstract' produces the same domain as the
-- declarative 'shlAbstractSpec'. Together with 'correct_shlAbstract',
-- this proves 'shlAbstract' is point-wise optimal at this domain.
correct_equiv_shlAbstract ::
  (1 <= n) => NatRepr n -> Domain n -> Domain n -> Property
correct_equiv_shlAbstract :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Domain n -> Domain n -> Property
correct_equiv_shlAbstract NatRepr n
n Domain n
a Domain n
b =
  Bool -> Property
property (NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
shlAbstract NatRepr n
n Domain n
a Domain n
b Domain n -> Domain n -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
shlAbstractSpec NatRepr n
n Domain n
a Domain n
b)

correct_equiv_lshrAbstract ::
  (1 <= n) => NatRepr n -> Domain n -> Domain n -> Property
correct_equiv_lshrAbstract :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Domain n -> Domain n -> Property
correct_equiv_lshrAbstract NatRepr n
n Domain n
a Domain n
b =
  Bool -> Property
property (NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
lshrAbstract NatRepr n
n Domain n
a Domain n
b Domain n -> Domain n -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
lshrAbstractSpec NatRepr n
n Domain n
a Domain n
b)

correct_equiv_ashrAbstract ::
  (1 <= n) => NatRepr n -> Domain n -> Domain n -> Property
correct_equiv_ashrAbstract :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Domain n -> Domain n -> Property
correct_equiv_ashrAbstract NatRepr n
n Domain n
a Domain n
b =
  Bool -> Property
property (NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
ashrAbstract NatRepr n
n Domain n
a Domain n
b Domain n -> Domain n -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
ashrAbstractSpec NatRepr n
n Domain n
a Domain n
b)

correct_equiv_rolAbstract ::
  (1 <= n) => NatRepr n -> Domain n -> Domain n -> Property
correct_equiv_rolAbstract :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Domain n -> Domain n -> Property
correct_equiv_rolAbstract NatRepr n
n Domain n
a Domain n
b =
  Bool -> Property
property (NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
rolAbstract NatRepr n
n Domain n
a Domain n
b Domain n -> Domain n -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
rolAbstractSpec NatRepr n
n Domain n
a Domain n
b)

correct_equiv_rorAbstract ::
  (1 <= n) => NatRepr n -> Domain n -> Domain n -> Property
correct_equiv_rorAbstract :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Domain n -> Domain n -> Property
correct_equiv_rorAbstract NatRepr n
n Domain n
a Domain n
b =
  Bool -> Property
property (NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
rorAbstract NatRepr n
n Domain n
a Domain n
b Domain n -> Domain n -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat). NatRepr w -> Domain w -> Domain w -> Domain w
rorAbstractSpec NatRepr n
n Domain n
a Domain n
b)

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

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) = 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
==> Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
x' Bool -> Bool -> Bool
&& Integer
x' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
hi
  where
  x' :: Integer
x' = NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x
  (Integer
lo, Integer
hi) = Domain n -> (Integer, Integer)
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) = 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
==> Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
x' Bool -> Bool -> Bool
&& Integer
x' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
hi
  where
  x' :: Integer
x' = NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x
  (Integer
lo, Integer
hi) = NatRepr n -> Domain n -> (Integer, Integer)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> (Integer, Integer)
sbounds NatRepr n
n Domain n
a

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) =
  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
ult 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. Ord 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. Ord 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_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) =
  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 NatRepr n -> Domain n -> Domain n -> Maybe Bool
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  -> NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y
      Just Bool
False -> NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y
      Maybe Bool
Nothing    -> Bool
True

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) = 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
add Domain n
a Domain n
b) (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y)

correct_sub :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_sub :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_sub 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
sub Domain n
a Domain n
b) (Integer
x Integer -> Integer -> Integer
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) = 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
negate Domain n
a) (Integer -> Integer
forall a. Num a => a -> a
Prelude.negate Integer
x)

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) = 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 (Integer -> Domain n -> Domain n
forall (w :: Nat). Integer -> Domain w -> Domain w
scale Integer
k' Domain n
a) (Integer
k' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
x)
  where
  k' :: Integer
k' = NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
k

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) = 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
mul Domain n
a Domain n
b) (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y)

correct_mulPrecise :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_mulPrecise :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_mulPrecise 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
mulPrecise Domain n
a Domain n
b) (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y)

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) =
  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 -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 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
udiv Domain n
a Domain n
b) (Integer
x' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` 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_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) =
  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 -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 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
urem Domain n
a Domain n
b) (Integer
x' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` 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_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) =
  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 -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 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 -> Domain n -> Domain 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' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
y')
  where
  x' :: Integer
x' = NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x
  y' :: Integer
y' = NatRepr n -> Integer -> Integer
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) =
  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 -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 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 -> Domain n -> Domain 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' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
y')
  where
  x' :: Integer
x' = NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x
  y' :: Integer
y' = NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y

correct_udivPrecise :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_udivPrecise :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_udivPrecise 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 -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 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 -> Domain n -> Domain n
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
udivPrecise NatRepr n
n Domain n
a Domain n
b) (Integer
x' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` 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_uremPrecise :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_uremPrecise :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_uremPrecise 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 -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 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 -> Domain n -> Domain n
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
uremPrecise NatRepr n
n Domain n
a Domain n
b) (Integer
x' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` 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_udivSmtlib ::
  (1 <= n) =>
  NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_udivSmtlib :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_udivSmtlib 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). (1 <= w) => Domain w -> Domain w -> Domain w
udivSmtlib Domain n
a Domain n
b)
      (if Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then NatRepr n -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr n
n else Integer
x' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` 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_uremSmtlib ::
  (1 <= n) =>
  NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_uremSmtlib :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_uremSmtlib 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). (1 <= w) => Domain w -> Domain w -> Domain w
uremSmtlib Domain n
a Domain n
b) (if Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Integer
x' else Integer
x' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` 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_sdivSmtlib ::
  (1 <= n) =>
  NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_sdivSmtlib :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_sdivSmtlib 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 (NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
sdivSmtlib NatRepr n
n Domain n
a Domain n
b) Integer
result
  where
  x' :: Integer
x' = NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x
  y' :: Integer
y' = NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y
  result :: Integer
result
    | Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0   = Integer
x' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
y'
    | Integer
x' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0   = NatRepr n -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr n
n
    | Bool
otherwise = Integer
1

correct_sremSmtlib ::
  (1 <= n) =>
  NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_sremSmtlib :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_sremSmtlib 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 (NatRepr n -> Domain n -> Domain n -> Domain n
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
sremSmtlib NatRepr n
n Domain n
a Domain n
b) (if Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Integer
x' else Integer
x' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
y')
  where
  x' :: Integer
x' = NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x
  y' :: Integer
y' = NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y