Skip to Content
Quint
DocumentationLessonsAnatomy

Anatomy of a Protocol

In this lesson, we explain the standard structure of a Quint protocol specification. Although Quint does not impose a very rigid structure on protocol designers, we have found that following common practices helps protocol authors and their readers to cooperate more effectively.

As a running example, we specify the ledger of a simple bank. The bank keeps an account balance for every customer, denominated in cents. Like most real ledger software, the bank’s core system stores each balance in a fixed-width machine integer. In our case, an unsigned 32-bit integer. This means our specification has to worry about a very real-world problem: arithmetic overflow.

Our bank operates under the following rules:

  • One account holder is designated as the issuer (think of it as the central bank): only the issuer can create new money.
  • The issuer may deposit newly issued money into any account, including their own.
  • Account holders may transfer money to other accounts, provided that they have enough on their balance.

What this lesson covers:

  • The standard layers of a Quint specification: types, functional layer, and state machine.
  • Declaring protocol parameters, state variables, and helper definitions.
  • Actions that read and modify the protocol state, and non-deterministic inputs (nondet and oneOf).
  • Invariants and temporal properties.
  • Writing tests as runs: from single data points to non-deterministic inputs.
  • Running the random simulator to discover an invariant violation.

If you would like to see the complete code before diving into the details, check bank.qnt. To follow along with the examples, download that file and save it as bank.qnt.

Declaring a Module

Quint specifications are organized in modules, and may consist of one or many top-level module declarations. Nested module declarations are currently not supported.

module bank {

In this lesson, we declare a single module. In general, we recommend starting with a single module and introducing multiple modules only if you are going to reuse various parts of your protocol.

Type Definitions

Similar to programming languages, it is common in Quint to declare type aliases for the types that appear often in the protocol description. A type alias is simply a declaration of the form type [name] = [tp], where [name] is a unique identifier that will be associated with the type, and [tp] is the type to be associated with the name, e.g., int or Set[int]. The Types lesson covers all available types in detail.

  // TYPE DEFINITIONS
 
  // account holders are identified by name
  type Account = str
 
  // The bank's ledger stores amounts of cents as unsigned 32-bit integers.
  // We declare UInt32 as an alias of Quint's int. Note that these UInt32
  // values are still integers, which can get arbitrarily large. Hence, we
  // have to take care of overflows ourselves.
  type UInt32 = int

Although it is convenient to declare type aliases, it is not mandatory. Protocol authors should decide together with their audience whether they prefer minimal type definitions, or an abundance of types. Quint replaces type aliases with the types on the right-hand sides of type. For example, it does not distinguish between different kinds of “integers” when they are referred to via different type aliases.

The Functional Layer

It often happens that a protocol requires auxiliary definitions that do not depend on the protocol state, but only on the values of their parameters. Such computations are often called “pure”. In the code below, we define two pure definitions:

  • The pure value MAX_UINT32.
  • The pure definition isUInt32 that computes whether a given integer i is within the range from 0 to MAX_UINT32 (inclusive).
  // FUNCTIONAL LAYER:
  // Values and functions that are state-independent
 
  // the maximal value the ledger can store for a single balance
  pure val MAX_UINT32 = 2^32 - 1
 
  // does a big integer represent an unsigned 32-bit integer?
  pure def isUInt32(i: int): bool = (0 <= i and i <= MAX_UINT32)

The main property of pure values is that they always return the same value. Pure definitions always return the same value, if they are supplied with the same arguments. To see that no state is needed, evaluate these definitions in the REPL (read-evaluate-print-loop):

quint -r bank.qnt::bank "MAX_UINT32"
quint -r bank.qnt::bank "isUInt32(22)"
quint -r bank.qnt::bank "isUInt32(-1)"
quint -r bank.qnt::bank "isUInt32(MAX_UINT32 + 1)"

The functional layer is actually quite powerful; a lot of protocol behavior can be defined here without referring to protocol state. This pattern of modelling bounded integers with predicates is explored in depth in the Numbers lesson.

As you can see, we have omitted the type of MAX_UINT32 but specified the type of isUInt32. Most of the time, the type checker can infer the types of values and operator definitions, and giving additional type annotations is up to you. In rare cases, the type checker may get confused, and then explicit type annotations will help you in figuring out the issue.

The State Machine

Protocol Parameters

In this section, we start to describe the protocol structure and behavior in terms of a state machine.

It often happens that protocols are parameterized in the sense that the protocol may be instantiated for different parameter values, and different instances still make sense. The typical parameters are:

