From 0ccf1e2a24b28a2ea673d6b0f382bfdeed88ab74 Mon Sep 17 00:00:00 2001 From: Joshua Liebow-Feeser Date: Tue, 28 Nov 2023 17:43:16 +0000 Subject: [PATCH] [proofs] Initial commit Add axioms and lemmas which are useful in proving the soundness of some trait impls. Makes progress on #429 --- src/lib.rs | 50 +++++++++-------------- src/proof_utils.rs | 100 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 120 insertions(+), 30 deletions(-) create mode 100644 src/proof_utils.rs diff --git a/src/lib.rs b/src/lib.rs index 9c4a1e91aed..ba76443d08a 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -243,6 +243,7 @@ mod macros; pub mod byteorder; #[doc(hidden)] pub mod macro_util; +mod proof_utils; mod util; // TODO(#252): If we make this pub, come up with a better name. mod wrappers; @@ -2303,17 +2304,18 @@ safety_comment! { } safety_comment! { /// SAFETY: - /// `Wrapping` is guaranteed by its docs [1] to have the same layout as - /// `T`. Also, `Wrapping` is `#[repr(transparent)]`, and has a single - /// field, which is `pub`. Per the reference [2], this means that the - /// `#[repr(transparent)]` attribute is "considered part of the public ABI". + /// `Wrapping` is `#[repr(transparent)]` and has a single `T` field, + /// which is `pub`. [1] Per axiom-repr-transparent-layout-validity, we may + /// take this to imply that `Wrapping: transparent-layout-validity(T)`. + /// This is bolstered by [2]. Per lemma-repr-transparent-zerocopy-traits, if + /// `T` satisfies the safety preconditions of `FromZeroes`, `FromBytes`, + /// `AsBytes`, or `Unaligned`, then `Wrapping` does too (respectively). /// - /// TODO(#429): Add quotes from documentation. + /// [1] https://doc.rust-lang.org/core/num/struct.Wrapping.html /// - /// [1] TODO(https://doc.rust-lang.org/nightly/core/num/struct.Wrapping.html#layout-1): - /// Reference this documentation once it's available on stable. + /// [2] Per https://doc.rust-lang.org/nightly/core/num/struct.Wrapping.html: /// - /// [2] https://doc.rust-lang.org/nomicon/other-reprs.html#reprtransparent + /// `Wrapping` is guaranteed to have the same layout and ABI as `T`. unsafe_impl!(T: FromZeroes => FromZeroes for Wrapping); unsafe_impl!(T: FromBytes => FromBytes for Wrapping); unsafe_impl!(T: AsBytes => AsBytes for Wrapping); @@ -2347,31 +2349,19 @@ safety_comment! { } safety_comment! { /// SAFETY: - /// `ManuallyDrop` has the same layout and bit validity as `T` [1], and - /// accessing the inner value is safe (meaning that it's unsound to leave - /// the inner value uninitialized while exposing the `ManuallyDrop` to safe - /// code). - /// - `FromZeroes`, `FromBytes`: Since it has the same layout as `T`, any - /// valid `T` is a valid `ManuallyDrop`. If `T: FromZeroes`, a sequence - /// of zero bytes is a valid `T`, and thus a valid `ManuallyDrop`. If - /// `T: FromBytes`, any sequence of bytes is a valid `T`, and thus a valid - /// `ManuallyDrop`. - /// - `AsBytes`: Since it has the same layout as `T`, and since it's unsound - /// to let safe code access a `ManuallyDrop` whose inner value is - /// uninitialized, safe code can only ever access a `ManuallyDrop` whose - /// contents are a valid `T`. Since `T: AsBytes`, this means that safe - /// code can only ever access a `ManuallyDrop` with all initialized bytes. - /// - `Unaligned`: `ManuallyDrop` has the same layout (and thus alignment) - /// as `T`, and `T: Unaligned` guarantees that that alignment is 1. - /// - /// `ManuallyDrop` is guaranteed to have the same layout and bit - /// validity as `T` + /// `ManuallyDrop` has the same layout and bit validity as `T` [1]. Per + /// axiom-transparent-layout-validity, we may use this to assume that + /// `ManuallyDrop: transparent-layout-validity(T)`. Per + /// lemma-repr-transparent-zerocopy-traits, if `T` satisfies the safety + /// preconditions of `FromZeroes`, `FromBytes`, `AsBytes`, or `Unaligned`, + /// then `ManuallyDrop` does too (respectively). /// /// [1] Per https://doc.rust-lang.org/nightly/core/mem/struct.ManuallyDrop.html: /// - /// TODO(#429): - /// - Add quotes from docs. - /// - Once [1] (added in + /// `ManuallyDrop` is guaranteed to have the same layout and bit + /// validity as `T`. + /// + /// TODO(#429): Once [1] (added in /// https://github.com/rust-lang/rust/pull/115522) is available on stable, /// quote the stable docs instead of the nightly docs. unsafe_impl!(T: ?Sized + FromZeroes => FromZeroes for ManuallyDrop); diff --git a/src/proof_utils.rs b/src/proof_utils.rs new file mode 100644 index 00000000000..b5b0018aa22 --- /dev/null +++ b/src/proof_utils.rs @@ -0,0 +1,100 @@ +// Copyright 2023 The Fuchsia Authors +// +// Licensed under a BSD-style 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. + +//! This module exists to hold this doc comment, which provides lemmas which can +//! be used in soundness proofs. +//! +//! # Definitions +//! +//! ## transparent-layout-validity +//! +//! A type, `T`, has the property `transparent-layout-validity(U)` if the +//! following all hold: +//! - `T` and `U` have the same alignment +//! - For all `t: *const T`, `let u = t as *const U` is valid and +//! `size_of_val_raw(t) == size_of_val_raw(u)`. +//! - For all `u: *const U`, `let t = *const T` is valid and `size_of_val_raw(u) +//! == size_of_val_raw(t)`. +//! - For all `(t, u): (*const T, *const U)` where `size_of_val_raw(t) == +//! size_of_val_raw(u)`: +//! - `t` and `u` refer to `UnsafeCell`s at the same byte ranges. +//! - If `*t` contains a valid `T`, that implies that `*u` contains a valid +//! `U`. +//! - If `*u` contains a valid `U`, that implies that `*t` contains a valid +//! `T`. +//! +//! # Axioms +//! +//! These are statements which are not technically logically bulletproof, but +//! capture the way that language is used in practice in the Rust Reference and +//! standard library documentation. +//! +//! ## axiom-transparent-layout-validity +//! +//! Given types `T` and `U`, the phrase "`T` is guaranteed to have the same +//! layout and bit validity as `U`" is taken to imply that `T` has the property +//! `transparent-layout-validity(U)`. +//! +//! The term "layout" is used in Rust documentation to refer to a type's size +//! and alignment and the sizes, alignments, and byte offsets of each of the +//! type's fields. In practice, phrases like the above are only ever used in +//! contexts where the following additional properties also hold: +//! - `T` and `U` have the same vtable kinds. `T`'s and `U`'s pointer metadata +//! is such that raw pointer casts preserve size and field placement. +//! - `T` and `U` have `UnsafeCell`s at the same byte ranges. +//! +//! ## axiom-repr-transparent-layout-validity +//! +//! Given types `T` and `U`, if `T` is a `#[repr(transparent)]` struct with a +//! `pub` field of type `U`, and `T` does not contain any other fields, then +//! `T` has the property `transparent-layout-validity(U)`. +//! +//! Per the [Rust Reference][repr-transparent]: +//! +//! > \[`repr(transparent)`\] is only considered part of the public ABI of a +//! > type if either its single field is `pub`, or if its layout is documented +//! > in prose. +//! +//! [repr-transparent]: https://doc.rust-lang.org/nomicon/other-reprs.html#reprtransparent +//! +//! # Lemmas +//! +//! ## lemma-repr-transparent-zerocopy-traits +//! +//! - Lemma: Given types `T` and `U` where `T` is +//! `transparent-layout-validity(U)`, for each `Trait` in `FromZeroes`, +//! `FromBytes`, `AsBytes`, and `Unaligned`, if `U` satisfies the safety +//! preconditions of `Trait`, then `T` does as well. +//! - Proof: +//! - `FromZeroes`, `FromBytes`, and `AsBytes` all require that a type not +//! contain any `UnsafeCell`s. `T: transparent-layout-validity(U)` +//! guarantees that, for all pairs of `t: *const T` and `u: *const U` of +//! equal size, `t` and `u` refer to `UnsafeCell`s at the same byte ranges. +//! If `U: FromZeroes`, `U: FromBytes`, or `U: AsBytes`, no instance of `U` +//! contains `UnsafeCell`s at any byte ranges. Thus, no instance of `T` +//! contains `UnsafeCell`s at any byte ranges. +//! - `U: FromZeroes` additionally requires that, given `u: *const U`, it is +//! sound to initialize `*u` to contain all zero bytes. Since, for all `t: +//! *const T` and `u: *const U` of equal size, `*t` and `*u` have equal bit +//! validity, then it must also be the case that, given `t: *const T`, it is +//! sound to initialize `*t` to contain all zero bytes. +//! - `U: FromBytes` additionally requires that, given `u: *const U`, it is +//! sound to initialize `*u` to contain any sequence of `u8`s. Since, for +//! all `t: *const T` and `u: *const U` of equal size, `*t` and `*u` have +//! equal bit validity, then it must also be the case that, given `t: *const +//! T`, it is sound to initialize `*t` to contain any sequence of `u8`s. +//! - `U: AsBytes` additionally requires that, given `u: &U`, it is sound to +//! treat `t` as an immutable `[u8]` of length `size_of_val(u)`. This is +//! equivalent to saying that no instance of `U` can contain bytes which are +//! invalid for `u8`. Since, for all `t: *const T` and `u: *const U` of +//! equal size, `*t` and `*u` have equal bit validity, then it must also be +//! the case that no instance of `T` can contain bytes which are invalid for +//! `u8`. +//! - `U: Unaligned` requires that `U`'s alignment is 1. `T: +//! transparent-layout-validity(U)` guarantees that `T`'s alignment is equal +//! to `U`'s, and is thus also 1.