# K1301 — typed kernel object handles

This contract applies to the native process runtime. The authoritative source
is `os-handles/src/handles.rs`; isolated development Image builds copy it to
the planned `kernel/src/runtime/handles.rs` path. The frozen root `kernel/src`
tree stays intact. The older `kernel/src/handle.rs` is a separate, two-slot
experiment.

## Inputs and ownership

The kernel supplies the live process ID, including its generation, to every
operation. A user process supplies only an opaque handle number. The kernel
creates object IDs; neither a handle nor an object ID is a memory address.
The table has a fixed capacity and one owner per live entry. A task exit
closes all entries owned by that exact process generation.

| Object kind | Kernel entry | Permitted typed operation |
| --- | --- | --- |
| File | `Object::File(id)` | `file_read` |
| Channel | `Object::Channel(id)` | `channel_send` |
| Task | `Object::Task(id)` | `task_inspect` |

Object IDs must be nonzero. In this first type phase, each entry carries the
single operation shown above; finer rights and delegation are later work.
The kernel adapter must verify that the owner and object are live before
opening. It must not use a user-provided owner or object ID to mint an entry.

## Transitions and errors

`open` checks the object ID, free capacity, and next opaque number before it
publishes one entry. On success, entry count rises by one. On any error, the
table remains byte-for-byte equivalent. `close` removes one entry only when
the number belongs to the exact owner generation. `close_owner` removes all
such entries on exit. Issued numbers increase monotonically and are never
reused. An exhausted number space fails closed.

The three typed operations are read-only lookups. Unknown, stale, foreign,
zero, and wrong-kind handles all return `BadFd` (`EBADF`, errno 9). They do
not allocate, close, transfer, or change the next number. In particular,
passing a File handle to `channel_send` returns `BadFd`; the File and healthy
Channel entries remain usable. `open` uses `InvalidObject` for zero ID,
`Full` for a full table, and `IdExhausted` for counter overflow. These
errors also leave ownership and capacity unchanged.

Positive evidence is exactly three entries, one of each kind, owned by one
live process and resolved only by its corresponding typed operation.
Negative evidence records a complete table snapshot before and after the
wrong-kind call, checks `EBADF`, then resolves the healthy Channel handle.
Local model tests do not prove guest integration; K1305 requires the same
Image to pass direct and UEFI guest profiles with serial and QMP evidence.