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.

(TODO: More on module refinement should be added here).