Skip to content

Commit

Permalink
TxTrace: add assertion on fanned out UTxO
Browse files Browse the repository at this point in the history
  • Loading branch information
ch1bo authored and v0d1ch committed May 7, 2024
1 parent 238e479 commit 54e9f77
Showing 1 changed file with 12 additions and 4 deletions.
16 changes: 12 additions & 4 deletions hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ import Cardano.Api.UTxO qualified as UTxO
import Data.List ((\\))
import Data.Map.Strict qualified as Map
import Data.Time.Clock.POSIX (posixSecondsToUTCTime)
import Hydra.Cardano.Api (SlotNo (..), mkTxOutDatumInline)
import Hydra.Cardano.Api (SlotNo (..), mkTxOutDatumInline, renderUTxO)
import Hydra.Cardano.Api.Pretty (renderTxWithUTxO)
import Hydra.Chain.Direct.Contract.Mutation (addParticipationTokens)
import Hydra.Chain.Direct.Fixture qualified as Fixture
Expand Down Expand Up @@ -282,9 +282,17 @@ instance RunModel Model IO where
counterexamplePost $ "Wrong contesters: expected " <> show (alreadyContested modelAfter) <> ", got " <> show contesters
pure $ length contesters == length (alreadyContested modelAfter)
_ -> pure False
Fanout{} -> expectValid result $ \case
Tx.Fanout{} -> pure True
_ -> pure False
Fanout{snapshotNumber} -> do
valid <- expectValid result $ \case
Tx.Fanout{} -> pure True
_ -> pure False
correctlyFannedOut <- case result of
TxResult{newUTxO} -> do
counterexamplePost ("Fanned out UTxO does not match: " <> renderUTxO newUTxO)
counterexamplePost ("SnapshotUTxO: " <> renderUTxO (snapshotUTxO snapshotNumber))
pure $ newUTxO == snapshotUTxO snapshotNumber
-- XXX: PostconditionM does not allow case specific counterexamples like Property(M)
pure $ valid && correctlyFannedOut
_ -> pure True

postconditionOnFailure (modelBefore, _modelAfter) action _lookup result = do
Expand Down

0 comments on commit 54e9f77

Please sign in to comment.