tests: MBT for votekeeper (#63)

* 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 <romain@informal.systems> * 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 <josef@informal.systems> 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 <josef@informal.systems> Co-authored-by: Romain Ruetschi <romain@informal.systems> Co-authored-by: Anca Zamfir <anca@informal.systems> Co-authored-by: Ranadeep Biswas <rano@informal.systems>
informalsystems · Nov 28, 2023 · 1dafd49 · 1dafd49
1 parent 952c4e3
commit 1dafd49
Show file tree

Hide file tree

Showing 34 changed files with 1,048 additions and 327 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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<Address, ConsensusState>);
+pub struct System(HashMap<Address, ConsensusState>);
 
 #[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
@@ -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<Option<ItfBigInt>, D::Error>
+pub(crate) fn minus_one_as_none<'de, D>(de: D) -> Result<Option<BigInt>, D::Error>
 where
     D: serde::Deserializer<'de>,
 {
-    let opt = Option::<ItfBigInt>::deserialize(de)?;
+    let opt = Option::<BigInt>::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
@@ -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
@@ -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();
+    }
+}
Original file line number	Diff line number	Diff line change
Expand Up		@@ -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
Original file line number	Diff line number	Diff line change
Expand Up		@@ -2,3 +2,4 @@ pub mod consensus;
		pub mod votekeeper;

		mod deserializers;
		pub mod utils;