Include rewrite antecedents in CanCall assumptions

[RustanLeino]

Fixes #6158
Fixes #6183

This PR fixes an unsoundness that came about from a bad interaction between quantifier rewrites and CanCall assumptions.

The need to rewrite quantifiers

To describe the issue and the fix, consider a user-provided quantifier

forall  x :: Q(x, F(x-1), F(x))

As written, this quantifier has no good triggers, because x-1 involves the interpreted symbol - and F(x) would give rise to a matching loop via F(x-1). To nevertheless try to make this quantifier work, Dafny rewrites it into

forall x, tmp :: tmp == x-1 ==> Q(x, F(tmp), F(x))

This quantifier has a trigger {F(tmp), F(x)}. The reason this is a good trigger is that it does not generate any new F terms -- both F(tmp) and F(x) had to have already existed before the quantifier is triggered.

VC generation for rewritten quantifiers

During VC generation, expressions are processed in 3 major ways. One is to translate the expression into Boogie form; this uses the rewritten quantifier. Another is to generate Boogie code that checks the well-formedness of the expression; this uses the original (non-rewritten) quantifier. The third is to produce various assumptions as consequences of the expression being well-formed; these go under the name "CanCall assumptions" (even though they also include assumptions that are unrelated to CanCall), and these present a problem for rewritten quantifiers.

The problem is that the "definition" of the new variable tmp is introduced as an antecedent of the quantifier body. I'll refer to these as antecedent definitions. The RHS of the equality tmp == e in the antecedent definition may, in Dafny, not be well-formed. For example, suppose the original quantifier were

forall  x :: 1 <= x ==> F(G(x-1)) <= F(x)

where G is a function that takes a nat.

In general, it would be difficult to get this antecedent closer to the place where the variable is used, because the expression being replaced (here, G(x-1)) may be deeply nested inside an arbitrary expression--it is for this reason that the antecedent definition is placed at the outermost level in the first place. Soundness requires the CanCall assumptions to be generated for the same expression that has been checked for well-formedness. For example, it would be unsound to generate the CanCall assumption for the Dafny expression

forall x, tmp :: tmp == G(x-1) ==> 1 <= x ==> F(tmp) <= F(x)

because that would give

(forall x: int, tmp: int ::
  CanCall$G(x-1) && 
  (tmp == G(x-1) ==> 1 <= x ==> CanCall$F(tmp) && CanCall$F(x)))

despite the fact that x-1 is not certain to meet the precondition of G.

In conclusion, it is not possible to generate CanCall assumptions from the rewritten quantifier. (Yet, that's what was being done, leading to the unsoundness #6158.)

So, then, what about generate CanCall assumptions from the original (non-rewritten) quantifier? This also doesn't work, because the CanCall assumption will be a universal quantifier that needs a trigger, and the whole reason for the rewrite in the first place was that the original quantifier does not have a good trigger.

First attempt

My first attempt a solving this brought up a learning point that is worth recording.

In that first attempt, I tried storing away the original body along with the

To be continued...

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