  • the set of all possible accounts,
  • the account that performs a special role,
  • minimal and maximal values,
  • timeout values.
  // STATE MACHINE:
  // State-dependent definitions and actions
 
  // Currently, we fix the set of accounts to a small set of names.
  // In the future, we will be using the commented-out constant declaration.
  //const ACCOUNTS: Set[Account]
  pure val ACCOUNTS = Set("alice", "bob", "charlie", "dave", "eve")

For this purpose, Quint offers const declarations. You can see one of them in the commented-out section of the code above. You may be wondering what the difference is between const and pure val. They mean to express the same concept: a value that stays the same for all computations. However, they differ in the time when they are bound to a value:

  • The pure val values are immediately defined via an expression in the right-hand side.
  • The const values are first declared, and later they are substituted with actual values via an instance declaration.

At the moment, we simply declare the value for a small set of accounts ACCOUNTS, in order to be able to iterate on the protocol specification quickly.

State Variables

As a next step, we declare state variables, which together represent a state of the protocol:

  // the issuer's account name
  var issuer: Account
  // the balances of all accounts, in cents
  var balances: Account -> UInt32

In the above code, we introduce two such variables:

  • The variable issuer to store the name of the account holder who plays the issuer role. The type of this variable is Account.
  • The variable balances to store the balances of all accounts. The type of this variable is Account -> UInt32, which means a map from values of type Account to values of type UInt32.

Variable definitions always require a type. Otherwise, it may be too hard for the type checker to infer the types of the state variables.

If you think of how a bank implements its ledger, these two variables are conceptually similar to a configuration entry designating the issuer and a database table mapping every account to its balance.

Helper Definitions

It is often convenient to define a few helper operators. We start with the definition of state that represents the entire state as a record:

  // a handy definition to query the whole state in REPL at once
  val state = { issuer: issuer, balances: balances }

Notice that the definition of state is prefixed with val, not pure val. Since state accesses state variables, it is impure. You can try to evaluate the definition of state in REPL right away:

quint -r bank.qnt::bank "state"

If you tried that, you saw several error messages. The reason is that the state variables are not initialized by default. We would have to introduce an initialization action, which is usually called init. You will see how to do that shortly.

We introduce one more helper definition, computing the total amount of money in circulation:

  // compute the total money supply over all balances
  val totalSupply = ACCOUNTS.fold(0, (sum, a) => sum + balances.get(a))

The definition of totalSupply may look a bit complex if you have never seen similar code before. Let’s break it down into smaller pieces:

  • The definition of totalSupply defines a value, but not a pure one. Hence, even though totalSupply does not take any parameters, it implicitly depends on the state. As a result, totalSupply may evaluate to different values in different states, that is, in those states where the values of balances differ.

  • ACCOUNTS.fold(0, f) iterates over the set of accounts in some order and for every account a, it applies f(s, a) for the accumulator value s, which is initialized with 0. In our example, the operator f is defined as an anonymous lambda operator: (sum, a) => sum + balances.get(a). For our definition of ACCOUNTS, the computed value would be equal to:

      ((((0 + balances.get("alice")) + balances.get("bob")) + balances.get("charlie"))
    + balances.get("dave")) + balances.get("eve")

