Add StateSpec properties for decrement

Remove === from the checkDecrement validator since it requires proper ordering.
input-output-hk · May 7, 2024 · 6d9a8cb · 6d9a8cb
1 parent f4dc94b
commit 6d9a8cb
Show file tree

Hide file tree

Showing 5 changed files with 21 additions and 8 deletions.
diff --git a/hydra-node/src/Hydra/Chain.hs b/hydra-node/src/Hydra/Chain.hs
@@ -21,16 +21,14 @@ import Hydra.Cardano.Api (
   Coin (..),
  )
 import Hydra.ContestationPeriod (ContestationPeriod)
-import Hydra.Environment (Environment (..))
 import Hydra.Crypto (MultiSignature)
+import Hydra.Environment (Environment (..))
 import Hydra.HeadId (HeadId, HeadSeed)
 import Hydra.Ledger (ChainSlot, IsTx, UTxOType)
 import Hydra.OnChainId (OnChainId)
 import Hydra.Party (Party)
-import Hydra.Snapshot (ConfirmedSnapshot, SnapshotNumber)
-import Test.Cardano.Ledger.Core.Arbitrary ()
 import Hydra.Snapshot (ConfirmedSnapshot, Snapshot, SnapshotNumber)
-import Test.QuickCheck (scale, suchThat)
+import Test.Cardano.Ledger.Core.Arbitrary ()
 import Test.QuickCheck.Instances.Semigroup ()
 import Test.QuickCheck.Instances.Time ()
 

diff --git a/hydra-node/src/Hydra/Chain/Direct/State.hs b/hydra-node/src/Hydra/Chain/Direct/State.hs
@@ -104,7 +104,7 @@ import Hydra.Contract.Head qualified as Head
 import Hydra.Contract.HeadState qualified as Head
 import Hydra.Contract.HeadTokens (headPolicyId, mkHeadTokenScript)
 import Hydra.Contract.Initial qualified as Initial
-import Hydra.Crypto (HydraKey, MultiSignature)
+import Hydra.Crypto (HydraKey, MultiSignature, aggregate, sign)
 import Hydra.HeadId (HeadId (..))
 import Hydra.Ledger (ChainSlot (ChainSlot), IsTx (hashUTxO))
 import Hydra.Ledger.Cardano (genOneUTxOFor, genUTxOAdaOnlyOfSize, genVerificationKey)
@@ -1034,7 +1034,7 @@ genDecrementTx numParties = do
     number <- getPositive <$> arbitrary
     (utxo, toDecommit) <- splitUTxO u0
     pure Snapshot{headId, number, confirmed = [], utxo, utxoToDecommit = Just toDecommit}
-  signatures <- arbitrary
+  let signatures = aggregate $ fmap (`sign` snapshot) (ctxHydraSigningKeys ctx)
   let openUTxO = getKnownUTxO stOpen
   pure (cctx, stOpen, unsafeDecrement cctx headId (ctxHeadParameters ctx) openUTxO snapshot signatures)
 

diff --git a/hydra-node/test/Hydra/Chain/Direct/StateSpec.hs b/hydra-node/test/Hydra/Chain/Direct/StateSpec.hs
@@ -68,6 +68,7 @@ import Hydra.Chain.Direct.State (
   genCommits,
   genCommits',
   genContestTx,
+  genDecrementTx,
   genFanoutTx,
   genHydraContext,
   genInitTx,
@@ -123,6 +124,7 @@ import Test.QuickCheck (
   forAll,
   forAllBlind,
   forAllShow,
+  forAllShrink,
   getPositive,
   label,
   sized,
@@ -307,6 +309,10 @@ spec = parallel $ do
     propBelowSizeLimit maxTxSize forAllCollectCom
     propIsValid forAllCollectCom
 
+  describe "decrement" $ do
+    propBelowSizeLimit maxTxSize forAllDecrement
+    propIsValid forAllDecrement
+
   describe "close" $ do
     propBelowSizeLimit maxTxSize forAllClose
     propIsValid forAllClose
@@ -573,6 +579,15 @@ forAllCollectCom action =
      in action utxo tx
           & counterexample ("Committed UTxO: " <> show committedUTxO)
 
+forAllDecrement ::
+  Testable property =>
+  (UTxO -> Tx -> property) ->
+  Property
+forAllDecrement action = do
+  forAllShrink (genDecrementTx maximumNumberOfParties) shrink $ \(ctx, st, tx) ->
+    let utxo = getKnownUTxO st <> getKnownUTxO ctx
+     in action utxo tx
+
 forAllClose ::
   Testable property =>
   (UTxO -> Tx -> property) ->

diff --git a/hydra-node/test/Hydra/HeadLogicSpec.hs b/hydra-node/test/Hydra/HeadLogicSpec.hs
@@ -154,7 +154,7 @@ spec =
           let input = NetworkInput defaultTTL alice reqDec
           st <- pickBlind $ oneof $ pure <$> [inInitialState threeParties, inIdleState, inClosedState threeParties]
           pure $
-            update aliceEnv ledger st event
+            update aliceEnv ledger st input
               `shouldNotBe` cause (NetworkEffect reqDec)
 
         it "wait for second decommit when another one is in flight" $ do

diff --git a/hydra-plutus/src/Hydra/Contract/Head.hs b/hydra-plutus/src/Hydra/Contract/Head.hs
@@ -259,7 +259,7 @@ checkDecrement ctx@ScriptContext{scriptContextTxInfo = txInfo} prevParties prevS
 
   mustDecreaseValue =
     traceIfFalse $(errorCode HeadValueIsNotPreserved) $
-      headInValue === headOutValue <> foldMap txOutValue decommitOutputs
+      headInValue == headOutValue <> foldMap txOutValue decommitOutputs
 
   -- 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.