tendermint/spec/light-client/verification.md

# Core Verification

## Problem statement

We assume that the light client knows a (base) header `inithead` it trusts (by social consensus or because
the light client has decided to trust the header before). The goal is to check whether another header
`newhead` can be trusted based on the data in `inithead`.

The correctness of the protocol is based on the assumption that `inithead` was generated by an instance of
Tendermint consensus.

### Failure Model

For the purpose of the following definitions we assume that there exists a function
`validators` that returns the corresponding validator set for the given hash.

The light client protocol is defined with respect to the following failure model:

Given a known bound `TRUSTED_PERIOD`, and a block `b` with header `h` generated at time `Time`
(i.e. `h.Time = Time`), a set of validators that hold more than 2/3 of the voting power
in `validators(b.Header.NextValidatorsHash)` is correct until time `b.Header.Time + TRUSTED_PERIOD`.

*Assumption*: "correct" is defined w.r.t. realtime (some Newtonian global notion of time, i.e., wall time),
while `Header.Time` corresponds to the [BFT time](../consensus/bft-time.md). In this note, we assume that clocks of correct processes
are synchronized (for example using NTP), and therefore there is bounded clock drift (`CLOCK_DRIFT`) between local clocks and
BFT time. More precisely, for every correct light client process and every `header.Time` (i.e. BFT Time, for a header correctly
generated by the Tendermint consensus), the following inequality holds: `Header.Time < now + CLOCK_DRIFT`,
where `now` corresponds to the system clock at the light client process.

Furthermore, we assume that `TRUSTED_PERIOD` is (several) order of magnitude bigger than `CLOCK_DRIFT` (`TRUSTED_PERIOD >> CLOCK_DRIFT`),
as `CLOCK_DRIFT` (using NTP) is in the order of milliseconds and `TRUSTED_PERIOD` is in the order of weeks.

We expect a light client process defined in this document to be used in the context in which there is some
larger period during which misbehaving validators can be detected and punished (we normally refer to it as `UNBONDING_PERIOD`
due to the "bonding" mechanism in modern proof of stake systems). Furthermore, we assume that
`TRUSTED_PERIOD < UNBONDING_PERIOD` and that they are normally of the same order of magnitude, for example
`TRUSTED_PERIOD = UNBONDING_PERIOD / 2`.

The specification in this document considers an implementation of the light client under the Failure Model defined above.
Mechanisms like `fork accountability` and `evidence submission` are defined in the context of `UNBONDING_PERIOD` and
they incentivize validators to follow the protocol specification defined in this document. If they don't,
and we have 1/3 (or more) faulty validators, safety may be violated. Our approach then is
to *detect* these cases (after the fact), and take suitable repair actions (automatic and social).
This is discussed in document on [Fork accountability](./accountability.md).

The term "trusted" above indicates that the correctness of the protocol depends on
this assumption. It is in the responsibility of the user that runs the light client to make sure that the risk
of trusting a corrupted/forged `inithead` is negligible.

*Remark*: This failure model might change to a hybrid version that takes heights into account in the future.

### High Level Solution

Upon initialization, the light client is given a header `inithead` it trusts (by
social consensus). When a light clients sees a new signed header `snh`, it has to decide whether to trust the new
header. Trust can be obtained by (possibly) the combination of three methods.

1. **Uninterrupted sequence of headers.** Given a trusted header `h` and an untrusted header `h1`,
the light client trusts a header `h1` if it trusts all headers in between `h` and `h1`.

2. **Trusted period.** Given a trusted header `h`, an untrusted header `h1 > h` and `TRUSTED_PERIOD` during which
the failure model holds, we can check whether at least one validator, that has been continuously correct
from `h.Time` until now, has signed `h1`. If this is the case, we can trust `h1`.

3. **Bisection.** If a check according to 2. (trusted period) fails, the light client can try to
obtain a header `hp` whose height lies between `h` and `h1` in order to check whether `h` can be used to
get trust for `hp`, and `hp` can be used to get trust for `snh`. If this is the case we can trust `h1`;
if not, we continue recursively until either we found set of headers that can build (transitively) trust relation
between `h` and `h1`, or we failed as two consecutive headers don't verify against each other.

