…Unless you are specifying a garbage collector.

I have written about 1100 lines of Quint over this week. Similar to my experience of writing TLA+ specifications, what I noticed with Quint is that there is a big difference in my specification style that depends on where I start from:

  1. Source code. This is the case when a protocol already has an implementation. In this case, there is a high chance that the code is the only reliable source of truth. Even if there is a high-level protocol specification, it either too imprecise or outdated. Arguably, having an outdated protocol specification is still better than having no specification at all. Typically, the code is “working”, but it is not exactly clear what happens if things “go wrong”.

  2. Specification in English. This is the case when a protocol is still in the design phase. The project may already have a code prototype, but there is a lot of uncertainty about failure scenarios. Typically, the what is known at this stage is the “happy path”, that is, an example of how the protocol is supposed to work, when “nothing wrong” happens.

This time I started with the source code, having essentially no specification. When you are starting with the code, it is very tempting to use exactly the same data structures and operations, as you see them in the code. This is a trap! The rule that I have learned over multiple iterations is as follows:

The data structures in a protocol specification shall be more abstract than the data structures in the source code.

Every time I deviate from this rule, I have to re-learn it. There are many instances of this rule. In this blog post, I am focusing only on one instance: The use of maps and the memory considerations that are related to this data structure.

1. What are maps?

If you are developing software, there is a very good chance that you have been using maps. They have slightly different names in different programming languages: HashMap and SortedMap in Java/Scala, a map in Go, HashMap and BTreeMap in Rust, dictionaries in Python, mapping in Solidity, etc. In all these languages, maps have more or less the same abstract behavior. Since there is no common denominator in programming languages, I am using Quint REPL to demonstrate this abstract behavior:

  1. Construct a map. Construct an empty map. Alternatively, construct a non-empty map by enumerating key-value pairs. This is done with Map(...) in Quint: 
       $ quint
   >>> Map()
   Map()
   >>> Map("alice" -> 3, "bob" -> 5)
   Map("alice" -> 3, "bob" -> 5)
  2. Add or update a key-value pair. Bind a value to a key in a map. For example, bind the value 42 to the key "igor". Importantly, if the map already has a value bound to the key, update the entry, so the key becomes associated with the new value. This is done with put in Quint: 
       $ quint
   >>> Map().put("igor", 42)
   Map("igor", 2024)
   >>> Map("igor" -> 41, "bob" -> 5).put("igor", 42)
   Map("igor" -> 42, "bob" -> 5)
  3. Update a key-value pair. If a value $v_1$ is bound to a key $k$ in a map, then bind a new value $v_2$ to the key $k$. If the map does not have a value for the key $k$, then the behavior is either undefined, or an error is expected (this varies from a language to language). This is done with set in Quint: 
       $ quint
   >>> Map("igor" -> 41, "bob" -> 5).set("igor", 42)
   Map("igor" -> 42, "bob" -> 5)
   >>> Map().set("igor", 42)
   runtime error: error: [QNT507] Called 'set' with a non-existing key
  4. Retrieve the value. Given a key $k$, retrieve the value bound to the key in a map. Usually, it is assumed that there must be such a value. Otherwise, the behavior is either undefined, or an error is expected. This is done with get in Quint: 
       $ quint
   >>> Map("igor" -> 41, "bob" -> 5).get("igor")
   Map("igor" -> 42, "bob" -> 5)
   >>> Map().get("igor")
   runtime error: error: [QNT507] Called 'get' with a non-existing key
  5. Get the keys. Get the keys that are bound to some values in a map. What is actually returned, depends on a programming language. It can be a list, an array, a set, or an iterator. Quint returns the set of keys: 
       $ quint
   >>> Map("alice" -> 3, "bob" -> 7).keys()
   Set("alice", "bob")

:raising_hand: Many programming languages usually have another operation that iterates over key-value pairs. The way it looks like usually depends on the language. I am omitting this operation here, as it can be implemented via a combination of keys, get, and iteration. Similar to that, many languages have an operation m.contains(k) for checking whether a key $k$ has a value bound to $k$ in a map $m$. This one can be implemented via m.keys() and its set membership: m.keys().contains(k).

:information_source: If you know $\tla{}$ or Quint, you know that they both have an additional operator for constructing maps. It looks like S.mapBy(x => e) in Quint and $[x \in S \mapsto e]$ in $\tla{}$. This operator is essential to our discussion. I will talk about it in Section 2.

:warning: I have omitted one more operation over maps. Can you figure out which one is it? Actually, I forgot about it when writing this text, since this operation is almost never used in protocol specifications.

