Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

• Auto
• Light
• Dark

Algorand Specifications

We define the player state SS to be the following tuple:

S=(r,p,s,s¯,V,P,v¯)

where

• rr is the current round,
• pp is the current period,
• ss is the current step,
• s¯s¯ is the last concluding step,
• VV is the set of all votes,
• PP is the set of all proposals, and
• v¯v¯ is the pinned value.

We say that a player has observed

• Proposal(v) if Proposal(v)∈P,
• Vote(r,p,s,v) if Vote(r,p,s,v)∈V,
• Bundle(r,p,s,v) if Bundle(r,p,s,v)⊂V,
• That the round rr (period p=0) has begun if there exists some pp such that Bundle(r−1,p,cert,v) was also observed for some vv,
• That the round rr, period p>0 has begun if there exists some pp such that either
  • Bundle(r,p−1,s,v) was also observed for some s>cert,v, or
  • Bundle(r,p,soft,v) was observed for some vv.

An event causes a player to observe something if the player has not observed that thing before receiving the event and has observed that thing after receiving the event. For instance, a player may observe a vote VoteVote, which adds this vote to VV:

N((r,p,s,s¯,V,P,v¯),L0,Vote)=((r′,p′,…,V∪{Vote},P,v¯′),L1,…)

We abbreviate the transition above as

N((r,p,s,s¯,V,P,v¯),L0,Vote)=((S∪Vote,P,v¯),L1,…)

Note that observing a message is distinct from receiving a message. A message which has been received might not be observed (for instance, the message may be from an old round). Refer to the relay rules for details.

We define two functions μ(S,r,p),σ(S,r,p), which are defined as follows:

The frozen value μ(S,r,p) is defined as the proposal-value vv in the proposal vote in round rr and period pp with the minimal credential.

More formally, then, let

Vr,p,0={Vote(I,r,p,0,v) | Vote∈V}

where VV is the set of votes in SS.

Then if Votel(r,p,0,vl) is the vote with the smallest weight in Vr,p, then μ(S,r,p)=vl.

If Vr,p is empty, then μ(S,r,p)=⊥.

The staged value σ(S,r,p) is defined as the sole proposal-value for which there exists a soft-bundle in round rr and period pp.

More formally, suppose Bundle(r,p,Soft,v)⊂V. Then σ(S,r,p)=v.

If no such soft-bundle exists, then σ(S,r,p)=⊥.

If there exists a proposal-value vv such that Proposal(v)∈P and σ(S,r,p)=v, we say that vv is committable for round rr, period pp (or simply that vv is committable if (r,p) is unambiguous).

Important

IMPLEMENTATION:
The current implementation constructs a Proposal Tracker which, amongst other things, is in charge of handling both frozen and staged value tracking.