/*
This file contains a Cryptol implementation of the bitwise
bitvector abstract domain operations from What4.Utils.BVDomain
In addition to the algorithms themselves, this file also contains
specifications of correctness for each of the operations. All of the
correctness properties can be formally proven (each at some specific
bit width) by loading this file in cryptol and entering ":prove".
*/
module bitsdomain where
// This type represents _bitwise_ bounds as opposed to the
// arithmetic bounds described by BVDom. Note that
// this representation allows the empty set if
// lomask is not bitwise below himask. However, all
// the operations (other than intersection) preserve the property
// of being nonempty (implied by their various soundness properties).
type Dom n = { lomask : [n] , himask : [n] }
// Alias used to mark predicates that are intended to be checked as
// properties. The TestCoverage Haskell test uses this alias to
// identify which Cryptol functions correspond to PBT properties.
type Property = Bit
/** Membership predicate that defines the set of concrete values
represented by a bitwise abstract domain element. */
mem : {n} (fin n) => Dom n -> [n] -> Bit
mem a x = bitle a.lomask x /\ bitle x a.himask
bitle : {n} (fin n) => [n] -> [n] -> Bit
bitle x y = x || y == y
nonempty : {n} (fin n) => Dom n -> Bit
nonempty b = bitle b.lomask b.himask
singleton : {n} (fin n) => [n] -> Dom n
singleton x = { lomask = x, himask = x }
isSingleton : {n} (fin n) => Dom n -> Bit
isSingleton a = a.lomask == a.himask
top : {n} (fin n) => Dom n
top = { lomask = 0, himask = ~0 }
overlap : {n} (fin n) => Dom n -> Dom n -> Bit
overlap a b = nonempty (intersection a b)
intersection : {n} (fin n) => Dom n -> Dom n -> Dom n
intersection a b = { lomask = a.lomask || b.lomask, himask = a.himask && b.himask }
union : {n} (fin n) => Dom n -> Dom n -> Dom n
union a b = { lomask = a.lomask && b.lomask, himask = a.himask || b.himask }
////////////////////////////////////////////////////////////
// Lattice operations
/** Bottom element of the lattice: an improper domain whose
membership predicate is unsatisfiable. */
bottom : {n} (fin n) => Dom n
bottom = { lomask = ~0, himask = 0 }
/** Lattice join (least upper bound). Synonym for `union`. */
join : {n} (fin n) => Dom n -> Dom n -> Dom n
join = union
/** Lattice meet (greatest lower bound). Synonym for `intersection`.
Note: meet may produce an improper domain. */
meet : {n} (fin n) => Dom n -> Dom n -> Dom n
meet = intersection
/** Lattice ordering: every element of `a` is also in `b`. */
leq : {n} (fin n) => Dom n -> Dom n -> Bit
leq a b = bitle b.lomask a.lomask /\ bitle a.himask b.himask
////////////////////////////////////////////////////////////
zero_ext : {m, n} (fin m, m >= n) => Dom n -> Dom m
zero_ext a = { lomask = zext a.lomask, himask = zext a.himask }
sign_ext : {m, n} (fin m, m >= n, n >= 1) => Dom n -> Dom m
sign_ext a = { lomask = sext a.lomask, himask = sext a.himask }
concat : {m, n} (fin m, fin n) => Dom m -> Dom n -> Dom (m + n)
concat a b = { lomask = a.lomask # b.lomask, himask = a.himask # b.himask }
shrink : {m, n} (fin m, fin n) => Dom (m + n) -> Dom m
shrink a = { lomask = take`{m} a.lomask, himask = take`{m} a.himask }
trunc : {m, n} (fin m, fin n) => Dom (m + n) -> Dom n
trunc a = { lomask = drop`{m} a.lomask, himask = drop`{m} a.himask }
bnot : {n} (fin n) => Dom n -> Dom n
bnot b = { lomask = ~b.himask, himask = ~b.lomask }
band : {n} (fin n) => Dom n -> Dom n -> Dom n
band a b = { lomask = a.lomask && b.lomask, himask = a.himask && b.himask }
bor : {n} (fin n) => Dom n -> Dom n -> Dom n
bor a b = { lomask = a.lomask || b.lomask, himask = a.himask || b.himask }
// Note, this requires quite a few more operations than AND and OR.
// See "xordomain.cry" for a domain optimized for XOR and AND operations.
bxor : {n} (fin n) => Dom n -> Dom n -> Dom n
bxor a b = { lomask = lo, himask = hi }
where
ua = a.lomask ^ a.himask
ub = b.lomask ^ b.himask
c = a.lomask ^ b.lomask
u = ua || ub
hi = c || u
lo = hi ^ u
// Note: shift and rotate operations in this domain only apply
// when the shift amount is known
shl : {n} (fin n) => Dom n -> [n] -> Dom n
shl a x = { lomask = a.lomask << x', himask = a.himask << x' }
where x' = if x < `n then x else `n
lshr : {n} (fin n) => Dom n -> [n] -> Dom n
lshr a x = { lomask = a.lomask >> x', himask = a.himask >> x' }
where x' = if x < `n then x else `n
ashr : {n} (fin n, n >= 1) => Dom n -> [n] -> Dom n
ashr a x = { lomask = a.lomask >>$ x', himask = a.himask >>$ x' }
where x' = if x < `n then x else `n
rol : {n} (fin n) => Dom n -> [n] -> Dom n
rol a x = { lomask = a.lomask <<< x, himask = a.himask <<< x }
ror : {n} (fin n) => Dom n -> [n] -> Dom n
ror a x = { lomask = a.lomask >>> x, himask = a.himask >>> x }
// Range-analysis variants: the shift/rotate amount is itself a Dom.
// These declarative specifications union per-shift results over every
// member of @b@. The Haskell in @What4.Domains.BV.Bitwise@ has
// performance-optimized implementations (LLVM @KnownBits@-style
// tristate skip, bounded iteration, saturation collapse, early exit)
// that are property-tested to be equivalent to these specs.
emptyDom : {n} (fin n) => Dom n
emptyDom = { lomask = ~0, himask = 0 }
shlAbstract : {n} (fin n) => Dom n -> Dom n -> Dom n
shlAbstract a b = foldl union emptyDom contribs
where
contribs = [ if mem b y then shl a y else emptyDom | y <- take`{2^^n} [0 ...] ]
lshrAbstract : {n} (fin n) => Dom n -> Dom n -> Dom n
lshrAbstract a b = foldl union emptyDom contribs
where
contribs = [ if mem b y then lshr a y else emptyDom | y <- take`{2^^n} [0 ...] ]
ashrAbstract : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n
ashrAbstract a b = foldl union emptyDom contribs
where
contribs = [ if mem b y then ashr a y else emptyDom | y <- take`{2^^n} [0 ...] ]
rolAbstract : {n} (fin n) => Dom n -> Dom n -> Dom n
rolAbstract a b = foldl union emptyDom contribs
where
contribs = [ if mem b y then rol a y else emptyDom | y <- take`{2^^n} [0 ...] ]
rorAbstract : {n} (fin n) => Dom n -> Dom n -> Dom n
rorAbstract a b = foldl union emptyDom contribs
where
contribs = [ if mem b y then ror a y else emptyDom | y <- take`{2^^n} [0 ...] ]
////////////////////////////////////////////////////////////
// Bounds and comparisons
// Unsigned bounds: the bit-pattern lo and hi are also the unsigned min/max.
ubounds : {n} (fin n) => Dom n -> ([n], [n])
ubounds a = (a.lomask, a.himask)
// Signed bounds: if the sign bit is known (lomask and himask agree on
// it), the bit-pattern bounds are also the signed bounds. If the sign
// bit is unknown, the most-negative value sets the sign bit and clears
// all other unknowns; the most-positive clears the sign bit and sets
// all other unknowns.
sbounds : {n} (fin n, n >= 1) => Dom n -> ([n], [n])
sbounds a =
if (a.lomask && signbit) == (a.himask && signbit)
then (a.lomask, a.himask)
else (a.lomask || signbit, a.himask && (~ signbit))
where
signbit = 1 << (`n - 1 : [n]) : [n]
ult : {n} (fin n) => Dom n -> Dom n -> Bit
ult a b = (ubounds a).1 < (ubounds b).0
slt : {n} (fin n, n >= 1) => Dom n -> Dom n -> Bit
slt a b = (sbounds a).1 <$ (sbounds b).0
////////////////////////////////////////////////////////////
// Arithmetic operations (tristate-number algorithms)
//
// These follow the algorithms used by the Linux kernel BPF verifier
// for "tnum" (tristate-number) propagation.
// Internal: tristate-number add. Given (av, am) and (bv, bm) where
// "value" is the known-1 bits and "mask" is the unknown bits, compute
// the tnum representing the sum.
addTnum : {n} (fin n) => [n] -> [n] -> [n] -> [n] -> ([n], [n])
addTnum av am bv bm = (resv, resm)
where
sm = am + bm
sv = av + bv
sigma = sm + sv
chi = sigma ^ sv
resm = chi || am || bm
resv = sv && (~ resm)
// Convert a (value, mask) pair into a Dom.
fromTnum : {n} (fin n) => [n] -> [n] -> Dom n
fromTnum v m = { lomask = v, himask = v || m }
// Convert a Dom to a (value, mask) pair.
toTnum : {n} (fin n) => Dom n -> ([n], [n])
toTnum a = (a.lomask, a.lomask ^ a.himask)
add : {n} (fin n) => Dom n -> Dom n -> Dom n
add a b = fromTnum resv resm
where
(av, am) = toTnum a
(bv, bm) = toTnum b
(resv, resm) = addTnum av am bv bm
bneg : {n} (fin n, n >= 1) => Dom n -> Dom n
bneg a = add (bnot a) (singleton 1)
sub : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n
sub a b = add a (bneg b)
// scale uses the precise (shift-and-add) multiplication so that
// constant-by-domain products preserve bit-level structure.
scale : {n} (fin n, n >= 1) => [n] -> Dom n -> Dom n
scale k a = mulPrecise (singleton k) a
// Population count: number of 1 bits.
popcount : {n} (fin n, n >= 1) => [n] -> [n]
popcount x = sum [ zero # [b] | b <- x ]
// Count trailing zeros, returning n for x == 0. Computed via the
// bit-trick popcount ((x .&. -x) - 1): x .&. -x isolates the lowest
// set bit, and the popcount of one less than that gives its position.
ctz : {n} (fin n, n >= 1) => [n] -> [n]
ctz x = if x == 0 then `n else popcount ((x && (- x)) - 1)
// Count leading zeros, returning n for x == 0. Smearing the highest
// set bit downward (bitsBelow) yields a 2^k-1 mask whose popcount is
// the position of the highest set bit plus one; subtract from n.
clz : {n} (fin n, n >= 1) => [n] -> [n]
clz x = `n - popcount (bitsBelow x)
// knownBitsOfInterval lo hi: given an arithmetic interval [lo, hi]
// (with 0 <= lo <= hi), return (value, mask) in tnum form. Bits above
// the highest disagreement between lo and hi are determined (recorded
// in value); bits at-or-below it 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.
//
// Subsumes leading-zero analysis (when lo = 0) and adds leading-1
// (and arbitrary leading-prefix) analysis when lo > 0.
knownBitsOfInterval : {n} (fin n, n >= 1) => [n] -> [n] -> ([n], [n])
knownBitsOfInterval lo hi = (lo && (~ varying), varying)
where
varying = bitsBelow (lo ^ hi)
// Like knownBitsOfInterval but for the image of [lo, hi] under
// reduction mod 2^n. Three cases:
//
// * the interval is at least 2^n wide -- every residue is reached, so
// no bits are determined;
// * the interval fits in one modulus -- use knownBitsOfInterval on
// the wrapped bounds directly;
// * the interval crosses one modulus boundary -- analyze each half
// and join (a bit is known only when both halves agree on it).
//
// The inputs are 2n-bit so they can represent the unbounded product of
// two n-bit values.
wrappedKnownBitsOfInterval : {n} (fin n, n >= 1) => [n + n] -> [n + n] -> ([n], [n])
wrappedKnownBitsOfInterval lo hi =
if take`{n} (hi - lo) != 0
then (zero, ~ zero)
else if wLo <= wHi
then knownBitsOfInterval wLo wHi
else
// wraps: [wLo, ~zero] U [0, wHi]
(vA && (~ mAB), mAB)
where
(vA, mA) = knownBitsOfInterval wLo (~ zero)
(vB, mB) = knownBitsOfInterval 0 wHi
mAB = mA || mB || (vA ^ vB)
where
wLo = drop`{n} lo
wHi = drop`{n} hi
// Fast multiply via interval, trailing-zero, and low-bit 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
// av and am have that bit clear), and similarly for ctzB;
// * known bits derived from the arithmetic interval
// [aMin*bMin, aMax*bMax] reduced mod 2^n
// (see wrappedKnownBitsOfInterval); and
// * exact low bits from multiplying the known-one values: the bottom
// min(trailBitsKnownA - ctzA, trailBitsKnownB - ctzB) + trailZ
// bits of aMin*bMin are exact (LLVM KnownBits::mul trick).
//
// Special case: when both operands are concrete singletons (mask == 0),
// the result is the exact concrete product.
mul : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n
mul a b =
if a.lomask == a.himask /\ b.lomask == b.himask
then singleton (a.lomask * b.lomask)
else { lomask = resValue, himask = resValue || resUnknown }
where
(av, am) = toTnum a
(bv, bm) = toTnum b
ctzA = ctz (av || am)
ctzB = ctz (bv || bm)
trailZ = ctzA + ctzB
// Compute aMin*bMin and aMax*bMax in 2n-bit width so the product is
// exact (no overflow); wrappedKnownBitsOfInterval handles wrap-around.
aMinExt = (zext av : [n + n])
bMinExt = (zext bv : [n + n])
aMaxExt = (zext (av || am) : [n + n])
bMaxExt = (zext (bv || bm) : [n + n])
prodMin = aMinExt * bMinExt
prodMax = aMaxExt * bMaxExt
(highValue, highUnknown) = wrappedKnownBitsOfInterval`{n} prodMin prodMax
// Low-bit multiplication: consecutive known bits from LSB in each operand
trailBitsKnownA : [n]
trailBitsKnownA = if am == 0 then `n else ctz am
trailBitsKnownB : [n]
trailBitsKnownB = if bm == 0 then `n else ctz bm
smallestOperand = min (trailBitsKnownA - ctzA) (trailBitsKnownB - ctzB)
resultBitsKnown = min (smallestOperand + trailZ) `n
bottomKnown : [n]
bottomKnown = av * bv
lowKnownMask : [n]
lowKnownMask = (1 << resultBitsKnown) - 1
// Combine: unknown only where both sources are unknown
resUnknown = highUnknown && (~ lowKnownMask)
resValue = (highValue || (bottomKnown && lowKnownMask)) && (~ resUnknown)
// Precise multiply via shift-and-add over the bits of a (BPF tnum_mul).
// Strictly more precise than mul on its own, but quadratic in n.
// Captures bit-level structure of the product that trailing-zero
// analysis can't see.
//
// Accumulate contributions from each bit of a. A known-1 bit at
// position i adds bm shifted to position i (b's value bits are already
// included via the initial av*bv product). An unknown bit at position
// i adds (bv|bm) shifted in, since the bit might or might not
// contribute b.
mulPrecise : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n
mulPrecise a b = intersection schoolbook fast
where
fast = mul a b
schoolbook = fromTnum resv resm
(av, am) = toTnum a
(bv, bm) = toTnum b
// Initial value-by-value product
init = (av * bv, 0 : [n])
// Shift contributions for each bit position i in [0..n-1]
contribs = [ if av @ (`n - 1 - i)
then (0, bm << i)
else if am @ (`n - 1 - i)
then (0, (bv || bm) << i)
else (0, 0)
| i <- [0 .. n-1] ]
// Sum them all using addTnum
(resv, resm) = foldl step init contribs
step (v, m) (cv, cm) = addTnum v m cv cm
foldl : {a, b, n} (fin n) => (a -> b -> a) -> a -> [n]b -> a
foldl f z xs = (zs : [_]a) ! 0
where
zs = [z] # [ f y x | y <- zs | x <- xs ]
////////////////////////////////////////////////////////////
// Division and remainder
//
// All four operations assume the divisor is nonzero, matching the
// convention of What4.Domains.BV.Arith.
// bitsBelow x: smallest mask of the form 2^k - 1 that is >= x.
// Computed by repeatedly smearing the highest set bit downward.
// Every value in [0, x] has all its set bits within bitsBelow x.
bitsBelow : {n} (fin n, n >= 1) => [n] -> [n]
bitsBelow x = ys ! 0
where
ys = [x] # [ y || (y >> 1) | y <- ys | _ <- [0 .. n - 1] ]
// Unsigned division. When the divisor is a singleton power of
// two 2^k, the result is exact (a logical shift right by k);
// otherwise, the result is bounded by interval analysis on
// [aMin/bMax, aMax/bMin], keeping every bit above the highest
// disagreement between the bounds.
udiv : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n
udiv a b =
if (bm == 0) /\ (bv != 0) /\ ((bv && (bv - 1)) == 0)
then { lomask = av / bv, himask = (av || am) / bv }
else { lomask = highValue, himask = highValue || highUnknown }
where
(av, am) = toTnum a
(bv, bm) = toTnum b
aMin = av
aMax = av || am
// bv = 0 means b.lomask = 0, i.e. b's domain might contain zero. We use
// max 1 to avoid division by zero; the result is sound under our
// assumption that b is nonzero.
bMin = if bv == 0 then 1 else bv
bMax = if (bv || bm) == 0 then 1 else (bv || bm)
qMin = aMin / bMax
qMax = aMax / bMin
(highValue, highUnknown) = knownBitsOfInterval qMin qMax
// Unsigned remainder. When the divisor is a singleton power of
// two 2^k, the result is exact (the low k bits of the dividend);
// otherwise, the result is bounded above by min(aMax, bMax-1) and
// every bit above that is known zero. Additionally, if the divisor
// has k known trailing zeros (definitely divisible by 2^k), the
// remainder preserves the dividend's low k bits exactly.
//
//
// (The remainder's lower bound is trivially 0, so the same
// interval-agreement analysis used in udiv would not yield additional
// leading bits here.)
urem : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n
urem a b =
if (bm == 0) /\ (bv != 0) /\ ((bv && (bv - 1)) == 0)
then { lomask = av % bv, himask = (av || am) % bv }
else { lomask = resValue, himask = resValue || resUnknown }
where
(av, am) = toTnum a
(bv, bm) = toTnum b
aMax = av || am
bMax = bv || bm
rMax = if bMax == 0 then 0 else (if aMax < bMax - 1 then aMax else bMax - 1)
highUnknown = bitsBelow rMax
// If the divisor has k trailing zeros, the remainder preserves
// the dividend's low k bits.
rhsTrailingZeros = ctz (bv || bm)
lowMask : [n]
lowMask = (1 << rhsTrailingZeros) - 1
lowValue = av && lowMask
lowUnknown = am && lowMask
resUnknown = (highUnknown && (~ lowMask)) || lowUnknown
resValue = lowValue && (~ resUnknown)
// 3-valued unsigned-less-than on Doms: returns 0 (definitely false),
// 1 (definitely true), or 2 (unknown). Used by long division.
ultMaybe : {n} (fin n) => Dom n -> Dom n -> [2]
ultMaybe a b =
if a.himask < b.lomask then 1
else if a.lomask >= b.himask then 0
else 2
// Long division: walk the bits of a from high to low, maintaining a
// running partial remainder r as a Dom. At each step, shift r left
// and inject the corresponding bit of a; then compare to b. If r >= b
// definitely, subtract and set the quotient bit. If r < b definitely,
// leave the quotient bit clear. If undetermined, union both branches
// into r and leave the quotient bit unknown.
//
// Returns (quotient, remainder) Doms.
longDivision : {n} (fin n, n >= 1) => Dom n -> Dom n -> (Dom n, Dom n)
longDivision a b = (states ! 0).0
where
// states !! i is (qDom, rDom) after processing the i-th iteration
// (from MSB down).
states : [n + 1]((Dom n, Dom n), [width n])
states = [((singleton 0, singleton 0), 0)]
# [ step s i | s <- states | i <- [0 .. n - 1] ]
step ((q, r), _) i =
((q', r'), i + 1)
where
bitIdx = `n - 1 - i
aBit = testBitDom a bitIdx
rShifted = shl r 1
rPrime = bor rShifted aBit
rMinusB = sub rPrime b
cmp = ultMaybe rPrime b
(q', r') =
if cmp == 1 // rPrime < b: quotient bit 0
then (q, rPrime)
else if cmp == 0 // rPrime >= b: quotient bit 1
then (setBitDom q bitIdx, rMinusB)
else (unknownBitDom q bitIdx, union rPrime rMinusB)
// Get bit i of a Dom as a 1-bit-wide Dom (in width n: low bit only).
testBitDom : {n} (fin n, n >= 1) => Dom n -> [width n] -> Dom n
testBitDom a i =
if a.lomask @ idx
then singleton 1 // bit known set
else if a.himask @ idx
then { lomask = 0, himask = 1 } // bit unknown
else singleton 0 // bit known clear
where
// Cryptol indexes from the MSB; convert from LSB index i.
idx : [width n]
idx = `n - 1 - i
// Set bit i of a Dom (assumes it was previously known to be 0).
setBitDom : {n} (fin n, n >= 1) => Dom n -> [width n] -> Dom n
setBitDom a i = bor a (singleton (1 << i))
// Mark bit i of a Dom as unknown (assumes it was previously known to be 0).
unknownBitDom : {n} (fin n, n >= 1) => Dom n -> [width n] -> Dom n
unknownBitDom a i =
{ lomask = a.lomask, himask = a.himask || (1 << i) }
// Unsigned division combining schoolbook long division with the
// leading-zero analysis of udiv. Strictly at least as precise as udiv.
udivPrecise : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n
udivPrecise a b = intersection (longDivision a b).0 (udiv a b)
// Unsigned remainder combining schoolbook long division with the
// leading-zero analysis of urem. Strictly at least as precise as urem.
uremPrecise : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n
uremPrecise a b = intersection (longDivision a b).1 (urem a b)
// splitSign a returns (zero_circle, one_circle), where the first
// is a's restriction to non-negative values (sign bit cleared)
// and the second is its restriction to negative values (sign bit
// set).
//
// One of the two circles may be empty in the sense that
// (lomask || himask) != himask: if a's sign bit is already known,
// clearing or setting it in only one of the masks produces a
// pair that no concrete value can satisfy. That's fine here: any
// x that satisfied the input ends up in the *other* circle, the
// soundness implication is vacuously true on the empty side, and
// union with an empty domain contributes nothing.
splitSign : {n} (fin n, n >= 1) => Dom n -> (Dom n, Dom n)
splitSign a = (zero_circle, one_circle)
where
signbit = 1 << (`n - 1 : [n]) : [n]
zero_circle = { lomask = a.lomask, himask = a.himask && (~ signbit) }
one_circle = { lomask = a.lomask || signbit, himask = a.himask }
// Signed division (rounds toward zero). Splits both operands on
// the sign bit, calls udiv on absolute values, and negates the
// sub-result when the input signs differ. Joins all four cases.
sdiv : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n
sdiv a b = union (union r00 r11) (union r01 r10)
where
(aPos, aNeg) = splitSign a
(bPos, bNeg) = splitSign b
r00 = udiv aPos bPos // (+,+) -> +
r01 = bneg (udiv aPos (bneg bNeg)) // (+,-) -> -
r10 = bneg (udiv (bneg aNeg) bPos) // (-,+) -> -
r11 = udiv (bneg aNeg) (bneg bNeg) // (-,-) -> +
// Signed remainder. Same shape as sdiv, but the result takes the
// dividend's sign rather than the XOR of the input signs.
//
// After the union, refine using the LLVM KnownBits::srem sign/magnitude
// bound: srem has the dividend's sign (or is zero), and |x %$ y| is
// bounded by both |x| and |y|, so the result has at least
// max(clz |x|, signBits y) identical sign bits. See @lemma_srem_*@
// properties below.
srem : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n
srem a b = meet base (signMagnitudeBound a b base)
where
(aPos, aNeg) = splitSign a
(bPos, bNeg) = splitSign b
r00 = urem aPos bPos // dividend +
r01 = urem aPos (bneg bNeg) // dividend +
r10 = bneg (urem (bneg aNeg) bPos) // dividend -
r11 = bneg (urem (bneg aNeg) (bneg bNeg)) // dividend -
base = union (union r00 r01) (union r10 r11)
// Sign/magnitude refinement for srem. If the dividend's sign is
// known, the result's leading bits replicate that sign; how many
// such bits is bounded by the magnitudes of both operands.
signMagnitudeBound : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n -> Dom n
signMagnitudeBound a b base =
if (signbit && a.himask) == 0
// dividend known non-negative: |x %$ y| <= min(|x|, |y|-1).
then { lomask = 0, himask = (~0 : [n]) >> leadZ }
else if (signbit && a.lomask) != 0 /\ ~ (mem base 0)
// dividend known negative and result definitely nonzero:
// result has at least `leading` leading 1 bits.
then { lomask = ~ ((~0 : [n]) >> leading), himask = ~0 }
else top
where
signbit = 1 << (`n - 1 : [n]) : [n]
// Minimum number of identical sign bits guaranteed in b's magnitude.
// Non-negative b: leading zeros come from himask (upper bound).
// Negative b: leading ones come from lomask (lower bound).
bSignBits =
if (signbit && b.himask) == 0
then clz b.himask
else if (signbit && b.lomask) != 0
then clz (~ b.lomask)
else 1
leadZ = max (clz a.himask) bSignBits
leadO = clz (~ a.lomask)
leading = max leadO bSignBits
////////////////////////////////////////////////////////////
// Soundness properties
correct_any : {n} (fin n) => [n] -> Property
correct_any x = mem top x
correct_singleton : {n} (fin n) => [n] -> [n] -> Property
correct_singleton x y = mem (singleton x) y == (x == y)
correct_overlap : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
correct_overlap a b x =
mem a x ==> mem b x ==> overlap a b
correct_overlap_inv : {n} (fin n) => Dom n -> Dom n -> Property
correct_overlap_inv a b =
overlap a b ==> (mem a (a.lomask || b.lomask) /\ mem b (a.lomask || b.lomask))
correct_union : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
correct_union a b x =
(mem a x \/ mem b x) ==> mem (union a b) x
correct_intersection : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
correct_intersection a b x =
(mem a x /\ mem b x) == mem (intersection a b) x
correct_join : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
correct_join a b x =
(mem a x \/ mem b x) ==> mem (join a b) x
correct_meet : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
correct_meet a b x =
(mem a x /\ mem b x) ==> mem (meet a b) x
// Precision of meet: not just sound, but tight - any element of the
// meet really is in both arguments. (Bitwise meet is the exact
// intersection of masks, so this holds with equality on the
// implication.)
precise_meet : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
precise_meet a b x =
mem (meet a b) x ==> (mem a x /\ mem b x)
correct_leq : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
correct_leq a b x =
(leq a b /\ mem a x) ==> mem b x
// Lattice laws
join_commutative : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
join_commutative a b x =
mem (join a b) x == mem (join b a) x
join_idempotent : {n} (fin n) => Dom n -> [n] -> Property
join_idempotent a x =
mem (join a a) x == mem a x
meet_commutative : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
meet_commutative a b x =
mem (meet a b) x == mem (meet b a) x
meet_idempotent : {n} (fin n) => Dom n -> [n] -> Property
meet_idempotent a x =
mem (meet a a) x == mem a x
join_top : {n} (fin n) => Dom n -> [n] -> Property
join_top a x = mem (join a top) x
join_bottom : {n} (fin n) => Dom n -> [n] -> Property
join_bottom a x =
mem (join a bottom) x == mem a x
meet_top : {n} (fin n) => Dom n -> [n] -> Property
meet_top a x =
mem (meet a top) x == mem a x
meet_bottom : {n} (fin n) => Dom n -> [n] -> Property
meet_bottom a x =
~ (mem (meet a bottom) x)
leq_reflexive : {n} (fin n) => Dom n -> Property
leq_reflexive a = leq a a
leq_transitive : {n} (fin n) => Dom n -> Dom n -> Dom n -> Property
leq_transitive a b c =
(leq a b /\ leq b c) ==> leq a c
meet_lower_bound : {n} (fin n) => Dom n -> Dom n -> Property
meet_lower_bound a b = leq (meet a b) a
join_upper_bound : {n} (fin n) => Dom n -> Dom n -> Property
join_upper_bound a b = leq a (join a b)
join_monotone : {n} (fin n) => Dom n -> Dom n -> Dom n -> Property
join_monotone a b c =
leq a b ==> leq (join a c) (join b c)
meet_monotone : {n} (fin n) => Dom n -> Dom n -> Dom n -> Property
meet_monotone a b c =
leq a b ==> leq (meet a c) (meet b c)
join_associative : {n} (fin n) => Dom n -> Dom n -> Dom n -> [n] -> Property
join_associative a b c x =
mem (join (join a b) c) x == mem (join a (join b c)) x
meet_associative : {n} (fin n) => Dom n -> Dom n -> Dom n -> [n] -> Property
meet_associative a b c x =
mem (meet (meet a b) c) x == mem (meet a (meet b c)) x
join_absorb : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
join_absorb a b x =
mem (join a (meet a b)) x == mem a x
meet_absorb : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
meet_absorb a b x =
mem (meet a (join a b)) x == mem a x
// `join` preserves non-emptiness: the union of two non-empty domains
// is non-empty.
join_proper : {n} (fin n) => Dom n -> Dom n -> Property
join_proper a b = (nonempty a /\ nonempty b) ==> nonempty (join a b)
// `meet` cannot conjure elements: if the meet is non-empty, both
// inputs must have been.
meet_proper : {n} (fin n) => Dom n -> Dom n -> Property
meet_proper a b = nonempty (meet a b) ==> (nonempty a /\ nonempty b)
correct_zero_ext : {m, n} (fin m, m >= n) => Dom n -> [n] -> Property
correct_zero_ext a x =
mem a x ==> mem (zero_ext`{m} a) (zext`{m} x)
correct_sign_ext : {m, n} (fin m, m >= n, n >= 1) => Dom n -> [n] -> Property
correct_sign_ext a x =
mem a x ==> mem (sign_ext`{m} a) (sext`{m} x)
correct_concat : {m, n} (fin m, fin n) => Dom m -> Dom n -> [m] -> [n] -> Property
correct_concat a b x y =
mem a x ==> mem b y ==> mem (concat a b) (x # y)
correct_shrink : {m, n} (fin m, fin n) => Dom (m + n) -> [m+n] -> Property
correct_shrink a x =
mem a x ==> mem (shrink`{m} a) (take`{m} x)
correct_trunc : {m, n} (fin m, fin n) => Dom (m + n) -> [m+n] -> Property
correct_trunc a x =
mem a x ==> mem (trunc`{m} a) (drop`{m} x)
correct_asSingleton : {n} (fin n) => Dom n -> Property
correct_asSingleton a =
isSingleton a ==> a == singleton a.lomask
correct_not : {n} (fin n) => Dom n -> [n] -> Property
correct_not a x =
mem a x == mem (bnot a) (~ x)
correct_and : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_and a b x y =
mem a x ==> mem b y ==> mem (band a b) (x && y)
correct_or : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_or a b x y =
mem a x ==> mem b y ==> mem (bor a b) (x || y)
correct_xor : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_xor a b x y =
mem a x ==> mem b y ==> mem (bxor a b) (x ^ y)
correct_shl : {n} (fin n) => Dom n -> [n] -> [n] -> Property
correct_shl a x y =
mem a x ==> mem (shl a y) (x << y)
correct_lshr : {n} (fin n) => Dom n -> [n] -> [n] -> Property
correct_lshr a x y =
mem a x ==> mem (lshr a y) (x >> y)
correct_ashr : {n} (fin n, n >= 1) => Dom n -> [n] -> [n] -> Property
correct_ashr a x y =
mem a x ==> mem (ashr a y) (x >>$ y)
correct_rol : {n} (fin n) => Dom n -> [n] -> [n] -> Property
correct_rol a x y =
mem a x ==> mem (rol a y) (x <<< y)
correct_ror : {n} (fin n) => Dom n -> [n] -> [n] -> Property
correct_ror a x y =
mem a x ==> mem (ror a y) (x >>> y)
correct_shlAbstract : {n} (fin n) => Dom n -> [n] -> Dom n -> [n] -> Property
correct_shlAbstract a x b y =
mem a x ==> mem b y ==> mem (shlAbstract a b) (x << y)
correct_lshrAbstract : {n} (fin n) => Dom n -> [n] -> Dom n -> [n] -> Property
correct_lshrAbstract a x b y =
mem a x ==> mem b y ==> mem (lshrAbstract a b) (x >> y)
correct_ashrAbstract : {n} (fin n, n >= 1) => Dom n -> [n] -> Dom n -> [n] -> Property
correct_ashrAbstract a x b y =
mem a x ==> mem b y ==> mem (ashrAbstract a b) (x >>$ y)
correct_rolAbstract : {n} (fin n) => Dom n -> [n] -> Dom n -> [n] -> Property
correct_rolAbstract a x b y =
mem a x ==> mem b y ==> mem (rolAbstract a b) (x <<< y)
correct_rorAbstract : {n} (fin n) => Dom n -> [n] -> Dom n -> [n] -> Property
correct_rorAbstract a x b y =
mem a x ==> mem b y ==> mem (rorAbstract a b) (x >>> y)
correct_ubounds : {n} (fin n) => Dom n -> [n] -> Property
correct_ubounds a x =
mem a x ==> lo <= x /\ x <= hi
where
(lo, hi) = ubounds a
correct_sbounds : {n} (fin n, n >= 1) => Dom n -> [n] -> Property
correct_sbounds a x =
mem a x ==> lo <=$ x /\ x <=$ hi
where
(lo, hi) = sbounds a
correct_add : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_add a b x y =
mem a x ==> mem b y ==> mem (add a b) (x + y)
correct_sub : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_sub a b x y =
mem a x ==> mem b y ==> mem (sub a b) (x - y)
correct_neg : {n} (fin n, n >= 1) => Dom n -> [n] -> Property
correct_neg a x =
mem a x ==> mem (bneg a) (- x)
correct_scale : {n} (fin n, n >= 1) => [n] -> Dom n -> [n] -> Property
correct_scale k a x =
mem a x ==> mem (scale k a) (k * x)
correct_mul : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_mul a b x y =
mem a x ==> mem b y ==> mem (mul a b) (x * y)
correct_mulPrecise : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_mulPrecise a b x y =
mem a x ==> mem b y ==> mem (mulPrecise a b) (x * y)
correct_udiv : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_udiv a b x y =
mem a x ==> mem b y ==> y != 0 ==> mem (udiv a b) (x / y)
correct_urem : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_urem a b x y =
mem a x ==> mem b y ==> y != 0 ==> mem (urem a b) (x % y)
correct_udivPrecise : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_udivPrecise a b x y =
mem a x ==> mem b y ==> y != 0 ==> mem (udivPrecise a b) (x / y)
correct_uremPrecise : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_uremPrecise a b x y =
mem a x ==> mem b y ==> y != 0 ==> mem (uremPrecise a b) (x % y)
correct_sdiv : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_sdiv a b x y =
mem a x ==> mem b y ==> y != 0 ==> mem (sdiv a b) (x /$ y)
correct_srem : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_srem a b x y =
mem a x ==> mem b y ==> y != 0 ==> mem (srem a b) (x %$ y)
correct_ult : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_ult a b x y =
ult a b ==> mem a x ==> mem b y ==> x < y
correct_slt : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_slt a b x y =
slt a b ==> mem a x ==> mem b y ==> x <$ y
property b1 = correct_any`{16}
property b2 = correct_singleton`{16}
property b3 = correct_overlap`{16}
property b4 = correct_overlap_inv`{16}
property b5 = correct_union`{8}
property b6 = correct_intersection`{8}
property b7 = correct_zero_ext`{32, 16}
property b8 = correct_sign_ext`{32, 16}
property b9 = correct_concat`{16, 16}
property b10 = correct_shrink`{8, 8}
property b11 = correct_trunc`{8, 8}
property b12 = correct_asSingleton`{16}
property l1 = correct_not`{16}
property l2 = correct_and`{16}
property l3 = correct_or`{16}
property l4 = correct_xor`{16}
property s1 = correct_shl`{16}
property s2 = correct_lshr`{16}
property s3 = correct_ashr`{16}
property s4 = correct_rol`{16}
property s5 = correct_ror`{16}
property s6 = correct_shlAbstract`{8}
property s7 = correct_lshrAbstract`{8}
property s8 = correct_ashrAbstract`{8}
property s9 = correct_rolAbstract`{8}
property s10 = correct_rorAbstract`{8}
property a1 = correct_ubounds`{8}
property a2 = correct_sbounds`{8}
property a3 = correct_add`{8}
property a4 = correct_sub`{8}
property a5 = correct_neg`{8}
property a6 = correct_mul`{8}
property a7 = correct_scale`{8}
property a8 = correct_ult`{8}
property a9 = correct_slt`{8}
property a10 = correct_udiv`{8}
property a11 = correct_urem`{8}
property a12 = correct_sdiv`{8}
property a13 = correct_srem`{8}
property a14 = correct_mulPrecise`{8} // NB: takes 60s
property a15 = correct_udivPrecise`{8}
property a16 = correct_uremPrecise`{8}
property lat1 = correct_join`{8}
property lat2 = correct_meet`{8}
property lat3 = correct_leq`{8}
property lat4 = join_commutative`{8}
property lat5 = join_idempotent`{8}
property lat6 = meet_commutative`{8}
property lat7 = meet_idempotent`{8}
property lat8 = join_top`{8}
property lat9 = join_bottom`{8}
property lat10 = meet_top`{8}
property lat11 = meet_bottom`{8}
property lat12 = leq_reflexive`{8}
property lat13 = join_upper_bound`{8}
property lat14 = leq_transitive`{8}
property lat15 = meet_lower_bound`{8}
property lat16 = join_monotone`{8}
property lat17 = meet_monotone`{8}
property lat18 = join_associative`{8}
property lat19 = meet_associative`{8}
property lat20 = join_absorb`{8}
property lat21 = meet_absorb`{8}
property lat22 = precise_meet`{8}
property lat23 = join_proper`{8}
property lat24 = meet_proper`{8}
////////////////////////////////////////////////////////////
// Operations preserve singletons
singleton_overlap : {n} (fin n) => [n] -> [n] -> Bit
singleton_overlap x y =
overlap (singleton x) (singleton y) == (x == y)
singleton_zero_ext : {m, n} (fin m, m >= n) => [n] -> Bit
singleton_zero_ext x =
zero_ext`{m} (singleton x) == singleton (zext`{m} x)
singleton_sign_ext : {m, n} (fin m, m >= n, n >= 1) => [n] -> Bit
singleton_sign_ext x =
sign_ext`{m} (singleton x) == singleton (sext`{m} x)
singleton_concat : {m, n} (fin m, fin n) => [m] -> [n] -> Bit
singleton_concat x y =
concat (singleton x) (singleton y) == singleton (x # y)
singleton_shrink : {m, n} (fin m, fin n) => [m + n] -> Bit
singleton_shrink x =
shrink`{m} (singleton x) == singleton (take`{m} x)
singleton_trunc : {m, n} (fin m, fin n) => [m + n] -> Bit
singleton_trunc x =
trunc`{m} (singleton x) == singleton (drop`{m} x)
singleton_bnot : {n} (fin n) => [n] -> Bit
singleton_bnot x =
bnot (singleton x) == singleton (~ x)
singleton_band : {n} (fin n) => [n] -> [n] -> Bit
singleton_band x y =
band (singleton x) (singleton y) == singleton (x && y)
singleton_bor : {n} (fin n) => [n] -> [n] -> Bit
singleton_bor x y =
bor (singleton x) (singleton y) == singleton (x || y)
singleton_bxor : {n} (fin n) => [n] -> [n] -> Bit
singleton_bxor x y =
bxor (singleton x) (singleton y) == singleton (x ^ y)
singleton_shl : {n} (fin n) => [n] -> [n] -> Bit
singleton_shl x y =
shl (singleton x) y == singleton (x << y)
singleton_lshr : {n} (fin n) => [n] -> [n] -> Bit
singleton_lshr x y =
lshr (singleton x) y == singleton (x >> y)
singleton_ashr : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
singleton_ashr x y =
ashr (singleton x) y == singleton (x >>$ y)
////////////////////////////////////////////////////////////
// Sub-lemma properties: prove key techniques used in mul, urem, srem.
// Lemma: low bits of a product depend only on low bits of the operands.
// Specifically, (x * y) % 2^k == ((x % 2^k) * (y % 2^k)) % 2^k.
// This justifies using av * bv (the known-one values) to determine
// the low bits of the product when those low bits are fully known.
lemma_mul_low_bits : {n} (fin n, n >= 1) => [n] -> [n] -> [n] -> Bit
lemma_mul_low_bits x y k =
k < `n ==>
((x * y) && mask) == (((x && mask) * (y && mask)) && mask)
where mask = (1 << k) - 1
// Lemma: if y is divisible by 2^k (i.e., y % 2^k == 0 and y != 0),
// then (x % y) preserves the low k bits of x: (x % y) % 2^k == x % 2^k.
// Proof sketch: write y = 2^k * q. Then x = y*d + r with 0 <= r < y.
// Reducing mod 2^k: x ≡ r (mod 2^k), so r's low k bits equal x's.
lemma_urem_low_bits : {n} (fin n, n >= 1) => [n] -> [n] -> [n] -> Bit
lemma_urem_low_bits x y k =
k < `n ==> y != 0 ==> (y && mask) == 0 ==>
((x % y) && mask) == (x && mask)
where mask = (1 << k) - 1
// Lemma: if the dividend x >= 0 (as signed), then x %$ y >= 0 and
// x %$ y <= x (as unsigned), so clz(x %$ y) >= clz(x).
lemma_srem_nonneg_leading_zeros : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
lemma_srem_nonneg_leading_zeros x y =
y != 0 ==> x >=$ 0 ==> (x %$ y) >=$ 0
// Lemma: if x %$ y != 0 and x <$ 0, then x %$ y <$ 0.
// (srem has the sign of the dividend, unless the result is zero.)
lemma_srem_neg_sign : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
lemma_srem_neg_sign x y =
y != 0 ==> x <$ 0 ==> (x %$ y == 0 \/ x %$ y <$ 0)
// Lemma: |x %$ y| < |y|, so if |y| < 2^(w-k) then |x %$ y| < 2^(w-k),
// meaning the result has at least k sign bits.
lemma_srem_magnitude_bound : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
lemma_srem_magnitude_bound x y =
y != 0 ==>
(if x %$ y >=$ 0
then x %$ y < (abs_val y)
else (- (x %$ y)) < (abs_val y))
where abs_val v = if v >=$ 0 then v else - v
property lem1 = lemma_mul_low_bits`{8}
property lem2 = lemma_urem_low_bits`{8}
property lem3 = lemma_srem_nonneg_leading_zeros`{16}
property lem4 = lemma_srem_neg_sign`{16}
property lem5 = lemma_srem_magnitude_bound`{8}
property i01 = singleton_overlap`{16}
property i02 = singleton_zero_ext`{32, 16}
property i03 = singleton_sign_ext`{32, 16}
property i04 = singleton_concat`{16, 16}
property i05 = singleton_shrink`{8, 8}
property i06 = singleton_trunc`{8, 8}
property i07 = singleton_band`{16}
property i08 = singleton_bor`{16}
property i09 = singleton_bxor`{16}
property i10 = singleton_bnot`{16}
property i11 = singleton_shl`{8}
property i12 = singleton_lshr`{8}
property i13 = singleton_ashr`{8}