In this exploration, we investigate how the safety proofs for the minimal CBC Casper family is formally verified in the proof assistant Coq. In an attempt to make this readable for non-Coq practitioners, sufficient explanation on the proof strategies have been expanded to make this a fulfilling read. As the reader will realise, one of the core characteristic of proving in Coq is the constructivism nature of its language - a proof is exhibited by constructing an algorithm. Without further ado, let’s get proving!

Two protocol states who do not cross the threshold can have a common future

Theorem 1. \(\forall \sigma_1, \sigma_2 \in \Sigma_t\),

\[F(\sigma_1 \cup \sigma_2) \leq t \implies Futures_t(\sigma_1) \cap Futures_t(\sigma_2) \neq \emptyset\] 
(* Theorem 1 *)
Theorem pair_common_futures '{CBC_protocol_eq}:
  forall s1 s2 : pstate, (equivocation_weight (state_union s1 s2) <= proj1_sig t)%R ->
    exists s : pstate, pstate_rel s1 s /\ pstate_rel s2 s.

In the statement of the theorems here, the parameter declarations '{CBC_protocol_eq} within the statement of a theorem is a class constraint, which means the theorems is applicable to data types which have been rigorously established to fulfil the requirements of the CBC_protocol_eq class. The pstate type refers to states that satisfy the properties of a protocol state, where the properties are stored in the parameter prot_state of CBC_protocol_eq. The pstate_rel refers to the reachability relation parameter reach within CBC_protocol_eq. Observe that the pair_common_futures theorem (algorithm) constructs a protocol state from s1 and s2 with proofs of reachability from s1 and s2.

Note: The repeated expression (equivocation_weight (state_union s1 s2) <= proj1_sig t)%R means that the equivocation weight of the expression applied to equivocation_weight is less than or equal to the value t. The clunky expression proj1_sig t is used to project out the numerical value within t to evaluate the inequality expression of real numbers, hence the bounded by (...)%R environment.

Proof.
  (* extract the data from the protocol states to be used for the proof *)
  intros s1 s2 H_weight. remember s1 as ps1. remember s2 as ps2.
  destruct s1 as [s1 H_s1]. destruct s2 as [s2 H_s2].
  rewrite Heqps1, Heqps2 in H_weight; simpl in H_weight.
  (* proposing the union of s1 and s2 as a common future  *)
  exists (exist _ (state_union s1 s2) (about_prot_state s1 s2 H_s1 H_s2 H_weight)).
  subst. unfold pstate_rel. simpl.
  (* shows that the union of s1 and s2 is reachable from both s1 and s2 *)
  split. apply reach_union.
  apply (reach_morphism s2 (state_union s2 s1) (state_union s1 s2)).
  apply reach_union.
  apply state_union_comm.
  Qed.
  • As we will observe in subsequent proofs, the preliminary step is to extract out the data of the pstate as the proofs that come along with the terms of pstate is not necessary for computations such as state_union and reach_morphism.

Note: Such a repetitive preliminary steps incurs lots of overhead for the human prover mechanising the proof and is a common occurrence in the formalisation of proofs. One way of overcoming this issue is through the use of coercion, where the Coq engine helps insert a function to change the type of a term in another to prevent a type error, which in our case is pstate to state. While the coercion command for this has actually been implemented, it is unclear why the authors did not make use of this functionality in their proofs.

  • The proof approach is to show existence of a common future for two arbitrary protocol states, where the equivocation weight of their union still falls within the threshold. This is exhibited by showing that the union of the two protocol states

  • Using the helper lemmas, it can be easily shown that the union of two protocol states can be reached by the protocol states themselves.

It is not surprising that Theorem 1 can be generalised.

Protocol states who do not cross the threshold can have a common future

Theorem 2. \(\forall \sigma_i \in \Sigma_t\),

\[F\left(\bigcup_{i=1}^{n}\sigma_i\right) \leq t \implies \bigcap_{i=1}^{n}Futures_t(\sigma_i)\neq \emptyset\] 
(* Theorem 2 *)
Theorem n_common_futures '{CBC_protocol_eq} : forall ls : list pstate,
  (equivocation_weight (fold_right state_union state0 (map (fun ps => proj1_sig ps) ls))
    <= proj1_sig t)%R -> exists ps : pstate, Forall (fun ps' => pstate_rel ps' ps) ls.

To extend the results from a pair of protocol states to a larger set of n protocol states, a list of protocol states denoted by list pstate is used. The application of a function on each of the items in the list is done using map, and the union of the items in the list is recursively done using fold_right and state_union. The Forall is used to express all elements of a given list satisfy a given proposition P : Prop, which in Theorem 2 is pstate_rel ps' ps, i.e. the reachability of ps from ps' with ps' iterating over the list ls.

