For function postcondition violations, point to the problematic expression branch

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs

@@ -1560,10 +1560,10 @@ void CheckPostconditionForRhs(BoogieStmtListBuilder innerBuilder, Expression bod
         var letBody = Substitute(e.Body, null, substMap);
         CheckWellformed(letBody, wfOptions, locals, builder, etran);
         if (e.Constraint_Bounds != null) {
-          var substMapPrime = SetupBoundVarsAsLocals(lhsVars, builder, locals, etran);
+          var substMap2 = SetupBoundVarsAsLocals(lhsVars, builder, locals, etran);
           var nonGhostMapPrime = new Dictionary<IVariable, Expression>();
           foreach (BoundVar bv in lhsVars) {
-            nonGhostMapPrime.Add(bv, bv.IsGhost ? substMap[bv] : substMapPrime[bv]);
+            nonGhostMapPrime.Add(bv, bv.IsGhost ? substMap[bv] : substMap2[bv]);
           }
           var rhsPrime = Substitute(e.RHSs[0], null, nonGhostMapPrime);
           var letBodyPrime = Substitute(e.Body, null, nonGhostMapPrime);

Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs

@@ -120,7 +120,7 @@ public void Check(Function f) {
       // assume each one of them.  After all that (in particular, after assuming all
       // of them), do the postponed reads checks.
       delayer.DoWithDelayedReadsChecks(false, wfo => {
-        builder.Add(new CommentCmd("Check Wfness of preconditions, and then assume them"));
+        builder.Add(new CommentCmd("Check well-formedness of preconditions, and then assume them"));
         foreach (AttributedExpression require in f.Req) {
           if (require.Label != null) {
             require.Label.E = (f is TwoStateFunction ? ordinaryEtran : etran.Old).TrExpr(require.E);
@@ -135,14 +135,14 @@ public void Check(Function f) {
       // the preconditions.  In other words, the well-formedness of the reads clause is
       // allowed to assume the precondition (yet, the requires clause is checked to
       // read only those things indicated in the reads clause).
-      builder.Add(new CommentCmd("Check Wfness of the reads clause"));
+      builder.Add(new CommentCmd("Check well-formedness of the reads clause"));
       delayer.DoWithDelayedReadsChecks(false,
         wfo => { generator.CheckFrameWellFormed(wfo, f.Reads.Expressions, locals, builder, etran); });
 
       ConcurrentAttributeCheck(f, etran, builder);
 
       // check well-formedness of the decreases clauses (including termination, but no reads checks)
-      builder.Add(new CommentCmd("Check Wfness of the decreases clause"));
+      builder.Add(new CommentCmd("Check well-formedness of the decreases clause"));
       foreach (Expression p in f.Decreases.Expressions) {
         generator.CheckWellformed(p, new WFOptions(null, false), locals, builder, etran);
       }
@@ -172,7 +172,6 @@ public void Check(Function f) {
       generator.Reset();
     }
 
-    // TODO should be moved so its injected
     private void ConcurrentAttributeCheck(Function f, ExpressionTranslator etran, BoogieStmtListBuilder builder) {
       // If the function is marked as {:concurrent}, check that the reads clause is empty.
       if (Attributes.Contains(f.Attributes, Attributes.ConcurrentAttributeName)) {
@@ -208,7 +207,7 @@ private BoogieStmtListBuilder GetBodyCheckBuilder(Function f, ExpressionTranslat
       var selfCall = GetSelfCall(f, etran, parameters);
       var context = new BodyTranslationContext(f.ContainsHide);
       var bodyCheckBuilder = new BoogieStmtListBuilder(generator, generator.options, context);
-      bodyCheckBuilder.Add(new CommentCmd("Check Wfness of body and result subset type constraint"));
+      bodyCheckBuilder.Add(new CommentCmd("Check well-formedness of body and result subset type constraint"));
       if (f.Body != null && generator.RevealedInScope(f)) {
         var doReadsChecks = etran.readsFrame != null;
         var wfo = new WFOptions(null, doReadsChecks, doReadsChecks, false);
@@ -278,7 +277,7 @@ private Expr GetSelfCall(Function f, ExpressionTranslator etran, List<Variable>
     private BoogieStmtListBuilder GetPostCheckBuilder(Function f, ExpressionTranslator etran, List<Variable> locals) {
       var context = new BodyTranslationContext(f.ContainsHide);
       var postCheckBuilder = new BoogieStmtListBuilder(generator, generator.options, context);
-      postCheckBuilder.Add(new CommentCmd("Check Wfness of postcondition and assume false"));
+      postCheckBuilder.Add(new CommentCmd("Check well-formedness of postcondition and assume false"));
 
       // Assume the type returned by the call itself respects its type (this matters if the type is "nat", for example)
       var args = new List<Expr>();

Source/DafnyCore/Verifier/BoogieGenerator.Types.cs

@@ -1431,16 +1431,16 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) {
     // parameters of the procedure
     var inParams = MkTyParamFormals(decl.TypeArgs, true);
     Type baseType;
-    Bpl.Expr wh;
+    Bpl.Expr whereClause;
     if (decl.Var != null) {
       baseType = decl.Var.Type;
       Bpl.Type varType = TrType(baseType);
-      wh = GetWhereClause(decl.Var.tok, new Bpl.IdentifierExpr(decl.Var.tok, decl.Var.AssignUniqueName(decl.IdGenerator), varType), baseType, etran, NOALLOC);
+      whereClause = GetWhereClause(decl.Var.tok, new Bpl.IdentifierExpr(decl.Var.tok, decl.Var.AssignUniqueName(decl.IdGenerator), varType), baseType, etran, NOALLOC);
       // Do NOT use a where-clause in this declaration, because that would spoil the witness checking.
       inParams.Add(new Bpl.Formal(decl.Var.tok, new Bpl.TypedIdent(decl.Var.tok, decl.Var.AssignUniqueName(decl.IdGenerator), varType), true));
     } else {
       baseType = ((NewtypeDecl)decl).BaseType;
-      wh = null;
+      whereClause = null;
     }
 
     // the procedure itself
@@ -1487,7 +1487,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) {
     // }
 
     // check well-formedness of the constraint (including termination, and delayed reads checks)
-    var builderInitializationArea = CheckConstraintWellformedness(decl, context, etran, locals, builder);
+    var builderInitializationArea = CheckConstraintWellformedness(decl, context, whereClause, etran, locals, builder);
 
     // Check that the type is inhabited.
     // Note, the possible witness in this check should be coordinated with the compiler, so the compiler knows how to do the initialization
@@ -1507,15 +1507,16 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) {
             CheckResultToBeInType(result.Tok, result, decl.Var.Type, locals, returnBuilder, etran);
           }
 
+          // check that the witness is assignable to the type of the given bound variable
+          CheckResultToBeInType(decl.Witness.tok, decl.Witness, baseType, locals, witnessCheckBuilder, etran);
           // check that the witness expression checks out
-          witnessExpr = Substitute(decl.Constraint, decl.Var, result);
+          witnessExpr = decl.Constraint != null ? Substitute(decl.Constraint, decl.Var, decl.Witness) : null;
           witnessExpr.tok = result.Tok;
           var desc = new PODesc.WitnessCheck(witnessString, witnessExpr);
 
           SplitAndAssertExpression(returnBuilder, witnessExpr, etran, context, desc);
         });
       codeContext = ghostCodeContext;
-
     } else if (decl.WitnessKind == SubsetTypeDecl.WKind.CompiledZero) {
       var witness = Zero(decl.tok, baseType);
       if (witness == null) {
@@ -1524,8 +1525,8 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) {
       } else {
         // before trying 0 as a witness, check that 0 can be assigned to baseType
         witnessString = Printer.ExprToString(options, witness);
-        CheckResultToBeInType(decl.tok, witness, decl.Var.Type, locals, witnessCheckBuilder, etran, $"trying witness {witnessString}: ");
-        witnessExpr = Substitute(decl.Constraint, decl.Var, witness);
+        CheckResultToBeInType(decl.tok, witness, baseType, locals, witnessCheckBuilder, etran, $"trying witness {witnessString}: ");
+        witnessExpr = decl.Constraint != null ? Substitute(decl.Constraint, decl.Var, witness) : null;
 
         witnessExpr.tok = decl.tok;
         var desc = new PODesc.WitnessCheck(witnessString, witnessExpr);
@@ -1556,7 +1557,6 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) {
   private void SplitAndAssertExpression(BoogieStmtListBuilder witnessCheckBuilder, Expression witnessExpr,
     ExpressionTranslator etran, BodyTranslationContext context, PODesc.WitnessCheck desc) {
     witnessCheckBuilder.Add(new Bpl.AssumeCmd(witnessExpr.tok, etran.CanCallAssumption(witnessExpr)));
-    var witnessCheck = etran.TrExpr(witnessExpr);
 
     var ss = TrSplitExpr(context, witnessExpr, etran, true, out var splitHappened);
     if (!splitHappened) {
@@ -1572,13 +1572,26 @@ private void SplitAndAssertExpression(BoogieStmtListBuilder witnessCheckBuilder,
   }
 
   private BoogieStmtListBuilder CheckConstraintWellformedness(RedirectingTypeDecl decl, BodyTranslationContext context,
-    ExpressionTranslator etran, List<Variable> locals, BoogieStmtListBuilder builder) {
+    Bpl.Expr whereClause, ExpressionTranslator etran, List<Variable> locals, BoogieStmtListBuilder builder) {
     var constraintCheckBuilder = new BoogieStmtListBuilder(this, options, context);
     var builderInitializationArea = new BoogieStmtListBuilder(this, options, context);
-    var delayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, constraintCheckBuilder);
-    delayer.DoWithDelayedReadsChecks(false, wfo => {
-      CheckWellformedAndAssume(decl.Constraint, wfo, locals, constraintCheckBuilder, etran, "predicate subtype constraint");
-    });
+    if (decl.Constraint == null) {
+      constraintCheckBuilder.Add(new Bpl.CommentCmd($"well-formedness of {decl.WhatKind} constraint is trivial"));
+    } else {
+      constraintCheckBuilder.Add(new Bpl.CommentCmd($"check well-formedness of {decl.WhatKind} constraint"));
+      if (whereClause != null) {
+        constraintCheckBuilder.Add(new Bpl.AssumeCmd(decl.tok, whereClause));
+      }
+      var delayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, constraintCheckBuilder);
+      delayer.DoWithDelayedReadsChecks(false, wfo => {
+        CheckWellformedAndAssume(decl.Constraint, wfo, locals, constraintCheckBuilder, etran, "predicate subtype constraint");
+      });
+    }
+
+    // var delayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, constraintCheckBuilder);
+    // delayer.DoWithDelayedReadsChecks(false, wfo => {
+    //   CheckWellformedAndAssume(decl.Constraint, wfo, locals, constraintCheckBuilder, etran, "predicate subtype constraint");
+    // });
     PathAsideBlock(decl.Tok, constraintCheckBuilder, builder);
     return builderInitializationArea;
   }

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

@@ -1,4 +1,4 @@
 
-Dafny program verifier finished with 15 verified, 0 errors
-Total resources used is 26054889
-Max resources used by VC is 15592113
+Dafny program verifier finished with 272 verified, 0 errors
+Total resources used is 30533115
+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 15 verified, 0 errors
-Total resources used is 28044434
-Max resources used by VC is 16505967
+Dafny program verifier finished with 276 verified, 0 errors
+Total resources used is 28989931
+Max resources used by VC is 1092418

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804c.dfy

@@ -21,6 +21,6 @@ function Test(x: bool): int
         assert P(2) by { reveal p21; } // p21 can be revealed and this assertion is visible outside.
         2
     };
-  assert P(x); // No longer verifies since we scoped expression proofs
+  assert P(x);
   x
 }