From 563265423b747a6020dd13f7d5e161ace3c61f0d Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 17 Jul 2026 05:18:57 +0000 Subject: [PATCH 1/4] feat(launcher): E-Grade Launcher Standard conformant launch.sh Implements the Hyperpolymath E-Grade Launcher Standard (hyperpolymath/standards launcher-standard.adoc/.a2ml) for vsh: - launch.sh: full mode surface --auto/--start/--stop/--status/--browser/ --web/--integ/--disinteg/--help/--version. Version output matches the required 'vsh () []' format exactly. - Desktop integration (Linux first-class): idempotent --integ/--disinteg, copy-not-symlink launcher, Terminal=true, .desktop at 0444, config+logs preserved on --disinteg. macOS/Windows best-effort. - err()/log(), stderr-always, GUI-error + soft-attach sourced via the published desktop-tools resolution ladder with graceful no-op degradation. - PID/log paths in 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. - scripts/run.sh: canonical startup command the standard searches for. - just run / just launch delegate to ./launch.sh --auto. - docs/LAUNCHER.md: conformance attestation + deferred-phase rationale. Verified: --version format, --status, --stop, --auto passthrough, --help, --browser/--web aliases, unknown-mode exit 2, and a full --integ/--disinteg idempotency cycle. shellcheck clean (warning+); bash -n clean. Scope note: full alignment used the public standard fetched from hyperpolymath/standards (that repo is not in this session's GitHub scope). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU --- CHANGELOG.adoc | 21 +++ Justfile | 8 +- QUICKSTART-USER.adoc | 16 +++ docs/LAUNCHER.md | 78 ++++++++++++ launch.sh | 296 +++++++++++++++++++++++++++++++++++++++++++ scripts/run.sh | 20 +++ 6 files changed, 436 insertions(+), 3 deletions(-) create mode 100644 docs/LAUNCHER.md create mode 100755 launch.sh create mode 100755 scripts/run.sh diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index af92a87..761b9f5 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -17,6 +17,27 @@ 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 + +==== 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/Justfile b/Justfile index a9a131a..4371e43 100644 --- a/Justfile +++ b/Justfile @@ -126,13 +126,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 6d1e93d..326e788 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/docs/LAUNCHER.md b/docs/LAUNCHER.md new file mode 100644 index 0000000..756b713 --- /dev/null +++ b/docs/LAUNCHER.md @@ -0,0 +1,78 @@ + +# 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/launch.sh b/launch.sh new file mode 100755 index 0000000..41df974 --- /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/scripts/run.sh b/scripts/run.sh new file mode 100755 index 0000000..fb6579f --- /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" "$@" From 378e7e206c124ab5a9e4e0bf70f2d7e4fbef9fa8 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 17 Jul 2026 05:32:03 +0000 Subject: [PATCH 2/4] feat(correspondence): compiled Lean model as differential test oracle MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Advances the Lean->Rust correspondence toward mechanization by making the compiled proof artifact the test oracle. - proofs/lean4/ModelOracle.lean + lean_exe model_oracle: compiles the exact proven model defs (mkdir/rmdir/createFile/deleteFile/fsUpdate from FilesystemModel + FileOperations) into a standalone executable that reports the node type (DIR/FILE/NONE) at probe paths. - impl/rust-cli/tests/model_oracle_correspondence.rs: generates precondition-respecting op sequences (shadow tracker ensures validity), applies them to the real Rust ShellState, drives the same sequence through the Lean oracle, and asserts model and impl agree at every touched path. 1218 probes agree across 200 sequences. Skips cleanly if the oracle is not built (no Lean toolchain required for ). - just build-model-oracle / test-correspondence-model; wired into lean-verification.yml CI. - docs/LEAN4_RUST_CORRESPONDENCE.md: documents the harness and, honestly, its limits — this is differential testing against the proof artifact, not a full refinement proof (still the v1.0 blocker). Records why the Coq extraction is not executable (Path -> option FSNode function domain + classical axioms in is_empty_dir_dec; needs FMaps.t FSNode migration) and the mechanization roadmap. Verified: lake build model_oracle OK; oracle smoke test matches model semantics (incl. non-recursive rmdir leaving orphan children); differential test passes with and without VSH_MODEL_ORACLE env (auto-detects .lake path). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU --- .github/workflows/lean-verification.yml | 12 + CHANGELOG.adoc | 18 ++ Justfile | 12 + docs/LEAN4_RUST_CORRESPONDENCE.md | 68 +++- .../tests/model_oracle_correspondence.rs | 296 ++++++++++++++++++ proofs/lean4/ModelOracle.lean | 64 ++++ proofs/lean4/lakefile.lean | 6 + 7 files changed, 473 insertions(+), 3 deletions(-) create mode 100644 impl/rust-cli/tests/model_oracle_correspondence.rs create mode 100644 proofs/lean4/ModelOracle.lean diff --git a/.github/workflows/lean-verification.yml b/.github/workflows/lean-verification.yml index 7872dd7..b4ff293 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/CHANGELOG.adoc b/CHANGELOG.adoc index 761b9f5..f87886a 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -19,6 +19,24 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 === Added — 2026-07-17 +==== 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`, diff --git a/Justfile b/Justfile index 4371e43..de2799f 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..." diff --git a/docs/LEAN4_RUST_CORRESPONDENCE.md b/docs/LEAN4_RUST_CORRESPONDENCE.md index 62695e2..87b1db1 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/impl/rust-cli/tests/model_oracle_correspondence.rs b/impl/rust-cli/tests/model_oracle_correspondence.rs new file mode 100644 index 0000000..389301d --- /dev/null +++ b/impl/rust-cli/tests/model_oracle_correspondence.rs @@ -0,0 +1,296 @@ +// 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/proofs/lean4/ModelOracle.lean b/proofs/lean4/ModelOracle.lean new file mode 100644 index 0000000..c6e3745 --- /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 fa1b7cf..7aaca91 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 := "." From 4883a4298624751aad1f83f6cdc0a378d83d0517 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 17 Jul 2026 05:47:11 +0000 Subject: [PATCH 3/4] feat(rmo): wire obliterate into dispatch + audit residue (secure deletion) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 /.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 Claude-Session: https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU --- .../ECHO_TYPES_OCHRANCE_BRIDGE.a2ml | 4 +- .../bot_directives/methodology.a2ml | 2 +- CHANGELOG.adoc | 22 +++ CLAUDE.md | 21 ++- FAQ.adoc | 6 +- README.adoc | 2 +- ROADMAP.adoc | 6 +- TOPOLOGY.md | 2 +- docs/ECHO-TYPES-OCHRANCE-BRIDGE.adoc | 4 +- docs/ROADMAP_TO_V1.md | 2 +- docs/wiki/For-Marketers-and-Journalists.md | 2 +- docs/wiki/For-Users.md | 7 +- docs/wiki/Verification-Status.md | 4 +- impl/rust-cli/src/commands/secure_deletion.rs | 39 +++++ impl/rust-cli/src/executable.rs | 28 +++- impl/rust-cli/src/parser.rs | 21 +++ impl/rust-cli/tests/obliterate_rmo_tests.rs | 134 ++++++++++++++++++ 17 files changed, 282 insertions(+), 24 deletions(-) create mode 100644 impl/rust-cli/tests/obliterate_rmo_tests.rs diff --git a/.machine_readable/ECHO_TYPES_OCHRANCE_BRIDGE.a2ml b/.machine_readable/ECHO_TYPES_OCHRANCE_BRIDGE.a2ml index d7f813c..b906f3a 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 3004b0b..2c767d3 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 f87886a..ca63b0c 100644 --- 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 + `/.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 index 1d82708..a46d17e 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 b2f1828..1a6e703 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/README.adoc b/README.adoc index 9c05782..2aeb19d 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: `< --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 6801504..0ccdc90 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/secure_deletion.rs b/impl/rust-cli/src/commands/secure_deletion.rs index 54b0d26..b28d909 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 28716de..9fe8797 100644 --- a/impl/rust-cli/src/executable.rs +++ b/impl/rust-cli/src/executable.rs @@ -122,6 +122,22 @@ 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 +1236,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 +1248,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 +1260,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 3695a2c..8fc8751 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, @@ -3289,6 +3297,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")); 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 0000000..8209c8b --- /dev/null +++ b/impl/rust-cli/tests/obliterate_rmo_tests.rs @@ -0,0 +1,134 @@ +// 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"); +} From a96306425726bd6dcae3d0ddf4e7c30b35c8e67b Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 17 Jul 2026 05:54:32 +0000 Subject: [PATCH 4/4] style(rust-cli): fix clippy 1.97 + rustfmt for CI green CI (Rust 1.97) failed two checks on this branch: - rustfmt: new test files + the Obliterate executor arm needed formatting. - clippy -D warnings: unneeded_wildcard_pattern (field: _ redundant with ..) in commands.rs (Chmod/Chown) and parser.rs (External/Touch), which clippy 1.97 newly errors on; plus a pre-existing let_and_return in the ${VAR:=default} expansion path. Fixes: - cargo fmt across the crate (new tests + executable.rs). - Remove redundant bindings where already covers them. - Inline the let-and-return in AssignDefault expansion (behavior unchanged). Verified against CI's exact toolchain: cargo +1.97.0 clippy --all-targets --all-features -- -D warnings is clean; cargo +1.97.0 fmt --check has 0 diffs. Full lib suite (317) + obliterate RMO tests (6) still green. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU --- impl/rust-cli/src/commands.rs | 3 +- impl/rust-cli/src/executable.rs | 7 +++- impl/rust-cli/src/parser.rs | 7 ++-- .../tests/model_oracle_correspondence.rs | 36 ++++++++++++++----- impl/rust-cli/tests/obliterate_rmo_tests.rs | 15 ++++++-- 5 files changed, 50 insertions(+), 18 deletions(-) diff --git a/impl/rust-cli/src/commands.rs b/impl/rust-cli/src/commands.rs index c1e22c4..1f42faf 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/executable.rs b/impl/rust-cli/src/executable.rs index 9fe8797..03cd202 100644 --- a/impl/rust-cli/src/executable.rs +++ b/impl/rust-cli/src/executable.rs @@ -129,7 +129,12 @@ impl ExecutableCommand for Command { } => { let expanded_path = crate::parser::expand_variables(path, state); if redirects.is_empty() { - commands::secure_deletion::obliterate_path(state, &expanded_path, false, *force)?; + 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) diff --git a/impl/rust-cli/src/parser.rs b/impl/rust-cli/src/parser.rs index 8fc8751..467ab0a 100644 --- a/impl/rust-cli/src/parser.rs +++ b/impl/rust-cli/src/parser.rs @@ -2264,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 @@ -4346,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 index 389301d..f448c8a 100644 --- a/impl/rust-cli/tests/model_oracle_correspondence.rs +++ b/impl/rust-cli/tests/model_oracle_correspondence.rs @@ -131,7 +131,10 @@ fn gen_sequence(rng: &mut Rng, max_ops: usize) -> (Vec, Vec) { } shadow.insert(p.clone(), Kind::Dir); touched.insert(p.clone(), ()); - ops.push(Op { verb: "MKDIR", path: p }); + ops.push(Op { + verb: "MKDIR", + path: p, + }); } else if roll < 8 { // TOUCH under an existing directory let ds = dirs(&shadow); @@ -143,7 +146,10 @@ fn gen_sequence(rng: &mut Rng, max_ops: usize) -> (Vec, Vec) { } shadow.insert(p.clone(), Kind::File); touched.insert(p.clone(), ()); - ops.push(Op { verb: "TOUCH", path: p }); + ops.push(Op { + verb: "TOUCH", + path: p, + }); } else if roll < 9 { // RM an existing file let files: Vec = shadow @@ -157,7 +163,10 @@ fn gen_sequence(rng: &mut Rng, max_ops: usize) -> (Vec, Vec) { let p = files[rng.below(files.len())].clone(); shadow.remove(&p); touched.insert(p.clone(), ()); - ops.push(Op { verb: "RM", path: p }); + ops.push(Op { + verb: "RM", + path: p, + }); } else { // RMDIR an empty directory let empties: Vec = shadow @@ -171,7 +180,10 @@ fn gen_sequence(rng: &mut Rng, max_ops: usize) -> (Vec, Vec) { let p = empties[rng.below(empties.len())].clone(); shadow.remove(&p); touched.insert(p.clone(), ()); - ops.push(Op { verb: "RMDIR", path: p }); + ops.push(Op { + verb: "RMDIR", + path: p, + }); } } @@ -260,7 +272,10 @@ fn rust_matches_proven_lean_model() { _ => unreachable!(), }; r.unwrap_or_else(|e| { - panic!("seq {seq}: generated op {} {} rejected by impl: {e}", op.verb, op.path) + panic!( + "seq {seq}: generated op {} {} rejected by impl: {e}", + op.verb, op.path + ) }); } @@ -278,11 +293,14 @@ fn rust_matches_proven_lean_model() { for (probe, model_kind) in probes.iter().zip(model.iter()) { let impl_kind = rust_kind(temp.path(), probe); assert_eq!( - model_kind, impl_kind, + 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::>() + ops.iter() + .map(|o| format!("{} {}", o.verb, o.path)) + .collect::>() ); checked_probes += 1; } @@ -292,5 +310,7 @@ fn rust_matches_proven_lean_model() { checked_probes > 0, "no probes were checked — generator produced only empty sequences" ); - eprintln!("model_oracle_correspondence: {checked_probes} probes agreed across {SEQUENCES} 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 index 8209c8b..64f9e32 100644 --- a/impl/rust-cli/tests/obliterate_rmo_tests.rs +++ b/impl/rust-cli/tests/obliterate_rmo_tests.rs @@ -33,7 +33,10 @@ fn obliterate_is_wired_into_dispatch() { } // --force before or after the path both work. - for input in ["obliterate --force secret.txt", "obliterate secret.txt --force"] { + 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}"); @@ -79,7 +82,10 @@ fn obliterate_writes_rmo_audit_residue() { .expect("execute"); let audit = temp.path().join(".vsh-audit.log"); - assert!(audit.exists(), "RMO audit residue must be written to the sandbox"); + 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"), @@ -130,5 +136,8 @@ fn obliterate_then_recreate_has_no_old_content() { 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"); + assert!( + !back.windows(4).any(|w| w == b"4111"), + "no old plaintext remains" + ); }