-
Notifications
You must be signed in to change notification settings - Fork 224
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Light Client TLA+ Specification #314
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Some initial comments on the Lightclient_A_1.tla model. I still have to look at the properties, load the mdel and try it. And also at the blockchain one.
|
||
TODO: add a traceability tag as soon as the English spec has one | ||
*) | ||
ValidAndVerifiedPre(trusted, untrusted) == |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have some doubts about the name here and I know this is part of preconditions in the english spec. But imho this is not really a precondition. It should reflect what it does: given two headers, it checks that they are both within trusting period, > 2/3rds have signed the untrusted, etc. So it performs basic validation. I also don't see where the > 2/3rds check is done for the skipping case.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The naming is ok. It is just the precondition for ValidAndVerified
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Regarding, 2/3rds, good catch. We promoted the check to the general case, not only the non-skipping case.
* Check that the commits in an untrusted block form 1/3 of the next validators | ||
* in a trusted header. | ||
*) | ||
OneThird(trusted, untrusted) == |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe the name should reflect the meaning of the >1/3rd, i.e. the untrusted validator set should be trusted.
OneThird(trusted, untrusted) == | |
TrustedValidatorSet(trusted, untrusted) == |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Renamed it to SignedByOneThirdOfTrusted
ValidAndVerified(trusted, untrusted) == | ||
IF ~ValidAndVerifiedPre(trusted, untrusted) | ||
THEN "FAILED_VERIFICATION" | ||
ELSE IF ~BC!InTrustingPeriod(untrusted.header) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can we reach this? We are here with ValidAndVerifiedPre(trusted, untrusted)
being TRUE
that checked:
BC!InTrustingPeriod(trusted.header)
trusted.header.time <= untrusted.header.time
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You are totally right! This is a good lemma :-)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We have added a comment like this:
(* We leave the following test for the documentation purposes.
The implementation should do this test, as signature verification may be slow.
In the TLA+ specification, ValidAndVerified happens in no time. *)
/\ fetchedLightBlocks = [h \in {TRUSTED_HEIGHT} |-> trustedLightBlock] | ||
\* initially, lightBlockStatus is a function of one element, i.e., TRUSTED_HEIGHT | ||
/\ lightBlockStatus = [h \in {TRUSTED_HEIGHT} |-> "StateVerified"] | ||
\* the latest verified block the the trusted block | ||
/\ latestVerified = trustedLightBlock |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could all this be grouped in a single store
record so it better reflects the code and english spec? Here is not too bad but it becomes harder to follow in the rest of the spec
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would prefer to keep the specification to the minimum. A record would introduce unnecessary detail here. One can also argue that LCInit
encodes a method of the corresponding block store, so the variables are implicitly referenced with this
;-)
LightStoreGetInto(block, height) == | ||
block = fetchedLightBlocks[height] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I am curious why not return the block here.
LightStoreGetInto(block, height) == | |
block = fetchedLightBlocks[height] | |
LightStoreBlock(height) == | |
fetchedLightBlocks[height] |
Same question for most of the other defs.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good question. It looks like an artifact of an older spec. We just inlined it.
\* Check, whether newHeight is a possible next height for the light client. | ||
\* | ||
\* TODO: add a traceability tag when Josef adds it in the English spec | ||
ScheduleTo(newHeight, pNextHeight, pTargetHeight, pLatestVerified) == |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a predicate. Also I find it easier to read if the parameters reflect the height order
ScheduleTo(newHeight, pNextHeight, pTargetHeight, pLatestVerified) == | |
CanScheduleTo(newHeight, pLatestVerified, pNextHeight, pTargetHeight) == |
This is incredibly hard to read, and I know in the english spec it is kept vague. I understand that we want to allow some flexibility on how we pick headers during bisection but in this model we can just take the half. Since the strategy doesn't affect correctness this should be fine. I also don't understand why it is called schedule
. We do not schedule anything. Same in english spec. It is just a simple operation of selecting a new height.
In case we keep it this way, it might be easier if the caller decides whether to pick a header:
- either between
pLatestVerified
andpNextHeight
or - between
pNextHeight
andpTargetHeight
...and have something like:
ScheduleTo(newHeight, pNextHeight, pTargetHeight, pLatestVerified) == | |
CanSchedule(newHeight, low, high) == |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Regarding the name, "schedule" comes from the Rust implementation, so we better keep it like that. Let's rename it to CanScheduleTo
though.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For the responsibilities of the caller, it is better to keep the verified and block scheduler as independent from each other, as possible. Splitting the decision into two parts on two sides complicates the interface. The current version might be hard to read, but that is because it captures all possible block schedulers we may implement in the future. A concrete implementation of the scheduler should be more intuitive.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We have changed the parameter order. Your version makes more sense.
\* the loop condition is true | ||
/\ latestVerified.header.height < TARGET_HEIGHT | ||
\* pick a light block, which will be constrained later | ||
/\ \E current \in BC!LightBlocks: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a bit confusing. We pick any block from the blockchain only to immediately overwrite it with the block with nextHeight
either from the light store or from chain. Can we remove this line altogether?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We pick any block from the blockchain only to immediately overwrite
Here is the place where TLA+ differs from a programming language. In a model checker like TLC, all blocks will be enumerated and then the blocks that do not match the constraint will be rejected. (No overwriting happens.) In Apalache, this will be just a constraint, the solver has to come up with a value of current
that matches the constraint.
What we do here is a common idiom in verification: Non-deterministically guess a value and then constrain it with your assumptions. Essentially, all symbolic tools use this idiom, one way or another.
/\ IF nextHeight \in DOMAIN fetchedLightBlocks | ||
THEN /\ LightStoreGetInto(current, nextHeight) | ||
/\ UNCHANGED fetchedLightBlocks | ||
ELSE /\ FetchLightBlockInto(current, nextHeight) | ||
/\ fetchedLightBlocks' = LightStoreUpdateBlocks(fetchedLightBlocks, current) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Would it be possible to make this into something like:
/\ IF nextHeight \in DOMAIN fetchedLightBlocks | |
THEN /\ LightStoreGetInto(current, nextHeight) | |
/\ UNCHANGED fetchedLightBlocks | |
ELSE /\ FetchLightBlockInto(current, nextHeight) | |
/\ fetchedLightBlocks' = LightStoreUpdateBlocks(fetchedLightBlocks, current) | |
/\ IF GetFromStore(current, store, nextHeight) THEN | |
newStore = store | |
ELSE | |
/\ FetchLightBlockInto(current, nextHeight) | |
/\ newStore = UpdateStore(store, current) |
...so it's easier to follow with the spec and code.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This will be hard to do without introducing side effects. In your suggestion, current
and store
are updated simultaneously. In the proposed code, we would compute new store
and constrain current
. These are two different things that should not happen in the same place, for clarity of the spec.
It would be really cool to discuss this question and the above question in a dev session. This is really something, where the programming ends and logic starts :-)
THEN "working" | ||
ELSE "finishedSuccess" | ||
/\ \E newHeight \in HEIGHTS: | ||
/\ ScheduleTo(newHeight, nextHeight, TARGET_HEIGHT, current) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is nicer than english spec as we know where we are. So we could say: pick a height in (nextHeight, TARGET_HEIGHT]
/\ ScheduleTo(newHeight, nextHeight, TARGET_HEIGHT, current) | |
/\ ScheduleTo(newHeight, nextHeight, TARGET_HEIGHT) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Here you like a non-deterministic choice 👍
*) | ||
/\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateUnverified") | ||
/\ \E newHeight \in HEIGHTS: | ||
/\ ScheduleTo(newHeight, nextHeight, TARGET_HEIGHT, latestVerified) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
..and here: pick a height in (latestVerified, nextHeight-1]
/\ ScheduleTo(newHeight, nextHeight, TARGET_HEIGHT, latestVerified) | |
/\ ScheduleTo(newHeight, latestVerified, nextHeight-1) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Josef and I still think that we should not change the number of parameters and the parameters to CanScheduleTo
, as we may change the scheduling decision in the future.
@ancazamfir, thank you for the deep review! Josef and I went over your comments and implemented some of them (and commented on the ones we skipped). |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks great. We will add tags later. This shouldn't block merging.
A TLA+ spec for the light client verification, in accordance with the English spec.