Skip to content

Commit

Permalink
Renamed [LCV-DIST-LIFE.1] -> [LCV-DIST-LIVE.1] (#307)
Browse files Browse the repository at this point in the history
  • Loading branch information
konnov committed Jun 9, 2020
1 parent 393a2ef commit bcef28b
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions docs/spec/lightclient/verification.md
Original file line number Diff line number Diff line change
Expand Up @@ -270,7 +270,7 @@ never be stored.

## Sequential Problem statement

#### **[LCV-SEQ-LIFE.1]**:
#### **[LCV-SEQ-LIVE.1]**:
The *Verifier* gets as input a height *targetHeight*, and eventually stores the
header of height *targetHeight* of the blockchain.

Expand Down Expand Up @@ -361,7 +361,7 @@ generated by the Tendermint consensus. We say *trustedHeader* is verified.
It is always the case that every verified header in *LightStore* was
generated by an instance of Tendermint consensus.

#### **[LCV-DIST-LIFE.1]**:
#### **[LCV-DIST-LIVE.1]**:
From time to time, a new instance of *Core Verification* is called with a
height *targetHeight*. Each instance must eventually terminate.
- If
Expand All @@ -377,7 +377,7 @@ height *targetHeight*. Each instance must eventually terminate.
> [**[LCV-DIST-SAFE.1]**](#lcv-vc-inv) must hold.
> The invariant [**[LCV-DIST-SAFE.1]**](#lcv-dist-safe) and the liveness
> requirement [**[LCV-DIST-LIFE.1]**](#lcv-dist-life)
> requirement [**[LCV-DIST-LIVE.1]**](#lcv-dist-life)
> allow that verified headers are added to *LightStore* whose
> height was not passed
> to the verifier (e.g., intermediate headers used in bisection; see below).
Expand Down Expand Up @@ -738,7 +738,7 @@ have the state *StateVerified*.
set to *StateVerified*.


#### Argument for [**[LCV-DIST-LIFE.1]**](#lcv-dist-life):
#### Argument for [**[LCV-DIST-LIVE.1]**](#lcv-dist-life):

- If *primary* is correct,
- `FetchLightBlock` will always return a light block consistent
Expand Down

0 comments on commit bcef28b

Please sign in to comment.