Skip to Content
PostsUnderstanding Solana's Alpenglow with Quint

Understanding Solana’s Alpenglow with Quint

• Written by: Josef Widder and Gabriela Moreira

If you are interested in understanding the next Solana consensus algorithm, this is for you. We are not going to explain the algorithm to you, but will show you an efficient way how you can figure it out for yourself using the Quint toolset to interact with the specification.

Recently, Anza research shared the exciting news  that they propose Alpenglow consensus as a replacement for Solana’s current consensus engine. As we at Informal Systems are currently working on a library that aims at speeding up specifying protocols for distributed systems, we are implementing several consensus engines to collect benchmarks, and define rules on how to specify distributed protocols for different needs (checking the protocol vs. checking the code).

While this is useful for our research, we believe the Alpenglow Quint specification will be a great tool for you to deep dive into Alpenglow.


Check out the spec

Doing is better than reading

Contrary to our natural perception, struggling to find answers makes us learn much more than reading or listening to other people’s experience. This post gives you the opportunity to be hands-on (but we’ll also give you the outputs in case you prefer just reading).

For the hands-on experience, you’ll need:

Alpenglow’s components

Alpenglow is separated into several components:

  • Block Propagation (Rotor)
  • Voting (Votor)
    • Pool
    • Consensus logic

We focus on Votor in this post. The Alpenglow paper describes a modular architecture: The Pool component collects messages, does bookkeeping, and generates events as input to the consensus logic, which we call consensus inputs. These consensus inputs are e.g., “I have received a quorum of votes” or “I have received a quorum of skip messages”. The consensus logic then reacts to these by generating consensus outputs, such as broadcasting messages or starting timeouts. (We have a very similar architecture for our own Malachite consensus engine, where the driver uses the vote keeper to collect messages and sends consensus inputs to the consensus state machine. Our Quint spec of Malachite can be found here ).

We have specified:

  • The consensus logic in a very detailed way. The spec is close to the paper, and potentially quite similar to the implementation.
  • The pool quite abstractly. The state machine we defined with Quint doesn’t make a transition for each single message it receives, counting them locally until there is some quorum. Rather, we model conditions on the messages globally sent that are required for consensus inputs to occur.

We are going into a deep dive into this soon, when we publish the first version of our library mentioned in the beginning. But observe that, in a distributed protocol, the received messages that you store locally, are the node’s imperfect perception of the messages sent to the node by others in the system.

  • The Rotor not at all. We were interested in the novel voting mechanism that enables fast finalization. This can be studied by just having blocks preloaded in the simulation environment and allowing the Block consensus input to occur at any time.

Interacting with the specification

Quint is a toolset that helps designing and understanding protocols. The REPL allows you to interact with the specification. So let’s go: We have modeled the voting mechanism in a parameterized way, and have already set up an instance called some_byz with 5 correct validators, and 1 Byzantine one. You can start the Quint REPL requiring the statemachine.qnt model and loading the some_byz instance in one single command:

quint -r statemachine.qnt::some_byz

You can then check that the validators are here as promised:

Quint REPL 0.25.1
Type ".exit" to exit, or ".help" for more information
>>> correct
 
Set("v1", "v2", "v3", "v4", "v5")
>>> byzantine
 
Set("b1")

This instance also preloads a few blocks for us to use:

>>> allBlocks
 
Set(
  { hash: 42, parent: -1, slot: 0 },
  { hash: 43, parent: 42, slot: 1 },
  { hash: 44, parent: 43, slot: 2 },
  { hash: 46, parent: 42, slot: 1 },
  { hash: 47, parent: 45, slot: 1 },
  { hash: 48, parent: 43, slot: 2 },
  { hash: 49, parent: 45, slot: 2 }
)

Now, let’s try to call init to initialize the global state of the system (called s to save us all some keystrokes), and then inspect it:

>>> init
 
true
>>> s
 
