cbc-casper/cbc-casper-paper

An Introduction to CBC Casper Consensus Protocols

Introducing the "minimal" CBC Casper Consensus Protocols.

CBC Casper is a family of "correct-by-construction" consensus protocols that share the same proof of asynchronous, Byzantine fault tolerant consensus safety. We describe this family of protocols by defining their protocol states and protocol state transitions, and then we provide a proof of Byzantine fault tolerant consensus safety for the entire Minimal CBC Casper family of protocols. We give examples of members of this family of protocols, including a binary consensus protocol. "Casper the Friendly Ghost", a blockchain consensus protocol, and a sharded blockchain consensus protocol. Each of these examples is "correct-by-construction" because the way they are defined guarantees that they are part of this family of protocols, and therefore satisfy the consensus safety theorem. This draft is intended to be introductory and educational, it is not a complete description of a system that can be implemented exactly as specified.

cbc-casper-paper's Issues

Is the signature of Later_From in def 4.5 correct?

Hi, now I try to do cbc casper formal verification by using Isabelle (see: https://github.com/LayerXcom/cbc-casper-proof).
I noticed that the signature of Later_From in definition 4.5 seems wrong.

Later and From_Sender are defined as follows.

Later: M * P(M) -> P(M)
From_Sender: V * P(M) -> P(M)

So I think Later_From should be defined as:

Later_From: M * V * P(M) -> P(M)

How do you think?

Should be "latest estimate driven"

Needs clarification on what a "single execution of the protocol" means

cbc-casper-paper/cbc-casper-paper-draft.tex

Line 125 in 96a94e5

\item Equivocation fault: producing valid messages in a way that could not have been produced by a \emph{single} execution of the protocol

Right now not sure if this means:

• Every message changes only a single state.
• Messages must not conflict with each other/must be mutually exclusive.
• Something else?

Draft

Lemmas 6 and 9 should be formulated differently.

Maybe I'm misreading them but in their current form they look wrong to me:

Lemma 6 states that every protocol state's messages are totally ordered.
The proof correctly shows that there is a function f : S → ℕ assigning to each message the size of its justification, and that the relation m ≼ n can be defined as f(m) ≥ f(n), but that doesn't imply that ≼ is a total order itself, since f usually won't be injective, and therefore ≼ isn't necessarily antisymmetric.
Maybe the intention of the lemma is to say that (S, ≼) is a total order whenever S is a set of messages that are all from the same, non-equivocating validator?

The proof of Lemma 9 states that due to the "Well-Ordering Principle, a non-empty countable total order always has a minimal element". That's not true (e.g. (ℤ, ≤)), but it's also unneeded: Every finite, partially ordered non-empty set has at least one minimal element, which is sufficient for Lemma 9.

Need to correct to either "a protocol's states" or "a protocol state"

cbc-casper-paper/cbc-casper-paper-draft.tex

Line 342 in 96a94e5

We will define the common futures of a protocol states in terms of the intersection of their ``futures cones":

Line is repeated on page 12, in n party consesus safety proof

`Blocks_In` is not defined

Blocks_In used in definition 4.40 is not defined in this paper.

Page 23, in epoch score, the input e is not used

I think we either need to only use e
OR
specify that b is the block at epoch e

Page 16, Lemma 5 Justification only takes a message, not a protocol state

Remove \sigma from the input to justification

Remove an empty set from a power set

AFAIK, the general meaning of A \ B is a difference between a set A and a set B.

So in the function signature of estimators, I guess P(C) \ {∅} is correct.

Is the signature of the fork choice rule correct? or maybe its usage is incorrect.

The fork choice rule F is used by giving it 2 sets of blocks as input:

but the function signature takes a block and a set of blocks as input:

GHOST estimator should return _children_ of the heaviest subtree.

Definition 4.31 (Casper the Friendly Ghost) gives the estimator as:
ℰ(σ) = GHOST({g}, σ)
which is the set of all blocks occurring in σ that are reachable from the genesis block g by always picking a child with maximum score. In particular, all elements of ℰ(σ) are blocks that are already the estimate of a message in σ, so that estimator wouldn't allow creating new blocks.

Should that definition be changed to instead allow all conceivable children of the elements of GHOST({g}, σ)? Because the next estimate should not be a block that has been proposed before, but a new child.