[ptr] Simplify the conceptual model for pointer transmutes

*Authored by an AI agent acting on joshlf's behalf.*

## Overview

`Ptr`'s transmute machinery currently spreads one semantic question across a number of traits: `TryTransmuteFromPtr`, `TransmuteFromPtr`, `TransmuteFrom`, `MutationCompatible`, `InvariantsEq`, `Read`, `SizeEq`, `CastableFrom`, and the various `Because*` witnesses.

I think the underlying model is simpler than the trait graph makes it appear. In particular, most of these traits are not independent semantic concepts. They are proof machinery for one rule: when is it sound to reinterpret the same memory region under a different referent type and validity state?

This issue proposes making that rule the conceptual center of the model. This is related to #1866 and #2354, but is orthogonal to the question of where the invariants are encoded in Rust's type system.

## Proposed model

A `Ptr` carries four logically distinct things:

1. **A memory region.** `PtrInner` establishes the region's provenance, extent, and lifetime. `Project`, `Cast`, and `CastExact` describe how one region relates geometrically to another.
2. **An access discipline.** `Shared` and `Exclusive` describe who else may access the region and where mutation may come from.
3. **Alignment knowledge.** `Aligned` and `Unaligned` describe what this pointer proves about the address for its current referent type.
4. **An admissible-state contract.** The pair `(T, V)` determines what states may inhabit the referent of `Ptr`.

The fourth item is already close to the model in `Validity`: the documentation defines a set `S(T, V)` of values that may appear in the referent. The important point is that the *pair* `(T, V)` determines the state contract. Changing either `T` or `V` may change what states are permitted.

I don't think wrapping `(T, V)` in another conceptual object would simplify this model. `T` and `V` genuinely vary independently. A wrapper may still be a useful Rust encoding because it makes invalid independent updates harder to express.

## Exact reinterpretation has one rule

Consider an exact reinterpretation:

```text
Ptr -> Ptr
```

where the source and destination describe exactly the same bytes.

Let `Q(T, V)` denote the admissible states for a referent with type `T` and validity state `V`. The reinterpretation is sound if:

1. The current referent satisfies `Q(Dst, DV)`.
2. If the referent can be mutated through the source side, or through another mechanism permitted by the source while the destination is live, those writes preserve `Q(Dst, DV)`.
3. If the destination permits mutation, writes through the destination preserve `Q(Src, SV)`.
4. If `A = Shared`, simultaneously operating on the source and destination typed views is safe.

For state contracts that can be modeled as sets of possible referent values, (2) can often be proved by

```text
Q(Src, SV) ⊆ Q(Dst, DV)
```

and (3) by

```text
Q(Dst, DV) ⊆ Q(Src, SV).
```

This is already essentially the proof in `TryTransmuteFromPtr`. Its "forwards transmutation" condition establishes (2); its "reverse transmutation" condition establishes (3); and its final condition establishes (4). `TryTransmuteFromPtr` also deliberately leaves (1) to a separate mechanism, such as `TransmuteFrom` or a runtime validity check.

I think this should be the authoritative semantic rule. The rest of the transmute traits should be understood as ways to prove its premises.

## How the current traits fit

Under this model:

- `TransmuteFrom` proves a state implication: every `SV`-admissible `Src` state is `DV`-admissible for `Dst`, when the two referents have the same size. It does not itself describe a transmutation operation.
- `TryTransmuteFromPtr` proves that the reinterpretation is sound *conditional on* establishing the destination's current admissibility.
- `TransmuteFromPtr` is exactly the conjunction of `TryTransmuteFromPtr` and `TransmuteFrom`. It adds no new semantic concept.
- `MutationCompatible` packages sufficient proofs for some of the mutation and coexistence premises above. It is useful proof machinery, but I don't think "mutation compatibility" needs to be a separate part of the conceptual model.
- `InvariantsEq`'s actual contract is that safe code can operate on two differently typed shared views of the same region at the same time. That is closer to a relation such as `SharedCompatible` than to "the invariants are equal".
- `Read` and the `Because*` types select proof paths. They need not appear in the conceptual model.
- `SizeEq` selects a `CastExact` implementation. Its documentation already says that `SizeEq` itself conveys no safety guarantee; the guarantee comes from `CastExact`.
- `CastableFrom` is a proof helper for validity states whose admissibility is insensitive to the referent type in the cases it supports.

This framing also explains the existing FIXME comments around blanket `TransmuteFrom<_, Initialized, Initialized>` and `TransmuteFrom<_, _, Uninit>` impls. In those cases, the state relation genuinely does not depend on both Rust types. That looks strange only because a relation between state contracts is encoded as a trait relation between referent types.

## `Validity` and `Safe` need a clearer domain

There is one place where I don't think the current documentation quite supports the model it is trying to express.

`Validity` defines `S(T, V)` as a set of *bit values* and requires it to depend only on `T`'s bit validity. In particular, types with the same bit validity must induce the same set for a given `V`.

At the same time, `Safe` says that the referent is valid for `T`, "upholding bit validity and any library safety invariants."

