Accountable safety
This file proves the main accountable-safety theorem: a
finalization fork — two k-finalized blocks that are mutual
non-ancestors — forces a q_intersection_slashed witness.
This is the structural half of the Casper FFG accountable-safety
guarantee: it produces a pair of \frac{2}{3}-quorums whose
intersection consists entirely of slashed validators, without
asserting that the intersection is nonempty (the quantitative
half, carried out in Theories/SlashableBound.lean).
The result generalises the original Casper FFG theorem (Casper FFG,
Theorem 1 / Gasper, Theorem 5.2) from 1-finalization to
arbitrary k-finalization, and from static to dynamic validator
sets (the two quorums may belong to different blocks with different
validator sets V(b_L), V(b_R)).
Definitions
-
finalization_fork — a pair of finalized blocks with mutual
non-ancestry (the safety-violation predicate)
-
k_finalization_fork / same_k_finalization_fork — the
k-finalized generalisation with independent depths
Case analysis
The proof of k_safety' proceeds by three-way case split on
the heights b_{1,h} and b_{2,h} of the two k-finalized
blocks. Each branch terminates by exhibiting a
q_intersection_slashed witness from one of two slashing
conditions:
-
Equal heights (k_equal_height_case) — Casper (S1):
two distinct justified blocks at the same height force a
double-vote witness via
two_justified_same_height_slashed.
-
Surround case (k_slash_surround_case_general) —
Casper (S2): a justification link that spans the finalized
block's chain on the height axis produces a surround-vote
witness, or collapses to a same-height double-vote.
-
Non-equal heights, inductive
(k_non_equal_height_case_ind) — strong induction on the
height gap b_{1,h} - b_{2,h} via strong_induction_sub,
descending along justification links until one of the two base
cases above applies.
Derivation chain
\operatorname{accountable\_safety} \;\xleftarrow{\text{convert}}\; \operatorname{k\_accountable\_safety} \;\xleftarrow{\text{destruct}}\; \operatorname{k\_safety'} \;\xleftarrow{\text{3-way}}\; \begin{cases} \operatorname{k\_equal\_height\_case} \\ \operatorname{k\_non\_equal\_height\_case} \to \operatorname{k\_non\_equal\_height\_case\_ind} \end{cases}
Non-goals of this file
This file is the structural half only. It proves that every
shared validator is slashed, but does not prove that the shared
set has positive weight. The quantitative bound
\operatorname{wt}(V_L \cap V_R) - f_{1/3}(\operatorname{wt}(V_L)) - f_{1/3}(\operatorname{wt}(V_R)) \le \operatorname{wt}(q_L \cap q_R)
is established independently in Theories/SlashableBound.lean.
variable {Validator : Type u}variable {Hash : Type v}variable [DecidableEq Validator]variable [DecidableEq Hash]variable [Fintype Validator]
Two finalized blocks with mutual non-ancestry
A finalization fork: two blocks b_1, b_2, each finalized in
\sigma, such that neither is an ancestor of the other.
Formal content
\exists\, b_1\, b_{1,h}\, b_2\, b_{2,h},\;\; \operatorname{finalized}(\sigma, b_1, b_{1,h}) \;\wedge\; \operatorname{finalized}(\sigma, b_2, b_{2,h}) \;\wedge\; \neg\,(b_2 \xrightarrow{*} b_1) \;\wedge\; \neg\,(b_1 \xrightarrow{*} b_2)
Interpretation
This is the abstract formulation of a safety violation in
Casper FFG: two blocks have been irreversibly committed by
\frac{2}{3}-quorum support, yet neither lies on the other's
chain. In a tree-structured block universe, this means the protocol
has committed to two incompatible histories.
Non-assumptions
The predicate does not assert that b_1 \ne b_2 (distinctness
is a consequence of the mutual non-ancestry, since reflexivity of
ancestry gives b \xrightarrow{*} b). It also does not assert
any relationship between the two heights b_{1,h} and b_{2,h}.
def finalization_fork
(τ : Threshold)
(stake : Validator → Nat)
(vset : Hash → Finset Validator)
(parent : HashParent Hash)
(genesis : Hash)
(st : State Validator Hash) : Prop :=
∃ b1 : Hash, ∃ b1_h : Nat, ∃ b2 : Hash, ∃ b2_h : Nat,
finalized τ stake vset parent genesis st b1 b1_h ∧
finalized τ stake vset parent genesis st b2 b2_h ∧
¬ hash_ancestor parent b2 b1 ∧
¬ hash_ancestor parent b1 b2
k-finalization fork
The k-finalized generalisation of finalization_fork: two
blocks b_1, b_2, each k_i-finalized, with mutual non-ancestry.
Formal content
\exists\, b_1\, b_{1,h}\, b_2\, b_{2,h},\;\; \operatorname{k\_finalized}(\sigma, b_1, b_{1,h}, k_1) \;\wedge\; \operatorname{k\_finalized}(\sigma, b_2, b_{2,h}, k_2) \;\wedge\; \neg\,(b_2 \xrightarrow{*} b_1) \;\wedge\; \neg\,(b_1 \xrightarrow{*} b_2)
Interpretation
The two finalization depths k_1, k_2 are independent parameters,
allowing the two conflicting blocks to have different depths of
confirmation. At k_1 = k_2 = 1 this recovers
finalization_fork (via
finalization_fork_means_same_finalization_fork_one).
def k_finalization_fork
(τ : Threshold)
(stake : Validator → Nat)
(vset : Hash → Finset Validator)
(parent : HashParent Hash)
(genesis : Hash)
(st : State Validator Hash)
(k1 k2 : Nat) : Prop :=
∃ b1 : Hash, ∃ b1_h : Nat, ∃ b2 : Hash, ∃ b2_h : Nat,
k_finalized τ stake vset parent genesis st b1 b1_h k1 ∧
k_finalized τ stake vset parent genesis st b2 b2_h k2 ∧
¬ hash_ancestor parent b2 b1 ∧
¬ hash_ancestor parent b1 b2
Symmetric k-finalization fork
Both blocks share the same finalization depth k:
\operatorname{same\_k\_finalization\_fork}(\sigma, k) \;\;\coloneqq\;\; \operatorname{k\_finalization\_fork}(\sigma, k, k)
This specialisation is the form consumed by
finalization_fork_means_same_finalization_fork_one, where
the k = 1 instance recovers finalization_fork.
def same_k_finalization_fork
(τ : Threshold)
(stake : Validator → Nat)
(vset : Hash → Finset Validator)
(parent : HashParent Hash)
(genesis : Hash)
(st : State Validator Hash)
(k : Nat) : Prop :=
k_finalization_fork τ stake vset parent genesis st k k
Finalization fork is equivalent to 1-finalization fork
Statement
\operatorname{finalization\_fork}(\sigma) \;\iff\; \operatorname{same\_k\_finalization\_fork}(\sigma, 1)
Proof idea
Both directions apply finalized_means_one_finalized to
each of the two finalized blocks in the fork, converting between
finalized and \operatorname{k\_finalized}(\cdot, \cdot, 1).
The non-ancestry hypotheses \neg\,(b_2 \xrightarrow{*} b_1) and
\neg\,(b_1 \xrightarrow{*} b_2) pass through unchanged.
Role in the development
The single bridge between the finalization_fork definition
(stated in terms of finalized) and the k-parameterised
proof machinery. Consumed by accountable_safety to enter
the k-finalized world, and inversely available if the user wishes
to return to the one-step formulation.
theorem finalization_fork_means_same_finalization_fork_one
(τ : Threshold)
(stake : Validator → Nat)
(vset : Hash → Finset Validator)
(parent : HashParent Hash)
(genesis : Hash)
(st : State Validator Hash) :
finalization_fork τ stake vset parent genesis st
↔
same_k_finalization_fork τ stake vset parent genesis st 1 :=
⟨fun ⟨b1, b1_h, b2, b2_h, hfin1, hfin2, hn1, hn2⟩ =>
⟨b1, b1_h, b2, b2_h,
(finalized_means_one_finalized τ stake vset parent genesis st b1 b1_h).mp hfin1,
(finalized_means_one_finalized τ stake vset parent genesis st b2 b2_h).mp hfin2,
hn1, hn2⟩,
fun ⟨b1, b1_h, b2, b2_h, hk1, hk2, hn1, hn2⟩ =>
⟨b1, b1_h, b2, b2_h,
(finalized_means_one_finalized τ stake vset parent genesis st b1 b1_h).mpr hk1,
(finalized_means_one_finalized τ stake vset parent genesis st b2 b2_h).mpr hk2,
hn1, hn2⟩⟩
finalization_fork_means_same_finalization_fork_one : ∀ {Validator : Type u} {Hash : Type v}
[inst : DecidableEq Validator] [inst_1 : DecidableEq Hash] [inst_2 : Fintype Validator] (τ : Threshold)
(stake : Validator → Nat) (vset : Hash → Finset Validator) (parent : HashParent Hash) (genesis : Hash)
(st : State Validator Hash),
Iff (finalization_fork τ stake vset parent genesis st)
(same_k_finalization_fork τ stake vset parent genesis st (1 : Nat))
0 │ │ Validator ├ Type
u
1 │ │ Hash ├ Type
v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ x✝ │ ┌ finalization_fork
τ stake vset parent genesis st
12│ │ b1 │ │ ┌ Hash
13│ │ b1_h │ │ ├ Nat
14│ │ b2 │ │ ├ Hash
15│ │ b2_h │ │ ├ Nat
16│ │ hfin1 │ │ ├ finalized
τ stake vset parent genesis st b1 b1_h
17│ │ hfin2 │ │ ├ finalized
τ stake vset parent genesis st b2 b2_h
18│ │ hn1 │ │ ├ Not
(hash_ancestor parent b2 b1)
19│ │ hn2 │ │ ├ Not
(hash_ancestor parent b1 b2)
20│ │ finalized_means_one_finalized │ │ │ Iff
(finalized τ stake vset parent genesis st b1 b1_h) (k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat))
21│20,16 │ Iff.mp │ │ │ k_finalized
τ stake vset parent genesis st b1 b1_h (1 : Nat)
22│ │ finalized_means_one_finalized │ │ │ Iff
(finalized τ stake vset parent genesis st b2 b2_h) (k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
23│22,17 │ Iff.mp │ │ │ k_finalized
τ stake vset parent genesis st b2 b2_h (1 : Nat)
24│18,19 │ And.intro │ │ │ And
(Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))
25│23,24 │ And.intro │ │ │ And
(k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2)))
26│21,25 │ And.intro │ │ │ And
(k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat))
(And (k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
27│26 │ Exists.intro │ │ │ Exists
fun (b2_h : Nat) =>
And (k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat))
(And (k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
28│27 │ Exists.intro │ │ │ Exists
fun (b2 : Hash) =>
Exists fun (b2_h : Nat) =>
And (k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat))
(And (k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
29│28 │ Exists.intro │ │ │ Exists
fun (b1_h : Nat) =>
Exists fun (b2 : Hash) =>
Exists fun (b2_h : Nat) =>
And (k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat))
(And (k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
30│29 │ Exists.intro │ │ │ Exists
fun (b1 : Hash) =>
Exists fun (b1_h : Nat) =>
Exists fun (b2 : Hash) =>
Exists fun (b2_h : Nat) =>
And (k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat))
(And (k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
31│12,13,14,15,16,17,18,19,30│ ∀I │ │ ∀
(b1 : Hash) (b1_h : Nat) (b2 : Hash) (b2_h : Nat),
finalized τ stake vset parent genesis st b1 b1_h →
finalized τ stake vset parent genesis st b2 b2_h →
Not (hash_ancestor parent b2 b1) →
Not (hash_ancestor parent b1 b2) →
Exists fun (b1 : Hash) =>
Exists fun (b1_h : Nat) =>
Exists fun (b2 : Hash) =>
Exists fun (b2_h : Nat) =>
And (k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat))
(And (k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
32│11,31 │ finalization_fork_means_same_finalization_fork_one.match_1 │ │ same_k_finalization_fork τ
stake vset parent genesis st (1 : Nat)
33│11,32 │ ∀I │ finalization_fork
τ stake vset parent genesis st →
same_k_finalization_fork τ stake vset parent genesis st (1 : Nat)
34│ │ x✝ │ ┌ same_k_finalization_fork
τ stake vset parent genesis st (1 : Nat)
35│ │ b1 │ │ ┌ Hash
36│ │ b1_h │ │ ├ Nat
37│ │ b2 │ │ ├ Hash
38│ │ b2_h │ │ ├ Nat
39│ │ hk1 │ │ ├ k_finalized
τ stake vset parent genesis st b1 b1_h (1 : Nat)
40│ │ hk2 │ │ ├ k_finalized
τ stake vset parent genesis st b2 b2_h (1 : Nat)
41│ │ hn1 │ │ ├ Not
(hash_ancestor parent b2 b1)
42│ │ hn2 │ │ ├ Not
(hash_ancestor parent b1 b2)
43│ │ finalized_means_one_finalized │ │ │ Iff
(finalized τ stake vset parent genesis st b1 b1_h) (k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat))
44│43,39 │ Iff.mpr │ │ │ finalized
τ stake vset parent genesis st b1 b1_h
45│ │ finalized_means_one_finalized │ │ │ Iff
(finalized τ stake vset parent genesis st b2 b2_h) (k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
46│45,40 │ Iff.mpr │ │ │ finalized
τ stake vset parent genesis st b2 b2_h
47│41,42 │ And.intro │ │ │ And
(Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))
48│46,47 │ And.intro │ │ │ And
(finalized τ stake vset parent genesis st b2 b2_h)
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2)))
49│44,48 │ And.intro │ │ │ And
(finalized τ stake vset parent genesis st b1 b1_h)
(And (finalized τ stake vset parent genesis st b2 b2_h)
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
50│49 │ Exists.intro │ │ │ Exists
fun (b2_h : Nat) =>
And (finalized τ stake vset parent genesis st b1 b1_h)
(And (finalized τ stake vset parent genesis st b2 b2_h)
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
51│50 │ Exists.intro │ │ │ Exists
fun (b2 : Hash) =>
Exists fun (b2_h : Nat) =>
And (finalized τ stake vset parent genesis st b1 b1_h)
(And (finalized τ stake vset parent genesis st b2 b2_h)
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
52│51 │ Exists.intro │ │ │ Exists
fun (b1_h : Nat) =>
Exists fun (b2 : Hash) =>
Exists fun (b2_h : Nat) =>
And (finalized τ stake vset parent genesis st b1 b1_h)
(And (finalized τ stake vset parent genesis st b2 b2_h)
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
53│52 │ Exists.intro │ │ │ Exists
fun (b1 : Hash) =>
Exists fun (b1_h : Nat) =>
Exists fun (b2 : Hash) =>
Exists fun (b2_h : Nat) =>
And (finalized τ stake vset parent genesis st b1 b1_h)
(And (finalized τ stake vset parent genesis st b2 b2_h)
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
54│35,36,37,38,39,40,41,42,53│ ∀I │ │ ∀
(b1 : Hash) (b1_h : Nat) (b2 : Hash) (b2_h : Nat),
k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat) →
k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat) →
Not (hash_ancestor parent b2 b1) →
Not (hash_ancestor parent b1 b2) →
Exists fun (b1 : Hash) =>
Exists fun (b1_h : Nat) =>
Exists fun (b2 : Hash) =>
Exists fun (b2_h : Nat) =>
And (finalized τ stake vset parent genesis st b1 b1_h)
(And (finalized τ stake vset parent genesis st b2 b2_h)
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
55│34,54 │ finalization_fork_means_same_finalization_fork_one.match_2 │ │ finalization_fork τ stake
vset parent genesis st
56│34,55 │ ∀I │ same_k_finalization_fork
τ stake vset parent genesis st (1 : Nat) →
finalization_fork τ stake vset parent genesis st
57│33,56 │ Iff.intro │ Iff
(finalization_fork τ stake vset parent genesis st) (same_k_finalization_fork τ stake vset parent genesis st (1 : Nat))
58│0,1,2,3,4,5,6,7,8,9,10,57 │ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash),
Iff (finalization_fork τ stake vset parent genesis st)
(same_k_finalization_fork τ stake vset parent genesis st (1 : Nat))
#detail_explode finalization_fork_means_same_finalization_fork_onefinalization_fork_means_same_finalization_fork_one : ∀ {Validator : Type u} {Hash : Type v}
[inst : DecidableEq Validator] [inst_1 : DecidableEq Hash] [inst_2 : Fintype Validator] (τ : Threshold)
(stake : Validator → Nat) (vset : Hash → Finset Validator) (parent : HashParent Hash) (genesis : Hash)
(st : State Validator Hash),
Iff (finalization_fork τ stake vset parent genesis st)
(same_k_finalization_fork τ stake vset parent genesis st (1 : Nat))
0 │ │ Validator ├ Type
u
1 │ │ Hash ├ Type
v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ x✝ │ ┌ finalization_fork
τ stake vset parent genesis st
12│ │ b1 │ │ ┌ Hash
13│ │ b1_h │ │ ├ Nat
14│ │ b2 │ │ ├ Hash
15│ │ b2_h │ │ ├ Nat
16│ │ hfin1 │ │ ├ finalized
τ stake vset parent genesis st b1 b1_h
17│ │ hfin2 │ │ ├ finalized
τ stake vset parent genesis st b2 b2_h
18│ │ hn1 │ │ ├ Not
(hash_ancestor parent b2 b1)
19│ │ hn2 │ │ ├ Not
(hash_ancestor parent b1 b2)
20│ │ finalized_means_one_finalized │ │ │ Iff
(finalized τ stake vset parent genesis st b1 b1_h) (k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat))
21│20,16 │ Iff.mp │ │ │ k_finalized
τ stake vset parent genesis st b1 b1_h (1 : Nat)
22│ │ finalized_means_one_finalized │ │ │ Iff
(finalized τ stake vset parent genesis st b2 b2_h) (k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
23│22,17 │ Iff.mp │ │ │ k_finalized
τ stake vset parent genesis st b2 b2_h (1 : Nat)
24│18,19 │ And.intro │ │ │ And
(Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))
25│23,24 │ And.intro │ │ │ And
(k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2)))
26│21,25 │ And.intro │ │ │ And
(k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat))
(And (k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
27│26 │ Exists.intro │ │ │ Exists
fun (b2_h : Nat) =>
And (k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat))
(And (k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
28│27 │ Exists.intro │ │ │ Exists
fun (b2 : Hash) =>
Exists fun (b2_h : Nat) =>
And (k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat))
(And (k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
29│28 │ Exists.intro │ │ │ Exists
fun (b1_h : Nat) =>
Exists fun (b2 : Hash) =>
Exists fun (b2_h : Nat) =>
And (k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat))
(And (k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
30│29 │ Exists.intro │ │ │ Exists
fun (b1 : Hash) =>
Exists fun (b1_h : Nat) =>
Exists fun (b2 : Hash) =>
Exists fun (b2_h : Nat) =>
And (k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat))
(And (k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
31│12,13,14,15,16,17,18,19,30│ ∀I │ │ ∀
(b1 : Hash) (b1_h : Nat) (b2 : Hash) (b2_h : Nat),
finalized τ stake vset parent genesis st b1 b1_h →
finalized τ stake vset parent genesis st b2 b2_h →
Not (hash_ancestor parent b2 b1) →
Not (hash_ancestor parent b1 b2) →
Exists fun (b1 : Hash) =>
Exists fun (b1_h : Nat) =>
Exists fun (b2 : Hash) =>
Exists fun (b2_h : Nat) =>
And (k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat))
(And (k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
32│11,31 │ finalization_fork_means_same_finalization_fork_one.match_1 │ │ same_k_finalization_fork τ
stake vset parent genesis st (1 : Nat)
33│11,32 │ ∀I │ finalization_fork
τ stake vset parent genesis st →
same_k_finalization_fork τ stake vset parent genesis st (1 : Nat)
34│ │ x✝ │ ┌ same_k_finalization_fork
τ stake vset parent genesis st (1 : Nat)
35│ │ b1 │ │ ┌ Hash
36│ │ b1_h │ │ ├ Nat
37│ │ b2 │ │ ├ Hash
38│ │ b2_h │ │ ├ Nat
39│ │ hk1 │ │ ├ k_finalized
τ stake vset parent genesis st b1 b1_h (1 : Nat)
40│ │ hk2 │ │ ├ k_finalized
τ stake vset parent genesis st b2 b2_h (1 : Nat)
41│ │ hn1 │ │ ├ Not
(hash_ancestor parent b2 b1)
42│ │ hn2 │ │ ├ Not
(hash_ancestor parent b1 b2)
43│ │ finalized_means_one_finalized │ │ │ Iff
(finalized τ stake vset parent genesis st b1 b1_h) (k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat))
44│43,39 │ Iff.mpr │ │ │ finalized
τ stake vset parent genesis st b1 b1_h
45│ │ finalized_means_one_finalized │ │ │ Iff
(finalized τ stake vset parent genesis st b2 b2_h) (k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat))
46│45,40 │ Iff.mpr │ │ │ finalized
τ stake vset parent genesis st b2 b2_h
47│41,42 │ And.intro │ │ │ And
(Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))
48│46,47 │ And.intro │ │ │ And
(finalized τ stake vset parent genesis st b2 b2_h)
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2)))
49│44,48 │ And.intro │ │ │ And
(finalized τ stake vset parent genesis st b1 b1_h)
(And (finalized τ stake vset parent genesis st b2 b2_h)
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
50│49 │ Exists.intro │ │ │ Exists
fun (b2_h : Nat) =>
And (finalized τ stake vset parent genesis st b1 b1_h)
(And (finalized τ stake vset parent genesis st b2 b2_h)
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
51│50 │ Exists.intro │ │ │ Exists
fun (b2 : Hash) =>
Exists fun (b2_h : Nat) =>
And (finalized τ stake vset parent genesis st b1 b1_h)
(And (finalized τ stake vset parent genesis st b2 b2_h)
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
52│51 │ Exists.intro │ │ │ Exists
fun (b1_h : Nat) =>
Exists fun (b2 : Hash) =>
Exists fun (b2_h : Nat) =>
And (finalized τ stake vset parent genesis st b1 b1_h)
(And (finalized τ stake vset parent genesis st b2 b2_h)
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
53│52 │ Exists.intro │ │ │ Exists
fun (b1 : Hash) =>
Exists fun (b1_h : Nat) =>
Exists fun (b2 : Hash) =>
Exists fun (b2_h : Nat) =>
And (finalized τ stake vset parent genesis st b1 b1_h)
(And (finalized τ stake vset parent genesis st b2 b2_h)
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
54│35,36,37,38,39,40,41,42,53│ ∀I │ │ ∀
(b1 : Hash) (b1_h : Nat) (b2 : Hash) (b2_h : Nat),
k_finalized τ stake vset parent genesis st b1 b1_h (1 : Nat) →
k_finalized τ stake vset parent genesis st b2 b2_h (1 : Nat) →
Not (hash_ancestor parent b2 b1) →
Not (hash_ancestor parent b1 b2) →
Exists fun (b1 : Hash) =>
Exists fun (b1_h : Nat) =>
Exists fun (b2 : Hash) =>
Exists fun (b2_h : Nat) =>
And (finalized τ stake vset parent genesis st b1 b1_h)
(And (finalized τ stake vset parent genesis st b2 b2_h)
(And (Not (hash_ancestor parent b2 b1)) (Not (hash_ancestor parent b1 b2))))
55│34,54 │ finalization_fork_means_same_finalization_fork_one.match_2 │ │ finalization_fork τ stake
vset parent genesis st
56│34,55 │ ∀I │ same_k_finalization_fork
τ stake vset parent genesis st (1 : Nat) →
finalization_fork τ stake vset parent genesis st
57│33,56 │ Iff.intro │ Iff
(finalization_fork τ stake vset parent genesis st) (same_k_finalization_fork τ stake vset parent genesis st (1 : Nat))
58│0,1,2,3,4,5,6,7,8,9,10,57 │ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash),
Iff (finalization_fork τ stake vset parent genesis st)
(same_k_finalization_fork τ stake vset parent genesis st (1 : Nat))
A k-finalized block and a distinct justified block have different heights
Statement
\operatorname{k\_finalized}(\sigma, b_f, h_f, k) \;\wedge\; \operatorname{justified}(\sigma, b_j, h_j) \;\wedge\; \neg\,\operatorname{q\_intersection\_slashed}(\sigma) \;\wedge\; b_j \ne b_f \;\implies\; h_j \ne h_f
Interpretation
A k-finalized block occupies a unique height slot among
justified blocks: no other justified block can share its height
without triggering slashing. This is the height-separation
guarantee that feeds the three-way case split in k_safety'.
Proof idea
Extract b_f's justification from its k-finalization via
k_finalized_means_justified, then apply
no_two_justified_same_height to the two justified blocks
b_j and b_f at heights h_j and h_f with the
non-slashing hypothesis.
Role in the development
A convenience lemma that packages the two-step reduction
(k-finalized \to justified \to height-separation) into
a single invocation. Used in the equal-height branch of the safety
argument to derive a contradiction when two non-ancestor blocks
appear at the same height.
no_k_finalized_justified_same_height : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator]
[inst_1 : DecidableEq Hash] [inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat)
(vset : Hash → Finset Validator) (parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash)
{bf bj : Hash} {bf_h bj_h k : Nat},
k_finalized τ stake vset parent genesis st bf bf_h k →
justified τ stake vset parent genesis st bj bj_h →
Not (q_intersection_slashed τ stake vset st) → Ne bj bf → Ne bj_h bf_h
0 │ │ Validator ├ Type u
1 │ │ Hash ├ Type v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ bf ├ Hash
12│ │ bj ├ Hash
13│ │ bf_h ├ Nat
14│ │ bj_h ├ Nat
15│ │ k ├ Nat
16│ │ hf ├ k_finalized
τ stake vset parent genesis st bf bf_h k
17│ │ hj ├ justified
τ stake vset parent genesis st bj bj_h
18│ │ hno ├ Not
(q_intersection_slashed τ stake vset st)
19│ │ hneq ├ Ne bj bf
20│16 │ k_finalized_means_justified │ justified τ stake vset parent
genesis st bf bf_h
21│17,20,18,19 │ no_two_justified_same_height │ Ne bj_h bf_h
22│0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,21│ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {bf bj : Hash} {bf_h bj_h k : Nat},
k_finalized τ stake vset parent genesis st bf bf_h k →
justified τ stake vset parent genesis st bj bj_h →
Not (q_intersection_slashed τ stake vset st) → Ne bj bf → Ne bj_h bf_h
#detail_explode no_k_finalized_justified_same_heightno_k_finalized_justified_same_height : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator]
[inst_1 : DecidableEq Hash] [inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat)
(vset : Hash → Finset Validator) (parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash)
{bf bj : Hash} {bf_h bj_h k : Nat},
k_finalized τ stake vset parent genesis st bf bf_h k →
justified τ stake vset parent genesis st bj bj_h →
Not (q_intersection_slashed τ stake vset st) → Ne bj bf → Ne bj_h bf_h
0 │ │ Validator ├ Type u
1 │ │ Hash ├ Type v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ bf ├ Hash
12│ │ bj ├ Hash
13│ │ bf_h ├ Nat
14│ │ bj_h ├ Nat
15│ │ k ├ Nat
16│ │ hf ├ k_finalized
τ stake vset parent genesis st bf bf_h k
17│ │ hj ├ justified
τ stake vset parent genesis st bj bj_h
18│ │ hno ├ Not
(q_intersection_slashed τ stake vset st)
19│ │ hneq ├ Ne bj bf
20│16 │ k_finalized_means_justified │ justified τ stake vset parent
genesis st bf bf_h
21│17,20,18,19 │ no_two_justified_same_height │ Ne bj_h bf_h
22│0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,21│ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {bf bj : Hash} {bf_h bj_h k : Nat},
k_finalized τ stake vset parent genesis st bf bf_h k →
justified τ stake vset parent genesis st bj bj_h →
Not (q_intersection_slashed τ stake vset st) → Ne bj bf → Ne bj_h bf_h
Equal-height case: both blocks at the same height
Statement
\operatorname{k\_finalized}(\sigma, b_1, h, k_1) \;\wedge\; \operatorname{k\_finalized}(\sigma, b_2, h, k_2) \;\wedge\; b_1 \ne b_2 \;\implies\; \operatorname{q\_intersection\_slashed}(\sigma)
Interpretation
Two distinct k-finalized blocks at the same height h —
this is the direct manifestation of Casper's slashing condition
(S1): the two supporting \frac{2}{3}-quorums have cast votes
to distinct targets at the same target height, so every shared
validator has equivocated (slashed_double_vote).
Proof idea
Extract both blocks' justifications via
k_finalized_means_justified, then apply
two_justified_same_height_slashed — the same-height
slashing kernel from Lemmas/AccountableSafety.lean — to
the two justified blocks b_1, b_2 at height h with
b_1 \ne b_2.
Role in the development
The base case of the safety case analysis: the equal-height branch
of k_safety'. The other two branches (surround and
inductive) eventually reduce to this case or to a direct surround
witness.
k_equal_height_case : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {b1 b2 : Hash} {h k1 k2 : Nat},
k_finalized τ stake vset parent genesis st b1 h k1 →
k_finalized τ stake vset parent genesis st b2 h k2 → Ne b1 b2 → q_intersection_slashed τ stake vset st
0 │ │ Validator ├ Type u
1 │ │ Hash ├ Type v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ b1 ├ Hash
12│ │ b2 ├ Hash
13│ │ h ├ Nat
14│ │ k1 ├ Nat
15│ │ k2 ├ Nat
16│ │ hf1 ├ k_finalized
τ stake vset parent genesis st b1 h k1
17│ │ hf2 ├ k_finalized
τ stake vset parent genesis st b2 h k2
18│ │ hneq ├ Ne b1
b2
19│16 │ k_finalized_means_justified │ justified τ stake vset parent
genesis st b1 h
20│17 │ k_finalized_means_justified │ justified τ stake vset parent
genesis st b2 h
21│19,20,18 │ two_justified_same_height_slashed │ q_intersection_slashed τ stake
vset st
22│0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,21│ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {b1 b2 : Hash} {h k1 k2 : Nat},
k_finalized τ stake vset parent genesis st b1 h k1 →
k_finalized τ stake vset parent genesis st b2 h k2 → Ne b1 b2 → q_intersection_slashed τ stake vset st
#detail_explode k_equal_height_casek_equal_height_case : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {b1 b2 : Hash} {h k1 k2 : Nat},
k_finalized τ stake vset parent genesis st b1 h k1 →
k_finalized τ stake vset parent genesis st b2 h k2 → Ne b1 b2 → q_intersection_slashed τ stake vset st
0 │ │ Validator ├ Type u
1 │ │ Hash ├ Type v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ b1 ├ Hash
12│ │ b2 ├ Hash
13│ │ h ├ Nat
14│ │ k1 ├ Nat
15│ │ k2 ├ Nat
16│ │ hf1 ├ k_finalized
τ stake vset parent genesis st b1 h k1
17│ │ hf2 ├ k_finalized
τ stake vset parent genesis st b2 h k2
18│ │ hneq ├ Ne b1
b2
19│16 │ k_finalized_means_justified │ justified τ stake vset parent
genesis st b1 h
20│17 │ k_finalized_means_justified │ justified τ stake vset parent
genesis st b2 h
21│19,20,18 │ two_justified_same_height_slashed │ q_intersection_slashed τ stake
vset st
22│0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,21│ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {b1 b2 : Hash} {h k1 k2 : Nat},
k_finalized τ stake vset parent genesis st b1 h k1 →
k_finalized τ stake vset parent genesis st b2 h k2 → Ne b1 b2 → q_intersection_slashed τ stake vset st
Surround case: full containment
Statement
\operatorname{justification\_link}(\sigma, s, t, h_s, h_t) \;\wedge\; \operatorname{k\_finalized}(\sigma, b, b_h, k) \;\wedge\; b_h + k < h_t \;\wedge\; h_s < b_h \;\implies\; \operatorname{q\_intersection\_slashed}(\sigma)
The outer link (s, t) fully contains the finalized chain
(b, b_h) \to (b_h + k) on the height axis: h_s < b_h and
b_h + k < h_t.
Interpretation
This is the direct manifestation of Casper's slashing condition
(S2): the outer justification link's vote spans
[h_s,\, h_t] and the inner finalization link's vote spans
[b_h,\, b_h + k], with the strict containment
h_s < b_h \le b_h + k < h_t giving the surround ordering
h_{s_{\text{outer}}} < h_{s_{\text{inner}}} and
h_{t_{\text{inner}}} < h_{t_{\text{outer}}}. Every validator
who voted in both links has cast a surround vote.
Proof idea
The outer vote is the justification link's supermajority link from
(s, h_s) to (t, h_t), witnessed by
link_supporters (s, t, h_s, h_t). The inner vote is the
k-finalization chain's supermajority link from
(\mathit{final}, b_h) to (\mathit{ls.getLastD\, final},\, b_h + k).
The four heights satisfy
h_s < b_h \le b_h + k < h_t (the surround condition),
and every validator in the intersection of the two quorums has cast
both votes — hence satisfies slashed_surround_vote, wrapped
in Or.inr to inhabit slashed.
theorem k_slash_surround_full_containment
(τ : Threshold)
(stake : Validator → Nat)
(vset : Hash → Finset Validator)
(parent : HashParent Hash)
(genesis : Hash)
(st : State Validator Hash)
{s t final : Hash}
{s_h t_h final_h k : Nat}
(hlink_st : justification_link τ stake vset parent st s t s_h t_h)
(hfinal : k_finalized τ stake vset parent genesis st final final_h k)
(h_full : final_h + k < t_h)
(h_surround_start : s_h < final_h) :
q_intersection_slashed τ stake vset st :=
match hlink_st, hfinal with
| ⟨_, _, hsm_outer⟩, ⟨_, ls, _, _, _, hsm_inner⟩ =>
match hsm_outer, hsm_inner with
| ⟨hsm_outer_sub, _⟩, ⟨hsm_inner_sub, _⟩ =>
⟨t, ls.getLastD final,
link_supporters st s t s_h t_h,
link_supporters st final (ls.getLastD final) final_h (final_h + k),
hsm_outer_sub, hsm_inner_sub, hsm_outer, hsm_inner,
fun _ hvO hvI => Or.inr ⟨s, t, s_h, t_h, final, ls.getLastD final,
final_h, final_h + k,
mem_link_supporters.mp hvO, mem_link_supporters.mp hvI,
h_surround_start, h_full⟩⟩
k_slash_surround_full_containment : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator]
[inst_1 : DecidableEq Hash] [inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat)
(vset : Hash → Finset Validator) (parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash)
{s t final : Hash} {s_h t_h final_h k : Nat},
justification_link τ stake vset parent st s t s_h t_h →
k_finalized τ stake vset parent genesis st final final_h k →
LT.lt (HAdd.hAdd final_h k) t_h → LT.lt s_h final_h → q_intersection_slashed τ stake vset st
0 │ │ Validator ├ Type
u
1 │ │ Hash ├ Type
v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ s ├ Hash
12│ │ t ├ Hash
13│ │ final ├ Hash
14│ │ s_h ├ Nat
15│ │ t_h ├ Nat
16│ │ final_h ├ Nat
17│ │ k ├ Nat
18│ │ hlink_st ├ justification_link
τ stake vset parent st s t s_h t_h
19│ │ hfinal ├ k_finalized
τ stake vset parent genesis st final final_h k
20│ │ h_full ├ LT.lt
(HAdd.hAdd final_h k) t_h
21│ │ h_surround_start ├ LT.lt
s_h final_h
22│ │ left✝⁵ │ ┌ LT.lt
s_h t_h
23│ │ left✝⁴ │ ├ nth_ancestor
parent (HSub.hSub t_h s_h) s t
24│ │ hsm_outer │ ├ supermajority_link
τ stake vset st s t s_h t_h
25│ │ left✝³ │ ├ LE.le
(1 : Nat) k
26│ │ ls │ ├ List
Hash
27│ │ left✝² │ ├ Eq
(List.length ls) (HAdd.hAdd k (1 : Nat))
28│ │ left✝¹ │ ├ Eq
(List.headD ls final) final
29│ │ left✝ │ ├ ∀
(n : Nat),
LE.le n k →
And (justified τ stake vset parent genesis st (List.getD ls n final) (HAdd.hAdd final_h n))
(nth_ancestor parent n final (List.getD ls n final))
30│ │ hsm_inner │ ├ supermajority_link
τ stake vset st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)
31│ │ hsm_outer_sub │ │ ┌ Subset
(link_supporters st s t s_h t_h) (vset t)
32│ │ right✝¹ │ │ ├ LE.le
(Threshold.two_third τ (wt stake (vset t))) (wt stake (link_supporters st s t s_h t_h))
33│ │ hsm_inner_sub │ │ ├ Subset
(link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)) (vset (List.getLastD ls final))
34│ │ right✝ │ │ ├ LE.le
(Threshold.two_third τ (wt stake (vset (List.getLastD ls final))))
(wt stake (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)))
35│ │ x✝ │ │ │ ┌ Validator
36│ │ hvO │ │ │ ├ Membership.mem
(link_supporters st s t s_h t_h) x✝
37│ │ hvI │ │ │ ├ Membership.mem
(link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)) x✝
38│ │ mem_link_supporters │ │ │ │ Iff
(Membership.mem (link_supporters st s t s_h t_h) x✝) (vote_msg st x✝ s t s_h t_h)
39│38,36 │ Iff.mp │ │ │ │ vote_msg
st x✝ s t s_h t_h
40│ │ mem_link_supporters │ │ │ │ Iff
(Membership.mem (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)) x✝)
(vote_msg st x✝ final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
41│40,37 │ Iff.mp │ │ │ │ vote_msg
st x✝ final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)
42│21,20 │ And.intro │ │ │ │ And
(LT.lt s_h final_h) (LT.lt (HAdd.hAdd final_h k) t_h)
43│41,42 │ And.intro │ │ │ │ And
(vote_msg st x✝ final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(And (LT.lt s_h final_h) (LT.lt (HAdd.hAdd final_h k) t_h))
44│39,43 │ And.intro │ │ │ │ And
(vote_msg st x✝ s t s_h t_h)
(And (vote_msg st x✝ final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(And (LT.lt s_h final_h) (LT.lt (HAdd.hAdd final_h k) t_h)))
45│44 │ Exists.intro │ │ │ │ Exists
fun (t₂_h : Nat) =>
And (vote_msg st x✝ s t s_h t_h)
(And (vote_msg st x✝ final (List.getLastD ls final) final_h t₂_h) (And (LT.lt s_h final_h) (LT.lt t₂_h t_h)))
46│45 │ Exists.intro │ │ │ │ Exists
fun (s₂_h : Nat) =>
Exists fun (t₂_h : Nat) =>
And (vote_msg st x✝ s t s_h t_h)
(And (vote_msg st x✝ final (List.getLastD ls final) s₂_h t₂_h) (And (LT.lt s_h s₂_h) (LT.lt t₂_h t_h)))
47│46 │ Exists.intro │ │ │ │ Exists
fun (t₂ : Hash) =>
Exists fun (s₂_h : Nat) =>
Exists fun (t₂_h : Nat) =>
And (vote_msg st x✝ s t s_h t_h) (And (vote_msg st x✝ final t₂ s₂_h t₂_h) (And (LT.lt s_h s₂_h) (LT.lt t₂_h t_h)))
48│47 │ Exists.intro │ │ │ │ Exists
fun (s₂ : Hash) =>
Exists fun (t₂ : Hash) =>
Exists fun (s₂_h : Nat) =>
Exists fun (t₂_h : Nat) =>
And (vote_msg st x✝ s t s_h t_h) (And (vote_msg st x✝ s₂ t₂ s₂_h t₂_h) (And (LT.lt s_h s₂_h) (LT.lt t₂_h t_h)))
49│48 │ Exists.intro │ │ │ │ Exists
fun (t₁_h : Nat) =>
Exists fun (s₂ : Hash) =>
Exists fun (t₂ : Hash) =>
Exists fun (s₂_h : Nat) =>
Exists fun (t₂_h : Nat) =>
And (vote_msg st x✝ s t s_h t₁_h)
(And (vote_msg st x✝ s₂ t₂ s₂_h t₂_h) (And (LT.lt s_h s₂_h) (LT.lt t₂_h t₁_h)))
50│49 │ Exists.intro │ │ │ │ Exists
fun (s₁_h : Nat) =>
Exists fun (t₁_h : Nat) =>
Exists fun (s₂ : Hash) =>
Exists fun (t₂ : Hash) =>
Exists fun (s₂_h : Nat) =>
Exists fun (t₂_h : Nat) =>
And (vote_msg st x✝ s t s₁_h t₁_h)
(And (vote_msg st x✝ s₂ t₂ s₂_h t₂_h) (And (LT.lt s₁_h s₂_h) (LT.lt t₂_h t₁_h)))
51│50 │ Exists.intro │ │ │ │ Exists
fun (t₁ : Hash) =>
Exists fun (s₁_h : Nat) =>
Exists fun (t₁_h : Nat) =>
Exists fun (s₂ : Hash) =>
Exists fun (t₂ : Hash) =>
Exists fun (s₂_h : Nat) =>
Exists fun (t₂_h : Nat) =>
And (vote_msg st x✝ s t₁ s₁_h t₁_h)
(And (vote_msg st x✝ s₂ t₂ s₂_h t₂_h) (And (LT.lt s₁_h s₂_h) (LT.lt t₂_h t₁_h)))
52│51 │ Exists.intro │ │ │ │ Exists
fun (s₁ : Hash) =>
Exists fun (t₁ : Hash) =>
Exists fun (s₁_h : Nat) =>
Exists fun (t₁_h : Nat) =>
Exists fun (s₂ : Hash) =>
Exists fun (t₂ : Hash) =>
Exists fun (s₂_h : Nat) =>
Exists fun (t₂_h : Nat) =>
And (vote_msg st x✝ s₁ t₁ s₁_h t₁_h)
(And (vote_msg st x✝ s₂ t₂ s₂_h t₂_h) (And (LT.lt s₁_h s₂_h) (LT.lt t₂_h t₁_h)))
53│52 │ Or.inr │ │ │ │ Or
(slashed_double_vote st x✝) (slashed_surround_vote st x✝)
54│35,36,37,53 │ ∀I │ │ │ ∀
(x : Validator),
Membership.mem (link_supporters st s t s_h t_h) x →
Membership.mem (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)) x →
Or (slashed_double_vote st x) (slashed_surround_vote st x)
55│30,54 │ And.intro │ │ │ And
(quorum_2 τ stake vset (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(List.getLastD ls final))
(∀ (v : Validator),
Membership.mem (link_supporters st s t s_h t_h) v →
Membership.mem (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)) v → slashed st v)
56│24,55 │ And.intro │ │ │ And
(quorum_2 τ stake vset (link_supporters st s t s_h t_h) t)
(And
(quorum_2 τ stake vset (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(List.getLastD ls final))
(∀ (v : Validator),
Membership.mem (link_supporters st s t s_h t_h) v →
Membership.mem (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)) v →
slashed st v))
57│33,56 │ And.intro │ │ │ And
(Subset (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(vset (List.getLastD ls final)))
(And (quorum_2 τ stake vset (link_supporters st s t s_h t_h) t)
(And
(quorum_2 τ stake vset (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(List.getLastD ls final))
(∀ (v : Validator),
Membership.mem (link_supporters st s t s_h t_h) v →
Membership.mem (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)) v →
slashed st v)))
58│31,57 │ And.intro │ │ │ And
(Subset (link_supporters st s t s_h t_h) (vset t))
(And
(Subset (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(vset (List.getLastD ls final)))
(And (quorum_2 τ stake vset (link_supporters st s t s_h t_h) t)
(And
(quorum_2 τ stake vset (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(List.getLastD ls final))
(∀ (v : Validator),
Membership.mem (link_supporters st s t s_h t_h) v →
Membership.mem (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)) v →
slashed st v))))
59│58 │ Exists.intro │ │ │ Exists
fun (qR : Finset Validator) =>
And (Subset (link_supporters st s t s_h t_h) (vset t))
(And (Subset qR (vset (List.getLastD ls final)))
(And (quorum_2 τ stake vset (link_supporters st s t s_h t_h) t)
(And (quorum_2 τ stake vset qR (List.getLastD ls final))
(∀ (v : Validator), Membership.mem (link_supporters st s t s_h t_h) v → Membership.mem qR v → slashed st v))))
60│59 │ Exists.intro │ │ │ Exists
fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset t))
(And (Subset qR (vset (List.getLastD ls final)))
(And (quorum_2 τ stake vset qL t)
(And (quorum_2 τ stake vset qR (List.getLastD ls final))
(∀ (v : Validator), Membership.mem qL v → Membership.mem qR v → slashed st v))))
61│60 │ Exists.intro │ │ │ Exists
fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset t))
(And (Subset qR (vset bR))
(And (quorum_2 τ stake vset qL t)
(And (quorum_2 τ stake vset qR bR)
(∀ (v : Validator), Membership.mem qL v → Membership.mem qR v → slashed st v))))
62│61 │ Exists.intro │ │ │ Exists
fun (bL : Hash) =>
Exists fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(And (quorum_2 τ stake vset qL bL)
(And (quorum_2 τ stake vset qR bR)
(∀ (v : Validator), Membership.mem qL v → Membership.mem qR v → slashed st v))))
63│31,32,33,34,62 │ ∀I │ │ Subset
(link_supporters st s t s_h t_h) (vset t) →
LE.le (Threshold.two_third τ (wt stake (vset t))) (wt stake (link_supporters st s t s_h t_h)) →
Subset (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(vset (List.getLastD ls final)) →
LE.le (Threshold.two_third τ (wt stake (vset (List.getLastD ls final))))
(wt stake (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))) →
Exists fun (bL : Hash) =>
Exists fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(And (quorum_2 τ stake vset qL bL)
(And (quorum_2 τ stake vset qR bR)
(∀ (v : Validator), Membership.mem qL v → Membership.mem qR v → slashed st v))))
64│24,30,63 │ k_slash_surround_full_containment.match_1 │ │ q_intersection_slashed
τ stake vset st
65│22,23,24,25,26,27,28,29,30,64 │ ∀I │ LT.lt
s_h t_h →
nth_ancestor parent (HSub.hSub t_h s_h) s t →
supermajority_link τ stake vset st s t s_h t_h →
LE.le (1 : Nat) k →
∀ (ls : List Hash),
Eq (List.length ls) (HAdd.hAdd k (1 : Nat)) →
Eq (List.headD ls final) final →
(∀ (n : Nat),
LE.le n k →
And (justified τ stake vset parent genesis st (List.getD ls n final) (HAdd.hAdd final_h n))
(nth_ancestor parent n final (List.getD ls n final))) →
supermajority_link τ stake vset st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k) →
q_intersection_slashed τ stake vset st
66│18,19,65 │ k_slash_surround_full_containment.match_2 │ q_intersection_slashed
τ stake vset st
67│0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,66│ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {s t final : Hash} {s_h t_h final_h k : Nat},
justification_link τ stake vset parent st s t s_h t_h →
k_finalized τ stake vset parent genesis st final final_h k →
LT.lt (HAdd.hAdd final_h k) t_h → LT.lt s_h final_h → q_intersection_slashed τ stake vset st
#detail_explode k_slash_surround_full_containmentk_slash_surround_full_containment : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator]
[inst_1 : DecidableEq Hash] [inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat)
(vset : Hash → Finset Validator) (parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash)
{s t final : Hash} {s_h t_h final_h k : Nat},
justification_link τ stake vset parent st s t s_h t_h →
k_finalized τ stake vset parent genesis st final final_h k →
LT.lt (HAdd.hAdd final_h k) t_h → LT.lt s_h final_h → q_intersection_slashed τ stake vset st
0 │ │ Validator ├ Type
u
1 │ │ Hash ├ Type
v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ s ├ Hash
12│ │ t ├ Hash
13│ │ final ├ Hash
14│ │ s_h ├ Nat
15│ │ t_h ├ Nat
16│ │ final_h ├ Nat
17│ │ k ├ Nat
18│ │ hlink_st ├ justification_link
τ stake vset parent st s t s_h t_h
19│ │ hfinal ├ k_finalized
τ stake vset parent genesis st final final_h k
20│ │ h_full ├ LT.lt
(HAdd.hAdd final_h k) t_h
21│ │ h_surround_start ├ LT.lt
s_h final_h
22│ │ left✝⁵ │ ┌ LT.lt
s_h t_h
23│ │ left✝⁴ │ ├ nth_ancestor
parent (HSub.hSub t_h s_h) s t
24│ │ hsm_outer │ ├ supermajority_link
τ stake vset st s t s_h t_h
25│ │ left✝³ │ ├ LE.le
(1 : Nat) k
26│ │ ls │ ├ List
Hash
27│ │ left✝² │ ├ Eq
(List.length ls) (HAdd.hAdd k (1 : Nat))
28│ │ left✝¹ │ ├ Eq
(List.headD ls final) final
29│ │ left✝ │ ├ ∀
(n : Nat),
LE.le n k →
And (justified τ stake vset parent genesis st (List.getD ls n final) (HAdd.hAdd final_h n))
(nth_ancestor parent n final (List.getD ls n final))
30│ │ hsm_inner │ ├ supermajority_link
τ stake vset st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)
31│ │ hsm_outer_sub │ │ ┌ Subset
(link_supporters st s t s_h t_h) (vset t)
32│ │ right✝¹ │ │ ├ LE.le
(Threshold.two_third τ (wt stake (vset t))) (wt stake (link_supporters st s t s_h t_h))
33│ │ hsm_inner_sub │ │ ├ Subset
(link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)) (vset (List.getLastD ls final))
34│ │ right✝ │ │ ├ LE.le
(Threshold.two_third τ (wt stake (vset (List.getLastD ls final))))
(wt stake (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)))
35│ │ x✝ │ │ │ ┌ Validator
36│ │ hvO │ │ │ ├ Membership.mem
(link_supporters st s t s_h t_h) x✝
37│ │ hvI │ │ │ ├ Membership.mem
(link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)) x✝
38│ │ mem_link_supporters │ │ │ │ Iff
(Membership.mem (link_supporters st s t s_h t_h) x✝) (vote_msg st x✝ s t s_h t_h)
39│38,36 │ Iff.mp │ │ │ │ vote_msg
st x✝ s t s_h t_h
40│ │ mem_link_supporters │ │ │ │ Iff
(Membership.mem (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)) x✝)
(vote_msg st x✝ final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
41│40,37 │ Iff.mp │ │ │ │ vote_msg
st x✝ final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)
42│21,20 │ And.intro │ │ │ │ And
(LT.lt s_h final_h) (LT.lt (HAdd.hAdd final_h k) t_h)
43│41,42 │ And.intro │ │ │ │ And
(vote_msg st x✝ final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(And (LT.lt s_h final_h) (LT.lt (HAdd.hAdd final_h k) t_h))
44│39,43 │ And.intro │ │ │ │ And
(vote_msg st x✝ s t s_h t_h)
(And (vote_msg st x✝ final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(And (LT.lt s_h final_h) (LT.lt (HAdd.hAdd final_h k) t_h)))
45│44 │ Exists.intro │ │ │ │ Exists
fun (t₂_h : Nat) =>
And (vote_msg st x✝ s t s_h t_h)
(And (vote_msg st x✝ final (List.getLastD ls final) final_h t₂_h) (And (LT.lt s_h final_h) (LT.lt t₂_h t_h)))
46│45 │ Exists.intro │ │ │ │ Exists
fun (s₂_h : Nat) =>
Exists fun (t₂_h : Nat) =>
And (vote_msg st x✝ s t s_h t_h)
(And (vote_msg st x✝ final (List.getLastD ls final) s₂_h t₂_h) (And (LT.lt s_h s₂_h) (LT.lt t₂_h t_h)))
47│46 │ Exists.intro │ │ │ │ Exists
fun (t₂ : Hash) =>
Exists fun (s₂_h : Nat) =>
Exists fun (t₂_h : Nat) =>
And (vote_msg st x✝ s t s_h t_h) (And (vote_msg st x✝ final t₂ s₂_h t₂_h) (And (LT.lt s_h s₂_h) (LT.lt t₂_h t_h)))
48│47 │ Exists.intro │ │ │ │ Exists
fun (s₂ : Hash) =>
Exists fun (t₂ : Hash) =>
Exists fun (s₂_h : Nat) =>
Exists fun (t₂_h : Nat) =>
And (vote_msg st x✝ s t s_h t_h) (And (vote_msg st x✝ s₂ t₂ s₂_h t₂_h) (And (LT.lt s_h s₂_h) (LT.lt t₂_h t_h)))
49│48 │ Exists.intro │ │ │ │ Exists
fun (t₁_h : Nat) =>
Exists fun (s₂ : Hash) =>
Exists fun (t₂ : Hash) =>
Exists fun (s₂_h : Nat) =>
Exists fun (t₂_h : Nat) =>
And (vote_msg st x✝ s t s_h t₁_h)
(And (vote_msg st x✝ s₂ t₂ s₂_h t₂_h) (And (LT.lt s_h s₂_h) (LT.lt t₂_h t₁_h)))
50│49 │ Exists.intro │ │ │ │ Exists
fun (s₁_h : Nat) =>
Exists fun (t₁_h : Nat) =>
Exists fun (s₂ : Hash) =>
Exists fun (t₂ : Hash) =>
Exists fun (s₂_h : Nat) =>
Exists fun (t₂_h : Nat) =>
And (vote_msg st x✝ s t s₁_h t₁_h)
(And (vote_msg st x✝ s₂ t₂ s₂_h t₂_h) (And (LT.lt s₁_h s₂_h) (LT.lt t₂_h t₁_h)))
51│50 │ Exists.intro │ │ │ │ Exists
fun (t₁ : Hash) =>
Exists fun (s₁_h : Nat) =>
Exists fun (t₁_h : Nat) =>
Exists fun (s₂ : Hash) =>
Exists fun (t₂ : Hash) =>
Exists fun (s₂_h : Nat) =>
Exists fun (t₂_h : Nat) =>
And (vote_msg st x✝ s t₁ s₁_h t₁_h)
(And (vote_msg st x✝ s₂ t₂ s₂_h t₂_h) (And (LT.lt s₁_h s₂_h) (LT.lt t₂_h t₁_h)))
52│51 │ Exists.intro │ │ │ │ Exists
fun (s₁ : Hash) =>
Exists fun (t₁ : Hash) =>
Exists fun (s₁_h : Nat) =>
Exists fun (t₁_h : Nat) =>
Exists fun (s₂ : Hash) =>
Exists fun (t₂ : Hash) =>
Exists fun (s₂_h : Nat) =>
Exists fun (t₂_h : Nat) =>
And (vote_msg st x✝ s₁ t₁ s₁_h t₁_h)
(And (vote_msg st x✝ s₂ t₂ s₂_h t₂_h) (And (LT.lt s₁_h s₂_h) (LT.lt t₂_h t₁_h)))
53│52 │ Or.inr │ │ │ │ Or
(slashed_double_vote st x✝) (slashed_surround_vote st x✝)
54│35,36,37,53 │ ∀I │ │ │ ∀
(x : Validator),
Membership.mem (link_supporters st s t s_h t_h) x →
Membership.mem (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)) x →
Or (slashed_double_vote st x) (slashed_surround_vote st x)
55│30,54 │ And.intro │ │ │ And
(quorum_2 τ stake vset (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(List.getLastD ls final))
(∀ (v : Validator),
Membership.mem (link_supporters st s t s_h t_h) v →
Membership.mem (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)) v → slashed st v)
56│24,55 │ And.intro │ │ │ And
(quorum_2 τ stake vset (link_supporters st s t s_h t_h) t)
(And
(quorum_2 τ stake vset (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(List.getLastD ls final))
(∀ (v : Validator),
Membership.mem (link_supporters st s t s_h t_h) v →
Membership.mem (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)) v →
slashed st v))
57│33,56 │ And.intro │ │ │ And
(Subset (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(vset (List.getLastD ls final)))
(And (quorum_2 τ stake vset (link_supporters st s t s_h t_h) t)
(And
(quorum_2 τ stake vset (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(List.getLastD ls final))
(∀ (v : Validator),
Membership.mem (link_supporters st s t s_h t_h) v →
Membership.mem (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)) v →
slashed st v)))
58│31,57 │ And.intro │ │ │ And
(Subset (link_supporters st s t s_h t_h) (vset t))
(And
(Subset (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(vset (List.getLastD ls final)))
(And (quorum_2 τ stake vset (link_supporters st s t s_h t_h) t)
(And
(quorum_2 τ stake vset (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(List.getLastD ls final))
(∀ (v : Validator),
Membership.mem (link_supporters st s t s_h t_h) v →
Membership.mem (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)) v →
slashed st v))))
59│58 │ Exists.intro │ │ │ Exists
fun (qR : Finset Validator) =>
And (Subset (link_supporters st s t s_h t_h) (vset t))
(And (Subset qR (vset (List.getLastD ls final)))
(And (quorum_2 τ stake vset (link_supporters st s t s_h t_h) t)
(And (quorum_2 τ stake vset qR (List.getLastD ls final))
(∀ (v : Validator), Membership.mem (link_supporters st s t s_h t_h) v → Membership.mem qR v → slashed st v))))
60│59 │ Exists.intro │ │ │ Exists
fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset t))
(And (Subset qR (vset (List.getLastD ls final)))
(And (quorum_2 τ stake vset qL t)
(And (quorum_2 τ stake vset qR (List.getLastD ls final))
(∀ (v : Validator), Membership.mem qL v → Membership.mem qR v → slashed st v))))
61│60 │ Exists.intro │ │ │ Exists
fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset t))
(And (Subset qR (vset bR))
(And (quorum_2 τ stake vset qL t)
(And (quorum_2 τ stake vset qR bR)
(∀ (v : Validator), Membership.mem qL v → Membership.mem qR v → slashed st v))))
62│61 │ Exists.intro │ │ │ Exists
fun (bL : Hash) =>
Exists fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(And (quorum_2 τ stake vset qL bL)
(And (quorum_2 τ stake vset qR bR)
(∀ (v : Validator), Membership.mem qL v → Membership.mem qR v → slashed st v))))
63│31,32,33,34,62 │ ∀I │ │ Subset
(link_supporters st s t s_h t_h) (vset t) →
LE.le (Threshold.two_third τ (wt stake (vset t))) (wt stake (link_supporters st s t s_h t_h)) →
Subset (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))
(vset (List.getLastD ls final)) →
LE.le (Threshold.two_third τ (wt stake (vset (List.getLastD ls final))))
(wt stake (link_supporters st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k))) →
Exists fun (bL : Hash) =>
Exists fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(And (quorum_2 τ stake vset qL bL)
(And (quorum_2 τ stake vset qR bR)
(∀ (v : Validator), Membership.mem qL v → Membership.mem qR v → slashed st v))))
64│24,30,63 │ k_slash_surround_full_containment.match_1 │ │ q_intersection_slashed
τ stake vset st
65│22,23,24,25,26,27,28,29,30,64 │ ∀I │ LT.lt
s_h t_h →
nth_ancestor parent (HSub.hSub t_h s_h) s t →
supermajority_link τ stake vset st s t s_h t_h →
LE.le (1 : Nat) k →
∀ (ls : List Hash),
Eq (List.length ls) (HAdd.hAdd k (1 : Nat)) →
Eq (List.headD ls final) final →
(∀ (n : Nat),
LE.le n k →
And (justified τ stake vset parent genesis st (List.getD ls n final) (HAdd.hAdd final_h n))
(nth_ancestor parent n final (List.getD ls n final))) →
supermajority_link τ stake vset st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k) →
q_intersection_slashed τ stake vset st
66│18,19,65 │ k_slash_surround_full_containment.match_2 │ q_intersection_slashed
τ stake vset st
67│0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,66│ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {s t final : Hash} {s_h t_h final_h k : Nat},
justification_link τ stake vset parent st s t s_h t_h →
k_finalized τ stake vset parent genesis st final final_h k →
LT.lt (HAdd.hAdd final_h k) t_h → LT.lt s_h final_h → q_intersection_slashed τ stake vset st
Statement
\operatorname{justified}(\sigma, s, h_s) \;\wedge\; \operatorname{justification\_link}(\sigma, s, t, h_s, h_t) \;\wedge\; \operatorname{k\_finalized}(\sigma, b, b_h, k) \;\wedge\; b_h < h_t \;\wedge\; \neg\,(b \xrightarrow{*} t) \;\wedge\; h_s < b_h \;\implies\; \operatorname{q\_intersection\_slashed}(\sigma)
Interpretation
Given a justified source s at height h_s < b_h, a
justification link from s to t at height h_t > b_h, a
k-finalized block b at height b_h, and
\neg\,(b \xrightarrow{*} t), produces a slashing witness.
This generalises k_slash_surround_full_containment to the
case where h_t may equal or fall within the finalization chain's
height range [b_h,\, b_h + k], not only above it. The three
sub-cases correspond to the three possible positions of h_t
relative to b_h + k.
Proof idea
First justify t via justified_link. Then case-split on
b_h + k vs h_t:
-
b_h + k < h_t: k_slash_surround_full_containment
produces a surround-vote witness.
-
b_h + k = h_t: extract the chain's last block via
k_finalized_last_justified. If t equals the last block,
then b \xrightarrow{*} t
(by nth_ancestor_ancestor), contradicting the non-ancestry
hypothesis. Otherwise two distinct blocks are justified at height
h_t = b_h + k, so
two_justified_same_height_slashed applies.
-
h_t < b_h + k: the chain's interior block at index
h_t - b_h is justified at height h_t
(from the chain's universal quantifier, transported via
Nat.add_sub_cancel'). If t equals this block, ancestry
b \xrightarrow{*} t contradicts the hypothesis; otherwise
two_justified_same_height_slashed applies.
theorem k_slash_surround_case_general
(τ : Threshold)
(stake : Validator → Nat)
(vset : Hash → Finset Validator)
(parent : HashParent Hash)
(genesis : Hash)
(st : State Validator Hash)
{s t final : Hash}
{s_h t_h final_h k : Nat}
(hjust_s : justified τ stake vset parent genesis st s s_h)
(hlink_st : justification_link τ stake vset parent st s t s_h t_h)
(hfinal : k_finalized τ stake vset parent genesis st final final_h k)
(hft : final_h < t_h)
(hnoans : ¬ hash_ancestor parent final t)
(hsf : s_h < final_h) :
q_intersection_slashed τ stake vset st :=
have hjust_t : justified τ stake vset parent genesis st t t_h :=
justified.justified_link hjust_s hlink_st
if hlt : final_h + k < t_h then
k_slash_surround_full_containment
τ stake vset parent genesis st hlink_st hfinal hlt hsf
else if heq : final_h + k = t_h then
match k_finalized_last_justified τ stake vset parent genesis st hfinal with
| ⟨last, hjust_last, hanc_last, _⟩ =>
if htlast : t = last then
False.elim (hnoans (match htlast with | rfl => nth_ancestor_ancestor hanc_last))
else
two_justified_same_height_slashed
τ stake vset parent genesis st hjust_t
(Eq.subst (motive := fun h => justified τ stake vset parent genesis st last h)
heq hjust_last) htlast
else
have hgt : t_h < final_h + k :=
Nat.lt_of_le_of_ne (Nat.le_of_not_lt hlt) (fun h => heq h.symm)
match hfinal with
| ⟨_, ls, _, _, hrel, _⟩ =>
have hhn : final_h + (t_h - final_h) = t_h :=
Nat.add_sub_cancel' (Nat.le_of_lt hft)
match hrel (t_h - final_h)
(Nat.sub_le_of_le_add
(Eq.subst (motive := fun x => t_h ≤ x)
(Nat.add_comm final_h k) (Nat.le_of_lt hgt))) with
| ⟨hj_mid, ha_mid⟩ =>
have hjust_mid : justified τ stake vset parent genesis st
(ls.getD (t_h - final_h) final) t_h :=
Eq.subst (motive := fun h =>
justified τ stake vset parent genesis st
(ls.getD (t_h - final_h) final) h)
hhn hj_mid
if htm : t = ls.getD (t_h - final_h) final then
False.elim (hnoans
(Eq.subst (motive := fun x => hash_ancestor parent final x)
htm.symm (nth_ancestor_ancestor ha_mid)))
else
two_justified_same_height_slashed
τ stake vset parent genesis st hjust_t hjust_mid htm
k_slash_surround_case_general : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator]
[inst_1 : DecidableEq Hash] [inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat)
(vset : Hash → Finset Validator) (parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash)
{s t final : Hash} {s_h t_h final_h k : Nat},
justified τ stake vset parent genesis st s s_h →
justification_link τ stake vset parent st s t s_h t_h →
k_finalized τ stake vset parent genesis st final final_h k →
LT.lt final_h t_h →
Not (hash_ancestor parent final t) → LT.lt s_h final_h → q_intersection_slashed τ stake vset st
0 │ │ Validator ├ Type
u
1 │ │ Hash ├ Type
v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ s ├ Hash
12│ │ t ├ Hash
13│ │ final ├ Hash
14│ │ s_h ├ Nat
15│ │ t_h ├ Nat
16│ │ final_h ├ Nat
17│ │ k ├ Nat
18│ │ hjust_s ├ justified
τ stake vset parent genesis st s s_h
19│ │ hlink_st ├ justification_link
τ stake vset parent st s t s_h t_h
20│ │ hfinal ├ k_finalized
τ stake vset parent genesis st final final_h k
21│ │ hft ├ LT.lt
final_h t_h
22│ │ hnoans ├ Not
(hash_ancestor parent final t)
23│ │ hsf ├ LT.lt
s_h final_h
24│18,19 │ justified.justified_link │ justified τ
stake vset parent genesis st t t_h
26│ │ hlt │ ┌ LT.lt
(HAdd.hAdd final_h k) t_h
27│19,20,26,23 │ k_slash_surround_full_containment │ │ q_intersection_slashed
τ stake vset st
28│26,27 │ ∀I │ LT.lt
(HAdd.hAdd final_h k) t_h →
q_intersection_slashed τ stake vset st
29│ │ hlt │ ┌ Not
(LT.lt (HAdd.hAdd final_h k) t_h)
30│ │ heq │ │ ┌ Eq
(HAdd.hAdd final_h k) t_h
31│20 │ k_finalized_last_justified │ │ │ Exists
fun (last : Hash) =>
And (justified τ stake vset parent genesis st last (HAdd.hAdd final_h k))
(And (nth_ancestor parent k final last)
(supermajority_link τ stake vset st final last final_h (HAdd.hAdd final_h k)))
32│ │ last │ │ │ ┌ Hash
33│ │ hjust_last │ │ │ ├ justified
τ stake vset parent genesis st last (HAdd.hAdd final_h k)
34│ │ hanc_last │ │ │ ├ nth_ancestor
parent k final last
35│ │ right✝ │ │ │ ├ supermajority_link
τ stake vset st final last final_h (HAdd.hAdd final_h k)
36│ │ htlast │ │ │ │ ┌ Eq
t last
37│ │ hjust_last │ │ │ │ │ ┌ justified
τ stake vset parent genesis st t (HAdd.hAdd final_h k)
38│ │ hanc_last │ │ │ │ │ ├ nth_ancestor
parent k final t
39│ │ right✝ │ │ │ │ │ ├ supermajority_link
τ stake vset st final t final_h (HAdd.hAdd final_h k)
40│38 │ nth_ancestor_ancestor │ │ │ │ │ │ hash_ancestor
parent final t
41│37,38,39,40 │ ∀I │ │ │ │ │ justified
τ stake vset parent genesis st t (HAdd.hAdd final_h k) →
nth_ancestor parent k final t →
supermajority_link τ stake vset st final t final_h (HAdd.hAdd final_h k) → hash_ancestor parent final t
42│36,33,34,35,41 │ k_slash_surround_case_general.match_1 │ │ │ │ │ hash_ancestor
parent final t
43│22,42 │ ∀E │ │ │ │ │ False
44│43 │ False.elim │ │ │ │ │ q_intersection_slashed
τ stake vset st
45│36,44 │ ∀I │ │ │ │ Eq
t last →
q_intersection_slashed τ stake vset st
46│ │ htlast │ │ │ │ ┌ Not
(Eq t last)
47│30,33 │ Eq.subst │ │ │ │ │ justified
τ stake vset parent genesis st last t_h
48│24,47,46 │ two_justified_same_height_slashed │ │ │ │ │ q_intersection_slashed
τ stake vset st
49│46,48 │ ∀I │ │ │ │ Not
(Eq t last) →
q_intersection_slashed τ stake vset st
50│45,49 │ dite │ │ │ │ q_intersection_slashed
τ stake vset st
51│32,33,34,35,50 │ ∀I │ │ │ ∀
(last : Hash),
justified τ stake vset parent genesis st last (HAdd.hAdd final_h k) →
nth_ancestor parent k final last →
supermajority_link τ stake vset st final last final_h (HAdd.hAdd final_h k) →
q_intersection_slashed τ stake vset st
52│31,51 │ k_slash_surround_case_general.match_2 │ │ │ q_intersection_slashed
τ stake vset st
53│30,52 │ ∀I │ │ Eq
(HAdd.hAdd final_h k) t_h →
q_intersection_slashed τ stake vset st
54│ │ heq │ │ ┌ Not
(Eq (HAdd.hAdd final_h k) t_h)
55│29 │ Nat.le_of_not_lt │ │ │ LE.le
t_h (HAdd.hAdd final_h k)
56│ │ h │ │ │ ┌ Eq
t_h (HAdd.hAdd final_h k)
57│56 │ Eq.symm │ │ │ │ Eq
(HAdd.hAdd final_h k) t_h
58│54,57 │ ∀E │ │ │ │ False
59│56,58 │ ∀I │ │ │ Eq
t_h (HAdd.hAdd final_h k) →
False
60│55,59 │ Nat.lt_of_le_of_ne │ │ │ LT.lt
t_h (HAdd.hAdd final_h k)
62│ │ left✝² │ │ │ ┌ LE.le
(1 : Nat) k
63│ │ ls │ │ │ ├ List
Hash
64│ │ left✝¹ │ │ │ ├ Eq
(List.length ls) (HAdd.hAdd k (1 : Nat))
65│ │ left✝ │ │ │ ├ Eq
(List.headD ls final) final
66│ │ hrel │ │ │ ├ ∀
(n : Nat),
LE.le n k →
And (justified τ stake vset parent genesis st (List.getD ls n final) (HAdd.hAdd final_h n))
(nth_ancestor parent n final (List.getD ls n final))
67│ │ right✝ │ │ │ ├ supermajority_link
τ stake vset st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)
68│21 │ Nat.le_of_lt │ │ │ │ LE.le
final_h t_h
69│68 │ Nat.add_sub_cancel' │ │ │ │ Eq
(HAdd.hAdd final_h (HSub.hSub t_h final_h)) t_h
71│ │ Nat.add_comm │ │ │ │ Eq
(HAdd.hAdd final_h k) (HAdd.hAdd k final_h)
72│60 │ Nat.le_of_lt │ │ │ │ LE.le
t_h (HAdd.hAdd final_h k)
73│71,72 │ Eq.subst │ │ │ │ LE.le
t_h (HAdd.hAdd k final_h)
74│73 │ Nat.sub_le_of_le_add │ │ │ │ LE.le
(HSub.hSub t_h final_h) k
75│66,74 │ ∀E │ │ │ │ And
(justified τ stake vset parent genesis st (List.getD ls (HSub.hSub t_h final_h) final)
(HAdd.hAdd final_h (HSub.hSub t_h final_h)))
(nth_ancestor parent (HSub.hSub t_h final_h) final (List.getD ls (HSub.hSub t_h final_h) final))
76│ │ hj_mid │ │ │ │ ┌ justified
τ stake vset parent genesis st (List.getD ls (HSub.hSub t_h final_h) final)
(HAdd.hAdd final_h (HSub.hSub t_h final_h))
77│ │ ha_mid │ │ │ │ ├ nth_ancestor
parent (HSub.hSub t_h final_h) final (List.getD ls (HSub.hSub t_h final_h) final)
78│69,76 │ Eq.subst │ │ │ │ │ justified
τ stake vset parent genesis st (List.getD ls (HSub.hSub t_h final_h) final) t_h
80│ │ htm │ │ │ │ │ ┌ Eq
t (List.getD ls (HSub.hSub t_h final_h) final)
81│80 │ Eq.symm │ │ │ │ │ │ Eq
(List.getD ls (HSub.hSub t_h final_h) final) t
82│77 │ nth_ancestor_ancestor │ │ │ │ │ │ hash_ancestor
parent final (List.getD ls (HSub.hSub t_h final_h) final)
83│81,82 │ Eq.subst │ │ │ │ │ │ hash_ancestor
parent final t
84│22,83 │ ∀E │ │ │ │ │ │ False
85│84 │ False.elim │ │ │ │ │ │ q_intersection_slashed
τ stake vset st
86│80,85 │ ∀I │ │ │ │ │ Eq
t (List.getD ls (HSub.hSub t_h final_h) final) →
q_intersection_slashed τ stake vset st
87│ │ htm │ │ │ │ │ ┌ Not
(Eq t (List.getD ls (HSub.hSub t_h final_h) final))
88│24,78,87 │ two_justified_same_height_slashed │ │ │ │ │ │ q_intersection_slashed
τ stake vset st
89│87,88 │ ∀I │ │ │ │ │ Not
(Eq t (List.getD ls (HSub.hSub t_h final_h) final)) →
q_intersection_slashed τ stake vset st
90│86,89 │ dite │ │ │ │ │ q_intersection_slashed
τ stake vset st
91│76,77,90 │ ∀I │ │ │ │ justified
τ stake vset parent genesis st (List.getD ls (HSub.hSub t_h final_h) final)
(HAdd.hAdd final_h (HSub.hSub t_h final_h)) →
nth_ancestor parent (HSub.hSub t_h final_h) final (List.getD ls (HSub.hSub t_h final_h) final) →
q_intersection_slashed τ stake vset st
92│75,91 │ k_slash_surround_case_general.match_3 │ │ │ │ q_intersection_slashed
τ stake vset st
93│62,63,64,65,66,67,92 │ ∀I │ │ │ LE.le
(1 : Nat) k →
∀ (ls : List Hash),
Eq (List.length ls) (HAdd.hAdd k (1 : Nat)) →
Eq (List.headD ls final) final →
(∀ (n : Nat),
LE.le n k →
And (justified τ stake vset parent genesis st (List.getD ls n final) (HAdd.hAdd final_h n))
(nth_ancestor parent n final (List.getD ls n final))) →
supermajority_link τ stake vset st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k) →
q_intersection_slashed τ stake vset st
94│20,93 │ k_slash_surround_case_general.match_4 │ │ │ q_intersection_slashed
τ stake vset st
95│54,94 │ ∀I │ │ Not
(Eq (HAdd.hAdd final_h k) t_h) →
q_intersection_slashed τ stake vset st
96│53,95 │ dite │ │ q_intersection_slashed
τ stake vset st
97│29,96 │ ∀I │ Not
(LT.lt (HAdd.hAdd final_h k) t_h) →
q_intersection_slashed τ stake vset st
98│28,97 │ dite │ q_intersection_slashed
τ stake vset st
99│0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,98│ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {s t final : Hash} {s_h t_h final_h k : Nat},
justified τ stake vset parent genesis st s s_h →
justification_link τ stake vset parent st s t s_h t_h →
k_finalized τ stake vset parent genesis st final final_h k →
LT.lt final_h t_h →
Not (hash_ancestor parent final t) → LT.lt s_h final_h → q_intersection_slashed τ stake vset st
#detail_explode k_slash_surround_case_generalk_slash_surround_case_general : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator]
[inst_1 : DecidableEq Hash] [inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat)
(vset : Hash → Finset Validator) (parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash)
{s t final : Hash} {s_h t_h final_h k : Nat},
justified τ stake vset parent genesis st s s_h →
justification_link τ stake vset parent st s t s_h t_h →
k_finalized τ stake vset parent genesis st final final_h k →
LT.lt final_h t_h →
Not (hash_ancestor parent final t) → LT.lt s_h final_h → q_intersection_slashed τ stake vset st
0 │ │ Validator ├ Type
u
1 │ │ Hash ├ Type
v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ s ├ Hash
12│ │ t ├ Hash
13│ │ final ├ Hash
14│ │ s_h ├ Nat
15│ │ t_h ├ Nat
16│ │ final_h ├ Nat
17│ │ k ├ Nat
18│ │ hjust_s ├ justified
τ stake vset parent genesis st s s_h
19│ │ hlink_st ├ justification_link
τ stake vset parent st s t s_h t_h
20│ │ hfinal ├ k_finalized
τ stake vset parent genesis st final final_h k
21│ │ hft ├ LT.lt
final_h t_h
22│ │ hnoans ├ Not
(hash_ancestor parent final t)
23│ │ hsf ├ LT.lt
s_h final_h
24│18,19 │ justified.justified_link │ justified τ
stake vset parent genesis st t t_h
26│ │ hlt │ ┌ LT.lt
(HAdd.hAdd final_h k) t_h
27│19,20,26,23 │ k_slash_surround_full_containment │ │ q_intersection_slashed
τ stake vset st
28│26,27 │ ∀I │ LT.lt
(HAdd.hAdd final_h k) t_h →
q_intersection_slashed τ stake vset st
29│ │ hlt │ ┌ Not
(LT.lt (HAdd.hAdd final_h k) t_h)
30│ │ heq │ │ ┌ Eq
(HAdd.hAdd final_h k) t_h
31│20 │ k_finalized_last_justified │ │ │ Exists
fun (last : Hash) =>
And (justified τ stake vset parent genesis st last (HAdd.hAdd final_h k))
(And (nth_ancestor parent k final last)
(supermajority_link τ stake vset st final last final_h (HAdd.hAdd final_h k)))
32│ │ last │ │ │ ┌ Hash
33│ │ hjust_last │ │ │ ├ justified
τ stake vset parent genesis st last (HAdd.hAdd final_h k)
34│ │ hanc_last │ │ │ ├ nth_ancestor
parent k final last
35│ │ right✝ │ │ │ ├ supermajority_link
τ stake vset st final last final_h (HAdd.hAdd final_h k)
36│ │ htlast │ │ │ │ ┌ Eq
t last
37│ │ hjust_last │ │ │ │ │ ┌ justified
τ stake vset parent genesis st t (HAdd.hAdd final_h k)
38│ │ hanc_last │ │ │ │ │ ├ nth_ancestor
parent k final t
39│ │ right✝ │ │ │ │ │ ├ supermajority_link
τ stake vset st final t final_h (HAdd.hAdd final_h k)
40│38 │ nth_ancestor_ancestor │ │ │ │ │ │ hash_ancestor
parent final t
41│37,38,39,40 │ ∀I │ │ │ │ │ justified
τ stake vset parent genesis st t (HAdd.hAdd final_h k) →
nth_ancestor parent k final t →
supermajority_link τ stake vset st final t final_h (HAdd.hAdd final_h k) → hash_ancestor parent final t
42│36,33,34,35,41 │ k_slash_surround_case_general.match_1 │ │ │ │ │ hash_ancestor
parent final t
43│22,42 │ ∀E │ │ │ │ │ False
44│43 │ False.elim │ │ │ │ │ q_intersection_slashed
τ stake vset st
45│36,44 │ ∀I │ │ │ │ Eq
t last →
q_intersection_slashed τ stake vset st
46│ │ htlast │ │ │ │ ┌ Not
(Eq t last)
47│30,33 │ Eq.subst │ │ │ │ │ justified
τ stake vset parent genesis st last t_h
48│24,47,46 │ two_justified_same_height_slashed │ │ │ │ │ q_intersection_slashed
τ stake vset st
49│46,48 │ ∀I │ │ │ │ Not
(Eq t last) →
q_intersection_slashed τ stake vset st
50│45,49 │ dite │ │ │ │ q_intersection_slashed
τ stake vset st
51│32,33,34,35,50 │ ∀I │ │ │ ∀
(last : Hash),
justified τ stake vset parent genesis st last (HAdd.hAdd final_h k) →
nth_ancestor parent k final last →
supermajority_link τ stake vset st final last final_h (HAdd.hAdd final_h k) →
q_intersection_slashed τ stake vset st
52│31,51 │ k_slash_surround_case_general.match_2 │ │ │ q_intersection_slashed
τ stake vset st
53│30,52 │ ∀I │ │ Eq
(HAdd.hAdd final_h k) t_h →
q_intersection_slashed τ stake vset st
54│ │ heq │ │ ┌ Not
(Eq (HAdd.hAdd final_h k) t_h)
55│29 │ Nat.le_of_not_lt │ │ │ LE.le
t_h (HAdd.hAdd final_h k)
56│ │ h │ │ │ ┌ Eq
t_h (HAdd.hAdd final_h k)
57│56 │ Eq.symm │ │ │ │ Eq
(HAdd.hAdd final_h k) t_h
58│54,57 │ ∀E │ │ │ │ False
59│56,58 │ ∀I │ │ │ Eq
t_h (HAdd.hAdd final_h k) →
False
60│55,59 │ Nat.lt_of_le_of_ne │ │ │ LT.lt
t_h (HAdd.hAdd final_h k)
62│ │ left✝² │ │ │ ┌ LE.le
(1 : Nat) k
63│ │ ls │ │ │ ├ List
Hash
64│ │ left✝¹ │ │ │ ├ Eq
(List.length ls) (HAdd.hAdd k (1 : Nat))
65│ │ left✝ │ │ │ ├ Eq
(List.headD ls final) final
66│ │ hrel │ │ │ ├ ∀
(n : Nat),
LE.le n k →
And (justified τ stake vset parent genesis st (List.getD ls n final) (HAdd.hAdd final_h n))
(nth_ancestor parent n final (List.getD ls n final))
67│ │ right✝ │ │ │ ├ supermajority_link
τ stake vset st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k)
68│21 │ Nat.le_of_lt │ │ │ │ LE.le
final_h t_h
69│68 │ Nat.add_sub_cancel' │ │ │ │ Eq
(HAdd.hAdd final_h (HSub.hSub t_h final_h)) t_h
71│ │ Nat.add_comm │ │ │ │ Eq
(HAdd.hAdd final_h k) (HAdd.hAdd k final_h)
72│60 │ Nat.le_of_lt │ │ │ │ LE.le
t_h (HAdd.hAdd final_h k)
73│71,72 │ Eq.subst │ │ │ │ LE.le
t_h (HAdd.hAdd k final_h)
74│73 │ Nat.sub_le_of_le_add │ │ │ │ LE.le
(HSub.hSub t_h final_h) k
75│66,74 │ ∀E │ │ │ │ And
(justified τ stake vset parent genesis st (List.getD ls (HSub.hSub t_h final_h) final)
(HAdd.hAdd final_h (HSub.hSub t_h final_h)))
(nth_ancestor parent (HSub.hSub t_h final_h) final (List.getD ls (HSub.hSub t_h final_h) final))
76│ │ hj_mid │ │ │ │ ┌ justified
τ stake vset parent genesis st (List.getD ls (HSub.hSub t_h final_h) final)
(HAdd.hAdd final_h (HSub.hSub t_h final_h))
77│ │ ha_mid │ │ │ │ ├ nth_ancestor
parent (HSub.hSub t_h final_h) final (List.getD ls (HSub.hSub t_h final_h) final)
78│69,76 │ Eq.subst │ │ │ │ │ justified
τ stake vset parent genesis st (List.getD ls (HSub.hSub t_h final_h) final) t_h
80│ │ htm │ │ │ │ │ ┌ Eq
t (List.getD ls (HSub.hSub t_h final_h) final)
81│80 │ Eq.symm │ │ │ │ │ │ Eq
(List.getD ls (HSub.hSub t_h final_h) final) t
82│77 │ nth_ancestor_ancestor │ │ │ │ │ │ hash_ancestor
parent final (List.getD ls (HSub.hSub t_h final_h) final)
83│81,82 │ Eq.subst │ │ │ │ │ │ hash_ancestor
parent final t
84│22,83 │ ∀E │ │ │ │ │ │ False
85│84 │ False.elim │ │ │ │ │ │ q_intersection_slashed
τ stake vset st
86│80,85 │ ∀I │ │ │ │ │ Eq
t (List.getD ls (HSub.hSub t_h final_h) final) →
q_intersection_slashed τ stake vset st
87│ │ htm │ │ │ │ │ ┌ Not
(Eq t (List.getD ls (HSub.hSub t_h final_h) final))
88│24,78,87 │ two_justified_same_height_slashed │ │ │ │ │ │ q_intersection_slashed
τ stake vset st
89│87,88 │ ∀I │ │ │ │ │ Not
(Eq t (List.getD ls (HSub.hSub t_h final_h) final)) →
q_intersection_slashed τ stake vset st
90│86,89 │ dite │ │ │ │ │ q_intersection_slashed
τ stake vset st
91│76,77,90 │ ∀I │ │ │ │ justified
τ stake vset parent genesis st (List.getD ls (HSub.hSub t_h final_h) final)
(HAdd.hAdd final_h (HSub.hSub t_h final_h)) →
nth_ancestor parent (HSub.hSub t_h final_h) final (List.getD ls (HSub.hSub t_h final_h) final) →
q_intersection_slashed τ stake vset st
92│75,91 │ k_slash_surround_case_general.match_3 │ │ │ │ q_intersection_slashed
τ stake vset st
93│62,63,64,65,66,67,92 │ ∀I │ │ │ LE.le
(1 : Nat) k →
∀ (ls : List Hash),
Eq (List.length ls) (HAdd.hAdd k (1 : Nat)) →
Eq (List.headD ls final) final →
(∀ (n : Nat),
LE.le n k →
And (justified τ stake vset parent genesis st (List.getD ls n final) (HAdd.hAdd final_h n))
(nth_ancestor parent n final (List.getD ls n final))) →
supermajority_link τ stake vset st final (List.getLastD ls final) final_h (HAdd.hAdd final_h k) →
q_intersection_slashed τ stake vset st
94│20,93 │ k_slash_surround_case_general.match_4 │ │ │ q_intersection_slashed
τ stake vset st
95│54,94 │ ∀I │ │ Not
(Eq (HAdd.hAdd final_h k) t_h) →
q_intersection_slashed τ stake vset st
96│53,95 │ dite │ │ q_intersection_slashed
τ stake vset st
97│29,96 │ ∀I │ Not
(LT.lt (HAdd.hAdd final_h k) t_h) →
q_intersection_slashed τ stake vset st
98│28,97 │ dite │ q_intersection_slashed
τ stake vset st
99│0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,98│ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {s t final : Hash} {s_h t_h final_h k : Nat},
justified τ stake vset parent genesis st s s_h →
justification_link τ stake vset parent st s t s_h t_h →
k_finalized τ stake vset parent genesis st final final_h k →
LT.lt final_h t_h →
Not (hash_ancestor parent final t) → LT.lt s_h final_h → q_intersection_slashed τ stake vset st
Non-equal-height case: strong induction on the height gap
Statement
\operatorname{justified}(\sigma, b_1, b_{1,h}) \;\wedge\; \operatorname{k\_finalized}(\sigma, b_2, b_{2,h}, k) \;\wedge\; \neg\,(b_2 \xrightarrow{*} b_1) \;\wedge\; b_{2,h} < b_{1,h} \;\implies\; \operatorname{q\_intersection\_slashed}(\sigma)
Interpretation
This is the inductive core of the safety argument: given a
justified block b_1 strictly above a k-finalized block
b_2 that is not its ancestor, trace b_1's justification
chain downward toward b_2. At each step the predecessor's
height is strictly smaller (since justification links are
forward), so the gap b_{1,h} - b_{2,h} strictly decreases.
The descent terminates in one of two base cases: if the
predecessor's height equals b_{2,h}, the equal-height case
(S1) applies; if it falls below b_{2,h}, the surround case
(S2) applies. The argument mirrors the "walking backwards along
supermajority links" in Gasper's proof of Lemma 5.1.
Proof idea
Strong induction on the gap b_{1,h} - b_{2,h} via
strong_induction_sub (offset k = b_{2,h}). Case-split
b_1's justification via justified_cases:
-
Genesis: height 0 < b_{2,h} is impossible.
-
Link from (s, h_s): the non-ancestry of b_2 propagates to
s via hash_ancestor_conflict. Then:
-
if h_s > b_{2,h}: the gap h_s - b_{2,h} < b_{1,h} - b_{2,h}
and the induction hypothesis applies to s;
-
if h_s = b_{2,h}: two_justified_same_height_slashed
on s and b_2;
-
if h_s < b_{2,h}: k_slash_surround_case_general on
the link (s, b_1) and the finalized b_2.
k_non_equal_height_case_ind : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator]
[inst_1 : DecidableEq Hash] [inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat)
(vset : Hash → Finset Validator) (parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash)
{b1 b2 : Hash} {b1_h b2_h k : Nat},
justified τ stake vset parent genesis st b1 b1_h →
k_finalized τ stake vset parent genesis st b2 b2_h k →
Not (hash_ancestor parent b2 b1) → LT.lt b2_h b1_h → q_intersection_slashed τ stake vset st
0 │ │ Validator ├ Type
u
1 │ │ Hash ├ Type
v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ b1 ├ Hash
12│ │ b2 ├ Hash
13│ │ b1_h ├ Nat
14│ │ b2_h ├ Nat
15│ │ k ├ Nat
16│ │ hb1j ├ justified
τ stake vset parent genesis st b1 b1_h
17│ │ hb2f ├ k_finalized
τ stake vset parent genesis st b2 b2_h k
18│ │ hconf ├ Not
(hash_ancestor parent b2 b1)
19│ │ hh ├ LT.lt
b2_h b1_h
20│ │ x✝¹ │ ┌ Nat
21│ │ x✝ │ ├ Hash
22│ │ IH │ ├ ∀
(v1a : Nat) (h1a : Hash),
LT.lt b2_h v1a →
LT.lt (HSub.hSub v1a b2_h) (HSub.hSub x✝¹ b2_h) →
justified τ stake vset parent genesis st h1a v1a →
k_finalized τ stake vset parent genesis st b2 b2_h k →
Not (hash_ancestor parent b2 h1a) → LT.lt b2_h v1a → q_intersection_slashed τ stake vset st
23│ │ hj1 │ ├ justified
τ stake vset parent genesis st x✝ x✝¹
24│ │ hb2f' │ ├ k_finalized
τ stake vset parent genesis st b2 b2_h k
25│ │ hconf1 │ ├ Not
(hash_ancestor parent b2 x✝)
26│ │ hh1 │ ├ LT.lt
b2_h x✝¹
27│23 │ justified_cases │ │ Or
(And (Eq x✝ genesis) (Eq x✝¹ (0 : Nat)))
(Exists fun (s : Hash) =>
Exists fun (s_h : Nat) =>
And (justified τ stake vset parent genesis st s s_h) (justification_link τ stake vset parent st s x✝ s_h x✝¹))
28│ │ x✝ │ │ ┌ And
(Eq x✝¹ genesis) (Eq x✝² (0 : Nat))
29│ │ left✝ │ │ │ ┌ Eq
x✝¹ genesis
30│ │ hh_zero │ │ │ ├ Eq
x✝² (0 : Nat)
31│ │ _ │ │ │ │ ┌ Unit
32│31,26 │ ∀I │ │ │ │ ∀
(_ : Unit), LT.lt b2_h x✝²
33│30,32 │ k_non_equal_height_case_ind.match_1 │ │ │ │ LT.lt b2_h
(0 : Nat)
34│33 │ Nat.not_lt_zero │ │ │ │ False
35│34 │ False.elim │ │ │ │ q_intersection_slashed
τ stake vset st
36│29,30,35 │ ∀I │ │ │ Eq
x✝¹ genesis →
Eq x✝² (0 : Nat) → q_intersection_slashed τ stake vset st
37│28,36 │ k_non_equal_height_case_ind.match_2 │ │ │ q_intersection_slashed
τ stake vset st
38│28,37 │ ∀I │ │ And
(Eq x✝¹ genesis) (Eq x✝² (0 : Nat)) →
q_intersection_slashed τ stake vset st
39│ │ x✝ │ │ ┌ Exists
fun (s : Hash) =>
Exists fun (s_h : Nat) =>
And (justified τ stake vset parent genesis st s s_h) (justification_link τ stake vset parent st s x✝¹ s_h x✝²)
40│ │ s │ │ │ ┌ Hash
41│ │ s_h │ │ │ ├ Nat
42│ │ hsj │ │ │ ├ justified
τ stake vset parent genesis st s s_h
43│ │ hlink │ │ │ ├ justification_link
τ stake vset parent st s x✝¹ s_h x✝²
44│ │ hlink_lt │ │ │ │ ┌ LT.lt
s_h x✝²
45│ │ hlink_nth │ │ │ │ ├ nth_ancestor
parent (HSub.hSub x✝² s_h) s x✝¹
46│ │ right✝ │ │ │ │ ├ supermajority_link
τ stake vset st s x✝¹ s_h x✝²
47│45 │ nth_ancestor_ancestor │ │ │ │ │ hash_ancestor
parent s x✝¹
48│47,25 │ hash_ancestor_conflict │ │ │ │ │ Not
(hash_ancestor parent b2 s)
50│ │ hlt │ │ │ │ │ ┌ LT.lt
b2_h s_h
51│50 │ Nat.le_of_lt │ │ │ │ │ │ LE.le
b2_h s_h
52│51,44 │ Nat.sub_lt_sub_right │ │ │ │ │ │ LT.lt
(HSub.hSub s_h b2_h) (HSub.hSub x✝² b2_h)
53│22,50,52,42,24,48,50 │ ∀E │ │ │ │ │ │ q_intersection_slashed
τ stake vset st
54│50,53 │ ∀I │ │ │ │ │ LT.lt
b2_h s_h →
q_intersection_slashed τ stake vset st
55│ │ hlt │ │ │ │ │ ┌ Not
(LT.lt b2_h s_h)
56│ │ heq │ │ │ │ │ │ ┌ Eq
b2_h s_h
57│24 │ k_finalized_means_justified │ │ │ │ │ │ │ justified τ
stake vset parent genesis st b2 b2_h
58│56,57 │ Eq.subst │ │ │ │ │ │ │ justified
τ stake vset parent genesis st b2 s_h
59│ │ hs │ │ │ │ │ │ │ ┌ Eq
s b2
60│ │ hash_ancestor.refl │ │ │ │ │ │ │ │ hash_ancestor
parent s s
61│59,60 │ Eq.subst │ │ │ │ │ │ │ │ hash_ancestor
parent b2 s
62│48,61 │ ∀E │ │ │ │ │ │ │ │ False
63│62 │ False.elim │ │ │ │ │ │ │ │ False
64│59,63 │ ∀I │ │ │ │ │ │ │ Eq
s b2 →
False
65│42,58,64 │ two_justified_same_height_slashed │ │ │ │ │ │ │ q_intersection_slashed
τ stake vset st
66│56,65 │ ∀I │ │ │ │ │ │ Eq
b2_h s_h →
q_intersection_slashed τ stake vset st
67│ │ heq │ │ │ │ │ │ ┌ Not
(Eq b2_h s_h)
68│55 │ Nat.le_of_not_lt │ │ │ │ │ │ │ LE.le
s_h b2_h
69│ │ h │ │ │ │ │ │ │ ┌ Eq
s_h b2_h
70│69 │ Eq.symm │ │ │ │ │ │ │ │ Eq
b2_h s_h
71│67,70 │ ∀E │ │ │ │ │ │ │ │ False
72│69,71 │ ∀I │ │ │ │ │ │ │ Eq
s_h b2_h →
False
73│68,72 │ Nat.lt_of_le_of_ne │ │ │ │ │ │ │ LT.lt
s_h b2_h
74│42,43,24,26,25,73 │ k_slash_surround_case_general │ │ │ │ │ │ │ q_intersection_slashed
τ stake vset st
75│67,74 │ ∀I │ │ │ │ │ │ Not
(Eq b2_h s_h) →
q_intersection_slashed τ stake vset st
76│66,75 │ dite │ │ │ │ │ │ q_intersection_slashed
τ stake vset st
77│55,76 │ ∀I │ │ │ │ │ Not
(LT.lt b2_h s_h) →
q_intersection_slashed τ stake vset st
78│54,77 │ dite │ │ │ │ │ q_intersection_slashed
τ stake vset st
79│44,45,46,78 │ ∀I │ │ │ │ LT.lt
s_h x✝² →
nth_ancestor parent (HSub.hSub x✝² s_h) s x✝¹ →
supermajority_link τ stake vset st s x✝¹ s_h x✝² → q_intersection_slashed τ stake vset st
80│43,79 │ k_non_equal_height_case_ind.match_3 │ │ │ │ q_intersection_slashed
τ stake vset st
81│40,41,42,43,80 │ ∀I │ │ │ ∀
(s : Hash) (s_h : Nat),
justified τ stake vset parent genesis st s s_h →
justification_link τ stake vset parent st s x✝¹ s_h x✝² → q_intersection_slashed τ stake vset st
82│39,81 │ k_non_equal_height_case_ind.match_4 │ │ │ q_intersection_slashed
τ stake vset st
83│39,82 │ ∀I │ │ (Exists
fun (s : Hash) =>
Exists fun (s_h : Nat) =>
And (justified τ stake vset parent genesis st s s_h) (justification_link τ stake vset parent st s x✝¹ s_h x✝²)) →
q_intersection_slashed τ stake vset st
84│27,38,83 │ Or.elim │ │ q_intersection_slashed
τ stake vset st
85│20,21,22,23,24,25,26,84 │ ∀I │ ∀
(x : Nat) (x_1 : Hash),
(∀ (v1a : Nat) (h1a : Hash),
LT.lt b2_h v1a →
LT.lt (HSub.hSub v1a b2_h) (HSub.hSub x b2_h) →
justified τ stake vset parent genesis st h1a v1a →
k_finalized τ stake vset parent genesis st b2 b2_h k →
Not (hash_ancestor parent b2 h1a) → LT.lt b2_h v1a → q_intersection_slashed τ stake vset st) →
justified τ stake vset parent genesis st x_1 x →
k_finalized τ stake vset parent genesis st b2 b2_h k →
Not (hash_ancestor parent b2 x_1) → LT.lt b2_h x → q_intersection_slashed τ stake vset st
86│85,16,17,18,19 │ strong_induction_sub │ q_intersection_slashed τ
stake vset st
87│0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,86│ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {b1 b2 : Hash} {b1_h b2_h k : Nat},
justified τ stake vset parent genesis st b1 b1_h →
k_finalized τ stake vset parent genesis st b2 b2_h k →
Not (hash_ancestor parent b2 b1) → LT.lt b2_h b1_h → q_intersection_slashed τ stake vset st
#detail_explode k_non_equal_height_case_indk_non_equal_height_case_ind : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator]
[inst_1 : DecidableEq Hash] [inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat)
(vset : Hash → Finset Validator) (parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash)
{b1 b2 : Hash} {b1_h b2_h k : Nat},
justified τ stake vset parent genesis st b1 b1_h →
k_finalized τ stake vset parent genesis st b2 b2_h k →
Not (hash_ancestor parent b2 b1) → LT.lt b2_h b1_h → q_intersection_slashed τ stake vset st
0 │ │ Validator ├ Type
u
1 │ │ Hash ├ Type
v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ b1 ├ Hash
12│ │ b2 ├ Hash
13│ │ b1_h ├ Nat
14│ │ b2_h ├ Nat
15│ │ k ├ Nat
16│ │ hb1j ├ justified
τ stake vset parent genesis st b1 b1_h
17│ │ hb2f ├ k_finalized
τ stake vset parent genesis st b2 b2_h k
18│ │ hconf ├ Not
(hash_ancestor parent b2 b1)
19│ │ hh ├ LT.lt
b2_h b1_h
20│ │ x✝¹ │ ┌ Nat
21│ │ x✝ │ ├ Hash
22│ │ IH │ ├ ∀
(v1a : Nat) (h1a : Hash),
LT.lt b2_h v1a →
LT.lt (HSub.hSub v1a b2_h) (HSub.hSub x✝¹ b2_h) →
justified τ stake vset parent genesis st h1a v1a →
k_finalized τ stake vset parent genesis st b2 b2_h k →
Not (hash_ancestor parent b2 h1a) → LT.lt b2_h v1a → q_intersection_slashed τ stake vset st
23│ │ hj1 │ ├ justified
τ stake vset parent genesis st x✝ x✝¹
24│ │ hb2f' │ ├ k_finalized
τ stake vset parent genesis st b2 b2_h k
25│ │ hconf1 │ ├ Not
(hash_ancestor parent b2 x✝)
26│ │ hh1 │ ├ LT.lt
b2_h x✝¹
27│23 │ justified_cases │ │ Or
(And (Eq x✝ genesis) (Eq x✝¹ (0 : Nat)))
(Exists fun (s : Hash) =>
Exists fun (s_h : Nat) =>
And (justified τ stake vset parent genesis st s s_h) (justification_link τ stake vset parent st s x✝ s_h x✝¹))
28│ │ x✝ │ │ ┌ And
(Eq x✝¹ genesis) (Eq x✝² (0 : Nat))
29│ │ left✝ │ │ │ ┌ Eq
x✝¹ genesis
30│ │ hh_zero │ │ │ ├ Eq
x✝² (0 : Nat)
31│ │ _ │ │ │ │ ┌ Unit
32│31,26 │ ∀I │ │ │ │ ∀
(_ : Unit), LT.lt b2_h x✝²
33│30,32 │ k_non_equal_height_case_ind.match_1 │ │ │ │ LT.lt b2_h
(0 : Nat)
34│33 │ Nat.not_lt_zero │ │ │ │ False
35│34 │ False.elim │ │ │ │ q_intersection_slashed
τ stake vset st
36│29,30,35 │ ∀I │ │ │ Eq
x✝¹ genesis →
Eq x✝² (0 : Nat) → q_intersection_slashed τ stake vset st
37│28,36 │ k_non_equal_height_case_ind.match_2 │ │ │ q_intersection_slashed
τ stake vset st
38│28,37 │ ∀I │ │ And
(Eq x✝¹ genesis) (Eq x✝² (0 : Nat)) →
q_intersection_slashed τ stake vset st
39│ │ x✝ │ │ ┌ Exists
fun (s : Hash) =>
Exists fun (s_h : Nat) =>
And (justified τ stake vset parent genesis st s s_h) (justification_link τ stake vset parent st s x✝¹ s_h x✝²)
40│ │ s │ │ │ ┌ Hash
41│ │ s_h │ │ │ ├ Nat
42│ │ hsj │ │ │ ├ justified
τ stake vset parent genesis st s s_h
43│ │ hlink │ │ │ ├ justification_link
τ stake vset parent st s x✝¹ s_h x✝²
44│ │ hlink_lt │ │ │ │ ┌ LT.lt
s_h x✝²
45│ │ hlink_nth │ │ │ │ ├ nth_ancestor
parent (HSub.hSub x✝² s_h) s x✝¹
46│ │ right✝ │ │ │ │ ├ supermajority_link
τ stake vset st s x✝¹ s_h x✝²
47│45 │ nth_ancestor_ancestor │ │ │ │ │ hash_ancestor
parent s x✝¹
48│47,25 │ hash_ancestor_conflict │ │ │ │ │ Not
(hash_ancestor parent b2 s)
50│ │ hlt │ │ │ │ │ ┌ LT.lt
b2_h s_h
51│50 │ Nat.le_of_lt │ │ │ │ │ │ LE.le
b2_h s_h
52│51,44 │ Nat.sub_lt_sub_right │ │ │ │ │ │ LT.lt
(HSub.hSub s_h b2_h) (HSub.hSub x✝² b2_h)
53│22,50,52,42,24,48,50 │ ∀E │ │ │ │ │ │ q_intersection_slashed
τ stake vset st
54│50,53 │ ∀I │ │ │ │ │ LT.lt
b2_h s_h →
q_intersection_slashed τ stake vset st
55│ │ hlt │ │ │ │ │ ┌ Not
(LT.lt b2_h s_h)
56│ │ heq │ │ │ │ │ │ ┌ Eq
b2_h s_h
57│24 │ k_finalized_means_justified │ │ │ │ │ │ │ justified τ
stake vset parent genesis st b2 b2_h
58│56,57 │ Eq.subst │ │ │ │ │ │ │ justified
τ stake vset parent genesis st b2 s_h
59│ │ hs │ │ │ │ │ │ │ ┌ Eq
s b2
60│ │ hash_ancestor.refl │ │ │ │ │ │ │ │ hash_ancestor
parent s s
61│59,60 │ Eq.subst │ │ │ │ │ │ │ │ hash_ancestor
parent b2 s
62│48,61 │ ∀E │ │ │ │ │ │ │ │ False
63│62 │ False.elim │ │ │ │ │ │ │ │ False
64│59,63 │ ∀I │ │ │ │ │ │ │ Eq
s b2 →
False
65│42,58,64 │ two_justified_same_height_slashed │ │ │ │ │ │ │ q_intersection_slashed
τ stake vset st
66│56,65 │ ∀I │ │ │ │ │ │ Eq
b2_h s_h →
q_intersection_slashed τ stake vset st
67│ │ heq │ │ │ │ │ │ ┌ Not
(Eq b2_h s_h)
68│55 │ Nat.le_of_not_lt │ │ │ │ │ │ │ LE.le
s_h b2_h
69│ │ h │ │ │ │ │ │ │ ┌ Eq
s_h b2_h
70│69 │ Eq.symm │ │ │ │ │ │ │ │ Eq
b2_h s_h
71│67,70 │ ∀E │ │ │ │ │ │ │ │ False
72│69,71 │ ∀I │ │ │ │ │ │ │ Eq
s_h b2_h →
False
73│68,72 │ Nat.lt_of_le_of_ne │ │ │ │ │ │ │ LT.lt
s_h b2_h
74│42,43,24,26,25,73 │ k_slash_surround_case_general │ │ │ │ │ │ │ q_intersection_slashed
τ stake vset st
75│67,74 │ ∀I │ │ │ │ │ │ Not
(Eq b2_h s_h) →
q_intersection_slashed τ stake vset st
76│66,75 │ dite │ │ │ │ │ │ q_intersection_slashed
τ stake vset st
77│55,76 │ ∀I │ │ │ │ │ Not
(LT.lt b2_h s_h) →
q_intersection_slashed τ stake vset st
78│54,77 │ dite │ │ │ │ │ q_intersection_slashed
τ stake vset st
79│44,45,46,78 │ ∀I │ │ │ │ LT.lt
s_h x✝² →
nth_ancestor parent (HSub.hSub x✝² s_h) s x✝¹ →
supermajority_link τ stake vset st s x✝¹ s_h x✝² → q_intersection_slashed τ stake vset st
80│43,79 │ k_non_equal_height_case_ind.match_3 │ │ │ │ q_intersection_slashed
τ stake vset st
81│40,41,42,43,80 │ ∀I │ │ │ ∀
(s : Hash) (s_h : Nat),
justified τ stake vset parent genesis st s s_h →
justification_link τ stake vset parent st s x✝¹ s_h x✝² → q_intersection_slashed τ stake vset st
82│39,81 │ k_non_equal_height_case_ind.match_4 │ │ │ q_intersection_slashed
τ stake vset st
83│39,82 │ ∀I │ │ (Exists
fun (s : Hash) =>
Exists fun (s_h : Nat) =>
And (justified τ stake vset parent genesis st s s_h) (justification_link τ stake vset parent st s x✝¹ s_h x✝²)) →
q_intersection_slashed τ stake vset st
84│27,38,83 │ Or.elim │ │ q_intersection_slashed
τ stake vset st
85│20,21,22,23,24,25,26,84 │ ∀I │ ∀
(x : Nat) (x_1 : Hash),
(∀ (v1a : Nat) (h1a : Hash),
LT.lt b2_h v1a →
LT.lt (HSub.hSub v1a b2_h) (HSub.hSub x b2_h) →
justified τ stake vset parent genesis st h1a v1a →
k_finalized τ stake vset parent genesis st b2 b2_h k →
Not (hash_ancestor parent b2 h1a) → LT.lt b2_h v1a → q_intersection_slashed τ stake vset st) →
justified τ stake vset parent genesis st x_1 x →
k_finalized τ stake vset parent genesis st b2 b2_h k →
Not (hash_ancestor parent b2 x_1) → LT.lt b2_h x → q_intersection_slashed τ stake vset st
86│85,16,17,18,19 │ strong_induction_sub │ q_intersection_slashed τ
stake vset st
87│0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,86│ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {b1 b2 : Hash} {b1_h b2_h k : Nat},
justified τ stake vset parent genesis st b1 b1_h →
k_finalized τ stake vset parent genesis st b2 b2_h k →
Not (hash_ancestor parent b2 b1) → LT.lt b2_h b1_h → q_intersection_slashed τ stake vset st
Non-equal-height case: lifting from justified to k-finalized
Statement
\operatorname{k\_finalized}(\sigma, b_1, b_{1,h}, k_1) \;\wedge\; \operatorname{k\_finalized}(\sigma, b_2, b_{2,h}, k_2) \;\wedge\; \neg\,(b_2 \xrightarrow{*} b_1) \;\wedge\; b_{2,h} < b_{1,h} \;\implies\; \operatorname{q\_intersection\_slashed}(\sigma)
Interpretation
The version of the non-equal-height case where both blocks are
k-finalized (not merely justified). The asymmetry in the
height condition b_{2,h} < b_{1,h} is absorbed by k_safety',
which handles the symmetric case by swapping the two blocks.
Proof idea
Extract b_1's justification from its k-finalization via
k_finalized_means_justified, then delegate to
k_non_equal_height_case_ind with the justified b_1 and
the k-finalized b_2.
Role in the development
The b_{2,h} < b_{1,h} and b_{1,h} < b_{2,h} branches of
k_safety' both route through this lemma (the latter after
swapping b_1 \leftrightarrow b_2).
k_non_equal_height_case : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator]
[inst_1 : DecidableEq Hash] [inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat)
(vset : Hash → Finset Validator) (parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash)
{b1 b2 : Hash} {b1_h b2_h k1 k2 : Nat},
k_finalized τ stake vset parent genesis st b1 b1_h k1 →
k_finalized τ stake vset parent genesis st b2 b2_h k2 →
Not (hash_ancestor parent b2 b1) → LT.lt b2_h b1_h → q_intersection_slashed τ stake vset st
0 │ │ Validator ├ Type u
1 │ │ Hash ├ Type v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ b1 ├ Hash
12│ │ b2 ├ Hash
13│ │ b1_h ├ Nat
14│ │ b2_h ├ Nat
15│ │ k1 ├ Nat
16│ │ k2 ├ Nat
17│ │ hb1f ├ k_finalized
τ stake vset parent genesis st b1 b1_h k1
18│ │ hb2f ├ k_finalized
τ stake vset parent genesis st b2 b2_h k2
19│ │ hconf ├ Not
(hash_ancestor parent b2 b1)
20│ │ hh ├ LT.lt
b2_h b1_h
21│17 │ k_finalized_means_justified │ justified τ stake vset parent
genesis st b1 b1_h
22│21,18,19,20 │ k_non_equal_height_case_ind │ q_intersection_slashed τ stake
vset st
23│0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,22│ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {b1 b2 : Hash} {b1_h b2_h k1 k2 : Nat},
k_finalized τ stake vset parent genesis st b1 b1_h k1 →
k_finalized τ stake vset parent genesis st b2 b2_h k2 →
Not (hash_ancestor parent b2 b1) → LT.lt b2_h b1_h → q_intersection_slashed τ stake vset st
#detail_explode k_non_equal_height_casek_non_equal_height_case : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator]
[inst_1 : DecidableEq Hash] [inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat)
(vset : Hash → Finset Validator) (parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash)
{b1 b2 : Hash} {b1_h b2_h k1 k2 : Nat},
k_finalized τ stake vset parent genesis st b1 b1_h k1 →
k_finalized τ stake vset parent genesis st b2 b2_h k2 →
Not (hash_ancestor parent b2 b1) → LT.lt b2_h b1_h → q_intersection_slashed τ stake vset st
0 │ │ Validator ├ Type u
1 │ │ Hash ├ Type v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ b1 ├ Hash
12│ │ b2 ├ Hash
13│ │ b1_h ├ Nat
14│ │ b2_h ├ Nat
15│ │ k1 ├ Nat
16│ │ k2 ├ Nat
17│ │ hb1f ├ k_finalized
τ stake vset parent genesis st b1 b1_h k1
18│ │ hb2f ├ k_finalized
τ stake vset parent genesis st b2 b2_h k2
19│ │ hconf ├ Not
(hash_ancestor parent b2 b1)
20│ │ hh ├ LT.lt
b2_h b1_h
21│17 │ k_finalized_means_justified │ justified τ stake vset parent
genesis st b1 b1_h
22│21,18,19,20 │ k_non_equal_height_case_ind │ q_intersection_slashed τ stake
vset st
23│0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,22│ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {b1 b2 : Hash} {b1_h b2_h k1 k2 : Nat},
k_finalized τ stake vset parent genesis st b1 b1_h k1 →
k_finalized τ stake vset parent genesis st b2 b2_h k2 →
Not (hash_ancestor parent b2 b1) → LT.lt b2_h b1_h → q_intersection_slashed τ stake vset st
k-safety: two k-finalized mutual non-ancestors force slashing
Statement
\operatorname{k\_finalized}(\sigma, b_1, b_{1,h}, k_1) \;\wedge\; \operatorname{k\_finalized}(\sigma, b_2, b_{2,h}, k_2) \;\wedge\; \neg\,(b_2 \xrightarrow{*} b_1) \;\wedge\; \neg\,(b_1 \xrightarrow{*} b_2) \;\implies\; \operatorname{q\_intersection\_slashed}(\sigma)
Assumptions
-
two k-finalized blocks (b_1, b_{1,h}, k_1) and
(b_2, b_{2,h}, k_2) in the same state \sigma;
-
mutual non-ancestry: \neg\,(b_2 \xrightarrow{*} b_1) and
\neg\,(b_1 \xrightarrow{*} b_2).
No good_votes, no QuorumContext — the justification
derivations carried by the k-finalized hypotheses already encode
the required supermajority links.
Proof idea
Three-way case split on b_{1,h} vs b_{2,h}:
-
b_{1,h} = b_{2,h}: transport b_2's finalization to height
b_{1,h} via Eq.subst, derive b_1 \ne b_2 from
\neg\,(b_1 \xrightarrow{*} b_2) via
hash_nonancestor_nonequal, then apply
k_equal_height_case.
-
b_{2,h} < b_{1,h}: k_non_equal_height_case.
-
b_{1,h} < b_{2,h}: symmetric application of
k_non_equal_height_case with the two blocks swapped.
Role in the development
The core of the safety proof, consumed by
k_accountable_safety and ultimately by
accountable_safety.
k_safety' : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {b1 b2 : Hash} {b1_h b2_h k1 k2 : Nat},
k_finalized τ stake vset parent genesis st b1 b1_h k1 →
k_finalized τ stake vset parent genesis st b2 b2_h k2 →
Not (hash_ancestor parent b2 b1) → Not (hash_ancestor parent b1 b2) → q_intersection_slashed τ stake vset st
0 │ │ Validator ├ Type u
1 │ │ Hash ├ Type v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ b1 ├ Hash
12│ │ b2 ├ Hash
13│ │ b1_h ├ Nat
14│ │ b2_h ├ Nat
15│ │ k1 ├ Nat
16│ │ k2 ├ Nat
17│ │ hb1f ├ k_finalized
τ stake vset parent genesis st b1 b1_h k1
18│ │ hb2f ├ k_finalized
τ stake vset parent genesis st b2 b2_h k2
19│ │ hconf1 ├ Not
(hash_ancestor parent b2 b1)
20│ │ hconf2 ├ Not
(hash_ancestor parent b1 b2)
21│ │ heq │ ┌ Eq b1_h
b2_h
22│21 │ Eq.symm │ │ Eq b2_h
b1_h
23│22,18 │ Eq.subst │ │ k_finalized
τ stake vset parent genesis st b2 b1_h k2
24│20 │ hash_nonancestor_nonequal │ │ Ne b1 b2
25│17,23,24 │ k_equal_height_case │ │ q_intersection_slashed τ stake
vset st
26│21,25 │ ∀I │ Eq b1_h
b2_h →
q_intersection_slashed τ stake vset st
27│ │ heq │ ┌ Not
(Eq b1_h b2_h)
28│ │ hgt │ │ ┌ LT.lt
b2_h b1_h
29│17,18,19,28 │ k_non_equal_height_case │ │ │ q_intersection_slashed τ
stake vset st
30│28,29 │ ∀I │ │ LT.lt
b2_h b1_h →
q_intersection_slashed τ stake vset st
31│ │ hgt │ │ ┌ Not
(LT.lt b2_h b1_h)
32│31 │ Nat.le_of_not_lt │ │ │ LE.le
b1_h b2_h
33│32,27 │ Nat.lt_of_le_of_ne │ │ │ LT.lt
b1_h b2_h
34│18,17,20,33 │ k_non_equal_height_case │ │ │ q_intersection_slashed τ
stake vset st
35│31,34 │ ∀I │ │ Not
(LT.lt b2_h b1_h) →
q_intersection_slashed τ stake vset st
36│30,35 │ dite │ │ q_intersection_slashed
τ stake vset st
37│27,36 │ ∀I │ Not
(Eq b1_h b2_h) →
q_intersection_slashed τ stake vset st
38│26,37 │ dite │ q_intersection_slashed
τ stake vset st
39│0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,38│ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {b1 b2 : Hash} {b1_h b2_h k1 k2 : Nat},
k_finalized τ stake vset parent genesis st b1 b1_h k1 →
k_finalized τ stake vset parent genesis st b2 b2_h k2 →
Not (hash_ancestor parent b2 b1) → Not (hash_ancestor parent b1 b2) → q_intersection_slashed τ stake vset st
#detail_explode k_safety'k_safety' : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {b1 b2 : Hash} {b1_h b2_h k1 k2 : Nat},
k_finalized τ stake vset parent genesis st b1 b1_h k1 →
k_finalized τ stake vset parent genesis st b2 b2_h k2 →
Not (hash_ancestor parent b2 b1) → Not (hash_ancestor parent b1 b2) → q_intersection_slashed τ stake vset st
0 │ │ Validator ├ Type u
1 │ │ Hash ├ Type v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ b1 ├ Hash
12│ │ b2 ├ Hash
13│ │ b1_h ├ Nat
14│ │ b2_h ├ Nat
15│ │ k1 ├ Nat
16│ │ k2 ├ Nat
17│ │ hb1f ├ k_finalized
τ stake vset parent genesis st b1 b1_h k1
18│ │ hb2f ├ k_finalized
τ stake vset parent genesis st b2 b2_h k2
19│ │ hconf1 ├ Not
(hash_ancestor parent b2 b1)
20│ │ hconf2 ├ Not
(hash_ancestor parent b1 b2)
21│ │ heq │ ┌ Eq b1_h
b2_h
22│21 │ Eq.symm │ │ Eq b2_h
b1_h
23│22,18 │ Eq.subst │ │ k_finalized
τ stake vset parent genesis st b2 b1_h k2
24│20 │ hash_nonancestor_nonequal │ │ Ne b1 b2
25│17,23,24 │ k_equal_height_case │ │ q_intersection_slashed τ stake
vset st
26│21,25 │ ∀I │ Eq b1_h
b2_h →
q_intersection_slashed τ stake vset st
27│ │ heq │ ┌ Not
(Eq b1_h b2_h)
28│ │ hgt │ │ ┌ LT.lt
b2_h b1_h
29│17,18,19,28 │ k_non_equal_height_case │ │ │ q_intersection_slashed τ
stake vset st
30│28,29 │ ∀I │ │ LT.lt
b2_h b1_h →
q_intersection_slashed τ stake vset st
31│ │ hgt │ │ ┌ Not
(LT.lt b2_h b1_h)
32│31 │ Nat.le_of_not_lt │ │ │ LE.le
b1_h b2_h
33│32,27 │ Nat.lt_of_le_of_ne │ │ │ LT.lt
b1_h b2_h
34│18,17,20,33 │ k_non_equal_height_case │ │ │ q_intersection_slashed τ
stake vset st
35│31,34 │ ∀I │ │ Not
(LT.lt b2_h b1_h) →
q_intersection_slashed τ stake vset st
36│30,35 │ dite │ │ q_intersection_slashed
τ stake vset st
37│27,36 │ ∀I │ Not
(Eq b1_h b2_h) →
q_intersection_slashed τ stake vset st
38│26,37 │ dite │ q_intersection_slashed
τ stake vset st
39│0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,38│ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {b1 b2 : Hash} {b1_h b2_h k1 k2 : Nat},
k_finalized τ stake vset parent genesis st b1 b1_h k1 →
k_finalized τ stake vset parent genesis st b2 b2_h k2 →
Not (hash_ancestor parent b2 b1) → Not (hash_ancestor parent b1 b2) → q_intersection_slashed τ stake vset st
Statement
\operatorname{k\_finalization\_fork}(\sigma, k_1, k_2) \;\implies\; \operatorname{q\_intersection\_slashed}(\sigma)
Interpretation
The existential wrapper around k_safety': given a
k-finalization fork (two k-finalized blocks with mutual
non-ancestry, packed as an existential), produces the slashing
witness. This converts the bundled fork into the unbundled
hypotheses that k_safety' consumes.
Proof idea
Destruct the fork existential to obtain the two blocks
b_1, b_2, their heights b_{1,h}, b_{2,h}, the two
k-finalization hypotheses, and the mutual non-ancestry
conditions. Pass all six components directly to k_safety'.
theorem k_accountable_safety
(τ : Threshold)
(stake : Validator → Nat)
(vset : Hash → Finset Validator)
(parent : HashParent Hash)
(genesis : Hash)
(st : State Validator Hash)
{k1 k2 : Nat}
(hfork : k_finalization_fork τ stake vset parent genesis st k1 k2) :
q_intersection_slashed τ stake vset st :=
match hfork with
| ⟨_, _, _, _, hb1f, hb2f, hc1, hc2⟩ =>
k_safety' τ stake vset parent genesis st hb1f hb2f hc1 hc2
k_accountable_safety : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {k1 k2 : Nat},
k_finalization_fork τ stake vset parent genesis st k1 k2 → q_intersection_slashed τ stake vset st
0 │ │ Validator ├ Type u
1 │ │ Hash ├ Type v
2 │ │ inst✝² ├ DecidableEq Validator
3 │ │ inst✝¹ ├ DecidableEq Hash
4 │ │ inst✝ ├ Fintype Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator → Nat
7 │ │ vset ├ Hash → Finset Validator
8 │ │ parent ├ HashParent Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State Validator Hash
11│ │ k1 ├ Nat
12│ │ k2 ├ Nat
13│ │ hfork ├ k_finalization_fork τ stake
vset parent genesis st k1 k2
14│ │ w✝³ │ ┌ Hash
15│ │ w✝² │ ├ Nat
16│ │ w✝¹ │ ├ Hash
17│ │ w✝ │ ├ Nat
18│ │ hb1f │ ├ k_finalized τ stake vset
parent genesis st w✝³ w✝² k1
19│ │ hb2f │ ├ k_finalized τ stake vset
parent genesis st w✝¹ w✝ k2
20│ │ hc1 │ ├ Not
(hash_ancestor parent w✝¹ w✝³)
21│ │ hc2 │ ├ Not
(hash_ancestor parent w✝³ w✝¹)
22│18,19,20,21 │ k_safety' │ │ q_intersection_slashed τ stake vset st
23│14,15,16,17,18,19,20,21,22 │ ∀I │ ∀ (w : Hash) (w_1 : Nat)
(w_2 : Hash) (w_3 : Nat),
k_finalized τ stake vset parent genesis st w w_1 k1 →
k_finalized τ stake vset parent genesis st w_2 w_3 k2 →
Not (hash_ancestor parent w_2 w) → Not (hash_ancestor parent w w_2) → q_intersection_slashed τ stake vset st
24│13,23 │ k_accountable_safety.match_1 │ q_intersection_slashed τ stake vset st
25│0,1,2,3,4,5,6,7,8,9,10,11,12,13,24│ ∀I │ ∀ {Validator : Type u}
{Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash] [inst_2 : Fintype Validator]
(τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator) (parent : HashParent Hash) (genesis : Hash)
(st : State Validator Hash) {k1 k2 : Nat},
k_finalization_fork τ stake vset parent genesis st k1 k2 → q_intersection_slashed τ stake vset st
#detail_explode k_accountable_safetyk_accountable_safety : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) {k1 k2 : Nat},
k_finalization_fork τ stake vset parent genesis st k1 k2 → q_intersection_slashed τ stake vset st
0 │ │ Validator ├ Type u
1 │ │ Hash ├ Type v
2 │ │ inst✝² ├ DecidableEq Validator
3 │ │ inst✝¹ ├ DecidableEq Hash
4 │ │ inst✝ ├ Fintype Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator → Nat
7 │ │ vset ├ Hash → Finset Validator
8 │ │ parent ├ HashParent Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State Validator Hash
11│ │ k1 ├ Nat
12│ │ k2 ├ Nat
13│ │ hfork ├ k_finalization_fork τ stake
vset parent genesis st k1 k2
14│ │ w✝³ │ ┌ Hash
15│ │ w✝² │ ├ Nat
16│ │ w✝¹ │ ├ Hash
17│ │ w✝ │ ├ Nat
18│ │ hb1f │ ├ k_finalized τ stake vset
parent genesis st w✝³ w✝² k1
19│ │ hb2f │ ├ k_finalized τ stake vset
parent genesis st w✝¹ w✝ k2
20│ │ hc1 │ ├ Not
(hash_ancestor parent w✝¹ w✝³)
21│ │ hc2 │ ├ Not
(hash_ancestor parent w✝³ w✝¹)
22│18,19,20,21 │ k_safety' │ │ q_intersection_slashed τ stake vset st
23│14,15,16,17,18,19,20,21,22 │ ∀I │ ∀ (w : Hash) (w_1 : Nat)
(w_2 : Hash) (w_3 : Nat),
k_finalized τ stake vset parent genesis st w w_1 k1 →
k_finalized τ stake vset parent genesis st w_2 w_3 k2 →
Not (hash_ancestor parent w_2 w) → Not (hash_ancestor parent w w_2) → q_intersection_slashed τ stake vset st
24│13,23 │ k_accountable_safety.match_1 │ q_intersection_slashed τ stake vset st
25│0,1,2,3,4,5,6,7,8,9,10,11,12,13,24│ ∀I │ ∀ {Validator : Type u}
{Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash] [inst_2 : Fintype Validator]
(τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator) (parent : HashParent Hash) (genesis : Hash)
(st : State Validator Hash) {k1 k2 : Nat},
k_finalization_fork τ stake vset parent genesis st k1 k2 → q_intersection_slashed τ stake vset st
Accountable safety (main theorem)
Statement
\operatorname{finalization\_fork}(\sigma) \;\implies\; \operatorname{q\_intersection\_slashed}(\sigma)
Interpretation
The formal counterpart of Casper FFG's Theorem 1 (Accountable
Safety): if two conflicting blocks are both finalized — i.e. the
protocol has committed to two incompatible histories — then there
exist two \frac{2}{3}-quorums whose shared members have all
violated a slashing condition and can therefore be held
accountable (their deposits destroyed). The word "accountable"
is the key: the theorem does not merely assert that honest
validators would not create a fork, but that if a fork occurs,
provable evidence exists to identify and punish the responsible
validators.
Proof idea
Convert the finalization_fork to a
same_k_finalization_fork at k = 1 via
finalization_fork_means_same_finalization_fork_one, then
apply k_accountable_safety.
Assumptions
Only the fork hypothesis hfork — no good_votes,
no QuorumContext, no block-tree axioms beyond those already
encoded in the justification derivations that the fork carries.
Non-assumptions
This theorem does not assert that the slashed intersection is
nonempty (that is the quantitative half in
Theories/SlashableBound.lean). It asserts that every
validator in the intersection is slashed.
accountable_safety : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash),
finalization_fork τ stake vset parent genesis st → q_intersection_slashed τ stake vset st
0 │ │ Validator ├ Type u
1 │ │ Hash ├ Type v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ hfork ├ finalization_fork
τ stake vset parent genesis st
12│ │ finalization_fork_means_same_finalization_fork_one │ Iff
(finalization_fork τ stake vset parent genesis st) (same_k_finalization_fork τ stake vset parent genesis st (1 : Nat))
13│12,11 │ Iff.mp │ same_k_finalization_fork
τ stake vset parent genesis st (1 : Nat)
14│13 │ k_accountable_safety │ q_intersection_slashed τ stake
vset st
15│0,1,2,3,4,5,6,7,8,9,10,11,14│ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash),
finalization_fork τ stake vset parent genesis st → q_intersection_slashed τ stake vset st
#detail_explode accountable_safetyaccountable_safety : ∀ {Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash),
finalization_fork τ stake vset parent genesis st → q_intersection_slashed τ stake vset st
0 │ │ Validator ├ Type u
1 │ │ Hash ├ Type v
2 │ │ inst✝² ├ DecidableEq
Validator
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ hfork ├ finalization_fork
τ stake vset parent genesis st
12│ │ finalization_fork_means_same_finalization_fork_one │ Iff
(finalization_fork τ stake vset parent genesis st) (same_k_finalization_fork τ stake vset parent genesis st (1 : Nat))
13│12,11 │ Iff.mp │ same_k_finalization_fork
τ stake vset parent genesis st (1 : Nat)
14│13 │ k_accountable_safety │ q_intersection_slashed τ stake
vset st
15│0,1,2,3,4,5,6,7,8,9,10,11,14│ ∀I │ ∀
{Validator : Type u} {Hash : Type v} [inst : DecidableEq Validator] [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash),
finalization_fork τ stake vset parent genesis st → q_intersection_slashed τ stake vset st