docs(proof): proof narrative + open frontier + reconciled PROOF-NEEDS

Three docs that together replace the drifted proof-status story.

**docs/PROOF-NARRATIVE.adoc** — the canonical theorem-level account:
- Cross-system witness matrix (Coq / Lean 4 / Agda / Isabelle / Mizar / Z3)
  for ~42 named theorems
- Composition story: how single_op_reversible composes through
  operation_sequence_reversible to is_CNO_sequence (Absolute Zero
  connection)
- Per-area narrative: file ops, content, copy/move, symlinks, perms,
  RMO, equivalence, composition, POSIX error wrappers
- Assumption registry with explicit escape hatches:
  * `funext` (Agda) — standard intensional-TT, provable in cubical
  * `admit.` (Coq filesystem_composition.v:199) — model gap for
    `rmdir → mkdir` under non-default perms; three closure paths
    documented (strengthen `reversible`, OpMkdirWithPerms variant,
    UndoLog model)
  * `is_empty_dir_dec` (Coq) — justified, infinite-domain quantification

Adds the Idris2 ABI layer (omitted from prior audits): 23 `?holes`
across 4 files. Eleven are pure ports from Coq/Lean 4 canonical proofs;
twelve depend on either the model gap or external NIST SP 800-88 /
information-theoretic axioms (now made explicit in §10).

**docs/PROOF-OPEN-FRONTIER.adoc** — every valuable but unproven theorem,
per directive "even marginal stuff":
- Tier S (4 foundational): Lean→Rust mechanised refinement,
  close-the-admit, crash-consistency, concurrency safety
- Tier A (12 single-PR): Idris2 structural holes, glob complexity,
  Pratt-style precedence, redirection semantics, path-traversal
  containment
- Tier B (8 multi-day): POSIX 2024, subshell scoping, word splitting,
  pipeline data-flow, job control state machine, symlink loops, audit
  HMAC, MCP conformance
- Tier C (10 marginal-but-named): reverse-direction lemmas, base cases,
  CNO algebra, parent_path corollaries, well_formed lifting, lattice
  laws on path_prefix, idempotence negative theorems, transposition,
  fold equivalences
- Tier D (5 meta/process): Print Assumptions CI guard, Idris2
  --check-hole CI, cross-system name alignment, narrative
  auto-generation, witness-coverage test

**PROOF-NEEDS.md** — reconciled to current state. The old file listed
7 Agda postulates from a pre-2026-04-03 snapshot; all were closed in
that session. Updated to reflect the live assumption registry, full
closure-session history, and pointers into the new narrative.

No proof bodies changed; this PR is documentation only. The companion
proof-closure PR (strengthen `reversible` OpRmdir branch, port 11
structural Idris2 holes) will follow once the build oracle is verified
locally.

Refs #42 (proof inventory tracking issue).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

PROOF-NEEDS.md

@@ -1,45 +1,92 @@
 # PROOF-NEEDS.md
 <!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 
-## Current State
+> **Reconciled 2026-06-01.** This file used to list 7 open Agda postulates
+> from a pre-2026-04-03 snapshot — all 7 were closed during that session
+> (see `docs/PROOF_HOLES_AUDIT.md`). The actual current state below.
+>
+> Canonical detail: **[docs/PROOF-NARRATIVE.adoc](docs/PROOF-NARRATIVE.adoc)**
+> (assumption registry, cross-system witness matrix) and
+> **[docs/PROOF-OPEN-FRONTIER.adoc](docs/PROOF-OPEN-FRONTIER.adoc)**
+> (every valuable but unproven theorem, with tractability classification).
 
-- **LOC**: ~57,650
-- **Languages**: Rust, ReScript, Agda, Idris2, Zig
-- **Existing ABI proofs**: `src/abi/*.idr` plus extensive Agda proof suite (9 files in `proofs/agda/`)
-- **Dangerous patterns**:
-  - `proofs/agda/FileContentOperations.agda`: 5 `postulate`
-  - `proofs/agda/FilesystemModel.agda`: 1 `postulate`
-  - `proofs/agda/RMOOperations.agda`: 1 `postulate`
-  - `impl/mcp/src/Server.res`: 20+ `Obj.magic` in MCP tool handlers
+## Current State (2026-06-01)
 
-## What Needs Proving
+- **LOC**: ~11,000 lines of formal proof (Coq 4,500 + Lean 4 2,400 + Agda 2,250 + Isabelle 1,800)
+- **Languages**: Rust, ReScript, Agda, Idris2, Lean 4, Coq, Isabelle/HOL, Mizar, Z3, Zig
+- **Proof systems**: 6 closed-core (Coq, Lean 4, Agda, Isabelle, Mizar, Z3) + 1 ABI-stub tier (Idris2)
+- **Named theorems**: ~478 across the 7 systems (see narrative §3)
 
-### FileContentOperations Postulates (5)
-- These are in the core filesystem proof — content operations are critical for shell correctness
-- Audit each postulate: are they about byte-level I/O (acceptable axiom) or about logical properties (should be proven)?
+### Assumption Registry (live)
 
