1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
// Copyright (C) 2019-2024 Algorand, Inc.
// This file is part of go-algorand
//
// go-algorand is free software: you can redistribute it and/or modify
// it under the terms of the GNU Affero General Public License as
// published by the Free Software Foundation, either version 3 of the
// License, or (at your option) any later version.
//
// go-algorand is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
// GNU Affero General Public License for more details.
//
// You should have received a copy of the GNU Affero General Public License
// along with go-algorand. If not, see <https://www.gnu.org/licenses/>.
package agreement
import (
"fmt"
)
// A voteMachine should track a new vote.
//
// Preconditions:
// - e.T = voteAccepted or voteFilterRequest
// - v.R.Step != propose
// - for all votes v = e.Vote, v.R.Step is the same
// - (Algorand safety assumptions on the equivocation of votes)
//
// Postconditions (let e be the returned event):
//
// if Input is of type voteAccepted:
// - e.T is one of {none, {soft,cert,next}Threshold}
// - e.T corresponds to the input event's step (e.g. if the input event had v.R.Step = soft, then e.T is either none or softThreshold)
// - e.T != none if and only if e.Bundle contains a valid bundle for e.Proposal
// - if e.T is a {soft,cert}Threshold event, it will be emitted at most once and e.Proposal != bottom
// - if e.T is a {next}Threshold event, it will be emitted at most once and e.Proposal != bottom
// if Input is of type voteFilterRequest:
// - e.T is one of {none, voteFilteredStep}
// - e.T = none for a given input only once (the first time the vote is seen, if we have not previously detected equivocation
//
// Trace properties
// - voteFilterRequest is idempotent
type voteTrackerContract struct {
_struct struct{} `codec:","`
Step step
StepOk bool
Emitted bool
}
func (c *voteTrackerContract) pre(p player, in0 event) (pre []error) {
switch in0.t() {
case voteAccepted:
in := in0.(voteAcceptedEvent)
if in.Vote.R.Step == propose {
pre = append(pre, fmt.Errorf("incoming event has step propose"))
}
if !c.StepOk {
c.StepOk = true
c.Step = in.Vote.R.Step
} else {
if c.Step != in.Vote.R.Step {
pre = append(pre, fmt.Errorf("incoming event has step %d but expected step %d", in.Vote.R.Step, c.Step))
}
}
return
case voteFilterRequest, dumpVotesRequest:
return
default:
pre = append(pre, fmt.Errorf("incoming event has invalid type: %v", in0.t()))
}
return
}
func (c *voteTrackerContract) post(p player, in0, out0 event) (post []error) {
switch in0.t() {
case voteAccepted:
in := in0.(voteAcceptedEvent)
switch out0.t() {
case none:
case softThreshold:
if in.Vote.R.Step != soft {
post = append(post, fmt.Errorf("incoming event has step %d but outgoing event has type softThreshold", in.Vote.R.Step))
}
case certThreshold:
if in.Vote.R.Step != cert {
post = append(post, fmt.Errorf("incoming event has step %d but outgoing event has type certThreshold", in.Vote.R.Step))
}
case nextThreshold:
if in.Vote.R.Step <= cert {
post = append(post, fmt.Errorf("incoming event has step %d but outgoing event has type nextThreshold", in.Vote.R.Step))
}
default:
post = append(post, fmt.Errorf("outgoing event has invalid type: %v", out0.t()))
}
switch out0.t() {
case softThreshold, certThreshold, nextThreshold:
if c.Emitted {
post = append(post, fmt.Errorf("event %v was emitted twice", out0))
} else {
c.Emitted = true
}
}
out := out0.(thresholdEvent)
switch out0.t() {
case softThreshold, certThreshold:
if out.Proposal == bottom {
post = append(post, fmt.Errorf("out.Proposal = bottom but out.T = %v", out.T))
}
}
emptyBundle := len(out.Bundle.Votes) == 0
if (out.T == none) != emptyBundle {
post = append(post, fmt.Errorf("out.T must be none if and only if out.Bundle is empty, but out.T = %v while len(out.Bundle.Votes) = %d", out.T, len(out.Bundle.Votes)))
}
if out.T != none && out.Proposal == bottom && out.Step < next {
post = append(post, fmt.Errorf("outgoing event has bottom proposal but step %d", out.Step))
}
return
case voteFilterRequest:
switch out0.t() {
case none:
case voteFilteredStep:
// once we write safety properties/contracts on traces, we can test the duplication detection
default:
post = append(post, fmt.Errorf("outgoing filter event has invalid type: %v", out0.t()))
}
default:
}
return
}
|