What about types? Perhaps, the biggest differentiator between maps in different programming languages is whether a map may contain values of incompatible types. In statically-typed languages (e.g., Rust), the answer is usually “No”, whereas in dynamically-typed languages (e.g., Python), the answer is “Yes”. Similar to that, Quint answers with “No” to this question, and $\tla{}$ answers with “Yes”.

2. The map-function dualism

If you know $\tla{}$, you must have noticed that what I have been calling a map is actually called a function in $\tla{}$. This may be confusing, as functions in programming languages are different from maps in many ways. However, there is a very good reason for why maps are called functions in $\tla{}$. If you were to math classes, you probably remember the Sign function. It is usually defined over real numbers, but I will define it over the set of all integers $\mathbb{Z}$, to keep things simple. In the spirit of math classes, we would say that $sgn: \mathbb{Z} \rightarrow \mathbb{Z}$ is a function that is defined as follows:

\[sgn(n) = \begin{cases} -1, & \text{if $n < 0$} \\ 0, & \text{if $n = 0$} \\ 1, & \text{if $n > 0$} \\ \end{cases}\]

Similar to the school math, $\tla{}$ offers us a way to write the above function sgn as follows:

$[n \in Int \mapsto \texttt{IF } n < 0 \texttt{ THEN } -1 \texttt{ ELSE } (\texttt{IF } n = 0 \texttt{ THEN } 0 \texttt{ ELSE } 1)]$

Since Quint is following the logic of $\tla{}$, it is possible to write the same in Quint:

Int.mapBy(n => if (n < 0) -1 else (if (n == 0) 0 else 1))

Now, it all makes sense in math, but having a map over a set of all integers sounds like it would require an infinite memory supply. In theory, it does not have to be the case though, since all elements are mapped by the same law in the case of sgn. However, maps are represented as immutable maps in the Quint REPL, which is implemented in TypeScript. So Quint REPL would give up immediately on the above map:

$ quint
>>> Int.mapBy(n => if (n < 0) -1 else (if (n == 0) 0 else 1))
runtime error: error: [QNT501] Infinite set Int is non-enumerable

:information_source: Actually, the set of all integers is Enumerable. What is meant here is that the Quint simulator is trying to enumerate all of the set members to construct a map, and it is clear that it would not be able to do that for an infinite set in finite time. Again, the simulator could be improved to simply cache the lambda expression instead of populating an actual map in this case. We simply did not have time to implement that.

To be able to evaluate our map in REPL, we could define our map over a small finite set. For example, we could define it over the interval $[-2^7, 2^7)$:

$ quint
>>> pure val m = (-2^7).to(2^7 - 1).mapBy(n => if (n < 0) -1 else (if (n == 0) 0 else 1))
>>> m.get(55)
1
>>> m.get(-42)
-1

:information_source: The Quint simulator may internally represent m as an immutable TypeScript map (and it currently does). This looks wasteful :do_not_litter:. I don’t know anyone who would represent the sign function as a map in a programming language. What is important to us:

We are writing specifications to ease our understanding and reasoning about protocols. Hence, we should not expect our specifications to be memory-efficient.

After all, if our specification was as efficient as the implementation, why would we need the implementation? If using a map makes the rest of your specification simpler, then use a map.

Instead of using a map in our example, we could simply define an operator in Quint (and similar in $\tla{}$):

pure def sgnf(n) = if (n < 0) -1 else (if (n == 0) 0 else 1)

In this case, we would not have to worry about memory limitations. Our definition of sgnf is quite similar to a definition in a programming language, where it would be a function. Notice that this approach has a few limitations:

  • You cannot store sgnf as a value of a variable. (This is possible in functional languages though.)

  • You cannot easily do a point-wise update similar to set(key, value).

  • You cannot easily extract the function domain similar to keys().

:information_source: If you would like to learn more about $\tla{}$ functions (which are also Quint maps) and how they compare to maps in programming languages, the Apalache manual has a detailed discussion about TLA+ Functions.

3. Incremental construction vs. immediate construction

Essentially, there are two ways to construct and use maps:

  1. Incremental: Start with an empty map and populate it when needed. This is how it is done in programming languages.

  2. Immediate: Declare a map over its domain (the keys) right away and change the associated values when needed. This is how it is done in math/$\tla{}$.

The incremental construction is the only way to build a map in many programming languages that I know. Dict comprehensions in Python are perhaps a rare exception to this. If you have more examples of languages that would allow for something like mapBy out of the box, I would really love to learn about them.

