[kani] Tighten slice and Ref proof scopes

zerocopy/src/layout.rs

@@ -122,7 +122,7 @@ impl DstLayout {
 
     /// The current, documented max alignment of a type \[1\].
     ///
-    /// \[1\] Per <https://doc.rust-lang.org/reference/type-layout.html#the-alignment-modifiers>:
+    /// \[1\] Per <https://doc.rust-lang.org/1.93.0/reference/type-layout.html#the-alignment-modifiers>:
     ///
     ///   The alignment value must be a power of two from 1 up to
     ///   2<sup>29</sup>.
@@ -365,7 +365,7 @@ impl DstLayout {
         // The field's alignment is clamped by `repr_packed` (i.e., the
         // `repr(packed(N))` attribute, if any) [1].
         //
-        // [1] Per https://doc.rust-lang.org/reference/type-layout.html#the-alignment-modifiers:
+        // [1] Per https://doc.rust-lang.org/1.93.0/reference/type-layout.html#the-alignment-modifiers:
         //
         //   The alignments of each field, for the purpose of positioning
         //   fields, is the smaller of the specified alignment and the alignment
@@ -386,7 +386,7 @@ impl DstLayout {
                 // satisfy the field's alignment, and offset of the trailing
                 // field. [1]
                 //
-                // [1] Per https://doc.rust-lang.org/reference/type-layout.html#the-alignment-modifiers:
+                // [1] Per https://doc.rust-lang.org/1.93.0/reference/type-layout.html#the-alignment-modifiers:
                 //
                 //   Inter-field padding is guaranteed to be the minimum
                 //   required in order to satisfy each field's (possibly

zerocopy/src/lib.rs

@@ -366,6 +366,12 @@ mod macros;
 pub mod pointer;
 #[cfg(kani)]
 mod proof_support;
+// Coordinator for proof families that exercise crate-level APIs or generated
+// implementations rather than one source module. Each child module's
+// top-level documentation enumerates its exact entry points, symbolic and
+// concrete bounds, established properties, and non-goals. This list therefore
+// controls compilation only; it is not itself a claim that the listed proofs
+// cover all implementations of the corresponding trait.
 #[cfg(kani)]
 mod proofs {
     #[cfg(all(feature = "alloc", not(no_zerocopy_panic_in_const_and_vec_try_reserve_1_57_0)))]

zerocopy/src/proofs/into_bytes.rs

@@ -177,8 +177,10 @@
 //! `expected[..len]` destination and calls safe
 //! `slice::last_chunk_mut::<4>`, whose contract directly selects its last four
 //! elements or returns `None` when fewer exist [20]. It is reached only on the
-//! `len >= 4` policy branch and fails closed if that safe oracle nevertheless
-//! returns `None`. Thus suffix placement uses no reconstructed subtraction.
+//! branch where the shared safe minimum-length oracle reports that the actual
+//! passed slice contains a value-sized chunk, and it fails closed if this safe
+//! suffix oracle nevertheless returns `None`. Thus suffix placement uses no
+//! reconstructed subtraction.
 //! These operations are the Rust/library placement oracles; the target API
 //! policy still decides whether a write is supposed to succeed.
 //!
@@ -192,13 +194,18 @@
 //! incomplete aliasing, provenance, and reference-lifetime checks remain
 //! TOOL/TCB premises for this outer-frame observation [22].
 //!
-//! Success-ordering basis: Rust comparison expressions use `PartialOrd`, whose
-//! `ge` method implements `>=`; primitive `usize` supplies that implementation
-//! [24]. `assert_modeled_u32_size` establishes `VALUE_SIZE == 4`, while
-//! `destination_len` ranges over exactly `0..=6`. Thus
-//! `len >= VALUE_SIZE` is true exactly for lengths 4, 5, and 6. This comparison
-//! is only the language mechanism implementing the documented zerocopy
-//! minimum-length policy; it is not an independent source of that policy.
+//! Minimum-length policy oracle basis: the shared
+//! `minimum_length_policy_oracle` asks safe
+//! `slice::first_chunk::<VALUE_SIZE>` about the actual passed destination.
+//! `first_chunk` "Returns the first `N` elements of the slice, or `None` if it
+//! has fewer than `N` elements," and `Option::is_some` returns true exactly for
+//! `Some` [24]. `assert_modeled_u32_size` establishes `VALUE_SIZE == 4`, while
+//! `destination_len` reaches every logical length in `0..=6`. The oracle
+//! therefore reports success exactly for lengths 4, 5, and 6 without manually
+//! reconstructing `len >= VALUE_SIZE`. Both minimum-length APIs use this one
+//! factored translation. It remains a zerocopy policy oracle: the safe
+//! language/library operations establish destination capacity, not that the
+//! public API ought to use this acceptance policy.
 //!
 //! Result-classification basis: `classify_write_result` exhaustively matches
 //! the target `Result` together with the API-policy success Boolean. Rust match
@@ -243,9 +250,8 @@
 //!       https://doc.rust-lang.org/1.93.0/std/macro.assert_eq.html
 //!       https://doc.rust-lang.org/1.93.0/std/cmp/trait.PartialEq.html#tymethod.eq
 //!       https://doc.rust-lang.org/1.93.0/std/primitive.usize.html#impl-PartialEq-for-usize
-//! [24]: https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#comparison-operators
-//!       https://doc.rust-lang.org/1.93.0/std/cmp/trait.PartialOrd.html#method.ge
-//!       https://doc.rust-lang.org/1.93.0/std/primitive.usize.html#impl-PartialOrd-for-usize
+//! [24]: https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.first_chunk
+//!       https://doc.rust-lang.org/1.93.0/std/option/enum.Option.html#method.is_some
 //! [25]: https://github.com/model-checking/kani/blob/kani-0.67.0/library/std/src/lib.rs#L19-L45
 //!       https://github.com/model-checking/kani/blob/kani-0.67.0/library/std/src/lib.rs#L91-L107
 //! [26]: https://github.com/model-checking/kani/blob/kani-0.67.0/docs/src/tutorial-kinds-of-failure.md#L1-L5
@@ -275,6 +281,13 @@ fn destination_len() -> usize {
     any_usize_inclusive(MAX_DST_LEN)
 }
 
+// This is a policy oracle, not evidence that zerocopy chose the right policy.
+// Safe `first_chunk` independently reports whether the actual passed slice has
+// room for a value-sized chunk [24], avoiding a duplicate manual inequality.
+fn minimum_length_policy_oracle(destination: &[u8]) -> bool {
+    destination.first_chunk::<VALUE_SIZE>().is_some()
+}
+
 // Factor the initial view's size and contents together; pointer identity stays
 // local because shared and mutable views expose different pointer types.
 fn assert_initial_u32_byte_view(bytes: &[u8], before: &[u8; VALUE_SIZE]) {
@@ -453,7 +466,7 @@ fn prove_into_bytes_write_to_prefix() {
     let before = copy_snapshot(&destination);
     let len = destination_len();
 
-    let expected_success = len >= VALUE_SIZE;
+    let expected_success = minimum_length_policy_oracle(&destination[..len]);
     let succeeded =
         classify_write_result(value.write_to_prefix(&mut destination[..len]), expected_success);
 
@@ -494,7 +507,7 @@ fn prove_into_bytes_write_to_suffix() {
     let before = copy_snapshot(&destination);
     let len = destination_len();
 
-    let expected_success = len >= VALUE_SIZE;
+    let expected_success = minimum_length_policy_oracle(&destination[..len]);
     let succeeded =
         classify_write_result(value.write_to_suffix(&mut destination[..len]), expected_success);