duplicate ids in used ring

TL;DR: The virtio spec does not consider duplicate entries (IDs) in the used
ring. Should this case be promoted to undefined behaviour [1] in the spec?

Background: I am developing proofs that the rust-vmm/virtio-queue [2]
implementation meets the virtio spec. I noticed that the spec does not state
anything about queue behaviour when a device adds a 
descriptor_table_index ID to
the used ring that is already present. As a result, implementations diverge:

* QEMU (with VIRTIO_F_IN_ORDER): The queue enforces a uniqueness invariant —
only one copy of an element may exist in the ring. If a duplicate is 
added, QEMU
overwrites the matching element with the new length [3].

* QEMU (with VIRTIO_F_RING_PACKED or split): The implementation assumes the
device will not add duplicates, and correctness relies on the device [4].

Problem: For packed and split queues, the implementation implicitly 
expects the
device to uphold the uniqueness invariant. For in-order queues, uniqueness
emerges implicitly from ordering. From a device developer’s perspective, 
it is
not clear that duplicates must never be inserted into the used ring. Since
implementations differ, the invariant is not consistently enforced, making
device conformance difficult to check.

Proposed solution: The spec could explicitly state that breaking the 
uniqueness
invariant is undefined behaviour. This mirrors the ISO C standard’s 
practice of
using "undefined behaviour" to signal obligations developers must 
uphold. The
term is widely understood by systems developers and would make expectations
clear.

```
Example change (to section 2.7.8 The Virtqueue Used Ring):
   ...
   Adding an index into the used ring when a virtq_used_elem entry with 
the same
   id already exists and has not yet been read by the driver results in 
undefined
   behaviour.
```

Looking forward to your thoughts.

Siddharth

[1] https://en.cppreference.com/w/c/language/behavior.html [2]
https://github.com/rust-vmm/vm-virtio [3]
https://github.com/qemu/qemu/blob/master/hw/virtio/virtio.c#L938 [4]
https://github.com/qemu/qemu/blob/5836af0783213b9355a6bbf85d9e6bc4c9c9363f/hw/net/virtio-net.c#L1977