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

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

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

    module What4.Utils.BVDomain.Arith
      ( Domain(..)
      , proper
      , bvdMask
      , member
      , pmember
      , interval
      , size
      -- * Projection functions
      , asSingleton
      , ubounds
      , sbounds
      , eq
      , slt
      , ult
      , isUltSumCommonEquiv
      , domainsOverlap
      , arithDomainData
      , bitbounds
      , unknowns
      , fillright
        -- * Operations
      , any
      , singleton
      , range
      , fromAscEltList
      , union
      , concat
      , select
      , zext
      , sext
        -- ** Shifts
      , shl
      , lshr
      , ashr
        -- ** Arithmetic
      , add
      , negate
      , scale
      , mul
      , udiv
      , urem
      , sdiv
      , srem
        -- ** Bitwise
      , What4.Utils.BVDomain.Arith.not

      -- * Correctness properties
      , genDomain
      , genElement
      , genPair
      , correct_any
      , correct_ubounds
      , correct_sbounds
      , correct_singleton
      , correct_overlap
      , correct_union
      , correct_zero_ext
      , correct_sign_ext
      , correct_concat
      , correct_shrink
      , correct_trunc
      , correct_select
      , correct_add
      , correct_neg
      , correct_mul
      , correct_scale
      , correct_scale_eq
      , correct_udiv
      , correct_urem
      , correct_sdivRange
      , correct_sdiv
      , correct_srem
      , correct_not
      , correct_shl
      , correct_lshr
      , correct_ashr
      , correct_eq
      , correct_ult
      , correct_slt
      , correct_isUltSumCommonEquiv
      , correct_unknowns
      , correct_bitbounds
      ) where

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

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

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

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

    -- | A value of type @'BVDomain' w@ represents a set of bitvectors of
    -- width @w@. Each 'BVDomain' can represent a single contiguous
    -- interval of bitvectors that may wrap around from -1 to 0.
    data Domain (w :: Nat)
      = BVDAny !Integer
      -- ^ The set of all bitvectors of width @w@. Argument caches @2^w-1@.
      | BVDInterval !Integer !Integer !Integer
      -- ^ Intervals are represented by a starting value and a size.
      -- @BVDInterval mask l d@ represents the set of values of the form
      -- @x mod 2^w@ for @x@ such that @l <= x <= l + d@. It should
      -- satisfy the invariants @0 <= l < 2^w@ and @0 <= d < 2^w@. The
      -- first argument caches the value @2^w-1@.
      deriving Int -> Domain w -> ShowS
    [Domain w] -> ShowS
    Domain w -> String
    (Int -> Domain w -> ShowS)
    -> (Domain w -> String) -> ([Domain w] -> ShowS) -> Show (Domain w)
    forall (w :: Nat). Int -> Domain w -> ShowS
    forall (w :: Nat). [Domain w] -> ShowS
    forall (w :: Nat). Domain w -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall (w :: Nat). Int -> Domain w -> ShowS
    showsPrec :: Int -> Domain w -> ShowS
    $cshow :: forall (w :: Nat). Domain w -> String
    show :: Domain w -> String
    $cshowList :: forall (w :: Nat). [Domain w] -> ShowS
    showList :: [Domain w] -> ShowS
    Show

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

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

    -- | Test if the given integer value is a member of the abstract domain
    member :: Domain w -> Integer -> Bool
    member :: forall (w :: Nat). Domain w -> Integer -> Bool
    member (BVDAny Integer
    _) Integer
    _ = Bool
    True
    member (BVDInterval Integer
    mask Integer
    lo Integer
    sz) Integer
    x = ((Integer
    x' Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    lo) Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. Integer
    mask) Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    sz
      where x' :: Integer
    x' = Integer
    x Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. Integer
    mask

    -- | Check if the domain satisfies its invariants
    proper :: NatRepr w -> Domain w -> Bool
    proper :: forall (w :: Nat). NatRepr w -> Domain w -> Bool
    proper NatRepr w
    w (BVDAny Integer
    mask) = Integer
    mask Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == NatRepr w -> Integer
    forall (w :: Nat). NatRepr w -> Integer
    maxUnsigned NatRepr w
    w
    proper NatRepr w
    w (BVDInterval Integer
    mask Integer
    lo Integer
    sz) =
      Integer
    mask Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == NatRepr w -> Integer
    forall (w :: Nat). NatRepr w -> Integer
    maxUnsigned NatRepr w
    w Bool -> Bool -> Bool
    &&
      Integer
    lo Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .|. Integer
    mask Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    mask Bool -> Bool -> Bool
    &&
      Integer
    sz Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .|. Integer
    mask Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    mask Bool -> Bool -> Bool
    &&
      Integer
    sz Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    mask

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

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

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

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

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

    -- | @halfRange n@ returns @2^(n-1)@.
    halfRange :: (1 <= w) => NatRepr w -> Integer
    halfRange :: forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
    halfRange NatRepr w
    w = Int -> Integer
    forall a. Bits a => Int -> a
    bit (NatRepr w -> Int
    forall (n :: Nat). NatRepr n -> Int
    widthVal NatRepr w
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)

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

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

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

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

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

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

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

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

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

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

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

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

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

    -- | Represents all values
    any :: (1 <= w) => NatRepr w -> Domain w
    any :: forall (w :: Nat). (1 <= w) => NatRepr w -> Domain w
    any NatRepr w
    w = Integer -> Domain w
    forall (w :: Nat). Integer -> Domain w
    BVDAny (NatRepr w -> Integer
    forall (w :: Nat). NatRepr w -> Integer
    maxUnsigned NatRepr w
    w)

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

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

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

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

    -- | Return union of two domains.
    union :: (1 <= w) => Domain w -> Domain w -> Domain w
    union :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
    union Domain w
    a Domain w
    b =
      case Domain w
    a of
        BVDAny Integer
    _ -> Domain w
    a
        BVDInterval Integer
    _ Integer
    al Integer
    aw ->
          case Domain w
    b of
            BVDAny Integer
    _ -> Domain w
    b
            BVDInterval Integer
    mask Integer
    bl Integer
    bw ->
              Integer -> Integer -> Integer -> Domain w
    forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
    interval Integer
    mask Integer
    cl (Integer
    ch Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    cl)
              where
                sz :: Integer
    sz = Integer
    mask Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1
                ac :: Integer
    ac = Integer
    2 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    al Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    aw -- twice the average value of a
                bc :: Integer
    bc = Integer
    2 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    bl Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    bw -- twice the average value of b
                -- If the averages are 2^(w-1) or more apart,
                -- then shift the lower interval up by 2^w.
                al' :: Integer
    al' = if Integer
    ac Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    mask Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    bc then Integer
    al Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    sz else Integer
    al
                bl' :: Integer
    bl' = if Integer
    bc Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    mask Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    ac then Integer
    bl Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    sz else Integer
    bl
                ah' :: Integer
    ah' = Integer
    al' Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    aw
                bh' :: Integer
    bh' = Integer
    bl' Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    bw
                cl :: Integer
    cl = Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    min Integer
    al' Integer
    bl'
                ch :: Integer
    ch = Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    ah' Integer
    bh'

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

    -- | @shrink i a@ drops the @i@ least significant bits from @a@.
    shrink ::
      NatRepr i ->
      Domain (i + n) -> Domain n
    shrink :: forall (i :: Nat) (n :: Nat).
    NatRepr i -> Domain (i + n) -> Domain n
    shrink NatRepr i
    i Domain (i + n)
    a =
      case Domain (i + n)
    a of
        BVDAny Integer
    mask -> Integer -> Domain n
    forall (w :: Nat). Integer -> Domain w
    BVDAny (Integer -> Integer
    shr Integer
    mask)
        BVDInterval Integer
    mask Integer
    al Integer
    aw ->
          Integer -> Integer -> Integer -> Domain n
    forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
    interval (Integer -> Integer
    shr Integer
    mask) Integer
    bl (Integer
    bh Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    bl)
          where
            bl :: Integer
    bl = Integer -> Integer
    shr Integer
    al
            bh :: Integer
    bh = Integer -> Integer
    shr (Integer
    al Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    aw)
      where
        shr :: Integer -> Integer
    shr Integer
    x = Integer
    x Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftR` NatRepr i -> Int
    forall (n :: Nat). NatRepr n -> Int
    widthVal NatRepr i
    i

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    udiv :: (1 <= w) => Domain w -> Domain w -> Domain w
    udiv :: forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
    udiv Domain w
    a Domain w
    b = Integer -> Integer -> Integer -> Domain w
    forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
    interval Integer
    mask Integer
    ql (Integer
    qh Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    ql)
      where
        mask :: Integer
    mask = Domain w -> Integer
    forall (w :: Nat). Domain w -> Integer
    bvdMask Domain w
    a
        (Integer
    al, Integer
    ah) = Domain w -> (Integer, Integer)
    forall (w :: Nat). Domain w -> (Integer, Integer)
    ubounds Domain w
    a
        (Integer
    bl, Integer
    bh) = Domain w -> (Integer, Integer)
    forall (w :: Nat). Domain w -> (Integer, Integer)
    ubounds Domain w
    b
        ql :: Integer
    ql = Integer
    al Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    1 Integer
    bh -- assume that division by 0 does not happen
        qh :: Integer
    qh = Integer
    ah Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    1 Integer
    bl -- assume that division by 0 does not happen

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

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

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

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

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

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

    srem :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w
    srem :: forall (w :: Nat).
    (1 <= w) =>
    NatRepr w -> Domain w -> Domain w -> Domain w
    srem NatRepr w
    w Domain w
    a Domain w
    b =
      -- If the quotient is a singleton @q@, then we compute the remainder
      -- @r = a - q*b@.
      if Integer
    ql Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    qh then
        (if Integer
    ql Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    0
         then Integer -> Integer -> Integer -> Domain w
    forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
    interval Integer
    mask (Integer
    al Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    ql Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    bl) (Integer
    aw Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    ql Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    bw)
         else Integer -> Integer -> Integer -> Domain w
    forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
    interval Integer
    mask (Integer
    al Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    ql Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    bh) (Integer
    aw Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    ql Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    bw))
      -- Otherwise the range of possible remainders is determined by the
      -- modulus and the sign of the first argument.
      else Integer -> Integer -> Integer -> Domain w
    forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
    interval Integer
    mask Integer
    rl (Integer
    rh Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    rl)
      where
        mask :: Integer
    mask = Domain w -> Integer
    forall (w :: Nat). Domain w -> Integer
    bvdMask Domain w
    a
        (Integer
    al, Integer
    ah) = NatRepr w -> Domain w -> (Integer, Integer)
    forall (w :: Nat).
    (1 <= w) =>
    NatRepr w -> Domain w -> (Integer, Integer)
    sbounds NatRepr w
    w Domain w
    a
        (Integer
    bl, Integer
    bh) = NatRepr w -> Domain w -> (Integer, Integer)
    forall (w :: Nat).
    (1 <= w) =>
    NatRepr w -> Domain w -> (Integer, Integer)
    sbounds NatRepr w
    w Domain w
    b
        (Integer
    ql, Integer
    qh) = (Integer, Integer) -> ReciprocalRange -> (Integer, Integer)
    sdivRange (Integer
    al, Integer
    ah) (NatRepr w -> Domain w -> ReciprocalRange
    forall (w :: Nat).
    (1 <= w) =>
    NatRepr w -> Domain w -> ReciprocalRange
    rbounds NatRepr w
    w Domain w
    b)
        rl :: Integer
    rl = if Integer
    al Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    0 then Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    min (Integer
    blInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1) (-Integer
    bhInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1) else Integer
    0
        rh :: Integer
    rh = if Integer
    ah Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0 then Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max (-Integer
    blInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1) (Integer
    bhInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1) else Integer
    0
        aw :: Integer
    aw = Integer
    ah Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    al
        bw :: Integer
    bw = Integer
    bh Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    bl

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

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

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

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

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

    -- | @fillright x@ rounds up @x@ to the nearest 2^n-1.
    fillright :: Integer -> Integer
    fillright :: Integer -> Integer
    fillright = Int -> Integer -> Integer
    go Int
    1
      where
      go :: Int -> Integer -> Integer
      go :: Int -> Integer -> Integer
    go Int
    i Integer
    x
        | Integer
    x' Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    x = Integer
    x
        | Bool
    otherwise = Int -> Integer -> Integer
    go (Int
    2 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * Int
    i) Integer
    x'
        where x' :: Integer
    x' = Integer
    x Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .|. (Integer
    x Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftR` Int
    i)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    correct_scale_eq :: (1 <= n) => NatRepr n -> Integer -> Domain n -> Property
    correct_scale_eq :: forall (n :: Nat).
    (1 <= n) =>
    NatRepr n -> Integer -> Domain n -> Property
    correct_scale_eq NatRepr n
    n Integer
    k Domain n
    a = Bool -> Property
    property (Bool -> Property) -> Bool -> Property
    forall a b. (a -> b) -> a -> b
    $ Domain n -> Domain n -> Bool
    forall (w :: Nat). Domain w -> Domain w -> Bool
    sameDomain (Integer -> Domain n -> Domain n
    forall (w :: Nat). (1 <= w) => Integer -> Domain w -> Domain w
    scale Integer
    k' Domain n
    a) (Domain n -> Domain n -> Domain n
    forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
    mul (NatRepr n -> Integer -> Domain n
    forall (w :: Nat).
    (HasCallStack, 1 <= w) =>
    NatRepr w -> Integer -> Domain w
    singleton NatRepr n
    n Integer
    k) Domain n
    a)
      where
      k' :: Integer
    k' = NatRepr n -> Integer -> Integer
    forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
    toSigned NatRepr n
    n Integer
    k

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

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

    correct_sdivRange :: (Integer, Integer) -> (Integer, Integer) -> Integer -> Integer -> Property
    correct_sdivRange :: (Integer, Integer)
    -> (Integer, Integer) -> Integer -> Integer -> Property
    correct_sdivRange (Integer, Integer)
    a (Integer, Integer)
    b Integer
    x Integer
    y =
       (Integer, Integer) -> Integer -> Bool
    forall {a}. Ord a => (a, a) -> a -> Bool
    mem (Integer, Integer)
    a Integer
    x Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> (Integer, Integer) -> Integer -> Bool
    forall {a}. Ord a => (a, a) -> a -> Bool
    mem (Integer, Integer)
    b Integer
    y Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> Integer
    y Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    0 Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> (Integer, Integer) -> Integer -> Bool
    forall {a}. Ord a => (a, a) -> a -> Bool
    mem ((Integer, Integer) -> ReciprocalRange -> (Integer, Integer)
    sdivRange (Integer, Integer)
    a ReciprocalRange
    b') (Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `quot` Integer
    y)
     where
     b' :: ReciprocalRange
    b' = Integer -> Integer -> ReciprocalRange
    ReciprocalRange ((Integer, Integer) -> Integer
    forall a b. (a, b) -> b
    snd (Integer, Integer)
    b) ((Integer, Integer) -> Integer
    forall a b. (a, b) -> a
    fst (Integer, Integer)
    b)
     mem :: (a, a) -> a -> Bool
    mem (a
    lo,a
    hi) a
    v = a
    lo a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    <= a
    v Bool -> Bool -> Bool
    && a
    v a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    <= a
    hi

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

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

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

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

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

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

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

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

    correct_isUltSumCommonEquiv ::
      (1 <= n) =>
      NatRepr n ->
      (Domain n, Integer) ->
      (Domain n, Integer) ->
      (Domain n, Integer) ->
      Property
    correct_isUltSumCommonEquiv :: forall (n :: Nat).
    (1 <= n) =>
    NatRepr n
    -> (Domain n, Integer)
    -> (Domain n, Integer)
    -> (Domain n, Integer)
    -> Property
    correct_isUltSumCommonEquiv NatRepr n
    n (Domain n
    a, Integer
    x) (Domain n
    b, Integer
    y) (Domain n
    c, Integer
    z) =
      Domain n -> Integer -> Bool
    forall (w :: Nat). Domain w -> Integer -> Bool
    member Domain n
    a Integer
    x Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> Domain n -> Integer -> Bool
    forall (w :: Nat). Domain w -> Integer -> Bool
    member Domain n
    b Integer
    y Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> Domain n -> Integer -> Bool
    forall (w :: Nat). Domain w -> Integer -> Bool
    member Domain n
    c Integer
    z Bool -> Property -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==>
        Domain n -> Domain n -> Domain n -> Bool
    forall (w :: Nat). Domain w -> Domain w -> Domain w -> Bool
    isUltSumCommonEquiv Domain n
    a Domain n
    b Domain n
    c Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==>
          ((NatRepr n -> Integer -> Integer
    forall (w :: Nat). NatRepr w -> Integer -> Integer
    toUnsigned NatRepr n
    n (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    z) Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr n -> Integer -> Integer
    forall (w :: Nat). NatRepr w -> Integer -> Integer
    toUnsigned NatRepr n
    n (Integer
    y Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    z)) Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == (NatRepr n -> Integer -> Integer
    forall (w :: Nat). NatRepr w -> Integer -> Integer
    toUnsigned NatRepr n
    n Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr n -> Integer -> Integer
    forall (w :: Nat). NatRepr w -> Integer -> Integer
    toUnsigned NatRepr n
    n Integer
    y))

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

    correct_bitbounds :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Property
    correct_bitbounds :: forall (n :: Nat).
    (1 <= n) =>
    NatRepr n -> (Domain n, Integer) -> Property
    correct_bitbounds NatRepr n
    n (Domain n
    a,Integer
    x) =
        Domain n -> Integer -> Bool
    forall (w :: Nat). Domain w -> Integer -> Bool
    member Domain n
    a Integer
    x Bool -> Bool -> Property
    forall t. Verifiable t => Bool -> t -> Property
    ==> (Integer -> Integer -> Bool
    bitle Integer
    lo Integer
    x' Bool -> Bool -> Bool
    && Integer -> Integer -> Bool
    bitle Integer
    x' Integer
    hi Bool -> Bool -> Bool
    && Integer -> Integer -> Bool
    bitle Integer
    hi (NatRepr n -> Integer
    forall (w :: Nat). NatRepr w -> Integer
    maxUnsigned NatRepr n
    n))
      where
      x' :: Integer
    x' = NatRepr n -> Integer -> Integer
    forall (w :: Nat). NatRepr w -> Integer -> Integer
    toUnsigned NatRepr n
    n Integer
    x
      (Integer
    lo, Integer
    hi) = Domain n -> (Integer, Integer)
    forall (w :: Nat). Domain w -> (Integer, Integer)
    bitbounds Domain n
    a