[pointer] Make validity transport `Safe`-based and cast-relative

The issue names no files or tests. Start by reading the existing TransmuteFrom, CastExact, TryTransmuteFromPtr, and TransmuteFromPtr definitions alongside #3686 and #3699. Done means the model expresses both validity-implication directions along one exact correspondence and the listed pointer, byte-trait, and wrapper cases use it.

Overview

#3686 reframed pointer transmutation around admissible-state preservation, and #3690 clarified the existing documentation in that direction. #3699 then exposed a more specific limitation in the current model: for DSTs, an equal byte length does not identify the concrete referent shape whose validity we need to compare. Its local ByteReprEq witness fixes that by combining an exact metadata-aware referent mapping with bidirectional Safe equivalence.

I think #3699 is the right narrow fix and should remain scoped as-is. This issue tracks the follow-on model in which that special-purpose witness becomes unnecessary.

The refined end state is:

1. Validity describes admissible referent states, not merely bit patterns.
2. Safe is the canonical state for a referent that may be treated as a typed T once the separately-modeled alignment and access/aliasing requirements are satisfied.
3. A concrete CastExact defines which source and destination referents correspond, including any required DST metadata transformation.
4. The relation currently modeled by TransmuteFrom becomes a directional admissible-state implication along that exact correspondence, rather than a claim about every pair of equally-sized referents.
5. The direction of the validity implication is independent of the direction in which the correspondence can be executed as a cast.

This would generalize the proof structure discovered in #3699 into the core pointer-transmute model.

Why Safe, rather than a new BitValid state

The current Validity contract describes S(T, V) as a set of bit values and requires it to depend only on T's bit validity. At the same time, Safe is documented as meaning that the referent is valid for T, including library safety invariants.

Those descriptions are in tension, and the rest of zerocopy already needs a notion stronger than raw compiler bit validity. For example, TryFromBytes for str checks UTF-8 before the bytes may be exposed through typed safe APIs.

I do not think adding a separate BitValid validity mode solves the underlying problem. It adds another state, but:

• pointer APIs ultimately need to know when a referent is safe to expose as a typed value/reference;
• the byte traits are naturally statements about transitions to or from that typed-safe state; and
• it does nothing to solve the DST metadata-correspondence problem which motivated #3699.

Instead, Validity should be defined over complete referent states, including which bytes are initialized. Safe should cover the referent-local typed/value invariants zerocopy requires before typed exposure. Alignment, aliasing, shared coexistence, and other access-discipline obligations remain separate concepts.

In particular, this does not mean that Safe should absorb arbitrary whole-program protocols. If an invariant cannot be stated as a property of the referent state itself, it belongs in another capability/proof relation rather than in Validity.

Under this model, several existing byte-trait contracts have especially simple meanings:

FromBytes:  Initialized ⊆ Safe(T)
IntoBytes:  Safe(T)    ⊆ Initialized
FromZeros:  zero       ∈ Safe(T)

TryFromBytes:
    Initialized --runtime check--> Safe(T)

A valid T may still have uninitialized padding, so Safe and Initialized remain genuinely independent states.

Exact correspondence must be part of validity transport

The existing TransmuteFrom<Src, SV, DV> contract is type-only: for equally-sized referents, it requires every SV-admissible Src state to be DV-admissible for the destination.

That is too coarse for DSTs.

Different metadata values can produce the same byte length while imposing different validity requirements. A slice DST with trailing padding can, for example, have two distinct metadata values whose referents occupy the same number of bytes even though a byte is padding under one interpretation and a typed element under the other.

So the statement we actually need is not:

for all equally-sized Src and Dst referents:
    Q(Src, SV) ⊆ Q(Dst, DV)

but instead:

for every pair of referents related by this exact correspondence C:
    Q(left, LV) ⊆ Q(right, RV)

where C preserves the exact referent bytes and may transform pointer metadata.

A CastExact<L, R> already provides a natural way to define such a correspondence: each concrete L referent is paired with the R referent produced by the cast.

Implication direction must be independent of cast direction

This is the subtle part exposed by #3699.

Suppose a correspondence is witnessed operationally by:

C: Self -> Repr

For the byte traits, we need both possible logical directions along the same pairs:

FromZeros / FromBytes / TryFromBytes:
    Safe(Repr(C(self))) -> Safe(Self(self))

IntoBytes:
    Safe(Self(self)) -> Safe(Repr(C(self)))

The first direction must not require an executable Repr -> Self cast. Such a cast can be stronger than necessary or may not exist. The Self -> Repr mapping is load-bearing because it covers every Self referent; a reverse-only mapping would require a separate surjectivity guarantee.

So the successor to the current TransmuteFrom model should separate:

• the orientation of the exact correspondence used to pair referents; and
• the direction of the admissible-state implication across those pairs.

