Frames & Extract

frame and extract make proof checking more local. They move a block or loop into a separate proof obligation with an explicit contract, which often makes the proof smaller and more robust.

Purpose

• frame introduces a scoped proof context.
• extract checks the enclosed block or loop as a separate extracted method.
• This is useful when the surrounding proof is too large or too brittle because too much local information is visible at once.

Framing & Extracting Code

The following example, frames a piece of code.

void test() {
  int x = 3;
  int old_x = x;
  frame
    requires x == old_x;
    ensures x == old_x + 1;
  {
    x = x + 1;
  }
  assert x == 4;
}

This is use full to explicitly set the behaviour of some piece of code, in this cases that it increases the x variable by one.

The code can be also extracted, which puts it in its own method, as shown in the following example.

void test() {
  int x = 3;
  int old_x = x;
  extract frame
    requires x == old_x;
    ensures x == old_x + 1;
  {
    x = x + 1;
  }
  assert x == 4;
}

This code is converted to the following.

  given int x;
  given int old_x;
  yields int modified_x;
  requires x == old_x;
  ensures modified_x == old_x + 1;
void extracted(){
  x = x + 1;
  modified_x = x;
}

void test() {
  int x = 3;
  int old_x = x;
  extracted() given {x=x, old_x=old_x} yields {x=modified_x};
  assert x == 4;
}

[!Caution] Be aware that framing removes known information about local variables. Thus the following fails:

void test() {
  int x = 3;
  frame
  {
    x = x + 1;
  }
  assert x == 4;
}

Whilst normally without the frame, this local information is kept.

void test() {
  int x = 3;
  x = x + 1;
  assert x == 4;
}

Additionally, without setting explicit preconditions, the framed code does not know otherwise known information.

void test() {
  int x = 3;
  extract frame
  {
    x = x + 1;
    assert x > 0;
  }
}

Similarly, explicit permission must be set for memory locations which are used.

Extracting loops

Loops can also be extracted. In that case, the extracted code is checked as a method that contains exactly the loop.

• For a for loop, the initialization statement is moved before the extracted call.
• The update statement of the for loop is appended as the final step of the generated while loop.
• The loop invariants are added as context annotations.
• The initialization statement is added as a requires fact.
• The loop condition is added as the negation of the precondition, so the extracted contract effectively records ensures !(i < n).

Example:

int test() {
  int x = 2;
  extract
    loop_invariant 0 <= i && i <= 10;
    loop_invariant x == 2 + i;
  for (int i = 0; i < 10; i++) {
    x++;
  }
  assert x == 12;
  return x;
}

Termination

If the enclosing method has a decreases obligation, the extracted unit may also need an explicit decreases clause.

  decreases;
int test() {
  int x = 2;
  extract decreases
    loop_invariant 0 <= i && i <= 10;
    loop_invariant x == 2 + i;
    decreases 10 - i;
  for (int i = 0; i < 10; i++) {
    x++;
  }
  assert x == 12;
  return x;
}

If the extracted section contains a recursive call, a plain decrease clause may not be enough. In that case, use a tuple decrease so the recursive call is still decreasing at the extracted level.

  decreases p, 1;
  requires p >= 0;
int test(int p) {
  if (p == 0) return 0;

  int result;
  extract decreases p, 0 frame
  requires p > 0;
  {
    result = test(p - 1);
  }
  return result;
}