diff --git a/Code/itf/src/utils.rs b/Code/itf/src/utils.rs index 9d35de834..4bba8df74 100644 --- a/Code/itf/src/utils.rs +++ b/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(); - } } diff --git a/README.md b/README.md index 498705e32..895400e40 100644 --- a/README.md +++ b/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 diff --git a/Specs/Quint/consensusTest.qnt b/Specs/Quint/consensusTest.qnt index 4b4749468..526a41afb 100644 --- a/Specs/Quint/consensusTest.qnt +++ b/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) } diff --git a/Specs/Quint/voteBookkeeperTest.qnt b/Specs/Quint/voteBookkeeperTest.qnt index ef9bf9f5e..d37d5f9c4 100644 --- a/Specs/Quint/voteBookkeeperTest.qnt +++ b/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)) }