Incremental decommit

[ch1bo]

Why

Hydra Heads should not need to be closed to remove funds. This will make Hydra Heads more flexible in enables use cases where long-living Heads are beneficial.

Also, the current protocol may result in "non-finalizable" heads when some UTxO can't be represented on the Cardano mainchain. It would be desirable to recover at least compatible outputs back on L1.

What

Implement the protocol extension for de-committing only part of the Head state (without closing the Head) as already briefly described in the original Hydra Head paper.

"As user, I want to remove my funds from the head to make them available on the Cardano L1"

• When the head is open, a hydra client can request an incremental decommit using the Decommit websocket command or http request POST /decommit
  • The payload / request body is a "decommit transaction" Tx ~~is just a list of transaction output references (aka. transaction inputs), in cardano-api: [TxIn]~~
  • A decommit tx is spending inputs from the confirmed UTxO in the head, but will produce UTxO which are to be decommitted into the L1
  • All head participants agree on the decommit tx by validating it against the L2 ledger state.
  • With this agreement, the hydra-node does create and submit a decrementTx onto the L1
• ~~Submitting the decrementTx will make the requested outputs available on the Cardano L1~~
• A client output informs about the requested, approved and completed decommit

Properties

• Closing the head with a same snapshot as a previous decrement must not produce the UTxO again.
• Funds must be returned even if decrementTx was never submitted and the head gets closed instead.
• The head should be live while decommitting, i.e. process transactions of independent UTxOs.

Security

• The specification is updated and checked with researchers whether it is consistent with the properties above (walk-through)
• All validator changes are tested using the mutation testing framework, covering all constraints from the specification and we saw each test "fail for the right reason", i.e. no specification change without a corresponding mutation and (at least) one mutation per constraint

Out of scope

• Multiple decommits should be issuable irrespective whether they are "settled" yet or not. i.e. there can be times when no decommit is possible (yet)
• Incremental decommit when head is closed (= partial fanout)
• Validator changes are audited by the internal audit team at IO

How

Idea: Re-use the ReqSn and snapshots in off-chain consensus to request exclusion of UTxO. With that "granted", on-chain open state is updated in a new decrementTx. We need to make sure off-chain snapshots can only be used to close specific open heads (replay protection).

1. Head is open, $\eta_0$ locked, off-chain busy transacting
2. Client requests decommit by submitting a decommit transaction $\mathsf{tx_{dec}}$ which translates into a $ReqDec(\mathsf{tx_{dec}})$ network request
3. Each participant validates $\mathsf{tx_{dec}}$ against the confirmed ledger state $\bar{U}$ and if valid, stores outputs of $\mathsf{tx_{dec}}$ as $U_\omega$
4. Snapshot leader requests exclusion of UTxO $U_\omega$: $ReqSn(sn, txids, U_\omega)$ (TBD: only submit out-refs?)
5. All participants acknowledge $\bar{U}$ excludes $U_\omega$ by signing the corresponding snapshot's number, $\eta = \mathsf{Digest}(\bar{U})$ and $\eta_\omega = \mathsf{Digest}(U_\omega))$, where $\mathsf{Digest}$ is the same function we use today to create a "combine" of some UTxO set into a "digest" (see specification section 5.3)
6. decrementTx
   • evolves head state $(open, sn_i, \eta_i)$ by spending head output,
   • into head state $(open, sn_{i+1}, \eta_{i+1})$ + outputs equivalent to $U_\omega$
   • given a multi-signed $\xi$ of $\eta_i$, $\eta_{i+1}$, and $\eta_\omega$ as redeemer.
7. closeTx
   • evolves head state $(open, sn_i, \eta_i)$
   • into head state $(closed, sn_c, \eta_c, \eta_\omega^?)$,
   • given a multi-signed certificate "referring" $\eta_i$ of snapshotted $\eta_c$ (corresponding to a confirmed $\bar{U}$) and, if a decommit is in-flight the $\eta_\omega$, which must be present in the output head state
