Add weak reference tests and view Kani proofs

CHANGELOG.md

@@ -6,6 +6,7 @@
 - move weak reference and downcasting examples into module docs
 - expand module introduction describing use cases
 - document rationale for separating `ByteSource` and `ByteOwner`
+- add tests for weak reference upgrade/downgrade and Kani proofs for view helpers
 - add examples for quick start and PyBytes usage
 - add example showing how to wrap Python `bytes` into `Bytes`
 - summarize built-in `ByteSource`s and show how to extend them

src/tests.rs

@@ -76,3 +76,41 @@ fn test_slice_to_bytes_unrelated_slice() {
     let slice = &other[1..4];
     assert!(bytes.slice_to_bytes(slice).is_none());
 }
+
+#[test]
+fn test_weakbytes_multiple_upgrades() {
+    let bytes = Bytes::from(b"hello".to_vec());
+    let weak = bytes.downgrade();
+
+    // Upgrade works while strong reference exists
+    let strong1 = weak.upgrade().unwrap();
+    assert_eq!(strong1.as_ref(), bytes.as_ref());
+    drop(strong1);
+
+    // Can upgrade multiple times
+    let strong2 = weak.upgrade().unwrap();
+    assert_eq!(strong2.as_ref(), b"hello".as_ref());
+
+    drop(bytes);
+    drop(strong2);
+
+    // After all strong refs are gone, upgrade returns None
+    assert!(weak.upgrade().is_none());
+}
+
+#[cfg(feature = "zerocopy")]
+#[test]
+fn test_weakview_downgrade_upgrade() {
+    let bytes = Bytes::from(b"abcdef".to_vec());
+    let view = bytes.clone().view::<[u8]>().unwrap();
+
+    let weak = view.downgrade();
+    let strong = weak.upgrade().unwrap();
+    assert_eq!(strong.as_ref(), view.as_ref());
+
+    drop(bytes);
+    drop(view);
+    drop(strong);
+
+    assert!(weak.upgrade().is_none());
+}

src/view.rs

@@ -442,3 +442,66 @@ mod tests {
         assert_eq!(&bytes[..], [1u8, 2, 3].as_slice());
     }
 }
+
+#[cfg(kani)]
+mod verification {
+    use super::*;
+    use kani::BoundedArbitrary;
+
+    #[kani::proof]
+    #[kani::unwind(16)]
+    pub fn check_view_prefix_ok() {
+        let data: Vec<u8> = Vec::bounded_any::<16>();
+        kani::assume(data.len() >= 4);
+        let mut bytes = Bytes::from_source(data.clone());
+        let original = bytes.clone();
+        let view = bytes.view_prefix::<[u8; 4]>().expect("prefix exists");
+        let expected: [u8; 4] = original.as_ref()[..4].try_into().unwrap();
+        assert_eq!(*view, expected);
+        assert_eq!(bytes.as_ref(), &original.as_ref()[4..]);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(16)]
+    pub fn check_view_suffix_ok() {
+        let data: Vec<u8> = Vec::bounded_any::<16>();
+        kani::assume(data.len() >= 4);
+        let mut bytes = Bytes::from_source(data.clone());
+        let original = bytes.clone();
+        let view = bytes.view_suffix::<[u8; 4]>().expect("suffix exists");
+        let start = original.len() - 4;
+        let expected: [u8; 4] = original.as_ref()[start..].try_into().unwrap();
+        assert_eq!(*view, expected);
+        assert_eq!(bytes.as_ref(), &original.as_ref()[..start]);
+    }
+
+    #[derive(
+        zerocopy::TryFromBytes,
+        zerocopy::IntoBytes,
+        zerocopy::KnownLayout,
+        zerocopy::Immutable,
+        Clone,
+        Copy,
+    )]
+    #[repr(C)]
+    struct Pair {
+        a: u32,
+        b: u32,
+    }
+
+    #[kani::proof]
+    #[kani::unwind(8)]
+    pub fn check_field_to_view_ok() {
+        let value = Pair {
+            a: kani::any(),
+            b: kani::any(),
+        };
+        let bytes = Bytes::from_source(Box::new(value));
+        let view = bytes.view::<Pair>().unwrap();
+        let field = view.field_to_view(&view.a).expect("field view");
+        assert_eq!(*field, view.a);
+
+        let other: u32 = kani::any();
+        assert!(view.field_to_view(&other).is_none());
+    }
+}