diff --git a/docs/plans/VSH-ROUTE-PLAN-2026-11-04.adoc b/docs/plans/VSH-ROUTE-PLAN-2026-11-04.adoc new file mode 100644 index 0000000..96d4eff --- /dev/null +++ b/docs/plans/VSH-ROUTE-PLAN-2026-11-04.adoc @@ -0,0 +1,778 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += valence-shell: route plan (proof-first), architecture, and ultracode session plan +Jonathan Jewell (hyperpolymath) +:toc: left +:toc-title: Contents +:doctype: article +:icons: font +:sectanchors: + +*Date:* 2026-11-04 +*Status:* PLAN. Nothing in it is implemented yet. + +*Scope of this document:* the gates state the *properties* the implementation must meet, together with the measured failures and regressions that test them. The full protocol specifications are not in this document. They are drafted in session 1 Phase 5, must refine these gates, and are reviewed in their own PRs: + +* the containment threat model: attacker capabilities, path resolution, links, mounts and ownership; +* the journal and recovery protocol; +* the file-identity rules; +* the OS-assumption ledger. + +Review findings at that level of detail are recorded here as gate requirements and carried into those specifications. +*Basis:* valence-shell `main` @ `295c3ca`, plus 14 sibling repos (read-only). Reconciled with `ce16ce3` (#221, merged 2026-11-01), which changed docs, proofs and banner text but no shell behaviour. The runtime findings were re-run against it. + +*Revision 2026-11-05:* this revision adds the symlink-escape failure (j) found in review. It also scopes G6, defines nested-root locking, makes the G5 write alphabet finite, and builds P5 on the Agda tree that #221 repaired. + +*How the evidence was gathered:* + +* An ultracode workflow ran 50 agents, all of which completed: +** 8 repo readers; +** 4 route architects (proof-first, engineering-first, verified-subset, contrarian); +** 3 judges; +** a synthesis, followed by an adversarial pass. That pass extracted 16 load-bearing claims and gave each to 2 independent skeptics. 12 claims survived, and 4 were refuted in part (C06, C07, C11, C14; corrections are applied below). +** A final critic, which found 3 new high-severity runtime bugs. +* I re-ran those 3 bugs, plus two others, in the planning session. + +*Evidence grades used throughout:* + +* *Measured*: a command was run or a file read in the planning session. +* *Inference*: reasoned from measured facts. +* *Unverified*: not checked. This includes every prover-side claim. Only `cargo` and `rustc` were installed, so no Lean, Coq, Agda, Idris2 or Z3 run happened during planning. + +== Owner rulings (2026-11-04) + +[cols=",,",options="header",] +|=== +|# |Ruling |Effect on this plan +|*OD-0* |*Proof-first* is the spine. This is the elegant arm (judges' mean E 8.7 / D 6.7). |One canonical, decidable, finite spec in Lean. The shipped Rust core is to be mechanically proven to refine it (Aeneas). A second, independent, in-repo witness comes from a `--safe --without-K` Agda finite-map mirror. A golden-trace corpus is the explicit seam, checked by Rust, Lean `decide` and Agda `refl`. Coq, Isabelle and Mizar are archived *only after* their unique content is ported and the witness threshold holds without them. +|*OD-22* |The v1 gate "all reversible operations proven across the six proof systems" becomes a *witness-coverage threshold*. |Every `OperationType` needs *≥2 independent CI-gated provers plus the differential oracle*. The count is computed from a generated `proofs/MANIFEST.toml` (frontier D-5). This is the formal guard on archival. +|*OD-23* |*No theory-feeder import until G1–G5 are green.* After that, use echo-types `EchoResidueCell` + `EchoDeniability` if the Agda pin experiment passes, otherwise residual-evidence `Core` + epistemic `Warrant`. |The in-repo Agda mirror is not a feeder import, so it proceeds. absolute-zero `CNOInterface`, echo-types, residual-evidence and epistemic edges move to the session *after* G1–G5. +|*OD-22a* (2026-11-05) |*HardwareErase is excluded from G6 until it is wired* into the parser and executor. This is the elegant arm (E 9 / D 8), chosen over approving an oracle exemption (E 6 / D 7), wiring it in session 2 (E 8 / D 6) and retiring the variant (E 7 / D 9). |G6 counts only operations the shell runs; there is no `exempt` oracle column. The Lean port of the Idris2 HardwareErase statement is dropped from session 1. HardwareErase re-enters G6 with the full gate (≥2 provers plus the oracle) once it is wired. +|— |Commit this plan and open a draft PR. Wait for the owner's go before running the implementation workflows. |This document. +|=== + +*Why proof-first still fixes runtime holes first.* The proof-first architect's own thesis orders the work as "holes come first (rungs 0–1), wiring next (CI lanes before claims), features last". It also argues that the drift guard and the WAL are _proof-necessary_: they discharge, at runtime, the one hypothesis a refinement proof cannot cover, namely that the real OS state equals the abstract state. So the Rust hole fixes (Phase 1) are part of the spine, not a departure from it. They also touch disjoint files from the Lean work (Phase 2), so the two run in parallel and the proofs are not held up. + +''''' + +== 0. Bottom line + +[arabic] +. *The spec has to mean what it says.* +* The Lean `isEmptyDir` quantifies over ancestors, so `RmdirPrecondition` is (Inference) uninhabited and the Lean rmdir theorems are vacuous. +* The same vacuity class exists in Idris2 (the hypothesis equals the conclusion), Agda (emptiness is missing) and Z3 (the predicate is uninterpreted). +* CI builds at most 4 of the 12 Lean libraries, and 4 libraries are self-declared broken. ++ +Fix all of this first, and make every precondition carry a checked non-vacuity witness. +. *One canonical finite spec.* `FinFS` is a Mathlib-free, decidable finite map with a proved refinement to the current function model. Three things run over it: +* the differential oracle, extended with undo, redo and transactions; +* a golden-trace corpus checked three ways (Rust tests, Lean `decide`, Agda `refl`); +* an in-repo Agda mirror, which serves as the second independent witness. +. *Prove that the shipped Rust refines the spec.* Extract a pure `vsh-core` crate. Run a Charon/Aeneas spike with a 2-session kill rule. If it passes, the refinement theorem becomes F-1's closure. +*The runtime must discharge what the proof assumes.* Fourteen safety failures reproduce today through ordinary `vsh -c` commands (§3.2): +* undo after `cd` deletes the wrong file; +* `cd ..` escapes the sandbox, and so do `>`, `touch`, `mkdir` and the `mv` destination through in-root symlinks; +* `obliterate` on an in-root symlink or hard link destroys the *outside* file's contents; +* a 0600 file comes back as 0644, and its bytes sit in a world-readable state file; +* obliterate in a transaction is reported as rolled back; +* three arithmetic expressions panic; +* obliterate writes its audit record after the irreversible step. ++ +These are fixed in Phase 1, in parallel with the Lean work, together with the drift guard and a single shared inverse table. The durability journal (WAL) and its crash-recovery theorem follow in the next session. +. *Feeders wait for G1–G5.* The estate theory attaches later through the same Agda layer. +. *Archival is gated by witnesses.* Coq, Isabelle and Mizar are archived (never deleted) only once Lean and Agda between them give every op ≥2 witnesses. + +''''' + +== 1. The done-definition: "valence-shell v1.0-honest" (proof-first) + +Every gate below is a required CI check on `main` with a recorded job id. No admin override is allowed. *Session* is the first session in which the gate can close. + +[cols=",,,",options="header",] +|=== +|Gate |Done when |Status today (Measured) |Session +|*G1 Safety* a|Every case in §3.2 passes through the parsed `vsh -c` path. There is one inverse table for undo, redo and rollback. Ops with no inverse are hard failures in rollback. Obliterate is refused inside a txn. The drift guard stores both fingerprints of each op. It checks the post-state fingerprint before undo and the pre-state fingerprint before redo, because redo runs against the restored pre-state. The undo payload carries the entry kind (with a symlink's `readlink` target), mode, owner and mtime. The session root is fixed and separate from cwd. Every mutation target is contained *after resolution*, not just lexically, with a *per-operation follow policy*: + +* *Content operations* (write, append, truncate, redirection, chmod, chown, the cp destination, and *obliterate*) resolve the full path beneath the session root and refuse a target that escapes. Obliterate in particular must never overwrite through a symlink: it opens the target with no-follow semantics beneath the root and refuses a symlink or escaping target before any byte is written. +* *Hard links.* Symlink-safe resolution cannot detect them, so every content operation `fstat`s the opened descriptor. A regular file with `st_nlink > 1` is refused by every content operation, unconditionally. No override flag exists, because an override would bypass the only check that can see the alias. The check is made on the descriptor and repeated with a second `fstat` after the write, the overwrite or the metadata change (`chmod`, `chown`). If the link count changed in between, the op fails loudly and its record gets a *tainted* flag, which is separate from its loss grade; for obliterate, the completion residue records that an alias appeared. *Scope of this guarantee:* it covers aliases that exist when vsh checks, which includes every alias planted in the root beforehand. It does not prevent a *concurrent* same-uid process from creating an alias inside the check-to-write window; that is detected after the fact, not prevented, and only if the alias still exists at the second check: an alias created and removed again inside the window leaves the link count unchanged and is not detected (by then no outside name remains attached to the written inode). Such a process already holds write authority over the outside file, so no privilege boundary is crossed. Other users cannot race this way where `fs.protected_hardlinks=1` (recorded in OS-ASSUMPTIONS). The race is closed fully only by the stronger, optional boundary: a session root on its own filesystem, where an outside hard-link alias cannot exist at all. Users who need to edit hard-linked files use that boundary too. Regression: a test-only hook links the target between check and write, and the op reports the alias and its record carries the tainted flag. The same test runs for `chmod` and `chown`, with the hook placed between the first check and the metadata change. +* *Directory-entry operations* (rm, rmdir, *mkdir*, *touch/create*, ln, unlink, and *both the mv source and the mv destination*) resolve the parent beneath the root, refusing any parent component that escapes. They then act on the entry itself with `mkdirat`, `openat(O_CREAT\|O_EXCL\|O_NOFOLLOW)`, `unlinkat` or `renameat`, and never follow a final symlink. `rm link` therefore removes the link and leaves the referent alone, as it does today. + +Resolution uses `openat2(RESOLVE_BENEATH \| RESOLVE_NO_XDEV)`, or an `O_NOFOLLOW` component walk where that is unavailable. The walk compares each component's mount id (`statx` `STATX_MNT_ID`) with the root's, so a bind mount of an outside directory inside the root is refused, not crossed. A privileged CI regression bind-mounts an outside directory into the root and checks that writes and obliterate through it are refused. If neither `openat2` nor `STATX_MNT_ID` is available (Linux before 5.8), vsh refuses mutations rather than run unchecked. *Platform scope:* the G1 containment guarantee is gated on Linux. macOS, which `compilation_tests.yml` still builds, has neither call. There the walk compares each component's `st_dev` with the root's (`fstatat` with `AT_SYMLINK_NOFOLLOW`); macOS has no bind mounts, so entering another mount changes `st_dev`. A macOS regression attaches a disk image (`hdiutil attach`) mounted inside the root and checks that writes through it are refused. Until that regression is green, the macOS release artefact is withdrawn from the v1 release rather than shipped without containment. `eval_arith` never panics (proptest under both debug and release profiles). |14 safety regressions reproduce |1 +|*G2 Durability* |State lives in `$XDG_STATE_HOME/vsh//`, mode 0700, files 0600. *Migration from the in-root file:* when a session starts on a root that still holds a legacy `.vsh_state.json`, vsh opens it with `O_NOFOLLOW`, checks it as E1d does, copies it into the new store with temp-fsync-rename, parses the copy back, and only then unlinks the in-root file and syncs the root directory. Any failure before the unlink leaves the in-root file untouched and refuses the session with a message, so history never lives in both places. The in-root bytes are removed by unlink, not overwritten, with the same in-place-only limits as obliterate. Regression: a root with a legacy state file starts, `undo` works on the migrated history, and no `.vsh_state.json` remains in the root. Writes are atomic. On load, any existing state or journal file is set to 0600 (and its directory to 0700) before it is read. The file is opened with `O_NOFOLLOW`, checked with `fstat` to be a regular file owned by the invoking user, and tightened with `fchmod` on that descriptor, so a symlinked state file is refused rather than followed. A corrupt state is a hard error. `flock` makes a second vsh fail closed. The session root is canonicalised, symlinks and `..` included. Overlap is decided on filesystem identity, not on path strings. Each root is reduced to a key: its device plus its path relative to that filesystem's root, taken from `/proc/self/mountinfo` (the mount's root field joined with the path below the mount point). A bind mount of `/work/sub` at `/alias` therefore has the same key as `/work/sub`. Two roots conflict when they share a device and one key is a prefix of the other. Privileged regression: with `/work` active, a session rooted at a bind alias of `/work/sub` is refused. On macOS, which has no bind mounts, the key is the device plus the canonical path. A registry of active roots, kept at the fixed per-user registry path described below under its own lock, refuses a session whose root equals, contains or lies inside an active one. A registry entry is live only while its owner holds that root's `flock`. The lock, not the stored entry, is the source of truth. When acquiring, vsh tries each conflicting entry's lock: if the lock is free, the entry is stale (its process crashed) and is reaped. *Admission is atomic.* vsh takes the registry lock with `LOCK_EX \| LOCK_NB`, retrying for at most one second (B4). While it holds that lock it checks and reaps conflicting entries, takes its own root lock non-blocking, and only then publishes its entry; then it releases the registry lock. On exit the order is fixed: take the registry lock, remove the entry, release the root lock, and only then release the registry lock. No other session can be admitted while the exiting session still holds its root lock. Every entry is therefore published only by a process that already holds its root lock, and reaped only under the registry lock. A second session can never admit an overlapping root in the gap, and can never reap an entry whose owner is about to take its lock. Regression: two sessions started concurrently on `/work` and `/work/sub`, repeated 1000 times, never both admit. Each entry also records a non-reusable process identity (pid plus process start time) for diagnostics. A killed session therefore never blocks recovery, and the crash-injection runs exercise this path. The registry itself does not live under `XDG_STATE_HOME`. It sits at a fixed per-user path derived from the effective uid alone, never from an environment variable: `/run/user//vsh/` where that directory exists and is owned by the user, otherwise under the passwd home directory from `getpwuid`. Every vsh session of one user therefore shares it whatever its state namespace. A session whose canonical root contains the registry or its lock is refused, exactly like a root that contains the state dir, so no protected shell can unlink or replace the registry under another session. Regression: sessions with different `XDG_STATE_HOME` values on `/work` and `/work/sub` never both admit. The guarantee is scoped honestly: it coordinates the sessions of one user. Each session also takes an advisory `flock` on the *canonical root directory's own descriptor* (`open(root, O_DIRECTORY)` then `flock(LOCK_EX \| LOCK_NB)`; a conflict is refused immediately with a message naming the root, never waited on, which meets B4's one-second bound), not on a file inside the root. External commands launched from a session could unlink or replace a lock file, but cannot replace the root directory that the session holds open. Cooperating vsh processes with different state namespaces therefore still exclude each other on the same root. Processes that ignore advisory locks (including other users' non-vsh tools) are outside the claim, consistent with R18. + +State must also live outside every root it protects. vsh refuses to start when the canonical session root contains its state dir, audit log, key file or overlap registry (for example a root of `$HOME` with the default `XDG_STATE_HOME`), and names the conflicting path. The shell's own commands therefore cannot alter or obliterate their history. An intent/commit journal recovers on startup. Crash injection: 100 kills per PR and ≥1000 nightly. *`JournalModel.recover_sound`* is proved: recovery first compares the path's current fingerprint with the recorded pre- and post-state fingerprints. On a match, an RMR op recovers to \{pre, post}. On a mismatch, because something outside vsh changed the path after the crash, recovery leaves the filesystem untouched and reports `unresolved`. Rolling back could destroy the newer data, and rolling forward would not reach the recorded post-state. RMO ops are different, because an interrupted overwrite leaves a partially overwritten file that is neither. For them the model adds an `incomplete` state, and recovery rolls forward: the recorded intent is completed by finishing the overwrite and unlink. Before rolling forward, recovery opens the path with no-follow semantics and compares its device, inode and incarnation stamp with the identity stored in the intent. It also requires `st_nlink == 1` on the opened descriptor immediately before each recovery overwrite, for the target and for every regular-file descendant of a directory intent, because a hard link may have been created while vsh was down; a higher count ends in `unresolved` with nothing overwritten. Regression: crash after the intent and before the overwrite, add an outside hard link, restart; the linked file is byte-identical afterwards. If they differ, because the path was replaced while vsh was down, recovery does not touch it and reports an unresolved incomplete obliteration for the user to decide. When the identity check fails, recovery ends in a third terminal state, `unresolved`, with the path untouched and the intent kept. For a directory obliteration (`obliterate_dir` exists today) the intent also records a manifest of every descendant's identity and type. Recovery rolls forward only if every entry still present matches the manifest, with no added or replaced entry. An entry already gone counts as obliterated only if its own `overwrite-done` record is present, because the crash may have come partway through the walk; a missing entry without one ends in `unresolved`. Otherwise recovery ends in `unresolved`. *Crash after the overwrite:* absence of the name alone proves nothing, because another process may have renamed the intact file while vsh was down. The barrier is therefore a durable `overwrite-done` record, appended and fsynced after the overwrite passes and their fsync, and before the unlink. The intent also records the parent directory's identity and the entry name. If on restart the name is absent and `overwrite-done` is present, the original bytes were already destroyed, so any renamed copy holds only overwrite bytes: recovery touches nothing on disk, completes the history scrub, and appends an `obliterate-completed` entry marked `target-absent-after-overwrite`. If the name is absent and there is no `overwrite-done`, or the parent's identity no longer matches, recovery ends in `unresolved`. Crash-point regressions: kill after `overwrite-done` and before the completion entry (recovery writes the marked completion); and kill before the overwrite, then rename the target away externally (recovery ends in `unresolved`, and the renamed file is untouched). Regression: crash midway through obliterating a directory, add a file before restart, and recovery leaves the new file untouched. The crash harness's oracle is therefore \{pre, post, unresolved} for RMR and \{post, unresolved} for RMO, where `unresolved` is allowed only when the harness itself changed the path between crash and restart, and a harness case replaces the path between crash and restart to exercise `unresolved`. |Non-atomic, in cwd, corruption swallowed, no lock |1 does the quick part (0600, atomic write, fail-loud load); 2 does the rest +|*G3 Honest UI* |Printed proof status is derived only from `proofs/MANIFEST.toml`. A `proof_refs_resolve` test passes. No hard-coded system or theorem count remains. The gate is `! grep -rnE -e '[0-9]+ ([a-z]+ )?systems' -e 'theorem candidates' -e 'All filesystem operations are reversible' impl/rust-cli/src`, which uses separate `-e` patterns rather than alternation so the pattern contains no pipe characters. Run on the 2026-11-05 tree it matches all 7 current sites (so the gate fails today, as intended). Its success condition is *no output* (run as `! grep ...`, because grep exits 1 when nothing matches), which covers all six sites, including `Verification (6 systems):` and the `main.rs` banner. Beyond the grep, a test asserts that every printed status comes from the MANIFEST. ECHIDNA properties no longer `Pass` unconditionally, and because `echidna_integration` sits behind the non-default `echidna` feature, `cargo test --features echidna` asserts that every still-stubbed property returns `Skip`. |4 overclaim sites, and 1 cited theorem that exists nowhere |1 +|*G4 Spec* |`isEmptyDir` uses the child direction. `NonVacuity.lean` holds one witness per `*Precondition` (count-checked). *All 12 Lean libs* build as named CI targets, none quarantined; the 4 broken libs are repaired and the Coq RMO theorems are ported into Lean. Sorry and axiom counts are gated (`#print axioms` allow-list). A precondition-faithfulness table covers every prover: Idris2 gets NoDupKeys, and Z3 gets `is-empty-dir` defined. |Ancestor direction; 1 default target; 4 libs broken |1 +|*G5 Oracle + seam* a|`FinFS` refines the function model (`abs (finOp s) = op (abs s)`). The oracle runs over FinFS with undo, redo, txn and ERR verdicts, using every sequence of length ≤4 over 3 paths plus ≥1000 random ones, with 0 disagreements. *Keeping the required gate tractable.* The bounded-exhaustive part covers a *core alphabet*: mkdir, rmdir, touch and rm over 3 paths, `a`, `a/b` and `c`, so one pair is parent and child, plus UNDO, REDO, BEGIN, COMMIT and ROLLBACK. That is 17 symbols, so 88,740 sequences of length ≤4 before deduplication. Because the transaction controls are in the alphabet, every committed, rolled-back and invalid transaction trace of that length is enumerated (invalid means COMMIT or ROLLBACK with no open txn, or a nested BEGIN), and the gate asserts that each of the three classes was hit. It also asserts that `rmdir` of a non-empty directory (refused) and of an empty directory (succeeds) both occur. It is deduplicated by reachable state and runs in batch mode, with one oracle process consuming many sequences rather than one process per sequence. The full O alphabet below is covered by pairwise (all-pairs) generation, plus ≥1000 random sequences. That is the required gate. Nightly runs extend the exhaustive part to length 5. The exhaustive and pairwise parts stay finite because *every operand* has a fixed alphabet: + +* *Content* (write, append): the empty string, `a`, `b`, and one 4 KiB block. +* *Truncate sizes*: 0, 1 and 4096. +* *chmod modes*: 0600, 0644 and 0755. +* *chown*: the invoking uid:gid, plus one other uid:gid. A privileged CI lane (root in a container, with a fixture user) runs the chown cases so that a non-trivial ownership change and its undo are actually exercised. On the non-root lane, chown cases are reported as *skipped*, never counted as covered. +* *Symlink targets*: the 3 paths, plus one outside-root path that must be refused. +* *Paths*: the 3 paths. The random part draws content up to the OD-21 per-op cap. A negative control must fail. A golden corpus of ≥200 sequences, including precondition-violating ones, is checked by Rust, Lean `decide` and Agda `refl`, and CI fails if any of the three disagrees. The sequence ids in `tests/golden`, `GoldenTraces.lean` and `GoldenTraces.agda` must be equal as sets (a three-way check), or all three are regenerated in CI, which then fails on any diff. |4 of 17 op kinds, forward only; no corpus |1 (4 verbs), then 2 (all verbs) +|*G6 Witness coverage* (OD-22) |The MANIFEST shows *≥2 independent CI-gated provers plus the oracle* for every `OperationType` in scope. *Scope*: of the 17 `OperationType` variants, 14 are in scope (16 until E1e lands): the 12 filesystem verbs of O (mkdir, rmdir, touch/CreateFile, rm/DeleteFile, WriteFile, FileTruncated, FileAppended, CopyFile, Move, Symlink, Chmod, Chown). Unlink is counted with Symlink as its inverse. Obliterate is an RMO op. Its witnesses are the *irreversibility and residue* properties (`obliterate_not_injective`, overwrite coverage, intent residue written before mutation), not reversibility, and it needs ≥2 provers as well. Obliterate already has Coq, and gets Lean through P1b. Before P10 archives Coq, its replacement second witness is the Idris2 `ObliterationProof` in `Filesystem/RMO.idr`. That statement is mapped into the MANIFEST and gated by the Idris2 `--total` build, and it counts only if it is witness-eligible. *HardwareErase is out of G6 scope until it is wired* into the parser and executor (OD-22a): G6 counts only operations the shell actually runs, so no op carries an exempt oracle column. When it is wired it re-enters with the full gate, ≥2 provers plus the oracle. Its existing Idris2 theorem in `Filesystem/RMO.idr` stays as it is in the meantime. Obliterate *is* covered by the oracle (P4). Its finite semantics: the path is absent afterwards; a later UNDO of it is refused; any open transaction refuses it; and probes of earlier states of that file return no content. SetVariable and UnsetVariable are out of G6 scope *only once E1e lands*, which makes them session-scoped and not journalled per OD-27. That exemption is reviewable by the owner. Coq stays gated (`pipefail`, per-theorem assumption allow-lists) until its witnesses are replaced. Isabelle and Mizar are labelled _unchecked_ until archived. MANIFEST statuses use the #221 ledger vocabulary: `proven`, `proven-with-postulates`, `argued`, `tested-only`, `open`. *Only witness-eligible rows count*, and a row is eligible when two conditions hold. First, its status is `proven`, or it is `proven-with-postulates` and every postulate is on the registered allow-list (today that is only Agda `funext`, and only until P5 removes it). Second, its CI target ran green on the current head. `argued`, `tested-only` and `open` rows never count. `gen-proof-manifest` has a unit test asserting that disqualified rows contribute zero coverage. |No theorem has 6 witnesses; Coq is not gated |1 measures it; 2+ closes it +|*G7 RMO + audit* |Obliterate writes an intent residue first (write-ahead), and a failure to write it aborts before the overwrite. A completion residue is appended only after the unlink and directory sync succeed, so the audit never claims an obliteration that did not finish. It scrubs prior undo payloads of the target, identified by *resolved file identity*, not by path string, so content written through a symlink or another alias is caught. The identity is device plus inode plus an incarnation stamp: the `statx` birth time where available, otherwise the inode generation from `FS_IOC_GETVERSION`, otherwise a random id that vsh writes into a `user.vsh.id` extended attribute at first sight. The change time (`ctime`) is *never* used, because it is not unique. Legacy history entries written before E1d carry only a path. When obliterate runs, every legacy entry whose path resolves to the target, or whose path cannot be resolved, is scrubbed conservatively, and the scrub is reported. Legacy bytes are never left behind for lack of an identity. Records with an identity are matched on the *full* triple (device, inode and incarnation stamp), never on device and inode alone. Each incarnation also carries a *lineage id*. When undo or redo recreates a file on a new inode, the recreated incarnation inherits the lineage of the one it restores, and obliterate scrubs every record of the whole lineage. Regression: `echo secret > f; rm f; undo; obliterate f` leaves no `secret` bytes in history, redo or blobs. If none of the three stamp sources is available, identity is ambiguous and vsh fails closed toward privacy: for that target only, obliterate scrubs every history entry that matches device and inode, and reports any unrelated undo entries it consumed, rather than risk leaving obliterated bytes behind. Each record also stores which source supplied its stamp. If that source was the `user.vsh.id` xattr and the xattr on the same device and inode is now missing or different, vsh does not mint a fresh stamp: it treats the identity as ambiguous, applies the device-and-inode scrub above, and reports the change. Regression: record a payload, remove the xattr externally, then obliterate; no prior bytes remain in history. Recovery refuses to roll forward on an ambiguous identity. An incarnation is retired, and its history entries stop matching, only when vsh observes the *last* link go: `fstat` before the unlink shows `st_nlink == 1`. If other links remain (for example one an external command created), the incarnation stays live. Because G1 refuses obliterate while `st_nlink > 1`, a surviving alias can be obliterated only once it is the last remaining link (after `rm` of the other names), and that obliterate still scrubs the whole incarnation's history. If an external process removes the last link, vsh never sees it, and the incarnation stays live. That is harmless: a file that later reuses the inode gets a new stamp (a new birth time, a new inode generation, or no `user.vsh.id` until vsh writes a fresh one), so the full-triple match never pulls in the old file's history. Regression: create, record, delete externally, recreate until the inode is reused, then obliterate the new file; the old file's entries are untouched. Because `obliterate_dir` exists today, a directory obliterate scrubs history and removes content-store references for every descendant in its manifest, by the same identity rules. The alias regressions are repeated for a file inside an obliterated directory. Regressions: write through an alias then obliterate the canonical path, and the reverse; no prior bytes remain in history, redo or blobs. Once a content store exists (E4), obliterate also removes the target's references to its pre- and post-content blobs. A blob left with no reference is deleted (overwrite, then unlink) only after the residue is durable. A blob still referenced by another history is kept, and the residue records that it was retained. For such blobs the gate claims removal of the target's references only, not erasure of the bytes. Purging a still-referenced blob needs a separate owner decision that names the affected histories. Physical erasure on CoW or SSD remains a non-goal. The non-identification claim is stated over the joint observer. The residue stores a path commitment. The log lives outside the root and is keyed (OD-24). `vsh audit verify` detects 6 tamper classes. `secure_erase_file` is private and returns `Err` on HDD. |Unsigned, in the root, written after the unlink |1 does ordering, scrub and `secure_erase`; 2 does keying, verify and content-store cleanup +|*G8 Docs + hygiene* |`regen-status.sh` is idempotent. `just test && just quality` pass. A non-root job runs a security test that asserts something. The ROADMAP_TO_V1 v1 gate is amended per OD-22. |Counts drift; the security test asserts nothing |1 +|*G9 Refinement* |*Aeneas:* `VshRefine` proves `core_refines_spec` and `core_undo_refines` for the declared op set. The trusted base is listed (Charon/Aeneas, `PosixAx`). |Not started |1 does the spike (GO/NO-GO); later sessions prove it +|*G10 Estate theory* (after G1–G5) |The Agda mirror instantiates absolute-zero `CNOInterface` (T7). It imports the OD-23 edge, with every library pinned to a SHA in its own CI lane. |No mechanised feeder import exists |3+ +|_G11 (later)_ |ShellEvent v0 JSONL is a projection of the journal. |No emitter |later +|=== + +*Non-goals (never claimed):* + +* full POSIX; +* crash consistency beyond the journal model and the OS-assumption ledger; +* CoW/SSD erasure; +* linearizability (#90); +* multi-process serializability beyond the leaf-disjoint diamond; +* MCP and Ochrance receipts in this programme window. + +''''' + +== 2. Architecture + +.... + PRINTED CLAIMS (derived from proofs/MANIFEST.toml, never hard-coded) + | + +-----------------------------------v------------------------------------------+ + | L1 vsh shell: parser / REPL / -c / externals [effects only] | + | session_root fixed at start != cwd | + | | Op | + | v | + | L1a vsh-core crate (pure, no std::fs/anyhow/PathBuf) == Aeneas input | + | Pre / step / inverse / undo / redo / txn over a Vec-backed FinFS mirror | + | ONE inverse table | fingerprint | loss-grade table (lossless/lossy/obl.) | + | | | + | | drift guard = runtime discharge of the refinement hypothesis | + | | abs(real OS state) == recorded post-state | + | v | + | L2 Journal = WAL = undo history = audit chain = receipts [session 2] | + | XDG// 0700; intent->mutate->commit; recover; flock | + | L2a CAS blobs (pre AND post content) L3 keyed audit + verify + anchors | + +-------|------------------------------|---------------------------------------+ + | Charon/Aeneas | golden corpus (>=200 seqs) crash injection + v v + +------------------------------------------------------------------------------+ + | P1 Lean v4.34.1 VshSpec (Mathlib-free, canonical) | + | FilesystemModel (isEmptyDir FIXED) + NonVacuity + all 12 libs built | + | FinModel ==refines==> function model | + | ModelOracle (undo/redo/txn/ERR) GoldenTraces (decide) | + | JournalModel.recover_sound [session 2] | + | ^ require | + | P1r VshRefine (separate package; Mathlib allowed only here) | + | core_refines_spec, core_undo_refines [spike in session 1; KILL @ 2] | + +------------------------------------------------------------------------------+ + | P2 Agda --safe --without-K finite-map MIRROR of VshSpec (in-repo witness) | + | FinModel.agda + GoldenTraces.agda (refl) [session 1] | + | VshCNO (absolute-zero CNOInterface, T7) + OD-23 edge [after G1-G5] | + +------------------------------------------------------------------------------+ + | P3 Z3: SAT non-vacuity + bounded crash relation (solver rung) | + | P4 Coq: gated witness until its content is ported and the witness | + | threshold holds without it; then archive/ (never deleted) | + | P5 Isabelle, Mizar: labelled "unchecked" -> archive/ | + | P6 Idris2: NoDupKeys fix; ABI seam kept (src/abi -> januskey/ochrance Ph.3) | + +------------------------------------------------------------------------------+ + Seams that are explicit and machine-checked: (1) Aeneas extraction, + (2) golden corpus Rust / Lean / Agda, (3) differential oracle, + (4) MANIFEST witness count. + Feeders (L5) parked until G1-G5: absolute-zero, echo-types, residual-evidence, + epistemic, januskey CAS, typell, others citation-level. +.... + +=== Layer table + +[cols=",,,",options="header",] +|=== +|Layer |Where |Responsibility |Interface +|L0 host OS |`docs/OS-ASSUMPTIONS.adoc` (new) |The trusted base. Each entry later becomes one `PosixAx` Lean axiom. |syscalls +|L1 shell |`impl/rust-cli` |Parser, REPL, externals, effects. A fixed `session_root`. |`vsh` binary +|L1a vsh-core |`impl/vsh-core` (new workspace crate) |The pure decision core and the Aeneas input. One inverse table, fingerprints, loss grades. |`plan`, `step`, `inverse`, `fingerprint` +|L2/L2a/L3 |`src/{journal,blobs,commitment,anchor}.rs` |WAL = history = audit = receipts; CAS; keyed audit (session 2) |`append_intent/commit/recover`, `vsh audit verify` +|P1 VshSpec |`proofs/lean4` |The canonical spec, non-vacuity, FinFS, oracle, golden traces, journal model |named lake targets +|P1r VshRefine |`proofs/lean4-refine` (new package) |Aeneas output plus the refinement proof |`core_refines_spec` +|P2 Agda mirror |`proofs/agda` (the #221-repaired tree, taken to `--safe --without-K`) |The second independent witness, golden `refl`, and later the estate CNO and feeder instances |`agda --safe --without-K All.agda` in its own CI lane +|P3 Z3 |`proofs/z3` |SAT non-vacuity, bounded crash relation |`verify-z3.sh` +|P4–P6 |`proofs/{coq,isabelle,mizar,idris2}` |Coq is a gated witness until replaced. Isabelle and Mizar are unchecked. Idris2 gets NoDupKeys. |existing workflows +|Seams |`scripts/gen-golden`, `scripts/gen-proof-manifest` |The golden corpus and the witness count |`tests/golden/`, `proofs/MANIFEST.toml` +|=== + +=== Mechanised edges + +[cols=",",options="header",] +|=== +|Edge |State +|Rust ↔ Lean `model_oracle` (differential) |*Exists*, green, 4 of 17 op kinds, forward only. Extended in G5. +|`FinModel.lean` ⇒ `FilesystemModel.lean` (refinement) |New, session 1 +|`GoldenTraces.{lean,agda}` ↔ `tests/golden` (same sequence ids, scripted set equality) |New, session 1 +|`proofs/agda/FinModel.agda` ≅ `FinModel.lean` (transcription, checked through the golden corpus) |New, session 1. Graded "checked", never "mechanised". +|`vsh-core` → Charon/Aeneas → `VshRefine` → `VshSpec` |Spike in session 1 +|`JournalModel.lean` ↔ `journal.rs` (barrier table + crash injection) |Session 2 +|Agda mirror → absolute-zero `CNOInterface.agda` (T7) |After G1–G5 +|Agda mirror → echo-types `EchoResidueCell`/`EchoDeniability`, or residual + epistemic |After G1–G5 (OD-23) +|=== + +''''' + +== 3. Measured current state + +=== 3.1 What is green + +* `cargo test` in `impl/rust-cli` passes *827, fails 0, ignores 15* across 23 result lines. +* `cargo fmt --check` and `clippy -D warnings` are clean. +* `ffi/rust` passes 24 tests. +* januskey `reversible-core` passes 43 tests. +* CI on `295c3ca`: Rust CLI, Lean Verification (including the oracle differential), Idris2, Correspondence, CodeQL, Dogfood, Secret Scanner and Bridge Forbidden Phrases are all green. +* CI red: Governance (`actions.lock` verify), Mirror, weekly ECHIDNA (NW-2/#162), scorecard, and one Hypatia run. Compilation Tests had its macOS beta/nightly jobs cancelled. + +=== 3.2 Runtime holes + +Each was reproduced through the parsed `vsh -c` path. Five were confirmed by the skeptics, and I re-ran the rest in this session. + +[cols=",,,",options="header",] +|=== +|# |Repro (`vsh -r $ROOT -c …`) |Observed |Root cause +|a |`touch g; echo hi > g; undo` |"Undo write failed: No such file or directory" |`redirection.rs:415/428` records an absolute path, and undo re-resolves it under the root +|b |`touch f; sh -c 'echo precious > f'; undo` |Deletes the externally written data |No drift guard +|c |`begin; touch a; obliterate a --force; rollback` |Reports "rolled back" |`commands.rs:1397` `if let Some(inverse)` has no `else` +|d |`echo a>f; echo b>f; obliterate f --force` |Prior content of `f` survives in `.vsh_state.json` |No scrub of undo payloads +|e |`x=$(( (-9223372036854775807-1) / -1 ))`, the same with `%`, and `x=$(( -(-9223372036854775807-1) ))` |*Panic* (rc 101) |Unchecked i64 `/`, `%` and unary minus (`arith.rs:607,646,653`) +|f |Pre-existing `sub/f` containing KEEP; `touch f; cd sub; undo` |Prints "undo rm f", rc 0. *Deletes the user's `sub/f`* and leaves the created `f`. |`executable.rs:404-411` reassigns `state.root` on every `cd`; history paths are relative +|g |`vsh -r $S/box -c 'cd ..; touch escaped'` |Creates `$S/escaped`, rc 0. *Sandbox escape.* |Same as (f) +|h |`chmod 600 s; rm s; undo` |Content comes back, but *mode 0600 becomes 0644*. The state file is *0644 and holds the secret bytes* (`undo_data:[84,79,80,…]` = "TOP…"). |The payload stores content only; no `set_permissions` anywhere +|i |obliterate |It overwrites and unlinks *before* recording the op and writing the residue. A residue failure is only an `eprintln!` warning. |`secure_deletion.rs:325-339`, `:67-79` +|j |In-root `link -> /outside/victim`; `echo PWNED > link` |rc 0. *The file outside the root is overwritten* (re-run 2026-11-05 on code identical to `ce16ce3`). `rm link` correctly removes only the link. |Containment is lexical only: the target is never resolved beneath the root. Found in review on #222. +|k |`lp -> /outside` (in-root symlink to a directory); `touch lp/new; mkdir lp/newdir` |rc 0. *A file and a directory are created outside the root* (re-run 2026-11-05). |Creation follows a symlinked parent component. Found in the Codex review of #222. +|l |Same `lp`; `touch f; mv f lp/f` |rc 0. *The file is moved outside the root.* |`commands::mv` passes the destination straight to `fs::rename`. Found in the Codex review. +|m |In-root `vl -> /outside/victim` (content `PRECIOUS`); `obliterate vl --force` |rc 0, prints "securely obliterated". *The outside file's contents are overwritten with `0xFF` bytes; only the link is unlinked.* Irreversible destruction outside the sandbox. |`secure_deletion::obliterate` follows the symlink for metadata and overwrite. Found in the Codex review; the most severe failure in this table. +|n |In-root hard link `hl` to outside `victim`; `obliterate hl --force`, and `echo X > h2` on another outside hard link |rc 0 for both. *The outside file is overwritten with `0xFF`, and the other outside file's content becomes `X`* (re-run 2026-11-05). |Hard links share the inode, and symlink-safe resolution (`RESOLVE_BENEATH`, `O_NOFOLLOW`) cannot see them. Found in the Codex review. +|— |`echo $((1+2))` (builtin echo) |Prints `$((1+2))` literally. Assignment and `/bin/echo` expand it. |A-7: arithmetic expansion is missing on the builtin path. This is a POSIX bug, not a safety bug, but it means any arith test must use assignment form or it passes vacuously. +|=== + +Other measured defects: + +*Code defects* + +* `secure_erase_file` is public and unused. It would erase a whole device with no confirmation, and returns `Ok` as a no-op on HDD. +* The audit is unsigned: the only production caller passes `None` for the key. The audit log lives inside the root, follows `cd`, and logs the plaintext path, `$USER` and pid. +* Variables are journalled in history but not persisted, so undoing them in a later session is incoherent. +* Checkpoint indices are not adjusted when history is trimmed. + +*Test and documentation defects* + +* `security_no_privilege_escalation` *has no assertion in any branch*, so it passes as root and as non-root. Adding a non-root CI job would therefore add zero signal until the test is given a real check. +* CLAUDE.md lists 15 security tests; 17 exist. + +=== 3.3 Proof-side state + +These were read from source. *No prover ran here.* + +*Lean* + +* `isEmptyDir` quantifies over ancestors (`FilesystemModel.lean:69-71`). Coq (`filesystem_model.v:107-111`) and Isabelle (`FilesystemModel.thy:70-72`) state the correct child direction. +* Only `FilesystemModel` is `@[default_target]`. `lean-verification.yml` builds `Extraction` plus `model_oracle`. Of the 12 `lean_lib`s, the rest are not CI-built except transitively. +* 4 libs are self-declared broken: CopyMove, FileContent, RMO and Permission. + +*The same vacuity class in other provers* + +* Idris2: `rmdirMkdirReversible` and `rmTouchReversible` take a `canonical` hypothesis that is the conclusion (`Operations.idr:173-180, 216-223`). +* Agda (after #221): 9/9 modules type-check under Agda 2.6.4.3 + stdlib 2.1.1 and 2.7.0.1 + stdlib 2.2, with one postulate (`funext`). `--safe`, `--without-K` and `--cubical-compatible` each reject it (`proofs/agda/VERIFICATION.adoc`). `IsEmptyDir` still has no emptiness field (`FilesystemModel.agda:91-94`). No CI job type-checks the Agda tree. +* Z3 (per #221): `symlink_operations.smt2` contains one bare `sat` and never negates a goal, so it proves nothing and contributes no witness. +* Z3: `is-empty-dir` is uninterpreted, so a satisfiability check cannot detect a wrong direction. + +*Coq* + +* The whole `_CoqProject` builds in CI. +* `Print Assumptions` goes through `tee` with no `pipefail`, so it gates nothing. +* The proposed allow-list `{functional_extensionality_dep, classic}` is wrong in both directions. +** `is_empty_dir_dec` is a theorem resting on `excluded_middle_informative`, which also pulls in `constructive_indefinite_description`. +** The owner's D-1 text allows only FunctionalExtensionality. + +*Op coverage and doc drift* + +* `OperationType` has *17* variants. In my earlier message I said 19; that was wrong. The Lean oracle covers 4 of them, and januskey covers 7 of 17. +* `proof_refs.rs` hard-codes names and line numbers. `variable_assignment_reversible` exists in no proof file, yet the UI says "all proven in 6 systems". + +*Feeder and cross-repo facts* + +* Agda pins disagree across at least 2 Agda versions and at least 4 stdlib sources: +** `2.6.4.3-1+b2` with Debian stdlib `2.1-4` (epistemic, choreographic); +** `2.6.4.3` with a git-commit stdlib (residual-evidence); +** unpinned apt with stdlib `v2.3` (echo-types); +** `2.6.3` with stdlib `1.7.3` (absolute-zero); +** `2.6.3-1build1` (one januskey workflow). +* absolute-zero's T7 Agda CNO interface (ruled D204) *does not exist yet*. Governance conflicts on whether it is Agda (T7) or Coq (ULTRAPLAN Q10). +* januskey: `ReversibleExecutor` has 0 implementors. The "merkle root" is a linear chain, and its root does not commit the full op record, so a measured collision exists. `MetadataStore::save` is non-atomic. It emits A2ML, which is retired estate-wide. +* januskey already has `--safe --without-K` Agda prior art the synthesis missed: `TransactionAtomicity.agda` (`rollback-restores`, `at-most-one-active`) and `Reversibility.agda` (`obliterate-absorbs`, graded by a Loss resource algebra). + +''''' + +== 4. Engineering route + +The engineering route serves the spine. Each step either closes a measured hole or builds what the proof needs from the code: a pure core to extract, and runtime discharge of the refinement hypothesis. + +[cols=",,,",options="header",] +|=== +|Step |What |Size |Session +|*E0* |`tests/regressions_parsed_path.rs` holds *14 fail-first safety tests* (§3.2 a–n). They must fail on `295c3ca` for the documented reason. Also rewrite `security_no_privilege_escalation` with real assertions (no euid elevation, no setuid files, created-file uid equals the invoker), and keep it runnable: it carries `#[ignore = "needs non-root"]`, and the non-root CI job runs `cargo test --test security_tests -- --include-ignored`. That job asserts that it is not running as root, so the test can never pass vacuously. |hours |1 +|*E1* |Local fixes: redirection records a root-relative path (a); checked `/`, `%` and unary minus, with an explicit pow policy and a never-panics proptest under debug and release (e); `secure_erase_file` private, with confirmation, `Err` on HDD; builtin `echo` arithmetic expansion (A-7); the `>` vs `>>` property (A-10). |1 day |1 +|*E1b* a|*Session root ≠ cwd and resolved containment* (f, g, j). Fix the root at start, confine `cd` to it (OD-26), and store paths relative to the session root. Apply G1's per-operation follow policy: + +* *Content operations* (redirection, write, append, truncate, chmod, chown, the cp destination, obliterate) resolve fully beneath the root (`openat2` with `RESOLVE_BENEATH`, falling back to an `O_NOFOLLOW` walk with a per-component mount-id check) and refuse an escaping or mount-crossing target. Obliterate refuses a symlink target outright, before any overwrite. Content operations `fstat` the opened descriptor and refuse `st_nlink > 1` unconditionally. There is no override. +* *Entry operations* (rm, rmdir, mkdir, touch/create, ln, both mv endpoints) resolve the parent beneath the root and use `mkdirat`, `openat(O_CREAT\|O_EXCL\|O_NOFOLLOW)`, `unlinkat` or `renameat` on the entry, never following a final symlink. + +Regressions (parsed path): + +* `echo X > link`, `touch lp/new`, `mkdir lp/newdir` and `mv f lp/f` are refused, and nothing appears outside the root. +* `obliterate vl --force` (symlink) and `obliterate hl --force` (hard link) are refused, and the outside files stay byte-identical. `echo X > h2` through a hard link is refused. +* `rm link` removes only the link, and `rm link; undo` restores a symlink with the same target, not a regular file. The same holds for a dangling link. |1–2 days |1 +|*E1c* |RMO ordering (i): an `obliterate-intent` residue entry is written and fsynced before the overwrite, and a failure to write it aborts. An `overwrite-done` entry is appended and fsynced after the overwrite passes and before the unlink. A separate `obliterate-completed` entry is appended only after the unlink and the directory sync succeed. A failed or crashed obliterate therefore leaves an intent with no completion, which recovery and `audit verify` report as incomplete, never as obliterated. Scrub prior payloads of the target (d), matched by recorded device, inode and incarnation stamp rather than path string, so aliases are covered and reused inodes are not. Refuse obliterate inside a txn (c). Inverse-less ops become a hard rollback failure. Rollback is resumable (OD-11). |1 day |1 +|*E1d* |Quick durability (h): the state file is written 0600 with an atomic temp-fsync-rename. On load, an existing state file, including one created earlier at 0644, is set to 0600 before it is read, so a session that never saves still closes the leak. The file is opened with `O_NOFOLLOW`, checked with `fstat` (regular file, owned by the invoker), and tightened with `fchmod` on that descriptor. Regressions: a 0644 state file holding undo bytes reads 0600 after a no-mutation session; a `.vsh_state.json` symlink to another file is refused, and the target's mode is unchanged. In addition, a corrupt load fails loudly, and the undo payload carries the entry kind, mode, uid, gid and mtime. For a symlink it also carries the `readlink` target, and undo recreates the link with `symlinkat`; a symlink has no content to save, and its referent is never read. *Restorability preflight:* a non-root session cannot `chown` a file to another user, and can only `chown` it to a group it belongs to. Any removal or move of an entry is therefore refused when its uid differs from the invoker's, or when its gid is neither the invoker's effective gid nor one of its supplementary groups. That covers `rm`, `mv`, `rmdir`, and every entry inside a recursive deletion, which is pre-checked as a whole before anything is removed. An explicit `--accept-ownership-loss` records the op with a *lossy* grade (OD-25). Its undo restores content and mode under the invoker's ownership and reports the loss. Regressions: removing another user's file, and `rmdir` of another user's empty directory, in a directory the invoker owns, are both refused, and with the flag both are recorded as lossy. So is removing a file the invoker owns whose group is one the invoker no longer belongs to. *Content capture:* `rm` and every content-replacing op must read the full pre-content before the unlink or write. A read failure (for example on a mode-000 file) refuses the op unless `--accept-content-loss` is given, which records a lossy grade; the `unwrap_or_default()` at `commands.rs:287`, which turns an unreadable file into an empty undo payload, is removed. *Hard links:* `rm` of a regular file with `st_nlink > 1` is refused unless `--accept-link-split` is given, which records a lossy grade, because undo recreates a new inode and cannot restore the alias. Regressions: `rm` of a mode-000 file is refused and the file is untouched; `ln f g; rm f` is refused, and with the flag `undo` reports the split. The new fields are additive and optional on load (serde defaults), so no backup-then-migrate is needed. An older record without them loads with metadata marked `unknown`. Undo of such a record restores content only and prints that the mode, owner and mtime were not recorded. Regression: a state file written before E1d loads, and undo restores its content and reports the missing metadata. |hours |1 +|*E1e* |OD-27: variable ops stay session-scoped. `set_variable_tracked` and `unset_variable_tracked` keep their undo entries in memory only, and they are filtered out of durable history. Regression: `x=1; exit`, restart, `undo` must not touch variables, and persisted history contains no SetVariable or UnsetVariable entry. State files written before E1e may already hold such records. On load they are dropped, together with every transaction reference to them, and the drop is reported once. Checkpoints store a history index, so each is rebased to the number of retained entries before it. Variable ops have no filesystem effect, so a rebased checkpoint restores the same filesystem state. Nothing else in the file changes. E3's checkpoint-by-ID representation uses the same rule: a checkpoint that named a dropped entry moves to the nearest preceding retained one. Regression: a mixed history with checkpoints before and after a dropped variable entry restores the same filesystem state after migration as before. Regression: a pre-E1e fixture holding `SetVariable` entries loads, `undo` does not touch variables, and the next save contains none. |hours |1 +|*E2* |*Extract `vsh-core`*: a pure workspace crate with `Pre`, `step`, `inverse`, undo, redo and txn over plain data, one inverse table, fingerprints and loss grades. *Drift guard* (b): each op records pre- and post-state fingerprints. Undo checks the post-state before acting, and redo checks the pre-state; a mismatch refuses, or proceeds only with an explicit recorded `--force`. Regression: `touch f; undo; redo` succeeds, and redo after an external change to the undone state is refused. This is the Aeneas input and the runtime discharge of `abs(OS) = recorded`. |days |1 +|*E5* |Honest UI plus witness counting: a `gen-proof-manifest` script produces `MANIFEST.toml` (theorem id, prover, file, CI target, status, op kind); `proof_refs` reads it; a `proof_refs_resolve` test; replace the `repl.rs:295` banner "All filesystem operations are reversible with 'undo'" (false for obliterate and hardware-erase) with a statement derived from the inverse and loss-grade table; delete every hard-coded system and theorem count (`commands.rs:2131,2313,2328,2404`, `parser.rs:458`, the `main.rs:328` banner); ECHIDNA returns Skip, not Pass, checked under `cargo test --features echidna`; `docs/PROOF-SYSTEM-STATUS.adoc` with a *per-op witness table* (OD-22). |1 day |1 +|*E-golden* |`scripts/gen-golden` writes one corpus (≥200 sequences, including precondition-violating ones with expected `Err`), emitted as a Rust test, Lean `decide` checks and Agda `refl` checks. |1 day |1 +|*E8* |Docs: `regen-status.sh`; THEORY-FEED corrections (NW-1 → T7 Agda; NW-3 mappings; bridge `.md` → `.adoc`); the ROADMAP_TO_V1 gate amendment (OD-22); a PROOF_HOLES_AUDIT entry for the vacuity; remove `impl/mcp/deno.lock` and the dead recipes. Licence text is not touched. |1 day |1 +|*E9* |CI to green: Governance `actions.lock`, Mirror, ECHIDNA `--library` roots (advisory until a tri-state verdict exists), fuzz runs all targets. *Proposed* required checks are applied by the owner. |1 day |1 +|E3 |Full durable store: XDG dir 0700, `flock`, redo and checkpoints persisted by id, backup-then-migrate. |days |2 +|E4 |Journal = WAL; CAS blobs (pre and post content; unblocks redo of writes, C-1); `recover()`; segment rotation; crash points including between unlink and record. Designed together with `JournalModel`. |~1 week |2 +|E6/E7 |Path commitments; obliterate removes content-store references, with the shared-blob rule from G7; log outside the root; `KeySource`; keyed chain (OD-24); `vsh audit verify` with 6 tamper classes; anchors. |~1–2 weeks |2 +|E10–E14 |ShellEvent v0; resource bounds (#190/#191); januskey CAS swap (after JK-1..4); typell txn monitor; MCP (OD-17). |— |later +|=== + +''''' + +== 5. Proof route (the spine) + +[cols=",,,",options="header",] +|=== +|Step |What |Size |Session +|*P0* |*EXP-1:* prove the current `RmdirPrecondition` uninhabited, so the defect is recorded as a theorem. Then fix `isEmptyDir` to the child direction. Add `NonVacuity.lean` with one `example` per precondition, count-checked by a script. Re-check the dependents (`rmdir_mkdir_reversible`, `rmdirPreservesEquiv`, the Composition `.rmdirOp` branches). EXP-2 measures the blast radius. |hours to 1 day |1 +|*P0b* |*Faithfulness table across provers.* Idris2's restore theorems drop the circular `canonical` hypothesis. NoDupKeys alone cannot do this, because the model is an ordered list: removing then re-inserting `p` in `[q, p]` yields `[p, q]`. The theorems are restated up to the existing observational `Equiv` (`Model.idr:396`). The alternative, if exact equality is wanted, is a sorted canonical representation with NoDupKeys as its invariant. Z3 defines `is-empty-dir` instead of leaving it uninterpreted, and adds SAT checks. The legacy Agda gap (no emptiness field) is noted, and that tree is archived when P5 lands. |1 day |1 +|*P1* |*All 12 Lean libs as named CI targets* plus `model_oracle`. Gate on sorry/axiom counts via `#print axioms`. |hours |1 +|*P1b* |*Repair the 4 broken libs* (CopyMove, FileContent, RMO, Permission), starting from the nonexistent namespace opens (`CopyMoveOperations.lean:19-20`). *Port the Coq `obliterate_overwrites_all_blocks` and `obliterate_not_injective` into Lean*, so Lean carries the RMO chain. The gate is a named lake target for both and a MANIFEST entry each. Time-box: if a lib needs more than a day, quarantine it visibly and report. |1–3 days |1 +|*P2* |*Coq stays an honest witness until replaced:* `set -o pipefail` and per-theorem allow-lists. `{functional_extensionality_dep}` covers the reversibility theorems. A scoped `{classic, constructive_indefinite_description}` exception covers `is_empty_dir_dec` and its dependents; this is labelled a D-1 departure for the owner. |hours |1 +|*P3* |*FinFS canonical model:* a Mathlib-free sorted association list, decidable `isEmptyDir`, `abs`, and the refinement `abs (finOp s) = op (abs s)`. Do mkdir, rmdir, touch and rm first, then the rest of the op set O (write, truncate, append, cp, mv, symlink, chmod, chown). Transport lemmas so the existing theorems hold for FinFS. Use the Idris2 `Filesystem/Model.idr` theorem shapes (`undoRedoIdentity`, `TraceReversible`) as the checklist. C-5 (`well_formed` preserved) is the FinFS invariant. Kill rule: if 4 verbs need more than ~600 LoC, fall back to `decide` checks and re-plan. |days |1 (4 verbs), 2 (O) +|*P4* |*Oracle v2* over FinFS: UNDO and REDO via `reverseOp`, BEGIN/COMMIT/ROLLBACK, *OBLITERATE*, precondition verdicts, content and permission probes. Bounded-exhaustive plus random generation. Negative control EXP-6. *GoldenTraces.lean* (`decide`) over the E-golden corpus. |days |1 +|*P5* a|*Agda second witness, built on the #221-repaired tree.* Take `proofs/agda` to `--safe --without-K`: + +* Drop the `funext` postulate by stating equivalence pointwise (`FsEquiv`, already in the tree) instead of `≡` on functions. +* Remove the K-dependence: stop case-splitting `Dec (p ≡ p)` against `refl`, and use a decidable path equality whose proofs are compared propositionally. +* Add the missing emptiness field to `IsEmptyDir`, matching the corrected Lean precondition. +* Add `GoldenTraces.agda`: the same sequence ids, checked by `refl` on probe results. + +The pin comes from EXP-agda. #221 showed both 2.6.4.3 + stdlib 2.1.1 and 2.7.0.1 + stdlib 2.2 work for the non-safe tree. Mirror the Lean preconditions, inverses and reversibility theorems for the 4 core verbs first. Fallback, if the K-free refactor stalls past the kill rule: a fresh builtins-only mirror (`--no-libraries`). |days |1 (4 verbs), 2 (O) +|*P6* |*Aeneas spike:* a 50–150 line slice of `vsh-core` (mkdir, rmdir, touch, rm, undo stack over a Vec FinFS, paths as `Vec` ids) → Charon → Aeneas → Lean, in the separate `lean4-refine` package. Prove `core_mkdir_refines`. *GO* = the build passes on a toolchain reconcilable with v4.34.1, with no Mathlib in VshSpec. *NO-GO* = a written record of the blocking pins. *Kill after 2 sessions in total.* |≤2 sessions |1 (first attempt) +|P7 |Tier-C items: C-1, C-3, C-4, C-8, C-10, and C-9 over path independence. |≤1 day |1–2 +|P8 |*JournalModel:* state is FS × IntentLog. `recover_sound` says an in-flight RMR op ends in \{pre, post} when the observed fingerprint matches a recorded endpoint, and otherwise in `unresolved` with the filesystem untouched; an in-flight RMO op ends either in \{post} after roll-forward (passing through a modelled `incomplete` state), or in `unresolved` when the recorded identity no longer matches the path. In the `unresolved` case the replacement path is untouched and the intent is kept for the user. Committed ops survive. Do mkdir first, then generalise over the inverse table. P8 also models the crash after the overwrite: an absent target with a durable `overwrite-done` record under a parent whose identity matches ends in `post`, with the completion marked `target-absent-after-overwrite`; an absent target without that record, or a changed parent, ends in `unresolved`. Its per-class outcome sets are the crash harness's oracle, exactly as in G2: \{pre, post, unresolved} for RMR and \{post, unresolved} for RMO, with `unresolved` allowed only when the harness itself changed the path between crash and restart. A bounded SMT encoding (k ≤ 4) cross-checks it. |~1 week |2 +|P9 |*Full refinement* (if P6 is GO): `core_refines_spec` and `core_undo_refines` for O, RMR-only rollback, redo. The `#print axioms` allow-list is \{propext, Quot.sound, Classical.choice?, Aeneas library axioms, PosixAx}. *If NO-GO:* an owner decision between the proof-first architect's fallback (Lean `@[export]` FinFS ops linked into Rust as the decision core; the judges scored it E 5 / D 5 for its unsafe FFI seam and the Lean runtime in every build) and a declared terminal state of "differential vs proven-refining FinFS" (E 6 / D 7). |weeks |2+ +|P10 |*Archival* (when G6 holds without them): move Coq, Isabelle and Mizar to `archive/proofs/`, with a README mapping every theorem to its Lean or Agda successor. In the same change, update or deliberately retire every consumer of those paths: `validation.yml` (whose working directory is `proofs/coq`), `echidna-validation.yml`, the Justfile, `scripts/verify-proofs.sh`, `scripts/validate-with-echidna.sh` and the `ffi/rust` proof references. Then run CI cold after the move. Never delete. |1–2 days |2+ +|P11 |*Estate theory* (after G1–G5): absolute-zero `CNOInterface.agda` (T7, setoid-parametric, so no funext) plus a `VshCNO` instance over the mirror. The OD-23 edge comes next. Then epistemic `AuditLog`/`AuditReceipt` for the keyed audit. Never use the vacuous `copyFile → A↔ΣEcho` pairing or the nonexistent `const-fibre-↔-domain`. |~1–2 weeks |3+ +|=== + +''''' + +== 6. The ladders + +*Theory* + +* T0: RMR/RMO boundary as a rule. +* T1: OS-assumption ledger. +* T2: refinement relation written in prose before any proof. +* T3: event-log semantics (state is a fold; checkpoints are event ids). +* T4: crash relation. +* T5: commitment semantics (touched subtree, not a global hash). +* T6: audit trust model (Opaque / Designated / Public). +* T7: C-9 over path independence, with occupancy high-water-mark grades excluded from serializability. +* T8 _(later)_: residue vocabulary after echo-types ET-RESCLASS-1. +* T9 _(optional)_: verified script subset. +* T10 _(not this window)_: tropical, occupancy, anytype, choreographic, secret-types. + +*Proving* + +* R0: EXP-1 then the fix. +* R1: named CI targets and the Coq gate. +* R2: broken libs. +* R3: Tier-C. +* R4: FinFS refinement. +* R5: undo laws on FinFS. +* R6: `recover_sound`. +* R7: Aeneas spike. +* R8: one feeder edge. +* R9: audit receipts. +* R10: CNO and echo edges. +* R11: script-subset theorems. + +*Solving* + +* S0: Z3 satisfiability non-vacuity. +* S1: Lean `decide` over FinFS with ≤4 paths, as a cheap model checker compared against `verification.rs`. +* S2: bounded-exhaustive differential. +* S3: bounded SMT encoding of the crash relation (k ≤ 4). +* S4: Kani on L1a (arith panic-freedom, totality of `inverse`, JCS determinism). +* S5: ECHIDNA tri-state, where "unknown" is not green. + +*Testing and benching* + +* B0: floor of 827/0/15 plus the 14 fail-first tests. +* B1: property tests (`inverse ∘ apply = id`, arith never panics, mixed RMR/RMO rollback never reports success, mode preserved over undo). +* B2: oracle v2 as a required check. +* B3: crash injection, 100 per PR and ≥1000 nightly. EXP-4 first measures today's loss window. +* B4: a second vsh fails closed within 1 s. +* B5: audit tamper suite, plus "no `.vsh*` file under root after e2e". +* B6: fuzz baseline for the 7 targets, plus `journal_recover`, `redirection_parse`, `audit_verify` and `event_parse`. +* B7: benches for `record_operation` at 10/1k/10k history (today O(history)), fsync p50/p95, HMAC verify at 100k events, and blob dedup ratio. +* B8: a non-root job running `cargo test --test security_tests -- --include-ignored`, asserting that euid is not 0. +* B9: `regen-status` idempotency, and a grep gate on unsupported "M" link claims. + +''''' + +== 7. What else needs creating + +*In valence-shell (whole programme):* + +* `tests/regressions_parsed_path.rs`, `durability_tests.rs`, `crash_injection.rs`, `audit_integrity_tests.rs` +* `src/journal.rs`, `src/blobs.rs`, `src/commitment.rs`, `src/anchor.rs` +* `proofs/lean4/{NonVacuity,FinModel,JournalModel}.lean` +* `proofs/MANIFEST.toml` and `scripts/gen-proof-manifest` +* `docs/{OS-ASSUMPTIONS,REFINEMENT-RELATION,PROOF-SYSTEM-STATUS}.adoc` +* `scripts/regen-status.sh`, Justfile `test`/`quality` recipes, `deny.toml` +* Session 1 (proof-first): `impl/vsh-core/` (pure workspace crate; the Aeneas input); the `--safe --without-K` version of the #221-repaired `proofs/agda` tree plus `GoldenTraces.agda` and `All.agda`; `proofs/lean4/GoldenTraces.lean`; the `proofs/lean4-refine/` spike package; `scripts/{gen-golden,toolchain-check.sh}`; `tests/golden/`; `docs/TOOLCHAIN.adoc`; `docs/decisions/` (kill and GO/NO-GO records) +* Session 2+: the journal, blobs, commitment and anchor modules; `JournalModel.lean`; `archive/proofs/` with a successor table +* Later: `schemas/shell-event.v0.json`, `docs/SHELL-EVENT-SPEC.adoc`, and the Agda feeder instances (after G1–G5) + +*In other repos* (all later or parked; see §11): + +* absolute-zero `CNOInterface.agda` (T7) +* januskey JK-1..JK-4 +* residual-evidence `Examples/VshObliterate.agda` +* epistemic `Applications/AuditLog/AuditReceipt.agda` +* typell `vsh-txn` spec and session monitor +* one shared estate Agda pin + +''''' + +== 8. Owner decisions, rated + +Scores are *E = elegance and correctness*, then *D = dependability and security/privacy*, out of 10. + +* OD-0 to OD-21 are the synthesis's options, scored as the mean of 3 judges for OD-0 and by the synthesis for the rest. +* OD-22 to OD-29 come from the critique, are scored by me, and are labelled so. +* *[ELEGANT]* marks the default arm. +* *RULED* marks the 2026-11-04 rulings. + +=== Ruled + +[cols=",,",options="header",] +|=== +|# |Decision |Ruling +|*OD-0* |Overall strategy. Options: A proof-first [ELEGANT] 8.7 / 6.7 · B engineering-first 7.7 / 9.0 (most dependable) · C verified script subset 7.3 / 5.7 · D contrarian 7.0 / 7.7 · S synthesis |*RULED: A, proof-first.* Its dependability gap is closed by running the Phase 1 hole fixes in parallel with the proof work, which A's own rung order requires. +|*OD-22* |v1 gate "all reversible operations proven across six systems" |*RULED: witness threshold* [ELEGANT] 9 / 8. ≥2 independent CI-gated provers plus the oracle per op, computed from the MANIFEST. +|*OD-23* |First feeder edge |*RULED: none until G1–G5.* After that, echo-types `EchoResidueCell` + `EchoDeniability` [ELEGANT] 9 / 7 if EXP-agda passes, otherwise residual + epistemic (5 files / 284 lines) 7 / 8. +|*OD-1* |Prover stack |*Follows from OD-0:* Lean canonical, plus the Agda mirror as second witness, plus Z3. Archive Coq, Isabelle and Mizar after porting [ELEGANT] 9 / 7. The archive step is gated by OD-22, which closes the risk the synthesis flagged (archiving the best-gated tree too early). +|=== + +=== Open, with provisional defaults the session can use + +[cols=",,,",options="header",] +|=== +|# |Decision |Options (E / D) |Recommendation (provisional default) +|*OD-24* _(critique)_ |Audit authentication |(a) HMAC chain only: designated-verifier, so the key holder can rewrite 6 / 7 · (b) *Ed25519 chain over JCS bytes plus anchors*: the audited party can verify, matching MAA's "no party above audit" [ELEGANT] 9 / 9 · (c) HMAC per event plus Ed25519-signed checkpoints, like a certificate-transparency "signed tree head" 8 / 8 |(b) if a signing-key story is acceptable, otherwise (c). Needed only in session 2 (E7). +|OD-2 |F-1 route |(a) Aeneas spike [ELEGANT] 9 / 8 · (b) Lean `@[export]` linked into Rust 5 / 5 · (c) Coq FMaps extraction 5 / 6 · (d) differential-only, honestly labelled 6 / 7 |(a) with a 2-session kill; on NO-GO, owner decides between the proof-first fallback and (d) — see P9. Reject (b): it adds an unsafe seam and proves nothing about Rust. _Note:_ the owner's ROADMAP_TO_V1 D2 says "tested correspondence for v1.0, verified kernel for v2.0", so the spike is a labelled departure in timing only. +|OD-3 |RMO inside a txn |(a) refuse 8 / 9 · (b) typed Irrevocable protocol state [ELEGANT] 9 / 8 · (c) implicit commit 6 / 7 |(a) now, (b) when the typell spec lands +|OD-4 |Obliterate scrubs prior payloads |(a) yes, scrub and record [ELEGANT] 9 / 9 · (b) audit-only claim 5 / 4 |(a) +|OD-5 |Persistence |(a) journal is the single source of truth [ELEGANT] 9 / 9 · (b) WAL beside the state file 6 / 7 · (c) embedded DB 5 / 7 |(a), staged after E3 +|OD-6 |januskey dependency |(a) local CAS now, swap later 8 / 9 · (b) git dependency now 8 / 5 · (c) widen its enum 4 / 6 · (d) a versioned crate with a generic op kind [ELEGANT] 9 / 8 |(a), moving to (d) +|OD-7 |Event format |(a) JSONL + JCS 7 / 8 · (b) deterministic CBOR + COSE [ELEGANT] 9 / 8 · (c) A2ML 3 / 5 (retired) · (d) defer 6 / 6 |(d) until E10, then (a) with a path to (b) +|OD-8 |Digest |(a) alg-tagged, SHA-256 default [ELEGANT] 9 / 9 · (b) SHA-256 only 6 / 8 · (c) BLAKE3 only 6 / 7 |(a). Reserve a `blake3-merkle` form for ochrance compatibility (januskey "Deferred"). +|OD-9 |Key lifecycle |(a) key file, fail closed when configured 8 / 8 · (b) mandatory key 6 / 9 · (c) januskey KeyManager [ELEGANT] 9 / 9 · (d) OS keyring 7 / 8 |(a) now, (c) later +|OD-10 |Anchor target |(a) pluggable sinks (file, git, later ochrance) [ELEGANT] 8 / 8 · (b) RFC 3161 TSA 7 / 9 · (c) none 6 / 6 |(c) until E7, then (a) +|OD-11 |Rollback partial failure |(a) resumable [ELEGANT] 9 / 9 · (b) clear and report (current) 4 / 5 |(a) +|OD-12 |State location |(a) XDG keyed by session root [ELEGANT] 9 / 9 · (b) `/.vsh/` 6 / 5 · (c) cwd (current) 2 / 2 |(a). Must key by the *session root*, not the cwd-tracking root (critique). +|OD-14 |Estate Agda pin |(a) 2.6.4.3 + Debian stdlib 2.1-4 7 / 8 · (b) 2.6.4.3 + stdlib v2.3 7 / 6 · (c) Guix-pinned by SHA [ELEGANT] 9 / 9 |(a) after EXP-agda, (c) as the target +|OD-15 |Verified-script subset |(a) later, optional 8 / 6 · (b) now 7 / 5 · (c) never 5 / 7. *Sub-choice:* *Oblibeny* as the subset (the owner's named NW-6 route, also MAA's reference language) [ELEGANT] vs a vsh `Script.lean` |(a). Prefer Oblibeny if inspectable (not cloned; Unverified). Use jtv-halting-islands-ct's "grammar membership = termination certificate" as the design pattern. +|OD-16 |Parked layers |(a) archive with a README 8 / 8 · (b) keep, labelled parked 5 / 6 · (c) wire the Idris2 ABI now 7 / 6 · (d) *archive everything except `src/abi`, kept as the januskey Phase-3 ochrance ABI seam* (mine) 8 / 8 |(d). Departure from the synthesis's (a): ROADMAP v2.0 keeps `src/abi` and Zig FFI as planned surfaces. +|OD-17 |MCP runtime |(a) Rust over L1a+L2 8 / 9 · (b) AffineScript + Bun once affinescript#746 adds hashing/HMAC [ELEGANT per the estate language policy] 8 / 4 |(a). Departure: `impl/mcp` today is an in-flight AffineScript port (only `.affine` files, with a stale `deno.lock`). +|OD-18 |NW-1 canonical record |(a) T7 Agda, setoid-parametric [ELEGANT] 9 / 8 · (b) Q10 Coq 4 / 6 |(a), and mark Q10 superseded +|OD-19 |Mathlib policy |(a) only in `lean4-refine` [ELEGANT] 9 / 8 · (b) everywhere 6 / 6 · (c) none 7 / 7 |(a) +|OD-20 |`residue_class` vocabulary |(a) local exploratory enum 6 / 7 · (b) wait for ET-RESCLASS-1 [ELEGANT] 9 / 7 · (c) residual-evidence verdicts 7 / 7 |(a), labelled exploratory. Keep the bridge field name `echo_residue_class`. +|OD-21 |Resource bound numbers |(a) the owner picks depth, per-op cap and byte budget [ELEGANT] 9 / 9 · (b) count-only 3 / 3 |(a) +|OD-25 _(mine)_ |Rollback admissibility rule |(a) `inverse()==None` means hard failure 7 / 8 · (b) *loss grade*: rollback admissible iff `traceGrade = fin 0`, mirroring januskey `Reversibility.agda`, with `explain` printing the grade [ELEGANT] 9 / 8 |(a) now, with the grade table as data so that (b) is a refactor, not a rewrite. (b) depends on `resource-algebra` (not cloned). +|OD-26 _(mine)_ |`cd` and the sandbox |(a) confine `cd` to the session root 8 / 9 · (b) allow `cd` out, but refuse journalled mutations outside the root [ELEGANT] 9 / 8 · (c) absolute paths, no sandbox 5 / 4 |(a) now (closes the escape in hours), (b) later. +|OD-27 _(mine)_ |Variable ops in history |(a) persist variables 7 / 7 · (b) mark variable ops session-scoped and not journalled 8 / 8 |(b) +|OD-28 _(critique)_ |Placement of proofs that import two or more feeders |(a) vsh `proofs/agda/feeds` 7 / 7 · (b) `nextgen-typing/verification/proofs` per its placement rule [ELEGANT per estate boundary] 8 / 6 (that repo has no Agda CI yet) |Avoid the question by choosing a single-feeder edge (OD-23 (a)). Otherwise (b), plus a CI lane there. +|OD-29 _(mine)_ |Idris2 role |(a) "no new scope" 6 / 7 · (b) Idris2 list model as the reference finite model 6 / 7 · (c) Lean FinFS using the Idris2 theorem shapes as its spec, with Idris2 as a second differential oracle if codegen works [ELEGANT] 9 / 8 |(c). Resolves the frontier question "promote Idris2 to load-bearing?". +|=== + +''''' + +== 9. The ultracode session plan (session 1, proof-first) + +*Goal:* close the holes, then make the spec sound and fully CI-built. Stand up FinFS with refinement for 4 verbs, oracle v2 with undo, the golden seam, and the Agda mirror as second witness. Record an Aeneas GO or NO-GO. Out of scope for this session: feeder imports (OD-23), archival, the journal, receipts and MCP. + +*Size:* the default workflow size guideline is under 10 agents per workflow. The plan uses 2 resumable workflows: + +* Workflow A covers Phases 0–2, with about 9 agents. +* Workflow B covers Phases 3–6, with about 9 agents. + +Gate checks run in the coordinating context between phases. + +*Reference cost:* the planning run used 50 agents, ~10.9 M subagent tokens and ~65 minutes. Implementation agents cost more each, because they compile and test. + +*Branch and PR discipline:* + +* Work on `claude/laughing-hawking-pibzji`, in *one PR per phase*, all signed. +* Any change to a sibling repo (absolute-zero, echo-types and so on) is out of scope for session 1. + +[cols=",,,",options="header",] +|=== +|Phase |Agents |Gate (machine-checked) |Parallel +|*0 Provision + ground truth* |toolchain-provisioner (elan + Lean v4.34.1; z3; coqc 8.18; Agda 2.6.4.3 with `--no-libraries` and, for EXP-agda, Debian stdlib 2.1-4; opam + Charon/Aeneas at a recorded rev; cargo-fuzz + nightly; cargo-deny; write `docs/TOOLCHAIN.adoc`); ground-truther (cargo test/fmt/clippy; `lake build` per lib, recording the exit code and first error; Coq build; verify-z3) |`scripts/toolchain-check.sh` prints each tool's exact version, or marks it *unavailable* (never reported as passed). `docs/audits/BASELINE-.adoc` lists exit codes for all 12 Lean libs and the cargo summary (827/0/15 expected). If Lean is unavailable, only the Lean-dependent agents and gates are skipped and reported Unverified: P0, P1, P1b, P3, P4, the Lean golden check and the Aeneas spike. The Coq, Z3 and Idris2 work in Phase 2, the honest-UI, MANIFEST and Agda work in Phase 4, and the benches, crash probe and spec drafts in Phase 5 still run, and their partial phase results are reported. |yes +|*1 Runtime holes* (Rust; runs in parallel with Phase 2) |bug-reproducer (E0: 14 fail-first tests, plus the security test with real assertions); fixer-A (E1); fixer-B (E1b: session root and resolved-target containment); fixer-C (E1c RMO ordering, scrub, txn refusal, resumable rollback; E1d 0600 + atomic + fail-loud + inode metadata); core-extractor (E2: `vsh-core` crate, one inverse table, drift guard); adversarial-reviewer |On the base commit the 14 tests fail for the documented reasons (the run is recorded). After the fixes, all 14 pass, and every symlink case leaves the outside tree byte-identical. `cargo test` has 0 failures and a total ≥ 827 plus the new tests. Clippy is clean. `! grep -rn -e 'std::fs' -e 'anyhow' -e 'PathBuf' impl/vsh-core/src` succeeds (no matches). It uses separate `-e` patterns, with no pipe characters to escape. A proptest of `eval_arith` runs 10k cases under debug and release with no panic. The state file is 0600. |yes +|*2 Spec soundness* (Lean, Coq, Z3, Idris2) |lean-prover-1 (EXP-1, P0, NonVacuity, EXP-2); lean-prover-2 (P1b: repair the 4 libs, port the Coq RMO theorems); ci-wirer (P1 named targets, axiom gate; P2 Coq `pipefail` + per-theorem allow-lists; Z3 SAT checks); faithfulness-prover (P0b: Idris2 NoDupKeys, Z3 `is-empty-dir` definition, faithfulness table) |`lake build` over all 12 libs plus `NonVacuity` and `model_oracle` exits 0. Zero non-comment `sorry` or `axiom`. Witness count equals precondition count (scripted). `#print axioms` stays within the allow-list. The Coq Print Assumptions step fails the job on an unlisted axiom (tested with a deliberately bad allow-list). The Idris2 build stays `--total` with 0 holes. |yes +|*3 FinFS + oracle v2 + golden seam* |lean-prover-3 (P3: FinModel with refinement for mkdir, rmdir, touch, rm); oracle-engineer (P4: oracle v2 + Rust generator; EXP-6 negative control); seam-engineer (E-golden: the corpus, the Rust test, GoldenTraces.lean) |`lake build FinModel GoldenTraces && lake build model_oracle` exits 0 (the oracle is the lowercase `lean_exe model_oracle` target, as in the Justfile and `lean-verification.yml`). `cargo test --test model_oracle_correspondence -- --ignored` passes on bounded-exhaustive plus ≥1000 random sequences, including undo, redo and txn, with 0 disagreements. The negative control fails as expected. The golden Rust test passes. `#print axioms` on the refinement theorems stays within the allow-list. |partly (seam waits on P3's model shape) +|*4 Second witness + honest UI* |agda-prover (P5: the #221 tree taken to `--safe --without-K` for the 4 verbs, plus `GoldenTraces.agda`); ci-wirer-2 (an Agda CI lane with pinned versions); honesty-engineer (E5: MANIFEST, `proof_refs` reads it, delete the overclaims, per-op witness table) |`agda --safe --without-K proofs/agda/All.agda` exits 0 in CI on the pinned toolchain. `--safe` accepting the tree is the postulate check. As a belt-and-braces check, `grep -nE '^[[:space:]]*postulate\b' proofs/agda/*.agda` returns nothing; it matches declarations only, not prose or comments. The sequence ids in `tests/golden`, `GoldenTraces.lean` and `GoldenTraces.agda` are equal as sets (a three-way scripted check). The G3 gate (`! grep` with separate `-e` patterns) exits 0, meaning no over-claim string remains, and `cargo test --features echidna` passes. `proof_refs_resolve` passes. The MANIFEST shows ≥2 witnesses (Lean + Agda) plus the oracle for mkdir, rmdir, touch and rm. |yes +|*5 Experiments* (report only) |aeneas-spiker (P6: GO or NO-GO); agda-prober (EXP-agda: echo-types `EchoResidueCell`/`EchoDeniability` cone, and residual + epistemic, under 2.6.4.3 + stdlib 2.1-4. This decides OD-23's post-G5 arm. Nothing is imported.); bench-runner (EXP-persist: `record_operation` at 10/1k/10k; EXP-fsync p50/p95 on ext4 and tmpfs, input to E4 in session 2); crash-prober (EXP-4: the loss window on current code); spec-drafter (DRAFT `OS-ASSUMPTIONS`, `REFINEMENT-RELATION`, `JOURNAL-PROTOCOL` and `CONTAINMENT-THREAT-MODEL` docs, each refining the gates above) |A written report: Aeneas GO (`lake build VshRefine` with `core_mkdir_refines` proved and axioms recorded) or NO-GO (pins and errors); the Agda pin verdict for both OD-23 arms; bench numbers; the crash-loss window; 4 DRAFT docs. *Decision rules:* every intent record is fsynced before its own mutation, whatever the benchmark says. If fsync p95 exceeds 2 ms on ext4, only *commit* records are group-committed per command line. A crash then leaves at most uncommitted-but-intended ops, which recovery handles. It never leaves a mutation without a durable intent. NO-GO goes to the owner for the P9 fallback decision. |yes +|*6 Consolidate + cold verify* |doc-reconciler (E8: regen counts; THEORY-FEED NW-1/NW-3 fixes; PROOF-OPEN-FRONTIER updates (F-2 closed, the Lean vacuity recorded and closed, C-9 restated); the ROADMAP_TO_V1 witness-gate amendment; PROOF_HOLES_AUDIT; CLAUDE.md); verifier (re-runs every gate from a fresh clone: `lake clean`, a fresh cargo target, `--ignore-interfaces` for Agda) |All Phase 1–4 gates pass from cold. `regen-status.sh` run twice gives an empty diff. `check-bridge-forbidden-phrases.sh` passes. No "M" cell is claimed without a CI-built import. |no +|=== + +*Session 2 (sequenced; each item starts after its predecessor's gate):* + +[arabic] +. FinFS and the Agda mirror extended to all of O (G5, G6). +. E3 and E4: the full durable store and the journal, designed together with P8 `JournalModel.recover_sound`. Then crash injection, 100 per PR and ≥1000 nightly (G2). +. E6 and E7: the keyed audit (OD-24) and verify (G7). +. P9 full refinement if P6 was GO; otherwise the owner's fallback ruling. +. P10 archival, once the MANIFEST shows G6 holding without Coq, Isabelle and Mizar. + +*Session 3+ (after G1–G5):* P11 estate theory (T7 `CNOInterface` in absolute-zero, needing that repo's own PR; the `VshCNO` instance; the OD-23 edge; epistemic audit receipts). After that: ShellEvent, the januskey CAS swap, the typell monitor, MCP. + +*Toolchain prerequisites:* + +* Present during planning: rustc 1.97.0 and cargo only. +* Everything else installs through the agent proxy. A failed install is recorded as *unavailable* and the dependent phases are skipped. A failure is never reported as a pass. + +*Stop rules:* + +_Tooling and proofs_ + +* No proof file is committed unless it was checked. If a toolchain is missing, the phase is reported Unverified. +* Stop any proof slice that needs `sorry`, a postulate, `believe_me` or an axiom outside the allow-list, and report it instead. + +_Tests and safety_ + +* Revert any change that drops `cargo test` below the floor. Never `#[ignore]` a test to get green; the only exception is the root-only privilege test, which is `#[ignore]`d only because the non-root job runs it with `--include-ignored`. +* An on-disk format change without backup-then-migrate means stop and escalate. In session 1 the format changes only by adding fields, and old files must still load. +* New data loss found on an unchanged path means fix or document it before anything else. + +_Kill rules (recorded in `docs/decisions/`)_ + +* Aeneas: 2 sessions in total, or an incompatible pin. +* Lean lib repair: 1 day each, then a visible quarantine. +* FinFS: ~600 LoC for 4 verbs, then re-plan. +* Agda mirror: ~700 LoC for 4 verbs, then re-plan. +* EXP-2: if more than half the composition theorems break after the `isEmptyDir` fix, re-plan before building FinFS on top. + +_Feeders and archival_ + +* No feeder import before G1–G5 (OD-23). +* No archival before G6 holds without the archived provers (OD-22). + +_Repository and owner boundaries_ + +* Never: admin-merge, force-push, delete branches or layers (archive instead), edit licence text, SPDX headers or third-party code, push unsigned commits, or promote a claim from a status document rather than a run. +* Outward-facing actions (sibling-repo PRs, required-check changes, anchor publication) happen only with owner confirmation. + +*Experiments that decide the long routes:* + +* EXP-1: vacuity as a theorem. +* EXP-2: blast radius of the fix. +* EXP-4: crash-loss window. +* EXP-5: Lean `decide` over FinFS vs `verification.rs`. +* EXP-6: oracle negative control. +* EXP-aeneas (P6). +* EXP-agda: decides the OD-23 arm and the mirror's pin. +* EXP-fsync and EXP-persist: inputs to E4. +* EXP-fuzz-baseline: 10 minutes per existing target. +* EXP-cas: API frictions with januskey `reversible-core`; no dependency is added. + +''''' + +== 10. Tropes, types and logics that may give a more final solution + +*Engineering and persistence* + +* *Event sourcing* (Inference). One append-only log, with state as a fold. This makes WAL, undo, audit and export a single object with a single recovery proof (P8, `JournalModel`), instead of four that drift apart. +* *Transparency-log Merkle tree* (RFC 6962/9162 style). It replaces the "hash chain called a merkle root" in januskey and in the vsh audit, and gives O(log n) inclusion and consistency proofs. Truncation becomes detectable relative to any signed tree head. This is the principled form of OD-10/OD-24. + +*Rust types and grades* + +* *Affine types for undo payloads* (Inference, Rust-native). An undo payload is a linear resource: undo consumes it, and obliterate destroys it. In Rust that is a non-`Clone` `UndoToken` that `undo` and `obliterate` take by value. The current `redo_stack` clone (`state.rs:478-486`) is exactly the violation. This mirrors echo-types `EchoResidueCell` (`once-only`) and januskey's Loss grade at the type level, so it is checked by the Rust compiler with no prover. +* *Loss-graded resource algebra.* A single semiring grading each op as lossless, lossy or obliterating. It also carries cost (MaxPlus, tropical `hub_ceiling_le`). One algebra then covers OD-25 (reversibility) and #190/#191 (bounds). + +*Proof patterns* + +* *Refinement with a runtime-discharged abstraction hypothesis.* The drift guard checks at runtime that the OS state abstracts to the recorded post-state. This is what makes any refinement theorem (P9) say something about the real system. +* *Non-vacuity as a mandatory pattern.* Every precondition gets an inhabitation witness in every prover. This turns a whole defect class into build failures. + +*Semantics and observers* + +* *Choreographic `two-thread-diamond`* (proved in choreographic-types). This is the theorem shape for F-4's first slice, with independence defined as path non-prefix. It is better than a fresh Lean statement. +* *Noninterference* (secret-types TINI over a down-closed observer lattice). This is the eventual statement form for "an observer at trust tier _t_ cannot learn obliterated content". Combined with absolute-zero's `OND5-composition-leaks`, the claim must be made over the joint observer. +* *Grammar membership as a termination certificate* (jtv-halting-islands-ct pattern). This is the cheap totality story for a verified script subset or arithmetic island. + +''''' + +== 11. Beyond this repo (for the maintained list) + +*januskey* + +* JK-1: the manifest root must commit the full canonical op record (measured collision). +* JK-2: atomic `MetadataStore`; the `save()` side has no size cap, so the store can become unopenable. +* JK-3: first `ReversibleExecutor` implementor. +* JK-4: a generic op kind. +* JK-5: move HMAC into `reversible-core`. +* Remove `python3` from e2e. +* Make the Agda and Idris CI lanes required. +* Fix the stale ARCHITECTURE Phase-2 claims. +* Phases 3 and 4 (ochrance ABI; cross-references). +* Deferred: BLAKE3 Merkle compatibility. + +*absolute-zero* + +* Write T7 `CNOInterface.agda` plus an Idris2 mirror. +* Mark Q10 superseded. +* Move the Agda pin off 2.6.3 / stdlib 1.7.3. +* Register or discharge the 5 measured `believe_me` sites (the docs say 10). +* Fix the PROOF-STATUS banner and the ECHIDNA "Production-ready" claim. +* Finish the #175 rename. + +*echo-types* + +* #322: pin Agda (CI uses unpinned apt; the cited `flake.guix` does not exist). +* Make `EchoJanusBridge` content-bearing, and stop naming obliterate "Reversible". +* ET-GEN-1 and ET-RESCLASS-1. +* Add a valence-shell row to `cross-repo-bridge-status.adoc`. +* The bridge doc cites `bridge-status.md`; the real file is `.adoc`. +* Promote the `accountable-shell` exploration (THEORY-FEED:346). + +*residual-evidence-types* + +* RE-1 `VshObliterate` (only if OD-23 picks (b)). +* DECISION-002 (family vs view). +* RE-2 generic checker. + +*epistemic-types* + +* `AuditLog`/`AuditReceipt` plus 5 reject fixtures. +* Record a hosted run id. + +*secret-types* + +* Identity metadata still says rsr-template-repo. +* The doc contradicts PROOF-STATUS. +* No declassification exists yet. + +*typell* + +* `vsh-txn` spec plus session monitor. +* Stale AFFIRMATION (the workspace now builds; 447/0/3). +* README overclaims "cryptographic proof certificates". + +*nextgen-typing* + +* Add a vsh consumer row. +* Amend D-2026-10-12 with the vsh scope ruling. +* Record D204/T7. +* Add Agda CI for `verification/proofs` (it has none). +* Migrate the placement routing off retired A2ML. +* Fix the banned-language line in CLAUDE.md/AGENTS.md. + +*tropical, occupancy, choreographic* + +* Parked. Lean toolchain skew (v4.13/4.15 vs v4.34.1). +* Occupancy `check-agda.sh` is not wired to CI. +* Choreographic proofs CI is not required. + +*anytype and jtv-halting-islands-ct* + +* Citation-level only. JtV's Rust rewrite has 0 tests, and its Creusot `ensures(true)` is vacuous. + +*maa-framework* + +* The absolute-zero submodule pin `87902bb` predates T7. +* The aletheia README overclaims. +* Its PMPL licence is an owner-only flag. + +*Not cloned, so everything about them is Unverified:* ochrance, echidna and echidnabot, proof-burrower, oblibeny, affinescript (#746), systemet, resource-algebra, tangle. + +*Estate-wide* + +* A2ML retirement vs load-bearing vsh files: `ECHO_TYPES_OCHRANCE_BRIDGE.a2ml` is required by `check-bridge-forbidden-phrases.sh`, and `IDRIS2_AXIOMS.a2ml` sits in the idris workflow paths. This needs an owner ruling before CI is touched. +* One Guix-pinned Agda (OD-14). +* Branch protection and required checks are owner-only. +* Commit hygiene: 47 of 58 commits authored as "Test" (use `.mailmap`, never force-push). +* Licence flags (never automated): alkahest PMPL badge, aletheia PMPL licence, `ffi/rust` author line. + +*Owner's charter to reconcile:* `docs/ROADMAP_TO_V1.adoc`. + +* D1–D5. +* Lanes A–G: security tests 15→75 and fuzz targets 7→20, a 24-hour fuzz soak, a MAA guide and man page. +* The six-system gate (OD-22). + +*Issues to keep linked:* valence-shell #51 #62 #63–#66 #90–#93 #162 #189–#192 #210; januskey#137; absolute-zero#167/#175; echo-types#322/#329; nextgen-typing#118; typell#62; tropical-types#57/#58. + +''''' + +== 12. Risks + +*Specific to the proof-first spine* + +* *Slower to a dependable shell.* Durability (the journal) lands in session 2. This is mitigated by fixing the 14 measured holes, plus a 0600 atomic state file, in session 1, in parallel with the Lean work. +* *Lean↔Agda transcription drift.* The mirror is a transcription, not a proof of equivalence. It is mitigated by the golden corpus, which both provers check against the same sequence ids. It is graded "checked", never "mechanised". +* *Archiving the best-gated tree (Coq) too early.* Mitigated by the OD-22 witness gate, plus porting the Coq RMO theorems into Lean first. +* *The Aeneas fallback* (Lean `@[export]` linked into Rust) would add an unsafe FFI seam and a Lean runtime to every build. It is not taken automatically; on NO-GO it is put to the owner. + +*Proof-side* + +* *Vacuity fallout.* The `isEmptyDir` fix will break Lean theorems that relied on vacuity. That is good, but it will look like a regression. EXP-2 sizes it. +* *Testing is not proof.* The oracle and golden traces test equivalence; they do not prove it. Any Lean↔Agda seam is labelled "checked", never "mechanised". +* *Aeneas sink.* Toolchain pins can eat weeks. The kill rule and separate package are the mitigations. +* *Agda pin skew* makes every cross-repo edge brittle. +* *Evidence provenance.* Every proof-side fact here comes from source reads. The "~34 → ~65 checked Lean theorems" figure is a grep estimate. + +*Runtime and persistence* + +* *State-format migration* breaks existing state files. Backup-then-migrate is mandatory. +* *Journal recovery bugs are worse than no journal.* The crash harness and fuzzing must be green before it is on by default. +* *Drift guard* has false positives on benign touches, and an unavoidable TOCTOU window. Mitigations: `O_NOFOLLOW`, a re-check, and documenting the bound. +* *OS semantics.* fsync and rename behaviour vary by filesystem. Claims hold only under the OS-assumption ledger. +* *Concurrency.* `flock` is same-host advisory only. F-4 and #90 stay open. +* *CoW/SSD.* Obliterate stays best-effort. The scrub fixes the shell-level leak, not storage remanence. + +*Security and privacy* + +* *Crypto overclaim.* HMAC is designated-verifier. Truncation after the last anchor is undetectable. +* *Privacy.* Until E1d (session 1) lands, secret file bytes sit in a 0644 state file in cwd. Until E6 (session 2) lands, the residue holds plaintext paths, user and pid. No export or MCP may ship before path commitments. +* *Latent catastrophic API.* `secure_erase_file` stays a hole until E1. + +*Process and owner* + +* *Owner bandwidth.* About 30 decisions. Phases 0–4 run on labelled provisional defaults, which may need reverting. +* *CI churn.* Governance, Mirror and ECHIDNA are red. Fix or isolate them before adding required checks. +* *Status-doc drift recurs.* Without `regen-status` in CI, this plan's counts will drift too. +* *Parallel sessions* rebase branches in estate repos. Re-fetch, use `--only` paths, never force-push. + +''''' + +== 13. What was not verified + +* No Lean, Coq, Agda, Idris2, Isabelle, Mizar or Z3 run happened here. Specifically Unverified: +** that `RmdirPrecondition` is uninhabited (needs EXP-1); +** the 0-admits claim for Coq; +** the 0-holes claim for Idris2; +** the existence and buildability of every feeder theorem cited; +** whether echo-types builds under `2.6.4.3` + stdlib 2.1-4. +* The CI run states come from `gh` snapshots taken by the readers on 2026-10-27, not re-queried today. +* Not cloned: ochrance, echidna, oblibeny, affinescript, resource-algebra, systemet, tangle. +* The raw workflow output (synthesis, judgements, critique and per-claim skeptic evidence) stayed in the planning session's container and is not committed. Every measured claim here gives its file and line, or the command used to reproduce it, so it can be re-checked from the repo.