spec: Rust like pseudo code for Sequential supervisor and core verification #509

OStevan · 2020-08-07T10:05:33Z

As @josef-widder mentioned here is the pseudo code proposal for specification and code changes. I was not sure how to name this and where to put it so we can change it as others see fit.

Goals?

The proposed pseudo code should solve the main issues of LightStore having an unbounded interface which makes code of skipping forward verification more complicated than needed. If implemented it should solve several issues which came out of it.

Possible issues?

with this proposal the LightStore requires that when inserting new information it is always possible to build a verification chain with what is already in it
the requirement above makes backward verification using just hashes impossible as the links with lower LightBlocks are impossible to recreate in this situation

Proposal details

current LightStore is now split:
1. what were once verified LightBlocks are now stored in Trace
2. Unverified LightBlocks are now on the FetchedStack
3. There are no longer Failed LightBlocks as there can be only one and that one is returned as an error reason in verify_to_target
4. The notion of Trusted is removed, and with the sequential supervisor everything in what is now LightStore is what were previously trusted.
History of how LightBlocks were verified can be retrieved from the LightStore
LightStore can recover from possible forks in the future by removing LightBlocks which are now considered to be from a fork.

Order in which to review for easier understanding

basically top to bottom
first part is related to skipping verification until the LightStore (excluding)
second part relevant for supervisor and possible ForkDetection and Relayer requirements

Issue which prompted this PR

spec: Detector refactor #494

Issues this approach should solve.

Lightstore Invariants + Maintain Verification Information #499 : chain invariant is easily retrievable, and chain computation is built-in the LightStore now
light-node: does not recover from primary restart #487 : previous losses of trusted LightBlock are no longer possible as we always ask for the highest from the supervisor LightStore
light-client: improve separation of concerns in get_or_fetch_block #434 : no longer relevant with refactors proposed here
light-client: improve LightStore API #428 : logic is very much split and the API is now easier to reason about
Ensure a trusted light block stays trusted permanently, even if its peer fails later #420 : same as for 487
Basic bisecting schedule logic can be simplified #333 : simplified by design

Should help with easier implementation of

light-client: Fork Detection Evidence Submission Review #415 : should be easier to collect evidence as verification trace is collected
Relayer requirements for the Light Client #497 : for all the mentioned height combinations it should be possible to easily get the light block for verification.

Issues which should be reworded depending on the changes here

Do we need current_height in the schedule function? #334 : everything stored in the LightStore is assumed to have passed verification at some point

Referenced an issue explaining the need for the change
Updated all relevant documentation in docs
Updated all code comments where relevant
Wrote tests
Updated CHANGELOG.md

OStevan · 2020-08-07T10:06:59Z

@milosevic @brapse @ebuchman @romac @xla

josef-widder · 2020-08-07T10:29:58Z

Thanks a lot! Both for the proposal of the code and the awesome overview of the issues!

