[byte_slice] Add Kani proofs (#2451)

gherrit-pr-id: Ide939969b8d0c3bc117aa9f1dba06e6d570f262f

Author: joshlf

.github/workflows/ci.yml

@@ -595,7 +595,7 @@ jobs:
           args: "--package zerocopy --features __internal_use_only_features_that_work_on_stable --output-format=terse -Zfunction-contracts --randomize-layout --memory-safety-checks --overflow-checks --undefined-function-checks --unwinding-checks"
           # This version is automatically rolled by
           # `roll-pinned-toolchain-versions.yml`.
-          kani-version: 0.55.0
+          kani-version: 0.60.0
 
   # NEON intrinsics are currently broken on big-endian platforms. [1] This test ensures
   # that we don't accidentally attempt to compile these intrinsics on such platforms. We

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,7 +377,7 @@ 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))]
 use alloc::{boxed::Box, vec::Vec};