Fence unsettled runs by recorded provider subject across auth locators (model + production replay)

.github/workflows/ci.yml

@@ -289,7 +289,7 @@ jobs:
   quint:
     name: quint ${{ matrix.shard }}/4
     runs-on: ubuntu-latest
-    timeout-minutes: 25
+    timeout-minutes: 35
     strategy:
       fail-fast: false
       matrix:
@@ -331,7 +331,7 @@ jobs:
       # over the models scripts/verification-tools.ts assigns to this shard.
       # Every model runs in exactly one shard; the shard packing is tested.
       - run: bun run ./scripts/verification-tools.ts quint ${{ matrix.shard }} 4
-        timeout-minutes: 20
+        timeout-minutes: 30
       - name: Retain checker output
         if: always()
         uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1

AGENTS.md

@@ -109,7 +109,7 @@
 
 - `costs.json` at the repository root is the checked registry of every product data surface: store, kind (`authoritative` | `derived` | `telemetry` | `served`), retention class (`ephemeral` | `ttl:<ISO-8601>` | `account` | `tombstone` | `persistent`), owner module, and budget. A new table, bucket, stream, dynamic route, blob, or provider meter fails `check:cost-surfaces` until it registers.
 - Bound every input before storage or provider I/O: request bytes, row counts, page sizes, batch sizes, retry counts, and event payloads. Unbounded input is a contract violation.
-- No writes on read paths. Reads may cache; they never mutate. Hand a read path a read capability with no writer members, such as `AuthIncarnationReader`, not an environment that reaches writers. The menu-bar snapshot and its account and permission listings take no admission and create no state; account saves, the control-service startup backfill, and admitted execution paths create auth incarnations. The auth checks of a cache read, a live-read publication, and an omni materialization read the incarnation through `AuthIncarnationReader`, so a missing incarnation reads as changed and nothing is created. Read-path preparation (capability and omni reads, cache-only invocations, and control-plane inspection), confirmation preparation, and the operation-permission account identity bind the current incarnation the same way: they read it through `AuthIncarnationReader`, fail closed when it is missing, and create none. Only explicit invocation preparation, an admitted execution path, may create a missing incarnation. Two bounded exemptions (D14). First, a read-projection cache read may create and release its own admission claim and remove a claim whose recorded owner is proven dead, because it must exclude a concurrent projection transition; the claim is coordination state with no data. Second, a cache read may create the projection encryption key and its store-key marker when they are absent, because a miss returns the query key that this encryption key derives; each is created at most once per state home and holds no user data. The exemptions cover nothing else.
+- No writes on read paths. Reads may cache; they never mutate. Hand a read path a read capability with no writer members, such as `AuthIncarnationReader`, not an environment that reaches writers. The menu-bar snapshot and its account and permission listings take no admission and create no state; account saves, the control-service startup backfill, and admitted execution paths create auth incarnations. The auth checks of a cache read, a live-read publication, and an omni materialization read the incarnation through `AuthIncarnationReader`, so a missing incarnation reads as changed and nothing is created. Read-path preparation (capability and omni reads, cache-only invocations, and control-plane inspection), confirmation preparation, and the operation-permission account identity bind the current incarnation the same way: they read it through `AuthIncarnationReader`, fail closed when it is missing, and create none. Only explicit invocation preparation, an admitted execution path, may create a missing incarnation. `invoke --projection-identity-only` is the SDK's identity preflight for a live invoke, so it is execution preparation and remains an admitted creator; `invoke --cache-only` is a read path and creates none. Two bounded exemptions (D14). First, a read-projection cache read may create and release its own admission claim and remove a claim whose recorded owner is proven dead, because it must exclude a concurrent projection transition; the claim is coordination state with no data. Second, a cache read may create the projection encryption key and its store-key marker when they are absent, because a miss returns the query key that this encryption key derives; each is created at most once per state home and holds no user data. The exemptions cover nothing else.
 - `repair-signals` is a bounded derived diagnostic cache, not execution authority or an audit log. Keep failed-invocation signals free of account identifiers, inputs, private content, and raw errors. Catalog/check/cache-only/identity-only inspection must not record demand. Repair handoffs never authorize capture, retry, activation, or publication; changed contracts remain unverified candidates.
 - Derived state is rebuildable and lives in the cheapest tier that can serve it. Only authoritative state pays for transactional storage.
 - Every mutation carries an idempotency key; a retried write never double-charges storage, quota, or provider spend.

