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 <[email protected]>

Author: MatiasVara

virtio-queue/Cargo.toml

@@ -13,7 +13,7 @@ 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.6" }

virtio-queue/src/queue.rs

@@ -276,9 +276,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::*;