{
  activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0), "v4" -> Set(0), "v5" -> Set(0)),
  msgBuffer: Set(),
  system:
    Map(
      "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
      "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
      "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
      "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
      "v5" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] }
    )
}

Moving the state machine

Alright, enough viewing. Let’s now control the system and let validator v1 receive a block (one of the blocks we have already preloaded in the model, that we could observe with allBlocks):

>>> receiveSpecificBlock("v1", { hash: 42, parent: -1, slot: 0 })
 
true

As a result, we see that, v1 sends a notar vote message:

>>> s
 
{
  activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0), "v4" -> Set(0), "v5" -> Set(0)),
  msgBuffer: Set({ msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v1" }),
  system:
    Map(
      "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()] },
      "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
      "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
      "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
      "v5" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] }
    )
}

We can also call s.msgBuffer to inspect only this part of the state. The state is simply a record:

>>> s.msgBuffer
 
Set({ msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v1" })

Fast Finalization

fastFinalized(0, s.msgBuffer) checks whether enough messages are sent such that processes can fast finalize. That doesn’t seem to be the case. Try and let all other honest validators ("v2", "v3", "v4" and "v5") also receive the block and check again.

Here are the results if you don’t want to try it yourself

>>> receiveSpecificBlock("v1", { hash: 42, parent: -1, slot: 0 })
 
true
>>> fastFinalized(0, allMessages)
 
Set()
>>> receiveSpecificBlock("v2", { hash: 42, parent: -1, slot: 0 })
 
true
>>> receiveSpecificBlock("v3", { hash: 42, parent: -1, slot: 0 })
 
true
>>> receiveSpecificBlock("v4", { hash: 42, parent: -1, slot: 0 })
 
true
>>> receiveSpecificBlock("v5", { hash: 42, parent: -1, slot: 0 })
 
true
>>> fastFinalized(0, s.msgBuffer)
 
Set(42)

There are four more actions:

  • blockNotarizedAction(v, slot),
  • parentReadyAction(v, slot),
  • safeToNotarAction(v, slot),
  • safeToSkipAction(v, slot),

These actions will check whether a consensus input is enabled based on the messages in the message buffer. If this is the case, they will execute consensus with the input. For instance, the consensus input BlockNotarizedInput needs 60% of the voting power to have sent a notar vote for a slot and a block. If you managed above to get fastFinalized(0, s.msgBuffer) evaluate to true, you can call blockNotarizedAction("v3", 0) in this state and see that "v3" has learned that the block has been notarized.

Here are the results if you don’t want to try it yourself

>>> blockNotarizedAction("v3", 0)
 
true
>>> s
 
{
  activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0), "v4" -> Set(0), "v5" -> Set(0)),
  msgBuffer:
    Set(
      { msg: FinalVoteMsg(0), sender: "v3" },
      { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v1" },
      { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v2" },
      { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v3" },
      { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v4" },
      { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v5" }
    ),
  system:
    Map(
      "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()] },
      "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()] },
      "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(BlockNotarized(42), ItsOver, ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()] },
      "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()] },
      "v5" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()] }
    )
}

Timeouts

Receiving blocks or messages is just one functionality of the Votor. Handling timeouts is another. Let’s reset the system with init, and see what happens when v2’s timeout for slot 0 expires:

Controlling timeouts is usually hard and prone to a lot of interference, but we avoid all of that thanks to being in a more abstract environment. A timeout is just something that can non-deterministically expire, and we can control at which point of the state machine evolution that happens when using the REPL.

Quint REPL 0.25.1
Type ".exit" to exit, or ".help" for more information
>>> init
 
true
>>> s
 
{
  activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0), "v4" -> Set(0), "v5" -> Set(0)),
  msgBuffer: Set(),
  system:
    Map(
      "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
      "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
      "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
      "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
      "v5" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] }
    )
}
>>> fireTimeoutEvent("v2", 0)
 
