[Idris2] proof-hole inventory + closure-plan audit (17 remaining holes post-#117)

[hyperpolymath]

Now that the Idris2 build oracle is green (#106 + #112 + #113 + #117) and --total passes, the 17 remaining ?holes can be triaged honestly. Classification follows the pattern set by #60/#61 (theorem-shape redesign vs. honest closure vs. axiomatic placeholder).

A. Non-theorems as currently stated (need restate)

File	Hole	Why it cannot close
Operations.idr:242	?cnoWriteSameContentProof	Statement writeFile p c fs = fs requires ordered-list equality. writeFile is addEntry p (File c) (removeEntry p fs), which moves (p, File c) to the head — equivalent up to permutation, not equal. Restate to equiv (writeFile p c fs) fs = True or getEntry p (writeFile p c fs) = getEntry p fs.
RMO.idr:243	?appendOnlyAuditLogProof	Statement newLog = log ++ [entry] for arbitrary newLog is provably false (caller passes any newLog). Restate to (newLog = log ++ [entry]) -> isAppendOnly newLog log or remove the parameter and define appendEntry : Log -> Entry -> Log as the only mutator.

Pattern matches #60 / #61 (refuted by recovery = id / recovery = const empty). File sub-issues per redesign.

B. Tractable but non-trivial (need stdlib lemmas + Bool reasoning)

File	Hole	Closure sketch
Model.idr:215	?equivReflProof	Needs all (\x => elem x xs) xs = True. Lemma elemRefl : (x : a) -> Elem x (x :: xs) exists in stdlib; thread via all distribution.
Model.idr:222	?equivSymProof	&& commutativity on Booleans: prf : a && b = True ⊢ b && a = True. Standard Bool case-split.
Model.idr:230	?equivTransProof	elem is transitive on ⊆ (lifted to all). Induction on entries.
Composition.idr:215	?undoRedoIdentityProof	Should reduce by redo (undo (execute op state)) ≡ Just (execute op state) after unfolding undo/redo definitions. Try Refl first; if not, case-split on state.undoStack.
Composition.idr:235	?undoRedoCompositionProof	Induction on n with the >>=-chain.

Suitable as gap-per-PR.

C. Hard (ordered-list permutation / dependent-precondition cascade)

File	Hole	Why hard
Operations.idr:144	?mkdirRmdirReversibleProof	rmdir p (mkdir p fs) = fs requires p to be at head after mkdir + filter to leave entries intact. Ordered-list model bites here. May need equiv restatement.
Operations.idr:155	?rmdirMkdirReversibleProof	Same plus dependent precondition reconstruction.
Operations.idr:164	?touchRmReversibleProof	Same.
Operations.idr:176	?rmTouchReversibleProof	Same plus content reconstruction.
Operations.idr:194	?writeFileReversibleProof	Needs old-content preservation lemma.
Operations.idr:217	?operationIndependenceProof	Sibling-path independence. Requires lemma that addEntry p _ preserves MkdirPrecondition q _ when Not (p = q).
Composition.idr:125	?sequenceReversibleProof	Induction over List Operation with sequence-of-reversibles, depends on single-op reversibility (which needs equiv restatement).
Composition.idr:139	?compositionReversibleProof	Depends on single-op reversibility for op1 + op2.

Realistic plan: restate with equiv instead of =, then close.

D. Axiomatic (placeholder for physical / information-theoretic claims)

File	Hole	Notes
RMO.idr:128	?overwriteIrreversibleProof	NIST SP 800-88 / Shannon entropy assumption. Document as axiom; do not attempt closure within Idris2.
RMO.idr:213	?hardwareEraseIrreversibleProof	Hardware-level physical claim. Document as axiom.
RMO.idr:253	?auditTrailCompletenessProof	Needs audit-log invariant (isAppendOnly chain ⇒ membership). Tractable after appendOnlyAuditLog redesign (Category A above).

Plan

1. Category A: 2 sub-issues for restates (mirror [Idris2] close RMO.idr:92 secureDeleteIrreversibleProof — type signature is non-theorem (Tier-S blocker) #60/[Idris2] close RMO.idr:169 gdprDeletionCompliantProof — type signature is non-theorem (Tier-S blocker) #61 pattern). Quick land.
2. Category B: 5 gap-per-PR closures, now machine-verifiable via [infra] Establish Idris2 build oracle: build-idris2 Justfile target + verify-idris2 CI job + working stdlib provision #70's strict oracle.
3. Category C: 1 umbrella issue + restate-to-equiv design RFC. Bigger track.
4. Category D: 3 documented-axiom PRs (postulate-style — but Idris2 doesn't have postulate; use a flag like assumption-NIST-800-88 and gate via CI explicit-list).

References:

• [Idris2] close RMO.idr:92 secureDeleteIrreversibleProof — type signature is non-theorem (Tier-S blocker) #60 / [Idris2] close RMO.idr:169 gdprDeletionCompliantProof — type signature is non-theorem (Tier-S blocker) #61 (theorem-shape redesign precedent — closed via fix(proofs/idris2): redesign RMO theorems to theorem-shape-correct (closes #60 + #61) #105)
• Tier-S: #41 sub — 10 Idris2 partial markers (BLOCKED on #70) #89 (partial markers — closed via refactor(proofs/idris2): drop misleading partial markers (2 of 10 from #89) #108 + fix(proofs/idris2): close remaining 8 Composition.idr partial markers (#89) #109)
• [infra] Establish Idris2 build oracle: build-idris2 Justfile target + verify-idris2 CI job + working stdlib provision #70 (build oracle — closed via feat(ci): add Idris2 build oracle (closes #70) #106)
• ~/.claude/.../reference_idris2_0_8_0_reserved_keywords.md (proof keyword + parser gotchas)

🤖 Filed by triage sweep 2026-06-02

[hyperpolymath]

Revised Cat-B classification (post-PR #123)

While auditing the 5 Cat-B holes for parallel closure, only 1 of 5 is closeable as pure boolean algebra. The other 4 are structurally blocked on either primitive equality reflexivity or fundamental theorem-shape issues that mirror Cat-C.

Reclassification table

Hole	Original	Revised	Blocker
equivSym	Cat B	Cat B (closed via PR #123)	none — Data.Bool.andCommutative
equivRefl	Cat B	Cat D-style axiom	needs (s : String) -> (s == s) = True
equivTrans	Cat B	Cat D-style axiom + Cat C-style restate	elem-transitivity through filtered lists + primitive eq at leaves
undoRedoIdentity	Cat B	Cat C-style restate	applyOp op (applyOp (inverse op) (applyOp op fs)) ≠ applyOp op fs propositionally; needs equiv
undoRedoComposition	Cat B	Cat C-style restate	same as undoRedoIdentity

And Cat-A residual cnoWriteSameContent body has the SAME blocker — needs the equiv-membership lemma chain whose leaves require primitive eq reflexivity.

Why this matters for the Q4/Q5 planning

The pre-compact plan recommended Cat-B as the next wave (1 helper-lemma PR + 5 parallel close-PRs). That premise is incorrect: 4 of the 5 holes require a Q4 decision (axiom representation) before any closure attempt makes sense. Spinning up 5 sub-agents would mostly produce "blocked on primitive eq reflexivity" reports.

Root cause: Idris2 0.8.0 + == over primitives

Idris2's == on String and Bits8 is implemented via prim__strEq / prim__b8Eq — primitive operations whose reflexivity is not derivable in pure Idris2 0.8.0 type theory. It's only assumed true at runtime. Any proof that bottoms out at "two equal primitives compare equal" needs either:

1. An axiom — e.g., assert_total $ believe_me Refl, or a documented prim__strEqRefl : (s : String) -> (s == s) = True postulate
2. A DecEq-based equivalence — replace elem (Eq-based) with elemBy decEq-based comparison in equiv. Provable, but requires reworking equiv's definition + all call sites
3. A propositional restate — express equivalence as (p : (Path, FSEntry)) -> Elem p e1 -> Elem p e2 rather than the current Bool-returning equiv (loses computability)

Recommended split

• Cat B (revised): 1 hole — equivSym. Closed via proof(model): close equivSym via Data.Bool.andCommutative (1/5 Cat B) #123. Done.
• Cat D (revised): 2 holes — equivRefl, equivTrans. Need Q4 axiom representation.
• Cat C (revised): 3 holes — undoRedoIdentity, undoRedoComposition, cnoWriteSameContent. Need RFC (Q3) on the equiv-restate pattern.

Net effect: Cat-B is done as far as no-decision-needed closures go. Real progress on the remaining 16 holes blocks on owner decisions Q3 + Q4.

[hyperpolymath]

Reclassification finding — 2026-06-02 PM session

Closer reading during the Coq-admit-triumvirate closure pass (PR #128) showed the issue-#119 triage was over-optimistic on Cat-D and slightly off on Cat-B:

Cat-D reclassification — these are Cat-A non-theorems

File:Line	Hole	Refutation
RMO.idr:130	overwriteIrreversibleProof	recovery = Just makes the conclusion recovery randomData = Nothing false
RMO.idr:215	hardwareEraseIrreversibleProof	Any non-empty Unit -> Filesystem (e.g. \_ => empty) refutes the Void conclusion
RMO.idr:270	auditTrailCompletenessProof	entries = [] refutes the Elem p (map AuditEntry.path entries) conclusion

Recommend filing as 3 #119 sub-issues with explicit refutations + correct theorem shapes, per the #60 / #61 precedent.

Cat-B clarification — DecEq Path is NOT the unblock

The "tractable via stdlib lemmas" framing of Cat-B holes assumes a path-equality reflexivity lemma can be derived locally. It cannot — DecEq Path transitively depends on DecEq String, which itself uses primitive ==. The blocker is the same one across the entire batch.

Three closure paths, each requiring owner direction:

1. believe_me axioms for String / Bits8 reflexivity, gated by CI allow-list. Smallest change, but introduces believe_me into the proof system.
2. Path representation migration to Nat-interned identifiers. Nat == Nat IS reducible on opaque variables. Bigger migration, no believe_me.
3. Theorem-shape reformulation to use decEq-style branches instead of ==-style booleans across ~20 statements.

Until one is chosen, the equivRefl / equivTrans / cnoWriteSameContent / 4× ?XXXPrfAfter / 7× reversibility theorems are all blocked.

Detailed reclassification + frozen-hole list landed in PROOF-NEEDS.md via PR #128 (commit 824b84f).

🤖 Filed from the proof-audit pass that closed the Coq admit triumvirate (#56 / #57 / #58)