8. fanoutTx
   • ensures outputs correspond to both, $\eta_c$ and $\eta_{omega}$ (if present), in sequence

flowchart LR
  open0([open η0])

  open0 -- "Cert(η0,η1) + ηω" --> decrementTx
  decrementTx --> open1([open η0 η1])
  decrementTx --> decommit1([decommitted o1])
  decrementTx --> decommit2([decommitted o2])

  open1 -- "Cert(η1,ηc)"  --> closeTx
  closeTx --> closed1([closed ηc])

Possible tasks

• [x] #1205
• [x] #1209
• [x] #1223
  • Off-chain protocol changes to ReqDec and extend snapshots to hold optional $U_\omega^?$
  • Decrement transaction construction & observation
• On-chain script changes
  • [x] Verify decrementTx as open -> open transition
  • Changes to verify closeTx with state references (additional data in redeemers?)
  • Changes to verify fanoutTx to handle new $\eta_\omega^?$
• [x] #1390
• Schedule and have a spec walk-through with researchers

Latest task breakdown

• [x] #1473
• [x] #1474
• [ ] Clear red areas from #1473 by reviewing their coverage through tests in #1344

To be discussed

• How can any participant request removal if not snapshot leader?
  • [x] Add a new message $ReqDec(U_\omega)$ to request a decrement in the next snapshot (even the snapshot leader, like ReqTx)
• What happens if the incremental decommit is requested and acknowledged on the L2, but the decrementTx is never submitted to L1?
  • [x] The removed UTxO $U_\omega$ must remain part of the off-chain state and is used to fanout the full state, i.e. the closed state $\eta ~ \widehat{=} ~ \bar{U} \cup U_\omega$. For example, assuming the decrementTx above never happens, $\eta_0$ must correspond to $\bar{U} \cup U_\omega$ and fanoutTx produce all corresponding outputs
  • SMT proofs where only some UTxO are realized would make this more flexible.
  • (S)MT could allow verify $\eta \cup \eta_\omega$ in closeTx and lead to a normal closed state with a single $\eta$
  • [x] Any participant can post the decrementTx to avoid stalling.
• What if the agreed to remove state is not "fitting" into a single decrementTx?
  • Only agree "small enough" decrements off-chain (maybe complicated, but should be possible), or
  • Split off decremented state from $\eta$ and allow one or more withdrawTx (= partial fanout)?
  • [x] This can be seen as an orthogonal issue very related to the purpose of #190
• Do we need a "fancy" state reference as outlined by @mfitzi or are snapshot numbers enough?
  • Not for incremental decrement alone. Because decrements on-chain never impact off-chain availability of UTxOs. Also, rollbacks would only affect semantics if participants agree "too early" (upon seeing a decrementTx) to clean-up the corresponding $U_\omega$ from the off-chain state.
  • [x] The state reference is the same meachanism as explained in #688, but generalized for multiple open states. A state reference is basically just the $\eta$ of the previous open state and needs to be used to decide on whether an off-chain snapshot is valid against the current state or the previous state. Detailed case separation TBD here (available as draft slides).
• Why are SMT roots and non-inclusion proofs needed on the decrementTx instead of just multi-signing $\bar{U}$ and $U_\omega$?
  • [x] They not needed and we can stick with the hand-rolled concat + hash approach, iff we extend the closed state with the "to-be-decommitted" $\eta_\omega$ derived from $U_\omega$ next to the normal $eta$ and the fanoutTx needs to recreate outputs satisfying both $\eta$ and $\eta_omega$ (related to point 2)
• Is having [TxIn] on the endpoints convenient?
  • If not, change it to UTxO
  • [x] Change it to Tx as we need to authorize a decommit (see comments)
• Shall we add decrements (partial fanout) from a closed head?
  • [x] Out of scope (see What)