Casper CBC: Clique Oracle

A clique of validators for some proposition p can be thought of as a set of validators who pairwise see each other agreeing with p, where there are also no later messages from these validators that are disagreeing with p. A clique can have mulitple layers, although the minimum viable safety oracle will only be 1 − layer deep.

https://gyazo.com/6de95ee79743785b7898654f255e307b

I guess ! s are missing

The definition of $ {\rm agreeing}is wrong?

They should be observed non-equivocating validators

and by the definition of !, clique implicitly means

1. $ {\rm agreeing}implies $ L^H_J(\sigma)(v) is not empty (if $ \neg \ p \ \empty)

2. Then, by the definition,$ L^H_J(\sigma)(v) and $ L^H_M(\sigma)(v)are singleton.

Therefore,$ V are observed non-equivocating validators.

3. Also,$ {\rm agreeing}implies $ L^H_M(L^H_M(\sigma)(v))(v') is not empty (if $ \neg \ p \ \empty)

Because$ v'is not equivocating, this is also singleton

Why "no later disagreeing"?

"Latest message agreeing" is not enough. Latest message in$ \sigmamight be later than the latest message in$ \mathrm{L^H_J(\sigma)(v)}

https://gyazo.com/5169be8bfae11d27967e89eb9562a78b

Threshold

For majority driven property

Clique oracle threshold

(honest agreeing) > (majority) + (potential equivocation)

$ W(V) > W(\mathcal{V})/2 + (t - F(\sigma))

For plausible liveness, the clique must be able to form when non-equivocating validators that have$ tweight go offline

$ W(V) \leq W(\mathcal{V}) - t - F(\sigma)

nrryuya.icon > From this, CBC can tolerate any equivocation faults less than$ tplus$ tomission faults (for both safety and plausible liveness)

From these, for$ W(V)to be exist, we have$ t < W(\mathcal{V})/4

For max driven property

Clique oracle threshold

(honest agreeing) > (honest disagreeing) + (potential equivocation)

$ W(V) > W(\mathcal{V} \setminus V \setminus E(\sigma)) + (t - F(\sigma))

$ \iff 2 * W(V) > W(\mathcal{V}) + t - 2 * F(\sigma)

$ \iff W(V) > W(\mathcal{V})/2 + t/2 - F(\sigma)

For plausible liveness, $ t < W(\mathcal{V})/3

NB. We don't count the votes from equivocating validators but even if we count them, these threshold won't change.

Subjective finality

For "plausible liveness", clique must be able to form in the most difficult case$ F(\sigma) = 0

Comparison

Nakamoto has probabilistic finality where threshold is parameterized by fault tolerance

threshold is the depth of the block in the chain

In PoS blocks older than the checkpoint are final for any fault tolerance (with subjective assumption on time)

Casper TFG has deterministic finality parameterized by fault tolerance and observed equivocation fault weight

also has checkpointing

threshold is the weight of the clique

BA has in-protocol quorum threshold

Once blocks are agreed, they are final for any fault tolerance (with subjective assumption on time)

In TFG, the weight of biggest clique is monotonically grows when looking deeper depth (in a certain view$ \sigma)

But this is not smooth function like the one in Nakamoto PoW

Notes

Q. $ \neg \mathrm{P_{block}}(b) can be finalized?

A. No, because it's not max-driven.

Non-membership property:$ \mathrm{Q_{block}}(b) := \lambda c. ~\exists b' \in C. ~\mathrm{Conflicting}(b, b') \land \mathrm{P_{block}}(b')(c)

Others

The inspector

GitHub barnabemonnot/cbc-finality

ethresear.ch 2018.10 Casper CBC lite via committees