Drop sending the initial chain

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.

src/Ouroboros-Mini_Protocols-Chain_Sync.thy

@@ -116,19 +116,19 @@ corec client_main_loop where
           client_main_loop \<psi> \<kappa> C u ChainUpdate
       ) |
     ChainUpdate \<Rightarrow>
-      u \<leftarrow> C;
+      let continue_with_new_chain = \<lambda>C'. u \<leftarrow> C'; client_main_loop \<psi> \<kappa> C' u \<phi> in
       \<up> Cont RequestNext;
       \<down> M. (partial_case M of
         Cont (RollForward i) \<Rightarrow>
-          client_main_loop \<psi> \<kappa> (C @ [i]) u \<phi> |
+          continue_with_new_chain (C @ [i]) |
         Cont (RollBackward q) \<Rightarrow>
-          client_main_loop \<psi> \<kappa> (roll_back \<psi> C q) u \<phi> |
+          continue_with_new_chain (roll_back \<psi> C q) |
         Cont AwaitReply \<Rightarrow>
           \<down> M. (partial_case M of
             Cont (RollForward i) \<Rightarrow>
-              client_main_loop \<psi> \<kappa> (C @ [i]) u \<phi> |
+              continue_with_new_chain (C @ [i]) |
             Cont (RollBackward q) \<Rightarrow>
-              client_main_loop \<psi> \<kappa> (roll_back \<psi> C q) u \<phi>
+              continue_with_new_chain (roll_back \<psi> C q)
           )
       )
   )"