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

Provides an interval-based implementation of bitvector abstract
domains.
-}

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

module What4.Domains.BV.Arith
  ( Domain(..)
  , proper
  , bvdMask
  , member
  , pmember
  , interval
  , size
  -- * Projection functions
  , asSingleton
  , ubounds
  , sbounds
  , eq
  , slt
  , ult
  , isUltSumCommonEquiv
  , domainsOverlap
  , arithDomainData
  , bitbounds
  , unknowns
  , fillright
  -- * Lattice operations
  , top
  , any
  , bottom
  , isBottom
  , join
  , union
  , meet
  , leq
    -- * Operations
  , singleton
  , range
  , fromAscEltList
  , concat
  , select
  , zext
  , sext
    -- ** Shifts
  , shl
  , lshr
  , ashr
    -- ** Arithmetic
  , add
  , negate
  , scale
  , mul
  , udiv
  , urem
  , sdiv
  , srem
    -- ** Arithmetic (SMT-LIB div-by-zero semantics)
  , udivSmtlib
  , uremSmtlib
  , sdivSmtlib
  , sremSmtlib
    -- ** Bitwise
  , What4.Domains.BV.Arith.not

  -- * Correctness properties
  , genDomain
  , genElement
  , genPair
  , correct_any
  , correct_ubounds
  , correct_sbounds
  , correct_singleton
  , correct_overlap
  , correct_overlap_inv
  , correct_asSingleton
  , correct_mulRange
  , correct_union
  , correct_join
  , correct_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
  , join_upper_bound
  , join_proper
  , meet_proper
  , correct_zero_ext
  , correct_sign_ext
  , correct_concat
  , correct_shrink
  , correct_trunc
  , correct_select
  , correct_add
  , correct_neg
  , correct_mul
  , correct_scale
  , correct_scale_eq
  , correct_udiv
  , correct_urem
  , correct_sdivRange
  , correct_shrinkRange
  , correct_sdiv
  , correct_srem
  , correct_udivSmtlib
  , correct_uremSmtlib
  , correct_sdivSmtlib
  , correct_sremSmtlib
  , correct_not
  , correct_shl
  , correct_lshr
  , correct_ashr
  , correct_eq
  , correct_ult
  , correct_slt
  , correct_isUltSumCommonEquiv
  , correct_unknowns
  , correct_bitbounds
  ) where

import qualified Data.Bits as Bits
import           Data.Bits hiding (testBit, xor)
import           Data.Parameterized.NatRepr
import           GHC.TypeNats
import           GHC.Stack

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

import qualified What4.Domains.Arithmetic as Arith
import           What4.Domains.Verification ( Property, property, (==>), Gen, chooseInteger )

--------------------------------------------------------------------------------
-- BVDomain definition

-- | A value of type @'BVDomain' w@ represents a set of bitvectors of
-- width @w@. Each 'BVDomain' can represent a single contiguous
-- interval of bitvectors that may wrap around from -1 to 0.
data Domain (w :: Nat)
  = BVDAny !Integer
  -- ^ The set of all bitvectors of width @w@. Argument caches @2^w-1@.
  | BVDInterval !Integer !Integer !Integer
  -- ^ Intervals are represented by a starting value and a size.
  -- @BVDInterval mask l d@ represents the set of values of the form
  -- @x mod 2^w@ for @x@ such that @l <= x <= l + d@. It should
  -- satisfy the invariants @0 <= l < 2^w@ and @0 <= d < 2^w@. The
  -- first argument caches the value @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)

sameDomain :: Domain w -> Domain w -> Bool
sameDomain :: forall (w :: Nat). Domain w -> Domain w -> Bool
sameDomain (BVDAny Integer
_) (BVDAny Integer
_) = Bool
True
sameDomain (BVDInterval Integer
_ Integer
x Integer
w) (BVDInterval Integer
_ Integer
x' Integer
w') = Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
x' Bool -> Bool -> Bool
&& Integer
w Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
w'
sameDomain Domain w
_ Domain w
_ = Bool
False

-- | Compute how many concrete elements are in the abstract domain
size :: Domain w -> Integer
size :: forall (w :: Nat). Domain w -> Integer
size (BVDAny Integer
mask)        = Integer
mask Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
size (BVDInterval Integer
_ Integer
_ Integer
sz) = Integer
sz Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1

-- | 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 (BVDAny Integer
_) Integer
_ = Bool
True
member (BVDInterval Integer
mask Integer
lo Integer
sz) Integer
x = ((Integer
x' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lo) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
sz
  where x' :: Integer
x' = Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask

-- | Check 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 (BVDAny Integer
mask) = 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
proper NatRepr w
w (BVDInterval Integer
mask Integer
lo Integer
sz) =
  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
lo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
mask Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
mask Bool -> Bool -> Bool
&&
  Integer
sz Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
mask Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
mask Bool -> Bool -> Bool
&&
  Integer
sz Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
mask

-- | Return the bitvector mask value from this domain
bvdMask :: Domain w -> Integer
bvdMask :: forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
x =
  case Domain w
x of
    BVDAny Integer
mask -> Integer
mask
    BVDInterval Integer
mask Integer
_ Integer
_ -> Integer
mask

-- | Random generator for 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
sz <- (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
sz

-- | Generate a random element from a domain
genElement :: Domain w -> Gen Integer
genElement :: forall (w :: Nat). Domain w -> Gen Integer
genElement (BVDAny Integer
mask) = (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, Integer
mask)
genElement (BVDInterval Integer
mask Integer
lo Integer
sz) =
   do Integer
x <- (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, Integer
sz)
      Integer -> Gen Integer
forall a. a -> Gen a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
lo) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask)

-- | Generate a random 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)

--------------------------------------------------------------------------------

-- | @halfRange n@ returns @2^(n-1)@.
halfRange :: (1 <= w) => NatRepr w -> Integer
halfRange :: forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
halfRange 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)

--------------------------------------------------------------------------------
-- Projection functions

-- | Return value if this is a singleton.
asSingleton :: Domain w -> Maybe Integer
asSingleton :: forall (w :: Nat). Domain w -> Maybe Integer
asSingleton Domain w
x =
  case Domain w
x of
    BVDAny Integer
_ -> Maybe Integer
forall a. Maybe a
Nothing
    BVDInterval Integer
_ Integer
xl Integer
xd
      | Integer
xd Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
xl
      | Bool
otherwise -> Maybe Integer
forall a. Maybe a
Nothing

isSingletonZero :: Domain w -> Bool
isSingletonZero :: forall (w :: Nat). Domain w -> Bool
isSingletonZero Domain w
x =
  case Domain w
x of
    BVDInterval Integer
_ Integer
0 Integer
0 -> Bool
True
    Domain w
_ -> Bool
False

isBVDAny :: Domain w -> Bool
isBVDAny :: forall (w :: Nat). Domain w -> Bool
isBVDAny Domain w
x =
  case Domain w
