Merge pull request #73 from tendermint/bucky/light-reorg

Move light specs to their own dir, add readme and diagram
5 years ago · dc542068ae
--- a/spec/consensus/fork-accountability.md
+++ b/spec/consensus/fork-accountability.md
@ -1,319 +1,3 @@
 # Fork accountability -- Problem statement and attacks
 # Fork Accountability - MOVED!

 ## Problem Statement

 Tendermint consensus guarantees the following specifications for all heights:
 * agreement -- no two correct full nodes decide differently.
 * validity -- the decided block satisfies the predefined predicate *valid()*.
 * termination -- all correct full nodes eventually decide,

 if the
 faulty validators have at most 1/3 of voting power in the current validator set. In the case where this assumption
 does not hold, each of the specification may be violated.

 The agreement property says that for a given height, any two correct validators that decide on a block for that height decide on the same block. That the block was indeed generated by the blockchain, can be verified starting from a trusted (genesis) block, and checking that all subsequent blocks are properly signed.


 However, faulty nodes may forge blocks and try to convince users (lite clients) that the blocks had been correctly generated. In addition, Tendermint agreement might be violated in the case where more than 1/3 of the voting power belongs to faulty validators: Two correct validators decide on different blocks. The latter case motivates the term "fork": as Tendermint consensus also agrees on the next validator set, correct validators may have decided on disjoint next validator sets, and the chain branches into two or more partitions (possibly having faulty validators in common) and each branch continues to generate blocks independently of the other.

 We say that a fork is a case in which there are two commits for different blocks at the same height of the blockchain. The proplem is to ensure that in those cases we are able to detect faulty validators (and not mistakenly accuse correct validators), and incentivize therefore validators to behave according to the protocol specification.

 **Conceptual Limit.** In order to prove misbehavior of a node, we have to show that the behavior deviates from correct behavior with respect to a given algorithm. Thus, an algorithm that detects misbehavior of nodes executing some algorithm *A* must be defined with respect to algorithm *A*. In our case, *A* is Tendermint consensus (+ other protocols in the infrastructure; e.g.,full nodes and the Lite Client). If the consensus algorithm is changed/updated/optimized in the future, we have to check whether changes to the accountability algorithm are also required. All the discussions in this document are thus inherently specific to Tendermint consensus and the Lite Client specification.

 **Q:** Should we distinguish agreement for validators and full nodes for agreement? The case where all correct validators agree on a block, but a correct full node decides on a different block seems to be slightly less severe that the case where two correct validators decide on different blocks. Still, if a contaminated full node becomes validator that may be problematic later on. Also it is not clear how gossiping is impaired if a contaminated full node is on a different branch.

 *Remark.* In the case more than 1/3 of the voting power belongs to faulty validators, also validity and termination can be broken. Termination can be broken if faulty processes just do not send the messages that are needed to make progress. Due to asynchrony, this is not punishable, because faulty validators can always claim they never received the messages that would have forced them to send messages.


 ## The Misbehavior of Faulty Validators

 Forks are the result of faulty validators deviating from the protocol. In principle several such deviations can be detected without a fork actually occurring:

 1. double proposal: A faulty proposer proposes two different values (blocks) for the same height and the same round in Tendermint consensus.

 2. double signing: Tendermint consensus forces correct validators to prevote and precommit for at most one value per round. In case a faulty validator sends multiple prevote and/or precommit messages for different values for the same height/round, this is a misbehavior.

 3. lunatic validator: Tendermint consensus forces correct validators to prevote and precommit only for values *v* that satisfy *valid(v)*. If faulty validators prevote and precommit for *v* although *valid(v)=false* this is misbehavior.

 *Remark.* In isolation, Point 3 is an attack on validity (rather than agreement). However, the prevotes and precommits can then also be used to forge blocks.

 1. amnesia: Tendermint consensus has a locking mechanism. If a validator has some value v locked, then it can only prevote/precommit for v or nil. Sending prevote/precomit message for a different value v' (that is not nil) while holding lock on value v is misbehavior.   

 2. spurious messages: In Tendermint consensus most of the message send instructions are guarded by threshold guards, e.g., one needs to receive *2f + 1* prevote messages to send precommit. Faulty validators may send precommit without having received the prevote messages.


 Independently of a fork happening, punishing this behavior might be important to prevent forks altogether. This should keep attackers from misbehaving: if at most 1/3 of the voting power is faulty, this misbehavior is detectable but will not lead to a safety violation. Thus, unless they have more than 1/3 (or in some cases more than 2/3) of the voting power attackers have the incentive to not misbehave. If attackers control too much voting power, we have to deal with forks, as discussed in this document.   


 ## Two types of forks

 * Fork-Full. Two correct validators decide on different blocks for the same height. Since also the next validator sets are decided upon, the correct validators may be partitioned to participate in two distinct branches of the forked chain.

 As in this case we have two different blocks (both having the same right/no right to exist), a central system invariant (one block per height decided by correct validators) is violated. As full nodes are contaminated in this case, the contamination can spread also to lite clients. However, even without breaking this system invariant, lite clients can be subject to a fork:

 * Fork-Lite. All correct validators decide on the same block for height *h*, but faulty processes (validators or not), forge a different block for that height, in order to fool users (who use the lite client).


 # Attack scenarios

 ## On-chain attacks

 ### Equivocation (one round)

 There are several scenarios in which forks might happen. The first is double signing within a round.

 * F1. Equivocation: faulty validators sign multiple vote messages (prevote and/or precommit) for different values *during the same round r* at a given height h.


 ### Flip-flopping

 Tendermint consensus implements a locking mechanism: If a correct validator *p* receives proposal for value v and *2f + 1* prevotes for a value *id(v)* in round *r*, it locks *v* and remembers *r*. In this case, *p* also sends a precommit message for *id(v)*, which later may serve as proof that *p* locked *v*.
 In subsequent rounds, *p* only sends prevote messages for a value it had previously locked. However, it is possible to change the locked value if in a future round *r' > r*, if the process receives proposal and *2f + 1* prevotes for a different value *v'*. In this case, *p* could send a prevote/precommit for *id(v')*. This algorithmic feature can be exploited in two ways:



 * F2. Faulty Flip-flopping (Amnesia): faulty validators precommit some value *id(v)* in round *r* (value *v* is locked in round *r*) and then prevote for different value *id(v')* in higher round *r' > r* without previously correctly unlocking value *v*. In this case faulty processes "forget" that they have locked value *v* and prevote some other value in the following rounds.
 Some correct validators might have decided on *v* in *r*, and other correct validators decide on *v'* in *r'*. Here we can have branching on the main chain (Fork-Full).


 * F3. Correct Flip-flopping (Back to the past): There are some precommit messages signed by (correct) validators for value *id(v)* in  round *r*. Still, *v* is not decided upon, and all processes move on to the next round. Then correct validators (correctly) lock and decide a different value *v'* in some round *r' > r*. And the correct validators continue; there is no branching on the main chain.
 However, faulty validators may use the correct precommit messages from round *r* together with a posteriori generated faulty precommit messages for round *r* to forge a block for a value that was not decided on the main chain (Fork-Lite).





 ## Off-chain attacks

 F1-F3 may contaminate the state of full nodes (and even validators). Contaminated (but otherwise correct) full nodes may thus communicate faulty blocks to lite clients.
 Similarly, without actually interfering with the main chain, we can have the following:

 * F4. Phantom validators: faulty validators vote (sign prevote and precommit messages) in heights in which they are not part of the validator sets (at the main chain).

 * F5. Lunatic validator: faulty validator that sign vote messages to support (arbitrary) application state that is different from the application state that resulted from valid state transitions.

 ## Types of victims

 We consider three types of potential attack victims:


 - FN: full node
 - LCS: lite client with sequential header verification
 - LCB: lite client with bisection based header verification

 F1 and F2 can be used by faulty validators to actually create multiple branches on the blockchain. That means that correctly operating full nodes decide on different blocks for the same height. Until a fork is detected locally by a full node (by receiving evidence from others or by some other local check that fails), the full node can spread corrupted blocks to lite clients.

 *Remark.* If full nodes take a branch different from the one taken by the validators, it may be that the liveness of the gossip protocol may be affected. We should eventually look at this more closely. However, as it does not influence safety it is not a primary concern.

 F3 is similar to F1, except that no two correct validators decide on different blocks. It may still be the case that full nodes become affected.

 In addition, without creating a fork on the main chain, lite clients can be contaminated by more than a third of validators that are faulty and sign a forged header
 F4 cannot fool correct full nodes as they know the current validator set. Similarly, LCS know who the validators are. Hence, F4 is an attack against LCB that do not necessarily know the complete prefix of headers (Fork-Lite), as they trust a header that is signed by at least one correct validator (trusting period method).






 The following table gives an overview of how the different attacks may affect different nodes. F1-F3 are *on-chain* attacks so they can corrupt the state of full nodes. Then if a lite client (LCS or LCB) contacts a full node to obtain headers (or blocks), the corrupted state may propagate to the lite client.  

 F4 and F5 are *off-chain*, that is, these attacks cannot be used to corrupt the state of full nodes (which have sufficient knowledge on the state of the chain to not be fooled). 


 | Attack |  FN | LCS | LCB |
 |:------:|:------:|:------:|:------:|
 | F1 |  direct  | FN |     FN |
 | F2 |   direct | FN |     FN |
 | F3 |  direct  | FN |     FN |
 | F4 |          |    | direct |
 | F5 |          |    | direct |



 **Q:** Lite clients are more vulnerable than full nodes, because the former do only verify headers but do not execute transactions. What kind of certainty is gained by a full node that executes a transaction?

 As a full node verifies all transactions, it can only be
 contaminated by an attack if the blockchain itself violates its invariant (one block per height), that is, in case of a fork that leads to branching.




 ## Detailed Attack Scenarios

 ### Equivocation based attacks

 In case of equivocation based attacks, faulty validators sign multiple votes (prevote and/or precommit) in the same
 round of some height. This attack can be executed on both full nodes and lite clients. It requires more than 1/3 of voting power to be executed.

 #### Scenario 1: Equivocation on the main chain

 Validators:
 * CA - a set of correct validators with less than 1/3 of the voting power
 * CB - a set of correct validators with less than 1/3 of the voting power
 * CA and CB are disjoint
 * F - a set of faulty validators with more than 1/3 voting power

 Observe that this setting violates the Tendermint failure model.

 Execution:

 * A faulty proposer proposes block A to CA
 * A faulty proposer proposes block B to CB
 * Validators from the set CA and CB prevote for A and B, respectively.
 * Faulty validators from the set F prevote both for A and B.
 * The faulty prevote messages
  - for A arrive at CA long before the B messages
  - for B arrive at CB long before the A messages
 * Therefore correct validators from set CA and CB will observe
 more than 2/3 of prevotes for A and B and precommit for A and B, respectively.
 * Faulty validators from the set F precommit both values A and B.
 * Thus, we have more than 2/3 commits for both A and B.

 Consequences:
 * Creating evidence of misbehavior is simple in this case as we have multiple messages signed by the same faulty processes for different values in the same round.

 * We have to ensure that these different messages reach a correct process (full node, monitor?), which can submit evidence.

 * This is an attack on the full node level (Fork-Full).
 * It extends also to the lite clients,
 * For both we need a detection and recovery mechanism.

 #### Scenario 2: Equivocation to a lite client (LCS)


 Validators:
 * a set F of faulty validators with more than 2/3 of the voting power.

 Execution:
 * for the main chain F behaves nicely
 * F coordinates to sign a block B that is different from the one on the main chain.
 * the lite clients obtains B and trusts at as it is signed by more than 2/3 of the voting power.

 Consequences:

 Once equivocation is used to attack lite client it opens space
 for different kind of attacks as application state can be diverged in any direction. For example, it can modify validator set such that it contains only validators that do not have any stake bonded. Note that after a lite client is fooled by a fork, that means that an attacker can change application state and validator set arbitrarily.

 In order to detect such (equivocation-based attack), the lite client would need to cross check its state with some correct validator (or to obtain a hash of the state from the main chain using out of band channels).

 *Remark.* The lite client would be able to create evidence of misbehavior, but this would require to pull potentially a lot of data from correct full nodes. Maybe we need to figure out different architecture where a lite client that is attacked will push all its data for the current unbonding period to a correct node that will inspect this data and submit corresponding evidence. There are also architectures that assumes a special role (sometimes called fisherman) whose goal is to collect as much as possible useful data from the network, to do analysis and create evidence transactions. That functionality is outside the scope of this document.

 *Remark.* The difference between LCS and LCB might only be in the amount of voting power needed to convince lite client about arbitrary state. In case of LCB where security threshold is at minimum, an attacker can arbitrarily modify application state with  more than 1/3 of voting power, while in case of LCS it requires more than 2/3 of the voting power.

 ### Flip-flopping: Amnesia based attacks



 In case of amnesia, faulty validators lock some value *v* in some round *r*, and then vote for different value *v'* in higher rounds without correctly unlocking value *v*. This attack can be used both on full nodes and lite clients.

 #### Scenario 3: At most 2/3 of faults

 Validators:

 * a set F of faulty validators with more than 1/3 but at most 2/3 of the voting power
 * a set C of correct validators

 Execution:

 * Faulty validators commit (without exposing it on the main chain) a block A in round *r* by collecting more than 2/3 of the 
  voting power (containing correct and faulty validators).
 * All validators (correct and faulty) reach a round *r' > r*.
 * Some correct validators in C do not lock any value before round *r'*.
 * The faulty validators in F deviate from Tendermint consensus by ignoring that they locked A in *r*, and propose a different block B in *r'*.
 * As the validators in C that have not locked any value find B acceptable, they accept the proposal for B and commit a block B.

 *Remark.* In this case, the more than 1/3 of faulty validators do not need to commit an equivocation (F1) as they only vote once per round in the execution.

 Detecting faulty validators in the case of such an attack can be done by the fork accountability mechanism described in: https://docs.google.com/document/d/11ZhMsCj3y7zIZz4udO9l25xqb0kl7gmWqNpGVRzOeyY/edit?usp=sharing.

 If a lite client is attacked using this attack with more than 1/3 of voting power (and less than 2/3), the attacker cannot change the application state arbitrarily. Rather, the attacker is limited to a state a correct validator finds acceptable: In the execution above, correct validators still find the value acceptable, however, the block the lite client trusts deviates from the one on the main chain.

 #### Scenario 4: More than 2/3 of faults

 In case there is an attack with more than 2/3 of the voting power, an attacker can arbitrarily change application state.

 Validators:

 * a set F1 of faulty validators with more than 1/3 of the voting power
 * a set F2 of faulty validators with at most 1/3 of the voting power

 Execution

 * Similar to Scenario 3 (however, messages by correct validators are not needed)
 * The faulty validators in F1 lock value A in round *r*
 * They sign a different value in follow-up rounds
 * F2 does not lock A in round *r*

 Consequences:

 * The validators in F1 will be detectable by the the fork accountability mechanisms.
 * The validators in F2 cannot be detected using this mechanism.
 Only in case they signed something which conflicts with the application this can be used against them. Otherwise they do not do anything incorrect.
 * This case is not covered by the report https://docs.google.com/document/d/11ZhMsCj3y7zIZz4udO9l25xqb0kl7gmWqNpGVRzOeyY/edit?usp=sharing as it only assumes at most 2/3 of faulty validators.

 **Q:** do we need to define a special kind of attack for the case where a validator sign arbitrarily state? It seems that detecting such attack requires a different mechanism that would require as an evidence a sequence of blocks that led to that state. This might be very tricky to implement.

 ### Back to the past

 In this kind of attack, faulty validators take advantage of the fact that they did not sign messages in some of the past rounds. Due to the asynchronous network in which Tendermint operates, we cannot easily differentiate between such an attack and delayed message. This kind of attack can be used at both full nodes and lite clients.

 #### Scenario 5:

 Validators:
 * C1 -  a set of correct validators with 1/3 of the voting power
 * C2 - a set of correct validators with 1/3 of the voting power
 * C1 and C2 are disjoint
 * F - a set of faulty validators with 1/3 voting power
 * one additional faulty process *q*
 * F and *q* violate the Tendermint failure model.


 Execution:

 * in a round *r* of height *h* we have C1 precommitting a value A,
 * C2 precommits nil,
 * F does not send any message
 * *q* precommits nil.
 * In some round *r' > r*, F and *q* and C2 commit some other value B different from A.
 * F and *fp* "go back to the past" and sign precommit message for value A in round *r*.
 * Together with precomit messages of C1 this is sufficient for a commit for value A.


 Consequences:

 * Only a single faulty validator that previously precommited nil did equivocation, while the other 1/3 of faulty validators actually executed an attack that has exactly the same sequence of messages as part of amnesia attack. Detecting this kind of attack boil down to mechanisms for equivocation and amnesia.

 **Q:** should we keep this as a separate kind of attack? It seems that equivocation, amnesia and phantom validators are the only kind of attack we need to support and this gives us security also in other cases. This would not be surprising as equivocation and amnesia are attacks that followed from the protocol and phantom attack is not really an attack to Tendermint but more to the Proof of Stake module.

 ### Phantom validators

 In case of phantom validators, processes that are not part of the current validator set but are still bonded (as attack happen during their unbonding period) can be part of the attack by signing vote messages. This attack can be executed against both full nodes and lite clients.

 #### Scenario 6:

 Validators:
 * F -- a set of faulty validators that are not part of the validator set on the main chain at height *h + k*

 Execution:

 * There is a fork, and there exist two different headers for height *h + k*, with different validator sets:
  - VS2 on the main chain
  - forged header VS2', signed by F (and others)

 * a lite client has a trust in a header for height *h* (and the corresponding validator set VS1).
 * As part of bisection header verification, it verifies the header at height *h + k* with new validator set VS2'.

 Consequences:

 * To detect this, a node needs to see both, the forged header and the canonical header from the chain.
 * If this is the case, detecting these kind of attacks is easy as it just requires verifying if processes are signing messages in heights in which they are not part of the validator set.  

 **Remark.** We can have phantom-validator-based attacks as a follow up of equivocation or amnesia based attack where forked state contains validators that are not part of the validator set at the main chain. In this case, they keep signing messages contributed to a forked chain (the wrong branch) although they are not part of the validator set on the main chain. This attack can also be used to attack full node during a period of time it is eclipsed.

 ### Lunatic validator

 Lunatic validator agrees to sign commit messages for arbitrary application state. It is used to attack lite clients.
 Note that detecting this behavior require application knowledge. Detecting this behavior can probably be done by
 referring to the block before the one in which height happen.  

 **Q:** can we say that in this case a validator declines to check if a proposed value is valid before voting for it?
 Fork Accountability has moved to [light](./light).
--- a/spec/consensus/light-client.md
+++ b/spec/consensus/light-client.md
@ -1,587 +1,3 @@
 # Lite client

 A lite client is a process that connects to Tendermint full node(s) and then tries to verify application
 data using the Merkle proofs.

 ## Problem statement

 We assume that the lite client knows a (base) header *inithead* it trusts (by social consensus or because
 the lite 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.

 ## 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
        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 lite 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

    // return 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
 ```

 ### Failure Model

 For the purpose of model definitions we assume that there exists a function
 `validators` that returns the corresponding validator set for the given hash.
 The lite client specification 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](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 lite 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 lite 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 lite 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 `PUNISHMENT_PERIOD`).
 Furthermore, we assume that `TRUSTED_PERIOD < PUNISHMENT_PERIOD` and that they are normally of the same order of magnitude, for example
 `TRUSTED_PERIOD = PUNISHMENT_PERIOD / 2`. Note that `PUNISHMENT_PERIOD` is often referred to as an
 unbonding period due to the "bonding" mechanism in modern proof of stake systems.

 The specification in this document considers an implementation of the lite client under the Failure Model defined above.
 Mechanisms like `fork accountability` and `evidence submission` are defined in the context of `PUNISHMENT_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](fork-accountability.md).

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

 ### Functions

 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 assume `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 lite 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`.


 **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 lite 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`.

 **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 `untrusted_h.Header.height < trusted_h.Header.height`

 In the use case where someone tells the lite client that application data that is relevant for it 
 can be read in the block of height `k` and the lite 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 lite 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 Backwards(trusted_h,untrusted_h) error {
  assert (untrusted_h.Header.height < trusted_h.Header.height)
  if !isWithinTrustedPeriod(trusted_h) return ErrHeaderNotTrusted(trusted_h)

  old := trusted_h
  for i := trusted_h.Header.height - 1; i > untrusted_h.Header.height; i-- {
    new := Commit(i)
    if (hash(new) != old.Header.hash) {
      return ErrInvalidAdjacentHeaders
    }
    old := new
    if !isWithinTrustedPeriod(trusted_h) return ErrHeaderNotTrusted(trusted_h)
  }
  if hash(untrusted_h) != old.Header.hash return ErrInvalidAdjacentHeaders
  return nil
 }
 ```

 In order to incentivize correct behavior of validators that run Tendermint consensus protocol, fork detection protocol (it will be explained in different document) is executed in case of a fork (conflicting
 headers are detected). As detecting conflicting headers, its propagation through the network (by the gossip protocol) and execution of the fork accountability
 protocol on the chain takes time, the lite client logic assumes conservative value for trusted period. More precisely, in the context of lite client we always
 operate with a smaller trusted period that we call *lite client trusted period* (LITE_CLIENT_TRUSTED_PERIOD). If we assume that upper bound
 for fork detection, propagation and processing on the chain is denoted with *fork procession period* (FORK_PROCESSING_PERIOD), then the following formula
 holds:
 ```LITE_CLIENT_TRUSTED_PERIOD + FORK_PROCESSING_PERIOD < TRUSTED_PERIOD```, where TRUSTED_PERIOD comes from the Tendermint Failure Model.


 *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 lite client communicates with one full node
 - the lite client locally stores all the headers that has passed basic verification and that are within lite 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 lite 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 lite client should disconnect and reinitialise with new peer. If the trusted header has expired,
  we need to reinitialise lite 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).



 ## Context of this document

 In order to make sure that full nodes have the incentive to follow the protocol, we have to address the
 following three Issues

 1) The lite client needs a method to verify headers it obtains from a full node it connects to according to trust assumptions -- this document.

 2) The lite client must be able to connect to other full nodes to detect and report on failures in the trust assumptions (i.e., conflicting headers) -- a future document (see #4215).

 3) In the event the trust assumption fails (i.e., a lite client is fooled by a conflicting header), the Tendermint fork accountability protocol must account for the evidence -- a future document (see #3840).

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

 * For each header *h* it has locally stored, the lite client stores whether
    it trusts *h*. We write *trust(h) = true*, if this is the case.

 * signed header fields: contains a header and a  *commit* for the current header; a "seen commit".
  In Tendermint consensus the "canonical commit" is stored in header *height* + 1.


  * Validator fields. We will write a validator as a tuple *(v,p)* such that
    + *v* is the identifier (we assume identifiers are unique in each validator set)
    + *p* is its voting power

 ### Definitions

 * *TRUSTED_PERIOD*: trusting 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).


 ### Tendermint Failure Model

 If a block *b* is generated at time *Time* (and this time is stored in the block), then 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```.

 Formally,
 \[
 \sum_{(v,p) \in h.Header.NextV \wedge correct(v,h.Header.bfttime + TRUSTED_PERIOD)} p >
 2/3 \sum_{(v,p) \in h.Header.NextV} p
 \]


 ## Lite Client Trusting Spec

 The lite 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:

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

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

 *Remark*: If in the course of the computation, the lite 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.Header.bfttime + tp*. If not, the block cannot be trusted because it is too old.

 *Remark*: If a header *h* is marked with *trust(h)*, but it is too old (its bfttime is more than *tp* ago), then the lite client should set *trust(h)* to false again.

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

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

 *Verification Condition: Lite Client Invariant.*
 For each lite client *l* and each header *h*:
 if *l* has set *trust(h) = true*,
  then validators that are correct until time *h.Header.bfttime + tp* have more than two thirds of the voting power in *h.Header.NextV*.

  Formally,
  \[
  \sum_{(v,p) \in h.Header.NextV \wedge correct(v,h.Header.bfttime + tp)} p >
  2/3 \sum_{(v,p) \in h.Header.NextV} p
  \]

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


 ## High Level Solution

 Upon initialization, the lite client is given a header *inithead* it trusts (by
 social consensus). It is assumed that *inithead* satisfies the lite client invariant. (If *inithead* has been correctly generated by Tendermint consensus, the invariant follows from the Tendermint Failure Model.)
 Note that the *inithead* should be within its trusted period during initialization.

 When a lite clients sees a signed new 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 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 lite client knows all headers in the prefix.
 Intuitively, a trusted validator set is assumed to only chose a new validator set that will obey the Tendermint Failure Model.

 2. **Trusting period.** Based on a trusted block *h*, and the lite client
 invariant, which ensures the fault assumption during the trusting period, we can check whether at least one  validator, that has been continuously correct from *h.Header.bfttime* until now, has signed *snh*.
 If this is the case, similarly to above, the chosen validator set in *snh* does not violate the Tendermint Failure Model.

 3. **Bisection.** If a check according to the trusting period fails, the lite client can try to obtain a header *hp* whose height lies between *h* and *snh* 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 *snh*; if not, we may continue recursively.

 ## How to use it

 We consider the following use case:
 the lite client wants to verify a header for some given height *k*. Thus:
  - it requests the signed header for height *k* from a full node
  - it tries to verify this header with the methods described here.

 This can be used in several settings:
  - someone tells the lite client that application data that is relevant for it can be read in the block of height *k*.
  - the lite clients wants the latest state. It asks a full nude for the current height, and uses the response for *k*.
  - in case of inter-blockchain communication protocol (IBC) the light client runs on a chain and someone feeds it
  signed headers as input and it computes whether it can trust it.


 ## Details

 **Observation 1.** If *h.Header.bfttime + tp > now*, we trust the old
 validator set *h.Header.NextV*.

 When we say we trust *h.Header.NextV* we do *not* trust that each individual validator in *h.Header.NextV* 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).



 *Correctness arguments*

 Towards Lite Client Accuracy:
 - Assume by contradiction that `untrusted_h` was not generated correctly and the lite client sets trust to true because `CheckSupport` returns true.
 - trusted_h is trusted and sufficiently new
 - by Tendermint Fault Model, less than 1/3 of voting power held by faulty validators => at least one correct validator *v* has signed `untrusted_h`.
 - as *v* is correct up to now, it followed the Tendermint consensus protocol at least up to signing `untrusted_h` => `untrusted_h` was correctly generated, we arrive at the required contradiction.


 Towards Lite Client Completeness:
 - The check is successful if sufficiently many validators of `trusted_h` are still validators in `untrusted_h` and signed `untrusted_h`.
 - If *untrusted_h.Header.height = trusted_h.Header.height + 1*, and both headers were generated correctly, the test passes

 *Verification Condition:* We may need a Tendermint invariant stating that if *untrusted_h.Header.height = trusted_h.Header.height + 1* then *signers(untrusted_h.Commit) \subseteq trusted_h.Header.NextV*.

 *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 CheckSupport returns true for non-adjacent headers.




 *Correctness arguments (sketch)*

 Lite Client Accuracy:
 - Assume by contradiction that `untrusted_h` was not generated correctly and the lite client sets trust to true because CanTrustBisection returns nil.
 - CanTrustBisection returns true only if all calls to CheckSupport in the recursion return nil.
 - Thus we have a sequence of headers that all satisfied the CheckSupport
 - again a contradiction

 Lite Client Completeness:

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

 *Stalling*

 With CanTrustBisection, a faulty full node could stall a lite client by creating a long sequence of headers that are queried one-by-one by the lite client and look OK, before the lite 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 lite 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, Bisection would then be executed at the full node.
 * We may set a timeout how long bisection may take.




 # Light Client - MOVED!

 Light Client has moved to [light](./light).
--- a/spec/consensus/light/README.md
+++ b/spec/consensus/light/README.md
@ -0,0 +1,66 @@
 # Tendermint Light Client Protocol

 NOTE: This specification is under heavy development and is not yet complete nor
 accurate. 

 ## Contents

 - [Motivation](#motivation)
 - [Structure](#structure)
 - [Core Verification](./verification.md)
 - [Fork Detection](./detection.md)
 - [Fork Accountability](./accountability.md)

 ## Motivation

 The Tendermint Light Client is motivated by the need for a light weight protocol
 to sync with a Tendermint blockchain, with the least processing necessary to
 securely verify a recent state. The protocol consists
 primarily of checking hashes and verifying Tendermint commit signatures to
 update trusted validator sets and committed block headers from the chain.

 Motivating use cases include:

 - Light Node: a daemon that syncs a blockchain to the latest committed header by making RPC requests to full nodes.
 - State Sync: a reactor that syncs a blockchain to a recent committed state by making P2P requests to full nodes.
 - IBC Client: an ABCI application library that syncs a blockchain to a recent committed header by receiving proof-carrying
 transactions from "IBC relayers", who make RPC requests to full nodes on behalf of the IBC clients.

 ## Structure

 ### Components

 The Tendermint Light Client consists of three primary components:  

 - [Core Verification](./verification.md): verifying hashes, signatures, and validator set changes
 - [Fork Detection](./detection.md): talking to multiple peers to detect byzantine behaviour
 - [Fork Accountability](./accountability.md): analyzing byzantine behaviour to hold validators accountable.

 While every light client must perform core verification and fork detection
 to achieve their prescribed security level, fork accountability is expected to
 be done by full nodes and validators, and is thus more accurately a component of
 the full node consensus protocol, though it is included here since it is
 primarily concerned with providing security to light clients.

 A schematic of the core verification and fork detection components in
 a Light Node are depicted below. The schematic is quite similar for other use cases.
 Note fork accountability is not depicted, as it is the responsibility of the
 full nodes.

 ![Light Client Diagram](./assets/light-node-image.png).

 ### Synchrony

 Light clients are fundamentally synchronous protocols, 
 where security is restricted by the interval during which a validator can be punished
 for byzantine behaviour. We assume here that such intervals have fixed and known minima
 referred to commonly as a blockchain's Unbonding Period.

 A secure light client must guarantee that all three components - 
 core verification, fork detection, and fork accountability - 
 each with their own synchrony assumptions and fault model, can execute
 sequentially and to completion within the given Unbonding Period.

 TODO: define all the synchrony parameters used in the protocol and their
 relation to the Unbonding Period.

--- a/spec/consensus/light/accountability.md
+++ b/spec/consensus/light/accountability.md
@ -0,0 +1,319 @@
 # Fork accountability 

 ## Problem Statement

 Tendermint consensus guarantees the following specifications for all heights:
 * agreement -- no two correct full nodes decide differently.
 * validity -- the decided block satisfies the predefined predicate *valid()*.
 * termination -- all correct full nodes eventually decide,

 if the
 faulty validators have at most 1/3 of voting power in the current validator set. In the case where this assumption
 does not hold, each of the specification may be violated.

 The agreement property says that for a given height, any two correct validators that decide on a block for that height decide on the same block. That the block was indeed generated by the blockchain, can be verified starting from a trusted (genesis) block, and checking that all subsequent blocks are properly signed.


 However, faulty nodes may forge blocks and try to convince users (lite clients) that the blocks had been correctly generated. In addition, Tendermint agreement might be violated in the case where more than 1/3 of the voting power belongs to faulty validators: Two correct validators decide on different blocks. The latter case motivates the term "fork": as Tendermint consensus also agrees on the next validator set, correct validators may have decided on disjoint next validator sets, and the chain branches into two or more partitions (possibly having faulty validators in common) and each branch continues to generate blocks independently of the other.

 We say that a fork is a case in which there are two commits for different blocks at the same height of the blockchain. The proplem is to ensure that in those cases we are able to detect faulty validators (and not mistakenly accuse correct validators), and incentivize therefore validators to behave according to the protocol specification.

 **Conceptual Limit.** In order to prove misbehavior of a node, we have to show that the behavior deviates from correct behavior with respect to a given algorithm. Thus, an algorithm that detects misbehavior of nodes executing some algorithm *A* must be defined with respect to algorithm *A*. In our case, *A* is Tendermint consensus (+ other protocols in the infrastructure; e.g.,full nodes and the Lite Client). If the consensus algorithm is changed/updated/optimized in the future, we have to check whether changes to the accountability algorithm are also required. All the discussions in this document are thus inherently specific to Tendermint consensus and the Lite Client specification.

 **Q:** Should we distinguish agreement for validators and full nodes for agreement? The case where all correct validators agree on a block, but a correct full node decides on a different block seems to be slightly less severe that the case where two correct validators decide on different blocks. Still, if a contaminated full node becomes validator that may be problematic later on. Also it is not clear how gossiping is impaired if a contaminated full node is on a different branch.

 *Remark.* In the case more than 1/3 of the voting power belongs to faulty validators, also validity and termination can be broken. Termination can be broken if faulty processes just do not send the messages that are needed to make progress. Due to asynchrony, this is not punishable, because faulty validators can always claim they never received the messages that would have forced them to send messages.


 ## The Misbehavior of Faulty Validators

 Forks are the result of faulty validators deviating from the protocol. In principle several such deviations can be detected without a fork actually occurring:

 1. double proposal: A faulty proposer proposes two different values (blocks) for the same height and the same round in Tendermint consensus.

 2. double signing: Tendermint consensus forces correct validators to prevote and precommit for at most one value per round. In case a faulty validator sends multiple prevote and/or precommit messages for different values for the same height/round, this is a misbehavior.

 3. lunatic validator: Tendermint consensus forces correct validators to prevote and precommit only for values *v* that satisfy *valid(v)*. If faulty validators prevote and precommit for *v* although *valid(v)=false* this is misbehavior.

 *Remark.* In isolation, Point 3 is an attack on validity (rather than agreement). However, the prevotes and precommits can then also be used to forge blocks.

 1. amnesia: Tendermint consensus has a locking mechanism. If a validator has some value v locked, then it can only prevote/precommit for v or nil. Sending prevote/precomit message for a different value v' (that is not nil) while holding lock on value v is misbehavior.   

 2. spurious messages: In Tendermint consensus most of the message send instructions are guarded by threshold guards, e.g., one needs to receive *2f + 1* prevote messages to send precommit. Faulty validators may send precommit without having received the prevote messages.


 Independently of a fork happening, punishing this behavior might be important to prevent forks altogether. This should keep attackers from misbehaving: if at most 1/3 of the voting power is faulty, this misbehavior is detectable but will not lead to a safety violation. Thus, unless they have more than 1/3 (or in some cases more than 2/3) of the voting power attackers have the incentive to not misbehave. If attackers control too much voting power, we have to deal with forks, as discussed in this document.   


 ## Two types of forks

 * Fork-Full. Two correct validators decide on different blocks for the same height. Since also the next validator sets are decided upon, the correct validators may be partitioned to participate in two distinct branches of the forked chain.

 As in this case we have two different blocks (both having the same right/no right to exist), a central system invariant (one block per height decided by correct validators) is violated. As full nodes are contaminated in this case, the contamination can spread also to lite clients. However, even without breaking this system invariant, lite clients can be subject to a fork:

 * Fork-Lite. All correct validators decide on the same block for height *h*, but faulty processes (validators or not), forge a different block for that height, in order to fool users (who use the lite client).


 # Attack scenarios

 ## On-chain attacks

 ### Equivocation (one round)

 There are several scenarios in which forks might happen. The first is double signing within a round.

 * F1. Equivocation: faulty validators sign multiple vote messages (prevote and/or precommit) for different values *during the same round r* at a given height h.


 ### Flip-flopping

 Tendermint consensus implements a locking mechanism: If a correct validator *p* receives proposal for value v and *2f + 1* prevotes for a value *id(v)* in round *r*, it locks *v* and remembers *r*. In this case, *p* also sends a precommit message for *id(v)*, which later may serve as proof that *p* locked *v*.
 In subsequent rounds, *p* only sends prevote messages for a value it had previously locked. However, it is possible to change the locked value if in a future round *r' > r*, if the process receives proposal and *2f + 1* prevotes for a different value *v'*. In this case, *p* could send a prevote/precommit for *id(v')*. This algorithmic feature can be exploited in two ways:



 * F2. Faulty Flip-flopping (Amnesia): faulty validators precommit some value *id(v)* in round *r* (value *v* is locked in round *r*) and then prevote for different value *id(v')* in higher round *r' > r* without previously correctly unlocking value *v*. In this case faulty processes "forget" that they have locked value *v* and prevote some other value in the following rounds.
 Some correct validators might have decided on *v* in *r*, and other correct validators decide on *v'* in *r'*. Here we can have branching on the main chain (Fork-Full).


 * F3. Correct Flip-flopping (Back to the past): There are some precommit messages signed by (correct) validators for value *id(v)* in  round *r*. Still, *v* is not decided upon, and all processes move on to the next round. Then correct validators (correctly) lock and decide a different value *v'* in some round *r' > r*. And the correct validators continue; there is no branching on the main chain.
 However, faulty validators may use the correct precommit messages from round *r* together with a posteriori generated faulty precommit messages for round *r* to forge a block for a value that was not decided on the main chain (Fork-Lite).





 ## Off-chain attacks

 F1-F3 may contaminate the state of full nodes (and even validators). Contaminated (but otherwise correct) full nodes may thus communicate faulty blocks to lite clients.
 Similarly, without actually interfering with the main chain, we can have the following:

 * F4. Phantom validators: faulty validators vote (sign prevote and precommit messages) in heights in which they are not part of the validator sets (at the main chain).

 * F5. Lunatic validator: faulty validator that sign vote messages to support (arbitrary) application state that is different from the application state that resulted from valid state transitions.

 ## Types of victims

 We consider three types of potential attack victims:


 - FN: full node
 - LCS: lite client with sequential header verification
 - LCB: lite client with bisection based header verification

 F1 and F2 can be used by faulty validators to actually create multiple branches on the blockchain. That means that correctly operating full nodes decide on different blocks for the same height. Until a fork is detected locally by a full node (by receiving evidence from others or by some other local check that fails), the full node can spread corrupted blocks to lite clients.

 *Remark.* If full nodes take a branch different from the one taken by the validators, it may be that the liveness of the gossip protocol may be affected. We should eventually look at this more closely. However, as it does not influence safety it is not a primary concern.

 F3 is similar to F1, except that no two correct validators decide on different blocks. It may still be the case that full nodes become affected.

 In addition, without creating a fork on the main chain, lite clients can be contaminated by more than a third of validators that are faulty and sign a forged header
 F4 cannot fool correct full nodes as they know the current validator set. Similarly, LCS know who the validators are. Hence, F4 is an attack against LCB that do not necessarily know the complete prefix of headers (Fork-Lite), as they trust a header that is signed by at least one correct validator (trusting period method).






 The following table gives an overview of how the different attacks may affect different nodes. F1-F3 are *on-chain* attacks so they can corrupt the state of full nodes. Then if a lite client (LCS or LCB) contacts a full node to obtain headers (or blocks), the corrupted state may propagate to the lite client.  

 F4 and F5 are *off-chain*, that is, these attacks cannot be used to corrupt the state of full nodes (which have sufficient knowledge on the state of the chain to not be fooled). 


 | Attack |  FN | LCS | LCB |
 |:------:|:------:|:------:|:------:|
 | F1 |  direct  | FN |     FN |
 | F2 |   direct | FN |     FN |
 | F3 |  direct  | FN |     FN |
 | F4 |          |    | direct |
 | F5 |          |    | direct |



 **Q:** Lite clients are more vulnerable than full nodes, because the former do only verify headers but do not execute transactions. What kind of certainty is gained by a full node that executes a transaction?

 As a full node verifies all transactions, it can only be
 contaminated by an attack if the blockchain itself violates its invariant (one block per height), that is, in case of a fork that leads to branching.




 ## Detailed Attack Scenarios

 ### Equivocation based attacks

 In case of equivocation based attacks, faulty validators sign multiple votes (prevote and/or precommit) in the same
 round of some height. This attack can be executed on both full nodes and lite clients. It requires more than 1/3 of voting power to be executed.

 #### Scenario 1: Equivocation on the main chain

 Validators:
 * CA - a set of correct validators with less than 1/3 of the voting power
 * CB - a set of correct validators with less than 1/3 of the voting power
 * CA and CB are disjoint
 * F - a set of faulty validators with more than 1/3 voting power

 Observe that this setting violates the Tendermint failure model.

 Execution:

 * A faulty proposer proposes block A to CA
 * A faulty proposer proposes block B to CB
 * Validators from the set CA and CB prevote for A and B, respectively.
 * Faulty validators from the set F prevote both for A and B.
 * The faulty prevote messages
  - for A arrive at CA long before the B messages
  - for B arrive at CB long before the A messages
 * Therefore correct validators from set CA and CB will observe
 more than 2/3 of prevotes for A and B and precommit for A and B, respectively.
 * Faulty validators from the set F precommit both values A and B.
 * Thus, we have more than 2/3 commits for both A and B.

 Consequences:
 * Creating evidence of misbehavior is simple in this case as we have multiple messages signed by the same faulty processes for different values in the same round.

 * We have to ensure that these different messages reach a correct process (full node, monitor?), which can submit evidence.

 * This is an attack on the full node level (Fork-Full).
 * It extends also to the lite clients,
 * For both we need a detection and recovery mechanism.

 #### Scenario 2: Equivocation to a lite client (LCS)


 Validators:
 * a set F of faulty validators with more than 2/3 of the voting power.

 Execution:
 * for the main chain F behaves nicely
 * F coordinates to sign a block B that is different from the one on the main chain.
 * the lite clients obtains B and trusts at as it is signed by more than 2/3 of the voting power.

 Consequences:

 Once equivocation is used to attack lite client it opens space
 for different kind of attacks as application state can be diverged in any direction. For example, it can modify validator set such that it contains only validators that do not have any stake bonded. Note that after a lite client is fooled by a fork, that means that an attacker can change application state and validator set arbitrarily.

 In order to detect such (equivocation-based attack), the lite client would need to cross check its state with some correct validator (or to obtain a hash of the state from the main chain using out of band channels).

 *Remark.* The lite client would be able to create evidence of misbehavior, but this would require to pull potentially a lot of data from correct full nodes. Maybe we need to figure out different architecture where a lite client that is attacked will push all its data for the current unbonding period to a correct node that will inspect this data and submit corresponding evidence. There are also architectures that assumes a special role (sometimes called fisherman) whose goal is to collect as much as possible useful data from the network, to do analysis and create evidence transactions. That functionality is outside the scope of this document.

 *Remark.* The difference between LCS and LCB might only be in the amount of voting power needed to convince lite client about arbitrary state. In case of LCB where security threshold is at minimum, an attacker can arbitrarily modify application state with  more than 1/3 of voting power, while in case of LCS it requires more than 2/3 of the voting power.

 ### Flip-flopping: Amnesia based attacks



 In case of amnesia, faulty validators lock some value *v* in some round *r*, and then vote for different value *v'* in higher rounds without correctly unlocking value *v*. This attack can be used both on full nodes and lite clients.

 #### Scenario 3: At most 2/3 of faults

 Validators:

 * a set F of faulty validators with more than 1/3 but at most 2/3 of the voting power
 * a set C of correct validators

 Execution:

 * Faulty validators commit (without exposing it on the main chain) a block A in round *r* by collecting more than 2/3 of the 
  voting power (containing correct and faulty validators).
 * All validators (correct and faulty) reach a round *r' > r*.
 * Some correct validators in C do not lock any value before round *r'*.
 * The faulty validators in F deviate from Tendermint consensus by ignoring that they locked A in *r*, and propose a different block B in *r'*.
 * As the validators in C that have not locked any value find B acceptable, they accept the proposal for B and commit a block B.

 *Remark.* In this case, the more than 1/3 of faulty validators do not need to commit an equivocation (F1) as they only vote once per round in the execution.

 Detecting faulty validators in the case of such an attack can be done by the fork accountability mechanism described in: https://docs.google.com/document/d/11ZhMsCj3y7zIZz4udO9l25xqb0kl7gmWqNpGVRzOeyY/edit?usp=sharing.

 If a lite client is attacked using this attack with more than 1/3 of voting power (and less than 2/3), the attacker cannot change the application state arbitrarily. Rather, the attacker is limited to a state a correct validator finds acceptable: In the execution above, correct validators still find the value acceptable, however, the block the lite client trusts deviates from the one on the main chain.

 #### Scenario 4: More than 2/3 of faults

 In case there is an attack with more than 2/3 of the voting power, an attacker can arbitrarily change application state.

 Validators:

 * a set F1 of faulty validators with more than 1/3 of the voting power
 * a set F2 of faulty validators with at most 1/3 of the voting power

 Execution

 * Similar to Scenario 3 (however, messages by correct validators are not needed)
 * The faulty validators in F1 lock value A in round *r*
 * They sign a different value in follow-up rounds
 * F2 does not lock A in round *r*

 Consequences:

 * The validators in F1 will be detectable by the the fork accountability mechanisms.
 * The validators in F2 cannot be detected using this mechanism.
 Only in case they signed something which conflicts with the application this can be used against them. Otherwise they do not do anything incorrect.
 * This case is not covered by the report https://docs.google.com/document/d/11ZhMsCj3y7zIZz4udO9l25xqb0kl7gmWqNpGVRzOeyY/edit?usp=sharing as it only assumes at most 2/3 of faulty validators.

 **Q:** do we need to define a special kind of attack for the case where a validator sign arbitrarily state? It seems that detecting such attack requires a different mechanism that would require as an evidence a sequence of blocks that led to that state. This might be very tricky to implement.

 ### Back to the past

 In this kind of attack, faulty validators take advantage of the fact that they did not sign messages in some of the past rounds. Due to the asynchronous network in which Tendermint operates, we cannot easily differentiate between such an attack and delayed message. This kind of attack can be used at both full nodes and lite clients.

 #### Scenario 5:

 Validators:
 * C1 -  a set of correct validators with 1/3 of the voting power
 * C2 - a set of correct validators with 1/3 of the voting power
 * C1 and C2 are disjoint
 * F - a set of faulty validators with 1/3 voting power
 * one additional faulty process *q*
 * F and *q* violate the Tendermint failure model.


 Execution:

 * in a round *r* of height *h* we have C1 precommitting a value A,
 * C2 precommits nil,
 * F does not send any message
 * *q* precommits nil.
 * In some round *r' > r*, F and *q* and C2 commit some other value B different from A.
 * F and *fp* "go back to the past" and sign precommit message for value A in round *r*.
 * Together with precomit messages of C1 this is sufficient for a commit for value A.


 Consequences:

 * Only a single faulty validator that previously precommited nil did equivocation, while the other 1/3 of faulty validators actually executed an attack that has exactly the same sequence of messages as part of amnesia attack. Detecting this kind of attack boil down to mechanisms for equivocation and amnesia.

 **Q:** should we keep this as a separate kind of attack? It seems that equivocation, amnesia and phantom validators are the only kind of attack we need to support and this gives us security also in other cases. This would not be surprising as equivocation and amnesia are attacks that followed from the protocol and phantom attack is not really an attack to Tendermint but more to the Proof of Stake module.

 ### Phantom validators

 In case of phantom validators, processes that are not part of the current validator set but are still bonded (as attack happen during their unbonding period) can be part of the attack by signing vote messages. This attack can be executed against both full nodes and lite clients.

 #### Scenario 6:

 Validators:
 * F -- a set of faulty validators that are not part of the validator set on the main chain at height *h + k*

 Execution:

 * There is a fork, and there exist two different headers for height *h + k*, with different validator sets:
  - VS2 on the main chain
  - forged header VS2', signed by F (and others)

 * a lite client has a trust in a header for height *h* (and the corresponding validator set VS1).
 * As part of bisection header verification, it verifies the header at height *h + k* with new validator set VS2'.

 Consequences:

 * To detect this, a node needs to see both, the forged header and the canonical header from the chain.
 * If this is the case, detecting these kind of attacks is easy as it just requires verifying if processes are signing messages in heights in which they are not part of the validator set.  

 **Remark.** We can have phantom-validator-based attacks as a follow up of equivocation or amnesia based attack where forked state contains validators that are not part of the validator set at the main chain. In this case, they keep signing messages contributed to a forked chain (the wrong branch) although they are not part of the validator set on the main chain. This attack can also be used to attack full node during a period of time it is eclipsed.

 ### Lunatic validator

 Lunatic validator agrees to sign commit messages for arbitrary application state. It is used to attack lite clients.
 Note that detecting this behavior require application knowledge. Detecting this behavior can probably be done by
 referring to the block before the one in which height happen.  

 **Q:** can we say that in this case a validator declines to check if a proposed value is valid before voting for it?
--- a/spec/consensus/light/assets/light-node-image.png
+++ b/spec/consensus/light/assets/light-node-image.png
--- a/spec/consensus/light/detection.md
+++ b/spec/consensus/light/detection.md
@ -0,0 +1,3 @@
 # Detection

 TODO
--- a/spec/consensus/light/verification-non-recursive.md
+++ b/spec/consensus/light/verification-non-recursive.md
@ -0,0 +1,612 @@
 # Lite client

 A lite client is a process that connects to Tendermint full node(s) and then tries to verify application
 data using the Merkle proofs.

 ## Problem statement

 We assume that the lite client knows a (base) header *inithead* it trusts (by social consensus or because
 the lite 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.

 ## 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

        // hashes from the app output from the prev block
        ValidatorsHash     []byte        // hash of the validators for the current block
        NextValidatorsHash []byte        // hash of the validators for the next block

        // hashes of block data
       	LastCommitHash []byte            // hash of the commit from validators from the last 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 lite 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 the validator set for the given validator hash
    func validators(validatorsHash []byte) ValidatorSet

    // returns true if commit corresponds to the block data in 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
    // it does not assume signature verification
    func signers(commit Commit, validatorSet ValidatorSet) []Validator

    // return the voting power the validators in v1 have according to their voting power in set v2
    // it assumes signature verification so it can be computationally expensive
    func votingPowerIn(v1 []Validator, v2 ValidatorSet) int64

    // add this state as trusted to the store
    func add(store Store, trustedState TrustedState) error

    // retrieve the trusted state at given height if it exists (error = nil)
    // return an error if there are no trusted state for the given height
    // if height = 0, return the latest trusted state
    func get(store Store, height int64) (TrustedState, error)
 ```


 **VerifyHeaderAtHeight.** TODO.
 ```go
 func VerifyHeaderAtHeight(untrustedHeight int64,
                          trustThreshold TrustThreshold,
                          trustingPeriod Duration,
                          clockDrift Duration,
                          store Store) (error, (TrustedState, Time)) {

    now := System.Time()
    initTrustedState, newTrustedState, err := VerifyAndUpdateNonRecursive(untrustedHeight,
                                                                          trustThreshold,
                                                                          trustingPeriod,
                                                                          clockDrift,
                                                                          now,
                                                                          store Store)

    if err != nil return err

    now = System.Time()
    if !isWithinTrustedPeriod(initTrustedState.SignedHeader.Header, trustingPeriod, now) {
               return ErrHeaderNotWithinTrustedPeriod
    }
    return nil, (newTrustedState, now)
 }
 ```

 If we get some trustedState at time t (now = t),


 **VerifyAndUpdateNonRecursive.** TODO.
 ```go
 func VerifyAndUpdateNonRecursive(untrustedHeight int64,
                                 trustThreshold TrustThreshold,
                                 trustingPeriod Duration,
                                 clockDrift Duration,
                                 now Time,
                                 store Store) error {

    // fetch the latest state and ensure it hasn't expired
    trustedState, error = get(store, 0)
    if error != nil return error

    trustedSh = trustedState.SignedHeader
    trustedHeader = trustedSh.Header
    assert trustedHeader.Height < untrustedHeight AND
           trustedHeader.Time < now

    if !isWithinTrustedPeriod(trustedHeader, trustingPeriod, now) {
        return ErrHeaderNotWithinTrustedPeriod
    }

    th := trustedHeader // th is trusted header

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

    untrustedHeader = untrustedSh.Header
    assert untrustedHeader.Time < now + clockDrift

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

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

    // untrustedHeader is a list of headers that have not passed verifySingle
    untrustedHeaders := [untrustedHeader]

    while true {
        for h in untrustedHeaders {
            // we assume here that iteration is done in the order of header heights
            error = verifySingle(
                         trustedState,
                         untrustedSh,
                         untrustedVs,
                         untrustedNextVs,
                         trustThreshold)

            if err == nil {
                // the untrusted header is now trusted. update the store
                trustedState = TrustedState(untrustedSh, untrustedNextVs)
                add(store, trustedState)

                untrustedHeaders.RemoveHeadersSmallerOrEqual(h.Header.Height)
                if trustedState.SignedHeader.Header == untrustedSh.Header {
                    return nil
                }
            }
            if fatalError(err) { return err }
        }

        endHeight = min(untrustedHeaders)
        while true {
            trustedSh = trustedState.SignedHeader
            trustedHeader = trustedSh.Header
            pivotHeight := ceil((trustedHeader.Height + endHeight) / 2)

            untrustedSh, error := Commit(pivotHeight)
            if error != nil return error

            untrustedHeader = untrustedSh.Header
            assert untrustedHeader.Time < now + clockDrift

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

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

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

            if fatalError(error) return error

            if err == nil {
                trustedState = TrustedState(untrustedSh, untrustedNextVs)
                add(store, trustedState)
                break
            }

            untrustedHeaders.add(untrustedHeader)
            endHeight = pivot
        }
    }
    return nil // this line should never be reached
 }
 ```



 The function `CanTrust` checks whether to trust header `untrusted_h` based on the trusted header `trusted_h` It does so by (potentially)
 building transitive trust relation between `trusted_h` and `untrusted_h`, over some intermediate headers. For example, in case we cannot trust
 header `untrusted_h` based on the trusted header `trusted_h`, the function `CanTrust` will try to find headers such that we can transition trust
 from `trusted_h` over intermediate headers to `untrusted_h`. We will give two implementations of `CanTrust`, the one based
 on bisection that is recursive and the other that is non-recursive. We give two implementations as recursive version might be easier
 to understand but non-recursive version might be simpler to formally express and verify using TLA+/TLC.

 Both implementations of `CanTrust` function are based on `CheckSupport` function that implements the skipping conditions under which we can trust a
 header `untrusted_h` given the trust in the header `trusted_h` as a single step,
 i.e., it does not assume ensuring transitive trust relation between headers through some intermediate headers.


 ```go
 // return nil in case we can trust header untrusted_h based on header trusted_h; otherwise return error
 // where error captures the nature of the error.
 // Note that untrusted_h must have been verified by the caller, i.e. verify(untrusted_h) was successful.
 func CanTrust(trusted_h,untrusted_h,trustThreshold) error {
  assert trusted_h.Header.Height < untrusted_h.header.Height

  th := trusted_h // th is trusted header
  // untrustedHeader is a list of (?) verified headers that have not passed CheckSupport()
  untrustedHeaders := [untrusted_h]

  while true {
    for h in untrustedHeaders {
        // we assume here that iteration is done in the order of header heights
        err = CheckSupport(th,h,trustThreshold)
        if err == nil {
            if !verify(h) { return ErrInvalidHeader(h) }
            th = h
            Store.Add(h)
            untrustedHeaders.RemoveHeadersSmallerOrEqual(h.Header.Height)
            if th == untrusted_h { return nil }
        }
        if fatalCheckSupportError(err) { return err }
    }

    endHeight = min(untrustedHeaders)
    while true {
        pivot := ceil((th.Header.height + endHeight) / 2)
        hp := Commit(pivot)
        // try to move trusted header forward to hp
        err = CheckSupport(th,hp,trustThreshold)
        if fatalCheckSupportError(err) return err
        if err == nil {
            if !verify(hp) { return ErrInvalidHeader(hp) }
            th = hp
            Store.Add(th)
            break
        }
        untrustedHeaders.add(hp)
        endHeight = pivot
    }
  }
  return nil // this line should never be reached
 }

 func CheckSupport(trusted_h,untrusted_h,trustThreshold) error {
    assert trusted_h.Header.Height < untrusted_h.header.Height and
           trusted_h.Header.bfttime < untrusted_h.Header.bfttime and
           untrusted_h.Header.bfttime < now

    if !isWithinTrustedPeriod(trusted_h) return ErrHeaderNotWithinTrustedPeriod(trusted_h)

    // Although while executing the rest of CheckSupport function, trusted_h can expire based
    // on the lite client trusted period, this is not problem as lite client trusted
    // period is smaller than trusted period of the header based on Tendermint Failure
    // model, i.e., there is a significant time period (measure in days) during which
    // validator set that has signed trusted_h can be trusted. Furthermore, CheckSupport function
    // is not doing expensive operation (neither rpc nor signature verification), so it
    // should execute fast.

    // check for adjacent headers
    if untrusted_h.Header.height == trusted_h.Header.height + 1 {
        if trusted_h.Header.NextV == untrusted_h.Header.V
            return nil
        return ErrInvalidAdjacentHeaders
    }

    // total sum of voting power of validators in trusted_h.NextV
    vp_all := totalVotingPower(trusted_h.Header.NextV)

    // check for non-adjacent headers
    if votingPowerIn(signers(untrusted_h.Commit),trusted_h.Header.NextV) > max(1/3,trustThreshold) * vp_all {
        return nil
    }
    return ErrTooMuchChange
 }

 func fatalCheckSupportError(err) bool {
    return err == ErrHeaderNotWithinTrustedPeriod or err == ErrInvalidAdjacentHeaders
 ```

 ```go
 func CanTrustBisection(trusted_h,untrusted_h,trustThreshold) error {
  assume trusted_h.Header.Height < untrusted_h.header.Height

  err = CheckSupport(trusted_h,untrusted_h,trustThreshold)
  if err == nil {
    Store.Add(untrusted_h)
    return nil
  }
  if err != ErrTooMuchChange return err

  pivot := (trusted_h.Header.height + untrusted_h.Header.height) / 2
  hp := Commit(pivot)
  if !verify(hp) return ErrInvalidHeader(hp)

  err = CanTrustBisection(trusted_h,hp,trustThreshold)
  if err == nil {
      Store.Add(hp)
      err2 = CanTrustBisection(hp,untrusted_h,trustThreshold)
      if err2 == nil {
        Store.Add(untrusted_h)
        return nil
      }
      return err2
  }
  return err
 }
 ```

 **CheckSupport.** The following function defines skipping condition under the Tendermint Failure model, i.e., it defines when we can trust the header untrusted_h based on header trusted_h.
 Time validity of a header is captured by the ```isWithinTrustedPeriod``` function that depends on lite client trusted period (`LITE_CLIENT_TRUSTED_PERIOD`) and it returns
 true in case the header is within its lite client trusted period.
 ```verify``` function is capturing basic header verification, i.e., it ensures that the header is signed by more than 2/3 of the voting power of the corresponding validator set.

 ```go
  // Captures skipping condition. trusted_h and untrusted_h have already passed basic validation
  // (function `verify`).
  // Returns nil in case untrusted_h can be trusted based on trusted_h, otherwise returns error.
  // ErrHeaderNotWithinTrustedPeriod is used when trusted_h has expired with respect to lite client trusted period,
  // ErrInvalidAdjacentHeaders when that adjacent headers are not consistent and
  // ErrTooMuchChange when there is not enough intersection between validator sets to have
  // skipping condition true.
  func CheckSupport(trusted_h,untrusted_h,trustThreshold) error {
    assert trusted_h.Header.Height < untrusted_h.header.Height and
           trusted_h.Header.bfttime < untrusted_h.Header.bfttime and
           untrusted_h.Header.bfttime < now

    if !isWithinTrustedPeriod(trusted_h) return ErrHeaderNotWithinTrustedPeriod(trusted_h)

    // Although while executing the rest of CheckSupport function, trusted_h can expire based
    // on the lite client trusted period, this is not problem as lite client trusted
    // period is smaller than trusted period of the header based on Tendermint Failure
    // model, i.e., there is a significant time period (measure in days) during which
    // validator set that has signed trusted_h can be trusted. Furthermore, CheckSupport function
    // is not doing expensive operation (neither rpc nor signature verification), so it
    // should execute fast.

    // check for adjacent headers
    if untrusted_h.Header.height == trusted_h.Header.height + 1 {
        if trusted_h.Header.NextV == untrusted_h.Header.V
            return nil
        return ErrInvalidAdjacentHeaders
    }

    // total sum of voting power of validators in trusted_h.NextV
    vp_all := totalVotingPower(trusted_h.Header.NextV)

    // check for non-adjacent headers
    if votingPowerIn(signers(untrusted_h.Commit),trusted_h.Header.NextV) > max(1/3,trustThreshold) * vp_all {
        return nil
    }
    return ErrTooMuchChange
  }
 ```


 ### The case `untrusted_h.Header.height < trusted_h.Header.height`

 In the use case where someone tells the lite client that application data that is relevant for it
 can be read in the block of height `k` and the lite 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 lite 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 Backwards(trusted_h,untrusted_h) error {
  assert (untrusted_h.Header.height < trusted_h.Header.height)
  if !isWithinTrustedPeriod(trusted_h) return ErrHeaderNotTrusted(trusted_h)

  old := trusted_h
  for i := trusted_h.Header.height - 1; i > untrusted_h.Header.height; i-- {
    new := Commit(i)
    if (hash(new) != old.Header.hash) {
      return ErrInvalidAdjacentHeaders
    }
    old := new
    if !isWithinTrustedPeriod(trusted_h) return ErrHeaderNotTrusted(trusted_h)
  }
  if hash(untrusted_h) != old.Header.hash return ErrInvalidAdjacentHeaders
  return nil
 }
 ```



 In order to incentivize correct behavior of validators that run Tendermint consensus protocol, fork detection protocol (it will be explained in different document) is executed in case of a fork (conflicting
 headers are detected). As detecting conflicting headers, its propagation through the network (by the gossip protocol) and execution of the fork accountability
 protocol on the chain takes time, the lite client logic assumes conservative value for trusted period. More precisely, in the context of lite client we always
 operate with a smaller trusted period that we call *lite client trusted period* (LITE_CLIENT_TRUSTED_PERIOD). If we assume that upper bound
 for fork detection, propagation and processing on the chain is denoted with *fork procession period* (FORK_PROCESSING_PERIOD), then the following formula
 holds:
 ```LITE_CLIENT_TRUSTED_PERIOD + FORK_PROCESSING_PERIOD < TRUSTED_PERIOD```, where TRUSTED_PERIOD comes from the Tendermint Failure Model.


 *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 lite client communicates with one full node
 - the lite client locally stores all the headers that has passed basic verification and that are within lite 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 lite 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 lite client should disconnect and reinitialise with new peer. If the trusted header has expired,
  we need to reinitialise lite 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).



 ## Context of this document

 In order to make sure that full nodes have the incentive to follow the protocol, we have to address the
 following three Issues

 1) The lite client needs a method to verify headers it obtains from a full node it connects to according to trust assumptions -- this document.

 2) The lite client must be able to connect to other full nodes to detect and report on failures in the trust assumptions (i.e., conflicting headers) -- a future document (see #4215).

 3) In the event the trust assumption fails (i.e., a lite client is fooled by a conflicting header), the Tendermint fork accountability protocol must account for the evidence -- a future document (see #3840).

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

 * For each header *h* it has locally stored, the lite client stores whether
    it trusts *h*. We write *trust(h) = true*, if this is the case.

 * signed header fields: contains a header and a  *commit* for the current header; a "seen commit".
  In Tendermint consensus the "canonical commit" is stored in header *height* + 1.


  * Validator fields. We will write a validator as a tuple *(v,p)* such that
    + *v* is the identifier (we assume identifiers are unique in each validator set)
    + *p* is its voting power

 ### Definitions

 * *TRUSTED_PERIOD*: trusting 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).


 ### Tendermint Failure Model

 If a block *b* is generated at time *Time* (and this time is stored in the block), then 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```.

 Formally,
 \[
 \sum_{(v,p) \in h.Header.NextV \wedge correct(v,h.Header.bfttime + TRUSTED_PERIOD)} p >
 2/3 \sum_{(v,p) \in h.Header.NextV} p
 \]


 ## Lite Client Trusting Spec

 The lite 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:

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

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

 *Remark*: If in the course of the computation, the lite 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.Header.bfttime + tp*. If not, the block cannot be trusted because it is too old.

 *Remark*: If a header *h* is marked with *trust(h)*, but it is too old (its bfttime is more than *tp* ago), then the lite client should set *trust(h)* to false again.

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

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

 *Verification Condition: Lite Client Invariant.*
 For each lite client *l* and each header *h*:
 if *l* has set *trust(h) = true*,
  then validators that are correct until time *h.Header.bfttime + tp* have more than two thirds of the voting power in *h.Header.NextV*.

  Formally,
  \[
  \sum_{(v,p) \in h.Header.NextV \wedge correct(v,h.Header.bfttime + tp)} p >
  2/3 \sum_{(v,p) \in h.Header.NextV} p
  \]

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


 ## High Level Solution

 Upon initialization, the lite client is given a header *inithead* it trusts (by
 social consensus). It is assumed that *inithead* satisfies the lite client invariant. (If *inithead* has been correctly generated by Tendermint consensus, the invariant follows from the Tendermint Failure Model.)
 Note that the *inithead* should be within its trusted period during initialization.

 When a lite clients sees a signed new 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 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 lite client knows all headers in the prefix.
 Intuitively, a trusted validator set is assumed to only chose a new validator set that will obey the Tendermint Failure Model.

 2. **Trusting period.** Based on a trusted block *h*, and the lite client
 invariant, which ensures the fault assumption during the trusting period, we can check whether at least one  validator, that has been continuously correct from *h.Header.bfttime* until now, has signed *snh*.
 If this is the case, similarly to above, the chosen validator set in *snh* does not violate the Tendermint Failure Model.

 3. **Bisection.** If a check according to the trusting period fails, the lite client can try to obtain a header *hp* whose height lies between *h* and *snh* 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 *snh*; if not, we may continue recursively.

 ## How to use it

 We consider the following use case:
 the lite client wants to verify a header for some given height *k*. Thus:
  - it requests the signed header for height *k* from a full node
  - it tries to verify this header with the methods described here.

 This can be used in several settings:
  - someone tells the lite client that application data that is relevant for it can be read in the block of height *k*.
  - the lite clients wants the latest state. It asks a full nude for the current height, and uses the response for *k*.
  - in case of inter-blockchain communication protocol (IBC) the light client runs on a chain and someone feeds it
  signed headers as input and it computes whether it can trust it.


 ## Details

 **Observation 1.** If *h.Header.bfttime + tp > now*, we trust the old
 validator set *h.Header.NextV*.

 When we say we trust *h.Header.NextV* we do *not* trust that each individual validator in *h.Header.NextV* 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).



 *Correctness arguments*

 Towards Lite Client Accuracy:
 - Assume by contradiction that `untrusted_h` was not generated correctly and the lite client sets trust to true because `CheckSupport` returns true.
 - trusted_h is trusted and sufficiently new
 - by Tendermint Fault Model, less than 1/3 of voting power held by faulty validators => at least one correct validator *v* has signed `untrusted_h`.
 - as *v* is correct up to now, it followed the Tendermint consensus protocol at least up to signing `untrusted_h` => `untrusted_h` was correctly generated, we arrive at the required contradiction.


 Towards Lite Client Completeness:
 - The check is successful if sufficiently many validators of `trusted_h` are still validators in `untrusted_h` and signed `untrusted_h`.
 - If *untrusted_h.Header.height = trusted_h.Header.height + 1*, and both headers were generated correctly, the test passes

 *Verification Condition:* We may need a Tendermint invariant stating that if *untrusted_h.Header.height = trusted_h.Header.height + 1* then *signers(untrusted_h.Commit) \subseteq trusted_h.Header.NextV*.

 *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 CheckSupport returns true for non-adjacent headers.




 *Correctness arguments (sketch)*

 Lite Client Accuracy:
 - Assume by contradiction that `untrusted_h` was not generated correctly and the lite client sets trust to true because CanTrustBisection returns nil.
 - CanTrustBisection returns true only if all calls to CheckSupport in the recursion return nil.
 - Thus we have a sequence of headers that all satisfied the CheckSupport
 - again a contradiction

 Lite Client Completeness:

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

 *Stalling*

 With CanTrustBisection, a faulty full node could stall a lite client by creating a long sequence of headers that are queried one-by-one by the lite client and look OK, before the lite 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 lite 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, Bisection would then be executed at the full node.
 * We may set a timeout how long bisection may take.





