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.

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

Tracking issue for outstanding safety proofs blocking 0.8 #896

Closed
Tracked by #671
joshlf opened this issue Feb 17, 2024 · 0 comments · Fixed by #1620
Closed
Tracked by #671

Tracking issue for outstanding safety proofs blocking 0.8 #896

joshlf opened this issue Feb 17, 2024 · 0 comments · Fixed by #1620
Labels
blocking-next-release This issue should be resolved before we release on crates.io

Comments

@joshlf
Copy link
Member

joshlf commented Feb 17, 2024

This issue tracks all safety proofs which are not complete and need to be completed before we perform a stable release. All such proofs are marked as // TODO(#896).


Outstanding TODOs as of b96b620 (2024-04-29):

zerocopy/src/lib.rs

Lines 3831 to 3870 in b96b620

/// SAFETY:
/// - The safety requirements for `unsafe_impl!` with an `is_bit_valid`
/// closure:
/// - Given `t: *mut NonZeroXxx` and `let r = *mut xxx`, `r` refers to an
/// object of the same size as that referred to by `t`. This is true
/// because `NonZeroXxx` and `xxx` have the same size. [1] Neither `r`
/// nor `t` refer to any `UnsafeCell`s because neither `NonZeroXxx` [2]
/// nor `xxx` do.
/// - Since the closure takes a `&xxx` argument, given a `Maybe<'a,
/// NonZeroXxx>` which satisfies the preconditions of
/// `TryFromBytes::<NonZeroXxx>::is_bit_valid`, it must be guaranteed
/// that the memory referenced by that `MabyeValid` always contains a
/// valid `xxx`. Since `NonZeroXxx`'s bytes are always initialized [1],
/// `is_bit_valid`'s precondition requires that the same is true of its
/// argument. Since `xxx`'s only bit validity invariant is that its
/// bytes must be initialized, this memory is guaranteed to contain a
/// valid `xxx`.
/// - The impl must only return `true` for its argument if the original
/// `Maybe<NonZeroXxx>` refers to a valid `NonZeroXxx`. The only
/// `xxx` which is not also a valid `NonZeroXxx` is 0. [1]
///
/// [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.
///
/// [2] TODO(#896): Write a safety proof for this before the next stable
/// release.
unsafe_impl!(NonZeroU8: TryFromBytes; |n: MaybeAligned<u8>| NonZeroU8::new(n.read_unaligned()).is_some());
unsafe_impl!(NonZeroI8: TryFromBytes; |n: MaybeAligned<i8>| NonZeroI8::new(n.read_unaligned()).is_some());
unsafe_impl!(NonZeroU16: TryFromBytes; |n: MaybeAligned<u16>| NonZeroU16::new(n.read_unaligned()).is_some());
unsafe_impl!(NonZeroI16: TryFromBytes; |n: MaybeAligned<i16>| NonZeroI16::new(n.read_unaligned()).is_some());
unsafe_impl!(NonZeroU32: TryFromBytes; |n: MaybeAligned<u32>| NonZeroU32::new(n.read_unaligned()).is_some());
unsafe_impl!(NonZeroI32: TryFromBytes; |n: MaybeAligned<i32>| NonZeroI32::new(n.read_unaligned()).is_some());
unsafe_impl!(NonZeroU64: TryFromBytes; |n: MaybeAligned<u64>| NonZeroU64::new(n.read_unaligned()).is_some());
unsafe_impl!(NonZeroI64: TryFromBytes; |n: MaybeAligned<i64>| NonZeroI64::new(n.read_unaligned()).is_some());
unsafe_impl!(NonZeroU128: TryFromBytes; |n: MaybeAligned<u128>| NonZeroU128::new(n.read_unaligned()).is_some());
unsafe_impl!(NonZeroI128: TryFromBytes; |n: MaybeAligned<i128>| NonZeroI128::new(n.read_unaligned()).is_some());
unsafe_impl!(NonZeroUsize: TryFromBytes; |n: MaybeAligned<usize>| NonZeroUsize::new(n.read_unaligned()).is_some());
unsafe_impl!(NonZeroIsize: TryFromBytes; |n: MaybeAligned<isize>| NonZeroIsize::new(n.read_unaligned()).is_some());

