From f4617e71f5fd074000d1e3a9376644c744210562 Mon Sep 17 00:00:00 2001
From: "Tobin C. Harding" <me@tobin.cc>
Date: Thu, 19 Dec 2024 08:59:12 +1100
Subject: [PATCH] kani: Verify no out of bounds for ArrayVec

I'm not super confident that I know exactly what kani does but I believe
this test verifies that the `ArrayVec` can add and access elements less
than capacity and upto capacity.
---
 internals/Cargo.toml       |  2 +-
 internals/src/array_vec.rs | 42 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 43 insertions(+), 1 deletion(-)

diff --git a/internals/Cargo.toml b/internals/Cargo.toml
index 0b9b6c252..12a5daa1d 100644
--- a/internals/Cargo.toml
+++ b/internals/Cargo.toml
@@ -35,4 +35,4 @@ all-features = true
 rustdoc-args = ["--cfg", "docsrs"]
 
 [lints.rust]
-unexpected_cfgs = { level = "deny" }
+unexpected_cfgs = { level = "deny", check-cfg = ['cfg(kani)'] }
diff --git a/internals/src/array_vec.rs b/internals/src/array_vec.rs
index 49fca83d8..24003e14b 100644
--- a/internals/src/array_vec.rs
+++ b/internals/src/array_vec.rs
@@ -188,3 +188,45 @@ mod tests {
         av.extend_from_slice(b"abc");
     }
 }
+
+#[cfg(kani)]
+mod verification {
+    use super::*;
+
+    #[kani::unwind(16)]         // One greater than 15 (max number of elements).
+    #[kani::proof]
+    fn no_out_of_bounds_less_than_cap() {
+        const CAP: usize = 32;
+        let n = kani::any::<u32>();
+        let elements = (n & 0x0F) as usize; // Just use 4 bits.
+
+        let val = kani::any::<u32>();
+
+        let mut v = ArrayVec::<u32, CAP>::new();
+        for _ in 0..elements {
+            v.push(val);
+        }
+
+        for i in 0..elements {
+            assert_eq!(v[i], val);
+        }
+    }
+
+    #[kani::unwind(16)]         // One grater than 15.
+    #[kani::proof]
+    fn no_out_of_bounds_upto_cap() {
+        const CAP: usize = 15;
+        let elements = CAP;
+
+        let val = kani::any::<u32>();
+
+        let mut v = ArrayVec::<u32, CAP>::new();
+        for _ in 0..elements {
+            v.push(val);
+        }
+
+        for i in 0..elements {
+            assert_eq!(v[i], val);
+        }
+    }
+}