Add proof for conformance to 2.7.7.2 section

[MatiasVara]

Summary of the PR

This is WIP in which I try to add a kany proof to meet the requirements outlined in 2.7.7.2 of the virtio specification regarding the notification suppression mechanism. I sketched this proof from the same proof defined for the queue implemented in firecraker. This commit adds the verify_spec_2_7_7_2() proof to verify that the implementation of queue meets 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 queue. To run the proof, you can run:

cargo kani

The proof currently passes:

SUMMARY:
 ** 0 of 4802 failed (280 unreachable)

 ** 1 of 1 cover properties satisfied


VERIFICATION:- SUCCESSFUL
Verification Time: 41.5208s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.

If you have any comment, feel free to let me know.

Thanks.

Requirements

Before submitting your PR, please make sure you addressed the following
requirements:

• All commits in this PR have Signed-Off-By trailers (with
  git commit -s), and the commit message has max 60 characters for the
  summary and max 75 characters for each description line.
• All added/changed functionality has a corresponding unit/integration
  test.
• All added/changed public-facing functionality has entries in the "Upcoming
  Release" section of CHANGELOG.md (if no such section exists, please create one).
• Any newly added unsafe code is properly documented.