zerocopy/src/lib.rs

Lines 3908 to 3920 in b96b620

/// SAFETY:
/// While it's not fully documented, the consensus is that `Box<T>` does not
/// contain any `UnsafeCell`s for `T: Sized` [1].
///
/// [1] https://github.com/rust-lang/unsafe-code-guidelines/issues/492
///
/// TODO(#896): Write a more complete safety proof before the next stable
/// release.
#[cfg(feature = "alloc")]
unsafe_impl!(
#[cfg_attr(doc_cfg, doc(cfg(feature = "alloc")))]
T: Sized => Immutable for Box<T>
);

zerocopy/src/lib.rs

Lines 3984 to 3987 in b96b620

/// SAFETY:
/// TODO(#896): Write this safety proof before the next stable release.
unsafe_impl_for_power_set!(A, B, C, D, E, F, G, H, I, J, K, L -> M => Immutable for opt_fn!(...));
unsafe_impl_for_power_set!(A, B, C, D, E, F, G, H, I, J, K, L -> M => Immutable for opt_extern_c_fn!(...));

zerocopy/src/lib.rs

Lines 4009 to 4029 in b96b620

/// SAFETY:
/// Per [1], `AtomicBool`, `AtomicU8`, and `AtomicI8` have the same size as
/// `bool`, `u8`, and `i8` respectively. Since a type's alignment cannot be
/// smaller than 1 [2], and since its alignment cannot be greater than its
/// size [3], the only possible value for the alignment is 1. Thus, it is
/// sound to implement `Unaligned`.
///
/// [1] TODO(#896), TODO(https://github.com/rust-lang/rust/pull/121943):
/// Cite docs once they've landed.
///
/// [2] Per https://doc.rust-lang.org/reference/type-layout.html#size-and-alignment:
///
/// Alignment is measured in bytes, and must be at least 1.
///
/// [3] Per https://doc.rust-lang.org/reference/type-layout.html#size-and-alignment:
///
/// The size of a value is always a multiple of its alignment.
unsafe_impl!(AtomicBool: Unaligned);
unsafe_impl!(AtomicU8: Unaligned);
unsafe_impl!(AtomicI8: Unaligned);
assert_unaligned!(AtomicBool, AtomicU8, AtomicI8);

zerocopy/src/lib.rs

Lines 4267 to 4270 in b96b620

/// SAFETY:
///
/// TODO(#896): Write this safety proof before the next stable release.
unsafe_impl!(T: ?Sized => Immutable for NonNull<T>);

zerocopy/src/util.rs

Lines 107 to 119 in b96b620