    Note that the order of the accounts in the brackets may be different from the one above. Hence, you should not rely on a particular order when using fold over sets. We are fine when using commutative operators such as + and *.

The Initializer

As you may have seen in the previous sections, the state variables issuer and balances are not initialized by default. In order to compute an initial state (there may be several!), we define a special action that we call an initializer. In our code, such an action is called init:

  // state initialization
  action init: bool = {
    // Our protocol does not fix who plays the issuer role: any account
    // holder could be appointed. Hence, we choose the issuer from the set
    // of all accounts non-deterministically.
    nondet chosenIssuer = oneOf(ACCOUNTS)
    all {
      issuer' = chosenIssuer,
      balances' = ACCOUNTS.mapBy(a => 0)
    }
  }

This definition is essential for describing the protocol. When you read somebody else’s protocol, it is one of the key parts to look at.

In an implementation, the identity of the issuer would come from some configuration that is out of our control. Quint does not have any built-in mechanism for reading configuration or user input. Instead, Quint offers a very powerful mechanism of non-deterministic choice. This is exactly what we do with the following line of code:

    nondet chosenIssuer = oneOf(ACCOUNTS)

This expression non-deterministically chooses one value from the set ACCOUNTS (assuming that the set is not empty) and binds this value to the name chosenIssuer. The qualifier nondet indicates that the value of chosenIssuer is special: the name chosenIssuer is bound to a fixed value, but it may evaluate to two different values when init is called twice or is called in different runs. This behavior may look complicated, but this is exactly what we expect from external input, too: the environment may supply different values, even if the protocol resides in two identical states. For more details, check oneOf  in the reference manual.

The rest of init is simple: the value of issuer is set to the value of chosenIssuer, and the value of balances is set to the map that maps all accounts from ACCOUNTS to value 0. Notice that the variables issuer and balances are not assigned their new values immediately; they are assigned once init is evaluated completely (and only if init evaluated to true).

Now we can call init and evaluate an initialized state in REPL:

quint -r bank.qnt::bank "init" "state"

Try calling init multiple times in REPL and evaluating state after each call. Did you get the same initial states every time, or were some states different?

Remember that we called init an initializer? This is because init only assigns new values to state variables, but does not read their previous values.

Issuing Money

Our first transition is the action issue, which puts newly created money on an account:

  // Deposits an amount of newly issued cents into the receiver's account.
  // Can only be done by the issuer.
  // Note that we have to add `sender` as an action parameter: in an
  // implementation, the caller identity would be implicit in the session.
  action issue(sender: Account, receiver: Account, amount: UInt32): bool = all {
    // only the issuer may create new money
    sender == issuer,
    val newBal = balances.get(receiver) + amount
    all {
      // the ledger stores balances as unsigned 32-bit integers,
      // so we have to make sure the new balance does not overflow
      isUInt32(newBal),
      // update the balances and keep the issuer
      balances' = balances.set(receiver, newBal),
      issuer' = issuer,
    }
  }

In contrast to init, we have decided to avoid non-deterministic choice in issue. Instead, we are passing the inputs as action parameters. You will see later that this makes debugging and testing easier.

If you understood how init works, the behavior of issue should be also easy to figure out. If you wonder what get and set are doing, here is the explanation:

  • balances.get(receiver) produces the value assigned to the key receiver in the map balances. If the key receiver has no value assigned in the map balances, REPL would show a runtime error. For more details, check get  in the reference manual.

  • balances.set(receiver, newBal) produces a new map that assigns the value of newBal to the key receiver, and keeps the other key-value pairs as in balances. For more details, check set  in the reference manual.

Now it’s time to issue some money in REPL! Try the following:

quint -r bank.qnt::bank 'init' 'issue(issuer, "bob", 2023)' 'state'

As you can see, the issuer can deposit 2023 cents into Bob’s account. Now try issuing MAX_UINT32 cents to Bob on top of that. Do you understand what happened in this case?

Transferring Money

If you understood the mechanics of the action issue, you should easily figure out the behavior of transfer:

