Three v1.0 items: E-Grade launcher, mechanized correspondence oracle, RMO secure-deletion runtime (#165)

Three outstanding items, in order, each verified with the real
toolchain.

## 1 — Launcher conforms to the E-Grade Launcher Standard

`launch.sh` implements the Hyperpolymath **E-Grade Launcher Standard**
(fetched from the public `hyperpolymath/standards`): full mode surface
`--auto/--start/--stop/--status/--browser/--web/--integ/--disinteg/--help/--version`,
version format `vsh <ver> (<sha>) [<platform>]`, idempotent Linux
desktop integration (copy-not-symlink, `Terminal=true`, `.desktop` at
0444, config/logs preserved on `--disinteg`), desktop-tools resolution
ladder with graceful no-op degradation, XDG PID/log paths.

Because `vsh` is a **foreground terminal shell with no server**, the
server-oriented clauses (nohup daemon, `wait_for_server` URL polling,
browser launch) are **honestly declared *deferred*** in the
`a2ml-metadata-block` header rather than silently skipped.
`scripts/run.sh` is the canonical startup command the standard searches
for; `just run`/`just launch` delegate to it. `docs/LAUNCHER.md` is the
conformance attestation.

*Verified:* every mode, a full `--integ`/`--disinteg` idempotency cycle,
shellcheck clean.

## 2 — Mechanized correspondence: compiled proven model as test oracle

`proofs/lean4/ModelOracle.lean` (`lean_exe model_oracle`) compiles the
**exact proven** model defs
(`mkdir/rmdir/createFile/deleteFile/fsUpdate`) into an oracle.
`impl/rust-cli/tests/model_oracle_correspondence.rs` generates
precondition-respecting sequences, applies them to the real Rust
`ShellState`, drives the same sequence through the compiled Lean model,
and asserts agreement at every touched path.

**1218 probes agree across 200 sequences.** This makes the proof
artifact itself the oracle (stronger than hand-transcribed property
tests) — but it is honestly **still differential testing, not a full
refinement proof** (the v1.0 blocker).
`docs/LEAN4_RUST_CORRESPONDENCE.md` documents why the Coq extraction is
*not* executable (`Path → option FSNode` domain + classical axioms in
`is_empty_dir_dec`; needs `FMaps.t FSNode` migration) and the roadmap.
Wired into `lean-verification.yml` CI; `just test-correspondence-model`.

## 3 — RMO secure-deletion runtime (the big one)

`obliterate` was fully implemented in `commands/secure_deletion.rs` but
**never wired into dispatch** — unreachable dead code. Added the
`Command::Obliterate` variant, parser case (`--force`), and executor arm
→ `secure_deletion::obliterate_path`. Added the **audit residue**:
obliterate appends to `<sandbox-root>/.vsh-audit.log` — the
MAA/GDPR-Art.17 attestation that survives the deletion.

*Verified:* `impl/rust-cli/tests/obliterate_rmo_tests.rs` (6 tests —
wiring, destruction, audit residue, irreversibility,
no-plaintext-remains), full suite green, and driven through the real
`vsh` binary in script mode.

**Honest scope:** best-effort 3-pass overwrite on in-place filesystems
only; CoW/SSD need hardware `secure_erase`; audit HMAC signing pending;
**not a complete GDPR framework**. Status docs reconciled from "RMO
stubs only" across CLAUDE.md, README, FAQ, ROADMAP(+_TO_V1), TOPOLOGY,
`docs/wiki/*`, `methodology.a2ml`, and the ECHO-TYPES-OCHRANCE bridge
(adoc + a2ml, in lock-step).

## What remains genuinely open

Full mechanized Lean→Rust *refinement proof* and a complete GDPR/RMO
framework (hardware erase, HMAC-signed audit) — both flagged honestly
in-repo, neither overclaimed.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU

---
_Generated by [Claude
Code](https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU)_

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/lean-verification.yml

@@ -106,6 +106,18 @@ jobs:
           cargo test --test correspondence_tests
           cargo test --test property_correspondence_tests
 
+      - name: Build Lean model oracle (proof artifact as test oracle)
+        run: |
+          source $HOME/.elan/env
+          cd proofs/lean4
+          lake build model_oracle
+          ls -lh .lake/build/bin/model_oracle
+
+      - name: Differential correspondence (proven Lean model vs Rust impl)
+        run: |
+          cd impl/rust-cli
+          cargo test --test model_oracle_correspondence -- --nocapture
+
       - name: Report Rust binary size
         run: |
           echo "Rust binary: $(stat -c%s impl/rust-cli/target/release/vsh) bytes"

.machine_readable/ECHO_TYPES_OCHRANCE_BRIDGE.a2ml

@@ -49,7 +49,7 @@ do-not-claim = "total erasure"
 name = "Remove-Match-Obliterate (irreversible + audit residue)"
 echo-reading = "proof-relevant certificate of elimination with permitted audit residue"
 do-not-claim = "undoable deletion"
-current-status = "stubs only"
+current-status = "best-effort obliterate implemented + wired (3-pass overwrite + unlink + append-only audit residue); full RMO/GDPR framework incomplete (no hardware erase for CoW/SSD, no HMAC-signed audit)"
 
 [valence-shell-cases.narration]
 name = "explain / checkpoint / restore / diff / replay"
@@ -78,7 +78,7 @@ ochrance-usage = "name receipts and attestation surfaces; do not claim crypto gu
 [agent-rules.forbidden-moves]
 production-ready = "do not claim valence-shell is production-ready"
 lean-rust-mechanised = "do not claim the Lean-to-Rust correspondence is mechanised"
-rmo-gdpr-beyond-stubs = "do not claim RMO/GDPR support exists beyond stubs"
+rmo-gdpr-beyond-stubs = "do not claim RMO/GDPR beyond the implemented best-effort obliterate (in-place FS only, no hardware erase, no HMAC-signed audit); do not claim a complete GDPR compliance framework"
 echo-proves-implementation = "do not claim Echo Types proves Valence Shell implementation correctness"
 ochrance-crypto = "do not claim Ochrance cryptographic integrity while hash/attestation gaps remain"
 exploratory-as-core = "do not merge exploratory Echo bridges into core claims without checking echo-types/docs/bridge-status.md"

.machine_readable/bot_directives/methodology.a2ml

@@ -101,7 +101,7 @@ constraints = [
   "Coq has 0 remaining real proof gaps: obliterate_overwrites_all_blocks is CLOSED (Print Assumptions: Closed under the global context, re-verified 2026-07-16 under Coq 8.18.0) — see docs/PROOF_HOLES_AUDIT.md",
   "Agda has 1 structural axiom (funext) — provable in cubical Agda, intentional in intensional TT",
   "Coq has 1 justified decidability axiom (is_empty_dir_dec) — infinite-domain Filesystem = Path -> option FSNode; switching to FMaps.t FSNode is the documented migration",
-  "RMO (GDPR / secure deletion) primitives are stubs in impl/rust-cli/src/commands/secure_deletion.rs — proofs exist for the model, runtime does not yet bind to them",
+  "RMO (GDPR / secure deletion): the obliterate command IS implemented and wired (parser+executor -> commands::secure_deletion::obliterate_path; 3-pass overwrite + unlink + append-only audit residue at <root>/.vsh-audit.log; tests/obliterate_rmo_tests.rs). Best-effort on in-place filesystems only; CoW/SSD need hardware secure_erase; audit HMAC signing still pending. Do NOT claim a full GDPR compliance framework.",
   "OCaml extraction path exists in proofs/coq/extraction.v but the extracted code is not wired into a build target",
   "Idris2 ABI carrier has 2 holes + 10 partial markers per the 2026-06-01 deep audit (issue #42) — these are the FFI boundary obligations",
 ]

CHANGELOG.adoc

@@ -17,6 +17,67 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Full POSIX shell compliance (subset)
 - RMO (Remove-Match-Obliterate) proofs for GDPR compliance
 
+=== Added — 2026-07-17
+
+==== RMO / secure deletion (runtime)
+- `obliterate` is now **wired into the shell** and reachable from the REPL and
+  scripts. It was previously implemented in `commands/secure_deletion.rs` but
+  never dispatched (no `Command` variant, parser case, or executor arm), so it
+  was unreachable dead code. Added `Command::Obliterate { path, force, .. }`, the
+  `"obliterate"` parser case (with `--force`/`-f`), and the executor arm routing
+  to `secure_deletion::obliterate_path` (file/dir dispatch). Proof reference:
+  `OBLITERATE_IRREVERSIBLE`.
+- **Audit residue**: obliterate now appends an append-only record to
+  `<sandbox-root>/.vsh-audit.log` — the MAA attestation that survives the data
+  destruction (GDPR Article 17 evidence). Data is destroyed; proof-of-deletion
+  persists.
+- Tests: `impl/rust-cli/tests/obliterate_rmo_tests.rs` (6 tests) — dispatch
+  wiring, missing-operand error, end-to-end destruction, audit residue,
+  irreversibility (undo cannot resurrect), and no-old-plaintext-remains. Full
+  suite green; verified through the real binary in script mode.
+- **Honest scope**: best-effort 3-pass overwrite (random/0x00/0xFF + fsync) on
+  in-place filesystems only. CoW (btrfs/ZFS/APFS)/SSD FTL defeat overwrite (use
+  `secure_erase` for hardware NIST SP 800-88 Purge); audit-log HMAC signing is
+  still pending. NOT a complete GDPR compliance framework. Status docs
+  reconciled from "RMO stubs only" accordingly.
+
+==== Correspondence (mechanized differential oracle)
+- `proofs/lean4/ModelOracle.lean` + `lean_exe model_oracle` — compiles the
+  **proven** Lean model definitions (`mkdir`/`rmdir`/`createFile`/`deleteFile`/
+  `fsUpdate`) into a standalone oracle that reports the node type at probe paths.
+- `impl/rust-cli/tests/model_oracle_correspondence.rs` — differential test that
+  generates precondition-respecting operation sequences, applies them to the real
+  Rust `ShellState`, runs the same sequence through the compiled Lean model, and
+  asserts they agree at every touched path. **1218 probes agree across 200
+  sequences.** This makes the proof artifact itself the test oracle (stronger
+  than hand-transcribed property tests); it remains differential testing, not a
+  full refinement proof — the latter is still the v1.0 blocker. The test skips
+  cleanly when the oracle is not built.
+- `just build-model-oracle` / `just test-correspondence-model`; wired into
+  `lean-verification.yml` CI.
+- `docs/LEAN4_RUST_CORRESPONDENCE.md` documents the harness, why the Coq
+  extraction is not executable (function-typed filesystem + classical axioms;
+  needs `FMaps.t FSNode` migration), and the roadmap to full mechanization.
+
+==== Launcher (E-Grade Launcher Standard)
+- `launch.sh` — a standard-conformant launcher implementing the Hyperpolymath
+  E-Grade Launcher Standard mode surface: `--auto` (default), `--start`,
+  `--stop`, `--status`, `--browser`/`--web`, `--integ`, `--disinteg`, `--help`,
+  `--version`. Version output matches the required
+  `vsh <version> (<sha>) [<platform>]` format. Desktop integration (Linux
+  first-class) is idempotent, copies rather than symlinks, sets `Terminal=true`,
+  writes the `.desktop` at 0444, and `--disinteg` preserves config and logs.
+  Sources `keepopen.sh`/`soft-attach.sh`/`gui-error.sh` via the published
+  resolution ladder with graceful no-op degradation when the desktop-tools are
+  absent. PID/log paths use XDG dirs (never `/tmp`). Server-oriented clauses
+  (nohup daemon, `wait_for_server` URL polling, browser launch) are honestly
+  **declared deferred** in the `a2ml-metadata-block` header, since `vsh` is a
+  foreground terminal shell with no HTTP server. See `docs/LAUNCHER.md`.
+- `scripts/run.sh` — the canonical startup command the standard searches for
+  (`{repo-dir}/scripts/run.sh`); builds the release binary on first use and
+  execs the shell.
+- `just run` / `just launch` now delegate to `./launch.sh --auto`.
+
 === Added — 2026-07-16
 
 ==== Launcher

CLAUDE.md

@@ -53,8 +53,8 @@ The Rust CLI is a functional interactive shell with these features:
 - NOT a full POSIX shell (word splitting in external command args, $IFS in all contexts, full function nesting still incomplete)
 - NOT formally verified end-to-end (Lean -> Rust is ~95% confidence via property testing, not proven)
 - NOT a replacement for bash/zsh in current state
-- No GDPR compliance (RMO/secure deletion are stubs)
-- No mechanized correspondence proof (property testing only)
+- Partial GDPR/RMO: the `obliterate` secure-deletion command is implemented and wired (3-pass overwrite + unlink + append-only audit residue), best-effort on in-place filesystems only — CoW/SSD need hardware erase and audit HMAC signing is still pending, so this is NOT a full GDPR compliance framework
+- No mechanized correspondence proof (property testing only; a compiled-Lean-model differential oracle now backstops it — see `docs/LEAN4_RUST_CORRESPONDENCE.md`)
 - Elixir NIF build broken (low priority)
 - BEAM daemon not implemented (planned, not built)
 
@@ -111,7 +111,7 @@ deep-audit session). The corresponding Phase 4C design docs under
 ### Medium Priority
 
 1. Full POSIX compliance incomplete (see `docs/POSIX_COMPLIANCE.md`)
