[kani] Prove some PtrInner methods

.github/workflows/ci.yml

@@ -592,10 +592,10 @@ jobs:
           # TODO(https://github.com/model-checking/kani-github-action/issues/56):
           # Go back to testing all features once the Kani GitHub Action supports
           # specifying a particular toolchain.
-          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"
+          args: "--package zerocopy --features __internal_use_only_features_that_work_on_stable --output-format=terse -Zfunction-contracts -Zmem-predicates --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

.github/workflows/roll-pinned-toolchain-versions.yml

@@ -144,7 +144,7 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        branch: ["main", "v0.7.x"]
+        branch: ["main"]
     name: Roll pinned Kani version
     steps:
       - name: Checkout code

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};
@@ -738,8 +738,13 @@ pub unsafe trait KnownLayout {
     /// The type of metadata stored in a pointer to `Self`.
     ///
     /// This is `()` for sized types and `usize` for slice DSTs.
+    #[cfg(not(kani))]
     type PointerMetadata: PointerMetadata;
 
+    #[cfg(kani)]
+    #[allow(missing_docs)]
+    type PointerMetadata: PointerMetadata + kani::Arbitrary;
+
     /// A maybe-uninitialized analog of `Self`
     ///
     /// # Safety