refactor(proofs/idris2): drop misleading partial markers (2 of 10 from #89)

[hyperpolymath]

Summary

Partial closure of #89 (10 Idris2 partial markers). The two markers in `RMO.idr` are misleading annotations — `secureDelete` and `gdprDelete` are IO computations that exhaust their case-splits and never recurse. IO does not introduce partiality in Idris2 — these are legitimately total. Dropping the `partial` keyword.

Closes 2 of 10

File	Function	Reason it was marked partial	New status
RMO.idr:54	`secureDelete`	Comment said "Partial because it performs I/O" — but IO does not introduce partiality	TOTAL
RMO.idr:139	`gdprDelete`	(No comment) — but the body is a do-block with exhaustive case-split	TOTAL

What remains (8 markers, all in Composition.idr)

`applyOp` / `applySequence` / `execute` / `undo` / `redo` / `sequenceReversible` / `undoRedoIdentity` / `undoRedoComposition`. These require a real refactor: `applyOp` returns `Filesystem` instead of `Maybe Filesystem`, so operations with unmet preconditions can't be made total without either changing the return type (cascading downstream) or carrying precondition proofs as dependent arguments. Substantive enough for its own track; gated on #70's build oracle landing (#106).

Verification

Locally verified with #105's Model.idr fixes applied:

```
$ idris2 --build proofs/idris2/valence-shell.ipkg
1/4: Building Filesystem.Model OK
2/4: Building Filesystem.RMO (passes both newly-total functions;
fails downstream on pre-existing non-theorem signatures —
#105 territory)
```

Test plan

• Both functions still emit valid IO computations
• Local build proceeds past both (no totality-checker complaint)
• CI green when stacked atop fix(proofs/idris2): redesign RMO theorems to theorem-shape-correct (closes #60 + #61) #105 + feat(ci): add Idris2 build oracle (closes #70) #106

#89 stays open for the remaining 8 markers.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 142 issues detected

Severity	Count
🔴 Critical	10
🟠 High	37
🟡 Medium	95

⚠️Action Required: Critical security issues found!

View findings

[
{
"reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
"type": "download_then_run",
"file": "lean-verification.yml",
"action": "verify_download_integrity",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
"type": "download_then_run",
"file": "rust-cli.yml",
"action": "verify_download_integrity",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in boj-build.yml",
"type": "missing_timeout_minutes",
"file": "boj-build.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in casket-pages.yml",
"type": "missing_timeout_minutes",
"file": "casket-pages.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in casket-pages.yml",
"type": "missing_timeout_minutes",
"file": "casket-pages.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in cflite_batch.yml",
"type": "missing_timeout_minutes",
"file": "cflite_batch.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in cflite_pr.yml",
"type": "missing_timeout_minutes",
"file": "cflite_pr.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in codeql.yml",
"type": "missing_timeout_minutes",
"file": "codeql.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in compilation_tests.yml",
"type": "missing_timeout_minutes",
"file": "compilation_tests.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in compilation_tests.yml",
"type": "missing_timeout_minutes",
"file": "compilation_tests.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
}
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence