Implement a proof-by-contradiction attribute

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.