Update specification of light client algorithm to align with the code #61

milosevic · 2019-11-15T11:24:11Z

Fix timing issues by introducing Delta parameter

- Fix timing issues by introducing Delta parameter

ancazamfir

Did a first pass. Added some comments. In general I think we could simplify more.

spec/consensus/light-client.md

ancazamfir

I added some comment mainly to help with readability. For the purpose of this document I think having (bool, err) as return in CheckSupport() makes the pseudocode harder to read.

spec/consensus/light-client.md

Co-Authored-By: Anca Zamfir <ancazamfir@users.noreply.github.com>

…ent_algo # Conflicts: # spec/consensus/light-client.md

ancazamfir

Lots of good changes! Left a few comments.

spec/consensus/light-client.md

ebuchman

A few concerns from reviewing the latest implementation update (informalsystems/tendermint-rs#100 (review))

ebuchman · 2019-12-20T18:12:27Z

spec/consensus/light-client.md

+    Store.Add(h2)
+    return nil
+  }
+  if err != ErrTooMuchChange return err


If we do this here, doesn't it mean we never start bisecting?

We are in line 359 with err != nil and, if err != ErrTooMuchChange, the only possible values for err (looking at CheckSupport()) are:

ErrHeaderNotWithinTrustedPeriod

ErrInvalidAdjacentHeaders

They are both indicators that current bisection has failed, further recursive calls should not be done and therefore the call stack will unwind propagating this error to the final caller (VerifyHeader()).

I mentioned this in an earlier comment, it is better to write 359 and others like:
if fatalCheckSupportError(err) return err
Also, potential future error types added to CheckSupport() would be easier to implement without changing all the callers.

