From 5a293c8f3e1fc5c96b3ccdcce9e8ed093c87cf3d Mon Sep 17 00:00:00 2001 From: Callum Flack Date: Wed, 11 Nov 2026 17:12:40 +1000 Subject: [PATCH] docs(cli): map and verify state machines --- .../verify-collection-admission/SKILL.md | 26 ++ .../skills/verify-export-settlement/SKILL.md | 29 ++ .../verify-hosted-provisioning/SKILL.md | 28 ++ .../verify-mainnet-registration/SKILL.md | 27 ++ .../skills/verify-paid-read-recovery/SKILL.md | 105 ++++++ .../skills/verify-server-supervision/SKILL.md | 30 ++ .agents/skills/verify-setup-resume/SKILL.md | 105 ++++++ docs/STATE-MACHINE-INVENTORY.md | 71 ++++ docs/STATECHARTS.md | 357 ++++++++++++++++++ verification/collection-admission/README.md | 54 +++ verification/collection-admission/check.py | 169 +++++++++ .../models/CollectionAdmission.tla | 96 +++++ .../collection-admission/models/current.cfg | 4 + .../models/no-foreign-guard.cfg | 4 + .../models/no-owner-recheck.cfg | 4 + .../collection-admission/models/view.mjs | 71 ++++ verification/export-settlement/README.md | 64 ++++ verification/export-settlement/check.py | 242 ++++++++++++ .../fixtures/loopback-only.cjs | 11 + .../models/ExportSettlement.tla | 91 +++++ .../models/no-publish-guard.cfg | 6 + .../models/no-settle-guard.cfg | 6 + .../export-settlement/models/same-owner.cfg | 6 + .../export-settlement/models/two-owners.cfg | 6 + .../export-settlement/models/view.mjs | 55 +++ verification/hosted-provisioning/README.md | 58 +++ verification/hosted-provisioning/check.py | 171 +++++++++ .../models/HostedProvisioning.tla | 71 ++++ .../hosted-provisioning/models/current.cfg | 3 + .../models/refuse-provisioning-delete.cfg | 3 + .../hosted-provisioning/models/view.mjs | 46 +++ .../hosted-provisioning/replay.test.ts | 137 +++++++ verification/mainnet-registration/README.md | 56 +++ verification/mainnet-registration/check.py | 213 +++++++++++ .../models/MainnetRegistration.tla | 102 +++++ .../mainnet-registration/models/current.cfg | 10 + .../models/no-proof-identity.cfg | 10 + .../models/no-proof-wait.cfg | 10 + .../models/no-save-context.cfg | 10 + .../models/repeat-visible-registration.cfg | 10 + .../mainnet-registration/models/view.mjs | 69 ++++ verification/paid-read-recovery/README.md | 77 ++++ verification/paid-read-recovery/check.py | 160 ++++++++ .../fixtures/no-external-io.ts | 6 + .../fixtures/paid-read-crash-driver.ts | 99 +++++ .../fixtures/paid-read-process.test.ts | 118 ++++++ .../fixtures/vitest.formal.config.ts | 12 + .../paid-read-recovery/models/PaidRead.tla | 144 +++++++ .../models/concurrent-crash.cfg | 3 + .../paid-read-recovery/models/concurrent.cfg | 5 + .../models/no-read-lock.cfg | 3 + .../paid-read-recovery/models/no-refusal.cfg | 5 + .../paid-read-recovery/models/no-save.cfg | 5 + .../models/no-write-lock.cfg | 3 + .../paid-read-recovery/models/overview.mjs | 76 ++++ .../paid-read-recovery/models/single.cfg | 5 + .../paid-read-recovery/models/writers.cfg | 3 + verification/server-supervision/README.md | 36 ++ verification/server-supervision/check.py | 156 ++++++++ .../fixtures/stop-replay.txt | 42 +++ .../models/ServerSupervision.tla | 51 +++ .../server-supervision/models/backoff.cfg | 4 + .../server-supervision/models/current.cfg | 5 + .../models/no-backoff-fence.cfg | 4 + .../server-supervision/models/port-fence.cfg | 5 + .../server-supervision/models/view.mjs | 36 ++ verification/setup-resume/README.md | 74 ++++ verification/setup-resume/check.py | 167 ++++++++ .../setup-resume/fixtures/no-external-io.ts | 6 + .../fixtures/setup-overlap.test.ts | 187 +++++++++ .../fixtures/vitest.formal.config.ts | 13 + .../setup-resume/models/SetupResume.tla | 157 ++++++++ .../setup-resume/models/changed-context.cfg | 16 + verification/setup-resume/models/claim.cfg | 16 + .../setup-resume/models/concurrent-crash.cfg | 16 + .../setup-resume/models/concurrent.cfg | 16 + verification/setup-resume/models/details.mjs | 47 +++ .../setup-resume/models/existing-credit.cfg | 16 + .../setup-resume/models/new-consent-key.cfg | 16 + .../setup-resume/models/new-funding-key.cfg | 16 + .../setup-resume/models/no-context.cfg | 16 + .../setup-resume/models/no-persist.cfg | 16 + .../setup-resume/models/no-readiness.cfg | 16 + verification/setup-resume/models/overview.cfg | 16 + verification/setup-resume/models/overview.mjs | 96 +++++ .../models/post-known-operation.cfg | 16 + .../setup-resume/models/regress-funding.cfg | 16 + verification/setup-resume/models/single.cfg | 16 + 88 files changed, 4680 insertions(+) create mode 100644 .agents/skills/verify-collection-admission/SKILL.md create mode 100644 .agents/skills/verify-export-settlement/SKILL.md create mode 100644 .agents/skills/verify-hosted-provisioning/SKILL.md create mode 100644 .agents/skills/verify-mainnet-registration/SKILL.md create mode 100644 .agents/skills/verify-paid-read-recovery/SKILL.md create mode 100644 .agents/skills/verify-server-supervision/SKILL.md create mode 100644 .agents/skills/verify-setup-resume/SKILL.md create mode 100644 docs/STATE-MACHINE-INVENTORY.md create mode 100644 docs/STATECHARTS.md create mode 100644 verification/collection-admission/README.md create mode 100644 verification/collection-admission/check.py create mode 100644 verification/collection-admission/models/CollectionAdmission.tla create mode 100644 verification/collection-admission/models/current.cfg create mode 100644 verification/collection-admission/models/no-foreign-guard.cfg create mode 100644 verification/collection-admission/models/no-owner-recheck.cfg create mode 100644 verification/collection-admission/models/view.mjs create mode 100644 verification/export-settlement/README.md create mode 100644 verification/export-settlement/check.py create mode 100644 verification/export-settlement/fixtures/loopback-only.cjs create mode 100644 verification/export-settlement/models/ExportSettlement.tla create mode 100644 verification/export-settlement/models/no-publish-guard.cfg create mode 100644 verification/export-settlement/models/no-settle-guard.cfg create mode 100644 verification/export-settlement/models/same-owner.cfg create mode 100644 verification/export-settlement/models/two-owners.cfg create mode 100644 verification/export-settlement/models/view.mjs create mode 100644 verification/hosted-provisioning/README.md create mode 100644 verification/hosted-provisioning/check.py create mode 100644 verification/hosted-provisioning/models/HostedProvisioning.tla create mode 100644 verification/hosted-provisioning/models/current.cfg create mode 100644 verification/hosted-provisioning/models/refuse-provisioning-delete.cfg create mode 100644 verification/hosted-provisioning/models/view.mjs create mode 100644 verification/hosted-provisioning/replay.test.ts create mode 100644 verification/mainnet-registration/README.md create mode 100644 verification/mainnet-registration/check.py create mode 100644 verification/mainnet-registration/models/MainnetRegistration.tla create mode 100644 verification/mainnet-registration/models/current.cfg create mode 100644 verification/mainnet-registration/models/no-proof-identity.cfg create mode 100644 verification/mainnet-registration/models/no-proof-wait.cfg create mode 100644 verification/mainnet-registration/models/no-save-context.cfg create mode 100644 verification/mainnet-registration/models/repeat-visible-registration.cfg create mode 100644 verification/mainnet-registration/models/view.mjs create mode 100644 verification/paid-read-recovery/README.md create mode 100644 verification/paid-read-recovery/check.py create mode 100644 verification/paid-read-recovery/fixtures/no-external-io.ts create mode 100644 verification/paid-read-recovery/fixtures/paid-read-crash-driver.ts create mode 100644 verification/paid-read-recovery/fixtures/paid-read-process.test.ts create mode 100644 verification/paid-read-recovery/fixtures/vitest.formal.config.ts create mode 100644 verification/paid-read-recovery/models/PaidRead.tla create mode 100644 verification/paid-read-recovery/models/concurrent-crash.cfg create mode 100644 verification/paid-read-recovery/models/concurrent.cfg create mode 100644 verification/paid-read-recovery/models/no-read-lock.cfg create mode 100644 verification/paid-read-recovery/models/no-refusal.cfg create mode 100644 verification/paid-read-recovery/models/no-save.cfg create mode 100644 verification/paid-read-recovery/models/no-write-lock.cfg create mode 100644 verification/paid-read-recovery/models/overview.mjs create mode 100644 verification/paid-read-recovery/models/single.cfg create mode 100644 verification/paid-read-recovery/models/writers.cfg create mode 100644 verification/server-supervision/README.md create mode 100644 verification/server-supervision/check.py create mode 100644 verification/server-supervision/fixtures/stop-replay.txt create mode 100644 verification/server-supervision/models/ServerSupervision.tla create mode 100644 verification/server-supervision/models/backoff.cfg create mode 100644 verification/server-supervision/models/current.cfg create mode 100644 verification/server-supervision/models/no-backoff-fence.cfg create mode 100644 verification/server-supervision/models/port-fence.cfg create mode 100644 verification/server-supervision/models/view.mjs create mode 100644 verification/setup-resume/README.md create mode 100644 verification/setup-resume/check.py create mode 100644 verification/setup-resume/fixtures/no-external-io.ts create mode 100644 verification/setup-resume/fixtures/setup-overlap.test.ts create mode 100644 verification/setup-resume/fixtures/vitest.formal.config.ts create mode 100644 verification/setup-resume/models/SetupResume.tla create mode 100644 verification/setup-resume/models/changed-context.cfg create mode 100644 verification/setup-resume/models/claim.cfg create mode 100644 verification/setup-resume/models/concurrent-crash.cfg create mode 100644 verification/setup-resume/models/concurrent.cfg create mode 100644 verification/setup-resume/models/details.mjs create mode 100644 verification/setup-resume/models/existing-credit.cfg create mode 100644 verification/setup-resume/models/new-consent-key.cfg create mode 100644 verification/setup-resume/models/new-funding-key.cfg create mode 100644 verification/setup-resume/models/no-context.cfg create mode 100644 verification/setup-resume/models/no-persist.cfg create mode 100644 verification/setup-resume/models/no-readiness.cfg create mode 100644 verification/setup-resume/models/overview.cfg create mode 100644 verification/setup-resume/models/overview.mjs create mode 100644 verification/setup-resume/models/post-known-operation.cfg create mode 100644 verification/setup-resume/models/regress-funding.cfg create mode 100644 verification/setup-resume/models/single.cfg diff --git a/.agents/skills/verify-collection-admission/SKILL.md b/.agents/skills/verify-collection-admission/SKILL.md new file mode 100644 index 0000000..3eb1628 --- /dev/null +++ b/.agents/skills/verify-collection-admission/SKILL.md @@ -0,0 +1,26 @@ +--- +name: verify-collection-admission +description: Verify CLI collection admission across identity, Personal Server approval and foreign-server confirmation. Use for collection readiness or its identity recheck. +--- + +# Verify collection admission + +Read the [transition map, bounds and scratch controls](../../../verification/collection-admission/README.md). +The [checker](../../../verification/collection-admission/check.py) pins the +covered source and replay from main `a55d0a0006da6a743b6452796435afa6ed177dd8`. + +Automated collection must refuse another account's server before probing +credentials. A late approval response must not admit collection for an +account that changed while preparation was pending. + +Use Python 3.12 or newer, installed Node and Vitest, and pinned TLC 1.7.4 +with Java. Set `TLA2TOOLS` and `JAVA` to installed paths. Run from the CLI root. + +```sh +python3 verification/collection-admission/check.py --out "$(mktemp -d)/proof" +``` + +Require the current config and offline replay to pass. The named broken +configurations and their scratch source changes must fail on their intended +contracts. Read every outcome with Pstack `/statechart`. Reconcile new awaits +and owner boundaries before advancing the source pins. diff --git a/.agents/skills/verify-export-settlement/SKILL.md b/.agents/skills/verify-export-settlement/SKILL.md new file mode 100644 index 0000000..5bb0c63 --- /dev/null +++ b/.agents/skills/verify-export-settlement/SKILL.md @@ -0,0 +1,29 @@ +--- +name: verify-export-settlement +description: Verify queued export owner binding and generation settlement. Use for result publication, pending upload receipts, or retry and sync changes. +--- + +# Verify queued export settlement + +Read the [transition map, source pins, bounds and replay](../../../verification/export-settlement/README.md). +This proof was reconciled against CLI main `a55d0a0006da6a743b6452796435afa6ed177dd8` +and the integrated main snapshot recorded in its checker. + +A late upload must leave the current generation's receipt and visible result +aligned. A foreign collection must preserve pending bytes that belong to +another owner. The proof checks both with TLC 1.7.4 and the built CLI. + +Run from the CLI root with Python 3.12 or newer, the installed package +dependencies and Java. Set `TLA2TOOLS` and `JAVA` to installed tool paths. + +```sh +python3 verification/export-settlement/check.py +``` + +Require both current cases and offline CLI replays to pass. Require each +broken case and corresponding scratch source mutation to fail on the intended +contract. Read every TLA+ outcome with Pstack `/statechart`. + +When covered source changes, trace publication and settlement at their actual +lock and commit boundaries. Advance the source pins after the checked model, +broken controls and restored replays agree. diff --git a/.agents/skills/verify-hosted-provisioning/SKILL.md b/.agents/skills/verify-hosted-provisioning/SKILL.md new file mode 100644 index 0000000..14208bf --- /dev/null +++ b/.agents/skills/verify-hosted-provisioning/SKILL.md @@ -0,0 +1,28 @@ +--- +name: verify-hosted-provisioning +description: Verify hosted Personal Server resource ownership across create and delete. Use for Connect's server API, provisioning-row updates, or deprovisioning admission. +--- + +# Verify hosted Personal Server provisioning + +Read the [transition map, bounds and known finding](../../../verification/hosted-provisioning/README.md). +The [checker](../../../verification/hosted-provisioning/check.py) pins the reviewed +route source and requires the model and offline API replay to agree. + +An accepted provider resource needs a durable row with the handles required +for cleanup. A delete during provisioning can race the provider result +before either handle exists. + +Use Python 3.12 or newer, installed Node and CLI and Connect dependencies, +and pinned TLC 1.7.4 with Java. Set `TLA2TOOLS` and `JAVA` to installed +paths. Run from the CLI root. + +```sh +python3 verification/hosted-provisioning/check.py +``` + +Read the current counterexample and the scratch-guard outcome with Pstack +`/statechart`. Require the signed route replay to reproduce the current +finding and the scratch guard to block it. Restore the source and rerun. +Reconcile the provider boundary, database state, and observed HTTP outcomes +before moving the source pins. diff --git a/.agents/skills/verify-mainnet-registration/SKILL.md b/.agents/skills/verify-mainnet-registration/SKILL.md new file mode 100644 index 0000000..7959586 --- /dev/null +++ b/.agents/skills/verify-mainnet-registration/SKILL.md @@ -0,0 +1,27 @@ +--- +name: verify-mainnet-registration +description: Verify mainnet app registration and Account association recovery. Use for the registration journal, gateway confirmation, retry, or ownership check. +--- + +# Verify mainnet app registration + +Read the [transition map, bounds and replay](../../../verification/mainnet-registration/README.md). +The [checker](../../../verification/mainnet-registration/check.py) pins the reviewed +source from CLI main `a55d0a0006da6a743b6452796435afa6ed177dd8`. + +Persist the original registration context before the first gateway request. +Require a matching confirmed app before associating it with Account, and +confirm Account ownership before clearing the recovery journal. + +Use Python 3.12 or newer, installed Node and Vitest, and pinned TLC 1.7.4 with +Java. Set `TLA2TOOLS` and `JAVA` if mise cannot locate them. Run from the CLI root. + +```sh +python3 verification/mainnet-registration/check.py +``` + +Require the current model and real-command replays to pass. The checker must +observe every named model violation, catch its scratch source mutant, restore +the source, and pass the baseline again. Read all outcomes with Pstack +`/statechart`. Update the pinned source only after rechecking the model's +journal, remote confirmation, and Account ownership boundaries. diff --git a/.agents/skills/verify-paid-read-recovery/SKILL.md b/.agents/skills/verify-paid-read-recovery/SKILL.md new file mode 100644 index 0000000..3a0a720 --- /dev/null +++ b/.agents/skills/verify-paid-read-recovery/SKILL.md @@ -0,0 +1,105 @@ +--- +name: verify-paid-read-recovery +description: Verify interrupted and overlapping CLI paid reads, receipt-file writers and dead-owner recovery. Use when changing src/cli/app/read.ts, src/core/receipts.ts or src/core/receipts-lock.ts. Runs TLA+ models and offline real-code replays without live paid reads. +--- + +# Verify paid-read recovery + +The promise: an interrupted or overlapping read retains the exact payment +identity needed to resume, without authorizing another payment for the same read +intent. A concurrent state update must not erase a saved receipt. + +## Source record + +Last confirmed source commit: `a55d0a0006da6a743b6452796435afa6ed177dd8`. The runner records the exact source blobs and rejects drift. + +| Owner | Coverage | +| --------------------------------------------------------------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `src/cli/app/read.ts`, `runAppRead` and `runPersonalServerRead` | Acquire the intent lock before loading saved state; retain it through signing, persistence, transport and error handling. Replay exact headers and refuse rejected-receipt replacement. Contention uses existing `not_ready` / exit 6. | +| `src/core/receipts.ts`, `withReadLock`, `nextNonce`, `saveReceipt`, `dropReceipt` | Intent exclusion and writer exclusion around the complete file read/modify/write. Preserve temporary-file fsync, rename and directory fsync. | +| `src/core/receipts-lock.ts`, `acquireReceiptLock` | Atomic publication of an identified owner; retain live/unknown owners, reclaim demonstrably dead ones, and preserve successor locks. | +| SDK 4.3.1 direct read/payment helpers | Real fixture signing and request construction. One signed header is reused across transport retries. | + +## Run + +From the repo root with installed dependencies, Python 3.12+, compatible Node, +TLC 1.7.4 and Java installed through mise: + +```sh +python3 verification/paid-read-recovery/check.py +``` + +The runner exports the recorded fixed commit and overlays only the named +working-tree source owners and regression tests. Expected blob identities prevent +silent source/model drift. `--ref` checks a committed revision instead; it still +must match the checked source blobs. No branch switch or product mutation occurs +in the working checkout. `TLA2TOOLS` and `JAVA` may select existing local tools; +the TLC jar hash is pinned and no dependencies are downloaded. + +The command runs four fixed models, four negative models, the real-code tests, +four deliberate source mutations in a disposable copy, then restores all source +bytes and reruns the baseline. It prints the evidence directory. Exit 0 means all +expected positive and negative results hold; exit 2 means an execution or proof +failure. Unexpected external fetches are rejected. Java may need permission for +its local management socket. + +## Read every model with /statechart + +Use pstack **`/statechart`**, with the Codex adapter when applicable. Follow the +installed skill's current runtime instructions and use a scratch folder outside +the repository. The copied model is `PaidRead.tla`, with `overview.mjs` as the +view and these configurations: + +- `single.cfg`: one reader, one crash/restart. +- `concurrent.cfg`: two readers, no crash. +- `writers.cfg`: one reader plus an independent nonce writer sharing the file. +- `concurrent-crash.cfg`: two readers, one crash/restart. +- `no-save.cfg`, `no-refusal.cfg`, `no-read-lock.cfg`, `no-write-lock.cfg`: + deliberately removed protections. Each must break its original invariant. + +`DurableBeforeSend`, `NoDuplicateCharge`, `RejectedNeverReauthorizes` and +`NoDeadlock` must hold in every fixed configuration. The supplied report records +state counts, counterexamples and exact guard mutations. A passing reproduction +test never substitutes for a passing invariant check. + +## Real-code owner proof + +`test/cli/app-read-loop.test.ts` owns saved-header recovery, rejected receipts, +store corruption/persistence failure, competing writes and overlapping reads. +`test/core/receipts-lock.test.ts` covers unknown owners and the stale-reclaimer +race. Avoid copying these contracts into another fixture test. + +The process fixture independently exercises abrupt exits after nonce persistence, +before receipt rename, after persistence, after send and after simulated +settlement. It also blocks a second process behind a live reader, kills that +reader and checks exact-payment recovery. Real SDK signing runs on a public test +key and synthetic data. Transport and settlement are local fixtures. + +Removing pre-send save or rejection refusal must fail the existing owner tests. +Removing the read lock must fail the overlap test; removing the writer lock must +fail the competing-write test. Restore every mutation and confirm the baseline +passes again. Do not weaken the invariant to make a control pass. + +## Bounds and maintenance + +The fixed models cover one payer, network, grant, scope and a fixed supported +legacy grant-fee challenge. Successful signing and rename durability after process +exit are assumed. Lock acquisition abstracts the successful atomic directory +rename; process death makes its lock reclaimable. Unknown owners, PID reuse and +inaccessible owner processes fail closed in the implementation. The actual lock +recovery and successor race also have real-code proof. + +Real gateway/chain deduplication, live escrow, access records, server-supplied +nonces, expiry, power loss, remote filesystems and arbitrary numbers of readers +are outside this proof. There is no liveness proof. The 1,654-state passing crash +case exceeds the chart budget, so `/statechart` emits only its passing report. + +When an owner changes, read its entire relevant path and update the model from +the code before changing expected blobs. Keep file reads, renames and releases +separate where the code separates them. Use `/maintain-formal-verification-skill` +for skipped verification updates. Follow the updated skill once as the next agent +would, including all negative controls. Keep product and verification changes +reviewable separately; no commit or publication is implied. + +See `verification/paid-read-recovery/README.md` for the result. +Do not retrieve credentials or run live paid reads as part of this procedure. diff --git a/.agents/skills/verify-server-supervision/SKILL.md b/.agents/skills/verify-server-supervision/SKILL.md new file mode 100644 index 0000000..171857f --- /dev/null +++ b/.agents/skills/verify-server-supervision/SKILL.md @@ -0,0 +1,30 @@ +--- +name: verify-server-supervision +description: Verify the local Personal Server stop and restart boundary. Use when changing the supervisor's backoff, port probing, replacement launch or Stop handling. +--- + +# Verify local Personal Server supervision + +Read the [transition map, bounds and known finding](../../../verification/server-supervision/README.md). +The production source and owner replay were reconciled at +`a55d0a0006da6a743b6452796435afa6ed177dd8`. The [checker](../../../verification/server-supervision/check.py) +pins their exact Git blobs and requires the named TLC verdicts and CLI events. + +Use Python 3.12 or newer, the installed Node and Vitest, and pinned TLC 1.7.4 +with Java. Set `TLA2TOOLS` and `JAVA` to installed paths if mise cannot locate +them. Run from the CLI root. + +```sh +python3 verification/server-supervision/check.py --out "$(mktemp -d)/proof" +``` + +The current port-probe model and route replay show a late restart. The known +finding must reproduce. The backoff property must hold. The scratch control +removing its fence must fail on a restart event. The scratch port fence must +prevent that event, and the restored source must reproduce both original +results. The replay uses controlled handles and starts no Personal Server. + +Read every outcome with Pstack `/statechart`. After a code change, reconcile +the source, the model's await boundaries and the exact replay before moving +the pinned revision. If the port-probe finding is repaired, change its +expected verdict only after showing the old path fail and the new path pass. diff --git a/.agents/skills/verify-setup-resume/SKILL.md b/.agents/skills/verify-setup-resume/SKILL.md new file mode 100644 index 0000000..3fd2f95 --- /dev/null +++ b/.agents/skills/verify-setup-resume/SKILL.md @@ -0,0 +1,105 @@ +--- +name: verify-setup-resume +description: Verify BUI-936 setup/resume identities, funding readiness and overlapping resumes. Use when changing app request, test-credit transport or the request journal. Runs bounded TLA+ checks and offline real-code replays without live funding or paid reads. +--- + +# Verify setup/resume + +An interrupted or overlapping setup must recover its saved funding and consent +identities, and must not create consent before credit is usable. Losing an +identity can allocate another operation or leave the original consent stranded. + +## Source record + +Last confirmed source commit: `a55d0a0006da6a743b6452796435afa6ed177dd8`. The runner records the exact source blobs and rejects drift. + +| Owner | Model and real-code coverage | +| ------------------------------------------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `src/cli/app/request.ts`, `runAppRequest`, `runConsentIntent` | Save frozen setup before transport; reject changed resume context; recover consent using the exact saved payload/key; known requests use status lookup. | +| `src/cli/app/test-credit.ts`, `prepareTestCredit` | Reuse funding key until operation ID is known; gate consent on usable credit; adopt authoritative journal progress after overlapping responses. | +| `src/core/test-credit.ts`, `requestTestCredit` | Unknown funding identity uses POST with the saved key; known identity uses GET. Validate returned identity; pending deposits are not spendable credit. | +| `src/core/requests-store.ts`, `saveIntent`, `updateFunding`, `save` | Serialize the complete read/modify/write, reject conflicting identities and duplicate unfinished setups, keep terminal funding progress, atomically publish journal updates. | +| `src/cli/app/requests.ts`, `checkGrant` | Existing owner tests additionally check resumed approval against the current grant; this stage is outside the TLA+ model. | + +## Run + +From the repository root with installed dependencies, Python 3.12+, Node, TLC +1.7.4 and Java installed through mise: + +```sh +python3 verification/setup-resume/check.py +``` + +`TLA2TOOLS` and `JAVA` can select already-installed tools. The TLC jar SHA256 is +pinned; nothing is downloaded. Java may require permission for its local +management socket. `--out` selects a new evidence directory. `--ref` checks a +committed revision with matching source blobs. + +The runner exports the pinned commit into a disposable directory, overlays only +the checked working-tree source owners and owner tests, then runs seven positive +models, seven deliberately broken models, real-code replays, seven source +mutations, byte-exact restoration, and the baseline again. It does not change +product files or the Git index. Unexpected global fetches are rejected; the +owner tests inject synthetic Account/gateway transport and use a public test key. +Exit 0 means all expected results hold; exit 2 means execution or proof failed. + +## Read every result with /statechart + +Use the installed pstack **`/statechart`** skill and the Codex adapter when +applicable. Follow its current runtime instructions in a scratch directory +outside the repository. Copy `verification/setup-resume/models/` there. + +- `overview.cfg`: one command, one resume, no process crash; readable chart. +- `single.cfg`: one command, two resumes, one process crash. +- `concurrent.cfg`: two commands, one resume each, no process crash. +- `concurrent-crash.cfg`: two commands, one resume each, one process crash. +- `claim.cfg`, `existing-credit.cfg`, `changed-context.cfg`: claim handoff, + existing usable/pending credit, and changed context, with two resumes and one + crash each. +- The other seven configurations deliberately remove one protection each. + +Use `overview.mjs` for passing configurations and `details.mjs` for negative +controls. The detailed view keeps both concurrent commands and the individual +journal phases visible. Never suppress a counterexample or merge away the stale +write. Passing graphs above the tool's 500-state budget have reports without +charts. Keep their full bounds; the smaller overview does not replace them. + +## Oracles and sensitivity + +Keep the existing owner tests in `test/cli/app-test-credit.test.ts` and +`test/cli/app-request-recovery.test.ts`; avoid copying their contracts into a +second suite. The verification-local fixture adds actual write-failure and +overlapping-resume schedules: unknown/known operation, confirmed/failed result, +then a stale pending response. It checks the durable result, transmitted keys, +GET/POST counts, consent count and subsequent recovery. + +Each modeled removed protection must also cause a behavioral assertion failure +when removed from real source in the disposable snapshot. The runner checks the +specific invariant for each model, checks test failure rather than a tool error, +restores every source byte, and reruns all 61 tests. A passing replay does not +replace a passing model check. Replay any new model finding against the real +code before reporting it as a defect; first suspect a modeling error when it +does not reproduce. Do not edit product code without authorization. + +## Bounds and maintenance + +The model covers one app/network/environment/payload and one admitted setup. +Writer lock acquisition, reads, publication and release are separate actions; +atomic journal rename is the publication step. Process death releases the +writer through eventual dead-owner recovery. Individual fsync syscalls, PID +reuse, lock reaper races and power loss are not modeled; existing owner tests +cover interrupted writers and successor-lock preservation. + +Account funding and gateway consent deduplicate the same key/body and retain +that mapping for recovery. Returned funding readiness and operation identity are +assumed truthful. These are external service assumptions, not locally proved +facts. Arbitrary client counts, multiple independent contexts, provider rollout, +chain settlement, real escrow, live authentication, paid reads and liveness are +outside this proof. Pending, failed, claim-required, denied and expired outcomes +can remain stopped; the checker does not promise eventual human/service action. + +See `verification/setup-resume/README.md` for source mapping, evidence and +counterexample paths. When source changes, inspect the changed path before +updating the model and blob identities. Use `/maintain-formal-verification-skill` +if verification has drifted, then follow this skill once with negative controls +and restoration. No commit, funding, collection or publication is implied. diff --git a/docs/STATE-MACHINE-INVENTORY.md b/docs/STATE-MACHINE-INVENTORY.md new file mode 100644 index 0000000..4e15acd --- /dev/null +++ b/docs/STATE-MACHINE-INVENTORY.md @@ -0,0 +1,71 @@ +# Vana CLI state machine inventory + +This inventory follows GitHub main at `a55d0a0006da6a743b6452796435afa6ed177dd8`. +PRs in the tables identify implementation history and pending changes. +See [the eight statecharts](STATECHARTS.md). + +A machine belongs to the code that can advance it. A command can report +separate facts about sign-in, provider collection, saved exports, server +acceptance, consent, or payment. Local success at one step cannot stand in +for success at the next. Account, Personal Server, Gateway, the connector +provider, and Factory internals are external authorities to the CLI. + +## Formal checks + +| Subsystem | Reusable skill | Result and scope | +| -------------------------------------- | ------------------------------------------------------------------------------ | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Builder setup and request recovery | [Setup and resume](../.agents/skills/verify-setup-resume/SKILL.md) | Existing verifier rerun against the pinned main snapshot. Recover the same funding and consent identities, wait for usable credit, reject changed resume context and retain terminal funding. The runtime landed in [#106](https://github.com/vana-com/vana-cli/pull/106) and [#109](https://github.com/vana-com/vana-cli/pull/109). | +| Paid data reads | [Paid-read recovery](../.agents/skills/verify-paid-read-recovery/SKILL.md) | Existing local verifier rerun at its matching source blobs. Serialize receipt writes and each read intent, persist payment before sending, replay its exact header and refuse to pay again after rejection. Runtime repair merged in [#119](https://github.com/vana-com/vana-cli/pull/119). | +| Local Personal Server supervision | [Server supervision](../.agents/skills/verify-server-supervision/SKILL.md) | Stop during restart backoff holds. Stop during the subsequent port probe can start a replacement before the next Stop check. The same supervisor source is on main. [#83](https://github.com/vana-com/vana-cli/pull/83) and [#85](https://github.com/vana-com/vana-cli/pull/85) own related restart and tunnel behavior. | +| Queued export ownership and settlement | [Export settlement](../.agents/skills/verify-export-settlement/SKILL.md) | Two positive bounds and matching CLI replays pass on the session and main. A stale upload settlement cannot overwrite the newer receipt, and a foreign collection must preserve pending bytes. [#93](https://github.com/vana-com/vana-cli/pull/93), [#94](https://github.com/vana-com/vana-cli/pull/94), [#108](https://github.com/vana-com/vana-cli/pull/108), [#124](https://github.com/vana-com/vana-cli/pull/124). | +| Mainnet app registration | [Mainnet registration](../.agents/skills/verify-mainnet-registration/SKILL.md) | A matching confirmed Gateway read precedes Account association. Keep recovery context through lost responses and until ownership is observed. The replay uses the pinned main snapshot. [#115](https://github.com/vana-com/vana-cli/pull/115) separately proposes terminal classification for Account refusals. | +| Hosted server provisioning | [Hosted provisioning](../.agents/skills/verify-hosted-provisioning/SKILL.md) | The signed API can accept deletion while provisioning, then acknowledge the original create with no tracking row. Two controlled schedules reproduced against the session and main source. The normal page hides Remove Server in that phase. | +| Collection admission | [Collection admission](../.agents/skills/verify-collection-admission/SKILL.md) | Refuse a foreign destination in automation before probing credentials, and recheck the collecting account after approval. | + +These seven owners have executable bounded models. Other rows record inspected +lifecycles and focused tests where available. The proofs use controlled +transports. They establish no live provider, deployed Account, payment +settlement, real signal delivery, or bundled runtime behavior. + +## Owner side + +| Subsystem | States, guards and source owner | PR evidence | +| ------------------------------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Account login, Personal Server session and owner change | [Auth](../src/cli/auth.ts), [identity](../src/cli/identity.ts), and [relay](../src/server/session-relay.ts). Device login issues and polls an approval, then validates and saves the Account identity. A Personal Server session has its own expiry and can remain valid when Account expires. A change of identity changes the allowed destination. | [#3](https://github.com/vana-com/vana-cli/pull/3), [#38](https://github.com/vana-com/vana-cli/pull/38), [#76](https://github.com/vana-com/vana-cli/pull/76), [#77](https://github.com/vana-com/vana-cli/pull/77), [#93](https://github.com/vana-com/vana-cli/pull/93). | +| Welcome, destination admission and recovery | [Collection readiness](../src/cli/collection-readiness.ts) and [command entry](../src/cli/index.ts). Discover a source before asking for credentials. Establish the collecting owner and eligible destination before starting collection. Human retry carries source, network, checkout and destination. Machine modes must stop at actionable outcomes. | [#39](https://github.com/vana-com/vana-cli/pull/39), [#106](https://github.com/vana-com/vana-cli/pull/106), [#112](https://github.com/vana-com/vana-cli/pull/112), [#116](https://github.com/vana-com/vana-cli/pull/116). | +| Connector discovery, install and profile | [PDPP installer](../src/pdpp/installer.ts), [profiles](../src/pdpp/profile.ts), [local connector registry](../src/pdpp/local-connectors.ts), and [managed browser](../src/runtime/managed-playwright.ts). Resolve pin or local checkout, validate, install and reuse a profile, or refuse a live lock or unsupported browser. | [#40](https://github.com/vana-com/vana-cli/pull/40), [#45](https://github.com/vana-com/vana-cli/pull/45), [#69](https://github.com/vana-com/vana-cli/pull/69), [#123](https://github.com/vana-com/vana-cli/pull/123). | +| Collection attempt and cancellation | [PDPP runtime](../src/pdpp/runtime.ts), [protocol](../src/pdpp/protocol.ts) and [host](../src/pdpp/host.ts). Spawn, authorize, receive stream data and checkpoint, settle successful streams, classify empty or incomplete results, abort and reap before releasing the run lock. Legacy Playwright owns a separate browser lifetime. | [#45](https://github.com/vana-com/vana-cli/pull/45), [#70](https://github.com/vana-com/vana-cli/pull/70), [#75](https://github.com/vana-com/vana-cli/pull/75), [#108](https://github.com/vana-com/vana-cli/pull/108). [#74](https://github.com/vana-com/vana-cli/pull/74) is open for interleaved stream-total publication. | +| Factory workflow | [Build commands](../src/cli/connector-build.ts), [Factory transport](../src/core/factory-transport.ts), and [verification gate](../src/pdpp/factory-gate.ts). Prepare a job and attempt, verify the actual run before committing result/checkpoint, retry or resume with bound evidence. CLI keeps authority over collection and writes. | [#108](https://github.com/vana-com/vana-cli/pull/108), [#113](https://github.com/vana-com/vana-cli/pull/113), [#124](https://github.com/vana-com/vana-cli/pull/124), [#129](https://github.com/vana-com/vana-cli/pull/129). | +| Saved export, delivery and sync | [State store](../src/core/state-store.ts), [export receipts](../src/core/source-export.ts) and [ingest](../src/personal-server/index.ts). Publish accepted generation, queue scopes, ingest for its owner, retain failed scopes, and settle only the same generation. | Bounded export check above. [#30](https://github.com/vana-com/vana-cli/pull/30), [#94](https://github.com/vana-com/vana-cli/pull/94). | +| Detached collection and schedule | [CLI entry](../src/cli/index.ts) and [schedule](../src/cli/schedule.ts). Install or remove an explicitly authorized task. Pin the job's state and logs. Scheduled and detached runs must preserve owner and context, report failures and avoid foreground prompts. | [#35](https://github.com/vana-com/vana-cli/pull/35), [#81](https://github.com/vana-com/vana-cli/pull/81), [#116](https://github.com/vana-com/vana-cli/pull/116). | +| Local server setup, registration and tunnel | [Start and supervisor](../src/cli/server-start.ts), [runtime](../src/personal-server/local/runtime.ts), [detach](../src/personal-server/local/detach.ts), [data directory](../src/personal-server/local/data-dir.ts) and [tunnel process](../src/personal-server/local/tunnel-process.ts). Select the owner directory, reuse or lock it, prepare runtime and credentials, wait for ready, register the public endpoint, and supervise or stop. | [#47](https://github.com/vana-com/vana-cli/pull/47), [#48](https://github.com/vana-com/vana-cli/pull/48), [#60](https://github.com/vana-com/vana-cli/pull/60), [#63](https://github.com/vana-com/vana-cli/pull/63), [#78](https://github.com/vana-com/vana-cli/pull/78), [#83](https://github.com/vana-com/vana-cli/pull/83), [#85](https://github.com/vana-com/vana-cli/pull/85). Only stop/restart is modeled here. | +| Owner MCP approval and tools | [MCP server](../src/cli/mcp-server.ts) and [requests](../src/cli/mcp-requests.ts). Discover a scope request, pick approval route, check approval, and expose or page data through the eligible server. Collection tools share the same readiness and ingest owners. | [#65](https://github.com/vana-com/vana-cli/pull/65), [#79](https://github.com/vana-com/vana-cli/pull/79), [#86](https://github.com/vana-com/vana-cli/pull/86), [#90](https://github.com/vana-com/vana-cli/pull/90). | +| Private Desktop handoff | The [#121 draft](https://github.com/vana-com/vana-cli/pull/121) packages a frozen immutable descriptor and bytes. Status and resume bind to owner, Account authority, network, environment and digest. Desktop owns activation and settlement. | Draft candidate. The CLI session snapshot does not contain the proposed command. | + +## Builder side + +| Subsystem | States, guards and source owner | PR evidence | +| ----------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Moksha registration and builder key | [Register](../src/cli/app/register.ts), [app key](../src/core/app-key.ts) and [profile](../src/core/app-profile.ts). Reuse or generate the key, check remote registration, register if absent, and preserve keys for URL-less registration recovery. | [#10](https://github.com/vana-com/vana-cli/pull/10) introduced registration. [#125](https://github.com/vana-com/vana-cli/pull/125) and [#128](https://github.com/vana-com/vana-cli/pull/128) went to dev. [#126](https://github.com/vana-com/vana-cli/pull/126) closed unmerged. [#130](https://github.com/vana-com/vana-cli/pull/130) landed the safe existing-key path on main. | +| Account app claim | [Claim command](../src/cli/app/claim.ts) and [claim store](../src/core/app-claim-store.ts). Verify builder and Account subject, retain a signed handoff while valid, regenerate after expiry, and complete only after matching ownership is confirmed. | [#67](https://github.com/vana-com/vana-cli/pull/67), [#109](https://github.com/vana-com/vana-cli/pull/109). Setup recovery treats claim as an outcome. It does not model concurrent claim-link creation. | +| Mainnet promotion | [Mainnet registration](../src/cli/app/mainnet-registration.ts) and [registration journal](../src/core/app-registration-store.ts). Establish original ownership, persist context, observe or submit registration, wait for matching confirmed proof, associate Account, then verify ownership before clearing the journal. | Bounded check above. [#107](https://github.com/vana-com/vana-cli/pull/107) closed unmerged. Its implementation is present through the older dev integration. [#115](https://github.com/vana-com/vana-cli/pull/115) remains open for permanent Account refusals. | +| Funding and request setup | [Request](../src/cli/app/request.ts), [test credit](../src/cli/app/test-credit.ts), and [journal](../src/core/requests-store.ts). Save intent before either POST, recover the funding operation, use GET after learning its ID, and start consent after credit becomes usable. | Existing setup/resume proof. [#106](https://github.com/vana-com/vana-cli/pull/106). | +| Consent, scope union and delivery | [Request status](../src/cli/app/requests.ts) and [grant union](../src/core/grant-union.ts). Select owner, reconcile prior scopes, retain request ID, await approval or denial/expiry, and verify a live matching grant. An example acknowledges delivery after saving it. | [#16](https://github.com/vana-com/vana-cli/pull/16), [#87](https://github.com/vana-com/vana-cli/pull/87), [#89](https://github.com/vana-com/vana-cli/pull/89). [#127](https://github.com/vana-com/vana-cli/pull/127) adds configured-server approval links on dev. [#104](https://github.com/vana-com/vana-cli/pull/104) covers an example's delivery acknowledgement. | +| Read authority and paid recovery | [Read](../src/cli/app/read.ts), [receipts](../src/core/receipts.ts), and [locks](../src/core/receipts-lock.ts). Resolve grant and route, probe fee, save or replay the exact payment identity, and hold the read lock through settlement. A rejected saved receipt ends this read. | Existing paid-read proof. [#13](https://github.com/vana-com/vana-cli/pull/13), [#23](https://github.com/vana-com/vana-cli/pull/23), [#119](https://github.com/vana-com/vana-cli/pull/119). The enclave fee route is outside the formal proof. | +| Manual escrow | [Escrow](../src/cli/app/escrow.ts) and [authorization](../src/core/escrow-authorization.ts). Resolve asset and balance, sign relayed or direct funding, and distinguish final, pending, rejected or uncertain delivery. | [#71](https://github.com/vana-com/vana-cli/pull/71). Automatic test credit is a separate workflow. | +| Derived answer and readback | [Ask](../src/cli/app/ask.ts) and [derivative status](../src/cli/app/derivatives.ts). Request the derived scope only, observe server readiness or failure, resolve lineage and read the ready derivative through the standard read command. | [#21](https://github.com/vana-com/vana-cli/pull/21), [#82](https://github.com/vana-com/vana-cli/pull/82). Personal Server owns computation. | +| Connector submission | [#133 draft](https://github.com/vana-com/vana-cli/pull/133). Prepare one connector diff and matching verification at a pinned base and head. Confirm by digest, push a stable branch to the authenticated fork, and look up an existing PR before attempting creation or after an ambiguous result. | Draft candidate. The fixture runs a synthetic GitHub transport. | + +## Connect web app in the same repository + +| Subsystem | States, guards and source owner | +| ----------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Browser handoff and device approval | [Handoff contract](../connect/src/app/_lib/handoff-contract.ts), [resolution](../connect/src/app/_lib/use-handoff-resolution.ts) and [device routes](../connect/src/app/api/auth/device). Resolve expiring URL, cookie and storage context. Approve a code and optionally bind a scoped Personal Server session before polling returns it. | +| Hosted Personal Server | [Create/list API](../connect/src/app/api/servers/route.ts), [get/delete API](../connect/src/app/api/servers/%5Bid%5D/route.ts), and [GCP provider](../connect/src/lib/server-provider/gcp.ts). Reserve a database row, provision VM, disk, DNS and tunnel, publish handles and credentials, register on-chain when ready, and delete after deprovisioning. | +| Unrouted host | [Worker](../worker/src/index.ts) returns a stateless 404. Cloudflare routes active hosts directly to their tunnels. | + +The two existing CLI verification bundles are tracked on the local session +branch. The behavior repairs cited above landed on main, while neither +verification bundle is in GitHub main's tree. The setup verifier's covered +`requests.ts` differs in the dirty checkout. Its rerun used the committed +snapshot explicitly. diff --git a/docs/STATECHARTS.md b/docs/STATECHARTS.md new file mode 100644 index 0000000..04fc1d3 --- /dev/null +++ b/docs/STATECHARTS.md @@ -0,0 +1,357 @@ +# Vana CLI statecharts + +[Source inventory and verifier entry points](STATE-MACHINE-INVENTORY.md) + +Each TLC report records the state count and omitted steps that stay in the same label. Use the model owner’s README for exact bounds and excluded behavior. + +To redraw a model, copy its model directory to scratch. Set the Pstack Statechart executable and select the TLA+ module, config, and view named in the proof owner. + +```sh +$STATECHART "$scratch/$module.tla" --config "$scratch/$config.cfg" --view "$scratch/$view.mjs" --out "$(mktemp -d)/chart" +``` + +## Prepare to collect a source + +Confirm an eligible Personal Server before collection. A late approval cannot authorize an obsolete owner. + +```mermaid +--- +title: "Prepare to collect into a Personal Server" +--- +stateDiagram-v2 + s0: Checking the Vana account + s1: Finding a Personal Server + s2: Collection blocked + s3: Sign in to Vana + s4: Server belongs to another account + s5: Preparing a Personal Server + s6: Checking server access + s7: Approve this CLI + s8: Server access confirmed + s9: Account changed during the access check + s10: Ready to collect + [*] --> s0 + s0 --> s1: Account identified + s0 --> s2: No usable account + s0 --> s3: Sign-in required + s1 --> s4: Found another owner's server + s1 --> s2: No usable server + s1 --> s6: Found your server + s1 --> s5: No server found + s3 --> s1: Sign-in succeeds + s3 --> s2: Sign-in fails + s4 --> s2: Permission missing + s4 --> s6: Person allows this server + s5 --> s1: Try to find the prepared server + s6 --> s2: Access unavailable + s6 --> s8: Server accepts the CLI + s6 --> s9: Account changes or Send access check + s6 --> s7: Approval required + s7 --> s2: Approval fails + s7 --> s6: Person approves + s8 --> s10: Admit collection + s9 --> s2: Access unavailable or Retry with intended account + s9 --> s7: Approval required +``` + +## Save collected data and retry upload + +A late upload can settle only the generation it started with. + +```mermaid +--- +title: "Collect data and preserve the latest accepted export" +--- +stateDiagram-v2 + s0: Collectors running without an accepted export + s1: Accepted export recorded locally + s2: Accepted export local. Upload pending + s3: Accepted export remains local after an upload failure + s4: Accepted export stored + s5: Older response discarded. Newer export retained + [*] --> s0 + s0 --> s1: Record the local export + s1 --> s2: Upload to Personal Server + s2 --> s1: Personal Server responds or Accept the newer export + s1 --> s3: Record the upload result + s1 --> s4: Record the upload result + s3 --> s1: Accept the newer export + s1 --> s5: Discard settlement for the older export + s4 --> s1: Accept the newer export + s2 --> s5: Discard settlement for the older export + s3 --> s5: Discard settlement for the older export + s4 --> s5: Discard settlement for the older export +``` + +## Switch accounts with an upload still pending + +A foreign collection must leave the pending bytes and receipt with their owner. + +```mermaid +--- +title: "Collect data and preserve the latest accepted export" +--- +stateDiagram-v2 + s0: Collectors running without an accepted export + s1: Accepted export recorded locally + s2: Accepted export local. Upload pending + s3: Other account's export stays local + s4: Accepted export remains local after an upload failure + s5: Accepted export stored + [*] --> s0 + s0 --> s1: Record the local export + s1 --> s2: Upload to Personal Server + s1 --> s3: Refuse to replace another account's export + s2 --> s1: Personal Server responds + s1 --> s4: Record the upload result + s1 --> s5: Record the upload result + s2 --> s3: Refuse to replace another account's export + s4 --> s3: Refuse to replace another account's export + s5 --> s1: Accept the newer export +``` + +## Set up a builder request and resume + +Persist recovery identity, wait for usable credit, then create consent. The chart uses the small overview configuration. + +```mermaid +--- +title: "Setup resumes with the saved funding and consent identities" +--- +stateDiagram-v2 + s0: New setup + s1: Saving setup identity + s2: Requesting funding with saved key + s3: Funding pending + s4: Saving funding result + s5: Setup saved for resume + s6: Checking resume context + s7: Funding failed + s8: Usable credit confirmed + s9: Inspecting saved funding + s10: Creating consent with saved key + s11: Consent accepted remotely + s12: Saving consent identity + s13: Checking approval + s14: Waiting for approval + s15: Approval received + s16: Denied or expired + [*] --> s0 + s0 --> s1: start setup + s1 --> s2: release journal writer lock + s2 --> s3: send the saved funding key + s3 --> s4: accept funding response + s3 --> s5: lose the response after remote acceptance + s5 --> s6: run saved resume command + s6 --> s2: validate saved identity and options + s2 --> s7: send the saved funding key + s2 --> s8: send the saved funding key + s4 --> s5: release journal writer lock + s7 --> s4: accept funding response + s7 --> s5: lose the response after remote acceptance + s8 --> s4: accept funding response + s8 --> s5: lose the response after remote acceptance + s6 --> s9: validate saved identity and options + s9 --> s3: GET the saved operation + s9 --> s7: GET the saved operation + s9 --> s8: GET the saved operation + s4 --> s10: release journal writer lock + s10 --> s11: send the saved consent payload + s11 --> s5: lose the response after remote acceptance + s11 --> s12: take journal writer lock + s12 --> s13: release journal writer lock + s13 --> s14: read approval result + s13 --> s15: read approval result + s13 --> s16: read approval result +``` + +## Recover an interrupted paid read + +Reuse the saved payment identity and keep overlapping readers from paying again. The chart shows the single-reader profile. + +```mermaid +--- +title: "Paid-read recovery: one reader and overlapping readers" +--- +stateDiagram-v2 + s0: Start or restart + s1: Read lock held#59; loading saved receipt + s2: Checking whether payment is needed + s3: Preparing payment + s4: Stopped for repair + s5: Saving recovery receipt + s6: Ready to send + s7: Payment sent + s8: Retrying saved payment + s9: Charged#59; waiting for data + s10: Data received + [*] --> s0 + s0 --> s1: you reserve this read intent + s1 --> s0: the CLI closes and you restart + s1 --> s2: you open the saved payment state + s2 --> s0: the CLI closes and you restart + s2 --> s3: the server requests payment + s3 --> s0: the CLI closes and you restart + s3 --> s4: saving payment state fails + s4 --> s0: the CLI closes and you restart + s3 --> s5: you finish preparing the payment + s5 --> s0: the CLI closes and you restart + s5 --> s4: saving payment state fails + s5 --> s6: the recovery receipt is saved + s6 --> s0: the CLI closes and you restart + s6 --> s7: you send the signed payment + s1 --> s8: you open the saved payment state + s7 --> s0: the CLI closes and you restart + s7 --> s9: the fixture settles a distinct payment + s8 --> s4: the server rejects the saved receipt + s8 --> s6: you reuse the same saved header + s9 --> s10: the data arrives + s9 --> s0: the CLI closes and you restart + s6 --> s9: you send the signed payment +``` + +## Register an app on mainnet + +A matching confirmed Gateway read must precede Account association. Ownership confirmation clears the saved recovery context. + +```mermaid +--- +title: "Promote an existing app from Moksha to mainnet" +--- +stateDiagram-v2 + s0: Ready to promote an owned app + s1: App and Account verified + s2: Recovery context ready + s3: Mainnet record absent + s4: Registration submitted + s5: Waiting for mainnet confirmation + s6: Stopped with recovery context + s7: Account association ready + s8: Waiting for Account association + s9: Verifying Account ownership + s10: App ready on mainnet + [*] --> s0 + s0 --> s1: choose app and production URL + s1 --> s2: save recovery context + s2 --> s3: no registration found + s3 --> s4: submit to the gateway + s4 --> s5: registration reply arrives + s4 --> s6: registration reply is lost + s5 --> s6: confirmation times out or proof fails or names another app + s6 --> s1: resume the original app + s5 --> s7: matching confirmed proof arrives + s7 --> s8: ask Account to associate the app + s2 --> s5: use the visible registration + s8 --> s6: Account association or ownership is unconfirmed + s8 --> s9: Account accepts the association + s9 --> s6: Account association or ownership is unconfirmed + s9 --> s10: Account confirms ownership +``` + +## Stop a local server while it restarts + +Current behavior. Stop during a pending restart port check can still start the replacement. + +```mermaid +--- +title: "Stop a local Personal Server during automatic restart" +--- +stateDiagram-v2 + state "Legend" as legend { + lg0: Breaks NoLaunchAfterStop + lg1: Path to the NoLaunchAfterStop bug + } + class lg0 breaks + class lg1 bugPath + s0: Personal Server running + s1: Waiting before retry + s2: Stop requested during restart wait + s3: Checking a port for restart + s4: Personal Server stopped + s5: Starting a replacement + s6: Stop requested while restart checks a port + s7: Personal Server restarted + s8: Replacement starts after Stop + s9: Restart reported after Stop + s10: Replacement stopped again + [*] --> s0 + s0 --> s1: Server exits unexpectedly + s1 --> s2: You stop the server + s1 --> s3: Restart wait settles + s0 --> s4: Supervisor stops the server + s2 --> s4: Restart wait settles + s3 --> s5: Port check returns + s3 --> s6: You stop the server + s5 --> s7: Replacement answers + s6 --> s8: Port check returns + s8 --> s9: Replacement answers + s7 --> s4: Supervisor stops the server + s9 --> s10: Supervisor stops the server + classDef breaks fill:#ffecee,stroke:#e72e3b,stroke-width:2.5px,color:#cd2834 + class s0 bugPath + class s1 bugPath + class s3 bugPath + class s6 bugPath + class s8 breaks + class s8 bugPath + class s9 breaks + class s10 breaks +``` + +## Delete a hosted server during provisioning + +Current behavior. The signed API can delete the row before the provider has returned the resource handles. + +```mermaid +--- +title: "Delete a hosted server while provisioning is pending" +--- +stateDiagram-v2 + state "Legend" as legend { + lg0: Breaks CreatedResourceHasTrackingRow + lg1: Path to the CreatedResourceHasTrackingRow bug + } + class lg0 breaks + class lg1 bugPath + s0: No hosted server + s1: Server provisioning + s2: Owner can see the provisioning record + s3: Deletion sees no provider handles + s4: Record removed before provider finished + s5: Provisioned server is tracked + s6: Server running + s7: Provider returned after deletion + s8: Cleaning up provider resources + s9: Provider resources removed + s10: Creation reports success but the server has no record + s11: Server removed + [*] --> s0 + s0 --> s1: start server creation + s1 --> s2: owner lists servers + s2 --> s3: owner deletes before handles exist + s1 --> s5: try to store provider handles + s3 --> s4: delete the server record + s4 --> s4: start provider provisioning + s5 --> s6: provider reports running + s2 --> s5: try to store provider handles + s4 --> s7: provider creates the server + s5 --> s8: owner requests deletion + s3 --> s7: delete the server record + s7 --> s7: try to store provider handles + s6 --> s8: owner requests deletion + s8 --> s9: provider finishes cleanup + s7 --> s10: create returns success + s9 --> s4: delete the server record + s3 --> s10: delete the server record + s4 --> s11: create returns success + s9 --> s11: delete the server record + classDef breaks fill:#ffecee,stroke:#e72e3b,stroke-width:2.5px,color:#cd2834 + class s0 bugPath + class s1 bugPath + class s2 bugPath + class s3 bugPath + class s4 bugPath + class s7 bugPath + class s10 breaks + class s10 bugPath +``` diff --git a/verification/collection-admission/README.md b/verification/collection-admission/README.md new file mode 100644 index 0000000..3b0771e --- /dev/null +++ b/verification/collection-admission/README.md @@ -0,0 +1,54 @@ +# Collection admission + +`prepareCollection` must leave a foreign server unprobed until a person +confirms it. Otherwise the CLI can use a credential for a destination the +person did not authorize. A successful access reply must also still belong to +the bound account when collection is admitted. Otherwise collection can start +under an obsolete owner. + +## Source map + +The checker pins the owner and replay at main `a55d0a0006da6a743b6452796435afa6ed177dd8`. + +| Model action | Implementation in [collection-readiness.ts](../../src/cli/collection-readiness.ts) | +| ------------------------------------ | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `ReadSession`, `SignIn` | Read the session, distinguish missing and unknown ownership, and bind the known owner. An interactive run may await one sign-in. | +| `DetectServer`, `PrepareServer` | Await destination discovery. An interactive run may prepare a missing server and detect it again. Refuse a missing destination or one that cannot identify its owner. | +| `DecideForeignConsent`, `StartProbe` | Compare server ownership against the bound account. Only an interactive confirmation allows a foreign target through to `checkAccess`. | +| `ProbeReturns`, `ApproveServer` | Observe ready, unauthorized or unavailable access. An interactive run may approve once and probe again. | +| `AccountChanges`, `VerifyOwner` | The bounded change occurs while an access check or approval is pending. After successful access, the final session read and owner comparison synchronously choose ready or refusal. | + +The model covers one invocation, one bound account, at most one change of +account or session validity during access or approval, one sign-in, one destination preparation and +one approval retry. Session validity and account identity collapse to +"still matches the bound owner" at the final check. A target's reported +owner is stable once detected. The model does not cover exceptions, identity +changes during discovery or after admission, subsequent provider calls, or whether the credentials +used by a live Personal Server actually work. + +## Rerun + +Use Python 3.12 or later, the installed CLI's Node and Vitest, and TLC 1.7.4 +with Java. Set `JAVA` and `TLA2TOOLS` to installed tool paths if mise cannot +resolve them. Run from the CLI repository root. + +```sh +python3 verification/collection-admission/check.py --out "$(mktemp -d)/proof" +``` + +The checker requires the current model to pass and the two broken variants to +fail on their specific invariants. It archives the pinned source into a temporary +directory. It reuses [the seven existing readiness replays](../../test/cli/collection-readiness.test.ts), +substitutes dependencies, blocks external fetches, and runs each source mutation +against its targeted test. It restores the source and reruns all seven replays. + +| Deliberate control | Model counterexample and code replay | +| ------------------ | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | +| `no-foreign-guard` | A run finds a foreign server, proceeds without permission and probes it. Removing the foreign refusal causes the automated replay to return ready instead of refusing before access. | +| `no-owner-recheck` | A run binds an account, starts an access check, the account changes and the check returns ready. Removing the final session guard makes the existing replay admit collection for the previous account. | + +Read the current result and both control paths with Pstack `/statechart`. +The view groups the access check and its single retry, and omits terminal +stuttering. It keeps the two forbidden outcomes distinct. Update the source +pin only after comparing the model actions, guards and restored replay to +the revised owner. diff --git a/verification/collection-admission/check.py b/verification/collection-admission/check.py new file mode 100644 index 0000000..89a9ad5 --- /dev/null +++ b/verification/collection-admission/check.py @@ -0,0 +1,169 @@ +#!/usr/bin/env python3 +"""Check collection admission and replay the two guards against CLI source.""" + +import argparse +import hashlib +import io +import json +import os +from pathlib import Path +import re +import shutil +import subprocess +import tarfile +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +REVISION = "a55d0a0006da6a743b6452796435afa6ed177dd8" +SOURCE = "src/cli/collection-readiness.ts" +TEST = "test/cli/collection-readiness.test.ts" +NO_EXTERNAL_IO = "verification/setup-resume/fixtures/no-external-io.ts" +BLOBS = { + SOURCE: "c4ad048c7c42fff2f10122ff41156c7a59367a6e", + TEST: "d8f868bb147dacbe420873e945fbf2bf50d03050", + "src/core/source-export.ts": "af46b8ad4f4a64d92f6962ec9e8626d952319ef8", + "src/personal-server/index.ts": "7bc722ef96d3e97b626c192a404bb8f1d27ba8ce", + "test/setup/isolate-home.ts": "0341171c4dcd2df5e42f226a42bc7a9551d7ae73", + NO_EXTERNAL_IO: "ad91a47d1321bbf34acdba2b7a726291ac3a9cc7", +} +TLC_HASH = "936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88" +CONTROLS = { + "no-foreign-guard": ( + "ForeignProbeNeedsConsent", + "if (!allowForeignServer) {", + "if (false) {", + "refuses another account's server without testing its credentials", + ), + "no-owner-recheck": ( + "CurrentOwnerAtAdmission", + "if (!current.authenticated || !sameExportOwner(owner, current.owner)) {", + "if (false) {", + "does not bind collection to an account switched during approval", + ), +} + + +def capture(args, cwd=ROOT): + return subprocess.check_output(args, cwd=cwd, text=True).strip() + + +def run(args, cwd, log, env=None): + result = subprocess.run( + args, cwd=cwd, env=env, text=True, stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, timeout=90, + ) + log.write_text(result.stdout) + return result.returncode, result.stdout + + +def check_models(out, java, jar): + modeldir = out / "models" + shutil.copytree(HERE / "models", modeldir) + results = {} + for case in ("current", *CONTROLS): + log = out / f"{case}-tlc.log" + code, output = run([ + java, "-Xmx512m", "-XX:+UseParallelGC", "-cp", jar, "tlc2.TLC", + "-workers", "1", "-fp", "0", "-metadir", str(out / f"{case}-states"), + "-config", f"{case}.cfg", "CollectionAdmission.tla", + ], modeldir, log) + count = re.search(r"(\d+) distinct states found", output) + violation = re.search(r"Invariant (\w+) is violated", output) + expected = CONTROLS[case][0] if case in CONTROLS else None + observed = violation[1] if violation else None + if ( + code != (12 if expected else 0) or observed != expected or not count + or (expected is None and "No error has been found" not in output) + ): + raise RuntimeError(f"Unexpected TLC verdict. See {log}") + results[case] = {"states": int(count[1]), "violation": observed} + return results + + +def replay(out, vitest): + with tempfile.TemporaryDirectory(prefix="vana-collection-admission-") as tmp: + snapshot = Path(tmp) + archive = subprocess.check_output( + ["git", "archive", REVISION, "--", "src", "package.json", + TEST, "test/setup/isolate-home.ts"], + cwd=ROOT, + ) + with tarfile.open(fileobj=io.BytesIO(archive)) as handle: + handle.extractall(snapshot, members=[ + member for member in handle.getmembers() if member.isfile() or member.isdir() + ], filter="data") + (snapshot / NO_EXTERNAL_IO).parent.mkdir(parents=True) + shutil.copy2(ROOT / NO_EXTERNAL_IO, snapshot / NO_EXTERNAL_IO) + (snapshot / "node_modules").symlink_to(ROOT / "node_modules", target_is_directory=True) + (snapshot / "vitest.formal.config.mts").write_text( + "export default {test:{" + f"include:[{json.dumps(TEST)}]," + f"setupFiles:['test/setup/isolate-home.ts',{json.dumps(NO_EXTERNAL_IO)}]" + "}};\n" + ) + command = ["node", str(vitest), "run", "--config", "vitest.formal.config.mts", "--reporter=verbose"] + env = {**os.environ, "CI": "true", "TMPDIR": tmp, "NO_COLOR": "1"} + source = snapshot / SOURCE + original = source.read_bytes() + + def passing(label): + log = out / f"{label}-replay.log" + code, output = run(command, snapshot, log, env) + count = re.search(r"^ *Tests +([0-9]+) passed \(\1\) *$", output, re.MULTILINE) + if code or not count: + raise RuntimeError(f"Expected passing replays. See {log}") + return int(count[1]) + + baseline = passing("baseline") + for name, (_, anchor, mutation, selected) in CONTROLS.items(): + if original.count(anchor.encode()) != 1: + raise RuntimeError(f"Scratch mutation anchor drift: {name}") + log = out / f"{name}-replay.log" + try: + source.write_bytes(original.replace(anchor.encode(), mutation.encode())) + code, output = run([*command, "-t", selected], snapshot, log, env) + finally: + source.write_bytes(original) + if code != 1 or f"> {selected}" not in output or "AssertionError: expected" not in output: + raise RuntimeError(f"Expected selected assertion failure. See {log}") + restored = passing("restored") + if baseline != restored or source.read_bytes() != original: + raise RuntimeError("Scratch replay was not restored") + return {"baseline": baseline, "caught_controls": list(CONTROLS), "restored": restored} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--out", required=True, type=Path) + args = parser.parse_args() + for owner, expected in BLOBS.items(): + if ( + capture(["git", "hash-object", str(ROOT / owner)]) != expected + or (owner != NO_EXTERNAL_IO and capture(["git", "rev-parse", f"{REVISION}:{owner}"]) != expected) + ): + raise RuntimeError(f"Source drift in {owner}. Reconcile the model before advancing its pin.") + java = os.environ.get("JAVA") or capture(["mise", "which", "java", "--tool", "java@temurin-25"]) + jar = Path(os.environ.get("TLA2TOOLS") or ( + Path(capture(["mise", "where", "github:tlaplus/tlaplus@1.7.4"])) / "tla2tools.jar" + )).resolve() + if hashlib.sha256(jar.read_bytes()).hexdigest() != TLC_HASH: + raise RuntimeError("Use the pinned TLC 1.7.4 jar") + vitest = ROOT / "node_modules/vitest/vitest.mjs" + if not vitest.is_file() or not shutil.which("node"): + raise RuntimeError("Use Node and the repository's installed Vitest") + out = args.out.resolve() + out.mkdir() + summary = { + "source_revision": REVISION, + "source_blobs": BLOBS, + "tool": "TLC 1.7.4", + "models": check_models(out, java, str(jar)), + "replays": replay(out, vitest), + } + (out / "summary.json").write_text(json.dumps(summary, indent=2) + "\n") + print(f"Checked collection admission. Evidence in {out}") + + +if __name__ == "__main__": + main() diff --git a/verification/collection-admission/models/CollectionAdmission.tla b/verification/collection-admission/models/CollectionAdmission.tla new file mode 100644 index 0000000..cbc8278 --- /dev/null +++ b/verification/collection-admission/models/CollectionAdmission.tla @@ -0,0 +1,96 @@ +---- MODULE CollectionAdmission ---- +CONSTANTS RequireForeignConsent, RecheckAccount +VARIABLES phase, interactive, initialSession, target, consent, probed, ownerChanged +vars == <> + +Init == + /\ phase = "session" + /\ interactive \in BOOLEAN + /\ initialSession \in {"signed-in", "signed-out", "unknown-owner"} + /\ target = "none" + /\ consent = FALSE + /\ probed = FALSE + /\ ownerChanged = FALSE + +ReadSession == + /\ phase = "session" + /\ phase' = CASE initialSession = "signed-in" -> "detect" + [] initialSession = "signed-out" /\ interactive -> "sign-in" + [] OTHER -> "refused" + /\ UNCHANGED <> + +SignIn == + /\ phase = "sign-in" + /\ phase' \in {"detect", "refused"} + /\ UNCHANGED <> + +DetectServer(result) == + /\ phase \in {"detect", "redetect"} + /\ target' = result + /\ phase' = CASE result = "none" /\ phase = "detect" /\ interactive -> "prepare" + [] result \in {"none", "unknown-owner"} -> "refused" + [] result = "foreign" -> "foreign" + [] OTHER -> "probe" + /\ UNCHANGED <> + +PrepareServer == + /\ phase = "prepare" + /\ phase' = "redetect" + /\ UNCHANGED <> + +DecideForeignConsent == + /\ phase = "foreign" + /\ consent' \in (IF interactive THEN BOOLEAN ELSE {FALSE}) + /\ phase' = IF consent' \/ ~RequireForeignConsent THEN "probe" ELSE "refused" + /\ UNCHANGED <> + +StartProbe == + /\ phase \in {"probe", "reprobe"} + /\ phase' = IF phase = "probe" THEN "checking" ELSE "rechecking" + /\ probed' = TRUE + /\ UNCHANGED <> + +ProbeReturns(result) == + /\ phase \in {"checking", "rechecking"} + /\ phase' = CASE result = "ready" -> "verify" + [] phase = "checking" /\ result = "auth" /\ interactive -> "approve" + [] OTHER -> "refused" + /\ UNCHANGED <> + +ApproveServer == + /\ phase = "approve" + /\ phase' \in {"reprobe", "refused"} + /\ UNCHANGED <> + +AccountChanges == + /\ phase \in {"checking", "approve", "rechecking"} + /\ ~ownerChanged + /\ ownerChanged' = TRUE + /\ UNCHANGED <> + +VerifyOwner == + /\ phase = "verify" + /\ phase' = IF ownerChanged /\ RecheckAccount THEN "refused" ELSE "ready" + /\ UNCHANGED <> + +Done == + /\ phase \in {"ready", "refused"} + /\ UNCHANGED vars + +Next == + \/ ReadSession + \/ SignIn + \/ \E result \in {"none", "unknown-owner", "own", "foreign"} : DetectServer(result) + \/ PrepareServer + \/ DecideForeignConsent + \/ StartProbe + \/ \E result \in {"ready", "auth", "unavailable"} : ProbeReturns(result) + \/ ApproveServer + \/ AccountChanges + \/ VerifyOwner + \/ Done + +Spec == Init /\ [][Next]_vars +ForeignProbeNeedsConsent == (target = "foreign" /\ probed) => (interactive /\ consent) +CurrentOwnerAtAdmission == (phase = "ready") => ~ownerChanged +==== diff --git a/verification/collection-admission/models/current.cfg b/verification/collection-admission/models/current.cfg new file mode 100644 index 0000000..de21d95 --- /dev/null +++ b/verification/collection-admission/models/current.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANT RequireForeignConsent = TRUE +CONSTANT RecheckAccount = TRUE +INVARIANTS ForeignProbeNeedsConsent CurrentOwnerAtAdmission diff --git a/verification/collection-admission/models/no-foreign-guard.cfg b/verification/collection-admission/models/no-foreign-guard.cfg new file mode 100644 index 0000000..c66e51b --- /dev/null +++ b/verification/collection-admission/models/no-foreign-guard.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANT RequireForeignConsent = FALSE +CONSTANT RecheckAccount = TRUE +INVARIANTS ForeignProbeNeedsConsent CurrentOwnerAtAdmission diff --git a/verification/collection-admission/models/no-owner-recheck.cfg b/verification/collection-admission/models/no-owner-recheck.cfg new file mode 100644 index 0000000..38cc46a --- /dev/null +++ b/verification/collection-admission/models/no-owner-recheck.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANT RequireForeignConsent = TRUE +CONSTANT RecheckAccount = FALSE +INVARIANTS ForeignProbeNeedsConsent CurrentOwnerAtAdmission diff --git a/verification/collection-admission/models/view.mjs b/verification/collection-admission/models/view.mjs new file mode 100644 index 0000000..5db2e76 --- /dev/null +++ b/verification/collection-admission/models/view.mjs @@ -0,0 +1,71 @@ +export const title = "Prepare to collect into a Personal Server"; + +export function state(v) { + if (v.target === "foreign" && v.probed && !v.consent) { + return "CLI probes a foreign server without permission"; + } + if (v.phase === "ready" && v.ownerChanged) { + return "Collection is admitted for the previous account"; + } + if ( + ["checking", "rechecking", "verify"].includes(v.phase) && + v.ownerChanged + ) { + return "Account changed during the access check"; + } + return { + session: "Checking the Vana account", + "sign-in": "Sign in to Vana", + detect: "Finding a Personal Server", + prepare: "Preparing a Personal Server", + redetect: "Finding a Personal Server", + foreign: "Server belongs to another account", + probe: "Checking server access", + checking: "Checking server access", + approve: "Approve this CLI", + reprobe: "Checking server access", + rechecking: "Checking server access", + verify: "Server access confirmed", + refused: "Collection blocked", + ready: "Ready to collect", + }[v.phase]; +} + +export function step(action, from, to) { + switch (action) { + case "ReadSession": + if (to.phase === "detect") return "Account identified"; + if (to.phase === "sign-in") return "Sign-in required"; + return "No usable account"; + case "SignIn": + return to.phase === "detect" ? "Sign-in succeeds" : "Sign-in fails"; + case "DetectServer": + if (to.phase === "prepare") return "No server found"; + if (to.phase === "foreign") return "Found another owner's server"; + if (to.phase === "probe") return "Found your server"; + return "No usable server"; + case "PrepareServer": + return "Try to find the prepared server"; + case "DecideForeignConsent": + if (to.phase === "refused") return "Permission missing"; + return to.consent + ? "Person allows this server" + : "CLI proceeds without permission"; + case "StartProbe": + return "Send access check"; + case "ProbeReturns": + if (to.phase === "verify") return "Server accepts the CLI"; + if (to.phase === "approve") return "Approval required"; + return "Access unavailable"; + case "ApproveServer": + return to.phase === "reprobe" ? "Person approves" : "Approval fails"; + case "AccountChanges": + return "Account changes"; + case "VerifyOwner": + return to.phase === "ready" + ? "Admit collection" + : "Retry with intended account"; + case "Done": + return "Finish"; + } +} diff --git a/verification/export-settlement/README.md b/verification/export-settlement/README.md new file mode 100644 index 0000000..56cfdc7 --- /dev/null +++ b/verification/export-settlement/README.md @@ -0,0 +1,64 @@ +# Verify CLI export settlement + +A collection can finish while an older upload is still in flight. The local +result path and sync status must belong to the currently accepted receipt. +When a pending export belongs to another account, a competing collector must +keep its result separate and leave the accepted receipt in place. + +## Code map + +| Model action | CLI owner | +| ---------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `CompleteCollection` | `runConnect` in `src/cli/index.ts` receives the runtime's result at its run-specific path and computes the receipt and byte digest. | +| `PublishReceipt` and `RefusePublication` | `updateSourceState` in `src/core/state-store.ts` reloads the source slot under the file lock. `pendingExportBlockReason` in `src/core/source-export.ts` refuses replacement of unresolved foreign or unattributed bytes. A successful publish advances the receipt, result path and initial sync status together. | +| `StartUpload` and `ReceiveUploadResult` | `ingestResult` in `src/personal-server/index.ts` validates the receipt and performs remote I/O outside the source-state lock. | +| `SettleResult` and `RejectStaleResult` | `runConnect` supplies the receipt ID as `settle`. `updateSourceState` compares it with the accepted ID under the lock before merging the result path and sync status. `syncPendingSources` uses the same guard for deferred sync. | + +## Run the check + +From the CLI repository root with installed repository dependencies, +Python 3.12 or later, Node 24, Java and TLC 1.7.4: + +```sh +python3 verification/export-settlement/check.py +``` + +The runner verifies the mapped source and replay blobs at main `a55d0a0006da6a743b6452796435afa6ed177dd8`. + +Use `TLA2TOOLS` and `JAVA` to select installed binaries, or the runner resolves +them through mise. The TLC jar checksum is pinned. The runner checks the two +normal models and two deliberately broken controls. It exports the pinned +revision to scratch, builds the CLI with installed dependencies, runs both +existing regressions, removes one source guard at a time, and restores the +original bytes before rerunning. The synthetic connector and Personal Server +use test records and loopback HTTP. The scratch replay preserves a Node +preload across the fixture's environment filtering to reject outbound +non-loopback connections. It does not open a browser or start a real server. +Use `--out` for a fresh evidence directory. + +Use Pstack `/statechart` with the model files and `view.mjs` in a scratch copy. +The chart combines adjacent steps that keep the same visible receipt and +status. The full TLC verdict comes from the configuration and bounds. + +## Invariants and controls + +The same-owner configuration explores 100 states. The two-owner configuration +explores 52. Both complete without deadlock. The selected built-CLI assertions +pass before and after both deliberate source mutations on each pinned revision. + +| Configuration | Rule checked or broken | +| ------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `same-owner.cfg` and `two-owners.cfg` | `VisibleResultMatchesReceipt` and `ForeignPendingReceiptPreserved` both hold. | +| `no-settle-guard.cfg` | `VisibleResultMatchesReceipt` breaks. A first export starts uploading, a second export becomes current, then the first upload reports back and overwrites the visible state. The real CLI replay holds the first response until the second export has also uploaded. Removing the comparison lets the first command exit successfully instead of refusing stale settlement with exit 5. | +| `no-publish-guard.cfg` | `ForeignPendingReceiptPreserved` breaks. Two collectors finish for different accounts. The second replaces the first account's pending receipt. The real CLI replay lets A queue an interrupted upload before it releases B's already-running collector. Removing the pending-export check lets B publish and upload instead of keeping its result separate with exit 5. | + +The model has one source, two distinct run IDs and two collectors that have +already passed collection admission. Each collector produces one result and +gets one success or failure response. An unresolved export is represented by +a local or failed status. A partial upload with failed scopes is treated as +unresolved. The model treats locked publication and settlement as atomic +transitions. It does not prove the lock algorithm, browser or provider +collection, auth, upload order on the Personal Server, visibility of remote +writes, byte hashing, scope merge behavior, legacy receipt migration, process +crash recovery, or liveness. Deferred sync shares the same settlement guard +but its retry, scope selection and upload behavior is outside this check. diff --git a/verification/export-settlement/check.py b/verification/export-settlement/check.py new file mode 100644 index 0000000..361b8c0 --- /dev/null +++ b/verification/export-settlement/check.py @@ -0,0 +1,242 @@ +#!/usr/bin/env python3 +"""Check export settlement and its negative controls on a pinned CLI revision.""" + +import argparse +import hashlib +import io +import json +import os +from pathlib import Path +import re +import shutil +import subprocess +import sys +import tarfile +import tempfile + +HERE = Path(__file__).resolve().parent +REPO = HERE.parents[1] +JAR_SHA256 = "936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88" +LOCAL = "777cb1824825364aed2b665b5fa9bede59768565" +MAIN = "a55d0a0006da6a743b6452796435afa6ed177dd8" +OWNER_TEST = "test/cli/export-owner.test.ts" +STORE = "src/core/state-store.ts" +REJECT_PUBLISH = ( + "preserves A's admitted bytes when B's already-running collection loses publication" +) +REJECT_SETTLE = ( + "settles only the accepted generation when an earlier upload finishes after a newer collection" +) +SHARED_BLOBS = { + STORE: "b44b264c30d1763ba8c68507abb86c81e88d9946", + "src/core/source-export.ts": "af46b8ad4f4a64d92f6962ec9e8626d952319ef8", + "src/personal-server/index.ts": "7bc722ef96d3e97b626c192a404bb8f1d27ba8ce", +} +SOURCES = { + LOCAL: { + **SHARED_BLOBS, + "src/cli/index.ts": "0a441304a3f7ca729b9b614aa86f8ac472f1425a", + OWNER_TEST: "48a2fe754dc2dfe9275eae8305438ead8027c5cf", + }, + MAIN: { + **SHARED_BLOBS, + "src/cli/index.ts": "817051b3a0f7788c181eca9a684850451ca69766", + OWNER_TEST: "3fbd1d57d23b7e3d086b84ecc0cd20e25cca5fad", + }, +} +CONTROLS = { + "no-publish-guard": { + "rule": "ForeignPendingReceiptPreserved", + "test": REJECT_PUBLISH, + "before": " if (pendingExportBlockReason(current, exportGuard.publish.owner))\n return false;", + "after": " void pendingExportBlockReason;", + "failure": "expected +0 to be 5", + }, + "no-settle-guard": { + "rule": "VisibleResultMatchesReceipt", + "test": REJECT_SETTLE, + "before": "readExportReceipt(current.exportReceipt)?.id !== exportGuard.settle", + "after": "(void readExportReceipt, false)", + "failure": "expected +0 to be 5", + }, +} + + +def command(argv, cwd=REPO, env=None): + return subprocess.run( + argv, cwd=cwd, env=env, capture_output=True, text=True, timeout=100 + ) + + +def checked(argv): + result = command(argv) + if result.returncode: + raise RuntimeError(result.stderr.strip() or result.stdout.strip()) + return result.stdout.strip() + + +def replace_once(source, before, after): + if source.count(before) != 1: + raise RuntimeError(f"Expected a unique scratch mutation anchor: {before}") + return source.replace(before, after) + + +def run_models(out): + pinned_tool = "github:tlaplus/tlaplus@1.7.4" + jar = Path(os.environ.get("TLA2TOOLS") or + Path(checked(["mise", "where", pinned_tool])) / "tla2tools.jar").resolve() + if hashlib.sha256(jar.read_bytes()).hexdigest() != JAR_SHA256: + raise RuntimeError("Use the pinned TLC 1.7.4 jar") + java = os.environ.get("JAVA") or checked( + ["mise", "which", "java", "--tool", "java@temurin-25"] + ) + models = out / "models" + shutil.copytree(HERE / "models", models) + verdicts = {} + for case in ("same-owner", "two-owners", *CONTROLS): + expected = CONTROLS.get(case, {}).get("rule") + result = command([ + java, "-XX:+UseParallelGC", "-cp", str(jar), "tlc2.TLC", + "-workers", "1", "-fp", "0", "-metadir", str(out / f"tlc-{case}"), + "-config", f"{case}.cfg", "ExportSettlement.tla", + ], models) + log = result.stdout + result.stderr + (out / f"{case}-tlc.log").write_text(log) + count = re.search(r"([\d,]+) distinct states found", log) + if expected: + success = result.returncode == 12 and f"Invariant {expected} is violated" in log + else: + success = ( + result.returncode == 0 + and "Model checking completed. No error has been found." in log + and "0 states left on queue" in log + ) + if not success or count is None: + raise RuntimeError(f"Unexpected model verdict: see {out / f'{case}-tlc.log'}") + verdicts[case] = {"states": int(count[1].replace(",", "")), "violation": expected} + return verdicts + + +def replay(snapshot, out, label, cases, control=None): + report = out / f"{label}-tests.json" + node = shutil.which("node") + if not node: + raise RuntimeError("Node 24 is required for the synthetic connector") + preload = snapshot / "loopback-only.cjs" + env = { + "PATH": os.environ["PATH"], + "HOME": str(snapshot), + "VANA_PDPP_NODE": node, + "NODE_OPTIONS": f"--require={json.dumps(str(preload))}", + "CI": "true", + } + result = command( + [ + node, "node_modules/vitest/vitest.mjs", "run", OWNER_TEST, + "-t", "|".join(re.escape(test) for test in cases), + "--reporter=json", f"--outputFile={report}", + ], + snapshot, env, + ) + log = out / f"{label}-tests.log" + log.write_text(result.stdout + result.stderr) + if result.returncode != (1 if control else 0) or not report.is_file(): + raise RuntimeError(f"Unexpected replay exit: see {log}") + assertions = [ + test + for file in json.loads(report.read_text())["testResults"] + for test in file["assertionResults"] + if test["title"] in cases + ] + if sorted(test["title"] for test in assertions) != sorted(cases): + raise RuntimeError(f"Missing replay assertions: see {report}") + for test in assertions: + if control: + errors = " ".join(test["failureMessages"]) + if test["status"] != "failed" or control["failure"] not in errors: + raise RuntimeError(f"Wrong mutation failure: see {report}") + elif test["status"] != "passed": + raise RuntimeError(f"Replay did not pass: see {report}") + + +def run_replays(revision, out): + with tempfile.TemporaryDirectory(prefix="vana-export-replay-") as scratch: + snapshot = Path(scratch) + archive = subprocess.check_output(["git", "archive", revision], cwd=REPO) + with tarfile.open(fileobj=io.BytesIO(archive)) as tar: + tar.extractall( + snapshot, + members=[member for member in tar if not (member.issym() or member.islnk())], + filter="data", + ) + (snapshot / "node_modules").symlink_to(REPO / "node_modules", target_is_directory=True) + shutil.copy2(HERE / "fixtures/loopback-only.cjs", snapshot / "loopback-only.cjs") + owner_test = snapshot / OWNER_TEST + owner_test.write_text(replace_once( + owner_test.read_text(), + " ...cleanEnv,", + " ...cleanEnv,\n NODE_OPTIONS: process.env.NODE_OPTIONS,", + )) + cases = (REJECT_PUBLISH, REJECT_SETTLE) + replay(snapshot, out, "baseline", cases) + source = snapshot / STORE + original = source.read_bytes() + for name, control in CONTROLS.items(): + try: + source.write_text(replace_once( + original.decode(), control["before"], control["after"], + )) + replay(snapshot, out, name, (control["test"],), control) + finally: + source.write_bytes(original) + replay(snapshot, out, "restored", cases) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--ref", help="Check a pinned committed revision") + parser.add_argument("--out", type=Path, help="New evidence directory") + args = parser.parse_args() + revision = checked(["git", "rev-parse", args.ref or MAIN]) + if revision not in SOURCES: + raise RuntimeError("Unknown source revision. Reconcile the model before advancing SOURCES.") + blobs = SOURCES[revision] + for owner, expected in blobs.items(): + if checked(["git", "rev-parse", f"{revision}:{owner}"]) != expected: + raise RuntimeError(f"Model source drift at {owner}") + if not args.ref: + if checked(["git", "hash-object", str(REPO / owner)]) != expected: + raise RuntimeError(f"Working-tree model source drift at {owner}") + if not (REPO / "node_modules/vitest/vitest.mjs").is_file(): + raise RuntimeError("Use existing repository dependencies") + out = args.out.resolve() if args.out else Path(tempfile.mkdtemp(prefix="vana-export-check-")) + if args.out: + out.mkdir(parents=True, exist_ok=False) + verdicts = run_models(out) + run_replays(revision, out) + model_hashes = { + path.name: hashlib.sha256(path.read_bytes()).hexdigest() + for path in sorted((out / "models").iterdir()) + if path.is_file() + } + summary = { + "status": "passed", + "source_revision": revision, + "source_blobs": blobs, + "models": verdicts, + "model_sha256": model_hashes, + "baseline_assertions": 2, + "caught_source_mutations": list(CONTROLS), + "restored_assertions": 2, + "transport": "synthetic loopback only", + } + (out / "summary.json").write_text(json.dumps(summary, indent=2) + "\n") + print(json.dumps({"evidence": str(out), **summary}, indent=2)) + + +if __name__ == "__main__": + try: + main() + except (OSError, RuntimeError, subprocess.SubprocessError) as error: + print(f"Verification error: {error}", file=sys.stderr) + raise SystemExit(2) from error diff --git a/verification/export-settlement/fixtures/loopback-only.cjs b/verification/export-settlement/fixtures/loopback-only.cjs new file mode 100644 index 0000000..e1e8df0 --- /dev/null +++ b/verification/export-settlement/fixtures/loopback-only.cjs @@ -0,0 +1,11 @@ +const net = require("node:net"); + +const connect = net.Socket.prototype.connect; +net.Socket.prototype.connect = function (...args) { + const first = Array.isArray(args[0]) ? args[0][0] : args[0]; + const host = typeof first === "object" ? first?.host : args[1]; + if (host !== "127.0.0.1" && host !== "::1") { + throw new Error("Formal export replay refused a non-loopback connection"); + } + return Reflect.apply(connect, this, args); +}; diff --git a/verification/export-settlement/models/ExportSettlement.tla b/verification/export-settlement/models/ExportSettlement.tla new file mode 100644 index 0000000..81f60fe --- /dev/null +++ b/verification/export-settlement/models/ExportSettlement.tla @@ -0,0 +1,91 @@ +-------------------------- MODULE ExportSettlement -------------------------- +CONSTANTS SameOwner, GuardPublish, GuardSettle + +VARIABLES stage, receipt, visibleGeneration, visibleStatus, foreignReplacement + +vars == <> +Attempts == {"earlier", "later"} +Statuses == {"none", "local", "stored", "failed"} +Phases == {"running", "local", "admitted", "uploading", "response-stored", + "response-failed", "settled", "refused", "superseded"} + +Init == + /\ stage = [id \in Attempts |-> "running"] + /\ receipt = "none" + /\ visibleGeneration = "none" + /\ visibleStatus = "none" + /\ foreignReplacement = FALSE + +CompleteCollection(id) == + /\ stage[id] = "running" + /\ stage' = [stage EXCEPT ![id] = "local"] + /\ UNCHANGED <> + +ForeignPending(id) == + /\ receipt \in Attempts + /\ receipt # id + /\ ~SameOwner + /\ visibleStatus \in {"local", "failed"} + +PublishReceipt(id) == + /\ stage[id] = "local" + /\ (~GuardPublish \/ ~ForeignPending(id)) + /\ stage' = [stage EXCEPT ![id] = "admitted"] + /\ receipt' = id + /\ visibleGeneration' = id + /\ visibleStatus' = "local" + /\ foreignReplacement' = (foreignReplacement \/ ForeignPending(id)) + +RefusePublication(id) == + /\ stage[id] = "local" + /\ GuardPublish /\ ForeignPending(id) + /\ stage' = [stage EXCEPT ![id] = "refused"] + /\ UNCHANGED <> + +StartUpload(id) == + /\ stage[id] = "admitted" + /\ stage' = [stage EXCEPT ![id] = "uploading"] + /\ UNCHANGED <> + +ReceiveUploadResult(id, ok) == + /\ stage[id] = "uploading" + /\ stage' = [stage EXCEPT ![id] = IF ok THEN "response-stored" ELSE "response-failed"] + /\ UNCHANGED <> + +SettleResult(id) == + /\ stage[id] \in {"response-stored", "response-failed"} + /\ (~GuardSettle \/ receipt = id) + /\ stage' = [stage EXCEPT ![id] = "settled"] + /\ visibleGeneration' = id + /\ visibleStatus' = IF stage[id] = "response-stored" THEN "stored" ELSE "failed" + /\ UNCHANGED <> + +RejectStaleResult(id) == + /\ stage[id] \in {"response-stored", "response-failed"} + /\ GuardSettle /\ receipt # id + /\ stage' = [stage EXCEPT ![id] = "superseded"] + /\ UNCHANGED <> + +Done == + /\ \A id \in Attempts : stage[id] \in {"settled", "refused", "superseded"} + /\ UNCHANGED vars + +Next == + \/ \E id \in Attempts : + CompleteCollection(id) \/ PublishReceipt(id) \/ RefusePublication(id) \/ + StartUpload(id) \/ SettleResult(id) \/ RejectStaleResult(id) + \/ \E id \in Attempts, ok \in BOOLEAN : ReceiveUploadResult(id, ok) + \/ Done + +Spec == Init /\ [][Next]_vars + +TypeOK == + /\ stage \in [Attempts -> Phases] + /\ receipt \in Attempts \cup {"none"} + /\ visibleGeneration \in Attempts \cup {"none"} + /\ visibleStatus \in Statuses + /\ foreignReplacement \in BOOLEAN + +VisibleResultMatchesReceipt == visibleGeneration = receipt +ForeignPendingReceiptPreserved == ~foreignReplacement +============================================================================= diff --git a/verification/export-settlement/models/no-publish-guard.cfg b/verification/export-settlement/models/no-publish-guard.cfg new file mode 100644 index 0000000..ca0cce8 --- /dev/null +++ b/verification/export-settlement/models/no-publish-guard.cfg @@ -0,0 +1,6 @@ +SPECIFICATION Spec +CONSTANTS + SameOwner = FALSE + GuardPublish = FALSE + GuardSettle = TRUE +INVARIANTS TypeOK VisibleResultMatchesReceipt ForeignPendingReceiptPreserved diff --git a/verification/export-settlement/models/no-settle-guard.cfg b/verification/export-settlement/models/no-settle-guard.cfg new file mode 100644 index 0000000..701dd6a --- /dev/null +++ b/verification/export-settlement/models/no-settle-guard.cfg @@ -0,0 +1,6 @@ +SPECIFICATION Spec +CONSTANTS + SameOwner = TRUE + GuardPublish = TRUE + GuardSettle = FALSE +INVARIANTS TypeOK VisibleResultMatchesReceipt ForeignPendingReceiptPreserved diff --git a/verification/export-settlement/models/same-owner.cfg b/verification/export-settlement/models/same-owner.cfg new file mode 100644 index 0000000..0ee9ab3 --- /dev/null +++ b/verification/export-settlement/models/same-owner.cfg @@ -0,0 +1,6 @@ +SPECIFICATION Spec +CONSTANTS + SameOwner = TRUE + GuardPublish = TRUE + GuardSettle = TRUE +INVARIANTS TypeOK VisibleResultMatchesReceipt ForeignPendingReceiptPreserved diff --git a/verification/export-settlement/models/two-owners.cfg b/verification/export-settlement/models/two-owners.cfg new file mode 100644 index 0000000..f9d3f20 --- /dev/null +++ b/verification/export-settlement/models/two-owners.cfg @@ -0,0 +1,6 @@ +SPECIFICATION Spec +CONSTANTS + SameOwner = FALSE + GuardPublish = TRUE + GuardSettle = TRUE +INVARIANTS TypeOK VisibleResultMatchesReceipt ForeignPendingReceiptPreserved diff --git a/verification/export-settlement/models/view.mjs b/verification/export-settlement/models/view.mjs new file mode 100644 index 0000000..4ede7c9 --- /dev/null +++ b/verification/export-settlement/models/view.mjs @@ -0,0 +1,55 @@ +export const title = "Collect data and preserve the latest accepted export"; + +export function state(values) { + if (values.visibleGeneration !== values.receipt) { + return "An old response replaces the accepted result"; + } + if (values.foreignReplacement) { + return "Another account replaces the pending export"; + } + if (values.receipt === "none") { + return "Collectors running without an accepted export"; + } + if (Object.values(values.stage).includes("superseded")) { + return "Older response discarded. Newer export retained"; + } + if (Object.values(values.stage).includes("refused")) { + return "Other account's export stays local"; + } + if (values.visibleStatus === "stored") { + return "Accepted export stored"; + } + if (values.visibleStatus === "failed") { + return "Accepted export remains local after an upload failure"; + } + if (values.stage[values.receipt] === "uploading") { + return "Accepted export local. Upload pending"; + } + return "Accepted export recorded locally"; +} + +export function step(action, from, to) { + if (action === "PublishReceipt" && from.receipt !== "none") { + return to.foreignReplacement + ? "Accept the other account's export" + : "Accept the newer export"; + } + const changed = Object.keys(from.stage).find( + (id) => from.stage[id] !== to.stage[id], + ); + if (changed && changed !== from.receipt) { + if (action === "StartUpload") return "Older export starts uploading"; + if (action === "ReceiveUploadResult") return "Older upload reports back"; + if (action === "SettleResult") return "Apply the older upload result"; + } + return { + CompleteCollection: "A connector finishes collecting", + PublishReceipt: "Record the local export", + RefusePublication: "Refuse to replace another account's export", + StartUpload: "Upload to Personal Server", + ReceiveUploadResult: "Personal Server responds", + SettleResult: "Record the upload result", + RejectStaleResult: "Discard settlement for the older export", + Done: "Finish", + }[action]; +} diff --git a/verification/hosted-provisioning/README.md b/verification/hosted-provisioning/README.md new file mode 100644 index 0000000..3b32cde --- /dev/null +++ b/verification/hosted-provisioning/README.md @@ -0,0 +1,58 @@ +# Hosted server provisioning and deletion + +The current Connect API can acknowledge deletion of a provisioning row, then +acknowledge the original creation after the provider finishes. The successful +create has no row or provider handles left for the owner to find or remove. + +The normal [server page](../../connect/src/app/server/page.tsx) hides Remove +Server while provisioning. The authenticated API still allows it. A signed +owner can list the provisioning record and send its ID to DELETE directly. +This is a source and controlled-route finding. Deployment exposure and live +cloud resources were outside the replay. + +## Source and model + +The runner pins the checked source and replays at main `a55d0a0006da6a743b6452796435afa6ed177dd8`. + +| Action | Source boundary | +| ------------------------ | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Reserve and list | [Server collection route](../../connect/src/app/api/servers/route.ts) inserts a provisioning row without handles before it awaits the provider. The owner can list this row while the POST waits. | +| Read for deletion | [Server item route](../../connect/src/app/api/servers/%5Bid%5D/route.ts) checks the owner and starts provider cleanup only if the row snapshot has a VM, tunnel or DNS handle. | +| Delete the row | The item route awaits cleanup when it found handles, otherwise it immediately calls `deleteServer` and returns success. | +| Publish provider handles | The collection route writes provider handles and the control-plane token. [The store](../../connect/src/lib/db/neon.ts) returns null when the row is missing. The route falls back to the earlier row and returns 201. | + +TLC checks one owner, one hosted server, one creation, and one deletion. +Reservation, provider reply, handle publication and response are separate steps. +The model assumes successful provider calls and a surviving resource after +provider success. It leaves out retries, partial provider cleanup, database +failures, a second create, and the network and chain lifecycle. The replay +substitutes an in-memory database and provider. It holds either the reservation +response, after the row is visible, or the provider response. +It uses the actual route handlers and signature recovery with an ephemeral test +wallet. Unexpected external fetch fails. + +## Run + +Use Python 3.12+, Node and Connect's installed Vitest. The checker uses TLC +1.7.4 and Java, with `TLA2TOOLS` and `JAVA` available as overrides. + +```sh +python3 verification/hosted-provisioning/check.py +``` + +The current model must violate `CreatedResourceHasTrackingRow`. Its replay +lists the new row and deletes it with HTTP 200 before provider handles exist. +The shortest path holds the DB reply before the provider is invoked. The other +replay holds the provider itself. Both then let creation finish. Create returns HTTP 201, no cleanup was sent and the +owner's listing is empty while the fixture resource remains. + +The scratch control adds a 409 refusal while the row is provisioning. Its model +passes and the same replay keeps the provider handles in the list. The runner +restores the original route and reproduces the finding again. It prints the +evidence directory. Exit 0 means the known finding and both replay outcomes were +observed. The guard remains in the scratch replay only. + +Read both models with Pstack `/statechart`, using `models/view.mjs` in a +scratch copy. The chart folds internal transitions that leave the display +label unchanged. Reconcile the code, model and expected outcomes if the covered +source changes. diff --git a/verification/hosted-provisioning/check.py b/verification/hosted-provisioning/check.py new file mode 100644 index 0000000..0858a65 --- /dev/null +++ b/verification/hosted-provisioning/check.py @@ -0,0 +1,171 @@ +#!/usr/bin/env python3 +"""Reproduce the hosted provisioning/delete race and check a scratch guard.""" + +import argparse +import hashlib +import io +import json +import os +from pathlib import Path +import re +import shutil +import subprocess +import sys +import tarfile +import tempfile + +HERE = Path(__file__).resolve().parent +REPO = HERE.parents[1] +SOURCE_REVISION = "a55d0a0006da6a743b6452796435afa6ed177dd8" +DELETE_ROUTE = "connect/src/app/api/servers/[id]/route.ts" +OWNERS = { + "connect/src/app/api/servers/route.ts": "118c75f3f1fd3f130cb831b5a04d6391a5a3b956", + DELETE_ROUTE: "0260ec6d1b468546fcd64b102bda992149209785", + "connect/src/lib/db/neon.ts": "13dc895dd0783f863d9ec258a5999994ac48b9f6", + "connect/src/lib/api-auth.ts": "e2c1a60fda0a05a313a8c63cf509a41318016a54", + "connect/src/lib/api-server.ts": "b196dafa9e0b89f59c1c7cbf7d55ee7e86e755cb", + "connect/src/lib/api-error.ts": "5b0c1f5de52af344afd5addffa37377e7a26ee67", + "connect/src/lib/server-provider/gcp.ts": "985af1d609a559f5ad5751dee29a8774f8514ea6", + "connect/vitest.config.ts": "b7689c0dc27e999c37e7da456d26b9ab87298e9a", +} +JAR_SHA256 = "936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88" +FINDING = "CreatedResourceHasTrackingRow" +GUARD_ANCHOR = ' if (server.provider_id || server.tunnel_id || server.dns_record_id) {' +GUARD = ''' if (server.state === "provisioning") { + return apiError("conflict_error", "Wait for provisioning to finish.", 409); + } + +''' + + +def git(*args): + return subprocess.check_output(["git", *args], cwd=REPO, text=True).strip() + + +def run(argv, cwd, log, env=None): + result = subprocess.run(argv, cwd=cwd, env=env, capture_output=True, text=True, timeout=90) + text = result.stdout + result.stderr + log.write_text(text) + return result.returncode, text + + +def check_models(out, java, jar): + modeldir = out / "models" + shutil.copytree(HERE / "models", modeldir) + reports = {} + for name, expected in (("current", FINDING), ("refuse-provisioning-delete", None)): + log = out / f"{name}-tlc.log" + code, text = run( + [java, "-XX:+UseParallelGC", "-Xmx768m", "-cp", jar, "tlc2.TLC", + "-workers", "1", "-fp", "0", "-metadir", str(out / f"tlc-{name}"), + "-config", f"{name}.cfg", "HostedProvisioning.tla"], + modeldir, log, + ) + state_count = re.search(r"(\d+) distinct states found", text) + violated = re.search(r"Invariant (\w+) is violated", text) + actual = violated[1] if violated else None + if ( + code != (12 if expected else 0) + or actual != expected + or not state_count + or (expected is None and "No error has been found" not in text) + ): + raise RuntimeError(f"Unexpected model outcome for {name}. See {log}") + reports[name] = {"states": int(state_count[1]), "violation": actual} + return reports + + +def replay(revision, out): + node = shutil.which("node") + deps = REPO / "connect/node_modules" + vitest = deps / "vitest/vitest.mjs" + if not node or not vitest.is_file(): + raise RuntimeError("Use Node and Connect's installed Vitest") + with tempfile.TemporaryDirectory(prefix="vana-hosted-provisioning-") as tmp: + snapshot = Path(tmp) + archive = subprocess.check_output( + ["git", "archive", revision, "--", "connect"], cwd=REPO, + ) + with tarfile.open(fileobj=io.BytesIO(archive)) as tar: + tar.extractall( + snapshot, + members=[m for m in tar.getmembers() if not (m.issym() or m.islnk())], + filter="data", + ) + connect = snapshot / "connect" + (connect / "node_modules").symlink_to(deps, target_is_directory=True) + fixture = "src/app/api/servers/provision-delete-race.test.ts" + shutil.copy2(HERE / "replay.test.ts", connect / fixture) + command = [node, str(vitest), "run", fixture, "--environment", "node", "--reporter=verbose"] + source = snapshot / DELETE_ROUTE + original = source.read_bytes() + contents = original.decode() + if contents.count(GUARD_ANCHOR) != 1: + raise RuntimeError("Delete guard anchor drift") + + def require_outcome(name, guarded): + log = out / f"{name}-replay.log" + env = { + **os.environ, "CI": "true", "TMPDIR": tmp, "NO_COLOR": "1", + "VANA_HOSTED_REPLAY_GUARD": str(int(guarded)), + } + code, text = run(command, connect, log, env) + if code != 0 or not re.search(r"^ *Tests +2 passed \(2\) *$", text, re.MULTILINE): + raise RuntimeError(f"Unexpected replay outcome for {name}. See {log}") + + require_outcome("current", False) + try: + source.write_text(contents.replace(GUARD_ANCHOR, GUARD + GUARD_ANCHOR)) + require_outcome("guarded", True) + finally: + source.write_bytes(original) + require_outcome("restored", False) + if source.read_bytes() != original: + raise RuntimeError("Scratch route was not restored") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--ref", help="Check the named revision if its source blobs match") + parser.add_argument("--out", type=Path) + args = parser.parse_args() + revision = git("rev-parse", args.ref or SOURCE_REVISION) + for owner, expected in OWNERS.items(): + current = git("rev-parse", f"{revision}:{owner}") if args.ref else git("hash-object", str(REPO / owner)) + if current != expected or git("rev-parse", f"{revision}:{owner}") != expected: + raise RuntimeError(f"Model/source drift in {owner}. Reconcile the model before advancing its source record.") + jar = os.environ.get("TLA2TOOLS") + if not jar: + tools = subprocess.check_output(["mise", "where", "github:tlaplus/tlaplus@1.7.4"], cwd=REPO, text=True).strip() + jar = str(Path(tools) / "tla2tools.jar") + jar = str(Path(jar).resolve()) + if hashlib.sha256(Path(jar).read_bytes()).hexdigest() != JAR_SHA256: + raise RuntimeError("Use the pinned TLC 1.7.4 jar") + java = os.environ.get("JAVA") or subprocess.check_output( + ["mise", "which", "java", "--tool", "java@temurin-25"], cwd=REPO, text=True + ).strip() + out = args.out.resolve() if args.out else Path(tempfile.mkdtemp(prefix="vana-hosted-proof-")) + if args.out: + out.mkdir(parents=True, exist_ok=False) + models = check_models(out, java, jar) + replay(revision, out) + summary = { + "revision": revision, "source_blobs": OWNERS, "tool": "TLC 1.7.4", + "models": models, "finding": FINDING, + "replays": { + "current": "two schedules: DELETE 200, POST 201, resource not listed", + "guarded": "two schedules: DELETE 409, POST 201, provider handles listed", + "restored": "both original schedules reproduced again", + }, + "scratch_source_restored": True, + } + (out / "summary.json").write_text(json.dumps(summary, indent=2) + "\n") + print(f"Reproduced hosted provisioning race and checked the scratch guard. Evidence in {out}") + + +if __name__ == "__main__": + try: + main() + except (OSError, RuntimeError, subprocess.SubprocessError) as error: + print(f"Verification error: {error}", file=sys.stderr) + raise SystemExit(2) from error diff --git a/verification/hosted-provisioning/models/HostedProvisioning.tla b/verification/hosted-provisioning/models/HostedProvisioning.tla new file mode 100644 index 0000000..3c520e2 --- /dev/null +++ b/verification/hosted-provisioning/models/HostedProvisioning.tla @@ -0,0 +1,71 @@ +---- MODULE HostedProvisioning ---- + +CONSTANT RefuseProvisioningDelete +VARIABLES row, create, deletion, resource, listed +vars == <> + +Init == /\ row = "absent" + /\ create = "idle" + /\ deletion = "idle" + /\ resource = FALSE + /\ listed = FALSE + +ReserveRow == /\ create = "idle" + /\ create' = "reserved" + /\ row' = "without_handles" + /\ UNCHANGED <> + +StartProvider == /\ create = "reserved" + /\ create' = "provisioning" + /\ UNCHANGED <> + +ListRow == /\ row # "absent" + /\ ~listed + /\ listed' = TRUE + /\ UNCHANGED <> + +ProviderReturns == /\ create = "provisioning" + /\ create' = "provider_returned" + /\ resource' = TRUE + /\ UNCHANGED <> + +SaveHandles == /\ create = "provider_returned" + /\ row' = IF row = "absent" THEN "absent" ELSE "with_handles" + /\ create' = "handles_written" + /\ UNCHANGED <> + +ReturnCreated == /\ create = "handles_written" + /\ create' = "created" + /\ UNCHANGED <> + +ObserveRunning == /\ row = "with_handles" + /\ row' = "running" + /\ UNCHANGED <> + +ReadDeleteRow == /\ listed + /\ row # "absent" + /\ deletion = "idle" + /\ deletion' = IF RefuseProvisioningDelete /\ row # "running" THEN "refused" + ELSE IF row = "without_handles" THEN "skip_cleanup" + ELSE "cleaning" + /\ UNCHANGED <> + +ProviderCleanup == /\ deletion = "cleaning" + /\ resource' = FALSE + /\ deletion' = "cleanup_done" + /\ UNCHANGED <> + +DeleteRow == /\ deletion \in {"skip_cleanup", "cleanup_done"} + /\ row' = "absent" + /\ deletion' = "deleted" + /\ UNCHANGED <> + +Done == /\ create = "created" + /\ UNCHANGED vars + +Next == ReserveRow \/ StartProvider \/ ListRow \/ ProviderReturns \/ SaveHandles + \/ ReturnCreated \/ ObserveRunning \/ ReadDeleteRow \/ ProviderCleanup \/ DeleteRow \/ Done +Spec == Init /\ [][Next]_vars + +CreatedResourceHasTrackingRow == ~(create = "created" /\ resource /\ row = "absent") +==== diff --git a/verification/hosted-provisioning/models/current.cfg b/verification/hosted-provisioning/models/current.cfg new file mode 100644 index 0000000..ac0d160 --- /dev/null +++ b/verification/hosted-provisioning/models/current.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +CONSTANT RefuseProvisioningDelete = FALSE +INVARIANT CreatedResourceHasTrackingRow diff --git a/verification/hosted-provisioning/models/refuse-provisioning-delete.cfg b/verification/hosted-provisioning/models/refuse-provisioning-delete.cfg new file mode 100644 index 0000000..1573571 --- /dev/null +++ b/verification/hosted-provisioning/models/refuse-provisioning-delete.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +CONSTANT RefuseProvisioningDelete = TRUE +INVARIANT CreatedResourceHasTrackingRow diff --git a/verification/hosted-provisioning/models/view.mjs b/verification/hosted-provisioning/models/view.mjs new file mode 100644 index 0000000..626b0c7 --- /dev/null +++ b/verification/hosted-provisioning/models/view.mjs @@ -0,0 +1,46 @@ +export const title = "Delete a hosted server while provisioning is pending"; + +export function state(value) { + if (value.row === "absent" && value.resource && value.create === "created") + return "Creation reports success but the server has no record"; + if (value.deletion === "deleted") { + if (value.create === "created") return "Server removed"; + if (value.resource) return "Provider returned after deletion"; + return "Record removed before provider finished"; + } + if (value.deletion === "refused") { + return value.create === "created" + ? "Server creation retained" + : "Deletion refused while provisioning"; + } + if (value.deletion === "skip_cleanup") + return "Deletion sees no provider handles"; + if (value.deletion === "cleaning") return "Cleaning up provider resources"; + if (value.deletion === "cleanup_done") return "Provider resources removed"; + if (value.row === "running") return "Server running"; + if (value.row === "with_handles") return "Provisioned server is tracked"; + if (value.listed) return "Owner can see the provisioning record"; + if (value.create === "idle") return "No hosted server"; + return "Server provisioning"; +} + +export function step(action, _from, to) { + if (action === "ReadDeleteRow") { + if (to.deletion === "refused") return "owner attempts deletion too early"; + if (to.deletion === "skip_cleanup") + return "owner deletes before handles exist"; + return "owner requests deletion"; + } + return { + ReserveRow: "start server creation", + StartProvider: "start provider provisioning", + ListRow: "owner lists servers", + ProviderReturns: "provider creates the server", + SaveHandles: "try to store provider handles", + ReturnCreated: "create returns success", + ObserveRunning: "provider reports running", + ProviderCleanup: "provider finishes cleanup", + DeleteRow: "delete the server record", + Done: "finish", + }[action]; +} diff --git a/verification/hosted-provisioning/replay.test.ts b/verification/hosted-provisioning/replay.test.ts new file mode 100644 index 0000000..726daa8 --- /dev/null +++ b/verification/hosted-provisioning/replay.test.ts @@ -0,0 +1,137 @@ +import { afterEach, expect, it, vi } from "vitest"; +import { NextRequest } from "next/server"; +import { generatePrivateKey, privateKeyToAccount } from "viem/accounts"; +import type { PersonalServer } from "@/lib/db/neon"; + +type HoldAt = "reservation" | "provider"; + +const ports = vi.hoisted(() => ({ + holdAt: "provider" as HoldAt, + row: null as PersonalServer | null, + resources: new Set(), + started: Promise.withResolvers(), + release: Promise.withResolvers(), + deprovision: vi.fn(), +})); + +vi.mock("@/lib/db/neon", () => ({ + findServerByUserId: async (userId: string) => + ports.row?.user_id === userId ? ports.row : null, + insertServerIfNotExists: async (identity: Partial) => { + ports.row = { + ...identity, + provider_id: null, + control_plane_token: null, + vm_ip: null, + url: null, + disk_id: null, + disk_expires: null, + tunnel_id: null, + dns_record_id: null, + created_at: "2026-01-01", + updated_at: "2026-01-01", + } as PersonalServer; + const inserted = ports.row; + if (ports.holdAt === "reservation") { + ports.started.resolve(); + await ports.release.promise; + } + return inserted; + }, + findServerById: async (id: string) => + ports.row?.id === id ? ports.row : null, + deleteServer: async (id: string) => { + if (ports.row?.id === id) ports.row = null; + }, + updateServer: async (id: string, fields: Partial) => { + if (ports.row?.id !== id) return null; + ports.row = { ...ports.row, ...fields }; + return ports.row; + }, + updateServerControlPlaneToken: async () => {}, +})); + +vi.mock("@/lib/server-provider", () => ({ + getServerProvider: () => ({ + provision: async () => { + if (ports.holdAt === "provider") { + ports.started.resolve(); + await ports.release.promise; + } + ports.resources.add("fixture-vm"); + return { serverId: "fixture-vm", url: "https://fixture.example" }; + }, + deprovision: ports.deprovision, + }), +})); + +import { GET, POST } from "./route"; +import { DELETE } from "./[id]/route"; + +afterEach(() => vi.unstubAllGlobals()); + +it.each(["reservation", "provider"])( + "replays authenticated DELETE during a held %s response", + async (holdAt) => { + ports.row = null; + ports.holdAt = holdAt; + ports.started = Promise.withResolvers(); + ports.release = Promise.withResolvers(); + ports.resources.clear(); + ports.deprovision.mockClear(); + vi.stubGlobal("fetch", () => { + throw new Error("External I/O disabled"); + }); + const account = privateKeyToAccount(generatePrivateKey()); + const signature = await account.signMessage({ + message: "vana-master-key-v1", + }); + const headers = { authorization: `Bearer ${signature}` }; + const collection = "https://fixture.example/api/servers"; + const creating = POST( + new NextRequest(collection, { + method: "POST", + headers: { "content-type": "application/json" }, + body: JSON.stringify({ masterKeySignature: signature }), + }), + ); + + let deleted: Response; + try { + await ports.started.promise; + const listed = await GET(new NextRequest(collection, { headers })); + const { + data: [entry], + } = await listed.json(); + expect(entry).toMatchObject({ state: "provisioning", provider_id: null }); + + deleted = await DELETE( + new NextRequest(`${collection}/${entry.id}`, { + method: "DELETE", + headers, + }), + { params: Promise.resolve({ id: entry.id }) }, + ); + } finally { + ports.release.resolve(); + } + + const created = await creating; + const inventory = await ( + await GET(new NextRequest(collection, { headers })) + ).json(); + expect(created.status).toBe(201); + expect(ports.deprovision).not.toHaveBeenCalled(); + expect([...ports.resources]).toEqual(["fixture-vm"]); + + if (process.env.VANA_HOSTED_REPLAY_GUARD === "1") { + expect(deleted.status).toBe(409); + expect(inventory.data).toMatchObject([{ provider_id: "fixture-vm" }]); + return; + } + + expect(deleted.status).toBe(200); + expect(await deleted.json()).toMatchObject({ deleted: true }); + expect(inventory).toMatchObject({ data: [] }); + }, +); diff --git a/verification/mainnet-registration/README.md b/verification/mainnet-registration/README.md new file mode 100644 index 0000000..3911379 --- /dev/null +++ b/verification/mainnet-registration/README.md @@ -0,0 +1,56 @@ +# Mainnet registration recovery + +This check covers `vana app register --network mainnet` after a builder has a +Moksha app owned by their Account. The CLI saves the exact promotion context, +reuses a visible registration after an interrupted response, and waits for a +confirmed proof of the same app before asking Account to associate it. + +## Source and model + +The runner pins the checked source and replays at main `a55d0a0006da6a743b6452796435afa6ed177dd8`. + +| Step | Source boundary | +| -------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Admit existing app | `runAppRegister` resolves an existing key. `runMainnetRegistration` checks the saved app, account origin, gateway, network, environment, and production metadata. It checks current Account subject and Moksha ownership before saving. | +| Save context | `createAppRegistrationStore.saveRegistration` compares the existing identity under a writer lock and writes through a temporary file, atomic rename, and directory sync. The model steps at successful return. | +| Read then submit | `runMainnetRegistration` calls `getBuilder` and invokes `registerBuilder` only on an absent result. The model separates a gateway acceptance from whether its response reaches the CLI. | +| Wait and match proof | `waitForMainnetConfirmation` polls the gateway with GET. It requires a confirmed response and compares its owner, grantee address, key, and app URL before returning. | +| Associate and finish | The CLI submits the association proof, checks mainnet ownership for the original Account subject, saves the production profile and clears the matching journal. | + +The model covers one app, one Account, one frozen production URL and name, +and at most two sequential invocations. It abstracts filesystem publication +as a completed store call. It assumes the gateway lookup sees an accepted +registration when a later invocation starts. If the gateway still reports +absence, the source can submit again. The invariant covers visible records. +The check does not cover overlapping invocations, clock accuracy, the chain's +registration idempotency, signature correctness or delivery by live services. +The owner replays independently check the signed association wire payload, +context mismatch, and no replacement key behavior. + +## Run + +Use Python 3.12+, Node and the repo's installed Vitest. The checker uses +TLC 1.7.4 and Java, with `TLA2TOOLS` and `JAVA` available as overrides. + +```sh +python3 verification/mainnet-registration/check.py +``` + +The checker verifies the source blobs, runs TLC, and replays the production CLI +command against synthetic gateway and Account responses. It removes each guard +in a temporary source snapshot, checks the selected test fails at its expected +assertion, restores the snapshot, and runs the tests again. The replay uses +fixture state and rejects external fetch. The reported evidence directory +contains raw logs and `summary.json`. + +| Control | Named violation | Observable replay failure | +| ----------------------------- | -------------------------------- | ---------------------------------------------------------------------------------------------------------------- | +| `no-save-context` | `ContextSavedBeforeRegistration` | Gateway returns pending until timeout and the expected recovery journal is absent. | +| `no-proof-wait` | `MatchingProofBeforeAssociation` | The command asks Account while the proof is pending. The synthetic Account rejects the association. | +| `no-proof-identity` | `MatchingProofBeforeAssociation` | A confirmed proof for a different owner reaches Account. The command reports success instead of refusing it. | +| `repeat-visible-registration` | `NoPostForVisibleRegistration` | The first registration reply is lost. A later invocation submits again instead of recovering the visible record. | + +Use Pstack `/statechart` on a scratch copy with `models/view.mjs`. The chart +folds polling and proof settlement that leave the person waiting into the +same displayed state. Reconcile the model and tests when the covered code +changes, then update the source record and rerun all controls. diff --git a/verification/mainnet-registration/check.py b/verification/mainnet-registration/check.py new file mode 100644 index 0000000..bdbfd57 --- /dev/null +++ b/verification/mainnet-registration/check.py @@ -0,0 +1,213 @@ +#!/usr/bin/env python3 +"""Check the mainnet registration model and its offline CLI replays.""" + +import argparse +import hashlib +import io +import json +import os +from pathlib import Path +import re +import shutil +import subprocess +import sys +import tarfile +import tempfile + +HERE = Path(__file__).resolve().parent +REPO = HERE.parents[1] +SOURCE_REVISION = "a55d0a0006da6a743b6452796435afa6ed177dd8" +SOURCE = "src/cli/app/mainnet-registration.ts" +TEST = "test/cli/app-mainnet-registration.test.ts" +NO_EXTERNAL_IO = "verification/setup-resume/fixtures/no-external-io.ts" +OWNERS = { + SOURCE: "91ddcd4e45b7a2db29ec56f37a6d1af7e2ffa84f", + "src/cli/app/register.ts": "3913660436ac5bf8d2ee7a81ff3072626b7942be", + "src/core/app-registration-store.ts": "be4bf315897c7fc177b81479fe36428463c496c6", + "src/core/app-profile.ts": "28e749ce192b697d37c166b67b3e42c9839979e1", + "src/core/network.ts": "5d7ed00b5e234edb98f278243522b59dd8d433c5", + "src/core/app-key.ts": "380b625fad6e98eb8f0c18bbd56a5e8ed83492e7", + TEST: "9595034418fd6e002e8dca74ae60e0ef201fcd24", + "test/setup/isolate-home.ts": "0341171c4dcd2df5e42f226a42bc7a9551d7ae73", + NO_EXTERNAL_IO: "ad91a47d1321bbf34acdba2b7a726291ac3a9cc7", +} +JAR_SHA256 = "936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88" +CONTROLS = { + "no-save-context": ( + "ContextSavedBeforeRegistration", + "store.saveRegistration(context);", + "void store;", + "retains the operation when confirmation stays pending", + "expected null not to be null", + ), + "no-proof-wait": ( + "MatchingProofBeforeAssociation", + "await waitForMainnetConfirmation(network, key, appUrl, request);", + "void waitForMainnetConfirmation;", + "waits for the gateway's pending proof", + "expected 6 to be +0", + ), + "no-proof-identity": ( + "MatchingProofBeforeAssociation", + "if (!matchesRegistration(body.data, key, appUrl)) {", + "if (false) {", + "does not associate a changed-owner confirmation", + "expected +0 to be 2", + ), + "repeat-visible-registration": ( + "NoPostForVisibleRegistration", + "if (!builder) {", + "if (!builder || saved) {", + "recovers a lost gateway response", + "expected 6 to be +0", + ), +} + + +def git(*args): + return subprocess.check_output(["git", *args], cwd=REPO, text=True).strip() + + +def run(argv, cwd, log, env=None): + result = subprocess.run(argv, cwd=cwd, env=env, capture_output=True, text=True, timeout=90) + output = result.stdout + result.stderr + log.write_text(output) + return result.returncode, output + + +def check_models(out, java, jar): + modeldir = out / "models" + shutil.copytree(HERE / "models", modeldir) + reports = {} + for case in ("current", *CONTROLS): + log = out / f"{case}-tlc.log" + code, text = run( + [java, "-XX:+UseParallelGC", "-Xmx768m", "-cp", jar, "tlc2.TLC", + "-workers", "1", "-fp", "0", "-metadir", str(out / f"tlc-{case}"), + "-config", f"{case}.cfg", "MainnetRegistration.tla"], + modeldir, log, + ) + state_count = re.search(r"(\d+) distinct states found", text) + violated = re.search(r"Invariant (\w+) is violated", text) + actual = violated[1] if violated else None + expected = CONTROLS[case][0] if case in CONTROLS else None + expected_code = 12 if expected else 0 + if ( + code != expected_code + or actual != expected + or not state_count + or (expected is None and "No error has been found" not in text) + ): + raise RuntimeError(f"Unexpected model outcome for {case}. See {log}") + reports[case] = {"states": int(state_count[1]), "violation": actual} + return reports + + +def replay(revision, out): + node = shutil.which("node") + vitest = REPO / "node_modules/vitest/vitest.mjs" + if not node or not vitest.is_file(): + raise RuntimeError("Use Node and the repository's installed Vitest") + with tempfile.TemporaryDirectory(prefix="vana-mainnet-registration-") as tmp: + snapshot = Path(tmp) + archive = subprocess.check_output( + ["git", "archive", revision, "--", "src", "package.json", + TEST, "test/setup/isolate-home.ts"], + cwd=REPO, + ) + with tarfile.open(fileobj=io.BytesIO(archive)) as tar: + tar.extractall( + snapshot, + members=[m for m in tar.getmembers() if not (m.issym() or m.islnk())], + filter="data", + ) + (snapshot / NO_EXTERNAL_IO).parent.mkdir(parents=True) + shutil.copy2(REPO / NO_EXTERNAL_IO, snapshot / NO_EXTERNAL_IO) + (snapshot / "node_modules").symlink_to(REPO / "node_modules", target_is_directory=True) + (snapshot / "vitest.formal.config.mts").write_text( + "export default {test:{" + f"include:[{json.dumps(TEST)}]," + f"setupFiles:['test/setup/isolate-home.ts',{json.dumps(NO_EXTERNAL_IO)}]" + "}};\n" + ) + command = [node, str(vitest), "run", "--config", "vitest.formal.config.mts", "--reporter=verbose"] + env = {**os.environ, "CI": "true", "TMPDIR": tmp, "NO_COLOR": "1"} + reports = {} + source = snapshot / SOURCE + original = source.read_bytes() + + def require_passing(name): + log = out / f"{name}-tests.log" + code, text = run(command, snapshot, log, env) + count = re.search(r"^ *Tests +([0-9]+) passed \(\1\) *$", text, re.MULTILINE) + if code != 0 or not count: + raise RuntimeError(f"Expected passing tests. See {log}") + return int(count[1]) + + reports["baseline"] = require_passing("baseline") + for name, (_, old, new, selection, assertion) in CONTROLS.items(): + contents = original.decode() + if contents.count(old) != 1: + raise RuntimeError(f"Mutation anchor drift for {name}") + log = out / f"{name}-mutation.log" + try: + source.write_text(contents.replace(old, new)) + code, text = run([*command, "-t", selection], snapshot, log, env) + finally: + source.write_bytes(original) + if code != 1 or f"AssertionError: {assertion}" not in text or selection not in text: + raise RuntimeError(f"Expected a selected behavioral failure. See {log}") + reports[name] = "selected test rejected the source mutation" + reports["restored"] = require_passing("restored") + if reports["restored"] != reports["baseline"] or source.read_bytes() != original: + raise RuntimeError("Scratch replay was not restored") + return reports + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--ref", help="Check the named revision if its source blobs match") + parser.add_argument("--out", type=Path) + args = parser.parse_args() + revision = git("rev-parse", args.ref or SOURCE_REVISION) + for owner, expected in OWNERS.items(): + path = REPO / owner + if owner == NO_EXTERNAL_IO: + if git("hash-object", str(path)) != expected: + raise RuntimeError(f"Replay fixture drift in {owner}") + continue + actual = git("rev-parse", f"{revision}:{owner}") if args.ref else git("hash-object", str(path)) + if actual != expected: + raise RuntimeError(f"Model/source drift in {owner}. Reconcile the model before advancing its source record.") + if git("rev-parse", f"{revision}:{owner}") != expected: + raise RuntimeError(f"Replay revision does not contain the pinned {owner}") + + jar = os.environ.get("TLA2TOOLS") + if not jar: + tools = subprocess.check_output(["mise", "where", "github:tlaplus/tlaplus@1.7.4"], cwd=REPO, text=True).strip() + jar = str(Path(tools) / "tla2tools.jar") + jar = str(Path(jar).resolve()) + if hashlib.sha256(Path(jar).read_bytes()).hexdigest() != JAR_SHA256: + raise RuntimeError("Use the pinned TLC 1.7.4 jar") + java = os.environ.get("JAVA") or subprocess.check_output( + ["mise", "which", "java", "--tool", "java@temurin-25"], cwd=REPO, text=True + ).strip() + out = args.out.resolve() if args.out else Path(tempfile.mkdtemp(prefix="vana-mainnet-proof-")) + if args.out: + out.mkdir(parents=True, exist_ok=False) + models = check_models(out, java, jar) + replays = replay(revision, out) + summary = { + "revision": revision, "source_blobs": OWNERS, "tool": "TLC 1.7.4", + "models": models, "replays": replays, "scratch_source_restored": True, + } + (out / "summary.json").write_text(json.dumps(summary, indent=2) + "\n") + print(f"Checked mainnet registration. Evidence in {out}") + + +if __name__ == "__main__": + try: + main() + except (OSError, RuntimeError, subprocess.SubprocessError) as error: + print(f"Verification error: {error}", file=sys.stderr) + raise SystemExit(2) from error diff --git a/verification/mainnet-registration/models/MainnetRegistration.tla b/verification/mainnet-registration/models/MainnetRegistration.tla new file mode 100644 index 0000000..8192e58 --- /dev/null +++ b/verification/mainnet-registration/models/MainnetRegistration.tla @@ -0,0 +1,102 @@ +---- MODULE MainnetRegistration ---- +EXTENDS Naturals + +CONSTANTS SaveContext, AwaitProof, MatchProof, ReadBeforePost +VARIABLES phase, gateway, saved, attempts, proof, unsafePost, duplicatePost, unsafeAssociation +vars == <> + +Init == /\ phase = "idle" + /\ gateway = "absent" + /\ saved = FALSE + /\ attempts = 0 + /\ proof = FALSE + /\ unsafePost = FALSE + /\ duplicatePost = FALSE + /\ unsafeAssociation = FALSE + +AdmitOriginalApp == /\ phase \in {"idle", "stopped"} + /\ attempts < 2 + /\ phase' = "admitted" + /\ attempts' = attempts + 1 + /\ proof' = FALSE + /\ UNCHANGED <> + +SaveIdentity == /\ phase = "admitted" + /\ phase' = "lookup" + /\ saved' = SaveContext + /\ UNCHANGED <> + +ReadGateway == /\ phase = "lookup" + /\ phase' = IF gateway # "absent" /\ (ReadBeforePost \/ attempts = 1) + THEN "confirm" ELSE "post" + /\ UNCHANGED <> + +PostGateway == /\ phase = "post" + /\ phase' = "gateway_reply" + /\ gateway' = IF gateway = "absent" THEN "pending" ELSE gateway + /\ unsafePost' = (unsafePost \/ ~saved) + /\ duplicatePost' = (duplicatePost \/ gateway # "absent") + /\ UNCHANGED <> + +ReceiveGatewayReply == /\ phase = "gateway_reply" + /\ phase' = "confirm" + /\ UNCHANGED <> + +LoseGatewayReply == /\ phase = "gateway_reply" + /\ phase' = "stopped" + /\ UNCHANGED <> + +SettleGateway(result) == /\ gateway = "pending" + /\ gateway' = result + /\ UNCHANGED <> + +ReadConfirmedProof == /\ phase = "confirm" + /\ AwaitProof + /\ (gateway = "confirmed" \/ (gateway = "mismatched" /\ ~MatchProof)) + /\ phase' = "associate" + /\ proof' = (gateway = "confirmed") + /\ UNCHANGED <> + +SkipProofRead == /\ phase = "confirm" + /\ ~AwaitProof + /\ phase' = "associate" + /\ UNCHANGED <> + +StopWaiting == /\ phase = "confirm" + /\ AwaitProof + /\ (gateway \in {"pending", "failed"} \/ (gateway = "mismatched" /\ MatchProof)) + /\ phase' = "stopped" + /\ UNCHANGED <> + +PostAssociation == /\ phase = "associate" + /\ phase' = "account_reply" + /\ unsafeAssociation' = (unsafeAssociation \/ ~proof) + /\ UNCHANGED <> + +AccountAccepts == /\ phase = "account_reply" + /\ phase' = "verify_ownership" + /\ UNCHANGED <> + +AccountUnavailable == /\ phase \in {"account_reply", "verify_ownership"} + /\ phase' = "stopped" + /\ UNCHANGED <> + +VerifyOwnershipAndFinish == /\ phase = "verify_ownership" + /\ phase' = "complete" + /\ saved' = FALSE + /\ UNCHANGED <> + +Done == /\ (phase = "complete" \/ (phase = "stopped" /\ attempts = 2)) + /\ UNCHANGED vars + +Next == AdmitOriginalApp \/ SaveIdentity \/ ReadGateway \/ PostGateway + \/ ReceiveGatewayReply \/ LoseGatewayReply + \/ (\E result \in {"confirmed", "failed", "mismatched"} : SettleGateway(result)) + \/ ReadConfirmedProof \/ SkipProofRead \/ StopWaiting \/ PostAssociation + \/ AccountAccepts \/ AccountUnavailable \/ VerifyOwnershipAndFinish \/ Done +Spec == Init /\ [][Next]_vars + +ContextSavedBeforeRegistration == ~unsafePost +NoPostForVisibleRegistration == ~duplicatePost +MatchingProofBeforeAssociation == ~unsafeAssociation +==== diff --git a/verification/mainnet-registration/models/current.cfg b/verification/mainnet-registration/models/current.cfg new file mode 100644 index 0000000..2b6edad --- /dev/null +++ b/verification/mainnet-registration/models/current.cfg @@ -0,0 +1,10 @@ +SPECIFICATION Spec +CONSTANTS + SaveContext = TRUE + AwaitProof = TRUE + MatchProof = TRUE + ReadBeforePost = TRUE +INVARIANTS + ContextSavedBeforeRegistration + NoPostForVisibleRegistration + MatchingProofBeforeAssociation diff --git a/verification/mainnet-registration/models/no-proof-identity.cfg b/verification/mainnet-registration/models/no-proof-identity.cfg new file mode 100644 index 0000000..8cb3092 --- /dev/null +++ b/verification/mainnet-registration/models/no-proof-identity.cfg @@ -0,0 +1,10 @@ +SPECIFICATION Spec +CONSTANTS + SaveContext = TRUE + AwaitProof = TRUE + MatchProof = FALSE + ReadBeforePost = TRUE +INVARIANTS + ContextSavedBeforeRegistration + NoPostForVisibleRegistration + MatchingProofBeforeAssociation diff --git a/verification/mainnet-registration/models/no-proof-wait.cfg b/verification/mainnet-registration/models/no-proof-wait.cfg new file mode 100644 index 0000000..496fff0 --- /dev/null +++ b/verification/mainnet-registration/models/no-proof-wait.cfg @@ -0,0 +1,10 @@ +SPECIFICATION Spec +CONSTANTS + SaveContext = TRUE + AwaitProof = FALSE + MatchProof = TRUE + ReadBeforePost = TRUE +INVARIANTS + ContextSavedBeforeRegistration + NoPostForVisibleRegistration + MatchingProofBeforeAssociation diff --git a/verification/mainnet-registration/models/no-save-context.cfg b/verification/mainnet-registration/models/no-save-context.cfg new file mode 100644 index 0000000..7e97ebe --- /dev/null +++ b/verification/mainnet-registration/models/no-save-context.cfg @@ -0,0 +1,10 @@ +SPECIFICATION Spec +CONSTANTS + SaveContext = FALSE + AwaitProof = TRUE + MatchProof = TRUE + ReadBeforePost = TRUE +INVARIANTS + ContextSavedBeforeRegistration + NoPostForVisibleRegistration + MatchingProofBeforeAssociation diff --git a/verification/mainnet-registration/models/repeat-visible-registration.cfg b/verification/mainnet-registration/models/repeat-visible-registration.cfg new file mode 100644 index 0000000..69b1c22 --- /dev/null +++ b/verification/mainnet-registration/models/repeat-visible-registration.cfg @@ -0,0 +1,10 @@ +SPECIFICATION Spec +CONSTANTS + SaveContext = TRUE + AwaitProof = TRUE + MatchProof = TRUE + ReadBeforePost = FALSE +INVARIANTS + ContextSavedBeforeRegistration + NoPostForVisibleRegistration + MatchingProofBeforeAssociation diff --git a/verification/mainnet-registration/models/view.mjs b/verification/mainnet-registration/models/view.mjs new file mode 100644 index 0000000..053a8ad --- /dev/null +++ b/verification/mainnet-registration/models/view.mjs @@ -0,0 +1,69 @@ +export const title = "Promote an existing app from Moksha to mainnet"; + +export function state(values) { + if (values.unsafePost) return "Submitted without a recovery journal"; + if (values.duplicatePost) return "Sent another registration"; + if (values.unsafeAssociation) + return "Asked Account before matching confirmation"; + return { + idle: "Ready to promote an owned app", + admitted: "App and Account verified", + lookup: values.saved + ? "Recovery context ready" + : "Recovery context missing", + post: + values.gateway === "absent" + ? "Mainnet record absent" + : "Visible registration bypassed", + gateway_reply: "Registration submitted", + confirm: "Waiting for mainnet confirmation", + associate: "Account association ready", + account_reply: "Waiting for Account association", + verify_ownership: "Verifying Account ownership", + stopped: values.saved + ? "Stopped with recovery context" + : "Stopped without recovery context", + complete: "App ready on mainnet", + }[values.phase]; +} + +export function step(action, from, to) { + if (action === "AdmitOriginalApp") { + return from.phase === "stopped" + ? "resume the original app" + : "choose app and production URL"; + } + if (action === "ReadGateway") { + if (to.phase === "post") { + return from.gateway === "absent" + ? "no registration found" + : "ignore the visible registration"; + } + return "use the visible registration"; + } + if (action === "StopWaiting") { + return from.gateway === "pending" + ? "confirmation times out" + : "proof fails or names another app"; + } + if (action === "ReadConfirmedProof") { + return from.gateway === "confirmed" + ? "matching confirmed proof arrives" + : "accept proof for a different owner"; + } + return { + SaveIdentity: to.saved + ? "save recovery context" + : "skip saving recovery context", + PostGateway: "submit to the gateway", + ReceiveGatewayReply: "registration reply arrives", + LoseGatewayReply: "registration reply is lost", + SettleGateway: "mainnet proof settles", + SkipProofRead: "skip the confirmation read", + PostAssociation: "ask Account to associate the app", + AccountAccepts: "Account accepts the association", + AccountUnavailable: "Account association or ownership is unconfirmed", + VerifyOwnershipAndFinish: "Account confirms ownership", + Done: "finish", + }[action]; +} diff --git a/verification/paid-read-recovery/README.md b/verification/paid-read-recovery/README.md new file mode 100644 index 0000000..73596b2 --- /dev/null +++ b/verification/paid-read-recovery/README.md @@ -0,0 +1,77 @@ +# Paid-read concurrency repair — local verification + +The repair on main serializes overlapping reads and receipt-file writes. Receipt-file updates now +hold a process-owned lock across the complete read/modify/write. Each read intent +also holds its own lock from loading recovery state through payment and response +handling. An overlapping invocation returns the existing `not_ready` outcome +(exit 6); retrying later reloads the saved header. + +All fixed model configurations pass. The real CLI/SDK/store regressions pass, +including abrupt-process recovery. Removing either new lock brings back the +corresponding failure. No live paid reads, credentials, publication or release +were used. + +## What changed + +| Owner | Protection | +| ----------------------------------------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `src/core/receipts.ts`, `nextNonce`, `saveReceipt`, `dropReceipt` | One writer owns the full file update, including reading the prior state. Temporary write, fsync, rename and directory fsync stay unchanged. A competing writer fails before loading mutable state. | +| `src/core/receipts.ts`, `withReadLock` | A receipt-key-specific lock excludes overlapping decisions/payments for the same network, grant and scope. | +| `src/cli/app/read.ts`, `runAppRead`, `runPersonalServerRead` | Load the saved receipt inside that read lock. Hold it until the read finishes or fails. Contention uses existing exit 6, without another payment attempt. | +| `src/core/receipts-lock.ts`, `acquireReceiptLock` | Publish a nonempty owner directory with atomic rename. Reclaim only a lock whose recorded process no longer exists. Invalid, inaccessible or live owners remain blocked. Unique owner filenames keep stale recovery from removing a successor. | + +Both positive regressions failed on the original implementation before repair: +competing receipt writes were admitted, and an overlapping read sent another +payment instead of returning exit 6. Their primary owner is +`test/cli/app-read-loop.test.ts`; duplicate discovery-only fixture tests were +removed. `test/core/receipts-lock.test.ts` covers unidentified owners and the +stale-reclaimer/successor race. + +The version-1 receipt schema, payment headers and central exit-code table are +unchanged. Contention fails promptly; it does not spin, wait indefinitely, retry +a failed payment or expire a live lock on a timer. + +## Formal result: updated and passing + +The invariants remain unchanged: + +- `DurableBeforeSend`: the exact payment header is retained when it is sent. +- `NoDuplicateCharge`: the simulated server cannot settle two payment identities + for one fixed read intent. +- `RejectedNeverReauthorizes`: rejection of a saved header cannot authorize a + replacement payment. + +`NoDeadlock` also passes. The model now separates read-lock acquisition, saved +state loading, write-lock acquisition, file reads, temporary writes, renames, +directory fsync and lock release. This follows the implementation rather than +treating a whole store operation as indivisible. + +| Fixed configuration | Bounds | Reached states | Result | +| ---------------------- | ------------------------------------------- | -------------- | -------------- | +| `single.cfg` | One reader, one crash/restart | 96 | All rules hold | +| `concurrent.cfg` | Two readers, no crash | 250 | All rules hold | +| `writers.cfg` | One reader plus an independent nonce writer | 219 | All rules hold | +| `concurrent-crash.cfg` | Two readers, one crash/restart | 1,654 | All rules hold | + +The independent writer case ensures that the read lock alone cannot mask the +file-update defect. The crash case releases model ownership after process death; +real-code child-process tests check that dead owner directories can be reclaimed. +No invariant was weakened and the earlier bounds were retained; the writer and +concurrent-crash cases add coverage. + +## Run + +Use Python 3.12+, the CLI's installed Node dependencies, Java and TLC 1.7.4. +Set `TLA2TOOLS` and `JAVA` for locally installed tools. + +```sh +python3 verification/paid-read-recovery/check.py --out /tmp/vana-cli-paid-read-recovery-proof +``` + +Use a fresh evidence path. The runner checks the main source at `a55d0a0006da6a743b6452796435afa6ed177dd8`. +It checks current and deliberately broken models, exercises the real code with +synthetic transport, restores the scratch source and repeats the replay. +The output directory contains the individual verdicts and replay logs. + +Use Pstack `/statechart` with the configs and view in `models/`. +The [CLI statecharts](../../docs/STATECHARTS.md) show the shorter scenarios. diff --git a/verification/paid-read-recovery/check.py b/verification/paid-read-recovery/check.py new file mode 100644 index 0000000..a39fe03 --- /dev/null +++ b/verification/paid-read-recovery/check.py @@ -0,0 +1,160 @@ +#!/usr/bin/env python3 +"""Verify the pinned paid-read code in a disposable offline snapshot.""" + +import argparse +import hashlib +import io +import json +import os +import re +from pathlib import Path +import shutil +import subprocess +import sys +import tarfile +import tempfile + +SOURCE_REVISION = "a55d0a0006da6a743b6452796435afa6ed177dd8" +OWNERS = {'src/cli/app/read.ts': '225b144bf71c658a9324c576c387a66d3144d747', 'src/core/receipts.ts': '5f3b4307207441e06d7810c751608c31cac80d0d', 'src/core/receipts-lock.ts': '5b10b659badeee27ab5252cf41d4259568e35000'} +JAR_SHA256 = "936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88" +HERE = Path(__file__).resolve().parent +REPO = HERE.parents[1] + + +def command(argv, cwd, env=None, timeout=90): + return subprocess.run( + argv, cwd=cwd, env=env, capture_output=True, text=True, timeout=timeout + ) + + +def checked(argv, cwd): + result = command(argv, cwd) + if result.returncode: + raise RuntimeError(result.stderr.strip() or result.stdout.strip()) + return result.stdout.strip() + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--ref", help="Check a committed revision instead of the working-tree patch") + parser.add_argument("--out", type=Path) + args = parser.parse_args() + revision = checked(["git", "rev-parse", args.ref or SOURCE_REVISION], REPO) + for owner, expected in OWNERS.items(): + actual = checked(["git", "rev-parse", f"{revision}:{owner}"], REPO) if args.ref else checked(["git", "hash-object", str(REPO / owner)], REPO) + if actual != expected: + raise RuntimeError( + f"Model/source drift: {owner} differs from its checked blob. " + "Review the model mapping before updating OWNERS." + ) + jar = os.environ.get("TLA2TOOLS") + if not jar: + jar = str( + Path(checked(["mise", "where", "github:tlaplus/tlaplus@1.7.4"], REPO)) + / "tla2tools.jar" + ) + if hashlib.sha256(Path(jar).read_bytes()).hexdigest() != JAR_SHA256: + raise RuntimeError("TLC jar differs from the pinned v1.7.4 SHA256") + java = os.environ.get("JAVA") or checked( + ["mise", "which", "java", "--tool", "java@temurin-25"], REPO + ) + out = args.out.resolve() if args.out else Path(tempfile.mkdtemp(prefix="paid-read-check-")) + if args.out: + out.mkdir(parents=True, exist_ok=False) + snapshot = out / "snapshot" + snapshot.mkdir() + archive = subprocess.check_output(["git", "archive", revision], cwd=REPO) + with tarfile.open(fileobj=io.BytesIO(archive)) as tar: + # The archive has an unrelated absolute fixture symlink; never follow it. + tar.extractall( + snapshot, + members=[m for m in tar.getmembers() if not (m.issym() or m.islnk())], + filter="data", + ) + if not args.ref: + for owner in OWNERS: + shutil.copy2(REPO / owner, snapshot / owner) + for owner_test in ["test/cli/app-read-loop.test.ts", "test/core/receipts-lock.test.ts"]: + shutil.copy2(REPO / owner_test, snapshot / owner_test) + (snapshot / "node_modules").symlink_to(REPO / "node_modules", target_is_directory=True) + for source in (HERE / "fixtures").iterdir(): + if source.name == "vitest.formal.config.ts": + target = snapshot / source.name + elif source.name == "no-external-io.ts": + target = snapshot / "test/setup" / source.name + else: + target = snapshot / "test/cli" / source.name + shutil.copy2(source, target) + modeldir = out / "models" + shutil.copytree(HERE / "models", modeldir) + node = shutil.which("node") + testcmd = [node, str(snapshot / "node_modules/vitest/vitest.mjs"), "run", "--config", "vitest.formal.config.ts", "--reporter=verbose"] + summary = {"revision": revision, "owners": OWNERS, "source_mode": "commit" if args.ref else "verified working-tree files", "live_reads": False, "models": {}} + for case, expected in [("single", 0), ("concurrent", 0), ("writers", 0), ("concurrent-crash", 0), ("no-save", 12), ("no-refusal", 12), ("no-read-lock", 12), ("no-write-lock", 12)]: + state_dir = out / f"tlc-{case}" + state_dir.mkdir() + result = command([ + java, "-XX:+UseParallelGC", "-cp", jar, "tlc2.TLC", + "-workers", "1", "-fp", "0", "-lncheck", "final", + "-metadir", str(state_dir), "-config", str(modeldir / f"{case}.cfg"), + str(modeldir / "PaidRead.tla"), + ], modeldir) + (out / f"{case}-tlc.log").write_text(result.stdout + result.stderr) + if result.returncode != expected: + raise RuntimeError(f"{case}: expected TLC exit {expected}, got {result.returncode}; see {out}") + summary["models"][case] = result.returncode + baseline = command(testcmd, snapshot) + (out / "baseline-tests.log").write_text(baseline.stdout + baseline.stderr) + if baseline.returncode: + raise RuntimeError(f"Real-code replay failed; inspect {out / 'baseline-tests.log'}") + originals = {owner: (snapshot / owner).read_bytes() for owner in OWNERS} + read_text = originals["src/cli/app/read.ts"].decode() + store_text = originals["src/core/receipts.ts"].decode() + save_pattern = r"receipts\.saveReceipt\(storedKey, \{.*?\n\s*\}\);" + if len(re.findall(save_pattern, read_text, re.S)) != 1 or read_text.count("if (stored) {") != 1: + raise RuntimeError("Mutation anchors drifted; review the source") + write_lock = 'const release = acquireReceiptLock(`${file}.lock`);' + read_lock = 'const release = acquireReceiptLock(`${file}.${intent}.read.lock`);' + if store_text.count(write_lock) != 1 or store_text.count(read_lock) != 1: + raise RuntimeError("Lock mutation anchors drifted; review the source") + summary["mutations"] = {} + try: + for name, owner, mutated, selected in [ + ("no-save", "src/cli/app/read.ts", re.sub(save_pattern, "void paymentQuote;", read_text, flags=re.S), "retains a paid read's exact header"), + ("no-refusal", "src/cli/app/read.ts", read_text.replace("if (stored) {", "if (false) {"), "refuses a new payment after a saved receipt"), + ("no-read-lock", "src/core/receipts.ts", store_text.replace(read_lock, "const release = () => {};"), "refuses an overlapping read"), + ("no-write-lock", "src/core/receipts.ts", store_text.replace(write_lock, "const release = () => {};"), "refuses a competing write"), + ]: + source = snapshot / owner + source.write_text(mutated) + result = command(testcmd + ["test/cli/app-read-loop.test.ts", "-t", selected], snapshot) + (out / f"mutation-{name}.log").write_text(result.stdout + result.stderr) + source.write_bytes(originals[owner]) + if result.returncode != 1 or "AssertionError" not in result.stdout + result.stderr: + raise RuntimeError(f"{name}: expected a behavioral assertion failure; inspect {out}") + summary["mutations"][name] = "caught by real-code assertion" + finally: + for owner, original in originals.items(): + (snapshot / owner).write_bytes(original) + restored = command(testcmd, snapshot) + (out / "restored-tests.log").write_text(restored.stdout + restored.stderr) + if restored.returncode: + raise RuntimeError(f"Restored baseline failed; inspect {out}") + for owner, blob in OWNERS.items(): + actual = checked(["git", "hash-object", str(snapshot / owner)], REPO) + if actual != blob: + raise RuntimeError(f"Scratch source was not restored: {owner}") + summary["product_snapshot_restored"] = True + summary["status"] = "passed: recovery, overlapping reads and independent state writes" + (out / "summary.json").write_text(json.dumps(summary, indent=2) + "\n") + print(json.dumps({"status": summary["status"], "evidence": str(out)}, indent=2)) + return 0 + + +if __name__ == "__main__": + try: + result = main() + except Exception as error: + print(f"Verification error: {error}", file=sys.stderr) + raise SystemExit(2) from error + raise SystemExit(result) diff --git a/verification/paid-read-recovery/fixtures/no-external-io.ts b/verification/paid-read-recovery/fixtures/no-external-io.ts new file mode 100644 index 0000000..ad91a47 --- /dev/null +++ b/verification/paid-read-recovery/fixtures/no-external-io.ts @@ -0,0 +1,6 @@ +import { beforeEach, vi } from "vitest"; +beforeEach(() => { + vi.stubGlobal("fetch", async () => { + throw new Error("External network disabled for formal verification"); + }); +}); diff --git a/verification/paid-read-recovery/fixtures/paid-read-crash-driver.ts b/verification/paid-read-recovery/fixtures/paid-read-crash-driver.ts new file mode 100644 index 0000000..860a56e --- /dev/null +++ b/verification/paid-read-recovery/fixtures/paid-read-crash-driver.ts @@ -0,0 +1,99 @@ +import fs from "node:fs"; +import path from "node:path"; +import { createHash } from "node:crypto"; +import { privateKeyToAccount } from "viem/accounts"; +import { readPersonalServerData } from "@opendatalabs/vana-sdk/direct/personal-server-read"; +import { runAppRead } from "../../src/cli/app/read.js"; +import { createReceiptsStore } from "../../src/core/receipts.js"; +import { createRequestsStore } from "../../src/core/requests-store.js"; + +const [root, stage] = process.argv.slice(2); +const key = + "0x59c6995e998f97a5a0044966f0945389dc9e86dae88c7a8412f4603b6b78690d"; +const account = privateKeyToAccount(key); +const grant = `0x${"1".repeat(64)}`; +const scope = "github.repos"; +const file = path.join(root, "receipts.json"); +const ledgerFile = path.join(root, "fixture-ledger.json"); +const receipts = createReceiptsStore(file); +let inReceipt = false; +const rename = fs.renameSync; +fs.renameSync = (...args) => { + if (inReceipt && stage === "before-receipt-rename" && args[1] === file) + process.exit(86); + return Reflect.apply(rename, fs, args); +}; +const writeLedger = (ledger) => + fs.writeFileSync(ledgerFile, JSON.stringify(ledger)); +const loadLedger = () => + fs.existsSync(ledgerFile) + ? JSON.parse(fs.readFileSync(ledgerFile, "utf8")) + : { sent: [], pending: [], settled: [] }; +globalThis.fetch = async (input, init) => { + if (!String(input).startsWith("https://fixture.invalid/")) + throw new Error("External I/O disabled"); + const header = new Headers(init?.headers).get("X-PAYMENT"); + if (!header) + return Response.json({ grantId: grant, amount: "1" }, { status: 402 }); + const identity = createHash("sha256").update(header).digest("hex"); + const ledger = loadLedger(); + ledger.sent.push(identity); + ledger.pending = [...new Set([...ledger.pending, identity])]; + writeLedger(ledger); + if (stage === "after-send") process.exit(86); + if (stage === "hold-read") { + process.send?.("payment-pending"); + await new Promise(() => {}); + } + ledger.settled = [...new Set([...ledger.settled, ...ledger.pending])]; + ledger.pending = []; + writeLedger(ledger); + if (stage === "after-settlement") process.exit(86); + return Response.json({ rows: ["synthetic"] }); +}; +process.env.VANA_ENV = "dev"; +const exit = await runAppRead( + scope, + { + json: true, + grant, + network: "moksha", + server: "https://fixture.invalid", + pay: true, + }, + { + resolveKey: () => ({ + privateKey: key, + address: account.address, + publicKey: account.publicKey, + source: "env", + }), + createClient: () => ({ + getGrant: async () => ({ + id: grant, + grantorAddress: `0x${"2".repeat(40)}`, + scopes: [scope], + status: "active", + expiresAt: null, + }), + }), + requests: createRequestsStore(path.join(root, "requests.json")), + receipts: { + ...receipts, + nextNonce(payer) { + const n = receipts.nextNonce(payer); + if (stage === "after-nonce") process.exit(86); + return n; + }, + saveReceipt(k, receipt) { + inReceipt = true; + receipts.saveReceipt(k, receipt); + inReceipt = false; + if (stage === "after-receipt") process.exit(86); + }, + }, + read: (params) => + readPersonalServerData({ ...params, transportRetry: { attempts: 1 } }), + }, +); +process.exitCode = exit; diff --git a/verification/paid-read-recovery/fixtures/paid-read-process.test.ts b/verification/paid-read-recovery/fixtures/paid-read-process.test.ts new file mode 100644 index 0000000..b2800d5 --- /dev/null +++ b/verification/paid-read-recovery/fixtures/paid-read-process.test.ts @@ -0,0 +1,118 @@ +import fs from "node:fs"; +import os from "node:os"; +import path from "node:path"; +import { spawn, spawnSync } from "node:child_process"; +import { buildSync } from "esbuild"; +import { afterAll, beforeAll, expect, it } from "vitest"; +let buildDir: string; +let driver: string; +beforeAll(() => { + buildDir = fs.mkdtempSync(path.join(process.cwd(), ".paid-read-driver-")); + driver = path.join(buildDir, "driver.mjs"); + buildSync({ + entryPoints: ["test/cli/paid-read-crash-driver.ts"], + outfile: driver, + platform: "node", + format: "esm", + bundle: true, + packages: "external", + logLevel: "silent", + }); +}); +afterAll(() => fs.rmSync(buildDir, { recursive: true, force: true })); +it.each([ + "after-nonce", + "before-receipt-rename", + "after-receipt", + "after-send", + "after-settlement", +])("restarts an abruptly terminated process at %s", (stage) => { + const root = fs.mkdtempSync(path.join(os.tmpdir(), "paid-read-process-")); + const env = { + ...process.env, + HOME: root, + USERPROFILE: root, + VANA_HOME: root, + }; + try { + const first = spawnSync(process.execPath, [driver, root, stage], { + env, + encoding: "utf8", + timeout: 10000, + }); + expect(first.status, first.stderr).toBe(86); + const second = spawnSync(process.execPath, [driver, root, "resume"], { + env, + encoding: "utf8", + timeout: 10000, + }); + expect(second.status, second.stderr).toBe(0); + const ledger = JSON.parse( + fs.readFileSync(path.join(root, "fixture-ledger.json"), "utf8"), + ); + expect(ledger.settled).toHaveLength(1); + expect(new Set(ledger.sent).size).toBe(1); + expect(ledger.pending).toEqual([]); + } finally { + fs.rmSync(root, { recursive: true, force: true }); + } +}); + +it("blocks another process, then recovers the killed owner's exact payment", async () => { + const root = fs.mkdtempSync(path.join(os.tmpdir(), "paid-read-process-")); + const env = { + ...process.env, + HOME: root, + USERPROFILE: root, + VANA_HOME: root, + }; + const child = spawn(process.execPath, [driver, root, "hold-read"], { + env, + stdio: ["ignore", "ignore", "pipe", "ipc"], + }); + const exited = new Promise((resolve) => + child.once("exit", () => resolve()), + ); + let errors = ""; + child.stderr?.on("data", (data) => { + errors += String(data); + }); + try { + await new Promise((resolve, reject) => { + child.once("message", (message) => + message === "payment-pending" + ? resolve() + : reject(new Error("Unexpected fixture checkpoint")), + ); + child.once("error", reject); + child.once("exit", () => + reject(new Error(`Fixture exited before checkpoint: ${errors}`)), + ); + }); + const overlap = spawnSync(process.execPath, [driver, root, "resume"], { + env, + encoding: "utf8", + timeout: 10000, + }); + expect(overlap.status, overlap.stderr).toBe(6); + expect(JSON.parse(overlap.stdout).code).toBe("not_ready"); + child.kill("SIGKILL"); + await exited; + const retry = spawnSync(process.execPath, [driver, root, "resume"], { + env, + encoding: "utf8", + timeout: 10000, + }); + expect(retry.status, retry.stderr).toBe(0); + const ledger = JSON.parse( + fs.readFileSync(path.join(root, "fixture-ledger.json"), "utf8"), + ); + expect(new Set(ledger.sent).size).toBe(1); + expect(ledger.settled).toHaveLength(1); + } finally { + if (child.exitCode === null && child.signalCode === null) + child.kill("SIGKILL"); + await exited; + fs.rmSync(root, { recursive: true, force: true }); + } +}); diff --git a/verification/paid-read-recovery/fixtures/vitest.formal.config.ts b/verification/paid-read-recovery/fixtures/vitest.formal.config.ts new file mode 100644 index 0000000..c80deed --- /dev/null +++ b/verification/paid-read-recovery/fixtures/vitest.formal.config.ts @@ -0,0 +1,12 @@ +import { defineConfig } from "vitest/config"; +export default defineConfig({ + test: { + globals: true, + include: [ + "test/cli/paid-read-process.test.ts", + "test/cli/app-read-loop.test.ts", + "test/core/receipts-lock.test.ts", + ], + setupFiles: ["test/setup/isolate-home.ts", "test/setup/no-external-io.ts"], + }, +}); diff --git a/verification/paid-read-recovery/models/PaidRead.tla b/verification/paid-read-recovery/models/PaidRead.tla new file mode 100644 index 0000000..9c32e08 --- /dev/null +++ b/verification/paid-read-recovery/models/PaidRead.tla @@ -0,0 +1,144 @@ +---------------------------- MODULE PaidRead ---------------------------- +EXTENDS Naturals, FiniteSets, TLC +CONSTANTS Readers, Restarts, SaveBeforeSend, RefuseRejected, SerializeReads, SerializeWrites, CounterWriter +VARIABLES phase, loaded, header, snapshot, disk, pending, charged, + crashes, unsafeSend, reauthorized, rejected, readOwner, writeOwner +vars == <> +Clients == 1..Readers +Counter == IF CounterWriter THEN Readers + 1 ELSE 0 +Workers == 1..(Readers + IF CounterWriter THEN 1 ELSE 0) +Empty == [nonce |-> 0, receipt |-> 0] +Init == /\ phase = [w \in Workers |-> IF w = Counter THEN "NonceRead" ELSE "Open"] + /\ loaded = [w \in Workers |-> 0] + /\ header = [w \in Workers |-> 0] + /\ snapshot = [w \in Workers |-> Empty] + /\ disk = Empty /\ pending = {} /\ charged = {} + /\ readOwner = 0 /\ writeOwner = 0 + /\ crashes = 0 /\ unsafeSend = FALSE + /\ reauthorized = FALSE /\ rejected = [w \in Workers |-> FALSE] +AcquireRead(w) == /\ phase[w] = "Open" + /\ (~SerializeReads \/ readOwner = 0) + /\ readOwner' = IF SerializeReads THEN w ELSE readOwner + /\ phase' = [phase EXCEPT ![w] = "ReadState"] + /\ UNCHANGED <> +ReadBusy(w) == /\ phase[w] = "Open" /\ SerializeReads /\ readOwner # 0 + /\ phase' = [phase EXCEPT ![w] = "Busy"] + /\ UNCHANGED <> +Open(w) == /\ phase[w] = "ReadState" + /\ loaded' = [loaded EXCEPT ![w] = disk.receipt] + /\ header' = [header EXCEPT ![w] = disk.receipt] + /\ phase' = [phase EXCEPT ![w] = "Probe"] + /\ UNCHANGED <> +Challenge(w) == /\ phase[w] = "Probe" /\ loaded[w] = 0 + /\ phase' = [phase EXCEPT ![w] = "NonceRead"] + /\ UNCHANGED <> +Replay(w) == /\ phase[w] = "Probe" /\ loaded[w] # 0 + /\ phase' = [phase EXCEPT ![w] = "Ready"] + /\ UNCHANGED <> +AcquireWrite(w) == /\ phase[w] \in {"NonceRead", "ReceiptRead"} + /\ (~SerializeWrites \/ writeOwner = 0) + /\ writeOwner' = IF SerializeWrites THEN w ELSE writeOwner + /\ phase' = [phase EXCEPT ![w] = IF @ = "NonceRead" THEN "NonceLoad" ELSE "ReceiptLoad"] + /\ UNCHANGED <> +WriteBusy(w) == /\ phase[w] \in {"NonceRead", "ReceiptRead"} + /\ SerializeWrites /\ writeOwner # 0 + /\ phase' = [phase EXCEPT ![w] = "Blocked"] + /\ UNCHANGED <> +ReadNonce(w) == /\ phase[w] = "NonceLoad" + /\ snapshot' = [snapshot EXCEPT ![w] = disk] + /\ phase' = [phase EXCEPT ![w] = "NonceTemp"] + /\ UNCHANGED <> +SyncNonceTemp(w) == /\ phase[w] = "NonceTemp" + /\ phase' = [phase EXCEPT ![w] = "NonceRename"] + /\ UNCHANGED <> +CommitNonce(w) == /\ phase[w] = "NonceRename" + /\ disk' = [snapshot[w] EXCEPT !.nonce = @ + 1] + /\ header' = [header EXCEPT ![w] = snapshot[w].nonce + 1] + /\ phase' = [phase EXCEPT ![w] = "NonceSync"] + /\ UNCHANGED <> +SyncNonceDirectory(w) == /\ phase[w] = "NonceSync" + /\ phase' = [phase EXCEPT ![w] = IF w = Counter THEN "Done" ELSE IF SaveBeforeSend THEN "ReceiptRead" ELSE "Ready"] + /\ reauthorized' = (reauthorized \/ rejected[w]) + /\ writeOwner' = 0 + /\ UNCHANGED <> +ReadReceipt(w) == /\ phase[w] = "ReceiptLoad" + /\ snapshot' = [snapshot EXCEPT ![w] = disk] + /\ phase' = [phase EXCEPT ![w] = "ReceiptTemp"] + /\ UNCHANGED <> +SyncReceiptTemp(w) == /\ phase[w] = "ReceiptTemp" + /\ phase' = [phase EXCEPT ![w] = "ReceiptRename"] + /\ UNCHANGED <> +CommitReceipt(w) == /\ phase[w] = "ReceiptRename" + /\ disk' = [snapshot[w] EXCEPT !.receipt = header[w]] + /\ phase' = [phase EXCEPT ![w] = "ReceiptSync"] + /\ UNCHANGED <> +SyncReceiptDirectory(w) == /\ phase[w] = "ReceiptSync" + /\ phase' = [phase EXCEPT ![w] = "Ready"] + /\ writeOwner' = 0 + /\ UNCHANGED <> +Send(w) == /\ phase[w] = "Ready" + /\ pending' = pending \cup {header[w]} + /\ unsafeSend' = (unsafeSend \/ disk.receipt # header[w]) + /\ phase' = [phase EXCEPT ![w] = "Waiting"] + /\ UNCHANGED <> +Settle(h) == /\ h \in pending /\ charged' = charged \cup {h} + /\ pending' = pending \ {h} + /\ UNCHANGED <> +Receive(w) == /\ phase[w] = "Waiting" /\ header[w] \in charged + /\ phase' = [phase EXCEPT ![w] = "Done"] + /\ UNCHANGED <> +RejectSaved(w) == /\ phase[w] = "Probe" /\ loaded[w] # 0 + /\ rejected' = [rejected EXCEPT ![w] = TRUE] + /\ phase' = [phase EXCEPT ![w] = IF RefuseRejected THEN "Blocked" ELSE "NonceRead"] + /\ UNCHANGED <> +StoreFails(w) == /\ phase[w] \in {"NonceTemp", "NonceRename", "NonceSync", "ReceiptTemp", "ReceiptRename", "ReceiptSync"} + /\ phase' = [phase EXCEPT ![w] = "Blocked"] + /\ writeOwner' = IF writeOwner = w THEN 0 ELSE writeOwner + /\ readOwner' = IF readOwner = w THEN 0 ELSE readOwner + /\ UNCHANGED <> +CrashAndRestart(w) == /\ w \in Clients /\ crashes < Restarts /\ phase[w] # "Done" + /\ phase' = [phase EXCEPT ![w] = "Open"] + /\ loaded' = [loaded EXCEPT ![w] = 0] + /\ header' = [header EXCEPT ![w] = 0] + /\ crashes' = crashes + 1 + /\ writeOwner' = IF writeOwner = w THEN 0 ELSE writeOwner + /\ readOwner' = IF readOwner = w THEN 0 ELSE readOwner + /\ UNCHANGED <> +ReleaseRead(w) == /\ phase[w] \in {"Done", "Blocked", "Busy"} /\ readOwner = w + /\ readOwner' = 0 + /\ UNCHANGED <> +Finished == /\ \A w \in Workers : phase[w] \in {"Done", "Blocked", "Busy"} + /\ pending = {} /\ readOwner = 0 /\ writeOwner = 0 /\ UNCHANGED vars +Next == (\E w \in Workers : AcquireRead(w) \/ ReadBusy(w) \/ Open(w) \/ AcquireWrite(w) \/ WriteBusy(w) \/ ReleaseRead(w) \/ Challenge(w) \/ Replay(w) \/ ReadNonce(w) + \/ SyncNonceTemp(w) \/ CommitNonce(w) \/ SyncNonceDirectory(w) + \/ ReadReceipt(w) \/ SyncReceiptTemp(w) \/ CommitReceipt(w) + \/ SyncReceiptDirectory(w) \/ Send(w) \/ Receive(w) \/ RejectSaved(w) + \/ StoreFails(w) \/ CrashAndRestart(w)) \/ (\E h \in pending : Settle(h)) \/ Finished +Spec == Init /\ [][Next]_vars +DurableBeforeSend == ~unsafeSend +NoDuplicateCharge == Cardinality(charged) <= 1 +RejectedNeverReauthorizes == ~reauthorized +============================================================================= diff --git a/verification/paid-read-recovery/models/concurrent-crash.cfg b/verification/paid-read-recovery/models/concurrent-crash.cfg new file mode 100644 index 0000000..790d9f7 --- /dev/null +++ b/verification/paid-read-recovery/models/concurrent-crash.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +CONSTANTS Readers = 2 Restarts = 1 SaveBeforeSend = TRUE RefuseRejected = TRUE SerializeReads = TRUE SerializeWrites = TRUE CounterWriter = FALSE +INVARIANTS DurableBeforeSend NoDuplicateCharge RejectedNeverReauthorizes diff --git a/verification/paid-read-recovery/models/concurrent.cfg b/verification/paid-read-recovery/models/concurrent.cfg new file mode 100644 index 0000000..8cadac5 --- /dev/null +++ b/verification/paid-read-recovery/models/concurrent.cfg @@ -0,0 +1,5 @@ +SPECIFICATION Spec +CONSTANTS Readers = 2 Restarts = 0 SaveBeforeSend = TRUE RefuseRejected = TRUE +INVARIANTS DurableBeforeSend NoDuplicateCharge RejectedNeverReauthorizes + +CONSTANTS SerializeReads = TRUE SerializeWrites = TRUE CounterWriter = FALSE diff --git a/verification/paid-read-recovery/models/no-read-lock.cfg b/verification/paid-read-recovery/models/no-read-lock.cfg new file mode 100644 index 0000000..4bbeea7 --- /dev/null +++ b/verification/paid-read-recovery/models/no-read-lock.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +CONSTANTS Readers = 2 Restarts = 0 SaveBeforeSend = TRUE RefuseRejected = TRUE SerializeReads = FALSE SerializeWrites = TRUE CounterWriter = FALSE +INVARIANTS DurableBeforeSend NoDuplicateCharge RejectedNeverReauthorizes diff --git a/verification/paid-read-recovery/models/no-refusal.cfg b/verification/paid-read-recovery/models/no-refusal.cfg new file mode 100644 index 0000000..cf15d13 --- /dev/null +++ b/verification/paid-read-recovery/models/no-refusal.cfg @@ -0,0 +1,5 @@ +SPECIFICATION Spec +CONSTANTS Readers = 1 Restarts = 1 SaveBeforeSend = TRUE RefuseRejected = FALSE +INVARIANTS DurableBeforeSend NoDuplicateCharge RejectedNeverReauthorizes + +CONSTANTS SerializeReads = TRUE SerializeWrites = TRUE CounterWriter = FALSE diff --git a/verification/paid-read-recovery/models/no-save.cfg b/verification/paid-read-recovery/models/no-save.cfg new file mode 100644 index 0000000..ab4f2ae --- /dev/null +++ b/verification/paid-read-recovery/models/no-save.cfg @@ -0,0 +1,5 @@ +SPECIFICATION Spec +CONSTANTS Readers = 1 Restarts = 1 SaveBeforeSend = FALSE RefuseRejected = TRUE +INVARIANTS DurableBeforeSend NoDuplicateCharge RejectedNeverReauthorizes + +CONSTANTS SerializeReads = TRUE SerializeWrites = TRUE CounterWriter = FALSE diff --git a/verification/paid-read-recovery/models/no-write-lock.cfg b/verification/paid-read-recovery/models/no-write-lock.cfg new file mode 100644 index 0000000..c0b957c --- /dev/null +++ b/verification/paid-read-recovery/models/no-write-lock.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +CONSTANTS Readers = 1 Restarts = 0 SaveBeforeSend = TRUE RefuseRejected = TRUE SerializeReads = TRUE SerializeWrites = FALSE CounterWriter = TRUE +INVARIANTS DurableBeforeSend NoDuplicateCharge RejectedNeverReauthorizes diff --git a/verification/paid-read-recovery/models/overview.mjs b/verification/paid-read-recovery/models/overview.mjs new file mode 100644 index 0000000..12a3af7 --- /dev/null +++ b/verification/paid-read-recovery/models/overview.mjs @@ -0,0 +1,76 @@ +export const title = "Paid-read recovery: one reader and overlapping readers"; +export const state = (v) => { + const broken = [ + v.unsafeSend && "Saved receipt erased", + v.charged.length > 1 && "Two fees possible", + v.reauthorized && "Rejected receipt replaced", + ] + .filter(Boolean) + .join(" + "); + if (Object.keys(v.phase).length > 1) { + if (v.phase[1] === "Busy" || v.phase[2] === "Busy") + return "Overlapping read stopped; retry reloads receipt"; + if (v.unsafeSend || v.charged.length > 1 || v.reauthorized) return broken; + if (v.charged.length) + return "One payment settled; recovery receipt retained"; + if (Object.values(v.phase).includes("Waiting")) + return "One payment sent; receipt retained"; + if (v.disk.receipt) return "Payment receipt saved"; + if (v.writeOwner) return "One writer updating payment state"; + if (v.readOwner) return "One reader holds the payment decision"; + return "Readers ready; payment locks available"; + } + const labels = { + Open: "Start or restart", + ReadState: "Read lock held; loading saved receipt", + Busy: "Read already running; retry later", + NonceLoad: "Preparing payment", + ReceiptLoad: "Saving recovery receipt", + Probe: v.loaded[1] + ? "Retrying saved payment" + : "Checking whether payment is needed", + NonceRead: "Preparing payment", + NonceTemp: "Preparing payment", + NonceRename: "Preparing payment", + NonceSync: "Preparing payment", + ReceiptRead: "Saving recovery receipt", + ReceiptTemp: "Saving recovery receipt", + ReceiptRename: "Saving recovery receipt", + ReceiptSync: "Saving recovery receipt", + Ready: "Ready to send", + Waiting: v.charged.length ? "Charged; waiting for data" : "Payment sent", + Done: "Data received", + Blocked: "Stopped for repair", + }; + return `${broken ? broken + ": " : ""}${labels[v.phase[1]]}`; +}; +export const step = (action, from, to) => { + if (action === "AcquireRead") return "you reserve this read intent"; + if (action === "ReadBusy") return "another read returns not ready"; + if (action === "WriteBusy") return "a competing write returns not ready"; + if (action === "AcquireWrite") return "you reserve the payment state file"; + if (action === "ReleaseRead") return "you release the read intent"; + if (action === "SyncNonceDirectory") + return "you finish preparing the payment"; + if (action === "SyncReceiptDirectory") return "the recovery receipt is saved"; + if (action === "CommitNonce") + return from.disk.receipt !== to.disk.receipt + ? "a stale counter write erases the saved receipt" + : "the payment counter is committed"; + if (action === "CommitReceipt") return "the payment receipt is committed"; + if (action === "Send") return "you send the signed payment"; + if (from.charged.length !== to.charged.length) + return "the fixture settles a distinct payment"; + return ( + { + Open: "you open the saved payment state", + Challenge: "the server requests payment", + Replay: "you reuse the same saved header", + Receive: "the data arrives", + RejectSaved: "the server rejects the saved receipt", + StoreFails: "saving payment state fails", + CrashAndRestart: "the CLI closes and you restart", + ReadNonce: "you start preparing a new payment", + }[action] ?? "you continue the local write" + ); +}; diff --git a/verification/paid-read-recovery/models/single.cfg b/verification/paid-read-recovery/models/single.cfg new file mode 100644 index 0000000..8c04c74 --- /dev/null +++ b/verification/paid-read-recovery/models/single.cfg @@ -0,0 +1,5 @@ +SPECIFICATION Spec +CONSTANTS Readers = 1 Restarts = 1 SaveBeforeSend = TRUE RefuseRejected = TRUE +INVARIANTS DurableBeforeSend NoDuplicateCharge RejectedNeverReauthorizes + +CONSTANTS SerializeReads = TRUE SerializeWrites = TRUE CounterWriter = FALSE diff --git a/verification/paid-read-recovery/models/writers.cfg b/verification/paid-read-recovery/models/writers.cfg new file mode 100644 index 0000000..8743603 --- /dev/null +++ b/verification/paid-read-recovery/models/writers.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +CONSTANTS Readers = 1 Restarts = 0 SaveBeforeSend = TRUE RefuseRejected = TRUE SerializeReads = TRUE SerializeWrites = TRUE CounterWriter = TRUE +INVARIANTS DurableBeforeSend NoDuplicateCharge RejectedNeverReauthorizes diff --git a/verification/server-supervision/README.md b/verification/server-supervision/README.md new file mode 100644 index 0000000..bdfde1f --- /dev/null +++ b/verification/server-supervision/README.md @@ -0,0 +1,36 @@ +# Local Personal Server supervision + +When Stop arrives before a replacement process starts, the supervisor must +keep it from launching. Otherwise `vana server stop` can be followed by +`server-restarted` before the supervisor stops the replacement. + +| Model action | CLI source | +| --------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------ | +| `ServerExits` | `runServerStart` receives the running child's exit and stops that handle before backoff. | +| `RequestStop` | `stopRequested` settles and records `stopping` in the supervisor. The data directory remains locked. | +| `EndWait` | The restart sleep races Stop. The branch returns success and emits `server-stopped` when Stop wins. | +| `PortAvailable` | Restart awaits `choosePort` and may try a second port. On a usable port, it calls `launch` without rechecking Stop. | +| `ServerReady`, `StopServer` | The replacement supplies credentials and emits `server-restarted`. The next loop observes Stop, stops the new handle and emits `server-stopped`. | + +TLC explores one foreground server, one unexpected exit, one restart wait, +one successful port probe, one replacement launch and one stop request. It +starts after initial readiness. An already invoked launch may finish after +Stop. The invariant concerns a new launch invoked after Stop. Runtime install, +the detached child handshake, registration, tunnels, actual OS signal delivery, +multiple restarts and a failed port probe are outside this model. + +## Read the current finding + +`NoLaunchAfterStop` breaks. A server exits, the backoff ends, Stop arrives +while the replacement's port probe is pending, and the usable result starts a +replacement. The command replay holds the real `runServerStart` restart +workflow at that exact dependency boundary. The injected transport observes +`server-restarted` before `server-stopped`. The first server and replacement +are controlled handles. No OS process, provider, browser or tunnel is started. + +The existing backoff guard holds. The checker removes it in scratch and +requires the wait replay to observe an unwanted restart. The checker also +tries a scratch guard immediately after the port probe, before any launch. +That variation passes the port-probe replay. The checker restores all source +bytes and repeats both baseline outcomes. The guarded replay also checks that the start port received no second call. +The scratch guard isolates the counterexample's cause. It is outside the delivered runtime source. diff --git a/verification/server-supervision/check.py b/verification/server-supervision/check.py new file mode 100644 index 0000000..cfd4aeb --- /dev/null +++ b/verification/server-supervision/check.py @@ -0,0 +1,156 @@ +#!/usr/bin/env python3 +"""Check a stopped server's restart boundary in a disposable source snapshot.""" + +import argparse +import hashlib +import json +import os +from pathlib import Path +import shutil +import subprocess +import tarfile +import tempfile + +HERE = Path(__file__).resolve().parent +REPO = HERE.parents[1] +REVISION = "a55d0a0006da6a743b6452796435afa6ed177dd8" +SOURCE = "src/cli/server-start.ts" +TEST = "test/personal-server/server-start.test.ts" +BLOBS = { + SOURCE: "55fc49d9f7e9d5b543ed6761a7c2eb283d0535b2", + TEST: "af5ff6c4d65028349bf295bb485c9408a24d3c1b", +} +TLC_HASH = "936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88" +MODEL_CASES = { + "current": "NoLaunchAfterStop", + "backoff": None, + "no-backoff-fence": "BackoffStopPreventsLaunch", + "port-fence": None, +} + + +def run(args, cwd=REPO): + return subprocess.run( + args, cwd=cwd, text=True, stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, timeout=90, + ) + + +def output(args): + result = run(args) + if result.returncode: + raise RuntimeError(result.stdout) + return result.stdout.strip() + + +def run_model(out, models, java, jar, case, violation): + result = run([ + java, "-Xmx768m", "-XX:+UseParallelGC", "-cp", jar, "tlc2.TLC", + "-workers", "1", "-config", f"{case}.cfg", "-metadir", + str(out / f"{case}-states"), "ServerSupervision.tla", + ], models) + (out / f"{case}-tlc.log").write_text(result.stdout) + expected = f"Invariant {violation} is violated" if violation else "Model checking completed. No error has been found" + if result.returncode != (12 if violation else 0) or expected not in result.stdout: + raise RuntimeError(f"{case}: wrong model verdict. See {out}") + return {"case": case, "violation": violation} + + +def replace_once(text, before, after): + if text.count(before) != 1: + raise RuntimeError("Scratch replay anchor has drifted") + return text.replace(before, after) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--out", required=True, type=Path) + args = parser.parse_args() + out = args.out.resolve() + for file, blob in BLOBS.items(): + if output(["git", "hash-object", str(REPO / file)]) != blob: + raise RuntimeError(f"Source drift: {file}. Reconcile the model first.") + java = os.environ.get("JAVA") or output(["mise", "which", "java", "--tool", "java@temurin-25"]) + jar = os.environ.get("TLA2TOOLS") or str( + Path(output(["mise", "where", "github:tlaplus/tlaplus@1.7.4"])) / "tla2tools.jar" + ) + if hashlib.sha256(Path(jar).read_bytes()).hexdigest() != TLC_HASH: + raise RuntimeError("TLC jar does not match the pinned 1.7.4 checksum") + vitest = REPO / "node_modules/vitest/vitest.mjs" + if not vitest.is_file(): + raise RuntimeError("The installed CLI Vitest is required") + out.mkdir() + models = out / "models" + shutil.copytree(HERE / "models", models) + results = [run_model(out, models, java, jar, case, expected) for case, expected in MODEL_CASES.items()] + + with tempfile.TemporaryDirectory(prefix="vana-server-supervision-") as tmp: + snapshot = Path(tmp) + archive = snapshot / "source.tar" + with archive.open("wb") as handle: + subprocess.run(["git", "archive", REVISION], cwd=REPO, stdout=handle, check=True) + with tarfile.open(archive) as handle: + handle.extractall(snapshot, members=[ + member for member in handle.getmembers() if member.isfile() or member.isdir() + ], filter="data") + archive.unlink() + (snapshot / "node_modules").symlink_to(REPO / "node_modules", target_is_directory=True) + replay = (HERE / "fixtures/stop-replay.txt").read_text() + test = snapshot / TEST + anchor = ' it("backs off and gives up on a server that keeps crashing",' + test.write_text(replace_once(test.read_text(), anchor, replay + anchor)) + source = snapshot / SOURCE + original = source.read_text() + guard = ''' if (waited === "stopped" || stopping) { + io.say("Stopped."); + io.event({ type: "server-stopped" }); + return CliExitCode.OK; + } +''' + port_anchor = " if (!port) {\n" + fixed = replace_once(original, port_anchor, guard.replace('waited === "stopped" || stopping', "stopping") + port_anchor) + mutant = replace_once(original, guard, "") + + def check_replay(name, stage, expected_failure=False): + result = run([ + "node", str(vitest), "run", TEST, "--reporter=verbose", + "-t", f"does not launch a replacement after Stop during the {stage}", + ], snapshot) + (out / f"{name}-replay.log").write_text(result.stdout) + expected = ( + "to not include 'server-restarted'" if expected_failure + else "1 passed" + ) + if result.returncode != int(expected_failure) or expected not in result.stdout: + raise RuntimeError(f"{name}: wrong replay verdict. See {out}") + return {"replay": name, "failure_reproduced": expected_failure} + + replays = [ + check_replay("baseline-backoff", "restart wait"), + check_replay("baseline-port", "port probe", True), + ] + try: + source.write_text(mutant) + replays.append(check_replay("removed-backoff-fence", "restart wait", True)) + source.write_text(fixed) + replays.append(check_replay("added-port-fence", "port probe")) + finally: + source.write_text(original) + replays += [ + check_replay("restored-backoff", "restart wait"), + check_replay("restored-port", "port probe", True), + ] + if output(["git", "hash-object", str(source)]) != BLOBS[SOURCE]: + raise RuntimeError("Scratch source was not restored") + (out / "summary.json").write_text(json.dumps({ + "source_revision": REVISION, + "expected_outcomes_observed": True, + "known_finding": "NoLaunchAfterStop", + "models": results, + "replays": replays, + }, indent=2) + "\n") + print(f"Expected verdicts observed. Current port-probe restart finding reproduced. {out}") + + +if __name__ == "__main__": + main() diff --git a/verification/server-supervision/fixtures/stop-replay.txt b/verification/server-supervision/fixtures/stop-replay.txt new file mode 100644 index 0000000..2d5a3ad --- /dev/null +++ b/verification/server-supervision/fixtures/stop-replay.txt @@ -0,0 +1,42 @@ + it.each(["restart wait", "port probe"])( + "does not launch a replacement after Stop during the %s", + async (when) => { + const first = crashingServer(); + const replacement = crashingServer(); + const stop = Promise.withResolvers(); + const waiting = Promise.withResolvers(); + const probing = Promise.withResolvers(); + const port = Promise.withResolvers(); + const h = harness({ + start: vi + .fn() + .mockResolvedValueOnce(first.handle) + .mockResolvedValueOnce(replacement.handle), + stopRequested: () => stop.promise, + sleep: () => { + waiting.resolve(); + return when === "restart wait" ? new Promise(() => {}) : Promise.resolve(); + }, + choosePort: vi.fn() + .mockResolvedValueOnce(8080) + .mockImplementation(() => { + probing.resolve(); + return port.promise; + }), + }); + + const run = runServerStart({ network: "moksha", local: true }, h.io, h.deps); + await vi.waitFor(() => expect(h.deps.start).toHaveBeenCalledTimes(1)); + first.crash(1); + await (when === "restart wait" ? waiting.promise : probing.promise); + stop.resolve(); + await stop.promise; + port.resolve(8080); + + expect(await run).toBe(0); + const publishedEvents = h.events.map((event) => event.type); + expect(publishedEvents).not.toContain("server-restarted"); + expect(h.deps.start).toHaveBeenCalledTimes(1); + expect(publishedEvents.at(-1)).toBe("server-stopped"); + }, + ); diff --git a/verification/server-supervision/models/ServerSupervision.tla b/verification/server-supervision/models/ServerSupervision.tla new file mode 100644 index 0000000..1d996e4 --- /dev/null +++ b/verification/server-supervision/models/ServerSupervision.tla @@ -0,0 +1,51 @@ +---- MODULE ServerSupervision ---- +CONSTANTS StopAfterBackoff, StopAfterPortProbe +VARIABLES phase, stoppedAt, launchedAfterStop +vars == <> + +Init == phase = "running" /\ stoppedAt = "none" /\ launchedAfterStop = FALSE + +ServerExits == + /\ phase = "running" + /\ stoppedAt = "none" + /\ phase' = "backoff" + /\ UNCHANGED <> + +RequestStop == + /\ phase \in {"running", "backoff", "probing", "launching", "restarted"} + /\ stoppedAt = "none" + /\ stoppedAt' = phase + /\ UNCHANGED <> + +EndWait == + /\ phase = "backoff" + /\ phase' = IF stoppedAt = "backoff" /\ StopAfterBackoff THEN "stopped" ELSE "probing" + /\ UNCHANGED <> + +PortAvailable == + /\ phase = "probing" + /\ phase' = IF stoppedAt # "none" /\ StopAfterPortProbe THEN "stopped" ELSE "launching" + /\ launchedAfterStop' = (phase' = "launching" /\ stoppedAt # "none") + /\ UNCHANGED stoppedAt + +ServerReady == + /\ phase = "launching" + /\ phase' = "restarted" + /\ UNCHANGED <> + +StopServer == + /\ phase \in {"running", "restarted"} + /\ stoppedAt # "none" + /\ phase' = "stopped" + /\ UNCHANGED <> + +Done == + /\ phase \in {"stopped", "restarted"} + /\ UNCHANGED vars + +Next == ServerExits \/ RequestStop \/ EndWait \/ PortAvailable + \/ ServerReady \/ StopServer \/ Done +Spec == Init /\ [][Next]_vars +NoLaunchAfterStop == ~launchedAfterStop +BackoffStopPreventsLaunch == (stoppedAt = "backoff") => ~launchedAfterStop +==== diff --git a/verification/server-supervision/models/backoff.cfg b/verification/server-supervision/models/backoff.cfg new file mode 100644 index 0000000..a283506 --- /dev/null +++ b/verification/server-supervision/models/backoff.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANT StopAfterBackoff = TRUE +CONSTANT StopAfterPortProbe = FALSE +INVARIANT BackoffStopPreventsLaunch diff --git a/verification/server-supervision/models/current.cfg b/verification/server-supervision/models/current.cfg new file mode 100644 index 0000000..1ec8e8f --- /dev/null +++ b/verification/server-supervision/models/current.cfg @@ -0,0 +1,5 @@ +SPECIFICATION Spec +CONSTANT StopAfterBackoff = TRUE +CONSTANT StopAfterPortProbe = FALSE +INVARIANT NoLaunchAfterStop +INVARIANT BackoffStopPreventsLaunch diff --git a/verification/server-supervision/models/no-backoff-fence.cfg b/verification/server-supervision/models/no-backoff-fence.cfg new file mode 100644 index 0000000..7acdf55 --- /dev/null +++ b/verification/server-supervision/models/no-backoff-fence.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANT StopAfterBackoff = FALSE +CONSTANT StopAfterPortProbe = FALSE +INVARIANT BackoffStopPreventsLaunch diff --git a/verification/server-supervision/models/port-fence.cfg b/verification/server-supervision/models/port-fence.cfg new file mode 100644 index 0000000..f7e4c50 --- /dev/null +++ b/verification/server-supervision/models/port-fence.cfg @@ -0,0 +1,5 @@ +SPECIFICATION Spec +CONSTANT StopAfterBackoff = TRUE +CONSTANT StopAfterPortProbe = TRUE +INVARIANT NoLaunchAfterStop +INVARIANT BackoffStopPreventsLaunch diff --git a/verification/server-supervision/models/view.mjs b/verification/server-supervision/models/view.mjs new file mode 100644 index 0000000..63d281a --- /dev/null +++ b/verification/server-supervision/models/view.mjs @@ -0,0 +1,36 @@ +export const title = "Stop a local Personal Server during automatic restart"; + +export function state(values) { + if (values.launchedAfterStop) { + return { + launching: "Replacement starts after Stop", + restarted: "Restart reported after Stop", + stopped: "Replacement stopped again", + }[values.phase]; + } + if (values.phase === "probing" && values.stoppedAt !== "none") { + return "Stop requested while restart checks a port"; + } + if (values.phase === "backoff" && values.stoppedAt !== "none") { + return "Stop requested during restart wait"; + } + return { + running: "Personal Server running", + backoff: "Waiting before retry", + probing: "Checking a port for restart", + launching: "Starting a replacement", + restarted: "Personal Server restarted", + stopped: "Personal Server stopped", + }[values.phase]; +} + +export const step = (action) => + ({ + ServerExits: "Server exits unexpectedly", + RequestStop: "You stop the server", + EndWait: "Restart wait settles", + PortAvailable: "Port check returns", + ServerReady: "Replacement answers", + StopServer: "Supervisor stops the server", + Done: "Finish", + })[action]; diff --git a/verification/setup-resume/README.md b/verification/setup-resume/README.md new file mode 100644 index 0000000..0313f9e --- /dev/null +++ b/verification/setup-resume/README.md @@ -0,0 +1,74 @@ +# BUI-936 setup/resume verification + +The current CLI passed the bounded setup/resume checks. No current-code defect +reproduced. Seven passing TLA+ configurations, 61 offline real-code tests and seven +source-mutation controls support that result. Product code is unchanged. The fixtures use synthetic funding and read services. + +Checked main source: `a55d0a0006da6a743b6452796435afa6ed177dd8`. The runner records the exact source blobs. + +## What holds + +| Promise | Invariant | Owning implementation | +| ---------------------------------------------------------------------------------------------------- | ------------------------- | ---------------------------------------------------------------------------------------------------------------------------------- | +| Save recovery identity before either POST. | `DurableBeforePost` | `src/cli/app/request.ts`: frozen `intent`, `requests.saveIntent`, then `runConsentIntent`. | +| An uncertain funding POST recovers one operation using its original key. | `OneFundingOperation` | `src/cli/app/test-credit.ts`: saved funding UUID; `src/core/test-credit.ts`: POST body. | +| An uncertain consent POST replays the exact original request. | `OneConsentRequest` | `src/cli/app/request.ts`: `createAccessRequest(intent.input)`. | +| Pending funding or a claim link does not authorize consent creation. | `ConsentNeedsReadyCredit` | `prepareTestCredit`, authoritative `updateFunding` result, early `fundingOutcome` return. | +| Changed app, network, environment, endpoint or supplied payload is rejected before resume transport. | `ChangedResumeRejected` | `runAppRequest`: saved context and `REQUEST_PAYLOAD_OPTIONS` comparison. | +| Once a funding operation ID is saved, inspect it with GET. | `KnownFundingIsGetOnly` | `prepareTestCredit` forwards saved ID; `requestTestCredit` selects GET and omits body. | +| A delayed pending response cannot overwrite funded/failed progress. | `TerminalFundingRetained` | `src/core/requests-store.ts`: terminal check within the complete writer-locked read/modify/write; caller adopts returned progress. | + +`NoDeadlock` also holds. Stopped/pending/human-action states can stutter; this is +a safety check, not a promise of eventual completion. + +## Model bounds and source mapping + +The model represents one admitted setup, app, network, environment and opaque +frozen request payload. Funding and consent have separate immutable identities. +There are separate actions for writer acquisition, current-state read, temporary +setup write, atomic publication and release. Atomic rename is the visible commit +point. A process crash can happen between actions, including before/after a +remote acceptance or journal publication. Restart reloads saved context. + +| Configuration | Bound/scenario | Reachable states | Result | +| ------------------ | --------------------------------------------------------------- | ---------------: | ------ | +| `overview` | One command, one resume, no process crash | 128 | Pass | +| `single` | One command, two resumes, one crash | 606 | Pass | +| `concurrent` | Two commands, one resume each, no crash | 13,738 | Pass | +| `concurrent-crash` | Two commands, one resume each, one crash | 33,873 | Pass | +| `claim` | Claim required; two resumes, one crash | 659 | Pass | +| `existing-credit` | Pending existing deposit becomes usable; two resumes, one crash | 553 | Pass | +| `changed-context` | Changed context rejected on resume; two resumes, one crash | 90 | Pass | + +Response loss is separately allowed at either remote acceptance; it does not +consume the process-crash bound. Remote funding can become confirmed or failed. +Consent can remain pending, be approved, denied or expire. A second fresh command +either observes the unfinished setup or loses the admission race under the +journal writer lock. It must explicitly resume the admitted setup. + +The TLA+ model stops at the approval-result boundary. It does not model current +grant verification, signed claim construction, exact payload serialization or +schema validation. Existing real-code tests cover those, including refusal to +call an approved grant current when its gateway lookup fails. + +The writer-lock primitive is abstracted as exclusion with eventual recovery of +a demonstrably dead owner. Existing real-code tests also exercise interrupted +writers, a stale pre-lock read, a live owner, and preservation of a newer lock +owner. This is not a new proof of the lock algorithm itself. + +## Run + +Use Python 3.12+, the CLI's installed Node dependencies, Java and TLC 1.7.4. +Set `TLA2TOOLS` and `JAVA` for locally installed tools. + +```sh +python3 verification/setup-resume/check.py --out /tmp/vana-cli-setup-resume-proof +``` + +Use a fresh evidence path. The runner checks the main source at `a55d0a0006da6a743b6452796435afa6ed177dd8`. +It checks current and deliberately broken models, exercises the real code with +synthetic transport, restores the scratch source and repeats the replay. +The output directory contains the individual verdicts and replay logs. + +Use Pstack `/statechart` with the configs and view in `models/`. +The [CLI statecharts](../../docs/STATECHARTS.md) show the shorter scenarios. diff --git a/verification/setup-resume/check.py b/verification/setup-resume/check.py new file mode 100644 index 0000000..db1986d --- /dev/null +++ b/verification/setup-resume/check.py @@ -0,0 +1,167 @@ +#!/usr/bin/env python3 +"""Verify the pinned setup-resume code in a disposable offline snapshot.""" + +import argparse +import hashlib +import io +import json +import os +import re +from pathlib import Path +import shutil +import subprocess +import sys +import tarfile +import tempfile + +SOURCE_REVISION = "a55d0a0006da6a743b6452796435afa6ed177dd8" +OWNERS = {'src/cli/app/request.ts': 'adb502d804e1d0b77df9dfcaeba7c2ed797fcff9', 'src/cli/app/test-credit.ts': 'e347931d67126e125de682d14c06cfc2d659495d', 'src/core/test-credit.ts': 'fe8e30a1b1479efb1d69f0c96ed6f8eb45fe02a2', 'src/core/requests-store.ts': 'a963a68a387d68ee30a7fdb9e279534ffb8ed37d', 'src/cli/app/requests.ts': '2d24676082e008ee9a54b4e0dc2f98f3c8ba6055'} +JAR_SHA256 = "936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88" +HERE = Path(__file__).resolve().parent +REPO = HERE.parents[1] + + +def command(argv, cwd, env=None, timeout=90): + return subprocess.run( + argv, cwd=cwd, env=env, capture_output=True, text=True, timeout=timeout + ) + + +def checked(argv, cwd): + result = command(argv, cwd) + if result.returncode: + raise RuntimeError(result.stderr.strip() or result.stdout.strip()) + return result.stdout.strip() + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--ref", help="Check a committed revision instead of the working-tree patch") + parser.add_argument("--out", type=Path) + args = parser.parse_args() + revision = checked(["git", "rev-parse", args.ref or SOURCE_REVISION], REPO) + for owner, expected in OWNERS.items(): + actual = checked(["git", "rev-parse", f"{revision}:{owner}"], REPO) if args.ref else checked(["git", "hash-object", str(REPO / owner)], REPO) + if actual != expected: + raise RuntimeError( + f"Model/source drift: {owner} differs from its checked blob. " + "Review the model mapping before updating OWNERS." + ) + jar = os.environ.get("TLA2TOOLS") + if not jar: + jar = str( + Path(checked(["mise", "where", "github:tlaplus/tlaplus@1.7.4"], REPO)) + / "tla2tools.jar" + ) + if hashlib.sha256(Path(jar).read_bytes()).hexdigest() != JAR_SHA256: + raise RuntimeError("TLC jar differs from the pinned v1.7.4 SHA256") + java = os.environ.get("JAVA") or checked( + ["mise", "which", "java", "--tool", "java@temurin-25"], REPO + ) + out = args.out.resolve() if args.out else Path(tempfile.mkdtemp(prefix="setup-resume-check-")) + if args.out: + out.mkdir(parents=True, exist_ok=False) + snapshot = out / "snapshot" + snapshot.mkdir() + archive = subprocess.check_output(["git", "archive", revision], cwd=REPO) + with tarfile.open(fileobj=io.BytesIO(archive)) as tar: + # The archive has an unrelated absolute fixture symlink; never follow it. + tar.extractall( + snapshot, + members=[m for m in tar.getmembers() if not (m.issym() or m.islnk())], + filter="data", + ) + if not args.ref: + for owner in OWNERS: + shutil.copy2(REPO / owner, snapshot / owner) + for owner_test in ["test/cli/app-test-credit.test.ts", "test/cli/app-request-recovery.test.ts"]: + shutil.copy2(REPO / owner_test, snapshot / owner_test) + (snapshot / "node_modules").symlink_to(REPO / "node_modules", target_is_directory=True) + for source in (HERE / "fixtures").iterdir(): + if source.name == "vitest.formal.config.ts": + target = snapshot / source.name + elif source.name == "no-external-io.ts": + target = snapshot / "test/setup" / source.name + else: + target = snapshot / "test/cli" / source.name + shutil.copy2(source, target) + modeldir = out / "models" + shutil.copytree(HERE / "models", modeldir) + node = shutil.which("node") + testcmd = [node, str(snapshot / "node_modules/vitest/vitest.mjs"), "run", "--config", "vitest.formal.config.ts", "--reporter=verbose"] + summary = {"revision": revision, "owners": OWNERS, "source_mode": "commit" if args.ref else "verified working-tree files", "live_funding": False, "live_reads": False, "models": {}} + summary["model_files_sha256"] = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() for p in sorted(modeldir.iterdir()) if p.is_file()} + passing = ["overview", "single", "concurrent", "concurrent-crash", "claim", "existing-credit", "changed-context"] + negative = ["no-persist", "new-funding-key", "new-consent-key", "post-known-operation", "no-readiness", "no-context", "regress-funding"] + for case in passing + negative: + state_dir = out / f"tlc-{case}" + state_dir.mkdir() + result = command([ + java, "-XX:+UseParallelGC", "-cp", jar, "tlc2.TLC", + "-workers", "1", "-fp", "0", "-metadir", str(state_dir), + "-config", str(modeldir / f"{case}.cfg"), str(modeldir / "SetupResume.tla"), + ], modeldir) + (out / f"{case}-tlc.log").write_text(result.stdout + result.stderr) + expected = 0 if case in passing else 12 + if result.returncode != expected: + raise RuntimeError(f"{case}: expected TLC exit {expected}, got {result.returncode}; see {out}") + count = re.search(r"(\d+) distinct states found", result.stdout) + violation = re.search(r"Invariant (\w+) is violated", result.stdout) + expected_rule = dict(zip(negative, ["DurableBeforePost", "OneFundingOperation", "OneConsentRequest", "KnownFundingIsGetOnly", "ConsentNeedsReadyCredit", "ChangedResumeRejected", "TerminalFundingRetained"])) + if case in negative and (not violation or violation[1] != expected_rule[case]): + raise RuntimeError(f"{case}: did not break its intended invariant") + summary["models"][case] = {"exit": result.returncode, "states": int(count[1]) if count else None, "violation": violation[1] if violation else None} + baseline = command(testcmd, snapshot) + (out / "baseline-tests.log").write_text(baseline.stdout + baseline.stderr) + if baseline.returncode: + raise RuntimeError(f"Real-code replay failed; inspect {out / 'baseline-tests.log'}") + originals = {owner: (snapshot / owner).read_bytes() for owner in OWNERS} + def changed(owner, old, new): + source = originals[owner].decode() + if source.count(old) != 1: + raise RuntimeError(f"Mutation anchor drift: {owner}: {old}") + return source.replace(old, new) + mutations = [ + ("no-persist", "src/cli/app/request.ts", "requests.saveIntent(intent);", "void intent;", "setup-overlap", "does not transmit after a pre-POST journal write failure"), + ("new-funding-key", "src/core/test-credit.ts", "idempotencyKey: input.idempotencyKey", "idempotencyKey: randomUUID()", "app-test-credit", "resumes the same funding after"), + ("new-consent-key", "src/cli/app/request.ts", "controller.createAccessRequest(intent.input)", "controller.createAccessRequest({ ...intent.input, idempotencyKey: randomUUID() })", "app-request-recovery", "persists the exact consent intent before POST"), + ("post-known-operation", "src/cli/app/test-credit.ts", "operationId: intent.fundingProgress?.operationId,", "operationId: undefined,", "app-test-credit", "resumes the same funding after"), + ("no-readiness", "src/cli/app/request.ts", "if (fundingOutcome) return emitAppOutcome(options, fundingOutcome);", "void fundingOutcome;", "app-test-credit", "holds consent until finalization"), + ("no-context", "src/cli/app/request.ts", " payloadConflict\n", " false\n", "app-request-recovery", "refuses changed resume inputs"), + ("regress-funding", "src/core/requests-store.ts", 'intent.fundingProgress.status !== "pending"', "false", "setup-overlap", "retains terminal funding"), + ] + summary["mutations"] = {} + try: + for name, owner, old, new, file, selected in mutations: + source = snapshot / owner + source.write_text(changed(owner, old, new)) + result = command(testcmd + [f"test/cli/{file}.test.ts", "-t", selected], snapshot) + (out / f"mutation-{name}.log").write_text(result.stdout + result.stderr) + source.write_bytes(originals[owner]) + if result.returncode != 1 or "AssertionError" not in result.stdout + result.stderr: + raise RuntimeError(f"{name}: expected a behavioral assertion failure; inspect {out}") + summary["mutations"][name] = "caught by real-code assertion" + finally: + for owner, original in originals.items(): + (snapshot / owner).write_bytes(original) + restored = command(testcmd, snapshot) + (out / "restored-tests.log").write_text(restored.stdout + restored.stderr) + if restored.returncode: + raise RuntimeError(f"Restored baseline failed; inspect {out}") + for owner, blob in OWNERS.items(): + if checked(["git", "hash-object", str(snapshot / owner)], REPO) != blob: + raise RuntimeError(f"Scratch source was not restored: {owner}") + summary["product_snapshot_restored"] = True + summary["status"] = "passed: setup/resume safety under the documented bounds" + (out / "summary.json").write_text(json.dumps(summary, indent=2) + "\n") + print(json.dumps({"status": summary["status"], "evidence": str(out)}, indent=2)) + return 0 + + +if __name__ == "__main__": + try: + result = main() + except Exception as error: + print(f"Verification error: {error}", file=sys.stderr) + raise SystemExit(2) from error + raise SystemExit(result) diff --git a/verification/setup-resume/fixtures/no-external-io.ts b/verification/setup-resume/fixtures/no-external-io.ts new file mode 100644 index 0000000..ad91a47 --- /dev/null +++ b/verification/setup-resume/fixtures/no-external-io.ts @@ -0,0 +1,6 @@ +import { beforeEach, vi } from "vitest"; +beforeEach(() => { + vi.stubGlobal("fetch", async () => { + throw new Error("External network disabled for formal verification"); + }); +}); diff --git a/verification/setup-resume/fixtures/setup-overlap.test.ts b/verification/setup-resume/fixtures/setup-overlap.test.ts new file mode 100644 index 0000000..777f618 --- /dev/null +++ b/verification/setup-resume/fixtures/setup-overlap.test.ts @@ -0,0 +1,187 @@ +import fs from "node:fs"; +import os from "node:os"; +import path from "node:path"; +import { afterEach, beforeEach, expect, it, vi } from "vitest"; +import { privateKeyToAccount } from "viem/accounts"; +import { runAppRequest } from "../../src/cli/app/request.js"; +import { createRequestsStore } from "../../src/core/requests-store.js"; +import { appOutcomeSchema } from "../../src/cli/app/outcome.js"; + +// Public test key, also used by the owning recovery tests. +const privateKey = + "0x59c6995e998f97a5a0044966f0945389dc9e86dae88c7a8412f4603b6b78690d"; +const account = privateKeyToAccount(privateKey); +let directory: string; +let outcomes: ReturnType[]; + +beforeEach(() => { + directory = fs.mkdtempSync(path.join(os.tmpdir(), "vana-setup-overlap-")); + outcomes = []; + vi.stubEnv("VANA_ENV", "dev"); + vi.stubEnv("VANA_NETWORK", "moksha"); + vi.spyOn(process.stdout, "write").mockImplementation((chunk) => { + outcomes.push(appOutcomeSchema.parse(JSON.parse(String(chunk)))); + return true; + }); + vi.spyOn(process.stderr, "write").mockImplementation(() => true); +}); + +afterEach(() => { + vi.restoreAllMocks(); + vi.unstubAllEnvs(); + fs.rmSync(directory, { recursive: true, force: true }); +}); + +it("does not transmit after a pre-POST journal write failure", async () => { + const requests = createRequestsStore(path.join(directory, "requests.json")); + requests.saveIntent = () => { + throw new Error("fixture: rename failed"); + }; + const fetchCredit = vi.fn(async () => { + throw new Error("unexpected transmission"); + }); + const createConsent = vi.fn(async () => { + throw new Error("unexpected consent"); + }); + const result = await runAppRequest( + { json: true, noInput: true, scopes: "github.repositories" }, + { + requests, + resolveKey: () => ({ + privateKey, + address: account.address, + publicKey: account.publicKey, + source: "env" as const, + }), + readProfile: () => ({}), + fetchTestCredit: fetchCredit, + createController: (() => ({ + createAccessRequest: createConsent, + })) as never, + }, + ); + expect(result).toBe(1); + expect(fetchCredit).not.toHaveBeenCalled(); + expect(createConsent).not.toHaveBeenCalled(); +}); + +it.each([ + ["known operation", "confirmed"], + ["unknown operation", "confirmed"], + ["known operation", "failed"], + ["unknown operation", "failed"], +])( + "retains terminal funding when overlapping resumes reorder %s / %s", + async (identity, terminal) => { + const requests = createRequestsStore(path.join(directory, "requests.json")); + const fundingKeys = new Set(); + const consentKeys = new Set(); + let initial = true; + let calls = 0; + let posts = 0; + let gets = 0; + let releaseStale!: () => void; + let reachedStale!: () => void; + const staleReached = new Promise((resolve) => { + reachedStale = resolve; + }); + const staleRelease = new Promise((resolve) => { + releaseStale = resolve; + }); + const operation = (status: string) => + Response.json( + { + id: "credit_overlap", + appAddress: account.address, + status, + reason: "first_setup", + amountWei: "1000000000000000000", + txHash: `0x${"a".repeat(64)}`, + lastError: null, + }, + { status: 200 }, + ); + const fetchCredit: typeof fetch = async (url, init) => { + const target = new URL(String(url)); + expect(target.origin).toBe("https://account-dev.vana.org"); + if (init?.method === "POST") { + expect(target.pathname).toBe("/api/v1/moksha-test-credits"); + const body = JSON.parse( + new TextDecoder().decode(init.body as Uint8Array), + ); + expect( + fs.readFileSync(path.join(directory, "requests.json"), "utf8"), + ).toContain(body.idempotencyKey); + fundingKeys.add(body.idempotencyKey); + posts += 1; + } else { + expect(target.pathname).toBe( + "/api/v1/moksha-test-credits/operations/credit_overlap", + ); + gets += 1; + } + if (initial) { + if (identity === "unknown operation") + throw new Error("fixture accepted funding; response lost"); + return operation("submitted"); + } + calls += 1; + if (calls === 1) { + reachedStale(); + await staleRelease; + return operation("submitted"); + } + return operation(terminal); + }; + const deps = { + requests, + resolveKey: () => ({ + privateKey, + address: account.address, + publicKey: account.publicKey, + source: "env" as const, + }), + readProfile: () => ({}), + fetchTestCredit: fetchCredit, + createController: (() => ({ + createAccessRequest: async (input: { idempotencyKey: string }) => { + consentKeys.add(input.idempotencyKey); + return { + requestId: "dcr_overlap", + approvalUrl: "https://app-dev.vana.org/approve/overlap", + appAddress: account.address, + network: "moksha", + }; + }, + getAccessRequestStatus: async () => ({ status: "pending" }), + })) as never, + }; + await runAppRequest( + { json: true, noInput: true, scopes: "github.repositories" }, + deps, + ); + expect(outcomes.at(-1)?.exitCode).toBe(6); + const setupId = requests.listIntents()[0].setupId; + initial = false; + const resume = () => + runAppRequest({ json: true, noInput: true, resume: setupId }, deps); + const stale = resume(); + await staleReached; + await resume(); + releaseStale(); + await stale; + const expected = terminal === "confirmed" ? "funded" : "failed"; + expect(requests.getIntent(setupId)?.fundingProgress?.status).toBe(expected); + expect(outcomes.slice(1).map((outcome) => outcome.exitCode)).toEqual( + terminal === "confirmed" ? [7, 7] : [6, 6], + ); + expect(fundingKeys.size).toBe(1); + expect(consentKeys.size).toBe(terminal === "confirmed" ? 1 : 0); + expect(posts).toBe(identity === "known operation" ? 1 : 3); + expect(gets).toBe(identity === "known operation" ? 2 : 0); + const callsBefore = calls; + await resume(); + expect(calls).toBe(callsBefore); + expect(consentKeys.size).toBe(terminal === "confirmed" ? 1 : 0); + }, +); diff --git a/verification/setup-resume/fixtures/vitest.formal.config.ts b/verification/setup-resume/fixtures/vitest.formal.config.ts new file mode 100644 index 0000000..b5a3055 --- /dev/null +++ b/verification/setup-resume/fixtures/vitest.formal.config.ts @@ -0,0 +1,13 @@ +import { defineConfig } from "vitest/config"; + +export default defineConfig({ + test: { + globals: true, + include: [ + "test/cli/app-test-credit.test.ts", + "test/cli/app-request-recovery.test.ts", + "test/cli/setup-overlap.test.ts", + ], + setupFiles: ["test/setup/isolate-home.ts", "test/setup/no-external-io.ts"], + }, +}); diff --git a/verification/setup-resume/models/SetupResume.tla b/verification/setup-resume/models/SetupResume.tla new file mode 100644 index 0000000..ccb7ba1 --- /dev/null +++ b/verification/setup-resume/models/SetupResume.tla @@ -0,0 +1,157 @@ +------------------------- MODULE SetupResume ------------------------- +EXTENDS Naturals, FiniteSets +CONSTANTS Clients, Resumes, Crashes, ClaimRequired, ExistingBalance, + ContextMatches, PersistIntent, StableFundingKey, StableConsentKey, + KnownIdsReadOnly, RequireReady, CheckContext, MonotonicFunding +VARIABLE state +Workers == 1..Clients +Ready == {"funded", "not_needed"} +TerminalFunding == {"funded", "not_needed", "failed"} +InitialClient == [pc |-> "Fresh", fk |-> 0, ck |-> 0, fo |-> 0, fs |-> "none", + ci |-> 0, reply |-> "none", remote |-> 0, resumes |-> 0, + resuming |-> FALSE, writeFs |-> "none", writeFo |-> 0] +Init == state = [saved |-> FALSE, fk |-> 0, ck |-> 0, fo |-> 0, + fs |-> "none", ci |-> 0, writer |-> 0, + clients |-> [w \in Workers |-> InitialClient], + fundOps |-> {}, consentOps |-> {}, funded |-> FALSE, failed |-> FALSE, + claimed |-> ~ClaimRequired, decision |-> "pending", + existingReady |-> FALSE, crashes |-> 0, + unsafeDurability |-> FALSE, unsafeContext |-> FALSE, + unsafeKnown |-> FALSE, unsafeReady |-> FALSE, + regressed |-> FALSE] +CtxBad(w) == state.clients[w].resuming /\ ~ContextMatches +FundingKey(w) == state.clients[w].fk + IF StableFundingKey THEN 0 ELSE state.clients[w].resumes +ConsentKey(w) == state.clients[w].ck + IF StableConsentKey THEN 0 ELSE state.clients[w].resumes +Fresh(w) == /\ state.clients[w].pc = "Fresh" + /\ state' = [state EXCEPT !.clients[w].pc = IF state.saved THEN "Stopped" ELSE "SaveBegin"] +BeginSave(w) == /\ state.clients[w].pc = "SaveBegin" /\ state.writer = 0 + /\ state' = [state EXCEPT !.writer = w, !.clients[w].pc = "SaveCheck"] +CheckSave(w) == /\ state.clients[w].pc = "SaveCheck" + /\ state' = IF state.saved + THEN [state EXCEPT !.writer = 0, !.clients[w].pc = "Stopped"] + ELSE [state EXCEPT !.clients[w].pc = "SaveTemp", !.clients[w].fk = w, !.clients[w].ck = w] +SaveTemp(w) == /\ state.clients[w].pc = "SaveTemp" + /\ state' = [state EXCEPT !.clients[w].pc = "SaveCommit"] +SaveCommit(w) == /\ state.clients[w].pc = "SaveCommit" + /\ state' = IF PersistIntent + THEN [state EXCEPT !.saved = TRUE, !.fk = w, !.ck = w, !.clients[w].pc = "SaveRelease"] + ELSE [state EXCEPT !.clients[w].pc = "SaveRelease"] +SaveRelease(w) == /\ state.clients[w].pc = "SaveRelease" + /\ state' = [state EXCEPT !.writer = 0, !.clients[w].pc = "Funding"] +Resume(w) == /\ state.clients[w].pc \in {"Stopped", "Human", "AwaitApproval"} + /\ state.saved /\ state.clients[w].resumes < Resumes + /\ state' = [state EXCEPT !.clients[w].pc = "Load", !.clients[w].resuming = TRUE, + !.clients[w].resumes = @ + 1] +Load(w) == /\ state.clients[w].pc = "Load" + /\ state' = IF CheckContext /\ CtxBad(w) + THEN [state EXCEPT !.clients[w].pc = "Rejected"] + ELSE [state EXCEPT !.clients[w].fk = state.fk, !.clients[w].ck = state.ck, + !.clients[w].fo = state.fo, !.clients[w].fs = state.fs, + !.clients[w].ci = state.ci, !.clients[w].pc = "Funding"] +SkipReady(w) == /\ state.clients[w].pc = "Funding" /\ state.clients[w].fs \in Ready + /\ state' = [state EXCEPT !.clients[w].pc = "Consent"] +StopFailed(w) == /\ state.clients[w].pc = "Funding" /\ state.clients[w].fs = "failed" + /\ state' = [state EXCEPT !.clients[w].pc = "Stopped"] +FundPost(w) == /\ state.clients[w].pc = "Funding" /\ state.clients[w].fs \notin TerminalFunding + /\ (state.clients[w].fo = 0 \/ ~KnownIdsReadOnly) + /\ state' = [state EXCEPT + !.unsafeDurability = (@ \/ ~state.saved), + !.unsafeKnown = (@ \/ state.clients[w].fo # 0), + !.unsafeContext = (@ \/ CtxBad(w)), + !.fundOps = IF state.claimed /\ ~ExistingBalance THEN @ \cup {FundingKey(w)} ELSE @, + !.clients[w].remote = IF ExistingBalance THEN 0 ELSE FundingKey(w), + !.clients[w].reply = IF ~state.claimed THEN "claim" + ELSE IF ExistingBalance THEN IF state.existingReady THEN "not_needed" ELSE "pending" + ELSE IF state.failed THEN "failed" ELSE IF state.funded THEN "funded" ELSE "pending", + !.clients[w].pc = "FundReply"] +FundGet(w) == /\ state.clients[w].pc = "Funding" /\ state.clients[w].fs \notin TerminalFunding + /\ state.clients[w].fo # 0 /\ KnownIdsReadOnly + /\ state' = [state EXCEPT !.unsafeContext = (@ \/ CtxBad(w)), + !.clients[w].remote = state.clients[w].fo, + !.clients[w].reply = IF state.failed THEN "failed" ELSE IF state.funded THEN "funded" ELSE "pending", + !.clients[w].pc = "FundReply"] +Claim(w) == /\ state.clients[w].pc = "FundReply" /\ state.clients[w].reply = "claim" + /\ state' = [state EXCEPT !.clients[w].pc = IF RequireReady THEN "Human" ELSE "Consent"] +AcceptFunding(w) == /\ state.clients[w].pc = "FundReply" /\ state.clients[w].reply # "claim" + /\ state' = [state EXCEPT !.clients[w].pc = "FundSaveBegin"] +BeginFundSave(w) == /\ state.clients[w].pc = "FundSaveBegin" /\ state.writer = 0 + /\ state' = [state EXCEPT !.writer = w, !.clients[w].pc = "FundSaveRead"] +ReadFundSave(w) == /\ state.clients[w].pc = "FundSaveRead" + /\ state' = IF state.fo # 0 /\ state.fo # state.clients[w].remote + THEN [state EXCEPT !.writer = 0, !.clients[w].pc = "Stopped"] + ELSE IF MonotonicFunding /\ state.fs \in TerminalFunding + THEN [state EXCEPT !.clients[w].pc = "FundRetainRelease"] + ELSE [state EXCEPT + !.clients[w].writeFo = state.clients[w].remote, + !.clients[w].writeFs = state.clients[w].reply, + !.clients[w].pc = "FundSaveCommit"] +CommitFundSave(w) == /\ state.clients[w].pc = "FundSaveCommit" + /\ state' = [state EXCEPT + !.regressed = (@ \/ (state.fs \in TerminalFunding /\ state.clients[w].writeFs \notin TerminalFunding)), + !.fs = state.clients[w].writeFs, !.fo = state.clients[w].writeFo, + !.clients[w].fs = state.clients[w].writeFs, + !.clients[w].fo = state.clients[w].writeFo, + !.clients[w].pc = "FundSaveRelease"] +ReleaseRetainedFunding(w) == /\ state.clients[w].pc = "FundRetainRelease" + /\ state' = [state EXCEPT !.writer = 0, + !.clients[w].fs = state.fs, !.clients[w].fo = state.fo, + !.clients[w].pc = IF state.fs \in Ready THEN "Consent" ELSE "Stopped"] +JournalBusy(w) == /\ state.clients[w].pc \in {"SaveBegin", "FundSaveBegin", "ConsentReply"} + /\ state.writer # 0 + /\ state' = [state EXCEPT !.clients[w].pc = "Stopped"] +ReleaseFundSave(w) == /\ state.clients[w].pc = "FundSaveRelease" + /\ state' = [state EXCEPT !.writer = 0, + !.clients[w].pc = IF state.clients[w].fs \in Ready \/ ~RequireReady THEN "Consent" ELSE "Stopped"] +ConsentPost(w) == /\ state.clients[w].pc = "Consent" /\ state.clients[w].ci = 0 + /\ state' = [state EXCEPT + !.unsafeDurability = (@ \/ ~state.saved), + !.unsafeContext = (@ \/ CtxBad(w)), + !.unsafeReady = (@ \/ state.clients[w].fs \notin Ready), + !.consentOps = @ \cup {ConsentKey(w)}, + !.clients[w].remote = ConsentKey(w), !.clients[w].pc = "ConsentReply"] +ConsentGet(w) == /\ state.clients[w].pc = "Consent" /\ state.clients[w].ci # 0 + /\ state' = [state EXCEPT !.unsafeContext = (@ \/ CtxBad(w)), !.clients[w].pc = "CheckApproval"] +BeginConsentSave(w) == /\ state.clients[w].pc = "ConsentReply" /\ state.writer = 0 + /\ state' = [state EXCEPT !.writer = w, !.clients[w].pc = "ConsentSaveRead"] +ReadConsentSave(w) == /\ state.clients[w].pc = "ConsentSaveRead" + /\ state' = IF state.ci # 0 /\ state.ci # state.clients[w].remote + THEN [state EXCEPT !.writer = 0, !.clients[w].pc = "Stopped"] + ELSE [state EXCEPT !.clients[w].pc = "ConsentSaveCommit"] +CommitConsentSave(w) == /\ state.clients[w].pc = "ConsentSaveCommit" + /\ state' = [state EXCEPT !.ci = state.clients[w].remote, + !.clients[w].ci = state.clients[w].remote, !.clients[w].pc = "ConsentSaveRelease"] +ReleaseConsentSave(w) == /\ state.clients[w].pc = "ConsentSaveRelease" + /\ state' = [state EXCEPT !.writer = 0, !.clients[w].pc = "CheckApproval"] +CheckApproval(w) == /\ state.clients[w].pc = "CheckApproval" + /\ state' = [state EXCEPT !.clients[w].pc = IF state.decision = "pending" THEN "AwaitApproval" + ELSE IF state.decision = "approved" THEN "Done" ELSE "Refused"] +LoseResponse(w) == /\ state.clients[w].pc \in {"FundReply", "ConsentReply"} + /\ state' = [state EXCEPT !.clients[w].pc = "Stopped"] +Crash(w) == /\ state.crashes < Crashes /\ state.clients[w].pc \notin {"Done", "Refused", "Rejected"} + /\ state' = [state EXCEPT !.crashes = @ + 1, !.clients[w].pc = "Stopped", + !.writer = IF @ = w THEN 0 ELSE @] +HumanClaims == /\ ~state.claimed /\ state.saved /\ state' = [state EXCEPT !.claimed = TRUE] +CreditReady == /\ state.fundOps # {} /\ ~state.funded /\ ~state.failed /\ state' = [state EXCEPT !.funded = TRUE] +CreditFails == /\ state.fundOps # {} /\ ~state.funded /\ ~state.failed /\ state' = [state EXCEPT !.failed = TRUE] +ExistingReady == /\ ExistingBalance /\ ~state.existingReady /\ state.saved + /\ state' = [state EXCEPT !.existingReady = TRUE] +HumanDecides == /\ state.consentOps # {} /\ state.decision = "pending" + /\ \E decision \in {"approved", "denied", "expired"} : state' = [state EXCEPT !.decision = decision] +Finished == /\ \A w \in Workers : state.clients[w].pc \in {"Done", "Refused", "Rejected", "Stopped", "Human", "AwaitApproval"} + /\ state.writer = 0 /\ UNCHANGED state +Next == (\E w \in Workers : Fresh(w) \/ BeginSave(w) \/ CheckSave(w) \/ SaveTemp(w) + \/ SaveCommit(w) \/ SaveRelease(w) \/ Resume(w) \/ Load(w) \/ SkipReady(w) + \/ StopFailed(w) \/ FundPost(w) \/ FundGet(w) \/ Claim(w) \/ AcceptFunding(w) + \/ JournalBusy(w) \/ ReleaseRetainedFunding(w) \/ BeginFundSave(w) \/ ReadFundSave(w) \/ CommitFundSave(w) \/ ReleaseFundSave(w) + \/ ConsentPost(w) \/ ConsentGet(w) \/ BeginConsentSave(w) \/ ReadConsentSave(w) + \/ CommitConsentSave(w) \/ ReleaseConsentSave(w) \/ CheckApproval(w) + \/ LoseResponse(w) \/ Crash(w)) \/ HumanClaims \/ CreditReady \/ CreditFails \/ ExistingReady \/ HumanDecides \/ Finished +Spec == Init /\ [][Next]_state +DurableBeforePost == ~state.unsafeDurability +OneFundingOperation == Cardinality(state.fundOps) <= 1 +OneConsentRequest == Cardinality(state.consentOps) <= 1 +ConsentNeedsReadyCredit == ~state.unsafeReady +ChangedResumeRejected == ~state.unsafeContext +KnownFundingIsGetOnly == ~state.unsafeKnown +TerminalFundingRetained == ~state.regressed +============================================================================= diff --git a/verification/setup-resume/models/changed-context.cfg b/verification/setup-resume/models/changed-context.cfg new file mode 100644 index 0000000..286bdec --- /dev/null +++ b/verification/setup-resume/models/changed-context.cfg @@ -0,0 +1,16 @@ +SPECIFICATION Spec +CONSTANTS +Clients = 1 +Resumes = 2 +Crashes = 1 +ClaimRequired = FALSE +ExistingBalance = FALSE +ContextMatches = FALSE +PersistIntent = TRUE +StableFundingKey = TRUE +StableConsentKey = TRUE +KnownIdsReadOnly = TRUE +RequireReady = TRUE +CheckContext = TRUE +MonotonicFunding = TRUE +INVARIANTS DurableBeforePost OneFundingOperation OneConsentRequest ConsentNeedsReadyCredit ChangedResumeRejected KnownFundingIsGetOnly TerminalFundingRetained diff --git a/verification/setup-resume/models/claim.cfg b/verification/setup-resume/models/claim.cfg new file mode 100644 index 0000000..8b76f47 --- /dev/null +++ b/verification/setup-resume/models/claim.cfg @@ -0,0 +1,16 @@ +SPECIFICATION Spec +CONSTANTS +Clients = 1 +Resumes = 2 +Crashes = 1 +ClaimRequired = TRUE +ExistingBalance = FALSE +ContextMatches = TRUE +PersistIntent = TRUE +StableFundingKey = TRUE +StableConsentKey = TRUE +KnownIdsReadOnly = TRUE +RequireReady = TRUE +CheckContext = TRUE +MonotonicFunding = TRUE +INVARIANTS DurableBeforePost OneFundingOperation OneConsentRequest ConsentNeedsReadyCredit ChangedResumeRejected KnownFundingIsGetOnly TerminalFundingRetained diff --git a/verification/setup-resume/models/concurrent-crash.cfg b/verification/setup-resume/models/concurrent-crash.cfg new file mode 100644 index 0000000..fef7b9e --- /dev/null +++ b/verification/setup-resume/models/concurrent-crash.cfg @@ -0,0 +1,16 @@ +SPECIFICATION Spec +CONSTANTS +Clients = 2 +Resumes = 1 +Crashes = 1 +ClaimRequired = FALSE +ExistingBalance = FALSE +ContextMatches = TRUE +PersistIntent = TRUE +StableFundingKey = TRUE +StableConsentKey = TRUE +KnownIdsReadOnly = TRUE +RequireReady = TRUE +CheckContext = TRUE +MonotonicFunding = TRUE +INVARIANTS DurableBeforePost OneFundingOperation OneConsentRequest ConsentNeedsReadyCredit ChangedResumeRejected KnownFundingIsGetOnly TerminalFundingRetained diff --git a/verification/setup-resume/models/concurrent.cfg b/verification/setup-resume/models/concurrent.cfg new file mode 100644 index 0000000..5738cc1 --- /dev/null +++ b/verification/setup-resume/models/concurrent.cfg @@ -0,0 +1,16 @@ +SPECIFICATION Spec +CONSTANTS +Clients = 2 +Resumes = 1 +Crashes = 0 +ClaimRequired = FALSE +ExistingBalance = FALSE +ContextMatches = TRUE +PersistIntent = TRUE +StableFundingKey = TRUE +StableConsentKey = TRUE +KnownIdsReadOnly = TRUE +RequireReady = TRUE +CheckContext = TRUE +MonotonicFunding = TRUE +INVARIANTS DurableBeforePost OneFundingOperation OneConsentRequest ConsentNeedsReadyCredit ChangedResumeRejected KnownFundingIsGetOnly TerminalFundingRetained diff --git a/verification/setup-resume/models/details.mjs b/verification/setup-resume/models/details.mjs new file mode 100644 index 0000000..675666a --- /dev/null +++ b/verification/setup-resume/models/details.mjs @@ -0,0 +1,47 @@ +import { state as overview, step, title } from "./overview.mjs"; +export { step, title }; + +const phases = { + Fresh: "new command", + SaveBegin: "waiting to save setup", + SaveCheck: "checking unfinished setups under lock", + SaveTemp: "preparing temporary journal", + SaveCommit: "ready to rename setup journal", + SaveRelease: "setup publication finished; release lock next", + Load: "validating resume context", + Funding: "ready to inspect funding", + FundReply: "funding response received", + FundSaveBegin: "waiting to save funding", + FundSaveRead: "reading current funding under lock", + FundSaveCommit: "ready to publish selected funding result", + FundSaveRelease: "funding publication finished; release lock next", + FundRetainRelease: "terminal funding retained; release lock next", + Consent: "ready to recover consent", + ConsentReply: "consent accepted remotely", + ConsentSaveRead: "checking consent identity under lock", + ConsentSaveCommit: "ready to publish consent identity", + ConsentSaveRelease: "consent publication finished; release lock next", + CheckApproval: "checking approval", + Stopped: "stopped", + Human: "waiting for claim", + AwaitApproval: "waiting for approval", + Done: "approval received", + Refused: "denied or expired", + Rejected: "changed context rejected", +}; + +// Counterexamples retain each command's phase and the journal/service changes. +// In particular, a second command must remain visible during a stale write. +export function state(v) { + const s = v.state; + const commands = Object.entries(s.clients).map( + ([id, c]) => + `Command ${id}: ${phases[c.pc]}; cached funding ${c.fs}; reply ${c.reply}; selected write ${c.writeFs}; resume ${c.resumes}`, + ); + return [ + overview(v), + ...commands, + `Journal: ${s.saved ? "setup saved" : "setup absent"}, funding ${s.fs}, operation ${s.fo || "unknown"}, consent ${s.ci || "unknown"}, writer ${s.writer || "none"}`, + `Service: ${s.claimed ? "claimed" : "unclaimed"}, credit ${s.failed ? "failed" : s.funded || s.existingReady ? "usable" : "pending"}, approval ${s.decision}, funding keys ${s.fundOps.join(",") || "none"}, consent keys ${s.consentOps.join(",") || "none"}, exits ${s.crashes}`, + ].join(" | "); +} diff --git a/verification/setup-resume/models/existing-credit.cfg b/verification/setup-resume/models/existing-credit.cfg new file mode 100644 index 0000000..b38ecb5 --- /dev/null +++ b/verification/setup-resume/models/existing-credit.cfg @@ -0,0 +1,16 @@ +SPECIFICATION Spec +CONSTANTS +Clients = 1 +Resumes = 2 +Crashes = 1 +ClaimRequired = FALSE +ExistingBalance = TRUE +ContextMatches = TRUE +PersistIntent = TRUE +StableFundingKey = TRUE +StableConsentKey = TRUE +KnownIdsReadOnly = TRUE +RequireReady = TRUE +CheckContext = TRUE +MonotonicFunding = TRUE +INVARIANTS DurableBeforePost OneFundingOperation OneConsentRequest ConsentNeedsReadyCredit ChangedResumeRejected KnownFundingIsGetOnly TerminalFundingRetained diff --git a/verification/setup-resume/models/new-consent-key.cfg b/verification/setup-resume/models/new-consent-key.cfg new file mode 100644 index 0000000..93173ac --- /dev/null +++ b/verification/setup-resume/models/new-consent-key.cfg @@ -0,0 +1,16 @@ +SPECIFICATION Spec +CONSTANTS +Clients = 1 +Resumes = 2 +Crashes = 1 +ClaimRequired = FALSE +ExistingBalance = FALSE +ContextMatches = TRUE +PersistIntent = TRUE +StableFundingKey = TRUE +StableConsentKey = FALSE +KnownIdsReadOnly = TRUE +RequireReady = TRUE +CheckContext = TRUE +MonotonicFunding = TRUE +INVARIANTS DurableBeforePost OneFundingOperation OneConsentRequest ConsentNeedsReadyCredit ChangedResumeRejected KnownFundingIsGetOnly TerminalFundingRetained diff --git a/verification/setup-resume/models/new-funding-key.cfg b/verification/setup-resume/models/new-funding-key.cfg new file mode 100644 index 0000000..309ec7c --- /dev/null +++ b/verification/setup-resume/models/new-funding-key.cfg @@ -0,0 +1,16 @@ +SPECIFICATION Spec +CONSTANTS +Clients = 1 +Resumes = 2 +Crashes = 1 +ClaimRequired = FALSE +ExistingBalance = FALSE +ContextMatches = TRUE +PersistIntent = TRUE +StableFundingKey = FALSE +StableConsentKey = TRUE +KnownIdsReadOnly = TRUE +RequireReady = TRUE +CheckContext = TRUE +MonotonicFunding = TRUE +INVARIANTS DurableBeforePost OneFundingOperation OneConsentRequest ConsentNeedsReadyCredit ChangedResumeRejected KnownFundingIsGetOnly TerminalFundingRetained diff --git a/verification/setup-resume/models/no-context.cfg b/verification/setup-resume/models/no-context.cfg new file mode 100644 index 0000000..ff49b63 --- /dev/null +++ b/verification/setup-resume/models/no-context.cfg @@ -0,0 +1,16 @@ +SPECIFICATION Spec +CONSTANTS +Clients = 1 +Resumes = 2 +Crashes = 1 +ClaimRequired = FALSE +ExistingBalance = FALSE +ContextMatches = FALSE +PersistIntent = TRUE +StableFundingKey = TRUE +StableConsentKey = TRUE +KnownIdsReadOnly = TRUE +RequireReady = TRUE +CheckContext = FALSE +MonotonicFunding = TRUE +INVARIANTS DurableBeforePost OneFundingOperation OneConsentRequest ConsentNeedsReadyCredit ChangedResumeRejected KnownFundingIsGetOnly TerminalFundingRetained diff --git a/verification/setup-resume/models/no-persist.cfg b/verification/setup-resume/models/no-persist.cfg new file mode 100644 index 0000000..56171db --- /dev/null +++ b/verification/setup-resume/models/no-persist.cfg @@ -0,0 +1,16 @@ +SPECIFICATION Spec +CONSTANTS +Clients = 1 +Resumes = 2 +Crashes = 1 +ClaimRequired = FALSE +ExistingBalance = FALSE +ContextMatches = TRUE +PersistIntent = FALSE +StableFundingKey = TRUE +StableConsentKey = TRUE +KnownIdsReadOnly = TRUE +RequireReady = TRUE +CheckContext = TRUE +MonotonicFunding = TRUE +INVARIANTS DurableBeforePost OneFundingOperation OneConsentRequest ConsentNeedsReadyCredit ChangedResumeRejected KnownFundingIsGetOnly TerminalFundingRetained diff --git a/verification/setup-resume/models/no-readiness.cfg b/verification/setup-resume/models/no-readiness.cfg new file mode 100644 index 0000000..e270436 --- /dev/null +++ b/verification/setup-resume/models/no-readiness.cfg @@ -0,0 +1,16 @@ +SPECIFICATION Spec +CONSTANTS +Clients = 1 +Resumes = 2 +Crashes = 1 +ClaimRequired = FALSE +ExistingBalance = FALSE +ContextMatches = TRUE +PersistIntent = TRUE +StableFundingKey = TRUE +StableConsentKey = TRUE +KnownIdsReadOnly = TRUE +RequireReady = FALSE +CheckContext = TRUE +MonotonicFunding = TRUE +INVARIANTS DurableBeforePost OneFundingOperation OneConsentRequest ConsentNeedsReadyCredit ChangedResumeRejected KnownFundingIsGetOnly TerminalFundingRetained diff --git a/verification/setup-resume/models/overview.cfg b/verification/setup-resume/models/overview.cfg new file mode 100644 index 0000000..b179e65 --- /dev/null +++ b/verification/setup-resume/models/overview.cfg @@ -0,0 +1,16 @@ +SPECIFICATION Spec +CONSTANTS +Clients = 1 +Resumes = 1 +Crashes = 0 +ClaimRequired = FALSE +ExistingBalance = FALSE +ContextMatches = TRUE +PersistIntent = TRUE +StableFundingKey = TRUE +StableConsentKey = TRUE +KnownIdsReadOnly = TRUE +RequireReady = TRUE +CheckContext = TRUE +MonotonicFunding = TRUE +INVARIANTS DurableBeforePost OneFundingOperation OneConsentRequest ConsentNeedsReadyCredit ChangedResumeRejected KnownFundingIsGetOnly TerminalFundingRetained diff --git a/verification/setup-resume/models/overview.mjs b/verification/setup-resume/models/overview.mjs new file mode 100644 index 0000000..d12d532 --- /dev/null +++ b/verification/setup-resume/models/overview.mjs @@ -0,0 +1,96 @@ +export const title = + "Setup resumes with the saved funding and consent identities"; + +export function state({ state: s }) { + const c = s.clients[1]; + let label; + if (c.pc === "Fresh") label = "New setup"; + else if (c.pc.startsWith("Save")) label = "Saving setup identity"; + else if (c.pc === "Load") label = "Checking resume context"; + else if (c.pc === "Funding") + label = + c.fs === "failed" + ? "Funding failed" + : ["funded", "not_needed"].includes(c.fs) + ? "Credit ready" + : c.fo + ? "Inspecting saved funding" + : "Requesting funding with saved key"; + else if (c.pc === "FundReply") + label = { + claim: "Claim required", + pending: "Funding pending", + funded: "Usable credit confirmed", + not_needed: "Existing credit usable", + failed: "Funding failed", + }[c.reply]; + else if (c.pc.startsWith("FundSave") || c.pc === "FundRetainRelease") + label = "Saving funding result"; + else if (c.pc === "Consent") + label = c.ci + ? "Inspecting saved consent" + : "Creating consent with saved key"; + else if (c.pc === "ConsentReply") label = "Consent accepted remotely"; + else if (c.pc.startsWith("ConsentSave")) label = "Saving consent identity"; + else + label = + { + Stopped: s.saved + ? "Setup saved for resume" + : "Stopped before setup was saved", + Human: "Waiting for a person to claim", + AwaitApproval: "Waiting for approval", + CheckApproval: "Checking approval", + Done: "Approval received", + Refused: "Denied or expired", + Rejected: "Changed context rejected", + }[c.pc] ?? c.pc; + const failures = []; + if (s.unsafeDurability) failures.push("sent before saving"); + if (s.fundOps.length > 1) failures.push("second funding operation"); + if (s.consentOps.length > 1) failures.push("second consent request"); + if (s.unsafeKnown) failures.push("POST despite known funding ID"); + if (s.unsafeReady) failures.push("consent before usable credit"); + if (s.unsafeContext) failures.push("changed resume transmitted"); + if (s.regressed) failures.push("terminal funding overwritten"); + return failures.length ? `${label}: ${failures.join(", ")}` : label; +} + +export const step = (action) => + ({ + JournalBusy: "leave setup resumable while another command writes", + ReleaseRetainedFunding: "retain terminal funding and release the journal", + Fresh: "start setup", + BeginSave: "take journal writer lock", + CheckSave: "check for an unfinished setup", + SaveTemp: "write and sync temporary journal", + SaveCommit: "atomically publish setup identity", + SaveRelease: "release journal writer lock", + Resume: "run saved resume command", + Load: "validate saved identity and options", + SkipReady: "reuse saved usable credit", + StopFailed: "retain failure for inspection", + FundPost: "send the saved funding key", + FundGet: "GET the saved operation", + Claim: "show claim handoff", + AcceptFunding: "accept funding response", + BeginFundSave: "take journal writer lock", + ReadFundSave: "read current funding under lock", + CommitFundSave: "atomically publish funding result", + ReleaseFundSave: "release journal writer lock", + ConsentPost: "send the saved consent payload", + ConsentGet: "GET the saved request", + BeginConsentSave: "take journal writer lock", + ReadConsentSave: "check the saved request identity", + CommitConsentSave: "atomically publish consent identity", + ReleaseConsentSave: "release journal writer lock", + CheckApproval: "read approval result", + LoseResponse: "lose the response after remote acceptance", + Crash: "process exits before the next step", + HumanClaims: "person completes claim", + CreditReady: "service confirms usable credit", + CreditFails: "service reports funding failure", + ExistingReady: "existing deposit becomes usable", + HumanDecides: "person approves or refuses", + Finished: "wait for another invocation", + })[action] ?? action; diff --git a/verification/setup-resume/models/post-known-operation.cfg b/verification/setup-resume/models/post-known-operation.cfg new file mode 100644 index 0000000..52562ff --- /dev/null +++ b/verification/setup-resume/models/post-known-operation.cfg @@ -0,0 +1,16 @@ +SPECIFICATION Spec +CONSTANTS +Clients = 1 +Resumes = 2 +Crashes = 1 +ClaimRequired = FALSE +ExistingBalance = FALSE +ContextMatches = TRUE +PersistIntent = TRUE +StableFundingKey = TRUE +StableConsentKey = TRUE +KnownIdsReadOnly = FALSE +RequireReady = TRUE +CheckContext = TRUE +MonotonicFunding = TRUE +INVARIANTS DurableBeforePost OneFundingOperation OneConsentRequest ConsentNeedsReadyCredit ChangedResumeRejected KnownFundingIsGetOnly TerminalFundingRetained diff --git a/verification/setup-resume/models/regress-funding.cfg b/verification/setup-resume/models/regress-funding.cfg new file mode 100644 index 0000000..b240bf6 --- /dev/null +++ b/verification/setup-resume/models/regress-funding.cfg @@ -0,0 +1,16 @@ +SPECIFICATION Spec +CONSTANTS +Clients = 2 +Resumes = 1 +Crashes = 0 +ClaimRequired = FALSE +ExistingBalance = FALSE +ContextMatches = TRUE +PersistIntent = TRUE +StableFundingKey = TRUE +StableConsentKey = TRUE +KnownIdsReadOnly = TRUE +RequireReady = TRUE +CheckContext = TRUE +MonotonicFunding = FALSE +INVARIANTS DurableBeforePost OneFundingOperation OneConsentRequest ConsentNeedsReadyCredit ChangedResumeRejected KnownFundingIsGetOnly TerminalFundingRetained diff --git a/verification/setup-resume/models/single.cfg b/verification/setup-resume/models/single.cfg new file mode 100644 index 0000000..073094f --- /dev/null +++ b/verification/setup-resume/models/single.cfg @@ -0,0 +1,16 @@ +SPECIFICATION Spec +CONSTANTS +Clients = 1 +Resumes = 2 +Crashes = 1 +ClaimRequired = FALSE +ExistingBalance = FALSE +ContextMatches = TRUE +PersistIntent = TRUE +StableFundingKey = TRUE +StableConsentKey = TRUE +KnownIdsReadOnly = TRUE +RequireReady = TRUE +CheckContext = TRUE +MonotonicFunding = TRUE +INVARIANTS DurableBeforePost OneFundingOperation OneConsentRequest ConsentNeedsReadyCredit ChangedResumeRejected KnownFundingIsGetOnly TerminalFundingRetained