Decrement on-chain: Check value in the Head is preserved

Add this check in the specfication too.

hydra-plutus/src/Hydra/Contract/Head.hs

@@ -241,10 +241,21 @@ checkDecrement ctx@ScriptContext{scriptContextTxInfo = txInfo} prevParties prevS
     && checkSnapshot
     && checkSnapshotSignature
     && mustBeSignedByParticipant ctx prevHeadId
+    && mustPreserveValue
  where
+  mustPreserveValue =
+    traceIfFalse $(errorCode HeadValueIsNotPreserved) $
+      headInValue === headOutValue
+  -- NOTE: head output + whatever is decommitted needs to be equal to the head input.
+  headOutValue = txOutValue $ head $ txInfoOutputs txInfo <> decommitOutputs
+
+  headInValue = maybe mempty (txOutValue . txInInfoResolved) $ findOwnInput ctx
+
+  decommitOutputs = tail (txInfoOutputs txInfo)
+
   -- NOTE: we always assume Head output is the first one so we pick all other
   -- outputs of a decommit tx to calculate the expected hash.
-  decommitUtxoHash = hashTxOuts $ tail (txInfoOutputs txInfo)
+  decommitUtxoHash = hashTxOuts decommitOutputs
   (nextUtxoHash, nextParties, nextSnapshotNumber, nextCperiod, nextHeadId) =
     case fromBuiltinData @DatumType $ getDatum (headOutputDatum ctx) of
       Just

spec/onchain.tex

@@ -314,6 +314,7 @@ \subsection{Decrement Transaction}\label{sec:increment-tx}
 	\]
 	\item Transaction is signed by a participant $\exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valHead' \Rightarrow \keyHash_{i} \in \txKeys$.
 	\todo{Need a constraint on the value in the head?}
+	\item Value in the head is preserved $\valHead' = \valHead$.
 \end{menumerate}
 
 \begin{figure}[h] \centering