Teach transmute_{ref,mut}! to handle slice DSTs #2428

joshlf · 2025-03-07T22:27:19Z

TODO:

Convince ourselves that it's acceptable to drop the TransmuteFrom: SizeCompatible super-trait bound.
Write Kani tests for layout computations
Print useful error message when try_compute_cast_params fails during
static assertion
Test when post padding doesn't match between types
Do we need to prevent the padded size from increasing? While it's not
a problem on today's Rust, it would become a problem if unsized locals
are ever introduced, as you could then do *dst = ..., which would
have the effect of writing padding past the end of *src

Makes progress on #1817

Co-authored-by: Jack Wrenn [email protected]

This PR is on branch cell-traits.

joshlf · 2025-03-09T01:10:45Z

src/layout.rs

+    /// constructed using the address of `src` and using `dst_meta` as its
+    /// pointer metadata, then `dst` will address the same bytes as `src`.
+    ///
+    /// TODO: Mention that post-padding may not be preserved.


joshlf · 2025-03-09T01:10:51Z

src/layout.rs

+        //
+        // (15) `dst_len = src_len`
+        //
+        // [1] TODO


joshlf · 2025-03-09T01:10:54Z

src/layout.rs

+        //
+        // [1] TODO
+        //
+        // TODO: Clarify that this algorithm is agnostic to post-padding, and


joshlf · 2025-03-09T01:10:59Z

src/layout.rs

+        #[allow(clippy::arithmetic_side_effects)]
+        let elem_multiple = slf.elem_size / other.elem_size;
+
+        // INVARIANTS: TODO


joshlf · 2025-03-09T01:11:10Z

src/macros.rs

-            $crate::util::macro_util::must_use(u)
+            use $crate::util::macro_util::TransmuteRefDst;
+            let t = $crate::util::macro_util::Wrap(e);
+            // SAFETY: todo


joshlf · 2025-03-09T01:11:33Z

src/util/macros.rs

+        // SAFETY: TODO
+        unsafe_impl_for_transparent_wrapper!(T: ?Sized => $dst<T>);
+
+        // SAFETY: TODO


joshlf · 2025-03-09T01:11:37Z

src/util/macros.rs

+        // SAFETY: TODO
+        unsafe impl<T: ?Sized> InvariantsEq<$src<T>> for T {}
+
+        // SAFETY: TODO


joshlf · 2025-03-09T01:11:44Z

src/util/macros.rs

+        // SAFETY: TODO
+        unsafe impl<T: ?Sized> InvariantsEq<$dst<T>> for T {}
+
+        // SAFETY: TODO


joshlf · 2025-03-09T01:11:55Z

src/util/macros.rs

+        impl_for_transmute_from!(U: ?Sized + FromZeros => FromZeros for $dst<U>[<U>]);
+        impl_for_transmute_from!(U: ?Sized + IntoBytes => IntoBytes for $dst<U>[<U>]);
+
+        // SAFETY: TODO


joshlf · 2025-03-09T01:11:58Z

src/util/macros.rs

+        // SAFETY: TODO
+        unsafe_impl!(T: ?Sized + Immutable => Immutable for $src<T>);
+
+        // SAFETY: TODO


TODO: - Convince ourselves that it's acceptable to drop the `TransmuteFrom: SizeCompatible` super-trait bound. - Write Kani tests for layout computations - Print useful error message when `try_compute_cast_params` fails during static assertion - Test when post padding doesn't match between types - Do we need to prevent the padded size from increasing? While it's not a problem on today's Rust, it would become a problem if unsized locals are ever introduced, as you could then do `*dst = ...`, which would have the effect of writing padding past the end of `*src` Makes progress on #1817 Co-authored-by: Jack Wrenn <[email protected]> gherrit-pr-id: Ib4bc62202e0b3b09d155333b525087f7aa8f02c2

joshlf · 2025-03-09T07:01:08Z

src/pointer/transmute.rs

+/// For all [valid sizes] of `Src`, `ssize`, the following must hold:
+///
+/// Let `dsize` be the smallest valid size of `Dst` such that `dsize >=
+/// ssize`.\* For all `DV`-valid values of `Dst` with size `dsize`, `dst`, and
+/// for all `SV`-valid values of `Src` with size `ssize`, `src`, let `dst'` be
+/// constructed by concatenating `src` with the trailing `dsize - ssize` bytes
+/// of `dst`. It must be the case that `dst'` is a `DV`-valid `Dst`.
+///
+/// Now, instead let `dsize` be the largest valid size of `Dst` such that `dsize
+/// <= ssize`.\* For all `SV`-valid values of `Src` with size `ssize`, `src`, it
+/// must be the case that the leading `dsize` bytes of `src` constitute a
+/// `DV`-valid `Dst`.


