docs: followup for PRs #112 / #113 / #115 merged during sweep (#116)

hyperpolymath · claude · web-flow · commit c7fe57204864 · 2026-06-02T10:53:12.000+01:00
Three additional Idris2 surgical PRs merged after the initial doc refresh (PR #114) made the just-landed counts stale: - #112: AuditEntry.proof keyword-clash rename - #113: hardwareEraseIrreversible multi-line signature parse fix - #115: reverseConcat closed via Data.List.revAppend PROOF-NEEDS.md hole count 23 -> 22; Composition.idr line entry updated; foundational-closure table extended with the three PRs. proofs/idris2/README.md table + oracle-status notes updated. State + manifest counts updated. CHANGELOG.adoc extended. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
@@ -76,7 +76,7 @@ note = "Promotion to C-grade dogfooding evidence requires real daily-driver use
 # 2026-04-12: P0 sweep — Coq layer: 1 justified Axiom (was 3 Axiom + structural bugs); Admitted not yet declared
 # 2026-04-19: .expect("TODO") anti-pattern sweep CLOSED (~512 sites); admitted=0 → admitted=1 declared; [dogfooding-status] section added; impl/rust-ffi/ deleted as duplicate; 19 per-directory READMEs landed (coverage 23% → all originally-missing addressed); Phase 4C Lean-extraction docs archived; FIFO-path race fixed; ROADMAP populated; ANCHOR + alkahest email drift fixed
 # 2026-06-01: Three-phase day — foundation (#59-#73), full sweep (#40 #47 #48 #52-#55), Option-2 (#74-#75) + license-batch SPDX sweep (#95-#102) + governance SHA-pin (#103) + changelog (#104). single_op_reversible Qed-closed (PR #67). Coq build oracle re-enabled (#55). 3 new Admitted markers surfaced → tracked as #56/#57/#58. 757 tests passing.
-# 2026-06-02: Post-merge sweep — Idris2 layer cleanup. PR #105 (RMO theorem-shape redesign, closes #60+#61), PR #106 (Idris2 build oracle, closes #70), PR #108 + #109 (10 partial markers cleared, closes #89). PR #107 dropped codeql.yml. Branches cleaned to main-only; safedom orphan branch deleted with #111 salvage decision filed.
+# 2026-06-02: Post-merge sweep — Idris2 layer cleanup. PR #105 (RMO theorem-shape redesign, closes #60+#61), PR #106 (Idris2 build oracle, closes #70), PR #108 + #109 (10 partial markers cleared, closes #89), PR #112 (AuditEntry.proof keyword-clash rename), PR #113 (hardwareEraseIrreversible signature parse fix), PR #114 (doc refresh), PR #115 (reverseConcat closed via revAppend). PR #107 dropped codeql.yml. Branches cleaned to main-only; safedom orphan branch deleted with #111 salvage decision filed. Idris2 partial count 10 → 0, hole count 21+8 → 22.
 
 [crg]
 grade = "C"
diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml
@@ -43,7 +43,7 @@ theorem-candidates       = 478
 proof-systems            = 6
 coq-admits-remaining     = 3       # #56 + #57 + #58 (3 surfaced post-#55)
 coq-axioms-justified     = 1       # is_empty_dir_dec
-idris2-holes-remaining   = 23      # was 21 + 8 partial; now 23 holes + 0 partial post-PRs #105/#108/#109
+idris2-holes-remaining   = 22      # was 21 + 8 partial; now 22 holes + 0 partial post-PRs #105/#108/#109/#115
 idris2-partial-markers   = 0       # cleared 2026-06-02
 rust-source-files        = 32
 rust-loc                 = 21331
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
@@ -23,10 +23,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Idris2: RMO theorem-shape redesigns landed via PR #105 — `secureDeleteNotInjective` (mirrors Coq `obliterate_not_injective`, closes #60) + `gdprDeletionCompliant` structural redesign (closes #61). New `removeEntryDeterminedByFilter` + `keepIfNotP` helpers in `Filesystem.Model`. Drive-by `DecEq Path` fix + `equivRefl` hole unblock the build past Model.
 - Idris2: 8 remaining `partial` markers in `Composition.idr` cleared via PR #109 — `applyOp` now calls underlying `addEntry`/`removeEntry`/`updateEntry` primitives directly. Theorem-shape fixes for `All` import, Maybe-monadic undo-redo chain, `LTE` length predicate, and reverseConcat hole. Closes #89.
 - Idris2: 2 misleading `partial` markers in `RMO.idr` (secureDelete + gdprDelete IO computations) dropped via PR #108 — IO does not introduce partiality.
-- **Total Idris2 `partial` count is now zero**, down from 10 at the start of the session.
+- **Total Idris2 `partial` count is now zero**, down from 10 at the start of the session. Hole count 21 + 8 partial → 22 + 0 partial.
+- Idris2 0.8.0 parse fixes — `AuditEntry.proof` reserved-token clash renamed to `obliterated` (PR #112); `hardwareEraseIrreversible` multi-line signature converted to single-line via `Unit` (PR #113).
+- `reverseConcat` hole closed via `Data.List.revAppend` from base stdlib (PR #115). One fewer Composition.idr hole.
 
 ==== CI/CD hardening
-- Idris2 build oracle merged via PR #106 — `idris-verification.yml` workflow + Justfile recipes (`build-idris2`, `verify-idris2`). Non-blocking initially (pre-existing build issues at `hardwareEraseIrreversible`). Closes #70.
+- Idris2 build oracle merged via PR #106 — `idris-verification.yml` workflow + Justfile recipes (`build-idris2`, `verify-idris2`). Non-blocking initially (pre-existing build issues at `hardwareEraseIrreversible` — resolved same day by PR #113). Closes #70.
 
 ==== Doc + housekeeping
 - Stale sweep: 4 `claude/issue-*` branches deleted post-merge (#105/#106/#108/#109 squash-merge cleanup) + 1 orphan `claude/safedom-res-stale-sweep` branch removed (PR #34 merged 2026-05-27; 3 subsequent campaign commits were superseded). Salvaged `.github/copilot/coding-agent.yml` decision filed as #111.
diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md
@@ -27,12 +27,12 @@
 | 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 | 23 `?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) |
+| 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 |
 
-Idris2 holes by file (counts as of 2026-06-02):
+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)
-- `proofs/idris2/src/Filesystem/Composition.idr`: 5 holes (reverseConcat + Operations.idr drive-by holes; the prior 7 `partial` markers were cleared by direct-primitive refactor in PR #109)
+- `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)
 
 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.
@@ -52,6 +52,7 @@ All `partial` markers in `proofs/idris2/src/Filesystem/*.idr` were cleared 2026-
 | 2026-06-02 | Idris2 RMO theorem-shape redesigns | `secureDeleteNotInjective` (closes #60) + `gdprDeletionCompliant` structural redesign (closes #61) via PR #105 |
 | 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)
 
diff --git a/proofs/idris2/README.md b/proofs/idris2/README.md
@@ -29,10 +29,10 @@ This directory contains **executable specifications** of filesystem operations w
 |--------|---------|--------|-------|
 | `Filesystem.Model` | Core types: Path, Filesystem, FSEntry | ✅ Implemented | 3 (equivalence) |
 | `Filesystem.Operations` | mkdir, rmdir, touch, rm, writeFile | ✅ Implemented | 11 (reversibility) |
-| `Filesystem.Composition` | Operation sequences, undo/redo | ✅ Implemented | 5 (composition) |
+| `Filesystem.Composition` | Operation sequences, undo/redo | ✅ Implemented | 4 (composition) |
 | `Filesystem.RMO` | Irreversible operations (GDPR) | ✅ Implemented | 4 (irreversibility) |
 
-**Total**: 4 modules, 23 proof holes to fill, 0 `partial` annotations (cleared 2026-06-02 via PRs #108 + #109)
+**Total**: 4 modules, 22 proof holes to fill, 0 `partial` annotations (cleared 2026-06-02 via PRs #108 + #109; reverseConcat closed via PR #115)
 
 ### Proof Holes (TODO)
 
@@ -110,8 +110,8 @@ just verify-idris2   # build + count distinct ?holes for regression tracking
 `build-idris2` currently fails on pre-existing issues outside the #60/#61/#89 scope:
 
 - `Filesystem/Model.idr` — `equivSym` / `equivTrans` / `equivReflProof` are deliberate `?holes`; trivial closure when needed.
-- `Filesystem/RMO.idr` — `hardwareEraseIrreversible`'s `() -> Filesystem` parameter has a parse issue under Idris2 0.8.0 (tracked as part of #94, the remaining practice gaps under #45). The 10 `partial` annotations previously listed in this bullet were cleared 2026-06-02 by PRs #108 + #109 (closing #89).
-- `Filesystem/Composition.idr` — 5 remaining holes pending Coq/Lean port.
+- `Filesystem/RMO.idr` — `hardwareEraseIrreversible` parse issue under Idris2 0.8.0 fixed 2026-06-02 via PR #113 (multi-line → single-line signature using `Unit`); `AuditEntry.proof` keyword-clash fixed via PR #112. The 10 `partial` annotations previously listed in this bullet were cleared 2026-06-02 by PRs #108 + #109 (closing #89).
+- `Filesystem/Composition.idr` — 4 remaining holes pending Coq/Lean port (reverseConcat closed 2026-06-02 via PR #115 using `Data.List.revAppend`).
 
 The CI job is configured non-blocking until the pre-existing parse/typecheck
 issues land. Once green, flip the final `exit 0` in `idris-verification.yml`
@@ -285,7 +285,7 @@ pub extern "C" fn vsh_mkdir_wrapper(path: *const c_char) -> c_int {
 
 ### Phase 1: Complete Proofs (Weeks 1-2)
 
-- [ ] Fill all 23 proof holes
+- [ ] Fill all 22 proof holes
 - [ ] Verify totality of all functions
 - [ ] Add property tests
 
