feat: Compute matching patterns for automatic induction #5835

RustanLeino · 2024-10-16T15:19:24Z

This PR aims to help stabilize verification by filling in matching patterns for the quantifiers introduced by automatic induction to represent the induction hypothesis. It also suppresses the generation of the induction hypothesis if no such matching patterns are found.

Full description

This PR computes matching patterns for the quantification that's about to be used with automatic induction. If there are no matching patterns, the induction hypothesis is not added. Tooltips or warnings show the patterns or announce the lack thereof.

The PR no longer uses arrow-typed variables as induction variables. (If a user really wants them, an {:induction ...} attribute can be given manually.)

Treat this more like other parameters when computing induction variables.

With this PR, ternary expressions (that is, _ ==#[_] _ and _ !=#[_] _) are considered as candidate trigger expressions. In addition, a codatatype == (which is defined by Dafny as a greatest predicate) is considered as a focal predicate for extreme predicates.

The PR also fixes a crash in trigger selection when the candidate expression has a lambda expression.

Finally, the "selected trigger" tooltip is extended to also show the t := e binding for any bound variable added as part of a quantifier rewrite.

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

# Conflicts: # Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs

# Conflicts: # Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs # Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs

cpitclaudel

Here is a first pass with mostly cosmetic details. I'm currently making my way through the core computation.

Source/DafnyCore/AST/ExtremeCloner.cs

cpitclaudel · 2024-10-19T01:29:05Z

Source/DafnyStandardLibraries/src/Std/Arithmetic/LittleEndianNat.dfy

+      (ToNatRight([]) * BASE() + First(xs1)) * BASE() + First(xs);
+      { reveal ToNatRight(); }
+      (0 * BASE() + First(xs1)) * BASE() + First(xs);
+    }


Why isn't the right proof here to rewrite xs as [xs[0], xs[1]]?

I don't see how that rewrite helps any. It's nice to have a name for the expression [xs[1]]. But I removed the assertion assert DropFirst(xs1) == [];, which wasn't needed.

cpitclaudel · 2024-10-19T01:30:53Z

docs/dev/news/5835.feat

@@ -0,0 +1,5 @@
+Fill in matching patterns for the quantifiers introduced by automatic induction to represent the induction hypothesis. Suppress the generation of the induction hypothesis if no such matching patterns are found. Enhance tooltips accordingly. This feature is added to make stabilize verification, but by sometimes not generating induction hypotheses, some automatic proofs may no longer go through.


Typo: "is added to make stabilize verification"

Shouldn't we include an example or two?

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Abstemious.dfy

cpitclaudel · 2024-10-19T02:11:41Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/let-expressions.dfy.expect