true
>>> s
 
{
  activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(), "v3" -> Set(0), "v4" -> Set(0), "v5" -> Set(0)),
  msgBuffer:
    Set(
      { msg: SkipVoteMsg(0), sender: "v2" },
      { msg: SkipVoteMsg(1), sender: "v2" },
      { msg: SkipVoteMsg(2), sender: "v2" },
      { msg: SkipVoteMsg(3), sender: "v2" }
    ),
  system:
    Map(
      "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
      "v2" ->
        {
          pendingBlocks: [None, None, None, None, None],
          state:
            [Set(BadWindow, ParentReady(-1), Voted), Set(BadWindow, Voted), Set(BadWindow, Voted), Set(BadWindow, Voted), Set()]
        },
      "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
      "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
      "v5" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] }
    )
}
>>>

We see that the effect is much bigger. Rather than timing out on Slot 0, and sending a skip message just for that slot, validator "v2" sent skip messages for slots 0..3. Actually what happens here is that v2 gives up on the proposer and thus sends skip messages for the whole proposer window consisting of slots 0..3.

With these actions you now can unroll the protocol step-by-step and investigate different scenarios of interest.

Understanding Disagreement

To understand why and how a protocol works, it is useful to understand when it doesn’t work. For instance, the too_many_byz model defines a setting in which there are more faults than the protocol is designed for (more than a fifth of the voting power). In the model we have already sent a couple of messages and blocks that Byzantine nodes may send. You can investigate them as follows:

quint -r statemachine.qnt::too_many_byz
Quint REPL 0.25.1
Type ".exit" to exit, or ".help" for more information
>>> correct
 
Set("v1", "v2", "v3", "v4")
>>> byzantine
 
Set("b1", "b2")
>>> init
 
true
>>> allMessages
 
Set(
  { msg: FinalVoteMsg(0), sender: "b1" },
  { msg: FinalVoteMsg(0), sender: "b2" },
  { msg: NotarFallBackVoteMsg({ hash: 41, slot: 0 }), sender: "b1" },
  { msg: NotarFallBackVoteMsg({ hash: 41, slot: 0 }), sender: "b2" },
  { msg: NotarFallBackVoteMsg({ hash: 42, slot: 0 }), sender: "b1" },
  { msg: NotarFallBackVoteMsg({ hash: 42, slot: 0 }), sender: "b2" },
  { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "b1" },
  { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "b2" },
  { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "b1" },
  { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "b2" },
  { msg: SkipFallbackVoteMsg(0), sender: "b1" },
  { msg: SkipFallbackVoteMsg(0), sender: "b2" },
  { msg: SkipVoteMsg(0), sender: "b1" },
  { msg: SkipVoteMsg(0), sender: "b2" }
)
>>> allBlocks
 
Set({ hash: 41, parent: -1, slot: 0 }, { hash: 42, parent: -1, slot: 0 })

You can now try to use the REPL and the actions we introduce above to construct an execution where processes receive such Byzantine messages and messages sent by correct processes so that two conflicting blocks are finalized. You can check that by evaluating the agreement property in a global state. It evaluates to false in a state with at least conflicting finalized blocks. The precise definitions of “agreement” and “finalized” are not so complicated. You can look them up in the statemachine.qnt  file.

Did you succeed? Was it easy? There is an easier way of doing it!

Using Quint to find out how disagreement happens

quint run statemachine.qnt --main too_many_byz --invariant agreement

This does random simulation, and it typically finds and prints an execution trace that ends in a state where agreement is violated. If you are unlucky, try again, if you are still unlucky then run

quint run statemachine.qnt --main too_many_byz --invariant agreement --seed=0x184321e08ff45d

