Formal methods on another Casper

In a previous post, I talked about proving properties of Vitalik’s Casper. This post is about Vlad’s Casper. They are very different. The two Caspers are not just two different protocols, but two opposite approaches to protocol designs.

Vitalik’s Casper looks implementable. It is a direct construction that solves a simple problem first and puts on more and more sophistication to match the real requirements.

Vlad’s Casper is more like an effort to find fundamental difficulties. It leaves not-so-fundamental problems open and focuses on the essence. The hardest core of the problem comes from asynchrony, where messages can be delayed and reshuffled. This is equivalent to nodes being slowed down at arbitrary rates. That, in turn, is equivalent to having an attacker making as many moves as it wants, at any moment. The core of the problem is how to establish secure knowledge about the future, just by looking at the subjective past.

Vlad’s Casper at the current form does not specify the way of communication between validators. Is it round-based? No, but even a round-based protocol can be analyzed as one instantiation of Vlad’s Casper. Does it have liveness assumptions? No, but arbitrary assumptions on the message delays or validator liveness can be added to Vlad’s Casper. It is a stem cell of many protocols. It is also a gauge that can measure many different-looking algorithms.

I guess it’s just 5% of Vlad’s Casper, but somehow Vlad and I proved some portion of his Casper in Isabelle/HOL. The code is available on GitHub.

Toward the end of this first part, the most important notion is estimate-safety: “an estimate is safe based on a view.” The special thing about it is, any participant can locally judge if an estimate is safe just by looking at their view of the past, and the safety would tell them the estimate is never going to change. That’s the solution to the hardest problem of establishing a secure knowledge about the future just by looking at the subjective past. Vlad’s Casper goes further and describes an algorithm that guarantees the estimate-safety, but we have not formalized this algorithm in Isabelle/HOL.

At one point one needs to stop talking and start typing code. This is the same as in software development. The first lines are typically boring. That’s why it’s important to look ahead and talk freely, sometimes. After knowing what we want, sometimes we can endure the boring parts.

Validators. What are validators? We don’t know much. We just say there are as many validators as there are integers. Integers in Isabelle/HOL are infinitely many.

datatype validator = Validator int

After we say this, Isabelle/HOL allows us to compare two validators and see if they are equal or not. It does not allow us to “add” or “multiply” validators. It does not allow us to ask if a validator is larger than another validator. It does not allow us to compare a validator against an integer. That’s a comfortable situation. We are protected from many mistakes.

Validators have weights. We just talk about functions that assign weights to validators.

type_synonym weight = “validator ⇒ int”

After we say this, whenever Isabelle/HOL sees weight, it does not see weightbut sees validator => int, which is the type of (usual total) functions that take validators and return integers. The function just returns one integer on every validator.

Of course, we can specify properties on the weight functions.

definition tie_breaking :: “validator set ⇒ weight ⇒ bool”
where
“tie_breaking V w =
 ( ∀ S0 S1.
 S0 ⊆ V ⟶
 S1 ⊆ V ⟶
 S0 ≠ S1 ⟶
 sum w S0 ≠ sum w S1 )”

After typing these lines, Isabelle/HOL knows tie_breakingmeans something. It does not automatically replace occurrences of tie_breakingwith the lengthier definition, but it’s aware that tie_breakingis defined. Some plugins even look at the content of the definitions to figure out how to (dis)prove stuff.

The weight function w is tie_breaking on the validator set V if and only if, for arbitrary different subsets S0 and S1 of V, the sum of W over S0 is not equal to the sum of w over S1.

The initial part of the formalization is boring but also dangerous. A mistake here might cost thousands of lines later. Maybe we should perform an experiment. Let’s say there are two validators of weight one; then the tie-breaking property should not hold. We prepare a uniform weight function that assigns 1 to every validator.

definition uniform_weight :: “validator ⇒ int” 
where
“uniform_weight v = 1”

On this uniform weight function should be tie-breaking on two validators.

