diff --git a/CHANGELOG.md b/CHANGELOG.md index 483c9d40..f0c7a107 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,8 @@ releases could contain breaking changes when called out explicitly. ### Fixed +- Keep conversation compilation previews recoverable after lock-contention and filesystem errors, returning an error reply and preserving pending actions instead of failing the turn. + - Preserve affected artifact references such as `go.mod` in conversation previews without treating them as source-model locations. - Advertise conversation protocol support in the actual LSP initialize response so native editor chat can pass capability negotiation. diff --git a/cli/src/modelable/llm/filesystem_conversation.py b/cli/src/modelable/llm/filesystem_conversation.py index 9ff39469..8179b456 100644 --- a/cli/src/modelable/llm/filesystem_conversation.py +++ b/cli/src/modelable/llm/filesystem_conversation.py @@ -164,6 +164,8 @@ def preview_compilation( CompilationPolicy, CompilationRequest, ) + from modelable.operations.file_transaction import LockContentionError + from modelable.registry.ids import RegistryIdLockContentionError replaced = self._pending actual_replaced_id = _pending_id(replaced) @@ -182,7 +184,14 @@ def preview_compilation( ), policy=CompilationPolicy.conversation(), ) - except (CompilationError, json.JSONDecodeError, sqlite3.OperationalError) as error: + except ( + CompilationError, + json.JSONDecodeError, + sqlite3.OperationalError, + LockContentionError, + RegistryIdLockContentionError, + OSError, + ) as error: return ConversationReply( kind="error", text=f"Could not preview compilation: {_escape_inline(error)}", diff --git a/cli/tests/test_conversation_preview_recovery.py b/cli/tests/test_conversation_preview_recovery.py index 4437981f..e85fb646 100644 --- a/cli/tests/test_conversation_preview_recovery.py +++ b/cli/tests/test_conversation_preview_recovery.py @@ -8,6 +8,16 @@ from modelable.llm.conversation import ConversationSession from modelable.operations.compilation import CompilationError +from modelable.operations.file_transaction import LockContentionError +from modelable.registry.ids import RegistryIdLockContentionError + +OPERATIONAL_ERRORS = [ + json.JSONDecodeError("bad ledger", "{", 1), + sqlite3.OperationalError("database unavailable"), + RegistryIdLockContentionError("ledger contention"), + LockContentionError("publication contention"), + OSError("staging allocation failure"), +] @pytest.fixture @@ -20,9 +30,7 @@ def preview_session(catalog_workspace): session.close() -@pytest.mark.parametrize( - "error", [json.JSONDecodeError("bad ledger", "{", 1), sqlite3.OperationalError("database unavailable")] -) +@pytest.mark.parametrize("error", OPERATIONAL_ERRORS) def test_first_preview_operational_failure_is_a_domain_error(preview_session, monkeypatch, error): session, root, stages, request, service = preview_session original = request.source.read_bytes() @@ -52,11 +60,7 @@ def test_preview_programming_faults_still_propagate(preview_session, monkeypatch @pytest.mark.parametrize( "error", - [ - CompilationError("preview rejected"), - json.JSONDecodeError("bad ledger", "{", 1), - sqlite3.OperationalError("database unavailable"), - ], + [CompilationError("preview rejected"), *OPERATIONAL_ERRORS], ) def test_failed_replacement_keeps_pending_stage_until_close(preview_session, monkeypatch, error): session, root, stages, _request, service = preview_session diff --git a/cli/tests/test_offline_feature_qualification.py b/cli/tests/test_offline_feature_qualification.py index d5d005fd..d394c51a 100644 --- a/cli/tests/test_offline_feature_qualification.py +++ b/cli/tests/test_offline_feature_qualification.py @@ -18,7 +18,7 @@ from modelable.emitters.targets import list_implemented_codegen_targets RUST_FIXTURE = Path(__file__).parent / "fixtures" / "offline-rust-consumer" -FAST_GENERATION_BUDGET_SECONDS = 30 +FAST_GENERATION_BUDGET_SECONDS = 45 LANGUAGE_MATRIX_BUDGET_SECONDS = 120 PRODUCER_V1 = """ diff --git a/docs/superpowers/specs/system-spec/README.md b/docs/superpowers/specs/system-spec/README.md index 8e42c9be..cb5e8c2c 100644 --- a/docs/superpowers/specs/system-spec/README.md +++ b/docs/superpowers/specs/system-spec/README.md @@ -3,6 +3,9 @@ - Historical intake: 2026-10-31. Product baseline: `0fead2321bdef11c72b2746eb57f3a8b0e327c94` (Modelable 1.15.1). - Historical metamodel: system-specification `00188b037797fd37240dab9a0a11c431815e3ac9`; original schema retained as [schema-baseline.json](schema-baseline.json), original hashes/environment in [baseline.json](baseline.json). The manifest describes the original files at Modelable commit `5f48ed00`, not the migrated compilation/schema files. - Compilation characterization: Modelable `72de182a47e1c045f586be73a2c3a79b68f9130b` (1.15.2), capture validator `b187e43628c7dc89935d17c2c382094ad37eb2eb`. Current [schema.json](schema.json), pins/hashes in [adoption.json](adoption.json), and [current recovery checks](evidence/recovery-validation.json). Prior captures remain historical. +- Whole-product Level 3 **readiness record** (not accepted; release stage fails): [whole-product-level3.md](whole-product-level3.md). +- Whole-product Level 2 **draft** (not accepted): five pinned behaviors with evidence in [evidence/level2](evidence/level2), [decision record](whole-product-level2.md); validates at `verification`. +- Whole-product Level 1 **draft** (not accepted): [whole-product.yaml](whole-product.yaml), [decision record](whole-product-level1.md). - Status: whole-product inventory recorded; compilation behavior pinned for the bounded scope below, with explicit source/version and artifact bindings. Whole-product Levels 1–3 remain open. - Live onboarding TODO: inventory and bounded compilation discovery recorded; [dependency/state map](compilation-map.md) covers 141 source modules and 19 declared dataclass shapes. The two missing symlink cases now pass on Linux. Shared IR/schema semantics, public failure catalog and remaining recovery/transport coverage, classification, quality criteria, formal assessment and release review remain open. - This is internal development metadata. Product authority remains [architecture.md](../../../architecture.md), the existing capability catalog and native acceptance gates. The metadata changes no language, dependencies, installed skills or product commands. The accompanying native-gate repair moves graph controls above the canvas and makes browser characterization wait for the requested layout. @@ -92,6 +95,8 @@ system-spec --version system-spec docs/superpowers/specs/system-spec/inventory.yaml --stage inventory --check-artifacts --root . system-spec docs/superpowers/specs/system-spec/compilation.yaml --stage verification --check-artifacts --root . system-spec docs/superpowers/specs/system-spec/compilation-contract-proposal.yaml --stage architecture --check-artifacts --root . +system-spec docs/superpowers/specs/system-spec/whole-product.yaml --stage architecture --check-artifacts --root . +system-spec docs/superpowers/specs/system-spec/whole-product.yaml --stage verification --check-artifacts --root . system-spec docs/superpowers/specs/system-spec/compilation.yaml --context compilation-unit system-spec docs/superpowers/specs/system-spec/compilation.yaml --impact apply-compilation system-spec docs/superpowers/specs/system-spec/inventory.yaml --plan local-contract-toolchain diff --git a/docs/superpowers/specs/system-spec/browser-persistence-map.md b/docs/superpowers/specs/system-spec/browser-persistence-map.md new file mode 100644 index 00000000..45e81152 --- /dev/null +++ b/docs/superpowers/specs/system-spec/browser-persistence-map.md @@ -0,0 +1,47 @@ +# Browser persistence map (bounded) + +- Source: branch `fix/conversation-preview-operational-errors` at `e78a03be`; read from `web/src/{workspace-repository,usePersistentWorkspace,workspace,theme,sw-registration}.ts(x)`, `web/src/App.tsx` (repository wiring), `web/vite.config.ts` and `docs/playground-design.md` §15–16. Observed behavior only; no tests or browser runs were performed for this map. +- Authority: the existing playground design doc, source and native gates. This extends the [inventory](inventory.yaml) "Playground" row; it changes no contract. +- **Not mapped:** the Pyodide worker's in-memory state, the AI/WebLLM session and model-download state (`web/src/ai/**`), and the browser DTO/protocol schemas. Their lifetimes remain open. + +## Persistent stores + +| Store | Owner | Contents / lifetime | +|---|---|---| +| IndexedDB `modelable-playground`, version 1, object store `workspaces` (keyPath `id`) | `IndexedDbWorkspaceRepository` | One `PlaygroundWorkspace` per id: `schemaVersion` (1), `id`, `revision`, `files[] {path, content, version}`, `activeFile`, optional `metadata.lastAiAccept {provider, model, timestamp}`. Source of truth for user source; survives reloads. | +| `localStorage` key `modelable:theme` | `theme.ts` | `'light'` or `'dark'`; absence means `system`. Reads/writes are wrapped in try/catch (storage may be disabled). | +| Service worker + Workbox precache | `vite-plugin-pwa` in `vite.config.ts` | `registerType: 'autoUpdate'`, scope `/modelable/playground/`; precaches `js, css, html, wasm, mjs, zip, json, whl, ttf, woff, woff2, png` (excluding `fixtures/**`, files up to 30 MB), navigate fallback to `index.html`. Holds app and Pyodide assets, not user data. | + +Derived results (compiled artifacts, diagnostics, graph) are memory-only; the design doc says the same (§ around line 1041). + +## Repository protocol + +| Operation | Observed behavior | +|---|---| +| `load(id)` | Readonly transaction. `missing` if absent; `ready` with the parsed workspace; `recovery-required` (`invalid` or `incompatible`, carrying the raw record) when `parseWorkspaceRecord` throws `WorkspaceValidationError`. Other errors propagate. Unsupported `schemaVersion` -> `incompatible`. | +| `save(workspace)` | Readwrite transaction; reads the stored record and returns `'stale'` without writing only if the stored `revision` is **greater** than the one being saved. Equal or lower stored revision is overwritten. Writes a `structuredClone`. | +| `remove(id)` | Deletes the record. | +| Schema upgrade | `onupgradeneeded` creates the `workspaces` store if missing. There is no migration path beyond version 1; a different stored `schemaVersion` is surfaced for recovery rather than migrated. | + +## Hook protocol (`usePersistentWorkspace`) + +- Phases: `restoring`, `saving`, `saved`, `memory-only`, `recovery-required`. +- On mount: `load(default id)`; `missing` -> adopt the default workspace and save immediately; `recovery-required` -> hold the raw record and block normal editing; load rejection -> `memory-only`. +- Edits: set dirty, debounce 300 ms, then save; a monotonic sequence number and the current revision gate the `saved` transition so a late older save cannot mark a newer edit as saved. +- `pagehide` with unsaved changes triggers an un-awaited save. +- Save rejection (including IndexedDB unavailable) -> `memory-only`; no automatic retry was found. + +## Observations for follow-up (from reading source, not confirmed by tests) + +- **`'stale'` result is ignored.** The hook awaits `repository.save(snapshot)` without inspecting its return value, so a `'stale'` result is treated the same as `'saved'` (phase becomes `saved` if the in-memory revision still matches). With two tabs on the same workspace id, the lower-revision tab's save is rejected by the repository but shown as saved. No test in `usePersistentWorkspace.test.tsx` references a `'stale'` save result (grep); repository-level behavior is tested in `workspace-repository.test.ts`. Maintainers should decide the intended UI state before treating this as a defect. +- **Equal-revision overwrite.** Two tabs at the same revision overwrite each other; there is no cross-tab notification (grep found no `BroadcastChannel` or `storage` listener in `web/src`). +- **Unmount drops a pending debounce.** The effect cleanup clears the timer without flushing; only `pagehide` flushes. An unmount that is not a page unload would lose the last debounced edit. +- **`pagehide` save is best effort.** The IndexedDB write is not awaited by the browser lifecycle, so completion is not guaranteed. +- **Design-doc drift.** `docs/playground-design.md` lists IndexedDB stores for editor state, cached compiler metadata, graph layouts and model download state; the only store in code is `workspaces`. Record as an as-is discrepancy rather than a missing requirement until maintainers confirm which is authoritative. +- **Service-worker update safety.** The design doc requires that an update must not silently invalidate unsaved state; the config uses `autoUpdate`. Whether an update reloads the page while the workspace is dirty was not verified here. +- **Secrets.** `metadata.lastAiAccept` stores provider/model names only; the design doc forbids secrets in IndexedDB/`localStorage`. No secret storage was found in the files read, but `web/src/ai/**` was not searched exhaustively beyond a storage-API grep, which found none. + +## Disposition + +- Accepted as a bounded observed map of workspace persistence. Classification of stored data remains open: workspace content is user source text and should be treated as at least the compilation DTOs' provisional `restricted` handling; this is not an observed product classification. +- Candidate follow-ups for maintainers to schedule: a test and decision for handling `'stale'` saves; a decision on cross-tab behavior; confirmation of the service-worker update/dirty-state behavior; reconciling the design doc's store list with the code. diff --git a/docs/superpowers/specs/system-spec/compilation-map.md b/docs/superpowers/specs/system-spec/compilation-map.md index 67a4d06f..bee8c150 100644 --- a/docs/superpowers/specs/system-spec/compilation-map.md +++ b/docs/superpowers/specs/system-spec/compilation-map.md @@ -64,6 +64,7 @@ Direct and conversational policies differ. Direct path mapping preserves the exi - Compensation restores backups/removes newly written files where possible. Errors and preserved backups are reported. Cleanup can leave quarantined `.modelable-cleanup-*` files or released-lock artifacts; they are operational recovery state, not accepted product output. - These are multiple per-file replacements with compensation. No durable multi-file commit journal or crash-atomicity proof is asserted. PID-based stale-lock reclamation is observed behavior, not formal assurance against every crash/race scenario. - `LockContentionError` and `RegistryIdLockContentionError`, plus lower-level filesystem failures, can cross helper boundaries beyond the short service exception list in the original specification. Complete adapter translation/error-catalog review remains under MOD-COMP-09; this map does not silently redefine the frozen contract or claim those cases are covered by the original characterization record. +- Conversation preview (`filesystem_conversation.py`) now returns a `kind="error"` reply for `LockContentionError`, `RegistryIdLockContentionError` and `OSError`, keeping any pending action; characterized in `cli/tests/test_conversation_preview_recovery.py`. Apply already caught all exceptions. The service contract and other adapters (LSP wire, editor) are unchanged; this is not a full error-catalog closure. - Formal applicability remains open for lock ordering, freshness under contention, rollback and crash windows. Existing unit tests are supporting behavior evidence; this source map is not a proof. ## Symlink coverage decision @@ -81,4 +82,6 @@ To reproduce, create a fresh temporary build context, extract `git -c core.autoc - Archive the merged [migration plan](../../plans/archived/system-spec-evidence-migration.md); the ongoing onboarding specification stays active. - Accept this bounded observed dependency/state map and the suitable-host execution of MOD-COMP-10 as supporting evidence. Preserve the original capability/data contracts and the existing category waiver. - Keep whole-product architecture/release open. MOD-COMP-09 still owns measured performance/scalability/observability requirements, complete public error/failure review, transitive IR/schema semantics and formal applicability. Provisional classification review is also open. +- Browser workspace persistence is mapped in [browser-persistence-map.md](browser-persistence-map.md). +- Registry transport, ledger and lock protocols are mapped in [registry-protocol-map.md](registry-protocol-map.md). - Next bounded review: reconcile the public error catalog and lock/compensation obligations, then map shared registry protocols and browser persistence against their existing authorities. Maintainers own acceptance and remediation scheduling. diff --git a/docs/superpowers/specs/system-spec/evidence/formal/A_no_faults.cfg b/docs/superpowers/specs/system-spec/evidence/formal/A_no_faults.cfg new file mode 100644 index 00000000..185e907e --- /dev/null +++ b/docs/superpowers/specs/system-spec/evidence/formal/A_no_faults.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +CONSTANTS RollbackMayFail = FALSE CanCrash = FALSE +INVARIANTS PromotionExclusive LocksHeldByActive FilesConsistent NoLostUpdate diff --git a/docs/superpowers/specs/system-spec/evidence/formal/B_rollback_may_fail.cfg b/docs/superpowers/specs/system-spec/evidence/formal/B_rollback_may_fail.cfg new file mode 100644 index 00000000..43ecad30 --- /dev/null +++ b/docs/superpowers/specs/system-spec/evidence/formal/B_rollback_may_fail.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +CONSTANTS RollbackMayFail = TRUE CanCrash = FALSE +INVARIANTS FilesConsistent diff --git a/docs/superpowers/specs/system-spec/evidence/formal/C_crash.cfg b/docs/superpowers/specs/system-spec/evidence/formal/C_crash.cfg new file mode 100644 index 00000000..f819cd93 --- /dev/null +++ b/docs/superpowers/specs/system-spec/evidence/formal/C_crash.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +CONSTANTS RollbackMayFail = FALSE CanCrash = TRUE +INVARIANTS FilesConsistent diff --git a/docs/superpowers/specs/system-spec/evidence/formal/CompilationProtocol.tla b/docs/superpowers/specs/system-spec/evidence/formal/CompilationProtocol.tla new file mode 100644 index 00000000..1567ff7f --- /dev/null +++ b/docs/superpowers/specs/system-spec/evidence/formal/CompilationProtocol.tla @@ -0,0 +1,134 @@ +---------------------------- MODULE CompilationProtocol ---------------------------- +(* Bounded abstraction of the observed compilation promotion protocol. + Sources: cli/src/modelable/operations/compilation.py (execute_direct, apply, + _verify_freshness), file_transaction.py (workspace lock, per-file promotion, + compensation) and registry/ids.py (ledger lock). Two processes: "d" runs a + direct compilation, "a" applies a previously previewed compilation. + + Abstractions (assumptions, not code facts): + - Two destination files stand for the ledger and artifact destinations; a + file is a version number. + - The registry-ID and enum-number ledger locks are one ordered pair. Apply + takes only the ID lock (compilation.py apply); direct takes ID then enum. + - Apply's freshness check runs once under the ID lock and again under the + workspace lock (validate callback); both compare every destination with + the preview snapshot. + - A process crash releases its locks (stale-lock reclamation by PID + liveness is assumed to complete) and leaves promoted files in place: the + implementation has no commit journal. + - Rollback restores the previous version of every promoted file; when + RollbackMayFail it may skip a file. + Not modeled: staging, hashes, permissions, audit file, cleanup errors, + timeouts, more than two processes, PID reuse. *) +EXTENDS Naturals, FiniteSets + +CONSTANTS RollbackMayFail, CanCrash + +Procs == {"d", "a"} +Files == {1, 2} +NoOne == "none" +Terminal == {"committed", "rolledBack", "rejected", "crashed"} + +VARIABLES pc, idLock, enumLock, wsLock, disk, base, todo, done, rbFailed + +vars == <> + +Init == + /\ pc = [p \in Procs |-> "start"] + /\ idLock = NoOne /\ enumLock = NoOne /\ wsLock = NoOne + /\ disk = [f \in Files |-> 0] + /\ base = [p \in Procs |-> [f \in Files |-> 0]] + /\ todo = [p \in Procs |-> {}] + /\ done = [p \in Procs |-> {}] + /\ rbFailed = FALSE + +Release(p) == + /\ idLock' = IF idLock = p THEN NoOne ELSE idLock + /\ enumLock' = IF enumLock = p THEN NoOne ELSE enumLock + /\ wsLock' = IF wsLock = p THEN NoOne ELSE wsLock + +SetPc(p, v) == pc' = [pc EXCEPT ![p] = v] + +\* ---- direct compilation: ID lock, enum lock, workspace lock ---- +DAcqId == pc["d"] = "start" /\ idLock = NoOne + /\ idLock' = "d" /\ SetPc("d", "hasId") + /\ UNCHANGED <> +DAcqEnum == pc["d"] = "hasId" /\ enumLock = NoOne + /\ enumLock' = "d" /\ SetPc("d", "hasBoth") + /\ base' = [base EXCEPT !["d"] = disk] \* reads current state under both ledger locks + /\ UNCHANGED <> +DAcqWs == pc["d"] = "hasBoth" /\ wsLock = NoOne + /\ wsLock' = "d" /\ SetPc("d", "promote") + /\ todo' = [todo EXCEPT !["d"] = Files] /\ done' = [done EXCEPT !["d"] = {}] + /\ UNCHANGED <> + +\* ---- apply: ID lock, freshness check, workspace lock, freshness check ---- +AAcqId == pc["a"] = "start" /\ idLock = NoOne + /\ idLock' = "a" /\ SetPc("a", "hasId") + /\ UNCHANGED <> +ACheck1 == pc["a"] = "hasId" + /\ (IF disk = base["a"] + THEN SetPc("a", "fresh1") /\ UNCHANGED <> + ELSE SetPc("a", "rejected") /\ Release("a")) + /\ UNCHANGED <> +AAcqWs == pc["a"] = "fresh1" /\ wsLock = NoOne + /\ wsLock' = "a" /\ SetPc("a", "fresh2") + /\ UNCHANGED <> +ACheck2 == pc["a"] = "fresh2" + /\ (IF disk = base["a"] + THEN /\ SetPc("a", "promote") /\ UNCHANGED <> + /\ todo' = [todo EXCEPT !["a"] = Files] /\ done' = [done EXCEPT !["a"] = {}] + ELSE /\ SetPc("a", "rejected") /\ Release("a") /\ UNCHANGED <>) + /\ UNCHANGED <> + +\* ---- promotion, failure, compensation (shared) ---- +Promote(p) == pc[p] = "promote" /\ todo[p] # {} + /\ \E f \in todo[p] : + /\ disk' = [disk EXCEPT ![f] = base[p][f] + 1] + /\ todo' = [todo EXCEPT ![p] = @ \ {f}] + /\ done' = [done EXCEPT ![p] = @ \cup {f}] + /\ UNCHANGED <> +Commit(p) == pc[p] = "promote" /\ todo[p] = {} + /\ SetPc(p, "committed") /\ Release(p) + /\ UNCHANGED <> +Fail(p) == pc[p] = "promote" /\ todo[p] # {} \* a failure_mode raised before the last file + /\ SetPc(p, "rollback") + /\ UNCHANGED <> +Rollback(p) == pc[p] = "rollback" /\ done[p] # {} + /\ \E f \in done[p] : + /\ done' = [done EXCEPT ![p] = @ \ {f}] + /\ IF RollbackMayFail + THEN \/ (disk' = [disk EXCEPT ![f] = base[p][f]] /\ UNCHANGED rbFailed) + \/ (UNCHANGED disk /\ rbFailed' = TRUE) + ELSE disk' = [disk EXCEPT ![f] = base[p][f]] /\ UNCHANGED rbFailed + /\ UNCHANGED <> +RolledBack(p) == pc[p] = "rollback" /\ done[p] = {} + /\ SetPc(p, "rolledBack") /\ Release(p) + /\ UNCHANGED <> +Crash(p) == CanCrash /\ pc[p] = "promote" + /\ SetPc(p, "crashed") /\ Release(p) + /\ UNCHANGED <> + +Terminated == /\ \A p \in Procs : pc[p] \in Terminal + /\ UNCHANGED vars + +Next == + \/ DAcqId \/ DAcqEnum \/ DAcqWs \/ AAcqId \/ ACheck1 \/ AAcqWs \/ ACheck2 + \/ \E p \in Procs : Promote(p) \/ Commit(p) \/ Fail(p) \/ Rollback(p) \/ RolledBack(p) \/ Crash(p) + \/ Terminated + +Spec == Init /\ [][Next]_vars + +\* ---- properties, one per contract clause ---- +\* Workspace promotion is exclusive (file_transaction workspace lock). +PromotionExclusive == Cardinality({p \in Procs : pc[p] \in {"promote", "rollback"}}) <= 1 +\* Lock holders are always live, non-terminated processes unless crashed processes released them. +LocksHeldByActive == + \A l \in {idLock, enumLock, wsLock} : l = NoOne \/ pc[l] \notin Terminal +Quiescent == \A p \in Procs : pc[p] \notin {"promote", "rollback"} +Faulted == rbFailed \/ (\E p \in Procs : pc[p] = "crashed") +CommitCount == Cardinality({p \in Procs : pc[p] = "committed"}) +\* Without crashes or failed compensation, files move together and no committed update is lost. +FilesConsistent == Quiescent => disk[1] = disk[2] +NoLostUpdate == (Quiescent /\ ~Faulted) => (disk[1] = CommitCount /\ disk[2] = CommitCount) +================================================================================== diff --git a/docs/superpowers/specs/system-spec/evidence/formal/D_all_faults_safety.cfg b/docs/superpowers/specs/system-spec/evidence/formal/D_all_faults_safety.cfg new file mode 100644 index 00000000..ff5f366b --- /dev/null +++ b/docs/superpowers/specs/system-spec/evidence/formal/D_all_faults_safety.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +CONSTANTS RollbackMayFail = TRUE CanCrash = TRUE +INVARIANTS PromotionExclusive LocksHeldByActive NoLostUpdate diff --git a/docs/superpowers/specs/system-spec/evidence/formal/tlc-output.txt b/docs/superpowers/specs/system-spec/evidence/formal/tlc-output.txt new file mode 100644 index 00000000..46bde208 --- /dev/null +++ b/docs/superpowers/specs/system-spec/evidence/formal/tlc-output.txt @@ -0,0 +1,192 @@ +tla2tools.jar v1.7.4 sha256 936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88; java openjdk version "25.0.5.0.2" 2026-10-22 LTS +##### A_no_faults.cfg (expected: no error) +Model checking completed. No error has been found. + Estimates of the probability that TLC did not check all reachable states + because two distinct states had the same fingerprint: + calculated (optimistic): val = 2.7E-16 +171 states generated, 133 distinct states found, 0 states left on queue. +The depth of the complete state graph search is 16. +The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 3 and the 95th percentile is 3). +Finished in 00s at (2026-11-04 20:27:23) +##### B_rollback_may_fail.cfg (expected: FilesConsistent violated) +Error: Invariant FilesConsistent is violated. +Error: The behavior up to this point is: +State 1: +/\ rbFailed = FALSE +/\ wsLock = "none" +/\ done = [a |-> {}, d |-> {}] +/\ todo = [a |-> {}, d |-> {}] +/\ idLock = "none" +/\ base = [a |-> <<0, 0>>, d |-> <<0, 0>>] +/\ pc = [a |-> "start", d |-> "start"] +/\ disk = <<0, 0>> +/\ enumLock = "none" + +State 2: +/\ rbFailed = FALSE +/\ wsLock = "none" +/\ done = [a |-> {}, d |-> {}] +/\ todo = [a |-> {}, d |-> {}] +/\ idLock = "d" +/\ base = [a |-> <<0, 0>>, d |-> <<0, 0>>] +/\ pc = [a |-> "start", d |-> "hasId"] +/\ disk = <<0, 0>> +/\ enumLock = "none" + +State 3: +/\ rbFailed = FALSE +/\ wsLock = "none" +/\ done = [a |-> {}, d |-> {}] +/\ todo = [a |-> {}, d |-> {}] +/\ idLock = "d" +/\ base = [a |-> <<0, 0>>, d |-> <<0, 0>>] +/\ pc = [a |-> "start", d |-> "hasBoth"] +/\ disk = <<0, 0>> +/\ enumLock = "d" + +State 4: +/\ rbFailed = FALSE +/\ wsLock = "d" +/\ done = [a |-> {}, d |-> {}] +/\ todo = [a |-> {}, d |-> {1, 2}] +/\ idLock = "d" +/\ base = [a |-> <<0, 0>>, d |-> <<0, 0>>] +/\ pc = [a |-> "start", d |-> "promote"] +/\ disk = <<0, 0>> +/\ enumLock = "d" + +State 5: +/\ rbFailed = FALSE +/\ wsLock = "d" +/\ done = [a |-> {}, d |-> {1}] +/\ todo = [a |-> {}, d |-> {2}] +/\ idLock = "d" +/\ base = [a |-> <<0, 0>>, d |-> <<0, 0>>] +/\ pc = [a |-> "start", d |-> "promote"] +/\ disk = <<1, 0>> +/\ enumLock = "d" + +State 6: +/\ rbFailed = FALSE +/\ wsLock = "d" +/\ done = [a |-> {}, d |-> {1}] +/\ todo = [a |-> {}, d |-> {2}] +/\ idLock = "d" +/\ base = [a |-> <<0, 0>>, d |-> <<0, 0>>] +/\ pc = [a |-> "start", d |-> "rollback"] +/\ disk = <<1, 0>> +/\ enumLock = "d" + +State 7: +/\ rbFailed = TRUE +/\ wsLock = "d" +/\ done = [a |-> {}, d |-> {}] +/\ todo = [a |-> {}, d |-> {2}] +/\ idLock = "d" +/\ base = [a |-> <<0, 0>>, d |-> <<0, 0>>] +/\ pc = [a |-> "start", d |-> "rollback"] +/\ disk = <<1, 0>> +/\ enumLock = "d" + +State 8: +/\ rbFailed = TRUE +/\ wsLock = "none" +/\ done = [a |-> {}, d |-> {}] +/\ todo = [a |-> {}, d |-> {2}] +/\ idLock = "none" +/\ base = [a |-> <<0, 0>>, d |-> <<0, 0>>] +/\ pc = [a |-> "start", d |-> "rolledBack"] +/\ disk = <<1, 0>> +/\ enumLock = "none" + +33 states generated, 31 distinct states found, 9 states left on queue. +The depth of the complete state graph search is 8. +The average outdegree of the complete state graph is 1 (minimum is 1, the maximum 3 and the 95th percentile is 3). +Finished in 00s at (2026-11-04 20:27:24) +##### C_crash.cfg (expected: FilesConsistent violated) +Error: Invariant FilesConsistent is violated. +Error: The behavior up to this point is: +State 1: +/\ rbFailed = FALSE +/\ wsLock = "none" +/\ done = [a |-> {}, d |-> {}] +/\ todo = [a |-> {}, d |-> {}] +/\ idLock = "none" +/\ base = [a |-> <<0, 0>>, d |-> <<0, 0>>] +/\ pc = [a |-> "start", d |-> "start"] +/\ disk = <<0, 0>> +/\ enumLock = "none" + +State 2: +/\ rbFailed = FALSE +/\ wsLock = "none" +/\ done = [a |-> {}, d |-> {}] +/\ todo = [a |-> {}, d |-> {}] +/\ idLock = "d" +/\ base = [a |-> <<0, 0>>, d |-> <<0, 0>>] +/\ pc = [a |-> "start", d |-> "hasId"] +/\ disk = <<0, 0>> +/\ enumLock = "none" + +State 3: +/\ rbFailed = FALSE +/\ wsLock = "none" +/\ done = [a |-> {}, d |-> {}] +/\ todo = [a |-> {}, d |-> {}] +/\ idLock = "d" +/\ base = [a |-> <<0, 0>>, d |-> <<0, 0>>] +/\ pc = [a |-> "start", d |-> "hasBoth"] +/\ disk = <<0, 0>> +/\ enumLock = "d" + +State 4: +/\ rbFailed = FALSE +/\ wsLock = "d" +/\ done = [a |-> {}, d |-> {}] +/\ todo = [a |-> {}, d |-> {1, 2}] +/\ idLock = "d" +/\ base = [a |-> <<0, 0>>, d |-> <<0, 0>>] +/\ pc = [a |-> "start", d |-> "promote"] +/\ disk = <<0, 0>> +/\ enumLock = "d" + +State 5: +/\ rbFailed = FALSE +/\ wsLock = "d" +/\ done = [a |-> {}, d |-> {1}] +/\ todo = [a |-> {}, d |-> {2}] +/\ idLock = "d" +/\ base = [a |-> <<0, 0>>, d |-> <<0, 0>>] +/\ pc = [a |-> "start", d |-> "promote"] +/\ disk = <<1, 0>> +/\ enumLock = "d" + +State 6: +/\ rbFailed = FALSE +/\ wsLock = "none" +/\ done = [a |-> {}, d |-> {1}] +/\ todo = [a |-> {}, d |-> {2}] +/\ idLock = "none" +/\ base = [a |-> <<0, 0>>, d |-> <<0, 0>>] +/\ pc = [a |-> "start", d |-> "crashed"] +/\ disk = <<1, 0>> +/\ enumLock = "none" + +15 states generated, 15 distinct states found, 6 states left on queue. +The depth of the complete state graph search is 6. +The average outdegree of the complete state graph is 2 (minimum is 1, the maximum 4 and the 95th percentile is 4). +Finished in 00s at (2026-11-04 20:27:25) +##### D_all_faults_safety.cfg (expected: no error) +Model checking completed. No error has been found. + Estimates of the probability that TLC did not check all reachable states + because two distinct states had the same fingerprint: + calculated (optimistic): val = 3.2E-15 +530 states generated, 368 distinct states found, 0 states left on queue. +The depth of the complete state graph search is 16. +The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 4 and the 95th percentile is 3). +Finished in 00s at (2026-11-04 20:27:26) +##### Sanity probes (manual, temporary invariants appended to a temp copy; outputs not retained) +- config A with Probe == pc["a"] # "committed": violated (apply can commit) +- config A with Probe == pc["a"] # "rejected": violated (stale apply is rejected) +- config A with Probe == pc["d"] # "committed": violated (direct can commit) +- mutant with both apply freshness checks replaced by TRUE, invariant NoLostUpdate: violated (the property detects a missing freshness check) diff --git a/docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt b/docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt new file mode 100644 index 00000000..c69fe032 --- /dev/null +++ b/docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt @@ -0,0 +1,11 @@ +........................................................................ [ 23%] +....................................................................s... [ 47%] +........................................................................ [ 71%] +...........................................................sss.......... [ 94%] +.RR............... [100%] +=========================== short test summary info =========================== +SKIPPED [1] tests\test_lsp_conversation_service.py:486: platform cannot create symlinks: [WinError 1314] A required privilege is not held by the client: 'C:\\Users\\ktjn\\AppData\\Local\\Temp\\tmp.itZCJ4Zhmx\\pt\\test_registry_rejects_symlinke0\\outside-docs.json' -> 'C:\\Users\\ktjn\\AppData\\Local\\Temp\\tmp.itZCJ4Zhmx\\pt\\test_registry_rejects_symlinke0\\workspace\\docs-index\\docs\\outside-link.json' +SKIPPED [1] tests\test_file_transaction.py:290: POSIX file metadata semantics +SKIPPED [1] tests\test_file_transaction.py:308: POSIX file metadata semantics +SKIPPED [1] tests\test_file_transaction.py:333: POSIX file metadata semantics +300 passed, 4 skipped, 2 rerun in 52.51s diff --git a/docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml b/docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml new file mode 100644 index 00000000..2ad353a8 --- /dev/null +++ b/docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml @@ -0,0 +1 @@ +C:\git\modelable\cli\tests\test_lsp_conversation_service.py:486: platform cannot create symlinks: [WinError 1314] A required privilege is not held by the client: 'C:\\Users\\ktjn\\AppData\\Local\\Temp\\tmp.itZCJ4Zhmx\\pt\\test_registry_rejects_symlinke0\\outside-docs.json' -> 'C:\\Users\\ktjn\\AppData\\Local\\Temp\\tmp.itZCJ4Zhmx\\pt\\test_registry_rejects_symlinke0\\workspace\\docs-index\\docs\\outside-link.json'C:\git\modelable\cli\tests\test_file_transaction.py:290: POSIX file metadata semanticsC:\git\modelable\cli\tests\test_file_transaction.py:308: POSIX file metadata semanticsC:\git\modelable\cli\tests\test_file_transaction.py:333: POSIX file metadata semantics \ No newline at end of file diff --git a/docs/superpowers/specs/system-spec/evidence/level2/web-level2.txt b/docs/superpowers/specs/system-spec/evidence/level2/web-level2.txt new file mode 100644 index 00000000..04c879c2 --- /dev/null +++ b/docs/superpowers/specs/system-spec/evidence/level2/web-level2.txt @@ -0,0 +1,9 @@ + + RUN v4.1.10 C:/git/modelable/web + + + Test Files 4 passed (4) + Tests 24 passed (24) + Start at 20:16:37 + Duration 3.19s (transform 135ms, setup 104ms, import 1.12s, tests 405ms, environment 4.11s) + diff --git a/docs/superpowers/specs/system-spec/registry-protocol-map.md b/docs/superpowers/specs/system-spec/registry-protocol-map.md new file mode 100644 index 00000000..fba94ca1 --- /dev/null +++ b/docs/superpowers/specs/system-spec/registry-protocol-map.md @@ -0,0 +1,40 @@ +# Registry shared-protocol map (bounded) + +- Source: branch `fix/conversation-preview-operational-errors` on `b6176914`; read from `cli/src/modelable/registry/{base,factory,local,oci,ids,enum_numbers,index}.py`, `schema.sql` and `operations/compilation.py`. Observed behavior only; no tests were run for this map. +- Authority: existing source, [architecture](../../../architecture.md) and native gates. This extends the [compilation map](compilation-map.md); it does not change any frozen contract. +- **Not mapped:** `snapshot.py` (2704 lines), `resolver.py`, `usage*.py`, `apicurio.py`, `openlineage.py`, `sources.py`, `signature.py`. Snapshot, usage and external-publication protocols remain open. + +## Registry transport (index push/pull) + +| Piece | Observed behavior | +|---|---| +| `Registry` (ABC, `base.py`) | `push(registry_path)` / `pull(dest_path)` of a registry index file. | +| `get_registry` (`factory.py`) | `oci://` prefix -> `OCIRegistry`; anything else -> `LocalRegistry(Path)`. | +| `LocalRegistry` | `push`: creates parent dirs, `copy2` unless source and destination resolve identically. `pull`: `copy2` unless identical. Plain copy: no lock, no temp-file-and-replace, no hash check. | +| `OCIRegistry` | Both operations raise `OCIRegistryError` ("not implemented"). Consistent with the compilation map: no remote OCI commit exists to roll back. | + +## Local state owned by the registry package + +| State | Writer | Notes | +|---|---|---| +| `registry.db` (SQLite) | `build_registry` in `index.py` | Rebuildable index: deletes any existing file, runs `schema.sql` (15 tables incl. `registry_ids`), inserts workspace content, commits. Not incremental; not guarded by `RegistryIdLock`. | +| Registry-ID ledger (JSON `name -> int`) | `write_lock_file` in `ids.py` | Temp file in same dir, `fsync`, `os.replace`. IDs are never reassigned or reused; orphaned IDs raise `ValueError` unless `allow_orphaned`. | +| Enum-number ledger (JSON, per-declaration members + reservations) | `write_lock_file` in `enum_numbers.py` | Same temp/fsync/replace pattern. Removed members become reservations; a reappearing removed name raises `EnumNumberConflictError`. | +| Ledger lock (`..lock`) | `RegistryIdLock` in `ids.py` | `O_CREAT|O_EXCL` file holding the PID; polls every 10 ms up to 30 s, then `RegistryIdLockContentionError`. Stale locks reclaimed when the recorded PID is not alive (Windows `OpenProcess`/`GetExitCodeProcess`, POSIX `kill(pid, 0)`). Release retries `unlink` 20 times, then renames to `.released-` and deletes best-effort. | + +`RegistryIdLock` is a generic per-path lock despite its name; compilation uses it for both ledgers. + +## Observations relevant to MOD-COMP-09 formal review + +These are observations from reading source, not defects confirmed by a test. + +- **Lock asymmetry.** `execute_direct` (`compilation.py:285-288`) holds the registry-ID lock then the enum-number lock. `apply` (`compilation.py:507`) holds only the registry-ID lock; ID-ledger freshness is checked by equality with `registry_ids_before`, and other files by `_verify_apply_freshness`. Whether enum-ledger changes during apply are always caught by that fingerprint check, and whether a concurrent direct run can interleave, needs targeted review or a model; the existing tests do not state it. +- **Lock order.** Only one order (ID, then enum) is observed in direct execution; no code path takes them in the reverse order. Workspace promotion lock (`.modelable/locks/compilation.lock`) is taken inside, via `FileTransaction`. Nesting order ID -> enum -> workspace is the candidate invariant. +- **PID-based reclamation.** A recycled PID can make a dead owner's lock look live (blocks until timeout); nothing in the code excludes a race where a stale lock is read, a new owner recreates it, and the old reader then unlinks the new lock. Both are crash/race windows, not proven. +- **Non-atomic index/transport.** `build_registry` unlinks the old `registry.db` before rebuilding, and `LocalRegistry` copies in place; an interrupted run can leave a missing or partial file. Not exercised by the compilation characterization. +- **Contention surface.** `RegistryIdLockContentionError` and `LockContentionError` are not in the frozen `failure_modes`; conversation preview now translates them (see the compilation map), while service contract and LSP wire behavior are unchanged. + +## Disposition + +- Accepted as a bounded observed map for the pieces compilation touches. Not accepted: snapshot, usage, resolver, Apicurio/OpenLineage and signature protocols; browser persistence (IndexedDB workspace, service worker) is the next map. +- Candidate follow-ups, for maintainers to schedule: a targeted test for enum-ledger change between preview and apply; a lock-order/freshness model under the formal-review requirement; a decision on atomic replace for `LocalRegistry.push` and `build_registry`. diff --git a/docs/superpowers/specs/system-spec/whole-product-level1.md b/docs/superpowers/specs/system-spec/whole-product-level1.md new file mode 100644 index 00000000..7da03b4b --- /dev/null +++ b/docs/superpowers/specs/system-spec/whole-product-level1.md @@ -0,0 +1,28 @@ +# Whole-product Level 1 draft (dependency and data mapping) + +- Date: 2026-11-04. Source: branch `fix/conversation-preview-operational-errors`, Modelable 1.15.2. Spec: [whole-product.yaml](whole-product.yaml); validates with `system-spec docs/superpowers/specs/system-spec/whole-product.yaml --stage architecture --check-artifacts --root .`. +- Status: **draft for maintainer review.** Level 1 is not accepted. The inventory ([inventory.yaml](inventory.yaml)) stays the Level 0 record; the compilation slice stays in [compilation.yaml](compilation.yaml) and is not duplicated. + +## What the draft records + +| Area | Disposition | +|---|---| +| Capabilities and components | The six inventory components with observed `provides`/`requires` only. Cross-component capabilities carry minimal interfaces (Python API, stdio JSON-RPC, browser dispatch). | +| Data models | Seven models with owners: registry ID ledger, enum-number ledger, registry index DB, snapshot, usage manifest (semantic-toolchain); workspace record, theme preference (browser-playground). Fields come from [registry-protocol-map.md](registry-protocol-map.md), [browser-persistence-map.md](browser-persistence-map.md) and source. | +| Lineage | Only `registry-index-db` derived from `registry-id-ledger` (the index inserts the IDs). Other lineage not traced. | +| Classification | Provisional and conservative (`restricted`; `internal` for the theme flag), each tied to active requirement MOD-ADOPT-03. Not observed product classifications. | +| Boundary waiver | `semantic-toolchain` is a coarse boundary spanning seven source trees and keeps a `max_owns_data: 5` override, with risk `coarse-toolchain-boundary` waiving `context-budget` until release (MOD-ADOPT-04). | + +## Known gaps (recorded, not hidden) + +- `usage-manifest` and `registry-snapshot` fields are minimal: only the protocol name and snapshot paths were read. `snapshot.py`, resolver, usage graph, Apicurio, OpenLineage, Git source and signature protocols are not mapped in detail. +- Pyodide worker state, AI provider/WebLLM state and model-download state are not modeled as data. +- No external-provider components were declared: external endpoints stay as `external_sources` because no configured endpoint was exercised. OCI is listed as an external source although implementation raises "not implemented". +- No evidence is bound (`evidence: []`); characterization beyond compilation is MOD-ADOPT-02. +- Release-stage diagnostics fail as expected: no requirements per capability, eight missing verification categories, statuses below `verified`. +- Capability pre/post/invariants were written from the maps and tests already cited; they are descriptions, not verified contracts. + +## Decision + +- **Defer** Level 1 acceptance to maintainers. Do not advance to Level 2/3 for the whole product. +- Observed dependency wiring comes from the inventory; running `--check-drift` reports no drift, but it can miss absolute imports rooted at `cli/src` (see the toolkit upgrade note), so it is not dependency closure. diff --git a/docs/superpowers/specs/system-spec/whole-product-level2.md b/docs/superpowers/specs/system-spec/whole-product-level2.md new file mode 100644 index 00000000..63491a75 --- /dev/null +++ b/docs/superpowers/specs/system-spec/whole-product-level2.md @@ -0,0 +1,40 @@ +# Whole-product Level 2 draft (behavioral pinning) + +- Date: 2026-11-04. Source revision for all evidence: `dbd8807977bafdfdd4981596045a2cbdaab12efb` (clean tree). Spec: [whole-product.yaml](whole-product.yaml) validates at `--stage verification --check-artifacts --root .`. +- Status: **draft for maintainer review; Level 2 is not accepted.** This pins five narrow behaviors, not whole-product conformance. + +## Runs ([evidence/level2](evidence/level2)) + +| Suite | Result | Output | +|---|---|---| +| Python: 13 test modules across browser API/conformance/conversation, LSP conversation/integration/server, CLI compile/errors, registry IDs, file transaction, preview recovery (`-n 0`) | 300 passed, 4 skipped, 2 reruns | [txt](evidence/level2/python-level2.txt), [JUnit](evidence/level2/python-level2.xml) | +| Web (vitest): workspace repository, persistent-workspace hook, workspace model, recovery UI | 24 passed, 4 files | [txt](evidence/level2/web-level2.txt) | + +- The 2 reruns come from the one `flaky`-marked case in `test_file_transaction.py` (project policy: pytest-rerunfailures with a recorded cause). No cited evidence record uses that test. +- The 4 skips are Windows symlink and POSIX-metadata cases; none is cited as passing evidence. +- Python 3.14.5, pytest 9.1.1, Node v26.13.0, vitest 4.1.10, Windows. No Linux or browser-engine run. + +## Pinned behaviors (one named test each) + +| Requirement | Capability | Test | +|---|---|---| +| MOD-PROD-01 | local-contract-toolchain | `test_registry_ids.py::test_allocate_never_reassigns_existing_ids` | +| MOD-PROD-02 | native-command-workflows | `test_cli_compilation_errors.py::test_compile_renders_known_operational_errors[ledger-lock]` | +| MOD-PROD-03 | desktop-language-and-conversation | `test_conversation_preview_recovery.py::test_wire_error_keeps_existing_pending_source_action` | +| MOD-PROD-04 | browser-compiler-api | `test_browser_conformance.py::test_native_browser_snapshots_are_deterministic` | +| MOD-PROD-05 | playground-workspace | `workspace-repository.test.ts` "a stale revision cannot overwrite a newer workspace" | + +Evidence binds each record to the capability source files it exercises plus the test and output hashes. A tampered source hash is rejected (probe: modifying the `workspace-repository.ts` digest fails the artifact check). + +## Gaps and waiver + +- **vscode-model-authoring has no passing evidence.** MOD-PROD-06 is `specified` with two criteria; the extension's tests need the VS Code extension host (`npm test` -> `runTests.js`), which was not run. +- **Not pinned:** the stale-save UI behavior found in the [browser map](browser-persistence-map.md) (hook ignores `'stale'`), cross-tab behavior, snapshot/usage/Apicurio/OpenLineage/Git protocols, real WebLLM chat (manual conformance per AGENTS.md), and live integrations. +- **Waiver:** risk `product-category-gap` waives `verification-category` until `verification`, mitigated by MOD-ADOPT-02. Missing categories: serialization, concurrency, performance, scalability, resilience, observability. It blocks release. +- **No compatibility baseline** (`--compat`) was run: the Level 1 spec has no earlier pinned version to compare against. +- Test names pinned are one per criterion; a passing suite count does not establish untested behavior. +- Release stage fails as expected: waiver expiry, six missing categories, unverified ADOPT requirements, statuses below `verified`. + +## Decision + +- **Defer** Level 2 acceptance to maintainers. Do not advance to Level 3. Next: run the extension-host tests, decide the `'stale'` save policy, then add concurrency/resilience characterization for registry locks and promotion. diff --git a/docs/superpowers/specs/system-spec/whole-product-level3.md b/docs/superpowers/specs/system-spec/whole-product-level3.md new file mode 100644 index 00000000..762e3475 --- /dev/null +++ b/docs/superpowers/specs/system-spec/whole-product-level3.md @@ -0,0 +1,43 @@ +# Whole-product Level 3 readiness (not accepted) + +- Date: 2026-11-04. Evidence source revision `dbd8807977bafdfdd4981596045a2cbdaab12efb`, reusing the [Level 2 run](evidence/level2/python-level2.txt) (300 passed, 4 skipped, 2 reruns from the flaky-marked case, which is not cited). Spec: [whole-product.yaml](whole-product.yaml) validates at `verification`; **`release` still fails.** + +## Progress in this step + +Three more requirements on `local-contract-toolchain`, each one named passing test with source-bound evidence (MOD-PROD-07..09): + +| Category | Test | +|---|---| +| serialization | `test_registry_ids.py::test_write_then_read_lock_file_round_trips_sorted_by_id` | +| concurrency | `test_registry_ids.py::test_registry_id_lock_serializes_processes` | +| resilience | `test_file_transaction.py::test_transaction_verifies_promoted_hash_and_rolls_back` | + +Release diagnostics dropped from six missing verification categories to three. `file_transaction.py` was added to the capability's source binding. + +## Remaining release blockers (from `--stage release`) + +| Blocker | Owner / needed | +|---|---| +| Missing categories: performance, scalability, observability | Maintainers define measurable targets; no measurements exist. Waiver `product-category-gap` (expires at `verification`) cannot remain at release. | +| Waiver `coarse-toolchain-boundary` (context-budget) | Discover finer `semantic-toolchain` boundaries (MOD-ADOPT-04). | +| MOD-ADOPT-01..04 and MOD-PROD-06 lack evidence | Complete discovery maps, classification review (MOD-ADOPT-03), VS Code extension-host tests. | +| Capability, component and system status below `verified` | Follows from the above. | + +## Not done, and why + +- **Formal model:** now done as a bounded TLC model; see the next section. Crash-atomicity and failed-compensation behavior are not guaranteed by the observed protocol. +- **Native and manual gates:** the full pre-push gate, `run_browser_playground.py`, and the manual real-model WebLLM chat conformance (needs WebGPU hardware) were not run. +- **Evidence strength:** each record is one test per criterion on Windows only; the concurrency test is a process-level lock test, not a proof of ordering or crash safety. +- **Product discrepancies still open:** playground hook ignores `'stale'` saves; apply holds only the registry-ID lock (see the [registry](registry-protocol-map.md) and [browser](browser-persistence-map.md) maps). + +## Formal model (TLA+ / TLC) + +- Files: [CompilationProtocol.tla](evidence/formal/CompilationProtocol.tla), four `.cfg` files and [tlc-output.txt](evidence/formal/tlc-output.txt) under `evidence/formal`. Tool: `tla2tools.jar` v1.7.4 (TLC 2.19, OpenJDK 25.0.5) downloaded from the `tlaplus/tlaplus` GitHub release into a directory outside the repository, size 2274532 bytes, SHA-256 `936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88` (the release publishes no digest, so this is a self-computed fingerprint, not a verified checksum). The jar is not committed. +- Model: two processes (direct, apply), two destination files, ID/enum/workspace locks, freshness checks, per-file promotion, failure and compensation, optional crash. Assumptions (abstractions, crash releases locks, rollback restores previous version) are in the module header. +- Results: config A (no faults) and D (compensation may fail and crash; safety invariants) pass, 171 and 530 states, no deadlock reported. Config B (compensation may fail) and C (crash mid-promotion) violate `FilesConsistent`: destination files can end in different versions. Reachability probes show apply can commit, be rejected, and direct can commit; a mutant with both freshness checks removed violates `NoLostUpdate`. +- Spec binding: MOD-PROD-10 (concurrency, `model-check`, passed) and MOD-PROD-11 (resilience, failing evidence, release blocker REQ-04) in [whole-product.yaml](whole-product.yaml). Risk `promotion-not-crash-atomic` tracks the gap. +- Reading: with locks as observed, a preview-based apply and a conflicting direct run cannot both commit in the bounded model; the earlier question about apply not holding the enum lock is covered because freshness compares every destination under the workspace lock. The model abstracts away code; a model pass is not proof of the implementation, and the freshness comparison was modeled from `_verify_freshness` as read, not run. + +## Decision + +- **Level 3 is not accepted and cannot be claimed.** Release needs zero waivers, all ten categories and `verified` statuses; three categories, two waivers and several requirements remain. diff --git a/docs/superpowers/specs/system-spec/whole-product.yaml b/docs/superpowers/specs/system-spec/whole-product.yaml new file mode 100644 index 00000000..9748be9c --- /dev/null +++ b/docs/superpowers/specs/system-spec/whole-product.yaml @@ -0,0 +1,531 @@ +# yaml-language-server: $schema=./schema.json +# Level 1 DRAFT: observed whole-product dependency and data mapping. Not an acceptance claim. +# Observed from source at Modelable 1.15.2 (branch fix/conversation-preview-operational-errors); +# see compilation-map.md, registry-protocol-map.md, browser-persistence-map.md, whole-product-level1.md. +# The bounded compilation slice stays in compilation.yaml and is not duplicated here. +system: + id: modelable-product + version: "1.15.2" + status: specified + external_sources: + - user-mdl-workspaces + - modelable-config-and-facet-sidecars + - local-registry-snapshots-and-locks + - optional-oci-registries + - optional-apicurio-json-schema-registry + - optional-marquez-lineage-endpoint + - optional-dbt-fhir-odcs-specifications + - optional-llm-provider-endpoints + - browser-local-workspace-storage +capabilities: + - id: local-contract-toolchain + version: "1.0" + status: specified + preconditions: [readable .mdl workspace supplied] + postconditions: [diagnostics, generated artifacts, plans and local registry state produced through the existing staging and promotion boundary] + invariants: [registry IDs and enum numbers are never reassigned or reused, OCI publication is unsupported and fails explicitly] + failure_modes: [CompilationError, CompilationDiagnosticsError, FileTransactionError, FileTransactionCommittedError, LockContentionError, RegistryIdLockContentionError, OCIRegistryError] + interface: + operation: "Python API: modelable.operations.compilation.CompilationService plus compiler, parser, validation, planner, emitters and registry modules" + idempotent: false + auth: caller filesystem permissions; explicit local invocation + errors: {CompilationError: python-exception, CompilationDiagnosticsError: python-exception, FileTransactionError: python-exception, FileTransactionCommittedError: committed-with-cleanup-error, LockContentionError: python-exception, RegistryIdLockContentionError: python-exception, OCIRegistryError: python-exception} + - id: native-command-workflows + version: "1.0" + status: specified + preconditions: [command invoked with local filesystem access] + postconditions: [command effects limited to the toolchain and optional configured integrations] + invariants: [known operational failures render as CLI errors with nonzero status] + failure_modes: [click-error] + - id: desktop-language-and-conversation + version: "1.0" + status: specified + preconditions: [stdio language-server session with workspace URI] + postconditions: [diagnostics and conversation previews returned; applying a preview requires explicit confirmation] + invariants: [conversation preview does not change workspace files, a failed preview keeps any pending action] + failure_modes: [error-reply] + interface: + operation: "stdio JSON-RPC language server started by 'modelable lsp', including the conversation protocol (protocolVersion 2 in tests)" + idempotent: false + auth: local stdio session; apply requires an exact confirmation binding + errors: {error-reply: "ConversationReply kind=error"} + - id: browser-compiler-api + version: "1.0" + status: specified + preconditions: [browser DTO request from the playground worker] + postconditions: [same Python semantics returned through browser DTOs] + invariants: [browser wheel targets Python 3.14 only] + failure_modes: [browser-error-dto] + interface: + operation: "modelable.browser.api.BrowserCompiler via browser dispatch in the Pyodide worker" + idempotent: false + auth: same-origin worker; no remote authentication + errors: {browser-error-dto: "browser error DTO"} + - id: playground-workspace + version: "1.0" + status: specified + preconditions: [browser with a Pyodide worker] + postconditions: [workspace source persisted to IndexedDB when available, otherwise held in memory] + invariants: [a stored record with a greater revision is not overwritten by the repository, derived results are memory-only] + failure_modes: [memory-only, recovery-required] + - id: vscode-model-authoring + version: "1.0" + status: specified + preconditions: [configured Python interpreter able to start the language server] + postconditions: [editor connected to the stdio language server] + invariants: [conversation apply crosses an explicit preview and confirm boundary] + failure_modes: [server-start-failure] +components: + - id: semantic-toolchain + version: "1.15.2" + status: specified + provides: [local-contract-toolchain] + owns_data: [registry-id-ledger, enum-number-ledger, registry-index-db, registry-snapshot, usage-manifest] + # Coarse inventory-level boundary: spans compiler, parser, validation, planner, emitters, registry and operations. + # Override preserves the existing shared local-state boundary; splitting needs discovery (MOD-ADOPT-04). + context_budget: {max_owns_data: 5} + source_paths: + - cli/src/modelable/compiler + - cli/src/modelable/parser + - cli/src/modelable/validation + - cli/src/modelable/planner + - cli/src/modelable/emitters + - cli/src/modelable/registry + - cli/src/modelable/operations + - id: native-cli + version: "1.15.2" + status: specified + provides: [native-command-workflows] + requires: [local-contract-toolchain] + source_paths: [cli/src/modelable/cli.py, cli/src/modelable/commands, cli/src/modelable/llm, cli/src/modelable/specs] + - id: desktop-language-server + version: "1.15.2" + status: specified + provides: [desktop-language-and-conversation] + requires: [local-contract-toolchain] + source_paths: [cli/src/modelable/lsp, cli/src/modelable/language] + - id: browser-facade + version: "1.15.2" + status: specified + provides: [browser-compiler-api] + requires: [local-contract-toolchain] + source_paths: [cli/src/modelable/browser, cli/browser] + - id: browser-playground + version: "1.15.2" + status: specified + provides: [playground-workspace] + requires: [browser-compiler-api] + owns_data: [workspace-record, theme-preference] + source_paths: [web/src, web/package.json] + - id: vscode-extension + version: "1.15.2" + status: specified + provides: [vscode-model-authoring] + requires: [desktop-language-and-conversation] + source_paths: [vscode/extension.js, vscode/package.json] +data_models: + - id: registry-id-ledger + version: "1.0" + owner: semantic-toolchain + classification: restricted + classification_review: MOD-ADOPT-03 + fields: + entries: "dict[str, int] mapping 'domain.Name' to a never-reused small integer" + - id: enum-number-ledger + version: "1.0" + owner: semantic-toolchain + classification: restricted + classification_review: MOD-ADOPT-03 + fields: + members: "list of {name, number} per qualified declaration" + reservations: "list of {name, number}; numbers and names of removed members, never reused" + - id: registry-index-db + version: "1.0" + owner: semantic-toolchain + classification: restricted + classification_review: MOD-ADOPT-03 + schema_path: cli/src/modelable/registry/schema.sql + derived_from: [registry-id-ledger] + fields: + tables: "15 SQLite tables defined in schema.sql, rebuilt from the validated workspace on each build" + - id: registry-snapshot + version: "1.0" + owner: semantic-toolchain + classification: restricted + classification_review: MOD-ADOPT-03 + fields: + lock_file: registry.lock under the snapshot root + objects_dir: registry/objects under the snapshot root + - id: usage-manifest + version: "1.0" + owner: semantic-toolchain + classification: restricted + classification_review: MOD-ADOPT-03 + fields: + protocol: "modelable.usage/v0 JSON manifest; remaining fields not yet mapped" + - id: workspace-record + version: "1.0" + owner: browser-playground + classification: restricted + classification_review: MOD-ADOPT-03 + external_source: browser-local-workspace-storage + fields: + schemaVersion: "1" + id: str + revision: int + files: "list of {path: str, content: str, version: int}" + activeFile: str + metadata: "optional {lastAiAccept: {provider, model, timestamp}}" + - id: theme-preference + version: "1.0" + owner: browser-playground + classification: internal + classification_review: MOD-ADOPT-03 + external_source: browser-local-workspace-storage + fields: + modelable_theme: "'light' or 'dark'; absence means system" +requirements: + - id: MOD-ADOPT-01 + version: "1.0" + status: specified + target: modelable-product + category: functional + criteria: + - Complete ownership and dependency discovery before accepting whole-product architecture. + - Map native integrations, registry side effects, browser storage and all public protocol schemas. + - Preserve docs/architecture.md and modelable capabilities as existing product authorities. + - id: MOD-ADOPT-02 + version: "1.0" + status: specified + target: modelable-product + category: functional + criteria: + - Expand characterization beyond compilation before accepting whole-product behavioral conformance. + - Review every verification category and applicable formal models with current evidence before release. + - id: MOD-ADOPT-03 + version: "1.0" + status: specified + target: modelable-product + kind: non-functional + category: security + criteria: + - Replace each provisional classification on whole-product data models with a maintainer-reviewed classification. + - Classification labels in this draft are conservative handling policy, not observed product classifications. + - id: MOD-ADOPT-04 + version: "1.0" + status: specified + target: modelable-product + category: functional + criteria: + - Discover finer consistency boundaries inside semantic-toolchain before removing its context-budget override. + - Map snapshot, usage, resolver, Apicurio, OpenLineage and Git source protocols, Pyodide worker state and AI provider state. + - id: MOD-PROD-01 + version: "1.0" + status: verified + target: local-contract-toolchain + category: semantic + criteria: + - Registry IDs are never reassigned once allocated. + - id: MOD-PROD-02 + version: "1.0" + status: verified + target: native-command-workflows + category: functional + criteria: + - Known compilation operational failures render as CLI errors with nonzero status. + - id: MOD-PROD-03 + version: "1.0" + status: verified + target: desktop-language-and-conversation + category: functional + criteria: + - A failed conversation preview keeps the existing pending action over the language-server conversation service. + - id: MOD-PROD-04 + version: "1.0" + status: verified + target: browser-compiler-api + category: contract + criteria: + - Native and browser compilation snapshots are deterministic for the same scenarios. + - id: MOD-PROD-05 + version: "1.0" + status: verified + target: playground-workspace + category: functional + criteria: + - The workspace repository does not overwrite a stored record with a greater revision. + - id: MOD-PROD-06 + version: "1.0" + status: specified + target: vscode-model-authoring + category: functional + criteria: + - A failed language-server start is reported to the user as an error message. + - Conversation apply crosses an explicit preview and confirm boundary in the extension. + - id: MOD-PROD-07 + version: "1.0" + status: verified + target: local-contract-toolchain + category: serialization + criteria: + - The registry ID ledger round-trips through its JSON file sorted by id. + - id: MOD-PROD-08 + version: "1.0" + status: verified + target: local-contract-toolchain + category: concurrency + criteria: + - Registry ID ledger access is serialized across processes by the ledger lock. + - id: MOD-PROD-09 + version: "1.0" + status: verified + target: local-contract-toolchain + kind: non-functional + category: resilience + criteria: + - A promoted file whose hash does not verify is rolled back by the file transaction. + - id: MOD-PROD-10 + version: "1.0" + status: verified + target: local-contract-toolchain + category: concurrency + criteria: + - "Promotion of staged files is exclusive, and an apply based on a stale preview cannot commit alongside a conflicting direct compilation (bounded model: two processes, two files)." + - id: MOD-PROD-11 + version: "1.0" + status: specified + kind: non-functional + target: local-contract-toolchain + category: resilience + criteria: + - Promotion leaves destination files consistent after a process crash or a failed compensation. +risks: + - {id: incomplete-architecture-discovery, target: modelable-product, treatment: mitigation, mitigated_by: [MOD-ADOPT-01]} + - {id: incomplete-product-characterization, target: modelable-product, treatment: mitigation, mitigated_by: [MOD-ADOPT-02]} + - {id: provisional-data-classification, target: modelable-product, treatment: mitigation, mitigated_by: [MOD-ADOPT-03]} + - {id: product-category-gap, target: modelable-product, treatment: mitigation, mitigated_by: [MOD-ADOPT-02], waives: verification-category, expires: verification} + - {id: promotion-not-crash-atomic, target: modelable-product, treatment: mitigation, mitigated_by: [MOD-PROD-11]} + - {id: coarse-toolchain-boundary, target: modelable-product, treatment: mitigation, mitigated_by: [MOD-ADOPT-04], waives: context-budget, expires: release} +evidence: + - id: ev-mod-prod-01 + environment: "Windows; CPython 3.14.5; pytest 9.1.1; 300 passed, 4 skipped, 2 reruns (flaky-marked test_file_transaction case, not cited)" + criteria: + - Registry IDs are never reassigned once allocated. + requirement_id: MOD-PROD-01 + requirement_version: "1.0" + method: test + passed: true + provenance: "cli/tests/test_registry_ids.py::test_allocate_never_reassigns_existing_ids" + subject_id: local-contract-toolchain + subject_version: "1.0" + subject_revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + artifacts: + docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 70bc4fb81cc7dcd5bd4c15ff51cb4bb2f5a452d033e9d3a16790700538a80aba + docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: 10397146c4a586399b55aa4b1e2878b3a7e971be1b0af97cacf969ec47144561 + cli/tests/test_registry_ids.py: 24d66db6bac6e6b39c2d8f28a02c60c9a357acdcf04c164ed1954d7f30ba76c8 + timestamp: "2026-11-04" + verifier: "CPython 3.14.5; pytest 9.1.1; Windows" + bounds: "Single named test only; the suite totals are in the retained output. Does not cover other behavior of the capability." + - id: ev-mod-prod-02 + environment: "Windows; CPython 3.14.5; pytest 9.1.1; 300 passed, 4 skipped, 2 reruns (flaky-marked test_file_transaction case, not cited)" + criteria: + - Known compilation operational failures render as CLI errors with nonzero status. + requirement_id: MOD-PROD-02 + requirement_version: "1.0" + method: test + passed: true + provenance: "cli/tests/test_cli_compilation_errors.py::test_compile_renders_known_operational_errors[ledger-lock]" + subject_id: native-command-workflows + subject_version: "1.0" + subject_revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + artifacts: + docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 70bc4fb81cc7dcd5bd4c15ff51cb4bb2f5a452d033e9d3a16790700538a80aba + docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: 10397146c4a586399b55aa4b1e2878b3a7e971be1b0af97cacf969ec47144561 + cli/tests/test_cli_compilation_errors.py: f50ac380689c416c54999bd5b106fa3e8dbc42056a5f44c39b718531b1d3e820 + timestamp: "2026-11-04" + verifier: "CPython 3.14.5; pytest 9.1.1; Windows" + bounds: "Single named test only; the suite totals are in the retained output. Does not cover other behavior of the capability." + - id: ev-mod-prod-03 + environment: "Windows; CPython 3.14.5; pytest 9.1.1; 300 passed, 4 skipped, 2 reruns (flaky-marked test_file_transaction case, not cited)" + criteria: + - A failed conversation preview keeps the existing pending action over the language-server conversation service. + requirement_id: MOD-PROD-03 + requirement_version: "1.0" + method: test + passed: true + provenance: "cli/tests/test_conversation_preview_recovery.py::test_wire_error_keeps_existing_pending_source_action" + subject_id: desktop-language-and-conversation + subject_version: "1.0" + subject_revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + artifacts: + docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 70bc4fb81cc7dcd5bd4c15ff51cb4bb2f5a452d033e9d3a16790700538a80aba + docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: 10397146c4a586399b55aa4b1e2878b3a7e971be1b0af97cacf969ec47144561 + cli/tests/test_conversation_preview_recovery.py: 02c7881dbc5dd358bc64779d634a980a9d2061e0dea1c4a86f05c97bc4d5f795 + timestamp: "2026-11-04" + verifier: "CPython 3.14.5; pytest 9.1.1; Windows" + bounds: "Single named test only; the suite totals are in the retained output. Does not cover other behavior of the capability." + - id: ev-mod-prod-04 + environment: "Windows; CPython 3.14.5; pytest 9.1.1; 300 passed, 4 skipped, 2 reruns (flaky-marked test_file_transaction case, not cited)" + criteria: + - Native and browser compilation snapshots are deterministic for the same scenarios. + requirement_id: MOD-PROD-04 + requirement_version: "1.0" + method: test + passed: true + provenance: "cli/tests/test_browser_conformance.py::test_native_browser_snapshots_are_deterministic" + subject_id: browser-compiler-api + subject_version: "1.0" + subject_revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + artifacts: + docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 70bc4fb81cc7dcd5bd4c15ff51cb4bb2f5a452d033e9d3a16790700538a80aba + docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: 10397146c4a586399b55aa4b1e2878b3a7e971be1b0af97cacf969ec47144561 + cli/tests/test_browser_conformance.py: 6ee86288dfd252a670cf6d3ccecaa501a126e54bac8f7f7dfde08f883a7a808a + timestamp: "2026-11-04" + verifier: "CPython 3.14.5; pytest 9.1.1; Windows" + bounds: "Single named test only; the suite totals are in the retained output. Does not cover other behavior of the capability." + - id: ev-mod-prod-05 + environment: "Windows; Node v26.13.0; vitest 4.1.10; 24 passed (4 files)" + criteria: + - The workspace repository does not overwrite a stored record with a greater revision. + requirement_id: MOD-PROD-05 + requirement_version: "1.0" + method: test + passed: true + provenance: "web/src/workspace-repository.test.ts::a stale revision cannot overwrite a newer workspace" + subject_id: playground-workspace + subject_version: "1.0" + subject_revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + artifacts: + docs/superpowers/specs/system-spec/evidence/level2/web-level2.txt: ed7902e0714270e12d16b7ba3fb6ae7f3b5ad66d8fef0de0e61583e33c81091e + web/src/workspace-repository.test.ts: 4e62b239f2ab4d4b8bc61eb6d18def7ca537aed62efe7d67c6ddbb3eecc8584f + timestamp: "2026-11-04" + verifier: "Node v26.13.0; vitest 4.1.10; Windows" + bounds: "Single named test only; the suite totals are in the retained output. Does not cover other behavior of the capability." + - id: ev-mod-prod-07 + environment: "Windows; CPython 3.14.5; pytest 9.1.1; 300 passed, 4 skipped, 2 reruns (flaky-marked test_file_transaction case, not cited)" + criteria: + - The registry ID ledger round-trips through its JSON file sorted by id. + requirement_id: MOD-PROD-07 + requirement_version: "1.0" + method: test + passed: true + provenance: "cli/tests/test_registry_ids.py::test_write_then_read_lock_file_round_trips_sorted_by_id" + subject_id: local-contract-toolchain + subject_version: "1.0" + subject_revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + artifacts: + docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 70bc4fb81cc7dcd5bd4c15ff51cb4bb2f5a452d033e9d3a16790700538a80aba + docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: 10397146c4a586399b55aa4b1e2878b3a7e971be1b0af97cacf969ec47144561 + cli/tests/test_registry_ids.py: 24d66db6bac6e6b39c2d8f28a02c60c9a357acdcf04c164ed1954d7f30ba76c8 + timestamp: "2026-11-04" + verifier: "CPython 3.14.5; pytest 9.1.1; Windows" + bounds: "Single named test only; the suite totals are in the retained output." + - id: ev-mod-prod-08 + environment: "Windows; CPython 3.14.5; pytest 9.1.1; 300 passed, 4 skipped, 2 reruns (flaky-marked test_file_transaction case, not cited)" + criteria: + - Registry ID ledger access is serialized across processes by the ledger lock. + requirement_id: MOD-PROD-08 + requirement_version: "1.0" + method: test + passed: true + provenance: "cli/tests/test_registry_ids.py::test_registry_id_lock_serializes_processes" + subject_id: local-contract-toolchain + subject_version: "1.0" + subject_revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + artifacts: + docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 70bc4fb81cc7dcd5bd4c15ff51cb4bb2f5a452d033e9d3a16790700538a80aba + docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: 10397146c4a586399b55aa4b1e2878b3a7e971be1b0af97cacf969ec47144561 + cli/tests/test_registry_ids.py: 24d66db6bac6e6b39c2d8f28a02c60c9a357acdcf04c164ed1954d7f30ba76c8 + timestamp: "2026-11-04" + verifier: "CPython 3.14.5; pytest 9.1.1; Windows" + bounds: "Single named test only; the suite totals are in the retained output." + - id: ev-mod-prod-09 + environment: "Windows; CPython 3.14.5; pytest 9.1.1; 300 passed, 4 skipped, 2 reruns (flaky-marked test_file_transaction case, not cited)" + criteria: + - A promoted file whose hash does not verify is rolled back by the file transaction. + requirement_id: MOD-PROD-09 + requirement_version: "1.0" + method: test + passed: true + provenance: "cli/tests/test_file_transaction.py::test_transaction_verifies_promoted_hash_and_rolls_back" + subject_id: local-contract-toolchain + subject_version: "1.0" + subject_revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + artifacts: + docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 70bc4fb81cc7dcd5bd4c15ff51cb4bb2f5a452d033e9d3a16790700538a80aba + docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: 10397146c4a586399b55aa4b1e2878b3a7e971be1b0af97cacf969ec47144561 + cli/tests/test_file_transaction.py: 135bcfa3c49ffb2500c8a4cce34f10dc9ea2dae76ad74e85fff476a0b8e58d8c + timestamp: "2026-11-04" + verifier: "CPython 3.14.5; pytest 9.1.1; Windows" + bounds: "Single named test only; the suite totals are in the retained output." + - id: ev-mod-prod-10-tla + environment: "Windows; TLC 2.19 (tla2tools.jar v1.7.4); OpenJDK 25.0.5" + criteria: + - "Promotion of staged files is exclusive, and an apply based on a stale preview cannot commit alongside a conflicting direct compilation (bounded model: two processes, two files)." + requirement_id: MOD-PROD-10 + requirement_version: "1.0" + method: model-check + passed: true + provenance: "tla+::docs/superpowers/specs/system-spec/evidence/formal/CompilationProtocol.tla" + subject_id: local-contract-toolchain + subject_version: "1.0" + subject_revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + artifacts: + docs/superpowers/specs/system-spec/evidence/formal/CompilationProtocol.tla: dd505b32cb8fd23cb42fe93167bd9199eec063561f0ae70241defd1a49825d4e + docs/superpowers/specs/system-spec/evidence/formal/A_no_faults.cfg: 055eca9784d67c3cf0787ea9fa8e53b6e26da151dde09f9add631525158767da + docs/superpowers/specs/system-spec/evidence/formal/D_all_faults_safety.cfg: 04c9cf0833c6d019c726873867be61efeb1a6a1b9a18ef6d5ac8cb15c8c9dbd5 + docs/superpowers/specs/system-spec/evidence/formal/tlc-output.txt: bf4dca8eb76dd3e15cbc34ea4b036c3835aa1c9f709a7c42f4b4073543286f4c + timestamp: "2026-11-04" + verifier: "TLC 2.19 model checker" + bounds: "Two processes (direct d, apply a), two destination files, one workspace lock, ID and enum locks as an ordered pair; configs A (no faults) and D (rollback may fail and crash; safety invariants only) explored exhaustively, 171 and 530 states. Abstraction assumptions are listed in the module header; this is a bounded model of the observed protocol, not a proof of the implementation." + - id: ev-mod-prod-11-tla + environment: "Windows; TLC 2.19 (tla2tools.jar v1.7.4); OpenJDK 25.0.5" + criteria: + - Promotion leaves destination files consistent after a process crash or a failed compensation. + requirement_id: MOD-PROD-11 + requirement_version: "1.0" + method: model-check + passed: false + provenance: "tla+::docs/superpowers/specs/system-spec/evidence/formal/CompilationProtocol.tla" + subject_id: local-contract-toolchain + subject_version: "1.0" + subject_revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + artifacts: + docs/superpowers/specs/system-spec/evidence/formal/CompilationProtocol.tla: dd505b32cb8fd23cb42fe93167bd9199eec063561f0ae70241defd1a49825d4e + docs/superpowers/specs/system-spec/evidence/formal/B_rollback_may_fail.cfg: 5e4b8c38f379f2da6a5f5e645d8889aaff9afbd70fe049706e7f55129aeb83d9 + docs/superpowers/specs/system-spec/evidence/formal/C_crash.cfg: 71cfe35c76a042e307245540b5a7d0cdb487608421c4d0e273a56dc3254fd38d + docs/superpowers/specs/system-spec/evidence/formal/tlc-output.txt: bf4dca8eb76dd3e15cbc34ea4b036c3835aa1c9f709a7c42f4b4073543286f4c + timestamp: "2026-11-04" + verifier: "TLC 2.19 model checker" + bounds: "Same bounds. TLC found counterexamples in config B (compensation may fail) and config C (crash mid-promotion): destination files end in different versions. This records an as-is gap in the observed protocol (no commit journal), not a defect confirmed by a product test." +subject_bindings: + local-contract-toolchain: + version: "1.0" + revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + artifacts: + cli/src/modelable/registry/ids.py: 7d0a7b260ae780ed338a6073c428407d84e56d88f0ec8e631b4538de6b801069 + cli/src/modelable/operations/file_transaction.py: 628fe1a047fb8ecd682ba5eb2f1d1545665f84dd90a4038da1e6a6e5e3785794 + cli/src/modelable/operations/compilation.py: b003590e348e061f684a9f78b98a9ae61e8f8748afb3f8ff324e3df04f7d7cc3 + native-command-workflows: + version: "1.0" + revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + artifacts: + cli/src/modelable/commands/compile.py: 004ae26dfab6174fb3b9a73b5d4021a9ea5d36671662b7f4e54dd832db7490e8 + desktop-language-and-conversation: + version: "1.0" + revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + artifacts: + cli/src/modelable/llm/filesystem_conversation.py: aafb5a26a9c4993505548be98b23fd144fe24f8685824261f2a7753b9fc2065f + cli/src/modelable/lsp/conversation_service.py: d492a25393150aa90273c546643a1560004ae803e550bb1e31383e3a389e78fe + browser-compiler-api: + version: "1.0" + revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + artifacts: + cli/src/modelable/browser/api.py: 47074420dc6f630d401e0f2514ecd0d183b42580f56eae5e5cbcc6afe98f9dfd + cli/src/modelable/browser/dispatch.py: f83e38aa01c9636f370d75c23b819e0912df654d763dc7fd9628c31e6e18fd13 + playground-workspace: + version: "1.0" + revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + artifacts: + web/src/workspace-repository.ts: f9604c1768e472faab787efb2192ceb40e3f614c5fe2b0a6d5ff74c3a970ac39 + web/src/usePersistentWorkspace.ts: 36fac0e43a22cca18d66ec629821abf9eeb2cfaae2e601660dd0ec8b00057b6c