diff --git a/zerocopy/src/layout.rs b/zerocopy/src/layout.rs index 0c23bdfba1..cf47f03405 100644 --- a/zerocopy/src/layout.rs +++ b/zerocopy/src/layout.rs @@ -122,7 +122,7 @@ impl DstLayout { /// The current, documented max alignment of a type \[1\]. /// - /// \[1\] Per : + /// \[1\] Per : /// /// The alignment value must be a power of two from 1 up to /// 229. @@ -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 diff --git a/zerocopy/src/lib.rs b/zerocopy/src/lib.rs index 401a66ab1d..046bdd80dd 100644 --- a/zerocopy/src/lib.rs +++ b/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)))] diff --git a/zerocopy/src/proofs/into_bytes.rs b/zerocopy/src/proofs/into_bytes.rs index 3cfe667896..6bb799befe 100644 --- a/zerocopy/src/proofs/into_bytes.rs +++ b/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::` 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::().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); diff --git a/zerocopy/src/ref.rs b/zerocopy/src/ref.rs index 51ac6d12d7..f2381c6ab0 100644 --- a/zerocopy/src/ref.rs +++ b/zerocopy/src/ref.rs @@ -1005,6 +1005,15 @@ mod proofs { const CAPACITY: usize = 8; const SIZE: usize = mem::size_of::(); + // This factored Rust-library oracle asks `usize::checked_sub` for one byte + // below `u32`'s actual size rather than manually reconstructing `SIZE - 1`. + // `SIZE` comes from `size_of::()` [12], `checked_sub` returns `None` + // instead of underflowing [38], and `expect` makes that case fail closed as + // a checked Kani property [28][30]. + fn one_byte_short_of_u32() -> usize { + SIZE.checked_sub(1).expect("u32 must have nonzero size") + } + // 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, @@ -1030,10 +1039,11 @@ mod proofs { /// A safe contiguous view of an eight-byte backing buffer. /// - /// `View::any` covers all 45 pairs satisfying `0 <= start <= end <= 8`, - /// including every empty view. Keeping range selection here makes the - /// quantified range identical across the six harnesses without hiding - /// any zerocopy operation under test. + /// Under the shared Kani input-model premise below, `View::any` quantifies + /// over all 45 pairs satisfying `0 <= start <= end <= 8`, including every + /// empty view. Keeping range selection here makes the quantified range + /// identical across the six harnesses without hiding any zerocopy operation + /// under test. #[derive(Clone, Copy)] struct View { start: usize, @@ -1065,6 +1075,110 @@ mod proofs { source.len() == SIZE && source.as_ptr().cast::().is_aligned() } + // Each operation harness checks two setup modes over the same symbolic + // inputs. The public mode retains end-to-end coverage through + // `Ref::from_bytes`. The direct mode bypasses that constructor and creates + // a `Ref` only after safe Rust observations recheck the current slice's + // size and alignment. The concrete byte-slice stability premise below + // completes `Ref::new_unchecked`'s temporal safety precondition for this + // sized `u32`. + // Relative to that explicit stability premise, a compensating + // `from_bytes`/operation defect cannot satisfy both modes. The direct mode + // still trusts the unsafe byte-slice trait contracts as proof setup; those + // are not conclusions of the operation harnesses. + fn ref_operation_setup<'a>( + source: &'a mut [u8], + use_public_constructor: bool, + ) -> Ref<&'a mut [u8], u32> { + assert_eq!(source.len(), SIZE); + assert!(source.as_ptr().cast::().is_aligned()); + if use_public_constructor { + Ref::<_, u32>::from_bytes(source).expect("constructible view should produce a Ref") + } else { + // SAFETY: Here `B` is exactly `&mut [u8]`. The two assertions above + // establish that its current referent is exactly + // `size_of::()` bytes and aligned for `u32`. `&mut [u8]`'s + // `ByteSlice`, `ByteSliceMut`, `IntoByteSlice`, and + // `IntoByteSliceMut` implementations promise that its shared, + // mutable, and consuming byte-slice views preserve that address and + // length, as detailed in the direct-setup stability premise below. + // Thus every view named by `new_unchecked`'s safety contract + // retains the established size and alignment. + unsafe { Ref::new_unchecked(source) } + } + } + + // The direct error mode likewise bypasses `Ref::from_bytes`: it passes the + // exact source to the error constructors for the independently observed + // rejection reason. The source-level payload lemma below establishes how + // those expressions store it. This isolates `CastError::into_src` from a + // compensating `Ref::from_bytes` defect while retaining the public mode's + // end-to-end error-restoration check. + fn error_operation_setup<'a>( + source: &'a mut [u8], + use_public_constructor: bool, + ) -> CastError<&'a mut [u8], u32> { + assert!(!construction_oracle(source)); + if use_public_constructor { + match Ref::<_, u32>::from_bytes(source) { + Err(err) => err, + Ok(typed) => { + mem::forget(typed); + panic!() + } + } + } else if source.len() != SIZE { + ConvertError::Size(SizeError::<_, u32>::new(source)) + } else { + assert!(!source.as_ptr().cast::().is_aligned()); + assert!(mem::align_of::() > 1); + // SAFETY: The preceding `align_of` assertion is exactly + // `AlignmentError::new_unchecked`'s precondition for `Dst = u32`. + ConvertError::Alignment(unsafe { AlignmentError::<_, u32>::new_unchecked(source) }) + } + } + + fn cover_operation_setup_modes(use_public_constructor: bool) { + kani::cover!( + use_public_constructor, + "the public Ref::from_bytes setup reaches the named operation" + ); + kani::cover!( + !use_public_constructor, + "the direct-constructor setup reaches the named operation" + ); + } + + // Direct-setup payload and stability lemma: At each `new`/`new_unchecked` + // function call, Rust passes the argument through the declared parameter + // and returns the function body's value [47]. With moved-place semantics + // [17], the non-`Copy` source is therefore moved into the `bytes` or `src` + // parameter. + // The exact body of `Ref::new_unchecked` is `Ref(bytes, PhantomData)`; it + // moves `bytes` into `Ref`'s only data-bearing field. `SizeError::new` and + // `AlignmentError::new_unchecked` have `Self { src, ... }` bodies, whose + // field shorthand moves that same `src` into the field of that name. The + // direct error branch then moves that error into the corresponding + // `ConvertError` tuple variant. Rust's struct-expression rules—including + // tuple structs and variants' use of call expressions—[45], call-expression + // semantics [44], and value-producing block tail expressions [46] complete + // these payload facts without observing the later target operation. Thus + // these exact constructors cannot shift, replace, or otherwise reconstruct + // the source consumed by the named operation. Their source bodies and this + // derivation are a versioned proof artifact which must be re-audited if any + // constructor changes. + // + // Separately, the local unsafe `ByteSlice` contract promises that repeated + // `Deref`/`DerefMut` views preserve address and length across calls to its + // byte-slice super-APIs. `IntoByteSlice` and `IntoByteSliceMut` promise + // their consuming views have that same address and length. This proof uses + // the crate's concrete unsafe implementations of those traits for + // `&mut [u8]` as a setup premise. Combined with the safe current-slice size + // and alignment assertions at the unsafe call, that stability premise + // discharges the remainder of `Ref::new_unchecked`'s temporal contract. The + // harnesses do not prove those unsafe trait implementations; they remain in + // the zerocopy TCB alongside the pinned Rust/Kani model. + // This independent value oracle copies from the immutable pre-operation // snapshot using safe slice-to-array conversion, then asks `u32` to decode // its own native-endian memory representation. `None` exposes rather than @@ -1115,48 +1229,60 @@ mod proofs { original } - // Domain: The constructor harness covers every one of the 45 contiguous - // ranges of an eight-byte, deliberately `u32`-aligned buffer and every - // buffer value on Kani's target. The error-restoration harness covers the - // same values and ranges and every replacement `u8`, then assumes the - // explicit construction policy rejects its range. `View` records only the - // two range endpoints; every length used by a policy, cover, or result - // observation comes directly from `slice::len` on the safely indexed - // source rather than reconstructed as `end - start`. The immutable - // `Deref` harness and three mutation harnesses generate the same ranges, - // then assume the explicit construction policy oracle as setup; their - // effective range is therefore every generated range whose length is - // `size_of::()` and whose start pointer Rust's - // `is_aligned::()` observation accepts. Covers witness constructible - // views at offsets zero and `SIZE`; they do not claim that those witnesses + // Domain: The constructor harness universally quantifies over each of the + // 45 contiguous ranges of an eight-byte, deliberately `u32`-aligned buffer + // and every buffer value on Kani's target. The error-restoration harness + // universally quantifies over the same values and ranges and every + // replacement `u8`, then assumes the explicit construction policy rejects + // its range. `View` records only the two range endpoints; every length used + // by a policy, cover, or result observation comes directly from + // `slice::len` on the safely indexed source rather than reconstructed as + // `end - start`. The immutable `Deref` harness and three mutation harnesses + // generate the same ranges, then assume the explicit construction policy + // oracle as setup; their effective range is therefore every generated + // range whose length is `size_of::()` and whose start pointer Rust's + // `is_aligned::()` observation accepts. Each of those five operation + // harnesses additionally quantifies over both values of a fresh Boolean + // setup choice: one branch reaches the named operation through public + // `Ref::from_bytes`, while the other bypasses it through the direct + // invariant-bearing setup above. Covers witness constructible views at + // offsets zero and `SIZE`; they do not claim that those witnesses // exhaustively classify aligned offsets on every target. Each mutation - // harness independently covers every buffer value and replacement `u32`; - // splitting them removes an irrelevant Cartesian product without + // harness independently quantifies over every buffer value and replacement + // `u32`; splitting them removes an irrelevant Cartesian product without // restricting any individual mutation API's value domain. // - // Kani 0.67 documents that `kani::any::()` creates a symbolic valid - // `T`, with `Arbitrary` representing all possible valid values of that - // type [35]. The two `usize` calls in `View::any` therefore initially cover - // every pair of target `usize` values. Primitive ordering supplies the two - // Boolean range predicates [25], and Kani documents that `kani::assume` - // makes a true predicate valid on subsequent paths while successfully - // exiting paths where it is false [36]. Those two assumptions consequently - // retain exactly the 45 pairs satisfying `start <= end <= CAPACITY`; they - // define this domain rather than prove the inequalities. The same `any` - // contract quantifies each harness's `[u8; CAPACITY]` buffer and its `u8` - // or `u32` replacement over every valid value of that concrete type. + // Kani 0.67 documents that `kani::any::()` creates an arbitrary valid + // `T`, and that `Arbitrary` implementations are expected to represent all + // possible values of their type [35]. Under the Kani input + // translation/model TOOL/TCB premise recorded in + // `agent_docs/validation.md`, the two primitive `usize` calls in + // `View::any` jointly quantify over every pair of target `usize` values. + // Primitive ordering supplies the two Boolean range predicates [25], and + // Kani documents that `kani::assume` makes a true predicate valid on + // subsequent paths while successfully exiting paths where it is false + // [36]. Those two assumptions consequently retain exactly the 45 pairs + // satisfying `start <= end <= CAPACITY`; they define this domain rather + // than prove the inequalities. Under the same TOOL/TCB + // premise, each harness's `[u8; CAPACITY]` buffer, its `u8` or `u32` + // replacement, and each operation harness's setup Boolean universally + // range over every valid value of those concrete types. // Each successful-operation harness later passes the independently // evaluated `construction_oracle(source)` Boolean to the same Kani // assumption primitive [36]. Those calls retain exactly the generated // views which the explicit size-and-alignment policy accepts, defining the - // effective operation domain described above without assuming that the - // target constructor itself succeeds. - // The error-restoration harness instead assumes the negation of that - // independently evaluated Boolean, retaining exactly the generated views - // rejected by the policy. Each harness uses one fixed, stack-backed - // `AlignedBytes` object and separate fixed-size value snapshots. It - // performs no dynamic allocation and contains no explicit proof loop. The - // unwind bound of nine applies to + // effective operation domain described above. The setup helper then + // rechecks the exact size and alignment with safe Rust observations before + // either requiring the public constructor to succeed or calling the unsafe + // invariant-bearing constructor directly. The error-restoration harness + // instead assumes the negation of that independently evaluated Boolean, + // retaining exactly the generated views rejected by the policy. Its public + // branch requires `Ref::from_bytes` to return an error; its direct branch + // constructs the independently classified size or alignment error around + // the same source. Each harness uses one fixed, stack-backed `AlignedBytes` + // object and separate fixed-size value snapshots. It performs no dynamic + // allocation and contains no explicit proof loop. The unwind bound of nine + // applies to // every loop reached in zerocopy or the standard-library oracles, with // unwinding assertions enabled. // @@ -1165,29 +1291,54 @@ mod proofs { // that property and triggers the condition [37]. The fail-closed Kani // runner described in `agent_docs/validation.md` requires every emitted // cover property to be satisfied. The constructor and error-restoration - // harnesses each cover rejected examples with a three-byte aligned view, a - // four-byte misaligned view, a three-byte misaligned view, and an empty end - // view; the constructor also covers accepted views at offsets zero and - // `SIZE`. Each rejected-view cover group contains both `SIZE - 1` - // expressions, which equal three without overflow as derived below. The - // error-restoration `u8` inequality cover witnesses a non-idempotent - // recovered-source write. The `Deref`, `DerefMut`, `write`, and `into_mut` - // covers each witness accepted views at offsets zero and + // harnesses each cover rejected examples with an aligned view one byte + // shorter than `SIZE`, an exact-sized misaligned view, a one-byte-short + // misaligned view, and an empty end view; the constructor also covers + // accepted views at offsets zero and `SIZE`. Each rejected-view cover group + // obtains both one-byte-short boundaries from the checked Rust-library + // oracle above. The error-restoration `u8` inequality cover witnesses a + // non-idempotent recovered-source write. The `Deref`, `DerefMut`, `write`, + // and `into_mut` covers each witness accepted views at offsets zero and // `SIZE`; the `DerefMut` and `into_mut` `u32` inequality covers witness // non-idempotent typed writes, while `write`'s iterator-inequality cover // witnesses a replacement whose native bytes differ from the selected - // pre-call bytes. These covers establish only existence in the modeled - // domain, not the correctness or exhaustiveness of a partition. + // pre-call bytes. Every operation harness also covers both setup choices + // after the named operation returns, so neither the public integration path + // nor the direct-isolation path can disappear vacuously. These covers + // establish only existence in the modeled domain, not the correctness or + // exhaustiveness of a partition. // - // Together, the six harnesses establish: the safe sized + // Relative to the direct-setup payload/stability lemma and the common + // tool-model premises, the six harnesses establish: the safe sized // `Ref<&mut [u8], u32>` constructor succeeds exactly for a - // size-and-alignment-valid range; immutable and mutable dereference - // preserve exact address and contents; each mutation API writes through - // to exactly the selected bytes; and a construction error returns a slice - // whose modeled raw address, element count, and ordered bytes match the - // input. A modeled first-byte write through that returned slice produces - // the expected whole-buffer final frame. These observations do not prove - // the returned slice's provenance, reference identity, or lifetime. + // size-and-alignment-valid range; both the public-constructor integration + // path and the direct-invariant setup path give immutable and mutable + // dereference the expected address and contents; each mutation API has the + // expected final write-through frame on both paths; and both a public + // construction error and a directly constructed error return a slice whose + // modeled raw address, element count, and ordered bytes match the input. A + // modeled first-byte write through that returned slice produces the + // expected whole-buffer final frame. These observations do not prove the + // returned slice's provenance, reference identity, or lifetime. + // + // Setup isolation and timing: Every complete backing-frame assertion is a + // final-state observation at its stated normal-return control point. It + // does not exclude a transient write that is restored before that + // observation. The constructor-classification harness independently proves + // that `Ref::from_bytes`, followed by forgetting either result payload, + // leaves the final backing bytes unchanged for every generated constructor + // case; it does not establish either payload's internal source state. The + // other five harnesses therefore do not attempt to derive a named + // operation's result by composing that weak constructor frame. Instead, + // each checks the same named operation under both public-constructor setup + // and direct setup. The direct observations do not execute or depend on + // `Ref::from_bytes`; relative to the direct-setup payload and byte-slice + // stability lemma above, a defect in that constructor cannot mask a named + // operation defect on the direct state. The exact constructor expressions + // plus Rust's move/construction semantics establish the payload portion of + // that lemma; the concrete unsafe byte-slice stability implementations + // remain its explicit zerocopy TCB premise. Neither setup mode rules out + // restored transient writes or proves destructor behavior excluded below. // // API-policy oracles: `Ref::from_bytes` documents the rejection direction: // invalid source size or alignment returns `Err`. The constructor harness @@ -1197,11 +1348,10 @@ mod proofs { // For this sized `u32`, the checks are `len == size_of::()` and the // compiler's pointer `is_aligned` observation. Slice `len` supplies the // number of source `u8` byte elements [11], while `size_of::()` - // independently supplies `u32`'s size in bytes [12]. The primitive-layout - // table fixes that size at four bytes [38]. Consequently `SIZE: usize` is - // four, and each `SIZE - 1` cover computes integer subtraction `4 - 1 = 3`; - // three is representable by `usize`, so the subtraction cannot produce a - // value below the type's minimum and does not overflow [38]. Primitive + // independently supplies `u32`'s size in bytes [12]. Every one-byte-short + // cover obtains its boundary through the factored `checked_sub` oracle; + // Rust returns `None` instead of underflowing [38], and `expect` plus + // Kani's panic checking makes that case fail closed [28][30]. Primitive // `usize` equality supplies only the `==`/`!=` classification mechanics // [24]; it does not make this zerocopy policy independent. Rust's lazy // Boolean `&&` evaluates its right operand only when its left operand is @@ -1219,7 +1369,7 @@ mod proofs { // safe length and alignment observations identify the failed condition but // do not independently choose its error variant. Constructing a `Ref` from // the source is expected to preserve its referent address. The constructor - // is also expected not to mutate the source: its + // is also expected to return with the source bytes unchanged: its // `#[must_use = "has no side effects"]` annotation motivates that policy, // but the harness conservatively treats source non-mutation as an adopted // zerocopy regression property rather than inferring it from a diagnostic @@ -1229,12 +1379,13 @@ mod proofs { // These are zerocopy API policies, not independent Rust-language evidence; // the constructor harness checks the implementation and error // discriminants against them. The immutable-`Deref` and mutation harnesses - // assume only this independent policy oracle before using the constructor - // as setup; they never assume that the constructor's result is successful. - // Their `expect` calls therefore recheck valid-input acceptance, while only - // the constructor harness classifies rejected views. The - // error-restoration harness separately assumes policy rejection and - // rechecks that setup before calling `into_src`. + // assume only this policy oracle to define their range. Their public setup + // branches recheck valid-input acceptance, while their direct branches + // separately assert the unsafe constructor's exact size/alignment + // preconditions and never call `Ref::from_bytes`. The error-restoration + // harness similarly assumes policy rejection: its public branch rechecks + // that `Ref::from_bytes` fails, while its direct branch constructs the + // independently classified error variant without calling it. // // Referent and mutation-placement policies: `Ref`'s type documentation // defines it as a reference to a `T` stored in `B`, with `B`'s mutability. @@ -1257,10 +1408,11 @@ mod proofs { // mutable reference to `T`; the adopted placement policy is that the // reference addresses the same selected backing bytes and writes through // to them. - // These policies connect each target operation to the independently built - // whole-buffer effect oracle. The byte-conversion and safe-slice contracts - // below determine the expected bytes, but do not themselves establish where - // any zerocopy API places a write. + // These policies connect each target operation, under either explicitly + // selected setup mode, to the independently built whole-buffer effect + // oracle. The byte-conversion and safe-slice contracts below determine the + // expected bytes, but do not themselves establish where any zerocopy API + // places a write. // // Value and effect oracles: safe slice-to-array conversion copies into // `[u8; N]` when the slice length is `N` [1]. `u32::{from,to}_ne_bytes` @@ -1316,6 +1468,10 @@ mod proofs { // [35], and [36] exactly as mapped above. `value_oracle`'s explicit // `Result` match consumes the safe conversion contract [1] and Rust's // match/variant semantics [23]; its error arm returns `None` directly. + // The checked one-byte-short oracle consumes [12]'s actual size, [38]'s + // checked subtraction, and [30]'s success-or-panic extraction; [28] makes a + // hypothetical underflow fail verification rather than silently narrowing + // a cover. // The constructor harness's match on `(result, expected_success)` consumes // [23] to classify the actual `Result`; either mismatched // variant/value arm triggers a deliberately false shared Boolean @@ -1325,9 +1481,18 @@ mod proofs { // error-kind assertions additionally consume [23]'s explicit variant // matches and the zerocopy variant policy // in [22]; neither safe observation selects a `ConvertError` discriminant. - // The error-restoration harness's separate `Result` match consumes [23]; - // its unexpected `Ok` arm forgets the wrapper, fails a verification - // assertion, and returns, while its `Err` arm alone reaches `into_src`. + // The error-restoration setup's public-branch `Result` match consumes [23]; + // its unexpected `Ok` arm forgets the wrapper and panics, while its `Err` + // arm alone reaches `into_src`. The direct successful setup rechecks + // `slice::len`, `size_of`, and pointer alignment before calling the local + // unsafe `Ref::new_unchecked`; its safety comment combines the observations + // and concrete byte-slice stability premise to discharge the constructor's + // complete sized-`u32` precondition. The direct error + // setup selects `SizeError::new` from length inequality. Its alignment arm + // rechecks source misalignment, and `align_of::() > 1` [43] discharges + // `AlignmentError::new_unchecked`'s exact safety precondition. The direct + // setup payload lemma maps the exact constructor expressions through + // [17] and [44]-[46], rather than merely assuming their payload result. // Every proof assertion here omits custom formatting arguments. Kani 0.67's // verification standard library maps those `assert!` and `assert_eq!` // forms, including the shared Boolean assertion, to `kani::assert` [27]. A @@ -1344,12 +1509,14 @@ mod proofs { // consume the symbolic replacement, dereference semantics [8], assignment // semantics [9], [21], and the applicable method-placement policy above. // The `Ref::write` harness deliberately - // performs no `Deref` observation: after constructor setup, its only + // performs no `Deref` observation: after the selected setup, its only // post-target assertion is the complete backing frame. Its distinct-value - // cover compares copied iteration over the selected original bytes with - // consuming array iteration over the replacement bytes [18][19]. The array - // `IntoIterator` implementation moves each array value in start-to-end - // order [33]. Every post-mutation + // cover occurs after `write` returns and the wrapper is forgotten, and + // compares copied iteration over the selected original bytes with consuming + // array iteration over the replacement bytes [18][19]. It witnesses + // reachability of that post-target control point, not the write result. The + // array `IntoIterator` implementation moves each array value in + // start-to-end order [33]. Every post-mutation // whole-buffer frame assertion consumes [3], [4], [6], [11], [12], // [17]-[20], [24], [32], [34], [40], and [41], plus the applicable // placement policy; @@ -1363,24 +1530,20 @@ mod proofs { // `into_mut` harnesses instead wrap each returned mutable-reference value // in `ManuallyDrop` [42] after its last observation and before the outer // frame observation. That deliberate automatic-drop isolation proves no - // general reference-destruction behavior. Those outer frames therefore - // observe only the named target operation rather than a - // target-plus-destruction composition. The constructor-classification - // harness's own whole-buffer - // frame independently checks the adopted constructor non-mutation policy - // for every generated buffer and view, across both accepted and rejected - // cases. The proof-family argument for each of the five consumer or error - // harnesses composes that separately established producer theorem with its - // target-specific frame. Thus a constructor mutation cannot be hidden by a - // compensating consumer or error-path mutation. This is a modular - // composition of verified harness results, not one harness mechanically - // importing another as a lemma. The immutable-`Deref` frame additionally - // consumes its placement/value and whole-backing non-mutation policies - // above. The separate error-restoration frame consumes [6]-[9], [11], - // [17]-[20], [23]-[24], [34], and [40]: an - // empty selected range is unchanged, while a nonempty range has only its - // first byte replaced. The modeled-address assertions consume [5]'s sized - // pointer casts and the + // general reference-destruction behavior. Each operation frame directly + // observes + // the selected setup plus the named target. The public branch is an + // end-to-end constructor-rooted sequence; the direct branch supplies the + // target-specific result conditional on the explicitly bounded setup + // premise above, rather than composing with the constructor harness. The + // constructor frame consumes the adopted constructor non-mutation policy; + // the immutable-`Deref` frame additionally consumes its placement/value + // and whole-backing non-mutation policies above. The separate + // error-restoration frame + // consumes [6]-[9], [11], [17]-[20], [23]-[24], [34], and [40]: an empty + // selected range is unchanged, while a nonempty range has only its first + // byte replaced. The modeled-address assertions consume [5]'s sized pointer + // casts and the // reference-to-pointer coercion and address-equality contracts in [10]. The // backing-object alignment premise consumes [13]-[14]. // @@ -1435,6 +1598,18 @@ mod proofs { // the maximum field alignment rounded up to a valid final size. // - [15] `DerefMut::deref_mut` returns `&mut Self::Target`; `Ref`'s `Deref` // implementation defines `Target = T`. + // - [43] `align_of::()` returns `T`'s ABI-required minimum alignment in + // bytes; the direct alignment-error setup checks that value rather than + // manually reconstructing `u32`'s numeric alignment. + // - [47] At a function call, arguments pass through parameters. Evaluating + // the body conceptually binds parameter patterns to argument expressions + // and returns the body's value. With [17]'s move semantics, + // the non-`Copy` source is moved into each constructor's `bytes` or `src` + // parameter. [45]'s struct field shorthand installs that `src` operand in + // the named field and specifies that tuple structs and variants are + // instantiated with call expressions; [44] defines those calls. [46] + // makes each constructor body's final expression its block value. Thus + // the exact source—not a reconstruction—reaches the corresponding field. // - [20]-[21] `u8` and `u32` document that `PartialEq::eq` tests whether // its operands are equal and is used by `==`, while `PartialEq::ne` // tests whether they are not equal and is used by `!=`. @@ -1450,9 +1625,8 @@ mod proofs { // its pattern to match. // - [37] Each `kani::cover!` creates a cover property, and `SATISFIED` // means Kani found an execution which triggers its condition. - // - [38] The primitive-layout table fixes `u32`'s size at four bytes, `-` - // is integer subtraction, and subtraction overflows only when its result - // is outside the integer type's range. + // - [38] `usize::checked_sub` returns `None` when integer underflow occurs + // and otherwise returns the subtraction result. // - [39] `&&` is logical AND and evaluates its right operand only when its // left operand is true; `!` on a Boolean is logical negation. // - [40] Evaluating `return` moves its argument to the function's output @@ -1527,13 +1701,13 @@ mod proofs { // https://doc.rust-lang.org/1.93.0/reference/expressions/if-expr.html#if-let-patterns // https://doc.rust-lang.org/1.93.0/reference/expressions/if-expr.html#r-expr.if.condition-true // https://doc.rust-lang.org/1.93.0/reference/expressions/if-expr.html#r-expr.if.else-if - // [35]: https://model-checking.github.io/kani/crates/doc/kani/fn.any.html - // [36]: https://model-checking.github.io/kani/crates/doc/kani/fn.assume.html + // [35]: 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-L70 + // https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/arbitrary.rs#L125-L131 + // [36]: https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/lib.rs#L139-L167 // [37]: https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani/src/lib.rs#L66-L77 // https://github.com/model-checking/kani/blob/kani-0.67.0/docs/src/verification-results.md#cover-property-results - // [38]: https://doc.rust-lang.org/1.93.0/reference/type-layout.html#primitive-data-layout - // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#overflow - // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#arithmetic-and-logical-binary-operators + // [38]: https://doc.rust-lang.org/1.93.0/std/primitive.usize.html#method.checked_sub // [39]: https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#lazy-boolean-operators // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#negation-operators // [40]: https://doc.rust-lang.org/1.93.0/reference/expressions/return-expr.html @@ -1542,6 +1716,11 @@ mod proofs { // https://doc.rust-lang.org/1.93.0/reference/type-coercions.html#r-coerce.unsize.slice // [42]: https://doc.rust-lang.org/1.93.0/core/mem/struct.ManuallyDrop.html // https://doc.rust-lang.org/1.93.0/reference/destructors.html#r-destructors.manually-suppressing + // [43]: https://doc.rust-lang.org/1.93.0/core/mem/fn.align_of.html + // [44]: https://doc.rust-lang.org/1.93.0/reference/expressions/call-expr.html + // [45]: https://doc.rust-lang.org/1.93.0/reference/expressions/struct-expr.html + // [46]: https://doc.rust-lang.org/1.93.0/reference/expressions/block-expr.html + // [47]: https://doc.rust-lang.org/1.93.0/reference/items/functions.html#function-body // // These are not generic `Ref` theorems. `Ref::from_bytes` performs no // representation-validity check for any `T`; `u32: FromBytes` only enables @@ -1565,7 +1744,10 @@ mod proofs { // harness deliberately does not dereference a successful `Ref` or recover // an error's source. It forgets either result payload before observing the // whole-buffer frame, so that frame excludes destruction of the wrapper, - // error, and their `B` fields. It proves no generic drop behavior. + // error, and their `B` fields. This is only a constructor final-state + // property: it neither exposes a result payload's internal source nor + // composes into an operation-specific theorem. It does not rule out a + // restored transient write and proves no generic drop behavior. #[kani::proof] #[kani::unwind(9)] fn prove_sized_u32_from_bytes_classification() { @@ -1588,9 +1770,10 @@ mod proofs { mem::forget(typed); } (Err(err), false) => { - kani::cover!(view.start == 0 && source_len == SIZE - 1); + let one_byte_short = one_byte_short_of_u32(); + kani::cover!(view.start == 0 && source_len == one_byte_short); kani::cover!(view.start == 1 && source_len == SIZE); - kani::cover!(view.start == 1 && source_len == SIZE - 1); + kani::cover!(view.start == 1 && source_len == one_byte_short); kani::cover!(view.start == CAPACITY && source_len == 0); if source_len != SIZE && source_aligned { match &err { @@ -1619,19 +1802,22 @@ mod proofs { assert_same_u8_elements(&backing.bytes, &original); } - // Scope: successful construction is setup; immutable `Deref::deref` is - // the operation under proof. For every constructible view and buffer - // value, it must preserve the selected referent's address and initial value - // and leave the entire backing-byte frame unchanged. The harness then - // forgets the temporary `Ref` before checking the whole-buffer frame, - // excluding wrapper and `B` destruction and proving no generic drop - // behavior. It does not establish provenance, reference identity, or - // lifetime safety. + // Scope: For every constructible view and buffer value, immutable + // `Deref::deref` must preserve the selected referent's address and initial + // value and leave the entire backing-byte frame unchanged under both setup + // modes. The public mode proves the complete `Ref::from_bytes`-then-`Deref` + // integration sequence. The direct mode bypasses `from_bytes` and + // attributes the result to `Deref`, conditional on the explicit + // direct-setup premise above. The harness forgets the temporary `Ref` + // before its final-state frame, excluding wrapper and `B` destruction and + // proving no generic drop behavior. It does not establish provenance, + // reference identity, or lifetime safety. #[kani::proof] #[kani::unwind(9)] fn prove_sized_u32_deref() { let original: [u8; CAPACITY] = kani::any(); let view = View::any(); + let use_public_constructor: bool = kani::any(); let mut backing = AlignedBytes { bytes: copy_snapshot(&original), _align: [] }; assert!(backing.bytes.as_mut_ptr().cast::().is_aligned()); @@ -1642,8 +1828,7 @@ mod proofs { kani::assume(construction_oracle(source)); let expected_value = value_oracle(&original, view) .expect("construction oracle requires an exact-size value oracle"); - let typed = - Ref::<_, u32>::from_bytes(source).expect("constructible view should produce a Ref"); + let typed = ref_operation_setup(source, use_public_constructor); kani::cover!(view.start == 0 && source_len == SIZE); kani::cover!(view.start == SIZE && source_len == SIZE); @@ -1652,20 +1837,24 @@ mod proofs { let typed_ptr: *const u32 = typed_ref; assert_eq!(typed_ptr.cast::(), source_ptr as *const u8); assert_eq!(*typed_ref, expected_value); + cover_operation_setup_modes(use_public_constructor); mem::forget(typed); } assert_same_u8_elements(&backing.bytes, &original); } - // Scope: failed construction is setup; `CastError::into_src` is the - // operation under proof. For every rejected view and replacement byte, the - // returned slice must preserve the input's modeled address, length, and - // ordered bytes. A modeled first-byte write through that slice must have - // the independent repair oracle's whole-buffer frame. The returned mutable - // reference is explicitly wrapped in `ManuallyDrop` after the modeled - // write and before the outer frame assertion; this does not prove - // source-reference identity, provenance, lifetime safety, or general + // Scope: For every policy-rejected view and replacement byte, + // `CastError::into_src` must return a slice preserving the input's modeled + // address, length, and ordered bytes under both setup modes. The public + // mode proves the failed-`Ref::from_bytes`-then-`into_src` integration + // sequence. Direct mode wraps the source in the classified error and + // isolates `into_src`, conditional on the source-level direct-setup payload + // lemma above. A modeled first-byte write through the returned slice must + // then have the independent repair oracle's final whole-buffer frame. The + // returned mutable reference is explicitly wrapped in `ManuallyDrop` after + // the modeled write and before the outer frame assertion; this does not + // prove source-reference identity, provenance, lifetime safety, or general // reference-destruction behavior. #[kani::proof] #[kani::unwind(9)] @@ -1673,6 +1862,7 @@ mod proofs { let original: [u8; CAPACITY] = kani::any(); let error_replacement: u8 = kani::any(); let view = View::any(); + let use_public_constructor: bool = kani::any(); let mut backing = AlignedBytes { bytes: copy_snapshot(&original), _align: [] }; assert!(backing.bytes.as_mut_ptr().cast::().is_aligned()); @@ -1681,18 +1871,12 @@ mod proofs { let source_ptr = source.as_mut_ptr(); let source_len = source.len(); kani::assume(!construction_oracle(source)); - let err = match Ref::<_, u32>::from_bytes(source) { - Err(err) => err, - Ok(typed) => { - mem::forget(typed); - assert_same_bool(false, true); - return; - } - }; + let err = error_operation_setup(source, use_public_constructor); - kani::cover!(view.start == 0 && source_len == SIZE - 1); + let one_byte_short = one_byte_short_of_u32(); + kani::cover!(view.start == 0 && source_len == one_byte_short); kani::cover!(view.start == 1 && source_len == SIZE); - kani::cover!(view.start == 1 && source_len == SIZE - 1); + kani::cover!(view.start == 1 && source_len == one_byte_short); kani::cover!(view.start == CAPACITY && source_len == 0); if let Some(first) = view.get(&original).first() { kani::cover!(error_replacement != *first); @@ -1704,6 +1888,7 @@ mod proofs { if let Some(first) = recovered.first_mut() { *first = error_replacement; } + cover_operation_setup_modes(use_public_constructor); let _recovered_without_automatic_drop = mem::ManuallyDrop::new(recovered); } @@ -1711,21 +1896,24 @@ mod proofs { assert_same_u8_elements(&backing.bytes, &expected); } - // Scope: successful construction is setup; `DerefMut::deref_mut` is the - // operation under proof. For every constructible view and every original - // and replacement value, it must preserve address and initial value, and a - // write through the returned reference must have the exact whole-buffer - // frame supplied by the independent oracle. After its last use, the - // returned mutable reference is wrapped in `ManuallyDrop`, and the harness - // then forgets the temporary `Ref`; the outer frame therefore excludes - // automatic destruction of that reference, the wrapper, and its `B` field - // and proves no generic drop behavior. + // Scope: For every constructible view and every original and replacement + // value, `DerefMut::deref_mut` must preserve address and initial value, and + // a write through the returned reference must have the independent oracle's + // exact whole-buffer frame under both setup modes. The public mode proves + // the constructor-rooted integration sequence; the direct mode bypasses + // `from_bytes` and isolates `DerefMut`, conditional on the direct-setup + // premise above. After its last use, the returned mutable reference is + // wrapped in `ManuallyDrop`, and the harness then forgets the temporary + // `Ref`; the outer final-state frame therefore excludes automatic + // destruction of that reference, the wrapper, and its `B` field and proves + // no generic drop behavior. #[kani::proof] #[kani::unwind(9)] fn prove_sized_u32_deref_mut() { let original: [u8; CAPACITY] = kani::any(); let replacement: u32 = kani::any(); let view = View::any(); + let use_public_constructor: bool = kani::any(); let mut backing = AlignedBytes { bytes: copy_snapshot(&original), _align: [] }; assert!(backing.bytes.as_mut_ptr().cast::().is_aligned()); @@ -1736,8 +1924,7 @@ mod proofs { kani::assume(construction_oracle(source)); let original_value = value_oracle(&original, view) .expect("construction oracle requires an exact-size value oracle"); - let mut typed = - Ref::<_, u32>::from_bytes(source).expect("constructible view should produce a Ref"); + let mut typed = ref_operation_setup(source, use_public_constructor); kani::cover!(view.start == 0 && source_len == SIZE); kani::cover!(view.start == SIZE && source_len == SIZE); @@ -1750,6 +1937,7 @@ mod proofs { *typed_mut = replacement; let _typed_mut_without_automatic_drop = mem::ManuallyDrop::new(typed_mut); } + cover_operation_setup_modes(use_public_constructor); mem::forget(typed); } @@ -1758,24 +1946,28 @@ mod proofs { assert_same_u8_elements(&backing.bytes, &expected); } - // Scope: successful construction is setup; `Ref::write` is the operation - // under proof. For every constructible view and every original and - // replacement value, the independent oracle supplies the exact - // whole-buffer native-byte frame. The harness performs no typed `Deref` - // observation, so a separate `Deref` regression cannot be misattributed to - // `write`. It is fixed to `u32` and does not establish `Ref::write`'s - // separate promise to forget its argument; `u32` destruction is - // unobservable here. After the target call, the harness uses safe - // `mem::forget` to consume the wrapper without running its drop glue; this - // isolates the outer frame from wrapper destruction and proves no generic - // `Ref` drop behavior. A snapshot-only cover witnesses a replacement whose - // native bytes differ from the selected pre-call bytes. + // Scope: For every constructible view and every original and replacement + // value, the independent oracle supplies `Ref::write`'s exact whole-buffer + // native-byte frame under both setup modes. The public mode proves the + // constructor-rooted integration sequence; the direct mode bypasses + // `from_bytes` and isolates `write`, conditional on the direct-setup + // premise above. The harness performs no typed `Deref` observation, so a + // separate `Deref` regression cannot be misattributed to `write`. This is + // fixed to `u32`; it does not establish `Ref::write`'s separate promise to + // forget its argument. `u32` destruction is unobservable here. After the + // target call, the harness uses safe `mem::forget` to consume the wrapper + // without running its drop glue; this excludes wrapper destruction and + // proves no generic `Ref` drop behavior. A snapshot-only cover after setup + // and `write` witnesses post-target reachability for a changing input; it + // is not a write-result oracle. #[kani::proof] #[kani::unwind(9)] fn prove_sized_u32_write() { let original: [u8; CAPACITY] = kani::any(); let replacement: u32 = kani::any(); let view = View::any(); + let use_public_constructor: bool = kani::any(); + let replacement_bytes = replacement.to_ne_bytes(); let mut backing = AlignedBytes { bytes: copy_snapshot(&original), _align: [] }; assert!(backing.bytes.as_mut_ptr().cast::().is_aligned()); @@ -1783,16 +1975,18 @@ mod proofs { let source = view.get_mut(&mut backing.bytes); let source_len = source.len(); kani::assume(construction_oracle(source)); - let replacement_bytes = replacement.to_ne_bytes(); - kani::cover!(!view.get(&original).iter().copied().eq(replacement_bytes)); - let mut typed = - Ref::<_, u32>::from_bytes(source).expect("constructible view should produce a Ref"); + let mut typed = ref_operation_setup(source, use_public_constructor); kani::cover!(view.start == 0 && source_len == SIZE); kani::cover!(view.start == SIZE && source_len == SIZE); Ref::write(&mut typed, replacement); mem::forget(typed); + cover_operation_setup_modes(use_public_constructor); + kani::cover!( + !view.get(&original).iter().copied().eq(replacement_bytes), + "a changing input reaches the post-Ref::write control point" + ); } let expected = write_frame_oracle(&original, view, replacement) @@ -1800,20 +1994,22 @@ mod proofs { assert_same_u8_elements(&backing.bytes, &expected); } - // Scope: successful construction is setup; `Ref::into_mut` is the - // operation under proof. For every constructible view and every original - // and replacement value, its returned reference must preserve address and + // Scope: For every constructible view and every original and replacement + // value, `Ref::into_mut`'s returned reference must preserve address and // initial value, and a write through it must have the independent oracle's - // exact whole-buffer frame. After the final typed observation, the returned - // mutable reference is explicitly wrapped in `ManuallyDrop` before the - // outer frame; the harness therefore proves no general - // reference-destruction behavior. + // exact whole-buffer frame under both setup modes. The public mode proves + // the constructor-rooted integration sequence; the direct mode bypasses + // `from_bytes` and isolates `into_mut`, conditional on the direct-setup + // premise above. After the final typed observation, the returned mutable + // reference is explicitly wrapped in `ManuallyDrop` before the outer frame; + // the harness therefore proves no general reference-destruction behavior. #[kani::proof] #[kani::unwind(9)] fn prove_sized_u32_into_mut() { let original: [u8; CAPACITY] = kani::any(); let replacement: u32 = kani::any(); let view = View::any(); + let use_public_constructor: bool = kani::any(); let mut backing = AlignedBytes { bytes: copy_snapshot(&original), _align: [] }; assert!(backing.bytes.as_mut_ptr().cast::().is_aligned()); @@ -1824,8 +2020,7 @@ mod proofs { kani::assume(construction_oracle(source)); let original_value = value_oracle(&original, view) .expect("construction oracle requires an exact-size value oracle"); - let typed = - Ref::<_, u32>::from_bytes(source).expect("constructible view should produce a Ref"); + let typed = ref_operation_setup(source, use_public_constructor); let typed = Ref::into_mut(typed); kani::cover!(view.start == 0 && source_len == SIZE); @@ -1836,6 +2031,7 @@ mod proofs { assert_eq!(*typed, original_value); *typed = replacement; assert_eq!(*typed, replacement); + cover_operation_setup_modes(use_public_constructor); let _typed_without_automatic_drop = mem::ManuallyDrop::new(typed); } diff --git a/zerocopy/src/split_at.rs b/zerocopy/src/split_at.rs index dde6015239..82e82d3f06 100644 --- a/zerocopy/src/split_at.rs +++ b/zerocopy/src/split_at.rs @@ -961,44 +961,43 @@ mod proofs { // `-Zfunction-contracts`, and one layout selected by `--randomize-layout` // per invocation. // - // Domain: Each harness considers every initialized `[u32; 8]`, every + // Domain: Each harness quantifies over 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 + // `0..=source.len()`. The mutable consumer additionally quantifies over + // every pair of `u32` values written through its left and right results. + // Kani 0.67 documents `kani::any::()` as constructing an arbitrary valid + // `T`, with `Arbitrary` expected to represent all possible values [21]. Its + // tagged built-in implementations obtain scalar `u32` and `usize` from the + // raw model hook [22]. The generic array implementation delegates + // `[T; N]` generation to `T::any_array`; primitive `u32` overrides that + // method and obtains the complete `[u32; 8]` through the raw-array hook + // [22][23]. The raw hooks lower to destination-typed nondeterministic + // expressions, and pinned CBMC permits separate evaluations to choose + // differently [24]. Completeness, validity, and the premise that each + // evaluation is a fresh, mutually unconstrained choice are explicit + // TOOL/TCB inputs. Thus `any_slice_split_case` initially ranges over + // `[u32; 8]` x `usize` x `usize`. Its two calls to + // `assume_usize_at_most` retain exactly `source_len <= 8` and + // `split <= source_len`: they pass independently evaluated Rust `usize` + // ordering results to Kani's assumption primitive as documented below. + // The mutable consumer's later two `u32` calls independently range over + // the complete `u32` x `u32` product. This argument is limited to those + // exact built-in types; it does not extend to custom or derived + // `Arbitrary` implementations without a separate domain/image argument. + // Separate harnesses exercise shared and mutable slices. 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]. + // limits [25]. // // Proof decomposition: // - The two `split_at_*_unchecked` harnesses call only the descriptor @@ -1230,15 +1229,15 @@ mod proofs { // 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 + // [22] https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/arbitrary.rs#L22-L70 + // [23] https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/arbitrary.rs#L125-L131 + // [24] https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/lib.rs#L333-L367 + // 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 + // [25] 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