docs/assurance.md

@@ -8,14 +8,14 @@ A claim is *evidenced* when its layer runs in CI, *planned* when a plan phase sc
 
 ## Summary
 
-The register holds 245 claims: 222 evidenced, 4 planned, and 19 not verified. It maps 90 guidelines from 5 guides; 70 list claims and 20 are exempt.
+The register holds 246 claims: 223 evidenced, 4 planned, and 19 not verified. It maps 90 guidelines from 5 guides; 70 list claims and 20 are exempt.
 
 | Layer | Evidenced | Planned | Not verified |
 | --- | ---: | ---: | ---: |
 | example test | 146 | 1 | 0 |
 | property test | 20 | 1 | 0 |
 | stateful model | 24 | 0 | 0 |
-| Quint model with production trace replay | 20 | 2 | 0 |
+| Quint model with production trace replay | 21 | 2 | 0 |
 | Lean proof with differential test | 8 | 0 | 0 |
 | differential oracle | 4 | 0 | 0 |
 | configuration readback | 0 | 0 | 15 |
@@ -107,8 +107,8 @@ Each claim holds only while its listed assumptions hold.
 | --- | --- | ---: |
 | `bun-runtime` | Bun and JavaScriptCore execute the sources and the test runner as specified. | 8 |
 | `filesystem-atomic-rename` | Same-volume rename and link are atomic. | 33 |
-| `filesystem-durability` | Data and directory entries that were fsynced persist across a crash or power loss. | 30 |
-| `same-user-trusted` | Processes running as the same operating-system user are trusted; file modes and owner-only sockets separate users. | 32 |
+| `filesystem-durability` | Data and directory entries that were fsynced persist across a crash or power loss. | 31 |
+| `same-user-trusted` | Processes running as the same operating-system user are trusted; file modes and owner-only sockets separate users. | 33 |
 | `process-liveness` | Process ID, process start time, and boot identity readings are truthful. | 10 |
 | `monotonic-clock` | The injected monotonic clock never runs backward. | 6 |
 | `whatwg-url` | Bun's URL parser implements the WHATWG URL Standard. | 13 |
@@ -1130,7 +1130,7 @@ The messaging automation protocol rejects a second ordinary in-flight request an
 - Assumptions: `filesystem-durability`, `provider-behaviour`
 - Not verified: Only the enumerated example cases are checked.
 
-### `mutations` (11 claims)
+### `mutations` (12 claims)
 
 #### `mutation-exact-preview-confirmation`
 
@@ -1281,6 +1281,20 @@ The confirmed-write public boundary preserves the exact selected rejection value
 - Assumptions: `filesystem-durability`, `provider-behaviour`
 - Not verified: Only the enumerated example cases are checked.
 
+#### `intent-fence-subject-across-locators`
+
+New run journals record the provider subject their auth record named; before dispatch, the confirmed-write fence also refuses while an unsettled run of the same provider target, operation, canonical input, and duplicate-risk source recorded the same subject under a different auth locator, both in its journal scan and in a recheck after its own claim is on record. Journals without a subject keep the per-locator fence and stay valid.
+
+- Evidenced by Quint model with production trace replay.
+- Source: `docs/effect-confirmed-write-runtime.md`: “the fence also refuses while an unsettled run of the same provider target, operation, and canonical input”
+- Evidence: `scripts/verification-fence-replay.test.ts`, `src/confirmed-write-intent-fence.test.ts`, `src/run-journal.test.ts`, `verification/quint/fence.qnt`
+- Assumptions: `filesystem-durability`, `same-user-trusted`
+- Not verified:
+  - Subjects are compared as strings. The operator may type a subject, so two locators that record one subject are fenced as one account even when they are not; this only refuses more. Two locators of one account with no recorded subject, or a run recorded before journals kept the subject, are not fenced against each other.
+  - Two runs that race past their scans may both refuse at the recheck; neither dispatches, and each is retried after the other settles. No progress law is checked.
+  - The fence model has two locators, one subject, three runs, 5,000 simulated samples of up to 12 steps, and Apalache to length 8; the replay drives the subject scan and recheck through the pure fence cores and a five-trace file-backed cover, not the `confirmInvocation` program, which the listed example tests cover.
+  - A succeeded run under another locator neither fences nor replays across locators, by design.
+
 ### `npm` (17 claims)
 
 #### `npm-publish-after-canonical-only`

