Add section on impl existence reasoning

unsafe_rust_review/SKILL.md

@@ -805,6 +805,90 @@ Examples:
 Postconditions are especially important for unsafe traits and unsafe
 constructors whose results are later used by safe code or other unsafe proofs.
 
+### 11. Do not rely on the absence of an impl
+
+An `unsafe impl`'s obligation must be discharged with facts that remain true
+under program extension: new crates, new types, new impls. The impl set of a
+safe trait is open and extendable by safe code, and the absence of a trait
+implementation on a type is not such a fact.
+
+The suspect pattern:
+```rust
+/// # Safety
+/// If a type implements both `UnsafeTr` and `SafeTr`, `SafeTr` must behave
+/// a certain way.
+unsafe trait UnsafeTr {}
+```
+
+This conditions an unsafe obligation on the behavior of a safe trait.
+Whichever impl completes the pair `UnsafeTr + SafeTr` last decides soundness,
+and the `SafeTr` half can be completed in safe code. Classify as follows.
+
+Bad:
+
+1.  The unsafe trait is dyn-compatible. Downstream safe code may write:
+
+    ```rust
+    trait Sub: UnsafeTr {}
+    impl SafeTr for dyn Sub { // impl that behaves incorrectly }
+    ```
+    `dyn Sub: UnsafeTr` holds via the built-in supertrait impl; no `unsafe`
+    appears downstream. Reject the contract as designed unless the defining
+    crate owns a blanket `impl<T: UnsafeTr + ?Sized> SafeTr for T` (making
+    every such downstream impl a coherence error), or the unsafe trait is
+    non-dyn-compatible *by construction* — an explicit dyn-incompatible
+    supertrait or other property that would be a semver-breaking-change
+    to remove. A bare marker trait is dyn-compatible by default.
+
+2.  A blanket `unsafe impl` over a `#[fundamental]` constructor:
+
+    ```rust
+    unsafe impl<T: UnsafeTr> UnsafeTr for Box<T> {}
+    ```
+
+    No party can discharge this. A downstream crate owning `Local` may
+    soundly write `unsafe impl UnsafeTr for Local` (vacuous: `Local` has no
+    `SafeTr` impl) and then, because `Box` is fundamental, legally write
+    `impl SafeTr for Box<Local>` in safe code. `Box<Local>: UnsafeTr +
+    SafeTr` now violates a contract that no single impl broke. Reject
+    fundamental blankets under a conditional cross-trait contract unless the
+    defining crate owns the matching safe-trait blanket for the same coverage
+    (`impl<T: UnsafeTr> SafeTr for Box<T>`).
+
+Iffy (accept, with an explicit label):
+
+3.  Coherence-based negative reasoning about a concrete local type:
+
+    ```rust
+    // dyn-incompatible; same safety requirements.
+    unsafe trait UnsafeTr: Sized {}
+
+    // SAFETY: `ExampleStruct` has no `SafeTr` impl in this crate, and
+    // the orphan rule prevents any other crate from adding one, so the
+    // conditional obligation is vacuous.
+    unsafe impl UnsafeTr for ExampleStruct {}
+    ```
+
+    Sound today, but only because current coherence rules forbid the
+    downstream impl. The orphan rule exists to make enforcing coherence easier,
+    but it is not a stated soundness guarantee, and active proposals would weaken
+    it. Accept only when cases 1 and 2 are absent (non-dyn-compatible unsafe trait,
+    no fundamental blankets) and the premise is flagged as orphan-rule-reliant so it
+    can be found and re-audited if coherence rules change. Flag as fragile
+    and prefer a restructuring below.
+
+Good:
+
+-   Move the constrained behavior into the unsafe trait itself, so each
+    `unsafe impl` carries the obligation directly (such as by making `SafeTr`
+    a supertrait, or tying the constrained behaviour to an unsafe marker
+    trait which is a subtrait of both).
+-   Validate dynamically before unsafe reliance (check the returned value,
+    then use the checked value).
+-   Have the defining crate own the safe trait's impl for the entire
+    `T: UnsafeTr + ?Sized` coverage, closing the impl set by coherence.
+-   Seal the safe trait, with sealing airtight per the sealing rule.
+
 ## Criteria for safety comments
 
 A safety comment (e.g., using `// safety:`, `// SAFETY:`, or doc comment