Feat: `assert {:only}` to temporarily work on a single assertion #3933

MikaelMayer · 2023-05-01T14:42:28Z

This PR fixes #3095 by introducing assert {:only}. As stated in the documentation:

assert {:only} X; temporarily transforms all other non-{:only} assertions in the surrounding declaration into assumptions.

method Test() {
  assert true;                  // Unchecked
  assert {:only} true by {      // Checked
    assert true;                // Checked
  }
  assert true;                  // Unchecked
  assert {:only "after"} true;  // Checked
  assert true;                  // Checked
  assert {:only "before"} true; // Checked
  assert true;                  // Unchecked
}

{:only} can help focusing on a particular proof or a particular branch, as it transforms not only other explicit assertions, but also other implicit assertions, and call requirements, into assumptions.
Since it's meant to be a temporary construct, it always emits a warning.
It also has two variants assert {:only "before"} and assert {:only "after"}.
Here is precisely how Dafny determines what to verify or not.
{:only} annotations define "verification interval" which are visual:

assert {:only} X [by {...} | ;] sets a verification interval that starts at the keyword assert and ends either at the end of the proof } or the semicolon ;, depending on which variant of assert is being used.
assert {:only} ... inside an other verification interval removes that verification interval and sets a new one.
assert {:only "before"} ... inside another verification interval finishes that verification interval earlier at the end of this assertion. Outside verification intervals, it sets a verification interval from the beginning of the declaration to the end of this assertion, but only if there were no other verification intervals before.
assert {:only "after"} ... inside another verification interval moves the start of that verification interval to the start of this new assert. Outside verification interval, it sets a verification interval from the beginning of this assert to the end of the declaration.

The start of an asserted expression is used to determines if it's inside a verification interval or not.
For example, in assert B ==> (assert {:only "after"} true; C), C is actually the start of the asserted expression, so it is verified because it's after assert {:only "after"} true.

As soon as a declaration contains one assert {:only}, none of the postconditions are verified; you'd need to explicit them with assertions if you wanted to verify them at the same time.

Integration

I updated the auditor to report usages of assert {:only}
I updated the doc
I added a code action to suggest to remove the {:only ...} in VSCode.

Alternatives considered

It's currently possible to use {:selective_checking true} on a declaration and and {:start_checking_there} on an assertion to "comment out" all previous assertions.
However, this mechanism is not suitable for us, even transpiling our attributes to that, for the following reasons:. It works at the Boogie level, but at the Dafny level it's often misleading. For example, {:start_checking_there} on an assert {:start_checking_there} X by { Y } will actually start checking X but not the proof Y because in Boogie the proof is written before the assertion.

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

…dafny into fix-3095-assert-only

atomb

This is a feature I expect I'll use frequently. :) I had a few nits about wording, and a broader comment about whether the notion of "range" used here is the right one. It might be, but I'm not yet 100% convinced.

atomb · 2023-05-02T20:52:12Z

Source/DafnyCore/Auditor/Assumption.cs


