diff --git a/hydra-node/src/Hydra/HeadLogic.hs b/hydra-node/src/Hydra/HeadLogic.hs index 6b20a238c18..b9d6108edd9 100644 --- a/hydra-node/src/Hydra/HeadLogic.hs +++ b/hydra-node/src/Hydra/HeadLogic.hs @@ -238,7 +238,7 @@ data CoordinatedHeadState tx = CoordinatedHeadState -- ^ List of transactions applied locally and pending inclusion in a snapshot. Spec: T̂ , allTxs :: Map.Map (TxIdType tx) tx -- ^ Map containing all the transactions ever seen by this node and not yet - -- included in a snapshot. Spec: T̂all + -- included in a snapshot. Spec: Tall , confirmedSnapshot :: ConfirmedSnapshot tx -- ^ The latest confirmed snapshot. Spec: U̅, s̅ and σ̅ , seenSnapshot :: SeenSnapshot tx @@ -652,7 +652,7 @@ onOpenNetworkReqTx :: tx -> Outcome tx onOpenNetworkReqTx env ledger st ttl tx = do - -- Spec: T̂all ← ̂Tall ∪ { (hash(tx), tx) } + -- Spec: Tall ← ̂Tall ∪ { (hash(tx), tx) } let chs' = coordinatedHeadState{allTxs = allTxs <> fromList [(txId tx, tx)]} -- Spec: wait L̂ ◦ tx ≠ ⊥ combined with L̂ ← L̂ ◦ tx waitApplyTx chs' $ \utxo' -> do @@ -673,9 +673,9 @@ onOpenNetworkReqTx env ledger st ttl tx = do { coordinatedHeadState = chs'' { seenSnapshot = - -- FIXME: Open point: This state update has no - -- equivalence in the spec. Do we really need to - -- store that we have requested a snapshot? + -- XXX: This state update has no equivalence in the + -- spec. Do we really need to store that we have + -- requested a snapshot? If yes, should update spec. RequestedSnapshot { lastSeen = seenSnapshotNumber seenSnapshot , requested = nextSn @@ -752,9 +752,9 @@ onOpenNetworkReqSn env ledger st otherParty sn requestedTxIds = requireReqSn $ -- Spec: wait s̅ = ŝ waitNoSnapshotInFlight $ - -- Spec: wait ∀h ∈ Treq : (h, ·) ∈ T̂all + -- Spec: wait ∀h ∈ Treq : (h, ·) ∈ Tall waitResolvableTxs $ do - -- Spec: Treq ← {T̂all [h] | h ∈ Treq#} + -- Spec: Treq ← {Tall [h] | h ∈ Treq#} let requestedTxs = mapMaybe (`Map.lookup` allTxs) requestedTxIds -- Spec: require U̅ ◦ Treq /= ⊥ combined with Û ← Ū̅ ◦ Treq requireApplyTxs requestedTxs $ \u -> do @@ -765,7 +765,7 @@ onOpenNetworkReqSn env ledger st otherParty sn requestedTxIds = (Effects [NetworkEffect $ AckSn snapshotSignature sn] `Combined`) $ do -- Spec: for loop which updates T̂ and L̂ let (localTxs', localUTxO') = pruneTransactions u - -- Spec: T̂all ← {tx | ∀tx ∈ T̂all : tx ∉ Treq } + -- Spec: Tall ← {tx | ∀tx ∈ Tall : tx ∉ Treq } let allTxs' = foldr Map.delete allTxs requestedTxIds NewState ( Open diff --git a/spec/fig_offchain_prot.tex b/spec/fig_offchain_prot.tex index c396caf5502..1d039091663 100644 --- a/spec/fig_offchain_prot.tex +++ b/spec/fig_offchain_prot.tex @@ -75,7 +75,7 @@ \On{$(\hpRT,\tx)$ from $\party_j$}{% % track tx in state - $\hatmT_{\mathsf{all}} \gets \hatmT_{\mathsf{all}} \cup \{ (\hash(\tx),\tx )\}$ + $\mT_{\mathsf{all}} \gets \mT_{\mathsf{all}} \cup \{ (\hash(\tx),\tx )\}$ \Wait{$\hatmL \applytx \tx \neq \bot$}{ @@ -98,13 +98,13 @@ \Req{$s = \hats + 1 ~ \land ~ \hpLdr(s) = j$} \; % % Wait for snapshot no snapshot in flight anymore and all txs applicable - \Wait{$\bars = \hats ~ \land ~ \forall h \in \mT^{\#}_{req} : (h, \cdot) \in \hatmT_{\mathsf{all}}$}{ + \Wait{$\bars = \hats ~ \land ~ \forall h \in \mT^{\#}_{req} : (h, \cdot) \in \mT_{\mathsf{all}}$}{ - $\mT_{req} \gets \{ \hatmT_{\mathsf{all}}[h] ~ | ~ \forall h \in \mT^{\#}_{req} \}$ + $\mT_{\mathsf{req}} \gets \{ \mT_{\mathsf{all}}[h] ~ | ~ \forall h \in \mT^{\#}_{req} \}$ - \Req{$\barmU \applytx \mT_{req} \not= \bot$} + \Req{$\barmU \applytx \mT_{\mathsf{req}} \not= \bot$} - $\hatmU \gets \barmU \applytx \mT_{req}$ \; % + $\hatmU \gets \barmU \applytx \mT_{\mathsf{req}}$ \; % $\hats \gets \bars + 1$ \; % @@ -117,7 +117,7 @@ $\Multi{}~(\hpAS,\hats,\msSig_i)$ \; % - $\forall \tx \in \mT_{req}: \Out~(\hpSeen,\tx)$ \; % + $\forall \tx \in \mT_{\mathsf{req}}: \Out~(\hpSeen,\tx)$ \; % % TODO: Should we inform users if we drop a transaction? % XXX: This is a bit verbose for the spec @@ -129,7 +129,7 @@ $\hatmL\gets\hatmL\applytx \tx$ \; } - $\hatmT_{\mathsf{all}} \gets \{ tx ~ | ~ \forall tx \in \hatmT_{\mathsf{all}} : tx \notin \mT_{req} \}$ + $\mT_{\mathsf{all}} \gets \{ tx ~ | ~ \forall tx \in \mT_{\mathsf{all}} : tx \notin \mT_{\mathsf{req}} \}$ } \end{walgo} } & @@ -160,7 +160,7 @@ $\barsigma \gets \msCSig$ \; % %$\Out~(\hpSnap,(\bars,\barmU))$ \; % - $\forall \tx \in \mT_{req} : \Out (\hpConf,\tx)$ \; % + $\forall \tx \in \mT_{\mathsf{req}} : \Out (\hpConf,\tx)$ \; % % issue snapshot if we are leader \If{$\hpLdr(s+1) = i \land \hatmT \neq \emptyset$}{% diff --git a/spec/offchain.tex b/spec/offchain.tex index 804c04b2adc..48646ac0471 100644 --- a/spec/offchain.tex +++ b/spec/offchain.tex @@ -108,7 +108,7 @@ \subsection{Variables} applying $\hatmT$ to $\barmU$ to validate requested transactions. \item $\hatmT \in \mT^{*}$: List of transactions applied locally and pending inclusion in a snapshot (if this party is the next leader). - \item $\hatmT_{\mathsf{all}} \in (\tyBytes \times \mT)^{*}$: Associative list of all + \item $\mT_{\mathsf{all}} \in (\tyBytes \times \mT)^{*}$: Associative list of all seen transactions not yet included in a snapshot. \end{itemize} @@ -162,42 +162,50 @@ \subsubsection{Processing transactions off-chain} results in it being sent out to all parties as a $(\hpRT,\tx)$ message.\\ \dparagraph{$\hpRT$.}\quad Upon receiving request $(\hpRT,\tx)$, the transaction -gets recorded in $\hatmT$ and $\mT$ and applied to the local \emph{seen} ledger state -$\hatmL \applytx \tx$. If there is no current snapshot ``in flight'' -($\hats = \bars$) and the receiving party $\party_{i}$ is the next snapshot +gets recorded in $\mT_{\mathsf{all}}$ and applied to the \emph{local} ledger +state $\hatmL \applytx \tx$. If not applicable yet, the protocol does $\KwWait$ +to retry later or eventually marks this transaction as invalid (see assumption +about events piling up). After applying and if there is no current snapshot ``in +flight'' ($\hats = \bars$) and the receiving party $\party_{i}$ is the next +snapshot leader, a message to request snapshot signatures $\hpRS$ is sent. \\ -\dparagraph{$\hpRS$.}\quad Upon receiving request $(\hpRS,s,\mT_{res})$ from -party $\party_j$, the receiver $\party_i$ checks that $s$ is the next snapshot -number and that party $\party_j$ is responsible for leading its -creation.\todo{define $\hpLdr$} Party $\party_i$ then waits until the previous -snapshot is confirmed ($\bars = \hats$), and all requested transactions have -been seen ($\mT_{res} \subseteq \mT$). Then all requested transactions $\mT_{res}$ -must be applicable to $\barmU$, otherwise the snapshot is rejected as invalid. -Only then, $\party_i$ increments their seen-snapshot counter $\hats$, resets the -signature accumulator $\hatSigma$, and computes the UTxO set $\hatmU$ of the new -(seen) snapshot as $\hatmU \gets \barmU \applytx \mT_{res}$. Then, $\party_i$ -creates a signature $\msSig_i$ using their signing key $\hydraSigningKey$ on a -message comprised by \textcolor{red}{the $\cid$, the $\eta_{0}$ corresponding to - the initial UTxO set $\Uinit$, and} the new $\eta'$ given by the new snapshot -number $\hats$ and canonically combining $\hatmU$ (see -Section~\ref{sec:close-tx} for details). The signature is sent to all head -members via message $(\hpAS,\hats,\msSig_i)$. Finally, the pending transaction -set $\hatmT$ gets pruned by the just requested transactions $\mT_{res}$ and the -local ledger state $\hatmL$ is updated accordingly.\\ - -\dparagraph{$\hpAS$.}\quad Upon receiving acknowledgment $(\hpAS,s,\msSig_j)$, -all participants $\Req$ that it is from an expected snapshot (either the last -seen $\hats$ or + 1), potentially $\KwWait$ for the corresponding $\hpRS$ such -that $\hats = s$ and $\Req$ that the signature is not yet included in -$\hatSigma$. They store the received signature in the signature accumulator -$\hatSigma$, and if signature from each party has been collected, $\party_i$ -aggregates the multisignature $\msCSig$ and $\Req$ it to be valid. If everything -is fine, the snapshot can be considered confirmed by updating $\bars=s$ and -participants also store the UTxO set in $\barmU$, as well as the signature in -$\barsigma$ for later reference. Similar to the $\hpRT$, if $\party_i$ is the -next snapshot leader and there are already transactions to snapshot in $\hatmT$, -a corresponding $\hpRS$ is distributed. +\dparagraph{$\hpRS$.}\quad Upon receiving request +$(\hpRS,s,\mT_{\mathsf{req}}^{\#})$ from party $\party_j$, the receiver +$\party_i$ checks that $s$ is the next snapshot number and that party $\party_j$ +is responsible for leading its creation.\todo{define $\hpLdr$} Party $\party_i$ +has to $\KwWait$ until the previous snapshot is confirmed ($\bars = \hats$) and +all requested transaction hashes $\mT_{\mathsf{req}}^{\#}$ can be resolved in +$\mT_{\mathsf{all}}$. Then, all those resolved transactions $\mT_{\mathsf{req}}$ +are $\Req$d to be applicable to $\barmU$, otherwise the snapshot is rejected +as invalid. Only then, $\party_i$ increments their seen-snapshot counter +$\hats$, resets the signature accumulator $\hatSigma$, and computes the UTxO set +$\hatmU$ of the new (seen) snapshot as +$\hatmU \gets \barmU \applytx \mT_{\mathsf{req}}$. Then, $\party_i$ creates a +signature $\msSig_i$ using their signing key $\hydraSigningKey$ on a message +comprised by \textcolor{red}{the $\cid$, the $\eta_{0}$ corresponding to the + initial UTxO set $\Uinit$, and} the new $\eta'$ given by the new snapshot number +$\hats$ and canonically combining $\hatmU$ (see Section~\ref{sec:close-tx} for +details). The signature is sent to all head members via message +$(\hpAS,\hats,\msSig_i)$. Finally, the pending transaction set $\hatmT$ gets +pruned by re-applying all locally pending transactions $\hatmT$ to the just +requested snapshot's UTxO set $\hatmU$ iteratively and ultimately yielding a +``pruned'' version of $\hatmT$ and $\hatmU$. Also, the set of all transactions +$\mT_{\mathsf{all}}$ can be reduced by the requested +transactions $\mT_{\mathsf{req}}$.\\ + +\dparagraph{$\hpAS$.}\quad Upon receiving acknowledgment $(\hpAS,s,\msSig_j)$, all +participants $\Req$ that it is from an expected snapshot (either the last seen +$\hats$ or + 1), potentially $\KwWait$ for the corresponding $\hpRS$ such that +$\hats = s$ and $\Req$ that the signature is not yet included in $\hatSigma$. +They store the received signature in the signature accumulator $\hatSigma$, and +if the signature from each party has been collected, $\party_i$ aggregates the +multisignature $\msCSig$ and $\Req$ it to be valid. If everything is fine, the +snapshot can be considered confirmed by updating $\bars=s$ and participants also +store the UTxO set in $\barmU$, as well as the signature in $\barsigma$ for +later reference. Similar to the $\hpRT$, if $\party_i$ is the next snapshot +leader and there are already transactions to snapshot in $\hatmT$, a +corresponding $\hpRS$ is distributed. \subsubsection{Closing the head}