Tier-S: #45 Frontier 4 — GDPR / RMO completeness theory (BLOCKED on #60, #61)

[hyperpolymath]

Scope (sub-issue of #45 Frontier 4)

GDPR / RMO completeness — the highest-leverage theory gap. RMO operations claim mathematical irreversibility but the formal layer doesn't model physical-layer recoverability.

Theorem targets

• obliterate_implies_no_filesystem_recovery — physical-layer claim, requires modelling block layer / SSD wear-levelling / journal
• obliterate_resists_forensic_undelete — explicit threat model: file-carving from raw disk? Journal-replay? Inode reuse?
• gdpr_audit_trail_completeness — append-only audit log (now real after feat(rust-cli): secure_delete + audit_log real impls + typed-error refactor + 15-25 prop-tests #72) needs forall delete_op, exists audit_record proof
• right_to_be_forgotten_temporal_bound — within how many ms must obliterate complete? Per GDPR Art. 17 "reasonable timeliness"

Theory frontier

NIST 800-88 Clear/Purge/Destroy physical semantics — currently modelled only as logical "overwrite then unlink".

Resolution

1. Prerequisite: [Idris2] close RMO.idr:92 secureDeleteIrreversibleProof — type signature is non-theorem (Tier-S blocker) #60 and [Idris2] close RMO.idr:169 gdprDeletionCompliantProof — type signature is non-theorem (Tier-S blocker) #61 (RMO.idr theorem-shape redesigns) — these unblock the Idris2 side.
2. After approval: design doc with explicit threat model.
3. Theorem in Lean 4 + Idris2 (cross-system mirror per estate [Proofs MUST check + cross-doc echo-types] directive).
4. Practice gaps from Filesystem-theory + practice gap analysis (POSIX 2024, atomicity, crash-consistency) #45 (RMO/GDPR cluster): physical-layer test harness, journal-aware mode, wear-levelling check.

References

• Parent: Filesystem-theory + practice gap analysis (POSIX 2024, atomicity, crash-consistency) #45 Frontier 4
• Blockers: [Idris2] close RMO.idr:92 secureDeleteIrreversibleProof — type signature is non-theorem (Tier-S blocker) #60, [Idris2] close RMO.idr:169 gdprDeletionCompliantProof — type signature is non-theorem (Tier-S blocker) #61

[hyperpolymath]

Status correction: this issue's blockers #60 and #61 are both CLOSED (Idris2 RMO non-theorem signatures resolved), so the GDPR/RMO completeness-theory frontier is unblocked.

Next gate is a scoping decision (D4 in the production charter, PR pending): ship RMO in v1.0 as best-effort overwrite + proven audit residue with the hardware boundary documented per #66/#130, or drop GDPR claims from v1.0 entirely. Implementation work should start only after that call.

🤖 Generated with Claude Code