lemma should_be_false: “¬ tie_breaking {Validator 0, Validator 1} uniform_weight“

When a user types in this statement, Isabelle/HOL tries to find a counter-example for a second or two (if you want a longer check, type nitpick). At the same time Isabelle/HOL echoes back the statement, as the goal to be proven.

proof (prove)
goal (1 subgoal):
 1. ¬ tie_breaking {Validator 0, Validator 1} uniform_weight

Now it’s up to the user how to prove this. I said, “use the definition of tie_breaking and crunch down the goal.”

apply(simp add: tie_breaking_def)

Isabelle/HOL replies immediately with the result.

proof (prove)
goal (1 subgoal):
 1. ∃S0⊆{Validator 0, Validator 1}. ∃S1⊆{Validator 0, Validator 1}. S0 ≠ S1 ∧ sum uniform_weight S0 = sum uniform_weight S1

The crunched-down statement reads like; there exist two different subsets of {Validator 0, Validator 1} over which the sum of uniform_weight is the same.

Again it’s my turn what to do. I have to pick S0 and S1 that witness the tie-breaking property. When I actually do that (I’m not showing the commands anymore), Isabelle/HOL acknowledges the theorem.

theorem should_be_false:
¬ tie_breaking {Validator 0, Validator 1} uniform_weight

I have another conjecture: any weight function should be tie_breaking on an infinite set of validators. In Isabelle/HOL, sum over an infinite set is defined to be zero. I haven’t checked this conjecture, but moved on to bets and views.

In Vlad’s Casper, validators sign bets. A bet contains an estimate. Intuitively the estimate is on the outcome of the consensus, but we don’t rely on this intuition. Our problem is to set up some criteria on a validator’s behavior, and ultimately to build a game that rewards and punishes validators. The validators might be purely implemented as a computer program or as a swarm of bees. So it does not make much sense to ask the validators’ intensions. The whole game must be defined using only the observable behavior.

Who observes the validator’s behavior? I don’t know. We don’t need to know this right now. Whoever observes the validators’ bets, an observation would contain a set of bets signed by validators.

Eventually, we will want to form a consensus on a history. The desired history might be linear or not. Depending on the contents of the history, some events might be compatible with other events. That sort of combinatorics causes its own headaches. So, the problem is a binary choice right now: choosing one of two values. This is another act of delaying a smaller problem and focusing on the essence.

Isabelle/HOL has a datatype with two values: a boolean. Using this, we define a datatype called estimate.

datatype estimate = Estimate bool

After I type this, Estimate True and Estimate False are two different estimates. There are no other estimates.

A bet is inductively defined as a triple of a validator (signer), an estimate and a set of bets (justifications). I said “inductively defined as” because otherwise the sentence didn’t form a definition. Can a bet’s justification’s justification contain the first bet in question? Can one start with one bet and find a justification, and a justification of that, and so on infinitely? The answer to both questions is “no”, as we will prove later, but that’s just because I said “inductively”.

In Isabelle/HOL, every datatype definition is taken as an inductive definition. I don’t have to say “inductive” there.

datatype bet =
 Bet “estimate * validator * bet list”

Something tricky happens here. I don’t know how Isabelle/HOL handles this. Somehow Isabelle/HOL proves a theorem in the background (this statement looks particularly ugly, but don’t be scared. Isabelle/HOL is usually very nice-looking on the UI):

BetsAndValidators.bet.induct:
 (⋀xa. (⋀xaa xaaa xaaaa. xaa ∈ Basic_BNFs.snds xa ⟹ xaaa ∈ Basic_BNFs.snds xaa ⟹ xaaaa ∈ set xaaa ⟹ ?P xaaaa) ⟹
 ?P (Bet xa)) ⟹
 ?P ?bet

This allows one to prove things about all bets by mathematical induction.

The sender of a bet is the validator contained in the bet:

fun sender :: “bet ⇒ validator”
where
“sender (Bet (_, v, _)) = v”

