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

[steffahn]

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

(this section has become somewhat outdated due to this update, click to expand anyway)

I'm not quite sure if this can perhaps be "simplified" to remove the need for GATs; however, I wasn't able to the Rewrite… stuff to work without this trick

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

where the (vacuous) _Dummy: RewriteReflRightHelper restriction prevents the compiler from already knowing the concrete RewriteReflRightHelper impl. (If you worry about the syntactical mismatch of

type Proof<_Dummy: RewriteReflRightHelper>

here vs

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

without bounds on _Dummy in the trait definition: that's actually avoidable (<- see this playground on how the bound can be repeated everywhere and the impl RewriteReflRightHelper for … can even be for a concrete type only).

So for now, I would conjecture that this soundness hole does require GATs.

Edit: I completely forgot about the (generous) usage of GATs inside of RewriteReflRightHelper ~ so, yes, GATs seem fairly integral to this.

Edit2: Nevermind, those can all be eliminated leaving only a single GAT.

(end of somewhat outdated section)

---

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

[saethlin]

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?)

With LLVM assertions enabled, I get this instead of just a SIGILL:

rustc: /checkout/src/llvm-project/llvm/lib/IR/Instructions.cpp:2974: static CastInst *llvm::CastInst::Create(Instruction::CastOps, Value *, Type *, const Twine &, InsertPosition): Assertion `castIsValid(op, S, Ty) && "Invalid cast!"' failed.

and if I pass -Zverify-llvm-ir, I get the same nice error:

Invalid bitcast
  %5 = bitcast { ptr, i64 } %4 to ptr
rustc-LLVM ERROR: Broken module found, compilation aborted!

I believe the difference you're observing on nightly is #133499 cc @nikic

Oh oops, we document that IR is not verified by default, so it's definitely intentional that on nightly we crash somewhat incoherently with invalid IR.

[apiraino]

@steffahn Can you (or anyone else having context here) please provide a digestible summary of this issue? What is happening that shouldn't?

This is not a more recent regression (i.e. it "works" ever since GATs were introduced). It also isn't influenced by -Znext-solver.

By reading this sentence I infer that it's not a simple regression. Would you like the appropriate team to discuss this?

Thank you from the triage.

[workingjubilee]

It's not really a regression at all in the conventional sense.