A mechanized safety proof for PoS with dynamic validators

I used a theorem prover Isabelle/HOL to check Vitalik’s post about a proof-of-stake protocol that uses dynamic validator sets. (If you haven’t seen, I did something similar for the simpler proof-of-stake protocol where the validator set is constant.) The proof script is available online.

Once this was not a faithful formalization. Vitalik pointed out my formalization of slashing condition 1. only talked about the rear validators. And I realized, I didn’t use slashing conditions one or two. This wasbecause the way I defined forks (I was looking at prepare — prepare_src relation already). This has been fixed in the current online versions.

One important property of the protocol is called accountable safety. The word accountable appears here because some validators are held accountable if forking blocks are finalized. By the time forking blocks are finalized, the protocol (Casper) would have forfeited deposits of certain validators. The rules are meant to make the validators careful about what they sign.

Last time, the set of validators was constant. If forking blocks got finalized, at least 1/3 of the validators were slashed, said accountable safety. This time, accountable safety means something else. The dynamic validator change forces us to change the properties that we seek.

What are forking blocks? Last time, any two hashes were in conflict when neither is a descendant of the other. We cannot use this definition anymore. Think about two unrelated chains of blocks that are completely fine. These chains do not share any blocks. Nor do they share any of the validators involved. If we use the original definition of conflicting blocks, any block on one chain is in conflict with all blocks on the other chain, and accountable safety would demand some validators be slashed. That sounds unfair. We were fine last time because all blocks shared the same set of validators. If they supported two separate chains, they should be blamed. This time, the conflicting blocks need to share the same ancestor.

Who should be slashed? Yes, 2/3 of the validators, but which validators? Now we have dynamically changing validator sets. So we need a point of reference. We have one. In the previous paragraph, I chose to require a common ancestor of the forking blocks. The common ancestor has a set of validators, they choose some validators, and their heirs choose some further descendant sets. I request that one of the descendant sets have 2/3 of its members slashed.

Is this artificial complication that the validator sets need to be the heirs of the original validator set? I don’t think so. To me, it sounds natural that validators are validators because previous validators chose them. It’s a common account that names and references get resolved by the history.

That’s what I had to choose about accountable safety. The statement of accountable safety looks like this:

lemma accountable_safety :
"validator_sets_finite s ⟹
fork_with_commits s (h, v) (h1, v1) (h2, v2) ⟹
∃ h' v'.
heir s (h, v) (h', v') ∧
one_third_of_fwd_slashed s h' "

The first line validator_sets_finite s is an assumption that all hashes have a finite forward validator set and a finite rear validator set. The second line fork_with_commits s (h, v) (h1, v1) (h2, v2) is another assumption that the hash h is committed at view v, h1 at v1 and h2 at v2. Moreover, there is a chain from (h, v) to (h1, v1) and another from (h, v) to (h2, v2), but no chains from (h1, v1) to (h2, v2) or the other way around. With these assumptions, one can find a hash h’ and a view v’ in a chain starting from (h, v), and at least one-third of the forward validator set of h' is slashed.

The proof was somewhat easier than the last time because I had a common root of the two conflicting blocks. Given a fork, I was able to choose the highest commit from which two branches extend. I was also able to cut down the branches until each of them contains at most one validator set change. This small fork has a single, responsible validator set. Using the familiar argument, I was able to see 2/3 of them slashed.

Now, maybe go to the PDF generated by Isabelle/HOL. I’ve put together the skippable definitions and lemmata under “skippable” section. Whenever you are stuck, ask a question in the formal methods Gitter channel.

What does not appear in the final document is what it could have been. Here I document the subtlest choice I made during the mechanization of the proof. More blatantly, I had to change something when the proof stuck.

Initially, in the statement of accountable safety, I assumed that h1 and h2 are not in ancestor-descendant relation. The minute proof details forced me to prove a stronger theorem with an weaker assumption that (h1, v1) and (h2, v2) are not on the same chain (that follows prepare and prepare sources). Without this strengthening, I was not able to cut down branches of the fork. There was a chance that the shorter branches do not form a fork because the new tips are in ancestor-descendant relation while they are no on the same chain. Anyway, I was just forced to prove a better theorem. When you have a fork with tips not in ancestor-descendant relation, they are not on the same chain for sure.

Another subtlety is when blocks are prepared and committed. Currently in the formalization, 2/3 of forward validators and 2/3 of rear validators are always required. I haven’t tried changing this. I haven’t tried to prove plausible liveness either.

Anyway it has been two weeks since the original post came about, so it’s about time the arguments are mechanized somehow. I think I was able to check that the trick works. Having forward and rear validator sets, one can blame a validator set in any fork.