High level fast sync spec

informalsystems / verification

Specifications of the protocols and the experiments on their verification

9 stars 2 forks source link

Closed milosevic closed 4 years ago

konnov commented 4 years ago

I have found several typos by asking TLC to check for deadlocks. Going to commit soon.

konnov commented 4 years ago

I have fixed TypeOK, so TLC goes through on MAX_HEIGHT = 2, one correct peer, and one faulty peer. Please check, whether it makes sense now.

konnov commented 4 years ago

Also, as discussed with @milosevic, GrowBlockchain is now advancing one peer, not all peers.