(Partially) Explained Casper CBC specs – Part two: Protocols from the Abstract

From abstract specs to practical protocols

In my previous post, I gave a brief visual interpretation to the latest paper by Vlad Zamfir, Nate Rush, Aditya Asgaonkar and Georgios Piliouras. We saw there that Casper CBC defines an abstract protocol specification, made up of validators sending messages to reach consensus. Once we prove some very nice properties on this general family of protocols, we can define a bit further some components of the mechanisms to obtain specific protocol instances. This is the magic of CBC: Do the hard work on the foundations and reap the profits downstream!

CBC Casper can be refined to yield various specific consensus protocols, starting from its abstract specifications.

The abstract CBC Casper (part one recap)

A group of validators attempts to reach consensus over some object. They can talk to other validators by sending messages. Each time a validator sends a message, it has to give an estimate, i.e. state the value it believes should be the consensus, and justify its message by referring to some previous protocol state. This justification is none other than a set of previous messages, acknowledging “I have seen these messages, and my new message is a continuation of that”. Meanwhile, nodes observe the messages and the protocol state transitions, in an asynchronous fashion: not everyone lives in the same state, but all states are made of messages referencing earlier states.

Two nodes A and B are respectively at states σ1 and σ2. They have a common future if from their current states they can reach a common state σ1 u σ2. The safety property guarantees that if less than t validators equivocate, there is such a common future where decided properties are consistent and still less than t validators equivocate. Every other state in the intersection of the futures cone σ’ or σ’’ is a superset of σ1 u σ2.

Forming consensus

We stand on solid ground with the protocol specs and its safety guarantee, it is time to make good use of it all. The protocol is developed to reach consensus and this is what we turn our attention to now.

Latest messages

When validators send messages, they are actively vouching for some value to be decided as consensus. Dishonest validators can try to derail the protocol by vouching for two different values, or justifying the same value from two different states that do not include either messages. This entails that validators that do not equivocate will always have at most one latest message – they can have none if they have never spoken, or if their messages are not observed in a particular state. If they are observed in the state however, there is only one such latest message. The consensus is argued over this set of honest observed validators’ messages.

We have three validators, A, B and C. 1) A and C send a message (states σ1 and σ2). 2) B equivocates, sends two messages m and m’. 3) At state σ4, we have one latest message from A (observed honest validator), two latest messages from B (observed equivocating validator) and zero message from C (unobserved honest validator).

Messages as input to the estimator

After we collect the latest messages of observed honest validators, we can move from the protocol state to the consensus values. Definition 4.13 gives us a function mapping validators to their own estimate, or to the empty set if the validator is not observed or if it is equivocating. The estimate is the consensus value they have included in their latest message.

Minimal Casper consensus protocols

What do we have left to do? We proved that nodes cannot decide on contradictory consensus values unless the weight of equivocating validators is too high. We saw that validators who play nice and are included at some state of the protocol have sent only one latest message each. Finally, we mapped these latest messages to the consensus value they are estimating.

The friendly binary consensus

The simplest of the family of minimal CBC Casper protocols, the binary consensus, asks of validators to choose between two values, say, 0 and 1. The consensus value is obtained very naturally: validator weights are tallied up for those who estimated value 0 vs. those who estimated value 1, and the heaviest set wins. Note that in case of a tie, both values are returned: remember that the estimator returns a subset of the set of consensus values, and this subset can have multiple elements.

4 validators estimate the consensus value. 2 are out of the final decision: B has equivocated and C has not been observed. D estimates 0 but its weight of 2 is inferior to that of A, who estimated 1. Thus, the consensus yields 1.

The friendly integer consensus

The logical next step is to reach consensus over a set that contains more than 2 elements. In this version, validators estimate the value of an integer. We could again take the value returned by the heaviest set of validators, as we did for the binary consensus protocol. However, this might not best represent the idea of consensus, as the mode of a distribution (its highest peak) can be very different from its mean or its median.

The first array gives the estimates of six observed honest validators, with the validators’ weights. The second array gives the total score for each of the estimated integers. In the chart, we show in pink the cumulative score distribution, with the dashed line representing the median line, where half of the validators’ weight is. Since 2 is the only integer such that the total score of smaller integers is less than 7 (= 6, blue arrow) and the total score of larger integers is also less than 7 (= 4, second blue arrow), we get that 2 is the weighted median, and thus the consensus value. You could check as an exercise that 1 is not the weighted median. Can you find an example where the weighted median returns a set of multiple integers?

The friendly GHOST

Seemingly, we have strayed rather far from the blockchain issues that motivated all this in the first place. Rest assured, however, that with all this power in our hands, we can very quickly adapt Casper to fit in a more blockchain-oriented framework. Its first application is to the fork choice rule nicknamed GHOST, for Greedy Heaviest Observed Sub-Tree (can you see the connection with Casper? 👻)

Coming next

The paper goes on to provide another flavour of Casper: the Finality Gadget. If you have already heard of it before, it is because it is actively discussed and researched on at the moment by the Ethereum community. It started as a consensus gadget on top of PoW, but was recently redesigned to allow for full PoS on top of sharding. It is a super interesting topic, and a very recent paper by Vitalik Buterin, Daniël Reijsbergen and Georgios Piliouras makes the case for the cryptoeconomics of deposits and rewards in the finality gadget.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store