Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

spec: Refactor votekeeper using quint's new sum types #76

Merged
merged 28 commits into from
Dec 8, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
bcd7ee4
Use sum type for VoteType
hvanz Nov 20, 2023
c30d73c
Use sum type for Threshold
hvanz Nov 20, 2023
7aff9de
Use sum type for ExecutorEvent
hvanz Nov 20, 2023
96b4fc1
Use sum type for Value
hvanz Nov 20, 2023
aa5476c
Update executor using votekeeper's new types
hvanz Nov 22, 2023
d9e422c
Move unit tests near definition
hvanz Nov 28, 2023
0a853c6
Merge branch 'main' into hvanz/votekeeper-sum-types
hvanz Nov 28, 2023
084032a
Fix SM and tests after merge
hvanz Nov 30, 2023
9626e83
Add types module
hvanz Dec 6, 2023
b11edf2
Merge branch 'main' into hvanz/votekeeper-sum-types
hvanz Dec 6, 2023
f224614
Comment out id in types
hvanz Dec 6, 2023
08e096c
spec: remove initialRound
hvanz Dec 7, 2023
c4608b6
fix spec
hvanz Dec 7, 2023
f9547a5
Update itf tests
hvanz Dec 7, 2023
31c0663
cargo fmt
hvanz Dec 7, 2023
e6f0d22
Rename conflicting definitions
hvanz Dec 7, 2023
fd8f39c
Merge branch 'main' into hvanz/votekeeper-sum-types
hvanz Dec 7, 2023
808b028
Use `itf` native support for sum types (#111)
romac Dec 7, 2023
6f1ce15
spec driver: Bring some changes from main + some nits
hvanz Dec 7, 2023
12068fa
spec driver: another missing fix
hvanz Dec 7, 2023
c63267e
Rename voteBookkeepesSM to Models
hvanz Dec 7, 2023
0a05dc0
Move votekeeper types to common types
hvanz Dec 7, 2023
0a6a274
Workspace dependencies
romac Dec 8, 2023
224661a
Small cleanup
romac Dec 8, 2023
e1b1c6f
Ensure syntax highlighting on GitHub
romac Dec 8, 2023
661ab33
spec: Rename outputs to keep it consistent with other modules
hvanz Dec 8, 2023
643283e
Revert "spec: Rename outputs to keep it consistent with other modules"
hvanz Dec 8, 2023
9f6f3d4
Rename enum variants
romac Dec 8, 2023
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion Code/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -22,10 +22,11 @@ async-trait = "0.1"
ed25519-consensus = "2.1.0"
futures = "0.3"
glob = "0.3.0"
itf = "0.2.1"
itf = "0.2.2"
num-bigint = "0.4.4"
rand = { version = "0.8.5", features = ["std_rng"] }
serde = "1.0"
serde_json = "1.0"
serde_with = "3.4"
sha2 = "0.10.8"
signature = "2.1.0"
6 changes: 4 additions & 2 deletions Code/itf/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -9,14 +9,16 @@ license.workspace = true
publish.workspace = true

[dependencies]
itf = { workspace = true }
rand = { workspace = true }
malachite-common = { version = "0.1.0", path = "../common" }
malachite-vote = { version = "0.1.0", path = "../vote" }
malachite-test = { version = "0.1.0", path = "../test" }

itf = { workspace = true }
rand = { workspace = true }
num-bigint = { workspace = true, features = ["serde"] }
serde = { workspace = true, features = ["derive"] }
serde_json = { workspace = true }
serde_with = { workspace = true }
glob = { workspace = true }

[dev-dependencies]
Expand Down
1 change: 1 addition & 0 deletions Code/itf/src/lib.rs
Original file line number Diff line number Diff line change
@@ -1,2 +1,3 @@
pub mod types;
pub mod utils;
pub mod votekeeper;
34 changes: 34 additions & 0 deletions Code/itf/src/types.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
use itf::de::{As, Integer};
use serde::Deserialize;

pub type Height = i64;
pub type Weight = i64;
pub type Round = i64;
pub type Address = String;
pub type NonNilValue = String;

#[derive(Clone, Debug, PartialEq, Eq, Hash, Deserialize)]
#[serde(tag = "tag", content = "value")]
pub enum Value {
Nil,
Val(NonNilValue),
}

#[derive(Clone, Debug, PartialEq, Eq, Deserialize)]
#[serde(tag = "tag", content = "value")]
pub enum VoteType {
Prevote,
Precommit,
}

#[derive(Clone, Debug, PartialEq, Eq, Deserialize)]
#[serde(rename_all = "camelCase")]
pub struct Vote {
pub vote_type: VoteType,
#[serde(with = "As::<Integer>")]
pub height: Height,
#[serde(with = "As::<Integer>")]
pub round: Round,
pub value_id: Value,
pub src_address: Address,
}
75 changes: 45 additions & 30 deletions Code/itf/src/votekeeper.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,33 +3,59 @@ use std::collections::{HashMap, HashSet};

use serde::Deserialize;

pub type Height = i64;
pub type Weight = i64;
pub type Round = i64;
pub type Address = String;
pub type Value = String;
pub type VoteType = String;
use crate::types::{Address, Height, NonNilValue, Round, Value, Vote, Weight};

#[derive(Clone, Debug, PartialEq, Eq, Deserialize)]
#[serde(rename_all = "camelCase")]
pub struct Bookkeeper {
#[serde(tag = "tag", content = "value")]
pub enum WeightedVote {
#[serde(rename = "NoWeightedVote")]
NoVote,

#[serde(rename = "WV")]
#[serde(with = "As::<(Same, Integer, Integer)>")]
Vote(Vote, Weight, Round),
}

#[derive(Clone, Debug, PartialEq, Eq, Hash, Deserialize)]
#[serde(tag = "tag", content = "value")]
pub enum VoteKeeperOutput {
#[serde(rename = "NoVKOutput")]
NoOutput,

#[serde(rename = "PolkaAnyVKOutput")]
#[serde(with = "As::<Integer>")]
pub height: Height,
PolkaAny(Round),

#[serde(rename = "PolkaNilVKOutput")]
#[serde(with = "As::<Integer>")]
pub total_weight: Weight,
#[serde(with = "As::<HashMap<Integer, Same>>")]
pub rounds: HashMap<Round, RoundVotes>,
PolkaNil(Round),

#[serde(rename = "PolkaValueVKOutput")]
#[serde(with = "As::<(Integer, Same)>")]
PolkaValue(Round, NonNilValue),

#[serde(rename = "PrevoteAnyVKOutput")]
#[serde(with = "As::<Integer>")]
PrecommitAny(Round),

#[serde(rename = "PrevoteNilVKOutput")]
#[serde(with = "As::<(Integer, Same)>")]
PrecommitValue(Round, NonNilValue),

#[serde(rename = "SkipVKOutput")]
#[serde(with = "As::<Integer>")]
Skip(Round),
}

#[derive(Clone, Debug, PartialEq, Eq, Deserialize)]
pub struct Vote {
pub typ: VoteType,
#[serde(rename_all = "camelCase")]
pub struct Bookkeeper {
#[serde(with = "As::<Integer>")]
pub height: Height,
#[serde(with = "As::<Integer>")]
pub round: Round,
pub value: Value,
pub address: Address,
pub total_weight: Weight,
#[serde(with = "As::<HashMap<Integer, Same>>")]
pub rounds: HashMap<Round, RoundVotes>,
}

#[derive(Clone, Debug, PartialEq, Eq, Deserialize)]
Expand All @@ -56,21 +82,10 @@ pub struct VoteCount {
pub votes_addresses: HashSet<Address>,
}

#[derive(Clone, Debug, PartialEq, Eq, Deserialize, Hash)]
pub struct VoteKeeperOutput {
#[serde(with = "As::<Integer>")]
pub round: Round,
pub name: String,
pub value: Value,
}

#[derive(Clone, Debug, PartialEq, Eq, Deserialize)]
#[serde(rename_all = "camelCase")]
pub struct State {
#[serde(rename = "voteBookkeeperTest::voteBookkeeperSM::bookkeeper")]
pub bookkeeper: Bookkeeper,
#[serde(rename = "voteBookkeeperTest::voteBookkeeperSM::lastEmitted")]
pub last_emitted: VoteKeeperOutput,
#[serde(rename = "voteBookkeeperTest::voteBookkeeperSM::weightedVote")]
#[serde(with = "As::<(Same, Integer, Integer)>")]
pub weighted_vote: (Vote, Weight, Round),
pub weighted_vote: WeightedVote,
}
122 changes: 69 additions & 53 deletions Code/itf/tests/votekeeper/runner.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
use std::collections::HashMap;

use malachite_common::{Context, Round, Value};
use malachite_itf::votekeeper::State;
use malachite_itf::types::{Value as ModelValue, VoteType};
use malachite_itf::votekeeper::VoteKeeperOutput::*;
use malachite_itf::votekeeper::{State, WeightedVote};
use malachite_test::{Address, Height, TestContext, Vote};
use malachite_vote::{
keeper::{Output, VoteKeeper},
Expand All @@ -23,12 +25,11 @@ impl ItfRunner for VoteKeeperRunner {
type Error = ();

fn init(&mut self, expected: &Self::ExpectedState) -> Result<Self::ActualState, Self::Error> {
// Initialize VoteKeeper from the initial total_weight from the first state in the model.
let (input_vote, weight, current_round) = &expected.weighted_vote;
let round = Round::new(input_vote.round);
let height = expected.bookkeeper.height as u64;
let total_weight = expected.bookkeeper.total_weight as u64;
println!(
"🔵 init: vote={:?}, round={:?}, value={:?}, address={:?}, weight={:?}, current_round={:?}",
input_vote.typ, round, input_vote.value, input_vote.address, weight, current_round
"🔵 init: height={:?}, total_weight={:?}",
height, total_weight
);
Ok(VoteKeeper::new(
expected.bookkeeper.total_weight as u64,
Expand All @@ -41,61 +42,68 @@ impl ItfRunner for VoteKeeperRunner {
actual: &mut Self::ActualState,
expected: &Self::ExpectedState,
) -> Result<Self::Result, Self::Error> {
// Build step to execute.
let (input_vote, weight, current_round) = &expected.weighted_vote;
let round = Round::new(input_vote.round);
let height = Height::new(input_vote.height as u64);
let value = value_from_model(&input_vote.value);
let address = self.address_map.get(input_vote.address.as_str()).unwrap();
let vote = match input_vote.typ.as_str() {
"Prevote" => Vote::new_prevote(height, round, value, *address),
"Precommit" => Vote::new_precommit(height, round, value, *address),
_ => unreachable!(),
};
println!(
"🔵 step: vote={:?}, round={:?}, value={:?}, address={:?}, weight={:?}, current_round={:?}",
input_vote.typ, round, value, input_vote.address, weight, current_round
);
match &expected.weighted_vote {
WeightedVote::NoVote => Err(()),

WeightedVote::Vote(input_vote, weight, current_round) => {
// Build step to execute.
let round = Round::new(input_vote.round);
let height = Height::new(input_vote.height as u64);
let value = value_from_model(&input_vote.value_id);
let address = self
.address_map
.get(input_vote.src_address.as_str())
.unwrap();
let vote = match &input_vote.vote_type {
VoteType::Prevote => Vote::new_prevote(height, round, value, *address),
VoteType::Precommit => Vote::new_precommit(height, round, value, *address),
};
println!(
"🔵 step: vote={:?}, round={:?}, value={:?}, address={:?}, weight={:?}, current_round={:?}",
input_vote.vote_type, round, value, input_vote.src_address, weight, current_round
);

// Execute step.
Ok(actual.apply_vote(vote, *weight as u64, Round::new(*current_round)))
// Execute step.
Ok(actual.apply_vote(vote, *weight as u64, Round::new(*current_round)))
}
}
}

fn result_invariant(
&self,
result: &Self::Result,
expected: &Self::ExpectedState,
) -> Result<bool, Self::Error> {
// Get expected result.
let expected_result = &expected.last_emitted;
println!(
"🟣 result: model={:?}({:?},{:?}), code={:?}",
expected_result.name, expected_result.value, expected_result.round, result
);
// Check result against expected result.
match result {
Some(result) => match result {
Output::PolkaValue(value) => {
assert_eq!(expected_result.name, "PolkaValue");
Some(result) => match (result, expected_result) {
// TODO: check expected_round
romac marked this conversation as resolved.
Show resolved Hide resolved
(Output::PolkaNil, PolkaNil(_expected_round)) => (),
(Output::PolkaAny, PolkaAny(_expected_round)) => (),
(Output::PolkaValue(value), PolkaValue(_expected_round, expected_value)) => {
assert_eq!(
value_from_model(&expected_result.value).as_ref(),
Some(value)
Some(value),
value_from_model(&ModelValue::Val(expected_value.to_string())).as_ref()
);
}
Output::PrecommitValue(value) => {
assert_eq!(expected_result.name, "PrecommitValue");
(Output::PrecommitAny, PrecommitAny(_expected_round)) => (),
(
Output::PrecommitValue(value),
PrecommitValue(_expected_round, expected_value),
) => {
assert_eq!(
value_from_model(&expected_result.value).as_ref(),
Some(value)
Some(value),
value_from_model(&ModelValue::Val(expected_value.to_string())).as_ref()
);
}
Output::SkipRound(round) => {
assert_eq!(expected_result.name, "Skip");
assert_eq!(&Round::new(expected_result.round), round);
(Output::SkipRound(round), Skip(expected_round)) => {
assert_eq!(round, &Round::new(*expected_round));
}
(actual, expected) => {
panic!("actual: {:?}, expected: {:?}", actual, expected)
}
msg => assert_eq!(expected_result.name, format!("{msg:?}")),
},
None => assert_eq!(expected_result.name, "None"),
None => assert_eq!(*expected_result, NoOutput),
}
Ok(true)
}
Expand Down Expand Up @@ -135,18 +143,29 @@ impl ItfRunner for VoteKeeperRunner {
let mut event_count = HashMap::new();

for event in expected_outputs {
let count = event_count.entry(event.name.clone()).or_insert(0);
let event_name = match event {
PolkaAny(_) => "PolkaAny".to_string(),
PolkaNil(_) => "PolkaNil".to_string(),
PolkaValue(_, _) => "PolkaValue".to_string(),
PrecommitAny(_) => "PrecommitAny".to_string(),
PrecommitValue(_, _) => "PrecommitValue".to_string(),
Skip(_) => "Skip".to_string(),
_ => format!("{event:?}"),
};

let count = event_count.entry(event_name).or_insert(0);
*count += 1;
}

for event in actual_outputs {
let event_name = match event {
Output::PolkaValue(_) => "PolkaValue".into(),
Output::PrecommitValue(_) => "PrecommitValue".into(),
Output::SkipRound(_) => "Skip".into(),
Output::PolkaValue(_) => "PolkaValue".to_string(),
Output::PrecommitValue(_) => "PrecommitValue".to_string(),
Output::SkipRound(_) => "Skip".to_string(),
_ => format!("{event:?}"),
};
let count = event_count.entry(event_name.clone()).or_insert(0);

let count = event_count.entry(event_name).or_insert(0);
*count -= 1;
}

Expand All @@ -156,13 +175,10 @@ impl ItfRunner for VoteKeeperRunner {

let expected_addresses_weights = &expected_round.votes_addresses_weights;
let actual_addresses_weights = &actual_round.addresses_weights().get_inner();
for address in expected_addresses_weights.keys() {
for (address, expected_weight) in expected_addresses_weights {
assert_eq!(
actual_addresses_weights.get(self.address_map.get(address).unwrap()),
expected_addresses_weights
.get(address)
.map(|&w| w as u64)
.as_ref(),
Some(&(*expected_weight as u64)),
"weight for address {address:?}"
);
}
Expand Down
18 changes: 9 additions & 9 deletions Code/itf/tests/votekeeper/utils.rs
Original file line number Diff line number Diff line change
@@ -1,19 +1,19 @@
use std::collections::HashMap;

use malachite_itf::votekeeper::Value;
use malachite_itf::types::Value;
use malachite_test::{Address, ValueId};

pub const ADDRESSES: [&str; 3] = ["alice", "bob", "john"];
pub const NIL_VALUE: &str = "nil";

pub fn value_from_model(value: &Value) -> Option<ValueId> {
match value.as_str() {
NIL_VALUE => None,
"proposal" => Some(0.into()),
"val1" => Some(1.into()),
"val2" => Some(2.into()),
"val3" => Some(3.into()),
_ => unimplemented!("unknown value {value:?}"),
match value {
Value::Nil => None,
Value::Val(v) => match v.as_str() {
"v1" => Some(1.into()),
"v2" => Some(2.into()),
"v3" => Some(3.into()),
_ => unimplemented!("unknown value {value:?}"),
},
}
}

Expand Down
5 changes: 4 additions & 1 deletion Specs/Quint/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,10 @@ test: test-con test-sm test-vk
.PHONY: test

verify:
npx @informalsystems/quint verify --max-steps 10 --invariant Inv voteBookkeeperTest.qnt
npx @informalsystems/quint verify --max-steps 10 \
--main voteBookkeeperModels --init=VK1::init --step=VK1::step \
--invariant VK1::Inv \
voteBookkeeperModels.qnt
.PHONY: verify

# Generate traces by random simulation from properties describing the last desired state.
Expand Down
Loading
Loading