{-|
Module      : What4.Utils.BVDomain
Description : Abstract domains for bitvectors
Copyright   : (c) Galois Inc, 2019-2020
License     : BSD3
Maintainer  : huffman@galois.com

Provides an implementation of abstract domains for bitvectors.
This abstract domain has essentially two modes: arithmetic
and bitvector modes. The arithmetic mode is a fairly straightforward
interval domain, albeit one that is carefully implemented to deal
properly with intervals that "cross zero", as is relatively common
when using 2's complement signed representations. The bitwise
mode tracks the values of individual bits independently in a
3-valued logic (true, false or unknown).  The abstract domain
transitions between the two modes when necessary, but attempts
to retain as much precision as possible.

The operations of these domains are formalized in the companion
Cryptol files found together in this package under the \"doc\"
directory, and their soundness properties stated and established.
-}

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

module What4.Utils.BVDomain
  ( -- * Bitvector abstract domains
    BVDomain(..)
  , proper
  , member
  , size
    -- ** Domain transfer functions
  , asArithDomain
  , asBitwiseDomain
  , asXorDomain
  , fromXorDomain
  , arithToXorDomain
  , bitwiseToXorDomain
  , xorToBitwiseDomain
    -- ** Projection functions
  , asSingleton
  , eq
  , slt
  , ult
  , testBit
  , domainsOverlap
  , ubounds
  , sbounds
  , A.arithDomainData
  , B.bitbounds
    -- * Operations
  , any
  , singleton
  , range
  , fromAscEltList
  , union
  , concat
  , select
  , zext
  , sext
    -- ** Shifts and rotates
  , shl
  , lshr
  , ashr
  , rol
  , ror
    -- ** Arithmetic
  , add
  , negate
  , scale
  , mul
  , udiv
  , urem
  , sdiv
  , srem
    -- ** Bitwise
  , What4.Utils.BVDomain.not
  , and
  , or
  , xor

    -- ** Misc
  , popcnt
  , clz
  , ctz

    -- * Useful bitvector computations
  , bitwiseRoundAbove
  , bitwiseRoundBetween

    -- * Correctness properties
  , genDomain
  , genElement
  , genPair

  , correct_arithToBitwise
  , correct_bitwiseToArith
  , correct_bitwiseToXorDomain
  , correct_arithToXorDomain
  , correct_xorToBitwiseDomain
  , correct_asXorDomain
  , correct_fromXorDomain

  , correct_bra1
  , correct_bra2
  , correct_brb1
  , correct_brb2

  , correct_any
  , correct_ubounds
  , correct_sbounds
  , correct_singleton
  , correct_overlap
  , precise_overlap
  , correct_union
  , correct_zero_ext
  , correct_sign_ext
  , correct_concat
  , correct_select
  , correct_add
  , correct_neg
  , correct_mul
  , correct_scale
  , correct_udiv
  , correct_urem
  , correct_sdiv
  , correct_srem
  , correct_shl
  , correct_lshr
  , correct_ashr
  , correct_rol
  , correct_ror
  , correct_eq
  , correct_ult
  , correct_slt
  , correct_and
  , correct_or
  , correct_not
  , correct_xor
  , correct_testBit
  , correct_popcnt
  , correct_clz
  , correct_ctz
  ) where

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

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

import qualified What4.Utils.Arithmetic as Arith

import qualified What4.Utils.BVDomain.Arith as A
import qualified What4.Utils.BVDomain.Bitwise as B
import qualified What4.Utils.BVDomain.XOR as X

import           Test.Verification ( Property, property, (==>), Gen, chooseBool )


arithToBitwiseDomain :: A.Domain w -> B.Domain w
arithToBitwiseDomain :: forall (w :: Nat). Domain w -> Domain w
arithToBitwiseDomain Domain w
a =
  let mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
A.bvdMask Domain w
a in
  case forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
A.arithDomainData Domain w
a of
    Maybe (Integer, Integer)
Nothing -> forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
B.interval Integer
mask Integer
0 Integer
mask
    Just (Integer
alo,Integer
_) -> forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
B.interval Integer
mask Integer
lo Integer
hi
      where
        u :: Integer
u = forall (w :: Nat). Domain w -> Integer
A.unknowns Domain w
a
        hi :: Integer
hi = Integer
alo forall a. Bits a => a -> a -> a
.|. Integer
u
        lo :: Integer
lo = Integer
hi forall a. Bits a => a -> a -> a
`Bits.xor` Integer
u

bitwiseToArithDomain :: B.Domain w -> A.Domain w
bitwiseToArithDomain :: forall (w :: Nat). Domain w -> Domain w
bitwiseToArithDomain Domain w
b = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
A.interval Integer
mask Integer
lo ((Integer
hi forall a. Num a => a -> a -> a
- Integer
lo) forall a. Bits a => a -> a -> a
.&. Integer
mask)
  where
  mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