The motivation behind this invariant is case analysis:

When going from &Src to &Dst, we require that ssize >= dsize, or else we'd produce a &Dst that addresses bytes past the end of the original referent. So long as we always implement such transmutes by choosing the largest dsize such that dsize <= ssize, then the second condition ensures that this is sound.

If we have already gone from &mut Dst to &mut Src (or & with interior mutation), then we need it to be the case that writing a src to this reference will not invalidate the original Dst. Again, so long as we always implement reference transmutes by choosing the largest possible valid size for the produced reference, then the first condition ensures that it is sound for the resulting &mut Src to be modified, overwriting the prefix of Dst.

My intention is that this should handle by-reference transmutations for all four combinations of sized or unsized Src to sized or unsized Dst:

Unsized to unsized is the fully general case described by this prose.

Sized to unsized means that there's exactly one value of ssize, but the subsequent condition still needs to hold (regarding the largest and smallest values of dsize on either size of ssize).

Unsized to sized means that there's exactly one value of dsize to consider in the analysis

For all values of ssize such that dsize <= ssize, we consider truncating transmutes

For all values of ssize such that dsize >= ssize, we consider tearing transmutes

Sized to sized is trivial, since there are no "foralls" or "there exists" involved. There are again two sub-cases:

If dsize <= ssize, we must consider truncating transmutes

If dsize >= ssize, we must consider tearing transmutes

This was referenced Mar 7, 2025

Remove obsolete safety proofs #2423

Merged

Implement traits for Cell #2421

Merged

[pointer] SizeEq supports raw pointer transmutes #2427

Merged

Teach transmute_{ref,mut}! to handle slice DSTs #1924

Closed

joshlf force-pushed the Ib4bc62202e0b3b09d155333b525087f7aa8f02c2 branch 6 times, most recently from 829b199 to a7c40db Compare March 8, 2025 16:58

joshlf force-pushed the I70d5aa5ace6bd2e39e679eac7f00a66d4b843d57 branch from 4d09d7c to f2ec335 Compare March 8, 2025 16:58

Base automatically changed from I70d5aa5ace6bd2e39e679eac7f00a66d4b843d57 to main March 8, 2025 19:16

joshlf force-pushed the Ib4bc62202e0b3b09d155333b525087f7aa8f02c2 branch 3 times, most recently from 98bbab7 to 5196fac Compare March 9, 2025 01:10

joshlf commented Mar 9, 2025

View reviewed changes

joshlf force-pushed the Ib4bc62202e0b3b09d155333b525087f7aa8f02c2 branch 2 times, most recently from 398966d to 976b234 Compare March 9, 2025 03:03

joshlf changed the base branch from main to I691b42ce8c0c3c6e5990e7684fc66f8f5dd73d85 March 9, 2025 03:03

joshlf mentioned this pull request Mar 9, 2025

[layout] Move Kani proofs from crate root #2430

Open

joshlf force-pushed the Ib4bc62202e0b3b09d155333b525087f7aa8f02c2 branch 3 times, most recently from 8634aa4 to bd3b50a Compare March 9, 2025 06:43

joshlf force-pushed the Ib4bc62202e0b3b09d155333b525087f7aa8f02c2 branch from bd3b50a to e972a2c Compare March 9, 2025 06:47

joshlf commented Mar 9, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Teach transmute_{ref,mut}! to handle slice DSTs #2428

Teach transmute_{ref,mut}! to handle slice DSTs #2428

joshlf commented Mar 7, 2025 •

edited

Loading

joshlf Mar 9, 2025

joshlf Mar 9, 2025

joshlf Mar 9, 2025

joshlf Mar 9, 2025

joshlf Mar 9, 2025

joshlf Mar 9, 2025

joshlf Mar 9, 2025

joshlf Mar 9, 2025

joshlf Mar 9, 2025

joshlf Mar 9, 2025

joshlf Mar 9, 2025

Teach transmute_{ref,mut}! to handle slice DSTs #2428

Are you sure you want to change the base?

Teach transmute_{ref,mut}! to handle slice DSTs #2428

Conversation

joshlf commented Mar 7, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

joshlf commented Mar 7, 2025 •

edited

Loading