The exact Rust encoding is deliberately left open here. It could be a revised TransmuteFrom, a successor relation parameterized by a CastExact, or another encoding. The semantic requirement is that both implication directions can be stated about the same one-way exact correspondence without requiring an inverse cast.

How this maps existing cases

This model should preserve the existing useful cases while making their actual proof obligations clearer.

Type-insensitive validity transitions

Relations such as these hold along any exact correspondence:

• Initialized -> Initialized;
• any validity -> Uninit;
• Safe -> Initialized when the source is IntoBytes;
• Initialized -> Safe when the destination is FromBytes.

They can remain blanket proof rules without pretending that the referent types themselves are semantically important.

Transparent wrappers and atomics

The current transparent-wrapper TransmuteFrom<_, Safe, Safe> impls intend to express that corresponding wrapper and representation referents have the same admissible typed states.

Under the new model, those claims would be made only along the wrapper's exact metadata-aware correspondence. They would no longer implicitly claim equivalence between arbitrary equally-sized DST referents.

This is the core generalization of #3699.

Pointer transmutation

TryTransmuteFromPtr already consumes a particular C: CastExact<Src, Dst>. Its source- and destination-preservation obligations should use admissible-state implications along that same C:

• writes possible through the source side require the forward implication;
• writes possible through the destination side require the reverse implication;
• establishing the destination's current validity can come from the forward implication or from a runtime check.

Shared coexistence remains a separate requirement such as SharedCompatible; equal Safe state sets do not prove that simultaneous typed access is harmless.

TransmuteFromPtr can continue to mean the infallible conjunction of the conditional pointer-transmute proof and the implication which establishes current destination validity.

By-value transmutation

#3688 and #3689 deliberately keep values as a separate carrier, but they want to share the carrier-independent validity relation.

For exact-size sized values, metadata is trivial and a canonical exact correspondence can recover the intended use:

Safe(Src) -> Safe(Dst)

So this refinement should preserve the main conclusion of those issues: values and pointers have different surviving-capability obligations, while the typed-state implication can still be shared.

Replacing ByteReprEq after #3699

#3699's private ByteReprEq<R> should be treated as the narrow repair, not as the final foundational abstraction.

It currently packages:

1. ToRepr: CastExact<ReadOnly<Self>, ReadOnly<R>>; and
2. bidirectional Safe equivalence along the referents selected by that cast.

Once the core model can express directional Safe implications along one named exact correspondence, the byte-trait helper should be expressible using those general pieces:

• FromZeros, FromBytes, and TryFromBytes require the Repr -> Self Safe implication along ToRepr;
• IntoBytes requires the Self -> Repr implication;
• TryFromBytes additionally executes ToRepr at Initialized validity to delegate the runtime validator.

At that point, ByteReprEq can likely disappear or become a trivial composition of the general relations.

Proposed migration order

1. Land #3699 unchanged in scope. It closes #3691 without waiting for this redesign.
2. Clarify the semantic domain of Validity and Safe. Replace the bit-pattern-only formulation with referent-state predicates, and explicitly keep alignment/access/coexistence outside Safe.
3. Introduce a cast-relative admissible-state implication relation. The model must support both logical directions along one one-way CastExact.
4. Port the existing blanket validity transitions (Initialized, Uninit, IntoBytes, FromBytes) to the new relation.
5. Port wrapper/atomic Safe relations so they are stated only for corresponding referents.
6. Refactor TryTransmuteFromPtr / TransmuteFromPtr to consume those cast-relative relations.
7. Refactor the helper added by #3699 and remove ByteReprEq if the general relation fully subsumes it.
8. Only then decide whether the old TransmuteFrom name/trait should be replaced, retained as a compatibility layer, or narrowed to cases where metadata ambiguity cannot occur.

Non-goals

This issue should not:

• reopen #3699 or delay its narrow soundness fix;
• merge alignment, aliasing, or shared coexistence into Validity;
• make by-value values another Ptr carrier;
• require an inverse CastExact merely to state the reverse validity implication;
• add BitValid merely for terminological symmetry;
• redesign shrinking projection, whose validity can depend on bytes outside the projected region.

Relationship to other work

• #1866 established that validity is both knowledge and a constraint on future writes.
• #2354 tracks how validity/invariants are represented in Rust types; this issue is about the semantic relation those encodings must preserve.
• #3686 proposed the admissible-state model and identified the existing tension between bit validity and Safe. This issue chooses a more concrete follow-on: referent-state validity, with access/protocol obligations kept separate.
• #3688 separates by-value transmutation from pointer carrier semantics.
• #3689 proposes a valid-only Value<T> and uses TransmuteFrom<_, Safe, Safe> as the carrier-independent validity relation; this issue refines what that relation should mean.
• #3690 clarified the current pointer-transmute documentation without changing its contract.
• #3691 identified the immediate hole in impl_for_transmute_from!.
• #3699 fixes #3691 locally with a metadata-aware ByteReprEq; this issue tracks the foundational model which could later subsume that helper.

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