Merge branch 'main' into anca/keeper_skip_test

.github/workflows/quint.yml

@@ -15,15 +15,22 @@ jobs:
   quint-typecheck:
     name: Typecheck
     runs-on: ubuntu-latest
-    defaults:
-      run:
-        working-directory: ./Specs/Quint
     steps:
       - uses: actions/checkout@v4
       - uses: actions/setup-node@v3
         with:
           node-version: "18"
       - run: npm install -g @informalsystems/quint
-      - run: npx @informalsystems/quint typecheck consensus.qnt
-      - run: npx @informalsystems/quint typecheck voteBookkeeper.qnt
+      - run: bash Scripts/quint-forall.sh typecheck Specs/Quint/*.qnt
+
+  quint-test:
+    name: Test
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-node@v3
+        with:
+          node-version: "18"
+      - run: npm install -g @informalsystems/quint
+      - run: bash Scripts/quint-forall.sh test Specs/Quint/*Test.qnt
 

Code/Cargo.toml

@@ -4,9 +4,10 @@ resolver = "2"
 members = [
   "common",
   "driver",
+  "itf",
   "round",
-  "vote",
   "test",
+  "vote",
 ]
 
 [workspace.package]
@@ -20,6 +21,8 @@ publish      = false
 async-trait       = "0.1"
 futures           = "0.3"
 ed25519-consensus = "2.1.0"
+itf               = "0.1.2"
 rand              = { version = "0.8.5", features = ["std_rng"] }
+serde             = "1.0"
 sha2              = "0.10.8"
 signature         = "2.1.0"

Code/common/src/context.rs

@@ -40,6 +40,7 @@ where
     /// Build a new prevote vote by the validator with the given address,
     /// for the value identified by the given value id, at the given round.
     fn new_prevote(
+        height: Self::Height,
         round: Round,
         value_id: Option<ValueId<Self>>,
         address: Self::Address,
@@ -48,6 +49,7 @@ where
     /// Build a new precommit vote by the validator with the given address,
     /// for the value identified by the given value id, at the given round.
     fn new_precommit(
+        height: Self::Height,
         round: Round,
         value_id: Option<ValueId<Self>>,
         address: Self::Address,

Code/common/src/height.rs

@@ -9,6 +9,6 @@ use core::fmt::Debug;
 pub trait Height
 where
     // TODO: Require Copy as well?
-    Self: Clone + Debug + PartialEq + Eq + PartialOrd + Ord,
+    Self: Default + Clone + Debug + PartialEq + Eq + PartialOrd + Ord,
 {
 }

Code/common/src/vote.rs

@@ -21,6 +21,9 @@ where
     Self: Clone + Debug + Eq,
     Ctx: Context,
 {
+    /// The height for which the vote is for.
+    fn height(&self) -> Ctx::Height;
+
     /// The round for which the vote is for.
     fn round(&self) -> Round;
 

Code/driver/src/driver.rs

@@ -1,5 +1,3 @@
-use alloc::collections::BTreeMap;
-
 use malachite_round::state_machine::RoundData;
 
 use malachite_common::{
@@ -33,13 +31,11 @@ where
     pub env: Env,
     pub proposer_selector: PSel,
 
-    pub height: Ctx::Height,
     pub address: Ctx::Address,
     pub validator_set: Ctx::ValidatorSet,
 
-    pub round: Round,
     pub votes: VoteKeeper<Ctx>,
-    pub round_states: BTreeMap<Round, RoundState<Ctx>>,
+    pub round_state: RoundState<Ctx>,
 }
 
 impl<Ctx, Env, PSel> Driver<Ctx, Env, PSel>
@@ -52,7 +48,6 @@ where
         ctx: Ctx,
         env: Env,
         proposer_selector: PSel,
-        height: Ctx::Height,
         validator_set: Ctx::ValidatorSet,
         address: Ctx::Address,
     ) -> Self {
@@ -65,17 +60,25 @@ where
             ctx,
             env,
             proposer_selector,
-            height,
             address,
             validator_set,
-            round: Round::NIL,
             votes,
-            round_states: BTreeMap::new(),
+            round_state: RoundState::default(),
         }
     }
 
-    async fn get_value(&self, round: Round) -> Option<Ctx::Value> {
-        self.env.get_value(self.height.clone(), round).await
+    pub fn height(&self) -> &Ctx::Height {
+        &self.round_state.height
+    }
+
+    pub fn round(&self) -> Round {
+        self.round_state.round
+    }
+
+    async fn get_value(&self) -> Option<Ctx::Value> {
+        self.env
+            .get_value(self.height().clone(), self.round())
+            .await
     }
 
     pub async fn execute(&mut self, msg: Event<Ctx>) -> Result<Option<Message<Ctx>>, Error<Ctx>> {
@@ -85,11 +88,7 @@ where
         };
 
         let msg = match round_msg {
-            RoundMessage::NewRound(round) => {
-                // XXX: Check if there is an existing state?
-                assert!(self.round < round);
-                Message::NewRound(round)
-            }
+            RoundMessage::NewRound(round) => Message::NewRound(self.height().clone(), round),
 
             RoundMessage::Proposal(proposal) => {
                 // sign the proposal
@@ -112,21 +111,27 @@ where
         Ok(Some(msg))
     }
 
-    async fn apply(&mut self, msg: Event<Ctx>) -> Result<Option<RoundMessage<Ctx>>, Error<Ctx>> {
-        match msg {
-            Event::NewRound(round) => self.apply_new_round(round).await,
+    async fn apply(&mut self, event: Event<Ctx>) -> Result<Option<RoundMessage<Ctx>>, Error<Ctx>> {
+        match event {
+            Event::NewRound(height, round) => self.apply_new_round(height, round).await,
+
             Event::Proposal(proposal, validity) => {
                 Ok(self.apply_proposal(proposal, validity).await)
             }
+
             Event::Vote(signed_vote) => self.apply_vote(signed_vote),
+
             Event::TimeoutElapsed(timeout) => Ok(self.apply_timeout(timeout)),
         }
     }
 
     async fn apply_new_round(
         &mut self,
+        height: Ctx::Height,
         round: Round,
     ) -> Result<Option<RoundMessage<Ctx>>, Error<Ctx>> {
+        self.round_state = RoundState::new(height, round);
+
         let proposer_address = self
             .proposer_selector
             .select_proposer(round, &self.validator_set);
@@ -140,7 +145,7 @@ where
             // We are the proposer
             // TODO: Schedule propose timeout
 
-            let Some(value) = self.get_value(round).await else {
+            let Some(value) = self.get_value().await else {
                 return Err(Error::NoValueToPropose);
             };
 
@@ -149,11 +154,6 @@ where
             RoundEvent::NewRound
         };
 
-        assert!(self.round < round);
-        self.round_states
-            .insert(round, RoundState::default().new_round(round));
-        self.round = round;
-
         Ok(self.apply_event(round, event))
     }
 
@@ -163,23 +163,24 @@ where
         validity: Validity,
     ) -> Option<RoundMessage<Ctx>> {
         // Check that there is an ongoing round
-        let Some(round_state) = self.round_states.get(&self.round) else {
-            // TODO: Add logging
+        if self.round_state.round == Round::NIL {
             return None;
-        };
+        }
 
         // Only process the proposal if there is no other proposal
-        if round_state.proposal.is_some() {
+        if self.round_state.proposal.is_some() {
             return None;
         }
 
         // Check that the proposal is for the current height and round
-        if self.height != proposal.height() || self.round != proposal.round() {
+        if self.round_state.height != proposal.height()
+            || self.round_state.round != proposal.round()
+        {
             return None;
         }
 
         // TODO: Document
-        if proposal.pol_round().is_defined() && proposal.pol_round() >= round_state.round {
+        if proposal.pol_round().is_defined() && proposal.pol_round() >= self.round_state.round {
             return None;
         }
 
@@ -237,11 +238,12 @@ where
             ));
         }
 
-        let round = signed_vote.vote.round();
+        let vote_round = signed_vote.vote.round();
+        let current_round = self.round();
 
         let Some(vote_msg) =
             self.votes
-                .apply_vote(signed_vote.vote, validator.voting_power(), self.round)
+                .apply_vote(signed_vote.vote, validator.voting_power(), current_round)
         else {
             return Ok(None);
         };
@@ -255,7 +257,7 @@ where
             VoteMessage::SkipRound(r) => RoundEvent::SkipRound(r),
         };
 
-        Ok(self.apply_event(round, round_event))
+        Ok(self.apply_event(vote_round, round_event))
     }
 
     fn apply_timeout(&mut self, timeout: Timeout) -> Option<RoundMessage<Ctx>> {
@@ -270,10 +272,9 @@ where
 
     /// Apply the event, update the state.
     fn apply_event(&mut self, round: Round, event: RoundEvent<Ctx>) -> Option<RoundMessage<Ctx>> {
-        // Get the round state, or create a new one
-        let round_state = self.round_states.remove(&round).unwrap_or_default();
+        let round_state = core::mem::take(&mut self.round_state);
 
-        let data = RoundData::new(round, &self.height, &self.address);
+        let data = RoundData::new(round, round_state.height.clone(), &self.address);
 
         // Multiplex the event with the round state.
         let mux_event = match event {
@@ -297,13 +298,9 @@ where
         let transition = round_state.apply_event(&data, mux_event);
 
         // Update state
-        self.round_states.insert(round, transition.next_state);
+        self.round_state = transition.next_state;
 
         // Return message, if any
         transition.message
     }
-
-    pub fn round_state(&self, round: Round) -> Option<&RoundState<Ctx>> {
-        self.round_states.get(&round)
-    }
 }

Code/driver/src/event.rs

@@ -8,7 +8,7 @@ pub enum Event<Ctx>
 where
     Ctx: Context,
 {
-    NewRound(Round),
+    NewRound(Ctx::Height, Round),
     Proposal(Ctx::Proposal, Validity),
     Vote(SignedVote<Ctx>),
     TimeoutElapsed(Timeout),

Code/driver/src/message.rs

@@ -11,7 +11,7 @@ where
     Vote(SignedVote<Ctx>),
     Decide(Round, Ctx::Value),
     ScheduleTimeout(Timeout),
-    NewRound(Round),
+    NewRound(Ctx::Height, Round),
 }
 
 // NOTE: We have to derive these instances manually, otherwise
@@ -26,7 +26,7 @@ impl<Ctx: Context> Clone for Message<Ctx> {
             Message::Vote(signed_vote) => Message::Vote(signed_vote.clone()),
             Message::Decide(round, value) => Message::Decide(*round, value.clone()),
             Message::ScheduleTimeout(timeout) => Message::ScheduleTimeout(*timeout),
-            Message::NewRound(round) => Message::NewRound(*round),
+            Message::NewRound(height, round) => Message::NewRound(height.clone(), *round),
         }
     }
 }
@@ -39,7 +39,7 @@ impl<Ctx: Context> fmt::Debug for Message<Ctx> {
             Message::Vote(signed_vote) => write!(f, "Vote({:?})", signed_vote),
             Message::Decide(round, value) => write!(f, "Decide({:?}, {:?})", round, value),
             Message::ScheduleTimeout(timeout) => write!(f, "ScheduleTimeout({:?})", timeout),
-            Message::NewRound(round) => write!(f, "NewRound({:?})", round),
+            Message::NewRound(height, round) => write!(f, "NewRound({:?}, {:?})", height, round),
         }
     }
 }
@@ -60,7 +60,9 @@ impl<Ctx: Context> PartialEq for Message<Ctx> {
             (Message::ScheduleTimeout(timeout), Message::ScheduleTimeout(other_timeout)) => {
                 timeout == other_timeout
             }
-            (Message::NewRound(round), Message::NewRound(other_round)) => round == other_round,
+            (Message::NewRound(height, round), Message::NewRound(other_height, other_round)) => {
+                height == other_height && round == other_round
+            }
             _ => false,
         }
     }

Code/itf/Cargo.toml

@@ -0,0 +1,13 @@
+[package]
+name        = "malachite-itf"
+description = "Library for working with ITF traces for the Malachite consensus engine"
+
+version.workspace      = true
+edition.workspace      = true
+repository.workspace   = true
+license.workspace      = true
+publish.workspace      = true
+
+[dependencies]
+itf.workspace = true
+serde         = { workspace = true, features = ["derive"] }