"....must be allocated in the two-state function's previous state"

[MikaelMayer]

I don't know what this error means:

datatype IncomingMessage = IncomingMessage(id: int)
datatype OutgoingMessage = OutgoingMessage(id: int)

class TestClass {
  twostate predicate onMessageSpec(inMessage: IncomingMessage, outMessage: OutgoingMessage) {
    true
  }
  method onMessage(message: IncomingMessage) returns (answer: OutgoingMessage)
    modifies this
    ensures onMessageSpec(message, answer) {
  }
}

The error message is:

[{
	"message": "argument 1 ('outMessage') must be allocated in the two-state function's previous state",
	"source": "Verifier",
	"startLineNumber": 10,
	"startColumn": 36,
	"endLineNumber": 10,
	"endColumn": 42
}]

[robin-aws]

I've hit this a bunch myself, especially while working on dafny-lang/libraries#37 which involves repeating a common post-condition many times. :P

Currently, all parameters to a two-state definition must be allocated before the previous state. This is so expressions using old(...) are always well-formed, as otherwise you can attempt to read heap state that didn't actually exist in the previous state of the heap.

You have more flexibility when making assertions in, for example, the body of a method, since you will only hit an error if you actually attempt to apply old(...) to an expression that refers to objects that were not already allocated on entry to the method. But a twostate abstraction currently has no way to specify whether a particular argument is safe to dereference in the previous state, so it has to be conservative and require that ALL arguments are. You can technically add a pre-condition of old(allocated(outMessage)) to your onMessageSpec predicate, but in practice you often won't be able to satisfy that, since you often DO need to allocate your result.

I'd love to have a way of relaxing this restriction, but haven't put any thought into what the language feature would look like yet.

[MikaelMayer]

In my case, onMessageSpec only reads this, but its argument are datatypes, and I just want to match what the method returns with the pre/post state of the class. What is the right abstraction to do that?

[robin-aws]

Ah, I missed the fact that in this case your arguments are datatypes. In that case you can just add another ensures clause to make Dafny happy - it reads oddly, but it's enough to make the verifier realize that the argument doesn't reference the heap at all:

datatype IncomingMessage = IncomingMessage(id: int)
datatype OutgoingMessage = OutgoingMessage(id: int)

class TestClass {
  twostate predicate onMessageSpec(inMessage: IncomingMessage, outMessage: OutgoingMessage) {
    true
  }
  method onMessage(message: IncomingMessage) returns (answer: OutgoingMessage)
    modifies this
    ensures old(allocated(answer)) // <--
    ensures onMessageSpec(message, answer) {
  }
}

[MikaelMayer]

That's the answer, thank you very much !