In the SCP, condition 2 of the accept definition allows a node to vote for one statement and later accept a contradictory one. Condition 2 assumes the existence of a v-blocking set which has not only voted for a but also accepted it. What is the argument to show that this is the case?
1 Answer
$\begingroup$
$\endgroup$
What is guaranteed is that if a quorum of an intact nodes accepts a statement s, then eventually every intact node v will find itself v-blocked by a set of nodes that has accepted s, i.e. "accept s" cascades throughout all intact nodes until all have accepted and then confirmed s. This is called the cascade theorem in the paper "Fast and secure global payments with Stellar". You can find a brief justification of this theorem at the end of section 3.1.2. There is also a formal proof in Isabelle/HOL here: https://github.com/stellar/scp-proofs. Finally it is also guaranteed that if an intact node is v-blocked by "accept s", then at least one intact node saw a quorum voting for s.
