Tier-S: #41 sub — 10 Idris2 partial markers (BLOCKED on #70) #89

Scope (sub-issue of #41 Phase 4)

Convert 10 Idris2 partial markers in proofs/idris2/src/Filesystem/ to totality-checked definitions.

Status

Blocked on #70 (Idris2 build oracle infra: Justfile target + CI job + stdlib provision). Without local rebuilds working, each partial → total conversion can't be machine-verified.

Most are tractable per estate experience — compare proven-stack patterns where assert_total is rarely needed and inductive case-split is enough.

Resolution

After #70 lands:

1. Per-marker PR (~10 PRs).
2. Use Coq's Operation inductive case-split pattern (proven on proofs(coq): close single_op_reversible OpRmdir branch via OpMkdirWithPerms variant #67) where applicable.
3. Each PR verifies via idris2 --check (run from [infra] Establish Idris2 build oracle: build-idris2 Justfile target + verify-idris2 CI job + working stdlib provision #70's Justfile target).

References

• Parent: Seam walk: 3 prod panics + 10 unreachables + 28 TODOs + 6 proof holes (audit 2026-06-01) #41
• Blocker: [infra] Establish Idris2 build oracle: build-idris2 Justfile target + verify-idris2 CI job + working stdlib provision #70 Idris2 build oracle infra