refactor(proofs/idris2): drop misleading partial markers on RMO.idr secureDelete + gdprDelete (2 of 10 from #89)

Two of the 10 `partial` markers in #89's scope were misleading
annotations: `secureDelete` and `gdprDelete` are IO computations,
exhaust their case-splits, and never recurse. IO does not introduce
partiality in Idris2 — these are legitimately total.

Verified locally with #105's Model.idr fixes applied (post-#105 the
Idris2 build proceeds past both functions without partial-checker
complaint).

The remaining 8 partial markers all live in `Composition.idr`:
- `applyOp` / `applySequence` — partial because operations have
  preconditions that aren't represented in the type. Requires a real
  refactor to either return `Maybe Filesystem` or carry precondition
  proofs as dependent arguments.
- `execute` / `undo` / `redo` — partial because they call `applyOp`;
  cascade-cleanup as applyOp becomes total.
- `sequenceReversible` / `undoRedoIdentity` / `undoRedoComposition` —
  proof bodies with `?holes`; require closure before totality.

Per #89's resolution: gap-per-PR. The Composition.idr refactor is
substantive enough for its own track and is gated on #70's build
oracle landing (in flight as #106) so each conversion can be machine-
verified.

Closes 2 of 10 markers in #89; #89 stays open for the remaining 8.

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

Author: hyperpolymath

proofs/idris2/src/Filesystem/RMO.idr

@@ -50,8 +50,10 @@ data ObliterationProof : Path -> Type where
 |||
 ||| This is DELIBERATELY irreversible. Once called, data is permanently destroyed.
 ||| Returns a proof that data was obliterated.
+|||
+||| Total: 3 exhaustive cases on SecureDeleteLevel, no recursion. The `IO`
+||| wrapper does not introduce partiality — IO computations can be total.
 export
-partial  -- Partial because it performs I/O
 secureDelete :
   (p : Path) ->
   (level : SecureDeleteLevel) ->
@@ -135,8 +137,10 @@ record GDPRDeletionProof where
   auditLog : String
 
 ||| GDPR-compliant delete operation
+|||
+||| Total: do-block with case-split on Either, calls only total functions
+||| (secureDelete is now total). IO does not introduce partiality.
 export
-partial
 gdprDelete :
   (p : Path) ->
   (requestTime : Integer) ->