# A tight and intuitive Casper slashing condition

#1

TLDR: We present a single simplified Casper slashing condition to replace the two slashing conditions in the Casper FFG paper. The new slashing condition cannot be weakened, i.e. it is tight. It is also intuitive and makes the safety proof (even more) obvious.

Context

A year ago @vbuterin simplified the Casper slashing conditions, reducing the count from 4 to 2. Three months ago @dlubarov noticed the slashing conditions were not tight, i.e. that they could be weakened. Specifically, it was noticed that the second â€śno-surroundâ€ť slashing condition can be specialised to finalisation votes, i.e. votes from a checkpoint to a direct child. It turns out the first â€śno-equivocationâ€ť slashing condition can also be weakened. By weakening both slashing conditions, a unifiedâ€”and more naturalâ€”slashing condition emerges.

Construction

Notation: Below s and \tilde{s} are sources, t and \tilde{t} are targets, and h() is the height function.

Slashing condition: A validator must not cast a vote (s, t) that â€śhops overâ€ť one of his finalisation votes (\tilde{s}, \tilde{t}), i.e. h(s)\le h(\tilde{s}) and h(t)\ge h(\tilde{t}).

Visualisation: It is natural to visualise votes as edges from source to target placed on a line according to their height. In that context a finalisation vote is a short edge of length 1, and vote hopping corresponds to edge hopping.

Safety proof: Suppose two conflicting checkpoints finalise and consider their justification paths, each ending with a finalisation edge. One of the paths is no shorter (in height) than the other. Clearly, that path contains an edge that hops over the finalisation edge of the other path. This implies at least 1/3 of the validators cast a vote to hop over a finalisation vote.

Tightness: The slashing condition is tight. Indeed, suppose it was possible to hop over one of your finalisation votes without getting slashed. If all validators vote, all vote the same way, and make a conflicting hop over one of their finalisation votes, then they can extend the conflicting hopping edge with a finalisation edge, thereby yielding two conflicting finalised checkpoints.

Should we simplify Casper votes to remove the "source" param?
Should we simplify Casper votes to remove the "source" param?
#2

Hm, the safety proof makes sense (and itâ€™s nice and intuitive now), but I think we still need Commandment I to ensure liveness. Consider this checkpoint structure â€“

  ,-b--c--d
/
a
\
-e--f--g


If we allow multiple (non-finalization) votes at the same height, a->c and a->f could both get a supermajority. Then if thereâ€™s a 50/50 split vote between c->d and f->g, half of voters would be â€śstuckâ€ť on the top fork and half on the bottom fork. Right?

Itâ€™s interesting to compare Casper FFG to Tendermint. If you took Tendermintâ€™s rules, converted it to an overlay system, and changed some terminology, I think youâ€™d end up with the â€śtweakedâ€ť Casper rules in my post. A Casper justification vote is like a Tendermint prevote, and a Casper finalization vote is like a Tendermint precommit. In either system, voters become â€ślockedâ€ť when they cast a finalization vote, and they unlock after observing some block become justified in a later round. (With Casper, you could vote with an unjustified source while locked, but it wouldnâ€™t have any effect.)

#3

What @dlubarov said, and also, technically I donâ€™t think your unified condition is tight, because it doesnâ€™t say anything about the targets conflicting. That is, referring to Danielâ€™s diagram, if I cast a finalization vote b->c, and then a non-finalization vote a->d`, the latter â€śhops overâ€ť the former and thus I could be slashed, even though the targets didnâ€™t conflict.

Easy to fix - just add in the requirement that the validator only gets slashed if the two votesâ€™ targets conflict.