-
Notifications
You must be signed in to change notification settings - Fork 264
Modeling External State Correctly
When interfacing with libraries written in C#, we have to write specs for them. Getting these specs correct is crucial, because they are part of our assumptions, and if they don't hold, our proof assumes false, so we don't prove anything.
One thing which is particularly tricky is to model external state correctly.
Let's start with an example:
class {:extern} StringMap {
ghost var content: map<string, string>
constructor {:extern} ()
ensures this.content == map[]
method {:extern} Put(key: string, value: string)
ensures this.content == old(this.content)[key := value]
}
In this first (and bad) approach, we use a ghost var content to model the elements of a StringMap which is implemented in C#, and for all methods, we specify how they affect content.
This specification might look innocent, but it has a serious flaw: Assuming a class satisfies this interface is equivalent to assuming false, as the following example shows:
method Test() {
var m := new StringMap();
m.Put("testkey", "testvalue");
assert "testkey" in m.content;
assert m.content == map[];
assert false;
}
The problem is that we forgot the modifies clause for Put.
Therefore, Dafny assumes that m.content before m.Put equals m.content after m.Put, so we get into a state where m does and does not contain "testkey" at the same time, which is a contradiction.
If we update StringMap as follows, we can't prove false any more.
class {:extern} StringMap {
ghost var content: map<string, string>
constructor {:extern} ()
ensures this.content == map[]
method {:extern} Put(key: string, value: string)
modifies this
ensures this.content == old(this.content)[key := value]
}
However, this is still not good, because var fields in Dafny are public, so the following code verifies:
method Test() {
var m := new StringMap();
m.content := map["never added key" := "never added value"];
assert m.content["never added key"] == "never added value";
}
So we can prove that m contains keys which it will not contain when compiled to C# and run with the C# implementation of StringMap, so our proofs don't apply to what's happening in the compiled program.
The only way to make a variable readonly is to turn it into a function, so we can do the following:
class {:extern} StringMap {
function {:extern} content(): map<string, string>
constructor {:extern} ()
ensures this.content() == map[]
method {:extern} Put(key: string, value: string)
modifies this
ensures this.content() == old(this.content())[key := value]
}
Note that we don't need to annotate the function with ghost, because functions are ghost by default.
Putting the {:extern} annotation on content() is a bit confusing, because there won't be any function called content in the C# code, it's only used for specification purposes. The reason we have to put this annotation is that otherwise the Dafny to C# compiler would complain that content() has no body.
But now, the test from before passes again:
method Test() {
var m := new StringMap();
m.Put("testkey", "testvalue");
assert "testkey" in m.content();
assert m.content() == map[];
assert false;
}
So why can we prove false again? What's wrong about our specification?
The reason is that in Dafny, functions are mathematical functions, whose output can only depend on their input, and on nothing else.
In the function call m.content(), the only input is the (address of) m, and since that is the same before and after m.Put, Dafny infers that m.content() is the same before and after m.Put, and we can prove false the same way as before.
To fix this, we have to tell Dafny that content actually depends on more state: It also depends on the external state of StringMap.
We use this within StringMap for that, because Put already has a modifies this clause, so this will tell Dafny that the state of StringMap has changed.
So we just add reads this to content(), and to make the example more interesting, we also add a Get function.
class {:extern} StringMap {
function {:extern} content(): map<string, string> reads this
constructor {:extern} ()
ensures this.content() == map[]
method {:extern} Put(key: string, value: string)
modifies this
ensures this.content() == old(this.content())[key := value]
function method {:extern} Get(key: string): (r: Result<string>)
ensures
match r
case Success(value) => key in content() && content()[key] == value
case Failure(e) => key !in content()
}
datatype Result<T> =
| Success(value: T)
| Failure(error: string)
Unfortunately, we forgot the reads clause of Get, and now Dafny can prove false again:
method Test() {
var m := new StringMap();
m.Put("testkey", "testvalue");
var r := m.Get("testkey");
assert false;
}
The reason why it can prove false is quite involved:
The postcondition of Get says that in order to know whether to return Success or Failure, every implementation of Get must be able to determine whether key is in content(), but assuming an implementation can do that is a contradiction, because Get has no reads clause, so Dafny can infer false from this.
So finally, this is how to specify the class correctly:
class {:extern} StringMap {
function {:extern} content(): map<string, string> reads this
constructor {:extern} ()
ensures this.content() == map[]
method {:extern} Put(key: string, value: string)
modifies this
ensures this.content() == old(this.content())[key := value]
function method {:extern} Get(key: string): (r: Result<string>)
reads this
ensures
match r
case Success(value) => key in content() && content()[key] == value
case Failure(e) => key !in content()
}
A good way to catch such problems early is to use module refinement to provide a dummy implementation of each extern class to check if the specs we're assuming are feasible.
We put the StringMap into a module called Externs (or any other name we choose), and we create an additional module Externs_Feasability which refines Externs.
That is, it has to have all definitions of Externs, but may strengthen the specifications (in our case it will not do any strengthening, but just provide implementations).
We do this in a file called externalState_feasability.dfy (which does not depend on the previous code snippets):
module {:extern "Lib"} Lib {
datatype Result<T> =
| Success(value: T)
| Failure(error: string)
}
module {:extern "Externs"} Externs {
import opened Lib
class {:extern} StringMap {
function {:extern} content(): map<string, string>
// If I forget the reads clause here, I will get
// "insufficient reads clause to read field"
// in the implementation in Externs_Feasability
reads this
constructor {:extern} ()
ensures this.content() == map[]
method {:extern} Put(key: string, value: string)
// If I forget the modifies clause here, I will get
// "assignment may update an object not in the enclosing context's
// modifies clause" in the implementation in Externs_Feasability
modifies this
ensures this.content() == old(this.content())[key := value]
function method {:extern} Get(key: string): (r: Result<string>)
// If I forget the reads clause here, I will get
// "insufficient reads clause to read field"
// in the implementation in Externs_Feasability
reads this
ensures
match r
case Success(value) =>
key in content() && content()[key] == value
case Failure(e) =>
key !in content()
}
}
module Externs_Feasability refines Externs {
class StringMap {
var private_content: map<string, string>
function content(): map<string, string> { private_content }
function method Get(key: string): (r: Result<string>) {
if key in private_content
then Success(private_content[key])
else Failure("key not found")
}
method Put(key: string, value: string) {
print "Externs_Feasability.StringMap.Put is called\n";
this.private_content := this.private_content[key := value];
}
}
}
module Program {
// uncomment import below if you want to check that all methods
// have a feasability check (need to compile to C# to detect missing ones)
//import opened Externs_Feasability
import opened Externs
method Main() {
var m := new StringMap();
m.Put("testkey", "testvalue");
assert m.content()["testkey"] == "testvalue";
var v := m.Get("testkey").value;
assert v == "testvalue";
print v, "\n";
}
}
When trying to implement StringMap.content, StringMap.Get, and StringMap.Put in Dafny, we will get errors if we forgot the reads clauses or modifies clauses, and if we had added a postcondition which is always false, we would notice because we wouldn't be able to prove the postcondition.
Note that Externs_Feasability.StringMap inherits the specifications of Externs.StringMap, so we don't have to write them down again (unless we wanted to strengthen them).
So now our assumptions about the external functions can still be wrong, but at least we know that they are not contradictory, because we have given an implementation in Dafny which satisfies them.
Now to complete the example, let's implement our external StringMap in C# in a file called StringMap.cs:
using System;
using System.Collections.Generic;
using Lib;
namespace Externs {
class StringMap {
private IDictionary<String, String> content;
public StringMap () {
this.content = new Dictionary<String, String>();
}
public void Put(Dafny.Sequence<char> key, Dafny.Sequence<char> value) {
Console.WriteLine("C# Externs.StringMap.Put is called");
this.content.Add(key.ToString(), value.ToString());
}
public Result<Dafny.Sequence<char>> Get(Dafny.Sequence<char> key) {
String result;
if (content.TryGetValue(key.ToString(), out result)) {
return Result<Dafny.Sequence<char>>.create_Success(
Dafny.Sequence<char>.FromString(result));
} else {
return Result<Dafny.Sequence<char>>.create_Failure(
Dafny.Sequence<char>.FromString("key not found"));
}
}
}
}
If we run dafny externalState_feasability.dfy StringMap.cs /compile:3 it verifies, compiles and runs the program, and prints
Dafny 2.3.0.10506
Dafny program verifier finished with 7 verified, 0 errors
Compiled program written to externalState_feasability.cs
Running...
C# Externs.StringMap.Put is called
testvalue
A final minor note: We actually have to also compile our program to C# using the _Feasability module, because otherwise, if we forget to implement a method in the _Feasibility module, Dafny does not complain, because the method was declared external in the original module, so we wouldn't notice that we forgot a feasibility check.
Compiling the program to C# using the _Feasability module catches this, because the Dafny to C# compiler will complain that a method is missing.