-### FilesystemModel Postulate (1)
-- Foundation postulate — if this is wrong, all downstream proofs are unsound
-- Should be the highest priority to eliminate or justify
+| Layer | Item | Location | Nature |
+|---|---|---|---|
+| Agda | `postulate funext` | `proofs/agda/FilesystemModel.agda:161-162` | Standard intensional-TT axiom; provable under `--cubical` |
+| Coq | `admit.` mid-`single_op_reversible`, OpRmdir branch | `proofs/coq/filesystem_composition.v:199` | Model gap — `mkdir` writes `default_perms`, original may have had non-default |
+| Coq | `Axiom is_empty_dir_dec` (justified) | `proofs/coq/posix_errors.v` | Infinite-domain universal quantification |
+| Idris2 | 23 `?holes` across 4 files | `proofs/idris2/src/Filesystem/*.idr` | Type-stated, body un-discharged |
 
-### RMOOperations Postulate (1)
-- Reversible Mutable Operations — the core innovation of valence-shell
-- Any unproven claim about reversibility undermines the entire system guarantee
+Idris2 holes by file:
+- `Operations.idr`: 11 holes (mkdir/rmdir, touch/rm, write, op-independence, CNO)
+- `RMO.idr`: 6 holes (secureDelete, overwrite, GDPR, hardwareErase, audit log)
+- `Composition.idr`: 4 holes (sequence + composition + undo/redo)
+- `Model.idr`: 2 holes (equivalence sym + trans)
 
-### MCP Server Obj.magic (impl/mcp/src/Server.res)
-- Every filesystem operation handler uses `Obj.magic` for JSON result construction
-- `makeToolResult` and `makeJsonResult` return type-erased values
-- Prove: MCP tool responses conform to MCP protocol schema
+### Foundational Closure (history)
 
-### Rust FFI Verification (ffi/rust/)
-- `ffi/rust/src/preconditions.rs`, `verification.rs`, `rmo.rs` — safety-critical FFI
-- Precondition checking and operation verification should have formal backing
+| Date | Session | Closed |
+|---|---|---|
+| 2026-03-08 | P5 — Core reversibility | 4 priority-1 theorems |
+| 2026-03-08 | P5 — Equivalence relations | 4 priority-2 theorems |
+| 2026-03-22 | RMO closure | `obliterate_not_injective` (Lean 4) via 3 aux lemmas |
+| 2026-04-03 | Agda closure session | All 7 Agda postulates eliminated (only `funext` remains, annotated) |
+| 2026-04-03 | ReScript closure | All 24 `Obj.magic` in `impl/mcp/src/Server.res` replaced with `toolResultToJson` |
+| 2026-04-12 | Coq well-formedness | `well_formed_ancestor_exists`, `mkdir_preserves_well_formed`, 5/6 decidability axioms proven |
+| 2026-06-01 | Narrative reconciliation | `obliterate_overwrites_all_blocks` (which PROOF_HOLES_AUDIT listed as the gap) confirmed closed; actual gap identified as model-perm gap in composition.v |
 
-## Recommended Prover
+### What Needs Proving (current, prioritised)
 
-- **Agda** (already in use — eliminate remaining 7 postulates)
-- **Idris2** for ABI layer and Rust FFI interface contracts
+See `docs/PROOF-OPEN-FRONTIER.adoc` for the full Tier-S/A/B/C/D catalogue.
+Highlights:
 
-## Priority
+**Tier S (foundational)**:
+1. Lean → Rust mechanised refinement
+2. Close the `single_op_reversible` admit (Coq) — Tier A overlap; tractable
+3. Crash-consistency for begin/commit/rollback
+4. Concurrency safety (two `vsh` invocations on shared filesystem)
 
-**HIGH** — Filesystem shell with formal reversibility guarantees. The 7 postulates in the Agda proofs are close to full verification. Eliminating them would make this a genuinely formally verified filesystem tool.
+**Tier A (single-PR, <1 day each)**:
+- Idris2: 11 of the 23 holes are purely-structural and could land in one porting PR
+- Glob expansion termination + complexity bound
+- Pratt-style precedence test corpus (POSIX shell `&&`/`||`/`!`)
+- Path-traversal containment proof (`resolve_path` cannot escape sandbox)
+
+**Tier B (multi-day)**:
+- POSIX 2024 conformance proofs per M-feature
+- Subshell `(...)` scoping
+- Word splitting under quote-context
+- Audit log HMAC signing + verification (impl + proof)
+
+### Recommended Provers
+
+- **Coq** — primary truth source for filesystem model
+- **Lean 4** — canonical RMO proofs (`obliterate_not_injective` chain)
+- **Agda** — minimum-axiom witness (eliminate funext via cubical)
+- **Idris2** — ABI-level type expression (per estate convention `Zig=APIs+FFIs, Idris2=ABIs`)
+- **Isabelle/HOL** — Sledgehammer cross-validation
+- **Mizar** — set-theoretic third opinion
+- **Z3 SMT** — counterexample search for non-existent recovery functions
+
+### Priority
+
+**HIGH** — Single Coq admit + 23 Idris2 holes are visible and closeable;
+the bigger frontier (Lean→Rust refinement, crash-consistency, concurrency)
+is real research-level work.
+
+The MAA/GDPR claims depend on `?secureDeleteIrreversibleProof`,
+`?overwriteIrreversibleProof`, and `?gdprDeletionCompliantProof` being
+discharged. Until they are, the externally-facing "formally verified"
+claim leans on the closed Coq/Lean 4 layer plus axiomatic NIST SP 800-88
+/ Shannon-entropy / physical-world assumptions which should be made
+explicit (see narrative §10).