$$ \newcommand \pk {\mathrm{pk}} \newcommand \sk {\mathrm{sk}} \newcommand \fv {\text{first}} \newcommand \lv {\text{last}} \newcommand \Vote {\mathrm{Vote}} \newcommand \Equivocation {\mathrm{Equivocation}} \newcommand \Propose {\mathit{propose}} \newcommand \Soft {\mathit{soft}} \newcommand \Cert {\mathit{cert}} \newcommand \Late {\mathit{late}} \newcommand \Redo {\mathit{redo}} \newcommand \Down {\mathit{down}} \newcommand \Seed {\mathrm{Seed}} \newcommand \Record {\mathrm{Record}} \newcommand \Stake {\mathrm{Stake}} \newcommand \CommitteeSize {\mathrm{CommitteeSize}} \newcommand \CommitteeThreshold {\mathrm{CommitteeThreshold}} \newcommand \Sign {\mathrm{Sign}} \newcommand \Verify {\mathrm{Verify}} \newcommand \abs[1] {\lvert #1 \rvert} $$

Votes

Let

• \( I \) be an address,

• \( r \) be a round,

• \( p \) be a period,

• \( s \) be a step,

• \( v \) be a proposal-value.

Let \( x \) be a canonical encoding of the 5-tuple \( (I, r, p, s, v) \), and let \( x’ \) be a canonical encoding of the 4-tuple \( (I, r, p, s) \).

Let \( y \) be an arbitrary bitstring.

Then we say that the tuple

$$ (I, r, p, s, v, y) $$

is a vote from \( I \) for \( v \) at round \( r \), period \( p \), step \( s \) (or a vote from \( I \) for \( v \) at \( (r, p, s) \)), denoted

$$ \Vote(I, r, p, s, v) $$

⚙️ IMPLEMENTATION

Vote reference implementation.

Moreover, let \( L \) be a ledger where \( \abs{L} \geq \delta_b \).

Let

• \( (\sk, \pk) \) be a keypair,
• \( B, \bar{B} \) be 64-bit integers,
• \( Q \) be a 256-bit integer,
• \( \tau, \bar{\tau} \) 32-bit integers.

We say that this vote is valid with respect to \( L \) (or simply valid if \( L \) is unambiguous) if the following conditions are true:

⚙️ IMPLEMENTATION

The reference implementation builds an asynchronous vote verifier, which builds a verification pool and under the hood uses two different verifying routines: one for regular unauthenticated votes, and one for unauthenticated equivocation votes.

See the non-normative Algorand ABFT Overview for further details.

• \( r \leq |L| + 2 \)

• Let \( v = (I_{orig}, p_{orig}, d, h )\).

  • If \( s = 0 \), then \( p_{orig} \le p \).
  • Furthermore, if \( s = 0 \) and \( p = p_{orig} \), then \( I = I_{orig} \).

• If \( s \in \{ \Propose, \Soft, \Cert, \Late, \Redo\} \), \( v \neq \bot \). Conversely, if \( s = \Down \), \( v = \bot \).

• Let

  • \( (\pk, B, r_\fv, r_\lv) = \Record(L, r - \delta_b, I) \),
  • \( \bar{B} = \Stake(L, r - \delta_b, r) \),
  • \( Q = \Seed(L, r - \delta_s) \),
  • \( \tau = \CommitteeThreshold(s) \),
  • \( \bar{\tau} = \CommitteeSize(s) \).

  Then

  • \( \Verify(y, x, x’, \pk, B, \bar{B}, Q, \tau, \bar{\tau}) \neq 0 \),
  • \( r_\fv \leq r \leq r_\lv \).

Observe that valid votes contain outputs of the \( \Sign \) procedure; i.e., \( y := \Sign(x, x’, \sk, B, \bar{B}, Q, \tau, \bar{\tau}) \).

Informally, these conditions check the following:

• The vote is not too far in the future for \( L \) to be able to validate.

• “Propose”-step votes can either propose a new proposal-value for this period (\( p_{orig} = p \)) or claim to “re-propose” a value originally proposed in an earlier period (\( p_{orig} < p \)). But they can’t claim to “re-propose” a value from a future period. And if the proposal-value is new (\( p_{orig} = p \)) then the “original proposer” must be the voter.

• The \( \Propose \), \( \Soft \), \( \Cert \), \( \Late \), and \( \Redo \) steps must vote for an actual proposal. The \( \Down \) step must only vote for \( \bot \).

• The last condition checks that the vote was properly signed by a voter who was selected to serve on the committee for this round, period, and step. The committee selection process uses the voter’s stake and keys as of \( \delta_b \) rounds before the vote and the seed as of \(\delta_s\) rounds before the vote. It also checks if the vote’s round is within the range associated with the voter’s participation key.

An equivocation vote pair or equivocation vote \( \Equivocation(I, r, p, s) \) is a pair of votes that differ in their proposal values. In other words,

$$ \begin{aligned} \Equivocation(I, r, p, s) = (&\Vote(I, r, p, s, v_1), \\ &\Vote(I, r, p, s, v_2)) \end{aligned} $$

for some \( v_1 \neq v_2 \).

An equivocation vote pair is valid with respect to \( L \) (or simply valid if \( L \) is unambiguous) if both of its constituent votes are also valid with respect to \( L \).