proofs(idris2): close all proof holes at the root (0 holes, 0 new axioms) — #151

Discharge every `?hole` in the Idris2 ABI proof layer with real, total,
machine-checked terms. `idris2 --build valence-shell.ipkg` builds green under
`--total`; `grep` for `?holes` over `proofs/idris2/src` now returns 0 (was 17).
Verified locally with a from-source Idris2 0.8.0 (Chez) toolchain.

The closure adds NO new axioms. The two believe_me-backed primitive-eq axioms in
Filesystem.Axioms remain the only assumptions (still gated by
check-idris2-believe-me.sh) — they are the irreducible primitive-String/Bits8
equality boundary. Where a stated theorem was a genuine non-theorem in the
ordered-list model, its signature was redesigned to the true statement rather
than closed with believe_me, following the #60/#61/#119 precedent.

Model.idr — new structural lemma kit (all proved): removeAbsentId,
removeAddAbsent, keepSelfFalse, lookupConsSame, getEntry/pathExists/isFile/
isDir-after-add, notExistsLookupNothing, updateEntryDeterminedByFilter,
filterIdem, updateOverwrite, updateCanonicalId, removeAddRemove, allElemSelf,
equivSwapHead, equivAddSwap. addEntry/removeEntry/updateEntry promoted to
public export so downstream modules can compute with them.

Operations.idr — touchRmReversible, mkdirRmdirReversible (rmdir applicability
made an explicit precondition; mkdir does not preclude orphan children),
rmdirMkdirReversible/rmTouchReversible/writeFileReversible (canonical-form
precondition; the restore direction is not injective in general),
operationIndependence (restated =→Equiv via equivAddSwap; the = form was a
non-theorem), cnoWriteSameContent (canonical form + equivRefl).

Composition.idr — Applicable + opInvOpId; undoRedoIdentity; compositionReversible
(vacuous isReversible=True gates replaced by genuine per-step reversibility);
sequenceReversible (induction over a new TraceReversible witness);
undoRedoComposition (induction over a new Undoable witness + Maybe-monad laws
applyNSnoc/bindAssoc/bindCong/bindRightId).

RMO.idr — overwriteIrreversible and hardwareEraseIrreversible redesigned to
non-injectivity (information loss); the prior `recovery … = Nothing` and
`… -> Void` shapes were refutable (by recovery=Just / any total recovery).

Docs/tooling: PROOF-NEEDS.md, proofs/idris2/README.md, docs/PROOF-NARRATIVE.adoc,
docs/PROOF_HOLES_AUDIT.md, CLAUDE.md and IDRIS2_AXIOMS.a2ml updated to reflect 0
holes. Fixed a pre-existing verify-idris2 recipe bug (shell `$$` = PID, not `$`)
so `just verify-idris2` reports the hole count correctly.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU

Author: claude

.machine_readable/IDRIS2_AXIOMS.a2ml

@@ -17,9 +17,21 @@
 
 @a2ml-version: "0.1"
 @registry-kind: idris2-axioms
-@updated: "2026-06-02"
+@updated: "2026-07-01"
 @policy: "Q1-C pilot, soft believe_me policy with named + gated axioms"
 
+// 2026-07-01 (issue #151 root): the entire Idris2 proof layer was closed to
+// ZERO ?holes without adding any new axioms. This registry is unchanged at two
+// entries. These two are the irreducible primitive-String/Bits8 equality
+// boundary in intensional type theory — morally identical to Idris2's own
+// `DecEq String` internals (which also rest on `believe_me`) and to Agda's
+// `postulate funext`. Eliminating them would require representing path
+// components with a non-primitive inductive type, trading a standard axiom for
+// unnatural encoding overhead; that is deliberately NOT done. Note the restore-
+// direction reversibility theorems (rmdirMkdir/rmTouch/writeFile/cnoWrite) were
+// closed with canonical-form preconditions specifically so that NO `==`→`=`
+// soundness axiom was needed.
+
 axioms:
   - name: axStringEqRefl
     location: proofs/idris2/src/Filesystem/Axioms.idr:42