-2. No GDPR compliance (RMO/secure deletion are stubs)
+2. Partial GDPR/RMO: `obliterate` implemented (best-effort secure deletion + audit residue); full GDPR framework incomplete (HW erase for CoW/SSD, HMAC signing)
 3. Elixir NIF build broken (low priority)
 
 ### Low Priority
@@ -303,9 +303,18 @@ cargo run
 - Working in Rust CLI
 
 ### RMO (Remove-Match-Obliterate)
-- Irreversible deletion with proof of complete removal
-- Stubs only — NOT implemented
-- Needed for GDPR compliance
+- Irreversible deletion with proof of complete removal (model proven in
+  `proofs/coq/rmo_operations.v`: `obliterate_overwrites_all_blocks`,
+  `obliterate_not_injective`)
+- **Implemented and wired** in the CLI: `obliterate <file> [--force]` does a
+  3-pass overwrite (random/0x00/0xFF, fsync) + unlink, records an irreversible
+  `Obliterate` op, and appends an **audit residue** to `<root>/.vsh-audit.log`
+  (the MAA attestation that survives the deletion). Parser+executor →
+  `commands::secure_deletion::obliterate_path`. Tests:
+  `tests/obliterate_rmo_tests.rs`.
+- **Honest limits** (still not full GDPR): best-effort on in-place filesystems
+  only — CoW (btrfs/ZFS/APFS)/SSD FTL defeat overwrite (use `secure_erase` for
+  hardware NIST SP 800-88 Purge); audit-log HMAC signing is still a TODO.
 
 ## License
 