Proof.
  intros pls H_weight.
  (* obtain a list of states from extracting data from the list of protocol states *)
  remember (map (fun ps => proj1_sig ps) pls) as ls.
  assert (H_ls : Forall prot_state ls) by (subst; apply pstate_list).
  (* proposing the union of the protocol states in the list as a common future  *)
  exists (exist _ (fold_right state_union state0 ls) (prot_state_union_iter ls H_ls H_weight)).
  (* shows that the union the protocol states in the list is 
     reachable from all the protocol states in the list *)
  apply Forall_forall. intros. destruct x as [x H_x]. unfold pstate_rel. simpl.
  apply reach_union_iter.
  subst. apply in_map_iff.
  exists (exist (fun s : state => prot_state s) x H_x). simpl.
  split; reflexivity || assumption.
  Qed.

The proof of Theorem 2 is simply a generalisation of the reasoning steps taken in Theorem 1. Estabilising the union of protocol states in ls as a protocol state was done in prot_state_union_iter, and reach_union_iter shows that every protocol state in the list can reach their union.

The next theorem involves the notion of decided on protocol states. A protocol state s is decided on a property of a protocol state P : pstate -> Prop, if all the protocol states in its future cone forall s', pstate_rel s s', satisfies the property.

Definition decided '{CBC_protocol_eq} (P : pstate -> Prop) : pstate -> Prop :=
  fun (s : pstate) => forall s', pstate_rel s s' -> P s'.

We are now ready to specify Theorem 3.

Two protocol states who do not cross the threshold are decided on the same properties

Theorem 3. \(\forall \sigma_1,\sigma_2 \in \Sigma_t, \forall p \in P_\Sigma\),

\[F(\sigma_1 \cup \sigma_2) \leq t \implies \neg(Decided_{\Sigma,t}(p,\sigma_1)\wedge Decided_{\Sigma,t}(\neg p,\sigma_2))\] 
(* Theorem 3 *)
Theorem pair_consistency_prot '{CBC_protocol_eq} :
  forall s1 s2 : pstate, (equivocation_weight (state_union s1 s2) <= proj1_sig t)%R ->
    forall P, ~ (decided P s1 /\ decided (not P) s2).

In Coq notation, ~A is the shorthand for not A defined by A -> False. Within the Coq, False is a type which we cannot construct a proof for or an object of it. Thus to show negation of A, it says if we can construct an object of A, it will also mean we can construct an object of False which is impossible. In the proof of Theorem 3, we proof by showing absurdity.

Proof.
  (* H_dec is proof that s1 is decided on P and 
     H_dec_not is proof that s2 is not decided on P *)
  intros s1 s2 H_weight P [H_dec H_dec_not].
  (* Theorem 1 allows us to find a common future for s1, s2
     H_r1 and H_r2 is proof of reachability to the common future from s1, s2 *)
  destruct (pair_common_futures s1 s2 H_weight) as [s [H_r1 H_r2]].
  (* reachability from s1 means common future is decided on P *)
  spec H_dec s H_r1.
  (* reachability from s2 means common future is not decided on P, 
     which gives a contradiction *)
  spec H_dec_not s H_r2. contradiction.
  Qed.

  • The expression ~ (decided P s1 /\ decided (not P) s2) means (decided P s1 /\ decided (not P) s2) -> False, thus we are able to introduce proofs of decided P s1 and decided (not P) s2 respectively as H_dec and H_dec_not.

  • Applying pair_common_futures to the protocol states, we get a union of s1, s2 as the state s, accompanied by reachability proofs H_r1, H_r2.

  • The data that s1 is decided on a protocol state property P together with s in its future cone, means s is decided on P

  • A contradiction is derived as a similar argument with the data on s2 would give us s not decided on P

The fourth theorem is built from the definitions of consistent and decisions. Within Coq, it is packed in the definition of state_consistency, which says a list of protocol states ls satisfy state_consistency if there exists a protocol state that satisfy all protocol state properties, given that there is at least one protocols state from the list which is decided on each protocol state property.

Definition state_consistency '{CBC_protocol_eq} (ls : list pstate) : Prop :=
  exists s : pstate,  forall (P : pstate -> Prop),
    Exists (fun s => decided P s) ls -> P s.

This definition compacts the consistent checking of the union of decisions of various protocol states into a single function. The list of protocol states is used to track the various protocol states whose decisions are of interest and forall (P : pstate -> Prop), Exists (fun s => decided P s) ls ensures that we only consider the relevant properties of the protocol states.

Note: Exists checks if any element in the list satisfies a condition; a proof can be constructed only if such an element exists.

Protocol states who do not cross the threshold have a common future which satisfies all their properties

Theorem 4. \(\forall \sigma_i \in \Sigma_t\),

\[F\left(\bigcup_{i=1}^{n}\sigma_i\right) \leq t \implies Consistent_\Sigma\left(\bigcup_{i=1}^{n} Decisions_{\Sigma,t}(\sigma_i)\right)\] 
(* Theorem 4 *)
Theorem n_consistency_prot '{CBC_protocol_eq} :
  forall ls : list pstate,
  (equivocation_weight (fold_right state_union state0 (map (fun ps => proj1_sig ps) ls))
  <= proj1_sig t)%R 
    -> state_consistency ls.