CLAUDE.md

@@ -87,7 +87,7 @@ The Rust CLI is a functional interactive shell with these features:
 - 21,331 lines of Rust across 32 source files (`find impl/rust-cli/src -name '*.rs' | wc -l`; `wc -l` aggregate, measured 2026-06-01)
 - ~478 theorem candidates across 6 proof systems + Idris2 ABI layer (per issue #42 deep-audit inventory, 2026-06-01)
 - 3 proof holes remaining: 1 real gap (Coq `obliterate_overwrites_all_blocks`), 1 justified axiom (Coq `is_empty_dir_dec` — infinite-domain decidability), 1 structural axiom (Agda `funext` — standard in intensional TT) — see `docs/PROOF_HOLES_AUDIT.md`
-- Idris2 ABI layer: ~22 theorems + 2 holes + 10 partial markers (per issue #42)
+- Idris2 ABI layer: **0 proof holes** (all closed 2026-07-01, issue #151 root — builds under `--total`), 0 `partial` markers, 2 registered primitive-eq axioms (`axStringEqRefl`, `axBits8EqRefl`; gated by `.github/scripts/check-idris2-believe-me.sh`)
 - 7 fuzz targets in `impl/rust-cli/fuzz/fuzz_targets/` (parser, arith, job-spec, signal-parse, path-ops, glob-expansion, state-machine)
 
 ## Critical Issues
@@ -196,7 +196,7 @@ valence-shell/
     isabelle/           # HOL proofs (76 theorems)
     mizar/              # Set theory proofs (63 theorems)
     z3/                 # SMT proofs (125 asserts)
-    idris2/             # ABI carrier (~22 theorems, 2 holes, 10 partials)
+    idris2/             # ABI carrier (0 holes, 0 partials, 2 primitive-eq axioms)
   docs/                 # Design docs, roadmaps, PROOF_HOLES_AUDIT.md
     audits/             # Deep-audit log (per estate standards)
   .machine_readable/    # INTENT/MUST/TRUST/ADJUST contractiles + a2ml agent state

Justfile

@@ -63,8 +63,7 @@ build-idris2:
 # Verify Idris2: build then count remaining ?holes (regression signal).
 verify-idris2: build-idris2
     @echo "Counting Idris2 holes..."
-    @holes=$$(grep -rohE "\\?[a-zA-Z_][a-zA-Z0-9_']*" proofs/idris2/src/ 2>/dev/null | sort -u | wc -l); \
-        echo "  Distinct holes: $$holes"
+    @echo "  Distinct holes: $(grep -rohE --include='*.idr' '\?[a-zA-Z_][a-zA-Z0-9_]*' proofs/idris2/src 2>/dev/null | sort -u | wc -l)"
 
 # Extract Coq to OCaml
 extract:

PROOF-NEEDS.md

@@ -31,20 +31,46 @@
 | Coq | (closed) `obliterate_not_injective` | `rmo_operations.v` | Closed via threaded strengthened `Hgeom` through `multi_pass_same_start_same_result` (#58 closed — only standard funext) |
 | Idris2 | `axStringEqRefl` (primitive-eq axiom) | `proofs/idris2/src/Filesystem/Axioms.idr:42` | `believe_me`-backed; registered in `.machine_readable/IDRIS2_AXIOMS.a2ml`; CI-gated via `.github/scripts/check-idris2-believe-me.sh` (Q1-C pilot 2026-06-02 PM) |
 | Idris2 | `axBits8EqRefl` (primitive-eq axiom) | `proofs/idris2/src/Filesystem/Axioms.idr:55` | `believe_me`-backed; registered in `.machine_readable/IDRIS2_AXIOMS.a2ml`; CI-gated (same pilot) |
-| Idris2 | 14 `?holes` across 4 files (zero `partial` annotations) | `proofs/idris2/src/Filesystem/*.idr` | `equivReflProof` closed via Q1-C pilot; `equivTransProof` closed via Q5-option-3 propositional `Equiv` migration (2026-06-03); rest per #119 |
+| Idris2 | `axStringEqRefl`, `axBits8EqRefl` — **the only remaining assumptions** | `proofs/idris2/src/Filesystem/Axioms.idr` | Primitive-eq reflexivity; see "Idris2 layer fully closed" below |
 
-**Idris2 holes by file (verified by grep against `proofs/idris2/src/Filesystem/*.idr`, 2026-06-03):**
+**Idris2 holes by file — ALL CLOSED (grep against `proofs/idris2/src/Filesystem/*.idr`, 2026-07-01):**
 
 | File | Top-level proof holes | Sub-holes (clause `prf` args) |
 |---|---|---|
-| `Operations.idr` | 7 (`mkdirRmdirReversibleProof`, `rmdirMkdirReversibleProof`, `touchRmReversibleProof`, `rmTouchReversibleProof`, `writeFileReversibleProof`, `operationIndependenceProof`, `cnoWriteSameContentProof` — now propositional `Equiv` shape) | 4 (`?rmdirPrfAfterMkdir`, `?mkdirPrfAfterRmdir`, `?rmPrfAfterTouch`, `?touchPrfAfterRm`) |
-| `Composition.idr` | 4 (`sequenceReversibleProof`, `compositionReversibleProof`, `undoRedoIdentityProof`, `undoRedoCompositionProof`) | 0 |
-| `Model.idr` | 0 (`equivSym` closed via constructor-swap on the propositional form; `equivRefl` + `equivTrans` closed structurally via `Data.List.Quantifiers` Q5-option-3 migration) | 0 |
-| `RMO.idr` | 3 (`overwriteIrreversibleProof`, `hardwareEraseIrreversibleProof`, `auditTrailCompletenessProof`; `appendOnlyAuditLogProof` is closed via `Refl`) | 0 |
-
-Drift from previous PROOF-NEEDS.md tally (22 holes) to current (16 holes) is mechanical: `equivSymProof` and `appendOnlyAuditLogProof` closed silently during the 2026-06-02 morning sweep (visible by grep but the inventory text was not updated). No body changes — this paragraph reconciles the count.
-
-All `partial` markers in `proofs/idris2/src/Filesystem/*.idr` were cleared 2026-06-02 (PRs #108 + #109, closing #89). The total `partial` count is zero.
+| `Operations.idr` | 0 | 0 |
+| `Composition.idr` | 0 | 0 |
+| `Model.idr` | 0 | 0 |
+| `RMO.idr` | 0 | 0 |
+
+**Idris2 layer fully closed (2026-07-01, issue #151 root).** The 17 distinct
+`?holes` (16 tallied here plus `equivSymProof`) are all discharged with real,
+`--total`-checked terms — `grep -rohE '\?[A-Za-z_][A-Za-z0-9_]*'
+proofs/idris2/src --include='*.idr'` returns **0**. Closure added **zero new
+axioms**: where a stated theorem was a non-theorem in the ordered-list model, its
+signature was redesigned to the true statement rather than closed with
+`believe_me` (following the #60/#61/#119 precedent) —
+
+- `operationIndependence`: `=` → `Equiv` (pure permutation, `equivAddSwap`).
+- `overwriteIrreversible` / `hardwareEraseIrreversible`: redesigned to
+  non-injectivity (`updateEntryDeterminedByFilter`, `hardwareErase → empty`);
+  the prior `recovery … = Nothing` / `… -> Void` shapes were refutable.
+- `rmdirMkdir` / `rmTouch` / `writeFile` / `cnoWriteSameContent`: closed under an
+  honest canonical-form precondition (the general in-list-position version needs
+  a `NoDupKeys` model strengthening — tracked below).
+- `sequenceReversible` / `undoRedoIdentity` / `compositionReversible` /
+  `undoRedoComposition`: the vacuous `isReversible = True` / `LTE n …` premises
+  are replaced by genuine reversibility witnesses (`TraceReversible`, `Undoable`,
+  `Applicable`) and proved by induction + the `Maybe`-monad laws.
+
+The two `believe_me`-backed axioms in `Filesystem.Axioms` remain (gated by
+`.github/scripts/check-idris2-believe-me.sh`); they are the irreducible
+primitive-`String`/`Bits8` equality boundary — morally identical to Idris2's own
+`DecEq String` internals and to Agda's `postulate funext`. Eliminating them would
+require an inductive (non-primitive) component representation, which trades a
+standard axiom for unnatural encoding overhead; it is explicitly NOT done.
+
+All `partial` markers were already cleared 2026-06-02 (PRs #108 + #109). The
+total `partial` count is zero.
 
 ### Foundational Closure (history)
 

docs/PROOF-NARRATIVE.adoc

@@ -484,43 +484,37 @@ 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).
 
-In its current state, this layer is *stated, not proven*: 23 holes
-(`?proofname`) across 4 files. Each hole is a known proof obligation
-that has been registered in the type system but not yet discharged.
-
-[cols="2,1,4,2",options="header"]
+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_][A-Za-z0-9_]*' 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.
+
+[cols="2,4",options="header"]
 |===
-| File | Line | Hole name | Provable today?
-
-| `Operations.idr` | 138 | `?rmdirPrfAfterMkdir` | YES — mirror of Coq's `mkdir_rmdir_reversible`; needs `funext` equivalent + case split.
-| `Operations.idr` | 143 | `?mkdirRmdirReversibleProof` | YES — same.
-| `Operations.idr` | 153 | `?mkdirPrfAfterRmdir` | NO — same model gap as <<assumption-rmdir-perms>>.
-| `Operations.idr` | 154 | `?rmdirMkdirReversibleProof` | NO — depends on the same model gap.
-| `Operations.idr` | 162 | `?rmPrfAfterTouch` | YES — file analogue of mkdir/rmdir; clean fact.
-| `Operations.idr` | 163 | `?touchRmReversibleProof` | YES.
-| `Operations.idr` | 174 | `?touchPrfAfterRm` | YES — but suffers the *file-perms* variant of the same model gap as rmdir/mkdir.
-| `Operations.idr` | 175 | `?rmTouchReversibleProof` | YES with caveat.
-| `Operations.idr` | 186 | `?writeFileReversibleProof` | YES — Lean 4 has the canonical proof; port directly.
-| `Operations.idr` | 201 | `?operationIndependenceProof` | YES — `mkdir_preserves_other_paths` analogue.
-| `Operations.idr` | 226 | `?cnoWriteSameContentProof` | YES — `is_CNO_sequence` instance.
-| `RMO.idr` | 82 | `secureDeleteNotInjective` (was `?secureDeleteIrreversibleProof`) | CLOSED 2026-06-01 (#60) — signature redesigned to mirror Coq's `obliterate_not_injective`. The prior `recovery fs = fs -> Void` shape was a non-theorem (refuted by `recovery = id`). Closes via `removeEntryDeterminedByFilter` in `Filesystem.Model`.
-| `RMO.idr` | 112 | `?overwriteIrreversibleProof` | PARTIAL — depends on the *information-theoretic random data* assumption (random data of sufficient length destroys information about the original).
-| `RMO.idr` | 178 | `gdprDeletionCompliant` (was `?gdprDeletionCompliantProof`) | CLOSED 2026-06-01 (#61) — signature redesigned to mirror Coq's `obliterate_leaves_no_trace` shape. The prior `recovery = id` shape was a non-theorem (refuted by `recovery = const empty`). Compliance is now a structural property of the deletion record (carries an obliteration witness for the deleted path).
-| `RMO.idr` | 201 | `?hardwareEraseIrreversibleProof` | PARTIAL — depends on a *physical hardware* assumption.
-| `RMO.idr` | 231 | `?appendOnlyAuditLogProof` | YES — purely structural.
-| `RMO.idr` | 241 | `?auditTrailCompletenessProof` | YES — given the audit log invariant.
-| `Composition.idr` | 125 | `?sequenceReversibleProof` | YES — direct port of Coq's `operation_sequence_reversible` (modulo the OpRmdir gap).
-| `Composition.idr` | 139 | `?compositionReversibleProof` | YES.
-| `Composition.idr` | 213 | `?undoRedoIdentityProof` | YES — undo/redo from `vsh::commands::undo` / `redo` is the user-facing instance.
-| `Model.idr` | 182 | `?equivSymProof` | YES — equivalence relation symmetry; trivial.
-| `Model.idr` | 190 | `?equivTransProof` | YES — equivalence relation transitivity; trivial.
+| Theorem | Closure
+
+| `mkdirRmdirReversible` | `removeAddAbsent`; rmdir applicability made an explicit precondition (mkdir does not preclude orphan children).
+| `touchRmReversible` | `removeAddAbsent` + unconditional `RmPrecondition` after touch.
+| `rmdirMkdirReversible`, `rmTouchReversible` | canonical-form precondition + `cong MkFS` — the restore direction is not injective in general (a shadowed duplicate key would be lost).
+| `writeFileReversible` | `updateOverwrite` + `updateCanonicalId`.
+| `operationIndependence` | restated over `Equiv` (`equivAddSwap`); the `=` version was a non-theorem (list order differs).
+| `cnoWriteSameContent` | canonical-form precondition + `updateCanonicalId` + `equivRefl`.
+| `sequenceReversible` | induction over a `TraceReversible` witness (real per-step reversibility replaces the vacuous `isReversible = True`).
+| `compositionReversible` | genuine per-step reversibility hypotheses (the `isReversible = True` gates were vacuous).
+| `undoRedoIdentity` | `opInvOpId` + an `Applicable` precondition.
+| `undoRedoComposition` | induction over an `Undoable` witness + the `Maybe`-monad laws (`applyNSnoc`, `bindAssoc`, `bindCong`).
+| `overwriteIrreversible`, `hardwareEraseIrreversible` | redesigned to non-injectivity (information loss); the prior `recovery … = Nothing` / `… -> Void` shapes were refutable.
+| `secureDeleteNotInjective`, `gdprDeletionCompliant`, `appendOnlyAuditLog`, `auditTrailCompleteness`, `equivRefl/Sym/Trans` | closed in earlier sessions.
 |===
 
-Eleven of the 23 holes are *purely-structural* (case splits, equivalence-relation
-laws) and could land in one PR by porting from the Coq/Lean 4 canonical
-proofs. The other twelve depend on the model gap from
-<<assumption-rmdir-perms>> or on physical/cryptographic axioms from
-<<assumption-nist-800-88>>.
+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

docs/PROOF_HOLES_AUDIT.md

@@ -4,9 +4,16 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 # Proof Holes Audit - Valence Shell
 
-**Date**: 2026-04-12 (updated after P0 believe_me sweep — Coq layer)
+**Date**: 2026-07-01 (Idris2 layer closed to 0 holes — issue #151 root; prior: 2026-04-12 believe_me sweep, Coq layer)
 **Auditor**: Opus (deep audit + proof closure)
-**Total Holes**: 6 across 4 proof systems (down from 31; -2 Coq axioms proved 2026-04-12)
+**Total Holes**: 6 across the 4 closed-core proof systems tracked here (down from 31; -2 Coq axioms proved 2026-04-12)
+
+> **Idris2 ABI layer (tracked separately in `PROOF-NEEDS.md` /
+> `proofs/idris2/README.md`): 0 holes as of 2026-07-01.** All 17 `?holes` were
+> discharged with total, `--total`-checked terms and **zero new axioms**; the two
+> primitive-eq axioms in `Filesystem.Axioms` are the only remaining assumptions
+> (gated by `.github/scripts/check-idris2-believe-me.sh`). Non-theorem signatures
+> were redesigned to true statements rather than closed with `believe_me`.
 
 ## Summary