docs/effect-confirmed-write-runtime.md

@@ -35,10 +35,25 @@ The fence scans run journals before its exclusive create under
 `idempotency/intents`, so a run recorded before the fence existed still blocks.
 
 The realm is the locator ID, not the provider account, because the verified
-subject is optional and journals do not record it. Three limits follow:
-
-- The same account connected under a second locator ID is a different intent
-  and is not fenced against the first locator's runs.
+subject is optional. New run journals record the provider subject their auth
+record named, as an optional `authSubject`; journals written before this field
+existed carry none and stay valid. Before dispatch, the fence also refuses
+while an unsettled run of the same provider target, operation, and canonical
+input (and the same elected duplicate-risk source) recorded the same subject
+under a different locator ID. It checks this in its journal scan and again
+once the run's own intent claim is on record, just before the dispatch
+boundary, so two locators racing past the scan cannot both dispatch; both may
+refuse, and each is then retried after the other settles. The refusal names
+the other locator, where the blocking run is inspected and reconciled.
+Subjects may be typed by the operator, so two locators that record one subject
+are treated as one account even when they are not: the cross-locator fence can
+only refuse more, never less. Three limits follow:
+
+- The same account connected under a second locator ID with no recorded
+  subject on either side, or a run recorded before journals kept the subject,
+  is a different intent and is not fenced against the first locator's runs. A
+  succeeded run under another locator does not fence or replay: its receipt
+  belongs to that locator.
 - A fulfilled run whose auth record differs from the current one (a reconnect
   with new settings, or `--force` onto another account) is not replayed as the
   current account's result. Confirmation refuses until the dedupe window ends

kb/plans/formal-verification-assurance.md

