[kani] Prove some PtrInner methods

Also add Kani `requires` and `ensures` annotations to some methods and
to some functions in `util`.

While we're here, roll Kani to 0.60.0 and fix the Kani roller.

gherrit-pr-id: Ic1e352d3d92a45ff86d8ca85b8221bccfb07033b

Author: joshlf

.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/lib.rs

@@ -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