x of
    BVDAny {} -> Bool
True
    BVDInterval {} -> Bool
False

-- | Return unsigned bounds for domain.
ubounds :: Domain w -> (Integer, Integer)
ubounds :: forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
a =
  case Domain w
a of
    BVDAny Integer
mask -> (Integer
0, Integer
mask)
    BVDInterval Integer
mask Integer
al Integer
aw
      | Integer
ah Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
mask -> (Integer
0, Integer
mask)
      | Bool
otherwise -> (Integer
al, Integer
ah)
      where ah :: Integer
ah = Integer
al Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
aw

-- | Return signed bounds for 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 Domain w
a = (Integer
lo Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
delta, Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
delta)
  where
    delta :: Integer
delta = NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
halfRange NatRepr w
w
    (Integer
lo, Integer
hi) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds (Domain w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
add Domain w
a (Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDInterval (Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a) Integer
delta Integer
0))

-- | Return the @(lo,sz)@, the low bound and size
--   of the given arithmetic interval.  A value @x@ is in
--   the set defined by this domain iff
--   @(x - lo) `mod` w <= sz@ holds.
--   Returns @Nothing@ if the domain contains all values.
arithDomainData :: Domain w -> Maybe (Integer, Integer)
arithDomainData :: forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
arithDomainData (BVDAny Integer
_) = Maybe (Integer, Integer)
forall a. Maybe a
Nothing
arithDomainData (BVDInterval Integer
_ Integer
al Integer
aw) = (Integer, Integer) -> Maybe (Integer, Integer)
forall a. a -> Maybe a
Just (Integer
al, Integer
aw)

-- | Return true if domains contain a common element.
domainsOverlap :: Domain w -> Domain w -> Bool
domainsOverlap :: forall (w :: Nat). Domain w -> Domain w -> Bool
domainsOverlap Domain w
a Domain w
b =
  case Domain w
a of
    BVDAny Integer
_ -> Bool
True
    BVDInterval Integer
_ Integer
al Integer
aw ->
      case Domain w
b of
        BVDAny Integer
_ -> Bool
True
        BVDInterval Integer
mask Integer
bl Integer
bw ->
          Integer
diff Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
bw Bool -> Bool -> Bool
|| Integer
diff Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
aw Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
mask
          where diff :: Integer
diff = (Integer
al Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
bl) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask

eq :: Domain w -> Domain w -> Maybe Bool
eq :: forall (w :: Nat). Domain w -> Domain w -> Maybe Bool
eq Domain w
a Domain w
b
  | Just Integer
x <- 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)
  | Domain w -> Domain w -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
domainsOverlap Domain w
a Domain w
b Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
False = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
  | Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing

-- | Check if all elements in one domain are less than all elements in 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
a_max Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
b_min = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
  | Integer
a_min Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
b_max = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
  | Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing
  where
    (Integer
a_min, Integer
a_max) = 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
b_min, Integer
b_max) = NatRepr w -> Domain w -> (Integer, Integer)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> (Integer, Integer)
sbounds NatRepr w
w Domain w
b

-- | Check if all elements in one domain are less than all elements in other.
ult :: (1 <= w) => Domain w -> Domain w -> Maybe Bool
ult :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Maybe Bool
ult Domain w
a Domain w
b
  | Integer
a_max Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
b_min = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
  | Integer
a_min Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
b_max = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
  | Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing
  where
    (Integer
a_min, Integer
a_max) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
a
    (Integer
b_min, Integer
b_max) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
b

-- | Check if @(bvult (bvadd a c) (bvadd b c))@ is equivalent to @(bvult a b)@.
--
-- This is true if and only if for all natural values @i_a@, @i_b@, @i_c@ in
-- @a@, @b@, @c@, either both @i_a + i_c@ and @i_b + i_c@ are less than @2^w@,
-- or both are not. We prove this by contradiction. If @i_a = i_b@, then the
-- property is trivial. Assume that @i_a < i_b@. Then @i_a + i_c < i_b + i_c@.
-- If exactly one of the additions is less than @2^w@, it must be the case that
-- @i_a + i_c < 2^w@ and @0 <= i_b + i_c - 2^w < 2^w@. Since @i_b < 2^w@, it
-- follows that @i_b + i_c < 2^w + i_c@, that @i_b + i_c - 2^w < i_c@, and that
-- @i_b + i_c - 2^w < i_a + i_c@. Thus, for these values of @i_a@, @i_b@, @i_c@,
-- @(bvult a b)@ is true, but @(bvult (bvadd a c) (bvadd b c))@ is false, which
-- is a contradiction.
--
-- We check this property by case analysis on whether @c@ is a single
-- non-wrapping interval, or it wraps around and is a union of two non-wrapping
-- intervals. For a non-wrapping (sub)interval @c'@ of @c@, there are four
-- possible cases:
-- 1. @a@ and @b@ contain a single value.
-- 2. @(bvadd a c')@ and @(bvadd b c')@ do not wrap around for any values in
--    @a@, @b@, @c'@.
-- 3. @(bvadd a c')@ and @(bvadd b c')@ wrap around for all values in @a@, @b@,
--    @c'@.
--
-- This is used to simplify @bvult@.
isUltSumCommonEquiv :: Domain w -> Domain w -> Domain w -> Bool
isUltSumCommonEquiv :: forall (w :: Nat). Domain w -> Domain w -> Domain w -> Bool
isUltSumCommonEquiv Domain w
a Domain w
b Domain w
c = if Integer
al Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
ah Bool -> Bool -> Bool
&& Integer
bl Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
bh Bool -> Bool -> Bool
&& Integer
al Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
bl
  then Bool
True
  else if Integer
cl Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
cw Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
ch
    then Integer -> Integer -> Bool
checkSameWrapInterval Integer
cl Integer
ch
    else Integer -> Integer -> Bool
checkSameWrapInterval Integer
cl Integer
mask Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
checkSameWrapInterval Integer
0 Integer
ch
  where
    (Integer
mask, Integer
cl, Integer
cw) = case Domain w
c of
      BVDInterval Integer
mask' Integer
cl' Integer
cw' -> (Integer
mask', Integer
cl', Integer
cw')
      BVDAny Integer
mask' -> (Integer
mask', Integer
0, Integer
mask')
    ch :: Integer