  // Transfers an amount of cents from any account holder (sender)
  // to a receiver's account.
  action transfer(sender: Account, receiver: Account, amount: UInt32): bool = all {
    // the sender must have enough money on their balance
    not(amount > balances.get(sender)),
    if (sender == receiver) {
      balances' = balances
    } else {
      val newSenderBal = balances.get(sender) - amount
      val newReceiverBal = balances.get(receiver) + amount
      all {
        // again, we have to prevent the ledger from overflowing
        isUInt32(newSenderBal),
        isUInt32(newReceiverBal),
        balances' =
          balances
          .set(sender, newSenderBal)
          .set(receiver, newReceiverBal)
      }
    },
    // keep the issuer unchanged
    issuer' = issuer,
  }

Play with issue and transfer in REPL! The simplest scenario would be:

quint -r bank.qnt::bank 'init' 'issue(issuer, "bob", 2023)' 'transfer("bob", "eve", 1024)' 'state'

The Protocol Step

Finally, we can put together issue and transfer to describe every possible transition of the protocol! To this end, we non-deterministically choose the sender, the receiver, and the amount (from the set of integers from 0 to MAX_UINT32, inclusive):

  // All possible behaviors of the protocol in one action.
  action step: bool = {
    nondet sender = oneOf(ACCOUNTS)
    nondet receiver = oneOf(ACCOUNTS)
    nondet amount = 0.to(MAX_UINT32).oneOf()
    // execute one of the available actions
    any {
      issue(sender, receiver, amount),
      transfer(sender, receiver, amount),
    }
  }

The expression any { ... } executes one of its arguments; if both could be executed, one of them is executed non-deterministically.

Run the REPL, execute init once and execute step multiple times. Do you understand why some of the occurrences of step evaluate to false and some evaluate to true? It may help you if you print state after init and step.

We have defined the state variables, the initializer, and a step of the protocol. This is the minimal set of tasks for defining a working protocol. What we have achieved here is great! You can play with the protocol, feed it with different parameters in REPL, and experiment with your protocol.

Although you should definitely play with the protocol at this point, we urge you not to stop here! In the next sections, we show you the real magic of Quint.

Invariants and Temporal Properties

Having defined the protocol behavior with init and step, it is time to think about what we expect from the protocol. This is a good place for specifying protocol invariants and temporal properties.

The Most Basic Invariant

One of the most basic properties that we expect from the protocol is defined by the property balancesRangeInv:

  // INVARIANTS AND TEMPORAL PROPERTIES
 
  // One of the simplest properties is that all balances fit into the
  // unsigned 32-bit integers stored by the ledger. Our specification is
  // using big integers, so it makes sense to check the range.
  val balancesRangeInv: bool =
    ACCOUNTS.forall(a => isUInt32(balances.get(a)))

This property goes over all accounts in ACCOUNTS and tests whether the value stored in balances for every account is in the range from 0 to MAX_UINT32 (inclusive). We can immediately check this invariant for a few states:

quint -r bank.qnt::bank 'init' 'balancesRangeInv' 'issue(issuer, "bob", 2023)' 'balancesRangeInv' 'transfer("bob", "eve", 1024)' 'balancesRangeInv'

Properties like balancesRangeInv are called invariants, because we expect them to hold in every state that could be produced by init and a number of step actions. Intuitively, whatever happens, the property should hold true.

It is important to distinguish between the properties that we would like to be invariants and the properties that we have proven to be invariants. To be precise, the former properties are called invariant candidates, whereas the latter are actually called invariants.

The Total Supply Invariant

Another basic invariant that we intuitively expect to hold is defined in totalSupplyDoesNotOverflowInv:

  // It is desirable that the total money supply fits into UInt32.
  // Otherwise, the bank's software or the user interface may run into
  // an unexpected overflow when adding up the balances.
  val totalSupplyDoesNotOverflowInv: bool = {
    isUInt32(totalSupply)
  }

It is so simple that it should hold true, right? If we have your attention now, read further!

Temporal Properties

After we have defined state invariants, we should normally think about temporal properties in general, such as safety and liveness:

