From bcc66cd29a9dd24dbf102cba32191fa81260ba82 Mon Sep 17 00:00:00 2001
From: Jan-Paul Bultmann
 <74891396+somethingelseentirely@users.noreply.github.com>
Date: Wed, 15 Oct 2025 17:15:37 +0200
Subject: [PATCH] Document Kani downcast invariants

---
 CHANGELOG.md |  1 +
 src/bytes.rs | 28 ++++++++++++++++++++++++++++
 2 files changed, 29 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 728536a..673459c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,7 @@
 # Changelog
 
 ## Unreleased
+- add Kani proof checking `Bytes::downcast_to_owner` for matching and mismatched owners
 - avoid flushing empty memory maps in `Section::freeze` to prevent macOS errors
 - derived zerocopy traits for `SectionHandle` to allow storing handles in `ByteArea` sections
 - added example demonstrating `ByteArea` with multiple typed sections, concurrent mutations, and freezing or persisting the area
diff --git a/src/bytes.rs b/src/bytes.rs
index c534b94..96f95ee 100644
--- a/src/bytes.rs
+++ b/src/bytes.rs
@@ -656,4 +656,32 @@ mod verification {
         drop(bytes);
         assert!(weak.upgrade().is_none());
     }
+
+    #[kani::proof]
+    #[kani::unwind(16)]
+    pub fn check_downcast_to_owner_preserves_data() {
+        let data: Vec<u8> = Vec::bounded_any::<16>();
+        kani::assume(data.len() <= 16);
+
+        let bytes = Bytes::from_source(data.clone());
+
+        // Invariant: when the owner really is a Vec<u8>, downcasting the Bytes
+        // owner should succeed and recover the same Arc<Vec<u8>> that backs the
+        // original allocation.  This ensures Bytes keeps the concrete owner
+        // type intact through cloning and slicing operations.
+        let arc_vec = bytes
+            .clone()
+            .downcast_to_owner::<Vec<u8>>()
+            .expect("downcast to Vec<u8>");
+        assert_eq!(&*arc_vec, &data);
+
+        // Invariant: attempting to downcast to the wrong owner type must fail
+        // without mutating the Bytes value.  The returned Bytes should still
+        // expose the same data slice so callers can continue using it.
+        let result = bytes.downcast_to_owner::<String>();
+        let Err(returned) = result else {
+            panic!("downcast to String should fail");
+        };
+        assert_eq!(returned.as_ref(), data.as_slice());
+    }
 }