Termination of dynamic dispatch

[RustanLeino]

Dafny decreases clauses were designed before the language had dynamic dispatch via trait members. As such, decreases clauses are made to be as simple as possible within each module, and decreases clauses are unnecessary across modules (see below for more details). When dynamic dispatch was added to the language, a draconian restriction was put in place to maintain soundness, namely to disallow dynamic dispatch across module boundaries. This is enforced by insisting that a class that implements a trait is declared in the same module that declares the trait.

The draconian restriction outlaws the useful case where a trait is placed in a library. Indeed, we are seeing this in dafny-lang/libraries now. So, Dafny supports a way for a user to lift the draconian restriction and instead take responsibility themselves for termination of dynamically dispatched calls via a trait--it is to mark the trait with {:termination false}.

This Issue calls out the need to replace the {:termination false} workaround with a sound solution.

More details of the current design

Here's how it works today. A decreases E declaration (where E is a list of expressions) applied to a method (or function) in a program is really a termination metric m, s, E, where m denotes the enclosing module and s denotes the strongly connected component (SCC) of the method inside its module. The import ordering on modules forms a well-founded order, and so does the connectivity ordering between SCCs in a module's call graph.

When a method with termination metric m, s, E, calls a method with termination metric m', s', E', a proof of termination requires showing that

m, s, E    >>    m', s', E'

where I'm using >> to denote the (well-founded) strict greater-than ordering on lexicographic tuples that Dafny uses. In the absence of dynamic dispatch across module boundaries, note the following:

• If the caller and callee are in the same module, then m == m', so the verification condition can be optimized by dropping the first components of the m, s, E and m', s', E' tuples.
• If the caller and callee are in different module, then necessarily m > m', because the caller's module must import the callee's module in order to make the call. In this case, the whole >> condition above is known (statically) to be true, so the verification condition can be optimized to just true.
• Similarly, within a module, if caller and callee are in the same SCC, then s == s', so the s/s' components of the >> condition above can be optimized away.
• And if caller and callee are in different SCCs, then necessarily s > s' (because of the way SCCs are defined), so the whole verification condition can be optimized to true.

What I just described in these bullets is how Dafny works today. That is, the m and s components are always optimized away and are never part of the verification conditions that are passed to the verifier. Also, note that, since the m and s components are always implicit, there is no need for any syntax for a user to write those components--indeed, Dafny currently does not have any such syntax.

One more detail: Dafny builds the intra-module call graph for each module and computes the SCCs of each such call graph. Since no global information is needed for this, this technique is compatible with modular verification. In the call graph of a module, there is an edge from a trait method T.m to each class method C.m that overrides it. That is, it is as dynamic dispatch is achieved through a synthetic implementation of T.m that does the following:

if this is C {
  C.m(...);
} else if ...

