Who feels the weekend is just too short this days? Well I actually feel this way right now, bit its a new week and its time to work. Please note: This article is written for those who have some familiarity with distributed consensus as it applies to blockchains.
INTRODUCTION TO CORRECT-BY-CONSTRUCTION CASPER The correct-by-construction design philosophy follows these steps:
Lay out an abstract (mathematical) framework for the thing that you want to create;
Prove that all instances of things following that framework have certain desirable properties (i.e. prove it is correct);
Create a concrete thing, matching your use case, within that proven correct framework.
The main advantage of this approach is being certain the outcome has the properties you need. Moreover, working in an abstract setting means that steps 1 and 2 can actually solve many problems at once if they have sufficient similarities. For example, an abstract consensus framework does not necessarily need to reference the specifics of what we are looking for consensus on; thus a single framework could give rise to proven correct protocols for many different blockchain-like systems (regardless of architecture) or indeed anything at all we might want multiple parties to agree on.
Much of the work for the first two steps of the CBC process have already been done for the case of a distributed, asynchronous, trustless consensus algorithm (details have been uploaded to GitHub). This work was done by Vlad Zamfir in collaboration with Vitalik Buterin, Greg Meredith, and others in a research group initiated by the Ethereum Foundation. In short, the abstract framework represents the protocol itself as a category where the objects are the protocol states and the morphisms are the protocol executions, and defines a function called the “estimator” which maps protocol states onto satisfiable logical propositions about the consensus. One of the properties this framework has is “consensus safety.” This means that as long as two protocol states have a common future (i.e. there is a pair of protocol executions which bring the two states to the same state), then any propositions that each state is certain of must not be contradictory. Phrased another way, consensus is always possible.
Vlad and others have also done work to apply their framework to the case where we want consensus on a blockchain (the paper is uploaded to GitHub). A key insight in that work is that if “justifications” are required as part of the protocol, then certain Byzantine Faults (non-protocol behaviors) can be easily detected, thus providing further safety to the protocol. From this, the main achievement of the work is to specify an asynchronous and Byzantine fault tolerant protocol with very low message passing overhead. The paper also makes use of the Greedy Heaviest Observed Sub-Tree (GHOST) fork choice rule (which, yes, is a pun that is 100% on purpose), originally developed by Aviv Zohar and Yonatan Sompolinsky. GHOST tells validators how to decide what branch of the chain to build on, based on the information they have received so far. The details of GHOST itself can be found in Vlad’s paper, but these details are not strictly necessary for the present article. The main idea is that “scores” are calculated for each block at the top of the chain based on some “weights” that are related to the validators. The block with the highest score is the one which is chosen as the parent for new blocks.
RChain’s CBC Casper
The development team for The RChain Cooperative is building on the above foundational work in two important and related ways:
Consensus is happening on a directed acyclic graph of blocks (blockDAG), rather than a blockchain;
Introducing agency of the validators through block acknowledgement and political capital (PC).
The first point simply means that a block may have multiple parents and multiple children. The DAG structure allows for the acknowledgement (as per the second point) of multiple blocks. This in turn serves as a “join” operation and allows independent branches can be merged into a single branch, thus reducing the time to reach consensus.
The second point, validator agency, is the key departure from previous CBC Casper work. The amount of PC a validator spends on a block corresponds to its weight in the GHOST fork choice rule. Therefore, a block with more PC is more likely to remain a part of the main blockDAG. The amount of PC a validator chooses to attach to a block can be thought of as a “bet” on the success of that block. The other aspect of validator agency is the ability to acknowledge blocks. Acknowledgements, unlike new block proposals, are not subject to the GHOST fork choice rule, thus validators have more influence over which branch of the blockDAG continues. Acknowledgements of blocks serve both as a vote of support, and the only mechanism of earning PC. Earning PC exclusively through acknowledgements is important because it means that the only way to contribute to new blocks which have a significant amount of PC attached (and thus will be more likely to remain part of the main DAG) is to participate in the consensus for an extended period of time.
A more detailed description of the protocol can be found on RChain’s wiki.
UNDERSTANDING THE IMPACT OF AGENCY
Once agency is allowed into a protocol, it essentially becomes a game. For a validator on a Proof-of-Stake distributed computing platform such as RChain, the goal of the game is to maximize the fees earned from running smart contracts. Infinitely many strategies exist for this game, not all of which may be good for the network. It is therefore critical to try to ensure that only strategies which embody desired behaviors are successful. To this end, a simulation engine for RChain’s Casper has been written to allow experimenting with different strategies. In the end, bad actors are necessarily identified and discharged from the network, but it is important to systematically disincentivize such behaviour in the first place in order to make the network safer for everyone. The purpose of the simulation is to help us ensure bad behaviour is indeed disadvantageous compared to behaviour which improves the network.
A simulation is only as good as the data it produces. The post-simulation data allows us to draw conclusions about the behaviours the protocol promotes. Quantitative data can put numbers behind statements like some strategy is advantageous, telling us precisely how much better it might be than some other strategy. Visualizations, on the other hand, can provide intuitions and deeper explanations of the quantitative data — both are important. And, as it turns out, RChain’s Casper implementation looks really cool too!
To read a comprehensive version of this document please view the link of original document provided.