B.bvdMask Domain w
b
  (Integer
lo,Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b

bitwiseToXorDomain :: B.Domain w -> X.Domain w
bitwiseToXorDomain :: forall (w :: Nat). Domain w -> Domain w
bitwiseToXorDomain Domain w
b = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
X.interval Integer
mask Integer
lo Integer
hi
  where
  mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
B.bvdMask Domain w
b
  (Integer
lo,Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b

arithToXorDomain :: A.Domain w -> X.Domain w
arithToXorDomain :: forall (w :: Nat). Domain w -> Domain w
arithToXorDomain Domain w
a =
  let mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
A.bvdMask Domain w
a in
  case forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
A.arithDomainData Domain w
a of
    Maybe (Integer, Integer)
Nothing -> forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
X.BVDXor Integer
mask Integer
mask Integer
mask
    Just (Integer
alo,Integer
_) -> forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
X.BVDXor Integer
mask Integer
hi Integer
u
      where
        u :: Integer
u = forall (w :: Nat). Domain w -> Integer
A.unknowns Domain w
a
        hi :: Integer
hi = Integer
alo forall a. Bits a => a -> a -> a
.|. Integer
u

xorToBitwiseDomain :: X.Domain w -> B.Domain w
xorToBitwiseDomain :: forall (w :: Nat). Domain w -> Domain w
xorToBitwiseDomain Domain w
x = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
B.interval Integer
mask Integer
lo Integer
hi
  where
  mask :: Integer
mask = forall (w :: Nat). Domain w -> Integer
X.bvdMask Domain w
x
  (Integer
lo, Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
X.bitbounds Domain w
x

asXorDomain :: BVDomain w -> X.Domain w
asXorDomain :: forall (w :: Nat). BVDomain w -> Domain w
asXorDomain (BVDArith Domain w
a) = forall (w :: Nat). Domain w -> Domain w
arithToXorDomain Domain w
a
asXorDomain (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> Domain w
bitwiseToXorDomain Domain w
b

fromXorDomain :: X.Domain w -> BVDomain w
fromXorDomain :: forall (w :: Nat). Domain w -> BVDomain w
fromXorDomain Domain w
x = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat). Domain w -> Domain w
xorToBitwiseDomain Domain w
x)

asArithDomain :: BVDomain w -> A.Domain w
asArithDomain :: forall (w :: Nat). BVDomain w -> Domain w
asArithDomain (BVDArith Domain w
a)   = Domain w
a
asArithDomain (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> Domain w
bitwiseToArithDomain Domain w
b

asBitwiseDomain :: BVDomain w -> B.Domain w
asBitwiseDomain :: forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain (BVDArith Domain w
a)   = forall (w :: Nat). Domain w -> Domain w
arithToBitwiseDomain Domain w
a
asBitwiseDomain (BVDBitwise Domain w
b) = Domain w
b

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

-- | A value of type @'BVDomain' w@ represents a set of bitvectors of
-- width @w@. A BVDomain represents either an arithmetic interval, or
-- a bitwise interval.

data BVDomain (w :: Nat)
  = BVDArith !(A.Domain w)
  | BVDBitwise !(B.Domain w)
  deriving Int -> BVDomain w -> ShowS
forall (w :: Nat). Int -> BVDomain w -> ShowS
forall (w :: Nat). [BVDomain w] -> ShowS
forall (w :: Nat). BVDomain w -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BVDomain w] -> ShowS
$cshowList :: forall (w :: Nat). [BVDomain w] -> ShowS
show :: BVDomain w -> String
$cshow :: forall (w :: Nat). BVDomain w -> String
showsPrec :: Int -> BVDomain w -> ShowS
$cshowsPrec :: forall (w :: Nat). Int -> BVDomain w -> ShowS
Show

-- | Return the bitvector mask value from this domain
bvdMask :: BVDomain w -> Integer
bvdMask :: forall (w :: Nat). BVDomain w -> Integer
bvdMask BVDomain w
x =
  case BVDomain w
x of
    BVDArith Domain w
a   -> forall (w :: Nat). Domain w -> Integer
A.bvdMask Domain w
a
    BVDBitwise Domain w
b -> forall (w :: Nat). Domain w -> Integer
B.bvdMask Domain w
b

-- | Test if the domain satisfies its invariants
proper :: NatRepr w -> BVDomain w -> Bool
proper :: forall (w :: Nat). NatRepr w -> BVDomain w -> Bool
proper NatRepr w
w (BVDArith Domain w
a) = forall (w :: Nat). NatRepr w -> Domain w -> Bool
A.proper NatRepr w
w Domain w
a
proper NatRepr w
w (BVDBitwise Domain w
b) = forall (w :: Nat). NatRepr w -> Domain w -> Bool
B.proper NatRepr w
w Domain w
b

-- | Test if the given integer value is a member of the abstract domain
member :: BVDomain w -> Integer -> Bool
member :: forall (w :: Nat). BVDomain w -> Integer -> Bool
member (BVDArith Domain w
a) Integer
x = forall (w :: Nat). Domain w -> Integer -> Bool
A.member Domain w
a Integer
x
member (BVDBitwise Domain w
a) Integer
x = forall (w :: Nat). Domain w -> Integer -> Bool
B.member Domain w
a Integer
x

-- | Compute how many concrete elements are in the abstract domain
size :: BVDomain w -> Integer
size :: forall (w :: Nat). BVDomain w -> Integer
size (BVDArith Domain w
a)   = forall (w :: Nat). Domain w -> Integer
A.size Domain w
a
size (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> Integer
B.size Domain w
b

-- | Generate a random nonempty domain
genDomain :: NatRepr w -> Gen (BVDomain w)
genDomain :: forall (w :: Nat). NatRepr w -> Gen (BVDomain w)
genDomain NatRepr w
w =
  do Bool
b <- Gen Bool
chooseBool
     if Bool
b then
       forall (w :: Nat). Domain w -> BVDomain w
BVDArith forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Nat). NatRepr w -> Gen (Domain w)
A.genDomain NatRepr w
w
     else
       forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Nat). NatRepr w -> Gen (Domain w)
B.genDomain NatRepr w
w

-- | Generate a random element from a domain, which
--   is assumed to be nonempty
genElement :: BVDomain w -> Gen Integer
genElement :: forall (w :: Nat). BVDomain w -> Gen Integer
genElement (BVDArith Domain w
a) = forall (w :: Nat). Domain w -> Gen Integer
A.genElement Domain w
a
genElement (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> Gen Integer
B.genElement Domain w
b

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

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

-- | Return value if this is a singleton.
asSingleton :: BVDomain w -> Maybe Integer
asSingleton :: forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton (BVDArith Domain w
a)   = forall (w :: Nat). Domain w -> Maybe Integer
A.asSingleton Domain w
a
asSingleton (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> Maybe Integer
B.asSingleton Domain w
b

{- |
 Precondition: @x <= lomask@.  Find the (arithmetically) smallest
 @z@ above @x@ which is bitwise above @lomask@.  In other words
 find the smallest @z@ such that @x <= z@ and @lomask .|. z == z@.
-}
bitwiseRoundAbove ::
  Integer {- ^ @bvmask@, based on the width of the bitvectors in question -} ->
  Integer {- ^ @x@ -} ->
  Integer {- ^ @lomask@ -} ->
  Integer
bitwiseRoundAbove :: Integer -> Integer -> Integer -> Integer
bitwiseRoundAbove Integer
bvmask Integer
x Integer
lomask = Integer
upperbits forall a. Bits a => a -> a -> a
.|. Integer
lowerbits
  where
  upperbits :: Integer
upperbits = Integer
x forall a. Bits a => a -> a -> a
.&. (Integer
bvmask forall a. Bits a => a -> a -> a
`Bits.xor` Integer
fillmask)
  lowerbits :: Integer
lowerbits = Integer
lomask forall a. Bits a => a -> a -> a
.&. Integer
fillmask
  fillmask :: Integer
fillmask = Integer -> Integer
A.fillright ((Integer
x forall a. Bits a => a -> a -> a
.|. Integer
lomask) forall a. Bits a => a -> a -> a
`Bits.xor` Integer
x)

{- |
 Precondition: @lomask <= x <= himask@ and @lomask .|. himask == himask@.
 Find the (arithmetically) smallest @z@ above @x@ which is bitwise between
 @lomask@ and @himask@.  In other words, find the smallest @z@ such that
 @x <= z@ and @lomask .|. z = z@ and @z .|. himask == himask@.
-}
bitwiseRoundBetween ::
  Integer {- ^ @bvmask@, based on the width of the bitvectors in question -} ->
  Integer {- ^ @x@ -} ->
  Integer {- ^ @lomask@ -} ->
  Integer {- ^ @himask@ -} ->
  Integer
bitwiseRoundBetween :: Integer -> Integer -> Integer -> Integer -> Integer
bitwiseRoundBetween Integer
bvmask Integer
x Integer
lomask Integer
himask = Integer
final
  -- read these steps bottom up...
  where
  -- Finally mask out the low bits and only set those required by the lomask
  final :: Integer
final = (Integer
upper forall a. Bits a => a -> a -> a
.&. (Integer
lobits forall a. Bits a => a -> a -> a
`Bits.xor` Integer
bvmask)) forall a. Bits a => a -> a -> a
.|. Integer
lomask

  -- add the correcting bit and mask out any extraneous bits set in
  -- the previous step
  upper :: Integer
upper = (Integer
z forall a. Num a => a -> a -> a
+ Integer
highbit) forall a. Bits a => a -> a -> a
.&. Integer
himask

  -- set ourselves up so that when we add the high bit to correct,
  -- the carry will ripple until it finds a bit position that we
  -- are allowed to set.
  z :: Integer
z = Integer
loup forall a. Bits a => a -> a -> a
.|. Integer
himask'

  -- isolate just the highest incorrect bit
  highbit :: Integer
highbit = Integer
rmask forall a. Bits a => a -> a -> a
`Bits.xor` Integer
lobits

  -- a mask for all the bits to the right of the highest incorrect bit
  lobits :: Integer
lobits = Integer
rmask forall a. Bits a => a -> Int -> a
`shiftR` Int
1

  -- set all the bits to the right of the highest incorrect bit
  rmask :: Integer
rmask = Integer -> Integer
A.fillright Integer
r

  -- now, compute all the bits that are set, but are not
  -- allowed to be set according to the himask
  r :: Integer
r = Integer
loup forall a. Bits a => a -> a -> a
.&. Integer
himask'

  -- complement of the highmask
  himask' :: Integer
himask' = Integer
himask forall a. Bits a => a -> a -> a
`Bits.xor` Integer
bvmask

  -- first, round up to the lomask
  loup :: Integer
loup = Integer -> Integer -> Integer -> Integer
bitwiseRoundAbove Integer
bvmask Integer
x Integer
lomask


-- | Test if an arithmetic domain overlaps with a bitwise domain
mixedDomainsOverlap :: A.Domain a -> B.Domain b -> Bool
mixedDomainsOverlap :: forall (a :: Nat) (b :: Nat). Domain a -> Domain b -> Bool
mixedDomainsOverlap Domain a
a Domain b
b =
   case forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
A.arithDomainData Domain a
a of
     Maybe (Integer, Integer)
Nothing -> forall (w :: Nat). Domain w -> Bool
B.nonempty Domain b
b
     Just (Integer
alo,Integer
_) ->
       let (Integer
lomask,Integer
himask) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain b
b
           brb :: Integer
brb = Integer -> Integer -> Integer -> Integer -> Integer
bitwiseRoundBetween (forall (w :: Nat). Domain w -> Integer
A.bvdMask Domain a
a) Integer
alo Integer
lomask Integer
himask
        in forall (w :: Nat). Domain w -> Bool
B.nonempty Domain b
b Bool -> Bool -> Bool
&& (forall (w :: Nat). Domain w -> Integer -> Bool
A.member Domain a
a Integer
lomask Bool -> Bool -> Bool
|| forall (w :: Nat). Domain w -> Integer -> Bool
A.member Domain a
a Integer
himask Bool -> Bool -> Bool
|| forall (w :: Nat). Domain w -> Integer -> Bool
A.member Domain a
a Integer
brb)


-- | Return true if domains contain a common element.
domainsOverlap :: BVDomain w -> BVDomain w -> Bool
domainsOverlap :: forall (w :: Nat). BVDomain w -> BVDomain w -> Bool
domainsOverlap (BVDBitwise Domain w
a) (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> Domain w -> Bool
B.domainsOverlap Domain w
a Domain w
b
domainsOverlap (BVDArith Domain w
a)   (BVDArith Domain w
b)   = forall (w :: Nat). Domain w -> Domain w -> Bool
A.domainsOverlap Domain w
a Domain w
b
domainsOverlap (BVDArith Domain w
a)   (BVDBitwise Domain w
b) = forall (a :: Nat) (b :: Nat). Domain a -> Domain b -> Bool
mixedDomainsOverlap Domain w
a Domain w
b
domainsOverlap (BVDBitwise Domain w
b) (BVDArith Domain w
a)   = forall (a :: Nat) (b :: Nat). Domain a -> Domain b -> Bool
mixedDomainsOverlap Domain w
a Domain w
b

arithDomainLo :: A.Domain w -> Integer
arithDomainLo :: forall (w :: Nat). Domain w -> Integer
arithDomainLo Domain w
a =
  case forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
A.arithDomainData Domain w
a of
    Maybe (Integer, Integer)
Nothing -> Integer
0
    Just (Integer
lo,Integer
_) -> Integer
lo

mixedCandidates :: A.Domain w -> B.Domain w -> [Integer]
mixedCandidates :: forall (w :: Nat). Domain w -> Domain w -> [Integer]
mixedCandidates Domain w
a Domain w
b =
  case forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
A.arithDomainData Domain w
a of
    Maybe (Integer, Integer)
Nothing -> [ Integer
lomask ]
    Just (Integer
alo,Integer
_) -> [ Integer
lomask, Integer
himask, Integer -> Integer -> Integer -> Integer -> Integer
bitwiseRoundBetween (forall (w :: Nat). Domain w -> Integer
A.bvdMask Domain w
a) Integer
alo Integer
lomask Integer
himask ]
 where
 (Integer
lomask,Integer
himask) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b

-- | Return a list of "candidate" overlap elements.  If two domains
--   overlap, then they will definitely share one of the given
--   values.
overlapCandidates :: BVDomain w -> BVDomain w -> [Integer]
overlapCandidates :: forall (w :: Nat). BVDomain w -> BVDomain w -> [Integer]
overlapCandidates (BVDArith Domain w
a)   (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> Domain w -> [Integer]
mixedCandidates Domain w
a Domain w
b
overlapCandidates (BVDBitwise Domain w
b) (BVDArith Domain w
a)   = forall (w :: Nat). Domain w -> Domain w -> [Integer]
mixedCandidates Domain w
a Domain w
b
overlapCandidates (BVDArith Domain w
a)   (BVDArith Domain w
b)   = [ forall (w :: Nat). Domain w -> Integer
arithDomainLo Domain w
a, forall (w :: Nat). Domain w -> Integer
arithDomainLo Domain w
b ]
overlapCandidates (BVDBitwise Domain w
a) (BVDBitwise Domain w
b) = [ Integer
loa forall a. Bits a => a -> a -> a
.|. Integer
lob ]
  where
  (Integer
loa,Integer
_) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
a
  (Integer
lob,Integer
_) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b


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

-- | Check if all elements in one domain are less than all elements in other.
slt :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> Maybe Bool
slt :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> Maybe Bool
slt NatRepr w
w BVDomain w
a BVDomain w
b = forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Maybe Bool
A.slt NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
b)

-- | Check if all elements in one domain are less than all elements in other.
ult :: (1 <= w) => BVDomain w -> BVDomain w -> Maybe Bool
ult :: forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> Maybe Bool
ult BVDomain w
a BVDomain w
b = forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Maybe Bool
A.ult (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
b)

-- | Return @Just@ if every bitvector in the domain has the same bit
-- at the given index.
testBit ::
  NatRepr w ->
  BVDomain w ->
  Natural {- ^ Index of bit (least-significant bit has index 0) -} ->
  Maybe Bool
testBit :: forall (w :: Nat). NatRepr w -> BVDomain w -> Nat -> Maybe Bool
testBit NatRepr w
_w BVDomain w
a Nat
i = forall (w :: Nat). Domain w -> Nat -> Maybe Bool
B.testBit (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
a) Nat
i

ubounds :: BVDomain w -> (Integer, Integer)
ubounds :: forall (w :: Nat). BVDomain w -> (Integer, Integer)
ubounds BVDomain w
a = forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a)

sbounds :: (1 <= w) => NatRepr w -> BVDomain w -> (Integer, Integer)
sbounds :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> (Integer, Integer)
sbounds NatRepr w
w BVDomain w
a = forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> (Integer, Integer)
A.sbounds NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a)

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

-- | Represents all values
any :: (1 <= w) => NatRepr w -> BVDomain w
any :: forall (w :: Nat). (1 <= w) => NatRepr w -> BVDomain w
any NatRepr w
w = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat). NatRepr w -> Domain w
B.any NatRepr w
w)

