From e3fea82ec320ba5d0b3e07fc7c9386907d0d59c4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=E2=9A=AB=EF=B8=8F?= <jp@bultmann.eu>
Date: Wed, 25 Sep 2024 22:10:59 +0200
Subject: [PATCH] add some kani proofs

---
 .github/workflows/rust.yml |  2 ++
 Cargo.toml                 |  4 +--
 src/bytes.rs               | 10 ------
 src/owners.rs              | 69 ++++++++++++++++++++++++++++++++++++++
 4 files changed, 73 insertions(+), 12 deletions(-)

diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
index 562f992..c89dcd8 100644
--- a/.github/workflows/rust.yml
+++ b/.github/workflows/rust.yml
@@ -19,3 +19,5 @@ jobs:
       run: cargo build --verbose --all-features
     - name: Run tests
       run: cargo test --verbose --all-features
+    - name: Run Verification
+      run: cargo kani --verbose --all-features
diff --git a/Cargo.toml b/Cargo.toml
index 626bc7b..8afbc8c 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -7,10 +7,10 @@ repository = "https://github.com/triblespace/anybytes"
 description = "A small library abstracting over bytes owning types in an extensible way."
 
 [dependencies]
-bytes = { version = "1.6.0", features = ["serde"], optional = true }
+bytes = { version = "1.6.0", optional = true }
 ownedbytes = { version = "0.7.0", optional = true }
 memmap2 = { version = "0.9.4", optional = true }
-zerocopy = { version = "0.7.35", optional = true }
+zerocopy = { version = "0.7.35", optional = true, features = ["derive"] }
 
 [dev-dependencies]
 quickcheck = "1.0"
diff --git a/src/bytes.rs b/src/bytes.rs
index 26cd784..ec7b792 100644
--- a/src/bytes.rs
+++ b/src/bytes.rs
@@ -290,13 +290,3 @@ mod tests {
         assert_eq!(size_of::<Bytes>(), size_of::<Option<Bytes>>());
     }
 }
-
-#[cfg(kani)]
-mod verification {
-    use super::*;
-
-    #[kani::proof]
-    pub fn check_something() {
-        // ....
-    }
-}
\ No newline at end of file
diff --git a/src/owners.rs b/src/owners.rs
index dae135e..4c716ff 100644
--- a/src/owners.rs
+++ b/src/owners.rs
@@ -92,3 +92,72 @@ unsafe impl ByteOwner for memmap2::Mmap {
         self.as_ref()
     }
 }
+
+#[cfg(kani)]
+mod verification {
+    use std::sync::Arc;
+
+    use crate::Bytes;
+
+    use super::*;
+
+    static STATIC_U8: [u8; 1024] = [0; 1024];
+
+    #[kani::proof]
+    #[kani::unwind(1025)]
+    pub fn check_static() {
+        let owner: &'static [u8] = &STATIC_U8;
+        let bytes = Bytes::from_owner(owner);
+        let bytes_slice: &[u8] = &bytes;
+        assert_eq!(owner, bytes_slice)
+    }
+
+    #[kani::proof]
+    #[kani::unwind(1025)]
+    pub fn check_box() {
+        let owner: Box<[u8]> = STATIC_U8.into();
+        let arc = Arc::new(owner);
+        let bytes = Bytes::from_arc(arc.clone());
+        let arc_slice: &[u8] = &arc;
+        let bytes_slice: &[u8] = &bytes;
+        assert_eq!(arc_slice, bytes_slice)
+    }
+
+    #[cfg(feature = "zerocopy")]
+    #[derive(zerocopy::FromZeroes, zerocopy::FromBytes, zerocopy::AsBytes, Clone, Copy)]
+    #[repr(C)]
+    struct ComplexZC {
+        a: u64,
+        b: [u8; 4],
+        c: u32
+    }
+
+    #[cfg(feature = "zerocopy")]
+    static STATIC_ZC: [ComplexZC; 1024] = [ComplexZC {
+        a: 42,
+        b: [0; 4],
+        c: 9000
+    }; 1024];
+
+    #[cfg(feature = "zerocopy")]
+    #[kani::proof]
+    #[kani::unwind(16_385)]
+    pub fn check_static_zeroconf() {
+        let owner: &'static [ComplexZC] = &STATIC_ZC;
+        let bytes = Bytes::from_owner(owner);
+        let bytes_slice: &[u8] = &bytes;
+        assert_eq!(owner.as_bytes(), bytes_slice)
+    }
+
+    #[cfg(feature = "zerocopy")]
+    #[kani::proof]
+    #[kani::unwind(16_385)]
+    pub fn check_box_zeroconf() {
+        let owner: Box<[ComplexZC]> = STATIC_ZC.into();
+        let arc = Arc::new(owner);
+        let bytes = Bytes::from_arc(arc.clone());
+        let arc_slice: &[u8] = arc.as_bytes();
+        let bytes_slice: &[u8] = &bytes;
+        assert_eq!(arc_slice, bytes_slice)
+    }
+}
\ No newline at end of file