## Definitions

### Data structures

In the following, only the details of the data structures needed for this specification are given.

 ```go
   type Header struct {
        Height               int64
        Time                 Time          // the chain time when the header (block) was generated

        LastBlockID          BlockID       // prev block info
        ValidatorsHash       []byte        // hash of the validators for the current block
        NextValidatorsHash   []byte        // hash of the validators for the next block
   }

   type SignedHeader struct {
        Header        Header
        Commit        Commit            // commit for the given header
   }

   type ValidatorSet struct {
        Validators         []Validator
        TotalVotingPower   int64
   }

   type Validator struct {
        Address       Address           // validator address (we assume validator's addresses are unique)
        VotingPower   int64             // validator's voting power
   }

   type TrustedState {
        SignedHeader   SignedHeader
        ValidatorSet   ValidatorSet
   }
 ```

### Functions

For the purpose of this light client specification, we assume that the Tendermint Full Node
exposes the following functions over Tendermint RPC:

```go
    // returns signed header: Header with Commit, for the given height
    func Commit(height int64) (SignedHeader, error)

    // returns validator set for the given height
    func Validators(height int64) (ValidatorSet, error)
```

Furthermore, we assume the following auxiliary functions:

```go
    // returns true if the commit is for the header, ie. if it contains
    // the correct hash of the header; otherwise false
    func matchingCommit(header Header, commit Commit) bool

    // returns the set of validators from the given validator set that
    // committed the block (that correctly signed the block)
    // it assumes signature verification so it can be computationally expensive
    func signers(commit Commit, validatorSet ValidatorSet) []Validator

    // returns the voting power the validators in v1 have according to their voting power in set v2
    // it does not assume signature verification
    func votingPowerIn(v1 []Validator, v2 ValidatorSet) int64

    // returns hash of the given validator set
    func hash(v2 ValidatorSet) []byte
```

In the functions below we will be using `trustThreshold` as a parameter. For simplicity
we assume that `trustThreshold` is a float between `1/3` and `2/3` and we will not be checking it
in the pseudo-code.

**VerifySingle.** The function `VerifySingle` attempts to validate given untrusted header and the corresponding validator sets
based on a given trusted state. It ensures that the trusted state is still within its trusted period,
and that the untrusted header is within assumed `clockDrift` bound of the passed time `now`.
Note that this function is not making external (RPC) calls to the full node; the whole logic is
based on the local (given) state. This function is supposed to be used by the IBC handlers.

```go
func VerifySingle(untrustedSh SignedHeader,
                  untrustedVs ValidatorSet,
                  untrustedNextVs ValidatorSet,
                  trustedState TrustedState,
                  trustThreshold float,
                  trustingPeriod Duration,
                  clockDrift Duration,
                  now Time) (TrustedState, error) {

    if untrustedSh.Header.Time > now + clockDrift {
        return (trustedState, ErrInvalidHeaderTime)
    }

    trustedHeader = trustedState.SignedHeader.Header
    if !isWithinTrustedPeriod(trustedHeader, trustingPeriod, now) {
        return (state, ErrHeaderNotWithinTrustedPeriod)
    }

    // we assume that time it takes to execute verifySingle function
    // is several order of magnitudes smaller than trustingPeriod
    error = verifySingle(
                trustedState,
                untrustedSh,
                untrustedVs,
                untrustedNextVs,
                trustThreshold)

    if error != nil return (state, error)

    // the untrusted header is now trusted
    newTrustedState = TrustedState(untrustedSh, untrustedNextVs)
    return (newTrustedState, nil)
}

// return true if header is within its light client trusted period; otherwise returns false
func isWithinTrustedPeriod(header Header,
                           trustingPeriod Duration,
                           now Time) bool {

    return header.Time + trustedPeriod > now
}
```

