[Feature request]: Weakest Precondition calculus (a.k.a. verification debugging or "Move assert up") with Code Actions

[MikaelMayer]

What is the feature you would like to see in a future version of Dafny?

I would like to be able to "move assertions up" a.k.a. weakest precondition calculus.
There is a whole chapter in the doc that could simply be automated by code actions
https://dafny.org/latest/DafnyRef/DafnyRef#sec-verification-debugging

We also need to decide whether or not we keep the implied assertion, and how to offer this affordance to users. Our choices are the following:

1. We never overwrite in place, always create a new assertion without removing the previous one.

• Pro:
  • Might speed up the verifier.
  • Possibility to see that previous assertions are now conditionally verified - gives the sense of "digging" into the proof while having a clear history path.
  • Assertions could always be removed manually anyway.
  • Assertions could be removed with another code action.
• Con:
  • Might clutter the code, especially for obvious assertions rewriting.

2. We always delete an assertion once we inserted the newest one if the new one implies the old one.

• Pro:
  • The error is really "moving up"
  • No clutter with obsolete assertions at the end of the process
• Con:
  • Users lose track on why the assertion moving up should hold.

3. We could offer a code action to remove conditionally verified assertions

• Pro:
  • All the pros of the first choice
  • Fine-grain choice of which assertions to really remove
  • Only four clicks to reproduce the choice of "moving up an assertion" described in the previous bullet point, which required two clicks.
• Con:
  • Four clicks instead of two to remove conditionally verified assertions

4. Instead of offering one code action, we could offer two, one only creating a new assertion, the other doing in-place overwrite or assertion move. We would need to choose the order.

• Pro:
  • Only two clicks for either action (move up, or clone the assertion up with modifications)
• Con:
  • Clutter the code action interface, will be hard to choose from. Order might not be obvious to users.

5. We could make it an option in the IDE to choose from, either in-place overwrite or assertion adding.

• Pro:
  • Only two clicks for either action (move up, or clone the assertion up)
  • Choice made upfront by the user
• Con:
  • Might not suit all the scenarios and create frustrations

With my experience, I would be inclined to vote for 1 and 3 together, until we have something automatic to clean up useless assertions.

Move an assertion to a requires or an invariant

To a requires clause

method Test(i: int) {
  assert i % 2 == 0;
}

could become, after a code action on hovering the failing assertion:

method Test(i: int)
  requires i % 2 == 0; // Just added
{
  assert i % 2 == 0;
}

To an invariant

method Test(i: int) {
  while C(i) {
    i := F(i);
  }
  assert i % 2 == 0;
}

could become, after a code action on hovering the failing assertion:

method Test(i: int) {
  while C(i)
    invariant !C(i) ==> i % 2 == 0
  {
    i := F(i);
  }
  assert i % 2 == 0;
}

Simple example: if-then-else

Propagate assertions up

In the following code, every time an assertion n is failing, a code action could insert the assertion n+1 (and n+1b if relevant)

method Foo(b: bool, x: int, y: int) returns (r: int) 
  // requires if b then x % 2 == 0 else y % 2 == 0 // Assertion 5
{
  // assert if b then x % 2 == 0 else y % 2 == 0 // Assertion 4
  if (b) {
     // assert b ==> x % 2 == 0 :/ Assertion 3b
    r := x;
   // assert b ==> r % 2 == 0 // Assertion 2b
  } else {
   // assert !b ==> y % 2 == 0  // Assertion 3
    r := y;
   // assert !b ==> r % 2 == 0 // Assertion 2
  }
  assert r % 2 == 0 // Assertion 1
}

Advanced example: Quantum precondition

Here is an interesting example I came across of where automated back-propagation of assertions could be useful. Let's say we have this function, and we want to know what's missing to prove the requirement of the last function call:

type Cmd(!new)

function operationCNot(s: (nat, nat)): Cmd
  requires s.0 != s.1

