Lightstore Invariants + Maintain Verification Information

[josef-widder]

In order to generate "proof of fork" (#461 , tendermint/tendermint#5149), it would be good to efficiently compute a sequence of lightblocks b(1), b(2), ... b(n), so that b(i+1) can be verified with b(i) in one step. If the light client does forward verification only, this property is maintained by the algorithm (I think @konnov checked that property already). However, if the light client has to fetch lightblocks whose height is less than latestTrusted (see LCV-FUNC-IBCMAIN.1), this property might not be maintained.

For instance, if b(1).NextValidators = b(2).Validators, but for a later added lightblock in-between, b(1.5).NextValidators and b(1.5).Validators may be piecewise disjunct from both.

To compute the proof of fork, I don't think we should re-verify the blocks to generate a sequence; this is expensive. I wonder whether we should maintain in the light store, for each lightblock which lightblock was used to originally verify it. We would need to add recording this information within VerifyToTarget.

Alternatively, we just keep these additional blocks in the proof of fork, but then the complexity of the "proof of fork verification" at the nodes who receive it increases.

[OStevan]

@josef-widder As a note to this issue at least in the forward verification case:

1. if the property is that there is a sequence of light blocks with increasing heights in the light store which maintains this property than it is ok
2. but if the property is that all stored light blocks represent such a sequence than this property is not currently maintained in TLA nor Rust (explanation below)

In the case of TLA, this is explicitly mentioned in StoredHeadersAreVerifiedOrNotTrustedInv. And in rust it is a bit more involved, if we look at the Scheduler, specifically the bisecting scheduler and the invariants, it can ignore Unverified light blocks in the store and as such might, miss previously fetched light blocks leaving them in Unverified state.

As a result in both cases, the light store will have a mix of Verified and Unverified light blocks after finishing verification. It is easy to extract just the sequence of Verified blocks, but it is not true that all stored light blocks form this sequence.

[josef-widder]

You are right. In my discussion I was not precise. In my text I ignore unverified lightblocks.

More generally, unverified lightblocks are something that is relevant for verification, but I guess we should not expose them to an outside observer.

[milosevic]

Would be good to explain a bit better the context. I understand that maintaining this property of the light store might be useful, but explaining better the requirement (use case) would be helpful.

[josef-widder]

The main use case is to generate proof of fork.

• Assume in the LightStore you have b1, b10, b50, b100
• You get a block b100' that conflicts b100 and can be verified from b1

The question is what should be the proof of fork.

• The easiest PoF to generate, would be to include all blocks b1, b10, b50, b100.
  • But there is the case where b50 was installed by skipping in one step based on b1, and
  • b10 was installed later, and b10 cannot be used to verify b50 because changes in validator sets
  • in this case, the complexity is on the receiver side of the PoF: The receiver has to check that b50 is indeed OK, based on b1 (the receiver should not dismiss the PoF because it cannot verify b50 based on b10). It might be that you have to check each block against all earlier blocks
• So, it would relieve the receiver of the PoF (and would make the proof smaller) if the lightclient would just include b1, b50, b100. To compute this,
  • the lightclient either has to re-verify; that is, figure out to dismiss b10
  • or remember how (based on what block) a block was installed and use this information. If b100 points to b50, and b50 points to b1, this information could be used to generate PoF efficiently

[josef-widder]

After some more thinking, the most efficient thing would be to store for each verified lightblock b2 the height of the lightblock b1 that was used to one-step verify b2, that is, where ValidAndVerified(b1, b2) returned successfully. This information just has to be recorded during VerifyToTarget. I suggest to adapt the specification and implementation accordingly.

[xla]

After some more thinking, the most efficient thing would be to store for each verified lightblock b2 the height of the lightblock b1 that was used to one-step verify b2, that is, where ValidAndVerified(b1, b2) returned successfully. This information just has to be recorded during VerifyToTarget. I suggest to adapt the specification and implementation accordingly.

At a glance this looks like a great trade-off between preserving the context and keeping the data lean.

[josef-widder]

OK, then let's add this verification information in the next revision of the spec. In #479 in verification.md I have added a section "Status" that explains that this change need to come and I have pointed to this issue.

[josef-widder]

spec-wise the required logic is on master. #415 will need to make the link to implementation. For the relayer we may also need to compute evidence, but the spec work for storing the required information is there.