From 1dafd49c0e511b4662654c7956de54ecd47aa900 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hern=C3=A1n=20Vanzetto?= <15466498+hvanz@users.noreply.github.com> Date: Tue, 28 Nov 2023 11:11:34 +0100 Subject: [PATCH] tests: MBT for votekeeper (#63) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * executor start * PreCommit function * TODOs * line 28 is in the books * prevote, precommit, and timeout done. proposal missing * starting to put things together for state machine * a somewhat complete version of the executor logic * state machine, but needs to be debugged * moving statemachine. problem with chooseSome * it moves * more things moving * some problem with bookkeeper * more things move * I have seen a Polka * cleanup * cleaning * successful test of statemachine * before consensus return refactor * first pending event added * cleaned consensus * commit to merge with Manuel's updated votekeeper * to merge Daniel's comment * executor start * PreCommit function * TODOs * line 28 is in the books * prevote, precommit, and timeout done. proposal missing * starting to put things together for state machine * a somewhat complete version of the executor logic * state machine, but needs to be debugged * moving statemachine. problem with chooseSome * it moves * more things moving * some problem with bookkeeper * more things move * I have seen a Polka * cleanup * cleaning * successful test of statemachine * before consensus return refactor * first pending event added * cleaned consensus * commit to merge with Manuel's updated votekeeper * to merge Daniel's comment * addressed Daniel's comments * addressed Daniel's comments and run tests * completed the timeout test * clean up and comments * added checks for increasing round numbers * added hash function checks * valset error thrown in test fixed * added action and logic to get value from the outside into the system * comments following the discussion on where to put the reponsibility for getValue * transformed that executed events into list * added an asynchronous execution environment * added round number checks to ProposalMsg * test for disagreement in asynchronous setting * Parameterization of the Asynchronous model * Typecheck all Quint specs on CI and run test for `consensustest.qnt` * Update Specs/Quint/AsyncModels.qnt Co-authored-by: Romain Ruetschi * added a type invariant * updated syntax to Quint 0.14.4 * WIP: Deserialize ITF traces emitted by consensus Quint spec * Use fixtures from `Specs/Quint` directory * Use workspace dependencies and common settings * Add `step` action to vote keeper spec * Parse traces for the vote keeper spec * Add test fixtures for vote keeper * Cleanup * Use BigInts * moved bookkeeper statemachine out for modularity * Update Quint test job * commented a line that failed a test. Need to discuss with Manu * Run test on all Quint files * Use script to run all tests even in the presence of failures * fixed the logic and the test for Precommit,Nil * Update Specs/Quint/voteBookkeeperTest.qnt Signed-off-by: Josef Widder Co-authored-by: Hernán Vanzetto <15466498+hvanz@users.noreply.github.com> * rename files for test CI * Update .github/workflows/quint.yml * renamed one more file with a test * module renamed * Register step taken in spec with weightedVote variable * First implementation of trace player for votekeeper * Add valid trace; remove old traces * Failing test for skip round * Fix expected_output and add test for skip with quorum * fix(votekeeper): Compute threshold directly in `VoteKeeper` to account for `Skip` threshold * test: Re-enable VoteCount tests * test: Re-enable RoundVotes tests * test: Remove duplicate tests * test: Re-enable VoteKeeper tests * Re-remove invalid test cases * Remove duplicate commented test * fix(spec/votekeeper): Fix the VoteKeeper spec to account for skip threshold from higher round * fix: Fix a bug where we would double count the weight of validators which both prevoted and precommited * Fix executor spec * fix(votekeeper): Do not count validator weights twice if they prevoted and precommited when checking for Skip threshold * More refactoring; move tests near their function definitions * Add voteBookkeeperSM.qnt with consts; move state and actions to voteBookkeeper * Add Makefile and gen-traces.sh * use rstest for testdata files and fixtures * nits for Cargo.toml * fix clippy warn for items_after_test_module * use .into() to be succinct * use imports * refactor util methods * reorder imports * rename json fixture var * avoid redundant unwrap * use unimplemented!() * rm redundant type annotation * add TraceRunner trait * refactor test using TraceRunner * add Heights in Votes in ITF trace * add Height in Vote in test * pass Height in Vote creation * Update bookkeepers currentRound after calling into consensus * Rename `init` to `initWith` * Add vote invariants * Rename value in test * Make nil always one of the values to pick * Fix merge * Fix trace runner after merge * spec: Add height to vote * spec: add one more round to model * spec: add emitSkip property + a few small improvements * spec: add gitignore * Add new trace files; remove old one * add field current_round to Bookkeeper; fix tests * Fix formatting * spec: Fix executor.qnt * comment out failing test in driver.rs * mv Runner trait to itf crate * override itf crate til next release * update test * deserialize itf to native types * rm itf::Itf usages * add getters for testing * update test * fix consensus trace parsing * depend on informalsystems repo * update types for new itf-rs * refactor test module structure * use Trace::run_on * use rust i64 over BigInt * Add to quint workflow a step to generate traces, including Script/trace-remove-stuttering-steps.sh * fix consensus trace parsing * fix failing trace generation * Fix github workflow env variables * Update task name * Add mbt workflow * mbt workflow: remove branch requirement; simplify env variables * Rename workflow, task * mbt workflow: change trigger * update jq filter * update jq filter * workflow: store traces as artifact * workflow: fix env variable * update workflow * workflow: fix paths * workflow: add fixture dir variable * spec: update Makefile and gen-traces.sh * remove trace files * update Makefile * pick test fixtures at runtime * remove rstest and add glob dependency * format workflow ymls * run coverage with generated traces from MBT workflow * trigger mbt workflow at changes on the workflow yml * store round in vote * update votekeeper rust types and runner * add current_round in step log * add init step log * util method to generate itf traces * update votekeeper mbt * update mbt workflow * revert coverage workflow * set QUINT_SEED in coverage workflow * setup quint to generate traces on ci * disable output capturing in cargo test * nits * spec nits * Add back test on applyVote * Update comment in script * fix typos * use default seed in coverage workflow * update mbt workflow env vars * update rust workflow trigger paths * rm serde_with dep * Remove unused script * Use workspace dependencies --------- Co-authored-by: Josef Widder Co-authored-by: Romain Ruetschi Co-authored-by: Anca Zamfir Co-authored-by: Ranadeep Biswas --- .github/workflows/coverage.yml | 8 + .github/workflows/mbt.yml | 45 ++ .github/workflows/quint.yml | 1 - .github/workflows/rust.yml | 10 +- Code/Cargo.toml | 7 +- Code/common/src/round.rs | 4 +- Code/driver/src/util.rs | 2 +- Code/itf/Cargo.toml | 14 +- Code/itf/src/consensus.rs | 19 +- Code/itf/src/deserializers.rs | 8 +- Code/itf/src/lib.rs | 1 + Code/itf/src/utils.rs | 91 ++++ Code/itf/src/votekeeper.rs | 47 ++- Code/itf/tests/consensus.rs | 21 +- .../voteBookkeeper_polkaAnyTest_6.itf.json | 1 - .../voteBookkeeper_polkaNilTest_7.itf.json | 1 - ...keeper_synchronousConsensusTest_5.itf.json | 1 - Code/itf/tests/votekeeper.rs | 66 ++- Code/itf/tests/votekeeper/runner.rs | 183 ++++++++ Code/itf/tests/votekeeper/utils.rs | 55 +++ Code/round/src/events.rs | 4 +- Code/round/src/state_machine.rs | 2 +- Code/vote/src/keeper.rs | 22 +- Code/vote/src/round_votes.rs | 8 + Code/vote/src/round_weights.rs | 4 + Docs/architecture/adr-template.md | 2 +- Specs/Quint/.gitignore | 2 + Specs/Quint/Makefile | 43 ++ Specs/Quint/executor.qnt | 2 +- Specs/Quint/extraSpells.qnt | 11 +- Specs/Quint/scripts/gen-traces.sh | 62 +++ Specs/Quint/voteBookkeeper.qnt | 397 +++++++++++------- Specs/Quint/voteBookkeeperSM.qnt | 36 ++ Specs/Quint/voteBookkeeperTest.qnt | 195 ++++----- 34 files changed, 1048 insertions(+), 327 deletions(-) create mode 100644 .github/workflows/mbt.yml create mode 100644 Code/itf/src/utils.rs delete mode 100644 Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaAnyTest_6.itf.json delete mode 100644 Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaNilTest_7.itf.json delete mode 100644 Code/itf/tests/fixtures/votekeeper/voteBookkeeper_synchronousConsensusTest_5.itf.json create mode 100644 Code/itf/tests/votekeeper/runner.rs create mode 100644 Code/itf/tests/votekeeper/utils.rs create mode 100644 Specs/Quint/.gitignore create mode 100644 Specs/Quint/Makefile create mode 100755 Specs/Quint/scripts/gen-traces.sh create mode 100644 Specs/Quint/voteBookkeeperSM.qnt diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index c141726f3..86bf4fede 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -5,9 +5,13 @@ on: branches: main paths: - Code/** + - Specs/Quint/** + - .github/workflows/coverage.yml pull_request: paths: - Code/** + - Specs/Quint/** + - .github/workflows/coverage.yml jobs: coverage: @@ -20,6 +24,10 @@ jobs: steps: - name: Checkout uses: actions/checkout@v4 + - uses: actions/setup-node@v3 + with: + node-version: "18" + - run: npm install -g @informalsystems/quint - name: Setup Rust toolchain uses: actions-rust-lang/setup-rust-toolchain@v1 with: diff --git a/.github/workflows/mbt.yml b/.github/workflows/mbt.yml new file mode 100644 index 000000000..639213c65 --- /dev/null +++ b/.github/workflows/mbt.yml @@ -0,0 +1,45 @@ +name: MBT +on: + push: + branches: + - main + paths: + - Specs/Quint/** + - Code/** + - .github/workflows/mbt.yml + pull_request: + paths: + - Specs/Quint/** + - Code/** + - .github/workflows/mbt.yml + +jobs: + gen-and-exec-traces: + name: Generate and execute random traces + runs-on: ubuntu-latest + env: + CARGO_INCREMENTAL: 0 + CARGO_PROFILE_DEV_DEBUG: 1 + CARGO_PROFILE_RELEASE_DEBUG: 1 + RUST_BACKTRACE: short + CARGO_NET_RETRY: 10 + RUSTUP_MAX_RETRIES: 10 + steps: + - name: Checkout + uses: actions/checkout@v4 + - uses: actions/setup-node@v3 + with: + node-version: "18" + - run: npm install -g @informalsystems/quint + - name: Setup Rust toolchain + uses: actions-rust-lang/setup-rust-toolchain@v1 + - name: Install cargo-nextest + uses: taiki-e/install-action@cargo-nextest + - name: Build code + working-directory: Code/itf + run: cargo nextest run --workspace --all-features --no-run + - name: Current time as random seed for Quint + run: echo "QUINT_SEED=$(date +%s)" >> $GITHUB_ENV + - name: Run tests from traces (with random seed) + working-directory: Code/itf + run: cargo nextest run --workspace --all-features test_itf diff --git a/.github/workflows/quint.yml b/.github/workflows/quint.yml index 186268d6f..26099622f 100644 --- a/.github/workflows/quint.yml +++ b/.github/workflows/quint.yml @@ -33,4 +33,3 @@ jobs: node-version: "18" - run: npm install -g @informalsystems/quint - run: bash Scripts/quint-forall.sh test Specs/Quint/*Test.qnt - diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index df6b8d3ee..272dfcf45 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -5,9 +5,13 @@ on: branches: main paths: - Code/** + - Specs/Quint/** + - .github/workflows/rust.yml pull_request: paths: - Code/** + - Specs/Quint/** + - .github/workflows/rust.yml env: CARGO_INCREMENTAL: 0 @@ -27,6 +31,10 @@ jobs: steps: - name: Checkout uses: actions/checkout@v4 + - uses: actions/setup-node@v3 + with: + node-version: "18" + - run: npm install -g @informalsystems/quint - name: Setup Rust toolchain uses: actions-rust-lang/setup-rust-toolchain@v1 - name: Install cargo-nextest @@ -51,7 +59,7 @@ jobs: with: token: ${{secrets.GITHUB_TOKEN}} args: --all-features --all-targets --manifest-path Code/Cargo.toml - + fmt: name: Formatting runs-on: ubuntu-latest diff --git a/Code/Cargo.toml b/Code/Cargo.toml index 6ab8f0f25..705510c26 100644 --- a/Code/Cargo.toml +++ b/Code/Cargo.toml @@ -19,10 +19,13 @@ publish = false [workspace.dependencies] async-trait = "0.1" -futures = "0.3" ed25519-consensus = "2.1.0" -itf = "0.1.2" +futures = "0.3" +glob = "0.3.0" +itf = "0.2.1" +num-bigint = "0.4.4" rand = { version = "0.8.5", features = ["std_rng"] } serde = "1.0" +serde_json = "1.0" sha2 = "0.10.8" signature = "2.1.0" diff --git a/Code/common/src/round.rs b/Code/common/src/round.rs index 6bb5cd3d6..db71c456e 100644 --- a/Code/common/src/round.rs +++ b/Code/common/src/round.rs @@ -41,12 +41,12 @@ impl Round { } } - /// Wether the round is defined, ie. `Round::Some(r)` where `r >= 0`. + /// Whether the round is defined, ie. `Round::Some(r)` where `r >= 0`. pub fn is_defined(&self) -> bool { matches!(self, Round::Some(r) if *r >= 0) } - /// Wether the round is `Round::Nil`. + /// Whether the round is `Round::Nil`. pub fn is_nil(&self) -> bool { matches!(self, Round::Nil) } diff --git a/Code/driver/src/util.rs b/Code/driver/src/util.rs index fd71a5915..9428d6f2c 100644 --- a/Code/driver/src/util.rs +++ b/Code/driver/src/util.rs @@ -1,4 +1,4 @@ -/// Wether or not a proposal is valid. +/// Whether or not a proposal is valid. #[derive(Copy, Clone, Debug, PartialEq, Eq)] pub enum Validity { /// The proposal is valid. diff --git a/Code/itf/Cargo.toml b/Code/itf/Cargo.toml index 316394356..b8a977cb8 100644 --- a/Code/itf/Cargo.toml +++ b/Code/itf/Cargo.toml @@ -9,5 +9,15 @@ license.workspace = true publish.workspace = true [dependencies] -itf.workspace = true -serde = { workspace = true, features = ["derive"] } +itf = { workspace = true } +rand = { workspace = true } +malachite-common = { version = "0.1.0", path = "../common" } +malachite-vote = { version = "0.1.0", path = "../vote" } +malachite-test = { version = "0.1.0", path = "../test" } +num-bigint = { workspace = true, features = ["serde"] } +serde = { workspace = true, features = ["derive"] } +serde_json = { workspace = true } +glob = { workspace = true } + +[dev-dependencies] +tempfile = { version = "3.8.1" } diff --git a/Code/itf/src/consensus.rs b/Code/itf/src/consensus.rs index f631e4f45..2bb430b6a 100644 --- a/Code/itf/src/consensus.rs +++ b/Code/itf/src/consensus.rs @@ -1,13 +1,14 @@ -use itf::{ItfBigInt, ItfMap}; +use num_bigint::BigInt; use serde::Deserialize; +use std::collections::HashMap; use crate::deserializers as de; pub type Address = String; pub type Value = String; pub type Step = String; -pub type Round = ItfBigInt; -pub type Height = ItfBigInt; +pub type Round = BigInt; +pub type Height = BigInt; #[derive(Clone, Debug, Deserialize)] pub enum Timeout { @@ -33,7 +34,7 @@ pub struct State { } #[derive(Clone, Debug, Deserialize)] -pub struct System(ItfMap); +pub struct System(HashMap); #[derive(Clone, Debug, Deserialize)] #[serde(tag = "name")] @@ -132,9 +133,9 @@ 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) + && self.height == BigInt::from(-1) + && self.round == BigInt::from(-1) + && self.valid_round == BigInt::from(-1) } } @@ -152,8 +153,8 @@ 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.height == BigInt::from(-1) + && self.round == BigInt::from(-1) && self.step.is_empty() } } diff --git a/Code/itf/src/deserializers.rs b/Code/itf/src/deserializers.rs index 192e39401..53231f40d 100644 --- a/Code/itf/src/deserializers.rs +++ b/Code/itf/src/deserializers.rs @@ -1,4 +1,4 @@ -use itf::ItfBigInt; +use num_bigint::BigInt; use serde::de::IntoDeserializer; use serde::Deserialize; @@ -16,14 +16,14 @@ where } } -pub(crate) fn minus_one_as_none<'de, D>(de: D) -> Result, D::Error> +pub(crate) fn minus_one_as_none<'de, D>(de: D) -> Result, D::Error> where D: serde::Deserializer<'de>, { - let opt = Option::::deserialize(de)?; + let opt = Option::::deserialize(de)?; match opt { None => Ok(None), - Some(i) if i == ItfBigInt::from(-1) => Ok(None), + Some(i) if i == BigInt::from(-1) => Ok(None), Some(i) => Ok(Some(i)), } } diff --git a/Code/itf/src/lib.rs b/Code/itf/src/lib.rs index ce877e0f6..d8bacfb93 100644 --- a/Code/itf/src/lib.rs +++ b/Code/itf/src/lib.rs @@ -2,3 +2,4 @@ pub mod consensus; pub mod votekeeper; mod deserializers; +pub mod utils; diff --git a/Code/itf/src/utils.rs b/Code/itf/src/utils.rs new file mode 100644 index 000000000..c77f99c47 --- /dev/null +++ b/Code/itf/src/utils.rs @@ -0,0 +1,91 @@ +use glob::glob; +use std::path::Path; + +// TODO(rano): simplify this function once quint is fixed +pub fn generate_traces(spec_rel_path: &str, gen_dir: &str, quint_seed: u64) { + let spec_abs_path = format!( + "{}/../../Specs/Quint/{}", + env!("CARGO_MANIFEST_DIR"), + spec_rel_path + ); + + let spec_path = Path::new(&spec_abs_path); + + std::process::Command::new("quint") + .arg("test") + .arg("--output") + .arg(format!("{}/{{}}.itf.json", gen_dir)) + .arg("--seed") + .arg(quint_seed.to_string()) + .arg(spec_path) + .current_dir(spec_path.parent().unwrap()) + .output() + .expect("Failed to run quint test"); + + // Remove traces from imported modules + for redundant_itf in glob(&format!( + "{}/*{}::*.*", + gen_dir, + spec_path.file_stem().unwrap().to_str().unwrap() + )) + .expect("Failed to read glob pattern") + .flatten() + { + std::fs::remove_file(&redundant_itf).unwrap(); + } + + // Rerun quint per tests + // https://github.com/informalsystems/quint/issues/1263 + for itf_json in glob(&format!("{}/*.itf.json", gen_dir,)) + .expect("Failed to read glob pattern") + .flatten() + { + std::fs::remove_file(&itf_json).unwrap(); + + std::process::Command::new("quint") + .arg("test") + .arg("--output") + .arg(format!( + "{}/{}_{{}}.itf.json", + gen_dir, + spec_path.file_stem().unwrap().to_str().unwrap() + )) + .arg("--match") + .arg( + itf_json + .file_name() + .unwrap() + .to_string_lossy() + .strip_suffix(".itf.json") + .unwrap(), + ) + .arg("--seed") + .arg(quint_seed.to_string()) + .arg(spec_path) + .current_dir(spec_path.parent().unwrap()) + .output() + .expect("Failed to run quint test"); + } + + // Remove duplicate states + // https://github.com/informalsystems/quint/issues/1252 + for itf_json in glob(&format!("{}/*.itf.json", gen_dir,)) + .expect("Failed to read glob pattern") + .flatten() + { + let mut json: serde_json::Value = + serde_json::from_reader(std::fs::File::open(&itf_json).unwrap()).unwrap(); + + let states = json["states"].as_array_mut().unwrap(); + states.retain(|state| { + let index = state["#meta"]["index"].as_u64().unwrap(); + index % 2 == 0 + }); + states.iter_mut().enumerate().for_each(|(i, state)| { + state["#meta"]["index"] = serde_json::Value::from(i as u64); + }); + + let mut json_file = std::fs::File::create(&itf_json).unwrap(); + serde_json::to_writer_pretty(&mut json_file, &json).unwrap(); + } +} diff --git a/Code/itf/src/votekeeper.rs b/Code/itf/src/votekeeper.rs index be3fb73ae..933de3137 100644 --- a/Code/itf/src/votekeeper.rs +++ b/Code/itf/src/votekeeper.rs @@ -1,49 +1,76 @@ -use itf::{ItfBigInt, ItfMap, ItfSet}; +use itf::de::{As, Integer, Same}; +use std::collections::{HashMap, HashSet}; + use serde::Deserialize; -pub type Height = ItfBigInt; -pub type Weight = ItfBigInt; -pub type Round = ItfBigInt; +pub type Height = i64; +pub type Weight = i64; +pub type Round = i64; pub type Address = String; pub type Value = String; +pub type VoteType = String; #[derive(Clone, Debug, PartialEq, Eq, Deserialize)] #[serde(rename_all = "camelCase")] pub struct Bookkeeper { + #[serde(with = "As::")] pub height: Height, + #[serde(with = "As::")] pub total_weight: Weight, - pub rounds: ItfMap, + #[serde(with = "As::>")] + pub rounds: HashMap, +} + +#[derive(Clone, Debug, PartialEq, Eq, Deserialize)] +pub struct Vote { + pub typ: VoteType, + #[serde(with = "As::")] + pub height: Height, + #[serde(with = "As::")] + pub round: Round, + pub value: Value, + pub address: Address, } #[derive(Clone, Debug, PartialEq, Eq, Deserialize)] #[serde(rename_all = "camelCase")] pub struct RoundVotes { + #[serde(with = "As::")] pub height: Height, + #[serde(with = "As::")] pub round: Round, pub prevotes: VoteCount, pub precommits: VoteCount, - pub emitted_events: ItfSet, - pub votes_addresses_weights: ItfMap, + pub emitted_events: HashSet, + #[serde(with = "As::>")] + pub votes_addresses_weights: HashMap, } #[derive(Clone, Debug, PartialEq, Eq, Deserialize)] #[serde(rename_all = "camelCase")] pub struct VoteCount { + #[serde(with = "As::")] pub total_weight: Weight, - pub values_weights: ItfMap, - pub votes_addresses: ItfSet
, + #[serde(with = "As::>")] + pub values_weights: HashMap, + pub votes_addresses: HashSet
, } #[derive(Clone, Debug, PartialEq, Eq, Deserialize, Hash)] pub struct ExecutorEvent { + #[serde(with = "As::")] pub round: Round, pub name: String, pub value: Value, } #[derive(Clone, Debug, PartialEq, Eq, Deserialize)] -#[serde(rename_all = "camelCase")] pub struct State { + #[serde(rename = "voteBookkeeperTest::voteBookkeeperSM::bookkeeper")] pub bookkeeper: Bookkeeper, + #[serde(rename = "voteBookkeeperTest::voteBookkeeperSM::lastEmitted")] pub last_emitted: ExecutorEvent, + #[serde(rename = "voteBookkeeperTest::voteBookkeeperSM::weightedVote")] + #[serde(with = "As::<(Same, Integer, Integer)>")] + pub weighted_vote: (Vote, Weight, Round), } diff --git a/Code/itf/tests/consensus.rs b/Code/itf/tests/consensus.rs index 435ec6481..9eac81275 100644 --- a/Code/itf/tests/consensus.rs +++ b/Code/itf/tests/consensus.rs @@ -1,19 +1,16 @@ +use glob::glob; + 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()); +fn test_itf() { + for json_fixture in glob("tests/fixtures/consensus/*.json") + .expect("Failed to read glob pattern") + .flatten() + { + println!("Parsing {json_fixture:?}"); - let json = std::fs::read_to_string(&fixture).unwrap(); + let json = std::fs::read_to_string(&json_fixture).unwrap(); let state = itf::trace_from_str::(&json).unwrap(); dbg!(state); diff --git a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaAnyTest_6.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaAnyTest_6.itf.json deleted file mode 100644 index e766285a1..000000000 --- a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaAnyTest_6.itf.json +++ /dev/null @@ -1 +0,0 @@ -{"#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 deleted file mode 100644 index b5bf98cda..000000000 --- a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaNilTest_7.itf.json +++ /dev/null @@ -1 +0,0 @@ -{"#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 deleted file mode 100644 index 75bc07e59..000000000 --- a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_synchronousConsensusTest_5.itf.json +++ /dev/null @@ -1 +0,0 @@ -{"#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 index 1515d18ec..757bcf7fc 100644 --- a/Code/itf/tests/votekeeper.rs +++ b/Code/itf/tests/votekeeper.rs @@ -1,22 +1,64 @@ +#[path = "votekeeper/runner.rs"] +pub mod runner; +#[path = "votekeeper/utils.rs"] +pub mod utils; + +use glob::glob; +use rand::rngs::StdRng; +use rand::SeedableRng; + +use malachite_itf::utils::generate_traces; use malachite_itf::votekeeper::State; +use malachite_test::{Address, PrivateKey}; + +use runner::VoteKeeperRunner; +use utils::ADDRESSES; + +const RANDOM_SEED: u64 = 0x42; #[test] -fn parse_fixtures() { - // read fixtures files in test/fixtures/votekeeper/ - let folder = format!("{}/tests/fixtures/votekeeper", env!("CARGO_MANIFEST_DIR")); +fn test_itf() { + let temp_dir = tempfile::tempdir().expect("Failed to create temp 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::>(); + let quint_seed = option_env!("QUINT_SEED") + // use inspect when stabilized + .map(|x| { + println!("using QUINT_SEED={}", x); + x + }) + .or(Some("118")) + .and_then(|x| x.parse::().ok()) + .filter(|&x| x != 0) + .expect("invalid random seed for quint"); - for fixture in fixtures { - println!("Parsing '{}'", fixture.display()); + generate_traces( + "voteBookkeeperTest.qnt", + &temp_dir.path().to_string_lossy(), + quint_seed, + ); - let json = std::fs::read_to_string(&fixture).unwrap(); + for json_fixture in glob(&format!("{}/*.itf.json", temp_dir.path().display())) + .expect("Failed to read glob pattern") + .flatten() + { + println!("Parsing {json_fixture:?}"); + + let json = std::fs::read_to_string(&json_fixture).unwrap(); let trace = itf::trace_from_str::(&json).unwrap(); - dbg!(trace); + let mut rng = StdRng::seed_from_u64(RANDOM_SEED); + + // build mapping from model addresses to real addresses + let vote_keeper_runner = VoteKeeperRunner { + address_map: ADDRESSES + .iter() + .map(|&name| { + let pk = PrivateKey::generate(&mut rng).public_key(); + (name.into(), Address::from_public_key(&pk)) + }) + .collect(), + }; + + trace.run_on(vote_keeper_runner).unwrap(); } } diff --git a/Code/itf/tests/votekeeper/runner.rs b/Code/itf/tests/votekeeper/runner.rs new file mode 100644 index 000000000..482186b7f --- /dev/null +++ b/Code/itf/tests/votekeeper/runner.rs @@ -0,0 +1,183 @@ +use std::collections::HashMap; + +use malachite_common::{Context, Round, Value}; +use malachite_itf::votekeeper::State; +use malachite_test::{Address, Height, TestContext, Vote}; +use malachite_vote::{ + keeper::{Message, VoteKeeper}, + ThresholdParams, +}; + +use itf::Runner as ItfRunner; + +use super::utils::{check_votes, value_from_model}; + +pub struct VoteKeeperRunner { + pub address_map: HashMap, +} + +impl ItfRunner for VoteKeeperRunner { + type ActualState = VoteKeeper; + type Result = Option::Value as Value>::Id>>; + type ExpectedState = State; + type Error = (); + + fn init(&mut self, expected: &Self::ExpectedState) -> Result { + // Initialize VoteKeeper from the initial total_weight from the first state in the model. + let (input_vote, weight, current_round) = &expected.weighted_vote; + let round = Round::new(input_vote.round); + println!( + "🔵 init: vote={:?}, round={:?}, value={:?}, address={:?}, weight={:?}, current_round={:?}", + input_vote.typ, round, input_vote.value, input_vote.address, weight, current_round + ); + Ok(VoteKeeper::new( + expected.bookkeeper.total_weight as u64, + ThresholdParams::default(), + )) + } + + fn step( + &mut self, + actual: &mut Self::ActualState, + expected: &Self::ExpectedState, + ) -> Result { + // Build step to execute. + let (input_vote, weight, current_round) = &expected.weighted_vote; + let round = Round::new(input_vote.round); + let height = Height::new(input_vote.height as u64); + let value = value_from_model(&input_vote.value); + let address = self.address_map.get(input_vote.address.as_str()).unwrap(); + let vote = match input_vote.typ.as_str() { + "Prevote" => Vote::new_prevote(height, round, value, *address), + "Precommit" => Vote::new_precommit(height, round, value, *address), + _ => unreachable!(), + }; + println!( + "🔵 step: vote={:?}, round={:?}, value={:?}, address={:?}, weight={:?}, current_round={:?}", + input_vote.typ, round, value, input_vote.address, weight, current_round + ); + + // Execute step. + Ok(actual.apply_vote(vote, *weight as u64, Round::new(*current_round))) + } + + fn result_invariant( + &self, + result: &Self::Result, + expected: &Self::ExpectedState, + ) -> Result { + // Get expected result. + let expected_result = &expected.last_emitted; + println!( + "🟣 result: model={:?}({:?},{:?}), code={:?}", + expected_result.name, expected_result.value, expected_result.round, result + ); + // Check result against expected result. + match result { + Some(result) => match result { + Message::PolkaValue(value) => { + assert_eq!(expected_result.name, "PolkaValue"); + assert_eq!( + value_from_model(&expected_result.value).as_ref(), + Some(value) + ); + } + Message::PrecommitValue(value) => { + assert_eq!(expected_result.name, "PrecommitValue"); + assert_eq!( + value_from_model(&expected_result.value).as_ref(), + Some(value) + ); + } + Message::SkipRound(round) => { + assert_eq!(expected_result.name, "Skip"); + assert_eq!(&Round::new(expected_result.round), round); + } + msg => assert_eq!(expected_result.name, format!("{msg:?}")), + }, + None => assert_eq!(expected_result.name, "None"), + } + Ok(true) + } + + fn state_invariant( + &self, + actual: &Self::ActualState, + expected: &Self::ExpectedState, + ) -> Result { + // doesn't check for current Height and Round + + let actual_state = actual; + let expected_state = &expected.bookkeeper; + + assert_eq!( + actual_state.total_weight(), + &(expected_state.total_weight as u64), + "total_weight for the current height" + ); + + assert_eq!(actual_state.per_round().len(), expected_state.rounds.len()); + + for (&round, expected_round) in &expected_state.rounds { + // doesn't check for current Height and Round + + let actual_round = actual_state.per_round().get(&Round::new(round)).unwrap(); + + let expected_events = &expected_round.emitted_events; + let actual_events = actual_round.emitted_msgs(); + + assert_eq!( + actual_events.len(), + expected_events.len(), + "number of emitted events" + ); + + let mut event_count = HashMap::new(); + + for event in expected_events { + let count = event_count.entry(event.name.clone()).or_insert(0); + *count += 1; + } + + for event in actual_events { + let event_name = match event { + Message::PolkaValue(_) => "PolkaValue".into(), + Message::PrecommitValue(_) => "PrecommitValue".into(), + Message::SkipRound(_) => "Skip".into(), + _ => format!("{event:?}"), + }; + let count = event_count.entry(event_name.clone()).or_insert(0); + *count -= 1; + } + + for (event_name, count) in event_count { + assert_eq!(count, 0, "event {event_name:?} not matched"); + } + + let expected_addresses_weights = &expected_round.votes_addresses_weights; + let actual_addresses_weights = &actual_round.addresses_weights().get_inner(); + for address in expected_addresses_weights.keys() { + assert_eq!( + actual_addresses_weights.get(self.address_map.get(address).unwrap()), + expected_addresses_weights + .get(address) + .map(|&w| w as u64) + .as_ref(), + "weight for address {address:?}" + ); + } + + let actual_votes = &actual_round.votes(); + + let expected_prevotes = &expected_round.prevotes; + let actual_prevotes = actual_votes.prevotes(); + check_votes(expected_prevotes, actual_prevotes, &self.address_map); + + let expected_precommits = &expected_round.precommits; + let actual_precommits = actual_votes.precommits(); + check_votes(expected_precommits, actual_precommits, &self.address_map); + } + + Ok(true) + } +} diff --git a/Code/itf/tests/votekeeper/utils.rs b/Code/itf/tests/votekeeper/utils.rs new file mode 100644 index 000000000..91504697d --- /dev/null +++ b/Code/itf/tests/votekeeper/utils.rs @@ -0,0 +1,55 @@ +use std::collections::HashMap; + +use malachite_itf::votekeeper::Value; +use malachite_test::{Address, ValueId}; + +pub const ADDRESSES: [&str; 3] = ["alice", "bob", "john"]; +pub const NIL_VALUE: &str = "nil"; + +pub fn value_from_model(value: &Value) -> Option { + match value.as_str() { + NIL_VALUE => None, + "proposal" => Some(0.into()), + "val1" => Some(1.into()), + "val2" => Some(2.into()), + "val3" => Some(3.into()), + _ => unimplemented!("unknown value {value:?}"), + } +} + +pub fn check_votes( + expected: &malachite_itf::votekeeper::VoteCount, + actual: &malachite_vote::count::VoteCount, + address_map: &HashMap, +) { + // expected has `total_weight` which is not present in actual + + let expected_values_weights = &expected.values_weights; + let actual_values_weights = &actual.values_weights; + + // should check length too + + for value in expected_values_weights.keys() { + assert_eq!( + actual_values_weights.get(&value_from_model(value)), + *expected_values_weights.get(value).unwrap() as u64, + "weight for value {value:?}" + ); + } + + let expected_votes_addresses = &expected.votes_addresses; + let actual_votes_addresses = &actual.validator_addresses; + + assert_eq!( + actual_votes_addresses.len(), + expected_votes_addresses.len(), + "number of voted addresses" + ); + + for address in expected_votes_addresses { + assert!( + actual_votes_addresses.contains(address_map.get(address).unwrap()), + "address {address:?} not voted" + ); + } +} diff --git a/Code/round/src/events.rs b/Code/round/src/events.rs index 7954ac59c..0ea71c90f 100644 --- a/Code/round/src/events.rs +++ b/Code/round/src/events.rs @@ -9,8 +9,8 @@ where ProposeValue(Ctx::Value), // Propose a value.L14 Proposal(Ctx::Proposal), // Receive a proposal. L22 + L23 (valid) InvalidProposal, // Receive an invalid proposal. L26 + L32 (invalid) - ProposalAndPolkaPrevious(Ctx::Proposal), // Recieved a proposal and a polka value from a previous round. L28 + L29 (valid) - InvalidProposalAndPolkaPrevious(Ctx::Proposal), // Recieved a proposal and a polka value from a previous round. L28 + L29 (invalid) + ProposalAndPolkaPrevious(Ctx::Proposal), // Received a proposal and a polka value from a previous round. L28 + L29 (valid) + InvalidProposalAndPolkaPrevious(Ctx::Proposal), // Received a proposal and a polka value from a previous round. L28 + L29 (invalid) PolkaValue(ValueId), // Receive +2/3 prevotes for valueId. L44 PolkaAny, // Receive +2/3 prevotes for anything. L34 PolkaNil, // Receive +2/3 prevotes for nil. L44 diff --git a/Code/round/src/state_machine.rs b/Code/round/src/state_machine.rs index f525c1303..a34346f60 100644 --- a/Code/round/src/state_machine.rs +++ b/Code/round/src/state_machine.rs @@ -114,7 +114,7 @@ where // We are the proposer. (Step::Propose, Event::TimeoutPropose) if this_round && info.is_proposer() => { - // TOOD: Do we need to do something else here? + // TODO: Do we need to do something else here? prevote_nil(state, info.address) // L57 } // We are not the proposer. diff --git a/Code/vote/src/keeper.rs b/Code/vote/src/keeper.rs index a0e21fe25..16864e06d 100644 --- a/Code/vote/src/keeper.rs +++ b/Code/vote/src/keeper.rs @@ -19,7 +19,7 @@ pub enum Message { SkipRound(Round), } -struct PerRound +pub struct PerRound where Ctx: Context, { @@ -39,6 +39,18 @@ where emitted_msgs: BTreeSet::new(), } } + + pub fn votes(&self) -> &RoundVotes> { + &self.votes + } + + pub fn addresses_weights(&self) -> &RoundWeights { + &self.addresses_weights + } + + pub fn emitted_msgs(&self) -> &BTreeSet>> { + &self.emitted_msgs + } } impl Clone for PerRound @@ -91,6 +103,14 @@ where } } + pub fn total_weight(&self) -> &Weight { + &self.total_weight + } + + pub fn per_round(&self) -> &BTreeMap> { + &self.per_round + } + /// Apply a vote with a given weight, potentially triggering an event. pub fn apply_vote( &mut self, diff --git a/Code/vote/src/round_votes.rs b/Code/vote/src/round_votes.rs index 58307b597..c54aab7f0 100644 --- a/Code/vote/src/round_votes.rs +++ b/Code/vote/src/round_votes.rs @@ -18,6 +18,14 @@ impl RoundVotes { } } + pub fn prevotes(&self) -> &VoteCount { + &self.prevotes + } + + pub fn precommits(&self) -> &VoteCount { + &self.precommits + } + pub fn add_vote( &mut self, vote_type: VoteType, diff --git a/Code/vote/src/round_weights.rs b/Code/vote/src/round_weights.rs index 63213782d..77c3396aa 100644 --- a/Code/vote/src/round_weights.rs +++ b/Code/vote/src/round_weights.rs @@ -14,6 +14,10 @@ impl
RoundWeights
{ } } + pub fn get_inner(&self) -> &BTreeMap { + &self.map + } + pub fn set_once(&mut self, address: Address, weight: Weight) where Address: Ord, diff --git a/Docs/architecture/adr-template.md b/Docs/architecture/adr-template.md index 28a5ecfbb..83d323eee 100644 --- a/Docs/architecture/adr-template.md +++ b/Docs/architecture/adr-template.md @@ -31,6 +31,6 @@ If the proposed change will be large, please also indicate a way to do the chang ## References -> Are there any relevant PR comments, issues that led up to this, or articles referrenced for why we made the given design choice? If so link them here! +> Are there any relevant PR comments, issues that led up to this, or articles referenced for why we made the given design choice? If so link them here! * {reference link} diff --git a/Specs/Quint/.gitignore b/Specs/Quint/.gitignore new file mode 100644 index 000000000..efaa2423b --- /dev/null +++ b/Specs/Quint/.gitignore @@ -0,0 +1,2 @@ +traces/ +_apalache-out/ diff --git a/Specs/Quint/Makefile b/Specs/Quint/Makefile new file mode 100644 index 000000000..2b9227986 --- /dev/null +++ b/Specs/Quint/Makefile @@ -0,0 +1,43 @@ +parse: + npx @informalsystems/quint parse asyncModelsTest.qnt + npx @informalsystems/quint parse consensusTest.qnt + npx @informalsystems/quint parse executor.qnt + npx @informalsystems/quint parse statemachineTest.qnt + npx @informalsystems/quint parse voteBookkeeperTest.qnt +.PHONY: parse + +test-con: + npx @informalsystems/quint run consensusTest.qnt +.PHONY: test-con + +test-sm: + npx @informalsystems/quint test statemachineTest.qnt +.PHONY: test-sm + +test-vk: + npx @informalsystems/quint test voteBookkeeperTest.qnt +.PHONY: test-vk + +test: test-con test-sm test-vk +.PHONY: test + +verify: + npx @informalsystems/quint verify --max-steps 10 --invariant Inv voteBookkeeperTest.qnt +.PHONY: verify + +# Generate traces by random simulation from properties describing the last desired state. +traces-sim: + ./scripts/gen-traces.sh voteBookkeeperTest.qnt emitPrecommitValue 30 + ./scripts/gen-traces.sh voteBookkeeperTest.qnt emitPolkaAny 30 + ./scripts/gen-traces.sh voteBookkeeperTest.qnt emitPolkaNil 30 + ./scripts/gen-traces.sh voteBookkeeperTest.qnt emitSkip 30 +.PHONY: traces-sim + +# Generate traces from `run` statements. +traces-run: + mkdir -p traces/votekeeper + npx @informalsystems/quint test --output traces/votekeeper/{}.itf.json voteBookkeeperTest.qnt +.PHONY: traces-run + +traces: traces-sim traces-run +.PHONY: traces diff --git a/Specs/Quint/executor.qnt b/Specs/Quint/executor.qnt index 1a671d071..6aeb71a6a 100644 --- a/Specs/Quint/executor.qnt +++ b/Specs/Quint/executor.qnt @@ -78,7 +78,7 @@ val defaultInput: ExecutorInput = { // 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 } + { typ: v.step, height: v.height, round: v.round, value: v.id, address: v.src } val defaultEvent : Event = { name : "", height : 0, round: 0, value: "", vr: 0 } diff --git a/Specs/Quint/extraSpells.qnt b/Specs/Quint/extraSpells.qnt index a0fb9b7cc..0400dfda0 100644 --- a/Specs/Quint/extraSpells.qnt +++ b/Specs/Quint/extraSpells.qnt @@ -188,7 +188,7 @@ module extraSpells { /// /// - @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 = + pure def mapSumValues(__map: a -> int): int = __map.keys().fold(0, (__acc, __val) => __acc + __map.get(__val)) run mapSumValuesTest = all { @@ -196,4 +196,13 @@ module extraSpells { assert(6 == Map("a" -> 0, "b" -> 1, "c" -> 2, "d" -> 3).mapSumValues()), } + /// True iff all (key, value) pairs in the map satisfy the given predicate. + pure def forallEntries(__map: a -> b, __f: (a, b) => bool): bool = + __map.keys().forall(__key => __f(__key, __map.get(__key))) + + + /// True iff all values in the map satisfy the given predicate. + pure def forallValues(__map: a -> b, __f: b => bool): bool = + __map.keys().forall(__key => __f(__map.get(__key))) + } \ No newline at end of file diff --git a/Specs/Quint/scripts/gen-traces.sh b/Specs/Quint/scripts/gen-traces.sh new file mode 100755 index 000000000..3f8debe4b --- /dev/null +++ b/Specs/Quint/scripts/gen-traces.sh @@ -0,0 +1,62 @@ +#!/usr/bin/env bash + +BLUE=$(tput setaf 4) +RED=$(tput setaf 1) +RESET=$(tput sgr0) + +# [INFO] message in blue +info() +{ + echo "${BLUE}[INFO] $*${RESET}" +} + +# [ERROR] message in red +error() +{ + echo "${RED}[ERROR] $*${RESET} " +} + +FILEPATH=$1 +PROP=$2 +MAX_STEPS=${3:-100} +[[ ! -f "$FILEPATH" ]] && error "file $FILEPATH does not exist" && exit 1 +[[ -z "$PROP" ]] && error "property name required" && exit 1 + +MODULE=$(basename ${FILEPATH%".qnt"}) +TRACES_DIR="traces/$MODULE" +mkdir -p "$TRACES_DIR" + +# Given dir, name and ext, if "dir/name-N.ext" exists, it will return +# "dir/name-M.ext" with M=N+1, otherwise it will return "dir/name-1.ext". +function nextFilename() { + local dir=$1 + local name=$2 + local ext=$3 + local result="$dir/$name.$ext" + if [ -f $result ]; then + i=1 + result="$dir/$name-$i.$ext" + while [[ -e "$result" || -L "$result" ]] ; do + result="$dir/$name-$((i+1)).$ext" + done + fi + echo "$result" +} + +TRACE_PATH=$(nextFilename "$TRACES_DIR" "$PROP" "itf.json") +OUTPUT=$(npx @informalsystems/quint run \ + --max-steps=$MAX_STEPS \ + --max-samples=1 \ + --invariant "$PROP" \ + --out-itf "$TRACE_PATH" \ + "$FILEPATH" 2>&1) +case $OUTPUT in + "error: Invariant violated") + # info "Success: reached a state that violates $FILEPATH::$PROP" + info "Generated trace: $TRACE_PATH" + ;; + *) + error "Failed: did not find a state that violates $FILEPATH::$PROP in $MAX_STEPS steps" + [ -f $TRACE_PATH ] && info "Generated trace: $TRACE_PATH" + ;; +esac diff --git a/Specs/Quint/voteBookkeeper.qnt b/Specs/Quint/voteBookkeeper.qnt index cde151a75..3e9bca343 100644 --- a/Specs/Quint/voteBookkeeper.qnt +++ b/Specs/Quint/voteBookkeeper.qnt @@ -9,34 +9,40 @@ module voteBookkeeper { // Types // **************************************************************************** - // An address is an string + // Node address type Address = str - // A round is an integer + // Round in the Tendermint algorithm type Round = int - // A height is an integer + // Height in the Tendermint algorithm type Height = int - // A value is a string + // Value proposed and voted to be included in the chain type Value = str + val Nil: Value = "nil" // a special value of type Value - // Weight is an integer + // The stake of a node type Weight = int type VoteType = str + val VoteTypes: Set[VoteType] = Set("Prevote", "Precommit") + def isPrevote(voteType) = voteType == "Prevote" + def isPrecommit(voteType) = voteType == "Precommit" type Vote = { typ: VoteType, + height: Height, round: Round, value: Value, address: Address } + type WeightedVote = (Vote, Weight, Round) + type VoteCount = { totalWeight: Weight, - // includes nil - valuesWeights: Value -> Weight, + valuesWeights: Value -> Weight, // including the "nil" value votesAddresses: Set[Address] } @@ -53,12 +59,25 @@ module voteBookkeeper { name: str, value: Value } + val unreachedThreshold = { name: "Unreached", value: "null" } + val nilThreshold = { name: "Nil", value: "null" } + val anyThreshold = { name: "Any", value: "null" } + val skipThreshold = { name: "Skip", value: "null" } + pure def valueThreshold(value) = { name: "Value", value: value } + pure def isThresholdOnValue(t: Threshold): bool = t.name == "Value" type ExecutorEvent = { round: Round, name: str, value: Value } + pure def noEvent(round) = { round: round, name: "None", value: "null" } + pure def polkaValueEvent(round, value) = { round: round, name: "PolkaValue", value: value } + pure def polkaNilEvent(round) = { round: round, name: "PolkaNil", value: "null" } + pure def polkaAnyEvent(round) = { round: round, name: "PolkaAny", value: "null" } + pure def precommitValueEvent(round, value) = { round: round, name: "PrecommitValue", value: value } + pure def precommitAnyEvent(round) = { round: round, name: "PrecommitAny", value: "null" } + pure def skipEvent(round) = { round: round, name: "Skip", value: "null" } type Bookkeeper = { height: Height, @@ -72,6 +91,15 @@ module voteBookkeeper { // Internal functions + pure def newRoundVotes(height: Height, round: Round, totalWeight: Weight): RoundVotes = { + height: height, + round: round, + prevotes: newVoteCount(totalWeight), + precommits: newVoteCount(totalWeight), + emittedEvents: Set(), + votesAddressesWeights: Map() + } + // creates a new voteCount pure def newVoteCount(total: Weight): VoteCount = { totalWeight: total, valuesWeights: Map(), votesAddresses: Set() } @@ -80,10 +108,21 @@ module voteBookkeeper { pure def isQuorum(weight: Weight, total: Weight): bool = 3 * weight > 2 * total + run isQuorumTest = all { + assert(isQuorum(0,0) == false), + assert(isQuorum(2,6) == false), + assert(isQuorum(4,6) == false), + assert(isQuorum(5,6) == true), + } + // 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 value nil. + pure def hasQuorumOnNil(voteCount: VoteCount): bool = + hasQuorumOnValue(voteCount, Nil) + // True iff the vote count has a quorum on any value. pure def hasQuorumOnAny(voteCount: VoteCount): bool = isQuorum(voteCount.valuesWeights.mapSumValues(), voteCount.totalWeight) @@ -92,7 +131,13 @@ module voteBookkeeper { 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. + run isSkipTest = all { + assert(isSkip(0,0) == false), + assert(isSkip(2,6) == false), + assert(isSkip(3,6) == true), + } + + // Adds a weighted vote to a voteCount if there is no vote registered for the voter. 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. @@ -103,76 +148,109 @@ module voteBookkeeper { .with("valuesWeights", voteCount.valuesWeights.mapSafeSet(vote.value, newWeight)) .with("votesAddresses", voteCount.votesAddresses.setAdd(vote.address)) + run addVoteTest = + val voteCount = { + totalWeight: 100, + valuesWeights: Map("val1" -> 30, "val2" -> 20), + votesAddresses: Set("alice", "bob") + } + val vote = { typ: "Precommit", height: 1, round: 10, value: "val3", address: "john" } + all { + // new voter, new value + assert(addVote(voteCount, vote, 10) == { + totalWeight: 100, + valuesWeights: Map("val1" -> 30, "val2" -> 20, "val3" -> 10), + votesAddresses: Set("alice", "bob", "john") + }), + // new voter, existing value + assert(addVote(voteCount, vote.with("value", "val2"), 10) == { + totalWeight: 100, + valuesWeights: Map("val1" -> 30, "val2" -> 30), + votesAddresses: Set("alice", "bob", "john") + }), + // existing voter + assert(addVote(voteCount, vote.with("address", "alice"), 10) == voteCount), + } + // 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 Any if there is no quorum for the value or nil and there is a quorum for any (including nil); // - A threshold Unreached otherwise indicating that no quorum has been yet reached. pure def computeThreshold(voteCount: VoteCount, value: Value): Threshold = if (voteCount.hasQuorumOnValue(value)) { - if (value == "nil") - { name: "Nil", value: "null" } + if (value == Nil) + nilThreshold else - { name: "Value", value: value } + valueThreshold(value) } else if (voteCount.hasQuorumOnAny()) { - { name: "Any", value: "null" } + anyThreshold } else - { name: "Unreached", value: "null" } + unreachedThreshold // 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" } + if (threshold == unreachedThreshold) + noEvent(round) // 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" } + else if (voteType.isPrevote() and threshold.isThresholdOnValue()) + polkaValueEvent(round, threshold.value) + else if (voteType.isPrevote() and threshold == nilThreshold) + polkaNilEvent(round) + else if (voteType.isPrevote() and threshold == anyThreshold) + polkaAnyEvent(round) // 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 if (voteType.isPrecommit() and threshold.isThresholdOnValue()) + precommitValueEvent(round, threshold.value) + else if (voteType.isPrecommit() and threshold.in(Set(anyThreshold, nilThreshold))) + precommitAnyEvent(round) + + else if (threshold == skipThreshold) + skipEvent(round) else - { round: round, name: "None", value: "null" } + noEvent(round) + + run toEventTest = + val round = 10 + all { + assert(toEvent(round, "Prevote", unreachedThreshold) == noEvent(round)), + assert(toEvent(round, "Precommit", unreachedThreshold) == noEvent(round)), + + assert(toEvent(round, "Prevote", anyThreshold) == polkaAnyEvent(round)), + assert(toEvent(round, "Prevote", nilThreshold) == polkaNilEvent(round)), + assert(toEvent(round, "Prevote", valueThreshold("val1")) == polkaValueEvent(round, "val1")), + + assert(toEvent(round, "Precommit", anyThreshold) == precommitAnyEvent(round)), + assert(toEvent(round, "Precommit", nilThreshold) == precommitAnyEvent(round)), + assert(toEvent(round, "Precommit", valueThreshold("val1")) == precommitValueEvent(round, "val1")), + + assert(toEvent(round, "Prevote", skipThreshold) == skipEvent(round)), + assert(toEvent(round, "Precommit", skipThreshold) == skipEvent(round)), + + assert(toEvent(round, "Precommit", { name: "Error", value: "null" }) == noEvent(round)), + assert(toEvent(round, "Error", anyThreshold) == noEvent(round)), + } // Executor interface type BKResult = { bookkeeper: Bookkeeper, event: ExecutorEvent } // 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. + // - If there exist a threshold and has not emitted before, the function returns the corresponding ExecutorEvent. // - Otherwise, the function returns a no-threshold event. // - Note that if there is no threshold after adding the vote, the function checks if there is a skip threshold. // TO DISCUSS: // - There might be a problem if we generalize from single-shot to multi-shot: the keeper only keeps the totalWeight // of the current height; I wonder if we need to keep the totalWeight for every Height that we may receive a vote for. pure def applyVote(keeper: Bookkeeper, vote: Vote, weight: Weight, currentRound: Round): { bookkeeper: Bookkeeper, event: ExecutorEvent } = - val height = keeper.height - val total = keeper.totalWeight - - 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 round = vote.round + val roundVotes = keeper.rounds.getOrElse(round, newRoundVotes(keeper.height, round, keeper.totalWeight)) val updatedVoteCount = - if (vote.typ == "Prevote") + if (vote.typ.isPrevote()) roundVotes.prevotes.addVote(vote, weight) else roundVotes.precommits.addVote(vote, weight) @@ -183,40 +261,57 @@ module voteBookkeeper { 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 > currentRound and isSkip(combinedWeight, total)) - { round: vote.round, name: "Skip", value: "null" } + if (vote.round > currentRound and isSkip(combinedWeight, keeper.totalWeight)) + skipEvent(vote.round) 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") + noEvent(vote.round) + val updatedRoundVotes = + if (vote.typ.isPrevote()) + roundVotes.with("prevotes", updatedVoteCount) + else + roundVotes.with("precommits", updatedVoteCount) val updatedRoundVotes2 = updatedRoundVotes - .with("votesAddressesWeights", updatedVotesAddressesWeights) - .with("emittedEvents", updatedEmittedEvents) - - val newBookkeeper = - keeper.with("rounds", keeper.rounds.mapSafeSet(vote.round, updatedRoundVotes2)) - - { - bookkeeper: newBookkeeper, - event: finalEvent + .with("votesAddressesWeights", updatedVotesAddressesWeights) + .with("emittedEvents", roundVotes.emittedEvents.setAddIf(finalEvent, finalEvent.name != "None")) + + val updatedBookkeeper = keeper + .with("rounds", keeper.rounds.mapSafeSet(vote.round, updatedRoundVotes2)) + + { bookkeeper: updatedBookkeeper, event: finalEvent } + + run applyVoteTest = + val roundVotes: RoundVotes = { + height: 0, + round: 0, + prevotes: { totalWeight: 4, votesAddresses: Set(), valuesWeights: Map("v1" -> 1, Nil -> 3) }, + precommits: { totalWeight: 4, votesAddresses: Set(), valuesWeights: Map() }, + emittedEvents: Set(), + votesAddressesWeights: Map(), } - + val vk: Bookkeeper = { height: 0, totalWeight: 4, rounds: Map(0 -> roundVotes) } + val o1 = applyVote(vk, { height: 0, round: 0, address: "a0", typ: "Precommit", value: Nil }, 1, 0) + val o2 = applyVote(o1.bookkeeper, { height: 0, round: 0, address: "a1", typ: "Precommit", value: Nil }, 1, 0) + val o3 = applyVote(o2.bookkeeper, { height: 0, round: 0, address: "a2", typ: "Precommit", value: Nil }, 1, 0) + val o4 = applyVote(o3.bookkeeper, { height: 0, round: 0, address: "a3", typ: "Precommit", value: Nil }, 1, 0) + val o5 = applyVote(o4.bookkeeper, { height: 0, round: 1, address: "a4", typ: "Precommit", value: Nil }, 3, 0) + all { + assert(o1.event.name == "None"), + assert(o2.event.name == "None"), + assert(o3.event.name == "PrecommitAny"), + assert(o4.event.name == "None"), + assert(o5.event.name == "Skip"), + } + // 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 @@ -225,108 +320,92 @@ module voteBookkeeper { 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 - 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 + val voteCount = if (voteType.isPrevote()) roundVotes.prevotes else roundVotes.precommits + checkThresholdOnVoteCount(threshold, voteCount) } 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") -// } -// } + pure def checkThresholdOnVoteCount(threshold: Threshold, voteCount: VoteCount): bool = + if (threshold.isThresholdOnValue()) + voteCount.hasQuorumOnValue(threshold.value) + else if (threshold == nilThreshold) + voteCount.hasQuorumOnNil() + else if (threshold == anyThreshold) + voteCount.hasQuorumOnAny() + else false - // **************************************************************************** - // Unit tests - // **************************************************************************** + 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") == unreachedThreshold), + assert(computeThreshold(voteCount.with("valuesWeights", mapValueReached), "val1") == valueThreshold("val1")), + assert(computeThreshold(voteCount.with("valuesWeights", mapValueReached), "val2") == anyThreshold), + assert(computeThreshold(voteCount.with("valuesWeights", mapNilReached), Nil) == nilThreshold), + assert(computeThreshold(voteCount.with("valuesWeights", mapNilReached), "val2") == anyThreshold), + assert(computeThreshold(voteCount.with("valuesWeights", mapNoneReached), "val1") == unreachedThreshold), + assert(computeThreshold(voteCount.with("valuesWeights", mapNoneReached), Nil) == unreachedThreshold), + } - run isQuorumTest = all { - assert(isQuorum(0,0) == false), - assert(isQuorum(2,6) == false), - assert(isQuorum(4,6) == false), - assert(isQuorum(5,6) == true) - } + // ************************************************************************ + // Properties/Invariants + // ************************************************************************ - run isSkipTest = all { - assert(isSkip(0,0) == false), - assert(isSkip(2,6) == false), - assert(isSkip(3,6) == true) + // Each weight in a voteCount is less or equal than the total weight. + def voteValidWeightInv(voteCount) = + voteCount.valuesWeights.forallValues(weight => weight <= voteCount.totalWeight) + + // The sum of all weights is less or equal than the total weight. + def voteValidWeightSumInv(voteCount: VoteCount): bool = + voteCount.valuesWeights.mapSumValues() <= voteCount.totalWeight + + def roundVotesInv(rounds: Round -> RoundVotes): bool = + rounds.forallEntries((round, roundVotes) => all { + voteValidWeightInv(roundVotes.prevotes), + voteValidWeightInv(roundVotes.precommits), + voteValidWeightSumInv(roundVotes.prevotes), + voteValidWeightSumInv(roundVotes.precommits), + }) + + def Inv = all { + roundVotesInv(bookkeeper.rounds) } - 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 { - // new voter, new value - assert(addVote(voteCount, vote, 10) == {totalWeight: 100, valuesWeights: Map("val1" -> 30, "val2" -> 20, "val3" -> 10), votesAddresses: Set("alice", "bob", "john")}), - // new voter, existing value - assert(addVote(voteCount, vote.with("value", "val2"), 10) == {totalWeight: 100, valuesWeights: Map("val1" -> 30, "val2" -> 30), votesAddresses: Set("alice", "bob", "john")}), - // existing voter - assert(addVote(voteCount, vote.with("address", "alice"), 10) == voteCount), - } + // ************************************************************************ + // State + // ************************************************************************ + + // The value used as parameter on each action taken. + var weightedVote: WeightedVote + // The state of the Bookkeeper. + var bookkeeper: Bookkeeper + // The event resulting from applying a weighted vote to the bookkeeper. + var lastEmitted: ExecutorEvent + + // ************************************************************************ + // Actions + // ************************************************************************ + + action allUnchanged: bool = all { + weightedVote' = weightedVote, + bookkeeper' = bookkeeper, + lastEmitted' = lastEmitted, + } - 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"}), - assert(computeThreshold(voteCount.with("valuesWeights", mapValueReached), "val2") == {name: "Any", value: "null"}), - assert(computeThreshold(voteCount.with("valuesWeights", mapNilReached), "nil") == {name: "Nil", value: "null"}), - assert(computeThreshold(voteCount.with("valuesWeights", mapNilReached), "val2") == {name: "Any", value: "null"}), - assert(computeThreshold(voteCount.with("valuesWeights", mapNoneReached), "val1") == {name: "Unreached", value: "null"}), - assert(computeThreshold(voteCount.with("valuesWeights", mapNoneReached), "nil") == {name: "Unreached", value: "null"}), - } + action initWith(initialHeight: Height, totalWeight: Weight): bool = all { + weightedVote' = ({ typ: "", height: initialHeight, round: -1, value: "", address: "" }, -1, -1), + bookkeeper' = { height: initialHeight, totalWeight: totalWeight, rounds: Map() }, + lastEmitted' = { round: -1, name: "", value: "null" } + } - run toEventTest = - val thresholdUnreached = {name: "Unreached", value: "null"} - val thresholdAny = {name: "Any", value: "null"} - val thresholdNil = {name: "Nil", value: "null"} - val thresholdValue = {name: "Value", value: "val1"} - val thresholdSkip = {name: "Skip", value: "null"} - val round = 10 + // The vote keeper receives a weighted vote and produces an event. + action applyVoteAction(vote: Vote, weight: Weight, currentRound: Round): bool = + val result = applyVote(bookkeeper, vote, weight, currentRound) all { - assert(toEvent(round, "Prevote", thresholdUnreached) == {round: round, name: "None", value: "null"}), - assert(toEvent(round, "Precommit", thresholdUnreached) == {round: round, name: "None", value: "null"}), - assert(toEvent(round, "Prevote", thresholdAny) == {round: round, name: "PolkaAny", value: "null"}), - 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: "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"}), + weightedVote' = (vote, weight, currentRound), + bookkeeper' = result.bookkeeper, + lastEmitted' = result.event } } - diff --git a/Specs/Quint/voteBookkeeperSM.qnt b/Specs/Quint/voteBookkeeperSM.qnt new file mode 100644 index 000000000..e52921c48 --- /dev/null +++ b/Specs/Quint/voteBookkeeperSM.qnt @@ -0,0 +1,36 @@ +// **************************************************************************** +// Vote Bookkeeper State machine +// **************************************************************************** + +module voteBookkeeperSM { + + import voteBookkeeper.* from "./voteBookkeeper" + export voteBookkeeper.* + + // ************************************************************************ + // Model parameters + // ************************************************************************ + + const INITIAL_HEIGHT: Height + const INITIAL_TOTAL_WEIGHT: Weight + const ADDRESS_WEIGHTS: Address -> Weight // an address has a constant weight during a height + const ROUNDS: Set[Round] + const VALUES: Set[Value] + + // ************************************************************************ + // State machine + // ************************************************************************ + + action init = + initWith(INITIAL_HEIGHT, INITIAL_TOTAL_WEIGHT) + + action step = + nondet voteType = oneOf(VoteTypes) + nondet round = oneOf(ROUNDS) + nondet value = oneOf(VALUES.union(Set(Nil))) + nondet address = oneOf(ADDRESS_WEIGHTS.keys()) + val height = INITIAL_HEIGHT + val vote: Vote = { typ: voteType, height: height, round: round, value: value, address: address } + applyVoteAction(vote, ADDRESS_WEIGHTS.get(address), 1) + +} diff --git a/Specs/Quint/voteBookkeeperTest.qnt b/Specs/Quint/voteBookkeeperTest.qnt index 4541bb798..44419ca27 100644 --- a/Specs/Quint/voteBookkeeperTest.qnt +++ b/Specs/Quint/voteBookkeeperTest.qnt @@ -1,143 +1,134 @@ module voteBookkeeperTest { - import voteBookkeeper.* from "./voteBookkeeper" + import voteBookkeeperSM( + INITIAL_HEIGHT = 1, + INITIAL_TOTAL_WEIGHT = 100, + ADDRESS_WEIGHTS = Map("alice" -> 10, "bob" -> 30, "john" -> 60), + ROUNDS = 1.to(2), + VALUES = Set("val1", "val2") + ).* from "./voteBookkeeperSM" // **************************************************************************** - // 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(totalWeight: Weight): bool = all { - bookkeeper' = { height: 10, totalWeight: totalWeight, rounds: Map() }, - lastEmitted' = { round: -1, name: "", value: "null" }, - } - - action applyVoteAction(vote: Vote, weight: Weight, currentRound: Round): bool = - val result = applyVote(bookkeeper, vote, weight, currentRound) - all { - bookkeeper' = result.bookkeeper, - lastEmitted' = result.event, - } - - // **************************************************************************** - // Test traces + // Tests // **************************************************************************** // auxiliary action for tests action _assert(predicate: bool): bool = - all { predicate, allUnchanged } + all { assert(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% + // all messages are received in order. We assume three validators in the validator set with 60%, 30% and 10% // each of the total voting power run synchronousConsensusTest = - initWith(100) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60, 1)) - .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == {round: 1, name: "PolkaValue", value: "proposal"})) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "bob"}, 30, 1)) - .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "bob"}, 30, 1)) - .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "alice"}, 60, 1)) - .then(_assert(lastEmitted == {round: 1, name: "PrecommitValue", value: "proposal"})) + initWith(1, 100) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 60, 1)) + .then(_assert(lastEmitted == noEvent(1))) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "john"}, 10, 1)) + .then(_assert(lastEmitted == polkaValueEvent(1, "val1"))) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "bob"}, 30, 1)) + .then(_assert(lastEmitted == noEvent(1))) + .then(applyVoteAction({typ: "Precommit", height: 1, round: 1, value: "val1", address: "bob"}, 30, 1)) + .then(_assert(lastEmitted == noEvent(1))) + .then(applyVoteAction({typ: "Precommit", height: 1, round: 1, value: "val1", address: "john"}, 10, 1)) + .then(_assert(lastEmitted == noEvent(1))) + .then(applyVoteAction({typ: "Precommit", height: 1, round: 1, value: "val1", address: "alice"}, 60, 1)) + .then(_assert(lastEmitted == precommitValueEvent(1, "val1"))) // Reaching PolkaAny run polkaAnyTest = - initWith(100) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "val1", address: "alice"}, 60, 1)) - .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == {round: 1, name: "PolkaAny", value: "null"})) + initWith(1, 100) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 60, 1)) + .then(_assert(lastEmitted == noEvent(1))) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "nil", address: "john"}, 10, 1)) + .then(_assert(lastEmitted == polkaAnyEvent(1))) // Reaching PolkaNil run polkaNilTest = - initWith(100) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "alice"}, 60, 1)) - .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == {round: 1, name: "PolkaNil", value: "null"})) + initWith(1, 100) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "nil", address: "alice"}, 60, 1)) + .then(_assert(lastEmitted == noEvent(1))) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "nil", address: "john"}, 10, 1)) + .then(_assert(lastEmitted == polkaNilEvent(1))) // Reaching Skip via n+1 threshold with prevotes from two validators at a future round run skipSmallQuorumAllPrevotesTest = - initWith(100) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60, 1)) - .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == {round: 2, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "bob"}, 30, 1)) - .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"})) + initWith(1, 100) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 60, 1)) + .then(_assert(lastEmitted == noEvent(1))) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 10, 1)) + .then(_assert(lastEmitted == noEvent(2))) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "bob"}, 30, 1)) + .then(_assert(lastEmitted == skipEvent(2))) // Cannot reach Skip via f+1 threshold with one prevote and one precommit from the same validator at a future round run noSkipSmallQuorumMixedVotesSameValTest = - initWith(90) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10, 1)) - .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 20, 1)) - .then(_assert(lastEmitted == {round: 2, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 20, 1)) - .then(_assert(lastEmitted != {round: 2, name: "Skip", value: "null"})) + initWith(1, 90) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 10, 1)) + .then(_assert(lastEmitted == noEvent(1))) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 20, 1)) + .then(_assert(lastEmitted == noEvent(2))) + .then(applyVoteAction({typ: "Precommit", height: 1, round: 2, value: "val1", address: "john"}, 20, 1)) + .then(_assert(lastEmitted != skipEvent(2))) // Reaching Skip via f+1 threshold with one prevote and one precommit from two validators at a future round run skipSmallQuorumMixedVotesTwoValsTest = - initWith(80) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 50, 1)) - .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == {round: 2, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "bob"}, 20, 1)) - .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"})) - + initWith(1, 80) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 50, 1)) + .then(_assert(lastEmitted == noEvent(1))) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 10, 1)) + .then(_assert(lastEmitted == noEvent(2))) + .then(applyVoteAction({typ: "Precommit", height: 1, round: 2, value: "val1", address: "bob"}, 20, 1)) + .then(_assert(lastEmitted == skipEvent(2))) + // Reaching Skip via 2f+1 threshold with a single prevote from a single validator at a future round run skipQuorumSinglePrevoteTest = - initWith(100) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10, 1)) - .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 60, 1)) - .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"})) + initWith(1, 100) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 10, 1)) + .then(all { assert(lastEmitted == noEvent(1)), allUnchanged }) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 60, 1)) + .then(all { assert(lastEmitted == skipEvent(2)), allUnchanged }) // Reaching Skip via 2f+1 threshold with a single precommit from a single validator at a future round run skipQuorumSinglePrecommitTest = - initWith(100) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10, 1)) + initWith(1, 100) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 10, 1)) .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 60, 1)) - .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"})) + .then(applyVoteAction({typ: "Precommit", height: 1, round: 2, value: "val1", address: "john"}, 60, 1)) + .then(_assert(lastEmitted == skipEvent(2))) // Cannot reach Skip via 2f+1 threshold with one prevote and one precommit from the same validator at a future round run noSkipQuorumMixedVotesSameValTest = - initWith(100) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10, 1)) - .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 30, 1)) - .then(_assert(lastEmitted == {round: 2, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 30, 1)) - .then(_assert(lastEmitted != {round: 2, name: "Skip", value: "null"})) + initWith(1, 100) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 10, 1)) + .then(_assert(lastEmitted == noEvent(1))) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 30, 1)) + .then(_assert(lastEmitted == noEvent(2))) + .then(applyVoteAction({typ: "Precommit", height: 1, round: 2, value: "val1", address: "john"}, 30, 1)) + .then(_assert(lastEmitted != skipEvent(2))) // Reaching Skip via 2f+1 threshold with one prevote and one precommit from two validators at a future round run skipQuorumMixedVotesTwoValsTest = - initWith(80) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 20, 1)) - .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == {round: 2, name: "None", value: "null"})) - .then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "bob"}, 50, 1)) - .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"})) + initWith(1, 80) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 20, 1)) + .then(_assert(lastEmitted == noEvent(1))) + .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 10, 1)) + .then(_assert(lastEmitted == noEvent(2))) + .then(applyVoteAction({typ: "Precommit", height: 1, round: 2, value: "val1", address: "bob"}, 50, 1)) + .then(_assert(lastEmitted == skipEvent(2))) + + // **************************************************************************** + // Properties that define an expected final state (for generating traces) + // **************************************************************************** + + val emitPrecommitValueState = lastEmitted.name == "PrecommitValue" + val emitPrecommitValue = not(emitPrecommitValueState) + + val emitPolkaAnyState = lastEmitted.name == "PolkaAny" + val emitPolkaAny = not(emitPolkaAnyState) + + val emitPolkaNilState = lastEmitted.name == "PolkaNil" + val emitPolkaNil = not(emitPolkaNilState) + val emitSkipState = lastEmitted.name == "Skip" + val emitSkip = not(emitSkipState) }