function operateCNotOnAll(s: seq<(nat, nat)>): seq<Cmd>
  requires forall k <- s :: k.0 != k.1
{
  if |s| == 0 then [] else [operationCNot(s[0])] + operateCNOTOnAll(s[1..])
}

function applyCNot(s: seq<nat>): seq<Cmd>
  requires |s| >= 1
  // What other requires do we need?
{
  var init := s[0..|s|-1];
  var last := s[1..];
  var pairs := seq(
    |s|-1,
    (i: int) requires 0 <= i < |s|-1 => (init[i], last[i]));
  operateCNOTOnAll(pairs) // Precondition is failing
}

First step, we could explicit the failing precondition using a code action that would replace the variable "s" by the expression

function applyCNot(s: seq<nat>): seq<Cmd>
  requires |s| >= 1
  // What other requires do we need?
{
  var init := s[0..|s|-1];
  var last := s[1..];
  var pairs := seq(
    |s|-1,
    (i: int) requires 0 <= i < |s|-1 => (init[i], last[i]));
  assert forall k <- pair :: k.0 != k.1; // Just inserted
  operateCNOTOnAll(pairs)
}

Since we have the definition of pairs, we can replace pairs with that definition using a code action that would insert a new assertion

function applyCNot(s: seq<nat>): seq<Cmd>
  requires |s| >= 1
  // What other requires do we need?
{
  var init := s[0..|s|-1];
  var last := s[1..];
  assert forall k <- seq(|s|-1,(i: int) requires 0 <= i < |s|-1 => (init[i], last[i])) :: k.0 != k.1; // Just inserted
  var pairs := seq(
    |s|-1,
    (i: int) requires 0 <= i < |s|-1 => (init[i], last[i]));
  assert forall k <- pair :: k.0 != k.1;
  operateCNOTOnAll(pairs)
}

Another code action could then simplify this expression idiomatically by inserting a new assertion again, as described in #3114 :

function applyCNot(s: seq<nat>): seq<Cmd>
  requires |s| >= 1
  // What other requires do we need?
{
  var init := s[0..|s|-1];
  var last := s[1..];
  assert forall i, k | 0 <= i < |s|-1 && k == (init[i], last[i]) :: k.0 != k.1; // Just inserted
  assert forall k <- seq(|s|-1,(i: int) requires 0 <= i < |s|-1 => (init[i], last[i])) :: k.0 != k.1;
  var pairs := seq(
    |s|-1,
    (i: int) requires 0 <= i < |s|-1 => (init[i], last[i]));
  assert forall k <- pair :: k.0 != k.1;
  operateCNOTOnAll(pairs)
}

Another code action now can simplify this forall further by inlining the definition of k:

function applyCNot(s: seq<nat>): seq<Cmd>
  requires |s| >= 1
  // What other requires do we need?
{
  var init := s[0..|s|-1];
  var last := s[1..];
  assert forall i | 0 <= i < |s|-1 :: (init[i], last[i]).0 != (init[i], last[i]).1; // Just inserted
  assert forall i, k | 0 <= i < |s|-1 && k == (init[i], last[i]) :: k.0 != k.1;
  assert forall k <- seq(|s|-1,(i: int) requires 0 <= i < |s|-1 => (init[i], last[i])) :: k.0 != k.1;
  var pairs := seq(
    |s|-1,
    (i: int) requires 0 <= i < |s|-1 => (init[i], last[i]));
  assert forall k <- pair :: k.0 != k.1;
  operateCNOTOnAll(pairs)
}

One more code action can simplify the code an add an assertion above.

function applyCNot(s: seq<nat>): seq<Cmd>
  requires |s| >= 1
  // What other requires do we need?
{
  var init := s[0..|s|-1];
  var last := s[1..];
  assert forall i | 0 <= i < |s|-1 :: init[i] != last[i]; // Just inserted
  assert forall i | 0 <= i < |s|-1 :: (init[i], last[i]).0 != (init[i], last[i]).1;
  assert forall i, k | 0 <= i < |s|-1 && k == (init[i], last[i]) :: k.0 != k.1;
  assert forall k <- seq(|s|-1,(i: int) requires 0 <= i < |s|-1 => (init[i], last[i])) :: k.0 != k.1;
  var pairs := seq(
    |s|-1,
    (i: int) requires 0 <= i < |s|-1 => (init[i], last[i]));
  assert forall k <- pair :: k.0 != k.1;
  operateCNOTOnAll(pairs)
}

