TLA+ quickie: modelling rust code

One often has mutable objects when working on network protocols. It’d be nice to be able to model these in TLA+ to check message flows but can be confusing.

I like the pattern I came up with for modelling mutable objects whose methods have return values.

We’ll start with the basics of Result. I’ve chosen a 2-tuple to represent the success of the result and the final state of the object resulting from a method call. It’s easy to get into the habit of using IsErr(x)/OkOf(x) when simulating the transformation resulting from a method call that can yield an error. Doing this, you can write a method resulting in error as a cascade of IF/THEN applications or a single decision and a call to another function. Returning early in the error case makes sense for text flow. I used it like this (which is fairly readable by pure TLA+ standards).

ReceiveMessage(ob,m) ==
  LET ob1 == UpdateStats(ob, m) IN
  IF IsErr(ob1) THEN
    ob1
  ELSE 
  LET ob2 == ReactToMessage(OkOf(ob1), m) IN
  IF IsErr(ob2) THEN
    ob2
  ELSE
  Ok(QueueReaction(OkOf(ob2)))

Because I only needed int returns from methods that could return Err, I modeled Result as below. This configuration made Ok(obj) the same as Return(0, obj) which was convenient for my purposes.

\* Basic result accessors
IsErr(v) == v[1] < 0
OkOf(v) == v[2]
Err(p) == << -1, p >>
Ok(p) == << 0, p >>
RvOf(p) == p[1]
Return(v,p) == << v, p >>

Extending it to support more interesting results is pretty easy. Return and Ok become distinct, but IsErr and OkOf work on Return, Ok and Err results:

\* Basic result accessors
IsErr(v) == v[1] < 0
OkOf(v) == v[2]
Err(p) == << -1, p >>
Ok(p) == << 0, p >>
RvOf(p) == p[3]
Return(v,p) == << 0, p, v >>

Applying a pattern consistently can let you do surprisingly well at tasks that seem daunting, such as translating a fair amount of code from one language to another. This kind of modelling can easily reveal cases where the ordering of events or amount of time certain steps take is critical even if it doesn’t seem like it should matter, and give indications about what kinds of grief are worth writing tests for.