Traits

[Chris-Hawblitzel]

When we support traits, we'll need:

• a place to put the requires/ensures of the methods in the traits
• a way to coordinate requires/ensures between trait method declarations and method implementations

We can put the trait method requires/ensures in a dummy default method:

trait T {
    fn foo(&self) {
        requires(...);
        ensures(...);
        no_method_body()
    }
}

When the ghost code eraser sees no_method_body(), it will erase the method body, leaving fn foo(&self);.

Trait method implementations inherit the requires/ensures of the trait method declarations. It is sound to allow implementations to weaken the requires or strengthen the ensures. We can consider various policies for how this inheritance works:

1. The implementation inherits the declaration's requires/ensures exactly, with no modifications.
2. The implementation can "or" the requires (inherited_requires || additional_requires) and "and" the ensures (inherited_ensures && additional_ensures).
3. The implementation can redeclare all the requires or ensures from scratch, and we have an additional check that the new requires are weaker than the inherited requires and that the new ensures are stronger than the inherited ensures.

We could also have some combination of 1, 2, and 3.

Strictly speaking, 1 is all we need, because the requires/ensures declared by the trait can call out to spec methods that the implementation can override:

trait T {
    #[spec]
    fn f1(self) -> bool;

    #[spec]
    fn f2(self) -> bool;

    fn foo(&self) {
        requires(self.f1());
        ensures(self.f2());
        no_method_body()
    }
}

One example that we'll encounter right away is the Index trait. In this case, I think it would be most flexible to have the requires/ensures call out to spec methods, as in the code shown above. Otherwise, the declared requires/ensures might just be a placeholder that's not very useful on its own, like requires(false); ensures(true), which would then be overridden via the approaches described in 2 or 3.

I'm advocating approach 1, particularly for the initial implementation. It's the simplest approach and it encourages programmers to factor their specifications into spec methods for maximum flexibility.

[utaal]

I like the overall approach here. Something that I'm trying to wrap my head around is what this means and what impact this has for those trait in rust that are used to control specific language features (Deref, DerefMut, Index, ...). In my experience these are very rarely used as trait bounds, which makes the requires/ensures in the trait definition maybe less desirable.

Index is one such trait; the impl for Vec has something specific to say about the implementation:

impl<T> Index<usize, Output=T> for Vec<T> {
  fn index(&self, idx: usize) -> &T {
    requires(idx < self.len());
    ensures(|res: &T| self.view().index(idx) == res);
...
  }
}

and similarly, but with a more complicated spec for IndexMut:

impl<T> IndexMut<usize, Output=T> for Vec<T> {
  fn index_mut<'a>(&mut self, idx: usize) -> &'a mut T {
    requires(idx < self.len());
    ensures(|res: &mut T| old(self).view().index(idx) == res);
    // and, hypothetically,
    after<'a>(|ref: &mut T| {
      ensures(self.view() == old(self).view().set(idx, *ref))
    })
  }
}

Of course the design for traits may influence decisions on returning mutable references, or viceversa, depending on what ends up making the most sense in general.

