# K1351–K1354 waitset deadline and cancellation contract

This isolated `no_std` model tracks one wait registration and one timer per
owner. A new registration gets a fresh generation token. Only the owner may
observe or consume the completion. The kernel adapter binds the owner to a live
process generation and validates a real waitset before arming this model.

At the deadline tick, a timer observation is provisional until that tick is
closed. An event stamped with the same tick wins, regardless of whether the
timer or event callback arrived first. Closing the tick without an event makes
timeout the single completion. After completion, subsequent callbacks cannot
publish another result. Consuming the result removes the registration and
invalidates its timer. Old timer callbacks, including those arriving after a
new registration occupies the slot, return `Stale` without changing state.

An event stamped after the deadline cannot win. A timer before the deadline
returns `NotDue`. Foreign owners return `Access`; stale tokens return `Stale`.
Denials preserve the full snapshot and resource count. A counter overflow
returns `Overflow` without publishing a registration.

The local gate verifies deadline-tick event precedence, timeout-only completion,
single-result consumption, resource cleanup, stale timer rejection, and an
AArch64 `no_std` compile. The K1355 guest gate must bind serial/QMP and the
same Image across direct/UEFI 256, 512, and 1024 MiB profiles. This model alone
does not establish product acceptance.