-let-expressions.dfy(8,8): Info: Selected triggers: {s[_t#0], s[i]}
-let-expressions.dfy(9,8): Info: Selected triggers: {s[_t#0], s[i]}
+let-expressions.dfy(8,8): Info: Selected triggers: {s[_t#0], s[i]} where _t#0 := i + 1
+let-expressions.dfy(9,8): Info: Selected triggers: {s[_t#0], s[i]} where _t#0 := i + 1


These temporary variable names appeared when we started supporting automatic rewriting of matching loops, but the trigger that we add is (almost?) always the same for this new variable as it was for the original variable that it looped with (after all, it was precisely because the new term caused a loop with the trigger of the first one that we created a new variable).

Given this, shouldn't we just hide that redundant trigger and print only {s[i]}, rather that showing the temporary variable with the additional where clause?

We used to print something like

loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (may loop with "f(i + 1)") /!\ Suppressing loops would leave this expression without triggers.

Once these loops were eliminated by rewriting we returned to normal messages, but I'm not sure that this was a purposeful choice (6904c90). Perhaps we should print something like "potential matching loop with … eliminated by rewriting"

It seems I've been confused about the role of these names, and indeed about their worth as well. For now, I just back out my changes that had added printing of where t#0 := ... tooltips. Separately from this PR, we should rethink whether or not we really want to do these rewrites.

Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs

Source/DafnyCore/Rewriters/InductionHeuristic.cs

Source/DafnyCore/Rewriters/InductionRewriter.cs

cpitclaudel · 2024-10-19T03:24:13Z

Source/DafnyCore/Rewriters/InductionRewriter.cs

        inductionVariables.Add(new IdentifierExpr(n.Tok, n));
      }
    }

    if (inductionVariables.Count != 0) {
+      List<List<Expression>> triggers = null;
+      if (lemma != null) {
+        triggers = ComputeInductionTriggers(inductionVariables, body, lemma.EnclosingClass.EnclosingModuleDefinition);


I find the logic here a bit hard to follow: we have ComputeInductionTriggers and ComputeAndReportInductionTriggers and ReportInductionTriggers, and two sets of calls for each of these methods. Is the duplication necessary? Can we add a comment why?

I added a comment. (The reason is to get the tooltips to come out in a nice order.)

Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs

cpitclaudel · 2024-10-19T03:30:21Z

Source/DafnyCore/Rewriters/InductionRewriter.cs

+
+          Reporter.Message(MessageSource.Rewriter, warningLevel, null, tok,
+            $"Could not find a trigger for the induction hypothesis. Without a trigger, this may cause brittle verification. " +
+            $"Change or remove the {{:induction}} attribute to generate a different induction hypothesis, or add {{:nowarn}} to silence this warning. " +


Is there a way to make it produce a quantifier without triggers (and thus recover the previous behavior?)

cpitclaudel

OK, I finished reading through. It looks good to me! Beyond stylistic concerns that I left in individual comments, my main worry is the impact that this will have on customers: how many proofs will be broken, and how good a transition path are we giving them? Is there an easy way to recover the previous behavior (e.g. what if we made :induction true do that, though with a warning?

(When we started generating triggers automatically we did so under a flag at first.)

- Mention --manual-lemma-induction - Mention {:inductionTrigger}

cpitclaudel · 2024-10-24T09:57:39Z

I think this is ready for review. We can do the forall statement generation in a separate PR. I tried to split things into relevant commits, so reviewing them one by one might be best.

Also: I'm not sure how to regenerate the .doo files: running the recommended make command creates errors:

$ make -C Source/DafnyStandardLibraries update-binary
make: Entering directory 'Source/DafnyStandardLibraries'
dotnet run --project ../Dafny --no-build --roll-forward LatestMajor -- build -t:lib --hidden-no-verify=false  src/Std/dfyconfig.toml --output:build/DafnyStandardLibraries.doo
[…]
src/Std/Arithmetic/LittleEndianNat.dfy[ParametricConversion](113,30): Error: member 'First' does not exist in top-level module declaration '_default'
    |
113 |     ensures ToNatRight(xs) == First(xs)
    |                               ^^^^^

# Conflicts: # Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs # Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo # Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect

* By using _inductionTrigger for generated triggers, the Dafny machinery for cloning things into refinement modules works correctly * Tooltips only show things not already in the program text

RustanLeino · 2024-10-31T20:14:35Z

@cpitclaudel Thanks for your help. I think everything has been addressed now.

# Conflicts: # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo

…nduction

cpitclaudel

The follow-up changes look good, thanks. I merged with main.

…nduction

RustanLeino added 20 commits October 11, 2024 23:31

chore: Improve trigger/induction code

8c4c4a6

# Conflicts: # Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs

Compute triggers for automatic induction

e62d2b6

# Conflicts: # Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs # Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs

Improve induction heuristics

ad1c724

chore: Change “ghost method” to “lemma”

29d715a

chore: Improve C#

4cfbe21

Also consider codatatype equality as a greatest focal predicate

b17c662

Show tooltips for any quantifier rewrite substitutions

cee8d58

feat!: Auto-induction for twostate lemmas but not ghost methods

dda37cb

fix: Don’t consider arrow-typed variables for auto induction

fa79ba3

feat: allow ternary expressions in triggers

0028a3a

Compute and use triggers for induction hypotheses

394c635

Tooltip named expressions from trigger selection

659d4ba

chore: Remove deprecated semi-colons

6b5b207

Add tests for ternary expressions in triggers

3fc56d3

Adjust resource count in test

73d2d61

Merge branch 'master' into triggers-for-auto-induction

73406c6

Add release notes

f4815f4

Help proof

e4e4ce8

Update test, which no longer exhausts resources

3a0f1c0

Improve proofs

703c661

cpitclaudel reviewed Oct 19, 2024

View reviewed changes

Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs Outdated Show resolved Hide resolved

cpitclaudel reviewed Oct 19, 2024

View reviewed changes

cpitclaudel requested changes Oct 19, 2024

View reviewed changes

RustanLeino added 5 commits October 20, 2024 06:49

Fix typo in method name

54e9ddb

Remove unnecessary assertion

b46f0dc

Remove unnecessary $’s

022685c

Improve C# and comments

4cb3f5a

Revert tooltip printing of trigger named expressions

a213285

Update documentation

a3702d2

- Mention --manual-lemma-induction - Mention {:inductionTrigger}

cpitclaudel force-pushed the triggers-for-auto-induction branch from 6b37d78 to cf8c9ec Compare October 24, 2024 09:15

Add one more test for induction triggers

ffe54af

cpitclaudel force-pushed the triggers-for-auto-induction branch from cf8c9ec to ffe54af Compare October 24, 2024 09:18

Document {:inductionTrigger}

8c7b06c

RustanLeino added 8 commits October 30, 2024 16:06

Always report “inductionTrigger”, not just in DEBUG build

769d6cd

Fix format of expected test output

2c7fcc9

Use underscore name for generated attributes

af0223b

* By using _inductionTrigger for generated triggers, the Dafny machinery for cloning things into refinement modules works correctly * Tooltips only show things not already in the program text

Update tests

6cdaa08

Update tests and expected output

a1149c9

Fix previous code edit

c447ffa

Merge branch 'master' into triggers-for-auto-induction

3d8d0e7

RustanLeino enabled auto-merge (squash) October 31, 2024 20:16

RustanLeino and others added 6 commits October 31, 2024 14:29

Update standard libraries

63683d1

Merge branch 'master' into triggers-for-auto-induction

808a2b3

Update standard library

3652ff3

Update standard library

b070751

Merge remote-tracking branch 'origin/master' into triggers-for-auto-i…

ee3cbd6

…nduction

cpitclaudel previously approved these changes Nov 7, 2024

View reviewed changes

cpitclaudel added 2 commits November 8, 2024 14:39

Update resource usage in CoinductiveProofs.dfy.expect

e15ebf5

Merge remote-tracking branch 'origin/master' into triggers-for-auto-i…

5b085d8

…nduction

cpitclaudel dismissed their stale review via 5b085d8 November 8, 2024 13:40

Merge branch 'master' into triggers-for-auto-induction

e743c67

cpitclaudel approved these changes Nov 8, 2024

View reviewed changes

RustanLeino merged commit e77b51e into dafny-lang:master Nov 8, 2024
22 checks passed

RustanLeino deleted the triggers-for-auto-induction branch November 12, 2024 01:08

		@@ -0,0 +1,5 @@
		Fill in matching patterns for the quantifiers introduced by automatic induction to represent the induction hypothesis. Suppress the generation of the induction hypothesis if no such matching patterns are found. Enhance tooltips accordingly. This feature is added to make stabilize verification, but by sometimes not generating induction hypotheses, some automatic proofs may no longer go through.

feat: Compute matching patterns for automatic induction #5835

feat: Compute matching patterns for automatic induction #5835

Uh oh!

Conversation

RustanLeino commented Oct 16, 2024

Full description

Uh oh!

cpitclaudel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

cpitclaudel left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

cpitclaudel commented Oct 24, 2024

Uh oh!

RustanLeino commented Oct 31, 2024

Uh oh!

cpitclaudel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

cpitclaudel left a comment •

edited

Loading