// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Valence Shell (vsh) — Show Me The Receipts :toc: :icons: font The README makes claims. This file backs them up with evidence from real code. == Core Claims & Evidence === Claim 1: "794 tests passing, 0 failures — ~478 theorem candidates across 6 proof systems" **From README**: the test count and the theorem-candidate count are separate claims, and the second is a count of *candidates*, not of proved theorems. **Evidence**: `impl/rust-cli/` is where the tests live (`cargo test --all-features`); the proof trees are `proofs/{coq,lean4,agda,idris2,isabelle,mizar,z3}/`. The Coq tree alone declares 133 `Theorem`/`Lemma` commands and contains no `admit`/`Admitted`. **Caveat** — the status of every obligation is recorded in the <> below, and the two claims must not be merged. A test suite result is `tested-only`. A theorem in a proof assistant is `proven` *for the abstract model*. Nothing in this repository is `proven` about the Rust code, and no percentage is quoted for that correspondence: it is `argued` plus `tested-only` (see the ledger's model→code rows). === Claim 2: "Formally proven reversibility: `rmdir(mkdir(p, fs)) = fs`" **From README**: the theorem holds under stated preconditions. **Evidence**: `proofs/coq/filesystem_model.v:207` (`mkdir_rmdir_reversible`), with the same property restated in `proofs/lean4/FilesystemModel.lean`, `proofs/agda/FilesystemModel.agda`, `proofs/isabelle/`, `proofs/mizar/` and `proofs/z3/`. The composition lemma is `proofs/coq/filesystem_composition.v:352` (`operation_sequence_reversible`). **Caveat**: this is a theorem about an abstract `Filesystem` function, not about POSIX. The Rust CLI calls `libc`; whether that code refines the model is the open correspondence row in the ledger — argued and tested, never proved. === Claim 3: "Advanced research prototype (v0.9.0) — not production-ready" See <<_status,Status>>. This claim is accurate and is the one the repository wants readers to take away. [[proof-ledger]] == Proof Ledger Required by link:https://github.com/hyperpolymath/standards[`standards`] `docs/README-EXPLAINME-STANDARD.adoc` §5, and graded per `3-practice/PROOF-POLICY.adoc` (status vocabulary: `proven`, `proven-with-postulates`, `argued`, `tested-only`, `open`) and `mathesis` §5 (grades 3/2i/2ii/1). *Reading rule:* a row may only be as strong as the weakest step it depends on. A theorem about the model is `proven` *for the model*; the link from model to code is its own row, and it is `argued` here. Nothing in this ledger is grade 1 or grade 2ii. *Provenance of these rows (2026-11-01).* When this ledger was first written no proof assistant was installed, so no row had been re-run. **Agda and Z3 have since been installed and re-run** (see `docs/audits/2026-11-01-assurance-boundary-audit.adoc`, "Verification round, 2026-11-01"): all nine Agda modules now type-check and the Z3 scripts were replayed, and the Agda tree needed substantial source repair before it would compile at all. Coq, Lean, Creusot, Idris2, Isabelle and Mizar could not be installed in that environment, so **those rows still record the repository's own evidence** and name, in the checker column, the invocation a future audit must reproduce. Absence of a tool is an open obligation, not a passing leg (PROOF-POLICY §2.1). [cols="3,1,2,2,3",options="header"] |=== | Obligation | Status | Checker (version, flags) | Where | Trust boundary | `rmdir` undoes `mkdir` under its precondition | proven-with-postulates | Coq 8.18.0, `coqc` via `_CoqProject`, then `Print Assumptions` | `proofs/coq/filesystem_model.v:207` `mkdir_rmdir_reversible` | Equality of whole filesystems is extensional, so the 2026-07-16 record names `functional_extensionality`. Over the total-function model only; POSIX, permissions, crashes and concurrency are outside it | `write` restores previous content | proven-with-postulates | Coq 8.18.0 + `Print Assumptions` | `proofs/coq/file_content_operations.v:117` `write_file_reversible` | Same extensionality assumption; model only, and real writes go through `libc` | Sequences of reversible ops invert | proven-with-postulates | Coq 8.18.0 + `Print Assumptions` | `proofs/coq/filesystem_composition.v:352` `operation_sequence_reversible` | Extensionality where stated; model only; no crash or partial-failure semantics | Obliteration is non-injective (information is lost in the model) | proven-with-postulates | Coq 8.18.0 + `Print Assumptions` | `proofs/coq/rmo_operations.v:530` `obliterate_not_injective` | Assumptions as recorded for this file; says nothing about bytes on a device — see `docs/RMO-DURABILITY-BOUNDARY.adoc` | Overwrite covers every block of the modelled file | proven | Coq 8.18.0, `Print Assumptions`: closed under the global context (2026-07-16 record) | `proofs/coq/rmo_operations.v:315` `obliterate_overwrites_all_blocks` | The one row the record reports closed; still a theorem about the block mapping — copy-on-write, journals, spares and replicas are not modelled | Same reversibility theorems restated in Lean 4 | proven (per module; four modules do not build) | Lean 4 v4.34.1 (`lake build`; the modules that do not build are listed in `lakefile.lean`) | `proofs/lean4/FilesystemModel.lean`, `FileOperations.lean`, `FilesystemComposition.lean` | Independent restatement, *not* a translation of the Coq term, so it is not mathesis grade 2; the Lean model is also separately typed | Same theorems restated in Agda | proven-with-postulates (reproduced 2026-11-01) | `agda --library-file= .agda`, Agda 2.6.4.3 + stdlib 2.1.1 *and* 2.7.0.1 + stdlib 2.2: 9/9 modules type-check | `proofs/agda/` (all nine modules; `postulate funext` at `FilesystemModel.agda:179`) | One postulate (`funext`), no holes -- but *not* the estate invocation. `--safe` reports `Cannot postulate funext with safe flag`; `--without-K` reports `Cannot eliminate reflexive equation p = p ... K has been disabled`. So this row is reproduced under a waiver, is not mathesis grade 3, and the waiver must be recorded beside the artefact per PROOF-POLICY §4. See the audit's AP-6 and its verification round | Same theorems restated in Isabelle / Mizar / Z3 | proven-with-postulates (Isabelle) / open (Mizar) / Z3: reproduced for 4 of 5 files, `open` for `symlink_operations.smt2` | `isabelle build -D .`; `mizf` (failure-swallowing target); z3-solver 5.3.3, one process per file, parsing each `(check-sat)` | `proofs/isabelle/`, `proofs/mizar/`, `proofs/z3/` | §4 exceptions to PROOF-POLICY §1 with no recorded exception note yet; the Mizar target ends in `|| echo`, so a failing Mizar build is not distinguishable from a pass | Sandbox path normalisation never escapes the root | proven (model) / tested-only (code) | Lean 4 for the model; `proptest` for the code | `proofs/lean4/PathTraversal.lean:163`; `impl/rust-cli/tests/security_tests.rs` | The Lean theorem is about the Lean model. The property test is evidence that `resolve_path` matches, not a proof | The Rust CLI refines the proven model | argued | - | `docs/LEAN4_RUST_CORRESPONDENCE.adoc`; `docs/PROOF-OPEN-FRONTIER.adoc` F-1 | Not formalised. Creusot contracts (PROOF-POLICY §1) do not exist on this code yet | Rust and model agree on sampled operation sequences | tested-only | `just test-correspondence-model` (compiled `ModelOracle`), 1,218 probes / 200 sequences | `impl/rust-cli/tests/model_oracle_correspondence.rs` | Sampled, precondition-respecting sequences only; a divergence would be a real bug but agreement is not a proof | Idris2 ABI layout, encodings and round-trips match the C header | tested-only | `--total`, plus `scripts/check-abi-layout.sh` | `proofs/idris2/src/Filesystem/`, `.machine_readable/IDRIS2_AXIOMS.a2ml` | Two registered `believe_me` axioms (`axStringEqRefl`, `axBits8EqRefl`); the C/FFI layer beyond layout is unchecked | Audit log detects mutation/truncation of its own chain | tested-only | HMAC-SHA-256 chaining tests | `impl/rust-cli/src/audit_log.rs` | Only when a key is supplied; tail truncation needs an external checkpoint, which does not exist | RMO key provisioning, external anchoring, device erasure | open | - | - | No key source, no anchor, no `secure_erase`; not a GDPR determination | A test or oracle implies refinement | open | - | - | A test is `tested-only` by definition (PROOF-POLICY §5); no test may be cited as a refinement proof | Valence Shell's audit entries are *known* rather than *believed* (warrant/receipt) | open | - | - | `hyperpolymath/epistemic-types` is not imported (0 imports). Warrant ≠ proof and receipt ≠ certificate upstream; nothing here models that distinction yet | JanusKey operations refine Valence Shell's model | open | - | - | `hyperpolymath/januskey` / `reversible-core` are not imported or depended on. The D204 ruling records intent only |=== == Dogfooded Across The Account Uses polyglot formal verification stack (Coq + Lean 4 + Agda + Isabelle + Mizar + Z3). Same pattern across: - https://github.com/hyperpolymath/absolute-zero[absolute-zero] — Compositional algebra with CNO (Certified Null Operation) theory - https://github.com/hyperpolymath/proven-servers[proven-servers] — Protocol verification (Idris2 ABI) - https://github.com/hyperpolymath/burble[burble] — Telecom control plane (Lean 4 core) All share: *Multiple proof systems for cross-validation, honest status reporting, no extraction claims without mechanization.* == File Map [cols="1,3"] |=== | Path | Contents & Purpose | `impl/rust-cli/src/main.rs` | Rust CLI entry: REPL loop, command parsing, interactive shell with reedline | `impl/rust-cli/src/lib.rs` | Library root: module declarations, public API | `impl/rust-cli/src/state.rs` | ShellState: file system state, operation history, undo/redo stacks. Core reversibility tracking. | `impl/rust-cli/src/commands.rs` | Built-in commands: mkdir, rmdir, touch, rm, cp, mv, ln, undo, redo, explain, checkpoint, restore, diff | `impl/rust-cli/src/parser.rs` | Command parsing: tokenization, variable expansion, glob expansion, quote processing. No formal proofs—empirical parsing. | `impl/rust-cli/src/external.rs` | External command execution: PATH lookup, subprocess spawning, pipe handling, redirection setup | `impl/rust-cli/src/pipeline.rs` | Unix pipeline implementation: multi-stage pipes with proper file descriptor management | `impl/rust-cli/src/redirection.rs` | I/O redirection: > (write), >> (append), < (read), 2> (stderr), 2>> (append stderr), &> (both), 2>&1 (combine) | `impl/rust-cli/src/glob.rs` | POSIX-compliant glob expansion: *, ?, [...], {...}. Hidden file handling (requires explicit leading dot). | `impl/rust-cli/src/job_control.rs` | Job control: bg, fg, jobs, kill commands. Signal handling for Ctrl+Z (SIGTSTP), Ctrl+C (SIGINT). | `impl/rust-cli/src/process_substitution.rs` | Process substitution: <(cmd) and >(cmd) via FIFOs | `impl/rust-cli/src/arithmetic.rs` | Arithmetic expansion: $((expr)) with full operator support, shift overflow protection | `impl/rust-cli/src/here_doc.rs` | Here documents: <>). **What works**: - Functional shell: 794 tests passing, interactive REPL working - 133 Coq theorems plus restatements in five further systems, all about abstract models; every obligation's status is a ledger row - Reversibility tracking: undo/redo functional for modelled operations - Most POSIX features: pipes, redirections, glob, job control, variables **What is not established**: - No `proven` correspondence between the model and the Rust CLI (Creusot contracts do not exist here); the status is `argued` + `tested-only` - No shell functions (`func() { ... }`) or script execution of `.sh` files - RMO: `obliterate` is implemented as best-effort overwrite + unlink + an unsigned residue; no key provisioning, no anchor, no GDPR determination - POSIX coverage is a subset == Questions? Open an issue or reach out at j.d.a.jewell@open.ac.uk — happy to explain the proof architecture, reversibility guarantees, or the honest gap between proofs and implementation.