ch = (Integer
cl Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
cw) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask
    (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
    checkSameWrapInterval :: Integer -> Integer -> Bool
checkSameWrapInterval Integer
lo Integer
hi =
      Integer
ah Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
hi Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
mask Bool -> Bool -> Bool
&& Integer
bh Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
hi Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
mask Bool -> Bool -> Bool
|| Integer
mask Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
al Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
lo Bool -> Bool -> Bool
&& Integer
mask Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
bl Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
lo

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

-- | Top element of the lattice: represents all bitvectors of width @w@.
top :: (1 <= w) => NatRepr w -> Domain w
top :: forall (w :: Nat). (1 <= w) => NatRepr w -> Domain w
top NatRepr w
w = Integer -> Domain w
forall (w :: Nat). Integer -> Domain w
BVDAny (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w)
{-# INLINE top #-}

-- | Represents all values.
{-# DEPRECATED any "Use 'top' instead" #-}
any :: (1 <= w) => NatRepr w -> Domain w
any :: forall (w :: Nat). (1 <= w) => NatRepr w -> Domain w
any = NatRepr w -> Domain w
forall (w :: Nat). (1 <= w) => NatRepr w -> Domain w
top
{-# INLINE any #-}

-- | Bottom element of the lattice for the given mask: represents the empty
-- set of bitvectors. This is an improper domain whose membership predicate
-- is unsatisfiable.
bottomForMask :: Integer -> Domain w
bottomForMask :: forall (w :: Nat). Integer -> Domain w
bottomForMask Integer
mask = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDInterval Integer
mask Integer
0 (-Integer
1)
{-# INLINE bottomForMask #-}

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

-- | Returns 'True' if this domain has no members (i.e., is 'bottom'),
--   detected as an improper interval with negative size.
isBottom :: Domain w -> Bool
isBottom :: forall (w :: Nat). Domain w -> Bool
isBottom (BVDInterval Integer
_ Integer
_ Integer
sz) = Integer
sz Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
isBottom (BVDAny Integer
_) = Bool
False

-- | Lattice join (least upper bound) of two domains.
-- If both inputs are proper (or bottom), so is the result.
--
-- For two non-bottom intervals, the result is the shortest single
-- interval containing both. The trick is to compare each interval's
-- \"average value\" @2*lo + sz@ (twice the midpoint, doubled to avoid
-- fractions). If the averages are more than half the modulus apart,
-- the inputs sit on opposite sides of zero, so we lift the smaller-
-- midpoint interval by @2^w@ before taking the enclosing range. This
-- yields the shorter of the two enclosing arcs — the one that wraps
-- around zero when appropriate — rather than always going clockwise.
-- 'interval' then collapses sizes @>= 2^w@ to 'BVDAny'.
--
-- @
--     Visualize the modular number line @[0, mask]@ as a horizontal strip.
--
--     midpoints close — naive convex hull is already optimal:
--            0                                     mask
--     a:     [-----]
--     b:               [-----]
--     naive: [---------------]   (= our result)
--
--     midpoints far apart — naive hull is wasteful, wrapping is shorter:
--            0                                     mask
--     a:     [-----]
--     b:                                   [-----]
--     naive: [-----------------------------------]   (covers nearly everything)
--     ours:  -----]                        [------   (wraps around; tight)
-- @
join :: (1 <= w) => Domain w -> Domain w -> Domain w
join :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
join Domain w
a Domain w
b | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isBottom Domain w
a = Domain w
b
         | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isBottom Domain w
b = Domain w
a
join a :: Domain w
a@BVDAny{} Domain w
_ = Domain w
a
join Domain w
_ b :: Domain w
b@BVDAny{} = Domain w
b
join (BVDInterval Integer
mask Integer
al Integer
aw) (BVDInterval Integer
_ Integer
bl Integer
bw) =
  Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
cl (Integer
ch Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
cl)
  where
    sz :: Integer
sz = Integer
mask Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
    ac :: Integer
ac = Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
al Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
aw -- twice the average value of a
    bc :: Integer
bc = Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
bl Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
bw -- twice the average value of b
    -- If the averages are 2^(w-1) or more apart,
    -- then shift the lower interval up by 2^w.
    al' :: Integer
al' = if Integer
ac Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
mask Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
bc then Integer
al Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
sz else Integer
al
    bl' :: Integer
bl' = if Integer
bc Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
mask Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
ac then Integer
bl Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
sz else Integer
bl
    ah' :: Integer
ah' = Integer
al' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
aw
    bh' :: Integer
bh' = Integer
bl' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
bw
    cl :: Integer
cl = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
al' Integer
bl'
    ch :: Integer
ch = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
ah' Integer
bh'

-- | Return union of two domains.
{-# DEPRECATED union "Use 'join' instead" #-}
union :: (1 <= w) => Domain w -> Domain w -> Domain w
union :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
union = Domain w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
join
{-# INLINE union #-}

-- | Lattice meet: an over-approximation of the intersection of two domains.
-- For any concrete value @x@, if @x@ is a member of both @a@ and @b@, then
-- @x@ is a member of @meet a b@.
-- If both inputs are proper (or bottom), so is the result.
meet :: (1 <= w) => Domain w -> Domain w -> Domain w
meet :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
meet Domain w
a Domain w
_ | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isBottom Domain w
a = Domain w
a
meet Domain w
_ Domain w
b | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isBottom Domain w
b = Domain w
b
meet (BVDAny Integer
_) Domain w
b = Domain w
b
meet Domain w
a (BVDAny Integer
_) = Domain w
a
meet Domain w
a Domain w
b
  | Domain w -> Domain w -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
sameDomain Domain w
a Domain w
b = Domain w
a
meet Domain w
a Domain w
b =
  let (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
      cl :: Integer
cl = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
al Integer
bl
      ch :: Integer
ch = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
ah Integer
bh
      mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
  in if Integer
cl Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
ch
     then Integer -> Domain w
forall (w :: Nat). Integer -> Domain w
bottomForMask Integer
mask
     else Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
cl (Integer
ch Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
cl)

-- | 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 Domain w
a Domain w
_ | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isBottom Domain w
a = Bool
True
leq Domain w
_ Domain w
b | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isBottom Domain w
b = Bool
False
leq Domain w
_ (BVDAny Integer
_) = Bool
True
leq (BVDAny Integer
_) (BVDInterval Integer
_ Integer
_ Integer
_) = Bool
False
leq (BVDInterval Integer
mask Integer
al Integer
aw) (BVDInterval Integer
_ Integer
bl Integer
bw) =
  ((Integer
al Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
bl) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
aw Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
bw
{-# INLINE leq #-}

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

-- | Create a bitvector domain representing the integer.
singleton :: (HasCallStack, 1 <= w) => NatRepr w -> Integer -> Domain w
singleton :: forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
x = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDInterval Integer
mask (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask) Integer
0
  where mask :: Integer
mask = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w

-- | @range w l u@ returns domain containing all bitvectors formed
-- from the @w@ low order bits of some @i@ in @[l,u]@.  Note that per
-- @testBit@, the least significant bit has index @0@.
range :: NatRepr w -> Integer -> Integer -> Domain w
range :: forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr w
w Integer
al Integer
ah = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
al ((Integer
ah Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
al) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask)
  where mask :: Integer
mask = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w

-- | Unsafe constructor for internal use only. Caller must ensure that
-- @mask = maxUnsigned w@, and that @aw@ is non-negative.
interval :: Integer -> Integer -> Integer -> Domain w
interval :: forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
al Integer
aw =
  if Integer
aw Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
mask then Integer -> Domain w
forall (w :: Nat). Integer -> Domain w
BVDAny Integer
mask else Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDInterval Integer
mask (Integer
al Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask) Integer
aw

-- | Create an abstract domain from an ascending list of elements.
-- The elements are assumed to be distinct.
fromAscEltList :: (1 <= w) => NatRepr w -> [Integer] -> Domain w
fromAscEltList :: forall (w :: Nat). (1 <= w) => NatRepr w -> [Integer] -> Domain w
fromAscEltList NatRepr w
w [] = NatRepr w -> Integer -> Domain w
forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
0
fromAscEltList NatRepr w
w [Integer
x] = NatRepr w -> Integer -> Domain w
forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
x
fromAscEltList NatRepr w
w (Integer
x0 : Integer
x1 : [Integer]
xs) = (Integer, Integer) -> (Integer, Integer) -> [Integer] -> Domain w
go (Integer
x0, Integer
x0) (Integer
x1, Integer
x1) [Integer]
xs
  where
    -- Invariant: the gap between @b@ and @c@ is the biggest we've
    -- seen between adjacent values so far.
    go :: (Integer, Integer) -> (Integer, Integer) -> [Integer] -> Domain w
go (Integer
a, Integer
b) (Integer
c, Integer
d) [] = Domain w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
join (NatRepr w -> Integer -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr w
w Integer
a Integer
b) (NatRepr w -> Integer -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr w
w Integer
c Integer
d)
    go (Integer
a, Integer
b) (Integer
c, Integer
d) (Integer
e : [Integer]
rest)
      | Integer
e Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
d Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b = (Integer, Integer) -> (Integer, Integer) -> [Integer] -> Domain w
go (Integer
a, Integer
d) (Integer
e, Integer
e) [Integer]
rest
      | Bool
otherwise     = (Integer, Integer) -> (Integer, Integer) -> [Integer] -> Domain w
go (Integer
a, Integer
b) (Integer
c, Integer
e) [Integer]
rest

-- | @concat a y@ returns domain where each element in @a@ has been
-- concatenated with an element in @y@.  The most-significant bits
-- are @a@, and the least significant bits are @y@.
concat :: NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
concat :: forall (u :: Nat) (v :: Nat).
NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
concat NatRepr u
u Domain u
a NatRepr v
v Domain v
b =
  case Domain u
a of
    BVDAny Integer
_ -> Integer -> Domain (u + v)
forall (w :: Nat). Integer -> Domain w
BVDAny Integer
mask
    BVDInterval Integer
_ Integer
al Integer
aw -> Integer -> Integer -> Integer -> Domain (u + v)
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask (Integer -> Integer -> Integer
cat Integer
al Integer
bl) (Integer -> Integer -> Integer
cat Integer
aw Integer
bw)
  where
    cat :: Integer -> Integer -> Integer
cat Integer
i Integer
j = (Integer
i 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)
    (Integer
bl, Integer
bh) = Domain v -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain v
b
    bw :: Integer
bw = Integer
bh Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
bl

-- | @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 Domain (i + n)
a =
  case Domain (i + n)
a of
    BVDAny Integer
mask -> Integer -> Domain n
forall (w :: Nat). Integer -> Domain w
BVDAny (Integer -> Integer
shr Integer
mask)
    BVDInterval Integer
mask Integer
al Integer
aw ->
      Integer -> Integer -> Integer -> Domain n
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval (Integer -> Integer
shr Integer
mask) Integer
bl (Integer
bh Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
bl)
      where
        bl :: Integer
bl = Integer -> Integer
shr Integer
al
        bh :: Integer
bh = Integer -> Integer
shr (Integer
al Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
aw)
  where
    shr :: Integer -> Integer
shr Integer
x = Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` NatRepr i -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr i
i

-- | @trunc n d@ selects the @n@ least significant bits from @d@.
trunc ::
  (n <= w) =>
  NatRepr n ->
  Domain w -> Domain n
trunc :: forall (n :: Nat) (w :: Nat).
(n <= w) =>
NatRepr n -> Domain w -> Domain n
trunc NatRepr n
n Domain w
a =
  case Domain w
a of
    BVDAny Integer
_ -> Integer -> Domain n
forall (w :: Nat). Integer -> Domain w
BVDAny Integer
mask
    BVDInterval Integer
_ Integer
al Integer
aw -> Integer -> Integer -> Integer -> Domain n
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
al Integer
aw
  where
    mask :: Integer
mask = NatRepr n -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr n
n

-- | @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)

zext :: (1 <= w, w + 1 <= u) => Domain w -> NatRepr u -> Domain u
zext :: forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
Domain w -> NatRepr u -> Domain u
zext Domain w
a NatRepr u
u = NatRepr u -> Integer -> Integer -> Domain u
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr u
u Integer
al Integer
ah
  where (Integer
al, Integer
ah) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
a

sext ::
  forall w u. (1 <= w, w + 1 <= u) =>
  NatRepr w ->
  Domain w ->
  NatRepr u ->
  Domain u
sext :: forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> Domain w -> NatRepr u -> Domain u
sext NatRepr w
w Domain w
a NatRepr u
u =
  case LeqProof 1 u
fProof of
    LeqProof 1 u
LeqProof ->
      NatRepr u -> Integer -> Integer -> Domain u
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr u
u Integer
al Integer
ah
      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
  where
    wProof :: LeqProof 1 w
    wProof :: LeqProof 1 w
wProof = LeqProof 1 w
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof
    uProof :: LeqProof (w + 1) u
    uProof :: LeqProof (w + 1) u
uProof = LeqProof (w + 1) u
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof
    fProof :: LeqProof 1 u
    fProof :: LeqProof 1 u
fProof = LeqProof 1 (w + 1) -> LeqProof (w + 1) u -> LeqProof 1 u
forall (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans (LeqProof 1 w -> NatRepr 1 -> LeqProof 1 (w + 1)
forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 w
wProof (NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat :: NatRepr 1)) LeqProof (w + 1) u
uProof

--------------------------------------------------------------------------------
-- Shifts

shl :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
shl :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
shl NatRepr w
w Domain w
a Domain w
b
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isBVDAny Domain w
a = Domain w
a
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isSingletonZero Domain w
a = Domain w
a
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isSingletonZero Domain w
b = Domain w
a
  | Bool
otherwise = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
lo (Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lo)
    where
      mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
      sz :: Integer
sz = Integer
mask Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
      (Integer
bl, Integer
bh) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
b
      bl' :: Int
bl' = NatRepr w -> Integer -> Int
forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
bl
      bh' :: Int
bh' = NatRepr w -> Integer -> Int
forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
bh
      -- compute bounds for c = 2^b
      cl :: Integer
cl = if (Integer
mask Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
bl' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0) then Integer
sz else Int -> Integer
forall a. Bits a => Int -> a
bit Int
bl'
      ch :: Integer
ch = if (Integer
mask Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
bh' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0) then Integer
sz else Int -> Integer
forall a. Bits a => Int -> a
bit Int
bh'
      (Integer
lo, Integer
hi) = (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer)
mulRange (Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
zbounds Domain w
a) (Integer
cl, Integer
ch)

lshr :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
lshr :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
lshr NatRepr w
w Domain w
a Domain w
b = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
cl (Integer
ch Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
cl)
  where
    mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
    (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
    cl :: Integer
cl = Integer
al Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` NatRepr w -> Integer -> Int
forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
bh
    ch :: Integer
ch = Integer
ah Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` NatRepr w -> Integer -> Int
forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
bl

ashr :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
ashr :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
ashr NatRepr w
w Domain w
a Domain w
b = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
cl (Integer
ch Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
cl)
  where
    mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
    (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) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
ubounds Domain w
b
    cl :: Integer
cl = Integer
al Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` (if Integer
al Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then NatRepr w -> Integer -> Int
forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
bl else NatRepr w -> Integer -> Int
forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
bh)
    ch :: Integer
ch = Integer
ah Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` (if Integer
ah Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then NatRepr w -> Integer -> Int
forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
bh else NatRepr w -> Integer -> Int
forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
bl)

-- | Clamp the given shift amount to the word width indicated by the
--   nat repr
clamp :: NatRepr w -> Integer -> Int
clamp :: forall (w :: Nat). NatRepr w -> Integer -> Int
clamp NatRepr w
w Integer
x = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w) Integer
x)

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

add :: (1 <= w) => Domain w -> Domain w -> Domain w
add :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
add Domain w
a Domain w
b =
  case Domain w
a of
    BVDAny Integer
_ -> Domain w
a
    BVDInterval Integer
_ Integer
al Integer
aw ->
      case Domain w
b of
        BVDAny Integer
_ -> Domain w
b
        BVDInterval Integer
mask Integer
bl Integer
bw ->
          Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask (Integer
al Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
bl) (Integer
aw Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
bw)

negate :: (1 <= w) => Domain w -> Domain w
negate :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w
negate Domain w
a =
  case Domain w
a of
    BVDAny Integer
_ -> Domain w
a
    BVDInterval Integer
mask Integer
al Integer
aw -> Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDInterval Integer
mask ((-Integer
ah) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask) Integer
aw
      where ah :: Integer
ah = Integer
al Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
aw

scale :: (1 <= w) => Integer -> Domain w -> Domain w
scale :: forall (w :: Nat). (1 <= w) => Integer -> Domain w -> Domain w
scale Integer
k Domain w
a
  | Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDInterval (Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a) Integer
0 Integer
0
  | Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 = Domain w
a
  | Bool
otherwise =
    case Domain w
a of
      BVDAny Integer
_ -> Domain w
a
      BVDInterval Integer
mask Integer
al Integer
aw
        | Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 -> Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
al) (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
aw)
        | Bool
otherwise -> Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
ah) (Integer -> Integer
forall a. Num a => a -> a
abs Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
aw)
        where ah :: Integer
ah = Integer
al Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
aw

mul :: (1 <= w) => Domain w -> Domain w -> Domain w
mul :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
mul Domain w
a Domain w
b
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isSingletonZero Domain w
a = Domain w
a
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isSingletonZero Domain w
b = Domain w
b
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isBVDAny Domain w
a = Domain w
a
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isBVDAny Domain w
b = Domain w
b
  | Bool
otherwise = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
cl (Integer
ch Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
cl)
    where
      mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
      (Integer
cl, Integer
ch) = (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer)
mulRange (Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
zbounds Domain w
a) (Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
zbounds Domain w
b)

-- | Choose a representative integer range (positive or negative) for
-- the given bitvector domain such that the endpoints are as close to
-- zero as possible.
zbounds :: Domain w -> (Integer, Integer)
zbounds :: forall (w :: Nat). Domain w -> (Integer, Integer)
zbounds Domain w
a =
  case Domain w
a of
    BVDAny Integer
mask -> (Integer
0, Integer
mask)
    BVDInterval Integer
mask Integer
lo Integer
sz -> (Integer
lo', Integer
lo' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
sz)
      where lo' :: Integer
lo' = if Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
lo Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
sz Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
mask then Integer
lo Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- (Integer
mask Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) else Integer
lo

mulRange :: (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer)
mulRange :: (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer)
mulRange (Integer
al, Integer
ah) (Integer
bl, Integer
bh) = (Integer
cl, Integer
ch)
  where
    (Integer
albl, Integer
albh) = Integer -> (Integer, Integer) -> (Integer, Integer)
scaleRange Integer
al (Integer
bl, Integer
bh)
    (Integer
ahbl, Integer
ahbh) = Integer -> (Integer, Integer) -> (Integer, Integer)
scaleRange Integer
ah (Integer
bl, Integer
bh)
    cl :: Integer
cl = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
albl Integer
ahbl
    ch :: Integer
ch = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
albh Integer
ahbh

scaleRange :: Integer -> (Integer, Integer) -> (Integer, Integer)
scaleRange :: Integer -> (Integer, Integer) -> (Integer, Integer)
scaleRange Integer
k (Integer
lo, Integer
hi)
  | Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
hi, Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
lo)
  | Bool
otherwise = (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
lo, Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
hi)

udiv :: (1 <= w) => Domain w -> Domain w -> Domain w
udiv :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
udiv Domain w
a Domain w
b
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isSingletonZero Domain w
b = Integer -> Domain w
forall (w :: Nat). Integer -> Domain w
BVDAny Integer
mask
  | Bool
otherwise = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
ql (Integer
qh Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
ql)
  where
    mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
    (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
    ql :: Integer
ql = Integer
al Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
1 Integer
bh -- assume that division by 0 does not happen
    qh :: Integer
qh = Integer
ah Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
1 Integer
bl -- assume that division by 0 does not happen

urem :: (1 <= w) => Domain w -> Domain w -> Domain w
urem :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
urem Domain w
a Domain w
b
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isSingletonZero Domain w
b = Integer -> Domain w
forall (w :: Nat). Integer -> Domain w
BVDAny Integer
mask
  | Integer
qh Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
ql = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
rl (Integer
rh Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
rl)
  | Bool
otherwise = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
0 (Integer
bh Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
  where
    mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
    (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
    (Integer
ql, Integer
rl) = Integer
al Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`divMod` Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
1 Integer
bh -- assume that division by 0 does not happen
    (Integer
qh, Integer
rh) = Integer
ah Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`divMod` Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
1 Integer
bl -- assume that division by 0 does not happen

-- | Pairs of nonzero integers @(lo, hi)@ such that @1\/lo <= 1\/hi@.
-- This pair represents the set of all nonzero integers @x@ such that
-- @1\/lo <= 1\/x <= 1\/hi@.
data ReciprocalRange = ReciprocalRange Integer Integer

-- | Nonzero signed values in a domain with the least and greatest
-- reciprocals.
rbounds :: (1 <= w) => NatRepr w -> Domain w -> ReciprocalRange
rbounds :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> ReciprocalRange
rbounds NatRepr w
w Domain w
a =
  case Domain w
a of
    BVDAny Integer
_ -> Integer -> Integer -> ReciprocalRange
ReciprocalRange (-Integer
1) Integer
1
    BVDInterval Integer
mask Integer
al Integer
aw
      | Integer
ah Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
mask Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 -> Integer -> Integer -> ReciprocalRange
ReciprocalRange (-Integer
1) Integer
1
      | Bool
otherwise     -> Integer -> Integer -> ReciprocalRange
ReciprocalRange (Integer -> Integer
signed (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
mask Integer
ah)) (Integer -> Integer
signed (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
1 Integer
al))
      where
        ah :: Integer
ah = Integer
al Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
aw
        signed :: Integer -> Integer
signed Integer
x = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
halfRange NatRepr w
w then Integer
x else Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- (Integer
mask Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)

-- | Interval arithmetic for integer division (rounding towards 0).
-- Given @a@ and @b@ with @al <= a <= ah@ and @1\/bl <= 1\/b <= 1/bh@,
-- @sdivRange (al, ah) (ReciprocalRange bl bh)@ returns @(ql, qh)@
-- such that @ql <= a `quot` b <= qh@.
sdivRange :: (Integer, Integer) -> ReciprocalRange -> (Integer, Integer)
sdivRange :: (Integer, Integer) -> ReciprocalRange -> (Integer, Integer)
sdivRange (Integer
al, Integer
ah) (ReciprocalRange Integer
bl Integer
bh) = (Integer
ql, Integer
qh)
  where
    (Integer
ql1, Integer
qh1) = (Integer, Integer) -> Integer -> (Integer, Integer)
scaleDownRange (Integer
al, Integer
ah) Integer
bh
    (Integer
ql2, Integer
qh2) = (Integer, Integer) -> Integer -> (Integer, Integer)
scaleDownRange (Integer
al, Integer
ah) Integer
bl
    ql :: Integer
ql = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
ql1 Integer
ql2
    qh :: Integer
qh = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
qh1 Integer
qh2

shrinkRange :: (Integer, Integer) -> Integer -> (Integer, Integer)
shrinkRange :: (Integer, Integer) -> Integer -> (Integer, Integer)
shrinkRange (Integer
lo, Integer
hi) Integer
k =
  if Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 then (Integer
lo Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
k, Integer
hi Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
k) else
  if Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then (Integer
hi Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
k, Integer
lo Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
k) else (Integer
lo, Integer
hi)

-- | @scaleDownRange (lo, hi) k@ returns an interval @(ql, qh)@ such that for any
-- @x@ in @[lo..hi]@, @x `quot` k@ is in @[ql..qh]@.
scaleDownRange :: (Integer, Integer) -> Integer -> (Integer, Integer)
scaleDownRange :: (Integer, Integer) -> Integer -> (Integer, Integer)
scaleDownRange (Integer
lo, Integer
hi) Integer
k
  | Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 = (Integer
lo Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
k, Integer
hi Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
k)
  | Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = (Integer
hi Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
k, Integer
lo Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
k)
  | Bool
otherwise = (Integer
lo, Integer
hi) -- assume k is nonzero


sdiv :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
sdiv :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
sdiv NatRepr w
w Domain w
a Domain w
b
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isSingletonZero Domain w
b = Integer -> Domain w
forall (w :: Nat). Integer -> Domain w
BVDAny Integer
mask
  | Bool
otherwise = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
ql (Integer
qh Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
ql)
  where
    mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
    (Integer
ql, Integer
qh) = (Integer, Integer) -> ReciprocalRange -> (Integer, Integer)
sdivRange (NatRepr w -> Domain w -> (Integer, Integer)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> (Integer, Integer)
sbounds NatRepr w
w Domain w
a) (NatRepr w -> Domain w -> ReciprocalRange
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> ReciprocalRange
rbounds NatRepr w
w Domain w
b)

srem :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
srem :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
srem NatRepr w
w Domain w
a Domain w
b
  -- Division by zero is unspecified; widen to any rather than building
  -- an improper domain. (Without this guard, the @rh < rl@ branch below
  -- builds @BVDInterval mask _ (rh - rl)@ with a negative size.)
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isSingletonZero Domain w
b = Integer -> Domain w
forall (w :: Nat). Integer -> Domain w
BVDAny Integer
mask
  -- If the quotient is a singleton @q@, then we compute the remainder
  -- @r = a - q*b@.
  | Integer
ql Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
qh =
      if Integer
ql Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
      then Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask (Integer
al Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
ql Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
bl) (Integer
aw Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
ql Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
bw)
      else Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask (Integer
al Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
ql Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
bh) (Integer
aw Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
ql Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
bw)
  -- Otherwise the range of possible remainders is determined by the
  -- modulus and the sign of the first argument.
  | Bool
otherwise = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
rl (Integer
rh Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
rl)
  where
    mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
    (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
    (Integer
ql, Integer
qh) = (Integer, Integer) -> ReciprocalRange -> (Integer, Integer)
sdivRange (Integer
al, Integer
ah) (NatRepr w -> Domain w -> ReciprocalRange
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> ReciprocalRange
rbounds NatRepr w
w Domain w
b)
    rl :: Integer
rl = if Integer
al Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min (Integer
bl Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (-Integer
bh Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) else Integer
0
    rh :: Integer
rh = if Integer
ah Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 then Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max (-Integer
blInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) (Integer
bhInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) else Integer
0
    aw :: Integer
aw = Integer
ah Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
al
    bw :: Integer
bw = Integer
bh Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
bl

-- | Like 'udiv', but using the SMT-LIB @FixedSizeBitVectors@ theory's
-- div-by-zero semantics:
--
-- > [[(bvudiv s t)]] := if bv2nat([[t]]) = 0
-- >                     then λx:[0, m). 1
-- >                     else nat2bv[m](bv2nat([[s]]) div bv2nat([[t]]))
--
-- i.e.\ the all-ones bitvector when the divisor is zero. 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
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isSingletonZero Domain w
b = Integer -> Integer -> Domain w
forall {w :: Nat}. Integer -> Integer -> Domain w
singleton' 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). (1 <= w) => Domain w -> Domain w -> Domain w
join (Domain w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
udiv Domain w
a Domain w
b) (Integer -> Integer -> Domain w
forall {w :: Nat}. Integer -> Integer -> Domain w
singleton' Integer
mask Integer
mask)
  | Bool
otherwise         = Domain w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => 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
    singleton' :: Integer -> Integer -> Domain w
singleton' Integer
m Integer
v = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDInterval Integer
m Integer
v Integer
0

-- | Like 'urem', but using the SMT-LIB @FixedSizeBitVectors@ theory's
-- div-by-zero semantics:
--
-- > [[(bvurem s t)]] := if bv2nat([[t]]) = 0
-- >                     then [[s]]
-- >                     else nat2bv[m](bv2nat([[s]]) mod bv2nat([[t]]))
--
-- i.e.\ the dividend itself when the divisor is zero. 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
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isSingletonZero 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). (1 <= w) => Domain w -> Domain w -> Domain w
join (Domain w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => 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). (1 <= w) => Domain w -> Domain w -> Domain w
urem Domain w
a Domain w
b

-- | Like 'sdiv', but using the SMT-LIB QF_BV logic's div-by-zero
-- convention: @(bvsdiv s 0)@ is all-ones when the dividend is
-- non-negative, @1@ when it is negative. The signed variants are not
-- in the core @FixedSizeBitVectors@ theory; this convention matches
-- Z3, CVC5, Bitwuzla, and Yices. 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
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isSingletonZero 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). (1 <= w) => Domain w -> Domain w -> Domain w
join (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 the dividend'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 (Integer
al Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0, Integer
ah Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0) of
    (Bool
False, Bool
_    ) -> NatRepr w -> Integer -> Domain w
forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
mask        -- s >= 0: all-ones
    (Bool
True,  Bool
False) -> NatRepr w -> Integer -> Domain w
forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
1           -- s < 0: one
    (Bool
True,  Bool
True ) -> Domain w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
join (NatRepr w -> Integer -> Domain w
forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
1) (NatRepr w -> Integer -> Domain w
forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
mask)
  where
    mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain w
a
    (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

-- | Like 'srem', but using the SMT-LIB QF_BV logic's div-by-zero
-- convention: @(bvsrem s 0)@ is the dividend itself. The signed
-- variants are not in the core @FixedSizeBitVectors@ theory; this
-- convention matches Z3, CVC5, Bitwuzla, and Yices. 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
  | Domain w -> Bool
forall (w :: Nat). Domain w -> Bool
isSingletonZero 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). (1 <= w) => Domain w -> Domain w -> Domain w
join (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

--------------------------------------------------------------------------------
-- Bitwise logical

-- | Complement bits in range.
not :: Domain w -> Domain w
not :: forall (w :: Nat). Domain w -> Domain w
not Domain w
a =
  case Domain w
a of
    BVDAny Integer
_ -> Domain w
a
    BVDInterval Integer
mask Integer
al Integer
aw ->
      Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDInterval Integer
mask (Integer -> Integer
forall a. Bits a => a -> a
complement Integer
ah Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask) Integer
aw
      where ah :: Integer
ah = Integer
al Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
aw

-- | Return bitwise bounds for domain (i.e. logical AND of all
-- possible values, paired with logical OR of all possible values).
bitbounds :: Domain w -> (Integer, Integer)
bitbounds :: forall (w :: Nat). Domain w -> (Integer, Integer)
bitbounds Domain w
a =
  case Domain w
a of
    BVDAny Integer
mask -> (Integer
0, Integer
mask)
    BVDInterval Integer
mask Integer
al Integer
aw
      | Integer
al Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
aw Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
mask -> (Integer
0, Integer
mask)
      | Bool
otherwise -> (Integer
lo, Integer
hi)
      where
        au :: Integer
au = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
unknowns Domain w
a
        hi :: Integer
hi = Integer
al Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
au
        lo :: Integer
lo = Integer
hi Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
au

-- | @unknowns lo hi@ returns a bitmask representing the set of bit
-- positions whose values are not constant throughout the range
-- @lo..hi@.
unknowns :: Domain w -> Integer
unknowns :: forall (w :: Nat). Domain w -> Integer
unknowns (BVDAny Integer
mask) = Integer
mask
unknowns (BVDInterval Integer
mask Integer
al Integer
aw) = Integer
mask Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. (Integer -> Integer
fillright (Integer
al Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` (Integer
al Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
aw)))

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

-- | @fillright x@ rounds up @x@ to the nearest 2^n-1.
fillright :: Integer -> Integer
fillright :: Integer -> Integer
fillright = Integer -> Integer
Arith.bitsBelow
{-# INLINE fillright #-}

------------------------------------------------------------------
-- 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
w Integer
x = Bool -> Property
property (NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
w (NatRepr n -> Domain n
forall (w :: Nat). (1 <= w) => NatRepr w -> Domain w
any NatRepr n
w) Integer
x)

correct_ubounds :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Property
correct_ubounds :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> Property
correct_ubounds NatRepr n
n (Domain n
a,Integer
x) = NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n 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) = NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n 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_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).
(HasCallStack, 1 <= w) =>
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
-- among the low-bound candidates of either domain.
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
    witness :: Integer
witness = case (Domain n -> Maybe (Integer, Integer)
forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
arithDomainData Domain n
a, Domain n -> Maybe (Integer, Integer)
forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
arithDomainData Domain n
b) of
      (Just (Integer
alo, Integer
_), Maybe (Integer, Integer)
_) | Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
alo -> Integer
alo
      (Maybe (Integer, Integer)
_, Just (Integer
blo, Integer
_)) -> Integer
blo
      (Maybe (Integer, Integer), Maybe (Integer, Integer))
_ -> Integer
0

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).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
singleton NatRepr n
n Integer
x)
    Maybe Integer
Nothing -> Bool -> Property
property Bool
True

correct_mulRange :: (Integer, Integer) -> (Integer, Integer) -> Integer -> Integer -> Property
correct_mulRange :: (Integer, Integer)
-> (Integer, Integer) -> Integer -> Integer -> Property
correct_mulRange (Integer, Integer)
a (Integer, Integer)
b Integer
x Integer
y =
  (Integer, Integer) -> Integer -> Bool
forall {a}. Ord a => (a, a) -> a -> Bool
inRange (Integer, Integer)
a Integer
x Bool -> Bool -> Bool
&& (Integer, Integer) -> Integer -> Bool
forall {a}. Ord a => (a, a) -> a -> Bool
inRange (Integer, Integer)
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> (Integer, Integer) -> Integer -> Bool
forall {a}. Ord a => (a, a) -> a -> Bool
inRange ((Integer, Integer) -> (Integer, Integer) -> (Integer, Integer)
mulRange (Integer, Integer)
a (Integer, Integer)
b) (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y)
  where
    inRange :: (a, a) -> a -> Bool
inRange (a
lo, a
hi) a
v = a
lo a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
v Bool -> Bool -> Bool
&& a
v a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
hi

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). (1 <= w) => Domain w -> Domain w -> Domain w
union 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). (1 <= w) => 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). (1 <= w) => Domain w -> Domain w -> Domain w
meet Domain n
a Domain n
b) Integer
x

