Feat: Better format in hover messages (#3687)

Fixes #3686

- Added the trace of proof even in successes
- Replaced intermediate "Could not prove" and "Did prove" by "Inside "
to indicate this is just a trace
- Use backticks to indicate quoted code
- Better error message instead of "error is impossible: This is the
precondition that might not hold"
- First-class support of {:error} in hover messages.
- BONUS: Not described in the issue: Hover support for `{:error}` in
failed postconditions.

Acts as a precursor to #3324 by harmonizing the change made in boogie
"might not hold" => "could not be proved" in preconditions and
postconditions
```
before: function precondition might not hold
after:  function precondition could not be proved

before: the calculation step between the previous line and this line might not hold
after:  the calculation step between the previous line and this line could not be proved

before: This postcondition might not hold on a return path.
after:  this postcondition could not be proved on a return path
```

The screenshots of the issue are now fixed w.r.t. the described errors.

![image](https://user-images.githubusercontent.com/3601079/222830841-be6e4157-fc1d-44b1-bf8c-603efe6146e4.png)

![image](https://user-images.githubusercontent.com/3601079/222830776-6edb430d-7765-4f52-860b-c5a8f4221f7e.png)

With support for `{:error}` in postconditions

![image](https://user-images.githubusercontent.com/3601079/222868101-f2956c8e-8d54-4fe5-ad54-6ca7b02cd701.png)

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/AST/Substituter.cs

@@ -3,7 +3,6 @@
 using System.Diagnostics.Contracts;
 using System.Linq;
 using JetBrains.Annotations;
-using Microsoft.Boogie.Clustering;
 
 namespace Microsoft.Dafny {
   /// <summary>

Source/DafnyCore/Verifier/ProofObligationDescription.cs

@@ -2,7 +2,7 @@
 using System.Diagnostics.Contracts;
 using System.Linq;
 using JetBrains.Annotations;
-using Microsoft.CodeAnalysis.CSharp.Syntax;
+using Microsoft.Boogie;
 
 namespace Microsoft.Dafny.ProofObligationDescription;
 
@@ -294,57 +294,99 @@ public IsOlderProofObligation(int olderParameterCount, int allParameterCount) {
 
 //// Contract constraints
 
-public class PreconditionSatisfied : ProofObligationDescriptionWithNoExpr {
+public abstract class ProofObligationDescriptionCustomMessages : ProofObligationDescriptionWithNoExpr {
+  protected readonly string customErrMsg;
+  private readonly string customSuccessMsg;
+
   public override string SuccessDescription =>
-    customErrMsg is null
-      ? "function precondition satisfied"
-      : $"error is impossible: {customErrMsg}";
+    customSuccessMsg ?? DefaultSuccessDescription;
 
+  public abstract string DefaultSuccessDescription { get; }
   public override string FailureDescription =>
-    customErrMsg ?? "function precondition might not hold";
+    customErrMsg ?? DefaultFailureDescription;
+  public abstract string DefaultFailureDescription { get; }
+  public ProofObligationDescriptionCustomMessages([CanBeNull] string customErrMsg, [CanBeNull] string customSuccessMsg) {
+    this.customErrMsg = customErrMsg;
+    this.customSuccessMsg = customSuccessMsg;
+  }
+}
 
-  public override string ShortDescription => "precondition";
+public class PreconditionSatisfied : ProofObligationDescriptionCustomMessages {
+  public override string DefaultSuccessDescription =>
+    "function precondition satisfied";
 
-  private readonly string customErrMsg;
+  public override string DefaultFailureDescription =>
+    "function precondition could not be proved";
 
-  public PreconditionSatisfied([CanBeNull] string customErrMsg) {
-    this.customErrMsg = customErrMsg;
+  public override string ShortDescription => "precondition";
+
+  public PreconditionSatisfied([CanBeNull] string customErrMsg, [CanBeNull] string customSuccessMsg)
+    : base(customErrMsg, customSuccessMsg) {
   }
 }
 
-public class AssertStatement : ProofObligationDescriptionWithNoExpr {
-  public override string SuccessDescription =>
-    customErrMsg is null
-      ? "assertion always holds"
-      : $"error is impossible: {customErrMsg}";
+public class AssertStatement : ProofObligationDescriptionCustomMessages {
+  public override string DefaultSuccessDescription =>
+    "assertion always holds";
 
-  public override string FailureDescription =>
-    customErrMsg ?? "assertion might not hold";
+  public override string DefaultFailureDescription =>
+    "assertion might not hold";
 
   public override string ShortDescription => "assert statement";
 
-  private readonly string customErrMsg;
+  public AssertStatement([CanBeNull] string customErrMsg, [CanBeNull] string customSuccessMsg)
+    : base(customErrMsg, customSuccessMsg) {
+  }
+}
 
-  public AssertStatement([CanBeNull] string customErrMsg) {
-    this.customErrMsg = customErrMsg;
+// The Boogie version does not support custom error messages yet
+public class RequiresDescription : ProofObligationDescriptionCustomMessages {
+  public override string DefaultSuccessDescription =>
+    "the precondition always holds";
+
+  public override string DefaultFailureDescription =>
+    "this is the precondition that could not be proved";
+
+  public override string ShortDescription => "requires";
+
+  public RequiresDescription([CanBeNull] string customErrMsg, [CanBeNull] string customSuccessMsg)
+    : base(customErrMsg, customSuccessMsg) {
   }
 }
 
-public class LoopInvariant : ProofObligationDescriptionWithNoExpr {
-  public override string SuccessDescription =>
-    customErrMsg is null
-      ? "loop invariant always holds"
-      : $"error is impossible: {customErrMsg}";
+// The Boogie version does not support custom error messages yet
+public class EnsuresDescription : ProofObligationDescriptionCustomMessages {
+  public override string DefaultSuccessDescription =>
+    "this postcondition holds";
 
-  public override string FailureDescription =>
-    customErrMsg ?? "loop invariant violation";
+  public override string DefaultFailureDescription =>
+    "this is the postcondition that could not be proved";
 
-  public override string ShortDescription => "loop invariant";
+  // Same as FailureDescription but used not as a "related" error, but as an error by itself
+  public string FailureDescriptionSingle =>
+    customErrMsg ?? "this postcondition could not be proved on a return path";
 
-  private readonly string customErrMsg;
+  public string FailureAtPathDescription =>
+    customErrMsg ?? new PostconditionDescription().FailureDescription;
 
-  public LoopInvariant([CanBeNull] string customErrMsg) {
-    this.customErrMsg = customErrMsg;
+  public override string ShortDescription => "ensures";
+
+  public EnsuresDescription([CanBeNull] string customErrMsg, [CanBeNull] string customSuccessMsg)
+    : base(customErrMsg, customSuccessMsg) {
+  }
+}
+
+public class LoopInvariant : ProofObligationDescriptionCustomMessages {
+  public override string DefaultSuccessDescription =>
+"loop invariant always holds";
+
+  public override string DefaultFailureDescription =>
+    "loop invariant violation";
+
+  public override string ShortDescription => "loop invariant";
+
+  public LoopInvariant([CanBeNull] string customErrMsg, [CanBeNull] string customSuccessMsg)
+    : base(customErrMsg, customSuccessMsg) {
   }
 }
 
@@ -353,7 +395,7 @@ public class CalculationStep : ProofObligationDescriptionWithNoExpr {
     "the calculation step between the previous line and this line always holds";
 
   public override string FailureDescription =>
-    "the calculation step between the previous line and this line might not hold";
+    "the calculation step between the previous line and this line could not be proved";
 
   public override string ShortDescription => "calc step";
 }
@@ -999,8 +1041,8 @@ public override Expression GetAssertedExpr(DafnyOptions options) {
     var bvarsExprs = bvars.Select(bvar => new IdentifierExpr(bvar.tok, bvar)).ToList();
     var bvarprimes = bvars.Select(bvar => new BoundVar(bvar.tok, bvar.Name + "'", bvar.Type)).ToList();
     var bvarprimesExprs = bvarprimes.Select(bvar => new IdentifierExpr(bvar.tok, bvar) as Expression).ToList();
-    var subContract = new Substituter(null,
-      bvars.Zip(bvarprimesExprs).ToDictionary<(BoundVar, Expression), IVariable, Expression>(
+    var subContract = new Substituter(null, Enumerable.Zip(
+      bvars, bvarprimesExprs).ToDictionary<(BoundVar, Expression), IVariable, Expression>(
         item => item.Item1, item => item.Item2),
       new Dictionary<TypeParameter, Type>()
     );

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

@@ -889,13 +889,13 @@ private void AddFunctionOverrideCheckImpl(Function f) {
       // the procedure itself
       var req = new List<Boogie.Requires>();
       // free requires fh == FunctionContextHeight;
-      req.Add(Requires(f.tok, true, etran.HeightContext(f), null, null));
+      req.Add(Requires(f.tok, true, etran.HeightContext(f), null, null, null));
       if (f is TwoStateFunction) {
         // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap)
         var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr);
         var a1 = HeapSucc(prevHeap, currHeap);
         var a2 = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, currHeap);
-        req.Add(Requires(f.tok, true, BplAnd(a0, BplAnd(a1, a2)), null, null));
+        req.Add(Requires(f.tok, true, BplAnd(a0, BplAnd(a1, a2)), null, null, null));
       }
       // modifies $Heap
       var mod = new List<Boogie.IdentifierExpr> {
@@ -1439,13 +1439,13 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
       // FREE PRECONDITIONS
       if (kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation || kind == MethodTranslationKind.OverrideCheck) {  // the other cases have no need for a free precondition
         // free requires mh == ModuleContextHeight && fh == FunctionContextHeight;
-        req.Add(Requires(m.tok, true, etran.HeightContext(m), null, null));
+        req.Add(Requires(m.tok, true, etran.HeightContext(m), null, null, null));
         if (m is TwoStateLemma) {
           // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap)
           var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr);
           var a1 = HeapSucc(prevHeap, currHeap);
           var a2 = FunctionCall(m.tok, BuiltinFunction.IsGoodHeap, null, currHeap);
-          req.Add(Requires(m.tok, true, BplAnd(a0, BplAnd(a1, a2)), null, null));
+          req.Add(Requires(m.tok, true, BplAnd(a0, BplAnd(a1, a2)), null, null, null));
         }
       }
       if (m is TwoStateLemma) {
@@ -1457,7 +1457,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
             var pIdx = m.Ins.Count == 1 ? "" : " at index " + index;
             var desc = new PODesc.IsAllocated($"parameter{pIdx} ('{formal.Name}')", "in the two-state lemma's previous state");
             var require = Requires(formal.tok, false, MkIsAlloc(etran.TrExpr(dafnyFormalIdExpr), formal.Type, prevHeap),
-              desc.FailureDescription, null);
+              desc.FailureDescription, desc.SuccessDescription, null);
             require.Description = desc;
             req.Add(require);
           }
@@ -1472,7 +1472,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
         // USER-DEFINED SPECIFICATIONS
         var comment = "user-defined preconditions";
         foreach (var p in m.Req) {
-          string errorMessage = CustomErrorMessage(p.Attributes);
+          var (errorMessage, successMessage) = CustomErrorMessage(p.Attributes);
           if (p.Label != null && kind == MethodTranslationKind.Implementation) {
             // don't include this precondition here, but record it for later use
             p.Label.E = (m is TwoStateLemma ? ordinaryEtran : etran.Old).TrExpr(p.E);
@@ -1483,7 +1483,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
               } else if (s.IsOnlyFree && !bodyKind) {
                 // don't include in split -- it would be ignored, anyhow
               } else {
-                req.Add(Requires(s.Tok, s.IsOnlyFree, s.E, errorMessage, comment));
+                req.Add(Requires(s.Tok, s.IsOnlyFree, s.E, errorMessage, successMessage, comment));
                 comment = null;
                 // the free here is not linked to the free on the original expression (this is free things generated in the splitting.)
               }
@@ -1492,8 +1492,8 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
         }
         comment = "user-defined postconditions";
         foreach (var p in m.Ens) {
-          string errorMessage = CustomErrorMessage(p.Attributes);
-          AddEnsures(ens, Ensures(p.E.tok, true, CanCallAssumption(p.E, etran), errorMessage, comment));
+          var (errorMessage, successMessage) = CustomErrorMessage(p.Attributes);
+          AddEnsures(ens, Ensures(p.E.tok, true, CanCallAssumption(p.E, etran), errorMessage, successMessage, comment));
           comment = null;
           foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) {
             var post = s.E;
@@ -1506,16 +1506,16 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
             } else if (s.IsOnlyChecked && !bodyKind) {
               // don't include in split
             } else {
-              AddEnsures(ens, Ensures(s.Tok, s.IsOnlyFree || this.assertionOnlyFilter != null, post, errorMessage, null));
+              AddEnsures(ens, Ensures(s.Tok, s.IsOnlyFree || this.assertionOnlyFilter != null, post, errorMessage, successMessage, null));
             }
           }
         }
         if (m is Constructor && kind == MethodTranslationKind.Call) {
           var fresh = Boogie.Expr.Not(etran.Old.IsAlloced(m.tok, new Boogie.IdentifierExpr(m.tok, "this", TrReceiverType(m))));
-          AddEnsures(ens, Ensures(m.tok, false || this.assertionOnlyFilter != null, fresh, null, "constructor allocates the object"));
+          AddEnsures(ens, Ensures(m.tok, false || this.assertionOnlyFilter != null, fresh, null, null, "constructor allocates the object"));
         }
         foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, m.AllowsAllocation, ordinaryEtran.Old, ordinaryEtran, ordinaryEtran.Old)) {
-          AddEnsures(ens, Ensures(tri.tok, tri.IsFree || this.assertionOnlyFilter != null, tri.Expr, tri.ErrorMessage, tri.Comment));
+          AddEnsures(ens, Ensures(tri.tok, tri.IsFree || this.assertionOnlyFilter != null, tri.Expr, tri.ErrorMessage, tri.SuccessMessage, tri.Comment));
         }
 
         // add the fuel assumption for the reveal method of a opaque method
@@ -1533,11 +1533,11 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
                 Boogie.Expr layer = etran.layerInterCluster.LayerN(1, moreFuel_expr);
                 Boogie.Expr layerAssert = etran.layerInterCluster.LayerN(2, moreFuel_expr);
 
-                AddEnsures(ens, Ensures(m.tok, true, Boogie.Expr.Eq(startFuel, layer), null, null));
-                AddEnsures(ens, Ensures(m.tok, true, Boogie.Expr.Eq(startFuelAssert, layerAssert), null, null));
-                AddEnsures(ens, Ensures(m.tok, true, GetRevealConstant(f), null, null));
+                AddEnsures(ens, Ensures(m.tok, true, Boogie.Expr.Eq(startFuel, layer), null, null, null));
+                AddEnsures(ens, Ensures(m.tok, true, Boogie.Expr.Eq(startFuelAssert, layerAssert), null, null, null));
+                AddEnsures(ens, Ensures(m.tok, true, GetRevealConstant(f), null, null, null));
 
-                AddEnsures(ens, Ensures(m.tok, true, Boogie.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.AsFuelBottom, null, moreFuel_expr), moreFuel_expr), null, "Shortcut to LZ"));
+                AddEnsures(ens, Ensures(m.tok, true, Boogie.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.AsFuelBottom, null, moreFuel_expr), moreFuel_expr), null, null, "Shortcut to LZ"));
               }
             }
           }

Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs

@@ -567,7 +567,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
             if (!fnCoreType.IsArrowTypeWithoutPreconditions) {
               // check precond
               var precond = FunctionCall(e.tok, Requires(arity), Bpl.Type.Bool, args);
-              builder.Add(Assert(GetToken(expr), precond, new PODesc.PreconditionSatisfied(null)));
+              builder.Add(Assert(GetToken(expr), precond, new PODesc.PreconditionSatisfied(null, null)));
             }
 
             if (wfOptions.DoReadsChecks && !fnCoreType.IsArrowTypeWithoutReadEffects) {
@@ -698,16 +698,16 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
               // check that the preconditions for the call hold
               foreach (AttributedExpression p in e.Function.Req) {
                 Expression precond = Substitute(p.E, e.Receiver, substMap, e.GetTypeArgumentSubstitutions());
-                string errorMessage = CustomErrorMessage(p.Attributes);
+                var (errorMessage, successMessage) = CustomErrorMessage(p.Attributes);
                 foreach (var ss in TrSplitExpr(precond, etran, true, out var splitHappened)) {
                   if (ss.IsChecked) {
                     var tok = new NestedToken(GetToken(expr), ss.Tok);
-                    var desc = new PODesc.PreconditionSatisfied(errorMessage);
+                    var desc = new PODesc.PreconditionSatisfied(errorMessage, successMessage);
                     if (wfOptions.AssertKv != null) {
                       // use the given assert attribute only
-                      builder.Add(Assert(tok, ss.E, new PODesc.PreconditionSatisfied(errorMessage), wfOptions.AssertKv));
+                      builder.Add(Assert(tok, ss.E, new PODesc.PreconditionSatisfied(errorMessage, successMessage), wfOptions.AssertKv));
                     } else {
-                      builder.Add(AssertNS(tok, ss.E, new PODesc.PreconditionSatisfied(errorMessage)));
+                      builder.Add(AssertNS(tok, ss.E, new PODesc.PreconditionSatisfied(errorMessage, successMessage)));
                     }
                   }
                 }

Source/DafnyCore/Verifier/Translator.TrStatement.cs

@@ -518,7 +518,7 @@ private void TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder,
       Contract.Requires(etran != null);
 
       var stmtBuilder = new BoogieStmtListBuilder(this, options);
-      string errorMessage = CustomErrorMessage(stmt.Attributes);
+      var (errorMessage, successMessage) = CustomErrorMessage(stmt.Attributes);
       this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, stmt.Tok, this.fuelContext, this.reporter);
       var defineFuel = DefineFuelConstant(stmt.Tok, stmt.Attributes, stmtBuilder, etran);
       var b = defineFuel ? stmtBuilder : builder;
@@ -548,14 +548,14 @@ private void TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder,
         var ss = TrSplitExpr(stmt.Expr, etran, true, out var splitHappened);
         if (!splitHappened) {
           var tok = enclosingToken == null ? GetToken(stmt.Expr) : new NestedToken(enclosingToken, GetToken(stmt.Expr));
-          var desc = new PODesc.AssertStatement(errorMessage);
+          var desc = new PODesc.AssertStatement(errorMessage, successMessage);
           (proofBuilder ?? b).Add(Assert(tok, etran.TrExpr(stmt.Expr), desc, stmt.Tok,
             etran.TrAttributes(stmt.Attributes, null)));
         } else {
           foreach (var split in ss) {
             if (split.IsChecked) {
               var tok = enclosingToken == null ? split.E.tok : new NestedToken(enclosingToken, split.Tok);
-              var desc = new PODesc.AssertStatement(errorMessage);
+              var desc = new PODesc.AssertStatement(errorMessage, successMessage);
               (proofBuilder ?? b).Add(AssertNS(ToDafnyToken(tok), split.E, desc, stmt.Tok,
                 etran.TrAttributes(stmt.Attributes, null))); // attributes go on every split
             }
@@ -1405,20 +1405,20 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr,
       }
       BoogieStmtListBuilder invDefinednessBuilder = new BoogieStmtListBuilder(this, options);
       foreach (AttributedExpression loopInv in s.Invariants) {
-        string errorMessage = CustomErrorMessage(loopInv.Attributes);
+        var (errorMessage, successMessage) = CustomErrorMessage(loopInv.Attributes);
         TrStmt_CheckWellformed(loopInv.E, invDefinednessBuilder, locals, etran, false);
         invDefinednessBuilder.Add(TrAssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));
 
         invariants.Add(TrAssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, CanCallAssumption(loopInv.E, etran))));
         var ss = TrSplitExpr(loopInv.E, etran, false, out var splitHappened);
         if (!splitHappened) {
           var wInv = Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E));
-          invariants.Add(Assert(loopInv.E.tok, wInv, new PODesc.LoopInvariant(errorMessage)));
+          invariants.Add(Assert(loopInv.E.tok, wInv, new PODesc.LoopInvariant(errorMessage, successMessage)));
         } else {
           foreach (var split in ss) {
             var wInv = Bpl.Expr.Binary(split.E.tok, BinaryOperator.Opcode.Imp, w, split.E);
             if (split.IsChecked) {
-              invariants.Add(Assert(split.Tok, wInv, new PODesc.LoopInvariant(errorMessage)));  // TODO: it would be fine to have this use {:subsumption 0}
+              invariants.Add(Assert(split.Tok, wInv, new PODesc.LoopInvariant(errorMessage, successMessage)));  // TODO: it would be fine to have this use {:subsumption 0}
             } else {
               invariants.Add(TrAssumeCmd(split.E.tok, wInv));
             }