fix(proofs/idris2): RMO.idr hardwareEraseIrreversible single-line signature (parse fix)

The pre-existing multi-line signature

    hardwareEraseIrreversible :
      (proof : HardwareEraseProof) ->
      -- No recovery function exists
      (recovery : () -> Filesystem) ->
      Void

failed to parse under Idris2 0.8.0 with "Expected a type declaration"
at the trailing colon of `hardwareEraseIrreversible :`. Sanity check
(replacing the body with `hardwareEraseIrreversible : Bool`) confirmed
the parser proceeded past the declaration, isolating the failure to
this specific multi-line shape.

Suspected trigger: the combination of a `--` line comment inside the
type signature plus a `() -> ...` parameter, which the 0.8.0 parser
mis-recovers from. The single-line signature avoids both potential
triggers and parses cleanly. Same semantics:

    hardwareEraseIrreversible :
      HardwareEraseProof -> (Unit -> Filesystem) -> Void

Switched `()` to `Unit` to be explicit (both denote the same type;
`Unit` is the more conventional form for a parameter type). The body
is unchanged (still `?hardwareEraseIrreversibleProof` — separate proof
debt tracked under #89's parked sub-markers).

Verified locally: `idris2 --build` now proceeds past
`hardwareEraseIrreversible`. The next pre-existing parse error is at
the `AuditEntry` record's dependent `proof : ObliterationProof path`
field (separate sub-issue, addressed in parallel).

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

Author: hyperpolymath

proofs/idris2/src/Filesystem/RMO.idr

@@ -203,19 +203,13 @@ data HardwareEraseProof : Type where
     (timestamp : Integer) ->
     HardwareEraseProof
 
-||| Hardware erase is absolutely irreversible
-|||
+||| Hardware erase is absolutely irreversible.
 ||| Even with physical access to the device, data cannot be recovered.
+||| The recovery function is parameterised by `Unit` so it represents
+||| any nullary recovery procedure ("just try and reconstruct").
 export
-hardwareEraseIrreversible :
-  (proof : HardwareEraseProof) ->
-  -- No recovery function exists
-  (recovery : () -> Filesystem) ->
-  Void
-hardwareEraseIrreversible (MkHardwareEraseProof device method ts) recovery =
-  -- Physical impossibility: data is gone at the hardware level
-  -- Magnetic domains/flash cells are reset
-  -- This is guaranteed by hardware specifications (NIST SP 800-88 Purge/Destroy)
+hardwareEraseIrreversible : HardwareEraseProof -> (Unit -> Filesystem) -> Void
+hardwareEraseIrreversible (MkHardwareEraseProof _ _ _) _ =
   ?hardwareEraseIrreversibleProof
 
 --------------------------------------------------------------------------------