-- Note: 'meet' for the arithmetic domain is *not* a precise intersection
-- when one of the arguments is a wrap-around interval. In that case
-- 'ubounds' returns @(0, mask)@, and the result over-approximates. The
-- bitwise domain's meet (in "What4.Domains.BV.Bitwise") *is* precise; see
-- 'What4.Domains.BV.Bitwise.precise_meet'.

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

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

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

join_bottom :: (1 <= n) => NatRepr n -> Domain n -> Integer -> Property
join_bottom :: forall (n :: Nat).
(1 <= n) =>
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). (1 <= w) => Domain w -> Domain w -> Domain w
join Domain n
a (NatRepr n -> Domain n
forall (w :: Nat). (1 <= w) => 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 :: (1 <= n) => NatRepr n -> Domain n -> Integer -> Property
meet_top :: forall (n :: Nat).
(1 <= n) =>
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). (1 <= w) => Domain w -> Domain w -> Domain w
meet Domain n
a (NatRepr n -> Domain n
forall (w :: Nat). (1 <= w) => 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 :: (1 <= n) => NatRepr n -> Domain n -> Integer -> Property
meet_bottom :: forall (n :: Nat).
(1 <= n) =>
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). (1 <= w) => Domain w -> Domain w -> Domain w
meet Domain n
a (NatRepr n -> Domain n
forall (w :: Nat). (1 <= w) => 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

join_upper_bound :: (1 <= n) => Domain n -> Domain n -> Property
join_upper_bound :: forall (n :: Nat). (1 <= n) => 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). (1 <= w) => Domain w -> Domain w -> Domain w
join Domain n
a Domain n
b))

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). (1 <= w) => 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). (1 <= w) => 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_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). (1 <= w) => 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_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). (1 <= w) => Domain w -> Domain w
negate Domain n
a) (Integer -> Integer
forall a. Num a => a -> a
Prelude.negate Integer
x)

