Implement `decreases to` expressions #5367

atomb · 2024-04-25T22:39:13Z

Description

Implement the decreases to and nonincreases to expression forms. This allows you to state that the left-hand sequence of expressions decreases (or at least doesn't increase) to the right-hand sequence.

One caveat: for now, decreases to is allowed only inside parentheses, to avoid parsing ambiguities. This is a strict subset of what we'd ideally like to support. I think it should be possible to allow it to appear elsewhere as part of a separate, backward-compatible PR.

Fixes #5252

How has this been tested?

Added dafny0/DecreasesTo{1,2,3,4,5}.dfy

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

Things remaining: * Better syntax * Fill in error messages * Ensure correct parameters to DecreasesCheck * Figure out why most proof obligation descriptions aren't really useful

This has shortcomings, and in particular is only allowed in `assert` statements at the moment. Making it fully general may require some more parser refactoring.

MikaelMayer · 2024-05-01T15:44:48Z

Having looked only at the test, I like the design so far. Could you also include something like ambiguous parsing tests, such as tuples assert (true, true decreases to false) == true; or assert (true, true decreases to false) == (true, true); depending on your parsing strategy?

fabiomadge

There are a couple of instances where you can remove whitespace, but I'm mostly happy with the rest. Unfortunately, I'm not of much help when it comes to the parser.

fabiomadge · 2024-05-24T19:07:23Z

docs/DafnyRef/Expressions.md

+When proving that a loop or recursive callable terminates, Dafny
+automatically generates a proof obligation that the sequence of
+expressions listed in a `decreases` clause gets smaller (in the
+termination ordering) with each iteration or recursive call. Normally,


Maybe add that it's a lexicographical ordering?

fabiomadge · 2024-05-24T20:07:24Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DecreasesTo2.dfy.expect

+DecreasesTo2.dfy(5,24): Error: invalid UnaryExpression
+DecreasesTo2.dfy(9,21): Error: ident expected
+DecreasesTo2.dfy(9,12): Error: expected 'to'
+DecreasesTo2.dfy(13,10): Error: invalid ParensExpression


I would love to see more helpful error messages, but they're just as good as the ones for other operators, so that's what we probably have to settle for.

Yeah, I agree, on both sides.

fabiomadge · 2024-05-24T20:07:56Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DecreasesTo1.dfy

+
+/*
+method BadTypes () {
+  assert (true decreases to 0);
+}
+*/


Suggested change

/*

method BadTypes () {

assert (true decreases to 0);

}

*/

fabiomadge · 2024-05-24T20:18:55Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DecreasesTo1.dfy

+}
+
+method BadInstance5(i: int, b: bool) {
+  assert (i decreases to b);


Shouldn't the resolver catch this?

I originally thought so, too, but I think there's a good reason for it not to. When Dafny compares two tuples of expressions for termination ordering, it requires only that a prefix of those expression even be comparable. So something like x, 0 decreases to x-1, false should succeed (and does, in the current implementation -- maybe I should add a test showing that). To make this general, the comparable prefix can be empty, in which case the decreases to expression will always be false.

fabiomadge · 2024-05-24T20:19:45Z

Source/DafnyLanguageServer/Language/SyntaxTreeVisitor.cs

@@ -1,4 +1,6 @@
-namespace Microsoft.Dafny.LanguageServer.Language {
+using Microsoft.Boogie;


Suggested change

using Microsoft.Boogie;

Looks like this one is actually used.

fabiomadge · 2024-05-24T20:31:30Z

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -1165,6 +1166,13 @@ public partial class ModuleResolver {

      } else if (expr is NestedMatchExpr nestedMatchExpr) {
        ResolveNestedMatchExpr(nestedMatchExpr, resolutionContext);
+


Suggested change

fabiomadge · 2024-05-24T20:37:28Z

Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs

+      } else if (expr is DecreasesToExpr decreasesToExpr) {
+        var comma = false;
+        foreach (var oldExpr in decreasesToExpr.OldExpressions) {
+          if (comma) {
+            wr.Write(", ");
+          }
+          PrintExpression(oldExpr, false);
+          comma = true;
+        }
+        if (decreasesToExpr.AllowNoChange) {
+          wr.Write(" nonincreases to ");
+        } else {
+          wr.Write(" decreases to ");
+        }
+        comma = false;
+        foreach (var newExpr in decreasesToExpr.NewExpressions) {
+          if (comma) {
+            wr.Write(", ");
+          }
+          PrintExpression(newExpr, false);
+          comma = true;
+        }


Do we test this?

Yep. See the Asserted expression: lines in the added tests.

fabiomadge · 2024-05-24T20:39:50Z

Source/DafnyCore/Dafny.atg

@@ -144,6 +144,7 @@ TOKENS
  by = "by".
  in = "in".
  decreases = "decreases".
+  nonincreases = "nonincreases".


Now that it's there, we might as well keep it, but was there a strong reason to add it?

Sometimes the check that Dafny needs to perform is, roughly speaking, <= instead of <. To be able to express those conditions, it seemed most natural to have a form of the expression that encoded <= instead of <. It would be possible, alternatively, to have (x decreases to y) || x == y, but it seems a little more awkward, and I think would be more difficult to implement, as well (though I'm no longer sure of that).

fabiomadge · 2024-05-24T20:40:24Z

Source/DafnyCore/Dafny.atg

@@ -2919,7 +2920,7 @@ AssertStmt<out Statement/*!*/ s>
      BlockStmt<out proof, out proofStart, out proofEnd>
    | ";"
    | (.
-        SemErr(ErrorId.p_assert_needs_by_or_semicolon, t, "expected either 'by' or a semicolon following the assert expression");
+        SemErr(ErrorId.p_assert_needs_by_or_semicolon, t, $"expected either 'by' or a semicolon following the assert expression");


Suggested change

SemErr(ErrorId.p_assert_needs_by_or_semicolon, t, $"expected either 'by' or a semicolon following the assert expression");

SemErr(ErrorId.p_assert_needs_by_or_semicolon, t, "expected either 'by' or a semicolon following the assert expression");

fabiomadge · 2024-05-24T20:42:57Z

Source/DafnyCore/Dafny.atg

+Expression<out Expression e, bool allowLemma, bool allowLambda, bool allowBitwiseOps = true>
+=
+  NotDecreasesToExpression<out e, allowLemma, allowLambda, allowBitwiseOps>
+  .


I have no idea how to improve on that, but making this the top level seems like a big change.

Yeah, and now that you mention it this change isn't necessary anymore. I made it to help with switching certain things back and forth during debugging, but in the final version I don't think it's necessary. I'll try to remove it.

alex-chew

Looks good to me!

atomb added 6 commits April 24, 2024 15:44

Barebones end-to-end pipeline

53a1a9d

Things remaining: * Better syntax * Fill in error messages * Ensure correct parameters to DecreasesCheck * Figure out why most proof obligation descriptions aren't really useful

Reasonable old and new expressions

14c8e49

Undo spurious changes

e20e735

More reasonable decreases to syntax

23eabb4

This has shortcomings, and in particular is only allowed in `assert` statements at the moment. Making it fully general may require some more parser refactoring.

Update error messages

cd7b8d9

Add initial test

5fe0e36

atomb requested review from MikaelMayer, alex-chew and RustanLeino April 25, 2024 23:34

atomb added 20 commits May 13, 2024 16:17

Merge remote-tracking branch 'upstream/master' into decreasesto

3aa0609

Merge remote-tracking branch 'upstream/master' into decreasesto

30f81df

Adjust parser for decreases to

ee6059e

Remove ICanFormat from DecreasesToExpr

1757a58

Support decreases to only in parentheses

bccfb40

Add release notes

59f74d0

Add documentation for decreases to

341f8e8

Update parse error message capitalization

bd4a58c

Update news file

7b2a9f1

More tests

4ad5ae1

Merge remote-tracking branch 'upstream/master' into decreasesto

cc89ec1

Fix parsing of the unit value

ad26c21

Fix numbering in reference manual

bbd3828

Error message discrepancies

7c4672e

Create error IDs for new error messages

31dbe3d

Merge remote-tracking branch 'upstream/master' into decreasesto

1faa65d

Merge remote-tracking branch 'upstream/master' into decreasesto

54e1b00

Make new GetExtraExplanation methods proper overrides

6f86ce9

Support allowNoChange in DecreasesToExpr

cd93069

Add test for decreases to in non-ghost context

2c1a505

atomb added 5 commits May 22, 2024 15:40

Fix nonincreases to

e87c990

Fix cloning of DecreasesToExpr

e69bbfb

Fix token on some DecreasesToExpr translations

ca3fab5

Fix type checking of decreases to

76a7896

Fix checking of decreases to reference examples

a1a3dcb

atomb marked this pull request as ready for review May 23, 2024 22:43

Merge remote-tracking branch 'upstream/master' into decreasesto

1856361

atomb mentioned this pull request May 24, 2024

Implement GetAssertedExpr for DecreasesBoundedBelow #5489

Merged

Fix tests

aefe775

fabiomadge requested changes May 24, 2024

View reviewed changes

atomb added 5 commits May 24, 2024 15:24

Remove unnecessary grammar complexity

1c6f182

Remove unused lines

e2700c3

Cross-reference decreases and decreases to

a4c910a

Fix tests

089811a

Merge remote-tracking branch 'upstream/master' into decreasesto

5e84606

alex-chew approved these changes May 26, 2024

View reviewed changes

atomb requested a review from fabiomadge May 28, 2024 15:59

fabiomadge approved these changes May 28, 2024

View reviewed changes

atomb enabled auto-merge (squash) May 28, 2024 16:22

atomb added 2 commits May 28, 2024 09:22

Merge branch 'master' into decreasesto

a4181a4

Merge branch 'master' into decreasesto

15d21a4

atomb merged commit 4eb179e into dafny-lang:master May 29, 2024
21 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implement `decreases to` expressions #5367

Implement `decreases to` expressions #5367

atomb commented Apr 25, 2024 •

edited

MikaelMayer commented May 1, 2024

fabiomadge left a comment

fabiomadge May 24, 2024

fabiomadge May 24, 2024

atomb May 24, 2024

fabiomadge May 24, 2024

fabiomadge May 24, 2024

atomb May 24, 2024

fabiomadge May 24, 2024

atomb May 24, 2024

fabiomadge May 24, 2024

fabiomadge May 24, 2024

atomb May 24, 2024

fabiomadge May 24, 2024

atomb May 24, 2024

fabiomadge May 24, 2024

fabiomadge May 24, 2024

atomb May 24, 2024

alex-chew left a comment

		@@ -1,4 +1,6 @@
		namespace Microsoft.Dafny.LanguageServer.Language {
		using Microsoft.Boogie;

		@@ -1165,6 +1166,13 @@ public partial class ModuleResolver {

		} else if (expr is NestedMatchExpr nestedMatchExpr) {
		ResolveNestedMatchExpr(nestedMatchExpr, resolutionContext);

	SemErr(ErrorId.p_assert_needs_by_or_semicolon, t, $"expected either 'by' or a semicolon following the assert expression");
	SemErr(ErrorId.p_assert_needs_by_or_semicolon, t, "expected either 'by' or a semicolon following the assert expression");

Implement decreases to expressions #5367

Implement decreases to expressions #5367

Conversation

atomb commented Apr 25, 2024 • edited

Description

How has this been tested?

MikaelMayer commented May 1, 2024

fabiomadge 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

alex-chew left a comment

Choose a reason for hiding this comment

Implement `decreases to` expressions #5367

Implement `decreases to` expressions #5367

atomb commented Apr 25, 2024 •

edited