FAQ.adoc

@@ -97,8 +97,10 @@ What is **not** solid enough for production:
 
 * The link from the proven model to the Rust runtime is *property-tested*
   (~85% confidence), not *mechanically proven*. This is the v1.0.0 blocker.
-* RMO (secure deletion / GDPR) primitives are stubs in the runtime even where
-  the model is proved.
+* RMO (secure deletion / GDPR): the `obliterate` command is implemented and
+  wired (`obliterate <file> --force` → 3-pass overwrite + unlink + append-only
+  audit residue), but it is best-effort on in-place filesystems only (CoW/SSD
+  need hardware erase via `secure_erase`) and is not a complete GDPR framework.
 * POSIX coverage is a strict subset; word-splitting in external command args,
   full subshell `(...)` syntax, and `~user` tilde expansion are not implemented.
 

Justfile

@@ -43,6 +43,18 @@ build-lean4:
     cd proofs/lean4 && lean FileOperations.lean
     @echo "✓ Lean 4 proofs checked"
 
+# Build the executable model oracle (the compiled proven Lean model) used by the
+# differential correspondence test impl/rust-cli/tests/model_oracle_correspondence.rs
+build-model-oracle:
+    @echo "Building Lean model oracle..."
+    cd proofs/lean4 && lake build model_oracle
+    @echo "✓ model oracle -> proofs/lean4/.lake/build/bin/model_oracle"
+
+# Run the differential correspondence test (proven Lean model vs Rust impl).
+# Builds the oracle first so the test does not skip.
+test-correspondence-model: build-model-oracle
+    cd impl/rust-cli && cargo test --test model_oracle_correspondence -- --nocapture
+
 # Build Agda proofs
 build-agda:
     @echo "Building Agda proofs..."
