# workgroup.queue_priority
`workgroup.queue_priority` is a Category C bounded max-priority queue backed by
a binary heap in workgroup SRAM. It exposes `push(value, priority)`, `pop_max()`,
and `peek_max()` for `u32` payloads and priorities.
The WGSL lowering stores heap values and priorities in `var<workgroup>` arrays.
Push reserves the next heap slot with an atomic length increment, then performs
sift-up. `pop_max` removes the root, moves the last element to the root, and
performs sift-down. The command stream is uniform across lanes and synchronized
after every operation.
Algebraic laws:
- `PriorityQueuePopMaxReturnsMaximumPriority`: `pop_max` returns an item whose
priority is greater than or equal to every remaining item.
- `PriorityQueuePeekDoesNotMutate`: repeated `peek_max` calls return the same
item and preserve `len()`.
- `BoundedCapacity`: push beyond capacity returns overflow and preserves the
existing heap.