This synthetic implementation is a true representation of the effect of dynamic dispatch (but it's done more efficiently at run time by the use of v-tables or the like). To argue once-and-for-all about the termination of the calls that emanate from the synthetic implementation, one can change the m, s, E of T.m to m, s, E, 1 and change all other m, s, E triples into m, s, E, 0.

A possible design

To soundly allow dynamic dispatch across module boundaries, we need to do three things:

• Don't always apply the optimizations above. That is, the Dafny implementation should associate an m component and an s components of each decreases clauses, and should then look at the associated components when determining whether or not the optimizations can be applied.
• Provide a syntax for these components, so that a program can specify them. Ideally, no extra syntax should be required when the m and s components are those that are implicitly used today. This will keep the specification clutter low.
• Provide syntax to export information about a module's SCCs, how these compare, and also how various modules imported compare. (See below for an example.)

I'm suggesting that a decreases clause can start with an optional component that looks like #X where # is concrete syntax and X is the qualified name of a name of a method/function/whatever. For example, #X would typically have the form #M.T.F where M names a module, T names a type within that module, and F names a member of that type. Since it starts with #, the optional #X component is easy to distinguish from the other E components of the decreases clause. The m component discussed above will be (explicit or implicit) module part of X, and the s component discussed above will be the SCC of X in its declaring module.

Example: Consider a trait

module Library {
  trait MyTrait {
    method M(n: nat)
      decreases #MyTrait.M, n
    method P(n: nat)
      decreases n
    method Q(n: nat)
  }
}

I'll use R(_) as a function that gives a representative identifier of the SCC containing a given entity. The termination metric for M is then Library, R(Library.MyTrait.M), n, the termination metric for P is Library, R(Library.MyTrait.P), n (note that the first two components are implicit), and the termination metric for Q is Library, R(Library.MyTrait.Q), n (note that all three components are implicit).

Now, consider a class in a different module that implements MyTrait:

module Client {
  import Library

  class MyClass extends Library.MyTrait {
    method M(n: nat)
      decreases #Library.MyTrait.M, n
    { ... }
    method P(n: nat)
      decreases n
    { ... }
    method Q(n: nat)
    { ... }
    method S(n: nat)
    { ... }
  }
}

The termination metric of MyClass.M is the one given explicitly, namely Library, R(Library.MyTrait.M), n. This is the same as the method it overrides, so the decreases-overrides check passes trivially.

The override MyClass.P does not give a # component in its decreases clause. Since it is an override, I suggest that Dafny fill in the # component in the same way as the method being overridden. This means the the termination metric of MyClass.P is Library, R(Library.MyTrait.P), n. Note, it would not be friendly to pick Client, R(Client.MyClass.P), n as the default termination metric, because that's certain to fail the decreases-overrides check.

Similarly, the override MyClass.Q, which does not have an explicit decreases clause at all, defaults to a termination metric of Library, R(Library.MyTrait.Q), n.

Method S is not an override, so it defaults to a termination metric Client, R(Client.MyClass.S), n.

As given in the example, all of the decreases-overrides check will pass. But consider what happens to calls in the implementations of the methods in MyClass. If S calls into one of the other methods, then things are fine, because Client >> Library. But if one of the other methods, say P, tries to call S, then the verifier will flag it with a termination error. To correct such an error, the recourse would be to change the specification of S to say decreases #Library.MyTrait.P.

If P in MyClass calls Q, then the verifier will also report a termination error, because it does not know how R(Library.MyTrait.P) and R(Library.MyTrait.Q) compare--these refer to SCCs inside Library, which are (because of modular verification) not available in Client. Instead, the solution here is that Library must export something that says how these compare. I suggest extending the language to allow export clauses to export ordering information. In particular, I suggest the syntax

export
  provides MyTrait.M >> MyTrait.P
  provides MyTrait.P == MyTrait.Q

to say that M lies above P in Library's SCC ordering and that P and Q are in the same SCC. If there's no export declaration, then no such orderings are exported--in other words, any such ordering has to be exported explicitly. There needs to be a check for all export sets to see if the orderings they claim are consistent. A good way to do that check seems to be add an edge from M to P for >> export, and to add an edge from P to Q and an edge from Q to P for the == export, and then to check that M is indeed above P in the final ordering. (No additional check is needed for the == export, since adding the two edges ensures that P and Q will be in the same SCC.)

(One will also need to express that certain modules lie above other modules in the import ordering. That can probably be done with this same syntax.)

An explicit decreases clause can give just the # component. That is, if a program says just decreases #M.X, then the E components are filled in as usual in Dafny. For example, four ways for MyClass.Q above to have the same termination metric would be to

• leave off the decreases clause altogether (as was done above)
• write decreases #Library.MyTrait.Q and let the E components default to n
• write decreases n and let the # component default to #Library.MyTrait.Q
• write decreases #Library.MyTrait.Q, n

One thing I have not detailed--in fact, I'm not sure of its answer--is how to construct the call graph inside a module and compute its SCCs. I'm guessing this should be done in the same way as always, without regard to any (implicit or explicit) decreases clauses.

Other designs

I know of only one other design that solves this problem and achieves modular verification. It is by Bart Jacobs and colleagues, and it makes use of a multiset ordering of method names. (I think it is implemented in VeriFast.) I haven't worked out a detailed comparison, but I'm guessing Jacobs's design is more flexible than what I have sketched above. Nevertheless, I'm hoping the design sketched above might be good enough, might be lighter in required syntax, and might fit into what Dafny programmers are used to today. If not, we may need to adopt Jacobs's design more directly.

[MikaelMayer]

The issue and the proposed solution seem consistent and appropriate, I like them.

However, rather than the (new) syntax:

export
provides MyTrait.M >> MyTrait.P
provides MyTrait.P == MyTrait.Q

woudl it be possible to reuse the same usual trick in the trait, to add one more element in the tuple that decreases to indicate explicit method ordering? It is already part of the specification.
This forces to write down the expression decreases for Q, but I think this is a minor inconvenient since we are encoding knowledge about termination order.

module Library {
  trait MyTrait {
    method M(n: nat)
      decreases #MyTrait.M, n, 1
    method P(n: nat)
      decreases n, 0
    method Q(n: nat)
      decreases n, 0
  }
}

[keyboardDrummer]

The termination metric of MyClass.M is the one given explicitly, namely Library, R(Library.MyTrait.M), n. This is the same as the method it overrides, so the decreases-overrides check passes trivially.

I think this is the first time that you mention a decreases-overrides check. What does this check do? What's a use-case in which an overriding method will have a different decreases clause as the trait method?

I get the impression you're asking the author of trait method to define a decrease clause on it, which I find confusing. How are you supposed to know what the method will need to call without having an implementation for it yet?

[cpitclaudel]

Following a quick discussion today:

I wonder how deep call trees across modules tend to be in real programs. If they are not too deep, it might be possible to abandon the modularity aspect and just verify termination at the whole-program level. If we did that, the current system might actually be sufficient?

[robin-aws]

I've realized there's a decent workaround to this problem for shared libraries, which definitely doesn't remove the need for a deeper solution as above, but does allow soundly providing reusable traits in many contexts.

Here's the idiom we can provide (using my first attempt to add a trait to dafny-lang/libraries as an example, since unlike MutableMap the intent is for consuming projects to provide their own implementing classes: dafny-lang/libraries#22)

// Frames.dfy, in a shared library

abstract module FramesTemplate {

  trait Validatable {
    // ...
  }
}

module Frames refines FramesTemplate {}

// MyStuff.dfy in a consuming project

module MyObjects refines FramesTemplate {
  
  // No warning about extending traits across modules
  class MyThing extends Validatable {
    // ...
  }

  // ...
}

Inside the MyObjects module, the relationship between MyThing and Validatable is no longer across modules, because for the purposes of validation the latter is essentially defined in MyObjects module as well. As long as a consuming project can define all implementors of the traits in one such module, this avoids having to put {:termination false} on anything.

This is still clearly limited, and in this particular example this would mean putting a lot of classes in a single module. It also doesn't scale well to using many such sets of reusable traits, and I'm sure there are cases of needing to use more than one at one in a module. This is still better than the current situation of immediately giving up on the soundness of termination checking, though. The concrete Frames module is still provided so that it is possible to import the trait directly and opt-in to that unsoundness (once #4642 allows it). Once we have a sound solution for extending traits across modules, Frames can soundly be used directly.

[robin-aws]

I've realized I'm not 100% confident the idiom above is sound and would like to double-check before encouraging anyone to use it. I don't have a counterexample handy to try, and it might be that the cross-module trait extension check happens after the contents of an abstract module are copied into a refining module but should be before, etc.

[keyboardDrummer]

I want to suggest the following:

Each function/method is given a matching height function that takes the same parameters and returns a nat. Height functions may not have cycles in their call-graph, otherwise it is a user error, which means they don't need to worry about non-termination.

When you call a function/method M from a function/method C, the termination check will assert that (M_Height(..), M_decreases(...)) < (C_Height(...), C_decreases(...)).

Here's an example of how height functions resolve termination issues with traits:

trait T {
  // If you have a trait with a bodyless method, then the height function of that method is also kept bodyless.
  function M_Height()
  method M() {}
  
  function FirstCaller_Height(): nat { 
    M_Height() + 1 // call to abstract height function is allowed because it's in the same trait. 
  }
  method FirstCaller() {
    assert M_Height() < FirstCaller_Height(); // implicit assertion, passes because X < X + 1
    M();
  }
}

class Valid extends T {
  function M_Height(): nat { 2 }
  method M() {
    assert Helper_Height() < M_Height(); // implicit assertion, passes because 1 < 2
    Helper();
  }

  method Helper_Height(): nat { 1 }
  method Helper() {
  }
}

class Invalid1 extends T {
  function M_Height(): nat { FirstCaller_Height() + 1 } // error, cycle detected in call graph of height functions
  method M() {
    assert FirstCaller_Height() < M_Height();
    FirstCaller();
  }
}

class Invalid2 extends T {
  function M_Height(): nat { 1 }
  method M() {
    assert FirstCaller_Height() < M_Height(); // implicit assertion, fails because !(2 < 1)
    FirstCaller();
  }
}

function SecondCaller_Height(a: Valid): nat { 3 }
method SecondCaller(a: Valid) {
  assert a.M_Height() < SecondCaller_Height(a) // implicit assertion, passes because 2 < 3
  a.M();
}

class AlsoValid extends T {
  function M_Height(): nat { 4 }
  method M() {
    var valid = new Valid();
    assert Dangerous_Height([this, valid]) < M_Height(); // implicit assertion, passes because (valid.M_Height()+1) < 4
    Dangerous([this, valid]);
  }

  function Dangerous_Height(ts: seq<T>) { ts[1].M_Height() + 1 }
  method Dangerous(ts: seq<T>) 
    requires |ts| > 1 && ts[1] is Valid
  {
    ts[0], ts[1] := ts[1], ts[0];
    assert ts[1].M_Height() < Dangerous_Height(ts); // implicit assertion, passes because x < x + 1
    ts[0].M();
  }
}

Now lets improve the user experience by introducing calls clauses. These are used to generate the height functions. The above program translates to.

trait T {
  method M() {}
  
  method FirstCaller() 
    calls M() // Can be inferred because this is a call on `this` which can not be assigned to.
  {
    M();
  }
}

class Valid extends T {
  method M() 
    calls Helper() // Calls clause can be inferred because this is a non-virtual call
  {
    Helper();
  }

  method Helper() {
  }
}

class Invalid1 extends T {
  method M() 
    calls FirstCaller() // error, cycle detected in calls clauses. Calls clause can be inferred.
  {
    FirstCaller();
  }
}

class Invalid2 extends T {
  method M() {
    assert FirstCaller_Height() < M_Height(); // implicit assertion, fails because !(2 < 1)
    FirstCaller();
  }
}

method SecondCaller(a: Valid) 
  calls a.M() // If we notice 'a' is never assigned, this can be inferred.
{
  a.M();
}

class AlsoValid extends T {
  method M() 
    calls Dangerous([this, new Valid()]) // awkward because I thought calls clauses were just expressions, and now it's not. Have to think about the syntax.
  {
    var valid = new Valid();
    Dangerous([this, valid]);
  }

  method Dangerous(ts: seq<T>) 
    requires |ts| > 1 && ts[1] is Valid
    calls ts[1].M() // can not be inferred
  {
    ts[0], t[1] := ts[1], ts[0];
    ts[0].M();
  }
}

[keyboardDrummer]

About the "A possible design" proposal in the details.

It mentions having to write export ordering in MyTrait if you want the overriding methods P to call Q:

module Library {
  export
    provides MyTrait.M >> MyTrait.P
    provides MyTrait.P == MyTrait.Q

  trait MyTrait {
    method M(n: nat)
      decreases #MyTrait.M, n
    method P(n: nat)
      decreases n
    method Q(n: nat)
  }
}

But how would the designer of Library already know whether M will call P and that P and Q are in the same SCC, given that these methods have not been implemented yet?

---

Another thing, if I write

module Client {
  import opened Library
  import UnrelatedLibrary

  static method Foo(traitInstance: MyTrait)
    // The decreases clause is required because of the call to `M`
    decreases #Library.MyTrait.M
  {
    traitInstance.M(3);
    AnyOtherLibrary.Bar(); // would this call always fail because Library does not import UnrelatedLibrary?
  }
}

[MikaelMayer]

What if every unimplemented function in a trait or in an abstract class was required to have a decreases clause, and we relax the assumption of inter-module call?
I know it's a bit heavy but that would take care of most if not all termination problems.

I'm taking an example @fabiomadge shared where I simulate such decreases clause. I'm not sure how much it would solve the problem

module Reals {
  trait {:termination false} Function {
    function Decreases(): nat

    predicate Valid()

    function Apply(r: real, ghost previousDecreases: nat): real reads *
      requires Valid()
      requires Decreases() < previousDecreases
  }
}

module Math {
  import Reals
  function Derivative(f: Reals.Function, x: real, ghost previousDecreases: nat): real reads *
    requires previousDecreases >= 1
    requires f.Valid()
    requires f.Decreases() < previousDecreases - 1
  {
    f.Apply(x + 1.0, previousDecreases - 1) - f.Apply(x, previousDecreases - 1)
  }
}

module Implementation {
  import Reals
  import Math

  class Linear extends Reals.Function {
    var m: real
    var t: real

    constructor (m: real, t: real) {
      this.m := m;
      this.t := t;
    }

    predicate Valid() {
      true
    }
    
    function Decreases(): nat { 0 }

    function Apply(x: real, ghost previousDecreases: nat): real reads *
      requires Decreases() < previousDecreases
    {
      m * x + t
    }
  }

  class Good extends Reals.Function {
    const f: Reals.Function

    predicate Valid() {
      f.Valid() && f.Decreases() < Decreases() - 1
    }

    function Decreases(): nat { 2 }

    constructor () ensures Valid() {
      f := new Linear(1.0, -1.0);
    }

    function Apply(x: real, ghost previousDecreases: nat): real reads *
      requires Decreases() < previousDecreases
      requires Valid()
    {
      Math.Derivative(this.f, x, previousDecreases - 1)
    }
  }

  class Bad extends Reals.Function {
    constructor () ensures Valid() {}

    predicate Valid() {
      true
    }

    function Decreases(): nat { 1 }

    function Apply(x: real, ghost previousDecreases: nat): real reads *
      requires Decreases() < previousDecreases
      requires Valid()
    {
      Math.Derivative(this, x, previousDecreases - 1) // Cannot prove anything here.
    }
  }
}

method Main() {
  var c := new Implementation.Bad();
  print c.Apply(42.0, 2), "\n";
}

[keyboardDrummer]

The previous proposal I wrote suffers from the problem that the heights functions themselves need decreases clauses. I think the following proposal is simpler and does not suffer from that.

---

Currently Dafny does not allow implementing traits from another module, because that can cause cycles in the call-graph that cross module boundaries, and to prove termination for these would require doing whole-program verification.

We can resolve this problem by changing how dynamic calls are tracked in the call-graph so that it no longer has cycles across modules even when modules implement traits from other modules, but in a way that preserves the graph's ability to be used in termination checking.

To be able to construct this call-graph while preserving modularity, functions that call dynamically dispatched methods, must record this in their contract, for which we introduce calls clauses.

Example of how it works:

module Producer {
  trait F {
    method Foo()
  }

  method Dynamic(f: F) 
    calls f.Foo 
  {
    // No termination check since this call is in the calls clause, 
    // so the termination check is moved to the caller of Dynamic.
    f.Foo();
  }
}

module Consumer {
  import opened Producer

  method M1() 
  {
    var c := new F2;
    // Termination check: assert Scc_Height(M1) > Scc_Height(c.Foo)
    // This check passes because the verifier determines `c.Foo == F2.Foo`, so the assert becomes
    // assert Scc_Height(M1) > Scc_Height(F2.Foo), which becomes
    // assert 2 > 1

    // Note that this check only looks at the Scc_Height component, but not the decreases clause. 
    // This is because the calls clause of `Dynamic`,   
    // does not specify with which arguments the dynamic call to c.Foo is done,
    // so we can't use the decreases clause of c.Foo
    // A more expressive design with more complicated calls clauses is possible
    Dynamic(c);
  }

  class F1 extends F {
    method Foo() {
      M1();
    }
  }

  class F2 extends F {
    method Foo() { }
  }
}

Call-graph:

Dynamic -> { }
F2.Foo -> { }
M1 -> { Dynamic, F2.Foo }
F1.Foo -> { M1 }

Note that when calling a function with calls clauses, an additional termination check has to be done for each calls clause.

It might be possible to always infer the calls clauses, and in that case they won't need to be part of the language.

More powerful lambdas

For each function type, ->, --> and ~>, we define a complementary function type ?->, ?--> and ?~>, which consists of a pair of the original function type and an element of the termination metric.

In the following example, we create a lambda that current Dafny does not except.

function HigherOrder(i: nat, f: nat ?-> nat): nat
  calls f.calls
  decreases f.decreases - 1
{
  1 + f(i - 1)
}

function Recursive(i: nat): int
  decreases i, 1
{
  var f: nat ?-> nat := j => Recursive(j) decreases j;
  // Termination check: assert (Scc_Height(Recursive), i) >= (Scc_Height(Recursive), i - 1)
  HigherOrder(i, f)
}

[MikaelMayer]

Having a f.decreases is a very interesting idea; however, it was shown that its relation with requires and reads clauses is extremely dangerous in general #2750 (comment)

But in general I like the idea to have a type that indicate that the function should have a decreases clause.

[fabiomadge]

@MikaelMayer

What if every unimplemented function in a trait or in an abstract class was required to have a decreases clause, and we relax the assumption of inter-module call? I know it's a bit heavy but that would take care of most if not all termination problems.

Every function or method always has a decreases clause, even if you don't specify one. In that case, it's the default.
I'm not sure what you mean by the assumption on the inter-module call.

[fabiomadge]

@keyboardDrummer

Currently Dafny does not allow implementing traits from another module, because that can cause cycles in the call-graph that cross module boundaries, and to prove termination for these would require doing whole-program verification.

We can resolve this problem by changing how dynamic calls are tracked in the call-graph so that it no longer has cycles across modules even when modules implement traits from other modules, but in a way that preserves the graph's ability to be used in termination checking.

To be able to construct this call-graph while preserving modularity, functions that call dynamically dispatched methods, must record this in their contract, for which we introduce calls clauses.

Here are the two issues, one minor, and one major, with this proposal:
To be sound, the calls clauses would need to be on every member transitively calling a dynamically dispatched member.
The real problem is that I don't see how your proposal efficiently catches the issue with the following program:

module Tr {
  trait {:termination false} T {
    function A(other: T): int
    function B(other: T): int
  }
}

module X {
  import Tr
  class X extends Tr.T {
    constructor () { }
    function A(other: Tr.T): int {
      0
    }
    function B(other: Tr.T): int {
      other.A(this)
    }
  }
}

module L {
  import Tr
  function Tie(t1: Tr.T, t2: Tr.T): int { t1.B(t2) }
}

module Y {
  import Tr
  class Y extends Tr.T {
    constructor () { }
    function A(other: Tr.T): int {
      other.B(this)
    }
    function B(other: Tr.T): int {
      1
    }
  }
}

module M {
  import Tr
  import X
  import Y
  import L

  method Main() {
    var x: Tr.T := new X.X();
    var y: Tr.T := new Y.Y();
    print L.Tie(x, y), "\n";
  }
}

L doesn't import X, so there's no way of knowing that B calls A when verifying L. You'd have to check it on a program level, which wouldn't end up being too dissimilar from doing a whole program analysis.

[keyboardDrummer]

@fabiomadge

Thanks for your reply! I agree, what I described doesn't seem to work for the Tie program.

I feel like at a high level there's two options. One is fully static analysis of the call-graph, which is what we do now, and the other a dynamic analysis that requires the verifier to also construct a type of call-graph, that would accept more valid programs.

I think extending the static analysis to work across modules can work. If we include as part of a module signature, for each function/method, the trait functions/methods that it calls, then we apply the static call graph analysis that we currently do within a module, also when traits from other modules are used.

In the Tie program above, the termination analysis of module M would result in the call graph:

M -> { L.Tie } // edge comes from the source of the current module `M`
L.Tie -> { Tr.T.B } // edge comes from the cross-module exposed signature of L.Tie
Tr.T.B -> { X.X.B } // any trait extending classes in the current module scope, even if they are imported, create edges from the trait method to the overriding method
X.X.B -> { Tr.T.A } // edge comes from the cross-module exposed signature of X.X.B 
Tr.T.A -> { Y.Y.A } // any trait extending classes in the current module scope, even if they are imported, create edges from the trait method to the overriding method
Y.Y.A -> { Tr.T.B } // edge comes from the cross-module exposed signature of X.X.B

So the SCC graph is:

{ M } -> { { L.Tie } }
{ L.Tie } -> { { Tr.T.B, X.X.B, Tr.T.A, Y.Y.A } }

And then it could say, "Error: detected a call-graph cycle in methods defined outside module M. Please remove either X.X or Y.Y from the scope of M"

For a cycle where at least one method of the cycle is defined in the current module, then the error can be shown there.

module Producer {
  trait Trait {
    method Foo();
  }
  method CallsFoo(t: Trait) { // Dafny infers that this calls Trait.Foo and exposes that in the contract of Producer
    t.Foo();
  }
}

module Consumer {
  import Producer
  class Bar extends Producer {
    method Foo() {
      // Error: cannot prove termination; try supplying a decreases clause
      Producer.CallsFoo();
    }
  }
} 

Call-graph:

{ Producer.Trait.Foo, Producer.CallsFoo, Consumer.Bar.Foo }

I think I've left out some things related to decreases clauses. If you're curious I have thoughts on how to tackle that.

---

I was excited about a call-graph analysis that uses the verifier, because it would admit more valid programs, and I was worried that the static approach wouldn't scale to very large applications. I was thinking that as an application grows, each trait will be have more and more classes that extend it, so the SCCs that its abstract methods are apart of will keep growing. However, given that a module only cares about the trait-extending-classes that it has imported, I think the scaling issue might not be so bad.

[MikaelMayer]

Every function or method always has a decreases clause, even if you don't specify one. In that case, it's the default.
I'm not sure what you mean by the assumption on the inter-module call.

Indeed, based on our discussion after my comment, it looks like what I was looking for is to state something like "When determining a group of mutually recursive definitions, any call to a bodiless function is considered part of the clique and thus requires a decreases clause.
Any implementation of a bodiless function that calls into a mutually recursive set of definitions is also required to have the decreases check as if it was part of it.

An example to make sense of what I say. On the program above, we would end up with an error:

module Tr {
  trait T {
    function A(other: T): int
    function B(other: T): int
  }
}

module X {
  import Tr
  class X extends Tr.T {
    constructor () { }
    function A(other: Tr.T): int {
      0
    }
    function B(other: Tr.T): int {
      other.A(this) // Error: could not prove that decreases clauses decrease (calling into a bodiless function automatically requires a decreases clause check)
    }
  }
}

module L {
  import Tr
  function Tie(t1: Tr.T, t2: Tr.T): int {
    t1.B(t2) // Error: Could not prove that decreases clause decreases. B is a bodiless function so it could get back to Tie.
  }
}

module Y {
  import Tr
  class Y extends Tr.T {
    constructor () { }
    function A(other: Tr.T): int {
      other.B(this)  // Error: Could not prove that decreases clause decreases. B is a bodiless function so it could get back to Tie.
    }
    function B(other: Tr.T): int {
      1
    }
  }
}

module M {
  import Tr
  import X
  import Y
  import L

  method Main() {
    var x: Tr.T := new X.X();
    var y: Tr.T := new Y.Y();
    print L.Tie(x, y), "\n";
  }
}