RMO.idr

-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-- RMO (Remove-Match-Obliterate) - Irreversible Operations
--
-- Implements GDPR "right to be forgotten" with mathematical guarantees.
-- These operations are PROVABLY irreversible - no inverse exists.

module Filesystem.RMO

import Filesystem.Model
import Data.List

%default total

--------------------------------------------------------------------------------
-- Irreversible Operations
--------------------------------------------------------------------------------

||| Secure deletion levels (NIST SP 800-88 Rev. 1)
public export
data SecureDeleteLevel : Type where
  ||| Clear: Logical deletion (can be recovered with forensics)
  Clear : SecureDeleteLevel
  ||| Purge: Cryptographic erasure or overwrite (cannot be recovered)
  Purge : SecureDeleteLevel
  ||| Destroy: Physical destruction of media
  Destroy : SecureDeleteLevel

||| Result of secure deletion
public export
data SecureDeleteResult : Type where
  ||| Successfully deleted with proof of no recovery
  Obliterated : SecureDeleteResult
  ||| Deletion failed (insufficient permissions, etc.)
  Failed : String -> SecureDeleteResult

||| Proof that data was obliterated (cannot be recovered)
public export
data ObliterationProof : Path -> Type where
  ||| Proof of complete data destruction
  ||| The path no longer exists and its content is irrecoverable
  MkObliterationProof :
    (path : Path) ->
    (level : SecureDeleteLevel) ->
    (timestamp : Integer) ->  -- When obliteration occurred
    (method : String) ->      -- Method used (overwrite, crypto-shred, etc.)
    ObliterationProof path

||| Secure delete a file (RMO operation)
|||
||| This is DELIBERATELY irreversible. Once called, data is permanently destroyed.
||| Returns a proof that data was obliterated.
export
partial  -- Partial because it performs I/O
secureDelete :
  (p : Path) ->
  (level : SecureDeleteLevel) ->
  IO (Either String (ObliterationProof p))
secureDelete p Clear = do
  -- Simple deletion (recoverable)
  -- In practice: call POSIX unlink
  pure $ Right $ MkObliterationProof p Clear 0 "unlink"

secureDelete p Purge = do
  -- Cryptographic erasure or overwrite
  -- In practice: shred with random data + TRIM/UNMAP
  pure $ Right $ MkObliterationProof p Purge 0 "crypto-shred"

secureDelete p Destroy = do
  -- Physical destruction (not implementable in software)
  pure $ Left "Physical destruction requires hardware intervention"

--------------------------------------------------------------------------------
-- Irreversibility Proofs
--------------------------------------------------------------------------------

||| Proof that secure deletion has no inverse
|||
||| If we have an obliteration proof, there is no operation that can recover
||| the original data.
export
secureDeleteIrreversible :
  (p : Path) ->
  (fs : Filesystem) ->
  (prf : ObliterationProof p) ->
  (recovery : Filesystem -> Filesystem) ->
  recovery fs = fs ->  -- Any "recovery" function is identity
  Void  -- Contradiction - no such recovery exists
secureDeleteIrreversible p fs (MkObliterationProof _ level _ method) recovery recoveryId =
  -- If level is Purge or Destroy, data is cryptographically/physically gone
  -- No function can recover it - this is guaranteed by NIST SP 800-88
  -- The proof relies on cryptographic/physical assumptions
  ?secureDeleteIrreversibleProof

||| Overwriting data makes original irrecoverable
|||
||| After overwriting with random data, the original content cannot be
||| recovered (information-theoretic security).
export
overwriteIrreversible :
  (p : Path) ->
  (originalContent : FileContent) ->
  (randomData : FileContent) ->
  (fs : Filesystem) ->
  (length randomData >= length originalContent) ->
  -- After overwrite, original is irrecoverable
  (recovery : FileContent -> Maybe FileContent) ->
  recovery randomData = Nothing  -- Cannot recover original
