Create updated specification for coordinated head protocol

[ch1bo]

Why

While implementing, we have evolved the "Simplified Head protocol" from the version in the paper to an even more simplified form to something we would call the "Coordinated Head Protocol".

Hence, not all specified parts in the paper are relevant anymore. Also, the formalism used in the paper for the on-chain verification (OCV) part is actually mixing off- and on-chain syntax and is different to how Cardano smart contracts (Plutus scripts) work.

What

Goal is to create an updated specification serving as a foundation to discuss & audit the protocol itself, and to validate it from a theoretical standpoint (eg. does it provide the same security as the paper's protocol) and a practical standpoint (verifies the implementation is secure).

How

• Create a versioned specification document containing

  • overview & introduction to the protocol
  • protocol logic describing the states, transitions and any variables; e.g. what, when, how
    • this can be generic or specific to eUTxO
  • on-chain logic verifying each transition
    • this needs to be specific to eUTxO
  • specification of the primitive functions involved (e.g. the multi-signature scheme)

• Using a formalism that is clear & unambiguous, but also easy to read & understand; it needs to serve as an interface between hydra researchers and engineers

  • Understandable by the internal auditor
  • Understandable by an IOG engineer which is used to reading papers

• No simplification, extensions or variants; just describing a single version of the protocol -> that will be Hydra Head V1

• Also, a list of gaps between implementation and the specification is created (in Align implementation with HeadV1 protocol specification #452)

Tasks

• Refactor Head.Logic and document individual event processing steps in prose #425
• Walk-through and help rewrite new protocol spec with researchers #435
• Read/comment on HydraHeadV1 spec draft #545
• Help the researchers to extend the document of on-chain specification to also cover off-chain logic
• Interview the internal auditor to see what kind of specification they will require to audit the protocol logic #502
• Address all comments raised -> potentially updating gap list in Align implementation with HeadV1 protocol specification #452.
• Update transaction trace diagram (on miro), add explanation and add to documentation
• Backport latest HeadV1 spec into the paper ("with a red pen")
  • Using/updating "set notation" definitions (e.g. on the validation context)
• (researchers) Update properties and pen & paper proof for the Coordinated Head protocol
• Consolidate write everything into a Hydra Head V1 spec PDF
  • Write about rollbacks
  • Updated CEM pictures (at least "by hand" or using some drawing tool)
• Put it into the hydra repository Keep separate (currently on https://github.com/ch1bo/hydra-spec) to keep overleaf editing/reviewing for now -> follow-up for this Open specification with change process #693

[ch1bo]

Created this to have less in #194 and allow for more concise definition of done. Still not fleshed out fully so that's why it's 🔴

[ch1bo]

Marked 🟡 as we have made great progress and have a good write-up now with clear points what is still left to do. Some open points will remain when we close this and a follow-up is likely also required to round-off some corners on the security definition.