(Partially) Explained Casper CBC specs
With pictures!
A consensus protocol is a mechanism that provides guarantees for a set of communicating agents to agree on something. In the blockchain context, nodes that download new blocks want to make sure they agree on a set of transactions as canonical, a unique history of the system. With Proof of Work (PoW), as soon as a node solves the hashing puzzle with a set of transactions, it can publish this set with a proof of solution to its peers and hope to be included in the canonical chain.
The drawbacks of PoW have been widely covered: its extremely wasteful energy consumption aside, it is not clear that its throughput can be significantly increased while maintaining the same level of security. [1] By making it very difficult to be granted the right to publish a new block, PoW effectively controls writing access to the main chain. Is there another way we could grant this right while maintaining integrity?
Any alternative would need to make it costly to produce faulty, out-of-consensus blocks. In PoW, should you decide to mine out of the main chain, agreed by consensus, your loss will be the work done (solving the cryptographic puzzle) to mine these non-consensus blocks. This loss can very well be measured in dollars and cents, via the energy wasted on the puzzle. Why not cut out the extrinsic penalties and make them intrinsic to the framework?
This is the strategy of Proof of Stake (PoS). In this paradigm, some nodes have the option to become validators. To do so, they must agree to lock up a certain amount of capital (in protocol currency, e.g.) and participate collectively in the selection of the canonical next block. If a validator starts acting funny and deviates from the protocol in a malicious way, its deposit is slashed, in true game theory fashion of rewards and punishments.
But for this idea to even be feasible, we need to understand what it means to equivocate. We call validators a set of consensus-forming peers. Validators must reach consensus on the chain and work to maintain a canonical version of the protocol history, in spite of faults. This is the object of the paper by Vlad Zamfir, Nate Rush, Aditya Asgaonkar and Georgios Piliouras. Aditya already gave an excellent overview of the paper and its place in consensus research. This post serves instead as a hand-holding walkthrough to visually see the concepts behind the maths! [2]
What is CBC?
When designing systems, more so for multibillion dollars systems, security is fundamental. Testing thoroughly the system is one way of ensuring the system works as intended. Is it acting in a predictable way? Does a given set of inputs lead to an internal inconsistency (perhaps, a crash)?
The Correct-By-Construction methodology takes a different approach. We specify a set of first principles and derive correctness by logical induction from these first principles: the CBC way. To be practically useful, the first principles should not be inconsistent and should be specified by a set of formal rules. From these rules, properties of the system can be derived by formal logic and proven to be correct always.
The CBC way, exposed in the paper, also entails the following: Parts of the system may be left undefined, i.e. await for further specifications. One can prove that some property P holds for mechanisms living in some space S. On a subset of S, say a subcategory of mechanisms S’, we may prove some property P’, in addition to P, that may not hold for mechanisms in S that are not in S’. For instance, take S to be the space of blockchain consensus mechanisms. Restrict S’ to be the space of mechanisms that use the longest chain fork choice rule. We know e.g. that the extra specification (the fork choice rule) gives us consistency, a property P’ that may not hold for any other rule. The paper thus starts from a general, abstract specification, of which any part can be further refined to yield additional properties.
The protocol space
CBC Casper’s strength lies in the definition of a general protocol space, that each successive refinement can build on and assume to be correct. The initial difficulty here is to understand where the protocol space lives. The mechanism needs a few basic elements: weighted validators who send each other messages, to arrive at consensus. With each new message, the protocol state grows.
The messages argue about the true value of some object out of a set of possible consensus values, and are sent to reach consensus on this value. If the set of possible values has two elements, it is a binary consensus. If the set is a set of possible blocks, it is a blockchain consensus. The general pattern of the messages is:
- A consensus value,
- A reference to a validator (the sender)
- A reference to some protocol state (the justification)
Definition 2.7 gives the (recursive) rules of construction of the protocol states and message sets. They are perhaps better understood by unrolling them for a few iterations:
Why do we need a justification? The notion of time is not trivial in an asynchronous protocol. While two messages may have been sent one after the other, there is no guarantee they will be received after some known delay by any other node. Thus, we need each message to justify itself, i.e. give a reference to some earlier protocol state that it builds on. Protocol states, in turn, are simply a set of messages, each of which refers to some anterior state. The figure below gives an example of a few protocol steps.
The notion of state transition formalises the concept of “after”: one state follows the other if the former includes all messages composing the latter. For instance, there is no state transition from {(1, B, ø)} to {(1, A, ø)}. Each state 𝜎 then defines a new futures cone: the set of possible states the protocol may transition to starting from state 𝜎.
Equivocation
So far, we have not considered what happens when validators equivocate, or in other words, send a pair of messages, none of which is justified by a state containing the other, as if existing in two different realities. At this point, the protocol can be thought of as branching, or living in two different threads.
Once validator B equivocates, and A notices, A will flag B as equivocating for the remainder of the protocol, and thus the weight of equivocating validators is nondecreasing. (Can you prove it? See page 7, “Note that F is a monotonic function”) States where the weight of all equivocating validators is lower than some constant t are said to belong to 𝛴_t.
By Theorem 2, as long as less than t validators equivocate, there is a common future where still less than t validators equivocate. Two protocol states have a common future if both can transition to some shared state. This means that for every honest validator, their “current” state (latest justification) leads to some other state that can also be reached by all other honest validators. This is good news since it allows us to stay in 𝛴_t and thus know at least one path exists where the number of equivocating validators is still less than t.
Safety of the protocol
When a common future exists (with equivocation weight smaller than some threshold t), agents must be able to decide what is true in the system. The end goal is to guarantee that agents cannot decide on a property and its opposite: they cannot decide that the consensus value is both 0 and 1. This is the safety guarantee.
A property is decided at some state 𝜎 if it is true in all futures of 𝜎. If some validators equivocate, we want to be certain that unless their weight is larger than some t, the property holds at all states in 𝛴_t that belong to the futures cone of 𝜎.
Of course, if a property is decided at some state 𝜎, it is also decided at a state 𝜎’ that belongs to the futures of 𝜎 (Lemma 2). Conversely, deciding a property at a state 𝜎 entails that it is not possible to have decided the negation of that property at a state 𝜎’ that contains 𝜎 in its futures (Lemma 3).
This is almost enough machinery to prove that nodes at different protocol states cannot decide on a property and its opposite, the desired safety guarantee. It is easy enough for two agents: either they agree or they each choose one of the (mutually exclusive) alternatives. When we have more than two agents however, no two properties decided by two agents may disagree, while all properties together may be inconsistent.
For instance, suppose that two switches need to be on for a light to switch on. Two agents observe the switches, while the third one observes the light itself. The following is “reported”: both switches are on, yet the light is off. Every pairwise combinations of report is consistent: that one switch is on does not imply the light necessarily is on, and two switches can be observed on at the same time. But it is the combination of all three that is inconsistent: one cannot observe both switches on while the light is turned off. Definitions 3.4 and 3.5 gives meaning to exactly this type of situation: A set of properties is consistent if there is a state where all hold at the same time.
Theorem 4 can then be stated: non-equivocating nodes make consistent decisions as long as the weight of equivocating validators is less than t. Safety is proven for decisions on protocol states!
Carrying over to consensus values
Until now, the decisions are only made over protocol states. We need something to carry us from the space of protocol states to that of the consensus values: this is the job of the estimator, via the map H given in Definition 3.8. Given a protocol state, the estimator returns a set of consensus values. In the CBC approach, the estimator is left undefined and will be different from one protocol to the next. [4]
Later, Lemma 4 allows us to translate consistency over protocol states back to consistency over consensus values. With these maps doing the back-and-forth for us, Theorem 4 can be restated in terms of consensus values: this is Theorem 5. We have now the safety guarantee for our general class of protocols! Woohoo!
With the concepts in place and the safety proof obtained for this general class of consensus mechanisms, the paper goes on to specify more refined protocols, via definitions of the consensus values, estimators and their associated properties. The general class is large enough to contain distinct flavours of the protocol, given in Section 4. As this post is running long already, we will look at this in part two, available now!
Any mistake? Question? I am still learning and would love your comments!
Many thanks to Aditya, Nate and the CBC team for their introduction to the topic and useful comments, and to Georgios of course for having me at Devcon!
More links!
- Aditya’s simplified exposition of CBC Casper protocols.
- Jon Choi’s Ethereum Casper 101.
- Vlad’s Devcon iv talk (starts around 6:30:00).
- Vlad’s whiteboard talk at RCon.
Footnotes
[1] To some, this may be a feature.
[2] References to definitions and lemmas and theorems are taken from the paper.
[3] I have attempted to draw Casper apparitions in one of the pictures. It was so bad that I prefer to stick to abstract circles and lines for now :)
[4] One example of an estimator is given in Section 4. In a consensus where validators vote on some integer value, each integer can be attributed a score at a state 𝜎: the weight of the validators voting on that integer in state 𝜎. From the score, a simple weighted median gives us a consensus value (or several, if the median is not exact). The estimator thus maps the protocol state to that median via the score.
