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.

[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.