Extending external_trait_specification with spec functions

[Chris-Hawblitzel]

@ziqiaozhou @tjhance @utaal This is a follow-up to #1527 and discussions that we've had in meetings. It is relevant to #1465 and #1569 .

We often write Verus traits with a mixture of exec and spec functions:

trait T {
    spec fn r(&self, u: u8) -> bool;
    fn e(&self, u: u8)
        requires self.r(u);
}

However, if the trait is an external trait, such as an std library trait like PartialOrd or Add, then the trait will not have any spec functions in it, making it harder to declare requires and ensures for the exec functions in the trait. To overcome this limitation, we've previously discussed approaches to extend existing traits with additional ghost functions. Here, I will detail a proposal to implement such an approach. I'll only consider spec functions, leaving proof functions for future work.

Suppose we have an external trait T with an exec function e:

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

Suppose we allow the external_trait_specification to extend T with additional spec functions as follows:

#[verifier::external_trait_specification(TSpec, TImplSpec)]
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 could generate the following additional traits and trait impls from the ExT declaration:

pub(crate) trait TImplSpec: T {
    spec fn r(&self, u: u8) -> bool;
}
pub(crate) trait TSpec: T {
    spec fn r(&self, u: u8) -> bool;
}
impl<A: T + ?Sized> TSpec for A {
    uninterp spec fn r(&self, u: u8) -> bool;
}

TSpec::r is an uninterpreted function that represents all implementations of T::r. There would be two ways to define TSpec::r for various types that implement T: (1) a verified way based on trait implementations, and (2) an unverified way based on user-supplied axioms. When Rust's trait coherence rules can be satisfied, (1) is better, but in case Rust's trait coherence rules are an insurmountable obstacle, (2) is available as a backup strategy.

For (1), a user simply implements TImplSpec along with T:

impl T for u32 {
    fn e(&self, u: u8) {
    }
}
impl TImplSpec for u32 {
    spec fn r(&self, u: u8) -> bool {
        u < 100
    }
}

Verus would emit an axiom saying that TSpec always agrees with TImplSpec. It would be equivalent to the following broadcast (although it would be an internal axiom, not a named broadcast function):

// Would be an internal axiom, not a named broadcast function
pub(crate) broadcast proof fn broadcast_TImplSpec<A: TImplSpec + ?Sized>(_self: &A, u: u8)
    ensures
        #![trigger <A as TSpec>::r(_self, u)]
        #![trigger <A as TImplSpec>::r(_self, u)]
        <A as TSpec>::r(_self, u) == <A as TImplSpec>::r(_self, u)
{
    admit();
}

User functions can then use T and TSpec:

fn test(x: u32) {
    assert(x.r(20));
    x.e(20);
}

Although T, TSpec, and TImplSpec appear as separate traits to Rust's type system, Verus would group them together internally in VIR. By doing this, Verus would prohibit circular definitions such as the following:

impl TImplSpec for u32 {
    spec fn r(&self, u: u8) -> bool {
        !<u32 as TSpec>::r(_self, u) // ERROR
    }
}

Here, <u32 as TSpec> would depend on impl<A: T + ?Sized> TSpec for A with A = u32, which would in turn depend on u32: T. If, for example, we set up an internal dependency of u32: T on u32: TImplSpec, we can catch the circular definition.