From 807b0c536d2f06f281c87180016617d5e176bff1 Mon Sep 17 00:00:00 2001 From: ktjn Date: Thu, 5 Nov 2026 07:20:08 +0100 Subject: [PATCH 1/5] fix(web): surface rejected saves and sync playground tabs A stale save result was shown as saved; the hook now enters memory-only. Tabs announce saved revisions over a BroadcastChannel: clean tabs adopt a newer revision, tabs with unsaved edits are marked memory-only. Co-Authored-By: Claude Sonnet 5.5 --- .../system-spec/browser-persistence-map.md | 4 +- web/src/usePersistentWorkspace.test.tsx | 132 ++++++++++++++++++ web/src/usePersistentWorkspace.ts | 61 +++++++- 3 files changed, 194 insertions(+), 3 deletions(-) diff --git a/docs/superpowers/specs/system-spec/browser-persistence-map.md b/docs/superpowers/specs/system-spec/browser-persistence-map.md index 45e81152..67cd5a1b 100644 --- a/docs/superpowers/specs/system-spec/browser-persistence-map.md +++ b/docs/superpowers/specs/system-spec/browser-persistence-map.md @@ -33,8 +33,8 @@ Derived results (compiled artifacts, diagnostics, graph) are memory-only; the de ## 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`). +- **`'stale'` result (fixed after this map was drafted: the hook now enters `memory-only`; the paragraph below describes the earlier behavior).** 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. +- **Cross-tab notification (added after this map was drafted: the hook now uses a `BroadcastChannel` to announce saved revisions; the sentence below describes the earlier behavior).** 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. diff --git a/web/src/usePersistentWorkspace.test.tsx b/web/src/usePersistentWorkspace.test.tsx index 6d54e180..2111050e 100644 --- a/web/src/usePersistentWorkspace.test.tsx +++ b/web/src/usePersistentWorkspace.test.tsx @@ -172,3 +172,135 @@ test('retry saves newer in-memory work instead of loading older storage', async expect(repository.save).toHaveBeenCalledWith(edited); expect(repository.load).toHaveBeenCalledTimes(1); }); + +test('a stale save result is not reported as saved', async () => { + const edited = mutateWorkspace(defaultWorkspace, { + type: 'update', + path: 'main.mdl', + content: 'domain edited {}', + }); + const repository: WorkspaceRepository = { + load: vi.fn(async (): Promise => ({ + status: 'ready', + workspace: defaultWorkspace, + })), + save: vi.fn(async (): Promise => 'stale'), + remove: vi.fn(async () => undefined), + }; + const { result } = renderHook(() => + usePersistentWorkspace({ repository, defaultWorkspace, debounceMs: 1 }), + ); + await waitFor(() => expect(result.current.phase).toBe('saved')); + + act(() => result.current.replace(edited, { immediate: true })); + + await waitFor(() => expect(result.current.phase).toBe('memory-only')); + expect(result.current.workspace).toEqual(edited); +}); + +class FakeChannel { + static instances: FakeChannel[] = []; + onmessage: ((event: { data: unknown }) => void) | null = null; + posted: unknown[] = []; + constructor(public name: string) { + FakeChannel.instances.push(this); + } + postMessage(data: unknown): void { + this.posted.push(data); + } + close(): void { + FakeChannel.instances = FakeChannel.instances.filter((c) => c !== this); + } +} + +function channelRepository(stored: () => WorkspaceLoadResult) { + const repository: WorkspaceRepository = { + load: vi.fn(async () => stored()), + save: vi.fn(async (): Promise => 'saved'), + remove: vi.fn(async () => undefined), + }; + return repository; +} + +test('announces saved revisions to other tabs', async () => { + FakeChannel.instances = []; + vi.stubGlobal('BroadcastChannel', FakeChannel); + try { + const repository = channelRepository(() => ({ + status: 'ready', + workspace: defaultWorkspace, + })); + const { result } = renderHook(() => + usePersistentWorkspace({ repository, defaultWorkspace, debounceMs: 1 }), + ); + await waitFor(() => expect(result.current.phase).toBe('saved')); + act(() => result.current.replace(restoredWorkspace, { immediate: true })); + await waitFor(() => expect(result.current.phase).toBe('saved')); + expect(FakeChannel.instances[0]?.posted).toContainEqual({ + id: defaultWorkspace.id, + revision: restoredWorkspace.revision, + }); + } finally { + vi.unstubAllGlobals(); + } +}); + +test('a clean tab reloads when another tab saves a newer revision', async () => { + FakeChannel.instances = []; + vi.stubGlobal('BroadcastChannel', FakeChannel); + try { + let stored: WorkspaceLoadResult = { + status: 'ready', + workspace: defaultWorkspace, + }; + const repository = channelRepository(() => stored); + const { result } = renderHook(() => + usePersistentWorkspace({ repository, defaultWorkspace, debounceMs: 1 }), + ); + await waitFor(() => expect(result.current.phase).toBe('saved')); + stored = { status: 'ready', workspace: restoredWorkspace }; + + act(() => + FakeChannel.instances[0]?.onmessage?.({ + data: { id: defaultWorkspace.id, revision: restoredWorkspace.revision }, + }), + ); + + await waitFor(() => expect(result.current.workspace).toEqual(restoredWorkspace)); + expect(result.current.phase).toBe('saved'); + } finally { + vi.unstubAllGlobals(); + } +}); + +test('a dirty tab is flagged memory-only when another tab saves newer', async () => { + FakeChannel.instances = []; + vi.stubGlobal('BroadcastChannel', FakeChannel); + try { + const repository = channelRepository(() => ({ + status: 'ready', + workspace: defaultWorkspace, + })); + const { result } = renderHook(() => + usePersistentWorkspace({ repository, defaultWorkspace, debounceMs: 60_000 }), + ); + await waitFor(() => expect(result.current.phase).toBe('saved')); + const edited = mutateWorkspace(defaultWorkspace, { + type: 'update', + path: 'main.mdl', + content: 'domain local {}', + }); + act(() => result.current.replace(edited)); + + act(() => + FakeChannel.instances[0]?.onmessage?.({ + data: { id: defaultWorkspace.id, revision: edited.revision + 5 }, + }), + ); + + expect(result.current.phase).toBe('memory-only'); + expect(result.current.workspace).toEqual(edited); + } finally { + vi.unstubAllGlobals(); + } +}); diff --git a/web/src/usePersistentWorkspace.ts b/web/src/usePersistentWorkspace.ts index 47a322d7..03d304d9 100644 --- a/web/src/usePersistentWorkspace.ts +++ b/web/src/usePersistentWorkspace.ts @@ -28,6 +28,8 @@ export interface PersistentWorkspaceState { reset(): Promise; } +const CHANNEL_NAME = 'modelable:workspace-saved'; + export function usePersistentWorkspace({ repository, defaultWorkspace, @@ -46,13 +48,22 @@ export function usePersistentWorkspace({ const timerRef = useRef | null>(null); const saveSequenceRef = useRef(0); const mountedRef = useRef(true); + const channelRef = useRef(null); const save = useCallback( async (snapshot: PlaygroundWorkspace): Promise => { const sequence = saveSequenceRef.current + 1; saveSequenceRef.current = sequence; try { - await repository.save(snapshot); + const outcome = await repository.save(snapshot); + if (outcome === 'stale') { + // A newer revision is already stored (e.g. another tab); the write + // was rejected, so this work is not persisted. + if (mountedRef.current && sequence === saveSequenceRef.current) { + setPhase('memory-only'); + } + return; + } if ( mountedRef.current && sequence === saveSequenceRef.current && @@ -60,6 +71,10 @@ export function usePersistentWorkspace({ ) { dirtyRef.current = false; setPhase('saved'); + channelRef.current?.postMessage({ + id: snapshot.id, + revision: snapshot.revision, + }); } } catch { if (mountedRef.current && sequence === saveSequenceRef.current) { @@ -127,6 +142,50 @@ export function usePersistentWorkspace({ }; }, [applyLoadResult, defaultWorkspace.id, repository]); + useEffect(() => { + if (typeof BroadcastChannel === 'undefined') { + return undefined; + } + // Other tabs announce the revision they saved. A clean tab adopts it; a tab + // with unsaved edits can no longer save over it, so it is marked unsaved. + const channel = new BroadcastChannel(CHANNEL_NAME); + channelRef.current = channel; + channel.onmessage = (event: MessageEvent): void => { + const message = event.data as { id?: unknown; revision?: unknown } | null; + if ( + message === null || + message.id !== defaultWorkspace.id || + typeof message.revision !== 'number' || + message.revision <= workspaceRef.current.revision + ) { + return; + } + if (dirtyRef.current) { + setPhase('memory-only'); + return; + } + void repository.load(defaultWorkspace.id).then( + (result) => { + if ( + mountedRef.current && + !dirtyRef.current && + result.status === 'ready' && + result.workspace.revision > workspaceRef.current.revision + ) { + workspaceRef.current = result.workspace; + setWorkspace(result.workspace); + setPhase('saved'); + } + }, + () => undefined, + ); + }; + return () => { + channel.close(); + channelRef.current = null; + }; + }, [defaultWorkspace.id, repository]); + useEffect(() => { const handlePageHide = (): void => { if (dirtyRef.current) { From 68d8cf8ccabb7e3797c949c402d82d31e05279eb Mon Sep 17 00:00:00 2001 From: ktjn Date: Thu, 5 Nov 2026 07:20:08 +0100 Subject: [PATCH 2/5] fix(cli): journal promotions and recover interrupted ones FileTransaction writes a fsync'd journal before replacing files and removes it at the commit point; the next lock holder rolls back a leftover journal. Direct compilation recovers before staging so it never builds output from a half-promoted workspace. Changelog also covers the web persistence changes. Co-Authored-By: Claude Sonnet 5.5 --- CHANGELOG.md | 6 + cli/src/modelable/operations/compilation.py | 3 + .../modelable/operations/file_transaction.py | 126 ++++++++++++++ cli/tests/test_compilation_service.py | 69 ++++++++ cli/tests/test_file_transaction.py | 155 ++++++++++++++++++ .../specs/system-spec/compilation-map.md | 2 +- 6 files changed, 360 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f0c7a107..ff2036fb 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,10 +8,16 @@ releases could contain breaking changes when called out explicitly. ### Added +- Keep multiple playground tabs on the same workspace in sync: a tab without unsaved edits adopts a newer revision saved by another tab, and a tab with unsaved edits is marked memory-only instead of silently losing the race. + ### Changed ### Fixed +- Recover from a compilation that was killed mid-promotion: the next compilation rolls the workspace back to its pre-promotion files using a journal kept under `.modelable/locks`. An unreadable journal blocks compilation instead of being ignored. + +- Show the playground as memory-only instead of saved when a workspace save is rejected because a newer revision is already stored (for example from another tab). + - 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. diff --git a/cli/src/modelable/operations/compilation.py b/cli/src/modelable/operations/compilation.py index 2ed7ea4f..2b0c205e 100644 --- a/cli/src/modelable/operations/compilation.py +++ b/cli/src/modelable/operations/compilation.py @@ -307,6 +307,9 @@ def _execute_direct_staged( workspace_root: Path, staging_dir: Path, ) -> DirectCompilationResult: + # Finish or undo a promotion that a dead process left behind before + # reading any workspace state to stage from. + self.transaction_factory(workspace_root).recover() staged_output = staging_dir / "output" staged_registry_ids = staging_dir / "registry-ids.lock" staged_enum_numbers = staging_dir / "enum-numbers.lock" diff --git a/cli/src/modelable/operations/file_transaction.py b/cli/src/modelable/operations/file_transaction.py index 1c4905d4..0911a6ec 100644 --- a/cli/src/modelable/operations/file_transaction.py +++ b/cli/src/modelable/operations/file_transaction.py @@ -1,6 +1,7 @@ from __future__ import annotations import hashlib +import json import os import shutil import sys @@ -57,6 +58,10 @@ def __init__( super().__init__(message) +class _JournalError(Exception): + """The promotion journal was unreadable or could not be fully replayed.""" + + class FileTransactionCommittedError(Exception): """Promotion committed, but post-commit cleanup was incomplete.""" @@ -132,6 +137,13 @@ def promote( release_errors = self._release_lock() raise FileTransactionError(error, release_errors) from error + try: + self._recover_interrupted_promotion() + except Exception as error: + recovery_errors = [RollbackError(self._journal_path(), error)] if isinstance(error, _JournalError) else [] + recovery_errors.extend(self._release_lock()) + raise FileTransactionError(error, recovery_errors) from error + if validate is not None: try: validate() @@ -176,6 +188,8 @@ def promote( if validate is not None: validate() + self._write_journal(promotions, created_directories) + for promotion in promotions: metadata_source = ( promotion.file.destination if promotion.backup is not None else promotion.file.staged_path @@ -187,12 +201,19 @@ def promote( for promotion in promotions: if _file_hash(promotion.file.destination) != promotion.file.content_hash: raise OSError(f"post-write hash verification failed for {promotion.file.destination}") + + # Removing the journal is the commit point: until it is gone, a + # crash is rolled back by the next transaction. + self._unlink(self._journal_path(), missing_ok=True) except Exception as error: rollback_errors = self._rollback( promoted, promotions, created_directories, ) + if not rollback_errors: + with suppress(OSError): + self._unlink(self._journal_path(), missing_ok=True) rollback_errors.extend(self._release_lock()) raise FileTransactionError(error, rollback_errors) from error @@ -203,6 +224,111 @@ def promote( raise FileTransactionCommittedError(written_paths, cleanup_errors) return written_paths + def recover(self) -> None: + """Roll back a promotion interrupted by a dead process, if one left a journal. + + Callers that read workspace state before promoting call this first, so + they never stage output derived from a half-promoted workspace. + """ + if self.workspace_root is None: + raise ValueError("recover() requires workspace_root") + journal = self.workspace_root / ".modelable" / "locks" / "compilation.journal" + if not journal.exists(): + return + self._acquire_lock(self.workspace_root) + try: + self._recover_interrupted_promotion() + except Exception as error: + recovery_errors = [RollbackError(journal, error)] if isinstance(error, _JournalError) else [] + recovery_errors.extend(self._release_lock()) + raise FileTransactionError(error, recovery_errors) from error + release_errors = self._release_lock() + if release_errors: + raise FileTransactionError(OSError("could not release the workspace lock"), release_errors) + + def _journal_path(self) -> Path: + assert self._lock_path is not None + return self._lock_path.with_name("compilation.journal") + + def _write_journal( + self, + promotions: Sequence[_Promotion], + created_directories: Sequence[Path], + ) -> None: + journal = { + "version": 1, + "entries": [ + { + "destination": str(item.file.destination), + "temporary": str(item.temporary), + "backup": str(item.backup) if item.backup is not None else None, + "hash": item.file.content_hash, + } + for item in promotions + ], + "created_directories": [str(path) for path in dict.fromkeys(created_directories)], + } + path = self._journal_path() + temporary = path.with_name(f"{path.name}.{self._token}.tmp") + descriptor = os.open( + temporary, + os.O_CREAT | os.O_EXCL | os.O_WRONLY | getattr(os, "O_BINARY", 0), + 0o600, + ) + try: + os.write(descriptor, json.dumps(journal).encode()) + os.fsync(descriptor) + finally: + os.close(descriptor) + os.replace(temporary, path) + + def _recover_interrupted_promotion(self) -> None: + """Roll back a promotion whose process died before it committed. + + Runs under the workspace lock. A journal that still exists means the + commit point was never reached, so every destination is returned to its + pre-promotion state. A journal that cannot be read blocks the + transaction and is kept for inspection. + """ + path = self._journal_path() + try: + data = path.read_bytes() + except FileNotFoundError: + return + try: + journal = json.loads(data) + entries = [ + ( + Path(entry["destination"]), + Path(entry["temporary"]), + Path(entry["backup"]) if entry["backup"] is not None else None, + str(entry["hash"]), + ) + for entry in journal["entries"] + ] + created = [Path(item) for item in journal["created_directories"]] + except (ValueError, KeyError, TypeError) as error: + raise _JournalError(f"Unreadable compilation journal {path}: {error}") from error + + errors: list[RollbackError] = [] + for destination, temporary, backup, content_hash in reversed(entries): + try: + if backup is not None: + if backup.exists(): + self._replace(backup, destination) + elif destination.exists() and _file_hash(destination) == content_hash: + self._unlink(destination, missing_ok=True) + self._unlink(temporary, missing_ok=True) + except Exception as error: + errors.append(RollbackError(destination, error)) + for directory in reversed(created): + with suppress(OSError): + directory.rmdir() + if errors: + details = os.linesep.join(f" - {item}" for item in errors) + raise _JournalError(f"Could not recover interrupted compilation promotion:{os.linesep}{details}") + self._unlink(path, missing_ok=True) + def _acquire_lock(self, root: Path) -> None: lock_path = root / ".modelable" / "locks" / "compilation.lock" self._lock_directories = (lock_path.parent, lock_path.parent.parent) diff --git a/cli/tests/test_compilation_service.py b/cli/tests/test_compilation_service.py index de6dc761..9ae6b4d8 100644 --- a/cli/tests/test_compilation_service.py +++ b/cli/tests/test_compilation_service.py @@ -1717,3 +1717,72 @@ def fail_staging_cleanup(path: Path) -> None: if pending is not None: audit = tmp_path / ".modelable" / "audit" / "compilations" / f"{pending.action_id}.json" assert audit.exists() + + +class _SimulatedProcessDeath(BaseException): + """Skips every ``except Exception`` handler, like a killed process.""" + + +def test_direct_compilation_recovers_an_interrupted_promotion_before_staging( + tmp_path: Path, + monkeypatch: pytest.MonkeyPatch, +) -> None: + events: list[str] = [] + + class RecordingTransaction(FileTransaction): + def recover(self) -> None: + events.append("recover") + super().recover() + + def promote(self, files, **kwargs): # type: ignore[no-untyped-def] + events.append("promote") + return super().promote(files, **kwargs) + + source = write_workspace(tmp_path) + request = request_for(tmp_path, source, "rust") + CompilationService( + transaction_factory=lambda root: RecordingTransaction(workspace_root=root), + ).execute_direct(request) + + assert events == ["recover", "promote"] + + +def test_direct_compilation_after_a_crashed_promotion_matches_a_clean_run( + tmp_path: Path, + monkeypatch: pytest.MonkeyPatch, +) -> None: + def crash_on_second_replace(source_path, destination_path): + if ".modelable-tmp-" in Path(source_path).name: + if crash_on_second_replace.count == 1: # type: ignore[attr-defined] + raise _SimulatedProcessDeath + crash_on_second_replace.count += 1 # type: ignore[attr-defined] + os.replace(source_path, destination_path) + + crash_on_second_replace.count = 0 # type: ignore[attr-defined] + + control = tmp_path / "control" + control.mkdir() + csrc = write_workspace(control) + CompilationService().execute_direct(request_for(control, csrc, "rust")) + + crashed = tmp_path / "crashed" + crashed.mkdir() + source = write_workspace(crashed) + with pytest.raises(_SimulatedProcessDeath): + CompilationService( + transaction_factory=lambda root: FileTransaction(workspace_root=root, replace=crash_on_second_replace), + ).execute_direct(request_for(crashed, source, "rust")) + monkeypatch.setattr("modelable.operations.file_transaction._process_alive", lambda pid: False) + monkeypatch.setattr("modelable.registry.ids._process_alive", lambda pid: False, raising=False) + + CompilationService().execute_direct(request_for(crashed, source, "rust")) + + def snapshot(root: Path) -> dict[str, bytes]: + return { + path.relative_to(root).as_posix(): path.read_bytes() + for path in sorted(root.rglob("*")) + if path.is_file() and ".modelable-" not in path.name and path.name != "registry.db" + } + + assert snapshot(crashed) == snapshot(control) + assert not list(crashed.rglob("compilation.journal")) diff --git a/cli/tests/test_file_transaction.py b/cli/tests/test_file_transaction.py index df47a4ab..74ddbe2a 100644 --- a/cli/tests/test_file_transaction.py +++ b/cli/tests/test_file_transaction.py @@ -658,3 +658,158 @@ def synchronized_mkdir(path: Path) -> None: assert results == [(workspace / "first.txt",), (workspace / "second.txt",)] assert not (workspace / ".modelable" / "locks").exists() + + +class SimulatedCrash(BaseException): + """Process death: skips every ``except Exception`` handler in the transaction.""" + + +def _crash_on_replace(fail_after: int): + seen = {"count": 0} + + def replace(source: str | Path, destination: str | Path) -> None: + if ".modelable-tmp-" in Path(source).name: + if seen["count"] == fail_after: + raise SimulatedCrash + seen["count"] += 1 + os.replace(source, destination) + + return replace + + +def _simulate_dead_owner(workspace: Path, monkeypatch: pytest.MonkeyPatch) -> None: + # The crashed "process" was this one, whose PID is alive; make it look dead. + monkeypatch.setattr("modelable.operations.file_transaction._process_alive", lambda pid: False) + assert (workspace / ".modelable" / "locks" / "compilation.lock").exists() + + +@pytest.mark.parametrize("fail_after", [0, 1, 2]) +def test_crash_mid_promotion_is_rolled_back_by_the_next_transaction( + tmp_path: Path, + monkeypatch: pytest.MonkeyPatch, + fail_after: int, +) -> None: + workspace = tmp_path / "workspace" + stage = tmp_path / "stage" + workspace.mkdir() + stage.mkdir() + destinations = [workspace / f"{index}.txt" for index in range(3)] + for index, destination in enumerate(destinations): + destination.write_bytes(f"before-{index}".encode()) + before = _snapshot(workspace) + + with pytest.raises(SimulatedCrash): + FileTransaction(workspace_root=workspace, replace=_crash_on_replace(fail_after)).promote( + _staged_files(stage, destinations) + ) + _simulate_dead_owner(workspace, monkeypatch) + + other = workspace / "other.txt" + other_stage = tmp_path / "stage2" + other_stage.mkdir() + FileTransaction(workspace_root=workspace).promote(_staged_files(other_stage, [other])) + + after = _snapshot(workspace) + assert after.pop(Path("other.txt")) == b"after-0" + assert after == before + assert not list(workspace.rglob("*.modelable-*")) + assert not (workspace / ".modelable").exists() + + +def test_crash_recovery_removes_new_files_and_created_directories( + tmp_path: Path, + monkeypatch: pytest.MonkeyPatch, +) -> None: + workspace = tmp_path / "workspace" + stage = tmp_path / "stage" + workspace.mkdir() + stage.mkdir() + destinations = [workspace / "new" / "a.txt", workspace / "new" / "b.txt"] + + with pytest.raises(SimulatedCrash): + FileTransaction(workspace_root=workspace, replace=_crash_on_replace(1)).promote( + _staged_files(stage, destinations) + ) + assert destinations[0].exists() + _simulate_dead_owner(workspace, monkeypatch) + + other_stage = tmp_path / "stage2" + other_stage.mkdir() + FileTransaction(workspace_root=workspace).promote(_staged_files(other_stage, [workspace / "other.txt"])) + + assert not (workspace / "new").exists() + assert not list(workspace.rglob("*.modelable-*")) + + +def test_crash_after_all_replacements_but_before_commit_rolls_back( + tmp_path: Path, + monkeypatch: pytest.MonkeyPatch, +) -> None: + workspace = tmp_path / "workspace" + stage = tmp_path / "stage" + workspace.mkdir() + stage.mkdir() + destination = workspace / "result.txt" + destination.write_bytes(b"before") + + def crash_on_journal_removal(path: Path, *, missing_ok: bool = False) -> None: + if path.name == "compilation.journal": + raise SimulatedCrash + path.unlink(missing_ok=missing_ok) + + with pytest.raises(SimulatedCrash): + FileTransaction(workspace_root=workspace, unlink=crash_on_journal_removal).promote( + _staged_files(stage, [destination]) + ) + assert destination.read_bytes() == b"after-0" + _simulate_dead_owner(workspace, monkeypatch) + + other_stage = tmp_path / "stage2" + other_stage.mkdir() + FileTransaction(workspace_root=workspace).promote(_staged_files(other_stage, [workspace / "other.txt"])) + + assert destination.read_bytes() == b"before" + + +def test_crash_recovery_leaves_new_file_alone_when_content_changed( + tmp_path: Path, + monkeypatch: pytest.MonkeyPatch, +) -> None: + workspace = tmp_path / "workspace" + stage = tmp_path / "stage" + workspace.mkdir() + stage.mkdir() + destination = workspace / "new.txt" + + with pytest.raises(SimulatedCrash): + FileTransaction(workspace_root=workspace, replace=_crash_on_replace(1)).promote( + _staged_files(stage, [destination, workspace / "second.txt"]) + ) + destination.write_bytes(b"edited by someone else") + _simulate_dead_owner(workspace, monkeypatch) + + other_stage = tmp_path / "stage2" + other_stage.mkdir() + FileTransaction(workspace_root=workspace).promote(_staged_files(other_stage, [workspace / "other.txt"])) + + assert destination.read_bytes() == b"edited by someone else" + + +def test_unreadable_journal_blocks_promotion_and_keeps_the_journal( + tmp_path: Path, + monkeypatch: pytest.MonkeyPatch, +) -> None: + workspace = tmp_path / "workspace" + stage = tmp_path / "stage" + workspace.mkdir() + stage.mkdir() + journal = workspace / ".modelable" / "locks" / "compilation.journal" + journal.parent.mkdir(parents=True) + journal.write_bytes(b"{not json") + + with pytest.raises(FileTransactionError, match="journal"): + FileTransaction(workspace_root=workspace).promote(_staged_files(stage, [workspace / "x.txt"])) + + assert journal.read_bytes() == b"{not json" + assert not (workspace / "x.txt").exists() + assert not (workspace / ".modelable" / "locks" / "compilation.lock").exists() diff --git a/docs/superpowers/specs/system-spec/compilation-map.md b/docs/superpowers/specs/system-spec/compilation-map.md index bee8c150..73dbba8d 100644 --- a/docs/superpowers/specs/system-spec/compilation-map.md +++ b/docs/superpowers/specs/system-spec/compilation-map.md @@ -62,7 +62,7 @@ Direct and conversational policies differ. Direct path mapping preserves the exi - Registry-ID and enum-number ledgers use the registry lock helper. Direct execution holds both ledger locks; apply holds the registry-ID lock and validates its before-state. The workspace promotion lock is `.modelable/locks/compilation.lock`, with waiter/PID liveness handling in `FileTransaction`. - Promotion verifies staged hashes, prepares adjacent temporary/backup files, revalidates, replaces destinations, verifies final hashes, then disposes backups and releases locks. A destination collision uses `_last_writers` by resolved path identity. - 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. +- These are multiple per-file replacements with compensation. A promotion journal (`.modelable/locks/compilation.journal`, added after this map was drafted) now lets the next transaction roll back a promotion interrupted before its commit point; unit tests simulate crashes, but no crash-atomicity proof is asserted and the TLA+ model has not been updated for it. 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. From ad7796388c2709cc05658bdef85e66b964b703ab Mon Sep 17 00:00:00 2001 From: ktjn Date: Thu, 5 Nov 2026 07:21:48 +0100 Subject: [PATCH 3/5] docs: model the promotion journal in TLA+ and re-pin whole-product evidence The updated CompilationProtocol model passes all four configs once direct compilation recovers before staging; a mutant without that recovery fails. Level 2 evidence re-run at 68d8cf8c and pins refreshed. Co-Authored-By: Claude Sonnet 5.5 --- .../evidence/formal/A_no_faults.cfg | 2 +- .../system-spec/evidence/formal/C_crash.cfg | 2 +- .../evidence/formal/CompilationProtocol.tla | 117 ++++++---- .../evidence/formal/D_all_faults_safety.cfg | 2 +- .../evidence/formal/tlc-output.txt | 211 +++--------------- .../evidence/level2/python-level2.txt | 12 +- .../evidence/level2/python-level2.xml | 2 +- .../evidence/level2/web-level2.txt | 6 +- .../specs/system-spec/whole-product-level2.md | 4 +- .../specs/system-spec/whole-product-level3.md | 8 +- .../specs/system-spec/whole-product.yaml | 128 +++++------ 11 files changed, 190 insertions(+), 304 deletions(-) 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 index 185e907e..fbb271f7 100644 --- a/docs/superpowers/specs/system-spec/evidence/formal/A_no_faults.cfg +++ b/docs/superpowers/specs/system-spec/evidence/formal/A_no_faults.cfg @@ -1,3 +1,3 @@ SPECIFICATION Spec CONSTANTS RollbackMayFail = FALSE CanCrash = FALSE -INVARIANTS PromotionExclusive LocksHeldByActive FilesConsistent NoLostUpdate +INVARIANTS PromotionExclusive LocksHeldByActive FilesConsistent Recoverable NoLostUpdate diff --git a/docs/superpowers/specs/system-spec/evidence/formal/C_crash.cfg b/docs/superpowers/specs/system-spec/evidence/formal/C_crash.cfg index f819cd93..6e202ef5 100644 --- a/docs/superpowers/specs/system-spec/evidence/formal/C_crash.cfg +++ b/docs/superpowers/specs/system-spec/evidence/formal/C_crash.cfg @@ -1,3 +1,3 @@ SPECIFICATION Spec CONSTANTS RollbackMayFail = FALSE CanCrash = TRUE -INVARIANTS FilesConsistent +INVARIANTS FilesConsistent Recoverable diff --git a/docs/superpowers/specs/system-spec/evidence/formal/CompilationProtocol.tla b/docs/superpowers/specs/system-spec/evidence/formal/CompilationProtocol.tla index 1567ff7f..4d29ccc1 100644 --- a/docs/superpowers/specs/system-spec/evidence/formal/CompilationProtocol.tla +++ b/docs/superpowers/specs/system-spec/evidence/formal/CompilationProtocol.tla @@ -1,9 +1,10 @@ ---------------------------- 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. + _verify_freshness), file_transaction.py (workspace lock, promotion journal, + 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 @@ -12,14 +13,23 @@ 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. + the preview snapshot. The second check runs after journal recovery. - 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. + liveness is assumed to complete) and leaves promoted files and the + promotion journal in place. + - The promotion journal (compilation.journal) records the pre-promotion + version of every file (the backups). It is written after the workspace + lock is taken and recovery has run, and removed at the commit point. The + next holder of the workspace lock restores from a leftover journal before + doing anything else (Recover). + - Direct compilation calls FileTransaction.recover() after taking the ID + and enum locks and before reading the state it stages from (DRecover), + so it never stages output derived from a half-promoted workspace. + - Rollback restores the journaled version of every promoted file; when + RollbackMayFail it may skip a file, and then the journal is kept. Not modeled: staging, hashes, permissions, audit file, cleanup errors, - timeouts, more than two processes, PID reuse. *) + timeouts, more than two processes, PID reuse, a crash during preparation or + during recovery itself. *) EXTENDS Naturals, FiniteSets CONSTANTS RollbackMayFail, CanCrash @@ -29,9 +39,10 @@ Files == {1, 2} NoOne == "none" Terminal == {"committed", "rolledBack", "rejected", "crashed"} -VARIABLES pc, idLock, enumLock, wsLock, disk, base, todo, done, rbFailed +VARIABLES pc, idLock, enumLock, wsLock, disk, base, todo, done, rbFailed, jrnl, jbase -vars == <> +vars == <> +jvars == <> Init == /\ pc = [p \in Procs |-> "start"] @@ -41,6 +52,7 @@ Init == /\ todo = [p \in Procs |-> {}] /\ done = [p \in Procs |-> {}] /\ rbFailed = FALSE + /\ jrnl = NoOne /\ jbase = [f \in Files |-> 0] Release(p) == /\ idLock' = IF idLock = p THEN NoOne ELSE idLock @@ -52,34 +64,53 @@ 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 <> + /\ 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 ---- + /\ UNCHANGED <> +\* FileTransaction.recover(): take the workspace lock just long enough to roll +\* back a leftover journal, then read the (now consistent) state to stage from. +DRecover == pc["d"] = "hasBoth" /\ wsLock = NoOne + /\ (IF jrnl # NoOne THEN disk' = jbase ELSE disk' = disk) + /\ jrnl' = NoOne /\ UNCHANGED jbase + /\ base' = [base EXCEPT !["d"] = (IF jrnl # NoOne THEN jbase ELSE disk)] + /\ SetPc("d", "staged") + /\ UNCHANGED <> +DAcqWs == pc["d"] = "staged" /\ wsLock = NoOne + /\ wsLock' = "d" /\ SetPc("d", "ws") + /\ UNCHANGED <> + +\* ---- apply: ID lock, freshness check, workspace lock, recovery, freshness check ---- AAcqId == pc["a"] = "start" /\ idLock = NoOne /\ idLock' = "a" /\ SetPc("a", "hasId") - /\ UNCHANGED <> + /\ UNCHANGED <> ACheck1 == pc["a"] = "hasId" /\ (IF disk = base["a"] THEN SetPc("a", "fresh1") /\ UNCHANGED <> ELSE SetPc("a", "rejected") /\ Release("a")) - /\ UNCHANGED <> + /\ UNCHANGED <> AAcqWs == pc["a"] = "fresh1" /\ wsLock = NoOne - /\ wsLock' = "a" /\ SetPc("a", "fresh2") - /\ UNCHANGED <> + /\ wsLock' = "a" /\ SetPc("a", "ws") + /\ 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 <> + THEN SetPc("a", "prep") /\ UNCHANGED <> + ELSE SetPc("a", "rejected") /\ Release("a")) + /\ UNCHANGED <> + +\* ---- journal recovery and journal write (shared) ---- +\* The new workspace-lock holder first rolls back a leftover journal, then +\* continues (direct: prepare; apply: second freshness check). +Recover(p) == pc[p] = "ws" + /\ (IF jrnl # NoOne THEN disk' = jbase ELSE disk' = disk) + /\ jrnl' = NoOne /\ UNCHANGED jbase + /\ SetPc(p, IF p = "d" THEN "prep" ELSE "fresh2") + /\ UNCHANGED <> +WriteJournal(p) == pc[p] = "prep" + /\ jrnl' = p /\ jbase' = disk \* backups are taken from the files as they are now + /\ todo' = [todo EXCEPT ![p] = Files] /\ done' = [done EXCEPT ![p] = {}] + /\ SetPc(p, "promote") + /\ UNCHANGED <> \* ---- promotion, failure, compensation (shared) ---- Promote(p) == pc[p] = "promote" /\ todo[p] # {} @@ -87,34 +118,37 @@ Promote(p) == pc[p] = "promote" /\ todo[p] # {} /\ disk' = [disk EXCEPT ![f] = base[p][f] + 1] /\ todo' = [todo EXCEPT ![p] = @ \ {f}] /\ done' = [done EXCEPT ![p] = @ \cup {f}] - /\ UNCHANGED <> + /\ UNCHANGED <> Commit(p) == pc[p] = "promote" /\ todo[p] = {} /\ SetPc(p, "committed") /\ Release(p) - /\ UNCHANGED <> + /\ jrnl' = NoOne \* removing the journal is the commit point + /\ UNCHANGED <> Fail(p) == pc[p] = "promote" /\ todo[p] # {} \* a failure_mode raised before the last file /\ SetPc(p, "rollback") - /\ UNCHANGED <> + /\ 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) + THEN \/ (disk' = [disk EXCEPT ![f] = jbase[f]] /\ UNCHANGED rbFailed) \/ (UNCHANGED disk /\ rbFailed' = TRUE) - ELSE disk' = [disk EXCEPT ![f] = base[p][f]] /\ UNCHANGED rbFailed - /\ UNCHANGED <> + ELSE disk' = [disk EXCEPT ![f] = jbase[f]] /\ UNCHANGED rbFailed + /\ UNCHANGED <> RolledBack(p) == pc[p] = "rollback" /\ done[p] = {} /\ SetPc(p, "rolledBack") /\ Release(p) - /\ UNCHANGED <> + /\ jrnl' = (IF rbFailed THEN jrnl ELSE NoOne) \* the journal is kept when compensation failed + /\ UNCHANGED <> Crash(p) == CanCrash /\ pc[p] = "promote" /\ SetPc(p, "crashed") /\ Release(p) - /\ UNCHANGED <> + /\ 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) + \/ DAcqId \/ DAcqEnum \/ DRecover \/ DAcqWs \/ AAcqId \/ ACheck1 \/ AAcqWs \/ ACheck2 + \/ \E p \in Procs : Recover(p) \/ WriteJournal(p) \/ Promote(p) \/ Commit(p) \/ Fail(p) + \/ Rollback(p) \/ RolledBack(p) \/ Crash(p) \/ Terminated Spec == Init /\ [][Next]_vars @@ -128,7 +162,10 @@ LocksHeldByActive == 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] +\* When no journal is pending, files move together; a pending journal is replayed by the next lock holder. +FilesConsistent == (Quiescent /\ jrnl = NoOne) => disk[1] = disk[2] +\* What a pending journal would restore is itself a consistent state. +Recoverable == jrnl # NoOne => jbase[1] = jbase[2] +\* Without crashes or failed compensation, no committed update is lost. 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 index ff5f366b..9dd4ade6 100644 --- 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 @@ -1,3 +1,3 @@ SPECIFICATION Spec CONSTANTS RollbackMayFail = TRUE CanCrash = TRUE -INVARIANTS PromotionExclusive LocksHeldByActive NoLostUpdate +INVARIANTS PromotionExclusive LocksHeldByActive Recoverable 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 index 46bde208..1abf576a 100644 --- a/docs/superpowers/specs/system-spec/evidence/formal/tlc-output.txt +++ b/docs/superpowers/specs/system-spec/evidence/formal/tlc-output.txt @@ -3,190 +3,39 @@ tla2tools.jar v1.7.4 sha256 936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b 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. + calculated (optimistic): val = 3.2E-16 +194 states generated, 156 distinct states found, 0 states left on queue. +The depth of the complete state graph search is 21. 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) +Finished in 00s at (2026-11-05 07:18:06) +##### B_rollback_may_fail.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 = 8.6E-16 +300 states generated, 232 distinct states found, 0 states left on queue. +The depth of the complete state graph search is 21. +The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 3 and the 95th percentile is 2). +Finished in 00s at (2026-11-05 07:18:07) +##### C_crash.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 = 1.9E-15 +422 states generated, 308 distinct states found, 0 states left on queue. +The depth of the complete state graph search is 21. +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-05 07:18:07) ##### 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. + calculated (optimistic): val = 3.6E-15 +574 states generated, 412 distinct states found, 0 states left on queue. +The depth of the complete state graph search is 21. 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) +Finished in 00s at (2026-11-05 07:18:08) +##### Mutation probes (temporary copies of the module, config C_crash.cfg; outputs not retained) +- direct compilation reads state without calling recover (DRecover does not roll back the journal): FilesConsistent violated (the pre-staging recovery is necessary) +- Recover inside promotion ignores the journal: no violation in the bounded model (that recovery is a backstop here: apply's freshness checks reject stale previews and direct already recovered before staging) +- Earlier probes (apply can commit, apply can be rejected, direct can commit, and removal of both apply freshness checks violating NoLostUpdate) applied to the pre-journal model and were not repeated. diff --git a/docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt b/docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt index c69fe032..4e554f45 100644 --- a/docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt +++ b/docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt @@ -1,11 +1,11 @@ ........................................................................ [ 23%] -....................................................................s... [ 47%] -........................................................................ [ 71%] -...........................................................sss.......... [ 94%] -.RR............... [100%] +....................................................................s... [ 46%] +........................................................................ [ 69%] +...........................................................sss.......... [ 92%] +....................... [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_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.6aigXnVLb3\\pt\\test_registry_rejects_symlinke0\\outside-docs.json' -> 'C:\\Users\\ktjn\\AppData\\Local\\Temp\\tmp.6aigXnVLb3\\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 +307 passed, 4 skipped in 31.30s diff --git a/docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml b/docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml index 2ad353a8..96c3af25 100644 --- a/docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml +++ b/docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml @@ -1 +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 +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.6aigXnVLb3\\pt\\test_registry_rejects_symlinke0\\outside-docs.json' -> 'C:\\Users\\ktjn\\AppData\\Local\\Temp\\tmp.6aigXnVLb3\\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 index 04c879c2..c9b9510c 100644 --- a/docs/superpowers/specs/system-spec/evidence/level2/web-level2.txt +++ b/docs/superpowers/specs/system-spec/evidence/level2/web-level2.txt @@ -3,7 +3,7 @@ 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) + Tests 28 passed (28) + Start at 07:21:09 + Duration 1.90s (transform 73ms, setup 47ms, import 362ms, tests 950ms, environment 1.53s) diff --git a/docs/superpowers/specs/system-spec/whole-product-level2.md b/docs/superpowers/specs/system-spec/whole-product-level2.md index 63491a75..6895d18d 100644 --- a/docs/superpowers/specs/system-spec/whole-product-level2.md +++ b/docs/superpowers/specs/system-spec/whole-product-level2.md @@ -7,8 +7,8 @@ | 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) | +| Python: 13 test modules across browser API/conformance/conversation, LSP conversation/integration/server, CLI compile/errors, registry IDs, file transaction, preview recovery (`-n 0`) | 307 passed, 4 skipped | [txt](evidence/level2/python-level2.txt), [JUnit](evidence/level2/python-level2.xml) | +| Web (vitest): workspace repository, persistent-workspace hook, workspace model, recovery UI | 28 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. diff --git a/docs/superpowers/specs/system-spec/whole-product-level3.md b/docs/superpowers/specs/system-spec/whole-product-level3.md index 762e3475..301c5015 100644 --- a/docs/superpowers/specs/system-spec/whole-product-level3.md +++ b/docs/superpowers/specs/system-spec/whole-product-level3.md @@ -25,7 +25,7 @@ Release diagnostics dropped from six missing verification categories to three. ` ## 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. +- **Formal model:** now done as a bounded TLC model; see the next section. The model was updated for the promotion journal; crash-atomicity and failed-compensation behavior are still not guaranteed (see the model results). - **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). @@ -33,9 +33,9 @@ Release diagnostics dropped from six missing verification categories to three. ` ## 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. +- Model: two processes (direct, apply), two destination files, ID/enum/workspace locks, freshness checks, promotion journal and recovery by the next workspace-lock holder, per-file promotion, failure and compensation, optional crash. Assumptions are in the module header. The journal exists only in the working tree after the pinned revision, so the model describes that code. +- Results: configs A (no faults), B (compensation may fail), C (crash mid-promotion) and D (both; safety invariants) all pass exhaustively (194, 300, 422 and 574 states, no deadlock). An earlier model of the journal alone still violated `FilesConsistent` in B and C because a direct compilation staged ledger state before recovery; the code now calls `FileTransaction.recover()` before staging (DRecover in the model). Mutation probes: removing that recovery violates `FilesConsistent`; making in-promotion recovery ignore the journal does not (it is a backstop in this bounded model). Not modeled: a crash during preparation or recovery, more than two processes, PID reuse. Earlier probes from the pre-journal model were not repeated. +- Spec binding: MOD-PROD-10 (concurrency, `model-check`, passed) and MOD-PROD-11 (resilience, `model-check`, now passing; status left `specified` for maintainers) 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 diff --git a/docs/superpowers/specs/system-spec/whole-product.yaml b/docs/superpowers/specs/system-spec/whole-product.yaml index 9748be9c..9f1246d9 100644 --- a/docs/superpowers/specs/system-spec/whole-product.yaml +++ b/docs/superpowers/specs/system-spec/whole-product.yaml @@ -308,7 +308,7 @@ risks: - {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)" + environment: "Windows; CPython 3.14.5; pytest 9.1.1; 307 passed, 4 skipped" criteria: - Registry IDs are never reassigned once allocated. requirement_id: MOD-PROD-01 @@ -318,16 +318,16 @@ evidence: 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 + subject_revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: - docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 70bc4fb81cc7dcd5bd4c15ff51cb4bb2f5a452d033e9d3a16790700538a80aba - docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: 10397146c4a586399b55aa4b1e2878b3a7e971be1b0af97cacf969ec47144561 + docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 8e71367d6459c0028f709f814b96f3c72e4144574be28c15c7dd62e0485b2fda + docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: be8fd7e5faced7388ee46e633bf9323c04e5b1f1d3801bd7d03dbb58938fa9c5 cli/tests/test_registry_ids.py: 24d66db6bac6e6b39c2d8f28a02c60c9a357acdcf04c164ed1954d7f30ba76c8 - timestamp: "2026-11-04" + timestamp: "2026-11-05" 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)" + environment: "Windows; CPython 3.14.5; pytest 9.1.1; 307 passed, 4 skipped" criteria: - Known compilation operational failures render as CLI errors with nonzero status. requirement_id: MOD-PROD-02 @@ -337,16 +337,16 @@ evidence: 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 + subject_revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: - docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 70bc4fb81cc7dcd5bd4c15ff51cb4bb2f5a452d033e9d3a16790700538a80aba - docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: 10397146c4a586399b55aa4b1e2878b3a7e971be1b0af97cacf969ec47144561 + docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 8e71367d6459c0028f709f814b96f3c72e4144574be28c15c7dd62e0485b2fda + docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: be8fd7e5faced7388ee46e633bf9323c04e5b1f1d3801bd7d03dbb58938fa9c5 cli/tests/test_cli_compilation_errors.py: f50ac380689c416c54999bd5b106fa3e8dbc42056a5f44c39b718531b1d3e820 - timestamp: "2026-11-04" + timestamp: "2026-11-05" 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)" + environment: "Windows; CPython 3.14.5; pytest 9.1.1; 307 passed, 4 skipped" criteria: - A failed conversation preview keeps the existing pending action over the language-server conversation service. requirement_id: MOD-PROD-03 @@ -356,16 +356,16 @@ evidence: 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 + subject_revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: - docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 70bc4fb81cc7dcd5bd4c15ff51cb4bb2f5a452d033e9d3a16790700538a80aba - docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: 10397146c4a586399b55aa4b1e2878b3a7e971be1b0af97cacf969ec47144561 + docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 8e71367d6459c0028f709f814b96f3c72e4144574be28c15c7dd62e0485b2fda + docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: be8fd7e5faced7388ee46e633bf9323c04e5b1f1d3801bd7d03dbb58938fa9c5 cli/tests/test_conversation_preview_recovery.py: 02c7881dbc5dd358bc64779d634a980a9d2061e0dea1c4a86f05c97bc4d5f795 - timestamp: "2026-11-04" + timestamp: "2026-11-05" 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)" + environment: "Windows; CPython 3.14.5; pytest 9.1.1; 307 passed, 4 skipped" criteria: - Native and browser compilation snapshots are deterministic for the same scenarios. requirement_id: MOD-PROD-04 @@ -375,16 +375,16 @@ evidence: 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 + subject_revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: - docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 70bc4fb81cc7dcd5bd4c15ff51cb4bb2f5a452d033e9d3a16790700538a80aba - docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: 10397146c4a586399b55aa4b1e2878b3a7e971be1b0af97cacf969ec47144561 + docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 8e71367d6459c0028f709f814b96f3c72e4144574be28c15c7dd62e0485b2fda + docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: be8fd7e5faced7388ee46e633bf9323c04e5b1f1d3801bd7d03dbb58938fa9c5 cli/tests/test_browser_conformance.py: 6ee86288dfd252a670cf6d3ccecaa501a126e54bac8f7f7dfde08f883a7a808a - timestamp: "2026-11-04" + timestamp: "2026-11-05" 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)" + environment: "Windows; Node v26.13.0; vitest 4.1.10; 28 passed (4 files)" criteria: - The workspace repository does not overwrite a stored record with a greater revision. requirement_id: MOD-PROD-05 @@ -394,15 +394,15 @@ evidence: 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 + subject_revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: - docs/superpowers/specs/system-spec/evidence/level2/web-level2.txt: ed7902e0714270e12d16b7ba3fb6ae7f3b5ad66d8fef0de0e61583e33c81091e + docs/superpowers/specs/system-spec/evidence/level2/web-level2.txt: de7aa5fb8350d2b38760cf44a41f85e1c4b73c55384193f73621c714ac628c8f web/src/workspace-repository.test.ts: 4e62b239f2ab4d4b8bc61eb6d18def7ca537aed62efe7d67c6ddbb3eecc8584f - timestamp: "2026-11-04" + timestamp: "2026-11-05" 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)" + environment: "Windows; CPython 3.14.5; pytest 9.1.1; 307 passed, 4 skipped" criteria: - The registry ID ledger round-trips through its JSON file sorted by id. requirement_id: MOD-PROD-07 @@ -412,16 +412,16 @@ evidence: 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 + subject_revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: - docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 70bc4fb81cc7dcd5bd4c15ff51cb4bb2f5a452d033e9d3a16790700538a80aba - docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: 10397146c4a586399b55aa4b1e2878b3a7e971be1b0af97cacf969ec47144561 + docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 8e71367d6459c0028f709f814b96f3c72e4144574be28c15c7dd62e0485b2fda + docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: be8fd7e5faced7388ee46e633bf9323c04e5b1f1d3801bd7d03dbb58938fa9c5 cli/tests/test_registry_ids.py: 24d66db6bac6e6b39c2d8f28a02c60c9a357acdcf04c164ed1954d7f30ba76c8 - timestamp: "2026-11-04" + timestamp: "2026-11-05" 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)" + environment: "Windows; CPython 3.14.5; pytest 9.1.1; 307 passed, 4 skipped" criteria: - Registry ID ledger access is serialized across processes by the ledger lock. requirement_id: MOD-PROD-08 @@ -431,16 +431,16 @@ evidence: 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 + subject_revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: - docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 70bc4fb81cc7dcd5bd4c15ff51cb4bb2f5a452d033e9d3a16790700538a80aba - docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: 10397146c4a586399b55aa4b1e2878b3a7e971be1b0af97cacf969ec47144561 + docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 8e71367d6459c0028f709f814b96f3c72e4144574be28c15c7dd62e0485b2fda + docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: be8fd7e5faced7388ee46e633bf9323c04e5b1f1d3801bd7d03dbb58938fa9c5 cli/tests/test_registry_ids.py: 24d66db6bac6e6b39c2d8f28a02c60c9a357acdcf04c164ed1954d7f30ba76c8 - timestamp: "2026-11-04" + timestamp: "2026-11-05" 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)" + environment: "Windows; CPython 3.14.5; pytest 9.1.1; 307 passed, 4 skipped" criteria: - A promoted file whose hash does not verify is rolled back by the file transaction. requirement_id: MOD-PROD-09 @@ -450,12 +450,12 @@ evidence: 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 + subject_revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb 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" + docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 8e71367d6459c0028f709f814b96f3c72e4144574be28c15c7dd62e0485b2fda + docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: be8fd7e5faced7388ee46e633bf9323c04e5b1f1d3801bd7d03dbb58938fa9c5 + cli/tests/test_file_transaction.py: 7757da8d9f92b697d9eeda58aa71f372b84db762ee6f4e3f5c16476e056cabaa + timestamp: "2026-11-05" 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 @@ -469,15 +469,15 @@ evidence: provenance: "tla+::docs/superpowers/specs/system-spec/evidence/formal/CompilationProtocol.tla" subject_id: local-contract-toolchain subject_version: "1.0" - subject_revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + subject_revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb 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" + docs/superpowers/specs/system-spec/evidence/formal/CompilationProtocol.tla: bcfd020946a0439f8b98c0bbfbe01da6cfbabb91743b7e350c4c28d000eace65 + docs/superpowers/specs/system-spec/evidence/formal/A_no_faults.cfg: 3a047430c4b4260ce9ea0f867956515b39519a1025eb82d4314cce52b277bd21 + docs/superpowers/specs/system-spec/evidence/formal/D_all_faults_safety.cfg: 1851cc2f6b8155f53f5ade855fcff0b669c41515c2026de0e5de94066ccbcb88 + docs/superpowers/specs/system-spec/evidence/formal/tlc-output.txt: 562deb7f51390aff5da77cb028c35d0602ba7c4507f85ab389a4f1dd88b01097 + timestamp: "2026-11-05" 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." + 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, 194 and 574 states. The model includes the promotion journal and recovery added in the working tree after this revision (file_transaction.py), so it describes that code, not the pinned revision. 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: @@ -485,47 +485,47 @@ evidence: requirement_id: MOD-PROD-11 requirement_version: "1.0" method: model-check - passed: false + 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 + subject_revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: - docs/superpowers/specs/system-spec/evidence/formal/CompilationProtocol.tla: dd505b32cb8fd23cb42fe93167bd9199eec063561f0ae70241defd1a49825d4e + docs/superpowers/specs/system-spec/evidence/formal/CompilationProtocol.tla: bcfd020946a0439f8b98c0bbfbe01da6cfbabb91743b7e350c4c28d000eace65 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" + docs/superpowers/specs/system-spec/evidence/formal/C_crash.cfg: db56af8fab6ef072f2135020826e6efb3b9d823447d65b67022c0f0455baeaff + docs/superpowers/specs/system-spec/evidence/formal/tlc-output.txt: 562deb7f51390aff5da77cb028c35d0602ba7c4507f85ab389a4f1dd88b01097 + timestamp: "2026-11-05" 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." + bounds: "Same bounds. Configs B (compensation may fail) and C (crash mid-promotion) pass exhaustively (300 and 422 states) with the promotion journal, recovery by the next lock holder, and direct compilation recovering before it stages. An earlier model without the pre-staging recovery had counterexamples in B and C; a mutant that removes that recovery violates FilesConsistent again. Not modeled: a crash during preparation or during recovery, more than two processes, PID reuse. A bounded model of the working-tree code, not a proof of the implementation." subject_bindings: local-contract-toolchain: version: "1.0" - revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: cli/src/modelable/registry/ids.py: 7d0a7b260ae780ed338a6073c428407d84e56d88f0ec8e631b4538de6b801069 - cli/src/modelable/operations/file_transaction.py: 628fe1a047fb8ecd682ba5eb2f1d1545665f84dd90a4038da1e6a6e5e3785794 - cli/src/modelable/operations/compilation.py: b003590e348e061f684a9f78b98a9ae61e8f8748afb3f8ff324e3df04f7d7cc3 + cli/src/modelable/operations/file_transaction.py: 882f5272e813eb0e5e74768d4c90551a3bcdf43b38339d5648913884414f6963 + cli/src/modelable/operations/compilation.py: e97c6b06adf258771e272f6232f6596ee79f9d437699c52064be062566d24eaf native-command-workflows: version: "1.0" - revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: - cli/src/modelable/commands/compile.py: 004ae26dfab6174fb3b9a73b5d4021a9ea5d36671662b7f4e54dd832db7490e8 + cli/src/modelable/commands/compile.py: 3abb2bde882c61e6edf4630c8380160f41140d6ff22366cc743fe8d2362c37f6 desktop-language-and-conversation: version: "1.0" - revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: cli/src/modelable/llm/filesystem_conversation.py: aafb5a26a9c4993505548be98b23fd144fe24f8685824261f2a7753b9fc2065f - cli/src/modelable/lsp/conversation_service.py: d492a25393150aa90273c546643a1560004ae803e550bb1e31383e3a389e78fe + cli/src/modelable/lsp/conversation_service.py: 4dd86850a4b8b846ef23ce58ba55c924c4c8a50df93e480f88a7f48d721924d4 browser-compiler-api: version: "1.0" - revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: cli/src/modelable/browser/api.py: 47074420dc6f630d401e0f2514ecd0d183b42580f56eae5e5cbcc6afe98f9dfd cli/src/modelable/browser/dispatch.py: f83e38aa01c9636f370d75c23b819e0912df654d763dc7fd9628c31e6e18fd13 playground-workspace: version: "1.0" - revision: dbd8807977bafdfdd4981596045a2cbdaab12efb + revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: web/src/workspace-repository.ts: f9604c1768e472faab787efb2192ceb40e3f614c5fe2b0a6d5ff74c3a970ac39 - web/src/usePersistentWorkspace.ts: 36fac0e43a22cca18d66ec629821abf9eeb2cfaae2e601660dd0ec8b00057b6c + web/src/usePersistentWorkspace.ts: d6b68d38829618fdd1b943f35909c60d01ce895d685b2032bfb6cbfc2a35b7e3 From 6e3cf5c1fc1f9c4e80294225765acc37189aa2e2 Mon Sep 17 00:00:00 2001 From: ktjn Date: Thu, 5 Nov 2026 07:22:16 +0100 Subject: [PATCH 4/5] docs: pin whole-product source hashes to LF blobs Matches compilation.yaml; CRLF working copies on Windows will not verify. Co-Authored-By: Claude Sonnet 5.5 --- .../specs/system-spec/whole-product.yaml | 36 +++++++++---------- 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/docs/superpowers/specs/system-spec/whole-product.yaml b/docs/superpowers/specs/system-spec/whole-product.yaml index 9f1246d9..2a401afc 100644 --- a/docs/superpowers/specs/system-spec/whole-product.yaml +++ b/docs/superpowers/specs/system-spec/whole-product.yaml @@ -322,7 +322,7 @@ evidence: artifacts: docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 8e71367d6459c0028f709f814b96f3c72e4144574be28c15c7dd62e0485b2fda docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: be8fd7e5faced7388ee46e633bf9323c04e5b1f1d3801bd7d03dbb58938fa9c5 - cli/tests/test_registry_ids.py: 24d66db6bac6e6b39c2d8f28a02c60c9a357acdcf04c164ed1954d7f30ba76c8 + cli/tests/test_registry_ids.py: cffb020d4d2fc1980c1a7988aed8799b2b7e617b0088c2bbc5abec7723400ae8 timestamp: "2026-11-05" 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." @@ -341,7 +341,7 @@ evidence: artifacts: docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 8e71367d6459c0028f709f814b96f3c72e4144574be28c15c7dd62e0485b2fda docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: be8fd7e5faced7388ee46e633bf9323c04e5b1f1d3801bd7d03dbb58938fa9c5 - cli/tests/test_cli_compilation_errors.py: f50ac380689c416c54999bd5b106fa3e8dbc42056a5f44c39b718531b1d3e820 + cli/tests/test_cli_compilation_errors.py: 4acdf153840682d3db98a8a4c16e115ae13b7b7bef9c663bfc9cc26b1ce6a235 timestamp: "2026-11-05" 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." @@ -360,7 +360,7 @@ evidence: artifacts: docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 8e71367d6459c0028f709f814b96f3c72e4144574be28c15c7dd62e0485b2fda docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: be8fd7e5faced7388ee46e633bf9323c04e5b1f1d3801bd7d03dbb58938fa9c5 - cli/tests/test_conversation_preview_recovery.py: 02c7881dbc5dd358bc64779d634a980a9d2061e0dea1c4a86f05c97bc4d5f795 + cli/tests/test_conversation_preview_recovery.py: d5f2dfa0d29c0302af3c8f92eb8371bc9f697e1fcbcfe3482252db6302b380c6 timestamp: "2026-11-05" 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." @@ -379,7 +379,7 @@ evidence: artifacts: docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 8e71367d6459c0028f709f814b96f3c72e4144574be28c15c7dd62e0485b2fda docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: be8fd7e5faced7388ee46e633bf9323c04e5b1f1d3801bd7d03dbb58938fa9c5 - cli/tests/test_browser_conformance.py: 6ee86288dfd252a670cf6d3ccecaa501a126e54bac8f7f7dfde08f883a7a808a + cli/tests/test_browser_conformance.py: 34461c2448cb1057173e4a792c0be44b044a09ba9abf65e767d66dc86ec23583 timestamp: "2026-11-05" 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." @@ -397,7 +397,7 @@ evidence: subject_revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: docs/superpowers/specs/system-spec/evidence/level2/web-level2.txt: de7aa5fb8350d2b38760cf44a41f85e1c4b73c55384193f73621c714ac628c8f - web/src/workspace-repository.test.ts: 4e62b239f2ab4d4b8bc61eb6d18def7ca537aed62efe7d67c6ddbb3eecc8584f + web/src/workspace-repository.test.ts: 3914e3c5751d0b0f0c51a5c87d14b0b1c43e7474d286aea1da19f30cb87b6da7 timestamp: "2026-11-05" 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." @@ -416,7 +416,7 @@ evidence: artifacts: docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 8e71367d6459c0028f709f814b96f3c72e4144574be28c15c7dd62e0485b2fda docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: be8fd7e5faced7388ee46e633bf9323c04e5b1f1d3801bd7d03dbb58938fa9c5 - cli/tests/test_registry_ids.py: 24d66db6bac6e6b39c2d8f28a02c60c9a357acdcf04c164ed1954d7f30ba76c8 + cli/tests/test_registry_ids.py: cffb020d4d2fc1980c1a7988aed8799b2b7e617b0088c2bbc5abec7723400ae8 timestamp: "2026-11-05" verifier: "CPython 3.14.5; pytest 9.1.1; Windows" bounds: "Single named test only; the suite totals are in the retained output." @@ -435,7 +435,7 @@ evidence: artifacts: docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 8e71367d6459c0028f709f814b96f3c72e4144574be28c15c7dd62e0485b2fda docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: be8fd7e5faced7388ee46e633bf9323c04e5b1f1d3801bd7d03dbb58938fa9c5 - cli/tests/test_registry_ids.py: 24d66db6bac6e6b39c2d8f28a02c60c9a357acdcf04c164ed1954d7f30ba76c8 + cli/tests/test_registry_ids.py: cffb020d4d2fc1980c1a7988aed8799b2b7e617b0088c2bbc5abec7723400ae8 timestamp: "2026-11-05" verifier: "CPython 3.14.5; pytest 9.1.1; Windows" bounds: "Single named test only; the suite totals are in the retained output." @@ -454,7 +454,7 @@ evidence: artifacts: docs/superpowers/specs/system-spec/evidence/level2/python-level2.xml: 8e71367d6459c0028f709f814b96f3c72e4144574be28c15c7dd62e0485b2fda docs/superpowers/specs/system-spec/evidence/level2/python-level2.txt: be8fd7e5faced7388ee46e633bf9323c04e5b1f1d3801bd7d03dbb58938fa9c5 - cli/tests/test_file_transaction.py: 7757da8d9f92b697d9eeda58aa71f372b84db762ee6f4e3f5c16476e056cabaa + cli/tests/test_file_transaction.py: e64f21fc56037e5f84d28e5b6c322808fd037bd725c3cf28db19494892f1cadf timestamp: "2026-11-05" verifier: "CPython 3.14.5; pytest 9.1.1; Windows" bounds: "Single named test only; the suite totals are in the retained output." @@ -503,29 +503,29 @@ subject_bindings: version: "1.0" revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: - cli/src/modelable/registry/ids.py: 7d0a7b260ae780ed338a6073c428407d84e56d88f0ec8e631b4538de6b801069 - cli/src/modelable/operations/file_transaction.py: 882f5272e813eb0e5e74768d4c90551a3bcdf43b38339d5648913884414f6963 - cli/src/modelable/operations/compilation.py: e97c6b06adf258771e272f6232f6596ee79f9d437699c52064be062566d24eaf + cli/src/modelable/registry/ids.py: 9c1053d0f8927b66b04d1b1a1df4bd841fabc1ffb00a41eccc3ca6322956aa3b + cli/src/modelable/operations/file_transaction.py: 041988323be33210b958b79072302e3d974f00233705da212c437b8794fdec7c + cli/src/modelable/operations/compilation.py: b5bf90092d9b9d1503c4a791bdf0c7b9a72cadb7e810f186a68c223d35b65e1f native-command-workflows: version: "1.0" revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: - cli/src/modelable/commands/compile.py: 3abb2bde882c61e6edf4630c8380160f41140d6ff22366cc743fe8d2362c37f6 + cli/src/modelable/commands/compile.py: 004ae26dfab6174fb3b9a73b5d4021a9ea5d36671662b7f4e54dd832db7490e8 desktop-language-and-conversation: version: "1.0" revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: - cli/src/modelable/llm/filesystem_conversation.py: aafb5a26a9c4993505548be98b23fd144fe24f8685824261f2a7753b9fc2065f - cli/src/modelable/lsp/conversation_service.py: 4dd86850a4b8b846ef23ce58ba55c924c4c8a50df93e480f88a7f48d721924d4 + cli/src/modelable/llm/filesystem_conversation.py: 5f287fcb78cedc8b127ebb51958c715fa421bdf048090ca96a3b34afd61e0082 + cli/src/modelable/lsp/conversation_service.py: d492a25393150aa90273c546643a1560004ae803e550bb1e31383e3a389e78fe browser-compiler-api: version: "1.0" revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: - cli/src/modelable/browser/api.py: 47074420dc6f630d401e0f2514ecd0d183b42580f56eae5e5cbcc6afe98f9dfd - cli/src/modelable/browser/dispatch.py: f83e38aa01c9636f370d75c23b819e0912df654d763dc7fd9628c31e6e18fd13 + cli/src/modelable/browser/api.py: 066eeae1a89af090c436fdaf00771dd7d7871d9528ae7d8690904efcd4d3bf4e + cli/src/modelable/browser/dispatch.py: 15ecc536c6721368c5917add0148364fab4b55c0c418c9da07217045ae0afa2a playground-workspace: version: "1.0" revision: 68d8cf8ccabb7e3797c949c402d82d31e05279eb artifacts: - web/src/workspace-repository.ts: f9604c1768e472faab787efb2192ceb40e3f614c5fe2b0a6d5ff74c3a970ac39 - web/src/usePersistentWorkspace.ts: d6b68d38829618fdd1b943f35909c60d01ce895d685b2032bfb6cbfc2a35b7e3 + web/src/workspace-repository.ts: ce9eb8723e639e82cdd56078841411065a58ee86df5c348a94b5748f8e353adf + web/src/usePersistentWorkspace.ts: 1bc6322a09e41c34ea63b3571c1837e9e620f72542e5a2db4f6bcbdb01faac6a From 44f2d48b4ad48b69bb3af0494a4fe78a7df05e60 Mon Sep 17 00:00:00 2001 From: ktjn Date: Thu, 5 Nov 2026 07:31:19 +0100 Subject: [PATCH 5/5] test: follow the setup-uv bump in the release-prep workflow test The dependabot bump to v10.3.3 updated every workflow but left this assertion on v10.3.2, so the full suite and the pre-push gate failed. Co-Authored-By: Claude Sonnet 5.5 --- cli/tests/test_release_workflow.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cli/tests/test_release_workflow.py b/cli/tests/test_release_workflow.py index 4e40a844..92f2c034 100644 --- a/cli/tests/test_release_workflow.py +++ b/cli/tests/test_release_workflow.py @@ -195,7 +195,7 @@ def test_release_prep_is_manual_dispatch_with_version_input() -> None: steps = workflow["jobs"]["prepare"]["steps"] assert any( - step.get("uses") == "astral-sh/setup-uv@v10.3.2" + step.get("uses") == "astral-sh/setup-uv@v10.3.3" and step.get("with", {}).get("cache-dependency-glob") == "cli/uv.lock" for step in steps )