Skip to content

Commit

Permalink
TxTrace: Assert outputs of fanout in postcondition
Browse files Browse the repository at this point in the history
  • Loading branch information
ch1bo authored and v0d1ch committed May 7, 2024
1 parent 30ab1d7 commit a5ba64a
Showing 1 changed file with 12 additions and 5 deletions.
17 changes: 12 additions & 5 deletions hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ import Cardano.Api.UTxO (UTxO)
import Cardano.Api.UTxO qualified as UTxO
import Data.Map.Strict qualified as Map
import Data.Time.Clock.POSIX (posixSecondsToUTCTime)
import Hydra.Cardano.Api (SlotNo (..), mkTxOutDatumInline, renderUTxO)
import Hydra.Cardano.Api (SlotNo (..), mkTxOutDatumInline, renderUTxO, selectLovelace, txOutAddress, txOutValue)
import Hydra.Cardano.Api.Pretty (renderTxWithUTxO)
import Hydra.Chain.Direct.Contract.Mutation (addParticipationTokens)
import Hydra.Chain.Direct.Fixture qualified as Fixture
Expand All @@ -18,7 +18,7 @@ import Hydra.Chain.Direct.Tx qualified as Tx
import Hydra.ContestationPeriod qualified as CP
import Hydra.Contract.HeadState qualified as Head
import Hydra.Crypto (MultiSignature, aggregate, sign)
import Hydra.Ledger (hashUTxO)
import Hydra.Ledger (hashUTxO, utxoFromTx)
import Hydra.Ledger.Cardano (Tx, adjustUTxO, genUTxOFor, genVerificationKey)
import Hydra.Ledger.Cardano.Evaluate (evaluateTx)
import Hydra.Party (partyToChain)
Expand Down Expand Up @@ -112,6 +112,7 @@ data Actor = Alice | Bob | Carol

data TxResult = TxResult
{ newUTxO :: UTxO
, tx :: Tx
, validationError :: Maybe String
, observation :: HeadObservation
}
Expand Down Expand Up @@ -263,10 +264,15 @@ instance RunModel Model IO where
Tx.Fanout{} -> pure True
_ -> pure False
correctlyFannedOut <- case result of
TxResult{newUTxO} -> do
counterexamplePost ("Fanned out UTxO does not match: " <> renderUTxO newUTxO)
TxResult{tx} -> do
-- NOTE: Sort `[TxOut]` by the address and values. We want to make
-- sure that the fanout outputs match what we had in the open Head
-- 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 snapshotNumber))
pure $ newUTxO == snapshotUTxO snapshotNumber
pure $ sorted fannedOut == sorted (snapshotUTxO snapshotNumber)
-- XXX: PostconditionM does not allow case specific counterexamples like Property(M)
pure $ valid && correctlyFannedOut
_ -> pure True
Expand Down Expand Up @@ -445,6 +451,7 @@ performTx utxo tx =
pure
TxResult
{ newUTxO = adjustUTxO tx utxo
, tx
, validationError
, observation = observeHeadTx Fixture.testNetworkId utxo tx
}
Expand Down

0 comments on commit a5ba64a

Please sign in to comment.