$$ \newcommand \Domain[1] {\texttt{#1}} $$
$$ \newcommand \Vote {\mathrm{Vote}} \newcommand \Proposal {\mathrm{Proposal}} \newcommand \Bundle {\mathrm{Bundle}} \newcommand \Soft {\mathit{soft}} \newcommand \Cert {\mathit{cert}} \newcommand \Next {\mathit{next}} \newcommand \Priority {\mathrm{Priority}} \newcommand \VRF {\mathrm{VRF}} \newcommand \ProofToHash {\mathrm{ProofToHash}} \newcommand \Hash {\mathrm{Hash}} \newcommand \Encoding {\mathrm{Encoding}} $$
Player State Definition
We define the player state \( S \) to be the following tuple:
$$ S = (r, p, s, \bar{s}, V, P, \bar{v}, H) $$
where
- \( r \) is the current round,
- \( p \) is the current period,
- \( s \) is the current step,
- \( \bar{s} \) is the last concluding step,
- \( V \) is the set of accepted votes,
- \( P \) is the set of validated proposal payloads,
- \( \bar{v} \) is the pinned value,
- \( H \) is the ordered history of protocol events and outputs.
The definitions below are derived from \( S \); observation, threshold formation, and freshness comparisons are evaluated in \( H \) order.
We say that a player has observed
- \( \Proposal(v) \) if \( \Proposal(v) \in P \),
- \( \Vote(I, r, p, s, v) \) if \( \Vote(I, r, p, s, v) \in V \),
- \( \Bundle(r, p, s, v) \) if \( \Bundle(r, p, s, v) \subset V \) and its threshold is fresher than every threshold previously observed for round \( r \),
- That the round \( r > 0 \) (period \( p = 0 \)) has begun if an entry was committed in round \( r-1 \),
- That the round \( r \), period \( p > 0 \) has begun if either
- \( \Bundle(r, p-1, s, v) \) was observed for some \( s > \Cert, v \), or
- \( \Bundle(r, p, s, v) \) was observed for some \( s \in { \Soft, \Cert }, v \).
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 \( \Vote \), which adds this vote to \( V \):
$$ N((r, p, s, \bar{s}, V, P, \bar{v}, H), L, \Vote) = ((r’, p’, s’, \bar{s}‘, V \cup \{\Vote\}, P, \bar{v}’, H’), L’, \ldots) $$
We write \( S’ \cup \{\Vote\} \) for an output state whose \( V \) additionally contains \( \Vote \), and \( S’ \cup \{\Proposal(v)\} \) likewise for \( P \); thus the transition above is
$$ N((r, p, s, \bar{s}, V, P, \bar{v}, H), L, \Vote) = (S’ \cup \{\Vote\}, L’, \ldots) $$
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.
Special Values
We define two functions \( \mu(S, r, p), \sigma(S, r, p) \), which are defined as follows:
The frozen value \( \mu(S, r, p) \) is defined as the proposal-value \( v \) in the highest-priority accepted proposal vote in round \( r \) and period \( p \).
More formally, then, let
$$ V_{r, p, 0} = \{\Vote(I, r, p, 0, v) | \Vote \in V\} $$
where \( V \) is the set of votes in \( S \).
Let \( z_k \) be the raw selection-VRF output in \( \Vote_k \in V_{r, p, 0} \) and \( w_k \) its weight. Its priority is
$$ \Priority(\Vote_k) = \min_{1 \leq i \leq w_k}\Hash(\Domain{CR} || \Encoding((z_k, I_k, i))). $$
Hash outputs are compared as unsigned big-endian integers. A proposal vote has higher priority when its \( \Priority \) value is smaller. \( \mu(S, r, p) \) is the value of the highest-priority accepted proposal vote. It is fixed as soon as a value is staged for \( (r, p) \) or the player processes the filter timeout of period \( p \), whichever occurs first; later proposal votes do not change it.
If \( V_{r, p, 0} \) is empty, then \( \mu(S, r, p) = \bot \).
The staged value \( \sigma(S, r, p) \) is defined as the sole proposal-value for which the player observed a soft or cert threshold in round \( r \) and period \( p \).
More formally, if the player observed a threshold \( \Bundle(r, p, s, v) \), where \( s \in \{\Soft, \Cert\} \), then \( \sigma(S, r, p) = v \).
If no such threshold exists, then \( \sigma(S, r, p) = \bot \).
If there exists a proposal-value \( v \) such that \( \Proposal(v) \in P \) and \( \sigma(S, r, p) = v \), we say that \( v \) is committable for round \( r \), period \( p \) (or simply that \( v \) is committable if \( (r, p) \) is unambiguous).
The relevant value is
$$ \rho(S, r, p) = \begin{cases} \sigma(S, r, p) & \text{if } \sigma(S, r, p) \neq \bot, \\ \mu(S, r, p) & \text{otherwise}. \end{cases} $$
For each \( (r, p) \), let \( C(S, r, p) = (b, v) \) summarize the thresholds with step at least \( \Next_0 \) formed in \( H \): \( b = 1 \) if any has proposal value \( \bot \), and \( v \) is the proposal value of the latest threshold for a value \( \neq \bot \), or \( \bot \) if none exists.
For thresholds in one round, \( T_1 \) is fresher than \( T_0 \) if the first applicable condition holds:
- \( T_1 \) is a cert threshold and \( T_0 \) is not;
- Neither is a cert threshold and \( T_1 \) has the later period;
- They have the same period, \( T_1 \) is a next threshold, and \( T_0 \) is a soft threshold;
- Both are next thresholds in the same period, \( T_1 \) is for \( \bot \), and \( T_0 \) is not.
The numeric next-step index does not otherwise affect freshness. A threshold for a future round is considered when that round begins. The summary \( C \) includes thresholds that are not fresh enough to be observed.
Important
IMPLEMENTATION:
The current implementation constructs a Proposal Tracker which, amongst other things, is in charge of handling both frozen and staged value tracking.