testing: kani test for packet number map

aws · Sep 22, 2022 · 88618ae · 88618ae
1 parent b8f38ad
commit 88618ae
Showing 1 changed file with 23 additions and 0 deletions.
diff --git a/quic/s2n-quic-core/src/packet/number/map.rs b/quic/s2n-quic-core/src/packet/number/map.rs
@@ -769,4 +769,27 @@ mod tests {
             .with_type::<Vec<Operation>>()
             .for_each(|ops| model(ops))
     }
+
+
+    #[test]
+    #[cfg_attr(kani, kani::proof, kani::unwind(9))]
+    fn kani_test() {
+        // Confirm that a 
+        let gen = gen::<VarInt>();
+
+        check!()
+            .with_generator(gen)
+            .cloned()
+            .for_each(|pn| {
+                let space = PacketNumberSpace::ApplicationData;
+                let mut map = Map::default();
+                assert!(map.is_empty());
+                let pn = space.new_packet_number(pn);
+
+                map.insert(pn, ());
+
+                assert!(map.get(pn).is_some());
+                assert!(!map.is_empty());
+            });
+    }
 }