Update 2024-05-06: Kotlin has association transformations that work very similar to Quint’s mapBy. Thanks, Alexey Zubkov, for sending me the link!

I believe that there is a simple explanation for why maps are constructed incrementally in source code. When you are writing a program, it has to be reasonably efficient. This is why nobody wants to pay the upfront cost of constructing a map that is filled, say, with a lot of zeroes or other default values. Not only would it waste CPU cycles, it would also introduce massive memory overhead. After all, maps are implemented via hash tables or balanced trees.

Update 2024-05-06: As noted by Alexey Zubkov, Kotlin has the function with-default to avoid such upfront construction costs.

What is important to understand is that when you are writing a protocol specification, maps are just another building block, similar to sets. Both sets and maps have non-trivial associated costs in programming languages. This does not matter in protocol specifications:

First, you have to understand how to do something right. Second, think about how to do the right thing efficiently.

4. Thoughts in action

There was a lot of abstract text. Let’s work through a concrete example. I cannot show you the specification that I wrote over this week. Yet, there is a simple example called coin.qnt in the Quint repository. This example specifies the behavior of a Solidity smart contract, see Coin in Solidity for details. If you like to understand the specification, there is a detailed tutorial called Coin in Quint. In the following, I would assume that you understand what is going on in coin.qnt.

We will compare the two styles of using maps, namely, immediate construction and incremental construction, which we have discussed in Section 3.

4.1. Immediate construction

The specification coin.qnt is written in the style of immediate construction. I am going to highlight only the important pieces.

The specification is quite small. It declares a map called balances in Line 52:

    // the balances in the subcurrency tokens
    var balances: Addr -> UInt

Since we want to initialize the variable balances in one go, instead of constructing it step by step, we have to decide on the set of keys of balances. As this specification stems from the Coin in Solidity, the most straightforward answer is: The set of keys is the set of all Ethereum addresses. An Ethereum address is 20 bytes long. This makes $2^{8^{20}}$ addresses, which is approximately $1.4 \cdot 10^{47}$. If this was essential for the smart contract in question, we could define this set. It is not really important though.

One way of dealing with predefined values like the set of all addresses is to define a constant:

// all 20-byte strings
const ADDR: Set[Addr]

By doing so, we could reason about the protocol without fixing the set of all addresses. For testing purposes, we could instantiate ADDR with a small set of addresses. In coin.qnt, we do not declare ADDR as a constant, which would require us to declare another module for testing, but we simply fix it to be a small set of addresses right away in Line 47:

pure val ADDR = Set("null", "alice", "bob", "charlie", "eve")

Having the set of all addresses, we can immediately initialize the balances, see Line 62. I have replaced the non-essential code with [...]:

// state initialization
action init = {
  // [...]
  all {
    // [...]
    balances' = ADDR.mapBy(a => 0)
  }
}

This initialization is surprisingly consistent with how maps are initialized in Solidity. They are initialized with the default values. That is, with all zeroes in this case. (This does not mean that Ethereum stores $1.4 \cdot 10^{47}$ zeroes!)

Now let’s have a look at how balances is queried and updated. We will only look at the action send in Line 94, all non-essential code is replaced with [...]:

action send(sender: Addr, receiver: Addr, amount: UInt): bool = all {
  require(not(amount > balances.get(sender))),
  if (sender == receiver) {
    // [...]
  } else {
    val newSenderBal = balances.get(sender) - amount
    val newReceiverBal = balances.get(receiver) + amount
    all {
      // [...]
      balances' =
        balances.set(sender, newSenderBal).set(receiver, newReceiverBal)
    }
  },
  // [...]
}

There are a few things to note here:

  • We simply use balances.get(sender) and balances.get(receiver) instead of testing, whether sender and receiver belong to the balances.keys(). We know they do, since we have initialized balances over all addresses from ADDR.

  • We do not have to think about whether to insert a new key-value pair, or to update an existing one. Again, we know that that all keys from ADDR are present in balances. So we are simply using set.

There is not much to talk about here. The specification is quite simple. This is actually the point! We do not have to do any memory-related manipulations over maps. Instead, we focus on the logic of the smart contract.

Now we are going to compare this simple approach with the “standard” approach of incremental construction.

4.2. Incremental construction

To illustrate my point, I have modified coin.qnt to construct balances incrementally, as you would typically find it in many implementations (not in Solidity though!). You can find the modified version in coin_incremental.qnt.

First, we modify the action init to initialize balances with an empty map.