-- | Create a bitvector domain representing the integer.
singleton :: (HasCallStack, 1 <= w) => NatRepr w -> Integer -> BVDomain w
singleton :: forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> BVDomain w
singleton NatRepr w
w Integer
x = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
A.singleton NatRepr w
w Integer
x)

-- | @range 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 -> BVDomain w
range :: forall (w :: Nat). NatRepr w -> Integer -> Integer -> BVDomain w
range NatRepr w
w Integer
al Integer
ah = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
A.range NatRepr w
w Integer
al Integer
ah)

-- | Create an abstract domain from an ascending list of elements.
-- The elements are assumed to be distinct.
fromAscEltList :: (1 <= w) => NatRepr w -> [Integer] -> BVDomain w
fromAscEltList :: forall (w :: Nat). (1 <= w) => NatRepr w -> [Integer] -> BVDomain w
fromAscEltList NatRepr w
w [Integer]
xs = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => NatRepr w -> [Integer] -> Domain w
A.fromAscEltList NatRepr w
w [Integer]
xs)

-- | Return union of two domains.
union :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w
union :: forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
union (BVDBitwise Domain w
a) (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union Domain w
a Domain w
b)
union (BVDArith Domain w
a) (BVDArith Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.union Domain w
a Domain w
b)
union (BVDBitwise Domain w
a) (BVDArith Domain w
b) = forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> BVDomain w
mixedUnion Domain w
b Domain w
a
union (BVDArith Domain w
a) (BVDBitwise Domain w
b) = forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> BVDomain w
mixedUnion Domain w
a Domain w
b

