Assertions/reveal localized in expressions

[MikaelMayer]

Summary

This feature requests consists in adding a way in Dafny to ensure that some assertions are visible only within a certain scope.

Background and Motivation

Proof durability is one of the major concerns of some of our high-level Dafny customers. Basically, it all boils down to ensure that the verifier is not provided with too many facts that could blow up verification time.
One very practical way to reduce the number of facts known to the verifier is to use opaque labelled assertions associated with reveal statements. Unfortunately, this is system is not very robust. Some efforts has been made but problems still remain (#2260, #3719, #3506, #2941, #3805 ...). One of the most emblematic ones is #1382, that indicates that revealing functions inside functions extends past the function definition itself.

We need better mechanisms to make things opaque and not blow up

Context

We cannot just state that assertions don't leak outside of their scope.
In Dafny, assertions and reveals inside blocks always "leak" to outer scopes, and for good reasons. It makes it possible to develop appropriate proofs in different assumption contexts.

So, whereas the following works

predicate P()
method Test(b: bool)
  requires p: b <==> P()
{
  if b {
    assert P() by { reveal p; }
  }
  assert b ==> P(); // Can be proved even if p is not visible
  assert P() ==> b; // Cannot be proved
}

Which poses the question: Don't we want the same for functions? Since in functions, there is no "after" an if statement, the best equivalent we can think of is an assignment:

predicate P()
function Test(b: bool): int
{
  var x := if b then
      assert P() by { assume b <==> P(); }
      15 else 16;
  assert b ==> P(); // Can be proved even if the assumption is not visible
  assert P() ==> b; // Cannot be proved
  x
}

And indeed this one works the same. Hence if we want assertions/reveal that are local in their block, we need to either do one of these two things:

• Create a new language feature.
• Redesign the semantics of an existing language feature.

In the following alternatives, we are going to only consider at first ways to make assertions in expressions local in their block.

Alternative A: Redesign the semantics of an existing language feature

1. We keep the same semantics for assertion assumptions and reveal in statements.
2. In expressions, assert, reveal and assume are only visible to the expressions that they are next to. However, the assumptions of the expressions themselves are still visible from the outside. In a sense, an expression like assert A; x is the same as "assume PrecondX; x", + an unrelated proof of "assert A; assume A; assert PrecondX" where PreCondX is the precondition to be able to build X.

So for example,

opaque function F(x: int): nat {
  1
}

function AllArgumentsNotZero(x: int, y: int): int
  requires x != 0
  requires y != 0

function testCallF(): int {
    var r := (reveal F(); AllArgumentsNotZero(F(0), F(1)));
    assert F(0) != 0; // Always verified
    assert F(1) != 0; // Always verified
    assert F(0) == 1; // Used to verify, should not verify anymore
    assert F(1) == 1; // Used to verify, should not verify anymore
    r
}

This should be the same for assume and assert StmtExpr.

Pro

• No new language construct.
• Clear semantics: Statement leak explicit assumptions, expressions don't.

Cons

• Breaking change. Users used to proving assertions inside expressions so that these assertions can be used somewhere else will be penalized as they have to lift all their assertions, or duplicate their pattern matching. This is cumbersome.

Alternative B: New prefix language construct

We could repurpose a keyword so that Alternative A is implemented but only for assert/reveal/assume prefixed with that keyword, e.g.

• opaque assert, opaque reveal, opaque assume
• locally assert, locally reveal, locally assume
• local assert, local reveal, local assume
• assert here, reveal here, assume here

Pro

• No breaking of existing proofs
• Ability to speed up some proofs by adding this special keyword in front of certain assertions.
• Clear semantics: Assertions are always visible in the flow after them, except if they are labelled with the keyword, in which case only
• Works on statements and expressions

Cons

• If we repurpose "opaque", opaque reveal sounds really weird, no one will guess what it means.
• If we use another keyword, adding a keyword in the language is always a difficult choice, as it can break people's code.

Alternative C: Season assert/assume/reveal with attribute

We don't reinvent a keyword for now, but we introduce an attribute..

• assert {:local}, reveal {:local}, assume {:local}
• assert {:locally}, reveal {:locally}, assume {:locally}
• assert {:here}, reveal {:here}, assume {:here}
• assert {:scoped}, reveal {:scoped}, assume {:scoped}
• assert {:opaque}, reveal {:opaque}, assume {:opaque}
• assert {:only-in-scope}, reveal {:only-in-scope}, assume {:only-in-scope}

Pro

• No breaking of existing proofs
• We already did this for "opaque" before promoting it to a keyword
• Makes it possible to optimize proofs, similar to {:split_here}
• Since it's often an optimization step for verification to make it faster (we are only removing hypotheses), it makes sense to be an attribute.

Cons

• It's an attribute, so feels awkward.

Alternative D: Expand the assert statement

We could invent the following expression and statement

assert X within { expression or statements }
assert X by { Proof } within { expression or statements }
assume X within { expression or statements }
reveal a, b within { expression or statements } 

Pro

• No breaking of existing proofs
• The scope the assertion applies to is clearly delimited

Cons

• Weird semantics: What is in Proof is not visible to expressions or statement, but expression or statement is visible afterwards?
• Need of curly braces is really annoying for expressions, I would prefer to have something that is the prefix of an expression so that I don't nest the expression with more parentheses.
• If we used the keyword for: Ambiguity in statements if an assert ... by was followed by a for loop.
• If we used the keyword in: Impossible due to ambiguity with the existing keyword "in"

Alternative E. Invent a new "by" construct.

An expression E could be affixed with by { Proof }
in which case all assert/assume/reveal in Proof are accessible to prove E, but not outside of the entire expression. It could be prefixed or suffixed:

E by { proof }
by { proof } E

    // for example:
    var r := AllArgumentsNotZero(F(0), F(1)) by {reveal P(); };
    var r := by { reveal P();} AllArgumentsNotZero(F(0), F(1));

Pro

• No breaking of existing proofs
• Similar to "assert by" except that it is computed, so clear semantics.
• Possibility to add parentheses to disambiguate?

Cons

• If Prefix: Ambiguity to resolve or at least process visually: in assert X by { Proof } E the visual sub expression by { Proof } E could be interpreted visually as an expression on which Proof is visible to E. This is clearly not desirable.
• If Suffix: Ambiguity to resolve assert X by { Proof } E, does it mean assert (X by { Proof }) E? If not, That means we would need to forbid the parsing of "by" suffix when parsing the expression X, which is cumbersome both to implement and to understand.

Why bothering?

Not having this feature prevents some Dafny customers to scale up their designs and their proofs.
Workaround include more refactoring, which is not always practical or desirable, or increasing the number of cores.

Other test cases to consider:

opaque predicate P(x: int) {
  true
}

function F(u: int): (r: int)
  ensures P(r)
{
  reveal P(); // Without annotation, assert P(2); below verifies. However, with the annotation, the assert P(2) should no longer verify.
  u
} by method {
  assert P(2); // expected error, but Dafny does not report any error
  r := u;
}

Other alternatives

Other solutions we considered included:

• We could invent a way to make expressions "opaque", meaning only the type and possibly some properties leak out of an expression. However, it would not provide a way for users to reveal and assert locally while letting the verifier know about the shape of the expression.

[MikaelMayer]

@atomb @alex-chew @fabiomadge and myself discussed this today. Here is the fruit of our discussion.

Decision

In a first phase, we will solve this issue by implementing the following decisions:

• We will use an attribute (alternative C) for the flexibility it provides in this experimentation phase.
• We will use {:scoped} so that it can have suitable antonym and is memorable.

Notes about decision

• Making more assertions local has the potential to speed up verification, we should be able to measure some performance improvement
• by {...} construct is nice because it enables to state something before proving it. However, we don't have a good solution for the ambiguity resolution with the existing assert ... by {}.
• If anything, we want the language feature to not break existing code, but we can consider migration.
• Between all the alternatives, the attribute route is the least disruptive for now, also it goes along with {:split_here} {:focus} and {:subsumption 0} (to not assume an assertion after proving it)
• To choose between the keywords for attributes, we decided that it should have a clear antonym for if we make local assertions the default (more about this below). So {:here} or {:local} that don't have suitable antonyms are not preferred, but {:scoped} is suitable, we could have {:unscoped} for example.

Future considerations

After having implementing the decisions, we will be able to consider the following extensions

• Add attribute to function calls so that we could use {:scoped} on lemmas calls as well.
• Define a module-level and declaration-level {:scoped-assumptions} attribute to make assertions scoped by default.
• Define an equivalent CLI option --scoped-assumptions true

We will then be able to experiment on our codebase and of selected Dafny users, to determine how much it is desirable and a hassle that scoped assumptions become the default.
In the case we consider making scoped assumptions the default (e.g. in Dafny 5),

• We can use the migratory attribute {:scoped-assumptions false}
• Making an assertion reach out to other scopes would be possible through {:unscoped} or {:scoped false}
• The last assertion of a block would automatically be marked {:unscoped} (similar to a function returning a value or the current mechanism of forall .... {} statements that ensures the last assertion if none provided.
• It will be possible to override any behavior or option by writing {:scoped-assumptions false}.

If we do not consider making it the default:

• We might want to lift the attribute to a keyword, for the same reason that {:opaque} became a keyword.

[keyboardDrummer]

Thanks for sharing the notes! Sounds good.

In case you're looking for another opinion about how to continue after doing more experimentation, I'm in favor of the breaking change, but with the option of getting the old behavior using a CLI flag, so existing customers can use that flag for as long as they want, and new customers get the new behavior.