With two code actions, one could inline the definition of init and last, like this:

function applyCNot(s: seq<nat>): seq<Cmd>
  requires |s| >= 1
  // What other requires do we need?
{
  assert forall i | 0 <= i < |s|-1 :: s[0..|s|-1][i] != s[1..][i]); // Just inserted
  var init := s[0..|s|-1];
  var last := s[1..];
  assert forall i | 0 <= i < |s|-1 :: init[i] != last[i]);
  assert forall i | 0 <= i < |s|-1 :: (init[i], last[i]).0 != (init[i], last[i]).1;
  assert forall i, k | 0 <= i < |s|-1 && k == (init[i], last[i]) :: k.0 != k.1;
  assert forall k <- seq(|s|-1,(i: int) requires 0 <= i < |s|-1 => (init[i], last[i])) :: k.0 != k.1;
  var pairs := seq(
    |s|-1,
    (i: int) requires 0 <= i < |s|-1 => (init[i], last[i]));
  assert forall k <- pair :: k.0 != k.1;
  operateCNOTOnAll(pairs)
}

Another code action could help simplification

function applyCNot(s: seq<nat>): seq<Cmd>
  requires |s| >= 1
  // What other requires do we need?
{
  assert forall i | 0 <= i < |s|-1 :: s[i] != s[1+i]); // Just inserted
  assert forall i | 0 <= i < |s|-1 :: s[0..|s|-1][i] != s[1..][i]);
  var init := s[0..|s|-1];
  var last := s[1..];
  assert forall i | 0 <= i < |s|-1 :: init[i] != last[i]);
  assert forall i | 0 <= i < |s|-1 :: (init[i], last[i]).0 != (init[i], last[i]).1;
  assert forall i, k | 0 <= i < |s|-1 && k == (init[i], last[i]) :: k.0 != k.1;
  assert forall k <- seq(|s|-1,(i: int) requires 0 <= i < |s|-1 => (init[i], last[i])) :: k.0 != k.1;
  var pairs := seq(
    |s|-1,
    (i: int) requires 0 <= i < |s|-1 => (init[i], last[i]));
  assert forall k <- pair :: k.0 != k.1;
  operateCNOTOnAll(pairs)
}

Last but not least, another code action could simply move the first assert to a requires, making the function to verify:

function applyCNot(s: seq<nat>): seq<Cmd>
  requires |s| >= 1
  requires forall i | 0 <= i < |s|-1 :: s[i] != s[1+i]) // Just inserted
{
  assert forall i | 0 <= i < |s|-1 :: s[i] != s[1+i]);
  assert forall i | 0 <= i < |s|-1 :: s[0..|s|-1][i] != s[1..][i]);
  var init := s[0..|s|-1];
  var last := s[1..];
  assert forall i | 0 <= i < |s|-1 :: init[i] != last[i]);
  assert forall i | 0 <= i < |s|-1 :: (init[i], last[i]).0 != (init[i], last[i]).1;
  assert forall i, k | 0 <= i < |s|-1 && k == (init[i], last[i]) :: k.0 != k.1;
  assert forall k <- seq(|s|-1,(i: int) requires 0 <= i < |s|-1 => (init[i], last[i])) :: k.0 != k.1;
  var pairs := seq(
    |s|-1,
    (i: int) requires 0 <= i < |s|-1 => (init[i], last[i]));
  assert forall k <- pair :: k.0 != k.1;
  operateCNOTOnAll(pairs)
}

Another idea then is to automatically detect redundant assertions to clean up this code, but this is another issue.

Heap-sensitive weakest precondition calculus

