**Question:** What should be the precise assumption here. Is the invariant on $h.V$ or on $h.NextV$ or both?
*Assumption:* If a header is properly generated, then the above equations hold.
### Liveness
*Draft:* If a header $h$ as been properly generated by the blockchain (and its age is less than the trusting period), then a correct LightClient will eventually set $trust(h) = true$.
## High Level Solution
Upon initialization, the LightClient is given a header *inithead* it trusts by
social consensus. It is assumed that *inithead* satisfies the LightClient
Invariant.
When a LightClients sees a new header it has to decide whether to trust the new
header. Trust can be obtained by (possibly) the combination of two methods.
1.**an uninterrupted sequence of proof.** If a block is appended to the chain, where the last block
is trusted (and properly committed by the old validator set in the next block),
and the new block contains a new validator set, the new block is trusted if the LightClient knows all headers in the prefix.
Intuitively, a trusted validator set is assumed to not chose a new validator set
that violates the fault assumption.
2.**trusting period.** Based on a trusted block *h*, and the LightClient
Invariant, which ensures the fault assumption during the trusting period, we can
try to infer wether it is guaranteed that the validator set of the new block
contains > 2/3 correct voting power. If such a validator set commits a block, we
can trust it, as these processes have been continuously correct by the
**Theorem 1.** If for all potential adversaries PA, in $nh$ the combined voting
powers of PA and UV is less than a third of the total voting power, then in
$nh$, more than 2/3 of the voting power is held by correct processes. Formally,
if for all PA
\[
\sum_{(v,old) \in PA \wedge \\ (v,p) \in nh.V} p + \sum_{(v,p) \in UV} p <1/3
\sum_{(v,p) \in nh.V} p,
\]
then
\[
\sum_{(v,p) \in nh.V \wedge \\correct(v,oh.bfttime + tp)} p > 2/3 \sum_{(v,p) \in h.V} p
\]
*Proof.* By the definition of PA, Proposition 1, and the LightClient invariant.
By Assumption 3, there is sufficient voting power to trust the new validator set. (And thus the validator set it signs in that block, for which the $tp$ starts at the $bfttime$ of the header).
Below, we thus sketch a function that checks whether the premise of Theorem 1 holds. If the results is positive, we can trust $nh$, otherwise not.
### An Algorithm
In pseudo go...
```go
func CheckVS(oh, nh) bool {
if oh.bfttime + unbonding_period <now{//Observation1
return false // old header was once trusted but it is expired
}
PAs := compute_all_PAs(oh) // Definition 1
PAs := reduce (PAs) // remove every PA that is a subset of another PA
UV := compute_UV(oh,nh) // Definition 2
vpUV := votingpower(UV,nh) // second sum in Theorem 1
vpNH := votingpower(nh.V,nh) // right hand side of premise of Theorem 1
vpMaxPA := maximumvotingpower(PAs,nh) // voting powers of all PA and big max
**Remark.** Computing all PAs might be too expensive (all subsets of $oh.V$ that have a certain combined voting power in oh). Similarly, we then have to compute all voting powers of PAs in nh to get the maximum. This is disturbing, as right now, based on the examples, I expect that CheckVS will mostly return false, assuming that there are frequent changes in the validator sets. However, $oh.V=nh.V$ might be the common case.
**To Do.** The current invariant assumes that the 1/3 fault assumption is always satisfied. If this is not the case, and there is slashing, etc., we should write the spec of the fault assumptions with temporary violations. Cf. fork accountability, slashing, "counter factual signing" etc.
