Prove referent validity implications for native trait impls

verification/aeneas/DESIGN.md

@@ -414,11 +414,12 @@ parallel coverage registry or automatic Rust ABI assumptions.
 - **Broader carriers and effects.** Recursive nominal groups, general indexed
   carriers, const generics, associated-type trait laws, higher-ranked bounds, bounded
   nominal models, and escaping borrow reconstruction remain unsupported with
-  explicit errors. The first trait-law bridge supports `Self`-only traits and
-  simple generic bounds, with `Unaligned` and a total byte codec as checked
-  examples. Add semantics and admission checks before accepting
-  them. Stateful or nondeterministic APIs may need observable traces and
-  effects, rather than only result contracts.
+  explicit errors. The trait-law bridge supports type-parameterized traits
+  and type-only bounds, preserving every original argument and native
+  dictionary. `TransmuteFrom` exercises four ordered type arguments and
+  generic state-model providers. Add semantics and admission checks before
+  accepting the remaining carriers. Stateful or nondeterministic APIs may need
+  observable traces and effects, rather than only result contracts.
 - **Abstract storage and bit validity.** Check byte-to-value production before
   entering Aeneas's typed value domain; rejection must remain a forbidden
   execution, independently of ordinary library-model admission. A storage model
@@ -471,3 +472,22 @@ The generic-field staging problem and copy-back gap are resolved. Model proof
 completion is scoped to decoder construction rather than defaults attached to
 the model declaration. Encoders, losslessness, and representation certificates
 remain optional properties justified by particular operation proofs.
+
+## Referent contents: implemented scope
+
+The shared `Rust.Referent` algebra covers uninitialized, initialized, and safe
+byte domains, including empty safe domains. The zerocopy adapter uses the
+retained physical and mathematical decoders. Validity markers carry optional
+type-level codes, checked against their actual `Validity::KIND` dictionaries.
+This uses the existing model-provider binding and audit; it adds no separate
+state-dictionary inference mechanism.
+
+Marked `TransmuteFrom` blanket impls, ordinary wrapper pairs, and the two
+`Cell`/`UnsafeCell` chains have checked native law proofs. `CastableFrom` retains
+its exact two identity pairs. Generic clients consume those laws, while
+independent outcome families state the actual byte implications. Execution
+success remains outside any conditional interpretation of a validity state.
+
+`AsInitialized` contents and opaque `MaybeUninit` storage remain deferred.
+Pointer casts and projections will additionally need explicit byte-range,
+metadata, access, and resource arguments. These content laws do not grant them.

verification/aeneas/README.md

@@ -533,10 +533,12 @@ admitted implementation method body in the original and final ASTs, even when
 only the law refers to the method. Excluded provided methods cannot execute;
 interface-only validators retain their required signatures but cannot be called.
 
-This initial bridge accepts traits with only their `Self` parameter and simple
-generic bounds. It compares compiler-resolved original and final type
-applications, rather than matching clause ordinals. Associated types, higher
-ranked bounds, transformed carrier identities, and bounds on nominal model
+The bridge accepts type-parameterized traits and type-only bounds, including
+`?Sized`. It preserves the complete ordered application: `Self` and every other
+Rust type argument. Source syntax records bound arity; compiler identities
+resolve the arguments. Original and final applications must agree, including
+repeated arguments, rather than merely matching clause ordinals. Associated
+types, higher ranked bounds, transformed carrier identities, and bounds on nominal model
 definitions fail closed. The compiled audit independently enumerates
 implementation dictionaries and
 requires the same complete set of proof obligations. Omitting or swapping a
@@ -1325,3 +1327,42 @@ size guard, providers, trait premises, and destination admission. The exact
 [semantic scope and Rust premises](SEMANTICS.md#generic-owned-conversion-through-transmute_copy)
 exclude pointer provenance, resource ownership, meaningful destructor execution,
 and general storage-copy effects. The production `transmute!` macro is unchanged.
+
+## Referent validity implications
+
+`Rust.Referent` in `anneal/lean` describes three byte-content promises at an
+explicit width: `Uninit` permits any contents, `Initialized` requires initialized
+bytes, and `Safe` requires successful physical and mathematical decoding. An
+uninhabited type can have an empty safe domain. No default value, inhabitedness,
+unique representation, or canonical encoding is required.
+
+The `TransmuteFrom` annotation in `pointer/transmute.rs` checks directional
+inclusion of these domains when widths agree. Four blanket impls use the
+existing `IntoBytes` and `FromBytes` laws or weaken the content promise. Twelve
+wrapper directions compare the actual mapped physical decoder and its retained
+mathematical decoder. The two `Cell`/`UnsafeCell` chains use those same domain
+equivalences. `CastableFrom` has a separate, exact invariant: both states are
+`Uninit`, or both are `Initialized`.
+
+The four empty validity-marker types retain their empty extracted carriers.
+Their generated model providers carry an optional type-level code; the
+`Validity` law checks that code against the actual `KIND` constant. Missing code
+metadata rejects the law. The code identifies `AsInitialized` but supplies no
+interpretation of its contents. Forgetting any state to `Uninit` remains valid
+without that interpretation.
+
+`pointer/referent_checks.rs` consumes the actual Rust bounds, including unused
+bounds, and selects concrete blanket and wrapper dictionaries. Its generic
+composition test requires equal source and intermediate widths. Without that
+premise, two transfers could hold only because their individual width guards
+are false. Independent required contracts restate the byte implications and
+require successful execution even when no modeled state matches a marker.
+Both golden and live builds check every marked impl and discovered spec.
+
+These are conditional facts about contents. Applying them to Rust requires the
+installed physical decoder and mathematical model to describe that referent.
+A missing physical decoder supplies no view from which to reason; it is not an
+empty safe domain. Pointer access, provenance, aliasing, mutation permissions,
+and external resources remain separate obligations. The pinned extractor gives
+`MaybeUninit<T>` an opaque carrier without a byte-storage interpretation, so
+its transitive wrapper impls remain unmarked and deferred.

verification/aeneas/SEMANTICS.md

@@ -322,3 +322,23 @@ and [`transmute_copy` documentation](https://doc.rust-lang.org/1.74.0/core/mem/f
 The numeric, resource-free representation profiles remain the supported domain;
 this proof does not admit arbitrary downstream representations merely because a
 trait dictionary can be extracted.
+
+## Referent-content boundary
+
+`Rust.Referent.Allowed` combines an explicit byte width with a content promise.
+`Safe` requires a raw value from physical decoding and a mathematical value
+from that same retained model's decoder. An empty safe domain makes a
+safe-source implication vacuous without constructing an impossible value.
+Completeness in the other direction still requires an actual decoded result.
+
+`TransmuteFrom` is conditional on equal widths. Its composition theorem also
+requires the intermediate width to agree; outer equality alone is insufficient.
+Transparent-wrapper proofs compare both decoding stages, so equal layout alone
+cannot erase a library invariant. `CastableFrom` states its two permitted type
+identity pairs directly, rather than accepting coincidentally equal safe domains.
+
+The type-level validity codes identify the four empty Rust markers and agree
+with their actual associated constants. They do not inhabit the marker types
+or interpret `AsInitialized`. The resource-free numeric representation premise
+still governs application to Rust; these laws provide no permission to access
+or mutate memory. Opaque `MaybeUninit` has no admitted storage model here.