Answer to this problem: https://stackoverflow.com/questions/74677214/dafny-verification-of-the-most-simple-array-summation-does-not-work-can-somebo/74691162#74691162

Consider the following code:

method addThreeArrays(a: array<int>, b: array<int>, c: array<int>, h: int, i: int, j: int)
  modifies c
  requires 0 <= h < a.Length
  requires 0 <= i < b.Length
  requires 0 <= j < c.Length  
  ensures c[j] == a[h] + b[i]  // Failing
  {
    c[j] := a[h] + b[i];
  }

Making the assertion explicit would result in

  {
    c[j] := a[h] + b[i];
    assert c[j] == a[h] + b[i];
  }

Now, we cannot just "move the assert up", because we would otherwise have to reason about the state of the heap after the assignment, and old@ cannot refer to a label defined afterwards yet (right, @RustanLeino ?)
So, the next step would be to introduce the label and do the weakest precondition calculus below the assignment

  {
    label before: // Added
    c[j] := a[h] + b[i];
    assert old@before(a[h] + b[i]) == a[h] + b[i]; // Added, now failing
    assert c[j] == a[h] + b[i];
  }

The nice thing about that is that it would help the user discover the "old" syntax in a natural way.
Because the weakest precondition now sees two more potentially conflicting references, it could suggest the following code action to remove the reference to the heap after the assignment:

  {
    label before: // Added
    c[j] := a[h] + b[i];
    assert old@before(a[h] + b[i]) == (if a == c && j == h then old@before(a[h] + b[i]) else a[h]) + (if b == c && j == i then old@before(a[h] + b[i]) else b[i]); 
    assert c[j] == a[h] + b[i];
  }

Now, because this expression does not refer at all to the heap after the assignment c[j}, the weakest precondition calculus would be able to move this assertion before and remove the old@ expressions.

  {
    assert a[h] + b[i] == (if a == c && j == h then a[h] + b[i] else a[h]) + (if b == c && j == i then a[h] + b[i] else b[i]); // Just added, now failing.
    label before:
    c[j] := a[h] + b[i];
    assert old@before(a[h] + b[i]) == (if a == c && j == h then old@before(a[h] + b[i]) else a[h]) + (if b == c && j == i then old@before(a[h] + b[i]) else b[i]); 
    assert old@before(a[h] + b[i]) == a[h] + b[i];
    assert c[j] == a[h] + b[i];
  }

and eventually move it to a requires of the method. The user can then refine this weakest precondition so that they only keep a != c && b != c if they wanted to. Or not.

[keyboardDrummer]

In the advanced example you describe refactorings that simplify expressions, but that seems like a feature that's quite different from using WP rules to move assertions up. Could you put that in a separate issue? I think it would be good to have a crisp scope for this one.

Also, one cool feature of moving assertion using WP rules is that it can cause a program to verify when it did not do so before, if it moves assertions are into loop invariants or requires clauses, since both of those are proof boundaries. You mention this at the end of your advanced example, but I would highlight this early and show a simple example where this works.

Also, I would mention that we can choose to either copy or move assertions, and choose to take steps of 1 statement or step until the requires, and say something about which one we would like to offer and why.

[MikaelMayer]

In the advanced example you describe refactorings that simplify expressions, but that seems like a feature that's quite different from using WP rules to move assertions up. Could you put that in a separate issue? I think it would be good to have a crisp scope for this one.

Issue created. Good idea, although the mechanisms are the same, we could make it two different projects given their nature.
#3114

Also, one cool feature of moving assertion using WP rules is that it can cause a program to verify when it did not do so before, if it moves assertions are into loop invariants or requires clauses, since both of those are proof boundaries. You mention this at the end of your advanced example, but I would highlight this early and show a simple example where this works.

Done, I edited the description.

Also, I would mention that we can choose to either copy or move assertions, and choose to take steps of 1 statement or step until the requires, and say something about which one we would like to offer and why.

I added all the possible envisioned alternatives and my currently favorite.