Token-generic, windowed int-proxy tactics, with reference backends and benchmarks - #808
Open
frankmcsherry wants to merge 18 commits into
Open
Token-generic, windowed int-proxy tactics, with reference backends and benchmarks#808frankmcsherry wants to merge 18 commits into
frankmcsherry wants to merge 18 commits into
Conversation
The proxy tactics fixed both bridge coordinates at u64; the time-logic library beneath them (ValueHistory, bilinear_wave, discover_times) was already generic at V: Copy + Ord, so u64 was an instantiation posing as the architecture. This makes the tokens backend-chosen associated types: * `Group: Copy + Ord + 'static` on both backend traits: the granule name, commonly a u64 key hash but exactly the key for small Copy keys (collisions then impossible), wider hashes for insurance. `'static` because groups are the one token that crosses invocations (pending times are held per group). * `Token: Copy + Ord` (per input side on join: Token0/Token1): the ephemeral value token, scoped to one invocation. * `ProxyBridge<G, I, T, R>`; `bilinear_wave` widened to distinct value types per side; `KeyView`, `DiscoverScratch`, `discover_times`, and `IdHistory` generalized to match. Tests are invariant under (u64, u64); no in-tree backend impls existed to migrate. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
JOIN materialized whole-instance bridges (present0/present1) and all outputs eagerly, returning a Vec costumed as Box<dyn Iterator>; REDUCE was windowed but staged seed_times for the entire invocation up front (its own doc comment asked for the fix). Both tactics now stream in ascending group order with peak state O(window): * JOIN: present0/present1 are replaced by next_window, yielding a JoinWindow of both inputs' presentations for a contiguous group range. Units are genuinely lazy: JoinUnit owns its batches and produces outputs window by window as the join driver's fuel drains it — the driver already held units across activations, the proxy tactic just never delivered a lazy one. The backend sits behind Rc<RefCell<_>> since half-drained units from both input queues interleave; per-unit progress lives in the unit's opaque cursor, never on the backend. Fresh is now Copy. * REDUCE: seed_times is deleted; seeds arrive per window on ReduceWindow (novel-batch time support, with the discover_times seeding contract documented on the field). next_window now takes the pending groups (all the harness knows that the backend does not) and must cover novel-input groups union pending; a debug_assert checks all pending groups were covered. The empty-invocation fast path checks batch lengths instead of staged seeds. No in-tree backends existed to migrate; validation is compile-level until the reference backends land (next step). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The value-token instantiation from the seam design as a behavioral test (tests/int_proxy_graphs.rs): edges (src, dst) grouped by source, with Group = u32 the source itself (exact, no hashing) and the whole edge as the value token (self-redeeming: cross and finish build outputs from tokens alone). Oracle tests drive both tactics directly — join against a naive nested-loop join, reduce (per-source counts, with corrections and full retractions) against per-time accumulation — at window sizes down to one group per window. Writing the backend surfaced two protocol corrections, applied here: * JOIN: the per-unit resumption state is now `type Cursor: Default` on the backend, owned by the unit. A single usize could not carry real resumption state (a position per batch per side), and unit progress cannot live on `&mut self` since half-drained units interleave. * REDUCE: next_window loses its cursor parameter entirely — a retire's windows all happen within one synchronous begin/finish-bracketed call, so the backend keeps progress in its session state. The pending-coverage check moves to the harness, which now verifies ascending windows and that no pending group is skipped, from window.keys alone. Not yet exercised: the pending path (carried interesting times), which requires partially ordered time to arise; that belongs to the partial-order test alongside the hash and ordinal backends. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
tests/int_proxy_bytes.rs: the compressing-token instantiation over opaque [u8] rows of unknown shape, stored columnar (bytes + bounds + aligned time/diff columns) with a stored (G, I) token column computed at formation — presentation is a column read, never a re-hash. Group collisions are *resolved*, not detected: join's cross re-checks real key bytes and drops false pairs; reduce partitions each granule by real key and reduces the parts separately. Weak-hash tests force both collision kinds: value collisions panic at their T1 site (formation, redemption, stash); group collisions must yield byte-identical output to the naive oracle. A six-angle adversarial review of the branch produced fixes applied here: Harness contract completeness: * Stray records/seeds — anything presented for a group absent from window.keys was silently discarded by the skip loops; now hard asserts (per-key strays-below, end-of-window trailing). * Empty-window progress guards: a backend returning Some with nothing presented used to hang the retire loop / scheduler; now asserted. * Ascending-window watermark: one shared checker (assert_ascending_ window) replaces two divergent inline copies; pending-coverage and watermark checks upgraded from debug_assert to hard asserts — the failure class (dropped carried times, released capabilities, lost matches) is silent corruption, and the checks are O(1)/window. * Join's fresh-coverage clause documented as uncheckable (the harness is data-oblivious); missing it silently loses matches. Indirection-tax fixes in JoinUnit: * Yields per key rather than per window: ready holds at most one key's containers instead of a whole window's cross product. * Match buffers and replay histories hoisted onto the unit; cross now takes slices, ending the mem::take capacity destruction each flush. * Reduce phase 2 sweeps a live-key list with swap-remove rather than rescanning exhausted slots under moment-count skew. Reference-backend upgrades: * Fresh-side driving restored (the old present0-then-filter behavior): both join backends window over the fresh side's groups and skip the accumulated side's others — O(fresh) presentations, empty fresh side free. * Interleaved-units test: two half-drained units alternately polled against one shared backend, the scenario that motivated type Cursor. * started flags replaced by idempotent resize; RowBatch::form now uses consolidate_updates; test-grade patterns (next_group rescan, redeem by search) labeled with the real-backend alternative. Deferred with notes: window-buffer recycling in the protocol, scratch pooling vs the Token 'static bound (both for SEAM.md open items). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
examples/int_proxy_bench.rs measures the indirection tax where it is purest: value tokens (G = src, token = edge), so every gap is protocol, not tokenization. Hand-written merge-join and streaming count over the same batches are the baselines. Release mode, best of 5. Numbers at 100k keys, fanout 4 (400k edges/side), window 1024: join native 7.5ms proxy 16.9ms 2.26x reduce native 0.36ms proxy 17.3ms ~48x Localization by sweeps: * Window size (64 / 1024 / 65536): join flat at 2.3-2.7x; reduce flat through 1024 and WORSE at 65536 (35ms — oversized phase-2 state). Harness crossings are not the bottleneck at sane window sizes. * Values per key (fanout 1 / 4 / 16): reduce per-key cost 85ns -> 173ns -> 632ns. The tax scales with replay volume: per-key ValueHistory loads, TimeHistory sorts, and discovery machinery — running on data with exactly ONE moment, where discovery is pure overhead. Reading: the join tax (~2.3x) is bridge materialization plus output allocation — the window-buffer recycling and resumable-wave items on SEAM.md's open list. The reduce tax is dominated by running the full interesting-times apparatus per key on single-moment granules; the top optimization candidate is a single-moment fast path (after advancing, all times equal -> skip discovery and replay, evaluate once, subtract output). Native count is also not an incremental operator, so the fair gap is smaller than 48x — but the snapshot case is common enough that the fast path should exist before this number is taken at face value. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
tests/int_proxy_pending.rs exercises the last unexercised clause of the windowed reduce contract: carried interesting times. Updates at incomparable Pair times (0,1) and (1,0) make their join (1,1) an interesting time beyond the retire's upper frontier; the test asserts it is pended (returned in the frontier, holding the capability), carried by the tactic, and handed back as a pending group next retire — where it must appear in a window with no novel input, merged in group order with a novel-only group at window size 1. A grid oracle over the partial order checks exact per-key counts at every probe, confirming the deferred correction collapses the two partial counts. The hard pending-coverage asserts run live throughout. tests/common/mod.rs extracts the shared scaffold the review prescribed (EdgeBatch<T>, the value-token join/reduce backends generic over the timestamp, Pair itself) before this third test could become the third copy; int_proxy_graphs.rs now uses it. The byte-rows test keeps its own scaffold deliberately — its columnar layout is the point. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The bench localized the reduce tax to per-key discovery/replay running on granules with exactly one interesting moment — the steady-state snapshot shape. This adds the safe fast path: when a key has no pending times, exactly one distinct seed time t*, and every presented input and output time at-or-before t*, then discover_times would compute moments == [t*] with nothing pended (history times before t* pass without becoming moments; no join can escape t*), so the key is evaluated directly from its bridge slices — no TimeHistory loads, no ValueHistory replays, no KeyState. Fast keys batch into one window-wide reduce_corrections call (round zero); their corrections go straight to the tiles. Keys with no seeds and no pending are skipped outright. Bench (100k keys, window 1024, release, best of 5): fanout 4: 17.3ms -> 7.6ms (48x -> 20x vs native count) fanout 1: 8.5ms -> 5.2ms (24x -> 11.5x) Remaining cost is presentation-side (whole-window consolidate_updates sorts in the backend, bridge allocation) — the open buffer-recycling and k-way-merge items, not harness machinery. tests/int_proxy_graphs.rs gains reduce_multitime_rounds: two distinct times per retire under total order, so the slow path stays exercised (a two-seed key cannot take the fast path) and fast and slow keys mix within one window. The partial-order pending test covers the other slow-path shapes. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
reduce_fuzz_matches_oracle: deterministic LCG-driven rounds of random insertions and retractions over a small key space, times randomized within each round's width-3 interval so every round mixes fast-path keys (one distinct time) with slow-path keys, at window sizes 1/3/100, checked against exact per-time counting after every round. This is the empirical half of the fast-path equivalence argument (the analytic half: under the guard, discover_times computes moments == [t*] with nothing pended, and the round-zero accumulation equals the slice consolidation). Retractions draw only from prior rounds' insertions so every prefix accumulation stays non-negative. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The hand-written natives are a floor; the decision-relevant comparison
is against the shipping cursor tactics on the same real storage. The
bench now builds OrdValBatch inputs and consumes them two ways: the
cursor tactics directly, and the proxy tactics through backends that
present from those same batches via the same cursors — identical
storage access, so the difference is pure protocol.
The cursors modules in join.rs/reduce.rs become public (the tactic
entry points already were; these are the incumbent reference
implementations, and benches and differential tests drive them
directly).
Results (100k keys, window 1024, release, best of 5):
join fanout 4: cursor 14.4ms proxy 21.6ms 1.50x
fanout 1: cursor 3.4ms proxy 3.9ms 1.16x
reduce fanout 4: cursor 12.0ms proxy 8.4ms 0.70x
fanout 1: cursor 6.8ms proxy 5.6ms 0.83x
Reading: against the incumbent (rather than the non-incremental native
floor) the join protocol costs 1.2-1.5x — the bridge copy and staging
double-write, partially offset by the proxy's batch-at-a-time group
processing. The proxy REDUCE is 17-30% FASTER than the cursor
incumbent: the single-moment fast path skips per-key interesting-time
machinery the cursor path always runs. The decoupling is not a tax on
reduce at all on snapshot-shaped work; it is currently a modest tax on
join with identified, protocol-level fixes queued (buffer recycling,
cross-by-emit).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The two measured per-record taxes in the join protocol, removed:
* cross (staged slices) becomes absorb + flush: each match goes
straight from the merge to the backend, which accumulates into its
own output representation and yields containers at its own size
target (JOIN_CHUNK leaves the harness — container granularity is the
backend's decision). The li/ri/ot/od staging buffers are deleted
outright: the double-write goes away, not just its allocation.
join_key emits through a closure; the wave path feeds absorb
directly.
* next_window (both tactics) gains a reuse parameter returning the
previous, fully-processed window, so backends clear() and refill
with retained capacity instead of allocating fresh bridges per
window — the steady-state allocation churn item from the review.
Bench movement (100k keys, window 1024, release, best of 5):
join vs native: 2.7x -> 1.49x (fanout 4)
join vs cursor incumbent: 1.50x -> 0.94x (fanout 4)
1.16x -> 0.90x (fanout 1)
reduce vs cursor: 0.70x -> 0.68x
Both proxy tactics are now FASTER than the shipping cursor tactics on
identical OrdValBatch storage. The remaining gap to the hand-written
native floor (1.49x) is the bridge presentation copy itself, which is
the present-by-reference / lens territory deliberately parked in
SEAM.md.
All backends updated (graphs/common, bytes, bench x2); the bytes
absorb keeps the group-collision key re-check per match. Tests
unchanged in behavior; test backends use small container targets to
exercise multi-container yields.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The adversarial review of the absorb/flush protocol found a real bug in it: staged output lived on the backend, which all live units share (Rc<RefCell>, and the driver interleaves half-drained units under fuel). Unit A could pause holding a partial container in the shared buffer; unit B's next container would then ship A's matches — under B's capability, into B's output stream — and a unit dropped at shutdown would leave residue poisoning every later unit. The fix is the write-side twin of the Cursor finding: `type Sink: Default` on ProxyJoinBackend, owned by the unit, passed to absorb and flush. Per-unit state now has both halves — read progress (Cursor) and output staging (Sink) — and neither can live on `&mut self`. The review also caught that the interleaving regression test was blind: with target = 1 staging empties at every yield, so the bug shape passes. The test now uses target = 2 with a 3-match key, so a unit pauses mid-stream holding a straddling partial container; the bug shape was temporarily re-injected to confirm the test fails against it, then removed. Also from the review: docs reconciled to the absorb/flush protocol (the trait narrative and the bytes/graphs module headers still named `cross`; the container-boundary parity clause is now stated on absorb; JoinUnit's peak-state claim now counts one key's containers in `ready`); reuse vecs route back to the side they served (they alternated duties under Fresh::Input1, growing both to max capacity); two rustdoc links introduced by publishing `cursors` fixed; bench reduce backends hoist a per-key allocation off the proxy side. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
examples/scc_proxy.rs runs the stock SCC computation with trim_edges' two joins substituted through join_with_tactic and a value-token proxy backend over the same ValSpine arrangements (Group = the key itself, tokens = the values; time-generic, so it runs at the nested Product<usize, usize> of the iterative scope). propagate and all other stages are stock; SCC_VALIDATE=1 runs stock strongly_connected alongside and asserts exact agreement at every time (verified through load plus incremental rounds). This is the proxy tactics' first run inside a real dataflow, and a deliberately hostile one: nested iteration, Product timestamps, regions, and many fuel-interleaved lazy units live at once — the scenario the unit-owned Cursor/Sink state exists for. The harness's hard asserts (ascending windows, progress) ran throughout. Numbers (1 worker, release, batch 1000, 5 rounds), stock vs proxy: 100k nodes / 200k edges: load 4.35s vs 4.28s; rounds ~2.71s vs ~2.67s 200k nodes / 400k edges: load 10.33s vs 10.04s; rounds ~4.38s vs ~4.31s Parity with a consistent slight edge — as the microbenchmarks predict (join at 0.90-0.95x of the cursor tactic) once diluted by the rest of the dataflow. One comparison hazard worth recording: an earlier draft accidentally used propagate_at's label-staggering variant and appeared 7-20x faster; the numbers above use |_| 0 exactly as stock, and the validation mode exists so that mistake class gets caught by an oracle rather than by suspicion. The backend needed no cursor-bound vocabulary at all: plain Data bounds and the projections normalize. (Asserting redundant Key<'a> = &'a K equalities actually breaks the trait solver — deleting them was the fix.) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The PR carried ~2.7k lines of tests and benches against a ~280-line
net library change. Pruned by the criterion: keep tests that check
general properties against oracles, drop demonstrations and anything
that locks in current behavior.
Removed:
* examples/int_proxy_bench.rs — a benchmark, not an example. Its
numbers and their analysis are recorded in the branch's commit
messages; the harness is recoverable from history when next needed.
* tests/int_proxy_bytes.rs — the [u8]-rows recipe was a demonstration
wearing a test costume. Its genuinely general content (collision
resolution under compressing tokens) goes with it for now; the
hashed-token instantiation is currently uncovered, noted as a gap
for a slimmer future test.
Consolidated tests/{common/mod.rs, int_proxy_graphs.rs,
int_proxy_pending.rs} into one tests/int_proxy.rs (821 lines) keeping
the property tests: join vs a naive oracle, reduce vs exact per-time
counting, the randomized differential fuzz, the multi-time slow-path
oracle, the partial-order pending contract, and interleaved-unit
isolation (which pinned the Sink bug and is verified to fail against
the bug shape).
examples/scc_proxy.rs stays: it is an actual example (how to write a
backend and mount the tactic in a dataflow), and its SCC_VALIDATE
oracle is the deepest integration check we have.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…at proxy joins Audit of whether the int-proxy join carries the bug fixed in TimelyDataflow#802 (in-flight batches overtaken by advance_upper, silently dropped): * The bug lived in join_with_tactic's driver — the acknowledged- frontier admission guard — which both tactics share, and this branch is based past the fix (59dfd3d, f8f1645); its only diffs to join.rs are a derive and module visibility. The proxy path inherits the fix. * The tactic-level assumptions survive the fix's new admission rule: `meet` is the timely message capability, which lower-bounds the fresh batch's times on the overtaken path exactly as elsewhere (overtaking changes which batches are admitted and what the opposing trace reads through, not the capability relationship), so the backend's advance-by-lower algebra and the exactly-once argument (driver-level, tactic-agnostic) are unaffected. * Empirically: SCC_STAGGER=1 switches both the proxy trim and the oracle to the prioritized strongly_connected_at shape (labels introduced in rounds — the TimelyDataflow#801 trigger), and the oracle-validated runs at the regression suite's sizes (10/20 x 1000 single-edge rounds, 100/200 x 10, 100/2000) with three workers all pass: exact agreement at every time. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
They were made public solely so the (since pruned) benchmark could drive them directly; with that gone, nothing outside the crate names them, and the public surface shrinks back. The intra-doc link fix stays. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This PR's role is the protocol substrate for the Corgi/DDIR work (TimelyDataflow#795): the reshaped int-proxy tactics that its columnar backends port onto. Under that lens the SCC example's job — in-dataflow validation against a real backend — is superseded by the Corgi backend's differential gate (whole .ddp programs vs the vec reference), which is the stronger version of the same check. The example's findings stay on the record in its commits (1bc0752, ed19240): proxy joins at parity with join_core end-to-end, oracle-validated including under the TimelyDataflow#801 trigger shape at the regression suite's sizes. What remains in-tree is the harness's own property suite (tests/int_proxy.rs), which guards the contract the Corgi port will code against and is the one thing the downstream gate does not cover. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Two items from downstream (TimelyDataflow#795) review of the substrate: * retire's final zip would silently truncate a backend returning the wrong number of batches from finish(), shipping batches at the wrong held times. Now a hard assert (one batch per tile description), consistent with the harness's fail-loudly posture. * join_key's >=16x>=16 bilinear_wave path had no in-tree exercise — every key in the property suite was small, and the SCC example that covered the path was pruned. join_wave_path_matches_naive builds one deliberately fat key (20 presented records per side: spread-time insertions plus non-cancelling retractions, so consolidation keeps all of them) alongside a small key, so both join_key paths run in one unit, against the naive oracle. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Review feedback: the unit had become a flat 13-field bag with no visible organization — one field accreted per protocol change, none of them prompting reorganization. The grouping that was missing is the protocol itself, so the type now displays it: * Task — the immutable work description (batches, fresh side, capability time), with the JoinInstance construction as its method. * The shared backend and the two per-unit state halves it interprets: cursor (read resumption) and sink (output staging). * Phase — the window machine, previously three fields in a trench coat (done + flushed + current: Option): Fetch, Merge(window, i, j), Drained, Spent. next() is now a match over it, and the can't-flush-twice property is the state graph rather than a boolean to reason about. * spent + high — the harness's reuse stash and ascending-window watermark; h0/h1 merge scratch; ready the output queue. WindowFor<B0, B1, Bk> names the bridge type that was previously spelled out six-parameters-long at each use. No behavioral change; the suite is the witness. 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.
Generalizes the int-proxy tactics from
u64-only proxies to backend-chosen tokens and brings both tactics to windowed streaming operation. This is the substrate for the Corgi/DDIR work (#795): its columnar backends are the intended first real consumers, and this PR reshapes the protocol they port onto. Validation here is the harness's own property suite plus measurements recorded below; end-to-end validation lands with the Corgi gate. Both proxy tactics measured faster than the cursor tactics on identicalOrdValBatchstorage (join 0.90–0.95×, reduce 0.58–0.70×).Tokens (
70d7e288)ProxyBridge<G, I, T, R>; backends chooseGroup: Copy + Ord + 'static(the granule name — commonly au64key hash, exactly the key for smallCopykeys, in which case collisions are impossible) and per-sideToken: Copy + Ord(invocation-scoped value tokens). The time-logic library beneath (ValueHistory,bilinear_wave,discover_times) was already generic at this bound;u64was one instantiation posing as the architecture.'staticsits exactly on the one token that crosses invocations, encoding the memory rule in types.Streaming protocols (
e197207f,b52cac66,3945cb8e)present0/present1+ eager whole-instance staging withnext_window(bounded group-range presentations of both sides) driven through a genuinely lazyJoinUnit— the driver already drained units under fuel across activations; the tactic now delivers a lazy one. Matches flow one at a time to the backend'sabsorb, which cuts output containers at its own granularity;flushyields the remainder. No match is ever staged in the harness.seed_timesstaging its own doc comment apologized for: seeds arrive per window onReduceWindow, andnext_windowreceives the pending groups (all the harness knows that the backend does not). Peak state is O(window) for both tactics.Cursor(read progress — a resumption state richer than theusizethe first draft assumed) andSink(output staging). Neither can live on&mut self: half-drained units from both input queues interleave against one shared backend. TheSinkhalf fixes a real bug the review found in the firstabsorbdraft — shared staging shipped one unit's matches in another unit's containers, under the wrong capability. The interleaving regression test pauses a unit mid-stream holding a straddling partial container, and was verified to fail against the bug shape.next_window(..., reuse)for capacity reclamation.Harness contract enforcement
The harness now hard-asserts (not
debug_asserts) the window contract clauses whose violation is silent corruption rather than a crash: strictly ascending windows (shared checker), pending-group coverage, no stray/trailing records or seeds outsidewindow.keys, and per-window progress. Join's fresh-side coverage clause is documented as uncheckable (the harness is data-oblivious); the reference backends and oracle tests are its enforcement.Single-moment fast path (
9a7a1262)When a key has no pending times, one distinct seed time, and history at-or-before it, the harness evaluates directly from the bridge slices — no discovery, no replays — with one batched crossing per window. This is the steady-state snapshot shape, and it was the dominant per-key cost. Equivalence is argued against
discover_times(under the guard: moments =[t*], nothing pended) and checked by a deterministic fuzz test mixing fast- and slow-path keys against an exact per-time oracle; a multi-time test keeps the slow path exercised.Property tests (
tests/int_proxy.rs)One consolidated file of oracle-backed property tests over the value-token instantiation (
G = srcexact, token = the edge): join vs a naive nested-loop oracle (including a fat-key case that runs the ≥16×≥16bilinear_wavepath, which no small-key test reaches); reduce vs exact per-time counting, including a randomized differential fuzz mixing fast- and slow-path keys; the partial-order pending contract (incomparablePairtimes whose join lies beyond the frontier — pended, carried, re-windowed as a pending-only group, corrected next retire, checked on a grid oracle); and interleaved-unit isolation (which pinned theSinkbug, and is verified to fail against the bug shape). Tests that demonstrated rather than checked — including a 700-line[u8]-rows recipe backend — were pruned from the tree per volume discipline; they live in the branch history (05c48113), and the compressing-token instantiation's collision handling is a noted coverage gap for a slimmer future test.Benchmarks (
c1b99551,a36dda82; harness pruned from the final tree, recoverable from those commits)Against hand-written natives over the same batches (the floor), and against the shipping cursor tactics on identical
OrdValBatchstorage through the same cursors (the decision-relevant comparison; thecursorsmodules were public while the bench drove them, re-privatized with its pruning). 100k keys, fanout 4, release:The reduce advantage is the fast path — an optimization that was a few slice scans here and would be an intrusive rewrite in interleaved cursor navigation, which is the decoupling argument in miniature. The remaining join gap to the native floor is the bridge presentation copy (owned, consolidated, harness-checkable presentations), left as a deliberate open item.
In-dataflow validation (recorded in branch history)
An SCC example ran the proxy join inside the stock SCC dataflow (nested iteration,
Producttimes, many fuel-interleaved units) at parity withjoin_core— load 4.28s vs 4.35s, rounds ~2.67s vs ~2.71s at 100k/200k — oracle-validated for exact agreement, including under the #801 trigger shape (staggered labels, 3 workers, the regression suite's sizes). It was removed from the final tree (1bc07522,ed19240ehold it and its findings): the Corgi differential gate is the stronger version of that check, and this PR defers end-to-end validation to it.Migration notes for the #795 backends
The Corgi backends bind the pre-reshape protocol; the port is mechanical:
ProxyBridge<G, I, T, R>; backends declareGroup: Copy + Ord + 'staticandToken: Copy + Ord(join:Token0/Token1per side). Corgi's value-as-id / content-hash ids becomeGroup = u64,Token = u64verbatim.seed_timesis gone — eachReduceWindowcarries its ownseeds(novel-batch time support for its keys, sorted by group; the seeding-provenance contract is documented on the field).next_window(&mut self, instance, pending, reuse)—pendingis the harness's carried groups (must be covered, in group order, even with no novel input);reusereturns the spent window forclear()-and-refill. Progress within a retire lives on&mut self(synchronousbegin/finishbracket), as before.next_window(&mut self, instance, fresh, cursor, reuse)withtype Cursor: Defaultper-unit resumption state;crossis replaced byabsorb(&mut self, instance, sink, left, right, time, diff) -> Option<Output>+flush(&mut self, instance, sink)withtype Sink: Defaultper-unit output staging. NeitherCursornorSinkstate may live on&mut self: half-drained units interleave against the shared backend (a shared sink ships one unit's matches under another's capability — the bug class the property suite pins). Container granularity is the backend's (JOIN_CHUNKleft the harness).window.keys. A port that violates the contract fails loudly rather than corrupting.Every increment was passed through adversarial review (eight finder/verifier agents across two passes); the review's findings — including the
Sinkbug and a blind regression test — are fixed in-branch.🤖 Generated with Claude Code