virtio-queue: kani proofs for virtio queue

virtio-queue/src/queue/verification.rs

@@ -459,6 +459,17 @@ impl kani::Arbitrary for ProofContext {
     }
 }
 
+/// Helper function to determine if `point` is in the wrapping range `[start, stop)`.
+fn pred_in_wrapping_range(start: Wrapping<u16>, stop: Wrapping<u16>, point: Wrapping<u16>) -> bool {
+    // Check if point is in the range [start, stop) in a wrapping manner.
+    if start <= stop {
+        start <= point && point < stop
+    } else {
+        // If start > stop, we wrap around the maximum value of u16.
+        point >= start || point < stop
+    }
+}
+
 /// # Specification (VirtIO 1.3, Section 2.7.7.2: "Device Requirements: Used Buffer Notification Suppression")
 ///
 /// Section 2.7.7.2 deals with device-to-driver notification suppression. It
@@ -468,46 +479,35 @@ impl kani::Arbitrary for ProofContext {
 /// specific number of descriptors has been processed. This is done by the
 /// driver defining a "used_event" index, which tells the device "please do not
 /// notify me until used.ring[used_event] has been written to by you".
+///
+/// This proof checks:
+//  - If event_idx is not enabled, a notification is always needed.
+//  - If event_idx is enabled, a notification is needed if the used_event index
+//    is in the wrapping range [next_used - num_added, next_used).
 #[kani::proof]
 // There are no loops anywhere, but kani really enjoys getting stuck in
 // std::ptr::drop_in_place. This is a compiler intrinsic that has a "dummy"
 // implementation in stdlib that just recursively calls itself. Kani will
 // generally unwind this recursion infinitely.
 #[kani::unwind(0)]
-fn verify_device_notification_suppression() {
-    let ProofContext {
-        mut queue,
-        memory: mem,
-    } = kani::any();
-
-    let num_added_old = queue.num_added.0;
-    let needs_notification = queue.needs_notification(&mem);
+fn verify_device_to_driver_notification() {
+    let ProofContext { mut queue, memory } = kani::any();
 
-    // event_idx_enabled equivalent to VIRTIO_F_EVENT_IDX negotiated
+    // If the event_idx_enabled is false, we always need a notification
     if !queue.event_idx_enabled {
-        // The specification here says
-        // After the device writes a descriptor index into the used ring:
-        // – If flags is 1, the device SHOULD NOT send a notification.
-        // – If flags is 0, the device MUST send a notification
-        // flags is the first field in the avail_ring_address, which we completely ignore. We
-        // always send a notification, and as there only is a SHOULD NOT, that is okay
-        assert!(needs_notification.unwrap());
+        assert!(queue.needs_notification(&memory).unwrap());
     } else {
-        // next_used - 1 is where the previous descriptor was placed
-        if Wrapping(queue.used_event(&mem, Ordering::Relaxed).unwrap())
-            == std::num::Wrapping(queue.next_used - Wrapping(1))
-            && num_added_old > 0
-        {
-            // If the idx field in the used ring (which determined where that descriptor index
-            // was placed) was equal to used_event, the device MUST send a
-            // notification.
-            assert!(needs_notification.unwrap());
-
-            kani::cover!();
-        }
-
-        // The other case is handled by a "SHOULD NOT send a notification" in the spec.
-        // So we do not care
+        // If the event_idx_enabled is true, we only need a notification if
+        // the used_event is in the range of [next_used - num_added, next_used)
+        let used_event = queue.used_event(&memory, Ordering::Relaxed).unwrap();
+        let current_used = queue.next_used;
+        let old = current_used - queue.num_added;
+        let should_notify = pred_in_wrapping_range(old, current_used, used_event);
+        assert_eq!(
+            queue.needs_notification(&memory).unwrap(), /* actual */
+            should_notify,                              /* expected */
+        );
+        assert_eq!(queue.num_added.0, 0);
     }
 }
 
@@ -565,3 +565,139 @@ fn verify_add_used() {
         kani::cover!();
     }
 }
+
+/// This proof checks that after setting the `next_used` field of the queue
+/// using `set_next_used(x)`, reading back the value of `next_used` returns the
+/// same value `x`.
+#[kani::proof]
+#[kani::unwind(0)]
+fn verify_used_ring_avail_event() {
+    let ProofContext {
+        mut queue,
+        memory: _,
+    } = kani::any();
+    let x = kani::any();
+    queue.set_next_used(x);
+    assert_eq!(x, queue.next_used.0);
+}
+
+/// # Specification (VirtIO 1.3, Section 2.7.6.1: "Driver Requirements: The Virtqueue Available Ring")
+///
+/// This proof checks that:
+/// - If there are pending entries in the avail ring (avail_idx != next_avail),
+///   `enable_notification` returns true.
+/// - If there are no pending entries (avail_idx == next_avail), it returns false.
+/// This matches the monotonicity property of the avail ring in VirtIO 1.3 Section 2.7.6.1.
+#[kani::proof]
+#[kani::unwind(0)]
+fn verify_enable_driver_to_device_notification() {
+    let ProofContext { mut queue, memory } = kani::any();
+
+    // The enable_notification method sets notification to true and returns
+    //   - true, if there are pending entries in the `idx` field of the
+    //     avail ring
+    //   - false, if there are no pending entries in the `idx` field of the
+    // avail ring The check for pending entries is done by comparing the
+    // current `avail_idx` with the `next_avail` field of the queue. If they
+    // are different, there are pending entries, otherwise there are no
+    // pending entries. The equality check is a consequence of the
+    // monotonicity property of `idx` (2.7.6.1) that it cannot be decreased
+    // by the driver.
+    if queue.enable_notification(&memory).unwrap() {
+        assert_ne!(
+            queue.avail_idx(&memory, Ordering::Relaxed).unwrap(),
+            queue.next_avail
+        );
+    } else {
+        assert_eq!(
+            queue.avail_idx(&memory, Ordering::Relaxed).unwrap(),
+            queue.next_avail
+        );
+    }
+}
+
+// Helper method that reads `val` from the `avail_event` field of the used ring, using
+// the provided ordering. Takes used_ring address and queue size directly.
+fn get_avail_event<M: GuestMemory>(
+    used_ring_addr: GuestAddress,
+    queue_size: u16,
+    mem: &M,
+    order: Ordering,
+) -> Result<u16, Error> {
+    // This can not overflow an u64 since it is working with relatively small numbers compar
+    // to u64::MAX.
+    let avail_event_offset =
+        VIRTQ_USED_RING_HEADER_SIZE + VIRTQ_USED_ELEMENT_SIZE * u64::from(queue_size);
+    let addr = used_ring_addr
+        .checked_add(avail_event_offset)
+        .ok_or(Error::AddressOverflow)?;
+
+    mem.load::<u16>(addr, order).map_err(Error::GuestMemory)
+}
+
+// Get the value of the `flags` field of the used ring, applying the specified ordering.
+fn get_used_flags<M: GuestMemory>(queue: &Queue, mem: &M, order: Ordering) -> Result<u16, Error> {
+    mem.load::<u16>(queue.used_ring, order)
+        .map(u16::from_le)
+        .map_err(Error::GuestMemory)
+}
+/// # Specification (VirtIO 1.3, Section 2.7.7: "Used Buffer Notification Suppression")
+///
+/// This proof checks:
+/// - If event_idx is not enabled, `set_notification(false)` sets used.flags to 1 (NO_NOTIFY).
+/// - If event_idx is enabled, the call is a no-op.
+#[kani::proof]
+#[kani::unwind(0)]
+fn verify_set_notification_true() {
+    let ProofContext { mut queue, memory } = kani::any();
+    if queue
+        .set_notification(&memory, true /* enable notification */)
+        .is_ok()
+    {
+        if queue.event_idx_enabled {
+            // Since VIRTIO_F_EVENT_IDX is negotiated, we make sure that set_notification
+            // has updated the used.avail_event field with the tail position of
+            // the avail ring.
+            let used_ring_addr = queue.used_ring;
+            let queue_size = queue.size();
+            kani::cover!();
+            assert_eq!(
+                get_avail_event(used_ring_addr, queue_size, &memory, Ordering::Relaxed).unwrap(),
+                queue.next_avail.0
+            );
+        } else {
+            // If VIRTIO_F_EVENT_IDX is not negotiated, we make sure that the
+            // used.flags field is set to 0, meaning that the driver should not
+            // send notifications to the device.
+            kani::cover!();
+            assert_eq!(
+                get_used_flags(&queue, &memory, Ordering::Relaxed).unwrap(),
+                0
+            );
+        }
+    }
+}
+
+/// # Specification (VirtIO 1.3, Section 2.7.7: "Used Buffer Notification Suppression")
+///
+/// This proof checks:
+/// - If event_idx is not enabled, `set_notification(false)` sets used.flags to 1 (NO_NOTIFY).
+/// - If event_idx is enabled, the call is a no-op.
+#[kani::proof]
+#[kani::unwind(0)]
+fn verify_set_notification_false() {
+    let ProofContext { mut queue, memory } = kani::any();
+    let result = queue.set_notification(&memory, false /* disable notification */);
+    if !queue.event_idx_enabled {
+        // Check for Sec 2.7.10
+        assert_eq!(
+            get_used_flags(&queue, &memory, Ordering::Relaxed).unwrap(),
+            1
+        );
+        // don't check Ok() result since that is a property of the
+        // underlying mem system and out of scope. E.g., it is stubbed for
+        // this proof and we always expect it to succeed.
+    } else {
+        assert!(result.is_ok());
+    }
+}