diff --git a/.changeset/ordered-repair-obsolete-step.md b/.changeset/ordered-repair-obsolete-step.md new file mode 100644 index 0000000000..dabeaa4992 --- /dev/null +++ b/.changeset/ordered-repair-obsolete-step.md @@ -0,0 +1,5 @@ +--- +'@tanstack/db': patch +--- + +Start the replacement of an ordered repair before an obsolete step runs. When the source ordering changed while a repair's next page or refill was waiting, for example behind joined work, the obsolete repair issued one more request before it was replaced. diff --git a/docs/contributing/oracle-coverage.md b/docs/contributing/oracle-coverage.md index 3be2a97542..e9b3f10eec 100644 --- a/docs/contributing/oracle-coverage.md +++ b/docs/contributing/oracle-coverage.md @@ -2109,7 +2109,7 @@ generic visitor behavior outside the named collectors. | Observer hydration under terminal statuses | `packages/db/tests/live-query-observer-hydration-oracle.property.test.ts` | ARCHITECTURE.md law 16 and the glossary "crash": while a hydration seed is active, a Collection `error` or `crashed` shows in the snapshot, attached or detached, and is announced; an attached observer that sees the failure ends the seed, so cleanup then shows `cleaned-up` and live rows, not the stale failure or the seed. Decision (not a law-16 claim): `cleaned-up` and restart under an active seed keep the seed as `ready`, because cleanup is not a failure and the next sync run's readiness hands off. After the seed ends (readiness or a failure), cleanup and restart show the live Collection: `cleaned-up` with no rows, then every row the new sync run writes or reacquires, including a row equal to one shown before cleanup. That restart claim adds no rule: its authority is the header's law 2 (an observer whose seed ended behaves like one without a seed and shows the live Collection) with the glossary's "cleanup" (it ends the sync run; the Collection remains available for restart) and "crash" (cleanup discards all state, so a later start is a fresh start); the ARCHITECTURE sentence on the observer's subscription documents the mechanism, not the authority. The `live-query-observer.hydration-terminal` property (`oracleProperty`, in the path-replay registry) generates histories of up to 10 steps that cross both modes, an eager or an on-demand source (whose loader re-delivers the provider's rows, which survive cleanup), a seed of 0..3 rows or none (an observer without a DbClient, the reference case of law 2), attach order, live writes, `markReady()`, `fail()`, `crash()`, cleanup, and restart. Its 13 declared states are model states (a status while the seed is active, attached or detached; attach to a failure; cleanup after a failure ended the seed; restart under the seed; a row from before cleanup back after restart once the seed ended; the same through an unseeded granular observer's own on-demand subset demand). Eleven constructed histories enter them, so every fixed and random campaign reaches every state, and half of each grammar's histories start with a constructed history; each grammar prints its reach counts. Fixed histories replay the crash, fail-then-cleanup, and crash-before-attach traces and the two restart-rewrite traces in both modes and against both source kinds, and the restart-rewrite traces also without a seed. The check judges laws `view` (status, flags, claimed rows) and `announcement` (last-read snapshot, granular rebuilt rows). The migration from the hand-built campaign kept every mutant kill and every gap-report outcome on `src/live-query-observer.ts` (seed 42); the old prefixed histories ran up to 13 steps. Limits: rows under a failure status are not claimed; the source is a plain controlled Collection, not a live-query graph; on-demand loads settle at once, with no predicate, window, or pending load across cleanup; streamed client errors, handoff timing, and framework adapters stay with the focused observer and adapter tests. Closed cleanup/restart witness [#2334](https://github.com/TanStack/db/issues/2334) (also the random campaign's seed 1779366423, path 30:6:8:8:8:8): attach; ready; write `a=1`; cleanup; restart; write `a=1` again. The observer reset its rows at `cleaned-up`, but its Collection subscription kept them as its last publication (ARCHITECTURE "Cleanup, restart, and detached waiters"), so it dropped the equal rewrite as already shown; an on-demand restart's replay and sent-key filter dropped reacquired rows the same way. The observer's subscription now discards its published rows and sent keys at cleanup (`discardsRowsOnCleanup`). RED on `a17c8e468`: 19 of 38 tests fail with law `view`, rows [] where the model owes the row, also at a ready checkpoint when only ready checkpoints are judged. Mutants that drop the option, take the stale copy before the discard, discard only in granular mode, keep the sent keys, or keep the published rows each fail; an observer that keeps rows under `cleaned-up` fails at the cleanup checkpoint. The fix's production half is in `CollectionSubscription.handleCollectionCleanup`, so the oracle's owns name it (the gap report follows only `#function` entries into other files, and no Collection subscription owner subscribes with the option). Gap-report limit: on `@tanstack/oracles` b937148 the gap report refuses to run on `src/collection/subscription.ts`: its statement-deletion mutant rewrites the constructor's `super()` as `m(n) \|\| super()`, which breaks a derived class with parameter properties (`ReferenceError: Must call super constructor`), so every oracle that builds a subscription fails with no mutant active. Until TanStack/oracles fixes it, the hydration oracle's kills there are shown by direct runs: the authored mutants above and operator mutant M92 (`if-false` on the option) fail it with law `view`; M91 (`if-true`, every subscriber discards) and M88 (`if-true` on `!reload`) survive it, as they change only direct subscribers and reloads, which this grammar does not draw. | | Query DB SSR dehydration | `packages/query-db-collection/tests/ssr-dehydration-oracle.test.ts`, [review record](oracle-reviews/issue-1950-ssr-dehydration.md) | A plain Query cache control, a live on-demand compound predicate, a signal-only request, and an ordered cursor with a custom comparator all retain their row through QueryClient dehydration, reconstruction of Seroval's emitted stream payload, and Query Core hydration from that payload. The on-demand query functions still receive the original IR, comparator, and signal; serialized metadata retains enumerable user metadata but excludes request options. The original implementation fails the compound and signal cases at the stream checkpoint. A serializable stream-only request-options leak passes the former chunk-count check but fails the current payload assertion. This owner covers successful Query cache entries at the installed Query Core 5.90.20 and Seroval 1.5.0 versions. A TanStack Start integration owner still needs the reporter's Router 1.171.33 and Seroval 1.6.8 path, browser Collection resume/refetch, and request cancellation across SSR. Query subset and pagination oracles remain owners of predicate/order/cursor meaning and supported value types. The issue's `shouldDehydrateQuery` workaround replaces Query Core's success-only default and admits pending/error queries; any documented workaround must preserve that default filter. | | Query DB ordered refetch | `packages/query-db-collection/tests/refetch-ordered-prefix-oracle.test.ts` | Issue #2136: after preload, and after `utils.refetch()` or a Query invalidation settles, an on-demand Query Collection behind a LEFT-joined, ordered, limited live query must show the window over the current backend rows. The design under test: query-db reports `invalidateLoadedSubsets()` when an ordered page ends earlier in the order than before, including when its keys stay the same, or when its keys change and it has a later page. Each ordered loader runs its bounded prefix repair. A persisting optimistic update or delete can hide the visible order change that otherwise starts repair. The `query-db.refetch-held-page-end` property constructs that same-key earlier-end overlap through the real QueryClient and core receiver, with 24 fixed and 24 random histories (reach minimum 24 each), numeric finite cursor pages, static/function keys, one/two order terms, limits 1–3, offsets 0–1, varied row IDs, and explicit refetch/Query invalidation. Each history requires the same-key earlier end on the deleted held boundary, a fresh gap between the two answers, a delivered report, and a subsequent real core repair acquisition. Forty-eight structural histories cross widths/offsets with delete/update/unrelated-delete/no hold and earlier/later ends. Six delete-gap width/offset states each require structural reach. Label-only edits are negative report controls. The [nine-item review](oracle-reviews/2026-11-02-query-refetch-nine-item-review.md) records the strengthened classifier, experiments, portable commands, and finite limits. The exact failing CI history replays the shared model and comparison. Both the original implementation and the restored equal-key guard fail the public source-prefix comparison after release. See [the held-page-end review](oracle-reviews/2026-11-02-query-refetch-held-page-end.md) for exact source bindings, evidence, and limits. Its model is a pure top-k of marked backend rows. A fixed and a random campaign generate rounds of marker flips (which serve continuation pages), backend changes while the provider lags, a second live query (`observe`) whose own demand can load a page's new row first, optional Query invalidation with further changes, and a refetch, across one or two order terms, a numeric or locale-collated string order, limits 1–3, offsets 0–1, and a static or function Query key. With an unchanged backend, a repeated refetch must serve no more rows, start at most one first-page request, and report nothing. A refetch or invalidation must never start a new full-source request. A coverage law runs at the same checkpoints: every backend row from the start of the order through the window's last row (every row, when the window is short) must be in the source Collection with its current values, so a latent gap fails before a marker exposes it; a named fixed history of the issue trace with the moved row unmarked passes the window law and fails only the coverage law when Query DB never reports. The grammar can hold an optimistic update across a refetch, with the checkpoint moved to its release, and a premise-directed campaign under a hold (other rows observed, a row moved ahead of the page's end, a new row further ahead, a write to the last-sorting observed row) requires a report during a hold in every case and fails a skip that reads rows held back behind the transaction; the general campaigns did not. The general grammar holds optimistic deletes as well as updates. The generated campaigns declare reach (minimum 3) for a lagging refetch after a continuation, one during a hold, and a refetch that reported while the window was full, where the loader decides between ignoring the report and repairing. A named fixed history of a refetch during a held delete left the window short after release, also with this PR's report and overlap changes reverted, until the fix that resumes a continuation after a synchronous answer; no window is checked during a hold, where #2148 and #2169 remain open. Reports (`loadedSubsets:invalidated`) are bounded: a step reports at most once, and only when an ordered reanswer changes key membership or moves its end earlier, so unrelated value changes do not justify reports; named fixed histories require no report when a one-page window, or a window's last page, only loses a row, and a sync-boundary replay requires a report when a page ending on a row without an order value has its end move earlier (on the earlier gate, which read that page as empty, it reported nothing), and another requires a report when the provider returns a one-page window's rows in reverse order (the earlier gate took the last array row as the page's end). When a page's end moves earlier, Query DB reports. A loader whose window lies inside its own first page skips the repair only while its page read past the window or it read the tie of the current end; after an insert into a top-N list moves the end, a named fixed history requires the loader to prove the window again with bounded reads, no full-source read, and an unchanged Query count. A filtered one-page window whose page end moves past an unseen row must still repair (found by the random campaign; a loader that always skips fails it, the f9 tie replay, and the ordered-work oracle's signalling replays). The skip also refuses while the source holds accepted sync rows back: a replay refetches while an optimistic update persists, so the report arrives before the refetched rows are visible, and a skip that reads those older rows fails it. The ordered loader state oracle checks that a prefix read issued before an ordering invalidation, which settles after the bounded repair, does not retire the repair's prefix; the repair-first order failed before that fix. A `loadSubset` call that acquires a released, invalidated page can report, because Query then refetches that page on its own. A failed repair shows only the last window or the right one. Named replays cover the issue trace after a refetch and after an invalidation, with a page-capping provider, with another live query loading the page's new row first, with an empty later page, with a page whose end moves earlier while a tie request holds its old last row, a second refetch after an invalidation, a repair failure, and a provider that honors neither cursor nor offset. Never signalling, the old overlap-to-full-source rule, ignoring empty later pages, reporting on any page change, removing the repair loop guard, and reporting once per page each fail it by assertion. A replay makes a page's application fail and checks the window shows its last result or the right one, then the next refetch restores it; recording a page before its rows are accepted cannot be distinguished, because the failed attempt reports on its own. Open: the report laws bound reports but do not require each one; a page whose end moves earlier reports even with unique order values, where no row can be missing; it does not check whether a repair waits for in-flight work; the generated campaigns use an uncapped cursor provider only (an offset-only provider and a page-capping provider each hit a loader defect that reproduces on main: #2182, #2183); the generated campaigns do not check the window after a marker flip (a named fixed history checks the trace where the loader stopped refilling after a joined-side removal, which the repair-retirement fix below closed); a failed repair still recovers through the loader's full-source retry; interval, focus, and reconnect refetches share the invalidation path but are not driven; NaN order values have no executable witness; overlapping `refetch: true` acquisitions on one Query hash are counted, so the first to finish does not clear the loop guard for the other, but no witness separates that from a plain set; a Query refetch that joins a running `refetch: true` acquisition on the same hash does not report, and no witness reaches it (#2185); follower tabs of a multi-tab persisted collection never receive the report (#2174). The offset-only and page-capping loader defects have `it.fails` witnesses in the oracle. A finished bounded repair used to discard its boundary when its retirement made Query DB remove a row the loader had sent; the loader then restarted paging with a smaller first page that could not retire the repair's prefix, so every later refetch read both. A named fixed history found by the random campaign (at four times the run count) and an ordered loader state witness fail on that, and the fix also closed the joined-side refill defect. At four times the run count, the random campaign found a short window that stopped paging before the last row of the order: a report's repair released continuation Queries, and Query DB answered their reacquisition synchronously from its cache, so the graph turn inside each request asked for more while the loader was still requesting and nothing resumed the staged continuation. Only the coverage law failed. A named fixed history and an ordered loader state witness (a synchronous answer whose writes the graph already processed must continue the chain) fail on that, and pass with the fix. The loader side of the report also has a second owner: the ordered-work oracle's `refetch-signal` provider re-runs each served request alone and reports when any answer changed, across that oracle's generated plans, and a signalling refetch must start no full-source request unless a bounded page in that step ended on a null or NaN rank, which takes the documented full-source fallback (a random seed found that case). Never signalling and the old overlap-to-full-source rule each fail it. It excludes a peer live query, which can keep a short window after a refetch (#2155). The persisted-collection oracle checks that a source's report reaches the Collection through the managed cache-generation wrapper and that a retired source session's report is dropped. Remaining work for this class is tracked in #2186. | -| Ordered acquisition | [pagination](https://github.com/TanStack/db/blob/main/packages/db/tests/query/pagination-oracle.property.test.ts), [ordered work](https://github.com/TanStack/db/blob/main/packages/db/tests/query/ordered-work-oracle.property.test.ts), [ordered lifecycle](https://github.com/TanStack/db/blob/main/packages/db/tests/query/ordered-lifecycle-oracle.property.test.ts), [ordered loader state](https://github.com/TanStack/db/blob/main/packages/db/tests/query/ordered-source-loader-state-oracle.test.ts), [graph scheduler](https://github.com/TanStack/db/blob/main/packages/db/tests/query/scheduler.test.ts), [issue #1880 ordered-repair review](oracle-reviews/issue-1880-ordered-repair.md), [issue #1882 custom local collation review](oracle-reviews/issue-1882-custom-local-collation.md), [issue #1898 relation-filter review](oracle-reviews/issue-1898-relation-filter.md), [PR #1909 external review](oracle-reviews/pr-1909-external-review.md), [eager ordered-window repair review](oracle-reviews/perf-ordered-window-repair.md), [reversed index reads](https://github.com/TanStack/db/blob/main/packages/db/tests/reverse-index-oracle.property.test.ts) | Complete finite provider results, inherited locale and bounded/unbounded custom collation with exact request options, query-level inheritance across source aliases, real lexical/numeric disagreement, custom comparator ties, scan/index paths, pending windows, ties/nulls, lease ownership, Effect callback gates, including an indexed source update during Effect startup, and documented repair timing. Direct LEFT-joined filters cover local finite prefixes, pending child demand, child removal, and anti-join publication with custom full-source and unindexed fallback loading; unrelated include demand cannot stall the root continuation, and an empty joined replay wakes held Effect callbacks; remote relation hints remain outside this owner. Graph scheduler checks coalescing, dependency order, synchronous loader input, and repeated-alias failure ownership. The ordered-work oracle checks that a synchronous root refill reaches D2 before joined publication; a mutant that omitted the post-loader graph step failed at the second child demand. Custom collation proves local full-source acquisition only; it does not establish provider cursor capability or backend collation fidelity. Sibling-source input during a synchronous ordered continuation returns to graph work before another ordered acquisition. Request completion is not proof of unrequested source extent. A window move during existing joined demand waits for its root continuation, including an independently held root request; current demand failure rejects the move, while retirement and an obsolete rejection do not. A bounded ordered repair resumes its refill after joined demand settles. The ordered-source-loader state test checks that an explicit failed-request retry blocked by joined demand retains its generation until it can issue a request. Multiple simultaneously pending joined plans during a window move and a public-query failed-retry overlap still need dedicated witnesses. The ordered-work oracle also checks an eager indexed window over generated upserts and deletes: the rows equal the filtered, sorted model, and each change delivers a bounded number of source rows; an unbounded or always-full repair read fails it. Its filter dimension adds a function filter and a LEFT-joined filter, and a campaign fixed to the joined premise checks that a window refilled past a distant row the query already received holds the first eligible rows. Joined filters also run as anti-joins, change eligibility through the marker or the root row's join key, and drive an Effect beside the Collection. A full-join filter keeps every root row and adds a null-ranked rootless row for each marker no root row matches; on main a bounded root prefix showed markers whose root rows were not yet loaded as unmatched rows, and restoring the old inner-or-right full-source rule fails eight tests. Null placement is a generated dimension, with the index built to match, and a query that ignores it fails six tests. A full-join campaign has few or no filler rows, a matched null-ranked root row and at least one orphan marker in every case, so its windows reach the null group where rootless rows and null-ranked root rows tie; a reconstruction check samples exactly the cases its fixed-seed run executes and requires such windows (19 rootless and 7 mixed null-group windows of 40 at one times the run count), and the Effect runs beside the Collection. Full joins read their full source, so only the rows law covers them; paging them under the old join rule fails the window law. Fixed cases cover a null-ranked root row past a prefix that ends in the null group. Paging a nulls-last full join passed this oracle but was not adopted: it cost more per delete when the window reached the null group, which no work law here measures, and #2130 tracks full-join paging. Joined filters can match a row through several markers, and the model keeps one result row per matched pair; a model that collapses them fails. The eager harness also runs an on-demand source whose provider follows the LoadSubsetOptions contract (offset only without a cursor, the applied receipt returned). Its test provider combines a sync adapter and its provider (glossary model alignment rule 2); a held request is a physical acquisition whose provider answer is delayed, a served range is the prefix and boundary one answer establishes (a model abstraction), and the peer is a second live-query Collection. The provider sorts by the requested order and keeps its own ledger of sent rows. A forwarding provider sends live changes only for rows it sent or rows that match a served subset, and its served rows obey the work bound; a loader that asks for 100 extra rows fails it. A refetching provider, like query-db-collection, sends nothing until a refetch. The refetch keeps every served ordered range whole, as the LoadSubset contract requires: it sends every row from the start of the order through the last order value a limited page returned, and rows in no range leave; the rows law over the model applies once no change is pending. After every step on either provider, the Collection must hold exactly the rows in the provider's ledger, and the query and the Effect must show their window over those rows; a mutant that drops marker removals fails this law at steps 0 and 1 of the fixed refetching campaigns, earlier than the model's rows law, and in one more campaign. A holding provider answers each load only at an `answer` step, from the rows at that moment, so live changes arrive while loads are in flight. While a load is in flight, the query and its peer either keep the window they showed at the previous checkpoint or show distinct ledger rows that pass the query, in its order; the Effect is not checked then. That is weaker than the architecture's barrier rule, under which a repair or window move keeps the last public snapshot until it settles: a barrier law fails today on on-demand joined plans, where a visible-delete repair and a held `setWindow` publish before they settle (#2131; the law and traces are kept for that fix). The provider records a request as served only once it answers it, and an abort (or an adapter unload) of a held request follows `LoadSubsetOptions.signal`: a cooperative provider installs none of its rows and its load fulfills at once, while a provider that cannot cancel in-flight work (`late` cancellation, generated) answers it anyway and its load fulfills after those rows become visible. A `release-peer` step cleans up the peer while its loads are held, which aborts them; each request counts once although its acquisition release both aborts and unloads it. The fixed held campaign reaches 5 aborted held requests and 1 late answer, and its reconstruction check requires at least 3 cooperative cancellations and 1 late answer. A held load rejects when its applied receipt rejects, and the step then fails, because no signal or cleanup rejects a receipt in these histories; that branch is unwitnessed. The held campaign fixes a forwarding provider, so `release-peer` never reaches a refetching provider; that branch is unwitnessed. A request whose signal is already aborted when the provider receives it is never reached; that branch is unwitnessed. The held campaign uses a forwarding provider and an indexed source filter or a joined filter, deletes three visible rows and then upserts an eligible row with an id no other command uses; its reconstruction check runs in the same test as the fixed-seed campaign and reads its per-case counts: 35 of 40 cases issue a held request, and every one of them changes rows while it is in flight. Loading must reach a fixed point: past a request budget the provider rejects and records it, and the initial load, every step and the end of each history assert the record is clear (a loader that re-requests a prefix it already holds can loop without reaching the provider, which this cannot see). A bounded step makes at most four provider requests, and each consumer's initial proven-prefix load is bounded separately, in total transfers (a repeated request for the same prefix counts) and in distinct rows (at most the source's size); a loader that asks for 100 extra rows on every page fails that bound and the initial-load work law. Loader mutants that never resume after a boundary request, or that ignore a load request while another load is pending, fail it; a mutant that drops a window move blocked behind a pending load still survives, even with the settlement check on held moves; whether it is equivalent is open. Open (#2148): on an on-demand source with a joined or anti-joined filter, an optimistic delete of the visible row leaves the window short until the delete persists, because the next row is never loaded. On an on-demand source with a source filter, and on an eager source with any filter, the same delete refills the window correctly; these are the contrast cases. Owner: this oracle. Needed witness: the optimistic-delete dimension (kept as a patch for #2148) in the grammar, plus a fixed histories of the anti-join trace. A refetch that re-runs each page alone, as query-db-collection does today, leaves a row that moved between two pages unloaded; random seeds found that trace, a named fixed history fails on it, and a query-db receiving witness reproduces it (#2136 tracks the provider fix). An Electric-style provider, which skips updates to rows it never sent, is not modeled; a mocked-stream witness shows a row moving into a served ordered range never arriving under the default replica mode (#2138). At one times the run count, the campaigns reach 87 refetch steps: 39 change the window, 6 remove a visible row, and 13 lead to a further provider request. A random seed found a refetch that empties a joined window, after which the loader refills it over several page requests and publishes `[]`, one row, then the final rows; a named fixed history keeps that trace for #2131. No incorrect final window has appeared on that path, and no loader mutant tried so far is caught only by it; the work law does not cover it. For an on-demand joined or anti-joined filter, the initial load must not request the whole source when the first window's worth of source rows in query order all pass the join and no boundary value is null or NaN; 35 executed cases meet that premise, and a compiler that reads the whole source for every joined filter fails eight tests on this law alone. The rows served by that initial load stay within the prefix, its boundary ties and a refill, for each consumer. Later steps of those plans have no work bound. An unindexed join filter over it left the window empty on main, until the plan counted the rows it still needs; restoring the old guard fails the campaigns and a fixed histories. A step that changes the visible rows must publish, and its subscriber starts with every visible key, so a removal-only change reaches it; mutants that drop update-only or removal-only publications fail. A step may publish one intermediate window per provider request it made, and only its last publication must show the final window, because a repair or refill can publish after each round trip (#2131); the content of those intermediate windows is unchecked. The model keeps its own copy of the markers, and full-join histories can insert the root rows of orphan markers. A premise-directed campaign inserts a fresh row and then changes an initial row's eligibility alone, so the row leaves the window only through the join; it and a named fixed history fail when a window row past the loader's settled boundary counts toward a full window. One case in four adds a second live query over the same sources with a larger window, and its rows law holds at every checkpoint; the work laws do not apply to those cases. #2155: a second live-query Collection over a refetching on-demand provider kept a short joined window after a refetch removed a tied row (the peer showed ranks `[0, 0]` where the model shows `[0, 0, 100]`). The loader fix that resumes a staged continuation after a synchronous answer the graph already processed closed that trace. The fixed histories of that indexed trace now expects the right window. Still open: an unindexed peer over a refetching provider keeps a short joined window (the peer shows `[100]` where the model shows `[100, 101]`), which also fails without that fix; each campaign therefore still excludes the peer and refetching pairing, as its last map. Owner: this oracle. Needed witness: a fixed histories of the unindexed trace flipped to pass, and the pairing restored to the grammar. Limits: Effects are checked for rows after each step, not for publication counts or positions. Histories move the first query's window with `setWindow` (150 moves at one times the run count, 56 on demand), and its rows law and ledger law then follow the moved window; the Effect and the peer keep theirs. On a holding provider every window-move promise must have fulfilled after the final drain. A refetching provider models query-db's unload: it drops the unloaded request and removes rows that no remaining request's last answer holds. The per-step work law applies only to forwarding, immediate, single-consumer cases: it skips refetching, holding and peer cases and move steps; a two-term indexed move scanned the source four times, which no law here bounds. Multi-term joined plans stay outside this harness, on both paths; on the on-demand path, the provider's transfer is bounded only for indexed single-term source-predicate plans. Joined windows compare order values, so a wrong row tied with the expected one passes; a window row tied with the boundary counts as proven before its tie request settles, which no witness exercises. A boundary that cannot advance past a window row would repeat one page per new key; reading the boundary's range locally should always reach that row, but no witness shows it. Joined ties are compared as any valid first rows; whether source-filter ties may be fixed to the source key is open. The same grammar includes NaN and null ranks and a second-order term, and bounds both rows read and rows delivered, including the initial load and index refills; a scan law limits each change to one pass over the source. A fixed case checks that an indexed descending window places nulls first, and a lifecycle witness checks that an eager full-source window is ready with its rows at creation when its source answers synchronously. The initial fallback cells check indexed and unindexed locale strings with distinct and tied values, plus a null boundary after a warm ordered request. The warm null-boundary case crosses preload-started and constructor-started live-query sync runs: the former completes at the synchronous cut, while the latter resumes deferred on-demand acquisition asynchronously and publishes after settlement. They require an unfiltered full-source request, no public row at fallback entry, and the expected row and status at the immediate readiness check. A Promise fallback stays loading at that checkpoint. A React receiving witness checks an eager locale-string `findOne()` at the first layout commit. A Query DB receiving witness checks warm cached subsets: both raw adapter calls return literal `true` with the source rows visible at each return, and the live query is immediately ready without a fetch. The same fallback cells observe subscriber changes from before the first source write: literal-true and Promise fallbacks each publish one nonempty final-window insert after the fallback settles, and the callback sees the complete row. Promise cells show no nonempty event at the immediate cut; a duplicate-event fault fails all eight cells. Other adapters and a real on-demand React first commit remain unwitnessed. Full-source work after initial publication and repair remain outside this synchronous guarantee. A separate post-publication oracle crosses marker deletion and retargeting with literal, Promise, and held-applied-receipt fallback responses. It also settles the child demand before holding the receipt, so the public live-query loading flag isolates the root fallback. The model checks final rows and net events, while event replay checks every callback snapshot; a retained or empty intermediate window is allowed. A loader fault that ignores the pending receipt fails at the held loading-flag check. Two literal-true cleanup-failure histories require that the replacement still publishes and the adapter error reaches the public query status without making the unrelated marker commit throw; the provider's applied receipts are recorded and compared outside provider callbacks. The Promise case checks eventual coherence on an asynchronous callback path, without claiming a separate timing cut. Four held-Promise histories apply fallback writes, change another join marker before provider settlement, and compare each callback and the final winner; an injected stale extra publication fails the event comparison. Other marker actions and overlapping root-source changes remain open; the provider has no later write or rejection, so this schedule does not establish when the loader claims full-source authority. The reversed-index oracle checks every reversed read's order and filter work for both null placements. The retirement-invalidation grammar (`ordered-loader.retirement-invalidation`) composes a constructive invalidation prefix, up to four settled answers that let the repair chain complete, and generated command suffixes with index availability, limit 1/2, joined deferral, needed rows, release errors, reentrant truncate and disposal, reentrant ordinary passes, retry timers, offset 0/1, and full-source plans. Its declared `completed-repair-release` reach counts only an invalidating release observed while a successful repair-chain answer settles and issues no further chain step; an instrumented run matched the production retirement path in 66 of 72 such histories, and the rest owed nothing more after a late disposal or full coverage; an ablation that invalidates only on other releases passes the older `release-invalidation` reach and fails this one. Only an on-demand source answers a release with an adapter unload, so neither this grammar nor the broad `ordered-loader.request-authority` arbitrary pairs `releaseInvalidates` with a synchronous repair answer, which reads an eager source whose releases bypass the adapter (`CollectionSyncManager.unloadSubset`). The broad arbitrary weights `releaseInvalidates` 5:1 like the other release reactions, because an invalidating release leaves the quiet report laws. The directed grammar also places the invalidation after the callback's disposal, reentrant pass, and truncate (`late-release-invalidation`). Broad overlap states require 20 histories each, and the rarer full-source-plan overlap requires 5. An invalidating unload also writes graph input, so the driver's drain runs one more loader pass before it judges progress, as the live-query Collection and Effect graph loops do; without that pass, a repair that finishes inside a loader pass after joined work clears was misjudged as owing no further read. Its independent request ledger records issue and invalidation events on one clock. It requires an authoritative start after the callback's invalidation for a live finite repair after retry/drain; complete full-source coverage absorbs invalidation, cursor reset transfers pre-reset work to replay, disposal ends ownership, and unanswered authoritative work retains its existing no-timeout limit. Each normal broad campaign measures callback overlap with release error, truncate, disposal, pass reentry, offset one, timer-enabled scenarios, full-source plans, and multiple successor chains. A separate `ordered-loader.retirement-receiver` property runs real live-query Collection and Effect consumers, and a live-query Collection whose `setWindow` to the other offset starts in the same turn as the ordering write. It varies indexed/unindexed sources, limit 1/2, offset 0/1, literal/Promise adapter answers, a held newer replacement answer, and the unload's change: moving the repaired prefix, deleting its rows before the boundary, deleting the boundary row, or deleting a prefix row that ties with it, each of which owes a replacement, or evicting a sent row past the repair's boundary, including a row that ties with the boundary but lies outside the prefix, which keeps that boundary and starts no read. A tie row sorts before or after the boundary row by key, as live-query Collections order ties. A same-turn window move may repair either window's prefix, so that kind keeps only the move and row 1's eviction; prefix deletes and ties run on the other kinds. Each consumer has separate declared adapter-unload and held-answer reach, and delete, boundary-row delete, tie delete, tie eviction, and eviction unloads have their own reach; each grammar runs 600 histories. A loader that skipped every retirement-time delete fails the delete histories at the progress relation, one that treated every sent-row delete as new information fails the eviction histories, one that treated every boundary tie as eviction fails the boundary-row and tie deletes, one that treated every boundary tie as new information fails the tie evictions, and one that kept only the boundary row's key fails the tie deletes. The loader keeps the keys of the settled prefix rows that tie with its boundary row. The focused `keeps a repair's boundary when its retirement removes a row the loader sent` test remains as a supplemental example. An instrumented run placed every invalidating receiver unload inside retirement (200 of 200 per campaign). Following Atomic window publication, the window move stays pending while the replacement is held and settles with its chosen window visible; a mutant whose subset loads stop joining the active window operation fails only those move comparisons. Held-answer reach is recorded only after the provider answer is blocked and the prior-window and no-publication comparisons pass. The provider moves its repaired prefix behind a still-uninstalled row during unload and supplies no later external graph input. The shared progress relation checks that an authoritative start follows the invalidation and precedes the first replacement publication. Independent full-provider sorting checks final rows; held answers retain the previous complete public window and publish no callbacks, and completion publishes one complete replacement. Fixed replay witnesses force the held-answer premise for each consumer. An executed public-method call probe observed reentrant `loadMore` inside every sampled unload for both consumers, with no production-state reads. Original debt-clearing and deliberately delayed-one-pass mutants fail the progress/publication judgments; start observations before the invalidation or at publication fail calibration. This evidence does not require recursive synchronous dispatch: deferred replacement remains legal while the public gate holds. The replay-continuation grammar (`ordered-loader.replay-continuation`) follows ARCHITECTURE.md, Ordered requests/continuation/recovery: a pre-reset request belongs to truncate replay and cannot revive its discarded cursor; a graph continuation survives bookkeeping until a graph pass consumes it or cursor reset discards it. `continuationOwed` is model-only classification provenance, not product completion state. The unchanged handoff/reset grammar and exact shared-model replay reject consuming that provenance during replay bookkeeping. This is a harness correction; it supplies no production resource-leak claim. Its `deferred-refill` state is reached only when a synchronous repair answer meets a release-triggered truncate (6 of 96 inputs). An eager source's release never reaches the adapter (`CollectionSubscription.createSubsetAcquisitionRecord`), so production cannot produce that pairing, and the grammar calibrates continuation provenance without a production-reach claim. The broad request-authority arbitrary pairs synchronous repair answers with release faults, truncates, disposals, and reentrant passes in the same over-approximating way; those histories pass and support no production-reach claim either. The random handoff campaign runs 400 histories so that state stays above its minimum. Limits: the real receiver uses distinct finite numeric ranks, ascending root order, one source and consumer, one qualifying callback invalidation, no failure/truncate/disposal inside the real unload callback, one window move per history and no failed replacement under a move, and no provider-specific network. Its on-demand source settles every repair answer asynchronously in the loader, even a literal adapter answer; the loader's synchronous repair settlement needs an eager source, which has no adapter unload to invalidate. The controlled grammar measures the combined lifecycle cases; it does not transfer all such combinations across the public receiver boundary. No claim about obsolete later cursor-demand retirement (#2223) or arbitrary callback composition follows. Existing run budgets remain unchanged. Random samples do not establish bounded exhaustiveness. The controlled and receiving grammars have distinct registered replay properties, so each seed and shrink path selects only its own driver. The no-leak calibration supplies a retained-lease observation to the same request-ledger comparison after an unmodified run of the same covering-repair history; it reads no private member names. | +| Ordered acquisition | [pagination](https://github.com/TanStack/db/blob/main/packages/db/tests/query/pagination-oracle.property.test.ts), [ordered work](https://github.com/TanStack/db/blob/main/packages/db/tests/query/ordered-work-oracle.property.test.ts), [ordered lifecycle](https://github.com/TanStack/db/blob/main/packages/db/tests/query/ordered-lifecycle-oracle.property.test.ts), [ordered loader state](https://github.com/TanStack/db/blob/main/packages/db/tests/query/ordered-source-loader-state-oracle.test.ts), [graph scheduler](https://github.com/TanStack/db/blob/main/packages/db/tests/query/scheduler.test.ts), [issue #1880 ordered-repair review](oracle-reviews/issue-1880-ordered-repair.md), [issue #1882 custom local collation review](oracle-reviews/issue-1882-custom-local-collation.md), [issue #1898 relation-filter review](oracle-reviews/issue-1898-relation-filter.md), [PR #1909 external review](oracle-reviews/pr-1909-external-review.md), [eager ordered-window repair review](oracle-reviews/perf-ordered-window-repair.md), [reversed index reads](https://github.com/TanStack/db/blob/main/packages/db/tests/reverse-index-oracle.property.test.ts) | Complete finite provider results, inherited locale and bounded/unbounded custom collation with exact request options, query-level inheritance across source aliases, real lexical/numeric disagreement, custom comparator ties, scan/index paths, pending windows, ties/nulls, lease ownership, Effect callback gates, including an indexed source update during Effect startup, and documented repair timing. Direct LEFT-joined filters cover local finite prefixes, pending child demand, child removal, and anti-join publication with custom full-source and unindexed fallback loading; unrelated include demand cannot stall the root continuation, and an empty joined replay wakes held Effect callbacks; remote relation hints remain outside this owner. Graph scheduler checks coalescing, dependency order, synchronous loader input, and repeated-alias failure ownership. The ordered-work oracle checks that a synchronous root refill reaches D2 before joined publication; a mutant that omitted the post-loader graph step failed at the second child demand. Custom collation proves local full-source acquisition only; it does not establish provider cursor capability or backend collation fidelity. Sibling-source input during a synchronous ordered continuation returns to graph work before another ordered acquisition. Request completion is not proof of unrequested source extent. A window move during existing joined demand waits for its root continuation, including an independently held root request; current demand failure rejects the move, while retirement and an obsolete rejection do not. A bounded ordered repair resumes its refill after joined demand settles. The ordered-source-loader state test checks that an explicit failed-request retry blocked by joined demand retains its generation until it can issue a request. Multiple simultaneously pending joined plans during a window move and a public-query failed-retry overlap still need dedicated witnesses. The ordered-work oracle also checks an eager indexed window over generated upserts and deletes: the rows equal the filtered, sorted model, and each change delivers a bounded number of source rows; an unbounded or always-full repair read fails it. Its filter dimension adds a function filter and a LEFT-joined filter, and a campaign fixed to the joined premise checks that a window refilled past a distant row the query already received holds the first eligible rows. Joined filters also run as anti-joins, change eligibility through the marker or the root row's join key, and drive an Effect beside the Collection. A full-join filter keeps every root row and adds a null-ranked rootless row for each marker no root row matches; on main a bounded root prefix showed markers whose root rows were not yet loaded as unmatched rows, and restoring the old inner-or-right full-source rule fails eight tests. Null placement is a generated dimension, with the index built to match, and a query that ignores it fails six tests. A full-join campaign has few or no filler rows, a matched null-ranked root row and at least one orphan marker in every case, so its windows reach the null group where rootless rows and null-ranked root rows tie; a reconstruction check samples exactly the cases its fixed-seed run executes and requires such windows (19 rootless and 7 mixed null-group windows of 40 at one times the run count), and the Effect runs beside the Collection. Full joins read their full source, so only the rows law covers them; paging them under the old join rule fails the window law. Fixed cases cover a null-ranked root row past a prefix that ends in the null group. Paging a nulls-last full join passed this oracle but was not adopted: it cost more per delete when the window reached the null group, which no work law here measures, and #2130 tracks full-join paging. Joined filters can match a row through several markers, and the model keeps one result row per matched pair; a model that collapses them fails. The eager harness also runs an on-demand source whose provider follows the LoadSubsetOptions contract (offset only without a cursor, the applied receipt returned). Its test provider combines a sync adapter and its provider (glossary model alignment rule 2); a held request is a physical acquisition whose provider answer is delayed, a served range is the prefix and boundary one answer establishes (a model abstraction), and the peer is a second live-query Collection. The provider sorts by the requested order and keeps its own ledger of sent rows. A forwarding provider sends live changes only for rows it sent or rows that match a served subset, and its served rows obey the work bound; a loader that asks for 100 extra rows fails it. A refetching provider, like query-db-collection, sends nothing until a refetch. The refetch keeps every served ordered range whole, as the LoadSubset contract requires: it sends every row from the start of the order through the last order value a limited page returned, and rows in no range leave; the rows law over the model applies once no change is pending. After every step on either provider, the Collection must hold exactly the rows in the provider's ledger, and the query and the Effect must show their window over those rows; a mutant that drops marker removals fails this law at steps 0 and 1 of the fixed refetching campaigns, earlier than the model's rows law, and in one more campaign. A holding provider answers each load only at an `answer` step, from the rows at that moment, so live changes arrive while loads are in flight. While a load is in flight, the query and its peer either keep the window they showed at the previous checkpoint or show distinct ledger rows that pass the query, in its order; the Effect is not checked then. That is weaker than the architecture's barrier rule, under which a repair or window move keeps the last public snapshot until it settles: a barrier law fails today on on-demand joined plans, where a visible-delete repair and a held `setWindow` publish before they settle (#2131; the law and traces are kept for that fix). The provider records a request as served only once it answers it, and an abort (or an adapter unload) of a held request follows `LoadSubsetOptions.signal`: a cooperative provider installs none of its rows and its load fulfills at once, while a provider that cannot cancel in-flight work (`late` cancellation, generated) answers it anyway and its load fulfills after those rows become visible. A `release-peer` step cleans up the peer while its loads are held, which aborts them; each request counts once although its acquisition release both aborts and unloads it. The fixed held campaign reaches 5 aborted held requests and 1 late answer, and its reconstruction check requires at least 3 cooperative cancellations and 1 late answer. A held load rejects when its applied receipt rejects, and the step then fails, because no signal or cleanup rejects a receipt in these histories; that branch is unwitnessed. The held campaign fixes a forwarding provider, so `release-peer` never reaches a refetching provider; that branch is unwitnessed. A request whose signal is already aborted when the provider receives it is never reached; that branch is unwitnessed. The held campaign uses a forwarding provider and an indexed source filter or a joined filter, deletes three visible rows and then upserts an eligible row with an id no other command uses; its reconstruction check runs in the same test as the fixed-seed campaign and reads its per-case counts: 35 of 40 cases issue a held request, and every one of them changes rows while it is in flight. Loading must reach a fixed point: past a request budget the provider rejects and records it, and the initial load, every step and the end of each history assert the record is clear (a loader that re-requests a prefix it already holds can loop without reaching the provider, which this cannot see). A bounded step makes at most four provider requests, and each consumer's initial proven-prefix load is bounded separately, in total transfers (a repeated request for the same prefix counts) and in distinct rows (at most the source's size); a loader that asks for 100 extra rows on every page fails that bound and the initial-load work law. Loader mutants that never resume after a boundary request, or that ignore a load request while another load is pending, fail it; a mutant that drops a window move blocked behind a pending load still survives, even with the settlement check on held moves; whether it is equivalent is open. Open (#2148): on an on-demand source with a joined or anti-joined filter, an optimistic delete of the visible row leaves the window short until the delete persists, because the next row is never loaded. On an on-demand source with a source filter, and on an eager source with any filter, the same delete refills the window correctly; these are the contrast cases. Owner: this oracle. Needed witness: the optimistic-delete dimension (kept as a patch for #2148) in the grammar, plus a fixed histories of the anti-join trace. A refetch that re-runs each page alone, as query-db-collection does today, leaves a row that moved between two pages unloaded; random seeds found that trace, a named fixed history fails on it, and a query-db receiving witness reproduces it (#2136 tracks the provider fix). An Electric-style provider, which skips updates to rows it never sent, is not modeled; a mocked-stream witness shows a row moving into a served ordered range never arriving under the default replica mode (#2138). At one times the run count, the campaigns reach 87 refetch steps: 39 change the window, 6 remove a visible row, and 13 lead to a further provider request. A random seed found a refetch that empties a joined window, after which the loader refills it over several page requests and publishes `[]`, one row, then the final rows; a named fixed history keeps that trace for #2131. No incorrect final window has appeared on that path, and no loader mutant tried so far is caught only by it; the work law does not cover it. For an on-demand joined or anti-joined filter, the initial load must not request the whole source when the first window's worth of source rows in query order all pass the join and no boundary value is null or NaN; 35 executed cases meet that premise, and a compiler that reads the whole source for every joined filter fails eight tests on this law alone. The rows served by that initial load stay within the prefix, its boundary ties and a refill, for each consumer. Later steps of those plans have no work bound. An unindexed join filter over it left the window empty on main, until the plan counted the rows it still needs; restoring the old guard fails the campaigns and a fixed histories. A step that changes the visible rows must publish, and its subscriber starts with every visible key, so a removal-only change reaches it; mutants that drop update-only or removal-only publications fail. A step may publish one intermediate window per provider request it made, and only its last publication must show the final window, because a repair or refill can publish after each round trip (#2131); the content of those intermediate windows is unchecked. The model keeps its own copy of the markers, and full-join histories can insert the root rows of orphan markers. A premise-directed campaign inserts a fresh row and then changes an initial row's eligibility alone, so the row leaves the window only through the join; it and a named fixed history fail when a window row past the loader's settled boundary counts toward a full window. One case in four adds a second live query over the same sources with a larger window, and its rows law holds at every checkpoint; the work laws do not apply to those cases. #2155: a second live-query Collection over a refetching on-demand provider kept a short joined window after a refetch removed a tied row (the peer showed ranks `[0, 0]` where the model shows `[0, 0, 100]`). The loader fix that resumes a staged continuation after a synchronous answer the graph already processed closed that trace. The fixed histories of that indexed trace now expects the right window. Still open: an unindexed peer over a refetching provider keeps a short joined window (the peer shows `[100]` where the model shows `[100, 101]`), which also fails without that fix; each campaign therefore still excludes the peer and refetching pairing, as its last map. Owner: this oracle. Needed witness: a fixed histories of the unindexed trace flipped to pass, and the pairing restored to the grammar. Limits: Effects are checked for rows after each step, not for publication counts or positions. Histories move the first query's window with `setWindow` (150 moves at one times the run count, 56 on demand), and its rows law and ledger law then follow the moved window; the Effect and the peer keep theirs. On a holding provider every window-move promise must have fulfilled after the final drain. A refetching provider models query-db's unload: it drops the unloaded request and removes rows that no remaining request's last answer holds. The per-step work law applies only to forwarding, immediate, single-consumer cases: it skips refetching, holding and peer cases and move steps; a two-term indexed move scanned the source four times, which no law here bounds. Multi-term joined plans stay outside this harness, on both paths; on the on-demand path, the provider's transfer is bounded only for indexed single-term source-predicate plans. Joined windows compare order values, so a wrong row tied with the expected one passes; a window row tied with the boundary counts as proven before its tie request settles, which no witness exercises. A boundary that cannot advance past a window row would repeat one page per new key; reading the boundary's range locally should always reach that row, but no witness shows it. Joined ties are compared as any valid first rows; whether source-filter ties may be fixed to the source key is open. The same grammar includes NaN and null ranks and a second-order term, and bounds both rows read and rows delivered, including the initial load and index refills; a scan law limits each change to one pass over the source. A fixed case checks that an indexed descending window places nulls first, and a lifecycle witness checks that an eager full-source window is ready with its rows at creation when its source answers synchronously. The initial fallback cells check indexed and unindexed locale strings with distinct and tied values, plus a null boundary after a warm ordered request. The warm null-boundary case crosses preload-started and constructor-started live-query sync runs: the former completes at the synchronous cut, while the latter resumes deferred on-demand acquisition asynchronously and publishes after settlement. They require an unfiltered full-source request, no public row at fallback entry, and the expected row and status at the immediate readiness check. A Promise fallback stays loading at that checkpoint. A React receiving witness checks an eager locale-string `findOne()` at the first layout commit. A Query DB receiving witness checks warm cached subsets: both raw adapter calls return literal `true` with the source rows visible at each return, and the live query is immediately ready without a fetch. The same fallback cells observe subscriber changes from before the first source write: literal-true and Promise fallbacks each publish one nonempty final-window insert after the fallback settles, and the callback sees the complete row. Promise cells show no nonempty event at the immediate cut; a duplicate-event fault fails all eight cells. Other adapters and a real on-demand React first commit remain unwitnessed. Full-source work after initial publication and repair remain outside this synchronous guarantee. A separate post-publication oracle crosses marker deletion and retargeting with literal, Promise, and held-applied-receipt fallback responses. It also settles the child demand before holding the receipt, so the public live-query loading flag isolates the root fallback. The model checks final rows and net events, while event replay checks every callback snapshot; a retained or empty intermediate window is allowed. A loader fault that ignores the pending receipt fails at the held loading-flag check. Two literal-true cleanup-failure histories require that the replacement still publishes and the adapter error reaches the public query status without making the unrelated marker commit throw; the provider's applied receipts are recorded and compared outside provider callbacks. The Promise case checks eventual coherence on an asynchronous callback path, without claiming a separate timing cut. Four held-Promise histories apply fallback writes, change another join marker before provider settlement, and compare each callback and the final winner; an injected stale extra publication fails the event comparison. Other marker actions and overlapping root-source changes remain open; the provider has no later write or rejection, so this schedule does not establish when the loader claims full-source authority. The reversed-index oracle checks every reversed read's order and filter work for both null placements. The retirement-invalidation grammar (`ordered-loader.retirement-invalidation`) composes a constructive invalidation prefix, up to four settled answers that let the repair chain complete, and generated command suffixes with index availability, limit 1/2, joined deferral, needed rows, release errors, reentrant truncate and disposal, reentrant ordinary passes, retry timers, offset 0/1, and full-source plans. Its declared `completed-repair-release` reach counts only an invalidating release observed while a successful repair-chain answer settles and issues no further chain step; an instrumented run matched the production retirement path in 66 of 72 such histories, and the rest owed nothing more after a late disposal or full coverage; an ablation that invalidates only on other releases passes the older `release-invalidation` reach and fails this one. Only an on-demand source answers a release with an adapter unload, so neither this grammar nor the broad `ordered-loader.request-authority` arbitrary pairs `releaseInvalidates` with a synchronous repair answer, which reads an eager source whose releases bypass the adapter (`CollectionSyncManager.unloadSubset`). The broad arbitrary weights `releaseInvalidates` 5:1 like the other release reactions, because an invalidating release leaves the quiet report laws. The directed grammar also places the invalidation after the callback's disposal, reentrant pass, and truncate (`late-release-invalidation`). Broad overlap states require 20 histories each, and the rarer full-source-plan overlap requires 5. An invalidating unload also writes graph input, so the driver's drain runs one more loader pass before it judges progress, as the live-query Collection and Effect graph loops do; without that pass, a repair that finishes inside a loader pass after joined work clears was misjudged as owing no further read. Its independent request ledger records issue and invalidation events on one clock. It requires an authoritative start after the callback's invalidation for a live finite repair after retry/drain; complete full-source coverage absorbs invalidation, cursor reset transfers pre-reset work to replay, disposal ends ownership, and unanswered authoritative work retains its existing no-timeout limit. Each normal broad campaign measures callback overlap with release error, truncate, disposal, pass reentry, offset one, timer-enabled scenarios, full-source plans, and multiple successor chains. A separate `ordered-loader.retirement-receiver` property runs real live-query Collection and Effect consumers, and a live-query Collection whose `setWindow` to the other offset starts in the same turn as the ordering write. It varies indexed/unindexed sources, limit 1/2, offset 0/1, literal/Promise adapter answers, a held newer replacement answer, and the unload's change: moving the repaired prefix, deleting its rows before the boundary, deleting the boundary row, or deleting a prefix row that ties with it, each of which owes a replacement, or evicting a sent row past the repair's boundary, including a row that ties with the boundary but lies outside the prefix, which keeps that boundary and starts no read. A tie row sorts before or after the boundary row by key, as live-query Collections order ties. A same-turn window move may repair either window's prefix, so that kind keeps only the move and row 1's eviction; prefix deletes and ties run on the other kinds. Each consumer has separate declared adapter-unload and held-answer reach, and delete, boundary-row delete, tie delete, tie eviction, and eviction unloads have their own reach; each grammar runs 600 histories. A loader that skipped every retirement-time delete fails the delete histories at the progress relation, one that treated every sent-row delete as new information fails the eviction histories, one that treated every boundary tie as eviction fails the boundary-row and tie deletes, one that treated every boundary tie as new information fails the tie evictions, and one that kept only the boundary row's key fails the tie deletes. The loader keeps the keys of the settled prefix rows that tie with its boundary row. The focused `keeps a repair's boundary when its retirement removes a row the loader sent` test remains as a supplemental example. An instrumented run placed every invalidating receiver unload inside retirement (200 of 200 per campaign). Following Atomic window publication, the window move stays pending while the replacement is held and settles with its chosen window visible; a mutant whose subset loads stop joining the active window operation fails only those move comparisons. Held-answer reach is recorded only after the provider answer is blocked and the prior-window and no-publication comparisons pass. The provider moves its repaired prefix behind a still-uninstalled row during unload and supplies no later external graph input. The shared progress relation checks that an authoritative start follows the invalidation and precedes the first replacement publication. Independent full-provider sorting checks final rows; held answers retain the previous complete public window and publish no callbacks, and completion publishes one complete replacement. Fixed replay witnesses force the held-answer premise for each consumer. An executed public-method call probe observed reentrant `loadMore` inside every sampled unload for both consumers, with no production-state reads. Original debt-clearing and deliberately delayed-one-pass mutants fail the progress/publication judgments; start observations before the invalidation or at publication fail calibration. This evidence does not require recursive synchronous dispatch: deferred replacement remains legal while the public gate holds. The replay-continuation grammar (`ordered-loader.replay-continuation`) follows ARCHITECTURE.md, Ordered requests/continuation/recovery: a pre-reset request belongs to truncate replay and cannot revive its discarded cursor; a graph continuation survives bookkeeping until a graph pass consumes it or cursor reset discards it. A graph pass that a release callback runs consumes nothing, because the loader blocks refinement until its release pass unwinds. `continuationOwed` is model-only classification provenance, not product completion state. The handoff/reset grammar and exact shared-model replay reject consuming that provenance during replay bookkeeping or during a release pass. These are harness corrections; they supply no production resource-leak claim. The grammar crosses a graph pass in each release callback, a truncate before the repair, and one or two provider answers with the earlier axes. Its states `deferred-refill`, `reset-continuation`, and `release-pass-refill-resumed` are declared, and two constructed histories reach them; `release-pass-continuation`, which the driver's provenance over-approximates, is measured only. The release-pass history uses an on-demand source (`syncRepair=false`), whose release reaches the adapter, so production can produce it. At one times the run count, with constructed histories building half of each campaign, the fixed seed reaches the declared states in 78, 59, and 60 of about 200 histories (the measured state in 96), and the random campaign in about 142, 123, and 105 of about 400. Generated histories alone reach them in 42, 23, and 17 of 200 at the fixed seed. The held law covers every successful acquisition of the latest repair chain, and the driver treats only the stale self-release as an unblocked release (see the ordered-loader authority entry). The held law is also checked after each replay settlement and request settlement inside the drain. A loader that releases every held lease, the chain's own included, when replay settlement finishes a repair chain passed these histories at the after-drain checkpoint, because the refill covers the prefix before then; the drain checks reject it in both fixed regressions and the constructed history. A synchronous repair answer still pairs with a release-triggered truncate in the generated half. An eager source's release never reaches the adapter (`CollectionSubscription.createSubsetAcquisitionRecord`), so those pairings calibrate continuation provenance without a production-reach claim. The broad request-authority arbitrary pairs synchronous repair answers with release faults, truncates, disposals, and reentrant passes in the same over-approximating way; those histories pass and support no production-reach claim either. The random handoff campaign runs 400 histories so that state stays above its minimum. Limits: the real receiver uses distinct finite numeric ranks, ascending root order, one source and consumer, one qualifying callback invalidation, no failure/truncate/disposal inside the real unload callback, one window move per history and no failed replacement under a move, and no provider-specific network. Its on-demand source settles every repair answer asynchronously in the loader, even a literal adapter answer; the loader's synchronous repair settlement needs an eager source, which has no adapter unload to invalidate. The controlled grammar measures the combined lifecycle cases; it does not transfer all such combinations across the public receiver boundary. No claim about obsolete later cursor-demand retirement (#2223) or arbitrary callback composition follows. Existing run budgets remain unchanged. Random samples do not establish bounded exhaustiveness. The controlled and receiving grammars have distinct registered replay properties, so each seed and shrink path selects only its own driver. The no-leak calibration supplies a retained-lease observation to the same request-ledger comparison after an unmodified run of the same covering-repair history; it reads no private member names. | | Indexed predicate filtering | `packages/db/tests/query/index-path-collision-oracle.test.ts` | A bounded cross product of numeric values checks exact public keys before and after adding a nested-field BTree index. Direct predicates vary argument order, bound inclusivity, reversed operands, and bound field. Public Collection subscription and live-query callbacks run with and without the index. Selected-field ordering compares a direct JavaScript sort with a public `$selected` callback; restoring the dotted-key proxy cache made that comparison fail. The original compound grouping failed four indexed cases while scan controls passed. The original callback proxy caches also failed both unindexed public routes. A mutant cleanup control preserves the primary mismatch and secondary release error. Arbitrary path segments, nullish values, custom collation, and incremental publication need separate witnesses if claimed. | | Lazy target path identity | `packages/db/tests/query/compiler/lazy-targets.test.ts` | A focused same-source `UnionFrom`/`coalesce` witness requires both [`a.b`] and [`a`, `b`] demand targets. Restoring dotted-string deduplication drops the second target at the compiler boundary. A public on-demand adapter and row-publication history still need a separate witness. | @@ -8448,12 +8448,193 @@ Input: `indexed=false`, `limit=1`, `settledFirst=true`, `releaseFault=false`, History: `truncate; settle(0, success); invalidateThenFailOldest; move(-1); joinedBusy; settle(0, success)`. -Status: confirmed baseline oracle failure, underlying repair location unresolved. -Next witness: distinguish whether the final authoritative read covers the held -requests while joined work defers a reentrant pass, then check the real -subscription receiving path. This remains separate from PR #2346's observer -metadata-sharing and discarded-publication scope. The test, grammar and run -budget remain unchanged; a green later random campaign does not close it. +Status: resolved as a harness correction (2026-11-11). It is not a production +defect. CI random seed `-1691316941` (path +`7958:0:0:1:5:14:13:13:17:16:17`) found the same failure on an on-demand +source (`syncRepair=false`), with history `settle(0, success); report; +truncate; move(-1); joinedBusy; settle(0, success); settle(0, success); +settleNewest`. In both traces, replay settlement finishes the repair chain +and retires the pre-truncate leases. Each release callback runs a graph pass +while joined work still defers the chain's refill. The loader blocks ordered +refinement for the whole release pass (`releaseOwned` sets `requesting`), so +that pass is ignored and the staged refill survives. The next pass resumes it +as a `refetch: true` prefix of the same chain. The driver's `run` helper took +the blocked pass for one that consumed the refill. It then classified the +refill as a new repair start, and the chain's own prefix and tie as leaked. +The same ledger without the release pass passes, and the progress probe's +next chain retires all three leases. Authority: ARCHITECTURE.md, Ordered +requests, continuation, and recovery ("ordered refinement stays blocked until +the pass unwinds"). The model rule for chain steps is unchanged; the driver +no longer consumes provenance in a release callback's pass. Both traces are +fixed regressions. The `ordered-loader.replay-continuation` grammar reaches +the state through a declared, constructed history. RED: the fixed seed +`20261029` failed with `no leak: requests [3,4] are still held after +authoritative request 5 succeeded` before the correction. + +Follow-up, same date. The release-pass rule now applies only to releases +inside a release pass. The one release outside a pass is the stale finite +request that settles after its repair finished and is released at once, from +its own settlement handler (`ordered-source-loader.ts`, the +`retiringSupersededAcquisitions` block). A graph pass there is not blocked. +The driver identifies that release from its own ledger: the request is the one +it is settling, it is finite, it was issued before the current ordering epoch, +in the current truncate generation, and no full-source lease covers the +source. Its graph pass then counts as an ordinary pass. A scratch calibration +compared this rule with an instrumented production branch on all 50,298 +releases of the file's campaigns: 26 stale self-releases, no mismatch. With a +continuation owed, the broad campaign meets such a pass 3 times at the fixed +seed and 1 to 4 times in each of five random campaigns of 10,000 histories, +and prints the count as `unblockedReleasePasses`. + +Stated assumption: that the stale self-release's graph pass is not blocked +has no ARCHITECTURE.md authority. ARCHITECTURE.md says only that such a request +is released at once. The driver follows current production here. If +production later blocks refinement during that release, the driver will +misclassify the next request and may report a false failure; the repair then +belongs in the driver, not in ARCHITECTURE.md. + +The held law now covers every successful acquisition of the latest repair +chain: its prefix, ties, and refills. Only a later prefix at least as long may +retire a prefix member, and nothing retires a tie or cursor page +(ARCHITECTURE.md, ordered repair: only the new repair acquisitions remain; a +successful larger prefix retires settled smaller prefixes, not ties or cursor +suffixes). A reviewer mutant that releases the chain's refill as soon as it +settles (`droprefill`) passed every test at `0721dec92` and fails 6 tests with +this law. A mutant that lets any later current prefix retire a settled prefix, +even a smaller one, passed every test at `4d12a16c2` and fails 3 tests now. +Production passes. + +`release-pass-continuation` counts release passes where the driver's +provenance owes a continuation. That over-approximates a pending one, so it +is measured only. The required state is `release-pass-refill-resumed`: a +blocked release pass ran while a continuation was owed, and a later graph pass +in the same epoch and truncate generation issued a refetch step of the same +chain whose demand the chain had not read. Only a staged or blocked +continuation issues such a step from a pass. A scratch calibration against the +loader's private `stagedContinuation` and `blockedLoadMore` fields matched it +on every handoff history: 192 release passes with a real pending continuation, +all observed as resumed; 97 driver-owed passes with nothing pending, none +observed. Reach, generated histories only (a scratch run without the +constructed histories): fixed seed `20261029` reaches it in 17 of 200 +histories, and random seeds in 26 to 32 of 400. With the constructed +histories, which build half of each campaign, the fixed seed reaches it in 60 +of 202, and random seeds in about 105 to 128 of 402. + +Production defect, fixed 2026-11-11 (reviewer finding on `4d12a16c2`). Law: +a repair chain whose ordering epoch moved is replaced before it issues another +tie or refill (ARCHITECTURE.md, ordered repair). The settlement path checked +that (`repairNeedsReplacement()` before it continues). A continuation that +the chain staged, or a window move that joined work blocked with +`continuesOrderedPrefixRepair`, ran later through `loadMore`. `loadMore`'s +exception for a running chain then let the obsolete chain issue one more page +or refill. Invalidation had cleared the boundary, so that step had no cursor, +and the driver took it for the replacement start. When it settled, +`finishOrderedPrefixRepair` started the real replacement, which the driver +classified as a step. That is the "replacement start without an epoch move" +described in the earlier version of this entry: the epoch had moved. Trace +(request-authority, fixed seed `20261016`, path `61:1:1:2:2:5:4:9:9:7`): +`indexed=true`, `limit=1`, `settledFirst=false`, `syncRepair=true`; history +`settle(0, success); sourceDelete(react); invalidateThenFailOldest; settle(0, +success)`. It is now a fixed regression, beside two older fixed regressions +that also failed on it. Fix: `loadMore` calls `finishOrderedPrefixRepair`, so +the replacement starts, when a resumed repair step's chain needs replacement. +A staged boundary step also reaches that check, because invalidation cleared +the settled boundary it would read. A scratch probe of production counted +zero obsolete steps over ten random seeds of the whole file after the fix, and +38 in one run before it. Laws: + +- No stale step, extended to resumed requests. A request that a pending + continuation issued after its chain's epoch moved must start the + replacement. So its own successful settlement must not start a repair of + the same epoch. The premise uses the driver's provenance, which + over-approximates, so the law judges the request by what its settlement + issues. A hung or failed obsolete step is not judged. +- One start per epoch. A chain step does not read its chain's start demand + again unless an optimistic departure, a head insert, or a source delete + happened since the start. + +Reach: the new state `continuation-before-epoch-move` (the epoch moves while +a repair continuation is owed) is reached in 75 of 10,000 generated histories +at fixed seed `20261016` and 69 of 10,000 at the random seed, with a minimum +of 20. RED on unchanged production: 6 tests (both laws; two existing fixed +regressions among them). GREEN after the fix: the four ordered-loader oracle +files pass, 918 tests. Mutants: restoring the defect fails 6 tests (7 with the +new fixed regression). The `restart` mutant now fails 6 tests on the +one-start-per-epoch law. One run of the smaller-prefix mutant also reported +one no-stale-step flag while the production probe saw no obsolete step. That +run's random seed was not recorded, and 16 seeds did not reproduce it; it may +be a false flag of the law's over-approximating premise. + +Review follow-up: two false flags on unchanged production, found by the +review at the default random budget (2 of 40 seeds failed with no mutant), +are repaired in the oracle only. + +- The no-stale-step law counted any full-source read that a settlement + started as proof of an obsolete step. A genuine replacement start whose + settlement falls back to a full-source read (a head insert, or an + unexpressible boundary rank) was flagged. Witness: request-authority, + seed 4, path `17698:0:0:0:10:16:17:17:17`. The law now counts a full-source + read only when every installed rank is finite. +- The fake's drain settled a pending replay while a request issued inside + that replay attempt was still in flight, and the held law then flagged the + retirement that followed. ARCHITECTURE.md (Replay participants) publishes a + replay only after every acquisition of its attempt settles. Witness: seed + 119, path `1430:0:1:1:5:4:10:12:14:15:15`. The drain now settles those + requests first. + +After both repairs, 40 random seeds (300 to 339) pass the whole file with no +mutant. With the review's production mutants at seed 7, `nofix` fails 8 +tests, `restart` 6, `droprefill` 6, `retireown` 29, and `smaller` 1. One +premise risk remains undrawn: a fresh start whose prefix returns empty would +issue a refill prefix from its own settlement and be flagged. The fake never +returns an empty start prefix there. + +Awaiting maintainer decision. Owner: this oracle. + +- `m3`: a blocked pass drops a staged continuation. The refill is later + issued as an ordinary page without `refetch: true`, which ARCHITECTURE.md + forbids for a repair chain's acquisitions. Only the constructed history's + required reach rejects it (fixed seed `20261029`, constructed history over + the replay-continuation grammar with `syncRepair=false`, `joined=true`, + `releaseReenters=true`, `reset=before-repair`, `answers=2`; history + `settle(0, success); settle(0, success); report; truncate; move(-1); + joinedBusy; settleNewest; settleNewest`). A candidate law ("a finite + request issued while a chain continuation is owed carries `refetch: true`") + failed four campaigns on unchanged production, because `continuationOwed` + over-approximates. +- Re-reads after new source input. The one-start-per-epoch law exempts a + chain step that re-reads its start demand after an optimistic departure, a + head insert, or a source delete. Production does both: it re-reads the + chain's prefix as an optimistic refill (an existing fixed regression keeps + that trace as a legal chain step), and it reads the same cursor page twice + after a head insert. Whether those re-reads are required, or should grow the + read instead (optimistic headroom, ARCHITECTURE.md), is undecided. + +Next witness, restored: check the real subscription receiving path. +`collection-subscriber.ts` calls `settleFullSourceReplay()` in the replay's +`succeed` callback and then schedules a graph run +(`scheduleGraphRunIfSyncRunCurrent`), so the resumed refill reaches the loader +through that scheduled run, not through the fake's drain. No executed witness +covers that path. + +### Ordered refill publication after replay settlement, 2026-11-11 + +Owner: `packages/db/tests/query/ordered-work-oracle.property.test.ts`, whose +holding provider compares publications while loads are held. When replay +settlement finishes a repair chain and joined work defers the chain's refill, +the refill registers its participant with `holdPublication` set to +`needsOrderingRepair`, which is then false (`ordered-source-loader.ts`, the +`onResult` call at the end of `requestAndObserve`). Publication can therefore +open between the replay settlement and the refill's settlement. +ARCHITECTURE.md, Atomic window publication, requires every page, tie, and +refill needed to reach the fixed point to publish once, as one operation. The +request-authority oracle does not observe publication, so it cannot judge +this. Needed witness: an on-demand, joined, unindexed live-query Collection +and Effect whose truncate replay settles while joined work defers a repair +refill. It must show that no publication happens between replay settlement +and the refill's settlement, and that one publication happens after it. The +existing in-flight comparison there is weaker than the barrier law (#2131). +Status: recorded only; not reproduced. ## Compiler group reduction boundary diff --git a/packages/db/src/query/live/ARCHITECTURE.md b/packages/db/src/query/live/ARCHITECTURE.md index 24232dd485..0e0c6e9879 100644 --- a/packages/db/src/query/live/ARCHITECTURE.md +++ b/packages/db/src/query/live/ARCHITECTURE.md @@ -1141,7 +1141,10 @@ new repair acquisitions remain. Every acquisition in this chain uses reusing completed or in-flight work. A source-order invalidation generation fences the chain. If another qualifying mutation arrives before it finishes, core starts a replacement repair before releasing the publication barrier and -before the obsolete chain can issue another tie or refill. A qualifying change +before the obsolete chain can issue another tie or refill. That holds for a +step that a continuation the chain staged, or a window move that joined work +blocked, would resume after the mutation: resuming it starts the replacement +instead. A qualifying change that a retirement release delivers after the chain succeeds belongs to the same fence, including a delete of a row in its prefix, such as the boundary row or a tie the prefix holds: the repair keeps that newer debt, the next ordered pass starts its replacement before the barrier releases, and a window move waiting for the diff --git a/packages/db/src/query/live/ordered-source-loader.ts b/packages/db/src/query/live/ordered-source-loader.ts index 405f06f053..a14222327c 100644 --- a/packages/db/src/query/live/ordered-source-loader.ts +++ b/packages/db/src/query/live/ordered-source-loader.ts @@ -327,6 +327,15 @@ export class OrderedSourceLoader { return this.pending } this.blockedLoadMore = undefined + // A repair step that a staged continuation or a blocked window move + // resumes after the chain's epoch moved starts the replacement instead: + // the obsolete chain issues no further tie or refill. A staged boundary + // step reaches this check too, because the invalidation cleared the + // settled boundary it would read. + if (continuesOrderedPrefixRepair && this.repairNeedsReplacement()) { + this.finishOrderedPrefixRepair(windowOperationGeneration) + return this.pending + } // A finite step staged under ordering debt cannot run ahead of the owed // read. An invalidation drops it. A failure, even one from before a // cursor reset that keeps the work staged after it, clears the boundary, diff --git a/packages/db/tests/query/ordered-source-loader-state-oracle.test.ts b/packages/db/tests/query/ordered-source-loader-state-oracle.test.ts index 3219745482..9a3f78e35f 100644 --- a/packages/db/tests/query/ordered-source-loader-state-oracle.test.ts +++ b/packages/db/tests/query/ordered-source-loader-state-oracle.test.ts @@ -1,3 +1,4 @@ +import { isDeepStrictEqual } from 'node:util' import fc from 'fast-check' import { afterEach, beforeEach, describe, expect, it, vi } from 'vitest' import { @@ -51,13 +52,16 @@ function tieValue(options: RequestOptions): unknown { * ARCHITECTURE.md, "Ordered requests, continuation, and recovery", gives the * loader authority rules for requests that overlap an ordering invalidation: * - * - **Held:** a successful bounded repair holds the acquisitions it read. - * Only a later read that covers them may retire them: a newer repair, a - * full-source read, or a truncate replay that covers the source, or a - * prefix read issued after the repair that reaches every repair row still - * inside the window. That prefix counts once it succeeds or once a - * successful replay reacquires its demand while it is still in flight. A request issued before the invalidation proves no - * current coverage, so it never retires them. + * - **Held:** a successful bounded repair holds the acquisitions it read: + * its prefix, its ties, and its refills. Only a later read that covers + * them may retire them: a newer repair, a full-source read, or a truncate + * replay that covers the source. A prefix read at least as long, issued + * after one of the chain's prefixes, may also retire that prefix, but no + * tie or cursor page (ARCHITECTURE.md: a successful larger prefix retires + * settled smaller prefixes, not ties or cursor suffixes). That prefix counts once it succeeds or once a successful + * replay reacquires its demand while it is still in flight. A request + * issued before the invalidation proves no current coverage, so it never + * retires them. * - **No leak:** once loading is quiet and no failure blocks it, the loader * holds nothing issued before its last successful authoritative read. * Otherwise every later refetch would read that request again. A @@ -71,7 +75,14 @@ function tieValue(options: RequestOptions): unknown { * oracle records any `OrderedLoaderInvariantError` the loader throws, so * the generated histories also fuzz that table. * - **No stale step:** a repair chain whose ordering epoch moved is replaced - * before it issues another tie or refill. + * before it issues another tie or refill. That includes a step that a + * continuation the chain staged, or a window move that joined work + * blocked, resumes after the move: the request it issues must start the + * replacement, so its settlement cannot start the replacement again. + * - **One start per epoch:** a chain step does not read the chain's start + * demand again unless an optimistic departure, a head insert, or a source + * delete gave the window new source input since the start. Reading it + * again restarts the repair without new debt. * - **Error identity:** a request that fails reports its own error through * its participant. Neither a release's cleanup error nor a read the loader * starts while handling it can replace that error. A dead request's failure @@ -142,7 +153,24 @@ function tieValue(options: RequestOptions): unknown { * - a repair prefix is a step of a running chain, not a start, when it is * issued while a chain member settles or by the continuation such a * settlement left staged (a synchronous answer) or deferred (joined work), - * as an optimistic refill or a shrunk window's prefix is; + * as an optimistic refill or a shrunk window's prefix is. The chain's start + * and its steps are the chain's acquisitions. A graph pass that a release + * callback runs does not consume that continuation: the loader blocks + * ordered refinement until its release pass unwinds (ARCHITECTURE.md), so + * the refinement resumes on a later pass. The one release outside a + * release pass is a stale finite request that settles after its repair + * finished and is released at once; the ledger sees it as the request + * being settled, issued before the current epoch, in this truncate + * generation, with no full-source lease. That its graph pass is ordinary + * is a stated assumption: ARCHITECTURE.md says only that such a request + * is released at once, not whether refinement is blocked meanwhile. If + * production later blocks it, the driver may misclassify the next request + * and report a false failure; + * - a request is resumed after an epoch move when it is authoritative and + * finite, a continuation was owed, no request was settling, and the + * ordering epoch moved since the latest start. That premise + * over-approximates a pending continuation, so the no-stale-step law + * judges such a request by what its own settlement issues; * - a truncate replay that settles while the subscription holds a * full-source lease, even a failed one, covers the source and counts as a * successful start after every earlier request; the leases it reacquired @@ -216,7 +244,10 @@ function tieValue(options: RequestOptions): unknown { * * ## Checkpoints * - * Held, one request at a time, and release are checked after every step. + * Held, one request at a time, and release are checked after every step, + * and inside the drain after each replay settlement and each request it + * settles: replay retirement can release a lease that a later read in the + * same drain covers. * A release that throws is an adapter bug: the loader reports it uncaught * from a microtask and changes nothing else, so each one must be reported * that way exactly once, and no other error may escape a microtask. @@ -241,7 +272,10 @@ function tieValue(options: RequestOptions): unknown { * is not required then, the leak law does not judge the unfinished chain, * and the strand law accepts recovery that is owed behind it. A failed replay stays pending until the drain * settles it. The fake releases an acquisition when the loader calls its - * release; it does not model an adapter that removes rows later. + * release; it does not model an adapter that removes rows later. The + * no-stale-step law sees an obsolete step only when it succeeds and its + * settlement then starts the replacement; a hung or failed obsolete step + * is not judged by it. */ type LedgerRequest = { index: number @@ -271,6 +305,15 @@ type LedgerRequest = { issuedTruncates: number failedTruncates: number failedAt: number + // How the loader asked for it, and the epoch moves before it was issued. A + // finite request issued before the current epoch is stale. + method: Observed[`method`] + issuedEpochMoves: number + // The repair chain the request belongs to: the ledger index of that chain's + // start. A full-source read and an ordinary page belong to none. + chain: number | undefined + // A pending continuation issued the request after its chain's epoch moved. + resumedAfterEpochMove: boolean } type AuthorityCommand = @@ -532,6 +575,10 @@ type AuthorityObservation = { hungRequests: number offsetWindows: number releaseInvalidations: number + // Graph passes in the stale self-release, which runs outside a release + // pass, while a continuation was owed. + unblockedReleasePasses: number + epochMovesWithContinuation: number retirementSuccessorChains: number replayContinuationHandoffs: number // Current failed requests whose participant reason reached the identity cut. @@ -948,7 +995,9 @@ async function checkAuthorityCase( | `late-release-invalidation` | `completed-repair-release` | `deferred-refill` - | `reset-continuation`, + | `reset-continuation` + | `release-pass-continuation` + | `release-pass-refill-resumed`, ) => void, observeRejection?: (reason: unknown) => unknown, observeRelease: (released: boolean) => boolean = (released) => released, @@ -1029,6 +1078,8 @@ async function checkAuthorityCase( } } let releaseViolation: string | undefined + let obsoleteStepViolation: string | undefined + let restartViolation: string | undefined let unexpressibleTieViolation: string | undefined let resetViolation: string | undefined // A disposed loader owns nothing: it issues no request and releases no @@ -1052,6 +1103,35 @@ async function checkAuthorityCase( // continuation survives bookkeeping, while cursor reset discards its // boundary and every pre-reset request belongs to truncate replay. let continuationOwed = false + // The repair chain of the latest start, the request being settled, and a + // blocked release pass that ran while a continuation was owed. + let currentChain: number | undefined + // The ledger length at the last command that delivered new source input + // to the window: an optimistic departure, a head insert, or a source + // delete. + let lastSourceInputAt = -1 + // Epoch moves while a repair continuation was owed. + let epochMovesWithContinuation = 0 + let settlingRequest: LedgerRequest | undefined + let deferredByReleasePass: + { epochMoves: number; truncates: number } | undefined + let unblockedReleasePasses = 0 + const sameDemand = (a: LedgerRequest, b: LedgerRequest) => + a.method === b.method && + isDeepStrictEqual( + [ + a.options.orderBy, + a.options.limit, + a.options.where, + a.options.minValues, + ], + [ + b.options.orderBy, + b.options.limit, + b.options.where, + b.options.minValues, + ], + ) let invalidateNextPage = false let releaseFaults = 0 let releaseInvalidations = 0 @@ -1112,6 +1192,21 @@ async function checkAuthorityCase( issuedTruncates: truncates, failedTruncates: -1, failedAt: -1, + method, + issuedEpochMoves: epochMoves, + chain: undefined, + // A continuation that the chain staged, or that joined work blocked, + // issues this request from a later graph pass after the chain's epoch + // moved. The chain must be replaced first (ARCHITECTURE.md, ordered + // repair), so this request must start the replacement. + resumedAfterEpochMove: + authoritative && + !fullSource && + continuationOwed && + !settlingChainMember && + settlingRequest === undefined && + epochMovesAtLastStart >= 0 && + epochMoves !== epochMovesAtLastStart, } ledger.push(request) // No cursor expresses a NaN or infinite rank, so the loader reads the @@ -1153,7 +1248,68 @@ async function checkAuthorityCase( if (startsAuthority(request)) { epochMovesAtLastStart = epochMoves repairOwed = false + currentChain = fullSource ? undefined : request.index } + if (startsAuthority(request) || request.chainStep) + request.chain = currentChain + // No obsolete step: a request that a pending continuation issued after + // its chain's epoch moved must start the replacement. If its own + // successful settlement starts a repair of the same epoch, the request + // was a step of the obsolete chain. Its shape alone cannot tell: an + // unindexed step and a replacement start read the same prefix. + const resumed = settlingRequest + if ( + resumed?.resumedAfterEpochMove && + resumed.outcome === `ok` && + resumed.issuedTruncates === truncates && + resumed.issuedEpochMoves === epochMoves && + authoritative && + // A full-source read proves an obsolete step only when every installed + // rank is finite: a head insert or an unexpressible boundary sends a + // genuine replacement start's settlement to a full-source read too. + ((fullSource && + snapshot().every(({ value }) => Number.isFinite(value.rank))) || + (options.orderBy !== undefined && + options.where === undefined && + options.minValues === undefined)) + ) { + obsoleteStepViolation ??= `request ${resumed.index} resumed a repair continuation after its chain's epoch moved, and its settlement started the replacement (request ${request.index}): it was a step of the obsolete chain` + } + // One start per epoch: a chain step that reads its chain's start demand + // again restarts the repair without new debt. Only new source input + // since the start, an optimistic departure, a head insert, or a source + // delete, can make that read return more (ARCHITECTURE.md, ordered + // repair: a prefix, then a tie and refill per new boundary). + if ( + request.chainStep && + request.chain !== undefined && + sameDemand(ledger[request.chain]!, request) && + lastSourceInputAt <= request.chain + ) { + restartViolation ??= `request ${request.index}, a step of repair chain ${request.chain}, read the chain's start demand again with no new source input since` + } + // A blocked release pass deferred a pending refill, and a later graph pass + // resumed it: a refetch step of the same chain, in the same epoch, that + // reads a demand the chain has not read. Only a staged or blocked + // continuation issues such a step from a pass; a new start, or a restart + // inside the chain, would read the chain's first prefix again. + if ( + deferredByReleasePass && + request.chainStep && + ledger.every( + (other) => + other === request || + other.chain !== request.chain || + !sameDemand(other, request), + ) && + settlingRequest === undefined && + !settlingChainMember && + deferredByReleasePass.epochMoves === epochMoves && + deferredByReleasePass.truncates === truncates + ) { + reached?.(`release-pass-refill-resumed`) + } + deferredByReleasePass = undefined // An issued request consumes an owed continuation. An ordinary page also // shows the chain finished, since none is issued while a repair runs. continuationOwed = false @@ -1222,6 +1378,19 @@ async function checkAuthorityCase( if (truncatePending && !explicitRetrying && !coveredBySource) { releaseViolation ??= `request ${request.index} was released while a truncate replay was pending` } + // Every release the loader makes runs inside a release pass, which + // blocks ordered refinement until it unwinds, except one: a stale + // finite request that settles after its repair finished is released at + // once, from its own settlement (ARCHITECTURE.md, ordered repair). The + // driver sees that case directly: the request is the one it is + // settling, it was issued before the current epoch, in this truncate + // generation, and no full-source lease covers the source. + const selfRelease = + request === settlingRequest && + !request.authoritative && + request.issuedEpochMoves !== epochMoves && + request.issuedTruncates === truncates && + !coveredBySource request.released = true const invalidate = () => { if (!testCase.releaseInvalidates || releaseInvalidations > 0) return @@ -1258,10 +1427,24 @@ async function checkAuthorityCase( return } if (testCase.releaseReenters && !reentering) { + // A release callback runs a graph pass while a repair continuation + // is still owed: the state where a pass that issues nothing must not + // be read as consuming that continuation. + if (continuationOwed && selfRelease) unblockedReleasePasses++ + if (continuationOwed && !selfRelease) { + reached?.(`release-pass-continuation`) + deferredByReleasePass = { epochMoves, truncates } + } reentering = true reentrantPasses++ try { - run(() => loader.loadMore()) + // The loader blocks ordered refinement until its release pass + // unwinds (ARCHITECTURE.md, Ordered requests, continuation, and + // recovery), so that pass consumes no owed continuation. The + // refinement it asked for resumes on a later pass as the same chain. + // The stale self-release runs no pass, so its graph pass is an + // ordinary one. + run(() => loader.loadMore(), selfRelease) } finally { reentering = false } @@ -1376,6 +1559,8 @@ async function checkAuthorityCase( ) const invalidateSourceOrdering = loader.invalidateSourceOrdering.bind(loader) loader.invalidateSourceOrdering = () => { + if (continuationOwed && currentChain !== undefined) + epochMovesWithContinuation++ epochMoves++ invalidateSourceOrdering() } @@ -1488,7 +1673,7 @@ async function checkAuthorityCase( observe(error) } // A pass that issues nothing consumed or finished an owed continuation, - // unless joined work deferred it. + // unless joined work deferred it or a release pass blocked it. if (consumesContinuation && ledger.length === before && !joinedPending) { continuationOwed = false } @@ -1501,6 +1686,8 @@ async function checkAuthorityCase( const replayPending = () => truncatePending function truncate() { truncates++ + currentChain = undefined + deferredByReleasePass = undefined // Reset discards any staged continuation. A later settlement may stage a // new one only for a request issued in this replay generation. if (continuationOwed) reached?.(`reset-continuation`) @@ -1531,6 +1718,7 @@ async function checkAuthorityCase( const chainMember = request.authoritative && !request.fullSource const before = ledger.length settlingChainMember = chainMember + settlingRequest = request if (ok) request.deferred.resolve() else { request.error = new Error(`request ${request.index} failed`) @@ -1539,6 +1727,7 @@ async function checkAuthorityCase( settlingFailure = !ok answeringRepair = ok && chainMember await flush() + settlingRequest = undefined settlingFailure = false answeringRepair = false // The chain completed in this settlement when it issued no further step: @@ -1649,6 +1838,18 @@ async function checkAuthorityCase( ), ) } + if (obsoleteStepViolation) { + rejectAt( + `ordered-source-loader-state-oracle.test.ts:obsolete-step`, + new Error(`no obsolete step ${checkpoint}: ${obsoleteStepViolation}`), + ) + } + if (restartViolation) { + rejectAt( + `ordered-source-loader-state-oracle.test.ts:restart`, + new Error(`one start per epoch ${checkpoint}: ${restartViolation}`), + ) + } if (concurrencyViolation) { rejectAt( `ordered-source-loader-state-oracle.test.ts:1599`, @@ -1673,29 +1874,43 @@ async function checkAuthorityCase( lastAuthoritativeSuccess() > repair.index ) return - // A prefix read issued after the repair covers the repair's rows that are - // still inside the window when it reaches as far; it may retire the - // repair's prefix. One issued before the repair proves no current - // coverage and may not. - const windowRows = Math.min( - repair.options.limit ?? 0, - info.offset + info.limit, - ) - const coveredByLaterPrefix = ledger.some( - (request) => - request.index > repair.index && - (request.outcome === `ok` || request.replayed) && - request.options.orderBy !== undefined && - request.options.where === undefined && - request.options.minValues === undefined && - (request.options.limit ?? 0) >= windowRows, - ) - if (coveredByLaterPrefix) return - if (repair.released) { + // Every successful acquisition of that chain stays held: its prefix, + // ties, and refills (ARCHITECTURE.md: only the new repair acquisitions + // remain, and a larger prefix does not retire ties or cursor suffixes). + // A prefix read issued after a prefix member covers that member's rows + // still inside the window when it reaches as far; it may retire it. One + // issued before it proves no current coverage and may not. + const isPrefix = (request: LedgerRequest) => + request.options.orderBy !== undefined && + request.options.where === undefined && + request.options.minValues === undefined + for (const member of ledger) { + if ( + member.chain !== repair.index || + member.outcome !== `ok` || + !member.released + ) + continue + // Only a prefix at least as long retires a prefix member: a smaller + // later prefix that still reaches the window does not hold the + // member's other rows (ARCHITECTURE.md: a successful larger prefix + // retires settled smaller prefix acquisitions). + const coveredByLaterPrefix = + isPrefix(member) && + ledger.some( + (request) => + request.index > member.index && + (request.outcome === `ok` || request.replayed) && + isPrefix(request) && + (request.options.limit ?? 0) >= (member.options.limit ?? 0), + ) + if (coveredByLaterPrefix) continue rejectAt( `ordered-source-loader-state-oracle.test.ts:1638`, new Error( - `held ${checkpoint}: request ${repair.index}, a successful repair prefix, was released before a later authoritative read succeeded`, + member === repair + ? `held ${checkpoint}: request ${repair.index}, a successful repair prefix, was released before a later authoritative read succeeded` + : `held ${checkpoint}: request ${member.index}, a successful acquisition of repair chain ${repair.index}, was released before a later authoritative read succeeded`, ), ) } @@ -1704,10 +1919,27 @@ async function checkAuthorityCase( joinedPending = false for (let round = 0; round < 40; round++) { // A release during the drain can start a truncate of its own. - if (truncatePending) settleReplay() + // A replay publishes only after every acquisition started inside its + // attempt settles (ARCHITECTURE.md, Replay participants), so the drain + // settles those first, as the real subscription waits for them. + const attempt = inflight().find( + (request) => request.index >= replayOwnedBefore, + ) + if (truncatePending && attempt) { + await settle(attempt, true) + checkHeld(`after the drain settles request ${attempt.index}`) + continue + } + if (truncatePending) { + settleReplay() + // Replay retirement can release leases that a later read in this + // drain covers, so the held law is checked at each drain event. + checkHeld(`after the drain's replay settles`) + } const next = inflight()[0] if (next) { await settle(next, true) + checkHeld(`after the drain settles request ${next.index}`) continue } const before = ledger.length @@ -1967,6 +2199,7 @@ async function checkAuthorityCase( } // A refetch delivered a row that sorts before every installed row. case `headInsert`: { + lastSourceInputAt = ledger.length // One `-Infinity` row at most: a second would tie with it, which // the fake's subtraction order cannot compare. const unexpressible = @@ -2059,6 +2292,7 @@ async function checkAuthorityCase( // An optimistic overlay hides the window's row, so the loader must // refill it from the source. case `optimisticDeparture`: + lastSourceInputAt = ledger.length optimisticDepartures++ loader.onSourceChanges( [{ type: `delete`, key: 1, value: { id: 1, rank: 1 } }], @@ -2069,6 +2303,7 @@ async function checkAuthorityCase( await flush() break case `sourceDelete`: + lastSourceInputAt = ledger.length repairOwed = true sourceDeletes++ loader.onSourceChanges( @@ -2416,6 +2651,8 @@ async function checkAuthorityCase( hungRequests, offsetWindows: testCase.offset > 0 && ledger.length > 0 ? 1 : 0, releaseInvalidations, + unblockedReleasePasses, + epochMovesWithContinuation, retirementSuccessorChains: ledger.filter( (request) => startsAuthority(request) && @@ -2565,9 +2802,10 @@ describe(`Ordered source request authority`, () => { // start error replaced the request's own error in its participant); // A superseded page that fails before a covering replay settles reaches // the failed-lease law through a replay, which the campaigns rarely do. - // Two fixed regressions keep traces that first failed the generated + // Four fixed regressions keep traces that first failed the generated // campaign's own model: a chain step it took for a chain start (an optimistic - // refill, and a shrunk window's prefix deferred by joined work). + // refill, a shrunk window's prefix deferred by joined work, and two refills + // deferred across a release pass during replay retirement). it.each([ { name: `a throwing release during a window move that resumes a repair`, @@ -2973,6 +3211,81 @@ describe(`Ordered source request authority`, () => { ], }, }, + // A release callback ran a graph pass during replay retirement while + // joined work deferred the repair's refill. The driver took that blocked + // pass for one that consumed the refill, so the refill that resumed later + // counted as a new repair start and its chain's own leases as a leak. + // CI random seed -1691316941; an on-demand source. + { + name: `a release pass during replay retirement while a refill is deferred`, + testCase: { + indexed: false, + limit: 1, + settledFirst: false, + releaseFault: false, + syncRepair: false, + ...ordinaryScenario, + joined: true, + releaseReenters: true, + releaseInvalidates: false, + history: [ + { type: `settle`, pick: 0, ok: true }, + { type: `report`, react: false }, + { type: `truncate` }, + { type: `move`, delta: -1 }, + { type: `joinedBusy` }, + { type: `settle`, pick: 0, ok: true }, + { type: `settle`, pick: 0, ok: true }, + { type: `settleNewest` }, + ], + }, + }, + // The same misclassification after a synchronous repair answer, from the + // 2026-11-03 coverage-map entry (CI run 41699469835). + { + name: `a release pass during replay retirement after a synchronous repair answer`, + testCase: { + indexed: false, + limit: 1, + settledFirst: true, + releaseFault: false, + syncRepair: true, + ...ordinaryScenario, + joined: true, + releaseReenters: true, + releaseInvalidates: false, + history: [ + { type: `truncate` }, + { type: `settle`, pick: 0, ok: true }, + { type: `invalidateThenFailOldest` }, + { type: `move`, delta: -1 }, + { type: `joinedBusy` }, + { type: `settle`, pick: 0, ok: true }, + ], + }, + }, + // A continuation of a repair chain resumed after its epoch moved and + // issued one more step of the obsolete chain; that step's settlement then + // started the replacement. Fixed seed 20261016 of the request-authority + // campaign found it once the no-stale-step law judged resumed requests. + { + name: `a staged repair step resumed after its epoch moved`, + testCase: { + indexed: true, + limit: 1, + settledFirst: false, + releaseFault: false, + syncRepair: true, + ...ordinaryScenario, + releaseInvalidates: false, + history: [ + { type: `settle`, pick: 0, ok: true }, + { type: `sourceDelete`, react: true }, + { type: `invalidateThenFailOldest` }, + { type: `settle`, pick: 0, ok: true }, + ], + }, + }, { // Without the settled check, a report before the first page settled // forced a full-source read. @@ -3024,46 +3337,91 @@ describe(`Ordered source request authority`, () => { // The broad grammar already generated the source trace. This directed // grammar makes its replay/continuation handoff frequent enough to measure, // while index-free prefix size, local rows, joined deferral, synchronous - // answers, and release-triggered truncation vary independently. Without - // joined deferral there is no held continuation; without the release truncate - // there is no replay bookkeeping to distinguish from a graph pass. - // `deferred-refill` needs a synchronous answer and a release-triggered - // truncate together: 6 of the 96 inputs. An eager source never reaches its - // adapter on release, so production cannot pair them; the campaign calibrates - // the driver's continuation provenance rather than a reachable product state. - // Random draws run twice the fixed count so that rare state stays above its - // minimum (expected 25 of 400). + // answers, release-triggered truncation, a graph pass inside each release + // callback, the truncate's place, and one or two provider answers vary + // independently. Without joined deferral there is no held continuation; + // without a truncate there is no replay bookkeeping to distinguish from a + // graph pass. A synchronous answer settles the repair prefix and issues its + // tie at once; an asynchronous one needs a second answer before joined work + // can defer the refill. A truncate before the repair hands the pre-truncate + // leases to replay retirement, so an on-demand source, whose release reaches + // the adapter, reaches `deferred-refill` and a release pass during it. + // Each declared state has a constructed history that fixes only the axes it + // needs. The campaign-local minima stay as they were. Random draws run twice + // the fixed count. const handoffProperty = `ordered-loader.replay-continuation` - const handoffCase = fc + const handoffResets = [ + `none` as const, + `before-repair` as const, + `before-settle` as const, + `after-settle` as const, + ] + type HandoffAxes = { + limit: 1 | 2 + snapshotRows: 1 | 3 + syncRepair: boolean + joined: boolean + releaseTruncates: boolean + releaseReenters: boolean + reset: (typeof handoffResets)[number] + answers: 1 | 2 + } + const handoffHistory = ({ + reset, + answers, + ...axes + }: HandoffAxes): AuthorityCase => ({ + ...ordinaryScenario, + indexed: false, + settledFirst: true, + releaseFault: false, + ...axes, + history: [ + { type: `settle`, pick: 0, ok: true }, + { type: `settle`, pick: 0, ok: true }, + { type: `report`, react: false }, + ...(reset === `before-repair` ? [{ type: `truncate` as const }] : []), + { type: `move`, delta: -1 }, + { type: `joinedBusy` }, + ...(reset === `before-settle` ? [{ type: `truncate` as const }] : []), + ...Array.from({ length: answers }, () => ({ + type: `settleNewest` as const, + })), + ...(reset === `after-settle` ? [{ type: `truncate` as const }] : []), + ], + }) + // The unmapper takes a history back to its axes, so constructed histories + // stay inside this grammar and shrink like generated ones. + const handoffAxes = (value: unknown): HandoffAxes => { + const candidate = value as AuthorityCase + for (const reset of handoffResets) + for (const answers of [1, 2] as const) { + const axes: HandoffAxes = { + limit: candidate.limit, + snapshotRows: candidate.snapshotRows, + syncRepair: candidate.syncRepair, + joined: candidate.joined, + releaseTruncates: candidate.releaseTruncates, + releaseReenters: candidate.releaseReenters, + reset, + answers, + } + if (isDeepStrictEqual(handoffHistory(axes), value)) return axes + } + throw new Error(`not a replay-continuation history`) + } + const handoffCase: fc.Arbitrary = fc .record({ limit: fc.constantFrom(1 as const, 2 as const), snapshotRows: fc.constantFrom(1 as const, 3 as const), syncRepair: fc.boolean(), joined: fc.boolean(), releaseTruncates: fc.boolean(), - reset: fc.constantFrom( - `none` as const, - `before-settle` as const, - `after-settle` as const, - ), + releaseReenters: fc.boolean(), + reset: fc.constantFrom(...handoffResets), + answers: fc.constantFrom(1 as const, 2 as const), }) - .map(({ reset, ...axes }): AuthorityCase => ({ - ...ordinaryScenario, - indexed: false, - settledFirst: true, - releaseFault: false, - ...axes, - history: [ - { type: `settle`, pick: 0, ok: true }, - { type: `settle`, pick: 0, ok: true }, - { type: `report`, react: false }, - { type: `move`, delta: -1 }, - { type: `joinedBusy` }, - ...(reset === `before-settle` ? [{ type: `truncate` as const }] : []), - { type: `settleNewest` }, - ...(reset === `after-settle` ? [{ type: `truncate` as const }] : []), - ], - })) + .map(handoffHistory, handoffAxes) describe(`preserves repair continuation identity across replay bookkeeping`, () => { // Campaign-local counters preserve the legacy history minima; fixed examples @@ -3073,12 +3431,59 @@ describe(`Ordered source request authority`, () => { let counts = new Map() let executed = 0 + // A release callback runs a graph pass while the repair's deferred + // refill may still be pending. The loader blocks refinement until its + // release pass unwinds, so that pass consumes nothing, and the refill + // that resumes later is still a step of the repair chain. An on-demand + // source reaches it: an explicit truncate before the repair hands the + // pre-truncate leases to replay retirement, and two asynchronous answers + // settle the repair prefix and its tie while joined work defers the + // refill. The release reaches the adapter, so this pairing is one that + // production can produce. + // `release-pass-continuation` counts the passes where the driver's + // provenance owes a continuation, which over-approximates a pending one, + // so it is measured only. `release-pass-refill-resumed` is the required + // state: production then resumed the pending refill on a later graph pass + // as a step of the same chain that reads a new demand. + const releasePassState = `release-pass-continuation` + const resumedState = `release-pass-refill-resumed` + // The pinned runner reads this object at execution. Keep the existing // fixed/random asymmetry without adding or widening a campaign. const histories = { arbitrary: handoffCase, runs: 400, fixedSeeds: [20261029], + states: [...states, resumedState], + measured: [releasePassState], + // Each builder keeps the generated limit, local rows, and release + // truncate, and fixes only the axes its states need. + constructed: [ + { + name: `a release pass during replay retirement while an on-demand refill is deferred`, + enters: [`deferred-refill`, resumedState], + build: (generated: AuthorityCase) => + handoffHistory({ + ...handoffAxes(generated), + syncRepair: false, + joined: true, + releaseReenters: true, + reset: `before-repair`, + answers: 2, + }), + }, + { + name: `a truncate after the repair's refill is deferred`, + enters: [`reset-continuation`], + build: (generated: AuthorityCase) => + handoffHistory({ + ...handoffAxes(generated), + joined: true, + reset: `after-settle`, + answers: 2, + }), + }, + ], } beforeEach(({ task }) => { counts = new Map(states.map((state) => [state, 0])) @@ -3107,7 +3512,7 @@ describe(`Ordered source request authority`, () => { law: { statement: `preserves repair continuation identity across replay bookkeeping`, authority: `query/live/ARCHITECTURE.md: Ordered requests, continuation, and recovery; Atomic window publication.`, - limits: `The existing request-ledger and receiving grammars retain their bounded laws and observation checkpoints; no coverage expansion.`, + limits: `One unindexed loader over a fake subscription, limit 1/2, offset 0, one fixed history shape around a deferred refill, and the request-ledger laws at their checkpoints. A loader that drops a deferred refill during a blocked pass fails only the constructed history's required reach, not a law; elsewhere in the grammar it passes (coverage map, ordered-loader authority, awaiting a maintainer decision).`, }, owns: [ 'src/collection/index.ts#createCollection', @@ -3119,8 +3524,9 @@ describe(`Ordered source request authority`, () => { histories: histories, model: (history, observations) => recordedComparison(history, observations), - driver: async (history, observe) => - observeComparison(history, observe, async () => { + driver: async (history, observe) => { + const reached = new Set() + await observeComparison(history, observe, async () => { executed++ const entered = new Set() const enter = (state: State) => { @@ -3136,8 +3542,18 @@ describe(`Ordered source request authority`, () => { await checkAuthorityCase(testCase, (state) => { if (state === `deferred-refill` || state === `reset-continuation`) enter(state) + if ( + state === `deferred-refill` || + state === `reset-continuation` || + state === releasePassState || + state === resumedState + ) + reached.add(state) }) - }), + }) + // The comparison's verdict is the first observation, so reach follows it. + for (const state of reached) observe(`reach`, state) + }, check: (_history, _observations, verdict) => verdict, }) }) @@ -3542,6 +3958,9 @@ describe(`Ordered source request authority`, () => { `retirement-with-retry-timer`, `retirement-with-later-chains`, `retirement-with-full-source-plan`, + // The ordering epoch moved while a repair continuation was owed: the + // premise of the no-obsolete-step law. + `continuation-before-epoch-move`, ] as const type State = (typeof states)[number] let counts = new Map() @@ -3554,6 +3973,8 @@ describe(`Ordered source request authority`, () => { let releaseFaults = 0 let syncRepairs = 0 let invalidatingPages = 0 + // Measured, not gated: graph passes in the stale self-release. + let unblockedReleasePasses = 0 let later = { unexpressibleBoundaries: 0, joinedDeferrals: 0, @@ -3589,6 +4010,7 @@ describe(`Ordered source request authority`, () => { releaseFaults = 0 syncRepairs = 0 invalidatingPages = 0 + unblockedReleasePasses = 0 later = { unexpressibleBoundaries: 0, joinedDeferrals: 0, @@ -3620,7 +4042,7 @@ describe(`Ordered source request authority`, () => { ) return process.stderr.write( - `${authorityProperty} ${task.name} ${JSON.stringify({ histories: executed, ...Object.fromEntries(counts) })}\n`, + `${authorityProperty} ${task.name} ${JSON.stringify({ histories: executed, ...Object.fromEntries(counts), unblockedReleasePasses })}\n`, ) if (oracleReplayRequested()) return for (const state of states) @@ -3700,6 +4122,8 @@ describe(`Ordered source request authority`, () => { if (observation.retirementSuccessorChains > 1) enter(`retirement-with-later-chains`) } + if (observation.epochMovesWithContinuation > 0) + enter(`continuation-before-epoch-move`) if (observation.requestErrorChecks > 0) { enter(`current-request-error`) if (observation.releaseFaults > 0) @@ -3714,6 +4138,7 @@ describe(`Ordered source request authority`, () => { releaseFaults += observation.releaseFaults syncRepairs += observation.syncRepairs invalidatingPages += observation.invalidatingPages + unblockedReleasePasses += observation.unblockedReleasePasses for (const key of Object.keys(later) as Array) { later[key] += observation[key] }