diff --git a/.github/workflows/spec.yaml b/.github/workflows/spec.yaml index 469eb169..6c1971fb 100644 --- a/.github/workflows/spec.yaml +++ b/.github/workflows/spec.yaml @@ -16,11 +16,11 @@ jobs: - name: Install node uses: actions/setup-node@v4 with: - node-version: ">= 18" + node-version: 20 check-latest: true - name: Install quint - run: npm i @informalsystems/quint -g + run: npm i @informalsystems/quint@0.21.0 -g - name: Run test run: cd spec && make test diff --git a/spec/protocol-spec/experiments/n6f1b0.qnt b/spec/protocol-spec/experiments/n6f1b0.qnt index 1c818d9e..9b97f80f 100644 --- a/spec/protocol-spec/experiments/n6f1b0.qnt +++ b/spec/protocol-spec/experiments/n6f1b0.qnt @@ -1,3 +1,4 @@ +// -*- mode: Bluespec; -*- // A specification instance for n=6, f=1, and no Byzantine faults module n6f1b0 { import replica( @@ -11,4 +12,4 @@ module n6f1b0 { VALID_BLOCKS = Set("val_b0", "val_b1"), INVALID_BLOCKS = Set("inv_b3") ).* from "../replica" -} \ No newline at end of file +} diff --git a/spec/protocol-spec/experiments/n6f1b0_guided_no_proposing_leader.qnt b/spec/protocol-spec/experiments/n6f1b0_guided_no_proposing_leader.qnt index b26c1374..773b3351 100644 --- a/spec/protocol-spec/experiments/n6f1b0_guided_no_proposing_leader.qnt +++ b/spec/protocol-spec/experiments/n6f1b0_guided_no_proposing_leader.qnt @@ -1,3 +1,4 @@ +// -*- mode: Bluespec; -*- // A specification instance for n=6, f=1, and 1 Byzantine fault // // Due to import/export limitations of Quint, use the definitions starting with g_: @@ -38,4 +39,4 @@ module n6f1b1_two_blocks { ] ).* from "../guided_replica" -} \ No newline at end of file +} diff --git a/spec/protocol-spec/experiments/n6f1b1.qnt b/spec/protocol-spec/experiments/n6f1b1.qnt index c675ef99..62d518e5 100644 --- a/spec/protocol-spec/experiments/n6f1b1.qnt +++ b/spec/protocol-spec/experiments/n6f1b1.qnt @@ -1,3 +1,4 @@ +// -*- mode: Bluespec; -*- // A specification instance for n=6, f=1, and 1 Byzantine fault module n6f1b1 { import replica( @@ -11,4 +12,4 @@ module n6f1b1 { VALID_BLOCKS = Set("val_b0", "val_b1"), INVALID_BLOCKS = Set("inv_b3") ).* from "../replica" -} \ No newline at end of file +} diff --git a/spec/protocol-spec/experiments/n6f1b1_guided_dead_lock.qnt b/spec/protocol-spec/experiments/n6f1b1_guided_dead_lock.qnt index 8d8f399a..12e7548e 100644 --- a/spec/protocol-spec/experiments/n6f1b1_guided_dead_lock.qnt +++ b/spec/protocol-spec/experiments/n6f1b1_guided_dead_lock.qnt @@ -1,3 +1,5 @@ +// -*- mode: Bluespec; -*- +// // A specification instance for n=6, f=1, and 1 Byzantine fault // /// Test a liveness issue where some validators have the HighQC but don't have the block payload and have to wait for it, @@ -42,4 +44,4 @@ module n6f1b1_two_blocks { OnProposalStep("n1"), OnProposalStep("n2"), OnProposalStep("n3"), OnProposalStep("n4"), OnProposalStep("n5"), ] ).* from "../guided_replica" -} \ No newline at end of file +} diff --git a/spec/protocol-spec/experiments/n6f1b1_guided_two_blocks.qnt b/spec/protocol-spec/experiments/n6f1b1_guided_two_blocks.qnt index 8288ec21..a9363770 100644 --- a/spec/protocol-spec/experiments/n6f1b1_guided_two_blocks.qnt +++ b/spec/protocol-spec/experiments/n6f1b1_guided_two_blocks.qnt @@ -1,3 +1,5 @@ +// -*- mode: Bluespec; -*- +// // A specification instance for n=6, f=1, and 1 Byzantine fault // // Due to import/export limitations of Quint, use the definitions starting with g_: @@ -29,4 +31,4 @@ module n6f1b1_two_blocks { OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), ] ).* from "../guided_replica" -} \ No newline at end of file +} diff --git a/spec/protocol-spec/experiments/n6f1b2.qnt b/spec/protocol-spec/experiments/n6f1b2.qnt index 0eee87c9..c30ebf8f 100644 --- a/spec/protocol-spec/experiments/n6f1b2.qnt +++ b/spec/protocol-spec/experiments/n6f1b2.qnt @@ -1,3 +1,5 @@ +// -*- mode: Bluespec; -*- +// // A specification instance for n=6, f=1, and 2 Byzantine faults module n6f1b2 { import replica( @@ -11,4 +13,4 @@ module n6f1b2 { VALID_BLOCKS = Set("val_b0", "val_b1"), INVALID_BLOCKS = Set("inv_b3") ).* from "../replica" -} \ No newline at end of file +} diff --git a/spec/protocol-spec/experiments/n6f1b2_boxed.qnt b/spec/protocol-spec/experiments/n6f1b2_boxed.qnt index 600b63ff..2426e0e0 100644 --- a/spec/protocol-spec/experiments/n6f1b2_boxed.qnt +++ b/spec/protocol-spec/experiments/n6f1b2_boxed.qnt @@ -1,3 +1,5 @@ +// -*- mode: Bluespec; -*- +// // A specification instance for n=6, f=1, and 2 Byzantine faults. // We box the number of different steps. module n6f1b2_boxed { @@ -137,4 +139,4 @@ module n6f1b2_boxed { } } } -} \ No newline at end of file +} diff --git a/spec/protocol-spec/experiments/n6f1b2_guided_agreement.qnt b/spec/protocol-spec/experiments/n6f1b2_guided_agreement.qnt index a3d5b798..cf173538 100644 --- a/spec/protocol-spec/experiments/n6f1b2_guided_agreement.qnt +++ b/spec/protocol-spec/experiments/n6f1b2_guided_agreement.qnt @@ -1,3 +1,5 @@ +// -*- mode: Bluespec; -*- +// // A specification instance for n=6, f=1, and 2 Byzantine faults // // Due to import/export limitations of Quint, use the definitions starting with g_: @@ -32,4 +34,4 @@ module n6f1b2_agreement { OnCommitStep("n3"), OnCommitStep("n3"), OnCommitStep("n3"), OnCommitStep("n3"), OnCommitStep("n3"), ] ).* from "../guided_replica" -} \ No newline at end of file +} diff --git a/spec/protocol-spec/experiments/n6f1b3.qnt b/spec/protocol-spec/experiments/n6f1b3.qnt index 683974bc..44cf5d9b 100644 --- a/spec/protocol-spec/experiments/n6f1b3.qnt +++ b/spec/protocol-spec/experiments/n6f1b3.qnt @@ -1,3 +1,5 @@ +// -*- mode: Bluespec; -*- +// // A specification instance for n=6, f=1, and 3 Byzantine faults module n6f1b0 { import replica( @@ -11,4 +13,4 @@ module n6f1b0 { VALID_BLOCKS = Set("val_b0", "val_b1"), INVALID_BLOCKS = Set("inv_b3") ).* from "../replica" -} \ No newline at end of file +} diff --git a/spec/protocol-spec/experiments/n7f1b0.qnt b/spec/protocol-spec/experiments/n7f1b0.qnt index b1beb6d7..292e38df 100644 --- a/spec/protocol-spec/experiments/n7f1b0.qnt +++ b/spec/protocol-spec/experiments/n7f1b0.qnt @@ -1,7 +1,9 @@ +// -*- mode: Bluespec; -*- +// // A specification instance for n=6, f=1, and no Byzantine faults module n7f1b0 { import replica( - CORRECT = Set("n0", "n1", "n2", "n3", "n4", "n5", "n5"), + CORRECT = Set("n0", "n1", "n2", "n3", "n4", "n5", "n6"), FAULTY = Set(), WEIGHTS = Map("n0"->1, "n1"->1, "n2"->1, "n3"->1, "n4"->1, "n5"->1, "n6"->1), REPLICA_KEYS = Map("n0"->"n0", "n1"->"n1", "n2"->"n2", "n3"->"n3", "n4"->"n4", "n5"->"n5", "n6"->"n6"), @@ -11,4 +13,4 @@ module n7f1b0 { VALID_BLOCKS = Set("val_b0", "val_b1"), INVALID_BLOCKS = Set("inv_b3") ).* from "../replica" -} \ No newline at end of file +} diff --git a/spec/protocol-spec/experiments/n7f1b0_quided_three_blocks.qnt b/spec/protocol-spec/experiments/n7f1b0_quided_three_blocks.qnt index b0ae55e6..0a246b84 100644 --- a/spec/protocol-spec/experiments/n7f1b0_quided_three_blocks.qnt +++ b/spec/protocol-spec/experiments/n7f1b0_quided_three_blocks.qnt @@ -1,3 +1,5 @@ +// -*- mode: Bluespec; -*- +// // A specification instance for n=7, f=1, and 0 byzantine nodes. // // Due to import/export limitations of Quint, use the definitions starting with g_: @@ -63,4 +65,4 @@ module n6f1b1_two_blocks { OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), ] ).* from "../guided_replica" -} \ No newline at end of file +} diff --git a/spec/protocol-spec/experiments/n7f1b1.qnt b/spec/protocol-spec/experiments/n7f1b1.qnt new file mode 100644 index 00000000..f2da73f7 --- /dev/null +++ b/spec/protocol-spec/experiments/n7f1b1.qnt @@ -0,0 +1,16 @@ +// -*- mode: Bluespec; -*- +// +// A specification instance for n=6, f=1, and no Byzantine faults +module n7f1b1 { + import replica( + CORRECT = Set("n0", "n1", "n2", "n3", "n4", "n5"), + FAULTY = Set("n6"), + WEIGHTS = Map("n0"->1, "n1"->1, "n2"->1, "n3"->1, "n4"->1, "n5"->1, "n6"->1), + REPLICA_KEYS = Map("n0"->"n0", "n1"->"n1", "n2"->"n2", "n3"->"n3", "n4"->"n4", "n5"->"n5", "n6"->"n6"), + N = 7, + F = 1, + VIEWS = 0.to(3), + VALID_BLOCKS = Set("val_b0", "val_b1"), + INVALID_BLOCKS = Set("inv_b3") + ).* from "../replica" +} diff --git a/spec/protocol-spec/guided_replica.qnt b/spec/protocol-spec/guided_replica.qnt index 0353e59c..d6558e64 100644 --- a/spec/protocol-spec/guided_replica.qnt +++ b/spec/protocol-spec/guided_replica.qnt @@ -1,3 +1,4 @@ +// -*- mode: Bluespec; -*- // A restriction of replica.qnt to guide the model checker's search module guided_replica { import types.* from "./types" @@ -139,4 +140,4 @@ module guided_replica { } } } -} \ No newline at end of file +} diff --git a/spec/protocol-spec/main.qnt b/spec/protocol-spec/main.qnt index e5f6cfa5..5eb2fad8 100644 --- a/spec/protocol-spec/main.qnt +++ b/spec/protocol-spec/main.qnt @@ -1,3 +1,4 @@ +// -*- mode: Bluespec; -*- /// A few handy small models that are good for debugging and inspection module main { // A specification instance for n=6, f=1, and 1 Byzantine fault @@ -12,4 +13,4 @@ module main { VALID_BLOCKS = Set("val_b0", "val_b1"), INVALID_BLOCKS = Set("inv_b3") ) .* from "./replica" -} \ No newline at end of file +} diff --git a/spec/protocol-spec/option.qnt b/spec/protocol-spec/option.qnt index 3e061ca4..fcb918e2 100644 --- a/spec/protocol-spec/option.qnt +++ b/spec/protocol-spec/option.qnt @@ -28,10 +28,11 @@ module option { } } - // if is Some(e), test whether `pred(e)` holds true + // If is Some(e), test whether `pred(e)` holds true. + // If None, return false. def option_has(opt: Option[a], pred: a => bool): bool = { match (opt) { - | None => true + | None => false | Some(e) => pred(e) } } diff --git a/spec/protocol-spec/replica.qnt b/spec/protocol-spec/replica.qnt index c7bf1002..f89ac1fd 100644 --- a/spec/protocol-spec/replica.qnt +++ b/spec/protocol-spec/replica.qnt @@ -106,9 +106,10 @@ module replica { }), replica_view' = CORRECT.mapBy(id => 0), proposer_view' = CORRECT.mapBy(id => 0), - // all correct replicas send TimeoutVote as their first step + // all correct replicas send SignedTimeoutVote as their first step msgs_signed_timeout' = CORRECT.map(id => { - vote: { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc: HIGH_COMMIT_QC_NONE }, + vote: { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc_view: None }, + high_commit_qc: HIGH_COMMIT_QC_NONE, sig: sig_of_id(id) }), msgs_signed_commit' = Set(), @@ -131,14 +132,16 @@ module replica { votes: REPLICAS.map(id => sig_of_id(id)).mapBy(_ => { view: 0, high_vote: COMMIT_VOTE_NONE, - high_commit_qc: HIGH_COMMIT_QC_NONE + high_commit_qc_view: VIEW_NUMBER_NONE }), agg_sig: REPLICAS.map(id => sig_of_id(id)), + high_commit_qc: HIGH_COMMIT_QC_NONE, ghost_view: 0, } pure val timeout_votes0 = REPLICAS.map(id => sig_of_id(id)).map(sig => { sig: sig, - vote: { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc: HIGH_COMMIT_QC_NONE}, + vote: { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc_view: VIEW_NUMBER_NONE }, + high_commit_qc: HIGH_COMMIT_QC_NONE, }) all { replica_state' = CORRECT.mapBy(id => { @@ -277,12 +280,15 @@ module replica { } nondet has_high_vote = oneOf(Bool) nondet has_commit_qc = oneOf(Bool) + nondet high_commit_qc_view = oneOf(VIEWS) + nondet has_high_commit_qc_view = oneOf(Bool) val signed_timeout_vote = { vote: { view: msg_view, high_vote: if (has_high_vote) Some(commit_vote.vote) else COMMIT_VOTE_NONE, - high_commit_qc: if (has_commit_qc) Some(commit_qc) else HIGH_COMMIT_QC_NONE, + high_commit_qc_view: if (has_high_commit_qc_view) Some(high_commit_qc_view) else VIEW_NUMBER_NONE, }, + high_commit_qc: if (has_commit_qc) Some(commit_qc) else HIGH_COMMIT_QC_NONE, sig: sig, } all { @@ -294,7 +300,6 @@ module replica { // add the message by a faulty replica msgs_signed_timeout' = msgs_signed_timeout.union(Set(signed_timeout_vote)), } - }, all { nondet msg_view = VIEWS.oneOf() @@ -306,21 +311,27 @@ module replica { nondet commit_qc_block_hash = oneOf(ALL_BLOCKS) nondet commit_qc_agg_sig = REPLICAS.powerset().oneOf() val commit_qc_vote: CommitVote = { - view: commit_qc_view, block_number: commit_qc_block_number, + view: commit_qc_view, + block_number: commit_qc_block_number, block_hash: commit_qc_block_hash } val commit_qc = { vote: commit_qc_vote, agg_sig: commit_qc_agg_sig, } - // introduce a timeout qc + // Introduce a timeout qc. + // We recycle commit_qc when constructing timeout_qc, as commit_qc and timeout_qc + // are not used at the same time, see justification_case. nondet timeout_qc_view = VIEWS.oneOf() nondet timeout_qc_voters = REPLICAS.powerset().oneOf() nondet timeout_qc_agg_sig = timeout_qc_voters.powerset().oneOf() nondet timeout_qc_votes = timeout_qc_voters.setOfMaps(msgs_signed_timeout.map(sv => sv.vote)).oneOf() + nondet has_high_commit_qc_view = oneOf(Bool) val timeout_qc: TimeoutQC = { votes: timeout_qc_votes, agg_sig: timeout_qc_agg_sig, + high_commit_qc: + if (has_high_commit_qc_view) Some(commit_qc) else HIGH_COMMIT_QC_NONE, ghost_view: timeout_qc_view, } // make new view @@ -339,7 +350,7 @@ module replica { FAULTY.contains(id), msgs_signed_commit.exists(sv => sv.sig == id and sv.vote == commit_qc_vote), }), - timeout_qc_agg_sig.forall(id => or { + justification_case != "commit" implies timeout_qc_agg_sig.forall(id => or { FAULTY.contains(id), msgs_signed_timeout.exists(sv => sv.sig == id and sv.vote == timeout_qc_votes.get(id)), }), @@ -363,15 +374,19 @@ module replica { val commit_qc = { vote: commit_qc_vote, agg_sig: commit_qc_agg_sig, } - // introduce a timeout qc + // Introduce a timeout qc. + // We recycle commit_qc when constructing timeout_qc, as commit_qc and timeout_qc + // are not used at the same time, see justification_case. nondet timeout_qc_view = VIEWS.oneOf() nondet timeout_qc_voters = REPLICAS.powerset().oneOf() nondet timeout_qc_agg_sig = timeout_qc_voters.powerset().oneOf() nondet timeout_qc_votes = timeout_qc_voters.setOfMaps(msgs_signed_timeout.map(sv => sv.vote)).oneOf() + nondet has_high_commit_qc_view = oneOf(Bool) val timeout_qc: TimeoutQC = { votes: timeout_qc_votes, agg_sig: timeout_qc_agg_sig, + high_commit_qc: if (has_high_commit_qc_view) Some(commit_qc) else HIGH_COMMIT_QC_NONE, ghost_view: timeout_qc_view, } // non-deterministically select a block @@ -396,7 +411,7 @@ module replica { FAULTY.contains(id), msgs_signed_commit.exists(sv => sv.sig == id and sv.vote == commit_qc_vote), }), - timeout_qc_agg_sig.forall(id => or { + justification_case != "commit" implies timeout_qc_agg_sig.forall(id => or { FAULTY.contains(id), msgs_signed_timeout.exists(sv => sv.sig == id and sv.vote == timeout_qc_votes.get(id)), }), @@ -488,20 +503,20 @@ module replica { // See validation below. hash } - + | None => { // See state verification below. unwrap_or(proposal.block, "").hash() } } - + // the replica vote to send val vote: CommitVote = { view: proposal_view, block_number: block_number, block_hash: block_hash, } - + all { // Vote only if you have collected all committed blocks so far (see a check in all {...}). block_number == length(self.committed_blocks), @@ -539,7 +554,7 @@ module replica { match (proposal.justification) { | Commit(qc) => self1.process_commit_qc(Some(qc)) | Timeout(qc) => { - ...self1.process_commit_qc(qc.high_qc()), + ...self1.process_commit_qc(qc.high_commit_qc), high_timeout_qc: max_timeout_qc(Some(qc), self1.high_timeout_qc) } } @@ -612,9 +627,14 @@ module replica { vote: { view: self.view, high_vote: self.high_vote, - high_commit_qc: self.high_commit_qc, + high_commit_qc_view: + match (self.high_commit_qc) { + | None => VIEW_NUMBER_NONE + | Some(qc) => Some(qc.vote.view) + } }, sig: sig_of_id(id), + high_commit_qc: self.high_commit_qc, } all { // If we have already timed out, we don't need to send another timeout vote. @@ -655,7 +675,7 @@ module replica { | Some(qc) => all { val self1 = { - ...self.process_commit_qc(qc.high_qc()), + ...self.process_commit_qc(qc.high_commit_qc), high_timeout_qc: max_timeout_qc(qc_opt, self.high_timeout_qc) } start_new_view(id, self1, signed_vote.vote.view + 1, Timeout(qc)), @@ -685,11 +705,11 @@ module replica { | Commit(qc) => self.process_commit_qc(Some(qc)) | Timeout(qc) => { - ...self.process_commit_qc(qc.high_qc()), + ...self.process_commit_qc(qc.high_commit_qc), high_timeout_qc: max_timeout_qc(Some(qc), self.high_timeout_qc) } } - + if (new_view_view > self.view) { start_new_view(id, self1, new_view_view, new_view.justification) } else { @@ -956,6 +976,8 @@ module replica { if (view_signed_votes.size() < QUORUM_WEIGHT) { None } else { + val high_commit_qc: Option[CommitQC] = view_signed_votes.fold(HIGH_COMMIT_QC_NONE, + (prev_max_qc, sv) => max_commit_qc(prev_max_qc, sv.high_commit_qc)) // Importantly, view_signed_votes does not have two votes with the same signature. // We check that in store_signed_timeout_all_inv. val qc_votes: ReplicaKey -> TimeoutVote = @@ -963,7 +985,8 @@ module replica { Some({ votes: qc_votes, agg_sig: view_signed_votes.map(v => v.sig), - ghost_view: view + high_commit_qc: high_commit_qc, + ghost_view: view, }) } } @@ -997,7 +1020,7 @@ module replica { match (justification) { | Timeout(qc) => qc.timeout_qc_verify() - + | Commit(qc) => qc.commit_qc_verify() } @@ -1030,7 +1053,14 @@ module replica { pure def signed_timeout_vote_verify(signed_vote: SignedTimeoutVote): bool = all { signed_vote.vote.view >= 0, - signed_vote.vote.high_commit_qc.option_has(qc => commit_qc_verify(qc)), + match (signed_vote.high_commit_qc) { + | None => + signed_vote.vote.high_commit_qc_view.is_none() + | Some(qc) => and { + Some(qc.vote.view) == signed_vote.vote.high_commit_qc_view, + commit_qc_verify(qc), + } + }, timeout_vote_verify(signed_vote.vote) } @@ -1047,18 +1077,17 @@ module replica { } // Timeout vote verification that a replica can do locally - // There are two invariants that are easy to check: - // self.view() >= self.high_vote.view() && self.high_vote.view() >= self.high_commit_qc.view() pure def timeout_vote_verify(vote: TimeoutVote): bool = all { vote.view >= 0, match vote.high_vote { | None => true | Some(high_vote) => and { commit_vote_verify(high_vote), + // There are two invariants that are easy to check but aren't required for correctness: vote.view >= high_vote.view, - match vote.high_commit_qc { + match vote.high_commit_qc_view { | None => true - | Some(high_commit_qc) => high_vote.view >= high_commit_qc.vote.view + | Some(v) => high_vote.view >= v } } } @@ -1086,13 +1115,30 @@ module replica { qc.agg_sig.aggregate_verify(), // It is essential that no vote is missing qc.votes.keys() == qc.agg_sig, + // Check that all votes have the same view and get the highest commit QC view of the timeout QC. + val high_qc_view: Option[ViewNumber] = + votes.fold(VIEW_NUMBER_NONE, (prev_max_opt, v) => match (prev_max_opt) { + | None => + v.high_commit_qc_view + | Some(prev_max) => + if (v.high_commit_qc_view.option_has(qcv => qcv > prev_max)) { + v.high_commit_qc_view + } else { + prev_max_opt + } + }) // Get the high commit QC of the timeout QC. We compare the high QC field of all // timeout votes in the QC, and get the highest one, if it exists. // We then need to verify that it is valid. We don't need to verify the commit QCs // of the other timeout votes, since they don't have any influence in the result. - match (qc.high_qc()) { - | None => true - | Some (high_qc) => high_qc.commit_qc_verify() + match (qc.high_commit_qc) { + | None => + high_qc_view.is_none() + + | Some (high_qc) => and { + high_qc_view == Some(high_qc.vote.view), + commit_qc_verify(high_qc), + } } } } @@ -1133,7 +1179,7 @@ module replica { // all timeout votes in the QC, and get the highest one, if it exists. match (qc_high_vote) { | Some(hv) => - match (high_qc(qc)) { + match (qc.high_commit_qc) { | Some(hqc) => if (hv.block_number > hqc.vote.block_number) { // There was some proposal last view that might have been finalized. @@ -1156,7 +1202,7 @@ module replica { // Either the previous proposal was finalized or we know for certain // that it couldn't have been finalized. Either way, we can propose // a new block. - match (high_qc(qc)) { + match (qc.high_commit_qc) { | Some(hqc) => (hqc.vote.block_number + 1, None) | None => (0, None) } @@ -1193,25 +1239,6 @@ module replica { } } - /// Get the high QC of the timeout QC. We compare the high QC field of all 4f+1 - /// timeout votes in the QC, and get the highest one. - pure def high_qc(qc: TimeoutQC): Option[CommitQC] = { - // Assumption: qc.votes does not have two different QCs for the same view. - qc.votes.keys().map(pk => qc.votes.get(pk)).fold(None, (max_qc_opt, v) => { - match (v.high_commit_qc) { - | None => max_qc_opt - | Some(hc_qc) => - // if max_qc is None, choose hc_qc, otherwise compare the views - match (max_qc_opt) { - | None => - Some(hc_qc) - | Some(max_qc) => - if (hc_qc.vote.view > max_qc.vote.view) Some(hc_qc) else max_qc_opt - } - } - }) - } - // ------------------------------------------------------------------------- // Invariants to check @@ -1236,7 +1263,12 @@ module replica { ghost_justifications.keys().exists(((id2, view)) => and { id2 == id, match (ghost_justifications.get((id2, view))) { - | Timeout(qc) => false + | Timeout(qc) => + qc.high_commit_qc.option_has(hqc => and { + hqc.vote.block_number == block_number, + hqc.vote.block_hash == block_hash, + view == hqc.vote.view or view == hqc.vote.view + 1, + }) | Commit(qc) => and { qc.vote.block_number == block_number, qc.vote.block_hash == block_hash, @@ -1266,7 +1298,11 @@ module replica { val no_timeout_equivocation_inv = tuples(msgs_signed_timeout, msgs_signed_timeout).forall(((m1, m2)) => or { not(m1.vote.view == m2.vote.view and m1.sig == m2.sig), FAULTY.exists(id => sig_of_id(id) == m1.sig), - m1.vote.high_vote == m2.vote.high_vote and m1.vote.high_commit_qc == m2.vote.high_commit_qc, + and { + m1.vote.high_vote == m2.vote.high_vote, + m1.high_commit_qc == m2.high_commit_qc, + m1.vote.high_commit_qc_view == m2.vote.high_commit_qc_view, + } }) // a correct proposer should not send two new views in the same view @@ -1305,10 +1341,10 @@ module replica { // no duplicates (v1.sig == v2.sig and v1.vote.view == v2.vote.view) implies (v1.vote == v2.vote), // the quorums have an intersection - match (v1.vote.high_commit_qc) { + match (v1.high_commit_qc) { | None => true | Some(qc1) => - match (v2.vote.high_commit_qc) { + match (v2.high_commit_qc) { | None => true | Some(qc2) => or { qc1.vote.view != qc2.vote.view, @@ -1337,6 +1373,7 @@ module replica { // have justifications for the views below. val view_justification_continuous_inv = { VIEWS.forall(v => or { + v == 0, CORRECT.forall(id => replica_state.get(id).view < v), ghost_justifications.keys().exists(((id, other_view)) => other_view == v) }) @@ -1386,8 +1423,10 @@ module replica { }) } - replica_state.keys() - .forall(id => replica_state.get(id).high_timeout_qc.option_has(one_high_vote)) + replica_state.keys().forall(id => { + val timeout_qc = replica_state.get(id).high_timeout_qc + timeout_qc.is_none() or timeout_qc.option_has(one_high_vote) + }) } // There are no two quorums for different block hashes in one view. @@ -1442,34 +1481,26 @@ module replica { match (qc_opt) { | None => true | Some(qc) => - val signed_votes = qc.votes.keys().map(pk => {vote: qc.votes.get(pk), sig: pk }) - val votes = signed_votes.map(v => v.vote) + val votes = qc.votes.keys().map(pk => qc.votes.get(pk)) val public_keys = qc.votes.keys() and { qc.ghost_view >= 0, qc.agg_sig.aggregate_verify(), - signed_votes.size() == qc.agg_sig.size(), public_keys == qc.agg_sig, - signed_votes.forall(v => v.signed_timeout_vote_verify()), + votes.forall(v => v.timeout_vote_verify()), // make sure that all votes are cast for the same view votes.forall(v => qc.ghost_view == v.view), - // even though quorums in the votes may slightly differ, - // they must have enough votes in the intersection - signed_votes.forall(v1 => signed_votes.forall(v2 => { - match (v1.vote.high_commit_qc) { - | None => true - | Some(qc1) => - match (v2.vote.high_commit_qc) { - | None => true - | Some(qc2) => or { - qc1.vote.view != qc2.vote.view, - FAULTY.exists(id => sig_of_id(id) == v1.sig or sig_of_id(id) == v2.sig), - // TODO: use QUORUM_WEIGHT - F? - qc1.agg_sig.intersect(qc2.agg_sig).size() >= SUBQUORUM_WEIGHT, - } - } + // The commit quorum certificate with the highest view that all replicas in this + // QC have observed, if any. It MUST match the highest `high_commit_qc_view` in `votes`. + match (qc.high_commit_qc) { + | None => + votes.forall(v => v.high_commit_qc_view.is_none()) + + | Some(commit_qc) => and { + votes.forall(v => v.view <= commit_qc.vote.view), + votes.exists(v => v.view == commit_qc.vote.view) } - })) + } } } } @@ -1527,7 +1558,7 @@ module replica { } }) } - + // a high vote is the highest among the votes sent by a replica val timeout_high_vote_is_highest_inv: bool = { msgs_signed_timeout.forall(tv => or { @@ -1598,7 +1629,7 @@ module replica { // ------------------------------------------------------------------------- // Falsy invariants to check reachability of certain states - + // check this invariant to see an example of reaching PhaseCommit val phase_commit_example = CORRECT.forall(id => replica_state.get(id).phase != PhaseCommit) diff --git a/spec/protocol-spec/state_monitor.qnt b/spec/protocol-spec/state_monitor.qnt index 08f3f153..1efdd986 100644 --- a/spec/protocol-spec/state_monitor.qnt +++ b/spec/protocol-spec/state_monitor.qnt @@ -1,3 +1,4 @@ +// -*- mode: Bluespec; -*- // A state monitor that allows us to compare new state against the old states. // For example, we compare phase transitions. // To do so, we save the old replica states in old_replica_state. @@ -16,7 +17,7 @@ module state_monitor { INVALID_BLOCKS = Set("inv_b3") ) as i from "./replica" - var old_replica_state: Option[ReplicaPubKey -> ReplicaState] + var old_replica_state: Option[ReplicaId -> ReplicaState] action init = all { i::init, @@ -33,7 +34,7 @@ module state_monitor { // Within the same view, a replica’s phase can only change through two paths. // 1) Prepare→Commit→Timeout or 2) Prepare→Timeout. val phase_inv = { - def for_replica(id: ReplicaPubKey): bool = { + def for_replica(id: ReplicaId): bool = { match (old_replica_state) { | None => true @@ -55,4 +56,4 @@ module state_monitor { i::CORRECT.forall(id => for_replica(id)) } -} \ No newline at end of file +} diff --git a/spec/protocol-spec/tests/tests_n6f1b0.qnt b/spec/protocol-spec/tests/tests_n6f1b0.qnt index ee9edd9e..b3212221 100644 --- a/spec/protocol-spec/tests/tests_n6f1b0.qnt +++ b/spec/protocol-spec/tests/tests_n6f1b0.qnt @@ -18,9 +18,10 @@ module tests_n6f1b0 { // an initial quorum certificate pure val init_timeout_qc: TimeoutQC = { - votes: CORRECT.mapBy(id => { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc: HIGH_COMMIT_QC_NONE}), + votes: CORRECT.mapBy(id => { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc_view: VIEW_NUMBER_NONE }), agg_sig: CORRECT, ghost_view: 0, + high_commit_qc: HIGH_COMMIT_QC_NONE, } def replica_committed(id: ReplicaId): List[Block] = { @@ -121,14 +122,15 @@ module tests_n6f1b0 { } val timeout_qc_v1: TimeoutQC = { votes: Map( - "n0" -> { view: 2, high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(commit_vote_v1_b0) }, - "n1" -> { view: 2, high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(commit_vote_v1_b0) }, - "n2" -> { view: 2, high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(commit_vote_v1_b0) }, - "n3" -> { view: 2, high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(commit_vote_v1_b0) }, - "n5" -> { view: 2, high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(commit_vote_v1_b0) } + "n0" -> { view: 2, high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(commit_vote_v1_b0) }, + "n1" -> { view: 2, high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(commit_vote_v1_b0) }, + "n2" -> { view: 2, high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(commit_vote_v1_b0) }, + "n3" -> { view: 2, high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(commit_vote_v1_b0) }, + "n5" -> { view: 2, high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(commit_vote_v1_b0) } ), agg_sig: Set("n0", "n1", "n2", "n3", "n5"), - ghost_view: 2 + ghost_view: 2, + high_commit_qc: HIGH_COMMIT_QC_NONE, } init_view_1_with_leader(Map(0 -> "n0", 1 -> "n5", 2 -> "n1", 3 -> "n2", 4 -> "n3", 5 -> "n4")) // the leader proposes, all replicas in view=1 @@ -250,15 +252,15 @@ module tests_n6f1b0 { replica_state.get("n1").high_commit_qc==Some({ vote: commit_vote_v1_b0, agg_sig: Set("n0", "n1", "n2", "n3", "n5")}), unchanged_all }) .expect(all_invariants) - .then(replica_receives_all_timeout_votes("n0", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1)) + .then(replica_receives_all_timeout_votes("n0", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1)) .expect(all_invariants) - .then(replica_receives_all_timeout_votes("n2", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1)) + .then(replica_receives_all_timeout_votes("n2", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1)) .expect(all_invariants) - .then(replica_receives_all_timeout_votes("n3", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1)) + .then(replica_receives_all_timeout_votes("n3", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1)) .expect(all_invariants) - .then(replica_receives_all_timeout_votes("n4", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1)) + .then(replica_receives_all_timeout_votes("n4", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1)) .expect(all_invariants) - .then(replica_receives_all_timeout_votes("n5", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1)) + .then(replica_receives_all_timeout_votes("n5", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1)) .expect(all_invariants) .then(all { proposer_step("n1", "val_b1"), @@ -295,26 +297,30 @@ module tests_n6f1b0 { }) } - action replica_receives_all_timeout_votes(id: ReplicaId, high_vote: Option[CommitVote], high_commit_qc: Option[CommitQC], view: ViewNumber):bool = all { - on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n0"} ), - unchanged_leader_replica, + action replica_receives_all_timeout_votes(id: ReplicaId, high_vote: Option[CommitVote], + high_commit_qc_view: Option[ViewNumber], high_commit_qc: Option[CommitQC], view: ViewNumber): bool = { + val timeout_vote: TimeoutVote = { view: view, high_commit_qc_view: high_commit_qc_view, high_vote: high_vote } + all { + on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n0" }), + unchanged_leader_replica, + } + .then(all { + on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n1" }), + unchanged_leader_replica, + }) + .then(all { + on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n2" }), + unchanged_leader_replica, + }) + .then(all { + on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n3" }), + unchanged_leader_replica, + }) + .then(all { + on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n4" }), + unchanged_leader_replica, + }) } - .then(all { - on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n1"} ), - unchanged_leader_replica, - }) - .then(all { - on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n2"} ), - unchanged_leader_replica, - }) - .then(all { - on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n3"} ), - unchanged_leader_replica, - }) - .then(all { - on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n4"} ), - unchanged_leader_replica, - }) action five_replicas_get_propose(block: Block, block_number: BlockNumber, leader: ReplicaId, justification: Justification): bool = { diff --git a/spec/protocol-spec/tests/tests_n6f1b1.qnt b/spec/protocol-spec/tests/tests_n6f1b1.qnt index 49bcea9e..e6649aeb 100644 --- a/spec/protocol-spec/tests/tests_n6f1b1.qnt +++ b/spec/protocol-spec/tests/tests_n6f1b1.qnt @@ -16,17 +16,19 @@ module tests { ).* from "../replica" // an initial quorum certificate from all replicas - val init_timeout_qc: TimeoutQC = { - votes: REPLICAS.mapBy(id => { view: 0, high_vote: None, high_commit_qc: None}), - agg_sig: REPLICAS, + pure val init_timeout_qc: TimeoutQC = { + votes: CORRECT.mapBy(id => { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc_view: VIEW_NUMBER_NONE }), + agg_sig: CORRECT, ghost_view: 0, + high_commit_qc: HIGH_COMMIT_QC_NONE, } // an initial quorum certificate from the correct replicas val init_timeout_corr_qc: TimeoutQC = { - votes: CORRECT.mapBy(id => { view: 0, high_vote: None, high_commit_qc: None}), + votes: CORRECT.mapBy(id => { view: 0, high_vote: None, high_commit_qc_view: VIEW_NUMBER_NONE }), agg_sig: CORRECT, ghost_view: 0, + high_commit_qc: HIGH_COMMIT_QC_NONE, } def replica_committed(id: ReplicaId): List[Block] = { @@ -36,10 +38,11 @@ module tests { run replicas_bootstrap_in_view0_Test = { pure val timeout_votes0 = CORRECT.map(id => { sig: sig_of_id(id), - vote: { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc: HIGH_COMMIT_QC_NONE}, + vote: { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc_view: VIEW_NUMBER_NONE }, + high_commit_qc: HIGH_COMMIT_QC_NONE, }) init_view_0_with_leader(Map(0 -> "n0", 1 -> "n0", 2 -> "n1", 3 -> "n2", 4 -> "n3")) - .then(replica_receives_all_timeout_votes("n0", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 0)) + .then(replica_receives_all_timeout_votes("n0", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 0)) .expect(all_invariants) .then(replica_receives_new_view("n1", Timeout(init_timeout_corr_qc))) .expect(all_invariants) @@ -238,15 +241,15 @@ module tests { }) .expect(all_invariants) // all replicas send TimeoutVote to each other, each replica gets all messages from all other replicas including itself - .then(replica_receives_all_timeout_votes("n0", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1)) + .then(replica_receives_all_timeout_votes("n0", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1)) .expect(all_invariants) - .then(replica_receives_all_timeout_votes("n1", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1)) + .then(replica_receives_all_timeout_votes("n1", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1)) .expect(all_invariants) - .then(replica_receives_all_timeout_votes("n2", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1)) + .then(replica_receives_all_timeout_votes("n2", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1)) .expect(all_invariants) - .then(replica_receives_all_timeout_votes("n3", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1)) + .then(replica_receives_all_timeout_votes("n3", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1)) .expect(all_invariants) - .then(replica_receives_all_timeout_votes("n4", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1)) + .then(replica_receives_all_timeout_votes("n4", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1)) .expect(all_invariants) .then(all { proposer_step("n1", "val_b1"), @@ -299,27 +302,30 @@ module tests { }) } - action replica_receives_all_timeout_votes(id: ReplicaId, high_vote: Option[CommitVote], high_commit_qc: Option[CommitQC], view: ViewNumber):bool = all { - on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n0"} ), - unchanged_leader_replica, + action replica_receives_all_timeout_votes(id: ReplicaId, high_vote: Option[CommitVote], + high_commit_qc_view: Option[ViewNumber], high_commit_qc: Option[CommitQC], view: ViewNumber): bool = { + val timeout_vote: TimeoutVote = { view: view, high_commit_qc_view: high_commit_qc_view, high_vote: high_vote } + all { + on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n0" }), + unchanged_leader_replica, + } + .then(all { + on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n1" }), + unchanged_leader_replica, + }) + .then(all { + on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n2" }), + unchanged_leader_replica, + }) + .then(all { + on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n3" }), + unchanged_leader_replica, + }) + .then(all { + on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n4" }), + unchanged_leader_replica, + }) } - .then(all { - on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n1"} ), - unchanged_leader_replica, - }) - .then(all { - on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n2"} ), - unchanged_leader_replica, - }) - .then(all { - on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n3"} ), - unchanged_leader_replica, - }) - .then(all { - on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n4"} ), - unchanged_leader_replica, - }) - action replica_commits(id: ReplicaId, block_hash: BlockHash, block_number: BlockNumber, view: ViewNumber):bool = all { on_commit(id, { vote: {block_hash: block_hash, block_number: block_number, view: view }, sig:"n0"}), diff --git a/spec/protocol-spec/tests/tests_n6f1b2.qnt b/spec/protocol-spec/tests/tests_n6f1b2.qnt index b80cfd38..7f4a14d9 100644 --- a/spec/protocol-spec/tests/tests_n6f1b2.qnt +++ b/spec/protocol-spec/tests/tests_n6f1b2.qnt @@ -18,9 +18,10 @@ module tests_n6f1b2 { // an initial quorum certificate pure val init_timeout_qc: TimeoutQC = { - votes: REPLICAS.mapBy(id => { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc: HIGH_COMMIT_QC_NONE}), + votes: REPLICAS.mapBy(id => { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc_view: VIEW_NUMBER_NONE }), agg_sig: REPLICAS, ghost_view: 0, + high_commit_qc: HIGH_COMMIT_QC_NONE, } def replica_committed(id: ReplicaId): List[Block] = { @@ -33,8 +34,8 @@ module tests_n6f1b2 { run disagreement_Test = { val high_vote_b0 = Some({ view: 1, block_number: 0, block_hash: "val_b0" }) val high_vote_b1 = Some({ view: 1, block_number: 0, block_hash: "val_b1" }) - val timeout_vote_b0: TimeoutVote = { view: 1, high_commit_qc: None, high_vote: high_vote_b0 } - val timeout_vote_b1: TimeoutVote = { view: 1, high_commit_qc: None, high_vote: high_vote_b1 } + val timeout_vote_b0: TimeoutVote = { view: 1, high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: high_vote_b0 } + val timeout_vote_b1: TimeoutVote = { view: 1, high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: high_vote_b1 } // n4 and n5 partition the correct replicas into n0, n1, n2 and n1, n2, n3 val timeout_qc: TimeoutQC = { ghost_view: 1, @@ -45,7 +46,8 @@ module tests_n6f1b2 { } else { timeout_vote_b1 } - }) + }), + high_commit_qc: HIGH_COMMIT_QC_NONE, } val new_view_timeout: NewView = { sig: "n4", @@ -123,10 +125,12 @@ module tests_n6f1b2 { val timeout_vote_n4: SignedTimeoutVote = { vote: timeout_vote_b1, sig: "n4", + high_commit_qc: HIGH_COMMIT_QC_NONE, } val timeout_vote_n5: SignedTimeoutVote = { vote: timeout_vote_b1, sig: "n5", + high_commit_qc: HIGH_COMMIT_QC_NONE, } all { msgs_signed_timeout' = msgs_signed_timeout.union(Set(timeout_vote_n4, timeout_vote_n5)), diff --git a/spec/protocol-spec/tests/unit_tests.qnt b/spec/protocol-spec/tests/unit_tests.qnt index d0a525f2..52b3dc25 100644 --- a/spec/protocol-spec/tests/unit_tests.qnt +++ b/spec/protocol-spec/tests/unit_tests.qnt @@ -33,7 +33,8 @@ module tests { pure val timeout: Justification = Timeout({ votes: Map(), agg_sig: Set(""), - ghost_view: 1 + ghost_view: 1, + high_commit_qc: HIGH_COMMIT_QC_NONE, }) all { @@ -80,13 +81,14 @@ module tests { ghost_view: 0, votes: Map( - "n0" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, - "n1" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, - "n2" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, - "n3" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, - "n4" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, - "n5" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 } - ) + "n0" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, + "n1" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, + "n2" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, + "n3" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, + "n4" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, + "n5" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 } + ), + high_commit_qc: HIGH_COMMIT_QC_NONE, } val timeout_qc_2: TimeoutQC = { @@ -94,13 +96,14 @@ module tests { ghost_view: 0, votes: Map( - "n0" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 0 }, - "n1" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, - "n2" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, - "n3" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, - "n4" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, - "n5" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 } - ) + "n0" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 0 }, + "n1" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, + "n2" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, + "n3" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, + "n4" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }, + "n5" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 } + ), + high_commit_qc: HIGH_COMMIT_QC_NONE, } val timeout_qc_3: TimeoutQC = { @@ -108,13 +111,14 @@ module tests { ghost_view: 2, votes: Map( - "n0" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 }, - "n1" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 }, - "n2" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 }, - "n3" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 }, - "n4" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 }, - "n5" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 } - ) + "n0" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 }, + "n1" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 }, + "n2" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 }, + "n3" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 }, + "n4" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 }, + "n5" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 } + ), + high_commit_qc: HIGH_COMMIT_QC_NONE, } val timeout_qc_4: TimeoutQC = { @@ -122,13 +126,14 @@ module tests { ghost_view: 2, votes: Map( - "n0" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 }, - "n1" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 }, - "n2" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 }, - "n3" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 }, - "n4" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote2), view: 2 }, - "n5" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote2), view: 2 } - ) + "n0" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 }, + "n1" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 }, + "n2" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 }, + "n3" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 }, + "n4" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote2), view: 2 }, + "n5" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote2), view: 2 } + ), + high_commit_qc: HIGH_COMMIT_QC_NONE, } val timeout_qc_5: TimeoutQC = { @@ -136,13 +141,14 @@ module tests { ghost_view: 2, votes: Map( - "n0" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 }, - "n1" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 }, - "n2" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote2), view: 2 }, - "n3" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote2), view: 2 }, - "n4" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote3), view: 2 }, - "n5" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote3), view: 2 } - ) + "n0" -> { high_commit_qc_view: Some(2), high_vote: Some(vote1), view: 2 }, + "n1" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 }, + "n2" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote2), view: 2 }, + "n3" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote2), view: 2 }, + "n4" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote3), view: 2 }, + "n5" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote3), view: 2 } + ), + high_commit_qc: Some(commit_qc_1), } val timeout_qc_6: TimeoutQC = { @@ -150,13 +156,14 @@ module tests { ghost_view: 2, votes: Map( - "n0" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 }, - "n1" -> { high_commit_qc: Some(commit_qc_2), high_vote: Some(vote1), view: 2 }, - "n2" -> { high_commit_qc: Some(commit_qc_3), high_vote: Some(vote2), view: 2 }, - "n3" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote2), view: 2 }, - "n4" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote3), view: 2 }, - "n5" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote3), view: 2 } - ) + "n0" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 }, + "n1" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 }, + "n2" -> { high_commit_qc_view: Some(2), high_vote: Some(vote2), view: 2 }, + "n3" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote2), view: 2 }, + "n4" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote3), view: 2 }, + "n5" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote3), view: 2 } + ), + high_commit_qc: Some(commit_qc_1), } val timeout_qc_7: TimeoutQC = { @@ -164,13 +171,14 @@ module tests { ghost_view: 2, votes: Map( - "n0" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 }, - "n1" -> { high_commit_qc: Some(commit_qc_2), high_vote: Some(vote1), view: 2 }, - "n2" -> { high_commit_qc: Some(commit_qc_3), high_vote: Some(vote1), view: 2 }, - "n3" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote2), view: 2 }, - "n4" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote2), view: 2 }, - "n5" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote2), view: 2 } - ) + "n0" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 }, + "n1" -> { high_commit_qc_view: Some(2), high_vote: Some(vote1), view: 2 }, + "n2" -> { high_commit_qc_view: Some(2), high_vote: Some(vote1), view: 2 }, + "n3" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote2), view: 2 }, + "n4" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote2), view: 2 }, + "n5" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote2), view: 2 } + ), + high_commit_qc: Some(commit_qc_1), } val timeout_qc_8: TimeoutQC = { @@ -178,13 +186,14 @@ module tests { ghost_view: 2, votes: Map( - "n0" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 }, - "n1" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 }, - "n2" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 }, - "n3" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 }, - "n4" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 }, - "n5" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 } - ) + "n0" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 }, + "n1" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 }, + "n2" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 }, + "n3" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 }, + "n4" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 }, + "n5" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 } + ), + high_commit_qc: Some(commit_qc_1), } run high_vote_Test = { @@ -201,15 +210,6 @@ module tests { } - run high_qc_Test = { - all { - assert(high_qc(timeout_qc_1) == HIGH_COMMIT_QC_NONE), - assert(high_qc(timeout_qc_5) == Some(commit_qc_1)), - assert(high_qc(timeout_qc_6) == Some(commit_qc_3)), - } - - } - run max_timeout_qc_Test = { all { max_timeout_qc(HIGH_TIMEOUT_QC_NONE, HIGH_TIMEOUT_QC_NONE) == HIGH_TIMEOUT_QC_NONE, @@ -235,9 +235,10 @@ module tests { vote: { view: 10, high_vote: COMMIT_VOTE_NONE, - high_commit_qc: HIGH_COMMIT_QC_NONE + high_commit_qc_view: VIEW_NUMBER_NONE, }, sig: "n1", + high_commit_qc: HIGH_COMMIT_QC_NONE, } ) val signed_timeout_votes_2 = Set( @@ -245,57 +246,62 @@ module tests { vote: { view: 10, high_vote: COMMIT_VOTE_NONE, - high_commit_qc: HIGH_COMMIT_QC_NONE + high_commit_qc_view: VIEW_NUMBER_NONE, }, sig: "n2", + high_commit_qc: HIGH_COMMIT_QC_NONE, }, { vote: { view: 10, high_vote: COMMIT_VOTE_NONE, - high_commit_qc: HIGH_COMMIT_QC_NONE + high_commit_qc_view: VIEW_NUMBER_NONE, }, sig: "n3", + high_commit_qc: HIGH_COMMIT_QC_NONE, }, { vote: { view: 10, high_vote: COMMIT_VOTE_NONE, - high_commit_qc: HIGH_COMMIT_QC_NONE + high_commit_qc_view: VIEW_NUMBER_NONE, }, sig: "n4", + high_commit_qc: HIGH_COMMIT_QC_NONE, }, { vote: { view: 10, high_vote: COMMIT_VOTE_NONE, - high_commit_qc: HIGH_COMMIT_QC_NONE + high_commit_qc_view: VIEW_NUMBER_NONE, }, sig: "n1", + high_commit_qc: HIGH_COMMIT_QC_NONE, }, { vote: { view: 10, high_vote: COMMIT_VOTE_NONE, - high_commit_qc: HIGH_COMMIT_QC_NONE + high_commit_qc_view: VIEW_NUMBER_NONE, }, sig: "n0", + high_commit_qc: HIGH_COMMIT_QC_NONE, } - ) run get_timeout_qc_Test = { - val qc = { + val qc: TimeoutQC = { ghost_view: 10, agg_sig: Set("n0", "n1", "n2", "n3", "n4"), votes: Map( - "n0" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 }, - "n1" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 }, - "n2" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 }, - "n3" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 }, - "n4" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 } - ) + "n0" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 }, + "n1" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 }, + "n2" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 }, + "n3" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 }, + "n4" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 } + ), + high_commit_qc: HIGH_COMMIT_QC_NONE, } all { get_timeout_qc(signed_timeout_votes_1, 10) == HIGH_TIMEOUT_QC_NONE, diff --git a/spec/protocol-spec/twins_n6f1b1.qnt b/spec/protocol-spec/twins_n6f1b1.qnt index 7346a948..30d3d504 100644 --- a/spec/protocol-spec/twins_n6f1b1.qnt +++ b/spec/protocol-spec/twins_n6f1b1.qnt @@ -1,3 +1,4 @@ +// -*- mode: Bluespec; -*- // This is an explorative module applying the Twins approach // to model byzantine behaviour with 1 faulty replicas and 5 correct replicas. module twins { @@ -31,4 +32,4 @@ module twins { action step = i::correct_step -} \ No newline at end of file +} diff --git a/spec/protocol-spec/twins_n6f1b2.qnt b/spec/protocol-spec/twins_n6f1b2.qnt index 46321eec..0596281a 100644 --- a/spec/protocol-spec/twins_n6f1b2.qnt +++ b/spec/protocol-spec/twins_n6f1b2.qnt @@ -1,3 +1,4 @@ +// -*- mode: Bluespec; -*- // This is an explorative module applying the Twins approach // to model byzantine behaviour with 2 faulty replicas and 4 correct replicas. module twins { @@ -31,4 +32,4 @@ module twins { action step = i::correct_step -} \ No newline at end of file +} diff --git a/spec/protocol-spec/types.qnt b/spec/protocol-spec/types.qnt index aaeb37fe..5187798e 100644 --- a/spec/protocol-spec/types.qnt +++ b/spec/protocol-spec/types.qnt @@ -9,7 +9,7 @@ module types { type Block = str // For specification purposes, we represent a hash of a string `s` as - // the string `s`. This representation is collision-free, + // the string `s`. This representation is collision-free, // and we interpret it as opaque. type BlockHash = str @@ -98,9 +98,9 @@ module types { // This proposal is being proposed after a view where we timed out. // A timeout QC is just a collection of timeout votes (with at least // QUORUM_WEIGHT) for the previous view. Unlike with the Commit QC, - // timeout votes don't need to be identical. + // timeout votes don't need to be identical. | Timeout(TimeoutQC) - + type CommitVote = { // The current view. @@ -138,16 +138,21 @@ module types { view: ViewNumber, // The commit vote with the highest view that this replica has signed. high_vote: Option[CommitVote], - // The commit quorum certificate with the highest view that this replica - // has observed. - high_commit_qc: Option[CommitQC], + // The view number of the highest commit quorum certificate that this replica + // has observed, if any. + high_commit_qc_view: Option[ViewNumber], } + pure val VIEW_NUMBER_NONE: Option[ViewNumber] = None + type SignedTimeoutVote = { // The timeout. vote: TimeoutVote, - // Signature of the sender. + // Signature of the sender. This signature is ONLY over the vote field. sig: Signature, + // The commit quorum certificate with the highest view that this replica + // has observed, if any. It MUST match `high_commit_qc_view` in `vote`. + high_commit_qc: Option[CommitQC], } // If we have timeout votes with at least QUORUM_WEIGHT for the same @@ -161,6 +166,9 @@ module types { // The aggregate signature of the replicas. We ignore the details here. // Can be something as simple as a vector of signatures. agg_sig: AggregateSignature, + // The commit quorum certificate with the highest view that all replicas in this + // QC have observed, if any. It MUST match the highest `high_commit_qc_view` in `votes`. + high_commit_qc: Option[CommitQC], // current view computed from the votes (not present in the original specification). ghost_view: ViewNumber,