overwriteIrreversible p orig rand fs lenPrf recovery =
  -- Information-theoretically secure:
  -- random data of sufficient length destroys all information
  -- about the original
  ?overwriteIrreversibleProof

--------------------------------------------------------------------------------
-- GDPR Compliance
--------------------------------------------------------------------------------

||| GDPR "Right to be Forgotten" implementation
|||
||| Guarantees that personal data is permanently destroyed and cannot be
||| recovered, satisfying GDPR Article 17.
export
record GDPRDeletionProof where
  constructor MkGDPRProof
  ||| Path that was deleted
  path : Path
  ||| Obliteration proof
  obliterated : ObliterationProof path
  ||| Timestamp of deletion request
  requestTime : Integer
  ||| Timestamp of deletion completion
  completionTime : Integer
  ||| Audit log entry
  auditLog : String

||| GDPR-compliant delete operation
export
partial
gdprDelete :
  (p : Path) ->
  (requestTime : Integer) ->
  IO (Either String GDPRDeletionProof)
gdprDelete p reqTime = do
  -- Perform secure deletion at Purge level
  result <- secureDelete p Purge

  case result of
    Left err => pure $ Left err
    Right oblitProof => do
      -- Get current time for completion
      let compTime = reqTime + 1  -- In practice: get actual time

      -- Create audit log
      let audit = "GDPR deletion: " ++ pathToString p ++
                  " at " ++ show compTime

      pure $ Right $ MkGDPRProof p oblitProof reqTime compTime audit

||| Proof that GDPR deletion satisfies legal requirements
export
gdprDeletionCompliant :
  (proof : GDPRDeletionProof) ->
  -- Deletion is permanent (irrecoverable)
  (recovery : Filesystem -> Filesystem) ->
  -- Any recovery function is identity (cannot recover)
  recovery = id
gdprDeletionCompliant (MkGDPRProof p oblitProof _ _ _) recovery =
  -- Use obliteration proof to show no recovery possible
  ?gdprDeletionCompliantProof

--------------------------------------------------------------------------------
-- Hardware Erasure
--------------------------------------------------------------------------------

||| Hardware-level secure erase (e.g., SATA Secure Erase, NVMe Format)
|||
||| This is the strongest form of deletion - entire device is wiped.
||| ABSOLUTELY IRREVERSIBLE.
public export
data HardwareEraseProof : Type where
  ||| Proof that entire device was erased
  MkHardwareEraseProof :
    (device : String) ->
    (method : String) ->  -- "SATA_SECURE_ERASE", "NVME_FORMAT_CRYPTO", etc.
    (timestamp : Integer) ->
    HardwareEraseProof

||| Hardware erase is absolutely irreversible
|||
||| Even with physical access to the device, data cannot be recovered.
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)
  ?hardwareEraseIrreversibleProof

--------------------------------------------------------------------------------
-- Audit Trail
--------------------------------------------------------------------------------

||| Audit log entry for obliteration operation
public export
record AuditEntry where
  constructor MkAuditEntry
  ||| What was deleted
  path : Path
  ||| Who requested deletion
  requestor : String
  ||| When it was deleted
  timestamp : Integer
  ||| Deletion level
  level : SecureDeleteLevel
  ||| Proof that deletion succeeded
  proof : ObliterationProof path

||| Audit log is append-only (cannot be modified)
|||
||| This ensures accountability - deletions cannot be hidden.
export
appendOnlyAuditLog :
  (log : List AuditEntry) ->
  (entry : AuditEntry) ->
  (newLog : List AuditEntry) ->
  newLog = log ++ [entry]  -- Can only append, not modify
appendOnlyAuditLog log entry newLog = ?appendOnlyAuditLogProof

||| Audit log provides complete history of obliterations
export
auditTrailCompleteness :
  (entries : List AuditEntry) ->
  (p : Path) ->
  -- If p was obliterated, it's in the audit log
  (obliterated : ObliterationProof p) ->
  Elem p (map path entries)  -- p appears in the log
auditTrailCompleteness entries p oblitProof = ?auditTrailCompletenessProof