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

    Provides a bitwise implementation of bitvector abstract domains.
    -}

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

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

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

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

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

    import qualified What4.Utils.Arithmetic as Arith

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    -- | @select i n a@ selects @n@ bits starting from index @i@ from @a@.
    select ::
      (1 <= n, i + n <= w) =>
      NatRepr i ->
      NatRepr n ->
      Domain w -> Domain n
    select :: forall (n :: Nat) (i :: Nat) (w :: Nat).
    (1 <= n, (i + n) <= w) =>
    NatRepr i -> NatRepr n -> Domain w -> Domain n
    select NatRepr i
    i NatRepr n
    n Domain w
    a = NatRepr i -> Domain (i + n) -> Domain n
    forall (i :: Nat) (n :: Nat).
    NatRepr i -> Domain (i + n) -> Domain n
    shrink NatRepr i
    i (NatRepr (i + n) -> Domain w -> Domain (i + n)
    forall (n :: Nat) (w :: Nat).
    (n <= w) =>
    NatRepr n -> Domain w -> Domain n
    trunc (NatRepr i -> NatRepr n -> NatRepr (i + n)
    forall (m :: Nat) (n :: Nat).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    addNat NatRepr i
    i NatRepr n
    n) Domain w
    a)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    correct_trunc :: (n <= w) => NatRepr n -> (Domain w, Integer) -> Property
    correct_trunc :: forall (n :: Nat) (w :: Nat).
    (n <= w) =>
    NatRepr n -> (Domain w, Integer) -> Property
    correct_trunc NatRepr n
    n (Domain w
    a,Integer
    x) = Domain w -> Integer -> Bool
    forall (w :: Nat). Domain w -> Integer -> Bool
    member Domain w
    a Integer
    x' Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> NatRepr n -> Domain n -> Integer -> Bool
    forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
    pmember NatRepr n
    n (NatRepr n -> Domain w -> Domain n
    forall (n :: Nat) (w :: Nat).
    (n <= w) =>
    NatRepr n -> Domain w -> Domain n
    trunc NatRepr n
    n Domain w
    a) (NatRepr n -> Integer -> Integer
    forall (w :: Nat). NatRepr w -> Integer -> Integer
    toUnsigned NatRepr n
    n Integer
    x')
      where
      x' :: Integer
    x' = Integer
    x Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. Domain w -> Integer
    forall (w :: Nat). Domain w -> Integer
    bvdMask Domain w
    a

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

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

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

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

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

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

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

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

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

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

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

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