From d4090cb9835b05c5c3aa8e0c8a1b348073b8b881 Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Thu, 30 Nov 2023 11:20:05 +0100 Subject: [PATCH] spec: Renaming and cleanup (#94) * Remove ITF trace * Rename executor to driver * Rename output of votekeeper to `VoteKeeperOutput` * Rename `Event` to `ConsensusInput` * Rename `ProposeMsg_t` to `Proposal_t` and `VoteMsg_t` to `Vote_t` * Cleanup * Rename `PendingEvent` to `PendingInput` * Fix last remaining instances of `result and `event` * Fix ITF structs * Cleanup in Rust code --- Code/itf/src/votekeeper.rs | 6 +- Code/itf/tests/votekeeper/runner.rs | 12 +- Code/vote/src/keeper.rs | 18 +- Specs/Quint/0DecideNonProposerTest.itf.json | 1 - Specs/Quint/Makefile | 2 +- Specs/Quint/consensus.qnt | 248 ++++++++++---------- Specs/Quint/consensusTest.qnt | 94 ++++---- Specs/Quint/{executor.qnt => driver.qnt} | 216 ++++++++--------- Specs/Quint/statemachineAsync.qnt | 38 +-- Specs/Quint/statemachineTest.qnt | 26 +- Specs/Quint/voteBookkeeper.qnt | 122 +++++----- Specs/Quint/voteBookkeeperTest.qnt | 56 ++--- 12 files changed, 418 insertions(+), 421 deletions(-) delete mode 100644 Specs/Quint/0DecideNonProposerTest.itf.json rename Specs/Quint/{executor.qnt => driver.qnt} (78%) diff --git a/Code/itf/src/votekeeper.rs b/Code/itf/src/votekeeper.rs index 933de3137..41e8d181e 100644 --- a/Code/itf/src/votekeeper.rs +++ b/Code/itf/src/votekeeper.rs @@ -41,7 +41,7 @@ pub struct RoundVotes { pub round: Round, pub prevotes: VoteCount, pub precommits: VoteCount, - pub emitted_events: HashSet, + pub emitted_outputs: HashSet, #[serde(with = "As::>")] pub votes_addresses_weights: HashMap, } @@ -57,7 +57,7 @@ pub struct VoteCount { } #[derive(Clone, Debug, PartialEq, Eq, Deserialize, Hash)] -pub struct ExecutorEvent { +pub struct VoteKeeperOutput { #[serde(with = "As::")] pub round: Round, pub name: String, @@ -69,7 +69,7 @@ pub struct State { #[serde(rename = "voteBookkeeperTest::voteBookkeeperSM::bookkeeper")] pub bookkeeper: Bookkeeper, #[serde(rename = "voteBookkeeperTest::voteBookkeeperSM::lastEmitted")] - pub last_emitted: ExecutorEvent, + pub last_emitted: VoteKeeperOutput, #[serde(rename = "voteBookkeeperTest::voteBookkeeperSM::weightedVote")] #[serde(with = "As::<(Same, Integer, Integer)>")] pub weighted_vote: (Vote, Weight, Round), diff --git a/Code/itf/tests/votekeeper/runner.rs b/Code/itf/tests/votekeeper/runner.rs index b5c876e06..781629d1d 100644 --- a/Code/itf/tests/votekeeper/runner.rs +++ b/Code/itf/tests/votekeeper/runner.rs @@ -123,23 +123,23 @@ impl ItfRunner for VoteKeeperRunner { 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(); + let expected_outputs = &expected_round.emitted_outputs; + let actual_outputs = actual_round.emitted_outputs(); assert_eq!( - actual_events.len(), - expected_events.len(), + actual_outputs.len(), + expected_outputs.len(), "number of emitted events" ); let mut event_count = HashMap::new(); - for event in expected_events { + for event in expected_outputs { let count = event_count.entry(event.name.clone()).or_insert(0); *count += 1; } - for event in actual_events { + for event in actual_outputs { let event_name = match event { Output::PolkaValue(_) => "PolkaValue".into(), Output::PrecommitValue(_) => "PrecommitValue".into(), diff --git a/Code/vote/src/keeper.rs b/Code/vote/src/keeper.rs index fc4371f00..e81001f6d 100644 --- a/Code/vote/src/keeper.rs +++ b/Code/vote/src/keeper.rs @@ -25,7 +25,7 @@ where { votes: RoundVotes>, addresses_weights: RoundWeights, - emitted_msgs: BTreeSet>>, + emitted_outputs: BTreeSet>>, } impl PerRound @@ -36,7 +36,7 @@ where Self { votes: RoundVotes::new(), addresses_weights: RoundWeights::new(), - emitted_msgs: BTreeSet::new(), + emitted_outputs: BTreeSet::new(), } } @@ -48,8 +48,8 @@ where &self.addresses_weights } - pub fn emitted_msgs(&self) -> &BTreeSet>> { - &self.emitted_msgs + pub fn emitted_outputs(&self) -> &BTreeSet>> { + &self.emitted_outputs } } @@ -62,7 +62,7 @@ where Self { votes: self.votes.clone(), addresses_weights: self.addresses_weights.clone(), - emitted_msgs: self.emitted_msgs.clone(), + emitted_outputs: self.emitted_outputs.clone(), } } } @@ -76,7 +76,7 @@ where f.debug_struct("PerRound") .field("votes", &self.votes) .field("addresses_weights", &self.addresses_weights) - .field("emitted_msgs", &self.emitted_msgs) + .field("emitted_outputs", &self.emitted_outputs) .finish() } } @@ -144,7 +144,7 @@ where if skip_round { let msg = Output::SkipRound(vote.round()); - round.emitted_msgs.insert(msg.clone()); + round.emitted_outputs.insert(msg.clone()); return Some(msg); } } @@ -160,8 +160,8 @@ where let msg = threshold_to_output(vote.vote_type(), vote.round(), threshold); match msg { - Some(msg) if !round.emitted_msgs.contains(&msg) => { - round.emitted_msgs.insert(msg.clone()); + Some(msg) if !round.emitted_outputs.contains(&msg) => { + round.emitted_outputs.insert(msg.clone()); Some(msg) } _ => None, diff --git a/Specs/Quint/0DecideNonProposerTest.itf.json b/Specs/Quint/0DecideNonProposerTest.itf.json deleted file mode 100644 index 5d30f6911..000000000 --- a/Specs/Quint/0DecideNonProposerTest.itf.json +++ /dev/null @@ -1 +0,0 @@ -{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"consensus.qnt","status":"passed","description":"Created by Quint on Wed Oct 25 2023 15:38:28 GMT+0200 (Central European Summer Time)","timestamp":1698241108633},"vars":["system","_Event","_Result"],"states":[{"#meta":{"index":0},"_Event":{"height":-1,"name":"Initial","round":-1,"value":"","vr":-1},"_Result":{"decided":"","name":"","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":1,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"newRound","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":1},"_Event":{"height":1,"name":"NewRound","round":0,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":1,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":2},"_Event":{"height":1,"name":"NewRound","round":0,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":1,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":3},"_Event":{"height":1,"name":"Proposal","round":0,"value":"block","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":1,"id":"block","round":0,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":1,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":4},"_Event":{"height":1,"name":"Proposal","round":0,"value":"block","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":1,"id":"block","round":0,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":1,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":5},"_Event":{"height":1,"name":"ProposalAndPolkaAndValid","round":0,"value":"block","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":1,"id":"block","round":0,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":1,"lockedRound":0,"lockedValue":"block","p":"Josef","round":0,"step":"precommit","validRound":0,"validValue":"block"}]]}},{"#meta":{"index":6},"_Event":{"height":1,"name":"ProposalAndPolkaAndValid","round":0,"value":"block","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":1,"id":"block","round":0,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":1,"lockedRound":0,"lockedValue":"block","p":"Josef","round":0,"step":"precommit","validRound":0,"validValue":"block"}]]}},{"#meta":{"index":7},"_Event":{"height":1,"name":"ProposalAndCommitAndValid","round":0,"value":"block","vr":-1},"_Result":{"decided":"block","name":"decided","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":1,"lockedRound":0,"lockedValue":"block","p":"Josef","round":0,"step":"decided","validRound":0,"validValue":"block"}]]}},{"#meta":{"index":8},"_Event":{"height":1,"name":"ProposalAndCommitAndValid","round":0,"value":"block","vr":-1},"_Result":{"decided":"block","name":"decided","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":1,"lockedRound":0,"lockedValue":"block","p":"Josef","round":0,"step":"decided","validRound":0,"validValue":"block"}]]}},{"#meta":{"index":9},"_Event":{"height":2,"name":"NewHeight","round":0,"value":"","vr":-1},"_Result":{"decided":"","name":"","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"newRound","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":10},"_Event":{"height":2,"name":"NewHeight","round":0,"value":"","vr":-1},"_Result":{"decided":"","name":"","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"newRound","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":11},"_Event":{"height":2,"name":"NewRoundProposer","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"proposal","proposal":{"height":2,"proposal":"nextBlock","round":0,"src":"Josef","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":12},"_Event":{"height":2,"name":"NewRoundProposer","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"proposal","proposal":{"height":2,"proposal":"nextBlock","round":0,"src":"Josef","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":13},"_Event":{"height":2,"name":"Proposal","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nextBlock","round":0,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":14},"_Event":{"height":2,"name":"Proposal","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nextBlock","round":0,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":15},"_Event":{"height":2,"name":"PolkaAny","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrevote","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":16},"_Event":{"height":2,"name":"PolkaAny","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrevote","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":17},"_Event":{"height":2,"name":"TimeoutPrevote","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":0,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":18},"_Event":{"height":2,"name":"TimeoutPrevote","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":0,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":19},"_Event":{"height":2,"name":"PrecommitAny","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrecommit","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":20},"_Event":{"height":2,"name":"PrecommitAny","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrecommit","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":21},"_Event":{"height":2,"name":"TimeoutPrecommit","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"skipRound","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":22},"_Event":{"height":2,"name":"TimeoutPrecommit","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"skipRound","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":23},"_Event":{"height":2,"name":"NewRound","round":1,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":24},"_Event":{"height":2,"name":"NewRound","round":1,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":25},"_Event":{"height":2,"name":"TimeoutPropose","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":1,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":26},"_Event":{"height":2,"name":"TimeoutPropose","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":1,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":27},"_Event":{"height":2,"name":"PolkaNil","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":1,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":28},"_Event":{"height":2,"name":"PolkaNil","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":1,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":29},"_Event":{"height":2,"name":"PrecommitAny","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrecommit","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":30},"_Event":{"height":2,"name":"PrecommitAny","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrecommit","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":31},"_Event":{"height":2,"name":"TimeoutPrecommit","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"skipRound","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":2,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":32},"_Event":{"height":2,"name":"TimeoutPrecommit","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"skipRound","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":2,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":33},"_Event":{"height":2,"name":"NewRound","round":2,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":2,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":34},"_Event":{"height":2,"name":"NewRound","round":2,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":2,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":35},"_Event":{"height":2,"name":"ProposalInvalid","round":2,"value":"","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":2,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":2,"step":"prevote","validRound":-1,"validValue":"nil"}]]}}]} \ No newline at end of file diff --git a/Specs/Quint/Makefile b/Specs/Quint/Makefile index 2b9227986..a7477d691 100644 --- a/Specs/Quint/Makefile +++ b/Specs/Quint/Makefile @@ -1,7 +1,7 @@ parse: npx @informalsystems/quint parse asyncModelsTest.qnt npx @informalsystems/quint parse consensusTest.qnt - npx @informalsystems/quint parse executor.qnt + npx @informalsystems/quint parse driver.qnt npx @informalsystems/quint parse statemachineTest.qnt npx @informalsystems/quint parse voteBookkeeperTest.qnt .PHONY: parse diff --git a/Specs/Quint/consensus.qnt b/Specs/Quint/consensus.qnt index 3e282a873..e7cf66ece 100644 --- a/Specs/Quint/consensus.qnt +++ b/Specs/Quint/consensus.qnt @@ -3,14 +3,14 @@ /* TODO: check - whether we have "step" checks in place everywhere -- "the first time": checks here or in executor +- "the first time": checks here or in driver - check against arXiv - tests - types (e.g., heights in the messages) -- discuss "decision tree" in executor +- discuss "decision tree" in driver - Should we think again about the components and the boundaries (especially between - voteBookkeeper and executor) -- Do we need tests for executor and bookkeeping + voteBookkeeper and driver) +- Do we need tests for driver and bookkeeping - test id(v): most likely we need to change the type of Value_t as Quint doesn't have string operators. Perhaps we make Value_t = int and then id(v) = -v */ @@ -32,7 +32,7 @@ module consensus { type Timeout_t = str // the type of propose messages -type ProposeMsg_t = { +type Proposal_t = { src: Address_t, height: Height_t, round: Round_t, @@ -41,7 +41,7 @@ type ProposeMsg_t = { } // the type of Prevote and Precommit messages -type VoteMsg_t = { +type Vote_t = { src: Address_t, height: Height_t, round: Round_t, @@ -51,7 +51,7 @@ type VoteMsg_t = { type ConsensusState = { p: Address_t, - height : Height_t, + height: Height_t, round: Round_t, step: Step_t, // "newRound", propose, Prevote, Precommit, decided lockedRound: Round_t, @@ -65,15 +65,15 @@ pure def initConsensusState (v: Address_t) : ConsensusState = { p: v, round: -1, step: "newRound", - height : 0, + height: 0, lockedRound: -1, lockedValue: "nil", validRound: -1, validValue: "nil" } -type Event = { - name : str, +type ConsensusInput = { + name: str, height : Height_t, round: Round_t, value: Value_t, @@ -82,9 +82,9 @@ type Event = { // what is a good way to encode optionals? I do with default values type ConsensusOutput = { - name : str, - proposal: ProposeMsg_t, - voteMessage: VoteMsg_t, + name: str, + proposal: Proposal_t, + voteMessage: Vote_t, timeout: Timeout_t, decided: Value_t, skipRound: Round_t @@ -104,9 +104,7 @@ type ConsResult = { // pending: Set[ConsensusOutput], // TODO: not sure we need this } -type ConsensusEvent = str - -val ConsensusEvents = Set( +val ConsensusInputNames = Set( "NewHeight", // Setups the state-machine for a single-height execution "NewRound", // Start a new round, not as proposer. "NewRoundProposer", // Start a new round as proposer with the proposed Value. @@ -131,12 +129,12 @@ val ConsensusEvents = Set( "PrecommitValue(ValueId)", // Receive +2/3 Precommits for Value. */ -val noProp : ProposeMsg_t = {src: "", height: -1, round: -1, proposal: "", validRound: -1} -val noVote : VoteMsg_t = {src: "", height: -1, round: -1, step: "", id: ""} +val noProp : Proposal_t = {src: "", height: -1, round: -1, proposal: "", validRound: -1} +val noVote : Vote_t = {src: "", height: -1, round: -1, step: "", id: ""} val noTimeout : Timeout_t = "" val noDecided = "" val noSkipRound : Round_t = -1 -val defaultResult : ConsensusOutput = { +val defaultOutput : ConsensusOutput = { name: "", proposal: noProp, voteMessage: noVote, @@ -146,73 +144,73 @@ val defaultResult : ConsensusOutput = { -pure def NewHeight (state: ConsensusState, ev: Event) : ConsResult = { - if (ev.height > state.height) +pure def NewHeight (state: ConsensusState, input: ConsensusInput) : ConsResult = { + if (input.height > state.height) val newstate = { p: state.p, round: -1, // must be -1, as nothing should be done before a NewRound // function is called step: "newRound", - height : ev.height, + height : input.height, lockedRound: -1, lockedValue: "nil", validRound: -1, validValue: "nil" } - {cs: newstate, out: defaultResult } + {cs: newstate, out: defaultOutput } else - {cs: state, out: defaultResult } + {cs: state, out: defaultOutput } } // line 11.14 -pure def NewRoundProposer (state: ConsensusState, ev: Event) : ConsResult = { - if (ev.round > state.round) - val newstate = { ...state, round: ev.round, step: "propose"} +pure def NewRoundProposer (state: ConsensusState, input: ConsensusInput) : ConsResult = { + if (input.round > state.round) + val newstate = { ...state, round: input.round, step: "propose"} val proposal = if (state.validValue != "nil") state.validValue - else ev.value - val result = { ...defaultResult, name: "proposal", + else input.value + val result = { ...defaultOutput, name: "proposal", proposal: { src: state.p, height: state.height, - round: ev.round, + round: input.round, proposal: proposal, validRound: state.validRound}} {cs: newstate, out: result } else - {cs: state, out: defaultResult } + {cs: state, out: defaultOutput } } // line 11.20 -pure def NewRound (state: ConsensusState, ev: Event) : ConsResult = { - // TODO: discuss comment "ev.round must match state.round" - if (ev.round > state.round) - val newstate = { ...state, round: ev.round, step: "propose" } - val result = { ...defaultResult, name: "timeout", timeout: "TimeoutPropose"} - // We just report that a timeout should be started. The executor must take care +pure def NewRound (state: ConsensusState, input: ConsensusInput) : ConsResult = { + // TODO: discuss comment "input.round must match state.round" + if (input.round > state.round) + val newstate = { ...state, round: input.round, step: "propose" } + val result = { ...defaultOutput, name: "timeout", timeout: "TimeoutPropose"} + // We just report that a timeout should be started. The driver must take care // of figuring out whether it needs to record the round number and height per // timeout {cs: newstate, out: result} else - {cs: state, out: defaultResult } + {cs: state, out: defaultOutput } } // line 22 // Here it is assumed that // - the value has been checked to be valid // - it is for the current round -// The executor checks this upon receiving a propose message "ProposalMsg" -pure def Proposal (state: ConsensusState, ev: Event) : ConsResult = { +// The driver checks this upon receiving a propose message "ProposalMsg" +pure def Proposal (state: ConsensusState, input: ConsensusInput) : ConsResult = { if (state.step == "propose") val newstate = { ...state, step: "Prevote" } - if (state.lockedRound == -1 or state.lockedValue == ev.value) - val result = { ...defaultResult, name: "votemessage", + if (state.lockedRound == -1 or state.lockedValue == input.value) + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, step: "Prevote", - id: ev.value}} + id: input.value}} {cs: newstate, out: result} else - val result = { ...defaultResult, name: "votemessage", + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, @@ -220,15 +218,15 @@ pure def Proposal (state: ConsensusState, ev: Event) : ConsResult = { id: "nil"}} {cs: newstate, out: result} else - {cs: state, out: defaultResult} - // This should be dead code as the executor checks the step + {cs: state, out: defaultOutput} + // This should be dead code as the driver checks the step } // line 26 -pure def ProposalInvalid (state: ConsensusState, ev: Event) : ConsResult = { +pure def ProposalInvalid (state: ConsensusState, input: ConsensusInput) : ConsResult = { if (state.step == "propose") val newstate = state.with("step", "Prevote") - val result = { ...defaultResult, name: "votemessage", + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, @@ -236,23 +234,23 @@ pure def ProposalInvalid (state: ConsensusState, ev: Event) : ConsResult = { id: "nil"}} {cs: newstate, out: result} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } // line 28 -pure def ProposalAndPolkaPreviousAndValid (state: ConsensusState, ev: Event) : ConsResult = { - if (state.step == "propose" and ev.vr >= 0 and ev.vr < state.round) +pure def ProposalAndPolkaPreviousAndValid (state: ConsensusState, input: ConsensusInput) : ConsResult = { + if (state.step == "propose" and input.vr >= 0 and input.vr < state.round) val newstate = state.with("step", "Prevote") - if (state.lockedRound <= ev.vr or state.lockedValue == ev.value) - val result = { ...defaultResult, name: "votemessage", + if (state.lockedRound <= input.vr or state.lockedValue == input.value) + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, step: "Prevote", - id: ev.value}} + id: input.value}} {cs: newstate, out: result} else - val result = { ...defaultResult, name: "votemessage", + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, @@ -260,53 +258,53 @@ pure def ProposalAndPolkaPreviousAndValid (state: ConsensusState, ev: Event) : C id: "nil"}} {cs: newstate, out: result} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} // TODO: should we add the event to pending in this case. We would need to - // do this in the executor + // do this in the driver } // line 34 -pure def PolkaAny (state: ConsensusState, ev: Event) : ConsResult = { +pure def PolkaAny (state: ConsensusState, input: ConsensusInput) : ConsResult = { if (state.step == "Prevote") - val result = { ...defaultResult, name: "timeout", timeout: "TimeoutPrevote" } - // We just report that a timeout should be started. The executor must take care + val result = { ...defaultOutput, name: "timeout", timeout: "TimeoutPrevote" } + // We just report that a timeout should be started. The driver must take care // of figuring out whether it needs to record the round number and height per // timeout {cs: state, out: result} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } // line 36 -pure def ProposalAndPolkaAndValid (state: ConsensusState, ev: Event) : ConsResult = { - val auxState = { ...state, validValue: ev.value, validRound: state.round } +pure def ProposalAndPolkaAndValid (state: ConsensusState, input: ConsensusInput) : ConsResult = { + val auxState = { ...state, validValue: input.value, validRound: state.round } if (state.step == "Prevote") - val newstate = { ...auxState, lockedValue: ev.value, + val newstate = { ...auxState, lockedValue: input.value, lockedRound: state.round, step: "Precommit" } - val result = { ...defaultResult, name: "votemessage", + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, step: "Precommit", - id: ev.value}} + id: input.value}} {cs: newstate, out: result} else if (state.step == "Precommit") // TODO: check whether Daniel's comment // "if state > prevote, we should update the valid round!" // was properly addressed - {cs: auxState, out: defaultResult} + {cs: auxState, out: defaultOutput} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} // TODO: should we add the event to pending in this case. We would need to - // do this in the executor + // do this in the driver } // line 44 -pure def PolkaNil (state: ConsensusState, ev: Event) : ConsResult = { +pure def PolkaNil (state: ConsensusState, input: ConsensusInput) : ConsResult = { if (state.step == "Prevote") val newstate = { ...state, step: "Precommit"} - val result = { ...defaultResult, name: "votemessage", + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, @@ -314,39 +312,39 @@ pure def PolkaNil (state: ConsensusState, ev: Event) : ConsResult = { id: "nil"}} {cs: newstate, out: result} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } // line 47 -pure def PrecommitAny (state: ConsensusState, ev: Event) : ConsResult = { - val result = { ...defaultResult, name: "timeout", timeout: "TimeoutPrecommit" } +pure def PrecommitAny (state: ConsensusState, input: ConsensusInput) : ConsResult = { + val result = { ...defaultOutput, name: "timeout", timeout: "TimeoutPrecommit" } {cs: state, out: result} } // line 49 -pure def ProposalAndCommitAndValid (state: ConsensusState, ev: Event) : ConsResult = { +pure def ProposalAndCommitAndValid (state: ConsensusState, input: ConsensusInput) : ConsResult = { if (state.step != "decided") { val newstate = { ...state, step: "decided"} - val result = { ...defaultResult, name: "decided", decided: ev.value} + val result = { ...defaultOutput, name: "decided", decided: input.value} {cs: newstate, out: result} } else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } // line 55 -pure def RoundSkip (state: ConsensusState, ev: Event) : ConsResult = { - if (ev.round > state.round) - val result = { ...defaultResult, name: "skipRound", skipRound: ev.round } +pure def RoundSkip (state: ConsensusState, input: ConsensusInput) : ConsResult = { + if (input.round > state.round) + val result = { ...defaultOutput, name: "skipRound", skipRound: input.round } {cs: state, out: result} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } -pure def TimeoutPropose (state: ConsensusState, ev: Event) : ConsResult = { - if (ev.height == state.height and ev.round == state.round and state.step == "propose") +pure def TimeoutPropose (state: ConsensusState, input: ConsensusInput) : ConsResult = { + if (input.height == state.height and input.round == state.round and state.step == "propose") val newstate = { ...state, step: "Prevote"} - val result = { ...defaultResult, name: "votemessage", + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, @@ -354,14 +352,14 @@ pure def TimeoutPropose (state: ConsensusState, ev: Event) : ConsResult = { id: "nil"}} {cs: newstate, out: result} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } -pure def TimeoutPrevote (state: ConsensusState, ev: Event) : ConsResult = { - if (ev.height == state.height and ev.round == state.round and state.step == "Prevote") +pure def TimeoutPrevote (state: ConsensusState, input: ConsensusInput) : ConsResult = { + if (input.height == state.height and input.round == state.round and state.step == "Prevote") val newstate = { ...state, step: "Precommit"} // TODO: should we send precommit nil again ? - val result = { ...defaultResult, name: "votemessage", + val result = { ...defaultOutput, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, @@ -369,17 +367,17 @@ pure def TimeoutPrevote (state: ConsensusState, ev: Event) : ConsResult = { id: "nil"}} {cs: newstate, out: result} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } -pure def TimeoutPrecommit (state: ConsensusState, ev: Event) : ConsResult = { - if (ev.height == state.height and ev.round == state.round) +pure def TimeoutPrecommit (state: ConsensusState, input: ConsensusInput) : ConsResult = { + if (input.height == state.height and input.round == state.round) // TODO: here we should call newRound. For this we would need to know whether // we are proposer for next round. - val result = {...defaultResult, name: "skipRound", skipRound: state.round + 1} + val result = {...defaultOutput, name: "skipRound", skipRound: state.round + 1} {cs: state, out: result} else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } @@ -387,39 +385,39 @@ pure def TimeoutPrecommit (state: ConsensusState, ev: Event) : ConsResult = { * Main entry point * ********************************************************/ -pure def consensus (state: ConsensusState, ev: Event) : ConsResult = { - if (ev.name == "NewHeight") - NewHeight (state, ev) - else if (ev.name == "NewRoundProposer") - NewRoundProposer(state, ev) - else if (ev.name == "NewRound") - NewRound(state, ev) - else if (ev.name == "Proposal") - Proposal(state, ev) - else if (ev.name == "ProposalAndPolkaPreviousAndValid") - ProposalAndPolkaPreviousAndValid(state, ev) - else if (ev.name == "ProposalInvalid") - ProposalInvalid(state, ev) - else if (ev.name == "PolkaAny") - PolkaAny(state, ev) - else if (ev.name == "ProposalAndPolkaAndValid") - ProposalAndPolkaAndValid(state, ev) - else if (ev.name == "PolkaNil") - PolkaNil(state, ev) - else if (ev.name == "PrecommitAny") - PrecommitAny(state, ev) - else if (ev.name == "ProposalAndCommitAndValid") - ProposalAndCommitAndValid(state, ev) - else if (ev.name == "RoundSkip") - RoundSkip (state, ev) - else if (ev.name == "TimeoutPropose") - TimeoutPropose (state, ev) - else if (ev.name == "TimeoutPrevote") - TimeoutPrevote (state, ev) - else if (ev.name == "TimeoutPrecommit") - TimeoutPrecommit (state, ev) +pure def consensus (state: ConsensusState, input: ConsensusInput) : ConsResult = { + if (input.name == "NewHeight") + NewHeight (state, input) + else if (input.name == "NewRoundProposer") + NewRoundProposer(state, input) + else if (input.name == "NewRound") + NewRound(state, input) + else if (input.name == "Proposal") + Proposal(state, input) + else if (input.name == "ProposalAndPolkaPreviousAndValid") + ProposalAndPolkaPreviousAndValid(state, input) + else if (input.name == "ProposalInvalid") + ProposalInvalid(state, input) + else if (input.name == "PolkaAny") + PolkaAny(state, input) + else if (input.name == "ProposalAndPolkaAndValid") + ProposalAndPolkaAndValid(state, input) + else if (input.name == "PolkaNil") + PolkaNil(state, input) + else if (input.name == "PrecommitAny") + PrecommitAny(state, input) + else if (input.name == "ProposalAndCommitAndValid") + ProposalAndCommitAndValid(state, input) + else if (input.name == "RoundSkip") + RoundSkip (state, input) + else if (input.name == "TimeoutPropose") + TimeoutPropose (state, input) + else if (input.name == "TimeoutPrevote") + TimeoutPrevote (state, input) + else if (input.name == "TimeoutPrecommit") + TimeoutPrecommit (state, input) else - {cs: state, out: defaultResult} + {cs: state, out: defaultOutput} } } diff --git a/Specs/Quint/consensusTest.qnt b/Specs/Quint/consensusTest.qnt index fb7a2df24..2f2a79d45 100644 --- a/Specs/Quint/consensusTest.qnt +++ b/Specs/Quint/consensusTest.qnt @@ -8,9 +8,9 @@ import consensus.* from "./consensus" * Global state * ************************************************************************* */ -var system : Address_t -> ConsensusState -var _Result : ConsensusOutput -var _Event : Event +var system: Address_t -> ConsensusState +var _output: ConsensusOutput +var _input: ConsensusInput pure def initialProcess (name: Address_t) : ConsensusState = { @@ -19,8 +19,8 @@ pure def initialProcess (name: Address_t) : ConsensusState = { action init = all { system' = Map ("Josef" -> initialProcess("Josef")), - _Result' = defaultResult, - _Event' = { name : "Initial", + _output' = defaultOutput, + _input' = { name : "Initial", height : 0, round: -1, value: "", @@ -30,7 +30,7 @@ action init = all { // just to write a test. -action FireEvent(eventName: str, proc: Address_t, h: Height_t, r: Round_t, value: Value_t, vr: Round_t) : bool = all { +action FireInput(eventName: str, proc: Address_t, h: Height_t, r: Round_t, value: Value_t, vr: Round_t) : bool = all { val event = { name : eventName, height : h, round: r, @@ -39,86 +39,86 @@ action FireEvent(eventName: str, proc: Address_t, h: Height_t, r: Round_t, value val res = consensus(system.get(proc), event ) all { system' = system.put(proc, res.cs), - _Result' = res.out, - _Event' = event + _output' = res.out, + _input' = event } } action step = any { - nondet name = oneOf(ConsensusEvents) + nondet name = oneOf(ConsensusInputNames) nondet height = 1//oneOf(1.to(4)) nondet round = 0//oneOf(1.to(4)) nondet value = oneOf(Set("block 1", "block 2", "block 3")) nondet vr = oneOf(Set(-1, 1, 2, 3, 4)) - FireEvent(name, "Josef", height, round, value, vr) + FireInput(name, "Josef", height, round, value, vr) } action unchangedAll = all { system' = system, - _Result' = _Result, - _Event' = _Event, + _output' = _output, + _input' = _input, } // This test should call each event at least once run DecideNonProposerTest = { init - .then(FireEvent("NewRound", "Josef", 1, 0, "", -1)) + .then(FireInput("NewRound", "Josef", 1, 0, "", -1)) .then(all{ - assert(_Result.timeout == "TimeoutPropose"), - FireEvent("Proposal", "Josef", 1, 0, "block", -1)}) + assert(_output.timeout == "TimeoutPropose"), + FireInput("Proposal", "Josef", 1, 0, "block", -1)}) .then(all{ - assert(_Result.voteMessage.step == "Prevote" and _Result.voteMessage.id == "block"), - FireEvent("ProposalAndPolkaAndValid", "Josef", 1, 0, "block", -1)}) + assert(_output.voteMessage.step == "Prevote" and _output.voteMessage.id == "block"), + FireInput("ProposalAndPolkaAndValid", "Josef", 1, 0, "block", -1)}) .then(all{ - assert(_Result.voteMessage.step == "Precommit" and _Result.voteMessage.id == "block"), - FireEvent("ProposalAndCommitAndValid", "Josef", 1, 0, "block", -1)}) + assert(_output.voteMessage.step == "Precommit" and _output.voteMessage.id == "block"), + FireInput("ProposalAndCommitAndValid", "Josef", 1, 0, "block", -1)}) .then(all{ - assert(_Result.decided == "block"), - FireEvent("NewHeight", "Josef", system.get("Josef").height + 1, 0, "", -1)}) + assert(_output.decided == "block"), + FireInput("NewHeight", "Josef", system.get("Josef").height + 1, 0, "", -1)}) .then(all{ assert(system.get("Josef").height == 2), - FireEvent("NewRoundProposer", "Josef", 2, 0, "nextBlock", -1)}) + FireInput("NewRoundProposer", "Josef", 2, 0, "nextBlock", -1)}) .then(all{ - assert(_Result.timeout != "TimeoutPropose" and _Result.proposal.proposal == "nextBlock"), - FireEvent("Proposal", "Josef", 2, 0, "nextBlock", -1)}) // it is assumed that the proposer receives its own message + assert(_output.timeout != "TimeoutPropose" and _output.proposal.proposal == "nextBlock"), + FireInput("Proposal", "Josef", 2, 0, "nextBlock", -1)}) // it is assumed that the proposer receives its own message .then(all{ - assert(_Result.voteMessage.step == "Prevote" and system.get("Josef").step == "Prevote"), - FireEvent("PolkaAny", "Josef", 2, 0, "nextBlock", -1)}) + assert(_output.voteMessage.step == "Prevote" and system.get("Josef").step == "Prevote"), + FireInput("PolkaAny", "Josef", 2, 0, "nextBlock", -1)}) .then(all{ - assert(_Result.timeout == "TimeoutPrevote"), - FireEvent("TimeoutPrevote", "Josef", 2, 0, "nextBlock", -1)}) + assert(_output.timeout == "TimeoutPrevote"), + FireInput("TimeoutPrevote", "Josef", 2, 0, "nextBlock", -1)}) .then(all{ - assert(_Result.voteMessage.step == "Precommit" and _Result.voteMessage.id == "nil" and + assert(_output.voteMessage.step == "Precommit" and _output.voteMessage.id == "nil" and system.get("Josef").step == "Precommit"), - FireEvent("PrecommitAny", "Josef", 2, 0, "nextBlock", -1)}) + FireInput("PrecommitAny", "Josef", 2, 0, "nextBlock", -1)}) .then(all{ - assert(_Result.timeout == "TimeoutPrecommit"), - FireEvent("TimeoutPrecommit", "Josef", 2, 0, "nextBlock", -1)}) + assert(_output.timeout == "TimeoutPrecommit"), + FireInput("TimeoutPrecommit", "Josef", 2, 0, "nextBlock", -1)}) .then(all{ - assert(_Result.skipRound == 1), - FireEvent("NewRound", "Josef", 2, 1, "", -1)}) + assert(_output.skipRound == 1), + FireInput("NewRound", "Josef", 2, 1, "", -1)}) .then(all{ - assert(_Result.timeout == "TimeoutPropose"), - FireEvent("TimeoutPropose", "Josef", 2, 1, "nextBlock", -1)}) + assert(_output.timeout == "TimeoutPropose"), + FireInput("TimeoutPropose", "Josef", 2, 1, "nextBlock", -1)}) .then(all{ - assert(_Result.voteMessage.step == "Prevote" and _Result.voteMessage.id == "nil" and + assert(_output.voteMessage.step == "Prevote" and _output.voteMessage.id == "nil" and system.get("Josef").step == "Prevote"), - FireEvent("PolkaNil", "Josef", 2, 1, "nextBlock", -1)}) + FireInput("PolkaNil", "Josef", 2, 1, "nextBlock", -1)}) .then(all{ - assert(_Result.voteMessage.step == "Precommit" and _Result.voteMessage.id == "nil" and + assert(_output.voteMessage.step == "Precommit" and _output.voteMessage.id == "nil" and system.get("Josef").step == "Precommit"), - FireEvent("PrecommitAny", "Josef", 2, 1, "nextBlock", -1)}) + FireInput("PrecommitAny", "Josef", 2, 1, "nextBlock", -1)}) .then(all{ - assert(_Result.timeout == "TimeoutPrecommit"), - FireEvent("TimeoutPrecommit", "Josef", 2, 1, "nextBlock", -1)}) + assert(_output.timeout == "TimeoutPrecommit"), + FireInput("TimeoutPrecommit", "Josef", 2, 1, "nextBlock", -1)}) .then(all{ - assert(_Result.skipRound == 2), - FireEvent("NewRound", "Josef", 2, 2, "", -1)}) + assert(_output.skipRound == 2), + FireInput("NewRound", "Josef", 2, 2, "", -1)}) .then(all{ - assert(_Result.timeout == "TimeoutPropose"), - FireEvent("ProposalInvalid", "Josef", 2, 2, "", -1)}) + assert(_output.timeout == "TimeoutPropose"), + FireInput("ProposalInvalid", "Josef", 2, 2, "", -1)}) .then(all{ - assert(_Result.voteMessage.step == "Prevote" and _Result.voteMessage.id == "nil" and + assert(_output.voteMessage.step == "Prevote" and _output.voteMessage.id == "nil" and system.get("Josef").step == "Prevote"), unchangedAll }) diff --git a/Specs/Quint/executor.qnt b/Specs/Quint/driver.qnt similarity index 78% rename from Specs/Quint/executor.qnt rename to Specs/Quint/driver.qnt index 6aeb71a6a..c5326d9db 100644 --- a/Specs/Quint/executor.qnt +++ b/Specs/Quint/driver.qnt @@ -1,11 +1,11 @@ // -*- mode: Bluespec; -*- /* - TODO: round switch upon f+1 messages from the future is not done yet. We need to catch - the event from the bookkeeper + TODO: round switch upon f+1 messages from the future is not done yet. + We need to catch the event from the bookkeeper */ -module executor { +module driver { import consensus.* from "./consensus" import voteBookkeeper.* from "./voteBookkeeper" @@ -14,73 +14,73 @@ pure def initBookKeeper(totalVotingPower: int): Bookkeeper = { height: 0, totalWeight: totalVotingPower, rounds: Map() } -type ExecutorState = { +type DriverState = { bk : Bookkeeper, cs : ConsensusState, - proposals: Set[ProposeMsg_t], + proposals: Set[Proposal_t], valset: Address_t -> int, - executedEvents: List[(Event, Height_t, Round_t)], // We record that to have the information in the trace - pendingEvents: Set[(Event, Height_t, Round_t)], + executedInputs: List[(ConsensusInput, Height_t, Round_t)], // We record that to have the information in the trace + pendingInputs: Set[(ConsensusInput, Height_t, Round_t)], started: bool, - applyvotesResult: ExecutorEvent, //debug TODO + voteKeeperOutput: VoteKeeperOutput, //debug TODO chain : List[Value_t], nextValueToPropose: Value_t, } -pure def initExecutor (v: Address_t, vs: Address_t -> int) : ExecutorState = { +pure def initDriver (v: Address_t, vs: Address_t -> int) : DriverState = { val tvp = vs.keys().fold(0, (sum, key) => sum + vs.get(key)) { bk: initBookKeeper(tvp), cs: initConsensusState(v), proposals: Set(), valset: vs, - executedEvents: List(), - pendingEvents: Set(), + executedInputs: List(), + pendingInputs: Set(), started: false, - applyvotesResult: toEvent(0, "", {name: "", value: ""}), // debug + voteKeeperOutput: toVoteKeeperOutput(0, "", {name: "", value: ""}), // debug chain : List(), nextValueToPropose: "", } } type NodeState = { - es: ExecutorState, + es: DriverState, timeout: Set[(Timeout_t, Height_t, Round_t)], - incomingVotes: Set[VoteMsg_t], - incomingProposals: Set[ProposeMsg_t], + incomingVotes: Set[Vote_t], + incomingProposals: Set[Proposal_t], } pure def initNode (v: Address_t, vs: Address_t -> int) : NodeState = { - es: initExecutor(v,vs), + es: initDriver(v,vs), timeout: Set(), incomingVotes: Set(), incomingProposals: Set(), } -type ExecutorInput = { +type DriverInput = { name: str, // TODO: make a set of values. - proposal: ProposeMsg_t, - vote: VoteMsg_t, + proposal: Proposal_t, + vote: Vote_t, timeout: str, - event: Event, + csInput: ConsensusInput, nextValueToPropose: Value_t } -val defaultInput: ExecutorInput = { +val defaultInput: DriverInput = { name: "", proposal: { src: "", height: 0, round: 0, proposal: "", validRound: 0 }, vote: { src: "", height: 0, round: 0, step: "", id: "", }, timeout: "", - event: defaultEvent, + csInput: defaultConsensusInput, nextValueToPropose: "" } // this is to match the type from the bookkeeper. When we add heights there we should // unify -pure def toVote (v: VoteMsg_t) : Vote = +pure def toVote (v: Vote_t) : Vote = { 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 } +val defaultConsensusInput : ConsensusInput = { name : "", height : 0, round: 0, value: "", vr: 0 } /* encode the following decision tree @@ -104,7 +104,7 @@ Prevote -> feed all events to Consensus */ -val emptyProposal : ProposeMsg_t= +val emptyProposal : Proposal_t= { src: "none", height: 0, round: 0, proposal: "none", validRound: 0 } val emptyVote = @@ -125,9 +125,9 @@ pure def Proposer(valset: Address_t -> int, height: Height_t, round: Round_t) : else "v4" } -pure def getValue(es: ExecutorState) : Value_t = es.nextValueToPropose +pure def getValue(es: DriverState) : Value_t = es.nextValueToPropose -pure def valid(p: ProposeMsg_t) :bool = { +pure def valid(p: Proposal_t) :bool = { // for simulation, if the value is "invalid", so is the proposal // if this is to become "non-deterministic", we must push it // and its use into the state machine @@ -139,8 +139,8 @@ pure def id(v) = v type ConsensusCall = { - es: ExecutorState, - event: Event, + es: DriverState, + csInput: ConsensusInput, out: ConsensusOutput } @@ -148,24 +148,24 @@ pure def ListContains(list, value) = list.foldl(false, (s,x) => s or x == value) // check whether the event has been already sent to consensus. If not, do so. -pure def callConsensus (es: ExecutorState, bk: Bookkeeper, ev: Event) : (ExecutorState, ConsensusOutput) = { +pure def callConsensus (es: DriverState, bk: Bookkeeper, csInput: ConsensusInput) : (DriverState, ConsensusOutput) = { // Check whether we already executed the event already - if (es.executedEvents.ListContains((ev, es.cs.height, es.cs.round))) - ({ ...es, bk: bk, cs: es.cs }, defaultResult) + if (es.executedInputs.ListContains((csInput, es.cs.height, es.cs.round))) + ({ ...es, bk: bk, cs: es.cs }, defaultOutput) else // Go to consensus - val res = consensus(es.cs, ev) + val res = consensus(es.cs, csInput) // Record that we executed the event - val events = es.executedEvents.append((ev, res.cs.height, res.cs.round)) + val csInputs = es.executedInputs.append((csInput, res.cs.height, res.cs.round)) - ({ ...es, bk: bk, cs: res.cs, executedEvents: events }, res.out) + ({ ...es, bk: bk, cs: res.cs, executedInputs: csInputs }, res.out) } -// We do this if the executor receives a Precommit -pure def Precommit (es: ExecutorState, input: ExecutorInput, eev: ExecutorEvent) : (ExecutorState, ConsensusOutput) = { - if (eev.name == "PrecommitValue") - if (es.proposals.exists(x => eev.round == x.round and eev.value == id(x.proposal))) { +// We do this if the driver receives a Precommit +pure def Precommit (es: DriverState, input: DriverInput, vkOutput: VoteKeeperOutput) : (DriverState, ConsensusOutput) = { + if (vkOutput.name == "PrecommitValue") + if (es.proposals.exists(x => vkOutput.round == x.round and vkOutput.value == id(x.proposal))) { callConsensus(es, es.bk, { name : "ProposalAndCommitAndValid", height : input.vote.height, round: input.vote.round, @@ -173,14 +173,14 @@ pure def Precommit (es: ExecutorState, input: ExecutorInput, eev: ExecutorEvent) vr: -1}) } else { - if (eev.round == es.cs.round) { + if (vkOutput.round == es.cs.round) { callConsensus(es, es.bk, { name: "PrecommitAny", height: input.vote.height, round: input.vote.round, value: input.vote.id, vr: -1}) } - else if (eev.round > es.cs.round) { + else if (vkOutput.round > es.cs.round) { // if it is for a future round I can trigger skipround // TODO: should we really do this. It is dead code as the f+1 event already happened callConsensus(es, es.bk, { name: "RoundSkip", @@ -191,17 +191,17 @@ pure def Precommit (es: ExecutorState, input: ExecutorInput, eev: ExecutorEvent) } else { // messages from past round -> ignore - (es, defaultResult) + (es, defaultOutput) } } - else if (eev.name == "PrecommitAny" and eev.round == es.cs.round) { + else if (vkOutput.name == "PrecommitAny" and vkOutput.round == es.cs.round) { callConsensus(es, es.bk, { name: "PrecommitAny", height: input.vote.height, round: input.vote.round, value: input.vote.id, vr: -1}) } - else if (eev.name == "Skip" and eev.round > es.cs.round) + else if (vkOutput.name == "Skip" and vkOutput.round > es.cs.round) callConsensus(es, es.bk, { name: "RoundSkip", height: input.vote.height, round: input.vote.round, @@ -209,84 +209,84 @@ pure def Precommit (es: ExecutorState, input: ExecutorInput, eev: ExecutorEvent) vr: -1}) else // none of the supported Precommit events. Do nothing - (es, defaultResult) + (es, defaultOutput) } -// We do this if the executor receives a Prevote -pure def Prevote (es: ExecutorState, input: ExecutorInput, eev: ExecutorEvent) : (ExecutorState, ConsensusOutput) = { +// We do this if the driver receives a Prevote +pure def Prevote (es: DriverState, input: DriverInput, vkOutput: VoteKeeperOutput) : (DriverState, ConsensusOutput) = { // TODO: events do not have heights now. // TODO: Polka implications missing. - if (eev.name == "PolkaValue") - if (eev.round < es.cs.round and + if (vkOutput.name == "PolkaValue") + if (vkOutput.round < es.cs.round and es.proposals.exists(p => p.round == es.cs.round and - eev.round == p.validRound and id(p.proposal) == eev.value)) + vkOutput.round == p.validRound and id(p.proposal) == vkOutput.value)) callConsensus(es, es.bk, { name: "ProposalAndPolkaPreviousAndValid", height: es.cs.height, round: es.cs.round, - value: eev.value, - vr: eev.round}) + value: vkOutput.value, + vr: vkOutput.round}) // TODO: the value should come from the proposal - else if (eev.round == es.cs.round and + else if (vkOutput.round == es.cs.round and es.proposals.exists(p => p.round == es.cs.round and - id(p.proposal) == eev.value)) + id(p.proposal) == vkOutput.value)) callConsensus(es, es.bk, { name: "ProposalAndPolkaAndValid", height: es.cs.height, round: es.cs.round, - value: eev.value, - vr: eev.round}) + value: vkOutput.value, + vr: vkOutput.round}) else // we don't have a matching proposal so we do nothing // TODO: we might check whether it is for a future round and jump - (es, defaultResult) - else if (eev.name == "PolkaAny") - if (eev.round == es.cs.round) + (es, defaultOutput) + else if (vkOutput.name == "PolkaAny") + if (vkOutput.round == es.cs.round) // call consensus and remember that we did it callConsensus(es, es.bk, { name: "PolkaAny", height: es.cs.height, round: es.cs.round, - value: eev.value, - vr: eev.round}) + value: vkOutput.value, + vr: vkOutput.round}) else // TODO: we might check whether it is for a future round and jump - (es, defaultResult) - else if (eev.name == "PolkaNil" and eev.round == es.cs.round) + (es, defaultOutput) + else if (vkOutput.name == "PolkaNil" and vkOutput.round == es.cs.round) callConsensus(es, es.bk, { name: "PolkaNil", height: es.cs.height, round: es.cs.round, - value: eev.value, - vr: eev.round}) - else if (eev.name == "Skip" and eev.round > es.cs.round) + value: vkOutput.value, + vr: vkOutput.round}) + else if (vkOutput.name == "Skip" and vkOutput.round > es.cs.round) callConsensus(es, es.bk, { name: "RoundSkip", height: input.vote.height, round: input.vote.round, value: input.vote.id, vr: -1}) else - (es, defaultResult) + (es, defaultOutput) } -// We do this if a timeout expires at the executor -pure def Timeout (es: ExecutorState, input: ExecutorInput) : (ExecutorState, ConsensusOutput) = { +// We do this if a timeout expires at the driver +pure def Timeout (es: DriverState, input: DriverInput) : (DriverState, ConsensusOutput) = { // TODO: We assume that the timeout event is always for the current round. If this is not // the case, we need to encode it in the input to which round the timeout belongs - val event: Event = {name: input.timeout, + val csInput: ConsensusInput = {name: input.timeout, height: es.cs.height, round: es.cs.round, value: "", vr: 0} - callConsensus(es, es.bk, event) + callConsensus(es, es.bk, csInput) } -// We do this if the executor receives a proposal -pure def ProposalMsg (es: ExecutorState, input: ExecutorInput) : (ExecutorState, ConsensusOutput) = { +// We do this if the driver receives a proposal +pure def ProposalMsg (es: DriverState, input: DriverInput) : (DriverState, ConsensusOutput) = { val newES = { ...es, proposals: es.proposals.union(Set(input.proposal))} if (input.proposal.src != Proposer(es.valset, input.proposal.height, input.proposal.round)) // proposer does not match the height/round of the proposal // keep ES (don't use newES here), that is, drop proposal - (es, defaultResult) + (es, defaultOutput) else if (valid(input.proposal)) val receivedCommit = checkThreshold( newES.bk, input.proposal.round, @@ -307,7 +307,7 @@ pure def ProposalMsg (es: ExecutorState, input: ExecutorInput) : (ExecutorState, else if (input.proposal.round != es.cs.round or input.proposal.height != es.cs.height) // the proposal is from the right proposer and valid, but not for this round // keep the proposal, do nothing else - (newES, defaultResult) + (newES, defaultOutput) else // for current round and q, valid, and from right proposer val receivedPolkaValidRoundVal = checkThreshold(newES.bk, @@ -352,7 +352,7 @@ pure def ProposalMsg (es: ExecutorState, input: ExecutorInput) : (ExecutorState, value: id(input.proposal.proposal), vr: input.proposal.validRound}) else - (newES, defaultResult) + (newES, defaultOutput) else if (newES.cs.step == "Prevote" or newES.cs.step == "Precommit") if (receivedCommitCurrentVal) // here we need to call both, Commit and Polka. @@ -364,7 +364,7 @@ pure def ProposalMsg (es: ExecutorState, input: ExecutorInput) : (ExecutorState, vr: input.proposal.validRound}, newES.cs.height, newES.cs.round) - callConsensus( { ...newES, pendingEvents: newES.pendingEvents.union(Set(pend))}, + callConsensus( { ...newES, pendingInputs: newES.pendingInputs.union(Set(pend))}, newES.bk, { name: "ProposalAndCommitAndValid", height: newES.cs.height, @@ -380,34 +380,34 @@ pure def ProposalMsg (es: ExecutorState, input: ExecutorInput) : (ExecutorState, value: id(input.proposal.proposal), vr: input.proposal.validRound}) else - (newES, defaultResult) + (newES, defaultOutput) else - (newES, defaultResult) + (newES, defaultOutput) else // (not(valid(input.proposal))) // keep ES (don't use newES here), that is, drop proposal if (es.cs.step == "propose" and es.cs.round == input.proposal.round and es.cs.height == input.proposal.height) if (checkThreshold(es.bk, es.cs.round, "Prevote", {name: "Value", value: id(input.proposal.proposal)})) - val event: Event = {name: "ProposalAndPolkaAndInValid", + val csInput: ConsensusInput = {name: "ProposalAndPolkaAndInValid", height: es.cs.height, round: es.cs.round, value: id(input.proposal.proposal), vr: input.proposal.validRound} - callConsensus(es, es.bk, event) + callConsensus(es, es.bk, csInput) else - val event: Event = {name: "ProposalInvalid", + val csInput: ConsensusInput = {name: "ProposalInvalid", height: es.cs.height, round: es.cs.round, value: id(input.proposal.proposal), vr: input.proposal.validRound} - callConsensus(es, es.bk, event) + callConsensus(es, es.bk, csInput) else - (es, defaultResult) + (es, defaultOutput) } // We do this when we need to jump to a new round -pure def skip (es: ExecutorState, r: int) : (ExecutorState, ConsensusOutput) = { +pure def skip (es: DriverState, r: int) : (DriverState, ConsensusOutput) = { // line 15 val prop = if (es.cs.validValue != "nil") es.cs.validValue else getValue(es) @@ -430,15 +430,15 @@ pure def skip (es: ExecutorState, r: int) : (ExecutorState, ConsensusOutput) = { // We do this when we have decided -pure def decided (es: ExecutorState, res: ConsensusOutput) : (ExecutorState, ConsensusOutput) = { +pure def decided (es: DriverState, res: ConsensusOutput) : (DriverState, ConsensusOutput) = { // here we call consensus to set a new height, that is, to initialize the state machine // and then we call skip to start round 0 /* // The following can be used to get to the next height. For now this // function does nothing - // If we choose to move getValue out of the executor logic into the environment (gossip) + // If we choose to move getValue out of the driver logic into the environment (gossip) // then, we would not do this here, but expect the environment to create a (to be defined) - // ExecutorInput + // DriverInput val s1 = callConsensus(es, es.bk, {name : "NewHeight", height : es.cs.height + 1, round: -1, @@ -451,15 +451,15 @@ pure def decided (es: ExecutorState, res: ConsensusOutput) : (ExecutorState, Con // take input out of pending events and then call consensus with that event -// We do this when the executor is asked to work on pending events -pure def PendingEvent (es: ExecutorState, input: ExecutorInput) : (ExecutorState, ConsensusOutput) = { - val newState = { ...es, pendingEvents: es.pendingEvents.exclude(Set((input.event, es.cs.height, es.cs.round)))} - callConsensus(newState, es.bk, input.event) +// We do this when the driver is asked to work on pending events +pure def PendingInput (es: DriverState, input: DriverInput) : (DriverState, ConsensusOutput) = { + val newState = { ...es, pendingInputs: es.pendingInputs.exclude(Set((input.csInput, es.cs.height, es.cs.round)))} + callConsensus(newState, es.bk, input.csInput) } -pure def setValue(es: ExecutorState, value: Value_t) : (ExecutorState, ConsensusOutput) = - ({ ...es, nextValueToPropose: value }, defaultResult) +pure def setValue(es: DriverState, value: Value_t) : (DriverState, ConsensusOutput) = + ({ ...es, nextValueToPropose: value }, defaultOutput) @@ -468,8 +468,8 @@ pure def setValue(es: ExecutorState, value: Value_t) : (ExecutorState, Consensus * Main entry point * ********************************************************/ -// TODO: return ConsensusEvent so that we know from outside what event was fired. -pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, ConsensusOutput) = { +// TODO: return ConsensusInput so that we know from outside what event was fired. +pure def driver (es: DriverState, input: DriverInput) : (DriverState, ConsensusOutput) = { // TODO: shall we check whether the sender actually is in the validator set if (input.name == "proposal") { val res = ProposalMsg(es, input) @@ -482,9 +482,9 @@ pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, Co } else if (input.name == "votemessage" and input.vote.step == "Precommit") { val res = applyVote(es.bk, toVote(input.vote), es.valset.get(input.vote.src), es.cs.round) - val newES = { ...es, bk: res.bookkeeper, applyvotesResult: res.event} + val newES = { ...es, bk: res.bookkeeper, voteKeeperOutput: res.output } // only a commit event can come here. - val cons_res = Precommit(newES, input, res.event) + val cons_res = Precommit(newES, input, res.output) if (cons_res._2.name == "decided") decided (cons_res._1, cons_res._2) else if (cons_res._2.name == "skipRound") @@ -494,9 +494,9 @@ pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, Co } else if (input.name == "votemessage" and input.vote.step == "Prevote") { val res = applyVote(es.bk, toVote(input.vote), es.valset.get(input.vote.src), es.cs.round) - val newES = { ...es, bk: res.bookkeeper, applyvotesResult: res.event} + val newES = { ...es, bk: res.bookkeeper, voteKeeperOutput: res.output} // only a commit event can come here. - val cons_res = Prevote(newES, input, res.event) + val cons_res = Prevote(newES, input, res.output) if (cons_res._2.name == "decided") // TODO: dead branch. But we should put this after consensus call logic into a function decided (cons_res._1, cons_res._2) @@ -511,8 +511,8 @@ pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, Co if (res._2.name == "skipRound") skip (res._1, res._2.skipRound) // skip starts a new round. This may involve getValue. If we choose to move the getValue - // logic out of the executor, we wouldn't call skip here but add a (to be defined) - // ExecutorInput + // logic out of the driver, we wouldn't call skip here but add a (to be defined) + // DriverInput else res } @@ -522,12 +522,12 @@ pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, Co skip (new, 0) } else if (input.name == "pending") { - PendingEvent(es, input) + PendingInput(es, input) } else if (input.name == "SetNextProposedValue") setValue(es, input.nextValueToPropose) else - (es, defaultResult) + (es, defaultOutput) } @@ -535,7 +535,7 @@ pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, Co // timeouts, etc.) the node should act. // currently this is linked in via the state machine. But we can move it into // the functional layer/ -pure def nextAction (state: NodeState) : (NodeState, ExecutorInput) = { +pure def nextAction (state: NodeState) : (NodeState, DriverInput) = { if (not(state.es.started)) (state, { ...defaultInput, name: "start" }) @@ -563,7 +563,7 @@ pure def nextAction (state: NodeState) : (NodeState, ExecutorInput) = { val newstate = { ...state, timeout: state.timeout.exclude(Set(timeout))} (newstate, { ...defaultInput, name: "timeout", timeout: timeout._1}) - else if (state.es.pendingEvents != Set()) + else if (state.es.pendingInputs != Set()) // this might be cheating as we look into the "es" (state, { ...defaultInput, name: "pending" }) // TODO: In the "starkBFT Spec" Google doc, it is written that pending events @@ -574,7 +574,7 @@ pure def nextAction (state: NodeState) : (NodeState, ExecutorInput) = { } // This function can be used to control test runs better. -pure def nextActionCommand (state: NodeState, command: str) : (NodeState, ExecutorInput) = { +pure def nextActionCommand (state: NodeState, command: str) : (NodeState, DriverInput) = { if (command == "start" and not(state.es.started)) (state, { ...defaultInput, name: "start" }) @@ -602,7 +602,7 @@ pure def nextActionCommand (state: NodeState, command: str) : (NodeState, Execut val newstate = { ...state, timeout: state.timeout.exclude(Set(timeout))} (newstate, { ...defaultInput, name: "timeout", timeout: timeout._1}) - else if (command == "pending" and state.es.pendingEvents != Set()) + else if (command == "pending" and state.es.pendingInputs != Set()) // this might be cheating as we look into the "es" (state, { ...defaultInput, name: "pending" }) diff --git a/Specs/Quint/statemachineAsync.qnt b/Specs/Quint/statemachineAsync.qnt index f714141d8..5192b5ef6 100644 --- a/Specs/Quint/statemachineAsync.qnt +++ b/Specs/Quint/statemachineAsync.qnt @@ -16,8 +16,8 @@ module statemachineAsync { -import executor.* from "./executor" -export executor.* +import driver.* from "./driver" +export driver.* import consensus.* from "./consensus" export consensus.* import voteBookkeeper.* from "./voteBookkeeper" @@ -38,26 +38,26 @@ const Heights : Set[Height_t] val RoundsOrNil = Rounds.union(Set(-1)) val Steps = Set("Prevote", "Precommit") -val AllFaultyVotes : Set[VoteMsg_t] = +val AllFaultyVotes : Set[Vote_t] = tuples(Faulty, Heights, Rounds, Values, Steps) .map(t => { src: t._1, height: t._2, round: t._3, id: t._4, step: t._5 }) -// val AllFaultyVotes : Set[VoteMsg_t] = +// val AllFaultyVotes : Set[Vote_t] = // tuples(Faulty, Heights, Rounds, Values, Steps) // .map(((p, h, r, v, s)) => { src: p, height: h, round: r, id: v, step: s }) -val AllFaultyProposals : Set[ProposeMsg_t] = +val AllFaultyProposals : Set[Proposal_t] = tuples(Faulty, Heights, Rounds, Values, RoundsOrNil) .map(t => { src: t._1, height: t._2, round: t._3, proposal: t._4, validRound: t._5 }) // Global State var system : Address_t -> NodeState -var propBuffer : Address_t -> Set[ProposeMsg_t] -var voteBuffer : Address_t -> Set[VoteMsg_t] -var _hist: { validator: Address_t, input: ExecutorInput, output: ConsensusOutput } +var propBuffer : Address_t -> Set[Proposal_t] +var voteBuffer : Address_t -> Set[Vote_t] +var _hist: { validator: Address_t, input: DriverInput, output: ConsensusOutput } -val ConsensusOutputInv = consensusOutputs.union(Set(defaultResult.name)).contains(_hist.output.name) +val ConsensusOutputInv = consensusOutputs.union(Set(defaultOutput.name)).contains(_hist.output.name) action unchangedAll = all { @@ -77,17 +77,17 @@ action init = all { system' = Correct.mapBy(v => initNode(v, validatorSet)), propBuffer' = Correct.mapBy(v => Set()), voteBuffer' = Correct.mapBy(v => Set()), - _hist' = { validator: "INIT", input: defaultInput, output: defaultResult } + _hist' = { validator: "INIT", input: defaultInput, output: defaultOutput } } // Put the proposal into the buffers of all validators -pure def sendProposal (buffer: Address_t -> Set[ProposeMsg_t], prop: ProposeMsg_t) : Address_t -> Set[ProposeMsg_t] = { +pure def sendProposal (buffer: Address_t -> Set[Proposal_t], prop: Proposal_t) : Address_t -> Set[Proposal_t] = { buffer.keys().mapBy(x => { buffer.get(x).union(Set(prop)) }) } // Put the vote into the inbuffers of all validators -pure def sendVote (sys: Address_t -> Set[VoteMsg_t], vote: VoteMsg_t) : Address_t -> Set[VoteMsg_t] = { +pure def sendVote (sys: Address_t -> Set[Vote_t], vote: Vote_t) : Address_t -> Set[Vote_t] = { sys.keys().mapBy(x => { ...sys.get(x).union(Set(vote)) }) } @@ -101,11 +101,11 @@ pure def startTimeout (sys: Address_t -> NodeState, v: Address_t, toName: str) : action valStep(v: Address_t) : bool = { // pick action - val input = system.get(v).nextAction() // TODO: nextAction could go within executor boundary + val input = system.get(v).nextAction() // TODO: nextAction could go within driver boundary // remove action from v val sys1 = system.put(v, input._1) - // call executor - val res = executor(sys1.get(v).es, input._2) + // call driver + val res = driver(sys1.get(v).es, input._2) all { // update v's state after the step val sys = sys1.put(v, { ...sys1.get(v), es: res._1}) @@ -130,7 +130,7 @@ action valStep(v: Address_t) : bool = { else if (res._2.name == "skipRound") all { propBuffer' = propBuffer, voteBuffer' = voteBuffer, - //skipRound should never leave the executor + //skipRound should never leave the driver system' = sys, } else all { @@ -144,7 +144,7 @@ action valStep(v: Address_t) : bool = { } action setNextValueToPropose(v: Address_t, value: Value_t) : bool = all { - val res = executor(system.get(v).es, { ...defaultInput, name: "SetNextProposedValue", nextValueToPropose: value}) + val res = driver(system.get(v).es, { ...defaultInput, name: "SetNextProposedValue", nextValueToPropose: value}) val newNS = { ...system.get(v), es: res._1} system' = system.put(v, newNS), _hist' = _hist, @@ -152,7 +152,7 @@ action setNextValueToPropose(v: Address_t, value: Value_t) : bool = all { voteBuffer' = voteBuffer, } -action deliverProposal(v: Address_t, p: ProposeMsg_t) : bool = all { +action deliverProposal(v: Address_t, p: Proposal_t) : bool = all { propBuffer.get(v).union(AllFaultyProposals).contains(p), // the proposal must be sent or from a faulty node propBuffer' = propBuffer.put(v, propBuffer.get(v).exclude(Set(p))), system' = system.put(v, { ...system.get(v), incomingProposals: system.get(v).incomingProposals.union(Set(p)) }), @@ -160,7 +160,7 @@ action deliverProposal(v: Address_t, p: ProposeMsg_t) : bool = all { voteBuffer' = voteBuffer, } -action deliverVote(v: Address_t, vote: VoteMsg_t) : bool = all { +action deliverVote(v: Address_t, vote: Vote_t) : bool = all { voteBuffer.get(v).union(AllFaultyVotes).contains(vote), // the vote must be sent or from a faulty node voteBuffer' = voteBuffer.put(v, voteBuffer.get(v).exclude(Set(vote))), system' = system.put(v, { ...system.get(v), incomingVotes: system.get(v).incomingVotes.union(Set(vote)) }), diff --git a/Specs/Quint/statemachineTest.qnt b/Specs/Quint/statemachineTest.qnt index 1e2115ae8..da367de2d 100644 --- a/Specs/Quint/statemachineTest.qnt +++ b/Specs/Quint/statemachineTest.qnt @@ -12,7 +12,7 @@ module statemachineTest { -import executor.* from "./executor" +import driver.* from "./driver" import consensus.* from "./consensus" import voteBookkeeper.* from "./voteBookkeeper" @@ -20,23 +20,23 @@ val validators = Set("v1", "v2", "v3", "v4") val validatorSet = validators.mapBy(x => 1) var system : Address_t -> NodeState -var _hist: (str, ExecutorInput, ConsensusOutput) +var _hist: (str, DriverInput, ConsensusOutput) //var _histSimple: (str, str, str) action init = all { system' = validators.mapBy(v => initNode(v, validatorSet)), - _hist' = ("INIT", defaultInput, defaultResult) + _hist' = ("INIT", defaultInput, defaultOutput) // _histSimple' = ("INIT", "", "") } // Put the proposal into the inbuffers of all validators -pure def deliverProposal (sys: Address_t -> NodeState, prop: ProposeMsg_t) : Address_t -> NodeState = { +pure def deliverProposal (sys: Address_t -> NodeState, prop: Proposal_t) : Address_t -> NodeState = { sys.keys().mapBy(x => { ...sys.get(x), incomingProposals: sys.get(x).incomingProposals.union(Set(prop)) }) } // Put the vote into the inbuffers of all validators -pure def deliverVote (sys: Address_t -> NodeState, vote: VoteMsg_t) : Address_t -> NodeState = { +pure def deliverVote (sys: Address_t -> NodeState, vote: Vote_t) : Address_t -> NodeState = { sys.keys().mapBy(x => { ...sys.get(x), incomingVotes: sys.get(x).incomingVotes.union(Set(vote)) }) } @@ -53,11 +53,11 @@ pure def startTimeout (sys: Address_t -> NodeState, v: Address_t, toName: str) : // hardly ever are fired action valStep(v: Address_t) : bool = { // pick action - val input = system.get(v).nextAction() // TODO: nextAction could go within executor boundary + val input = system.get(v).nextAction() // TODO: nextAction could go within driver boundary // remove action from v val sys1 = system.put(v, input._1) - // call executor - val res = executor(sys1.get(v).es, input._2) + // call driver + val res = driver(sys1.get(v).es, input._2) all { // update v's state after the step val sys = sys1.put(v, { ...sys1.get(v), es: res._1}) @@ -69,7 +69,7 @@ action valStep(v: Address_t) : bool = { else if (res._2.name == "timeout") system' = startTimeout(sys, v, res._2.timeout) else if (res._2.name == "skipRound") - //skipRound should never leave the executor + //skipRound should never leave the driver system' = sys else system' = sys, @@ -79,7 +79,7 @@ action valStep(v: Address_t) : bool = { } action setNextValueToPropose(v: Address_t, value: Value_t) : bool = all { - val res = executor(system.get(v).es, { ...defaultInput, name: "SetNextProposedValue", nextValueToPropose: value}) + val res = driver(system.get(v).es, { ...defaultInput, name: "SetNextProposedValue", nextValueToPropose: value}) val newNS = { ...system.get(v), es: res._1} system' = system.put(v, newNS), _hist' = _hist @@ -101,8 +101,8 @@ action valStepCommand(v: Address_t, command: str) : bool = { val input = system.get(v).nextActionCommand(command) // remove action from v val sys1 = system.put(v, input._1) - // call executor - val res = executor(sys1.get(v).es, input._2) + // call driver + val res = driver(sys1.get(v).es, input._2) all { // update v's state after the step val sys = sys1.put(v, { ...sys1.get(v), es: res._1}) @@ -114,7 +114,7 @@ action valStepCommand(v: Address_t, command: str) : bool = { else if (res._2.name == "timeout") system' = startTimeout(sys, v, res._2.timeout) else if (res._2.name == "skipRound") - //skipRound should never leave the executor + //skipRound should never leave the driver system' = sys else system' = sys, diff --git a/Specs/Quint/voteBookkeeper.qnt b/Specs/Quint/voteBookkeeper.qnt index 3e9bca343..1e1c1676f 100644 --- a/Specs/Quint/voteBookkeeper.qnt +++ b/Specs/Quint/voteBookkeeper.qnt @@ -51,7 +51,7 @@ module voteBookkeeper { round: Round, prevotes: VoteCount, precommits: VoteCount, - emittedEvents: Set[ExecutorEvent], + emittedOutputs: Set[VoteKeeperOutput], votesAddressesWeights: Address -> Weight } @@ -66,18 +66,18 @@ module voteBookkeeper { pure def valueThreshold(value) = { name: "Value", value: value } pure def isThresholdOnValue(t: Threshold): bool = t.name == "Value" - type ExecutorEvent = { + type VoteKeeperOutput = { 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" } + pure def noOutput(round) = { round: round, name: "None", value: "null" } + pure def polkaValueOutput(round, value) = { round: round, name: "PolkaValue", value: value } + pure def polkaNilOutput(round) = { round: round, name: "PolkaNil", value: "null" } + pure def polkaAnyOutput(round) = { round: round, name: "PolkaAny", value: "null" } + pure def precommitValueOutput(round, value) = { round: round, name: "PrecommitValue", value: value } + pure def precommitAnyOutput(round) = { round: round, name: "PrecommitAny", value: "null" } + pure def skipOutput(round) = { round: round, name: "Skip", value: "null" } type Bookkeeper = { height: Height, @@ -96,7 +96,7 @@ module voteBookkeeper { round: round, prevotes: newVoteCount(totalWeight), precommits: newVoteCount(totalWeight), - emittedEvents: Set(), + emittedOutputs: Set(), votesAddressesWeights: Map() } @@ -188,64 +188,64 @@ module voteBookkeeper { } else unreachedThreshold - // Given a round, voteType and threshold, return the corresponding ExecutorEvent - pure def toEvent(round: Round, voteType: VoteType, threshold: Threshold): ExecutorEvent = + // Given a round, voteType and threshold, return the corresponding VoteKeeperOutput + pure def toVoteKeeperOutput(round: Round, voteType: VoteType, threshold: Threshold): VoteKeeperOutput = if (threshold == unreachedThreshold) - noEvent(round) + noOutput(round) // prevote else if (voteType.isPrevote() and threshold.isThresholdOnValue()) - polkaValueEvent(round, threshold.value) + polkaValueOutput(round, threshold.value) else if (voteType.isPrevote() and threshold == nilThreshold) - polkaNilEvent(round) + polkaNilOutput(round) else if (voteType.isPrevote() and threshold == anyThreshold) - polkaAnyEvent(round) + polkaAnyOutput(round) // precommit else if (voteType.isPrecommit() and threshold.isThresholdOnValue()) - precommitValueEvent(round, threshold.value) + precommitValueOutput(round, threshold.value) else if (voteType.isPrecommit() and threshold.in(Set(anyThreshold, nilThreshold))) - precommitAnyEvent(round) + precommitAnyOutput(round) else if (threshold == skipThreshold) - skipEvent(round) + skipOutput(round) else - noEvent(round) + noOutput(round) - run toEventTest = + run toVoteKeeperOutputTest = val round = 10 all { - assert(toEvent(round, "Prevote", unreachedThreshold) == noEvent(round)), - assert(toEvent(round, "Precommit", unreachedThreshold) == noEvent(round)), + assert(toVoteKeeperOutput(round, "Prevote", unreachedThreshold) == noOutput(round)), + assert(toVoteKeeperOutput(round, "Precommit", unreachedThreshold) == noOutput(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(toVoteKeeperOutput(round, "Prevote", anyThreshold) == polkaAnyOutput(round)), + assert(toVoteKeeperOutput(round, "Prevote", nilThreshold) == polkaNilOutput(round)), + assert(toVoteKeeperOutput(round, "Prevote", valueThreshold("val1")) == polkaValueOutput(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(toVoteKeeperOutput(round, "Precommit", anyThreshold) == precommitAnyOutput(round)), + assert(toVoteKeeperOutput(round, "Precommit", nilThreshold) == precommitAnyOutput(round)), + assert(toVoteKeeperOutput(round, "Precommit", valueThreshold("val1")) == precommitValueOutput(round, "val1")), - assert(toEvent(round, "Prevote", skipThreshold) == skipEvent(round)), - assert(toEvent(round, "Precommit", skipThreshold) == skipEvent(round)), + assert(toVoteKeeperOutput(round, "Prevote", skipThreshold) == skipOutput(round)), + assert(toVoteKeeperOutput(round, "Precommit", skipThreshold) == skipOutput(round)), - assert(toEvent(round, "Precommit", { name: "Error", value: "null" }) == noEvent(round)), - assert(toEvent(round, "Error", anyThreshold) == noEvent(round)), + assert(toVoteKeeperOutput(round, "Precommit", { name: "Error", value: "null" }) == noOutput(round)), + assert(toVoteKeeperOutput(round, "Error", anyThreshold) == noOutput(round)), } - // Executor interface - type BKResult = { bookkeeper: Bookkeeper, event: ExecutorEvent } + // Driver interface + type BKOutput = { bookkeeper: Bookkeeper, output: VoteKeeperOutput } - // Called by the executor when it receives a vote. The function takes the following steps: + // Called by the driver 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 corresponding ExecutorEvent. - // - Otherwise, the function returns a no-threshold event. + // - If there exist a threshold and has not emitted before, the function returns the corresponding VoteKeeperOutput. + // - Otherwise, the function returns a no-threshold output. // - 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 } = + pure def applyVote(keeper: Bookkeeper, vote: Vote, weight: Weight, currentRound: Round): { bookkeeper: Bookkeeper, output: VoteKeeperOutput } = val round = vote.round val roundVotes = keeper.rounds.getOrElse(round, newRoundVotes(keeper.height, round, keeper.totalWeight)) @@ -264,16 +264,16 @@ module voteBookkeeper { // Combined weight of all validators at this height val combinedWeight = updatedVotesAddressesWeights.mapSumValues() - val finalEvent = + val finalOutput = if (vote.round > currentRound and isSkip(combinedWeight, keeper.totalWeight)) - skipEvent(vote.round) + skipOutput(vote.round) else val threshold = computeThreshold(updatedVoteCount, vote.value) - val event = toEvent(vote.round, vote.typ, threshold) - if (not(event.in(roundVotes.emittedEvents))) - event + val output = toVoteKeeperOutput(vote.round, vote.typ, threshold) + if (not(output.in(roundVotes.emittedOutputs))) + output else - noEvent(vote.round) + noOutput(vote.round) val updatedRoundVotes = if (vote.typ.isPrevote()) @@ -282,12 +282,12 @@ module voteBookkeeper { roundVotes.with("precommits", updatedVoteCount) val updatedRoundVotes2 = updatedRoundVotes .with("votesAddressesWeights", updatedVotesAddressesWeights) - .with("emittedEvents", roundVotes.emittedEvents.setAddIf(finalEvent, finalEvent.name != "None")) + .with("emittedOutputs", roundVotes.emittedOutputs.setAddIf(finalOutput, finalOutput.name != "None")) val updatedBookkeeper = keeper .with("rounds", keeper.rounds.mapSafeSet(vote.round, updatedRoundVotes2)) - { bookkeeper: updatedBookkeeper, event: finalEvent } + { bookkeeper: updatedBookkeeper, output: finalOutput } run applyVoteTest = val roundVotes: RoundVotes = { @@ -295,7 +295,7 @@ module voteBookkeeper { round: 0, prevotes: { totalWeight: 4, votesAddresses: Set(), valuesWeights: Map("v1" -> 1, Nil -> 3) }, precommits: { totalWeight: 4, votesAddresses: Set(), valuesWeights: Map() }, - emittedEvents: Set(), + emittedOutputs: Set(), votesAddressesWeights: Map(), } val vk: Bookkeeper = { height: 0, totalWeight: 4, rounds: Map(0 -> roundVotes) } @@ -305,16 +305,16 @@ module voteBookkeeper { 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"), + assert(o1.output.name == "None"), + assert(o2.output.name == "None"), + assert(o3.output.name == "PrecommitAny"), + assert(o4.output.name == "None"), + assert(o5.output.name == "Skip"), } - // Called by the executor to check if there is a specific threshold for a given round and voteType. + // Called by the driver 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 + // - The function does not consider Skip threshold. This because if the driver receives a Skip output // and do not act on it, this means that it will never do it in the future. We should discuss that this // is the case. pure def checkThreshold(keeper: Bookkeeper, round: Round, voteType: VoteType, threshold: Threshold): bool = @@ -380,8 +380,8 @@ module voteBookkeeper { 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 + // The output outputing from applying a weighted vote to the bookkeeper. + var lastEmitted: VoteKeeperOutput // ************************************************************************ // Actions @@ -399,13 +399,13 @@ module voteBookkeeper { lastEmitted' = { round: -1, name: "", value: "null" } } - // The vote keeper receives a weighted vote and produces an event. + // The vote keeper receives a weighted vote and produces an output. action applyVoteAction(vote: Vote, weight: Weight, currentRound: Round): bool = - val result = applyVote(bookkeeper, vote, weight, currentRound) + val output = applyVote(bookkeeper, vote, weight, currentRound) all { weightedVote' = (vote, weight, currentRound), - bookkeeper' = result.bookkeeper, - lastEmitted' = result.event + bookkeeper' = output.bookkeeper, + lastEmitted' = output.output } } diff --git a/Specs/Quint/voteBookkeeperTest.qnt b/Specs/Quint/voteBookkeeperTest.qnt index 44419ca27..95c369e70 100644 --- a/Specs/Quint/voteBookkeeperTest.qnt +++ b/Specs/Quint/voteBookkeeperTest.qnt @@ -22,71 +22,71 @@ module voteBookkeeperTest { run synchronousConsensusTest = initWith(1, 100) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 60, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == polkaValueEvent(1, "val1"))) + .then(_assert(lastEmitted == polkaValueOutput(1, "val1"))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "bob"}, 30, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Precommit", height: 1, round: 1, value: "val1", address: "bob"}, 30, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Precommit", height: 1, round: 1, value: "val1", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Precommit", height: 1, round: 1, value: "val1", address: "alice"}, 60, 1)) - .then(_assert(lastEmitted == precommitValueEvent(1, "val1"))) + .then(_assert(lastEmitted == precommitValueOutput(1, "val1"))) // Reaching PolkaAny run polkaAnyTest = initWith(1, 100) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 60, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "nil", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == polkaAnyEvent(1))) + .then(_assert(lastEmitted == polkaAnyOutput(1))) // Reaching PolkaNil run polkaNilTest = initWith(1, 100) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "nil", address: "alice"}, 60, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "nil", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == polkaNilEvent(1))) + .then(_assert(lastEmitted == polkaNilOutput(1))) // Reaching Skip via n+1 threshold with prevotes from two validators at a future round run skipSmallQuorumAllPrevotesTest = initWith(1, 100) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 60, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == noEvent(2))) + .then(_assert(lastEmitted == noOutput(2))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "bob"}, 30, 1)) - .then(_assert(lastEmitted == skipEvent(2))) + .then(_assert(lastEmitted == skipOutput(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(1, 90) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 10, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 20, 1)) - .then(_assert(lastEmitted == noEvent(2))) + .then(_assert(lastEmitted == noOutput(2))) .then(applyVoteAction({typ: "Precommit", height: 1, round: 2, value: "val1", address: "john"}, 20, 1)) - .then(_assert(lastEmitted != skipEvent(2))) + .then(_assert(lastEmitted != skipOutput(2))) // Reaching Skip via f+1 threshold with one prevote and one precommit from two validators at a future round run skipSmallQuorumMixedVotesTwoValsTest = initWith(1, 80) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 50, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == noEvent(2))) + .then(_assert(lastEmitted == noOutput(2))) .then(applyVoteAction({typ: "Precommit", height: 1, round: 2, value: "val1", address: "bob"}, 20, 1)) - .then(_assert(lastEmitted == skipEvent(2))) + .then(_assert(lastEmitted == skipOutput(2))) // Reaching Skip via 2f+1 threshold with a single prevote from a single validator at a future round run skipQuorumSinglePrevoteTest = 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(all { assert(lastEmitted == noOutput(1)), allUnchanged }) .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 60, 1)) - .then(all { assert(lastEmitted == skipEvent(2)), allUnchanged }) + .then(all { assert(lastEmitted == skipOutput(2)), allUnchanged }) // Reaching Skip via 2f+1 threshold with a single precommit from a single validator at a future round run skipQuorumSinglePrecommitTest = @@ -94,27 +94,27 @@ module voteBookkeeperTest { .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", height: 1, round: 2, value: "val1", address: "john"}, 60, 1)) - .then(_assert(lastEmitted == skipEvent(2))) + .then(_assert(lastEmitted == skipOutput(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(1, 100) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 10, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 30, 1)) - .then(_assert(lastEmitted == noEvent(2))) + .then(_assert(lastEmitted == noOutput(2))) .then(applyVoteAction({typ: "Precommit", height: 1, round: 2, value: "val1", address: "john"}, 30, 1)) - .then(_assert(lastEmitted != skipEvent(2))) + .then(_assert(lastEmitted != skipOutput(2))) // Reaching Skip via 2f+1 threshold with one prevote and one precommit from two validators at a future round run skipQuorumMixedVotesTwoValsTest = initWith(1, 80) .then(applyVoteAction({typ: "Prevote", height: 1, round: 1, value: "val1", address: "alice"}, 20, 1)) - .then(_assert(lastEmitted == noEvent(1))) + .then(_assert(lastEmitted == noOutput(1))) .then(applyVoteAction({typ: "Prevote", height: 1, round: 2, value: "val1", address: "john"}, 10, 1)) - .then(_assert(lastEmitted == noEvent(2))) + .then(_assert(lastEmitted == noOutput(2))) .then(applyVoteAction({typ: "Precommit", height: 1, round: 2, value: "val1", address: "bob"}, 50, 1)) - .then(_assert(lastEmitted == skipEvent(2))) + .then(_assert(lastEmitted == skipOutput(2))) // **************************************************************************** // Properties that define an expected final state (for generating traces)