diff --git a/.github/workflows/lean-verification.yml b/.github/workflows/lean-verification.yml index 7872dd75..b4ff293e 100644 --- a/.github/workflows/lean-verification.yml +++ b/.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" diff --git a/.machine_readable/ECHO_TYPES_OCHRANCE_BRIDGE.a2ml b/.machine_readable/ECHO_TYPES_OCHRANCE_BRIDGE.a2ml index d7f813c7..b906f3a7 100644 --- 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 index 3004b0b7..2c767d38 100644 --- 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 /.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 index af92a875..ca63b0c1 100644 --- a/CHANGELOG.adoc +++ b/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 + `/.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 () []` 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 diff --git a/CLAUDE.md b/CLAUDE.md index 1d82708a..a46d17ee 100644 --- 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 [--force]` does a + 3-pass overwrite (random/0x00/0xFF, fsync) + unlink, records an irreversible + `Obliterate` op, and appends an **audit residue** to `/.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 index b2f18287..1a6e7038 100644 --- 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 --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/Justfile b/Justfile index a9a131a7..de2799f4 100644 --- a/Justfile +++ b/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 diff --git a/QUICKSTART-USER.adoc b/QUICKSTART-USER.adoc index 6d1e93d8..326e7889 100644 --- a/QUICKSTART-USER.adoc +++ b/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] diff --git a/README.adoc b/README.adoc index 9c05782d..2aeb19de 100644 --- a/README.adoc +++ b/README.adoc @@ -54,7 +54,7 @@ Valence Shell is a formally verified shell with proven reversibility guarantees. * [x] Here Documents: `< +--> +# Launcher — `launch.sh` (E-Grade Launcher Standard) + +`launch.sh` at the repository root is the single, self-documenting entry point +for running and integrating `vsh`. It conforms to the Hyperpolymath +**E-Grade Launcher Standard** (`hyperpolymath/standards`, +`docs/UX-standards/launcher-standard.adoc` + `launcher/launcher-standard.a2ml`). + +```bash +./launch.sh # launch the interactive shell (default --auto) +./launch.sh --version # vsh 0.9.0 () [linux-x86_64] +./launch.sh --help # full usage +./launch.sh --status # binary, version, platform, daemon state +./launch.sh --integ # install desktop integration (Linux first-class) +./launch.sh --disinteg # remove integration (keeps config + logs) +``` + +`just run` / `just launch` delegate to `./launch.sh --auto`. + +## Modes + +| Mode | Behavior | +|------|----------| +| `--auto` (default) | Build if needed, then launch the interactive shell. | +| `--start` | Alias of `--auto` for a foreground shell (daemon phase deferred). | +| `--stop` | Stop a running daemon if one exists; otherwise a friendly no-op. | +| `--status` | Report binary path, version, platform, and daemon state. | +| `--browser` / `--web` | Aliases of `--auto` (no web endpoint; opens the shell). | +| `--integ` | Install desktop integration; idempotent (`--integ --force` reinstalls). | +| `--disinteg` | Remove integration, preserving `~/.config/vsh` and state/logs. | +| `--help` / `-h` | Usage, modes, file paths, detected platform. | +| `--version` / `-V` | `vsh () []`, exit 0. | + +Arguments after the mode pass through to `vsh` +(`./launch.sh --auto -- path/to/script.vsh`). + +## Files + +| Path | Role | +|------|------| +| `${XDG_STATE_HOME:-$HOME/.local/state}/vsh/server.log` | Log (never `/tmp`) | +| `${XDG_RUNTIME_DIR:-$TMPDIR:-/tmp}/vsh-server.pid` | PID file (deferred daemon phase) | +| `~/.local/share/applications/vsh.desktop` | Desktop entry (0444, `Terminal=true`) | +| `~/.local/bin/vsh-launcher` | Copied launcher (copy, not symlink) | + +## Conformance & honest deferrals + +`vsh` is a **foreground terminal shell with no HTTP server or daemon**. The +E-Grade standard is written primarily for web/GUI apps, so a subset of its MUST +clauses do not apply here. Rather than silently skip them, the launcher declares +them **deferred** in its `a2ml-metadata-block` header (`lifecycle-phases-deferred`): + +| Standard clause | Status | Rationale | +|-----------------|--------|-----------| +| Universal modes (`--start/--stop/--status/--auto/--browser/--web/--help/--version/--integ/--disinteg`) | ✅ Covered | Implemented and tested. | +| `--version` format ` () []` | ✅ Covered | Verified exact match. | +| Desktop integration (idempotent, copy-not-symlink, `Terminal=true`, 0444, config/log-preserving `--disinteg`) | ✅ Covered (Linux) | macOS/Windows are best-effort/deferred. | +| `err()`/`log()`, stderr-always, GUI-error + soft-attach via the resolution ladder (graceful no-op if absent) | ✅ Covered | Degrades cleanly when desktop-tools not installed. | +| PID file / logs in XDG dirs (never `/tmp`) | ✅ Covered | Paths wired; used when a daemon exists. | +| `nohup` background server, `wait_for_server()` URL polling, browser launch | ⏸️ **Deferred** | No server/URL — the BEAM daemon is designed but not implemented. `--auto` runs the shell in the terminal, not a browser. | + +When the BEAM daemon lands, the deferred server phases (nohup start, URL +readiness, browser open) can be enabled without changing the mode surface. + +## Testing + +The mode surface is verified manually per change: + +```bash +./launch.sh --version # exact format, exit 0 +./launch.sh --status # reports state +./launch.sh --integ # installs; second run is idempotent +./launch.sh --disinteg # removes; second run is a no-op +./launch.sh --auto -- --version # passthrough to vsh +``` diff --git a/docs/LEAN4_RUST_CORRESPONDENCE.md b/docs/LEAN4_RUST_CORRESPONDENCE.md index 62695e29..87b1db1c 100644 --- a/docs/LEAN4_RUST_CORRESPONDENCE.md +++ b/docs/LEAN4_RUST_CORRESPONDENCE.md @@ -36,12 +36,74 @@ This document establishes the **correspondence** between: └──────────────────────────────┘ ``` -**Verification Strategy**: +**Verification Strategy** (weakest → strongest): - **Manual proofs**: Argue why Rust code matches Lean 4 spec -- **Integration tests**: Validate behavior (28/28 passing) -- **Echidna**: Property-based testing (planned) +- **Integration tests**: Validate behavior +- **Property tests**: Hand-transcribed reversibility laws checked generatively +- **Mechanized differential oracle** *(new, 2026-07-17)*: the **compiled proven + Lean model** is executed as the test oracle — see below. - **Code review**: Multiple reviewers check correspondence +## Mechanized differential correspondence (model-as-oracle) + +`proofs/lean4/ModelOracle.lean` compiles the **exact** proven model definitions +(`mkdir`, `rmdir`, `createFile`, `deleteFile`, `fsUpdate` from `FilesystemModel` ++ `FileOperations`) into a standalone executable. Given an operation sequence and +a set of probe paths, it reports the node type (`DIR`/`FILE`/`NONE`) the *model* +computes at each path. + +`impl/rust-cli/tests/model_oracle_correspondence.rs` then: + +1. generates **precondition-respecting** operation sequences (the regime where the + reversibility theorems hold — a shadow tracker guarantees every op is valid); +2. applies each sequence to the real Rust `ShellState` (a sandboxed temp dir); +3. runs the same sequence through the compiled Lean model oracle; +4. asserts the model and the implementation agree at **every** touched path. + +This is stronger than the property tests: the oracle is the **proof artifact +itself**, not a hand-written re-statement of the laws. A divergence is a genuine +model↔implementation mismatch. Current status: **1218 probes agree across 200 +sequences** (`just test-correspondence-model`). + +```mermaid +flowchart LR + G[precondition-respecting
op sequence] --> R[Rust ShellState
real temp dir] + G --> O[compiled Lean model
ModelOracle] + R --> C{agree at
every probe?} + O --> C + C -->|yes| P[pass] + C -->|no| D[correspondence
divergence] +``` + +### What this does and does not establish + +- ✅ It executes the **proven** model (not a paraphrase) as the reference. +- ✅ It is reproducible and CI-gatable (`just build-model-oracle`). +- ⚠️ It is still **differential testing**, not a mechanized *refinement proof*. + Full mechanization (a machine-checked proof that the Rust semantics refine the + model) remains the v1.0 blocker. + +### Why not extraction-based (Coq → OCaml)? + +The Coq model extracts (`proofs/coq/extraction.v`) but is **not executable**: the +filesystem is modelled as a total function `Path → option FSNode` over an infinite +domain, and `is_empty_dir_dec` pulls in classical axioms +(`constructive_indefinite_description`, `excluded_middle_informative`) that the +extracted OCaml leaves unrealized. Making the *Coq* model executable requires +migrating the representation to a finite map (`FMaps.t FSNode`) and re-proving the +theorems over it — the same migration the proof-holes audit already recommends. +The Lean model sidesteps this because its operations are ordinary computable +`def`s that can be evaluated at any finite probe path, even though the state is +also a function. + +### Roadmap to full mechanization + +1. **(done)** Compiled-model differential oracle (this section). +2. Migrate the Coq filesystem model to `FMaps.t FSNode`; re-prove; extract an + executable OCaml oracle and cross-check it against the Lean oracle. +3. Model the Rust operational semantics (or a shared IR) and prove refinement — + the machine-checked correspondence that closes the v1.0 gap. + --- ## Filesystem Model Correspondence diff --git a/docs/ROADMAP_TO_V1.md b/docs/ROADMAP_TO_V1.md index 921ec02b..981c5e85 100644 --- 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 index 6f83ecaa..ff68b6aa 100644 --- 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 index 0857dbd1..5f11095e 100644 --- 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 --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 index 6801504b..0ccdc90c 100644 --- 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.rs b/impl/rust-cli/src/commands.rs index c1e22c49..1f42fafe 100644 --- a/impl/rust-cli/src/commands.rs +++ b/impl/rust-cli/src/commands.rs @@ -2233,8 +2233,7 @@ pub fn explain_command(cmd: &crate::parser::Command, state: &ShellState) -> Resu resolved.display() ); } - crate::parser::Command::Chmod { path: _, .. } - | crate::parser::Command::Chown { path: _, .. } => { + crate::parser::Command::Chmod { .. } | crate::parser::Command::Chown { .. } => { // Outer arm guarantees we are in {Chmod, Chown}; the inner match // exists only to extract the `path` field uniformly. Any other // variant here is a structural bug, surfaced as typed error. diff --git a/impl/rust-cli/src/commands/secure_deletion.rs b/impl/rust-cli/src/commands/secure_deletion.rs index 54b0d268..b28d9098 100644 --- 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 +/// (`/.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 { 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 index 28716ded..03cd202b 100644 --- a/impl/rust-cli/src/executable.rs +++ b/impl/rust-cli/src/executable.rs @@ -122,6 +122,27 @@ impl ExecutableCommand for Command { Ok(ExecutionResult::Success) } + Command::Obliterate { + path, + force, + redirects, + } => { + let expanded_path = crate::parser::expand_variables(path, state); + if redirects.is_empty() { + commands::secure_deletion::obliterate_path( + state, + &expanded_path, + false, + *force, + )?; + } else { + redirection::capture_and_redirect(redirects, state, |s| { + commands::secure_deletion::obliterate_path(s, &expanded_path, false, *force) + })?; + } + Ok(ExecutionResult::Success) + } + Command::Cp { src, dst, @@ -1220,7 +1241,8 @@ impl ExecutableCommand for Command { fn proof_reference(&self) -> Option { use crate::proof_refs::{ CHMOD_REVERSIBLE, CHOWN_REVERSIBLE, COPY_FILE_REVERSIBLE, CREATE_DELETE_REVERSIBLE, - MKDIR_RMDIR_REVERSIBLE, MOVE_REVERSIBLE, SYMLINK_UNLINK_REVERSIBLE, + MKDIR_RMDIR_REVERSIBLE, MOVE_REVERSIBLE, OBLITERATE_IRREVERSIBLE, + SYMLINK_UNLINK_REVERSIBLE, }; match self { @@ -1231,6 +1253,8 @@ impl ExecutableCommand for Command { Command::Ln { .. } => Some(SYMLINK_UNLINK_REVERSIBLE), Command::Chmod { .. } => Some(CHMOD_REVERSIBLE), Command::Chown { .. } => Some(CHOWN_REVERSIBLE), + // RMO: irreversible by design — the proof is of information loss. + Command::Obliterate { .. } => Some(OBLITERATE_IRREVERSIBLE), _ => None, } } @@ -1241,6 +1265,13 @@ impl ExecutableCommand for Command { Command::Rmdir { path, .. } => format!("rmdir {}", path), Command::Touch { path, .. } => format!("touch {}", path), Command::Rm { path, .. } => format!("rm {}", path), + Command::Obliterate { path, force, .. } => { + if *force { + format!("obliterate --force {}", path) + } else { + format!("obliterate {}", path) + } + } Command::Cp { src, dst, .. } => format!("cp {} {}", src, dst), Command::Mv { src, dst, .. } => format!("mv {} {}", src, dst), Command::Ln { target, link, .. } => format!("ln -s {} {}", target, link), diff --git a/impl/rust-cli/src/parser.rs b/impl/rust-cli/src/parser.rs index 3695a2cd..467ab0a4 100644 --- a/impl/rust-cli/src/parser.rs +++ b/impl/rust-cli/src/parser.rs @@ -210,6 +210,14 @@ pub enum Command { path: String, redirects: Vec, }, + /// Securely obliterate a file/dir (RMO — irreversible; multi-pass overwrite + + /// unlink + audit residue). Proven in `proofs/coq/rmo_operations.v` + /// (`obliterate_overwrites_all_blocks`, `obliterate_not_injective`). + Obliterate { + path: String, + force: bool, + redirects: Vec, + }, /// Copy file (reversible — proven in CopyMoveOperations.lean) Cp { src: String, @@ -2256,10 +2264,9 @@ fn apply_expansion(expansion: &ParameterExpansion, state: &crate::state::ShellSt // TODO: Assignment not implemented - requires mutable state // For v1.1.0, just return default without assigning (like Default) if is_unset || (*check_null && is_null) { - let default_expanded = expand_variables(value, state); - // Note: In bash, this would also assign to VAR + // Note: In bash, this would also assign to VAR. // Requires signature change: &mut ShellState - default_expanded + expand_variables(value, state) } else { // var_value is Some by construction here: the surrounding // `if is_unset || ...` branch is the unset/null path; this @@ -3289,6 +3296,19 @@ fn parse_base_command( redirects, }) } + "obliterate" => { + // GDPR-style secure deletion. `--force`/`-f` skips confirmation. + let force = args.iter().any(|a| a == "--force" || a == "-f"); + let path = args.iter().find(|a| !a.starts_with('-')).cloned(); + match path { + Some(path) => Ok(Command::Obliterate { + path, + force, + redirects, + }), + None => Err(anyhow!("obliterate: missing operand")), + } + } "cp" => { if args.len() < 2 { return Err(anyhow!("cp: missing destination operand")); @@ -4325,7 +4345,7 @@ mod tests { // Test using $1 in a command let cmd = parse_command("touch $1").unwrap(); match cmd { - Command::External { args: _, .. } | Command::Touch { path: _, .. } => { + Command::External { .. } | Command::Touch { .. } => { // After parsing, before execution, $1 should still be present // Expansion happens during execution } diff --git a/impl/rust-cli/tests/model_oracle_correspondence.rs b/impl/rust-cli/tests/model_oracle_correspondence.rs new file mode 100644 index 00000000..f448c8a5 --- /dev/null +++ b/impl/rust-cli/tests/model_oracle_correspondence.rs @@ -0,0 +1,316 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell +//! Differential correspondence: Rust implementation vs. the *proven Lean model*. +//! +//! Unlike the property tests (which check hand-transcribed laws), this test uses +//! the COMPILED Lean model as the oracle. `proofs/lean4/ModelOracle.lean` drives +//! the exact `mkdir`/`rmdir`/`createFile`/`deleteFile`/`fsUpdate` definitions that +//! the correspondence theorems are proven about, and reports the node type at a +//! set of probe paths. We generate precondition-respecting operation sequences +//! (the regime where the reversibility theorems hold), apply them to the real +//! Rust `ShellState`, run the same sequence through the Lean oracle, and assert +//! that the model and the implementation agree at every touched path. +//! +//! Any disagreement is a genuine correspondence divergence between the proven +//! model and the runtime — the thing a mechanized correspondence is meant to catch. +//! +//! Gating: if the oracle binary is not built, the test SKIPS (prints how to build +//! it) rather than failing, so `cargo test` stays green without a Lean toolchain. +//! Build it with: cd proofs/lean4 && lake build model_oracle +//! or: just build-model-oracle + +use std::collections::BTreeMap; +use std::io::Write; +use std::path::PathBuf; +use std::process::{Command, Stdio}; + +use tempfile::TempDir; +use vsh::commands::{mkdir, rm, rmdir, touch}; +use vsh::state::ShellState; + +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +enum Kind { + Dir, + File, +} + +/// Deterministic LCG so the corpus is reproducible (no external rand dependency, +/// and Miri/CI get identical sequences run-to-run). +struct Rng(u64); +impl Rng { + fn new(seed: u64) -> Self { + Rng(seed ^ 0x9E37_79B9_7F4A_7C15) + } + fn next_u64(&mut self) -> u64 { + self.0 = self + .0 + .wrapping_mul(6364136223846793005) + .wrapping_add(1442695040888963407); + self.0 + } + fn below(&mut self, n: usize) -> usize { + if n == 0 { + 0 + } else { + ((self.next_u64() >> 33) as usize) % n + } + } +} + +/// Locate the compiled Lean model oracle. Env override wins; otherwise the +/// default lake build path relative to this crate. +fn locate_oracle() -> Option { + if let Ok(p) = std::env::var("VSH_MODEL_ORACLE") { + let pb = PathBuf::from(p); + if pb.is_file() { + return Some(pb); + } + } + // impl/rust-cli/tests -> repo root -> proofs/lean4/.lake/build/bin/model_oracle + let manifest = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + let candidate = manifest + .join("../../proofs/lean4/.lake/build/bin/model_oracle") + .canonicalize() + .ok()?; + if candidate.is_file() { + Some(candidate) + } else { + None + } +} + +/// One generated operation. +#[derive(Clone)] +struct Op { + verb: &'static str, // MKDIR / RMDIR / TOUCH / RM + path: String, +} + +/// Generate a precondition-respecting sequence, maintaining a shadow of the +/// expected state so every emitted op is valid under real-filesystem rules. +fn gen_sequence(rng: &mut Rng, max_ops: usize) -> (Vec, Vec) { + let mut shadow: BTreeMap = BTreeMap::new(); + let mut ops: Vec = Vec::new(); + let mut touched: BTreeMap = BTreeMap::new(); + let mut counter = 0usize; + + let dirs = |shadow: &BTreeMap| -> Vec { + let mut v = vec![String::new()]; // root + v.extend( + shadow + .iter() + .filter(|(_, k)| **k == Kind::Dir) + .map(|(p, _)| p.clone()), + ); + v + }; + let is_empty_dir = |shadow: &BTreeMap, p: &str| -> bool { + let prefix = format!("{p}/"); + !shadow.keys().any(|k| k.starts_with(&prefix)) + }; + let child = |parent: &str, name: &str| -> String { + if parent.is_empty() { + name.to_string() + } else { + format!("{parent}/{name}") + } + }; + + let n = 1 + rng.below(max_ops); + for _ in 0..n { + // Weighted choice biased toward creation, with valid removals when possible. + let roll = rng.below(10); + if roll < 5 { + // MKDIR under an existing directory + let ds = dirs(&shadow); + let parent = ds[rng.below(ds.len())].clone(); + counter += 1; + let p = child(&parent, &format!("d{counter}")); + if shadow.contains_key(&p) { + continue; + } + shadow.insert(p.clone(), Kind::Dir); + touched.insert(p.clone(), ()); + ops.push(Op { + verb: "MKDIR", + path: p, + }); + } else if roll < 8 { + // TOUCH under an existing directory + let ds = dirs(&shadow); + let parent = ds[rng.below(ds.len())].clone(); + counter += 1; + let p = child(&parent, &format!("f{counter}.txt")); + if shadow.contains_key(&p) { + continue; + } + shadow.insert(p.clone(), Kind::File); + touched.insert(p.clone(), ()); + ops.push(Op { + verb: "TOUCH", + path: p, + }); + } else if roll < 9 { + // RM an existing file + let files: Vec = shadow + .iter() + .filter(|(_, k)| **k == Kind::File) + .map(|(p, _)| p.clone()) + .collect(); + if files.is_empty() { + continue; + } + let p = files[rng.below(files.len())].clone(); + shadow.remove(&p); + touched.insert(p.clone(), ()); + ops.push(Op { + verb: "RM", + path: p, + }); + } else { + // RMDIR an empty directory + let empties: Vec = shadow + .iter() + .filter(|(p, k)| **k == Kind::Dir && is_empty_dir(&shadow, p)) + .map(|(p, _)| p.clone()) + .collect(); + if empties.is_empty() { + continue; + } + let p = empties[rng.below(empties.len())].clone(); + shadow.remove(&p); + touched.insert(p.clone(), ()); + ops.push(Op { + verb: "RMDIR", + path: p, + }); + } + } + + (ops, touched.into_keys().collect()) +} + +/// Ask the Lean model oracle for the node type at each probe path. +fn oracle_query(oracle: &PathBuf, ops: &[Op], probes: &[String]) -> Vec { + let mut input = String::new(); + for op in ops { + input.push_str(op.verb); + input.push(' '); + input.push_str(&op.path); + input.push('\n'); + } + input.push_str("---\n"); + for p in probes { + input.push_str(p); + input.push('\n'); + } + + let mut child = Command::new(oracle) + .stdin(Stdio::piped()) + .stdout(Stdio::piped()) + .spawn() + .expect("spawn model oracle"); + child + .stdin + .take() + .expect("oracle stdin") + .write_all(input.as_bytes()) + .expect("write to oracle"); + let out = child.wait_with_output().expect("oracle output"); + assert!(out.status.success(), "oracle exited non-zero"); + String::from_utf8(out.stdout) + .expect("oracle utf8") + .lines() + .map(|l| l.trim().to_string()) + .filter(|l| !l.is_empty()) + .collect() +} + +/// The real Rust implementation's node type at a probe path (under the sandbox). +fn rust_kind(root: &std::path::Path, rel: &str) -> &'static str { + match std::fs::symlink_metadata(root.join(rel)) { + Ok(m) if m.is_dir() => "DIR", + Ok(m) if m.is_file() => "FILE", + Ok(_) => "OTHER", + Err(_) => "NONE", + } +} + +#[test] +fn rust_matches_proven_lean_model() { + let Some(oracle) = locate_oracle() else { + eprintln!( + "SKIP model_oracle_correspondence: Lean model oracle not built.\n\ + Build it with: cd proofs/lean4 && lake build model_oracle\n\ + or: just build-model-oracle\n\ + or set VSH_MODEL_ORACLE=/path/to/model_oracle" + ); + return; + }; + + const SEQUENCES: usize = 200; + const MAX_OPS: usize = 14; + let mut rng = Rng::new(20260717u64); + let mut checked_probes = 0usize; + + for seq in 0..SEQUENCES { + let (ops, probes) = gen_sequence(&mut rng, MAX_OPS); + if probes.is_empty() { + continue; + } + + // Apply the sequence to the real Rust implementation in a fresh sandbox. + let temp = TempDir::new().expect("tempdir"); + let mut state = + ShellState::new(temp.path().to_str().expect("utf8 path")).expect("shell state"); + for op in &ops { + let r = match op.verb { + "MKDIR" => mkdir(&mut state, &op.path, false), + "RMDIR" => rmdir(&mut state, &op.path, false), + "TOUCH" => touch(&mut state, &op.path, false), + "RM" => rm(&mut state, &op.path, false), + _ => unreachable!(), + }; + r.unwrap_or_else(|e| { + panic!( + "seq {seq}: generated op {} {} rejected by impl: {e}", + op.verb, op.path + ) + }); + } + + // Ask the proven model for the same probes. + let model = oracle_query(&oracle, &ops, &probes); + assert_eq!( + model.len(), + probes.len(), + "seq {seq}: oracle returned {} answers for {} probes", + model.len(), + probes.len() + ); + + // Differential assertion: model vs. real implementation at every probe. + for (probe, model_kind) in probes.iter().zip(model.iter()) { + let impl_kind = rust_kind(temp.path(), probe); + assert_eq!( + model_kind, + impl_kind, + "CORRESPONDENCE DIVERGENCE (seq {seq}) at '{probe}': \ + proven Lean model says {model_kind}, Rust impl says {impl_kind}.\n\ + ops: {:?}", + ops.iter() + .map(|o| format!("{} {}", o.verb, o.path)) + .collect::>() + ); + checked_probes += 1; + } + } + + assert!( + checked_probes > 0, + "no probes were checked — generator produced only empty sequences" + ); + eprintln!( + "model_oracle_correspondence: {checked_probes} probes agreed across {SEQUENCES} sequences" + ); +} diff --git a/impl/rust-cli/tests/obliterate_rmo_tests.rs b/impl/rust-cli/tests/obliterate_rmo_tests.rs new file mode 100644 index 00000000..64f9e32d --- /dev/null +++ b/impl/rust-cli/tests/obliterate_rmo_tests.rs @@ -0,0 +1,143 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell +//! End-to-end RMO (Remove-Match-Obliterate) tests. +//! +//! These exercise the `obliterate` command through the real parse -> execute +//! pipeline, verifying that the previously-unreachable secure-deletion command +//! is now wired into dispatch, destroys data, leaves a persistent audit residue +//! (the MAA / GDPR Article 17 attestation), and is irreversible. + +use std::fs; + +use tempfile::TempDir; +use vsh::executable::ExecutableCommand; +use vsh::parser::{parse_command, Command}; +use vsh::state::ShellState; + +fn setup() -> (TempDir, ShellState) { + let temp = TempDir::new().expect("tempdir"); + let state = ShellState::new(temp.path().to_str().expect("utf8")).expect("state"); + (temp, state) +} + +/// The core fix: `obliterate` must PARSE to `Command::Obliterate`. Before wiring +/// it fell through to external-command handling and was unreachable from the REPL. +#[test] +fn obliterate_is_wired_into_dispatch() { + match parse_command("obliterate secret.txt").expect("parse") { + Command::Obliterate { path, force, .. } => { + assert_eq!(path, "secret.txt"); + assert!(!force, "no --force means force=false"); + } + other => panic!("expected Command::Obliterate, got {other:?}"), + } + + // --force before or after the path both work. + for input in [ + "obliterate --force secret.txt", + "obliterate secret.txt --force", + ] { + match parse_command(input).expect("parse") { + Command::Obliterate { path, force, .. } => { + assert_eq!(path, "secret.txt", "input: {input}"); + assert!(force, "input: {input}"); + } + other => panic!("expected Command::Obliterate for {input:?}, got {other:?}"), + } + } +} + +/// obliterate with no operand is a clean error, not a panic. +#[test] +fn obliterate_requires_operand() { + assert!(parse_command("obliterate").is_err()); + assert!(parse_command("obliterate --force").is_err()); +} + +/// End-to-end: parse + execute actually destroys the file. +#[test] +fn obliterate_destroys_file_end_to_end() { + let (temp, mut state) = setup(); + let secret = temp.path().join("secret.txt"); + fs::write(&secret, b"TOP SECRET PERSONAL DATA").expect("write"); + assert!(secret.exists()); + + parse_command("obliterate secret.txt --force") + .expect("parse") + .execute(&mut state) + .expect("execute"); + + assert!(!secret.exists(), "obliterated file must not exist"); +} + +/// The RMO residue: an append-only audit record survives the data destruction. +#[test] +fn obliterate_writes_rmo_audit_residue() { + let (temp, mut state) = setup(); + fs::write(temp.path().join("pii.txt"), b"name,email\nalice,a@x\n").expect("write"); + + parse_command("obliterate pii.txt --force") + .expect("parse") + .execute(&mut state) + .expect("execute"); + + let audit = temp.path().join(".vsh-audit.log"); + assert!( + audit.exists(), + "RMO audit residue must be written to the sandbox" + ); + let contents = fs::read_to_string(&audit).expect("read audit"); + assert!( + contents.contains("Obliterate"), + "audit must record the Obliterate operation type; got: {contents}" + ); + assert!( + contents.contains("pii.txt"), + "audit must record the obliterated path; got: {contents}" + ); +} + +/// RMO is irreversible: undo must not resurrect an obliterated file. +#[test] +fn obliterate_is_irreversible() { + let (temp, mut state) = setup(); + let victim = temp.path().join("gone.txt"); + fs::write(&victim, b"data").expect("write"); + + parse_command("obliterate gone.txt --force") + .expect("parse") + .execute(&mut state) + .expect("execute"); + assert!(!victim.exists()); + + // Undo may report nothing-to-do or an error, but must never restore the file. + let _ = vsh::commands::undo(&mut state, 1, false); + assert!( + !victim.exists(), + "undo must not resurrect an obliterated file (RMO is irreversible)" + ); +} + +/// The overwrite actually changes bytes before unlink: obliterate a file, then +/// confirm no plaintext survives at the path (it is gone) — and that a fresh file +/// of the same name created afterward does not contain the old content. +#[test] +fn obliterate_then_recreate_has_no_old_content() { + let (temp, mut state) = setup(); + let p = temp.path().join("card.txt"); + fs::write(&p, b"4111111111111111").expect("write"); + + parse_command("obliterate card.txt --force") + .expect("parse") + .execute(&mut state) + .expect("execute"); + assert!(!p.exists()); + + fs::write(&p, b"fresh").expect("rewrite"); + let back = fs::read(&p).expect("read"); + assert_eq!(back, b"fresh"); + assert!( + !back.windows(4).any(|w| w == b"4111"), + "no old plaintext remains" + ); +} diff --git a/launch.sh b/launch.sh new file mode 100755 index 00000000..41df974c --- /dev/null +++ b/launch.sh @@ -0,0 +1,296 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) Jonathan D.A. Jewell +# +# ┌─ a2ml-metadata-block ────────────────────────────────────────────────────── +# id: valence-shell.launcher +# type: launcher +# version: 0.9.0 +# app-name: vsh +# app-display: Valence Shell +# app-url: "" # foreground terminal shell — no web endpoint +# standards-compliance: +# - launcher-standard.adoc (hyperpolymath/standards, E-Grade Launcher Standard) +# - LM-LA-LIFECYCLE-STANDARD.adoc +# - cross-platform-system-integration-modes +# - fallback-ladder-keepopen +# modes: [--auto, --start, --stop, --status, --browser, --web, --integ, --disinteg, --help, --version] +# platforms: [linux, macos, windows] +# lifecycle-phases-covered: +# - run/auto (launch the interactive shell) +# - status +# - help / version +# - system-integration (--integ / --disinteg; Linux first-class, macOS/Windows best-effort) +# lifecycle-phases-deferred: +# # vsh is a FOREGROUND terminal shell with no HTTP server or daemon, so the +# # server-oriented clauses of the standard do not apply and are declared +# # deferred (not silently skipped): +# - background-server (nohup daemon) # BEAM daemon designed, not implemented +# - url-readiness-polling (wait_for_server / curl) +# - browser-launch (--auto opens the shell in the terminal, not a browser) +# └──────────────────────────────────────────────────────────────────────────── +# +# E-Grade principle: one script to remember, one unified entry point for run, +# status, and system integration, self-documenting via --help / --version. + +set -euo pipefail + +# ── Standard variables ─────────────────────────────────────────────────────── +APP_NAME="vsh" +APP_DISPLAY="Valence Shell" +REPO_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +VERSION="$(grep -m1 '^version' "$REPO_DIR/impl/rust-cli/Cargo.toml" 2>/dev/null | sed -E 's/.*"([^"]+)".*/\1/')" +VERSION="${VERSION:-0.9.0}" +PID_FILE="${XDG_RUNTIME_DIR:-${TMPDIR:-/tmp}}/${APP_NAME}-server.pid" +LOG_DIR="${XDG_STATE_HOME:-$HOME/.local/state}/${APP_NAME}" +LOG_FILE="${LOG_DIR}/server.log" +MODE="${1:---auto}" + +# ── Feedback helpers ───────────────────────────────────────────────────────── +log() { printf '%s\n' "$*"; } +err() { printf '%s: %s\n' "$APP_NAME" "$*" >&2; } + +platform() { printf '%s-%s' "$(uname -s | tr '[:upper:]' '[:lower:]')" "$(uname -m)"; } + +build_sha() { + git -C "$REPO_DIR" rev-parse --short HEAD 2>/dev/null || printf 'unknown' +} + +# ── Desktop-tools resolution ladder (graceful degradation) ─────────────────── +# Source keepopen.sh / soft-attach.sh / gui-error.sh from the published ladder +# if present; otherwise install no-op shims so the launcher still works when the +# hyperpolymath desktop-tools are not installed (e.g. a fresh clone). +resolve_desktop_tools() { + local candidates=( + "${HP_DESKTOP_TOOLS:-}" + "${HP_ESTATE_ROOT:-}/.desktop-tools" + "${XDG_DATA_HOME:-$HOME/.local/share}/hyperpolymath/.desktop-tools" + "$HOME/developer/repos/.desktop-tools" + "$HOME/dev/repos/.desktop-tools" + ) + local d + for d in "${candidates[@]}"; do + [ -n "$d" ] && [ -d "$d" ] || continue + # shellcheck source=/dev/null + [ -f "$d/gui-error.sh" ] && . "$d/gui-error.sh" || true + # shellcheck source=/dev/null + [ -f "$d/soft-attach.sh" ] && . "$d/soft-attach.sh" || true + DESKTOP_TOOLS_DIR="$d" + return 0 + done + DESKTOP_TOOLS_DIR="" + return 0 +} + +# Surface an error via GUI dialog (if the helper resolved) AND always to stderr. +gui_err() { + err "$*" + if command -v hp_gui_error >/dev/null 2>&1; then + hp_gui_error "$APP_DISPLAY" "$*" || true + fi +} + +# Optional soft-attach hook on failure (no-op if tool absent). +on_start_failed() { + if command -v hp_soft_attach_event >/dev/null 2>&1; then + hp_soft_attach_event "$APP_NAME" "start-failed" "$LOG_FILE" || true + fi +} + +# ── vsh resolution ─────────────────────────────────────────────────────────── +resolve_bin() { + if command -v "$APP_NAME" >/dev/null 2>&1; then + command -v "$APP_NAME"; return 0 + fi + local rel="$REPO_DIR/impl/rust-cli/target/release/vsh" + [ -x "$rel" ] && { printf '%s' "$rel"; return 0; } + return 1 +} + +is_running() { + [ -f "$PID_FILE" ] || return 1 + kill -0 "$(cat "$PID_FILE" 2>/dev/null)" 2>/dev/null +} + +# ── Modes ──────────────────────────────────────────────────────────────────── +mode_version() { + printf '%s %s (%s) [%s]\n' "$APP_NAME" "$VERSION" "$(build_sha)" "$(platform)" + exit 0 +} + +mode_help() { + cat < () []' and exit 0. + +FILES: + repo: $REPO_DIR + startup: $REPO_DIR/scripts/run.sh + pid: $PID_FILE (deferred daemon phase) + log: $LOG_FILE + +PLATFORM: $(platform) + +Anything after the mode is passed through to vsh, e.g.: + ./launch.sh --auto -- --version + ./launch.sh --auto -- path/to/script.vsh +EOF + exit 0 +} + +mode_status() { + log "$APP_DISPLAY status" + log " version: $APP_NAME $VERSION ($(build_sha)) [$(platform)]" + if bin="$(resolve_bin)"; then + log " binary: $bin" + else + log " binary: not built (run './launch.sh --auto' or 'just build-cli')" + fi + if is_running; then + log " daemon: running (pid $(cat "$PID_FILE"))" + else + log " daemon: not running (vsh is a foreground shell; daemon phase deferred)" + fi + log " log: $LOG_FILE" + exit 0 +} + +# --auto / --start: launch the interactive shell in the current terminal. +mode_auto() { + mkdir -p "$LOG_DIR" + if ! bin="$(resolve_bin)"; then + log "Building $APP_NAME (first run)…" + if ! ( cd "$REPO_DIR/impl/rust-cli" && cargo build --release ); then + gui_err "build failed — see cargo output above" + on_start_failed + exit 1 + fi + bin="$(resolve_bin)" || { gui_err "vsh binary missing after build"; on_start_failed; exit 1; } + fi + # Foreground terminal app: exec into the shell (no nohup/daemon — that phase + # is declared deferred in the metadata header). + exec "$bin" "$@" +} + +mode_stop() { + if is_running; then + kill "$(cat "$PID_FILE")" 2>/dev/null || true + rm -f "$PID_FILE" + log "Stopped $APP_NAME daemon." + else + rm -f "$PID_FILE" 2>/dev/null || true + log "$APP_NAME is a foreground shell — no daemon to stop." + fi + exit 0 +} + +# ── Desktop integration (Linux first-class; macOS/Windows best-effort) ──────── +integ_linux() { + local force="${1:-}" + local apps="$HOME/.local/share/applications" + local bindir="$HOME/.local/bin" + local desktop="$apps/${APP_NAME}.desktop" + local launcher_copy="$bindir/${APP_NAME}-launcher" + + mkdir -p "$apps" "$bindir" + if [ -e "$desktop" ] && [ "$force" != "--force" ]; then + log "Already integrated ($desktop). Use '--integ --force' to reinstall." + exit 0 + fi + + # Copy, not symlink, so moving the repo doesn't break the menu entry. + cp "$REPO_DIR/launch.sh" "$launcher_copy" + chmod +x "$launcher_copy" + + # Terminal=true: vsh is an interactive terminal app. Route through keepopen + # if the desktop-tools are installed; otherwise launch the shell directly. + local exec_line + if [ -n "${DESKTOP_TOOLS_DIR:-}" ] && [ -x "$DESKTOP_TOOLS_DIR/keepopen.sh" ]; then + exec_line="$DESKTOP_TOOLS_DIR/keepopen.sh $APP_NAME $REPO_DIR \"$launcher_copy --auto\" \"$launcher_copy --auto\" $LOG_FILE" + else + exec_line="$launcher_copy --auto" + fi + + cat > "$desktop" </dev/null 2>&1 && \ + update-desktop-database "$apps" >/dev/null 2>&1 || true + + log "Integrated $APP_DISPLAY:" + log " desktop entry: $desktop" + log " launcher copy: $launcher_copy" + exit 0 +} + +mode_integ() { + resolve_desktop_tools + case "$(uname -s)" in + Linux) integ_linux "${1:-}";; + Darwin) log "macOS integration is best-effort/deferred; run './launch.sh --auto' to use the shell."; exit 0;; + *) log "Desktop integration for $(uname -s) is deferred; run './launch.sh --auto'."; exit 0;; + esac +} + +mode_disinteg() { + local apps="$HOME/.local/share/applications" + local bindir="$HOME/.local/bin" + local removed=0 + for f in "$apps/${APP_NAME}.desktop" "$HOME/Desktop/${APP_NAME}.desktop" "$bindir/${APP_NAME}-launcher"; do + [ -e "$f" ] && { rm -f "$f"; log "removed $f"; removed=1; } + done + rm -f "$PID_FILE" 2>/dev/null || true + command -v update-desktop-database >/dev/null 2>&1 && \ + update-desktop-database "$apps" >/dev/null 2>&1 || true + # Preserve ~/.config/$APP_NAME and $XDG_STATE_HOME/$APP_NAME by design. + [ "$removed" -eq 0 ] && log "$APP_DISPLAY was not integrated (no-op)." || \ + log "Removed $APP_DISPLAY integration (config and logs preserved)." + exit 0 +} + +# ── Dispatch ───────────────────────────────────────────────────────────────── +# Consume the mode arg, pass the remainder through to vsh where applicable. +shift || true +case "$MODE" in + --version|-V) mode_version;; + --help|-h) mode_help;; + --status) mode_status;; + --stop) mode_stop;; + --integ) mode_integ "${1:-}";; + --disinteg) mode_disinteg;; + --auto|--start|--browser|--web) + # allow './launch.sh --auto -- ARGS' or trailing ARGS + [ "${1:-}" = "--" ] && shift || true + mode_auto "$@";; + -* ) err "unknown mode: $MODE (try --help)"; exit 2;; + "" ) mode_auto;; + * ) # No mode given but args present: treat all as vsh args. + mode_auto "$MODE" "$@";; +esac diff --git a/proofs/lean4/ModelOracle.lean b/proofs/lean4/ModelOracle.lean new file mode 100644 index 00000000..c6e37452 --- /dev/null +++ b/proofs/lean4/ModelOracle.lean @@ -0,0 +1,64 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell +/- Valence Shell — Executable model oracle. + + A tiny CLI that drives the *proven* Lean filesystem model + (`mkdir`/`rmdir`/`createFile`/`deleteFile`/`fsUpdate` from FilesystemModel + + FileOperations — the exact `def`s the correspondence theorems are about) and + reports the resulting node type at a set of probe paths. + + This makes the compiled proof artifact the oracle for differential testing + against the Rust implementation (see impl/rust-cli/tests/model_oracle_correspondence.rs + and docs/LEAN4_RUST_CORRESPONDENCE.md). + + Protocol (stdin): + one operation per line, then a line "---", then one probe path per line. + Operations: `MKDIR p`, `RMDIR p`, `TOUCH p`, `RM p` (p is a '/'-joined path). + Output (stdout): one line per probe, in order — `DIR`, `FILE`, or `NONE`. +-/ +import FilesystemModel +import FileOperations + +/-- Parse a '/'-joined string into a model `Path` (list of components). -/ +def parsePath (s : String) : Path := + (s.splitOn "/").filter (· ≠ "") + +/-- Apply one operation line to the model filesystem. Unknown verbs are no-ops. -/ +def applyOp (fs : Filesystem) (line : String) : Filesystem := + match line.trim.splitOn " " with + | verb :: rest => + let p := parsePath (String.intercalate " " rest) + match verb with + | "MKDIR" => mkdir p fs + | "RMDIR" => rmdir p fs + | "TOUCH" => createFile p fs + | "RM" => deleteFile p fs + | _ => fs + | [] => fs + +/-- Query the model for the node type at a probe path. -/ +def probe (fs : Filesystem) (s : String) : String := + match fs (parsePath s) with + | none => "NONE" + | some node => + match node.nodeType with + | FSNodeType.directory => "DIR" + | FSNodeType.file => "FILE" + +/-- Read all lines from a stream until EOF (getLine returns "" at end). -/ +partial def readAllLines (s : IO.FS.Stream) (acc : List String) : IO (List String) := do + let line ← s.getLine + if line == "" then + return acc.reverse + else + readAllLines s (line.trim :: acc) + +def main : IO Unit := do + let stdin ← IO.getStdin + let raw : List String ← readAllLines stdin [] + let lines : List String := raw.filter (· ≠ "") + let ops : List String := lines.takeWhile (· ≠ "---") + let probes : List String := (lines.dropWhile (· ≠ "---")).drop 1 + let finalFS : Filesystem := ops.foldl applyOp emptyFS + for pr in probes do + IO.println (probe finalFS pr) diff --git a/proofs/lean4/lakefile.lean b/proofs/lean4/lakefile.lean index fa1b7cf1..7aaca912 100644 --- a/proofs/lean4/lakefile.lean +++ b/proofs/lean4/lakefile.lean @@ -51,3 +51,9 @@ lean_lib CrashConsistency where lean_lib PathTraversal where srcDir := "." + +-- Executable model oracle: drives the proven model for differential testing +-- against the Rust implementation. Build: `lake build model_oracle`. +lean_exe model_oracle where + root := `ModelOracle + srcDir := "." diff --git a/scripts/run.sh b/scripts/run.sh new file mode 100755 index 00000000..fb6579f5 --- /dev/null +++ b/scripts/run.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) Jonathan D.A. Jewell +# +# Startup command for the vsh shell. This is the canonical run entry point the +# Hyperpolymath launcher standard searches for ({repo-dir}/scripts/run.sh). +# It builds the release binary on first use, then execs the interactive shell. +# Extra arguments pass through to vsh (e.g. --version, a script path). +set -euo pipefail + +REPO_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +CLI_DIR="$REPO_DIR/impl/rust-cli" +BIN="$CLI_DIR/target/release/vsh" + +if [ ! -x "$BIN" ]; then + echo "vsh: building release binary (first run)…" >&2 + ( cd "$CLI_DIR" && cargo build --release ) +fi + +exec "$BIN" "$@"