diff --git a/zerocopy/agent_docs/validation.md b/zerocopy/agent_docs/validation.md index 6feee79a7e..124f8183ca 100644 --- a/zerocopy/agent_docs/validation.md +++ b/zerocopy/agent_docs/validation.md @@ -57,6 +57,16 @@ usually sufficient. (token streams) in `zerocopy-derive/src/output_tests.rs`. - **Formal Verification (Kani):** Place Kani proofs in a `mod proofs` module within the source file they test. + - **Generated-output exception:** A semantic proof of proc-macro-generated + code may live in a focused child of the consuming source file's inline + `mod proofs` when the defining proc-macro crate cannot invoke its own + macro and the proof requires consumer-crate internals. Keep each concrete + derive invocation beside the harness that verifies its expansion, and + cross-link the consumer proof and generator source so that changes to + either side trigger review. This exception covers only the enumerated + concrete expansions and their linked runtime paths; it does not turn + consumer-side verification into a universal theorem about the generator + or its token output. - **Purpose:** Use the [Kani Rust Verifier](https://model-checking.github.io/kani/) to prove the soundness of `unsafe` code or code relied upon by `unsafe` blocks. Unlike diff --git a/zerocopy/src/lib.rs b/zerocopy/src/lib.rs index d5c2d5dcbe..68d0a2efe0 100644 --- a/zerocopy/src/lib.rs +++ b/zerocopy/src/lib.rs @@ -366,6 +366,11 @@ mod macros; pub mod pointer; #[cfg(kani)] mod proof_support; +#[cfg(kani)] +mod proofs { + #[cfg(feature = "derive")] + mod try_from_bytes_derive; +} mod r#ref; mod split_at; // FIXME(#252): If we make this pub, come up with a better name. diff --git a/zerocopy/src/proofs/try_from_bytes_derive.rs b/zerocopy/src/proofs/try_from_bytes_derive.rs new file mode 100644 index 0000000000..9204605e6a --- /dev/null +++ b/zerocopy/src/proofs/try_from_bytes_derive.rs @@ -0,0 +1,460 @@ +// SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT +// +// Copyright 2026 The Fuchsia Authors +// +// Licensed under the 2-Clause BSD License , Apache License, Version 2.0 +// , or the MIT +// license , at your option. +// This file may not be copied, modified, or distributed except according to +// those terms. + +//! Representative Kani regression proofs for generated implementations. +//! +//! Placement and ownership: the concrete implementations exercised here are +//! emitted by `zerocopy-derive/src/derive/try_from_bytes.rs` into the fixture +//! types below. A proc-macro crate cannot invoke its own macro, while these +//! proofs also require the consuming `zerocopy` crate's private pointer and +//! validation machinery. The fixtures and harnesses therefore live together +//! in this focused child of `lib.rs`'s inline `mod proofs`, as permitted by the +//! generated-output exception in `agent_docs/validation.md`. The generator and +//! runtime crate jointly own these integration theorems; changing either side +//! requires rerunning them. +//! +//! 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, +//! `-Zfunction-contracts`, and one layout selected by `--randomize-layout` per +//! invocation. +//! +//! Storage and bounds: Each of the four harnesses uses one fixed-size input +//! array. The shared validator copies it into explicit offset-zero and +//! offset-one source subobjects: both exercise the `Unaligned` type marker, +//! while each source exercises `Aligned` only when Rust's raw-pointer +//! `is_aligned` oracle says its physical address is aligned for the target +//! type. The public read makes its own aligned candidate. Oracle witnesses and +//! layout surrogates are also fixed size. None performs dynamic allocation, +//! and the proof source contains no explicit loop. Every representation copy +//! is at most eight bytes on the common Kani target. Every harness carries +//! `#[kani::unwind(9)]`, permitting an inlined bytewise operation to examine +//! those eight bytes and terminate, with Kani's unwinding checks enforcing the +//! bound. The two concrete placements do not prove arbitrary absolute +//! addresses or offsets other than zero and one. +//! +//! These harnesses exercise the shared non-materializing +//! `ReadOnly`/`Ptr`/cast path ending in generated +//! [`TryFromBytes::is_bit_valid`] methods on initialized bytes with both the +//! `Unaligned` and `Aligned` type-level markers. They therefore prove those +//! composite paths, not the generated method in isolation. They +//! invoke the public value-reading API only after an independent safe +//! construction and documented layout rules establish that the candidate +//! representation is valid. Each theorem covers one fixed, sized derive input +//! and every byte pattern for that input on Kani's target. This is not a +//! generator theorem: it does not cover other derive inputs, configurations, +//! targets, or properties absent from Kani's memory model. The sized inputs +//! also deliberately avoid the nested-DST layout issue tracked in #3630. +//! +//! Exact-candidate validity premise: every candidate byte is initialized, and +//! compiler-computed `offset_of!` results, including direct nested field paths, +//! select each field's bytes [4]. For +//! structs, the +//! Reference "requires all fields/elements to be valid at their respective +//! type"; for enums, "all fields of the variant indicated by that discriminant +//! must be valid at their respective type" [1]. These rules impose no +//! padding-value condition. Consistently, for a representation with +//! "initialized bytes at byte offsets where the type has padding", +//! `MaybeUninit` documents that copying may lose those bytes while "the original +//! value will be preserved" [2]. Thus matching field values establish candidate +//! validity even when witness padding differs. This excludes extra user +//! invariants and remains a language premise rather than a Kani theorem. +//! For each `char` field, `char_from_bytes` safely selects the suffix at the +//! compiler-reported field offset and then asks `slice::first_chunk::<4>` for +//! its first four bytes [9]. Either safe operation fails closed if the +//! compiler-reported field is not fully in bounds; no `offset + 4` range end is +//! reconstructed. Dereferencing the returned array reference copies the +//! `[u8; 4]` because its element type is `Copy` [3]; that array then reaches the +//! shared `char_from_ne_bytes` oracle. The oracle's exact Rust 1.93.0 +//! `u32::from_ne_bytes`/`char::from_u32` bridge contracts and 32-bit `char` +//! representation premise are documented beside that helper. +//! +//! [1]: https://doc.rust-lang.org/1.93.0/reference/behavior-considered-undefined.html#invalid-values +//! [2]: https://doc.rust-lang.org/1.93.0/core/mem/union.MaybeUninit.html#validity +//! [3]: 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.array.html#trait-implementations-1 +//! https://doc.rust-lang.org/1.93.0/std/primitive.u8.html#impl-Copy-for-u8 +//! +//! [4]: https://doc.rust-lang.org/1.93.0/core/mem/macro.offset_of.html +//! +//! Expands to the offset in bytes of a field from the beginning of the +//! given type. +//! +//! For the packed struct, the `repr(C)` algorithm places fields in declaration +//! order after any required padding [5], while `packed(1)` guarantees no +//! inter-field padding [6]. The proof does not manually replay that algorithm: +//! it obtains the actual offsets and sizes from the compiler and checks that +//! both field ranges are in bounds, nonoverlapping, and together exhaust the +//! representation. `usize::checked_add` computes the range ends and combined +//! size, refutable `let...else` patterns make arithmetic failure fail closed, +//! and primitive `usize` ordering supplies the bound and disjointness +//! comparisons [10]. All size, alignment, offset, and length equality +//! assertions use the +//! shared `assert_same_usize`; its `assert_eq!`/`usize::PartialEq` operations +//! supply only equality mechanics, while compiler queries and the cited +//! language rules supply the operands [11]. +//! +//! [5]: https://doc.rust-lang.org/1.93.0/reference/type-layout.html#the-c-representation +//! [6]: https://doc.rust-lang.org/1.93.0/reference/type-layout.html#the-alignment-modifiers +//! [7]: https://doc.rust-lang.org/1.93.0/reference/type-layout.html#primitive-data-layout +//! [8]: https://doc.rust-lang.org/1.93.0/std/primitive.u8.html#method.from_ne_bytes +//! [9]: https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.get +//! https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.first_chunk +//! [10]: https://doc.rust-lang.org/1.93.0/std/primitive.usize.html#method.checked_add +//! https://doc.rust-lang.org/1.93.0/reference/statements.html#let-statements +//! https://doc.rust-lang.org/1.93.0/std/cmp/trait.PartialOrd.html +//! [11]: 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 + +use crate::{ + proof_support::{ + assert_same_usize, bool_from_byte, char_from_ne_bytes, validate_and_read_sized, + }, + TryFromBytes, +}; + +fn char_from_bytes(bytes: &[u8], offset: usize) -> Option { + let Some(suffix) = bytes.get(offset..) else { + panic!("compiler-reported char field must start within the representation") + }; + let Some(representation) = suffix.first_chunk::<4>() else { + panic!("compiler-reported char field must fit in the representation") + }; + char_from_ne_bytes(*representation) +} + +// Rust specifies that `u8` occupies one byte [7], and `u8::from_ne_bytes` +// constructs the integer whose memory representation is that byte [8]. Keep +// this language oracle explicit when a candidate representation becomes a +// safe `u8` field value; merely reusing the candidate byte as a value would +// leave the representation connection implicit. +fn u8_from_byte_representation(byte: u8) -> u8 { + u8::from_ne_bytes([byte]) +} + +fn cover_bool_cross_product(first: bool, second: bool) { + kani::cover!(first && second); + kani::cover!(first && !second); + kani::cover!(!first && second); + kani::cover!(!first && !second); +} + +// Use compiler-reported sizes and offsets as the layout oracle. Two +// nonoverlapping in-bounds field ranges whose sizes sum to the representation +// size exhaust it; no manually reconstructed `repr(C)` formula is needed. +fn assert_two_fields_cover( + representation_len: usize, + first_offset: usize, + first_size: usize, + second_offset: usize, + second_size: usize, +) { + let Some(first_end) = first_offset.checked_add(first_size) else { + panic!("first compiler-reported field range must not overflow") + }; + let Some(second_end) = second_offset.checked_add(second_size) else { + panic!("second compiler-reported field range must not overflow") + }; + assert!(first_end <= representation_len); + assert!(second_end <= representation_len); + assert!(first_end <= second_offset || second_end <= first_offset); + let Some(covered_size) = first_size.checked_add(second_size) else { + panic!("combined compiler-reported field size must not overflow") + }; + assert_same_usize(covered_size, representation_len); +} + +#[allow(dead_code)] +#[derive(TryFromBytes)] +#[repr(C)] +struct BoolAndChar { + flag: bool, + character: char, +} + +#[kani::proof] +#[kani::unwind(9)] +fn prove_try_from_bytes_derive_struct() { + let bytes = kani::any::<[u8; core::mem::size_of::()]>(); + let flag_offset = core::mem::offset_of!(BoolAndChar, flag); + let character_offset = core::mem::offset_of!(BoolAndChar, character); + let flag = bool_from_byte(bytes[flag_offset]); + let character = char_from_bytes(&bytes, character_offset); + let flag_valid = flag.is_some(); + let character_valid = character.is_some(); + let expected = match (flag, character) { + (Some(flag), Some(character)) => Some(BoolAndChar { flag, character }), + _ => None, + }; + + // Domain: all initialized representations of this fixed `repr(C)` type. + // Establishes: the composite non-materializing Ptr/cast/generated-validator + // path accepts exactly when both fields do. On those independently valid + // inputs, the public value-reading API succeeds and returns the oracle's + // field values. + // Oracle: actual field offsets plus safe checked `char` construction and the + // shared `bool` language-validity oracle. This is not a derive-generator or + // generic struct-layout theorem. + cover_bool_cross_product(flag_valid, character_valid); + let read = validate_and_read_sized!(BoolAndChar, bytes, expected); + if let Some(BoolAndChar { flag: actual_flag, character: actual_character }) = read { + assert_eq!(Some(actual_flag), flag); + assert_eq!(Some(actual_character), character); + } +} + +#[allow(dead_code)] +#[derive(TryFromBytes)] +#[repr(C, packed)] +struct PackedBoolAndChar { + flag: bool, + character: char, +} + +#[kani::proof] +#[kani::unwind(9)] +fn prove_try_from_bytes_derive_packed_struct() { + let bytes = kani::any::<[u8; core::mem::size_of::()]>(); + let flag_offset = core::mem::offset_of!(PackedBoolAndChar, flag); + let character_offset = core::mem::offset_of!(PackedBoolAndChar, character); + // Ask the compiler for every layout input, then check the complete field + // ranges rather than reconstructing the packed layout algorithm. + assert_two_fields_cover( + core::mem::size_of::(), + flag_offset, + core::mem::size_of::(), + character_offset, + core::mem::size_of::(), + ); + let flag = bool_from_byte(bytes[flag_offset]); + let character = char_from_bytes(&bytes, character_offset); + let flag_valid = flag.is_some(); + let character_valid = character.is_some(); + let expected = match (flag, character) { + (Some(flag), Some(character)) => Some(PackedBoolAndChar { flag, character }), + _ => None, + }; + + // Domain: all initialized representations of this fixed packed type. + // Establishes: the composite non-materializing Ptr/cast/generated-validator + // path accepts exactly when both fields do. On those independently valid + // inputs, the public value-reading API succeeds and returns the oracle's + // field values. + // Oracle: compiler-reported size and packed field offsets, explicit + // in-bounds/nonoverlapping/exhaustive range checks grounded in the cited + // `repr(C)` and `packed(1)` rules, safe checked `char` construction, and the + // shared `bool` language-validity oracle. This does not generalize to other + // packing, alignment, or field combinations. + cover_bool_cross_product(flag_valid, character_valid); + let read = validate_and_read_sized!(PackedBoolAndChar, bytes, expected); + // Move packed fields into aligned locals before comparing them. + if let Some(PackedBoolAndChar { flag: actual_flag, character: actual_character }) = read { + assert_eq!(Some(actual_flag), flag); + assert_eq!(Some(actual_character), character); + } +} + +#[allow(dead_code)] +#[derive(Copy, Clone, TryFromBytes)] +#[repr(C)] +struct BoolFirst { + flag: bool, + byte: u8, +} + +#[allow(dead_code)] +#[derive(Copy, Clone, TryFromBytes)] +#[repr(C)] +struct BoolLast { + byte: u8, + flag: bool, +} + +#[allow(dead_code)] +#[derive(TryFromBytes)] +#[repr(C)] +union BoolAtEitherEnd { + first: BoolFirst, + last: BoolLast, +} + +#[kani::proof] +#[kani::unwind(9)] +fn prove_try_from_bytes_derive_union() { + let bytes = kani::any::<[u8; core::mem::size_of::()]>(); + let first_offset = core::mem::offset_of!(BoolAtEitherEnd, first.flag); + let first_byte_offset = core::mem::offset_of!(BoolAtEitherEnd, first.byte); + let last_offset = core::mem::offset_of!(BoolAtEitherEnd, last.flag); + let last_byte_offset = core::mem::offset_of!(BoolAtEitherEnd, last.byte); + assert_same_usize(core::mem::size_of::(), 1); + assert_same_usize(core::mem::size_of::(), 1); + assert_two_fields_cover( + bytes.len(), + first_offset, + core::mem::size_of::(), + first_byte_offset, + core::mem::size_of::(), + ); + assert_two_fields_cover( + bytes.len(), + last_offset, + core::mem::size_of::(), + last_byte_offset, + core::mem::size_of::(), + ); + let first = bool_from_byte(bytes[first_offset]); + let last = bool_from_byte(bytes[last_offset]); + let first_byte = u8_from_byte_representation(bytes[first_byte_offset]); + let last_byte = u8_from_byte_representation(bytes[last_byte_offset]); + let first_valid = first.is_some(); + let last_valid = last.is_some(); + + // The compiler-reported sizes and effective offsets satisfy the explicit + // coverage checks above: either active field consists of two one-byte + // fields at distinct in-bounds offsets in this two-byte union. The safely + // constructed active field therefore reconstructs the exact candidate + // bytes without relying on a padding premise or an inactive field. No + // union field is read by this proof. + let expected = if let Some(flag) = first { + Some(BoolAtEitherEnd { first: BoolFirst { flag, byte: first_byte } }) + } else { + last.map(|flag| BoolAtEitherEnd { last: BoolLast { byte: last_byte, flag } }) + }; + + // Domain: all initialized representations of this fixed two-field union. + // Establishes: the composite non-materializing + // Ptr/cast/generated-validator path accepts iff at least one field + // interpretation is valid, using actual union and struct field offsets + // plus the shared `bool` oracle. On accepted inputs, the public value-read + // succeeds. The OR is explicitly a zerocopy policy oracle, not evidence + // about Rust union validity or a theorem about every union or derive input. + cover_bool_cross_product(first_valid, last_valid); + // Union fields cannot be inspected through safe Rust, so the returned value + // is deliberately not used as a value oracle. + let _ = validate_and_read_sized!(BoolAtEitherEnd, bytes, expected); +} + +#[allow(dead_code)] +#[derive(TryFromBytes)] +#[repr(u8)] +enum BoolOrByte { + Bool(bool), + Byte(u8), +} + +#[allow(dead_code)] +#[derive(Copy, Clone)] +#[repr(u8)] +enum BoolOrByteTag { + Bool, + Byte, +} + +#[derive(Copy, Clone)] +#[repr(C)] +struct BoolVariantRepr { + tag: BoolOrByteTag, + payload: bool, +} + +#[derive(Copy, Clone)] +#[repr(C)] +struct ByteVariantRepr { + tag: BoolOrByteTag, + payload: u8, +} + +#[allow(dead_code)] +#[derive(Copy, Clone)] +#[repr(C)] +union BoolOrByteRepr { + bool_variant: BoolVariantRepr, + byte_variant: ByteVariantRepr, +} + +#[kani::proof] +#[kani::unwind(9)] +fn prove_try_from_bytes_derive_data_enum() { + let bytes = kani::any::<[u8; core::mem::size_of::()]>(); + + // Residual language-layout rule: Rust Reference 1.93.0 specifies a + // primitive-representation enum with fields as a `repr(C)` union of + // `repr(C)` variant structs, whose first field is the tag and remaining + // fields are the variant payload [1]. Both the real enum and its tag + // surrogate declare the same implicit variants in the same order, so the + // Reference's implicit-discriminant rules give them the same tags [2]. The + // surrogate types above encode those language rules; `offset_of!` supplies + // every union and struct offset rather than duplicating byte positions. + // + // [1] Per https://doc.rust-lang.org/1.93.0/reference/type-layout.html#primitive-representation-of-enums-with-fields: + // + // Each union member is a `repr(C)` struct whose first field is the + // primitive-representation tag of the fieldless enum; "the remaining + // fields are the fields of that variant." + // + // [2] Per https://doc.rust-lang.org/1.93.0/reference/items/enumerations.html#implicit-discriminants: + // + // If the discriminant of the first variant ... is unspecified, then it + // is set to zero. Each later implicit discriminant is "one higher than + // the discriminant of the previous variant". + // + // [3] Per https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#enum-cast: + // + // A fieldless enum value can be cast to an integer, producing its + // discriminant value; the following numeric cast produces `u8` here. + assert_same_usize(core::mem::size_of::(), core::mem::size_of::()); + assert_same_usize(core::mem::align_of::(), core::mem::align_of::()); + let tag_offset = core::mem::offset_of!(BoolOrByteRepr, bool_variant.tag); + let byte_tag_offset = core::mem::offset_of!(BoolOrByteRepr, byte_variant.tag); + assert_same_usize(tag_offset, byte_tag_offset); + let bool_payload_offset = core::mem::offset_of!(BoolOrByteRepr, bool_variant.payload); + let byte_payload_offset = core::mem::offset_of!(BoolOrByteRepr, byte_variant.payload); + let tag = u8_from_byte_representation(bytes[tag_offset]); + let byte_payload = u8_from_byte_representation(bytes[byte_payload_offset]); + let bool_payload = bool_from_byte(bytes[bool_payload_offset]); + let bool_payload_valid = bool_payload.is_some(); + let expected = if tag == BoolOrByteTag::Bool as u8 { + bool_payload.map(BoolOrByte::Bool) + } else if tag == BoolOrByteTag::Byte as u8 { + Some(BoolOrByte::Byte(byte_payload)) + } else { + None + }; + + // Domain: all initialized representations of this fixed + // `repr(u8)` data enum. Establishes: the composite non-materializing + // Ptr/cast/generated-validator path requires the `Bool` tag's payload to be + // 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 + // 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 + // derive-generator theorem. + kani::cover!(tag == BoolOrByteTag::Bool as u8 && bool_payload_valid); + kani::cover!(tag == BoolOrByteTag::Bool as u8 && !bool_payload_valid); + kani::cover!(tag == BoolOrByteTag::Byte as u8); + kani::cover!(tag >= 2); + let read = validate_and_read_sized!(BoolOrByte, bytes, expected); + match read { + Some(BoolOrByte::Bool(actual)) => { + assert_eq!(tag, BoolOrByteTag::Bool as u8); + assert_eq!(Some(actual), bool_payload); + } + Some(BoolOrByte::Byte(actual)) => { + assert_eq!(tag, BoolOrByteTag::Byte as u8); + assert_eq!(actual, byte_payload); + } + None => {} + } +} diff --git a/zerocopy/zerocopy-derive/src/derive/try_from_bytes.rs b/zerocopy/zerocopy-derive/src/derive/try_from_bytes.rs index f77b765bba..330f6e4cce 100644 --- a/zerocopy/zerocopy-derive/src/derive/try_from_bytes.rs +++ b/zerocopy/zerocopy-derive/src/derive/try_from_bytes.rs @@ -443,6 +443,13 @@ pub(crate) fn derive_is_bit_valid( } }) } + +// Concrete consumer-side Kani proofs for representative expansions from this +// entry point live beside their derive invocations in +// `zerocopy/src/proofs/try_from_bytes_derive.rs`. They verify the emitted +// implementations together with the consuming crate's validation path, not +// this generator universally; see the generated-output exception in +// `zerocopy/agent_docs/validation.md`. pub(crate) fn derive_try_from_bytes(ctx: &Ctx, top_level: Trait) -> Result { match &ctx.ast.data { Data::Struct(strct) => derive_try_from_bytes_struct(ctx, strct, top_level), @@ -450,6 +457,7 @@ pub(crate) fn derive_try_from_bytes(ctx: &Ctx, top_level: Trait) -> Result Ok(derive_try_from_bytes_union(ctx, unn, top_level)), } } + fn derive_has_field_struct_union(ctx: &Ctx, data: &dyn DataExt) -> TokenStream { let fields = ctx.ast.data.fields(); if fields.is_empty() {