diff --git a/hydra-node/src/Hydra/Ledger/Cardano/Evaluate.hs b/hydra-node/src/Hydra/Ledger/Cardano/Evaluate.hs index 6416bf1d56d..1689c1e0081 100644 --- a/hydra-node/src/Hydra/Ledger/Cardano/Evaluate.hs +++ b/hydra-node/src/Hydra/Ledger/Cardano/Evaluate.hs @@ -66,7 +66,7 @@ import Hydra.Ledger.Cardano.Time (slotNoFromUTCTime, slotNoToUTCTime) import Ouroboros.Consensus.Cardano.Block (CardanoEras) import Ouroboros.Consensus.HardFork.History ( Bound (Bound, boundEpoch, boundSlot, boundTime), - EraEnd (EraEnd), + EraEnd (..), EraParams (..), EraSummary (..), SafeZone (..), @@ -324,6 +324,28 @@ eraHistoryWithHorizonAt slotNo@(SlotNo n) = eraSafeZone = UnsafeIndefiniteSafeZone } +eraHistoryWithoutHorizon :: EraHistory +eraHistoryWithoutHorizon = + EraHistory (mkInterpreter summary) + where + summary :: Summary (CardanoEras StandardCrypto) + summary = + Summary . NonEmptyOne $ + EraSummary + { eraStart = initBound + , eraEnd = EraUnbounded + , eraParams + } + + eraParams = + EraParams + { eraEpochSize = EpochSize 1 + , eraSlotLength = mkSlotLength 1 + , -- NOTE: unused if the 'eraEnd' is already defined, but would be used to + -- extend the last era accordingly in the real cardano-node + eraSafeZone = UnsafeIndefiniteSafeZone + } + epochSize :: EpochSize epochSize = EpochSize 100 diff --git a/hydra-node/test/Hydra/Model.hs b/hydra-node/test/Hydra/Model.hs index aabb01f2d6f..4010a46f168 100644 --- a/hydra-node/test/Hydra/Model.hs +++ b/hydra-node/test/Hydra/Model.hs @@ -72,9 +72,10 @@ import Hydra.Model.Payment (CardanoSigningKey (..), Payment (..), applyTx, genAd import Hydra.Node (createNodeState, runHydraNode) import Hydra.Party (Party (..), deriveParty) import Hydra.Snapshot qualified as Snapshot -import Test.QuickCheck (choose, counterexample, elements, frequency, resize, sized, tabulate, vectorOf) +import Test.Hydra.Prelude (failure) +import Test.QuickCheck (choose, elements, frequency, resize, sized, tabulate, vectorOf) import Test.QuickCheck.DynamicLogic (DynLogicModel) -import Test.QuickCheck.StateModel (Any (..), HasVariables, Realized, RunModel (..), StateModel (..), Var, VarContext) +import Test.QuickCheck.StateModel (Any (..), HasVariables, PostconditionM, Realized, RunModel (..), StateModel (..), Var, VarContext, counterexamplePost) import Test.QuickCheck.StateModel.Variables (HasVariables (..)) import Prelude qualified @@ -117,25 +118,12 @@ data GlobalState { headParameters :: HeadParameters , offChainState :: OffChainState } + | Closed + { closedUTxO :: UTxOType Payment + } | Final {finalUTxO :: UTxOType Payment} deriving stock (Eq, Show) -isInitialState :: GlobalState -> Bool -isInitialState Initial{} = True -isInitialState _ = False - -isOpenState :: GlobalState -> Bool -isOpenState Open{} = True -isOpenState _ = False - -isFinalState :: GlobalState -> Bool -isFinalState Final{} = True -isFinalState _ = False - -isIdleState :: GlobalState -> Bool -isIdleState Idle{} = True -isIdleState _ = False - isPendingCommitFrom :: Party -> GlobalState -> Bool isPendingCommitFrom party Initial{pendingCommits} = party `Map.member` pendingCommits @@ -143,7 +131,7 @@ isPendingCommitFrom _ _ = False type Uncommitted = Map.Map Party (UTxOType Payment) -data OffChainState = OffChainState {confirmedUTxO :: UTxOType Payment} +newtype OffChainState = OffChainState {confirmedUTxO :: UTxOType Payment} deriving stock (Eq, Show) -- This is needed to be able to use `WorldState` inside DL formulae @@ -170,11 +158,13 @@ instance StateModel WorldState where Commit :: Party -> UTxOType Payment -> Action WorldState ActualCommitted Abort :: Party -> Action WorldState () Close :: Party -> Action WorldState () + Fanout :: Party -> Action WorldState UTxO NewTx :: Party -> Payment -> Action WorldState Payment Wait :: DiffTime -> Action WorldState () ObserveConfirmedTx :: Var Payment -> Action WorldState () -- Check that all parties have observed the head as open ObserveHeadIsOpen :: Action WorldState () + RollbackAndForward :: Natural -> Action WorldState () StopTheWorld :: Action WorldState () initialState = @@ -197,6 +187,12 @@ instance StateModel WorldState where frequency [ (5, genNewTx) , (1, genClose) + , (1, genRollbackAndForward) + ] + Closed{} -> + frequency + [ (5, genFanout) + , (1, genRollbackAndForward) ] Final{} -> fmap Some genSeed where @@ -217,6 +213,13 @@ instance StateModel WorldState where let party = deriveParty key pure . Some $ Close party + genFanout = + Some . Fanout . deriveParty . fst <$> elements hydraParties + + genRollbackAndForward = do + numberOfBlocks <- choose (1, 2) + pure . Some $ RollbackAndForward (wordToNatural numberOfBlocks) + precondition WorldState{hydraState = Start} Seed{} = True precondition WorldState{hydraState = Idle{}} Init{} = @@ -235,6 +238,16 @@ instance StateModel WorldState where True precondition WorldState{hydraState = Open{}} ObserveHeadIsOpen = True + precondition WorldState{hydraState = Closed{}} (Fanout _) = + True + precondition WorldState{hydraState} (RollbackAndForward _) = + case hydraState of + Start{} -> False + Idle{} -> False + Initial{} -> False + Open{} -> True + Closed{} -> True + Final{} -> False precondition _ StopTheWorld = True precondition _ _ = @@ -305,7 +318,13 @@ instance StateModel WorldState where WorldState{hydraParties, hydraState = updateWithClose hydraState} where updateWithClose = \case - Open{offChainState} -> Final $ confirmedUTxO offChainState + Open{offChainState = OffChainState{confirmedUTxO}} -> Closed confirmedUTxO + _ -> error "unexpected state" + Fanout{} -> + WorldState{hydraParties, hydraState = updateWithFanout hydraState} + where + updateWithFanout = \case + Closed{closedUTxO} -> Final closedUTxO _ -> error "unexpected state" -- (NewTx _ tx) -> @@ -321,6 +340,7 @@ instance StateModel WorldState where } } _ -> error "unexpected state" + RollbackAndForward _numberOfBlocks -> s Wait _ -> s ObserveConfirmedTx _ -> s ObserveHeadIsOpen -> s @@ -353,7 +373,7 @@ genToCommit (hk, ck) = do genContestationPeriod :: Gen ContestationPeriod genContestationPeriod = do - n <- choose (1, 10) + n <- choose (1, 200) pure $ UnsafeContestationPeriod $ wordToNatural n genInit :: [(SigningKey HydraKey, b)] -> Gen (Action WorldState ()) @@ -464,21 +484,27 @@ instance ) => RunModel WorldState (RunMonad m) where - postcondition (_, st) action _l result = pure $ checkOutcome st action result - - monitoring (s, s') action _l result = - decoratePostconditionFailure - . decorateTransitions + postcondition (_, st) action _lookup result = + case action of + (Commit _party expectedCommitted) -> do + decorateFailure st action expectedCommitted result + pure $ expectedCommitted == result + Fanout{} -> + case hydraState st of + Final{finalUTxO} -> do + -- NOTE: Sort `[TxOut]` by the address and values. We want to make + -- sure that the fannout outputs match what we had in the open Head + -- exactly. + let sortByAddressAndValue = sortOn (\o -> (txOutAddress o, selectLovelace (txOutValue o))) + decorateFailure st action (toTxOuts finalUTxO) (toList result) + pure $ + sortByAddressAndValue (toTxOuts finalUTxO) == sortByAddressAndValue (toList result) + _ -> pure False + _ -> pure True + + monitoring (s, s') _action _lookup _result = + decorateTransitions where - -- REVIEW: This should be part of the quickcheck-dynamic runActions - decoratePostconditionFailure - | checkOutcome s action result = id - | otherwise = - counterexample "postcondition failed" - . counterexample ("Action: " <> show action) - . counterexample ("State: " <> show s) - . counterexample ("Result: " <> showFromAction (show result) action) - decorateTransitions = case (hydraState s, hydraState s') of (st, st') -> tabulate "Transitions" [unsafeConstructorName st <> " -> " <> unsafeConstructorName st'] @@ -497,6 +523,8 @@ instance performAbort party Close party -> performClose party + Fanout party -> + performFanout party Wait delay -> lift $ threadDelay delay ObserveConfirmedTx var -> do @@ -513,6 +541,8 @@ instance case find headIsOpen outputs of Just _ -> pure () Nothing -> error "The head is not open for node" + RollbackAndForward numberOfBlocks -> + performRollbackAndForward numberOfBlocks StopTheWorld -> stopTheWorld @@ -587,7 +617,6 @@ performCommit parties party paymentUTxO = do | cp == party -> Just committedUTxO err@CommandFailed{} -> error $ show err _ -> Nothing - pure $ fromUtxo observedUTxO where fromUtxo :: UTxO -> [(CardanoSigningKey, Value)] @@ -605,6 +634,16 @@ performCommit parties party paymentUTxO = do makeAddressFromSigningKey :: CardanoSigningKey -> AddressInEra makeAddressFromSigningKey = mkVkAddress testNetworkId . getVerificationKey . signingKey +toTxOuts :: [(CardanoSigningKey, Value)] -> [TxOut CtxUTxO] +toTxOuts payments = + uncurry mkTxOut <$> payments + where + mkTxOut (CardanoSigningKey sk) val = + TxOut (mkVkAddress testNetworkId (getVerificationKey sk)) val TxOutDatumNone ReferenceScriptNone + +-- | NOTE: This function generates input 'Ix' that start from zero so +-- can't be used with certainty when want to check equality with some 'UTxO' +-- even though the value and the key would match. toRealUTxO :: [(CardanoSigningKey, Value)] -> UTxO toRealUTxO paymentUTxO = UTxO.fromPairs $ @@ -650,11 +689,19 @@ performNewTx party tx = do waitForOpen :: MonadDelay m => TestHydraClient tx m -> RunMonad m () waitForOpen node = do outs <- lift $ serverOutputs node - unless (any headIsOpen outs) $ - waitAndRetry + unless (any headIsOpen outs) waitAndRetry where waitAndRetry = lift (threadDelay 0.1) >> waitForOpen node +-- | Wait for the head to be closed by searching from the beginning. Note that +-- there rollbacks or multiple life-cycles of heads are not handled here. +waitForReadyToFanout :: MonadDelay m => TestHydraClient tx m -> RunMonad m () +waitForReadyToFanout node = do + outs <- lift $ serverOutputs node + unless (any headIsReadyToFanout outs) waitAndRetry + where + waitAndRetry = lift (threadDelay 0.1) >> waitForReadyToFanout node + sendsInput :: (MonadSTM m, MonadThrow m) => Party -> ClientInput Tx -> RunMonad m () sendsInput party command = do nodes <- gets nodes @@ -696,6 +743,30 @@ performClose party = do err@CommandFailed{} -> error $ show err _ -> False +performFanout :: (MonadThrow m, MonadAsync m, MonadDelay m) => Party -> RunMonad m UTxO +performFanout party = do + nodes <- gets nodes + let thisNode = nodes ! party + waitForReadyToFanout thisNode + party `sendsInput` Input.Fanout + findInOutput thisNode (100 :: Int) + where + findInOutput node n + | n == 0 = failure "Failed to perform Fanout" + | otherwise = do + outputs <- lift $ serverOutputs node + case find headIsFinalized outputs of + Just HeadIsFinalized{utxo} -> pure utxo + _ -> lift (threadDelay 1) >> findInOutput node (n - 1) + headIsFinalized = \case + HeadIsFinalized{} -> True + _otherwise -> False + +performRollbackAndForward :: (MonadThrow m, MonadTimer m) => Natural -> RunMonad m () +performRollbackAndForward numberOfBlocks = do + SimulatedChainNetwork{rollbackAndForward} <- gets chain + lift $ rollbackAndForward numberOfBlocks + stopTheWorld :: MonadAsync m => RunMonad m () stopTheWorld = gets threads >>= mapM_ (lift . cancel) @@ -715,16 +786,26 @@ showFromAction k = \case Commit{} -> k Abort{} -> k Close{} -> k + Fanout{} -> k NewTx{} -> k Wait{} -> k ObserveConfirmedTx{} -> k + RollbackAndForward{} -> k StopTheWorld -> k ObserveHeadIsOpen -> k -checkOutcome :: WorldState -> Action WorldState a -> a -> Bool -checkOutcome _st (Commit _party expectedCommitted) actualCommitted = - expectedCommitted == actualCommitted -checkOutcome _ _ _ = True +decorateFailure :: + (Monad m, Show expected, Show actual) => + WorldState -> + Action WorldState a -> + expected -> + actual -> + PostconditionM m () +decorateFailure st action expected actual = do + counterexamplePost ("Action: " <> show action) + counterexamplePost ("State: " <> show st) + counterexamplePost ("Expected: " <> show expected) + counterexamplePost ("Actual: " <> show actual) waitForUTxOToSpend :: forall m. @@ -766,3 +847,8 @@ headIsOpen :: ServerOutput tx -> Bool headIsOpen = \case HeadIsOpen{} -> True _otherwise -> False + +headIsReadyToFanout :: ServerOutput tx -> Bool +headIsReadyToFanout = \case + ReadyToFanout{} -> True + _otherwise -> False diff --git a/hydra-node/test/Hydra/Model/MockChain.hs b/hydra-node/test/Hydra/Model/MockChain.hs index c1b8ad3f971..3e08bd4dc80 100644 --- a/hydra-node/test/Hydra/Model/MockChain.hs +++ b/hydra-node/test/Hydra/Model/MockChain.hs @@ -24,6 +24,8 @@ import Control.Monad.Class.MonadAsync (async, link) import Control.Monad.Class.MonadFork (labelThisThread) import Data.Sequence (Seq (Empty, (:|>))) import Data.Sequence qualified as Seq +import Data.Time (secondsToNominalDiffTime) +import Data.Time.Clock.POSIX (posixSecondsToUTCTime) import Hydra.BehaviorSpec ( SimulatedChainNetwork (..), ) @@ -42,7 +44,7 @@ import Hydra.Chain.Direct.Handlers ( ) import Hydra.Chain.Direct.ScriptRegistry (genScriptRegistry, registryUTxO) import Hydra.Chain.Direct.State (ChainContext (..), initialChainState) -import Hydra.Chain.Direct.TimeHandle (TimeHandle) +import Hydra.Chain.Direct.TimeHandle (TimeHandle, mkTimeHandle) import Hydra.Chain.Direct.Tx (verificationKeyToOnChainId) import Hydra.Chain.Direct.Wallet (TinyWallet (..)) import Hydra.Crypto (HydraKey) @@ -54,7 +56,7 @@ import Hydra.HeadLogic ( import Hydra.HeadLogic.State (ClosedState (..), HeadState (..), IdleState (..), InitialState (..), OpenState (..)) import Hydra.Ledger (ChainSlot (..), Ledger (..), txId) import Hydra.Ledger.Cardano (adjustUTxO, fromChainSlot, genTxOutAdaOnly) -import Hydra.Ledger.Cardano.Evaluate (evaluateTx) +import Hydra.Ledger.Cardano.Evaluate (eraHistoryWithoutHorizon, evaluateTx) import Hydra.Logging (Tracer) import Hydra.Model.Payment (CardanoSigningKey (..)) import Hydra.Network (Network (..)) @@ -62,6 +64,7 @@ import Hydra.Network.Message (Message) import Hydra.Node (HydraNode (..), NodeState (..)) import Hydra.Node.EventQueue (EventQueue (..)) import Hydra.Party (Party (..), deriveParty) +import Test.QuickCheck (getPositive) -- | Create a mocked chain which connects nodes through 'ChainSyncHandler' and -- 'Chain' interfaces. It calls connected chain sync handlers 'onRollForward' on @@ -126,7 +129,7 @@ mockChainAndNetwork tr seedKeys commits = do , ownParty , scriptRegistry } - let getTimeHandle = pure $ arbitrary `generateWith` 42 + let getTimeHandle = pure $ fixedTimeHandleIndefiniteHorizon `generateWith` 42 let HydraNode{eq = EventQueue{putEvent}} = node let -- NOTE: this very simple function put the transaction in a queue for @@ -187,10 +190,7 @@ mockChainAndNetwork tr seedKeys commits = do blockTime = 20 simulateChain nodes chain queue = - forever $ do - rollForward nodes chain queue - rollForward nodes chain queue - rollbackAndForward nodes chain 2 + forever $ rollForward nodes chain queue rollForward nodes chain queue = do threadDelay blockTime @@ -242,6 +242,17 @@ mockChainAndNetwork tr seedKeys commits = do <> show (fst <$> pairs utxo) Right utxo' -> (newSlot, position, blocks :|> (header, transactions, utxo), utxo') +-- | Construct fixed 'TimeHandle' that starts from 0 and has the era horizon far in the future. +-- This is used in our 'Model' tests and we want to make sure the tests finish before +-- the horizon is reached to prevent the 'PastHorizon' exceptions. +fixedTimeHandleIndefiniteHorizon :: Gen TimeHandle +fixedTimeHandleIndefiniteHorizon = do + let startSeconds = 0 + let startTime = posixSecondsToUTCTime $ secondsToNominalDiffTime startSeconds + uptimeSeconds <- getPositive <$> arbitrary + let currentSlotNo = SlotNo $ truncate $ uptimeSeconds + startSeconds + pure $ mkTimeHandle currentSlotNo (SystemStart startTime) eraHistoryWithoutHorizon + -- | A trimmed down ledger whose only purpose is to validate -- on-chain scripts. -- diff --git a/hydra-node/test/Hydra/ModelSpec.hs b/hydra-node/test/Hydra/ModelSpec.hs index 785d7645d7e..5008c03ed60 100644 --- a/hydra-node/test/Hydra/ModelSpec.hs +++ b/hydra-node/test/Hydra/ModelSpec.hs @@ -144,6 +144,7 @@ import Hydra.Party (Party (..), deriveParty) import Test.QuickCheck (Property, Testable, counterexample, forAll, property, withMaxSuccess, within) import Test.QuickCheck.DynamicLogic ( DL, + Quantification, action, anyActions_, forAllDL, @@ -155,6 +156,7 @@ import Test.QuickCheck.DynamicLogic ( ) import Test.QuickCheck.Gen.Unsafe (Capture (Capture), capture) import Test.QuickCheck.Monadic (PropertyM, assert, monadic', monitor, run) +import Test.QuickCheck.Property ((===)) import Test.QuickCheck.StateModel ( ActionWithPolarity (..), Actions, @@ -176,6 +178,35 @@ spec = do prop "implementation respects model" $ forAll arbitrary prop_checkModel prop "check conflict-free liveness" prop_checkConflictFreeLiveness prop "check head opens if all participants commit" prop_checkHeadOpensIfAllPartiesCommit + prop "fanout contains whole confirmed UTxO" prop_fanoutContainsWholeConfirmedUTxO + -- FIXME: implement toRealUTxO correctly so the distributive property holds + xprop "realUTxO is distributive" $ propIsDistributive Model.toRealUTxO + +propIsDistributive :: (Show b, Eq b, Semigroup b) => ([a] -> b) -> [a] -> [a] -> Property +propIsDistributive fn as bs = + fn as <> fn bs === fn (as <> bs) + & counterexample ("fn (as <> bs) " <> show (fn (as <> bs))) + & counterexample ("fn as <> fn bs: " <> show (fn as <> fn bs)) + +prop_fanoutContainsWholeConfirmedUTxO :: Property +prop_fanoutContainsWholeConfirmedUTxO = + forAllDL fanoutContainsWholeConfirmedUTxO prop_HydraModel + +-- | Given any random walk of the model, if the Head is open a NewTx getting +-- confirmed must be part of the UTxO after finalization. +fanoutContainsWholeConfirmedUTxO :: DL WorldState () +fanoutContainsWholeConfirmedUTxO = do + anyActions_ + getModelStateDL >>= \case + st@WorldState{hydraState = Open{}} -> do + (party, payment) <- forAllNonVariableQ (nonConflictingTx st) + tx <- action $ Model.NewTx party payment + eventually (ObserveConfirmedTx tx) + action_ $ Model.Close party + -- NOTE: The check is actually in the Model postcondition for 'Fanout' + void $ action $ Model.Fanout party + _ -> pure () + action_ Model.StopTheWorld prop_checkHeadOpensIfAllPartiesCommit :: Property prop_checkHeadOpensIfAllPartiesCommit = @@ -184,20 +215,38 @@ prop_checkHeadOpensIfAllPartiesCommit = headOpensIfAllPartiesCommit :: DL WorldState () headOpensIfAllPartiesCommit = do - _ <- seedTheWorld - _ <- initHead + seedTheWorld + initHead everybodyCommit - void $ eventually ObserveHeadIsOpen + observeHeadOpened where - eventually a = action (Wait 1000) >> action a - seedTheWorld = forAllQ (withGenQ genSeed (const [])) >>= action + seedTheWorld = do + WorldState{hydraState} <- getModelStateDL + case hydraState of + Start -> + forAllQ (withGenQ genSeed (const [])) >>= action_ + _ -> pure () initHead = do - WorldState{hydraParties} <- getModelStateDL - forAllQ (withGenQ (genInit hydraParties) (const [])) >>= action + WorldState{hydraParties, hydraState} <- getModelStateDL + case hydraState of + -- FIXME: We should be in 'Init' state when doing 'genInit'! + -- Also investigate why do we need to match on the state in all these actions? + Initial{} -> + forAllQ (withGenQ (genInit hydraParties) (const [])) >>= action_ + _ -> pure () everybodyCommit = do - WorldState{hydraParties} <- getModelStateDL - forM_ hydraParties $ \party -> - forAllQ (withGenQ (genCommit' hydraParties party) (const [])) >>= action + WorldState{hydraParties, hydraState} <- getModelStateDL + case hydraState of + Initial{} -> + forM_ hydraParties $ \party -> + forAllQ (withGenQ (genCommit' hydraParties party) (const [])) >>= action + _ -> pure () + observeHeadOpened = do + WorldState{hydraState} <- getModelStateDL + case hydraState of + Open{} -> + void $ eventually ObserveHeadIsOpen + _ -> pure () prop_checkConflictFreeLiveness :: Property prop_checkConflictFreeLiveness = @@ -226,14 +275,6 @@ conflictFreeLiveness = do eventually (ObserveConfirmedTx tx) _ -> pure () action_ Model.StopTheWorld - where - nonConflictingTx st = - withGenQ (genPayment st) (const []) - `whereQ` \(party, tx) -> precondition st (Model.NewTx party tx) - - eventually a = action_ (Wait 10) >> action_ a - - action_ = void . action prop_generateTraces :: Actions WorldState -> Property prop_generateTraces actions = @@ -352,6 +393,17 @@ runIOSimProp p = do , chain = dummySimulatedChainNetwork } +nonConflictingTx :: WorldState -> Quantification (Party, Payment.Payment) +nonConflictingTx st = + withGenQ (genPayment st) (const []) + `whereQ` \(party, tx) -> precondition st (Model.NewTx party tx) + +eventually :: Action WorldState () -> DL WorldState () +eventually a = action_ (Wait 10) >> action_ a + +action_ :: Action WorldState () -> DL WorldState () +action_ = void . action + unwrapAddress :: AddressInEra -> Text unwrapAddress = \case ShelleyAddressInEra addr -> serialiseToBech32 addr