test(mbt): MBT for round state machine (#120)

* Use sum type for VoteType

* Use sum type for Threshold

* Use sum type for ExecutorEvent

* Use sum type for Value

* Update executor using votekeeper's new types

* Move unit tests near definition

* Fix SM and tests after merge

* Add types module

* Comment out id in types

* spec: remove initialRound

* fix spec

* Update itf tests

* cargo fmt

* Rename conflicting definitions

* Use `itf` native support for sum types (#111)

* spec driver: Bring some changes from main + some nits

* spec driver: another missing fix

* Rename voteBookkeepesSM to Models

* Move votekeeper types to common types

* WIP

* Add timeout state functions

* Fixes to value types

* fix driver typecheck

* fix more types

* Fix value type

* Renaming + comments

* Fix another value expression + type annotations

* renaming, commentrs, type Command

* rename missing

* replace match for if

* Replace NewRoundStep with NoStep

* Fix driver.qnt

Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com>

* WIP

* nits

* spec: initial round from -1 to 0

* deserializer: NewRound to NoStep

* code formatting

* Revert "spec: initial round from -1 to 0"

This reverts commit 9ab2c7f.

* Fix BigInt deserializer in minus_one_as_none

* A few small fixes

* Remove NewHeightCInput

* Hack for initial round = -1 in spec

* debugging

* spec: forgot second arg for initFor

* spec: driver indentation

* Add NewRoundStep.. and more

* spec: set NewRoundStep when skipping round; change condition in NewRound input

* remove addresses from state in consensusTest: no need of multiple ConsensusStates

* code formatting

* more formatting

* Remove unused model values

* update makefile

* Handle more step cases

* Rename `DecidedStep` to `CommitStep`

* Cleanup

* Check expected value for `Vote` output

* Use `pretty_assertions` crate for prettier output on failure

* Add round to `TimeoutOutput` in the spec

* Basic check for `GetValueAndScheduleTimeout`

* Fix valid_round

* spec: fix TimeoutOutput

* Cleaner output

* Align code with spec to start in round nil instead of zero

* Add round number to `NewRound` input and update round in state machine

* Rename `Step::NewRound` to `Step::Unstarted`

* Rename `NewRoundStep` to `UnstartedStep` in the specs

* Remove leftover Skip threshold

---------

Co-authored-by: Romain Ruetschi <romain@informal.systems>
Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com>

Code/Cargo.toml

@@ -24,6 +24,8 @@ futures           = "0.3"
 glob              = "0.3.0"
 itf               = "0.2.2"
 num-bigint        = "0.4.4"
+num-traits        = "0.2.17"
+pretty_assertions = "1.4"
 rand              = { version = "0.8.5", features = ["std_rng"] }
 serde             = "1.0"
 serde_json        = "1.0"

Code/common/src/round.rs

@@ -15,9 +15,6 @@ pub enum Round {
 }
 
 impl Round {
-    /// The initial, zero round.
-    pub const INITIAL: Round = Round::new(0);
-
     /// Create a new round.
     ///
     /// If `round < 0`, then `Round::Nil` is returned.

Code/driver/src/driver.rs

@@ -74,7 +74,7 @@ where
             address,
             validator_set,
             vote_keeper: votes,
-            round_state: RoundState::new(height, Round::new(0)),
+            round_state: RoundState::new(height, Round::Nil),
             proposal: None,
             pending_input: None,
         }
@@ -173,7 +173,7 @@ where
             self.round_state = RoundState::new(height, round);
         }
 
-        self.apply_input(round, RoundInput::NewRound)
+        self.apply_input(round, RoundInput::NewRound(round))
     }
 
     async fn apply_propose_value(

Code/driver/src/mux.rs

@@ -207,7 +207,7 @@ where
         round: Round,
     ) -> Option<RoundInput<Ctx>> {
         match pending_step {
-            Step::NewRound => None, // Some(RoundInput::NewRound),
+            Step::Unstarted => None,
 
             Step::Propose => None,
 

Code/itf/Cargo.toml

@@ -11,15 +11,18 @@ publish.workspace      = true
 [dependencies]
 malachite-common = { version = "0.1.0", path = "../common" }
 malachite-vote   = { version = "0.1.0", path = "../vote" }
+malachite-round  = { version = "0.1.0", path = "../round" }
 malachite-test   = { version = "0.1.0", path = "../test" }
 
-itf              = { workspace = true }
-rand             = { workspace = true }
-num-bigint       = { workspace = true, features = ["serde"] }
-serde            = { workspace = true, features = ["derive"] }
-serde_json       = { workspace = true }
-serde_with       = { workspace = true }
-glob             = { workspace = true }
+itf               = { workspace = true }
+rand              = { workspace = true }
+num-bigint        = { workspace = true, features = ["serde"] }
+num-traits        = { workspace = true }
+serde             = { workspace = true, features = ["derive"] }
+serde_json        = { workspace = true }
+serde_with        = { workspace = true }
+glob              = { workspace = true }
+pretty_assertions = { workspace = true }
 
 [dev-dependencies]
 tempfile         = { version = "3.8.1" }

Code/itf/src/consensus.rs

@@ -0,0 +1,99 @@
+use itf::de::{As, Integer, Same};
+use serde::Deserialize;
+
+use crate::deserializers as de;
+use crate::types::{Address, Height, NonNilValue, Proposal, Round, Step, Timeout, Value, Vote};
+
+#[derive(Clone, Debug, Deserialize)]
+pub struct State {
+    pub state: ConsensusState,
+    pub input: Input,
+    pub output: Output,
+}
+
+#[derive(Clone, Debug, Deserialize)]
+#[serde(rename = "ConsensusInput")]
+#[serde(tag = "tag", content = "value")]
+pub enum Input {
+    #[serde(rename = "NoConsensusInput")]
+    NoInput,
+    #[serde(rename = "NewRoundCInput")]
+    #[serde(with = "As::<Integer>")]
+    NewRound(Round),
+    #[serde(rename = "NewRoundProposerCInput")]
+    #[serde(with = "As::<(Integer, Same)>")]
+    NewRoundProposer(Round, NonNilValue),
+    #[serde(rename = "ProposalCInput")]
+    #[serde(with = "As::<(Integer, Same)>")]
+    Proposal(Round, Value),
+    #[serde(rename = "ProposalAndPolkaPreviousAndValidCInput")]
+    #[serde(with = "As::<(Same, Integer)>")]
+    ProposalAndPolkaPreviousAndValid(Value, Round),
+    #[serde(rename = "ProposalInvalidCInput")]
+    ProposalInvalid,
+    #[serde(rename = "PolkaNilCInput")]
+    PolkaNil,
+    #[serde(rename = "PolkaAnyCInput")]
+    PolkaAny,
+    #[serde(rename = "ProposalAndPolkaAndValidCInput")]
+    ProposalAndPolkaAndValid(Value),
+    #[serde(rename = "PrecommitAnyCInput")]
+    PrecommitAny,
+    #[serde(rename = "ProposalAndCommitAndValidCInput")]
+    ProposalAndCommitAndValid(Value),
+    #[serde(rename = "RoundSkipCInput")]
+    #[serde(with = "As::<Integer>")]
+    RoundSkip(Round),
+    #[serde(rename = "TimeoutProposeCInput")]
+    #[serde(with = "As::<(Integer, Integer)>")]
+    TimeoutPropose(Height, Round),
+    #[serde(rename = "TimeoutPrevoteCInput")]
+    #[serde(with = "As::<(Integer, Integer)>")]
+    TimeoutPrevote(Height, Round),
+    #[serde(rename = "TimeoutPrecommitCInput")]
+    #[serde(with = "As::<(Integer, Integer)>")]
+    TimeoutPrecommit(Height, Round),
+    #[serde(rename = "ProposalAndPolkaAndInvalidCInputCInput")]
+    #[serde(with = "As::<(Integer, Integer, Same)>")]
+    ProposalAndPolkaAndInvalidCInput(Height, Round, Value),
+}
+
+#[derive(Clone, Debug, Deserialize)]
+#[serde(rename = "ConsensusOutput")]
+#[serde(tag = "tag", content = "value")]
+pub enum Output {
+    #[serde(rename = "NoConsensusOutput")]
+    NoOutput,
+    #[serde(rename = "ProposalOutput")]
+    Proposal(Proposal),
+    #[serde(rename = "VoteOutput")]
+    Vote(Vote),
+    #[serde(rename = "TimeoutOutput")]
+    #[serde(with = "As::<(Integer, Same)>")]
+    Timeout(Round, Timeout),
+    #[serde(rename = "DecidedOutput")]
+    Decided(Value),
+    #[serde(rename = "SkipRoundOutput")]
+    #[serde(with = "As::<Integer>")]
+    SkipRound(Round),
+    #[serde(rename = "ErrorOutput")]
+    Error(String),
+}
+
+#[derive(Clone, Debug, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct ConsensusState {
+    #[serde(rename = "p")]
+    pub process: Address,
+    #[serde(with = "As::<Integer>")]
+    pub height: Height,
+    #[serde(with = "As::<Integer>")]
+    pub round: Round,
+    pub step: Step,
+    #[serde(deserialize_with = "de::minus_one_as_none")]
+    pub locked_round: Option<Round>,
+    pub locked_value: Value,
+    #[serde(deserialize_with = "de::minus_one_as_none")]
+    pub valid_round: Option<Round>,
+    pub valid_value: Value,
+}

Code/itf/src/deserializers.rs

@@ -0,0 +1,15 @@
+use num_bigint::BigInt;
+use num_traits::cast::ToPrimitive;
+use serde::Deserialize;
+
+pub(crate) fn minus_one_as_none<'de, D>(de: D) -> Result<Option<i64>, D::Error>
+where
+    D: serde::Deserializer<'de>,
+{
+    let opt = Option::<BigInt>::deserialize(de).unwrap();
+    match opt {
+        None => Ok(None),
+        Some(i) if i == BigInt::from(-1) => Ok(None),
+        Some(i) => Ok(i.to_i64()),
+    }
+}

Code/itf/src/lib.rs

@@ -1,3 +1,5 @@
+pub mod consensus;
+pub mod deserializers;
 pub mod types;
 pub mod utils;
 pub mod votekeeper;

Code/itf/src/types.rs

@@ -1,4 +1,5 @@
 use itf::de::{As, Integer};
+use malachite_round::state::Step as RoundStep;
 use serde::Deserialize;
 
 pub type Height = i64;
@@ -14,13 +15,44 @@ pub enum Value {
     Val(NonNilValue),
 }
 
+impl Value {
+    pub fn fold<A>(&self, nil: A, val: impl FnOnce(&NonNilValue) -> A) -> A {
+        match self {
+            Value::Nil => nil,
+            Value::Val(value) => val(value),
+        }
+    }
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct Proposal {
+    pub src_address: Address,
+    #[serde(with = "As::<Integer>")]
+    pub height: Height,
+    #[serde(with = "As::<Integer>")]
+    pub round: Round,
+    pub proposal: NonNilValue,
+    #[serde(with = "As::<Integer>")]
+    pub valid_round: Round,
+}
+
 #[derive(Clone, Debug, PartialEq, Eq, Deserialize)]
 #[serde(tag = "tag", content = "value")]
 pub enum VoteType {
     Prevote,
     Precommit,
 }
 
+impl VoteType {
+    pub fn to_common(&self) -> malachite_common::VoteType {
+        match self {
+            VoteType::Prevote => malachite_common::VoteType::Prevote,
+            VoteType::Precommit => malachite_common::VoteType::Precommit,
+        }
+    }
+}
+
 #[derive(Clone, Debug, PartialEq, Eq, Deserialize)]
 #[serde(rename_all = "camelCase")]
 pub struct Vote {
@@ -32,3 +64,56 @@ pub struct Vote {
     pub value_id: Value,
     pub src_address: Address,
 }
+
+#[derive(Clone, Debug, PartialEq, Eq, Deserialize)]
+#[serde(tag = "tag", content = "value")]
+pub enum Step {
+    #[serde(rename = "NoStep")]
+    None,
+    #[serde(rename = "UnstartedStep")]
+    Unstarted,
+    #[serde(rename = "ProposeStep")]
+    Propose,
+    #[serde(rename = "PrevoteStep")]
+    Prevote,
+    #[serde(rename = "PrecommitStep")]
+    Precommit,
+    #[serde(rename = "CommitStep")]
+    Commit,
+}
+
+impl Step {
+    pub fn to_round_step(&self) -> Option<RoundStep> {
+        match self {
+            Step::None => None,
+            Step::Unstarted => Some(RoundStep::Unstarted),
+            Step::Propose => Some(RoundStep::Propose),
+            Step::Prevote => Some(RoundStep::Prevote),
+            Step::Precommit => Some(RoundStep::Precommit),
+            Step::Commit => Some(RoundStep::Commit),
+        }
+    }
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, Deserialize)]
+#[serde(tag = "tag", content = "value")]
+pub enum Timeout {
+    #[serde(rename = "ProposeTimeout")]
+    Propose,
+
+    #[serde(rename = "PrevoteTimeout")]
+    Prevote,
+
+    #[serde(rename = "PrecommitTimeout")]
+    Precommit,
+}
+
+impl Timeout {
+    pub fn to_common(&self) -> malachite_common::TimeoutStep {
+        match self {
+            Timeout::Propose => malachite_common::TimeoutStep::Propose,
+            Timeout::Prevote => malachite_common::TimeoutStep::Prevote,
+            Timeout::Precommit => malachite_common::TimeoutStep::Precommit,
+        }
+    }
+}

Code/itf/src/utils.rs

@@ -3,6 +3,8 @@ use std::path::Path;
 
 // TODO(rano): simplify this function once quint is fixed
 pub fn generate_traces(spec_rel_path: &str, gen_dir: &str, quint_seed: u64) {
+    println!("🪄 Generating traces for {spec_rel_path:?}...");
+
     let spec_abs_path = format!(
         "{}/../../Specs/Quint/{}",
         env!("CARGO_MANIFEST_DIR"),

Code/itf/tests/consensus.rs

@@ -0,0 +1,67 @@
+#[path = "consensus/runner.rs"]
+pub mod runner;
+#[path = "consensus/utils.rs"]
+pub mod utils;
+
+use glob::glob;
+use rand::rngs::StdRng;
+use rand::SeedableRng;
+
+use malachite_itf::consensus::State;
+use malachite_itf::utils::generate_traces;
+use malachite_test::{Address, PrivateKey};
+
+use runner::ConsensusRunner;
+use utils::ADDRESSES;
+
+const RANDOM_SEED: u64 = 0x42;
+
+#[test]
+fn test_itf() {
+    let temp_dir = tempfile::tempdir().expect("Failed to create temp dir");
+
+    let quint_seed = option_env!("QUINT_SEED")
+        // use inspect when stabilized
+        .map(|x| {
+            println!("using QUINT_SEED={}", x);
+            x
+        })
+        .or(Some("118"))
+        .and_then(|x| x.parse::<u64>().ok())
+        .filter(|&x| x != 0)
+        .expect("invalid random seed for quint");
+
+    generate_traces(
+        "consensusTest.qnt",
+        &temp_dir.path().to_string_lossy(),
+        quint_seed,
+    );
+
+    for json_fixture in glob(&format!("{}/*.itf.json", temp_dir.path().display()))
+        .expect("Failed to read glob pattern")
+        .flatten()
+    {
+        println!(
+            "🚀 Running trace {:?}",
+            json_fixture.file_name().unwrap().to_str().unwrap()
+        );
+
+        let json = std::fs::read_to_string(&json_fixture).unwrap();
+        let trace = itf::trace_from_str::<State>(&json).unwrap();
+
+        let mut rng = StdRng::seed_from_u64(RANDOM_SEED);
+
+        // build mapping from model addresses to real addresses
+        let consensus_runner = ConsensusRunner {
+            address_map: ADDRESSES
+                .iter()
+                .map(|&name| {
+                    let pk = PrivateKey::generate(&mut rng).public_key();
+                    (name.into(), Address::from_public_key(&pk))
+                })
+                .collect(),
+        };
+
+        trace.run_on(consensus_runner).unwrap();
+    }
+}