mixedUnion :: (1 <= w) => A.Domain w -> B.Domain w  -> BVDomain w
mixedUnion :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> BVDomain w
mixedUnion Domain w
a Domain w
b
  | Just Integer
_ <- forall (w :: Nat). Domain w -> Maybe Integer
A.asSingleton Domain w
a = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union (forall (w :: Nat). Domain w -> Domain w
arithToBitwiseDomain Domain w
a) Domain w
b)
  | Bool
otherwise = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.union Domain w
a (forall (w :: Nat). Domain w -> Domain w
bitwiseToArithDomain Domain w
b))

-- | @concat 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 -> BVDomain u -> NatRepr v -> BVDomain v -> BVDomain (u + v)
concat :: forall (u :: Nat) (v :: Nat).
NatRepr u
-> BVDomain u -> NatRepr v -> BVDomain v -> BVDomain (u + v)
concat NatRepr u
u (BVDArith Domain u
a) NatRepr v
v (BVDArith Domain v
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (u :: Nat) (v :: Nat).
NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
A.concat NatRepr u
u Domain u
a NatRepr v
v Domain v
b)
concat NatRepr u
u (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain u
a) NatRepr v
v (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain v
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (u :: Nat) (v :: Nat).
NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
B.concat NatRepr u
u Domain u
a NatRepr v
v Domain v
b)

-- | @select i n a@ selects @n@ bits starting from index @i@ from @a@.
select ::
  (1 <= n, i + n <= w) =>
  NatRepr i ->
  NatRepr n ->
  BVDomain w -> BVDomain n
select :: forall (n :: Nat) (i :: Nat) (w :: Nat).
(1 <= n, (i + n) <= w) =>
NatRepr i -> NatRepr n -> BVDomain w -> BVDomain n
select NatRepr i
i NatRepr n
n (BVDArith Domain w
a)   = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (n :: Nat) (i :: Nat) (w :: Nat).
(1 <= n, (i + n) <= w) =>
NatRepr i -> NatRepr n -> Domain w -> Domain n
A.select NatRepr i
i NatRepr n
n Domain w
a)
select NatRepr i
i NatRepr n
n (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (n :: Nat) (i :: Nat) (w :: Nat).
(1 <= n, (i + n) <= w) =>
NatRepr i -> NatRepr n -> Domain w -> Domain n
B.select NatRepr i
i NatRepr n
n Domain w
b)

