search

informalsystems / verification

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

spec for fast sync scheduler #5

Closed ancazamfir closed 4 years ago

ancazamfir commented 4 years ago

Review for the TLA+ specification for the scheduler handler in fastsync version 2. (just status request/ response and no-advance timer event for now)

ancazamfir commented 4 years ago

Thanks for the review! Temporal properties here are not perfect and still work in progress. As I mentioned before I find this the hardest part of a TLA spec. I played with a few variants to see the results and left the code in a bit of limbo. Will work more on these.

ancazamfir commented 4 years ago

I like the both specs. 👍👍👍

At the meta-level, both fastsync and the the low-level light client spec pay a lot of attention to the error codes. While it is indeed important to the implementation, this error processing obfuscates the main logic of the protocol. It would be really great to decouple the error-checking spec from the happy-logic spec. In the case of fastsync, we could decompose all handleXYZ operators into two versions: handleXYZwhenError and handleXYZwhenNoError. This would help us to see the core logic without focusing on errors too much and, at the same time, see more clearly, how the errors propagate through the protocol actions.

I will look into that