[kani] Prove utility memory operations

zerocopy/src/lib.rs

@@ -5987,11 +5987,7 @@ pub unsafe trait IntoBytes {
     {
         let src = self.as_bytes();
         if dst.len() == src.len() {
-            // SAFETY: Within this branch of the conditional, we have ensured
-            // that `dst.len()` is equal to `src.len()`. Neither the size of the
-            // source nor the size of the destination change between the above
-            // size check and the invocation of `copy_unchecked`.
-            unsafe { util::copy_unchecked(src, dst) }
+            util::copy_prefix(src, dst);
             Ok(())
         } else {
             Err(SizeError::new(self))
@@ -6074,12 +6070,7 @@ pub unsafe trait IntoBytes {
         let src = self.as_bytes();
         match dst.get_mut(..src.len()) {
             Some(dst) => {
-                // SAFETY: Within this branch of the `match`, we have ensured
-                // through fallible subslicing that `dst.len()` is equal to
-                // `src.len()`. Neither the size of the source nor the size of
-                // the destination change between the above subslicing operation
-                // and the invocation of `copy_unchecked`.
-                unsafe { util::copy_unchecked(src, dst) }
+                util::copy_prefix(src, dst);
                 Ok(())
             }
             None => Err(SizeError::new(self)),
@@ -6181,13 +6172,7 @@ pub unsafe trait IntoBytes {
             // than panicking.
             return Err(SizeError::new(self));
         };
-        // SAFETY: Through fallible subslicing of `dst`, we have ensured that
-        // `dst.len()` is equal to `src.len()`. Neither the size of the source
-        // nor the size of the destination change between the above subslicing
-        // operation and the invocation of `copy_unchecked`.
-        unsafe {
-            util::copy_unchecked(src, dst);
-        }
+        util::copy_prefix(src, dst);
         Ok(())
     }
 

zerocopy/src/proof_support.rs

@@ -397,3 +397,29 @@ pub(crate) fn nonzero_u16_from_ne_bytes(bytes: [u8; 2]) -> Option<core::num::Non
 pub(crate) fn copy_snapshot<T: Copy>(value: &T) -> T {
     *value
 }
+
+// Compare ordered byte values without treating slice or array `PartialEq` as
+// an implicit oracle. `slice::len` returns each slice's element count,
+// while the factored `assert_same_usize` supplies the documented equality
+// observation above. The first assertion therefore requires equal element
+// counts. `slice::iter` yields every item from start to end [1],
+// `Iterator::copied` copies those items and `Iterator::eq` compares the two
+// sequences [2], and `u8::eq` supplies element equality [3]. Rust specifies
+// that the final `assert!` panics when that equality expression
+// is false and cannot be disabled [4], so—under Kani's assertion/panic
+// translation—an ordered-value mismatch cannot silently pass the harness.
+// These safe operations call no zerocopy target, so they are
+// independent of that target implementation, but not of the compiler,
+// standard library, or Kani model. They establish values only, not storage
+// identity or provenance.
+//
+// [1] https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.len
+//     https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.iter
+// [2] https://doc.rust-lang.org/1.93.0/std/iter/trait.Iterator.html#method.copied
+//     https://doc.rust-lang.org/1.93.0/std/iter/trait.Iterator.html#method.eq
+// [3] https://doc.rust-lang.org/1.93.0/std/primitive.u8.html#impl-PartialEq-for-u8
+// [4] https://doc.rust-lang.org/1.93.0/std/macro.assert.html
+pub(crate) fn assert_same_u8_elements(actual: &[u8], expected: &[u8]) {
+    assert_same_usize(actual.len(), expected.len());
+    assert!(actual.iter().copied().eq(expected.iter().copied()));
+}