zext :: (1 <= w, w+1 <= u) => BVDomain w -> NatRepr u -> BVDomain u
zext :: forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
BVDomain w -> NatRepr u -> BVDomain u
zext (BVDArith Domain w
a) NatRepr u
u   = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
Domain w -> NatRepr u -> Domain u
A.zext Domain w
a NatRepr u
u)
zext (BVDBitwise Domain w
b) NatRepr u
u = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
Domain w -> NatRepr u -> Domain u
B.zext Domain w
b NatRepr u
u)

sext ::
  forall w u. (1 <= w, w + 1 <= u) =>
  NatRepr w ->
  BVDomain w ->
  NatRepr u ->
  BVDomain u
sext :: forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> BVDomain w -> NatRepr u -> BVDomain u
sext NatRepr w
w (BVDArith Domain w
a) NatRepr u
u   = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> Domain w -> NatRepr u -> Domain u
A.sext NatRepr w
w Domain w
a NatRepr u
u)
sext NatRepr w
w (BVDBitwise Domain w
b) NatRepr u
u = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> Domain w -> NatRepr u -> Domain u
B.sext NatRepr w
w Domain w
b NatRepr u
u)

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

-- An arbitrary value; if we have to union together more than this many
-- bitwise shifts or rotates we'll fall back on some default instead
shiftBound :: Integer
shiftBound :: Integer
shiftBound = Integer
16

shl :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
shl :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
shl NatRepr w
w (BVDBitwise Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b)
  | Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
hi' Bool -> Bool -> Bool
&& Integer
hi' forall a. Num a => a -> a -> a
- Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
shiftBound =
      forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union [ forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
B.shl NatRepr w
w Domain w
a Integer
y | Integer
y <- [Integer
lo .. Integer
hi'] ]
  where
  (Integer
lo, Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds Domain w
b
  hi' :: Integer
hi' = forall a. Ord a => a -> a -> a
max Integer
hi (forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w)

shl NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
A.shl NatRepr w
w Domain w
a Domain w
b)


lshr :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
lshr :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
lshr NatRepr w
w (BVDBitwise Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b)
  | Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
hi' Bool -> Bool -> Bool
&& Integer
hi' forall a. Num a => a -> a -> a
- Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
shiftBound =
      forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union [ forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
B.lshr NatRepr w
w Domain w
a Integer
y | Integer
y <- [Integer
lo .. Integer
hi'] ]
  where
  (Integer
lo, Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds Domain w
b
  hi' :: Integer
hi' = forall a. Ord a => a -> a -> a
max Integer
hi (forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w)

lshr NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
A.lshr NatRepr w
w Domain w
a Domain w
b)



ashr :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
ashr :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
ashr NatRepr w
w (BVDBitwise Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b)
  | Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
hi' Bool -> Bool -> Bool
&& Integer
hi' forall a. Num a => a -> a -> a
- Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
shiftBound =
      forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union [ forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Integer -> Domain w
B.ashr NatRepr w
w Domain w
a Integer
y | Integer
y <- [Integer
lo .. Integer
hi'] ]
  where
  (Integer
lo, Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds Domain w
b
  hi' :: Integer
hi' = forall a. Ord a => a -> a -> a
max Integer
hi (forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w)

ashr NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
A.ashr NatRepr w
w Domain w
a Domain w
b)


rol :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w

-- Special cases, rotating all 0 or all 1 bits makes no difference
rol :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
rol NatRepr w
_w a :: BVDomain w
a@(forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton -> Just Integer
x) BVDomain w
_
  | Integer
x forall a. Eq a => a -> a -> Bool
== Integer
0 = BVDomain w
a
  | Integer
x forall a. Eq a => a -> a -> Bool
== forall (w :: Nat). BVDomain w -> Integer
bvdMask BVDomain w
a = BVDomain w
a

rol NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) =
    if (Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
hi Bool -> Bool -> Bool
&& Integer
hi forall a. Num a => a -> a -> a
- Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
shiftBound) then
      forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union [ forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
B.rol NatRepr w
w Domain w
a Integer
y | Integer
y <- [Integer
lo .. Integer
hi] ]
    else
      forall (w :: Nat). (1 <= w) => NatRepr w -> BVDomain w
any NatRepr w
w

  where
  (Integer
lo, Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.urem Domain w
b (forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
A.singleton NatRepr w
w (forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w)))


ror :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w

-- Special cases, rotating all 0 or all 1 bits makes no difference
ror :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
ror NatRepr w
_w a :: BVDomain w
a@(forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton -> Just Integer
x) BVDomain w
_
  | Integer
x forall a. Eq a => a -> a -> Bool
== Integer
0 = BVDomain w
a
  | Integer
x forall a. Eq a => a -> a -> Bool
== forall (w :: Nat). BVDomain w -> Integer
bvdMask BVDomain w
a = BVDomain w
a

ror NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) =
    if (Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
hi Bool -> Bool -> Bool
&& Integer
hi forall a. Num a => a -> a -> a
- Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
shiftBound) then
      forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union [ forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
B.ror NatRepr w
w Domain w
a Integer
y | Integer
y <- [Integer
lo .. Integer
hi] ]
    else
      forall (w :: Nat). (1 <= w) => NatRepr w -> BVDomain w
any NatRepr w
w

  where
  (Integer
lo, Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.urem Domain w
b (forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
A.singleton NatRepr w
w (forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w)))

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

add :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w
add :: forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
add BVDomain w
a BVDomain w
b
  | Just Integer
0 <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a = BVDomain w
b
  | Just Integer
0 <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b = BVDomain w
a
  | Bool
otherwise = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.add (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
b))

negate :: (1 <= w) => BVDomain w -> BVDomain w
negate :: forall (w :: Nat). (1 <= w) => BVDomain w -> BVDomain w
negate (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => Domain w -> Domain w
A.negate Domain w
a)

scale :: (1 <= w) => Integer -> BVDomain w -> BVDomain w
scale :: forall (w :: Nat). (1 <= w) => Integer -> BVDomain w -> BVDomain w
scale Integer
k BVDomain w
a
  | Integer
k forall a. Eq a => a -> a -> Bool
== Integer
1 = BVDomain w
a
  | Bool
otherwise = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => Integer -> Domain w -> Domain w
A.scale Integer
k (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a))

mul :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w
mul :: forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
mul BVDomain w
a BVDomain w
b
  | Just Integer
1 <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a = BVDomain w
b
  | Just Integer
1 <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b = BVDomain w
a
  | Bool
otherwise = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.mul (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
b))

udiv :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w
udiv :: forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
udiv (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.udiv Domain w
a Domain w
b)

urem :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w
urem :: forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
urem (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.urem Domain w
a Domain w
b)

sdiv :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
sdiv :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
sdiv NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
A.sdiv NatRepr w
w Domain w
a Domain w
b)

