# Virtio split queue index contract (K1486–K1490)

The driver owns a bounded power-of-two queue of at most 1024 entries. The
published avail index and observed used index are `u16` values; every advance
uses explicit wrapping arithmetic. A head has one live generation at a time.

Descriptor and avail slot writes precede a release barrier and avail index
publication. The used index is read with acquire ordering before its used
element. The model checks an observed advance of exactly one entry and never
allows the device to complete more heads than the driver has outstanding.
The used head must name a live owner. A repeated used index and an old used
element with no new index advance are not a new completion.

Any failed publication, invalid used observation, or reset precondition leaves
the model unchanged. Reset retires outstanding heads only after device status,
queue readiness, and both ring indices are observed as zero. The generation
counter remains monotonic across reset. The local model validates arithmetic
and ownership; K1490 must bind the checks to a real QEMU queue in both boot
paths before guest acceptance.