    {-|
    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
      , isUltSumCommonEquiv
      , 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 = Domain w -> Integer
    forall (w :: Nat). Domain w -> Integer
    A.bvdMask Domain w
    a in
      case Domain w -> Maybe (Integer, Integer)
    forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
    A.arithDomainData Domain w
    a of
        Maybe (Integer, Integer)
    Nothing -> Integer -> Integer -> Integer -> Domain w
    forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
    B.interval Integer
    mask Integer
    0 Integer
    mask
        Just (Integer
    alo,Integer
    _) -> Integer -> Integer -> Integer -> Domain w
    forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
    B.interval Integer
    mask Integer
    lo Integer
    hi
          where
            u :: Integer
    u = Domain w -> Integer
    forall (w :: Nat). Domain w -> Integer
    A.unknowns Domain w
    a
            hi :: Integer
    hi = Integer
    alo Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .|. Integer
    u
            lo :: Integer
    lo = Integer
    hi Integer -> Integer -> Integer
    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 = Integer -> Integer -> Integer -> Domain w
    forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
    A.interval Integer
    mask Integer
    lo ((Integer
    hi Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    lo) Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. Integer
    mask)
      where
      mask :: Integer
    mask = Domain w -> Integer
    forall (w :: Nat). Domain w -> Integer
    B.bvdMask Domain w
    b
      (Integer
    lo,Integer
    hi) = Domain w -> (Integer, Integer)
    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 = Integer -> Integer -> Integer -> Domain w
    forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
    X.interval Integer
    mask Integer
    lo Integer
    hi
      where
      mask :: Integer
    mask = Domain w -> Integer
    forall (w :: Nat). Domain w -> Integer
    B.bvdMask Domain w
    b
      (Integer
    lo,Integer
    hi) = Domain w -> (Integer, Integer)
    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 = Domain w -> Integer
    forall (w :: Nat). Domain w -> Integer
    A.bvdMask Domain w
    a in
      case Domain w -> Maybe (Integer, Integer)
    forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
    A.arithDomainData Domain w
    a of
        Maybe (Integer, Integer)
    Nothing -> Integer -> Integer -> Integer -> Domain w
    forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
    X.BVDXor Integer
    mask Integer
    mask Integer
    mask
        Just (Integer
    alo,Integer
    _) -> Integer -> Integer -> Integer -> Domain w
    forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
    X.BVDXor Integer
    mask Integer
    hi Integer
    u
          where
            u :: Integer
    u = Domain w -> Integer
    forall (w :: Nat). Domain w -> Integer
    A.unknowns Domain w
    a
            hi :: Integer
    hi = Integer
    alo Integer -> Integer -> Integer
    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 = Integer -> Integer -> Integer -> Domain w
    forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
    B.interval Integer
    mask Integer
    lo Integer
    hi
      where
      mask :: Integer
    mask = Domain w -> Integer
    forall (w :: Nat). Domain w -> Integer
    X.bvdMask Domain w
    x
      (Integer
    lo, Integer
    hi) = Domain w -> (Integer, Integer)
    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) = Domain w -> Domain w
    forall (w :: Nat). Domain w -> Domain w
    arithToXorDomain Domain w
    a
    asXorDomain (BVDBitwise Domain w
    b) = Domain w -> Domain w
    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 = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDBitwise (Domain w -> Domain w
    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) = Domain w -> Domain w
    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)   = Domain w -> Domain w
    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
    [BVDomain w] -> ShowS
    BVDomain w -> String
    (Int -> BVDomain w -> ShowS)
    -> (BVDomain w -> String)
    -> ([BVDomain w] -> ShowS)
    -> Show (BVDomain w)
    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
    $cshowsPrec :: forall (w :: Nat). Int -> BVDomain w -> ShowS
    showsPrec :: Int -> BVDomain w -> ShowS
    $cshow :: forall (w :: Nat). BVDomain w -> String
    show :: BVDomain w -> String
    $cshowList :: forall (w :: Nat). [BVDomain w] -> ShowS
    showList :: [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   -> Domain w -> Integer
    forall (w :: Nat). Domain w -> Integer
    A.bvdMask Domain w
    a
        BVDBitwise Domain w
    b -> Domain w -> Integer
    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) = NatRepr w -> Domain w -> Bool
    forall (w :: Nat). NatRepr w -> Domain w -> Bool
    A.proper NatRepr w
    w Domain w
    a
    proper NatRepr w
    w (BVDBitwise Domain w
    b) = NatRepr w -> Domain w -> Bool
    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 = Domain w -> Integer -> Bool
    forall (w :: Nat). Domain w -> Integer -> Bool
    A.member Domain w
    a Integer
    x
    member (BVDBitwise Domain w
    a) Integer
    x = Domain w -> Integer -> Bool
    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)   = Domain w -> Integer
    forall (w :: Nat). Domain w -> Integer
    A.size Domain w
    a
    size (BVDBitwise Domain w
    b) = Domain w -> Integer
    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 b <- Gen Bool
    chooseBool
         if b then
           BVDArith <$> A.genDomain w
         else
           BVDBitwise <$> B.genDomain 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) = Domain w -> Gen Integer
    forall (w :: Nat). Domain w -> Gen Integer
    A.genElement Domain w
    a
    genElement (BVDBitwise Domain w
    b) = Domain w -> Gen Integer
    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 a <- NatRepr w -> Gen (BVDomain w)
    forall (w :: Nat). NatRepr w -> Gen (BVDomain w)
    genDomain NatRepr w
    w
         x <- genElement a
         return (a,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)   = Domain w -> Maybe Integer
    forall (w :: Nat). Domain w -> Maybe Integer
    A.asSingleton Domain w
    a
    asSingleton (BVDBitwise Domain w
    b) = Domain w -> Maybe Integer
    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 Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .|. Integer
    lowerbits
      where
      upperbits :: Integer
    upperbits = Integer
    x Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. (Integer
    bvmask Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    `Bits.xor` Integer
    fillmask)
      lowerbits :: Integer
    lowerbits = Integer
    lomask Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. Integer
    fillmask
      fillmask :: Integer
    fillmask = Integer -> Integer
    A.fillright ((Integer
    x Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .|. Integer
    lomask) Integer -> Integer -> Integer
    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 Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. (Integer
    lobits Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    `Bits.xor` Integer
    bvmask)) Integer -> Integer -> Integer
    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 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    highbit) Integer -> Integer -> Integer
    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 Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .|. Integer
    himask'

      -- isolate just the highest incorrect bit
      highbit :: Integer
    highbit = Integer
    rmask Integer -> Integer -> Integer
    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 Integer -> Int -> Integer
    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 Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. Integer
    himask'

      -- complement of the highmask
      himask' :: Integer
    himask' = Integer
    himask Integer -> Integer -> Integer
    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 Domain a -> Maybe (Integer, Integer)
    forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
    A.arithDomainData Domain a
    a of
         Maybe (Integer, Integer)
    Nothing -> Domain b -> Bool
    forall (w :: Nat). Domain w -> Bool
    B.nonempty Domain b
    b
         Just (Integer
    alo,Integer
    _) ->
           let (Integer
    lomask,Integer
    himask) = Domain b -> (Integer, Integer)
    forall (w :: Nat). Domain w -> (Integer, Integer)
    B.bitbounds Domain b
    b
               brb :: Integer
    brb = Integer -> Integer -> Integer -> Integer -> Integer
    bitwiseRoundBetween (Domain a -> Integer
    forall (w :: Nat). Domain w -> Integer
    A.bvdMask Domain a
    a) Integer
    alo Integer
    lomask Integer
    himask
            in Domain b -> Bool
    forall (w :: Nat). Domain w -> Bool
    B.nonempty Domain b
    b Bool -> Bool -> Bool
    && (Domain a -> Integer -> Bool
    forall (w :: Nat). Domain w -> Integer -> Bool
    A.member Domain a
    a Integer
    lomask Bool -> Bool -> Bool
    || Domain a -> Integer -> Bool
    forall (w :: Nat). Domain w -> Integer -> Bool
    A.member Domain a
    a Integer
    himask Bool -> Bool -> Bool
    || Domain a -> Integer -> 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) = Domain w -> Domain w -> Bool
    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)   = Domain w -> Domain w -> Bool
    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) = Domain w -> Domain w -> Bool
    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)   = Domain w -> Domain w -> Bool
    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 Domain w -> Maybe (Integer, Integer)
    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 Domain w -> Maybe (Integer, Integer)
    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 (Domain w -> Integer
    forall (w :: Nat). Domain w -> Integer
    A.bvdMask Domain w
    a) Integer
    alo Integer
    lomask Integer
    himask ]
     where
     (Integer
    lomask,Integer
    himask) = Domain w -> (Integer, Integer)
    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) = Domain w -> Domain w -> [Integer]
    forall (w :: Nat). Domain w -> Domain w -> [Integer]
    mixedCandidates Domain w
    a Domain w
    b
    overlapCandidates (BVDBitwise Domain w
    b) (BVDArith Domain w
    a)   = Domain w -> Domain w -> [Integer]
    forall (w :: Nat). Domain w -> Domain w -> [Integer]
    mixedCandidates Domain w
    a Domain w
    b
    overlapCandidates (BVDArith Domain w
    a)   (BVDArith Domain w
    b)   = [ Domain w -> Integer
    forall (w :: Nat). Domain w -> Integer
    arithDomainLo Domain w
    a, Domain w -> Integer
    forall (w :: Nat). Domain w -> Integer
    arithDomainLo Domain w
    b ]
    overlapCandidates (BVDBitwise Domain w
    a) (BVDBitwise Domain w
    b) = [ Integer
    loa Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .|. Integer
    lob ]
      where
      (Integer
    loa,Integer
    _) = Domain w -> (Integer, Integer)
    forall (w :: Nat). Domain w -> (Integer, Integer)
    B.bitbounds Domain w
    a
      (Integer
    lob,Integer
    _) = Domain w -> (Integer, 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 <- BVDomain w -> Maybe Integer
    forall (w :: Nat). BVDomain w -> Maybe Integer
    asSingleton BVDomain w
    a
      , Just Integer
    y <- BVDomain w -> Maybe Integer
    forall (w :: Nat). BVDomain w -> Maybe Integer
    asSingleton BVDomain 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)
      | BVDomain w -> BVDomain w -> Bool
    forall (w :: Nat). BVDomain w -> BVDomain w -> Bool
    domainsOverlap BVDomain w
    a BVDomain 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 -> 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 = NatRepr w -> Domain w -> Domain w -> Maybe Bool
    forall (w :: Nat).
    (1 <= w) =>
    NatRepr w -> Domain w -> Domain w -> Maybe Bool
    A.slt NatRepr w
    w (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain BVDomain w
    a) (BVDomain w -> Domain w
    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 = Domain w -> Domain w -> Maybe Bool
    forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Maybe Bool
    A.ult (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain BVDomain w
    a) (BVDomain w -> Domain w
    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 = Domain w -> Nat -> Maybe Bool
    forall (w :: Nat). Domain w -> Nat -> Maybe Bool
    B.testBit (BVDomain w -> Domain w
    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 = Domain w -> (Integer, Integer)
    forall (w :: Nat). Domain w -> (Integer, Integer)
    A.ubounds (BVDomain w -> Domain w
    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 = NatRepr w -> Domain w -> (Integer, Integer)
    forall (w :: Nat).
    (1 <= w) =>
    NatRepr w -> Domain w -> (Integer, Integer)
    A.sbounds NatRepr w
    w (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain BVDomain w
    a)

    -- | Check if (bvult (bvadd a c) (bvadd b c)) is equivalent to (bvult a b)
    isUltSumCommonEquiv :: BVDomain w -> BVDomain w -> BVDomain w -> Bool
    isUltSumCommonEquiv :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w -> Bool
    isUltSumCommonEquiv BVDomain w
    a BVDomain w
    b BVDomain w
    c =
      Domain w -> Domain w -> Domain w -> Bool
    forall (w :: Nat). Domain w -> Domain w -> Domain w -> Bool
    A.isUltSumCommonEquiv (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain BVDomain w
    a) (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain BVDomain w
    b) (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain BVDomain w
    c)

    --------------------------------------------------------------------------------
    -- 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 = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDBitwise (NatRepr w -> Domain w
    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 = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (NatRepr w -> Integer -> Domain w
    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 = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (NatRepr w -> Integer -> Integer -> Domain w
    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 = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (NatRepr w -> [Integer] -> Domain w
    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) = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDBitwise (Domain w -> Domain w -> Domain w
    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) = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (Domain w -> Domain w -> Domain w
    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) = Domain w -> Domain w -> BVDomain w
    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) = Domain w -> Domain w -> BVDomain w
    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
    _ <- Domain w -> Maybe Integer
    forall (w :: Nat). Domain w -> Maybe Integer
    A.asSingleton Domain w
    a = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDBitwise (Domain w -> Domain w -> Domain w
    forall (w :: Nat). Domain w -> Domain w -> Domain w
    B.union (Domain w -> Domain w
    forall (w :: Nat). Domain w -> Domain w
    arithToBitwiseDomain Domain w
    a) Domain w
    b)
      | Bool
    otherwise = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (Domain w -> Domain w -> Domain w
    forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
    A.union Domain w
    a (Domain w -> Domain w
    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) = Domain (u + v) -> BVDomain (u + v)
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
    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 (BVDomain u -> Domain u
    forall (w :: Nat). BVDomain w -> Domain w
    asBitwiseDomain -> Domain u
    a) NatRepr v
    v (BVDomain v -> Domain v
    forall (w :: Nat). BVDomain w -> Domain w
    asBitwiseDomain -> Domain v
    b) = Domain (u + v) -> BVDomain (u + v)
    forall (w :: Nat). Domain w -> BVDomain w
    BVDBitwise (NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
    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)   = Domain n -> BVDomain n
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (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
    A.select NatRepr i
    i NatRepr n
    n Domain w
    a)
    select NatRepr i
    i NatRepr n
    n (BVDBitwise Domain w
    b) = Domain n -> BVDomain n
    forall (w :: Nat). Domain w -> BVDomain w
    BVDBitwise (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
    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   = Domain u -> BVDomain u
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (Domain w -> NatRepr u -> Domain u
    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 = Domain u -> BVDomain u
    forall (w :: Nat). Domain w -> BVDomain w
    BVDBitwise (Domain w -> NatRepr u -> Domain u
    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   = Domain u -> BVDomain u
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (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
    A.sext NatRepr w
    w Domain w
    a NatRepr u
    u)
    sext NatRepr w
    w (BVDBitwise Domain w
    b) NatRepr u
    u = Domain u -> BVDomain u
    forall (w :: Nat). Domain w -> BVDomain w
    BVDBitwise (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
    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) (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain -> Domain w
    b)
      | Integer
    lo Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    hi' Bool -> Bool -> Bool
    && Integer
    hi' Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    lo Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    shiftBound =
          Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDBitwise (Domain w -> BVDomain w) -> Domain w -> BVDomain w
    forall a b. (a -> b) -> a -> b
    $ (Domain w -> Domain w -> Domain w) -> [Domain w] -> Domain w
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: Type -> Type) a.
    Foldable t =>
    (a -> a -> a) -> t a -> a
    foldl1 Domain w -> Domain w -> Domain w
    forall (w :: Nat). Domain w -> Domain w -> Domain w
    B.union [ NatRepr w -> Domain w -> Integer -> Domain w
    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) = Domain w -> (Integer, Integer)
    forall (w :: Nat). Domain w -> (Integer, Integer)
    A.ubounds Domain w
    b
      hi' :: Integer
    hi' = Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    hi (NatRepr w -> Integer
    forall (n :: Nat). NatRepr n -> Integer
    intValue NatRepr w
    w)

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

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

    ashr NatRepr w
    w (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain -> Domain w
    a) (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain -> Domain w
    b) = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (NatRepr w -> Domain w -> Domain w -> Domain w
    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@(BVDomain w -> Maybe Integer
    forall (w :: Nat). BVDomain w -> Maybe Integer
    asSingleton -> Just Integer
    x) BVDomain w
    _
      | Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 = BVDomain w
    a
      | Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == BVDomain w -> Integer
    forall (w :: Nat). BVDomain w -> Integer
    bvdMask BVDomain w
    a = BVDomain w
    a

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

      where
      (Integer
    lo, Integer
    hi) = Domain w -> (Integer, Integer)
    forall (w :: Nat). Domain w -> (Integer, Integer)
    A.ubounds (Domain w -> Domain w -> Domain w
    forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
    A.urem Domain w
    b (NatRepr w -> Integer -> Domain w
    forall (w :: Nat).
    (HasCallStack, 1 <= w) =>
    NatRepr w -> Integer -> Domain w
    A.singleton NatRepr w
    w (NatRepr w -> Integer
    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@(BVDomain w -> Maybe Integer
    forall (w :: Nat). BVDomain w -> Maybe Integer
    asSingleton -> Just Integer
    x) BVDomain w
    _
      | Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 = BVDomain w
    a
      | Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == BVDomain w -> Integer
    forall (w :: Nat). BVDomain w -> Integer
    bvdMask BVDomain w
    a = BVDomain w
    a

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

      where
      (Integer
    lo, Integer
    hi) = Domain w -> (Integer, Integer)
    forall (w :: Nat). Domain w -> (Integer, Integer)
    A.ubounds (Domain w -> Domain w -> Domain w
    forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
    A.urem Domain w
    b (NatRepr w -> Integer -> Domain w
    forall (w :: Nat).
    (HasCallStack, 1 <= w) =>
    NatRepr w -> Integer -> Domain w
    A.singleton NatRepr w
    w (NatRepr w -> Integer
    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 <- BVDomain w -> Maybe Integer
    forall (w :: Nat). BVDomain w -> Maybe Integer
    asSingleton BVDomain w
    a = BVDomain w
    b
      | Just Integer
    0 <- BVDomain w -> Maybe Integer
    forall (w :: Nat). BVDomain w -> Maybe Integer
    asSingleton BVDomain w
    b = BVDomain w
    a
      | Bool
    otherwise = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (Domain w -> Domain w -> Domain w
    forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
    A.add (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain BVDomain w
    a) (BVDomain w -> Domain w
    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 (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain -> Domain w
    a) = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (Domain w -> Domain w
    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 Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    1 = BVDomain w
    a
      | Bool
    otherwise = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (Integer -> Domain w -> Domain w
    forall (w :: Nat). (1 <= w) => Integer -> Domain w -> Domain w
    A.scale Integer
    k (BVDomain w -> Domain w
    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 <- BVDomain w -> Maybe Integer
    forall (w :: Nat). BVDomain w -> Maybe Integer
    asSingleton BVDomain w
    a = BVDomain w
    b
      | Just Integer
    1 <- BVDomain w -> Maybe Integer
    forall (w :: Nat). BVDomain w -> Maybe Integer
    asSingleton BVDomain w
    b = BVDomain w
    a
      | Bool
    otherwise = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (Domain w -> Domain w -> Domain w
    forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
    A.mul (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain BVDomain w
    a) (BVDomain w -> Domain w
    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 (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain -> Domain w
    a) (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain -> Domain w
    b) = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (Domain w -> Domain w -> Domain w
    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 (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain -> Domain w
    a) (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain -> Domain w
    b) = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (Domain w -> Domain w -> Domain w
    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 (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain -> Domain w
    a) (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain -> Domain w
    b) = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (NatRepr w -> Domain w -> Domain w -> Domain w
    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 (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain -> Domain w
    a) (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asArithDomain -> Domain w
    b) = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (NatRepr w -> Domain w -> Domain w -> Domain w
    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) = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (Domain w -> Domain w
    forall (w :: Nat). Domain w -> Domain w
    A.not Domain w
    a)
    not (BVDBitwise Domain w
    b) = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDBitwise (Domain w -> Domain w
    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 <- BVDomain w -> Maybe Integer
    forall (w :: Nat). BVDomain w -> Maybe Integer
    asSingleton BVDomain w
    a, Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    mask = BVDomain w
    b
      | Just Integer
    x <- BVDomain w -> Maybe Integer
    forall (w :: Nat). BVDomain w -> Maybe Integer
    asSingleton BVDomain w
    b, Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    mask = BVDomain w
    a
      | Bool
    otherwise = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDBitwise (Domain w -> Domain w -> Domain w
    forall (w :: Nat). Domain w -> Domain w -> Domain w
    B.and (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asBitwiseDomain BVDomain w
    a) (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asBitwiseDomain BVDomain w
    b))
     where
     mask :: Integer
    mask = BVDomain w -> Integer
    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 <- BVDomain w -> Maybe Integer
    forall (w :: Nat). BVDomain w -> Maybe Integer
    asSingleton BVDomain w
    a = BVDomain w
    b
      | Just Integer
    0 <- BVDomain w -> Maybe Integer
    forall (w :: Nat). BVDomain w -> Maybe Integer
    asSingleton BVDomain w
    b = BVDomain w
    a
      | Bool
    otherwise = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDBitwise (Domain w -> Domain w -> Domain w
    forall (w :: Nat). Domain w -> Domain w -> Domain w
    B.or (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asBitwiseDomain BVDomain w
    a) (BVDomain w -> Domain w
    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 <- BVDomain w -> Maybe Integer
    forall (w :: Nat). BVDomain w -> Maybe Integer
    asSingleton BVDomain w
    a = BVDomain w
    b
      | Just Integer
    0 <- BVDomain w -> Maybe Integer
    forall (w :: Nat). BVDomain w -> Maybe Integer
    asSingleton BVDomain w
    b = BVDomain w
    a
      | Bool
    otherwise = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDBitwise (Domain w -> Domain w -> Domain w
    forall (w :: Nat). Domain w -> Domain w -> Domain w
    B.xor (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asBitwiseDomain BVDomain w
    a) (BVDomain w -> Domain w
    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 (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asBitwiseDomain -> Domain w
    b) = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (NatRepr w -> Integer -> Integer -> Domain w
    forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
    A.range NatRepr w
    w Integer
    lo Integer
    hi)
      where
      (Integer
    bitlo, Integer
    bithi) = Domain w -> (Integer, Integer)
    forall (w :: Nat). Domain w -> (Integer, Integer)
    B.bitbounds Domain w
    b
      lo :: Integer
    lo = Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Integer -> Int
    forall a. Bits a => a -> Int
    Bits.popCount Integer
    bitlo)
      hi :: Integer
    hi = Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Integer -> Int
    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 (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asBitwiseDomain -> Domain w
    b) = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (NatRepr w -> Integer -> Integer -> Domain w
    forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
    A.range NatRepr w
    w Integer
    lo Integer
    hi)
      where
      (Integer
    bitlo, Integer
    bithi) = Domain w -> (Integer, Integer)
    forall (w :: Nat). Domain w -> (Integer, Integer)
    B.bitbounds Domain w
    b
      lo :: Integer
    lo = NatRepr w -> Integer -> Integer
    forall (w :: Nat). NatRepr w -> Integer -> Integer
    Arith.clz NatRepr w
    w Integer
    bithi
      hi :: Integer
    hi = NatRepr w -> Integer -> Integer
    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 (BVDomain w -> Domain w
    forall (w :: Nat). BVDomain w -> Domain w
    asBitwiseDomain -> Domain w
    b) = Domain w -> BVDomain w
    forall (w :: Nat). Domain w -> BVDomain w
    BVDArith (NatRepr w -> Integer -> Integer -> Domain w
    forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
    A.range NatRepr w
    w Integer
    lo Integer
    hi)
      where
      (Integer
    bitlo, Integer
    bithi) = Domain w -> (Integer, Integer)
    forall (w :: Nat). Domain w -> (Integer, Integer)
    B.bitbounds Domain w
    b
      lo :: Integer
    lo = NatRepr w -> Integer -> Integer
    forall (w :: Nat). NatRepr w -> Integer -> Integer
    Arith.ctz NatRepr w
    w Integer
    bithi
      hi :: Integer
    hi = NatRepr w -> Integer -> Integer
    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 = NatRepr n -> BVDomain n -> Bool
    forall (w :: Nat). NatRepr w -> BVDomain w -> Bool
    proper NatRepr n
    n BVDomain n
    a Bool -> Bool -> Bool
    && BVDomain n -> Integer -> 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) = Domain n -> Integer -> Bool
    forall (w :: Nat). Domain w -> Integer -> Bool
    A.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
    B.pmember NatRepr n
    n (Domain n -> Domain 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) = Domain n -> Integer -> Bool
    forall (w :: Nat). Domain w -> Integer -> Bool
    B.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
    A.pmember NatRepr n
    n (Domain n -> Domain 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) = Domain n -> Integer -> Bool
    forall (w :: Nat). Domain w -> Integer -> Bool
    B.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
    X.pmember NatRepr n
    n (Domain n -> Domain 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) = Domain n -> Integer -> Bool
    forall (w :: Nat). Domain w -> Integer -> Bool
    A.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
    X.pmember NatRepr n
    n (Domain n -> Domain 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) = Domain n -> Integer -> Bool
    forall (w :: Nat). Domain w -> Integer -> Bool
    X.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
    B.pmember NatRepr n
    n (Domain n -> Domain 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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain 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
    X.pmember NatRepr n
    n (BVDomain n -> Domain 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) = Domain n -> Integer -> Bool
    forall (w :: Nat). Domain w -> Integer -> Bool
    X.member Domain n
    a Integer
    x Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (Domain n -> BVDomain 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 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    x Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> (Integer
    x Integer -> Integer -> Bool
    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 (NatRepr n -> Integer
    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 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    q' Bool -> Bool -> Bool
    && Integer -> Integer -> Bool
    B.bitle Integer
    lomask Integer
    q') Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> Integer
    q Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    q'
     where
     q :: Integer
    q = Integer -> Integer -> Integer -> Integer
    bitwiseRoundAbove (NatRepr n -> Integer
    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 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
    himask) Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==>
        (Integer
    x Integer -> Integer -> Bool
    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 (NatRepr n -> Integer
    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 Integer -> Integer -> Bool
    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) Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> Integer
    q Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    q'
      where
      q :: Integer
    q = Integer -> Integer -> Integer -> Integer -> Integer
    bitwiseRoundBetween (NatRepr n -> Integer
    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 (NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (NatRepr n -> BVDomain 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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain 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) = BVDomain n -> (Integer, Integer)
    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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain 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 -> BVDomain n -> (Integer, Integer)
    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 (BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member (NatRepr n -> Integer -> BVDomain n
    forall (w :: Nat).
    (HasCallStack, 1 <= w) =>
    NatRepr w -> Integer -> BVDomain 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 :: 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 =
      BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Bool -> Bool
    && BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    x Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> BVDomain n -> Bool
    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 =
      BVDomain n -> BVDomain n -> Bool
    forall (w :: Nat). BVDomain w -> BVDomain w -> Bool
    domainsOverlap BVDomain n
    a BVDomain n
    b Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> [Bool] -> Bool
    forall (t :: Type -> Type). Foldable t => t Bool -> Bool
    List.or [ BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Bool -> Bool
    && BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    x | Integer
    x <- BVDomain n -> BVDomain n -> [Integer]
    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 =
      (BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Bool -> Bool
    || BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    x) Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (BVDomain n -> BVDomain n -> BVDomain 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 = BVDomain w -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain w
    a Integer
    x' Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr u -> BVDomain u -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr u
    u (BVDomain w -> NatRepr u -> BVDomain 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' = 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 -> 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 = BVDomain w -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain w
    a Integer
    x' Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr u -> BVDomain u -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr u
    u (NatRepr w -> BVDomain w -> NatRepr u -> BVDomain 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' = NatRepr w -> Integer -> Integer
    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) =
        BVDomain m -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain m
    a Integer
    x Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    y Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr (m + n) -> BVDomain (m + n) -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain 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
    -> BVDomain m -> NatRepr n -> BVDomain n -> BVDomain (m + 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 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_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) = BVDomain w -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain w
    a Integer
    x Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (NatRepr i -> NatRepr n -> BVDomain w -> BVDomain 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 = 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
    .&. BVDomain w -> Integer
    forall (w :: Nat). BVDomain w -> Integer
    bvdMask BVDomain 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 -> (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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    y Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (BVDomain n -> BVDomain n -> BVDomain n
    forall (w :: Nat).
    (1 <= w) =>
    BVDomain w -> BVDomain w -> BVDomain w
    add BVDomain n
    a BVDomain n
    b) (Integer
    x Integer -> Integer -> Integer
    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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (BVDomain n -> BVDomain n
    forall (w :: Nat). (1 <= w) => BVDomain w -> BVDomain w
    negate BVDomain n
    a) (Integer -> Integer
    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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    y Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (BVDomain n -> BVDomain n -> BVDomain n
    forall (w :: Nat).
    (1 <= w) =>
    BVDomain w -> BVDomain w -> BVDomain w
    mul BVDomain n
    a BVDomain n
    b) (Integer
    x Integer -> Integer -> Integer
    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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (Integer -> BVDomain n -> BVDomain n
    forall (w :: Nat). (1 <= w) => Integer -> BVDomain w -> BVDomain w
    scale Integer
    k' BVDomain 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_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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x' Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain 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 -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (BVDomain n -> BVDomain n -> BVDomain n
    forall (w :: Nat).
    (1 <= w) =>
    BVDomain w -> BVDomain w -> BVDomain w
    udiv BVDomain n
    a BVDomain 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 -> (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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x' Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain 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 -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (BVDomain n -> BVDomain n -> BVDomain n
    forall (w :: Nat).
    (1 <= w) =>
    BVDomain w -> BVDomain w -> BVDomain w
    urem BVDomain n
    a BVDomain n
    b) (Integer
    x' Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `rem` Integer
    y')
      where
      x' :: Integer
    x' = NatRepr n -> Integer -> Integer
    forall (w :: Nat). NatRepr w -> Integer -> Integer
    toUnsigned NatRepr n
    n Integer
    x
      y' :: Integer
    y' = NatRepr n -> Integer -> Integer
    forall (w :: Nat). NatRepr w -> Integer -> Integer
    toUnsigned NatRepr n
    n Integer
    y

    correct_sdiv :: (1 <= n) => NatRepr n -> (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) =
        BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x' Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain 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 -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (NatRepr n -> BVDomain n -> BVDomain n -> BVDomain 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' 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 -> (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) =
        BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x' Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain 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 -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (NatRepr n -> BVDomain n -> BVDomain n -> BVDomain 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' 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 -> (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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    y Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (NatRepr n -> BVDomain n -> BVDomain n -> BVDomain 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 = (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 (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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    y Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (NatRepr n -> BVDomain n -> BVDomain n -> BVDomain 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 = (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 (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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    y Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (NatRepr n -> BVDomain n -> BVDomain n -> BVDomain 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 = (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 (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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    y Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (NatRepr n -> BVDomain n -> BVDomain n -> BVDomain n
    forall (w :: Nat).
    (1 <= w) =>
    NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
    rol NatRepr n
    n BVDomain n
    a BVDomain n
    b) (NatRepr n -> Integer -> Integer -> Integer
    forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
    Arith.rotateLeft NatRepr n
    n Integer
    x Integer
    y)

    correct_ror :: (1 <= n) => NatRepr n -> (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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    y Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (NatRepr n -> BVDomain n -> BVDomain n -> BVDomain n
    forall (w :: Nat).
    (1 <= w) =>
    NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
    ror NatRepr n
    n BVDomain n
    a BVDomain n
    b) (NatRepr n -> Integer -> Integer -> Integer
    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) =
      BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    y Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==>
        case BVDomain n -> BVDomain n -> Maybe Bool
    forall (w :: Nat). BVDomain w -> BVDomain w -> Maybe Bool
    eq BVDomain n
    a BVDomain 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 -> (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) =
      BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    y Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==>
        case BVDomain n -> BVDomain n -> Maybe Bool
    forall (w :: Nat).
    (1 <= w) =>
    BVDomain w -> BVDomain w -> Maybe Bool
    ult BVDomain n
    a BVDomain 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 -> (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) =
      BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    y Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==>
        case NatRepr n -> BVDomain n -> BVDomain n -> Maybe Bool
    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  -> 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_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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (BVDomain n -> BVDomain n
    forall (w :: Nat). BVDomain w -> BVDomain w
    not BVDomain n
    a) (Integer -> Integer
    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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    y Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (BVDomain n -> BVDomain n -> BVDomain n
    forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
    and BVDomain n
    a BVDomain n
    b) (Integer
    x Integer -> Integer -> Integer
    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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    y Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (BVDomain n -> BVDomain n -> BVDomain n
    forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
    or BVDomain n
    a BVDomain n
    b) (Integer
    x Integer -> Integer -> Integer
    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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    b Integer
    y Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (BVDomain n -> BVDomain n -> BVDomain n
    forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
    xor BVDomain n
    a BVDomain n
    b) (Integer
    x Integer -> Integer -> Integer
    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 Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr n -> Nat
    forall (n :: Nat). NatRepr n -> Nat
    natValue NatRepr n
    n Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==>
        case NatRepr n -> BVDomain n -> Nat -> Maybe Bool
    forall (w :: Nat). NatRepr w -> BVDomain w -> Nat -> Maybe Bool
    testBit NatRepr n
    n BVDomain n
    a Nat
    i of
          Just Bool
    True  -> Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    Bits.testBit Integer
    x (Nat -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Nat
    i)
          Just Bool
    False -> Bool -> Bool
    Prelude.not (Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    Bits.testBit Integer
    x (Nat -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Nat
    i))
          Maybe Bool
    Nothing    -> Bool
    True

    correct_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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (NatRepr n -> BVDomain n -> BVDomain n
    forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
    popcnt NatRepr n
    n BVDomain n
    a) (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Integer -> Int
    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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (NatRepr n -> BVDomain n -> BVDomain n
    forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
    ctz NatRepr n
    n BVDomain n
    a) (NatRepr n -> Integer -> Integer
    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) = BVDomain n -> Integer -> Bool
    forall (w :: Nat). BVDomain w -> Integer -> Bool
    member BVDomain n
    a Integer
    x Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> BVDomain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
    pmember NatRepr n
    n (NatRepr n -> BVDomain n -> BVDomain n
    forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
    clz NatRepr n
    n BVDomain n
    a) (NatRepr n -> Integer -> Integer
    forall (w :: Nat). NatRepr w -> Integer -> Integer
    Arith.clz NatRepr n
    n Integer
    x)