Modularize the chain synchronization client program

[javierdiaz72]

The implementation of a chain synchronization fragment that resulted from resolving #65 contains a client program that is rather monolithic in that it uses a single, top-level recursion. As a result, the structure of the client program doesn’t reflect the fact that the client sequentially goes through two phases: intersection finding and chain update. Currently, the client program maintains an argument that states in what phase the client currently is, but we shall modularize the client program such that its structure reflects the two-phase process it performs.

Concretely, the idea is to compose the client program from two corecursively defined programs. One program constitutes the complete client program; it uses corecursion for going through the rounds for finding an intersection point and then invokes (essentially via a tail call) the other program, which uses corecursion for repeatedly updating the chain.

For proving conformance, we shall show conformance of the second program to the state machine and afterwards show conformance of the first program to the state machine, using the conformance result for the second program for handling the invocation of this program (perhaps this can even work with the present state_machine_bisimulation method by passing this conformance result as a chained fact). It seems that we could even have a state machine that uses different “idle” states for the first and the second phase; in this case, we would just need to prove conformance of the second program to the state machine with the initial state changed to the “idle” state that the protocol should be in at the start of the second phase.