Opaque block

[keyboardDrummer]

Description

• Add opaque blocks to the language Example:

  method Foo() returns (x: int)
  ensures x > 4 
  {
  x := 1;
  var y := 1;
  opaque
  ensures x > 3 
  {
  x := x + y;
  x := x + 2;
  }
  assert x == 4; // error, the precise value of x is unknown. We only know about x what the ensures clause told us.
  x := x + y; // precise value of y is still known
  }

Slightly larger program where they're more useful:

method Foo(x: int, switch: bool) returns (r: int) 
  requires x > 0
  ensures r > 5
{
  var y := x + 1; 

  opaque {
    r := y + 1;
    r := r + 1;
  } ensures r > 3; // only r is havocced, not y
  // the above two assignments aren't visible to the different branches in the following if, so there is a less N * M complexity.

  opaque {
    if (switch) {
      r := r + y; // we know facts about y here since it was not havocced
    } else {
      r := r + 2;
    }
  } ensures r > 4;

  r := r + 1;
  // the proof for the ensures clause is unaware of the branching from the if, so it's only asserted once.
}

Part of the goal of opaque statements is to enable statements blocks to grow in size without getting a quadratic increase in the resources required to prove the block.

When there are multiple paths through the method, if an assertion occurs after a merge, then conceptually it will be asserted for each path through that merge. Encasing the split and merge in an opaque block, as is done above, will simplify verification.

How has this been tested?

• Add the CLI test opaqueBlock.dfy

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

[dschoepe]

It might be a bit tedious to explicitly specify what a block ensures and in some cases one may just want to be able to selectively reveal the block in e.g. an assert .. by. Would it be feasible to add the ability to name a block and be able to reveal it elsewhere?

[keyboardDrummer]

It might be a bit tedious to explicitly specify what a block ensures and in some cases one may just want to be able to selectively reveal the block in e.g. an assert .. by. Would it be feasible to add the ability to name a block and be able to reveal it elsewhere?

Any mutation that happens inside the block causes all information to be lost about whatever was mutated, so if after the block you use any variable or reference that was mutated inside it, you won't know anything about it. It seems highly unlikely to me that you would want an opaque block without an ensures clause.

If you want to supply a name to a block of statements that does not mutate variables from outside its scope, then I think defining a lemma with a transparent body (does not exist at the moment, but I could argue for it) is more appropriate. If you only want to use the lemma inside that method and local variables from the method inside the lemma, so you need to specify fewer parameters for the lemma and arguments for the call, then we could allow defining an inline lemma.