Extract novel times explicitly - #830
Draft
frankmcsherry wants to merge 1 commit into
Draft
Conversation
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 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Each proxy key has a of times exogenously flagged as "of interest", and we directly add to that when loading novel inputs, rather than leaving them to be discovered in an independently accumulated collection of diffs. This is meant to separate concerns (explicit identification of novel times) and allow further consolidation of novel and prior input (which may cancel, but can be one list of updates rather than two).