Supporting dyn soundly

[Chris-Hawblitzel]

We've been discussing dyn for Verus recently, and I wanted to write down some notes about dyn's soundness when used in specifications and proofs. I think dyn should be sound, but there's at least one thing we have to be careful about: operations on dyn should be considered exec or proof mode operations, not spec mode operations. Otherwise, there would be a danger of fabricating fake implementations of impossible trait bounds (this would be similar to Dafny issue dafny-lang/dafny#851 ). I believe this should be a straightforward restriction that fits in naturally with Verus's mode system.

To see the potential issue in more detail, consider our model encoding of traits as dictionary datatypes, where we model a trait like this:

trait T {
    fn f(x: Self, y: Self) -> bool;
    fn g(x: Self, y: Self) -> Self requires f(x, y);
}

with a dictionary datatype like this:

#[derive(Clone, Copy)]
struct Dictionary_T<Self> {
    f: Fn(x: Self, y: Self) -> bool,
    g: Fn(x: Self, y: Self) -> Self requires f(x, y),
}

In this model, a bound A: T on type A:

proof fn test<A>() where A: T { ... }

is treated like a dictionary parameter:

proof fn test<A>(d: Dictionary_T<A>) { ... }

It's important that program cannot fabricate dictionaries, because not all dictionary types can be implemented. For example, if a trait has a method proof fn bad() ensures false;, then no dictionary value can implement this method, and if we accidentally assume a dictionary implementing this method, the program could call bad and prove false. So in Verus mode terminology, we have to treat dictionaries as having mode proof/tracked, not mode spec/ghost, since Verus allows fabrication of values for mode spec/ghost but prohibits fabrication for mode proof/tracked:

proof fn test<A>(tracked d: Dictionary_T<A>) { ... }

This matters for dyn, because the type dyn T is essentially an existential type or dependent product type that contains a type Self, a dictionary Dictionary_T<Self>, and a value of type Self:

struct Dyn_T {
    ghost Self: type,
    tracked bound: Dictionary_T<Self>,
    tracked value: Self, // could also have mode exec
}

Here, it's important that we treat the bound Dictionary_T<Self> as proof/tracked, not as spec/ghost. This means that a Dyn_T value is only useful if it has mode exec or proof/tracked. If the program created a spec/ghost Dyn_T value, we would have to assume that it had been fabricated (e.g. using arbitrary()) and we should not allow its dictionary to be used to instantiate bounds A: T. Therefore, the mode system should insist that any operations (in particular, method invocations) on a dyn T value require the dyn T value to have mode exec or proof/tracked. This should be required even for spec methods on T, since we intend to support ensures clauses on spec methods and we already support polymorphic broadcast lemmas (with trait bounds) triggered by spec functions.

