The Shift of Theseus – Toy Bit Provenance Abstract Domain

The piece presents a bit-provenance abstract domain for optimizing integer-operation traces. Unlike a known-bits analysis, which records whether each bit is zero, one, or unknown, provenance records the original bit behind each position, including whether it has been inverted. This lets the optimizer recognize when bits in different values are identical even after masking or shifting. For example, if two operations produce the same low four bits of an input, the domain can prove that a later combination is redundant and replace it with one of those values. The goal is to capture chains of bit movement and reuse without requiring a growing collection of local rewrite rules.

The implementation represents each bit as a constant or a reference to a source operation and bit position. Transfer functions propagate this information through logical shifts and bitwise AND, OR, XOR, and inversion. They simplify cases such as a bit combined with itself or its complement; when a result cannot be described precisely, they assign it fresh provenance. Constant shifts preserve or reposition known bits, while an unknown shift discards useful relationships. The article builds these rules in a small optimizer, checks them with examples and property-based tests, and describes how the resulting analysis can expose constants, identities, reusable earlier values, and simpler shifts. It also considers evaluation in Pydrofoil and PyPy.