Skip to content

Commit

Permalink
TxTrace: Refactor to a stateful SUT
Browse files Browse the repository at this point in the history
By creating an AppM which is a MonadState UTxO, we can get rid of some
book-keeping in the model in exchange of making the SUT actually
stateful: performing transactions depend on the UTxO of the previous
action.
  • Loading branch information
ch1bo authored and v0d1ch committed May 7, 2024
1 parent a5ba64a commit 89420c2
Show file tree
Hide file tree
Showing 4 changed files with 99 additions and 67 deletions.
1 change: 1 addition & 0 deletions hydra-node/src/Hydra/Chain/Direct/Handlers.hs
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ import Data.Map.Strict qualified as Map
import Hydra.Cardano.Api (
BlockHeader,
ChainPoint (..),
NetworkId,
Tx,
TxId,
chainPointToSlotNo,
Expand Down
150 changes: 83 additions & 67 deletions hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs
Original file line number Diff line number Diff line change
Expand Up @@ -26,16 +26,16 @@ import Hydra.Snapshot (ConfirmedSnapshot (..), Snapshot (..), SnapshotNumber, nu
import PlutusTx.Builtins (toBuiltin)
import Test.Hydra.Fixture (genForParty)
import Test.Hydra.Fixture qualified as Fixture
import Test.QuickCheck (Property, Smart (..), checkCoverage, cover, elements, forAll, frequency, oneof, resize)
import Test.QuickCheck.Monadic (monadicIO)
import Test.QuickCheck (Property, Smart (..), checkCoverage, cover, elements, forAll, frequency, ioProperty, oneof, resize)
import Test.QuickCheck.Monadic (monadic)
import Test.QuickCheck.StateModel (
ActionWithPolarity (..),
Actions (..),
Any (..),
HasVariables (getAllVariables),
LookUp,
Polarity (PosPolarity),
PostconditionM,
Realized,
RunModel (..),
StateModel (..),
Step ((:=)),
Expand Down Expand Up @@ -89,14 +89,18 @@ prop_traces =

prop_runActions :: Actions Model -> Property
prop_runActions actions =
monadicIO $
monadic runAppMProperty $ do
void (runActions actions)
where
runAppMProperty :: AppM Property -> Property
runAppMProperty action = ioProperty $ do
utxoV <- newIORef openHeadUTxO
runReaderT (runAppM action) utxoV

-- * Model

data Model = Model
{ headState :: State
, lastResult :: Maybe (Var TxResult)
, alreadyContested :: [Actor]
}
deriving (Show)
Expand All @@ -111,8 +115,7 @@ data Actor = Alice | Bob | Carol
deriving (Show, Eq)

data TxResult = TxResult
{ newUTxO :: UTxO
, tx :: Tx
{ tx :: Tx
, validationError :: Maybe String
, observation :: HeadObservation
}
Expand All @@ -130,7 +133,6 @@ instance StateModel Model where
initialState =
Model
{ headState = Open 0 -- TODO: move latestSnapshot out?
, lastResult = Nothing
, alreadyContested = []
}

Expand Down Expand Up @@ -192,23 +194,20 @@ instance StateModel Model where

nextState :: Model -> Action Model a -> Var a -> Model
nextState m Stop _ = m
nextState m t result =
nextState m t _result =
case t of
Decrement{snapshotNumber} ->
m
{ headState = Open snapshotNumber
, lastResult = Just result
}
Close{snapshotNumber} ->
m
{ headState = Closed snapshotNumber
, lastResult = Just result
, alreadyContested = []
}
Contest{actor, snapshotNumber} ->
m
{ headState = Closed snapshotNumber
, lastResult = Just result
, alreadyContested = actor : alreadyContested m
}
Fanout{} -> m{headState = Final}
Expand All @@ -222,26 +221,36 @@ instance HasVariables (Action Model a) where
deriving instance Eq (Action Model a)
deriving instance Show (Action Model a)

instance RunModel Model IO where
perform :: Model -> Action Model a -> LookUp IO -> IO a
perform Model{lastResult} action lookupVar = do
-- | Application monad to perform model actions. Currently it only keeps a
-- 'UTxO' which is updated whenever transactions are valid in 'performTx'.
newtype AppM a = AppM {runAppM :: ReaderT (IORef UTxO) IO a}
deriving newtype (Functor, Applicative, Monad, MonadIO, MonadFail, MonadThrow)

instance MonadReader UTxO AppM where
ask = AppM $ ask >>= liftIO . readIORef

local f action = do
utxo <- ask
r <- newIORef (f utxo)
AppM $ local (const r) $ runAppM action

instance MonadState UTxO AppM where
get = ask
put utxo = AppM $ ask >>= liftIO . flip writeIORef utxo

type instance Realized AppM a = a

instance RunModel Model AppM where
perform Model{} action _lookupVar = do
case action of
Decrement{actor, snapshotNumber} -> do
let utxo = maybe openHeadUTxO (newUTxO . lookupVar) lastResult
tx <- newDecrementTx utxo actor $ signedSnapshot snapshotNumber
performTx utxo tx
Close{actor, snapshotNumber} -> do
let utxo = maybe openHeadUTxO (newUTxO . lookupVar) lastResult
tx <- newCloseTx utxo actor $ confirmedSnapshot snapshotNumber
performTx utxo tx
Contest{actor, snapshotNumber} -> do
let utxo = maybe openHeadUTxO (newUTxO . lookupVar) lastResult
tx <- newContestTx utxo actor $ confirmedSnapshot snapshotNumber
performTx utxo tx
Fanout{snapshotNumber} -> do
let utxo = maybe openHeadUTxO (newUTxO . lookupVar) lastResult
tx <- newFanoutTx utxo Alice snapshotNumber
performTx utxo tx
Decrement{actor, snapshotNumber} ->
performTx =<< newDecrementTx actor (signedSnapshot snapshotNumber)
Close{actor, snapshotNumber} ->
performTx =<< newCloseTx actor (confirmedSnapshot snapshotNumber)
Contest{actor, snapshotNumber} ->
performTx =<< newContestTx actor (confirmedSnapshot snapshotNumber)
Fanout{snapshotNumber} ->
performTx =<< newFanoutTx Alice snapshotNumber
Stop -> pure ()

postcondition (modelBefore, modelAfter) action _lookup result = do
Expand Down Expand Up @@ -286,6 +295,35 @@ instance RunModel Model IO where
Contest{} -> expectInvalid result
_ -> pure True

-- | Perform a transaction by evaluating and observing it. This updates the
-- 'UTxO' in the 'AppM' if a transaction is valid and produces a 'TxResult' that
-- can be used to assert expected success / failure.
performTx :: Tx -> AppM TxResult
performTx tx = do
utxo <- get
let validationError = getValidationError utxo
when (isNothing validationError) $ do
put $ adjustUTxO tx utxo
pure
TxResult
{ tx
, validationError
, observation = observeHeadTx Fixture.testNetworkId utxo tx
}
where
getValidationError utxo =
case evaluateTx tx utxo of
Left err ->
Just $ show err
Right redeemerReport
| any isLeft (Map.elems redeemerReport) ->
Just . toString . unlines $
fromString
<$> [ "Transaction evaluation failed: " <> renderTxWithUTxO utxo tx
, "Some redeemers failed: " <> show redeemerReport
]
| otherwise -> Nothing

-- * Fixtures and glue code

-- | List of all model actors corresponding to the fixtures used.
Expand Down Expand Up @@ -357,27 +395,29 @@ openHeadUTxO =
}

-- | Creates a decrement transaction using given utxo and given snapshot.
newDecrementTx :: HasCallStack => UTxO -> Actor -> (Snapshot Tx, MultiSignature (Snapshot Tx)) -> IO Tx
newDecrementTx utxo actor (snapshot, signatures) =
newDecrementTx :: HasCallStack => Actor -> (Snapshot Tx, MultiSignature (Snapshot Tx)) -> AppM Tx
newDecrementTx actor (snapshot, signatures) = do
spendableUTxO <- get
either (failure . show) pure $
decrement
(actorChainContext actor)
(mkHeadId Fixture.testPolicyId)
Fixture.testHeadParameters
utxo
spendableUTxO
snapshot
signatures

-- | Creates a transaction that closes 'openHeadUTxO' with given the snapshot.
-- NOTE: This uses fixtures for headId, parties (alice, bob, carol),
-- contestation period and also claims to close at time 0 resulting in a
-- contestation deadline of 0 + cperiod.
newCloseTx :: HasCallStack => UTxO -> Actor -> ConfirmedSnapshot Tx -> IO Tx
newCloseTx utxo actor snapshot =
newCloseTx :: HasCallStack => Actor -> ConfirmedSnapshot Tx -> AppM Tx
newCloseTx actor snapshot = do
spendableUTxO <- get
either (failure . show) pure $
close
(actorChainContext actor)
utxo
spendableUTxO
(mkHeadId Fixture.testPolicyId)
Fixture.testHeadParameters
snapshot
Expand All @@ -391,8 +431,9 @@ newCloseTx utxo actor snapshot =
-- | Creates a contest transaction using given utxo and contesting with given
-- snapshot. NOTE: This uses fixtures for headId, contestation period and also
-- claims to contest at time 0.
newContestTx :: HasCallStack => UTxO -> Actor -> ConfirmedSnapshot Tx -> IO Tx
newContestTx spendableUTxO actor snapshot =
newContestTx :: HasCallStack => Actor -> ConfirmedSnapshot Tx -> AppM Tx
newContestTx actor snapshot = do
spendableUTxO <- get
either (failure . show) pure $
contest
(actorChainContext actor)
Expand All @@ -407,8 +448,9 @@ newContestTx spendableUTxO actor snapshot =
-- | Creates a fanout transaction using given utxo. NOTE: This uses fixtures for
-- seedTxIn and contestation period. Consequently, the lower bound used is
-- precisely at the maximum deadline slot as if everyone contested.
newFanoutTx :: HasCallStack => UTxO -> Actor -> SnapshotNumber -> IO Tx
newFanoutTx spendableUTxO actor snapshotNumber =
newFanoutTx :: HasCallStack => Actor -> SnapshotNumber -> AppM Tx
newFanoutTx actor snapshotNumber = do
spendableUTxO <- get
either (failure . show) pure $
fanout
(actorChainContext actor)
Expand Down Expand Up @@ -443,32 +485,6 @@ testScriptRegistry = genScriptRegistry `generateWith` 42

-- * Helpers

-- | Perform a transaction by evaluating and observing it. This produces a
-- 'TxResult' that also contains the new UTxO and can be used to assert expected
-- success / failure.
performTx :: Monad m => UTxO -> Tx -> m TxResult
performTx utxo tx =
pure
TxResult
{ newUTxO = adjustUTxO tx utxo
, tx
, validationError
, observation = observeHeadTx Fixture.testNetworkId utxo tx
}
where
validationError =
case evaluateTx tx utxo of
Left err ->
Just $ show err
Right redeemerReport
| any isLeft (Map.elems redeemerReport) ->
Just . toString . unlines $
fromString
<$> [ "Transaction evaluation failed: " <> renderTxWithUTxO utxo tx
, "Some redeemers failed: " <> show redeemerReport
]
| otherwise -> Nothing

-- | Assertion helper to check whether a 'TxResult' was valid and the expected
-- 'HeadObservation' could be made. To be used in 'postcondition'.
expectValid :: Monad m => TxResult -> (HeadObservation -> PostconditionM m Bool) -> PostconditionM m Bool
Expand Down
1 change: 1 addition & 0 deletions hydra-prelude/hydra-prelude.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ library
, generic-random
, gitrev
, io-classes >=1.0.0.0
, pretty-simple
, QuickCheck
, relude
, si-timers >=1.0.0.0
Expand Down
14 changes: 14 additions & 0 deletions hydra-prelude/src/Hydra/Prelude.hs
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
-- NOTE: Usage of 'trace' is accepted here.
{-# OPTIONS_GHC -Wno-deprecations #-}

module Hydra.Prelude (
module Relude,
module Control.Monad.Class.MonadSTM,
Expand Down Expand Up @@ -35,6 +38,8 @@ module Hydra.Prelude (
decodeBase16,
(?>),
withFile,
spy,
spy',
) where

import Cardano.Binary (
Expand Down Expand Up @@ -154,6 +159,7 @@ import Test.QuickCheck (
)
import Test.QuickCheck.Gen (Gen (..))
import Test.QuickCheck.Random (mkQCGen)
import Text.Pretty.Simple (pShow)

-- | Provides a sensible way of automatically deriving generic 'Arbitrary'
-- instances for data-types. In the case where more advanced or tailored
Expand Down Expand Up @@ -249,3 +255,11 @@ withFile fp mode action =
System.IO.withFile fp mode (try . action) >>= \case
Left (e :: IOException) -> throwIO e
Right x -> pure x

-- | Like 'traceShow', but with pretty printing of the value.
spy :: Show a => a -> a
spy a = trace (toString $ pShow a) a

-- | Like 'spy' but prefixed with a label.
spy' :: Show a => String -> a -> a
spy' msg a = trace (msg <> ": " <> toString (pShow a)) a

0 comments on commit 89420c2

Please sign in to comment.