See results

 
[State 0]
{
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 0,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0), "v4" -> Set(0)),
      msgBuffer: Set(),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 1]
{
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 1,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0), "v4" -> Set(0)),
      msgBuffer: Set({ msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" }),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v3" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()]
            },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 2]
{
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 2,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0), "v4" -> Set(0)),
      msgBuffer:
        Set(
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" }
        ),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v3" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()]
            },
          "v4" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()]
            }
        )
    }
}
 
[State 3]
{
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 3,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0), "v4" -> Set(0)),
      msgBuffer:
        Set(
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" }
        ),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v3" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()]
            },
          "v4" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()]
            }
        )
    }
}
 
[State 4]
{
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 4,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0, 1, 2, 3), "v4" -> Set(0)),
      msgBuffer:
        Set(
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" }
        ),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v3" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(ParentReady(-1), ParentReady(41), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()]
            },
          "v4" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()]
            }
        )
    }
}
 
[State 5]
{
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 5,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0, 1, 2, 3), "v4" -> Set(0)),
      msgBuffer:
        Set(
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" },
          { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v2" }
        ),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()]
            },
          "v3" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(ParentReady(-1), ParentReady(41), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()]
            },
          "v4" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()]
            }
        )
    }
}
 
[State 6]
{
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 6,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0, 1, 2, 3), "v4" -> Set(0)),
      msgBuffer:
        Set(
          { msg: FinalVoteMsg(0), sender: "v3" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" },
          { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v2" }
        ),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()]
            },
          "v3" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state:
                [
                  Set(BlockNotarized(41), ItsOver, ParentReady(-1), ParentReady(41), Voted, VotedNotar(41)),
                  Set(),
                  Set(),
                  Set(),
                  Set()
                ]
            },
          "v4" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()]
            }
        )
    }
}
 
[State 7]
{
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 7,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0, 1, 2, 3), "v4" -> Set(0)),
      msgBuffer:
        Set(
          { msg: FinalVoteMsg(0), sender: "v3" },
          { msg: FinalVoteMsg(0), sender: "v4" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" },
          { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v2" }
        ),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()]
            },
          "v3" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state:
                [
                  Set(BlockNotarized(41), ItsOver, ParentReady(-1), ParentReady(41), Voted, VotedNotar(41)),
                  Set(),
                  Set(),
                  Set(),
                  Set()
                ]
            },
          "v4" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(BlockNotarized(41), ItsOver, ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()]
            }
        )
    }
}
 
[State 8]
{
  too_many_byz::consensus::ch: Map(0 -> Set(41)),
  too_many_byz::consensus::counter: 8,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0, 1, 2, 3), "v4" -> Set(0)),
      msgBuffer:
        Set(
          { msg: FinalVoteMsg(0), sender: "v3" },
          { msg: FinalVoteMsg(0), sender: "v4" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" },
          { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v1" },
          { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v2" }
        ),
      system:
        Map(
          "v1" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()]
            },
          "v2" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()]
            },
          "v3" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state:
                [
                  Set(BlockNotarized(41), ItsOver, ParentReady(-1), ParentReady(41), Voted, VotedNotar(41)),
                  Set(),
                  Set(),
                  Set(),
                  Set()
                ]
            },
          "v4" ->
            {
              pendingBlocks: [None, None, None, None, None],
              state: [Set(BlockNotarized(41), ItsOver, ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()]
            }
        )
    }
}
 
