Merge branch 'main' into proofs/a12-path-traversal-containment

Author: hyperpolymath

.github/ISSUE_TEMPLATE/bug_report.md

@@ -1,12 +1,8 @@
-<!--
-SPDX-License-Identifier: MPL-2.0
-Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
--->
 ---
 name: Bug report
 about: Create a report to help us improve
-title: "[Bug]: "
-labels: 'bug, priority: unset, triage'
+title: ''
+labels: ''
 assignees: ''
 
 ---

.github/ISSUE_TEMPLATE/custom.md

@@ -1,7 +1,3 @@
-<!--
-SPDX-License-Identifier: MPL-2.0
-Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
--->
 ---
 name: Custom issue template
 about: Describe this issue template's purpose here.

.github/ISSUE_TEMPLATE/feature_request.md

@@ -1,12 +1,8 @@
-<!--
-SPDX-License-Identifier: MPL-2.0
-Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
--->
 ---
 name: Feature request
 about: Suggest an idea for this project
 title: ''
-labels: 'enhancement, priority: unset, triage'
+labels: ''
 assignees: ''
 
 ---

PROOF-NEEDS.md

@@ -2,9 +2,11 @@
 <!-- SPDX-License-Identifier: MPL-2.0 -->
 <!-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 
-> **Reconciled 2026-06-02.** 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.
+> **Reconciled 2026-06-02 (afternoon).** Earlier sweeps closed the
+> Agda postulates (2026-04-03). This pass closed the remaining 3 Coq
+> admits (#56 / #57 / #58 — see "Foundational Closure" below) and
+> reconciled the Idris2-hole inventory against the live source. The
+> actual current state below.
 >
 > Canonical detail: **[docs/PROOF-NARRATIVE.adoc](docs/PROOF-NARRATIVE.adoc)**
 > (assumption registry, cross-system witness matrix) and
@@ -23,19 +25,24 @@
 | Layer | Item | Location | Nature |
 |---|---|---|---|
 | Agda | `postulate funext` | `proofs/agda/FilesystemModel.agda:161-162` | Standard intensional-TT axiom; provable under `--cubical` |
-| Coq | `Admitted` — `mkdir_two_dirs_reversible` (non-LIFO sequence reversal) | `proofs/coq/filesystem_composition.v:697` | Tracked as #56 — needs LIFO-sequence restatement |
-| Coq | `Admitted` — `overwrite_pass_equalizes_storage` (model gap) | `proofs/coq/rmo_operations.v:422` | Tracked as #57 — needs `Hgeom` strengthening or conclusion relaxation |
-| Coq | `Admitted` — `obliterate_not_injective` (downstream of #57) | `proofs/coq/rmo_operations.v:535` | Tracked as #58 — reconnects once #57 closes |
 | Coq | `Axiom is_empty_dir_dec` (justified) | `proofs/coq/posix_errors.v` | Infinite-domain universal quantification |
-| Idris2 | 22 `?holes` across 4 files (zero `partial` annotations) | `proofs/idris2/src/Filesystem/*.idr` | Type-stated, body un-discharged; all `partial` markers cleared 2026-06-02 (PRs #108 + #109); reverseConcat closed via PR #115 |
+| Coq | (closed) `mkdir_two_dirs_reversible` | `filesystem_composition.v` | Closed via LIFO restate — only standard funext (#56 closed) |
+| Coq | (closed) `overwrite_pass_equalizes_storage` | `rmo_operations.v` | Closed via `Hgeom` strengthened with `block_overwritten` (#57 closed — zero axioms) |
+| 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 | 16 `?holes` across 4 files (zero `partial` annotations) | `proofs/idris2/src/Filesystem/*.idr` | Type-stated, body un-discharged; classification per issue #119 |
 
-Idris2 holes by file (counts as of 2026-06-02, post-#115):
-- `proofs/idris2/src/Filesystem/Operations.idr`: 11 holes (mkdir/rmdir, touch/rm, write, op-independence, CNO)
-- `proofs/idris2/src/Filesystem/RMO.idr`: 4 holes (overwrite, audit log; secureDelete + gdprDelete CLOSED via PRs #105+#108; parse fixes via #112 + #113)
-- `proofs/idris2/src/Filesystem/Composition.idr`: 4 holes (Operations.idr drive-by holes; the prior 7 `partial` markers cleared via PR #109; reverseConcat closed via PR #115)
-- `proofs/idris2/src/Filesystem/Model.idr`: 3 holes (equivSym + equivTrans + equivReflProof; the last added when DecEq Path fix landed via PR #105)
+**Idris2 holes by file (verified by grep against `proofs/idris2/src/Filesystem/*.idr`, 2026-06-02 PM):**
 
-All `partial` markers in `proofs/idris2/src/Filesystem/*.idr` were cleared 2026-06-02 (PRs #108 + #109, closing #89). The total `partial` count is now zero. Closure path for the remaining 23 holes: discharge with the precondition lemma per theorem.
+| File | Top-level proof holes | Sub-holes (clause `prf` args) |
+|---|---|---|
+| `Operations.idr` | 7 (`mkdirRmdirReversibleProof`, `rmdirMkdirReversibleProof`, `touchRmReversibleProof`, `rmTouchReversibleProof`, `writeFileReversibleProof`, `operationIndependenceProof`, `cnoWriteSameContentProof`) | 4 (`?rmdirPrfAfterMkdir`, `?mkdirPrfAfterRmdir`, `?rmPrfAfterTouch`, `?touchPrfAfterRm`) |
+| `Composition.idr` | 4 (`sequenceReversibleProof`, `compositionReversibleProof`, `undoRedoIdentityProof`, `undoRedoCompositionProof`) | 0 |
+| `Model.idr` | 2 (`equivReflProof`, `equivTransProof`; `equivSymProof` is closed via `andCommutative`) | 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.
 
 ### Foundational Closure (history)
 
@@ -53,29 +60,130 @@ All `partial` markers in `proofs/idris2/src/Filesystem/*.idr` were cleared 2026-
 | 2026-06-02 | Idris2 partial-marker sweep | All 10 `partial` annotations on `RMO.idr` + `Composition.idr` cleared (PRs #108 + #109, closing #89) |
 | 2026-06-02 | Idris2 build oracle | `idris-verification.yml` workflow + Justfile recipes shipped (PR #106, closes #70) |
 | 2026-06-02 | Idris2 0.8.0 parse fixes | `AuditEntry.proof` keyword-clash rename (PR #112); `hardwareEraseIrreversible` multi-line signature fix (PR #113); `reverseConcat` closed via `Data.List.revAppend` (PR #115) |
-
-### What Needs Proving (current, prioritised)
-
-See `docs/PROOF-OPEN-FRONTIER.adoc` for the full Tier-S/A/B/C/D catalogue.
-Highlights:
-
-**Tier S (foundational)**:
-1. Lean → Rust mechanised refinement
-2. Close the 3 remaining Coq `Admitted` markers (#56 / #57 / #58 — design-gap follow-ups of the #55 build-oracle closure)
-3. Crash-consistency for begin/commit/rollback
-4. Concurrency safety (two `vsh` invocations on shared filesystem)
-
-**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)
+| 2026-06-02 PM | Coq admit triumvirate | `mkdir_two_dirs_reversible` restated to LIFO and closed (#56); `overwrite_pass_equalizes_storage` strengthened with `block_overwritten` constraint, closed with zero new axioms (#57); `obliterate_not_injective` threaded through the strengthened lemma + `multi_pass_same_start_same_result`, closed with only standard funext (#58). Coq layer now has **zero `Admitted` markers** (only the justified `Axiom is_empty_dir_dec` remains). |
+
+### What Needs Proving (current, prioritised by tractability × value)
+
+See `docs/PROOF-OPEN-FRONTIER.adoc` for the full Tier-S/A/B/C/D
+catalogue. The list below is the **session-2026-06-02 PM** prioritised
+attack-list, reconciled against actual file state and ranked against
+prior-session findings (memory: `feedback_proven_overly_cautious_owed_pattern`
++ `reference_idris2_0_8_0_reduction_map` indicate that several
+ostensibly-tractable holes are blocked on primitive eq-reflexivity).
+
+#### Priority 1 — visible, tractable groundwork (no quick wins)
+
+**Reclassification finding (2026-06-02 PM)**: closer reading of every
+remaining hole shows there are **zero** "single-PR closeable" items left
+that don't require either (a) primitive-eq groundwork or (b)
+theorem-shape redesign. The original Cat-D classification of the 3 RMO
+holes was wrong — none of them are sound axiom shapes.
+
+**`cnoWriteSameContent`** (`Operations.idr:254`) — the signature
+restate (`equiv` instead of `=`) was already landed in a prior pass.
+The body is still blocked by primitive-eq: closure needs reasoning
+about `(q == p)` on opaque `Path` values inside `elem`, which Idris2
+0.8.0 only reduces on literals.
+
+**3 ostensibly-Cat-D RMO holes are Cat-A non-theorems-as-stated**:
+- `overwriteIrreversibleProof` (`RMO.idr:130`): conclusion
+  `recovery randomData = Nothing` is refuted by `recovery = Just`.
+  Correct shape needs "no UNIVERSAL recovery" — quantifier flip into
+  a non-existence claim with an explicit counter-witness.
+- `hardwareEraseIrreversibleProof` (`RMO.idr:215`): type
+  `HardwareEraseProof -> (Unit -> Filesystem) -> Void` is refuted by
+  any non-empty `recovery` (the function exists trivially). Correct
+  shape needs the recovery to take the post-erase state as input.
+- `auditTrailCompletenessProof` (`RMO.idr:270`): conclusion
+  `Elem p (map AuditEntry.path entries)` is refuted by `entries = []`.
+  Correct shape needs an "entry was appended" precondition naming the
+  insertion event in the log.
+
+These three should be filed as **`#119` sub-issues** with the
+non-theorem refutations, in line with the #60 / #61 precedent.
+
+**4 Operations.idr sub-holes** (`?rmdirPrfAfterMkdir`,
+`?mkdirPrfAfterRmdir`, `?rmPrfAfterTouch`, `?touchPrfAfterRm`) — same
+primitive-eq blocker as the Cat-B set above. Each requires showing
+that the post-operation precondition holds, which reduces to
+`(p == p) = True` on opaque `Path` — blocked.
+
+#### Priority 2 — primitive-eq groundwork (foundational, owner-decision required)
+
+Every remaining tractable hole reduces to a `(s == s) = True` step on
+opaque `String` or `Bits8` — Idris2 0.8.0 only reduces these on
+literals. `DecEq Path` does NOT help because it transitively depends
+on `DecEq String`, which itself depends on primitive `==`.
+
+Three closure paths, each requiring owner sign-off:
+
+1. **Add `String` / `Bits8` reflexivity axioms** — `axStringEqRefl :
+   (s : String) -> (s == s) = True := believe_me Refl`, gated by CI
+   allow-list (per the Cat-D `believe_me` pattern). Smallest change,
+   but introduces `believe_me` into the proof system which prior
+   sessions explicitly avoided.
+2. **Migrate `Path` to a structural representation** — replace
+   `String`-component paths with `Nat`-encoded interned identifiers.
+   `Nat == Nat` IS reducible on opaque values. Bigger migration but
+   no `believe_me`.
+3. **Reformulate every blocked theorem to use `decEq`-style branches**
+   rather than `==`-style booleans. Avoids touching the `Eq` instance
+   but ripples through ~20 theorem statements.
+
+Until one path is chosen, the following holes are **frozen**:
+
+- `equivReflProof` (Model.idr:216)
+- `equivTransProof` (Model.idr:244)
+- `cnoWriteSameContentProof` (Operations.idr:254)
+- 4 `?XXXPrfAfter` sub-holes in Operations.idr
+- 7 reversibility theorems in Operations.idr (mkdirRmdir, rmdirMkdir,
+  touchRm, rmTouch, writeFile, operationIndependence,
+  cnoWriteSameContent)
+
+Separately, `undoRedoIdentityProof` and `undoRedoCompositionProof`
+need a Cat-A redesign (missing `isReversible op = True` precondition;
+provably refuted for non-reversible `op`) before primitive-eq is even
+relevant.
+
+#### Priority 3 — Tier-S foundational (research-level)
+
+1. **Lean → Rust mechanised refinement** (F-1) — biggest verification
+   gap; today's link is property tests at ~85% confidence. Tractable
+   slice: `mkdir` + `rmdir` only, ~1 week.
+2. **Crash-consistency for begin/commit/rollback** (F-3) — gated on
+   modelling `Filesystem × UndoLog` first.
+3. **Concurrency safety** (F-4) — Iris-in-Coq is the strongest match.
+
+#### Priority 4 — Tier-A single-PR proofs from the frontier
+
+These are independent of the proof-hole inventory and can land any time:
+
+- Glob expansion termination + complexity bound (A-6)
+- Pratt-style short-circuit `&&`/`||` precedence proof (A-8)
+- Quote-context preservation matrix (A-11)
+- Path traversal containment lemma (A-12, regression-guard for the
+  2026-02-12 audit fix)
+- Pipe associativity property test → Lean lemma (A-9)
+
+#### Priority 5 — Tier-B multi-day
+
+POSIX-2024 per-M-feature (B-1), Subshell scoping (B-2), Word splitting
+under quote-context (B-3), Pipeline data-flow (B-4), Job-control state
+machine (B-5), Symlink-loop detection (B-6), Audit-log HMAC (B-7),
+MCP-response conformance (B-8).
+
+#### Priority 6 — Tier-C marginal-but-named
+
+Ten items in `docs/PROOF-OPEN-FRONTIER.adoc§Tier-C`. Each is minutes to
+state and seconds to check; cumulative effect is a much harder system
+to regress.
+
+#### Priority 7 — Tier-D tooling
+
+`Print Assumptions` CI guard (D-1, load-bearing — without it any
+re-introduced admit is silent drift), Idris2 `--check-hole` CI (D-2),
+cross-system theorem-name alignment (D-3), proof-narrative
+auto-generation (D-4), witness-coverage compile-time test (D-5).
 
 ### Recommended Provers
 
@@ -87,18 +195,35 @@ Highlights:
 - **Mizar** — set-theoretic third opinion
 - **Z3 SMT** — counterexample search for non-existent recovery functions
 
-### Priority
+### Priority Summary
+
+**HIGH (closeable now)** — Idris2 Cat-A redesigns (`cnoWriteSameContentProof`)
++ Cat-D axiomatic markers (3 RMO physical claims) — both are
+single-PR.
+
+**MEDIUM (needs infrastructure)** — the 4 ostensibly-Cat-B holes
+(equivRefl/Trans + undoRedoIdentity/Composition) are blocked on
+primitive-eq reflexivity OR theorem-shape redesign. Closure needs (a)
+a `Path`-equality reflexivity lemma + threading, or (b) a model
+migration sidestepping primitive `==`. Filing under #119 reclassified.
 
-**HIGH** — 3 Coq `Admitted` markers (#56/#57/#58) + 23 Idris2 holes are
-visible and closeable; the bigger frontier (Lean→Rust refinement,
-crash-consistency, concurrency) is real research-level work.
+**LOW BUT BLOCKING THE BIG CLAIMS** — Lean→Rust mechanised refinement,
+crash-consistency under WAL/undo-log model, concurrency safety. These
+are research-level work; the bigger frontier is real.
 
 `secureDeleteNotInjective` (closes #60) and `gdprDeletionCompliant`
 (closes #61) shipped 2026-06-02 via PR #105 with corrected theorem
-shapes: the prior `?secureDeleteIrreversibleProof` /
-`?gdprDeletionCompliantProof` holes had non-theorem signatures
-(refutable by `recovery = id` / `recovery = const empty` respectively)
-and have been redesigned. The MAA/GDPR claims now rest on these closed
-theorems plus `?overwriteIrreversibleProof` (still open) and axiomatic
-NIST SP 800-88 / Shannon-entropy / physical-world assumptions which
-should be made explicit (see narrative §10).
+shapes (the prior holes had non-theorem signatures refutable by
+`recovery = id` / `recovery = const empty`). The MAA/GDPR claims now
+rest on these closed theorems plus `?overwriteIrreversibleProof`
+(still open as Cat-D placeholder) and axiomatic NIST SP 800-88 /
+Shannon-entropy / physical-world assumptions which should be made
+explicit (see narrative §10).
+
+The three Coq admits (#56 / #57 / #58) closed in the 2026-06-02 PM
+session bring the Coq layer to **zero `Admitted` markers** — only the
+single justified `Axiom is_empty_dir_dec` remains. `obliterate_not_injective`
+— the formal grounding for the "mathematically irreversible secure
+deletion" marketing claim — is now soundly proven (under the
+strengthened `block_overwritten`-aware geometry hypothesis, which is
+trivially satisfied for first-time obliteration).

proofs/coq/filesystem_composition.v

@@ -669,32 +669,41 @@ Proof.
       exists pqnode. exact Hpqnode.
 Qed.
 
-(** Two-directory creation example.
-
-    NOTE (model gap, 2026-06-01): As stated, this example reverses
-    [mkdir p1; mkdir p2] with [rmdir p1] applied BEFORE [rmdir p2]
-    (reading the nested [apply_op] inside-out). That is not the LIFO
-    sequence-reversal that [operation_sequence_reversible] proves,
-    which would be [rmdir p2; rmdir p1]. The example as written is
-    not provable from [two_op_sequence_reversible] without further
-    well-formedness preservation lemmas on [rmdir]. Admitted pending
-    follow-up: either restate to LIFO order, or prove the non-LIFO
-    variant under stronger preconditions. See
-    [docs/PROOF-OPEN-FRONTIER.adoc] for closure paths. *)
+(** Two-directory creation example — restated to LIFO sequence order.
+
+    The earlier statement reversed [mkdir p1; mkdir p2] with [rmdir p1]
+    applied BEFORE [rmdir p2] (FIFO order), which is not derivable from
+    [two_op_sequence_reversible] (which proves the LIFO case). Restated
+    here so the OUTER rmdir undoes the FIRST mkdir, matching the LIFO
+    discipline that the general theorem establishes.
+
+    Closes #56.  See [docs/PROOF-OPEN-FRONTIER.adoc] for context. *)
 Example mkdir_two_dirs_reversible :
   forall p1 p2 fs,
     p1 <> p2 ->
     well_formed fs ->
     mkdir_precondition p1 fs ->
     mkdir_precondition p2 (mkdir p1 fs) ->
-    apply_op (OpRmdir p2)
-      (apply_op (OpRmdir p1)
+    apply_op (OpRmdir p1)
+      (apply_op (OpRmdir p2)
         (apply_op (OpMkdir p2)
           (apply_op (OpMkdir p1) fs))) = fs.
 Proof.
-  (* Admitted: non-LIFO sequence-reversal — not derivable from
-     two_op_sequence_reversible as stated; needs design fix. *)
-Admitted.
+  intros p1 p2 fs Hneq Hwf Hpre1 Hpre2.
+  pose proof (two_op_sequence_reversible (OpMkdir p1) (OpMkdir p2) fs) as Hseq.
+  simpl in Hseq.
+  apply Hseq.
+  - (* reversible (OpMkdir p1) fs *)
+    unfold reversible. split.
+    + simpl. exact Hpre1.
+    + simpl. apply rmdir_precondition_after_mkdir; assumption.
+  - (* reversible (OpMkdir p2) (apply_op (OpMkdir p1) fs) *)
+    unfold reversible. split.
+    + simpl. exact Hpre2.
+    + simpl.
+      apply rmdir_precondition_after_mkdir;
+        [apply mkdir_preserves_well_formed; assumption | exact Hpre2].
+Qed.
 
 (** * Composition Preservation *)