{-|
Module      : What4.Domains.BV.Bitwise.Tnum
Copyright   : (c) Galois Inc, 2026
License     : BSD3
Maintainer  : langston@galois.com

Tristate-numbers as used in the eBPF verifier.

Used by the bitwise abstract domain to implement arithmetic operations.

A tristate number ('Tnum') is a pair of bitvectors @(v, m)@ where @v@ records
the bits known to be 1 and @m@ records the bits whose value is unknown. The two
are required to be disjoint. The set of concrete bitvectors represented by @(v,
m)@ is @{ v .|. (x .&. m) | x <- all bitvectors }@ — equivalently, the bitwise
abstract-domain element with bit-pattern bounds @(v, v .|. m)@.

This module is for internal use by 'What4.Domains.BV.Bitwise' only and is not
part of the public API.

For 'add' and 'mul', see "Sound, Precise, and Fast Abstract Interpretation with
Tristate Numbers" https://arxiv.org/abs/2105.05398.

For 'udiv' and 'urem', see "Program Analysis Combining Generalized Bit-Level
and Word-Level Abstractions " https://dl.acm.org/doi/abs/10.1145/3728905, and
especially their Clam code artifact https://zenodo.org/records/14001988.
-}

{-# LANGUAGE BangPatterns #-}

module What4.Domains.BV.Bitwise.Tnum
  ( Tnum
  , tnumValue
  , tnumMask
  , mk
  , add
  , mul
  , mulPrecise
  , udiv
  , urem
  ) where

import qualified Control.Exception as X
import           Data.Bits

import           What4.Domains.Arithmetic (bitsBelow, isPow2Integer)

-- | A tristate-number representation.
--
-- The two fields are required to be disjoint (@tnumValue .&. tnumMask == 0@);
-- 'mk' enforces this with an 'X.assert'.
data Tnum = Tnum
  { Tnum -> Integer
tnumValue :: !Integer
    -- ^ The known-1 bits.
  , Tnum -> Integer
tnumMask  :: !Integer
    -- ^ The unknown bits.
  }

-- | /O(w)/. Smart constructor that asserts the disjointness invariant
-- (@v .&. m == 0@).
mk :: Integer -> Integer -> Tnum
mk :: Integer -> Integer -> Tnum
mk Integer
v Integer
m = Bool -> Tnum -> Tnum
forall a. (?callStack::CallStack) => Bool -> a -> a
X.assert (Integer
v Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0) (Integer -> Integer -> Tnum
Tnum Integer
v Integer
m)
{-# INLINE mk #-}

-- | /O(w)/. Tristate-number add, with the result truncated to @bvmask@.
add ::
  Integer {- ^ bvmask -} ->
  Tnum {- ^ a -} ->
  Tnum {- ^ b -} ->
  Tnum
add :: Integer -> Tnum -> Tnum -> Tnum
add Integer
bvmask (Tnum Integer
av Integer
am) (Tnum Integer
bv Integer
bm) = Integer -> Integer -> Tnum
mk Integer
resv Integer
resm
  where
  sm :: Integer
sm    = Integer
am Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
bm
  sv :: Integer
sv    = Integer
av Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
bv
  sigma :: Integer
sigma = Integer
sm Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
sv
  chi :: Integer
chi   = Integer
sigma Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
sv
  resm :: Integer
resm  = (Integer
chi Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
am Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
bm) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask
  resv :: Integer
resv  = (Integer
sv Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
resm) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask
{-# INLINE add #-}

-- | /O(w)/. Tristate-number multiply via interval and trailing-zero analysis.
--
-- The result has:
--
--   * at least @ctzA + ctzB@ trailing zero bits, where @ctzA@ is the longest
--     prefix of low bits that are known-zero in @a@ (i.e.\ both 'tnumValue' and
--     'tnumMask' have that bit clear), and similarly for @ctzB@; and
--   * known bits derived from the arithmetic interval @[aMin*bMin, aMax*bMax]@
--     reduced modulo @bvmask+1@ (see 'wrappedKnownBitsOfInterval'). When the
--     interval fits within one modulus, bits above the highest disagreement
--     between the wrapped bounds are determined; when it crosses a modulus
--     boundary once, we recover bits the two halves agree on; if it spans a
--     full modulus, no high bits are determined.
--
-- Special case: when both operands are concrete singletons (mask == 0), the
-- result is the exact concrete product.
mul ::
  Integer {- ^ bvmask -} ->
  Tnum {- ^ a -} ->
  Tnum {- ^ b -} ->
  Tnum
mul :: Integer -> Tnum -> Tnum -> Tnum
mul Integer
bvmask (Tnum Integer
av Integer
am) (Tnum Integer
bv Integer
bm)
  | Integer
am Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0, Integer
bm Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Integer -> Integer -> Tnum
mk ((Integer
av Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
bv) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask) Integer
0
  | Bool
otherwise = Integer -> Integer -> Tnum
mk (Integer
resValue Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask) (Integer
resUnknown Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask)
  where
  -- Trailing-zero analysis: ctz(value | mask) is the lowest bit that is not
  -- known-zero in each operand.
  ctzA :: Int
ctzA = Integer -> Int
countTrailingZerosOr0 (Integer
av Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
am)
  ctzB :: Int
ctzB = Integer -> Int
countTrailingZerosOr0 (Integer
bv Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
bm)
  trailZ :: Int
trailZ = Int
ctzA Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
ctzB
  -- Interval analysis: the product lies in [aMin*bMin, aMax*bMax] (computed
  -- in unbounded Integer). 'wrappedKnownBitsOfInterval' reduces this modulo
  -- @bvmask+1@ and extracts known bits whether or not the interval crosses a
  -- modulus boundary.
  prodMin :: Integer
prodMin = Integer
av Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
bv
  prodMax :: Integer
prodMax = (Integer
av Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
am) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* (Integer
bv Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
bm)
  (Integer
highValue, Integer
highUnknown) = Integer -> Integer -> Integer -> (Integer, Integer)
wrappedKnownBitsOfInterval Integer
bvmask Integer
prodMin Integer
prodMax
  -- Low-bit multiplication (LLVM KnownBits::mul trick):
  -- (x * y) mod 2^k depends only on (x mod 2^k) and (y mod 2^k) — carries
  -- propagate upward, not downward. So if we know the low nA bits of A and
  -- low nB bits of B, we know the low min(nA,nB) bits of A*B exactly, and
  -- they equal (av * bv) mod 2^min(nA,nB) since the unknown bits are all
  -- above those positions. Combined with trailing zeros: resultBitsKnown =
  -- min(nA,nB) + ctzA + ctzB. See @lemma_mul_low_bits@ in bitsdomain.cry.
  w :: Int
w = Integer -> Int
forall a. Bits a => a -> Int
popCount Integer
bvmask
  trailBitsKnownA :: Int
trailBitsKnownA = if Integer
am Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Int
w else Integer -> Int
countTrailingZerosOr0 Integer
am
  trailBitsKnownB :: Int
trailBitsKnownB = if Integer
bm Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Int
w else Integer -> Int
countTrailingZerosOr0 Integer
bm
  smallestOperand :: Int
smallestOperand =
    Bool -> Int -> Int
forall a. (?callStack::CallStack) => Bool -> a -> a
X.assert (Int
trailBitsKnownA Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
ctzA Bool -> Bool -> Bool
&& Int
trailBitsKnownB Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
ctzB) (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$
    Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (Int
trailBitsKnownA Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
ctzA) (Int
trailBitsKnownB Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
ctzB)
  resultBitsKnown :: Int
resultBitsKnown = Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (Int
smallestOperand Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
trailZ) Int
w
  bottomKnown :: Integer
bottomKnown = Integer
prodMin  -- av * bv
  lowKnownMask :: Integer
lowKnownMask = (Int -> Integer
forall a. Bits a => Int -> a
bit Int
resultBitsKnown Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask
  -- Combine interval analysis with low-bit knowledge via intersection:
  -- unknown only where BOTH are unknown; value is the OR of both known values.
  resUnknown :: Integer
resUnknown = Integer
highUnknown Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
lowKnownMask
  resValue :: Integer
resValue = (Integer
highValue Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. (Integer
bottomKnown Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
lowKnownMask)) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
resUnknown
{-# INLINE mul #-}

-- | /O(w)/. @knownBitsOfInterval lo hi@ analyzes the arithmetic interval @[lo, hi]@
-- (where @0 <= lo <= hi@) and returns @(value, mask)@ in tnum form: the bits
-- on which all values in @[lo, hi]@ agree are known (recorded in @value@),
-- and the bits below the highest disagreement are unknown (set in @mask@).
--
-- For example, if @lo = 0b1100@ and @hi = 0b1110@, every value in
-- @[lo, hi]@ has bits 3 and 2 set; bits 1 and 0 vary. So @value = 0b1100@
-- and @mask = 0b0011@.
--
-- This subsumes leading-zero analysis (when @lo = 0@) and adds leading-1
-- (and arbitrary leading-prefix) analysis when @lo > 0@.
knownBitsOfInterval :: Integer -> Integer -> (Integer, Integer)
knownBitsOfInterval :: Integer -> Integer -> (Integer, Integer)
knownBitsOfInterval Integer
lo Integer
hi = (Integer
lo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
varying, Integer
varying)
  where
  -- Bits at-or-below the highest position where lo and hi disagree.
  varying :: Integer
varying = Integer -> Integer
bitsBelow (Integer
lo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
hi)
{-# INLINE knownBitsOfInterval #-}

-- | /O(w)/. Like 'knownBitsOfInterval', but for the image of @[lo, hi]@ under
-- reduction modulo @bvmask + 1@ (where @0 <= lo <= hi@ and @bvmask@ is of the
-- form @2^w - 1@).
--
-- Three cases:
--
--   * @hi - lo + 1 >= bvmask + 1@: the image covers every residue, so no bits
--     are determined (returns @(0, bvmask)@).
--   * @lo \`quot\` (bvmask+1) == hi \`quot\` (bvmask+1)@: the interval fits
--     entirely within one modulus, so the wrapped bounds @lo \`rem\` (bvmask+1)@
--     and @hi \`rem\` (bvmask+1)@ are still ordered and we use
--     'knownBitsOfInterval' on them.
--   * Otherwise the interval crosses exactly one modulus boundary: the image is
--     @[wLo, bvmask] \\cup [0, wHi]@ where @wLo = lo \`rem\` (bvmask+1)@ and
--     @wHi = hi \`rem\` (bvmask+1)@. We analyze each half with
--     'knownBitsOfInterval' and join: a bit is known only when both halves
--     agree on it.
wrappedKnownBitsOfInterval :: Integer -> Integer -> Integer -> (Integer, Integer)
wrappedKnownBitsOfInterval :: Integer -> Integer -> Integer -> (Integer, Integer)
wrappedKnownBitsOfInterval Integer
bvmask Integer
lo Integer
hi
  | Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
modulus = (Integer
0, Integer
bvmask)
  | Integer
wLo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
wHi = Integer -> Integer -> (Integer, Integer)
knownBitsOfInterval Integer
wLo Integer
wHi
  | Bool
otherwise =
      let (Integer
vA, Integer
mA) = Integer -> Integer -> (Integer, Integer)
knownBitsOfInterval Integer
wLo Integer
bvmask
          (Integer
vB, Integer
mB) = Integer -> Integer -> (Integer, Integer)
knownBitsOfInterval Integer
0 Integer
wHi
          mAB :: Integer
mAB = Integer
mA Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
mB Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. (Integer
vA Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
vB)
      in (Integer
vA Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
mAB, Integer
mAB)
  where
  modulus :: Integer
modulus = Integer
bvmask Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
  wLo :: Integer
wLo = Integer
lo Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
modulus
  wHi :: Integer
wHi = Integer
hi Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
modulus
{-# INLINE wrappedKnownBitsOfInterval #-}

-- | Count trailing zeros of a non-negative 'Integer', returning @0@ for input
-- @0@. ('Data.Bits.countTrailingZeros' requires 'FiniteBits', which 'Integer'
-- doesn't have.)
--
-- Uses the bit-trick @popCount ((n .&. -n) - 1)@: @n .&. -n@ isolates the
-- lowest set bit (always a single power-of-two bit, for any nonzero @n@), and
-- @popCount@ of one less than that is the bit's position.
countTrailingZerosOr0 :: Integer -> Int
countTrailingZerosOr0 :: Integer -> Int
countTrailingZerosOr0 Integer
0 = Int
0
countTrailingZerosOr0 Integer
n = Integer -> Int
forall a. Bits a => a -> Int
popCount ((Integer
n Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Num a => a -> a
negate Integer
n) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
{-# INLINE countTrailingZerosOr0 #-}

-- | @log2OfPowerOfTwo n@ returns @k@ such that @n == 2^k@. Asserts that @n@
-- is a positive power of two, and that the fast computation
-- @popCount (n - 1)@ agrees with the general 'countTrailingZerosOr0'.
--
-- Faster than 'countTrailingZerosOr0' for known powers of two: skips the
-- @n .&. -n@ isolation step.
log2OfPowerOfTwo :: Integer -> Int
log2OfPowerOfTwo :: Integer -> Int
log2OfPowerOfTwo Integer
n =
  Bool -> Int -> Int
forall a. (?callStack::CallStack) => Bool -> a -> a
X.assert (Integer -> Bool
isPow2Integer Integer
n) (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$
  Bool -> Int -> Int
forall a. (?callStack::CallStack) => Bool -> a -> a
X.assert (Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Int
countTrailingZerosOr0 Integer
n) (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$
  Int
k
  where
  k :: Int
k = Integer -> Int
forall a. Bits a => a -> Int
popCount (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)

-- | /O(w²)/. Tristate-number multiply via shift-and-add (BPF
-- @tnum_mul@). The result is truncated to @bvmask@.
--
-- Strictly more precise than 'mul' on its own, but quadratic in @w@.
-- Captures bit-level structure of the product that trailing-zero
-- analysis can't see.
mulPrecise ::
  Integer {- ^ bvmask -} ->
  Tnum {- ^ a -} ->
  Tnum {- ^ b -} ->
  Tnum
mulPrecise :: Integer -> Tnum -> Tnum -> Tnum
mulPrecise Integer
bvmask (Tnum Integer
av0 Integer
am0) (Tnum Integer
bv0 Integer
bm0) = Integer -> Integer -> Integer -> Integer -> Tnum -> Tnum
forall {t} {t}.
(Num t, Num t, Bits t, Bits t) =>
t -> t -> Integer -> Integer -> Tnum -> Tnum
go Integer
av0 Integer
am0 Integer
bv0 Integer
bm0 Tnum
acc0
  where
  acc0 :: Tnum
acc0 = Integer -> Integer -> Tnum
mk ((Integer
av0 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
bv0) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask) Integer
0
  -- Accumulate contributions from each bit of a. A known-1 bit at
  -- position i adds b's mask shifted into position i (b's value bits
  -- are already included via the initial @av*bv@ product). An unknown
  -- bit at position i adds (b.value | b.mask) shifted in, since the
  -- bit might or might not contribute b.
  go :: t -> t -> Integer -> Integer -> Tnum -> Tnum
go !t
av !t
am !Integer
bv !Integer
bm !Tnum
acc
    | t
av t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0 Bool -> Bool -> Bool
&& t
am t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0 = Tnum
acc
    | Bool
otherwise =
        let acc' :: Tnum
acc'
              | t -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit t
av Int
0 = Integer -> Tnum -> Tnum -> Tnum
add Integer
bvmask Tnum
acc (Integer -> Integer -> Tnum
Tnum Integer
0 Integer
bm)
              | t -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit t
am Int
0 = Integer -> Tnum -> Tnum -> Tnum
add Integer
bvmask Tnum
acc (Integer -> Integer -> Tnum
Tnum Integer
0 (Integer
bv Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
bm))
              | Bool
otherwise    = Tnum
acc
        in t -> t -> Integer -> Integer -> Tnum -> Tnum
go (t
av t -> Int -> t
forall a. Bits a => a -> Int -> a
`shiftR` Int
1) (t
am t -> Int -> t
forall a. Bits a => a -> Int -> a
`shiftR` Int
1)
              (Integer
bv Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
1) (Integer
bm Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
1)
              Tnum
acc'
{-# INLINE mulPrecise #-}

-- | /O(w)/. Tristate-number unsigned division, with the result truncated to
-- @bvmask@.
--
-- Assumes the divisor is nonzero. When the divisor is a known power of two,
-- the result is exact (a logical right shift); otherwise the result is bounded
-- by interval analysis: every bit above the highest disagreement between
-- @aMin \`quot\` bMax@ and @aMax \`quot\` bMin@ is determined.
udiv ::
  Integer {- ^ bvmask -} ->
  Tnum {- ^ a -} ->
  Tnum {- ^ b -} ->
  Tnum
udiv :: Integer -> Tnum -> Tnum -> Tnum
udiv Integer
bvmask (Tnum Integer
av Integer
am) (Tnum Integer
bv Integer
bm)
  | Integer
bm Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0, Integer -> Bool
isPow2Integer Integer
bv =
      let k :: Int
k = Integer -> Int
log2OfPowerOfTwo Integer
bv
      in Integer -> Integer -> Tnum
mk ((Integer
av Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
k) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask) ((Integer
am Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
k) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask)
  | Bool
otherwise = Integer -> Integer -> Tnum
mk (Integer
highValue Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask) (Integer
highUnknown Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask)
  where
  aMin :: Integer
aMin = Integer
av Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask
  aMax :: Integer
aMax = (Integer
av Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
am) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask
  bMin :: Integer
bMin = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
1 Integer
bv
  bMax :: Integer
bMax = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
1 ((Integer
bv Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
bm) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask)
  -- a / b lies in [aMin/bMax, aMax/bMin]. Both quotients are non-negative
  -- and within @bvmask@, so no overflow check is needed.
  qMin :: Integer
qMin = Integer
aMin Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
bMax
  qMax :: Integer
qMax = Integer
aMax Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
bMin
  (Integer
highValue, Integer
highUnknown) = Integer -> Integer -> (Integer, Integer)
knownBitsOfInterval Integer
qMin Integer
qMax
{-# INLINE udiv #-}

-- | /O(w)/. Tristate-number unsigned remainder, with the result truncated to
-- @bvmask@.
--
-- When the divisor is a known power of two, the result is exact (a bitwise
-- mask); otherwise the result is bounded by:
--
--   * leading-zero analysis on @min(aMax, bMax-1)@; and
--   * low-bit preservation: if the divisor has @k@ known trailing zeros
--     (i.e.\ is definitely divisible by @2^k@), then @x rem y@ preserves the
--     low @k@ bits of @x@.
urem ::
  Integer {- ^ bvmask -} ->
  Tnum {- ^ a -} ->
  Tnum {- ^ b -} ->
  Tnum
urem :: Integer -> Tnum -> Tnum -> Tnum
urem Integer
bvmask (Tnum Integer
av Integer
am) (Tnum Integer
bv Integer
bm)
  | Integer
bm Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0, Integer -> Bool
isPow2Integer Integer
bv =
      let m :: Integer
m = Integer
bv Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
      in Integer -> Integer -> Tnum
mk (Integer
av Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
m) (Integer
am Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
m)
  | Bool
otherwise =
      let highUnknown :: Integer
highUnknown = Integer -> Integer
bitsBelow Integer
rMax Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask
          -- If the divisor has k known trailing zeros (both value and mask
          -- bits are 0 in the low k positions), every concrete divisor is
          -- divisible by 2^k. Since (x rem y) differs from x by a multiple
          -- of y, and every multiple of y is divisible by 2^k, we have
          -- (x rem y) mod 2^k == x mod 2^k. So we copy the dividend's low
          -- k bits (value and mask) into the result directly.
          -- See @lemma_urem_low_bits@ in bitsdomain.cry.
          rhsTrailingZeros :: Int
rhsTrailingZeros = Integer -> Int
countTrailingZerosOr0 (Integer
bv Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
bm)
          lowMask :: Integer
lowMask = (Int -> Integer
forall a. Bits a => Int -> a
bit Int
rhsTrailingZeros Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask
          lowValue :: Integer
lowValue = Integer
av Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
lowMask
          lowUnknown :: Integer
lowUnknown = Integer
am Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
lowMask
          resUnknown :: Integer
resUnknown = (Integer
highUnknown Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
lowMask) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
lowUnknown
          resValue :: Integer
resValue = Integer
lowValue Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
resUnknown
      in Integer -> Integer -> Tnum
mk (Integer
resValue Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask) (Integer
resUnknown Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask)
  where
  aMax :: Integer
aMax = (Integer
av Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
am) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask
  bMax :: Integer
bMax = (Integer
bv Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
bm) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bvmask
  rMax :: Integer
rMax = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
aMax (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
0 (Integer
bMax Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1))
{-# INLINE urem #-}