Compiled Dafny methods can be invoked in target language without satisfying preconditions

[robin-aws]

I believe this is a well-known implicit issue, but I'd like to make it explicit and propose a fix.

Example:

// In Dafny code:
module {:extern} MyMathModule {
  method SafeDiv(a: int, b: int) returns (c: int) requires b != 0 {
    return a / b;
  }
}

// In C# code:
MyMathModule.SafeDiv(5, 0) // Raises DivideByZeroException inside BigInteger

The key issue is that the error raised is pretty internal, and not at the point of actual failure. In more complicated cases this makes it a lot harder to reason about the behaviour of the program. In particular, null references could be passed through many layers or stored for later, since most target languages will not prevent passing nulls into Dafny methods.

Currently {:extern} really only provides stable naming, but I propose making {:extern} a hard requirement for making Dafny methods callable in the target language, and to make it a compiler error if the target language cannot guarantee the method's preconditions directly. This would force developers to dynamically check these requirements as needed:

  method {:extern} SafeDivExtern(a: int, b: int) returns (c: Result<int>) {
    if (b == 0) {
       c := Failure("Div by zero");
    } else {
      var result := SafeDiv(a, b);
      c := Success(result);
    }
  }

  method SafeDiv(a: int, b: int) returns (c: int) requires b != 0 {
    return a / b;
  }

Note that this idiom affects the result type, since it has to allow for dynamic errors somehow.

More or less the dual of #463 , but I wanted to cut the issues separately since they relate to two different use cases for {:extern}, and we may want to separate them.

[RustanLeino]

About the mechanism: Maybe the proposed stricter functionality could be a separate annotation? For example, {:extern} (as before) and {:safeExtern}, or perhaps {:unsafeExtern} (for the existing behavior) and {:extern}. And/or a command-line switch that says to make all externs safe.

About the check: Would the check work like this: It

• simply forbids all pre- and postconditions,
• forbids all subset types (including non-null types),
• forbids any datatype or class types with fields that have such types,
• ignores the possibility that the native routines might not terminate or might throw an exception,
• is unsound for modifies and reads clauses,
• is unsound for functions being deterministic (or perhaps it forbids functions altogether).

[robin-aws]

About the mechanism: Maybe the proposed stricter functionality could be a separate annotation? For example, {:extern} (as before) and {:safeExtern}, or perhaps {:unsafeExtern} (for the existing behavior) and {:extern}. And/or a command-line switch that says to make all externs safe.

My preference was just to have the command-line switch for the sake of backwards compatibility, but to strongly push code towards the safe version. I assert that if code wants to have externs with unverified assertions, they can be attached by wrapping functions that use axioms or assumes. I like the idea of having a limited number of mechanisms for controlled unsoundness, so it is as obvious as possible where assertions are unverified.

About the check: Would the check work like this: It

• simply forbids all pre- and postconditions,
• forbids all subset types (including non-null types),
• forbids any datatype or class types with fields that have such types,
• ignores the possibility that the native routines might not terminate or might throw an exception,
• is unsound for modifies and reads clauses,
• is unsound for functions being deterministic (or perhaps it forbids functions altogether).

Indeed, that's exactly the approach that I've partially implemented. I think it may be wise to not fully give up on soundness w.r.t. the heap, as it may be necessary to ensure invocations from external code back into Dafny can still ensure things like object invariants, but I'm still experimenting with that.

[samuelgruetter]

We should keep in mind that many kinds of pre- and postconditions are not (efficiently) testable:

• foralls over int would require an infinite number of tests, because int is arbitrary precision, and even foralls on int32 would require infeasibly many tests.
• exists has the same problem.
• Abstract predicates are not testable either, but very useful: For instance, if you're interfacing with an external crypto library, you don't need to re-implement or specify encryption and decryption in Dafny. All you need is to state that there exists a predicate R taking a plaintext and a ciphertext and returning a boolean telling if the ciphertext is the encrypted version of the plaintext. Then you can specify the external encryption and decryption methods in terms of R, and keep track of which ciphertexts correspond to which plaintexts in your Dafny code by using R. But since R has no body in Dafny, you won't be able to run it in Dafny to dynamically check if the external code did what you expected. And if you bother to write down an executable version of R in Dafny and are willling to run it each time you run the external method, there's actually no need to run the external method any more.
• modifies clauses are actually postconditions too: If a method is annotated with modifies x, this corresponds to a very strong postcondition, namely, "forall heap addresses a different from x, the heap at address a is the same after calling the method as it was before calling the method". This is a forall as well, and testing it dynamically won't work.