// SAFETY:
// - Per [1], `MaybeUninit<T>` has the same size as `T`.
// - See inline comments for other safety justifications.
//
// [1] TODO(#896): Write a safety proof before the next stable release.
unsafe impl<T, I: Invariants> TransparentWrapper<I> for MaybeUninit<T> {
type Inner = T;
// SAFETY: Per [1], `MaybeUninit<T>` has `UnsafeCell`s at the same byte
// ranges as `Inner = T`, and `UnsafeCell`s at the same byte offsets as `T`.
//
// [1] TODO(#896): Write a safety proof before the next stable release.
type UnsafeCellVariance = Covariant;

zerocopy/src/util.rs

Lines 149 to 161 in b96b620

// SAFETY:
// - Per [1], `ManuallyDrop<T>` has the same size as `T`.
// - See inline comments for other safety justifications.
//
// [1] TODO(#896): Write a safety proof before the next stable release.
unsafe impl<T: ?Sized, I: Invariants> TransparentWrapper<I> for ManuallyDrop<T> {
type Inner = T;
// SAFETY: Per [1], `ManuallyDrop<T>` has `UnsafeCell`s at the same byte
// ranges as `Inner = T`, and `UnsafeCell`s at the same byte offsets as `T`.
//
// [1] TODO(#896): Write a safety proof before the next stable release.
type UnsafeCellVariance = Covariant;

zerocopy/src/util.rs

Lines 194 to 206 in b96b620

// SAFETY:
// - Per [1], `Wrapping<T>` has the same size as `T`.
// - See inline comments for other safety justifications.
//
// [1] TODO(#896): Write a safety proof before the next stable release.
unsafe impl<T, I: Invariants> TransparentWrapper<I> for Wrapping<T> {
type Inner = T;
// SAFETY: Per [1], `Wrapping<T>` has `UnsafeCell`s at the same byte ranges
// as `Inner = T`, and `UnsafeCell`s at the same byte offsets as `T`.
//
// [1] TODO(#896): Write a safety proof before the next stable release.
type UnsafeCellVariance = Covariant;

zerocopy/src/util.rs

Lines 349 to 401 in b96b620

($(#[$attr:meta])* $tyvar:ident => $atomic:ty [$native:ty]) => {
// We implement for `$atomic` and set `Inner = $native`. The caller has
// promised that `$atomic` and `$native` are an atomic type and its
// native counterpart, respectively. Per [1], `$atomic` and `$native`
// have the same size.
//
// [1] TODO(#896), TODO(https://github.com/rust-lang/rust/pull/121943):
// Cite docs once they've landed.
$(#[$attr])*
unsafe impl<$tyvar, I: Invariants> TransparentWrapper<I> for $atomic {
unsafe_impl_transparent_wrapper_for_atomic!(@inner $atomic [$native]);
}
};
(@inner $atomic:ty [$native:ty]) => {
type Inner = UnsafeCell<$native>;
// SAFETY: It is "obvious" that each atomic type contains a single
// `UnsafeCell` that covers all bytes of the type, but we can also prove
// it:
// - Since `$atomic` provides an API which permits loading and storing
// values of type `$native` via a `&self` (shared) reference, *some*
// interior mutation must be happening, and interior mutation can only
// happen via `UnsafeCell`. Further, there must be enough bytes in
// `$atomic` covered by an `UnsafeCell` to hold every possible value
// of `$native`.
// - Per [1], `$atomic` has the same size as `$native`. This on its own
// isn't enough: it would still be possible for `$atomic` to store
// `$native` using a compact representation (for `$native` types for
// which some bit patterns are illegal). However, this is ruled out by
// the fact that `$atomic` has the same bit validity as `$native` [1].
// Thus, we can conclude that every byte of `$atomic` must be covered
// by an `UnsafeCell`.
//
// Thus, every byte of `$atomic` is covered by an `UnsafeCell`, and we
// set `type Inner = UnsafeCell<$native>`. Thus, `Self` and
// `Self::Inner` have `UnsafeCell`s covering the same byte ranges.
//
// [1] TODO(#896), TODO(https://github.com/rust-lang/rust/pull/121943):
// Cite docs once they've landed.
type UnsafeCellVariance = Covariant;
// SAFETY: No safety justification is required for an invariant
// variance.
type AlignmentVariance = Invariant;
// SAFETY: Per [1], all atomic types have the same bit validity as their
// native counterparts. The caller has promised that `$atomic` and
// `$native` are an atomic type and its native counterpart,
// respectively.
//
// [1] TODO(#896), TODO(https://github.com/rust-lang/rust/pull/121943):
// Cite docs once they've landed.
type ValidityVariance = Covariant;

@joshlf joshlf mentioned this issue Feb 17, 2024
87 tasks
@joshlf joshlf added the blocking-next-release This issue should be resolved before we release on crates.io label May 30, 2024
joshlf added a commit that referenced this issue Sep 7, 2024
Adds some informal proofs as accepted risks per #1358

Makes progress on #896
joshlf added a commit that referenced this issue Sep 7, 2024
Adds some informal proofs as accepted risks per #1358

Makes progress on #896
github-merge-queue bot pushed a commit that referenced this issue Sep 7, 2024
Adds some informal proofs as accepted risks per #1358

Makes progress on #896
joshlf added a commit that referenced this issue Sep 8, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
blocking-next-release This issue should be resolved before we release on crates.io
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant