## 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](https://specs.algorand.co/abft/abft-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](https://github.com/algorand/go-algorand/blob/b6e5bcadf0ad3861d4805c51cbf3f695c38a93b7/agreement/proposalTracker.go#L93) which, amongst other things, is in charge of handling both frozen and staged value tracking.