Implement a proof-by-contradiction attribute

Source/DafnyCore/ProofDependencyWarnings.cs

@@ -102,6 +102,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/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