[proofs] Initial commit

Add axioms and lemmas which are useful in proving the soundness of some
trait impls.

Makes progress on #429

Author: joshlf

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<T>` is guaranteed by its docs [1] to have the same layout as
-    /// `T`. Also, `Wrapping<T>` 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<T>` 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<T>: 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<T>` 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<T>` is guaranteed to have the same layout and ABI as `T`.
     unsafe_impl!(T: FromZeroes => FromZeroes for Wrapping<T>);
     unsafe_impl!(T: FromBytes => FromBytes for Wrapping<T>);
     unsafe_impl!(T: AsBytes => AsBytes for Wrapping<T>);
@@ -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<T>`. If `T: FromZeroes`, a sequence
-    ///   of zero bytes is a valid `T`, and thus a valid `ManuallyDrop<T>`. If
-    ///   `T: FromBytes`, any sequence of bytes is a valid `T`, and thus a valid
-    ///   `ManuallyDrop<T>`.
-    /// - `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<T>` is guaranteed to have the same layout and bit
-    ///   validity as `T`
+    /// `ManuallyDrop<T>` has the same layout and bit validity as `T` [1]. Per
+    /// axiom-transparent-layout-validity, we may use this to assume that
+    /// `ManuallyDrop<T>: transparent-layout-validity(T)`. Per
+    /// lemma-repr-transparent-zerocopy-traits, if `T` satisfies the safety
+    /// preconditions of `FromZeroes`, `FromBytes`, `AsBytes`, or `Unaligned`,
+    /// then `ManuallyDrop<T>` 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<T>` 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<T>);

src/proof_utils.rs

@@ -0,0 +1,100 @@
+// Copyright 2023 The Fuchsia Authors
+//
+// Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, 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.