Function by method bodies should not be allowed to contain expect statements

[robin-aws]

Similar to #1346, which is about tracking the side-effects of print, in particular in the context of function by methods, but arguably more concerning.

function method GoodFunction(n: nat): nat {
  expect n > 0; // Error: expect statement is not allowed in this context...
  0 / n + n
}

// Verifies and compiles without errors
function BadFunction(n: nat): nat {
  n
} by method {
  expect n > 0;
  return 0 / n + n;
}

This creates a function whose specification-time behavior does not completely align with its compiled behavior: BadFunction(0) is equal to 0 and yet halts at run time.

In retrospect, I would argue that expect is tightly coupled to termination proofs: a failed expect statement causes a method to fail to terminate just as infinite recursion would. I propose forbidding expect statements in any method that does not have decreases *, which would would then forbid its use in function by methods since they cannot skip termination proofs with that syntax. This would break backwards compatibility but could be reasonable, given expect is only used in test code to the best of my knowledge.

[hmijail]

How would this apply to the documentation's example of using expect to check an :extern result?

[robin-aws]

It just implies the method would need to declare decreases *, which is allowed since the example is a method and not a function method. That's arguably a more accurate declaration of the :extern signature anyway, since there is no guarantee external code will terminate.

It would be useful in the future for Dafny to still support termination proofs of methods that call other methods with decreases * somehow, but there isn't a concrete proposal for that yet.

[RustanLeino]

Thank you for pointing out that it would be good for Dafny to offer to track the use of expect statements, since these statements can cause the program to halt at run time.

It's sort of related to non-termination, in that expect can cause a program not to reach its end. But I think the enforcement mechanism should be different than decreases *. For one, you are not allowed to declare a function with decreases *, and yet an expect statement may be part of the execution of a function.

A primary use of the expect statement is to mitigate problems with specifications for :extern methods. For example,

method Random(n: int32) returns (r: int32)
  requires 0 < n
  ensures 0 <= r < n
{
  r := JavaRandom(n);
  expect 0 <= r < n;
}

method {:extern "java.util.Random"} JavaRandom(n: int32) returns (r: int32)
  requires 0 < n

shows how the Random method is able to promise a postcondition even though the specification of the extern JavaRandom is specified without one. It would be unfortunate if large parts of a program were not checked for termination, as would happen if all transitive callers of Random would have to be declared with decreases *.

So, while tracking "expect effects" is similar to tracking non-termination, in that both affect all transitive callers, I think the tracking mechanism of expect should be different than that for non-termination. Tracking "expect effects" thus looks very much like the tracking of "print effects" (#1346). Following #1346, I suggest that we add support for an {:expect} attribute and add a /trackExpectEffects flag (where "no expect-effect tracking" is the default).

[keyboardDrummer]

Following #1346, I suggest that we add support for an {:expect} attribute and add a /trackExpectEffects flag (where "no expect-effect tracking" is the default).

Note that if we ever add a feature to automatically generate expect statements related to extern calls, then you might need an {:expect} annotation even though you didn't write any expect. How do you feel about a name like {:canHalt} ?

Also, what would be the benefit of tracking expect-effects? Why would a programmer want to track where in their code there is the potential for a halt due to unverified downstream code?

Would the expect-effect tracking allow the programmer to avoid code like this?

var x = ClaimAResource()
DoSomethingThatMayHalt();
FreeResource(x);

I would like to understand the use-case for except-effect tracking better before adding it as a feature. I also wonder whether just tracking halts is enough, or whether this would also create the need for a mechanism to recover from halts.

[robin-aws]

As the original author of expect, let me provide some history and motivation to help clarify the current state. :) The original proposal is here: #547

The primary motivation was really being able to write tests in Dafny. We initially found that using Result<T> and :- made it technically possible to test assertions dynamically, but the user experience left a lot to be desired. The equivalent implementation of expect was a method like the following:

method Expect(p: bool) returns (result: Result<()>) 
  ensures result.Success? ==> p 
{
  if p {
    return Success(());
  } else {
    return Failure("Failed expectation");
  }
}

One of the more serious issues with this approach was that it was too easy to accidentally ignore the result:

var someValue := GoDoAThing();
var _ := Expect(someValue == 42);

This actually has no effect, even if someValue is not 42! The right way to use Expect was as follows, to ensure the Failure is propagated:

