Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Enable finer-grained control of redundant- and contradictory-assumption warnings #4778

Closed
alex-chew opened this issue Nov 15, 2023 · 7 comments · Fixed by #5001
Closed

Enable finer-grained control of redundant- and contradictory-assumption warnings #4778

alex-chew opened this issue Nov 15, 2023 · 7 comments · Fixed by #5001
Assignees
@atomb
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny

Comments

@alex-chew
Copy link
Contributor

Summary

No response

Background and Motivation

The --warn-redundant-assumptions and --warn-contradictory-assumptions options are useful for locating redundant and contradictory assumptions, but can generate false positives in nontrivial proofs. In some cases the proofs can be rewritten to avoid the warnings - but not always, it seems. It would be nice to be able to disable such warnings on a per-assertion (or per-declaration, or per-module) level.

Here is an excerpt from the Unicode libraries that generates contradictory-assumption warnings:

  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 {
        if m1 < m2 {
          // Here
          assert false by { assert m1 == m2[..|m1|]; }
        }
      }
    }
  }

The assert false near the end (labeled // Here) cannot be verified without the by { ... } portion. But the assertion within the by { ... } generates two warnings:

UnicodeEncodingForm.dfy(106,35): Error: proved using contradictory assumptions: assertion always holds
    |
106 |           assert false by { assert m1 == m2[..|m1|]; }
    |                                    ^^^^^^^^^^^^^^^^

UnicodeEncodingForm.dfy(106,41): Error: proved using contradictory assumptions: upper bound within range of sequence
    |
106 |           assert false by { assert m1 == m2[..|m1|]; }
    |                                          ^^^^^^^^^^

Proposed Feature

This feature could, for example, be implemented as attributes ({:warn_redundant_assumptions false}, etc.) that are valid in assertions and at the declaration-/module-level.

Alternatives

No response
@alex-chew alex-chew added the kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny label Nov 15, 2023
@alex-chew alex-chew mentioned this issue Nov 15, 2023
Merged
2 tasks
robin-aws pushed a commit that referenced this issue Nov 15, 2023
@alex-chew
feat: import Unicode libraries (#4780)
f81c316 
### Description
This PR imports the Unicode libraries from `dafny-lang/libraries`.

Notes:
- This disables redundant- and contradictory-assumptions warnings in
`dfyconfig.toml`, as not all of the many false-positives can be resolved
by rewriting existing proofs (as far as I can tell). We'll want to
re-enable them in the future, for example if/when [finer-grained
control](#4778) of such
warnings is possible.
- As a consequence of the above, verification performance of all the
libraries are subject to perturbation. This PR also makes some
non-Unicode-related changes to get other proofs to pass under the new
set of options.
- Because the `DafnyStdLibs` only supports a single set of verification
options right now, and we are proceeding with `--unicode-char:true`, the
`UnicodeStringsWithoutUnicodeChar` module is not included in this PR.
@atomb atomb self-assigned this Nov 16, 2023
@atomb atomb mentioned this issue Dec 11, 2023
Open
@atomb
Copy link
Member

atomb commented Jan 5, 2024

I'm wondering whether a more general {:nowarn ...} attribute might make sense, and that this could be an instance of it (perhaps the only one, at first). Do others have thoughts on that?

@keyboardDrummer
Copy link
Member

Do others have thoughts on that?

Should we not first understand why we're getting warnings for the above proof, before adding an option to turn them off? I didn't find this explanation in the issue details.

@atomb
Copy link
Member

atomb commented Jan 8, 2024

Ah, I guess it wasn't explicit here because @alex-chew and I discussed it offline. We do understand what's going on. The specific example above is an intentional proof by contradiction, which will always give rise to warnings about proof using contradictory assumptions. Because such proofs are legitimate, we fundamentally need a way to indicate that they're intentional.

We could have something specific to the case of contradictory assumptions (marking something as an intentional proof by contradiction in some way). But we also want something for redundant assumptions that, for whatever reason, the developer decides they want to keep. And, while we're at it, I expect there are other warnings we may want to be able to disable on a local basis.

@keyboardDrummer
Copy link
Member

keyboardDrummer commented Jan 8, 2024 •
edited
Loading

The specific example above is an intentional proof by contradiction, which will always give rise to warnings about proof using contradictory assumptions.

I thought it wouldn't produce warnings because you added an exception for assert false so that the false part is not marked unused even though the statement can not be reached, and I thought the by clause of assert false doesn't get to rely on the result of assert false, so it's not marked as contradictory.

How come there's a contradictory warning in this case?

@keyboardDrummer
Copy link
Member

keyboardDrummer commented Jan 8, 2024 •
edited
Loading

But we also want something for redundant assumptions that, for whatever reason, the developer decides they want to keep. And, while we're at it, I expect there are other warnings we may want to be able to disable on a local basis.

I hope I'm not being too cautious here, but I'd rather see these cases explicitly before adding features to cover them.

In C# for example, there's a warning you get when you call a method that returns a Task, and you do not await this task.

There's a C# feature added so you can avoid this warning, which is to assign to _, so it looks like _ = ReturnsATask(). Without this feature, users could get the same effect by adding a pragma that disables the warning, but I much prefer the _ = code because the warning disabling pragma does not feel super maintainable to me.

@atomb
Copy link
Member

atomb commented Jan 17, 2024

The specific example above is an intentional proof by contradiction, which will always give rise to warnings about proof using contradictory assumptions.

I thought it wouldn't produce warnings because you added an exception for assert false so that the false part is not marked unused even though the statement can not be reached, and I thought the by clause of assert false doesn't get to rely on the result of assert false, so it's not marked as contradictory.

How come there's a contradictory warning in this case?

Unfortunately, triggers make things complicated. It's possible to have a case where assert B; assert false; succeeds but assert false; on its own does not, because Z3 needs something in B to trigger a quantifier instantiation. However, the actual assertion is not part of the proof in this case because triggers are a way of controlling the search process, not part of the final proof produced. If you decide to instead write this assert false by { assert B; }, you wind up with the same problem. The surrounding context is already contradictory, but Z3 just can't prove that until it sees B. Once it sees B, it can prove that the context is contradictory and that B was therefore proved using contradictory assumptions. So, I think we fundamentally need a way to mark such assertions, which guide the triggering process to prove a contradiction, as things not to warn about when they're intentional.

@keyboardDrummer
Copy link
Member

keyboardDrummer commented Jan 22, 2024 •
edited
Loading

@atomb clear explanation! Thank you

Some follow-up questions. Is there a textbook example of this problem? Or does it happen mostly by coincidence? Does this problem also occur in idiomatic Dafny code?

So, I think we fundamentally need a way to mark such assertions, which guide the triggering process to prove a contradiction, as things not to warn about when they're intentional.

Seems like a simple solution. If there is a more automatic one we can always introduce that later.

atomb added a commit to atomb/dafny that referenced this issue Jan 22, 2024
@atomb
Implement a proof-by-contradiction attribute
cccf11c 
Allows a particular assertion to be marked as an intentional proof by
contradiction, preventing `--warn-contradictory-assumptions` from
flagging it.

Fixes dafny-lang#4778
@atomb atomb mentioned this issue Jan 22, 2024
Merged
atomb added a commit that referenced this issue Jan 31, 2024
@atomb
Implement a proof-by-contradiction attribute (#5001)
8221c9d 
### 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@atomb atomb

Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Implement a proof-by-contradiction attribute atomb/dafny
3 participants
@atomb @keyboardDrummer @alex-chew