diff --git a/zerocopy/src/impls.rs b/zerocopy/src/impls.rs index 1cb39f731a..12ffb7b24f 100644 --- a/zerocopy/src/impls.rs +++ b/zerocopy/src/impls.rs @@ -1385,10 +1385,13 @@ mod simd { #[cfg(kani)] mod proofs { - use core::num::NonZeroU16; + #[cfg(feature = "alloc")] + use alloc::boxed::Box; + use core::{mem, num::NonZeroU16, ptr::NonNull}; use crate::proof_support::{ - bool_from_byte, char_from_ne_bytes, nonzero_u16_from_ne_bytes, validate_and_read_sized, + all_zero_byte_policy_oracle, bool_from_byte, char_from_ne_bytes, nonzero_u16_from_ne_bytes, + validate_and_read_sized, }; // Configuration: Every harness in this module uses the common Kani CI @@ -1600,6 +1603,196 @@ mod proofs { assert_eq!(Some(values[3]), expected[3]); } } + + // Domain: Every initialized eight-byte source sequence for the thin + // pointer-bearing monomorphizations below. Eight bytes is the pointer size + // of the common 64-bit Kani CI target documented above. + // + // Storage and bounds: Every harness uses one fixed eight-byte stack input. + // Separate copies at byte offsets zero and one within 16-aligned `repr(C)` + // storage exercise the `Unaligned` specialization at both addresses. The + // `Aligned` specialization runs at offset zero; the offset-one address is + // independently confirmed physically misaligned and is therefore not + // passed under that marker. Compiler alignment queries and the standard + // raw-pointer `is_aligned` operation check this matrix before any zerocopy + // validator runs. The asserted nontrivial destination alignment is a + // fail-closed fact of the pinned compiler and target, not a claim that + // Rust's general pointer-layout rules universally fix that alignment; the + // independent placement oracle is `is_aligned` on each actual address. The + // public API makes its own aligned candidate. None dynamically allocates. + // In particular, the + // `Option>` harness constructs and reads only `None`, never a + // `Box`, so it exercises the null niche without exercising allocation. The + // proof source contains no explicit loop. No harness uses `kani::assume`; + // every initialized eight-byte input is unconstrained. The fixed pointer + // width and same-size premises use compiler `size_of` values compared + // through shared `assert_same_usize` [5]; that helper supplies equality + // mechanics, while the expected width is pinned configuration and the + // same-size relation is a fail-closed case premise. The destination + // greater-than-one guards use primitive `usize` ordering [6]. + // `#[kani::unwind(9)]` permits each modeled oracle array comparison or + // target scan to examine eight bytes and terminate, with Kani's unwinding + // checks enforcing the bound. + // + // Establishes: At the aligned placement, both `Unaligned` and `Aligned` + // type-level markers, and at the deliberately physically misaligned + // placement, the `Unaligned` marker, make the non-materializing raw-byte + // validator implement zerocopy's conservative policy of accepting exactly + // the all-zero byte sequence. On that independently known-valid input, the + // public read API succeeds; a raw-pointer read is null and a niche `Option` + // read is `None`. + // + // Oracle: The shared `all_zero_byte_policy_oracle` compares the complete + // candidate with a Rust repeat-array expression through safe iteration and + // primitive equality; its adjacent documentation supplies the exact Rust + // 1.93 contracts. A true result therefore establishes that every candidate + // byte is zero without manually reconstructing an integer or calling a + // zerocopy target. This family separately adopts that classification as its + // explicit representation-policy oracle, evaluated before the target byte + // scan rather than inferred from agreement with that scan. + // `validate_and_read_sized!` compares the + // target with this predicate at every in-scope placement and only + // materializes an oracle-valid candidate. The standard library guarantees + // that zero-initializing a thin raw pointer produces null [1] and that an + // all-zero representation produces `None` for every optional pointer + // family instantiated below [2]. The safe `is_null` [3] and `is_none` [4] + // operations then independently classify the already-valid result. These + // output oracles do not themselves establish representation validity. + // + // Excludes: This does not claim that rejected nonzero bytes are invalid + // Rust pointers, and it does not quantify over arbitrary absolute + // addresses or offsets other than zero and one in the controlled storage. + // It also excludes the public read API's rejected-input path, fat pointers, + // other pointees, function signatures and ABIs, and non-Kani targets. + // Reference aliasing, raw-pointer provenance, invalid-value production, and + // uninitialized-memory handling along the composite cast/validation/read + // path remain TOOL/TCB premises because Kani does not completely check + // those semantics. The initialized source storage and independently valid + // accepted representation do not establish those unmodeled obligations. + // + // [1] Per https://doc.rust-lang.org/1.93.0/std/ptr/fn.null.html and + // https://doc.rust-lang.org/1.93.0/std/ptr/fn.null_mut.html: + // + // Creates a null raw pointer. + // + // This function is equivalent to zero-initializing the pointer: + // `MaybeUninit::<*const T>::zeroed().assume_init()`. The resulting + // pointer has the address 0. + // + // Creates a null mutable raw pointer. + // + // This function is equivalent to zero-initializing the pointer: + // `MaybeUninit::<*mut T>::zeroed().assume_init()`. The resulting pointer + // has the address 0. + // + // [2] Per https://doc.rust-lang.org/1.93.0/std/option/index.html#representation, + // whose guarantee table includes references, `NonNull`, function pointers, + // and `Box` (specifically `Box`) when `U: Sized`: + // + // `transmute::<_, Option>([0u8; size_of::()])` is sound and + // produces `Option::::None`. + // + // [3] Per https://doc.rust-lang.org/1.93.0/std/primitive.pointer.html#method.is_null: + // + // `is_null` returns `true` when the raw pointer is null. + // + // [4] Per https://doc.rust-lang.org/1.93.0/std/option/enum.Option.html#method.is_none: + // + // `is_none` returns `true` when the option is `None`. + // + // [5] https://doc.rust-lang.org/1.93.0/std/mem/fn.size_of.html + // 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 + // + // [6] https://doc.rust-lang.org/1.93.0/std/mem/fn.align_of.html + // https://doc.rust-lang.org/1.93.0/std/cmp/trait.PartialOrd.html#method.gt + // https://doc.rust-lang.org/1.93.0/std/primitive.usize.html#impl-PartialOrd-for-usize + macro_rules! zero_only_pointer_proof { + ($proof:ident, $ty:ty, $zero:expr, $value:ident => $assertion:expr) => { + #[kani::proof] + #[kani::unwind(9)] + fn $proof() { + crate::proof_support::assert_same_usize(mem::size_of::(), 8); + crate::proof_support::assert_same_usize( + mem::size_of::<$ty>(), + mem::size_of::(), + ); + assert!(mem::align_of::<$ty>() > 1); + let bytes: [u8; mem::size_of::<$ty>()] = kani::any(); + let expected_valid = all_zero_byte_policy_oracle(&bytes); + let expected = if expected_valid { Some($zero) } else { None }; + let result = validate_and_read_sized!($ty, bytes, expected); + kani::cover!(expected_valid); + kani::cover!(!expected_valid); + if let Some($value) = result { + $assertion; + } + } + }; + } + + zero_only_pointer_proof!( + prove_const_pointer_try_read_from_bytes, + *const u8, + core::ptr::null(), + value => assert!(value.is_null()) + ); + zero_only_pointer_proof!( + prove_mut_pointer_try_read_from_bytes, + *mut u8, + core::ptr::null_mut(), + value => assert!(value.is_null()) + ); + zero_only_pointer_proof!( + prove_option_non_null_try_read_from_bytes, + Option>, + None, + value => assert!(value.is_none()) + ); + zero_only_pointer_proof!( + prove_option_ref_try_read_from_bytes, + Option<&'static u8>, + None, + value => assert!(value.is_none()) + ); + zero_only_pointer_proof!( + prove_option_mut_ref_try_read_from_bytes, + Option<&'static mut u8>, + None, + value => assert!(value.is_none()) + ); + #[cfg(feature = "alloc")] + zero_only_pointer_proof!( + prove_option_box_try_read_from_bytes, + Option>, + None, + value => assert!(value.is_none()) + ); + zero_only_pointer_proof!( + prove_option_fn_try_read_from_bytes, + Option, + None, + value => assert!(value.is_none()) + ); + zero_only_pointer_proof!( + prove_option_unsafe_fn_try_read_from_bytes, + Option, + None, + value => assert!(value.is_none()) + ); + zero_only_pointer_proof!( + prove_option_extern_c_fn_try_read_from_bytes, + Option, + None, + value => assert!(value.is_none()) + ); + zero_only_pointer_proof!( + prove_option_unsafe_extern_c_fn_try_read_from_bytes, + Option, + None, + value => assert!(value.is_none()) + ); } #[cfg(test)] diff --git a/zerocopy/src/proof_support.rs b/zerocopy/src/proof_support.rs index 39e4f5a28c..6ba8f28afa 100644 --- a/zerocopy/src/proof_support.rs +++ b/zerocopy/src/proof_support.rs @@ -382,6 +382,31 @@ pub(crate) fn nonzero_u16_from_ne_bytes(bytes: [u8; 2]) -> Option(bytes: &[u8; N]) -> bool { + bytes.iter().copied().eq([0u8; N].iter().copied()) +} + // Generate every `usize` in the inclusive range `0..=max` without scattering // domain arithmetic across harnesses. The common Kani configuration documents // that `kani::any::()` produces an arbitrary valid target `usize`.