@@ -126,13 +138,15 @@ test-cli:
     cd impl/rust-cli && cargo test
     @echo "✓ Rust CLI tests passed"
 
-# Launch the interactive vsh shell (the primary deliverable). Extra args pass
-# through to the binary:
+# Launch the interactive vsh shell via the E-Grade launcher (./launch.sh).
+# Extra args pass through to the binary:
 #   just run              # start the interactive REPL
 #   just run --version    # print version and exit
 #   just run script.vsh   # run a script
+# For the full launcher mode-set (--status/--integ/--disinteg/...), call
+# ./launch.sh directly. See docs/LAUNCHER.md.
 run *ARGS:
-    cd impl/rust-cli && cargo run -- {{ARGS}}
+    @"{{justfile_directory()}}/launch.sh" --auto -- {{ARGS}}
 
 # Build all FFI layers
 build-ffi: build-ffi-zig build-ffi-ocaml

QUICKSTART-USER.adoc

@@ -78,6 +78,22 @@ cargo build --release           # build the release binary
 ./target/release/vsh --version
 ----
 
+== Desktop integration (optional)
+
+`launch.sh` is the standard-conformant launcher (E-Grade Launcher Standard). It
+adds a desktop menu entry so you can start `vsh` from your application launcher:
+
+[source,bash]
+----
+./launch.sh --integ      # install a desktop entry (Linux; idempotent)
+./launch.sh --status     # show binary, version, platform
+./launch.sh --disinteg   # remove it again (keeps your config and logs)
+----
+
+`./launch.sh` with no arguments launches the shell (same as `just run`). See
+link:docs/LAUNCHER.md[docs/LAUNCHER.md] for the full mode set and conformance
+notes.
+
 == Run in a container
 
 [source,bash]

