Merge branch 'main' into anca/one_round_state

.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/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"] }

Code/itf/src/consensus.rs

@@ -0,0 +1,177 @@
+use itf::{ItfBigInt, ItfMap};
+use serde::Deserialize;
+
+use crate::deserializers as de;
+
+pub type Address = String;
+pub type Value = String;
+pub type Step = String;
+pub type Round = ItfBigInt;
+pub type Height = ItfBigInt;
+
+#[derive(Clone, Debug, Deserialize)]
+pub enum Timeout {
+    #[serde(rename = "timeoutPrevote")]
+    Prevote,
+
+    #[serde(rename = "timeoutPrecommit")]
+    Precommit,
+
+    #[serde(rename = "timeoutPropose")]
+    Propose,
+}
+
+#[derive(Clone, Debug, Deserialize)]
+pub struct State {
+    pub system: System,
+
+    #[serde(rename = "_Event")]
+    pub event: Event,
+
+    #[serde(rename = "_Result")]
+    pub result: Result,
+}
+
+#[derive(Clone, Debug, Deserialize)]
+pub struct System(ItfMap<Address, ConsensusState>);
+
+#[derive(Clone, Debug, Deserialize)]
+#[serde(tag = "name")]
+pub enum Event {
+    Initial,
+    NewRound {
+        height: Height,
+        round: Round,
+    },
+    Proposal {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    ProposalAndPolkaAndValid {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    ProposalAndCommitAndValid {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    NewHeight {
+        height: Height,
+        round: Round,
+    },
+    NewRoundProposer {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    PolkaNil {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    PolkaAny {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    PrecommitAny {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    TimeoutPrevote {
+        height: Height,
+        round: Round,
+    },
+    TimeoutPrecommit {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    TimeoutPropose {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    ProposalInvalid {
+        height: Height,
+        round: Round,
+    },
+}
+
+#[derive(Clone, Debug, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct Result {
+    pub name: String,
+    #[serde(deserialize_with = "de::proposal_or_none")]
+    pub proposal: Option<Proposal>,
+    #[serde(deserialize_with = "de::vote_message_or_none")]
+    pub vote_message: Option<VoteMessage>,
+    #[serde(deserialize_with = "de::empty_string_as_none")]
+    pub timeout: Option<Timeout>,
+    #[serde(deserialize_with = "de::empty_string_as_none")]
+    pub decided: Option<Value>,
+    #[serde(deserialize_with = "de::minus_one_as_none")]
+    pub skip_round: Option<Round>,
+}
+
+#[derive(Clone, Debug, Deserialize, PartialEq, Eq)]
+#[serde(rename_all = "camelCase")]
+pub struct Proposal {
+    pub src: Address,
+    pub height: Height,
+    pub round: Round,
+    pub proposal: Value,
+    pub valid_round: Round,
+}
+
+impl Proposal {
+    pub fn is_empty(&self) -> bool {
+        self.src.is_empty()
+            && self.proposal.is_empty()
+            && self.height == ItfBigInt::from(-1)
+            && self.round == ItfBigInt::from(-1)
+            && self.valid_round == ItfBigInt::from(-1)
+    }
+}
+
+#[derive(Clone, Debug, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct VoteMessage {
+    pub src: Address,
+    pub height: Height,
+    pub round: Round,
+    pub step: Step,
+    pub id: Value,
+}
+
+impl VoteMessage {
+    pub fn is_empty(&self) -> bool {
+        self.src.is_empty()
+            && self.id.is_empty()
+            && self.height == ItfBigInt::from(-1)
+            && self.round == ItfBigInt::from(-1)
+            && self.step.is_empty()
+    }
+}
+
+#[derive(Clone, Debug, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct ConsensusState {
+    pub p: Address,
+    pub height: Height,
+    pub round: Round,
+    pub step: Step,
+
+    #[serde(deserialize_with = "de::minus_one_as_none")]
+    pub locked_round: Option<Round>,
+    #[serde(deserialize_with = "de::empty_string_as_none")]
+    pub locked_value: Option<Value>,
+    #[serde(deserialize_with = "de::minus_one_as_none")]
+    pub valid_round: Option<Round>,
+    #[serde(deserialize_with = "de::empty_string_as_none")]
+    pub valid_value: Option<Value>,
+}

Code/itf/src/deserializers.rs

@@ -0,0 +1,53 @@
+use itf::ItfBigInt;
+use serde::de::IntoDeserializer;
+use serde::Deserialize;
+
+use crate::consensus::{Proposal, VoteMessage};
+
+pub(crate) fn empty_string_as_none<'de, D, T>(de: D) -> Result<Option<T>, D::Error>
+where
+    D: serde::Deserializer<'de>,
+    T: serde::Deserialize<'de>,
+{
+    let opt = Option::<String>::deserialize(de)?;
+    match opt.as_deref() {
+        None | Some("") => Ok(None),
+        Some(s) => T::deserialize(s.into_deserializer()).map(Some),
+    }
+}
+
+pub(crate) fn minus_one_as_none<'de, D>(de: D) -> Result<Option<ItfBigInt>, D::Error>
+where
+    D: serde::Deserializer<'de>,
+{
+    let opt = Option::<ItfBigInt>::deserialize(de)?;
+    match opt {
+        None => Ok(None),
+        Some(i) if i == ItfBigInt::from(-1) => Ok(None),
+        Some(i) => Ok(Some(i)),
+    }
+}
+
+pub(crate) fn proposal_or_none<'de, D>(de: D) -> Result<Option<Proposal>, D::Error>
+where
+    D: serde::Deserializer<'de>,
+{
+    let proposal = Proposal::deserialize(de)?;
+    if proposal.is_empty() {
+        Ok(None)
+    } else {
+        Ok(Some(proposal))
+    }
+}
+
+pub(crate) fn vote_message_or_none<'de, D>(de: D) -> Result<Option<VoteMessage>, D::Error>
+where
+    D: serde::Deserializer<'de>,
+{
+    let vote_message = VoteMessage::deserialize(de)?;
+    if vote_message.is_empty() {
+        Ok(None)
+    } else {
+        Ok(Some(vote_message))
+    }
+}

Code/itf/src/lib.rs

@@ -0,0 +1,4 @@
+pub mod consensus;
+pub mod votekeeper;
+
+mod deserializers;

Code/itf/src/votekeeper.rs

@@ -0,0 +1,49 @@
+use itf::{ItfBigInt, ItfMap, ItfSet};
+use serde::Deserialize;
+
+pub type Height = ItfBigInt;
+pub type Weight = ItfBigInt;
+pub type Round = ItfBigInt;
+pub type Address = String;
+pub type Value = String;
+
+#[derive(Clone, Debug, PartialEq, Eq, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct Bookkeeper {
+    pub height: Height,
+    pub total_weight: Weight,
+    pub rounds: ItfMap<Round, RoundVotes>,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct RoundVotes {
+    pub height: Height,
+    pub round: Round,
+    pub prevotes: VoteCount,
+    pub precommits: VoteCount,
+    pub emitted_events: ItfSet<ExecutorEvent>,
+    pub votes_addresses_weights: ItfMap<Address, Weight>,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct VoteCount {
+    pub total_weight: Weight,
+    pub values_weights: ItfMap<Value, Weight>,
+    pub votes_addresses: ItfSet<Address>,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, Deserialize, Hash)]
+pub struct ExecutorEvent {
+    pub round: Round,
+    pub name: String,
+    pub value: Value,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct State {
+    pub bookkeeper: Bookkeeper,
+    pub last_emitted: ExecutorEvent,
+}

Code/itf/tests/consensus.rs

@@ -0,0 +1,21 @@
+use malachite_itf::consensus::State;
+
+#[test]
+fn parse_fixtures() {
+    let folder = format!("{}/tests/fixtures/consensus", env!("CARGO_MANIFEST_DIR"));
+
+    let fixtures = std::fs::read_dir(folder)
+        .unwrap()
+        .map(|entry| entry.unwrap().path())
+        .filter(|path| path.extension().map_or(false, |ext| ext == "json"))
+        .collect::<Vec<_>>();
+
+    for fixture in fixtures {
+        println!("Parsing '{}'", fixture.display());
+
+        let json = std::fs::read_to_string(&fixture).unwrap();
+        let state = itf::trace_from_str::<State>(&json).unwrap();
+
+        dbg!(state);
+    }
+}

Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaAnyTest_6.itf.json

@@ -0,0 +1 @@
+{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"voteBookkeeper.qnt","status":"passed","description":"Created by Quint on Fri Nov 10 2023 14:26:21 GMT+0100 (GMT+01:00)","timestamp":1699622781761},"vars":["lastEmitted","bookkeeper"],"states":[{"#meta":{"index":0},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"","round":{"#bigint":"-1"},"value":"null"}},{"#meta":{"index":1},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":2},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":3},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"70"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}},{"#meta":{"index":4},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"70"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}},{"#meta":{"index":5},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":6},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":7},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"30"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":8},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"30"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":9},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"40"}]]},"votesAddresses":{"#set":["bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":10},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"40"}]]},"votesAddresses":{"#set":["bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":11},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"},{"name":"PrecommitValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alive","bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["alive",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PrecommitValue","round":{"#bigint":"1"},"value":"proposal"}}]}