  // The temporal property that says the following:
  // Assume that we want to check the temporal property `NoSupplyOverflow`
  // for every initial state. Then we have to check for every initial state
  // that it never produces a computation that ends in a state violating
  // `totalSupplyDoesNotOverflowInv`. In general, temporal properties may be
  // checked against any kinds of states, not only initial ones.
  temporal NoSupplyOverflow: bool = always(totalSupplyDoesNotOverflowInv)

However, temporal properties are an advanced topic, and financial ledgers are typically focused on safety. Thus, it is safe to skip this topic for now. It is just important to know that temporal properties are labelled with the qualifier temporal.

Tests

So far, we have been running sequences of actions in REPL, to get a basic understanding of the protocol mechanics. While REPL is capable of replaying actions one-by-one, it would be more convenient to run something similar to unit tests or integration tests, which are ubiquitous in programming languages.

We normally add tests at the very bottom of the protocol module, or in a separate module.

Expecting a Failure

Quint introduces runs to express “happy paths” and tests. The code below shows a simple test transferBeforeIssueTest:

  // TESTS
 
  // transfer should not work before any money is issued
  run transferBeforeIssueTest = {
    init.then(transfer(issuer, "bob", 5))
        .fail()
  }

In this test, the action init runs first. If it evaluates to true, then the action transfer(...) is run. Since this action is composed with fail(), the action transfer(...) is expected to evaluate to false.

Go ahead and see if this test goes through:

quint -r bank.qnt::bank 'transferBeforeIssueTest'

Actually, if you look carefully at the code of transfer, you can find one value for amount that makes transfer work even before any money was issued. Can you see what this value is?

A Single Data Point Test

We can write longer tests that are similar to unit/integration tests in normal programming languages. For instance, the test issueThenTransferTest makes sure that the exact sequence of issue and transfer transactions goes through and the resulting balances have the expected values:

  // `issue`, then `transfer`
  run issueThenTransferTest = {
    init.then(issue(issuer, "bob", 10))
        .then(transfer("bob", "eve", 4))
        .then(all {
          assert(balances.get("bob") == 6),
          assert(balances.get("eve") == 4),
          issuer' = issuer,
          balances' = balances,
        })
  }
quint -r bank.qnt::bank 'issueThenTransferTest'

Try changing some numbers in the test, run it again in REPL and observe what happens.

Although it is better to have a test like issueThenTransferTest than no test at all, issueThenTransferTest is testing only one data point. We can do better in Quint.

Testing with Non-deterministic Inputs

Instead of testing a sequence of transactions for a carefully crafted single input, we could fix a sequence of transactions and let the computer find the inputs that fail the test. This is exactly what we are doing in the test issueTwiceThenTransferError:

  // Issue some money for Eve and Bob.
  // Test that Eve can always transfer money to Bob,
  // if she has enough on her balance.
  // This test may fail sometimes. Do you see why?
  // If not, execute it multiple times in REPL, until it fails.
  run issueTwiceThenTransferError = {
    // non-deterministically pick some amounts to issue and transfer
    nondet issueEve = 0.to(MAX_UINT32).oneOf()
    nondet issueBob = 0.to(MAX_UINT32).oneOf()
    nondet eveToBob = 0.to(MAX_UINT32).oneOf()
    // execute a fixed sequence `init`, `issue`, `issue`, `transfer`
    init.then(issue(issuer, "eve", issueEve))
        .then(issue(issuer, "bob", issueBob))
        .then(
          if (eveToBob <= balances.get("eve")) {
            // if Eve has enough money, transfer to Bob should pass
            transfer("eve", "bob", eveToBob)
          } else {
            // otherwise, just ignore the test
            all { issuer' = issuer, balances' = balances }
          }
        )
  }

The test non-deterministically chooses the amounts of money to issue and transfer and then executes the actions issue, issue, and transfer. As the values are chosen non-deterministically, we know that some of the inputs should fail transfer. Our hypothesis is that transfer should never fail when Eve has enough money on her account. If she does not, we simply ignore this choice of inputs in the else-branch.

Let’s run this test:

quint -r bank.qnt::bank 'issueTwiceThenTransferError'

If you are lucky, it fails right away. If it does not fail, run it multiple times, until it fails. To see why it failed, evaluate state after executing the test. Do you understand why our hypothesis was wrong?

If you carefully look at issueTwiceThenTransferError, you will see that it is still a single data point test, though the data point (the inputs) is chosen non-deterministically every time we run the test. In fact, REPL implements non-determinism via random choice.

If you do not want to sit the whole day and run the test, you could integrate it into continuous integration, so it runs from time to time for different inputs. Quint comes with the command test that is designed for exactly this purpose. Try the command below. Most likely, it would find a violation after just a few tests:

quint test --match issueTwiceThenTransferError bank.qnt

Also, we had to fix the sequence of actions in our test. We can do better with Quint.

With the tests in place, our specification is complete, and we can close the module we declared at the very beginning:

}

