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]

This looks like it switches to using a local version of Boogie. Is that intended to be part of the PR?

[keyboardDrummer]

Not intended to be merged, but I used that to let it build while waiting for a new Boogie version. I've since reverted that change. Sorry for the noise.

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

[fabiomadge]

Suggested change

As a Dafny sequence of statements grows in length, it can become harder to verify later statements in the block. With each statement, new information can become available, and with each modification of the heap, it because more expensive to access information from an older heap version. To enable long lists of statements to maintain a verification cost linear in their size, Dafny users can extract part of this block into a separate method or lemma. However, doing so can introduce some boilerplate, whic is where opaque blocks come in. They achieve a similar effect on verification performance as extracting code, but are less work to use.

As a Dafny sequence of statements grows in length, it can become harder to verify later statements in the block. With each statement, new information can become available, and with each modification of the heap, it becomes more expensive to access information from an older heap version. To enable long lists of statements to maintain a verification cost closer to linear in their size, Dafny users can extract part of this block into a separate method or lemma. However, doing so can introduce some boilerplate, which is where opaque blocks come in. They achieve a similar effect on verification performance as extracting code, but are easier to use.

[fabiomadge]

Suggested change

An opaque block is similar to a block statement: it contains a sequence of zero or more statements, enclosed by curly braces. However, an opaque block is preceded by the keyword 'opaque', and may define ensures and modifies clauses before the curly braces. Anything that happens inside the block is invisible to the statements that come after it, so any effect that you wish to capture must be captured by the ensures clauses of the block. Here is an example:

An opaque block is similar to a block statement: it contains a sequence of zero or more statements, enclosed by curly braces. However, an opaque block is preceded by the keyword 'opaque', and may define ensures and modifies clauses before the curly braces. Anything that happens inside the block is invisible to the statements that come after it, so any externally observable effect must be captured by the ensures clauses of the block. Here is an example:

[fabiomadge]

Suggested change

	method OpaqueBlockuser() returns (x: int)
	method OpaqueBlockUser() returns (x: int)

[fabiomadge]

Suggested change

// public abstract IEnumerable<IVariable> AssignedVariables { get; }

[fabiomadge]

Have you considered testing a AssignOrReturnStmt?

[keyboardDrummer]

Good callout. Added some more tests and found bugs.

[fabiomadge]

Sorry for not thinking of it sooner: What about AssignSuchThatStmt?

[keyboardDrummer]

Added it and found another bug 🎉

[fabiomadge]

Sorry for the dripping of ideas: What about multiple LHSs and patterns on the LHS?

[keyboardDrummer]

What sort of patterns do you mean? Added the parallel assignment