Add proof for conformance to 2.7.7.2 section

Add the verify_spec_2_7_7_2() proof to verify that the implementation of
queue satisfies 2.7.7.2 requirement. The proof relies on whether the
EVENT_IDX feature has been negotiated. Conversely with
`test_needs_notification()` test, this proof `tests` for all possible
values of the queue structure.

Signed-off-by: Matias Ezequiel Vara Larsen <mvaralar@redhat.com>

Author: MatiasVara

virtio-queue/Cargo.toml

@@ -13,10 +13,11 @@ edition = "2021"
 test-utils = []
 
 [dependencies]
-vm-memory = { workspace = true }
+vm-memory = {  workspace = true, features = ["backend-mmap", "backend-bitmap"] }
 vmm-sys-util = { workspace = true }
 log = "0.4.17"
 virtio-bindings = { path="../virtio-bindings", version = "0.2.5" }
+libc = "0.2.161"
 
 [dev-dependencies]
 criterion = "0.6.0"

virtio-queue/src/queue.rs

@@ -273,9 +273,12 @@ impl Queue {
 #[allow(dead_code)]
 mod verification {
     use std::mem::ManuallyDrop;
+    use vm_memory::MmapRegion;
+
     use std::num::Wrapping;
+    use vm_memory::FileOffset;
 
-    use vm_memory::{FileOffset, GuestMemoryRegion, MemoryRegionAddress, MmapRegion};
+    use vm_memory::{GuestMemoryRegion, MemoryRegionAddress};
 
     use super::*;