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 57c8fd9 commit 0ccf1e2
Show file tree
Hide file tree
Showing 2 changed files with 120 additions and 30 deletions.
50 changes: 20 additions & 30 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 @@ -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>);
Expand Down Expand Up @@ -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>);
Expand Down
100 changes: 100 additions & 0 deletions src/proof_utils.rs
View file
Original file line number Diff line number Diff line change
@@ -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.

0 comments on commit 0ccf1e2

Please sign in to comment.