Bit projections and highest differing positions

Natural numbers represent bit strings, with an explicit width for bounded-word comparisons. Projections retain selected positions in list order; finite-set sketches sort those positions by significance. Prefix boundaries replace the low bits with fixed masks.

Main definitions

• differingBits, highestDiff: differing positions below a given width and their maximum.
• projectBits, sketch: list and finite-set bit projections.
• lowerBoundary, upperBoundary: words with a shared high prefix and fixed low-bit masks.

Main results

• highestDiff_spec: distinct bounded words differ at their highest differing position.
• projectBits_lt: a selected highest differing position preserves strict order.
• projectBits_ofFn_eq_sum: the positional numeric value of a projection.
• boundary_prefix: both boundaries preserve the high prefix.

References

See [FW93] for the use of significant-bit projections in fusion trees.

def Cslib.BitString.differingBits (w x y : ℕ) : Finset ℕ

The positions below w where the binary representations of x and y differ.

def Cslib.BitString.highestDiff (w x y : ℕ) : ℕ

The highest differing position below w, or zero when there are no differing positions.

theorem Cslib.BitString.testBit_eq_false_of_width {w x i : ℕ} (hx : x < 2 ^ w) (hi : w ≤ i) : x.testBit i = false

All bits at or above the word width of a bounded natural number vanish.

theorem Cslib.BitString.highestDiff_mem {w x y : ℕ} (hx : x < 2 ^ w) (hy : y < 2 ^ w) (hne : x ≠ y) : highestDiff w x y ∈ differingBits w x y

The highest differing bit is below the word width and really differs.

theorem Cslib.BitString.testBit_eq_of_highestDiff_lt {w x y i : ℕ} (hx : x < 2 ^ w) (hy : y < 2 ^ w) (hi : highestDiff w x y < i) : x.testBit i = y.testBit i

Two bounded words agree at every position above their highest differing bit.

theorem Cslib.BitString.highestDiff_spec {w x y : ℕ} (hx : x < 2 ^ w) (hy : y < 2 ^ w) (hne : x ≠ y) : highestDiff w x y < w ∧ x.testBit (highestDiff w x y) ≠ y.testBit (highestDiff w x y) ∧ ∀ (i : ℕ), highestDiff w x y < i → x.testBit i = y.testBit i

Unequal bounded words differ at highestDiff and share all more significant bits.

theorem Cslib.BitString.highestDiff_lt_iff_shiftRight_eq {w x y cut : ℕ} (hx : x < 2 ^ w) (hy : y < 2 ^ w) (hne : x ≠ y) : highestDiff w x y < cut ↔ x >>> cut = y >>> cut

For distinct bounded words, deleting their lowest cut bits leaves the same prefix exactly when cut lies above their highest differing position.

theorem Cslib.BitString.shiftRight_highestDiff_add_one_eq {w x y : ℕ} (hx : x < 2 ^ w) (hy : y < 2 ^ w) (hne : x ≠ y) : x >>> (highestDiff w x y + 1) = y >>> (highestDiff w x y + 1)

The prefix above the highest differing bit is shared.

theorem Cslib.BitString.shiftRight_highestDiff_ne {w x y : ℕ} (hx : x < 2 ^ w) (hy : y < 2 ^ w) (hne : x ≠ y) : x >>> highestDiff w x y ≠ y >>> highestDiff w x y

The prefix including the highest differing bit is not shared.

theorem Cslib.BitString.highestDiff_bits_of_lt {w x y : ℕ} (hx : x < 2 ^ w) (hy : y < 2 ^ w) (hxy : x < y) : x.testBit (highestDiff w x y) = false ∧ y.testBit (highestDiff w x y) = true

At the highest differing bit, the smaller word has zero and the larger word has one.

def Cslib.BitString.projectBits : List ℕ → ℕ → ℕ

Pack the indicated bits, least significant position first. Repeated or unordered positions are allowed; order preservation additionally requires the list to be strictly increasing.

theorem Cslib.BitString.projectBits_eq {positions : List ℕ} {x y : ℕ} (h : ∀ i ∈ positions, x.testBit i = y.testBit i) : projectBits positions x = projectBits positions y

Agreement at all selected positions implies equal projections.

theorem Cslib.BitString.testBit_projectBits (positions : List ℕ) (x i : ℕ) (hi : i < positions.length) : (projectBits positions x).testBit i = x.testBit positions[i]

Bit i of the packed projection is the input bit at the i-th selected position.

theorem Cslib.BitString.projectBits_lt {positions : List ℕ} {x y b : ℕ} (hsorted : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) positions) (hb : b ∈ positions) (hx : x.testBit b = false) (hy : y.testBit b = true) (habove : ∀ (i : ℕ), b < i → x.testBit i = y.testBit i) : projectBits positions x < projectBits positions y

A selected highest differing bit makes the projection strictly ordered.