README.adoc

@@ -54,7 +54,7 @@ Valence Shell is a formally verified shell with proven reversibility guarantees.
 * [x] Here Documents: `<<DELIMITER`, `<←DELIMITER`, `<<<word`
 * [x] Job Control: Background jobs, `fg`, `bg`, `kill`, job specifications
 * [x] Shell Variables: `$VAR`, `export`, assignment, expansion
-* [ ] GDPR Compliance: Secure deletion (`obliterate`) + audit logging (stubs only)
+* [~] GDPR/RMO: `obliterate` secure deletion implemented + wired (3-pass overwrite + unlink + append-only audit residue); best-effort on in-place filesystems — CoW/SSD need hardware `secure_erase`, HMAC signing pending (not a full GDPR framework)
 * [x] Syntax Highlighting: Real-time color-coded REPL
 * [x] Command Correction: Intelligent typo suggestions
 * [x] Friendly Errors: fish-style helpful error messages

ROADMAP.adoc

@@ -112,8 +112,10 @@ Hard requirements before any v1.0 claim:
 * [ ] CRG v2.0 grade B: 6+ diverse external targets, issues fed back.
   See audit `=== External validation` section for the proposed diverse-6
   shape.
-* [ ] Complete RMO (Remove-Match-Obliterate) implementation for GDPR
-  compliance — currently stubs only. Tracked under #41.
+* [~] RMO (Remove-Match-Obliterate): file-level `obliterate` implemented and
+  wired (best-effort 3-pass overwrite + unlink + append-only audit residue).
+  Remaining for full GDPR: hardware erase for CoW/SSD, audit HMAC signing,
+  recursive-dir hardening. Tracked under #41.
 * [ ] Echidna integration for automated property-based verification.
 
 == v2.0 — Idris2 Extraction Path