Fix: substitution of binding guards does not crash if splits present

[MikaelMayer]

This PR fixes #2748
I think it's a correct solution, at least locally, because there was previously a recursion which would just replace the comprehension by its split quantifier equivalent. That was obviously wrong for quantifiers which were split into a binary expression
Since it wanted to do it on an equivalent sub-comprehension, I removed the recursive call and it should have the same effect. At least, the test now passes.

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

[keyboardDrummer]

Do I read correctly that with this change, after substitution, SplitQuantifierExpression becomes null even if it was non-null?

[MikaelMayer]

Correct, but to avoid any doubts about that, note it was also the case before, as for "substituting" we were essentially returning the .SplitQuantifierExpression, whose .SplitQuantifierExpression is itself null.

[keyboardDrummer]

Sure, but that does seem quite different, because now the translation to SplitQuantifierExpression is lost. Are you sure we're not missing a test-case? Could we come up with a proof that requires the quantifier expression to be split and that is substituted?

[MikaelMayer]

I'm sure of one thing, this code was wrong, because it assumed that the .SplitQuantifierExpression was a ComprehensionExpr.
Let's analyse that. Take a deep breath.

If q.SplitQuantifierExpression is a ComprehensionExpr. it means that there was no splitting at all. This is because any split would make that q.SplitExpressions would be a list of length >= 2 and thus the generated .SplitQuantifierExpression would HAVE to be a binary expression
Hence the q.SplitQuantifierExpression is equal to the expression itself, minus the .SplitQuantifier which is now null (splitted quantifier expressions are not themselves splitted)
However, the remaining of SubstituteComprehensionExpr does not access .SplitQuantifier nor .SplitQuantifierExpression after line 937. Thus, accessing the .SplitQuantifierExpression is useless.

So, for the existing case where e.SplitQuantifierExpression is a ComprehensionExpr, the code does the same.

Now, note that my change only changes anything when forceSubstituteOfBoundVars is set to false.
If you look at the three call sites, two set forceSubstituteOfBoundVars to false - binding guard if statements and binding guard if expressions, and one set forceSubstituteOfBoundVars to true - all the other places.

So, in essence, forceSubstituteOfBoundVars is set to false in this context because we are in a binding guard, and the reason why we don't want to force substituting bound variables is that these variables are used afterwards in the body of the if. By the way, when forceSubstituteOfBoundVars == false, the bound variables are still substituted, it's just that the current scope's variables substitutation map is updated.

In conclusion when translating a binding guard, it makes sense to preserve its atomic quantifier-ness and discard splitted expressions. After all, splitted expressions are useful primarly for proving smaller assertions, but since it's a guard here, we don't need to split, since there is nothing to prove.
The only thing that we want to prove might be the existence and unicity of such an assignment, but these assertions appear outside of a binding guard, and thus can be splitted as normal (forceSubstituteOfBoundVars == true)

[keyboardDrummer]

Do you know why forceSubstituteOfBoundVars must sometimes be true? It looks like not forcing it is more performant and in the binding guard case, more correct, but apparently I'm missing something.

I'm also confused by the existing expression !forceSubstituteOfBoundVars in

