Merge `enhancement/complete-chain-sync-program-based` of pull request #93 into `master`
Complete the specification of the chain synchronization protocol
Complete the specification of the chain synchronization protocol
The initial chain is known and therefore doesn’t need to be communicated. Also, it is likely that right after the initial intersection finding the chain has to be partially revised, making it even less useful to send the initial chain.
`smt` doesn’t work in automated builds on GitHub.
Using the term “updates” may suggest that what the server receives are merely diffs instead of whole chains. The new identifier makes it clearer that from this channel the server gets chains.
For the `Idle` phase, there is not just one state that the server can be in; so the above name is misleading. This function is about the state that the server is in at the beginning of a cycle. We call this now the base state and have chosen the new identifier accordingly.
This commit additionally includes the following changes: * Cause rollback after `IntersectFound` to happen also when the server chain hasn’t changed * Streamline the conformance proof * Turn the names of the universally quantified variables in the conformance proof into single-letter variants * Make the subproof of `program Server` conformance more robust by removing the dependency on subgoals left over by an automated prover