// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell = Frequently Asked Questions :toc: macro :toclevels: 2 :icons: font toc::[] == What is valence-shell, in one sentence? A formally verified Unix-style shell whose model-layer filesystem operations (`mkdir`, `rmdir`, `cp`, `mv`, `ln -s`, `chmod`, `chown`, file content read/write) are proven reversible in machine-checked models (Agda as the theory source, rechecked in Lean 4 and Rocq/Coq, with supplementary Z3 checks), with a working interactive Rust CLI that mirrors those proven operations and provides undo/redo, named checkpoints, and proof-annotated dry-runs. == Why prove anything about a shell? Because every traditional shell silently relies on the user trusting the filesystem-mutation primitives the shell exposes. `mkdir` and `rmdir` are *assumed* to be inverses; `cp` is *assumed* to be a non-destructive copy; `rm -rf` is *assumed* to do what its name suggests. valence-shell makes those assumptions mathematical theorems with machine-checkable proofs in several logical foundations, so an error in one foundation's modelling does not propagate. This matters most for two classes of work: * **Reversible operations (RMR — Remove-Match-Reverse)** — undo/redo, checkpoint/restore, transaction grouping. If you can prove the operation is reversible, you can ship the rollback button. * **Irreversible, auditable operations (RMO — Remove-Match-Obliterate)** — deletion. Proving the *abstract* transition is non-injective tells you that the modelled state does not determine the pre-state. It does **not** show that bytes are gone from the storage stack, and it is not a third-party attestation of legal compliance; the implemented `obliterate` is best-effort local overwrite + unlink + an audit residue. == Why several proof systems and not one? Cross-validation. The checked systems sit on different logical foundations: * Agda — intensional type theory (theory source of truth, owner ruling 2026-11-09) * Lean 4 — dependent type theory (recheck leg and executable model oracle) * Rocq/Coq — Calculus of Inductive Constructions (recheck leg; extraction path to OCaml) * Z3 SMT — first-order logic with theories (supplementary; `ASSUMED` under PROOF-POLICY §5) Isabelle/HOL and Mizar proofs were archived unchecked on 2026-11-09 (`archive/proofs/`) and are not counted as evidence. When independently checked legs prove the same statement, it is unlikely that all of them modelled the problem incorrectly in the same way. The Lean and Rocq statements have not yet been compared against the Agda source one by one (`docs/audits/2026-11-09-proof-ground-truth.adoc`), so that agreement is a goal, not yet a measured fact. This is the same pattern seL4 and CompCert use, and it is the central technical commitment of the project — see `INTENT.contractile` and `.machine_readable/bot_directives/methodology.a2ml` for the architectural-invariant statement. == How do I trust the proofs? Run them yourself, air-gapped if you prefer: [source,bash] ---- # With Nix (recommended — pins the prover versions) nix develop just verify-proofs # Or per-system just build-coq # produces .vo certificates just build-lean4 # compiles to executable just build-agda # type-checks All.agda under --safe --without-K --cubical-compatible # Isabelle and Mizar are archived (archive/proofs/README.adoc has the successor map) just build-z3 # SMT SAT/UNSAT queries ---- The proof artefacts are the trust anchor, not the README claims. If the README claims a theorem exists and `just verify-proofs` does not produce a certificate for it, the README is wrong — file an issue. For an honest accounting of *which* theorems are open holes vs. proved, see `docs/PROOF_HOLES_AUDIT.adoc` (the single source of truth) and the deep-audit inventory in `docs/audits/2026-06-01-deep-audit.adoc`. == Is this production-ready? **No.** valence-shell at v0.9.0 is an advanced research prototype. What is solid: * The machine-checked proofs of the model-layer operations (Agda (theory source), Lean 4 and Rocq/Coq (rechecks), Z3 (supplementary); Isabelle/HOL and Mizar archived unchecked). ~478 theorem candidates in the 2026-06-01 census; 0 real gaps (Coq `obliterate_overwrites_all_blocks` CLOSED, re-verified 2026-07-16 via `Print Assumptions` under Coq 8.18.0) + 2 documented axioms (1 justified decidability + 1 structural funext). * The Rust CLI. 736 tests passing, 0 failures, 7 fuzz targets, working shell surface (pipelines, redirections, here-docs, job control, variables, control structures, glob, quoting). What is **not** solid enough for production: * The link from the proven model to the Rust runtime is `argued` and `tested-only` (property tests plus a compiled-model differential oracle), never `proven`. That is the v1.0.0 blocker. See link:EXPLAINME.adoc#proof-ledger[the Proof Ledger]; this repository quotes no confidence percentage for it. * 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. Use for research, education, experimentation. Do not use as your login shell on a system you care about. == Why is `200+ theorems` / `250+ theorems` / `~478 candidates` all over the place? Historical drift. The figure varied as proof work landed and as different counting methodologies were used (definitions vs. lemmas vs. all proof obligations including the Idris2 ABI). The 2026-06-01 deep audit (issue #42) locked the count at **478 theorem candidates** across the six proof systems then in use plus the Idris2 ABI layer, distributed as below. This is the 2026-06-01 census; Isabelle/HOL and Mizar proofs were archived unchecked on 2026-11-09 (`archive/proofs/`), and the current per-obligation status is in `EXPLAINME.adoc#proof-ledger`. [cols="1,1,3",options="header"] |=== |System |Count |Notes |Lean 4 |101 |Recheck leg (Agda is the theory source since 2026-11-09) |Coq |131 |Includes `extraction.v` — 0 admits (re-verified 2026-07-16, Coq 8.18.0) |Isabelle/HOL |76 |Archived unchecked 2026-11-09 |Agda |85 |3 postulates at the census; 0 since 2026-11-09 (funext removed) |Mizar |63 |Archived unchecked 2026-11-09 |Z3 SMT |125 asserts |Automated decision procedures |Idris2 (ABI + filesystem) |~22 |0 holes, 0 partials, 2 primitive-eq axioms (closed #151/#152) |=== If you see a stale number elsewhere in the repo, please file an issue — the audit log at `docs/audits/` is the bookkeeping. == What's the difference between RMR and RMO? * **RMR — Remove-Match-Reverse.** The operation is *reversible*: there exists an inverse that recovers the prior state exactly. Theorems of this form look like `precondition p fs -> reverse(op(p, fs)) = fs`. This is what `mkdir`/`rmdir`, `cp`/`mv`/`ln -s`, file write, and `chmod`/`chown` get. * **RMO — Remove-Match-Obliterate.** The operation *destroys information*: it is provably non-injective (different starting states can produce the same result). Theorems of this form look like `exists fs1 fs2, fs1 != fs2 /\ obliterate(fs1) = obliterate(fs2)`. This is the correct formalisation of "irreversibly deleted" — the historical formulation `not (exists recover, recover(obliterate(...)) = sfs)` is *false* (the constant function trivially satisfies it) and was caught and replaced 2026-04-03 across Agda, Isabelle, and Lean 4. The two are complementary: RMR gives you safety (rollback exists), RMO gives you privacy (no rollback is possible, by construction). == What's the difference between algorithmic and thermodynamic reversibility? * **Algorithmic** (what valence-shell has): `F⁻¹(F(s)) = s` — operations can be undone; the information needed to invert is preserved by the system. * **Thermodynamic** (what valence-shell does NOT have): the Landauer limit / Bennett's reversible computing — physical energy → 0 per bit erased. valence-shell makes claims about the former, not the latter. If you need thermodynamic guarantees, you need different hardware, not different proofs. == Can I use this in my project? * **For research / education / experimentation**: yes, please. * **For production**: not yet (wait for v1.0.0; the v1.0.0 blocker is the mechanised Lean → Rust correspondence proof). * **Licence**: `MPL-2.0` (SPDX). See `LICENSE`. Note that the project migrated from PMPL-1.0 to MPL-2.0 in commit `990b147` — the `LICENSES/` directory carries the REUSE-format SPDX metadata. == How does this relate to Absolute Zero / CNO? Absolute Zero contributed the **CNO (Certified Null Operation)** composition theory: a reversible operation followed by its inverse is provably the identity. valence-shell implements that theory specifically for filesystem operations — see the `cno_identity_element` theorem in the README and the proofs of `operation_sequence_reversible`. == Where is the FFI / ABI surface? Valence-shell follows the estate boundary-convention policy (`feedback_estate_boundary_conventions`): * In-process FFI (Rust ↔ C) — Zig scaffolding in `impl/zig/`. * Formal ABI / proof carrier — Idris2 in `proofs/idris2/` (~22 theorems, 0 holes, 0 partial markers, 2 primitive-eq axioms; closed via #151/#152, builds under `--total`). * BEAM ↔ native — would use SNIFs; not currently wired (BEAM daemon is designed but not implemented). * Compile target / typed-wasm — not currently a target. * Cross-system service discovery — Groove Protocol; not currently wired. The Rust CLI is the production runtime; OCaml extraction (`proofs/coq/extraction.v`) exists in design form but is not wired into a build target. == What is the MAA framework, exactly? **MAA — Mutually Assured Accountability.** Every filesystem-touching action in valence-shell falls into one of two provable categories: . RMR — reversible, with a proven inverse and an undo/redo path. . RMO — irreversible by design, with a proof that information was destroyed and an audit trail that survives the destruction. "Mutually assured" means *both* parties (the user and any third-party auditor) have machine-checkable evidence: the user knows what undo/redo guarantees they have; the auditor can verify that a claimed deletion actually destroyed the information. No party can claim a different story than the proofs allow. This is the broader reason the project exists. The shell is the artefact; the framework is the contribution. == Where do I report a problem? * **Bug** — https://github.com/Hyperpolymath/valence-shell/issues * **Security vulnerability** — see `SECURITY.md` and `.well-known/security.txt`. * **A documentation count is wrong** — file an issue tagged `docs` and cite the reality (`find ... | wc -l`, `cargo test`, etc.). The 2026-06-01 deep-audit log in `docs/audits/2026-06-01-deep-audit.adoc` is the bookkeeping baseline. * **The proofs don't reproduce** — please attach `just verify-proofs` output and the version of each prover you used (`nix develop` pins them). == Who maintains this? See `MAINTAINERS.adoc`. Primary development is on GitLab (`https://gitlab.com/non-initiate/rhodinised/vsh`); the GitHub repository is the canonical public mirror.