test: Fix bug in MBT test where some steps were skipped (#129)

* Use `expect` instead of `then(assert(...))` in specs to avoid stuttering states

* Update README

Code/itf/src/utils.rs

@@ -1,7 +1,6 @@
 use glob::glob;
 use std::path::Path;
 
-// TODO(rano): simplify this function once quint is fixed
 pub fn generate_traces(spec_rel_path: &str, gen_dir: &str, quint_seed: u64) {
     println!("🪄 Generating traces for {spec_rel_path:?}...");
 
@@ -35,59 +34,4 @@ pub fn generate_traces(spec_rel_path: &str, gen_dir: &str, quint_seed: u64) {
     {
         std::fs::remove_file(&redundant_itf).unwrap();
     }
-
-    // Rerun quint per tests
-    // https://github.com/informalsystems/quint/issues/1263
-    for itf_json in glob(&format!("{}/*.itf.json", gen_dir,))
-        .expect("Failed to read glob pattern")
-        .flatten()
-    {
-        std::fs::remove_file(&itf_json).unwrap();
-
-        std::process::Command::new("quint")
-            .arg("test")
-            .arg("--output")
-            .arg(format!(
-                "{}/{}_{{}}.itf.json",
-                gen_dir,
-                spec_path.file_stem().unwrap().to_str().unwrap()
-            ))
-            .arg("--match")
-            .arg(
-                itf_json
-                    .file_name()
-                    .unwrap()
-                    .to_string_lossy()
-                    .strip_suffix(".itf.json")
-                    .unwrap(),
-            )
-            .arg("--seed")
-            .arg(quint_seed.to_string())
-            .arg(spec_path)
-            .current_dir(spec_path.parent().unwrap())
-            .output()
-            .expect("Failed to run quint test");
-    }
-
-    // Remove duplicate states
-    // https://github.com/informalsystems/quint/issues/1252
-    for itf_json in glob(&format!("{}/*.itf.json", gen_dir,))
-        .expect("Failed to read glob pattern")
-        .flatten()
-    {
-        let mut json: serde_json::Value =
-            serde_json::from_reader(std::fs::File::open(&itf_json).unwrap()).unwrap();
-
-        let states = json["states"].as_array_mut().unwrap();
-        states.retain(|state| {
-            let index = state["#meta"]["index"].as_u64().unwrap();
-            index % 2 == 0
-        });
-        states.iter_mut().enumerate().for_each(|(i, state)| {
-            state["#meta"]["index"] = serde_json::Value::from(i as u64);
-        });
-
-        let mut json_file = std::fs::File::create(&itf_json).unwrap();
-        serde_json::to_writer_pretty(&mut json_file, &json).unwrap();
-    }
 }

README.md

@@ -7,6 +7,7 @@
 [![Apache 2.0 Licensed][license-image]][license-link]
 ![Rust Stable][rustc-image]
 ![Rust 1.74+][rustc-version]
+[![Quint 0.18][quint-version]][quint-repo]
 
 Tendermint consensus in Rust
 
@@ -18,7 +19,10 @@ The repository is split in three areas, each covering one of the important areas
 2. [Docs](./Docs): Comprises Architectural Decision Records (ADRs) and other documentation, such as the 2018 paper describing the core consensus algorithm.
 3. [Specs](./Specs): English and [Quint][quint-repo] specifications.
 
-[quint-repo]: https://github.com/informalsystems/quint
+## Requirements
+
+- Rust v1.74+ ([rustup.rs](https://rustup.rs))
+- Quint v0.18+ ([github.com](https://github.com/informalsystems/quint))
 
 ## License
 
@@ -41,5 +45,7 @@ Unless required by applicable law or agreed to in writing, software distributed
 [coverage-link]: https://codecov.io/gh/informalsystems/malachite
 [license-image]: https://img.shields.io/badge/license-Apache_2.0-blue.svg
 [license-link]: https://github.com/informalsystems/hermes/blob/master/LICENSE
-[rustc-image]: https://img.shields.io/badge/rustc-stable-orange.svg
-[rustc-version]: https://img.shields.io/badge/rustc-1.74+-orange.svg
+[rustc-image]: https://img.shields.io/badge/Rust-stable-orange.svg
+[rustc-version]: https://img.shields.io/badge/Rust-1.74+-orange.svg
+[quint-version]: https://img.shields.io/badge/Quint-0.18-purple.svg
+[quint-repo]: https://github.com/informalsystems/quint

Specs/Quint/consensusTest.qnt

@@ -71,57 +71,57 @@ module consensusTest {
     run DecideNonProposerTest =
         initFor("Josef", 1)
         .then(fireInput(NewRoundCInput(0)))
-        .then(_assert(output == TimeoutOutput((0, ProposeTimeout))))
+        .expect(output == TimeoutOutput((0, ProposeTimeout)))
 
         .then(fireInput(ProposalCInput((0, Val("block")))))
-        .then(_assert(output.isVoteMsgWith(Prevote, Val("block"))))
+        .expect(output.isVoteMsgWith(Prevote, Val("block")))
 
         .then(fireInput(ProposalAndPolkaAndValidCInput(Val("block"))))
-        .then(_assert(output.isVoteMsgWith(Precommit, Val("block"))))
+        .expect(output.isVoteMsgWith(Precommit, Val("block")))
 
         .then(fireInput(ProposalAndCommitAndValidCInput(Val("block"))))
-        .then(_assert(output == DecidedOutput(Val("block"))))
+        .expect(output == DecidedOutput(Val("block")))
 
     // TODO: rename test?
     run DecideNonProposerAtHeight2Test =
         initFor("Josef", 2)     
         .then(fireInput(NewRoundProposerCInput((0, "nextBlock"))))
-        .then(_assert(output == ProposalOutput(mkProposal("Josef", 2, 0, "nextBlock", -1))))
+        .expect(output == ProposalOutput(mkProposal("Josef", 2, 0, "nextBlock", -1)))
 
         .then(fireInput(ProposalCInput((0, Val("nextBlock"))))) // it is assumed that the proposer receives its own message
-        .then(_assert(output.isVoteMsgWith(Prevote, Val("nextBlock")) and state.step == PrevoteStep))
+        .expect(output.isVoteMsgWith(Prevote, Val("nextBlock")) and state.step == PrevoteStep)
 
         .then(fireInput(PolkaAnyCInput))
-        .then(_assert(output == TimeoutOutput((0, PrevoteTimeout))))
+        .expect(output == TimeoutOutput((0, PrevoteTimeout)))
 
         .then(fireInput(TimeoutPrevoteCInput((2, 0))))
-        .then(_assert(output.isVoteMsgWith(Precommit, Nil) and state.step == PrecommitStep))
+        .expect(output.isVoteMsgWith(Precommit, Nil) and state.step == PrecommitStep)
 
         .then(fireInput(PrecommitAnyCInput))
-        .then(_assert(output == TimeoutOutput((0, PrecommitTimeout))))
+        .expect(output == TimeoutOutput((0, PrecommitTimeout)))
 
         .then(fireInput(TimeoutPrecommitCInput((2, 0))))
-        .then(_assert(output == SkipRoundOutput(1) and state.step == UnstartedStep))
+        .expect(output == SkipRoundOutput(1) and state.step == UnstartedStep)
 
         .then(fireInput(NewRoundCInput(1)))
-        .then(_assert(output == TimeoutOutput((1, ProposeTimeout))))
+        .expect(output == TimeoutOutput((1, ProposeTimeout)))
 
         .then(fireInput(TimeoutProposeCInput((2, 1))))
-        .then(_assert(output.isVoteMsgWith(Prevote, Nil) and state.step == PrevoteStep))
+        .expect(output.isVoteMsgWith(Prevote, Nil) and state.step == PrevoteStep)
 
         .then(fireInput(PolkaNilCInput))
-        .then(_assert(output.isVoteMsgWith(Precommit, Nil) and state.step == PrecommitStep))
+        .expect(output.isVoteMsgWith(Precommit, Nil) and state.step == PrecommitStep)
 
         .then(fireInput(PrecommitAnyCInput))
-        .then(_assert(output == TimeoutOutput((1, PrecommitTimeout))))
+        .expect(output == TimeoutOutput((1, PrecommitTimeout)))
 
         .then(fireInput(TimeoutPrecommitCInput((2, 1))))
-        .then(_assert(output == SkipRoundOutput(2)))
+        .expect(output == SkipRoundOutput(2))
 
         .then(fireInput(NewRoundCInput(2)))
-        .then(_assert(output == TimeoutOutput((2, ProposeTimeout))))
+        .expect(output == TimeoutOutput((2, ProposeTimeout)))
 
         .then(fireInput(ProposalInvalidCInput))
-        .then(_assert(output.isVoteMsgWith(Prevote, Nil) and state.step == PrevoteStep))
+        .expect(output.isVoteMsgWith(Prevote, Nil) and state.step == PrevoteStep)
 
 }

Specs/Quint/voteBookkeeperTest.qnt

@@ -19,98 +19,98 @@ module voteBookkeeperTest {
     run synchronousConsensusTest =
         initWith(1, 100)
         .then(applyVoteAction(mkVote(Prevote, "alice", 1, 1, Val("v1")), 60, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Prevote, "john", 1, 1, Val("v1")), 10, 1))
-        .then(_assert(lastEmitted == PolkaValueVKOutput((1, "v1"))))
+        .expect(lastEmitted == PolkaValueVKOutput((1, "v1")))
         .then(applyVoteAction(mkVote(Prevote, "bob", 1, 1, Val("v1")), 30, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Precommit, "bob", 1, 1, Val("v1")), 30, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Precommit, "john", 1, 1, Val("v1")), 10, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Precommit, "alice", 1, 1, Val("v1")), 60, 1))
-        .then(_assert(lastEmitted == PrecommitValueVKOutput((1, "v1"))))
+        .expect(lastEmitted == PrecommitValueVKOutput((1, "v1")))
 
     // Reaching PolkaAny 
     run polkaAnyTest =
         initWith(1, 100)
         .then(applyVoteAction(mkVote(Prevote, "alice", 1, 1, Val("v1")), 60, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Prevote, "john", 1, 1, Nil), 10, 1))
-        .then(_assert(lastEmitted == PolkaAnyVKOutput(1)))
+        .expect(lastEmitted == PolkaAnyVKOutput(1))
 
     // Reaching PolkaNil
     run polkaNilTest =
         initWith(1, 100)
         .then(applyVoteAction(mkVote(Prevote, "alice", 1, 1, Nil), 60, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Prevote, "john", 1, 1, Nil), 10, 1))
-        .then(_assert(lastEmitted == PolkaNilVKOutput(1)))
+        .expect(lastEmitted == PolkaNilVKOutput(1))
 
     // Reaching Skip via n+1 threshold with prevotes from two validators at a future round
     run skipSmallQuorumAllPrevotesTest =
         initWith(1, 100)
         .then(applyVoteAction(mkVote(Prevote, "alice", 1, 1, Val("v1")), 60, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Prevote, "john", 1, 2, Val("v1")), 10, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Prevote, "bob", 1, 2, Val("v1")), 30, 1))
