docs: ABFT broadcast rules update

src/abft-broadcast-rules-recovery.md

@@ -12,8 +12,8 @@ On observing a timeout event of
 
 - \\( T = \DeadlineTimeout(p) \\) or
 
-- \\( T = \DeadlineTimeout(p) + 2^{s_t}\lambda + u \\) where
-\\( u \in [0, 2^{s_t}\lambda] \\) sampled uniformly at random, 
+- \\( T = \DeadlineTimeout(p) + 2^{s_t}\lambda + u \\) where \\( 0 < s_t \leq 249 \\)
+and \\( u \in [0, 2^{s_t}\lambda] \\) sampled uniformly at random, 
 
 the player attempts to resynchronize and then broadcasts*
 \\( \Vote(I, r, p, \Next_h, v) \\) where
@@ -26,6 +26,13 @@ such that \\( \Bundle(r, p-1, s_1, \bar{v} )\\) was observed,
 
 - and \\( v = \bot \\) otherwise.
 
+Note that the broadcast vote:
+
+- Is for step \\( \Next_0 \\) if \\( T = \DeadlineTimeout(p) \\),
+
+- Is for step \\( \Next_{s_t} \\) in any other case (this is, \\( h = 0 \\) or
+\\( h = s_t \\) according to the observed timeout event).
+
 {{#include ./.include/styles.md:impl}}
 > Next vote issuance [reference implementation](https://github.com/algorand/go-algorand/blob/b6e5bcadf0ad3861d4805c51cbf3f695c38a93b7/agreement/player.go#L214).
 >

src/abft-broadcast-rules-reproposals.md

@@ -5,6 +5,10 @@ $$
 
 # Reproposal Payloads
 
+A proposal rebroadcasting behavior is in place to further mitigate the chance of
+players reaching certification on a proposal-value for which its corresponding
+proposal has not been observed.
+
 On observing \\( \Vote(I, r, p, 0, v) \\), if \\( \Proposal(v) \in P \\) then the
 player broadcasts \\( \Proposal(v) \\).
 

src/abft-broadcast-rules-resync.md

@@ -13,23 +13,37 @@ A resynchronization attempt involves the following stages.
 
 First, the player broadcasts its _freshest bundle_, if one exists.
 
-A player's freshest bundle is a complete bundle defined as follows:
+We define a partial order relation of _freshness_, \\( f_> \\), in a hypothetical
+set of complete bundles observed for the same round \\( r \\). Given two distinct
+complete observed bundles, \\( \Bundle_e(r, p_e, s_e, v_e) \\) and \\( \Bundle_o(r, p_o, s_o, v_o) \\),
+then:
 
-- \\( \Bundle(r, p, \Soft, v) \subset V \\) for some \\( v \\), if it exists, or
-else
+- \\( \Bundle_e(r, p_e, \Cert, v_e) f_> \Bundle_o(r, p_o, s_o, v_o) \\) (note that it
+is implicitly assumed that \\( s_o \neq \Cert \\)), or else
 
-- \\( \Bundle(r, p-1, s, \bot) \subset V \\) for some \\( s > \Cert \\), if it exists,
-or else
+- \\( s_o, s_e \neq \Cert \\) and \\( \Bundle_e(r, p+i, s_e, v_e) f_> \Bundle_o(r, p, s_o, v_o) \\),
+with \\( i > 0 \\), or else
 
-- \\( \Bundle(r, p-1, s, v) \subset V \\) for some \\( s > \Cert, v \neq \bot \\),
-if it exists.
+- \\( \Bundle_e(r, p, Next_s, v_e) f_> \Bundle_o(r, p, \Soft, v_o )\\), otherwise
+
+- \\( Bundle_e(r, p, \Next_s, \bot) \ f_> \Bundle_o(r, p, \Next_{s'}, v_o) \\)
+(for any \\( v_o \neq \bot \\)).
+
+For all other cases, the relation is undefined.
 
 {{#include ./.include/styles.md:impl}}
 > Freshness relation [reference implementation](https://github.com/algorand/go-algorand/blob/b6e5bcadf0ad3861d4805c51cbf3f695c38a93b7/agreement/events.go#L745).
 
 Second, if the player broadcasted a bundle \\( \Bundle(r, p, s, v) \\), and \\( v \neq \bot \\),
 then the player broadcasts \\( \Proposal(v) \\) if the player has it.
 
+Third, if no \\( \Proposal(v) \\) associated with the freshest bundle exists, the protocol
+still falls back to relaying the pinned value \\( \bar{v} \\) for liveness.
+
+{{#include ./.include/styles.md:impl}}
+> In the [reference implementation](https://github.com/algorand/go-algorand/blob/b6e5bcadf0ad3861d4805c51cbf3f695c38a93b7/agreement/player.go#L518),
+> resynchronization attempts are performed by the `partitionPolicy(.)` function.
+
 Specifically, a resynchronization attempt:
 
 - Corresponds to no additional outputs if no freshest bundle exists
@@ -39,12 +53,22 @@ N(S, L, \ldots) = (S', L', \ldots),
 $$
 
 - Corresponds to a broadcast of the freshest bundle after a relay output and before
-any subsequent broadcast outputs, if said bundle exists, no matching proposal exists
+any subsequent broadcast outputs, if said bundle exists, no matching proposal exists,
+and the pinned value \\( \bar{v} = \bot \\) for the same round
 
 $$
 N(S, L, \ldots) = (S', L', (\ldots, \Bundle^\ast(r, p, s, v), \ldots)),
 $$
 
+- Corresponds to a broadcast of the freshest bundle and the pinned value for the same
+round after a relay output and before any subsequent broadcast outputs, if said bundle
+exists, no matching proposal exists, and a pinned value \\( \bar{v} \\) for the same
+round exists
+
+$$
+N(S, L, \ldots) = (S', L', (\ldots, \Bundle^\ast(r, p, s, v), \bar{v}, \ldots)),
+$$
+
 - Otherwise corresponds to a broadcast of both a bundle and its associated
 proposal after a relay output and before any subsequent broadcast
 outputs