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

[0thernet]

The confirmed-write fence keyed unsettled runs by auth locator ID, so the same provider account reached through two auth records could run a duplicate write. New journals now record the auth record's provider subject, and the 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 locator — in the journal scan and again in a recheck after the run's own claim is on record.

Claims moved

Claim	Layer	Evidence
intent-fence-subject-across-locators (new)	quint	fence.qnt models two locators that may each record one subject or none, checks fenceSafety over 5,000 simulated samples of up to 12 steps and Apalache to length 8, adds the stepSubjectBlind mutant, and replays through the production fence cores and the file-backed state layer

Evidence and how the evidence fails when broken

• Quint mutant. stepSubjectBlind drops the cross-locator subject check; both quint run and Apalache find the fenceSafety violation it allows.
• Replay. scripts/verification-fence-replay.test.ts replays every seeded trace through the production fence cores, then replays a greedy seven-trace cover — one that reaches every action result, including the new claim -> withheld and scan -> withheld — through the real file-backed state layer. A hash-keyed fence and a reconciler that releases on a caller's claim each diverge from the model traces on named states.
• Backwards compatibility. Journals written before authSubject existed parse unchanged and fence per locator only; parseAuthSubject normalizes and rejects malformed values. The fence can only refuse more.
• Tests. src/confirmed-write-intent-fence.test.ts gained per-locator subject cases (one test each) and strict journal subject parsing pins; src/run-journal.test.ts and src/read-path-preparation.test.ts cover the new field and the identity-preflight scope note.

Defects found

• The lane's own file-backed replay under-covered the new outcomes: withheld never appeared in a five-trace greedy cover. The cover is now sized at the measured minimum of seven traces (FILE_BACKED_TRACES = 7); eight fails because the greedy stops once coverage is complete.
• No production defect: the model and replay found the missing fence itself, which is the change.

Package budget

src/run-journal.ts, src/runtime.ts, and src/confirmed-write-*.ts ship, so the packed and unpacked measurements were rerun and scripts/package-budget.ts updated on this branch's earlier commits; the merge keeps main's measurement where the shipped set is unchanged by the merge itself.

CI cost

The Required verification job runs the enlarged fence.qnt with Apalache at length 8 (unchanged) and 5,000 simulation samples of up to 12 steps (was 3,000/10); the replay file adds the per-locator subject cases and two more file-backed cover traces, each a full bound-state-helper run.

Not covered

• Across locators the account realm is the recorded provider subject, which the operator may type: two locators recording one subject are fenced as one account even when they are not, so the cross-locator fence can only refuse more.
• Runs with no recorded subject — including every journal written before this field existed — fence per locator only; a succeeded run under another locator neither fences nor replays.
• Local validation on this host was partial under heavy load: typecheck, the claims render/check, the seeded-trace replay, and the cover test pass; the file-backed cover traces and the intent-fence suite's helper-heavy tests are delegated to the Required CI run on this head.

🤖 Generated with Claude Code

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated
ghostget	Building	Preview	Sep 25, 2026 4:54am UTC