correct_not :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Property
correct_not :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> Property
correct_not NatRepr n
n (Domain n
a,Integer
x) = 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_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). (1 <= w) => 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_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). (1 <= w) => 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_scale_eq :: (1 <= n) => NatRepr n -> Integer -> Domain n -> Property
correct_scale_eq :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Integer -> Domain n -> Property
correct_scale_eq NatRepr n
n Integer
k Domain n
a = Bool -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Domain n -> Domain n -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
sameDomain (Integer -> Domain n -> Domain n
forall (w :: Nat). (1 <= w) => Integer -> Domain w -> Domain w
scale Integer
k' Domain n
a) (Domain n -> Domain n -> Domain n
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
mul (NatRepr n -> Integer -> Domain n
forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
singleton NatRepr n
n Integer
k) Domain n
a)
  where
  k' :: Integer
k' = NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
k

correct_udiv :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_udiv :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_udiv NatRepr n
n (Domain n
a,Integer
x) (Domain n
b,Integer
y) = 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). (1 <= w) => 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). (1 <= w) => 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_sdivRange :: (Integer, Integer) -> (Integer, Integer) -> Integer -> Integer -> Property
correct_sdivRange :: (Integer, Integer)
-> (Integer, Integer) -> Integer -> Integer -> Property
correct_sdivRange (Integer, Integer)
a (Integer, Integer)
b Integer
x Integer
y =
   (Integer, Integer) -> Integer -> Bool
