Align implementation with HeadV1 protocol specification

[ch1bo]

Why

In the work stream to mature the Hydra Head protocol enough to aim for a mainnet release, we have been running our implementation against a formal model and created an updated specifiction (because the protocol evolved since publishing the peer-reviewed paper).

These prior works will/did highlight gaps in our implementation of the protocol behavior and/or the scripts that should ensure protocol security on the layer 1.

What

This work package is about addressing and closing these first gaps:

• Make sure the on-chain code (validators) is checking what is specified
• Make sure the off-chain code (HeadLogic + chain layer) is working as specified

How

• Create an updated version of transaction traces & publish them to website #639
  • Useful to do this before and after addressing the changes in this feature!
  • Also, we want to make this more visible in our documentation as it helps understand the protocol (e.g. create a page in "core concepts" on the website)
  • Not sure what we want to do about this traces now so let's keep them internal for now as a conversation tool and see what happens later
• Go through all the gaps and fix them (See below)
  • Update or create tests corresponding to each item and link them from the gap list closed in this work package

Gaps identified so far

Transition security

• ST in output not checked #658
• Upper tx validity could be very big on close/contest  #592
  • enforce a bound using T_max - T_min < some slots
• Any transaction spending the initial outputs or head output (i.e. any output created by the init transaction) should be authenticated but spending initial outputs with a ViaAbort redeemer is not authenticate and should be. Checking the ST is burned by the transaction could help solving this gap. ST in output not checked #658
• check commits are reimbursed in nu head #670
• Validator can assume head output is the first one #700
• Check that value is preserved in v_head #702
• Check for no token burning needs to be a part of v_head checks  #691
• Snapshot number and utxo hash need not be in the redeemer on close/contest #677
  • the output datum needs to include them and we can check using that
  • only the signature is enough
• Do allow contest only once #680
  • need to collect who contested in the datum and check it
  • needed to be followed-up by 👇 to have not a strict upper T_final
• Deadline handling changed between paper and V1 spec -> Deadline gets "pushed out" on each contest #716
  • this makes the contestation period easier to determine and scales with number of parties
• No need to check quantity, PT distribution when minting tokens #712
  • Extracted to Align minting policy #720
  • "Actors will need check off-chain whether an initTx is well formed"
  • Determine minted quantities and whether PTs are paid to v_initial off-chain.

Protocol logic

• Sign network messages / authenticate them to be sure they are from a given Party (Hydra VK)

  • Extracted into Authenticate network messages #727

• Not send transactions with ReqSn, but only transaction ids (Hashes of transactions)

  • Extracted into ReqSn only sends transaction ids #728

• Inline snapshot emission #729

• "Detect cheating" if we see a ReqSn or AckSn with s > s_seen + 1 Align HeadLogic: require snapshot not too far in the future #733

• Prune pending transactions by applicability, not only by id Align HeadLogic: Transaction pruning #740

• Actually check the aggregated signature and "detect cheating" if not Align HeadLogic: verify aggregated multi-signature #741

• Do not check transactions in NewTx Align HeadLogic: Not validate tx on NewTx #745

[ch1bo]

Marked 🔴 as not yet discussed. Depends on outcomes of #194 #448.

[abailly-iohk]

Marked amber as the list of gaps appears somewhat clearer (and solvable...)

[ch1bo]

When running hydra heads we might have discovered another gap / at least an annoyance: #612

[ch1bo]

Marking this 🔴 as the scope of this is very large and there is still substantial work to be done. Ideally, we should split things into smaller marketable features (e.g. safeguarding against one or the other attack)