(We could consider an exception for traits that consist entirely of spec methods and have no ensures clauses; I haven't thought much about this and I don't know if it would be useful. A more general exception would be if the program could prove the trait dictionary was an inhabited type, though again, I don't know if this is actually useful.)

[Chris-Hawblitzel]

(We could consider an exception for traits that consist entirely of spec methods and have no ensures clauses; I haven't thought much about this and I don't know if it would be useful. A more general exception would be if the program could prove the trait dictionary was an inhabited type, though again, I don't know if this is actually useful.)

I think there is a sound refinement of this that is useful: with a spec dyn T, you can refer to spec methods of T and call them, but you won't a priori know any properties about the spec methods or the results of calls to them. More specifically, properties about the spec methods still require the full proof/tracked dictionary, and this is reflected in the SMT encoding, where the (tr_bound%T ...) predicate represents evidence of the existence of the full proof/tracked dictionary. We already use (tr_bound%T ...) to guard broadcast proof axioms and definition axioms for recursive functions. For example, in the following definition:

trait T {
    spec fn f(&self) -> nat;
    proof fn about_f(&self) ensures self.f() < 10;
}

broadcast proof fn promote_f<A: T>(a: &A)
    ensures
        #[trigger] a.f() < 10,
{
    a.about_f();
}

the axiom for promote_f is:

(axiom (=>
  (fuel_bool fuel%promote_f.)
  (forall ((A&. Dcr) (A& Type) (a! Poly)) (!
    (=>
     (has_type a! A&)
     (=>
      (tr_bound%T. A&. A&)
      (< (%I (T.f.? A&. A& a!)) 10)
    ))
    :pattern ((T.f.? A&. A& a!))
    :qid user_crate__promote_f_0
    :skolemid skolem_user_crate__promote_f_0
))))

where the precondition (tr_bound%T. A&. A&) ensures that the axiom only activates for types A that have been proven to fully implement the trait T. This includes exec and proof/tracked dyn T values, but not spec dyn T values. For example:

proof fn test(s: &dyn T, tracked t: &dyn T)
    requires
        s.f() < 20,
{
    assert(s.f() >= 0); // SUCCEEDS, because every nat is >= 0
    assert(s.f() < 20); // SUCCEEDS, because of the requires
    assert(s.f() < 10); // FAILS, because we lack tr_bound%T for s, so promote_f isn't active
    assert(t.f() < 10); // SUCCEEDS, because we have tr_bound%T for t
}

One way to think about this is to (conceptually) split the dictionary into two dictionaries, a proof/exec dictionary that need not be inhabited, and a spec dictionary that is trivially inhabited. The spec dictionary would carry spec methods, but not their ensures clauses. All spec function types (excluding any ensures clauses) are trivially inhabited by functions that simply return arbitrary().

[Chris-Hawblitzel]

One additional consideration is that in Rust, for an object-safe T, the type dyn T itself implements T, or rather, T + ?Sized (i.e. dyn T implements T and dyn T does not implement Sized). This could circumvent our attempt to require that accesses to exec/proof methods go through exec or proof/tracked dyn T values:

trait False {
    proof fn ensure_false(&self) ensures false;
}

proof fn incorrect<F: False + ?Sized>(f: &F)
    ensures false
{
    f.ensure_false();
}

proof fn bad()
    ensures false
{
    incorrect::<dyn False>(&arbitrary());
}

Here, the code is able to call ensure_false with only a spec dyn False value. We want the code to have to use at least a proof/tracked dyn False value to call ensure_false. Therefore, I propose building on Rust's object safety rules ( https://doc.rust-lang.org/reference/items/traits.html ) with additional rules specific to modes and proof and spec methods:

• Dispatchable exec functions must have a receiver with mode exec (as expected).
• Dispatchable proof functions must have a tracked self& receiver.
• Dispatchable spec functions must not have any ensures clauses.

With these, code can still use dyn T as T + ?Sized, but all calls to T + ?Sized trait objects will either require tangible, unforged exec or proof/tracked values, for exec and proof methods, or will just call spec methods with no ensures, which is harmless even for forged spec values.

In addition, we have to make sure that F: False + ?Sized doesn't activate any broadcasts via the (tr_bound%False. A&. A&) predicate:

enum Opt<A: ?Sized> {
    None,
    Some(Box<A>),
}

spec fn f<A: ?Sized>(a: &Opt<A>) -> bool { true }

trait False {
    proof fn ensure_false() where Self: Sized ensures false;
}

broadcast proof fn promote_false<A: False>(a: Opt<A>)
    ensures
        #[trigger] f::<A>(&a),
        false,
{
    A::ensure_false();
}

proof fn incorrect<A: False + ?Sized>()
    ensures
        false,
{
    broadcast use promote_false;
    assert(f::<A>(&Opt::None));
}

proof fn bad()
    ensures
        false,
{
    incorrect::<dyn False>();
}

For this, I propose making the SMT encoding of trait bounds slightly more aware of Sized. (We should probably also add SMT bound predicates for the other marker traits like Copy and Send and Sync, independent of dyn.) Sized is a special case because it is added by default to most type parameters, and we don't want to add SMT overhead to things like impl<A> Seq<A> { pub spec fn len(self) -> nat; ... } that don't care about Sized. This is why, for type parameters with no trait bounds, Verus's SMT encoding simply ignores Sized and instead uses the pub spec fn is_sized<V: ?Sized>() -> bool; function to distinguish between types that do and do not support size_of. However the distinction between T + Sized and T + ?Sized will matter in the SMT encoding for dyn T. So I propose splitting our current tr_bound%T into separate predicates for the T + Sized and T + ?Sized cases. These predicates will be pruned if not needed (this pruning is already implemented for the existing tr_bound%T); I expect the T + Sized SMT predicate to be the common case and the T + ?Sized SMT predicate to usually be pruned away.

(As an alternative, we might consider having the syntax macro add where A: ?Sized to all type parameters for all spec and proof functions that don't explicitly mark A as Sized, although this is a lot of semantic work to ask of the syntax macro.)

[tjhance]

Automatically adding ?Sized to spec/proof code is something I have looked into. The problem is that Rust will throw up errors because it requires stuff to be sized unless it's used behind a pointer. Rustc performs these checks during type checking, so there is no way to disable them without forking the type checking crate.

[Chris-Hawblitzel]

Ah, that's good to know. I won't try to pursue that alternative, then.

[tjhance]

Also I'm in favor of anything that will let us get rid of is_sized

[utaal]

@tjhance: consider "call credits", for higher order recursive functions.

Also consider termination credits.

[utaal]

@Chris-Hawblitzel: we have a sound design for dyn for termination.

[utaal]

@marshtompsxd:

A use case that also motivates this: in the Anvil project we have to define a struct that needs to take a sequence of different types that all implement a trait T. Right now our solution is: (1) define an opaque type and use that type in the struct, (2) define (uninterpretable) functions to convert between each type to/from the opaque type, (3) define axioms for each type that any object of this type remains unchanged after a RTT of the conversion --- similar to marshal and unmarshal.

[jaybosamiya-ms]

Another use case for dyn: @y1ca1 was looking for support that would allow writing certain combinators (in https://github.com/secure-foundations/vest) that need a form of deferring. I believe the specific sort of dyn support he was looking for looked like impl Foo for Box<dyn Fn() -> T> where T: Foo.

[marshtompsxd]

We have another use case in Anvil that the user of the Anvil framework wants to provide some function f of Fn(A) -> B, and the Anvil framework has no way to know the concrete type of f during compile time. We'd like to use Box<dyn Fn(A) -> B> in this case.

[tjhance]

Potential soundness thing to watch out for:

dyn traits effectively have automatic impls impl T for dyn T; however, these can overlap with blanket impls. This is an open soundness issue in Rust: rust-lang/rust#57893

According to the linked discussion there, the main problem in Rust only occurs when the traits have associated types. I think it'll be problematic for us even without associated types, since conflicting trait impls can have inconsistent spec functions.

When we implement dyn, we should make sure Verus's conflict checker is able to catch the issue.

[utaal]

@tjhance @Chris-Hawblitzel: It may be easier to support only traits with exec functions

[junyang-zh]

Another cool thing we can have with dyn support is the physical frame management in the Asterinas OSTD. I am looking forward to it and seeing if I can help :)

https://github.com/asterinas/asterinas/blob/e4c5c36be9fb58ee78e558e72762e8450bcb5ba2/ostd/src/mm/frame/mod.rs#L70-L79

This API set enables opaque types for OSTD users to define arbitrary frame types, such as page cache frames, buffer frames, etc.

Under the hood, we utilize the pointer metadata to implement our own smart pointers. It seems to be another complex problem for Verus if we don't allow any cheats.