hyperpolymath · hyperpolymath · Jul 17, 2026 · Jul 17, 2026 · Jul 17, 2026 · Jul 17, 2026
@@ -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"

@@ -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"

@@ -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",
 ]

@@ -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

@@ -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
 

@@ -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.
 

@@ -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

@@ -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]

@@ -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

@@ -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

@@ -72,7 +72,7 @@ FORMAL VERIFICATION
   Reversibility Proofs             ██████████ 100%    All 8 ops proven in all 6 systems
   Permission Proofs (chmod/chown)  ██████████ 100%    NEW — 42 theorems across 6 systems
   MAA Framework (RMR)              ██████████ 100%    Reversible ops with audit trails
-  MAA Framework (RMO)              ██░░░░░░░░  20%    Irreversibility proofs, stubs only
+  MAA Framework (RMO)              ████░░░░░░  40%    Proofs + wired `obliterate` (best-effort + audit residue); no HW erase/HMAC
   Extraction Gap (Lean → Rust)     ██████░░░░  60%    ~95% confidence via property testing
 
 IMPLEMENTATION LAYERS

@@ -30,7 +30,7 @@ Valence Shell supplies the shell operations; Echo Types supplies the language fo
 Valence Shell already has RMR and RMO vocabulary:
 
 * RMR: Remove-Match-Reverse, reversible transactions with undo/redo proof.
-* RMO: Remove-Match-Obliterate, irreversible deletion with proof of complete removal; currently stubs only.
+* RMO: Remove-Match-Obliterate, irreversible deletion with proof of complete removal. The `obliterate` command is implemented and wired (best-effort 3-pass overwrite + unlink + append-only audit residue); the full RMO/GDPR framework (hardware erase for CoW/SSD, audit HMAC signing) is incomplete.
 
 Without Echo Types, these can be misread as only implementation features. With Echo Types, they become cases in a broader theory of information change.
 
@@ -148,7 +148,7 @@ When working in Valence Shell, Claude and similar agents must observe these rule
 
 * Do not claim Valence Shell is production-ready.
 * Do not claim the Lean-to-Rust correspondence is mechanised.
-* Do not claim RMO/GDPR support exists beyond stubs.
+* Do not claim RMO/GDPR support beyond the implemented best-effort `obliterate` (in-place FS only; no hardware erase, no HMAC-signed audit) — i.e. do not claim a complete GDPR compliance framework.
 * Do not claim Echo Types proves Valence Shell implementation correctness.
 * Do not claim Ochrance cryptographic integrity while its hash/attestation gaps remain open.
 * Do not merge exploratory Echo bridges into core claims without checking `docs/bridge-status.md` in echo-types.