// state initialization
action init = {
  // [...]
  all {
    // [...]
    balances' = Map()
  }
}

This is nice! The code is simpler and the map does not waste any resources.

Now, we have to modify the action send. Since balances may be empty, we have to be careful about not using balances.get(sender), if there is no value for sender.

This kind of logic is required so often that programming languages usually have a helper function that returns the default value, in case there is no value for a key. For example, in Scala such a function is called getOrElse. For this reason, we even have introduced getOrElse in the Quint common definitions, see basicSpells.qnt. It looks like this:

pure def getOrElse(map, key, default) = {
  if (map.keys().contains(key)) map.get(key) else default
}

Having getOrElse, we rewrite send as you can see below. To save your time, I have left the old lines in comments.

action send(sender: Addr, receiver: Addr, amount: UInt): bool = all {
  require(not(amount > balances.getOrElse(sender, 0))),
//require(not(amount > balances.get(sender))),
  if (sender == receiver) {
    // [...]
  } else {
    val newSenderBal = balances.get(sender) - amount
    val newReceiverBal = balances.getOrElse(receiver, 0) + amount
//  val newReceiverBal = balances.get(receiver) + amount
    all {
      // [...]
      balances' =
        balances.set(sender, newSenderBal)
                .put(receiver, newReceiverBal)
//              .set(receiver, newReceiverBal)
    }
  },
  // [...]
}

The modified version is also not bad, though it has a bit of additional complexity. What I would like to highlight here is that this version requires more attention from the reader:

  • When we don’t know, whether a key is present in balances, we are using getOrElse such as in balances.getOrElse(sender, 0).

  • When we know that the key is there, we are using get such as in the second occurrence of balances.get(sender).

  • Similarly, we distinguish between inserting into and updating balances such as balances.set(sender, newSenderBal) and balances.[...].put(receiver, newReceiverBal.

  • Every time we use getOrElse, we have to make a decision about the default value. In this case, it is just zero. Sometimes, we would have a more complex data structure. We would have to refer to a constant in that case.

In my opinion, this modified version of coin.qnt is harder to read. It was also harder to write. Instead of focusing on the core logic, we have to take of the contents of balances way too much.

5. Conclusions

I hope that you are convinced now that coin.qnt is a better specification than coin_incremental.qnt. When I was writing my specification this week, I also introduced getOrElse and put all over the place. After finishing the specification, I made a refactoring pass and replaced 20-30 occurrences of getOrElse and put with get and set, respectively. This made my specification much cleaner.

Why do I keep using getOrElse and put? Well, because when I am looking at the implementation code, I tend to think about all the uninteresting implementation details. The good news is that if you cannot stop thinking about all these getOrElse and put, you can use them and remove them later, as I did.

When it comes to $\tla{}$, something interesting is happening there:

  • It is possible to construct an empty map (a $\tla{}$ function) but it is not entirely obvious how to do that. One way is to write something like $[x \in \texttt{{}} \mapsto \texttt{FALSE}]$. Of course, if you care about types, like we do in Apalache, you would have to use a value of the proper type instead of $\texttt{FALSE}$.

  • $\tla{}$ does not have a built-in operator that behaves similar to put in Quint. The standard module of TLC (the explicit-state model checker of $\tla{}$) has the operator f @@ g that behaves similar to put, see @@.

  • $\tla{}$ does not have a built-in version of getOrElse, even though it would be quite easy to define one.

Given these considerations, my conclusion is that $\tla{}$ is clearly designed in favor of immediate map construction, which we discussed in Section 4.1. In my discussion of $\tla{}$ specifications with engineers, I was constantly asked to add something similar to Quint’s Map(), put, and getOrElse. This is why Quint has these primitives. Now I can see that the engineers were simply in the coding mindset, when they asked for that.

Having written multiple specifications in $\tla{}$ and Quint, I believe that Leslie Lamport has chosen the right set of primitives in $\tla{}$. Taking care of maps/functions is an implementation detail. This is similar to thinking about whether to allocate data on the stack, or on the heap. We simply do not care about these details in protocols. I will avoid Map(), put, and getOrElse in my Quint specifications in the future; obviously, the same applies to $\tla{}$. I recommend you doing the same.

There are many more specification patterns that violate the basic intuition of software engineers. I will cover them in follow up blog post, once I stumble upon them.

Do you want to receive notifications when I write something new? Subscribe to the newsletter. New blog posts are going to be announced once per week (maybe twice, if I really have something!).

Powered by Buttondown.