interaction between TAIT and const generics is unsound

[lcnr]

We consider the following pattern to be sound afaik:

mod prove_outlives {
    use std::marker::{PhantomData};
    #[derive(Copy, Clone, PartialEq, Eq)]
    pub struct OutlivesProof<'a, 'b>(PhantomData<*mut (&'a (), &'b ())>);
    impl<'a: 'b, 'b> OutlivesProof<'a, 'b> {
        pub const fn mk() -> Self {
            OutlivesProof(PhantomData)
        }
    }
    impl<'a, 'b> OutlivesProof<'a, 'b> {
        pub fn apply(self, x: &'a str) -> &'b str {
            // SAFETY: We've required `'a: 'b` when constructing the
            // proof object and both regions are invariant.
            unsafe { std::mem::transmute(x) }
        }
    }
}

now consider the following entirely safe code:

pub use prove_outlives::*;
// We're using const generics to move a `OutlivesProof` object into the type
// system so that we never have to actually call the defining function to use
// this proof.
struct ConstOutlives<'a, 'b, const PROOF: OutlivesProof<'a, 'b>>(Option<*mut (&'a (), &'b ())>);
trait Cast<'a, 'b> {
    fn cast(x: &'a str) -> &'b str;
}
impl<'a, 'b, const PROOF: OutlivesProof<'a, 'b>> Cast<'a, 'b> for ConstOutlives<'a, 'b, PROOF> {
    fn cast(x: &'a str) -> &'b str {
        PROOF.apply(x)
    }
}

const PROOF<'a: 'b, 'b>: OutlivesProof<'a, 'b> = OutlivesProof::mk();
type Opaque<'a, 'b> = impl Cast<'a, 'b>;
#[define_opaque(Opaque)]
fn mk<'a: 'b, 'b>() -> Option<Opaque<'a, 'b>> {
    None::<ConstOutlives<PROOF>>
}

fn transmute_static<'a>(x: &'a str) -> &'static str {
    Opaque::cast(x)
}

Ignore which unstable features would be required for this and the changes required for ConstOutlives to be a valid const parameter type. This would cause the above pattern to be unsound.

More generally: we currently support using values as proof of type system invariants. However, this relies on the assumption that if the invariants hold while computing the value, they will also hold when using it.

TAIT breaks this assumption. We only require the final returned value to be well-formed in case the TAIT is defined by a function which has stronger constraints than the TAIT itself. This means if the final value contains a const parameter of a type where the invariants are only checked by the constructor, TAIT allows using this value without proving them.

cc @rust-lang/types @RalfJung I've got 3 questions here:

• do we consider the prove_outlives module to be a safe abstraction (pretty sure yes)
• is there any principled reason why the above exploit via TAIT should error except by forbidding defining scopes with stronger requirements than the TAIT itself (i can't think of any)
• do we already have this issue with RPIT[IT] (i assume no, they don't allow weakening constraints)

I don't think keeping such types out of const generics is desirable, so IMO this issue is strongly on the TAIT side.

[lcnr]

A likely more contentious example which uses name privacy instead of const generics:

• The abstraction in prove_outlives is already unsound due to Normalization can skip WF #100041

#![feature(type_alias_impl_trait)]

// Should this be a safe abstraction?
pub mod prove_outlives {
    pub trait MakeProof<'a, 'b> {
        type Proof: Proof<'a, 'b>;
    }
    #[allow(unused)]
    mod private {
        struct Inv<'a>(*mut &'a ());
        pub struct Proof<'a, 'b>(Inv<'a>, Inv<'b>);
    }
    pub trait Proof<'a, 'b> {
        fn cast(x: &'a str) -> &'b str;
    }
    impl<'a, 'b> Proof<'a, 'b> for private::Proof<'a, 'b> {
        fn cast(x: &'a str) -> &'b str {
            // SAFETY: The only way to name `private::Proof` is via
            // `MakeProof` which requires `'a: 'b`.
            unsafe { &*(x as *const str) }
        }
    }
    impl<'a: 'b, 'b> MakeProof<'a, 'b> for () {
        type Proof = private::Proof<'a, 'b>;
    }
}
use prove_outlives::*;

type Opaque<'a, 'b> = impl Proof<'a, 'b>;
#[define_opaque(Opaque)]
fn define<'a: 'b, 'b>() -> Option<Opaque<'a, 'b>> {
    None::<<() as MakeProof<'a, 'b>>::Proof>
}

fn transmute_static<'a>(x: &'a str) -> &'static str {
    Opaque::cast(x)
}
fn main() {
    let s = {
        let temp = String::from("temporary");
        transmute_static(&temp)
    };
    println!("{s}");
}

[RalfJung]

prove_outlives (the original form in the first post) looks legit, I agree.

Nice catch!