[byte_slice] Add Kani proofs

gherrit-pr-id: Ide939969b8d0c3bc117aa9f1dba06e6d570f262f

Author: joshlf

src/byte_slice.rs

@@ -353,3 +353,46 @@ unsafe impl SplitByteSlice for cell::RefMut<'_, [u8]> {
             })
     }
 }
+
+#[cfg(kani)]
+mod proofs {
+    use super::*;
+
+    fn any_vec() -> Vec<u8> {
+        let len = kani::any();
+        kani::assume(len <= isize::MAX as usize);
+        vec![0u8; len]
+    }
+
+    #[kani::proof]
+    fn prove_split_at_unchecked() {
+        let v = any_vec();
+        let slc = v.as_slice();
+        let mid = kani::any();
+        kani::assume(mid <= slc.len());
+        let (l, r) = unsafe { slc.split_at_unchecked(mid) };
+        assert_eq!(l.len() + r.len(), slc.len());
+
+        let slc: *const _ = slc;
+        let l: *const _ = l;
+        let r: *const _ = r;
+
+        assert_eq!(slc.cast::<u8>(), l.cast::<u8>());
+        assert_eq!(unsafe { slc.cast::<u8>().add(mid) }, r.cast::<u8>());
+
+        let mut v = any_vec();
+        let slc = v.as_mut_slice();
+        let len = slc.len();
+        let mid = kani::any();
+        kani::assume(mid <= slc.len());
+        let (l, r) = unsafe { slc.split_at_unchecked(mid) };
+        assert_eq!(l.len() + r.len(), len);
+
+        let l: *mut _ = l;
+        let r: *mut _ = r;
+        let slc: *mut _ = slc;
+
+        assert_eq!(slc.cast::<u8>(), l.cast::<u8>());
+        assert_eq!(unsafe { slc.cast::<u8>().add(mid) }, r.cast::<u8>());
+    }
+}

src/lib.rs

@@ -302,7 +302,7 @@
     clippy::arithmetic_side_effects,
     clippy::indexing_slicing,
 ))]
-#![cfg_attr(not(any(test, feature = "std")), no_std)]
+#![cfg_attr(not(any(test, kani, feature = "std")), no_std)]
 #![cfg_attr(
     all(feature = "simd-nightly", any(target_arch = "x86", target_arch = "x86_64")),
     feature(stdarch_x86_avx512)
@@ -377,9 +377,9 @@ use std::io;
 
 use crate::pointer::invariant::{self, BecauseExclusive};
 
-#[cfg(any(feature = "alloc", test))]
+#[cfg(any(feature = "alloc", test, kani))]
 extern crate alloc;
-#[cfg(any(feature = "alloc", test))]
+#[cfg(any(feature = "alloc", test, kani))]
 use alloc::{boxed::Box, vec::Vec};
 
 #[cfg(any(feature = "alloc", test))]