diff --git a/zerocopy/src/impls.rs b/zerocopy/src/impls.rs index 12ffb7b24f..f2a0a44c06 100644 --- a/zerocopy/src/impls.rs +++ b/zerocopy/src/impls.rs @@ -1389,9 +1389,14 @@ mod proofs { use alloc::boxed::Box; use core::{mem, num::NonZeroU16, ptr::NonNull}; - use crate::proof_support::{ - all_zero_byte_policy_oracle, bool_from_byte, char_from_ne_bytes, nonzero_u16_from_ne_bytes, - validate_and_read_sized, + use crate::{ + 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, + }, + wrappers::ReadOnly, + TryFromBytes, }; // Configuration: Every harness in this module uses the common Kani CI @@ -1793,6 +1798,246 @@ mod proofs { None, 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`. + // + // 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 + // 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. + // + // 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. + // + // 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. + // + // 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. + // + // 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. + // + // [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 + // [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 + // [6] https://doc.rust-lang.org/1.93.0/std/ptr/fn.addr_eq.html + // [7] https://doc.rust-lang.org/1.93.0/std/primitive.str.html#method.as_bytes + // [8] https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.len + // https://doc.rust-lang.org/1.93.0/std/macro.assert_eq.html + // https://doc.rust-lang.org/1.93.0/std/cmp/trait.PartialEq.html#tymethod.eq + // https://doc.rust-lang.org/1.93.0/std/primitive.usize.html#impl-PartialEq-for-usize + // https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.iter + // https://doc.rust-lang.org/1.93.0/std/iter/trait.Iterator.html#method.copied + // https://doc.rust-lang.org/1.93.0/std/iter/trait.Iterator.html#method.eq + // 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 assert_str_validators_match(bytes: &[u8], expected_valid: bool) { + 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 aligned_candidate = candidate.reborrow_shared().bikeshed_recall_aligned(); + let aligned_valid = ::is_bit_valid(aligned_candidate); + assert_same_bool(unaligned_valid, expected_valid); + assert_same_bool(aligned_valid, expected_valid); + } + + fn assert_empty_valid_str_borrow(bytes: &[u8]) { + match str::try_ref_from_bytes(bytes) { + Ok(value) => assert_same_u8_elements(value.as_bytes(), bytes), + Err(_) => assert_same_bool(false, true), + } + } + + fn assert_nonempty_valid_str_borrow(bytes: &[u8]) { + match str::try_ref_from_bytes(bytes) { + Ok(value) => { + assert_same_u8_elements(value.as_bytes(), bytes); + assert_same_bool(core::ptr::addr_eq(value.as_ptr(), bytes.as_ptr()), true); + } + Err(_) => assert_same_bool(false, true), + } + } + + macro_rules! str_validator_proof { + ($proof:ident, $len:expr) => { + #[kani::proof] + #[kani::unwind(5)] + fn $proof() { + let bytes: [u8; $len] = kani::any(); + let expected_valid = utf8_oracle(&bytes); + match expected_valid { + true => kani::cover!(true, "independent grammar accepts this byte sequence"), + false => kani::cover!(true, "independent grammar rejects this byte sequence"), + } + assert_str_validators_match(&bytes, expected_valid); + } + }; + } + + #[kani::proof] + #[kani::unwind(5)] + fn prove_empty_str_validators() { + let bytes: [u8; 0] = []; + let expected_valid = utf8_oracle(&bytes); + assert_same_bool(expected_valid, true); + kani::cover!(expected_valid, "empty input is accepted"); + assert_str_validators_match(&bytes, expected_valid); + } + + str_validator_proof!(prove_one_byte_str_validators, 1); + str_validator_proof!(prove_two_byte_str_validators, 2); + str_validator_proof!(prove_three_byte_str_validators, 3); + str_validator_proof!(prove_four_byte_str_validators, 4); + + #[kani::proof] + #[kani::unwind(5)] + fn prove_empty_str_try_ref_from_bytes() { + let bytes: [u8; 0] = []; + let expected_valid = utf8_oracle(&bytes); + kani::cover!(expected_valid, "empty input is accepted"); + match expected_valid { + true => assert_empty_valid_str_borrow(&bytes), + false => assert_same_bool(false, true), + } + } + + macro_rules! nonempty_str_borrow_proof { + ($proof:ident, $len:expr) => { + #[kani::proof] + #[kani::unwind(5)] + fn $proof() { + let bytes: [u8; $len] = kani::any(); + match utf8_oracle(&bytes) { + true => { + kani::cover!(true, "independent grammar accepts this byte sequence"); + assert_nonempty_valid_str_borrow(&bytes); + } + false => { + kani::cover!(true, "independent grammar rejects this byte sequence"); + } + } + } + }; + } + + nonempty_str_borrow_proof!(prove_one_byte_str_try_ref_from_bytes, 1); + nonempty_str_borrow_proof!(prove_two_byte_str_try_ref_from_bytes, 2); + nonempty_str_borrow_proof!(prove_three_byte_str_try_ref_from_bytes, 3); + nonempty_str_borrow_proof!(prove_four_byte_str_try_ref_from_bytes, 4); } #[cfg(test)]