if (newBoundVars != e.BoundVars || newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes ||
          newBounds != e.Bounds || !forceSubstituteOfBoundVars) {

In conclusion when translating a binding guard, it makes sense to preserve its atomic quantifier-ness and discard splitted expressions.

Could we make that decision more explicit in the code? Something like:

// forceSubstituteOfBoundVars is implicitly always true here.
SubstituteComprehensionExpr(ComprehensionExpr expr) {
      var q = e as QuantifierExpr;
      if (q != null && q.SplitQuantifier != null) {
          return Substitute(q.SplitQuantifierExpression);
      }
      SubstituteComprehensionExprIgnoringSplits(expr, true);
}

// Called from binding guard situations
SubstituteComprehensionExprDiscardingSplits(ComprehensionExpr expr, bool forceSubstituteOfBoundVars) {
    ...
}

[MikaelMayer]

isBindingGuard is not only used to determine if we can discard splits or not, it's also used later when substituting variables. Do you really think it would be appropriate to transform the following:

var newBoundVars = CreateBoundVarSubstitutions(e.BoundVars, forceSubstitutionOfBoundVariables: !isBindingGuard && (expr is ForallExpr || expr is ExistsExpr || expr is SetComprehension));

to

var newBoundVars = CreateBoundVarSubstitutions(e.BoundVars, forceSubstitutionOfBoundVariables: !discardSplits && (expr is ForallExpr || expr is ExistsExpr || expr is SetComprehension));

?
I have a hard time swallowing the second. It seems that the first one conveys the direct meaning that we are not forcing substitution because we are in a binding guard. But the second one makes a hard case: why discarding splits would result in not forcing substitution of bound variables?
We discard splits because we are in a binding guard AND we don't force substitution because we are in a binding guard. But not forcing variable substitution does not seem directly linked to discarding splits, does it?

[keyboardDrummer]

I have a hard time swallowing the second. It seems that the first one conveys the direct meaning that we are not forcing substitution because we are in a binding guard. But the second one makes a hard case: why discarding splits would result in not forcing substitution of bound variables?
We discard splits because we are in a binding guard AND we don't force substitution because we are in a binding guard. But not forcing variable substitution does not seem directly linked to discarding splits, does it?

I agree, but I'm also not suggesting the second version.

I think ideally Substitutor doesn't discard splits, because that's not what you expect based on the name Substitutor. It should just substitute, not discard. How do you feel about the two alternatives that I suggested in #2968 (comment), of which neither discards the splits?

If you think discarding splits is something that needs to happen for binding guards to make them work correctly, that's fine, but let's not do it implicitly in Substitutor.

[MikaelMayer]

We should have never created splits for binding guard in the first place, that's the point of this PR. Let me bring a fresh solution to our problem, so that I don't have to worry about the code of the substituter which sparks debate.

Let's review your two suggestions so that I explain to you my point of view

protected Expression SubstituteComprehensionExpr(ComprehensionExpr expr) {

  var newSplits = e switch {
    QuantifierExpr { SplitQuantifier: { } splits } => splits.Select(Substitute).ToList(),
    _ => null
  };
  ...
}

The problem with this suggestion is that, in the case of a binding guard, the two spitted quantifiers will be assigned variables whose scope will never be the one of the body of an if..

public virtual Expression Substitute(Expression expr, bool forceSubstituteOfBoundVars) {
  ...
}

protected Expression SubstituteComprehensionExpr(ComprehensionExpr expr) {

  var newSplits = e switch {
    QuantifierExpr { SplitQuantifier: { } splits } => 
      splits.Select(split => Substitute(split, forceSubstituteOfBoundVars)).ToList(),
    _ => null
  };
  ...
}

Here we are introducing a complexity that I don't understand. Why do we add a function to force substitute of bound vars in the global substitute function? Replacing bound variables is a purely local decision, not a variable that traverses a set of expressions. Again, it does not make sense to traverse the splits and forcing or not the substitute of bound vars in a splitted quantifier for a guard, because it did not make sense anyway that the guard be splitted if they are binding guard.

So here is my new approach. I completely reverted my changes to Substituter.cs (so that there is no debate on how to handle seemingly weirdly designed features that were out of scope of this PR).
Instead, I changed the QuantifierSplitter class, that was blindly splitting all quantifiers (except those with {:split false}) to ensure quantifiers just below a if guard (statement or expression) are not splitted.
That solved the trick.

[keyboardDrummer]

Thanks, I like the new approach.

Any chance we can also refactor SubstituteComprehensionExpr to the 'first approach', to make substitutor more consistent with its name and avoid future discussion about it?

protected Expression SubstituteComprehensionExpr(ComprehensionExpr expr) {

  var newSplits = e switch {
    QuantifierExpr { SplitQuantifier: { } splits } => splits.Select(Substitute).ToList(),
    _ => null
  };
  ...
}

[MikaelMayer]

Any chance we can also refactor SubstituteComprehensionExpr to the 'first approach', to make substitutor more consistent with its name and avoid future discussion about it?

Seems like a good idea, but then the semantics of substituter would change, and that might impact verification in various places. I agree that the substituter shoujld not have inlined the split expressions when substituting, this is a really weird design. However, if this inlining is not done here, it must be done somewhere else, and I think that will require more discussion. Let's keep that for a future discussion.

[cpitclaudel]

I haven't followed the details of this PR, but we discussed this issue in depth with @jtristan a little while back in the comments of #2745 ; is there anything helpful there?

[MikaelMayer]

I haven't followed the details of this PR, but we discussed this issue in depth with @jtristan a little while back in the comments of #2745 ; is there anything helpful there?

Yes that was helpful. Basically, this conversation confirms my analysis above
https://github.com/dafny-lang/dafny/pull/2745/files#r971378730
Basically, in the PR you mentioned, it was only a code refactoring to ensure that binding guards had a different treatment, but it never addressed the issue that the split quantifier expression was not a quantifier by itself.
And your comment was right: we can just omit the second case. It was there only to ensure the previous behavior, but I agree with you it did not have any reason to stay.