Add a set X for explicitly finding the Byzantine validators

pdf/grandpa.tex

@@ -246,7 +246,7 @@ If we receive a valid commit message for $B$ for round $r$, then it contains eno
 
 The first thing we want to show is asynchronous safety, assuming we have at most $f$ Byzantine validators.
 
-\begin{theorem} If the protocol finalises any two blocks $B,B'$ for which valid commit messages were sent, but which do not lie on the same chain, then there are at least $f+1$ Byzantine voters who all voted in a particular vote. Furthermore, there is a synchronous procedure to find some such of $f+1$ Byzantine voters.
+\begin{theorem} If the protocol finalises any two blocks $B,B'$ for which valid commit messages were sent, but which do not lie on the same chain, then there are at least $f+1$ Byzantine voters who all voted in a particular vote. Furthermore, there is a synchronous procedure to find some such set $X$ of $f+1$ Byzantine voters.
 \end{theorem}
 
 The challenge procedure works as follows: If $B$ and $B'$ are committed in the same round, then the union of their precommits must contain at least $f$ equivocations, so we are done.  Otherwise, we may assume by symmetry that $B$ was committed in round $r$ and $B'$ in round $r' > r$.  There are at least $n-f$ validators who precomitted $\geq B'$ in round $r$ in their commit messages, so we ask them why they precomitted.
@@ -255,17 +255,16 @@ We ask queries of the following form:
 \begin{itemize}
 \item Why was $E_{r''-1} \not\geq B$  when you prevoted for or precomitted to $B'' \not\geq B$ in round $r'' > r$?
 \end{itemize}
-	
-Any honest validator should be able to respond to this, as is shown in Lemma \ref{lem:honest-answer} below. 
+\noindent Any honest validator should be able to respond to this, as is shown in Lemma \ref{lem:honest-answer} below. 
 
 The response is of the following form:
 \begin{itemize}
 \item A either a set $S$ of prevotes for round $r''-1$, or else a set $S$ of precommits for round $r''-1$, in either case such that it is impossible for $S$ to have a supermajority for $B$.
 \end{itemize}
 
-If no validator responds, then we have $n-f$ Byzantine validators. If any do, then if $r'' > r+1$, we can ask the same query for at least $n-f$ validators in round $r''-1$.
+We consider any non-responsive validator to be Byzantine and add them to the set $X$.  In particular, if no validator responds, then we have $n-f$ Byzantine validators. If any do, then if $r'' > r+1$, we can ask the same query for at least $n-(f - |X|)$ validators in round $r''-1$, .
 
-If any responded and $r''=r+1$, then we have either a set $S$ of prevotes or precommits in round $r$ that show it is impossible for $S$ to have a supermajority for $B$ in round $r$.
+If any validators respond when $r''=r+1$, then we have either a set $S$ of prevotes or precommits in round $r$ that show it is impossible for $S$ to have a supermajority for $B$ in round $r$.
 
 If $S$ is a set of precommits, then if we take the union of $S$ and the set of precommits in the commit message for $B$, then the resulting set of precommits for round $r$ has a supermajority for $B$ and it is impossible for it to have a supermajority for $B$. This is possible if the set is not tolerant and so there must be at least $f+1$ voters who equivocate an so are Byzantine.
 
@@ -273,8 +272,7 @@ If we get a set $S$ of prevotes for round $r$ that does not have a supermajority
 \begin{itemize}
 \item Which prevotes for round $r$ have you seen?
 \end{itemize}
-
-to all the voters of precommit in the commit message for $B$  who voted for blocks $B'' \geq B$. There must be $n-f$ such validators and a valid response to this query is a set $T$ of prevotes for round $r$ with a supermajority for $B''$ and so a supermajority for $B$.
+\noindent to all the voters of precommit in the commit message for $B$  who voted for blocks $B'' \geq B$. There must be $n-f$ such validators and a valid response to this query is a set $T$ of prevotes for round $r$ with a supermajority for $B''$ and so a supermajority for $B$.
 
 If any give a valid response, by a similar argument to the above, $S \cup T$ will have $f+1$ equivocations.