From ad0715ae20c3fc954e6e7c81592e312adccdeb6c Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Wed, 9 Oct 2024 08:39:16 +0200 Subject: [PATCH 01/21] Add coverage to prop_runActions This will ensure we have good coverage of the actual model test later. For now, the efficiency is way to low to checkCoverage on it too (it would go up to 6400 tests like prop_traces). --- .../test/Hydra/Chain/Direct/TxTraceSpec.hs | 40 +++++++++---------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 6d51b63c49e..6df6f02b62c 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -76,7 +76,7 @@ import Test.Hydra.Tx.Gen ( genVerificationKey, ) import Test.Hydra.Tx.Mutation (addParticipationTokens) -import Test.QuickCheck (Property, Smart (..), choose, cover, elements, forAll, frequency, ioProperty, oneof, shuffle, sublistOf, (===)) +import Test.QuickCheck (Property, Smart (..), Testable, checkCoverage, choose, cover, elements, frequency, ioProperty, oneof, shuffle, sublistOf, (===)) import Test.QuickCheck.Monadic (monadic) import Test.QuickCheck.StateModel ( ActionWithPolarity (..), @@ -98,25 +98,23 @@ import Text.Show (Show (..)) spec :: Spec spec = do - prop "generates interesting transaction traces" prop_traces - prop "all valid transactions" prop_runActions prop "realWorldModelUTxO preserves addition" $ \u1 u2 -> realWorldModelUTxO (u1 <> u2) === (realWorldModelUTxO u1 <> realWorldModelUTxO u2) + prop "generates interesting transaction traces" $ \actions -> + checkCoverage $ coversInterestingActions actions True + prop "all valid transactions" prop_runActions -prop_traces :: Property -prop_traces = - forAll (arbitrary :: Gen (Actions Model)) $ \(Actions_ _ (Smart _ steps)) -> - -- FIXME: fix generators and minimums and re-enable coverage - -- checkCoverage $ - True - & cover 1 (null steps) "empty" - & cover 5 (hasDecrement steps) "has decrements" - & cover 1 (countContests steps >= 2) "has multiple contests" - & cover 5 (closeNonInitial steps) "close with non initial snapshots" - & cover 10 (hasFanout steps) "reach fanout" - & cover 0.5 (fanoutWithEmptyUTxO steps) "fanout with empty UTxO" - & cover 1 (fanoutWithSomeUTxO steps) "fanout with some UTxO" - & cover 0.5 (fanoutWithDelta steps) "fanout with additional UTxO to distribute" +coversInterestingActions :: Testable p => Actions Model -> p -> Property +coversInterestingActions (Actions_ _ (Smart _ steps)) p = + p + & cover 1 (null steps) "empty" + & cover 5 (hasDecrement steps) "has decrements" + & cover 1 (countContests steps >= 2) "has multiple contests" + & cover 5 (closeNonInitial steps) "close with non initial snapshots" + & cover 10 (hasFanout steps) "reach fanout" + & cover 0.5 (fanoutWithEmptyUTxO steps) "fanout with empty UTxO" + & cover 1 (fanoutWithSomeUTxO steps) "fanout with some UTxO" + & cover 0.5 (fanoutWithDelta steps) "fanout with additional UTxO to distribute" where hasUTxOToDecommit snapshot = not . null $ decommitUTxO snapshot @@ -173,9 +171,11 @@ prop_traces = prop_runActions :: Actions Model -> Property prop_runActions actions = - monadic runAppMProperty $ do - -- print actions - void (runActions actions) + coversInterestingActions actions + . monadic runAppMProperty + $ do + -- print actions + void (runActions actions) where runAppMProperty :: AppM Property -> Property runAppMProperty action = ioProperty $ do From 523e2a1cad4a442731abd1ba9bf7e2f9f016b405 Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Wed, 9 Oct 2024 08:55:59 +0200 Subject: [PATCH 02/21] Increase likelihood of closed state with deltaUTxO --- hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 6df6f02b62c..1e5890983df 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -294,7 +294,9 @@ instance StateModel Model where , do actor <- elements allActors snapshot <- genSnapshot - pure $ Some $ Close{actor, snapshot} + -- XXX: Too much randomness in genSnapshot + version <- elements [currentVersion, currentVersion + 1] + pure $ Some $ Close{actor, snapshot = snapshot{version}} ) ] <> [ ( 1 From 85405f34a4ff305fdfbb6bb60c9bde0f0bc4d37c Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Wed, 9 Oct 2024 08:56:31 +0200 Subject: [PATCH 03/21] Increase likelihood of multiple commits --- .../test/Hydra/Chain/Direct/TxTraceSpec.hs | 32 +++++++++++-------- 1 file changed, 19 insertions(+), 13 deletions(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 1e5890983df..33a9622efc6 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -309,20 +309,26 @@ instance StateModel Model where not (null utxoInHead) ] Closed{} -> - oneof $ - [ do - -- Fanout with the currently known model state. - pure $ - Some $ - Fanout - { utxo = utxoInHead - , deltaUTxO = pendingDecommitUTxO - } + frequency $ + [ + ( 1 + , do + -- Fanout with the currently known model state. + pure $ + Some $ + Fanout + { utxo = utxoInHead + , deltaUTxO = pendingDecommitUTxO + } + ) ] - <> [ do - actor <- elements allActors - snapshot <- genSnapshot - pure $ Some Contest{actor, snapshot} + <> [ + ( 10 + , do + actor <- elements allActors + snapshot <- genSnapshot + pure $ Some Contest{actor, snapshot} + ) ] Final -> pure $ Some Stop where From 495ae2e0a73f4776340f6db08d271e0964e92cc5 Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Wed, 9 Oct 2024 09:14:53 +0200 Subject: [PATCH 04/21] WIP: Draft a plan Changing the way we generate actions will help in guiding the generators based on "what an honest node would approve" and reduce discarded values / improve coverage. --- .../test/Hydra/Chain/Direct/TxTraceSpec.hs | 31 ++++++++++--------- 1 file changed, 16 insertions(+), 15 deletions(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 33a9622efc6..6025cd12dbe 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -5,15 +5,17 @@ -- chain modules. -- -- The model is focusing on transitions between Open and Closed states of the --- head right now. It generates plausible sequences of Decrement and Close --- actions, along with Contest and Fanout, each using a snapshot of some version --- and number. UTxOs are simplified such that their identity is A-E and value is --- just a number. --- --- Actions and snapshots are generated "just-in-time" and result in valid, but --- also deliberately invalid combinations of versions/numbers. Generated --- snapshots are correctly signed and consistent in what they decommit from the -- head. +-- +-- TODO: implement it this way +-- Given an initial UTxO, the model generates a plausible sequence of snapshots +-- that an honest node would approve. That is, the total balance of UTxO remains +-- constant and utxoToDecommit is only allowed to clear if the version is +-- incremented. All snapshots are correctly signed and UTxOs are simplified such +-- that their identity is A-E and value is just a number. +-- +-- From this sequence of valid snapshots, possible Decrement and Close actions +-- are generated, along with occasional Contest and consequential Fanout. module Hydra.Chain.Direct.TxTraceSpec where import Hydra.Prelude hiding (Any, State, label, show) @@ -252,18 +254,13 @@ data TxResult = TxResult } deriving (Eq, Show) -initialAmount :: Natural -initialAmount = 10 - -initialModelUTxO :: ModelUTxO -initialModelUTxO = fromList $ map (,initialAmount) [A, B, C, D, E] - balanceUTxOInHead :: Ord k => Map k Natural -> Map k Natural -> Map k Natural balanceUTxOInHead currentUtxoInHead someUTxOToDecrement = currentUtxoInHead `Map.difference` someUTxOToDecrement instance StateModel Model where data Action Model a where + ProduceSnapshots :: {snapshots :: [ModelSnapshot]} -> Action Model () Decrement :: {actor :: Actor, snapshot :: ModelSnapshot} -> Action Model TxResult Close :: {actor :: Actor, snapshot :: ModelSnapshot} -> Action Model TxResult Contest :: {actor :: Actor, snapshot :: ModelSnapshot} -> Action Model TxResult @@ -278,7 +275,7 @@ instance StateModel Model where , currentVersion = 0 , latestSnapshot = 0 , alreadyContested = [] - , utxoInHead = initialModelUTxO + , utxoInHead = fromList $ map (,10) [A, B, C] , pendingDecommitUTxO = Map.empty } @@ -542,6 +539,10 @@ instance MonadState UTxO AppM where type instance Realized AppM a = a +-- XXX: Most of the heavy-lifting here is similar to what +-- quickcheck-contractmodel does. We could consider using that package and +-- define a corresponding RunModel using our tx construction / evaluation hooks +-- only. instance RunModel Model AppM where perform Model{currentVersion} action _lookupVar = do case action of From a3f63dae1e238fe3203c8cbb4212f57cd2efd19b Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Thu, 10 Oct 2024 15:01:47 +0200 Subject: [PATCH 05/21] Switch to individual snapshot production while in Open state --- .../test/Hydra/Chain/Direct/TxTraceSpec.hs | 52 ++++++++++++------- 1 file changed, 33 insertions(+), 19 deletions(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 6025cd12dbe..1e17d75e4fb 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -110,6 +110,7 @@ coversInterestingActions :: Testable p => Actions Model -> p -> Property coversInterestingActions (Actions_ _ (Smart _ steps)) p = p & cover 1 (null steps) "empty" + & cover 50 (hasSomeSnapshots steps) "has some snapshots" & cover 5 (hasDecrement steps) "has decrements" & cover 1 (countContests steps >= 2) "has multiple contests" & cover 5 (closeNonInitial steps) "close with non initial snapshots" @@ -118,6 +119,13 @@ coversInterestingActions (Actions_ _ (Smart _ steps)) p = & cover 1 (fanoutWithSomeUTxO steps) "fanout with some UTxO" & cover 0.5 (fanoutWithDelta steps) "fanout with additional UTxO to distribute" where + hasSomeSnapshots = + any $ + \(_ := ActionWithPolarity{polarAction, polarity}) -> case polarAction of + NewSnapshot{} -> + polarity == PosPolarity + _ -> False + hasUTxOToDecommit snapshot = not . null $ decommitUTxO snapshot hasFanout = @@ -176,7 +184,7 @@ prop_runActions actions = coversInterestingActions actions . monadic runAppMProperty $ do - -- print actions + print actions void (runActions actions) where runAppMProperty :: AppM Property -> Property @@ -197,6 +205,7 @@ type ModelUTxO = Map SingleUTxO Natural data Model = Model { headState :: State + , knownSnapshots :: [ModelSnapshot] , currentVersion :: SnapshotVersion , latestSnapshot :: SnapshotNumber , alreadyContested :: [Actor] @@ -260,7 +269,7 @@ balanceUTxOInHead currentUtxoInHead someUTxOToDecrement = instance StateModel Model where data Action Model a where - ProduceSnapshots :: {snapshots :: [ModelSnapshot]} -> Action Model () + NewSnapshot :: {newSnapshot :: ModelSnapshot} -> Action Model () Decrement :: {actor :: Actor, snapshot :: ModelSnapshot} -> Action Model TxResult Close :: {actor :: Actor, snapshot :: ModelSnapshot} -> Action Model TxResult Contest :: {actor :: Actor, snapshot :: ModelSnapshot} -> Action Model TxResult @@ -272,6 +281,7 @@ instance StateModel Model where initialState = Model { headState = Open + , knownSnapshots = [] , currentVersion = 0 , latestSnapshot = 0 , alreadyContested = [] @@ -285,23 +295,19 @@ instance StateModel Model where arbitraryAction _lookup Model{headState, currentVersion, latestSnapshot, utxoInHead, pendingDecommitUTxO} = case headState of Open{} -> - frequency $ - [ - ( 1 - , do - actor <- elements allActors - snapshot <- genSnapshot - -- XXX: Too much randomness in genSnapshot - version <- elements [currentVersion, currentVersion + 1] - pure $ Some $ Close{actor, snapshot = snapshot{version}} - ) + oneof $ + [ Some . NewSnapshot <$> genSnapshot + , do + actor <- elements allActors + snapshot <- genSnapshot + -- XXX: Too much randomness in genSnapshot + version <- elements [currentVersion, currentVersion + 1] + pure $ Some $ Close{actor, snapshot = snapshot{version}} ] - <> [ ( 1 - , do - actor <- elements allActors - snapshot <- genSnapshot - pure $ Some Decrement{actor, snapshot} - ) + <> [ do + actor <- elements allActors + snapshot <- genSnapshot + pure $ Some Decrement{actor, snapshot} | -- We dont want to generate decrements if there is nothing in the head. not (null utxoInHead) ] @@ -329,6 +335,7 @@ instance StateModel Model where ] Final -> pure $ Some Stop where + -- TODO: Generate a snapshot an honest node would sign given the current model state. genSnapshot = do someUTxOToDecrement <- reduceValues =<< genSubModelOf utxoInHead let filteredSomeUTxOToDecrement = Map.filter (> 0) someUTxOToDecrement @@ -404,8 +411,11 @@ instance StateModel Model where -- Determine actions we want to perform and expect to work. If this is False, -- validFailingAction is checked too. precondition :: Model -> Action Model a -> Bool - precondition Model{headState, latestSnapshot, alreadyContested, utxoInHead, pendingDecommitUTxO, currentVersion} = \case + precondition Model{headState, knownSnapshots, latestSnapshot, alreadyContested, utxoInHead, pendingDecommitUTxO, currentVersion} = \case Stop -> headState /= Final + NewSnapshot{newSnapshot} -> + -- None of the produced snapshots is already known + newSnapshot `notElem` knownSnapshots Decrement{snapshot} -> headState == Open && snapshot.version == currentVersion @@ -448,6 +458,7 @@ instance StateModel Model where validFailingAction :: Model -> Action Model a -> Bool validFailingAction Model{headState, utxoInHead, currentVersion} = \case Stop -> False + NewSnapshot{} -> False -- Only filter non-matching states as we are not interested in these kind of -- verification failures. Decrement{snapshot} -> @@ -484,6 +495,8 @@ instance StateModel Model where nextState m@Model{currentVersion} t _result = case t of Stop -> m + NewSnapshot{newSnapshot} -> + m{knownSnapshots = m.knownSnapshots <> [newSnapshot]} Decrement{snapshot} -> m { headState = Open @@ -559,6 +572,7 @@ instance RunModel Model AppM where Fanout{utxo, deltaUTxO} -> do tx <- newFanoutTx Alice utxo deltaUTxO performTx tx + NewSnapshot{} -> pure () Stop -> pure () postcondition (modelBefore, modelAfter) action _lookup result = runPostconditionM' $ do From 7e7003b206dadb961f3babc2a47328f0f8d3bac0 Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Thu, 10 Oct 2024 15:10:56 +0200 Subject: [PATCH 06/21] Only use existing genSnapshot when producing new snapshots Otherwise we simpliy pick from the models knownSnapshots --- .../test/Hydra/Chain/Direct/TxTraceSpec.hs | 28 +++++++++---------- 1 file changed, 13 insertions(+), 15 deletions(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 1e17d75e4fb..32a2eda6a6c 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -292,24 +292,22 @@ instance StateModel Model where -- FIXME: 1.5k discards on 100 runs arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model)) - arbitraryAction _lookup Model{headState, currentVersion, latestSnapshot, utxoInHead, pendingDecommitUTxO} = + arbitraryAction _lookup Model{headState, knownSnapshots, currentVersion, latestSnapshot, utxoInHead, pendingDecommitUTxO} = case headState of Open{} -> oneof $ - [ Some . NewSnapshot <$> genSnapshot - , do - actor <- elements allActors - snapshot <- genSnapshot - -- XXX: Too much randomness in genSnapshot - version <- elements [currentVersion, currentVersion + 1] - pure $ Some $ Close{actor, snapshot = snapshot{version}} - ] + [Some . NewSnapshot <$> genSnapshot] <> [ do actor <- elements allActors - snapshot <- genSnapshot + snapshot <- elements knownSnapshots pure $ Some Decrement{actor, snapshot} - | -- We dont want to generate decrements if there is nothing in the head. - not (null utxoInHead) + | not (null knownSnapshots) -- XXX: DRY this check + ] + <> [ do + actor <- elements allActors + snapshot <- elements knownSnapshots + pure $ Some $ Close{actor, snapshot = snapshot} + | not (null knownSnapshots) ] Closed{} -> frequency $ @@ -325,13 +323,13 @@ instance StateModel Model where } ) ] - <> [ - ( 10 + <> [ ( 10 , do actor <- elements allActors - snapshot <- genSnapshot + snapshot <- elements knownSnapshots pure $ Some Contest{actor, snapshot} ) + | not (null knownSnapshots) ] Final -> pure $ Some Stop where From 20913ca5bd736931d53cf4c886eb31a69b9d0218 Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Thu, 10 Oct 2024 15:37:19 +0200 Subject: [PATCH 07/21] Only keep knownSnapshots and derive latest version / number from it --- .../test/Hydra/Chain/Direct/TxTraceSpec.hs | 90 ++++++++++--------- 1 file changed, 47 insertions(+), 43 deletions(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 32a2eda6a6c..9a0d6048135 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -25,6 +25,7 @@ import Cardano.Api.UTxO (UTxO) import Cardano.Api.UTxO qualified as UTxO import Cardano.Ledger.Coin (Coin (..)) import Data.Map.Strict qualified as Map +import Data.Sequence (Seq (..), (|>)) import Data.Time.Clock.POSIX (posixSecondsToUTCTime) import GHC.Natural (naturalFromInteger, naturalToInteger) import Hydra.Cardano.Api ( @@ -205,15 +206,21 @@ type ModelUTxO = Map SingleUTxO Natural data Model = Model { headState :: State - , knownSnapshots :: [ModelSnapshot] - , currentVersion :: SnapshotVersion - , latestSnapshot :: SnapshotNumber + , knownSnapshots :: Seq ModelSnapshot , alreadyContested :: [Actor] , utxoInHead :: ModelUTxO , pendingDecommitUTxO :: ModelUTxO } deriving (Show) +latestVersion :: Model -> SnapshotVersion +latestVersion Model{knownSnapshots = _ :|> r} = r.version +latestVersion _ = 0 + +latestSnapshotNumber :: Model -> SnapshotNumber +latestSnapshotNumber Model{knownSnapshots = _ :|> r} = r.number +latestSnapshotNumber _ = 0 + -- | Model of a real snapshot which contains a 'SnapshotNumber` but also our -- simplified form of 'UTxO'. data ModelSnapshot = ModelSnapshot @@ -281,9 +288,7 @@ instance StateModel Model where initialState = Model { headState = Open - , knownSnapshots = [] - , currentVersion = 0 - , latestSnapshot = 0 + , knownSnapshots = mempty , alreadyContested = [] , utxoInHead = fromList $ map (,10) [A, B, C] , pendingDecommitUTxO = Map.empty @@ -292,20 +297,20 @@ instance StateModel Model where -- FIXME: 1.5k discards on 100 runs arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model)) - arbitraryAction _lookup Model{headState, knownSnapshots, currentVersion, latestSnapshot, utxoInHead, pendingDecommitUTxO} = + arbitraryAction _lookup m@Model{headState, knownSnapshots, utxoInHead, pendingDecommitUTxO} = case headState of Open{} -> oneof $ [Some . NewSnapshot <$> genSnapshot] <> [ do actor <- elements allActors - snapshot <- elements knownSnapshots + snapshot <- elements $ toList knownSnapshots pure $ Some Decrement{actor, snapshot} | not (null knownSnapshots) -- XXX: DRY this check ] <> [ do actor <- elements allActors - snapshot <- elements knownSnapshots + snapshot <- elements $ toList knownSnapshots pure $ Some $ Close{actor, snapshot = snapshot} | not (null knownSnapshots) ] @@ -326,24 +331,26 @@ instance StateModel Model where <> [ ( 10 , do actor <- elements allActors - snapshot <- elements knownSnapshots + snapshot <- elements $ toList knownSnapshots pure $ Some Contest{actor, snapshot} ) | not (null knownSnapshots) ] Final -> pure $ Some Stop where - -- TODO: Generate a snapshot an honest node would sign given the current model state. + -- FIXME: Generate a snapshot an honest node would sign given the current model state. genSnapshot = do someUTxOToDecrement <- reduceValues =<< genSubModelOf utxoInHead let filteredSomeUTxOToDecrement = Map.filter (> 0) someUTxOToDecrement let balancedUTxOInHead = balanceUTxOInHead utxoInHead filteredSomeUTxOToDecrement - version <- elements $ currentVersion : [currentVersion - 1 | currentVersion > 0] <> [currentVersion + 1] + let v = latestVersion m + let sn = latestSnapshotNumber m + version <- elements $ v : [v - 1 | v > 0] <> [v + 1] let validSnapshot = ModelSnapshot { version - , number = latestSnapshot + , number = sn , snapshotUTxO = balancedUTxOInHead , decommitUTxO = filteredSomeUTxOToDecrement } @@ -354,10 +361,10 @@ instance StateModel Model where pure validSnapshot{snapshotUTxO = utxoInHead} , do -- old - let number' = if latestSnapshot == 0 then 0 else latestSnapshot - 1 + let number' = if sn == 0 then 0 else sn - 1 pure (validSnapshot :: ModelSnapshot){number = number'} , -- new - pure (validSnapshot :: ModelSnapshot){number = latestSnapshot + 1} + pure (validSnapshot :: ModelSnapshot){number = sn + 1} , do -- shuffled someUTxOToDecrement' <- shuffleValues filteredSomeUTxOToDecrement @@ -409,26 +416,28 @@ instance StateModel Model where -- Determine actions we want to perform and expect to work. If this is False, -- validFailingAction is checked too. precondition :: Model -> Action Model a -> Bool - precondition Model{headState, knownSnapshots, latestSnapshot, alreadyContested, utxoInHead, pendingDecommitUTxO, currentVersion} = \case + precondition m@Model{headState, knownSnapshots, alreadyContested, utxoInHead, pendingDecommitUTxO} = \case Stop -> headState /= Final NewSnapshot{newSnapshot} -> - -- None of the produced snapshots is already known - newSnapshot `notElem` knownSnapshots + trace ("precondition NewSnapshot: " <> show newSnapshot) $ + -- None of the produced snapshots is already known + newSnapshot `notElem` knownSnapshots Decrement{snapshot} -> - headState == Open - && snapshot.version == currentVersion - -- you are decrementing from existing utxo in the head - && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) - -- your tx is balanced with the utxo in the head - && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead - && (not . null $ decommitUTxO snapshot) + trace ("precondition Decrement: " <> show snapshot) $ + headState == Open + && snapshot.version == latestVersion m + -- you are decrementing from existing utxo in the head + && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) + -- your tx is balanced with the utxo in the head + && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead + && (not . null $ decommitUTxO snapshot) Close{snapshot} -> headState == Open && ( if snapshot.number == 0 then snapshotUTxO snapshot == initialUTxOInHead else - snapshot.number >= latestSnapshot - && snapshot.version `elem` (currentVersion : [currentVersion - 1 | currentVersion > 0]) + snapshot.number >= latestSnapshotNumber m + && snapshot.version `elem` (latestVersion m : [latestVersion m - 1 | latestVersion m > 0]) ) -- you are decrementing from existing utxo in the head && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) @@ -439,8 +448,8 @@ instance StateModel Model where Contest{actor, snapshot} -> headState == Closed && actor `notElem` alreadyContested - && snapshot.version `elem` (currentVersion : [currentVersion - 1 | currentVersion > 0]) - && snapshot.number > latestSnapshot + && snapshot.version `elem` (latestVersion m : [latestVersion m - 1 | latestVersion m > 0]) + && snapshot.number > latestSnapshotNumber m -- you are decrementing from existing utxo in the head && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) -- your tx is balanced with the utxo in the head @@ -454,14 +463,14 @@ instance StateModel Model where -- False, the action is discarded (e.g. it's invalid or we don't want to see -- it tried to perform). validFailingAction :: Model -> Action Model a -> Bool - validFailingAction Model{headState, utxoInHead, currentVersion} = \case + validFailingAction m@Model{headState, utxoInHead} = \case Stop -> False NewSnapshot{} -> False -- Only filter non-matching states as we are not interested in these kind of -- verification failures. Decrement{snapshot} -> headState == Open - && snapshot.version /= currentVersion + && snapshot.version /= latestVersion m -- Ignore unbalanced decrements. -- TODO: make them fail gracefully and test this? && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead @@ -472,7 +481,7 @@ instance StateModel Model where Close{snapshot} -> headState == Open && ( snapshot.number == 0 - || snapshot.version `elem` (currentVersion : [currentVersion - 1 | currentVersion > 0]) + || snapshot.version `elem` (latestVersion m : [latestVersion m - 1 | latestVersion m > 0]) ) -- Ignore unbalanced close. -- TODO: make them fail gracefully and test this? @@ -490,30 +499,25 @@ instance StateModel Model where headState == Closed nextState :: Model -> Action Model a -> Var a -> Model - nextState m@Model{currentVersion} t _result = + nextState m t _result = case t of Stop -> m NewSnapshot{newSnapshot} -> - m{knownSnapshots = m.knownSnapshots <> [newSnapshot]} + m{knownSnapshots = m.knownSnapshots :|> newSnapshot} Decrement{snapshot} -> m { headState = Open - , currentVersion = m.currentVersion + 1 - , latestSnapshot = snapshot.number , utxoInHead = balanceUTxOInHead (utxoInHead m) (decommitUTxO snapshot) } Close{snapshot} -> m { headState = Closed - , latestSnapshot = snapshot.number - , alreadyContested = [] , utxoInHead = snapshotUTxO snapshot - , pendingDecommitUTxO = if currentVersion == snapshot.version then decommitUTxO snapshot else mempty + , pendingDecommitUTxO = if latestVersion m == snapshot.version then decommitUTxO snapshot else mempty } Contest{actor, snapshot} -> m { headState = Closed - , latestSnapshot = snapshot.number , alreadyContested = actor : alreadyContested m , utxoInHead = snapshotUTxO snapshot , pendingDecommitUTxO = decommitUTxO snapshot @@ -555,17 +559,17 @@ type instance Realized AppM a = a -- define a corresponding RunModel using our tx construction / evaluation hooks -- only. instance RunModel Model AppM where - perform Model{currentVersion} action _lookupVar = do + perform m action _lookupVar = do case action of Decrement{actor, snapshot} -> do let (s, signatures) = signedSnapshot snapshot tx <- newDecrementTx actor ConfirmedSnapshot{snapshot = s, signatures} performTx tx Close{actor, snapshot} -> do - tx <- newCloseTx actor currentVersion (confirmedSnapshot snapshot) + tx <- newCloseTx actor (latestVersion m) (confirmedSnapshot snapshot) performTx tx Contest{actor, snapshot} -> do - tx <- newContestTx actor currentVersion (confirmedSnapshot snapshot) + tx <- newContestTx actor (latestVersion m) (confirmedSnapshot snapshot) performTx tx Fanout{utxo, deltaUTxO} -> do tx <- newFanoutTx Alice utxo deltaUTxO From bd42c460ede068038281c7bf2e6f3cc52be6939a Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Thu, 10 Oct 2024 15:53:56 +0200 Subject: [PATCH 08/21] Revert "Only keep knownSnapshots and derive latest version / number from it" This reverts commit b92f0515ebe07898de3ecd575ac047ebdaede15d. --- .../test/Hydra/Chain/Direct/TxTraceSpec.hs | 90 +++++++++---------- 1 file changed, 43 insertions(+), 47 deletions(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 9a0d6048135..32a2eda6a6c 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -25,7 +25,6 @@ import Cardano.Api.UTxO (UTxO) import Cardano.Api.UTxO qualified as UTxO import Cardano.Ledger.Coin (Coin (..)) import Data.Map.Strict qualified as Map -import Data.Sequence (Seq (..), (|>)) import Data.Time.Clock.POSIX (posixSecondsToUTCTime) import GHC.Natural (naturalFromInteger, naturalToInteger) import Hydra.Cardano.Api ( @@ -206,21 +205,15 @@ type ModelUTxO = Map SingleUTxO Natural data Model = Model { headState :: State - , knownSnapshots :: Seq ModelSnapshot + , knownSnapshots :: [ModelSnapshot] + , currentVersion :: SnapshotVersion + , latestSnapshot :: SnapshotNumber , alreadyContested :: [Actor] , utxoInHead :: ModelUTxO , pendingDecommitUTxO :: ModelUTxO } deriving (Show) -latestVersion :: Model -> SnapshotVersion -latestVersion Model{knownSnapshots = _ :|> r} = r.version -latestVersion _ = 0 - -latestSnapshotNumber :: Model -> SnapshotNumber -latestSnapshotNumber Model{knownSnapshots = _ :|> r} = r.number -latestSnapshotNumber _ = 0 - -- | Model of a real snapshot which contains a 'SnapshotNumber` but also our -- simplified form of 'UTxO'. data ModelSnapshot = ModelSnapshot @@ -288,7 +281,9 @@ instance StateModel Model where initialState = Model { headState = Open - , knownSnapshots = mempty + , knownSnapshots = [] + , currentVersion = 0 + , latestSnapshot = 0 , alreadyContested = [] , utxoInHead = fromList $ map (,10) [A, B, C] , pendingDecommitUTxO = Map.empty @@ -297,20 +292,20 @@ instance StateModel Model where -- FIXME: 1.5k discards on 100 runs arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model)) - arbitraryAction _lookup m@Model{headState, knownSnapshots, utxoInHead, pendingDecommitUTxO} = + arbitraryAction _lookup Model{headState, knownSnapshots, currentVersion, latestSnapshot, utxoInHead, pendingDecommitUTxO} = case headState of Open{} -> oneof $ [Some . NewSnapshot <$> genSnapshot] <> [ do actor <- elements allActors - snapshot <- elements $ toList knownSnapshots + snapshot <- elements knownSnapshots pure $ Some Decrement{actor, snapshot} | not (null knownSnapshots) -- XXX: DRY this check ] <> [ do actor <- elements allActors - snapshot <- elements $ toList knownSnapshots + snapshot <- elements knownSnapshots pure $ Some $ Close{actor, snapshot = snapshot} | not (null knownSnapshots) ] @@ -331,26 +326,24 @@ instance StateModel Model where <> [ ( 10 , do actor <- elements allActors - snapshot <- elements $ toList knownSnapshots + snapshot <- elements knownSnapshots pure $ Some Contest{actor, snapshot} ) | not (null knownSnapshots) ] Final -> pure $ Some Stop where - -- FIXME: Generate a snapshot an honest node would sign given the current model state. + -- TODO: Generate a snapshot an honest node would sign given the current model state. genSnapshot = do someUTxOToDecrement <- reduceValues =<< genSubModelOf utxoInHead let filteredSomeUTxOToDecrement = Map.filter (> 0) someUTxOToDecrement let balancedUTxOInHead = balanceUTxOInHead utxoInHead filteredSomeUTxOToDecrement - let v = latestVersion m - let sn = latestSnapshotNumber m - version <- elements $ v : [v - 1 | v > 0] <> [v + 1] + version <- elements $ currentVersion : [currentVersion - 1 | currentVersion > 0] <> [currentVersion + 1] let validSnapshot = ModelSnapshot { version - , number = sn + , number = latestSnapshot , snapshotUTxO = balancedUTxOInHead , decommitUTxO = filteredSomeUTxOToDecrement } @@ -361,10 +354,10 @@ instance StateModel Model where pure validSnapshot{snapshotUTxO = utxoInHead} , do -- old - let number' = if sn == 0 then 0 else sn - 1 + let number' = if latestSnapshot == 0 then 0 else latestSnapshot - 1 pure (validSnapshot :: ModelSnapshot){number = number'} , -- new - pure (validSnapshot :: ModelSnapshot){number = sn + 1} + pure (validSnapshot :: ModelSnapshot){number = latestSnapshot + 1} , do -- shuffled someUTxOToDecrement' <- shuffleValues filteredSomeUTxOToDecrement @@ -416,28 +409,26 @@ instance StateModel Model where -- Determine actions we want to perform and expect to work. If this is False, -- validFailingAction is checked too. precondition :: Model -> Action Model a -> Bool - precondition m@Model{headState, knownSnapshots, alreadyContested, utxoInHead, pendingDecommitUTxO} = \case + precondition Model{headState, knownSnapshots, latestSnapshot, alreadyContested, utxoInHead, pendingDecommitUTxO, currentVersion} = \case Stop -> headState /= Final NewSnapshot{newSnapshot} -> - trace ("precondition NewSnapshot: " <> show newSnapshot) $ - -- None of the produced snapshots is already known - newSnapshot `notElem` knownSnapshots + -- None of the produced snapshots is already known + newSnapshot `notElem` knownSnapshots Decrement{snapshot} -> - trace ("precondition Decrement: " <> show snapshot) $ - headState == Open - && snapshot.version == latestVersion m - -- you are decrementing from existing utxo in the head - && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) - -- your tx is balanced with the utxo in the head - && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead - && (not . null $ decommitUTxO snapshot) + headState == Open + && snapshot.version == currentVersion + -- you are decrementing from existing utxo in the head + && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) + -- your tx is balanced with the utxo in the head + && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead + && (not . null $ decommitUTxO snapshot) Close{snapshot} -> headState == Open && ( if snapshot.number == 0 then snapshotUTxO snapshot == initialUTxOInHead else - snapshot.number >= latestSnapshotNumber m - && snapshot.version `elem` (latestVersion m : [latestVersion m - 1 | latestVersion m > 0]) + snapshot.number >= latestSnapshot + && snapshot.version `elem` (currentVersion : [currentVersion - 1 | currentVersion > 0]) ) -- you are decrementing from existing utxo in the head && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) @@ -448,8 +439,8 @@ instance StateModel Model where Contest{actor, snapshot} -> headState == Closed && actor `notElem` alreadyContested - && snapshot.version `elem` (latestVersion m : [latestVersion m - 1 | latestVersion m > 0]) - && snapshot.number > latestSnapshotNumber m + && snapshot.version `elem` (currentVersion : [currentVersion - 1 | currentVersion > 0]) + && snapshot.number > latestSnapshot -- you are decrementing from existing utxo in the head && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) -- your tx is balanced with the utxo in the head @@ -463,14 +454,14 @@ instance StateModel Model where -- False, the action is discarded (e.g. it's invalid or we don't want to see -- it tried to perform). validFailingAction :: Model -> Action Model a -> Bool - validFailingAction m@Model{headState, utxoInHead} = \case + validFailingAction Model{headState, utxoInHead, currentVersion} = \case Stop -> False NewSnapshot{} -> False -- Only filter non-matching states as we are not interested in these kind of -- verification failures. Decrement{snapshot} -> headState == Open - && snapshot.version /= latestVersion m + && snapshot.version /= currentVersion -- Ignore unbalanced decrements. -- TODO: make them fail gracefully and test this? && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead @@ -481,7 +472,7 @@ instance StateModel Model where Close{snapshot} -> headState == Open && ( snapshot.number == 0 - || snapshot.version `elem` (latestVersion m : [latestVersion m - 1 | latestVersion m > 0]) + || snapshot.version `elem` (currentVersion : [currentVersion - 1 | currentVersion > 0]) ) -- Ignore unbalanced close. -- TODO: make them fail gracefully and test this? @@ -499,25 +490,30 @@ instance StateModel Model where headState == Closed nextState :: Model -> Action Model a -> Var a -> Model - nextState m t _result = + nextState m@Model{currentVersion} t _result = case t of Stop -> m NewSnapshot{newSnapshot} -> - m{knownSnapshots = m.knownSnapshots :|> newSnapshot} + m{knownSnapshots = m.knownSnapshots <> [newSnapshot]} Decrement{snapshot} -> m { headState = Open + , currentVersion = m.currentVersion + 1 + , latestSnapshot = snapshot.number , utxoInHead = balanceUTxOInHead (utxoInHead m) (decommitUTxO snapshot) } Close{snapshot} -> m { headState = Closed + , latestSnapshot = snapshot.number + , alreadyContested = [] , utxoInHead = snapshotUTxO snapshot - , pendingDecommitUTxO = if latestVersion m == snapshot.version then decommitUTxO snapshot else mempty + , pendingDecommitUTxO = if currentVersion == snapshot.version then decommitUTxO snapshot else mempty } Contest{actor, snapshot} -> m { headState = Closed + , latestSnapshot = snapshot.number , alreadyContested = actor : alreadyContested m , utxoInHead = snapshotUTxO snapshot , pendingDecommitUTxO = decommitUTxO snapshot @@ -559,17 +555,17 @@ type instance Realized AppM a = a -- define a corresponding RunModel using our tx construction / evaluation hooks -- only. instance RunModel Model AppM where - perform m action _lookupVar = do + perform Model{currentVersion} action _lookupVar = do case action of Decrement{actor, snapshot} -> do let (s, signatures) = signedSnapshot snapshot tx <- newDecrementTx actor ConfirmedSnapshot{snapshot = s, signatures} performTx tx Close{actor, snapshot} -> do - tx <- newCloseTx actor (latestVersion m) (confirmedSnapshot snapshot) + tx <- newCloseTx actor currentVersion (confirmedSnapshot snapshot) performTx tx Contest{actor, snapshot} -> do - tx <- newContestTx actor (latestVersion m) (confirmedSnapshot snapshot) + tx <- newContestTx actor currentVersion (confirmedSnapshot snapshot) performTx tx Fanout{utxo, deltaUTxO} -> do tx <- newFanoutTx Alice utxo deltaUTxO From 31b614f53dd769ebddf0af5325b2c910e80736d7 Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Thu, 10 Oct 2024 16:06:04 +0200 Subject: [PATCH 09/21] Generate plausible sequences of snapshots (version and number) --- .../test/Hydra/Chain/Direct/TxTraceSpec.hs | 101 +++++++++--------- 1 file changed, 53 insertions(+), 48 deletions(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 32a2eda6a6c..290df2f7ae4 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -206,14 +206,20 @@ type ModelUTxO = Map SingleUTxO Natural data Model = Model { headState :: State , knownSnapshots :: [ModelSnapshot] + -- ^ List of off-chain snapshots, from most recent to oldest. , currentVersion :: SnapshotVersion - , latestSnapshot :: SnapshotNumber + , closedSnapshotNumber :: SnapshotNumber , alreadyContested :: [Actor] , utxoInHead :: ModelUTxO , pendingDecommitUTxO :: ModelUTxO } deriving (Show) +latestSnapshotNumber :: [ModelSnapshot] -> SnapshotNumber +latestSnapshotNumber = \case + (s : _) -> s.number + _ -> 0 + -- | Model of a real snapshot which contains a 'SnapshotNumber` but also our -- simplified form of 'UTxO'. data ModelSnapshot = ModelSnapshot @@ -283,7 +289,7 @@ instance StateModel Model where { headState = Open , knownSnapshots = [] , currentVersion = 0 - , latestSnapshot = 0 + , closedSnapshotNumber = 0 , alreadyContested = [] , utxoInHead = fromList $ map (,10) [A, B, C] , pendingDecommitUTxO = Map.empty @@ -292,7 +298,7 @@ instance StateModel Model where -- FIXME: 1.5k discards on 100 runs arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model)) - arbitraryAction _lookup Model{headState, knownSnapshots, currentVersion, latestSnapshot, utxoInHead, pendingDecommitUTxO} = + arbitraryAction _lookup Model{headState, knownSnapshots, currentVersion, utxoInHead, pendingDecommitUTxO} = case headState of Open{} -> oneof $ @@ -339,46 +345,47 @@ instance StateModel Model where let filteredSomeUTxOToDecrement = Map.filter (> 0) someUTxOToDecrement let balancedUTxOInHead = balanceUTxOInHead utxoInHead filteredSomeUTxOToDecrement - version <- elements $ currentVersion : [currentVersion - 1 | currentVersion > 0] <> [currentVersion + 1] let validSnapshot = ModelSnapshot - { version - , number = latestSnapshot + { version = currentVersion + , number = latestSnapshotNumber knownSnapshots + 1 , snapshotUTxO = balancedUTxOInHead , decommitUTxO = filteredSomeUTxOToDecrement } - oneof - [ -- valid - pure validSnapshot - , -- unbalanced - pure validSnapshot{snapshotUTxO = utxoInHead} - , do - -- old - let number' = if latestSnapshot == 0 then 0 else latestSnapshot - 1 - pure (validSnapshot :: ModelSnapshot){number = number'} - , -- new - pure (validSnapshot :: ModelSnapshot){number = latestSnapshot + 1} - , do - -- shuffled - someUTxOToDecrement' <- shuffleValues filteredSomeUTxOToDecrement - pure validSnapshot{decommitUTxO = someUTxOToDecrement'} - , do - -- more in head - utxoInHead' <- increaseValues utxoInHead - pure validSnapshot{snapshotUTxO = utxoInHead'} - , do - -- more in decommit - someUTxOToDecrement' <- increaseValues =<< genSubModelOf utxoInHead - let balancedUTxOInHead' = balanceUTxOInHead utxoInHead someUTxOToDecrement' - pure - validSnapshot - { snapshotUTxO = balancedUTxOInHead' - , decommitUTxO = someUTxOToDecrement' - } - , -- decommit all - pure validSnapshot{snapshotUTxO = mempty, decommitUTxO = utxoInHead} - , arbitrary - ] + -- TODO: check whether these cases are met + -- oneof + -- [ -- valid + -- pure validSnapshot + -- , -- unbalanced + -- pure validSnapshot{snapshotUTxO = utxoInHead} + -- , do + -- -- old + -- let number' = if closedSnapshotNumber == 0 then 0 else closedSnapshotNumber - 1 + -- pure (validSnapshot :: ModelSnapshot){number = number'} + -- , -- new + -- pure (validSnapshot :: ModelSnapshot){number = closedSnapshotNumber + 1} + -- , do + -- -- shuffled + -- someUTxOToDecrement' <- shuffleValues filteredSomeUTxOToDecrement + -- pure validSnapshot{decommitUTxO = someUTxOToDecrement'} + -- , do + -- -- more in head + -- utxoInHead' <- increaseValues utxoInHead + -- pure validSnapshot{snapshotUTxO = utxoInHead'} + -- , do + -- -- more in decommit + -- someUTxOToDecrement' <- increaseValues =<< genSubModelOf utxoInHead + -- let balancedUTxOInHead' = balanceUTxOInHead utxoInHead someUTxOToDecrement' + -- pure + -- validSnapshot + -- { snapshotUTxO = balancedUTxOInHead' + -- , decommitUTxO = someUTxOToDecrement' + -- } + -- , -- decommit all + -- pure validSnapshot{snapshotUTxO = mempty, decommitUTxO = utxoInHead} + -- , arbitrary + -- ] + pure validSnapshot genSubModelOf :: ModelUTxO -> Gen ModelUTxO genSubModelOf model = do @@ -409,11 +416,11 @@ instance StateModel Model where -- Determine actions we want to perform and expect to work. If this is False, -- validFailingAction is checked too. precondition :: Model -> Action Model a -> Bool - precondition Model{headState, knownSnapshots, latestSnapshot, alreadyContested, utxoInHead, pendingDecommitUTxO, currentVersion} = \case + precondition Model{headState, knownSnapshots, closedSnapshotNumber, alreadyContested, utxoInHead, pendingDecommitUTxO, currentVersion} = \case Stop -> headState /= Final NewSnapshot{newSnapshot} -> - -- None of the produced snapshots is already known - newSnapshot `notElem` knownSnapshots + newSnapshot.version == currentVersion + && newSnapshot.number > latestSnapshotNumber knownSnapshots Decrement{snapshot} -> headState == Open && snapshot.version == currentVersion @@ -427,8 +434,7 @@ instance StateModel Model where && ( if snapshot.number == 0 then snapshotUTxO snapshot == initialUTxOInHead else - snapshot.number >= latestSnapshot - && snapshot.version `elem` (currentVersion : [currentVersion - 1 | currentVersion > 0]) + snapshot.version `elem` (currentVersion : [currentVersion - 1 | currentVersion > 0]) ) -- you are decrementing from existing utxo in the head && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) @@ -440,7 +446,7 @@ instance StateModel Model where headState == Closed && actor `notElem` alreadyContested && snapshot.version `elem` (currentVersion : [currentVersion - 1 | currentVersion > 0]) - && snapshot.number > latestSnapshot + && snapshot.number > closedSnapshotNumber -- you are decrementing from existing utxo in the head && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) -- your tx is balanced with the utxo in the head @@ -494,18 +500,17 @@ instance StateModel Model where case t of Stop -> m NewSnapshot{newSnapshot} -> - m{knownSnapshots = m.knownSnapshots <> [newSnapshot]} + m{knownSnapshots = newSnapshot : m.knownSnapshots} Decrement{snapshot} -> m { headState = Open , currentVersion = m.currentVersion + 1 - , latestSnapshot = snapshot.number , utxoInHead = balanceUTxOInHead (utxoInHead m) (decommitUTxO snapshot) } Close{snapshot} -> m { headState = Closed - , latestSnapshot = snapshot.number + , closedSnapshotNumber = snapshot.number , alreadyContested = [] , utxoInHead = snapshotUTxO snapshot , pendingDecommitUTxO = if currentVersion == snapshot.version then decommitUTxO snapshot else mempty @@ -513,7 +518,7 @@ instance StateModel Model where Contest{actor, snapshot} -> m { headState = Closed - , latestSnapshot = snapshot.number + , closedSnapshotNumber = snapshot.number , alreadyContested = actor : alreadyContested m , utxoInHead = snapshotUTxO snapshot , pendingDecommitUTxO = decommitUTxO snapshot From 8b03153ce08756a15c9f2b614633033822a88e5d Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Thu, 10 Oct 2024 16:10:52 +0200 Subject: [PATCH 10/21] Allow for decrement with empty utxo to decommit The decrement validator allows for this and consequently this is a possible scenario: An adversary can construct decrement transactions with any snapshot we signed. --- hydra-node/src/Hydra/Chain/Direct/State.hs | 11 +---------- hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs | 3 --- 2 files changed, 1 insertion(+), 13 deletions(-) diff --git a/hydra-node/src/Hydra/Chain/Direct/State.hs b/hydra-node/src/Hydra/Chain/Direct/State.hs index 4b8bf147cb7..06c84645982 100644 --- a/hydra-node/src/Hydra/Chain/Direct/State.hs +++ b/hydra-node/src/Hydra/Chain/Direct/State.hs @@ -554,19 +554,10 @@ decrement ctx spendableUTxO headId headParameters decrementingSnapshot = do pid <- headIdToPolicyId headId ?> InvalidHeadIdInDecrement{headId} let utxoOfThisHead' = utxoOfThisHead pid spendableUTxO headUTxO <- UTxO.find (isScriptTxOut headScript) utxoOfThisHead' ?> CannotFindHeadOutputInDecrement - case utxoToDecommit of - Nothing -> - Left SnapshotMissingDecrementUTxO - Just decrementUTxO - | null decrementUTxO -> - Left SnapshotDecrementUTxOIsNull - _ -> - Right $ decrementTx scriptRegistry ownVerificationKey headId headParameters headUTxO sn sigs + Right $ decrementTx scriptRegistry ownVerificationKey headId headParameters headUTxO sn sigs where headScript = fromPlutusScript @PlutusScriptV2 Head.validatorScript - Snapshot{utxoToDecommit} = sn - (sn, sigs) = case decrementingSnapshot of ConfirmedSnapshot{snapshot, signatures} -> (snapshot, signatures) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 290df2f7ae4..2ce1aeac871 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -428,7 +428,6 @@ instance StateModel Model where && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) -- your tx is balanced with the utxo in the head && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead - && (not . null $ decommitUTxO snapshot) Close{snapshot} -> headState == Open && ( if snapshot.number == 0 @@ -473,8 +472,6 @@ instance StateModel Model where && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead -- Ignore decrements that work with non existing utxo in the head && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) - -- Ignore decrement without something to decommit - && (not . null $ decommitUTxO snapshot) Close{snapshot} -> headState == Open && ( snapshot.number == 0 From 9c6da4197de7784e9bdb99a7cc35a9c2c4706136 Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Thu, 10 Oct 2024 17:21:27 +0200 Subject: [PATCH 11/21] Generate Nothing if realWorldModelUTxO is empty This is more consistent with what the off-chain code does. --- .../test/Hydra/Chain/Direct/TxTraceSpec.hs | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 2ce1aeac871..8ad141da2ab 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -667,13 +667,6 @@ getValidationError tx utxo = allActors :: [Actor] allActors = [Alice, Bob, Carol] --- | A "random" UTxO distribution for a given 'ModelSnapshot'. -generateUTxOFromModelSnapshot :: ModelSnapshot -> (UTxO, UTxO) -generateUTxOFromModelSnapshot snapshot = - ( realWorldModelUTxO (snapshotUTxO snapshot) - , realWorldModelUTxO (decommitUTxO snapshot) - ) - -- | Map a 'ModelUTxO' to a real-world 'UTxO'. realWorldModelUTxO :: ModelUTxO -> UTxO realWorldModelUTxO = @@ -691,7 +684,6 @@ signedSnapshot :: ModelSnapshot -> (Snapshot Tx, MultiSignature (Snapshot Tx)) signedSnapshot ms = (snapshot, signatures) where - (utxo, toDecommit) = generateUTxOFromModelSnapshot ms snapshot = Snapshot { headId = mkHeadId Fixture.testPolicyId @@ -700,11 +692,17 @@ signedSnapshot ms = , confirmed = [] , utxo , utxoToCommit = Nothing - , utxoToDecommit = Just toDecommit + , utxoToDecommit } signatures = aggregate [sign sk snapshot | sk <- [Fixture.aliceSk, Fixture.bobSk, Fixture.carolSk]] + utxo = realWorldModelUTxO (snapshotUTxO ms) + + utxoToDecommit = + let u = realWorldModelUTxO (decommitUTxO ms) + in if null u then Nothing else Just u + -- | A confirmed snapshot (either initial or later confirmed), based onTxTra -- 'signedSnapshot'. confirmedSnapshot :: ModelSnapshot -> ConfirmedSnapshot Tx @@ -715,7 +713,7 @@ confirmedSnapshot modelSnapshot@ModelSnapshot{number} = { -- -- NOTE: The close validator would not check headId on close with -- initial snapshot, but we need to provide it still. headId = mkHeadId Fixture.testPolicyId - , initialUTxO = fst $ generateUTxOFromModelSnapshot modelSnapshot + , initialUTxO = realWorldModelUTxO $ snapshotUTxO modelSnapshot } _ -> ConfirmedSnapshot{snapshot, signatures} where From 1280f85c7b2746e2521ff3a05e0277b81d095277 Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Thu, 10 Oct 2024 17:32:22 +0200 Subject: [PATCH 12/21] Not shrink relevant NewSnapshots away --- hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 8ad141da2ab..fd02099f19b 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -423,6 +423,7 @@ instance StateModel Model where && newSnapshot.number > latestSnapshotNumber knownSnapshots Decrement{snapshot} -> headState == Open + && snapshot `elem` knownSnapshots && snapshot.version == currentVersion -- you are decrementing from existing utxo in the head && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) @@ -430,6 +431,7 @@ instance StateModel Model where && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead Close{snapshot} -> headState == Open + && snapshot `elem` knownSnapshots && ( if snapshot.number == 0 then snapshotUTxO snapshot == initialUTxOInHead else @@ -443,6 +445,7 @@ instance StateModel Model where Model{utxoInHead = initialUTxOInHead} = initialState Contest{actor, snapshot} -> headState == Closed + && snapshot `elem` knownSnapshots && actor `notElem` alreadyContested && snapshot.version `elem` (currentVersion : [currentVersion - 1 | currentVersion > 0]) && snapshot.number > closedSnapshotNumber @@ -459,13 +462,14 @@ instance StateModel Model where -- False, the action is discarded (e.g. it's invalid or we don't want to see -- it tried to perform). validFailingAction :: Model -> Action Model a -> Bool - validFailingAction Model{headState, utxoInHead, currentVersion} = \case + validFailingAction Model{headState, knownSnapshots, utxoInHead, currentVersion} = \case Stop -> False NewSnapshot{} -> False -- Only filter non-matching states as we are not interested in these kind of -- verification failures. Decrement{snapshot} -> headState == Open + && snapshot `elem` knownSnapshots && snapshot.version /= currentVersion -- Ignore unbalanced decrements. -- TODO: make them fail gracefully and test this? @@ -474,6 +478,7 @@ instance StateModel Model where && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) Close{snapshot} -> headState == Open + && snapshot `elem` knownSnapshots && ( snapshot.number == 0 || snapshot.version `elem` (currentVersion : [currentVersion - 1 | currentVersion > 0]) ) @@ -484,6 +489,7 @@ instance StateModel Model where && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) Contest{snapshot} -> headState == Closed + && snapshot `elem` knownSnapshots -- Ignore unbalanced close. -- TODO: make them fail gracefully and test this? && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead @@ -599,8 +605,6 @@ instance RunModel Model AppM where -- exactly. let sorted = sortOn (\o -> (txOutAddress o, selectLovelace (txOutValue o))) . toList let fannedOut = utxoFromTx tx - -- counterexamplePost ("Fanned out UTxO does not match: " <> renderUTxO fannedOut) - -- counterexamplePost ("SnapshotUTxO: " <> renderUTxO (snapshotUTxO snapshot)) guard $ sorted fannedOut == sorted (realWorldModelUTxO utxo <> realWorldModelUTxO deltaUTxO) expectValid result $ \case From 272268bab7a66d9c2292591775d2525058e36d5b Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Thu, 10 Oct 2024 17:41:26 +0200 Subject: [PATCH 13/21] Only update pendingDecommitUTxO in contest if not outdated --- hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index fd02099f19b..c7d68e7b912 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -509,6 +509,7 @@ instance StateModel Model where { headState = Open , currentVersion = m.currentVersion + 1 , utxoInHead = balanceUTxOInHead (utxoInHead m) (decommitUTxO snapshot) + -- TODO: why is this not needed?, pendingDecommitUTxO = m.pendingDecommitUTxO \\ snapshot.snapshotUTxO } Close{snapshot} -> m @@ -524,7 +525,7 @@ instance StateModel Model where , closedSnapshotNumber = snapshot.number , alreadyContested = actor : alreadyContested m , utxoInHead = snapshotUTxO snapshot - , pendingDecommitUTxO = decommitUTxO snapshot + , pendingDecommitUTxO = if currentVersion == snapshot.version then decommitUTxO snapshot else mempty } Fanout{} -> m{headState = Final} From 3d6ae8f69a59dd8d4d28edcca11cf63f62741b7d Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Thu, 10 Oct 2024 18:08:29 +0200 Subject: [PATCH 14/21] Make negative decrements fail gracefully Also disables some preconditions to decide whether we want to test this. --- hydra-node/src/Hydra/Chain/Direct/State.hs | 12 +++++-- .../test/Hydra/Chain/Direct/TxTraceSpec.hs | 31 +++++++++---------- 2 files changed, 25 insertions(+), 18 deletions(-) diff --git a/hydra-node/src/Hydra/Chain/Direct/State.hs b/hydra-node/src/Hydra/Chain/Direct/State.hs index 06c84645982..796d35b2693 100644 --- a/hydra-node/src/Hydra/Chain/Direct/State.hs +++ b/hydra-node/src/Hydra/Chain/Direct/State.hs @@ -45,6 +45,7 @@ import Hydra.Cardano.Api ( getTxId, isScriptTxOut, modifyTxOutValue, + negateValue, networkIdToNetwork, selectAsset, selectLovelace, @@ -535,7 +536,7 @@ increment ctx spendableUTxO headId headParameters incrementingSnapshot depositTx data DecrementTxError = InvalidHeadIdInDecrement {headId :: HeadId} | CannotFindHeadOutputInDecrement - | SnapshotMissingDecrementUTxO + | DecrementValueNegative | SnapshotDecrementUTxOIsNull deriving stock (Show) @@ -553,11 +554,18 @@ decrement :: decrement ctx spendableUTxO headId headParameters decrementingSnapshot = do pid <- headIdToPolicyId headId ?> InvalidHeadIdInDecrement{headId} let utxoOfThisHead' = utxoOfThisHead pid spendableUTxO - headUTxO <- UTxO.find (isScriptTxOut headScript) utxoOfThisHead' ?> CannotFindHeadOutputInDecrement + headUTxO@(_, headOut) <- UTxO.find (isScriptTxOut headScript) utxoOfThisHead' ?> CannotFindHeadOutputInDecrement + let balance = txOutValue headOut <> negateValue decommitValue + when (isNegative balance) $ + Left DecrementValueNegative Right $ decrementTx scriptRegistry ownVerificationKey headId headParameters headUTxO sn sigs where headScript = fromPlutusScript @PlutusScriptV2 Head.validatorScript + decommitValue = foldMap txOutValue $ fromMaybe mempty $ utxoToDecommit sn + + isNegative = any ((< 0) . snd) . IsList.toList + (sn, sigs) = case decrementingSnapshot of ConfirmedSnapshot{snapshot, signatures} -> (snapshot, signatures) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index c7d68e7b912..b878c9e268b 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -341,7 +341,7 @@ instance StateModel Model where where -- TODO: Generate a snapshot an honest node would sign given the current model state. genSnapshot = do - someUTxOToDecrement <- reduceValues =<< genSubModelOf utxoInHead + someUTxOToDecrement <- reduceValues =<< submapOf utxoInHead let filteredSomeUTxOToDecrement = Map.filter (> 0) someUTxOToDecrement let balancedUTxOInHead = balanceUTxOInHead utxoInHead filteredSomeUTxOToDecrement @@ -352,7 +352,7 @@ instance StateModel Model where , snapshotUTxO = balancedUTxOInHead , decommitUTxO = filteredSomeUTxOToDecrement } - -- TODO: check whether these cases are met + -- FIXME: check whether these cases are met -- oneof -- [ -- valid -- pure validSnapshot @@ -374,7 +374,7 @@ instance StateModel Model where -- pure validSnapshot{snapshotUTxO = utxoInHead'} -- , do -- -- more in decommit - -- someUTxOToDecrement' <- increaseValues =<< genSubModelOf utxoInHead + -- someUTxOToDecrement' <- increaseValues =<< submapOf utxoInHead -- let balancedUTxOInHead' = balanceUTxOInHead utxoInHead someUTxOToDecrement' -- pure -- validSnapshot @@ -387,8 +387,8 @@ instance StateModel Model where -- ] pure validSnapshot - genSubModelOf :: ModelUTxO -> Gen ModelUTxO - genSubModelOf model = do + submapOf :: Ord k => Map k v -> Gen (Map k v) + submapOf model = do subset <- sublistOf (Map.toList model) return $ Map.fromList subset @@ -425,10 +425,10 @@ instance StateModel Model where headState == Open && snapshot `elem` knownSnapshots && snapshot.version == currentVersion - -- you are decrementing from existing utxo in the head - && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) - -- your tx is balanced with the utxo in the head - && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead + -- you are decrementing from existing utxo in the head + -- && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) + -- your tx is balanced with the utxo in the head + -- && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead Close{snapshot} -> headState == Open && snapshot `elem` knownSnapshots @@ -471,11 +471,11 @@ instance StateModel Model where headState == Open && snapshot `elem` knownSnapshots && snapshot.version /= currentVersion - -- Ignore unbalanced decrements. - -- TODO: make them fail gracefully and test this? - && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead - -- Ignore decrements that work with non existing utxo in the head - && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) + -- Ignore unbalanced decrements. + -- TODO: make them fail gracefully and test this? + -- && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead + -- Ignore decrements that work with non existing utxo in the head + -- && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) Close{snapshot} -> headState == Open && snapshot `elem` knownSnapshots @@ -567,8 +567,7 @@ instance RunModel Model AppM where perform Model{currentVersion} action _lookupVar = do case action of Decrement{actor, snapshot} -> do - let (s, signatures) = signedSnapshot snapshot - tx <- newDecrementTx actor ConfirmedSnapshot{snapshot = s, signatures} + tx <- newDecrementTx actor (confirmedSnapshot snapshot) performTx tx Close{actor, snapshot} -> do tx <- newCloseTx actor currentVersion (confirmedSnapshot snapshot) From f8312ae2409491a8a72f2a3f751552363a6f1b33 Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Thu, 10 Oct 2024 18:41:15 +0200 Subject: [PATCH 15/21] Fix excessive discarding by generating better snapshots This also makes the output easier to read and removes several preconditions as we now expect construction to fail if we try to decrement too much. --- .../test/Hydra/Chain/Direct/TxTraceSpec.hs | 126 ++++++------------ 1 file changed, 41 insertions(+), 85 deletions(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index b878c9e268b..85f1e7f1de7 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -7,7 +7,6 @@ -- The model is focusing on transitions between Open and Closed states of the -- head. -- --- TODO: implement it this way -- Given an initial UTxO, the model generates a plausible sequence of snapshots -- that an honest node would approve. That is, the total balance of UTxO remains -- constant and utxoToDecommit is only allowed to clear if the version is @@ -24,6 +23,7 @@ import Test.Hydra.Prelude import Cardano.Api.UTxO (UTxO) import Cardano.Api.UTxO qualified as UTxO import Cardano.Ledger.Coin (Coin (..)) +import Data.Map (differenceWith) import Data.Map.Strict qualified as Map import Data.Time.Clock.POSIX (posixSecondsToUTCTime) import GHC.Natural (naturalFromInteger, naturalToInteger) @@ -78,7 +78,7 @@ import Test.Hydra.Tx.Gen ( genVerificationKey, ) import Test.Hydra.Tx.Mutation (addParticipationTokens) -import Test.QuickCheck (Property, Smart (..), Testable, checkCoverage, choose, cover, elements, frequency, ioProperty, oneof, shuffle, sublistOf, (===)) +import Test.QuickCheck (Property, Smart (..), Testable, checkCoverage, choose, cover, elements, frequency, ioProperty, oneof, sublistOf, (===)) import Test.QuickCheck.Monadic (monadic) import Test.QuickCheck.StateModel ( ActionWithPolarity (..), @@ -126,7 +126,7 @@ coversInterestingActions (Actions_ _ (Smart _ steps)) p = polarity == PosPolarity _ -> False - hasUTxOToDecommit snapshot = not . null $ decommitUTxO snapshot + hasUTxOToDecommit snapshot = not . null $ toDecommit snapshot hasFanout = any $ @@ -203,6 +203,11 @@ instance Arbitrary SingleUTxO where type ModelUTxO = Map SingleUTxO Natural +-- | Reduce left hand side by right hand side. +remove :: ModelUTxO -> ModelUTxO -> ModelUTxO +remove = + differenceWith $ \a b -> if a > b then Just $ a - b else Nothing + data Model = Model { headState :: State , knownSnapshots :: [ModelSnapshot] @@ -225,8 +230,8 @@ latestSnapshotNumber = \case data ModelSnapshot = ModelSnapshot { version :: SnapshotVersion , number :: SnapshotNumber - , snapshotUTxO :: ModelUTxO - , decommitUTxO :: ModelUTxO + , inHead :: ModelUTxO + , toDecommit :: ModelUTxO } deriving (Show, Eq, Ord, Generic) @@ -240,8 +245,8 @@ instance Num ModelSnapshot where ModelSnapshot { version = UnsafeSnapshotVersion 0 , number = UnsafeSnapshotNumber $ fromMaybe 0 $ integerToNatural x - , snapshotUTxO = mempty - , decommitUTxO = mempty + , inHead = mempty + , toDecommit = mempty } instance Arbitrary ModelSnapshot where @@ -269,10 +274,6 @@ data TxResult = TxResult } deriving (Eq, Show) -balanceUTxOInHead :: Ord k => Map k Natural -> Map k Natural -> Map k Natural -balanceUTxOInHead currentUtxoInHead someUTxOToDecrement = - currentUtxoInHead `Map.difference` someUTxOToDecrement - instance StateModel Model where data Action Model a where NewSnapshot :: {newSnapshot :: ModelSnapshot} -> Action Model () @@ -295,8 +296,6 @@ instance StateModel Model where , pendingDecommitUTxO = Map.empty } - -- FIXME: 1.5k discards on 100 runs - arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model)) arbitraryAction _lookup Model{headState, knownSnapshots, currentVersion, utxoInHead, pendingDecommitUTxO} = case headState of @@ -341,23 +340,20 @@ instance StateModel Model where where -- TODO: Generate a snapshot an honest node would sign given the current model state. genSnapshot = do - someUTxOToDecrement <- reduceValues =<< submapOf utxoInHead - let filteredSomeUTxOToDecrement = Map.filter (> 0) someUTxOToDecrement - let balancedUTxOInHead = balanceUTxOInHead utxoInHead filteredSomeUTxOToDecrement - + toDecommit <- reduceValues =<< submapOf utxoInHead let validSnapshot = ModelSnapshot { version = currentVersion , number = latestSnapshotNumber knownSnapshots + 1 - , snapshotUTxO = balancedUTxOInHead - , decommitUTxO = filteredSomeUTxOToDecrement + , inHead = utxoInHead `remove` toDecommit + , toDecommit } -- FIXME: check whether these cases are met -- oneof -- [ -- valid -- pure validSnapshot -- , -- unbalanced - -- pure validSnapshot{snapshotUTxO = utxoInHead} + -- pure validSnapshot{inHead = utxoInHead} -- , do -- -- old -- let number' = if closedSnapshotNumber == 0 then 0 else closedSnapshotNumber - 1 @@ -367,22 +363,22 @@ instance StateModel Model where -- , do -- -- shuffled -- someUTxOToDecrement' <- shuffleValues filteredSomeUTxOToDecrement - -- pure validSnapshot{decommitUTxO = someUTxOToDecrement'} + -- pure validSnapshot{toDecommit = someUTxOToDecrement'} -- , do -- -- more in head -- utxoInHead' <- increaseValues utxoInHead - -- pure validSnapshot{snapshotUTxO = utxoInHead'} + -- pure validSnapshot{inHead = utxoInHead'} -- , do -- -- more in decommit -- someUTxOToDecrement' <- increaseValues =<< submapOf utxoInHead -- let balancedUTxOInHead' = balanceUTxOInHead utxoInHead someUTxOToDecrement' -- pure -- validSnapshot - -- { snapshotUTxO = balancedUTxOInHead' - -- , decommitUTxO = someUTxOToDecrement' + -- { inHead = balancedUTxOInHead' + -- , toDecommit = someUTxOToDecrement' -- } -- , -- decommit all - -- pure validSnapshot{snapshotUTxO = mempty, decommitUTxO = utxoInHead} + -- pure validSnapshot{inHead = mempty, toDecommit = utxoInHead} -- , arbitrary -- ] pure validSnapshot @@ -393,25 +389,12 @@ instance StateModel Model where return $ Map.fromList subset reduceValues :: ModelUTxO -> Gen ModelUTxO - reduceValues = Map.traverseWithKey reduceValue + reduceValues = traverse reduceValue where - reduceValue :: SingleUTxO -> Natural -> Gen Natural - reduceValue _ n = do - let n' = naturalToInteger n - reduction <- choose (0, n') - let reduced = if n' < reduction then 0 else n' - reduction - return (naturalFromInteger reduced) - - increaseValues :: ModelUTxO -> Gen ModelUTxO - increaseValues = Map.traverseWithKey (\_ n -> pure (n + naturalFromInteger 1)) - - shuffleValues :: ModelUTxO -> Gen ModelUTxO - shuffleValues utxo = do - let x = Map.keys utxo - let y = Map.elems utxo - x' <- shuffle x - let shuffledUTxO = Map.fromList $ zip x' y - pure shuffledUTxO + reduceValue n = do + let i = naturalToInteger n + reduction <- choose (0, i) + pure . naturalFromInteger $ i - reduction -- Determine actions we want to perform and expect to work. If this is False, -- validFailingAction is checked too. @@ -425,22 +408,14 @@ instance StateModel Model where headState == Open && snapshot `elem` knownSnapshots && snapshot.version == currentVersion - -- you are decrementing from existing utxo in the head - -- && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) - -- your tx is balanced with the utxo in the head - -- && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead Close{snapshot} -> headState == Open && snapshot `elem` knownSnapshots && ( if snapshot.number == 0 - then snapshotUTxO snapshot == initialUTxOInHead + then inHead snapshot == initialUTxOInHead else snapshot.version `elem` (currentVersion : [currentVersion - 1 | currentVersion > 0]) ) - -- you are decrementing from existing utxo in the head - && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) - -- your tx is balanced with the utxo in the head - && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead where Model{utxoInHead = initialUTxOInHead} = initialState Contest{actor, snapshot} -> @@ -449,10 +424,6 @@ instance StateModel Model where && actor `notElem` alreadyContested && snapshot.version `elem` (currentVersion : [currentVersion - 1 | currentVersion > 0]) && snapshot.number > closedSnapshotNumber - -- you are decrementing from existing utxo in the head - && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) - -- your tx is balanced with the utxo in the head - && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead Fanout{utxo, deltaUTxO} -> headState == Closed && utxo == utxoInHead @@ -462,7 +433,7 @@ instance StateModel Model where -- False, the action is discarded (e.g. it's invalid or we don't want to see -- it tried to perform). validFailingAction :: Model -> Action Model a -> Bool - validFailingAction Model{headState, knownSnapshots, utxoInHead, currentVersion} = \case + validFailingAction Model{headState, knownSnapshots, currentVersion} = \case Stop -> False NewSnapshot{} -> False -- Only filter non-matching states as we are not interested in these kind of @@ -471,30 +442,15 @@ instance StateModel Model where headState == Open && snapshot `elem` knownSnapshots && snapshot.version /= currentVersion - -- Ignore unbalanced decrements. - -- TODO: make them fail gracefully and test this? - -- && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead - -- Ignore decrements that work with non existing utxo in the head - -- && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) Close{snapshot} -> headState == Open && snapshot `elem` knownSnapshots && ( snapshot.number == 0 || snapshot.version `elem` (currentVersion : [currentVersion - 1 | currentVersion > 0]) ) - -- Ignore unbalanced close. - -- TODO: make them fail gracefully and test this? - && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead - -- Ignore close that work with non existing utxo in the head - && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) Contest{snapshot} -> headState == Closed && snapshot `elem` knownSnapshots - -- Ignore unbalanced close. - -- TODO: make them fail gracefully and test this? - && sum (decommitUTxO snapshot) + sum (snapshotUTxO snapshot) == sum utxoInHead - -- Ignore close that work with non existing utxo in the head - && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) Fanout{} -> headState == Closed @@ -508,24 +464,24 @@ instance StateModel Model where m { headState = Open , currentVersion = m.currentVersion + 1 - , utxoInHead = balanceUTxOInHead (utxoInHead m) (decommitUTxO snapshot) - -- TODO: why is this not needed?, pendingDecommitUTxO = m.pendingDecommitUTxO \\ snapshot.snapshotUTxO + , utxoInHead = utxoInHead m `remove` toDecommit snapshot + -- TODO: why is this not needed?, pendingDecommitUTxO = m.pendingDecommitUTxO \\ snapshot.inHead } Close{snapshot} -> m { headState = Closed , closedSnapshotNumber = snapshot.number , alreadyContested = [] - , utxoInHead = snapshotUTxO snapshot - , pendingDecommitUTxO = if currentVersion == snapshot.version then decommitUTxO snapshot else mempty + , utxoInHead = inHead snapshot + , pendingDecommitUTxO = if currentVersion == snapshot.version then toDecommit snapshot else mempty } Contest{actor, snapshot} -> m { headState = Closed , closedSnapshotNumber = snapshot.number , alreadyContested = actor : alreadyContested m - , utxoInHead = snapshotUTxO snapshot - , pendingDecommitUTxO = if currentVersion == snapshot.version then decommitUTxO snapshot else mempty + , utxoInHead = inHead snapshot + , pendingDecommitUTxO = if currentVersion == snapshot.version then toDecommit snapshot else mempty } Fanout{} -> m{headState = Final} @@ -701,10 +657,10 @@ signedSnapshot ms = signatures = aggregate [sign sk snapshot | sk <- [Fixture.aliceSk, Fixture.bobSk, Fixture.carolSk]] - utxo = realWorldModelUTxO (snapshotUTxO ms) + utxo = realWorldModelUTxO (inHead ms) utxoToDecommit = - let u = realWorldModelUTxO (decommitUTxO ms) + let u = realWorldModelUTxO (toDecommit ms) in if null u then Nothing else Just u -- | A confirmed snapshot (either initial or later confirmed), based onTxTra @@ -717,7 +673,7 @@ confirmedSnapshot modelSnapshot@ModelSnapshot{number} = { -- -- NOTE: The close validator would not check headId on close with -- initial snapshot, but we need to provide it still. headId = mkHeadId Fixture.testPolicyId - , initialUTxO = realWorldModelUTxO $ snapshotUTxO modelSnapshot + , initialUTxO = realWorldModelUTxO $ inHead modelSnapshot } _ -> ConfirmedSnapshot{snapshot, signatures} where @@ -887,16 +843,16 @@ expectValid TxResult{observation, constructedTx, spendableUTxO} fn = do counterexample' $ "Wrong observation: " <> show observation fn observation --- | Assertion helper to check whether a 'TxResult' was invalid. +-- | Assertion helper to check whether a 'TxResult' was invalid or construction failed. expectInvalid :: Monad m => TxResult -> PostconditionM' m () expectInvalid = \case TxResult{validationError = Nothing, constructedTx, spendableUTxO} -> do - counterexample' "Expected tx to fail validation" case constructedTx of - Left err -> counterexample' $ "But construction failed with: " <> err + Left _ -> pure () Right tx -> do + counterexample' "Expected tx to fail validation" counterexample' $ renderTxWithUTxO spendableUTxO tx - fail "But it did not fail" + fail "But it did not fail" _ -> pure () -- | Generate sometimes a value with given generator, bur more often just use From cdebb64ddaa814e3c3dbf33382685f3fe8f6e8b5 Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Thu, 10 Oct 2024 18:48:46 +0200 Subject: [PATCH 16/21] Small tuning on generators --- .../test/Hydra/Chain/Direct/TxTraceSpec.hs | 60 ++++++++++--------- 1 file changed, 31 insertions(+), 29 deletions(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 85f1e7f1de7..5a90d99bfcc 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -78,7 +78,7 @@ import Test.Hydra.Tx.Gen ( genVerificationKey, ) import Test.Hydra.Tx.Mutation (addParticipationTokens) -import Test.QuickCheck (Property, Smart (..), Testable, checkCoverage, choose, cover, elements, frequency, ioProperty, oneof, sublistOf, (===)) +import Test.QuickCheck (Property, Smart (..), Testable, checkCoverage, choose, cover, elements, frequency, ioProperty, sublistOf, (===)) import Test.QuickCheck.Monadic (monadic) import Test.QuickCheck.StateModel ( ActionWithPolarity (..), @@ -184,7 +184,7 @@ prop_runActions actions = coversInterestingActions actions . monadic runAppMProperty $ do - print actions + -- print actions void (runActions actions) where runAppMProperty :: AppM Property -> Property @@ -300,42 +300,44 @@ instance StateModel Model where arbitraryAction _lookup Model{headState, knownSnapshots, currentVersion, utxoInHead, pendingDecommitUTxO} = case headState of Open{} -> - oneof $ - [Some . NewSnapshot <$> genSnapshot] - <> [ do - actor <- elements allActors - snapshot <- elements knownSnapshots - pure $ Some Decrement{actor, snapshot} + frequency $ + [(5, Some . NewSnapshot <$> genSnapshot)] + <> [ ( 10 + , do + actor <- elements allActors + snapshot <- elements knownSnapshots + pure $ Some Decrement{actor, snapshot} + ) | not (null knownSnapshots) -- XXX: DRY this check ] - <> [ do - actor <- elements allActors - snapshot <- elements knownSnapshots - pure $ Some $ Close{actor, snapshot = snapshot} + <> [ ( 1 + , do + actor <- elements allActors + snapshot <- elements knownSnapshots + pure $ Some $ Close{actor, snapshot = snapshot} + ) | not (null knownSnapshots) ] Closed{} -> frequency $ - [ - ( 1 - , do - -- Fanout with the currently known model state. - pure $ - Some $ - Fanout - { utxo = utxoInHead - , deltaUTxO = pendingDecommitUTxO - } - ) - ] - <> [ ( 10 - , do + ( 1 + , do + -- Fanout with the currently known model state. + pure $ + Some $ + Fanout + { utxo = utxoInHead + , deltaUTxO = pendingDecommitUTxO + } + ) + : [ ( 3 + , do actor <- elements allActors snapshot <- elements knownSnapshots pure $ Some Contest{actor, snapshot} - ) - | not (null knownSnapshots) - ] + ) + | not (null knownSnapshots) + ] Final -> pure $ Some Stop where -- TODO: Generate a snapshot an honest node would sign given the current model state. From d105327b27f5b0197f2eeeca1d6103f6fa96e943 Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Thu, 10 Oct 2024 19:59:32 +0200 Subject: [PATCH 17/21] Model toDecommit evolution as we would expect it This is reusing the models pendingDecommit for this purpose. However, it would be cleaner to separate the model states between Open and Closed. --- .../test/Hydra/Chain/Direct/TxTraceSpec.hs | 51 ++++++++++++------- 1 file changed, 32 insertions(+), 19 deletions(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 5a90d99bfcc..9ccab801d9b 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -184,7 +184,7 @@ prop_runActions actions = coversInterestingActions actions . monadic runAppMProperty $ do - -- print actions + print actions void (runActions actions) where runAppMProperty :: AppM Property -> Property @@ -216,7 +216,9 @@ data Model = Model , closedSnapshotNumber :: SnapshotNumber , alreadyContested :: [Actor] , utxoInHead :: ModelUTxO - , pendingDecommitUTxO :: ModelUTxO + , -- XXX: This is used in two ways, to track pending decommits for generating + -- snapshots and to remember the pending (delta) utxo during close/fanout + pendingDecommit :: ModelUTxO } deriving (Show) @@ -225,6 +227,11 @@ latestSnapshotNumber = \case (s : _) -> s.number _ -> 0 +latestSnapshot :: [ModelSnapshot] -> Maybe ModelSnapshot +latestSnapshot = \case + [] -> Nothing + (s : _) -> Just s + -- | Model of a real snapshot which contains a 'SnapshotNumber` but also our -- simplified form of 'UTxO'. data ModelSnapshot = ModelSnapshot @@ -293,11 +300,11 @@ instance StateModel Model where , closedSnapshotNumber = 0 , alreadyContested = [] , utxoInHead = fromList $ map (,10) [A, B, C] - , pendingDecommitUTxO = Map.empty + , pendingDecommit = Map.empty } arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model)) - arbitraryAction _lookup Model{headState, knownSnapshots, currentVersion, utxoInHead, pendingDecommitUTxO} = + arbitraryAction _lookup Model{headState, knownSnapshots, currentVersion, utxoInHead, pendingDecommit} = case headState of Open{} -> frequency $ @@ -327,7 +334,7 @@ instance StateModel Model where Some $ Fanout { utxo = utxoInHead - , deltaUTxO = pendingDecommitUTxO + , deltaUTxO = pendingDecommit } ) : [ ( 3 @@ -342,12 +349,17 @@ instance StateModel Model where where -- TODO: Generate a snapshot an honest node would sign given the current model state. genSnapshot = do - toDecommit <- reduceValues =<< submapOf utxoInHead + -- Only decommit if not already pending + toDecommit <- + if null pendingDecommit + then submapOf utxoInHead >>= reduceValues + else pure pendingDecommit let validSnapshot = ModelSnapshot { version = currentVersion , number = latestSnapshotNumber knownSnapshots + 1 - , inHead = utxoInHead `remove` toDecommit + , -- TODO: could shuffle UTxO in head (retaining balance) + inHead = utxoInHead `remove` toDecommit , toDecommit } -- FIXME: check whether these cases are met @@ -395,13 +407,13 @@ instance StateModel Model where where reduceValue n = do let i = naturalToInteger n - reduction <- choose (0, i) + reduction <- choose (1, i) pure . naturalFromInteger $ i - reduction -- Determine actions we want to perform and expect to work. If this is False, -- validFailingAction is checked too. precondition :: Model -> Action Model a -> Bool - precondition Model{headState, knownSnapshots, closedSnapshotNumber, alreadyContested, utxoInHead, pendingDecommitUTxO, currentVersion} = \case + precondition Model{headState, knownSnapshots, closedSnapshotNumber, alreadyContested, currentVersion, utxoInHead, pendingDecommit} = \case Stop -> headState /= Final NewSnapshot{newSnapshot} -> newSnapshot.version == currentVersion @@ -429,7 +441,7 @@ instance StateModel Model where Fanout{utxo, deltaUTxO} -> headState == Closed && utxo == utxoInHead - && deltaUTxO == pendingDecommitUTxO + && deltaUTxO == pendingDecommit -- Determine actions we want to perform and want to see failing. If this is -- False, the action is discarded (e.g. it's invalid or we don't want to see @@ -461,29 +473,30 @@ instance StateModel Model where case t of Stop -> m NewSnapshot{newSnapshot} -> - m{knownSnapshots = newSnapshot : m.knownSnapshots} + m + { knownSnapshots = newSnapshot : m.knownSnapshots + , pendingDecommit = newSnapshot.toDecommit + } Decrement{snapshot} -> m { headState = Open , currentVersion = m.currentVersion + 1 - , utxoInHead = utxoInHead m `remove` toDecommit snapshot - -- TODO: why is this not needed?, pendingDecommitUTxO = m.pendingDecommitUTxO \\ snapshot.inHead + , utxoInHead = m.utxoInHead `remove` snapshot.toDecommit + , pendingDecommit = mempty } Close{snapshot} -> m { headState = Closed , closedSnapshotNumber = snapshot.number , alreadyContested = [] - , utxoInHead = inHead snapshot - , pendingDecommitUTxO = if currentVersion == snapshot.version then toDecommit snapshot else mempty + , pendingDecommit = if currentVersion == snapshot.version then toDecommit snapshot else mempty } Contest{actor, snapshot} -> m { headState = Closed , closedSnapshotNumber = snapshot.number , alreadyContested = actor : alreadyContested m - , utxoInHead = inHead snapshot - , pendingDecommitUTxO = if currentVersion == snapshot.version then toDecommit snapshot else mempty + , pendingDecommit = if currentVersion == snapshot.version then toDecommit snapshot else mempty } Fanout{} -> m{headState = Final} @@ -763,7 +776,7 @@ newContestTx actor openVersion snapshot = do -- seedTxIn and contestation period. Consequently, the lower bound used is -- precisely at the maximum deadline slot as if everyone contested. newFanoutTx :: Actor -> ModelUTxO -> ModelUTxO -> AppM (Either FanoutTxError Tx) -newFanoutTx actor utxo deltaUTxO = do +newFanoutTx actor utxo pendingDecommit = do spendableUTxO <- get pure $ fanout @@ -772,7 +785,7 @@ newFanoutTx actor utxo deltaUTxO = do Fixture.testSeedInput (realWorldModelUTxO utxo) -- Model world has no 'Maybe ModelUTxO', but real world does. - (if null deltaUTxO then Nothing else Just $ realWorldModelUTxO deltaUTxO) + (if null pendingDecommit then Nothing else Just $ realWorldModelUTxO pendingDecommit) deadline where CP.UnsafeContestationPeriod contestationPeriod = Fixture.cperiod From 3a150cdd8ae1831bf44f4a7be2aa2ccb8e5468f2 Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Sun, 27 Oct 2024 09:46:24 +0100 Subject: [PATCH 18/21] Fix nextState of Close/Contest --- hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 9ccab801d9b..c55db42549a 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -350,6 +350,7 @@ instance StateModel Model where -- TODO: Generate a snapshot an honest node would sign given the current model state. genSnapshot = do -- Only decommit if not already pending + -- TODO: prevent 0 quantity decommit toDecommit <- if null pendingDecommit then submapOf utxoInHead >>= reduceValues @@ -489,6 +490,7 @@ instance StateModel Model where { headState = Closed , closedSnapshotNumber = snapshot.number , alreadyContested = [] + , utxoInHead = snapshot.inHead , pendingDecommit = if currentVersion == snapshot.version then toDecommit snapshot else mempty } Contest{actor, snapshot} -> @@ -496,6 +498,7 @@ instance StateModel Model where { headState = Closed , closedSnapshotNumber = snapshot.number , alreadyContested = actor : alreadyContested m + , utxoInHead = snapshot.inHead , pendingDecommit = if currentVersion == snapshot.version then toDecommit snapshot else mempty } Fanout{} -> m{headState = Final} From d96d55c156fedfd4cbde6a6182b50f15f00fdac0 Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Sun, 27 Oct 2024 10:14:23 +0100 Subject: [PATCH 19/21] Futher simplify ModelUTxO It is a list of A-E elements only where shuffling of the elements represents off-chain transactions that maintain balance. --- .../test/Hydra/Chain/Direct/TxTraceSpec.hs | 59 ++++++------------- 1 file changed, 18 insertions(+), 41 deletions(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index c55db42549a..64cfcb7bd04 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -10,8 +10,9 @@ -- Given an initial UTxO, the model generates a plausible sequence of snapshots -- that an honest node would approve. That is, the total balance of UTxO remains -- constant and utxoToDecommit is only allowed to clear if the version is --- incremented. All snapshots are correctly signed and UTxOs are simplified such --- that their identity is A-E and value is just a number. +-- incremented. Consequently, also all snapshots are correctly signed (we don't +-- test handling of adverarial signatures). UTxOs are simplified such that they +-- are A-E items, where each maps to an arbitrary real UTxO. -- -- From this sequence of valid snapshots, possible Decrement and Close actions -- are generated, along with occasional Contest and consequential Fanout. @@ -22,11 +23,9 @@ import Test.Hydra.Prelude import Cardano.Api.UTxO (UTxO) import Cardano.Api.UTxO qualified as UTxO -import Cardano.Ledger.Coin (Coin (..)) -import Data.Map (differenceWith) +import Data.List ((\\)) import Data.Map.Strict qualified as Map import Data.Time.Clock.POSIX (posixSecondsToUTCTime) -import GHC.Natural (naturalFromInteger, naturalToInteger) import Hydra.Cardano.Api ( PaymentKey, SlotNo (..), @@ -78,7 +77,7 @@ import Test.Hydra.Tx.Gen ( genVerificationKey, ) import Test.Hydra.Tx.Mutation (addParticipationTokens) -import Test.QuickCheck (Property, Smart (..), Testable, checkCoverage, choose, cover, elements, frequency, ioProperty, sublistOf, (===)) +import Test.QuickCheck (Property, Smart (..), Testable, checkCoverage, cover, elements, frequency, ioProperty, shuffle, sublistOf, (===)) import Test.QuickCheck.Monadic (monadic) import Test.QuickCheck.StateModel ( ActionWithPolarity (..), @@ -184,7 +183,7 @@ prop_runActions actions = coversInterestingActions actions . monadic runAppMProperty $ do - print actions + -- print actions void (runActions actions) where runAppMProperty :: AppM Property -> Property @@ -201,12 +200,7 @@ instance Arbitrary SingleUTxO where arbitrary = genericArbitrary shrink = genericShrink -type ModelUTxO = Map SingleUTxO Natural - --- | Reduce left hand side by right hand side. -remove :: ModelUTxO -> ModelUTxO -> ModelUTxO -remove = - differenceWith $ \a b -> if a > b then Just $ a - b else Nothing +type ModelUTxO = [SingleUTxO] data Model = Model { headState :: State @@ -299,8 +293,8 @@ instance StateModel Model where , currentVersion = 0 , closedSnapshotNumber = 0 , alreadyContested = [] - , utxoInHead = fromList $ map (,10) [A, B, C] - , pendingDecommit = Map.empty + , utxoInHead = fromList [A, B, C] + , pendingDecommit = mempty } arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model)) @@ -347,20 +341,18 @@ instance StateModel Model where ] Final -> pure $ Some Stop where - -- TODO: Generate a snapshot an honest node would sign given the current model state. genSnapshot = do -- Only decommit if not already pending - -- TODO: prevent 0 quantity decommit toDecommit <- if null pendingDecommit - then submapOf utxoInHead >>= reduceValues + then sublistOf utxoInHead else pure pendingDecommit + inHead <- shuffle $ utxoInHead \\ toDecommit let validSnapshot = ModelSnapshot { version = currentVersion , number = latestSnapshotNumber knownSnapshots + 1 - , -- TODO: could shuffle UTxO in head (retaining balance) - inHead = utxoInHead `remove` toDecommit + , inHead , toDecommit } -- FIXME: check whether these cases are met @@ -398,19 +390,6 @@ instance StateModel Model where -- ] pure validSnapshot - submapOf :: Ord k => Map k v -> Gen (Map k v) - submapOf model = do - subset <- sublistOf (Map.toList model) - return $ Map.fromList subset - - reduceValues :: ModelUTxO -> Gen ModelUTxO - reduceValues = traverse reduceValue - where - reduceValue n = do - let i = naturalToInteger n - reduction <- choose (1, i) - pure . naturalFromInteger $ i - reduction - -- Determine actions we want to perform and expect to work. If this is False, -- validFailingAction is checked too. precondition :: Model -> Action Model a -> Bool @@ -482,7 +461,7 @@ instance StateModel Model where m { headState = Open , currentVersion = m.currentVersion + 1 - , utxoInHead = m.utxoInHead `remove` snapshot.toDecommit + , utxoInHead = m.utxoInHead \\ snapshot.toDecommit , pendingDecommit = mempty } Close{snapshot} -> @@ -648,13 +627,11 @@ allActors = [Alice, Bob, Carol] -- | Map a 'ModelUTxO' to a real-world 'UTxO'. realWorldModelUTxO :: ModelUTxO -> UTxO realWorldModelUTxO = - Map.foldMapWithKey - ( \k balance -> - genUTxOWithBalance balance `generateWith` fromEnum k - ) + foldMap (\a -> gen `generateWith` fromEnum a) where - genUTxOWithBalance b = - genUTxO1 (modifyTxOutValue (const $ lovelaceToValue (Coin $ naturalToInteger b)) <$> genTxOut) + gen = do + lovelace <- arbitrary + genUTxO1 (modifyTxOutValue (const $ lovelaceToValue lovelace) <$> genTxOut) -- | A correctly signed snapshot. Given a snapshot number a snapshot signed by -- all participants (alice, bob and carol) with some UTxO contained is produced. @@ -873,7 +850,7 @@ expectInvalid = \case fail "But it did not fail" _ -> pure () --- | Generate sometimes a value with given generator, bur more often just use +-- | Generate sometimes a value with given generator, but more often just use -- the given value. orSometimes :: a -> Gen a -> Gen a orSometimes a gen = frequency [(1, pure a), (2, gen)] From ea603b9e74e005ab455cc05d1879e517904120d4 Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Sun, 27 Oct 2024 10:48:43 +0100 Subject: [PATCH 20/21] Drop old, commented code --- .../test/Hydra/Chain/Direct/TxTraceSpec.hs | 33 ------------------- 1 file changed, 33 deletions(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 64cfcb7bd04..ad221a9fd9e 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -355,39 +355,6 @@ instance StateModel Model where , inHead , toDecommit } - -- FIXME: check whether these cases are met - -- oneof - -- [ -- valid - -- pure validSnapshot - -- , -- unbalanced - -- pure validSnapshot{inHead = utxoInHead} - -- , do - -- -- old - -- let number' = if closedSnapshotNumber == 0 then 0 else closedSnapshotNumber - 1 - -- pure (validSnapshot :: ModelSnapshot){number = number'} - -- , -- new - -- pure (validSnapshot :: ModelSnapshot){number = closedSnapshotNumber + 1} - -- , do - -- -- shuffled - -- someUTxOToDecrement' <- shuffleValues filteredSomeUTxOToDecrement - -- pure validSnapshot{toDecommit = someUTxOToDecrement'} - -- , do - -- -- more in head - -- utxoInHead' <- increaseValues utxoInHead - -- pure validSnapshot{inHead = utxoInHead'} - -- , do - -- -- more in decommit - -- someUTxOToDecrement' <- increaseValues =<< submapOf utxoInHead - -- let balancedUTxOInHead' = balanceUTxOInHead utxoInHead someUTxOToDecrement' - -- pure - -- validSnapshot - -- { inHead = balancedUTxOInHead' - -- , toDecommit = someUTxOToDecrement' - -- } - -- , -- decommit all - -- pure validSnapshot{inHead = mempty, toDecommit = utxoInHead} - -- , arbitrary - -- ] pure validSnapshot -- Determine actions we want to perform and expect to work. If this is False, From 461282eebb66c98cca2337c02817214f70ed68ec Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Sun, 27 Oct 2024 10:46:04 +0100 Subject: [PATCH 21/21] Enable coverage check on main property Using lower Confidence values, we should not see way very long tests at the cost of occasional false positives. In such cases, the actual coverage numbers and "interesting values" test should give an indication whether it was rightfully failing or would have taken just very long. --- .../test/Hydra/Chain/Direct/TxTraceSpec.hs | 24 ++++++++++++------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index ad221a9fd9e..621f190fadf 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -77,7 +77,7 @@ import Test.Hydra.Tx.Gen ( genVerificationKey, ) import Test.Hydra.Tx.Mutation (addParticipationTokens) -import Test.QuickCheck (Property, Smart (..), Testable, checkCoverage, cover, elements, frequency, ioProperty, shuffle, sublistOf, (===)) +import Test.QuickCheck (Confidence (..), Property, Smart (..), Testable, checkCoverage, checkCoverageWith, cover, elements, frequency, ioProperty, shuffle, sublistOf, (===)) import Test.QuickCheck.Monadic (monadic) import Test.QuickCheck.StateModel ( ActionWithPolarity (..), @@ -103,7 +103,13 @@ spec = do realWorldModelUTxO (u1 <> u2) === (realWorldModelUTxO u1 <> realWorldModelUTxO u2) prop "generates interesting transaction traces" $ \actions -> checkCoverage $ coversInterestingActions actions True - prop "all valid transactions" prop_runActions + prop "all valid transactions" $ + -- NOTE: Using lower confidence to improve performance. In case of an error, + -- check coverage numbers and also the distribution in above test (which is + -- way faster). + checkCoverageWith + Confidence{certainty = 100, tolerance = 0.8} + prop_runActions coversInterestingActions :: Testable p => Actions Model -> p -> Property coversInterestingActions (Actions_ _ (Smart _ steps)) p = @@ -111,12 +117,12 @@ coversInterestingActions (Actions_ _ (Smart _ steps)) p = & cover 1 (null steps) "empty" & cover 50 (hasSomeSnapshots steps) "has some snapshots" & cover 5 (hasDecrement steps) "has decrements" - & cover 1 (countContests steps >= 2) "has multiple contests" + & cover 0.1 (countContests steps >= 2) "has multiple contests" & cover 5 (closeNonInitial steps) "close with non initial snapshots" & cover 10 (hasFanout steps) "reach fanout" - & cover 0.5 (fanoutWithEmptyUTxO steps) "fanout with empty UTxO" - & cover 1 (fanoutWithSomeUTxO steps) "fanout with some UTxO" - & cover 0.5 (fanoutWithDelta steps) "fanout with additional UTxO to distribute" + & cover 10 (fanoutWithEmptyUTxO steps) "fanout with empty UTxO" + & cover 10 (fanoutWithSomeUTxO steps) "fanout with some UTxO" + & cover 10 (fanoutWithDelta steps) "fanout with additional UTxO to distribute" where hasSomeSnapshots = any $ @@ -302,8 +308,8 @@ instance StateModel Model where case headState of Open{} -> frequency $ - [(5, Some . NewSnapshot <$> genSnapshot)] - <> [ ( 10 + [(3, Some . NewSnapshot <$> genSnapshot)] + <> [ ( 3 , do actor <- elements allActors snapshot <- elements knownSnapshots @@ -331,7 +337,7 @@ instance StateModel Model where , deltaUTxO = pendingDecommit } ) - : [ ( 3 + : [ ( 10 , do actor <- elements allActors snapshot <- elements knownSnapshots