[WIP] KnownLayout::validate_size_align

TODO: Tests

src/lib.rs

@@ -225,6 +225,11 @@ pub struct DstLayout {
     _trailing_slice_elem_size: Option<usize>,
 }
 
+enum _CastType {
+    _Prefix,
+    _Suffix,
+}
+
 impl DstLayout {
     /// Constructs a `DstLayout` which describes `T`.
     ///
@@ -251,6 +256,124 @@ impl DstLayout {
             _trailing_slice_elem_size: Some(mem::size_of::<T>()),
         }
     }
+
+    /// TODO
+    ///
+    /// The caller is responsible for ensuring that `addr + bytes_len` does not
+    /// overflow `usize`.
+    ///
+    /// # Panics
+    ///
+    /// If `addr + bytes_len` overflows `usize`, `validate_cast` may panic, or
+    /// it may return incorrect results. No guarantees are made about when
+    /// `validate_cast` will panic. The caller should not rely on
+    /// `validate_cast` panicking in any particular condition, even if
+    /// `debug_assertions` are enabled.
+    const fn _validate_cast(
+        &self,
+        addr: usize,
+        bytes_len: usize,
+        cast_type: _CastType,
+    ) -> Option<(usize, usize, usize)> {
+        let base_size = self._base_layout.size();
+
+        // LEMMA 0: max_slice_bytes + base_size == bytes_len
+        //
+        // LEMMA 1: base_size <= bytes_len:
+        // - If `base_size > bytes_len`, `bytes_len.checked_sub(base_size)`
+        //   returns `None`, and we return.
+        let Some(max_slice_bytes) = bytes_len.checked_sub(base_size) else {
+            return None;
+        };
+
+        let (elems, self_bytes) = if let Some(elem_size) = self._trailing_slice_elem_size {
+            let Some(elem_size) = NonZeroUsize::new(elem_size) else {
+                panic!("attempted to cast to slice type with zero-sized element");
+            };
+
+            // Guaranteed not to divide by 0 because `elem_size` is a
+            // `NonZeroUsize`.
+            //
+            // LEMMA 2: elems * elem_size <= max_slice_bytes
+            #[allow(clippy::arithmetic_side_effects)]
+            let elems = max_slice_bytes / elem_size.get();
+
+            // Guaranteed not to overflow:
+            // - elems * elem_size <= max_slice_bytes (lemma 2)
+            // - max_slice_bytes   <= usize::MAX      (max_slice_bytes: usize)
+            // - elems * elem_size <= usize::MAX      (substitution)
+            //
+            // LEMMA 3: slice_bytes <= max_slice_bytes:
+            // - max_slice_bytes + base_size == bytes_len                   (lemma 0)
+            // - base_size                   == bytes_len - max_slice_bytes
+            // - elems * elem_size           <= max_slice_bytes             (lemma 2)
+            // - slice_bytes                 <= max_slice_bytes             (substitution)
+            #[allow(clippy::arithmetic_side_effects)]
+            let slice_bytes = elems * elem_size.get();
+
+            // Guaranteed not to overflow:
+            // - max_slice_bytes + base_size == bytes_len       (lemma 0)
+            // - slice_bytes                 <= max_slice_bytes (lemma 3)
+            // - slice_bytes + base_size     <= bytes_len       (substitution)
+            // - bytes_len                   <= usize::MAX      (bytes_len: usize)
+            // - slice_bytes + base_size     <= usize::MAX      (substitution)
+            //
+            // LEMMA 3: self_bytes <= bytes_len: TODO
+            #[allow(clippy::arithmetic_side_effects)]
+            let self_bytes = base_size + slice_bytes;
+
+            (elems, self_bytes)
+        } else {
+            (0, base_size)
+        };
+
+        // LEMMA 4: self_bytes <= bytes_len:
+        // - `if` branch returns `self_bytes`; lemma 3 guarantees `self_bytes <=
+        //   bytes_len`
+        // - `else` branch returns `base_size`; lemma 1 guarantees `base_size <=
+        //   bytes_len`
+
+        // `self_addr` indicates where in the given byte range the `Self` will
+        // start. If we're doing a prefix cast, it starts at the beginning. If
+        // we're doing a suffix cast, it starts after whatever bytes are
+        // remaining.
+        let (self_addr, split_at) = match cast_type {
+            _CastType::_Prefix => (addr, self_bytes),
+            _CastType::_Suffix => {
+                // Guaranteed not to underflow because `self_bytes <= bytes_len`
+                // (lemma 4).
+                //
+                // LEMMA 5: split_at = bytes_len - self_bytes
+                #[allow(clippy::arithmetic_side_effects)]
+                let split_at = bytes_len - self_bytes;
+
+                // Guaranteed not to overflow:
+                // - addr + bytes_len <= usize::MAX                    (method precondition)
+                // - split_at         == bytes_len - self_bytes        (lemma 5)
+                // - addr + split_at  == addr + bytes_len - self_bytes (substitution)
+                // - addr + split_at  <= addr + bytes_len
+                // - addr + split_at  <= usize::MAX                    (substitution)
+                #[allow(clippy::arithmetic_side_effects)]
+                let self_addr = addr + split_at;
+
+                (self_addr, split_at)
+            }
+        };
+
+        // Guaranteed not to divide by 0 because `.align()` guarantees that it
+        // returns a non-zero value.
+        #[allow(clippy::arithmetic_side_effects)]
+        if self_addr % self._base_layout.align() != 0 {
+            return None;
+        }
+
+        // Guaranteed not to underflow because `self_bytes <= bytes_len` (lemma
+        // 4).
+        #[allow(clippy::arithmetic_side_effects)]
+        let prefix_suffix_bytes = bytes_len - self_bytes;
+
+        Some((elems, split_at, prefix_suffix_bytes))
+    }
 }
 
 /// A trait which carries information about a type's layout that is used by the