From 867d9c2605adb06887b46ad294a61b7420afb083 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser's Agent Date: Tue, 8 Sep 2026 23:51:33 +0000 Subject: [PATCH] [kani] Prove utility memory operations Replace the private raw copy helper with safe `copy_prefix`, prove its bounded frame behavior, and remove three caller unsafe blocks. Add concrete representation and mutation proofs for transmute helpers, plus sized, ZST, and plain-slice `new_box` smoke proofs. Document the remaining aliasing, provenance, allocator, and nested-DST limits. *Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: G4pavaeiw7kliymw4ujvmg43vcwah5v5p --- zerocopy/src/lib.rs | 21 +- zerocopy/src/proof_support.rs | 26 ++ zerocopy/src/util/mod.rs | 718 +++++++++++++++++++++++++++++++++- 3 files changed, 727 insertions(+), 38 deletions(-) diff --git a/zerocopy/src/lib.rs b/zerocopy/src/lib.rs index bc244b0150..d5c2d5dcbe 100644 --- a/zerocopy/src/lib.rs +++ b/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(()) } diff --git a/zerocopy/src/proof_support.rs b/zerocopy/src/proof_support.rs index 1a14f448f1..eeba4ea2a9 100644 --- a/zerocopy/src/proof_support.rs +++ b/zerocopy/src/proof_support.rs @@ -397,3 +397,29 @@ pub(crate) fn nonzero_u16_from_ne_bytes(bytes: [u8; 2]) -> Option(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())); +} diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs index bd0d83e78c..0d8b3a7b17 100644 --- a/zerocopy/src/util/mod.rs +++ b/zerocopy/src/util/mod.rs @@ -275,25 +275,11 @@ pub(crate) const fn min(a: NonZeroUsize, b: NonZeroUsize) -> NonZeroUsize { /// Copies `src` into the prefix of `dst`. /// -/// # Safety -/// -/// The caller guarantees that `src.len() <= dst.len()`. +/// Callers must ensure that `src.len() <= dst.len()`. #[inline(always)] -pub(crate) unsafe fn copy_unchecked(src: &[u8], dst: &mut [u8]) { +pub(crate) fn copy_prefix(src: &[u8], dst: &mut [u8]) { debug_assert!(src.len() <= dst.len()); - // SAFETY: This invocation satisfies the safety contract of - // copy_nonoverlapping [1]: - // - `src.as_ptr()` is trivially valid for reads of `src.len()` bytes - // - `dst.as_ptr()` is valid for writes of `src.len()` bytes, because the - // caller has promised that `src.len() <= dst.len()` - // - `src` and `dst` are, trivially, properly aligned - // - the region of memory beginning at `src` with a size of `src.len()` - // bytes does not overlap with the region of memory beginning at `dst` - // with the same size, because `dst` is derived from an exclusive - // reference. - unsafe { - core::ptr::copy_nonoverlapping(src.as_ptr(), dst.as_mut_ptr(), src.len()); - }; + dst.iter_mut().zip(src.iter()).for_each(|(dst, src)| *dst = *src); } /// Unsafely transmutes the given `src` into a type `Dst`. @@ -377,9 +363,11 @@ where /// # Safety /// /// `allocate` must be either `alloc::alloc::alloc` or -/// `alloc::alloc::alloc_zeroed`. The referent of the box returned by `new_box` -/// has the same bit-validity as the referent of the pointer returned by the -/// given `allocate` and sufficient size to store `T` with `meta`. +/// `alloc::alloc::alloc_zeroed`. Any `Box` returned by this function must +/// have a bit-valid referent with metadata `meta`. Thus `T` must permit the +/// corresponding initial memory state: its zero-byte representation for a +/// zero-sized instance, uninitialized bytes from `alloc`, or initialized +/// all-zero bytes from `alloc_zeroed`. #[must_use = "has no side effects (other than allocation)"] #[cfg(feature = "alloc")] #[inline] @@ -467,6 +455,696 @@ where Ok(unsafe { alloc::boxed::Box::from_raw(ptr.as_ptr()) }) } +#[cfg(kani)] +mod proofs { + use core::{convert::TryFrom as _, num::Wrapping}; + + use super::*; + use crate::{ + pointer::{BecauseImmutable, BecauseInvariantsEq, BecauseMutationCompatible}, + proof_support::{assert_same_u8_elements, assert_same_usize, copy_snapshot}, + }; + + // Configuration: The harnesses below use the common Kani CI configuration + // documented in `agent_docs/validation.md`: the CI-pinned Kani release and + // its bundled x86_64-unknown-linux-gnu compiler, the stable-compatible + // feature bundle, `-Zfunction-contracts`, and one layout selected by + // `--randomize-layout` per invocation. + // + // `copy_prefix` proof scope: + // + // Domain: Every source `[u8; 8]`, destination `[u8; 12]`, source length + // from 0 through 8, and destination length from the source length through + // 12. Both target slices and both safe-oracle slices are offset-zero + // prefixes of those fixed backing arrays. The proof uses only those arrays + // and fixed source and destination snapshots; it performs no dynamic + // allocation and has no explicit proof loop. Its unwind bound is 13, one + // more than the largest modeled slice, and applies to all target and oracle + // loops Kani reaches, with unwinding assertions enabled. + // Establishes: The copied prefix and every destination frame byte exactly + // match a safe copy, and the entire source equals its pre-call snapshot. + // Target mechanics: `copy_prefix` contains no unsafe operation. Safe + // `slice::iter_mut` visits the destination elements mutably while + // `slice::iter` visits the source elements by shared reference [26], `zip` + // pairs them until either iterator ends [27], and `for_each` applies the + // byte assignment to every pair [28]. + // The caller condition `src.len() <= dst.len()` therefore makes every + // source element participate. This safe iterator path is the target, not + // the expected-result oracle. + // Oracle: Safe `slice::copy_from_slice`, whose Rust 1.93 contract copies + // every element from an equal-length source [1], is applied to a separate + // destination copy. Shared and mutable `RangeTo` indexing selects + // the exact `..src_len` and `..dst_len` prefixes for the oracle and target + // inputs [12]; the domain bounds exclude its documented panic cases. The + // immutable `src_len` and `dst_len` selectors are `usize: Copy`, so each + // range expression copies their pre-call values under [19]; this is input + // construction, not an expectation reconstructed from target state. Both + // paths trust that same Rust indexing contract, which this proof does not + // itself establish. Before the call, ordinary `Copy` semantics for the + // fixed `[u8; 8]` source [19] create a separate snapshot through the shared + // `copy_snapshot`; comparing the source against it after the call + // independently supplies the source-frame oracle. + // Excludes: Inputs with `src.len() > dst.len()` (the debug assertion panics + // and the iterator body otherwise copies only the shorter length), larger + // fixed arrays, nonzero-offset or interior source and destination slices, + // preservation of frame bytes preceding such a destination slice, + // overlapping regions (which safe input references preclude), and aliasing + // or provenance properties outside Kani's model. This is not a generic + // contract proof. + // + // [1] Rust 1.93 specifies that `copy_from_slice` copies every element from + // `src` into the equal-length receiver: + // https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.copy_from_slice + // + // Transmutation proof scope: + // + // Domain: The value-to-bytes and shared-reference harnesses each cover + // every independently generated `u32`; the bytes-to-value harness covers + // every independently generated `[u8; 4]`; and the mutable-reference + // harness covers the full Cartesian product of every initial `u32` and + // every independently generated replacement `u32`. The reference + // harnesses view their respective source values as `Wrapping`. Each + // proof uses only fixed-size stack values, uses no `kani::assume`, performs + // no dynamic allocation, and has no explicit proof loop. The mutable + // harness's unequal-value `kani::cover!` is a reachability diagnostic and + // does not constrain that Cartesian domain. Primitive `u32` inequality + // classifies only this diagnostic [32]; expected-value assertions use the + // native-byte oracle instead. Every harness has unwind bound five, which + // also bounds any target or oracle loop Kani reaches, with unwinding + // assertions enabled. + // Establishes: Independently seeded value-to-bytes and bytes-to-value + // native representation contracts relative to independent pre-call + // snapshots, modeled address preservation, + // shared-reference returned-value and source final-state preservation + // relative to an independent pre-call snapshot, and mutable-reference + // mutation propagation. Neither value transmutation is used to construct + // the other's input. + // Oracle: Before any target call or assignment consumes a `Copy` operand, + // the shared `copy_snapshot` records that operand under its explicit + // `T: Copy` bound and documented copied-place rule [19]. Safe + // `u32::to_ne_bytes` and `u32::from_ne_bytes` directly map between each + // pre-call snapshot and its native-endian memory representation [2][3]; an + // explicit numbered-field `Wrapping { 0: replacement }` struct + // expression, its documented transparent layout, and Rust's tuple-field + // projection rule supply the reference expectations [25]. For the + // shared-reference harness, safe `copy_snapshot(&src)` records the initial + // `u32` before the target call under the helper's documented `T: Copy` + // semantics. After the call, the returned public field and source final + // state are each compared independently with that same target-independent + // snapshot; neither expectation is derived from the target or from + // post-call target state. The shared `assert_same_u32_value` oracle applies + // `u32::to_ne_bytes` [2] to each observed public field or scalar and + // compares the resulting ordered bytes through `assert_same_u8_elements`; + // it therefore avoids relying on `Wrapping::PartialEq` or an + // undocumented scalar equality. Rust's listed reference-to-raw-pointer + // coercions supply pointers to the source and returned referents [4]. The + // raw-pointer `cast` methods are documented as casts to another pointer + // type [5], and the Reference says a sized-to-sized pointer cast returns the + // pointer unchanged [6]. Raw-pointer equality is documented as address + // equality [5], so those operations provide an independent observer of the + // modeled addresses. The shared `dst` reference implements `Copy`; its + // coercion into `dst_ptr` copies that reference value under [19], allowing + // the later public-field observation without reconstructing a reference + // from the pointer. Requiring the two observed addresses to match is an + // explicit zerocopy same-address policy oracle under test, not an + // independent Rust-language oracle: Rust does not require this target to + // return a view at the source address. + // + // For mutation, dereferencing the local `dst: &mut Wrapping` denotes + // its pointed-to location and makes that location assignable [7]. Ordinary + // assignment then copies or moves the explicit + // `Wrapping { 0: replacement }` value into that place [8]. The expected + // replacement was independently snapshotted before this consuming + // assignment. These are safe Rust language operations independent of + // `transmute_mut`: they define the write through the returned reference. + // After that borrow ends, comparing `src` with the pre-assignment snapshot + // checks whether the target returned a view of the source storage. It does + // not derive the expected mutation from `transmute_mut` itself. + // TOOL/TCB boundary: Each harness reads, and the mutable harness writes, + // through the reference returned by the unsafe target. Rust's reference + // safety requirements include alignment, non-nullness, dereferenceability, + // valid representation, and a referent that remains live for the reference + // lifetime [33]. Kani does not completely check these properties [34]. The + // observations can test values and modeled addresses only under that + // premise; they cannot discharge it, because an invalid returned reference + // could make the observing Rust execution itself invalid. + // Excludes: Other source/destination types, invalid representations, and + // returned-reference lifetime, dereferenceability, provenance, or aliasing + // guarantees. In particular, the address operation used to define pointer + // equality discards provenance [5]; equal raw pointer addresses therefore + // do not establish equal provenance. These are not generic transmutation + // contract proofs. + // + // [2] Rust 1.93 specifies that `to_ne_bytes` returns the integer's memory + // representation as a native-byte-order array: + // https://doc.rust-lang.org/1.93.0/std/primitive.u32.html#method.to_ne_bytes + // + // [3] Rust 1.93 specifies that `from_ne_bytes` creates the native-endian + // integer value from its memory-representation array: + // https://doc.rust-lang.org/1.93.0/std/primitive.u32.html#method.from_ne_bytes + // + // [4] Rust 1.93 lists the coercions “`&T` to `*const T`” and “`&mut T` to + // `*mut T`”: + // https://doc.rust-lang.org/1.93.0/reference/type-coercions.html#coercion-types + // + // [5] Rust 1.93 says `cast`: “Casts to a pointer of another type.” Raw + // pointer `PartialEq` says: “Pointer equality is by address.” The `addr` + // documentation says “the provenance of the pointer is discarded” by that + // address operation: + // https://doc.rust-lang.org/1.93.0/std/primitive.pointer.html#method.cast + // https://doc.rust-lang.org/1.93.0/std/primitive.pointer.html#method.cast-1 + // https://doc.rust-lang.org/1.93.0/std/primitive.pointer.html#impl-PartialEq-for-*const+T + // https://doc.rust-lang.org/1.93.0/std/primitive.pointer.html#impl-PartialEq-for-*mut+T + // https://doc.rust-lang.org/1.93.0/std/primitive.pointer.html#method.addr + // + // [6] For sized source and destination types, Rust 1.93 says “the pointer + // is returned unchanged” by a pointer-to-pointer cast: + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#pointer-to-pointer-cast + // + // [7] For a dereference, Rust 1.93 specifies: + // + // When applied to a pointer it denotes the pointed-to location. + // + // It further specifies: + // + // If the expression is of type `&mut T` or `*mut T`, and is either a + // local variable, a (nested) field of a local variable or is a mutable + // place expression, then the resulting memory location can be assigned + // to. + // + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#r-expr.deref.result + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#r-expr.deref.mut + // + // [8] For assignment, Rust 1.93 specifies: + // + // Next it either copies or moves the assigned value to the assigned + // place. + // + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#r-expr.assign.behavior + // + // Allocation proof scope: + // + // Domain: Three fixed calls: `new_box::((), alloc_zeroed)`, + // `new_box::<[u8]>(4, alloc_zeroed)`, and `new_box::<()>((), alloc)`. The + // first two select the nonzero-size branch; the unit call selects the + // zero-size dangling-pointer branch. In the inspected source, each selected + // nonzero-size path reaches the single call through `allocate`, while the + // unit path bypasses it; the harnesses do not instrument allocator-call + // counts. Kani 0.67's tagged C runtime states that Rust's `__rust_alloc` + // and `__rust_alloc_zeroed` shims call `malloc` and `calloc` respectively + // [29]. We manually inspected the exact linked GOTO programs emitted for + // both nonzero-size harnesses after Function Pointer Removal: each indirect + // `allocate` parameter resolves to `std::alloc::alloc_zeroed`, then + // `__rust_alloc_zeroed`, then `calloc`; the unit harness's zero-size branch + // bypasses `allocate`. Kani 0.67 invokes CBMC with + // `--no-malloc-may-fail` [9], and the bundled CBMC 6.8.0's own `--help` + // defines that flag as "disable potential malloc failure" [10]. Inspecting + // CBMC's GOTO functions with that flag shows the built-in `calloc` model's + // nondeterministic may-fail mode fixed to zero. For these two calls, the + // asserted metadata policy supplies size four, so `calloc(1, 4)` also + // avoids the model's separate multiplication-overflow and maximum-size + // null returns. The link from the Rust calls through compiler/Kani lowering + // and those flag/model semantics is an audited TOOL/TCB premise, not a + // theorem of these harnesses. Under that premise, they do not model + // allocation failure. A Kani, compiler, linker, or allocation-model change + // requires repeating the call-graph and flag audit. + // + // The `u32` harness additionally quantifies over every replacement `u32` + // used by its post-allocation safe write/read check. Its equal-to and + // distinct-from the independently constructed initial-zero expectation + // covers witness the no-op and value-changing partitions; they are + // reachability diagnostics and do not constrain the every-`u32` domain. + // Primitive `u32` equality and inequality classify only those diagnostics + // [32]. Before assignment consumes the replacement, `copy_snapshot` records + // the expected value under its documented copied-place rule [19]; both + // covers and the post-assignment observation use that snapshot. Call + // metadata, allocated type and length, and the other oracle shapes are + // fixed. The first two target calls exercise Kani's allocation + // and normal deallocation models. There is no explicit proof loop. Each + // harness sets the loop-unwinding bound to five; common CI retains + // unwinding assertions for every translated reachable loop. This is not + // Rust panic-unwind coverage. + // Establishes: Under the metadata-policy and no-allocation-failure premises + // below, all three fixed calls return `Ok`. Every harness unconditionally + // asserts `result.is_ok()` before unwrapping. Rust specifies that `is_ok` + // is true for `Ok`, while `unwrap` returns an `Ok` value and panics for + // `Err` [11]. Thus an unexpected metadata, size, or allocation `Err` fails + // that assertion instead of silently skipping the content checks. On the + // proved `Ok` path, `unwrap` supplies the value they inspect. The `u32` + // call returns zeroed storage and, for every replacement `u32`, a safe + // `Box` write is read back exactly. The `[u8]` call returns four zero bytes + // with length four; the unit call returns a zero-sized referent. + // Metadata-policy oracle: before each target call, + // `assert_new_box_metadata_policy` receives an explicit pre-call metadata + // snapshot, reserving the original value for `new_box`, and a byte size + // computed by Rust's `size_of` or `size_of_val` operations [18][20]. For + // `[u8]`, the `size_of_val` input is a safely constructed four-element + // slice rather than a manual reconstruction of slice layout. Within the + // helper, explicit snapshots separate the metadata supplied to + // `is_valid_metadata` from the one supplied to `size_for_metadata`, and the + // size supplied to `TryFrom` from the final equality expectation. The + // associated metadata type implements this crate's `PointerMetadata` + // trait, whose `Copy` supertrait satisfies `copy_snapshot`; the size is a + // `usize`, whose `Copy` implementation is recorded in [19]. These are + // semantic-value snapshots, not claims of distinct storage identity or + // provenance. The helper checks that the independent size is representable + // as `isize` using safe `TryFrom` [23], then checks the + // `KnownLayout::is_valid_metadata` and `size_for_metadata` results used by + // `new_box`. `Option::is_some` and `unwrap` [31] make a missing size fail + // before the contained `usize` is compared through the equality chain in + // [30]. The `KnownLayout` contracts require acceptance and that exact size + // for these fixed `u32`, `[u8]`, and unit inputs. Because these checks + // consume zerocopy's own `KnownLayout` contract, they are explicitly policy + // premises, not independent evidence that its implementations are correct. + // They do establish, before the target call, that neither metadata check is + // an expected source of `Err`. + // + // Value oracle: Rust's repeat-array expression constructs the expected + // fixed arrays with the stated number of copies of zero [24]. Primitive + // `u32::from_ne_bytes` [3] independently maps four such bytes to the + // expected integer value. The shared `assert_same_u8_elements` [13]-[17], + // [30] supplies the expected slice length and ordered zero bytes, and + // `size_of_val` [18] observes the unit referent's size. The direct unit-size + // assertion also uses the documented `assert_eq!`/`usize::PartialEq` + // equality chain [30]. + // + // Box observation oracle: `Box` implements `Deref` and + // `DerefMut` [21]. Rust's dereference and assignment rules [7][8] specify + // the `*boxed` reads and write, while dereference coercion [22] supplies + // the `&Box<[u8]>` to `&[u8]` observation. These safe operations are + // independent of `new_box` and specify observations of a valid returned + // box. They cannot establish that `new_box` constructed a valid `Box`: if + // its raw-pointer, allocation, or referent obligations were already + // violated, these observations could themselves be outside Rust's valid + // execution model. + // Excludes: Configurations which permit modeled allocation failure, real + // resource exhaustion, and validation of the expected allocation-failure + // `Err` path. The required `Ok` result is conditional on the manually + // audited Rust-to-Kani-to-CBMC allocation bridge and Kani 0.67's CBMC model, + // not a claim that production allocation cannot fail. The harnesses do not + // prove that bridge, Kani's allocation shims, or the CBMC flag semantics. + // Also excluded are uninitialized non-ZST referents, arbitrary + // types/metadata, and nested slice DSTs (see + // https://github.com/google/zerocopy/pull/3630). In particular, these are + // behavioral smoke regressions, not proofs of the `Box::from_raw` + // provenance, alignment, ownership, or allocator/deallocator obligations + // called out by FIXME #429 above, nor of `new_box`'s overall soundness. + // + // [9] https://github.com/model-checking/kani/blob/kani-0.67.0/kani-driver/src/call_cbmc.rs#L213-L219 + // + // [10] `agent_docs/validation.md` records the exact bundled CBMC version and + // its inspected `--no-malloc-may-fail` / `--malloc-may-fail` help text. + // + // [11] Rust 1.93's `Result` contracts state: + // + // Returns `true` if the result is `Ok`. + // + // Returns the contained `Ok` value, consuming the `self` value. + // + // Panics if the value is an `Err`, with a panic message provided by the + // `Err`’s value. + // + // https://doc.rust-lang.org/1.93.0/std/result/enum.Result.html#method.is_ok + // https://doc.rust-lang.org/1.93.0/std/result/enum.Result.html#method.unwrap + + // Shared observation oracle: `assert_same_u8_elements` obtains both element + // counts through `slice::len` [13]; `assert_eq!` compares those counts using + // `usize::PartialEq` [30]. Safe `slice::iter` then yields every item in + // order [14], `Iterator::copied` copies those items, and `Iterator::eq` + // compares the two sequences [15] using primitive `u8` equality [16]. + // Fixed arrays reach this helper through the Reference's array-to-slice + // unsizing coercion [17]. These operations are independent of the zerocopy + // target, but not of the compiler, standard library, or Kani model. They + // observe element counts and ordered values, not storage identity or + // provenance. + // + // [12] Rust 1.93 defines `RangeTo` as including values below `end`, and its + // `SliceIndex<[T]>` implementation returns that prefix for shared and + // mutable indexing, panicking when `end` is out of bounds: + // https://doc.rust-lang.org/1.93.0/std/ops/struct.RangeTo.html + // https://doc.rust-lang.org/1.93.0/std/ops/struct.RangeTo.html#impl-SliceIndex%3C%5BT%5D%3E-for-RangeTo%3Cusize%3E + // + // [13] https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.len + // [14] https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.iter + // [15] https://doc.rust-lang.org/1.93.0/std/iter/trait.Iterator.html#method.copied + // and https://doc.rust-lang.org/1.93.0/std/iter/trait.Iterator.html#method.eq + // [16] https://doc.rust-lang.org/1.93.0/std/primitive.u8.html#impl-PartialEq-for-u8 + // [17] Rust 1.93 permits references to unsize at a coercion site and lists + // `[T; n]` to `[T]` as an unsized coercion: + // https://doc.rust-lang.org/1.93.0/reference/type-coercions.html#r-coerce.types.unsize + // https://doc.rust-lang.org/1.93.0/reference/type-coercions.html#r-coerce.unsize.slice + // + // Rust 1.93 specifies that `size_of_val` returns the size of the pointed-to + // value in bytes [18]. The unit allocation harness uses this only to + // observe the target referent's dynamic size. + // + // [18] https://doc.rust-lang.org/1.93.0/core/mem/fn.size_of_val.html + + // [19] The shared `copy_snapshot` helper has an explicit `T: Copy` bound + // and documents Rust 1.93's copied-place rule. Rust implements `Copy` for + // the proof's `u8`, `u32`, and `usize` scalars, shared references, and for + // `[T; N]` when `T: Copy`: + // https://doc.rust-lang.org/1.93.0/reference/expressions.html#moved-and-copied-types + // https://doc.rust-lang.org/1.93.0/std/primitive.array.html#impl-Copy-for-%5BT;+N%5D + // https://doc.rust-lang.org/1.93.0/std/primitive.u8.html#impl-Copy-for-u8 + // https://doc.rust-lang.org/1.93.0/std/primitive.u32.html#impl-Copy-for-u32 + // https://doc.rust-lang.org/1.93.0/std/primitive.usize.html#impl-Copy-for-usize + // https://doc.rust-lang.org/1.93.0/std/primitive.reference.html + // + // [20] Rust 1.93 specifies that `size_of` returns a type's size in bytes: + // https://doc.rust-lang.org/1.93.0/core/mem/fn.size_of.html + // + // [21] Rust 1.93's `Box` implementations dereference to `T` and permit + // mutable dereference: + // https://doc.rust-lang.org/1.93.0/alloc/boxed/struct.Box.html#impl-Deref-for-Box%3CT,+A%3E + // https://doc.rust-lang.org/1.93.0/alloc/boxed/struct.Box.html#impl-DerefMut-for-Box%3CT,+A%3E + // + // [22] Rust 1.93 permits `&T` to coerce to `&U` when + // `T: Deref`: + // https://doc.rust-lang.org/1.93.0/reference/type-coercions.html#r-coerce.types.deref + // + // [23] Rust 1.93's `TryFrom for isize` performs the checked integer + // conversion used by the metadata policy precheck: + // https://doc.rust-lang.org/1.93.0/std/primitive.isize.html#impl-TryFrom%3Cusize%3E-for-isize + + // [24] Rust 1.93 specifies: “`[a; b]` creates an array containing `b` + // copies of the value of `a`”: + // https://doc.rust-lang.org/1.93.0/reference/expressions/array-expr.html#array-expressions + + // [25] Rust 1.93 specifies explicit struct expressions, including numeric + // fields for tuple structs, and that tuple and tuple-struct fields are + // accessed with the number corresponding to the field's position: + // https://doc.rust-lang.org/1.93.0/reference/expressions/struct-expr.html#r-expr.struct.intro + // https://doc.rust-lang.org/1.93.0/reference/expressions/struct-expr.html#r-expr.struct.tuple-field + // https://doc.rust-lang.org/1.93.0/reference/expressions/tuple-expr.html#tuple-indexing-expressions + + // [26] https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.iter + // https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.iter_mut + // [27] https://doc.rust-lang.org/1.93.0/std/iter/trait.Iterator.html#method.zip + // [28] https://doc.rust-lang.org/1.93.0/std/iter/trait.Iterator.html#method.for_each + + // [29] Kani 0.67's tagged runtime implements `__rust_alloc` using `malloc` + // and `__rust_alloc_zeroed` using `calloc`: + // https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani/kani_lib.c#L31-L67 + + // [30] Rust 1.93 specifies that `slice::len` returns the number of elements, + // `assert_eq!` compares operands using `PartialEq`, and `usize` equality + // tests its two values for equality: + // https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.len + // 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 + + // [31] Rust 1.93 specifies that `Option::is_some` is true for `Some` and + // `Option::unwrap` returns the contained `Some` value or panics for `None`: + // https://doc.rust-lang.org/1.93.0/std/option/enum.Option.html#method.is_some + // https://doc.rust-lang.org/1.93.0/std/option/enum.Option.html#method.unwrap + + // [32] Rust 1.93 specifies `PartialEq::eq` and `PartialEq::ne`, and provides + // that implementation for `u32`: + // https://doc.rust-lang.org/1.93.0/std/cmp/trait.PartialEq.html#tymethod.eq + // https://doc.rust-lang.org/1.93.0/std/cmp/trait.PartialEq.html#method.ne + // https://doc.rust-lang.org/1.93.0/std/primitive.u32.html#impl-PartialEq-for-u32 + + // [33] Rust 1.93 lists the safety requirements for references: + // https://doc.rust-lang.org/1.93.0/std/primitive.reference.html#safety + + // [34] Kani documents the undefined-behavior checks it does and does not + // support; `agent_docs/validation.md` records the exact pinned-tool audit: + // https://model-checking.github.io/kani/undefined-behaviour.html + + fn assert_same_u32_value(actual: u32, expected: u32) { + assert_same_u8_elements(&actual.to_ne_bytes(), &expected.to_ne_bytes()); + } + + #[cfg(feature = "alloc")] + fn assert_new_box_metadata_policy(meta: T::PointerMetadata, expected_size: usize) + where + T: ?Sized + KnownLayout, + { + let metadata_for_size = copy_snapshot(&meta); + let expected_size_snapshot = copy_snapshot(&expected_size); + assert!(isize::try_from(expected_size).is_ok()); + assert!(T::is_valid_metadata(meta)); + let actual_size = T::size_for_metadata(metadata_for_size); + assert!(actual_size.is_some()); + assert_same_usize(actual_size.unwrap(), expected_size_snapshot); + } + + #[kani::proof] + #[kani::unwind(13)] + fn prove_copy_prefix_copies_prefix_and_preserves_frame() { + const SRC_CAPACITY: usize = 8; + const DST_CAPACITY: usize = 12; + + let src: [u8; SRC_CAPACITY] = kani::any(); + let original_src = copy_snapshot(&src); + let mut dst: [u8; DST_CAPACITY] = kani::any(); + let src_len: usize = kani::any(); + let dst_len: usize = kani::any(); + + kani::assume(src_len <= SRC_CAPACITY); + kani::assume(dst_len <= DST_CAPACITY); + kani::assume(src_len <= dst_len); + + kani::cover!(src_len == 0 && dst_len == 0); + kani::cover!(src_len == SRC_CAPACITY && src_len == dst_len); + kani::cover!(0 < src_len && src_len < dst_len && dst_len < DST_CAPACITY); + kani::cover!(src_len > 0 && src[0] != dst[0]); + + let mut expected_dst = copy_snapshot(&dst); + expected_dst[..src_len].copy_from_slice(&original_src[..src_len]); + + copy_prefix(&src[..src_len], &mut dst[..dst_len]); + + assert_same_u8_elements(&src, &original_src); + assert_same_u8_elements(&dst, &expected_dst); + } + + #[kani::proof] + #[kani::unwind(5)] + fn prove_transmute_unchecked_u32_to_bytes() { + let src: u32 = kani::any(); + let expected = copy_snapshot(&src).to_ne_bytes(); + + // SAFETY: `transmute_unchecked` statically checks that `[u8; 4]` and + // `u32` have the same size. `src` is initialized, and numeric bit + // validity is exactly that of an initialized byte array [1], so its + // representation is valid for `[u8; 4]`. + // + // [1] Per https://doc.rust-lang.org/1.93.0/reference/types/numeric.html#bit-validity: + // + // For every numeric type, `T`, the bit validity of `T` is + // equivalent to the bit validity of `[u8; size_of::()]`. An + // uninitialized byte is not a valid `u8`. + let bytes: [u8; 4] = unsafe { transmute_unchecked(src) }; + assert_same_u8_elements(&bytes, &expected); + } + + #[kani::proof] + #[kani::unwind(5)] + fn prove_transmute_unchecked_bytes_to_u32() { + // This consumer receives a fresh arbitrary representation, not the + // output of the opposite target transmutation. + let bytes: [u8; 4] = kani::any(); + let expected = u32::from_ne_bytes(copy_snapshot(&bytes)); + + // SAFETY: `transmute_unchecked` statically checks that `[u8; 4]` and + // `u32` have the same size. Every byte in `bytes` is initialized, and + // numeric bit validity is exactly that of an initialized byte array + // [1], so its representation is valid for `u32`. + // + // [1] Per https://doc.rust-lang.org/1.93.0/reference/types/numeric.html#bit-validity: + // + // For every numeric type, `T`, the bit validity of `T` is + // equivalent to the bit validity of `[u8; size_of::()]`. An + // uninitialized byte is not a valid `u8`. + let roundtrip: u32 = unsafe { transmute_unchecked(bytes) }; + assert_same_u32_value(roundtrip, expected); + } + + #[kani::proof] + #[kani::unwind(5)] + fn prove_transmute_ref_preserves_address_and_value() { + let src: u32 = kani::any(); + let original = copy_snapshot(&src); + let src_ptr: *const u32 = &src; + + // SAFETY: A type's layout includes its alignment [1], and + // `Wrapping` has the same layout as `u32` [2]. Their alignments + // are therefore equal, satisfying `transmute_ref`'s sole caller + // precondition. + // + // [1] Per https://doc.rust-lang.org/1.93.0/reference/type-layout.html: + // + // The layout of a type is its size, alignment, and the relative + // offsets of its fields. + // + // [2] Per https://doc.rust-lang.org/1.93.0/std/num/struct.Wrapping.html#layout-1: + // + // `Wrapping` is guaranteed to have the same layout and ABI as + // `T`. + let dst: &Wrapping = unsafe { transmute_ref::<_, _, BecauseImmutable>(&src) }; + let dst_ptr: *const Wrapping = dst; + + assert_eq!(src_ptr.cast::(), dst_ptr.cast::()); + assert_same_u32_value(dst.0, original); + assert_same_u32_value(src, original); + } + + #[kani::proof] + #[kani::unwind(5)] + fn prove_transmute_mut_preserves_address_and_mutates_source() { + let mut src: u32 = kani::any(); + let original = copy_snapshot(&src); + let replacement: u32 = kani::any(); + let expected_replacement = copy_snapshot(&replacement); + let src_ptr: *mut u32 = &mut src; + + { + // SAFETY: A type's layout includes its alignment [1], and + // `Wrapping` has the same layout as `u32` [2]. Their + // alignments are therefore equal, satisfying `transmute_mut`'s + // sole caller precondition. + // + // [1] Per https://doc.rust-lang.org/1.93.0/reference/type-layout.html: + // + // The layout of a type is its size, alignment, and the + // relative offsets of its fields. + // + // [2] Per https://doc.rust-lang.org/1.93.0/std/num/struct.Wrapping.html#layout-1: + // + // `Wrapping` is guaranteed to have the same layout and ABI + // as `T`. + let dst: &mut Wrapping = unsafe { + transmute_mut::<_, _, (BecauseMutationCompatible, BecauseInvariantsEq)>(&mut src) + }; + let dst_ptr: *mut Wrapping = dst; + + assert_eq!(src_ptr.cast::(), dst_ptr.cast::()); + assert_same_u32_value(dst.0, original); + *dst = Wrapping { 0: replacement }; + assert_same_u32_value(dst.0, expected_replacement); + } + + kani::cover!(expected_replacement != original); + assert_same_u32_value(src, expected_replacement); + } + + #[cfg(feature = "alloc")] + #[kani::proof] + #[kani::unwind(5)] + fn prove_new_box_zeroed_u32() { + let meta = (); + assert_new_box_metadata_policy::(copy_snapshot(&meta), mem::size_of::()); + + // SAFETY: This passes `alloc_zeroed` directly, one of the two allocator + // functions permitted by `new_box`. It returns initialized zeroed + // memory [1], and every initialized representation is valid for a + // numeric type such as `u32` [2]. + // + // [1] Per https://doc.rust-lang.org/1.93.0/std/alloc/fn.alloc_zeroed.html: + // + // Allocates zero-initialized memory with the global allocator. + // + // [2] Per https://doc.rust-lang.org/1.93.0/reference/types/numeric.html#bit-validity: + // + // For every numeric type, `T`, the bit validity of `T` is + // equivalent to the bit validity of `[u8; size_of::()]`. An + // uninitialized byte is not a valid `u8`. + // + // [3] Per https://doc.rust-lang.org/1.93.0/std/primitive.u32.html#method.from_ne_bytes: + // + // Creates a native endian integer value from its memory + // representation as a byte array in native endianness. + let result = unsafe { new_box::(meta, alloc::alloc::alloc_zeroed) }; + assert!(result.is_ok()); + + let mut boxed = result.unwrap(); + let expected = u32::from_ne_bytes([0; mem::size_of::()]); + assert_same_u32_value(*boxed, expected); + + let replacement: u32 = kani::any(); + let expected_replacement = copy_snapshot(&replacement); + kani::cover!(expected_replacement == expected); + kani::cover!(expected_replacement != expected); + *boxed = replacement; + assert_same_u32_value(*boxed, expected_replacement); + } + + #[cfg(feature = "alloc")] + #[kani::proof] + #[kani::unwind(5)] + fn prove_new_box_zst() { + let meta = (); + assert_new_box_metadata_policy::<()>(copy_snapshot(&meta), mem::size_of::<()>()); + + // SAFETY: This passes `alloc` directly, one of the two allocator + // functions permitted by `new_box`. The unit type has exactly one + // value [1] and occupies no bytes [2], so the resulting referent must + // be that valid value regardless of the allocator's byte contents. + // + // [1] Per https://doc.rust-lang.org/1.93.0/reference/types/tuple.html#unit: + // + // Its one value is also called unit or the unit value. + // + // [2] Per https://doc.rust-lang.org/1.93.0/reference/type-layout.html#tuple-layout: + // + // The exception to this is the unit tuple (`()`), which is + // guaranteed as a zero-sized type to have a size of 0 and an + // alignment of 1. + // + // The family-level `size_of_val` oracle [18] observes that size through + // the returned `Box`. + let result = unsafe { new_box::<()>(meta, alloc::alloc::alloc) }; + assert!(result.is_ok()); + + let boxed = result.unwrap(); + assert_same_usize(mem::size_of_val(&*boxed), 0); + } + + #[cfg(feature = "alloc")] + #[kani::proof] + #[kani::unwind(5)] + fn prove_new_box_zeroed_byte_slice() { + const LEN: usize = 4; + + let meta = LEN; + let expected = [0u8; LEN]; + // The explicit type invokes the documented array-to-slice coercion + // [17], avoiding `RangeFull` indexing as an unlisted oracle step. + let expected_slice: &[u8] = &expected; + let expected_size = mem::size_of_val(expected_slice); + assert_new_box_metadata_policy::<[u8]>(copy_snapshot(&meta), expected_size); + + // SAFETY: This passes `alloc_zeroed` directly, one of the two allocator + // functions permitted by `new_box`. It returns initialized zeroed + // memory [1]. Numeric bit validity is exactly the validity of an + // initialized byte array [2], so every element is a valid `u8`; slices + // have the layout of their array section [3]. + // + // [1] Per https://doc.rust-lang.org/1.93.0/std/alloc/fn.alloc_zeroed.html: + // + // Allocates zero-initialized memory with the global allocator. + // + // [2] Per https://doc.rust-lang.org/1.93.0/reference/types/numeric.html#bit-validity: + // + // For every numeric type, `T`, the bit validity of `T` is + // equivalent to the bit validity of `[u8; size_of::()]`. An + // uninitialized byte is not a valid `u8`. + // + // [3] Per https://doc.rust-lang.org/1.93.0/reference/type-layout.html#slice-layout: + // + // Slices have the same layout as the section of the array they + // slice. + let result = unsafe { new_box::<[u8]>(meta, alloc::alloc::alloc_zeroed) }; + assert!(result.is_ok()); + + let boxed = result.unwrap(); + assert_same_u8_elements(&boxed, &expected); + } +} + mod len_of { use super::*;