Add checkSnapshotNumber to checkClose

This makes sure we are closing with new enough snapshot number. Also adds changes to the spec.
input-output-hk · May 7, 2024 · 46e82a1 · 46e82a1
1 parent ef09456
commit 46e82a1
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 7 deletions.
diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs
@@ -188,7 +188,7 @@ instance StateModel Model where
         snapshotNumber `elem` snapshots && snapshotNumber > latestSnapshot
       -- TODO: assert what to decrement still there
       (Open{latestSnapshot}, Close{snapshotNumber}) ->
-        snapshotNumber `elem` snapshots && snapshotNumber > latestSnapshot
+        snapshotNumber `elem` snapshots && snapshotNumber >= latestSnapshot
       (Open{}, Contest{}) -> False
       (Closed{latestSnapshot}, Contest{snapshotNumber}) ->
         snapshotNumber `elem` snapshots && snapshotNumber > latestSnapshot

diff --git a/hydra-plutus/src/Hydra/Contract/Head.hs b/hydra-plutus/src/Hydra/Contract/Head.hs
@@ -75,8 +75,8 @@ headValidator oldState input ctx =
       checkAbort ctx headId parties
     (Open{parties, contestationPeriod, snapshotNumber, headId}, Decrement{signature, numberOfDecommitOutputs}) ->
       checkDecrement ctx parties snapshotNumber contestationPeriod headId signature numberOfDecommitOutputs
-    (Open{parties, utxoHash = initialUtxoHash, contestationPeriod, headId}, Close{signature}) ->
-      checkClose ctx parties initialUtxoHash signature contestationPeriod headId
+    (Open{parties, utxoHash = initialUtxoHash, contestationPeriod, headId, snapshotNumber}, Close{signature}) ->
+      checkClose ctx parties initialUtxoHash signature contestationPeriod headId snapshotNumber
     (Closed{parties, snapshotNumber = closedSnapshotNumber, contestationDeadline, contestationPeriod, headId, contesters}, Contest{signature}) ->
       checkContest ctx contestationDeadline contestationPeriod parties closedSnapshotNumber signature contesters headId
     (Closed{parties, utxoHash, contestationDeadline, headId}, Fanout{numberOfFanoutOutputs}) ->
@@ -298,8 +298,9 @@ checkClose ::
   [Signature] ->
   ContestationPeriod ->
   CurrencySymbol ->
+  SnapshotNumber ->
   Bool
-checkClose ctx parties initialUtxoHash sig cperiod headPolicyId =
+checkClose ctx parties initialUtxoHash sig cperiod headPolicyId snapshotNumber =
   mustNotMintOrBurn txInfo
     && hasBoundedValidity
     && checkDeadline
@@ -308,7 +309,12 @@ checkClose ctx parties initialUtxoHash sig cperiod headPolicyId =
     && mustInitializeContesters
     && mustPreserveValue
     && mustNotChangeParameters (parties', parties) (cperiod', cperiod) (headId', headPolicyId)
+    && checkSnapshotNumber
  where
+  checkSnapshotNumber =
+    traceIfFalse $(errorCode TooOldSnapshot) $
+      closedSnapshotNumber >= snapshotNumber
+
   mustPreserveValue =
     traceIfFalse $(errorCode HeadValueIsNotPreserved) $
       val === val'
@@ -326,15 +332,15 @@ checkClose ctx parties initialUtxoHash sig cperiod headPolicyId =
     case fromBuiltinData @DatumType $ getDatum (headOutputDatum ctx) of
       Just
         Closed
-          { snapshotNumber
+          { snapshotNumber = sn
           , utxoHash
           , utxoToDecommitHash
           , parties = p
           , contestationDeadline
           , headId
           , contesters
           , contestationPeriod
-          } -> (snapshotNumber, utxoHash, utxoToDecommitHash, p, contestationDeadline, contestationPeriod, headId, contesters)
+          } -> (sn, utxoHash, utxoToDecommitHash, p, contestationDeadline, contestationPeriod, headId, contesters)
       _ -> traceError $(errorCode WrongStateInOutputDatum)
 
   checkSnapshot

diff --git a/spec/onchain.tex b/spec/onchain.tex
@@ -448,7 +448,7 @@ \subsection{Close Transaction}\label{sec:close-tx}
 
 	\item Closing snapshot number $s'$ is higher than the currently stored snapshot number $s$
 	\[
-		s' > s
+		s' \geq s
 	\]
 	\item Record the closed head state
 	\[