From 22fe845c921bbaa7242cbf4418325117faf9a2a1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hern=C3=A1n=20Vanzetto?= <15466498+hvanz@users.noreply.github.com> Date: Tue, 19 Dec 2023 11:56:01 +0100 Subject: [PATCH] test(mbt): MBT for round state machine (#120) * Use sum type for VoteType * Use sum type for Threshold * Use sum type for ExecutorEvent * Use sum type for Value * Update executor using votekeeper's new types * Move unit tests near definition * Fix SM and tests after merge * Add types module * Comment out id in types * spec: remove initialRound * fix spec * Update itf tests * cargo fmt * Rename conflicting definitions * Use `itf` native support for sum types (#111) * spec driver: Bring some changes from main + some nits * spec driver: another missing fix * Rename voteBookkeepesSM to Models * Move votekeeper types to common types * WIP * Add timeout state functions * Fixes to value types * fix driver typecheck * fix more types * Fix value type * Renaming + comments * Fix another value expression + type annotations * renaming, commentrs, type Command * rename missing * replace match for if * Replace NewRoundStep with NoStep * Fix driver.qnt Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> * WIP * nits * spec: initial round from -1 to 0 * deserializer: NewRound to NoStep * code formatting * Revert "spec: initial round from -1 to 0" This reverts commit 9ab2c7fd79b9e7d4ee6d1d3c5deb3998ed159e6b. * Fix BigInt deserializer in minus_one_as_none * A few small fixes * Remove NewHeightCInput * Hack for initial round = -1 in spec * debugging * spec: forgot second arg for initFor * spec: driver indentation * Add NewRoundStep.. and more * spec: set NewRoundStep when skipping round; change condition in NewRound input * remove addresses from state in consensusTest: no need of multiple ConsensusStates * code formatting * more formatting * Remove unused model values * update makefile * Handle more step cases * Rename `DecidedStep` to `CommitStep` * Cleanup * Check expected value for `Vote` output * Use `pretty_assertions` crate for prettier output on failure * Add round to `TimeoutOutput` in the spec * Basic check for `GetValueAndScheduleTimeout` * Fix valid_round * spec: fix TimeoutOutput * Cleaner output * Align code with spec to start in round nil instead of zero * Add round number to `NewRound` input and update round in state machine * Rename `Step::NewRound` to `Step::Unstarted` * Rename `NewRoundStep` to `UnstartedStep` in the specs * Remove leftover Skip threshold --------- Co-authored-by: Romain Ruetschi Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> --- Code/Cargo.toml | 2 + Code/common/src/round.rs | 3 - Code/driver/src/driver.rs | 4 +- Code/driver/src/mux.rs | 2 +- Code/itf/Cargo.toml | 17 +- Code/itf/src/consensus.rs | 99 +++++++++ Code/itf/src/deserializers.rs | 15 ++ Code/itf/src/lib.rs | 2 + Code/itf/src/types.rs | 85 ++++++++ Code/itf/src/utils.rs | 2 + Code/itf/tests/consensus.rs | 67 ++++++ Code/itf/tests/consensus/runner.rs | 320 +++++++++++++++++++++++++++++ Code/itf/tests/consensus/utils.rs | 27 +++ Code/itf/tests/votekeeper.rs | 2 +- Code/round/src/input.rs | 8 +- Code/round/src/state.rs | 8 +- Code/round/src/state_machine.rs | 16 +- Code/test/src/utils.rs | 6 +- Code/test/tests/driver.rs | 6 +- Code/test/tests/round.rs | 6 +- Code/vote/src/count.rs | 2 +- Code/vote/src/keeper.rs | 9 +- Code/vote/src/lib.rs | 4 - Specs/Quint/Makefile | 25 +-- Specs/Quint/consensus.qnt | 45 ++-- Specs/Quint/consensusTest.qnt | 143 +++++++------ Specs/Quint/statemachineAsync.qnt | 13 +- Specs/Quint/statemachineTest.qnt | 4 +- Specs/Quint/types.qnt | 3 +- 29 files changed, 783 insertions(+), 162 deletions(-) create mode 100644 Code/itf/src/consensus.rs create mode 100644 Code/itf/src/deserializers.rs create mode 100644 Code/itf/tests/consensus.rs create mode 100644 Code/itf/tests/consensus/runner.rs create mode 100644 Code/itf/tests/consensus/utils.rs diff --git a/Code/Cargo.toml b/Code/Cargo.toml index daf378977..6ef4b6d6c 100644 --- a/Code/Cargo.toml +++ b/Code/Cargo.toml @@ -24,6 +24,8 @@ futures = "0.3" glob = "0.3.0" itf = "0.2.2" num-bigint = "0.4.4" +num-traits = "0.2.17" +pretty_assertions = "1.4" rand = { version = "0.8.5", features = ["std_rng"] } serde = "1.0" serde_json = "1.0" diff --git a/Code/common/src/round.rs b/Code/common/src/round.rs index db71c456e..713c8954d 100644 --- a/Code/common/src/round.rs +++ b/Code/common/src/round.rs @@ -15,9 +15,6 @@ pub enum Round { } impl Round { - /// The initial, zero round. - pub const INITIAL: Round = Round::new(0); - /// Create a new round. /// /// If `round < 0`, then `Round::Nil` is returned. diff --git a/Code/driver/src/driver.rs b/Code/driver/src/driver.rs index 92aba3cd6..19e9f0223 100644 --- a/Code/driver/src/driver.rs +++ b/Code/driver/src/driver.rs @@ -74,7 +74,7 @@ where address, validator_set, vote_keeper: votes, - round_state: RoundState::new(height, Round::new(0)), + round_state: RoundState::new(height, Round::Nil), proposal: None, pending_input: None, } @@ -173,7 +173,7 @@ where self.round_state = RoundState::new(height, round); } - self.apply_input(round, RoundInput::NewRound) + self.apply_input(round, RoundInput::NewRound(round)) } async fn apply_propose_value( diff --git a/Code/driver/src/mux.rs b/Code/driver/src/mux.rs index 94e16650a..9f52cdd6d 100644 --- a/Code/driver/src/mux.rs +++ b/Code/driver/src/mux.rs @@ -207,7 +207,7 @@ where round: Round, ) -> Option> { match pending_step { - Step::NewRound => None, // Some(RoundInput::NewRound), + Step::Unstarted => None, Step::Propose => None, diff --git a/Code/itf/Cargo.toml b/Code/itf/Cargo.toml index 011d60c72..a09a00b64 100644 --- a/Code/itf/Cargo.toml +++ b/Code/itf/Cargo.toml @@ -11,15 +11,18 @@ publish.workspace = true [dependencies] malachite-common = { version = "0.1.0", path = "../common" } malachite-vote = { version = "0.1.0", path = "../vote" } +malachite-round = { version = "0.1.0", path = "../round" } malachite-test = { version = "0.1.0", path = "../test" } -itf = { workspace = true } -rand = { workspace = true } -num-bigint = { workspace = true, features = ["serde"] } -serde = { workspace = true, features = ["derive"] } -serde_json = { workspace = true } -serde_with = { workspace = true } -glob = { workspace = true } +itf = { workspace = true } +rand = { workspace = true } +num-bigint = { workspace = true, features = ["serde"] } +num-traits = { workspace = true } +serde = { workspace = true, features = ["derive"] } +serde_json = { workspace = true } +serde_with = { workspace = true } +glob = { workspace = true } +pretty_assertions = { workspace = true } [dev-dependencies] tempfile = { version = "3.8.1" } diff --git a/Code/itf/src/consensus.rs b/Code/itf/src/consensus.rs new file mode 100644 index 000000000..1e0f5e506 --- /dev/null +++ b/Code/itf/src/consensus.rs @@ -0,0 +1,99 @@ +use itf::de::{As, Integer, Same}; +use serde::Deserialize; + +use crate::deserializers as de; +use crate::types::{Address, Height, NonNilValue, Proposal, Round, Step, Timeout, Value, Vote}; + +#[derive(Clone, Debug, Deserialize)] +pub struct State { + pub state: ConsensusState, + pub input: Input, + pub output: Output, +} + +#[derive(Clone, Debug, Deserialize)] +#[serde(rename = "ConsensusInput")] +#[serde(tag = "tag", content = "value")] +pub enum Input { + #[serde(rename = "NoConsensusInput")] + NoInput, + #[serde(rename = "NewRoundCInput")] + #[serde(with = "As::")] + NewRound(Round), + #[serde(rename = "NewRoundProposerCInput")] + #[serde(with = "As::<(Integer, Same)>")] + NewRoundProposer(Round, NonNilValue), + #[serde(rename = "ProposalCInput")] + #[serde(with = "As::<(Integer, Same)>")] + Proposal(Round, Value), + #[serde(rename = "ProposalAndPolkaPreviousAndValidCInput")] + #[serde(with = "As::<(Same, Integer)>")] + ProposalAndPolkaPreviousAndValid(Value, Round), + #[serde(rename = "ProposalInvalidCInput")] + ProposalInvalid, + #[serde(rename = "PolkaNilCInput")] + PolkaNil, + #[serde(rename = "PolkaAnyCInput")] + PolkaAny, + #[serde(rename = "ProposalAndPolkaAndValidCInput")] + ProposalAndPolkaAndValid(Value), + #[serde(rename = "PrecommitAnyCInput")] + PrecommitAny, + #[serde(rename = "ProposalAndCommitAndValidCInput")] + ProposalAndCommitAndValid(Value), + #[serde(rename = "RoundSkipCInput")] + #[serde(with = "As::")] + RoundSkip(Round), + #[serde(rename = "TimeoutProposeCInput")] + #[serde(with = "As::<(Integer, Integer)>")] + TimeoutPropose(Height, Round), + #[serde(rename = "TimeoutPrevoteCInput")] + #[serde(with = "As::<(Integer, Integer)>")] + TimeoutPrevote(Height, Round), + #[serde(rename = "TimeoutPrecommitCInput")] + #[serde(with = "As::<(Integer, Integer)>")] + TimeoutPrecommit(Height, Round), + #[serde(rename = "ProposalAndPolkaAndInvalidCInputCInput")] + #[serde(with = "As::<(Integer, Integer, Same)>")] + ProposalAndPolkaAndInvalidCInput(Height, Round, Value), +} + +#[derive(Clone, Debug, Deserialize)] +#[serde(rename = "ConsensusOutput")] +#[serde(tag = "tag", content = "value")] +pub enum Output { + #[serde(rename = "NoConsensusOutput")] + NoOutput, + #[serde(rename = "ProposalOutput")] + Proposal(Proposal), + #[serde(rename = "VoteOutput")] + Vote(Vote), + #[serde(rename = "TimeoutOutput")] + #[serde(with = "As::<(Integer, Same)>")] + Timeout(Round, Timeout), + #[serde(rename = "DecidedOutput")] + Decided(Value), + #[serde(rename = "SkipRoundOutput")] + #[serde(with = "As::")] + SkipRound(Round), + #[serde(rename = "ErrorOutput")] + Error(String), +} + +#[derive(Clone, Debug, Deserialize)] +#[serde(rename_all = "camelCase")] +pub struct ConsensusState { + #[serde(rename = "p")] + pub process: Address, + #[serde(with = "As::")] + pub height: Height, + #[serde(with = "As::")] + pub round: Round, + pub step: Step, + #[serde(deserialize_with = "de::minus_one_as_none")] + pub locked_round: Option, + pub locked_value: Value, + #[serde(deserialize_with = "de::minus_one_as_none")] + pub valid_round: Option, + pub valid_value: Value, +} diff --git a/Code/itf/src/deserializers.rs b/Code/itf/src/deserializers.rs new file mode 100644 index 000000000..2a90234bf --- /dev/null +++ b/Code/itf/src/deserializers.rs @@ -0,0 +1,15 @@ +use num_bigint::BigInt; +use num_traits::cast::ToPrimitive; +use serde::Deserialize; + +pub(crate) fn minus_one_as_none<'de, D>(de: D) -> Result, D::Error> +where + D: serde::Deserializer<'de>, +{ + let opt = Option::::deserialize(de).unwrap(); + match opt { + None => Ok(None), + Some(i) if i == BigInt::from(-1) => Ok(None), + Some(i) => Ok(i.to_i64()), + } +} diff --git a/Code/itf/src/lib.rs b/Code/itf/src/lib.rs index 04d544d47..908355fa3 100644 --- a/Code/itf/src/lib.rs +++ b/Code/itf/src/lib.rs @@ -1,3 +1,5 @@ +pub mod consensus; +pub mod deserializers; pub mod types; pub mod utils; pub mod votekeeper; diff --git a/Code/itf/src/types.rs b/Code/itf/src/types.rs index 3eb23e993..0b69d9ea8 100644 --- a/Code/itf/src/types.rs +++ b/Code/itf/src/types.rs @@ -1,4 +1,5 @@ use itf::de::{As, Integer}; +use malachite_round::state::Step as RoundStep; use serde::Deserialize; pub type Height = i64; @@ -14,6 +15,28 @@ pub enum Value { Val(NonNilValue), } +impl Value { + pub fn fold(&self, nil: A, val: impl FnOnce(&NonNilValue) -> A) -> A { + match self { + Value::Nil => nil, + Value::Val(value) => val(value), + } + } +} + +#[derive(Clone, Debug, PartialEq, Eq, Deserialize)] +#[serde(rename_all = "camelCase")] +pub struct Proposal { + pub src_address: Address, + #[serde(with = "As::")] + pub height: Height, + #[serde(with = "As::")] + pub round: Round, + pub proposal: NonNilValue, + #[serde(with = "As::")] + pub valid_round: Round, +} + #[derive(Clone, Debug, PartialEq, Eq, Deserialize)] #[serde(tag = "tag", content = "value")] pub enum VoteType { @@ -21,6 +44,15 @@ pub enum VoteType { Precommit, } +impl VoteType { + pub fn to_common(&self) -> malachite_common::VoteType { + match self { + VoteType::Prevote => malachite_common::VoteType::Prevote, + VoteType::Precommit => malachite_common::VoteType::Precommit, + } + } +} + #[derive(Clone, Debug, PartialEq, Eq, Deserialize)] #[serde(rename_all = "camelCase")] pub struct Vote { @@ -32,3 +64,56 @@ pub struct Vote { pub value_id: Value, pub src_address: Address, } + +#[derive(Clone, Debug, PartialEq, Eq, Deserialize)] +#[serde(tag = "tag", content = "value")] +pub enum Step { + #[serde(rename = "NoStep")] + None, + #[serde(rename = "UnstartedStep")] + Unstarted, + #[serde(rename = "ProposeStep")] + Propose, + #[serde(rename = "PrevoteStep")] + Prevote, + #[serde(rename = "PrecommitStep")] + Precommit, + #[serde(rename = "CommitStep")] + Commit, +} + +impl Step { + pub fn to_round_step(&self) -> Option { + match self { + Step::None => None, + Step::Unstarted => Some(RoundStep::Unstarted), + Step::Propose => Some(RoundStep::Propose), + Step::Prevote => Some(RoundStep::Prevote), + Step::Precommit => Some(RoundStep::Precommit), + Step::Commit => Some(RoundStep::Commit), + } + } +} + +#[derive(Clone, Debug, PartialEq, Eq, Deserialize)] +#[serde(tag = "tag", content = "value")] +pub enum Timeout { + #[serde(rename = "ProposeTimeout")] + Propose, + + #[serde(rename = "PrevoteTimeout")] + Prevote, + + #[serde(rename = "PrecommitTimeout")] + Precommit, +} + +impl Timeout { + pub fn to_common(&self) -> malachite_common::TimeoutStep { + match self { + Timeout::Propose => malachite_common::TimeoutStep::Propose, + Timeout::Prevote => malachite_common::TimeoutStep::Prevote, + Timeout::Precommit => malachite_common::TimeoutStep::Precommit, + } + } +} diff --git a/Code/itf/src/utils.rs b/Code/itf/src/utils.rs index c77f99c47..9d35de834 100644 --- a/Code/itf/src/utils.rs +++ b/Code/itf/src/utils.rs @@ -3,6 +3,8 @@ 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:?}..."); + let spec_abs_path = format!( "{}/../../Specs/Quint/{}", env!("CARGO_MANIFEST_DIR"), diff --git a/Code/itf/tests/consensus.rs b/Code/itf/tests/consensus.rs new file mode 100644 index 000000000..68775de6f --- /dev/null +++ b/Code/itf/tests/consensus.rs @@ -0,0 +1,67 @@ +#[path = "consensus/runner.rs"] +pub mod runner; +#[path = "consensus/utils.rs"] +pub mod utils; + +use glob::glob; +use rand::rngs::StdRng; +use rand::SeedableRng; + +use malachite_itf::consensus::State; +use malachite_itf::utils::generate_traces; +use malachite_test::{Address, PrivateKey}; + +use runner::ConsensusRunner; +use utils::ADDRESSES; + +const RANDOM_SEED: u64 = 0x42; + +#[test] +fn test_itf() { + let temp_dir = tempfile::tempdir().expect("Failed to create temp dir"); + + let quint_seed = option_env!("QUINT_SEED") + // use inspect when stabilized + .map(|x| { + println!("using QUINT_SEED={}", x); + x + }) + .or(Some("118")) + .and_then(|x| x.parse::().ok()) + .filter(|&x| x != 0) + .expect("invalid random seed for quint"); + + generate_traces( + "consensusTest.qnt", + &temp_dir.path().to_string_lossy(), + quint_seed, + ); + + for json_fixture in glob(&format!("{}/*.itf.json", temp_dir.path().display())) + .expect("Failed to read glob pattern") + .flatten() + { + println!( + "🚀 Running trace {:?}", + json_fixture.file_name().unwrap().to_str().unwrap() + ); + + let json = std::fs::read_to_string(&json_fixture).unwrap(); + let trace = itf::trace_from_str::(&json).unwrap(); + + let mut rng = StdRng::seed_from_u64(RANDOM_SEED); + + // build mapping from model addresses to real addresses + let consensus_runner = ConsensusRunner { + address_map: ADDRESSES + .iter() + .map(|&name| { + let pk = PrivateKey::generate(&mut rng).public_key(); + (name.into(), Address::from_public_key(&pk)) + }) + .collect(), + }; + + trace.run_on(consensus_runner).unwrap(); + } +} diff --git a/Code/itf/tests/consensus/runner.rs b/Code/itf/tests/consensus/runner.rs new file mode 100644 index 000000000..e4de1538f --- /dev/null +++ b/Code/itf/tests/consensus/runner.rs @@ -0,0 +1,320 @@ +use std::collections::HashMap; + +use pretty_assertions::assert_eq; + +use malachite_common::{Context, NilOrVal, Round, TimeoutStep}; +use malachite_itf::consensus::{Input as ModelInput, Output as ModelOutput, State}; +use malachite_itf::types::Step; +use malachite_round::input::Input; +use malachite_round::output::Output; +use malachite_round::{state::State as RoundState, state_machine::Info}; +use malachite_test::{Address, Height, TestContext}; + +use itf::Runner as ItfRunner; + +use crate::utils::{ + value_from_model, value_from_string, value_id_from_model, value_id_from_string, +}; + +pub struct ConsensusRunner { + pub address_map: HashMap, +} + +impl ItfRunner for ConsensusRunner { + type ActualState = RoundState; + type Result = Option>; + type ExpectedState = State; + type Error = (); + + fn init(&mut self, expected: &Self::ExpectedState) -> Result { + println!("🔵 init: expected state={:?}", expected.state); + + let height = Height::new(expected.state.height as u64); + let round = expected.state.round; + + let round = Round::new(round); + let init_state = RoundState::new(height, round); + + Ok(init_state) + } + + fn step( + &mut self, + actual: &mut Self::ActualState, + expected: &Self::ExpectedState, + ) -> Result { + println!("🔸 step: actual state={:?}", actual); + println!("🔸 step: model input={:?}", expected.input); + println!("🔸 step: model state={:?}", expected.state); + + let address = self.address_map.get(&expected.state.process).unwrap(); + let some_other_node = self.address_map.get("Other").unwrap(); // FIXME + + let (data, input) = match &expected.input { + ModelInput::NoInput => unreachable!(), + + ModelInput::NewRound(round) => { + let round = Round::new(*round); + + ( + Info::new(round, address, some_other_node), + Input::NewRound(round), + ) + } + + // TODO: proposal value not used? + ModelInput::NewRoundProposer(round, _value) => { + let round = Round::new(*round); + (Info::new(round, address, address), Input::NewRound(round)) + } + + ModelInput::Proposal(round, value) => { + let input_round = Round::new(*round); + let data = Info::new(input_round, address, some_other_node); + let proposal = TestContext::new_proposal( + actual.height, + input_round, + value_from_model(value).unwrap(), + Round::Nil, + ); + (data, Input::Proposal(proposal)) + } + + ModelInput::ProposalAndPolkaPreviousAndValid(value, valid_round) => { + let data = Info::new(actual.round, address, some_other_node); + let proposal = TestContext::new_proposal( + actual.height, + actual.round, + value_from_model(value).unwrap(), + Round::new(*valid_round), + ); + (data, Input::ProposalAndPolkaPrevious(proposal)) + } + + ModelInput::ProposalAndPolkaAndValid(value) => { + let data = Info::new(actual.round, address, some_other_node); + let proposal = TestContext::new_proposal( + actual.height, + actual.round, + value_from_model(value).unwrap(), + Round::Nil, + ); + (data, Input::ProposalAndPolkaCurrent(proposal)) + } + + ModelInput::ProposalAndPolkaAndInvalidCInput(height, round, value) => { + let input_round = Round::new(*round); + let data = Info::new(input_round, address, some_other_node); + let proposal = TestContext::new_proposal( + Height::new(*height as u64), + input_round, + value_from_model(value).unwrap(), + Round::Nil, + ); + (data, Input::InvalidProposalAndPolkaPrevious(proposal)) + } + + ModelInput::ProposalAndCommitAndValid(value) => { + let data = Info::new(actual.round, address, some_other_node); + let proposal = TestContext::new_proposal( + actual.height, + actual.round, + value_from_model(value).unwrap(), + Round::Nil, + ); + (data, Input::ProposalAndPrecommitValue(proposal)) + } + + ModelInput::ProposalInvalid => ( + Info::new(actual.round, address, some_other_node), + Input::InvalidProposal, + ), + + ModelInput::PolkaNil => ( + Info::new(actual.round, address, some_other_node), + Input::PolkaNil, + ), + + ModelInput::PolkaAny => ( + Info::new(actual.round, address, some_other_node), + Input::PolkaAny, + ), + + ModelInput::PrecommitAny => ( + Info::new(actual.round, address, some_other_node), + Input::PrecommitAny, + ), + + ModelInput::RoundSkip(round) => { + let input_round = Round::new(*round); + ( + Info::new(input_round, address, some_other_node), + Input::SkipRound(input_round), + ) + } + + ModelInput::TimeoutPropose(_height, round) => ( + Info::new(Round::new(*round), address, some_other_node), + Input::TimeoutPropose, + ), + + ModelInput::TimeoutPrevote(_height, round) => ( + Info::new(Round::new(*round), address, some_other_node), + Input::TimeoutPrevote, + ), + + ModelInput::TimeoutPrecommit(_height, round) => ( + Info::new(Round::new(*round), address, some_other_node), + Input::TimeoutPrecommit, + ), + }; + + let round_state = core::mem::take(actual); + let transition = round_state.apply(&data, input); + + println!("🔹 transition: next state={:?}", transition.next_state); + println!("🔹 transition: output={:?}", transition.output); + + *actual = transition.next_state; + + Ok(transition.output) + } + + fn result_invariant( + &self, + result: &Self::Result, + expected: &Self::ExpectedState, + ) -> Result { + // Get expected result. + let expected_result = &expected.output; + + println!("🟣 result invariant: actual output={:?}", result); + println!("🟣 result invariant: expected output={:?}", expected_result); + + // Check result against expected result. + match result { + Some(result) => match (result, expected_result) { + (Output::NewRound(round), ModelOutput::SkipRound(expected_round)) => { + assert_eq!(round.as_i64(), *expected_round); + } + + (Output::Proposal(proposal), ModelOutput::Proposal(expected_proposal)) => { + // TODO: check expected_proposal.src_address + assert_eq!(proposal.height.as_u64() as i64, expected_proposal.height); + assert_eq!(proposal.round.as_i64(), expected_proposal.round); + assert_eq!(proposal.pol_round.as_i64(), expected_proposal.valid_round); + assert_eq!( + Some(proposal.value), + value_from_string(&expected_proposal.proposal), + "unexpected proposal value" + ); + } + + (Output::Vote(vote), ModelOutput::Vote(expected_vote)) => { + let expected_src_address = self + .address_map + .get(expected_vote.src_address.as_str()) + .unwrap(); + + assert_eq!(vote.validator_address, *expected_src_address); + assert_eq!(vote.typ, expected_vote.vote_type.to_common()); + assert_eq!(vote.height.as_u64() as i64, expected_vote.height); + assert_eq!(vote.round.as_i64(), expected_vote.round); + + let expected_value = expected_vote.value_id.fold(NilOrVal::Nil, |value| { + NilOrVal::Val(value_id_from_string(value).unwrap()) + }); + assert_eq!(vote.value, expected_value); + } + + ( + Output::ScheduleTimeout(timeout), + ModelOutput::Timeout(expected_round, expected_timeout), + ) => { + assert_eq!(timeout.round.as_i64(), *expected_round); + assert_eq!(timeout.step, expected_timeout.to_common()); + } + + ( + Output::GetValueAndScheduleTimeout(round, timeout), + ModelOutput::Proposal(proposal), + ) => { + assert_eq!(round.as_i64(), proposal.round); + assert_eq!(timeout.step, TimeoutStep::Propose); + + // TODO: We need to manually feed `ProposeValue` to the round state + // machine here, and then check the emitted proposal. + } + + (Output::Decision(decision), ModelOutput::Decided(expected_decided_value)) => { + assert_eq!( + Some(decision.value), + value_from_model(expected_decided_value), + "unexpected decided value" + ); + } + + _ => panic!("actual: {result:?}\nexpected: {expected:?}"), + }, + + None => panic!("no actual result; expected result: {expected_result:?}"), + } + + Ok(true) + } + + fn state_invariant( + &self, + actual: &Self::ActualState, + expected: &Self::ExpectedState, + ) -> Result { + // TODO: What to do with actual.height? There is no height in the spec. + + println!("🟢 state invariant: actual state={:?}", actual); + println!("🟢 state invariant: expected state={:?}", expected.state); + + if expected.state.step == Step::None { + // This is the initial state. + assert_eq!(actual.round, Round::Nil, "unexpected round"); + } else { + assert_eq!(Some(actual.step), expected.state.step.to_round_step()); + + if expected.state.step == Step::Unstarted { + // In the spec, the new round comes from the input, it's not in the state. + assert_eq!( + actual.round.as_i64(), + expected.state.round + 1, + "unexpected round" + ); + } else { + assert_eq!( + actual.round.as_i64(), + expected.state.round, + "unexpected round" + ); + } + } + assert_eq!( + actual.valid.as_ref().map(|v| v.round.as_i64()), + expected.state.valid_round, + "unexpected valid round" + ); + assert_eq!( + actual.valid.as_ref().map(|v| v.value.id()), + value_id_from_model(&expected.state.valid_value), + "unexpected valid value" + ); + assert_eq!( + actual.locked.as_ref().map(|v| v.round.as_i64()), + expected.state.locked_round, + "unexpected locked round" + ); + assert_eq!( + actual.locked.as_ref().map(|v| v.value.id()), + value_id_from_model(&expected.state.locked_value), + "unexpected locked value" + ); + + Ok(true) + } +} diff --git a/Code/itf/tests/consensus/utils.rs b/Code/itf/tests/consensus/utils.rs new file mode 100644 index 000000000..d13822914 --- /dev/null +++ b/Code/itf/tests/consensus/utils.rs @@ -0,0 +1,27 @@ +use malachite_itf::types::{NonNilValue, Value as ModelValue}; +use malachite_test::{Value, ValueId}; + +pub const ADDRESSES: [&str; 2] = ["Josef", "Other"]; + +pub fn value_from_string(v: &NonNilValue) -> Option { + match v.as_str() { + "block" => Some(Value::new(1)), + "nextBlock" => Some(Value::new(2)), + _ => panic!("unknown value {v:?}"), + } +} + +pub fn value_from_model(value: &ModelValue) -> Option { + match value { + ModelValue::Nil => None, + ModelValue::Val(v) => value_from_string(v), + } +} + +pub fn value_id_from_model(value: &ModelValue) -> Option { + value_from_model(value).map(|v| v.id()) +} + +pub fn value_id_from_string(v: &NonNilValue) -> Option { + value_from_string(v).map(|v| v.id()) +} diff --git a/Code/itf/tests/votekeeper.rs b/Code/itf/tests/votekeeper.rs index 757bcf7fc..129da364d 100644 --- a/Code/itf/tests/votekeeper.rs +++ b/Code/itf/tests/votekeeper.rs @@ -41,7 +41,7 @@ fn test_itf() { .expect("Failed to read glob pattern") .flatten() { - println!("Parsing {json_fixture:?}"); + println!("🚀 Running trace {json_fixture:?}"); let json = std::fs::read_to_string(&json_fixture).unwrap(); let trace = itf::trace_from_str::(&json).unwrap(); diff --git a/Code/round/src/input.rs b/Code/round/src/input.rs index 65558c3dc..eb3d4c81b 100644 --- a/Code/round/src/input.rs +++ b/Code/round/src/input.rs @@ -11,7 +11,7 @@ where { /// Start a new round, either as proposer or not. /// L14/L20 - NewRound, + NewRound(Round), /// Propose a value. /// L14 @@ -78,7 +78,7 @@ impl Clone for Input { #[cfg_attr(coverage_nightly, coverage(off))] fn clone(&self) -> Self { match self { - Input::NewRound => Input::NewRound, + Input::NewRound(round) => Input::NewRound(*round), Input::ProposeValue(value) => Input::ProposeValue(value.clone()), Input::Proposal(proposal) => Input::Proposal(proposal.clone()), Input::InvalidProposal => Input::InvalidProposal, @@ -110,7 +110,7 @@ impl PartialEq for Input { #[cfg_attr(coverage_nightly, coverage(off))] fn eq(&self, other: &Self) -> bool { match (self, other) { - (Input::NewRound, Input::NewRound) => true, + (Input::NewRound(round), Input::NewRound(other_round)) => round == other_round, (Input::ProposeValue(value), Input::ProposeValue(other_value)) => value == other_value, (Input::Proposal(proposal), Input::Proposal(other_proposal)) => { proposal == other_proposal @@ -158,7 +158,7 @@ where #[cfg_attr(coverage_nightly, coverage(off))] fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { - Input::NewRound => write!(f, "NewRound"), + Input::NewRound(round) => write!(f, "NewRound({:?})", round), Input::ProposeValue(value) => write!(f, "ProposeValue({:?})", value), Input::Proposal(proposal) => write!(f, "Proposal({:?})", proposal), Input::InvalidProposal => write!(f, "InvalidProposal"), diff --git a/Code/round/src/state.rs b/Code/round/src/state.rs index f70d9230b..02f626de9 100644 --- a/Code/round/src/state.rs +++ b/Code/round/src/state.rs @@ -27,10 +27,10 @@ impl RoundValue { /// The step of consensus in this round #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord)] pub enum Step { - /// The round has just started - NewRound, + /// The round has not started yet + Unstarted, - /// We are at the propose step. + /// Propose step. /// Either we are the proposer or we are waiting for a proposal. Propose, @@ -74,7 +74,7 @@ where Self { height, round, - step: Step::NewRound, + step: Step::Unstarted, locked: None, valid: None, } diff --git a/Code/round/src/state_machine.rs b/Code/round/src/state_machine.rs index 83b27f315..53688cd07 100644 --- a/Code/round/src/state_machine.rs +++ b/Code/round/src/state_machine.rs @@ -58,7 +58,7 @@ where /// Valid transitions result in at least a change to the state and/or an output. /// /// Commented numbers refer to line numbers in the spec paper. -pub fn apply(state: State, info: &Info, input: Input) -> Transition +pub fn apply(mut state: State, info: &Info, input: Input) -> Transition where Ctx: Context, { @@ -66,17 +66,23 @@ where match (state.step, input) { // - // From NewRound. Input must be for current round. + // From NewRound. // // L18 - (Step::NewRound, Input::NewRound) if this_round && info.is_proposer() => { + (Step::Unstarted, Input::NewRound(round)) if info.is_proposer() => { + // Update the round + state.round = round; + // We are the proposer propose_valid_or_get_value(state) } // L11/L20 - (Step::NewRound, Input::NewRound) if this_round => { + (Step::Unstarted, Input::NewRound(round)) => { + // Update the round + state.round = round; + // We are not the proposer schedule_timeout_propose(state) } @@ -420,7 +426,7 @@ pub fn round_skip(state: State, round: Round) -> Transition where Ctx: Context, { - let new_state = state.with_round(round).with_step(Step::NewRound); + let new_state = state.with_round(round).with_step(Step::Unstarted); Transition::to(new_state).with_output(Output::NewRound(round)) } diff --git a/Code/test/src/utils.rs b/Code/test/src/utils.rs index 0e3fb1b16..3e3fc2b37 100644 --- a/Code/test/src/utils.rs +++ b/Code/test/src/utils.rs @@ -327,7 +327,7 @@ pub fn new_round(round: Round) -> State { State { height: Height::new(1), round, - step: Step::NewRound, + step: Step::Unstarted, valid: None, locked: None, } @@ -337,7 +337,7 @@ pub fn new_round_with_proposal_and_valid(round: Round, proposal: Proposal) -> St State { height: Height::new(1), round, - step: Step::NewRound, + step: Step::Unstarted, valid: Some(RoundValue { value: proposal.value, round: Round::new(0), @@ -353,7 +353,7 @@ pub fn new_round_with_proposal_and_locked_and_valid( State { height: Height::new(1), round, - step: Step::NewRound, + step: Step::Unstarted, valid: Some(RoundValue { value: proposal.value, round: Round::new(0), diff --git a/Code/test/tests/driver.rs b/Code/test/tests/driver.rs index b2ff1b33a..2962bbac7 100644 --- a/Code/test/tests/driver.rs +++ b/Code/test/tests/driver.rs @@ -836,7 +836,7 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { new_state: State { height: Height::new(1), round: Round::new(1), - step: Step::NewRound, + step: Step::Unstarted, locked: None, valid: None, }, @@ -1038,7 +1038,7 @@ fn driver_steps_skip_round_skip_threshold() { new_state: State { height, round: Round::new(1), - step: Step::NewRound, + step: Step::Unstarted, locked: None, valid: None, }, @@ -1146,7 +1146,7 @@ fn driver_steps_skip_round_quorum_threshold() { new_state: State { height, round: Round::new(1), - step: Step::NewRound, + step: Step::Unstarted, locked: None, valid: None, }, diff --git a/Code/test/tests/round.rs b/Code/test/tests/round.rs index 0cc47f9a8..bae0a21c2 100644 --- a/Code/test/tests/round.rs +++ b/Code/test/tests/round.rs @@ -24,7 +24,7 @@ fn test_propose() { // We are the proposer let data = Info::new(round, &ADDRESS, &ADDRESS); - let transition = apply(state.clone(), &data, Input::NewRound); + let transition = apply(state.clone(), &data, Input::NewRound(round)); state.step = Step::Propose; assert_eq!(transition.next_state, state); @@ -56,9 +56,9 @@ fn test_prevote() { }; // We are not the proposer - let data = Info::new(Round::new(1), &ADDRESS, &OTHER_ADDRESS); + let data = Info::new(round, &ADDRESS, &OTHER_ADDRESS); - let transition = apply(state, &data, Input::NewRound); + let transition = apply(state, &data, Input::NewRound(round)); assert_eq!(transition.next_state.step, Step::Propose); assert_eq!( diff --git a/Code/vote/src/count.rs b/Code/vote/src/count.rs index 7d9e08c44..0d09773d5 100644 --- a/Code/vote/src/count.rs +++ b/Code/vote/src/count.rs @@ -82,7 +82,7 @@ impl VoteCount { param.is_met(sum_weight, total_weight) } - Threshold::Skip | Threshold::Unreached => false, + Threshold::Unreached => false, } } } diff --git a/Code/vote/src/keeper.rs b/Code/vote/src/keeper.rs index 777c19704..bab3747d9 100644 --- a/Code/vote/src/keeper.rs +++ b/Code/vote/src/keeper.rs @@ -185,7 +185,7 @@ where self.total_weight, ); - let output = threshold_to_output(vote.vote_type(), vote.round(), threshold); + let output = threshold_to_output(vote.vote_type(), threshold); match output { Some(output) if !per_round.emitted_outputs.contains(&output) => { @@ -248,14 +248,9 @@ where } /// Map a vote type and a threshold to a state machine output. -fn threshold_to_output( - typ: VoteType, - round: Round, - threshold: Threshold, -) -> Option> { +fn threshold_to_output(typ: VoteType, threshold: Threshold) -> Option> { match (typ, threshold) { (_, Threshold::Unreached) => None, - (_, Threshold::Skip) => Some(Output::SkipRound(round)), (VoteType::Prevote, Threshold::Any) => Some(Output::PolkaAny), (VoteType::Prevote, Threshold::Nil) => Some(Output::PolkaNil), diff --git a/Code/vote/src/lib.rs b/Code/vote/src/lib.rs index 35231ecee..8f637e6f8 100644 --- a/Code/vote/src/lib.rs +++ b/Code/vote/src/lib.rs @@ -33,10 +33,6 @@ pub enum Threshold { /// No quorum has been reached yet Unreached, - /// Minimum number of votes correct processes, - /// if at a round higher than current then skip to that round. - Skip, - /// Quorum of votes but not for the same value Any, diff --git a/Specs/Quint/Makefile b/Specs/Quint/Makefile index a42dbf825..5a351eaac 100644 --- a/Specs/Quint/Makefile +++ b/Specs/Quint/Makefile @@ -6,19 +6,8 @@ parse: npx @informalsystems/quint parse voteBookkeeperTest.qnt .PHONY: parse -test-con: - npx @informalsystems/quint run consensusTest.qnt -.PHONY: test-con - -test-sm: - npx @informalsystems/quint test statemachineTest.qnt -.PHONY: test-sm - -test-vk: - npx @informalsystems/quint test voteBookkeeperTest.qnt -.PHONY: test-vk - -test: test-con test-sm test-vk +test: + find *Test.qnt -maxdepth 1 -type f -exec time quint test {} \; .PHONY: test verify: @@ -37,9 +26,17 @@ traces-sim: .PHONY: traces-sim # Generate traces from `run` statements. -traces-run: +traces-run-vk: mkdir -p traces/votekeeper npx @informalsystems/quint test --output traces/votekeeper/{}.itf.json voteBookkeeperTest.qnt +.PHONY: traces-run-vk + +traces-run-con: + mkdir -p traces/consensus + npx @informalsystems/quint test --output traces/consensus/{}.itf.json consensusTest.qnt +.PHONY: traces-run-con + +traces-run: traces-run-vk traces-run-con .PHONY: traces-run traces: traces-sim traces-run diff --git a/Specs/Quint/consensus.qnt b/Specs/Quint/consensus.qnt index ea597fb0e..e0a7fe8ed 100644 --- a/Specs/Quint/consensus.qnt +++ b/Specs/Quint/consensus.qnt @@ -21,7 +21,8 @@ module consensus { } pure def initConsensusState(p: Address, h: Height) : ConsensusState = { - p: p, + // The node address is only needed or setting the source of the Proposal and Vote messages. + p: p, // round must be -1, as nothing should be done before a NewRound // function is called round: -1, @@ -40,8 +41,6 @@ module consensus { type ConsensusInput = // For the initial state | NoConsensusInput - // Setup the state-machine for a single-height execution - | NewHeightCInput(Height) // Start a new round, not as proposer. | NewRoundCInput(Round) // Start a new round as proposer with the proposed Value. @@ -66,7 +65,7 @@ module consensus { // Proposal and 2/3+ commits for the proposal => decision | ProposalAndCommitAndValidCInput(Value) // Receive +1/3 messages from different validators for a higher round. - | RoundSkipCInput(Round) + | RoundSkipCInput(Round) // TODO: rename to SkipRoundCInput // Timeout waiting for proposal. | TimeoutProposeCInput((Height, Round)) // Timeout waiting for prevotes for a value. @@ -78,7 +77,7 @@ module consensus { | NoConsensusOutput | ProposalOutput(Proposal) | VoteOutput(Vote) - | TimeoutOutput(Timeout) + | TimeoutOutput((Round, Timeout)) | DecidedOutput(Value) | SkipRoundOutput(Round) | ErrorOutput(str) @@ -92,7 +91,7 @@ module consensus { pure def toPrecommitOutput(state, src, height, round, valueId) = { cs: state, out: VoteOutput(mkVote(Precommit, src, height, round, valueId)) } pure def toTimeoutOutput(state, timeout) = - { cs: state, out: TimeoutOutput(timeout) } + { cs: state, out: TimeoutOutput((state.round, timeout)) } pure def toDecidedOutput(state, value) = { cs: state, out: DecidedOutput(value) } pure def toSkipRoundOutput(state, round) = @@ -122,27 +121,29 @@ module consensus { | NoConsensusInput => state.toErrorOutput("NoConsensusInput is not a valid consensus input") - | NewHeightCInput(h) => - if (h > state.height) - initConsensusState(state.p, h).toNoConsensusOutput() - else state.toNoConsensusOutput() - // line 11.14 | NewRoundProposerCInput(round_value) => val r = round_value._1 val v = round_value._2 - if (r > state.round) + if (not(state.step.in(Set(UnstartedStep, NoStep)))) + state.toErrorOutput("state is not Unstarted or initial step") + else if (r <= state.round) + state.toErrorOutput("new round is not bigger than current round") + else val proposedValue = if (state.validValue != Nil) state.validValue.getVal() else v // lines 15-18 state .with("step", ProposeStep) .with("round", r) .toProposalOutput(state.p, state.height, r, proposedValue, state.validRound) // line 19 - else state.toErrorOutput("new round is not bigger than current round") // line 11.20 // TODO: discuss comment "ev.round must match state.round" | NewRoundCInput(r) => - if (r > state.round) + if (not(state.step.in(Set(UnstartedStep, NoStep)))) + state.toErrorOutput("state is not Unstarted or initial step") + else if (r <= state.round) + state.toErrorOutput("new round is not bigger than current round") + else // We just report that a timeout should be started. The executor must take care // of figuring out whether it needs to record the round number and height per // timeout @@ -150,7 +151,6 @@ module consensus { .with("step", ProposeStep) .with("round", r) .toTimeoutOutput(ProposeTimeout) // line 21 - else state.toErrorOutput("new round is not bigger than current round") // line 22 // Here it is assumed that @@ -241,11 +241,11 @@ module consensus { // line 49 | ProposalAndCommitAndValidCInput(v) => - if (state.step != DecidedStep) + if (state.step != CommitStep) state - .with("step", DecidedStep) + .with("step", CommitStep) .toDecidedOutput(v) - else state.toErrorOutput("ProposalAndCommitAndValidCInput when in DecidedStep") + else state.toErrorOutput("ProposalAndCommitAndValidCInput when in CommitStep") | ProposalAndPolkaAndInvalidCInput => // TODO @@ -254,7 +254,9 @@ module consensus { // line 55 | RoundSkipCInput(r) => if (r > state.round) - state.toSkipRoundOutput(r) + state + .with("step", UnstartedStep) + .toSkipRoundOutput(r) else state.toErrorOutput("RoundSkipCInput for round not bigger than current round") // line 57 @@ -285,7 +287,10 @@ module consensus { if (h == state.height and r == state.round) // TODO: here we should call newRound. For this we would need to know whether // we are proposer for next round. - state.toSkipRoundOutput(state.round + 1) + state + // CHECK: setting the step to UnstartedStep was added to match the code behavior + .with("step", UnstartedStep) + .toSkipRoundOutput(state.round + 1) else state.toErrorOutput("TimeoutPrecommitCInput") } diff --git a/Specs/Quint/consensusTest.qnt b/Specs/Quint/consensusTest.qnt index 7e5942e3b..4b4749468 100644 --- a/Specs/Quint/consensusTest.qnt +++ b/Specs/Quint/consensusTest.qnt @@ -9,25 +9,25 @@ module consensusTest { // Consensus state machine // ************************************************************************* - var system: Address -> ConsensusState - var _input: (Address, ConsensusInput) - var _output: ConsensusOutput - - action initFor(processes: Set[Address]): bool = all { - system' = processes.mapBy(p => initConsensusState(p, 1)), - _input' = (noAddress, NoConsensusInput), - _output' = NoConsensusOutput, + var state: ConsensusState + var input: ConsensusInput + var output: ConsensusOutput + + action initFor(p: Address, height: Height): bool = all { + state' = initConsensusState(p, height), + input' = NoConsensusInput, + output' = NoConsensusOutput, } - action init = initFor(Set("Josef")) + action init = initFor("Josef", 1) // For testing. - action fireInput(proc: Address, input: ConsensusInput): bool = - val res = consensus(system.get(proc), input) + action fireInput(__input: ConsensusInput): bool = + val res = consensus(state, __input) all { - system' = system.put(proc, res.cs), - _input' = (proc, input), - _output' = res.out, + state' = res.cs, + input' = __input, + output' = res.out, } action step = @@ -36,28 +36,27 @@ module consensusTest { nondet v = oneOf(Set("A", "B", "C")) nondet vr = oneOf(Set(-1, 1, 2, 3, 4)) any { - fireInput("Josef", NewHeightCInput(h)), - fireInput("Josef", NewRoundCInput(r)), - fireInput("Josef", NewRoundProposerCInput((r, v))), - fireInput("Josef", ProposalCInput((r, Val(v)))), - fireInput("Josef", ProposalAndPolkaPreviousAndValidCInput((Val(v), r))), - fireInput("Josef", ProposalInvalidCInput), - fireInput("Josef", PolkaNilCInput), - fireInput("Josef", PolkaAnyCInput), - fireInput("Josef", ProposalAndPolkaAndValidCInput(Val(v))), - fireInput("Josef", PrecommitAnyCInput), - fireInput("Josef", ProposalAndCommitAndValidCInput(Val(v))), - fireInput("Josef", RoundSkipCInput(r)), - fireInput("Josef", TimeoutProposeCInput((h, r))), - fireInput("Josef", TimeoutPrevoteCInput((h, r))), - fireInput("Josef", TimeoutPrecommitCInput((h, r))), - fireInput("Josef", ProposalAndPolkaAndInvalidCInput((h, r, Val(v)))), + fireInput(NewRoundCInput(r)), + fireInput(NewRoundProposerCInput((r, v))), + fireInput(ProposalCInput((r, Val(v)))), + fireInput(ProposalAndPolkaPreviousAndValidCInput((Val(v), r))), + fireInput(ProposalInvalidCInput), + fireInput(PolkaNilCInput), + fireInput(PolkaAnyCInput), + fireInput(ProposalAndPolkaAndValidCInput(Val(v))), + fireInput(PrecommitAnyCInput), + fireInput(ProposalAndCommitAndValidCInput(Val(v))), + fireInput(RoundSkipCInput(r)), + fireInput(TimeoutProposeCInput((h, r))), + fireInput(TimeoutPrevoteCInput((h, r))), + fireInput(TimeoutPrecommitCInput((h, r))), + fireInput(ProposalAndPolkaAndInvalidCInput((h, r, Val(v)))), } action unchangedAll = all { - system' = system, - _input' = _input, - _output' = _output, + state' = state, + input' = input, + output' = output, } // ************************************************************************* @@ -70,59 +69,59 @@ module consensusTest { // This test should call each input type at least once run DecideNonProposerTest = - initFor(Set("Josef")) - .then(fireInput("Josef", NewRoundCInput(0))) - .then(_assert(_output == TimeoutOutput(ProposeTimeout))) - - .then(fireInput("Josef", ProposalCInput((0, Val("block"))))) - .then(_assert(_output.isVoteMsgWith(Prevote, Val("block")))) + initFor("Josef", 1) + .then(fireInput(NewRoundCInput(0))) + .then(_assert(output == TimeoutOutput((0, ProposeTimeout)))) - .then(fireInput("Josef", ProposalAndPolkaAndValidCInput(Val("block")))) - .then(_assert(_output.isVoteMsgWith(Precommit, Val("block")))) + .then(fireInput(ProposalCInput((0, Val("block"))))) + .then(_assert(output.isVoteMsgWith(Prevote, Val("block")))) - .then(fireInput("Josef", ProposalAndCommitAndValidCInput(Val("block")))) - .then(_assert(_output == DecidedOutput(Val("block")))) + .then(fireInput(ProposalAndPolkaAndValidCInput(Val("block")))) + .then(_assert(output.isVoteMsgWith(Precommit, Val("block")))) - .then(fireInput("Josef", NewHeightCInput(system.get("Josef").height + 1))) - .then(_assert(system.get("Josef").height == 2)) - - .then(fireInput("Josef", NewRoundProposerCInput((0, "nextBlock")))) - .then(_assert(_output == ProposalOutput(mkProposal("Josef", 2, 0, "nextBlock", -1)))) + .then(fireInput(ProposalAndCommitAndValidCInput(Val("block")))) + .then(_assert(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)))) - .then(fireInput("Josef", ProposalCInput((0, Val("nextBlock"))))) // it is assumed that the proposer receives its own message - .then(_assert(_output.isVoteMsgWith(Prevote, Val("nextBlock")) and system.get("Josef").step == PrevoteStep)) + .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)) - .then(fireInput("Josef", PolkaAnyCInput)) - .then(_assert(_output == TimeoutOutput(PrevoteTimeout))) + .then(fireInput(PolkaAnyCInput)) + .then(_assert(output == TimeoutOutput((0, PrevoteTimeout)))) - .then(fireInput("Josef", TimeoutPrevoteCInput((2, 0)))) - .then(_assert(_output.isVoteMsgWith(Precommit, Nil) and system.get("Josef").step == PrecommitStep)) + .then(fireInput(TimeoutPrevoteCInput((2, 0)))) + .then(_assert(output.isVoteMsgWith(Precommit, Nil) and state.step == PrecommitStep)) - .then(fireInput("Josef", PrecommitAnyCInput)) - .then(_assert(_output == TimeoutOutput(PrecommitTimeout))) + .then(fireInput(PrecommitAnyCInput)) + .then(_assert(output == TimeoutOutput((0, PrecommitTimeout)))) - .then(fireInput("Josef", TimeoutPrecommitCInput((2, 0)))) - .then(_assert(_output == SkipRoundOutput(1))) + .then(fireInput(TimeoutPrecommitCInput((2, 0)))) + .then(_assert(output == SkipRoundOutput(1) and state.step == UnstartedStep)) - .then(fireInput("Josef", NewRoundCInput(1))) - .then(_assert(_output == TimeoutOutput(ProposeTimeout))) + .then(fireInput(NewRoundCInput(1))) + .then(_assert(output == TimeoutOutput((1, ProposeTimeout)))) - .then(fireInput("Josef", TimeoutProposeCInput((2, 1)))) - .then(_assert(_output.isVoteMsgWith(Prevote, Nil) and system.get("Josef").step == PrevoteStep)) + .then(fireInput(TimeoutProposeCInput((2, 1)))) + .then(_assert(output.isVoteMsgWith(Prevote, Nil) and state.step == PrevoteStep)) - .then(fireInput("Josef", PolkaNilCInput)) - .then(_assert(_output.isVoteMsgWith(Precommit, Nil) and system.get("Josef").step == PrecommitStep)) + .then(fireInput(PolkaNilCInput)) + .then(_assert(output.isVoteMsgWith(Precommit, Nil) and state.step == PrecommitStep)) - .then(fireInput("Josef", PrecommitAnyCInput)) - .then(_assert(_output == TimeoutOutput(PrecommitTimeout))) + .then(fireInput(PrecommitAnyCInput)) + .then(_assert(output == TimeoutOutput((1, PrecommitTimeout)))) - .then(fireInput("Josef", TimeoutPrecommitCInput((2, 1)))) - .then(_assert(_output == SkipRoundOutput(2))) + .then(fireInput(TimeoutPrecommitCInput((2, 1)))) + .then(_assert(output == SkipRoundOutput(2))) - .then(fireInput("Josef", NewRoundCInput(2))) - .then(_assert(_output == TimeoutOutput(ProposeTimeout))) + .then(fireInput(NewRoundCInput(2))) + .then(_assert(output == TimeoutOutput((2, ProposeTimeout)))) - .then(fireInput("Josef", ProposalInvalidCInput)) - .then(_assert(_output.isVoteMsgWith(Prevote, Nil) and system.get("Josef").step == PrevoteStep)) + .then(fireInput(ProposalInvalidCInput)) + .then(_assert(output.isVoteMsgWith(Prevote, Nil) and state.step == PrevoteStep)) } diff --git a/Specs/Quint/statemachineAsync.qnt b/Specs/Quint/statemachineAsync.qnt index 57a7a0b66..ed7753d03 100644 --- a/Specs/Quint/statemachineAsync.qnt +++ b/Specs/Quint/statemachineAsync.qnt @@ -115,11 +115,14 @@ action valStep(v: Address) : bool = { voteBuffer' = sendVote(voteBuffer, vote), system' = sys, } - | TimeoutOutput(timeout) => all { - propBuffer' = propBuffer, - voteBuffer' = voteBuffer, - system' = startTimeout(sys, v, timeout), - } + | TimeoutOutput(round_timeout) => + val round = round_timeout._1 // not used + val timeout = round_timeout._2 + all { + propBuffer' = propBuffer, + voteBuffer' = voteBuffer, + system' = startTimeout(sys, v, timeout), + } | SkipRoundOutput(round) => all { // CHECK: round is not used propBuffer' = propBuffer, voteBuffer' = voteBuffer, diff --git a/Specs/Quint/statemachineTest.qnt b/Specs/Quint/statemachineTest.qnt index 528e58b55..1f7156b1e 100644 --- a/Specs/Quint/statemachineTest.qnt +++ b/Specs/Quint/statemachineTest.qnt @@ -70,7 +70,7 @@ action valStep(v: Address): bool = | VoteOutput(vote) => system' = deliverVote(sys, vote) // TODO: this is immediate | TimeoutOutput(timeout) => - system' = startTimeout(sys, v, timeout) + system' = startTimeout(sys, v, timeout._2) | SkipRoundOutput(round) => // CHECK: round is not used //skipRound should never leave the driver system' = sys @@ -115,7 +115,7 @@ action valStepCommand(v: Address, command: Command): bool = | VoteOutput(vote) => system' = deliverVote(sys, vote) // TODO: this is immediate | TimeoutOutput(timeout) => - system' = startTimeout(sys, v, timeout) + system' = startTimeout(sys, v, timeout._2) | SkipRoundOutput(round) => // CHECK: round is not used //skipRound should never leave the driver system' = sys diff --git a/Specs/Quint/types.qnt b/Specs/Quint/types.qnt index 5f998c5fb..fd70ef64b 100644 --- a/Specs/Quint/types.qnt +++ b/Specs/Quint/types.qnt @@ -33,10 +33,11 @@ module types { // Steps in a round type Step = | NoStep + | UnstartedStep | ProposeStep | PrevoteStep | PrecommitStep - | DecidedStep + | CommitStep type Timeout = | ProposeTimeout // Timeout waiting for proposal.