From 629cc9085e36eb81fadd3a1cad857df4e658afe7 Mon Sep 17 00:00:00 2001 From: Frank McSherry Date: Thu, 13 Aug 2026 12:21:12 -0400 Subject: [PATCH] Seeds travel as times; records travel netted MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The novel data's two roles part ways. Its time support — the thing that seeds interesting times — rides the window as a compact `seeds: Vec<(key_hash, T)>` channel, recorded raw from the novel batches before anything else touches them. Its records, which were only ever accumulants and join partners, merge into one input presentation with the prior history, where they net against it and are advanced by the meet like every other record. The invariant that forced the runs apart (#824) was about seeding, not presentation: consolidating novel against compacted history can cancel a record and lose its interesting time. Consolidation only cancels equal-((key, id), time) pairs, and such a time is by construction in the seed channel. `reduce_seed_survives_cancellation` pins exactly this: a novel retraction that exactly cancels the compaction-advanced prior record presents an EMPTY merged input, and the seed alone retracts the key's stale output. Coverage-wise, `round_coverage`'s witness clause reads only times — the seed list carries the same support the novel run did — and its closure's novel partners are the seed-derived `reached` set, whose clause the deleted novel-buffer clause merely duplicated. The Sweep loses its novel ValueHistory: one fewer load+build+step per key, `close` loses a clause, the frontier polls four sources, and the warned (due) times merge with the novel support into one seed list — they always played the same role. Novel records become meet-advanceable (they could not while moonlighting as witnesses), so buffers compact strictly better. Both backends present once per window: the vec backend nets cancelling pairs inline at the bridge push (novel and prior share the id space, so the pair meets adjacently), and corgi's single consolidation now nets across the runs, which the split presentations could not. Interleaved runs (x3, medians), cursor mode flat within 1.5% as the control: churn 19.7 -> 18.7ms/round (-5.1%, the netting — a round's retraction cancels the prior round's insertion in the presentation itself), wide -2.4%, multimoment -2.0%, propagate noise; ddir adt on corgi -1.7%, scc flat. Honest ledger: +31 code lines net. The invariant moves from structural (two runs, raw one in hand) to contractual (the seeds obligation) plus a regression test; in exchange the tactic's reasoning core shrinks and the runtime shape improves. Co-Authored-By: Claude Fable 5 --- .../src/operators/int_proxy/reduce.rs | 187 ++++++++++-------- .../src/operators/int_proxy/vec_backend.rs | 26 ++- differential-dataflow/tests/int_proxy.rs | 33 ++++ interactive/src/corgi/reduce.rs | 28 ++- 4 files changed, 184 insertions(+), 90 deletions(-) diff --git a/differential-dataflow/src/operators/int_proxy/reduce.rs b/differential-dataflow/src/operators/int_proxy/reduce.rs index 736fcf817..1e46d2c4f 100644 --- a/differential-dataflow/src/operators/int_proxy/reduce.rs +++ b/differential-dataflow/src/operators/int_proxy/reduce.rs @@ -30,31 +30,35 @@ pub struct ReduceInstance<'a, B1: BatchReader, B2: BatchReader