-        .then(_assert(lastEmitted == SkipVKOutput(2)))
+        .expect(lastEmitted == SkipVKOutput(2))
 
     // Cannot reach Skip via f+1 threshold with one prevote and one precommit from the same validator at a future round
     run noSkipSmallQuorumMixedVotesSameValTest =
         initWith(1, 90)
         .then(applyVoteAction(mkVote(Prevote, "alice", 1, 1, Val("v1")), 10, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Prevote, "john", 1, 2, Val("v1")), 20, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Precommit, "john", 1, 2, Val("v1")), 20, 1))
-        .then(_assert(lastEmitted != SkipVKOutput(2)))
+        .expect(lastEmitted != SkipVKOutput(2))
 
     // Reaching Skip via f+1 threshold with one prevote and one precommit from two validators at a future round
     run skipSmallQuorumMixedVotesTwoValsTest =
         initWith(1, 80)
         .then(applyVoteAction(mkVote(Prevote, "alice", 1, 1, Val("v1")), 50, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Prevote, "john", 1, 2, Val("v1")), 10, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Prevote, "bob", 1, 2, Val("v1")), 20, 1))
-        .then(_assert(lastEmitted == SkipVKOutput(2)))
+        .expect(lastEmitted == SkipVKOutput(2))
 
     // Reaching Skip via 2f+1 threshold with a single prevote from a single validator at a future round
     run skipQuorumSinglePrevoteTest =
         initWith(1, 100)
         .then(applyVoteAction(mkVote(Prevote, "alice", 1, 1, Val("v1")), 10, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Prevote, "john", 1, 2, Val("v1")), 60, 1))
