Convex: application writes, load outcome equivalence and obsolete replay work#

Starting head: 8c24922026fb4a714cb54b992ac85faa2e876742. The changes remain local. This record supplies the current source bindings for the files in its manifest. Earlier versioned records and frozen evidence remain unchanged. No new TLA+ execution or independent delegated review is claimed; the final review is a self-review under the oracle-review skill.

Law and authority#

The #2269 maintainer decision motivates these three additions. Collection mutation handlers in packages/db/src/types.ts, optimistic-history-oracle.ts, LoadSubsetFn, SyncAppliedReceipt and live-query architecture laws 7, 9 and 14 supply this checkout's receiving contracts. The task-local laws-before-edits.md records the rival predictions before implementation and before the composition repair.

1. A confirmed application operation reaches the backend and the source key is correct when its application promise settles. A rejected atomic backend operation changes neither source truth nor the final promised window. Independently authored remote operations remain visible on both sides.
2. A synchronous throw and a rejected load promise give equivalent failed-load public observations and subsequent recovery. Their acquisition leases have different lifetimes; raw unload/status-event schedules need not agree.
3. Without accepted writes, native cancellation cannot wait for an absent provider response. Late transport success/error cannot corrupt a later successful replay or resurrect rows it excludes. Accepted writes retain their existing application/cleanup obligations.

Version reconciliation is explicit. #2168 remained open at 2bc79fc7c416ac0e2d691c0b622f1364e4eb5c12; its types and this checkout still describe waiting for uncancelable baselines. The later maintainer comment ends core request bookkeeping on abort. This change exercises cancellable native preacceptance work, which satisfies both accounts. It does not relax the older receipt/replay models or claim the prospective immediate-core-publication law for an arbitrary adapter that ignores abort. That remains #2168 integration.

Scientific model and receiving boundaries#

LazyWriteModel holds authored rows and one optimistic operation. The ledger predicts backend truth independently of every backend read. Its publication relation combines a monotone source revision, a monotone requested window and the current optimistic operation. It keeps all compatible explanations when an operation hides source changes. Acknowledging backend work and dropping a local optimistic operation are distinguishable: a rejected delete can restore an older applied source while a newer remote edit still waits. Once the newer source is public, the older source cannot return. Pages, caches, queues and commit partitions never enter this model.

An initial flat list of optimistic/source windows rejected that legal restored view under held SDK notifications. The old/new predictions and authority were recorded before replacing that formulation. This was a model-scope gap, not a production-defect RED. The existing source-only version model remains unchanged. Comparator controls preserve lawful optimistic rollback and reject source rollback, atomic mixing, lost confirmations and leaked atomic rejections.

The real-backend receiver uses actual Collection insert/update/delete handlers, both SDKs and an independently queried backend. Every history has all six operation/outcome cells. Each handler is held before the server call and after its response; independent visible and unread rows change during its optimistic operation. The first insert overlaps larger demand and an actual held receipt. Later, real SDK caches advance while their notifications are withheld. The source-key comparison runs at application settlement before notifications are released. Every graph callback reaches the scientific publication relation; quiet checkpoints additionally require the exact latest window and backend. The server rejection throws after attempted edits, so remote rollback is real.

The outcome receiver uses the same generated replay history for throw/rejection and for direct/live-query observation. Failed replacement and ordinary later writes retain the old publication; retry succeeds with the original failure identity preserved. Adapter-owned partial resources are released before a throw; accepted acquisitions release on unload or cleanup.

The abort receiver uses both controlled native SDK shapes. It proves a response is still withheld, aborts before any native acceptance, observes rejection, then delivers with no demand and checks that no rows/receipts were accepted. A fresh graph then receives two same-run core truncate replays with disjoint source keys. Retired callbacks deliver both success and error after each replay. Every graph callback and every retained sync error is checked. The test driver supplies truncate through real controls; production Convex does not initiate it. Core may lawfully request a full-source repair, so this profile makes no bounded work claim. An early fixture permission was too narrow and was corrected; its rejection was a harness error, not product evidence.

Grammar, reach and validation#

The app grammar varies 12–16 initial rows, page sizes 2–3, growth from width two to 5–6, short text and all permutations of the five-cell suffix after confirmed insert. Each normal fixed/random campaign has four histories; both SDKs receive every history: sixteen backend episodes, 96 application operations. Every one of the fourteen declared reach states reaches four histories per campaign. The multiplier-three campaign reaches twelve histories per state per campaign: 48 SDK/backend episodes, 288 application operations.

The outcome grammar varies 1–4 rows, short text, partial/no failed writes and 1–4 rejection turns. Its normal campaigns each have thirty histories and four receivers per history: 240 direct/query/outcome episodes. The abort grammar varies 12–18 rows, page sizes 2–3, windows 2–4, short text and both stale callback and delivery orders; thirty histories per campaign, both SDKs: 120 episodes. Every declared state reaches thirty histories in each normal campaign. Their multiplier-three campaigns use ninety histories per campaign. Campaign helpers enforce nonzero reach and retain both SDK failures.

Reconstruction: minimal row/page/window forms reconstruct each captured shrink. The fixed constructive sequences guarantee failure/retry, cancellation/replay and all write outcomes; the generators vary the relevant neighboring values and orders. Ablations lose independent distinctions: no ledger permits shared lost writes, no rejection loses rollback, no notification hold loses exact settlement, no growth loses held acquisition, no partial failed write loses unauthorized publication, and no disjoint replay loses stale-key resurrection. Nearby invalid histories include overlapping app operations, local settlement before backend acknowledgment and publication without any authored source/optimistic explanation.

Final commands/results are preserved in the frozen evidence directory. The package suite, full backend regression suite, deeper new campaigns, TypeScript, ESLint, oracle lint and diff checks are the validation boundaries. Individual runner cases are not counted as independent oracle owners.

Calibration and direct replay#

All correct production sources passed before calibration; no product-defect RED or production repair is claimed. The calibration script saves the current bytes, applies one semantic mutant, shrinks/replays the failure, restores the exact bytes in finally, verifies the hash, and reruns the direct replay GREEN. Backend calibrations run serially against isolated local deployments.

The first three are production-decision mutants. The fourth is a hostile driver behavior at the actual write boundary. Each failure is a semantic assertion, not a timeout/setup failure. Permanent model controls separately challenge the publication and two-sided comparisons. Calibration JSON records commands, source hashes, exit codes and checked replay paths.

Run from packages/convex-db-collection using the installed Vitest binary or pnpm --config.verify-deps-before-run=warn exec vitest. That command option avoids an automatic reinstall of the existing local dependency workaround. Normal selectors are CONVEX_LAZY_APP_ORACLE_SEED/PATH, CONVEX_LOAD_OUTCOME_ORACLE_SEED/PATH and CONVEX_ABORT_REPLAY_ORACLE_SEED/PATH. Backend commands additionally set CONVEX_TEST_BACKEND_VERSION=precompiled-2026-10-10-72ce13c.

Self-review against the oracle guide#

Limits: one app operation at a time, unique ascending finite ranks, bounded strings, one source, finite responsive schedules. Rich values/schema variation, reload/snapshot/resume and new health APIs retain their existing/deferred owners. Initial-load outcome equivalence and arbitrary callback reentry remain with the core lifecycle owners. No arbitrary nonquiescent temporal progress, real SDK adversarial-callback emission or immediate core cancellation of uncooperative work is established. Generalized field/backend normalization and the public cross-adapter kit remain outside this change.