Note that in case `VerifySingle` returns without an error (untrusted header
is successfully verified) then we have a guarantee that the transition of the trust
from `trustedState` to `newTrustedState` happened during the trusted period of
`trustedState.SignedHeader.Header`.

TODO: Explain what happens in case `VerifySingle` returns with an error.

**verifySingle.** The function `verifySingle` verifies a single untrusted header
against a given trusted state. It includes all validations and signature verification.
It is not publicly exposed since it does not check for header expiry (time constraints)
and hence it's possible to use it incorrectly.

```go
func verifySingle(trustedState TrustedState,
                  untrustedSh SignedHeader,
                  untrustedVs ValidatorSet,
                  untrustedNextVs ValidatorSet,
                  trustThreshold float) error {

    untrustedHeader = untrustedSh.Header
    untrustedCommit = untrustedSh.Commit

    trustedHeader = trustedState.SignedHeader.Header
    trustedVs = trustedState.ValidatorSet

    if trustedHeader.Height >= untrustedHeader.Height return ErrNonIncreasingHeight
    if trustedHeader.Time >= untrustedHeader.Time return ErrNonIncreasingTime

    // validate the untrusted header against its commit, vals, and next_vals
    error = validateSignedHeaderAndVals(untrustedSh, untrustedVs, untrustedNextVs)
    if error != nil return error

    // check for adjacent headers
    if untrustedHeader.Height == trustedHeader.Height + 1 {
        if trustedHeader.NextValidatorsHash != untrustedHeader.ValidatorsHash {
            return ErrInvalidAdjacentHeaders
        }
    } else {
        error = verifyCommitTrusting(trustedVs, untrustedCommit, untrustedVs, trustThreshold)
        if error != nil return error
    }

    // verify the untrusted commit
    return verifyCommitFull(untrustedVs, untrustedCommit)
}

// returns nil if header and validator sets are consistent; otherwise returns error
func validateSignedHeaderAndVals(signedHeader SignedHeader, vs ValidatorSet, nextVs ValidatorSet) error {
    header = signedHeader.Header
    if hash(vs) != header.ValidatorsHash return ErrInvalidValidatorSet
    if hash(nextVs) != header.NextValidatorsHash return ErrInvalidNextValidatorSet
    if !matchingCommit(header, signedHeader.Commit) return ErrInvalidCommitValue
    return nil
}

// returns nil if at least single correst signer signed the commit; otherwise returns error
func verifyCommitTrusting(trustedVs ValidatorSet,
                          commit Commit,
                          untrustedVs ValidatorSet,
                          trustLevel float) error {

    totalPower := trustedVs.TotalVotingPower
    signedPower := votingPowerIn(signers(commit, untrustedVs), trustedVs)

    // check that the signers account for more than max(1/3, trustLevel) of the voting power
    // this ensures that there is at least single correct validator in the set of signers
    if signedPower < max(1/3, trustLevel) * totalPower return ErrInsufficientVotingPower
    return nil
}

// returns nil if commit is signed by more than 2/3 of voting power of the given validator set
// return error otherwise
func verifyCommitFull(vs ValidatorSet, commit Commit) error {
    totalPower := vs.TotalVotingPower;
    signedPower := votingPowerIn(signers(commit, vs), vs)

    // check the signers account for +2/3 of the voting power
    if signedPower * 3 <= totalPower * 2 return ErrInvalidCommit
    return nil
}
```

**VerifyHeaderAtHeight.** The function `VerifyHeaderAtHeight` captures high level
logic, i.e., application call to the light client module to download and verify header
for some height.

```go
func VerifyHeaderAtHeight(untrustedHeight int64,
                          trustedState TrustedState,
                          trustThreshold float,
                          trustingPeriod Duration,
                          clockDrift Duration) (TrustedState, error)) {

    trustedHeader := trustedState.SignedHeader.Header

    now := System.Time()
    if !isWithinTrustedPeriod(trustedHeader, trustingPeriod, now) {
        return (trustedState, ErrHeaderNotWithinTrustedPeriod)
    }

    newTrustedState, err := VerifyBisection(untrustedHeight,
                                            trustedState,
                                            trustThreshold,
                                            trustingPeriod,
                                            clockDrift,
                                            now)

    if err != nil return (trustedState, err)

    now = System.Time()
    if !isWithinTrustedPeriod(trustedHeader, trustingPeriod, now) {
        return (trustedState, ErrHeaderNotWithinTrustedPeriod)
    }

    return (newTrustedState, err)
}
```