Those statements are only compatible if the relevant library safety invariants are themselves determined by the referent's bit validity. Library invariants can in principle depend on other state: registration, ownership relationships, synchronization protocols, addresses, or other objects.

I see two coherent resolutions:

1. Narrow `Safe` so that its contract is strictly representational, and model non-representational library invariants elsewhere.
2. Generalize `S(T, V)` from a set of bit strings to an admissible-state predicate `Q(T, V)`, which may include whatever contextual state is required by `Safe`.

I currently prefer (2) as the conceptual model because it matches the existing wording of `Safe`, while leaving `Uninit`, `AsInitialized`, and `Initialized` as purely representational special cases.

This is a modeling/documentation point, not a claim that the current implementation is unsound.

## Shared coexistence should be an explicit relation

The reinterpretation rule has another independent premise: under `Shared`, operations through the two typed views must be mutually safe.

`InvariantsEq` already states almost exactly that contract:

> It is sound for safe code to operate on a `&T` and a `&Self` pointing to the same referent at the same time.

I think that relation deserves a direct name, such as `SharedCompatible`, rather than being described as equality of invariants.

This also makes one current shortcut worth examining. `TryTransmuteFromPtr` has an implementation for `Shared` when both `Src: Immutable` and `Dst: Immutable`. Zerocopy's internal `Immutable` contract establishes that a shared reference does not permit interior mutation of its referent. That is enough to remove mutation races through the two references, but it does not obviously establish that arbitrary library protocols attached to two different types are mutually compatible.

If zerocopy intends `Safe` and the relevant library invariants to be restricted to referent-local, mutation-mediated properties, we should make that restriction explicit. Otherwise, I think shared coexistence is a separate relation that should be proved directly.

Again, I have not found a concrete production unsoundness here. The point is that the published contracts do not obviously imply the proof obligation as currently stated.

## This rule permits useful asymmetry

The model also exposes a generalization that is easy to obscure in the current trait graph.

If the source side cannot mutate the referent while the destination is live, but the destination can mutate it, only the reverse preservation condition is needed:

```text
Q(Dst, DV) ⊆ Q(Src, SV)
```

If the destination cannot mutate, but the source side can, only the forward condition is needed:

```text
Q(Src, SV) ⊆ Q(Dst, DV)
```

Mutual inclusion is required only when writes can arrive from both directions. Some current `MutationCompatible` / `TransmuteFrom` proof paths establish both relations because that is a convenient sufficient condition, but the semantic rule itself does not require symmetry.

This distinction may let us admit sound cases without adding more special-purpose traits.

## What should remain separate

I would not collapse every `Ptr` operation into this rule.

**Alignment should remain independent.** It is local knowledge about a particular pointer/type interpretation. Unlike validity, forgetting alignment is harmless. An exact transmute can conservatively return `Unaligned` and re-establish alignment separately.

**Projection should remain distinct from exact reinterpretation.** For an exact cast, the source and destination denote the same region, so the two state-preservation directions above are enough. A shrinking projection can have validity that depends on bytes outside the projected region. Enum-field projection is the obvious example: whether a field exists can depend on a discriminant outside the field. The `HasTag` / `ProjectField` machinery is solving a genuinely different problem.

**Access discipline should remain independent from admissible state.** `Shared` versus `Exclusive` changes which preservation premises apply, but it is not itself a property of the stored state.

## Possible implementation direction

I would first make the semantic model explicit without trying to redesign every trait at once:

- Document the exact reinterpretation rule in one place, probably around `TryTransmuteFromPtr` / `Validity`.
- Define precisely what domain `Safe` ranges over: bit validity only, or a more general admissible-state predicate.
- Rename or redefine `InvariantsEq` around the actual shared-coexistence relation.
- Describe `TransmuteFrom` explicitly as a directional state implication rather than as a transmutation capability.
- Treat `TransmuteFromPtr`, `MutationCompatible`, `Read`, `SizeEq`, and the proof witnesses as encodings used to discharge premises of the rule.

After that, we can evaluate whether the Rust representation can be simplified. I would not start by deleting traits: fewer traits are only an improvement if the same proof complexity does not simply move into larger bounds or harder coherence problems.

## Relationship to existing issues

- #1866 established the important shift from validity as knowledge to validity as both knowledge and a constraint on future writes. This proposal keeps that insight and expresses it as the two directional preservation obligations above.
- #2354 asks whether invariants should be encoded in the referent type, especially as `Ptr` grows toward owned pointer kinds. That encoding question remains open under this proposal. The proposed model is intended to say what the encoding must preserve, regardless of which type-level representation we choose.

The main goal here is to reduce the number of concepts we need to reason about independently: one region model, one access model, one alignment model, one admissible-state model, and one exact-reinterpretation rule.

Start by reading the `TryTransmuteFromPtr` and `Validity` entry points, then compare their contracts with `TransmuteFrom`, `TransmuteFromPtr`, `MutationCompatible`, and `InvariantsEq`. Done would mean an explicit exact-reinterpretation rule and clarified relationships among the proof traits, but the issue does not identify specific files or tests.

Written by the indexing model from the issue text.