docs: refresh state after 2026-06-02 post-merge sweep (#114)

After PRs #105 / #106 / #108 / #109 admin-merged closing #60 / #61 /
#70 / #89, several files held stale claims:

- PROOF-NEEDS.md: Idris2 listed "23 holes + 8 partial across 4 files"
  pre-#108/#109 — partial count is now 0 (10 dropped: 2 in RMO from
  IO-totality reclassification, 8 in Composition from primitive-call
  refactor). Coq admit detail rewritten: the single_op_reversible
  OpRmdir admit was Qed-closed by PR #67 (2026-06-01); 3 new admits
  surfaced from PR #55's design-gap pass tracked as #56/#57/#58.

- proofs/idris2/README.md: 21 holes -> 23 holes; "Known oracle status
  2026-06-01" -> 2026-06-02, with partial-count reference corrected.

- ROADMAP.adoc: last-refreshed bumped + post-merge attribution.

- CHANGELOG.adoc: new "Added -- 2026-06-02" section recording the
  Idris2 cleanup wave + branch sweep + #111 salvage decision.

- .machine_readable/6a2/STATE.a2ml: last-updated 2026-04-19 -> 2026-06-02
  (6-week drift); admitted 1 -> 3 with per-admit detail (#56/#57/#58);
  session-history bullets added for 2026-06-01 + 2026-06-02.

- 0-AI-MANIFEST.a2ml: last-updated bumped; tests 736 -> 757 (PR #72);
  proof-holes-remaining split into coq-admits + idris2 totals.

Issue #111 filed during the sweep for `.github/copilot/coding-agent.yml`
salvaged from the deleted `claude/safedom-res-stale-sweep` branch.

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

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -1,11 +1,11 @@
 # SPDX-License-Identifier: MPL-2.0
 # STATE.a2ml — Project state checkpoint
-# Last updated: 2026-04-19 (CRG-AUDIT-2026-04-18 closure pass: items 1+2+3+4+5+7+9+10c + FIFO race fix)
+# Last updated: 2026-06-02 (post-merge sweep — PRs #105/#106/#108/#109 closed #60/#61/#70/#89)
 
 [metadata]
 project = "valence-shell"
 version = "0.9.0"
-last-updated = "2026-04-19"
+last-updated = "2026-06-02"
 status = "active"
 
 [project-context]
@@ -31,9 +31,25 @@ tasks-completed = [
 ]
 
 [coq-proof-status]
-admitted = 1
+admitted = 3
 axioms-justified = 1
-admitted-detail = "single_op_reversible OpRmdir branch (proofs/coq/filesystem_composition.v:199): mkdir restores with default_perms, but the original directory may have had different permissions, so mkdir(rmdir(fs)) ≠ fs in general. Full reversibility requires the undo stack to preserve original node data. Known limitation of the Filesystem = Path -> option FSNode model. Pre-existing model gap, flagged in CRG-AUDIT-2026-04-18; the in-source comment at line 195-198 acknowledges it. Declaring honestly here corrects the prior `admitted = 0` claim."
+admitted-detail = """
+3 Admitted markers as of 2026-06-02 post-PR #55 design-gap surfacing:
+
+  1. mkdir_two_dirs_reversible (filesystem_composition.v:697) — non-LIFO
+     sequence reversal; not derivable from two_op_sequence_reversible as
+     stated. Tracked as #56 (restate as LIFO sequence).
+
+  2. overwrite_pass_equalizes_storage (rmo_operations.v:422) — model gap.
+     Needs Hgeom strengthening or conclusion relaxation. Tracked as #57.
+
+  3. obliterate_not_injective (rmo_operations.v:535) — downstream of #57;
+     reconnects once #57 closes. Tracked as #58.
+
+The prior single_op_reversible OpRmdir admit (declared 2026-04-19) was
+Qed-closed by PR #67 (2026-06-01) via OpMkdirWithPerms +
+OpCreateFileWithPerms constructor-variant approach — zero new axioms.
+"""
 axiom-detail = "is_empty_dir_dec: Filesystem = Path -> option FSNode is infinite-domain; universal quantification over all paths is not constructively decidable. Migration: switch to FMaps.t FSNode."
 proof-debt-items-closed = [1, 2]
 proof-debt-open = [3]
@@ -59,6 +75,8 @@ note = "Promotion to C-grade dogfooding evidence requires real daily-driver use
 # 2026-04-04: CRG-C blitz — 59 new tests, benchmarks, E2E, Zig, Elixir
 # 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.
 
 [crg]
 grade = "C"

0-AI-MANIFEST.a2ml

@@ -10,7 +10,7 @@ project = "valence-shell"
 version = "0.9.0"
 status = "Advanced research prototype — NOT production-ready"
 license = "MPL-2.0"
-last-updated = "2026-06-01"
+last-updated = "2026-06-02"
 
 # What this project IS — one-line summary; for the full statement read
 # .machine_readable/INTENT.contractile (the load-bearing artefact).
@@ -38,13 +38,16 @@ deep-audit-log-dir   = "docs/audits/"
 latest-deep-audit    = "docs/audits/2026-06-01-deep-audit.adoc"
 
 [counts-as-of-last-audit]
-# Per docs/audits/2026-06-01-deep-audit.adoc + issue #42.
+# Per docs/audits/2026-06-01-deep-audit.adoc + issue #42 + 2026-06-02 sweep.
 theorem-candidates       = 478
 proof-systems            = 6
-proof-holes-remaining    = 3       # 1 real gap + 1 justified axiom + 1 structural axiom
+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-partial-markers   = 0       # cleared 2026-06-02
 rust-source-files        = 32
 rust-loc                 = 21331
-tests-passing            = 736
+tests-passing            = 757     # +21 via PR #72 (2026-06-01)
 tests-ignored            = 14
 tests-failing            = 0
 fuzz-targets             = 7

CHANGELOG.adoc

@@ -17,6 +17,21 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Full POSIX shell compliance (subset)
 - RMO (Remove-Match-Obliterate) proofs for GDPR compliance
 
+=== Added — 2026-06-02
+
+==== Proof work
+- 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.
+
+==== 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.
+
+==== 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.
+- PROOF-NEEDS.md + `proofs/idris2/README.md` + ROADMAP.adoc refreshed to reflect zero `partial` count + 3-admit Coq state.
+
 === Added — 2026-06-01
 
 ==== Proof work

PROOF-NEEDS.md

@@ -2,7 +2,7 @@
 <!-- SPDX-License-Identifier: MPL-2.0 -->
 <!-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 
-> **Reconciled 2026-06-01.** This file used to list 7 open Agda postulates
+> **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.
 >
@@ -11,7 +11,7 @@
 > **[docs/PROOF-OPEN-FRONTIER.adoc](docs/PROOF-OPEN-FRONTIER.adoc)**
 > (every valuable but unproven theorem, with tractability classification).
 
-## Current State (2026-06-01)
+## Current State (2026-06-02)
 
 - **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
@@ -23,17 +23,19 @@
 | 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 | `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 | 23 `?holes` + 8 `partial` annotations across 4 files | `proofs/idris2/src/Filesystem/*.idr` | Type-stated, body un-discharged; `partial` is the Idris2 totality escape hatch |
+| 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 holes + `partial` markers by file:
+Idris2 holes by file (counts as of 2026-06-02):
 - `proofs/idris2/src/Filesystem/Operations.idr`: 11 holes (mkdir/rmdir, touch/rm, write, op-independence, CNO)
-- `proofs/idris2/src/Filesystem/RMO.idr`: 6 holes + 1 `partial` at line 138 (secureDelete, overwrite, GDPR, hardwareErase, audit log)
-- `proofs/idris2/src/Filesystem/Composition.idr`: 4 holes + 7 `partial` annotations at lines 84, 94, 109, 185, 192, 200, 208, 217 (sequence + composition + undo/redo; preconditions checked externally pending precondition lemmas)
-- `proofs/idris2/src/Filesystem/Model.idr`: 2 holes (equivalence sym + trans)
+- `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/Model.idr`: 3 holes (equivSym + equivTrans + equivReflProof; the last added when DecEq Path fix landed via PR #105)
 
-The `partial` annotations above are recognised by `standards/scripts/check-trusted-base.sh` as Idris2 totality escape hatches. They are enumerated here (full paths) so the trusted-base check finds them documented per estate policy (`docs/TRUSTED-BASE-REDUCTION-POLICY.adoc`). Closure path: discharge the corresponding `?hole` with the precondition lemma, then drop the `partial` annotation.
+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.
 
 ### Foundational Closure (history)
 
@@ -46,6 +48,10 @@ The `partial` annotations above are recognised by `standards/scripts/check-trust
 | 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 |
+| 2026-06-01 | `single_op_reversible` OpRmdir branch | Closed Qed via `OpMkdirWithPerms` + `OpCreateFileWithPerms` constructor-variant approach (PR #67); zero new axioms |
+| 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) |
 
 ### What Needs Proving (current, prioritised)
 
@@ -54,7 +60,7 @@ Highlights:
 
 **Tier S (foundational)**:
 1. Lean → Rust mechanised refinement
-2. Close the `single_op_reversible` admit (Coq) — Tier A overlap; tractable
+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)
 
@@ -82,15 +88,16 @@ Highlights:
 
 ### 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.
+**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.
 
 `secureDeleteNotInjective` (closes #60) and `gdprDeletionCompliant`
-(closes #61) shipped 2026-06-01 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).
+(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).

ROADMAP.adoc

@@ -16,7 +16,7 @@ replacement for bash/zsh.
 For the full honest status see `CLAUDE.md`; for caveats per claim see
 `EXPLAINME.adoc`; for proof-debt see `docs/PROOF_HOLES_AUDIT.md`.
 
-_Last refreshed: 2026-06-01 (maintenance sweep M2/M3/M4)._
+_Last refreshed: 2026-06-02 (post-merge sweep: PRs #105 #106 #108 #109 — closes #60 / #61 / #70 / #89; PR #107 dropped codeql.yml)._
 
 == v0.9.x — Stabilisation (D → C per CRG v2.0)
 

proofs/idris2/README.md

@@ -27,12 +27,12 @@ This directory contains **executable specifications** of filesystem operations w
 
 | Module | Purpose | Status | Holes |
 |--------|---------|--------|-------|
-| `Filesystem.Model` | Core types: Path, Filesystem, FSEntry | ✅ Implemented | 2 (equivalence) |
-| `Filesystem.Operations` | mkdir, rmdir, touch, rm, writeFile | ✅ Implemented | 8 (reversibility) |
+| `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.RMO` | Irreversible operations (GDPR) | ✅ Implemented | 6 (irreversibility) |
+| `Filesystem.RMO` | Irreversible operations (GDPR) | ✅ Implemented | 4 (irreversibility) |
 
-**Total**: 4 modules, 21 proof holes to fill
+**Total**: 4 modules, 23 proof holes to fill, 0 `partial` annotations (cleared 2026-06-02 via PRs #108 + #109)
 
 ### Proof Holes (TODO)
 
@@ -105,13 +105,13 @@ just build-idris2    # cd proofs/idris2 && idris2 --build valence-shell.ipkg
 just verify-idris2   # build + count distinct ?holes for regression tracking
 ```
 
-#### Known oracle status (2026-06-01)
+#### Known oracle status (2026-06-02)
 
-`build-idris2` currently fails on pre-existing issues outside #60/#61's scope:
+`build-idris2` currently fails on pre-existing issues outside the #60/#61/#89 scope:
 
-- `Filesystem/Model.idr` — `equivSym` / `equivTrans` 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 alongside the 10 partial markers).
-- `Filesystem/Composition.idr` — multiple holes pending Coq/Lean port.
+- `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.
 
 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 21 proof holes
+- [ ] Fill all 23 proof holes
 - [ ] Verify totality of all functions
 - [ ] Add property tests