features for structured proofs

[tjhance]

This is to collect a list of not-very-deep proof feature suggestions that might aid in writing cleaner, more structured proofs.

Feel free to add your own. I feel like calc statements ought to have room for improvement, but I don't have any concrete thoughts right now.

Loop invariants

on_exit and on_loop

Right now the only way to specify a loop invariant is with an invariant clause, but there are a handful of patterns that show up.

One pattern is that we often have invariants that we want to hold on the beginning of each iteration, but not on loop exit, or vice versa. Currently, this would be done like:

while cond {
  invariant(cond ==> X); // X should hold at beginning of each iteration
  invariant(!cond ==> Y); // Y should hold on loop exit
  ...
}

Instead we could have a dedicated way to specify such invariants:

while cond {
  on_loop(X); // X should hold at beginning of each iteration
  on_exit(Y); // Y should hold on loop exit
  ...
}

Besides documenting the intent better, these would generate better VCs in the case that the loop has a break statement inside it. Note that in the former example, !cond ==> Y is useless on loop exit if you can't actually show that !cond holds. Having an on_exit invariant would let us do the right thing.

per-iteration invariants

An extremely common pattern, when looping i from 0 to n is to have stuff like:

for i in 0..n {
  invariant([
    forall(|j| 0 < j < i :: f(j)),
    forall(|j| i <= j < n :: g(j)),
  ]);
  ...
}

It would be great to have a shortcut:

for i in 0..n {
  on_iter_exit(f(i));
  on_iter_entry(g(i));
}

This is basically read as, "on iteration i, we start the loop knowing g(i) and must prove f(i) at the end of the loop".
These are a lot easier to read, but they would basically de-sugar to the invariants given above. These are almost simple enough that they look like they could be implemented with macros, but they would need access to the 0..n range.

Extensionality

A common idiom is to prove 2 collections (sequences, maps, etc.) are equal by showing all elements are equal. It would be nice to have a dedicated (and documented) syntax for it, something like

assert_by_extensionality(s == t,
  length {
    // VC: assert |s| == |t|
  },
  elem |i| {
    // VC: assume 0 <= i < |s|
    ...
    // VC: assert s[i] == t[i]
});

I'm singling out extensionality here because it seems to me its an example of a useful idiom that one "just has to know about", which works because of hidden prelude axioms.

This is simple enough it could be a macro. (But see the next section.)

Named preconditions

The above could be a special case of a more general feature:
It would be nice to call lemmas and prove the preconditions in "assert-by" style.

#[proof]
pub fn my_lemma(x: int)
requires([
  pre1: x > 5
  pre2: forall(|i| | i > x :: f(i))
]);

#[proof]
pub fn foo() {
  // ...
  call_by ( my_lemma(x),
    pre1 {
      // VC: assert x > 5
    }
    pre2 |i| {
      // VC: assume i > x
      // VC: assert f(i) 
    }
  }
}

[parno]

for i in 0..n {
  on_iter_exit(f(i));
  on_iter_entry(g(i));
}

I think either this or the text explaining it is backwards, no? Or else I'm misunderstanding something.

I do like the notion of making extensionality more explicit. It's something that new Dafny users always stumble on, and it involves some pretty complex explanations. Having it explicit would mean it would be documented and something users could look up.

In the name preconditions, as a minor question, in foo(), it looks like you've merged the notion of named precondition with a forall statement. It seems like it might be cleaner to keep those separate.

[tjhance]

I think either this or the text explaining it is backwards, no? Or else I'm misunderstanding something.

Well, the fact that one of us got it backwards is proof that it's confusing and would benefit from having the built-in feature 😄

But I'm pretty sure I got it right. forall(|j| 0 < j < i :: f(j)) basically means you need to show that f(i) is true by the end of the loop (and f(j) will be true forall j at the end of the loop).

In the name preconditions, as a minor question, in foo(), it looks like you've merged the notion of named precondition with a forall statement. It seems like it might be cleaner to keep those separate.

I suggested this because I think it would be nice to skip having to write the forall block.

[tjhance]

oh, it's the text that's wrong. i gotchu

[parno]

I suggested this because I think it would be nice to skip having to write the forall block.

It does seem convenient when your precondition is entirely a quantifier. It won't work (or at least, it would be confusing) if your precondition is, say, (forall i :: P(i)) && (forall j :: Q(j)). From a language design perspective, I think we'd have to decide whether the savings in typing outweighs having programmers learn to recognize/write two forms of named precondition blocks.

[jaybosamiya]

Middle-of-loop invariants

This would allow an "in-body" loop invariant, rather than being restricted to being stuck to the top of the loop, thereby allowing the programmer to pick the "most natural" place in the loop to position the invariant, preventing hand-written forward/backward computation. Indeed, one could even mix and match positions for different parts of the overall loop invariant, placing each invariant at its most natural position within a loop.

As a toy example of how invariants currently work in most tools:

while cond {
  invariant (bar(foo(x + 3)) <= x^2)
  invariant (...)
  let z = foo(x + 3)
  let y = bar(z)
  ...
  x = ...
}

Notice that here we are computing ahead some part of the loop to write out an invariant upon x, while the most natural thing to write the invariant about would be about y and x (in fact, that's exactly what's being written out, just repeated twice manually by the programmer). Instead, imagine we could write the following:

while cond {
  invariant (...)
  let z = foo(x + 3)
  let y = bar(z)
  invariant (z <= x^2)
  ...
  x = ...
}

I've brought this idea up in multiple contexts over the past few years, such as with AES-GCM in Vale, but a more common use-case that comes to mind at the moment would be for "loop and a half" constructs.

These generalized loop invariants work because any loop invariant could (via a weakest precondition computation) be moved to any other location in the loop while having the same meaning. This does mean that it is no more expressive than before; on the other hand, allowing invariants to exist anywhere within the loop allows us to reduce syntactic and cognitive burden of writing invariants, without needing any new syntax (except potentially for disambiguating which loop an in-body invariant applies to in case of nested loops).

Note that it is likely that most loops probably still would write invariants at the head, since that is the most natural point for many/most invariants. This feature would simply allow one to pick that location as a choice, rather than being compelled to use only that.

[tjhance]

Relatedly, it would be nice to be able to something similar for function headers. I frequently felt it would be useful to be able to do something like:

fn foo() {
  requires(...);
  #[spec] let x = ... ;
  requires(... /* can reference x */);
  ensures(... /* can reference x */);

  // spec code in body can reference x
}

It looks like what you are suggesting is even more powerful though (i.e., you are suggesting that we could put exec code before the invariants).