fix: Frame and termination checks are now subject to by-proofs of method calls

Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs

@@ -1912,48 +1912,6 @@ void ProcessCallStmt(CallStmt cs, Dictionary<TypeParameter, Type> tySubst, Bpl.E
         }
       }
 
-      var directSub = new Substituter(null, directSubstMap, tySubst);
-
-      // Check that the reads clause of a subcall is a subset of the current reads frame,
-      // but support the optimization that we don't define a reads frame at all if it's `reads *`. 
-      if (etran.readsFrame != null) {
-        // substitute actual args for parameters in description expression frames...
-        var requiredFrames = callee.Reads.Expressions.ConvertAll(directSub.SubstFrameExpr);
-        var desc = new PODesc.ReadFrameSubset("call", requiredFrames, GetContextReadsFrames());
-
-        // ... but that substitution isn't needed for frames passed to CheckFrameSubset
-        var readsSubst = new Substituter(null, new Dictionary<IVariable, Expression>(), tySubst);
-        CheckFrameSubset(tok, callee.Reads.Expressions.ConvertAll(readsSubst.SubstFrameExpr),
-          receiver, substMap, etran, etran.ReadsFrame(tok), builder, desc, null);
-      }
-      // Check that the modifies clause of a subcall is a subset of the current modifies frame,
-      // but only if we're in a context that defines a modifies frame.
-      if (codeContext is IMethodCodeContext methodCodeContext) {
-        // substitute actual args for parameters in description expression frames...
-        var desc = new PODesc.ModifyFrameSubset(
-          "call",
-          callee.Mod.Expressions.ConvertAll(directSub.SubstFrameExpr),
-          methodCodeContext.Modifies.Expressions
-        );
-        // ... but that substitution isn't needed for frames passed to CheckFrameSubset
-        var modifiesSubst = new Substituter(null, new(), tySubst);
-        CheckFrameSubset(
-          tok, callee.Mod.Expressions.ConvertAll(modifiesSubst.SubstFrameExpr),
-          receiver, substMap, etran, etran.ModifiesFrame(tok), builder, desc, null);
-      }
-
-      // Check termination
-      if (isRecursiveCall) {
-        Contract.Assert(codeContext != null);
-        if (codeContext is DatatypeDecl) {
-          builder.Add(Assert(tok, Bpl.Expr.False, new PODesc.IsNonRecursive()));
-        } else {
-          List<Expression> contextDecreases = codeContext.Decreases.Expressions;
-          List<Expression> calleeDecreases = callee.Decreases.Expressions;
-          CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, directSubstMap, tySubst, etran, true, builder, codeContext.InferredDecreases, null);
-        }
-      }
-
       // Create variables to hold the output parameters of the call, so that appropriate unboxes can be introduced.
       var outs = new List<Bpl.IdentifierExpr>();
       var tmpOuts = new List<Bpl.IdentifierExpr>();
