diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index b64ce2dbe..c141726f3 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -23,6 +23,7 @@ jobs: - 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 diff --git a/.github/workflows/quint.yml b/.github/workflows/quint.yml index 03ebab6db..186268d6f 100644 --- a/.github/workflows/quint.yml +++ b/.github/workflows/quint.yml @@ -15,15 +15,22 @@ jobs: quint-typecheck: name: Typecheck runs-on: ubuntu-latest - defaults: - run: - working-directory: ./Specs/Quint steps: - uses: actions/checkout@v4 - uses: actions/setup-node@v3 with: node-version: "18" - run: npm install -g @informalsystems/quint - - run: npx @informalsystems/quint typecheck consensus.qnt - - run: npx @informalsystems/quint typecheck voteBookkeeper.qnt + - run: bash Scripts/quint-forall.sh typecheck Specs/Quint/*.qnt + + quint-test: + name: Test + runs-on: ubuntu-latest + 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 diff --git a/Code/Cargo.toml b/Code/Cargo.toml index fe4a15bb6..3202f6c70 100644 --- a/Code/Cargo.toml +++ b/Code/Cargo.toml @@ -4,10 +4,11 @@ resolver = "2" members = [ "common", "driver", + "itf", "round", - "vote", "tendermint", "test", + "vote", ] [workspace.package] @@ -18,9 +19,12 @@ license = "Apache-2.0" publish = false [workspace.dependencies] +async-trait = "0.1" +futures = "0.3" ed25519-consensus = "2.1.0" +itf = "0.1.2" rand = { version = "0.8.5", features = ["std_rng"] } -secrecy = "0.8.0" +serde = "1.0" sha2 = "0.10.8" signature = "2.1.0" tendermint = { version = "0.34.0", default-features = false, features = ["rust-crypto"] } diff --git a/Code/common/Cargo.toml b/Code/common/Cargo.toml index cd02c85dc..b39479cba 100644 --- a/Code/common/Cargo.toml +++ b/Code/common/Cargo.toml @@ -9,5 +9,4 @@ license.workspace = true publish.workspace = true [dependencies] -secrecy.workspace = true signature.workspace = true diff --git a/Code/common/src/context.rs b/Code/common/src/context.rs index 3ae930665..013d9e981 100644 --- a/Code/common/src/context.rs +++ b/Code/common/src/context.rs @@ -1,6 +1,6 @@ use crate::{ - Address, Height, PrivateKey, Proposal, PublicKey, Round, Signature, SignedVote, SigningScheme, - Validator, ValidatorSet, Value, ValueId, Vote, + Address, Height, Proposal, PublicKey, Round, SignedVote, SigningScheme, Validator, + ValidatorSet, Value, ValueId, Vote, }; /// This trait allows to abstract over the various datatypes @@ -18,9 +18,8 @@ where type Vote: Vote; type SigningScheme: SigningScheme; // TODO: Do we need to support multiple signing schemes? - /// Sign the given vote using the given private key. - /// TODO: Maybe move this as concrete methods in `SignedVote`? - fn sign_vote(&self, vote: &Self::Vote, private_key: &PrivateKey) -> Signature; + /// Sign the given vote with our private key. + fn sign_vote(&self, vote: Self::Vote) -> SignedVote; /// Verify the given vote's signature using the given public key. /// TODO: Maybe move this as concrete methods in `SignedVote`? @@ -41,6 +40,7 @@ where /// Build a new prevote vote by the validator with the given address, /// for the value identified by the given value id, at the given round. fn new_prevote( + height: Self::Height, round: Round, value_id: Option>, address: Self::Address, @@ -49,6 +49,7 @@ where /// Build a new precommit vote by the validator with the given address, /// for the value identified by the given value id, at the given round. fn new_precommit( + height: Self::Height, round: Round, value_id: Option>, address: Self::Address, diff --git a/Code/common/src/height.rs b/Code/common/src/height.rs index 511f69503..973ee3b61 100644 --- a/Code/common/src/height.rs +++ b/Code/common/src/height.rs @@ -9,6 +9,6 @@ use core::fmt::Debug; pub trait Height where // TODO: Require Copy as well? - Self: Clone + Debug + PartialEq + Eq + PartialOrd + Ord, + Self: Default + Clone + Debug + PartialEq + Eq + PartialOrd + Ord, { } diff --git a/Code/common/src/lib.rs b/Code/common/src/lib.rs index b9a6306af..bc0a00429 100644 --- a/Code/common/src/lib.rs +++ b/Code/common/src/lib.rs @@ -10,6 +10,7 @@ variant_size_differences )] #![cfg_attr(not(test), deny(clippy::unwrap_used, clippy::panic))] +#![cfg_attr(coverage_nightly, feature(coverage_attribute))] mod context; mod height; diff --git a/Code/common/src/signed_vote.rs b/Code/common/src/signed_vote.rs index 0eb38a429..33b663e72 100644 --- a/Code/common/src/signed_vote.rs +++ b/Code/common/src/signed_vote.rs @@ -1,8 +1,9 @@ +use core::fmt; + use crate::{Context, Signature, Vote}; // TODO: Do we need to abstract over `SignedVote` as well? -#[derive(Clone, Debug, PartialEq, Eq)] pub struct SignedVote where Ctx: Context, @@ -23,3 +24,36 @@ where self.vote.validator_address() } } + +// 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 SignedVote { + #[cfg_attr(coverage_nightly, coverage(off))] + fn clone(&self) -> Self { + Self { + vote: self.vote.clone(), + signature: self.signature.clone(), + } + } +} + +impl fmt::Debug for SignedVote { + #[cfg_attr(coverage_nightly, coverage(off))] + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.debug_struct("SignedVote") + .field("vote", &self.vote) + .field("signature", &self.signature) + .finish() + } +} + +impl PartialEq for SignedVote { + #[cfg_attr(coverage_nightly, coverage(off))] + fn eq(&self, other: &Self) -> bool { + self.vote == other.vote && self.signature == other.signature + } +} + +impl Eq for SignedVote {} diff --git a/Code/common/src/signing.rs b/Code/common/src/signing.rs index 07abc4ae5..8f52aef67 100644 --- a/Code/common/src/signing.rs +++ b/Code/common/src/signing.rs @@ -1,6 +1,5 @@ use core::fmt::Debug; -use secrecy::{CloneableSecret, DebugSecret, Zeroize}; use signature::{Keypair, Signer, Verifier}; pub trait SigningScheme @@ -11,10 +10,5 @@ where type PublicKey: Clone + Debug + Eq + Verifier; - type PrivateKey: Clone - + Signer - + Keypair - + Zeroize - + DebugSecret - + CloneableSecret; + type PrivateKey: Clone + Signer + Keypair; } diff --git a/Code/common/src/validator_set.rs b/Code/common/src/validator_set.rs index b75cbc1f7..4ba5a1bcf 100644 --- a/Code/common/src/validator_set.rs +++ b/Code/common/src/validator_set.rs @@ -1,4 +1,4 @@ -use core::fmt::Debug; +use core::fmt::{Debug, Display}; use crate::{Context, PublicKey}; @@ -12,7 +12,7 @@ pub type VotingPower = u64; /// TODO: Keep this trait or just add the bounds to Consensus::Address? pub trait Address where - Self: Clone + Debug + Eq + Ord, + Self: Clone + Debug + Display + Eq + Ord, { } diff --git a/Code/common/src/vote.rs b/Code/common/src/vote.rs index abd8d232f..885faaff8 100644 --- a/Code/common/src/vote.rs +++ b/Code/common/src/vote.rs @@ -21,6 +21,9 @@ where Self: Clone + Debug + Eq, Ctx: Context, { + /// The height for which the vote is for. + fn height(&self) -> Ctx::Height; + /// The round for which the vote is for. fn round(&self) -> Round; diff --git a/Code/driver/Cargo.toml b/Code/driver/Cargo.toml index bf2b34458..0b5c4ab5b 100644 --- a/Code/driver/Cargo.toml +++ b/Code/driver/Cargo.toml @@ -13,4 +13,4 @@ malachite-common = { version = "0.1.0", path = "../common" } malachite-round = { version = "0.1.0", path = "../round" } malachite-vote = { version = "0.1.0", path = "../vote" } -secrecy.workspace = true +async-trait.workspace = true diff --git a/Code/driver/src/client.rs b/Code/driver/src/client.rs deleted file mode 100644 index 1e240d730..000000000 --- a/Code/driver/src/client.rs +++ /dev/null @@ -1,14 +0,0 @@ -use malachite_common::Context; - -/// Client for use by the [`Driver`](crate::Driver) to ask -/// for a value to propose and validate proposals. -pub trait Client -where - Ctx: Context, -{ - /// Get the value to propose. - fn get_value(&self) -> Ctx::Value; - - /// Validate a proposal. - fn validate_proposal(&self, proposal: &Ctx::Proposal) -> bool; -} diff --git a/Code/driver/src/driver.rs b/Code/driver/src/driver.rs index eadbcc7bd..d941caacf 100644 --- a/Code/driver/src/driver.rs +++ b/Code/driver/src/driver.rs @@ -1,11 +1,8 @@ -use std::collections::BTreeMap; - use malachite_round::state_machine::RoundData; -use secrecy::{ExposeSecret, Secret}; use malachite_common::{ - Context, PrivateKey, Proposal, Round, SignedVote, Timeout, TimeoutStep, Validator, - ValidatorSet, Value, Vote, VoteType, + 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; @@ -14,154 +11,177 @@ use malachite_vote::keeper::Message as VoteMessage; use malachite_vote::keeper::VoteKeeper; use malachite_vote::Threshold; +use crate::env::Env as DriverEnv; use crate::event::Event; use crate::message::Message; +use crate::Error; +use crate::ProposerSelector; +use crate::Validity; -/// Driver for the state machine of the Malachite consensus engine. +/// Driver for the state machine of the Malachite consensus engine at a given height. #[derive(Clone, Debug)] -pub struct Driver +pub struct Driver where Ctx: Context, - Client: crate::client::Client, + Env: DriverEnv, + PSel: ProposerSelector, { pub ctx: Ctx, - pub client: Client, - pub height: Ctx::Height, - pub private_key: Secret>, + pub env: Env, + pub proposer_selector: PSel, + pub address: Ctx::Address, pub validator_set: Ctx::ValidatorSet, - pub round: Round, + pub votes: VoteKeeper, - pub round_states: BTreeMap>, + pub round_state: RoundState, } -impl Driver +impl Driver where Ctx: Context, - Client: crate::client::Client, + Env: DriverEnv, + PSel: ProposerSelector, { pub fn new( ctx: Ctx, - client: Client, - height: Ctx::Height, + env: Env, + proposer_selector: PSel, validator_set: Ctx::ValidatorSet, - private_key: PrivateKey, address: Ctx::Address, ) -> Self { let votes = VoteKeeper::new(validator_set.total_voting_power()); Self { ctx, - client, - height, - private_key: Secret::new(private_key), + env, + proposer_selector, address, validator_set, - round: Round::NIL, votes, - round_states: BTreeMap::new(), + round_state: RoundState::default(), } } - fn get_value(&self) -> Ctx::Value { - self.client.get_value() + async fn get_value(&self) -> Option { + self.env + .get_value(self.round_state.height.clone(), self.round_state.round) + .await } - fn validate_proposal(&self, proposal: &Ctx::Proposal) -> bool { - self.client.validate_proposal(proposal) - } - - pub fn execute(&mut self, msg: Event) -> Option> { - let round_msg = match self.apply(msg) { + pub async fn execute(&mut self, msg: Event) -> Result>, Error> { + let round_msg = match self.apply(msg).await? { Some(msg) => msg, - None => return None, + None => return Ok(None), }; - match round_msg { + let msg = match round_msg { RoundMessage::NewRound(round) => { - // XXX: Check if there is an existing state? - assert!(self.round < round); - Some(Message::NewRound(round)) + Message::NewRound(self.round_state.height.clone(), round) } RoundMessage::Proposal(proposal) => { // sign the proposal - Some(Message::Propose(proposal)) + Message::Propose(proposal) } RoundMessage::Vote(vote) => { - let signature = self.ctx.sign_vote(&vote, self.private_key.expose_secret()); - let signed_vote = SignedVote::new(vote, signature); - - Some(Message::Vote(signed_vote)) + let signed_vote = self.ctx.sign_vote(vote); + Message::Vote(signed_vote) } - RoundMessage::ScheduleTimeout(timeout) => Some(Message::ScheduleTimeout(timeout)), + RoundMessage::ScheduleTimeout(timeout) => Message::ScheduleTimeout(timeout), RoundMessage::Decision(value) => { // TODO: update the state - Some(Message::Decide(value.round, value.value)) + Message::Decide(value.round, value.value) } - } + }; + + Ok(Some(msg)) } - fn apply(&mut self, msg: Event) -> Option> { - match msg { - Event::NewRound(round, is_proposer) => self.apply_new_round(round, is_proposer), - Event::Proposal(proposal) => self.apply_proposal(proposal), + async fn apply(&mut self, event: Event) -> Result>, Error> { + match event { + Event::NewRound(height, round) => self.apply_new_round(height, round).await, + + Event::Proposal(proposal, validity) => { + Ok(self.apply_proposal(proposal, validity).await) + } + Event::Vote(signed_vote) => self.apply_vote(signed_vote), - Event::TimeoutElapsed(timeout) => self.apply_timeout(timeout), + + Event::TimeoutElapsed(timeout) => Ok(self.apply_timeout(timeout)), } } - fn apply_new_round(&mut self, round: Round, is_proposer: bool) -> Option> { - let event = if is_proposer { - let value = self.get_value(); + async fn apply_new_round( + &mut self, + height: Ctx::Height, + round: Round, + ) -> Result>, Error> { + self.round_state = RoundState::new(height, round); + + let proposer_address = self + .proposer_selector + .select_proposer(round, &self.validator_set); + + let proposer = self + .validator_set + .get_by_address(&proposer_address) + .ok_or_else(|| Error::ProposerNotFound(proposer_address.clone()))?; + + let event = if proposer.address() == self.address { + // We are the proposer + // TODO: Schedule propose timeout + + let Some(value) = self.get_value().await else { + return Err(Error::NoValueToPropose); + }; + RoundEvent::NewRoundProposer(value) } else { RoundEvent::NewRound }; - assert!(self.round < round); - self.round_states - .insert(round, RoundState::default().new_round(round)); - self.round = round; - - self.apply_event(round, event) + Ok(self.apply_event(round, event)) } - fn apply_proposal(&mut self, proposal: Ctx::Proposal) -> Option> { + async fn apply_proposal( + &mut self, + proposal: Ctx::Proposal, + validity: Validity, + ) -> Option> { // Check that there is an ongoing round - let Some(round_state) = self.round_states.get(&self.round) else { - // TODO: Add logging + if self.round_state.round == Round::NIL { return None; - }; + } // Only process the proposal if there is no other proposal - if round_state.proposal.is_some() { + if self.round_state.proposal.is_some() { return None; } // Check that the proposal is for the current height and round - if self.height != proposal.height() || self.round != proposal.round() { + if self.round_state.height != proposal.height() + || self.round_state.round != proposal.round() + { return None; } // TODO: Document - if proposal.pol_round().is_defined() && proposal.pol_round() >= round_state.round { + if proposal.pol_round().is_defined() && proposal.pol_round() >= self.round_state.round { return None; } // TODO: Verify proposal signature (make some of these checks part of message validation) - let is_valid = self.validate_proposal(&proposal); - match proposal.pol_round() { Round::Nil => { // Is it possible to get +2/3 prevotes before the proposal? // Do we wait for our own prevote to check the threshold? let round = proposal.round(); - let event = if is_valid { + let event = if validity.is_valid() { RoundEvent::Proposal(proposal) } else { RoundEvent::ProposalInvalid @@ -177,7 +197,7 @@ where ) => { let round = proposal.round(); - let event = if is_valid { + let event = if validity.is_valid() { RoundEvent::Proposal(proposal) } else { RoundEvent::ProposalInvalid @@ -189,25 +209,33 @@ where } } - fn apply_vote(&mut self, signed_vote: SignedVote) -> Option> { - // TODO: How to handle missing validator? + fn apply_vote( + &mut self, + signed_vote: SignedVote, + ) -> Result>, Error> { let validator = self .validator_set - .get_by_address(&signed_vote.validator_address())?; + .get_by_address(&signed_vote.validator_address()) + .ok_or_else(|| Error::ValidatorNotFound(signed_vote.validator_address().clone()))?; if !self .ctx .verify_signed_vote(&signed_vote, &validator.public_key()) { - // TODO: How to handle invalid votes? - return None; + return Err(Error::InvalidVoteSignature( + signed_vote.clone(), + validator.clone(), + )); } let round = signed_vote.vote.round(); - let vote_msg = self + let Some(vote_msg) = self .votes - .apply_vote(signed_vote.vote, validator.voting_power())?; + .apply_vote(signed_vote.vote, validator.voting_power()) + else { + return Ok(None); + }; let round_event = match vote_msg { VoteMessage::PolkaAny => RoundEvent::PolkaAny, @@ -218,7 +246,7 @@ where VoteMessage::SkipRound(r) => RoundEvent::SkipRound(r), }; - self.apply_event(round, round_event) + Ok(self.apply_event(round, round_event)) } fn apply_timeout(&mut self, timeout: Timeout) -> Option> { @@ -233,10 +261,9 @@ where /// Apply the event, update the state. fn apply_event(&mut self, round: Round, event: RoundEvent) -> Option> { - // Get the round state, or create a new one - let round_state = self.round_states.remove(&round).unwrap_or_default(); + let round_state = core::mem::take(&mut self.round_state); - let data = RoundData::new(round, &self.height, &self.address); + let data = RoundData::new(round, round_state.height.clone(), &self.address); // Multiplex the event with the round state. let mux_event = match event { @@ -260,13 +287,9 @@ where let transition = round_state.apply_event(&data, mux_event); // Update state - self.round_states.insert(round, transition.next_state); + self.round_state = transition.next_state; // Return message, if any transition.message } - - pub fn round_state(&self, round: Round) -> Option<&RoundState> { - self.round_states.get(&round) - } } diff --git a/Code/driver/src/env.rs b/Code/driver/src/env.rs new file mode 100644 index 000000000..2915da387 --- /dev/null +++ b/Code/driver/src/env.rs @@ -0,0 +1,19 @@ +use alloc::boxed::Box; + +use async_trait::async_trait; + +use malachite_common::{Context, Round}; + +/// Environment for use by the [`Driver`](crate::Driver) to ask +/// for a value to propose and validate proposals. +#[async_trait] +pub trait Env +where + Ctx: Context, +{ + /// Get the value to propose for the given height and round. + /// + /// If `None` is returned, the driver will understand this + /// as an error and will not propose a value. + async fn get_value(&self, height: Ctx::Height, round: Round) -> Option; +} diff --git a/Code/driver/src/error.rs b/Code/driver/src/error.rs new file mode 100644 index 000000000..85c2e77aa --- /dev/null +++ b/Code/driver/src/error.rs @@ -0,0 +1,59 @@ +use core::fmt; + +use malachite_common::{Context, SignedVote, Validator}; + +#[derive(Clone, Debug)] +pub enum Error +where + Ctx: Context, +{ + /// No value to propose + NoValueToPropose, + + /// Proposer not found + ProposerNotFound(Ctx::Address), + + /// Validator not found in validator set + ValidatorNotFound(Ctx::Address), + + /// Invalid vote signature + InvalidVoteSignature(SignedVote, Ctx::Validator), +} + +impl fmt::Display for Error +where + Ctx: Context, +{ + #[cfg_attr(coverage_nightly, coverage(off))] + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Error::NoValueToPropose => write!(f, "No value to propose"), + Error::ProposerNotFound(addr) => write!(f, "Proposer not found: {addr}"), + Error::ValidatorNotFound(addr) => write!(f, "Validator not found: {addr}"), + Error::InvalidVoteSignature(vote, validator) => write!( + f, + "Invalid vote signature by {} on vote {vote:?}", + validator.address() + ), + } + } +} + +impl PartialEq for Error +where + Ctx: Context, +{ + #[cfg_attr(coverage_nightly, coverage(off))] + fn eq(&self, other: &Self) -> bool { + match (self, other) { + (Error::NoValueToPropose, Error::NoValueToPropose) => true, + (Error::ProposerNotFound(addr1), Error::ProposerNotFound(addr2)) => addr1 == addr2, + (Error::ValidatorNotFound(addr1), Error::ValidatorNotFound(addr2)) => addr1 == addr2, + ( + Error::InvalidVoteSignature(vote1, validator1), + Error::InvalidVoteSignature(vote2, validator2), + ) => vote1 == vote2 && validator1 == validator2, + _ => false, + } + } +} diff --git a/Code/driver/src/event.rs b/Code/driver/src/event.rs index 8014971b9..fd54480da 100644 --- a/Code/driver/src/event.rs +++ b/Code/driver/src/event.rs @@ -1,5 +1,7 @@ use malachite_common::{Context, Round, SignedVote, Timeout}; +use crate::Validity; + /// Events that can be received by the [`Driver`](crate::Driver). #[derive(Clone, Debug, PartialEq, Eq)] pub enum Event @@ -8,10 +10,10 @@ where { /// A new round has started. /// The boolean indicates whether we are the proposer or not. - NewRound(Round, bool), + NewRound(Ctx::Height, Round), /// A new proposal has been received. - Proposal(Ctx::Proposal), + Proposal(Ctx::Proposal, Validity), /// A new vote has been received. Vote(SignedVote), diff --git a/Code/driver/src/lib.rs b/Code/driver/src/lib.rs index ce115e1e7..62401f55e 100644 --- a/Code/driver/src/lib.rs +++ b/Code/driver/src/lib.rs @@ -1,5 +1,6 @@ //! Driver for the state machine of the Malachite consensus engine +#![no_std] #![forbid(unsafe_code)] #![deny(unused_crate_dependencies, trivial_casts, trivial_numeric_casts)] #![warn( @@ -9,13 +10,25 @@ variant_size_differences )] #![cfg_attr(not(test), deny(clippy::unwrap_used, clippy::panic))] +#![cfg_attr(coverage_nightly, feature(coverage_attribute))] + +extern crate alloc; -mod client; mod driver; +mod env; +mod error; mod event; mod message; +mod proposer; +mod util; -pub use client::Client; pub use driver::Driver; +pub use env::Env; +pub use error::Error; pub use event::Event; pub use message::Message; +pub use proposer::ProposerSelector; +pub use util::Validity; + +// Re-export `#[async_trait]` macro for convenience. +pub use async_trait::async_trait; diff --git a/Code/driver/src/message.rs b/Code/driver/src/message.rs index e4ebde55d..b5f4d7073 100644 --- a/Code/driver/src/message.rs +++ b/Code/driver/src/message.rs @@ -1,7 +1,8 @@ +use core::fmt; + use malachite_common::{Context, Round, SignedVote, Timeout}; /// Messages emitted by the [`Driver`](crate::Driver) -#[derive(Clone, Debug, PartialEq, Eq)] pub enum Message where Ctx: Context, @@ -10,5 +11,61 @@ where Vote(SignedVote), Decide(Round, Ctx::Value), ScheduleTimeout(Timeout), - NewRound(Round), + NewRound(Ctx::Height, Round), } + +// 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::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::NewRound(height, round) => Message::NewRound(height.clone(), *round), + } + } +} + +impl fmt::Debug for Message { + #[cfg_attr(coverage_nightly, coverage(off))] + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + 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::NewRound(height, round) => write!(f, "NewRound({:?}, {:?})", height, round), + } + } +} + +impl PartialEq for Message { + #[cfg_attr(coverage_nightly, coverage(off))] + fn eq(&self, other: &Self) -> bool { + match (self, other) { + (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::NewRound(height, round), Message::NewRound(other_height, other_round)) => { + height == other_height && round == other_round + } + _ => false, + } + } +} + +impl Eq for Message {} diff --git a/Code/driver/src/proposer.rs b/Code/driver/src/proposer.rs new file mode 100644 index 000000000..47a0b4a75 --- /dev/null +++ b/Code/driver/src/proposer.rs @@ -0,0 +1,8 @@ +use malachite_common::{Context, Round}; + +pub trait ProposerSelector +where + Ctx: Context, +{ + fn select_proposer(&mut self, round: Round, validator_set: &Ctx::ValidatorSet) -> Ctx::Address; +} diff --git a/Code/driver/src/util.rs b/Code/driver/src/util.rs new file mode 100644 index 000000000..fd71a5915 --- /dev/null +++ b/Code/driver/src/util.rs @@ -0,0 +1,15 @@ +/// Wether or not a proposal is valid. +#[derive(Copy, Clone, Debug, PartialEq, Eq)] +pub enum Validity { + /// The proposal is valid. + Valid, + /// The proposal is invalid. + Invalid, +} + +impl Validity { + /// Returns `true` if the proposal is valid. + pub fn is_valid(self) -> bool { + self == Validity::Valid + } +} diff --git a/Code/itf/Cargo.toml b/Code/itf/Cargo.toml new file mode 100644 index 000000000..316394356 --- /dev/null +++ b/Code/itf/Cargo.toml @@ -0,0 +1,13 @@ +[package] +name = "malachite-itf" +description = "Library for working with ITF traces for the Malachite consensus engine" + +version.workspace = true +edition.workspace = true +repository.workspace = true +license.workspace = true +publish.workspace = true + +[dependencies] +itf.workspace = true +serde = { workspace = true, features = ["derive"] } diff --git a/Code/itf/src/consensus.rs b/Code/itf/src/consensus.rs new file mode 100644 index 000000000..f631e4f45 --- /dev/null +++ b/Code/itf/src/consensus.rs @@ -0,0 +1,177 @@ +use itf::{ItfBigInt, ItfMap}; +use serde::Deserialize; + +use crate::deserializers as de; + +pub type Address = String; +pub type Value = String; +pub type Step = String; +pub type Round = ItfBigInt; +pub type Height = ItfBigInt; + +#[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(ItfMap); + +#[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 == ItfBigInt::from(-1) + && self.round == ItfBigInt::from(-1) + && self.valid_round == ItfBigInt::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 == ItfBigInt::from(-1) + && self.round == ItfBigInt::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 new file mode 100644 index 000000000..192e39401 --- /dev/null +++ b/Code/itf/src/deserializers.rs @@ -0,0 +1,53 @@ +use itf::ItfBigInt; +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 == ItfBigInt::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 new file mode 100644 index 000000000..ce877e0f6 --- /dev/null +++ b/Code/itf/src/lib.rs @@ -0,0 +1,4 @@ +pub mod consensus; +pub mod votekeeper; + +mod deserializers; diff --git a/Code/itf/src/votekeeper.rs b/Code/itf/src/votekeeper.rs new file mode 100644 index 000000000..be3fb73ae --- /dev/null +++ b/Code/itf/src/votekeeper.rs @@ -0,0 +1,49 @@ +use itf::{ItfBigInt, ItfMap, ItfSet}; +use serde::Deserialize; + +pub type Height = ItfBigInt; +pub type Weight = ItfBigInt; +pub type Round = ItfBigInt; +pub type Address = String; +pub type Value = String; + +#[derive(Clone, Debug, PartialEq, Eq, Deserialize)] +#[serde(rename_all = "camelCase")] +pub struct Bookkeeper { + pub height: Height, + pub total_weight: Weight, + pub rounds: ItfMap, +} + +#[derive(Clone, Debug, PartialEq, Eq, Deserialize)] +#[serde(rename_all = "camelCase")] +pub struct RoundVotes { + pub height: Height, + pub round: Round, + pub prevotes: VoteCount, + pub precommits: VoteCount, + pub emitted_events: ItfSet, + pub votes_addresses_weights: ItfMap, +} + +#[derive(Clone, Debug, PartialEq, Eq, Deserialize)] +#[serde(rename_all = "camelCase")] +pub struct VoteCount { + pub total_weight: Weight, + pub values_weights: ItfMap, + pub votes_addresses: ItfSet
, +} + +#[derive(Clone, Debug, PartialEq, Eq, Deserialize, Hash)] +pub struct ExecutorEvent { + pub round: Round, + pub name: String, + pub value: Value, +} + +#[derive(Clone, Debug, PartialEq, Eq, Deserialize)] +#[serde(rename_all = "camelCase")] +pub struct State { + pub bookkeeper: Bookkeeper, + pub last_emitted: ExecutorEvent, +} diff --git a/Code/itf/tests/consensus.rs b/Code/itf/tests/consensus.rs new file mode 100644 index 000000000..435ec6481 --- /dev/null +++ b/Code/itf/tests/consensus.rs @@ -0,0 +1,21 @@ +use malachite_itf::consensus::State; + +#[test] +fn parse_fixtures() { + let folder = format!("{}/tests/fixtures/consensus", env!("CARGO_MANIFEST_DIR")); + + let fixtures = std::fs::read_dir(folder) + .unwrap() + .map(|entry| entry.unwrap().path()) + .filter(|path| path.extension().map_or(false, |ext| ext == "json")) + .collect::>(); + + for fixture in fixtures { + println!("Parsing '{}'", fixture.display()); + + let json = std::fs::read_to_string(&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 new file mode 100644 index 000000000..16347d3a4 --- /dev/null +++ b/Code/itf/tests/fixtures/consensus/consensus_DecideNonProposerTest_0.itf.json @@ -0,0 +1 @@ +{"#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/fixtures/votekeeper/voteBookkeeper_polkaAnyTest_6.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaAnyTest_6.itf.json new file mode 100644 index 000000000..e766285a1 --- /dev/null +++ b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaAnyTest_6.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"voteBookkeeper.qnt","status":"passed","description":"Created by Quint on Fri Nov 10 2023 14:26:21 GMT+0100 (GMT+01:00)","timestamp":1699622781761},"vars":["lastEmitted","bookkeeper"],"states":[{"#meta":{"index":0},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"","round":{"#bigint":"-1"},"value":"null"}},{"#meta":{"index":1},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":2},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":3},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"70"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}},{"#meta":{"index":4},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"70"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}},{"#meta":{"index":5},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":6},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":7},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"30"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":8},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"30"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":9},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"40"}]]},"votesAddresses":{"#set":["bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":10},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"40"}]]},"votesAddresses":{"#set":["bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":11},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"},{"name":"PrecommitValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alive","bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["alive",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PrecommitValue","round":{"#bigint":"1"},"value":"proposal"}}]} \ No newline at end of file diff --git a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaNilTest_7.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaNilTest_7.itf.json new file mode 100644 index 000000000..b5bf98cda --- /dev/null +++ b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaNilTest_7.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"voteBookkeeper.qnt","status":"passed","description":"Created by Quint on Fri Nov 10 2023 14:26:21 GMT+0100 (GMT+01:00)","timestamp":1699622781765},"vars":["lastEmitted","bookkeeper"],"states":[{"#meta":{"index":0},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"","round":{"#bigint":"-1"},"value":"null"}},{"#meta":{"index":1},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":2},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":3},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"70"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}},{"#meta":{"index":4},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"70"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}},{"#meta":{"index":5},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":6},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":7},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"30"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":8},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"30"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":9},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"40"}]]},"votesAddresses":{"#set":["bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":10},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"40"}]]},"votesAddresses":{"#set":["bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":11},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"},{"name":"PrecommitValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alive","bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["alive",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PrecommitValue","round":{"#bigint":"1"},"value":"proposal"}}]} \ No newline at end of file diff --git a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_synchronousConsensusTest_5.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_synchronousConsensusTest_5.itf.json new file mode 100644 index 000000000..75bc07e59 --- /dev/null +++ b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_synchronousConsensusTest_5.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"voteBookkeeper.qnt","status":"passed","description":"Created by Quint on Fri Nov 10 2023 14:26:21 GMT+0100 (GMT+01:00)","timestamp":1699622781758},"vars":["lastEmitted","bookkeeper"],"states":[{"#meta":{"index":0},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"","round":{"#bigint":"-1"},"value":"null"}},{"#meta":{"index":1},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":2},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":3},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"70"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}},{"#meta":{"index":4},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"70"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}},{"#meta":{"index":5},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":6},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":7},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"30"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":8},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"30"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":9},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"40"}]]},"votesAddresses":{"#set":["bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":10},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"40"}]]},"votesAddresses":{"#set":["bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":11},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"},{"name":"PrecommitValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alive","bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["alive",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PrecommitValue","round":{"#bigint":"1"},"value":"proposal"}}]} \ No newline at end of file diff --git a/Code/itf/tests/votekeeper.rs b/Code/itf/tests/votekeeper.rs new file mode 100644 index 000000000..1515d18ec --- /dev/null +++ b/Code/itf/tests/votekeeper.rs @@ -0,0 +1,22 @@ +use malachite_itf::votekeeper::State; + +#[test] +fn parse_fixtures() { + // read fixtures files in test/fixtures/votekeeper/ + let folder = format!("{}/tests/fixtures/votekeeper", env!("CARGO_MANIFEST_DIR")); + + let fixtures = std::fs::read_dir(folder) + .unwrap() + .map(|entry| entry.unwrap().path()) + .filter(|path| path.extension().map_or(false, |ext| ext == "json")) + .collect::>(); + + for fixture in fixtures { + println!("Parsing '{}'", fixture.display()); + + let json = std::fs::read_to_string(&fixture).unwrap(); + let trace = itf::trace_from_str::(&json).unwrap(); + + dbg!(trace); + } +} diff --git a/Code/round/src/lib.rs b/Code/round/src/lib.rs index 34ae70a59..d13887058 100644 --- a/Code/round/src/lib.rs +++ b/Code/round/src/lib.rs @@ -1,5 +1,6 @@ //! Per-round consensus state machine +#![no_std] #![forbid(unsafe_code)] #![deny(unused_crate_dependencies, trivial_casts, trivial_numeric_casts)] #![warn( @@ -9,6 +10,9 @@ variant_size_differences )] #![cfg_attr(not(test), deny(clippy::unwrap_used, clippy::panic))] +#![cfg_attr(coverage_nightly, feature(coverage_attribute))] + +extern crate alloc; pub mod events; pub mod message; diff --git a/Code/round/src/message.rs b/Code/round/src/message.rs index 8ec5a4556..877677f9e 100644 --- a/Code/round/src/message.rs +++ b/Code/round/src/message.rs @@ -1,8 +1,9 @@ +use core::fmt; + use malachite_common::{Context, Round, Timeout, TimeoutStep, ValueId}; use crate::state::RoundValue; -#[derive(Debug, PartialEq, Eq)] pub enum Message where Ctx: Context, @@ -14,25 +15,7 @@ where Decision(RoundValue), // Decide the value. } -impl Clone for Message -where - Ctx: Context, -{ - 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::Decision(round_value) => Message::Decision(round_value.clone()), - } - } -} - -impl Message -where - Ctx: Context, -{ +impl Message { pub fn proposal( height: Ctx::Height, round: Round, @@ -42,12 +25,22 @@ where Message::Proposal(Ctx::new_proposal(height, round, value, pol_round)) } - pub fn prevote(round: Round, value_id: Option>, address: Ctx::Address) -> Self { - Message::Vote(Ctx::new_prevote(round, value_id, address)) + pub fn prevote( + height: Ctx::Height, + round: Round, + value_id: Option>, + address: Ctx::Address, + ) -> Self { + Message::Vote(Ctx::new_prevote(height, round, value_id, address)) } - pub fn precommit(round: Round, value_id: Option>, address: Ctx::Address) -> Self { - Message::Vote(Ctx::new_precommit(round, value_id, address)) + pub fn precommit( + height: Ctx::Height, + round: Round, + value_id: Option>, + address: Ctx::Address, + ) -> Self { + Message::Vote(Ctx::new_precommit(height, round, value_id, address)) } pub fn schedule_timeout(round: Round, step: TimeoutStep) -> Self { @@ -58,3 +51,55 @@ where Message::Decision(RoundValue { round, value }) } } + +// 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(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::Decision(round_value) => Message::Decision(round_value.clone()), + } + } +} + +impl fmt::Debug for Message { + #[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::Decision(round_value) => write!(f, "Decision({:?})", round_value), + } + } +} + +impl PartialEq for Message { + #[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)) => { + proposal == other_proposal + } + (Message::Vote(vote), Message::Vote(other_vote)) => vote == other_vote, + (Message::ScheduleTimeout(timeout), Message::ScheduleTimeout(other_timeout)) => { + timeout == other_timeout + } + (Message::Decision(round_value), Message::Decision(other_round_value)) => { + round_value == other_round_value + } + _ => false, + } + } +} + +impl Eq for Message {} diff --git a/Code/round/src/state.rs b/Code/round/src/state.rs index 55ef389b4..c7edc6e5e 100644 --- a/Code/round/src/state.rs +++ b/Code/round/src/state.rs @@ -1,3 +1,5 @@ +use core::fmt; + use crate::events::Event; use crate::state_machine::RoundData; use crate::transition::Transition; @@ -28,11 +30,11 @@ pub enum Step { } /// The state of the consensus state machine -#[derive(Debug, PartialEq, Eq)] pub struct State where Ctx: Context, { + pub height: Ctx::Height, pub round: Round, pub step: Step, pub proposal: Option, @@ -40,28 +42,14 @@ where pub valid: Option>, } -impl Clone for State -where - Ctx: Context, -{ - fn clone(&self) -> Self { - Self { - round: self.round, - step: self.step, - proposal: self.proposal.clone(), - locked: self.locked.clone(), - valid: self.valid.clone(), - } - } -} - impl State where Ctx: Context, { - pub fn new() -> Self { + pub fn new(height: Ctx::Height, round: Round) -> Self { Self { - round: Round::INITIAL, + height, + round, step: Step::NewRound, proposal: None, locked: None, @@ -69,13 +57,6 @@ where } } - pub fn new_round(self, round: Round) -> Self { - Self { - round, - step: Step::NewRound, - ..self - } - } pub fn with_step(self, step: Step) -> Self { Self { step, ..self } } @@ -99,11 +80,64 @@ where } } +// 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 Default for State where Ctx: Context, { fn default() -> Self { - Self::new() + Self::new(Ctx::Height::default(), Round::NIL) + } +} + +impl Clone for State +where + Ctx: Context, +{ + #[cfg_attr(coverage_nightly, coverage(off))] + fn clone(&self) -> Self { + Self { + height: self.height.clone(), + round: self.round, + step: self.step, + proposal: self.proposal.clone(), + locked: self.locked.clone(), + valid: self.valid.clone(), + } } } + +impl fmt::Debug for State +where + Ctx: Context, +{ + #[cfg_attr(coverage_nightly, coverage(off))] + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.debug_struct("State") + .field("round", &self.round) + .field("step", &self.step) + .field("proposal", &self.proposal) + .field("locked", &self.locked) + .field("valid", &self.valid) + .finish() + } +} + +impl PartialEq for State +where + Ctx: Context, +{ + #[cfg_attr(coverage_nightly, coverage(off))] + fn eq(&self, other: &Self) -> bool { + self.round == other.round + && self.step == other.step + && self.proposal == other.proposal + && self.locked == other.locked + && self.valid == other.valid + } +} + +impl Eq for State where Ctx: Context {} diff --git a/Code/round/src/state_machine.rs b/Code/round/src/state_machine.rs index 5376a78ea..6c91137f2 100644 --- a/Code/round/src/state_machine.rs +++ b/Code/round/src/state_machine.rs @@ -16,7 +16,7 @@ where Ctx: Context, { pub round: Round, - pub height: &'a Ctx::Height, + pub height: Ctx::Height, pub address: &'a Ctx::Address, } @@ -24,7 +24,7 @@ impl<'a, Ctx> RoundData<'a, Ctx> where Ctx: Context, { - pub fn new(round: Round, height: &'a Ctx::Height, address: &'a Ctx::Address) -> Self { + pub fn new(round: Round, height: Ctx::Height, address: &'a Ctx::Address) -> Self { Self { round, height, @@ -62,7 +62,7 @@ where match (state.step, event) { // From NewRound. Event must be for current round. (Step::NewRound, Event::NewRoundProposer(value)) if this_round => { - propose(state, data.height, value) // L11/L14 + propose(state, &data.height, value) // L11/L14 } (Step::NewRound, Event::NewRound) if this_round => schedule_timeout_propose(state), // L11/L20 @@ -173,7 +173,7 @@ where None => Some(proposed), // not locked, prevote the value }; - let message = Message::prevote(state.round, value, address.clone()); + let message = Message::prevote(state.height.clone(), state.round, value, address.clone()); Transition::to(state.with_step(Step::Prevote)).with_message(message) } @@ -184,7 +184,7 @@ pub fn prevote_nil(state: State, address: &Ctx::Address) -> Transition where Ctx: Context, { - let message = Message::prevote(state.round, None, address.clone()); + let message = Message::prevote(state.height.clone(), state.round, None, address.clone()); Transition::to(state.with_step(Step::Prevote)).with_message(message) } @@ -211,7 +211,12 @@ where } let value = proposal.value(); - let message = Message::precommit(state.round, Some(value.id()), address.clone()); + let message = Message::precommit( + state.height.clone(), + state.round, + Some(value.id()), + address.clone(), + ); let current_value = match state.proposal { Some(ref proposal) => proposal.value().clone(), @@ -238,7 +243,7 @@ pub fn precommit_nil(state: State, address: &Ctx::Address) -> Transiti where Ctx: Context, { - let message = Message::precommit(state.round, None, address.clone()); + let message = Message::precommit(state.height.clone(), state.round, None, address.clone()); Transition::to(state.with_step(Step::Precommit)).with_message(message) } @@ -326,7 +331,7 @@ pub fn round_skip(state: State, round: Round) -> Transition where Ctx: Context, { - Transition::to(state.new_round(round)).with_message(Message::NewRound(round)) + Transition::to(State::new(state.height.clone(), round)).with_message(Message::NewRound(round)) } /// We received +2/3 precommits for a value - commit and decide that value! diff --git a/Code/tendermint/Cargo.toml b/Code/tendermint/Cargo.toml index 2a979a82d..962515ad4 100644 --- a/Code/tendermint/Cargo.toml +++ b/Code/tendermint/Cargo.toml @@ -12,7 +12,6 @@ malachite-common = { version = "0.1.0", path = "../common" } ed25519-consensus.workspace = true rand.workspace = true -secrecy.workspace = true sha2.workspace = true signature.workspace = true tendermint.workspace = true diff --git a/Code/tendermint/src/ed25519.rs b/Code/tendermint/src/ed25519.rs index af120d071..48c8b338d 100644 --- a/Code/tendermint/src/ed25519.rs +++ b/Code/tendermint/src/ed25519.rs @@ -1,6 +1,5 @@ use malachite_common::SigningScheme; use rand::{CryptoRng, RngCore}; -use secrecy::{CloneableSecret, DebugSecret, Zeroize}; use signature::{Keypair, Signer, Verifier}; pub use ed25519_consensus::Signature; @@ -55,15 +54,6 @@ impl Keypair for PrivateKey { } } -impl Zeroize for PrivateKey { - fn zeroize(&mut self) { - self.0.zeroize() - } -} - -impl DebugSecret for PrivateKey {} -impl CloneableSecret for PrivateKey {} - #[derive(Copy, Clone, Debug, PartialEq, Eq)] pub struct PublicKey(ed25519_consensus::VerificationKey); diff --git a/Code/tendermint/src/lib.rs b/Code/tendermint/src/lib.rs index 42ea31e1e..13e3b43dd 100644 --- a/Code/tendermint/src/lib.rs +++ b/Code/tendermint/src/lib.rs @@ -1,6 +1,9 @@ #![allow(unused_variables)] +use core::fmt; + use malachite_common as mc; +use mc::SignedVote; use tendermint as tm; pub mod ed25519; @@ -20,7 +23,13 @@ impl Context { pub struct Address(tm::account::Id); impl mc::Address for Address {} -#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord)] +impl fmt::Display for Address { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + self.0.fmt(f) + } +} + +#[derive(Copy, Clone, Debug, Default, PartialEq, Eq, PartialOrd, Ord)] pub struct Height(tm::block::Height); impl mc::Height for Height {} @@ -97,6 +106,10 @@ impl mc::ValidatorSet for ValidatorSet { pub struct Vote(tm::vote::Vote); impl mc::Vote for Vote { + fn height(&self) -> Height { + Height(self.0.height) + } + fn round(&self) -> mc::Round { mc::Round::from(self.0.round.value()) } @@ -127,11 +140,7 @@ impl mc::Context for Context { type Vote = Vote; type SigningScheme = crate::ed25519::Ed25519; - fn sign_vote( - &self, - vote: &Self::Vote, - private_key: &mc::PrivateKey, - ) -> mc::Signature { + fn sign_vote(&self, vote: Self::Vote) -> SignedVote { todo!() } @@ -167,11 +176,21 @@ impl mc::Context for Context { todo!() } - fn new_prevote(round: mc::Round, value_id: Option, address: Address) -> Self::Vote { + fn new_prevote( + height: Height, + round: mc::Round, + value_id: Option, + address: Address, + ) -> Self::Vote { todo!() } - fn new_precommit(round: mc::Round, value_id: Option, address: Address) -> Self::Vote { + fn new_precommit( + height: Height, + round: mc::Round, + value_id: Option, + address: Address, + ) -> Self::Vote { todo!() } } diff --git a/Code/test/Cargo.toml b/Code/test/Cargo.toml index 6b536bce3..93e682d9c 100644 --- a/Code/test/Cargo.toml +++ b/Code/test/Cargo.toml @@ -14,8 +14,10 @@ malachite-driver = { version = "0.1.0", path = "../driver" } malachite-round = { version = "0.1.0", path = "../round" } malachite-vote = { version = "0.1.0", path = "../vote" } +futures = { workspace = true, features = ["executor"] } + +async-trait.workspace = true ed25519-consensus.workspace = true signature.workspace = true rand.workspace = true sha2.workspace = true -secrecy.workspace = true diff --git a/Code/test/src/client.rs b/Code/test/src/client.rs deleted file mode 100644 index cc66f2381..000000000 --- a/Code/test/src/client.rs +++ /dev/null @@ -1,24 +0,0 @@ -use malachite_driver::Client; - -use crate::{Proposal, TestContext, Value}; - -pub struct TestClient { - pub value: Value, - pub is_valid: fn(&Proposal) -> bool, -} - -impl TestClient { - pub fn new(value: Value, is_valid: fn(&Proposal) -> bool) -> Self { - Self { value, is_valid } - } -} - -impl Client for TestClient { - fn get_value(&self) -> Value { - self.value.clone() - } - - fn validate_proposal(&self, proposal: &Proposal) -> bool { - (self.is_valid)(proposal) - } -} diff --git a/Code/test/src/context.rs b/Code/test/src/context.rs index ee2a3f413..28ff263be 100644 --- a/Code/test/src/context.rs +++ b/Code/test/src/context.rs @@ -4,13 +4,21 @@ use malachite_common::SignedVote; use crate::height::*; use crate::proposal::*; -use crate::signing::{Ed25519, PrivateKey, PublicKey, Signature}; +use crate::signing::{Ed25519, PrivateKey, PublicKey}; use crate::validator_set::*; use crate::value::*; use crate::vote::*; -#[derive(Copy, Clone, Debug, PartialEq, Eq)] -pub struct TestContext; +#[derive(Clone, Debug)] +pub struct TestContext { + private_key: PrivateKey, +} + +impl TestContext { + pub fn new(private_key: PrivateKey) -> Self { + Self { private_key } + } +} impl Context for TestContext { type Address = Address; @@ -22,9 +30,10 @@ impl Context for TestContext { type Vote = Vote; type SigningScheme = Ed25519; - fn sign_vote(&self, vote: &Self::Vote, private_key: &PrivateKey) -> Signature { + fn sign_vote(&self, vote: Self::Vote) -> SignedVote { use signature::Signer; - private_key.sign(&vote.to_bytes()) + let signature = self.private_key.sign(&vote.to_bytes()); + SignedVote::new(vote, signature) } fn verify_signed_vote(&self, signed_vote: &SignedVote, public_key: &PublicKey) -> bool { @@ -38,11 +47,21 @@ impl Context for TestContext { Proposal::new(height, round, value, pol_round) } - fn new_prevote(round: Round, value_id: Option, address: Address) -> Vote { - Vote::new_prevote(round, value_id, address) + fn new_prevote( + height: Height, + round: Round, + value_id: Option, + address: Address, + ) -> Vote { + Vote::new_prevote(height, round, value_id, address) } - fn new_precommit(round: Round, value_id: Option, address: Address) -> Vote { - Vote::new_precommit(round, value_id, address) + fn new_precommit( + height: Height, + round: Round, + value_id: Option, + address: Address, + ) -> Vote { + Vote::new_precommit(height, round, value_id, address) } } diff --git a/Code/test/src/env.rs b/Code/test/src/env.rs new file mode 100644 index 000000000..af79543a4 --- /dev/null +++ b/Code/test/src/env.rs @@ -0,0 +1,25 @@ +use async_trait::async_trait; + +use malachite_common::Round; +use malachite_driver::Env; + +use crate::{Height, TestContext, Value}; + +pub struct TestEnv { + get_value: Box Option + Send + Sync>, +} + +impl TestEnv { + pub fn new(get_value: impl Fn(Height, Round) -> Option + Send + Sync + 'static) -> Self { + Self { + get_value: Box::new(get_value), + } + } +} + +#[async_trait] +impl Env for TestEnv { + async fn get_value(&self, height: Height, round: Round) -> Option { + (self.get_value)(height, round) + } +} diff --git a/Code/test/src/lib.rs b/Code/test/src/lib.rs index fc979bccb..8e09b3a31 100644 --- a/Code/test/src/lib.rs +++ b/Code/test/src/lib.rs @@ -1,8 +1,9 @@ #![forbid(unsafe_code)] #![deny(trivial_casts, trivial_numeric_casts)] +#![cfg_attr(coverage_nightly, feature(coverage_attribute))] -mod client; mod context; +mod env; mod height; mod proposal; mod signing; @@ -10,8 +11,8 @@ mod validator_set; mod value; mod vote; -pub use crate::client::*; pub use crate::context::*; +pub use crate::env::*; pub use crate::height::*; pub use crate::proposal::*; pub use crate::signing::*; diff --git a/Code/test/src/signing.rs b/Code/test/src/signing.rs index af120d071..a0564f497 100644 --- a/Code/test/src/signing.rs +++ b/Code/test/src/signing.rs @@ -1,6 +1,5 @@ use malachite_common::SigningScheme; use rand::{CryptoRng, RngCore}; -use secrecy::{CloneableSecret, DebugSecret, Zeroize}; use signature::{Keypair, Signer, Verifier}; pub use ed25519_consensus::Signature; @@ -9,6 +8,7 @@ pub use ed25519_consensus::Signature; pub struct Ed25519; impl Ed25519 { + #[cfg_attr(coverage_nightly, coverage(off))] pub fn generate_keypair(rng: R) -> PrivateKey where R: RngCore + CryptoRng, @@ -27,6 +27,7 @@ impl SigningScheme for Ed25519 { pub struct PrivateKey(ed25519_consensus::SigningKey); impl PrivateKey { + #[cfg_attr(coverage_nightly, coverage(off))] pub fn generate(rng: R) -> Self where R: RngCore + CryptoRng, @@ -36,6 +37,7 @@ impl PrivateKey { Self(signing_key) } + #[cfg_attr(coverage_nightly, coverage(off))] pub fn public_key(&self) -> PublicKey { PublicKey::new(self.0.verification_key()) } @@ -55,15 +57,6 @@ impl Keypair for PrivateKey { } } -impl Zeroize for PrivateKey { - fn zeroize(&mut self) { - self.0.zeroize() - } -} - -impl DebugSecret for PrivateKey {} -impl CloneableSecret for PrivateKey {} - #[derive(Copy, Clone, Debug, PartialEq, Eq)] pub struct PublicKey(ed25519_consensus::VerificationKey); diff --git a/Code/test/src/validator_set.rs b/Code/test/src/validator_set.rs index 183680c2c..cc2010f0e 100644 --- a/Code/test/src/validator_set.rs +++ b/Code/test/src/validator_set.rs @@ -1,3 +1,5 @@ +use core::fmt; + use malachite_common::VotingPower; use crate::{signing::PublicKey, TestContext}; @@ -8,10 +10,12 @@ pub struct Address([u8; Self::LENGTH]); impl Address { const LENGTH: usize = 20; + #[cfg_attr(coverage_nightly, coverage(off))] pub const fn new(value: [u8; Self::LENGTH]) -> Self { Self(value) } + #[cfg_attr(coverage_nightly, coverage(off))] pub fn from_public_key(public_key: &PublicKey) -> Self { let hash = public_key.hash(); let mut address = [0; Self::LENGTH]; @@ -20,6 +24,16 @@ impl Address { } } +impl fmt::Display for Address { + #[cfg_attr(coverage_nightly, coverage(off))] + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + for byte in self.0.iter() { + write!(f, "{:02x}", byte)?; + } + Ok(()) + } +} + impl malachite_common::Address for Address {} /// A validator is a public key and voting power @@ -31,6 +45,7 @@ pub struct Validator { } impl Validator { + #[cfg_attr(coverage_nightly, coverage(off))] pub fn new(public_key: PublicKey, voting_power: VotingPower) -> Self { Self { address: Address::from_public_key(&public_key), @@ -56,7 +71,7 @@ impl malachite_common::Validator for Validator { /// A validator set contains a list of validators sorted by address. pub struct ValidatorSet { - validators: Vec, + pub validators: Vec, } impl ValidatorSet { @@ -64,7 +79,7 @@ impl ValidatorSet { let mut validators: Vec<_> = validators.into_iter().collect(); assert!(!validators.is_empty()); - ValidatorSet::sort_validators(&mut validators); + Self::sort_validators(&mut validators); Self { validators } } diff --git a/Code/test/src/value.rs b/Code/test/src/value.rs index 272cf1713..bed49dbf6 100644 --- a/Code/test/src/value.rs +++ b/Code/test/src/value.rs @@ -18,7 +18,7 @@ impl From for ValueId { } /// The value to decide on -#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)] +#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord)] pub struct Value(u64); impl Value { @@ -30,10 +30,6 @@ impl Value { self.0 } - pub const fn valid(&self) -> bool { - self.0 > 0 - } - pub const fn id(&self) -> ValueId { ValueId(self.0) } @@ -46,9 +42,3 @@ impl malachite_common::Value for Value { self.id() } } - -impl From for Value { - fn from(value: u64) -> Self { - Self::new(value) - } -} diff --git a/Code/test/src/vote.rs b/Code/test/src/vote.rs index 4d78ce7b6..52ce48e09 100644 --- a/Code/test/src/vote.rs +++ b/Code/test/src/vote.rs @@ -2,30 +2,43 @@ use signature::Signer; use malachite_common::{Round, SignedVote, VoteType}; -use crate::{Address, PrivateKey, TestContext, ValueId}; +use crate::{Address, Height, PrivateKey, TestContext, ValueId}; /// A vote for a value in a round #[derive(Clone, Debug, PartialEq, Eq)] pub struct Vote { pub typ: VoteType, + pub height: Height, pub round: Round, pub value: Option, pub validator_address: Address, } impl Vote { - pub fn new_prevote(round: Round, value: Option, validator_address: Address) -> Self { + pub fn new_prevote( + height: Height, + round: Round, + value: Option, + validator_address: Address, + ) -> Self { Self { typ: VoteType::Prevote, + height, round, value, validator_address, } } - pub fn new_precommit(round: Round, value: Option, address: Address) -> Self { + pub fn new_precommit( + height: Height, + round: Round, + value: Option, + address: Address, + ) -> Self { Self { typ: VoteType::Precommit, + height, round, value, validator_address: address, @@ -61,6 +74,10 @@ impl Vote { } impl malachite_common::Vote for Vote { + fn height(&self) -> Height { + self.height + } + fn round(&self) -> Round { self.round } diff --git a/Code/test/tests/driver.rs b/Code/test/tests/driver.rs index 77ff8f9f1..93d4006ba 100644 --- a/Code/test/tests/driver.rs +++ b/Code/test/tests/driver.rs @@ -1,13 +1,14 @@ +use futures::executor::block_on; +use rand::rngs::StdRng; +use rand::SeedableRng; + use malachite_common::{Round, Timeout}; -use malachite_driver::{Driver, Event, Message}; +use malachite_driver::{Driver, Error, Event, Message, ProposerSelector, Validity}; use malachite_round::state::{RoundValue, State, Step}; - use malachite_test::{ - Address, Height, PrivateKey, Proposal, TestClient, TestContext, Validator, ValidatorSet, Value, + Address, Height, PrivateKey, Proposal, TestContext, TestEnv, Validator, ValidatorSet, Value, Vote, }; -use rand::rngs::StdRng; -use rand::SeedableRng; struct TestStep { desc: &'static str, @@ -19,22 +20,51 @@ struct TestStep { fn to_input_msg(output: Message) -> Option> { match output { - Message::Propose(p) => Some(Event::Proposal(p)), + // 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::NewRound(height, round) => Some(Event::NewRound(height, round)), + } +} + +#[derive(Copy, Clone, Debug, Default)] +pub struct RotateProposer { + proposer_index: usize, +} - // XXX: we are only testing non-proposer after the initial round - Message::NewRound(round) => Some(Event::NewRound(round, false)), +impl ProposerSelector for RotateProposer { + fn select_proposer(&mut self, _round: Round, validator_set: &ValidatorSet) -> Address { + let proposer = &validator_set.validators[self.proposer_index]; + self.proposer_index = (self.proposer_index + 1) % validator_set.validators.len(); + proposer.address + } +} + +#[derive(Copy, Clone, Debug)] +pub struct FixedProposer { + proposer: Address, +} + +impl FixedProposer { + pub fn new(proposer: Address) -> Self { + Self { proposer } + } +} + +impl ProposerSelector for FixedProposer { + fn select_proposer(&mut self, _round: Round, _validator_set: &ValidatorSet) -> Address { + self.proposer } } #[test] fn driver_steps_proposer() { let value = Value::new(9999); - let value_id = value.id(); - let client = TestClient::new(value.clone(), |_| true); + let sel = RotateProposer::default(); + let env = TestEnv::new(move |_, _| Some(value)); let mut rng = StdRng::seed_from_u64(0x42); @@ -52,25 +82,21 @@ fn driver_steps_proposer() { let (my_sk, my_addr) = (sk1, addr1); + let ctx = TestContext::new(my_sk.clone()); + let vs = ValidatorSet::new(vec![v1, v2.clone(), v3.clone()]); - let mut driver = Driver::new( - TestContext, - client, - Height::new(1), - vs, - my_sk.clone(), - my_addr, - ); + let mut driver = Driver::new(ctx, env, sel, vs, my_addr); - let proposal = Proposal::new(Height::new(1), Round::new(0), value.clone(), Round::new(-1)); + let proposal = Proposal::new(Height::new(1), Round::new(0), value, Round::new(-1)); let steps = vec![ TestStep { desc: "Start round 0, we are proposer, propose value", - input_event: Some(Event::NewRound(Round::new(0), true)), + input_event: Some(Event::NewRound(Height::new(1), Round::new(0))), expected_output: Some(Message::Propose(proposal.clone())), expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Propose, proposal: None, @@ -82,10 +108,12 @@ fn driver_steps_proposer() { desc: "Receive our own proposal, prevote for it (v1)", input_event: None, expected_output: Some(Message::Vote( - Vote::new_prevote(Round::new(0), Some(value_id), my_addr).signed(&my_sk), + Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), my_addr) + .signed(&my_sk), )), expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Prevote, proposal: Some(proposal.clone()), @@ -99,6 +127,7 @@ fn driver_steps_proposer() { expected_output: None, expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Prevote, proposal: Some(proposal.clone()), @@ -109,11 +138,13 @@ fn driver_steps_proposer() { TestStep { desc: "v2 prevotes for our proposal", input_event: Some(Event::Vote( - Vote::new_prevote(Round::new(0), Some(value_id), addr2).signed(&sk2), + Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), addr2) + .signed(&sk2), )), expected_output: None, expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Prevote, proposal: Some(proposal.clone()), @@ -124,22 +155,25 @@ 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( - Vote::new_prevote(Round::new(0), Some(value_id), addr3).signed(&sk3), + Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), addr3) + .signed(&sk3), )), expected_output: Some(Message::Vote( - Vote::new_precommit(Round::new(0), Some(value_id), my_addr).signed(&my_sk), + Vote::new_precommit(Height::new(1), Round::new(0), Some(value.id()), my_addr) + .signed(&my_sk), )), expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Precommit, proposal: Some(proposal.clone()), locked: Some(RoundValue { - value: value.clone(), + value, round: Round::new(0), }), valid: Some(RoundValue { - value: value.clone(), + value, round: Round::new(0), }), }, @@ -150,15 +184,16 @@ fn driver_steps_proposer() { expected_output: None, expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Precommit, proposal: Some(proposal.clone()), locked: Some(RoundValue { - value: value.clone(), + value, round: Round::new(0), }), valid: Some(RoundValue { - value: value.clone(), + value, round: Round::new(0), }), }, @@ -166,20 +201,22 @@ fn driver_steps_proposer() { TestStep { desc: "v2 precommits for our proposal", input_event: Some(Event::Vote( - Vote::new_precommit(Round::new(0), Some(value_id), addr2).signed(&sk2), + Vote::new_precommit(Height::new(1), Round::new(0), Some(value.id()), addr2) + .signed(&sk2), )), expected_output: None, expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Precommit, proposal: Some(proposal.clone()), locked: Some(RoundValue { - value: value.clone(), + value, round: Round::new(0), }), valid: Some(RoundValue { - value: value.clone(), + value, round: Round::new(0), }), }, @@ -187,20 +224,22 @@ fn driver_steps_proposer() { TestStep { desc: "v3 precommits for our proposal, we get +2/3 precommits, decide it (v1)", input_event: Some(Event::Vote( - Vote::new_precommit(Round::new(0), Some(value_id), addr3).signed(&sk3), + Vote::new_precommit(Height::new(1), Round::new(0), Some(value.id()), addr3) + .signed(&sk3), )), - expected_output: Some(Message::Decide(Round::new(0), value.clone())), + expected_output: Some(Message::Decide(Round::new(0), value)), expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Commit, proposal: Some(proposal.clone()), locked: Some(RoundValue { - value: value.clone(), + value, round: Round::new(0), }), valid: Some(RoundValue { - value: value.clone(), + value, round: Round::new(0), }), }, @@ -216,13 +255,15 @@ fn driver_steps_proposer() { .input_event .unwrap_or_else(|| previous_message.unwrap()); - let output = driver.execute(execute_message); + let output = block_on(driver.execute(execute_message)).expect("execute succeeded"); assert_eq!(output, step.expected_output, "expected output message"); - assert_eq!(driver.round, step.expected_round, "expected round"); + assert_eq!( + driver.round_state.round, step.expected_round, + "expected round" + ); - let new_state = driver.round_state(Round::new(0)).unwrap(); - assert_eq!(new_state, &step.new_state, "expected state"); + assert_eq!(driver.round_state, step.new_state, "expected state"); previous_message = output.and_then(to_input_msg); } @@ -231,9 +272,9 @@ fn driver_steps_proposer() { #[test] fn driver_steps_not_proposer_valid() { let value = Value::new(9999); - let value_id = value.id(); - let client = TestClient::new(value.clone(), |_| true); + let sel = RotateProposer::default(); + let env = TestEnv::new(move |_, _| Some(value)); let mut rng = StdRng::seed_from_u64(0x42); @@ -252,25 +293,21 @@ fn driver_steps_not_proposer_valid() { // Proposer is v1, so we are not the proposer let (my_sk, my_addr) = (sk2, addr2); + let ctx = TestContext::new(my_sk.clone()); + let vs = ValidatorSet::new(vec![v1.clone(), v2.clone(), v3.clone()]); - let mut driver = Driver::new( - TestContext, - client, - Height::new(1), - vs, - my_sk.clone(), - my_addr, - ); + let mut driver = Driver::new(ctx, env, sel, vs, my_addr); - let proposal = Proposal::new(Height::new(1), Round::new(0), value.clone(), Round::new(-1)); + let proposal = Proposal::new(Height::new(1), Round::new(0), value, Round::new(-1)); let steps = vec![ TestStep { desc: "Start round 0, we are not the proposer", - input_event: Some(Event::NewRound(Round::new(0), false)), + input_event: Some(Event::NewRound(Height::new(1), Round::new(0))), expected_output: Some(Message::ScheduleTimeout(Timeout::propose(Round::new(0)))), expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Propose, proposal: None, @@ -280,12 +317,14 @@ fn driver_steps_not_proposer_valid() { }, TestStep { desc: "Receive a proposal, prevote for it (v2)", - input_event: Some(Event::Proposal(proposal.clone())), + input_event: Some(Event::Proposal(proposal.clone(), Validity::Valid)), expected_output: Some(Message::Vote( - Vote::new_prevote(Round::new(0), Some(value_id), my_addr).signed(&my_sk), + Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), my_addr) + .signed(&my_sk), )), expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Prevote, proposal: Some(proposal.clone()), @@ -299,6 +338,7 @@ fn driver_steps_not_proposer_valid() { expected_output: None, expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Prevote, proposal: Some(proposal.clone()), @@ -309,11 +349,13 @@ fn driver_steps_not_proposer_valid() { TestStep { desc: "v1 prevotes for its own proposal", input_event: Some(Event::Vote( - Vote::new_prevote(Round::new(0), Some(value_id), addr1).signed(&sk1), + Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), addr1) + .signed(&sk1), )), expected_output: None, expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Prevote, proposal: Some(proposal.clone()), @@ -324,22 +366,25 @@ 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( - Vote::new_prevote(Round::new(0), Some(value_id), addr3).signed(&sk3), + Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), addr3) + .signed(&sk3), )), expected_output: Some(Message::Vote( - Vote::new_precommit(Round::new(0), Some(value_id), my_addr).signed(&my_sk), + Vote::new_precommit(Height::new(1), Round::new(0), Some(value.id()), my_addr) + .signed(&my_sk), )), expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Precommit, proposal: Some(proposal.clone()), locked: Some(RoundValue { - value: value.clone(), + value, round: Round::new(0), }), valid: Some(RoundValue { - value: value.clone(), + value, round: Round::new(0), }), }, @@ -350,15 +395,16 @@ fn driver_steps_not_proposer_valid() { expected_output: None, expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Precommit, proposal: Some(proposal.clone()), locked: Some(RoundValue { - value: value.clone(), + value, round: Round::new(0), }), valid: Some(RoundValue { - value: value.clone(), + value, round: Round::new(0), }), }, @@ -366,20 +412,22 @@ fn driver_steps_not_proposer_valid() { TestStep { desc: "v1 precommits its proposal", input_event: Some(Event::Vote( - Vote::new_precommit(Round::new(0), Some(value_id), addr1).signed(&sk1), + Vote::new_precommit(Height::new(1), Round::new(0), Some(value.id()), addr1) + .signed(&sk1), )), expected_output: None, expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Precommit, proposal: Some(proposal.clone()), locked: Some(RoundValue { - value: value.clone(), + value, round: Round::new(0), }), valid: Some(RoundValue { - value: value.clone(), + value, round: Round::new(0), }), }, @@ -387,20 +435,22 @@ 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( - Vote::new_precommit(Round::new(0), Some(value_id), addr3).signed(&sk3), + Vote::new_precommit(Height::new(1), Round::new(0), Some(value.id()), addr3) + .signed(&sk3), )), - expected_output: Some(Message::Decide(Round::new(0), value.clone())), + expected_output: Some(Message::Decide(Round::new(0), value)), expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Commit, proposal: Some(proposal.clone()), locked: Some(RoundValue { - value: value.clone(), + value, round: Round::new(0), }), valid: Some(RoundValue { - value: value.clone(), + value, round: Round::new(0), }), }, @@ -416,13 +466,15 @@ fn driver_steps_not_proposer_valid() { .input_event .unwrap_or_else(|| previous_message.unwrap()); - let output = driver.execute(execute_message); + let output = block_on(driver.execute(execute_message)).expect("execute succeeded"); assert_eq!(output, step.expected_output, "expected output message"); - assert_eq!(driver.round, step.expected_round, "expected round"); + assert_eq!( + driver.round_state.round, step.expected_round, + "expected round" + ); - let new_state = driver.round_state(Round::new(0)).unwrap(); - assert_eq!(new_state, &step.new_state, "expected state"); + assert_eq!(driver.round_state, step.new_state, "expected state"); previous_message = output.and_then(to_input_msg); } @@ -431,9 +483,9 @@ fn driver_steps_not_proposer_valid() { #[test] fn driver_steps_not_proposer_invalid() { let value = Value::new(9999); - let value_id = value.id(); - let client = TestClient::new(value.clone(), |_| false); + let sel = RotateProposer::default(); + let env = TestEnv::new(move |_, _| Some(value)); let mut rng = StdRng::seed_from_u64(0x42); @@ -452,25 +504,21 @@ fn driver_steps_not_proposer_invalid() { // Proposer is v1, so we are not the proposer let (my_sk, my_addr) = (sk2, addr2); + let ctx = TestContext::new(my_sk.clone()); + let vs = ValidatorSet::new(vec![v1.clone(), v2.clone(), v3.clone()]); - let mut driver = Driver::new( - TestContext, - client, - Height::new(1), - vs, - my_sk.clone(), - my_addr, - ); + let mut driver = Driver::new(ctx, env, sel, vs, my_addr); - let proposal = Proposal::new(Height::new(1), Round::new(0), value.clone(), Round::new(-1)); + let proposal = Proposal::new(Height::new(1), Round::new(0), value, Round::new(-1)); let steps = vec![ TestStep { desc: "Start round 0, we are not the proposer", - input_event: Some(Event::NewRound(Round::new(0), false)), + input_event: Some(Event::NewRound(Height::new(1), Round::new(0))), expected_output: Some(Message::ScheduleTimeout(Timeout::propose(Round::new(0)))), expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Propose, proposal: None, @@ -480,12 +528,13 @@ fn driver_steps_not_proposer_invalid() { }, TestStep { desc: "Receive an invalid proposal, prevote for nil (v2)", - input_event: Some(Event::Proposal(proposal.clone())), + input_event: Some(Event::Proposal(proposal.clone(), Validity::Invalid)), expected_output: Some(Message::Vote( - Vote::new_prevote(Round::new(0), None, my_addr).signed(&my_sk), + Vote::new_prevote(Height::new(1),Round::new(0), None, my_addr).signed(&my_sk), )), expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Prevote, proposal: None, @@ -499,6 +548,7 @@ fn driver_steps_not_proposer_invalid() { expected_output: None, expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Prevote, proposal: None, @@ -509,11 +559,12 @@ fn driver_steps_not_proposer_invalid() { TestStep { desc: "v1 prevotes for its own proposal", input_event: Some(Event::Vote( - Vote::new_prevote(Round::new(0), Some(value_id), addr1).signed(&sk1), + Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), addr1).signed(&sk1), )), expected_output: None, expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Prevote, proposal: None, @@ -524,11 +575,12 @@ 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( - Vote::new_prevote(Round::new(0), Some(value_id), addr3).signed(&sk3), + Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), addr3).signed(&sk3), )), expected_output: Some(Message::ScheduleTimeout(Timeout::prevote(Round::new(0)))), expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Prevote, proposal: None, @@ -540,10 +592,11 @@ fn driver_steps_not_proposer_invalid() { desc: "prevote timeout elapses, we precommit for nil (v2)", input_event: Some(Event::TimeoutElapsed(Timeout::prevote(Round::new(0)))), expected_output: Some(Message::Vote( - Vote::new_precommit(Round::new(0), None, my_addr).signed(&my_sk), + Vote::new_precommit(Height::new(1), Round::new(0), None, my_addr).signed(&my_sk), )), expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Precommit, proposal: None, @@ -562,13 +615,15 @@ fn driver_steps_not_proposer_invalid() { .input_event .unwrap_or_else(|| previous_message.unwrap()); - let output = driver.execute(execute_message); + let output = block_on(driver.execute(execute_message)).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.round, step.expected_round, + "expected round" + ); - let new_state = driver.round_state(driver.round).unwrap(); - assert_eq!(new_state, &step.new_state, "expected state"); + assert_eq!(driver.round_state, step.new_state, "expected state"); previous_message = output.and_then(to_input_msg); } @@ -577,7 +632,9 @@ fn driver_steps_not_proposer_invalid() { #[test] fn driver_steps_not_proposer_timeout_multiple_rounds() { let value = Value::new(9999); - let value_id = value.id(); + + let sel = RotateProposer::default(); + let env = TestEnv::new(move |_, _| Some(value)); let mut rng = StdRng::seed_from_u64(0x42); @@ -596,25 +653,20 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { // Proposer is v1, so we, v3, are not the proposer let (my_sk, my_addr) = (sk3, addr3); + let ctx = TestContext::new(my_sk.clone()); + let vs = ValidatorSet::new(vec![v1.clone(), v2.clone(), v3.clone()]); - let client = TestClient::new(value.clone(), |_| true); - let mut driver = Driver::new( - TestContext, - client, - Height::new(1), - vs, - my_sk.clone(), - my_addr, - ); + let mut driver = Driver::new(ctx, env, sel, vs, my_addr); let steps = vec![ // 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(Round::new(0), false)), + input_event: Some(Event::NewRound(Height::new(1), Round::new(0))), expected_output: Some(Message::ScheduleTimeout(Timeout::propose(Round::new(0)))), expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Propose, proposal: None, @@ -627,11 +679,12 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { desc: "Receive a propose timeout, prevote for nil (v3)", input_event: Some(Event::TimeoutElapsed(Timeout::propose(Round::new(0)))), expected_output: Some(Message::Vote( - Vote::new_prevote(Round::new(0), None, my_addr).signed(&my_sk), + Vote::new_prevote(Height::new(1), Round::new(0), None, my_addr).signed(&my_sk), )), expected_round: Round::new(0), new_state: State { round: Round::new(0), + height: Height::new(1), step: Step::Prevote, proposal: None, locked: None, @@ -645,6 +698,7 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { expected_output: None, expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Prevote, proposal: None, @@ -656,11 +710,13 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { TestStep { desc: "v1 prevotes for its own proposal", input_event: Some(Event::Vote( - Vote::new_prevote(Round::new(0), Some(value_id), addr1).signed(&sk1), + Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), addr1) + .signed(&sk1), )), expected_output: None, expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Prevote, proposal: None, @@ -672,13 +728,14 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { TestStep { desc: "v2 prevotes for nil, we get +2/3 prevotes, precommit for nil", input_event: Some(Event::Vote( - Vote::new_prevote(Round::new(0), None, addr2).signed(&sk2), + Vote::new_prevote(Height::new(1), Round::new(0), None, addr2).signed(&sk2), )), expected_output: Some(Message::Vote( - Vote::new_precommit(Round::new(0), None, my_addr).signed(&my_sk), + Vote::new_precommit(Height::new(1), Round::new(0), None, my_addr).signed(&my_sk), )), expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Precommit, proposal: None, @@ -693,6 +750,7 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { expected_output: None, expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Precommit, proposal: None, @@ -704,11 +762,13 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { TestStep { desc: "v1 precommits its proposal", input_event: Some(Event::Vote( - Vote::new_precommit(Round::new(0), Some(value_id), addr1).signed(&sk1), + Vote::new_precommit(Height::new(1), Round::new(0), Some(value.id()), addr1) + .signed(&sk1), )), expected_output: None, expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Precommit, proposal: None, @@ -720,11 +780,12 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { TestStep { desc: "v2 precommits for nil", input_event: Some(Event::Vote( - Vote::new_precommit(Round::new(0), None, addr2).signed(&sk2), + Vote::new_precommit(Height::new(1), Round::new(0), None, addr2).signed(&sk2), )), expected_output: Some(Message::ScheduleTimeout(Timeout::precommit(Round::new(0)))), expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(0), step: Step::Precommit, proposal: None, @@ -736,9 +797,10 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { 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(Round::new(1))), + expected_output: Some(Message::NewRound(Height::new(1), Round::new(1))), expected_round: Round::new(0), new_state: State { + height: Height::new(1), round: Round::new(1), step: Step::NewRound, proposal: None, @@ -748,10 +810,11 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { }, TestStep { desc: "Start round 1, we are not the proposer", - input_event: Some(Event::NewRound(Round::new(1), false)), + input_event: Some(Event::NewRound(Height::new(1), Round::new(1))), expected_output: Some(Message::ScheduleTimeout(Timeout::propose(Round::new(1)))), expected_round: Round::new(1), new_state: State { + height: Height::new(1), round: Round::new(1), step: Step::Propose, proposal: None, @@ -770,14 +833,145 @@ fn driver_steps_not_proposer_timeout_multiple_rounds() { .input_event .unwrap_or_else(|| previous_message.unwrap()); - let output = driver.execute(execute_message); + let output = block_on(driver.execute(execute_message)).expect("execute succeeded"); assert_eq!(output, step.expected_output, "expected output message"); - assert_eq!(driver.round, step.expected_round, "expected round"); - - let new_state = driver.round_state(driver.round).unwrap(); - assert_eq!(new_state, &step.new_state, "new state"); + assert_eq!(driver.round_state, step.new_state, "new state"); previous_message = output.and_then(to_input_msg); } } + +#[test] +fn driver_steps_no_value_to_propose() { + // No value to propose + let env = TestEnv::new(|_, _| None); + + let mut rng = StdRng::seed_from_u64(0x42); + + let sk1 = PrivateKey::generate(&mut rng); + let sk2 = PrivateKey::generate(&mut rng); + let sk3 = PrivateKey::generate(&mut rng); + + let v1 = Validator::new(sk1.public_key(), 1); + let v2 = Validator::new(sk2.public_key(), 2); + let v3 = Validator::new(sk3.public_key(), 3); + + let (my_sk, my_addr) = (sk1, v1.address); + let ctx = TestContext::new(my_sk.clone()); + + // We are the proposer + let sel = FixedProposer::new(v1.address); + let vs = ValidatorSet::new(vec![v1.clone(), v2.clone(), v3.clone()]); + + let mut driver = Driver::new(ctx, env, sel, vs, my_addr); + + let output = block_on(driver.execute(Event::NewRound(Height::new(1), Round::new(0)))); + assert_eq!(output, Err(Error::NoValueToPropose)); +} + +#[test] +fn driver_steps_proposer_not_found() { + let value = Value::new(9999); + + let env = TestEnv::new(move |_, _| Some(value)); + + let mut rng = StdRng::seed_from_u64(0x42); + + let sk1 = PrivateKey::generate(&mut rng); + let sk2 = PrivateKey::generate(&mut rng); + let sk3 = PrivateKey::generate(&mut rng); + + let addr2 = Address::from_public_key(&sk2.public_key()); + + let v1 = Validator::new(sk1.public_key(), 1); + let v2 = Validator::new(sk2.public_key(), 2); + let v3 = Validator::new(sk3.public_key(), 3); + + let (my_sk, my_addr) = (sk2, addr2); + let ctx = TestContext::new(my_sk.clone()); + + // Proposer is v1, which is not in the validator set + let sel = FixedProposer::new(v1.address); + let vs = ValidatorSet::new(vec![v2.clone(), v3.clone()]); + + let mut driver = Driver::new(ctx, env, sel, vs, my_addr); + + let output = block_on(driver.execute(Event::NewRound(Height::new(1), Round::new(0)))); + assert_eq!(output, Err(Error::ProposerNotFound(v1.address))); +} + +#[test] +fn driver_steps_validator_not_found() { + let value = Value::new(9999); + + let env = TestEnv::new(move |_, _| Some(value)); + + let mut rng = StdRng::seed_from_u64(0x42); + + let sk1 = PrivateKey::generate(&mut rng); + let sk2 = PrivateKey::generate(&mut rng); + let sk3 = PrivateKey::generate(&mut rng); + + let v1 = Validator::new(sk1.public_key(), 1); + let v2 = Validator::new(sk2.public_key(), 2); + let v3 = Validator::new(sk3.public_key(), 3); + + let (my_sk, my_addr) = (sk3.clone(), v3.address); + let ctx = TestContext::new(my_sk.clone()); + + // Proposer is v1 + let sel = FixedProposer::new(v1.address); + // We omit v2 from the validator set + let vs = ValidatorSet::new(vec![v1.clone(), v3.clone()]); + + let mut driver = Driver::new(ctx, env, sel, vs, my_addr); + + // Start new height + block_on(driver.execute(Event::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( + Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), v2.address).signed(&sk2), + ))); + + assert_eq!(output, Err(Error::ValidatorNotFound(v2.address))); +} + +#[test] +fn driver_steps_invalid_signature() { + let value = Value::new(9999); + + let env = TestEnv::new(move |_, _| Some(value)); + + let mut rng = StdRng::seed_from_u64(0x42); + + let sk1 = PrivateKey::generate(&mut rng); + let sk2 = PrivateKey::generate(&mut rng); + let sk3 = PrivateKey::generate(&mut rng); + + let v1 = Validator::new(sk1.public_key(), 1); + let v2 = Validator::new(sk2.public_key(), 2); + let v3 = Validator::new(sk3.public_key(), 3); + + let (my_sk, my_addr) = (sk3.clone(), v3.address); + let ctx = TestContext::new(my_sk.clone()); + + let sel = FixedProposer::new(v1.address); + let vs = ValidatorSet::new(vec![v1.clone(), v2.clone(), v3.clone()]); + + let mut driver = Driver::new(ctx, env, sel, vs, my_addr); + + // Start new round + block_on(driver.execute(Event::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( + Vote::new_prevote(Height::new(1), Round::new(0), Some(value.id()), v2.address).signed(&sk1), + ))); + + assert!(matches!(output, Err(Error::InvalidVoteSignature(_, _)))); +} diff --git a/Code/test/tests/round.rs b/Code/test/tests/round.rs index 9f9b606fc..cd6d2b5b9 100644 --- a/Code/test/tests/round.rs +++ b/Code/test/tests/round.rs @@ -19,7 +19,7 @@ fn test_propose() { ..Default::default() }; - let data = RoundData::new(round, &height, &ADDRESS); + let data = RoundData::new(round, height, &ADDRESS); let transition = apply_event(state.clone(), &data, Event::NewRoundProposer(value)); @@ -36,9 +36,15 @@ fn test_propose() { fn test_prevote() { let value = Value::new(42); let height = Height::new(1); + let round = Round::new(1); - let state: State = State::default().new_round(Round::new(1)); - let data = RoundData::new(Round::new(1), &height, &ADDRESS); + let state: State = State { + height, + round, + ..Default::default() + }; + + let data = RoundData::new(Round::new(1), height, &ADDRESS); let transition = apply_event(state, &data, Event::NewRound); @@ -59,7 +65,7 @@ fn test_prevote() { Event::Proposal(Proposal::new( Height::new(1), Round::new(1), - value.clone(), + value, Round::Nil, )), ); @@ -67,6 +73,6 @@ fn test_prevote() { assert_eq!(transition.next_state.step, Step::Prevote); assert_eq!( transition.message.unwrap(), - Message::prevote(Round::new(1), Some(value.id()), ADDRESS) + Message::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 8dedc2b3c..47d8f4eca 100644 --- a/Code/test/tests/vote_keeper.rs +++ b/Code/test/tests/vote_keeper.rs @@ -1,7 +1,7 @@ use malachite_common::Round; use malachite_vote::keeper::{Message, VoteKeeper}; -use malachite_test::{Address, TestContext, ValueId, Vote}; +use malachite_test::{Address, Height, TestContext, ValueId, Vote}; const ADDRESS1: Address = Address::new([41; 20]); const ADDRESS2: Address = Address::new([42; 20]); @@ -12,15 +12,15 @@ const ADDRESS4: Address = Address::new([44; 20]); fn prevote_apply_nil() { let mut keeper: VoteKeeper = VoteKeeper::new(3); - let vote = Vote::new_prevote(Round::new(0), None, ADDRESS1); + let vote = Vote::new_prevote(Height::new(1), Round::new(0), None, ADDRESS1); let msg = keeper.apply_vote(vote.clone(), 1); assert_eq!(msg, None); - let vote = Vote::new_prevote(Round::new(0), None, ADDRESS2); + let vote = Vote::new_prevote(Height::new(1), Round::new(0), None, ADDRESS2); let msg = keeper.apply_vote(vote.clone(), 1); assert_eq!(msg, None); - let vote = Vote::new_prevote(Round::new(0), None, ADDRESS3); + let vote = Vote::new_prevote(Height::new(1), Round::new(0), None, ADDRESS3); let msg = keeper.apply_vote(vote, 1); assert_eq!(msg, Some(Message::PolkaNil)); } @@ -29,15 +29,15 @@ fn prevote_apply_nil() { fn precommit_apply_nil() { let mut keeper: VoteKeeper = VoteKeeper::new(3); - let vote = Vote::new_precommit(Round::new(0), None, ADDRESS1); + let vote = Vote::new_precommit(Height::new(1), Round::new(0), None, ADDRESS1); let msg = keeper.apply_vote(vote.clone(), 1); assert_eq!(msg, None); - let vote = Vote::new_precommit(Round::new(0), None, ADDRESS2); + let vote = Vote::new_precommit(Height::new(1), Round::new(0), None, ADDRESS2); let msg = keeper.apply_vote(vote.clone(), 1); assert_eq!(msg, None); - let vote = Vote::new_precommit(Round::new(0), None, ADDRESS3); + let vote = Vote::new_precommit(Height::new(1), Round::new(0), None, ADDRESS3); let msg = keeper.apply_vote(vote, 1); assert_eq!(msg, Some(Message::PrecommitAny)); } @@ -49,19 +49,19 @@ fn prevote_apply_single_value() { let v = ValueId::new(1); let val = Some(v); - let vote = Vote::new_prevote(Round::new(0), val, ADDRESS1); + let vote = Vote::new_prevote(Height::new(1), Round::new(0), val, ADDRESS1); let msg = keeper.apply_vote(vote.clone(), 1); assert_eq!(msg, None); - let vote = Vote::new_prevote(Round::new(0), val, ADDRESS2); + let vote = Vote::new_prevote(Height::new(1), Round::new(0), val, ADDRESS2); let msg = keeper.apply_vote(vote.clone(), 1); assert_eq!(msg, None); - let vote_nil = Vote::new_prevote(Round::new(0), None, ADDRESS3); + let vote_nil = Vote::new_prevote(Height::new(1), Round::new(0), None, ADDRESS3); let msg = keeper.apply_vote(vote_nil, 1); assert_eq!(msg, Some(Message::PolkaAny)); - let vote = Vote::new_prevote(Round::new(0), val, ADDRESS4); + let vote = Vote::new_prevote(Height::new(1), Round::new(0), val, ADDRESS4); let msg = keeper.apply_vote(vote, 1); assert_eq!(msg, Some(Message::PolkaValue(v))); } @@ -73,19 +73,19 @@ fn precommit_apply_single_value() { let v = ValueId::new(1); let val = Some(v); - let vote = Vote::new_precommit(Round::new(0), val, ADDRESS1); + let vote = Vote::new_precommit(Height::new(1), Round::new(0), val, ADDRESS1); let msg = keeper.apply_vote(vote.clone(), 1); assert_eq!(msg, None); - let vote = Vote::new_precommit(Round::new(0), val, ADDRESS2); + let vote = Vote::new_precommit(Height::new(1), Round::new(0), val, ADDRESS2); let msg = keeper.apply_vote(vote.clone(), 1); assert_eq!(msg, None); - let vote_nil = Vote::new_precommit(Round::new(0), None, ADDRESS3); + let vote_nil = Vote::new_precommit(Height::new(1), Round::new(0), None, ADDRESS3); let msg = keeper.apply_vote(vote_nil, 1); assert_eq!(msg, Some(Message::PrecommitAny)); - let vote = Vote::new_precommit(Round::new(0), val, ADDRESS4); + let vote = Vote::new_precommit(Height::new(1), Round::new(0), val, ADDRESS4); let msg = keeper.apply_vote(vote, 1); assert_eq!(msg, Some(Message::PrecommitValue(v))); } diff --git a/Code/vote/src/lib.rs b/Code/vote/src/lib.rs index cc27fe823..d474eae37 100644 --- a/Code/vote/src/lib.rs +++ b/Code/vote/src/lib.rs @@ -1,5 +1,6 @@ //! Tally votes of the same type (eg. prevote or precommit) +#![no_std] #![forbid(unsafe_code)] #![deny(unused_crate_dependencies, trivial_casts, trivial_numeric_casts)] #![warn( @@ -9,6 +10,7 @@ variant_size_differences )] #![cfg_attr(not(test), deny(clippy::unwrap_used, clippy::panic))] +#![cfg_attr(coverage_nightly, feature(coverage_attribute))] extern crate alloc; diff --git a/Scripts/quint-forall.sh b/Scripts/quint-forall.sh new file mode 100644 index 000000000..dc0fb1bd7 --- /dev/null +++ b/Scripts/quint-forall.sh @@ -0,0 +1,48 @@ +#!/bin/env bash + +BLUE=$(tput setaf 4) +RED=$(tput setaf 1) +RESET=$(tput sgr0) +UNDERLINE=$(tput smul) + +# [INFO] message in blue +info() +{ + echo "${BLUE}[INFO] $*${RESET}" +} + +# [ERROR] message in red +error() +{ + echo "${RED}[ERROR] $*${RESET} " +} + +# Run `quint $command` on all given files. + +cmd="$1" +files=("${@:2}") + +if [[ "${#files[@]}" -eq 0 ]]; then + echo "${UNDERLINE}Usage:${RESET} $0 [ ...]" + exit 1 +fi + +failed=0 +failed_files=() + +for file in "${files[@]}"; do + info "Running: quint $cmd ${UNDERLINE}$file" + if ! npx @informalsystems/quint "$cmd" "$file"; then + failed_files+=("$file") + failed=$((failed + 1)) + fi + echo "" +done + +if [[ "$failed" -gt 0 ]]; then + error "Failed on $failed files:" + for file in "${failed_files[@]}"; do + error " - ${UNDERLINE}$file" + done + exit 1 +fi diff --git a/Specs/Quint/asyncModelsTest.qnt b/Specs/Quint/asyncModelsTest.qnt new file mode 100644 index 000000000..5b22b976f --- /dev/null +++ b/Specs/Quint/asyncModelsTest.qnt @@ -0,0 +1,158 @@ +// -*- mode: Bluespec; -*- + +module asyncModelsTest { + +import statemachineAsync( + validators = Set("v1", "v2", "v3", "v4"), + validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), + Faulty = Set(), + Values = Set("a", "b"), + Rounds = Set(0, 1, 2, 3), + Heights = Set(0) // , 1, 2, 3) +) as N4F0 from "./statemachineAsync" + +run NewRoundTest = { + N4F0::init + .then(N4F0::setNextValueToPropose("v2", "block")) + .then(N4F0::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + .then(N4F0::valStep("v4")) + .then(N4F0::valStep("v1")) + .then(N4F0::deliverProposal("v2", { height: 0, proposal: "block", round: 0, src: "v2", validRound: -1 })) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v1", step: "Prevote" })) + .then(N4F0::deliverVote("v1", { height: 0, id: "block", round: 0, src: "v2", step: "Prevote" })) + .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v3", step: "Prevote" })) + .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v1", step: "Prevote" })) + .then(N4F0::deliverVote("v2", { height: 0, id: "block", round: 0, src: "v2", step: "Prevote" })) + .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v3", step: "Prevote" })) + .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v1", step: "Prevote" })) + .then(N4F0::deliverVote("v3", { height: 0, id: "block", round: 0, src: "v2", step: "Prevote" })) + .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v3", step: "Prevote" })) + .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::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + // timeoutPrevote started + .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: "nil", round: 0, src: "v1", step: "Precommit" })) + .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v2", step: "Precommit" })) + .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v3", step: "Precommit" })) + .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v1", step: "Precommit" })) + .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v2", step: "Precommit" })) + .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v3", step: "Precommit" })) + .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v1", step: "Precommit" })) + .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v2", step: "Precommit" })) + .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v3", step: "Precommit" })) + .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::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + .then(N4F0::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + // .then(N4F0::deliverProposal("v1", { height: 0, proposal: "block", round: 1, src: "v2", validRound: -1 })) +/* .then(N4F0::deliverProposal("v1", { height: 0, proposal: "block", round: 0, src: "v2", validRound: -1 })) + .then(N4F0::deliverProposal("v2", { height: 0, proposal: "block", round: 0, src: "v2", validRound: -1 })) + .then(N4F0::deliverProposal("v3", { height: 0, proposal: "block", round: 0, src: "v2", validRound: -1 })) + .then(N4F0::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + + */ +} + +import statemachineAsync( + validators = Set("v1", "v2", "v3", "v4"), + validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), + Faulty = Set("v1"), + Values = Set("a", "b"), + Rounds = Set(0, 1, 2, 3), + Heights = Set(0) // , 1, 2, 3) +) as N4F1 from "./statemachineAsync" + +// quint run --init=N4F1::init --step=N4F1::step --invariant=N4F1::AgreementInv AsyncModels.qnt +// quint run --init=N4F1::init --step=N4F1::step --invariant=N4F1::ConsensusOutputInv AsyncModels.qnt + +import statemachineAsync( + validators = Set("v1", "v2", "v3", "v4"), + validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), + Faulty = Set("v1", "v2"), + Values = Set("a", "b"), + Rounds = Set(0), // , 1, 2, 3) + Heights = Set(0) // , 1, 2, 3) +) as N4F2 from "./statemachineAsync" + +// v3 and v4 are correct. v2 is a N4N4F22aulty proposal and proposes diN4N4F22N4N4F22erently to v3 and v4 +// this run leads to disagreement +run DisagreementTest = { + N4F2::init + .then(N4F2::valStep("v3")) + .then(N4F2::valStep("v4")) + .then(N4F2::deliverProposal("v3", { height: 0, proposal: "b", round: 0, src: "v2", validRound: -1 })) + .then(N4F2::deliverProposal("v4", { height: 0, proposal: "a", round: 0, src: "v2", validRound: -1 })) + .then(N4F2::valStep("v3")) + .then(N4F2::valStep("v4")) + .then(all{ + // they voted diN4F2N4F2erently + 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" }), + "v4" -> Set({ height: 0, id: "a", round: 0, src: "v4", step: "Prevote" }, + { height: 0, id: "b", round: 0, src: "v3", step: "Prevote" }))), + N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v1", step: "Prevote" }) + }) + .then(N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v2", step: "Prevote" })) + .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v1", step: "Prevote" })) + .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v2", step: "Prevote" })) + .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v3", step: "Prevote" })) + .then(N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v4", step: "Prevote" })) + .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(all{ + // they precommited diN4F2N4F2erently + assert( N4F2::voteBuffer.get("v3").contains({ height: 0, id: "a", round: 0, src: "v4", step: "Precommit" }) and + N4F2::voteBuffer.get("v4").contains({ height: 0, id: "b", round: 0, src: "v3", step: "Precommit" })), + N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v1", step: "Precommit" }) }) + .then(N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v2", step: "Precommit" })) + .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v1", step: "Precommit" })) + .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v2", step: "Precommit" })) + .then(N4F2::valStep("v3")) + .then(N4F2::valStep("v3")) + .then(N4F2::valStep("v4")) + .then(N4F2::valStep("v4")) + .then(all{ + assert(N4F2::AgreementInv), + N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v4", step: "Precommit" }) }) + .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v3", step: "Precommit" })) + .then(N4F2::valStep("v3")) + .then(N4F2::valStep("v4")) + .then(all{ + assert(not(N4F2::AgreementInv)), + N4F2::unchangedAll}) +} + + + +} \ No newline at end of file diff --git a/Specs/Quint/consensus.qnt b/Specs/Quint/consensus.qnt index cf2d43b4c..3991b091b 100644 --- a/Specs/Quint/consensus.qnt +++ b/Specs/Quint/consensus.qnt @@ -1,7 +1,23 @@ // -*- mode: Bluespec; -*- -module consensus { +/* +TODO: check +- whether we have "step" checks in place everywhere +- "the first time": checks here or in executor +- check against arXiv +- tests +- types (e.g., heights in the messages) +- discuss "decision tree" in executor +- Should we think again about the components and the boundaries (especially between + voteBookkeeper and executor) +- Do we need tests for executor 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 +*/ + +module consensus { + // a process address is just a string type Address_t = str // a value is also a string @@ -15,36 +31,47 @@ module consensus { // timeours are identified by strings type Timeout_t = str - // the type of propose messages - type ProposeMsg_t = { +// the type of propose messages +type ProposeMsg_t = { src: Address_t, height: Height_t, round: Round_t, - proposal: Value_t, + proposal: Value_t, // an actual value. All other values are id(proposal) validRound: Round_t - } +} - // the type of Prevote and Precommit messages - type VoteMsg_t = { +// the type of Prevote and Precommit messages +type VoteMsg_t = { src: Address_t, height: Height_t, round: Round_t, - step: Step_t, // "prevote" or "precommit" + step: Step_t, // "Prevote" or "Precommit" id: Value_t, - } +} type ConsensusState = { p: Address_t, height : Height_t, round: Round_t, - step: Step_t, // "newRound", propose, prevote, precommit, decided + step: Step_t, // "newRound", propose, Prevote, Precommit, decided lockedRound: Round_t, - lockedValue: Value_t, + lockedValue: Value_t, // id("of a value") validRound: Round_t, - validValue: Value_t, + validValue: Value_t, // id("of a value") //continue } +pure def initConsensusState (v: Address_t) : ConsensusState = { + p: v, + round: -1, + step: "newRound", + height : 0, + lockedRound: -1, + lockedValue: "nil", + validRound: -1, + validValue: "nil" +} + type Event = { name : str, height : Height_t, @@ -54,7 +81,7 @@ type Event = { } // what is a good way to encode optionals? I do with default values -type Result = { +type ConsensusOutput = { name : str, proposal: ProposeMsg_t, voteMessage: VoteMsg_t, @@ -63,10 +90,26 @@ type Result = { skipRound: Round_t } -val consensusEvents = Set( +val consensusOutputs = Set ( + "proposal", + "votemessage", + "timeout", + "decided", + "skipRound" +) + +type ConsResult = { + cs: ConsensusState, + out: ConsensusOutput, +// pending: Set[ConsensusOutput], // TODO: not sure we need this +} + +type ConsensusEvent = str + +val ConsensusEvents = Set( "NewHeight", // Setups the state-machine for a single-height execution "NewRound", // Start a new round, not as proposer. - "NewRoundProposer(Value)", // Start a new round as proposer with the proposed Value. + "NewRoundProposer", // Start a new round as proposer with the proposed Value. "Proposal", // Receive a proposal without associated valid round. "ProposalAndPolkaPreviousAndValid", // Receive a valid proposal with an associated valid round, attested by a a Polka(vr). "ProposalInvalid", // Receive an invalid proposal: L26 and L32 when valid(v) == false @@ -78,22 +121,22 @@ val consensusEvents = Set( "RoundSkip", // Receive +1/3 messages from different validators for a higher round. "TimeoutPropose", // Timeout waiting for proposal. "TimeoutPrevote", // Timeout waiting for prevotes for a value. - "TimeoutPrecommit" // Timeout waiting for precommits for a value. + "TimeoutPrecommit", // Timeout waiting for precommits for a value. +// found after Montebello + "ProposalAndPolkaAndInValid" // TODO: Discuss what to do about it ) /* - - "PolkaValue(ValueId)", // Receive +2/3 prevotes for Value. - "PrecommitValue(ValueId)", // Receive +2/3 precommits for Value. - -) */ + "PolkaValue(ValueId)", // Receive +2/3 Prevotes for Value. + "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 noTimeout : Timeout_t = "" val noDecided = "" val noSkipRound : Round_t = -1 -val defaultResult : Result = { +val defaultResult : ConsensusOutput = { name: "", proposal: noProp, voteMessage: noVote, @@ -102,224 +145,249 @@ val defaultResult : Result = { skipRound: noSkipRound} -// Implies StartRound(0) -pure def NewHeight (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - val newstate = { ...state, - round: 0, + +pure def NewHeight (state: ConsensusState, ev: Event) : ConsResult = { + if (ev.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, lockedRound: -1, lockedValue: "nil", validRound: -1, validValue: "nil" - } - (newstate, defaultResult) + } + {cs: newstate, out: defaultResult } + else + {cs: state, out: defaultResult } } // line 11.14 -pure def NewRoundProposer (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - // TODO: ev.round must match state.round - val newstate = { ...state, round: ev.round, step: "propose"} - val proposal = if (state.validValue != "nil") state.validValue - else ev.value - val result = { ...defaultResult, name: "proposal", - proposal: { src: state.p, - height: state.height, - round: ev.round, - proposal: proposal, - validRound: state.validRound}} - (newstate, result) +pure def NewRoundProposer (state: ConsensusState, ev: Event) : ConsResult = { + if (ev.round > state.round) + val newstate = { ...state, round: ev.round, step: "propose"} + val proposal = if (state.validValue != "nil") state.validValue + else ev.value + val result = { ...defaultResult, name: "proposal", + proposal: { src: state.p, + height: state.height, + round: ev.round, + proposal: proposal, + validRound: state.validRound}} + {cs: newstate, out: result } + else + {cs: state, out: defaultResult } } // line 11.20 -pure def NewRound (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - // TODO: ev.round must match state.round - val newstate = { ...state, round: ev.round, step: "propose" } - val result = { ...defaultResult, name: "timeout", timeout: "timeoutPropose"} // do we need the roundnumber here? YES - (newstate, result) +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 + // of figuring out whether it needs to record the round number and height per + // timeout + {cs: newstate, out: result} + else + {cs: state, out: defaultResult } } // line 22 -pure def Proposal (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - if (state.step == "propose") { - val newstate = state.with("step", "prevote") +// 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 = { + if (state.step == "propose") + val newstate = { ...state, step: "Prevote" } if (state.lockedRound == -1 or state.lockedValue == ev.value) val result = { ...defaultResult, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, - step: "prevote", + step: "Prevote", id: ev.value}} - (newstate, result) + {cs: newstate, out: result} else val result = { ...defaultResult, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, - step: "prevote", + step: "Prevote", id: "nil"}} - (newstate, result) - } + {cs: newstate, out: result} + else + {cs: state, out: defaultResult} + // This should be dead code as the executor checks the step +} + +// line 26 +pure def ProposalInvalid (state: ConsensusState, ev: Event) : ConsResult = { + if (state.step == "propose") + val newstate = state.with("step", "Prevote") + val result = { ...defaultResult, name: "votemessage", + voteMessage: { src: state.p, + height: state.height, + round: state.round, + step: "Prevote", + id: "nil"}} + {cs: newstate, out: result} else - (state, defaultResult) + {cs: state, out: defaultResult} } // line 28 -pure def ProposalAndPolkaPreviousAndValid (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - if (state.step == "propose" and ev.vr >= 0 and ev.vr < state.round) { - val newstate = state.with("step", "prevote") +pure def ProposalAndPolkaPreviousAndValid (state: ConsensusState, ev: Event) : ConsResult = { + if (state.step == "propose" and ev.vr >= 0 and ev.vr < state.round) + val newstate = state.with("step", "Prevote") if (state.lockedRound <= ev.vr or state.lockedValue == ev.value) val result = { ...defaultResult, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, - step: "prevote", + step: "Prevote", id: ev.value}} - (newstate, result) + {cs: newstate, out: result} else val result = { ...defaultResult, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, - step: "prevote", + step: "Prevote", id: "nil"}} - (newstate, result) - } + {cs: newstate, out: result} else - (state, defaultResult) -} - -// Lines 22 or 28 with valid(v) == false -pure def ProposalInvalid (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - if (state.step == "propose") { - val newstate = state.with("step", "prevote") - val result = { ...defaultResult, name: "votemessage", - voteMessage: { src: state.p, - height: state.height, - round: state.round, - step: "prevote", - id: "nil"}} - (newstate, result) - } - else { - (state, defaultResult ) - } + {cs: state, out: defaultResult} + // TODO: should we add the event to pending in this case. We would need to + // do this in the executor } // line 34 -pure def PolkaAny (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - if (state.step == "prevote") { - val result = { ...defaultResult, name: "timeout", timeout: "timeoutPrevote" } // do we need the roundnumber here? YES - (state, result) - } +pure def PolkaAny (state: ConsensusState, ev: Event) : 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 + // of figuring out whether it needs to record the round number and height per + // timeout + {cs: state, out: result} else - (state, defaultResult) + {cs: state, out: defaultResult} } // line 36 -pure def ProposalAndPolkaAndValid (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { +pure def ProposalAndPolkaAndValid (state: ConsensusState, ev: Event) : ConsResult = { val auxState = { ...state, validValue: ev.value, validRound: state.round } - if (state.step == "prevote") { + if (state.step == "Prevote") val newstate = { ...auxState, lockedValue: ev.value, lockedRound: state.round, - step: "precommit" } + step: "Precommit" } val result = { ...defaultResult, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, - step: "precommit", + step: "Precommit", id: ev.value}} - (newstate, result) - } - else { - // TODO: if state > prevote, we should update the valid round! - (state, defaultResult) - } + {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} + else + {cs: state, out: defaultResult} + // TODO: should we add the event to pending in this case. We would need to + // do this in the executor } // line 44 -pure def PolkaNil (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - if (state.step == "prevote") - val newstate = { ...state, step: "precommit"} +pure def PolkaNil (state: ConsensusState, ev: Event) : ConsResult = { + if (state.step == "Prevote") + val newstate = { ...state, step: "Precommit"} val result = { ...defaultResult, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, - step: "precommit", + step: "Precommit", id: "nil"}} - (newstate, result) + {cs: newstate, out: result} else - (state, defaultResult) + {cs: state, out: defaultResult} } // line 47 -pure def PrecommitAny (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - if (state.step == "precommit") { - val result = { ...defaultResult, name: "timeout", timeout: "timeoutPrecommit" } // do we need the roundnumber here? YES - (state, result) - } - else - (state, defaultResult) +pure def PrecommitAny (state: ConsensusState, ev: Event) : ConsResult = { + val result = { ...defaultResult, name: "timeout", timeout: "TimeoutPrecommit" } + {cs: state, out: result} } // line 49 -pure def ProposalAndCommitAndValid (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { +pure def ProposalAndCommitAndValid (state: ConsensusState, ev: Event) : ConsResult = { if (state.step != "decided") { val newstate = { ...state, step: "decided"} val result = { ...defaultResult, name: "decided", decided: ev.value} - (newstate, result) + {cs: newstate, out: result} } else - (state, defaultResult) -} + {cs: state, out: defaultResult} +} // line 55 -pure def RoundSkip (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { +pure def RoundSkip (state: ConsensusState, ev: Event) : ConsResult = { if (ev.round > state.round) val result = { ...defaultResult, name: "skipRound", skipRound: ev.round } - (state, result) + {cs: state, out: result} else - (state, defaultResult) + {cs: state, out: defaultResult} } -pure def TimeoutPropose (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { +pure def TimeoutPropose (state: ConsensusState, ev: Event) : ConsResult = { if (ev.height == state.height and ev.round == state.round and state.step == "propose") - val newstate = { ...state, step: "prevote"} + val newstate = { ...state, step: "Prevote"} val result = { ...defaultResult, name: "votemessage", voteMessage: { src: state.p, - height: state.height, - round: state.round, - step: "prevote", - id: "nil"}} - (newstate, result) + height: state.height, + round: state.round, + step: "Prevote", + id: "nil"}} + {cs: newstate, out: result} else - (state, defaultResult) + {cs: state, out: defaultResult} } -pure def TimeoutPrevote (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - if (ev.height == state.height and ev.round == state.round and state.step == "prevote") - val newstate = { ...state, step: "precommit"} +pure def TimeoutPrevote (state: ConsensusState, ev: Event) : ConsResult = { + if (ev.height == state.height and ev.round == state.round and state.step == "Prevote") + val newstate = { ...state, step: "Precommit"} + // TODO: should we send precommit nil again ? val result = { ...defaultResult, name: "votemessage", voteMessage: { src: state.p, - height: state.height, - round: state.round, - step: "precommit", - id: "nil"}} - (newstate, result) + height: state.height, + round: state.round, + step: "Precommit", + id: "nil"}} + {cs: newstate, out: result} else - (state, defaultResult) + {cs: state, out: defaultResult} } -pure def TimeoutPrecommit (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { +pure def TimeoutPrecommit (state: ConsensusState, ev: Event) : ConsResult = { if (ev.height == state.height and ev.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} - (state, result) + {cs: state, out: result} else - (state, defaultResult) + {cs: state, out: defaultResult} } -pure def consensus (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { +/* ********************************************************* + * Main entry point + * ********************************************************/ + +pure def consensus (state: ConsensusState, ev: Event) : ConsResult = { if (ev.name == "NewHeight") NewHeight (state, ev) else if (ev.name == "NewRoundProposer") @@ -349,167 +417,8 @@ pure def consensus (state: ConsensusState, ev: Event) : (ConsensusState, Result) else if (ev.name == "TimeoutPrecommit") TimeoutPrecommit (state, ev) else - (state, defaultResult) -} - -/* **************************************************************************** - * Global state - * ************************************************************************* */ - -var system : Address_t -> ConsensusState - -// Auxiliary fields for better debugging -var _Result : Result -var _Event : Event - - -pure def initialProcess (name: Address_t) : ConsensusState = { - { p: name, height : 1, round: 0, step: "newRound", lockedRound: -1, lockedValue: "nil", validRound: -1, validValue: "nil"} -} - -action init = all { - system' = Map ("Josef" -> initialProcess("Josef")), - _Result' = defaultResult, - _Event' = {name : "Initial", - height : -1, - round: -1, - value: "", - vr: -1} -} - - - -// 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 { - val event = {name : eventName, - height : h, - round: r, - value: value, - vr: vr} - val res = consensus(system.get(proc), event ) - all { - system' = system.put(proc, res._1), - _Result' = res._2, - _Event' = event - } -} - -action step = any { - nondet name = oneOf(consensusEvents) - 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) -} - -action unchangedAll = all { - system' = system, - _Result' = _Result, - _Event' = _Event, + {cs: state, out: defaultResult} } - -// This test should call each event at least once -run DecideNonProposerTest = { - init - .then(FireEvent("NewRound", "Josef", 1, 0, "", -1)) - .then(all{ - assert(_Result.timeout == "timeoutPropose"), - unchangedAll - }) - .then(FireEvent("Proposal", "Josef", 1, 0, "block", -1)) - .then(all{ - assert(_Result.voteMessage.step == "prevote" and _Result.voteMessage.id == "block"), - unchangedAll - }) - .then(FireEvent("ProposalAndPolkaAndValid", "Josef", 1, 0, "block", -1)) - .then(all{ - assert(_Result.voteMessage.step == "precommit" and _Result.voteMessage.id == "block"), - unchangedAll - }) - .then(FireEvent("ProposalAndCommitAndValid", "Josef", 1, 0, "block", -1)) - .then(all{ - assert(_Result.decided == "block"), - unchangedAll - }) - .then(FireEvent("NewHeight", "Josef", system.get("Josef").height + 1, 0, "", -1)) - .then(all{ - assert(system.get("Josef").height == 2), - unchangedAll - }) - .then(FireEvent("NewRoundProposer", "Josef", 2, 0, "nextBlock", -1)) - .then(all{ - // TODO: should we prevent timeout in this case? See issue #21 - assert(_Result.timeout != "timeoutPropose" and _Result.proposal.proposal == "nextBlock"), - unchangedAll - }) - .then(FireEvent("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"), - unchangedAll - }) - .then(FireEvent("PolkaAny", "Josef", 2, 0, "nextBlock", -1)) - .then(all{ - assert(_Result.timeout == "timeoutPrevote"), - unchangedAll - }) - .then(FireEvent("TimeoutPrevote", "Josef", 2, 0, "nextBlock", -1)) // FIXME: why a value for the timeout? - .then(all{ - assert(_Result.voteMessage.step == "precommit" and _Result.voteMessage.id == "nil" and - system.get("Josef").step == "precommit"), - unchangedAll - }) - .then(FireEvent("PrecommitAny", "Josef", 2, 0, "nextBlock", -1)) - .then(all{ - assert(_Result.timeout == "timeoutPrecommit"), - unchangedAll - }) - .then(FireEvent("TimeoutPrecommit", "Josef", 2, 0, "nextBlock", -1)) - .then(all{ - assert(_Result.skipRound == 1), - unchangedAll - }) - .then(FireEvent("NewRound", "Josef", 2, 1, "", -1)) - .then(all{ - assert(_Result.timeout == "timeoutPropose"), - unchangedAll - }) - .then(FireEvent("TimeoutPropose", "Josef", 2, 1, "nextBlock", -1)) - .then(all{ - assert(_Result.voteMessage.step == "prevote" and _Result.voteMessage.id == "nil" and - system.get("Josef").step == "prevote"), - unchangedAll - }) - .then(FireEvent("PolkaNil", "Josef", 2, 1, "nextBlock", -1)) - .then(all{ - assert(_Result.voteMessage.step == "precommit" and _Result.voteMessage.id == "nil" and - system.get("Josef").step == "precommit"), - unchangedAll - }) - .then(FireEvent("PrecommitAny", "Josef", 2, 1, "nextBlock", -1)) - .then(all{ - assert(_Result.timeout == "timeoutPrecommit"), - unchangedAll - }) - .then(FireEvent("TimeoutPrecommit", "Josef", 2, 1, "nextBlock", -1)) - .then(all{ - assert(_Result.skipRound == 2), - unchangedAll - }) - .then(FireEvent("NewRound", "Josef", 2, 2, "", -1)) - .then(all{ - assert(_Result.timeout == "timeoutPropose"), - unchangedAll - }) - .then(FireEvent("ProposalInvalid", "Josef", 2, 2, "", -1)) - .then(all{ - assert(_Result.voteMessage.step == "prevote" and _Result.voteMessage.id == "nil" and - system.get("Josef").step == "prevote"), - unchangedAll - }) -} - - } diff --git a/Specs/Quint/consensusTest.qnt b/Specs/Quint/consensusTest.qnt new file mode 100644 index 000000000..fb7a2df24 --- /dev/null +++ b/Specs/Quint/consensusTest.qnt @@ -0,0 +1,129 @@ +// -*- mode: Bluespec; -*- + +module consensusTest { + +import consensus.* from "./consensus" + +/* **************************************************************************** + * Global state + * ************************************************************************* */ + +var system : Address_t -> ConsensusState +var _Result : ConsensusOutput +var _Event : Event + + +pure def initialProcess (name: Address_t) : ConsensusState = { + { p: name, height : 1, round: -1, step: "newRound", lockedRound: -1, lockedValue: "nil", validRound: -1, validValue: "nil"} +} + +action init = all { + system' = Map ("Josef" -> initialProcess("Josef")), + _Result' = defaultResult, + _Event' = { name : "Initial", + height : 0, + round: -1, + value: "", + vr: -1} +} + + + +// 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 { + val event = { name : eventName, + height : h, + round: r, + value: value, + vr: vr} + val res = consensus(system.get(proc), event ) + all { + system' = system.put(proc, res.cs), + _Result' = res.out, + _Event' = event + } +} + +action step = any { + nondet name = oneOf(ConsensusEvents) + 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) +} + +action unchangedAll = all { + system' = system, + _Result' = _Result, + _Event' = _Event, +} + +// This test should call each event at least once +run DecideNonProposerTest = { + init + .then(FireEvent("NewRound", "Josef", 1, 0, "", -1)) + .then(all{ + assert(_Result.timeout == "TimeoutPropose"), + FireEvent("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)}) + .then(all{ + assert(_Result.voteMessage.step == "Precommit" and _Result.voteMessage.id == "block"), + FireEvent("ProposalAndCommitAndValid", "Josef", 1, 0, "block", -1)}) + .then(all{ + assert(_Result.decided == "block"), + FireEvent("NewHeight", "Josef", system.get("Josef").height + 1, 0, "", -1)}) + .then(all{ + assert(system.get("Josef").height == 2), + FireEvent("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 + .then(all{ + assert(_Result.voteMessage.step == "Prevote" and system.get("Josef").step == "Prevote"), + FireEvent("PolkaAny", "Josef", 2, 0, "nextBlock", -1)}) + .then(all{ + assert(_Result.timeout == "TimeoutPrevote"), + FireEvent("TimeoutPrevote", "Josef", 2, 0, "nextBlock", -1)}) + .then(all{ + assert(_Result.voteMessage.step == "Precommit" and _Result.voteMessage.id == "nil" and + system.get("Josef").step == "Precommit"), + FireEvent("PrecommitAny", "Josef", 2, 0, "nextBlock", -1)}) + .then(all{ + assert(_Result.timeout == "TimeoutPrecommit"), + FireEvent("TimeoutPrecommit", "Josef", 2, 0, "nextBlock", -1)}) + .then(all{ + assert(_Result.skipRound == 1), + FireEvent("NewRound", "Josef", 2, 1, "", -1)}) + .then(all{ + assert(_Result.timeout == "TimeoutPropose"), + FireEvent("TimeoutPropose", "Josef", 2, 1, "nextBlock", -1)}) + .then(all{ + assert(_Result.voteMessage.step == "Prevote" and _Result.voteMessage.id == "nil" and + system.get("Josef").step == "Prevote"), + FireEvent("PolkaNil", "Josef", 2, 1, "nextBlock", -1)}) + .then(all{ + assert(_Result.voteMessage.step == "Precommit" and _Result.voteMessage.id == "nil" and + system.get("Josef").step == "Precommit"), + FireEvent("PrecommitAny", "Josef", 2, 1, "nextBlock", -1)}) + .then(all{ + assert(_Result.timeout == "TimeoutPrecommit"), + FireEvent("TimeoutPrecommit", "Josef", 2, 1, "nextBlock", -1)}) + .then(all{ + assert(_Result.skipRound == 2), + FireEvent("NewRound", "Josef", 2, 2, "", -1)}) + .then(all{ + assert(_Result.timeout == "TimeoutPropose"), + FireEvent("ProposalInvalid", "Josef", 2, 2, "", -1)}) + .then(all{ + assert(_Result.voteMessage.step == "Prevote" and _Result.voteMessage.id == "nil" and + system.get("Josef").step == "Prevote"), + unchangedAll + }) +} + + +} + diff --git a/Specs/Quint/executor.qnt b/Specs/Quint/executor.qnt new file mode 100644 index 000000000..da46db545 --- /dev/null +++ b/Specs/Quint/executor.qnt @@ -0,0 +1,594 @@ +// -*- 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 +*/ + +module executor { + +import consensus.* from "./consensus" +import voteBookkeeper.* from "./voteBookkeeper" + +pure def initBookKeeper (currentRound: Round, totalVotingPower: int): Bookkeeper = + { height: 0, currentRound: currentRound, totalWeight: totalVotingPower, rounds: Map() } + + +type ExecutorState = { + bk : Bookkeeper, + cs : ConsensusState, + proposals: Set[ProposeMsg_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)], + started: bool, + applyvotesResult: ExecutorEvent, //debug TODO + chain : List[Value_t], + nextValueToPropose: Value_t, +} + +pure def initExecutor (v: Address_t, vs: Address_t -> int) : ExecutorState = { + val tvp = vs.keys().fold(0, (sum, key) => sum + vs.get(key)) + { + bk: initBookKeeper(0, tvp), + cs: initConsensusState(v), + proposals: Set(), + valset: vs, + executedEvents: List(), + pendingEvents: Set(), + started: false, + applyvotesResult: toEvent(0, "", {name: "", value: ""}), // debug + chain : List(), + nextValueToPropose: "", + } +} + +type NodeState = { + es: ExecutorState, + timeout: Set[(Timeout_t, Height_t, Round_t)], + incomingVotes: Set[VoteMsg_t], + incomingProposals: Set[ProposeMsg_t], +} + +pure def initNode (v: Address_t, vs: Address_t -> int) : NodeState = { + es: initExecutor(v,vs), + timeout: Set(), + incomingVotes: Set(), + incomingProposals: Set(), +} + +type ExecutorInput = { + name: str, // TODO: make a set of values. + proposal: ProposeMsg_t, + vote: VoteMsg_t, + timeout: str, + event: Event, + nextValueToPropose: Value_t +} + +val defaultInput: ExecutorInput = { + name: "", + proposal: { src: "", height: 0, round: 0, proposal: "", validRound: 0 }, + vote: { src: "", height: 0, round: 0, step: "", id: "", }, + timeout: "", + event: defaultEvent, + 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 = + { typ: v.step, round: v.round, value: v.id, address: v.src } + +val defaultEvent : Event = { name : "", height : 0, round: 0, value: "", vr: 0 } + +/* +encode the following decision tree + +proposal + invalid -> consensus event + valid: BK list of events + generate all Consensus events C + feed all events to Consensus + +Precommit + BK applyVote + (see whether we can make (A) 2f+1 Any for current or + (B) 2f+1 plus proposal for current) + -> feed all events to Consensus + +Prevote + BK applyVote + For current round PolkaVal -> PolkaAny and PolkaNil -> PolkaAny: list of Events + check proposal: list of Consensus evens (considering line 28) + -> feed all events to Consensus +*/ + +val emptyProposal : ProposeMsg_t= + { src: "none", height: 0, round: 0, proposal: "none", validRound: 0 } + +val emptyVote = + { src: "none", height: 0, round: 0, step: "None", id: "None" } + +// +// Interface to app and/or mempool (Proposer, getValue, valid) +// + +// In the implementation this could be a callback to the application. But it needs to be +// a function, that is, any two validators need to agree on this +pure def Proposer(valset: Address_t -> int, height: Height_t, round: Round_t) : Address_t = { + // Here: rotating coordinator. We can do something more clever actually using the valset + val prop = (round + 1) % 4 + if (prop == 0) "v1" + else if (prop == 1) "v2" + else if (prop == 2) "v3" + else "v4" +} + +pure def getValue(es: ExecutorState) : Value_t = es.nextValueToPropose + +pure def valid(p: ProposeMsg_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 + p.proposal != "invalid" +} + +// efficient hashing function +pure def id(v) = v + + +type ConsensusCall = { + es: ExecutorState, + event: Event, + out: ConsensusOutput +} + +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) = { + // 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) + else + // Go to consensus + val res = consensus(es.cs, ev) + // Update the round in the vote keeper, in case we moved to a new round + val newBk = { ...bk, currentRound: res.cs.round } + // Record that we executed the event + val events = es.executedEvents.append((ev, res.cs.height, res.cs.round)) + + ({ ...es, bk: newBk, cs: res.cs, executedEvents: events }, 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))) { + callConsensus(es, es.bk, { name : "ProposalAndCommitAndValid", + height : input.vote.height, + round: input.vote.round, + value: input.vote.id, + vr: -1}) + } + else { + if (eev.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) { + // 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", + height: input.vote.height, + round: input.vote.round, + value: input.vote.id, + vr: -1}) + } + else { + // messages from past round -> ignore + (es, defaultResult) + } + } + else if (eev.name == "PrecommitAny" and eev.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 + // none of the supported Precommit events. Do nothing + // TODO: catch skip round event + (es, defaultResult) +} + + +// We do this if the executor receives a Prevote +pure def Prevote (es: ExecutorState, input: ExecutorInput, eev: ExecutorEvent) : (ExecutorState, ConsensusOutput) = { + // TODO: events do not have heights now. + // TODO: Polka implications missing. + if (eev.name == "PolkaValue") + if (eev.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)) + callConsensus(es, es.bk, { name: "ProposalAndPolkaPreviousAndValid", + height: es.cs.height, + round: es.cs.round, + value: eev.value, + vr: eev.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", + height: es.cs.height, + round: es.cs.round, + value: eev.value, + vr: eev.round}) + else + // we don't have a matching proposal so we do nothing + // 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) + // 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}) + 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) + callConsensus(es, es.bk, { name: "PolkaNil", + height: es.cs.height, + round: es.cs.round, + value: eev.value, + vr: eev.round}) + else + // TODO: catch skip round event + (es, defaultResult) +} + + +// We do this if a timeout expires at the executor +pure def Timeout (es: ExecutorState, input: ExecutorInput) : (ExecutorState, 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, + height: es.cs.height, + round: es.cs.round, + value: "", + vr: 0} + callConsensus(es, es.bk, event) +} + + +// We do this if the executor receives a proposal +pure def ProposalMsg (es: ExecutorState, input: ExecutorInput) : (ExecutorState, 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) + else if (valid(input.proposal)) + val receivedCommit = checkThreshold( newES.bk, + input.proposal.round, + "Precommit", + {name: "PrecommitValue", + value: id(input.proposal.proposal)}) + if (receivedCommit) + // we have a commit that matches the proposal. We don't need to compare against + // es.cs.round + // TODO: check heights in bookkeeper + callConsensus( newES, + newES.bk, + { name: "ProposalAndCommitAndValid", + height: input.proposal.height, + round: input.proposal.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound}) + else if (input.proposal.round != es.cs.round or input.proposal.height != es.cs.round) + // the proposal is from the right proposer and valid, but not for this round + // keep the proposal, do nothing else + (newES, defaultResult) + else + // for current round and q, valid, and from right proposer + val receivedPolkaValidRoundVal = checkThreshold(newES.bk, + input.proposal.validRound, + "Prevote", + {name: "PolkaValue", + value: id(input.proposal.proposal)}) + val receivedPolkaCurrentVal = checkThreshold( newES.bk, + newES.cs.round, + "Prevote", + {name: "PolkaValue", + value: id(input.proposal.proposal)}) + val receivedCommitCurrentVal = checkThreshold( newES.bk, + newES.cs.round, + "Precommit", + {name: "PrecommitValue", + value: id(input.proposal.proposal)}) + if (newES.cs.step == "propose") + if (input.proposal.validRound == -1) + if (receivedPolkaCurrentVal) + callConsensus( newES, + newES.bk, + { name: "ProposalAndPolkaAndValid", + height: input.proposal.height, + round: input.proposal.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound}) + else + callConsensus( newES, + newES.bk, + { name: "Proposal", + height: input.proposal.height, + round: input.proposal.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound}) + else if (receivedPolkaValidRoundVal) + callConsensus( newES, + newES.bk, + { name: "ProposalAndPolkaPreviousAndValid", + height: input.proposal.height, + round: input.proposal.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound}) + else + (newES, defaultResult) + 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 + val pend = ( { name: "ProposalAndPolkaAndValid", + height: newES.cs.height, + round: newES.cs.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound}, + newES.cs.height, + newES.cs.round) + callConsensus( { ...newES, pendingEvents: newES.pendingEvents.union(Set(pend))}, + newES.bk, + { name: "ProposalAndCommitAndValid", + height: newES.cs.height, + round: newES.cs.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound}) + else if (receivedPolkaCurrentVal) + callConsensus( newES , + newES.bk, + { name: "ProposalAndPolkaAndValid", + height: newES.cs.height, + round: newES.cs.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound}) + else + (newES, defaultResult) + else + (newES, defaultResult) + 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: "PolkaValue", value: id(input.proposal.proposal)})) + val event: Event = {name: "ProposalAndPolkaAndInValid", + height: es.cs.height, + round: es.cs.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound} + callConsensus(es, es.bk, event) + else + val event: Event = {name: "ProposalInvalid", + height: es.cs.height, + round: es.cs.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound} + callConsensus(es, es.bk, event) + else + (es, defaultResult) +} + + +// We do this when we need to jump to a new round +pure def skip (es: ExecutorState, r: int) : (ExecutorState, ConsensusOutput) = { + // line 15 + val prop = if (es.cs.validValue != "nil") es.cs.validValue + else getValue(es) + if (Proposer(es.valset, es.cs.height, es.cs.round + 1) == es.cs.p) + callConsensus(es, es.bk, { name: "NewRoundProposer", + height: es.cs.height, + round: r, + // what value? + value: prop, + vr: es.cs.validRound}) + else + callConsensus(es, es.bk, { name: "NewRound", + height: es.cs.height, + round: r, + value: "", + vr: es.cs.validRound}) + // what do we do now in the new round? Shouldn't we look whether we can build an event. + // TODO: compute pending events. +} + + +// We do this when we have decided +pure def decided (es: ExecutorState, res: ConsensusOutput) : (ExecutorState, 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) + // then, we would not do this here, but expect the environment to create a (to be defined) + // ExecutorInput + val s1 = callConsensus(es, es.bk, {name : "NewHeight", + height : es.cs.height + 1, + round: -1, + value: "", + vr: es.cs.validRound}) + skip (s1._1, 0) +*/ + ({ ...es, chain: es.chain.append(res.decided) } , res) +} + + +// 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) +} + + +pure def setValue(es: ExecutorState, value: Value_t) : (ExecutorState, ConsensusOutput) = + ({ ...es, nextValueToPropose: value }, defaultResult) + + + + +/* ********************************************************* + * 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: shall we check whether the sender actually is in the validator set + if (input.name == "proposal") { + val cons_res = ProposalMsg(es, input) + if (cons_res._2.name == "decided") + decided (cons_res._1, cons_res._2) + else + cons_res + } + else if (input.name == "votemessage" and input.vote.step == "Precommit") { + val res = applyVote(es.bk, toVote(input.vote), es.valset.get(input.vote.src)) + val newES = { ...es, bk: res.bookkeeper, applyvotesResult: res.event} + // only a commit event can come here. + val cons_res = Precommit(newES, input, res.event) + if (cons_res._2.name == "decided") + decided (cons_res._1, cons_res._2) + else + cons_res + } + else if (input.name == "votemessage" and input.vote.step == "Prevote") { + val res = applyVote(es.bk, toVote(input.vote), es.valset.get(input.vote.src)) + val newES = { ...es, bk: res.bookkeeper, applyvotesResult: res.event} + // only a commit event can come here. + Prevote(newES, input, res.event) + } + else if (input.name == "timeout") { + val res = Timeout(es, input) + // result should be vote or skip + 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 + else + res + } + else if (input.name == "start") { + // + val new = { ...es, started: true} + skip (new, 0) + } + else if (input.name == "pending") { + PendingEvent(es, input) + } + else if (input.name == "SetNextProposedValue") + setValue(es, input.nextValueToPropose) + else + (es, defaultResult) +} + + +// This is a simple function that figures out in what external events (messages, +// 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) = { + if (not(state.es.started)) + (state, { ...defaultInput, name: "start" }) + + else if (state.incomingProposals != Set()) + // pick proposal, remove it from incoming + // val prop = state.incomingProposals.chooseSome() + val prop = state.incomingProposals.fold (emptyProposal, (sum, y) => y) + val newstate = { ...state, incomingProposals: state.incomingProposals.exclude(Set(prop))} + (newstate, { ...defaultInput, name: "proposal", proposal: prop}) + + else if (state.incomingVotes != Set()) + // pick vote, remove it from incoming + // val vote = state.incomingVotes.chooseSome() + val vote = state.incomingVotes.fold(emptyVote, (sum, y) => y) + val newstate = { ...state, incomingVotes: state.incomingVotes.exclude(Set(vote))} + (newstate, { ...defaultInput, name: "votemessage", vote: vote}) + + else if (state.timeout.exists(x => x._2 == state.es.cs.height and + x._3 == state.es.cs.round)) + // pick timeout, remove it from incoming + val timeouts = state.timeout.filter(x => x._2 == state.es.cs.height and + x._3 == state.es.cs.round) + // val timeout = timeouts.chooseSome() + 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) = { + if (command == "start" and not(state.es.started)) + (state, { ...defaultInput, name: "start" }) + + else if (command == "proposal" and state.incomingProposals != Set()) + // pick proposal, remove it from incoming + // val prop = state.incomingProposals.chooseSome() + val prop = state.incomingProposals.fold (emptyProposal, (sum, y) => y) + val newstate = { ...state, incomingProposals: state.incomingProposals.exclude(Set(prop))} + (newstate, { ...defaultInput, name: "proposal", proposal: prop}) + + else if (command == "vote" and state.incomingVotes != Set()) + // pick vote, remove it from incoming + // val vote = state.incomingVotes.chooseSome() + val vote = state.incomingVotes.fold(emptyVote, (sum, y) => y) + val newstate = { ...state, incomingVotes: state.incomingVotes.exclude(Set(vote))} + (newstate, { ...defaultInput, name: "votemessage", vote: vote}) + + else if (command == "timeout" and state.timeout.exists(x => x._2 == state.es.cs.height and + x._3 == state.es.cs.round)) + // pick timeout, remove it from incoming + val timeouts = state.timeout.filter(x => x._2 == state.es.cs.height and + x._3 == state.es.cs.round) + // val timeout = timeouts.chooseSome() + 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 (command == "pending" and state.es.pendingEvents != Set()) + // this might be cheating as we look into the "es" + (state, { ...defaultInput, name: "pending" }) + + else + (state, defaultInput) +} + +} \ No newline at end of file diff --git a/Specs/Quint/extraSpells.qnt b/Specs/Quint/extraSpells.qnt index b0444ed17..a0fb9b7cc 100644 --- a/Specs/Quint/extraSpells.qnt +++ b/Specs/Quint/extraSpells.qnt @@ -115,6 +115,22 @@ module extraSpells { assert(Set(3) == Set(3).setAdd(3)), } + /// Add a set element only if a condition is true. + /// + /// - @param __set a set to add an element to + /// - @param __elem an element to add + /// - @param __cond a condition that must be true to add the element to the set + /// - @returns a new set that contains all elements of __set and __elem, if __cond is true + pure def setAddIf(__set: Set[a], __elem: a, __cond: bool): Set[a] = + if (__cond) __set.setAdd(__elem) else __set + + run setAddIfTest = all { + assert(Set(2, 3, 4, 5) == Set(2, 3, 4).setAddIf(5, true)), + assert(Set(2, 3, 4) == Set(2, 3, 4).setAddIf(5, false)), + assert(Set(3) == Set(3).setAddIf(3, true)), + assert(Set(3) == Set(3).setAddIf(3, false)), + } + /// Safely set a map entry. /// /// - @param __map a map to set an entry to @@ -160,11 +176,24 @@ module extraSpells { /// plus the ones in __entries pure def mapAddSet(__map: a -> int, __entries: a -> int): a -> int = { __map.keys().union(__entries.keys()).mapBy(__k => if (__map.has(__k) and __entries.has(__k)) __map.get(__k) + __entries.get(__k) - else if (__map.has(__k)) __map.get(__k) else __entries.get(__k)) + else if (__map.has(__k)) __map.get(__k) else __entries.get(__k)) } run mapAddSetTest = all { assert(Map(2 -> 3, 4 -> 5, 7 -> 8).mapAddSet(Map(3 -> 6, 8 -> 9)) == Map(2 -> 3, 4 -> 5, 3 -> 6, 7 -> 8, 8 -> 9)), assert(Map(2 -> 3, 4 -> 5, 7 -> 8).mapAddSet(Map(3 -> 6, 7 -> 9)) == Map(2 -> 3, 4 -> 5, 3 -> 6, 7 -> 17)), } + + /// Compute the sum of all values in the map. + /// + /// - @param __map a map with values of type int + /// - @returns the sum of the values of all entries in __map + pure def mapSumValues(__map: a -> int): int = + __map.keys().fold(0, (__acc, __val) => __acc + __map.get(__val)) + + run mapSumValuesTest = all { + assert(0 == Map().mapSumValues()), + assert(6 == Map("a" -> 0, "b" -> 1, "c" -> 2, "d" -> 3).mapSumValues()), + } + } \ No newline at end of file diff --git a/Specs/Quint/statemachineAsync.qnt b/Specs/Quint/statemachineAsync.qnt new file mode 100644 index 000000000..2d532e2ff --- /dev/null +++ b/Specs/Quint/statemachineAsync.qnt @@ -0,0 +1,187 @@ +// -*- mode: Bluespec; -*- + +/* + This contains asynchronous message transfer semantics, that is, + - upon sending, messages are put into a buffer (for each receiver). + The buffer is part of the network and not in any validator state + - there is a deliver event that takes a message out of the buffer + and puts it into the incoming set of the validator (alternatively + a message by a faulty process may be put into the incoming set) + - this allows re-ordering of message in the network, that is, a + process may receive message m1 before m2 while another process + may receive m2 before m1 + Example models using this specification can be found in AsyncModels.qnt +*/ + + +module statemachineAsync { + +import executor.* from "./executor" +import consensus.* from "./consensus" +import voteBookkeeper.* from "./voteBookkeeper" + +const validators : Set[Address_t] +const validatorSet : Address_t -> int +const Faulty : Set[Address_t] +val Correct = validators.exclude(Faulty) + +// These are used to define what messages can be sent by faulty validators +const Values : Set[Value_t] +const Rounds : Set[Round_t] +const Heights : Set[Height_t] + +// putting all messages that could be ever sent by faulty validators into +// AllFaultyVotes and AllFaultyProposals + +val RoundsOrNil = Rounds.union(Set(-1)) +val Steps = Set("Prevote", "Precommit") + +val AllFaultyVotes : Set[VoteMsg_t] = + tuples(Faulty, Heights, Rounds, Values, Steps) + .map(t => { src: t._1, height: t._2, round: t._3, id: t._4, step: t._5 }) + +// val AllFaultyVotes : Set[VoteMsg_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] = + 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 } + +val ConsensusOutputInv = consensusOutputs.union(Set(defaultResult.name)).contains(_hist.output.name) + + +action unchangedAll = all { + system' = system, + propBuffer' = propBuffer, + voteBuffer' = voteBuffer, + _hist' = _hist +} + +val AgreementInv = tuples(Correct, Correct).forall(p => + (system.get(p._1).es.chain != List() and system.get(p._2).es.chain != List()) + implies + system.get(p._1).es.chain[0] == system.get(p._2).es.chain[0]) + +// Actions +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 } +} + +// 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] = { + 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] = { + sys.keys().mapBy(x => + { ...sys.get(x).union(Set(vote)) }) +} + +// Record that a timeout has started at node v +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)} + ))}) +} + +action valStep(v: Address_t) : bool = { + // pick action + val input = system.get(v).nextAction() // TODO: nextAction could go within executor boundary + // remove action from v + val sys1 = system.put(v, input._1) + // call executor + val res = executor(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}) + // do networking + if (res._2.name == "proposal") all { + propBuffer' = sendProposal(propBuffer, res._2.proposal), // TODO: this is immediate + voteBuffer' = voteBuffer, + system' = sys, + } + else if (res._2.name == "votemessage") all { + propBuffer' = propBuffer, + voteBuffer' = sendVote(voteBuffer, res._2.voteMessage), // TODO: this is immediate + system' = sys, + } + else if (res._2.name == "timeout") all { + propBuffer' = propBuffer, + voteBuffer' = voteBuffer, + system' = startTimeout(sys, v, res._2.timeout), + } + else if (res._2.name == "skipRound") all { + propBuffer' = propBuffer, + voteBuffer' = voteBuffer, + //skipRound should never leave the executor + system' = sys, + } + else all { + propBuffer' = propBuffer, + voteBuffer' = voteBuffer, + system' = sys, + }, + _hist' = { validator: v, input: input._2, output: res._2 } +// _histSimple' = (v, input._2.name, res._2.name) + } +} + +action setNextValueToPropose(v: Address_t, value: Value_t) : bool = all { + val res = executor(system.get(v).es, { ...defaultInput, name: "SetNextProposedValue", nextValueToPropose: value}) + val newNS = { ...system.get(v), es: res._1} + system' = system.put(v, newNS), + _hist' = _hist, + propBuffer' = propBuffer, + voteBuffer' = voteBuffer, +} + +action deliverProposal(v: Address_t, p: ProposeMsg_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)) }), + _hist' = _hist, + voteBuffer' = voteBuffer, +} + +action deliverVote(v: Address_t, vote: VoteMsg_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)) }), + _hist' = _hist, + propBuffer' = propBuffer, +} + +// deliver a message. Take it from the network buffer of from the faulty set +// and put it into the incoming sets +action deliver(v: Address_t) : bool = any { + nondet prop = oneOf(propBuffer.get(v).union(AllFaultyProposals)) + deliverProposal(v, prop), + nondet vote = oneOf(voteBuffer.get(v).union(AllFaultyVotes)) + deliverVote(v, vote) +} + +action step = { + nondet v = oneOf(Correct) + nondet value = oneOf(Values) + any { + valStep(v), + deliver(v), + setNextValueToPropose(v, value), + } +} + + +} \ No newline at end of file diff --git a/Specs/Quint/statemachineTest.qnt b/Specs/Quint/statemachineTest.qnt new file mode 100644 index 000000000..1e2115ae8 --- /dev/null +++ b/Specs/Quint/statemachineTest.qnt @@ -0,0 +1,223 @@ +// -*- mode: Bluespec; -*- + +/* + This contains some (non-standard) synchronous message transfer + semantics, that is, + - upon sending, messages are put into the incoming set of the + validator + - no faulty messages are modeled here + The model is quite simple but might be useful to generates + traces. +*/ + +module statemachineTest { + +import executor.* from "./executor" +import consensus.* from "./consensus" +import voteBookkeeper.* from "./voteBookkeeper" + +val validators = Set("v1", "v2", "v3", "v4") +val validatorSet = validators.mapBy(x => 1) + +var system : Address_t -> NodeState +var _hist: (str, ExecutorInput, ConsensusOutput) +//var _histSimple: (str, str, str) + +action init = all { + system' = validators.mapBy(v => initNode(v, validatorSet)), + _hist' = ("INIT", defaultInput, defaultResult) +// _histSimple' = ("INIT", "", "") +} + +// Put the proposal into the inbuffers of all validators +pure def deliverProposal (sys: Address_t -> NodeState, prop: ProposeMsg_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 = { + sys.keys().mapBy(x => + { ...sys.get(x), incomingVotes: sys.get(x).incomingVotes.union(Set(vote)) }) +} + +// Record that a timeout has started at node v +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)} + ))}) +} + +// this is a simple semantics that puts messages that are sent immediately in the +// inbuffer of the receivers. By the way nextAction() is implemented timeouts +// 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 + // remove action from v + val sys1 = system.put(v, input._1) + // call executor + val res = executor(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}) + // do networking + if (res._2.name == "proposal") + system' = deliverProposal(sys, res._2.proposal) // TODO: this is immediate + else if (res._2.name == "votemessage") + system' = deliverVote(sys, res._2.voteMessage) // TODO: this is immediate + 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 + system' = sys + else + system' = sys, + _hist' = (v, input._2, res._2) +// _histSimple' = (v, input._2.name, res._2.name) + } +} + +action setNextValueToPropose(v: Address_t, value: Value_t) : bool = all { + val res = executor(system.get(v).es, { ...defaultInput, name: "SetNextProposedValue", nextValueToPropose: value}) + val newNS = { ...system.get(v), es: res._1} + system' = system.put(v, newNS), + _hist' = _hist +} + +action step = { + nondet v = oneOf(validators) + nondet value = oneOf(Set("a", "b", "c")) + any { + valStep(v), + setNextValueToPropose(v, value), + } +} + + + +action valStepCommand(v: Address_t, command: str) : bool = { + // pick action + 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) + all { + // update v's state after the step + val sys = sys1.put(v, { ...sys1.get(v), es: res._1}) + // do networking + if (res._2.name == "proposal") + system' = deliverProposal(sys, res._2.proposal) // TODO: this is immediate + else if (res._2.name == "votemessage") + system' = deliverVote(sys, res._2.voteMessage) // TODO: this is immediate + 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 + system' = sys + else + system' = sys, + _hist' = (v, input._2, res._2) +// _histSimple' = (v, input._2.name, res._2.name) + } +} + +run DecidingRunTest = { + init + .then(setNextValueToPropose("v2", "a block")) + .then(valStepCommand("v1", "start")) + .then(valStepCommand("v2", "start")) + .then(valStepCommand("v3", "start")) + .then(valStepCommand("v4", "start")) + .then(valStepCommand("v1", "proposal")) + .then(valStepCommand("v2", "proposal")) + .then(valStepCommand("v3", "proposal")) + .then(valStepCommand("v4", "proposal")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "vote")) + .then(all{ + assert(system.get("v1").incomingVotes.contains( + { src: "v1", height: 0, round: 0, step: "Precommit", id: "a block" } + )), + valStepCommand("v2", "vote") + }) + .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v2", "vote")) + .then(all{ + assert(system.get("v2").incomingVotes.contains( + { src: "v2", height: 0, round: 0, step: "Precommit", id: "a block" } + )), + valStepCommand("v3", "vote") + }) + .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v3", "vote")) + .then(all{ + assert(system.get("v3").incomingVotes.contains( + { src: "v3", height: 0, round: 0, step: "Precommit", id: "a block" } + )), + assert(system.get("v3").es.chain == List()), + valStepCommand("v3", "vote") + }) + .then(all{ + // validator 3 decided on "a block" + assert(system.get("v3").es.chain.head() == "a block"), + system' = system, + _hist' = _hist + }) +} + + +run TimeoutRunTest = { + init + .then(setNextValueToPropose("v2", "a block")) + .then(valStepCommand("v1", "start")) + .then(valStepCommand("v2", "start")) + .then(valStepCommand("v3", "start")) + .then(valStepCommand("v4", "start")) + .then(valStepCommand("v1", "timeout")) + .then(valStepCommand("v2", "proposal")) + .then(valStepCommand("v3", "timeout")) + .then(valStepCommand("v4", "timeout")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v4", "timeout")) + .then(all { + // validator 4 timed out and went to round 1 + assert(system.get("v4").es.cs.round == 1), + system' = system, + _hist' = _hist, + }) +} + +} + diff --git a/Specs/Quint/voteBookkeeper.qnt b/Specs/Quint/voteBookkeeper.qnt index b00e2b0a6..15d725605 100644 --- a/Specs/Quint/voteBookkeeper.qnt +++ b/Specs/Quint/voteBookkeeper.qnt @@ -21,12 +21,13 @@ module voteBookkeeper { // A value is a string type Value = str - // Weigth is an integer + // Weight is an integer type Weight = int - // The vote type + type VoteType = str + type Vote = { - typ: str, + typ: VoteType, round: Round, value: Value, address: Address @@ -61,6 +62,7 @@ module voteBookkeeper { type Bookkeeper = { height: Height, + currentRound: Round, totalWeight: Weight, rounds: Round -> RoundVotes } @@ -72,59 +74,83 @@ module voteBookkeeper { // Internal functions // creates a new voteCount - pure def newVoteCount(total: Weight): VoteCount = { - {totalWeight: total, valuesWeights: Map(), votesAddresses: Set()} - } + pure def newVoteCount(total: Weight): VoteCount = + { totalWeight: total, valuesWeights: Map(), votesAddresses: Set() } // Returns true if weight > 2/3 * total (quorum: at least f+1 correct) - pure def isQuorum(weight: int, total: int): bool = { + pure def isQuorum(weight: Weight, total: Weight): bool = 3 * weight > 2 * total - } + + // True iff the vote count has a quorum on a specific value. + pure def hasQuorumOnValue(voteCount: VoteCount, value: Value): bool = + isQuorum(voteCount.valuesWeights.getOrElse(value, 0), voteCount.totalWeight) + + // True iff the vote count has a quorum on any value. + pure def hasQuorumOnAny(voteCount: VoteCount): bool = + isQuorum(voteCount.valuesWeights.mapSumValues(), voteCount.totalWeight) // Returns true if weight > 1/3 * total (small quorum: at least one correct) - pure def isSkip(weight: int, total: int): bool = { + pure def isSkip(weight: Weight, total: Weight): bool = 3 * weight > total - } + // Adds a vote of weight weigth to a voteCount if there is not vote registered for the voter. - pure def addVote(voteCount: VoteCount, vote: Vote, weight: Weight): VoteCount = { - if (vote.address.in(voteCount.votesAddresses)) voteCount - else val newWeight = voteCount.valuesWeights.getOrElse(vote.value, 0) + weight - voteCount.with("valuesWeights", voteCount.valuesWeights.mapSafeSet(vote.value, newWeight)) - .with("votesAddresses", voteCount.votesAddresses.setAdd(vote.address)) - } + pure def addVote(voteCount: VoteCount, vote: Vote, weight: Weight): VoteCount = + if (vote.address.in(voteCount.votesAddresses)) + // Do not count vote if address has already voted. + voteCount + else + val newWeight = voteCount.valuesWeights.getOrElse(vote.value, 0) + weight + voteCount + .with("valuesWeights", voteCount.valuesWeights.mapSafeSet(vote.value, newWeight)) + .with("votesAddresses", voteCount.votesAddresses.setAdd(vote.address)) // Given a voteCount and a value, the function returns: // - A threshold Value if there is a quorum for the given value; // - A threshold Nil if there is a quorum for the nil and no quorum for the value; // - A threshold Any if there is no quorum for the value or nil and there is a quroum for any (including nil); // - A threshold Unreached otherwise indicating that no quorum has been yet reached. - pure def computeThreshold(voteCount: VoteCount, value: Value): Threshold = { - val weight = voteCount.valuesWeights.getOrElse(value, 0) - val totalWeight = voteCount.totalWeight - val sumWeight = voteCount.valuesWeights.keys().fold(0, (sum, v) => sum + voteCount.valuesWeights.get(v)) - if (value != "nil" and isQuorum(weight, totalWeight)) {name: "Value", value: value} - else if (value == "nil" and isQuorum(weight, totalWeight)) {name: "Nil", value: "null"} - else if (isQuorum(sumWeight, totalWeight)) {name: "Any", value: "null"} - else {name: "Unreached", value: "null"} - } - - // Given a round, voteType and threshold it resturns the corresponding ExecutorEvent - pure def toEvent(round: Round, voteType: str, threshold: Threshold): ExecutorEvent = { - if (threshold.name == "Unreached") {round: round, name: "None", value: "null"} - else if (voteType == "Prevote" and threshold.name == "Value") {round: round, name: "PolkaValue", value: threshold.value} - else if (voteType == "Prevote" and threshold.name == "Nil") {round: round, name: "PolkaNil", value: "null"} - else if (voteType == "Prevote" and threshold.name == "Any") {round: round, name: "PolkaAny", value: "null"} - else if (voteType == "Precommit" and threshold.name == "Value") {round: round, name: "PrecommitValue", value: threshold.value} - else if (voteType == "Precommit" and threshold.name == "Any") {round: round, name: "PrecommitAny", value: "null"} - else if (threshold.name == "Skip") {round: round, name: "Skip", value: "null"} - else {round: round, name: "None", value: "null"} - } - - + pure def computeThreshold(voteCount: VoteCount, value: Value): Threshold = + if (voteCount.hasQuorumOnValue(value)) { + if (value == "nil") + { name: "Nil", value: "null" } + else + { name: "Value", value: value } + } else if (voteCount.hasQuorumOnAny()) { + { name: "Any", value: "null" } + } else + { name: "Unreached", value: "null" } + + // Given a round, voteType and threshold, return the corresponding ExecutorEvent + pure def toEvent(round: Round, voteType: VoteType, threshold: Threshold): ExecutorEvent = + if (threshold.name == "Unreached") + { round: round, name: "None", value: "null" } + + // prevote + else if (voteType == "Prevote" and threshold.name == "Value") + { round: round, name: "PolkaValue", value: threshold.value } + else if (voteType == "Prevote" and threshold.name == "Nil") + { round: round, name: "PolkaNil", value: "null" } + else if (voteType == "Prevote" and threshold.name == "Any") + { round: round, name: "PolkaAny", value: "null" } + + // precommit + else if (voteType == "Precommit" and threshold.name == "Value") + { round: round, name: "PrecommitValue", value: threshold.value } + else if (voteType == "Precommit" and threshold.name == "Any") + { round: round, name: "PrecommitAny", value: "null" } + else if (voteType == "Precommit" and threshold.name == "Nil") + { round: round, name: "PrecommitAny", value: "null" } + + else if (threshold.name == "Skip") + { round: round, name: "Skip", value: "null" } + + else + { round: round, name: "None", value: "null" } // Executor interface + type BKResult = { bookkeeper: Bookkeeper, event: ExecutorEvent } - // Called by the executor when it receives a vote. The functiojn takes the following steps: + // Called by the executor 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 corresponsing ExecutorEvent. // - Othewise, the function returns a no-threshold event. @@ -132,52 +158,110 @@ module voteBookkeeper { // 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: int): {bookkeeper: Bookkeeper, event: ExecutorEvent} = { + pure def applyVote(keeper: Bookkeeper, vote: Vote, weight: Weight): { bookkeeper: Bookkeeper, event: ExecutorEvent } = val height = keeper.height val total = keeper.totalWeight - val roundVotes = keeper.rounds.getOrElse(vote.round, {height: height, - round: vote.round, - prevotes: newVoteCount(total), - precommits: newVoteCount(total), - emittedEvents: Set(), - votesAddressesWeights: Map()}) - val updatedVoteCount = if (vote.typ == "Prevote") roundVotes.prevotes.addVote(vote, weight) - else roundVotes.precommits.addVote(vote, weight) - val threshold = computeThreshold(updatedVoteCount, vote.value) - val event = toEvent(vote.round, vote.typ, threshold) - val updatedVotesAddressesWeights = if (roundVotes.votesAddressesWeights.has(vote.address)) roundVotes.votesAddressesWeights - else roundVotes.votesAddressesWeights.mapSafeSet(vote.address, weight) - val sumSkip = updatedVotesAddressesWeights.keys().fold(0, (sum, v) => sum + updatedVotesAddressesWeights.get(v)) - val finalEvent = if (not(event.in(roundVotes.emittedEvents))) event - else if (roundVotes.emittedEvents == Set() and isSkip(sumSkip, total)) {round: vote.round, name: "Skip", value: "null"} - else {round: vote.round, name: "None", value: "null"} - val updatedRoundVotes = if (vote.typ == "Prevote") roundVotes.with("prevotes", updatedVoteCount) - else roundVotes.with("precommits", updatedVoteCount) - val updatedEmmittedEvents = if (finalEvent.name != "None") roundVotes.emittedEvents.setAdd(finalEvent) - else roundVotes.emittedEvents - val updatedBookkeeper = keeper.with("rounds", keeper.rounds.mapSafeSet(vote.round, updatedRoundVotes.with("votesAddressesWeights", updatedVotesAddressesWeights) - .with("emittedEvents", updatedEmmittedEvents))) - {bookkeeper: updatedBookkeeper, event: finalEvent} - } + + val defaultRoundVotes = { + height: height, + round: vote.round, + prevotes: newVoteCount(total), + precommits: newVoteCount(total), + emittedEvents: Set(), + votesAddressesWeights: Map() + } + val roundVotes = keeper.rounds.getOrElse(vote.round, defaultRoundVotes) + + val updatedVoteCount = + if (vote.typ == "Prevote") + roundVotes.prevotes.addVote(vote, weight) + else + roundVotes.precommits.addVote(vote, weight) + + val updatedVotesAddressesWeights = + if (roundVotes.votesAddressesWeights.has(vote.address)) + roundVotes.votesAddressesWeights + else + roundVotes.votesAddressesWeights.mapSafeSet(vote.address, weight) + + val updatedRoundVotes = + if (vote.typ == "Prevote") + roundVotes.with("prevotes", updatedVoteCount) + else + roundVotes.with("precommits", updatedVoteCount) + + // Combined weight of all validators at this height + val combinedWeight = updatedVotesAddressesWeights.mapSumValues() + + val finalEvent = + if (vote.round > keeper.currentRound and isSkip(combinedWeight, total)) + { round: vote.round, name: "Skip", value: "null" } + else + val threshold = computeThreshold(updatedVoteCount, vote.value) + val event = toEvent(vote.round, vote.typ, threshold) + if (not(event.in(roundVotes.emittedEvents))) + event + else + { round: vote.round, name: "None", value: "null" } + + val updatedEmittedEvents = roundVotes.emittedEvents.setAddIf(finalEvent, finalEvent.name != "None") + + val updatedRoundVotes2 = updatedRoundVotes + .with("votesAddressesWeights", updatedVotesAddressesWeights) + .with("emittedEvents", updatedEmittedEvents) + + val newBookkeeper = + keeper.with("rounds", keeper.rounds.mapSafeSet(vote.round, updatedRoundVotes2)) + + { + bookkeeper: newBookkeeper, + event: finalEvent + } // Called by the executor 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 // 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: str, threshold: Threshold): bool = { + pure def checkThreshold(keeper: Bookkeeper, round: Round, voteType: VoteType, threshold: Threshold): bool = if (keeper.rounds.has(round)) { val roundVotes = keeper.rounds.get(round) - val voteCount = if (voteType == "Prevote") roundVotes.prevotes - else roundVotes.precommits - val total = voteCount.totalWeight - val sumWeight = voteCount.valuesWeights.keys().fold(0, (sum, v) => sum + voteCount.valuesWeights.get(v)) - if (threshold.name == "Value") isQuorum(voteCount.valuesWeights.getOrElse(threshold.value, 0), total) - else if (threshold.name == "Nil") isQuorum(voteCount.valuesWeights.getOrElse("nil", 0), total) - else if (threshold.name == "Any") isQuorum(sumWeight, total) - else false + val voteCount = if (voteType == "Prevote") roundVotes.prevotes else roundVotes.precommits + if (threshold.name == "Value") { + voteCount.hasQuorumOnValue(threshold.value) + } else if (threshold.name == "Nil") { + voteCount.hasQuorumOnValue("nil") + } else if (threshold.name == "Any") { + voteCount.hasQuorumOnAny() + } else false } else false - } + +// run PrecommitTest = all { +// val bin : Bookkeeper = { +// height: 0, +// rounds: +// Map( +// 0 -> +// { +// height: 0, +// precommits: { total: 4, valuesAddresses: Map(), valuesWeights: Map() }, +// prevotes: { total: 4, valuesAddresses: Map(), valuesWeights: Map("a block" -> 1, "nil" -> 3) }, +// round: 0 +// } +// ), +// totalWeight: 4 +// } +// val o1 = applyVote(bin, {value: "nil", round: 0, address: "v0", typ: "Precommit" }, 1) +// val o2 = applyVote(o1.bookkeeper, {value: "nil", round: 0, address: "v1", typ: "Precommit" }, 1) +// val o3 = applyVote(o2.bookkeeper, {value: "nil", round: 0, address: "v2", typ: "Precommit" }, 1) +// val o4 = applyVote(o3.bookkeeper, {value: "nil", round: 0, address: "v3", typ: "Precommit" }, 1) +// all{ +// assert(o1.event.name == "None"), +// assert(o2.event.name == "None"), +// assert(o3.event.name == "PrecommitAny"), +// assert(o4.event.name == "PrecommitAny") +// } +// } // **************************************************************************** // Unit tests @@ -196,7 +280,7 @@ module voteBookkeeper { assert(isSkip(3,6) == true) } - run addVoteTest = { + run addVoteTest = val voteCount = {totalWeight: 100, valuesWeights: Map("val1" -> 30, "val2" -> 20), votesAddresses: Set("alice", "bob")} val vote = {typ: "precommit", round: 10, value: "val3", address: "john"} all { @@ -207,14 +291,12 @@ module voteBookkeeper { // existing voter assert(addVote(voteCount, vote.with("address", "alice"), 10) == voteCount), } - } - run computeThresholdTest = { + run computeThresholdTest = val voteCount = {totalWeight: 100, valuesWeights: Map(), votesAddresses: Set("alice", "bob")} val mapValueReached = Map("val1" -> 67, "val2" -> 20) val mapNilReached = Map("nil" -> 70, "val2" -> 20) val mapNoneReached = Map("nil" -> 20, "val2" -> 20) - all { assert(computeThreshold(voteCount, "val3") == {name: "Unreached", value: "null"}), assert(computeThreshold(voteCount.with("valuesWeights", mapValueReached), "val1") == {name: "Value", value: "val1"}), @@ -224,9 +306,8 @@ module voteBookkeeper { assert(computeThreshold(voteCount.with("valuesWeights", mapNoneReached), "val1") == {name: "Unreached", value: "null"}), assert(computeThreshold(voteCount.with("valuesWeights", mapNoneReached), "nil") == {name: "Unreached", value: "null"}), } - } - run toEventTest = { + run toEventTest = val thresholdUnreached = {name: "Unreached", value: "null"} val thresholdAny = {name: "Any", value: "null"} val thresholdNil = {name: "Nil", value: "null"} @@ -240,84 +321,13 @@ module voteBookkeeper { assert(toEvent(round, "Prevote", thresholdNil) == {round: round, name: "PolkaNil", value: "null"}), assert(toEvent(round, "Prevote", thresholdValue) == {round: round, name: "PolkaValue", value: "val1"}), assert(toEvent(round, "Precommit", thresholdAny) == {round: round, name: "PrecommitAny", value: "null"}), - assert(toEvent(round, "Precommit", thresholdNil) == {round: round, name: "None", value: "null"}), + assert(toEvent(round, "Precommit", thresholdNil) == {round: round, name: "PrecommitAny", value: "null"}), assert(toEvent(round, "Precommit", thresholdValue) == {round: round, name: "PrecommitValue", value: "val1"}), assert(toEvent(round, "Prevote", thresholdSkip) == {round: round, name: "Skip", value: "null"}), assert(toEvent(round, "Precommit", thresholdSkip) == {round: round, name: "Skip", value: "null"}), assert(toEvent(round, "Precommit", {name: "Error", value: "null"}) == {round: round, name: "None", value: "null"}), assert(toEvent(round, "Error", thresholdAny) == {round: round, name: "None", value: "null"}), } - } - - // **************************************************************************** - // State machine state - // **************************************************************************** - // Bookkeeper state - var bookkeeper: Bookkeeper - // Last emitted event - var lastEmitted: ExecutorEvent - - // **************************************************************************** - // Execution - // **************************************************************************** +} - action allUnchanged: bool = all { - bookkeeper' = bookkeeper, - lastEmitted' = lastEmitted - } - - action init(totalWeight: Weight): bool = all { - bookkeeper' = {height: 10, totalWeight: totalWeight, rounds: Map()}, - lastEmitted' = {round: -1, name: "", value: "null"} - } - - action applyVoteAction(vote: Vote, weight: Weight): bool = all { - val result = applyVote(bookkeeper, vote, weight) - all { - bookkeeper' = result.bookkeeper, - lastEmitted' = result.event - } - } - - // **************************************************************************** - // Test traces - // **************************************************************************** - - // Consensus full execution with all honest validators (including the leader) and a synchronous network: - // all messages are received in order. We assume three validators in the validator set wtih 60%, 30% and 10% - // each of the total voting power - run synchronousConsensusTest = { - init(100) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "john"}, 10)) - .then(all{ assert(lastEmitted == {round: 1, name: "PolkaValue", value: "proposal"}), allUnchanged }) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "bob"}, 30)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) - .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "bob"}, 30)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) - .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "john"}, 10)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) - .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "alive"}, 60)) - .then(all{ assert(lastEmitted == {round: 1, name: "PrecommitValue", value: "proposal"}), allUnchanged }) - } - - // Reaching PolkaAny - run polkaAnyTest = { - init(100) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "val1", address: "alice"}, 60)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10)) - .then(all{ assert(lastEmitted == {round: 1, name: "PolkaAny", value: "null"}), allUnchanged }) - } - - // Reaching PolkaNil - run polkaNilTest = { - init(100) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "alice"}, 60)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10)) - .then(all{ assert(lastEmitted == {round: 1, name: "PolkaNil", value: "null"}), allUnchanged }) - } -} \ No newline at end of file diff --git a/Specs/Quint/voteBookkeeperTest.qnt b/Specs/Quint/voteBookkeeperTest.qnt new file mode 100644 index 000000000..ae635f823 --- /dev/null +++ b/Specs/Quint/voteBookkeeperTest.qnt @@ -0,0 +1,143 @@ +module voteBookkeeperTest { + + import voteBookkeeper.* from "./voteBookkeeper" + + // **************************************************************************** + // State machine state + // **************************************************************************** + + // Bookkeeper state + var bookkeeper: Bookkeeper + // Last emitted event + var lastEmitted: ExecutorEvent + + // **************************************************************************** + // Execution + // **************************************************************************** + + action allUnchanged: bool = all { + bookkeeper' = bookkeeper, + lastEmitted' = lastEmitted, + } + + action initWith(round: Round, totalWeight: Weight): bool = all { + bookkeeper' = { height: 10, currentRound: round, totalWeight: totalWeight, rounds: Map() }, + lastEmitted' = { round: -1, name: "", value: "null" }, + } + + action applyVoteAction(vote: Vote, weight: Weight): bool = + val result = applyVote(bookkeeper, vote, weight) + all { + bookkeeper' = result.bookkeeper, + lastEmitted' = result.event, + } + + // **************************************************************************** + // Test traces + // **************************************************************************** + + // auxiliary action for tests + action _assert(predicate: bool): bool = + all { predicate, allUnchanged } + + // Consensus full execution with all honest validators (including the leader) and a synchronous network: + // all messages are received in order. We assume three validators in the validator set wtih 60%, 30% and 10% + // each of the total voting power + run synchronousConsensusTest = + initWith(1, 100) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "john"}, 10)) + .then(_assert(lastEmitted == {round: 1, name: "PolkaValue", value: "proposal"})) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "bob"}, 30)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "bob"}, 30)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "john"}, 10)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "alice"}, 60)) + .then(_assert(lastEmitted == {round: 1, name: "PrecommitValue", value: "proposal"})) + + // Reaching PolkaAny + run polkaAnyTest = + initWith(1, 100) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "val1", address: "alice"}, 60)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10)) + .then(_assert(lastEmitted == {round: 1, name: "PolkaAny", value: "null"})) + + // Reaching PolkaNil + run polkaNilTest = + initWith(1, 100) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "alice"}, 60)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10)) + .then(_assert(lastEmitted == {round: 1, name: "PolkaNil", value: "null"})) + + // Reaching Skip via n+1 threshold with prevotes from two validators at a future round + run skipSmallQuorumAllPrevotesTest = + initWith(1, 100) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10)) + .then(_assert(lastEmitted == {round: 2, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "bob"}, 30)) + .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"})) + + // 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", round: 1, value: "proposal", address: "alice"}, 10)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 20)) + .then(_assert(lastEmitted == {round: 2, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 20)) + .then(_assert(lastEmitted != {round: 2, name: "Skip", value: "null"})) + + // 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", round: 1, value: "proposal", address: "alice"}, 50)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10)) + .then(_assert(lastEmitted == {round: 2, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "bob"}, 20)) + .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"})) + + // 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", round: 1, value: "proposal", address: "alice"}, 10)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 60)) + .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"})) + + // Reaching Skip via 2f+1 threshold with a single precommit from a single validator at a future round + run skipQuorumSinglePrecommitTest = + initWith(1, 100) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 60)) + .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"})) + + // 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", round: 1, value: "proposal", address: "alice"}, 10)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 30)) + .then(_assert(lastEmitted == {round: 2, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 30)) + .then(_assert(lastEmitted != {round: 2, name: "Skip", value: "null"})) + + // 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", round: 1, value: "proposal", address: "alice"}, 20)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10)) + .then(_assert(lastEmitted == {round: 2, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "bob"}, 50)) + .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"})) + +}