final trait default methods

[jonhnet]

In porting our marshaller from Dafny to Verus, I've encountered a pattern I can't reproduce. In the Dafny code, a "superclass" defines some predicates and some default methods whose implementations depend on the definitions of those predicates.

In the translation, the predicate becomes a trait default spec fn and the method becomes a trait default exec fn. The same trick doesn't work, however, because in verifying the exec fn, Verus doesn't know that the spec fn's meaning hasn't been overridden by the trait's impl. (I'm not entirely sure why the analogous definitions in Dafny are sound -- maybe it knows which proofs depend on redefining which predicates? Maybe it's unsound? 😨 )

If there were a way to mark a trait default fn as final -- presumably spec fns -- then other trait defaults could rely on those definitions in their proofs.

[jaybosamiya-ms]

Rust doesn't have a way to define final default functions, but you can work around it by introducing another (extension) trait that exists whenever the base trait exists---defining the extension's implementation as fully parametric in the type, restricted only by the original trait.

Specifically, something like (Playground link):

trait Foo {
    // this is the trait where you wanted `final bar`
    spec fn baz(&self) -> nat;  // a normal trait method

}

trait FooFinalExt {
    spec fn bar(&self) -> int;
}
impl<T: Foo> FooFinalExt for T {
    spec fn bar(&self) -> int {
        // the actual final function you wanted
        (self.baz() + 1337) as int
    }
}

proof fn test<T: Foo>(x: T) {
    assert(x.bar() >= 1337);
}

struct FooFighters {}
impl Foo for FooFighters {
    spec fn baz(&self) -> nat {
        30_000
    }
}

proof fn test2(x: FooFighters) {
    // Testing that if you know more about the type, you can learn more than just the definition of `bar`
    assert(x.bar() >= 31337);
}

That way, anywhere you know Foo, as long as there is a FooFinalExt is in scope (this is the one downside to this, you need to remember to add the use ... declaration), you also magically get the non-overrideable definition for bar and can depend on its value.

[jonhnet]

Wow, that's clever! I'll give that a spin. Thank you!