forall {a}. Ord a => (a, a) -> a -> Bool
mem (Integer, Integer)
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> (Integer, Integer) -> Integer -> Bool
forall {a}. Ord a => (a, a) -> a -> Bool
mem (Integer, Integer)
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
==> (Integer, Integer) -> Integer -> Bool
forall {a}. Ord a => (a, a) -> a -> Bool
mem ((Integer, Integer) -> ReciprocalRange -> (Integer, Integer)
sdivRange (Integer, Integer)
a ReciprocalRange
b') (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
y)
 where
 b' :: ReciprocalRange
b' = Integer -> Integer -> ReciprocalRange
ReciprocalRange ((Integer, Integer) -> Integer
forall a b. (a, b) -> b
snd (Integer, Integer)
b) ((Integer, Integer) -> Integer
forall a b. (a, b) -> a
fst (Integer, Integer)
b)
 mem :: (a, a) -> a -> Bool
mem (a
lo,a
hi) a
v = a
lo a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
v Bool -> Bool -> Bool
&& a
v a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
hi

correct_shrinkRange :: (Integer, Integer) -> Integer -> Integer -> Property
correct_shrinkRange :: (Integer, Integer) -> Integer -> Integer -> Property
correct_shrinkRange (Integer, Integer)
a Integer
x Integer
y =
   (Integer, Integer) -> Integer -> Bool
