Update Firecracker block example (rust-lang#1135)

Author: nchong-at-aws

tests/cargo-kani/firecracker-block-example/Cargo.toml

@@ -0,0 +1,7 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "firecracker-block-example"
+version = "0.1.0"
+edition = "2018"

tests/cargo-kani/firecracker-block-example/README.md

@@ -0,0 +1,38 @@
+This example accompanies Kani's post on Firecracker. This describes a proof
+harness for ensuring that the Firecracker block device `parse` method adheres
+to a virtio requirement (see below). We implement this as a standalone example
+with some simplifications (search for "Kani change" in the source).
+
+This example is based on code from Firecracker. In particular,
+
+  - <https://github.com/firecracker-microvm/firecracker/tree/main/src/devices/src/virtio/block>
+  - <https://github.com/firecracker-microvm/firecracker/blob/main/src/devices/src/virtio/queue.rs>
+
+## Virtio requirement
+
+We implement a simple finite-state-machine checker in `descriptor_permission_checker.rs` that ensures the following:
+
+> 2.6.4.2 Driver Requirements: Message Framing
+>
+> The driver MUST place any device-writable descriptor elements after any device-readable descriptor elements.
+>
+> Source: https://docs.oasis-open.org/virtio/virtio/v1.1/csprd01/virtio-v1.1-csprd01.html#x1-280004
+
+## Reproducing results locally
+
+### Dependencies
+
+  - Rust edition 2018
+  - [Kani](https://model-checking.github.io/kani/getting-started.html)
+
+If you have problems installing Kani then please file an [issue](https://github.com/model-checking/kani/issues/new/choose).
+
+### Using Kani
+
+Since there is only one harness in this example you can simply do the
+following, where the expected result is verification success.
+
+```bash
+$ cargo kani
+# expected result: verification success
+```

tests/cargo-kani/firecracker-block-example/requirement_2642.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/cargo-kani/firecracker-block-example/src/descriptor_permission_checker.rs

@@ -0,0 +1,49 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use crate::virtio_defs::*;
+
+#[derive(Clone, Copy)]
+pub enum DescriptorPermission {
+    ReadOnly,
+    WriteOnly,
+}
+
+impl DescriptorPermission {
+    pub fn from_flags(flags: u16) -> Self {
+        if 0 != (flags & VIRTQ_DESC_F_WRITE) { Self::WriteOnly } else { Self::ReadOnly }
+    }
+}
+
+// ANCHOR: fsm
+#[derive(std::cmp::PartialEq, Clone, Copy)]
+enum State {
+    ReadOrWriteOk,
+    OnlyWriteOk,
+    Invalid,
+}
+
+/// State machine checker for virtio requirement 2.6.4.2
+pub struct DescriptorPermissionChecker {
+    state: State,
+}
+
+impl DescriptorPermissionChecker {
+    pub fn new() -> Self {
+        DescriptorPermissionChecker { state: State::ReadOrWriteOk }
+    }
+
+    pub fn update(&mut self, next_permission: DescriptorPermission) {
+        let next_state = match (self.state, next_permission) {
+            (State::ReadOrWriteOk, DescriptorPermission::WriteOnly) => State::OnlyWriteOk,
+            (State::OnlyWriteOk, DescriptorPermission::ReadOnly) => State::Invalid,
+            (_, _) => self.state,
+        };
+        self.state = next_state;
+    }
+
+    pub fn virtio_2642_holds(&self) -> bool {
+        self.state != State::Invalid
+    }
+}
+// ANCHOR_END: fsm