Skip to content

Commit 14f4f93

Browse files
infrmtcsinfrmtcs
authored
refactor: Split Tendermint rules into separate files (#2735)
1 parent 1fc1c64 commit 14f4f93

12 files changed

+349
-338
lines changed

‎consensus/tendermint/precommit.go

-56
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,5 @@
11
package tendermint
22

3-
import (
4-
"maps"
5-
"slices"
6-
)
7-
83
func (t *Tendermint[V, H, A]) handlePrecommit(p Precommit[H, A]) {
94
if p.H < t.state.h {
105
return
@@ -34,54 +29,3 @@ func (t *Tendermint[V, H, A]) handlePrecommit(p Precommit[H, A]) {
3429

3530
t.line47(p, precommitsForHR)
3631
}
37-
38-
/*
39-
Check the upon condition on line 49:
40-
41-
49: upon {PROPOSAL, h_p, r, v, *} from proposer(h_p, r) AND 2f + 1 {PRECOMMIT, h_p, r, id(v)} while decision_p[h_p] = nil do
42-
50: if valid(v) then
43-
51: decisionp[hp] = v
44-
52: h_p ← h_p + 1
45-
53: reset lockedRound_p, lockedValue_p, validRound_p and validValue_p to initial values and empty message log
46-
54: StartRound(0)
47-
48-
Fetching the relevant proposal implies the sender of the proposal was the proposer for that
49-
height and round. Also, since only the proposals with valid value are added to the message set, the
50-
validity of the proposal can be skipped.
51-
52-
There is no need to check decision_p[h_p] = nil since it is implied that decision are made
53-
sequentially, i.e. x, x+1, x+2... .
54-
*/
55-
func (t *Tendermint[V, H, A]) line49WhenPrecommitIsReceived(p Precommit[H, A]) bool {
56-
if p.ID != nil {
57-
proposal := t.findMatchingProposal(p.R, *p.ID)
58-
59-
precommits, hasQuorum := t.checkForQuorumPrecommit(p.R, *p.ID)
60-
61-
if proposal != nil && hasQuorum {
62-
t.blockchain.Commit(t.state.h, *proposal.Value, precommits)
63-
64-
t.messages.deleteHeightMessages(t.state.h)
65-
t.state.h++
66-
t.startRound(0)
67-
68-
return true
69-
}
70-
}
71-
return false
72-
}
73-
74-
/*
75-
Check the upon condition on line 47:
76-
77-
47: upon 2f + 1 {PRECOMMIT, h_p, round_p, ∗} for the first time do
78-
48: schedule OnTimeoutPrecommit(h_p , round_p) to be executed after timeoutPrecommit(round_p)
79-
*/
80-
func (t *Tendermint[V, H, A]) line47(p Precommit[H, A], precommitsForHR map[A][]Precommit[H, A]) {
81-
vals := slices.Collect(maps.Keys(precommitsForHR))
82-
if p.R == t.state.r && !t.state.timeoutPrecommitScheduled &&
83-
t.validatorSetVotingPower(vals) >= q(t.validators.TotalVotingPower(p.H)) {
84-
t.scheduleTimeout(t.timeoutPrecommit(p.R), precommit, p.H, p.R)
85-
t.state.timeoutPrecommitScheduled = true
86-
}
87-
}

‎consensus/tendermint/prevote.go

-119
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,5 @@
11
package tendermint
22

3-
import (
4-
"maps"
5-
"slices"
6-
)
7-
83
func (t *Tendermint[V, H, A]) handlePrevote(p Prevote[H, A]) {
94
if p.H < t.state.h {
105
return
@@ -37,117 +32,3 @@ func (t *Tendermint[V, H, A]) handlePrevote(p Prevote[H, A]) {
3732
t.line36WhenPrevoteIsReceived(p)
3833
}
3934
}
40-
41-
/*
42-
Check the upon condition on line 28:
43-
44-
28: upon {PROPOSAL, h_p, round_p, v, vr} from proposer(h_p, round_p) AND 2f + 1 {PREVOTE,h_p, vr, id(v)} while
45-
step_p = propose ∧ (vr ≥ 0 ∧ vr < round_p) do
46-
29: if valid(v) ∧ (lockedRound_p ≤ vr ∨ lockedValue_p = v) then
47-
30: broadcast {PREVOTE, hp, round_p, id(v)}
48-
31: else
49-
32: broadcast {PREVOTE, hp, round_p, nil}
50-
33: step_p ← prevote
51-
52-
Fetching the relevant proposal implies the sender of the proposal was the proposer for that
53-
height and round. Also, since only the proposals with valid value are added to the message set, the
54-
validity of the proposal can be skipped.
55-
56-
Calculating quorum of prevotes is more resource intensive than checking other condition on line 28,
57-
therefore, it is checked in a subsequent if statement.
58-
*/
59-
func (t *Tendermint[V, H, A]) line28WhenPrevoteIsReceived(p Prevote[H, A]) {
60-
// vr >= 0 doesn't need to be checked since vr is a uint
61-
if vr := p.R; p.ID != nil && t.state.s == propose && vr < t.state.r {
62-
proposal := t.findMatchingProposal(t.state.r, *p.ID)
63-
hasQuorum := t.checkQuorumPrevotesGivenProposalVID(p.R, *p.ID)
64-
65-
if proposal != nil && hasQuorum {
66-
var votedID *H
67-
if t.state.lockedRound >= vr || (*t.state.lockedValue).Hash() == *p.ID {
68-
votedID = p.ID
69-
}
70-
t.sendPrevote(votedID)
71-
}
72-
}
73-
}
74-
75-
/*
76-
Check the upon condition on line 34:
77-
78-
34: upon 2f + 1 {PREVOTE, h_p, round_p, ∗} while step_p = prevote for the first time do
79-
35: schedule OnTimeoutPrevote(h_p, round_p) to be executed after timeoutPrevote(round_p)
80-
*/
81-
func (t *Tendermint[V, H, A]) line34(p Prevote[H, A], prevotesForHR map[A][]Prevote[H, A]) {
82-
vals := slices.Collect(maps.Keys(prevotesForHR))
83-
if !t.state.timeoutPrevoteScheduled && t.state.s == prevote &&
84-
t.validatorSetVotingPower(vals) >= q(t.validators.TotalVotingPower(p.H)) {
85-
t.scheduleTimeout(t.timeoutPrevote(p.R), prevote, p.H, p.R)
86-
t.state.timeoutPrevoteScheduled = true
87-
}
88-
}
89-
90-
/*
91-
Check the upon condition on line 44:
92-
93-
44: upon 2f + 1 {PREVOTE, h_p, round_p, nil} while step_p = prevote do
94-
45: broadcast {PRECOMMIT, hp, roundp, nil}
95-
46: step_p ← precommit
96-
97-
Line 36 and 44 for a round are mutually exclusive.
98-
*/
99-
func (t *Tendermint[V, H, A]) line44(p Prevote[H, A], prevotesForHR map[A][]Prevote[H, A]) {
100-
var vals []A
101-
for addr, valPrevotes := range prevotesForHR {
102-
for _, v := range valPrevotes {
103-
if v.ID == nil {
104-
vals = append(vals, addr)
105-
}
106-
}
107-
}
108-
109-
if t.state.s == prevote && t.validatorSetVotingPower(vals) >= q(t.validators.TotalVotingPower(p.H)) {
110-
t.sendPrecommit(nil)
111-
}
112-
}
113-
114-
/*
115-
Check upon condition on line 36:
116-
117-
36: upon {PROPOSAL, h_p, round_p, v, ∗} from proposer(h_p, round_p) AND 2f + 1 {PREVOTE, h_p, round_p, id(v)} while
118-
valid(v) ∧ step_p ≥ prevote for the first time do
119-
37: if step_p = prevote then
120-
38: lockedValue_p ← v
121-
39: lockedRound_p ← round_p
122-
40: broadcast {PRECOMMIT, h_p, round_p, id(v))}
123-
41: step_p ← precommit
124-
42: validValue_p ← v
125-
43: validRound_p ← round_p
126-
127-
Fetching the relevant proposal implies the sender of the proposal was the proposer for that
128-
height and round. Also, since only the proposals with valid value are added to the message set, the
129-
validity of the proposal can be skipped.
130-
131-
Calculating quorum of prevotes is more resource intensive than checking other condition on line 36,
132-
therefore, it is checked in a subsequent if statement.
133-
*/
134-
func (t *Tendermint[V, H, A]) line36WhenPrevoteIsReceived(p Prevote[H, A]) {
135-
if p.ID != nil && !t.state.lockedValueAndOrValidValueSet && t.state.s >= prevote {
136-
proposal := t.findMatchingProposal(t.state.r, *p.ID)
137-
hasQuorum := t.checkQuorumPrevotesGivenProposalVID(p.R, *p.ID)
138-
139-
if proposal != nil && hasQuorum {
140-
cr := t.state.r
141-
142-
if t.state.s == prevote {
143-
t.state.lockedValue = proposal.Value
144-
t.state.lockedRound = cr
145-
t.sendPrecommit(p.ID)
146-
}
147-
148-
t.state.validValue = proposal.Value
149-
t.state.validRound = cr
150-
t.state.lockedValueAndOrValidValueSet = true
151-
}
152-
}
153-
}

‎consensus/tendermint/propose.go

-130
Original file line numberDiff line numberDiff line change
@@ -48,133 +48,3 @@ func (t *Tendermint[V, H, A]) handleProposal(p Proposal[V, H, A]) {
4848
t.line28WhenProposalIsReceived(vr, proposalFromProposer, vID, validProposal)
4949
t.line36WhenProposalIsReceived(p, validProposal, proposalFromProposer, prevotesForHR, vID)
5050
}
51-
52-
/*
53-
Check the upon condition on line 49:
54-
55-
49: upon {PROPOSAL, h_p, r, v, *} from proposer(h_p, r) AND 2f + 1 {PRECOMMIT, h_p, r, id(v)} while decision_p[h_p] = nil do
56-
50: if valid(v) then
57-
51: decisionp[hp] = v
58-
52: h_p ← h_p + 1
59-
53: reset lockedRound_p, lockedValue_p, validRound_p and validValue_p to initial values and empty message log
60-
54: StartRound(0)
61-
62-
There is no need to check decision_p[h_p] = nil since it is implied that decision are made
63-
sequentially, i.e. x, x+1, x+2... . The validity of the proposal value can be checked in the same if
64-
statement since there is no else statement.
65-
*/
66-
func (t *Tendermint[V, H, A]) line49WhenProposalIsReceived(p Proposal[V, H, A], vID H, validProposal, proposalFromProposer bool) bool {
67-
precommits, hasQuorum := t.checkForQuorumPrecommit(p.R, vID)
68-
69-
if validProposal && proposalFromProposer && hasQuorum {
70-
// After committing the block, how the new height and round is started needs to be coordinated
71-
// with the synchronisation process.
72-
t.blockchain.Commit(t.state.h, *p.Value, precommits)
73-
74-
t.messages.deleteHeightMessages(t.state.h)
75-
t.state.h++
76-
t.startRound(0)
77-
78-
return true
79-
}
80-
return false
81-
}
82-
83-
/*
84-
Check the upon condition on line 22:
85-
86-
22: upon {PROPOSAL, h_p, round_p, v, nil} from proposer(h_p, round_p) while step_p = propose do
87-
23: if valid(v) ∧ (lockedRound_p = −1 ∨ lockedValue_p = v) then
88-
24: broadcast {PREVOTE, h_p, round_p, id(v)}
89-
25: else
90-
26: broadcast {PREVOTE, h_p, round_p, nil}
91-
27: step_p ← prevote
92-
93-
The implementation uses nil as -1 to avoid using int type.
94-
95-
Since the value's id is expected to be unique the id can be used to compare the values.
96-
*/
97-
func (t *Tendermint[V, H, A]) line22(vr round, proposalFromProposer, validProposal bool, vID H) {
98-
if vr == -1 && proposalFromProposer && t.state.s == propose {
99-
var votedID *H
100-
if validProposal && (t.state.lockedRound == -1 || (*t.state.lockedValue).Hash() == vID) {
101-
votedID = &vID
102-
}
103-
t.sendPrevote(votedID)
104-
}
105-
}
106-
107-
/*
108-
Check the upon condition on line 28:
109-
110-
28: upon {PROPOSAL, h_p, round_p, v, vr} from proposer(h_p, round_p) AND 2f + 1 {PREVOTE,h_p, vr, id(v)} while
111-
step_p = propose ∧ (vr ≥ 0 ∧ vr < round_p) do
112-
29: if valid(v) ∧ (lockedRound_p ≤ vr ∨ lockedValue_p = v) then
113-
30: broadcast {PREVOTE, hp, round_p, id(v)}
114-
31: else
115-
32: broadcast {PREVOTE, hp, round_p, nil}
116-
33: step_p ← prevote
117-
118-
Ideally, the condition on line 28 would be checked in a single if statement, however,
119-
this cannot be done because valid round needs to be non-nil before the prevotes are fetched.
120-
*/
121-
func (t *Tendermint[V, H, A]) line28WhenProposalIsReceived(vr round, proposalFromProposer bool,
122-
vID H, validProposal bool,
123-
) {
124-
if vr != -1 && proposalFromProposer && t.state.s == propose && vr >= 0 && vr < t.state.r {
125-
hasQuorum := t.checkQuorumPrevotesGivenProposalVID(vr, vID)
126-
if hasQuorum {
127-
var votedID *H
128-
if validProposal && (t.state.lockedRound <= vr || (*t.state.lockedValue).Hash() == vID) {
129-
votedID = &vID
130-
}
131-
t.sendPrevote(votedID)
132-
}
133-
}
134-
}
135-
136-
/*
137-
Check upon condition on line 36:
138-
139-
36: upon {PROPOSAL, h_p, round_p, v, ∗} from proposer(h_p, round_p) AND 2f + 1 {PREVOTE, h_p, round_p, id(v)} while
140-
valid(v) ∧ step_p ≥ prevote for the first time do
141-
37: if step_p = prevote then
142-
38: lockedValue_p ← v
143-
39: lockedRound_p ← round_p
144-
40: broadcast {PRECOMMIT, h_p, round_p, id(v))}
145-
41: step_p ← precommit
146-
42: validValue_p ← v
147-
43: validRound_p ← round_p
148-
149-
The condition on line 36 can should be checked in a single if statement, however,
150-
checking for quroum is more resource intensive than other conditions, therefore, they are checked
151-
first.
152-
*/
153-
func (t *Tendermint[V, H, A]) line36WhenProposalIsReceived(p Proposal[V, H, A], validProposal,
154-
proposalFromProposer bool, prevotesForHR map[A][]Prevote[H, A], vID H,
155-
) {
156-
if validProposal && proposalFromProposer && !t.state.lockedValueAndOrValidValueSet && t.state.s >= prevote {
157-
var vals []A
158-
for addr, valPrevotes := range prevotesForHR {
159-
for _, v := range valPrevotes {
160-
if *v.ID == vID {
161-
vals = append(vals, addr)
162-
}
163-
}
164-
}
165-
166-
if t.validatorSetVotingPower(vals) >= q(t.validators.TotalVotingPower(p.H)) {
167-
cr := t.state.r
168-
169-
if t.state.s == prevote {
170-
t.state.lockedValue = p.Value
171-
t.state.lockedRound = cr
172-
t.sendPrecommit(&vID)
173-
}
174-
175-
t.state.validValue = p.Value
176-
t.state.validRound = cr
177-
t.state.lockedValueAndOrValidValueSet = true
178-
}
179-
}
180-
}

‎consensus/tendermint/rule_first_proposal.go

+25
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
package tendermint
2+
3+
/*
4+
Check the upon condition on line 22:
5+
6+
22: upon {PROPOSAL, h_p, round_p, v, nil} from proposer(h_p, round_p) while step_p = propose do
7+
23: if valid(v) ∧ (lockedRound_p = −1 ∨ lockedValue_p = v) then
8+
24: broadcast {PREVOTE, h_p, round_p, id(v)}
9+
25: else
10+
26: broadcast {PREVOTE, h_p, round_p, nil}
11+
27: step_p ← prevote
12+
13+
The implementation uses nil as -1 to avoid using int type.
14+
15+
Since the value's id is expected to be unique the id can be used to compare the values.
16+
*/
17+
func (t *Tendermint[V, H, A]) line22(vr round, proposalFromProposer, validProposal bool, vID H) {
18+
if vr == -1 && proposalFromProposer && t.state.s == propose {
19+
var votedID *H
20+
if validProposal && (t.state.lockedRound == -1 || (*t.state.lockedValue).Hash() == vID) {
21+
votedID = &vID
22+
}
23+
t.sendPrevote(votedID)
24+
}
25+
}

‎consensus/tendermint/rule_polka_any.go

+21
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
package tendermint
2+
3+
import (
4+
"maps"
5+
"slices"
6+
)
7+
8+
/*
9+
Check the upon condition on line 34:
10+
11+
34: upon 2f + 1 {PREVOTE, h_p, round_p, ∗} while step_p = prevote for the first time do
12+
35: schedule OnTimeoutPrevote(h_p, round_p) to be executed after timeoutPrevote(round_p)
13+
*/
14+
func (t *Tendermint[V, H, A]) line34(p Prevote[H, A], prevotesForHR map[A][]Prevote[H, A]) {
15+
vals := slices.Collect(maps.Keys(prevotesForHR))
16+
if !t.state.timeoutPrevoteScheduled && t.state.s == prevote &&
17+
t.validatorSetVotingPower(vals) >= q(t.validators.TotalVotingPower(p.H)) {
18+
t.scheduleTimeout(t.timeoutPrevote(p.R), prevote, p.H, p.R)
19+
t.state.timeoutPrevoteScheduled = true
20+
}
21+
}

0 commit comments

Comments
 (0)