Made clear that we work backwards for accoutable safety

pdf/grandpa.tex

@@ -313,9 +313,9 @@ The first thing we want to show is asynchronous safety, assuming we have at most
 \begin{theorem} \label{thm:accountable} 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$ voters who precomitted $\geq B'$ in round $r$ in their commit messages, so we ask them why they precomitted.
+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$ voters who precomitted $\geq B'$ or equivocated in round $r$ in their commit messages, so we ask those who precommitted $\geq B'$ why they did so.
 
-We ask queries of the following form: 
+Starting with $r''='$, 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}
@@ -326,9 +326,9 @@ The response is of the following form:
 \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}
 
-Any honest voter should respond.  In particular, if no voter responds, then we consider all $n-f$ voters how should have responded but didn't as Byzantine and we return this set of voters. If any do respond, then if $r'' > r+1$, we can ask the same query for at least $n-f$ validators in round $r''-1$. (Note that if any do respond, we will not punish non-responders.)
+Any honest voter should respond.  In particular, if no voter responds, then we consider all  voters how should have responded but didn't as Byzantine and we return this set of voters, along with any equivocators, which will be at least $n-f$ voters total. If any do respond, then if $r'' > r+1$, we can ask the same query for at least $n-f$ validators in round $r''-1$. (Note that if any do respond, we will not punish non-responders.)
 
-If any voters 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 we ask such queries for a vote in all rounds between $r''=r'$ and $r''=r+1$ and get valid responses, since some voter responds 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.
 
@@ -342,14 +342,14 @@ If we get a set $S$ of prevotes for round $r$ that does not have a supermajority
 
 If any give a valid response, by a similar argument to the above, $S \cup T$ will have $f+1$ equivocations.
 
-So we either discover $f+1$ equivocations in a vote or else $n-f > f+1$ voters fail to validly respond like a honest voter could do to a query.
+So we either discover $f+1$ equivocations in a vote or else $n-f > f+1$ voters either equivocate or fail to validly respond like a honest voter could do to a query.
 
 
 \begin{lemma} \label{lem:honest-answer}
 An honest voter can answer the first type of query.
 \end{lemma}
 We first show that, if a prevote or precommit in round $r$ is cast by an honest voter $v$ for a block $B''$, then at the time of the vote we had $B'' \geq E_{r-1,v}$.
