Highest differing bits through exclusive or

Main results

• highestDiff_eq_log2_xor: the highest differing bit is the highest set bit of exclusive or.
• highestDiff_le_of_xor_le: comparing exclusive-or values suffices to compare divergences.

References

See [FW93] for longest-prefix selection in fusion nodes.

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

The most significant set bit of exclusive or is the highest differing bit. Distinct inputs ensure that this index identifies an actual set bit.

theorem Cslib.BitString.highestDiff_le_of_xor_le {w q x y : ℕ} (hq : q < 2 ^ w) (hx : x < 2 ^ w) (hy : y < 2 ^ w) (hqx : q ≠ x) (hqy : q ≠ y) (h : q ^^^ x ≤ q ^^^ y) : highestDiff w q x ≤ highestDiff w q y

Smaller exclusive-or values have no higher differing position. This includes ties in the highest differing position while retaining a concrete one-comparison selection rule.