diff --git a/zerocopy/src/lib.rs b/zerocopy/src/lib.rs index 909c42deec..bc244b0150 100644 --- a/zerocopy/src/lib.rs +++ b/zerocopy/src/lib.rs @@ -364,6 +364,8 @@ mod macros; #[cfg_attr(not(zerocopy_unstable_ptr), doc(hidden))] #[cfg_attr(doc_cfg, doc(cfg(zerocopy_unstable_ptr)))] pub mod pointer; +#[cfg(kani)] +mod proof_support; mod r#ref; mod split_at; // FIXME(#252): If we make this pub, come up with a better name. diff --git a/zerocopy/src/proof_support.rs b/zerocopy/src/proof_support.rs new file mode 100644 index 0000000000..129b80c946 --- /dev/null +++ b/zerocopy/src/proof_support.rs @@ -0,0 +1,31 @@ +// SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT +// +// Copyright 2026 The Fuchsia Authors +// +// Licensed under the 2-Clause BSD License , Apache License, Version 2.0 +// , or the MIT +// license , at your option. +// This file may not be copied, modified, or distributed except according to +// those terms. + +//! Shared mechanics for Kani proofs. +//! +//! Keep semantic expectations in their individual proof modules unless Rust +//! itself defines the expectation here. + +// Take a pre-operation value snapshot using safe Rust language operations, +// independently of any zerocopy target. Applying unary `*` to `value: &T` +// denotes the referenced location [1]. Because `*value` is the final operand +// of the function-body block, the block evaluates it in value-expression +// context [2]. Evaluating a place expression in that context copies it instead +// of moving it when the type implements `Copy` [3]; the bound makes that +// premise explicit for every use. This records a value, not allocation +// identity or independent storage for pointer-bearing `Copy` types. +// +// [1] https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#r-expr.deref.result +// [2] https://doc.rust-lang.org/1.93.0/reference/expressions/block-expr.html#r-expr.block.value +// [3] https://doc.rust-lang.org/1.93.0/reference/expressions.html#moved-and-copied-types +pub(crate) fn copy_snapshot(value: &T) -> T { + *value +} diff --git a/zerocopy/src/split_at.rs b/zerocopy/src/split_at.rs index 1695a0d740..dde6015239 100644 --- a/zerocopy/src/split_at.rs +++ b/zerocopy/src/split_at.rs @@ -950,6 +950,620 @@ where } } +#[cfg(kani)] +mod proofs { + use super::*; + use crate::proof_support::copy_snapshot; + + // Configuration: Uses 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. + // + // Domain: Each harness considers every initialized `[u32; 8]`, every + // source length in `0..=8`, and every split point in + // `0..=source.len()`. The mutable consumer additionally considers every + // pair of `u32` values written through its left and right results. Separate + // harnesses cover shared and mutable slices. The two calls to + // `assume_usize_at_most` in `any_slice_split_case` express exactly the + // finite length bounds: they pass independently evaluated Rust `usize` + // ordering results to Kani's assumption primitive as documented below; + // neither mutation value is constrained. The common covers witness empty, + // full, leading, trailing, and interior partitions. The two + // mutable-consumer covers use `partition_first_value_oracle` to separately + // witness a nonempty left or right partition whose first value changes; + // covers establish reachability only and do not narrow the universal + // mutation domain. + // + // Symbolic-input basis and TOOL boundary: Kani 0.67 documents + // `any::()` as representing every valid `T`. Its exact `Arbitrary` + // implementations for the unsigned primitive types and arrays route these + // `[u32; CAPACITY]`, `usize`, and `u32` requests through the raw-any path + // [21][22]. Kani lowers that path's `AnyRawHook` to a destination-typed + // nondeterministic expression, and its pinned CBMC 6.8.0 model permits + // separate nondeterministic calls to make different choices [23]. We + // accept as a TOOL/TCB premise, rather than a conclusion of these + // harnesses, that each dynamic `kani::any` evaluation is a fresh, mutually + // unconstrained valid choice. Thus the first three calls in + // `any_slice_split_case` initially range over the Cartesian product of all + // valid `[u32; CAPACITY]`, `usize`, and `usize` values; the two assumptions + // retain exactly `source_len <= CAPACITY && split <= source_len`. The + // mutable-consumer harness's later two calls independently range over the + // complete `u32` x `u32` value product and are not constrained. + // + // `kani::any` supplies initialized, valid values; it does not generate an + // invalid or uninitialized value [21]. That restriction omits no valid + // safe value of these exact unsigned integer and fixed-array types, but it + // means these harnesses say nothing about invalid or uninitialized source + // states. Kani's incomplete invalid-value, uninitialized-memory, aliasing, + // provenance, and reference-validity analyses remain explicit TOOL/TCB + // limits [24]. + // + // Proof decomposition: + // - The two `split_at_*_unchecked` harnesses call only the descriptor + // producer under proof. They inspect the private `Split` fields and + // establish that `source` preserves the input slice's contents, length, + // and start address and that `l_len` equals the requested split point. + // Those expected fields are explicitly a zerocopy representation-policy + // oracle, not Rust-level evidence: the local `Split` definition documents + // `source` as the source slice-DST pointer and `l_len` as the future left + // length, with `l_len <= source.len()`, while `Split::new` says it produces + // a `Split` of the supplied `source` with the supplied `l_len`. Direct + // field-pattern observation bypasses every descriptor consumer. The + // shared producer compares contents against an independent pre-call value + // snapshot; this is a final-state comparison and does not establish the + // absence of a transient illicit write followed by restoration. The + // mutable producer additionally checks that every element of the complete + // backing array has its original value after descriptor construction. + // This is an explicit zerocopy final-state preservation policy, grounded + // in the operation's documented role of packaging the supplied source and + // length. Neither check observes intermediate states or establishes the + // absence of writes. No safe Rust operation independently chooses this + // policy for a zerocopy producer. + // - The two `via_unchecked` harnesses construct a known-good `Split` + // literal without calling either descriptor producer. They establish + // exact returned lengths and contents for every partition; start + // addresses for nonempty partitions; contiguity when both partitions are + // nonempty; and the source endpoint via whichever terminal partition is + // nonempty. The mutable harness also establishes writes through both + // results and the frame condition for the entire backing array. No + // address is asserted for an empty returned partition. + // Thus no harness can pass because of compensating producer and consumer + // defects. + // + // Allocation, source-level size, and loop bounds: The shared descriptor + // and mutable descriptor harnesses each use two fixed `[u32; 8]` stack + // arrays, the shared consumer uses one, and the mutable consumer uses three. + // No harness requests dynamic allocation. Every slice passed to a target, + // oracle, fill, or elementwise observation has length at most 8. On the + // pinned target, each array is 32 bytes, the case producer's + // `([u32; 8], usize, usize)` value is 48 bytes, and `PartitionOracle` is 64 + // bytes. Thus `PartitionOracle`, not a backing array, is the largest + // explicitly named fixed-size Rust value in these harnesses. Every harness + // calls `assert_fixed_storage_sizes`, which uses + // `size_of` ("Returns the size of a type in bytes" [13]) to fail closed if + // any of those three concrete sizes differs. All size and length equality + // assertions below use the factored `assert_same_usize`: `assert_eq!` + // compares through `PartialEq`, and `usize::PartialEq` tests the two values + // for equality [14]. That helper supplies only equality mechanics; each + // caller separately supplies a compiler fact, std oracle, or explicit + // zerocopy policy expectation. This is a source-level bound, not a claim + // about compiler-generated temporaries or stack-frame layout. + // Separately, each harness sets the conservative bound `unwind(33)`. That + // bound is not derived from the storage size, and the proof does not assume + // how the compiler or Kani lowers these operations: successful unwinding + // assertions establish that 33 is sufficient for every loop reachable in + // this exact modeled configuration. They do not establish that 33 is the + // exact or minimum sufficient bound. + // + // Oracle: Rust 1.93 identifies `usize` as an unsigned integer type, and its + // `PartialOrd::{lt, le, gt}` implementations test less than, less than or + // equal to, and greater than and are used by the corresponding `<`, `<=`, + // and `>` operators [16]. `assume_usize_at_most` first evaluates `<=` to a + // `bool`, then passes the result to `kani::assume`. Kani 0.67 documents + // that this makes the assumption valid on subsequent paths and + // successfully exits paths on which it is false [17]. Thus the first call + // retains exactly `source_len` in `0..=CAPACITY`; the second retains exactly + // `split` in `0..=source_len`. This is independent of the zerocopy target, + // but remains conditional on Kani's translation of its assumption + // primitive as part of the documented tool boundary. These assumptions + // define the proof domain; they do not themselves prove either inequality, + // and an impossible assumption could otherwise make later checks vacuous. + // The fail-closed cover checks described in `agent_docs/validation.md` + // separately establish reachability of the documented partitions. + // + // Source-prefix bridge: Every target source is constructed from the + // complete `[u32; CAPACITY]` with `&values[..source_len]` or its mutable + // counterpart. Rust 1.93 specifies that `..source_len` is a `RangeTo` and, + // when used as a slicing index, produces the slice of all array elements + // before `source_len`; its `SliceIndex<[T]>` implementation has output + // `[T]` and documents an out-of-bounds end as the panic condition [19]. The + // first domain assumption establishes `source_len <= CAPACITY`, so these + // constructions select exactly the first `source_len` elements. Since + // `slice::len` reports a slice's element count [14], each constructed + // source has `source.len() == source_len`. The second domain assumption + // therefore entails the unchecked-call precondition + // `split <= source.len()`. This safe language/library bridge calls no + // zerocopy target; it trusts the cited Rust contract and Kani's model of the + // slicing operation. + // + // Safe Rust 1.93 `slice::split_at` and `slice::split_at_mut` are + // independent of zerocopy and supply the expected partitions [1][2]: + // + // Divides one slice into two at an index. + // + // Divides one mutable slice into two at an index. + // + // Both contracts continue: + // + // The first will contain all indices from `[0, mid)` (excluding the + // index `mid` itself) and the second will contain all indices from + // `[mid, len)` (excluding the index `len` itself). + // + // `slice::as_ptr` and `slice::as_ptr_range` independently supply address + // observations [3][4]: + // + // Returns a raw pointer to the slice’s buffer. + // + // Returns the two raw pointers spanning the slice. + // + // The latter contract continues: + // + // The returned range is half-open, which means that the end pointer + // points one past the last element of the slice. + // + // Every pointer assertion is factored through `core::ptr::eq`, whose Rust + // 1.93 contract says [10]: + // + // Compares raw pointers for equality. + // + // The Rust Reference specifies that raw pointers are compared by their + // address rather than their pointed-to value [11]. All pointers compared + // here are thin `*const u32` pointers, so no wide-pointer metadata is + // involved. Safe `slice::len` determines whether each std-oracle partition + // is nonempty. Each target length is checked against that oracle before its + // own `len() != 0` gate, so a target defect cannot suppress an applicable + // address assertion by reporting an empty partition. The `Option` fields + // record only that applicability: `assert_present_u32_address` + // pattern-matches the gate and fails on `None`, rather than using `Option` + // equality. Both address helpers call only this safe `core` operation and + // no zerocopy target. Pointer comparison ignores provenance [12], so these + // assertions establish only equality of Kani's modeled addresses. They do + // not prove allocation identity, compatible provenance, dereferenceability, + // aliasing, or reference validity. + // + // Safe `slice::fill` supplies the write oracle [5]: + // + // Fills `self` with elements by cloning `value`. + // + // For primitive `u32`, the versioned `Clone` implementation returns + // `*self`, and `u32` implements `Copy`; each cloned fill element is + // therefore exactly the independently generated symbolic input rather + // than a second zerocopy policy premise [15]. + // + // The mutation covers classify first-element changes through + // `partition_first_value_oracle`, not direct array indexing. The helper + // explicitly coerces the complete array to a slice [9], calls + // `split_at(source_len)`, then calls `split_at(split)` on that prefix [1]. + // `source_len <= CAPACITY` makes the first split nonpanicking, and + // `split <= source_len` does the same for the second. Under the stricter + // cover gates, `split > 0` makes the left `[0, split)` partition nonempty, + // while `split < source_len` makes the right `[split, source_len)` partition + // nonempty. Safe `slice::first` returns that partition's first element or + // `None` exactly when it is empty, and `Option::copied` copies the observed + // `u32` value [18]. `observed_first_value_changes` then uses + // `Option::is_some_and`, whose documented contract requires both a `Some` + // value and a true predicate; primitive `u32`'s `PartialEq::ne` + // implementation supplies the `original != replacement` predicate + // [8][18]. Thus the helper returns true exactly when the safe slice + // observation is present and differs from the independently generated + // replacement. The helpers and gates ground the two cover classifications + // in safe Rust observations; as with all covers here, they establish + // reachability only. + // + // Contents and the whole-array final-state frame use + // `assert_same_u32_elements`, not slice or array `PartialEq`. Safe + // `slice::iter` returns an iterator which + // “yields all items from start to end” [6]; `Iterator::copied` “copies all + // of its elements,” and `Iterator::eq` determines whether one iterator's + // elements equal another's [7]. `u32::eq` tests two `u32` values for + // equality [8]. The helper obtains each element count through `slice::len` + // and compares those counts through `assert_same_usize` [14], so these + // rules establish the same ordered `u32` values. Whole arrays reach the + // helper through the Reference's `[T; n]` to `[T]` unsizing coercion [9]. + // These safe operations do not call zerocopy and are independent value + // oracles; they establish neither allocation identity nor aliasing or + // provenance. + // + // Every complete-array duplication used by these proofs goes through the + // shared `copy_snapshot`: the shared descriptor harness snapshots its input, + // the mutable descriptor harness initializes its target from `original`, and + // the mutable consumer harness initializes both its target and independent + // expected state from `original`. The helper's own documentation grounds its + // dereference, block-result, and `Copy` operations in Rust 1.93 contracts. + // Arrays implement `Copy` when their element type does, and `u32` implements + // `Copy` [15][20]. Each result is therefore an independent value observation + // rather than an alias of the source. This language-level premise establishes + // neither distinct allocation identity nor provenance, and remains + // conditional on Kani's incomplete aliasing and reference-validity model as + // stated in the exclusions below. + // + // Each descriptor-producer harness captures `source.as_ptr()` from the + // exact source slice descriptor before supplying that descriptor to the + // target. Its address assertion therefore establishes only relative + // preservation of that modeled input address, including for an empty + // source; it does not assert one canonical address for every empty slice. + // No cited address contract selects a unique buffer address for an empty + // returned partition. `partition_oracle` therefore records expected + // pointers only for nonempty partitions, and `assert_partitions` gates every + // returned pointer assertion accordingly. Empty cases still establish + // exact lengths and contents. + // + // [1] https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.split_at + // [2] https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.split_at_mut + // [3] https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.as_ptr + // [4] https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.as_ptr_range + // [5] https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.fill + // [6] https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.iter + // [7] 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 + // [8] https://doc.rust-lang.org/1.93.0/std/primitive.u32.html#impl-PartialEq-for-u32 + // [9] https://doc.rust-lang.org/1.93.0/reference/type-coercions.html#unsized-coercions + // [10] https://doc.rust-lang.org/1.93.0/std/ptr/fn.eq.html + // [11] https://doc.rust-lang.org/1.93.0/reference/types/pointer.html#r-type.pointer.raw.cmp + // [12] https://doc.rust-lang.org/1.93.0/std/ptr/index.html#provenance + // [13] https://doc.rust-lang.org/1.93.0/std/mem/fn.size_of.html + // [14] 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 + // [15] https://doc.rust-lang.org/1.93.0/std/primitive.u32.html#impl-Clone-for-u32 + // https://doc.rust-lang.org/1.93.0/std/primitive.u32.html#impl-Copy-for-u32 + // [16] https://doc.rust-lang.org/1.93.0/std/primitive.usize.html + // https://doc.rust-lang.org/1.93.0/std/primitive.usize.html#impl-PartialOrd-for-usize + // [17] https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/lib.rs#L139-L167 + // [18] https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.first + // https://doc.rust-lang.org/1.93.0/std/option/enum.Option.html#method.copied + // https://doc.rust-lang.org/1.93.0/std/option/enum.Option.html#method.is_some_and + // [19] 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 + // [20] https://doc.rust-lang.org/1.93.0/std/primitive.array.html#impl-Copy-for-%5BT;+N%5D + // [21] https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/lib.rs#L255-L279 + // https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/arbitrary.rs#L32-L77 + // [22] https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/arbitrary.rs#L125-L132 + // https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/lib.rs#L333-L367 + // [23] https://github.com/model-checking/kani/blob/kani-0.67.0/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs#L334-L375 + // https://github.com/model-checking/kani/blob/kani-0.67.0/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs#L1034-L1044 + // https://github.com/model-checking/kani/blob/kani-0.67.0/kani-dependencies#L1-L3 + // https://github.com/diffblue/cbmc/blob/cbmc-6.8.0/doc/cprover-manual/modeling-nondeterminism.md#L7-L13 + // https://github.com/diffblue/cbmc/blob/cbmc-6.8.0/doc/cprover-manual/modeling-nondeterminism.md#L46-L59 + // [24] https://github.com/model-checking/kani/blob/kani-0.67.0/docs/src/undefined-behaviour.md#L22-L42 + // https://github.com/model-checking/kani/blob/kani-0.67.0/docs/src/rust-feature-support.md#L97-L105 + // + // Excludes: Other element types (including ZSTs), larger slices, custom + // slice DSTs and their padding (see #3630), other targets/layouts, and the + // aliasing, provenance, and reference-validity obligations that Kani does + // not fully model. Pointer equality checks Kani's modeled addresses, not + // provenance. These harnesses do not exercise the checked + // `SplitAt::split_at` or `SplitAt::split_at_mut` entry points, or + // `Split::{via_immutable, via_into_bytes, via_unaligned, + // via_runtime_check}` for either receiver mutability. A successful unwind + // check applies only to this bounded domain; it is not evidence for larger + // slices. Returned empty-slice pointer identity and exact/minimal unwind + // bounds are also excluded. This is not a generic `SplitAt` theorem. + const CAPACITY: usize = 8; + + struct PartitionOracle { + left_len: usize, + right_len: usize, + left_start: Option<*const u32>, + right_start: Option<*const u32>, + source_end: Option<*const u32>, + } + + fn assert_same_usize(actual: usize, expected: usize) { + assert_eq!(actual, expected); + } + + fn assert_fixed_storage_sizes() { + assert_same_usize(core::mem::size_of::<[u32; CAPACITY]>(), 32); + assert_same_usize(core::mem::size_of::<([u32; CAPACITY], usize, usize)>(), 48); + assert_same_usize(core::mem::size_of::(), 64); + } + + // Domain-bound mechanism: Rust's `usize::PartialOrd` supplies the Boolean + // ordering observation [16], and Kani consumes that already-evaluated + // observation as an assumption on subsequent paths [17]. + fn assume_usize_at_most(value: usize, upper: usize) { + let value_is_at_most_upper = value <= upper; + kani::assume(value_is_at_most_upper); + } + + fn any_slice_split_case() -> ([u32; CAPACITY], usize, usize) { + assert_fixed_storage_sizes(); + let values = kani::any(); + let source_len: usize = kani::any(); + assume_usize_at_most(source_len, CAPACITY); + let split: usize = kani::any(); + assume_usize_at_most(split, source_len); + + kani::cover!(source_len == 0); + kani::cover!(source_len == CAPACITY); + kani::cover!(source_len > 0 && split == 0); + kani::cover!(source_len > 0 && split == source_len); + kani::cover!(split > 0 && split < source_len); + + (values, source_len, split) + } + + fn partition_first_value_oracle( + values: &[u32; CAPACITY], + source_len: usize, + split: usize, + ) -> (Option, Option) { + let values: &[u32] = values; + let (source, _) = values.split_at(source_len); + let (left, right) = source.split_at(split); + (left.first().copied(), right.first().copied()) + } + + fn observed_first_value_changes(first: Option, replacement: u32) -> bool { + first.is_some_and(|original| original != replacement) + } + + fn partition_oracle(source: &[u32], split: usize) -> PartitionOracle { + let (left, right) = source.split_at(split); + PartitionOracle { + left_len: left.len(), + right_len: right.len(), + left_start: if left.len() == 0 { None } else { Some(left.as_ptr()) }, + right_start: if right.len() == 0 { None } else { Some(right.as_ptr()) }, + source_end: if source.len() == 0 { None } else { Some(source.as_ptr_range().end) }, + } + } + + fn assert_same_u32_elements(actual: &[u32], expected: &[u32]) { + assert_same_usize(actual.len(), expected.len()); + assert!(actual.iter().copied().eq(expected.iter().copied())); + } + + fn assert_same_u32_address(actual: *const u32, expected: *const u32) { + assert!(core::ptr::eq(actual, expected)); + } + + fn assert_present_u32_address(actual: *const u32, expected: Option<*const u32>) { + match expected { + Some(expected) => assert_same_u32_address(actual, expected), + None => panic!("nonempty partition has no oracle address"), + } + } + + // Zerocopy representation-policy oracle: the local `Split` representation + // stores its source pointer and future-left length, and `Split::new` says it + // produces a `Split` of the supplied arguments. This checks that policy by + // direct field observation; it is not an independent Rust layout oracle. + fn assert_split_descriptor_policy( + actual_source: &[u32], + actual_l_len: usize, + expected_contents: &[u32], + expected_source: *const u32, + expected_l_len: usize, + ) { + assert_same_u32_elements(actual_source, expected_contents); + assert_same_u32_address(actual_source.as_ptr(), expected_source); + assert_same_usize(actual_l_len, expected_l_len); + } + + fn assert_partitions( + original: &[u32; CAPACITY], + source_len: usize, + split: usize, + oracle: PartitionOracle, + left: &[u32], + right: &[u32], + ) { + let (expected_left, expected_right) = original[..source_len].split_at(split); + assert_same_u32_elements(left, expected_left); + assert_same_u32_elements(right, expected_right); + assert_same_usize(left.len(), oracle.left_len); + assert_same_usize(right.len(), oracle.right_len); + // Gate pointer observations through the already documented `len` + // oracle. The preceding equalities make a target length disagreement + // fail before a nonempty expected partition could be skipped. + if left.len() != 0 { + assert_present_u32_address(left.as_ptr(), oracle.left_start); + } + if right.len() != 0 { + assert_present_u32_address(right.as_ptr(), oracle.right_start); + assert_present_u32_address(right.as_ptr_range().end, oracle.source_end); + } else if left.len() != 0 { + assert_present_u32_address(left.as_ptr_range().end, oracle.source_end); + } + if left.len() != 0 && right.len() != 0 { + assert_same_u32_address(left.as_ptr_range().end, right.as_ptr()); + } + } + + // Zerocopy behavior-policy oracle: after constructing a mutable `Split` + // descriptor, every element of the complete backing array must have its + // original value. This compares only the final state; temporary writes + // followed by restoration are outside the observation. The ordered-value + // helper supplies comparison mechanics, but no safe Rust contract + // independently chooses this policy for the zerocopy target. + fn assert_mutable_descriptor_post_state_policy( + actual: &[u32; CAPACITY], + original: &[u32; CAPACITY], + ) { + assert_same_u32_elements(actual, original); + } + + fn apply_mutation_oracle( + expected: &mut [u32; CAPACITY], + source_len: usize, + split: usize, + left_value: u32, + right_value: u32, + ) { + let (left, right) = expected[..source_len].split_at_mut(split); + left.fill(left_value); + right.fill(right_value); + } + + #[kani::proof] + #[kani::unwind(33)] + fn prove_slice_split_at_unchecked_descriptor() { + let (values, source_len, split) = any_slice_split_case(); + let original = copy_snapshot(&values); + let source = &values[..source_len]; + let expected_source = source.as_ptr(); + // SAFETY: `any_slice_split_case` passes the independently evaluated + // Rust `split <= source_len` result to Kani through the factored + // assumption mechanism documented above. The factored source-prefix + // bridge establishes `source.len() == source_len`, so this entails the + // bound required by `SplitAt::split_at_unchecked` and exactly the bound + // on the standard slice operation [1]. + // + // [1] Per https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.split_at_unchecked: + // + // The caller has to ensure that `0 <= mid <= self.len()`. + let parts = unsafe { SplitAt::split_at_unchecked(source, split) }; + let Split { source: actual_source, l_len: actual_l_len } = parts; + assert_split_descriptor_policy( + actual_source, + actual_l_len, + &original[..source_len], + expected_source, + split, + ); + } + + #[kani::proof] + #[kani::unwind(33)] + fn prove_slice_split_at_mut_unchecked_descriptor() { + let (original, source_len, split) = any_slice_split_case(); + let mut values = copy_snapshot(&original); + { + let source = &mut values[..source_len]; + // Capture the address from the exact slice descriptor supplied to + // the target. This remains meaningful when the slice is empty even + // though no contract selects one canonical address for all empty + // slices. + let expected_source = source.as_ptr(); + // SAFETY: `any_slice_split_case` passes the independently evaluated + // Rust `split <= source_len` result to Kani through the factored + // assumption mechanism documented above. The factored source- + // prefix bridge establishes `source.len() == source_len`, so this + // entails the bound required by + // `SplitAt::split_at_mut_unchecked` and exactly the bound on the + // standard mutable slice operation [1]. + // + // [1] Per https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.split_at_mut_unchecked: + // + // The caller has to ensure that `0 <= mid <= self.len()`. + let parts = unsafe { SplitAt::split_at_mut_unchecked(source, split) }; + let Split { source: actual_source, l_len: actual_l_len } = parts; + assert_split_descriptor_policy( + actual_source, + actual_l_len, + &original[..source_len], + expected_source, + split, + ); + } + assert_mutable_descriptor_post_state_policy(&values, &original); + } + + #[kani::proof] + #[kani::unwind(33)] + fn prove_split_via_unchecked_shared() { + let (values, source_len, split) = any_slice_split_case(); + let source = &values[..source_len]; + let oracle = partition_oracle(source, split); + + // This literal is the known-good consumer input, not an invocation of + // either descriptor producer under proof. `any_slice_split_case` + // establishes `split <= source_len` through the factored Rust-ordering/ + // Kani-assumption mechanism above; the source-prefix bridge establishes + // `source.len() == source_len`. Together these establish the private + // `Split` invariant `split <= source.len()`. + let parts = Split { source, l_len: split }; + + // SAFETY: The array and slice layout guarantees [1] place each element + // immediately after the last, so the two portions have no overlapping + // padding. This satisfies `Split::via_unchecked`'s conditional + // no-overlap precondition. + // + // [1] Per https://doc.rust-lang.org/1.93.0/reference/type-layout.html#array-layout + // and https://doc.rust-lang.org/1.93.0/reference/type-layout.html#slice-layout: + // + // An array of `[T; N]` has a size of `size_of::() * N` and + // the same alignment of `T`. + // + // Arrays are laid out so that the zero-based `nth` element of the + // array is offset from the start of the array by + // `n * size_of::()` bytes. + // + // Slices have the same layout as the section of the array they + // slice. + let (left, right) = unsafe { parts.via_unchecked() }; + assert_partitions(&values, source_len, split, oracle, left, right); + } + + #[kani::proof] + #[kani::unwind(33)] + fn prove_split_via_unchecked_mut() { + let (original, source_len, split) = any_slice_split_case(); + let mut values = copy_snapshot(&original); + let left_value: u32 = kani::any(); + let right_value: u32 = kani::any(); + let mut expected_values = copy_snapshot(&original); + apply_mutation_oracle(&mut expected_values, source_len, split, left_value, right_value); + let (left_first, right_first) = partition_first_value_oracle(&original, source_len, split); + + kani::cover!(split > 0 && observed_first_value_changes(left_first, left_value)); + kani::cover!(split < source_len && observed_first_value_changes(right_first, right_value)); + + { + let oracle = partition_oracle(&values[..source_len], split); + let source = &mut values[..source_len]; + + // This literal is the known-good consumer input, not an invocation + // of either descriptor producer under proof. + // `any_slice_split_case` establishes `split <= source_len` through + // the factored Rust-ordering/Kani-assumption mechanism above; the + // source-prefix bridge establishes `source.len() == source_len`. + // Together these establish the private `Split` invariant + // `split <= source.len()`. + let parts = Split { source, l_len: split }; + + // SAFETY: The array and slice layout guarantees [1] place each + // element immediately after the last, so the two exclusive + // portions have no overlapping padding. This satisfies + // `Split::via_unchecked`'s no-overlap precondition. + // + // [1] Per https://doc.rust-lang.org/1.93.0/reference/type-layout.html#array-layout + // and https://doc.rust-lang.org/1.93.0/reference/type-layout.html#slice-layout: + // + // An array of `[T; N]` has a size of `size_of::() * N` and + // the same alignment of `T`. + // + // Arrays are laid out so that the zero-based `nth` element of + // the array is offset from the start of the array by + // `n * size_of::()` bytes. + // + // Slices have the same layout as the section of the array they + // slice. + let (left, right) = unsafe { parts.via_unchecked() }; + + assert_partitions(&original, source_len, split, oracle, left, right); + left.fill(left_value); + right.fill(right_value); + } + assert_same_u32_elements(&values, &expected_values); + } +} + #[cfg(test)] mod tests { #[cfg(feature = "derive")]