From 1554b9853e50b9f0c03d5a6980fd1f1b3f5ebf2f Mon Sep 17 00:00:00 2001
From: toidiu <apoorv@toidiu.com>
Date: Wed, 29 Mar 2023 13:08:21 -0700
Subject: [PATCH] tests(s2n-quic-core): kani test for packet number map (#1508)

---
 quic/s2n-quic-core/src/packet/number/map.rs | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/quic/s2n-quic-core/src/packet/number/map.rs b/quic/s2n-quic-core/src/packet/number/map.rs
index 0399e37f0d..a06e4f7112 100644
--- a/quic/s2n-quic-core/src/packet/number/map.rs
+++ b/quic/s2n-quic-core/src/packet/number/map.rs
@@ -769,4 +769,21 @@ mod tests {
             .with_type::<Vec<Operation>>()
             .for_each(|ops| model(ops))
     }
+
+    #[test]
+    #[cfg_attr(kani, kani::proof, kani::unwind(9), kani::solver(kissat))]
+    fn insert_value() {
+        // Confirm that a value is inserted
+        check!().with_type().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());
+        });
+    }
 }