srem :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
srem :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
srem NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
A.srem NatRepr w
w Domain w
a Domain w
b)

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

-- | Complement bits in range.
not :: BVDomain w -> BVDomain w
not :: forall (w :: Nat). BVDomain w -> BVDomain w
not (BVDArith Domain w
a) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). Domain w -> Domain w
A.not Domain w
a)
not (BVDBitwise Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat). Domain w -> Domain w
B.not Domain w
b)

and :: BVDomain w -> BVDomain w -> BVDomain w
and :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
and BVDomain w
a BVDomain w
b
  | Just Integer
x <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a, Integer
x forall a. Eq a => a -> a -> Bool
== Integer
mask = BVDomain w
b
  | Just Integer
x <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b, Integer
x forall a. Eq a => a -> a -> Bool
== Integer
mask = BVDomain w
a
  | Bool
otherwise = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat). Domain w -> Domain w -> Domain w
B.and (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
b))
 where
 mask :: Integer
mask = forall (w :: Nat). BVDomain w -> Integer
bvdMask BVDomain w
a

or :: BVDomain w -> BVDomain w -> BVDomain w
or :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
or BVDomain w
a BVDomain w
b
  | Just Integer
0 <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a = BVDomain w
b
  | Just Integer
0 <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b = BVDomain w
a
  | Bool
otherwise = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat). Domain w -> Domain w -> Domain w
B.or (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
b))

xor :: BVDomain w -> BVDomain w -> BVDomain w
xor :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
xor BVDomain w
a BVDomain w
b
  | Just Integer
0 <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a = BVDomain w
b
  | Just Integer
0 <- forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b = BVDomain w
a
  | Bool
otherwise = forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (forall (w :: Nat). Domain w -> Domain w -> Domain w
B.xor (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
a) (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
b))

-------------------------------------------------------------------------------
-- Misc operations

popcnt :: NatRepr w -> BVDomain w -> BVDomain w
popcnt :: forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
popcnt NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
A.range NatRepr w
w Integer
lo Integer
hi)
  where
  (Integer
bitlo, Integer
bithi) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b
  lo :: Integer
lo = forall a. Integral a => a -> Integer
toInteger (forall a. Bits a => a -> Int
Bits.popCount Integer
bitlo)
  hi :: Integer
hi = forall a. Integral a => a -> Integer
toInteger (forall a. Bits a => a -> Int
Bits.popCount Integer
bithi)

clz :: NatRepr w -> BVDomain w -> BVDomain w
clz :: forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
clz NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
A.range NatRepr w
w Integer
lo Integer
hi)
  where
  (Integer
bitlo, Integer
bithi) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b
  lo :: Integer
lo = forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.clz NatRepr w
w Integer
bithi
  hi :: Integer
hi = forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.clz NatRepr w
w Integer
bitlo

ctz :: NatRepr w -> BVDomain w -> BVDomain w
ctz :: forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
ctz NatRepr w
w (forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain w
b) = forall (w :: Nat). Domain w -> BVDomain w
BVDArith (forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
A.range NatRepr w
w Integer
lo Integer
hi)
  where
  (Integer
bitlo, Integer
bithi) = forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b
  lo :: Integer
lo = forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.ctz NatRepr w
w Integer
bithi
  hi :: Integer
hi = forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.ctz NatRepr w
w Integer
bitlo


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

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

correct_arithToBitwise :: NatRepr n -> (A.Domain n, Integer) -> Property
correct_arithToBitwise :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
correct_arithToBitwise NatRepr n
n (Domain n
a,Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
A.member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
B.pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w
arithToBitwiseDomain Domain n
a) Integer
x

correct_bitwiseToArith :: NatRepr n -> (B.Domain n, Integer) -> Property
correct_bitwiseToArith :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
correct_bitwiseToArith NatRepr n
n (Domain n
b,Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
B.member Domain n
b Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
A.pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w
bitwiseToArithDomain Domain n
b) Integer
x

correct_bitwiseToXorDomain :: NatRepr n -> (B.Domain n, Integer) -> Property
correct_bitwiseToXorDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
correct_bitwiseToXorDomain NatRepr n
n (Domain n
b,Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
B.member Domain n
b Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
X.pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w
bitwiseToXorDomain Domain n
b) Integer
x

correct_arithToXorDomain :: NatRepr n -> (A.Domain n, Integer) -> Property
correct_arithToXorDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
correct_arithToXorDomain NatRepr n
n (Domain n
a,Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
A.member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
X.pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w
arithToXorDomain Domain n
a) Integer
x

correct_xorToBitwiseDomain :: NatRepr n -> (X.Domain n, Integer) -> Property
correct_xorToBitwiseDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
correct_xorToBitwiseDomain NatRepr n
n (Domain n
a,Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
X.member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
B.pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w
xorToBitwiseDomain Domain n
a) Integer
x

correct_asXorDomain :: NatRepr n -> (BVDomain n, Integer) -> Property
correct_asXorDomain :: forall (n :: Nat). NatRepr n -> (BVDomain n, Integer) -> Property
correct_asXorDomain NatRepr n
n (BVDomain n
a, Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
X.pmember NatRepr n
n (forall (w :: Nat). BVDomain w -> Domain w
asXorDomain BVDomain n
a) Integer
x

correct_fromXorDomain :: NatRepr n -> (X.Domain n, Integer) -> Property
correct_fromXorDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
correct_fromXorDomain NatRepr n
n (Domain n
a, Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
X.member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). Domain w -> BVDomain w
fromXorDomain Domain n
a) Integer
x