For this reason, I was considering whether it would make sense to consider an approach where, for some traits (mostly those that control language features), one does not provide requires/ensures on the trait definition, but they only provide one for each implementation (in the impl _ for _ block). This would mean that for some traits, the dispatch of VCs is always "static", i.e. it requires knowing the concrete type -- which is, in my experience, very often the case for things like Index. Choosing to only allow the spec on the implementation would also remove the need for additional checks that the impl requires and ensures are compatible (substitution principle) with the trait (as there's no requires/ensures on these traits).

---

Now, it's entirely possible these trait can also be defined and implemented using the approach Chris describes, but I'm not clear about the strategy to refer to spec functions for the requires/ensures.

Do we imagine we will redefine Index with additional spec functions for the requires and the ensures?

Are we concerned about the existing implementations of these traits in the standard library? We need to make sure these implementors may inherit trait requires/ensures.

---

To be clear, I like the fact that Chris' proposal is very consistent, and I'm trying to figure out how it would handle cases where traits could use a tailored requires/ensures.

I think what I'm trying to tease apart here is that I think traits have two uses in rust:

• writing generic code that can be used with different types that coherently implement a trait;
• as a way to define the behavior of operators, auto-deref, and Drop for user's types, in addition to being used as a way to have extension methods for a certain type which become available only when the trait that declares them is imported.

I'm wondering if these two uses warrant two different interactions with the verifier.

[utaal]

One additional note specifically about Index.

In the strategy of referring to #[spec] functions for the requires and ensures, if we had a View trait that defined a type View and a #[spec] fn view(&self) -> View, then it may be possible to define the Index trait's index pre and postconditions in terms of self.view().index() and self.view().contains() (this would require additional trait bounds that ensure that the View type has index() and contains(), or something like that.

[tjhance]

I think Chris's suggestion for having a 'spec' method that is used by the requires/ensures make sense. If I understand it correctly, the suggestion is that index(i) will have a precondition like is_valid_index(i). Any given type that implements Index would give the definition for is_valid_index(i) (for a Vec it would be something like 0 <= i < vec.len(). Then we could also write functions which are generic over T: Index, using is_valid_index in its spec if necessary. I think this makes sense. Though like Andrea said, Index is rarely used a trait bound, but I think this logic would probably hold up very well for other traits.

Like Andrea, I was too was wondering about how exactly we would "redefine" Index to have this extra spec function.

Drop presents its own challenges. (Although we probably don't need to figure them out for the first implementation of traits.) I imagine it's very common for code to attempt to drop variables of generic type T. But I presume we will want to allow types to add their own pre-conditions to drop (possibly through a similar spec function trick). In this case, we would have to disallow dropping everywhere unless we can prove it's safe.

[Chris-Hawblitzel]

We don't yet have a way to add extra spec functions to existing Rust types/traits. I'm assuming that we'll eventually want this for other reasons, such as adding a .view() spec function to existing Rust collection types. But in the meantime, static dispatch for Index would be a simple alternative. I think this would just mean that even though the Index trait is used to type check Rust HIR, the Index trait wouldn't exist in VIR. Instead, there would be various unrelated implementations of a method named "index", each with their own requires and ensures. The SMT encoding wouldn't need to know that they were originally related during type checking. With this static dispatch, we wouldn't yet be able to support dynamic method calls to index via the trait bound A: Index, but that's probably ok for now. We're mainly interested in Index for the [] syntax, not for the trait behavior.

[utaal]

adding a .view() spec function to existing Rust collection types.

Side-note: I think this could (should?) be done with a View trait.

[utaal]

The static dispatch for Index is I think what I was advocating for Index and similar traits that control language features such as [], and it's already partly implemented: the VIR treats the implemented trait functions as if they were regular impls (and additionally tracks the defining traits, just to disambiguate between functions that are defined by different traits but have the same name). As Chris is saying, the Index trait doesn't then exist in VIR, and in the SMT encoding there's no information that the impls were related during type-checking.

We can start (as it may already be the case now) by special-casing Index, and if other traits where this encoding makes sense we can considering e.g. adding an attribute to mark them.

We're mainly interested in Index for the [] syntax, not for the trait behavior.

Yep. (This is the part of this feature that isn't quite complete, I need to map [] to Index properly as IIRC it's not desugared in the HIR.)

[utaal]

Again, I generally think the design Chris is proposing is elegant and should cover the majority of uses. Another thing that came to mind (but I haven't thought about it carefully yet) is how it interacts with potential blanket trait implementations, e.g.

trait Something<T> {
  #[spec] fn some_fn(&self) -> bool { ... }
}

impl<T> Something for T where T: SomeOtherTrait {
  #[spec] fn some_fn(&self) -> bool { ... }
}

or, e.g.

impl<T> Something for Rc<T> {
  #[spec] fn some_fn(&self) -> bool { ... }
}

We could obviously disallow these, to start.

[tjhance]

What do you mean by "blanket trait implementation"? I don't see what's notable about the examples here.

[utaal]

T here is not a stand in for a concrete type, it's an universally quantified type variable; i.e. the impl of Something is for all T for which T: SomeOtherTrait. Does that clarify? Or am I misunderstanding the question?

So-called "blanket impls" are described here, https://doc.rust-lang.org/book/ch10-02-traits.html#using-trait-bounds-to-conditionally-implement-methods

[tjhance]

Yeah, I gotcha now.

[Chris-Hawblitzel]

One other related topic: we have to ensure that proof/spec trait methods terminate. It's very easy to write nonterminating trait methods in Rust. Here's an example infinite loop:

trait T {
    fn f(&self);
}

fn rec<A: T>(x: &A) {
    x.f();
}

struct S {
}

impl T for S {
    fn f(&self) {
        rec(self);
    }
}

fn main() {
    let s = S {};
    s.f();
}

Here's another infinite loop:

trait T {
    fn f<A: T>(&self, x: &A);
}

struct S {
}

impl T for S {
    fn f<A: T>(&self, x: &A) {
        x.f(x)
    }
}

fn main() {
    let s = S {};
    s.f(&s);
}

Coq and F* support type classes while still ensuring termination. I propose to follow their approach. (See https://coq.inria.fr/refman/addendum/type-classes.html for more information.) The key idea is that in Coq/F*, traits / type classes are just built out of ordinary datatypes and function types, so the rules for termination for datatypes and function types ensure that traits / type classes also terminate. A trait with methods m1...mn is encoded as a "dictionary" datatype containing fields f1...fn, where each field is a function type. Implementations of the trait are instantiations of the dictionary datatype with particular function values for the fields f1...fn. Trait bounds like f<A: T>(...) are dictionary values passed to the function f (they are implicit additional arguments to f). A method call x.f() looks up the method f in the dictionary that was passed in for the type of x.

So the termination criteria I'm proposing is to check whether a Rust program could in principle be translated into Coq/F*-style type classes. (We wouldn't actually have to do this translation -- we'd just have to check that it would be possible without causing a cycle in the datatype declarations and datatype instantiations.)

In the first example above, the call to rec(self); would be illegal, because the call needs to pass the dictionary for struct S as an argument to rec<A: T> to fulfill the A: T constraint. But this is a cycle, because we don't have the dictionary yet at this point in the code: impl T for S is the thing that constructs the dictionary for S, and it's still in the middle of construction when the call to rec<A: T> occurs.

In the second example above, the trait definition trait T { fn f<A: T>(&self, x: &A); } is at fault, because when translated into a dictionary datatype containing f's function type, the function type recursively takes the dictionary datatype as an argument (because of the <A: T>). This means that the dictionary datatype definition refers to itself recursively in a negative position, which is illegal in Coq/F* (and also in Verus and Dafny).

[tjhance]

This certainly makes sense to me (I'm not sure what the alternative would be).

How does Dafny handle it, for comparison's sake?

[Chris-Hawblitzel]

There's a discussion on Dafny's approach at dafny-lang/dafny#1588 . At the moment, there's a "draconian restriction [that] outlaws the useful case where a trait is placed in a library". Dafny traits are a little different since they are more like Java/C# interfaces than type classes, so they might be looking at a different point in the design space.

[utaal]

I believe all of what's been discussed here as been implemented (mainly by @Chris-Hawblitzel). @Chris-Hawblitzel can I go ahead and close this?