The fourth theorem when proved will provide a constructive algorithm to generate a protocol state which is decided on all the properties that are decided by at least one of protocol state, from the set of protocol states in consideration.

Proof.
  intros ls H_weight.
  (* proposing the union of the protocol states in the list as a candidate *)
  destruct (n_common_futures ls H_weight) as [s' H_reach].
  exists s'.
  (* checking that the candidate is decided on protocol state properties *)
  intros P H_exists.
  (* unpacking the decidability proofs *)
  apply Exists_exists in H_exists.
  destruct H_exists as [s'' [H_in'' H_dec'']].
  (* unpacking the reachability proofs *)
  rewrite Forall_forall in H_reach.
  spec H_reach s'' H_in''.
  spec H_dec'' s' H_reach.
  assumption.
  Qed.

  • n_common_futures constructs the union of the list of protocol state and its corresponding reachability proofs.

  • To check that the candidate satisfies the specifications we require the decidability proofs from premise in state_consistency and reachability proofs from the outputs of n_common_futures. Together they show that the union of the protocols states satisfy the relevant protocol state properties.

Protocol states who do not cross the threshold are guaranteed a consensus value satisfying some properties

We first introduce the definitions used to specify the last safety proof. Recall that the goal is to show that the CBC consensus protocol satisfies the safety property, that is - a common consensus can be guaranteed if the equivocation weights are within the threshold. Our current results only concern protocol states thus there is a need to connect properties of consensus values to properties of protocol states which is done by the lift function.

Definition lift '{CBC_protocol_eq} (P : consensus_values -> Prop) : pstate -> Prop :=
  fun s => forall c : consensus_values, E (proj1_sig s) c -> P c.

Central to this definition is the use of the estimator function E, which maps protocols states to consensus values which allows a protocol state property to be described by a consensus value property. With this we can define consensus_value_consistency which is the consensus value version of state_consistency. Observe that the properties are consensus value properties, which is can be applied in decided through the use of lift. The output is a proof of a consensus value c satisfying a consensus value property P as compared to P s in state_consistency.

Definition consensus_value_consistency '{CBC_protocol_eq} (ls : list pstate) : Prop :=
  exists c, forall (P : consensus_values -> Prop),
    Exists (fun s => decided (lift P) s) ls -> P c.

Theorem 5. \(\forall \sigma_i \in \Sigma_t\),

\[F\left(\bigcup_{i=1}^{n}\sigma_i\right) \leq t \implies Consistent_{\mathcal{C}}\left(\bigcup_{i=1}^{n} Decisions_{\mathcal{C},t}(\sigma_i)\right)\] 
(* Theorem 5 *)
Theorem n_consistency_consensus '{CBC_protocol_eq} :
  forall ls : list pstate,
  (equivocation_weight (fold_right state_union state0 (map (fun ps => proj1_sig ps) ls)) 
  <= proj1_sig t)%R ->
    consensus_value_consistency ls.

The reformulation of Theorem 4 with consensus values as the data of interest is our Theorem 5 above. The proof is more involved as we shall see subsequently.

Proof.
  intros ls H_weight.
  (* construct protocol state and decidability proofs on properties of protocol state  *)
  destruct (n_consistency_prot ls H_weight) as [s H_dec].
  (* consensus value obtained using the estimator is proposed as a candidate *)
  destruct (estimator_total s) as [c about_c]. exists c.
  (* unpacking decidability proofs based on properties of consensus values *)
  intros P H_exists.
  apply Exists_exists in H_exists.
  destruct H_exists as [s' [H_in' H_dec']].
  (* adapt decidability proofs to properties of consensus values to obtain (lift P s) *)
  spec H_dec (lift P).
  spec H_dec. apply Exists_exists.
  exists s'. split; assumption.
  (* Using c and about_c to transport (lift P s) to (P c) *)
  unfold lift in H_dec.
  spec H_dec c about_c; assumption.
  Qed.

  • Using the result of Theorem 4, we are able to generate a protocol state s which is decided on a set of protocol state properties and proofs H_dec that each protocol state property is decided for some protocol state in ls.

  • estimate_total guarantees a consensus value output c for any protocol state s that is fed into estimator. The about_c is proof that the output of E is c when s is provided. Thus we can propose c as the common consensus derived from the protocol states.

  • The premise in consensus_value_consistency gives us decidability proofs H_dec' on properties of protocol states which are lifted from properties of consensus values.

  • Adapting lift P to H_dec to get a protocol state satisfying property lift P, and the process involves using proofs H_in', H_dec'

  • By the definition of lift, by providing the proof c_about that c is a consensus values estimated by E from the protocol state s, the goal of P c is reached.