Note that in case `VerifyHeaderAtHeight` returns without an error (untrusted header
is successfully verified) then we have a guarantee that the transition of the trust
from `trustedState` to `newTrustedState` happened during the trusted period of
`trustedState.SignedHeader.Header`.

In case `VerifyHeaderAtHeight` returns with an error, then either (i) the full node we are talking to is faulty
or (ii) the trusted header has expired (it is outside its trusted period). In case (i) the full node is faulty so
light client should disconnect and reinitialise with new peer. In the case (ii) as the trusted header has expired,
we need to reinitialise light client with a new trusted header (that is within its trusted period),
but we don't necessarily need to disconnect from the full node we are talking to (as we haven't observed full node misbehavior in this case).

**VerifyBisection.** The function `VerifyBisection` implements
recursive logic for checking if it is possible building trust
relationship between `trustedState` and untrusted header at the given height over
finite set of (downloaded and verified) headers.

```go
func VerifyBisection(untrustedHeight int64,
                     trustedState TrustedState,
                     trustThreshold float,
                     trustingPeriod Duration,
                     clockDrift Duration,
                     now Time) (TrustedState, error) {

    untrustedSh, error := Commit(untrustedHeight)
    if error != nil return (trustedState, ErrRequestFailed)

    untrustedHeader = untrustedSh.Header

    // note that we pass now during the recursive calls. This is fine as
    // all other untrusted headers we download during recursion will be
    // for a smaller heights, and therefore should happen before.
    if untrustedHeader.Time > now + clockDrift {
        return (trustedState, ErrInvalidHeaderTime)
    }

    untrustedVs, error := Validators(untrustedHeight)
    if error != nil return (trustedState, ErrRequestFailed)

    untrustedNextVs, error := Validators(untrustedHeight + 1)
    if error != nil return (trustedState, ErrRequestFailed)

    error = verifySingle(
             trustedState,
             untrustedSh,
             untrustedVs,
             untrustedNextVs,
             trustThreshold)

    if fatalError(error) return (trustedState, error)

    if error == nil {
        // the untrusted header is now trusted.
        newTrustedState = TrustedState(untrustedSh, untrustedNextVs)
        return (newTrustedState, nil)
    }

    // at this point in time we need to do bisection
    pivotHeight := ceil((trustedHeader.Height + untrustedHeight) / 2)

    error, newTrustedState = VerifyBisection(pivotHeight,
                                             trustedState,
                                             trustThreshold,
                                             trustingPeriod,
                                             clockDrift,
                                             now)
    if error != nil return (newTrustedState, error)

    return VerifyBisection(untrustedHeight,
                           newTrustedState,
                           trustThreshold,
                           trustingPeriod,
                           clockDrift,
                           now)
}

func fatalError(err) bool {
    return err == ErrHeaderNotWithinTrustedPeriod OR
           err == ErrInvalidAdjacentHeaders OR
           err == ErrNonIncreasingHeight OR
           err == ErrNonIncreasingTime OR
           err == ErrInvalidValidatorSet OR
           err == ErrInvalidNextValidatorSet OR
           err == ErrInvalidCommitValue OR
           err == ErrInvalidCommit
}
```

### The case `untrustedHeader.Height < trustedHeader.Height`

In the use case where someone tells the light client that application data that is relevant for it
can be read in the block of height `k` and the light client trusts a more recent header, we can use the
hashes to verify headers "down the chain." That is, we iterate down the heights and check the hashes in each step.

*Remark.* For the case were the light client trusts two headers `i` and `j` with `i < k < j`, we should
discuss/experiment whether the forward or the backward method is more effective.

