Methodology notes for behavioral-equivalence testing: proving that a program transformation — an optimizer pass, a refactor, a transpiler, a minifier — changed nothing observable.
The question every transformation project eventually faces: fast is easy to measure; same is hard. These notes are the hard half.
| Note | The problem it attacks |
|---|---|
| scenario-inventory | "we tested it" with no list of what it includes |
| differential-oracles | needing an expected output you cannot write by hand |
| observability-boundary | deciding what counts as "the same behavior" before the argument starts |
| combinatorial-explosion | the pairwise matrix that quietly became 10⁶ cells |
| minimize-the-specimen | fixing the 400-line failure instead of the 6-line cause |
| nondeterminism-is-input | phantom failures and silent passes from unseeded randomness |
| golden-files-rot | the bulk snapshot update that approves everything |
| stream-equivalence | chunk-exact oracles failing on identical behavior |
| concurrent-equivalence | demanding sequential order from a parallelization |
| property-tests-are-half-an-oracle | invariants passing while the function changed |
| environment-is-part-of-the-program | a differential pair that passed because both sides ran in the same wrong environment |
| the-power-bound-is-the-result | a "no difference" reported without the effect size the study could have detected |
| byte-identity-is-a-perfect-oracle | behavioral oracles leak at "equivalent enough" |
- An equivalence claim names its observability boundary first: outputs, exit codes, throw paths, observable ordering, timings excluded or included. Unnamed boundaries are where "equivalent" goes to die.
- The scenario inventory is an artifact, not a vibe: a list a stranger can run, with the empty/long/malformed cases present by construction.
- A failing equivalence test is a specimen: minimize it before fixing anything. The minimized counterexample is the deliverable; the fix is the cleanup.
Orvii — Open, Research, Vision, Innovation & Ideas. Born as the public half of a private optimizer's test gate; the gate stays private, the method does not.
Part of the Orvii research set: harness-atlas · convention-map · provider-reliability · context-file-evidence · retractions · svg-instruments · bench-notes · ts-lto-research.