# Device registry identity contract (K1401–K1405)

The registry owns a bounded table of **logical** device descriptors. A physical
key is a transport and location pair: an MMIO base or a PCI BDF. A descriptor
also records whether the device is a block or network device. Neither a key nor
a slot number alone is a usable device handle.

The source of the development model is `os-device-registry/src/lib.rs`. The
isolated K1405 candidate copies it into `kernel/src/runtime/device_registry.rs`.
The canonical product kernel source inventory stays frozen until an integrated
product release is authorized and measured.

| Operation | Input | Success | Error and state |
| --- | --- | --- | --- |
| `attach` | physical key, kind | active handle `{slot, generation}` | `AlreadyAttached`, `Full`, or `GenerationExhausted`; table unchanged |
| `get` | handle | descriptor for that exact generation | `StaleHandle`; table unchanged |
| `detach` | handle | removed descriptor, slot vacant | `StaleHandle`; table unchanged |

A slot starts at generation zero. Each successful `attach` increments its
generation before publishing the descriptor. `detach` preserves that generation.
Reusing a vacant slot, including with the same physical key, increments it
again. Generation wrap is forbidden: a slot at `u64::MAX` is retired. Thus an
old handle cannot regain authority after detach and reattach. A duplicate
physical key cannot be attached while it is active, regardless of kind.

The registry owns only descriptors and generation state at this stage. The
transport driver remains responsible for MMIO mapping, DMA, IRQ, and physical
resource teardown. K1405 may demonstrate a guest attach/detach sequence; it
does not by itself prove physical hotplug, driver teardown, or product Image
integration. The positive case uses one block and one network descriptor. The
negative case rejects an old handle and compares complete state before and
after each rejected operation, then confirms a healthy live handle still works.