forall {a}. Ord a => (a, a) -> a -> Bool
mem (Integer, Integer)
a Integer
x 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
==> (Integer, Integer) -> Integer -> Bool
forall {a}. Ord a => (a, a) -> a -> Bool
mem ((Integer, Integer) -> Integer -> (Integer, Integer)
shrinkRange (Integer, Integer)
a Integer
y) (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
y)
 where
 mem :: (a, a) -> a -> Bool
mem (a
lo,a
hi) a
v = a
lo a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
v Bool -> Bool -> Bool
&& a
v a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
hi

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

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

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

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

correct_eq :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_eq :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_eq NatRepr n
n (Domain n
a,Integer
x) (Domain n
b,Integer
y) =
  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_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). (1 <= w) => 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_isUltSumCommonEquiv ::
  (1 <= n) =>
  NatRepr n ->
  (Domain n, Integer) ->
  (Domain n, Integer) ->
  (Domain n, Integer) ->
  Property
correct_isUltSumCommonEquiv :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (Domain n, Integer)
-> (Domain n, Integer)
-> (Domain n, Integer)
-> Property
correct_isUltSumCommonEquiv NatRepr n
n (Domain n
a, Integer
x) (Domain n
b, Integer
y) (Domain n
c, Integer
z) =
  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
==> Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
c Integer
z Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==>
    Domain n -> Domain n -> Domain n -> Bool
forall (w :: Nat). Domain w -> Domain w -> Domain w -> Bool
isUltSumCommonEquiv Domain n
a Domain n
b Domain n
c Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==>
      ((NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
z) 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 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
z)) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== (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))

correct_unknowns :: (1 <= n) => Domain n -> Integer -> Integer -> Property
correct_unknowns :: forall (n :: Nat).
(1 <= n) =>
Domain n -> Integer -> Integer -> Property
correct_unknowns Domain n
a Integer
x Integer
y = 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
a Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> ((Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
u) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== (Integer
y Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
u)) Bool -> Bool -> Bool
&& (Integer
u Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
mask Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
mask)
  where
  u :: Integer
u = Domain n -> Integer
forall (w :: Nat). Domain w -> Integer
unknowns Domain n
a
  mask :: Integer
mask = Domain n -> Integer
forall (w :: Nat). Domain w -> Integer
bvdMask Domain n
a

correct_bitbounds :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Property
correct_bitbounds :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> Property
correct_bitbounds NatRepr n
n (Domain n
a,Integer
x) =
    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 -> Integer -> Bool
bitle Integer
lo Integer
x' Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
bitle Integer
x' Integer
hi Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
bitle Integer
hi (NatRepr n -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr n
n))
  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)
bitbounds Domain n
a