fix: Cross-modular override check

[fabiomadge]

Reintroduces #3223, with support for additional use cases. Finally fixes #2500.

trait Trait {
  predicate Even(i: nat)
  predicate Odd(i: nat)
    ensures if i == 0 then true else (i % 2 == 1) == Even(i-1)
}

class Class extends Trait {
  predicate Even(i: nat) { if i == 0 then true else Odd(i-1) }
  predicate Odd(i: nat)
    ensures if i == 0 then true else (i % 2 == 1) == Even(i-1)
  { if i == 0 then false else Even(i-1) }
}

This didn't pass before the changes in this PR, as we fail to prove Cl.Odd.Ens ==> Tr.Odd.Ens, which is part of the override check for Cl.Odd. It boils down to … Cl.Even … ==> … Tr.Even …, but because they are in the same SCC, we can’t use Tr.Even == Cl.Even. This fix turns it into … Cl.Even … ==> … Cl.Even … instead, by lowering all functions (with the correct receiver) from trait to class, instead of just doing it for the function that is override tested.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[RustanLeino]

The change here seems to be to use the trait member's height to regulate the use-via-context of the override axiom. The solution appears to work, but I'm unable to state an argument for its correctness. In fact, in trying to do so, I find myself surprised at some of the levels that are being used. For example, the check-well-formedness procedure that is responsible for checking the condition expressed by the consequence axiom is assuming a function height that is 2 higher than the height used to activate the axiom.

Here's the playing field, as I see it. For each function F, we generate various axioms:

• The frame axiom states that the function is independent of the heap, except at those location listed in the function's reads clauses.
• The definition axiom says that the function returns the value one gets by evaluating the body of the function.
• The consequence axiom says that the function result satisfies the result type and ensures clauses of the function.
• If F overrides a function in a parent trait, then the override axiom says that the overridden function and the overriding function return the same value when type of the receiver is that of the overriding type.

The axioms are expressed with antecedents to make them apply only when the function's parameters have the expected types and the requires clauses of the function hold. (Well, the frame axiom is a little looser with its antecedents.)

Whenever we generate an axiom, we must make sure there are checks in place that justify the axiom. These checks are collected in two Boogie procedures:

• The CheckWellformed procedure checks the well-formedness of the function's specification and checks that any mutable heap locations read by the requires and reads clauses are included in the reads clauses. If the function has a body, the CheckWellformed procedure also checks the well-formedness of the body, checks that any mutable heap locations read by the body are included in the reads clauses, and checks that the value to which the body evaluates adheres to the function's result type and ensures clauses.
• If F overrides a function in a parent trait, then the OverrideCheck procedure checks that the function's specification is weaker than the specification of the overridden function (as if the overridden function were going to call the overriding function--which is really what dynamic dispatch is going to do at run time).

Since these procedures are supposed to check that the properties expressed by the axioms really hold, it is important that the procedures not be given access to the axioms before they are done checking. (This was the problem reported in #2500.) How this is done has changed during the history of the Dafny tool, but let me explain the current form of this enforcement mechanism.

The general form of these axioms (except the frame axiom, but I'll ignore it) is

axiom
  AXIOM_ACTIVATION
  ==>
  (forall args ::
    F#CanCall(args) || USE_VIA_CONTEXT
    ==>
    //... what we really wanted to say about the function

Each time a function is called, the Dafny verifier checks that the actual argument satisfy the types of the function's formal parameters, that the function's precondition holds, and that the call will terminate (that is, that the termination metric stated by decreases clauses decreases). After these checks, it emits the assumption assume F#CanCall(args);. For any invocation of the function with these arguments, the "CanCall" assumption is analogous to concert tickets for a particular show.

One could imagine that the verifier would use such CanCall assumptions as the only antecedent for the consequence and definitions axioms. Indeed, we have started an effort to remove the other preconditions, but this is not yet completed (PR #1400). Instead, the verifier uses a second (older) mechanism as well. It is built on the height of a function in the module's call graph (more precisely, the height of the function's SCC--strongly connected component--in the module's call graph). Essentially, if F has height, say, 13, then the CheckWellformed procedure starts with an assumption FunctionHeight == 13. Then, since all necessary checks for F are done at (or below) level 13, we know that it's safe to use the axioms at level 14 and above (for arguments that satisfy the function's precondition). However, before the invention of CanCall, this was not good enough, because it wouldn't let recursive calls use the axioms. Therefore, the axioms were written to allow use at level 13, provided the arguments have been shown to satisfy CanCall.

So, expanding AXIOM_ACTIVATION and USE_VIA_CONTEXT, we now have that the general form of each of these axioms is the following (again, where 13 is the height of the function's SCC):

axiom
  13 <= FunctionHeight
  ==>
  (forall args ::
    F#CanCall(args) || (14 <= FunctionHeight && PRECONDITION)
    ==>
    //... what we really wanted to say about the function

The override axiom has a different form, namely:

axiom
  13 <= FunctionHeight
  ==>
  (forall args ::
    //... what we really wanted to say about the function

That is, the override axiom is stated at a particular level, without regard to the specific arguments (that is, no CanCall antecedent and no USE_VIA_CONTEXT antecedent). It's plausible (but hasn't been rigorously argued) that those other antecedents are not needed.

Now, back to the PR at hand. The solution is to perform the CheckWellformed checks without giving access to the override axiom, and to perform the OverrideCheck under the assumptions of the consequence (and definition and frame) axioms. To pull this off, we use two heights per level of the call-graph. So, for a function whose SCC is at level n, we do something like this:

property	(a) height at which checking procedure is performed	(b) axiom activiation lower bound	(c) use-via-context lower bound
Consequence	2*n	2*n	2*(n+1)
Definition	2*n	2*n	2*(n+1)
Override	2*n + 1	2*n + 1

From a table like this, one then argues soundness based on (a) <= (b) and (a) < (c). I think (but am not certain) this is what #3223 had done.

Then, it was discovered that this isn't good for overrides, because then there are really two levels at play: the level t of the overridden function (that is, the one in the parent trait) and the level c of the overriding function. Since the overridden function "calls" the overriding one, the construction of the call graph ensures t >= c, but the two can be equal.

In the current PR, what I'm observing for an overriding function is

property	(a)	(b)	(c)
Consequence	2*c + 1	2*c	2*(t+1)
Definition	2*c + 1	2*c	2*(c+1)
Override	2*c	2*c + 1

This table looks suspicious to me, since it doesn't satisfy (a) <= (b) for the consequence and definition axioms. Then again, perhaps one can argue that column (b) isn't important anyhow, since the axiom is still protected by the CanCall antecedent.

The fact that t is used only once in the table---in particular, the fact that it isn't used for the definition axiom---can be explained by that the parent trait does not give a body for the function. Dafny's overriding rules do not allow a type to give a different body if a parent trait has already provided a trait.

Finally, it's odd to me that the well-formedness checks are performed at a greater height than the override check. It would make sense to me to say "first, we check that the class gives a function that, by itself, is okay, and then we check that that function has a specification that allows it to be an override for the function in the parent trait". If so, the table should look more like

property	(a)	(b)	(c)
Consequence	2*c	2*c	2*(t+1)
Definition	2*c	2*c	2*(c+1)
Override	2*c + 1	?

And to replace the ? with something, I'm wondering if we don't actually need the CanCall or USE_VIA_CONTEXT antecedents after all.