Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[proofs] Initial commit #652

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
+184 −81
Open

[proofs] Initial commit #652

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
92 changes: 29 additions & 63 deletions src/lib.rs
View file
Open in desktop
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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should axiom-repr-transparent-layout-validity perhaps be a intradoc link? It'd give us a modest defense against proof rot.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oooh good idea. I'll also need to make sure that our safety doc comments are actually being parsed by rustdoc.

/// 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
Open in desktop
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
Open in desktop
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`.
Comment on lines +14 to +29
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Concretely:

/// 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`.
#[allow(unsused)] // This only exists as an anchor for intradoc links.
const TRANSPARENT_LAYOUT_VALIDIDTY: () = ();

//!
//! # 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
jswrenn marked this conversation as resolved.
Show resolved Hide resolved
//! `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`.