correct_bra1 :: NatRepr n -> Integer -> Integer -> Property
correct_bra1 :: forall (n :: Nat). NatRepr n -> Integer -> Integer -> Property
correct_bra1 NatRepr n
n Integer
x Integer
lomask = Integer
lomask forall a. Ord a => a -> a -> Bool
<= Integer
x forall t. Verifiable t => Bool -> t -> Property
==> (Integer
x forall a. Ord a => a -> a -> Bool
<= Integer
q Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
lomask Integer
q)
 where
 q :: Integer
q = Integer -> Integer -> Integer -> Integer
bitwiseRoundAbove (forall (n :: Nat). NatRepr n -> Integer
maxUnsigned NatRepr n
n) Integer
x Integer
lomask

correct_bra2 :: NatRepr n -> Integer -> Integer -> Integer -> Property
correct_bra2 :: forall (n :: Nat).
NatRepr n -> Integer -> Integer -> Integer -> Property
correct_bra2 NatRepr n
n Integer
x Integer
lomask Integer
q' = (Integer
x forall a. Ord a => a -> a -> Bool
<= Integer
q' Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
lomask Integer
q') forall t. Verifiable t => Bool -> t -> Property
==> Integer
q forall a. Ord a => a -> a -> Bool
<= Integer
q'
 where
 q :: Integer
q = Integer -> Integer -> Integer -> Integer
bitwiseRoundAbove (forall (n :: Nat). NatRepr n -> Integer
maxUnsigned NatRepr n
n) Integer
x Integer
lomask

correct_brb1 :: NatRepr n -> Integer -> Integer -> Integer -> Property
correct_brb1 :: forall (n :: Nat).
NatRepr n -> Integer -> Integer -> Integer -> Property
correct_brb1 NatRepr n
n Integer
x Integer
lomask Integer
himask =
    (Integer -> Integer -> Bool
B.bitle Integer
lomask Integer
himask Bool -> Bool -> Bool
&& Integer
lomask forall a. Ord a => a -> a -> Bool
<= Integer
x Bool -> Bool -> Bool
&& Integer
x forall a. Ord a => a -> a -> Bool
<= Integer
himask) forall t. Verifiable t => Bool -> t -> Property
==>
    (Integer
x forall a. Ord a => a -> a -> Bool
<= Integer
q Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
lomask Integer
q Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
q Integer
himask)
  where
  q :: Integer
q = Integer -> Integer -> Integer -> Integer -> Integer
bitwiseRoundBetween (forall (n :: Nat). NatRepr n -> Integer
maxUnsigned NatRepr n
n) Integer
x Integer
lomask Integer
himask

correct_brb2 :: NatRepr n -> Integer -> Integer -> Integer -> Integer -> Property
correct_brb2 :: forall (n :: Nat).
NatRepr n -> Integer -> Integer -> Integer -> Integer -> Property
correct_brb2 NatRepr n
n Integer
x Integer
lomask Integer
himask Integer
q' =
    (Integer
x forall a. Ord a => a -> a -> Bool
<= Integer
q' Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
lomask Integer
q' Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
q' Integer
himask) forall t. Verifiable t => Bool -> t -> Property
==> Integer
q forall a. Ord a => a -> a -> Bool
<= Integer
q'
  where
  q :: Integer
q = Integer -> Integer -> Integer -> Integer -> Integer
bitwiseRoundBetween (forall (n :: Nat). NatRepr n -> Integer
maxUnsigned NatRepr n
n) Integer
x Integer
lomask Integer
himask

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

correct_ubounds :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_ubounds :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (BVDomain n, Integer) -> Property
correct_ubounds NatRepr n
n (BVDomain n
a,Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
x' Bool -> Bool -> Bool
&& Integer
x' forall a. Ord a => a -> a -> Bool
<= Integer
hi
  where
  x' :: Integer
x' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x
  (Integer
lo,Integer
hi) = forall (w :: Nat). BVDomain w -> (Integer, Integer)
ubounds BVDomain n
a

correct_sbounds :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_sbounds :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (BVDomain n, Integer) -> Property
correct_sbounds NatRepr n
n (BVDomain n
a,Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> Integer
lo forall a. Ord a => a -> a -> Bool
<= Integer
x' Bool -> Bool -> Bool
&& Integer
x' forall a. Ord a => a -> a -> Bool
<= Integer
hi
  where
  x' :: Integer
x' = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x
  (Integer
lo,Integer
hi) = forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> (Integer, Integer)
sbounds NatRepr n
n BVDomain n
a

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

correct_overlap :: BVDomain n -> BVDomain n -> Integer -> Property
correct_overlap :: forall (n :: Nat). BVDomain n -> BVDomain n -> Integer -> Property
correct_overlap BVDomain n
a BVDomain n
b Integer
x =
  forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Bool -> Bool
&& forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> BVDomain w -> Bool
domainsOverlap BVDomain n
a BVDomain n
b

precise_overlap :: BVDomain n -> BVDomain n -> Property
precise_overlap :: forall (n :: Nat). BVDomain n -> BVDomain n -> Property
precise_overlap BVDomain n
a BVDomain n
b =
  forall (w :: Nat). BVDomain w -> BVDomain w -> Bool
domainsOverlap BVDomain n
a BVDomain n
b forall t. Verifiable t => Bool -> t -> Property
==> forall (t :: Type -> Type). Foldable t => t Bool -> Bool
List.or [ forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Bool -> Bool
&& forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
x | Integer
x <- forall (w :: Nat). BVDomain w -> BVDomain w -> [Integer]
overlapCandidates BVDomain n
a BVDomain n
b ]

correct_union :: (1 <= n) => NatRepr n -> BVDomain n -> BVDomain n -> Integer -> Property
correct_union :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> BVDomain n -> BVDomain n -> Integer -> Property
correct_union NatRepr n
n BVDomain n
a BVDomain n
b Integer
x =
  (forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Bool -> Bool
|| forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
x) forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
union BVDomain n
a BVDomain n
b) Integer
x

correct_zero_ext :: (1 <= w, w+1 <= u) => NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property
correct_zero_ext :: forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property
correct_zero_ext NatRepr w
w BVDomain w
a NatRepr u
u Integer
x = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain w
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr u
u (forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
BVDomain w -> NatRepr u -> BVDomain u
zext BVDomain w
a NatRepr u
u) Integer
x'
  where
  x' :: Integer
x' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr w
w Integer
x

correct_sign_ext :: (1 <= w, w+1 <= u) => NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property
correct_sign_ext :: forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property
correct_sign_ext NatRepr w
w BVDomain w
a NatRepr u
u Integer
x = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain w
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr u
u (forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> BVDomain w -> NatRepr u -> BVDomain u
sext NatRepr w
w BVDomain w
a NatRepr u
u) Integer
x'
  where
  x' :: Integer
x' = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr w
w Integer
x

correct_concat :: NatRepr m -> (BVDomain m,Integer) -> NatRepr n -> (BVDomain n,Integer) -> Property
correct_concat :: forall (m :: Nat) (n :: Nat).
NatRepr m
-> (BVDomain m, Integer)
-> NatRepr n
-> (BVDomain n, Integer)
-> Property
correct_concat NatRepr m
m (BVDomain m
a,Integer
x) NatRepr n
n (BVDomain n
b,Integer
y) =
    forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain m
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember (forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr m
m NatRepr n
n) (forall (u :: Nat) (v :: Nat).
NatRepr u
-> BVDomain u -> NatRepr v -> BVDomain v -> BVDomain (u + v)
concat NatRepr m
m BVDomain m
a NatRepr n
n BVDomain n
b) Integer
z
  where
  z :: Integer
z = (Integer
x forall a. Bits a => a -> Int -> a
`shiftL` (forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr n
n)) forall a. Bits a => a -> a -> a
.|. Integer
y

correct_select :: (1 <= n, i + n <= w) =>
  NatRepr i -> NatRepr n -> (BVDomain w, Integer) -> Property
correct_select :: forall (n :: Nat) (i :: Nat) (w :: Nat).
(1 <= n, (i + n) <= w) =>
NatRepr i -> NatRepr n -> (BVDomain w, Integer) -> Property
correct_select NatRepr i
i NatRepr n
n (BVDomain w
a, Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain w
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (n :: Nat) (i :: Nat) (w :: Nat).
(1 <= n, (i + n) <= w) =>
NatRepr i -> NatRepr n -> BVDomain w -> BVDomain n
select NatRepr i
i NatRepr n
n BVDomain w
a) Integer
y
  where
  y :: Integer
y = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n ((Integer
x forall a. Bits a => a -> a -> a
.&. forall (w :: Nat). BVDomain w -> Integer
bvdMask BVDomain w
a) forall a. Bits a => a -> Int -> a
`shiftR` (forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr i
i))

correct_add :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_add :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_add NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
add BVDomain n
a BVDomain n
b) (Integer
x forall a. Num a => a -> a -> a
+ Integer
y)

