Handling Equivocations in Casper

The following is a result of a discussion with Michael Birch.

Definition "Irrelevance of equivocations"

Let E1, E2 be two blocks by the same creator C that have the same justification, and thus is an example of an equivocation. Let V be a view that already includes E1 and has a tip (a block at the tip of the forkchoice) T. Adding E2 to the view V should not change the tip T. Note that including a block that has E2 as a parent may change the tip T without breaking this property.

--

Definition "Irrelevance of slashing"

For all blocks B in the blockchain of T, where T is a block that contains a slashing transaction, removing that slashing transaction from T does not change whether B is in the forkchoice.

--

THM "Double counting fails"

Any protocol that double counts the weights of a equivocation will break the irrelevance of equivocations property.

Informal Proof of "Double counting fails"

Assume there is a blockchain with tip T as follows:

A <- B1 <- Long chain follows <- T
A <- B2 <- B3

such that score(B1) > score(B2). If there is a equivocation

B2 <- B3
B2 <- B4
...
B2 <- B999

then eventually score(B2) > score(B1). B2 will then be in the blockchain of the tip.

--

THM "Dropping all equivocations fail"

Any protocol that always removes all blocks by the same creator that have the same justification and their children will break the irrelevance of equivocations property.

Informal Proof of "Double counting fails"

Assume there is a blockchain with tip T as follows:

A <- B1 <- T
A <- B2

Removing both B1 and B2 and their children will remove the tip T.

--

Proposed protocol

Let E1, E2 be two blocks by the same creator C that have the same justification, and thus is an example of an equivocation. Let V be a view that already includes E1 and has a tip (a block at the tip of the forkchoice) T. When view V receives E2, ignore E2. If V receives a block from another validator that includes E2 in its blockchain, add E2 into the view and set the latest message from C to be E2. Then run inclusive ghost as normal.

Note that now anything in the blockchain of E1 has their score potentially lowered by the weight of C. If E1 is in the blockchain of the tip T, this may imply that T will no longer be the tip. But that is ok because if C has such a large weight, then tip T should never have been close to being finalized in the first place. Also note this doesn't break the "irrelevance of equivocations" property because it is the children of E2 that is changing the tip T not E2 itself.

Proposed slashing protocol

Slashes that prove that a validator equivocate should result in the validators weight in the current weight map to be turned to 0. Since since parent blocks are used for scoring, this doesn't break the "irrelevance of slashing" property as only scores of the children blocks after the slash are affected.

--

Define "justification regression"

Let B1 and B2 be two blocks created by B such that the creator justification of B2 is B1. Let A be an arbitrary validator and let B1, B2 's justification (latest message) for A be A1, A2 respectively. A1 is not in the justification chain of A2.

--

Slashing protocol

If you create a block with a justification regression, you must slash the validator(s) that forced you to create the justification regression or you are eligible to be slashed.