Typesystem soundness hole involving cyclically-defined associated type in trait, and normalization in trait bounds

View all comments

This isn't quite trivial, but well… it works.

a “transmute” in safe Rust:

fn main() {
    let s: String = transmute(vec![65_u8, 66, 67]);
    println!("{s}"); // ABC
}

fn transmute<L, R>(x: L) -> R {
    transmute_inner_1::<L, R, RewriteReflRight<FakeRefl<L, R>>>(x)
}

fn transmute_inner_1<L, R, P: TyEq<LHS = L, RHS = R>>(x: L) -> R {
    transmute_inner_2::<<P::ProofIsProofValue as TyEq>::ProofDef, L, R, P::ProofValue, P>(x)
}

fn transmute_inner_2<Rw, L, R, Actual, P: TyEq<LHS = L, RHS = R, ProofValue = Actual>>(x: L) -> R
where
    <Rw as TypeIs<P::ProofValue>>::Is: TyEq<LHS = L, RHS = R>,
{
    transmute_inner_3::<L, R, Actual>(x)
}

fn transmute_inner_3<L, R, P: TyEq<LHS = L, RHS = R>>(x: L) -> R {
    transmute_inner_4::<R, P::ProofDef>(x)
}

fn transmute_inner_4<R, Rw>(x: <Rw as TypeIs<R>>::Is) -> R {
    x
}

trait TypeIs<T> {
    type Is;
}
impl<_Self, T> TypeIs<T> for _Self {
    type Is = T;
}

trait TyEq: TyEqImpl {
    type ProofDef: TypeIs<Self::RHS, Is = Self::LHS>;
}

trait TyEqImpl {
    type LHS;
    type RHS;

    type Proof<_Dummy>: TyEq<LHS = Self::LHS, RHS = Self::RHS>;

    type ProofValue;
    type ProofIsProofValue: TyEq<LHS = Self::Proof<()>, RHS = Self::ProofValue>;
}

trait DeriveEqFromImpl {}
impl<P: TyEqImpl + DeriveEqFromImpl> TyEq for P {
    type ProofDef = <P::Proof<()> as TyEq>::ProofDef;
}

struct Refl<T>(T);
impl<T> TyEqImpl for Refl<T> {
    type LHS = T;
    type RHS = T;

    type Proof<_Dummy> = Refl<T>;

    type ProofValue = Refl<T>;
    type ProofIsProofValue = Refl<Refl<T>>;
}
impl<T> TyEq for Refl<T> {
    type ProofDef = ();
}

struct FakeRefl<L, R>(L, R);
impl<L, R> DeriveEqFromImpl for FakeRefl<L, R> {}
impl<L, R> TyEqImpl for FakeRefl<L, R> {
    type LHS = L;
    type RHS = R;

    type Proof<_Dummy> = FakeRefl<L, R>;

    type ProofValue = FakeRefl<L, R>;
    type ProofIsProofValue = Refl<FakeRefl<L, R>>;
}

struct RewriteReflRight<P>(P);
impl<P> DeriveEqFromImpl for RewriteReflRight<P> {}
impl<P, L, R> TyEqImpl for RewriteReflRight<P>
where
    P: TyEq<LHS = L, RHS = R>,
{
    type LHS = L;
    type RHS = R;

    type Proof<_Dummy: RewriteReflRightHelper> = _Dummy::RewriteRight<Refl<L>, R, P::ProofDef>;

    type ProofValue = Refl<L>;
    type ProofIsProofValue = Refl<Refl<L>>;
}

trait RewriteReflRightHelper {
    type RewriteRight<P, R, Rw>: TyEq<LHS = P::LHS, RHS = R>
    where
        P: TyEq<RHS = <Rw as TypeIs<R>>::Is>;
}

impl<_Dummy> RewriteReflRightHelper for _Dummy {
    type RewriteRight<P, R, Rw>
        = P
    where
        P: TyEq<RHS = <Rw as TypeIs<R>>::Is>;
}

(playground)

Besides this unsoundness, there are also many ICEs. This isn't surprising, since we're not really transmuting, but rather sort-of … convincing the type system that the 2 types were never different in the first place.

fn main() {
    let s: u8 = transmute(());
    println!("{s:?}");
}

Or interesting LLVM-errors

fn main() {
    let s: &() = transmute("hi");
    println!("{s:?}");
}

   Compiling playground v0.0.1 (/playground)
Invalid bitcast
  %7 = bitcast { ptr, i64 } %6 to ptr, !dbg !425
in function _ZN10playground17transmute_inner_317h363424402e6a7153E
rustc-LLVM ERROR: Broken function found, compilation aborted!
error: could not compile `playground` (bin "playground")

Oh… that one on nightly has… the compiler itself execute a SIGILL? (Is that actual UB in the compiler!? Or UB in LLVM? Or can SIGILL be part of a deliberate crash condition?)

From a background of “this works a bit like Coq”, the relevant parts that make this work is how:

• FakeRefl<L, R> is a “proof” that L and R are the same types, which doesn't terminate (i.e. it is cyclically defined in terms of itself)
  • unlike true proof assistants, Rust's trait system does allow some stuff to be defined in a somewhat cyclical manner, especially pre-monomorphization
• overflow during monomorphization is avoided anyways by:
  • introducing the Rewrite… step which rewrites Refl<L> (a proof of TyEq<LHS = L, RHS = R>) using this FakeRefl proof
  • at the same time also tracking that the proof term itself doesn't actually change with the rewrite
  • using this tracked meta-information in order to eliminate the usage of FakeRefl before its (indirectly and cyclically defined) ProofDef type ever ends up being instantiated

Of course, this is just my intuitive description from a user perspective :-)

I have no idea which part of this code to blame exactly. Perhaps someone else with better knowledge of the theory behind Rust's typesystem and trait system could have a better clue here.

I'm not quite sure if this can perhaps be "simplified" to remove the need for GATs

Update: It can be "simplified" to remove the need for GATs. (playground)

Update2: It's even possible to rework this into working since Rust 1.1

type Proof<_Dummy: RewriteReflRightHelper> = _Dummy::RewriteRight<Refl<L>, R, P::ProofDef>;

type Proof<_Dummy: RewriteReflRightHelper>

type Proof<_Dummy>: TyEq<LHS = Self::LHS, RHS = Self::RHS>;

This is not a regression. It also isn't influenced by -Znext-solver.

This is a relatively clean typesystem hole, on stable Rust, without many of the other known-problematic features such as HRTBs, lifetimes, variance, trait objects, or implicitly defined trait impls for functions/closures/etc…

@rustbot label I-unsound, I-ICE, I-crash, T-types, A-type-system, A-trait-system, A-associated-items

related issues

• https://github.com/rust-lang/rust/issues/149898

Start by reproducing the stable playground example and the linked ICE and LLVM-error cases, then compare behavior with nightly and -Znext-solver as described in the issue. Trace the cyclic associated-type normalization through Rust's type-system and trait-system components; done means the safe transmute, compiler crashes, and invalid LLVM output no longer occur.