So in order to make this feature possible, we would have to disallow all of the above features, but that would mean to disallow the very features which set Dafny apart from its alternatives.

But at the end, it all depends on the use cases: If you have many use cases which get away without using any of the above features, then I'll be convinced that the feature proposed here is a good one.

Also, when designing this feature, it could be very easy to introduce unsoundness, so the well-meant "safe" mode could actually be less safe than what we have now. Here's what could happen: Suppose that Joe the Dafny apprentice writes a stub for an external method

// intended spec: increments x.someField by 1
method {:extern} ExternFoo(x: Bar)

but doesn't add any pre- and postconditions or modifies clauses because he's been told to use this "safe" mode, and then dutifully checks after each invocation of ExternFoo that it did what he expects, and turns on dynamic checking of assume statements, so he'll write code like this:

var old = x.someField
ExternFoo(x)
assume(x.someField == old + 1)
// HERE

Now, at the spot marked with HERE, Dafny will be able to prove false, because ExternFoo has no modifies clause, so Dafny thinks it can't modify any part of the heap, so Dafny thinks that x.someField == old, but it's also told to assume x.someField == old + 1, which is a contradiction, so Dafny will now "prove" anything, no matter whether it holds or not. Joe won't notice, but he'll be delighted how fast and easily Dafny proves all verification conditions below the HERE marker...

The only way to fix this and to obtain a truly "safe" mode would be to say that if an external method has no modifies clause, it defaults to modifies *, that is, "potentially modifies any part of the heap". However, such methods are almost unusable, because most of the time, you need to assume that the values of the Dafny objects not involved in the external call remain the same after the external call -- if the external call were to havoc your whole heap, you'd be lost. Now you could say, we just add assume statements after the external call which test that the parts of the heap we care about were not changed, but usually we need to test that everything except some heap area is unchanged, and that would be impractical or even infeasible to test.

That being said, my comments are only based on the small number of use cases I have seen, but such language design decisions should be based on a large number of different use cases, so it would be good to collect more of them, ideally publically, before settling on how/whether to implement such a feature.

[robin-aws]

We should keep in mind that many kinds of pre- and postconditions are not (efficiently) testable: ... So in order to make this feature possible, we would have to disallow all of the above features, but that would mean to disallow the very features which set Dafny apart from its alternatives.

Definitely, and I've mentioned this in the closely-related issues on evaluating predicates at runtime (#547 is the latest). The intent is to force code to state more explicitly whether an assertion on external code is assumed true without statically or dynamically verifying it (using axioms) or dynamically checking it using something like expect. For some assertions the only practical option will be axiomizing them. I just like the idea of being more rigorous about the process and making code document more explicitly which is which.

Regarding the issues with modifies clauses, I'm hoping there's a middle-ground where we can assert that "Dafny" values and "external" values can be cleanly partitioned by controlling what kind of values are passed to external code, so that the default modifies {} clause can actually be true. This is definitely experimental though, and as a fallback it might be better to maintain the current behaviour of modifies on {:extern} methods, since as you say forcing developers to at least think about what the method actually modifies is better.

That being said, my comments are only based on the small number of use cases I have seen, but such language design decisions should be based on a large number of different use cases, so it would be good to collect more of them, ideally publically, before settling on how/whether to implement such a feature.

Absolutely, and that's one of the reasons I cut #461 and #463 well ahead of actually trying to implement any solution. @RustanLeino forced my hand a bit :) but don't take my response as the only possiblity.

[parno]

One quick observation:

forbids all subset types (including non-null types)

This would appear to mean that an API that takes in an integer must use int or nat, which would translate to a BitInteger of some sort. I suspect most callers wouldn't be happy with such an interface, so we may want to expand this to allow "basic" subset types that map directly to machine integers.