- 1. Overview
- 2. Reconciliation with prior docs
- 3. Cross-system witness matrix
- 4. The composition story (RMR path)
- 5. The RMO path (formal non-reversibility)
- 6. Per-area narrative
- 7. Assumption registry
- 8. The Idris2 layer (stated, not proven)
- 9. Open frontier
- 10. Building and checking
- 11. References
- 12. Changelog
|
Note
|
This is the canonical, theorem-level narrative of valence-shell’s verification.
It supersedes the earlier The verification has seven independent witnesses (Coq, Lean 4, Agda, Isabelle/HOL, Mizar, Z3 SMT, Idris2), ~9,860 lines of proof script in the 5-assistant closed core plus ~1,200 lines of Idris2 stubs, and roughly ~478 named theorems if we count every helper. After the closure passes of 2026-03-08, 2026-04-03, and 2026-04-12, the assumption count splits into two tiers:
All assumptions are explicit. All are documented below. |
Valence Shell is a formally verified reversible shell. The verification target is the MAA (Mutually Assured Accountability) framework: every operation that modifies the filesystem must either
-
compose with its inverse to produce a no-op (the RMR path —
Reverse · Match · Reverse), or -
carry a proof of non-injectivity — proving information loss is unrecoverable by any computable function (the RMO path —
Reverse · Match · Obliterate).
These two paths correspond to the two-mode design described in
arcvix-formally-verified-reversible-shell.tex (root-level paper).
The polyglot verification choice deliberately removes single-foundation
risk. If mkdir_rmdir_reversible held in Lean 4 but fell over in Coq we
would learn something important. Today the theorem stands in all five
proof assistants and is also queried in Z3 with no SAT counterexample.
Two earlier docs describe the proof landscape and have drifted in opposite directions:
| Doc | Date | Claim | Reality (2026-06-01) |
|---|---|---|---|
|
(undated, pre-2026-04-03) |
7 Agda postulates open across 3 files |
All 7 closed during the 2026-04-03 closure session. Only |
|
2026-04-12 |
1 real gap: Coq |
|
This document is the source of truth as of 2026-06-01.
Each row is a theorem; columns are proof assistants. ✓ = proven and checked; ◯ = stated but admitted/postulated/sorry; — = not formalised in that system; * = proven with explicit assumption (see registry).
| Theorem | Coq | Lean 4 | Agda | Isabelle | Mizar | Z3 |
|---|---|---|---|---|---|---|
|
✓ |
✓ |
✓ |
✓ |
✓ |
— |
|
✓ |
✓ |
✓ |
✓ |
✓ |
— |
|
✓ |
✓ |
✓ |
✓ |
✓ |
— |
|
✓ |
✓ |
✓* |
✓ |
✓ |
✓ |
|
✓* (model gap) |
✓ |
✓* |
✓ |
— |
— |
|
✓ |
✓ |
✓ |
✓ |
✓ |
— |
|
✓ |
✓ |
✓ |
✓ |
✓ |
— |
|
✓ |
✓ |
✓ |
✓ |
— |
— |
|
✓ |
✓ |
✓ |
✓ |
✓ |
— |
|
✓ |
✓ |
✓ |
✓ |
— |
— |
|
◯ (admit. line 199) |
✓ |
✓ |
✓ |
— |
— |
|
inherits admit. |
✓ |
✓ |
✓ |
— |
— |
|
✓ |
✓ |
✓ |
✓ |
✓ |
— |
|
✓ |
✓ |
✓* (postulate w/ proof sketch, deferred to Lean) |
✓ |
— |
— |
|
✓ |
✓ |
✓ |
✓ |
— |
— |
|
✓ |
✓ |
✓ |
✓ |
✓ |
✓ |
|
✓ |
✓ |
✓ |
✓ |
✓ |
✓ |
|
✓ |
✓ |
✓ |
✓ |
— |
✓ |
|
✓ |
✓ |
✓ |
— |
— |
— |
|
✓ |
✓ |
✓ |
✓ |
✓ |
✓ |
|
✓ |
✓ |
✓ |
✓ |
✓ |
— |
|
✓ |
✓ |
✓ |
✓ |
✓ |
— |
|
✓ |
✓ |
✓ |
✓ |
✓ |
— |
|
✓ |
✓ |
✓ |
✓ |
✓ |
✓ |
|
✓ |
✓ |
✓ |
✓ |
✓ |
— |
|
✓ |
✓ |
✓ |
✓ |
✓ |
— |
|
✓ |
✓ |
✓ |
✓ |
✓ |
— |
|
✓ |
✓ |
✓ |
✓ |
✓ |
✓ |
|
✓ |
✓ |
✓ |
— |
— |
— |
|
✓ |
✓ |
— |
— |
— |
— |
|
✓ |
✓ |
✓ |
✓ |
— |
— |
|
✓ |
✓ |
✓ |
✓ |
— |
— |
|
✓ |
✓ |
✓ |
— |
— |
— |
|
— |
✓ |
✓ |
✓ |
— |
— |
|
— |
✓ |
✓ |
✓ |
— |
— |
|
— |
✓ |
✓ |
✓ |
— |
— |
|
— |
✓ |
✓ |
✓ |
— |
— |
|
✓ |
✓ |
— |
— |
— |
— |
|
✓ |
✓ |
— |
✓ |
— |
— |
|
✓ (proved 2026-04-12) |
— |
— |
— |
— |
— |
|
✓ (proved 2026-04-12) |
— |
— |
— |
— |
— |
|
✓ |
— |
— |
— |
— |
— |
Total: ~42 named theorems above; full bench is ~200 if you count every
helper lemma, including the 8 Lean 4 storage-equalisation lemmas that
underpin obliterate_not_injective and the 6 path-prefix helpers behind
well_formed_ancestor_exists.
The single most load-bearing theorem in the system is
Theorem operation_sequence_reversible :
forall (ops : list Operation) (fs : Filesystem),
all_reversible ops fs ->
apply_sequence (reverse_sequence ops) (apply_sequence ops fs) = fs.(proofs/coq/filesystem_composition.v:216-240, mirror in proofs/lean4/FilesystemComposition.lean and similar in Agda/Isabelle.)
It says: any sequence of mutually-reversible operations, when reversed,
returns the filesystem to its starting state. Critically, this is what
underwrites the user-facing begin/commit/rollback transaction
grouping in the Rust CLI.
It compiles three smaller pieces:
-
Per-op reversibility (
single_op_reversible) — for each ofOpMkdir/OpRmdir/OpCreateFile/OpDeleteFile, applying the inverse recovers the input. -
Sequence semantics (
apply_sequence,reverse_sequence) — aFixpointoverlist Operationand amap reverse_op ∘ rev. -
Induction lemma —
apply_sequence (reverse_sequence (op :: ops')) fsexpands viamap_appso the inductive step terminates in a single application ofsingle_op_reversible.
The is_CNO_sequence definition then names the consequence: any
reversible op produces a Certified Null Operation (CNO) when followed by
its inverse, connecting the proof to Absolute Zero’s CNO algebra. This
is the formal correspondence the README and CLAUDE.md mention but rarely
spell out.
single_op_reversible is proven in Lean 4, Agda, and Isabelle without
admits. Coq alone has a missing branch:
Theorem single_op_reversible :
forall op fs, reversible op fs -> apply_op (reverse_op op) (apply_op op fs) = fs.
Proof.
intros op fs [Hpre Hrev]. destruct op.
- (* OpMkdir *) apply single_mkdir_reversible. assumption.
- (* OpRmdir *) (* MODEL GAP — see Assumption Registry *) simpl in *. admit.
- (* OpCreateFile *) apply single_create_file_reversible. assumption.
- (* OpDeleteFile *) simpl in *. apply create_delete_file_reversible. assumption.
Qed.The OpRmdir branch is impossible to discharge under the current model
because mkdir p writes Some (mkFSNode Directory default_perms), but
the original directory at p may have had non-default permissions. See
single_op_reversible OpRmdir branch — model gap for the registry entry and possible closures.
The RMO half of MAA — secure deletion / obliteration — has to prove that the operation is not reversible, otherwise the whole "obliterate beats anyone with a court order asking for the data" story fails.
This was the most subtle proof in the system. The first attempt
(obliterate_not_reversible) stated
¬ ∃ recover, ∀ sfs, recover (obliterate path sfs) = sfswhich is trivially false — the constant function fun _ ⇒ some_fixed_sfs
satisfies it for any single sfs. All three systems (Lean 4, Coq,
Isabelle) had the same incorrect statement.
The 2026-03-08 / 2026-04-03 fix replaced it with obliterate_not_injective:
theorem obliterate_not_injective (p : Path) :
∃ sfs1 sfs2, sfs1 ≠ sfs2 ∧ obliterate p sfs1 = obliterate p sfs2This is the correct formalisation of "information loss": two distinct starting states are made indistinguishable. Recovery is therefore not just unimplemented — it is impossible by any function.
Proven via three Lean 4 auxiliary lemmas (the "storage-equalisation chain"):
-
overwriteBlock_determined_by_shape— output block depends only on(block_id, length, pattern), not the original content. -
overwritePathBlocks_storage_eq— after one overwrite pass with a given pattern, mapped blocks are byte-identical between any two starting states that share(mapping, geometry). -
multiPassOverwrite_congr— subsequent passes operate on equal inputs and remain equal.
The same proof was then ported to Coq (full statement) and Agda
(stated; underlying lemmas live in proofs/lean4/RMOOperations.lean as
the canonical source of truth).
Lean 4’s obliterate_not_injective was strengthened during the 2026-03-22
session with two extra hypotheses:
-
hmapped— mapped blocks ofsfs1andsfs2have the sameblock_idandlength. -
hlen— the pattern list is non-empty.
Without these, two filesystems can have different mappings and remain
distinguishable. The strengthening makes the theorem statable and
provable; downstream consumers (e.g. the Rust obliterate command’s
contract in proof_refs.rs) cite the strengthened form.
-
mkdir_rmdir_reversible— the "Hello World" of valence-shell. Proven in all 5 assistants. The forward direction (mkdirthenrmdir) works in every model because the precondition¬ path_exists p fsforces the entry to have beenNoneoriginally, sormdir(= set toNone) restores it. -
rmdir_mkdir_reversible(the reverse) is the problem child — only works under the perms assumption. Seesingle_op_reversibleOpRmdir branch — model gap. -
create_delete_file_reversible/delete_create_file_reversible— same pattern, lifted to files. Proven via the samefs_updatemachinery.
-
writeFileReversible— writing contentcafter capturing the prior statec0and restoringc0is the identity. Proven in 5 assistants via thecontent-restore-lemma+just-injectivechain (Agda) andString.toList_append+List.take_left(Lean 4). -
captureRestoreIdentity—restore(capture(fs)) = fsfor anyfs. This is the heart of thecheckpoint/restoreuser-facing command; Lean 4 has the full proof, Agda carries a proof sketch with funext.
-
copy_file_reversible—delete(copy(p, q, fs)) = fswhenqwas empty infs. The Coq proof usesdestruct (fs p)case split; the Agda proof was rewritten from scratch in the 2026-04-03 closure session (10{!!}holes filled) using the correctFilesystemModelprimitives. -
move_reversible— same shape, proven across all systems. The Agda version uses funext + pointwise case analysis onfsUpdate.
-
symlink_unlink_reversible— proven via thenot-exists-is-nothinghelper, which translates "the target path was unmapped" into thefs target = nothingshape required by the model. Symlink resolution itself is not formalised yet (see Open frontier).
The chmod/chown family is the most uniformly-proven slice (8 theorems × 5 systems = 40 proven instances, zero gaps).
The non-obvious theorem here is chmod_chown_commute: at the same
path, chmod and chown produce the same final node regardless of order.
This relies on permissions and owner being independent fields of
FSNode, which is true in the abstract model but is a modelling
assumption relative to real POSIX (where some umask interactions can
fold the operations together).
proofs/coq/posix_errors.v lifts each filesystem op into the
option (Filesystem + ErrorCode) monad: instead of mkdir : Path →
Filesystem → Filesystem, you get safe_mkdir : Path → Filesystem →
Result Filesystem (EEXIST | ENOENT | EACCES | ENOTEMPTY). The
safe_mkdir_rmdir_reversible theorem then proves that the unwrapped
result, when both succeed, satisfies the underlying reversibility.
The 2026-04-12 session closed 5 of 6 decidability axioms in this file
by giving constructive proofs (matching paths under String.eqb,
checking is_directory against the case split on the FSNode tag,
etc.). The single remaining axiom, is_empty_dir_dec, is justified —
see is_empty_dir_dec — justified.
There are exactly two load-bearing assumptions in valence-shell as of 2026-06-01. Both are explicit in the source; both have a documented escape hatch.
| Field | Value |
|---|---|
Name |
|
File |
|
Statement |
|
Nature |
Standard axiom in intensional Martin-Löf type theory; provable in cubical Agda. |
Why |
Every Agda proof of equality between |
Escape hatch |
Switch |
Cost of removal |
Low — |
Provers without this axiom |
Coq (uses |
Print-Assumptions impact |
Every Agda theorem about |
| Field | Value |
|---|---|
Name |
The unnamed |
File |
|
Statement (informal) |
For an arbitrary |
Nature |
Model gap, not a missing induction. |
Why it slipped |
The forward direction ( |
Escape hatch A (smallest) |
Strengthen |
Escape hatch B (medium) |
Add an |
Escape hatch C (full closure) |
Change |
Provers without this gap |
Lean 4 (the |
Print-Assumptions impact |
Currently silent because |
| Field | Value |
|---|---|
Name |
|
File |
|
Statement |
|
Nature |
Justified axiom. |
Why retained |
The 2026-04-12 session converted 5 of 6 sibling decidability axioms into constructive lemmas. This one resists because the path space is unbounded. |
Escape hatch |
Migrate |
Cost of removal |
High — touches every operation definition and re-proves every theorem. Not currently planned. |
Provers without this axiom |
Lean 4, Agda, Isabelle, Mizar — all use either a finite-key model or are willing to take the same axiom. |
The directory proofs/idris2/ contains the Idris2 ABI-style mirror of
the proof suite — type-stated in the dependently-typed sense, with the
intent that the function definition itself carries the proof obligation
(rather than the Coq/Lean style of separate Proof. … Qed. blocks).
As of 2026-07-01 (issue #151 root) this layer is fully proven, not just
stated: 0 holes across the 4 files. grep -rohE
'\?[A-Za-z_]' proofs/idris2/src --include='.idr' returns 0, and
the package builds under --total, so every function is a total, machine-checked
proof. The closure added no new axioms — the two primitive-eq axioms in
Filesystem.Axioms are the only assumptions.
| Theorem | Closure |
|---|---|
|
|
|
|
|
canonical-form precondition + |
|
|
|
restated over |
|
canonical-form precondition + |
|
induction over a |
|
genuine per-step reversibility hypotheses (the |
|
|
|
induction over an |
|
redesigned to non-injectivity (information loss); the prior |
|
closed in earlier sessions. |
Where a stated theorem was a genuine non-theorem in the ordered-list model
(order-sensitive =, or a refutable "no recovery" shape), its signature was
redesigned to the true statement rather than closed with believe_me, following
the #60/#61/#119 precedent. The fully-general restore-cluster theorems (arbitrary
in-list position with uniqueness) would need a NoDupKeys model strengthening;
that remains the one honest frontier item for this layer.
The Idris2 layer is the canonical ABI-level expression of the
verification (per memory [Zig=APIs+FFIs, Idris2=ABIs]). Closing these
holes makes the Rust FFI surface in ffi/rust/src/preconditions.rs /
verification.rs / rmo.rs provably-correct at the type level rather
than at the test level.
The five sections above describe what is proven. The directive on
2026-06-01 was: "identify every single proof that would be valuable to
do, even marginal stuff". The catalog of unstated-but-valuable theorems
lives in docs/PROOF-OPEN-FRONTIER.adoc.
Highlights:
-
Lean → Rust mechanised correspondence. The single largest gap per
CLAUDE.md. Currently ~85% confidence via property tests (tests/lean4_proptest_correspondence.rs,tests/correspondence_tests.rs) but no mechanised refinement proof. Closure path: extract Lean 4 proofs to a reference implementation, then prove the Rust CLI refines the extracted code. -
Concurrency / linearizability. No proof covers two
vshinvocations modifying the same path. Open frontier. -
Crash-consistency. No theorem covers SIGKILL between begin/commit/rollback steps. The WAL/journal mechanism isn’t even modelled.
-
POSIX 2024 conformance. The current model is "POSIX-shaped" but not pinned to a specific POSIX version. POSIX 2024 added several features.
-
Parser correctness. The shell parser in
impl/rust-cli/src/parser.rshas no proof of unambiguity. Pratt-style precedence tests partly cover this empirically. -
Process substitution / pipeline / redirection semantics. None formally modelled; all currently rely on property tests.
-
Symlink resolution loops. The model treats symlinks as direct mappings; no proof of loop detection during traversal.
-
Glob complexity bound.
expand_globhas no termination/complexity proof.
The RMO obliteration proofs rest on external assumptions that cannot be discharged in any proof assistant:
-
NIST SP 800-88 — the standard for media sanitization. Stipulates that Purge-level overwrite + Destroy-level physical erasure render data unrecoverable. Cited in
proofs/idris2/src/Filesystem/RMO.idr:90as a foundational comment. -
Information-theoretic random data — overwriting with random data of length ≥ original length destroys information about the original (Shannon entropy argument).
-
Hardware physical erasure — degaussing / shredding cannot be undone by any computable function (physical-world assumption).
These are appropriate axioms for the RMO proofs — they live in the
physical world, not the formal world. They should be lifted into the
explicit registry rather than buried in ?holes.
# Coq
cd proofs/coq
coq_makefile -f _CoqProject -o Makefile && make
# Lean 4
cd proofs/lean4
lake build
# Agda
cd proofs/agda
agda --library-file=valence-shell.agda-lib FilesystemModel.agda
# Isabelle/HOL
cd proofs/isabelle
isabelle build -D .
# Mizar
cd proofs/mizar
for f in *.miz; do mizf "$f"; done
# Z3 SMT
cd proofs/z3
for f in *.smt2; do z3 "$f"; doneTo verify the assumption count, add Print Assumptions some_theorem.
to each Coq file and grep the output:
grep -A 20 "Print Assumptions" proofs/coq/*.vShould reveal exactly Coq.Logic.FunctionalExtensionality (which is the
same strength as Agda’s funext) for every theorem that goes through
function equality, and nothing else — once the admit. is closed.
-
Verdi (distributed systems in Coq) — methodological inspiration for proving sequence-level theorems via per-step lemmas.
-
Fscq (verified file system in Coq) — closest neighbour in the literature; uses a similar
Path → option FSNodemodel but with a crash-Hoare logic on top. -
CompCert (verified C compiler in Coq) — extraction precedent; valence follows the same Coq → OCaml extraction pattern (see
proofs/coq/extraction.v). -
seL4 (verified microkernel in Isabelle/HOL) — uses Sledgehammer automation, which valence’s Isabelle proofs deliberately mirror.
-
Shapiro et al., "Conflict-Free Replicated Data Types" (2011) — the
obliterate_not_injectiveproof style mirrors the non-CRDT-ness proofs in the CRDT literature. -
Buneman/Tan, "Provenance in Databases: Why, How, and Where" (2007) — the open-frontier proof "why-provenance for shell histories" is taken from this.