Align decommit off-chain spec/impl

These checks there are really not "require" statements, as they would not "detect cheating" as described in the specification.
input-output-hk · May 7, 2024 · 8ef2b16 · 8ef2b16
1 parent 5e922d2
commit 8ef2b16
Show file tree

Hide file tree

Showing 3 changed files with 42 additions and 56 deletions.
diff --git a/hydra-node/src/Hydra/HeadLogic.hs b/hydra-node/src/Hydra/HeadLogic.hs
@@ -620,24 +620,49 @@ onOpenClientDecommit ::
   tx ->
   Outcome tx
 onOpenClientDecommit env headId ledger currentSlot coordinatedHeadState decommitTx =
-  case mExistingDecommitTx of
-    Just existingDecommitTx ->
-      causes
-        [ ClientEffect
-            ServerOutput.DecommitInvalid
-              { headId
-              , decommitInvalidReason = ServerOutput.DecommitAlreadyInFlight{decommitTx = existingDecommitTx}
-              }
+  checkNoDecommitInFlight $
+    checkValidDecommitTx $
+      Effects
+        [ NetworkEffect ReqDec{transaction = decommitTx, decommitRequester = party}
         ]
-    Nothing ->
-      requireValidDecommitTx headId ledger currentSlot coordinatedHeadState decommitTx $
-        causes
-          [ NetworkEffect ReqDec{transaction = decommitTx, decommitRequester = party}
-          ]
  where
-  Environment{party} = env
+  checkNoDecommitInFlight continue =
+    case mExistingDecommitTx of
+      Just existingDecommitTx ->
+        Effects
+          [ ClientEffect
+              ServerOutput.DecommitInvalid
+                { headId
+                , decommitInvalidReason = ServerOutput.DecommitAlreadyInFlight{decommitTx = existingDecommitTx}
+                }
+          ]
+      Nothing -> continue
+
+  checkValidDecommitTx cont =
+    case applyTransactions ledger currentSlot confirmedUTxO [decommitTx] of
+      Left (_, err) ->
+        Effects
+          [ ClientEffect
+              ServerOutput.DecommitInvalid
+                { headId
+                , decommitInvalidReason =
+                    ServerOutput.DecommitTxInvalid
+                      { confirmedUTxO
+                      , decommitTx
+                      , validationError = err
+                      }
+                }
+          ]
+      Right _ -> cont
+
+  confirmedUTxO = (getSnapshot confirmedSnapshot).utxo
+
+  CoordinatedHeadState{confirmedSnapshot} = coordinatedHeadState
+
   CoordinatedHeadState{decommitTx = mExistingDecommitTx} = coordinatedHeadState
 
+  Environment{party} = env
+
 -- | Process the request 'ReqDec' to decommit something from the Open head.
 --
 -- __Transition__: 'OpenState' → 'OpenState'
@@ -1204,40 +1229,3 @@ recoverState ::
   t (StateChanged tx) ->
   HeadState tx
 recoverState = foldl' aggregate
-
--- Decommit helpers
-
--- TODO: Spec: require U̅ ◦ decTx /= ⊥
-
--- | Prevents further evaluation if Decommit tx is not applicable to the local
--- ledger state. In this case emits 'DecommitInvalid' otherwise it alows
--- continuation to proceed.
-requireValidDecommitTx ::
-  Monoid (UTxOType tx) =>
-  HeadId ->
-  Ledger tx ->
-  ChainSlot ->
-  CoordinatedHeadState tx ->
-  tx ->
-  Outcome tx ->
-  Outcome tx
-requireValidDecommitTx headId ledger currentSlot coordinatedHeadState decommitTx cont =
-  case applyTransactions ledger currentSlot confirmedUTxO [decommitTx] of
-    Left (_, err) ->
-      causes
-        [ ClientEffect
-            ServerOutput.DecommitInvalid
-              { headId
-              , decommitInvalidReason =
-                  ServerOutput.DecommitTxInvalid
-                    { confirmedUTxO
-                    , decommitTx
-                    , validationError = err
-                    }
-              }
-        ]
-    Right _ -> cont
- where
-  confirmedUTxO = (getSnapshot confirmedSnapshot).utxo
-
-  CoordinatedHeadState{confirmedSnapshot} = coordinatedHeadState
diff --git a/spec/fig_offchain_prot.tex b/spec/fig_offchain_prot.tex
@@ -90,10 +90,8 @@
 
 						%%% DECOMMIT
 						\On{$(\mathtt{decommit},\tx)$ from client}{
-						    \textcolor{red}{
-							% TODO: check U_\omega is bottom to not have multiple in-flight?
-							\Req{$\barmU \applytx \tx \not= \bot$} \;
-							\Multi{} $(\mathtt{reqDec},\tx)$%
+							\If{\textcolor{blue}{$\tx_{\omega} = \bot \land \barmU \applytx \tx \not= \bot$}}{
+							  \Multi{} $(\mathtt{reqDec},\tx)$%
 							}
 						}
 

diff --git a/spec/prel.tex b/spec/prel.tex
@@ -20,7 +20,7 @@ \subsection{Notation}
 
 \noindent Furthermore, given a set $\mathcal{A}$, let
 \begin{itemize}
-	\item $\mathcal{A}^? = \mathcal{A} \cup \Diamond$ denotes an option: a value from $\mathcal{A}$ or no value at all,
+	\item $\mathcal{A}^? = \mathcal{A} \cup \Diamond$ denotes an option: a value from $\mathcal{A}$ or no value at all indicated by $\bot$,
 	\item $\mathcal{A}^n$ be the set of all n-sized sequences over $\mathcal{A}$,
 	\item $\mathcal{A}^! = \bigcup_{i=1}^{n \in \tyNatural} \mathcal{A}^{i}$ be the set of non-empty sequences over $\mathcal{A}$, and
 	\item $\mathcal{A}^* = \bigcup_{i=0}^{n \in \tyNatural} \mathcal{A}^{i}$ be