test(mbt): Introduce Quint specs for Emerald #183

erickpintor · 2026-01-19T19:16:57Z

This patch introduces Quint specifications that model Emerald's behavior wrt. Malachite consensus inputs. These specs is based on the app.rs message handlers and will be used for MBT later.

bugarela

LGTM, just some minor comments!

specs/emerald.qnt

specs/emerald_tests.qnt

mpoke

Partial review. See my comments below.

mpoke · 2026-01-21T10:45:18Z

specs/emerald.qnt

+  // For simplicity, we generate payloads as sequential numbers based on how
+  // many pending proposals there are, thus ensuring a unique payload per
+  // proposal recorded.


Does this mean that decided proposal might have the same sequence number? Or are pending proposals all the proposals ever seen?

The later. We record any proposal in pending first, when they become decided they move to the decided_proposals set but they don't ever leave the pending set. Would renaming the pending set to all_proposals help?

I think it would help renaming to all_proposal. Thanks.

Pending proposals should be cleaned every time we have a decided proposal for a height. Will check the code again.

There seems to be a window of retained blocks:

emerald/app/src/state.rs

Lines 599 to 608 in 8315822

// This will compute the retain heigth for the certificates which is based on the

// retain height set in the config.

// The intermediary block data stored for Consensus is pruned at every height after

// VALUE_RETAIN_HEIGHT (defined in store.rs)

let retain_height = Height::new(

certificate

.height

.as_u64()

.saturating_sub(self.max_retain_blocks),

);

Right now the window is larger than any MBT test trace:

emerald/scripts/generate_testnet_config.sh

Line 251 in 8315822

echo "max_retain_blocks = 10064" >> "$TESTNET_DIR/config/$i/config.toml"

BTW: I've renamed pending_proposals to all_proposals.

So the retain_height has a twofold meaning. We have. height at which we delete also the certificates so those blocks are lost forever. And then there is also the fact that we (Emerald) also stores the last X blocks but as those are in the execution layer we delete them more aggressively than the certificates.

set but they don't ever leave the pending set.

Here is where the proposal parts get removed. And then when we c all prune on the database we delete also all data below the retain_height on UNDECIDED_PROPOSALS_TABLE , UNDECIDED_BLOCK_DATA_TABLE , PENDING_PROPOSAL_PARTS_TABLE , DECIDED_VALUES_TABLE ,DECIDED_BLOCK_DATA_TABLE .

This actually runs on every block (it keeps the last 10 heights). I am not sure how fast/slow this is and maybe it should run only at every 10 blocks rather than at every height.

specs/emerald.qnt

specs/emerald_types.qnt

specs/emerald.qnt

mpoke · 2026-01-21T14:21:25Z

specs/emerald.qnt

+        // Start next height by moving back to the ready phase, which enables
+        // the handle_started_round transition.
+        phase: Ready,
+        start_height: decided.height + 1,


Why is the start_height updated here? What is start_height used for?

This is tricky.

Initially I had handle_started_round always start from the current_height. So when we decide on a proposal, I'd increment the node's current height and move its phase back to Ready to start the next height. Similarly, when initializing a node from a genesis start, I'd set the current height to 1 and move it to the Ready phase to start the first height.

However, after introducing failures to the model, I've noticed that during a non-genesis start the current height set to the last decided height, but the node is supposed to start the next height instead of the current one.

At that point I had to split what's the current height from what's the height the node is supposed to start and that's when I introduced the start_height field.

No that I think about it, I could drop the start_height if I add some logic at the handle_started_round to handle the non-geneiss start case. I'll give that a try and see if it simplifies the model.

I think this might be a problem in the code. cc @jmalicevic

start_height is the next height we need to reach consensus on. That's why Emerald passes it to Malachite.

current_height is the current height of Emerald. This is set on AppMsg::StartedRound. There shouldn't be a difference between a restart or a genesis start.

That is exactly what is happening. Now, on genesis , current height is the same as start height because they are both 1.

On AppMsg::ConsensusReady , if we have a height stored in the store, this is the current_height and then the start height is current_height.incremnet() (see here). On AppMsg::StartedRound we then set the current_height to be whatever we are deciding on now.

But then we should have current_height set to zero on genesis start. To keep it consistent. Right?

I'll defer to you guys on the decision about the current_height initial value. Just FYI: I've removed the start_height field to simplify the state and moved the genesis vs non-genesis start logic at the listen_started_round function.