@@ -97,7 +97,7 @@ web gateway, the Edge middleware, media, release, and CI on `origin/main`
 | D11 | Media | `assertOwned` observes the lock but does not fence the promotion `rename`. Media-lock liveness trusts `kill(pid, 0)` over heartbeat age, which breaks on shared or namespaced filesystems. | code-read |
 | D12 | Edge | The direct `.md` branch calls `retrieve(new URL(url.pathname, url.origin))` (`edge/negotiation.ts:257`), so `//evil.example/x.md` resolves off-origin in-process. The live site is not affected: Vercel returns 308 to a single slash before middleware, and `/\` returns 404 (checked 2026-09-23). The code still violates same-origin retrieval if the platform changes. | reproduced in-process; latent live |
 | D13 | Approvals | Allow-once is enforced by the client. The broker leaves an `allowed` entry checkable for 600 s and relies on the Ghostget process calling `releaseApproval` in `finally`. A crash leaves a reusable lease for same-UID callers. | code-read |
-| D14 | Read paths | The menu-bar snapshot creates incarnation files through `ensureIncarnationUnderAdmission`, and read-projection listings unlink orphaned claims. Both break the literal rule "No writes on read paths". Either the rule gets an explicit, bounded exemption or the writes move. Done: #355 made the snapshot read-only, #371 moved the cache-read and omni auth checks to `AuthIncarnationReader` and recorded the two exemptions, and the residual-incarnation change binds read-path preparation, confirmation preparation, and the permission account identity the same way. Explicit invocation preparation remains the admitted creator. | code-confirmed; fixed |
+| D14 | Read paths | The menu-bar snapshot creates incarnation files through `ensureIncarnationUnderAdmission`, and read-projection listings unlink orphaned claims. Both break the literal rule "No writes on read paths". Either the rule gets an explicit, bounded exemption or the writes move. Done: #355 made the snapshot read-only, #371 moved the cache-read and omni auth checks to `AuthIncarnationReader` and recorded the two exemptions, and the residual-incarnation change binds read-path preparation, confirmation preparation, and the permission account identity the same way. Explicit invocation preparation remains the admitted creator. Owner decision (delegated): `invoke --projection-identity-only` is the SDK's identity preflight for a live invoke, so it is execution preparation and stays an admitted creator; `src/read-path-preparation.test.ts` pins that it creates a missing incarnation while `invoke --cache-only` creates none. | code-confirmed; fixed |
 | D15 | Release | Manual promotion refuses a Release that an intermediate attempt published. When a failed-jobs rerun publishes bytes an earlier attempt attested, the body names that earlier attempt. A later rerun of all jobs then fails its publish job, and `resolveReleaseAuthority` reads only the latest attempt and the receipt attempt, neither of which proved all four canonical jobs. Found by a strengthened `promotionNotBlocked` over `verification/quint/release.qnt` (attempts: publish fails, rerun failed jobs publishes, rerun all) and reproduced against `resolveReleaseAuthority` with the release replay fixtures. Fixed: when the receipt attempt attested but did not publish, manual recovery and the canonical download read at most three exact intermediate attempts, each through its own attempt record and job inventory, and the model's `promotionNotBlocked` now names any publishing attempt (mutant `stepD15`). | reproduced, fixed |
 | D16 | Release | A stable Release that completes out of band during publication is hidden. `publishCanonicalRelease` ran the completed-Release census before the PATCH but not after it, so a higher Release completed between that census and the PATCH (GitHub has no conditional publish) let the PATCH make the older target Latest and the run report success. Found by the stateful publisher model in `scripts/github-release-publish-model.test.ts` (shrunk to `Publish(R1, concurrent-higher at main read 7)`). Fixed: the census repeats after the terminal authority proof, and on an already-published target, so such a run fails closed; the immutable publication itself cannot be undone. | reproduced, fixed |
 | D17 | Release | Pending stable Release runs could be cancelled. GitHub keeps one running and one pending run per concurrency group and cancels the pending run when a third arrives, so a tag pushed while two runs were queued never published. Fixed: the `stable-release` group sets `queue: max`, which queues up to 100 pending runs in order. | code-read, fixed |
@@ -219,7 +219,7 @@ and passes after the fix, and `Required` passes.
 | Reconcile across a reauth | Done: web-session and portable reconcile and web duplicate-successor election accept a reconnect that keeps the locator, kind, and recorded subject. Capsules with no subject still need the exact record. |
 | Portable readback protocol | Done (claim `portable-retained-release`, `verification/quint/retained.qnt`). The owner chose an optional versioned readback: a write declares `readback: {version: 1, operation, contractVersion}`, protocol 2 carries only the `host.readback` and `plugin.readback.result` frames, and protocol 1 stays accepted. Ghostget invokes the readback itself, bound to the run, intent, auth realm, and manifest, and only its observed `not-applied` releases the fence. Undeclared plugins keep the explicit-input path. Still open: no owner-approval route reaches portable reconciliation. |
 | Duplicate successors for portable runs | Done (claim `portable-retained-release`). Portable writes elect duplicate-risk successors under the web path's rules. Once the successor settles, the source's journal records `supersededBy`, which releases its recovery material and assets so the bundle is quiescent; its ledger stays indeterminate. Supersession runs at plugin install, disable, and removal and in the doctor repair pass. |
-| Fence keyed by subject across locators | Open: run journals do not record the subject, so this needs a journal schema change. |
+| Fence keyed by subject across locators | Done: new run journals record an optional, strictly parsed `authSubject`; before dispatch the fence also refuses while an unsettled run of the same target, operation, input, and source recorded the same subject under another locator, at its scan and again after its claim. Journals without a subject keep the per-locator fence. Operator-typed subjects can only over-block. `fence.qnt` gained a locator and subject dimension and the `stepSubjectBlind` mutant, claim `intent-fence-subject-across-locators`. |
 
 ### Phase 2: test infrastructure
 

scripts/ci-pr-gate.test.ts

@@ -183,7 +183,7 @@ describe("complete local and release check composition", () => {
       standalone: ["standalone", "ubuntu-latest", 20],
       macos: ["macOS", "macos-15", 45],
       verification: ["verification", "ubuntu-latest", 30],
-      quint: [`quint \${{ matrix.shard }}/${String(QUINT_CI_SHARD_COUNT)}`, "ubuntu-latest", 25],
+      quint: [`quint \${{ matrix.shard }}/${String(QUINT_CI_SHARD_COUNT)}`, "ubuntu-latest", 35],
     } as const;
     const shardList = (count: number): number[] => Array.from({ length: count }, (_, index) => index + 1);
     const expectedNode = {