+ public static AssumptionDescription AssertOnly = new(


Could you use field labels here for consistency with the other instances above? In particular, it's hard to remember which of the bool fields is which without the labels. :)

Could you use field labels here for consistency with the other instances above? In particular, it's hard to remember which of the bool fields is which without the labels. :)

Indeed, I hadn't seen that these labels weren't explicit as my IDE displays them if they are not provided ^^. That made review more confusing than necessary.

Oh, right! Sometimes helpful things aren't as helpful. :)

atomb · 2023-05-02T20:57:47Z

Source/DafnyCore/Resolver/ResolutionErrors.cs

+ static ResolutionErrors() {
+ Add(ErrorId.r_assert_only_assumes_others,
+ @"
+When annotating an assert with the `{:only}` attribute, all other implicit and explicit assertions


Suggested change

When annotating an assert with the `{:only}` attribute, all other implicit and explicit assertions

When annotating an assertion with the `{:only}` attribute, all other implicit and explicit assertions

atomb · 2023-05-02T20:58:04Z

Source/DafnyCore/Resolver/ResolutionErrors.cs

+ Add(ErrorId.r_assert_only_assumes_others,
+ @"
+When annotating an assert with the `{:only}` attribute, all other implicit and explicit assertions
+are assumed. This is a way to focus on an assertion and its proof, but this annotation has to be removed once finished.


Suggested change

are assumed. This is a way to focus on an assertion and its proof, but this annotation has to be removed once finished.

are transformed into assumptions. This is a way to focus on an assertion and its proof, but this annotation has to be removed once finished.

atomb · 2023-05-02T20:58:37Z

Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs

+
+ if (assertStmt != null && Attributes.Find(assertStmt.Attributes, "only") is UserSuppliedAttributes attribute) {
+ reporter.Warning(MessageSource.Verifier, ResolutionErrors.ErrorId.r_assert_only_assumes_others.ToString(), attribute.RangeToken.ToToken(),
+ "Assertion with {:only} temporarily transforms other assertions in assumptions");


Suggested change

"Assertion with {:only} temporarily transforms other assertions in assumptions");

"Assertion with {:only} temporarily transforms other assertions into assumptions");

atomb · 2023-05-02T21:00:51Z

docs/DafnyRef/Attributes.md

+Since it's meant to be a temporary construct, it always emits a warning.
+It also has two variants `assert {:only "before"}` and `assert {:only "after"}`.
+Here is precisely how Dafny determines what to verify or not.
+`{:only}` annotations define "verification interval" which are visual:


Suggested change

`{:only}` annotations define "verification interval" which are visual:

Each `{:only}` annotation defines a "verification interval" which is visual:

atomb · 2023-05-02T21:04:19Z

Source/DafnyCore/Verifier/Translator.cs

@@ -3240,6 +3240,7 @@ class Specialization {
 bool inBodyInitContext = false; // true during the translation of the .BodyInit portion of a divided constructor body
 readonly Dictionary<string, Bpl.IdentifierExpr> definiteAssignmentTrackers = new Dictionary<string, Bpl.IdentifierExpr>();
 bool assertAsAssume = false; // generate assume statements instead of assert statements
+ Func<IToken, bool> assertionOnlyFilter = null; // generate assume statements instead of assert statements if not targetted by {:only}


Suggested change

Func<IToken, bool> assertionOnlyFilter = null; // generate assume statements instead of assert statements if not targetted by {:only}

Func<IToken, bool> assertionOnlyFilter = null; // generate assume statements instead of assert statements if not targeted by {:only}

atomb · 2023-05-02T21:05:36Z

Source/DafnyCore/Verifier/Translator.cs

@@ -7296,7 +7297,9 @@ public ForceCheckToken(IToken tok)
 Contract.Requires(condition != null);
 Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);

- if (assertAsAssume || (RefinementToken.IsInherited(refinesToken, currentModule) && (codeContext == null || !codeContext.MustReverify))) {
+ if (assertAsAssume
+ || (assertionOnlyFilter != null && !assertionOnlyFilter(tok))


Convenient that this code was already here, and you just had to add another condition under which to enable it! :)

atomb · 2023-05-02T21:06:22Z

Source/DafnyCore/Generic/ErrorRegistry.cs

@@ -26,6 +26,7 @@ public record DafnyAction(string Title, IReadOnlyList<DafnyCodeActionEdit> Edits

 public static class ErrorRegistry {

+ // Replace any NoneId by ParseErrors.p_... or ResolutionErrors.r_


I'm not sure I understand this comment, or why it's in this PR.

I came across warnings and errors which were using ErrorRegistry.NoneId as identifier. However, at first, I did not know how to put an identifier that has some meaning, so I had to do research and found out that meaningful identifiers are actually defined in ParseErrors.p_.... so I created the same for ResolutionErrors.r_.... and put a comment so that if a resolution error is using ErrorRegistry.NoneId and someone wants to create a rich error (e.g. that contains extended error text or a code action), they know where to go and what to do.

atomb · 2023-05-02T22:09:10Z

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

+ m.Visit(node => {
+ if (node is AssertStmt assertStmt && Attributes.Find(assertStmt.Attributes, "only") is UserSuppliedAttributes attribute) {
+ var (isBefore, isAfter) = attribute.Args.Count == 1 && attribute.Args[0] is LiteralExpr { Value: var value } &&
+ value is "after" or "before" ? (value is "before", value is "after") : (false, false);


If it were me, I'd move the logic for extracting the {:only} attribute to a separate definition. Then maybe you'd have a datatype AssertOnlyKind = After | Before | Only and a bool HasAssertOnlyAttribute(out var assertOnlyKind), or something like that.

atomb · 2023-05-02T22:14:06Z

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

@@ -1353,6 +1355,49 @@ public partial class Translator {
 builder.Add(Assert(tok, q, new PODesc.TraitFrame(m.WhatKind, true), kv));
 }

+ // Return a way to know if an assertion should be converted to an assumptions


The notion of "before" and "after" here seems potentially confusing. For instance, if you were to say assert {:only "before"} P; in the else branch of an if statement, it would enable assertions in the other branch of the if statement. It's a simple notion, though, so perhaps the strangeness of it isn't fatal.

Yeah I thought about that too. The advantage is that the notions are straightforward indeed for now. I primarily envision users to use {:only} by itself for a single proof, and if they really want, they can delimit without surprise which assertions should be verified using {:only "before"} and {:only "after"}. It's just that I had to give meaning to single instances of {:only "before"} and {:only "after"}.

I also thought of a more coarse-grained numerical notion of "level", which is one that @jtristan suggested one day. For example, assert {:only 0} will be the same as assert {:only}, whereas assert {:only 1} will define a verification interval on the surrounding block, assert {:only 2} on the block containing that block, etc. Because we traverse the program using a visitor pattern and nodes, this would be quite easy to implement.
If you like this idea, that would make three of us to like it so I would happily implement it as part of this PR.

Yeah, that makes sense. And adding those would be backward-compatible, so no need to hold up this PR for it.

atomb

Thanks for implementing this!

MikaelMayer added 5 commits April 28, 2023 10:03

Add test for issue #3095

c301337

Added documentation

233116c

Feat: assert {:only} to temporarily work on a single assertion

bad2568

More precision regarding postconditions

2b9a028

more precise semantics for before

01d682c

MikaelMayer requested a review from atomb May 1, 2023 14:42

MikaelMayer self-assigned this May 1, 2023

MikaelMayer and others added 12 commits May 1, 2023 09:54

Merge branch 'master' into fix-3095-assert-only

d2cfaac

fixed documentation

6a8fce3

Merge branch 'master' into fix-3095-assert-only

a4910ba

Added auditing capabilities

a7a8fcb

FIXER:auditor/TestAuditor.dfy

12badde

Support for auditor

ec26568

Merge branch 'fix-3095-assert-only' of https://github.com/dafny-lang/…

2d71399

…dafny into fix-3095-assert-only

Merge branch 'master' into fix-3095-assert-only

9ed7e8c

Merge branch 'master' into fix-3095-assert-only

66e5ca1

FIXER:separate-verification/assumptions.dfy

40c74fe

Fixed a CI test related to auditor

29ce7ce

Merge branch 'master' into fix-3095-assert-only

2548085

atomb requested changes May 2, 2023

View reviewed changes

review comments + check about only argument

2161269

atomb approved these changes May 3, 2023

View reviewed changes

Merge branch 'master' into fix-3095-assert-only

b8024ef

MikaelMayer enabled auto-merge (squash) May 3, 2023 15:29

Merge branch 'master' into fix-3095-assert-only

a6fe5fc

MikaelMayer merged commit e47bb85 into master May 3, 2023
19 checks passed

MikaelMayer deleted the fix-3095-assert-only branch May 3, 2023 17:51

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Feat: `assert {:only}` to temporarily work on a single assertion #3933

Feat: `assert {:only}` to temporarily work on a single assertion #3933

MikaelMayer commented May 1, 2023 •

edited

Loading

atomb left a comment

atomb May 2, 2023

MikaelMayer May 3, 2023

atomb May 3, 2023

atomb May 2, 2023

atomb May 2, 2023

atomb May 2, 2023

atomb May 2, 2023

atomb May 2, 2023

atomb May 2, 2023

atomb May 2, 2023

MikaelMayer May 3, 2023

atomb May 3, 2023

atomb May 2, 2023

atomb May 2, 2023

MikaelMayer May 3, 2023

atomb May 3, 2023

atomb left a comment

	When annotating an assert with the `{:only}` attribute, all other implicit and explicit assertions
	When annotating an assertion with the `{:only}` attribute, all other implicit and explicit assertions

	are assumed. This is a way to focus on an assertion and its proof, but this annotation has to be removed once finished.
	are transformed into assumptions. This is a way to focus on an assertion and its proof, but this annotation has to be removed once finished.

	"Assertion with {:only} temporarily transforms other assertions in assumptions");
	"Assertion with {:only} temporarily transforms other assertions into assumptions");

	`{:only}` annotations define "verification interval" which are visual:
	Each `{:only}` annotation defines a "verification interval" which is visual:

	Func<IToken, bool> assertionOnlyFilter = null; // generate assume statements instead of assert statements if not targetted by {:only}
	Func<IToken, bool> assertionOnlyFilter = null; // generate assume statements instead of assert statements if not targeted by {:only}

		@@ -26,6 +26,7 @@ public record DafnyAction(string Title, IReadOnlyList<DafnyCodeActionEdit> Edits

		public static class ErrorRegistry {

		// Replace any NoneId by ParseErrors.p_... or ResolutionErrors.r_

Feat: assert {:only} to temporarily work on a single assertion #3933

Feat: assert {:only} to temporarily work on a single assertion #3933

Conversation

MikaelMayer commented May 1, 2023 • edited Loading

Integration

Alternatives considered

atomb left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb left a comment

Choose a reason for hiding this comment

Feat: `assert {:only}` to temporarily work on a single assertion #3933

Feat: `assert {:only}` to temporarily work on a single assertion #3933

MikaelMayer commented May 1, 2023 •

edited

Loading