TLA+: Updating the fastsync spec after model checking

[konnov]

This is a new version that:

• introduces a more refined block model that allows us to check the protocol invariants such as CorrectBlocksInv
• fixes the block execution logic, so the faulty nodes cannot inject corrupted blocks
• goes through the apalache model checker.

[josef-widder]

Should we add tags?

[liamsi]

This is a new version

This indicates there is a older version that this PR is updating? The diff is indicating that this is mostly new code (added files only with a tiny exception). I'll add @brapse as a reviewer as he is likely the most familiar with fast-sync here.

I'm happy to review this as well but I think I need someone to walk me through this. It's a really large change and I'm neither deeply familiar with tla nor with fast-sync.

[konnov]

Right. There are plenty of files. The changes to the protocol spec can be found in fastsync.tla, whereas the other files are harness for model checking. There a few interesting changes in the protocol that are related to hashes and using a reference chain, which is modeled in Tinychain.tla.

[josef-widder]

Great specification and model checking results! I think it would be good to write a small markdown file that explains the hash abstraction. I looked at the spec some weeks ago and understood it back then, and now struggled to get it back into my brain. I would be happy work contribute to that.

[josef-widder]

looks great!

[josef-widder]

Thanks for addressing my comments. Looks great!