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

## 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:

```text
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:

```rust
struct SliceSizeFormula {
prefix: usize,
offset: usize,
elem_size: E,
alignment: NonZeroUsize,
}

struct TrailingSliceLayout {
trailing_slice_offset: usize,
size: SliceSizeFormula,
}
```

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 #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 #3617; #3630 supplies that semantic repair.
- Exposing the new representation publicly.
- Broadly replacing derive logic with meta-types; that remains #1948.
- Completing #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.*

Begin by locating the owning module for TrailingSliceLayout and its DstLayout composition, padding, casting, projection, allocation, and split consumers; then inspect existing Kani coverage and KnownLayout documentation. Done means formula fields are private, consumers use checked abstraction operations, regression tests cover differing physical and internal offsets, and public behavior is unchanged.

Written by the indexing model from the issue text.