Encapsulate slice-DST size formulas behind a private invariant-bearing type #3640

Context

#3630 fixes #3617 by representing a slice DST’s total-size sequence
independently from the physical offset of its trailing slice. After that
change, TrailingSliceLayout carries sibling pub(crate) fields for the
physical trailing-slice offset, trailing element size, and a normalized
formula:

size(elems) = prefix + round_up(offset + elems * elem_size, alignment)

where alignment is nonzero and a power of two and prefix < alignment.

This distinction is safety-critical. Packing can change a field’s physical
placement without changing trailing padding internal to the field’s type.
#3617 arose from conflating those concepts.

The representation and normalization arithmetic are currently exposed as
individual crate-visible fields. Callers can destructure, reconstruct, or
partially update them, making it possible for future changes to preserve one
coordinate while invalidating the other.

Proposal

Introduce a private invariant-bearing abstraction for the normalized
total-size sequence, conceptually:

struct SliceSizeFormula<E = usize> {
    prefix: usize,
    offset: usize,
    elem_size: E,
    alignment: NonZeroUsize,
}

struct TrailingSliceLayout<E = usize> {
    trailing_slice_offset: usize,
    size: SliceSizeFormula<E>,
}

Names and exact field division are open to bikeshedding. The important
properties are:

1. Formula fields are private to the smallest practical leaf module.
2. The physical trailing-field offset is represented separately from the
   formula’s internal offset.
3. Code outside that module cannot directly construct or partially mutate a
   formula.
4. Consumers use checked proof-oriented operations rather than reproducing
   normalization arithmetic.

Candidate operations include checked construction/normalization,
size_for_elems, exact-size-to-metadata inversion, equality of complete size
sequences, checked prefix composition/formula shifting, padding/alignment
composition, trailing-element-size access, and separate physical trailing-slice
offset/end computations. Operations used in constants must preserve the
project’s MSRV and const-evaluation requirements.

Invariants

The abstraction should make these properties local and reviewable:

• alignment is nonzero and a power of two;
• prefix < alignment;
• size_for_elems(n) implements the documented normalized formula whenever
  checked arithmetic succeeds;
• construction, composition, and padding preserve normalization;
• the physical trailing-slice range is never inferred from the formula’s
  internal offset;
• for layouts admitted by KnownLayout, the physical trailing-slice end is no
  greater than the computed total object size; and
• overflow remains explicit rather than hidden by normalization.

DstLayout may retain its existing public-contract posture; this proposal
shrinks the crate-internal region that can manipulate the safety-critical
formula representation.

Acceptance criteria

• No production code outside the owning module directly constructs or mutates
  formula fields.
• DstLayout composition, padding, casting, projection, allocation, and split
  consumers use the abstraction’s operations.
• Tests cover formulas whose physical trailing offset differs from the internal
  rounding origin, including Security Advisory: Nested packed DST layouts underallocate memory and permit out-of-bounds access #3617’s nested-packed regression.
• Existing Kani coverage is moved or extended to checked construction,
  normalization, composition, padding, inversion, and sequence equivalence
  over their stated domains.
• KnownLayout documentation describes the same canonical formula and
  physical-offset distinction.
• Public behavior and supported layout domains do not change.

Non-goals

• Re-fixing Security Advisory: Nested packed DST layouts underallocate memory and permit out-of-bounds access #3617; Preserve nested DST padding in layout formulas #3630 supplies that semantic repair.
• Exposing the new representation publicly.
• Broadly replacing derive logic with meta-types; that remains Meta types to replace derive logic #1948.
• Completing Prove soundness of layout::cast_from #3199’s formal-verification work, though this abstraction should
  make it smaller and more local.

Related: #3617, #3630, #3199, #1948, #2541.

Authored by an AI agent acting on Josh Liebow-Feeser's behalf.