Finding Violations with the Simulator

It is often hard to find a good sequence of actions that breaks an invariant. Similar to how we let the computer find the right inputs, we can use the computing power to look for bad sequences of actions. Quint comes with a random simulator that does exactly that. You can try it right away:

quint run --invariant totalSupplyDoesNotOverflowInv bank.qnt

The above command randomly produces sequences of steps, starting with init and continuing with step. It checks the invariant totalSupplyDoesNotOverflowInv after every step. If the invariant is violated, the random search stops and reports the violating execution. If no invariant violation is found, the search finishes after enumerating the specified number of runs. The search parameters, such as the number of runs and steps, can be tuned. Check the options of run:

quint run --help

Does Random Search Always Find Bugs?

To be honest, our example is relatively simple, and we were quite lucky that the invariant totalSupplyDoesNotOverflowInv was often violated by a completely random search. For more complex protocols, random search often gets stuck while looking for non-interesting inputs or sequences of actions. Hence, if you have a hunch about where an error could potentially be, you could restrict the scope of the search by:

  • Restricting the scope of non-deterministic choices, e.g., by making every set in oneOf(S) smaller.
  • Restricting the choice of actions, e.g., by removing non-essential actions from step.

Although the above tricks may help you in detecting some bugs, it is well known that there is always a probability of missing a bug with random search. If you are looking for better guarantees of correctness, use quint verify, which runs a model checker instead of a random simulation. Model checkers look for counterexamples exhaustively, so if they don’t find a bug, you get a guarantee that there is none (up to a bounded number of steps, when using the Apalache). Quint supports two model checkers:

  • TLC  (quint verify --backend=tlc) enumerates all reachable states one by one and checks the invariant on each of them. This is the easiest strategy to understand: it is like the random simulator, except that it systematically tries every possibility instead of sampling some of them.
  • Apalache  (the default for quint verify) covers the state space symbolically, by translating the specification into equations and handing them to a solver. This lets it handle state spaces that would be too large to enumerate, at the cost of being subject to the complexity of solving the equations.

See the Model Checkers documentation for a deeper comparison and guidance on when to reach for each.

Summing it up

This was a long lesson. We have specified the whole protocol, experimented with it, wrote several tests and even found some surprising behavior of this protocol. Along the way, we saw the standard anatomy of a Quint specification: type definitions first, then a functional layer of pure definitions, and finally the state machine with its parameters, state variables, actions, invariants and tests. We hope that by going through this lesson you have got an idea of how you could specify your own protocol in Quint and make Quint useful for solving your problems with protocols!

Although our running example was a bank ledger, there is not much special about banking in this specification. The same structure (a privileged role, a resource that is created and moved around, and bounded machine integers that can overflow) appears in all kinds of systems, from payment processors to token contracts to inventory management.

Last updated on
ListsWhat is Choreo?