Alternatively, we could use sth else than an error to indicate that there was too much change in the validator set (going from h1 to h2). Returning a bool for instance. Or simply renaming the method name to indicate the only relevant case directly: ValidatorsChangedTooMuch (or EnoughIntersection? I'm sure there are better names).

FWIW, linking the related discussion regarding the rust implementation: https://github.com/interchainio/tendermint-rs/pull/100/files#r360502272

ebuchman · 2019-12-20T18:14:06Z

spec/consensus/light-client.md


-_Verification Condition:_ We may need a Tendermint invariant stating that if _h2.Header.height = h1.Header.height + 1_ then _signers(h2.Commit) \subseteq h1.Header.NextV_.
+  h2 := Commit(height)
+  if !verify(h2) { return ErrInvalidHeader(h2) }


Shouldn't we have a flow where we CheckSupport before we verify ?

liamsi · 2019-12-24T12:43:13Z

spec/consensus/light-client.md

-  if CheckSupport(h1,h2,trustlevel) {
-    return true
+  if isWithinTrustedPeriod(h2) {
+    Store.add(h2)


Isn't this redundant? CanTrust already has stored h2 here. At least in the bisection case because:

func CanTrustBisection(h1,h2,trustThreshold) error { assume h1.Header.Height < h2.header.Height err = CheckSupport(h1,h2,trustThreshold) if err == nil { Store.Add(h2) return nil } if err != ErrTooMuchChange return err pivot := (h1.Header.height + h2.Header.height) / 2 hp := Commit(pivot) if !verify(hp) return ErrInvalidHeader(hp) err = CanTrustBisection(h1,hp,trustThreshold) if err == nil { Store.Add(hp) err2 = CanTrustBisection(hp,h2,trustThreshold) if err2 == nil { Store.Add(h2) return nil } return err2 } return err }

Bisection needs to store headers in between (the pivot headers). But maybe we leave it to the caller to actually deal with the last header h2?

I think the name of this method (CanTrust / CanTrustBisection) should actually indicate that it is updating the store and not just answering the question "Can we trust this header based on h1".

liamsi · 2019-12-24T12:52:00Z

spec/consensus/light-client.md

-func Bisection(h1,h2,trustlevel) bool{
-  if CheckSupport(h1,h2,trustlevel) {
-    return true
+  if isWithinTrustedPeriod(h2) {


Why do we do this twice? When we fetch the commit / signed header above and then again here? Shouldn't we assume that we are still within the trusted period here?

h2 := Commit(height) if !verify(h2) { return ErrInvalidHeader(h2) } if !isWithinTrustedPeriod(h2) { return ErrHeaderNotWithinTrustedPeriod(h2) } // ... if isWithinTrustedPeriod(h2) { /*...*/ }

If isWithinTrustedPeriod was false, we would have already returned with an error.

I think it's because of #57 but I agree it doesn't really make sense, especially if time is going to be passed in

liamsi · 2019-12-28T18:40:32Z

spec/consensus/light-client.md

+  err = CanTrust(trusted_h, untrusted_h, trustThreshold)  // or CanTrustBisection((trusted_h, untrusted_h, trustThreshold)
+  if err != nil { return err }
+
+  if isWithinTrustedPeriod(untrusted_h) {


If this re-checking is necessary, I think it needs an explanation (see #61 (comment)).

liamsi · 2019-12-28T18:45:39Z

spec/consensus/light-client.md

+  if err != nil { return err }
+
+  if isWithinTrustedPeriod(untrusted_h) {
+    Store.add(untrusted_h)


This seems redundant, at least in the CanTrustBisection case untrusted_h was already stored.

ebuchman · 2019-12-29T02:41:29Z

I think I may have a simpler structure - please see informalsystems/tendermint-rs#114

ebuchman

Nice work

spec/consensus/light-client.md

ebuchman · 2020-01-07T17:03:30Z

spec/consensus/light-client.md

+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 process p and every header (correctly generated by the Tendermint consensus)
+time (BFT time) the following inequality holds: `Header.Time < now + CLOCK_DRIFT`.


Do we want to include the lower bound here? Or at least mention why we don't care about it ? It might also be helpful to clarify that we mostly need this to hold for the light client's local clock, not just the validators ...

I am not sure what would be the lower bound? Not sure if we can say anything more precise than genesis time, but not sure how this is useful. My understanding is that upper bound ensures that we don't consider headers that are outside the assumption that lite client clock is in sync with blockchain time; as time progresses, not sure what we can say about the past.

Ah, but it's currently written from the perspective of validators. For the validators, we want a lower bound (I think?). For the light client, we only need the upper bound.

It is not clear to me when this inequality should hold. I guess when the header is generated? Also, there are two moving parts in the definition, i.e., "Header.Time" and "now", so it is not clear who to blame when the inequality is violated. I guess our assumption is that "Header.Time" is always correct (by definition; it serves as a time reference for the system), and that violation of the inequality means that the Lite Client is faulty. IOW it is in the responsibility of the lite client to keep its clock synchronized.

The inequality holds from the moment header is generated. I was assuming that header is always correct, i.e., that header is coming from the main chain that is not forked. We need to make this assumption more clear. As we also assume that lite client processes are synchronised with respect to BFT time, header that does not satisfy this inequality must come from a faulty full node. We can think about trying to weaken this assumption to eventually hold. I think that it would be useful trying to more precisely understand attack vectors in case local lite client clock drifts more than clockDrift. Ideally, safety should not be violated in case this assumption does not hold, but only termination should temporary be violated.

I agree. We rely on bfttime for the failure model and the checks heavily. So if the lite clients clock is off too far, everything might be lost. The question is, whether within the Bisection we should/can check whether the lite client's clock is synchronized (and what timing assumptions this would impose), or whether safety has to rely on the synchronization of the lite client's clock.

ebuchman · 2020-01-07T17:25:50Z

spec/consensus/light-client.md

-The function _Bisection_ checks whether to trust header _h2_ based on the trusted header _h1_. It does so by calling
-the function _CheckSupport_ in the process of
-bisection/recursion. _CheckSupport_ implements the trusted period method and, for two adjacent headers (in term of heights), it checks uninterrupted sequence of proof.
+    now = System.Time()


Do we really want the function to have access to the system clock ?

The idea of this function is to illustrate how to correctly use VerifyBisection function. In case we don't check if we are still within trusted period of initial trusted state after VerifyBisection is executed, we can't give precise guarantees to the user. I don't know how to avoid this. As most of complexity is happening within VerifyBisection this shouldn't be a big problem from the testing perspective.

spec/consensus/light-client.md

ebuchman

Can we merge this and iterate from there? We can also merge #73 into this or into master after

liamsi

I agree, we should merge this!

Move light specs to their own dir, add readme and diagram

milosevic force-pushed the zm_lite_client_algo branch 6 times, most recently from bb6b481 to 3fbdc58 Compare November 15, 2019 11:45

Add non-recursive specification of Bisection algorithm

a4b68ec

- Fix timing issues by introducing Delta parameter

milosevic force-pushed the zm_lite_client_algo branch from 3fbdc58 to a4b68ec Compare November 15, 2019 11:47

milosevic requested review from ancazamfir, ebuchman and melekes November 15, 2019 11:48

ancazamfir reviewed Nov 19, 2019

View reviewed changes

spec/consensus/light-client.md Outdated Show resolved Hide resolved

ancazamfir reviewed Nov 19, 2019

View reviewed changes

spec/consensus/light-client.md Outdated Show resolved Hide resolved

melekes reviewed Nov 21, 2019

View reviewed changes

Clean up error conditions and simplify pseudocode

4ee393c

ancazamfir reviewed Dec 2, 2019

View reviewed changes

melekes reviewed Dec 2, 2019

View reviewed changes

spec/consensus/light-client.md Outdated Show resolved Hide resolved

spec/consensus/light-client.md Outdated Show resolved Hide resolved

spec/consensus/light-client.md Outdated Show resolved Hide resolved

spec/consensus/light-client.md Outdated Show resolved Hide resolved

Apply suggestions from code review

2306108

Co-Authored-By: Anca Zamfir <ancazamfir@users.noreply.github.com>

milosevic force-pushed the zm_lite_client_algo branch from e17582c to 2306108 Compare December 2, 2019 11:40

Anca Zamfir and others added 3 commits December 6, 2019 12:43

some suggestions for pseuodocode changes

afda2d3

Improved error handling

5c58084

Improve algorithms

069906a

milosevic force-pushed the zm_lite_client_algo branch from 4d60a43 to 069906a Compare December 11, 2019 14:21

milosevic added 2 commits December 11, 2019 16:13

Add explanation on difference between trusted models

9ddfc79

Merge remote-tracking branch 'remotes/origin/master' into zm_lite_cli…

8528cdb

…ent_algo # Conflicts: # spec/consensus/light-client.md

ancazamfir reviewed Dec 11, 2019

View reviewed changes

liamsi reviewed Dec 12, 2019

View reviewed changes

spec/consensus/light-client.md Outdated Show resolved Hide resolved

milosevic force-pushed the zm_lite_client_algo branch from 60303ef to 74d6c04 Compare December 12, 2019 11:32

Address reviewer's comments

4f7c555

liamsi reviewed Dec 20, 2019

View reviewed changes

spec/consensus/light-client.md Outdated Show resolved Hide resolved

ebuchman reviewed Dec 20, 2019

View reviewed changes

liamsi reviewed Dec 24, 2019

View reviewed changes

milosevic added 2 commits December 25, 2019 13:58

Addressing reviewer's comments

ee0cc53

Separating algorithm from proofs

0adde9d

liamsi reviewed Dec 28, 2019

View reviewed changes

ebuchman mentioned this pull request Dec 29, 2019

Light Client Spec related follow up informalsystems/tendermint-rs#111

Closed

7 tasks

milosevic added 2 commits December 31, 2019 13:31

Intermediate commit (aligning spec with the code)

4a9eb1f

Removing Store from API and providing end-to-end timing guarantees

7130c2e

ebuchman reviewed Jan 7, 2020

View reviewed changes

Address reviewer comment's. Intermediate commit

146e251

melekes mentioned this pull request Jan 21, 2020

lite2: align with the newer version of the spec tendermint/tendermint#4329

Closed

ebuchman added 5 commits January 22, 2020 12:55

light client dir and readmes

f26eb4e

titles

eb9e1f9

add redirects

e342c21

add diagram

0358389

detection TODO

d1bd98d

ebuchman approved these changes Jan 22, 2020

View reviewed changes

ebuchman added 2 commits January 22, 2020 13:49

fix image

bd2f41b

update readme

c35d6e7

liamsi approved these changes Jan 22, 2020

View reviewed changes

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

dc54206

Move light specs to their own dir, add readme and diagram

milosevic changed the title ~~Add non-recursive specification of Bisection algorithm~~ Update specification of light client algorithm to align with the code Jan 23, 2020

Aligh the correctness arguments with the pseudocode changes

026fdde

milosevic force-pushed the zm_lite_client_algo branch from 22af52f to 026fdde Compare January 23, 2020 13:49

milosevic merged commit 033a0cb into master Jan 23, 2020

melekes deleted the zm_lite_client_algo branch February 17, 2020 10:17

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Update specification of light client algorithm to align with the code #61

Update specification of light client algorithm to align with the code #61

milosevic commented Nov 15, 2019

ancazamfir left a comment

ancazamfir left a comment

ancazamfir left a comment

ebuchman left a comment

ebuchman Dec 20, 2019

ancazamfir Dec 21, 2019

liamsi Dec 22, 2019 •

edited

Loading

ebuchman Dec 20, 2019

liamsi Dec 24, 2019

liamsi Dec 24, 2019

liamsi Dec 24, 2019 •

edited

Loading

ebuchman Dec 25, 2019

liamsi Dec 28, 2019

liamsi Dec 28, 2019

ebuchman commented Dec 29, 2019

ebuchman left a comment

ebuchman Jan 7, 2020

milosevic Jan 8, 2020

ebuchman Jan 8, 2020

josef-widder Jan 9, 2020

milosevic Jan 9, 2020 •

edited

Loading

josef-widder Jan 9, 2020

ebuchman Jan 7, 2020

milosevic Jan 8, 2020

ebuchman left a comment

liamsi left a comment

Update specification of light client algorithm to align with the code #61

Update specification of light client algorithm to align with the code #61

Conversation

milosevic commented Nov 15, 2019

ancazamfir left a comment

Choose a reason for hiding this comment

ancazamfir left a comment

Choose a reason for hiding this comment

ancazamfir left a comment

Choose a reason for hiding this comment

ebuchman left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

liamsi Dec 22, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

liamsi Dec 24, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ebuchman commented Dec 29, 2019

ebuchman left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

milosevic Jan 9, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ebuchman left a comment

Choose a reason for hiding this comment

liamsi left a comment

Choose a reason for hiding this comment

liamsi Dec 22, 2019 •

edited

Loading

liamsi Dec 24, 2019 •

edited

Loading

milosevic Jan 9, 2020 •

edited

Loading