The estimate of a bet is the estimate contained in the bet:

fun est :: “bet ⇒ estimate”
where
“est (Bet (e, _, _)) = e”

A bet justifies a bet if the former is one of the justifications of the latter:

fun justifies :: “bet ⇒ (bet ⇒ bool)”
where
“justifies b (Bet (e, v, js)) = (b ∈ set js)”

A bet depends on a bet when there is a sequence of justification from the latter to former. “justifies” is a binary relation on bets, and “is_dependency” is a transitive closure of that.

A transitive closure can be defined as:

inductive tran :: “(bet ⇒ bet ⇒ bool) ⇒ (bet ⇒ bet ⇒ bool)”
where
  tran_simple: “R x y ⟹ tran R x y”
| tran_composit: “tran R x y ⟹ R y z ⟹ tran R x z”

“tran R” is the smallest binary relation on bets such that “tran R x y” holds in two cases,
1) simply “R x y” holds, and when
2) “tran R x y” and “R y z” hold.

I have to say “the smallest” because the above two conditions are not specific enough to identify a single binary relation “tran R”. For instance, the conditions hold even if “tran R” connects every two bets. (Does this “smallest” thing exist? Good question! https://softech.informatik.uni-kl.de/homepage/teaching/SVHOL12/slides6a.pdf)

After doing this, we can just say “is_dependency” is the transitive closure of “justifies”.

definition is_dependency :: “bet ⇒ bet ⇒ bool”
where
“is_dependency = tran justifies”

In the definition of transitive closure, I said “tran R x y” and “R y z”. I could have added the third case “R x y” and “tran R y z”, but that shouldn’t have changed the transitive closure.

lemma is_dependency_tail_first :
 “tran R y z ⟹ R x y ⟹ tran R x z”

The proof is induction on the transitive closure.

I said the definition of bets is inductive. So I can prove that two bets are not mutually in dependency. There are no cycles of justifications. There are no vicious cycles, so to speak.

lemma dependency_no_cycle :
 “∀ a. is_dependency a b ⟶ ¬ is_dependency b a”

The proof is induction on b. The proof is interesting because the induction does not decrease the size of the cycle.

There is a less exciting fact that “is_dependency” is indeed transitive.

lemma dependency_is_transitive :
 “is_dependency y z ⟹
  ∀ x. is_dependency x y ⟶ is_dependency x z”

The proof is induction over transitive closure.

After so much bureaucracy, here is a meaningful concept. A validator equivocates when it signs two different bets, none of which is dependent on the other. This is the Casper equivalent of double-spending. Equivocation means not keeping one’s own linear history.

definition equivocation :: “bet ⇒ bet ⇒ bool”
where
“equivocation b0 b1 =
 (sender b0 = sender b1 ∧ ¬ is_dependency b0 b1
 ∧ ¬ is_dependency b1 b0 ∧ b0 ≠ b1 )”

This says, two bets b0 and b1 form an equivocation when they are from the same sender, neither depends on the other and
are different.

A view is a set of bets that does not contain equivocation.

definition is_view :: “bet set ⇒ bool”
where
“is_view bs = (∀ b0 b1. b0 ∈ bs ⟶ b1 ∈ bs ⟶ ¬ equivocation b0 b1)”

A set of bets is a view if and only if no two bets in the set form an equivocation.

We are usually interested in the latest bets from a validator.

definition latest_bets :: “bet set ⇒ validator ⇒ bet set”
where
“ latest_bets bs v =
   { l . l ∈ bs ∧ sender l = v 
      ∧ (¬ (∃ b’. b’ ∈ bs ∧ sender b’ = v ∧ is_dependency l b’))}“

I’m very sorry that v (an alphabet) and ∨ (the symbol for disjunction) look very similar. In the definition above, there is only the alphabet vee, not the disjunction symbol. The latest bets in a set bs of bets from a validator v consist of those bets in bs whose sender is v, which is not dependency of any bet in bs from v.

Regardless of validators, we can also talk about the latest bets in a set of bets.

definition is_latest_in :: “bet ⇒ bet set ⇒ bool”
where
“is_latest_in b bs =
  (b ∈ bs ∧ (¬ (∃ b’. b’ ∈ bs ∧ is_dependency b b’)))”

A bet is latest in a set of bets when the bet is an element of the set and the bet is not dependency of any bet in the set.

A set is non-empty when it has an element:

definition is_non_empty :: “‘a set ⇒ bool”
where
“is_non_empty bs = ( ∃b. b∈bs )”

When a set of bets is finite and non-empty, it has latest bets:

lemma latest_existence’ :
 “finite bs ⟹ is_non_empty bs ⟶ (∃ l. is_latest_in l bs)”

This depends on the fact that the chain of justifications does not form a cycle. The finiteness is necessary because otherwise there all bets might belong in an infinite chain of justification.

An interesting thing about the latest bets from a validator is, there can be only one unless the validator has equivocated. When there are two different latest bets from the same validator, they form an equivocation.

lemma two_latests_are_equivocation :
 “b0 ∈ latest_bets bs v ⟹ b1 ∈ latest_bets bs v ⟹ b0 ≠ b1 ⟹ equivocation b0 b1”

A set has at most one element when any two elements are equal:

definition at_most_one :: “‘a set ⇒ bool”
where
“at_most_one s = (∀ x y. x ∈ s ⟶ y ∈ s ⟶ x = y)”

Since a view does not contain equivocation, a view can contain at most one latest bet from a validator:

lemma view_has_at_most_one_latest_bet :
 “is_view bs ⟹ at_most_one (latest_bets bs v)”

Sometimes we are interested in validators who have signed bets in a set of bets:

definition observed_validators :: “bet set ⇒ validator set” 
where 
 “observed_validators bs =
({v :: validator. ∃b. b ∈ bs ∧ v = sender b })”

The observed validators in a set of bets consist of those validators who have signed some bets in the set. Note that this does not consider the justifications that are out of the set.

So, in a non-empty set of bets, we can find some validators.

lemma observed_validators_exist_in_non_empty_bet_set :
 “is_non_empty bs ⟹ is_non_empty (observed_validators bs)”

Maybe more interestingly, if the set of bets is not empty, an observed validator always has a latest bet.

lemma observed_validator_has_latest_bet :
 “finite bs ⟶ v ∈ (observed_validators bs) ⟶ is_non_empty (latest_bets bs v)”

Combining the above two, we know existence of a validator who has at least on latest bet, always on a finite non-empty set of bets.

lemma latest_bets_exist_in_non_empty_bet_set :
 “finite bs ⟹
 is_non_empty bs ⟹
 ∃v::validator.(is_non_empty (latest_bets bs v))”

We are interested in which validators are currently supporting which estimate. A validator has a latest bet on an estimate when it has a latest bet that contains the estimate.

definition has_a_latest_bet_on ::
 “bet set ⇒ validator ⇒ estimate ⇒ bool”
where
“has_a_latest_bet_on bs v e =
 (∃ b. b ∈ latest_bets bs v ∧ est b = e)”

In a view, a validator cannot have a latest bet on different estimates:

lemma validator_in_view_contributes_to_at_most_one_estimates_weight :
 “is_view bs ⟹
 ∀v. v∈(observed_validators bs) ⟶ at_most_one {e. (has_a_latest_bet_on bs v e)}”

The latest bets are combined with the weight function to give a weight on an estimate in a set of bets. The weight is the sum of the weights of validators that have latest bets on the estimate.

definition weight_of_estimate ::
 “bet set ⇒ weight ⇒ estimate ⇒ int”
where
“weight_of_estimate bs w e =
 sum w { v. has_a_latest_bet_on bs v e }”

Now we can talk about which estimate is leading the race. An estimate is a max-weight-estimate when its weight is at least as large as other estimates’ weights.

definition is_max_weight_estimate ::
 “bet set ⇒ weight ⇒ estimate ⇒ bool”
where
“is_max_weight_estimate bs w e =
 (∀ e’.
 weight_of_estimate bs w e ≥ weight_of_estimate bs w e’)”

Can there be more than one max-weight-estimates? No, under certain conditions: on a finite, non-empty view, with a positive, tie-breaking weight function.

lemma view_has_at_most_one_max_weight_estimate :
 “is_view bs ⟹
 finite bs ⟹
 is_non_empty bs ⟹
 positive_weights (observed_validators bs) w ⟹
 tie_breaking (observed_validators bs) w ⟹
 at_most_one {e. is_max_weight_estimate bs w e}”

With the notion of max-weight-estimate, now we are ready to describe the honest behavior. A validator should not equivocate. A validator should only produce valid bets.

When a validator has justifications, since the justifications are bets, there are max-weight-estimates. A valid bet is on a max-weight-estimate of the justifications.

fun is_valid :: “weight ⇒ bet ⇒ bool”
where
“is_valid w (Bet (e, v, js))
  = is_max_weight_estimate (set js) w e”

A valid view is a view that contains only valid bets:

definition is_valid_view :: “weight ⇒ bet set ⇒ bool”
where
“is_valid_view w bs = (is_view bs ∧ (∀ b ∈ bs. is_valid w b))”

In a valid view, every bet is honestly created. No validators equivocate. All bets with justifications follow the max_weight rule. Here we are not dealing with Byzantine faults (when validators do whatever, slightly dishonest or completely random). Maybe, provably dishonest bets are dropped from a view.

So far all arguments have been on one static set of bets. Now we talk about two views, one being a possible future of the other.

definition is_future_view :: “weight ⇒ bet set ⇒ bet set ⇒ bool”
where
“is_future_view w b0 b1 =
 (b0 ⊇ b1 ∧ is_valid_view w b0 ∧ is_valid_view w b1)”

The definition of the future views requires the views to be valid views.

Our goal was to ensure knowledge about the future based on an observation of the past. One form of desirable knowledge is estimate-safety. An estimate is safe when it is the max weight estimate on all future views:

definition is_estimate_safe ::
   “weight ⇒ bet set ⇒ estimate ⇒ bool”
where
“is_estimate_safe w bs e =
 (∀ bf. is_future_view w bf bs ⟶ is_max_weight_estimate bf w e)”

When a participant gets a safe estimate, and another participant obtains a safe estimate, it’s desirable they are equal. If that’s the case, whoever reaches a safe estimate will share the same estimate.

Two views are consistent when the union of them is a valid view.

definition consistent_views :: “weight ⇒ bet set ⇒ bet set ⇒ bool”
where
“consistent_views w b0 b1 =
 (is_valid_view w b0 ∧ is_valid_view w b1
 ∧ is_valid_view w (b0 ∪ b1))”

We were able to prove a nice property about estimate safety. When an estimate is safe on a view, and another estimate is safe on another view, the two estimates always coincide.

lemma consensus_safety :
 “finite b0 ⟹
 finite b1 ⟹
 is_non_empty b1 ⟹
 positive_weights (observed_validators b0) w ⟹
 positive_weights (observed_validators b1) w ⟹
 tie_breaking (observed_validators (b0 ∪ b1)) w ⟹
 is_estimate_safe w b0 e0 ⟹
 is_estimate_safe w b1 e1 ⟹
 consistent_views w b0 b1 ⟹
 e0 = e1”

Essentially, when you have a safe estimate, you needn’t worry that your knowledge of the world might be imperfect. You don’t need to learn more. All other parties that learn well enough will reach the same estimate as yours. It’s time to shout (or quietly receive conviction), this estimate is going to be the consensus.

It remains to see how to judge if an estimate is safe in a view. Vlad has this part on paper. He also has an implementation. The proof of the algorithm is not machine-checked yet.