# Device resource ownership contract (K1406–K1410)

An attach request contains a physical device key, a device kind, and one or
more `ResourceRange` values. Each range has a kind (`Mmio`, `Irq`, or `Dma`),
start, and nonzero length. The exclusive interval is `[start, start + length)`;
overflow is invalid. Ranges of different kinds use separate address spaces.

The resource registry owns a fixed array of claims. Each claim names exactly
one live generation-bearing device handle. Requested ranges must not overlap
one another or any live claim of the same kind. Adjacent ranges are allowed.
Only after validation and capacity checks may the registry publish the device
and its claims. A rejected attach leaves both tables byte-for-byte unchanged.

| Operation | Result | Failure |
| --- | --- | --- |
| `attach(key, kind, ranges)` | live handle and all claims | `EmptyResources`, `InvalidRange`, `Conflict`, `Capacity`, or underlying device error; no partial ownership |
| `detach(handle)` | descriptor and all owned claims removed | underlying `StaleHandle`; no changes |
| `get(handle)` | descriptor for the exact generation | underlying `StaleHandle` |

The positive case attaches a block and a network device with disjoint MMIO,
IRQ, and DMA resources and then detaches and reattaches one of them. The
negative case requests an overlapping MMIO BAR, checks complete before/after
state equality, and confirms the existing owner still works. The registry
tracks logical claims only. Real page-table mappings, interrupt routing, DMA
pinning, and QEMU hotplug teardown need separate guest evidence at K1410 and
later steps. The development source is `os-device-registry/src/lib.rs`; an
isolated candidate may copy it into the proposed kernel runtime path.