I think we should discuss this here, and then incorporate either the proposed pseudo code (or a go variant of it) into a supervisor spec and the existing verification.md. (A go variant of a supervisor lives in detection.md #479, but the way the lightstore is treated and the parameters that are passes here in #509 seem much more to the point in the rust pseudo code in this PR).

xla

This is some great work. The amount of potential improvements it touches is amazing to see. Generally the direction is promising, some thoughts inline and here:

If we start to develop this notion of a linked list a.k.a. chain, we should look closer at how we make it correct to construct. As we want to point to the previous block we ought to encode that in the linked list semantics.
I'd be curious to see how much simpler the design can be if we assume that the LightStore is immutable. This would mean it needs reconstruction, which will make it very easy to reason in the case of fork recovery. Currently it's proposed that the LightStore itself offers a recovery functionality. There is strong evidence that we might be better served with treating it as immutable and rather lean heavier on type encoding to for example have a deterministic function a la: fn recover(tainted: LightStore::Tainted, boundary: Height) -> LightStore::Trusted
It's great that we trying to address the divergence we observed when querying the Supervisor - yet I think we would benefit from separating these concerns. On the surface it looks like we rework the LightStore entity to give us historical data and traceability, while when disseminating the latest/highest state it is a really the most trusted ChainPair and we don't depend on the history of how we got there. Clarifying which component depends on what information will bring more clarity.

docs/spec/supervisor/supervisor.md

xla · 2020-08-07T13:05:13Z

docs/spec/supervisor/supervisor.md

+```rust
+/// Stores the Light Blocks which could not be confirmed to have originated from
+/// the same chain as the predecesor light blocks.
+type FetchedStack = Stack<LightBlock>;


What are the semantics of the stack? I don't believe there is a type definition in this file.

There is no semantics as we could use a Vec for this, the goal was just to name it here and explain it is going to be used as a stack (push, pop, peek, is_empty) and not with random access.

docs/spec/supervisor/supervisor.md

xla · 2020-08-07T13:27:38Z

docs/spec/supervisor/supervisor.md

+
+/// Pair of light block and height of the light block which was highest 
+/// highest one for which we believe originated from the same chain
+type ChainPair = (LightBlock, Height);


The naming is confusing as it indicates that a Chain is paired with something. What I'm also wondering doesn't the LightBlock contain its Height, what's the benefit of pairing it with the Height.

Height in this case is the height of the block which was used to check the light. For example if we inserted a light block A into the Trace after passing all the checks in verify_to_target using light block B of height h. The ChainPair for A would be (A, h).

Is it always the height of B -1? In any case the term Height is so ubiquitous everywhere that we should encode what height we are referring to here, which in turn an help challenge how it can be constructed.

Still the term ChainPair for a pairing of block with height is miss-leading, imho.

Made a custom enum VerificationChain.

docs/spec/supervisor/supervisor.md

xla · 2020-08-07T13:33:06Z

docs/spec/supervisor/supervisor.md

+
+    // insert the light block of target height, simplifies the loop
+    // we can say that at each iteration there should be something on stack
+    fetch_stack.push(fetch_light_block(primary, target_height));


What does fetch_light_block do?

It's just copied from the current specifications. In current code it's from the Io component.

It would greatly benefit if this side-effect is not done in this function, it could be a parameter to be called with.

This was an error. The structure is changed a but now.

xla · 2020-08-07T13:37:21Z

docs/spec/supervisor/supervisor.md

+/// LightStore no longer has notions of Trusted, Verified, Unverified and Failed.
+/// The LightBlocks which are stored are all assumed to have originated from the
+/// same chain, irrespective of the peer from which we received it. The store
+/// provides the invariant that there is a 1-1 mapping from height to a LightBlock.


If we want to ensure the 1-1 invariant we should think in terms of a Set where we have a uniqueness constraint on the height, unless I miss-understand this part.

I think it would make more sense to have a Map<Height, LightBlock> where keys would be automatically unique.

For clarification, every height can only exist once? And there is only exactly one LightBlock per unique height?

Yes, that was the intention. At each point in time, there can be only one LightBlock which can be considered to be from the valid blockchain. Conflict on a single height would mean there is a fork.

docs/spec/supervisor/supervisor.md

Co-authored-by: Alexander Simmerl <[email protected]>

OStevan · 2020-08-07T14:49:31Z

@xla thanks for the comments. One thing which might not be clear just from the pseudo code and which I was not sure how to capture. This PR only addresses the case when we are doing forward verification without implying how the backward verification case will be done. For example lets say we start from height 1 and want to verify with height 10. One possible trace could be (1<- 5 <- 10) and after verifying 10 we get a request for height 8.

Now this case is not clear for me yet, so I didn't imply anything about the LightStore. For example one can imagine a case where for height 8 we just used the previously fetched light block of height 5. In this case the LightStore would basically be comprised of two chains: (this is currently what is expected)

1 <- 5 <- 10
     ^
      - - 8

It does not seem reasonable to just insert 8 between 5 and 10 (1 <- 5 <-8 <- 10) because in the case of validator set change such that skipping trust can not be established between 8 and 10 and somebody wants to replay the verification process just with the LightBlocks in the chain. They will not be able to replay the process.

To solve this we would need to also verify 10 starting from 8, however in this case the question is what do we do with the previous information that originally the LightBlock of height 10 was checked with 5, do we update it and make one chain 1 <- 5 <- 8 <- 10 or just try and verify as a sanity check.

melekes · 2020-09-15T05:31:32Z

docs/spec/supervisor/supervisor.md

+		// Verify
+        let mut result = Err(NoPeer);
+        // try with primaries until you succeed or there are no more peers
+        while result.is_err() {


looks like this will never terminate, making the rest of the code unreachable

melekes · 2020-09-15T05:33:24Z

docs/spec/supervisor/supervisor.md

+
+		// Verify
+        let mut result = Err(NoPeer);
+        // try with primaries until you succeed or there are no more peers


don't you have a single primary at any moment?

melekes · 2020-09-15T05:34:27Z

docs/spec/supervisor/supervisor.md

+    fn recover(&mut self, boundary: Height) -> Result<VerificationChain, LightStoreError>;
+
+    /// Returns the firsts LightBlock above if it exists.
+    fn above(&self, height: Height) -> Result<&LightBlock, ListStoreError>;


why do you need above and below when you already have get?

josef-widder · 2020-09-25T20:04:54Z

The ideas in the PR are great. I tried to incorporate them into tendermint/spec#159.
I propose that we conclude the discussions there and close this PR.

josef-widder · 2020-09-28T13:06:41Z

Thanks for the discussions. Let's continue that the other PR tendermint/spec#159.

OStevan added 3 commits August 7, 2020 11:12

Pseudo code for 0 shared state and easier fork detection info.

27b9b06

Fix naming.

4bee782

Expand interface.

0774f29

josef-widder changed the title ~~Rust like pseudo code for Sequential supervisor and core verification~~ Spec: Rust like pseudo code for Sequential supervisor and core verification Aug 7, 2020

josef-widder added enhancement New feature or request spec Specifications labels Aug 7, 2020

xla changed the title ~~Spec: Rust like pseudo code for Sequential supervisor and core verification~~ spec: Rust like pseudo code for Sequential supervisor and core verification Aug 7, 2020

xla assigned OStevan Aug 7, 2020

xla requested review from xla, josef-widder, liamsi, romac, ebuchman and milosevic August 7, 2020 11:03

xla suggested changes Aug 7, 2020

View reviewed changes

Apply suggestions from code review

ef5973b

Co-authored-by: Alexander Simmerl <[email protected]>

OStevan added 4 commits August 7, 2020 16:54

Additional changes based on xla comments.

6aab62d

Change to Vec.

1351513

Made custome type for chain.

5910719

Named a bi differently.

59ed691

This was referenced Sep 1, 2020

Light client evidence handling #544

Merged

spec: Light Client Supervisor #555

Closed

josef-widder mentioned this pull request Sep 9, 2020

Light client supervisor tendermint/spec#159

Closed

melekes reviewed Sep 15, 2020

View reviewed changes

josef-widder mentioned this pull request Sep 25, 2020

spec: update light client verification to match supervisor tendermint/spec#171

Merged

josef-widder closed this Sep 28, 2020

josef-widder mentioned this pull request Oct 20, 2020

Sequential Supervisor tendermint/spec#186

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

spec: Rust like pseudo code for Sequential supervisor and core verification #509

spec: Rust like pseudo code for Sequential supervisor and core verification #509

OStevan commented Aug 7, 2020 •

edited by josef-widder

Loading

OStevan commented Aug 7, 2020

josef-widder commented Aug 7, 2020

xla left a comment

xla Aug 7, 2020

OStevan Aug 7, 2020

xla Aug 7, 2020

OStevan Aug 7, 2020

xla Aug 7, 2020

xla Aug 7, 2020

OStevan Aug 31, 2020

xla Aug 7, 2020

OStevan Aug 7, 2020

xla Aug 11, 2020

OStevan Aug 31, 2020

xla Aug 7, 2020

OStevan Aug 7, 2020

xla Aug 7, 2020

OStevan Aug 31, 2020

OStevan commented Aug 7, 2020 •

edited

Loading

melekes Sep 15, 2020

melekes Sep 15, 2020

melekes Sep 15, 2020

josef-widder commented Sep 25, 2020

josef-widder commented Sep 28, 2020

spec: Rust like pseudo code for Sequential supervisor and core verification #509

spec: Rust like pseudo code for Sequential supervisor and core verification #509

Conversation

OStevan commented Aug 7, 2020 • edited by josef-widder Loading

OStevan commented Aug 7, 2020

josef-widder commented Aug 7, 2020

xla 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

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

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

Choose a reason for hiding this comment

OStevan commented Aug 7, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

josef-widder commented Sep 25, 2020

josef-widder commented Sep 28, 2020

OStevan commented Aug 7, 2020 •

edited by josef-widder

Loading

OStevan commented Aug 7, 2020 •

edited

Loading