feat(rmo): wire obliterate into dispatch + audit residue (secure deletion)

claude · claude · commit 4883a4298624 · 2026-07-17T05:47:11.000Z
The obliterate secure-deletion command was fully implemented in commands/secure_deletion.rs but never wired into dispatch — no Command variant, no parser case, no executor arm — so it was unreachable dead code from the REPL/scripts. This binds the proven RMO model to a usable runtime. Wiring: - parser: Command::Obliterate { path, force, redirects } + "obliterate" case (--force/-f skips the confirmation guard). - executable: executor arm -> commands::secure_deletion::obliterate_path (routes file vs directory); proof_reference -> OBLITERATE_IRREVERSIBLE; description arm. - secure_deletion: obliterate_path dispatcher. Audit residue (MAA / GDPR Article 17 attestation): - obliterate/obliterate_dir append an append-only record to <sandbox-root>/.vsh-audit.log via AuditLog. The data is destroyed; the proof-of-deletion survives. Sandboxed under the shell root (testable, isolated). Tests: impl/rust-cli/tests/obliterate_rmo_tests.rs (6) — dispatch wiring, missing-operand error, end-to-end destruction, audit residue, irreversibility (undo cannot resurrect), no-old-plaintext-remains. Full suite green (317 lib + all integration); verified through the real vsh binary in script mode. Honest scope (docs reconciled from "RMO stubs only"): best-effort 3-pass overwrite (random/0x00/0xFF + fsync) on in-place filesystems only; CoW/SSD need hardware secure_erase; audit HMAC signing pending; NOT a complete GDPR framework. Updated CLAUDE.md, README, FAQ, ROADMAP(+_TO_V1), TOPOLOGY, docs/wiki/*, methodology.a2ml, and the ECHO-TYPES-OCHRANCE bridge (adoc + a2ml) in lock-step. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU
diff --git a/.machine_readable/ECHO_TYPES_OCHRANCE_BRIDGE.a2ml b/.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"
diff --git a/.machine_readable/bot_directives/methodology.a2ml b/.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",
 ]
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
@@ -19,6 +19,28 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 === 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`/
diff --git a/CLAUDE.md b/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
 
diff --git a/FAQ.adoc b/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.
 
diff --git a/README.adoc b/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
diff --git a/ROADMAP.adoc b/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
diff --git a/TOPOLOGY.md b/TOPOLOGY.md
@@ -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
diff --git a/docs/ECHO-TYPES-OCHRANCE-BRIDGE.adoc b/docs/ECHO-TYPES-OCHRANCE-BRIDGE.adoc
@@ -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.
diff --git a/docs/ROADMAP_TO_V1.md b/docs/ROADMAP_TO_V1.md
@@ -27,7 +27,7 @@ plan builds on.
 - Lean→Rust correspondence is **tested, not mechanized** (~85–95% confidence)
 - Not a full POSIX shell: word splitting in external args, `~user`,
   subshell `(...)`, SIGCHLD/Ctrl+Z incomplete (`docs/POSIX_COMPLIANCE.md`)
-- RMO/secure deletion are stubs; GDPR claims not yet shippable
+- RMO `obliterate` implemented + wired (best-effort overwrite + unlink + audit residue); full GDPR not yet shippable (HW erase for CoW/SSD, HMAC signing pending)
 - Backlog is decomposed fan-out-ready in Tier-S issues:
   #41→(#86,#87,#88) seams, #42→(#76–#81) proofs, #43→(#82–#85) tests,
   #45→(#63–#66, #90–#94) theory frontiers
diff --git a/docs/wiki/For-Marketers-and-Journalists.md b/docs/wiki/For-Marketers-and-Journalists.md
@@ -49,7 +49,7 @@ This is the heart of this page. Please read it before publishing.
 | "A shell with **formally proven** reversible operations." | "A **fully verified** shell." (The proof-to-code link isn't mechanically verified yet.) |
 | "Reversibility is **proven in the mathematical model**." | "Every line of the program is **proven correct**." |
 | "**Property-tested** correspondence between proofs and code (~85% confidence)." | "The Rust code is **proven** to match the proofs." (This is the explicit v1.0.0 blocker, not yet done.) |
-| "**Designed** for GDPR-style provable secure deletion." | "**GDPR-compliant** secure deletion." (RMO is a stub; not implemented.) |
+| "Has a **best-effort** secure-deletion command (`obliterate`) with an audit trail." | "**GDPR-compliant** secure deletion." (best-effort on in-place filesystems only; CoW/SSD need hardware erase; not a complete GDPR framework.) |
 | "An **advanced research prototype**." | "**Production-ready** / enterprise-ready / ready to ship." |
 | "Proven for its **modeled filesystem operations**." | "A **full POSIX / bash replacement**." (POSIX coverage is a subset.) |
 | "**Six proof systems** cross-validate the same theorems." | "**Impossible to have bugs.**" (Proofs cover the model, not the whole stack.) |
diff --git a/docs/wiki/For-Users.md b/docs/wiki/For-Users.md
@@ -70,8 +70,11 @@ and worked examples in
 - It is **not a full POSIX/bash replacement.** Word-splitting in external command
   arguments, full subshell `(...)` syntax, and `~user` tilde expansion are not
   implemented.
-- **Secure deletion / GDPR (`obliterate`)** is a stub — designed and proven in
-  the model, but not usable in the runtime.
+- **Secure deletion (`obliterate`)** is implemented: `obliterate <file> --force`
+  does a 3-pass overwrite (random/0x00/0xFF) + unlink and writes an append-only
+  audit record. It is **best-effort on in-place filesystems** (CoW like
+  btrfs/ZFS/APFS and SSDs need hardware erase) and is **not a full GDPR
+  framework** (audit HMAC signing still pending).
 - The proof-to-code correspondence is **property-tested (~85% confidence)**, not
   mechanically proven.
 
diff --git a/docs/wiki/Verification-Status.md b/docs/wiki/Verification-Status.md
@@ -70,9 +70,9 @@ The **Idris2 ABI layer is hole-free** (builds under `--total`, closed via issue
 |-----------|--------|
 | Reversible ops (**RMR**): undo/redo, checkpoint/restore, transactions | ✅ Working & proven |
 | Interactive shell surface (pipelines, redirs, glob, control structures, jobs, variables) | ✅ Working |
-| Secure deletion / GDPR (**RMO** / `obliterate`) | ❌ Proven in model, **stub in runtime** |
+| Secure deletion (**RMO** / `obliterate`) | ⚠️ Implemented & wired (3-pass overwrite + unlink + audit residue); best-effort on in-place FS only (CoW/SSD need HW erase); not a full GDPR framework |
 | Full POSIX compliance | ⚠️ Subset only (no external-arg word-splitting, subshells, `~user`) |
-| Mechanized Lean → Rust correspondence | ❌ Not done (v1.0.0 blocker) |
+| Mechanized Lean → Rust correspondence | ⚠️ Differential oracle vs compiled proven model (`just test-correspondence-model`); full refinement proof still the v1.0.0 blocker |
 
 ## Test posture
 
diff --git a/impl/rust-cli/src/commands/secure_deletion.rs b/impl/rust-cli/src/commands/secure_deletion.rs
@@ -41,6 +41,41 @@ use std::path::Path;
 
 use crate::state::{Operation, OperationType, ShellState};
 
+/// Dispatch `obliterate` to the file or directory variant by path type.
+/// This is the entry point wired into the shell parser/executor.
+pub fn obliterate_path(
+    state: &mut ShellState,
+    path: &str,
+    verbose: bool,
+    force: bool,
+) -> Result<()> {
+    if state.resolve_path(path).is_dir() {
+        obliterate_dir(state, path, verbose, force)
+    } else {
+        obliterate(state, path, verbose, force)
+    }
+}
+
+/// Append an RMO audit **residue**: the append-only proof that a compliant
+/// irreversible deletion occurred. The data is destroyed, but this record
+/// survives — the MAA (Mutually Assured Accountability) trail and the GDPR
+/// Article 17 attestation. Written within the shell's sandbox root
+/// (`<root>/.vsh-audit.log`) so it is session-isolated and testable.
+/// Best-effort: obliteration still succeeds if the residue cannot be written,
+/// but a warning is emitted so the failure is never silent.
+fn append_rmo_residue(state: &ShellState, op: &Operation, outcome: &str) {
+    let log_path = state.root.join(".vsh-audit.log");
+    match crate::audit_log::AuditLog::new(log_path, None) {
+        Ok(log) => {
+            let entry = crate::audit_log::AuditEntry::from_operation(op, outcome, None);
+            if let Err(e) = log.append(&entry) {
+                eprintln!("warning: RMO audit residue not written: {e}");
+            }
+        }
+        Err(e) => eprintln!("warning: RMO audit log unavailable: {e}"),
+    }
+}
+
 /// Simple yes/no confirmation prompt
 fn ask_confirmation(prompt: &str) -> Result<bool> {
     print!("{} [y/N] ", prompt);
@@ -279,6 +314,8 @@ pub fn obliterate(state: &mut ShellState, path: &str, verbose: bool, force: bool
     // Step 3: Record as irreversible operation (NO undo_data stored)
     let op = Operation::new(OperationType::Obliterate, path.to_string(), None);
     let op_id = op.id;
+    // RMO residue: persist the append-only attestation BEFORE moving `op`.
+    append_rmo_residue(state, &op, "obliterated");
     state.record_operation(op);
 
     // Output
@@ -412,6 +449,8 @@ pub fn obliterate_dir(
     // Record operation
     let op = Operation::new(OperationType::Obliterate, path.to_string(), None);
     let op_id = op.id;
+    // RMO residue: persist the append-only attestation BEFORE moving `op`.
+    append_rmo_residue(state, &op, "obliterated-dir");
     state.record_operation(op);
 
     println!(
diff --git a/impl/rust-cli/src/executable.rs b/impl/rust-cli/src/executable.rs
diff --git a/impl/rust-cli/src/parser.rs b/impl/rust-cli/src/parser.rs
diff --git a/impl/rust-cli/tests/obliterate_rmo_tests.rs b/impl/rust-cli/tests/obliterate_rmo_tests.rs

Original file line number	Diff line number	Diff line change
`@@ -101,7 +101,7 @@ constraints = [`
`101`	`101`	`"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",`
`102`	`102`	`"Agda has 1 structural axiom (funext) — provable in cubical Agda, intentional in intensional TT",`
`103`	`103`	`"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",`
`104`		`- "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",`
	`104`	`+ "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.",`
`105`	`105`	`"OCaml extraction path exists in proofs/coq/extraction.v but the extracted code is not wired into a build target",`
`106`	`106`	`"Idris2 ABI carrier has 2 holes + 10 partial markers per the 2026-06-01 deep audit (issue #42) — these are the FFI boundary obligations",`
`107`	`107`	`]`