theorem Cslib.BitString.projectBits_lt_two_pow (positions : List ℕ) (x : ℕ) : projectBits positions x < 2 ^ positions.length

Every projection fits in the number of bits selected by its position list.

def Cslib.BitString.sketch (positions : Finset ℕ) (x : ℕ) : ℕ

The perfect sketch packs the bits in a finite set in increasing significance order.

theorem Cslib.BitString.sketch_lt_two_pow (positions : Finset ℕ) (x : ℕ) : sketch positions x < 2 ^ positions.card

A perfect sketch is a word with one bit per selected position.

theorem Cslib.BitString.sketch_lt_of_highestDiff_mem {w x y : ℕ} {positions : Finset ℕ} (hx : x < 2 ^ w) (hy : y < 2 ^ w) (hxy : x < y) (hmem : highestDiff w x y ∈ positions) : sketch positions x < sketch positions y

Retaining the highest differing bit suffices to preserve an ordered pair of bounded words.

theorem Cslib.BitString.shiftRight_mono {x y : ℕ} (h : x ≤ y) (cut : ℕ) : x >>> cut ≤ y >>> cut

Deleting a fixed number of low bits preserves weak order.

theorem Cslib.BitString.shiftRight_eq_of_between {x y z cut : ℕ} (hxy : x ≤ y) (hyz : y ≤ z) (hprefix : x >>> cut = z >>> cut) : y >>> cut = x >>> cut

A prefix shared by the endpoints of an interval is shared by every word between them.

theorem Cslib.BitString.testBit_eq_of_shiftRight_eq {x y cut : ℕ} (h : x >>> cut = y >>> cut) {b : ℕ} (hb : cut ≤ b) : x.testBit b = y.testBit b

Equal prefixes imply agreement at all positions retained by the prefix.

theorem Cslib.BitString.highestDiff_eq_of_testBit {w x y p : ℕ} (hp : p < w) (hdiff : x.testBit p ≠ y.testBit p) (habove : ∀ (b : ℕ), p < b → x.testBit b = y.testBit b) : highestDiff w x y = p

A differing bit with agreement everywhere above it is the highest differing bit.

def Cslib.BitString.lowerBoundary (q p : ℕ) : ℕ

Keep the prefix above p, set bit p to zero, and set every lower bit to one.

def Cslib.BitString.upperBoundary (q p : ℕ) : ℕ

Keep the prefix above p, set bit p to one, and set every lower bit to zero.

theorem Cslib.BitString.testBit_lowerBoundary (q p b : ℕ) : (lowerBoundary q p).testBit b = if p < b then q.testBit b else decide (b < p)

The lower boundary agrees with the query above p and has the indicated low-bit mask.

theorem Cslib.BitString.testBit_upperBoundary (q p b : ℕ) : (upperBoundary q p).testBit b = if p < b then q.testBit b else decide (b = p)

The upper boundary agrees with the query above p and has only bit p set below it.

theorem Cslib.BitString.boundary_prefix (q p : ℕ) : lowerBoundary q p >>> (p + 1) = q >>> (p + 1) ∧ upperBoundary q p >>> (p + 1) = q >>> (p + 1)

Both correction boundaries keep the query's full prefix above p.

theorem Cslib.BitString.projectBits_le {positions : List ℕ} {x y : ℕ} (h : ∀ b ∈ positions, x.testBit b = true → y.testBit b = true) : projectBits positions x ≤ projectBits positions y

Pointwise implication between selected bits implies weak order of the packed sketches.

theorem Cslib.BitString.lt_iff_shiftRight_lt_of_ne {x y cut : ℕ} (hne : x >>> cut ≠ y >>> cut) : x < y ↔ x >>> cut < y >>> cut

Different prefixes compare in the same direction as the full words.

theorem Cslib.BitString.sketch_le_lowerBoundary {positions : Finset ℕ} {x q p : ℕ} (hprefix : x >>> (p + 1) = q >>> (p + 1)) (hbit : x.testBit p = false) : sketch positions x ≤ sketch positions (lowerBoundary q p)

Within a prefix block whose bit p is zero, the lower correction boundary has a sketch at least as large as every word in that block.

theorem Cslib.BitString.upperBoundary_le_sketch {positions : Finset ℕ} {x q p : ℕ} (hprefix : x >>> (p + 1) = q >>> (p + 1)) (hbit : x.testBit p = true) : sketch positions (upperBoundary q p) ≤ sketch positions x

Within a prefix block whose bit p is one, the upper correction boundary has a sketch at most as large as every word in that block.

theorem Cslib.BitString.projectBits_ofFn_eq_sum {r : ℕ} (b : Fin r → ℕ) (x : ℕ) : projectBits (List.ofFn b) x = ∑ i : Fin r, (x.testBit (b i)).toNat * 2 ^ ↑i

A projection's bits have their usual positional numeric value.