reduce: add a model-derived reference tactic (differential oracle)

[frankmcsherry]

Summary

Adds a second ReduceTactic — reference — that computes reduce's interesting times directly as the join-closure the formal model (formal/Differential/Model.lean) calls Reached, then evaluates them. It runs at parity with the default cursor tactic and exists to differential-test that tactic and tie the code to the proof. The default (cursors::CursorTactic) stays the only tactic on production paths; reference is opt-in.

Why

reduce's hard part is determining which times to re-evaluate (joins of input/output times). The optimized cursor tactic does this with an intricate incremental navigation; there was no independent implementation to check it against, and no executable link to the model. reference is both:

• a differential oracle — an independent determination whose output must match the cursor tactic on every input; and
• the operational form of the model — its determination is Reached, so agreement with the cursor is the operational↔declarative correspondence tested, and its agreement with f(accumulated input) is Model.lean's stream-correctness tested.

What it does

Per key, two phases:

• Determination (Reached) — close the seeds (batch + due pending) under join with the ground set (stored input/output times), truncated at upper. Computed the non-quadratic way: an ordered walk keeping its live join-partners an antichain by advancing them with the running meet. Time-only — reads the histories' times via a new TimeReplay, leaving each history intact.
• Application (emit_correct) — walk those times over the same loaded histories, keep accumulations tight by meet, apply the logic, emit corrections.

The naive (uncompacted) closure was ~230× slower on wide intervals; the meet-compaction is what makes it linear — the same idea the cursor tactic uses.

Also included: cursor tactic phase-split

cursors::CursorTactic's per-key compute is refactored into the same two phases (determination, then evaluation), so its structure mirrors the reference's. Semantically identical — validated by the full test suite. This touches the blessed tactic; happy to drop it into a separate PR if preferred.

Performance

Parity with the cursor tactic (examples/reduce_bench.rs, cursor vs reference): churn (reduce-dominated) ~1.0×, fewkeys (wide intervals) ~1.0×, bfs (iterative) ~1.0×.

Correctness & testing (tests/reduce_reference.rs)

• Differential (differential_*, bfs_*): cursor vs reference, assert_eq at every time, over Pair<u64,u64> partial-order random input with retractions, and an iterative BFS. The drift detector — run in CI to keep the tactics in sync.
• Oracle (oracle_*): each tactic vs a from-scratch f(accumulated input) at many times — the executable form of stream-correctness. Independent of the two agreeing, so it catches bugs in shared code (the driver, ValueHistory).
• Over-derivation (over_derivation, --features reduce-metrics): the reference is value-blind, so in theory it could derive extra zero-debt addresses. Measured across a cancellation-heavy density sweep: 1.00× — identical interesting-time counts.

Contract

reference computes the full Reached; the cursor tactic is a value-aware equivalent (its consolidation additionally drops advance-cancelled, zero-debt times). Both are output-equivalent; the tests verify output equality, not interesting-set equality — a set-size difference is not a bug.

Files

• src/operators/mod.rs — TimeReplay, ValueHistory::{walk, replay_times}.
• src/operators/reduce.rs — mod reference, reduce_trace_reference, feature-gated metrics; cursor phase-split.
• src/operators/arrange/arrangement.rs, src/collection.rs — reduce_reference entry points.
• tests/reduce_reference.rs, examples/reduce_bench.rs, Cargo.toml (reduce-metrics).

🤖 Generated with Claude Code