```go
func VerifyHeaderBackwards(trustedHeader Header,
                           untrustedHeader Header,
                           trustingPeriod Duration,
                           clockDrift Duration) error {

  if untrustedHeader.Height >= trustedHeader.Height return ErrErrNonDecreasingHeight
  if untrustedHeader.Time >= trustedHeader.Time return ErrNonDecreasingTime

  now := System.Time()
  if !isWithinTrustedPeriod(trustedHeader, trustingPeriod, now) {
    return ErrHeaderNotWithinTrustedPeriod
  }

  old := trustedHeader
  for i := trustedHeader.Height - 1; i > untrustedHeader.Height; i-- {
    untrustedSh, error := Commit(i)
    if error != nil return ErrRequestFailed

    if (hash(untrustedSh.Header) != old.LastBlockID.Hash) {
      return ErrInvalidAdjacentHeaders
    }

    old := untrustedSh.Header
  }

  if hash(untrustedHeader) != old.LastBlockID.Hash {
    return ErrInvalidAdjacentHeaders
  }

  now := System.Time()
  if !isWithinTrustedPeriod(trustedHeader, trustingPeriod, now) {
    return ErrHeaderNotWithinTrustedPeriod
  }

  return nil
 }
```

*Assumption*: In the following, we assume that *untrusted_h.Header.height > trusted_h.Header.height*. We will quickly discuss the other case in the next section.

We consider the following set-up:

