Skip to content

Commit

Permalink
[proofs] Initial commit
Browse files Browse the repository at this point in the history 
Add axioms and lemmas which are useful in proving the soundness of some
trait impls.

Makes progress on #429
  • Loading branch information
@joshlf
joshlf committed Nov 28, 2023
1 parent 6f773ef commit 55cdd4d
Show file tree
Hide file tree
Showing 3 changed files with 184 additions and 81 deletions.
92 changes: 29 additions & 63 deletions src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -2501,47 +2502,24 @@ safety_comment! {
}
safety_comment! {
/// SAFETY:
/// `Wrapping<T>` is guaranteed by its docs [1] to have the same layout and
/// bit validity 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".
///
/// - `TryFromBytes`: The safety requirements for `unsafe_impl!` with an
/// `is_bit_valid` closure:
/// - Given `t: *mut Wrapping<T>` and `let r = *mut T`, `r` refers to an
/// object of the same size as that referred to by `t`. This is true
/// because `Wrapping<T>` and `T` have the same layout
/// - The alignment of `Wrapping<T>` is equal to the alignment of `T`.
/// - The impl must only return `true` for its argument if the original
/// `Ptr<Wrapping<T>>` refers to a valid `Wrapping<T>`. Since
/// `Wrapping<T>` has the same bit validity as `T`, and since our impl
/// just calls `T::is_bit_valid`, our impl returns `true` exactly when
/// its argument contains a valid `Wrapping<T>`.
/// - `FromBytes`: Since `Wrapping<T>` has the same bit validity as `T`, if
/// `T: FromBytes`, then all initialized byte sequences are valid
/// instances of `Wrapping<T>`. Similarly, if `T: FromBytes`, then
/// `Wrapping<T>` doesn't contain any `UnsafeCell`s. Thus, `impl FromBytes
/// for Wrapping<T> where T: FromBytes` is a sound impl.
/// - `AsBytes`: Since `Wrapping<T>` has the same bit validity as `T`, if
/// `T: AsBytes`, then all valid instances of `Wrapping<T>` have all of
/// their bytes initialized. Similarly, if `T: AsBytes`, then
/// `Wrapping<T>` doesn't contain any `UnsafeCell`s. Thus, `impl AsBytes
/// for Wrapping<T> where T: AsBytes` is a valid impl.
/// - `Unaligned`: Since `Wrapping<T>` has the same layout as `T`,
/// `Wrapping<T>` has alignment 1 exactly when `T` does.
///
/// [1] Per https://doc.rust-lang.org/core/num/struct.NonZeroU16.html:
///
/// `NonZeroU16` is guaranteed to have the same layout and bit validity as
/// `u16` with the exception that `0` is not a valid instance.
///
/// TODO(#429): Add quotes from documentation.
///
/// [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] https://doc.rust-lang.org/nomicon/other-reprs.html#reprtransparent
/// `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].
/// - `TryFromBytes`: Since the closure takes `Ptr<T>`, `Wrapping<T>:
/// transparent-layout-validity(T)` satisfies `unsafe_impl!`'s safety
/// preconditions.
/// - `FromZeroes`, `FromBytes`, `AsBytes`, `Unaligned`: Per
/// lemma-repr-transparent-zerocopy-traits, since `Wrapping<T>:
/// transparent-layout-validity(T)`, if `T` satisfies the safety
/// preconditions of `FromZeroes`, `FromBytes`, `AsBytes`, or `Unaligned`,
/// then `Wrapping<T>` does too (respectively).
///
/// [1] https://doc.rust-lang.org/core/num/struct.Wrapping.html
///
/// [2] Per https://doc.rust-lang.org/nightly/core/num/struct.Wrapping.html:
///
/// `Wrapping<T>` is guaranteed to have the same layout and ABI as `T`.
unsafe_impl!(T: TryFromBytes => TryFromBytes for Wrapping<T>; |candidate: Ptr<T>| {
// SAFETY:
// - Since `T` and `Wrapping<T>` have the same layout and bit validity
Expand Down Expand Up @@ -2589,31 +2567,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>);
Expand Down
56 changes: 38 additions & 18 deletions src/macros.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,18 +44,22 @@ macro_rules! safety_comment {
/// be the case that any initialized sequence of bytes constitutes a valid
/// instance of `$ty`.
/// - If an `is_bit_valid` impl is provided, then:
/// - Regardless of whether the provided closure takes a `Ptr<$repr>` or
/// `&$repr` argument, it must be the case that, given `t: *mut $ty` and
/// `let r = t as *mut $repr`, `r` refers to an object of equal or lesser
/// size than the object referred to by `t`.
/// - If the provided closure takes a `&$repr` argument, then given a `Ptr<'a,
/// $ty>` which satisfies the preconditions of
/// - If `$ty: !transparent-layout-validity($repr)`, all of the following must
/// hold:
/// - Given `t: *mut $ty` and `let r = t as *mut $repr`, `r` refers to an
/// object of equal or lesser size than the object referred to by `t`.
/// - The alignment of `$repr` is less than or equal to the alignment of
/// `$ty`.
/// - If the provided closure takes a `&$repr` argument, then given a
/// `Ptr<'a, $ty>` which satisfies the preconditions of
/// `TryFromBytes::<$ty>::is_bit_valid`, it must be guaranteed that the
/// memory referenced by that `Ptr` always contains a valid `$repr`.
/// - The alignment of `$repr` is less than or equal to the alignment of
/// `$ty`.
/// - The impl of `is_bit_valid` must only return `true` for its argument
/// `Ptr<$repr>` if the original `Ptr<$ty>` refers to a valid `$ty`.
/// - At least one of the following must hold:
/// - The impl of `is_bit_valid` must only return `true` for its argument
/// `Ptr<$repr>` if the original `Ptr<$ty>` refers to a valid `$ty`.
/// - `$ty: transparent-layout-validity($repr)`, the provided closure takes
/// a `Ptr<'a, $repr>`, and the body of the closure is equal to
/// `TryFromBytes::<$repr>::is_bit_valid`.
macro_rules! unsafe_impl {
// Implement `$trait` for `$ty` with no bounds.
($(#[$attr:meta])* $ty:ty: $trait:ident $(; |$candidate:ident: &$repr:ty| $is_bit_valid:expr)?) => {
Expand Down Expand Up @@ -133,15 +137,20 @@ macro_rules! unsafe_impl {
};

(@method TryFromBytes ; |$candidate:ident: &$repr:ty| $is_bit_valid:expr) => {
// SAFETY: The caller has promised that this implementation is correct.
#[inline]
unsafe fn is_bit_valid(candidate: Ptr<'_, Self>) -> bool {
// SAFETY:
// - The argument to `cast_unsized` is `|p| p as *mut _` as required
// by that method's safety precondition.
// - The caller has promised that the cast results in an object of
// equal or lesser size.
// - The caller has promised that `$repr`'s alignment is less than
// or equal to `Self`'s alignment.
// - Either the caller has promised that the cast results in an
// object of equal or lesser size, or `$ty:
// transparent-layout-validity($repr)`, which guarantees that the
// cast results in an object of equal size.
// - Either the caller has promised that `$repr`'s alignment is less
// than or equal to `Self`'s alignment, or `$ty:
// transparent-layout-validity($repr)`, which guarantees that
// `$repr` and `$ty` have the same alignment.
#[allow(clippy::as_conversions)]
let candidate = unsafe { candidate.cast_unsized::<$repr, _>(|p| p as *mut _) };
// SAFETY:
Expand All @@ -160,15 +169,26 @@ macro_rules! unsafe_impl {
}
};
(@method TryFromBytes ; |$candidate:ident: Ptr<$repr:ty>| $is_bit_valid:expr) => {
// SAFETY: At least one of the following holds:
// - The caller has promised that this implementation is correct.
// - `$ty: transparent-layout-validity($repr)` and the body is equal to
// `TryFromBytes::<$repr>::is_bit_valid`. In this case, the bit
// validity of `$ty` and `$repr` are equivalent, and so
// `TryFromBytes::<$repr>::is_bit_valid` is a valid implementation of
// `TryFromBytes::<$ty>::is_bit_valid`.
#[inline]
unsafe fn is_bit_valid(candidate: Ptr<'_, Self>) -> bool {
// SAFETY:
// - The argument to `cast_unsized` is `|p| p as *mut _` as required
// by that method's safety precondition.
// - The caller has promised that the cast results in an object of
// equal or lesser size.
// - The caller has promised that `$repr`'s alignment is less than
// or equal to `Self`'s alignment.
// - Either the caller has promised that the cast results in an
// object of equal or lesser size, or `$ty:
// transparent-layout-validity($repr)`, which guarantees that the
// cast results in an object of equal size.
// - Either the caller has promised that `$repr`'s alignment is less
// than or equal to `Self`'s alignment, or `$ty:
// transparent-layout-validity($repr)`, which guarantees that
// `$repr` and `$ty` have the same alignment.
#[allow(clippy::as_conversions)]
let $candidate = unsafe { candidate.cast_unsized::<$repr, _>(|p| p as *mut _) };
$is_bit_valid
Expand Down
117 changes: 117 additions & 0 deletions src/proof_utils.rs
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,117 @@
// 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.
//!
//! ## lemma-transparent-layout-validity-is-bit-valid
//!
//! - Lemma: Given `T` and `U` where `T` is `transparent-layout-validity(U)`,
//! given `t: Ptr<'a, T>` which satisfies the safety preconditions of
//! `TryFromBytes::<T>::is_bit_valid`, and given `u: Ptr<'a, U>` which
//! addresses the same range as `t`, `u` satisfies the safety preconditions of
//! `TryFromBytes::<U>::is_bit_valid`.
//! - Proof: TODO
//!
//! WARNING: This might not actually be sound! In particular, `T:
//! transparent-layout-validity(U)` doesn't guarantee that, given an enum
//! discriminant with a particular value, the subset of values of `T` which are
//! valid for that discriminant is the same as the subset of values of `U` which
//! are valid for that discriminant. As a result, it may be possible to pass a
//! `Ptr<T>` which has uninitialized bytes which are not problematic for `T` but
//! which are problematic for `U`.

0 comments on commit 55cdd4d

Please sign in to comment.