Adds stub for read_be_u16 to Kani harnesses

The current implementation of read_be_u16 function leads to a
significant performance degradation given a necessary loop
unrolling. Using this stub, we read the same information from
the buffer while avoiding the loop, thus, notably improving
performance.

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Author: feliperodri

src/dumbo/src/pdu/ethernet.rs

@@ -238,6 +238,7 @@ mod tests {
 }
 
 #[cfg(kani)]
+#[allow(dead_code)] // Avoid warning when using stubs.
 mod kani_proofs {
     use utils::net::mac::MAC_ADDR_LEN;
 
@@ -253,6 +254,16 @@ mod kani_proofs {
         }
     }
 
+    mod stubs {
+        // The current implementation of read_be_u16 function leads to a significant
+        // performance degradation given a necessary loop unrolling. Using this stub,
+        // we read the same information from the buffer while avoiding the loop, thus,
+        // notably improving performance.
+        pub fn read_be_u16(input: &[u8]) -> u16 {
+            u16::from_be_bytes([input[0], input[1]])
+        }
+    }
+
     // We consider the MMDS Network Stack spec for all postconditions in the harnesses.
     // See https://github.com/firecracker-microvm/firecracker/blob/main/docs/mmds/mmds-design.md#mmds-network-stack
 
@@ -502,8 +513,8 @@ mod kani_proofs {
     }
 
     #[kani::proof]
-    #[kani::unwind(1515)]
     #[kani::solver(cadical)]
+    #[kani::stub(utils::byte_order::read_be_u16, stubs::read_be_u16)]
     fn verify_with_payload_len_unchecked() {
         // Create non-deterministic stream of bytes up to MAX_FRAME_SIZE
         let mut bytes: [u8; MAX_FRAME_SIZE] = kani::Arbitrary::any_array::<MAX_FRAME_SIZE>();