# Safe device detach contract (K1416–K1420)

`SafeRegistry` owns the driver binding, logical MMIO/IRQ/DMA claims, and a
bounded descriptor queue record for each attached device generation. Its
detach sequence is:

1. Stop admissions. No new descriptor may become device-owned.
2. Obtain a physical device reset acknowledgement from the transport and mark
   reset. A caller must keep DMA pages pinned until this acknowledgement.
3. Drain or cancel every outstanding descriptor. After reset, abandoned
   descriptors may be counted as cancelled; their memory is still held.
4. Mask and unregister the device IRQ, then mark IRQ detached.
5. Detach the driver binding and logical resource claims. Only after this
   success may the caller release physical DMA pages and MMIO mappings.

Every operation names an exact generation-bearing handle. A wrong phase,
stale handle, queue overflow, or early finish returns an error without changing
the full registry state. `finish_detach` requires the ordered reset, drain,
and IRQ steps and zero outstanding descriptors. Empty and fully occupied
queues use the same sequence; drain reports the number cancelled.

The model cannot manufacture a reset or IRQ witness. The guest integration
must read the real VirtIO reset/QueueReady registers and separately prove any
real IRQ deregistration and physical DMA release it claims. A model-only call
to `mark_reset` or `mark_irq_detached` is insufficient evidence of those
physical effects. Development source: `os-device-registry/src/lib.rs`.