docs: ABFT state machine update

src/abft-player-state.md

@@ -69,7 +69,20 @@ 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 proposal vote in round \\( r \\) and period \\( p \\) with the minimal credential.
+in the proposal vote in round \\( r \\) and period \\( p \\) that minimizes a credential
+priority function \\( \Priority(v) \\).
+
+Let
+
+- \\( I_j \\) be the address of a distinct player identified by the subscript \\( j \\),
+- \\( w_j \\) be the weight of the proposal vote for \\( v \\) by player \\( I_j \\),
+- \\( y \\) be the result of the signing procedure for \\( v \\) by player \\( I_j \\).
+
+Then the priority function is defined as
+
+$$
+\Priority(v) = \min_{i \in [0, w_j)} \left\\{ \Hash \left( \VRF.\ProofToHash(y) || I_j || i \right) \right\\}
+$$
 
 More formally, then, let
 
@@ -79,8 +92,14 @@ $$
 
 where \\( V \\) is the set of votes in \\( S \\).
 
-Then if \\( \Vote_l(r, p, 0, v_l) \\) is the vote with the smallest weight in
-\\( V_{r, p} \\), then \\( \mu(S, r, p) = v_l \\).
+Now if \\( \Vote(r, p, 0, v_{min}) \in V_{r, p, 0} \\) is the vote for the proposal
+value \\( v_\text{min} \\) such that
+
+$$
+v_\text{min} = \min_{\Vote(I, \ldots , v) \in V_{r, p, 0}}\\{\Priority(v)\\}
+$$
+
+then \\( \mu(S, r, p) = v_{min} \\).
 
 If \\( V_{r, p} \\) is empty, then \\( \mu(S, r, p) = \bot \\).