Add external_trait_extension feature to extend external traits with spec functions

[Chris-Hawblitzel]

This implements the proposal in #1618 , with some minor changes. Given an external trait:

trait T {
    fn e(&self, u: u8);
}

You can declare an external trait specification that extends T with additional spec functions that are held in a new trait TSpec:

#[verifier::external_trait_specification]
#[verifier::external_trait_extension(TSpec)]
pub(crate) trait ExT {
    type ExternalTraitSpecificationFor: T;
    spec fn r(&self, u: u8) -> bool;
    fn e(&self, u: u8)
        requires self.r(u);
}

The syntax macro generates additional internal declarations for this:

pub(crate) trait TSpec: T {
    spec fn r(&self, u: u8) -> bool;
}
#[verifier::external]
pub(crate) trait VERUS_SPEC__TSpec: T {
    fn r(&self, u: u8) -> bool;
}
#[verifier::external]
#[verus::internal(external_trait_blanket)]
impl<A: T + ?Sized> TSpec for A {
    fn r(&self, u: u8) -> bool { panic!() }
}

A program can then implement T and TSpec, where the syntax macro will internally rename impl TSpec to impl VERUS_SPEC__TSpec to avoid conflicting with the blanket impl shown above:

impl T for u32 {
    fn e(&self, u: u8) {
    }
}

#[verifier::external_trait_extension]
impl TSpec for u32 {
    spec fn r(&self, u: u8) -> bool {
        u < 100
    }
}

In VIR, impl VERUS_SPEC__TSpec is renamed back into impl TSpec, so that the impl provides an implementation for the otherwise uninterpreted spec function TSpec::r. If Rust's trait coherence rules are an obstacle, a program can also just provide axioms about the uninterpreted spec function TSpec::r.

In VIR's call graph, T and TSpec are merged together so that T's associated types, TSpec's spec functions, and T's exec functions are treated as if they had been declared together in a single trait in the first place when checking for cycles in the call graph. This allows T's exec functions to refer to TSpec's spec functions in requires/ensures and allows TSpec's spec functions to refer to T's associated types.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[tjhance]

Great to see this.

i'm a little confused about how this merging works. are the spec functions added to the vir TraitX object?

[Chris-Hawblitzel]

are the spec functions added to the vir TraitX object?

They are not. T and TSpec are separate traits in VIR, AIR, and SMT. It's just the call graph Nodes that are merged for termination checking. If it weren't for termination checking, no merging would be needed.

[utaal]

[retreat 2025] it may be useful to refer to #1465

[utaal]

• @utaal: consider whether it would be better to avoid magic renaming via external_trait_extension.

[Chris-Hawblitzel]

• @utaal: consider whether it would be better to avoid magic renaming via external_trait_extension.

I've gone back and forth on this. In the original proposal ( #1618 ), there was no magic renaming. Instead, the programmer explicitly named the third trait (e.g. TSpecImpl) and used that name in the impl:

#[verifier::external_trait_specification]
#[verifier::external_trait_extension(TSpec, TImplSpec)]
pub(crate) trait ExT {
...
}
impl TImplSpec for u32 {
...
}

One thing that bugged me about this is that the impl above doesn't mention TSpec, which obscures the purpose of the impl, which is to provide an implementation of TSpec. This is one reason I shifted to the implicit renaming in the pull request:

#[verifier::external_trait_extension]
impl TSpec for u32 {
...
}

This implicit renaming, though, also has drawbacks, particularly if you have to use the hidden name.

Would it be better to be more verbose? For example, would it be better to have no implicit renaming, and to require that the programmer repeat the entire #[verifier::external_trait_extension(TSpec, TImplSpec)] attribute in the impl to make it clearer that the impl is using TImplSpec to implement TSpec? For example:

#[verifier::external_trait_specification]
#[verifier::external_trait_extension(TSpec via TImplSpec)]
pub(crate) trait ExT {
...
}
#[verifier::external_trait_extension(TSpec via TImplSpec)]
impl TImplSpec for u32 {
...
}

[Chris-Hawblitzel]

• @utaal: consider whether it would be better to avoid magic renaming via external_trait_extension.

I decided to remove the magic renaming and go with:

#[verifier::external_trait_specification]
#[verifier::external_trait_extension(TSpec via TImplSpec)]
trait ExT {
...
}

impl TImplSpec for u32 {
...
}

This was the simplest alternative.