diff --git a/.github/dependabot.yml b/.github/dependabot.yml new file mode 100644 index 000000000..3884971d8 --- /dev/null +++ b/.github/dependabot.yml @@ -0,0 +1,8 @@ +# https://docs.github.com/github/administering-a-repository/configuration-options-for-dependency-updates + +version: 2 +updates: + - package-ecosystem: "cargo" + directory: "/Code" + schedule: + interval: "weekly" diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 86bf4fede..8d424afc1 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -15,6 +15,7 @@ on: jobs: coverage: + name: Integration runs-on: ubuntu-latest defaults: run: @@ -38,7 +39,7 @@ jobs: - name: Install cargo-llvm-cov uses: taiki-e/install-action@cargo-llvm-cov - name: Generate code coverage - run: cargo llvm-cov nextest --all-features --workspace --lcov --output-path lcov.info + run: cargo llvm-cov nextest --workspace --exclude malachite-itf --all-features --lcov --output-path lcov.info - name: Generate text report run: cargo llvm-cov report - name: Upload coverage to Codecov @@ -46,4 +47,41 @@ jobs: with: token: ${{ secrets.CODECOV_TOKEN }} files: Code/lcov.info + flags: integration + fail_ci_if_error: true + + mbt-coverage: + name: MBT + runs-on: ubuntu-latest + defaults: + run: + working-directory: Code + env: + CARGO_TERM_COLOR: always + steps: + - name: Checkout + uses: actions/checkout@v4 + - uses: actions/setup-node@v3 + with: + node-version: "18" + - run: npm install -g @informalsystems/quint + - name: Setup Rust toolchain + uses: actions-rust-lang/setup-rust-toolchain@v1 + with: + toolchain: nightly + components: llvm-tools-preview + - name: Install cargo-nextest + uses: taiki-e/install-action@cargo-nextest + - name: Install cargo-llvm-cov + uses: taiki-e/install-action@cargo-llvm-cov + - name: Generate code coverage + run: cargo llvm-cov nextest -p malachite-itf --all-features --lcov --output-path lcov.info + - name: Generate text report + run: cargo llvm-cov report + - name: Upload coverage to Codecov + uses: codecov/codecov-action@v3 + with: + token: ${{ secrets.CODECOV_TOKEN }} + files: Code/lcov.info + flags: mbt fail_ci_if_error: true diff --git a/.github/workflows/mbt.yml b/.github/workflows/mbt.yml index 639213c65..1f2f5f975 100644 --- a/.github/workflows/mbt.yml +++ b/.github/workflows/mbt.yml @@ -42,4 +42,4 @@ jobs: run: echo "QUINT_SEED=$(date +%s)" >> $GITHUB_ENV - name: Run tests from traces (with random seed) working-directory: Code/itf - run: cargo nextest run --workspace --all-features test_itf + run: cargo nextest run -p malachite-itf --all-features diff --git a/.github/workflows/quint.yml b/.github/workflows/quint.yml index 26099622f..83eb965bf 100644 --- a/.github/workflows/quint.yml +++ b/.github/workflows/quint.yml @@ -26,10 +26,12 @@ jobs: quint-test: name: Test runs-on: ubuntu-latest + env: + MAX_SAMPLES: 100 steps: - uses: actions/checkout@v4 - uses: actions/setup-node@v3 with: node-version: "18" - run: npm install -g @informalsystems/quint - - run: bash Scripts/quint-forall.sh test Specs/Quint/*Test.qnt + - run: bash Scripts/quint-forall.sh "test --max-samples $MAX_SAMPLES" Specs/Quint/*Test.qnt diff --git a/Code/.cargo/config.toml b/Code/.cargo/config.toml new file mode 100644 index 000000000..e914d4462 --- /dev/null +++ b/Code/.cargo/config.toml @@ -0,0 +1,3 @@ +[alias] +mbt = "nextest run -p malachite-itf --all-features" +integration = "nextest run --workspace --exclude malachite-itf" diff --git a/Code/QUESTIONS.md b/Code/QUESTIONS.md deleted file mode 100644 index 700c9fae4..000000000 --- a/Code/QUESTIONS.md +++ /dev/null @@ -1 +0,0 @@ -- How do we deal with errors? diff --git a/Code/TODO.md b/Code/TODO.md deleted file mode 100644 index 8a7878e9e..000000000 --- a/Code/TODO.md +++ /dev/null @@ -1,11 +0,0 @@ -is proposal complete -if polka not nil, then need to see proof of lock (2f+1 votes) -then send proposal - -count votes for cur, prev, 1/2 next round - -if complete proposal from a past round => to current one -if we have some threshold (f+1) of votes for a future round => skip to that round - -context (get proposer, get value) -signing context diff --git a/Code/driver/src/driver.rs b/Code/driver/src/driver.rs index f941927c6..137bd2bb7 100644 --- a/Code/driver/src/driver.rs +++ b/Code/driver/src/driver.rs @@ -5,17 +5,17 @@ use malachite_common::{ Context, Proposal, Round, SignedVote, Timeout, TimeoutStep, Validator, ValidatorSet, Value, Vote, VoteType, }; -use malachite_round::events::Event as RoundEvent; -use malachite_round::message::Message as RoundMessage; +use malachite_round::input::Input as RoundInput; +use malachite_round::output::Output as RoundOutput; use malachite_round::state::{State as RoundState, Step}; use malachite_round::state_machine::Info; -use malachite_vote::keeper::Message as VoteMessage; +use malachite_vote::keeper::Output as VoteKeeperOutput; use malachite_vote::keeper::VoteKeeper; use malachite_vote::Threshold; use malachite_vote::ThresholdParams; -use crate::event::Event; -use crate::message::Message; +use crate::input::Input; +use crate::output::Output; use crate::proposals::Proposals; use crate::Error; use crate::ProposerSelector; @@ -84,47 +84,47 @@ where Ok(proposer) } - pub async fn execute(&mut self, msg: Event) -> Result>, Error> { - let round_msg = match self.apply(msg).await? { + pub async fn execute(&mut self, msg: Input) -> Result>, Error> { + let round_output = match self.apply(msg).await? { Some(msg) => msg, None => return Ok(None), }; - let msg = match round_msg { - RoundMessage::NewRound(round) => Message::NewRound(self.height().clone(), round), + let output = match round_output { + RoundOutput::NewRound(round) => Output::NewRound(self.height().clone(), round), - RoundMessage::Proposal(proposal) => { - // sign the proposal - Message::Propose(proposal) + RoundOutput::Proposal(proposal) => { + // TODO: sign the proposal + Output::Propose(proposal) } - RoundMessage::Vote(vote) => { + RoundOutput::Vote(vote) => { let signed_vote = self.ctx.sign_vote(vote); - Message::Vote(signed_vote) + Output::Vote(signed_vote) } - RoundMessage::ScheduleTimeout(timeout) => Message::ScheduleTimeout(timeout), + RoundOutput::ScheduleTimeout(timeout) => Output::ScheduleTimeout(timeout), - RoundMessage::GetValueAndScheduleTimeout(round, timeout) => { - Message::GetValueAndScheduleTimeout(round, timeout) + RoundOutput::GetValueAndScheduleTimeout(round, timeout) => { + Output::GetValueAndScheduleTimeout(round, timeout) } - RoundMessage::Decision(value) => { + RoundOutput::Decision(value) => { // TODO: update the state - Message::Decide(value.round, value.value) + Output::Decide(value.round, value.value) } }; - Ok(Some(msg)) + Ok(Some(output)) } - async fn apply(&mut self, event: Event) -> Result>, Error> { - match event { - Event::NewRound(height, round) => self.apply_new_round(height, round).await, - Event::ProposeValue(round, value) => self.apply_propose_value(round, value).await, - Event::Proposal(proposal, validity) => self.apply_proposal(proposal, validity).await, - Event::Vote(signed_vote) => self.apply_vote(signed_vote), - Event::TimeoutElapsed(timeout) => self.apply_timeout(timeout), + async fn apply(&mut self, input: Input) -> Result>, Error> { + match input { + Input::NewRound(height, round) => self.apply_new_round(height, round).await, + Input::ProposeValue(round, value) => self.apply_propose_value(round, value).await, + Input::Proposal(proposal, validity) => self.apply_proposal(proposal, validity).await, + Input::Vote(signed_vote) => self.apply_vote(signed_vote), + Input::TimeoutElapsed(timeout) => self.apply_timeout(timeout), } } @@ -132,29 +132,29 @@ where &mut self, height: Ctx::Height, round: Round, - ) -> Result>, Error> { + ) -> Result>, Error> { if self.height() == &height { // If it's a new round for same height, just reset the round, keep the valid and locked values self.round_state.round = round; } else { self.round_state = RoundState::new(height, round); } - self.apply_event(round, RoundEvent::NewRound) + self.apply_input(round, RoundInput::NewRound) } async fn apply_propose_value( &mut self, round: Round, value: Ctx::Value, - ) -> Result>, Error> { - self.apply_event(round, RoundEvent::ProposeValue(value)) + ) -> Result>, Error> { + self.apply_input(round, RoundInput::ProposeValue(value)) } async fn apply_proposal( &mut self, proposal: Ctx::Proposal, validity: Validity, - ) -> Result>, Error> { + ) -> Result>, Error> { // Check that there is an ongoing round if self.round_state.round == Round::Nil { return Ok(None); @@ -182,12 +182,12 @@ where if self.round_state.step == Step::Propose { if proposal.pol_round().is_nil() { // L26 - return self.apply_event(proposal.round(), RoundEvent::InvalidProposal); + return self.apply_input(proposal.round(), RoundInput::InvalidProposal); } else if polka_previous { // L32 - return self.apply_event( + return self.apply_input( proposal.round(), - RoundEvent::InvalidProposalAndPolkaPrevious(proposal), + RoundInput::InvalidProposalAndPolkaPrevious(proposal), ); } else { return Ok(None); @@ -205,9 +205,9 @@ where VoteType::Precommit, Threshold::Value(proposal.value().id()), ) { - return self.apply_event( + return self.apply_input( proposal.round(), - RoundEvent::ProposalAndPrecommitValue(proposal), + RoundInput::ProposalAndPrecommitValue(proposal), ); } @@ -226,29 +226,29 @@ where // L36 if polka_current { - return self.apply_event( + return self.apply_input( proposal.round(), - RoundEvent::ProposalAndPolkaCurrent(proposal), + RoundInput::ProposalAndPolkaCurrent(proposal), ); } // L28 if self.round_state.step == Step::Propose && polka_previous { // TODO: Check proposal vr is equal to threshold vr - return self.apply_event( + return self.apply_input( proposal.round(), - RoundEvent::ProposalAndPolkaPrevious(proposal), + RoundInput::ProposalAndPolkaPrevious(proposal), ); } // TODO - Caller needs to store the proposal (valid or not) as the quorum (polka or commits) may be met later - self.apply_event(proposal.round(), RoundEvent::Proposal(proposal)) + self.apply_input(proposal.round(), RoundInput::Proposal(proposal)) } fn apply_vote( &mut self, signed_vote: SignedVote, - ) -> Result>, Error> { + ) -> Result>, Error> { let validator = self .validator_set .get_by_address(signed_vote.validator_address()) @@ -267,81 +267,81 @@ where let vote_round = signed_vote.vote.round(); let current_round = self.round(); - let Some(vote_msg) = + let Some(vote_output) = self.votes .apply_vote(signed_vote.vote, validator.voting_power(), current_round) else { return Ok(None); }; - let round_event = match vote_msg { - VoteMessage::PolkaAny => RoundEvent::PolkaAny, - VoteMessage::PolkaNil => RoundEvent::PolkaNil, - VoteMessage::PolkaValue(v) => RoundEvent::PolkaValue(v), - VoteMessage::PrecommitAny => RoundEvent::PrecommitAny, - VoteMessage::PrecommitValue(v) => RoundEvent::PrecommitValue(v), - VoteMessage::SkipRound(r) => RoundEvent::SkipRound(r), + let round_input = match vote_output { + VoteKeeperOutput::PolkaAny => RoundInput::PolkaAny, + VoteKeeperOutput::PolkaNil => RoundInput::PolkaNil, + VoteKeeperOutput::PolkaValue(v) => RoundInput::PolkaValue(v), + VoteKeeperOutput::PrecommitAny => RoundInput::PrecommitAny, + VoteKeeperOutput::PrecommitValue(v) => RoundInput::PrecommitValue(v), + VoteKeeperOutput::SkipRound(r) => RoundInput::SkipRound(r), }; - self.apply_event(vote_round, round_event) + self.apply_input(vote_round, round_input) } - fn apply_timeout(&mut self, timeout: Timeout) -> Result>, Error> { - let event = match timeout.step { - TimeoutStep::Propose => RoundEvent::TimeoutPropose, - TimeoutStep::Prevote => RoundEvent::TimeoutPrevote, - TimeoutStep::Precommit => RoundEvent::TimeoutPrecommit, + fn apply_timeout(&mut self, timeout: Timeout) -> Result>, Error> { + let input = match timeout.step { + TimeoutStep::Propose => RoundInput::TimeoutPropose, + TimeoutStep::Prevote => RoundInput::TimeoutPrevote, + TimeoutStep::Precommit => RoundInput::TimeoutPrecommit, }; - self.apply_event(timeout.round, event) + self.apply_input(timeout.round, input) } - /// Apply the event, update the state. - fn apply_event( + /// Apply the input, update the state. + fn apply_input( &mut self, - event_round: Round, - event: RoundEvent, - ) -> Result>, Error> { + input_round: Round, + input: RoundInput, + ) -> Result>, Error> { let round_state = core::mem::take(&mut self.round_state); let proposer = self.get_proposer(round_state.round)?; - let data = Info::new(event_round, &self.address, proposer.address()); + let data = Info::new(input_round, &self.address, proposer.address()); // Multiplex the event with the round state. - let mux_event = match event { - RoundEvent::PolkaValue(value_id) => { - let proposal = self.proposals.find(&value_id, |p| p.round() == event_round); + let mux_input = match input { + RoundInput::PolkaValue(value_id) => { + let proposal = self.proposals.find(&value_id, |p| p.round() == input_round); if let Some(proposal) = proposal { assert_eq!(proposal.value().id(), value_id); - RoundEvent::ProposalAndPolkaCurrent(proposal.clone()) + RoundInput::ProposalAndPolkaCurrent(proposal.clone()) } else { - RoundEvent::PolkaAny + RoundInput::PolkaAny } } - RoundEvent::PrecommitValue(value_id) => { - let proposal = self.proposals.find(&value_id, |p| p.round() == event_round); + RoundInput::PrecommitValue(value_id) => { + let proposal = self.proposals.find(&value_id, |p| p.round() == input_round); if let Some(proposal) = proposal { assert_eq!(proposal.value().id(), value_id); - RoundEvent::ProposalAndPrecommitValue(proposal.clone()) + RoundInput::ProposalAndPrecommitValue(proposal.clone()) } else { - RoundEvent::PrecommitAny + RoundInput::PrecommitAny } } - _ => event, + _ => input, }; - // Apply the event to the round state machine - let transition = round_state.apply_event(&data, mux_event); + // Apply the input to the round state machine + let transition = round_state.apply(&data, mux_input); // Update state self.round_state = transition.next_state; - // Return message, if any - Ok(transition.message) + // Return output, if any + Ok(transition.output) } } diff --git a/Code/driver/src/event.rs b/Code/driver/src/input.rs similarity index 96% rename from Code/driver/src/event.rs rename to Code/driver/src/input.rs index b2cf5f726..eda6d7944 100644 --- a/Code/driver/src/event.rs +++ b/Code/driver/src/input.rs @@ -4,7 +4,7 @@ use crate::Validity; /// Events that can be received by the [`Driver`](crate::Driver). #[derive(Clone, Debug, PartialEq, Eq)] -pub enum Event +pub enum Input where Ctx: Context, { diff --git a/Code/driver/src/lib.rs b/Code/driver/src/lib.rs index a7adc74ab..fd77260a5 100644 --- a/Code/driver/src/lib.rs +++ b/Code/driver/src/lib.rs @@ -16,16 +16,16 @@ extern crate alloc; mod driver; mod error; -mod event; -mod message; +mod input; +mod output; mod proposals; mod proposer; mod util; pub use driver::Driver; pub use error::Error; -pub use event::Event; -pub use message::Message; +pub use input::Input; +pub use output::Output; pub use proposer::ProposerSelector; pub use util::Validity; diff --git a/Code/driver/src/message.rs b/Code/driver/src/message.rs deleted file mode 100644 index 52b354d80..000000000 --- a/Code/driver/src/message.rs +++ /dev/null @@ -1,93 +0,0 @@ -use core::fmt; - -use malachite_common::{Context, Round, SignedVote, Timeout}; - -/// Messages emitted by the [`Driver`](crate::Driver) -pub enum Message -where - Ctx: Context, -{ - /// Start a new round - NewRound(Ctx::Height, Round), - - /// Broadcast a proposal - Propose(Ctx::Proposal), - - /// Broadcast a vote for a value - Vote(SignedVote), - - /// Decide on a value - Decide(Round, Ctx::Value), - - /// Schedule a timeout - ScheduleTimeout(Timeout), - - /// Ask for a value to propose and schedule a timeout - GetValueAndScheduleTimeout(Round, Timeout), -} - -// NOTE: We have to derive these instances manually, otherwise -// the compiler would infer a Clone/Debug/PartialEq/Eq bound on `Ctx`, -// which may not hold for all contexts. - -impl Clone for Message { - #[cfg_attr(coverage_nightly, coverage(off))] - fn clone(&self) -> Self { - match self { - Message::NewRound(height, round) => Message::NewRound(height.clone(), *round), - Message::Propose(proposal) => Message::Propose(proposal.clone()), - Message::Vote(signed_vote) => Message::Vote(signed_vote.clone()), - Message::Decide(round, value) => Message::Decide(*round, value.clone()), - Message::ScheduleTimeout(timeout) => Message::ScheduleTimeout(*timeout), - Message::GetValueAndScheduleTimeout(round, timeout) => { - Message::GetValueAndScheduleTimeout(*round, *timeout) - } - } - } -} - -impl fmt::Debug for Message { - #[cfg_attr(coverage_nightly, coverage(off))] - fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - match self { - Message::NewRound(height, round) => write!(f, "NewRound({:?}, {:?})", height, round), - Message::Propose(proposal) => write!(f, "Propose({:?})", proposal), - Message::Vote(signed_vote) => write!(f, "Vote({:?})", signed_vote), - Message::Decide(round, value) => write!(f, "Decide({:?}, {:?})", round, value), - Message::ScheduleTimeout(timeout) => write!(f, "ScheduleTimeout({:?})", timeout), - Message::GetValueAndScheduleTimeout(round, timeout) => { - write!(f, "GetValueAndScheduleTimeout({:?}, {:?})", round, timeout) - } - } - } -} - -impl PartialEq for Message { - #[cfg_attr(coverage_nightly, coverage(off))] - fn eq(&self, other: &Self) -> bool { - match (self, other) { - (Message::NewRound(height, round), Message::NewRound(other_height, other_round)) => { - height == other_height && round == other_round - } - (Message::Propose(proposal), Message::Propose(other_proposal)) => { - proposal == other_proposal - } - (Message::Vote(signed_vote), Message::Vote(other_signed_vote)) => { - signed_vote == other_signed_vote - } - (Message::Decide(round, value), Message::Decide(other_round, other_value)) => { - round == other_round && value == other_value - } - (Message::ScheduleTimeout(timeout), Message::ScheduleTimeout(other_timeout)) => { - timeout == other_timeout - } - ( - Message::GetValueAndScheduleTimeout(round, timeout), - Message::GetValueAndScheduleTimeout(other_round, other_timeout), - ) => round == other_round && timeout == other_timeout, - _ => false, - } - } -} - -impl Eq for Message {} diff --git a/Code/driver/src/output.rs b/Code/driver/src/output.rs new file mode 100644 index 000000000..d0565f484 --- /dev/null +++ b/Code/driver/src/output.rs @@ -0,0 +1,93 @@ +use core::fmt; + +use malachite_common::{Context, Round, SignedVote, Timeout}; + +/// Messages emitted by the [`Driver`](crate::Driver) +pub enum Output +where + Ctx: Context, +{ + /// Start a new round + NewRound(Ctx::Height, Round), + + /// Broadcast a proposal + Propose(Ctx::Proposal), + + /// Broadcast a vote for a value + Vote(SignedVote), + + /// Decide on a value + Decide(Round, Ctx::Value), + + /// Schedule a timeout + ScheduleTimeout(Timeout), + + /// Ask for a value to propose and schedule a timeout + GetValueAndScheduleTimeout(Round, Timeout), +} + +// NOTE: We have to derive these instances manually, otherwise +// the compiler would infer a Clone/Debug/PartialEq/Eq bound on `Ctx`, +// which may not hold for all contexts. + +impl Clone for Output { + #[cfg_attr(coverage_nightly, coverage(off))] + fn clone(&self) -> Self { + match self { + Output::NewRound(height, round) => Output::NewRound(height.clone(), *round), + Output::Propose(proposal) => Output::Propose(proposal.clone()), + Output::Vote(signed_vote) => Output::Vote(signed_vote.clone()), + Output::Decide(round, value) => Output::Decide(*round, value.clone()), + Output::ScheduleTimeout(timeout) => Output::ScheduleTimeout(*timeout), + Output::GetValueAndScheduleTimeout(round, timeout) => { + Output::GetValueAndScheduleTimeout(*round, *timeout) + } + } + } +} + +impl fmt::Debug for Output { + #[cfg_attr(coverage_nightly, coverage(off))] + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Output::NewRound(height, round) => write!(f, "NewRound({:?}, {:?})", height, round), + Output::Propose(proposal) => write!(f, "Propose({:?})", proposal), + Output::Vote(signed_vote) => write!(f, "Vote({:?})", signed_vote), + Output::Decide(round, value) => write!(f, "Decide({:?}, {:?})", round, value), + Output::ScheduleTimeout(timeout) => write!(f, "ScheduleTimeout({:?})", timeout), + Output::GetValueAndScheduleTimeout(round, timeout) => { + write!(f, "GetValueAndScheduleTimeout({:?}, {:?})", round, timeout) + } + } + } +} + +impl PartialEq for Output { + #[cfg_attr(coverage_nightly, coverage(off))] + fn eq(&self, other: &Self) -> bool { + match (self, other) { + (Output::NewRound(height, round), Output::NewRound(other_height, other_round)) => { + height == other_height && round == other_round + } + (Output::Propose(proposal), Output::Propose(other_proposal)) => { + proposal == other_proposal + } + (Output::Vote(signed_vote), Output::Vote(other_signed_vote)) => { + signed_vote == other_signed_vote + } + (Output::Decide(round, value), Output::Decide(other_round, other_value)) => { + round == other_round && value == other_value + } + (Output::ScheduleTimeout(timeout), Output::ScheduleTimeout(other_timeout)) => { + timeout == other_timeout + } + ( + Output::GetValueAndScheduleTimeout(round, timeout), + Output::GetValueAndScheduleTimeout(other_round, other_timeout), + ) => round == other_round && timeout == other_timeout, + _ => false, + } + } +} + +impl Eq for Output {} diff --git a/Code/itf/src/consensus.rs b/Code/itf/src/consensus.rs deleted file mode 100644 index 2bb430b6a..000000000 --- a/Code/itf/src/consensus.rs +++ /dev/null @@ -1,178 +0,0 @@ -use num_bigint::BigInt; -use serde::Deserialize; -use std::collections::HashMap; - -use crate::deserializers as de; - -pub type Address = String; -pub type Value = String; -pub type Step = String; -pub type Round = BigInt; -pub type Height = BigInt; - -#[derive(Clone, Debug, Deserialize)] -pub enum Timeout { - #[serde(rename = "timeoutPrevote")] - Prevote, - - #[serde(rename = "timeoutPrecommit")] - Precommit, - - #[serde(rename = "timeoutPropose")] - Propose, -} - -#[derive(Clone, Debug, Deserialize)] -pub struct State { - pub system: System, - - #[serde(rename = "_Event")] - pub event: Event, - - #[serde(rename = "_Result")] - pub result: Result, -} - -#[derive(Clone, Debug, Deserialize)] -pub struct System(HashMap); - -#[derive(Clone, Debug, Deserialize)] -#[serde(tag = "name")] -pub enum Event { - Initial, - NewRound { - height: Height, - round: Round, - }, - Proposal { - height: Height, - round: Round, - value: Value, - }, - ProposalAndPolkaAndValid { - height: Height, - round: Round, - value: Value, - }, - ProposalAndCommitAndValid { - height: Height, - round: Round, - value: Value, - }, - NewHeight { - height: Height, - round: Round, - }, - NewRoundProposer { - height: Height, - round: Round, - value: Value, - }, - PolkaNil { - height: Height, - round: Round, - value: Value, - }, - PolkaAny { - height: Height, - round: Round, - value: Value, - }, - PrecommitAny { - height: Height, - round: Round, - value: Value, - }, - TimeoutPrevote { - height: Height, - round: Round, - }, - TimeoutPrecommit { - height: Height, - round: Round, - value: Value, - }, - TimeoutPropose { - height: Height, - round: Round, - value: Value, - }, - ProposalInvalid { - height: Height, - round: Round, - }, -} - -#[derive(Clone, Debug, Deserialize)] -#[serde(rename_all = "camelCase")] -pub struct Result { - pub name: String, - #[serde(deserialize_with = "de::proposal_or_none")] - pub proposal: Option, - #[serde(deserialize_with = "de::vote_message_or_none")] - pub vote_message: Option, - #[serde(deserialize_with = "de::empty_string_as_none")] - pub timeout: Option, - #[serde(deserialize_with = "de::empty_string_as_none")] - pub decided: Option, - #[serde(deserialize_with = "de::minus_one_as_none")] - pub skip_round: Option, -} - -#[derive(Clone, Debug, Deserialize, PartialEq, Eq)] -#[serde(rename_all = "camelCase")] -pub struct Proposal { - pub src: Address, - pub height: Height, - pub round: Round, - pub proposal: Value, - pub valid_round: Round, -} - -impl Proposal { - pub fn is_empty(&self) -> bool { - self.src.is_empty() - && self.proposal.is_empty() - && self.height == BigInt::from(-1) - && self.round == BigInt::from(-1) - && self.valid_round == BigInt::from(-1) - } -} - -#[derive(Clone, Debug, Deserialize)] -#[serde(rename_all = "camelCase")] -pub struct VoteMessage { - pub src: Address, - pub height: Height, - pub round: Round, - pub step: Step, - pub id: Value, -} - -impl VoteMessage { - pub fn is_empty(&self) -> bool { - self.src.is_empty() - && self.id.is_empty() - && self.height == BigInt::from(-1) - && self.round == BigInt::from(-1) - && self.step.is_empty() - } -} - -#[derive(Clone, Debug, Deserialize)] -#[serde(rename_all = "camelCase")] -pub struct ConsensusState { - pub p: Address, - pub height: Height, - pub round: Round, - pub step: Step, - - #[serde(deserialize_with = "de::minus_one_as_none")] - pub locked_round: Option, - #[serde(deserialize_with = "de::empty_string_as_none")] - pub locked_value: Option, - #[serde(deserialize_with = "de::minus_one_as_none")] - pub valid_round: Option, - #[serde(deserialize_with = "de::empty_string_as_none")] - pub valid_value: Option, -} diff --git a/Code/itf/src/deserializers.rs b/Code/itf/src/deserializers.rs deleted file mode 100644 index 53231f40d..000000000 --- a/Code/itf/src/deserializers.rs +++ /dev/null @@ -1,53 +0,0 @@ -use num_bigint::BigInt; -use serde::de::IntoDeserializer; -use serde::Deserialize; - -use crate::consensus::{Proposal, VoteMessage}; - -pub(crate) fn empty_string_as_none<'de, D, T>(de: D) -> Result, D::Error> -where - D: serde::Deserializer<'de>, - T: serde::Deserialize<'de>, -{ - let opt = Option::::deserialize(de)?; - match opt.as_deref() { - None | Some("") => Ok(None), - Some(s) => T::deserialize(s.into_deserializer()).map(Some), - } -} - -pub(crate) fn minus_one_as_none<'de, D>(de: D) -> Result, D::Error> -where - D: serde::Deserializer<'de>, -{ - let opt = Option::::deserialize(de)?; - match opt { - None => Ok(None), - Some(i) if i == BigInt::from(-1) => Ok(None), - Some(i) => Ok(Some(i)), - } -} - -pub(crate) fn proposal_or_none<'de, D>(de: D) -> Result, D::Error> -where - D: serde::Deserializer<'de>, -{ - let proposal = Proposal::deserialize(de)?; - if proposal.is_empty() { - Ok(None) - } else { - Ok(Some(proposal)) - } -} - -pub(crate) fn vote_message_or_none<'de, D>(de: D) -> Result, D::Error> -where - D: serde::Deserializer<'de>, -{ - let vote_message = VoteMessage::deserialize(de)?; - if vote_message.is_empty() { - Ok(None) - } else { - Ok(Some(vote_message)) - } -} diff --git a/Code/itf/src/lib.rs b/Code/itf/src/lib.rs index d8bacfb93..be66ce483 100644 --- a/Code/itf/src/lib.rs +++ b/Code/itf/src/lib.rs @@ -1,5 +1,2 @@ -pub mod consensus; -pub mod votekeeper; - -mod deserializers; pub mod utils; +pub mod votekeeper; diff --git a/Code/itf/src/votekeeper.rs b/Code/itf/src/votekeeper.rs index 933de3137..41e8d181e 100644 --- a/Code/itf/src/votekeeper.rs +++ b/Code/itf/src/votekeeper.rs @@ -41,7 +41,7 @@ pub struct RoundVotes { pub round: Round, pub prevotes: VoteCount, pub precommits: VoteCount, - pub emitted_events: HashSet, + pub emitted_outputs: HashSet, #[serde(with = "As::>")] pub votes_addresses_weights: HashMap, } @@ -57,7 +57,7 @@ pub struct VoteCount { } #[derive(Clone, Debug, PartialEq, Eq, Deserialize, Hash)] -pub struct ExecutorEvent { +pub struct VoteKeeperOutput { #[serde(with = "As::")] pub round: Round, pub name: String, @@ -69,7 +69,7 @@ pub struct State { #[serde(rename = "voteBookkeeperTest::voteBookkeeperSM::bookkeeper")] pub bookkeeper: Bookkeeper, #[serde(rename = "voteBookkeeperTest::voteBookkeeperSM::lastEmitted")] - pub last_emitted: ExecutorEvent, + pub last_emitted: VoteKeeperOutput, #[serde(rename = "voteBookkeeperTest::voteBookkeeperSM::weightedVote")] #[serde(with = "As::<(Same, Integer, Integer)>")] pub weighted_vote: (Vote, Weight, Round), diff --git a/Code/itf/tests/consensus.rs b/Code/itf/tests/consensus.rs deleted file mode 100644 index 9eac81275..000000000 --- a/Code/itf/tests/consensus.rs +++ /dev/null @@ -1,18 +0,0 @@ -use glob::glob; - -use malachite_itf::consensus::State; - -#[test] -fn test_itf() { - for json_fixture in glob("tests/fixtures/consensus/*.json") - .expect("Failed to read glob pattern") - .flatten() - { - println!("Parsing {json_fixture:?}"); - - let json = std::fs::read_to_string(&json_fixture).unwrap(); - let state = itf::trace_from_str::(&json).unwrap(); - - dbg!(state); - } -} diff --git a/Code/itf/tests/fixtures/consensus/consensus_DecideNonProposerTest_0.itf.json b/Code/itf/tests/fixtures/consensus/consensus_DecideNonProposerTest_0.itf.json deleted file mode 100644 index 16347d3a4..000000000 --- a/Code/itf/tests/fixtures/consensus/consensus_DecideNonProposerTest_0.itf.json +++ /dev/null @@ -1 +0,0 @@ -{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"consensus.qnt","status":"passed","description":"Created by Quint on Fri Nov 10 2023 14:33:14 GMT+0100 (GMT+01:00)","timestamp":1699623194345},"vars":["system","_Event","_Result"],"states":[{"#meta":{"index":0},"_Event":{"height":{"#bigint":"-1"},"name":"Initial","round":{"#bigint":"-1"},"value":"","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"1"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"newRound","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":1},"_Event":{"height":{"#bigint":"1"},"name":"NewRound","round":{"#bigint":"0"},"value":"","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"timeout","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"timeoutPropose","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"1"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"propose","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":2},"_Event":{"height":{"#bigint":"1"},"name":"NewRound","round":{"#bigint":"0"},"value":"","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"timeout","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"timeoutPropose","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"1"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"propose","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":3},"_Event":{"height":{"#bigint":"1"},"name":"Proposal","round":{"#bigint":"0"},"value":"block","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"votemessage","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"1"},"id":"block","round":{"#bigint":"0"},"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":{"#bigint":"1"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"prevote","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":4},"_Event":{"height":{"#bigint":"1"},"name":"Proposal","round":{"#bigint":"0"},"value":"block","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"votemessage","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"1"},"id":"block","round":{"#bigint":"0"},"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":{"#bigint":"1"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"prevote","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":5},"_Event":{"height":{"#bigint":"1"},"name":"ProposalAndPolkaAndValid","round":{"#bigint":"0"},"value":"block","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"votemessage","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"1"},"id":"block","round":{"#bigint":"0"},"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":{"#bigint":"1"},"lockedRound":{"#bigint":"0"},"lockedValue":"block","p":"Josef","round":{"#bigint":"0"},"step":"precommit","validRound":{"#bigint":"0"},"validValue":"block"}]]}},{"#meta":{"index":6},"_Event":{"height":{"#bigint":"1"},"name":"ProposalAndPolkaAndValid","round":{"#bigint":"0"},"value":"block","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"votemessage","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"1"},"id":"block","round":{"#bigint":"0"},"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":{"#bigint":"1"},"lockedRound":{"#bigint":"0"},"lockedValue":"block","p":"Josef","round":{"#bigint":"0"},"step":"precommit","validRound":{"#bigint":"0"},"validValue":"block"}]]}},{"#meta":{"index":7},"_Event":{"height":{"#bigint":"1"},"name":"ProposalAndCommitAndValid","round":{"#bigint":"0"},"value":"block","vr":{"#bigint":"-1"}},"_Result":{"decided":"block","name":"decided","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"1"},"lockedRound":{"#bigint":"0"},"lockedValue":"block","p":"Josef","round":{"#bigint":"0"},"step":"decided","validRound":{"#bigint":"0"},"validValue":"block"}]]}},{"#meta":{"index":8},"_Event":{"height":{"#bigint":"1"},"name":"ProposalAndCommitAndValid","round":{"#bigint":"0"},"value":"block","vr":{"#bigint":"-1"}},"_Result":{"decided":"block","name":"decided","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"1"},"lockedRound":{"#bigint":"0"},"lockedValue":"block","p":"Josef","round":{"#bigint":"0"},"step":"decided","validRound":{"#bigint":"0"},"validValue":"block"}]]}},{"#meta":{"index":9},"_Event":{"height":{"#bigint":"2"},"name":"NewHeight","round":{"#bigint":"0"},"value":"","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"newRound","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":10},"_Event":{"height":{"#bigint":"2"},"name":"NewHeight","round":{"#bigint":"0"},"value":"","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"newRound","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":11},"_Event":{"height":{"#bigint":"2"},"name":"NewRoundProposer","round":{"#bigint":"0"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"proposal","proposal":{"height":{"#bigint":"2"},"proposal":"nextBlock","round":{"#bigint":"0"},"src":"Josef","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"propose","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":12},"_Event":{"height":{"#bigint":"2"},"name":"NewRoundProposer","round":{"#bigint":"0"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"proposal","proposal":{"height":{"#bigint":"2"},"proposal":"nextBlock","round":{"#bigint":"0"},"src":"Josef","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"propose","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":13},"_Event":{"height":{"#bigint":"2"},"name":"Proposal","round":{"#bigint":"0"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"votemessage","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"2"},"id":"nextBlock","round":{"#bigint":"0"},"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"prevote","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":14},"_Event":{"height":{"#bigint":"2"},"name":"Proposal","round":{"#bigint":"0"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"votemessage","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"2"},"id":"nextBlock","round":{"#bigint":"0"},"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"prevote","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":15},"_Event":{"height":{"#bigint":"2"},"name":"PolkaAny","round":{"#bigint":"0"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"timeout","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"timeoutPrevote","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"prevote","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":16},"_Event":{"height":{"#bigint":"2"},"name":"PolkaAny","round":{"#bigint":"0"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"timeout","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"timeoutPrevote","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"prevote","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":17},"_Event":{"height":{"#bigint":"2"},"name":"TimeoutPrevote","round":{"#bigint":"0"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"votemessage","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"2"},"id":"nil","round":{"#bigint":"0"},"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"precommit","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":18},"_Event":{"height":{"#bigint":"2"},"name":"TimeoutPrevote","round":{"#bigint":"0"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"votemessage","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"2"},"id":"nil","round":{"#bigint":"0"},"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"precommit","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":19},"_Event":{"height":{"#bigint":"2"},"name":"PrecommitAny","round":{"#bigint":"0"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"timeout","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"timeoutPrecommit","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"precommit","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":20},"_Event":{"height":{"#bigint":"2"},"name":"PrecommitAny","round":{"#bigint":"0"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"timeout","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"timeoutPrecommit","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"precommit","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":21},"_Event":{"height":{"#bigint":"2"},"name":"TimeoutPrecommit","round":{"#bigint":"0"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"skipRound","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"1"},"timeout":"","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"precommit","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":22},"_Event":{"height":{"#bigint":"2"},"name":"TimeoutPrecommit","round":{"#bigint":"0"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"skipRound","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"1"},"timeout":"","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"0"},"step":"precommit","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":23},"_Event":{"height":{"#bigint":"2"},"name":"NewRound","round":{"#bigint":"1"},"value":"","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"timeout","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"timeoutPropose","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"1"},"step":"propose","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":24},"_Event":{"height":{"#bigint":"2"},"name":"NewRound","round":{"#bigint":"1"},"value":"","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"timeout","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"timeoutPropose","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"1"},"step":"propose","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":25},"_Event":{"height":{"#bigint":"2"},"name":"TimeoutPropose","round":{"#bigint":"1"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"votemessage","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"2"},"id":"nil","round":{"#bigint":"1"},"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"1"},"step":"prevote","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":26},"_Event":{"height":{"#bigint":"2"},"name":"TimeoutPropose","round":{"#bigint":"1"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"votemessage","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"2"},"id":"nil","round":{"#bigint":"1"},"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"1"},"step":"prevote","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":27},"_Event":{"height":{"#bigint":"2"},"name":"PolkaNil","round":{"#bigint":"1"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"votemessage","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"2"},"id":"nil","round":{"#bigint":"1"},"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"1"},"step":"precommit","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":28},"_Event":{"height":{"#bigint":"2"},"name":"PolkaNil","round":{"#bigint":"1"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"votemessage","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"2"},"id":"nil","round":{"#bigint":"1"},"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"1"},"step":"precommit","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":29},"_Event":{"height":{"#bigint":"2"},"name":"PrecommitAny","round":{"#bigint":"1"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"timeout","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"timeoutPrecommit","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"1"},"step":"precommit","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":30},"_Event":{"height":{"#bigint":"2"},"name":"PrecommitAny","round":{"#bigint":"1"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"timeout","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"timeoutPrecommit","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"1"},"step":"precommit","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":31},"_Event":{"height":{"#bigint":"2"},"name":"TimeoutPrecommit","round":{"#bigint":"1"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"skipRound","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"2"},"timeout":"","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"1"},"step":"precommit","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":32},"_Event":{"height":{"#bigint":"2"},"name":"TimeoutPrecommit","round":{"#bigint":"1"},"value":"nextBlock","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"skipRound","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"2"},"timeout":"","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"1"},"step":"precommit","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":33},"_Event":{"height":{"#bigint":"2"},"name":"NewRound","round":{"#bigint":"2"},"value":"","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"timeout","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"timeoutPropose","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"2"},"step":"propose","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":34},"_Event":{"height":{"#bigint":"2"},"name":"NewRound","round":{"#bigint":"2"},"value":"","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"timeout","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"timeoutPropose","voteMessage":{"height":{"#bigint":"-1"},"id":"","round":{"#bigint":"-1"},"src":"","step":""}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"2"},"step":"propose","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}},{"#meta":{"index":35},"_Event":{"height":{"#bigint":"2"},"name":"ProposalInvalid","round":{"#bigint":"2"},"value":"","vr":{"#bigint":"-1"}},"_Result":{"decided":"","name":"votemessage","proposal":{"height":{"#bigint":"-1"},"proposal":"","round":{"#bigint":"-1"},"src":"","validRound":{"#bigint":"-1"}},"skipRound":{"#bigint":"-1"},"timeout":"","voteMessage":{"height":{"#bigint":"2"},"id":"nil","round":{"#bigint":"2"},"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":{"#bigint":"2"},"lockedRound":{"#bigint":"-1"},"lockedValue":"nil","p":"Josef","round":{"#bigint":"2"},"step":"prevote","validRound":{"#bigint":"-1"},"validValue":"nil"}]]}}]} \ No newline at end of file diff --git a/Code/itf/tests/votekeeper/runner.rs b/Code/itf/tests/votekeeper/runner.rs index 482186b7f..781629d1d 100644 --- a/Code/itf/tests/votekeeper/runner.rs +++ b/Code/itf/tests/votekeeper/runner.rs @@ -4,7 +4,7 @@ use malachite_common::{Context, Round, Value}; use malachite_itf::votekeeper::State; use malachite_test::{Address, Height, TestContext, Vote}; use malachite_vote::{ - keeper::{Message, VoteKeeper}, + keeper::{Output, VoteKeeper}, ThresholdParams, }; @@ -18,7 +18,7 @@ pub struct VoteKeeperRunner { impl ItfRunner for VoteKeeperRunner { type ActualState = VoteKeeper; - type Result = Option::Value as Value>::Id>>; + type Result = Option::Value as Value>::Id>>; type ExpectedState = State; type Error = (); @@ -75,21 +75,21 @@ impl ItfRunner for VoteKeeperRunner { // Check result against expected result. match result { Some(result) => match result { - Message::PolkaValue(value) => { + Output::PolkaValue(value) => { assert_eq!(expected_result.name, "PolkaValue"); assert_eq!( value_from_model(&expected_result.value).as_ref(), Some(value) ); } - Message::PrecommitValue(value) => { + Output::PrecommitValue(value) => { assert_eq!(expected_result.name, "PrecommitValue"); assert_eq!( value_from_model(&expected_result.value).as_ref(), Some(value) ); } - Message::SkipRound(round) => { + Output::SkipRound(round) => { assert_eq!(expected_result.name, "Skip"); assert_eq!(&Round::new(expected_result.round), round); } @@ -123,27 +123,27 @@ impl ItfRunner for VoteKeeperRunner { let actual_round = actual_state.per_round().get(&Round::new(round)).unwrap(); - let expected_events = &expected_round.emitted_events; - let actual_events = actual_round.emitted_msgs(); + let expected_outputs = &expected_round.emitted_outputs; + let actual_outputs = actual_round.emitted_outputs(); assert_eq!( - actual_events.len(), - expected_events.len(), + actual_outputs.len(), + expected_outputs.len(), "number of emitted events" ); let mut event_count = HashMap::new(); - for event in expected_events { + for event in expected_outputs { let count = event_count.entry(event.name.clone()).or_insert(0); *count += 1; } - for event in actual_events { + for event in actual_outputs { let event_name = match event { - Message::PolkaValue(_) => "PolkaValue".into(), - Message::PrecommitValue(_) => "PrecommitValue".into(), - Message::SkipRound(_) => "Skip".into(), + Output::PolkaValue(_) => "PolkaValue".into(), + Output::PrecommitValue(_) => "PrecommitValue".into(), + Output::SkipRound(_) => "Skip".into(), _ => format!("{event:?}"), }; let count = event_count.entry(event_name.clone()).or_insert(0); diff --git a/Code/round/src/events.rs b/Code/round/src/events.rs deleted file mode 100644 index 0ea71c90f..000000000 --- a/Code/round/src/events.rs +++ /dev/null @@ -1,25 +0,0 @@ -use malachite_common::{Context, Round, ValueId}; - -#[derive(Clone, Debug, PartialEq, Eq)] -pub enum Event -where - Ctx: Context, -{ - NewRound, // Start a new round, either as proposer or not. L14/L20 - ProposeValue(Ctx::Value), // Propose a value.L14 - Proposal(Ctx::Proposal), // Receive a proposal. L22 + L23 (valid) - InvalidProposal, // Receive an invalid proposal. L26 + L32 (invalid) - ProposalAndPolkaPrevious(Ctx::Proposal), // Received a proposal and a polka value from a previous round. L28 + L29 (valid) - InvalidProposalAndPolkaPrevious(Ctx::Proposal), // Received a proposal and a polka value from a previous round. L28 + L29 (invalid) - PolkaValue(ValueId), // Receive +2/3 prevotes for valueId. L44 - PolkaAny, // Receive +2/3 prevotes for anything. L34 - PolkaNil, // Receive +2/3 prevotes for nil. L44 - ProposalAndPolkaCurrent(Ctx::Proposal), // Receive +2/3 prevotes for Value in current round. L36 - PrecommitAny, // Receive +2/3 precommits for anything. L47 - ProposalAndPrecommitValue(Ctx::Proposal), // Receive +2/3 precommits for Value. L49 - PrecommitValue(ValueId), // Receive +2/3 precommits for ValueId. L51 - SkipRound(Round), // Receive +1/3 messages from a higher round. OneCorrectProcessInHigherRound, L55 - TimeoutPropose, // Timeout waiting for proposal. L57 - TimeoutPrevote, // Timeout waiting for prevotes. L61 - TimeoutPrecommit, // Timeout waiting for precommits. L65 -} diff --git a/Code/round/src/input.rs b/Code/round/src/input.rs new file mode 100644 index 000000000..c095f4dcd --- /dev/null +++ b/Code/round/src/input.rs @@ -0,0 +1,75 @@ +use malachite_common::{Context, Round, ValueId}; + +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum Input +where + Ctx: Context, +{ + /// Start a new round, either as proposer or not. + /// L14/L20 + NewRound, + + /// Propose a value. + /// L14 + ProposeValue(Ctx::Value), + + /// Receive a proposal. + /// L22 + L23 (valid) + Proposal(Ctx::Proposal), + + /// Receive an invalid proposal. + /// L26 + L32 (invalid) + InvalidProposal, + + /// Received a proposal and a polka value from a previous round. + /// L28 + L29 (valid) + ProposalAndPolkaPrevious(Ctx::Proposal), + + /// Received a proposal and a polka value from a previous round. + /// L28 + L29 (invalid) + InvalidProposalAndPolkaPrevious(Ctx::Proposal), + + /// Receive +2/3 prevotes for a value. + /// L44 + PolkaValue(ValueId), + + /// Receive +2/3 prevotes for anything. + /// L34 + PolkaAny, + + /// Receive +2/3 prevotes for nil. + /// L44 + PolkaNil, + + /// Receive +2/3 prevotes for a value in current round. + /// L36 + ProposalAndPolkaCurrent(Ctx::Proposal), + + /// Receive +2/3 precommits for anything. + /// L47 + PrecommitAny, + + /// Receive +2/3 precommits for a value. + /// L49 + ProposalAndPrecommitValue(Ctx::Proposal), + + /// Receive +2/3 precommits for a value. + /// L51 + PrecommitValue(ValueId), + + /// Receive +1/3 messages from a higher round. OneCorrectProcessInHigherRound. + /// L55 + SkipRound(Round), + + /// Timeout waiting for proposal. + /// L57 + TimeoutPropose, + + /// Timeout waiting for prevotes. + /// L61 + TimeoutPrevote, + + /// Timeout waiting for precommits. + /// L65 + TimeoutPrecommit, +} diff --git a/Code/round/src/lib.rs b/Code/round/src/lib.rs index d13887058..33b43bcf6 100644 --- a/Code/round/src/lib.rs +++ b/Code/round/src/lib.rs @@ -14,8 +14,8 @@ extern crate alloc; -pub mod events; -pub mod message; +pub mod input; +pub mod output; pub mod state; pub mod state_machine; pub mod transition; diff --git a/Code/round/src/message.rs b/Code/round/src/output.rs similarity index 50% rename from Code/round/src/message.rs rename to Code/round/src/output.rs index fc5d8f8f5..a7f586015 100644 --- a/Code/round/src/message.rs +++ b/Code/round/src/output.rs @@ -4,7 +4,7 @@ use malachite_common::{Context, Round, Timeout, TimeoutStep, ValueId}; use crate::state::RoundValue; -pub enum Message +pub enum Output where Ctx: Context, { @@ -16,14 +16,14 @@ where Decision(RoundValue), // Decide the value. } -impl Message { +impl Output { pub fn proposal( height: Ctx::Height, round: Round, value: Ctx::Value, pol_round: Round, ) -> Self { - Message::Proposal(Ctx::new_proposal(height, round, value, pol_round)) + Output::Proposal(Ctx::new_proposal(height, round, value, pol_round)) } pub fn prevote( @@ -32,7 +32,7 @@ impl Message { value_id: Option>, address: Ctx::Address, ) -> Self { - Message::Vote(Ctx::new_prevote(height, round, value_id, address)) + Output::Vote(Ctx::new_prevote(height, round, value_id, address)) } pub fn precommit( @@ -41,19 +41,19 @@ impl Message { value_id: Option>, address: Ctx::Address, ) -> Self { - Message::Vote(Ctx::new_precommit(height, round, value_id, address)) + Output::Vote(Ctx::new_precommit(height, round, value_id, address)) } pub fn schedule_timeout(round: Round, step: TimeoutStep) -> Self { - Message::ScheduleTimeout(Timeout { round, step }) + Output::ScheduleTimeout(Timeout { round, step }) } pub fn get_value_and_schedule_timeout(round: Round, step: TimeoutStep) -> Self { - Message::GetValueAndScheduleTimeout(round, Timeout { round, step }) + Output::GetValueAndScheduleTimeout(round, Timeout { round, step }) } pub fn decision(round: Round, value: Ctx::Value) -> Self { - Message::Decision(RoundValue { round, value }) + Output::Decision(RoundValue { round, value }) } } @@ -61,55 +61,55 @@ impl Message { // the compiler would infer a Clone/Debug/PartialEq/Eq bound on `Ctx`, // which may not hold for all contexts. -impl Clone for Message { +impl Clone for Output { #[cfg_attr(coverage_nightly, coverage(off))] fn clone(&self) -> Self { match self { - Message::NewRound(round) => Message::NewRound(*round), - Message::Proposal(proposal) => Message::Proposal(proposal.clone()), - Message::Vote(vote) => Message::Vote(vote.clone()), - Message::ScheduleTimeout(timeout) => Message::ScheduleTimeout(*timeout), - Message::GetValueAndScheduleTimeout(round, timeout) => { - Message::GetValueAndScheduleTimeout(*round, *timeout) + Output::NewRound(round) => Output::NewRound(*round), + Output::Proposal(proposal) => Output::Proposal(proposal.clone()), + Output::Vote(vote) => Output::Vote(vote.clone()), + Output::ScheduleTimeout(timeout) => Output::ScheduleTimeout(*timeout), + Output::GetValueAndScheduleTimeout(round, timeout) => { + Output::GetValueAndScheduleTimeout(*round, *timeout) } - Message::Decision(round_value) => Message::Decision(round_value.clone()), + Output::Decision(round_value) => Output::Decision(round_value.clone()), } } } -impl fmt::Debug for Message { +impl fmt::Debug for Output { #[cfg_attr(coverage_nightly, coverage(off))] fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { - Message::NewRound(round) => write!(f, "NewRound({:?})", round), - Message::Proposal(proposal) => write!(f, "Proposal({:?})", proposal), - Message::Vote(vote) => write!(f, "Vote({:?})", vote), - Message::ScheduleTimeout(timeout) => write!(f, "ScheduleTimeout({:?})", timeout), - Message::GetValueAndScheduleTimeout(round, timeout) => { + Output::NewRound(round) => write!(f, "NewRound({:?})", round), + Output::Proposal(proposal) => write!(f, "Proposal({:?})", proposal), + Output::Vote(vote) => write!(f, "Vote({:?})", vote), + Output::ScheduleTimeout(timeout) => write!(f, "ScheduleTimeout({:?})", timeout), + Output::GetValueAndScheduleTimeout(round, timeout) => { write!(f, "GetValueAndScheduleTimeout({:?}, {:?})", round, timeout) } - Message::Decision(round_value) => write!(f, "Decision({:?})", round_value), + Output::Decision(round_value) => write!(f, "Decision({:?})", round_value), } } } -impl PartialEq for Message { +impl PartialEq for Output { #[cfg_attr(coverage_nightly, coverage(off))] fn eq(&self, other: &Self) -> bool { match (self, other) { - (Message::NewRound(round), Message::NewRound(other_round)) => round == other_round, - (Message::Proposal(proposal), Message::Proposal(other_proposal)) => { + (Output::NewRound(round), Output::NewRound(other_round)) => round == other_round, + (Output::Proposal(proposal), Output::Proposal(other_proposal)) => { proposal == other_proposal } - (Message::Vote(vote), Message::Vote(other_vote)) => vote == other_vote, - (Message::ScheduleTimeout(timeout), Message::ScheduleTimeout(other_timeout)) => { + (Output::Vote(vote), Output::Vote(other_vote)) => vote == other_vote, + (Output::ScheduleTimeout(timeout), Output::ScheduleTimeout(other_timeout)) => { timeout == other_timeout } ( - Message::GetValueAndScheduleTimeout(round, timeout), - Message::GetValueAndScheduleTimeout(other_round, other_timeout), + Output::GetValueAndScheduleTimeout(round, timeout), + Output::GetValueAndScheduleTimeout(other_round, other_timeout), ) => round == other_round && timeout == other_timeout, - (Message::Decision(round_value), Message::Decision(other_round_value)) => { + (Output::Decision(round_value), Output::Decision(other_round_value)) => { round_value == other_round_value } _ => false, @@ -117,4 +117,4 @@ impl PartialEq for Message { } } -impl Eq for Message {} +impl Eq for Output {} diff --git a/Code/round/src/state.rs b/Code/round/src/state.rs index 47148b5fc..4198cee21 100644 --- a/Code/round/src/state.rs +++ b/Code/round/src/state.rs @@ -1,6 +1,6 @@ use core::fmt; -use crate::events::Event; +use crate::input::Input; use crate::state_machine::Info; use crate::transition::Transition; @@ -74,8 +74,8 @@ where } } - pub fn apply_event(self, data: &Info, event: Event) -> Transition { - crate::state_machine::apply_event(self, data, event) + pub fn apply(self, data: &Info, input: Input) -> Transition { + crate::state_machine::apply(self, data, input) } } diff --git a/Code/round/src/state_machine.rs b/Code/round/src/state_machine.rs index ecf1865ca..e4a524fe4 100644 --- a/Code/round/src/state_machine.rs +++ b/Code/round/src/state_machine.rs @@ -1,19 +1,19 @@ use malachite_common::{Context, Proposal, Round, TimeoutStep, Value}; -use crate::events::Event; -use crate::message::Message; +use crate::input::Input; +use crate::output::Output; use crate::state::{State, Step}; use crate::transition::Transition; -/// Immutable information about the event and our node: +/// Immutable information about the input and our node: /// - Address of our node /// - Proposer for the round we are at -/// - Round for which the event is for, can be different than the round we are at +/// - Round for which the input is for, can be different than the round we are at pub struct Info<'a, Ctx> where Ctx: Context, { - pub event_round: Round, + pub input_round: Round, pub address: &'a Ctx::Address, pub proposer: &'a Ctx::Address, } @@ -22,9 +22,9 @@ impl<'a, Ctx> Info<'a, Ctx> where Ctx: Context, { - pub fn new(event_round: Round, address: &'a Ctx::Address, proposer: &'a Ctx::Address) -> Self { + pub fn new(input_round: Round, address: &'a Ctx::Address, proposer: &'a Ctx::Address) -> Self { Self { - event_round, + input_round, address, proposer, } @@ -43,38 +43,38 @@ where pol_round.is_defined() && pol_round < state.round } -/// Apply an event to the current state at the current round. +/// Apply an input to the current state at the current round. /// -/// This function takes the current state and round, and an event, +/// This function takes the current state and round, and an input, /// and returns the next state and an optional message for the driver to act on. /// -/// Valid transitions result in at least a change to the state and/or an output message. +/// 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_event(state: State, info: &Info, event: Event) -> Transition +pub fn apply(state: State, info: &Info, input: Input) -> Transition where Ctx: Context, { - let this_round = state.round == info.event_round; + let this_round = state.round == info.input_round; - match (state.step, event) { - // From NewRound. Event must be for current round. + match (state.step, input) { + // From NewRound. Input must be for current round. // We are the proposer - (Step::NewRound, Event::NewRound) if this_round && info.is_proposer() => { + (Step::NewRound, Input::NewRound) if this_round && info.is_proposer() => { propose_valid_or_get_value(state) // L18 } // We are not the proposer - (Step::NewRound, Event::NewRound) if this_round => schedule_timeout_propose(state), // L11/L20 + (Step::NewRound, Input::NewRound) if this_round => schedule_timeout_propose(state), // L11/L20 - // From Propose. Event must be for current round. - (Step::Propose, Event::ProposeValue(value)) if this_round => { + // From Propose. Input must be for current round. + (Step::Propose, Input::ProposeValue(value)) if this_round => { debug_assert!(info.is_proposer()); propose(state, value) // L11/L14 } // L22 with valid proposal - (Step::Propose, Event::Proposal(proposal)) + (Step::Propose, Input::Proposal(proposal)) if this_round && proposal.pol_round().is_nil() => { if state @@ -89,7 +89,7 @@ where } // L28 with valid proposal - (Step::Propose, Event::ProposalAndPolkaPrevious(proposal)) + (Step::Propose, Input::ProposalAndPolkaPrevious(proposal)) if this_round && is_valid_pol_round(&state, proposal.pol_round()) => { let Some(locked) = state.locked.as_ref() else { @@ -104,32 +104,32 @@ where } // L28 with invalid proposal - (Step::Propose, Event::InvalidProposalAndPolkaPrevious(proposal)) + (Step::Propose, Input::InvalidProposalAndPolkaPrevious(proposal)) if this_round && is_valid_pol_round(&state, proposal.pol_round()) => { prevote_nil(state, info.address) } - (Step::Propose, Event::InvalidProposal) if this_round => prevote_nil(state, info.address), // L22/L25, L28/L31 + (Step::Propose, Input::InvalidProposal) if this_round => prevote_nil(state, info.address), // L22/L25, L28/L31 // We are the proposer. - (Step::Propose, Event::TimeoutPropose) if this_round && info.is_proposer() => { + (Step::Propose, Input::TimeoutPropose) if this_round && info.is_proposer() => { // TODO: Do we need to do something else here? prevote_nil(state, info.address) // L57 } // We are not the proposer. - (Step::Propose, Event::TimeoutPropose) if this_round => prevote_nil(state, info.address), // L57 + (Step::Propose, Input::TimeoutPropose) if this_round => prevote_nil(state, info.address), // L57 - // From Prevote. Event must be for current round. - (Step::Prevote, Event::PolkaAny) if this_round => schedule_timeout_prevote(state), // L34 - (Step::Prevote, Event::PolkaNil) if this_round => precommit_nil(state, info.address), // L44 - (Step::Prevote, Event::ProposalAndPolkaCurrent(proposal)) if this_round => { + // From Prevote. Input must be for current round. + (Step::Prevote, Input::PolkaAny) if this_round => schedule_timeout_prevote(state), // L34 + (Step::Prevote, Input::PolkaNil) if this_round => precommit_nil(state, info.address), // L44 + (Step::Prevote, Input::ProposalAndPolkaCurrent(proposal)) if this_round => { precommit(state, info.address, proposal) // L36/L37 - NOTE: only once? } - (Step::Prevote, Event::TimeoutPrevote) if this_round => precommit_nil(state, info.address), // L61 + (Step::Prevote, Input::TimeoutPrevote) if this_round => precommit_nil(state, info.address), // L61 - // From Precommit. Event must be for current round. - (Step::Precommit, Event::ProposalAndPolkaCurrent(proposal)) if this_round => { + // From Precommit. Input must be for current round. + (Step::Precommit, Input::ProposalAndPolkaCurrent(proposal)) if this_round => { set_valid_value(state, &proposal) // L36/L42 - NOTE: only once? } @@ -137,13 +137,13 @@ where (Step::Commit, _) => Transition::invalid(state), // From all (except Commit). Various round guards. - (_, Event::PrecommitAny) if this_round => schedule_timeout_precommit(state), // L47 - (_, Event::TimeoutPrecommit) if this_round => { - round_skip(state, info.event_round.increment()) + (_, Input::PrecommitAny) if this_round => schedule_timeout_precommit(state), // L47 + (_, Input::TimeoutPrecommit) if this_round => { + round_skip(state, info.input_round.increment()) } // L65 - (_, Event::SkipRound(round)) if state.round < round => round_skip(state, round), // L55 - (_, Event::ProposalAndPrecommitValue(proposal)) => { - commit(state, info.event_round, proposal) + (_, Input::SkipRound(round)) if state.round < round => round_skip(state, round), // L55 + (_, Input::ProposalAndPrecommitValue(proposal)) => { + commit(state, info.input_round, proposal) } // L49 // Invalid transition. @@ -166,18 +166,17 @@ where match &state.valid { Some(round_value) => { let pol_round = round_value.round; - let proposal = Message::proposal( + let proposal = Output::proposal( state.height.clone(), state.round, round_value.value.clone(), pol_round, ); - Transition::to(state.with_step(Step::Propose)).with_message(proposal) + Transition::to(state.with_step(Step::Propose)).with_output(proposal) } None => { - let timeout = - Message::get_value_and_schedule_timeout(state.round, TimeoutStep::Propose); - Transition::to(state.with_step(Step::Propose)).with_message(timeout) + let timeout = Output::get_value_and_schedule_timeout(state.round, TimeoutStep::Propose); + Transition::to(state.with_step(Step::Propose)).with_output(timeout) } } } @@ -190,8 +189,8 @@ pub fn propose(state: State, value: Ctx::Value) -> Transition where Ctx: Context, { - let proposal = Message::proposal(state.height.clone(), state.round, value, Round::Nil); - Transition::to(state.with_step(Step::Propose)).with_message(proposal) + let proposal = Output::proposal(state.height.clone(), state.round, value, Round::Nil); + Transition::to(state.with_step(Step::Propose)).with_output(proposal) } //--------------------------------------------------------------------- @@ -219,9 +218,8 @@ where None => Some(proposed), // not locked, prevote the value }; - let message = Message::prevote(state.height.clone(), state.round, value, address.clone()); - // state.proposal = Some(proposal.clone()); - Transition::to(state.with_step(Step::Prevote)).with_message(message) + let output = Output::prevote(state.height.clone(), state.round, value, address.clone()); + Transition::to(state.with_step(Step::Prevote)).with_output(output) } /// Received a complete proposal for an empty or invalid value, or timed out; prevote nil. @@ -231,8 +229,8 @@ pub fn prevote_nil(state: State, address: &Ctx::Address) -> Transition where Ctx: Context, { - let message = Message::prevote(state.height.clone(), state.round, None, address.clone()); - Transition::to(state.with_step(Step::Prevote)).with_message(message) + let output = Output::prevote(state.height.clone(), state.round, None, address.clone()); + Transition::to(state.with_step(Step::Prevote)).with_output(output) } // --------------------------------------------------------------------- @@ -258,7 +256,7 @@ where } let value = proposal.value(); - let message = Message::precommit( + let output = Output::precommit( state.height.clone(), state.round, Some(value.id()), @@ -280,7 +278,7 @@ where .set_valid(value.clone()) .with_step(Step::Precommit); - Transition::to(next).with_message(message) + Transition::to(next).with_output(output) } /// Received a polka for nil or timed out of prevote; precommit nil. @@ -290,8 +288,8 @@ pub fn precommit_nil(state: State, address: &Ctx::Address) -> Transiti where Ctx: Context, { - let message = Message::precommit(state.height.clone(), state.round, None, address.clone()); - Transition::to(state.with_step(Step::Precommit)).with_message(message) + let output = Output::precommit(state.height.clone(), state.round, None, address.clone()); + Transition::to(state.with_step(Step::Precommit)).with_output(output) } // --------------------------------------------------------------------- @@ -305,8 +303,8 @@ pub fn schedule_timeout_propose(state: State) -> Transition where Ctx: Context, { - let timeout = Message::schedule_timeout(state.round, TimeoutStep::Propose); - Transition::to(state.with_step(Step::Propose)).with_message(timeout) + let timeout = Output::schedule_timeout(state.round, TimeoutStep::Propose); + Transition::to(state.with_step(Step::Propose)).with_output(timeout) } /// We received a polka for any; schedule timeout prevote. @@ -320,8 +318,8 @@ where Ctx: Context, { if state.step == Step::Prevote { - let message = Message::schedule_timeout(state.round, TimeoutStep::Prevote); - Transition::to(state).with_message(message) + let output = Output::schedule_timeout(state.round, TimeoutStep::Prevote); + Transition::to(state).with_output(output) } else { Transition::to(state) } @@ -334,8 +332,8 @@ pub fn schedule_timeout_precommit(state: State) -> Transition where Ctx: Context, { - let message = Message::schedule_timeout(state.round, TimeoutStep::Precommit); - Transition::to(state).with_message(message) + let output = Output::schedule_timeout(state.round, TimeoutStep::Precommit); + Transition::to(state).with_output(output) } //--------------------------------------------------------------------- @@ -374,7 +372,7 @@ where ..state }; - Transition::to(new_state).with_message(Message::NewRound(round)) + Transition::to(new_state).with_output(Output::NewRound(round)) } /// We received +2/3 precommits for a value - commit and decide that value! @@ -384,6 +382,6 @@ pub fn commit(state: State, round: Round, proposal: Ctx::Proposal) -> where Ctx: Context, { - let message = Message::decision(round, proposal.value().clone()); - Transition::to(state.with_step(Step::Commit)).with_message(message) + let output = Output::decision(round, proposal.value().clone()); + Transition::to(state.with_step(Step::Commit)).with_output(output) } diff --git a/Code/round/src/transition.rs b/Code/round/src/transition.rs index 33bed24fb..5d28df5b0 100644 --- a/Code/round/src/transition.rs +++ b/Code/round/src/transition.rs @@ -1,6 +1,6 @@ use malachite_common::Context; -use crate::message::Message; +use crate::output::Output; use crate::state::State; #[derive(Clone, Debug, PartialEq, Eq)] @@ -9,7 +9,7 @@ where Ctx: Context, { pub next_state: State, - pub message: Option>, + pub output: Option>, pub valid: bool, } @@ -20,7 +20,7 @@ where pub fn to(next_state: State) -> Self { Self { next_state, - message: None, + output: None, valid: true, } } @@ -28,13 +28,13 @@ where pub fn invalid(next_state: State) -> Self { Self { next_state, - message: None, + output: None, valid: false, } } - pub fn with_message(mut self, message: Message) -> Self { - self.message = Some(message); + pub fn with_output(mut self, output: Output) -> Self { + self.output = Some(output); self } } diff --git a/Code/test/src/utils.rs b/Code/test/src/utils.rs index 0008f3483..31c405ee5 100644 --- a/Code/test/src/utils.rs +++ b/Code/test/src/utils.rs @@ -2,7 +2,7 @@ use rand::rngs::StdRng; use rand::SeedableRng; use malachite_common::{Round, Timeout, VotingPower}; -use malachite_driver::{Event, Message, ProposerSelector, Validity}; +use malachite_driver::{Input, Output, ProposerSelector, Validity}; use malachite_round::state::{RoundValue, State, Step}; use crate::{ @@ -52,117 +52,121 @@ pub fn make_validators( validators.try_into().expect("N validators") } -pub fn new_round_event(round: Round) -> Event { - Event::NewRound(Height::new(1), round) +pub fn new_round_input(round: Round) -> Input { + Input::NewRound(Height::new(1), round) } -pub fn new_round_msg(round: Round) -> Option> { - Some(Message::NewRound(Height::new(1), round)) +pub fn new_round_output(round: Round) -> Option> { + Some(Output::NewRound(Height::new(1), round)) } -pub fn proposal_msg( +pub fn proposal_output( round: Round, value: Value, locked_round: Round, -) -> Option> { +) -> Option> { let proposal = Proposal::new(Height::new(1), round, value, locked_round); - Some(Message::Propose(proposal)) + Some(Output::Propose(proposal)) } -pub fn proposal_event( +pub fn proposal_input( round: Round, value: Value, locked_round: Round, validity: Validity, -) -> Event { +) -> Input { let proposal = Proposal::new(Height::new(1), round, value, locked_round); - Event::Proposal(proposal, validity) + Input::Proposal(proposal, validity) } -pub fn prevote_msg(round: Round, addr: &Address, sk: &PrivateKey) -> Option> { +pub fn prevote_output( + round: Round, + addr: &Address, + sk: &PrivateKey, +) -> Option> { let value = Value::new(9999); - Some(Message::Vote( + Some(Output::Vote( Vote::new_prevote(Height::new(1), round, Some(value.id()), *addr).signed(sk), )) } -pub fn prevote_nil_msg( +pub fn prevote_nil_output( round: Round, addr: &Address, sk: &PrivateKey, -) -> Option> { - Some(Message::Vote( +) -> Option> { + Some(Output::Vote( Vote::new_prevote(Height::new(1), round, None, *addr).signed(sk), )) } -pub fn prevote_event(addr: &Address, sk: &PrivateKey) -> Event { +pub fn prevote_input(addr: &Address, sk: &PrivateKey) -> Input { let value = Value::new(9999); - Event::Vote( + Input::Vote( Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), *addr).signed(sk), ) } -pub fn prevote_event_at(round: Round, addr: &Address, sk: &PrivateKey) -> Event { +pub fn prevote_input_at(round: Round, addr: &Address, sk: &PrivateKey) -> Input { let value = Value::new(9999); - Event::Vote(Vote::new_prevote(Height::new(1), round, Some(value.id()), *addr).signed(sk)) + Input::Vote(Vote::new_prevote(Height::new(1), round, Some(value.id()), *addr).signed(sk)) } -pub fn precommit_msg( +pub fn precommit_output( round: Round, value: Value, addr: &Address, sk: &PrivateKey, -) -> Option> { - Some(Message::Vote( +) -> Option> { + Some(Output::Vote( Vote::new_precommit(Height::new(1), round, Some(value.id()), *addr).signed(sk), )) } -pub fn precommit_nil_msg(addr: &Address, sk: &PrivateKey) -> Option> { - Some(Message::Vote( +pub fn precommit_nil_output(addr: &Address, sk: &PrivateKey) -> Option> { + Some(Output::Vote( Vote::new_precommit(Height::new(1), Round::new(0), None, *addr).signed(sk), )) } -pub fn precommit_event( +pub fn precommit_input( round: Round, value: Value, addr: &Address, sk: &PrivateKey, -) -> Event { - Event::Vote(Vote::new_precommit(Height::new(1), round, Some(value.id()), *addr).signed(sk)) +) -> Input { + Input::Vote(Vote::new_precommit(Height::new(1), round, Some(value.id()), *addr).signed(sk)) } -pub fn decide_message(round: Round, value: Value) -> Option> { - Some(Message::Decide(round, value)) +pub fn decide_output(round: Round, value: Value) -> Option> { + Some(Output::Decide(round, value)) } -pub fn start_propose_timer_msg(round: Round) -> Option> { - Some(Message::ScheduleTimeout(Timeout::propose(round))) +pub fn start_propose_timer_output(round: Round) -> Option> { + Some(Output::ScheduleTimeout(Timeout::propose(round))) } -pub fn timeout_propose_event(round: Round) -> Event { - Event::TimeoutElapsed(Timeout::propose(round)) +pub fn timeout_propose_input(round: Round) -> Input { + Input::TimeoutElapsed(Timeout::propose(round)) } -pub fn start_prevote_timer_msg(round: Round) -> Option> { - Some(Message::ScheduleTimeout(Timeout::prevote(round))) +pub fn start_prevote_timer_output(round: Round) -> Option> { + Some(Output::ScheduleTimeout(Timeout::prevote(round))) } -pub fn timeout_prevote_event(round: Round) -> Event { - Event::TimeoutElapsed(Timeout::prevote(round)) +pub fn timeout_prevote_input(round: Round) -> Input { + Input::TimeoutElapsed(Timeout::prevote(round)) } -pub fn start_precommit_timer_msg(round: Round) -> Option> { - Some(Message::ScheduleTimeout(Timeout::precommit(round))) +pub fn start_precommit_timer_output(round: Round) -> Option> { + Some(Output::ScheduleTimeout(Timeout::precommit(round))) } -pub fn timeout_precommit_event(round: Round) -> Event { - Event::TimeoutElapsed(Timeout::precommit(round)) +pub fn timeout_precommit_input(round: Round) -> Input { + Input::TimeoutElapsed(Timeout::precommit(round)) } pub fn propose_state(round: Round) -> State { diff --git a/Code/test/tests/driver.rs b/Code/test/tests/driver.rs index 7e2d06dcd..578097a55 100644 --- a/Code/test/tests/driver.rs +++ b/Code/test/tests/driver.rs @@ -2,27 +2,27 @@ use futures::executor::block_on; use malachite_test::utils::{make_validators, FixedProposer, RotateProposer}; use malachite_common::{Round, Timeout, TimeoutStep}; -use malachite_driver::{Driver, Error, Event, Message, Validity}; +use malachite_driver::{Driver, Error, Input, Output, Validity}; use malachite_round::state::{RoundValue, State, Step}; use malachite_test::{Height, Proposal, TestContext, ValidatorSet, Value, Vote}; pub struct TestStep { desc: &'static str, - input_event: Option>, - expected_output: Option>, + input: Option>, + expected_output: Option>, expected_round: Round, new_state: State, } -pub fn msg_to_event(output: Message) -> Option> { +pub fn output_to_input(output: Output) -> Option> { match output { - Message::NewRound(height, round) => Some(Event::NewRound(height, round)), + Output::NewRound(height, round) => Some(Input::NewRound(height, round)), // Let's consider our own proposal to always be valid - Message::Propose(p) => Some(Event::Proposal(p, Validity::Valid)), - Message::Vote(v) => Some(Event::Vote(v)), - Message::Decide(_, _) => None, - Message::ScheduleTimeout(_) => None, - Message::GetValueAndScheduleTimeout(_, _) => None, + Output::Propose(p) => Some(Input::Proposal(p, Validity::Valid)), + Output::Vote(v) => Some(Input::Vote(v)), + Output::Decide(_, _) => None, + Output::ScheduleTimeout(_) => None, + Output::GetValueAndScheduleTimeout(_, _) => None, } } @@ -44,8 +44,8 @@ fn driver_steps_proposer() { let steps = vec![ TestStep { desc: "Start round 0, we are proposer, ask for a value to propose", - input_event: Some(Event::NewRound(Height::new(1), Round::new(0))), - expected_output: Some(Message::GetValueAndScheduleTimeout( + input: Some(Input::NewRound(Height::new(1), Round::new(0))), + expected_output: Some(Output::GetValueAndScheduleTimeout( Round::new(0), Timeout::new(Round::new(0), TimeoutStep::Propose), )), @@ -61,8 +61,8 @@ fn driver_steps_proposer() { }, TestStep { desc: "Feed a value to propose, propose that value", - input_event: Some(Event::ProposeValue(Round::new(0), value)), - expected_output: Some(Message::Propose(proposal.clone())), + input: Some(Input::ProposeValue(Round::new(0), value)), + expected_output: Some(Output::Propose(proposal.clone())), expected_round: Round::new(0), new_state: State { height: Height::new(1), @@ -75,8 +75,8 @@ fn driver_steps_proposer() { }, TestStep { desc: "Receive our own proposal, prevote for it (v1)", - input_event: None, - expected_output: Some(Message::Vote( + input: None, + expected_output: Some(Output::Vote( Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), my_addr) .signed(&my_sk), )), @@ -92,7 +92,7 @@ fn driver_steps_proposer() { }, TestStep { desc: "Receive our own prevote v1", - input_event: None, + input: None, expected_output: None, expected_round: Round::new(0), new_state: State { @@ -106,7 +106,7 @@ fn driver_steps_proposer() { }, TestStep { desc: "v2 prevotes for our proposal", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), v2.address) .signed(&sk2), )), @@ -123,11 +123,11 @@ fn driver_steps_proposer() { }, TestStep { desc: "v3 prevotes for our proposal, we get +2/3 prevotes, precommit for it (v1)", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), v3.address) .signed(&sk3), )), - expected_output: Some(Message::Vote( + expected_output: Some(Output::Vote( Vote::new_precommit(Height::new(1), Round::new(0), Some(value.id()), my_addr) .signed(&my_sk), )), @@ -149,7 +149,7 @@ fn driver_steps_proposer() { }, TestStep { desc: "v1 receives its own precommit", - input_event: None, + input: None, expected_output: None, expected_round: Round::new(0), new_state: State { @@ -169,7 +169,7 @@ fn driver_steps_proposer() { }, TestStep { desc: "v2 precommits for our proposal", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_precommit(Height::new(1), Round::new(0), Some(value.id()), v2.address) .signed(&sk2), )), @@ -192,11 +192,11 @@ fn driver_steps_proposer() { }, TestStep { desc: "v3 precommits for our proposal, we get +2/3 precommits, decide it (v1)", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_precommit(Height::new(1), Round::new(0), Some(value.id()), v3.address) .signed(&sk3), )), - expected_output: Some(Message::Decide(Round::new(0), value)), + expected_output: Some(Output::Decide(Round::new(0), value)), expected_round: Round::new(0), new_state: State { height: Height::new(1), @@ -215,17 +215,17 @@ fn driver_steps_proposer() { }, ]; - let mut event_from_previous_msg = None; + let mut output_from_prev_input = None; for step in steps { println!("Step: {}", step.desc); - let execute_event = step - .input_event - .unwrap_or_else(|| event_from_previous_msg.unwrap()); + let input = step + .input + .unwrap_or_else(|| output_from_prev_input.unwrap()); - let output = block_on(driver.execute(execute_event)).expect("execute succeeded"); - assert_eq!(output, step.expected_output, "expected output message"); + let output = block_on(driver.execute(input)).expect("execute succeeded"); + assert_eq!(output, step.expected_output, "expected output"); assert_eq!( driver.round_state.round, step.expected_round, @@ -234,7 +234,7 @@ fn driver_steps_proposer() { assert_eq!(driver.round_state, step.new_state, "expected state"); - event_from_previous_msg = output.and_then(msg_to_event); + output_from_prev_input = output.and_then(output_to_input); } } @@ -252,8 +252,8 @@ fn driver_steps_proposer_timeout_get_value() { let steps = vec![ TestStep { desc: "Start round 0, we are proposer, ask for a value to propose", - input_event: Some(Event::NewRound(Height::new(1), Round::new(0))), - expected_output: Some(Message::GetValueAndScheduleTimeout( + input: Some(Input::NewRound(Height::new(1), Round::new(0))), + expected_output: Some(Output::GetValueAndScheduleTimeout( Round::new(0), Timeout::new(Round::new(0), TimeoutStep::Propose), )), @@ -269,8 +269,8 @@ fn driver_steps_proposer_timeout_get_value() { }, TestStep { desc: "Receive a propose timeout", - input_event: Some(Event::TimeoutElapsed(Timeout::propose(Round::new(0)))), - expected_output: Some(Message::Vote( + input: Some(Input::TimeoutElapsed(Timeout::propose(Round::new(0)))), + expected_output: Some(Output::Vote( Vote::new_prevote(Height::new(1), Round::new(0), None, my_addr).signed(&my_sk), )), expected_round: Round::new(0), @@ -285,17 +285,17 @@ fn driver_steps_proposer_timeout_get_value() { }, ]; - let mut event_from_previous_msg = None; + let mut output_from_prev_input = None; for step in steps { println!("Step: {}", step.desc); - let execute_event = step - .input_event - .unwrap_or_else(|| event_from_previous_msg.unwrap()); + let input = step + .input + .unwrap_or_else(|| output_from_prev_input.unwrap()); - let output = block_on(driver.execute(execute_event)).expect("execute succeeded"); - assert_eq!(output, step.expected_output, "expected output message"); + let output = block_on(driver.execute(input)).expect("execute succeeded"); + assert_eq!(output, step.expected_output, "expected output"); assert_eq!( driver.round_state.round, step.expected_round, @@ -304,7 +304,7 @@ fn driver_steps_proposer_timeout_get_value() { assert_eq!(driver.round_state, step.new_state, "expected state"); - event_from_previous_msg = output.and_then(msg_to_event); + output_from_prev_input = output.and_then(output_to_input); } } @@ -328,8 +328,8 @@ fn driver_steps_not_proposer_valid() { let steps = vec![ TestStep { desc: "Start round 0, we are not the proposer", - input_event: Some(Event::NewRound(Height::new(1), Round::new(0))), - expected_output: Some(Message::ScheduleTimeout(Timeout::propose(Round::new(0)))), + input: Some(Input::NewRound(Height::new(1), Round::new(0))), + expected_output: Some(Output::ScheduleTimeout(Timeout::propose(Round::new(0)))), expected_round: Round::new(0), new_state: State { height: Height::new(1), @@ -342,8 +342,8 @@ fn driver_steps_not_proposer_valid() { }, TestStep { desc: "Receive a proposal, prevote for it (v2)", - input_event: Some(Event::Proposal(proposal.clone(), Validity::Valid)), - expected_output: Some(Message::Vote( + input: Some(Input::Proposal(proposal.clone(), Validity::Valid)), + expected_output: Some(Output::Vote( Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), my_addr) .signed(&my_sk), )), @@ -359,7 +359,7 @@ fn driver_steps_not_proposer_valid() { }, TestStep { desc: "Receive our own prevote (v2)", - input_event: None, + input: None, expected_output: None, expected_round: Round::new(0), new_state: State { @@ -373,7 +373,7 @@ fn driver_steps_not_proposer_valid() { }, TestStep { desc: "v1 prevotes for its own proposal", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), v1.address) .signed(&sk1), )), @@ -390,11 +390,11 @@ fn driver_steps_not_proposer_valid() { }, TestStep { desc: "v3 prevotes for v1's proposal, it gets +2/3 prevotes, precommit for it (v2)", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), v3.address) .signed(&sk3), )), - expected_output: Some(Message::Vote( + expected_output: Some(Output::Vote( Vote::new_precommit(Height::new(1), Round::new(0), Some(value.id()), my_addr) .signed(&my_sk), )), @@ -416,7 +416,7 @@ fn driver_steps_not_proposer_valid() { }, TestStep { desc: "we receive our own precommit", - input_event: None, + input: None, expected_output: None, expected_round: Round::new(0), new_state: State { @@ -436,7 +436,7 @@ fn driver_steps_not_proposer_valid() { }, TestStep { desc: "v1 precommits its proposal", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_precommit(Height::new(1), Round::new(0), Some(value.id()), v1.address) .signed(&sk1), )), @@ -459,11 +459,11 @@ fn driver_steps_not_proposer_valid() { }, TestStep { desc: "v3 precommits for v1's proposal, it gets +2/3 precommits, decide it", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_precommit(Height::new(1), Round::new(0), Some(value.id()), v3.address) .signed(&sk3), )), - expected_output: Some(Message::Decide(Round::new(0), value)), + expected_output: Some(Output::Decide(Round::new(0), value)), expected_round: Round::new(0), new_state: State { height: Height::new(1), @@ -482,17 +482,17 @@ fn driver_steps_not_proposer_valid() { }, ]; - let mut event_from_previous_msg = None; + let mut output_from_prev_input = None; for step in steps { println!("Step: {}", step.desc); - let execute_event = step - .input_event - .unwrap_or_else(|| event_from_previous_msg.unwrap()); + let input = step + .input + .unwrap_or_else(|| output_from_prev_input.unwrap()); - let output = block_on(driver.execute(execute_event)).expect("execute succeeded"); - assert_eq!(output, step.expected_output, "expected output message"); + let output = block_on(driver.execute(input)).expect("execute succeeded"); + assert_eq!(output, step.expected_output, "expected output"); assert_eq!( driver.round_state.round, step.expected_round, @@ -501,7 +501,7 @@ fn driver_steps_not_proposer_valid() { assert_eq!(driver.round_state, step.new_state, "expected state"); - event_from_previous_msg = output.and_then(msg_to_event); + output_from_prev_input = output.and_then(output_to_input); } } @@ -525,8 +525,8 @@ fn driver_steps_not_proposer_invalid() { let steps = vec![ TestStep { desc: "Start round 0, we are not the proposer", - input_event: Some(Event::NewRound(Height::new(1), Round::new(0))), - expected_output: Some(Message::ScheduleTimeout(Timeout::propose(Round::new(0)))), + input: Some(Input::NewRound(Height::new(1), Round::new(0))), + expected_output: Some(Output::ScheduleTimeout(Timeout::propose(Round::new(0)))), expected_round: Round::new(0), new_state: State { height: Height::new(1), @@ -539,8 +539,8 @@ fn driver_steps_not_proposer_invalid() { }, TestStep { desc: "Receive an invalid proposal, prevote for nil (v2)", - input_event: Some(Event::Proposal(proposal.clone(), Validity::Invalid)), - expected_output: Some(Message::Vote( + input: Some(Input::Proposal(proposal.clone(), Validity::Invalid)), + expected_output: Some(Output::Vote( Vote::new_prevote(Height::new(1),Round::new(0), None, my_addr).signed(&my_sk), )), expected_round: Round::new(0), @@ -555,7 +555,7 @@ fn driver_steps_not_proposer_invalid() { }, TestStep { desc: "Receive our own prevote (v2)", - input_event: None, + input: None, expected_output: None, expected_round: Round::new(0), new_state: State { @@ -569,7 +569,7 @@ fn driver_steps_not_proposer_invalid() { }, TestStep { desc: "v1 prevotes for its own proposal", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), v1.address).signed(&sk1), )), expected_output: None, @@ -585,10 +585,10 @@ fn driver_steps_not_proposer_invalid() { }, TestStep { desc: "v3 prevotes for v1's proposal, we have polka for any, schedule prevote timeout (v2)", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), v3.address).signed(&sk3), )), - expected_output: Some(Message::ScheduleTimeout(Timeout::prevote(Round::new(0)))), + expected_output: Some(Output::ScheduleTimeout(Timeout::prevote(Round::new(0)))), expected_round: Round::new(0), new_state: State { height: Height::new(1), @@ -601,8 +601,8 @@ fn driver_steps_not_proposer_invalid() { }, TestStep { desc: "prevote timeout elapses, we precommit for nil (v2)", - input_event: Some(Event::TimeoutElapsed(Timeout::prevote(Round::new(0)))), - expected_output: Some(Message::Vote( + input: Some(Input::TimeoutElapsed(Timeout::prevote(Round::new(0)))), + expected_output: Some(Output::Vote( Vote::new_precommit(Height::new(1), Round::new(0), None, my_addr).signed(&my_sk), )), expected_round: Round::new(0), @@ -617,16 +617,16 @@ fn driver_steps_not_proposer_invalid() { }, ]; - let mut event_from_previous_msg = None; + let mut output_from_prev_input = None; for step in steps { println!("Step: {}", step.desc); - let execute_event = step - .input_event - .unwrap_or_else(|| event_from_previous_msg.unwrap()); + let input = step + .input + .unwrap_or_else(|| output_from_prev_input.unwrap()); - let output = block_on(driver.execute(execute_event)).expect("execute succeeded"); + let output = block_on(driver.execute(input)).expect("execute succeeded"); assert_eq!(output, step.expected_output, "expected output"); assert_eq!( @@ -636,7 +636,7 @@ fn driver_steps_not_proposer_invalid() { assert_eq!(driver.round_state, step.new_state, "expected state"); - event_from_previous_msg = output.and_then(msg_to_event); + output_from_prev_input = output.and_then(output_to_input); } } @@ -661,8 +661,8 @@ fn driver_steps_not_proposer_other_height() { let steps = vec![ TestStep { desc: "Start round 0, we are not the proposer", - input_event: Some(Event::NewRound(Height::new(1), Round::new(0))), - expected_output: Some(Message::ScheduleTimeout(Timeout::propose(Round::new(0)))), + input: Some(Input::NewRound(Height::new(1), Round::new(0))), + expected_output: Some(Output::ScheduleTimeout(Timeout::propose(Round::new(0)))), expected_round: Round::new(0), new_state: State { height: Height::new(1), @@ -675,7 +675,7 @@ fn driver_steps_not_proposer_other_height() { }, TestStep { desc: "Receive a proposal for another height, ignore it (v2)", - input_event: Some(Event::Proposal(proposal.clone(), Validity::Invalid)), + input: Some(Input::Proposal(proposal.clone(), Validity::Invalid)), expected_output: None, expected_round: Round::new(0), new_state: State { @@ -689,16 +689,16 @@ fn driver_steps_not_proposer_other_height() { }, ]; - let mut event_from_previous_msg = None; + let mut output_from_prev_input = None; for step in steps { println!("Step: {}", step.desc); - let execute_event = step - .input_event - .unwrap_or_else(|| event_from_previous_msg.unwrap()); + let input = step + .input + .unwrap_or_else(|| output_from_prev_input.unwrap()); - let output = block_on(driver.execute(execute_event)).expect("execute succeeded"); + let output = block_on(driver.execute(input)).expect("execute succeeded"); assert_eq!(output, step.expected_output, "expected output"); assert_eq!( @@ -708,7 +708,7 @@ fn driver_steps_not_proposer_other_height() { assert_eq!(driver.round_state, step.new_state, "expected state"); - event_from_previous_msg = output.and_then(msg_to_event); + output_from_prev_input = output.and_then(output_to_input); } } @@ -733,8 +733,8 @@ fn driver_steps_not_proposer_other_round() { let steps = vec![ TestStep { desc: "Start round 0, we are not the proposer", - input_event: Some(Event::NewRound(Height::new(1), Round::new(0))), - expected_output: Some(Message::ScheduleTimeout(Timeout::propose(Round::new(0)))), + input: Some(Input::NewRound(Height::new(1), Round::new(0))), + expected_output: Some(Output::ScheduleTimeout(Timeout::propose(Round::new(0)))), expected_round: Round::new(0), new_state: State { height: Height::new(1), @@ -747,7 +747,7 @@ fn driver_steps_not_proposer_other_round() { }, TestStep { desc: "Receive a proposal for another round, ignore it (v2)", - input_event: Some(Event::Proposal(proposal.clone(), Validity::Invalid)), + input: Some(Input::Proposal(proposal.clone(), Validity::Invalid)), expected_output: None, expected_round: Round::new(0), new_state: State { @@ -761,16 +761,16 @@ fn driver_steps_not_proposer_other_round() { }, ]; - let mut event_from_previous_msg = None; + let mut output_from_prev_input = None; for step in steps { println!("Step: {}", step.desc); - let execute_event = step - .input_event - .unwrap_or_else(|| event_from_previous_msg.unwrap()); + let input = step + .input + .unwrap_or_else(|| output_from_prev_input.unwrap()); - let output = block_on(driver.execute(execute_event)).expect("execute succeeded"); + let output = block_on(driver.execute(input)).expect("execute succeeded"); assert_eq!(output, step.expected_output, "expected output"); assert_eq!( @@ -780,7 +780,7 @@ fn driver_steps_not_proposer_other_round() { assert_eq!(driver.round_state, step.new_state, "expected state"); - event_from_previous_msg = output.and_then(msg_to_event); + output_from_prev_input = output.and_then(output_to_input); } } @@ -803,8 +803,8 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { // Start round 0, we, v3, are not the proposer TestStep { desc: "Start round 0, we, v3, are not the proposer", - input_event: Some(Event::NewRound(Height::new(1), Round::new(0))), - expected_output: Some(Message::ScheduleTimeout(Timeout::propose(Round::new(0)))), + input: Some(Input::NewRound(Height::new(1), Round::new(0))), + expected_output: Some(Output::ScheduleTimeout(Timeout::propose(Round::new(0)))), expected_round: Round::new(0), new_state: State { height: Height::new(1), @@ -818,8 +818,8 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { // Receive a propose timeout, prevote for nil (from v3) TestStep { desc: "Receive a propose timeout, prevote for nil (v3)", - input_event: Some(Event::TimeoutElapsed(Timeout::propose(Round::new(0)))), - expected_output: Some(Message::Vote( + input: Some(Input::TimeoutElapsed(Timeout::propose(Round::new(0)))), + expected_output: Some(Output::Vote( Vote::new_prevote(Height::new(1), Round::new(0), None, my_addr).signed(&my_sk), )), expected_round: Round::new(0), @@ -835,7 +835,7 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { // Receive our own prevote v3 TestStep { desc: "Receive our own prevote v3", - input_event: None, + input: None, expected_output: None, expected_round: Round::new(0), new_state: State { @@ -850,7 +850,7 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { // v1 prevotes for its own proposal TestStep { desc: "v1 prevotes for its own proposal", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), v1.address) .signed(&sk1), )), @@ -868,10 +868,10 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { // v2 prevotes for nil, we get +2/3 nil prevotes and precommit for nil TestStep { desc: "v2 prevotes for nil, we get +2/3 prevotes, precommit for nil", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_prevote(Height::new(1), Round::new(0), None, v2.address).signed(&sk2), )), - expected_output: Some(Message::Vote( + expected_output: Some(Output::Vote( Vote::new_precommit(Height::new(1), Round::new(0), None, my_addr).signed(&my_sk), )), expected_round: Round::new(0), @@ -887,7 +887,7 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { // v3 receives its own precommit TestStep { desc: "v3 receives its own precommit", - input_event: None, + input: None, expected_output: None, expected_round: Round::new(0), new_state: State { @@ -902,7 +902,7 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { // v1 precommits its proposal TestStep { desc: "v1 precommits its proposal", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_precommit(Height::new(1), Round::new(0), Some(value.id()), v1.address) .signed(&sk1), )), @@ -920,10 +920,10 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { // v2 precommits for nil TestStep { desc: "v2 precommits for nil", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_precommit(Height::new(1), Round::new(0), None, v2.address).signed(&sk2), )), - expected_output: Some(Message::ScheduleTimeout(Timeout::precommit(Round::new(0)))), + expected_output: Some(Output::ScheduleTimeout(Timeout::precommit(Round::new(0)))), expected_round: Round::new(0), new_state: State { height: Height::new(1), @@ -937,8 +937,8 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { // we receive a precommit timeout, start a new round TestStep { desc: "we receive a precommit timeout, start a new round", - input_event: Some(Event::TimeoutElapsed(Timeout::precommit(Round::new(0)))), - expected_output: Some(Message::NewRound(Height::new(1), Round::new(1))), + input: Some(Input::TimeoutElapsed(Timeout::precommit(Round::new(0)))), + expected_output: Some(Output::NewRound(Height::new(1), Round::new(1))), expected_round: Round::new(0), new_state: State { height: Height::new(1), @@ -951,8 +951,8 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { }, TestStep { desc: "Start round 1, we are not the proposer", - input_event: Some(Event::NewRound(Height::new(1), Round::new(1))), - expected_output: Some(Message::ScheduleTimeout(Timeout::propose(Round::new(1)))), + input: Some(Input::NewRound(Height::new(1), Round::new(1))), + expected_output: Some(Output::ScheduleTimeout(Timeout::propose(Round::new(1)))), expected_round: Round::new(1), new_state: State { height: Height::new(1), @@ -965,21 +965,21 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { }, ]; - let mut event_from_previous_msg = None; + let mut output_from_prev_input = None; for step in steps { println!("Step: {}", step.desc); - let execute_event = step - .input_event - .unwrap_or_else(|| event_from_previous_msg.unwrap()); + let input = step + .input + .unwrap_or_else(|| output_from_prev_input.unwrap()); - let output = block_on(driver.execute(execute_event)).expect("execute succeeded"); - assert_eq!(output, step.expected_output, "expected output message"); + let output = block_on(driver.execute(input)).expect("execute succeeded"); + assert_eq!(output, step.expected_output, "expected output"); assert_eq!(driver.round_state, step.new_state, "new state"); - event_from_previous_msg = output.and_then(msg_to_event); + output_from_prev_input = output.and_then(output_to_input); } } @@ -996,12 +996,12 @@ fn driver_steps_no_value_to_propose() { let mut driver = Driver::new(ctx, sel, vs, my_addr); - let output = block_on(driver.execute(Event::NewRound(Height::new(1), Round::new(0)))) + let output = block_on(driver.execute(Input::NewRound(Height::new(1), Round::new(0)))) .expect("execute succeeded"); assert_eq!( output, - Some(Message::GetValueAndScheduleTimeout( + Some(Output::GetValueAndScheduleTimeout( Round::new(0), Timeout::propose(Round::new(0)) )) @@ -1022,7 +1022,7 @@ fn driver_steps_proposer_not_found() { let mut driver = Driver::new(ctx, sel, vs, my_addr); - let output = block_on(driver.execute(Event::NewRound(Height::new(1), Round::new(0)))); + let output = block_on(driver.execute(Input::NewRound(Height::new(1), Round::new(0)))); assert_eq!(output, Err(Error::ProposerNotFound(v1.address))); } @@ -1043,11 +1043,11 @@ fn driver_steps_validator_not_found() { let mut driver = Driver::new(ctx, sel, vs, my_addr); // Start new height - block_on(driver.execute(Event::NewRound(Height::new(1), Round::new(0)))) + block_on(driver.execute(Input::NewRound(Height::new(1), Round::new(0)))) .expect("execute succeeded"); // v2 prevotes for some proposal, we cannot find it in the validator set => error - let output = block_on(driver.execute(Event::Vote( + let output = block_on(driver.execute(Input::Vote( Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), v2.address).signed(&sk2), ))); @@ -1069,12 +1069,12 @@ fn driver_steps_invalid_signature() { let mut driver = Driver::new(ctx, sel, vs, my_addr); // Start new round - block_on(driver.execute(Event::NewRound(Height::new(1), Round::new(0)))) + block_on(driver.execute(Input::NewRound(Height::new(1), Round::new(0)))) .expect("execute succeeded"); // v2 prevotes for some proposal, with an invalid signature, // ie. signed by v1 instead of v2, just a way of forging an invalid signature - let output = block_on(driver.execute(Event::Vote( + let output = block_on(driver.execute(Input::Vote( Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), v2.address).signed(&sk1), ))); @@ -1102,8 +1102,8 @@ fn driver_steps_skip_round_skip_threshold() { // Start round 0, we, v3, are not the proposer TestStep { desc: "Start round 0, we, v3, are not the proposer", - input_event: Some(Event::NewRound(height, Round::new(0))), - expected_output: Some(Message::ScheduleTimeout(Timeout::propose(Round::new(0)))), + input: Some(Input::NewRound(height, Round::new(0))), + expected_output: Some(Output::ScheduleTimeout(Timeout::propose(Round::new(0)))), expected_round: Round::new(0), new_state: State { height, @@ -1117,8 +1117,8 @@ fn driver_steps_skip_round_skip_threshold() { // Receive a propose timeout, prevote for nil (from v3) TestStep { desc: "Receive a propose timeout, prevote for nil (v3)", - input_event: Some(Event::TimeoutElapsed(Timeout::propose(Round::new(0)))), - expected_output: Some(Message::Vote( + input: Some(Input::TimeoutElapsed(Timeout::propose(Round::new(0)))), + expected_output: Some(Output::Vote( Vote::new_prevote(height, Round::new(0), None, my_addr).signed(&my_sk), )), expected_round: Round::new(0), @@ -1134,7 +1134,7 @@ fn driver_steps_skip_round_skip_threshold() { // Receive our own prevote v3 TestStep { desc: "Receive our own prevote v3", - input_event: None, + input: None, expected_output: None, expected_round: Round::new(0), new_state: State { @@ -1149,7 +1149,7 @@ fn driver_steps_skip_round_skip_threshold() { // v1 prevotes for its own proposal TestStep { desc: "v1 prevotes for its own proposal in round 1", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_prevote(height, Round::new(1), Some(value.id()), v1.address).signed(&sk1), )), expected_output: None, @@ -1166,10 +1166,10 @@ fn driver_steps_skip_round_skip_threshold() { // v2 prevotes for v1 proposal in round 1, expected output is to move to next round TestStep { desc: "v2 prevotes for v1 proposal, we get +1/3 messages from future round", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_prevote(height, Round::new(1), Some(value.id()), v2.address).signed(&sk2), )), - expected_output: Some(Message::NewRound(height, Round::new(1))), + expected_output: Some(Output::NewRound(height, Round::new(1))), expected_round: Round::new(1), new_state: State { height, @@ -1182,22 +1182,22 @@ fn driver_steps_skip_round_skip_threshold() { }, ]; - let mut event_from_previous_msg = None; + let mut output_from_prev_input = None; for step in steps { println!("Step: {}", step.desc); - let execute_event = step - .input_event - .unwrap_or_else(|| event_from_previous_msg.unwrap()); + let input = step + .input + .unwrap_or_else(|| output_from_prev_input.unwrap()); - let output = block_on(driver.execute(execute_event)).expect("execute succeeded"); - assert_eq!(output, step.expected_output, "expected output message"); + let output = block_on(driver.execute(input)).expect("execute succeeded"); + assert_eq!(output, step.expected_output, "expected output"); assert_eq!(driver.round(), step.expected_round, "expected round"); assert_eq!(driver.round_state, step.new_state, "new state"); - event_from_previous_msg = output.and_then(msg_to_event); + output_from_prev_input = output.and_then(output_to_input); } } @@ -1222,8 +1222,8 @@ fn driver_steps_skip_round_quorum_threshold() { // Start round 0, we, v3, are not the proposer TestStep { desc: "Start round 0, we, v3, are not the proposer", - input_event: Some(Event::NewRound(height, Round::new(0))), - expected_output: Some(Message::ScheduleTimeout(Timeout::propose(Round::new(0)))), + input: Some(Input::NewRound(height, Round::new(0))), + expected_output: Some(Output::ScheduleTimeout(Timeout::propose(Round::new(0)))), expected_round: Round::new(0), new_state: State { height, @@ -1237,8 +1237,8 @@ fn driver_steps_skip_round_quorum_threshold() { // Receive a propose timeout, prevote for nil (from v3) TestStep { desc: "Receive a propose timeout, prevote for nil (v3)", - input_event: Some(Event::TimeoutElapsed(Timeout::propose(Round::new(0)))), - expected_output: Some(Message::Vote( + input: Some(Input::TimeoutElapsed(Timeout::propose(Round::new(0)))), + expected_output: Some(Output::Vote( Vote::new_prevote(height, Round::new(0), None, my_addr).signed(&my_sk), )), expected_round: Round::new(0), @@ -1254,7 +1254,7 @@ fn driver_steps_skip_round_quorum_threshold() { // Receive our own prevote v3 TestStep { desc: "Receive our own prevote v3", - input_event: None, + input: None, expected_output: None, expected_round: Round::new(0), new_state: State { @@ -1269,7 +1269,7 @@ fn driver_steps_skip_round_quorum_threshold() { // v1 prevotes for its own proposal TestStep { desc: "v1 prevotes for its own proposal in round 1", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_prevote(height, Round::new(1), Some(value.id()), v1.address).signed(&sk1), )), expected_output: None, @@ -1286,10 +1286,10 @@ fn driver_steps_skip_round_quorum_threshold() { // v2 prevotes for v1 proposal in round 1, expected output is to move to next round TestStep { desc: "v2 prevotes for v1 proposal, we get +1/3 messages from future round", - input_event: Some(Event::Vote( + input: Some(Input::Vote( Vote::new_prevote(height, Round::new(1), Some(value.id()), v2.address).signed(&sk2), )), - expected_output: Some(Message::NewRound(height, Round::new(1))), + expected_output: Some(Output::NewRound(height, Round::new(1))), expected_round: Round::new(1), new_state: State { height, @@ -1302,22 +1302,22 @@ fn driver_steps_skip_round_quorum_threshold() { }, ]; - let mut event_from_previous_msg = None; + let mut input_from_prev_output = None; for step in steps { println!("Step: {}", step.desc); - let execute_event = step - .input_event - .unwrap_or_else(|| event_from_previous_msg.unwrap()); + let input = step + .input + .unwrap_or_else(|| input_from_prev_output.unwrap()); - let output = block_on(driver.execute(execute_event)).expect("execute succeeded"); - assert_eq!(output, step.expected_output, "expected output message"); + let output = block_on(driver.execute(input)).expect("execute succeeded"); + assert_eq!(output, step.expected_output, "expected output"); assert_eq!(driver.round(), step.expected_round, "expected round"); assert_eq!(driver.round_state, step.new_state, "new state"); - event_from_previous_msg = output.and_then(msg_to_event); + input_from_prev_output = output.and_then(output_to_input); } } diff --git a/Code/test/tests/driver_extra.rs b/Code/test/tests/driver_extra.rs index dd88300f5..f0f665b87 100644 --- a/Code/test/tests/driver_extra.rs +++ b/Code/test/tests/driver_extra.rs @@ -1,7 +1,7 @@ use futures::executor::block_on; use malachite_common::Round; -use malachite_driver::{Driver, Event, Message, Validity}; +use malachite_driver::{Driver, Input, Output, Validity}; use malachite_round::state::State; use malachite_test::{Height, Proposal, TestContext, ValidatorSet, Value}; @@ -11,21 +11,21 @@ use malachite_test::utils::*; // TODO - move all below to utils? struct TestStep { desc: &'static str, - input_event: Event, - expected_output: Option>, + input: Input, + expected_output: Option>, expected_round: Round, new_state: State, } -pub fn msg_to_event(output: Message) -> Option> { +pub fn output_to_input(output: Output) -> Option> { match output { - Message::NewRound(height, round) => Some(Event::NewRound(height, round)), + Output::NewRound(height, round) => Some(Input::NewRound(height, round)), // Let's consider our own proposal to always be valid - Message::Propose(p) => Some(Event::Proposal(p, Validity::Valid)), - Message::Vote(v) => Some(Event::Vote(v)), - Message::Decide(_, _) => None, - Message::ScheduleTimeout(_) => None, - Message::GetValueAndScheduleTimeout(_, _) => None, + Output::Propose(p) => Some(Input::Proposal(p, Validity::Valid)), + Output::Vote(v) => Some(Input::Vote(v)), + Output::Decide(_, _) => None, + Output::ScheduleTimeout(_) => None, + Output::GetValueAndScheduleTimeout(_, _) => None, } } @@ -57,29 +57,29 @@ fn driver_steps_decide_current_with_no_locked_no_valid() { let steps = vec![ TestStep { desc: "Start round 0, we, v2, are not the proposer, start timeout propose", - input_event: new_round_event(Round::new(0)), - expected_output: start_propose_timer_msg(Round::new(0)), + input: new_round_input(Round::new(0)), + expected_output: start_propose_timer_output(Round::new(0)), expected_round: Round::new(0), new_state: propose_state(Round::new(0)), }, TestStep { desc: "v1 precommits a proposal", - input_event: precommit_event(Round::new(0), value, &v1.address, &sk1), + input: precommit_input(Round::new(0), value, &v1.address, &sk1), expected_output: None, expected_round: Round::new(0), new_state: propose_state(Round::new(0)), }, TestStep { desc: "v2 precommits for same proposal, we get +2/3 precommit, start precommit timer", - input_event: precommit_event(Round::new(0), value, &v2.address, &sk2), - expected_output: start_precommit_timer_msg(Round::new(0)), + input: precommit_input(Round::new(0), value, &v2.address, &sk2), + expected_output: start_precommit_timer_output(Round::new(0)), expected_round: Round::new(0), new_state: propose_state(Round::new(0)), }, TestStep { desc: "Receive proposal", - input_event: proposal_event(Round::new(0), value, Round::Nil, Validity::Valid), - expected_output: decide_message(Round::new(0), value), + input: proposal_input(Round::new(0), value, Round::Nil, Validity::Valid), + expected_output: decide_output(Round::new(0), value), expected_round: Round::new(0), new_state: decided_state( Round::new(0), @@ -129,57 +129,57 @@ fn driver_steps_decide_previous_with_no_locked_no_valid() { let steps = vec![ TestStep { desc: "Start round 0, we, v2, are not the proposer, start timeout propose", - input_event: new_round_event(Round::new(0)), - expected_output: start_propose_timer_msg(Round::new(0)), + input: new_round_input(Round::new(0)), + expected_output: start_propose_timer_output(Round::new(0)), expected_round: Round::new(0), new_state: propose_state(Round::new(0)), }, TestStep { desc: "Timeout propopse, prevote for nil (v2)", - input_event: timeout_propose_event(Round::new(0)), - expected_output: prevote_nil_msg(Round::new(0), &my_addr, &my_sk), + input: timeout_propose_input(Round::new(0)), + expected_output: prevote_nil_output(Round::new(0), &my_addr, &my_sk), expected_round: Round::new(0), new_state: prevote_state(Round::new(0)), }, TestStep { desc: "v1 prevotes a proposal", - input_event: prevote_event(&v1.address, &sk1), + input: prevote_input(&v1.address, &sk1), expected_output: None, expected_round: Round::new(0), new_state: prevote_state(Round::new(0)), }, TestStep { desc: "v2 prevotes for same proposal, we get +2/3 prevotes, start prevote timer", - input_event: prevote_event(&v2.address, &sk2), - expected_output: start_prevote_timer_msg(Round::new(0)), + input: prevote_input(&v2.address, &sk2), + expected_output: start_prevote_timer_output(Round::new(0)), expected_round: Round::new(0), new_state: prevote_state(Round::new(0)), }, TestStep { desc: "v1 precommits a proposal", - input_event: precommit_event(Round::new(0), value, &v1.address, &sk1), + input: precommit_input(Round::new(0), value, &v1.address, &sk1), expected_output: None, expected_round: Round::new(0), new_state: prevote_state(Round::new(0)), }, TestStep { desc: "v2 precommits for same proposal, we get +2/3 precommit, start precommit timer", - input_event: precommit_event(Round::new(0), value, &v2.address, &sk2), - expected_output: start_precommit_timer_msg(Round::new(0)), + input: precommit_input(Round::new(0), value, &v2.address, &sk2), + expected_output: start_precommit_timer_output(Round::new(0)), expected_round: Round::new(0), new_state: prevote_state(Round::new(0)), }, TestStep { desc: "Timeout precommit, start new round", - input_event: timeout_precommit_event(Round::new(0)), - expected_output: new_round_msg(Round::new(1)), + input: timeout_precommit_input(Round::new(0)), + expected_output: new_round_output(Round::new(1)), expected_round: Round::new(1), new_state: new_round(Round::new(1)), }, TestStep { desc: "Receive proposal", - input_event: proposal_event(Round::new(0), value, Round::Nil, Validity::Valid), - expected_output: decide_message(Round::new(0), value), + input: proposal_input(Round::new(0), value, Round::Nil, Validity::Valid), + expected_output: decide_output(Round::new(0), value), expected_round: Round::new(1), new_state: decided_state( Round::new(1), @@ -231,15 +231,15 @@ fn driver_steps_polka_previous_with_locked() { let steps = vec![ TestStep { desc: "Start round 0, we, v2, are not the proposer, start timeout propose", - input_event: new_round_event(Round::new(0)), - expected_output: start_propose_timer_msg(Round::new(0)), + input: new_round_input(Round::new(0)), + expected_output: start_propose_timer_output(Round::new(0)), expected_round: Round::new(0), new_state: propose_state(Round::new(0)), }, TestStep { desc: "receive a proposal from v1 - L22 send prevote", - input_event: proposal_event(Round::new(0), value, Round::Nil, Validity::Valid), - expected_output: prevote_msg(Round::new(0), &my_addr, &my_sk), + input: proposal_input(Round::new(0), value, Round::Nil, Validity::Valid), + expected_output: prevote_output(Round::new(0), &my_addr, &my_sk), expected_round: Round::new(0), new_state: prevote_state( Round::new(0), @@ -248,7 +248,7 @@ fn driver_steps_polka_previous_with_locked() { }, TestStep { desc: "v3 prevotes the proposal", - input_event: prevote_event(&v3.address, &sk3), + input: prevote_input(&v3.address, &sk3), expected_output: None, expected_round: Round::new(0), new_state: prevote_state( @@ -258,8 +258,8 @@ fn driver_steps_polka_previous_with_locked() { }, TestStep { desc: "v1 prevotes for same proposal, we get +2/3 prevotes, precommit", - input_event: prevote_event(&v1.address, &sk1), - expected_output: precommit_msg(Round::new(0), value, &my_addr, &my_sk), + input: prevote_input(&v1.address, &sk1), + expected_output: precommit_output(Round::new(0), value, &my_addr, &my_sk), expected_round: Round::new(0), new_state: precommit_state_with_proposal_and_locked_and_valid( Round::new(0), @@ -268,8 +268,8 @@ fn driver_steps_polka_previous_with_locked() { }, TestStep { desc: "Receive f+1 vote for round 1 from v3", - input_event: precommit_event(Round::new(1), Value::new(8888), &v3.address, &sk3), - expected_output: new_round_msg(Round::new(1)), + input: precommit_input(Round::new(1), Value::new(8888), &v3.address, &sk3), + expected_output: new_round_output(Round::new(1)), expected_round: Round::new(1), new_state: new_round_with_proposal_and_locked_and_valid( Round::new(1), @@ -278,8 +278,8 @@ fn driver_steps_polka_previous_with_locked() { }, TestStep { desc: "start round 1, we are proposer with a valid value, propose it", - input_event: new_round_event(Round::new(1)), - expected_output: proposal_msg(Round::new(1), value, Round::new(0)), + input: new_round_input(Round::new(1)), + expected_output: proposal_output(Round::new(1), value, Round::new(0)), expected_round: Round::new(1), new_state: propose_state_with_proposal_and_locked_and_valid( Round::new(1), @@ -288,8 +288,8 @@ fn driver_steps_polka_previous_with_locked() { }, TestStep { desc: "Receive our own proposal", - input_event: proposal_event(Round::new(1), value, Round::new(0), Validity::Valid), - expected_output: prevote_msg(Round::new(1), &my_addr, &my_sk), + input: proposal_input(Round::new(1), value, Round::new(0), Validity::Valid), + expected_output: prevote_output(Round::new(1), &my_addr, &my_sk), expected_round: Round::new(1), new_state: prevote_state_with_proposal_and_locked_and_valid( Round::new(1), @@ -317,15 +317,15 @@ fn driver_steps_polka_previous_invalid_proposal_with_locked() { let steps = vec![ TestStep { desc: "Start round 0, we, v2, are not the proposer, start timeout propose", - input_event: new_round_event(Round::new(0)), - expected_output: start_propose_timer_msg(Round::new(0)), + input: new_round_input(Round::new(0)), + expected_output: start_propose_timer_output(Round::new(0)), expected_round: Round::new(0), new_state: propose_state(Round::new(0)), }, TestStep { desc: "receive a proposal from v1 - L22 send prevote", - input_event: proposal_event(Round::new(0), value, Round::Nil, Validity::Valid), - expected_output: prevote_msg(Round::new(0), &my_addr, &my_sk), + input: proposal_input(Round::new(0), value, Round::Nil, Validity::Valid), + expected_output: prevote_output(Round::new(0), &my_addr, &my_sk), expected_round: Round::new(0), new_state: prevote_state( Round::new(0), @@ -334,7 +334,7 @@ fn driver_steps_polka_previous_invalid_proposal_with_locked() { }, TestStep { desc: "v3 prevotes the proposal", - input_event: prevote_event(&v3.address, &sk3), + input: prevote_input(&v3.address, &sk3), expected_output: None, expected_round: Round::new(0), new_state: prevote_state( @@ -344,8 +344,8 @@ fn driver_steps_polka_previous_invalid_proposal_with_locked() { }, TestStep { desc: "v1 prevotes for same proposal, we get +2/3 prevotes, precommit", - input_event: prevote_event(&v1.address, &sk1), - expected_output: precommit_msg(Round::new(0), value, &my_addr, &my_sk), + input: prevote_input(&v1.address, &sk1), + expected_output: precommit_output(Round::new(0), value, &my_addr, &my_sk), expected_round: Round::new(0), new_state: precommit_state_with_proposal_and_locked_and_valid( Round::new(0), @@ -354,8 +354,8 @@ fn driver_steps_polka_previous_invalid_proposal_with_locked() { }, TestStep { desc: "Receive f+1 vote for round 1 from v3", - input_event: precommit_event(Round::new(1), Value::new(8888), &v3.address, &sk3), - expected_output: new_round_msg(Round::new(1)), + input: precommit_input(Round::new(1), Value::new(8888), &v3.address, &sk3), + expected_output: new_round_output(Round::new(1)), expected_round: Round::new(1), new_state: new_round_with_proposal_and_locked_and_valid( Round::new(1), @@ -364,8 +364,8 @@ fn driver_steps_polka_previous_invalid_proposal_with_locked() { }, TestStep { desc: "start round 1, we are proposer with a valid value, propose it", - input_event: new_round_event(Round::new(1)), - expected_output: proposal_msg(Round::new(1), value, Round::new(0)), + input: new_round_input(Round::new(1)), + expected_output: proposal_output(Round::new(1), value, Round::new(0)), expected_round: Round::new(1), new_state: propose_state_with_proposal_and_locked_and_valid( Round::new(1), @@ -374,8 +374,8 @@ fn driver_steps_polka_previous_invalid_proposal_with_locked() { }, TestStep { desc: "Receive our own proposal", - input_event: proposal_event(Round::new(1), value, Round::new(0), Validity::Invalid), - expected_output: prevote_nil_msg(Round::new(1), &my_addr, &my_sk), + input: proposal_input(Round::new(1), value, Round::new(0), Validity::Invalid), + expected_output: prevote_nil_output(Round::new(1), &my_addr, &my_sk), expected_round: Round::new(1), new_state: prevote_state_with_proposal_and_locked_and_valid( Round::new(1), @@ -433,42 +433,42 @@ fn driver_steps_polka_previous_with_no_locked() { let steps = vec![ TestStep { desc: "Start round 0, we v2 are not the proposer, start timeout propose", - input_event: new_round_event(Round::new(0)), - expected_output: start_propose_timer_msg(Round::new(0)), + input: new_round_input(Round::new(0)), + expected_output: start_propose_timer_output(Round::new(0)), expected_round: Round::new(0), new_state: propose_state(Round::new(0)), }, TestStep { desc: "Timeout propopse, prevote for nil (v2)", - input_event: timeout_propose_event(Round::new(0)), - expected_output: prevote_nil_msg(Round::new(0), &my_addr, &my_sk), + input: timeout_propose_input(Round::new(0)), + expected_output: prevote_nil_output(Round::new(0), &my_addr, &my_sk), expected_round: Round::new(0), new_state: prevote_state(Round::new(0)), }, TestStep { desc: "v3 prevotes for some proposal", - input_event: prevote_event(&v3.address, &sk3), + input: prevote_input(&v3.address, &sk3), expected_output: None, expected_round: Round::new(0), new_state: prevote_state(Round::new(0)), }, TestStep { desc: "v1 prevotes for same proposal, we get +2/3 prevotes, start timeout prevote", - input_event: prevote_event(&v1.address, &sk1), - expected_output: start_prevote_timer_msg(Round::new(0)), + input: prevote_input(&v1.address, &sk1), + expected_output: start_prevote_timer_output(Round::new(0)), expected_round: Round::new(0), new_state: prevote_state(Round::new(0)), }, TestStep { desc: "timeout prevote, prevote for nil (v2)", - input_event: timeout_prevote_event(Round::new(0)), - expected_output: precommit_nil_msg(&my_addr, &my_sk), + input: timeout_prevote_input(Round::new(0)), + expected_output: precommit_nil_output(&my_addr, &my_sk), expected_round: Round::new(0), new_state: precommit_state(Round::new(0)), }, TestStep { desc: "receive a proposal - L36, we don't lock, we set valid", - input_event: proposal_event(Round::new(0), value, Round::Nil, Validity::Valid), + input: proposal_input(Round::new(0), value, Round::Nil, Validity::Valid), expected_output: None, expected_round: Round::new(0), new_state: precommit_state_with_proposal_and_valid( @@ -479,8 +479,8 @@ fn driver_steps_polka_previous_with_no_locked() { }, TestStep { desc: "Receive f+1 vote for round 1 from v3", - input_event: prevote_event_at(Round::new(1), &v3.address, &sk3), - expected_output: new_round_msg(Round::new(1)), + input: prevote_input_at(Round::new(1), &v3.address, &sk3), + expected_output: new_round_output(Round::new(1)), expected_round: Round::new(1), new_state: new_round_with_proposal_and_valid( Round::new(1), @@ -489,8 +489,8 @@ fn driver_steps_polka_previous_with_no_locked() { }, TestStep { desc: "start round 1, we are proposer with a valid value from round 0, propose it", - input_event: new_round_event(Round::new(1)), - expected_output: proposal_msg(Round::new(1), value, Round::new(0)), + input: new_round_input(Round::new(1)), + expected_output: proposal_output(Round::new(1), value, Round::new(0)), expected_round: Round::new(1), new_state: propose_state_with_proposal_and_valid( Round::new(1), @@ -500,8 +500,8 @@ fn driver_steps_polka_previous_with_no_locked() { }, TestStep { desc: "Receive our own proposal, prevote nil as we are not locked on the value", - input_event: proposal_event(Round::new(1), value, Round::new(0), Validity::Valid), - expected_output: prevote_nil_msg(Round::new(1), &my_addr, &my_sk), + input: proposal_input(Round::new(1), value, Round::new(0), Validity::Valid), + expected_output: prevote_nil_output(Round::new(1), &my_addr, &my_sk), expected_round: Round::new(1), new_state: prevote_state_with_proposal_and_valid( Round::new(1), @@ -518,8 +518,8 @@ fn run_steps(driver: &mut Driver, steps: Vec) { for step in steps { println!("Step: {}", step.desc); - let output = block_on(driver.execute(step.input_event)).expect("execute succeeded"); - assert_eq!(output, step.expected_output, "expected output message"); + let output = block_on(driver.execute(step.input)).expect("execute succeeded"); + assert_eq!(output, step.expected_output, "expected output"); assert_eq!( driver.round_state.round, step.expected_round, diff --git a/Code/test/tests/round.rs b/Code/test/tests/round.rs index 0952ff747..246194a7a 100644 --- a/Code/test/tests/round.rs +++ b/Code/test/tests/round.rs @@ -1,10 +1,10 @@ use malachite_test::{Address, Height, Proposal, TestContext, Value}; use malachite_common::{Round, Timeout, TimeoutStep}; -use malachite_round::events::Event; -use malachite_round::message::Message; +use malachite_round::input::Input; +use malachite_round::output::Output; use malachite_round::state::{State, Step}; -use malachite_round::state_machine::{apply_event, Info}; +use malachite_round::state_machine::{apply, Info}; const ADDRESS: Address = Address::new([42; 20]); const OTHER_ADDRESS: Address = Address::new([21; 20]); @@ -24,22 +24,22 @@ fn test_propose() { // We are the proposer let data = Info::new(round, &ADDRESS, &ADDRESS); - let transition = apply_event(state.clone(), &data, Event::NewRound); + let transition = apply(state.clone(), &data, Input::NewRound); state.step = Step::Propose; assert_eq!(transition.next_state, state); assert_eq!( - transition.message.unwrap(), - Message::get_value_and_schedule_timeout(round, TimeoutStep::Propose) + transition.output.unwrap(), + Output::get_value_and_schedule_timeout(round, TimeoutStep::Propose) ); - let transition = apply_event(transition.next_state, &data, Event::ProposeValue(value)); + let transition = apply(transition.next_state, &data, Input::ProposeValue(value)); state.step = Step::Propose; assert_eq!(transition.next_state, state); assert_eq!( - transition.message.unwrap(), - Message::proposal(Height::new(10), Round::new(0), Value::new(42), Round::Nil) + transition.output.unwrap(), + Output::proposal(Height::new(10), Round::new(0), Value::new(42), Round::Nil) ); } @@ -58,12 +58,12 @@ fn test_prevote() { // We are not the proposer let data = Info::new(Round::new(1), &ADDRESS, &OTHER_ADDRESS); - let transition = apply_event(state, &data, Event::NewRound); + let transition = apply(state, &data, Input::NewRound); assert_eq!(transition.next_state.step, Step::Propose); assert_eq!( - transition.message.unwrap(), - Message::ScheduleTimeout(Timeout { + transition.output.unwrap(), + Output::ScheduleTimeout(Timeout { round: Round::new(1), step: TimeoutStep::Propose }) @@ -71,10 +71,10 @@ fn test_prevote() { let state = transition.next_state; - let transition = apply_event( + let transition = apply( state, &data, - Event::Proposal(Proposal::new( + Input::Proposal(Proposal::new( Height::new(1), Round::new(1), value, @@ -84,7 +84,7 @@ fn test_prevote() { assert_eq!(transition.next_state.step, Step::Prevote); assert_eq!( - transition.message.unwrap(), - Message::prevote(Height::new(1), Round::new(1), Some(value.id()), ADDRESS) + transition.output.unwrap(), + Output::prevote(Height::new(1), Round::new(1), Some(value.id()), ADDRESS) ); } diff --git a/Code/test/tests/vote_keeper.rs b/Code/test/tests/vote_keeper.rs index f1d6d7849..f3cd9df3f 100644 --- a/Code/test/tests/vote_keeper.rs +++ b/Code/test/tests/vote_keeper.rs @@ -1,5 +1,5 @@ use malachite_common::Round; -use malachite_vote::keeper::{Message, VoteKeeper}; +use malachite_vote::keeper::{Output, VoteKeeper}; use malachite_test::{Address, Height, TestContext, ValueId, Vote}; @@ -24,7 +24,7 @@ fn prevote_apply_nil() { let vote = Vote::new_prevote(height, round, None, ADDRESS3); let msg = keeper.apply_vote(vote, 1, round); - assert_eq!(msg, Some(Message::PolkaNil)); + assert_eq!(msg, Some(Output::PolkaNil)); } #[test] @@ -43,7 +43,7 @@ fn precommit_apply_nil() { let vote = Vote::new_precommit(height, Round::new(0), None, ADDRESS3); let msg = keeper.apply_vote(vote, 1, round); - assert_eq!(msg, Some(Message::PrecommitAny)); + assert_eq!(msg, Some(Output::PrecommitAny)); } #[test] @@ -65,11 +65,11 @@ fn prevote_apply_single_value() { let vote_nil = Vote::new_prevote(height, Round::new(0), None, ADDRESS3); let msg = keeper.apply_vote(vote_nil, 1, round); - assert_eq!(msg, Some(Message::PolkaAny)); + assert_eq!(msg, Some(Output::PolkaAny)); let vote = Vote::new_prevote(height, Round::new(0), val, ADDRESS4); let msg = keeper.apply_vote(vote, 1, round); - assert_eq!(msg, Some(Message::PolkaValue(id))); + assert_eq!(msg, Some(Output::PolkaValue(id))); } #[test] @@ -91,11 +91,11 @@ fn precommit_apply_single_value() { let vote_nil = Vote::new_precommit(height, Round::new(0), None, ADDRESS3); let msg = keeper.apply_vote(vote_nil, 1, round); - assert_eq!(msg, Some(Message::PrecommitAny)); + assert_eq!(msg, Some(Output::PrecommitAny)); let vote = Vote::new_precommit(height, Round::new(0), val, ADDRESS4); let msg = keeper.apply_vote(vote, 1, round); - assert_eq!(msg, Some(Message::PrecommitValue(id))); + assert_eq!(msg, Some(Output::PrecommitValue(id))); } #[test] @@ -118,7 +118,7 @@ fn skip_round_small_quorum_prevotes_two_vals() { let vote = Vote::new_prevote(height, fut_round, val, ADDRESS3); let msg = keeper.apply_vote(vote, 1, cur_round); - assert_eq!(msg, Some(Message::SkipRound(Round::new(1)))); + assert_eq!(msg, Some(Output::SkipRound(Round::new(1)))); } #[test] @@ -141,7 +141,7 @@ fn skip_round_small_quorum_with_prevote_precommit_two_vals() { let vote = Vote::new_precommit(height, fut_round, val, ADDRESS3); let msg = keeper.apply_vote(vote, 1, cur_round); - assert_eq!(msg, Some(Message::SkipRound(Round::new(1)))); + assert_eq!(msg, Some(Output::SkipRound(Round::new(1)))); } #[test] @@ -164,7 +164,7 @@ fn skip_round_full_quorum_with_prevote_precommit_two_vals() { let vote = Vote::new_precommit(height, fut_round, val, ADDRESS3); let msg = keeper.apply_vote(vote, 2, cur_round); - assert_eq!(msg, Some(Message::SkipRound(Round::new(1)))); + assert_eq!(msg, Some(Output::SkipRound(Round::new(1)))); } #[test] diff --git a/Code/vote/src/keeper.rs b/Code/vote/src/keeper.rs index 808bf3685..a0e500712 100644 --- a/Code/vote/src/keeper.rs +++ b/Code/vote/src/keeper.rs @@ -10,7 +10,7 @@ use crate::{Threshold, ThresholdParam, ThresholdParams, Weight}; /// Messages emitted by the vote keeper #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub enum Message { +pub enum Output { PolkaAny, PolkaNil, PolkaValue(Value), @@ -25,7 +25,7 @@ where { votes: RoundVotes>, addresses_weights: RoundWeights, - emitted_msgs: BTreeSet>>, + emitted_outputs: BTreeSet>>, } impl PerRound @@ -36,7 +36,7 @@ where Self { votes: RoundVotes::new(), addresses_weights: RoundWeights::new(), - emitted_msgs: BTreeSet::new(), + emitted_outputs: BTreeSet::new(), } } @@ -48,8 +48,8 @@ where &self.addresses_weights } - pub fn emitted_msgs(&self) -> &BTreeSet>> { - &self.emitted_msgs + pub fn emitted_outputs(&self) -> &BTreeSet>> { + &self.emitted_outputs } } @@ -62,7 +62,7 @@ where Self { votes: self.votes.clone(), addresses_weights: self.addresses_weights.clone(), - emitted_msgs: self.emitted_msgs.clone(), + emitted_outputs: self.emitted_outputs.clone(), } } } @@ -76,7 +76,7 @@ where f.debug_struct("PerRound") .field("votes", &self.votes) .field("addresses_weights", &self.addresses_weights) - .field("emitted_msgs", &self.emitted_msgs) + .field("emitted_outputs", &self.emitted_outputs) .finish() } } @@ -111,13 +111,13 @@ where &self.per_round } - /// Apply a vote with a given weight, potentially triggering an event. + /// Apply a vote with a given weight, potentially triggering an output. pub fn apply_vote( &mut self, vote: Ctx::Vote, weight: Weight, current_round: Round, - ) -> Option>> { + ) -> Option>> { let per_round = self .per_round .entry(vote.round()) @@ -143,9 +143,9 @@ where .is_met(combined_weight, self.total_weight); if skip_round { - let msg = Message::SkipRound(vote.round()); - per_round.emitted_msgs.insert(msg.clone()); - return Some(msg); + let output = Output::SkipRound(vote.round()); + per_round.emitted_outputs.insert(output.clone()); + return Some(output); } } @@ -157,12 +157,12 @@ where self.total_weight, ); - let msg = threshold_to_message(vote.vote_type(), vote.round(), threshold); + let output = threshold_to_output(vote.vote_type(), vote.round(), threshold); - match msg { - Some(msg) if !per_round.emitted_msgs.contains(&msg) => { - per_round.emitted_msgs.insert(msg.clone()); - Some(msg) + match output { + Some(output) if !per_round.emitted_outputs.contains(&output) => { + per_round.emitted_outputs.insert(output.clone()); + Some(output) } _ => None, } @@ -217,23 +217,23 @@ where } } -/// Map a vote type and a threshold to a state machine event. -fn threshold_to_message( +/// Map a vote type and a threshold to a state machine output. +fn threshold_to_output( typ: VoteType, round: Round, threshold: Threshold, -) -> Option> { +) -> Option> { match (typ, threshold) { (_, Threshold::Unreached) => None, - (_, Threshold::Skip) => Some(Message::SkipRound(round)), + (_, Threshold::Skip) => Some(Output::SkipRound(round)), - (VoteType::Prevote, Threshold::Any) => Some(Message::PolkaAny), - (VoteType::Prevote, Threshold::Nil) => Some(Message::PolkaNil), - (VoteType::Prevote, Threshold::Value(v)) => Some(Message::PolkaValue(v)), + (VoteType::Prevote, Threshold::Any) => Some(Output::PolkaAny), + (VoteType::Prevote, Threshold::Nil) => Some(Output::PolkaNil), + (VoteType::Prevote, Threshold::Value(v)) => Some(Output::PolkaValue(v)), - (VoteType::Precommit, Threshold::Any) => Some(Message::PrecommitAny), - (VoteType::Precommit, Threshold::Nil) => Some(Message::PrecommitAny), - (VoteType::Precommit, Threshold::Value(v)) => Some(Message::PrecommitValue(v)), + (VoteType::Precommit, Threshold::Any) => Some(Output::PrecommitAny), + (VoteType::Precommit, Threshold::Nil) => Some(Output::PrecommitAny), + (VoteType::Precommit, Threshold::Value(v)) => Some(Output::PrecommitValue(v)), } } diff --git a/Scripts/quint-forall.sh b/Scripts/quint-forall.sh index 6ab2fe003..af308fdb0 100755 --- a/Scripts/quint-forall.sh +++ b/Scripts/quint-forall.sh @@ -32,7 +32,7 @@ failed_files=() for file in "${files[@]}"; do info "Running: quint $cmd ${UNDERLINE}$file" - if ! npx @informalsystems/quint "$cmd" "$file"; then + if ! npx @informalsystems/quint $cmd "$file"; then failed_files+=("$file") failed=$((failed + 1)) fi diff --git a/Specs/Quint/0DecideNonProposerTest.itf.json b/Specs/Quint/0DecideNonProposerTest.itf.json deleted file mode 100644 index 5d30f6911..000000000 --- a/Specs/Quint/0DecideNonProposerTest.itf.json +++ /dev/null @@ -1 +0,0 @@ -{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"consensus.qnt","status":"passed","description":"Created by Quint on Wed Oct 25 2023 15:38:28 GMT+0200 (Central European Summer Time)","timestamp":1698241108633},"vars":["system","_Event","_Result"],"states":[{"#meta":{"index":0},"_Event":{"height":-1,"name":"Initial","round":-1,"value":"","vr":-1},"_Result":{"decided":"","name":"","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":1,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"newRound","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":1},"_Event":{"height":1,"name":"NewRound","round":0,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":1,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":2},"_Event":{"height":1,"name":"NewRound","round":0,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":1,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":3},"_Event":{"height":1,"name":"Proposal","round":0,"value":"block","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":1,"id":"block","round":0,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":1,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":4},"_Event":{"height":1,"name":"Proposal","round":0,"value":"block","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":1,"id":"block","round":0,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":1,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":5},"_Event":{"height":1,"name":"ProposalAndPolkaAndValid","round":0,"value":"block","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":1,"id":"block","round":0,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":1,"lockedRound":0,"lockedValue":"block","p":"Josef","round":0,"step":"precommit","validRound":0,"validValue":"block"}]]}},{"#meta":{"index":6},"_Event":{"height":1,"name":"ProposalAndPolkaAndValid","round":0,"value":"block","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":1,"id":"block","round":0,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":1,"lockedRound":0,"lockedValue":"block","p":"Josef","round":0,"step":"precommit","validRound":0,"validValue":"block"}]]}},{"#meta":{"index":7},"_Event":{"height":1,"name":"ProposalAndCommitAndValid","round":0,"value":"block","vr":-1},"_Result":{"decided":"block","name":"decided","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":1,"lockedRound":0,"lockedValue":"block","p":"Josef","round":0,"step":"decided","validRound":0,"validValue":"block"}]]}},{"#meta":{"index":8},"_Event":{"height":1,"name":"ProposalAndCommitAndValid","round":0,"value":"block","vr":-1},"_Result":{"decided":"block","name":"decided","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":1,"lockedRound":0,"lockedValue":"block","p":"Josef","round":0,"step":"decided","validRound":0,"validValue":"block"}]]}},{"#meta":{"index":9},"_Event":{"height":2,"name":"NewHeight","round":0,"value":"","vr":-1},"_Result":{"decided":"","name":"","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"newRound","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":10},"_Event":{"height":2,"name":"NewHeight","round":0,"value":"","vr":-1},"_Result":{"decided":"","name":"","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"newRound","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":11},"_Event":{"height":2,"name":"NewRoundProposer","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"proposal","proposal":{"height":2,"proposal":"nextBlock","round":0,"src":"Josef","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":12},"_Event":{"height":2,"name":"NewRoundProposer","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"proposal","proposal":{"height":2,"proposal":"nextBlock","round":0,"src":"Josef","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":13},"_Event":{"height":2,"name":"Proposal","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nextBlock","round":0,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":14},"_Event":{"height":2,"name":"Proposal","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nextBlock","round":0,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":15},"_Event":{"height":2,"name":"PolkaAny","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrevote","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":16},"_Event":{"height":2,"name":"PolkaAny","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrevote","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":17},"_Event":{"height":2,"name":"TimeoutPrevote","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":0,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":18},"_Event":{"height":2,"name":"TimeoutPrevote","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":0,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":19},"_Event":{"height":2,"name":"PrecommitAny","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrecommit","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":20},"_Event":{"height":2,"name":"PrecommitAny","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrecommit","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":21},"_Event":{"height":2,"name":"TimeoutPrecommit","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"skipRound","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":22},"_Event":{"height":2,"name":"TimeoutPrecommit","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"skipRound","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":23},"_Event":{"height":2,"name":"NewRound","round":1,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":24},"_Event":{"height":2,"name":"NewRound","round":1,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":25},"_Event":{"height":2,"name":"TimeoutPropose","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":1,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":26},"_Event":{"height":2,"name":"TimeoutPropose","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":1,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":27},"_Event":{"height":2,"name":"PolkaNil","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":1,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":28},"_Event":{"height":2,"name":"PolkaNil","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":1,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":29},"_Event":{"height":2,"name":"PrecommitAny","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrecommit","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":30},"_Event":{"height":2,"name":"PrecommitAny","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrecommit","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":31},"_Event":{"height":2,"name":"TimeoutPrecommit","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"skipRound","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":2,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":32},"_Event":{"height":2,"name":"TimeoutPrecommit","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"skipRound","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":2,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":33},"_Event":{"height":2,"name":"NewRound","round":2,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":2,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":34},"_Event":{"height":2,"name":"NewRound","round":2,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":2,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":35},"_Event":{"height":2,"name":"ProposalInvalid","round":2,"value":"","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":2,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":2,"step":"prevote","validRound":-1,"validValue":"nil"}]]}}]} \ No newline at end of file diff --git a/Specs/Quint/Makefile b/Specs/Quint/Makefile index 2b9227986..a7477d691 100644 --- a/Specs/Quint/Makefile +++ b/Specs/Quint/Makefile @@ -1,7 +1,7 @@ parse: npx @informalsystems/quint parse asyncModelsTest.qnt npx @informalsystems/quint parse consensusTest.qnt - npx @informalsystems/quint parse executor.qnt + npx @informalsystems/quint parse driver.qnt npx @informalsystems/quint parse statemachineTest.qnt npx @informalsystems/quint parse voteBookkeeperTest.qnt .PHONY: parse diff --git a/Specs/Quint/TendermintDSL.qnt b/Specs/Quint/TendermintDSL.qnt new file mode 100644 index 000000000..501d46f0a --- /dev/null +++ b/Specs/Quint/TendermintDSL.qnt @@ -0,0 +1,52 @@ +// -*- mode: Bluespec; -*- + +module TendermintDSL { + +import statemachineAsync.* from "./statemachineAsync" +export statemachineAsync.* + +val validatorList = validators.fold(List(), (s, x) => s.append(x)) +val correctList = Correct.fold(List(), (s, x) => s.append(x)) +val faultyList = Faulty.fold(List(), (s, x) => s.append(x)) + +run ListTakeAStep (active) = { + active.length().reps(i => valStep(active[i])) +} + +run ListDeliverProposal (active, proposalMsg) = { + active.length().reps(i => deliverProposal(active[i], proposalMsg)) +} + +run ListDeliverSomeProposal (active) = { + active.length().reps(i => deliverSomeProposal(active[i])) +} + +run ProcessDeliverAllVotes (cstep, recepient, fromList, valset, h, r, value) = { + fromList.length().reps(i => deliverVote(recepient, { src: fromList[i], height: h, round: r, step: cstep, id: value })) +} + +run ListDeliverAllVotes (cstep, fromList, toList, valset, h, r, value) = { + toList.length().reps(i => ProcessDeliverAllVotes (cstep, toList[i], fromList, valset, h, r, value)) +} + + +run everyoneReceivesProposal (active, valList, valset, h, r, value) = { + val p = Proposer (valset, h, r) + setNextValueToPropose(p, value) + .then(ListTakeAStep(active)) + .then(all { + assert(true), + ListDeliverSomeProposal(active) + }) + .then(ListTakeAStep(active)) +} + +run fromPrevoteToPrecommit (prevoteSenders, prevoteReceivers, valList, valset, h, r, value) = { + ListDeliverAllVotes("Prevote", prevoteSenders, prevoteReceivers, valset, h, r, value) + .then(prevoteSenders.length().reps(_ => ListTakeAStep(prevoteReceivers))) + // extra step due to timeoutprevote double step + .then(ListTakeAStep(prevoteReceivers)) +} + + +} \ No newline at end of file diff --git a/Specs/Quint/asyncModelsTest.qnt b/Specs/Quint/asyncModelsTest.qnt index 93a120eae..50780fc1f 100644 --- a/Specs/Quint/asyncModelsTest.qnt +++ b/Specs/Quint/asyncModelsTest.qnt @@ -94,6 +94,9 @@ run ThreeDecideInRound1V4stillinZeroTest = { .then(N4F0::valStep("v1")) .then(N4F0::valStep("v2")) .then(N4F0::valStep("v3")) + .then(N4F0::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) .then(N4F0::deliverVote("v1", { height: 0, id: "another block", round: 1, src: "v1", step: "Precommit" })) .then(N4F0::deliverVote("v1", { height: 0, id: "another block", round: 1, src: "v2", step: "Precommit" })) .then(N4F0::deliverVote("v1", { height: 0, id: "another block", round: 1, src: "v3", step: "Precommit" })) @@ -112,6 +115,10 @@ run ThreeDecideInRound1V4stillinZeroTest = { .then(N4F0::valStep("v1")) .then(N4F0::valStep("v2")) .then(N4F0::valStep("v3")) + .then(all { + assert(N4F0::system.get("v3").es.chain.head() == "another block"), + N4F0::unchangedAll + }) } run DecideForFutureRoundTest = { @@ -156,10 +163,10 @@ run RoundswitchTest = { ThreeDecideInRound1V4stillinZeroTest .then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v1", step: "Precommit" })) .then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v2", step: "Prevote" })) - .then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v3", step: "Precommit" })) - .then(N4F0::valStep("v4")) - .then(N4F0::valStep("v4")) .then(N4F0::valStep("v4")) + .then(all { + assert(N4F0::system.get("v4").es.cs.round == 0), + N4F0::valStep("v4")}) .then(all { assert(N4F0::system.get("v4").es.cs.round == 1), N4F0::unchangedAll @@ -200,7 +207,7 @@ run DisagreementTest = { .then(N4F2::valStep("v3")) .then(N4F2::valStep("v4")) .then(all{ - // they voted diN4F2N4F2erently + // they voted differently assert(N4F2::voteBuffer == Map( "v3" -> Set({ height: 0, id: "a", round: 0, src: "v4", step: "Prevote" }, { height: 0, id: "b", round: 0, src: "v3", step: "Prevote" }), @@ -216,6 +223,8 @@ run DisagreementTest = { .then(N4F2::valStep("v3")) .then(N4F2::valStep("v3")) .then(N4F2::valStep("v3")) + .then(N4F2::valStep("v3")) + .then(N4F2::valStep("v4")) .then(N4F2::valStep("v4")) .then(N4F2::valStep("v4")) .then(N4F2::valStep("v4")) diff --git a/Specs/Quint/consensus.qnt b/Specs/Quint/consensus.qnt index 3e282a873..e7cf66ece 100644 --- a/Specs/Quint/consensus.qnt +++ b/Specs/Quint/consensus.qnt @@ -3,14 +3,14 @@ /* TODO: check - whether we have "step" checks in place everywhere -- "the first time": checks here or in executor +- "the first time": checks here or in driver - check against arXiv - tests - types (e.g., heights in the messages) -- discuss "decision tree" in executor +- discuss "decision tree" in driver - Should we think again about the components and the boundaries (especially between - voteBookkeeper and executor) -- Do we need tests for executor and bookkeeping + voteBookkeeper and driver) +- Do we need tests for driver and bookkeeping - test id(v): most likely we need to change the type of Value_t as Quint doesn't have string operators. Perhaps we make Value_t = int and then id(v) = -v */ @@ -32,7 +32,7 @@ module consensus { type Timeout_t = str // the type of propose messages -type ProposeMsg_t = { +type Proposal_t = { src: Address_t, height: Height_t, round: Round_t, @@ -41,7 +41,7 @@ type ProposeMsg_t = { } // the type of Prevote and Precommit messages -type VoteMsg_t = { +type Vote_t = { src: Address_t, height: Height_t, round: Round_t, @@ -51,7 +51,7 @@ type VoteMsg_t = { type ConsensusState = { p: Address_t, - height : Height_t, + height: Height_t, round: Round_t, step: Step_t, // "newRound", propose, Prevote, Precommit, decided lockedRound: Round_t, @@ -65,15 +65,15 @@ pure def initConsensusState (v: Address_t) : ConsensusState = { p: v, round: -1, step: "newRound", - height : 0, + height: 0, lockedRound: -1, lockedValue: "nil", validRound: -1, validValue: "nil" } -type Event = { - name : str, +type ConsensusInput = { + name: str, height : Height_t, round: Round_t, value: Value_t, @@ -82,9 +82,9 @@ type Event = { // what is a good way to encode optionals? I do with default values type ConsensusOutput = { - name : str, - proposal: ProposeMsg_t, - voteMessage: VoteMsg_t, + name: str, + proposal: Proposal_t, + voteMessage: Vote_t, timeout: Timeout_t, decided: Value_t, skipRound: Round_t @@ -104,9 +104,7 @@ type ConsResult = { // pending: Set[ConsensusOutput], // TODO: not sure we need this } -type ConsensusEvent = str - -val ConsensusEvents = Set( +val ConsensusInputNames = Set( "NewHeight", // Setups the state-machine for a single-height execution "NewRound", // Start a new round, not as proposer. "NewRoundProposer", // Start a new round as proposer with the proposed Value. @@ -131,12 +129,12 @@ val ConsensusEvents = Set( "PrecommitValue(ValueId)", // Receive +2/3 Precommits for Value. */ -val noProp : ProposeMsg_t = {src: "", height: -1, round: -1, proposal: "", validRound: -1} -val noVote : VoteMsg_t = {src: "", height: -1, round: -1, step: "", id: ""} +val noProp : Proposal_t = {src: "", height: -1, round: -1, proposal: "", validRound: -1} +val noVote : Vote_t = {src: "", height: -1, round: -1, step: "", id: ""} val noTimeout : Timeout_t = "" val noDecided = "" val noSkipRound : Round_t = -1 -val defaultResult : ConsensusOutput = { +val defaultOutput : ConsensusOutput = { name: "", proposal: noProp, voteMessage: noVote, @@ -146,73 +144,73 @@ val defaultResult : ConsensusOutput = { -pure def NewHeight (state: ConsensusState, ev: Event) : ConsResult = { - if (ev.height > state.height) +pure def NewHeight (state: ConsensusState, input: ConsensusInput) : ConsResult = { + if (input.height > state.height) val newstate = { p: state.p, round: -1, // must be -1, as nothing should be done before a NewRound // function is called step: "newRound", - height : ev.height, + height : input.height, lockedRound: -1, lockedValue: "nil", validRound: -1, validValue: "nil" } - {cs: newstate, out: defaultResult } + {cs: newstate, out: defaultOutput } else - {cs: state, out: defaultResult } + {cs: state, out: defaultOutput } } // line 11.14 -pure def NewRoundProposer (state: ConsensusState, ev: Event) : ConsResult = { - if (ev.round > state.round) - val newstate = { ...state, round: ev.round, step: "propose"} +pure def NewRoundProposer (state: ConsensusState, input: ConsensusInput) : ConsResult = { + if (input.round > state.round) + val newstate = { ...state, round: input.round, step: "propose"} val proposal = if (state.validValue != "nil") state.validValue - else ev.value - val result = { ...defaultResult, name: "proposal", + else input.value + val result = { ...defaultOutput, name: "proposal", proposal: { src: state.p, height: state.height, - round: ev.round, + round: input.round, proposal: proposal, validRound: state.validRound}} {cs: newstate, out: result } else - {cs: state, out: defaultResult } + {cs: state, out: defaultOutput } } // line 11.20 -pure def NewRound (state: ConsensusState, ev: Event) : ConsResult = { - // TODO: discuss comment "ev.round must match state.round" - if (ev.round > state.round) - val newstate = { ...state, round: ev.round, step: "propose" } - val result = { ...defaultResult, name: "timeout", timeout: "TimeoutPropose"} - // We just report that a timeout should be started. The executor must take care +pure def NewRound (state: ConsensusState, input: ConsensusInput) : ConsResult = { + // TODO: discuss comment "input.round must match state.round" + if (input.round > state.round) + val newstate = { ...state, round: input.round, step: "propose" } + val result = { ...defaultOutput, name: "timeout", timeout: "TimeoutPropose"} + // We just report that a timeout should be started. The driver must take care // of figuring out whether it needs to record the round number and height per // timeout {cs: newstate, out: result} else - {cs: state, out: defaultResult } + {cs: state, out: defaultOutput } } // line 22 // Here it is assumed that // - the value has been checked to be valid // - it is for the current round -// The executor checks this upon receiving a propose message "ProposalMsg" -pure def Proposal (state: ConsensusState, ev: Event) : ConsResult = { +// The driver checks this upon receiving a propose message "ProposalMsg" +pure def Proposal (state: ConsensusState, input: ConsensusInput) : ConsResult = { if (state.step == "propose") val newstate = { ...state, step: "Prevote" } - if (state.lockedRound == -1 or state.lockedValue == ev.value) - val result = { ...defaultResult, name: "votemessage", + if (state.lockedRound == -1 or state.lockedValue == input.value) + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, step: "Prevote", - id: ev.value}} + id: input.value}} {cs: newstate, out: result} else - val result = { ...defaultResult, name: "votemessage", + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, @@ -220,15 +218,15 @@ pure def Proposal (state: ConsensusState, ev: Event) : ConsResult = { id: "nil"}} {cs: newstate, out: result} else - {cs: state, out: defaultResult} - // This should be dead code as the executor checks the step + {cs: state, out: defaultOutput} + // This should be dead code as the driver checks the step } // line 26 -pure def ProposalInvalid (state: ConsensusState, ev: Event) : ConsResult = { +pure def ProposalInvalid (state: ConsensusState, input: ConsensusInput) : ConsResult = { if (state.step == "propose") val newstate = state.with("step", "Prevote") - val result = { ...defaultResult, name: "votemessage", + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, @@ -236,23 +234,23 @@ pure def ProposalInvalid (state: ConsensusState, ev: Event) : ConsResult = { id: "nil"}} {cs: newstate, out: result} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } // line 28 -pure def ProposalAndPolkaPreviousAndValid (state: ConsensusState, ev: Event) : ConsResult = { - if (state.step == "propose" and ev.vr >= 0 and ev.vr < state.round) +pure def ProposalAndPolkaPreviousAndValid (state: ConsensusState, input: ConsensusInput) : ConsResult = { + if (state.step == "propose" and input.vr >= 0 and input.vr < state.round) val newstate = state.with("step", "Prevote") - if (state.lockedRound <= ev.vr or state.lockedValue == ev.value) - val result = { ...defaultResult, name: "votemessage", + if (state.lockedRound <= input.vr or state.lockedValue == input.value) + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, step: "Prevote", - id: ev.value}} + id: input.value}} {cs: newstate, out: result} else - val result = { ...defaultResult, name: "votemessage", + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, @@ -260,53 +258,53 @@ pure def ProposalAndPolkaPreviousAndValid (state: ConsensusState, ev: Event) : C id: "nil"}} {cs: newstate, out: result} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} // TODO: should we add the event to pending in this case. We would need to - // do this in the executor + // do this in the driver } // line 34 -pure def PolkaAny (state: ConsensusState, ev: Event) : ConsResult = { +pure def PolkaAny (state: ConsensusState, input: ConsensusInput) : ConsResult = { if (state.step == "Prevote") - val result = { ...defaultResult, name: "timeout", timeout: "TimeoutPrevote" } - // We just report that a timeout should be started. The executor must take care + val result = { ...defaultOutput, name: "timeout", timeout: "TimeoutPrevote" } + // We just report that a timeout should be started. The driver must take care // of figuring out whether it needs to record the round number and height per // timeout {cs: state, out: result} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } // line 36 -pure def ProposalAndPolkaAndValid (state: ConsensusState, ev: Event) : ConsResult = { - val auxState = { ...state, validValue: ev.value, validRound: state.round } +pure def ProposalAndPolkaAndValid (state: ConsensusState, input: ConsensusInput) : ConsResult = { + val auxState = { ...state, validValue: input.value, validRound: state.round } if (state.step == "Prevote") - val newstate = { ...auxState, lockedValue: ev.value, + val newstate = { ...auxState, lockedValue: input.value, lockedRound: state.round, step: "Precommit" } - val result = { ...defaultResult, name: "votemessage", + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, step: "Precommit", - id: ev.value}} + id: input.value}} {cs: newstate, out: result} else if (state.step == "Precommit") // TODO: check whether Daniel's comment // "if state > prevote, we should update the valid round!" // was properly addressed - {cs: auxState, out: defaultResult} + {cs: auxState, out: defaultOutput} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} // TODO: should we add the event to pending in this case. We would need to - // do this in the executor + // do this in the driver } // line 44 -pure def PolkaNil (state: ConsensusState, ev: Event) : ConsResult = { +pure def PolkaNil (state: ConsensusState, input: ConsensusInput) : ConsResult = { if (state.step == "Prevote") val newstate = { ...state, step: "Precommit"} - val result = { ...defaultResult, name: "votemessage", + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, @@ -314,39 +312,39 @@ pure def PolkaNil (state: ConsensusState, ev: Event) : ConsResult = { id: "nil"}} {cs: newstate, out: result} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } // line 47 -pure def PrecommitAny (state: ConsensusState, ev: Event) : ConsResult = { - val result = { ...defaultResult, name: "timeout", timeout: "TimeoutPrecommit" } +pure def PrecommitAny (state: ConsensusState, input: ConsensusInput) : ConsResult = { + val result = { ...defaultOutput, name: "timeout", timeout: "TimeoutPrecommit" } {cs: state, out: result} } // line 49 -pure def ProposalAndCommitAndValid (state: ConsensusState, ev: Event) : ConsResult = { +pure def ProposalAndCommitAndValid (state: ConsensusState, input: ConsensusInput) : ConsResult = { if (state.step != "decided") { val newstate = { ...state, step: "decided"} - val result = { ...defaultResult, name: "decided", decided: ev.value} + val result = { ...defaultOutput, name: "decided", decided: input.value} {cs: newstate, out: result} } else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } // line 55 -pure def RoundSkip (state: ConsensusState, ev: Event) : ConsResult = { - if (ev.round > state.round) - val result = { ...defaultResult, name: "skipRound", skipRound: ev.round } +pure def RoundSkip (state: ConsensusState, input: ConsensusInput) : ConsResult = { + if (input.round > state.round) + val result = { ...defaultOutput, name: "skipRound", skipRound: input.round } {cs: state, out: result} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } -pure def TimeoutPropose (state: ConsensusState, ev: Event) : ConsResult = { - if (ev.height == state.height and ev.round == state.round and state.step == "propose") +pure def TimeoutPropose (state: ConsensusState, input: ConsensusInput) : ConsResult = { + if (input.height == state.height and input.round == state.round and state.step == "propose") val newstate = { ...state, step: "Prevote"} - val result = { ...defaultResult, name: "votemessage", + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, @@ -354,14 +352,14 @@ pure def TimeoutPropose (state: ConsensusState, ev: Event) : ConsResult = { id: "nil"}} {cs: newstate, out: result} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } -pure def TimeoutPrevote (state: ConsensusState, ev: Event) : ConsResult = { - if (ev.height == state.height and ev.round == state.round and state.step == "Prevote") +pure def TimeoutPrevote (state: ConsensusState, input: ConsensusInput) : ConsResult = { + if (input.height == state.height and input.round == state.round and state.step == "Prevote") val newstate = { ...state, step: "Precommit"} // TODO: should we send precommit nil again ? - val result = { ...defaultResult, name: "votemessage", + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, @@ -369,17 +367,17 @@ pure def TimeoutPrevote (state: ConsensusState, ev: Event) : ConsResult = { id: "nil"}} {cs: newstate, out: result} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } -pure def TimeoutPrecommit (state: ConsensusState, ev: Event) : ConsResult = { - if (ev.height == state.height and ev.round == state.round) +pure def TimeoutPrecommit (state: ConsensusState, input: ConsensusInput) : ConsResult = { + if (input.height == state.height and input.round == state.round) // TODO: here we should call newRound. For this we would need to know whether // we are proposer for next round. - val result = {...defaultResult, name: "skipRound", skipRound: state.round + 1} + val result = {...defaultOutput, name: "skipRound", skipRound: state.round + 1} {cs: state, out: result} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } @@ -387,39 +385,39 @@ pure def TimeoutPrecommit (state: ConsensusState, ev: Event) : ConsResult = { * Main entry point * ********************************************************/ -pure def consensus (state: ConsensusState, ev: Event) : ConsResult = { - if (ev.name == "NewHeight") - NewHeight (state, ev) - else if (ev.name == "NewRoundProposer") - NewRoundProposer(state, ev) - else if (ev.name == "NewRound") - NewRound(state, ev) - else if (ev.name == "Proposal") - Proposal(state, ev) - else if (ev.name == "ProposalAndPolkaPreviousAndValid") - ProposalAndPolkaPreviousAndValid(state, ev) - else if (ev.name == "ProposalInvalid") - ProposalInvalid(state, ev) - else if (ev.name == "PolkaAny") - PolkaAny(state, ev) - else if (ev.name == "ProposalAndPolkaAndValid") - ProposalAndPolkaAndValid(state, ev) - else if (ev.name == "PolkaNil") - PolkaNil(state, ev) - else if (ev.name == "PrecommitAny") - PrecommitAny(state, ev) - else if (ev.name == "ProposalAndCommitAndValid") - ProposalAndCommitAndValid(state, ev) - else if (ev.name == "RoundSkip") - RoundSkip (state, ev) - else if (ev.name == "TimeoutPropose") - TimeoutPropose (state, ev) - else if (ev.name == "TimeoutPrevote") - TimeoutPrevote (state, ev) - else if (ev.name == "TimeoutPrecommit") - TimeoutPrecommit (state, ev) +pure def consensus (state: ConsensusState, input: ConsensusInput) : ConsResult = { + if (input.name == "NewHeight") + NewHeight (state, input) + else if (input.name == "NewRoundProposer") + NewRoundProposer(state, input) + else if (input.name == "NewRound") + NewRound(state, input) + else if (input.name == "Proposal") + Proposal(state, input) + else if (input.name == "ProposalAndPolkaPreviousAndValid") + ProposalAndPolkaPreviousAndValid(state, input) + else if (input.name == "ProposalInvalid") + ProposalInvalid(state, input) + else if (input.name == "PolkaAny") + PolkaAny(state, input) + else if (input.name == "ProposalAndPolkaAndValid") + ProposalAndPolkaAndValid(state, input) + else if (input.name == "PolkaNil") + PolkaNil(state, input) + else if (input.name == "PrecommitAny") + PrecommitAny(state, input) + else if (input.name == "ProposalAndCommitAndValid") + ProposalAndCommitAndValid(state, input) + else if (input.name == "RoundSkip") + RoundSkip (state, input) + else if (input.name == "TimeoutPropose") + TimeoutPropose (state, input) + else if (input.name == "TimeoutPrevote") + TimeoutPrevote (state, input) + else if (input.name == "TimeoutPrecommit") + TimeoutPrecommit (state, input) else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } } diff --git a/Specs/Quint/consensusTest.qnt b/Specs/Quint/consensusTest.qnt index fb7a2df24..2f2a79d45 100644 --- a/Specs/Quint/consensusTest.qnt +++ b/Specs/Quint/consensusTest.qnt @@ -8,9 +8,9 @@ import consensus.* from "./consensus" * Global state * ************************************************************************* */ -var system : Address_t -> ConsensusState -var _Result : ConsensusOutput -var _Event : Event +var system: Address_t -> ConsensusState +var _output: ConsensusOutput +var _input: ConsensusInput pure def initialProcess (name: Address_t) : ConsensusState = { @@ -19,8 +19,8 @@ pure def initialProcess (name: Address_t) : ConsensusState = { action init = all { system' = Map ("Josef" -> initialProcess("Josef")), - _Result' = defaultResult, - _Event' = { name : "Initial", + _output' = defaultOutput, + _input' = { name : "Initial", height : 0, round: -1, value: "", @@ -30,7 +30,7 @@ action init = all { // just to write a test. -action FireEvent(eventName: str, proc: Address_t, h: Height_t, r: Round_t, value: Value_t, vr: Round_t) : bool = all { +action FireInput(eventName: str, proc: Address_t, h: Height_t, r: Round_t, value: Value_t, vr: Round_t) : bool = all { val event = { name : eventName, height : h, round: r, @@ -39,86 +39,86 @@ action FireEvent(eventName: str, proc: Address_t, h: Height_t, r: Round_t, value val res = consensus(system.get(proc), event ) all { system' = system.put(proc, res.cs), - _Result' = res.out, - _Event' = event + _output' = res.out, + _input' = event } } action step = any { - nondet name = oneOf(ConsensusEvents) + nondet name = oneOf(ConsensusInputNames) nondet height = 1//oneOf(1.to(4)) nondet round = 0//oneOf(1.to(4)) nondet value = oneOf(Set("block 1", "block 2", "block 3")) nondet vr = oneOf(Set(-1, 1, 2, 3, 4)) - FireEvent(name, "Josef", height, round, value, vr) + FireInput(name, "Josef", height, round, value, vr) } action unchangedAll = all { system' = system, - _Result' = _Result, - _Event' = _Event, + _output' = _output, + _input' = _input, } // This test should call each event at least once run DecideNonProposerTest = { init - .then(FireEvent("NewRound", "Josef", 1, 0, "", -1)) + .then(FireInput("NewRound", "Josef", 1, 0, "", -1)) .then(all{ - assert(_Result.timeout == "TimeoutPropose"), - FireEvent("Proposal", "Josef", 1, 0, "block", -1)}) + assert(_output.timeout == "TimeoutPropose"), + FireInput("Proposal", "Josef", 1, 0, "block", -1)}) .then(all{ - assert(_Result.voteMessage.step == "Prevote" and _Result.voteMessage.id == "block"), - FireEvent("ProposalAndPolkaAndValid", "Josef", 1, 0, "block", -1)}) + assert(_output.voteMessage.step == "Prevote" and _output.voteMessage.id == "block"), + FireInput("ProposalAndPolkaAndValid", "Josef", 1, 0, "block", -1)}) .then(all{ - assert(_Result.voteMessage.step == "Precommit" and _Result.voteMessage.id == "block"), - FireEvent("ProposalAndCommitAndValid", "Josef", 1, 0, "block", -1)}) + assert(_output.voteMessage.step == "Precommit" and _output.voteMessage.id == "block"), + FireInput("ProposalAndCommitAndValid", "Josef", 1, 0, "block", -1)}) .then(all{ - assert(_Result.decided == "block"), - FireEvent("NewHeight", "Josef", system.get("Josef").height + 1, 0, "", -1)}) + assert(_output.decided == "block"), + FireInput("NewHeight", "Josef", system.get("Josef").height + 1, 0, "", -1)}) .then(all{ assert(system.get("Josef").height == 2), - FireEvent("NewRoundProposer", "Josef", 2, 0, "nextBlock", -1)}) + FireInput("NewRoundProposer", "Josef", 2, 0, "nextBlock", -1)}) .then(all{ - assert(_Result.timeout != "TimeoutPropose" and _Result.proposal.proposal == "nextBlock"), - FireEvent("Proposal", "Josef", 2, 0, "nextBlock", -1)}) // it is assumed that the proposer receives its own message + assert(_output.timeout != "TimeoutPropose" and _output.proposal.proposal == "nextBlock"), + FireInput("Proposal", "Josef", 2, 0, "nextBlock", -1)}) // it is assumed that the proposer receives its own message .then(all{ - assert(_Result.voteMessage.step == "Prevote" and system.get("Josef").step == "Prevote"), - FireEvent("PolkaAny", "Josef", 2, 0, "nextBlock", -1)}) + assert(_output.voteMessage.step == "Prevote" and system.get("Josef").step == "Prevote"), + FireInput("PolkaAny", "Josef", 2, 0, "nextBlock", -1)}) .then(all{ - assert(_Result.timeout == "TimeoutPrevote"), - FireEvent("TimeoutPrevote", "Josef", 2, 0, "nextBlock", -1)}) + assert(_output.timeout == "TimeoutPrevote"), + FireInput("TimeoutPrevote", "Josef", 2, 0, "nextBlock", -1)}) .then(all{ - assert(_Result.voteMessage.step == "Precommit" and _Result.voteMessage.id == "nil" and + assert(_output.voteMessage.step == "Precommit" and _output.voteMessage.id == "nil" and system.get("Josef").step == "Precommit"), - FireEvent("PrecommitAny", "Josef", 2, 0, "nextBlock", -1)}) + FireInput("PrecommitAny", "Josef", 2, 0, "nextBlock", -1)}) .then(all{ - assert(_Result.timeout == "TimeoutPrecommit"), - FireEvent("TimeoutPrecommit", "Josef", 2, 0, "nextBlock", -1)}) + assert(_output.timeout == "TimeoutPrecommit"), + FireInput("TimeoutPrecommit", "Josef", 2, 0, "nextBlock", -1)}) .then(all{ - assert(_Result.skipRound == 1), - FireEvent("NewRound", "Josef", 2, 1, "", -1)}) + assert(_output.skipRound == 1), + FireInput("NewRound", "Josef", 2, 1, "", -1)}) .then(all{ - assert(_Result.timeout == "TimeoutPropose"), - FireEvent("TimeoutPropose", "Josef", 2, 1, "nextBlock", -1)}) + assert(_output.timeout == "TimeoutPropose"), + FireInput("TimeoutPropose", "Josef", 2, 1, "nextBlock", -1)}) .then(all{ - assert(_Result.voteMessage.step == "Prevote" and _Result.voteMessage.id == "nil" and + assert(_output.voteMessage.step == "Prevote" and _output.voteMessage.id == "nil" and system.get("Josef").step == "Prevote"), - FireEvent("PolkaNil", "Josef", 2, 1, "nextBlock", -1)}) + FireInput("PolkaNil", "Josef", 2, 1, "nextBlock", -1)}) .then(all{ - assert(_Result.voteMessage.step == "Precommit" and _Result.voteMessage.id == "nil" and + assert(_output.voteMessage.step == "Precommit" and _output.voteMessage.id == "nil" and system.get("Josef").step == "Precommit"), - FireEvent("PrecommitAny", "Josef", 2, 1, "nextBlock", -1)}) + FireInput("PrecommitAny", "Josef", 2, 1, "nextBlock", -1)}) .then(all{ - assert(_Result.timeout == "TimeoutPrecommit"), - FireEvent("TimeoutPrecommit", "Josef", 2, 1, "nextBlock", -1)}) + assert(_output.timeout == "TimeoutPrecommit"), + FireInput("TimeoutPrecommit", "Josef", 2, 1, "nextBlock", -1)}) .then(all{ - assert(_Result.skipRound == 2), - FireEvent("NewRound", "Josef", 2, 2, "", -1)}) + assert(_output.skipRound == 2), + FireInput("NewRound", "Josef", 2, 2, "", -1)}) .then(all{ - assert(_Result.timeout == "TimeoutPropose"), - FireEvent("ProposalInvalid", "Josef", 2, 2, "", -1)}) + assert(_output.timeout == "TimeoutPropose"), + FireInput("ProposalInvalid", "Josef", 2, 2, "", -1)}) .then(all{ - assert(_Result.voteMessage.step == "Prevote" and _Result.voteMessage.id == "nil" and + assert(_output.voteMessage.step == "Prevote" and _output.voteMessage.id == "nil" and system.get("Josef").step == "Prevote"), unchangedAll }) diff --git a/Specs/Quint/coverage.md b/Specs/Quint/coverage.md new file mode 100644 index 000000000..6bb4f7258 --- /dev/null +++ b/Specs/Quint/coverage.md @@ -0,0 +1,43 @@ +# Tests for consensus statemachine (and sometimes driver) + +## Overview over covered consensus algorithm lines + +| line | comment | (C) | test | +| -----:| ---- | -----| -----| + 16 | reuse valid value | | line28Test.qnt + 18 | new value | X2 + 19 | send proposal | | (A) RoundswitchTest (^1) + 21 | start timeoutPropose | X1, X2b, X2c + 24 | prevote value | X1, X2 + 26 | prevote nil (on invalid or locked) | X2c + 30 | prevote value on old prevotes | | line28Test.qnt + 32 | prevote nil on old prevotes (on invalid or locked) | + 35 | start timeoutPrevote | X2 + 40 | precommit value | X1 + 42 without 41 | set valid without locked | | line42Test + 45 | precommit nil | X2b + 48 | start timeoutPrecommit | X2 , X2b + 51 | decide | X1 + 56 | skip round | | (A) RoundswitchTest + 57 | OnTimeoutPropose | X2b + 61 | OnTimeOutPrevote | X2 + 64 | OnTimeOutPrecommit | X2, X2b + +## Comments + +- (C) + - refers to DecideNonProposerTest in consensusTest.qnt. + - X1 covered in height 1, X2b: covered in height 2 round 2, etc. + - is only containing the consensus state machine. No driver + - contains an event to go to height 1 +- (A) asyncModelsTest.qnt +- ^1 ThreeDecideInRound1V4stillinZeroTest delivers proposal so it must have been sent before + + +## Other tests + +- asyncModelsTest.qnt + - DisagreementTest: 2/4 faulty lead to disagreement + - three processes go to round 1 and decide, on process left behind. Test whether process decides + - DecideForFutureRoundTest: first receives proposal then precommits + - DecideOnProposalTest: first receives precommits then proposal \ No newline at end of file diff --git a/Specs/Quint/executor.qnt b/Specs/Quint/driver.qnt similarity index 74% rename from Specs/Quint/executor.qnt rename to Specs/Quint/driver.qnt index 6aeb71a6a..2715dc83d 100644 --- a/Specs/Quint/executor.qnt +++ b/Specs/Quint/driver.qnt @@ -1,11 +1,11 @@ // -*- mode: Bluespec; -*- /* - TODO: round switch upon f+1 messages from the future is not done yet. We need to catch - the event from the bookkeeper + TODO: round switch upon f+1 messages from the future is not done yet. + We need to catch the event from the bookkeeper */ -module executor { +module driver { import consensus.* from "./consensus" import voteBookkeeper.* from "./voteBookkeeper" @@ -14,73 +14,73 @@ pure def initBookKeeper(totalVotingPower: int): Bookkeeper = { height: 0, totalWeight: totalVotingPower, rounds: Map() } -type ExecutorState = { +type DriverState = { bk : Bookkeeper, cs : ConsensusState, - proposals: Set[ProposeMsg_t], + proposals: Set[Proposal_t], valset: Address_t -> int, - executedEvents: List[(Event, Height_t, Round_t)], // We record that to have the information in the trace - pendingEvents: Set[(Event, Height_t, Round_t)], + executedInputs: List[(ConsensusInput, Height_t, Round_t)], // We record that to have the information in the trace + pendingInputs: Set[(ConsensusInput, Height_t, Round_t)], started: bool, - applyvotesResult: ExecutorEvent, //debug TODO + voteKeeperOutput: VoteKeeperOutput, //debug TODO chain : List[Value_t], nextValueToPropose: Value_t, } -pure def initExecutor (v: Address_t, vs: Address_t -> int) : ExecutorState = { +pure def initDriver (v: Address_t, vs: Address_t -> int) : DriverState = { val tvp = vs.keys().fold(0, (sum, key) => sum + vs.get(key)) { bk: initBookKeeper(tvp), cs: initConsensusState(v), proposals: Set(), valset: vs, - executedEvents: List(), - pendingEvents: Set(), + executedInputs: List(), + pendingInputs: Set(), started: false, - applyvotesResult: toEvent(0, "", {name: "", value: ""}), // debug + voteKeeperOutput: toVoteKeeperOutput(0, "", {name: "", value: ""}), // debug chain : List(), nextValueToPropose: "", } } type NodeState = { - es: ExecutorState, + es: DriverState, timeout: Set[(Timeout_t, Height_t, Round_t)], - incomingVotes: Set[VoteMsg_t], - incomingProposals: Set[ProposeMsg_t], + incomingVotes: Set[Vote_t], + incomingProposals: Set[Proposal_t], } pure def initNode (v: Address_t, vs: Address_t -> int) : NodeState = { - es: initExecutor(v,vs), + es: initDriver(v,vs), timeout: Set(), incomingVotes: Set(), incomingProposals: Set(), } -type ExecutorInput = { +type DriverInput = { name: str, // TODO: make a set of values. - proposal: ProposeMsg_t, - vote: VoteMsg_t, + proposal: Proposal_t, + vote: Vote_t, timeout: str, - event: Event, + csInput: ConsensusInput, nextValueToPropose: Value_t } -val defaultInput: ExecutorInput = { +val defaultInput: DriverInput = { name: "", proposal: { src: "", height: 0, round: 0, proposal: "", validRound: 0 }, vote: { src: "", height: 0, round: 0, step: "", id: "", }, timeout: "", - event: defaultEvent, + csInput: defaultConsensusInput, nextValueToPropose: "" } // this is to match the type from the bookkeeper. When we add heights there we should // unify -pure def toVote (v: VoteMsg_t) : Vote = +pure def toVote (v: Vote_t) : Vote = { typ: v.step, height: v.height, round: v.round, value: v.id, address: v.src } -val defaultEvent : Event = { name : "", height : 0, round: 0, value: "", vr: 0 } +val defaultConsensusInput : ConsensusInput = { name : "", height : 0, round: 0, value: "", vr: 0 } /* encode the following decision tree @@ -104,7 +104,7 @@ Prevote -> feed all events to Consensus */ -val emptyProposal : ProposeMsg_t= +val emptyProposal : Proposal_t= { src: "none", height: 0, round: 0, proposal: "none", validRound: 0 } val emptyVote = @@ -125,9 +125,9 @@ pure def Proposer(valset: Address_t -> int, height: Height_t, round: Round_t) : else "v4" } -pure def getValue(es: ExecutorState) : Value_t = es.nextValueToPropose +pure def getValue(es: DriverState) : Value_t = es.nextValueToPropose -pure def valid(p: ProposeMsg_t) :bool = { +pure def valid(p: Proposal_t) :bool = { // for simulation, if the value is "invalid", so is the proposal // if this is to become "non-deterministic", we must push it // and its use into the state machine @@ -139,8 +139,8 @@ pure def id(v) = v type ConsensusCall = { - es: ExecutorState, - event: Event, + es: DriverState, + csInput: ConsensusInput, out: ConsensusOutput } @@ -148,24 +148,24 @@ pure def ListContains(list, value) = list.foldl(false, (s,x) => s or x == value) // check whether the event has been already sent to consensus. If not, do so. -pure def callConsensus (es: ExecutorState, bk: Bookkeeper, ev: Event) : (ExecutorState, ConsensusOutput) = { +pure def callConsensus (es: DriverState, bk: Bookkeeper, csInput: ConsensusInput) : (DriverState, ConsensusOutput) = { // Check whether we already executed the event already - if (es.executedEvents.ListContains((ev, es.cs.height, es.cs.round))) - ({ ...es, bk: bk, cs: es.cs }, defaultResult) + if (es.executedInputs.ListContains((csInput, es.cs.height, es.cs.round))) + ({ ...es, bk: bk, cs: es.cs }, defaultOutput) else // Go to consensus - val res = consensus(es.cs, ev) + val res = consensus(es.cs, csInput) // Record that we executed the event - val events = es.executedEvents.append((ev, res.cs.height, res.cs.round)) + val csInputs = es.executedInputs.append((csInput, res.cs.height, res.cs.round)) - ({ ...es, bk: bk, cs: res.cs, executedEvents: events }, res.out) + ({ ...es, bk: bk, cs: res.cs, executedInputs: csInputs }, res.out) } -// We do this if the executor receives a Precommit -pure def Precommit (es: ExecutorState, input: ExecutorInput, eev: ExecutorEvent) : (ExecutorState, ConsensusOutput) = { - if (eev.name == "PrecommitValue") - if (es.proposals.exists(x => eev.round == x.round and eev.value == id(x.proposal))) { +// We do this if the driver receives a Precommit +pure def Precommit (es: DriverState, input: DriverInput, vkOutput: VoteKeeperOutput) : (DriverState, ConsensusOutput) = { + if (vkOutput.name == "PrecommitValue") + if (es.proposals.exists(x => vkOutput.round == x.round and vkOutput.value == id(x.proposal))) { callConsensus(es, es.bk, { name : "ProposalAndCommitAndValid", height : input.vote.height, round: input.vote.round, @@ -173,14 +173,14 @@ pure def Precommit (es: ExecutorState, input: ExecutorInput, eev: ExecutorEvent) vr: -1}) } else { - if (eev.round == es.cs.round) { + if (vkOutput.round == es.cs.round) { callConsensus(es, es.bk, { name: "PrecommitAny", height: input.vote.height, round: input.vote.round, value: input.vote.id, vr: -1}) } - else if (eev.round > es.cs.round) { + else if (vkOutput.round > es.cs.round) { // if it is for a future round I can trigger skipround // TODO: should we really do this. It is dead code as the f+1 event already happened callConsensus(es, es.bk, { name: "RoundSkip", @@ -191,17 +191,17 @@ pure def Precommit (es: ExecutorState, input: ExecutorInput, eev: ExecutorEvent) } else { // messages from past round -> ignore - (es, defaultResult) + (es, defaultOutput) } } - else if (eev.name == "PrecommitAny" and eev.round == es.cs.round) { + else if (vkOutput.name == "PrecommitAny" and vkOutput.round == es.cs.round) { callConsensus(es, es.bk, { name: "PrecommitAny", height: input.vote.height, round: input.vote.round, value: input.vote.id, vr: -1}) } - else if (eev.name == "Skip" and eev.round > es.cs.round) + else if (vkOutput.name == "Skip" and vkOutput.round > es.cs.round) callConsensus(es, es.bk, { name: "RoundSkip", height: input.vote.height, round: input.vote.round, @@ -209,84 +209,99 @@ pure def Precommit (es: ExecutorState, input: ExecutorInput, eev: ExecutorEvent) vr: -1}) else // none of the supported Precommit events. Do nothing - (es, defaultResult) + (es, defaultOutput) } -// We do this if the executor receives a Prevote -pure def Prevote (es: ExecutorState, input: ExecutorInput, eev: ExecutorEvent) : (ExecutorState, ConsensusOutput) = { +// We do this if the driver receives a Prevote +pure def Prevote (es: DriverState, input: DriverInput, vkOutput: VoteKeeperOutput) : (DriverState, ConsensusOutput) = { // TODO: events do not have heights now. // TODO: Polka implications missing. - if (eev.name == "PolkaValue") - if (eev.round < es.cs.round and + if (vkOutput.name == "PolkaValue") + if (vkOutput.round < es.cs.round and es.proposals.exists(p => p.round == es.cs.round and - eev.round == p.validRound and id(p.proposal) == eev.value)) + vkOutput.round == p.validRound and id(p.proposal) == vkOutput.value)) callConsensus(es, es.bk, { name: "ProposalAndPolkaPreviousAndValid", height: es.cs.height, round: es.cs.round, - value: eev.value, - vr: eev.round}) + value: vkOutput.value, + vr: vkOutput.round}) // TODO: the value should come from the proposal - else if (eev.round == es.cs.round and - es.proposals.exists(p => p.round == es.cs.round and - id(p.proposal) == eev.value)) - callConsensus(es, es.bk, { name: "ProposalAndPolkaAndValid", + else if (vkOutput.round == es.cs.round) + if (es.proposals.exists(p => p.round == es.cs.round and + id(p.proposal) == vkOutput.value)) + val pend = ( { name: "ProposalAndPolkaAndValid", height: es.cs.height, round: es.cs.round, - value: eev.value, - vr: eev.round}) + value: vkOutput.value, + vr: vkOutput.round}, es.cs.height, es.cs.round) + callConsensus( { ...es, pendingInputs: es.pendingInputs.union(Set(pend)) }, + es.bk, + { name: "PolkaAny", + height: es.cs.height, + round: es.cs.round, + value: vkOutput.value, + vr: vkOutput.round}) + else + // there is no matching proposal + callConsensus(es, es.bk, { name: "PolkaAny", + height: es.cs.height, + round: es.cs.round, + value: vkOutput.value, + vr: vkOutput.round}) + else - // we don't have a matching proposal so we do nothing + // It is for a future round // TODO: we might check whether it is for a future round and jump - (es, defaultResult) - else if (eev.name == "PolkaAny") - if (eev.round == es.cs.round) + (es, defaultOutput) + else if (vkOutput.name == "PolkaAny") + if (vkOutput.round == es.cs.round) // call consensus and remember that we did it callConsensus(es, es.bk, { name: "PolkaAny", height: es.cs.height, round: es.cs.round, - value: eev.value, - vr: eev.round}) + value: vkOutput.value, + vr: vkOutput.round}) else // TODO: we might check whether it is for a future round and jump - (es, defaultResult) - else if (eev.name == "PolkaNil" and eev.round == es.cs.round) + (es, defaultOutput) + else if (vkOutput.name == "PolkaNil" and vkOutput.round == es.cs.round) callConsensus(es, es.bk, { name: "PolkaNil", height: es.cs.height, round: es.cs.round, - value: eev.value, - vr: eev.round}) - else if (eev.name == "Skip" and eev.round > es.cs.round) + value: vkOutput.value, + vr: vkOutput.round}) + else if (vkOutput.name == "Skip" and vkOutput.round > es.cs.round) callConsensus(es, es.bk, { name: "RoundSkip", height: input.vote.height, round: input.vote.round, value: input.vote.id, vr: -1}) else - (es, defaultResult) + (es, defaultOutput) } -// We do this if a timeout expires at the executor -pure def Timeout (es: ExecutorState, input: ExecutorInput) : (ExecutorState, ConsensusOutput) = { +// We do this if a timeout expires at the driver +pure def Timeout (es: DriverState, input: DriverInput) : (DriverState, ConsensusOutput) = { // TODO: We assume that the timeout event is always for the current round. If this is not // the case, we need to encode it in the input to which round the timeout belongs - val event: Event = {name: input.timeout, + val csInput: ConsensusInput = {name: input.timeout, height: es.cs.height, round: es.cs.round, value: "", vr: 0} - callConsensus(es, es.bk, event) + callConsensus(es, es.bk, csInput) } -// We do this if the executor receives a proposal -pure def ProposalMsg (es: ExecutorState, input: ExecutorInput) : (ExecutorState, ConsensusOutput) = { +// We do this if the driver receives a proposal +pure def ProposalMsg (es: DriverState, input: DriverInput) : (DriverState, ConsensusOutput) = { val newES = { ...es, proposals: es.proposals.union(Set(input.proposal))} if (input.proposal.src != Proposer(es.valset, input.proposal.height, input.proposal.round)) // proposer does not match the height/round of the proposal // keep ES (don't use newES here), that is, drop proposal - (es, defaultResult) + (es, defaultOutput) else if (valid(input.proposal)) val receivedCommit = checkThreshold( newES.bk, input.proposal.round, @@ -307,7 +322,7 @@ pure def ProposalMsg (es: ExecutorState, input: ExecutorInput) : (ExecutorState, else if (input.proposal.round != es.cs.round or input.proposal.height != es.cs.height) // the proposal is from the right proposer and valid, but not for this round // keep the proposal, do nothing else - (newES, defaultResult) + (newES, defaultOutput) else // for current round and q, valid, and from right proposer val receivedPolkaValidRoundVal = checkThreshold(newES.bk, @@ -352,11 +367,11 @@ pure def ProposalMsg (es: ExecutorState, input: ExecutorInput) : (ExecutorState, value: id(input.proposal.proposal), vr: input.proposal.validRound}) else - (newES, defaultResult) + (newES, defaultOutput) else if (newES.cs.step == "Prevote" or newES.cs.step == "Precommit") if (receivedCommitCurrentVal) // here we need to call both, Commit and Polka. - // We do commit and append pola to pending + // We do commit and append polka to pending val pend = ( { name: "ProposalAndPolkaAndValid", height: newES.cs.height, round: newES.cs.round, @@ -364,7 +379,7 @@ pure def ProposalMsg (es: ExecutorState, input: ExecutorInput) : (ExecutorState, vr: input.proposal.validRound}, newES.cs.height, newES.cs.round) - callConsensus( { ...newES, pendingEvents: newES.pendingEvents.union(Set(pend))}, + callConsensus( { ...newES, pendingInputs: newES.pendingInputs.union(Set(pend))}, newES.bk, { name: "ProposalAndCommitAndValid", height: newES.cs.height, @@ -380,34 +395,34 @@ pure def ProposalMsg (es: ExecutorState, input: ExecutorInput) : (ExecutorState, value: id(input.proposal.proposal), vr: input.proposal.validRound}) else - (newES, defaultResult) + (newES, defaultOutput) else - (newES, defaultResult) + (newES, defaultOutput) else // (not(valid(input.proposal))) // keep ES (don't use newES here), that is, drop proposal if (es.cs.step == "propose" and es.cs.round == input.proposal.round and es.cs.height == input.proposal.height) if (checkThreshold(es.bk, es.cs.round, "Prevote", {name: "Value", value: id(input.proposal.proposal)})) - val event: Event = {name: "ProposalAndPolkaAndInValid", + val csInput: ConsensusInput = {name: "ProposalAndPolkaAndInValid", height: es.cs.height, round: es.cs.round, value: id(input.proposal.proposal), vr: input.proposal.validRound} - callConsensus(es, es.bk, event) + callConsensus(es, es.bk, csInput) else - val event: Event = {name: "ProposalInvalid", + val csInput: ConsensusInput = {name: "ProposalInvalid", height: es.cs.height, round: es.cs.round, value: id(input.proposal.proposal), vr: input.proposal.validRound} - callConsensus(es, es.bk, event) + callConsensus(es, es.bk, csInput) else - (es, defaultResult) + (es, defaultOutput) } // We do this when we need to jump to a new round -pure def skip (es: ExecutorState, r: int) : (ExecutorState, ConsensusOutput) = { +pure def skip (es: DriverState, r: int) : (DriverState, ConsensusOutput) = { // line 15 val prop = if (es.cs.validValue != "nil") es.cs.validValue else getValue(es) @@ -430,15 +445,15 @@ pure def skip (es: ExecutorState, r: int) : (ExecutorState, ConsensusOutput) = { // We do this when we have decided -pure def decided (es: ExecutorState, res: ConsensusOutput) : (ExecutorState, ConsensusOutput) = { +pure def decided (es: DriverState, res: ConsensusOutput) : (DriverState, ConsensusOutput) = { // here we call consensus to set a new height, that is, to initialize the state machine // and then we call skip to start round 0 /* // The following can be used to get to the next height. For now this // function does nothing - // If we choose to move getValue out of the executor logic into the environment (gossip) + // If we choose to move getValue out of the driver logic into the environment (gossip) // then, we would not do this here, but expect the environment to create a (to be defined) - // ExecutorInput + // DriverInput val s1 = callConsensus(es, es.bk, {name : "NewHeight", height : es.cs.height + 1, round: -1, @@ -450,16 +465,20 @@ pure def decided (es: ExecutorState, res: ConsensusOutput) : (ExecutorState, Con } -// take input out of pending events and then call consensus with that event -// We do this when the executor is asked to work on pending events -pure def PendingEvent (es: ExecutorState, input: ExecutorInput) : (ExecutorState, ConsensusOutput) = { - val newState = { ...es, pendingEvents: es.pendingEvents.exclude(Set((input.event, es.cs.height, es.cs.round)))} - callConsensus(newState, es.bk, input.event) +// take input out of pending inputs and then call consensus with that input +// We do this when the driver is asked to work on pending events +pure def PendingInput (es: DriverState): (DriverState, ConsensusOutput) = { + val ev = es.pendingInputs.fold((defaultConsensusInput, -1, -1), (sum, y) => y) + val newState = { ...es, pendingInputs: es.pendingInputs.exclude(Set(ev))} + if (ev._2 == es.cs.height and ev._3 == es.cs.round) + callConsensus(newState, es.bk, ev._1) + else + (newState, defaultOutput) } -pure def setValue(es: ExecutorState, value: Value_t) : (ExecutorState, ConsensusOutput) = - ({ ...es, nextValueToPropose: value }, defaultResult) +pure def setValue(es: DriverState, value: Value_t) : (DriverState, ConsensusOutput) = + ({ ...es, nextValueToPropose: value }, defaultOutput) @@ -468,8 +487,8 @@ pure def setValue(es: ExecutorState, value: Value_t) : (ExecutorState, Consensus * Main entry point * ********************************************************/ -// TODO: return ConsensusEvent so that we know from outside what event was fired. -pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, ConsensusOutput) = { +// TODO: return ConsensusInput so that we know from outside what event was fired. +pure def driver (es: DriverState, input: DriverInput) : (DriverState, ConsensusOutput) = { // TODO: shall we check whether the sender actually is in the validator set if (input.name == "proposal") { val res = ProposalMsg(es, input) @@ -482,9 +501,9 @@ pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, Co } else if (input.name == "votemessage" and input.vote.step == "Precommit") { val res = applyVote(es.bk, toVote(input.vote), es.valset.get(input.vote.src), es.cs.round) - val newES = { ...es, bk: res.bookkeeper, applyvotesResult: res.event} + val newES = { ...es, bk: res.bookkeeper, voteKeeperOutput: res.output } // only a commit event can come here. - val cons_res = Precommit(newES, input, res.event) + val cons_res = Precommit(newES, input, res.output) if (cons_res._2.name == "decided") decided (cons_res._1, cons_res._2) else if (cons_res._2.name == "skipRound") @@ -494,9 +513,9 @@ pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, Co } else if (input.name == "votemessage" and input.vote.step == "Prevote") { val res = applyVote(es.bk, toVote(input.vote), es.valset.get(input.vote.src), es.cs.round) - val newES = { ...es, bk: res.bookkeeper, applyvotesResult: res.event} + val newES = { ...es, bk: res.bookkeeper, voteKeeperOutput: res.output} // only a commit event can come here. - val cons_res = Prevote(newES, input, res.event) + val cons_res = Prevote(newES, input, res.output) if (cons_res._2.name == "decided") // TODO: dead branch. But we should put this after consensus call logic into a function decided (cons_res._1, cons_res._2) @@ -511,8 +530,8 @@ pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, Co if (res._2.name == "skipRound") skip (res._1, res._2.skipRound) // skip starts a new round. This may involve getValue. If we choose to move the getValue - // logic out of the executor, we wouldn't call skip here but add a (to be defined) - // ExecutorInput + // logic out of the driver, we wouldn't call skip here but add a (to be defined) + // DriverInput else res } @@ -522,12 +541,12 @@ pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, Co skip (new, 0) } else if (input.name == "pending") { - PendingEvent(es, input) + PendingInput(es) } else if (input.name == "SetNextProposedValue") setValue(es, input.nextValueToPropose) else - (es, defaultResult) + (es, defaultOutput) } @@ -535,10 +554,16 @@ pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, Co // timeouts, etc.) the node should act. // currently this is linked in via the state machine. But we can move it into // the functional layer/ -pure def nextAction (state: NodeState) : (NodeState, ExecutorInput) = { +pure def nextAction (state: NodeState) : (NodeState, DriverInput) = { if (not(state.es.started)) (state, { ...defaultInput, name: "start" }) + else if (state.es.pendingInputs != Set()) + // this might be cheating as we look into the "es" + (state, { ...defaultInput, name: "pending" }) + // I DID IT. TODO: In the "starkBFT Spec" Google doc, it is written that pending events + // should be executed before new messages, which would requir to push this + // branch up. else if (state.incomingProposals != Set()) // pick proposal, remove it from incoming // val prop = state.incomingProposals.chooseSome() @@ -562,22 +587,19 @@ pure def nextAction (state: NodeState) : (NodeState, ExecutorInput) = { val timeout = timeouts.fold(("", 0, 0), (sum, y) => y) val newstate = { ...state, timeout: state.timeout.exclude(Set(timeout))} (newstate, { ...defaultInput, name: "timeout", timeout: timeout._1}) - - else if (state.es.pendingEvents != Set()) - // this might be cheating as we look into the "es" - (state, { ...defaultInput, name: "pending" }) - // TODO: In the "starkBFT Spec" Google doc, it is written that pending events - // should be executed before new messages, which would requir to push this - // branch up. else (state, defaultInput) } // This function can be used to control test runs better. -pure def nextActionCommand (state: NodeState, command: str) : (NodeState, ExecutorInput) = { +pure def nextActionCommand (state: NodeState, command: str) : (NodeState, DriverInput) = { if (command == "start" and not(state.es.started)) (state, { ...defaultInput, name: "start" }) + else if (command == "pending" and state.es.pendingInputs != Set()) + // this might be cheating as we look into the "es" + (state, { ...defaultInput, name: "pending" }) + else if (command == "proposal" and state.incomingProposals != Set()) // pick proposal, remove it from incoming // val prop = state.incomingProposals.chooseSome() @@ -602,10 +624,6 @@ pure def nextActionCommand (state: NodeState, command: str) : (NodeState, Execut val newstate = { ...state, timeout: state.timeout.exclude(Set(timeout))} (newstate, { ...defaultInput, name: "timeout", timeout: timeout._1}) - else if (command == "pending" and state.es.pendingEvents != Set()) - // this might be cheating as we look into the "es" - (state, { ...defaultInput, name: "pending" }) - else (state, defaultInput) } diff --git a/Specs/Quint/line28Test.qnt b/Specs/Quint/line28Test.qnt new file mode 100644 index 000000000..2902c7c67 --- /dev/null +++ b/Specs/Quint/line28Test.qnt @@ -0,0 +1,34 @@ +// -*- mode: Bluespec; -*- + +module line28Test { + +import line28run( + validators = Set("v1", "v2", "v3", "v4"), + validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), + Faulty = Set("v1"), + Values = Set("red", "blue"), + Rounds = Set(0, 1, 2, 3), + Heights = Set(0), // , 1, 2, 3) + otherSet = Set("v2", "v4") +) as N4F1 from "./line28run" + +run line28Test = { + N4F1::runToLine28 +} + +import line28run( + validators = Set("v1", "v2", "v3", "v4", "v5", "v6", "v7"), + validatorSet = Set("v1", "v2", "v3", "v4", "v5", "v6", "v7").mapBy(x => 1), + Faulty = Set("v1"), + Values = Set("red", "blue"), + Rounds = Set(0, 1, 2, 3), + Heights = Set(0), // , 1, 2, 3) + otherSet = Set("v2", "v4", "v6", "v7") +) as N7F1 from "./line28run" + +run Bigline28Test = { + N7F1::runToLine28 +} + + +} \ No newline at end of file diff --git a/Specs/Quint/line28run.qnt b/Specs/Quint/line28run.qnt new file mode 100644 index 000000000..1f8cf7374 --- /dev/null +++ b/Specs/Quint/line28run.qnt @@ -0,0 +1,40 @@ +// -*- mode: Bluespec; -*- + +module line28run { + +import TendermintDSL.* from "./TendermintDSL" +export TendermintDSL.* + +const otherSet : Set[Address_t] +val others = otherSet.fold(List(), (s, x) => s.append(x)) + +run runToLine28 = { + val nextProposer = Proposer (validatorSet, 0, 1) + init + .then(all { + // others should be at most 2/3. + // if this assertion fails the set need to be set differently + assert(3 * size(otherSet) <= 2 * size(validators)), + assert(3 * size(otherSet.union(Faulty)) > 2 * size(validators)), + everyoneReceivesProposal(correctList, validatorList, validatorSet, 0, 0, "blue") + }) + // receive all prevotes + .then(fromPrevoteToPrecommit (correctList, correctList, validatorList, validatorSet, 0, 0, "blue")) + // now the faulty nodes precommit nil + .then(ListDeliverAllVotes("Precommit", faultyList, correctList, validatorSet, 0, 0, "nil")) + .then(faultyList.length().reps(_ => ListTakeAStep(correctList))) + // now the other precommits are delivered, so that timeoutPrecommit is started + .then(ListDeliverAllVotes("Precommit", others, correctList, validatorSet, 0, 0, "blue")) + .then(others.length().reps(_ => ListTakeAStep(correctList))) + // TimeoutPrecommit is there an can fire and bring is to the next round. + .then(all{ + assert(system.get(nextProposer).timeout.contains(("TimeoutPrecommit", 0, 0))), + everyoneReceivesProposal(correctList, validatorList, validatorSet, 0, 0, "red") + }) + .then(all{ + assert(voteBuffer.get(nextProposer).contains( { height: 0, id: "blue", round: 1, src: nextProposer, step: "Prevote" })), + unchangedAll + }) +} + +} \ No newline at end of file diff --git a/Specs/Quint/line42Test.qnt b/Specs/Quint/line42Test.qnt new file mode 100644 index 000000000..900afcf14 --- /dev/null +++ b/Specs/Quint/line42Test.qnt @@ -0,0 +1,19 @@ +// -*- mode: Bluespec; -*- + +module line42Test { + +import line42run( + validators = Set("v1", "v2", "v3", "v4"), + validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), + Faulty = Set(), + Values = Set("red", "blue"), + Rounds = Set(0, 1, 2, 3), + Heights = Set(0), // , 1, 2, 3) + testedVal = "v4" +) as N4F0 from "./line42run" + +run line42Test = { + N4F0::runToLine42 +} + +} \ No newline at end of file diff --git a/Specs/Quint/line42run.qnt b/Specs/Quint/line42run.qnt new file mode 100644 index 000000000..5da4398fd --- /dev/null +++ b/Specs/Quint/line42run.qnt @@ -0,0 +1,48 @@ +// -*- mode: Bluespec; -*- + +module line42run { + +import TendermintDSL.* from "./TendermintDSL" +export TendermintDSL.* + +const testedVal : Address_t +val others = validators.exclude(Set(testedVal)) +val othersList = others.fold(List(), (s, x) => s.append(x)) + +run runToLine42 = { + val value = "blue" + init + .then(valStep(testedVal)) + .then(everyoneReceivesProposal(othersList, validatorList, validatorSet, 0, 0, value)) + .then(fromPrevoteToPrecommit(othersList, othersList, validatorList, validatorSet, 0, 0, value)) + // At this point we have set up the environment for "testedVal" to reach line 42 without + // any other process taking any steps + .then(all{ + assert(system.get(testedVal).timeout.contains(("TimeoutPropose", 0, 0))), + valStep(testedVal) + }) + .then(ProcessDeliverAllVotes("Prevote", testedVal, othersList, validatorSet, 0, 0, value)) + .then(othersList.length().reps(_ => valStep(testedVal))) + .then(all{ + assert(system.get(testedVal).timeout.contains(("TimeoutPrevote", 0, 0))), + valStep(testedVal) + }) + .then(all{ + assert(system.get(testedVal).es.cs.step == "Precommit"), + deliverSomeProposal(testedVal) + }) + .then(valStep(testedVal)) // here it executes line 36 with branch 42 + .then(all{ + val cstate = system.get(testedVal).es.cs + assert(all{ + cstate.lockedRound == -1, + cstate.lockedValue == "nil", + cstate.validRound == 0, + cstate.validValue == value + }), + unchangedAll + }) +} + +} + diff --git a/Specs/Quint/parameterizedTest.qnt b/Specs/Quint/parameterizedTest.qnt index cef260e93..b3e766a77 100644 --- a/Specs/Quint/parameterizedTest.qnt +++ b/Specs/Quint/parameterizedTest.qnt @@ -83,4 +83,5 @@ run multiRoundTest = { } + } \ No newline at end of file diff --git a/Specs/Quint/statemachineAsync.qnt b/Specs/Quint/statemachineAsync.qnt index f714141d8..e8b11a28c 100644 --- a/Specs/Quint/statemachineAsync.qnt +++ b/Specs/Quint/statemachineAsync.qnt @@ -16,8 +16,8 @@ module statemachineAsync { -import executor.* from "./executor" -export executor.* +import driver.* from "./driver" +export driver.* import consensus.* from "./consensus" export consensus.* import voteBookkeeper.* from "./voteBookkeeper" @@ -38,26 +38,26 @@ const Heights : Set[Height_t] val RoundsOrNil = Rounds.union(Set(-1)) val Steps = Set("Prevote", "Precommit") -val AllFaultyVotes : Set[VoteMsg_t] = - tuples(Faulty, Heights, Rounds, Values, Steps) +val AllFaultyVotes : Set[Vote_t] = + tuples(Faulty, Heights, Rounds, Values.union(Set("nil")), Steps) .map(t => { src: t._1, height: t._2, round: t._3, id: t._4, step: t._5 }) -// val AllFaultyVotes : Set[VoteMsg_t] = +// val AllFaultyVotes : Set[Vote_t] = // tuples(Faulty, Heights, Rounds, Values, Steps) // .map(((p, h, r, v, s)) => { src: p, height: h, round: r, id: v, step: s }) -val AllFaultyProposals : Set[ProposeMsg_t] = +val AllFaultyProposals : Set[Proposal_t] = tuples(Faulty, Heights, Rounds, Values, RoundsOrNil) .map(t => { src: t._1, height: t._2, round: t._3, proposal: t._4, validRound: t._5 }) // Global State var system : Address_t -> NodeState -var propBuffer : Address_t -> Set[ProposeMsg_t] -var voteBuffer : Address_t -> Set[VoteMsg_t] -var _hist: { validator: Address_t, input: ExecutorInput, output: ConsensusOutput } +var propBuffer : Address_t -> Set[Proposal_t] +var voteBuffer : Address_t -> Set[Vote_t] +var _hist: { validator: Address_t, input: DriverInput, output: ConsensusOutput } -val ConsensusOutputInv = consensusOutputs.union(Set(defaultResult.name)).contains(_hist.output.name) +val ConsensusOutputInv = consensusOutputs.union(Set(defaultOutput.name)).contains(_hist.output.name) action unchangedAll = all { @@ -77,22 +77,23 @@ action init = all { system' = Correct.mapBy(v => initNode(v, validatorSet)), propBuffer' = Correct.mapBy(v => Set()), voteBuffer' = Correct.mapBy(v => Set()), - _hist' = { validator: "INIT", input: defaultInput, output: defaultResult } + _hist' = { validator: "INIT", input: defaultInput, output: defaultOutput } } // Put the proposal into the buffers of all validators -pure def sendProposal (buffer: Address_t -> Set[ProposeMsg_t], prop: ProposeMsg_t) : Address_t -> Set[ProposeMsg_t] = { +pure def sendProposal (buffer: Address_t -> Set[Proposal_t], prop: Proposal_t) : Address_t -> Set[Proposal_t] = { buffer.keys().mapBy(x => { buffer.get(x).union(Set(prop)) }) } // Put the vote into the inbuffers of all validators -pure def sendVote (sys: Address_t -> Set[VoteMsg_t], vote: VoteMsg_t) : Address_t -> Set[VoteMsg_t] = { +pure def sendVote (sys: Address_t -> Set[Vote_t], vote: Vote_t) : Address_t -> Set[Vote_t] = { sys.keys().mapBy(x => { ...sys.get(x).union(Set(vote)) }) } // Record that a timeout has started at node v +// As we do set union here, there is no need to check whether this happens the first time pure def startTimeout (sys: Address_t -> NodeState, v: Address_t, toName: str) : Address_t -> NodeState = { sys.put(v, { ...sys.get(v), timeout: sys.get(v).timeout.union(Set( {(toName, sys.get(v).es.cs.height, sys.get(v).es.cs.round)} @@ -101,11 +102,11 @@ pure def startTimeout (sys: Address_t -> NodeState, v: Address_t, toName: str) : action valStep(v: Address_t) : bool = { // pick action - val input = system.get(v).nextAction() // TODO: nextAction could go within executor boundary + val input = system.get(v).nextAction() // TODO: nextAction could go within driver boundary // remove action from v val sys1 = system.put(v, input._1) - // call executor - val res = executor(sys1.get(v).es, input._2) + // call driver + val res = driver(sys1.get(v).es, input._2) all { // update v's state after the step val sys = sys1.put(v, { ...sys1.get(v), es: res._1}) @@ -130,7 +131,7 @@ action valStep(v: Address_t) : bool = { else if (res._2.name == "skipRound") all { propBuffer' = propBuffer, voteBuffer' = voteBuffer, - //skipRound should never leave the executor + //skipRound should never leave the driver system' = sys, } else all { @@ -144,7 +145,7 @@ action valStep(v: Address_t) : bool = { } action setNextValueToPropose(v: Address_t, value: Value_t) : bool = all { - val res = executor(system.get(v).es, { ...defaultInput, name: "SetNextProposedValue", nextValueToPropose: value}) + val res = driver(system.get(v).es, { ...defaultInput, name: "SetNextProposedValue", nextValueToPropose: value}) val newNS = { ...system.get(v), es: res._1} system' = system.put(v, newNS), _hist' = _hist, @@ -152,7 +153,7 @@ action setNextValueToPropose(v: Address_t, value: Value_t) : bool = all { voteBuffer' = voteBuffer, } -action deliverProposal(v: Address_t, p: ProposeMsg_t) : bool = all { +action deliverProposal(v: Address_t, p: Proposal_t) : bool = all { propBuffer.get(v).union(AllFaultyProposals).contains(p), // the proposal must be sent or from a faulty node propBuffer' = propBuffer.put(v, propBuffer.get(v).exclude(Set(p))), system' = system.put(v, { ...system.get(v), incomingProposals: system.get(v).incomingProposals.union(Set(p)) }), @@ -160,7 +161,12 @@ action deliverProposal(v: Address_t, p: ProposeMsg_t) : bool = all { voteBuffer' = voteBuffer, } -action deliverVote(v: Address_t, vote: VoteMsg_t) : bool = all { +action deliverSomeProposal(v: Address_t) : bool = any { + nondet prop = oneOf(propBuffer.get(v)) + deliverProposal(v, prop) +} + +action deliverVote(v: Address_t, vote: Vote_t) : bool = all { voteBuffer.get(v).union(AllFaultyVotes).contains(vote), // the vote must be sent or from a faulty node voteBuffer' = voteBuffer.put(v, voteBuffer.get(v).exclude(Set(vote))), system' = system.put(v, { ...system.get(v), incomingVotes: system.get(v).incomingVotes.union(Set(vote)) }), diff --git a/Specs/Quint/statemachineTest.qnt b/Specs/Quint/statemachineTest.qnt index 1e2115ae8..c9f2f05cf 100644 --- a/Specs/Quint/statemachineTest.qnt +++ b/Specs/Quint/statemachineTest.qnt @@ -12,7 +12,7 @@ module statemachineTest { -import executor.* from "./executor" +import driver.* from "./driver" import consensus.* from "./consensus" import voteBookkeeper.* from "./voteBookkeeper" @@ -20,23 +20,23 @@ val validators = Set("v1", "v2", "v3", "v4") val validatorSet = validators.mapBy(x => 1) var system : Address_t -> NodeState -var _hist: (str, ExecutorInput, ConsensusOutput) +var _hist: (str, DriverInput, ConsensusOutput) //var _histSimple: (str, str, str) action init = all { system' = validators.mapBy(v => initNode(v, validatorSet)), - _hist' = ("INIT", defaultInput, defaultResult) + _hist' = ("INIT", defaultInput, defaultOutput) // _histSimple' = ("INIT", "", "") } // Put the proposal into the inbuffers of all validators -pure def deliverProposal (sys: Address_t -> NodeState, prop: ProposeMsg_t) : Address_t -> NodeState = { +pure def deliverProposal (sys: Address_t -> NodeState, prop: Proposal_t) : Address_t -> NodeState = { sys.keys().mapBy(x => { ...sys.get(x), incomingProposals: sys.get(x).incomingProposals.union(Set(prop)) }) } // Put the vote into the inbuffers of all validators -pure def deliverVote (sys: Address_t -> NodeState, vote: VoteMsg_t) : Address_t -> NodeState = { +pure def deliverVote (sys: Address_t -> NodeState, vote: Vote_t) : Address_t -> NodeState = { sys.keys().mapBy(x => { ...sys.get(x), incomingVotes: sys.get(x).incomingVotes.union(Set(vote)) }) } @@ -53,11 +53,11 @@ pure def startTimeout (sys: Address_t -> NodeState, v: Address_t, toName: str) : // hardly ever are fired action valStep(v: Address_t) : bool = { // pick action - val input = system.get(v).nextAction() // TODO: nextAction could go within executor boundary + val input = system.get(v).nextAction() // TODO: nextAction could go within driver boundary // remove action from v val sys1 = system.put(v, input._1) - // call executor - val res = executor(sys1.get(v).es, input._2) + // call driver + val res = driver(sys1.get(v).es, input._2) all { // update v's state after the step val sys = sys1.put(v, { ...sys1.get(v), es: res._1}) @@ -69,7 +69,7 @@ action valStep(v: Address_t) : bool = { else if (res._2.name == "timeout") system' = startTimeout(sys, v, res._2.timeout) else if (res._2.name == "skipRound") - //skipRound should never leave the executor + //skipRound should never leave the driver system' = sys else system' = sys, @@ -79,7 +79,7 @@ action valStep(v: Address_t) : bool = { } action setNextValueToPropose(v: Address_t, value: Value_t) : bool = all { - val res = executor(system.get(v).es, { ...defaultInput, name: "SetNextProposedValue", nextValueToPropose: value}) + val res = driver(system.get(v).es, { ...defaultInput, name: "SetNextProposedValue", nextValueToPropose: value}) val newNS = { ...system.get(v), es: res._1} system' = system.put(v, newNS), _hist' = _hist @@ -101,8 +101,8 @@ action valStepCommand(v: Address_t, command: str) : bool = { val input = system.get(v).nextActionCommand(command) // remove action from v val sys1 = system.put(v, input._1) - // call executor - val res = executor(sys1.get(v).es, input._2) + // call driver + val res = driver(sys1.get(v).es, input._2) all { // update v's state after the step val sys = sys1.put(v, { ...sys1.get(v), es: res._1}) @@ -114,7 +114,7 @@ action valStepCommand(v: Address_t, command: str) : bool = { else if (res._2.name == "timeout") system' = startTimeout(sys, v, res._2.timeout) else if (res._2.name == "skipRound") - //skipRound should never leave the executor + //skipRound should never leave the driver system' = sys else system' = sys, @@ -137,6 +137,7 @@ run DecidingRunTest = { .then(valStepCommand("v1", "vote")) .then(valStepCommand("v1", "vote")) .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "pending")) .then(all{ assert(system.get("v1").incomingVotes.contains( { src: "v1", height: 0, round: 0, step: "Precommit", id: "a block" } @@ -146,6 +147,7 @@ run DecidingRunTest = { .then(valStepCommand("v2", "vote")) .then(valStepCommand("v2", "vote")) .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v2", "pending")) .then(all{ assert(system.get("v2").incomingVotes.contains( { src: "v2", height: 0, round: 0, step: "Precommit", id: "a block" } @@ -156,6 +158,7 @@ run DecidingRunTest = { .then(valStepCommand("v3", "vote")) .then(valStepCommand("v3", "vote")) .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v3", "pending")) .then(all{ assert(system.get("v3").incomingVotes.contains( { src: "v3", height: 0, round: 0, step: "Precommit", id: "a block" } diff --git a/Specs/Quint/voteBookkeeper.qnt b/Specs/Quint/voteBookkeeper.qnt index 3e9bca343..1e1c1676f 100644 --- a/Specs/Quint/voteBookkeeper.qnt +++ b/Specs/Quint/voteBookkeeper.qnt @@ -51,7 +51,7 @@ module voteBookkeeper { round: Round, prevotes: VoteCount, precommits: VoteCount, - emittedEvents: Set[ExecutorEvent], + emittedOutputs: Set[VoteKeeperOutput], votesAddressesWeights: Address -> Weight } @@ -66,18 +66,18 @@ module voteBookkeeper { pure def valueThreshold(value) = { name: "Value", value: value } pure def isThresholdOnValue(t: Threshold): bool = t.name == "Value" - type ExecutorEvent = { + type VoteKeeperOutput = { round: Round, name: str, value: Value } - pure def noEvent(round) = { round: round, name: "None", value: "null" } - pure def polkaValueEvent(round, value) = { round: round, name: "PolkaValue", value: value } - pure def polkaNilEvent(round) = { round: round, name: "PolkaNil", value: "null" } - pure def polkaAnyEvent(round) = { round: round, name: "PolkaAny", value: "null" } - pure def precommitValueEvent(round, value) = { round: round, name: "PrecommitValue", value: value } - pure def precommitAnyEvent(round) = { round: round, name: "PrecommitAny", value: "null" } - pure def skipEvent(round) = { round: round, name: "Skip", value: "null" } + pure def noOutput(round) = { round: round, name: "None", value: "null" } + pure def polkaValueOutput(round, value) = { round: round, name: "PolkaValue", value: value } + pure def polkaNilOutput(round) = { round: round, name: "PolkaNil", value: "null" } + pure def polkaAnyOutput(round) = { round: round, name: "PolkaAny", value: "null" } + pure def precommitValueOutput(round, value) = { round: round, name: "PrecommitValue", value: value } + pure def precommitAnyOutput(round) = { round: round, name: "PrecommitAny", value: "null" } + pure def skipOutput(round) = { round: round, name: "Skip", value: "null" } type Bookkeeper = { height: Height, @@ -96,7 +96,7 @@ module voteBookkeeper { round: round, prevotes: newVoteCount(totalWeight), precommits: newVoteCount(totalWeight), - emittedEvents: Set(), + emittedOutputs: Set(), votesAddressesWeights: Map() } @@ -188,64 +188,64 @@ module voteBookkeeper { } else unreachedThreshold - // Given a round, voteType and threshold, return the corresponding ExecutorEvent - pure def toEvent(round: Round, voteType: VoteType, threshold: Threshold): ExecutorEvent = + // Given a round, voteType and threshold, return the corresponding VoteKeeperOutput + pure def toVoteKeeperOutput(round: Round, voteType: VoteType, threshold: Threshold): VoteKeeperOutput = if (threshold == unreachedThreshold) - noEvent(round) + noOutput(round) // prevote else if (voteType.isPrevote() and threshold.isThresholdOnValue()) - polkaValueEvent(round, threshold.value) + polkaValueOutput(round, threshold.value) else if (voteType.isPrevote() and threshold == nilThreshold) - polkaNilEvent(round) + polkaNilOutput(round) else if (voteType.isPrevote() and threshold == anyThreshold) - polkaAnyEvent(round) + polkaAnyOutput(round) // precommit else if (voteType.isPrecommit() and threshold.isThresholdOnValue()) - precommitValueEvent(round, threshold.value) + precommitValueOutput(round, threshold.value) else if (voteType.isPrecommit() and threshold.in(Set(anyThreshold, nilThreshold))) - precommitAnyEvent(round) + precommitAnyOutput(round) else if (threshold == skipThreshold) - skipEvent(round) + skipOutput(round) else - noEvent(round) + noOutput(round) - run toEventTest = + run toVoteKeeperOutputTest = val round = 10 all { - assert(toEvent(round, "Prevote", unreachedThreshold) == noEvent(round)), - assert(toEvent(round, "Precommit", unreachedThreshold) == noEvent(round)), + assert(toVoteKeeperOutput(round, "Prevote", unreachedThreshold) == noOutput(round)), + assert(toVoteKeeperOutput(round, "Precommit", unreachedThreshold) == noOutput(round)), - assert(toEvent(round, "Prevote", anyThreshold) == polkaAnyEvent(round)), - assert(toEvent(round, "Prevote", nilThreshold) == polkaNilEvent(round)), - assert(toEvent(round, "Prevote", valueThreshold("val1")) == polkaValueEvent(round, "val1")), + assert(toVoteKeeperOutput(round, "Prevote", anyThreshold) == polkaAnyOutput(round)), + assert(toVoteKeeperOutput(round, "Prevote", nilThreshold) == polkaNilOutput(round)), + assert(toVoteKeeperOutput(round, "Prevote", valueThreshold("val1")) == polkaValueOutput(round, "val1")), - assert(toEvent(round, "Precommit", anyThreshold) == precommitAnyEvent(round)), - assert(toEvent(round, "Precommit", nilThreshold) == precommitAnyEvent(round)), - assert(toEvent(round, "Precommit", valueThreshold("val1")) == precommitValueEvent(round, "val1")), + assert(toVoteKeeperOutput(round, "Precommit", anyThreshold) == precommitAnyOutput(round)), + assert(toVoteKeeperOutput(round, "Precommit", nilThreshold) == precommitAnyOutput(round)), + assert(toVoteKeeperOutput(round, "Precommit", valueThreshold("val1")) == precommitValueOutput(round, "val1")), - assert(toEvent(round, "Prevote", skipThreshold) == skipEvent(round)), - assert(toEvent(round, "Precommit", skipThreshold) == skipEvent(round)), + assert(toVoteKeeperOutput(round, "Prevote", skipThreshold) == skipOutput(round)), + assert(toVoteKeeperOutput(round, "Precommit", skipThreshold) == skipOutput(round)), - assert(toEvent(round, "Precommit", { name: "Error", value: "null" }) == noEvent(round)), - assert(toEvent(round, "Error", anyThreshold) == noEvent(round)), + assert(toVoteKeeperOutput(round, "Precommit", { name: "Error", value: "null" }) == noOutput(round)), + assert(toVoteKeeperOutput(round, "Error", anyThreshold) == noOutput(round)), } - // Executor interface - type BKResult = { bookkeeper: Bookkeeper, event: ExecutorEvent } + // Driver interface + type BKOutput = { bookkeeper: Bookkeeper, output: VoteKeeperOutput } - // Called by the executor when it receives a vote. The function takes the following steps: + // Called by the driver when it receives a vote. The function takes the following steps: // - It first adds the vote and then computes a threshold. - // - If there exist a threshold and has not emitted before, the function returns the corresponding ExecutorEvent. - // - Otherwise, the function returns a no-threshold event. + // - If there exist a threshold and has not emitted before, the function returns the corresponding VoteKeeperOutput. + // - Otherwise, the function returns a no-threshold output. // - Note that if there is no threshold after adding the vote, the function checks if there is a skip threshold. // TO DISCUSS: // - There might be a problem if we generalize from single-shot to multi-shot: the keeper only keeps the totalWeight // of the current height; I wonder if we need to keep the totalWeight for every Height that we may receive a vote for. - pure def applyVote(keeper: Bookkeeper, vote: Vote, weight: Weight, currentRound: Round): { bookkeeper: Bookkeeper, event: ExecutorEvent } = + pure def applyVote(keeper: Bookkeeper, vote: Vote, weight: Weight, currentRound: Round): { bookkeeper: Bookkeeper, output: VoteKeeperOutput } = val round = vote.round val roundVotes = keeper.rounds.getOrElse(round, newRoundVotes(keeper.height, round, keeper.totalWeight)) @@ -264,16 +264,16 @@ module voteBookkeeper { // Combined weight of all validators at this height val combinedWeight = updatedVotesAddressesWeights.mapSumValues() - val finalEvent = + val finalOutput = if (vote.round > currentRound and isSkip(combinedWeight, keeper.totalWeight)) - skipEvent(vote.round) + skipOutput(vote.round) else val threshold = computeThreshold(updatedVoteCount, vote.value) - val event = toEvent(vote.round, vote.typ, threshold) - if (not(event.in(roundVotes.emittedEvents))) - event + val output = toVoteKeeperOutput(vote.round, vote.typ, threshold) + if (not(output.in(roundVotes.emittedOutputs))) + output else - noEvent(vote.round) + noOutput(vote.round) val updatedRoundVotes = if (vote.typ.isPrevote()) @@ -282,12 +282,12 @@ module voteBookkeeper { roundVotes.with("precommits", updatedVoteCount) val updatedRoundVotes2 = updatedRoundVotes .with("votesAddressesWeights", updatedVotesAddressesWeights) - .with("emittedEvents", roundVotes.emittedEvents.setAddIf(finalEvent, finalEvent.name != "None")) + .with("emittedOutputs", roundVotes.emittedOutputs.setAddIf(finalOutput, finalOutput.name != "None")) val updatedBookkeeper = keeper .with("rounds", keeper.rounds.mapSafeSet(vote.round, updatedRoundVotes2)) - { bookkeeper: updatedBookkeeper, event: finalEvent } + { bookkeeper: updatedBookkeeper, output: finalOutput } run applyVoteTest = val roundVotes: RoundVotes = { @@ -295,7 +295,7 @@ module voteBookkeeper { round: 0, prevotes: { totalWeight: 4, votesAddresses: Set(), valuesWeights: Map("v1" -> 1, Nil -> 3) }, precommits: { totalWeight: 4, votesAddresses: Set(), valuesWeights: Map() }, - emittedEvents: Set(), + emittedOutputs: Set(), votesAddressesWeights: Map(), } val vk: Bookkeeper = { height: 0, totalWeight: 4, rounds: Map(0 -> roundVotes) } @@ -305,16 +305,16 @@ module voteBookkeeper { val o4 = applyVote(o3.bookkeeper, { height: 0, round: 0, address: "a3", typ: "Precommit", value: Nil }, 1, 0) val o5 = applyVote(o4.bookkeeper, { height: 0, round: 1, address: "a4", typ: "Precommit", value: Nil }, 3, 0) all { - assert(o1.event.name == "None"), - assert(o2.event.name == "None"), - assert(o3.event.name == "PrecommitAny"), - assert(o4.event.name == "None"), - assert(o5.event.name == "Skip"), + assert(o1.output.name == "None"), + assert(o2.output.name == "None"), + assert(o3.output.name == "PrecommitAny"), + assert(o4.output.name == "None"), + assert(o5.output.name == "Skip"), } - // Called by the executor to check if there is a specific threshold for a given round and voteType. + // Called by the driver to check if there is a specific threshold for a given round and voteType. // TO DISCUSS: - // - The function does not consider Skip threshold. This because if the executor receives a Skip event + // - The function does not consider Skip threshold. This because if the driver receives a Skip output // and do not act on it, this means that it will never do it in the future. We should discuss that this // is the case. pure def checkThreshold(keeper: Bookkeeper, round: Round, voteType: VoteType, threshold: Threshold): bool = @@ -380,8 +380,8 @@ module voteBookkeeper { var weightedVote: WeightedVote // The state of the Bookkeeper. var bookkeeper: Bookkeeper - // The event resulting from applying a weighted vote to the bookkeeper. - var lastEmitted: ExecutorEvent + // The output outputing from applying a weighted vote to the bookkeeper. + var lastEmitted: VoteKeeperOutput // ************************************************************************ // Actions @@ -399,13 +399,13 @@ module voteBookkeeper { lastEmitted' = { round: -1, name: "", value: "null" } } - // The vote keeper receives a weighted vote and produces an event. + // The vote keeper receives a weighted vote and produces an output. action applyVoteAction(vote: Vote, weight: Weight, currentRound: Round): bool = - val result = applyVote(bookkeeper, vote, weight, currentRound) + val output = applyVote(bookkeeper, vote, weight, currentRound) all { weightedVote' = (vote, weight, currentRound), - bookkeeper' = result.bookkeeper, - lastEmitted' = result.event + bookkeeper' = output.bookkeeper, + lastEmitted' = output.output } } diff --git a/Specs/Quint/voteBookkeeperTest.qnt b/Specs/Quint/voteBookkeeperTest.qnt index 44419ca27..95c369e70 100644 --- a/Specs/Quint/voteBookkeeperTest.qnt +++ b/Specs/Quint/voteBookkeeperTest.qnt @@ -22,71 +22,71 @@ module voteBookkeeperTest { run synchronousConsensusTest = initWith(1, 100) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 60, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == polkaValueEvent(1, "val1"))) + .then(_assert(lastEmitted == polkaValueOutput(1, "val1"))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "bob"}, 30, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Precommit", height: 1, round: 1, value: "val1", address: "bob"}, 30, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Precommit", height: 1, round: 1, value: "val1", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Precommit", height: 1, round: 1, value: "val1", address: "alice"}, 60, 1)) - .then(_assert(lastEmitted == precommitValueEvent(1, "val1"))) + .then(_assert(lastEmitted == precommitValueOutput(1, "val1"))) // Reaching PolkaAny run polkaAnyTest = initWith(1, 100) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 60, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "nil", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == polkaAnyEvent(1))) + .then(_assert(lastEmitted == polkaAnyOutput(1))) // Reaching PolkaNil run polkaNilTest = initWith(1, 100) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "nil", address: "alice"}, 60, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "nil", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == polkaNilEvent(1))) + .then(_assert(lastEmitted == polkaNilOutput(1))) // Reaching Skip via n+1 threshold with prevotes from two validators at a future round run skipSmallQuorumAllPrevotesTest = initWith(1, 100) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 60, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == noEvent(2))) + .then(_assert(lastEmitted == noOutput(2))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "bob"}, 30, 1)) - .then(_assert(lastEmitted == skipEvent(2))) + .then(_assert(lastEmitted == skipOutput(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({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 10, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 20, 1)) - .then(_assert(lastEmitted == noEvent(2))) + .then(_assert(lastEmitted == noOutput(2))) .then(applyVoteAction({typ: "Precommit", height: 1, round: 2, value: "val1", address: "john"}, 20, 1)) - .then(_assert(lastEmitted != skipEvent(2))) + .then(_assert(lastEmitted != skipOutput(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({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 50, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == noEvent(2))) + .then(_assert(lastEmitted == noOutput(2))) .then(applyVoteAction({typ: "Precommit", height: 1, round: 2, value: "val1", address: "bob"}, 20, 1)) - .then(_assert(lastEmitted == skipEvent(2))) + .then(_assert(lastEmitted == skipOutput(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({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 10, 1)) - .then(all { assert(lastEmitted == noEvent(1)), allUnchanged }) + .then(all { assert(lastEmitted == noOutput(1)), allUnchanged }) .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 60, 1)) - .then(all { assert(lastEmitted == skipEvent(2)), allUnchanged }) + .then(all { assert(lastEmitted == skipOutput(2)), allUnchanged }) // Reaching Skip via 2f+1 threshold with a single precommit from a single validator at a future round run skipQuorumSinglePrecommitTest = @@ -94,27 +94,27 @@ module voteBookkeeperTest { .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 10, 1)) .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) .then(applyVoteAction({typ: "Precommit", height: 1, round: 2, value: "val1", address: "john"}, 60, 1)) - .then(_assert(lastEmitted == skipEvent(2))) + .then(_assert(lastEmitted == skipOutput(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({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 10, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 30, 1)) - .then(_assert(lastEmitted == noEvent(2))) + .then(_assert(lastEmitted == noOutput(2))) .then(applyVoteAction({typ: "Precommit", height: 1, round: 2, value: "val1", address: "john"}, 30, 1)) - .then(_assert(lastEmitted != skipEvent(2))) + .then(_assert(lastEmitted != skipOutput(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({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 20, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == noEvent(2))) + .then(_assert(lastEmitted == noOutput(2))) .then(applyVoteAction({typ: "Precommit", height: 1, round: 2, value: "val1", address: "bob"}, 50, 1)) - .then(_assert(lastEmitted == skipEvent(2))) + .then(_assert(lastEmitted == skipOutput(2))) // **************************************************************************** // Properties that define an expected final state (for generating traces) diff --git a/codecov.yml b/codecov.yml index 4a394a747..d15ffde23 100644 --- a/codecov.yml +++ b/codecov.yml @@ -1,6 +1,10 @@ codecov: require_ci_to_pass: yes +# ignore: +# - "Code/itf" +# - "Code/test" + coverage: precision: 2 round: nearest