Skip to content

Commit 55cdd4d

Browse files
joshlfjoshlf
committed
[proofs] Initial commit
Add axioms and lemmas which are useful in proving the soundness of some trait impls. Makes progress on #429
1 parent 6f773ef commit 55cdd4d

File tree

3 files changed

+184
-81
lines changed

3 files changed

+184
-81
lines changed

‎src/lib.rs

Lines changed: 29 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -243,6 +243,7 @@ mod macros;
243243
pub mod byteorder;
244244
#[doc(hidden)]
245245
pub mod macro_util;
246+
mod proof_utils;
246247
mod util;
247248
// TODO(#252): If we make this pub, come up with a better name.
248249
mod wrappers;
@@ -2501,47 +2502,24 @@ safety_comment! {
25012502
}
25022503
safety_comment! {
25032504
/// SAFETY:
2504-
/// `Wrapping<T>` is guaranteed by its docs [1] to have the same layout and
2505-
/// bit validity as `T`. Also, `Wrapping<T>` is `#[repr(transparent)]`, and
2506-
/// has a single field, which is `pub`. Per the reference [2], this means
2507-
/// that the `#[repr(transparent)]` attribute is "considered part of the
2508-
/// public ABI".
2509-
///
2510-
/// - `TryFromBytes`: The safety requirements for `unsafe_impl!` with an
2511-
/// `is_bit_valid` closure:
2512-
/// - Given `t: *mut Wrapping<T>` and `let r = *mut T`, `r` refers to an
2513-
/// object of the same size as that referred to by `t`. This is true
2514-
/// because `Wrapping<T>` and `T` have the same layout
2515-
/// - The alignment of `Wrapping<T>` is equal to the alignment of `T`.
2516-
/// - The impl must only return `true` for its argument if the original
2517-
/// `Ptr<Wrapping<T>>` refers to a valid `Wrapping<T>`. Since
2518-
/// `Wrapping<T>` has the same bit validity as `T`, and since our impl
2519-
/// just calls `T::is_bit_valid`, our impl returns `true` exactly when
2520-
/// its argument contains a valid `Wrapping<T>`.
2521-
/// - `FromBytes`: Since `Wrapping<T>` has the same bit validity as `T`, if
2522-
/// `T: FromBytes`, then all initialized byte sequences are valid
2523-
/// instances of `Wrapping<T>`. Similarly, if `T: FromBytes`, then
2524-
/// `Wrapping<T>` doesn't contain any `UnsafeCell`s. Thus, `impl FromBytes
2525-
/// for Wrapping<T> where T: FromBytes` is a sound impl.
2526-
/// - `AsBytes`: Since `Wrapping<T>` has the same bit validity as `T`, if
2527-
/// `T: AsBytes`, then all valid instances of `Wrapping<T>` have all of
2528-
/// their bytes initialized. Similarly, if `T: AsBytes`, then
2529-
/// `Wrapping<T>` doesn't contain any `UnsafeCell`s. Thus, `impl AsBytes
2530-
/// for Wrapping<T> where T: AsBytes` is a valid impl.
2531-
/// - `Unaligned`: Since `Wrapping<T>` has the same layout as `T`,
2532-
/// `Wrapping<T>` has alignment 1 exactly when `T` does.
2533-
///
2534-
/// [1] Per https://doc.rust-lang.org/core/num/struct.NonZeroU16.html:
2535-
///
2536-
/// `NonZeroU16` is guaranteed to have the same layout and bit validity as
2537-
/// `u16` with the exception that `0` is not a valid instance.
2538-
///
2539-
/// TODO(#429): Add quotes from documentation.
2540-
///
2541-
/// [1] TODO(https://doc.rust-lang.org/nightly/core/num/struct.Wrapping.html#layout-1):
2542-
/// Reference this documentation once it's available on stable.
2543-
///
2544-
/// [2] https://doc.rust-lang.org/nomicon/other-reprs.html#reprtransparent
2505+
/// `Wrapping<T>` is `#[repr(transparent)]` and has a single `T` field,
2506+
/// which is `pub`. [1] Per axiom-repr-transparent-layout-validity, we may
2507+
/// take this to imply that `Wrapping<T>: transparent-layout-validity(T)`.
2508+
/// This is bolstered by [2].
2509+
/// - `TryFromBytes`: Since the closure takes `Ptr<T>`, `Wrapping<T>:
2510+
/// transparent-layout-validity(T)` satisfies `unsafe_impl!`'s safety
2511+
/// preconditions.
2512+
/// - `FromZeroes`, `FromBytes`, `AsBytes`, `Unaligned`: Per
2513+
/// lemma-repr-transparent-zerocopy-traits, since `Wrapping<T>:
2514+
/// transparent-layout-validity(T)`, if `T` satisfies the safety
2515+
/// preconditions of `FromZeroes`, `FromBytes`, `AsBytes`, or `Unaligned`,
2516+
/// then `Wrapping<T>` does too (respectively).
2517+
///
2518+
/// [1] https://doc.rust-lang.org/core/num/struct.Wrapping.html
2519+
///
2520+
/// [2] Per https://doc.rust-lang.org/nightly/core/num/struct.Wrapping.html:
2521+
///
2522+
/// `Wrapping<T>` is guaranteed to have the same layout and ABI as `T`.
25452523
unsafe_impl!(T: TryFromBytes => TryFromBytes for Wrapping<T>; |candidate: Ptr<T>| {
25462524
// SAFETY:
25472525
// - Since `T` and `Wrapping<T>` have the same layout and bit validity
@@ -2589,31 +2567,19 @@ safety_comment! {
25892567
}
25902568
safety_comment! {
25912569
/// SAFETY:
2592-
/// `ManuallyDrop` has the same layout and bit validity as `T` [1], and
2593-
/// accessing the inner value is safe (meaning that it's unsound to leave
2594-
/// the inner value uninitialized while exposing the `ManuallyDrop` to safe
2595-
/// code).
2596-
/// - `FromZeroes`, `FromBytes`: Since it has the same layout as `T`, any
2597-
/// valid `T` is a valid `ManuallyDrop<T>`. If `T: FromZeroes`, a sequence
2598-
/// of zero bytes is a valid `T`, and thus a valid `ManuallyDrop<T>`. If
2599-
/// `T: FromBytes`, any sequence of bytes is a valid `T`, and thus a valid
2600-
/// `ManuallyDrop<T>`.
2601-
/// - `AsBytes`: Since it has the same layout as `T`, and since it's unsound
2602-
/// to let safe code access a `ManuallyDrop` whose inner value is
2603-
/// uninitialized, safe code can only ever access a `ManuallyDrop` whose
2604-
/// contents are a valid `T`. Since `T: AsBytes`, this means that safe
2605-
/// code can only ever access a `ManuallyDrop` with all initialized bytes.
2606-
/// - `Unaligned`: `ManuallyDrop` has the same layout (and thus alignment)
2607-
/// as `T`, and `T: Unaligned` guarantees that that alignment is 1.
2608-
///
2609-
/// `ManuallyDrop<T>` is guaranteed to have the same layout and bit
2610-
/// validity as `T`
2570+
/// `ManuallyDrop<T>` has the same layout and bit validity as `T` [1]. Per
2571+
/// axiom-transparent-layout-validity, we may use this to assume that
2572+
/// `ManuallyDrop<T>: transparent-layout-validity(T)`. Per
2573+
/// lemma-repr-transparent-zerocopy-traits, if `T` satisfies the safety
2574+
/// preconditions of `FromZeroes`, `FromBytes`, `AsBytes`, or `Unaligned`,
2575+
/// then `ManuallyDrop<T>` does too (respectively).
26112576
///
26122577
/// [1] Per https://doc.rust-lang.org/nightly/core/mem/struct.ManuallyDrop.html:
26132578
///
2614-
/// TODO(#429):
2615-
/// - Add quotes from docs.
2616-
/// - Once [1] (added in
2579+
/// `ManuallyDrop<T>` is guaranteed to have the same layout and bit
2580+
/// validity as `T`.
2581+
///
2582+
/// TODO(#429): Once [1] (added in
26172583
/// https://github.com/rust-lang/rust/pull/115522) is available on stable,
26182584
/// quote the stable docs instead of the nightly docs.
26192585
unsafe_impl!(T: ?Sized + FromZeroes => FromZeroes for ManuallyDrop<T>);

‎src/macros.rs

Lines changed: 38 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -44,18 +44,22 @@ macro_rules! safety_comment {
4444
/// be the case that any initialized sequence of bytes constitutes a valid
4545
/// instance of `$ty`.
4646
/// - If an `is_bit_valid` impl is provided, then:
47-
/// - Regardless of whether the provided closure takes a `Ptr<$repr>` or
48-
/// `&$repr` argument, it must be the case that, given `t: *mut $ty` and
49-
/// `let r = t as *mut $repr`, `r` refers to an object of equal or lesser
50-
/// size than the object referred to by `t`.
51-
/// - If the provided closure takes a `&$repr` argument, then given a `Ptr<'a,
52-
/// $ty>` which satisfies the preconditions of
47+
/// - If `$ty: !transparent-layout-validity($repr)`, all of the following must
48+
/// hold:
49+
/// - Given `t: *mut $ty` and `let r = t as *mut $repr`, `r` refers to an
50+
/// object of equal or lesser size than the object referred to by `t`.
51+
/// - The alignment of `$repr` is less than or equal to the alignment of
52+
/// `$ty`.
53+
/// - If the provided closure takes a `&$repr` argument, then given a
54+
/// `Ptr<'a, $ty>` which satisfies the preconditions of
5355
/// `TryFromBytes::<$ty>::is_bit_valid`, it must be guaranteed that the
5456
/// memory referenced by that `Ptr` always contains a valid `$repr`.
55-
/// - The alignment of `$repr` is less than or equal to the alignment of
56-
/// `$ty`.
57-
/// - The impl of `is_bit_valid` must only return `true` for its argument
58-
/// `Ptr<$repr>` if the original `Ptr<$ty>` refers to a valid `$ty`.
57+
/// - At least one of the following must hold:
58+
/// - The impl of `is_bit_valid` must only return `true` for its argument
59+
/// `Ptr<$repr>` if the original `Ptr<$ty>` refers to a valid `$ty`.
60+
/// - `$ty: transparent-layout-validity($repr)`, the provided closure takes
61+
/// a `Ptr<'a, $repr>`, and the body of the closure is equal to
62+
/// `TryFromBytes::<$repr>::is_bit_valid`.
5963
macro_rules! unsafe_impl {
6064
// Implement `$trait` for `$ty` with no bounds.
6165
($(#[$attr:meta])* $ty:ty: $trait:ident $(; |$candidate:ident: &$repr:ty| $is_bit_valid:expr)?) => {
@@ -133,15 +137,20 @@ macro_rules! unsafe_impl {
133137
};
134138

135139
(@method TryFromBytes ; |$candidate:ident: &$repr:ty| $is_bit_valid:expr) => {
140+
// SAFETY: The caller has promised that this implementation is correct.
136141
#[inline]
137142
unsafe fn is_bit_valid(candidate: Ptr<'_, Self>) -> bool {
138143
// SAFETY:
139144
// - The argument to `cast_unsized` is `|p| p as *mut _` as required
140145
// by that method's safety precondition.
141-
// - The caller has promised that the cast results in an object of
142-
// equal or lesser size.
143-
// - The caller has promised that `$repr`'s alignment is less than
144-
// or equal to `Self`'s alignment.
146+
// - Either the caller has promised that the cast results in an
147+
// object of equal or lesser size, or `$ty:
148+
// transparent-layout-validity($repr)`, which guarantees that the
149+
// cast results in an object of equal size.
150+
// - Either the caller has promised that `$repr`'s alignment is less
151+
// than or equal to `Self`'s alignment, or `$ty:
152+
// transparent-layout-validity($repr)`, which guarantees that
153+
// `$repr` and `$ty` have the same alignment.
145154
#[allow(clippy::as_conversions)]
146155
let candidate = unsafe { candidate.cast_unsized::<$repr, _>(|p| p as *mut _) };
147156
// SAFETY:
@@ -160,15 +169,26 @@ macro_rules! unsafe_impl {
160169
}
161170
};
162171
(@method TryFromBytes ; |$candidate:ident: Ptr<$repr:ty>| $is_bit_valid:expr) => {
172+
// SAFETY: At least one of the following holds:
173+
// - The caller has promised that this implementation is correct.
174+
// - `$ty: transparent-layout-validity($repr)` and the body is equal to
175+
// `TryFromBytes::<$repr>::is_bit_valid`. In this case, the bit
176+
// validity of `$ty` and `$repr` are equivalent, and so
177+
// `TryFromBytes::<$repr>::is_bit_valid` is a valid implementation of
178+
// `TryFromBytes::<$ty>::is_bit_valid`.
163179
#[inline]
164180
unsafe fn is_bit_valid(candidate: Ptr<'_, Self>) -> bool {
165181
// SAFETY:
166182
// - The argument to `cast_unsized` is `|p| p as *mut _` as required
167183
// by that method's safety precondition.
168-
// - The caller has promised that the cast results in an object of
169-
// equal or lesser size.
170-
// - The caller has promised that `$repr`'s alignment is less than
171-
// or equal to `Self`'s alignment.
184+
// - Either the caller has promised that the cast results in an
185+
// object of equal or lesser size, or `$ty:
186+
// transparent-layout-validity($repr)`, which guarantees that the
187+
// cast results in an object of equal size.
188+
// - Either the caller has promised that `$repr`'s alignment is less
189+
// than or equal to `Self`'s alignment, or `$ty:
190+
// transparent-layout-validity($repr)`, which guarantees that
191+
// `$repr` and `$ty` have the same alignment.
172192
#[allow(clippy::as_conversions)]
173193
let $candidate = unsafe { candidate.cast_unsized::<$repr, _>(|p| p as *mut _) };
174194
$is_bit_valid

‎src/proof_utils.rs

Lines changed: 117 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,117 @@
1+
// Copyright 2023 The Fuchsia Authors
2+
//
3+
// Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
4+
// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
5+
// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
6+
// This file may not be copied, modified, or distributed except according to
7+
// those terms.
8+
9+
//! This module exists to hold this doc comment, which provides lemmas which can
10+
//! be used in soundness proofs.
11+
//!
12+
//! # Definitions
13+
//!
14+
//! ## transparent-layout-validity
15+
//!
16+
//! A type, `T`, has the property `transparent-layout-validity(U)` if the
17+
//! following all hold:
18+
//! - `T` and `U` have the same alignment
19+
//! - For all `t: *const T`, `let u = t as *const U` is valid and
20+
//! `size_of_val_raw(t) == size_of_val_raw(u)`.
21+
//! - For all `u: *const U`, `let t = *const T` is valid and `size_of_val_raw(u)
22+
//! == size_of_val_raw(t)`.
23+
//! - For all `(t, u): (*const T, *const U)` where `size_of_val_raw(t) ==
24+
//! size_of_val_raw(u)`:
25+
//! - `t` and `u` refer to `UnsafeCell`s at the same byte ranges.
26+
//! - If `*t` contains a valid `T`, that implies that `*u` contains a valid
27+
//! `U`.
28+
//! - If `*u` contains a valid `U`, that implies that `*t` contains a valid
29+
//! `T`.
30+
//!
31+
//! # Axioms
32+
//!
33+
//! These are statements which are not technically logically bulletproof, but
34+
//! capture the way that language is used in practice in the Rust Reference and
35+
//! standard library documentation.
36+
//!
37+
//! ## axiom-transparent-layout-validity
38+
//!
39+
//! Given types `T` and `U`, the phrase "`T` is guaranteed to have the same
40+
//! layout and bit validity as `U`" is taken to imply that `T` has the property
41+
//! `transparent-layout-validity(U)`.
42+
//!
43+
//! The term "layout" is used in Rust documentation to refer to a type's size
44+
//! and alignment and the sizes, alignments, and byte offsets of each of the
45+
//! type's fields. In practice, phrases like the above are only ever used in
46+
//! contexts where the following additional properties also hold:
47+
//! - `T` and `U` have the same vtable kinds. `T`'s and `U`'s pointer metadata
48+
//! is such that raw pointer casts preserve size and field placement.
49+
//! - `T` and `U` have `UnsafeCell`s at the same byte ranges.
50+
//!
51+
//! ## axiom-repr-transparent-layout-validity
52+
//!
53+
//! Given types `T` and `U`, if `T` is a `#[repr(transparent)]` struct with a
54+
//! `pub` field of type `U`, and `T` does not contain any other fields, then
55+
//! `T` has the property `transparent-layout-validity(U)`.
56+
//!
57+
//! Per the [Rust Reference][repr-transparent]:
58+
//!
59+
//! > \[`repr(transparent)`\] is only considered part of the public ABI of a
60+
//! > type if either its single field is `pub`, or if its layout is documented
61+
//! > in prose.
62+
//!
63+
//! [repr-transparent]: https://doc.rust-lang.org/nomicon/other-reprs.html#reprtransparent
64+
//!
65+
//! # Lemmas
66+
//!
67+
//! ## lemma-repr-transparent-zerocopy-traits
68+
//!
69+
//! - Lemma: Given types `T` and `U` where `T` is
70+
//! `transparent-layout-validity(U)`, for each `Trait` in `FromZeroes`,
71+
//! `FromBytes`, `AsBytes`, and `Unaligned`, if `U` satisfies the safety
72+
//! preconditions of `Trait`, then `T` does as well.
73+
//! - Proof:
74+
//! - `FromZeroes`, `FromBytes`, and `AsBytes` all require that a type not
75+
//! contain any `UnsafeCell`s. `T: transparent-layout-validity(U)`
76+
//! guarantees that, for all pairs of `t: *const T` and `u: *const U` of
77+
//! equal size, `t` and `u` refer to `UnsafeCell`s at the same byte ranges.
78+
//! If `U: FromZeroes`, `U: FromBytes`, or `U: AsBytes`, no instance of `U`
79+
//! contains `UnsafeCell`s at any byte ranges. Thus, no instance of `T`
80+
//! contains `UnsafeCell`s at any byte ranges.
81+
//! - `U: FromZeroes` additionally requires that, given `u: *const U`, it is
82+
//! sound to initialize `*u` to contain all zero bytes. Since, for all `t:
83+
//! *const T` and `u: *const U` of equal size, `*t` and `*u` have equal bit
84+
//! validity, then it must also be the case that, given `t: *const T`, it is
85+
//! sound to initialize `*t` to contain all zero bytes.
86+
//! - `U: FromBytes` additionally requires that, given `u: *const U`, it is
87+
//! sound to initialize `*u` to contain any sequence of `u8`s. Since, for
88+
//! all `t: *const T` and `u: *const U` of equal size, `*t` and `*u` have
89+
//! equal bit validity, then it must also be the case that, given `t: *const
90+
//! T`, it is sound to initialize `*t` to contain any sequence of `u8`s.
91+
//! - `U: AsBytes` additionally requires that, given `u: &U`, it is sound to
92+
//! treat `t` as an immutable `[u8]` of length `size_of_val(u)`. This is
93+
//! equivalent to saying that no instance of `U` can contain bytes which are
94+
//! invalid for `u8`. Since, for all `t: *const T` and `u: *const U` of
95+
//! equal size, `*t` and `*u` have equal bit validity, then it must also be
96+
//! the case that no instance of `T` can contain bytes which are invalid for
97+
//! `u8`.
98+
//! - `U: Unaligned` requires that `U`'s alignment is 1. `T:
99+
//! transparent-layout-validity(U)` guarantees that `T`'s alignment is equal
100+
//! to `U`'s, and is thus also 1.
101+
//!
102+
//! ## lemma-transparent-layout-validity-is-bit-valid
103+
//!
104+
//! - Lemma: Given `T` and `U` where `T` is `transparent-layout-validity(U)`,
105+
//! given `t: Ptr<'a, T>` which satisfies the safety preconditions of
106+
//! `TryFromBytes::<T>::is_bit_valid`, and given `u: Ptr<'a, U>` which
107+
//! addresses the same range as `t`, `u` satisfies the safety preconditions of
108+
//! `TryFromBytes::<U>::is_bit_valid`.
109+
//! - Proof: TODO
110+
//!
111+
//! WARNING: This might not actually be sound! In particular, `T:
112+
//! transparent-layout-validity(U)` doesn't guarantee that, given an enum
113+
//! discriminant with a particular value, the subset of values of `T` which are
114+
//! valid for that discriminant is the same as the subset of values of `U` which
115+
//! are valid for that discriminant. As a result, it may be possible to pass a
116+
//! `Ptr<T>` which has uninitialized bytes which are not problematic for `T` but
117+
//! which are problematic for `U`.

0 commit comments

Comments
 (0)