diff --git a/zerocopy/src/impls.rs b/zerocopy/src/impls.rs index f2a0a44c06..199e3748e7 100644 --- a/zerocopy/src/impls.rs +++ b/zerocopy/src/impls.rs @@ -1393,7 +1393,7 @@ mod proofs { pointer::{cast::CastUnsized, invariant::Initialized, BecauseImmutable, Ptr}, proof_support::{ all_zero_byte_policy_oracle, assert_same_bool, assert_same_u8_elements, bool_from_byte, - char_from_ne_bytes, nonzero_u16_from_ne_bytes, validate_and_read_sized, + char_from_ne_bytes, copy_snapshot, nonzero_u16_from_ne_bytes, validate_and_read_sized, }, wrappers::ReadOnly, TryFromBytes, @@ -1799,101 +1799,101 @@ mod proofs { value => assert!(value.is_none()) ); - // Domain: Two independently selectable proof families each cover every - // byte sequence of lengths zero through four. This includes the empty DST - // boundary, every single UTF-8 scalar encoding, and every mixture whose - // total encoded length fits the bound. The direct-validator family checks - // both alignment-marker implementations sealed by the current pointer - // model: `Unaligned`, which `transmute_with` produces, and `Aligned`, which - // `bikeshed_recall_aligned` safely recalls because `str: Unaligned`. + // Domain: Two independently selectable proof families each quantify over + // every byte sequence of lengths zero through four under the common + // `kani::any` TOOL/TCB premise in `agent_docs/validation.md`. This includes + // the empty DST boundary, every single UTF-8 scalar encoding, and every + // mixture whose total encoded length fits the bound. The direct-validator + // family checks both alignment-marker implementations sealed by the current + // pointer model: `Unaligned`, which `transmute_with` produces, and + // `Aligned`, which `bikeshed_recall_aligned` safely recalls because `str: + // Unaligned`. // // Storage and bounds: Each harness uses one fixed stack array of zero to // four bytes and performs no dynamic allocation. Only the array elements // are symbolic inputs. The local source object's placement and allocation // identity are fixed by the harness rather than quantified by Kani, so // every conclusion below is restricted to that modeled stack-object - // placement. Every checking helper receives a shared slice borrow of that - // array; none copies it into a second array. The non-materializing + // placement. Each harness uses safe `copy_snapshot` before any target call + // to record a second fixed array with exactly the source's initial byte + // values. The helper's adjacent language-contract account makes this a + // value snapshot, not a storage-identity theorem. The non-materializing // validator helper's safe zerocopy conversion from `&[u8]` to // `&ReadOnly<[u8]>` creates only another shared reference, not wrapper - // storage. That conversion is target-path setup rather than an independent - // oracle: the harness relies on the Rust/Kani model to preserve the - // referent through it, then tests the resulting validator plumbing against - // the independent grammar oracle below. No harness uses `kani::assume`. - // The oracle's sole explicit loop consumes at least one and at most four - // bytes per iteration. Every harness carries `#[kani::unwind(5)]`, which - // permits all iterations for an initial length of at most four and makes - // Kani check that the bound suffices. + // storage. That conversion is target-path setup rather than an oracle. No + // harness uses `kani::assume`. Every harness carries `#[kani::unwind(5)]`; + // successful unwind assertions show that bound is sufficient for the safe + // elementwise observers over at most four bytes, but do not show it is + // minimal. // - // Establishes: At each harness's fixed modeled source placement, its five - // direct proofs establish that the non-materializing - // `is_bit_valid::` and `is_bit_valid::` specializations - // accept exactly when the external-specification oracle does. At the same - // modeled placements, five separate harnesses pass each grammar-accepted - // input to the public borrowed read API, which succeeds and returns the - // same ordered bytes and length. `str::as_bytes` provides the safe - // byte-slice view used by the shared elementwise observer [7]. That - // observer obtains both counts with `slice::len`, compares them through - // the shared equality helpers, and then compares ordered bytes through safe - // iteration [8]. The four syntactically nonempty public harnesses - // unconditionally check that the result retains that fixed input address - // within Kani's pointer model; pointer equality is only an address - // observation, not a provenance or aliasing theorem. No address identity is - // claimed for empty slices. + // Standard-library oracle and exact theorem: Safe + // `core::str::from_utf8` returns `Ok(&str)` exactly when its input contains + // valid UTF-8 and otherwise returns `Err` [1]. `Result::is_ok` observes + // that classification [2]. Each harness evaluates this oracle on its safe + // pre-call value snapshot before consulting zerocopy. It is therefore + // independent of zerocopy's pointer and cast plumbing and avoids a manually + // reconstructed UTF-8 grammar. After the target returns, the shared ordered + // byte observer compares the original source with that snapshot, so a + // normal-return final state which preserves only the UTF-8 validity class + // cannot satisfy the stated preservation result. These final-state + // observations do not rule out a transient write restored before the + // observer runs. However, the `TryFromBytes for str` + // implementation under proof deliberately delegates its validity decision + // to the same standard function. These harnesses consequently do not + // independently prove the correctness of Rust's UTF-8 classifier. The five + // direct proofs establish only that, at each fixed modeled placement, each + // actual `Unaligned` and `Aligned` argument has the original source address + // before validation, the original source bytes remain equal to the pre-call + // snapshot after validation, and the reported classification matches the + // standard-library operation it wraps. Thus redirection to a different + // address cannot satisfy the proof. This does not observe candidate metadata + // or prove that distinct zero-sized storage has a distinct address. // - // External-specification validity oracle: Rust requires every `str` to - // contain valid UTF-8 [1]. Unicode 17 definitions D85, D86, D89, and D92 - // define a valid UTF-8 string through well-formed UTF-8 code-unit sequences - // and the UTF-8 encoding form; Unicode's authoritative Table 3-7 then lists - // every well-formed byte sequence and declares values outside its listed - // ranges ill-formed [2]. The nine source alternatives in - // `utf8_suffix_after_scalar`, in order, correspond one-for-one to Table - // 3-7's nine rows. In each matching slice pattern, `rest @ ..` binds the - // untouched suffix after that one well-formed scalar encoding. + // At the same modeled placements, five separate harnesses pass each + // standard-library-accepted input to the public borrowed read API, which + // succeeds and returns the same ordered bytes and length as the pre-call + // snapshot; the post-call source must independently match it as well. + // `str::as_bytes` provides the safe byte-slice view used by the shared + // elementwise observer [7]. That observer obtains both counts with + // `slice::len`, compares them through the shared equality helpers, and then + // compares ordered bytes through safe iteration [8]. The four syntactically + // nonempty public harnesses unconditionally check that the result retains + // that fixed input address within Kani's pointer model; pointer equality is + // only an address observation, not a provenance or aliasing theorem. No + // returned-borrow address identity is claimed for empty slices; the + // direct-validator family still checks the empty candidate's address because + // address preservation is meaningful even for a zero-length raw referent. // - // The loop invariant is that the original input equals a sequence of - // already consumed well-formed scalar prefixes followed by `bytes`. Every - // `Some(rest)` step shortens that suffix by one through four bytes; - // `None` rejects immediately, and the tail `true` is reached exactly when - // the suffix is empty. This gives the repeated-prefix decomposition needed - // by D85/D86/D89. We admit both the bridge from Rust 1.93's term “valid - // UTF-8” to those Unicode definitions and the manual Table-3-7 transcription - // as EXTERNAL-SPEC/TCB premises, not conclusions proved by Kani. The oracle - // calls neither zerocopy nor the standard library's UTF-8 validator. It is - // code-path independent, though intentionally not algorithmically diverse: - // this smallest manual rule has no decoder arithmetic or indexing surface. - // - // Rust's safe slice, inclusive-range, or-pattern, binding, match, and loop - // semantics give the grammar transcription its executable meaning [9]. // Each harness's array-to-slice coercion is compiler-checked [3]. On a - // nonempty valid input, `slice::as_ptr` supplies the address of the borrowed - // source buffer [4], `str::as_ptr` supplies the address of the returned - // string's first byte [5], and `ptr::addr_eq` compares those addresses while - // discarding pointer metadata [6]. The expected address therefore comes - // from the original modeled storage, not from the validity oracle. These - // harnesses exercise the stated functional observations of zerocopy's - // validator/cast plumbing at those modeled placements. + // nonempty valid input, `slice::as_ptr` supplies the address of the + // borrowed source buffer [4], `str::as_ptr` supplies the address of the + // returned string's first byte [5], and `ptr::addr_eq` compares those + // addresses while discarding pointer metadata [6]. The direct family + // snapshots the first of those addresses before constructing a candidate, + // then observes each actual candidate's stored raw pointer through + // `Ptr::as_inner` and `PtrInner::as_ptr` before passing that candidate to the + // validator. Those exact target-representation accessors are not independent + // provenance or identity oracles; they only expose the address which the + // target path installed. This observation is also defined for the modeled + // empty candidate because it dereferences no pointer. The expected address + // therefore comes from the original modeled storage, not from a validity or + // validator result. // // Excludes: Arbitrary absolute source addresses, allocation identities, and // relative or subobject placement offsets—including heap/static sources and // other valid data-pointer choices for an empty slice—are outside the one // fixed local object modeled by each harness. Also excluded are strings - // longer than four bytes, a machine proof of the admitted Rust-to-Unicode - // bridge or Table-3-7 transcription, and the public borrowed API's - // invalid-input path. - // The latter is not invoked because a bug which materialized invalid `str` - // would be undefined before its `Result` could safely be inspected. Kani - // does not completely check reference aliasing, pointer provenance, invalid - // values, or uninitialized memory, so those obligations—including whether - // an observed equal address carries the required provenance—remain explicit - // tool/TCB premises rather than conclusions of these harnesses. + // longer than four bytes, correctness of `core::str::from_utf8` itself, and + // the public borrowed API's invalid-input path. The latter is not invoked + // because a bug which materialized invalid `str` would be undefined before + // its `Result` could safely be inspected. Kani does not completely check + // reference aliasing, pointer provenance, invalid values, or uninitialized + // memory, so those obligations—including whether an observed equal address + // carries the required provenance—remain explicit tool/TCB premises rather + // than conclusions of these harnesses. // - // [1] https://doc.rust-lang.org/1.93.0/reference/types/textual.html#r-type.text.str-value - // [2] https://www.unicode.org/versions/Unicode17.0.0/core-spec/chapter-3/#G32849 - // https://www.unicode.org/versions/Unicode17.0.0/core-spec/chapter-3/#G32854 - // https://www.unicode.org/versions/Unicode17.0.0/core-spec/chapter-3/#G32860 - // https://www.unicode.org/versions/Unicode17.0.0/core-spec/chapter-3/#G27817 - // https://www.unicode.org/versions/Unicode17.0.0/core-spec/chapter-3/#G27506 + // [1] https://doc.rust-lang.org/1.93.0/core/str/fn.from_utf8.html + // [2] https://doc.rust-lang.org/1.93.0/core/result/enum.Result.html#method.is_ok // [3] https://doc.rust-lang.org/1.93.0/reference/type-coercions.html#unsized-coercions // [4] https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.as_ptr // [5] https://doc.rust-lang.org/1.93.0/std/primitive.str.html#method.as_ptr @@ -1908,68 +1908,52 @@ mod proofs { // https://doc.rust-lang.org/1.93.0/std/iter/trait.Iterator.html#method.eq // https://doc.rust-lang.org/1.93.0/std/primitive.u8.html#impl-PartialEq-for-u8 // https://doc.rust-lang.org/1.93.0/std/primitive.bool.html#impl-PartialEq-for-bool - // [9] https://doc.rust-lang.org/1.93.0/reference/patterns.html#slice-patterns - // https://doc.rust-lang.org/1.93.0/reference/patterns.html#range-patterns - // https://doc.rust-lang.org/1.93.0/reference/patterns.html#or-patterns - // https://doc.rust-lang.org/1.93.0/reference/patterns.html#identifier-patterns - // https://doc.rust-lang.org/1.93.0/std/option/enum.Option.html - // https://doc.rust-lang.org/1.93.0/reference/expressions/match-expr.html - // https://doc.rust-lang.org/1.93.0/reference/expressions/return-expr.html - // https://doc.rust-lang.org/1.93.0/reference/expressions/block-expr.html#r-expr.block.result - // https://doc.rust-lang.org/1.93.0/reference/expressions/loop-expr.html#predicate-loops - // https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.is_empty - - fn utf8_suffix_after_scalar(bytes: &[u8]) -> Option<&[u8]> { - match bytes { - [0x00..=0x7F, rest @ ..] - | [0xC2..=0xDF, 0x80..=0xBF, rest @ ..] - | [0xE0, 0xA0..=0xBF, 0x80..=0xBF, rest @ ..] - | [0xE1..=0xEC, 0x80..=0xBF, 0x80..=0xBF, rest @ ..] - | [0xED, 0x80..=0x9F, 0x80..=0xBF, rest @ ..] - | [0xEE..=0xEF, 0x80..=0xBF, 0x80..=0xBF, rest @ ..] - | [0xF0, 0x90..=0xBF, 0x80..=0xBF, 0x80..=0xBF, rest @ ..] - | [0xF1..=0xF3, 0x80..=0xBF, 0x80..=0xBF, 0x80..=0xBF, rest @ ..] - | [0xF4, 0x80..=0x8F, 0x80..=0xBF, 0x80..=0xBF, rest @ ..] => Some(rest), - _ => None, - } - } - fn utf8_oracle(mut bytes: &[u8]) -> bool { - while !bytes.is_empty() { - bytes = match utf8_suffix_after_scalar(bytes) { - Some(rest) => rest, - None => return false, - }; - } - true + fn standard_utf8_oracle(bytes: &[u8]) -> bool { + core::str::from_utf8(bytes).is_ok() } - fn assert_str_validators_match(bytes: &[u8], expected_valid: bool) { + fn assert_str_validators_match(bytes: &[u8], snapshot: &[u8], expected_valid: bool) { + let source_address = bytes.as_ptr(); let source: &ReadOnly<[u8]> = bytes.into(); let mut candidate = Ptr::from_ref(source) .transmute_with::, Initialized, CastUnsized, BecauseImmutable>(); - let unaligned_valid = ::is_bit_valid(candidate.reborrow_shared()); + let unaligned_candidate = candidate.reborrow_shared(); + assert_same_bool( + core::ptr::addr_eq(unaligned_candidate.as_inner().as_ptr(), source_address), + true, + ); + let unaligned_valid = ::is_bit_valid(unaligned_candidate); + assert_same_bool(unaligned_valid, expected_valid); + assert_same_u8_elements(bytes, snapshot); + let aligned_candidate = candidate.reborrow_shared().bikeshed_recall_aligned(); + assert_same_bool( + core::ptr::addr_eq(aligned_candidate.as_inner().as_ptr(), source_address), + true, + ); let aligned_valid = ::is_bit_valid(aligned_candidate); - assert_same_bool(unaligned_valid, expected_valid); assert_same_bool(aligned_valid, expected_valid); + assert_same_u8_elements(bytes, snapshot); } - fn assert_empty_valid_str_borrow(bytes: &[u8]) { + fn assert_empty_valid_str_borrow(bytes: &[u8], snapshot: &[u8]) { match str::try_ref_from_bytes(bytes) { - Ok(value) => assert_same_u8_elements(value.as_bytes(), bytes), + Ok(value) => assert_same_u8_elements(value.as_bytes(), snapshot), Err(_) => assert_same_bool(false, true), } + assert_same_u8_elements(bytes, snapshot); } - fn assert_nonempty_valid_str_borrow(bytes: &[u8]) { + fn assert_nonempty_valid_str_borrow(bytes: &[u8], snapshot: &[u8]) { match str::try_ref_from_bytes(bytes) { Ok(value) => { - assert_same_u8_elements(value.as_bytes(), bytes); + assert_same_u8_elements(value.as_bytes(), snapshot); assert_same_bool(core::ptr::addr_eq(value.as_ptr(), bytes.as_ptr()), true); } Err(_) => assert_same_bool(false, true), } + assert_same_u8_elements(bytes, snapshot); } macro_rules! str_validator_proof { @@ -1978,12 +1962,13 @@ mod proofs { #[kani::unwind(5)] fn $proof() { let bytes: [u8; $len] = kani::any(); - let expected_valid = utf8_oracle(&bytes); + let snapshot = copy_snapshot(&bytes); + let expected_valid = standard_utf8_oracle(&snapshot); match expected_valid { - true => kani::cover!(true, "independent grammar accepts this byte sequence"), - false => kani::cover!(true, "independent grammar rejects this byte sequence"), + true => kani::cover!(true, "standard library accepts this byte sequence"), + false => kani::cover!(true, "standard library rejects this byte sequence"), } - assert_str_validators_match(&bytes, expected_valid); + assert_str_validators_match(&bytes, &snapshot, expected_valid); } }; } @@ -1992,10 +1977,11 @@ mod proofs { #[kani::unwind(5)] fn prove_empty_str_validators() { let bytes: [u8; 0] = []; - let expected_valid = utf8_oracle(&bytes); + let snapshot = copy_snapshot(&bytes); + let expected_valid = standard_utf8_oracle(&snapshot); assert_same_bool(expected_valid, true); kani::cover!(expected_valid, "empty input is accepted"); - assert_str_validators_match(&bytes, expected_valid); + assert_str_validators_match(&bytes, &snapshot, expected_valid); } str_validator_proof!(prove_one_byte_str_validators, 1); @@ -2007,10 +1993,11 @@ mod proofs { #[kani::unwind(5)] fn prove_empty_str_try_ref_from_bytes() { let bytes: [u8; 0] = []; - let expected_valid = utf8_oracle(&bytes); + let snapshot = copy_snapshot(&bytes); + let expected_valid = standard_utf8_oracle(&snapshot); kani::cover!(expected_valid, "empty input is accepted"); match expected_valid { - true => assert_empty_valid_str_borrow(&bytes), + true => assert_empty_valid_str_borrow(&bytes, &snapshot), false => assert_same_bool(false, true), } } @@ -2021,13 +2008,14 @@ mod proofs { #[kani::unwind(5)] fn $proof() { let bytes: [u8; $len] = kani::any(); - match utf8_oracle(&bytes) { + let snapshot = copy_snapshot(&bytes); + match standard_utf8_oracle(&snapshot) { true => { - kani::cover!(true, "independent grammar accepts this byte sequence"); - assert_nonempty_valid_str_borrow(&bytes); + kani::cover!(true, "standard library accepts this byte sequence"); + assert_nonempty_valid_str_borrow(&bytes, &snapshot); } false => { - kani::cover!(true, "independent grammar rejects this byte sequence"); + kani::cover!(true, "standard library rejects this byte sequence"); } } } diff --git a/zerocopy/src/macros.rs b/zerocopy/src/macros.rs index 22d3c999d6..01cc4ae992 100644 --- a/zerocopy/src/macros.rs +++ b/zerocopy/src/macros.rs @@ -1292,13 +1292,24 @@ mod proofs { // proof. Kani explores all 256 `u8` values, with covers for false, true, // and invalid inputs. The value and reference macros are invoked only for // the two independently valid representations; they check the decoded - // value, the explicit zerocopy same-address policy, and mutation - // propagation. `addr_of!` / `addr_of_mut!` obtain a raw pointer to the - // source place without creating an intermediate reference [5]. Rust's - // reference-to-raw coercions, sized pointer casts, and raw-pointer equality - // independently specify how both modeled addresses are observed [6][7]. - // Requiring them to match is a zerocopy policy oracle, not a Rust-language - // requirement, and establishes no provenance property. + // value and the explicit zerocopy same-address policy. `addr_of!` / + // `addr_of_mut!` obtain a raw pointer to the source place without creating + // an intermediate reference [5]. Rust's reference-to-raw coercions, sized + // pointer casts, and raw-pointer equality independently specify how both + // modeled addresses are observed [6][7]. Requiring them to match is a + // zerocopy policy oracle, not a Rust-language requirement, and establishes + // no provenance property. + // + // Before the mutable macro is called, logical `!` derives a replacement + // solely from the independently decoded `expected` bool [13], and [1] + // converts that replacement to its expected source byte. The target result + // cannot influence either value. On success, dereference observes the bool + // at the returned reference's location [14], assignment copies or moves + // the precomputed replacement into that location [15], and `assert_eq!` + // plus primitive `u8` equality compares the source with the precomputed + // byte after the mutable borrow ends [16]. This chain proves only modeled + // value propagation; the reference obligations remain in the TOOL/TCB + // boundary below. // // Owned-value pointer policy: Two independent harnesses exercise the // owned-value macro. The first covers every `usize` as a direct @@ -1308,7 +1319,16 @@ mod proofs { // safe iteration, and primitive equality. The helper's adjacent docs give // those exact Rust 1.93 contracts; it never reconstructs an integer or // calls zerocopy. This family separately adopts all-zero acceptance as the - // explicit conservative zerocopy pointer policy under test. + // explicit conservative zerocopy pointer policy under test. Before the + // macro consumes `src`, the shared safe-Rust `copy_snapshot` records its + // `Copy` value using the concrete `usize: Copy` implementation [17] and + // the dereference, value-expression, and copied-place rules documented + // next to that helper. On `Err`, the shared + // `assert_same_usize` observes the directly projected error field against + // that snapshot using `assert_eq!` and primitive `usize` equality. Neither + // helper calls zerocopy or consults its result while constructing the + // expectation. This recovery check establishes abstract `usize` equality, + // not byte preservation, independent storage, or provenance. // // The second harness covers every `[u8; 16]` source and transmutes to // `PaddedPointer`. Pinned compiler observations require an eight-byte thin @@ -1316,61 +1336,55 @@ mod proofs { // the remaining eight bytes are therefore genuine destination tail // padding [10][11]. Safe `slice::first_chunk` obtains exactly the first // eight source bytes, with `Option::expect` making a missing chunk fail - // closed [9]. The same shared all-zero classifier supplies the pointer-field - // policy while deliberately ignoring the padding bytes. The derived - // `TryFromBytes` validator is part of the target path, not an oracle. The - // end-to-end harness proves, rather than assumes, that macro acceptance - // matches that field policy and is independent of the padding. Covers - // witness acceptance and rejection with nonzero padding but do not - // constrain the universal input domain. On every rejection, the shared + // closed [9]. The same shared all-zero classifier supplies the + // pointer-field policy while deliberately ignoring the padding bytes. The + // derived `TryFromBytes` validator is part of the target path; it is not + // an oracle. The end-to-end harness proves, rather than assumes, that macro + // acceptance matches that field policy and is independent of the padding. + // Its covers witness acceptance and rejection with nonzero padding without + // constraining the universal input domain. On every rejection, the shared // ordered-byte observer compares all 16 returned source bytes with a safe // pre-call snapshot. It projects the crate-visible error field rather than // calling `ValidityError::into_src`, preventing accessor and macro defects // from compensating. // - // Mutable-bool write-back: The replacement `!expected` is computed from - // the independent checked-bool oracle before the target is invoked. For a - // `bool`, logical negation exchanges `true` and `false` [14]. Built-in - // dereference of `&mut bool` denotes the pointed-to assignable place, and - // assignment copies the independently computed right-hand value into that - // place [14]. After the target reference's last use, safe `u8::from` - // supplies the expected source representation [1], and primitive `u8` - // equality supplies the final observation [15]. None of those operations - // consults zerocopy to construct the expected mutation or result. - // // Destination validity and accepted value: Rust guarantees that every - // integer representation can validly produce a thin raw pointer [3]; - // [10][11] establish that bytes 8 through 15 are destination tail padding, - // and Rust expressly permits uninitialized memory in padding [12]. We use - // that language rule as the TCB premise that those padding bytes impose no - // additional value-validity constraint; Kani does not prove that premise. - // Thus an erroneous acceptance in either pointer harness still cannot - // materialize an invalid destination. On the accepted all-zero field, safe - // `core::ptr::null()` independently supplies the expected pointer by its - // standard-library contract [4]. Neither harness dereferences the result. + // integer representation can validly produce a thin raw pointer [3]. Rust + // also states both that padding need not be initialized and that a struct's + // validity requires its fields to be valid at their respective types [12]. + // `PaddedPointer` has exactly one field; [3] proves that field valid, while + // [10][11] identify every remaining destination byte as tail padding. + // Therefore those remaining bytes add no validity obligation. This + // derivation is independent of the derived validator and Kani's padding + // model. Thus an erroneous acceptance in either pointer harness still + // cannot materialize an invalid destination. On the accepted all-zero + // field, safe `core::ptr::null()` independently supplies the expected + // pointer by its standard-library contract [4]. Neither harness + // dereferences the result. // // Storage and bounds: Each bool harness uses one stack `u8`; the direct - // pointer harness uses one `usize` and its eight-byte representation. The - // padded harness uses one 16-byte source plus its safe snapshot; all other - // values are fixed-size compiler temporaries. No harness allocates, - // contains an explicit source loop, or uses `kani::assume`; every symbolic - // input is unconstrained. Bool harnesses use unwind one. The direct pointer - // harness uses unwind nine for an eight-byte target/helper scan plus - // termination. The padded harness uses unwind 17 for its 16-byte recovery - // comparison plus termination. Kani's unwinding checks enforce each bound. + // pointer harness uses one `usize`, its safe `Copy` value snapshot, and its + // eight-byte representation. The padded harness uses one 16-byte source + // plus its safe snapshot; all other values are fixed-size compiler + // temporaries. No harness allocates, contains an explicit source loop, or + // uses `kani::assume`; every symbolic input is unconstrained. Bool + // harnesses use unwind one. The direct pointer harness uses unwind nine for + // an eight-byte target/helper scan plus termination. The padded harness + // uses unwind 17 for its 16-byte recovery comparison plus termination. + // Kani's unwinding checks enforce each bound. // // Scope and TOOL/TCB boundary: These are end-to-end proofs only for the // listed `u8`-to-`bool`, `usize`-to-`*const u8`, and - // `[u8; 16]`-to-`PaddedPointer` instantiations on the pinned target. They do - // not prove other types, padding shapes, sizes, alignments, macro arms, or - // toolchains. Invalid-bool public paths remain uninvoked because Kani does - // not completely check invalid-value production. Reading and writing the - // reference-macro results presupposes live, dereferenceable references with - // valid lifetime, aliasing, and provenance; Kani does not completely check - // those obligations, so they remain TOOL/TCB premises rather than proof - // conclusions. Its uninitialized-memory/padding model is likewise a - // premise for the padded recovery result. In particular, this harness also - // verifies when the target body is locally replaced with the typed + // `[u8; 16]`-to-`PaddedPointer` instantiations on the pinned target. They + // do not prove other types, padding shapes, sizes, alignments, macro arms, + // or toolchains. Because Kani does not completely check invalid-value + // production, invalid-bool public paths remain uninvoked. Reading and + // writing reference-macro results presupposes live, dereferenceable + // references with valid lifetime, aliasing, and provenance; Kani does not + // completely check those obligations, so they remain TOOL/TCB premises + // rather than proof conclusions. Its uninitialized-memory/padding model is + // likewise a premise for the padded recovery result. In particular, it + // also verifies when the target body is locally replaced with the typed // `MaybeUninit>` implementation immediately before // 94f0da71; Kani does not expose that implementation's compiler-permitted // destination-padding loss. The theorem therefore observes every @@ -1448,14 +1462,37 @@ mod proofs { // https://doc.rust-lang.org/1.93.0/core/mem/fn.align_of.html // https://doc.rust-lang.org/1.93.0/core/mem/macro.offset_of.html // - // [12] https://doc.rust-lang.org/1.93.0/reference/behavior-considered-undefined.html#invalid-values - // [13] https://doc.rust-lang.org/1.93.0/reference/expressions.html#moved-and-copied-types - // https://doc.rust-lang.org/1.93.0/std/primitive.usize.html#impl-Copy-for-usize - // [14] https://doc.rust-lang.org/1.93.0/reference/types/boolean.html#logical-not + // [12] Rust 1.93 states that padding bytes need not be initialized, and + // states a struct's validity requirement in terms of its fields: + // https://doc.rust-lang.org/1.93.0/core/mem/union.MaybeUninit.html#initialization-invariant + // https://doc.rust-lang.org/1.93.0/reference/behavior-considered-undefined.html#invalid-values + // + // Padding bytes do not have to be initialized. + // + // A struct, tuple, and array requires all fields/elements to be valid + // at their respective type. + // + // [13] Rust 1.93 classifies `!` on a primitive `bool` as logical NOT and + // evaluates its operand in value-expression context: + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#negation-operators + // + // [14] Per Rust 1.93, dereferencing a pointer denotes its pointed-to + // location, and the location resulting from dereferencing `&mut T` can be + // assigned to: // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#the-dereference-operator - // https://doc.rust-lang.org/1.93.0/reference/expressions/assignment-expr.html - // [15] https://doc.rust-lang.org/1.93.0/std/macro.assert_eq.html + // + // [15] Rust 1.93 says that an assignment next copies or moves its assigned + // value to its assigned place: + // https://doc.rust-lang.org/1.93.0/reference/expressions/assignment-expr.html#basic-assignments + // + // [16] `assert_eq!` asserts equality of its operands, and primitive `bool` + // and `u8` supply the two equality operations used by the mutable harness: + // https://doc.rust-lang.org/1.93.0/std/macro.assert_eq.html + // https://doc.rust-lang.org/1.93.0/std/primitive.bool.html#impl-PartialEq-for-bool // https://doc.rust-lang.org/1.93.0/std/primitive.u8.html#impl-PartialEq-for-u8 + // + // [17] Rust 1.93 lists the primitive `usize` implementation of `Copy`: + // https://doc.rust-lang.org/1.93.0/std/primitive.usize.html#impl-Copy-for-usize #[kani::proof] #[kani::unwind(1)] @@ -1499,18 +1536,19 @@ mod proofs { let expected = checked_bool_oracle(src); cover_bool_oracle(expected); if let Some(expected) = expected { - let expected_after_mutation = !expected; + let replacement = !expected; + let replacement_byte = u8::from(replacement); let result: Result<&mut bool, ValidityError<&mut u8, bool>> = crate::try_transmute_mut!(&mut src); match result { Ok(dst) => { assert_eq!((dst as *mut bool).cast::(), src_ptr); assert_eq!(*dst, expected); - *dst = expected_after_mutation; + *dst = replacement; } Err(_) => panic!("mutable transmute rejected an independently valid bool"), } - assert_eq!(src, u8::from(expected_after_mutation)); + assert_eq!(src, replacement_byte); } } @@ -1521,21 +1559,18 @@ mod proofs { // `usize::to_ne_bytes` [8] plus the shared complete-array classifier supply // the independently observed bytes to which this family applies its // explicit zero-only pointer policy. Safe `core::ptr::null()` is the - // expected result on that branch by [4]. Before the target consumes its - // `usize` source, the shared `copy_snapshot` takes an independent safe-Rust - // pre-call value snapshot. Its documented dereference/value-expression - // kernel copies the value because `usize: Copy` [13]. On rejection, direct - // projection of the crate-visible error field avoids - // `ValidityError::into_src`, and the shared `assert_same_usize` supplies - // primitive `usize` equality independently of the target. Accessor and - // macro defects therefore cannot compensate. + // expected result on that branch by [4]. On rejection, direct projection + // of the crate-visible error field and the shared `usize` observer compare + // the restored source with the safe pre-call snapshot without calling + // `ValidityError::into_src`, so accessor and macro defects cannot + // compensate. // `#[allow(unknown_lints)]` is for `integer_to_ptr_transmutes` on the MSRV. #[allow(unknown_lints)] #[allow(integer_to_ptr_transmutes)] fn prove_try_transmute_usize_to_pointer_policy_and_recovery() { let src: usize = kani::any(); - let expected_src = copy_snapshot(&src); - let src_bytes = expected_src.to_ne_bytes(); + let snapshot = copy_snapshot(&src); + let src_bytes = snapshot.to_ne_bytes(); let expected_valid = all_zero_byte_policy_oracle(&src_bytes); let result: Result<*const u8, ValidityError> = crate::try_transmute!(src); @@ -1548,7 +1583,7 @@ mod proofs { } Err(error) => { assert!(!expected_valid); - assert_same_usize(error.src, expected_src); + assert_same_usize(error.src, snapshot); } } } diff --git a/zerocopy/src/proofs/try_from_bytes_derive.rs b/zerocopy/src/proofs/try_from_bytes_derive.rs index 9204605e6a..030236b781 100644 --- a/zerocopy/src/proofs/try_from_bytes_derive.rs +++ b/zerocopy/src/proofs/try_from_bytes_derive.rs @@ -436,7 +436,7 @@ fn prove_try_from_bytes_derive_data_enum() { // valid, accepts every payload for the `Byte` tag, and rejects every other // tag. The public API is invoked only for the first two cases, where it must // succeed and return the corresponding safe variant constructed above. The - // The Reference specifies the intended representation, but correspondence + // Reference specifies the intended representation, but correspondence // between this hand-written surrogate and the actual enum is a manually // reviewed proof-specification/TCB premise; Kani does not independently // query the enum payload offsets. This is not a generic enum-layout or diff --git a/zerocopy/src/wrappers.rs b/zerocopy/src/wrappers.rs index efbd3af665..8fbda259bc 100644 --- a/zerocopy/src/wrappers.rs +++ b/zerocopy/src/wrappers.rs @@ -1000,22 +1000,17 @@ mod proofs { // field by a language-checked value move, rather than through a reference. // Compiler/Kani lowering of the non-`Copy`, unaligned field move remains part // of the TOOL/TCB boundary below. Each - // closure maps its parameter to its body expression [4]. The bare `old`, - // `new`, and `result` paths in both bodies are capture paths rooted in the - // correspondingly named enclosing locals. Both closures omit `move`, so - // Rust infers their capture modes while preferring shared references; each - // body only reads these three locals, and therefore captures all three - // through `ImmBorrow` [38]. A local path is a place expression. Evaluating - // each captured occurrence in the assertion operand, assignment right-hand - // side, or tail result's value context obtains the stored value and copies - // it because `u8: Copy` [9][38]. Thus every `old`, `new`, and `result` use - // observes tuple fields zero, one, and two respectively. The body executes + // closure maps its parameter to its body expression [4]; the body executes // its statements in order and evaluates its final operand in value context - // [5]. Assignment copies or moves the right-hand value into the selected - // place [6]. - // Together those rules supply the expected closure input, field mutation, - // and closure result without treating compiler capture behavior as an - // unstated oracle. At the `update` function boundary, + // [5]. Both are explicitly `move` closures, so Rust captures the `old`, + // `new`, and `result` place expressions by value [38]. Since `u8: Copy`, + // each captured value is an exact byte copy and the original outer binding + // remains usable for the post-call observations [38]. Every use of those + // names in a closure body therefore evaluates the captured copy, rather + // than consulting a target result. Assignment copies or moves the + // right-hand value into the selected place [6]. Together those rules supply + // the expected closure input, field mutation, and closure result. At the + // `update` function boundary, // `return f(t)` short-circuits the implicit return while the tail expression // `ret` is returned to the caller [7]. Those two language paths map directly // to the two `returned` assertions. @@ -1330,17 +1325,11 @@ mod proofs { // 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 - // [38] Rust 1.93 specifies that a non-`move` closure infers captures while - // preferring shared references; capture modes borrow or move environmental - // places; local paths are place expressions; evaluating a place in value - // context obtains its stored value and copies it for `Copy` types; and - // `u8` implements `Copy`: - // https://doc.rust-lang.org/1.93.0/reference/expressions/closure-expr.html#r-expr.closure.capture-inference + // [38] Rust 1.93 specifies that `move` closures capture referenced place + // expressions by value. Reading a `Copy` value in value-expression context + // copies rather than moves it, and primitive `u8` implements `Copy`: // https://doc.rust-lang.org/1.93.0/reference/types/closure.html#capture-modes - // https://doc.rust-lang.org/1.93.0/reference/types/closure.html#copy-values - // https://doc.rust-lang.org/1.93.0/reference/expressions/path-expr.html#r-expr.path.place - // https://doc.rust-lang.org/1.93.0/reference/expressions.html#r-expr.move.intro - // https://doc.rust-lang.org/1.93.0/reference/expressions.html#r-expr.move.copy + // https://doc.rust-lang.org/1.93.0/reference/expressions.html#moved-and-copied-types // https://doc.rust-lang.org/1.93.0/std/primitive.u8.html#impl-Copy-for-u8 // [39] Rust 1.93 specifies that `&&` is logical AND and evaluates its right // operand only when its left operand is true: @@ -1399,7 +1388,7 @@ mod proofs { let (old, new, result) = any_unalign_update_values(); let mut value = Unalign(Byte(old)); - let returned = value.update(|value| { + let returned = value.update(move |value| { assert_eq!(value.0, old); value.0 = new; result @@ -1435,7 +1424,7 @@ mod proofs { assert!(!receiver.is_aligned()); kani::cover!(!receiver.is_aligned(), "write-back receiver is physically misaligned"); - let returned = backing.value.update(|value| { + let returned = backing.value.update(move |value| { assert_eq!(value.value, old); value.value = new; result