- the light client communicates with one full node
- the light client locally stores all the headers that has passed basic verification and that are within light client trust period. In the pseudo code below we
write *Store.Add(header)* for this. If a header failed to verify, then
the full node we are talking to is faulty and we should disconnect from it and reinitialise with new peer.
- If `CanTrust` returns *error*, then the light client has seen a forged header or the trusted header has expired (it is outside its trusted period).
    - In case of forged header, the full node is faulty so light client should disconnect and reinitialise with new peer. If the trusted header has expired,
  we need to reinitialise light client with new trusted header (that is within its trusted period), but we don't necessarily need to disconnect from the full node
  we are talking to (as we haven't observed full node misbehavior in this case).

## Correctness of the Light Client Protocols

### Definitions

- `TRUSTED_PERIOD`: trusted period
- for realtime `t`, the predicate `correct(v,t)` is true if the validator `v`
  follows the protocol until time `t` (we will see about recovery later).
- Validator fields. We will write a validator as a tuple `(v,p)` such that
    - `v` is the identifier (i.e., validator address; we assume identifiers are unique in each validator set)
    - `p` is its voting power
- For each header `h`, we write `trust(h) = true` if the light client trusts `h`.

### Failure Model

If a block `b` with a header `h` is generated at time `Time` (i.e. `h.Time = Time`), then a set of validators that
hold more than `2/3` of the voting power in `validators(h.NextValidatorsHash)` is correct until time
`h.Time + TRUSTED_PERIOD`.

Formally,
\[
\sum_{(v,p) \in validators(h.NextValidatorsHash) \wedge correct(v,h.Time + TRUSTED_PERIOD)} p >
2/3 \sum_{(v,p) \in validators(h.NextValidatorsHash)} p
\]

The light client communicates with a full node and learns new headers. The goal is to locally decide whether to trust a header. Our implementation needs to ensure the following two properties:

- *Light Client Completeness*: If a header `h` was correctly generated by an instance of Tendermint consensus (and its age is less than the trusted period),
then the light client should eventually set `trust(h)` to `true`.

- *Light Client Accuracy*: If a header `h` was *not generated* by an instance of Tendermint consensus, then the light client should never set `trust(h)` to true.

*Remark*: If in the course of the computation, the light client obtains certainty that some headers were forged by adversaries
(that is were not generated by an instance of Tendermint consensus), it may submit (a subset of) the headers it has seen as evidence of misbehavior.

*Remark*: In Completeness we use "eventually", while in practice `trust(h)` should be set to true before `h.Time + TRUSTED_PERIOD`. If not, the header
cannot be trusted because it is too old.

*Remark*: If a header `h` is marked with `trust(h)`, but it is too old at some point in time we denote with `now` (`h.Time + TRUSTED_PERIOD < now`),
then the light client should set `trust(h)` to `false` again at time `now`.

*Assumption*: Initially, the light client has a header `inithead` that it trusts, that is, `inithead` was correctly generated by the Tendermint consensus.

To reason about the correctness, we may prove the following invariant.

*Verification Condition: light Client Invariant.*
 For each light client `l` and each header `h`:
if `l` has set `trust(h) = true`,
  then validators that are correct until time `h.Time + TRUSTED_PERIOD` have more than two thirds of the voting power in `validators(h.NextValidatorsHash)`.

  Formally,
  \[
  \sum_{(v,p) \in validators(h.NextValidatorsHash) \wedge correct(v,h.Time + TRUSTED_PERIOD)} p >
  2/3 \sum_{(v,p) \in validators(h.NextValidatorsHash)} p
  \]

*Remark.* To prove the invariant, we will have to prove that the light client only trusts headers that were correctly generated by Tendermint consensus.
Then the formula above follows from the failure model.

## Details

**Observation 1.** If `h.Time + TRUSTED_PERIOD > now`, we trust the validator set `validators(h.NextValidatorsHash)`.

When we say we trust `validators(h.NextValidatorsHash)` we do `not` trust that each individual validator in `validators(h.NextValidatorsHash)`
is correct, but we only trust the fact that less than `1/3` of them are faulty (more precisely, the faulty ones have less than `1/3` of the total voting power).

*`VerifySingle` correctness arguments*

Light Client Accuracy:

- Assume by contradiction that `untrustedHeader` was not generated correctly and the light client sets trust to true because `verifySingle` returns without error.
- `trustedState` is trusted and sufficiently new
- by the Failure Model, less than `1/3` of the voting power held by faulty validators => at least one correct validator `v` has signed `untrustedHeader`.
- as `v` is correct up to now, it followed the Tendermint consensus protocol at least up to signing `untrustedHeader` => `untrustedHeader` was correctly generated.
We arrive at the required contradiction.

Light Client Completeness:

- The check is successful if sufficiently many validators of `trustedState` are still validators in the height `untrustedHeader.Height` and signed `untrustedHeader`.
- If `untrustedHeader.Height = trustedHeader.Height + 1`, and both headers were generated correctly, the test passes.

*Verification Condition:* We may need a Tendermint invariant stating that if `untrustedSignedHeader.Header.Height = trustedHeader.Height + 1` then
`signers(untrustedSignedHeader.Commit) \subseteq validators(trustedHeader.NextValidatorsHash)`.

*Remark*: The variable `trustThreshold` can be used if the user believes that relying on one correct validator is not sufficient.
However, in case of (frequent) changes in the validator set, the higher the `trustThreshold` is chosen, the more unlikely it becomes that
`verifySingle` returns with an error for non-adjacent headers.

- `VerifyBisection` correctness arguments (sketch)*

Light Client Accuracy:

- Assume by contradiction that the header at `untrustedHeight` obtained from the full node was not generated correctly and
the light client sets trust to true because `VerifyBisection` returns without an error.
- `VerifyBisection` returns without error only if all calls to `verifySingle` in the recursion return without error (return `nil`).
- Thus we have a sequence of headers that all satisfied the `verifySingle`
- again a contradiction

light Client Completeness:

This is only ensured if upon `Commit(pivot)` the light client is always provided with a correctly generated header.

*Stalling*

With `VerifyBisection`, a faulty full node could stall a light client by creating a long sequence of headers that are queried one-by-one by the light client and look OK,
before the light client eventually detects a problem. There are several ways to address this:

- Each call to `Commit` could be issued to a different full node
- Instead of querying header by header, the light client tells a full node which header it trusts, and the height of the header it needs. The full node responds with
the header along with a proof consisting of intermediate headers that the light client can use to verify. Roughly, `VerifyBisection` would then be executed at the full node.
- We may set a timeout how long `VerifyBisection` may take.