[kani] Prove bounded UTF-8 validation

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::<Unaligned>` and `is_bit_valid::<Aligned>` 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::<ReadOnly<str>, Initialized, CastUnsized, BecauseImmutable>();
+        let unaligned_valid = <str as TryFromBytes>::is_bit_valid(candidate.reborrow_shared());
+        let aligned_candidate = candidate.reborrow_shared().bikeshed_recall_aligned();
+        let aligned_valid = <str as TryFromBytes>::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)]