We shall formally specify the equivalence between sending a whole chain and running the chain synchronization mini-protocol when the client starts from the genesis block and the server is given the aforementioned chain, which then is never updated during the protocol run.

Additionally, since the definition of the semantics of mini-protocol programs (see #96) will likely not be ready when this GitHub issue is addressed, we shall assume the existence of the following semantics function:

⟦_⟧ :: ('p ⇒ 'm or_done program) ⇒ process family