-        .then(_assert(lastEmitted == SkipVKOutput(2)))
+        .expect(lastEmitted == SkipVKOutput(2))
 
     // Reaching Skip via 2f+1 threshold with a single precommit from a single validator at a future round
     run skipQuorumSinglePrecommitTest =
         initWith(1, 100)
         .then(applyVoteAction(mkVote(Prevote, "alice", 1, 1, Val("v1")), 10, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Precommit, "john", 1, 2, Val("v1")), 60, 1))
-        .then(_assert(lastEmitted == SkipVKOutput(2)))
+        .expect(lastEmitted == SkipVKOutput(2))
 
     // Cannot reach Skip via 2f+1 threshold with one prevote and one precommit from the same validator at a future round
     run noSkipQuorumMixedVotesSameValTest =
         initWith(1, 100)
         .then(applyVoteAction(mkVote(Prevote, "alice", 1, 1, Val("v1")), 10, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Prevote, "john", 1, 2, Val("v1")), 30, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Precommit, "john", 1, 2, Val("v1")), 30, 1))
-        .then(_assert(lastEmitted != SkipVKOutput(2)))
+        .expect(lastEmitted != SkipVKOutput(2))
 
     // Reaching Skip via 2f+1 threshold with one prevote and one precommit from two validators at a future round
     run skipQuorumMixedVotesTwoValsTest =
         initWith(1, 80)
         .then(applyVoteAction(mkVote(Prevote, "alice", 1, 1, Val("v1")), 20, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Prevote, "john", 1, 2, Val("v1")), 10, 1))
-        .then(_assert(lastEmitted == NoVKOutput))
+        .expect(lastEmitted == NoVKOutput)
         .then(applyVoteAction(mkVote(Precommit, "bob", 1, 2, Val("v1")), 50, 1))
-        .then(_assert(lastEmitted == SkipVKOutput(2)))
+        .expect(lastEmitted == SkipVKOutput(2))
 
 }