Is it safe to use reads this to say "depends on unspecified external state"?

[samuelgruetter]

class Foo {
    function Property(): int reads this
    method Modify() modifies this {}
    constructor() {}
}

method Main() {
    var f := new Foo();
    ghost var before := f.Property();
    f.Modify();
    ghost var after := f.Property();
    assert before == after; // assertion violation
}

In this example, Dafny fails to prove that before == after (and I think that's good).
However, in the future, someone might come and suggest the following reasoning:

Class Foo has no fields, so the function Property cannot read any state, so in this case, reads this should have no effect, and since Property also takes no arguments, it must be a constant value, therefore before == after holds.

They will implement this by doing something like "if class has no fields, then remove all reads this clauses from its functions", make a PR, which passes all existing tests, it will get merged, and everyone will be happy about this Dafny improvement.

However, in our project we're currently using extern classes which look very similar to the above pattern:

class {:extern} MetadataCollection {
    function {:extern} Content(): map<string, string> reads this
    method {:extern} Add(key: string, value: string) 
        modifies this
        ensures Content() == old(Content())[key := value]
    constructor {:extern} () ensures Content() == map[]
}

Assuming the person didn't think too hard about externs, the patch I described above will have the same effect as commenting out the reads this clause:

class {:extern} MetadataCollection {
    function {:extern} Content(): map<string, string> //reads this
    method {:extern} Add(key: string, value: string) 
        modifies this
        ensures Content() == old(Content())[key := value]
    constructor {:extern} () ensures Content() == map[]
}

But that's bad, because now we can prove false:

method Main() {
    var m := new MetadataCollection();
    ghost var before := m.Content();
    m.Add("testkey", "testvalue");
    ghost var after := m.Content();
    assert before == after;

    assert before["testkey" := "testvalue"] == after;
    assert before == map[];
    assert after == map[];
    assert "testkey" in after;

    assert false;
}

So my question is: Is it safe and future proof to specify extern classes like I did above?

[parno]

Perhaps you could add a test case that would fail if such an optimization were added?

[samuelgruetter]

Good idea! Will do so as soon as @RustanLeino confirms that this optimization should never be added.

[robin-aws]

See #461 and #463 - I assert that the compiler should "think too hard about externs" so you don't have to. :)