test(mbt): Add Model Based Test for Emerald by erickpintor · Pull Request #201 · informalsystems/emerald

erickpintor · 2026-01-29T13:26:29Z

This patch connects the newly added Quint specs to Emerald's code via the Quint Connect library.

PS: the best files to start reviewing are probable tests.rs and driver.rs.

erickpintor · 2026-01-29T22:03:20Z

tests/mbt/src/tests.rs

+#[quint_run(
+    spec = "../../specs/emerald_mbt.qnt",
+    step = "step_no_failures",
+    max_samples = 32,
+    max_steps = 128
+)]
+fn simulation_no_failures() -> impl Driver {
+    EmeraldDriver::default()
+}
+
+#[quint_run(
+    spec = "../../specs/emerald_mbt.qnt",
+    step = "step_with_failures",
+    max_samples = 32,
+    max_steps = 128
+)]
+fn simulation_with_failures() -> impl Driver {
+    EmeraldDriver::default()
+}


First uncached run took about 30m in the CI. Let me know if you want to generate fewer traces or reduce the number of steps to minimize test time.

bugarela

All good from my side!

rnbguy · 2026-02-05T16:57:12Z

tests/mbt/src/reth.rs

+    let res = Command::new("make")
+        .env("RETH_NODES", nodes)
+        .arg(cmd)
+        .current_dir("../..")


can we use absolute path here?

you may use CARGO_MANIFEST_DIR.

It seems like CARGO_MANIFEST_DIR points to tests/mbt. I had to make the path relative to that directory anyway. Lemme know if you want me to try something else.

tests/mbt/src/reth.rs

rnbguy · 2026-02-05T16:58:28Z

tests/mbt/src/runtime.rs

+impl Runtime {
+    pub fn new(temp_dir: TempDir) -> Result<Self> {
+        Ok(Self {
+            tokio: tokio::runtime::Runtime::new()?,


why not TokioRt::new() ?

.github/workflows/test.yml

rnbguy · 2026-02-05T17:04:11Z

tests/mbt/src/driver/environment.rs

+    /// creating one Emerald and Reth instance per [crate::NODES].
+    pub fn init(&mut self) -> Result<()> {
+        // Reset the driver
+        *self = Default::default();


can you explain this line ?

I would rather prefer pub fn reinit(self) -> Result<Self> { ... }

The intent is to reset the state of the driver to its default (empty) state. I could extract it into a function but, it'd just be a function that returns Self::default().

tests/mbt/src/driver/environment.rs

rnbguy · 2026-02-05T17:56:25Z

tests/mbt/src/driver/utils.rs

+impl EmeraldDriver {
+    /// Locates the system under test and use the driver's runtime to wait for
+    /// the execution of the given future.
+    pub fn perform<'a, F, Fut>(&'a mut self, node: Node, action: F) -> Result<()>


curious why this is implemented separately.

I didn't want pollute the driver.rs file with helper functions. The driver is the main entry point into the MBT code and I usually try to keep it clean and focused on the translation between quint actions and its associated code. Happy to move things around if needed, though.

rnbguy · 2026-02-05T18:11:24Z

tests/mbt/src/sut/receive_proposal.rs

+        let peer_id = PeerId::from_multihash(Default::default())
+            .map_err(|err| anyhow!("Failed to create peer id: {err:?}"))?;


so, it's always from the same peer_id?

Yes. Because we deliver all parts at once, I didn't find that to be a problem. I can try and make for some randomized ids if you think it can improve coverage.

tests/mbt/src/sut/get_decided.rs

rnbguy · 2026-02-05T18:26:13Z

tests/mbt/src/driver/utils.rs

+        F: FnOnce(&'a mut Sut, &'a mut History) -> Fut,
+        Fut: Future<Output = Result<()>>,


don't know if it'll fit nicely but there exists AsyncFnOnce.

I'm fought the borrow checker for 5m and didn't win. AsyncFnOnce seems like an nice interface. I'll try again later and see if I get a better luck.

.github/workflows/test.yml

erickpintor · 2026-02-05T22:12:40Z

@rnbguy thank you for the detailed review 🙏

I've addressed most comments and left a few replies.

This patch connects the newly added Quint specs to Emerald's code via the Quint Connect library.

erickpintor requested review from jmalicevic and mpoke January 29, 2026 13:26

erickpintor requested a review from a team as a code owner January 29, 2026 13:26

erickpintor force-pushed the erick/introduce-mbt-suite branch 4 times, most recently from 029e72f to d09bd51 Compare January 29, 2026 21:14

erickpintor changed the base branch from erick/fix-reth-recreate to erick/mbt-reset-timeouts January 29, 2026 21:14

erickpintor commented Jan 29, 2026

View reviewed changes

erickpintor requested a review from bugarela January 29, 2026 22:04

bugarela approved these changes Jan 30, 2026

View reviewed changes

erickpintor force-pushed the erick/mbt-reset-timeouts branch from 9b46ba5 to 6343e8e Compare February 3, 2026 14:25

erickpintor force-pushed the erick/introduce-mbt-suite branch 4 times, most recently from 58ca2f7 to 1de9af2 Compare February 3, 2026 15:23

erickpintor force-pushed the erick/mbt-reset-timeouts branch from 6343e8e to b9b7e32 Compare February 4, 2026 13:25

erickpintor force-pushed the erick/introduce-mbt-suite branch from 1de9af2 to 54fca10 Compare February 4, 2026 13:28

erickpintor force-pushed the erick/mbt-reset-timeouts branch from b9b7e32 to 133095a Compare February 4, 2026 13:30

Base automatically changed from erick/mbt-reset-timeouts to main February 4, 2026 13:45

erickpintor force-pushed the erick/introduce-mbt-suite branch 3 times, most recently from 3d62414 to 805fcc9 Compare February 4, 2026 16:56

rnbguy reviewed Feb 5, 2026

View reviewed changes

.github/workflows/test.yml Show resolved Hide resolved

erickpintor force-pushed the erick/introduce-mbt-suite branch from 2f24a10 to c083964 Compare February 5, 2026 22:05

erickpintor changed the base branch from main to erick/mbt-decide-on-round February 5, 2026 22:06

test(mbt): Add Model Based Test for Emerald

ffc1a1e

This patch connects the newly added Quint specs to Emerald's code via the Quint Connect library.

erickpintor force-pushed the erick/introduce-mbt-suite branch from c083964 to ffc1a1e Compare February 5, 2026 22:16

		let peer_id = PeerId::from_multihash(Default::default())
		.map_err(\|err\| anyhow!("Failed to create peer id: {err:?}"))?;

		F: FnOnce(&'a mut Sut, &'a mut History) -> Fut,
		Fut: Future<Output = Result<()>>,

Conversation

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

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

bugarela 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!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

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!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

erickpintor commented Feb 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

erickpintor commented Jan 29, 2026 •

edited

Loading