-Prevotes should be for the head of a chain containing either $E_{r-1,v}$ or $g(V_{r,v})$ by step 2 or 3.  Since $g(V_{r,v}) \geq E_{r-1,v}$, in either case we have $B'' \geq E_{r-1,v}$. Precommits should be for $g(V_{r,v})$ but $v$ waits until $g(V_{r,v}) \geq E_{r-1,v}$, by step 4, before precommiting, so again this holds.
+Prevotes should be for the head of a chain containing either $E_{r-1,v}$ or some $B''' > E_{r-1,v}$ by step 2 or 3.  In either case we have $B'' \geq E_{r-1,v}$. Precommits should be for $g(V_{r,v})$ but $v$ waits until $g(V_{r,v}) \geq E_{r-1,v}$, by step 4, before precommiting, so again this holds.
 It follows that, if $B'' \not\geq B$, then we had $E_{r-1,v} \not\geq B$.
 
 We next show that if we had $E_{r-1,v} \not\geq B$ at the time of the vote then we can respond to the query validly, by demonstrating the impossiblity of a supermajority for $B$. 
@@ -393,7 +393,7 @@ Since $v$ sees that $r$ is completable at time $t$,
 either $E_{r,v} < g(V_{r,v})$ requiring $(n+f+1)/2 > 2f + 1$ votes, or else it is impossible for $C_{r,v}$ to have a supermajority for any children of $g(V_{r,v})$, requiring $2f + 1$ votes.
 In either case, both $V_{r,v,t}$ and $C_{r,v,t}$ contain votes from $2f + 1$ voters and so the same holds for $V_{r,v',t'}$ and $C_{r,v',t'}$. 
 By Lemma \ref{lem:ghost-monotonicity} (ii), $g(V_{r,v',t'}) \geq g(V_{r,v,t})$.
-As it is impossible for $C_{r,v,t}$ to have a supermajority for any children of $g(V_{r,v,t})$, it follows from Lemma \ref{lem:impossible} (i \& ii) that it is impossible for $C_{r,v',t'})$ as well, and so both $E_{r,v',t'} \leq g(V_{r,v,t})$ and $v'$ sees $r$ is completable at time $t'$.
+As it is impossible for $C_{r,v,t}$ to have a supermajority for any children of $g(V_{r,v,t})$, it follows from Lemma \ref{lem:impossible} (i \& ii) that it is impossible for $C_{r,v',t'}$ as well, and so both $E_{r,v',t'} \leq g(V_{r,v,t})$ and $v'$ sees $r$ is completable at time $t'$.
 But now $E_{r,v,t}$ and $E_{r,v',t'}$ are the last blocks on $\textrm{chain}(g(V_{r,v,t}))$ for which it is possible for $C_{r,v,t}$ and $C_{r,v',t'}$ respectively to have a supermajority, 
 As it is possible for $C_{r,v',t'}$ to have a supermajority for $E_{r,v',t'}$, then it is possible for $C_{r,v,t}$ to have a supermajority for $E_{r,v',t'}$ as well, by Lemma \ref{lem:impossible} (ii) and tolerance assumptions, so $E_{r,v',t'} \leq E_{r,v,t}$.
 \end{proof}
@@ -491,7 +491,7 @@ For (b), combining (a) and Lemma \ref{lem:timings} (iii), we have that any hones
 
 \begin{proof} By Lemma \ref{lem:timings} and our network assumptions, no honest voter  prevotes before time $t_r+2T \geq t_{r,v}+2T$ and so at this time, they will have seen all prevotes and precommits seen by $v$ at $t_{r,v}$ and the block $B$ if $v$ broadcast it then. By Lemma \ref{lem:message-monotonicity-completed-estimate}, any honest voter $v'$ has $E_{r-1,v'} \leq B \leq g(V_{r-1,v}$ then.
 
-So if the primary broadcast $B$, then $v'$ prevotes for the best chain including $B$. If the primary did not broadcast $B$, then they finalise it. By Corollary \ref{cor:overestimate-final}, it must be that $E_{r-1,v'} \geq B$ and so $E_{r-1,v'}=B$ and so in this case $v'$ also prevotes for th best chain including $B$.
+So if the primary broadcast $B$, then $v'$ prevotes for the best chain including $B$. If the primary did not broadcast $B$, then they finalise it. By Corollary \ref{cor:overestimate-final}, it must be that $E_{r-1,v'} \geq B$ and so $E_{r-1,v'}=B$ and so in this case $v'$ also prevotes for the best chain including $B$.
 
 Since all honest voters prevote $\geq B$, $g(H_r) \geq B$ and so by Lemma \ref{lem:honest-prevote-timings}, all honest participants finalise $B$ by time $t_r+6T$
 \end{proof}
@@ -517,11 +517,11 @@ By assumption these chains include $B'$ and so $g(H_r) \geq B$. By Lemma \ref{le
 
 \begin{lemma} \label{lem:honest-recent-validity}
 Suppose that $t_r \geq \GST$, the primary of round $r$ is honest and all votes have at most $f$ Byzantine voters.
-Let $B$ be a block that no prevoter in round $r$ saw as being in the best chain of an ancestor of $B$ at the time they prevoted.
+Let $B$ be a block that less than $f+1$ honest prevoters in round $r$ saw as being in the best chain of an ancestor of $B$ at the time they prevoted.
 Then either all honest participants finalise $B$ before time $t_r+6T$ or no honest participant ever has $g(V_{r,v}) \geq B$ or $E_{r,v} \geq B$.
 \end{lemma}
 
-\begin{proof} Let $v'$ be the primary of round $r$ and let $B'=E_{r-1,v',t_{r,v'}}$. If $B' \geq B$, then by Lemma \ref{lem:primary-finalises}, all honest participants finalise $B$ by time $t_r+6T$. If $B' \not\geq B$, then by Lemma \ref{lem:primary-finalises}, no honest voter prevotes $\geq B$ and so no honest participant ever has $g(V_{r,v}) \geq B$.
+\begin{proof} Let $v'$ be the primary of round $r$ and let $B'=E_{r-1,v',t_{r,v'}}$. If $B' \geq B$, then by Lemma \ref{lem:primary-finalises}, all honest participants finalise $B$ by time $t_r+6T$. If $B' \not\geq B$, then by Lemma \ref{lem:primary-finalises}, at most $f$ honest voters prevotes $\geq B$. In this case, less than $2f+1 \leq (n+f+1)/2$ prevoters vote $\geq B$ or equivocate and so no honest participant ever has $g(V_{r,v}) \geq B$.
 \end{proof}
 
 
@@ -673,7 +673,7 @@ Here $g_{t}(S)$ is the $t$-GHOST function defined as follows. We construct a cha
 The idea behind the proof of asynchronous liveness is that for a particular block $B'$, some value of the common coin, either all the honest voters who received $4/5$ of precommits before the common coin was decided lock to $B'$ or none do.
 If we had a fixed threshold for locking, an adversarial choice of the number of precommits for $B'$ or its descendants could lead to some voters locking to it and some not (and indeed there would be runs that do this indefinitely as this is how the impossibility result works for this type of algorithm.)
 
-Firstly we note that much of the machinery of ? and ? carries over to the $1/5$ byzantine case.
+Firstly we note that much of the machinery of section $\ref{sec:prelims}$ carries over to the $1/5$ byzantine case.
 
 \begin{lemma} \label{lem:ghost-monotonicity-general}
 Let $T$ be a set of votes such that at most $f$ voters have multiple votes in $T$. Let $t \geq (n+f)/2n$ Then