{-# LANGUAGE DuplicateRecordFields #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Hydra.Chain.Direct.StateSpec where

import Hydra.Prelude hiding (label)
import Test.Hydra.Prelude

import Cardano.Api.UTxO qualified as UTxO
import Cardano.Binary (serialize)
import Data.ByteString.Lazy qualified as LBS
import Data.Set qualified as Set
import Hydra.Cardano.Api (
  CtxUTxO,
  NetworkId (Mainnet),
  PlutusScriptV2,
  Tx,
  TxIn,
  TxOut,
  UTxO,
  findRedeemerSpending,
  fromPlutusScript,
  genTxIn,
  hashScript,
  isScriptTxOut,
  lovelaceToValue,
  mkScriptAddress,
  modifyTxOutAddress,
  modifyTxOutValue,
  scriptPolicyId,
  toPlutusCurrencySymbol,
  toScriptData,
  txInputSet,
  txIns',
  txOutValue,
  txOuts',
  utxoFromTx,
  valueSize,
  pattern PlutusScript,
  pattern PlutusScriptSerialised,
 )
import Hydra.Cardano.Api.Pretty (renderTx, renderTxWithUTxO)
import Hydra.Chain (OnChainTx (..), PostTxError (..), maxMainnetLovelace, maximumNumberOfParties)
import Hydra.Chain.Direct.State (
  ChainContext (..),
  ChainState (..),
  ClosedState (..),
  HasKnownUTxO (getKnownUTxO),
  HydraContext (..),
  InitialState (..),
  OpenState (..),
  abort,
  closedThreadOutput,
  commit,
  ctxHeadParameters,
  ctxParticipants,
  ctxParties,
  genChainStateWithTx,
  genCloseTx,
  genCollectComTx,
  genCommitFor,
  genCommits,
  genCommits',
  genContestTx,
  genDecrementTx,
  genFanoutTx,
  genHydraContext,
  genInitTx,
  genStInitial,
  getContestationDeadline,
  getKnownUTxO,
  initialize,
  observeClose,
  observeCollect,
  observeCommit,
  pickChainContext,
  unsafeAbort,
  unsafeClose,
  unsafeCollect,
  unsafeCommit,
  unsafeFanout,
  unsafeObserveInitAndCommits,
 )
import Hydra.Chain.Direct.State qualified as Transition
import Hydra.Chain.Direct.Tx (AbortObservation (..), CloseObservation (..), CollectComObservation (..), CommitObservation (..), ContestObservation (..), DecrementObservation (..), FanoutObservation (..), HeadObservation (..), NotAnInitReason (..), observeCommitTx, observeDecrementTx, observeHeadTx, observeInitTx)
import Hydra.Contract.HeadTokens qualified as HeadTokens
import Hydra.Contract.Initial qualified as Initial
import Hydra.Ledger.Cardano (
  genTxOut,
  genTxOutByron,
 )
import Hydra.Ledger.Cardano.Evaluate (
  evaluateTx,
  genValidityBoundsFromContestationPeriod,
  maxTxSize,
  propTransactionEvaluates,
  propTransactionFailsEvaluation,
 )
import Hydra.Ledger.Cardano.Time (slotNoFromUTCTime)
import Hydra.Tx.Contest (ClosedThreadOutput (closedContesters))
import Hydra.Tx.ContestationPeriod (toNominalDiffTime)
import Hydra.Tx.Snapshot (ConfirmedSnapshot (InitialSnapshot, initialUTxO))
import Hydra.Tx.Snapshot qualified as Snapshot
import Hydra.Tx.Utils (splitUTxO)
import PlutusLedgerApi.Test.Examples qualified as Plutus
import PlutusLedgerApi.V2 qualified as Plutus
import Test.Aeson.GenericSpecs (roundtripAndGoldenSpecs)
import Test.Hydra.Tx.Fixture (slotLength, systemStart, testNetworkId)
import Test.Hydra.Tx.Gen (genOutput, genTxOutAdaOnly, genUTxO1, genUTxOSized)
import Test.Hydra.Tx.Mutation (
  Mutation (..),
  applyMutation,
  modifyInlineDatum,
  replaceHeadId,
  replacePolicyIdWith,
 )
import Test.QuickCheck (
  Property,
  Testable (property),
  checkCoverage,
  classify,
  conjoin,
  counterexample,
  cover,
  forAll,
  forAllBlind,
  forAllShow,
  forAllShrink,
  getPositive,
  label,
  sized,
  sublistOf,
  tabulate,
  (.&&.),
  (.||.),
  (===),
  (==>),
 )
import Test.QuickCheck.Monadic (monadicIO, monadicST, pick)
import Prelude qualified

spec :: Spec
spec :: Spec
spec = Spec -> Spec
forall a. SpecWith a -> SpecWith a
parallel (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
  Proxy PubKeyHash -> Spec
forall a.
(Arbitrary a, ToJSON a, FromJSON a, Typeable a) =>
Proxy a -> Spec
roundtripAndGoldenSpecs (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Plutus.PubKeyHash)

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"observeTx" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"All valid transitions for all possible states can be observed." Property
prop_observeAnyTx

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"splitUTxO" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> (UTxO -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"it splits at least one utxo off" UTxO -> Property
prop_splitUTxO

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"init" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    Natural -> ((UTxO -> Tx -> Property) -> Property) -> Spec
propBelowSizeLimit Natural
maxTxSize (UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllInit
    ((UTxO -> Tx -> Property) -> Property) -> Spec
propIsValid (UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllInit

    -- XXX: This is testing observeInitTx (we will get rid of 'observeInit')
    String -> Property -> SpecWith (Arg Property)
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"only proper head is observed" (Property -> SpecWith (Arg Property))
-> Property -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$
      PropertyM IO Property -> Property
forall a. Testable a => PropertyM IO a -> Property
monadicIO (PropertyM IO Property -> Property)
-> PropertyM IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
        HydraContext
ctx <- Gen HydraContext -> PropertyM IO HydraContext
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Int -> Gen HydraContext
genHydraContext Int
maximumNumberOfParties)
        ChainContext
cctx <- Gen ChainContext -> PropertyM IO ChainContext
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen ChainContext -> PropertyM IO ChainContext)
-> Gen ChainContext -> PropertyM IO ChainContext
forall a b. (a -> b) -> a -> b
$ HydraContext -> Gen ChainContext
pickChainContext HydraContext
ctx
        TxIn
seedInput <- Gen TxIn -> PropertyM IO TxIn
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind Gen TxIn
forall a. Arbitrary a => Gen a
arbitrary
        VerificationKey PaymentKey
vk <- Gen (VerificationKey PaymentKey)
-> PropertyM IO (VerificationKey PaymentKey)
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind Gen (VerificationKey PaymentKey)
forall a. Arbitrary a => Gen a
arbitrary
        TxOut CtxUTxO
seedTxOut <- Gen (TxOut CtxUTxO) -> PropertyM IO (TxOut CtxUTxO)
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen (TxOut CtxUTxO) -> PropertyM IO (TxOut CtxUTxO))
-> Gen (TxOut CtxUTxO) -> PropertyM IO (TxOut CtxUTxO)
forall a b. (a -> b) -> a -> b
$ VerificationKey PaymentKey -> Gen (TxOut CtxUTxO)
forall ctx. VerificationKey PaymentKey -> Gen (TxOut ctx)
genTxOutAdaOnly VerificationKey PaymentKey
vk

        let tx :: Tx
tx = ChainContext -> TxIn -> [OnChainId] -> HeadParameters -> Tx
initialize ChainContext
cctx TxIn
seedInput (HydraContext -> [OnChainId]
ctxParticipants HydraContext
ctx) (HydraContext -> HeadParameters
ctxHeadParameters HydraContext
ctx)
        (Mutation
mutation, String
cex, NotAnInitReason
expected) <- Gen (Mutation, String, NotAnInitReason)
-> PropertyM IO (Mutation, String, NotAnInitReason)
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen (Mutation, String, NotAnInitReason)
 -> PropertyM IO (Mutation, String, NotAnInitReason))
-> Gen (Mutation, String, NotAnInitReason)
-> PropertyM IO (Mutation, String, NotAnInitReason)
forall a b. (a -> b) -> a -> b
$ TxIn -> Tx -> Gen (Mutation, String, NotAnInitReason)
genInitTxMutation TxIn
seedInput Tx
tx
        let utxo :: UTxO
utxo = (TxIn, TxOut CtxUTxO) -> UTxO
forall out. (TxIn, out) -> UTxO' out
UTxO.singleton (TxIn
seedInput, TxOut CtxUTxO
seedTxOut)
        let (Tx
tx', UTxO
utxo') = Mutation -> (Tx, UTxO) -> (Tx, UTxO)
applyMutation Mutation
mutation (Tx
tx, UTxO
utxo)

            originalIsObserved :: Property
originalIsObserved = Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Either NotAnInitReason InitObservation -> Bool
forall a b. Either a b -> Bool
isRight (Tx -> Either NotAnInitReason InitObservation
observeInitTx Tx
tx)

            -- We expected mutated transaction to still be valid, but not observed.
            mutatedIsValid :: Property
mutatedIsValid = Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$
              case Tx -> UTxO -> Either EvaluationError EvaluationReport
evaluateTx Tx
tx' UTxO
utxo' of
                Left EvaluationError
_ -> Bool
False
                Right EvaluationReport
ok
                  | (Either ScriptExecutionError ExecutionUnits -> Bool)
-> EvaluationReport -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Either ScriptExecutionError ExecutionUnits -> Bool
forall a b. Either a b -> Bool
isRight EvaluationReport
ok -> Bool
True
                  | Bool
otherwise -> Bool
False

            mutatedIsNotObserved :: Property
mutatedIsNotObserved =
              Tx -> Either NotAnInitReason InitObservation
observeInitTx Tx
tx' Either NotAnInitReason InitObservation
-> Either NotAnInitReason InitObservation -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== NotAnInitReason -> Either NotAnInitReason InitObservation
forall a b. a -> Either a b
Left NotAnInitReason
expected

        Property -> PropertyM IO Property
forall a. a -> PropertyM IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> PropertyM IO Property)
-> Property -> PropertyM IO Property
forall a b. (a -> b) -> a -> b
$
          [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
            [ Property
originalIsObserved
                Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Tx -> String
renderTx Tx
tx)
                Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"Original transaction is not observed."
            , Property
mutatedIsValid
                Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Tx -> String
renderTx Tx
tx')
                Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"Mutated transaction is not valid."
            , Property
mutatedIsNotObserved
                Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Tx -> String
renderTx Tx
tx')
                Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"Should not observe mutated transaction"
            ]
            Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
cex
            Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
label (NotAnInitReason -> String
forall b a. (Show a, IsString b) => a -> b
show NotAnInitReason
expected)

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"commit" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    Natural -> ((UTxO -> Tx -> Property) -> Property) -> Spec
propBelowSizeLimit Natural
maxTxSize (UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllCommit
    ((UTxO -> Tx -> Property) -> Property) -> Spec
propIsValid (UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllCommit

    -- XXX: This is testing observeCommitTx. Eventually we will get rid of the
    -- state-ful layer anyways.
    String -> Property -> SpecWith (Arg Property)
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"only proper head is observed" (Property -> SpecWith (Arg Property))
-> Property -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$
      (ChainContext -> InitialState -> UTxO -> Tx -> Property)
-> Property
forall property.
Testable property =>
(ChainContext -> InitialState -> UTxO -> Tx -> property)
-> Property
forAllCommit' ((ChainContext -> InitialState -> UTxO -> Tx -> Property)
 -> Property)
-> (ChainContext -> InitialState -> UTxO -> Tx -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \ChainContext
ctx InitialState
st UTxO
committedUtxo Tx
tx ->
        PropertyM IO Property -> Property
forall a. Testable a => PropertyM IO a -> Property
monadicIO (PropertyM IO Property -> Property)
-> PropertyM IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
          let utxo :: UTxO
utxo = ChainContext -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainContext
ctx UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> InitialState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO InitialState
st UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> UTxO
committedUtxo
          Mutation
mutation <- Gen Mutation -> PropertyM IO Mutation
forall (m :: * -> *) a. (Monad m, Show a) => Gen a -> PropertyM m a
pick (Gen Mutation -> PropertyM IO Mutation)
-> Gen Mutation -> PropertyM IO Mutation
forall a b. (a -> b) -> a -> b
$ UTxO -> Tx -> Gen Mutation
genCommitTxMutation UTxO
utxo Tx
tx
          let (Tx
tx', UTxO
utxo') = Mutation -> (Tx, UTxO) -> (Tx, UTxO)
applyMutation Mutation
mutation (Tx
tx, UTxO
utxo)

              originalIsObserved :: Property
originalIsObserved = Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Maybe CommitObservation -> Bool
forall a. Maybe a -> Bool
isJust (Maybe CommitObservation -> Bool)
-> Maybe CommitObservation -> Bool
forall a b. (a -> b) -> a -> b
$ NetworkId -> UTxO -> Tx -> Maybe CommitObservation
observeCommitTx NetworkId
testNetworkId UTxO
utxo Tx
tx

              -- We expected mutated transaction to still be valid, but not observed.
              mutatedIsValid :: Property
mutatedIsValid =
                case Tx -> UTxO -> Either EvaluationError EvaluationReport
evaluateTx Tx
tx' UTxO
utxo' of
                  Left EvaluationError
err -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (EvaluationError -> String
forall b a. (Show a, IsString b) => a -> b
show EvaluationError
err)
                  Right EvaluationReport
ok
                    | (Either ScriptExecutionError ExecutionUnits -> Bool)
-> EvaluationReport -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Either ScriptExecutionError ExecutionUnits -> Bool
forall a b. Either a b -> Bool
isRight EvaluationReport
ok -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
                    | Bool
otherwise -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (EvaluationReport -> String
forall b a. (Show a, IsString b) => a -> b
show EvaluationReport
ok)

              mutatedIsNotObserved :: Bool
mutatedIsNotObserved =
                Maybe CommitObservation -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe CommitObservation -> Bool)
-> Maybe CommitObservation -> Bool
forall a b. (a -> b) -> a -> b
$ NetworkId -> UTxO -> Tx -> Maybe CommitObservation
observeCommitTx NetworkId
testNetworkId UTxO
utxo' Tx
tx'

          Property -> PropertyM IO Property
forall a. a -> PropertyM IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> PropertyM IO Property)
-> Property -> PropertyM IO Property
forall a b. (a -> b) -> a -> b
$
            [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
              [ Property
originalIsObserved
                  Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Tx -> String
renderTx Tx
tx)
                  Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"Original transaction is not observed."
              , Property
mutatedIsValid
                  Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Tx -> String
renderTx Tx
tx')
                  Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"Mutated transaction is not valid."
              , Bool
mutatedIsNotObserved
                  Bool -> (Bool -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Tx -> String
renderTx Tx
tx')
                  Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"Should not observe mutated transaction"
              ]

    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"consumes all inputs that are committed" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      (ChainContext -> InitialState -> UTxO -> Tx -> Bool) -> Property
forall property.
Testable property =>
(ChainContext -> InitialState -> UTxO -> Tx -> property)
-> Property
forAllCommit' ((ChainContext -> InitialState -> UTxO -> Tx -> Bool) -> Property)
-> (ChainContext -> InitialState -> UTxO -> Tx -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \ChainContext
ctx InitialState
st UTxO
_ Tx
tx ->
        case ChainContext
-> InitialState -> Tx -> Maybe (OnChainTx Tx, InitialState)
observeCommit ChainContext
ctx InitialState
st Tx
tx of
          Just (OnChainTx Tx
_, InitialState
st') ->
            let knownInputs :: Set TxIn
knownInputs = UTxO -> Set TxIn
forall out. UTxO' out -> Set TxIn
UTxO.inputSet (InitialState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO InitialState
st')
             in Set TxIn
knownInputs Set TxIn -> Set TxIn -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.disjoint` Tx -> Set TxIn
forall era. Tx era -> Set TxIn
txInputSet Tx
tx
          Maybe (OnChainTx Tx, InitialState)
Nothing ->
            Bool
False

    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"can only be applied / observed once" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      (ChainContext -> InitialState -> UTxO -> Tx -> Bool) -> Property
forall property.
Testable property =>
(ChainContext -> InitialState -> UTxO -> Tx -> property)
-> Property
forAllCommit' ((ChainContext -> InitialState -> UTxO -> Tx -> Bool) -> Property)
-> (ChainContext -> InitialState -> UTxO -> Tx -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \ChainContext
ctx InitialState
st UTxO
_ Tx
tx ->
        case ChainContext
-> InitialState -> Tx -> Maybe (OnChainTx Tx, InitialState)
observeCommit ChainContext
ctx InitialState
st Tx
tx of
          Just (OnChainTx Tx
_, InitialState
st') ->
            case ChainContext
-> InitialState -> Tx -> Maybe (OnChainTx Tx, InitialState)
observeCommit ChainContext
ctx InitialState
st' Tx
tx of
              Just{} -> Bool
False
              Maybe (OnChainTx Tx, InitialState)
Nothing -> Bool
True
          Maybe (OnChainTx Tx, InitialState)
Nothing ->
            Bool
False

    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"reject committing outputs with byron addresses" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      (forall s. PropertyM (ST s) Property) -> Property
forall a. Testable a => (forall s. PropertyM (ST s) a) -> Property
monadicST ((forall s. PropertyM (ST s) Property) -> Property)
-> (forall s. PropertyM (ST s) Property) -> Property
forall a b. (a -> b) -> a -> b
$ do
        HydraContext
hctx <- Gen HydraContext -> PropertyM (ST s) HydraContext
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen HydraContext -> PropertyM (ST s) HydraContext)
-> Gen HydraContext -> PropertyM (ST s) HydraContext
forall a b. (a -> b) -> a -> b
$ Int -> Gen HydraContext
genHydraContext Int
maximumNumberOfParties
        (ChainContext
ctx, stInitial :: InitialState
stInitial@InitialState{HeadId
headId :: HeadId
$sel:headId:InitialState :: InitialState -> HeadId
headId}) <- Gen (ChainContext, InitialState)
-> PropertyM (ST s) (ChainContext, InitialState)
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen (ChainContext, InitialState)
 -> PropertyM (ST s) (ChainContext, InitialState))
-> Gen (ChainContext, InitialState)
-> PropertyM (ST s) (ChainContext, InitialState)
forall a b. (a -> b) -> a -> b
$ HydraContext -> Gen (ChainContext, InitialState)
genStInitial HydraContext
hctx
        UTxO
utxo <- Gen UTxO -> PropertyM (ST s) UTxO
forall (m :: * -> *) a. (Monad m, Show a) => Gen a -> PropertyM m a
pick (Gen UTxO -> PropertyM (ST s) UTxO)
-> Gen UTxO -> PropertyM (ST s) UTxO
forall a b. (a -> b) -> a -> b
$ Gen (TxOut CtxUTxO) -> Gen UTxO
genUTxO1 Gen (TxOut CtxUTxO)
forall ctx. Gen (TxOut ctx)
genTxOutByron
        Property -> PropertyM (ST s) Property
forall a. a -> PropertyM (ST s) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> PropertyM (ST s) Property)
-> Property -> PropertyM (ST s) Property
forall a b. (a -> b) -> a -> b
$
          case ChainContext
-> HeadId -> UTxO -> UTxO -> Either (PostTxError Tx) Tx
commit ChainContext
ctx HeadId
headId (InitialState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO InitialState
stInitial) UTxO
utxo of
            Left UnsupportedLegacyOutput{} -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
            Either (PostTxError Tx) Tx
_ -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False

    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"reject Commits with more than maxMainnetLovelace Lovelace" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      (forall s. PropertyM (ST s) Property) -> Property
forall a. Testable a => (forall s. PropertyM (ST s) a) -> Property
monadicST ((forall s. PropertyM (ST s) Property) -> Property)
-> (forall s. PropertyM (ST s) Property) -> Property
forall a b. (a -> b) -> a -> b
$ do
        HydraContext
hctx <- Gen HydraContext -> PropertyM (ST s) HydraContext
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen HydraContext -> PropertyM (ST s) HydraContext)
-> Gen HydraContext -> PropertyM (ST s) HydraContext
forall a b. (a -> b) -> a -> b
$ Int -> Gen HydraContext
genHydraContext Int
maximumNumberOfParties
        (ChainContext
ctx, stInitial :: InitialState
stInitial@InitialState{HeadId
$sel:headId:InitialState :: InitialState -> HeadId
headId :: HeadId
headId}) <- Gen (ChainContext, InitialState)
-> PropertyM (ST s) (ChainContext, InitialState)
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen (ChainContext, InitialState)
 -> PropertyM (ST s) (ChainContext, InitialState))
-> Gen (ChainContext, InitialState)
-> PropertyM (ST s) (ChainContext, InitialState)
forall a b. (a -> b) -> a -> b
$ HydraContext -> Gen (ChainContext, InitialState)
genStInitial HydraContext
hctx
        UTxO
utxo <- Gen UTxO -> PropertyM (ST s) UTxO
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind Gen UTxO
genAdaOnlyUTxOOnMainnetWithAmountBiggerThanOutLimit
        let mainnetChainContext :: ChainContext
mainnetChainContext = ChainContext
ctx{networkId = Mainnet}
        Property -> PropertyM (ST s) Property
forall a. a -> PropertyM (ST s) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> PropertyM (ST s) Property)
-> Property -> PropertyM (ST s) Property
forall a b. (a -> b) -> a -> b
$
          case ChainContext
-> HeadId -> UTxO -> UTxO -> Either (PostTxError Tx) Tx
commit ChainContext
mainnetChainContext HeadId
headId (InitialState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO InitialState
stInitial) UTxO
utxo of
            Left CommittedTooMuchADAForMainnet{Coin
userCommittedLovelace :: Coin
$sel:userCommittedLovelace:NoSeedInput :: forall tx. PostTxError tx -> Coin
userCommittedLovelace, Coin
mainnetLimitLovelace :: Coin
$sel:mainnetLimitLovelace:NoSeedInput :: forall tx. PostTxError tx -> Coin
mainnetLimitLovelace} ->
              -- check that user committed more than our limit but also use 'maxMainnetLovelace'
              -- to be sure we didn't construct 'CommittedTooMuchADAForMainnet' wrongly
              Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Coin
userCommittedLovelace Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
> Coin
mainnetLimitLovelace Bool -> Bool -> Bool
&& Coin
userCommittedLovelace Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
> Coin
maxMainnetLovelace
            Either (PostTxError Tx) Tx
_ -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"abort" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    Natural -> ((UTxO -> Tx -> Property) -> Property) -> Spec
propBelowSizeLimit Natural
maxTxSize (UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllAbort
    ((UTxO -> Tx -> Property) -> Property) -> Spec
propIsValid (UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllAbort

    -- XXX: This is something we should test for all tx creation functions.
    -- Maybe extend the forAllXXX generators to work on artificially duplicated,
    -- compatible UTxOs.
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"can create valid abort transactions for any observed head" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      (forall s. PropertyM (ST s) Property) -> Property
forall a. Testable a => (forall s. PropertyM (ST s) a) -> Property
monadicST ((forall s. PropertyM (ST s) Property) -> Property)
-> (forall s. PropertyM (ST s) Property) -> Property
forall a b. (a -> b) -> a -> b
$ do
        HydraContext
hctx <- Gen HydraContext -> PropertyM (ST s) HydraContext
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen HydraContext -> PropertyM (ST s) HydraContext)
-> Gen HydraContext -> PropertyM (ST s) HydraContext
forall a b. (a -> b) -> a -> b
$ Int -> Gen HydraContext
genHydraContext Int
maximumNumberOfParties
        ChainContext
ctx <- Gen ChainContext -> PropertyM (ST s) ChainContext
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen ChainContext -> PropertyM (ST s) ChainContext)
-> Gen ChainContext -> PropertyM (ST s) ChainContext
forall a b. (a -> b) -> a -> b
$ HydraContext -> Gen ChainContext
pickChainContext HydraContext
hctx
        -- Generate a head in initialized state
        (Tx
initTx1, TxIn
seed1) <- Gen (Tx, TxIn) -> PropertyM (ST s) (Tx, TxIn)
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen (Tx, TxIn) -> PropertyM (ST s) (Tx, TxIn))
-> Gen (Tx, TxIn) -> PropertyM (ST s) (Tx, TxIn)
forall a b. (a -> b) -> a -> b
$ HydraContext -> Gen (Tx, TxIn)
genInitTxWithSeed HydraContext
hctx
        -- Generate another head in initialized state
        (Tx
initTx2, TxIn
seed2) <- Gen (Tx, TxIn) -> PropertyM (ST s) (Tx, TxIn)
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen (Tx, TxIn) -> PropertyM (ST s) (Tx, TxIn))
-> Gen (Tx, TxIn) -> PropertyM (ST s) (Tx, TxIn)
forall a b. (a -> b) -> a -> b
$ HydraContext -> Gen (Tx, TxIn)
genInitTxWithSeed HydraContext
hctx
        -- Expect to create abort transactions for either head
        let utxo :: UTxO
utxo = ChainContext -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainContext
ctx UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> Tx -> UTxO
utxoFromTx Tx
initTx1 UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> Tx -> UTxO
utxoFromTx Tx
initTx2
        let propIsValidAbortTx :: Either AbortTxError Tx -> Property
propIsValidAbortTx Either AbortTxError Tx
res =
              case Either AbortTxError Tx
res of
                Left AbortTxError
err -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Failed to create abort: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> AbortTxError -> String
forall b a. (Show a, IsString b) => a -> b
show AbortTxError
err)
                Right Tx
tx -> (Tx, UTxO) -> Property
propTransactionEvaluates (Tx
tx, UTxO
utxo)
        Property -> PropertyM (ST s) Property
forall a. a -> PropertyM (ST s) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> PropertyM (ST s) Property)
-> Property -> PropertyM (ST s) Property
forall a b. (a -> b) -> a -> b
$
          [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
            [ Either AbortTxError Tx -> Property
propIsValidAbortTx (ChainContext -> TxIn -> UTxO -> UTxO -> Either AbortTxError Tx
abort ChainContext
ctx TxIn
seed1 UTxO
utxo UTxO
forall a. Monoid a => a
mempty)
                Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"AbortTx of head 1"
            , Either AbortTxError Tx -> Property
propIsValidAbortTx (ChainContext -> TxIn -> UTxO -> UTxO -> Either AbortTxError Tx
abort ChainContext
ctx TxIn
seed2 UTxO
utxo UTxO
forall a. Monoid a => a
mempty)
                Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"AbortTx of head 2"
            ]

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"collectCom" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    Natural -> ((UTxO -> Tx -> Property) -> Property) -> Spec
propBelowSizeLimit Natural
maxTxSize (UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllCollectCom
    ((UTxO -> Tx -> Property) -> Property) -> Spec
propIsValid (UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllCollectCom

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"decrement" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    Natural -> ((UTxO -> Tx -> Property) -> Property) -> Spec
propBelowSizeLimit Natural
maxTxSize (UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllDecrement
    ((UTxO -> Tx -> Property) -> Property) -> Spec
propIsValid (UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllDecrement

    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"observes distributed outputs" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      ([TxOut CtxUTxO] -> UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
([TxOut CtxUTxO] -> UTxO -> Tx -> property) -> Property
forAllDecrement' (([TxOut CtxUTxO] -> UTxO -> Tx -> Property) -> Property)
-> ([TxOut CtxUTxO] -> UTxO -> Tx -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \[TxOut CtxUTxO]
toDistribute UTxO
utxo Tx
tx ->
        case UTxO -> Tx -> Maybe DecrementObservation
observeDecrementTx UTxO
utxo Tx
tx of
          Just DecrementObservation{[TxOut CtxUTxO]
distributedOutputs :: [TxOut CtxUTxO]
$sel:distributedOutputs:DecrementObservation :: DecrementObservation -> [TxOut CtxUTxO]
distributedOutputs} ->
            [TxOut CtxUTxO]
distributedOutputs [TxOut CtxUTxO] -> [TxOut CtxUTxO] -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== [TxOut CtxUTxO]
toDistribute
          Maybe DecrementObservation
Nothing ->
            Bool
False Bool -> (Bool -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"observeDecrementTx ignored transaction: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> UTxO -> Tx -> String
renderTxWithUTxO UTxO
utxo Tx
tx)

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"close" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    Natural -> ((UTxO -> Tx -> Property) -> Property) -> Spec
propBelowSizeLimit Natural
maxTxSize (UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllClose
    ((UTxO -> Tx -> Property) -> Property) -> Spec
propIsValid (UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllClose

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"contest" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    Natural -> ((UTxO -> Tx -> Property) -> Property) -> Spec
propBelowSizeLimit Natural
maxTxSize (UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllContest
    ((UTxO -> Tx -> Property) -> Property) -> Spec
propIsValid (UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllContest

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"fanout" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    Natural -> ((UTxO -> Tx -> Property) -> Property) -> Spec
propBelowSizeLimit Natural
maxTxSize (UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllFanout
    ((UTxO -> Tx -> Property) -> Property) -> Spec
propIsValid (UTxO -> Tx -> Property) -> Property
forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllFanout

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"acceptance" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> Property -> SpecWith (Arg Property)
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"can close & fanout every collected head" (Property -> SpecWith (Arg Property))
-> Property -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ do
      Property
prop_canCloseFanoutEveryCollect

genInitTxMutation :: TxIn -> Tx -> Gen (Mutation, String, NotAnInitReason)
genInitTxMutation :: TxIn -> Tx -> Gen (Mutation, String, NotAnInitReason)
genInitTxMutation TxIn
seedInput Tx
tx =
  Gen (Mutation, String, NotAnInitReason)
genChangeMintingPolicy
 where
  genChangeMintingPolicy :: Gen (Mutation, String, NotAnInitReason)
genChangeMintingPolicy =
    (Mutation, String, NotAnInitReason)
-> Gen (Mutation, String, NotAnInitReason)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( [Mutation] -> Mutation
Changes ([Mutation] -> Mutation) -> [Mutation] -> Mutation
forall a b. (a -> b) -> a -> b
$
          PlutusScript -> Mutation
ChangeMintingPolicy PlutusScript
alwaysSucceedsV2
            Mutation -> [Mutation] -> [Mutation]
forall a. a -> [a] -> [a]
: ((TxOut CtxTx, Word) -> Mutation)
-> [(TxOut CtxTx, Word)] -> [Mutation]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TxOut CtxTx, Word) -> Mutation
changeMintingPolicy ([TxOut CtxTx] -> [Word] -> [(TxOut CtxTx, Word)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TxOut CtxTx]
changedOutputsValue [Word
0 ..])
      , String
"new minting policy: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> ScriptHash -> String
forall b a. (Show a, IsString b) => a -> b
show (Script PlutusScriptV2 -> ScriptHash
forall lang. Script lang -> ScriptHash
hashScript (Script PlutusScriptV2 -> ScriptHash)
-> Script PlutusScriptV2 -> ScriptHash
forall a b. (a -> b) -> a -> b
$ PlutusScript -> Script PlutusScriptV2
PlutusScript PlutusScript
alwaysSucceedsV2)
      , NotAnInitReason
NotAHeadPolicy
      )

  -- We do replace the minting policy of all tokens and datum of a head output to
  -- simulate a faked init transaction.
  alwaysSucceedsV2 :: PlutusScript
alwaysSucceedsV2 = ShortByteString -> PlutusScript
PlutusScriptSerialised (ShortByteString -> PlutusScript)
-> ShortByteString -> PlutusScript
forall a b. (a -> b) -> a -> b
$ Natural -> ShortByteString
Plutus.alwaysSucceedingNAryFunction Natural
2
  originalPolicyId :: PolicyId
originalPolicyId = TxIn -> PolicyId
HeadTokens.headPolicyId TxIn
seedInput
  fakePolicyId :: PolicyId
fakePolicyId = Script PlutusScriptV2 -> PolicyId
forall lang. Script lang -> PolicyId
scriptPolicyId (Script PlutusScriptV2 -> PolicyId)
-> Script PlutusScriptV2 -> PolicyId
forall a b. (a -> b) -> a -> b
$ PlutusScript -> Script PlutusScriptV2
PlutusScript PlutusScript
alwaysSucceedsV2
  changeMintingPolicy :: (TxOut CtxTx, Word) -> Mutation
changeMintingPolicy (TxOut CtxTx
out, Word
idx)
    | Word
idx Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0 = Word -> TxOut CtxTx -> Mutation
ChangeOutput Word
idx (TxOut CtxTx -> Mutation) -> TxOut CtxTx -> Mutation
forall a b. (a -> b) -> a -> b
$ (State -> State) -> TxOut CtxTx -> TxOut CtxTx
forall a.
(FromScriptData a, ToScriptData a) =>
(a -> a) -> TxOut CtxTx -> TxOut CtxTx
modifyInlineDatum (CurrencySymbol -> State -> State
replaceHeadId (CurrencySymbol -> State -> State)
-> CurrencySymbol -> State -> State
forall a b. (a -> b) -> a -> b
$ PolicyId -> CurrencySymbol
toPlutusCurrencySymbol PolicyId
fakePolicyId) TxOut CtxTx
out
    | Bool
otherwise = Word -> TxOut CtxTx -> Mutation
ChangeOutput Word
idx TxOut CtxTx
out
  changedOutputsValue :: [TxOut CtxTx]
changedOutputsValue = PolicyId -> PolicyId -> TxOut CtxTx -> TxOut CtxTx
forall a. PolicyId -> PolicyId -> TxOut a -> TxOut a
replacePolicyIdWith PolicyId
originalPolicyId PolicyId
fakePolicyId (TxOut CtxTx -> TxOut CtxTx) -> [TxOut CtxTx] -> [TxOut CtxTx]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tx -> [TxOut CtxTx]
forall era. Tx era -> [TxOut CtxTx era]
txOuts' Tx
tx

genCommitTxMutation :: UTxO -> Tx -> Gen Mutation
genCommitTxMutation :: UTxO -> Tx -> Gen Mutation
genCommitTxMutation UTxO
utxo Tx
tx =
  Gen Mutation
mutateInitialAddress
 where
  mutateInitialAddress :: Gen Mutation
mutateInitialAddress = do
    let mutatedTxOut :: TxOut CtxUTxO
mutatedTxOut = (AddressInEra Era -> AddressInEra Era)
-> TxOut CtxUTxO -> TxOut CtxUTxO
forall era ctx.
(AddressInEra era -> AddressInEra era)
-> TxOut ctx era -> TxOut ctx era
modifyTxOutAddress (AddressInEra Era -> AddressInEra Era -> AddressInEra Era
forall a b. a -> b -> a
const AddressInEra Era
fakeScriptAddress) TxOut CtxUTxO
initialTxOut
    Mutation -> Gen Mutation
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Mutation -> Gen Mutation) -> Mutation -> Gen Mutation
forall a b. (a -> b) -> a -> b
$
      [Mutation] -> Mutation
Changes
        [ TxIn -> TxOut CtxUTxO -> Maybe HashableScriptData -> Mutation
ChangeInput TxIn
initialTxIn TxOut CtxUTxO
mutatedTxOut (HashableScriptData -> Maybe HashableScriptData
forall a. a -> Maybe a
Just (HashableScriptData -> Maybe HashableScriptData)
-> HashableScriptData -> Maybe HashableScriptData
forall a b. (a -> b) -> a -> b
$ RedeemerType -> HashableScriptData
forall a. ToScriptData a => a -> HashableScriptData
toScriptData RedeemerType
initialRedeemer)
        , PlutusScript -> Mutation
AddScript PlutusScript
forall {lang}. PlutusScript lang
fakeScript
        ]

  (TxIn
initialTxIn, TxOut CtxUTxO
initialTxOut) =
    (TxIn, TxOut CtxUTxO)
-> Maybe (TxIn, TxOut CtxUTxO) -> (TxIn, TxOut CtxUTxO)
forall a. a -> Maybe a -> a
fromMaybe (Text -> (TxIn, TxOut CtxUTxO)
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"not found initial script") (Maybe (TxIn, TxOut CtxUTxO) -> (TxIn, TxOut CtxUTxO))
-> Maybe (TxIn, TxOut CtxUTxO) -> (TxIn, TxOut CtxUTxO)
forall a b. (a -> b) -> a -> b
$
      (TxOut CtxUTxO -> Bool) -> UTxO -> Maybe (TxIn, TxOut CtxUTxO)
forall out. (out -> Bool) -> UTxO' out -> Maybe (TxIn, out)
UTxO.find (forall lang ctx era.
IsPlutusScriptLanguage lang =>
PlutusScript lang -> TxOut ctx era -> Bool
isScriptTxOut @PlutusScriptV2 PlutusScript
forall {lang}. PlutusScript lang
initialScript) UTxO
resolvedInputs

  resolvedInputs :: UTxO
resolvedInputs =
    [(TxIn, TxOut CtxUTxO)] -> UTxO
forall out. [(TxIn, out)] -> UTxO' out
UTxO.fromPairs ([(TxIn, TxOut CtxUTxO)] -> UTxO)
-> [(TxIn, TxOut CtxUTxO)] -> UTxO
forall a b. (a -> b) -> a -> b
$
      (TxIn -> Maybe (TxIn, TxOut CtxUTxO))
-> [TxIn] -> [(TxIn, TxOut CtxUTxO)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\TxIn
txIn -> (TxIn
txIn,) (TxOut CtxUTxO -> (TxIn, TxOut CtxUTxO))
-> Maybe (TxOut CtxUTxO) -> Maybe (TxIn, TxOut CtxUTxO)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TxIn -> UTxO -> Maybe (TxOut CtxUTxO)
forall out. TxIn -> UTxO' out -> Maybe out
UTxO.resolve TxIn
txIn UTxO
utxo) (Tx -> [TxIn]
forall era. Tx era -> [TxIn]
txIns' Tx
tx)

  initialRedeemer :: RedeemerType
initialRedeemer =
    RedeemerType -> Maybe RedeemerType -> RedeemerType
forall a. a -> Maybe a -> a
fromMaybe (Text -> RedeemerType
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"not found redeemer") (Maybe RedeemerType -> RedeemerType)
-> Maybe RedeemerType -> RedeemerType
forall a b. (a -> b) -> a -> b
$
      forall a. FromData a => Tx -> TxIn -> Maybe a
findRedeemerSpending @Initial.RedeemerType Tx
tx TxIn
initialTxIn

  initialScript :: PlutusScript lang
initialScript = ShortByteString -> PlutusScript lang
forall lang. ShortByteString -> PlutusScript lang
fromPlutusScript ShortByteString
Initial.validatorScript

  fakeScriptAddress :: AddressInEra Era
fakeScriptAddress = forall lang era.
(IsShelleyBasedEra era, IsPlutusScriptLanguage lang) =>
NetworkId -> PlutusScript lang -> AddressInEra era
mkScriptAddress @PlutusScriptV2 NetworkId
testNetworkId PlutusScript
forall {lang}. PlutusScript lang
fakeScript

  fakeScript :: PlutusScript lang
fakeScript = ShortByteString -> PlutusScript lang
forall lang. ShortByteString -> PlutusScript lang
fromPlutusScript (ShortByteString -> PlutusScript lang)
-> ShortByteString -> PlutusScript lang
forall a b. (a -> b) -> a -> b
$ Natural -> ShortByteString
Plutus.alwaysSucceedingNAryFunction Natural
3

genAdaOnlyUTxOOnMainnetWithAmountBiggerThanOutLimit :: Gen UTxO
genAdaOnlyUTxOOnMainnetWithAmountBiggerThanOutLimit :: Gen UTxO
genAdaOnlyUTxOOnMainnetWithAmountBiggerThanOutLimit = do
  Coin
adaAmount <- (Coin -> Coin -> Coin
forall a. Num a => a -> a -> a
+ Coin
maxMainnetLovelace) (Coin -> Coin) -> (Positive Coin -> Coin) -> Positive Coin -> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Positive Coin -> Coin
forall a. Positive a -> a
getPositive (Positive Coin -> Coin) -> Gen (Positive Coin) -> Gen Coin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Positive Coin)
forall a. Arbitrary a => Gen a
arbitrary
  Gen (TxOut CtxUTxO) -> Gen UTxO
genUTxO1 ((Value -> Value) -> TxOut CtxUTxO -> TxOut CtxUTxO
forall era ctx.
(IsMaryBasedEra era, IsShelleyBasedEra era) =>
(Value -> Value) -> TxOut ctx era -> TxOut ctx era
modifyTxOutValue (Value -> Value -> Value
forall a b. a -> b -> a
const (Value -> Value -> Value) -> Value -> Value -> Value
forall a b. (a -> b) -> a -> b
$ Coin -> Value
lovelaceToValue Coin
adaAmount) (TxOut CtxUTxO -> TxOut CtxUTxO)
-> Gen (TxOut CtxUTxO) -> Gen (TxOut CtxUTxO)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (TxOut CtxUTxO)
forall ctx. Gen (TxOut ctx)
genTxOut)

-- * Properties

-- | Given any Head protocol state and the transaction corresponding a protocol
-- transition we should be able to observe this transition correctly even in
-- presence of other valid Hydra Head protocol states in the used lookup utxo.
prop_observeAnyTx :: Property
prop_observeAnyTx :: Property
prop_observeAnyTx =
  Property -> Property
forall prop. Testable prop => prop -> Property
checkCoverage (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    Gen (ChainContext, ChainState, Tx, ChainTransition)
-> ((ChainContext, ChainState, Tx, ChainTransition) -> String)
-> ((ChainContext, ChainState, Tx, ChainTransition) -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> String) -> (a -> prop) -> Property
forAllShow Gen (ChainContext, ChainState, Tx, ChainTransition)
genChainStateWithTx (ChainContext, ChainState, Tx, ChainTransition) -> String
forall {a} {b} {a} {b} {c}.
(Show a, IsString b) =>
(a, b, c, a) -> b
showTransition (((ChainContext, ChainState, Tx, ChainTransition) -> Property)
 -> Property)
-> ((ChainContext, ChainState, Tx, ChainTransition) -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \(ChainContext
ctx, ChainState
st, Tx
tx, ChainTransition
transition) ->
      Gen (ChainContext, ChainState, Tx, ChainTransition)
-> ((ChainContext, ChainState, Tx, ChainTransition) -> String)
-> ((ChainContext, ChainState, Tx, ChainTransition) -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> String) -> (a -> prop) -> Property
forAllShow Gen (ChainContext, ChainState, Tx, ChainTransition)
genChainStateWithTx (ChainContext, ChainState, Tx, ChainTransition) -> String
forall {a} {b} {a} {b} {c}.
(Show a, IsString b) =>
(a, b, c, a) -> b
showTransition (((ChainContext, ChainState, Tx, ChainTransition) -> Property)
 -> Property)
-> ((ChainContext, ChainState, Tx, ChainTransition) -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \(ChainContext
_, ChainState
otherSt, Tx
_, ChainTransition
_) ->
        [ChainTransition] -> Property -> Property
forall a prop.
(Show a, Enum a, Bounded a, Typeable a, Testable prop) =>
[a] -> prop -> Property
genericCoverTable [ChainTransition
transition] (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ do
          let expectedHeadId :: Maybe HeadId
expectedHeadId = ChainState -> Maybe HeadId
chainStateHeadId ChainState
st
          case NetworkId -> UTxO -> Tx -> HeadObservation
observeHeadTx (ChainContext -> NetworkId
networkId ChainContext
ctx) (ChainState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainState
st UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> ChainState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainState
otherSt) Tx
tx of
            HeadObservation
NoHeadTx ->
              Bool
False Bool -> (Bool -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"observeHeadTx ignored transaction: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Tx -> String
forall b a. (Show a, IsString b) => a -> b
show Tx
tx)
            -- NOTE: we don't have the generated headId easily accessible in the initial state
            Init{} -> ChainTransition
transition ChainTransition -> ChainTransition -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== ChainTransition
Transition.Init
            Commit CommitObservation{HeadId
headId :: HeadId
$sel:headId:CommitObservation :: CommitObservation -> HeadId
headId} -> ChainTransition
transition ChainTransition -> ChainTransition -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== ChainTransition
Transition.Commit Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. HeadId -> Maybe HeadId
forall a. a -> Maybe a
Just HeadId
headId Maybe HeadId -> Maybe HeadId -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Maybe HeadId
expectedHeadId
            Abort AbortObservation{HeadId
headId :: HeadId
$sel:headId:AbortObservation :: AbortObservation -> HeadId
headId} -> ChainTransition
transition ChainTransition -> ChainTransition -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== ChainTransition
Transition.Abort Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. HeadId -> Maybe HeadId
forall a. a -> Maybe a
Just HeadId
headId Maybe HeadId -> Maybe HeadId -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Maybe HeadId
expectedHeadId
            CollectCom CollectComObservation{HeadId
headId :: HeadId
$sel:headId:CollectComObservation :: CollectComObservation -> HeadId
headId} -> ChainTransition
transition ChainTransition -> ChainTransition -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== ChainTransition
Transition.Collect Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. HeadId -> Maybe HeadId
forall a. a -> Maybe a
Just HeadId
headId Maybe HeadId -> Maybe HeadId -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Maybe HeadId
expectedHeadId
            Decrement DecrementObservation{HeadId
headId :: HeadId
$sel:headId:DecrementObservation :: DecrementObservation -> HeadId
headId} -> ChainTransition
transition ChainTransition -> ChainTransition -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== ChainTransition
Transition.Decrement Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. HeadId -> Maybe HeadId
forall a. a -> Maybe a
Just HeadId
headId Maybe HeadId -> Maybe HeadId -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Maybe HeadId
expectedHeadId
            Close CloseObservation{HeadId
headId :: HeadId
$sel:headId:CloseObservation :: CloseObservation -> HeadId
headId} -> ChainTransition
transition ChainTransition -> ChainTransition -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== ChainTransition
Transition.Close Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. HeadId -> Maybe HeadId
forall a. a -> Maybe a
Just HeadId
headId Maybe HeadId -> Maybe HeadId -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Maybe HeadId
expectedHeadId
            Contest ContestObservation{HeadId
headId :: HeadId
$sel:headId:ContestObservation :: ContestObservation -> HeadId
headId} -> ChainTransition
transition ChainTransition -> ChainTransition -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== ChainTransition
Transition.Contest Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. HeadId -> Maybe HeadId
forall a. a -> Maybe a
Just HeadId
headId Maybe HeadId -> Maybe HeadId -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Maybe HeadId
expectedHeadId
            Fanout FanoutObservation{HeadId
headId :: HeadId
$sel:headId:FanoutObservation :: FanoutObservation -> HeadId
headId} -> ChainTransition
transition ChainTransition -> ChainTransition -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== ChainTransition
Transition.Fanout Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. HeadId -> Maybe HeadId
forall a. a -> Maybe a
Just HeadId
headId Maybe HeadId -> Maybe HeadId -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Maybe HeadId
expectedHeadId
 where
  showTransition :: (a, b, c, a) -> b
showTransition (a
_, b
_, c
_, a
t) = a -> b
forall b a. (Show a, IsString b) => a -> b
show a
t

  chainStateHeadId :: ChainState -> Maybe HeadId
chainStateHeadId = \case
    Idle{} -> Maybe HeadId
forall a. Maybe a
Nothing
    Initial InitialState{HeadId
$sel:headId:InitialState :: InitialState -> HeadId
headId :: HeadId
headId} -> HeadId -> Maybe HeadId
forall a. a -> Maybe a
Just HeadId
headId
    Open OpenState{HeadId
headId :: HeadId
$sel:headId:OpenState :: OpenState -> HeadId
headId} -> HeadId -> Maybe HeadId
forall a. a -> Maybe a
Just HeadId
headId
    Closed ClosedState{HeadId
headId :: HeadId
$sel:headId:ClosedState :: ClosedState -> HeadId
headId} -> HeadId -> Maybe HeadId
forall a. a -> Maybe a
Just HeadId
headId

-- | Given a UTxO with more than one entry, we can split it into two non-empty UTxO.
prop_splitUTxO :: UTxO -> Property
prop_splitUTxO :: UTxO -> Property
prop_splitUTxO UTxO
utxo =
  (UTxO -> Int
forall a. UTxO' a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length UTxO
utxo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>
    let (UTxO
inHead, UTxO
toDecommit) = UTxO -> (UTxO, UTxO)
splitUTxO UTxO
utxo
     in [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
          [ Bool -> Bool
not (UTxO -> Bool
forall a. UTxO' a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null UTxO
inHead) Bool -> (Bool -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"inHead is empty"
          , Bool -> Bool
not (UTxO -> Bool
forall a. UTxO' a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null UTxO
toDecommit) Bool -> (Bool -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"toDecommit is empty"
          , UTxO
inHead UTxO -> UTxO -> Bool
forall a. Eq a => a -> a -> Bool
/= UTxO
toDecommit Bool -> (Bool -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"inHead == toDecommit"
          ]

prop_canCloseFanoutEveryCollect :: Property
prop_canCloseFanoutEveryCollect :: Property
prop_canCloseFanoutEveryCollect = (forall s. PropertyM (ST s) Property) -> Property
forall a. Testable a => (forall s. PropertyM (ST s) a) -> Property
monadicST ((forall s. PropertyM (ST s) Property) -> Property)
-> (forall s. PropertyM (ST s) Property) -> Property
forall a b. (a -> b) -> a -> b
$ do
  let maxParties :: Int
maxParties = Int
10
  ctx :: HydraContext
ctx@HydraContext{ContestationPeriod
ctxContestationPeriod :: ContestationPeriod
$sel:ctxContestationPeriod:HydraContext :: HydraContext -> ContestationPeriod
ctxContestationPeriod} <- Gen HydraContext -> PropertyM (ST s) HydraContext
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen HydraContext -> PropertyM (ST s) HydraContext)
-> Gen HydraContext -> PropertyM (ST s) HydraContext
forall a b. (a -> b) -> a -> b
$ Int -> Gen HydraContext
genHydraContext Int
maxParties
  ChainContext
cctx <- Gen ChainContext -> PropertyM (ST s) ChainContext
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen ChainContext -> PropertyM (ST s) ChainContext)
-> Gen ChainContext -> PropertyM (ST s) ChainContext
forall a b. (a -> b) -> a -> b
$ HydraContext -> Gen ChainContext
pickChainContext HydraContext
ctx
  -- Init
  Tx
txInit <- Gen Tx -> PropertyM (ST s) Tx
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen Tx -> PropertyM (ST s) Tx) -> Gen Tx -> PropertyM (ST s) Tx
forall a b. (a -> b) -> a -> b
$ HydraContext -> Gen Tx
genInitTx HydraContext
ctx
  -- Commits
  [Tx]
commits <- Gen [Tx] -> PropertyM (ST s) [Tx]
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen [Tx] -> PropertyM (ST s) [Tx])
-> Gen [Tx] -> PropertyM (ST s) [Tx]
forall a b. (a -> b) -> a -> b
$ Gen UTxO -> HydraContext -> Tx -> Gen [Tx]
genCommits' (Int -> Gen UTxO
genUTxOSized Int
1) HydraContext
ctx Tx
txInit
  let ([UTxO]
committed, InitialState
stInitial) = HasCallStack =>
ChainContext
-> [VerificationKey PaymentKey]
-> Tx
-> [Tx]
-> ([UTxO], InitialState)
ChainContext
-> [VerificationKey PaymentKey]
-> Tx
-> [Tx]
-> ([UTxO], InitialState)
unsafeObserveInitAndCommits ChainContext
cctx (HydraContext -> [VerificationKey PaymentKey]
ctxVerificationKeys HydraContext
ctx) Tx
txInit [Tx]
commits
  let InitialState{$sel:headId:InitialState :: InitialState -> HeadId
headId = HeadId
initialHeadId} = InitialState
stInitial
  -- Collect
  let initialUTxO :: UTxO
initialUTxO = [UTxO] -> UTxO
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold [UTxO]
committed
  let spendableUTxO :: UTxO
spendableUTxO = InitialState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO InitialState
stInitial
  let txCollect :: Tx
txCollect = ChainContext -> HeadId -> HeadParameters -> UTxO -> UTxO -> Tx
unsafeCollect ChainContext
cctx HeadId
initialHeadId (HydraContext -> HeadParameters
ctxHeadParameters HydraContext
ctx) UTxO
initialUTxO UTxO
spendableUTxO
  stOpen :: OpenState
stOpen@OpenState{TxIn
seedTxIn :: TxIn
$sel:seedTxIn:OpenState :: OpenState -> TxIn
seedTxIn, HeadId
$sel:headId:OpenState :: OpenState -> HeadId
headId :: HeadId
headId} <- Maybe OpenState -> PropertyM (ST s) OpenState
forall (m :: * -> *) a. MonadFail m => Maybe a -> m a
mfail (Maybe OpenState -> PropertyM (ST s) OpenState)
-> Maybe OpenState -> PropertyM (ST s) OpenState
forall a b. (a -> b) -> a -> b
$ (OnChainTx Tx, OpenState) -> OpenState
forall a b. (a, b) -> b
snd ((OnChainTx Tx, OpenState) -> OpenState)
-> Maybe (OnChainTx Tx, OpenState) -> Maybe OpenState
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InitialState -> Tx -> Maybe (OnChainTx Tx, OpenState)
observeCollect InitialState
stInitial Tx
txCollect
  -- Close
  (SlotNo
closeLower, (SlotNo, UTCTime)
closeUpper) <- Gen (SlotNo, (SlotNo, UTCTime))
-> PropertyM (ST s) (SlotNo, (SlotNo, UTCTime))
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen (SlotNo, (SlotNo, UTCTime))
 -> PropertyM (ST s) (SlotNo, (SlotNo, UTCTime)))
-> Gen (SlotNo, (SlotNo, UTCTime))
-> PropertyM (ST s) (SlotNo, (SlotNo, UTCTime))
forall a b. (a -> b) -> a -> b
$ ContestationPeriod -> Gen (SlotNo, (SlotNo, UTCTime))
genValidityBoundsFromContestationPeriod ContestationPeriod
ctxContestationPeriod
  let closeUTxO :: UTxO
closeUTxO = OpenState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO OpenState
stOpen
      txClose :: Tx
txClose = HasCallStack =>
ChainContext
-> UTxO
-> HeadId
-> HeadParameters
-> SnapshotVersion
-> ConfirmedSnapshot Tx
-> SlotNo
-> (SlotNo, UTCTime)
-> Tx
ChainContext
-> UTxO
-> HeadId
-> HeadParameters
-> SnapshotVersion
-> ConfirmedSnapshot Tx
-> SlotNo
-> (SlotNo, UTCTime)
-> Tx
unsafeClose ChainContext
cctx UTxO
closeUTxO HeadId
headId (HydraContext -> HeadParameters
ctxHeadParameters HydraContext
ctx) SnapshotVersion
0 InitialSnapshot{HeadId
headId :: HeadId
$sel:headId:InitialSnapshot :: HeadId
headId, UTxO
UTxOType Tx
$sel:initialUTxO:InitialSnapshot :: UTxOType Tx
initialUTxO :: UTxO
initialUTxO} SlotNo
closeLower (SlotNo, UTCTime)
closeUpper
  (UTCTime
deadline, ClosedState
stClosed) <- case OpenState -> Tx -> Maybe (OnChainTx Tx, ClosedState)
observeClose OpenState
stOpen Tx
txClose of
    Just (OnCloseTx{UTCTime
contestationDeadline :: UTCTime
$sel:contestationDeadline:OnInitTx :: forall tx. OnChainTx tx -> UTCTime
contestationDeadline}, ClosedState
st) -> (UTCTime, ClosedState) -> PropertyM (ST s) (UTCTime, ClosedState)
forall a. a -> PropertyM (ST s) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UTCTime
contestationDeadline, ClosedState
st)
    Maybe (OnChainTx Tx, ClosedState)
_ -> String -> PropertyM (ST s) (UTCTime, ClosedState)
forall a. String -> PropertyM (ST s) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"not observed close"
  -- Fanout
  let fanoutUTxO :: UTxO
fanoutUTxO = ClosedState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ClosedState
stClosed
  let txFanout :: Tx
txFanout = HasCallStack =>
ChainContext -> UTxO -> TxIn -> UTxO -> Maybe UTxO -> SlotNo -> Tx
ChainContext -> UTxO -> TxIn -> UTxO -> Maybe UTxO -> SlotNo -> Tx
unsafeFanout ChainContext
cctx UTxO
fanoutUTxO TxIn
seedTxIn UTxO
initialUTxO Maybe UTxO
forall a. Maybe a
Nothing (SystemStart -> SlotLength -> UTCTime -> SlotNo
slotNoFromUTCTime SystemStart
systemStart SlotLength
slotLength UTCTime
deadline)

  -- Properties
  let collectFails :: Property
collectFails =
        (Tx, UTxO) -> Property
propTransactionFailsEvaluation (Tx
txCollect, ChainContext -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainContext
cctx UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> InitialState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO InitialState
stInitial)
          Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"collect passed, but others failed?"
          Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
10 Bool
True String
"collect failed already"
  let collectCloseAndFanoutPass :: Property
collectCloseAndFanoutPass =
        [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
          [ (Tx, UTxO) -> Property
propTransactionEvaluates (Tx
txCollect, ChainContext -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainContext
cctx UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> InitialState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO InitialState
stInitial)
              Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"collect failed"
          , (Tx, UTxO) -> Property
propTransactionEvaluates (Tx
txClose, ChainContext -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainContext
cctx UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> OpenState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO OpenState
stOpen)
              Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"close failed"
          , (Tx, UTxO) -> Property
propTransactionEvaluates (Tx
txFanout, ChainContext -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainContext
cctx UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> ClosedState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ClosedState
stClosed)
              Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"fanout failed"
          ]
          Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
10 Bool
True String
"collect, close and fanout passed"
  Property -> PropertyM (ST s) Property
forall a. a -> PropertyM (ST s) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> PropertyM (ST s) Property)
-> Property -> PropertyM (ST s) Property
forall a b. (a -> b) -> a -> b
$
    -- XXX: Coverage does not work if we only collectFails
    Property -> Property
forall prop. Testable prop => prop -> Property
checkCoverage
      (Property
collectFails Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.||. Property
collectCloseAndFanoutPass)

--
-- Generic Properties
--

propBelowSizeLimit ::
  Natural ->
  ((UTxO -> Tx -> Property) -> Property) ->
  SpecWith ()
propBelowSizeLimit :: Natural -> ((UTxO -> Tx -> Property) -> Property) -> Spec
propBelowSizeLimit Natural
txSizeLimit (UTxO -> Tx -> Property) -> Property
forAllTx =
  String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (String
"transaction size is below " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Natural -> String
forall {a} {a}.
(Semigroup a, Show a, IsString a, Integral a) =>
a -> a
showKB Natural
txSizeLimit) (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
    (UTxO -> Tx -> Property) -> Property
forAllTx ((UTxO -> Tx -> Property) -> Property)
-> (UTxO -> Tx -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \UTxO
_ Tx
tx ->
      let cbor :: ByteString
cbor = Tx -> ByteString
forall a. ToCBOR a => a -> ByteString
serialize Tx
tx
          len :: Int64
len = ByteString -> Int64
LBS.length ByteString
cbor
       in Int64
len Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
< Natural -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
txSizeLimit
            Bool -> (Bool -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
label (Int64 -> String
forall {a} {a}.
(Semigroup a, Show a, IsString a, Integral a) =>
a -> a
showKB Int64
len)
            Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Tx -> String
renderTx Tx
tx)
            Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Actual size: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int64 -> String
forall b a. (Show a, IsString b) => a -> b
show Int64
len)
 where
  showKB :: a -> a
showKB a
nb = a -> a
forall b a. (Show a, IsString b) => a -> b
show (a
nb a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
1024) a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
"kB"

propIsValid ::
  ((UTxO -> Tx -> Property) -> Property) ->
  SpecWith ()
propIsValid :: ((UTxO -> Tx -> Property) -> Property) -> Spec
propIsValid (UTxO -> Tx -> Property) -> Property
forAllTx =
  String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"validates within maxTxExecutionUnits" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
    (UTxO -> Tx -> Property) -> Property
forAllTx ((UTxO -> Tx -> Property) -> Property)
-> (UTxO -> Tx -> Property) -> Property
forall a b. (a -> b) -> a -> b
$
      \UTxO
utxo Tx
tx -> (Tx, UTxO) -> Property
propTransactionEvaluates (Tx
tx, UTxO
utxo)

-- * Generators

-- TODO: These forAllXX functions are hard to use and understand. Maybe simple
-- 'Gen' or functions in 'PropertyM' are better combinable?

forAllInit ::
  Testable property =>
  (UTxO -> Tx -> property) ->
  Property
forAllInit :: forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllInit UTxO -> Tx -> property
action =
  Gen HydraContext -> (HydraContext -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind (Int -> Gen HydraContext
genHydraContext Int
maximumNumberOfParties) ((HydraContext -> Property) -> Property)
-> (HydraContext -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \HydraContext
ctx ->
    Gen ChainContext -> (ChainContext -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (HydraContext -> Gen ChainContext
pickChainContext HydraContext
ctx) ((ChainContext -> Property) -> Property)
-> (ChainContext -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ChainContext
cctx -> do
      Gen (TxIn, TxOut CtxUTxO)
-> ((TxIn, TxOut CtxUTxO) -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((,) (TxIn -> TxOut CtxUTxO -> (TxIn, TxOut CtxUTxO))
-> Gen TxIn -> Gen (TxOut CtxUTxO -> (TxIn, TxOut CtxUTxO))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen TxIn
genTxIn Gen (TxOut CtxUTxO -> (TxIn, TxOut CtxUTxO))
-> Gen (TxOut CtxUTxO) -> Gen (TxIn, TxOut CtxUTxO)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> VerificationKey PaymentKey -> Gen (TxOut CtxUTxO)
forall ctx. VerificationKey PaymentKey -> Gen (TxOut ctx)
genOutput (ChainContext -> VerificationKey PaymentKey
ownVerificationKey ChainContext
cctx)) (((TxIn, TxOut CtxUTxO) -> Property) -> Property)
-> ((TxIn, TxOut CtxUTxO) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \(TxIn
seedIn, TxOut CtxUTxO
seedOut) -> do
        let tx :: Tx
tx = ChainContext -> TxIn -> [OnChainId] -> HeadParameters -> Tx
initialize ChainContext
cctx TxIn
seedIn (HydraContext -> [OnChainId]
ctxParticipants HydraContext
ctx) (HydraContext -> HeadParameters
ctxHeadParameters HydraContext
ctx)
            utxo :: UTxO
utxo = (TxIn, TxOut CtxUTxO) -> UTxO
forall out. (TxIn, out) -> UTxO' out
UTxO.singleton (TxIn
seedIn, TxOut CtxUTxO
seedOut) UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> ChainContext -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainContext
cctx
         in UTxO -> Tx -> property
action UTxO
utxo Tx
tx
              property -> (property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Bool -> String -> property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify
                ([VerificationKey PaymentKey] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (HydraContext -> [VerificationKey PaymentKey]
ctxVerificationKeys HydraContext
ctx))
                String
"1 party"
              Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify
                (Bool -> Bool
not ([VerificationKey PaymentKey] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (HydraContext -> [VerificationKey PaymentKey]
ctxVerificationKeys HydraContext
ctx)))
                String
"2+ parties"

forAllCommit ::
  Testable property =>
  (UTxO -> Tx -> property) ->
  Property
forAllCommit :: forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllCommit UTxO -> Tx -> property
action =
  (ChainContext -> InitialState -> UTxO -> Tx -> property)
-> Property
forall property.
Testable property =>
(ChainContext -> InitialState -> UTxO -> Tx -> property)
-> Property
forAllCommit' ((ChainContext -> InitialState -> UTxO -> Tx -> property)
 -> Property)
-> (ChainContext -> InitialState -> UTxO -> Tx -> property)
-> Property
forall a b. (a -> b) -> a -> b
$ \ChainContext
ctx InitialState
st UTxO
toCommit Tx
tx ->
    let utxo :: UTxO
utxo = InitialState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO InitialState
st UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> UTxO
toCommit UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> ChainContext -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainContext
ctx
     in UTxO -> Tx -> property
action UTxO
utxo Tx
tx

forAllCommit' ::
  Testable property =>
  (ChainContext -> InitialState -> UTxO -> Tx -> property) ->
  Property
forAllCommit' :: forall property.
Testable property =>
(ChainContext -> InitialState -> UTxO -> Tx -> property)
-> Property
forAllCommit' ChainContext -> InitialState -> UTxO -> Tx -> property
action = do
  Gen HydraContext -> (HydraContext -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind (Int -> Gen HydraContext
genHydraContext Int
maximumNumberOfParties) ((HydraContext -> Property) -> Property)
-> (HydraContext -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \HydraContext
hctx ->
    Gen (ChainContext, InitialState)
-> ((ChainContext, InitialState) -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind (HydraContext -> Gen (ChainContext, InitialState)
genStInitial HydraContext
hctx) (((ChainContext, InitialState) -> Property) -> Property)
-> ((ChainContext, InitialState) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \(ChainContext
ctx, InitialState
stInitial) ->
      Gen UTxO -> (UTxO -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind (VerificationKey PaymentKey -> Gen UTxO
genCommitFor (VerificationKey PaymentKey -> Gen UTxO)
-> VerificationKey PaymentKey -> Gen UTxO
forall a b. (a -> b) -> a -> b
$ ChainContext -> VerificationKey PaymentKey
ownVerificationKey ChainContext
ctx) ((UTxO -> Property) -> Property) -> (UTxO -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \UTxO
toCommit ->
        -- TODO: generate script inputs here? <- SB: what script inputs?
        let InitialState{HeadId
$sel:headId:InitialState :: InitialState -> HeadId
headId :: HeadId
headId} = InitialState
stInitial
            tx :: Tx
tx = HasCallStack => ChainContext -> HeadId -> UTxO -> UTxO -> Tx
ChainContext -> HeadId -> UTxO -> UTxO -> Tx
unsafeCommit ChainContext
ctx HeadId
headId (ChainContext -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainContext
ctx UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> InitialState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO InitialState
stInitial) UTxO
toCommit
         in ChainContext -> InitialState -> UTxO -> Tx -> property
action ChainContext
ctx InitialState
stInitial UTxO
toCommit Tx
tx
              property -> (property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Bool -> String -> property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify
                (UTxO -> Bool
forall a. UTxO' a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null UTxO
toCommit)
                String
"Empty commit"
              Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify
                (Bool -> Bool
not (UTxO -> Bool
forall a. UTxO' a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null UTxO
toCommit))
                String
"Non-empty commit"

forAllAbort ::
  Testable property =>
  (UTxO -> Tx -> property) ->
  Property
forAllAbort :: forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllAbort UTxO -> Tx -> property
action = do
  Gen HydraContext -> (HydraContext -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Int -> Gen HydraContext
genHydraContext Int
maximumNumberOfParties) ((HydraContext -> Property) -> Property)
-> (HydraContext -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \HydraContext
ctx ->
    Gen ChainContext -> (ChainContext -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (HydraContext -> Gen ChainContext
pickChainContext HydraContext
ctx) ((ChainContext -> Property) -> Property)
-> (ChainContext -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ChainContext
cctx ->
      Gen Tx -> (Tx -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind (HydraContext -> Gen Tx
genInitTx HydraContext
ctx) ((Tx -> Property) -> Property) -> (Tx -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Tx
initTx -> do
        Gen [Tx] -> ([Tx] -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind ([Tx] -> Gen [Tx]
forall a. [a] -> Gen [a]
sublistOf ([Tx] -> Gen [Tx]) -> Gen [Tx] -> Gen [Tx]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< HydraContext -> Tx -> Gen [Tx]
genCommits HydraContext
ctx Tx
initTx) (([Tx] -> Property) -> Property) -> ([Tx] -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \[Tx]
commits ->
          let ([UTxO]
committed, InitialState
stInitialized) = HasCallStack =>
ChainContext
-> [VerificationKey PaymentKey]
-> Tx
-> [Tx]
-> ([UTxO], InitialState)
ChainContext
-> [VerificationKey PaymentKey]
-> Tx
-> [Tx]
-> ([UTxO], InitialState)
unsafeObserveInitAndCommits ChainContext
cctx (HydraContext -> [VerificationKey PaymentKey]
ctxVerificationKeys HydraContext
ctx) Tx
initTx [Tx]
commits
              utxo :: UTxO
utxo = InitialState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO InitialState
stInitialized UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> ChainContext -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainContext
cctx
              InitialState{TxIn
seedTxIn :: TxIn
$sel:seedTxIn:InitialState :: InitialState -> TxIn
seedTxIn} = InitialState
stInitialized
           in UTxO -> Tx -> property
action UTxO
utxo (HasCallStack => ChainContext -> TxIn -> UTxO -> UTxO -> Tx
ChainContext -> TxIn -> UTxO -> UTxO -> Tx
unsafeAbort ChainContext
cctx TxIn
seedTxIn UTxO
utxo ([UTxO] -> UTxO
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold [UTxO]
committed))
                property -> (property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Bool -> String -> property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify
                  ([Tx] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Tx]
commits)
                  String
"Abort immediately, after 0 commits"
                Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify
                  (Bool -> Bool
not ([Tx] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Tx]
commits) Bool -> Bool -> Bool
&& [Tx] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Tx]
commits Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Party] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (HydraContext -> [Party]
ctxParties HydraContext
ctx))
                  String
"Abort after some (but not all) commits"
                Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify
                  ([Tx] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Tx]
commits Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Party] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (HydraContext -> [Party]
ctxParties HydraContext
ctx))
                  String
"Abort after all commits"

forAllCollectCom ::
  Testable property =>
  (UTxO -> Tx -> property) ->
  Property
forAllCollectCom :: forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllCollectCom UTxO -> Tx -> property
action =
  Gen (ChainContext, [UTxO], InitialState, Tx)
-> ((ChainContext, [UTxO], InitialState, Tx) -> Property)
-> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind Gen (ChainContext, [UTxO], InitialState, Tx)
genCollectComTx (((ChainContext, [UTxO], InitialState, Tx) -> Property)
 -> Property)
-> ((ChainContext, [UTxO], InitialState, Tx) -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \(ChainContext
ctx, [UTxO]
committedUTxO, InitialState
stInitialized, Tx
tx) ->
    let utxo :: UTxO
utxo = InitialState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO InitialState
stInitialized UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> ChainContext -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainContext
ctx
     in UTxO -> Tx -> property
action UTxO
utxo Tx
tx
          property -> (property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Committed UTxO: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [UTxO] -> String
forall b a. (Show a, IsString b) => a -> b
show [UTxO]
committedUTxO)

forAllDecrement ::
  Testable property =>
  (UTxO -> Tx -> property) ->
  Property
forAllDecrement :: forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllDecrement UTxO -> Tx -> property
action = do
  ([TxOut CtxUTxO] -> UTxO -> Tx -> property) -> Property
forall property.
Testable property =>
([TxOut CtxUTxO] -> UTxO -> Tx -> property) -> Property
forAllDecrement' (([TxOut CtxUTxO] -> UTxO -> Tx -> property) -> Property)
-> ([TxOut CtxUTxO] -> UTxO -> Tx -> property) -> Property
forall a b. (a -> b) -> a -> b
$ \[TxOut CtxUTxO]
_ UTxO
utxo Tx
tx ->
    UTxO -> Tx -> property
action UTxO
utxo Tx
tx

forAllDecrement' ::
  Testable property =>
  ([TxOut CtxUTxO] -> UTxO -> Tx -> property) ->
  Property
forAllDecrement' :: forall property.
Testable property =>
([TxOut CtxUTxO] -> UTxO -> Tx -> property) -> Property
forAllDecrement' [TxOut CtxUTxO] -> UTxO -> Tx -> property
action = do
  Gen (ChainContext, [TxOut CtxUTxO], OpenState, Tx)
-> ((ChainContext, [TxOut CtxUTxO], OpenState, Tx)
    -> [(ChainContext, [TxOut CtxUTxO], OpenState, Tx)])
-> ((ChainContext, [TxOut CtxUTxO], OpenState, Tx) -> property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrink (Int -> Gen (ChainContext, [TxOut CtxUTxO], OpenState, Tx)
genDecrementTx Int
maximumNumberOfParties) (ChainContext, [TxOut CtxUTxO], OpenState, Tx)
-> [(ChainContext, [TxOut CtxUTxO], OpenState, Tx)]
forall a. Arbitrary a => a -> [a]
shrink (((ChainContext, [TxOut CtxUTxO], OpenState, Tx) -> property)
 -> Property)
-> ((ChainContext, [TxOut CtxUTxO], OpenState, Tx) -> property)
-> Property
forall a b. (a -> b) -> a -> b
$ \(ChainContext
ctx, [TxOut CtxUTxO]
distributed, OpenState
st, Tx
tx) ->
    let utxo :: UTxO
utxo = OpenState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO OpenState
st UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> ChainContext -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainContext
ctx
     in [TxOut CtxUTxO] -> UTxO -> Tx -> property
action [TxOut CtxUTxO]
distributed UTxO
utxo Tx
tx

forAllClose ::
  Testable property =>
  (UTxO -> Tx -> property) ->
  Property
forAllClose :: forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllClose UTxO -> Tx -> property
action = do
  -- FIXME: we should not hardcode number of parties but generate it within bounds
  Gen (ChainContext, OpenState, Tx, ConfirmedSnapshot Tx)
-> ((ChainContext, OpenState, Tx, ConfirmedSnapshot Tx)
    -> Property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Int -> Gen (ChainContext, OpenState, Tx, ConfirmedSnapshot Tx)
genCloseTx Int
maximumNumberOfParties) (((ChainContext, OpenState, Tx, ConfirmedSnapshot Tx) -> Property)
 -> Property)
-> ((ChainContext, OpenState, Tx, ConfirmedSnapshot Tx)
    -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \(ChainContext
ctx, OpenState
st, Tx
tx, ConfirmedSnapshot Tx
sn) ->
    let utxo :: UTxO
utxo = OpenState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO OpenState
st UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> ChainContext -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainContext
ctx
     in UTxO -> Tx -> property
action UTxO
utxo Tx
tx
          property -> (property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> property -> Property
forall prop. Testable prop => String -> prop -> Property
label ([String] -> String
forall a. HasCallStack => [a] -> a
Prelude.head ([String] -> String)
-> (ConfirmedSnapshot Tx -> [String])
-> ConfirmedSnapshot Tx
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
Prelude.words (String -> [String])
-> (ConfirmedSnapshot Tx -> String)
-> ConfirmedSnapshot Tx
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConfirmedSnapshot Tx -> String
forall b a. (Show a, IsString b) => a -> b
show (ConfirmedSnapshot Tx -> String) -> ConfirmedSnapshot Tx -> String
forall a b. (a -> b) -> a -> b
$ ConfirmedSnapshot Tx
sn)

forAllContest ::
  Testable property =>
  (UTxO -> Tx -> property) ->
  Property
forAllContest :: forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllContest UTxO -> Tx -> property
action =
  Gen (HydraContext, (SlotNo, UTCTime), ClosedState, Tx)
-> ((HydraContext, (SlotNo, UTCTime), ClosedState, Tx) -> Property)
-> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind Gen (HydraContext, (SlotNo, UTCTime), ClosedState, Tx)
genContestTx (((HydraContext, (SlotNo, UTCTime), ClosedState, Tx) -> Property)
 -> Property)
-> ((HydraContext, (SlotNo, UTCTime), ClosedState, Tx) -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \(hctx :: HydraContext
hctx@HydraContext{ContestationPeriod
$sel:ctxContestationPeriod:HydraContext :: HydraContext -> ContestationPeriod
ctxContestationPeriod :: ContestationPeriod
ctxContestationPeriod}, (SlotNo, UTCTime)
closePointInTime, ClosedState
stClosed, Tx
tx) ->
    -- XXX: Pick an arbitrary context to contest. We will stumble over this when
    -- we make contests only possible once per party.
    Gen ChainContext -> (ChainContext -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind (HydraContext -> Gen ChainContext
pickChainContext HydraContext
hctx) ((ChainContext -> Property) -> Property)
-> (ChainContext -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ChainContext
ctx ->
      let utxo :: UTxO
utxo = ClosedState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ClosedState
stClosed UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> ChainContext -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainContext
ctx
       in UTxO -> Tx -> property
action UTxO
utxo Tx
tx
            property -> (property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Contestation deadline: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> UTCTime -> String
forall b a. (Show a, IsString b) => a -> b
show (ClosedState -> UTCTime
getContestationDeadline ClosedState
stClosed))
            Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Contestation period: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> ContestationPeriod -> String
forall b a. (Show a, IsString b) => a -> b
show ContestationPeriod
ctxContestationPeriod)
            Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Close point: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> (SlotNo, UTCTime) -> String
forall b a. (Show a, IsString b) => a -> b
show (SlotNo, UTCTime)
closePointInTime)
            Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Closed contesters: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [PubKeyHash] -> String
forall b a. (Show a, IsString b) => a -> b
show (ClosedState -> [PubKeyHash]
getClosedContesters ClosedState
stClosed))
            Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Contestation period" (ContestationPeriod -> [String]
tabulateContestationPeriod ContestationPeriod
ctxContestationPeriod)
            Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Close point (slot)" (SlotNo -> [String]
forall {a} {a}. (Ord a, Num a, IsString a) => a -> [a]
tabulateNum (SlotNo -> [String]) -> SlotNo -> [String]
forall a b. (a -> b) -> a -> b
$ (SlotNo, UTCTime) -> SlotNo
forall a b. (a, b) -> a
fst (SlotNo, UTCTime)
closePointInTime)
 where
  tabulateNum :: a -> [a]
tabulateNum a
x
    | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 = [a
"> 0"]
    | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 = [a
"< 0"]
    | Bool
otherwise = [a
"== 0"]

  tabulateContestationPeriod :: ContestationPeriod -> [String]
tabulateContestationPeriod (ContestationPeriod -> NominalDiffTime
toNominalDiffTime -> NominalDiffTime
cp)
    | NominalDiffTime
cp NominalDiffTime -> NominalDiffTime -> Bool
forall a. Eq a => a -> a -> Bool
== NominalDiffTime
confirmedHorizon = [String
"k blocks on mainnet"]
    | NominalDiffTime
cp NominalDiffTime -> NominalDiffTime -> Bool
forall a. Eq a => a -> a -> Bool
== NominalDiffTime
oneDay = [String
"one day"]
    | NominalDiffTime
cp NominalDiffTime -> NominalDiffTime -> Bool
forall a. Eq a => a -> a -> Bool
== NominalDiffTime
oneWeek = [String
"one week"]
    | NominalDiffTime
cp NominalDiffTime -> NominalDiffTime -> Bool
forall a. Eq a => a -> a -> Bool
== NominalDiffTime
oneMonth = [String
"one month"]
    | NominalDiffTime
cp NominalDiffTime -> NominalDiffTime -> Bool
forall a. Eq a => a -> a -> Bool
== NominalDiffTime
oneYear = [String
"one year"]
    | NominalDiffTime
cp NominalDiffTime -> NominalDiffTime -> Bool
forall a. Ord a => a -> a -> Bool
< NominalDiffTime
confirmedHorizon = [String
"< k blocks"]
    | Bool
otherwise = [String
"> k blocks"]

  confirmedHorizon :: NominalDiffTime
confirmedHorizon = NominalDiffTime
2160 NominalDiffTime -> NominalDiffTime -> NominalDiffTime
forall a. Num a => a -> a -> a
* NominalDiffTime
20 -- k blocks on mainnet
  oneDay :: NominalDiffTime
oneDay = NominalDiffTime
3600 NominalDiffTime -> NominalDiffTime -> NominalDiffTime
forall a. Num a => a -> a -> a
* NominalDiffTime
24
  oneWeek :: NominalDiffTime
oneWeek = NominalDiffTime
oneDay NominalDiffTime -> NominalDiffTime -> NominalDiffTime
forall a. Num a => a -> a -> a
* NominalDiffTime
7
  oneMonth :: NominalDiffTime
oneMonth = NominalDiffTime
oneDay NominalDiffTime -> NominalDiffTime -> NominalDiffTime
forall a. Num a => a -> a -> a
* NominalDiffTime
30
  oneYear :: NominalDiffTime
oneYear = NominalDiffTime
oneDay NominalDiffTime -> NominalDiffTime -> NominalDiffTime
forall a. Num a => a -> a -> a
* NominalDiffTime
365

  getClosedContesters :: ClosedState -> [PubKeyHash]
getClosedContesters = ClosedThreadOutput -> [PubKeyHash]
closedContesters (ClosedThreadOutput -> [PubKeyHash])
-> (ClosedState -> ClosedThreadOutput)
-> ClosedState
-> [PubKeyHash]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClosedState -> ClosedThreadOutput
closedThreadOutput

forAllFanout ::
  Testable property =>
  (UTxO -> Tx -> property) ->
  Property
forAllFanout :: forall property.
Testable property =>
(UTxO -> Tx -> property) -> Property
forAllFanout UTxO -> Tx -> property
action =
  -- TODO: The utxo to fanout should be more arbitrary to have better test coverage
  Gen (HydraContext, ClosedState, Tx)
-> ((HydraContext, ClosedState, Tx) -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((Int -> Gen (HydraContext, ClosedState, Tx))
-> Gen (HydraContext, ClosedState, Tx)
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen (HydraContext, ClosedState, Tx))
 -> Gen (HydraContext, ClosedState, Tx))
-> (Int -> Gen (HydraContext, ClosedState, Tx))
-> Gen (HydraContext, ClosedState, Tx)
forall a b. (a -> b) -> a -> b
$ \Int
n -> Int -> Int -> Gen (HydraContext, ClosedState, Tx)
genFanoutTx Int
maximumNumberOfParties (Int
n Int -> Int -> Int
forall a. Ord a => a -> a -> a
`min` Int
maxSupported)) (((HydraContext, ClosedState, Tx) -> Property) -> Property)
-> ((HydraContext, ClosedState, Tx) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \(HydraContext
hctx, ClosedState
stClosed, Tx
tx) ->
    Gen ChainContext -> (ChainContext -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind (HydraContext -> Gen ChainContext
pickChainContext HydraContext
hctx) ((ChainContext -> Property) -> Property)
-> (ChainContext -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ChainContext
ctx ->
      let utxo :: UTxO
utxo = ClosedState -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ClosedState
stClosed UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> ChainContext -> UTxO
forall a. HasKnownUTxO a => a -> UTxO
getKnownUTxO ChainContext
ctx
       in UTxO -> Tx -> property
action UTxO
utxo Tx
tx
            property -> (property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> property -> Property
forall prop. Testable prop => String -> prop -> Property
label (String
"Fanout size: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
prettyLength ([TxOut CtxTx] -> Int
forall {ctx}. [TxOut ctx] -> Int
countAssets ([TxOut CtxTx] -> Int) -> [TxOut CtxTx] -> Int
forall a b. (a -> b) -> a -> b
$ Tx -> [TxOut CtxTx]
forall era. Tx era -> [TxOut CtxTx era]
txOuts' Tx
tx))
 where
  maxSupported :: Int
maxSupported = Int
58

  countAssets :: [TxOut ctx] -> Int
countAssets = Sum Int -> Int
forall a. Sum a -> a
getSum (Sum Int -> Int) -> ([TxOut ctx] -> Sum Int) -> [TxOut ctx] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TxOut ctx -> Sum Int) -> [TxOut ctx] -> Sum Int
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Int -> Sum Int
forall a. a -> Sum a
Sum (Int -> Sum Int) -> (TxOut ctx -> Int) -> TxOut ctx -> Sum Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Int
valueSize (Value -> Int) -> (TxOut ctx -> Value) -> TxOut ctx -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxOut ctx -> Value
forall ctx. TxOut ctx -> Value
txOutValue)

  prettyLength :: Int -> String
prettyLength Int
len
    | Int
len Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxSupported = String
"> " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall b a. (Show a, IsString b) => a -> b
show Int
maxSupported String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" ???"
    | Int
len Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
40 = String
"40-" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall b a. (Show a, IsString b) => a -> b
show Int
maxSupported
    | Int
len Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
10 = String
"10-40"
    | Int
len Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
1 = String
"1-10"
    | Bool
otherwise = String
"0"

-- | Generate an init tx with the used seed TxIn.
genInitTxWithSeed :: HydraContext -> Gen (Tx, TxIn)
genInitTxWithSeed :: HydraContext -> Gen (Tx, TxIn)
genInitTxWithSeed HydraContext
ctx = do
  ChainContext
cctx <- HydraContext -> Gen ChainContext
pickChainContext HydraContext
ctx
  TxIn
seedTxIn <- Gen TxIn
genTxIn
  (Tx, TxIn) -> Gen (Tx, TxIn)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ChainContext -> TxIn -> [OnChainId] -> HeadParameters -> Tx
initialize ChainContext
cctx TxIn
seedTxIn (HydraContext -> [OnChainId]
ctxParticipants HydraContext
ctx) (HydraContext -> HeadParameters
ctxHeadParameters HydraContext
ctx), TxIn
seedTxIn)

-- * Helpers

mfail :: MonadFail m => Maybe a -> m a
mfail :: forall (m :: * -> *) a. MonadFail m => Maybe a -> m a
mfail = \case
  Maybe a
Nothing -> String -> m a
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"encountered Nothing"
  Just a
a -> a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a