Identify some gaps and start removing sn from eta

cardano-scaling · Mar 7, 2024 · 3d991be · 3d991be
1 parent 159ce16
commit 3d991be
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 9 deletions.
diff --git a/hydra-node/src/Hydra/HeadLogic.hs b/hydra-node/src/Hydra/HeadLogic.hs
@@ -29,6 +29,7 @@ import Data.Set ((\\))
 import Data.Set qualified as Set
 import GHC.Records (getField)
 import Hydra.API.ClientInput (ClientInput (..))
+import Hydra.API.HTTPServer (DraftCommitTxRequest (utxoToCommit))
 import Hydra.API.ServerOutput qualified as ServerOutput
 import Hydra.Chain (
   ChainEvent (..),
@@ -441,6 +442,10 @@ onOpenNetworkReqSn env ledger st otherParty sn requestedTxIds mDecommitTx =
     case mDecommitTx of
       Nothing -> cont (confirmedUTxO, Nothing)
       Just decommitTx ->
+        -- FIXME: Why don't we apply the decommitTx to the confirmed UTxO? Right
+        -- now the inputs would still remain on the L2 state and actually don't
+        -- get removed by 'withoutUTxO' below, because the utxoToCommit are not
+        -- in confirmedUTxO (but the inputs of the decommitTx would be).
         case canApply ledger currentSlot confirmedUTxO decommitTx of
           Invalid err ->
             Error $ RequireFailed $ DecommitDoesNotApply decommitTx err

diff --git a/hydra-plutus/src/Hydra/Contract/HeadState.hs b/hydra-plutus/src/Hydra/Contract/HeadState.hs
@@ -30,15 +30,15 @@ data State
       { contestationPeriod :: ContestationPeriod
       , parties :: [Party]
       , utxoHash :: Hash
+      -- ^ Spec: η
       , headId :: CurrencySymbol
       , snapshotNumber :: SnapshotNumber
       }
   | Closed
       { parties :: [Party]
       , snapshotNumber :: SnapshotNumber
-      -- ^ Spec: fst of η
       , utxoHash :: Hash
-      -- ^ Spec: snd of η
+      -- ^ Spec: η
       , utxoToDecommitHash :: Hash
       -- ^ Spec: ηω
       , contestationDeadline :: POSIXTime

diff --git a/spec/fig_offchain_prot.tex b/spec/fig_offchain_prot.tex
@@ -35,6 +35,7 @@
 							$C_j \gets U $
 
 							\If{$\forall k \in [1..n]: C_k \neq \undefined$}{
+    						    %% FIXME: eta without snapshot number
 								$\eta \gets (0, \combine([C_1 \dots C_n]))$ \;
 								$\PostTx{}~(\mtxCCom, \eta)$ \;
 							}
@@ -101,12 +102,14 @@
 						\On{$(\mathtt{reqDec},\tx)$ from $\party_j$}{
 						    \textcolor{red}{
 							\Wait{$\tx_\omega = \bot ~ \land ~ \barmU \applytx \tx \not= \bot$}{
+							  \textcolor{black}{
 								$\tx_\omega \gets \tx$ \;
 								% issue snapshot if we are leader
 								\If{$\hats = \bars \land \hpLdr(\bars + 1) = i$}{
 									$\textcolor{blue}{\mT^{\#}_{req} \gets \{ \hash(\tx) ~ | ~ \forall tx \in \hatmT \}}$ \;
-									\Multi{} $(\hpRS,\bars+1,\mT^{\#}_{req}, \tx_{\omega})$ \;
+									\Multi{} $(\hpRS,\bars+1,\mT^{\#}_{req}, \textcolor{blue}{\tx})$ \;
 								}
+							  }
 							}
 							}
 						}
@@ -132,17 +135,16 @@
 							\Wait{$\bars = \hats ~ \land ~ \forall h \in  \mT^{\#}_{req} : (h, \cdot) \in \mT_{\mathsf{all}}$}{
 								$\mT_{\mathsf{req}} \gets \{ \mT_{\mathsf{all}}[h] ~ | ~ \forall h \in \mT^{\#}_{req} \}$ \;
 							    \textcolor{red}{\Req{$\barmU \applytx \tx_{\omega} \not= \bot$}} \;
-								\textcolor{red}{$\mathcal{U_{\omega}} \gets \mathsf{outputs}(\tx_{\omega})$} \;
-								\textcolor{red}{$\barmU_{\mathsf{active}} \gets \barmU \setminus \mathcal{U}_{\omega}$} \;
+							    \textcolor{red}{$\barmU_{\mathsf{active}} \gets \barmU \applytx \tx_{\omega}$} \;
 								\Req{$\textcolor{red}{\barmU_{\mathsf{active}}} \applytx \mT_{\mathsf{req}} \not= \bot$} \;
 								$\hatmU \gets \textcolor{red}{\barmU_{\mathsf{active}}} \applytx \mT_{\mathsf{req}}$ \;
 								$\hats \gets \bars + 1$ \;
-                                % TODO: eta without snapshot number
-								$\eta' \gets (\hats, \combine(\hatmU))$ \;
-								$\textcolor{red}{\eta_{\omega} \gets \combine(\mathcal{U}_{\omega})}$ \;
+								\textcolor{red}{$\eta' \gets \combine(\hatmU)$} \;
+								$\textcolor{red}{\eta_{\omega} \gets \combine(\mathsf{outputs}(\tx_{\omega}))}$ \;
 								% NOTE: WE could make included transactions auditable by adding
 								% a merkle tree root to the (signed) snapshot data \eta'
-								$\msSig_i \gets \msSign(\hydraSigningKey, (\cid || \textcolor{red}{\eta_{0} ||} \eta' || \textcolor{red}{\eta_{\omega}}))$ \;
+								% TODO: sign \eta_{0} / previous state?
+								$\msSig_i \gets \msSign(\hydraSigningKey, (\cid || \textcolor{red}{\hats || \eta' || \eta_{\omega}}))$ \;
 								$\hatSigma \gets \emptyset$ \;
 								$\Multi{}~(\hpAS,\hats,\msSig_i)$ \;
 								$\forall \tx \in \mT_{\mathsf{req}}: \Out~(\hpSeen,\tx)$ \;
@@ -209,6 +211,7 @@
 					\begin{walgo}{0.6}
 						% CLOSE from client
 						\On{$(\hpClose)$ from client}{
+						    %% FIXME: eta without snapshot number
 							$\eta' \gets (\bars, \combine(\barmU))$ \;
 							$\xi \gets \barsigma$ \;
 							$\PostTx{}~(\mtxClose, \eta', \xi)$ \;
@@ -221,6 +224,7 @@
 						\On{$(\gcChainClose, \eta) \lor (\gcChainContest, \eta)$ from chain}{
 							$(s_{c}, \cdot) \gets \eta$ \;
 							\If{$\bars > s_{c}$}{
+						        %% FIXME: eta without snapshot number
 								$\eta' \gets (\bars, \combine(\barmU))$ \;
 								$\xi \gets \barsigma$ \;
 								$\PostTx{}~(\mtxContest, \eta', \xi)$ \;