var _ :- Expect(someValue == 42);

Since expect was a useful way to dynamically test assertions without polluting code with Results, it also seemed to be a useful way to validate the contract of external methods.

@keyboardDrummer: I agree that halting is the real effect to track rather than expect. I don't think we should make it possible for user code to recover from halting though. If some feature higher in the "stack" was able to recover and continue execution, there would be no guarantee that the post-conditions of all the methods on the stack were satisfied, so you would be in major danger of runtime errors that should have been proven impossible.

In my opinion, an error state that is recoverable should be modelled as an explicit value and likely handled/propagated using :-. As I work out what thread safety guarantees Dafny can provide when used by concurrent code in one of the target languages, we may need to be more cautious about recommending using expect outside of test code. Internally, we likely need to treat halting with the same severity as an OutOfMemoryException in Java.

@RustanLeino: I think you're correct that decreases * is not the best way to allow expect. I was looking for a way to allow localized unsoundness by assuming that code terminated, either because it was implemented in native code or included expect statements that were not expected (ha) to be hit in practice. But I think we should think of decreases * as "this method does not terminate by design" rather than "this method should terminate but I can't prove it, so I want to turn off the termination prover".

[keyboardDrummer]

I don't think we should make it possible for user code to recover from halting though. If some feature higher in the "stack" was able to recover and continue execution, there would be no guarantee that the post-conditions of all the methods on the stack were satisfied, so you would be in major danger of runtime errors that should have been proven impossible.

In case you call a method that halts then I think you wouldn't do anything with the post-condition. Could you not compute a replacement post-condition based on the modifies clause that implements the maximum disturbance the method could have?

To be clear, the reason I mentioned a recovery mechanism is that I don't understand yet what the purpose is of tracking whether code can halt or not, and being able to recover from halted code would give tracking it more use.

[robin-aws]

Having mulled this over for a while, I've arrived at a concrete alternate proposal.

expect is a way of knowingly introducing unsoundness into your verified code. It's intended to let you avoid proving something you believe to always be true, without writing a bunch of error handling you expect to be dead code. By extension this makes it well-suited to writing tests, but also to interacting with external code where if an assumption is violated there's no reasonable way to continue execution.

I assert that by default expect should not be allowed anywhere in a Dafny codebase unless you opt into that unsoundness. You should be able to pass a /allowExpect flag if you want to use this feature. The typical default layout for a Dafny codebase would be to only pass this flag when building/verifying/testing the test source directory but NOT the src directory by default.

As an aside, I've wanted to find a way for Dafny to support more "incremental verification", so that people can get started and make progress on Dafny code quicker, while tracking the fact that they still have work to do to prove correctness. This would mirror the benefits of gradual typing. I've arrived at the conclusion that expect is ideal for that: you can count all the expects in your code as a metric to drive down over time, and likely set up the mechanism to forbid code built with /allowExpect from ever making it to production.

[RustanLeino]

I agree with this view of expect. Having an /allowExpect flag without which the compiler (not the resolver or verifier) complains upon encountering an expect statement is also fine with me.

To make sure I understand the alternate proposal, @robin-aws , you're suggesting that we not have any other finer-gain expect checking, right? That is, either you opt in and use the /allowExpect flag and that means you can use expect anywhere, or you don't use the /allowExpect flag and then the compiler will refuse to output any code that has an expect statement. Is that right? If so, that sounds fine with me.

As a general design point (now addressing @keyboardDrummer 's points and questions), I think that it seems reasonable for a verified language to offer some kind of control over each possible effect in the language. Since expect statements can bring about a "halting effect", then having some way to control it seems reasonable to me. The {:expect} attributes I proposed above are perhaps overkill, but /allowExpect would also satisfy me.

[robin-aws]

That's correct - I'm suggesting that the course-grained CLI flag is enough, mainly just to let the build process specify the scope where expect should be allowed, which I imagine will be much less of a pain than having to add {:expect} transitively everywhere.

The only advantage I can think of for the {:expect} attribute is for a Dafny codebase A to depend on another B as a library, and for A to be able to assert that B does not use expect anywhere. For now this isn't a problem because using include means that the build process for A will still examine the implementation of B and therefore object to any expect uses. When we support Dafny libraries, such as the proposal in dafny-lang/rfcs#5, we'll want to include metadata in however we represent libraries so that we can still support this use case.