search

informalsystems / verification

Specifications of the protocols and the experiments on their verification
9 stars 2 forks source link

Specification of the light client #4

Closed konnov closed 4 years ago

konnov commented 4 years ago

The TLA+ specification of the light client, including bisection. TLC checked this one for the height 3.

cwgoes commented 4 years ago

Is it possible to alter permissions on this repository so that I can self-request a review?

At present, I don't seem to be able to do so.

Looking forward to the TLA+ spec!

konnov commented 4 years ago

Hi Christopher, I am not sure how to do it at github. You should be on the list of collaborators now.

konnov commented 4 years ago

A question for discussion: when the lite client starts, should it be the case that (now - inithead.time) <= trustingPeriod. The TLA+ spec is assuming that if this is not true, the lite client should not trust the initial header and the header to be verified.

milosevic commented 4 years ago

A question for discussion: when the lite client starts, should it be the case that (now - inithead.time) <= trustingPeriod. The TLA+ spec is assuming that if this is not true, the lite client should not trust the initial header and the header to be verified.

The invariant above should always hold (also upon initialisation). It is probably simpler expressing it as inithead.time + trustedPeriod < now. Intuition is that trusted period of the header hasn’t expired yet.

konnov commented 4 years ago

I have fixed the spec after the discussion at dev-session. Additionally, the properties Correctness and Precision are refined now. All expected properties hold true on the minimal model: 2 validators + 1 full node, blockchain of length 3. This is apparently as much as we can get from TLC in a non-cloud mode.

konnov commented 4 years ago

I am going to merge this PR as lite client v1, so we can start: (1) verification efforts with Apalache and cloud TLC, and (2) work on v2 that does not use recursive bisection.

konnov commented 4 years ago

Actually, TLC just reported on a bug for NoDupsInv. In the current spec, the lite client makes two requests per pivot, and the full node may respond with two different headers for the same height. I will fix the spec, so the lite client would request for a pivot only once. The recursive algorithm is complicated...

konnov commented 4 years ago

I hope that this is the last fix for this version. TLC has found a violation of StoredHeadersAreSoundOrNonTrusted, as we were checking the left header instead of the right one. (Another fix is about the refinement of the property).

+++ b/spec/light-client/Lightclient.tla
@@ -195,7 +195,7 @@ OneStepOfBisection(pStoredSignedHeaders) ==
         lhdr == CHOOSE shdr \in pStoredSignedHeaders: shdr.header.height = lh
         rhdr == CHOOSE shdr \in pStoredSignedHeaders: shdr.header.height = rh
     IN
-    IF Verify(lhdr.header.VP, lhdr) = FALSE
+    IF Verify(rhdr.header.VP, rhdr) = FALSE
     THEN [verdict |-> FALSE, newStack |-> <<(* empty *)>> ] \* TERMINATE immediately
     ELSE \* pass only the header lhdr.header and signed header rhdr
       IF CheckSupport(lh, rh, lhdr.header, rhdr)
@@ -349,7 +349,7 @@ StoredHeadersAreSoundOrNotTrusted ==
     outEvent.type = "finished" /\ outEvent.verdict = TRUE
         =>
         \A left, right \in storedSignedHeaders: \* for every pair of different stored headers
-            \/ left = right
+            \/ left.header.height >= right.header.height
                \* either there is a header between them
             \/ \E middle \in storedSignedHeaders:
                 /\ left.header.height < middle.header.height
konnov commented 4 years ago

Termination, PrecisionInv, Correctness, NoDupsInv, StoredHeadersAreSoundOrNonTrusted holds true for the case of two nodes. Now we can continue with more elaborate verification.