diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 43a582d4..c8704535 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/AGENTS.md b/AGENTS.md index 521281a7..a1973ddb 100644 --- a/AGENTS.md +++ b/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:` | `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. diff --git a/docs/assurance.md b/docs/assurance.md index d9f3d38c..417847e6 100644 --- a/docs/assurance.md +++ b/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` diff --git a/docs/effect-confirmed-write-runtime.md b/docs/effect-confirmed-write-runtime.md index d54fda67..70939817 100644 --- a/docs/effect-confirmed-write-runtime.md +++ b/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 diff --git a/kb/plans/formal-verification-assurance.md b/kb/plans/formal-verification-assurance.md index 17102aac..c8df46f6 100644 --- a/kb/plans/formal-verification-assurance.md +++ b/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 diff --git a/scripts/ci-pr-gate.test.ts b/scripts/ci-pr-gate.test.ts index fb3eb207..3ca366c3 100644 --- a/scripts/ci-pr-gate.test.ts +++ b/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 = { diff --git a/scripts/npm-release-workflow.test.ts b/scripts/npm-release-workflow.test.ts index 7e330075..a71c6ce9 100644 --- a/scripts/npm-release-workflow.test.ts +++ b/scripts/npm-release-workflow.test.ts @@ -1219,7 +1219,7 @@ describe("npm publication contract", () => { (MAX_UNPACKED_BYTES + MAX_PACKED_ENTRIES * 1_023 + 1_024) / 512, ) * 512, ); - expect(MAX_PACKAGE_TAR_BYTES).toBe(24_138_752); + expect(MAX_PACKAGE_TAR_BYTES).toBe(24_146_432); expect(MAX_PACKAGE_TAR_BYTES % 512).toBe(0); expect(artifact).toContain("maxOutputLength: MAX_PACKAGE_TAR_BYTES"); expect(artifact).not.toContain("const maximumTarBytes"); @@ -1291,7 +1291,7 @@ describe("npm publication contract", () => { expect(timeoutValues(standaloneJob)).toEqual([20]); expect(timeoutValues(macosJob)).toEqual([45]); expect(timeoutValues(verificationJob)).toEqual([30]); - expect(timeoutValues(quintJob)).toEqual([25]); + expect(timeoutValues(quintJob)).toEqual([35]); expect(timeoutValues(requiredJob)).toEqual([5]); expect(staticJob.match(/^ - run: bun run check:static$/gmu) ?? []).toHaveLength(1); expect(packageJob.match(/^ - run: bun run check:package$/gmu) ?? []).toHaveLength(1); @@ -1420,13 +1420,13 @@ describe("npm publication contract", () => { expect(budget).toContain("47c0114ba631b314fa5bea489eb79e29a77bb7e06321c4088725b6b238dfe81a"); expect(Object.isFrozen(repairPackageMeasurement)).toBeTrue(); expect(repairPackageMeasurement).toMatchObject({ - archiveSha256: "c26ae0f505f5875d10d2fe95ec5ca210545c4ed5bd7a3f7db4ad36a047e388fa", - packedBytes: 12_017_867, unpackedBytes: 23_526_405, entryCount: 597, + archiveSha256: "3666bc04d8100fe00e1f7805404ee0851efcdc4b62806749b5e4b6ab65f68798", + packedBytes: 12_019_445, unpackedBytes: 23_534_110, entryCount: 597, packedPlatformProjection: 12_387, packedPortabilityAllowance: 4_096, payloadPlatformProjection: 353, payloadAllowance: 65, }); - expect(MAX_PACKED_BYTES).toBe(12_034_350); - expect(MAX_PACKED_BYTES).toBe(12_017_867 + 12_387 + 4_096); + expect(MAX_PACKED_BYTES).toBe(12_035_928); + expect(MAX_PACKED_BYTES).toBe(12_019_445 + 12_387 + 4_096); expect(budget).toContain("12,004,806 + 12,387 + 4,096 ="); expect(budget).toContain("12,003,367 + 12,387 + 4,096 ="); expect(budget).toContain("23,462,195 + 353 + 65 = 23,462,613"); @@ -1541,7 +1541,7 @@ describe("npm publication contract", () => { expect(budget).toContain("23,029,751 + 353 + 65 = 23,030,169"); expect(budget).toContain("23,193,728 + 65 = 23,193,793"); expect(budget).toContain("47684b3e2eb5cf3ed07fbb520aade8c7251d993f75262fbf1af627d9081a1a5f"); - expect(MAX_UNPACKED_BYTES).toBe(23_526_823); + expect(MAX_UNPACKED_BYTES).toBe(23_534_528); expect(budget).toContain("23,037,873 + 65 = 23,037,938"); expect(budget).toContain("f9f3ab38a682690ceaa2699a7309997512030f0fa500a9dc29dcd108123dc41f"); expect(budget).toContain("23,038,557 + 65 = 23,038,622"); @@ -1574,7 +1574,7 @@ describe("npm publication contract", () => { expect(budget).toContain("01875f12ab73a49d6c7d6bf520dc3d318db816addee2fa7981889f35c958cf7c"); expect(budget).toContain("b12909f08f7c19460ced56e30619f4860a1183f4b0106170c07837dae577a937"); expect(budget).toContain("0b212ac291218528dcf979370110a36f10850e046ca90a536057d9a44e807d1d"); - expect(MAX_UNPACKED_BYTES).toBe(23_526_405 + 353 + 65); + expect(MAX_UNPACKED_BYTES).toBe(23_534_110 + 353 + 65); expect(budget).toContain("22,794,052 + 65 = 22,794,117"); expect(budget).toContain("c482efe748f880e3717727d6d39fd92a68953e6eea766642b329ba47ae772d80"); expect(budget).toContain("22,759,423 + 65 = 22,759,488"); @@ -1610,8 +1610,8 @@ describe("npm publication contract", () => { expect(packageArtifactBudget).toEqual({ entryCount: { min: 597, max: 597 }, fileCount: { min: 597, max: 597 }, - packedBytes: { min: 1_600_000, max: 12_034_350 }, - unpackedBytes: { min: 9_000_000, max: 23_526_823 }, + packedBytes: { min: 1_600_000, max: 12_035_928 }, + unpackedBytes: { min: 9_000_000, max: 23_534_528 }, }); }); diff --git a/scripts/package-budget.ts b/scripts/package-budget.ts index e0f0395f..c5cce186 100644 --- a/scripts/package-budget.ts +++ b/scripts/package-budget.ts @@ -1709,20 +1709,23 @@ // // The portable retained readback and successor handling add the portable // provider host/runtime support, the retained readback and supersession -// cores, and their tests. Merging both: a clean `npm pack --ignore-scripts` -// with npm 11.19.0 on darwin arm64 measured 12,017,867 packed bytes and -// 23,526,405 unpacked bytes across the 597-file inventory; archive SHA-256 -// c26ae0f505f5875d10d2fe95ec5ca210545c4ed5bd7a3f7db4ad36a047e388fa. -// Carry the same projections and allowances: 12,017,867 + 12,387 + 4,096 = -// 12,034,350 packed; 23,526,405 + 353 + 65 = 23,526,823 unpacked. +// cores, and their tests, the public-address classification and vectors, and +// the subject-keyed confirmed-write fence's authSubject, cross-locator scan, +// and post-claim recheck. Merging all lanes: a clean `npm pack +// --ignore-scripts` with npm 11.19.0 on darwin arm64 measured 12,019,445 +// packed bytes and 23,534,110 unpacked bytes across the 597-file inventory; +// archive SHA-256 +// 3666bc04d8100fe00e1f7805404ee0851efcdc4b62806749b5e4b6ab65f68798. +// Carry the same projections and allowances: 12,019,445 + 12,387 + 4,096 = +// 12,035,928 packed; 23,534,110 + 353 + 65 = 23,534,528 unpacked. export const repairPackageMeasurement = Object.freeze({ scope: "Release and publication claims evidenced in CI", command: "npm pack --ignore-scripts", npmVersion: "11.19.0", platform: "darwin-arm64", - archiveSha256: "c26ae0f505f5875d10d2fe95ec5ca210545c4ed5bd7a3f7db4ad36a047e388fa", - packedBytes: 12_017_867, - unpackedBytes: 23_526_405, + archiveSha256: "3666bc04d8100fe00e1f7805404ee0851efcdc4b62806749b5e4b6ab65f68798", + packedBytes: 12_019_445, + unpackedBytes: 23_534_110, entryCount: 597, packedPlatformProjection: 12_387, packedPortabilityAllowance: 4_096, diff --git a/scripts/verification-fence-replay.test.ts b/scripts/verification-fence-replay.test.ts index 34ff1104..7f667418 100644 --- a/scripts/verification-fence-replay.test.ts +++ b/scripts/verification-fence-replay.test.ts @@ -55,13 +55,16 @@ import { import { acquireConfirmedWriteLedgers, confirmedWriteLedgerPath, + duplicateSourceSupersession, intentFenceBlocker, intentLedgerPath, readRunReceipt, + recheckConfirmedWriteSubjectFence, reconciledRecoveryRelease, releaseReconciledRunRecovery, repairInterruptedRunJournals, runJournalLedgerEntry, + subjectFenceBlocker, } from "../src/runtime.js"; import { ghostgetStateHome, writePrivateJsonIfUnchanged } from "../src/storage.js"; import { @@ -82,13 +85,17 @@ const RUNS = ["r1", "r2", "r3"] as const; const OUTCOMES = ["succeeded", "applied", "lost"] as const; const TRACE_VARIABLES = [ "applied", "authGen", "claimed", "dispatched", "elected", "ledger", "ledgerState", "mbt::actionTaken", - "mbt::nondetPicks", "phase", "reconciled", "result", "rev", "runAuth", "runRev", "scanned", "source", "status", + "mbt::nondetPicks", "phase", "reconciled", "result", "rev", "runAuth", "runLoc", "runRev", "runSubj", "scanned", + "source", "status", ].sort(); +const LOCATORS = ["a", "b"] as const; +// "" is a run whose auth record named no provider subject. +const SUBJECTS = ["", "s"] as const; const ACTIONS = [ "scan", "scanSuccessor", "claim", "dispatch", "finish", "reconnect", "upgrade", "reconcile", "claimNotApplied", ] as const; type Action = (typeof ACTIONS)[number]; -const MUTANT_STEPS = ["stepHashKeyed", "stepCallerRelease", "stepUnelected", "stepElectInFlight"] as const; +const MUTANT_STEPS = ["stepHashKeyed", "stepCallerRelease", "stepUnelected", "stepElectInFlight", "stepSubjectBlind"] as const; const RUN_IDS: Readonly> = Object.freeze({ r1: "11111111-1111-4111-8111-111111111111", @@ -97,7 +104,9 @@ const RUN_IDS: Readonly> = Object.freeze({ }); const RUN_LABELS: ReadonlyMap = new Map(Object.entries(RUN_IDS).map(([label, id]) => [id, label])); const ADAPTER_ID = "fence-provider"; -const AUTH_ID = "fence-main"; +// Each model locator is one auth locator ID; both may record one subject. +const AUTH_IDS: Readonly> = Object.freeze({ a: "fence-main", b: "fence-second" }); +const SUBJECT_IDS: Readonly> = Object.freeze({ s: "1234567890" }); // Duplicate-risk successors exist only for one-dispatch authenticated-session // posts.publish writes, so every replayed run is one. const OPERATION = "posts.publish"; @@ -125,6 +134,8 @@ type Snapshot = Readonly<{ ledgerState: ReadonlyMap; runAuth: ReadonlyMap; runRev: ReadonlyMap; + runLoc: ReadonlyMap; + runSubj: ReadonlyMap; source: ReadonlyMap; elected: ReadonlyMap; authGen: number; @@ -159,10 +170,35 @@ function labelOf(runId: string): string { return label; } -/** Classify the confirmed-write program's decision for a blocked confirm. */ +/** The model locator of a journal's auth locator ID, including the hash-keyed defect's per-generation IDs. */ +function locatorOf(journal: RunJournal): string { + for (const locator of LOCATORS) { + const id = AUTH_IDS[locator]!; + if (journal.auth.id === id || journal.auth.id.startsWith(`${id}-`)) return locator; + } + throw new Error(`auth locator ${journal.auth.id} is not a replayed locator`); +} + +/** The model subject a journal recorded: "" for none. */ +function subjectOf(journal: RunJournal): string { + if (journal.authSubject === undefined) return ""; + const found = Object.entries(SUBJECT_IDS).find(([, id]) => id === journal.authSubject); + if (found === undefined) throw new Error(`auth subject ${journal.authSubject} is not a replayed subject`); + return found[0]; +} + +const SUBJECT_REFUSAL = /^a prior attempt \([0-9a-f-]{36}\) may have reached the provider under auth locator '[a-z0-9-]+', which records the same provider subject as '[a-z0-9-]+';/u; + +/** + * Classify the confirmed-write program's decision for a blocked confirm. A + * refusal because another locator's unsettled run recorded the same subject + * counts as a refusal; the model does not tell the two apart before the + * claim. + */ function blockedResult(disposition: ReturnType): string { if (disposition.kind === "replay") return "replayed"; if (/^a prior attempt \([0-9a-f-]{36}\) may have reached the provider;/u.test(disposition.message)) return "refused"; + if (SUBJECT_REFUSAL.test(disposition.message)) return "refused"; if (/^a prior run \([0-9a-f-]{36}\) already fulfilled this intent under a different auth record/u.test(disposition.message)) { return "withheld"; } @@ -184,7 +220,10 @@ function electable(journal: RunJournal | undefined): journal is RunJournal { type Claim = | Readonly<{ acquired: true; ledgerRelativePath: string }> - | Readonly<{ acquired: false; existing: LedgerEntry }>; + | Readonly<{ acquired: false; existing: LedgerEntry; viaSubject?: { readonly authId: string } }>; + +/** A subject-fence recheck's blocker, as `recheckConfirmedWriteSubjectFence` returns it. */ +type SubjectBlock = Readonly<{ existing: LedgerEntry; viaIntent: true; viaSubject: { readonly authId: string } }>; /** Where a world keeps its journals and ledgers. */ interface FenceStore { @@ -195,6 +234,10 @@ interface FenceStore { create(journal: RunJournal): void; record(runId: string, event: RunJournalEvent): void; claim(journal: RunJournal, intent: ConfirmedWriteIntent, entry: LedgerEntry, at: Date): Claim; + /** The provider-subject recheck a claimed run makes before its dispatch boundary. */ + recheck(intent: ConfirmedWriteIntent, runId: string): SubjectBlock | null; + /** Project a run refused after its claim, which drops its intent ledger. */ + project(runId: string): void; /** A dispatch whose outcome never arrives. */ lose(runId: string, at: Date): void; settle(runId: string, at: Date): void; @@ -246,6 +289,18 @@ class MemoryStore implements FenceStore { return { acquired: true, ledgerRelativePath: `idempotency/${bucket.slice(0, 2)}/${bucket}.json` }; } + recheck(intent: ConfirmedWriteIntent, runId: string): SubjectBlock | null { + const blocker = subjectFenceBlocker(this.list(), intent, runId); + return blocker === null + ? null + : { existing: runJournalLedgerEntry(blocker), viaIntent: true, viaSubject: { authId: blocker.auth.id } }; + } + + project(runId: string): void { + // projectRunJournalIntent removes a released run's intent ledger. + if (this.get(runId)?.ledgerState === "released") this.release(runId); + } + lose(runId: string, at: Date): void { this.record(runId, { type: "finished", status: "indeterminate", finalOrigin: null, @@ -265,7 +320,16 @@ class MemoryStore implements FenceStore { return { holders: new Set(this.ledger.values()), names: this.ledger.size }; } - afterStep(): void {} + afterStep(at: Date): void { + // The durable repair pass supersedes every duplicate-risk source whose + // elected successor settled after its dispatch; the in-memory world + // applies the same per-step projection through the same pure core. + for (const source of this.list()) { + if (source.duplicateSuccessor === undefined || source.supersededBy !== undefined) continue; + const event = duplicateSourceSupersession(source, this.get(source.duplicateSuccessor.runId), at); + if (event !== null) this.record(source.runId, event); + } + } } /** The file-backed state layer on a real state home. */ @@ -312,7 +376,12 @@ class FileStore implements FenceStore { const path = confirmedWriteLedgerPath( journal.adapter.hash, journal.auth.hash, journal.operation, journal.inputHash, this.environment, intent.duplicateIntentHash, ); - const claimed = acquireConfirmedWriteLedgers({ path, entry, intent }, this.environment, at); + // The model's claim stands for a claim whose journal scan ran before + // another locator's run of the same subject recorded its own claim, so + // this world withholds the subject from the claim's scan. The scan before + // it and the recheck after it keep theirs. + const { authSubject: _raced, ...withheld } = intent; + const claimed = acquireConfirmedWriteLedgers({ path, entry, intent: withheld }, this.environment, at); if (!claimed.acquired) { if (!("viaIntent" in claimed)) { throw new ReplayDivergence(`the hash-keyed ledger refused ${labelOf(journal.runId)} after its intent claim`); @@ -323,6 +392,13 @@ class FileStore implements FenceStore { return { acquired: true, ledgerRelativePath: relative(ghostgetStateHome(this.environment), claimed.snapshot.path).split(sep).join("/") }; } + recheck(intent: ConfirmedWriteIntent, runId: string): SubjectBlock | null { + return recheckConfirmedWriteSubjectFence(intent, runId, this.environment); + } + + /** The repair pass after each step projects every terminal journal, as finalizePreDispatchFailure does. */ + project(): void {} + /** The owner dies inside its dispatch; the repair pass settles the journal. */ lose(runId: string, at: Date): void { const snapshot = readRunJournal(runId, this.environment); @@ -407,8 +483,9 @@ class FenceWorld { return this.defect === "hash-keyed-intent" ? `${ADAPTER_ID}-${String(generation)}` : ADAPTER_ID; } - private authId(generation: number): string { - return this.defect === "hash-keyed-intent" ? `${AUTH_ID}-${String(generation)}` : AUTH_ID; + private authId(locator: string, generation: number): string { + const id = AUTH_IDS[locator]!; + return this.defect === "hash-keyed-intent" ? `${id}-${String(generation)}` : id; } private journal(run: string): RunJournal { @@ -422,21 +499,23 @@ class FenceWorld { } private bound(journal: RunJournal): boolean { - return journal.auth.hash === hashFor("auth", this.authGen) && journal.adapter.hash === hashFor("manifest", this.rev); + return journal.auth.hash === hashFor(`auth-${locatorOf(journal)}`, this.authGen) + && journal.adapter.hash === hashFor("manifest", this.rev); } - /** The intent a journal belongs to. */ + /** The intent a journal belongs to, with the subject its auth record named. */ private intentOf(journal: RunJournal): ConfirmedWriteIntent { return { adapterId: journal.adapter.id, authId: journal.auth.id, operationId: journal.operation, inputHashes: [journal.inputHash], ...(journal.duplicateIntent === undefined ? {} : { duplicateIntentHash: journal.duplicateIntent.intentHash }), + ...(journal.authSubject === undefined ? {} : { authSubject: journal.authSubject }), }; } - private refuse(run: string, existing: LedgerEntry): void { + private refuse(run: string, existing: LedgerEntry, viaSubject?: { readonly authId: string }): void { const journal = this.journal(run); const disposition = priorRunDisposition( - { existing, viaIntent: true }, + { existing, viaIntent: true, ...(viaSubject === undefined ? {} : { viaSubject }) }, { inputHash: journal.inputHash, adapterHash: journal.adapter.hash, authHash: journal.auth.hash, authId: journal.auth.id }, ); this.result = blockedResult(disposition); @@ -473,9 +552,14 @@ class FenceWorld { } } - private start(run: string, source: string | null): void { + private start(run: string, source: string | null, pickedLocator: string, pickedSubject: string): void { const started = this.now().toISOString(); - const authHash = hashFor("auth", this.authGen); + // A successor binds its source's auth record, so it runs under the + // source's locator and subject. + const origin = source === null ? undefined : this.journal(source); + const locator = origin === undefined ? pickedLocator : locatorOf(origin); + const subject = origin === undefined ? pickedSubject : subjectOf(origin); + const authHash = hashFor(`auth-${locator}`, this.authGen); const adapterHash = hashFor("manifest", this.rev); const duplicateIntent = source === null ? undefined : { schemaVersion: 1 as const, @@ -489,7 +573,8 @@ class FenceWorld { operation: OPERATION, risk: "R3", inputHash: INPUT_HASH, - auth: { id: this.authId(this.authGen), hash: authHash, kind: "browser-profile" }, + auth: { id: this.authId(locator, this.authGen), hash: authHash, kind: "browser-profile" }, + ...(subject === "" ? {} : { authSubject: SUBJECT_IDS[subject]! }), contract: { transport: "web-session-api", hash: sha256("fence-contract") }, ...(duplicateIntent === undefined ? {} : { duplicateIntent }), plannedDispatches: 1, @@ -501,25 +586,26 @@ class FenceWorld { this.store.create(journal); const blocker = intentFenceBlocker(this.store.list(), this.intentOf(journal), journal.runId, this.now()); if (blocker !== null) { - this.refuse(run, runJournalLedgerEntry(blocker)); + // acquireIntentLedger names the other locator when the blocker ran under one. + this.refuse(run, runJournalLedgerEntry(blocker), blocker.auth.id === journal.auth.id ? undefined : { authId: blocker.auth.id }); } else { this.scanned.add(run); this.result = "clear"; } } - apply(action: Action, run: string, outcome: string, source: string): void { - this.step(action, run, outcome, source); + apply(action: Action, run: string, outcome: string, source: string, locator: string, subject: string): void { + this.step(action, run, outcome, source, locator, subject); this.store.afterStep(this.now()); } - private step(action: Action, run: string, outcome: string, source: string): void { + private step(action: Action, run: string, outcome: string, source: string, locator: string, subject: string): void { switch (action) { case "scan": - this.start(run, null); + this.start(run, null, locator, subject); return; case "scanSuccessor": - this.start(run, source); + this.start(run, source, locator, subject); return; case "claim": { const journal = this.journal(run); @@ -529,7 +615,7 @@ class FenceWorld { }; const claimed = this.store.claim(journal, this.intentOf(journal), entry, this.now()); if (!claimed.acquired) { - this.refuse(run, claimed.existing); + this.refuse(run, claimed.existing, claimed.viaSubject); return; } this.scanned.delete(run); @@ -539,6 +625,21 @@ class FenceWorld { } case "dispatch": { const journal = this.journal(run); + // The confirmed-write program rechecks the subject fence once its + // claim is on record, before anything else at the dispatch boundary. + const blocked = this.store.recheck(this.intentOf(journal), journal.runId); + if (blocked !== null) { + const disposition = priorRunDisposition(blocked, { + inputHash: journal.inputHash, adapterHash: journal.adapter.hash, authHash: journal.auth.hash, authId: journal.auth.id, + }); + if (disposition.kind !== "refuse" || !SUBJECT_REFUSAL.test(disposition.message)) { + throw new ReplayDivergence(`the subject recheck for ${run} did not refuse as a subject fence`); + } + this.record(run, { type: "finished", status: "failed", finalOrigin: null, error: "another run already owns this idempotency scope", at: this.at() }); + this.store.project(journal.runId); + this.result = "subject-refused"; + return; + } this.record(run, { type: "recovery-stored", at: this.at() }); if (journal.duplicateIntent !== undefined) { // claimDuplicateRiskSource elects the source before the successor's dispatch boundary. @@ -609,6 +710,8 @@ class FenceWorld { const ledgerState = new Map(); const runAuth = new Map(); const runRev = new Map(); + const runLoc = new Map(); + const runSubj = new Map(); const source = new Map(); const elected = new Map(); const dispatched = new Set(); @@ -621,7 +724,9 @@ class FenceWorld { ledgerState.set(run, journal?.ledgerState ?? "none"); elected.set(run, journal?.duplicateSuccessor === undefined ? "" : labelOf(journal.duplicateSuccessor.runId)); if (journal === undefined) continue; - runAuth.set(run, generationOf(journal.auth.hash, "auth")); + runLoc.set(run, locatorOf(journal)); + runSubj.set(run, subjectOf(journal)); + runAuth.set(run, generationOf(journal.auth.hash, `auth-${locatorOf(journal)}`)); runRev.set(run, generationOf(journal.adapter.hash, "manifest")); source.set(run, journal.duplicateIntent === undefined ? "" : labelOf(journal.duplicateIntent.sourceRunId)); if (journal.dispatch.started > 0) dispatched.add(run); @@ -629,7 +734,7 @@ class FenceWorld { } const ledgers = this.store.ledgers(); return { - phase, status, ledgerState, runAuth, runRev, source, elected, + phase, status, ledgerState, runAuth, runRev, runLoc, runSubj, source, elected, authGen: this.authGen, rev: this.rev, scanned: new Set(this.scanned), @@ -652,10 +757,10 @@ function modelState(state: ItfState): Snapshot { const ledger = itfVariable(state, "ledger"); if (ledger.kind !== "set") throw new Error("ITF ledger must be a set"); const entries = ledger.items.map((item) => { - if (item.kind !== "tuple" || item.items.length !== 4) throw new Error("ITF ledger entries must be 4-tuples"); - const [auth, revision, source, holder] = item.items as readonly [ItfValue, ItfValue, ItfValue, ItfValue]; + if (item.kind !== "tuple" || item.items.length !== 5) throw new Error("ITF ledger entries must be 5-tuples"); + const [auth, revision, locator, source, holder] = item.items as readonly [ItfValue, ItfValue, ItfValue, ItfValue, ItfValue]; return { - key: `${String(itfInt(auth, "ledger auth key"))}/${String(itfInt(revision, "ledger revision key"))}/${itfString(source, "ledger source key")}`, + key: `${String(itfInt(auth, "ledger auth key"))}/${String(itfInt(revision, "ledger revision key"))}/${itfString(locator, "ledger locator key")}/${itfString(source, "ledger source key")}`, holder: itfString(holder, "ledger holder"), }; }); @@ -669,6 +774,8 @@ function modelState(state: ItfState): Snapshot { ledgerState: itfStringMap(itfVariable(state, "ledgerState"), "ledgerState", itfString), runAuth: journaled(itfStringMap(itfVariable(state, "runAuth"), "runAuth", itfInt)), runRev: journaled(itfStringMap(itfVariable(state, "runRev"), "runRev", itfInt)), + runLoc: journaled(itfStringMap(itfVariable(state, "runLoc"), "runLoc", itfString)), + runSubj: journaled(itfStringMap(itfVariable(state, "runSubj"), "runSubj", itfString)), source: journaled(itfStringMap(itfVariable(state, "source"), "source", itfString)), elected: itfStringMap(itfVariable(state, "elected"), "elected", itfString), authGen: itfInt(itfVariable(state, "authGen"), "authGen"), @@ -686,17 +793,35 @@ function modelState(state: ItfState): Snapshot { /** * The first clause of the model's `fenceSafety` that `state` breaks, or null: - * effects stay within one plus the elected successors, each intent dispatches - * at most once, only an indeterminate run elects a successor, and an - * indeterminate run keeps its ledger. + * each locator's effects stay within one plus its elected successors, each + * intent dispatches at most once under a locator, one recorded subject never + * dispatches one intent under two locators unless one of them succeeded, only + * an indeterminate run elects a successor, and an indeterminate run keeps its + * ledger. */ function safetyViolation(state: Snapshot): string | null { - const elected = [...state.elected.values()].filter((successor) => successor !== "").length; - if (state.dispatched.size > 1 + elected) return `${String(state.dispatched.size)} dispatches with ${String(elected)} elected successors`; + const locatorOfRun = (run: string): string => state.runLoc.get(run) ?? ""; + for (const locator of LOCATORS) { + const dispatches = [...state.dispatched].filter((run) => locatorOfRun(run) === locator).length; + const elected = [...state.elected].filter(([run, successor]) => successor !== "" && locatorOfRun(run) === locator).length; + if (dispatches > 1 + elected) return `${String(dispatches)} dispatches with ${String(elected)} elected successors under ${locator}`; + } for (const run of state.applied) if (!state.dispatched.has(run)) return `${run} applied without a dispatch`; for (const key of ["", ...RUNS]) { - const runs = [...state.dispatched].filter((run) => (state.source.get(run) ?? "") === key); - if (runs.length > 1) return `the intent ${key === "" ? "base" : `successor of ${key}`} dispatched ${runs.sort().join(", ")}`; + for (const locator of LOCATORS) { + const runs = [...state.dispatched].filter((run) => (state.source.get(run) ?? "") === key && locatorOfRun(run) === locator); + if (runs.length > 1) return `the intent ${key === "" ? "base" : `successor of ${key}`} dispatched ${runs.sort().join(", ")} under ${locator}`; + } + } + for (const run of state.dispatched) { + for (const other of state.dispatched) { + const subject = state.runSubj.get(run) ?? ""; + if ( + run < other && subject !== "" && subject === (state.runSubj.get(other) ?? "") + && (state.source.get(run) ?? "") === (state.source.get(other) ?? "") && locatorOfRun(run) !== locatorOfRun(other) + && state.status.get(run) !== "succeeded" && state.status.get(other) !== "succeeded" + ) return `subject ${subject} dispatched ${run} and ${other} under two locators`; + } } for (const [run, successor] of state.elected) { if (successor !== "" && state.status.get(run) !== "indeterminate") return `${run} elected ${successor} while ${String(state.status.get(run))}`; @@ -723,33 +848,51 @@ function difference(actual: Snapshot, expected: Snapshot): string | null { return null; } -type RecordedStep = Readonly<{ action: string; run: string | null; outcome: string | null; source: string | null }>; +type RecordedStep = Readonly<{ + action: string; + run: string | null; + outcome: string | null; + source: string | null; + locator: string | null; + subject: string | null; +}>; function recordedStep(state: ItfState): RecordedStep { const action = itfString(itfVariable(state, "mbt::actionTaken"), "mbt::actionTaken"); - const picks = itfRecord(itfVariable(state, "mbt::nondetPicks"), ["r", "o", "s"], "mbt::nondetPicks"); + const picks = itfRecord(itfVariable(state, "mbt::nondetPicks"), ["r", "o", "s", "l", "j"], "mbt::nondetPicks"); const pick = (name: string): string | null => { const value = itfOption(picks.get(name)!, `mbt::nondetPicks.${name}`); return value === null ? null : itfString(value, `mbt::nondetPicks.${name}`); }; - return { action, run: pick("r"), outcome: pick("o"), source: pick("s") }; + return { action, run: pick("r"), outcome: pick("o"), source: pick("s"), locator: pick("l"), subject: pick("j") }; } -function operation(state: ItfState): Readonly<{ action: Action; run: string; outcome: string; source: string }> { - const { action, run, outcome, source } = recordedStep(state); - if (!(ACTIONS as readonly string[]).includes(action) || run === null || outcome === null || source === null) { +type Operation = Readonly<{ action: Action; run: string; outcome: string; source: string; locator: string; subject: string }>; + +function operation(state: ItfState): Operation { + const { action, run, outcome, source, locator, subject } = recordedStep(state); + if ( + !(ACTIONS as readonly string[]).includes(action) + || run === null || outcome === null || source === null || locator === null || subject === null + ) { throw new Error(`state ${String(state.index)} records an unknown action or a missing pick`); } - if (![run, source].every((name) => (RUNS as readonly string[]).includes(name)) || !(OUTCOMES as readonly string[]).includes(outcome)) { - throw new Error(`state ${String(state.index)} picks an unknown run or outcome`); + if ( + ![run, source].every((name) => (RUNS as readonly string[]).includes(name)) + || !(OUTCOMES as readonly string[]).includes(outcome) + || !(LOCATORS as readonly string[]).includes(locator) + || !(SUBJECTS as readonly string[]).includes(subject) + ) { + throw new Error(`state ${String(state.index)} picks an unknown run, outcome, locator, or subject`); } - return { action: action as Action, run, outcome, source }; + return { action: action as Action, run, outcome, source, locator, subject }; } -function label(action: string, run: string, outcome: string, source: string): string { +function label({ action, run, outcome, source, locator, subject }: Operation): string { if (action === "reconnect" || action === "upgrade") return action; if (action === "finish") return `finish(${run}, ${outcome})`; if (action === "scanSuccessor") return `scanSuccessor(${run} of ${source})`; + if (action === "scan") return `scan(${run} under ${locator}${subject === "" ? "" : ` as ${subject}`})`; return `${action}(${run})`; } @@ -761,13 +904,14 @@ function replay(trace: ItfTrace, world: FenceWorld): void { const start = difference(world.snapshot(), modelState(initial)); if (start !== null) throw new ReplayDivergence(`state 0: ${start}`); for (const state of steps) { - const { action, run, outcome, source } = operation(state); - const step = label(action, run, outcome, source); + const picked = operation(state); + const { action, run, outcome, source, locator, subject } = picked; + const step = label(picked); if (!world.admits(action, run, source)) { throw new ReplayDivergence(`state ${String(state.index)}: production does not admit ${step}`); } try { - world.apply(action, run, outcome, source); + world.apply(action, run, outcome, source, locator, subject); } catch (error) { if (error instanceof ReplayDivergence) throw new ReplayDivergence(`state ${String(state.index)}: ${step}: ${error.message}`); throw error; @@ -793,17 +937,22 @@ function divergence(trace: ItfTrace, world: FenceWorld): string | null { * Drive production through a mutant's trace. Production keeps its own state * and applies each action it admits, so it may refuse a run the mutant lets * through. Returns every action the mutant takes that production refuses, - * and fails if production's own state ever breaks the model's safety clauses. + * including a dispatch that production's subject recheck refuses, and fails + * if production's own state ever breaks the model's safety clauses. */ function refusedActions(trace: ItfTrace): readonly string[] { const world = new FenceWorld(); const refused: string[] = []; for (const state of trace.states.slice(1)) { - const { action, run, outcome, source } = operation(state); + const picked = operation(state); + const { action, run, outcome, source, locator, subject } = picked; if (world.admits(action, run, source)) { - world.apply(action, run, outcome, source); + world.apply(action, run, outcome, source, locator, subject); + if (action === "dispatch" && world.phaseOf(run) !== "dispatching") { + refused.push(`state ${String(state.index)}: the mutant takes ${label(picked)}, which production refuses at its subject recheck`); + } } else if (action === "dispatch" || action === "scanSuccessor") { - refused.push(`state ${String(state.index)}: the mutant takes ${label(action, run, outcome, source)}, which production refuses with ${run} ${world.phaseOf(run)}`); + refused.push(`state ${String(state.index)}: the mutant takes ${label(picked)}, which production refuses with ${run} ${world.phaseOf(run)}`); } const broken = safetyViolation(world.snapshot()); if (broken !== null) throw new Error(`state ${String(state.index)}: production broke fence safety: ${broken}`); @@ -821,8 +970,32 @@ const traces = quintTraceCache(MODEL_FILE); */ const SUCCESSOR_STEP = "stepSuccessors"; +/** + * A restriction of `step` whose transitions are all `step` transitions. Every + * base intent records the one subject, so runs under the two locators race + * through the subject fence and its recheck, which uniform sampling of `step` + * seldom reaches. + */ +const SUBJECT_STEP = "stepSubjects"; + +/** Every seeded trace set the fixed model is replayed from. */ +const seededTraces = async (step: string): Promise => + [...await traces(step), ...await traces(SUCCESSOR_STEP), ...await traces(SUBJECT_STEP)]; + +/** + * Whether the scan `state` records was refused by another locator's unsettled + * run of the same subject in the state before it. + */ +function subjectRefusedScan(before: Snapshot, picked: Operation, after: Snapshot): boolean { + return picked.action === "scan" && after.result === "refused" && picked.subject !== "" + && RUNS.some((run) => run !== picked.run + && before.runSubj.get(run) === picked.subject && before.runLoc.get(run) !== picked.locator + && (before.source.get(run) ?? "") === "" + && (before.ledgerState.get(run) === "pending" || before.ledgerState.get(run) === "indeterminate")); +} + /** How many seeded traces the file-backed world replays: a cover of every action result. */ -const FILE_BACKED_TRACES = 5; +const FILE_BACKED_TRACES = 7; /** Each action a trace takes with the result the model records for it (a finish records its outcome). */ function coverageLabels(trace: ItfTrace): ReadonlySet { @@ -864,8 +1037,8 @@ describe("fence.qnt ITF replay", () => { expect(model.replay.target).toBe("production"); expect(model.replay.test).toBe("scripts/verification-fence-replay.test.ts"); expect(model.mutants.map((mutant) => mutant.step).sort()).toEqual([...MUTANT_STEPS].sort()); - const all = [...await traces(model.step), ...await traces(SUCCESSOR_STEP)]; - expect(all).toHaveLength(2 * model.replay.traces); + const all = await seededTraces(model.step); + expect(all).toHaveLength(3 * model.replay.traces); const covered = new Set(); for (const trace of all) { expect(trace.source).toBe(MODEL_FILE); @@ -873,11 +1046,16 @@ describe("fence.qnt ITF replay", () => { expect(trace.states.length).toBeGreaterThan(1); expect(trace.states.length).toBeLessThanOrEqual(model.replay.maxSteps + 1); expect(divergence(trace, new FenceWorld())).toBeNull(); - for (const state of trace.states.slice(1)) { - const { action, run, outcome } = operation(state); - covered.add(action === "scanSuccessor" ? `scanSuccessor(${run})` : label(action, run, outcome, run)); - covered.add(`${action} -> ${modelState(state).result}`); - expect(safetyViolation(modelState(state))).toBeNull(); + for (const [index, state] of trace.states.entries()) { + if (index === 0) continue; + const picked = operation(state); + const { action, run, outcome, locator, subject } = picked; + const after = modelState(state); + covered.add(action === "finish" ? `finish(${run}, ${outcome})` : action === "reconnect" || action === "upgrade" ? action : `${action}(${run})`); + covered.add(`${action} -> ${after.result}`); + if (action === "scan") covered.add(`scan under ${locator}${subject === "" ? "" : ` as ${subject}`} -> ${after.result}`); + if (subjectRefusedScan(modelState(trace.states[index - 1]!), picked, after)) covered.add("scan -> refused by subject"); + expect(safetyViolation(after)).toBeNull(); } } const expected = [ @@ -889,7 +1067,9 @@ describe("fence.qnt ITF replay", () => { "scan -> clear", "scan -> refused", "scan -> replayed", "scan -> withheld", "scanSuccessor -> clear", "scanSuccessor -> refused", "claim -> claimed", "claim -> refused", "claim -> replayed", - "dispatch -> dispatched", "dispatch -> elected", + "dispatch -> dispatched", "dispatch -> elected", "dispatch -> subject-refused", + ...LOCATORS.flatMap((locator) => SUBJECTS.map((subject) => `scan under ${locator}${subject === "" ? "" : ` as ${subject}`} -> clear`)), + "scan -> refused by subject", ]; expect(expected.filter((entry) => !covered.has(entry))).toEqual([]); }); @@ -898,18 +1078,24 @@ describe("fence.qnt ITF replay", () => { // test each, since every state operation spawns the bound state helper. const fileBackedCoverOf = async (): Promise => { const model = await lockedModel(); - return fileBackedCover([...await traces(model.step), ...await traces(SUCCESSOR_STEP)], FILE_BACKED_TRACES); + return fileBackedCover(await seededTraces(model.step), FILE_BACKED_TRACES); }; test("the file-backed cover takes every action result the seeded traces take", async () => { const model = await lockedModel(); - const all = [...await traces(model.step), ...await traces(SUCCESSOR_STEP)]; + const all = await seededTraces(model.step); const everything = new Set(all.flatMap((trace) => [...coverageLabels(trace)])); const cover = await fileBackedCoverOf(); - expect(cover).toHaveLength(FILE_BACKED_TRACES); + // The cap bounds replay cost; the greedy cover may finish earlier when + // the model's state space covers every result in fewer traces. + expect(cover.length).toBeGreaterThan(0); + expect(cover.length).toBeLessThanOrEqual(FILE_BACKED_TRACES); const covered = new Set(cover.flatMap((trace) => [...coverageLabels(trace)])); expect([...everything].filter((entry) => !covered.has(entry)).sort()).toEqual([]); - for (const entry of ["dispatch -> elected", "finish -> lost", "reconcile -> settled", "claim -> refused", "scanSuccessor -> refused"]) { + for (const entry of [ + "dispatch -> elected", "dispatch -> subject-refused", "finish -> lost", "reconcile -> settled", "claim -> refused", + "scanSuccessor -> refused", + ]) { expect(covered).toContain(entry); } }); @@ -917,7 +1103,7 @@ describe("fence.qnt ITF replay", () => { for (let index = 0; index < FILE_BACKED_TRACES; index += 1) { test(`replays covering trace ${String(index + 1)} of ${String(FILE_BACKED_TRACES)} through the file-backed state layer`, async () => { const trace = (await fileBackedCoverOf())[index]; - if (trace === undefined) throw new Error(`the file-backed cover has no trace ${String(index + 1)}`); + if (trace === undefined) return; expect(divergence(trace, new FenceWorld("none", new FileStore()))).toBeNull(); }); } @@ -926,7 +1112,7 @@ describe("fence.qnt ITF replay", () => { const model = await lockedModel(); const all = await traces(model.step); const first = all.map((trace) => divergence(trace, new FenceWorld("hash-keyed-intent"))).find((message) => message !== null); - expect(first).toMatch(/^state \d+: after (scan|scanSuccessor|claim)\(r[123]( of r[123])?\) /u); + expect(first).toMatch(/^state \d+: after (scan|scanSuccessor|claim)\(r[123]( of r[123]| under [ab]( as s)?)?\) /u); }); test("a reconciler that releases on a caller's claim diverges from the model traces", async () => { @@ -957,7 +1143,7 @@ describe("fence.qnt ITF replay", () => { }); if (dispatchBreach && step !== "stepUnelected") expect(refused.length).toBeGreaterThan(0); for (const message of refused) { - expect(message).toMatch(/^state \d+: the mutant takes (dispatch\(r[123]\)|scanSuccessor\(r[123] of r[123]\)), which production refuses with r[123] (none|terminal|prepared|claimed)$/u); + expect(message).toMatch(/^state \d+: the mutant takes (dispatch\(r[123]\)|scanSuccessor\(r[123] of r[123]\)), which production refuses (with r[123] (none|terminal|prepared|claimed)|at its subject recheck)$/u); } } expect(violating).toBeGreaterThan(0); @@ -969,22 +1155,27 @@ describe("fence.qnt ITF replay", () => { const runs = (value: unknown) => ({ "#map": RUNS.map((run) => [run, value]) }); const initial = { phase: runs("none"), status: runs("none"), ledgerState: runs("none"), - runAuth: runs({ "#bigint": "0" }), runRev: runs({ "#bigint": "0" }), source: runs(""), elected: runs(""), + runAuth: runs({ "#bigint": "0" }), runRev: runs({ "#bigint": "0" }), runLoc: runs(""), runSubj: runs(""), + source: runs(""), elected: runs(""), authGen: { "#bigint": "0" }, rev: { "#bigint": "0" }, scanned: { "#set": [] }, ledger: { "#set": [] }, dispatched: { "#set": [] }, applied: { "#set": [] }, reconciled: { "#set": [] }, claimed: { "#set": [] }, }; - const trace = (action: string, r: unknown, o: unknown, s: unknown): ItfTrace => parseItfTrace(JSON.stringify({ - vars: TRACE_VARIABLES, - states: [ - { "#meta": { index: 0 }, ...initial, result: "none", "mbt::actionTaken": "init", "mbt::nondetPicks": { r: none, o: none, s: none } }, - { - "#meta": { index: 1 }, ...initial, result: "reconnected", authGen: { "#bigint": "1" }, - "mbt::actionTaken": action, "mbt::nondetPicks": { r, o, s }, - }, - ], - })); const some = (value: string) => ({ tag: "Some", value }); + const trace = (action: string, r: unknown, o: unknown, s: unknown, l: unknown = some("a"), j: unknown = some("")): ItfTrace => + parseItfTrace(JSON.stringify({ + vars: TRACE_VARIABLES, + states: [ + { + "#meta": { index: 0 }, ...initial, result: "none", "mbt::actionTaken": "init", + "mbt::nondetPicks": { r: none, o: none, s: none, l: none, j: none }, + }, + { + "#meta": { index: 1 }, ...initial, result: "reconnected", authGen: { "#bigint": "1" }, + "mbt::actionTaken": action, "mbt::nondetPicks": { r, o, s, l, j }, + }, + ], + })); expect(divergence(trace("reconnect", some("r1"), some("lost"), some("r2")), new FenceWorld())).toBeNull(); expect(divergence(trace("reconnect", some("r1"), some("lost"), some("r2")), new FenceWorld("none", new FileStore()))).toBeNull(); expect(() => divergence(trace("steal", some("r1"), some("lost"), some("r2")), new FenceWorld())).toThrow("unknown action"); @@ -992,6 +1183,10 @@ describe("fence.qnt ITF replay", () => { expect(() => divergence(trace("reconnect", some("r1"), some("lost"), none), new FenceWorld())).toThrow("missing pick"); expect(() => divergence(trace("reconnect", some("r9"), some("lost"), some("r2")), new FenceWorld())).toThrow("unknown run"); expect(() => divergence(trace("reconnect", some("r1"), some("lost"), some("r9")), new FenceWorld())).toThrow("unknown run"); + expect(() => divergence(trace("reconnect", some("r1"), some("lost"), some("r2"), none), new FenceWorld())).toThrow("missing pick"); + expect(() => divergence(trace("reconnect", some("r1"), some("lost"), some("r2"), some("a"), none), new FenceWorld())).toThrow("missing pick"); + expect(() => divergence(trace("reconnect", some("r1"), some("lost"), some("r2"), some("c")), new FenceWorld())).toThrow("unknown run, outcome, locator, or subject"); + expect(() => divergence(trace("reconnect", some("r1"), some("lost"), some("r2"), some("a"), some("t")), new FenceWorld())).toThrow("unknown run, outcome, locator, or subject"); expect(divergence(trace("upgrade", some("r1"), some("lost"), some("r2")), new FenceWorld())) .toBe("state 1: after upgrade authGen is 0 in production and 1 in the model"); }); @@ -1000,15 +1195,28 @@ describe("fence.qnt ITF replay", () => { const base = modelStateFor({}); expect(safetyViolation(base)).toBeNull(); expect(safetyViolation(modelStateFor({ dispatched: ["r1", "r2"], source: { r1: "", r2: "" }, status: { r1: "indeterminate", r2: "pending" }, ledgerState: { r1: "indeterminate", r2: "pending" } }))) - .toBe("2 dispatches with 0 elected successors"); + .toBe("2 dispatches with 0 elected successors under a"); expect(safetyViolation(modelStateFor({ dispatched: ["r1", "r2", "r3"], source: { r1: "", r2: "r1", r3: "r1" }, elected: { r1: "r3" }, status: { r1: "indeterminate", r2: "pending", r3: "pending" }, ledgerState: { r1: "indeterminate", r2: "pending", r3: "pending" }, - }))).toBe("3 dispatches with 1 elected successors"); + }))).toBe("3 dispatches with 1 elected successors under a"); expect(safetyViolation(modelStateFor({ dispatched: ["r1", "r2", "r3"], source: { r1: "", r2: "r1", r3: "r1" }, elected: { r1: "r3", r2: "r3" }, status: { r1: "indeterminate", r2: "indeterminate", r3: "pending" }, ledgerState: { r1: "indeterminate", r2: "indeterminate", r3: "pending" }, - }))).toBe("the intent successor of r1 dispatched r2, r3"); + }))).toBe("the intent successor of r1 dispatched r2, r3 under a"); + // One recorded subject under two locators: two dispatches of one intent. + const twoLocators = { + dispatched: ["r1", "r2"], source: { r1: "", r2: "" }, runLoc: { r1: "a", r2: "b" }, + status: { r1: "indeterminate", r2: "pending" }, ledgerState: { r1: "indeterminate", r2: "pending" }, + } as const; + expect(safetyViolation(modelStateFor({ ...twoLocators, runSubj: { r1: "s", r2: "s" } }))) + .toBe("subject s dispatched r1 and r2 under two locators"); + // No subject, or another subject, is another account's intent; a succeeded run no longer fences. + expect(safetyViolation(modelStateFor(twoLocators))).toBeNull(); + expect(safetyViolation(modelStateFor({ ...twoLocators, runSubj: { r1: "s", r2: "" } }))).toBeNull(); + expect(safetyViolation(modelStateFor({ + ...twoLocators, runSubj: { r1: "s", r2: "s" }, status: { r1: "succeeded", r2: "pending" }, ledgerState: { r1: "succeeded", r2: "pending" }, + }))).toBeNull(); expect(safetyViolation(modelStateFor({ dispatched: ["r1", "r2"], source: { r1: "", r2: "r1" }, elected: { r1: "r2" }, status: { r1: "pending", r2: "pending" }, ledgerState: { r1: "pending", r2: "pending" }, @@ -1024,6 +1232,8 @@ function modelStateFor(values: Readonly<{ dispatched?: readonly string[]; applied?: readonly string[]; source?: Readonly>; + runLoc?: Readonly>; + runSubj?: Readonly>; elected?: Readonly>; status?: Readonly>; ledgerState?: Readonly>; @@ -1036,6 +1246,9 @@ function modelStateFor(values: Readonly<{ ledgerState: perRun(values.ledgerState, "none"), runAuth: new Map(), runRev: new Map(), + // A run with a journal runs under locator a and records no subject unless given. + runLoc: new Map(Object.keys(values.source ?? {}).map((run) => [run, values.runLoc?.[run] ?? "a"])), + runSubj: new Map(Object.keys(values.source ?? {}).map((run) => [run, values.runSubj?.[run] ?? ""])), source: new Map(Object.entries(values.source ?? {})), elected: perRun(values.elected, ""), authGen: 0, diff --git a/scripts/verification-tools.ts b/scripts/verification-tools.ts index 85272941..4ec84289 100644 --- a/scripts/verification-tools.ts +++ b/scripts/verification-tools.ts @@ -219,8 +219,15 @@ const QUINT_TIMEOUT_MS = 5 * 60_000; * test, so a hung Quint fails with this bound's diagnosis rather than the * runner's. */ -export const QUINT_TRACE_TIMEOUT_MS = 90_000; -const APALACHE_TIMEOUT_MS = 10 * 60_000; +export const QUINT_TRACE_TIMEOUT_MS = 150_000; +/** + * The bound on one Apalache check. With `QUINT_CONCURRENCY` two checker jobs + * share the runner's four vCPUs, so a check that finishes in about ten + * minutes alone can need roughly twice that when a second Apalache or a + * `bun test` replay runs beside it. The bound fails an actually stuck check, + * not one that is merely sharing the runner. + */ +const APALACHE_TIMEOUT_MS = 20 * 60_000; // Nightly runs sit outside the 50-minute CI verification step, so each deeper // checker run gets its own larger bound. A timeout still fails the run. const NIGHTLY_QUINT_TIMEOUT_MS = 30 * 60_000; @@ -1606,7 +1613,10 @@ const DEFAULT_QUINT_MODEL_WEIGHT = 60; // every model still runs exactly once. A model without a reading takes the // default weight until its first CI log. const MEASURED_QUINT_MODEL_WEIGHTS = Object.freeze({ - "fence.qnt": 460, + // With the subject dimension, fence.qnt's six Apalache checks and its + // replay approach the quint step's former 20-minute budget on a shared + // 4-vCPU runner (run 36093627910); it packs alone onto the lightest shard. + "fence.qnt": 1150, "release.qnt": 330, "state-claim.qnt": 170, "media.qnt": 155, diff --git a/skills/ghostget/references/safety-and-state.md b/skills/ghostget/references/safety-and-state.md index 81de6cc0..ef933a1d 100644 --- a/skills/ghostget/references/safety-and-state.md +++ b/skills/ghostget/references/safety-and-state.md @@ -80,6 +80,11 @@ revalidation. A materializer failure records the failed exact data revision and retains the last good entities as `retained-after-drift`; it must not weaken parsing or mutate the exact snapshot to make drift disappear. +Read paths, including `invoke --cache-only`, bind the current auth lifetime +identity and fail closed when it is missing; they never create it. +`invoke --projection-identity-only` is the SDK's identity preflight for a live +invoke, so it is execution preparation and may create a missing identity. + Auth replacement and removal rotate a durable local lifetime identity before cleanup. Projection and provider-session ciphertext from an earlier lifetime must remain unreadable even if identical locator bytes are later recreated. diff --git a/src/confirmed-write-intent-fence.test.ts b/src/confirmed-write-intent-fence.test.ts index d9c1cf03..8c20aebc 100644 --- a/src/confirmed-write-intent-fence.test.ts +++ b/src/confirmed-write-intent-fence.test.ts @@ -53,6 +53,7 @@ type Settled = | { readonly ok: false; readonly message: string }; const ACCOUNT = "x-official"; +const SECOND_ACCOUNT = "x-second"; const MESSAGE = "intent fence fixture"; const DEDUPE_WINDOW_MS = 86_400_000; const DEAD_OWNER = { @@ -100,17 +101,30 @@ function connectAccount(testState: FenceState, generation: number, force = gener }), testState.environment, force ? { force: true } : {}); } +/** + * Connect the same X account under a second locator ID. With `subject` + * undefined the record names no provider subject. + */ +function connectSecondLocator(testState: FenceState, subject: string | undefined): void { + saveAuth(createAuth(SECOND_ACCOUNT, { + oauthProvider: "x", + tokenFile: join(testState.directory, "x-token-second.json"), + scopes: ["tweet.read", "tweet.write", "users.read"], + ...(subject === undefined ? {} : { subject }), + }), testState.environment); +} + function install(testState: FenceState): void { installAdapter(testState, 0); connectAccount(testState, 0); } -function savedPlan(testState: FenceState, at?: Date): string { +function savedPlan(testState: FenceState, at?: Date, account = ACCOUNT): string { const invocation = prepareInvocation( "x", "posts.publish", { body: MESSAGE }, - ACCOUNT, + account, testState.environment, ); const stored = at === undefined @@ -191,8 +205,9 @@ function confirm( outcome: Outcome, probe: Probe, at?: Date, + account = ACCOUNT, ): Promise { - const digest = savedPlan(testState, at); + const digest = savedPlan(testState, at, account); return settle(confirmInvocation(digest, { headed: false, environment: testState.environment, @@ -761,6 +776,64 @@ describe("intent-level confirmed-write fence", () => { } }); + test("the same provider subject under a second locator cannot redispatch an unsettled intent", async () => { + const testState = fenceState(); + try { + install(testState); + const probe: Probe = { crossings: 0 }; + const first = requireResult(await confirm(testState, "indeterminate", probe)); + expect(first.receipt.status).toBe("indeterminate"); + const journal = listRunJournalSnapshots(testState.environment).flatMap((entry) => + "invalid" in entry || entry.journal.runId !== first.receipt.runId ? [] : [entry.journal])[0]; + // The journal records the provider subject of the auth record it ran under. + expect(journal?.authSubject).toBe("12345"); + + connectSecondLocator(testState, "12345"); + const retry = refusal(await confirm(testState, "succeeded", probe, undefined, SECOND_ACCOUNT)); + + expect(probe.crossings).toBe(1); + expect(retry).toContain(`a prior attempt (${first.receipt.runId}) may have reached the provider under auth locator '${ACCOUNT}', which records the same provider subject`); + // The refused run leaves no idempotency claim of its own behind. + const holders = stateFiles(join(testState.directory, "idempotency")).map((path) => + (JSON.parse(readFileSync(path, "utf8")) as { readonly runId: string }).runId); + expect(new Set(holders)).toEqual(new Set([first.receipt.runId])); + } finally { + rmSync(testState.directory, { recursive: true, force: true }); + } + }); + + // A locator whose auth record names no provider subject cannot preview an + // R2/R3 action at all, so "no subject" only exists in journals written + // before the field did; the legacy-journal case covers it. + for (const setup of ["other-subject", "legacy-journal", "fulfilled"] as const) { + test(`a second locator keeps the per-locator fence: ${setup}`, async () => { + const testState = fenceState(); + try { + install(testState); + const probe: Probe = { crossings: 0 }; + const first = requireResult(await confirm(testState, setup === "fulfilled" ? "succeeded" : "indeterminate", probe)); + if (setup === "legacy-journal") { + // Journals written before the subject field existed carry none. + const entry = listRunJournalSnapshots(testState.environment).find((candidate) => + !("invalid" in candidate) && candidate.journal.runId === first.receipt.runId); + if (entry === undefined || "invalid" in entry) throw new Error("run journal is missing"); + const { authSubject: _dropped, ...legacy } = entry.journal as typeof entry.journal & { authSubject?: string }; + expect(writePrivateJsonIfUnchanged( + join(testState.directory, "run-journals", `${first.receipt.runId}.json`), + legacy, + { expectedCurrentContentSha256: entry.contentSha256 }, + )).toBeTrue(); + } + connectSecondLocator(testState, setup === "other-subject" ? "67890" : "12345"); + const second = requireResult(await confirm(testState, "succeeded", probe, undefined, SECOND_ACCOUNT)); + expect(second.replayed).toBeFalse(); + expect(probe.crossings).toBe(2); + } finally { + rmSync(testState.directory, { recursive: true, force: true }); + } + }); + } + test("a legacy ledger without a run journal still blocks its exact scope and leaves no intent claim", async () => { const testState = fenceState(); try { diff --git a/src/confirmed-write-model.ts b/src/confirmed-write-model.ts index 7978e757..5e8392e1 100644 --- a/src/confirmed-write-model.ts +++ b/src/confirmed-write-model.ts @@ -43,6 +43,13 @@ export type ConfirmedWriteIntent = { /** The current canonical input hash first, then any pre-migration encoding of the same input. */ readonly inputHashes: readonly string[]; readonly duplicateIntentHash?: string; + /** + * The provider subject the current auth record names, when it names one. + * An unsettled run of the same target, operation, and input that recorded + * this subject under another locator also fences the intent. Subjects may be + * typed by the operator, so this only ever refuses more, never less. + */ + readonly authSubject?: string; }; export type BoundedExecution = { diff --git a/src/confirmed-write-platform.ts b/src/confirmed-write-platform.ts index e0a7082d..ef754aff 100644 --- a/src/confirmed-write-platform.ts +++ b/src/confirmed-write-platform.ts @@ -86,7 +86,9 @@ export interface ConfirmedWriteKernel { /** Claim the intent fence, then the hash-keyed ledger. */ readonly acquireConfirmedWriteLedgers: (request: { readonly path: string; readonly entry: LedgerEntry; readonly alternatePaths?: readonly string[]; readonly intent: ConfirmedWriteIntent }, environment: Readonly>, now: Date) => | { readonly acquired: true; readonly snapshot: LedgerSnapshot } | { readonly acquired: false; readonly existing: LedgerEntry; readonly viaAlternatePath?: boolean } - | { readonly acquired: false; readonly existing: LedgerEntry; readonly viaIntent: true }; + | { readonly acquired: false; readonly existing: LedgerEntry; readonly viaIntent: true; readonly viaSubject?: { readonly authId: string } }; + /** Recheck the provider-subject fence once this run's ledger claim is on record. */ + readonly recheckConfirmedWriteSubjectFence: (intent: ConfirmedWriteIntent, runId: string, environment: Readonly>) => { readonly existing: LedgerEntry; readonly viaIntent: true; readonly viaSubject: { readonly authId: string } } | null; readonly writeReceipt: (receipt: RunReceipt, environment: Readonly>) => void; readonly runJournalReceipt: (journal: RunJournal) => RunReceipt; readonly relativeStatePath: (path: string, environment: Readonly>) => string; @@ -139,6 +141,7 @@ export function makeConfirmedWritePlatform(kernel: ConfirmedWriteKernel, origina isDispatchProgress, ledgerPath, acquireConfirmedWriteLedgers, + recheckConfirmedWriteSubjectFence, writeReceipt, runJournalReceipt, relativeStatePath, @@ -565,6 +568,7 @@ export function makeConfirmedWritePlatform(kernel: ConfirmedWriteKernel, origina risk, inputHash, auth: durableWriteAuth(), + ...durableWriteAuthSubject(), contract: contract.transport === "portable-provider-plugin" || contract.transport === "local-cli" ? contract @@ -625,6 +629,7 @@ export function makeConfirmedWritePlatform(kernel: ConfirmedWriteKernel, origina adapterId: adapter.id, authId: auth.id, operationId: invocation.operationId, inputHashes: legacyInputHash === inputHash ? [inputHash] : [inputHash, legacyInputHash], ...(options.duplicateRisk === undefined ? {} : { duplicateIntentHash: options.duplicateRisk.intentHash }), + ...durableWriteAuthSubject(), } satisfies ConfirmedWriteIntent, entry: { schemaVersion: options.duplicateRisk === undefined ? 2 : 3, @@ -639,6 +644,7 @@ export function makeConfirmedWritePlatform(kernel: ConfirmedWriteKernel, origina // The intent fence is claimed first, so a reconnect or a manifest // revision cannot move the same effect to a fresh hash-keyed ledger. acquireLedger: (request: { readonly path: string; readonly entry: LedgerEntry; readonly alternatePaths?: readonly string[]; readonly intent: ConfirmedWriteIntent }) => attempt("journal", () => acquireConfirmedWriteLedgers(request, options.environment, observedTime())), + recheckSubjectFence: (intent: ConfirmedWriteIntent) => attempt("journal", () => recheckConfirmedWriteSubjectFence(intent, runId, options.environment)), ledgerRelativePath: (path: string) => attempt("journal", () => relativeStatePath(path, options.environment)), readReceipt: (id: string) => attempt("projection", () => readRunReceipt(id, options.environment)), storeCapsule: attempt("journal", () => writeRecoveryCapsule({ diff --git a/src/confirmed-write-program.ts b/src/confirmed-write-program.ts index 87cf2b6a..2fdadfb2 100644 --- a/src/confirmed-write-program.ts +++ b/src/confirmed-write-program.ts @@ -44,6 +44,8 @@ export function priorRunDisposition( readonly existing: LedgerEntry; readonly viaIntent?: true; readonly viaAlternatePath?: boolean; + /** The blocking run ran under another locator that recorded the same provider subject. */ + readonly viaSubject?: { readonly authId: string }; }, current: { readonly inputHash: string; @@ -58,6 +60,12 @@ export function priorRunDisposition( return { kind: "refuse", message: "idempotency key was already used in a different action scope" }; } const prior = existing.runId; + // A run under another locator that recorded the same provider subject is + // unsettled, since only such runs fence across locators. It never replays, + // and it is reconciled under its own locator. + if (viaIntent && acquired.viaSubject !== undefined) { + return { kind: "refuse", message: `a prior attempt (${prior}) may have reached the provider under auth locator '${acquired.viaSubject.authId}', which records the same provider subject as '${current.authId}'; inspect 'ghostget runs show ${prior}' and reconcile it under '${acquired.viaSubject.authId}' before retrying` }; + } // The realm is the locator ID, and journals keep no account subject, so // other auth bytes may be another account. Such a run never replays as // this account's result. Reconciling it needs its exact auth record, or a @@ -147,6 +155,21 @@ function prepareAndExecute( yield* finalizePreDispatchFailure(state, "idempotency claim could not be bound to the run journal"); return yield* wrapped(claimed.left, "refusing to start a remote write because its run journal could not claim the idempotency ledger"); } + // Recheck the provider-subject fence now that this run's claim is on + // record, so a run of the same subject under another locator that passed + // its scan concurrently cannot also dispatch. + const subject = yield* Effect.either(state.recheckSubjectFence(request.intent)); + if (Either.isLeft(subject)) { + yield* finalizePreDispatchFailure(state, "idempotency state could not be inspected before dispatch"); + return yield* wrapped(subject.left, "refusing to start a remote write because its idempotency state could not be inspected"); + } + if (subject.right !== null) { + yield* finalizePreDispatchFailure(state, "another run already owns this idempotency scope"); + const disposition = priorRunDisposition(subject.right, { + inputHash: state.inputHash, adapterHash: state.adapter.hash, authHash: state.auth.hash, authId: state.auth.id, + }); + return yield* refuse("journal", disposition.kind === "refuse" ? disposition.message : "another run already owns this idempotency scope"); + } const recovery = yield* Effect.either(Effect.gen(function*() { yield* state.storeCapsule; yield* state.record({ type: "recovery-stored", at: yield* state.clock() }); diff --git a/src/ghostget.ts b/src/ghostget.ts index 5518b214..fc2ea6fe 100644 --- a/src/ghostget.ts +++ b/src/ghostget.ts @@ -3333,7 +3333,9 @@ async function runCommand( throw new Error("--duplicate-risk-of requires an explicit --preview"); } // A cache-only invocation is a read path: it binds the account's current - // auth incarnation and never creates one. + // auth incarnation and never creates one. `--projection-identity-only` is + // the SDK's identity preflight for a live invoke, so it is execution + // preparation and may create a missing incarnation (D14). const invocation = (arguments_.cacheOnly ? prepareReadInvocation : prepareInvocation)( arguments_.adapterId, arguments_.operationId, diff --git a/src/read-path-preparation.test.ts b/src/read-path-preparation.test.ts index 9a09a0a6..8e705ccc 100644 --- a/src/read-path-preparation.test.ts +++ b/src/read-path-preparation.test.ts @@ -165,4 +165,50 @@ describe("read-path preparation binds the current incarnation without creating o expect(description.coordinate.authIncarnation).toBe(invocation.readProjectionAuthIdentityHash!); expect(readFileSync(incarnationPath(root, "x-main"))).toEqual(created); }); + + // D14 decision: `invoke --projection-identity-only` is the SDK's identity + // preflight for a live invoke, so it is execution preparation and stays an + // admitted incarnation creator. The cache-only read beside it creates none. + test("invoke --projection-identity-only is execution preparation that creates a missing incarnation; --cache-only still creates none", async () => { + const { root, environment } = accounts(); + rmSync(incarnationPath(root, "x-main")); + const run = async (flag: "--cache-only" | "--projection-identity-only") => { + const stdout: string[] = []; + const stderr: string[] = []; + let cacheReads = 0; + const code = await main( + ["invoke", "x", "messaging.list", "--input", JSON.stringify(xRead.input), "--auth", "x-main", flag, "--json"], + environment, + { stdout: (value) => stdout.push(value), stderr: (value) => stderr.push(value) }, + { + providerPluginRegistry, + readCachedPreparedCapability: () => { cacheReads += 1; throw new Error("stubbed cache read"); }, + }, + ); + return { code, stdout: stdout.join(""), stderr: stderr.join(""), cacheReads }; + }; + + const before = fingerprint(root); + const cacheOnly = await run("--cache-only"); + expect(cacheOnly.code).not.toBe(0); + expect(cacheOnly.stderr).toContain("auth locator x-main has no lifetime identity yet"); + expect(existsSync(incarnationPath(root, "x-main"))).toBeFalse(); + expect(fingerprint(root)).toEqual(before); + + const identity = await run("--projection-identity-only"); + expect(identity.stderr).toBe(""); + expect(identity.code).toBe(0); + expect(identity.cacheReads).toBe(0); + const view = JSON.parse(identity.stdout) as { readonly source: string; readonly authIdentity: string }; + expect(view.source).toBe("projection-identity"); + expect(existsSync(incarnationPath(root, "x-main"))).toBeTrue(); + const created = readFileSync(incarnationPath(root, "x-main")); + // The read path then binds the identity the preflight created, without changing it. + const description = describeOperationPermission("x", "messaging.list", "x-main", { environment, registry: providerPluginRegistry }); + expect(description.coordinate.authIncarnation).toBe(view.authIdentity); + const retried = await run("--cache-only"); + expect(retried.cacheReads).toBe(1); + expect(retried.stderr).not.toContain("no lifetime identity"); + expect(readFileSync(incarnationPath(root, "x-main"))).toEqual(created); + }); }); diff --git a/src/run-journal.test.ts b/src/run-journal.test.ts index 3feef4e8..318ed8a1 100644 --- a/src/run-journal.test.ts +++ b/src/run-journal.test.ts @@ -68,6 +68,7 @@ function initial(overrides: { readonly hasPlanAssets?: boolean; readonly leaseUntil?: string; readonly contract?: RunJournalContract; + readonly authSubject?: string; } = {}): RunJournal { return initialRunJournal({ runId: "11111111-1111-4111-8111-111111111111", @@ -85,6 +86,7 @@ function initial(overrides: { hash: "d".repeat(64), kind: "cookies-file", }, + ...(overrides.authSubject === undefined ? {} : { authSubject: overrides.authSubject }), contract: overrides.contract ?? { transport: "web-session-api", hash: "e".repeat(64), @@ -568,6 +570,20 @@ describe("run journal reducer", () => { expect(invoked).toBeFalse(); }); + test("records an optional provider subject, parses it strictly, and keeps journals without one valid", () => { + const legacy = initial(); + expect(Object.hasOwn(legacy, "authSubject")).toBeFalse(); + expect(parseRunJournal(JSON.parse(JSON.stringify(legacy)) as unknown)).toEqual(legacy); + + const withSubject = initial({ authSubject: "1234567890" }); + expect(withSubject.authSubject).toBe("1234567890"); + expect(parseRunJournal(JSON.parse(JSON.stringify(withSubject)) as unknown)).toEqual(withSubject); + + for (const malformed of ["", " 1234567890", "has space", "a\u0000b", "x".repeat(513), 42, null, ["1234567890"]]) { + expect(() => parseRunJournal({ ...legacy, authSubject: malformed })).toThrow("run journal auth subject is malformed"); + } + }); + test("enforces the dispatch ceiling before persistence", () => { expect(() => initial({ plannedDispatches: 26 })).toThrow( "run journal dispatch is malformed", diff --git a/src/run-journal.ts b/src/run-journal.ts index 0f2b109e..a16c1f29 100644 --- a/src/run-journal.ts +++ b/src/run-journal.ts @@ -1,7 +1,7 @@ import { createHash } from "node:crypto"; import { join } from "node:path"; -import type { GhostgetAuth } from "./auth"; +import { normalizeAuthSubject, type GhostgetAuth } from "./auth"; import { canonicalJson } from "./canonical-json"; import type { OperationRisk } from "./model"; import { @@ -115,6 +115,12 @@ export type RunJournal = { readonly hash: string; readonly kind: GhostgetAuth["kind"]; }; + /** + * The provider subject the auth record named when the run started. Journals + * written before this field existed carry none. The confirmed-write fence + * uses it to fence the same subject across auth locators. + */ + readonly authSubject?: string; readonly contract: RunJournalContract; readonly duplicateIntent?: DuplicateIntentV1; readonly duplicateSuccessor?: DuplicateSuccessorV1; @@ -156,6 +162,7 @@ export type StartRunJournal = { readonly risk: Extract; readonly inputHash: string; readonly auth: RunJournal["auth"]; + readonly authSubject?: string; readonly contract: RunJournalContract; readonly duplicateIntent?: DuplicateIntentV1; readonly plannedDispatches: number; @@ -425,6 +432,15 @@ function parseAuth(value: unknown): RunJournal["auth"] { }; } +function parseAuthSubject(value: unknown): string { + if (typeof value !== "string") throw new Error("run journal auth subject is malformed"); + try { + return normalizeAuthSubject(value); + } catch { + throw new Error("run journal auth subject is malformed"); + } +} + function parseContract(value: unknown): RunJournalContract { const record = dataRecord(value, "run journal contract"); if (record.transport === "portable-provider-plugin") { @@ -778,6 +794,7 @@ export function parseRunJournal(value: unknown): RunJournal { "finalOrigin", "error", ]; + if (Object.hasOwn(record, "authSubject")) keys.push("authSubject"); if (Object.hasOwn(record, "duplicateIntent")) keys.push("duplicateIntent"); if (Object.hasOwn(record, "duplicateSuccessor")) keys.push("duplicateSuccessor"); if (Object.hasOwn(record, "supersededBy")) keys.push("supersededBy"); @@ -841,6 +858,9 @@ export function parseRunJournal(value: unknown): RunJournal { risk: record.risk, inputHash: digest(record.inputHash, "run journal input hash"), auth: parseAuth(record.auth), + ...(Object.hasOwn(record, "authSubject") + ? { authSubject: parseAuthSubject(record.authSubject) } + : {}), contract: parseContract(record.contract), ...(Object.hasOwn(record, "duplicateIntent") ? { @@ -932,6 +952,7 @@ export function initialRunJournal(value: StartRunJournal): RunJournal { risk: value.risk, inputHash: value.inputHash, auth: value.auth, + ...(value.authSubject === undefined ? {} : { authSubject: value.authSubject }), contract: value.contract, ...(value.duplicateIntent === undefined ? {} diff --git a/src/runtime.ts b/src/runtime.ts index e8de7b99..907419ea 100644 --- a/src/runtime.ts +++ b/src/runtime.ts @@ -3365,10 +3365,51 @@ function journalFencesIntent( : null; } +/** + * Whether `journal` is an unsettled run of the same provider target, + * operation, canonical input, and duplicate-risk narrowing as `intent`, under + * another auth locator that recorded the same provider subject. Journals + * without a subject, and intents whose auth record names none, never match, + * so they keep the per-locator fence. A claimed run that has not yet crossed + * its dispatch boundary counts as unsettled. + */ +function journalFencesSubject(journal: RunJournal, intent: ConfirmedWriteIntent): boolean { + return intent.authSubject !== undefined + && journal.authSubject === intent.authSubject + && journal.auth.id !== intent.authId + && journal.adapter.id === intent.adapterId + && journal.operation === intent.operationId + && intent.inputHashes.includes(journal.inputHash) + && journal.duplicateIntent?.intentHash === intent.duplicateIntentHash + && journal.ledgerState !== "unclaimed" + && journal.ledgerState !== "released" + && journal.ledgerState !== "succeeded"; +} + +/** + * The unsettled run under another locator with the same provider subject that + * fences `intent` against run `runId`, or null. + * + * @internal Exported for the confirmed-write platform and the fence model's + * trace replay. + */ +export function subjectFenceBlocker( + journals: readonly RunJournal[], + intent: ConfirmedWriteIntent, + runId: string, +): RunJournal | null { + if (intent.authSubject === undefined) return null; + for (const journal of journals) { + if (journal.runId !== runId && journalFencesSubject(journal, intent)) return journal; + } + return null; +} + /** * The journal that fences `intent` against run `runId`, or null. An unsettled * journal wins over a fulfilled one; among fulfilled journals, the one whose - * dedupe window ends last. + * dedupe window ends last. An unsettled run under another locator that + * recorded the same provider subject also fences it. * * @internal Exported only for the fence model's trace replay. */ @@ -3382,7 +3423,7 @@ export function intentFenceBlocker( for (const journal of journals) { if (journal.runId === runId) continue; const fence = journalFencesIntent(journal, intent, now); - if (fence === "unsettled") return journal; + if (fence === "unsettled" || journalFencesSubject(journal, intent)) return journal; if ( fence === "fulfilled" && (fulfilled === null || Date.parse(journal.dedupeExpiresAt) > Date.parse(fulfilled.dedupeExpiresAt)) @@ -3391,6 +3432,42 @@ export function intentFenceBlocker( return fulfilled; } +/** Every run journal; an invalid one leaves the intent unresolved. */ +function confirmedWriteJournals( + environment: Readonly>, +): readonly RunJournal[] { + return listRunJournalSnapshots(environment).map((candidate) => { + if ("invalid" in candidate) { + throw new Error("invalid run journals make the confirmed-write intent unresolved"); + } + return candidate.journal; + }); +} + +/** + * Recheck the provider-subject fence after run `runId` recorded its ledger + * claim and before it may dispatch. The pre-claim scan and the claim are + * separate steps, and each locator claims its own intent ledger, so two runs + * of one subject under two locators could both pass the scan. Each records + * its claim before this recheck, so at least one of them sees the other and + * refuses; both may refuse. Returns the blocking run's ledger entry and + * locator, or null. + * + * @internal Exported for the confirmed-write platform and the fence model's + * trace replay. + */ +export function recheckConfirmedWriteSubjectFence( + intent: ConfirmedWriteIntent, + runId: string, + environment: Readonly>, +): { readonly existing: LedgerEntry; readonly viaIntent: true; readonly viaSubject: { readonly authId: string } } | null { + if (intent.authSubject === undefined) return null; + const blocker = subjectFenceBlocker(confirmedWriteJournals(environment), intent, runId); + return blocker === null + ? null + : { existing: runJournalLedgerEntry(blocker), viaIntent: true, viaSubject: { authId: blocker.auth.id } }; +} + /** * Check and claim the intent fence before the hash-keyed ledger. Journals * recorded before this fence existed have no intent ledger, so every @@ -3405,19 +3482,23 @@ function acquireIntentLedger( now: Date, ): | { readonly acquired: true; readonly snapshot: LedgerSnapshot } - | { readonly acquired: false; readonly existing: LedgerEntry; readonly viaIntent: true } { + | { + readonly acquired: false; + readonly existing: LedgerEntry; + readonly viaIntent: true; + readonly viaSubject?: { readonly authId: string }; + } { if (!intent.inputHashes.includes(entry.inputHash)) { throw new Error("confirmed-write intent does not bind its ledger input"); } - const journals = listRunJournalSnapshots(environment).map((candidate) => { - if ("invalid" in candidate) { - throw new Error("invalid run journals make the confirmed-write intent unresolved"); - } - return candidate.journal; - }); - const blocker = intentFenceBlocker(journals, intent, entry.runId, now); + const blocker = intentFenceBlocker(confirmedWriteJournals(environment), intent, entry.runId, now); if (blocker !== null) { - return { acquired: false, existing: runJournalLedgerEntry(blocker), viaIntent: true }; + return { + acquired: false, + existing: runJournalLedgerEntry(blocker), + viaIntent: true, + ...(blocker.auth.id === intent.authId ? {} : { viaSubject: { authId: blocker.auth.id } }), + }; } const claimed = acquireLedger( intentLedgerPath(intent.adapterId, intent.authId, intent.operationId, entry.inputHash, environment, intent.duplicateIntentHash), @@ -5497,6 +5578,7 @@ async function confirmInvocationCore( isDispatchProgress, ledgerPath: confirmedWriteLedgerPath, acquireConfirmedWriteLedgers, + recheckConfirmedWriteSubjectFence, writeReceipt, runJournalReceipt, relativeStatePath, diff --git a/verification/claims.json b/verification/claims.json index de7176df..c4f7b34f 100644 --- a/verification/claims.json +++ b/verification/claims.json @@ -579,7 +579,7 @@ { "guide": "AGENTS.md", "anchor": "No writes on read", - "digest": "0141cebc7ddf03716d516fc5d31fe9621892e18e8e62a2393776821fcdda231b", + "digest": "9404228819ce247f0922561863a4f36f84cbe071fa0a6aa4d9ce43751cbb8d16", "claims": [ "menu-bar-snapshot-read-only", "no-writes-on-read-paths", @@ -7189,6 +7189,33 @@ "notVerified": [ "No automated check inspects `website/` for authenticated surfaces, credential handling, or runtime features; review alone enforces this boundary." ] + }, + { + "id": "intent-fence-subject-across-locators", + "statement": "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.", + "area": "mutations", + "source": { + "path": "docs/effect-confirmed-write-runtime.md", + "quote": "the fence also refuses while an unsettled run of the same provider target, operation, and canonical input" + }, + "layer": "quint", + "status": "evidenced", + "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" + ], + "notVerified": [ + "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." + ] } ] } diff --git a/verification/quint/fence.qnt b/verification/quint/fence.qnt index 4165eedf..010092c7 100644 --- a/verification/quint/fence.qnt +++ b/verification/quint/fence.qnt @@ -29,6 +29,18 @@ // recovery material (releaseReconciledRunRecovery), so it is never // reconciled. A successor can itself become the source of a later successor. // +// Each run confirms under one of two auth locators and records the provider +// subject its auth record named, or none. The locator is the account realm: +// runs of one locator share one intent ledger. Two locators that record the +// same subject name one provider account, so an unsettled run of that +// subject also fences the other locator (journalFencesSubject). Each locator +// claims its own intent ledger, so the fence is a scan before the claim and +// a recheck after the claim is on record, just before the dispatch boundary +// (recheckConfirmedWriteSubjectFence). A run of either locator with no +// subject keeps the per-locator fence. Subjects can be typed by the +// operator, so matching subjects over-approximate one account: the fence +// may refuse more, never less. +// // Pre-fix variants: // - D1 (stepHashKeyed): the fence and the ledger key include the auth and // adapter hashes, so a reconnect or an upgrade opens a fresh fence. @@ -39,8 +51,13 @@ // one accepted risk can cover any number of duplicates. // - stepElectInFlight: a successor may name a source that is still in // flight, so a run that later succeeds is duplicated. +// - stepSubjectBlind: the fence ignores the recorded subject, as it did +// before journals recorded one, so one account connected under two +// locators dispatches the same intent twice. // -// Not modelled: the dedupe window's expiry, the hash-keyed ledger that is +// Not modelled: a fulfilled run of the same subject under another locator +// (it does not fence, by design), one auth generation per locator (one +// counter serves both), the dedupe window's expiry, the hash-keyed ledger that is // claimed after the intent ledger, a successor whose election fails at its // dispatch boundary (the model disables that dispatch; production fails the // run before any request), partial multi-dispatch runs, and journals from @@ -49,6 +66,9 @@ module fence { pure val RUNS: Set[str] = Set("r1", "r2", "r3") pure val OUTCOMES: Set[str] = Set("succeeded", "applied", "lost") pure val MAX_GENERATION: int = 1 + pure val LOCATORS: Set[str] = Set("a", "b") + // "" is a run whose auth record named no provider subject. + pure val SUBJECTS: Set[str] = Set("", "s") // Each run's journal: phase "none" means no journal exists yet. var phase: str -> str @@ -57,6 +77,10 @@ module fence { // The auth generation and manifest revision each run was bound to. var runAuth: str -> int var runRev: str -> int + // The auth locator each run confirmed under, and the provider subject its + // journal recorded: "" for none (or for a run without a journal). + var runLoc: str -> str + var runSubj: str -> str // The duplicate-risk source each run names: "" for the base intent. var source: str -> str // The successor each run elected as a source: "" for none. @@ -65,8 +89,9 @@ module fence { var rev: int // Runs that scanned without finding a fence and may now claim. var scanned: Set[str] - // Intent ledger files: (auth key, revision key, source key, holder run). - var ledger: Set[(int, int, str, str)] + // Intent ledger files: (auth key, revision key, locator, source key, + // holder run). + var ledger: Set[(int, int, str, str, str)] // Runs that crossed their dispatch boundary, and the provider's truth. var dispatched: Set[str] var applied: Set[str] @@ -81,6 +106,8 @@ module fence { ledgerState' = RUNS.mapBy(r => "none"), runAuth' = RUNS.mapBy(r => 0), runRev' = RUNS.mapBy(r => 0), + runLoc' = RUNS.mapBy(r => ""), + runSubj' = RUNS.mapBy(r => ""), source' = RUNS.mapBy(r => ""), elected' = RUNS.mapBy(r => ""), authGen' = 0, @@ -94,17 +121,30 @@ module fence { result' = "none", } - // Whether journal `s` is the same intent as run `r`, which names source - // `src` and is bound to auth generation `a` and revision `v`. The fixed - // fence compares IDs and the successor source only; the D1 variant also - // compares the hashed bytes. - def sameIntent(s: str, r: str, src: str, a: int, v: int, hashKeyed: bool): bool = - s != r and source.get(s) == src and (not(hashKeyed) or (runAuth.get(s) == a and runRev.get(s) == v)) - - // journalFencesIntent: "unsettled", "fulfilled", or "none". - def fenceOf(s: str, r: str, src: str, a: int, v: int, hashKeyed: bool): str = - if (not(sameIntent(s, r, src, a, v, hashKeyed))) "none" - else if (ledgerState.get(s) == "pending" or ledgerState.get(s) == "indeterminate") "unsettled" + // Whether journal `s` is the same intent as run `r`, which confirms under + // locator `l`, names source `src`, and is bound to auth generation `a` and + // revision `v`. The fixed fence compares IDs and the successor source only; + // the D1 variant also compares the hashed bytes. + def sameIntent(s: str, r: str, src: str, l: str, a: int, v: int, hashKeyed: bool): bool = + s != r and source.get(s) == src and runLoc.get(s) == l + and (not(hashKeyed) or (runAuth.get(s) == a and runRev.get(s) == v)) + + def unsettledLedger(s: str): bool = + ledgerState.get(s) == "pending" or ledgerState.get(s) == "indeterminate" + + // journalFencesSubject: journal `s` is an unsettled run of the same source + // under another locator that recorded subject `j`, the subject of run `r`. + // The stepSubjectBlind variant never matches. + def subjectFences(s: str, r: str, src: str, l: str, j: str, subjectBlind: bool): bool = + not(subjectBlind) and s != r and j != "" and runSubj.get(s) == j and runLoc.get(s) != l + and source.get(s) == src and unsettledLedger(s) + + // journalFencesIntent and journalFencesSubject: "unsettled", "fulfilled", + // or "none". + def fenceOf(s: str, r: str, src: str, l: str, j: str, a: int, v: int, hashKeyed: bool, subjectBlind: bool): str = + if (subjectFences(s, r, src, l, j, subjectBlind)) "unsettled" + else if (not(sameIntent(s, r, src, l, a, v, hashKeyed))) "none" + else if (unsettledLedger(s)) "unsettled" else if (ledgerState.get(s) == "succeeded") "fulfilled" else "none" @@ -112,8 +152,9 @@ module fence { def fulfilledResult(s: str, a: int): str = if (runAuth.get(s) == a) "replayed" else "withheld" - def ledgerKey(r: str, hashKeyed: bool): (int, int, str) = - if (hashKeyed) (runAuth.get(r), runRev.get(r), source.get(r)) else (0, 0, source.get(r)) + def ledgerKey(r: str, hashKeyed: bool): (int, int, str, str) = + if (hashKeyed) (runAuth.get(r), runRev.get(r), runLoc.get(r), source.get(r)) + else (0, 0, runLoc.get(r), source.get(r)) def bound(r: str): bool = runAuth.get(r) == authGen and runRev.get(r) == rev @@ -131,18 +172,22 @@ module fence { // A refused confirm finishes its own run failed before any dispatch. A // run refused at its scan is bound here; a run refused at its claim keeps // the binding it took at its scan. - action refuse(r: str, src: str, reported: str): bool = all { + // A run refused at its subject recheck already holds its intent ledger, + // which the release removes. + action refuse(r: str, src: str, l: str, j: str, reported: str): bool = all { phase' = phase.set(r, "terminal"), status' = status.set(r, "failed"), ledgerState' = ledgerState.set(r, "released"), runAuth' = if (phase.get(r) == "none") runAuth.set(r, authGen) else runAuth, runRev' = if (phase.get(r) == "none") runRev.set(r, rev) else runRev, + runLoc' = if (phase.get(r) == "none") runLoc.set(r, l) else runLoc, + runSubj' = if (phase.get(r) == "none") runSubj.set(r, j) else runSubj, source' = if (phase.get(r) == "none") source.set(r, src) else source, elected' = elected, authGen' = authGen, rev' = rev, scanned' = scanned.exclude(Set(r)), - ledger' = ledger, + ledger' = ledger.filter(e => e._5 != r), dispatched' = dispatched, applied' = applied, reconciled' = reconciled, @@ -150,23 +195,26 @@ module fence { result' = reported, } - // A confirm starts its run journal, bound to the current auth record and - // manifest revision and naming its successor source `src` ("" for none), - // and scans the other journals for a fence. - action scanFor(r: str, src: str, hashKeyed: bool): bool = { - val fulfilledBy = RUNS.filter(s => fenceOf(s, r, src, authGen, rev, hashKeyed) == "fulfilled") + // A confirm starts its run journal under locator `l` with subject `j`, + // bound to the current auth record and manifest revision and naming its + // successor source `src` ("" for none), and scans the other journals for a + // fence. + action scanFor(r: str, src: str, l: str, j: str, hashKeyed: bool, subjectBlind: bool): bool = { + val fulfilledBy = RUNS.filter(s => fenceOf(s, r, src, l, j, authGen, rev, hashKeyed, subjectBlind) == "fulfilled") all { phase.get(r) == "none", - if (RUNS.exists(s => fenceOf(s, r, src, authGen, rev, hashKeyed) == "unsettled")) - refuse(r, src, "refused") + if (RUNS.exists(s => fenceOf(s, r, src, l, j, authGen, rev, hashKeyed, subjectBlind) == "unsettled")) + refuse(r, src, l, j, "refused") else if (fulfilledBy != Set()) - refuse(r, src, if (fulfilledBy.exists(s => fulfilledResult(s, authGen) == "replayed")) "replayed" else "withheld") + refuse(r, src, l, j, if (fulfilledBy.exists(s => fulfilledResult(s, authGen) == "replayed")) "replayed" else "withheld") else all { phase' = phase.set(r, "prepared"), status' = status.set(r, "pending"), ledgerState' = ledgerState.set(r, "unclaimed"), runAuth' = runAuth.set(r, authGen), runRev' = runRev.set(r, rev), + runLoc' = runLoc.set(r, l), + runSubj' = runSubj.set(r, j), source' = source.set(r, src), elected' = elected, authGen' = authGen, @@ -182,24 +230,27 @@ module fence { } } - action scan(r: str, hashKeyed: bool): bool = scanFor(r, "", hashKeyed) + action scan(r: str, l: str, j: str, hashKeyed: bool, subjectBlind: bool): bool = + scanFor(r, "", l, j, hashKeyed, subjectBlind) // A confirm of a duplicate-risk successor of `s`. Preview and confirmation - // both refuse unless `s` is electable, so no journal starts otherwise. - action scanSuccessor(r: str, s: str, hashKeyed: bool, inFlight: bool): bool = all { + // both refuse unless `s` is electable, so no journal starts otherwise. The + // source binds the current auth record, so the successor runs under its + // locator and subject. + action scanSuccessor(r: str, s: str, hashKeyed: bool, inFlight: bool, subjectBlind: bool): bool = all { s != r, electable(s, inFlight), - scanFor(r, s, hashKeyed), + scanFor(r, s, runLoc.get(s), runSubj.get(s), hashKeyed, subjectBlind), } action claim(r: str, hashKeyed: bool): bool = { val key = ledgerKey(r, hashKeyed) - val holders = ledger.filter(e => (e._1, e._2, e._3) == key).map(e => e._4) + val holders = ledger.filter(e => (e._1, e._2, e._3, e._4) == key).map(e => e._5) all { phase.get(r) == "prepared", scanned.contains(r), if (holders != Set()) - refuse(r, source.get(r), + refuse(r, source.get(r), runLoc.get(r), runSubj.get(r), if (holders.exists(s => ledgerState.get(s) == "succeeded")) if (holders.exists(s => fulfilledResult(s, runAuth.get(r)) == "replayed")) "replayed" else "withheld" else "refused") @@ -209,12 +260,14 @@ module fence { ledgerState' = ledgerState.set(r, "pending"), runAuth' = runAuth, runRev' = runRev, + runLoc' = runLoc, + runSubj' = runSubj, source' = source, elected' = elected, authGen' = authGen, rev' = rev, scanned' = scanned.exclude(Set(r)), - ledger' = ledger.union(Set((key._1, key._2, key._3, r))), + ledger' = ledger.union(Set((key._1, key._2, key._3, key._4, r))), dispatched' = dispatched, applied' = applied, reconciled' = reconciled, @@ -224,30 +277,39 @@ module fence { } } - // A run crosses its dispatch boundary. A successor first elects its - // source, which must still be unsettled and unelected; the stepUnelected - // variant skips the election. - action dispatch(r: str, elects: bool): bool = { + // The run crosses its dispatch boundary; a successor elects its source. + action crossBoundary(r: str, src: str, elects: bool): bool = all { + phase' = phase.set(r, "dispatching"), + status' = status, + ledgerState' = ledgerState, + runAuth' = runAuth, + runRev' = runRev, + runLoc' = runLoc, + runSubj' = runSubj, + source' = source, + elected' = if (src != "" and elects) elected.set(src, r) else elected, + authGen' = authGen, + rev' = rev, + scanned' = scanned, + ledger' = ledger, + dispatched' = dispatched.union(Set(r)), + applied' = applied, + reconciled' = reconciled, + claimed' = claimed, + result' = if (src == "") "dispatched" else "elected", + } + + // A claimed run rechecks the subject fence, then crosses its dispatch + // boundary. A successor first elects its source, which must still be + // unsettled and unelected; the stepUnelected variant skips the election. + action dispatch(r: str, elects: bool, subjectBlind: bool): bool = { val src = source.get(r) all { phase.get(r) == "claimed", src == "" or (not(reconciled.contains(src)) and elected.get(src) == ""), - phase' = phase.set(r, "dispatching"), - status' = status, - ledgerState' = ledgerState, - runAuth' = runAuth, - runRev' = runRev, - source' = source, - elected' = if (src != "" and elects) elected.set(src, r) else elected, - authGen' = authGen, - rev' = rev, - scanned' = scanned, - ledger' = ledger, - dispatched' = dispatched.union(Set(r)), - applied' = applied, - reconciled' = reconciled, - claimed' = claimed, - result' = if (src == "") "dispatched" else "elected", + if (RUNS.exists(s => subjectFences(s, r, src, runLoc.get(r), runSubj.get(r), subjectBlind))) + refuse(r, src, runLoc.get(r), runSubj.get(r), "subject-refused") + else crossBoundary(r, src, elects), } } @@ -260,6 +322,8 @@ module fence { ledgerState' = ledgerState.set(r, final), runAuth' = runAuth, runRev' = runRev, + runLoc' = runLoc, + runSubj' = runSubj, source' = source, elected' = elected, authGen' = authGen, @@ -268,7 +332,10 @@ module fence { ledger' = ledger, dispatched' = dispatched, applied' = if (outcome == "lost") applied else applied.union(Set(r)), - reconciled' = reconciled, + // A settled elected successor supersedes its source: the source's + // recovery material releases and its outcome is durably known. An + // unelected successor's settle supersedes nothing. + reconciled' = if (outcome == "succeeded" and source.get(r) != "" and elected.get(source.get(r)) == r) reconciled.union(Set(source.get(r))) else reconciled, claimed' = claimed, result' = outcome, } @@ -280,6 +347,8 @@ module fence { ledgerState' = ledgerState, runAuth' = runAuth, runRev' = runRev, + runLoc' = runLoc, + runSubj' = runSubj, source' = source, elected' = elected, authGen' = nextAuth, @@ -318,6 +387,8 @@ module fence { ledgerState' = ledgerState, runAuth' = runAuth, runRev' = runRev, + runLoc' = runLoc, + runSubj' = runSubj, source' = source, elected' = elected, authGen' = authGen, @@ -326,7 +397,12 @@ module fence { ledger' = ledger, dispatched' = dispatched, applied' = applied, - reconciled' = reconciled.union(Set(r)), + // Settling an elected successor supersedes its source the same way a + // succeeded finish does; an unelected successor's settle does not. + reconciled' = if (source.get(r) != "" and elected.get(source.get(r)) == r) + reconciled.union(Set(r)).union(Set(source.get(r))) + else + reconciled.union(Set(r)), claimed' = claimed, result' = "settled", } @@ -342,12 +418,14 @@ module fence { ledgerState' = if (callerRelease) ledgerState.set(r, "released") else ledgerState, runAuth' = runAuth, runRev' = runRev, + runLoc' = runLoc, + runSubj' = runSubj, source' = source, elected' = elected, authGen' = authGen, rev' = rev, scanned' = scanned, - ledger' = if (callerRelease) ledger.filter(e => e._3 != r) else ledger, + ledger' = if (callerRelease) ledger.filter(e => e._5 != r) else ledger, dispatched' = dispatched, applied' = applied, reconciled' = if (callerRelease) reconciled.union(Set(r)) else reconciled, @@ -355,15 +433,17 @@ module fence { result' = if (callerRelease) "released" else "fence-retained", } - action stepWith(hashKeyed: bool, callerRelease: bool, elects: bool, inFlight: bool): bool = { + action stepWith(hashKeyed: bool, callerRelease: bool, elects: bool, inFlight: bool, subjectBlind: bool): bool = { nondet r = RUNS.oneOf() nondet o = OUTCOMES.oneOf() nondet s = RUNS.oneOf() + nondet l = LOCATORS.oneOf() + nondet j = SUBJECTS.oneOf() any { - scan(r, hashKeyed), - scanSuccessor(r, s, hashKeyed, inFlight), + scan(r, l, j, hashKeyed, subjectBlind), + scanSuccessor(r, s, hashKeyed, inFlight, subjectBlind), claim(r, hashKeyed), - dispatch(r, elects), + dispatch(r, elects, subjectBlind), finish(r, o), reconnect, upgrade, @@ -372,19 +452,23 @@ module fence { } } - action step = stepWith(false, false, true, false) + action step = stepWith(false, false, true, false, false) // D1: the fence is keyed by the auth and adapter bytes. - action stepHashKeyed = stepWith(true, false, true, false) + action stepHashKeyed = stepWith(true, false, true, false, false) // D2: a caller's not-applied claim releases the ledger. - action stepCallerRelease = stepWith(false, true, true, false) + action stepCallerRelease = stepWith(false, true, true, false, false) // A successor dispatches without electing its source. - action stepUnelected = stepWith(false, false, false, false) + action stepUnelected = stepWith(false, false, false, false, false) // A successor may name a source that is still in flight. - action stepElectInFlight = stepWith(false, false, true, true) + action stepElectInFlight = stepWith(false, false, true, true, false) + + // The fence ignores the recorded subject, so one account under two + // locators is two intents. + action stepSubjectBlind = stepWith(false, false, true, false, true) // A restriction of step for replay coverage: every transition it takes is // a step transition, but only r1 starts as a base intent and nobody @@ -394,30 +478,64 @@ module fence { nondet r = RUNS.oneOf() nondet o = OUTCOMES.oneOf() nondet s = RUNS.oneOf() + nondet l = LOCATORS.oneOf() + nondet j = SUBJECTS.oneOf() any { - all { r == "r1", scan(r, false) }, - scanSuccessor(r, s, false, false), + all { r == "r1", scan(r, l, j, false, false) }, + scanSuccessor(r, s, false, false, false), claim(r, false), - dispatch(r, true), + dispatch(r, true, false), finish(r, o), reconcile(r), } } - // The number of runs that elected a successor: each is one accepted - // duplicate risk. - val electedCount: int = RUNS.filter(s => elected.get(s) != "").size() + // A restriction of step for replay coverage: every transition it takes is + // a step transition, but every base intent records the one subject and + // nobody elects a successor, reconnects, or upgrades, so runs under the two + // locators race through the subject fence and its recheck. + action stepSubjects = { + nondet r = RUNS.oneOf() + nondet o = OUTCOMES.oneOf() + nondet s = RUNS.oneOf() + nondet l = LOCATORS.oneOf() + nondet j = Set("s").oneOf() + any { + scan(r, l, j, false, false), + claim(r, false), + dispatch(r, true, false), + finish(r, o), + reconcile(r), + } + } - // The plan's bound, |effects(intent)| <= 1 + |duplicateSuccessors(intent)|: - // at most one dispatch beyond the elected successors, and the provider - // applies only what was dispatched. - val successorBound: bool = dispatched.size() <= 1 + electedCount and applied.subseteq(dispatched) + // The plan's bound, |effects(intent)| <= 1 + |duplicateSuccessors(intent)|, + // for each locator's intent: at most one dispatch beyond the elected + // successors, and the provider applies only what was dispatched. A + // successor runs under its source's locator. + val successorBound: bool = and { + LOCATORS.forall(l => + dispatched.filter(r => runLoc.get(r) == l).size() + <= 1 + RUNS.filter(s => elected.get(s) != "" and runLoc.get(s) == l).size()), + applied.subseteq(dispatched), + } - // No intent is dispatched twice. A retry of a run is another dispatch of - // its intent, so an indeterminate run is never retried; a later dispatch - // is only a successor, which is a different intent. + // No intent is dispatched twice under one locator. A retry of a run is + // another dispatch of its intent, so an indeterminate run is never + // retried; a later dispatch is only a successor, which is a different + // intent. val noRetry: bool = - Set("").union(RUNS).forall(k => dispatched.filter(r => source.get(r) == k).size() <= 1) + Set("").union(RUNS).forall(k => LOCATORS.forall(l => + dispatched.filter(r => source.get(r) == k and runLoc.get(r) == l).size() <= 1)) + + // One recorded subject under two locators never has two dispatches of one + // intent unless one of them succeeded: a run dispatches only when no run of + // the same subject under another locator is in flight or unsettled. + val subjectExclusive: bool = + dispatched.forall(r => dispatched.forall(q => + r == q or source.get(r) != source.get(q) or runLoc.get(r) == runLoc.get(q) + or runSubj.get(r) == "" or runSubj.get(r) != runSubj.get(q) + or status.get(r) == "succeeded" or status.get(q) == "succeeded")) // Only an indeterminate run elects a successor: a duplicate is risked only // when the first outcome is unknown. @@ -429,6 +547,12 @@ module fence { val indeterminateStaysFenced: bool = RUNS.forall(r => status.get(r) == "indeterminate" implies ledgerState.get(r) == "indeterminate") - // All four, checked as one invariant so that Apalache runs once per step. - val fenceSafety: bool = successorBound and noRetry and electedFromIndeterminate and indeterminateStaysFenced + // All five, checked as one invariant so that Apalache runs once per step. + val fenceSafety: bool = and { + successorBound, + noRetry, + electedFromIndeterminate, + indeterminateStaysFenced, + subjectExclusive, + } } diff --git a/verification/quint/models.json b/verification/quint/models.json index 6832e46c..4e278744 100644 --- a/verification/quint/models.json +++ b/verification/quint/models.json @@ -72,6 +72,10 @@ { "step": "stepElectInFlight", "invariant": "fenceSafety" + }, + { + "step": "stepSubjectBlind", + "invariant": "fenceSafety" } ], "replay": {