BTW: we could also keep the model as is since it matches the current code and once we change the code the MBT tests will break, signaling that we need to adapt the model.

We updated the code. See #195
There is no longer a start_height in the code.
@erickpintor please make the spec consistent.

specs/emerald.qnt

This patch introduces Quint specifications that model Emerald's behavior wrt. Malachite consensus inputs. These specs is based on the `app.rs` message handlers and will be used for MBT later.

mpoke · 2026-01-23T10:41:17Z

specs/emerald.qnt

+        // value. Current height begins in 1.
+        {
+          ...s,
+          current_height: 1,


Set to 0. It will be incremented on receiving start_round.

mpoke · 2026-01-23T10:43:58Z

specs/emerald.qnt

+        s.current_height
+
+    if (timeout != None)       Set((s.current_height, s.current_round + 1))
+    else if (s.phase == Ready) Set((start_height, s.current_round))


In this case, start_height should always be current_height + 1.

Is there a scenario here where the round is not zero?

mpoke · 2026-01-23T11:05:00Z

specs/emerald.qnt

+        | Some(p) =>
+            if (and {
+              p.in(s.proposals),
+              p.height > s.last_decided_height,


Is this check needed or it's more of a sanity check? I would assume the invariant is that if phase == Working, then s.current_height > s.last_decided_height, right?

jmalicevic · 2026-01-23T11:09:18Z

specs/emerald.qnt

+
+    val decided_proposals =
+      s.proposals
+        .filter(p => p.in(ext.decided_proposals))


decided_proposals here is what we call in the code decided_block right?

mpoke · 2026-01-23T11:29:54Z

specs/emerald.qnt

+        current_height: decided.height + 1,
+        current_round: 0,


Isn't the new height and round updated on receiving start_round?

I've noticed that we are doing this in the code. It's weird.

mpoke · 2026-01-23T16:06:45Z

specs/emerald.qnt

+  pure def listen_received_proposal(ctx: LocalContext): Set[Proposal] = {
+    val s = ctx.state
+
+    if (s.phase == Working)


I think ReceivedProposalPart can be received also in the Ready phase.

erickpintor force-pushed the erick/mbt-quint-specs branch from e66a7e7 to e0ba0f9 Compare January 19, 2026 19:18

bugarela approved these changes Jan 19, 2026

View reviewed changes

specs/emerald.qnt Outdated Show resolved Hide resolved

specs/emerald.qnt Outdated Show resolved Hide resolved

specs/emerald.qnt Outdated Show resolved Hide resolved

specs/emerald.qnt Outdated Show resolved Hide resolved

specs/emerald_tests.qnt Outdated Show resolved Hide resolved

erickpintor force-pushed the erick/mbt-quint-specs branch from e0ba0f9 to 1cdf7c1 Compare January 20, 2026 12:39

erickpintor marked this pull request as ready for review January 20, 2026 12:39

erickpintor requested a review from a team as a code owner January 20, 2026 12:39

mpoke reviewed Jan 21, 2026

View reviewed changes

erickpintor force-pushed the erick/mbt-quint-specs branch 3 times, most recently from 685b0bb to 82100c8 Compare January 21, 2026 21:23

test(mbt): Introduce Quint specs for Emerald

8315822

This patch introduces Quint specifications that model Emerald's behavior wrt. Malachite consensus inputs. These specs is based on the `app.rs` message handlers and will be used for MBT later.

erickpintor force-pushed the erick/mbt-quint-specs branch from 82100c8 to 8315822 Compare January 22, 2026 14:04

mpoke reviewed Jan 23, 2026

View reviewed changes

Merge branch 'main' into erick/mbt-quint-specs

bc6fcc0

mpoke reviewed Jan 23, 2026

View reviewed changes

jmalicevic reviewed Jan 23, 2026

View reviewed changes

mpoke reviewed Jan 23, 2026

View reviewed changes

	// This will compute the retain heigth for the certificates which is based on the
	// retain height set in the config.
	// The intermediary block data stored for Consensus is pruned at every height after
	// VALUE_RETAIN_HEIGHT (defined in store.rs)
	let retain_height = Height::new(
	certificate
	.height
	.as_u64()
	.saturating_sub(self.max_retain_blocks),
	);

test(mbt): Introduce Quint specs for Emerald #183

Are you sure you want to change the base?

test(mbt): Introduce Quint specs for Emerald #183

Uh oh!

Conversation

erickpintor commented Jan 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

bugarela left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mpoke left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

erickpintor commented Jan 19, 2026 •

edited

Loading