@@ -1990,7 +1948,7 @@ void ProcessCallStmt(CallStmt cs, Dictionary<TypeParameter, Type> tySubst, Bpl.E
       }
 
       void AddCall(BoogieStmtListBuilder callBuilder) {
-        callBuilder.Add(new CommentCmd($"ProcessCallStmt: Check precondition"));
+        callBuilder.Add(new CommentCmd("ProcessCallStmt: Check precondition"));
         // Make the call
         AddReferencedMember(callee);
         Bpl.CallCmd call = Call(tok, MethodName(callee, isCoCall ? MethodTranslationKind.CoCallPre : MethodTranslationKind.CallPre), ins, new List<Bpl.IdentifierExpr>());
@@ -2006,6 +1964,50 @@ void AddCall(BoogieStmtListBuilder callBuilder) {
           call.IsFree = true;
         }
         callBuilder.Add(call);
+
+        callBuilder.Add(new CommentCmd("ProcessCallStmt: Check frame and termination"));
+
+        var directSub = new Substituter(null, directSubstMap, tySubst);
+
+        // Check that the reads clause of a subcall is a subset of the current reads frame,
+        // but support the optimization that we don't define a reads frame at all if it's `reads *`.
+        if (etran.readsFrame != null) {
+          // substitute actual args for parameters in description expression frames...
+          var requiredFrames = callee.Reads.Expressions.ConvertAll(directSub.SubstFrameExpr);
+          var desc = new PODesc.ReadFrameSubset("call", requiredFrames, GetContextReadsFrames());
+
+          // ... but that substitution isn't needed for frames passed to CheckFrameSubset
+          var readsSubst = new Substituter(null, new Dictionary<IVariable, Expression>(), tySubst);
+          CheckFrameSubset(tok, callee.Reads.Expressions.ConvertAll(readsSubst.SubstFrameExpr),
+            receiver, substMap, etran, etran.ReadsFrame(tok), callBuilder, desc, null);
+        }
+        // Check that the modifies clause of a subcall is a subset of the current modifies frame,
+        // but only if we're in a context that defines a modifies frame.
+        if (codeContext is IMethodCodeContext methodCodeContext) {
+          // substitute actual args for parameters in description expression frames...
+          var desc = new PODesc.ModifyFrameSubset(
+            "call",
+            callee.Mod.Expressions.ConvertAll(directSub.SubstFrameExpr),
+            methodCodeContext.Modifies.Expressions
+          );
+          // ... but that substitution isn't needed for frames passed to CheckFrameSubset
+          var modifiesSubst = new Substituter(null, new(), tySubst);
+          CheckFrameSubset(
+            tok, callee.Mod.Expressions.ConvertAll(modifiesSubst.SubstFrameExpr),
+            receiver, substMap, etran, etran.ModifiesFrame(tok), callBuilder, desc, null);
+        }
+
+        // Check termination
+        if (isRecursiveCall) {
+          Contract.Assert(codeContext != null);
+          if (codeContext is DatatypeDecl) {
+            callBuilder.Add(Assert(tok, Bpl.Expr.False, new PODesc.IsNonRecursive()));
+          } else {
+            List<Expression> contextDecreases = codeContext.Decreases.Expressions;
+            List<Expression> calleeDecreases = callee.Decreases.Expressions;
+            CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, directSubstMap, tySubst, etran, true, callBuilder, codeContext.InferredDecreases, null);
+          }
+        }
       }
 
       builder.Add(new CommentCmd("ProcessCallStmt: Make the call"));

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy

@@ -64,4 +64,16 @@ greatest lemma F(x: int)
 {
   F(x-2) by { ProveP(); }
   assert P(); // should fail
+}
+
+method H(x: int, y: int, s: set<object>, t: set<object>)
+  requires y % 2 == 0
+  modifies s
+  decreases x
+{
+  H(y, x, t, t) by {
+    assume x % 2 == 0; // to prove the precondition of the call
+    assume t <= s; // to prove the modifies clause of the call
+    assume 0 <= y < x; // to prove termination of the call
+  }
 }

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect

@@ -5,4 +5,4 @@ CallBy.dfy(50,10): Error: assertion might not hold
 CallBy.dfy(56,10): Error: assertion might not hold
 CallBy.dfy(66,10): Error: assertion might not hold
 
-Dafny program verifier finished with 3 verified, 6 errors
+Dafny program verifier finished with 5 verified, 6 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect

@@ -31,5 +31,5 @@ CoinductiveProofs.dfy(208,21): Related location: this is the postcondition that
 CoinductiveProofs.dfy(4,23): Related location: this proposition could not be proved
 
 Dafny program verifier finished with 23 verified, 12 errors
-Total resources used is 770731
+Total resources used is 775252
 Max resources used by VC is 60262

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect

@@ -1,4 +1,4 @@
 
 Dafny program verifier finished with 272 verified, 0 errors
-Total resources used is 30533110
+Total resources used is 30537041
 Max resources used by VC is 2074326

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect

@@ -1,4 +1,4 @@
 
 Dafny program verifier finished with 276 verified, 0 errors
-Total resources used is 28989926
+Total resources used is 28984183
 Max resources used by VC is 1092418