Formally specify correctness property of the chain sync mini-protocol with fixed chain

[javierdiaz72]

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

[jeltsch]

I think that it we should use either program families and process families or programs and processes. I guess that the latter is enough. To go to process families we could start with program families and apply ⟦_⟧ pointwise.

[javierdiaz72]

I think that it we should use either program families and process families or programs and processes. I guess that the latter is enough.

My current code attempt (which follows your former approach) is the following:

consts protocol_semantics :: "('p ⇒ 'm or_done program) ⇒ process family" (‹⟦_⟧›)

consts sync_repeated_send :: "'a sync_channel ⇒ 'a ⇒ process family" (infix ‹◃⇧∞⇘s⇙› 52)

definition list_sender :: "'a::embeddable sync_channel ⇒ 'a list ⇒ process family" where
  [simp]: "list_sender c xs = foldr (λx p. c ◃⇘s⇙ x; p) xs 𝟬"

context chain_sync
begin

definition spec :: "'i list ⇒ process family" where
  [simp]: "spec C = list_sender client_chains [C'. C' ← prefixes C, C' ≠ []]"

 definition impl :: "'i list ⇒ process family" where
  [simp]: "impl C = ⟦program⟧ ∥ server_chains ◃⇧∞⇘s⇙ C"

theorem fixed_chain_sync_from_genesis_conformance:
  assumes "initial_client_chain = [hd C]"
  shows "spec C ≈⇩s impl C"
  sorry

end

To go to process families we could start with program families and apply ⟦_⟧ pointwise.

Do you suggest to do something like ⟦program Client⟧ ∥ ⟦program Server⟧? If so, how could I turn this compound process into a process family?