Implement a proof-by-contradiction attribute (#5001)

### Description

Allows a particular assertion to be marked as an intentional proof by
contradiction, preventing `--warn-contradictory-assumptions` from
flagging it.

Fixes #4778

### How has this been tested?

`Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4778.dfy`

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

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -238,13 +238,14 @@ public enum GeneralTraitsOptions {
     "Emits a warning if the name of a declared variable caused another variable to be shadowed.");
   public static readonly Option<bool> WarnContradictoryAssumptions = new("--warn-contradictory-assumptions", @"
 (experimental) Emits a warning if any assertions are proved based on contradictory assumptions (vacuously).
-May slow down verification slightly.
-May produce spurious warnings.") {
+May slow down verification slightly, or make it more brittle.
+May produce spurious warnings.
+Use the `{:contradiction}` attribute to mark any `assert` statement intended to be part of a proof by contradiction.") {
     IsHidden = true
   };
   public static readonly Option<bool> WarnRedundantAssumptions = new("--warn-redundant-assumptions", @"
 (experimental) Emits a warning if any `requires` clause or `assume` statement was not needed to complete verification.
-May slow down verification slightly.
+May slow down verification slightly, or make it more brittle.
 May produce spurious warnings.") {
     IsHidden = true
   };

Source/DafnyCore/ProofDependencyWarnings.cs

@@ -40,8 +40,11 @@ public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions
       if (dafnyOptions.Get(CommonOptionBag.WarnContradictoryAssumptions)) {
         if (unusedDependency is ProofObligationDependency obligation) {
           if (ShouldWarnVacuous(dafnyOptions, logEntry.Name, obligation)) {
-            reporter.Warning(MessageSource.Verifier, "", obligation.Range,
-              $"proved using contradictory assumptions: {obligation.Description}");
+            var msg = $"proved using contradictory assumptions: {obligation.Description}";
+            var rest = obligation.ProofObligation is AssertStatementDescription
+                     ? ". (Use the `{:contradiction}` attribute on the `assert` statement to silence.)"
+                     : "";
+            reporter.Warning(MessageSource.Verifier, "", obligation.Range, msg + rest);
           }
         }
 
@@ -105,6 +108,10 @@ private static bool ShouldWarnVacuous(DafnyOptions options, string verboseName,
           lit == false) {
         return false;
       }
+
+      if (poDep.ProofObligation is AssertStatementDescription { IsIntentionalContradiction: true }) {
+        return false;
+      }
     }
 
     // Ensures clauses are often proven vacuously during well-formedness checks.

Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs

@@ -597,14 +597,14 @@ private void TrAssertStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, Lis
       var splits = 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(stmt.Expr, errorMessage, successMessage);
+        var desc = new PODesc.AssertStatementDescription(assertStmt, errorMessage, successMessage);
         (proofBuilder ?? b).Add(Assert(tok, etran.TrExpr(stmt.Expr), desc, stmt.Tok,
           etran.TrAttributes(stmt.Attributes, null)));
       } else {
         foreach (var split in splits) {
           if (split.IsChecked) {
             var tok = enclosingToken == null ? split.E.tok : new NestedToken(enclosingToken, split.Tok);
-            var desc = new PODesc.AssertStatement(stmt.Expr, errorMessage, successMessage);
+            var desc = new PODesc.AssertStatementDescription(assertStmt, errorMessage, successMessage);
             (proofBuilder ?? b).Add(AssertNS(ToDafnyToken(flags.ReportRanges, tok), split.E, desc, stmt.Tok,
               etran.TrAttributes(stmt.Attributes, null))); // attributes go on every split
           }

Source/DafnyCore/Verifier/ProofObligationDescription.cs

@@ -331,7 +331,7 @@ public PreconditionSatisfied([CanBeNull] string customErrMsg, [CanBeNull] string
   }
 }
 
-public class AssertStatement : ProofObligationDescriptionCustomMessages {
+public class AssertStatementDescription : ProofObligationDescriptionCustomMessages {
   public override string DefaultSuccessDescription =>
     "assertion always holds";
 
@@ -341,14 +341,20 @@ public class AssertStatement : ProofObligationDescriptionCustomMessages {
   public override string ShortDescription => "assert statement";
 
   public override Expression GetAssertedExpr(DafnyOptions options) {
-    return predicate;
+    return AssertStatement.Expr;
   }
 
-  private Expression predicate;
+  public AssertStmt AssertStatement { get; }
 
-  public AssertStatement(Expression predicate, [CanBeNull] string customErrMsg, [CanBeNull] string customSuccessMsg)
+  // We provide a way to mark an assertion as an intentional element of a
+  // proof by contradiction with the `{:contradiction}` attribute. Dafny
+  // skips warning about such assertions being proved due to contradictory
+  // assumptions.
+  public bool IsIntentionalContradiction => Attributes.Contains(AssertStatement.Attributes, "contradiction");
+
+  public AssertStatementDescription(AssertStmt assertStmt, [CanBeNull] string customErrMsg, [CanBeNull] string customSuccessMsg)
     : base(customErrMsg, customSuccessMsg) {
-    this.predicate = predicate;
+    this.AssertStatement = assertStmt;
   }
 
   public override bool IsImplicit => false;

Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs

@@ -34,7 +34,7 @@ public async Task RedundantAssumptionsGetWarnings() {
       Assert.Contains(diagnostics, diagnostic =>
         diagnostic.Severity == DiagnosticSeverity.Warning &&
         diagnostic.Range == new Range(13, 11, 13, 17) &&
-        diagnostic.Message == "proved using contradictory assumptions: assertion always holds"
+        diagnostic.Message == "proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.)"
       );
       Assert.Contains(diagnostics, diagnostic =>
         diagnostic.Severity == DiagnosticSeverity.Warning &&

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

@@ -0,0 +1,39 @@
+// RUN: %verify --warn-contradictory-assumptions "%s" > "%t"
+// DIFF: "%s.expect" "%t"
+
+type CodeUnit
+type CodeUnitSeq = seq<CodeUnit>
+type MinimalWellFormedCodeUnitSeq = s: CodeUnitSeq
+  | IsMinimalWellFormedCodeUnitSubsequence(s)
+  witness *
+
+function IsMinimalWellFormedCodeUnitSubsequence(s: CodeUnitSeq): (b: bool)
+  ensures b ==>
+            && |s| > 0
+            && forall i | 0 < i < |s| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i])
+  decreases |s|
+
+/**
+ * If minimal well-formed code unique subsequences `m1` and `m2` are prefixes of `s`, then they are equal.
+ */
+lemma LemmaUniquePrefixMinimalWellFormedCodeUnitSeq(
+  s: CodeUnitSeq, m1: MinimalWellFormedCodeUnitSeq, m2: MinimalWellFormedCodeUnitSeq
+)
+  decreases |s|, |m1|, |m2|
+  requires m1 <= s
+  requires m2 <= s
+  ensures m1 == m2
+{
+  // Handle only the |m1| <= |m2| case explicitly
+  if |m1| > |m2| {
+    LemmaUniquePrefixMinimalWellFormedCodeUnitSeq(s, m2, m1);
+  } else {
+    assert m1 <= m2;
+    assert m1 == m2 by {
+      var m2' := m2[..|m1|];
+      if m1 < m2 {
+        assert {:contradiction} m1 == m2';
+      }
+    }
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4778.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 2 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect

@@ -1,12 +1,12 @@
 ProofDependencies.dfy(176,11): Warning: unnecessary (or partly unnecessary) assume statement
 ProofDependencies.dfy(185,11): Warning: unnecessary (or partly unnecessary) assume statement
-ProofDependencies.dfy(186,13): Warning: proved using contradictory assumptions: assertion always holds
+ProofDependencies.dfy(186,13): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.)
 ProofDependencies.dfy(191,11): Warning: unnecessary (or partly unnecessary) assume statement
-ProofDependencies.dfy(193,13): Warning: proved using contradictory assumptions: assertion always holds
-ProofDependencies.dfy(202,11): Warning: proved using contradictory assumptions: assertion always holds
+ProofDependencies.dfy(193,13): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.)
+ProofDependencies.dfy(202,11): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.)
 ProofDependencies.dfy(203,4): Warning: proved using contradictory assumptions: value always satisfies the subset constraints of 'nat'
 ProofDependencies.dfy(209,10): Warning: ensures clause proved using contradictory assumptions
-ProofDependencies.dfy(211,11): Warning: proved using contradictory assumptions: assertion always holds
+ProofDependencies.dfy(211,11): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.)
 ProofDependencies.dfy(212,11): Warning: proved using contradictory assumptions: value always satisfies the subset constraints of 'nat'
 ProofDependencies.dfy(226,11): Warning: unnecessary requires clause
 ProofDependencies.dfy(241,11): Warning: unnecessary requires clause

docs/DafnyRef/Attributes.md

@@ -851,6 +851,10 @@ method Test()
 
 The success message is optional but is recommended if errorMessage is set.
 
+### 11.4.6. `{:contradiction}`
+
+Silences warnings about this assertion being involved in a proof using contradictory assumptions when `--warn-contradictory-assumptions` is enabled. This allows clear identification of intentional proofs by contradiction.
+
 ## 11.5. Attributes on variable declarations
 
 ### 11.5.1. `{:assumption}` {#sec-assumption}

docs/DafnyRef/UserGuide.md

@@ -1505,12 +1505,15 @@ included in the proof.
 
 * Contradictory assumptions. If the combination of all assumptions in
   scope at a particular program point is contradictory, anything can be
-  proved at that point. This indicates the serious situation that, unless done on purpose like in a proof by contradiction, your
-  proof may be entirely vacuous, and not say what you intended, giving
+  proved at that point. This indicates the serious situation that,
+  unless done on purpose in a proof by contradiction, your proof may be
+  entirely vacuous. It therefore may not say what you intended, giving
   you a false sense of confidence. The
   `--warn-contradictory-assumptions` flag instructs Dafny to warn about
   any assertion that was proved through the use of contradictions
-  between assumptions.
+  between assumptions. If a particular `assert` statement is part of an
+  intentional proof by contradiction, annotating it with the
+  `{:contradiction}` attribute will silence this warning.
 
 These options can be specified in `dfyconfig.toml`, and this is typically the most convenient way to use them with the IDE.
 

docs/dev/news/5001.feat

@@ -0,0 +1 @@
+The new `{:contradiction}` attribute can be placed on an `assert` statement to indicate that it forms part of an intentional proof by contradiction and therefore shouldn't be warned about when `--warn-contradictory-assumptions` is turned on.