[violation] Found an issue (37ms at 27 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0x184321e08ff45d to reproduce.
error: Invariant violated

The trace you get is a sequence of global states that, in state 8, violated agreement. It might be hard to see what happened between any two states. To get that information run

quint run statemachine.qnt --main too_many_byz --invariant agreement --seed=0x184321e08ff45d --mbt

Don’t worry about what mbt means! If you still worry, go here.

See results

An example execution:
 
[State 0]
{
  mbt::actionTaken: "init",
  mbt::nondetPicks: { b: None, block: None, slot: None, v: None },
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 0,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0), "v4" -> Set(0)),
      msgBuffer: Set(),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 1]
{
  mbt::actionTaken: "receiveBlock",
  mbt::nondetPicks: { b: None, block: Some({ hash: 41, parent: -1, slot: 0 }), slot: Some(0), v: Some("v3") },
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 1,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0), "v4" -> Set(0)),
      msgBuffer: Set({ msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" }),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 2]
{
  mbt::actionTaken: "receiveBlock",
  mbt::nondetPicks: { b: None, block: Some({ hash: 41, parent: -1, slot: 0 }), slot: Some(0), v: Some("v4") },
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 2,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0), "v4" -> Set(0)),
      msgBuffer: Set({ msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" }, { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" }),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 3]
{
  mbt::actionTaken: "receiveBlock",
  mbt::nondetPicks: { b: None, block: Some({ hash: 41, parent: -1, slot: 0 }), slot: Some(0), v: Some("v4") },
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 3,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0), "v4" -> Set(0)),
      msgBuffer: Set({ msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" }, { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" }),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 4]
{
  mbt::actionTaken: "parentReadyAction",
  mbt::nondetPicks: { b: Some({ hash: 41, parent: -1, slot: 0 }), block: None, slot: Some(0), v: Some("v3") },
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 4,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0, 1, 2, 3), "v4" -> Set(0)),
      msgBuffer: Set({ msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" }, { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" }),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), ParentReady(41), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 5]
{
  mbt::actionTaken: "receiveBlock",
  mbt::nondetPicks: { b: None, block: Some({ hash: 42, parent: -1, slot: 0 }), slot: Some(0), v: Some("v2") },
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 5,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0, 1, 2, 3), "v4" -> Set(0)),
      msgBuffer: Set({ msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" }, { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" }, { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v2" }),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), ParentReady(41), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 6]
{
  mbt::actionTaken: "blockNotarizedAction",
  mbt::nondetPicks: { b: Some({ hash: 41, parent: -1, slot: 0 }), block: None, slot: Some(0), v: Some("v3") },
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 6,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0, 1, 2, 3), "v4" -> Set(0)),
      msgBuffer:
        Set(
          { msg: FinalVoteMsg(0), sender: "v3" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" },
          { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v2" }
        ),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(BlockNotarized(41), ItsOver, ParentReady(-1), ParentReady(41), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 7]
{
  mbt::actionTaken: "blockNotarizedAction",
  mbt::nondetPicks: { b: Some({ hash: 41, parent: -1, slot: 0 }), block: None, slot: Some(0), v: Some("v4") },
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 7,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0, 1, 2, 3), "v4" -> Set(0)),
      msgBuffer:
        Set(
          { msg: FinalVoteMsg(0), sender: "v3" },
          { msg: FinalVoteMsg(0), sender: "v4" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" },
          { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v2" }
        ),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(BlockNotarized(41), ItsOver, ParentReady(-1), ParentReady(41), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(BlockNotarized(41), ItsOver, ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 8]
{
  mbt::actionTaken: "receiveBlock",
  mbt::nondetPicks: { b: None, block: Some({ hash: 42, parent: -1, slot: 0 }), slot: Some(0), v: Some("v1") },
  too_many_byz::consensus::ch: Map(0 -> Set(41)),
  too_many_byz::consensus::counter: 8,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0, 1, 2, 3), "v4" -> Set(0)),
      msgBuffer:
        Set(
          { msg: FinalVoteMsg(0), sender: "v3" },
          { msg: FinalVoteMsg(0), sender: "v4" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" },
          { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v1" },
          { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v2" }
        ),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(BlockNotarized(41), ItsOver, ParentReady(-1), ParentReady(41), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(BlockNotarized(41), ItsOver, ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[violation] Found an issue (35ms at 29 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0x184321e08ff45d to reproduce.
error: Invariant violated

This last command lets you derive a sequence of actions that takes the system from the initial state to an interesting state. It gives you the actions (mbt::actionTaken) and the non-deterministic choices (mbt::nondetPicks) that will inform which validator receives what block/message (which is chosen non-deterministically at each step). You will see there are some repeating actions. In our example, States 2 and 3 are the result of validator "v3" receiving the same block twice. Our models allow this at the moment. If you want more precision, you could restrict the actions in the model as an exercise.

Documenting the disagreement scenario

You can now extract the useful actions to arrive at the following run (we added some expect statements to check the global state).

run disagreementExampleTest =
  init
  .then(receiveSpecificBlock("v3", { hash: 41, parent: -1, slot: 0 }))
  .then(receiveSpecificBlock("v4", { hash: 41, parent: -1, slot: 0 }))
  .expect(
    s.msgBuffer == Set(
      { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" },
      { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" },
    ))
  .then(receiveSpecificBlock("v2", { hash: 42, parent: -1, slot: 0 }))
  .then(blockNotarizedAction("v3", 0))
  .then(blockNotarizedAction("v4", 0))
  .expect(
    Set(
      { msg: FinalVoteMsg(0), sender: "v3" },
      { msg: FinalVoteMsg(0), sender: "v4" },
    ).subseteq(s.msgBuffer))
  .then(receiveSpecificBlock("v1", { hash: 42, parent: -1, slot: 0 }))
  .expect(not(agreement))
  .expect(
    Set(
      { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" },
      { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" },
      { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "b1" },
      { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "b2" },
      { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v1" },
      { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v2" },
      { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "b1" },
      { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "b2" },
      { msg: FinalVoteMsg(0), sender: "v3" },
      { msg: FinalVoteMsg(0), sender: "v4" },
      { msg: FinalVoteMsg(0), sender: "b1" },
      { msg: FinalVoteMsg(0), sender: "b2" },
    ).subseteq(allMessages))

We see that, at first, validators v4 and v3 receive a block with hash 41 (and then their NotarVote messages are in-flight), and then validator v2 receives a conflicting block with hash 42. Because there are many messages from Byzantine nodes flying around, v3 and v4 then actually observe that slot 0 can be notarized (and their FinalVote messages are in-flight after that). Then v1 also receives the conflicting block, and now agreement is violated as there are also many final vote messages from Byzantine processes in the system.

Runs as the modern version of diagrams

For me, this run is like a space/time diagram that I would draw on a whiteboard to explain our protocol ideas or scenarios. For instance, the picture is taken from the whiteboard on our office. It shows a space time diagram where there is one line per process (from bottom to top: v1, v2, b1, b2, v3, v4), time moves from left to right, arrows between lines depict message transfers, and at the beginning and end of arrows we have send and receive events. Green lines are final vote messages. Red lines are blocks and notar vote messages (I only have two whiteboard markers at the moment):

Whiteboard with a space/time diagram

The Quint run is like this drawing but saved within a file in the repository as an executable artifact. Indeed, you can call disagreementExampleTest from within the REPL, which will execute the run. You will now be in the final state of this run, and you can use s to explore it.

From the command line (outside of the REPL), you can also call quint test statemachine.qnt that will execute the test and show the result. You can use quint test in CI within Github to make sure that changing the specification didn’t introduce weird behaviors.

So, Quint runs are executable whiteboard drawings! You can use the run above to explain to your friends why Alpenglow needs more than ⅘ of correct voting power!

So we promised to give you a guide to understand Alpenglow. Now you are even at a position where you can explain it to your friends 😉 have fun!

Writing specs is easier than you think

If you think you don’t have time to set up something like this for your protocol, think again! The full Quint specification for Alpenglow’s Votor, including properties and runs, is less than 1 KLOC, and could be derived pretty directly from the (very well written) paper  - take a look . There are several resources to learn how to write specifications like this - you can start here.

If you liked this post, you might also like Understanding Mysticeti Consensus with Quint .


Last updated on
Holiday protocols: Secret Santa with Quint 🎅