--- a/spec/consensus/light/verification.md
+++ b/spec/consensus/light/verification.md
@ -0,0 +1,587 @@
 # Core Verification

 A lite client is a process that connects to Tendermint full node(s) and then tries to verify application
 data using the Merkle proofs.

 ## Problem statement

 We assume that the lite client knows a (base) header *inithead* it trusts (by social consensus or because
 the lite 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.

 ## 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
        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 lite 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

    // return 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
 ```

 ### Failure Model

 For the purpose of model definitions we assume that there exists a function
 `validators` that returns the corresponding validator set for the given hash.
 The lite client specification 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](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 lite 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 lite 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 lite 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 `PUNISHMENT_PERIOD`).
 Furthermore, we assume that `TRUSTED_PERIOD < PUNISHMENT_PERIOD` and that they are normally of the same order of magnitude, for example
 `TRUSTED_PERIOD = PUNISHMENT_PERIOD / 2`. Note that `PUNISHMENT_PERIOD` is often referred to as an
 unbonding period due to the "bonding" mechanism in modern proof of stake systems.

 The specification in this document considers an implementation of the lite client under the Failure Model defined above.
 Mechanisms like `fork accountability` and `evidence submission` are defined in the context of `PUNISHMENT_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](fork-accountability.md).

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

 ### Functions

 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 assume `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 lite 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`.


 **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 lite 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`.

 **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 `untrusted_h.Header.height < trusted_h.Header.height`

 In the use case where someone tells the lite client that application data that is relevant for it 
 can be read in the block of height `k` and the lite 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 lite 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 Backwards(trusted_h,untrusted_h) error {
  assert (untrusted_h.Header.height < trusted_h.Header.height)
  if !isWithinTrustedPeriod(trusted_h) return ErrHeaderNotTrusted(trusted_h)

  old := trusted_h
  for i := trusted_h.Header.height - 1; i > untrusted_h.Header.height; i-- {
    new := Commit(i)
    if (hash(new) != old.Header.hash) {
      return ErrInvalidAdjacentHeaders
    }
    old := new
    if !isWithinTrustedPeriod(trusted_h) return ErrHeaderNotTrusted(trusted_h)
  }
  if hash(untrusted_h) != old.Header.hash return ErrInvalidAdjacentHeaders
  return nil
 }
 ```

 In order to incentivize correct behavior of validators that run Tendermint consensus protocol, fork detection protocol (it will be explained in different document) is executed in case of a fork (conflicting
 headers are detected). As detecting conflicting headers, its propagation through the network (by the gossip protocol) and execution of the fork accountability
 protocol on the chain takes time, the lite client logic assumes conservative value for trusted period. More precisely, in the context of lite client we always
 operate with a smaller trusted period that we call *lite client trusted period* (LITE_CLIENT_TRUSTED_PERIOD). If we assume that upper bound
 for fork detection, propagation and processing on the chain is denoted with *fork procession period* (FORK_PROCESSING_PERIOD), then the following formula
 holds:
 ```LITE_CLIENT_TRUSTED_PERIOD + FORK_PROCESSING_PERIOD < TRUSTED_PERIOD```, where TRUSTED_PERIOD comes from the Tendermint Failure Model.


 *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 lite client communicates with one full node
 - the lite client locally stores all the headers that has passed basic verification and that are within lite 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 lite 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 lite client should disconnect and reinitialise with new peer. If the trusted header has expired,
  we need to reinitialise lite 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).



 ## Context of this document

 In order to make sure that full nodes have the incentive to follow the protocol, we have to address the
 following three Issues

 1) The lite client needs a method to verify headers it obtains from a full node it connects to according to trust assumptions -- this document.

 2) The lite client must be able to connect to other full nodes to detect and report on failures in the trust assumptions (i.e., conflicting headers) -- a future document (see #4215).

 3) In the event the trust assumption fails (i.e., a lite client is fooled by a conflicting header), the Tendermint fork accountability protocol must account for the evidence -- a future document (see #3840).

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

 * For each header *h* it has locally stored, the lite client stores whether
    it trusts *h*. We write *trust(h) = true*, if this is the case.

 * signed header fields: contains a header and a  *commit* for the current header; a "seen commit".
  In Tendermint consensus the "canonical commit" is stored in header *height* + 1.


  * Validator fields. We will write a validator as a tuple *(v,p)* such that
    + *v* is the identifier (we assume identifiers are unique in each validator set)
    + *p* is its voting power

 ### Definitions

 * *TRUSTED_PERIOD*: trusting 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).


 ### Tendermint Failure Model

 If a block *b* is generated at time *Time* (and this time is stored in the block), then 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```.

 Formally,
 \[
 \sum_{(v,p) \in h.Header.NextV \wedge correct(v,h.Header.bfttime + TRUSTED_PERIOD)} p >
 2/3 \sum_{(v,p) \in h.Header.NextV} p
 \]


 ## Lite Client Trusting Spec

 The lite 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:

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

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

 *Remark*: If in the course of the computation, the lite 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.Header.bfttime + tp*. If not, the block cannot be trusted because it is too old.

 *Remark*: If a header *h* is marked with *trust(h)*, but it is too old (its bfttime is more than *tp* ago), then the lite client should set *trust(h)* to false again.

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

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

 *Verification Condition: Lite Client Invariant.*
 For each lite client *l* and each header *h*:
 if *l* has set *trust(h) = true*,
  then validators that are correct until time *h.Header.bfttime + tp* have more than two thirds of the voting power in *h.Header.NextV*.

  Formally,
  \[
  \sum_{(v,p) \in h.Header.NextV \wedge correct(v,h.Header.bfttime + tp)} p >
  2/3 \sum_{(v,p) \in h.Header.NextV} p
  \]

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


 ## High Level Solution

 Upon initialization, the lite client is given a header *inithead* it trusts (by
 social consensus). It is assumed that *inithead* satisfies the lite client invariant. (If *inithead* has been correctly generated by Tendermint consensus, the invariant follows from the Tendermint Failure Model.)
 Note that the *inithead* should be within its trusted period during initialization.

 When a lite clients sees a signed new 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 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 lite client knows all headers in the prefix.
 Intuitively, a trusted validator set is assumed to only chose a new validator set that will obey the Tendermint Failure Model.

 2. **Trusting period.** Based on a trusted block *h*, and the lite client
 invariant, which ensures the fault assumption during the trusting period, we can check whether at least one  validator, that has been continuously correct from *h.Header.bfttime* until now, has signed *snh*.
 If this is the case, similarly to above, the chosen validator set in *snh* does not violate the Tendermint Failure Model.

 3. **Bisection.** If a check according to the trusting period fails, the lite client can try to obtain a header *hp* whose height lies between *h* and *snh* 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 *snh*; if not, we may continue recursively.

 ## How to use it

 We consider the following use case:
 the lite client wants to verify a header for some given height *k*. Thus:
  - it requests the signed header for height *k* from a full node
  - it tries to verify this header with the methods described here.

 This can be used in several settings:
  - someone tells the lite client that application data that is relevant for it can be read in the block of height *k*.
  - the lite clients wants the latest state. It asks a full nude for the current height, and uses the response for *k*.
  - in case of inter-blockchain communication protocol (IBC) the light client runs on a chain and someone feeds it
  signed headers as input and it computes whether it can trust it.


 ## Details

 **Observation 1.** If *h.Header.bfttime + tp > now*, we trust the old
 validator set *h.Header.NextV*.

 When we say we trust *h.Header.NextV* we do *not* trust that each individual validator in *h.Header.NextV* 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).



 *Correctness arguments*

 Towards Lite Client Accuracy:
 - Assume by contradiction that `untrusted_h` was not generated correctly and the lite client sets trust to true because `CheckSupport` returns true.
 - trusted_h is trusted and sufficiently new
 - by Tendermint Fault Model, less than 1/3 of voting power held by faulty validators => at least one correct validator *v* has signed `untrusted_h`.
 - as *v* is correct up to now, it followed the Tendermint consensus protocol at least up to signing `untrusted_h` => `untrusted_h` was correctly generated, we arrive at the required contradiction.


 Towards Lite Client Completeness:
 - The check is successful if sufficiently many validators of `trusted_h` are still validators in `untrusted_h` and signed `untrusted_h`.
 - If *untrusted_h.Header.height = trusted_h.Header.height + 1*, and both headers were generated correctly, the test passes

 *Verification Condition:* We may need a Tendermint invariant stating that if *untrusted_h.Header.height = trusted_h.Header.height + 1* then *signers(untrusted_h.Commit) \subseteq trusted_h.Header.NextV*.

 *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 CheckSupport returns true for non-adjacent headers.




 *Correctness arguments (sketch)*

 Lite Client Accuracy:
 - Assume by contradiction that `untrusted_h` was not generated correctly and the lite client sets trust to true because CanTrustBisection returns nil.
 - CanTrustBisection returns true only if all calls to CheckSupport in the recursion return nil.
 - Thus we have a sequence of headers that all satisfied the CheckSupport
 - again a contradiction

 Lite Client Completeness:

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

 *Stalling*

 With CanTrustBisection, a faulty full node could stall a lite client by creating a long sequence of headers that are queried one-by-one by the lite client and look OK, before the lite 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 lite 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, Bisection would then be executed at the full node.
 * We may set a timeout how long bisection may take.





--- a/spec/consensus/non-recursive-light-client.md
+++ b/spec/consensus/non-recursive-light-client.md
@ -1,612 +1,3 @@
 # Lite client

 A lite client is a process that connects to Tendermint full node(s) and then tries to verify application
 data using the Merkle proofs.

 ## Problem statement

 We assume that the lite client knows a (base) header *inithead* it trusts (by social consensus or because
 the lite 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.

 ## 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

        // hashes from the app output from the prev block
        ValidatorsHash     []byte        // hash of the validators for the current block
        NextValidatorsHash []byte        // hash of the validators for the next block

        // hashes of block data
       	LastCommitHash []byte            // hash of the commit from validators from the last 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 lite 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 the validator set for the given validator hash
    func validators(validatorsHash []byte) ValidatorSet

    // returns true if commit corresponds to the block data in 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
    // it does not assume signature verification
    func signers(commit Commit, validatorSet ValidatorSet) []Validator

    // return the voting power the validators in v1 have according to their voting power in set v2
    // it assumes signature verification so it can be computationally expensive
    func votingPowerIn(v1 []Validator, v2 ValidatorSet) int64

    // add this state as trusted to the store
    func add(store Store, trustedState TrustedState) error

    // retrieve the trusted state at given height if it exists (error = nil)
    // return an error if there are no trusted state for the given height
    // if height = 0, return the latest trusted state
    func get(store Store, height int64) (TrustedState, error)
 ```


 **VerifyHeaderAtHeight.** TODO.
 ```go
 func VerifyHeaderAtHeight(untrustedHeight int64,
                          trustThreshold TrustThreshold,
                          trustingPeriod Duration,
                          clockDrift Duration,
                          store Store) (error, (TrustedState, Time)) {

    now := System.Time()
    initTrustedState, newTrustedState, err := VerifyAndUpdateNonRecursive(untrustedHeight,
                                                                          trustThreshold,
                                                                          trustingPeriod,
                                                                          clockDrift,
                                                                          now,
                                                                          store Store)

    if err != nil return err

    now = System.Time()
    if !isWithinTrustedPeriod(initTrustedState.SignedHeader.Header, trustingPeriod, now) {
               return ErrHeaderNotWithinTrustedPeriod
    }
    return nil, (newTrustedState, now)
 }
 ```

 If we get some trustedState at time t (now = t),


 **VerifyAndUpdateNonRecursive.** TODO.
 ```go
 func VerifyAndUpdateNonRecursive(untrustedHeight int64,
                                 trustThreshold TrustThreshold,
                                 trustingPeriod Duration,
                                 clockDrift Duration,
                                 now Time,
                                 store Store) error {

    // fetch the latest state and ensure it hasn't expired
    trustedState, error = get(store, 0)
    if error != nil return error

    trustedSh = trustedState.SignedHeader
    trustedHeader = trustedSh.Header
    assert trustedHeader.Height < untrustedHeight AND
           trustedHeader.Time < now

    if !isWithinTrustedPeriod(trustedHeader, trustingPeriod, now) {
        return ErrHeaderNotWithinTrustedPeriod
    }

    th := trustedHeader // th is trusted header

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

    untrustedHeader = untrustedSh.Header
    assert untrustedHeader.Time < now + clockDrift

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

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

    // untrustedHeader is a list of headers that have not passed verifySingle
    untrustedHeaders := [untrustedHeader]

    while true {
        for h in untrustedHeaders {
            // we assume here that iteration is done in the order of header heights
            error = verifySingle(
                         trustedState,
                         untrustedSh,
                         untrustedVs,
                         untrustedNextVs,
                         trustThreshold)

            if err == nil {
                // the untrusted header is now trusted. update the store
                trustedState = TrustedState(untrustedSh, untrustedNextVs)
                add(store, trustedState)

                untrustedHeaders.RemoveHeadersSmallerOrEqual(h.Header.Height)
                if trustedState.SignedHeader.Header == untrustedSh.Header {
                    return nil
                }
            }
            if fatalError(err) { return err }
        }

        endHeight = min(untrustedHeaders)
        while true {
            trustedSh = trustedState.SignedHeader
            trustedHeader = trustedSh.Header
            pivotHeight := ceil((trustedHeader.Height + endHeight) / 2)

            untrustedSh, error := Commit(pivotHeight)
            if error != nil return error

            untrustedHeader = untrustedSh.Header
            assert untrustedHeader.Time < now + clockDrift

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

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

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

            if fatalError(error) return error

            if err == nil {
                trustedState = TrustedState(untrustedSh, untrustedNextVs)
                add(store, trustedState)
                break
            }

            untrustedHeaders.add(untrustedHeader)
            endHeight = pivot
        }
    }
    return nil // this line should never be reached
 }
 ```



 The function `CanTrust` checks whether to trust header `untrusted_h` based on the trusted header `trusted_h` It does so by (potentially)
 building transitive trust relation between `trusted_h` and `untrusted_h`, over some intermediate headers. For example, in case we cannot trust
 header `untrusted_h` based on the trusted header `trusted_h`, the function `CanTrust` will try to find headers such that we can transition trust
 from `trusted_h` over intermediate headers to `untrusted_h`. We will give two implementations of `CanTrust`, the one based
 on bisection that is recursive and the other that is non-recursive. We give two implementations as recursive version might be easier
 to understand but non-recursive version might be simpler to formally express and verify using TLA+/TLC.

 Both implementations of `CanTrust` function are based on `CheckSupport` function that implements the skipping conditions under which we can trust a
 header `untrusted_h` given the trust in the header `trusted_h` as a single step,
 i.e., it does not assume ensuring transitive trust relation between headers through some intermediate headers.


 ```go
 // return nil in case we can trust header untrusted_h based on header trusted_h; otherwise return error
 // where error captures the nature of the error.
 // Note that untrusted_h must have been verified by the caller, i.e. verify(untrusted_h) was successful.
 func CanTrust(trusted_h,untrusted_h,trustThreshold) error {
  assert trusted_h.Header.Height < untrusted_h.header.Height

  th := trusted_h // th is trusted header
  // untrustedHeader is a list of (?) verified headers that have not passed CheckSupport()
  untrustedHeaders := [untrusted_h]

  while true {
    for h in untrustedHeaders {
        // we assume here that iteration is done in the order of header heights
        err = CheckSupport(th,h,trustThreshold)
        if err == nil {
            if !verify(h) { return ErrInvalidHeader(h) }
            th = h
            Store.Add(h)
            untrustedHeaders.RemoveHeadersSmallerOrEqual(h.Header.Height)
            if th == untrusted_h { return nil }
        }
        if fatalCheckSupportError(err) { return err }
    }

    endHeight = min(untrustedHeaders)
    while true {
        pivot := ceil((th.Header.height + endHeight) / 2)
        hp := Commit(pivot)
        // try to move trusted header forward to hp
        err = CheckSupport(th,hp,trustThreshold)
        if fatalCheckSupportError(err) return err
        if err == nil {
            if !verify(hp) { return ErrInvalidHeader(hp) }
            th = hp
            Store.Add(th)
            break
        }
        untrustedHeaders.add(hp)
        endHeight = pivot
    }
  }
  return nil // this line should never be reached
 }

 func CheckSupport(trusted_h,untrusted_h,trustThreshold) error {
    assert trusted_h.Header.Height < untrusted_h.header.Height and
           trusted_h.Header.bfttime < untrusted_h.Header.bfttime and
           untrusted_h.Header.bfttime < now

    if !isWithinTrustedPeriod(trusted_h) return ErrHeaderNotWithinTrustedPeriod(trusted_h)

    // Although while executing the rest of CheckSupport function, trusted_h can expire based
    // on the lite client trusted period, this is not problem as lite client trusted
    // period is smaller than trusted period of the header based on Tendermint Failure
    // model, i.e., there is a significant time period (measure in days) during which
    // validator set that has signed trusted_h can be trusted. Furthermore, CheckSupport function
    // is not doing expensive operation (neither rpc nor signature verification), so it
    // should execute fast.

    // check for adjacent headers
    if untrusted_h.Header.height == trusted_h.Header.height + 1 {
        if trusted_h.Header.NextV == untrusted_h.Header.V
            return nil
        return ErrInvalidAdjacentHeaders
    }

    // total sum of voting power of validators in trusted_h.NextV
    vp_all := totalVotingPower(trusted_h.Header.NextV)

    // check for non-adjacent headers
    if votingPowerIn(signers(untrusted_h.Commit),trusted_h.Header.NextV) > max(1/3,trustThreshold) * vp_all {
        return nil
    }
    return ErrTooMuchChange
 }

 func fatalCheckSupportError(err) bool {
    return err == ErrHeaderNotWithinTrustedPeriod or err == ErrInvalidAdjacentHeaders
 ```

 ```go
 func CanTrustBisection(trusted_h,untrusted_h,trustThreshold) error {
  assume trusted_h.Header.Height < untrusted_h.header.Height

  err = CheckSupport(trusted_h,untrusted_h,trustThreshold)
  if err == nil {
    Store.Add(untrusted_h)
    return nil
  }
  if err != ErrTooMuchChange return err

  pivot := (trusted_h.Header.height + untrusted_h.Header.height) / 2
  hp := Commit(pivot)
  if !verify(hp) return ErrInvalidHeader(hp)

  err = CanTrustBisection(trusted_h,hp,trustThreshold)
  if err == nil {
      Store.Add(hp)
      err2 = CanTrustBisection(hp,untrusted_h,trustThreshold)
      if err2 == nil {
        Store.Add(untrusted_h)
        return nil
      }
      return err2
  }
  return err
 }
 ```

 **CheckSupport.** The following function defines skipping condition under the Tendermint Failure model, i.e., it defines when we can trust the header untrusted_h based on header trusted_h.
 Time validity of a header is captured by the ```isWithinTrustedPeriod``` function that depends on lite client trusted period (`LITE_CLIENT_TRUSTED_PERIOD`) and it returns
 true in case the header is within its lite client trusted period.
 ```verify``` function is capturing basic header verification, i.e., it ensures that the header is signed by more than 2/3 of the voting power of the corresponding validator set.

 ```go
  // Captures skipping condition. trusted_h and untrusted_h have already passed basic validation
  // (function `verify`).
  // Returns nil in case untrusted_h can be trusted based on trusted_h, otherwise returns error.
  // ErrHeaderNotWithinTrustedPeriod is used when trusted_h has expired with respect to lite client trusted period,
  // ErrInvalidAdjacentHeaders when that adjacent headers are not consistent and
  // ErrTooMuchChange when there is not enough intersection between validator sets to have
  // skipping condition true.
  func CheckSupport(trusted_h,untrusted_h,trustThreshold) error {
    assert trusted_h.Header.Height < untrusted_h.header.Height and
           trusted_h.Header.bfttime < untrusted_h.Header.bfttime and
           untrusted_h.Header.bfttime < now

    if !isWithinTrustedPeriod(trusted_h) return ErrHeaderNotWithinTrustedPeriod(trusted_h)

    // Although while executing the rest of CheckSupport function, trusted_h can expire based
    // on the lite client trusted period, this is not problem as lite client trusted
    // period is smaller than trusted period of the header based on Tendermint Failure
    // model, i.e., there is a significant time period (measure in days) during which
    // validator set that has signed trusted_h can be trusted. Furthermore, CheckSupport function
    // is not doing expensive operation (neither rpc nor signature verification), so it
    // should execute fast.

    // check for adjacent headers
    if untrusted_h.Header.height == trusted_h.Header.height + 1 {
        if trusted_h.Header.NextV == untrusted_h.Header.V
            return nil
        return ErrInvalidAdjacentHeaders
    }

    // total sum of voting power of validators in trusted_h.NextV
    vp_all := totalVotingPower(trusted_h.Header.NextV)

    // check for non-adjacent headers
    if votingPowerIn(signers(untrusted_h.Commit),trusted_h.Header.NextV) > max(1/3,trustThreshold) * vp_all {
        return nil
    }
    return ErrTooMuchChange
  }
 ```


 ### The case `untrusted_h.Header.height < trusted_h.Header.height`

 In the use case where someone tells the lite client that application data that is relevant for it
 can be read in the block of height `k` and the lite 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 lite 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 Backwards(trusted_h,untrusted_h) error {
  assert (untrusted_h.Header.height < trusted_h.Header.height)
  if !isWithinTrustedPeriod(trusted_h) return ErrHeaderNotTrusted(trusted_h)

  old := trusted_h
  for i := trusted_h.Header.height - 1; i > untrusted_h.Header.height; i-- {
    new := Commit(i)
    if (hash(new) != old.Header.hash) {
      return ErrInvalidAdjacentHeaders
    }
    old := new
    if !isWithinTrustedPeriod(trusted_h) return ErrHeaderNotTrusted(trusted_h)
  }
  if hash(untrusted_h) != old.Header.hash return ErrInvalidAdjacentHeaders
  return nil
 }
 ```



 In order to incentivize correct behavior of validators that run Tendermint consensus protocol, fork detection protocol (it will be explained in different document) is executed in case of a fork (conflicting
 headers are detected). As detecting conflicting headers, its propagation through the network (by the gossip protocol) and execution of the fork accountability
 protocol on the chain takes time, the lite client logic assumes conservative value for trusted period. More precisely, in the context of lite client we always
 operate with a smaller trusted period that we call *lite client trusted period* (LITE_CLIENT_TRUSTED_PERIOD). If we assume that upper bound
 for fork detection, propagation and processing on the chain is denoted with *fork procession period* (FORK_PROCESSING_PERIOD), then the following formula
 holds:
 ```LITE_CLIENT_TRUSTED_PERIOD + FORK_PROCESSING_PERIOD < TRUSTED_PERIOD```, where TRUSTED_PERIOD comes from the Tendermint Failure Model.


 *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 lite client communicates with one full node
 - the lite client locally stores all the headers that has passed basic verification and that are within lite 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 lite 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 lite client should disconnect and reinitialise with new peer. If the trusted header has expired,
  we need to reinitialise lite 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).



 ## Context of this document

 In order to make sure that full nodes have the incentive to follow the protocol, we have to address the
 following three Issues

 1) The lite client needs a method to verify headers it obtains from a full node it connects to according to trust assumptions -- this document.

 2) The lite client must be able to connect to other full nodes to detect and report on failures in the trust assumptions (i.e., conflicting headers) -- a future document (see #4215).

 3) In the event the trust assumption fails (i.e., a lite client is fooled by a conflicting header), the Tendermint fork accountability protocol must account for the evidence -- a future document (see #3840).

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

 * For each header *h* it has locally stored, the lite client stores whether
    it trusts *h*. We write *trust(h) = true*, if this is the case.

 * signed header fields: contains a header and a  *commit* for the current header; a "seen commit".
  In Tendermint consensus the "canonical commit" is stored in header *height* + 1.


  * Validator fields. We will write a validator as a tuple *(v,p)* such that
    + *v* is the identifier (we assume identifiers are unique in each validator set)
    + *p* is its voting power

 ### Definitions

 * *TRUSTED_PERIOD*: trusting 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).


 ### Tendermint Failure Model

 If a block *b* is generated at time *Time* (and this time is stored in the block), then 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```.

 Formally,
 \[
 \sum_{(v,p) \in h.Header.NextV \wedge correct(v,h.Header.bfttime + TRUSTED_PERIOD)} p >
 2/3 \sum_{(v,p) \in h.Header.NextV} p
 \]


 ## Lite Client Trusting Spec

 The lite 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:

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

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

 *Remark*: If in the course of the computation, the lite 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.Header.bfttime + tp*. If not, the block cannot be trusted because it is too old.

 *Remark*: If a header *h* is marked with *trust(h)*, but it is too old (its bfttime is more than *tp* ago), then the lite client should set *trust(h)* to false again.

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

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

 *Verification Condition: Lite Client Invariant.*
 For each lite client *l* and each header *h*:
 if *l* has set *trust(h) = true*,
  then validators that are correct until time *h.Header.bfttime + tp* have more than two thirds of the voting power in *h.Header.NextV*.

  Formally,
  \[
  \sum_{(v,p) \in h.Header.NextV \wedge correct(v,h.Header.bfttime + tp)} p >
  2/3 \sum_{(v,p) \in h.Header.NextV} p
  \]

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


 ## High Level Solution

 Upon initialization, the lite client is given a header *inithead* it trusts (by
 social consensus). It is assumed that *inithead* satisfies the lite client invariant. (If *inithead* has been correctly generated by Tendermint consensus, the invariant follows from the Tendermint Failure Model.)
 Note that the *inithead* should be within its trusted period during initialization.

 When a lite clients sees a signed new 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 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 lite client knows all headers in the prefix.
 Intuitively, a trusted validator set is assumed to only chose a new validator set that will obey the Tendermint Failure Model.

 2. **Trusting period.** Based on a trusted block *h*, and the lite client
 invariant, which ensures the fault assumption during the trusting period, we can check whether at least one  validator, that has been continuously correct from *h.Header.bfttime* until now, has signed *snh*.
 If this is the case, similarly to above, the chosen validator set in *snh* does not violate the Tendermint Failure Model.

 3. **Bisection.** If a check according to the trusting period fails, the lite client can try to obtain a header *hp* whose height lies between *h* and *snh* 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 *snh*; if not, we may continue recursively.

 ## How to use it

 We consider the following use case:
 the lite client wants to verify a header for some given height *k*. Thus:
  - it requests the signed header for height *k* from a full node
  - it tries to verify this header with the methods described here.

 This can be used in several settings:
  - someone tells the lite client that application data that is relevant for it can be read in the block of height *k*.
  - the lite clients wants the latest state. It asks a full nude for the current height, and uses the response for *k*.
  - in case of inter-blockchain communication protocol (IBC) the light client runs on a chain and someone feeds it
  signed headers as input and it computes whether it can trust it.


 ## Details

 **Observation 1.** If *h.Header.bfttime + tp > now*, we trust the old
 validator set *h.Header.NextV*.

 When we say we trust *h.Header.NextV* we do *not* trust that each individual validator in *h.Header.NextV* 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).



 *Correctness arguments*

 Towards Lite Client Accuracy:
 - Assume by contradiction that `untrusted_h` was not generated correctly and the lite client sets trust to true because `CheckSupport` returns true.
 - trusted_h is trusted and sufficiently new
 - by Tendermint Fault Model, less than 1/3 of voting power held by faulty validators => at least one correct validator *v* has signed `untrusted_h`.
 - as *v* is correct up to now, it followed the Tendermint consensus protocol at least up to signing `untrusted_h` => `untrusted_h` was correctly generated, we arrive at the required contradiction.


 Towards Lite Client Completeness:
 - The check is successful if sufficiently many validators of `trusted_h` are still validators in `untrusted_h` and signed `untrusted_h`.
 - If *untrusted_h.Header.height = trusted_h.Header.height + 1*, and both headers were generated correctly, the test passes

 *Verification Condition:* We may need a Tendermint invariant stating that if *untrusted_h.Header.height = trusted_h.Header.height + 1* then *signers(untrusted_h.Commit) \subseteq trusted_h.Header.NextV*.

 *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 CheckSupport returns true for non-adjacent headers.




 *Correctness arguments (sketch)*

 Lite Client Accuracy:
 - Assume by contradiction that `untrusted_h` was not generated correctly and the lite client sets trust to true because CanTrustBisection returns nil.
 - CanTrustBisection returns true only if all calls to CheckSupport in the recursion return nil.
 - Thus we have a sequence of headers that all satisfied the CheckSupport
 - again a contradiction

 Lite Client Completeness:

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

 *Stalling*

 With CanTrustBisection, a faulty full node could stall a lite client by creating a long sequence of headers that are queried one-by-one by the lite client and look OK, before the lite 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 lite 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, Bisection would then be executed at the full node.
 * We may set a timeout how long bisection may take.




 # Non Recursive Verification - MOVED!

 Non Recursive verification has moved to [light](./light).
--- a/spec/consensus/readme.md
+++ b/spec/consensus/readme.md
@ -3,3 +3,27 @@ cards: true
 ---

 # Consensus

 Specification of the Tendermint consensus protocol. 

 ## Contents

 - [Consensus Paper](./consensus-paper) - Latex paper on
  [arxiv](https://arxiv.org/abs/1807.04938) describing the
  core Tendermint consensus state machine with proofs of safety and termination.
 - [BFT Time](./bft-time.md) - How the timestamp in a Tendermint
  block header is computed in a Byzantine Fault Tolerant manner
 - [Creating Proposal](./creating-proposal.md) - How a proposer
  creates a block proposal for consensus
 - [Light Client Protocol](./light) - A protocol for light weight consensus
  verification and syncing to the latest state
 - [Signing](./signing.md) - Rules for cryptographic signatures
  produced by validators.
 - [Write Ahead Log](./wal.md) - Write ahead log used by the
  consensus state machine to recover from crashes.

 The protocol used to gossip consensus messages between peers, which is critical
 for liveness, is described in the [reactors section](/spec/reactors/consensus).

 There is also a [stale markdown description](consensus.md) of the consensus state machine
 (TODO update this).