Fuse discovery and evaluation in the proxy reduce tactic

[frankmcsherry]

The proxy reduce tactic enumerated each key's interesting times and then walked them a second time to evaluate.
The conventional reduce does neither: it runs one ascending pass and evaluates as it discovers.
It can because discovery never looks backwards — every synthesized time is next_time.join(t) for a t not at or below next_time, so it is strictly greater, and new work only ever lands ahead of the sweep.

Sweep is that pass, cut where the conventional operator calls user logic.
Each next_crossing runs to the next in-interval time needing evaluation and suspends with the buffers positioned to read the accumulations; the caller evaluates and returns the corrections through commit; the next call resumes.
The tactic runs every live key to its next suspension and crosses them together, which is what a batched backend wants, and no key enumerates its times first.

It is written as a state machine rather than one body, so that each clause of formal/Differential/RoundCoverage.lean's round_coverage sits in one place: frontier finds the position, absorb steps the sources and decides whether the time is reached, close joins forward, settle recomputes the meet.

The second commit deletes what the sweep replaced.
discover_times lost its last caller, and KeyView, DiscoverScratch and TimeHistory existed only to serve it.
operators/common.rs goes with them: every live item in it had exactly one caller and all three callers were in int_proxy, so Sweep, tile_descriptions and update_meet move beside the tactic in int_proxy/reduce.rs and bilinear_wave into int_proxy/join.rs.
Net for the branch: -57 lines.

Measurements

tests/int_proxy_bench.rs, proxy tactic against the cursor tactic over identical ChunkSpine storage.
Both sides built in one target directory, three interleaved runs per binary, with the cursor mode carried as a control (it matched to within 1.5% across binaries throughout).

workload	cursor	before	after
churn 50k	50.1ms	30.7ms (0.61x)	28.1ms (0.56x)
churn 4M	4235ms	2614-2801ms (0.62-0.66x)	2419-2434ms (0.57x)
multimoment 10k	19.7ms	23.5ms (1.19x)	21.9ms (1.11x)
multimoment 1M	2293ms	2389ms (1.04x)	2171ms (0.95x)
wide 1M (String values)	2088ms	1909ms (0.91x)	1881ms (0.90x)
propagate (iterate, Product times)	2628us	3200us (1.22x)	3041us (1.16x)

On corgi, scc goes 4.84s to 4.47s with the vec control flat at 3.79-3.82s, so corgi/vec moves 1.27x to 1.17x.
reach is 293ms to 284ms and tour 188ms to 183ms, both near the noise floor.

A warning for anyone benchmarking the second commit on its own

Under the workspace release profile it appears to cost 8% on churn and multimoment.
That is an artifact of codegen-units, which [profile.release] leaves at the default 16 despite lto = true.
Rustc partitions codegen units by module, so folding common.rs into int_proxy/reduce.rs merges two partitions and the optimizer makes different choices.
Setting codegen-units = 1 makes the folded and unfolded arrangements indistinguishable, and both land at the faster number.
Code layout was ruled out separately, by permuting function order within an untouched file and remeasuring: that moves each arrangement by under 1% while the gap between them stays put.

Testing

cargo test -p differential-dataflow and -p interactive in debug, where debug_assert_sorted_bridge and the reduce_with_tactic contract checks are live.
That includes the ten int_proxy tests, which compare the proxy tactic against the mainline cursor reduce over the VecReduceBackend, and the twelve-program corgi-vs-vec differential gate.
Whole-workspace check under -D warnings.

🤖 Generated with Claude Code