Support impl Trait in attribute name interpolation

[jschneider-bensch]

If we have a signature like this

pub(crate) fn kem_keygen(
    alg: KemScheme,
    rng: &mut (impl CryptoRng + RngCore),
) -> Result<(KemSk, KemPk), TLSError>

it would be good to be able to refer to $:{impl CryptoRng + RngCore) when using e.g. proverif::replace.

---

We want to be able to write the following kind of code:

trait Foo: Bar {...}
fn f<T: Foo>(x: T) {
   fstar!("$<some syntax>{T as Bar}")
}

The bit $<some syntax>{T as Bar} should produce a impl. expression path in F*, in this case probably something like i1._super_HASH.

[W95Psp]

I think you can use the following as workaround:

pub(crate) fn kem_keygen<R: CryptoRng + RngCore>(
    alg: KemScheme,
    rng: &mut R,
) -> Result<(KemSk, KemPk), TLSError>

Then you'll be able to use $:{R}.

Example in the playground:

trait Rng {}

fn f<T: Rng>(rng: &mut T) {
    hax_lib::proverif!("$:{T}");
}

Open this code snippet in the playground

[jschneider-bensch]

This should work, at least for cases where only the impl trait is passed around:

trait Rng {}

fn f<T: Rng>(rng: &mut T) {
    hax_lib::proverif!("$:{T}");
}

fn g<T: Rng>(rng: &mut T) {
    f(rng)
}

Playground

ProVerif needs the types to have the same names, so it wouldn't work if we actually instantiate the type:

trait Rng {}

fn f<T: Rng>(rng: &mut T) {
    hax_lib::proverif!("$:{T}");
}

fn g<T: Rng>(rng: &mut T) {
    f(rng)
}

struct R;
impl Rng for R {}

fn h() {
    g(&mut R)
}

Playground

Here, the concrete type is playground__t_R which PV won't be able to match to v_T.

The other issue is that the PV backend does not yet do it's translation of Rust types to PV types for generics.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[maximebuyse]

Still relevant, @W95Psp can you check if it is a duplicate?

[W95Psp]

Done, there was another issue, but more recent, so I closed that other one.

[karthikbhargavan]

Still needed.

[W95Psp]

Here are some notes about this issue.

Context

We would like to be able to capture impl. expressions in quoted F* (or Coq, Lean, whatever.).

Implementations have no names and are implicit in Rust.

Thus we can’t denote them.

However, implementation expressions are the solution to a trait obligation, and Rust has a syntax for trait obligations: <SomeType as SomeTrait>.

Goal

Add a convenience syntax in the quoting macros to generate impl. expressions, e.g.:

fn f<T: Clone>(x: T) {
   // here, we would like to capture
   // `<T as Clone>`
   fstar!("($impl{<T as Clone>}).f_clone")
}
// should produce something like `(i1).f_clone`

How to implement?

Given a goal <MyType<M1, ..., Mn> as TheTrait<T1, ..., Tm>>, we generate the following, locally:

let _impl_expr = {
// The UUID is generated
#[hax_lib::associated_item(0f46abbe-c101-4d57-bcad-9b465291783c)]
// We include whatever M1..Mn type that appear in Bounds
// Bounds is the union of all bounds we can find on the parent item(s)
// The generics are the union of all generics on parent item(s), stripping unused ones (looking at Bounds)
trait<generics> Helper: TheTrait<T1, ..., Tm> where Bounds {}
impl<generics> TheTrait<T1, ...Tm> for MyType<M1, ..., Mn> {}
	"0f46abbe-c101-4d57-bcad-9b465291783c"
};

This will be parsed in the engine

[Nadrieril]

The stripping of unused parameters is necessary but not trivial. I'm thinking you could avoid that by making Helper depend on these generics:

#[hax_lib::associated_item(0f46abbe-c101-4d57-bcad-9b465291783c)]
// We include whatever M1..Mn type that appear in Bounds
// Bounds is the union of all bounds we can find on the parent item(s)
// The generics are the union of all generics on parent item(s)
trait<generics> Helper<generics>: TheTrait<T1, ..., Tm> where Bounds {}
impl<generics> Helper<generics> for MyType<M1, ..., Mn> {}

[W95Psp]

Ah, yeah, that will probably be fine indeed! I will play with it :)

From our last conversation on that topic: I tried numerous ugly hacks to capture ambient generics, but I could not make anything work sadly!