fix: Cross-modular override check

[fabiomadge]

Fixes #2500.

To achieve this, we first give the override axiom the visibility of the overriding function. To ensure we only use the axiom in case we pass the check, we introduce an intermediate visibility level. The ensures clause of the overridden function can reference the underlying function, so we need to substitute the overridden function by the overriding function in the override check.

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

[RustanLeino]

The fix looks good. Please add some test cases.

[RustanLeino]

I suggest making a SCCPredecessorCountToFunctionHeight method that performs the ... * 2 + 1 computation. And I guess the + 1 should then also be controlled by a boolean, like you're doing in HeightContext, etc.

[RustanLeino]

These two should be in the other order. That is, it should first check that the postcondition of the trait holds, and only then should it be given the information J.F(ins) == C.F(ins).

[fabiomadge]

The comment is outdated. There is no assume anymore. (At least not of that equality.)

[RustanLeino]

Here's another place for that ... * 2 + 0-or-1 method.

[RustanLeino]

And here, too. In this instance, it would make it clear that the + 1 is indeed placed in the right place.

[RustanLeino]

I don't find hidden to be such a good description. Can you make the name more descriptive? Or, if not, add a comment that describes it.

[RustanLeino]

I know Rider keeps saying the Bpl. is not necessary. I guess it's fine to get rid of it, but I've been fine with seeing the prefix, since it reminds me that Bpl.Expr is not Expression.

[RustanLeino]

I think this replaces too many occurrences of the function. For example, I suspect it will make the following override verify, but it mustn't:

trait Tr {
  function F(x: nat, other: Tr): int
    ensures x != 0 && other.F(x - 1, other) < 20 ==> F(x, other) % 2 == other.F(x - 1, other) % 2
}

class Cl extends Tr {
  function F(x: nat, other: Tr): int
    ensures 50 <= F(x, other)
}

Note that the calls other.F(x - 1, other) should not be changed by the substitution.

[RustanLeino]

Good. I like this ... * 2 + 1 < ... better than the (... + 1) * 2 <= ....

[RustanLeino]

Also add some tests that use the function itself (rather than the named result value ret), since those cases may be tricky.

[robin-aws]

Great simple solution, and appreciate the helpful comments and code cleanup along the way!

I assume we don't need the same solution for pre-conditions as well, since the equality axiom comes after the assertion in that case?

[robin-aws]

Suggested change

	ensures d(y) < 20 + y // error: specification is not weaker
	ensures d(y) < 20 + y // error: specification is weaker

And likewise throughout - unless I'm confused this was already wrong in the original comments you copied.

[robin-aws]

Suggested change

	// Missing: ensures ret != 0
	// Missing: ensures ret

[robin-aws]

Nit: consider using "intermediateScope" here instead, or renaming the parameter, for consistency.

[robin-aws]

Still a TODO or have you fixed it?

[fabiomadge]

Neither? I couldn't find a situation where it affects the way I use it, Boogie has more shallow types, but there may be others, where getting this right is crucial.

[robin-aws]

I'd add a comment about how this is a negative test of the limitations of the current substitution approach.

Also this is fine but it would be good to have a version that's "obviously true" to humans as well, to be clearer about the limitation, like:

module M {
  trait {:termination false} Tr {
    ...
    function True'': (ret: bool) ensures True''()
  }
}

class Class extends M.Tr {
  ...
  function True'': (ret: bool) ensures (var alsoThis := this; alsoThis.True''())
  { true }
}

[fabiomadge]

This is a positive test, as the ensures is a tautology. If we weren't careful when lowering Other the, the override check could pass. I did add a version of your suggestion nevertheless and it uncovered an issue.