correct_neg :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_neg :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (BVDomain n, Integer) -> Property
correct_neg NatRepr n
n (BVDomain n
a,Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). (1 <= w) => BVDomain w -> BVDomain w
negate BVDomain n
a) (forall a. Num a => a -> a
Prelude.negate Integer
x)

correct_mul :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_mul :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_mul NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
mul BVDomain n
a BVDomain n
b) (Integer
x forall a. Num a => a -> a -> a
* Integer
y)

correct_scale :: (1 <= n) => NatRepr n -> Integer -> (BVDomain n, Integer) -> Property
correct_scale :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Integer -> (BVDomain n, Integer) -> Property
correct_scale NatRepr n
n Integer
k (BVDomain n
a,Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). (1 <= w) => Integer -> BVDomain w -> BVDomain w
scale Integer
k' BVDomain n
a) (Integer
k' forall a. Num a => a -> a -> a
* Integer
x)
  where
  k' :: Integer
k' = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
k

correct_udiv :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_udiv :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_udiv NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y' forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' forall a. Eq a => a -> a -> Bool
/= Integer
0 forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
udiv BVDomain n
a BVDomain n
b) (Integer
x' forall a. Integral a => a -> a -> a
`quot` Integer
y')
  where
  x' :: Integer
x' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x
  y' :: Integer
y' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y

correct_urem :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_urem :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_urem NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y' forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' forall a. Eq a => a -> a -> Bool
/= Integer
0 forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
urem BVDomain n
a BVDomain n
b) (Integer
x' forall a. Integral a => a -> a -> a
`rem` Integer
y')
  where
  x' :: Integer
x' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x
  y' :: Integer
y' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y

correct_sdiv :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_sdiv :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_sdiv NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) =
    forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y' forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' forall a. Eq a => a -> a -> Bool
/= Integer
0 forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
sdiv NatRepr n
n BVDomain n
a BVDomain n
b) (Integer
x' forall a. Integral a => a -> a -> a
`quot` Integer
y')
  where
  x' :: Integer
x' = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x
  y' :: Integer
y' = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y

correct_srem :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_srem :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_srem NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) =
    forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y' forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' forall a. Eq a => a -> a -> Bool
/= Integer
0 forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
srem NatRepr n
n BVDomain n
a BVDomain n
b) (Integer
x' forall a. Integral a => a -> a -> a
`rem` Integer
y')
  where
  x' :: Integer
x' = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x
  y' :: Integer
y' = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y

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

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

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

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

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

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

correct_ult :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_ult :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_ult NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) =
  forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==>
    case forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> Maybe Bool
ult BVDomain n
a BVDomain n
b of
      Just Bool
True  -> forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x forall a. Ord a => a -> a -> Bool
< forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y
      Just Bool
False -> forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x forall a. Ord a => a -> a -> Bool
>= forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y
      Maybe Bool
Nothing    -> Bool
True

correct_slt :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_slt :: forall (n :: Nat).
(1 <= n) =>
NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_slt NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) =
  forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==>
    case forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> Maybe Bool
slt NatRepr n
n BVDomain n
a BVDomain n
b of
      Just Bool
True  -> forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x forall a. Ord a => a -> a -> Bool
< forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y
      Just Bool
False -> forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x forall a. Ord a => a -> a -> Bool
>= forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y
      Maybe Bool
Nothing    -> Bool
True

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

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

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

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

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

correct_popcnt :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_popcnt :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (BVDomain n, Integer) -> Property
correct_popcnt NatRepr n
n (BVDomain n
a,Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
popcnt NatRepr n
n BVDomain n
a) (forall a. Integral a => a -> Integer
toInteger (forall a. Bits a => a -> Int
Bits.popCount Integer
x))

correct_ctz :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_ctz :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (BVDomain n, Integer) -> Property
correct_ctz NatRepr n
n (BVDomain n
a,Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
ctz NatRepr n
n BVDomain n
a) (forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.ctz NatRepr n
n Integer
x)

correct_clz :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_clz :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (BVDomain n, Integer) -> Property
correct_clz NatRepr n
n (BVDomain n
a,Integer
x) = forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
clz NatRepr n
n BVDomain n
a) (forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.clz NatRepr n
n Integer
x)