feat: Compute matching patterns for automatic induction

[RustanLeino]

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.

[cpitclaudel]

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

[cpitclaudel]

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

[RustanLeino]

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]

Typo: "is added to make stabilize verification"

Shouldn't we include an example or two?

[cpitclaudel]

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?

[cpitclaudel]

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"

[RustanLeino]

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.

[cpitclaudel]

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?

[RustanLeino]

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

[cpitclaudel]

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.)

[RustanLeino]

Thanks for your useful comments, @cpitclaudel . I have addressed many and commented on others. For the good suggestion of making sure there is a way to support customers who want to keep their old possibly-trigger-less inductions, I started writing a specification in the release notes (5835.feat), adding some corresponding test cases to $TEST/triggers/InductionWithoutTriggers.dfy. However, I did not finish this. Here are some questions:

Currently, {:induction} (and equivalently {:induction true}) take the list of all variables (provided their types are reasonable types for induction). Is that what {:induction} should do? I would seem better to let {:induction} pick the list of variables heuristically, just like the absence of an :induction attribute would. That would make sense by itself, and it would also mean that one can get backward compatibility by {:induction} {:nowarn}.

[cpitclaudel]

Using {:induction} for backwards compatibility is tempting but I'm not sure it works: we have many cases of {:induction} already appearing in sources (mostly in quantifiers) in quantifiers.

We could use {:induction "auto"} to use the heuristic, plus {:nowarn}. Alternatively, we could use {:induction_triggers false} to indicate that no triggers should be generated. Or better, since you already generate an {:inductionPattern …}, we could allow users to write an explicit trigger and pass {:inductionPattern} (no terms) to recover the legacy behavior?

I'm not sure how much I like the power that {:inductionPattern …} would give in this case: one we have a way to generate the forall statement in the code, we might ask users to just use that instead?

[cpitclaudel]

Another thing: Should we have a warning specific to induction when we don't generate a trigger for the induction part of a quantifier expression? For example:

predicate f(n: nat)
method ExprInduction() {
  assert forall n: nat {:induction n} :: f(n + 1);
}

In this case we generate this Boogie:

    assert {:id "id1"} {:subsumption 0} (forall n#1: int :: 
      LitInt(0) <= n#1
           && (forall n$ih#0#0: int :: 
            LitInt(0) <= n$ih#0#0
               ==> 
              0 <= n$ih#0#0 && n$ih#0#0 < n#1
               ==> _module.__default.f(n$ih#0#0 + 1))
           && true
         ==> _module.__default.f(n#1 + 1));

Arguably this is fine, because we warn about the top-level quantifier.

[cpitclaudel]

I've made a pass through this:

• I renamed :inductionPattern to :inductionTrigger
• Passing {:inductionTrigger} (no trigger terms) restores the legacy behavior
• I moved the attribute generation to ComputeInductionTriggers.

Here are some examples:

predicate f(n: nat) { if n == 0 then true else f(n-1) }
predicate g(n: nat) { false }

// Default: auto-generated trigger. Proof works.
lemma Default(n: nat) ensures f(n) {}

// Manual list of variables. Proof works.
lemma {:induction n} ListOfVars(n: nat) ensures f(n) {}

// No induction. Proof fails.
lemma {:induction false} NoInduction(n: nat) ensures f(n) {}

// No induction, with manual proof. Proof works.
lemma {:induction false} ManualInduction(n: nat)
  ensures f(n)
{
  forall ih_n: nat | (n decreases to ih_n) {
    ManualInduction(ih_n);
  }
}

// No triggers, so no auto induction ⇒ Proof fails
lemma NoTriggers(n: nat) ensures f(n + 0) {}

// No triggers but forced induction, so warning. Proof works.
lemma {:induction} InductionWarning(n: nat) ensures f(n + 0) {}

// Explicit triggers, so no warning.  Proof works.
lemma {:induction} {:inductionTrigger f(n)} NoWarning2(n: nat) ensures f(n + 0) {}

// Legacy mode: auto induction with no triggers.  Proof works.
lemma {:inductionTrigger} Legacy(n: nat) ensures f(n) {}
lemma {:inductionTrigger} Legacy1(n: nat) ensures f(n + 0) {}
lemma {:induction} {:inductionTrigger} Legacy2(n: nat) ensures f(n + 0) {}

I updated the spec accordingly. I still need to fix a printing issue.

[cpitclaudel]

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)
    |                               ^^^^^

[RustanLeino]

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