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

-- | Model-Based testing of Hydra Head protocol implementation.
--
-- * Troubleshooting
--
-- ** Deadlocks
--
-- One of the most annoying problems one can face with those very high level properties involving multithreading and a lot
-- of complex moving parts is when the test execution deadlocks. Here is a short guide on what one can do to troubleshoort
-- this kind of issue:
--
-- * **Check generators**: `suchThat` combinator from QuickCheck is useful when one wants to refine another `Gen`erator's behaviour
--   but it can lead to deadlock if the filtering leads to no value being generated. Avoid it.
--
-- * **Dump nodes' logs**: In case of a "normal" failure of the tests, the logs from the nodes are dumped. However, if the test does
--   not even complete then no logs are produced because they are kept in memory. In this case. replacing `traceInIOSim` with
--   `traceInIOSim <> traceDebug` will ensure the logs are dumped on the `stderr`. It could be a good idea to store them in a file
--   as they can be quite large.
--
-- * **Use** `Debug.Trace.trace` liberally: Because getting a proper stack trace is hard in Haskell, esp. in pure code, sprinkling
--   `trace` statements at key points might help understand what's going on and zoom in on the culprits
--
-- * **Dump IOSim trace**: In case the deadlock (or race condition) is caused by having two or more concurrent threads competing
--   to access a resource, dumping the trace of IOSim's runtime scheduleer execution can help. io-sim generate its trace lazily which
--   means that even when it deadlocks, one can capture at least a significant prefix of the trace and dump it to `stderr`. One can
--   `map (\ t -> trace (ppEvents t) t) . traceEvents` over the `SimTrace` returned by `runSimTrace` to get some pretty-printed
--   output similar to:
--
--   @@
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventThrow AsyncCancelled
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventMask MaskedInterruptible
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventMask MaskedInterruptible
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventDeschedule Interruptible
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventTxCommitted [Labelled (TVarId 25) (Just "async-ThreadId [4]")] [] Nothing
--   Time 380.1s - ThreadId []   main          - EventTxWakeup [Labelled (TVarId 25) (Just "async-ThreadId [4]")]
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventUnblocked [ThreadId []]
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventDeschedule Yield
--   Time 380.1s - ThreadId []   main          - EventTxCommitted [] [] Nothing
--   Time 380.1s - ThreadId []   main          - EventUnblocked []
--   Time 380.1s - ThreadId []   main          - EventDeschedule Yield
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventThreadFinished
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventDeschedule Terminated
--   Time 380.1s - ThreadId []   main          - EventThreadFinished
--   @@
--
-- ** Recording trace failures
--
-- When a property fails it will dump the sequence of actions leading to the
-- failure:
--
-- @@
--   do action $ Seed {seedKeys = [("8bbc9f32e4faff669ed1561025f243649f1332902aa79ad7e6e6bbae663f332d",CardanoSigningKey {signingKey = "0400020803030302070808060405040001050408070401040604000005010603"})], seedContestationPeriod = 46s, seedDepositDeadline = 50s}
--      var2 <- action $ Init (Party {vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"})
--      action $ Deposit {headIdVar = var2, utxoToDeposit = [(CardanoSigningKey {signingKey = "0400020803030302070808060405040001050408070401040604000005010603"},valueFromList [(AdaAssetId,54862683)])], deadline = 1864-06-06 08:24:08.669152896211 UTC}
--      pure ()
-- @@
--
-- Which can be turned into a unit test after resolving most of the imports.
-- Common pitfalls are incorrect show instances (e.g. the UTCTime in deadline
-- above). Should the variables not be bound correctly, double check
-- HasVariables instances. A working example of the above output would be:
--
-- @@
--   it "troubleshoot" . withMaxSuccess 1 . flip forAllDL propHydraModel $ do
--     action $ Seed{seedKeys = [("8bbc9f32e4faff669ed1561025f243649f1332902aa79ad7e6e6bbae663f332d", CardanoSigningKey{signingKey = "0400020803030302070808060405040001050408070401040604000005010603"})], seedContestationPeriod = UnsafeContestationPeriod 46, seedDepositDeadline = UnsafeDepositDeadline 50}
--     var2 <- action $ Init (Party{vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"})
--     action $ Deposit{headIdVar = var2, utxoToDeposit = [(CardanoSigningKey{signingKey = "0400020803030302070808060405040001050408070401040604000005010603"}, valueFromList [(AdaAssetId, 54862683)])], deadline = read "1864-06-06 08:24:08.669152896211 UTC"}
--     pure ()
-- @@
module Hydra.ModelSpec where

import Hydra.Cardano.Api hiding (CardanoSigningKey (..))
import Hydra.Prelude
import Test.Hydra.Prelude hiding (after)

import Cardano.Api.UTxO qualified as UTxO
import Control.Monad.Class.MonadTimer ()
import Control.Monad.IOSim (Failure (FailureException), IOSim, SimTrace, runSimTrace, traceResult)
import Data.List (nub, (\\))
import Data.Map.Strict ((!))
import Data.Map.Strict qualified as Map
import Data.Set qualified as Set
import Data.Typeable (cast)
import Hydra.BehaviorSpec (RequeueMode (..), TestHydraClient (..), dummySimulatedChainNetwork)
import Hydra.Logging.Messages (HydraLog)
import Hydra.Model (
  Action (..),
  GlobalState (..),
  Nodes (Nodes, nodes),
  OffChainState (..),
  RunMonad,
  RunState (..),
  WorldState (..),
  genPartyKeysExactly,
  genPayment,
  genSeedWith,
  headUTxO,
  runMonad,
  toRealUTxO,
  toTxOuts,
 )
import Hydra.Model qualified as Model
import Hydra.Model.Payment (Payment (..))
import Hydra.Model.Payment qualified as Payment
import Hydra.Tx (HeadId)
import Hydra.Tx.ContestationPeriod (ContestationPeriod (..))
import Hydra.Tx.IsTx (UTxOType)
import Hydra.Tx.Party (Party (..), deriveParty)
import System.IO.Temp (writeSystemTempFile)
import System.IO.Unsafe (unsafePerformIO)
import Test.HUnit.Lang (formatFailureReason)
import Test.Hydra.Node.Fixture (alice, aliceSk)
import Test.Hydra.Tx.Fixture (fanoutOutputThreshold)
import Test.QuickCheck (Property, Testable, counterexample, forAllShrink, mapSize, noShrinking, property, suchThat, vectorOf, withMaxSuccess, within)
import Test.QuickCheck.DynamicLogic (
  DL,
  Quantification,
  action,
  anyActions_,
  forAllDL,
  forAllNonVariableQ,
  forAllQ,
  getModelStateDL,
  whereQ,
  withGenQ,
 )
import Test.QuickCheck.Gen.Unsafe (Capture (Capture), capture)
import Test.QuickCheck.Monadic (PropertyM, assert, monadic', run, stop)
import Test.QuickCheck.Property ((===))
import Test.QuickCheck.StateModel (
  ActionWithPolarity (..),
  Actions,
  Annotated (..),
  HasVariables (..),
  Step ((:=)),
  Var,
  precondition,
  runActions,
  pattern Actions,
 )
import Test.Util (printTrace, traceInIOSim)

instance HasVariables Payment.CardanoSigningKey where
  getAllVariables :: CardanoSigningKey -> Set (Any Var)
getAllVariables = CardanoSigningKey -> Set (Any Var)
forall a. Monoid a => a
mempty

spec :: Spec
spec :: Spec
spec = do
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
context String
"modeling" (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
"not generate actions with 0 Ada" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ Int -> (Actions WorldState -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
10000 Actions WorldState -> Property
propDoesNotGenerate0AdaUTxO
    String
-> ([(CardanoSigningKey, Value)]
    -> [(CardanoSigningKey, Value)] -> Property)
-> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"toRealUTxO is distributive" (([(CardanoSigningKey, Value)]
  -> [(CardanoSigningKey, Value)] -> Property)
 -> Spec)
-> ([(CardanoSigningKey, Value)]
    -> [(CardanoSigningKey, Value)] -> Property)
-> Spec
forall a b. (a -> b) -> a -> b
$ ([(CardanoSigningKey, Value)] -> UTxO Era)
-> [(CardanoSigningKey, Value)]
-> [(CardanoSigningKey, Value)]
-> Property
forall b a.
(Show b, Eq b, Semigroup a, Semigroup b) =>
(a -> b) -> a -> a -> Property
propIsDistributive [(CardanoSigningKey, Value)] -> UTxO Era
UTxOType Payment -> UTxOType Tx
toRealUTxO
    String
-> ([(CardanoSigningKey, Value)]
    -> [(CardanoSigningKey, Value)] -> Property)
-> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"toTxOuts is distributive" (([(CardanoSigningKey, Value)]
  -> [(CardanoSigningKey, Value)] -> Property)
 -> Spec)
-> ([(CardanoSigningKey, Value)]
    -> [(CardanoSigningKey, Value)] -> Property)
-> Spec
forall a b. (a -> b) -> a -> b
$ ([(CardanoSigningKey, Value)] -> [TxOut CtxUTxO])
-> [(CardanoSigningKey, Value)]
-> [(CardanoSigningKey, Value)]
-> Property
forall b a.
(Show b, Eq b, Semigroup a, Semigroup b) =>
(a -> b) -> a -> a -> Property
propIsDistributive [(CardanoSigningKey, Value)] -> [TxOut CtxUTxO]
toTxOuts
  -- The default random walk settles every deposit and decommit before the
  -- next action, see 'concurrentSettlements'.
  String -> (Actions WorldState -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"check model" Actions WorldState -> Property
propHydraModel
  String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"check model balances" Property
propCheckModelBalances
  -- This scenario seeds a head with a single party and an UTxO set of elements.
  -- See https://github.com/cardano-scaling/hydra/issues/2270
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
context String
"fanout limit" (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
"succeeds fanout with many outputs" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ Int -> Property
propFanoutLimit (Int
fanoutOutputThreshold Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"succeeds fanout with few outputs" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ Int -> Property
propFanoutLimit Int
fanoutOutputThreshold
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
context String
"logic" (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
"check conflict-free liveness" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ DL WorldState () -> Property
propDL DL WorldState ()
conflictFreeLiveness
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"fanout contains whole confirmed UTxO" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ DL WorldState () -> Property
propDL DL WorldState ()
fanoutContainsWholeConfirmedUTxO
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"parties contest to wrong closed snapshot" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ DL WorldState () -> Property
propDL DL WorldState ()
partyContestsToWrongClosedSnapshot
  -- Scripted settlement/rollback interleavings. Each drives an open head into
  -- a specific settlement race, forks the chain and then requires the head to
  -- still close and fan out its whole confirmed UTxO. Only the keys are
  -- random, so a handful of runs each is enough.
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
context String
"settlements under divergent forks" (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
"two finalized decrements are both erased by a fork" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      DL WorldState () -> Property
propScripted DL WorldState ()
twoFinalizedDecrementsErased
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"a fork erases the deposit transaction and its increment" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      DL WorldState () -> Property
propScripted DL WorldState ()
depositAndIncrementErasedThenRelanded
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"a second fork erases the re-posted increment" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      DL WorldState () -> Property
propScripted DL WorldState ()
rePostedIncrementErasedAgain
  -- Scripted fanouts of a head holding more outputs than one fanout
  -- transaction can distribute, so the node fans out in steps: driven
  -- automatically by 'Fanout' or one selection at a time by 'PartialFanout',
  -- with forks erasing steps along the way.
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
context String
"partial fanout" (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
"a manual fanout distributes the selections in turn" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      DL WorldState () -> Property
propScripted DL WorldState ()
manualPartialFanout
  -- Properties that find open bugs, pending ('xprop') until those are fixed.
  -- Re-enable them to check the fix.
  --
  -- The concurrent random walk lets several deposits and decommits settle at
  -- the same time as L2 traffic and divergent forks. It finds:
  --
  --   * A deposit that activates while a snapshot is in flight is never
  --     committed: 'DepositActivated' parks it in 'currentDepositTxId', but
  --     'onOpenChainTick' only requests a snapshot while that is 'Nothing'
  --     and 'maybeRequestNextSnapshot' only when there are local
  --     transactions. The deposit expires.
  --   * A snapshot requested while an increment or decrement is still
  --     settling can carry a stale version: a party that observed the
  --     settlement first parks the request on 'WaitOnSnapshotVersion' until
  --     its TTL drops it, and the leader never re-requests. No later snapshot
  --     confirms.
  --   * Settlements erased by a fork are not all re-posted.
  --
  -- The scripted settlement scenarios pin the last point down: only the last
  -- finalized increment/decrement is retained, the two re-post branches are
  -- alternatives instead of both, and re-posts are fire-and-forget (a later
  -- settlement is not posted again once the earlier one re-lands).
  --
  -- The scripted fanout scenarios show the same gap for a fanout in progress:
  -- after a fork erases a landed step, the node's fanout bookkeeping is ahead
  -- of the chain. Automatic mode re-posts the next step instead of the erased
  -- one, which cannot land, and manual mode posts nothing at all since it
  -- waits for the client. The head is never fully fanned out.
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
context String
"pending until the open settlement bugs are fixed" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"check model with concurrent settlements" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      DL WorldState () -> (Actions WorldState -> Property) -> Property
forall s a.
(DynLogicModel s, Testable a) =>
DL s () -> (Actions s -> a) -> Property
forAllDL DL WorldState ()
concurrentWalk Actions WorldState -> Property
propHydraModel
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"check model balances with concurrent settlements" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
within Int
30000000 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        DL WorldState () -> (Actions WorldState -> Property) -> Property
forall s a.
(DynLogicModel s, Testable a) =>
DL s () -> (Actions s -> a) -> Property
forAllDL DL WorldState ()
concurrentWalk Actions WorldState -> Property
checkModelBalances
    -- Heavy: run the deep-stress version only on nightly, where it does not
    -- compete with the rest of the suite for CPU (a starved io-sim schedule
    -- makes the driver's waits time out spuriously, cf. ServerSpec).
    (IO () -> IO ()) -> Spec -> Spec
forall a. (IO () -> IO ()) -> SpecWith a -> SpecWith a
around_ IO () -> IO ()
onlyNightly (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"check model balances under load with divergent forks @nightly" Property
propStressModelBalances
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"two finalized increments are both erased by a fork" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      DL WorldState () -> Property
propScripted DL WorldState ()
twoFinalizedIncrementsErased
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"a finalized increment is erased while the next increment is in flight" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      DL WorldState () -> Property
propScripted DL WorldState ()
finalizedIncrementErasedWithNextInFlight
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"a finalized increment and decrement are both erased by a fork" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      DL WorldState () -> Property
propScripted DL WorldState ()
finalizedIncrementAndDecrementErased
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"new settlements requested during a replay settle in order" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      DL WorldState () -> Property
propScripted DL WorldState ()
newSettlementsDuringReplay
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"a fork erases a step of an automatic fanout" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      DL WorldState () -> Property
propScripted DL WorldState ()
autoFanoutStepErased
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"a fork erases two steps of an automatic fanout" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      DL WorldState () -> Property
propScripted DL WorldState ()
autoFanoutTwoStepsErased
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"a fork erases a step of a manual fanout" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      DL WorldState () -> Property
propScripted DL WorldState ()
manualFanoutStepErased

propFanoutLimit :: Int -> Property
propFanoutLimit :: Int -> Property
propFanoutLimit Int
limit =
  Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
within Int
30000000 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ DL WorldState () -> Property
propDL (DL WorldState () -> Property) -> DL WorldState () -> Property
forall a b. (a -> b) -> a -> b
$ do
    [CardanoSigningKey]
signingKeys <- Quantification [CardanoSigningKey]
-> DL WorldState (Quantifies (Quantification [CardanoSigningKey]))
forall q s. Quantifiable q => q -> DL s (Quantifies q)
forAllQ (Quantification [CardanoSigningKey]
 -> DL WorldState (Quantifies (Quantification [CardanoSigningKey])))
-> Quantification [CardanoSigningKey]
-> DL WorldState (Quantifies (Quantification [CardanoSigningKey]))
forall a b. (a -> b) -> a -> b
$ Gen [CardanoSigningKey]
-> ([CardanoSigningKey] -> Bool)
-> ([CardanoSigningKey] -> [[CardanoSigningKey]])
-> Quantification [CardanoSigningKey]
forall a. Gen a -> (a -> Bool) -> (a -> [a]) -> Quantification a
withGenQ (Int -> Gen CardanoSigningKey -> Gen [CardanoSigningKey]
forall a. Int -> Gen a -> Gen [a]
vectorOf Int
limit (forall a. Arbitrary a => Gen a
arbitrary @Payment.CardanoSigningKey)) (Bool -> [CardanoSigningKey] -> Bool
forall a b. a -> b -> a
const Bool
True) ([[CardanoSigningKey]]
-> [CardanoSigningKey] -> [[CardanoSigningKey]]
forall a b. a -> b -> a
const [])
    let aliceCardanoSks :: NonEmpty CardanoSigningKey
aliceCardanoSks = NonEmpty CardanoSigningKey
-> Maybe (NonEmpty CardanoSigningKey) -> NonEmpty CardanoSigningKey
forall a. a -> Maybe a -> a
fromMaybe (Text -> NonEmpty CardanoSigningKey
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"propFanoutLimit: limit must be > 0") ([CardanoSigningKey] -> Maybe (NonEmpty CardanoSigningKey)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [CardanoSigningKey]
signingKeys)
    let utxo :: [(CardanoSigningKey, Value)]
utxo = (CardanoSigningKey -> (CardanoSigningKey, Value))
-> [CardanoSigningKey] -> [(CardanoSigningKey, Value)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,Lovelace -> Value
lovelaceToValue Lovelace
1_000_000) [CardanoSigningKey]
signingKeys
    DL WorldState (Var ()) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var ()) -> DL WorldState ())
-> DL WorldState (Var ()) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$
      Action WorldState () -> DL WorldState (Var ())
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState () -> DL WorldState (Var ()))
-> Action WorldState () -> DL WorldState (Var ())
forall a b. (a -> b) -> a -> b
$
        Seed
          { $sel:seedKeys:Seed :: [(Secret (SigningKey HydraKey), CardanoSigningKey)]
seedKeys = [(Secret (SigningKey HydraKey)
aliceSk, NonEmpty CardanoSigningKey -> CardanoSigningKey
forall (f :: * -> *) a. IsNonEmpty f a a "head" => f a -> a
head NonEmpty CardanoSigningKey
aliceCardanoSks)]
          , $sel:contestationPeriod:Seed :: ContestationPeriod
contestationPeriod = Natural -> ContestationPeriod
UnsafeContestationPeriod Natural
10
          , $sel:additionalUTxO:Seed :: UTxOType Payment
additionalUTxO = [(CardanoSigningKey, Value)]
UTxOType Payment
utxo
          , $sel:concurrentSettlements:Seed :: Bool
concurrentSettlements = Bool
False
          }
    Var HeadId
headId <- Action WorldState HeadId -> DL WorldState (Var HeadId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState HeadId -> DL WorldState (Var HeadId))
-> Action WorldState HeadId -> DL WorldState (Var HeadId)
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState HeadId
Init Party
alice
    DL WorldState (Var ()) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var ()) -> DL WorldState ())
-> DL WorldState (Var ()) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState () -> DL WorldState (Var ())
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState () -> DL WorldState (Var ()))
-> Action WorldState () -> DL WorldState (Var ())
forall a b. (a -> b) -> a -> b
$ Deposit{$sel:headIdVar:Seed :: Var HeadId
headIdVar = Var HeadId
headId, $sel:utxoToDeposit:Seed :: UTxOType Payment
utxoToDeposit = [(CardanoSigningKey, Value)]
UTxOType Payment
utxo}
    DL WorldState (Var ()) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var ()) -> DL WorldState ())
-> DL WorldState (Var ()) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState () -> DL WorldState (Var ())
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action Close{$sel:party:Seed :: Party
party = Party
alice}
    DL WorldState (Var ()) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var ()) -> DL WorldState ())
-> DL WorldState (Var ()) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState () -> DL WorldState (Var ())
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState () -> DL WorldState (Var ()))
-> Action WorldState () -> DL WorldState (Var ())
forall a b. (a -> b) -> a -> b
$ DiffTime -> Action WorldState ()
Wait DiffTime
3600
    DL WorldState (Var (UTxO Era)) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var (UTxO Era)) -> DL WorldState ())
-> DL WorldState (Var (UTxO Era)) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era)))
-> Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState (UTxO Era)
Fanout Party
alice

propDL :: DL WorldState () -> Property
propDL :: DL WorldState () -> Property
propDL DL WorldState ()
d = DL WorldState () -> (Actions WorldState -> Property) -> Property
forall s a.
(DynLogicModel s, Testable a) =>
DL s () -> (Actions s -> a) -> Property
forAllDL DL WorldState ()
d Actions WorldState -> Property
propHydraModel

-- | Like 'propDL' for scripted scenarios where only the keys are random.
-- Shrinking is off: it cannot simplify a fixed script, it only reruns it
-- hundreds of times with varied values (a failing run takes ~0.3s, a shrunk
-- one took minutes).
propScripted :: DL WorldState () -> Property
propScripted :: DL WorldState () -> Property
propScripted DL WorldState ()
d = Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Property -> Property
forall prop. Testable prop => prop -> Property
noShrinking (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ DL WorldState () -> (Actions WorldState -> Property) -> Property
forall s a.
(DynLogicModel s, Testable a) =>
DL s () -> (Actions s -> a) -> Property
forAllDL DL WorldState ()
d Actions WorldState -> Property
propHydraModel

-- * Settlement races under divergent forks

-- | Open a head of @n@ parties, each owning one UTxO that can be deposited,
-- and return the head id variable together with each party's deposit fuel.
--
-- Funds only enter the head through deposits (it opens empty), so every
-- scenario starts from here. The 'Wait' leaves room for deep forks that must
-- stay clear of the head-opening transactions.
openHeadWithDepositFuel :: Int -> DL WorldState (Var HeadId, [(Party, UTxOType Payment)])
openHeadWithDepositFuel :: Int -> DL WorldState (Var HeadId, [(Party, UTxOType Payment)])
openHeadWithDepositFuel Int
n = do
  [(Secret (SigningKey HydraKey), CardanoSigningKey)]
seedKeys <- Quantification [(Secret (SigningKey HydraKey), CardanoSigningKey)]
-> DL
     WorldState [(Secret (SigningKey HydraKey), CardanoSigningKey)]
forall a s.
QuantifyConstraints (HasNoVariables a) =>
Quantification a -> DL s a
forAllNonVariableQ (Quantification [(Secret (SigningKey HydraKey), CardanoSigningKey)]
 -> DL
      WorldState [(Secret (SigningKey HydraKey), CardanoSigningKey)])
-> Quantification
     [(Secret (SigningKey HydraKey), CardanoSigningKey)]
-> DL
     WorldState [(Secret (SigningKey HydraKey), CardanoSigningKey)]
forall a b. (a -> b) -> a -> b
$ Gen [(Secret (SigningKey HydraKey), CardanoSigningKey)]
-> ([(Secret (SigningKey HydraKey), CardanoSigningKey)] -> Bool)
-> ([(Secret (SigningKey HydraKey), CardanoSigningKey)]
    -> [[(Secret (SigningKey HydraKey), CardanoSigningKey)]])
-> Quantification
     [(Secret (SigningKey HydraKey), CardanoSigningKey)]
forall a. Gen a -> (a -> Bool) -> (a -> [a]) -> Quantification a
withGenQ (Int -> Gen [(Secret (SigningKey HydraKey), CardanoSigningKey)]
genPartyKeysExactly Int
n) (Bool -> [(Secret (SigningKey HydraKey), CardanoSigningKey)] -> Bool
forall a b. a -> b -> a
const Bool
True) ([[(Secret (SigningKey HydraKey), CardanoSigningKey)]]
-> [(Secret (SigningKey HydraKey), CardanoSigningKey)]
-> [[(Secret (SigningKey HydraKey), CardanoSigningKey)]]
forall a b. a -> b -> a
const [])
  let fuel :: [(Party, [(CardanoSigningKey, Value)])]
fuel = [(Secret (SigningKey HydraKey) -> Party
deriveParty Secret (SigningKey HydraKey)
hk, [(CardanoSigningKey
ck, Lovelace -> Value
lovelaceToValue Lovelace
10_000_000)]) | (Secret (SigningKey HydraKey)
hk, CardanoSigningKey
ck) <- [(Secret (SigningKey HydraKey), CardanoSigningKey)]
seedKeys]
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$
    Seed
      { [(Secret (SigningKey HydraKey), CardanoSigningKey)]
$sel:seedKeys:Seed :: [(Secret (SigningKey HydraKey), CardanoSigningKey)]
seedKeys :: [(Secret (SigningKey HydraKey), CardanoSigningKey)]
seedKeys
      , $sel:contestationPeriod:Seed :: ContestationPeriod
contestationPeriod = Natural -> ContestationPeriod
UnsafeContestationPeriod Natural
10
      , $sel:additionalUTxO:Seed :: UTxOType Payment
additionalUTxO = ((Party, [(CardanoSigningKey, Value)])
 -> [(CardanoSigningKey, Value)])
-> [(Party, [(CardanoSigningKey, Value)])]
-> [(CardanoSigningKey, Value)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Party, [(CardanoSigningKey, Value)])
-> [(CardanoSigningKey, Value)]
forall a b. (a, b) -> b
snd [(Party, [(CardanoSigningKey, Value)])]
fuel
      , $sel:concurrentSettlements:Seed :: Bool
concurrentSettlements = Bool
True
      }
  Party
leader <- case [(Party, [(CardanoSigningKey, Value)])]
fuel of
    (Party
party, [(CardanoSigningKey, Value)]
_) : [(Party, [(CardanoSigningKey, Value)])]
_ -> Party -> DL WorldState Party
forall a. a -> DL WorldState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Party
party
    [] -> Text -> DL WorldState Party
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"openHeadWithDepositFuel: no parties"
  Var HeadId
headId <- Action WorldState HeadId -> DL WorldState (Var HeadId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState HeadId -> DL WorldState (Var HeadId))
-> Action WorldState HeadId -> DL WorldState (Var HeadId)
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState HeadId
Init Party
leader
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ DiffTime -> Action WorldState ()
Model.Wait DiffTime
200
  (Var HeadId, [(Party, [(CardanoSigningKey, Value)])])
-> DL
     WorldState (Var HeadId, [(Party, [(CardanoSigningKey, Value)])])
forall a. a -> DL WorldState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Var HeadId
headId, [(Party, [(CardanoSigningKey, Value)])]
fuel)

-- | The fuel of a two-party head, see 'openHeadWithDepositFuel'.
twoParties :: [(Party, UTxOType Payment)] -> ((Party, UTxOType Payment), (Party, UTxOType Payment))
twoParties :: [(Party, UTxOType Payment)]
-> ((Party, UTxOType Payment), (Party, UTxOType Payment))
twoParties = \case
  [(Party, UTxOType Payment)
a, (Party, UTxOType Payment)
b] -> ((Party, UTxOType Payment)
a, (Party, UTxOType Payment)
b)
  [(Party, UTxOType Payment)]
other -> Text -> ((Party, UTxOType Payment), (Party, UTxOType Payment))
forall a t. (HasCallStack, IsText t) => t -> a
error (Text -> ((Party, UTxOType Payment), (Party, UTxOType Payment)))
-> Text -> ((Party, UTxOType Payment), (Party, UTxOType Payment))
forall a b. (a -> b) -> a -> b
$ Text
"expected two parties, got " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show ([(Party, [(CardanoSigningKey, Value)])] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Party, [(CardanoSigningKey, Value)])]
[(Party, UTxOType Payment)]
other)

-- | The fuel of a three-party head, see 'openHeadWithDepositFuel'.
threeParties :: [(Party, UTxOType Payment)] -> ((Party, UTxOType Payment), (Party, UTxOType Payment), (Party, UTxOType Payment))
threeParties :: [(Party, UTxOType Payment)]
-> ((Party, UTxOType Payment), (Party, UTxOType Payment),
    (Party, UTxOType Payment))
threeParties = \case
  [(Party, UTxOType Payment)
a, (Party, UTxOType Payment)
b, (Party, UTxOType Payment)
c] -> ((Party, UTxOType Payment)
a, (Party, UTxOType Payment)
b, (Party, UTxOType Payment)
c)
  [(Party, UTxOType Payment)]
other -> Text
-> ((Party, UTxOType Payment), (Party, UTxOType Payment),
    (Party, UTxOType Payment))
forall a t. (HasCallStack, IsText t) => t -> a
error (Text
 -> ((Party, UTxOType Payment), (Party, UTxOType Payment),
     (Party, UTxOType Payment)))
-> Text
-> ((Party, UTxOType Payment), (Party, UTxOType Payment),
    (Party, UTxOType Payment))
forall a b. (a -> b) -> a -> b
$ Text
"expected three parties, got " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show ([(Party, [(CardanoSigningKey, Value)])] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Party, [(CardanoSigningKey, Value)])]
[(Party, UTxOType Payment)]
other)

-- | Payment decommitting a party's deposited fuel back to itself.
decommitFuel :: UTxOType Payment -> Payment
decommitFuel :: UTxOType Payment -> Payment
decommitFuel UTxOType Payment
fuel = case UTxOType Payment
fuel of
  (CardanoSigningKey
ck, Value
value) : [(CardanoSigningKey, Value)]
_ -> Payment{$sel:from:Payment :: CardanoSigningKey
from = CardanoSigningKey
ck, $sel:to:Payment :: CardanoSigningKey
to = CardanoSigningKey
ck, Value
value :: Value
$sel:value:Payment :: Value
value}
  [] -> Text -> Payment
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"decommitFuel: no fuel"

-- | The head must still settle after the fork: confirm an L2 transaction,
-- close and fan out the whole confirmed UTxO (checked by the 'Fanout'
-- postcondition). A head wedged on an erased settlement fails here, either
-- because the close cannot land (its snapshot is ahead of the on-chain
-- version) or because the fanout does not match.
headStillSettles :: DL WorldState ()
headStillSettles :: DL WorldState ()
headStillSettles = do
  WorldState
st <- DL WorldState WorldState
forall s. DL s s
getModelStateDL
  case WorldState
st of
    WorldState{$sel:hydraState:WorldState :: WorldState -> GlobalState
hydraState = Open{}} -> do
      (Party
party, Payment
payment) <- Quantification (Party, Payment) -> DL WorldState (Party, Payment)
forall a s.
QuantifyConstraints (HasNoVariables a) =>
Quantification a -> DL s a
forAllNonVariableQ (WorldState -> Quantification (Party, Payment)
nonConflictingTx WorldState
st)
      Var Payment
tx <- Action WorldState Payment -> DL WorldState (Var Payment)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState Payment -> DL WorldState (Var Payment))
-> Action WorldState Payment -> DL WorldState (Var Payment)
forall a b. (a -> b) -> a -> b
$ Party -> Payment -> Action WorldState Payment
Model.NewTx Party
party Payment
payment
      Action WorldState () -> DL WorldState ()
eventually (Var Payment -> Action WorldState ()
ObserveConfirmedTx Var Payment
tx)
      Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState ()
Model.Close Party
party
      DL WorldState (Var (UTxO Era)) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var (UTxO Era)) -> DL WorldState ())
-> DL WorldState (Var (UTxO Era)) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era)))
-> Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState (UTxO Era)
Model.Fanout Party
party
    WorldState
_ -> () -> DL WorldState ()
forall a. a -> DL WorldState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Action WorldState ()
Model.StopTheWorld

-- | Scenario 1: two deposits settle back to back, then a fork erases both
-- increments for good (no mempool re-inclusion). Both must be re-posted.
twoFinalizedIncrementsErased :: DL WorldState ()
twoFinalizedIncrementsErased :: DL WorldState ()
twoFinalizedIncrementsErased = do
  (Var HeadId
headId, [(Party, [(CardanoSigningKey, Value)])]
fuel) <- Int -> DL WorldState (Var HeadId, [(Party, UTxOType Payment)])
openHeadWithDepositFuel Int
2
  let ((Party
_, UTxOType Payment
fuelA), (Party
_, UTxOType Payment
fuelB)) = [(Party, UTxOType Payment)]
-> ((Party, UTxOType Payment), (Party, UTxOType Payment))
twoParties [(Party, [(CardanoSigningKey, Value)])]
[(Party, UTxOType Payment)]
fuel
  Var TxId
a <- Action WorldState TxId -> DL WorldState (Var TxId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState TxId -> DL WorldState (Var TxId))
-> Action WorldState TxId -> DL WorldState (Var TxId)
forall a b. (a -> b) -> a -> b
$ Var HeadId -> UTxOType Payment -> Action WorldState TxId
Model.SubmitDeposit Var HeadId
headId UTxOType Payment
fuelA
  Var TxId
b <- Action WorldState TxId -> DL WorldState (Var TxId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState TxId -> DL WorldState (Var TxId))
-> Action WorldState TxId -> DL WorldState (Var TxId)
forall a b. (a -> b) -> a -> b
$ Var HeadId -> UTxOType Payment -> Action WorldState TxId
Model.SubmitDeposit Var HeadId
headId UTxOType Payment
fuelB
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
a
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
b
  -- Deep enough to erase both increments (a couple of blocks apart), shallow
  -- enough to keep both deposit transactions: they land back to back, at
  -- least 5 blocks (the activation period) before A's increment.
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Model.RollbackAndFork{$sel:numberOfBlocks:Seed :: Natural
numberOfBlocks = Natural
4, $sel:requeueErased:Seed :: RequeueMode
requeueErased = RequeueMode
RequeueNone}
  DL WorldState ()
headStillSettles

-- | Scenario 2: deposit B's transaction is on chain before A's increment
-- lands. Right after A settles, B's snapshot is approved and its increment is
-- in flight; a shallow fork then erases A's increment but keeps B's deposit.
-- Timing dependent by nature; the random walk covers the rest of this space.
finalizedIncrementErasedWithNextInFlight :: DL WorldState ()
finalizedIncrementErasedWithNextInFlight :: DL WorldState ()
finalizedIncrementErasedWithNextInFlight = do
  (Var HeadId
headId, [(Party, [(CardanoSigningKey, Value)])]
fuel) <- Int -> DL WorldState (Var HeadId, [(Party, UTxOType Payment)])
openHeadWithDepositFuel Int
2
  let ((Party
_, UTxOType Payment
fuelA), (Party
_, UTxOType Payment
fuelB)) = [(Party, UTxOType Payment)]
-> ((Party, UTxOType Payment), (Party, UTxOType Payment))
twoParties [(Party, [(CardanoSigningKey, Value)])]
[(Party, UTxOType Payment)]
fuel
  Var TxId
a <- Action WorldState TxId -> DL WorldState (Var TxId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState TxId -> DL WorldState (Var TxId))
-> Action WorldState TxId -> DL WorldState (Var TxId)
forall a b. (a -> b) -> a -> b
$ Var HeadId -> UTxOType Payment -> Action WorldState TxId
Model.SubmitDeposit Var HeadId
headId UTxOType Payment
fuelA
  Var TxId
b <- Action WorldState TxId -> DL WorldState (Var TxId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState TxId -> DL WorldState (Var TxId))
-> Action WorldState TxId -> DL WorldState (Var TxId)
forall a b. (a -> b) -> a -> b
$ Var HeadId -> UTxOType Payment -> Action WorldState TxId
Model.SubmitDeposit Var HeadId
headId UTxOType Payment
fuelB
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
a
  -- Fork as soon as B's snapshot is confirmed, while its increment is in
  -- flight. Deposit transactions re-land (B is still pending), the erased
  -- increment does not. B's snapshot confirms about one block after A's
  -- increment, so 2 reaches A's increment; the deposits are 8 blocks older.
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitApproved Var TxId
b
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Model.RollbackAndFork{$sel:numberOfBlocks:Seed :: Natural
numberOfBlocks = Natural
2, $sel:requeueErased:Seed :: RequeueMode
requeueErased = RequeueMode
RequeueDeposits}
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
b
  DL WorldState ()
headStillSettles

-- | Scenario 3: two decommits settle back to back (a second decommit is only
-- accepted once the first is finalized), then a fork erases both decrements.
twoFinalizedDecrementsErased :: DL WorldState ()
twoFinalizedDecrementsErased :: DL WorldState ()
twoFinalizedDecrementsErased = do
  (Var HeadId
headId, [(Party, [(CardanoSigningKey, Value)])]
fuel) <- Int -> DL WorldState (Var HeadId, [(Party, UTxOType Payment)])
openHeadWithDepositFuel Int
3
  let ((Party
partyA, UTxOType Payment
fuelA), (Party
partyB, UTxOType Payment
fuelB), (Party
_, UTxOType Payment
fuelC)) = [(Party, UTxOType Payment)]
-> ((Party, UTxOType Payment), (Party, UTxOType Payment),
    (Party, UTxOType Payment))
threeParties [(Party, [(CardanoSigningKey, Value)])]
[(Party, UTxOType Payment)]
fuel
  Var TxId
a <- Action WorldState TxId -> DL WorldState (Var TxId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState TxId -> DL WorldState (Var TxId))
-> Action WorldState TxId -> DL WorldState (Var TxId)
forall a b. (a -> b) -> a -> b
$ Var HeadId -> UTxOType Payment -> Action WorldState TxId
Model.SubmitDeposit Var HeadId
headId UTxOType Payment
fuelA
  Var TxId
b <- Action WorldState TxId -> DL WorldState (Var TxId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState TxId -> DL WorldState (Var TxId))
-> Action WorldState TxId -> DL WorldState (Var TxId)
forall a b. (a -> b) -> a -> b
$ Var HeadId -> UTxOType Payment -> Action WorldState TxId
Model.SubmitDeposit Var HeadId
headId UTxOType Payment
fuelB
  Var TxId
c <- Action WorldState TxId -> DL WorldState (Var TxId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState TxId -> DL WorldState (Var TxId))
-> Action WorldState TxId -> DL WorldState (Var TxId)
forall a b. (a -> b) -> a -> b
$ Var HeadId -> UTxOType Payment -> Action WorldState TxId
Model.SubmitDeposit Var HeadId
headId UTxOType Payment
fuelC
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
a
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
b
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
c
  Var (UTxO Era)
dA <- Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era)))
-> Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a b. (a -> b) -> a -> b
$ Party -> Payment -> Action WorldState (UTxO Era)
Model.SubmitDecommit Party
partyA (UTxOType Payment -> Payment
decommitFuel UTxOType Payment
fuelA)
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var (UTxO Era) -> Action WorldState ()
Model.ObserveDecommitFinalized Var (UTxO Era)
dA
  Var (UTxO Era)
dB <- Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era)))
-> Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a b. (a -> b) -> a -> b
$ Party -> Payment -> Action WorldState (UTxO Era)
Model.SubmitDecommit Party
partyB (UTxOType Payment -> Payment
decommitFuel UTxOType Payment
fuelB)
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var (UTxO Era) -> Action WorldState ()
Model.ObserveDecommitFinalized Var (UTxO Era)
dB
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Model.RollbackAndFork{$sel:numberOfBlocks:Seed :: Natural
numberOfBlocks = Natural
3, $sel:requeueErased:Seed :: RequeueMode
requeueErased = RequeueMode
RequeueNone}
  DL WorldState ()
headStillSettles

-- | Scenario 4: an increment and then a decrement settle in consecutive
-- versions; a fork erases both. The decrement can only re-land after the
-- increment did.
finalizedIncrementAndDecrementErased :: DL WorldState ()
finalizedIncrementAndDecrementErased :: DL WorldState ()
finalizedIncrementAndDecrementErased = do
  (Var HeadId
headId, [(Party, [(CardanoSigningKey, Value)])]
fuel) <- Int -> DL WorldState (Var HeadId, [(Party, UTxOType Payment)])
openHeadWithDepositFuel Int
2
  let ((Party
partyA, UTxOType Payment
fuelA), (Party
_, UTxOType Payment
fuelB)) = [(Party, UTxOType Payment)]
-> ((Party, UTxOType Payment), (Party, UTxOType Payment))
twoParties [(Party, [(CardanoSigningKey, Value)])]
[(Party, UTxOType Payment)]
fuel
  Var TxId
a <- Action WorldState TxId -> DL WorldState (Var TxId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState TxId -> DL WorldState (Var TxId))
-> Action WorldState TxId -> DL WorldState (Var TxId)
forall a b. (a -> b) -> a -> b
$ Var HeadId -> UTxOType Payment -> Action WorldState TxId
Model.SubmitDeposit Var HeadId
headId UTxOType Payment
fuelA
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
a
  Var TxId
b <- Action WorldState TxId -> DL WorldState (Var TxId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState TxId -> DL WorldState (Var TxId))
-> Action WorldState TxId -> DL WorldState (Var TxId)
forall a b. (a -> b) -> a -> b
$ Var HeadId -> UTxOType Payment -> Action WorldState TxId
Model.SubmitDeposit Var HeadId
headId UTxOType Payment
fuelB
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
b
  Var (UTxO Era)
dA <- Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era)))
-> Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a b. (a -> b) -> a -> b
$ Party -> Payment -> Action WorldState (UTxO Era)
Model.SubmitDecommit Party
partyA (UTxOType Payment -> Payment
decommitFuel UTxOType Payment
fuelA)
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var (UTxO Era) -> Action WorldState ()
Model.ObserveDecommitFinalized Var (UTxO Era)
dA
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Model.RollbackAndFork{$sel:numberOfBlocks:Seed :: Natural
numberOfBlocks = Natural
3, $sel:requeueErased:Seed :: RequeueMode
requeueErased = RequeueMode
RequeueNone}
  DL WorldState ()
headStillSettles

-- | While erased settlements are being re-posted, L2 keeps going: a new
-- decommit and a new deposit are requested right after the fork. Their
-- snapshots are signed at the local version, ahead of the chain, so their
-- settlements must queue behind the replayed ones and land in version order.
newSettlementsDuringReplay :: DL WorldState ()
newSettlementsDuringReplay :: DL WorldState ()
newSettlementsDuringReplay = do
  (Var HeadId
headId, [(Party, [(CardanoSigningKey, Value)])]
fuel) <- Int -> DL WorldState (Var HeadId, [(Party, UTxOType Payment)])
openHeadWithDepositFuel Int
3
  let ((Party
partyA, UTxOType Payment
fuelA), (Party
_, UTxOType Payment
fuelB), (Party
_, UTxOType Payment
fuelC)) = [(Party, UTxOType Payment)]
-> ((Party, UTxOType Payment), (Party, UTxOType Payment),
    (Party, UTxOType Payment))
threeParties [(Party, [(CardanoSigningKey, Value)])]
[(Party, UTxOType Payment)]
fuel
  Var TxId
a <- Action WorldState TxId -> DL WorldState (Var TxId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState TxId -> DL WorldState (Var TxId))
-> Action WorldState TxId -> DL WorldState (Var TxId)
forall a b. (a -> b) -> a -> b
$ Var HeadId -> UTxOType Payment -> Action WorldState TxId
Model.SubmitDeposit Var HeadId
headId UTxOType Payment
fuelA
  Var TxId
b <- Action WorldState TxId -> DL WorldState (Var TxId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState TxId -> DL WorldState (Var TxId))
-> Action WorldState TxId -> DL WorldState (Var TxId)
forall a b. (a -> b) -> a -> b
$ Var HeadId -> UTxOType Payment -> Action WorldState TxId
Model.SubmitDeposit Var HeadId
headId UTxOType Payment
fuelB
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
a
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
b
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Model.RollbackAndFork{$sel:numberOfBlocks:Seed :: Natural
numberOfBlocks = Natural
4, $sel:requeueErased:Seed :: RequeueMode
requeueErased = RequeueMode
RequeueNone}
  -- New work while the two increments are being re-posted.
  Var (UTxO Era)
dA <- Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era)))
-> Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a b. (a -> b) -> a -> b
$ Party -> Payment -> Action WorldState (UTxO Era)
Model.SubmitDecommit Party
partyA (UTxOType Payment -> Payment
decommitFuel UTxOType Payment
fuelA)
  Var TxId
c <- Action WorldState TxId -> DL WorldState (Var TxId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState TxId -> DL WorldState (Var TxId))
-> Action WorldState TxId -> DL WorldState (Var TxId)
forall a b. (a -> b) -> a -> b
$ Var HeadId -> UTxOType Payment -> Action WorldState TxId
Model.SubmitDeposit Var HeadId
headId UTxOType Payment
fuelC
  -- The erased increments re-land first, then the new settlements.
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
a
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
b
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var (UTxO Era) -> Action WorldState ()
Model.ObserveDecommitFinalized Var (UTxO Era)
dA
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
c
  DL WorldState ()
headStillSettles

-- | Scenario 5: a deep fork erases the deposit transaction itself along with
-- its increment; the mempool re-includes the deposit, so the increment must
-- be re-posted once the deposit is observed again.
depositAndIncrementErasedThenRelanded :: DL WorldState ()
depositAndIncrementErasedThenRelanded :: DL WorldState ()
depositAndIncrementErasedThenRelanded = do
  (Var HeadId
headId, [(Party, [(CardanoSigningKey, Value)])]
fuel) <- Int -> DL WorldState (Var HeadId, [(Party, UTxOType Payment)])
openHeadWithDepositFuel Int
2
  let ((Party
_, UTxOType Payment
fuelA), (Party, UTxOType Payment)
_) = [(Party, UTxOType Payment)]
-> ((Party, UTxOType Payment), (Party, UTxOType Payment))
twoParties [(Party, [(CardanoSigningKey, Value)])]
[(Party, UTxOType Payment)]
fuel
  Var TxId
a <- Action WorldState TxId -> DL WorldState (Var TxId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState TxId -> DL WorldState (Var TxId))
-> Action WorldState TxId -> DL WorldState (Var TxId)
forall a b. (a -> b) -> a -> b
$ Var HeadId -> UTxOType Payment -> Action WorldState TxId
Model.SubmitDeposit Var HeadId
headId UTxOType Payment
fuelA
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
a
  -- The deposit lands ~8 blocks before its increment (up to half a deposit
  -- period of grace, 5 blocks of activation, snapshotting); 11 reaches past
  -- it, and the fork never goes past the head-opening transactions anyway.
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Model.RollbackAndFork{$sel:numberOfBlocks:Seed :: Natural
numberOfBlocks = Natural
11, $sel:requeueErased:Seed :: RequeueMode
requeueErased = RequeueMode
RequeueAll}
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
a
  DL WorldState ()
headStillSettles

-- * Partial fanout

-- | Open a single-party head holding @n@ outputs of 1 ADA, each owned by a
-- different key, and close it. More than 'fanoutOutputThreshold' outputs do
-- not fit one fanout transaction, so the fanout takes several steps; how many
-- outputs each step carries is decided by the node from the script budget.
closedHeadWithManyOutputs :: Int -> DL WorldState (UTxOType Payment)
closedHeadWithManyOutputs :: Int -> DL WorldState (UTxOType Payment)
closedHeadWithManyOutputs Int
n = do
  [CardanoSigningKey]
ownerKeys <- Quantification [CardanoSigningKey]
-> DL WorldState [CardanoSigningKey]
forall a s.
QuantifyConstraints (HasNoVariables a) =>
Quantification a -> DL s a
forAllNonVariableQ (Quantification [CardanoSigningKey]
 -> DL WorldState [CardanoSigningKey])
-> Quantification [CardanoSigningKey]
-> DL WorldState [CardanoSigningKey]
forall a b. (a -> b) -> a -> b
$ Gen [CardanoSigningKey]
-> ([CardanoSigningKey] -> Bool)
-> ([CardanoSigningKey] -> [[CardanoSigningKey]])
-> Quantification [CardanoSigningKey]
forall a. Gen a -> (a -> Bool) -> (a -> [a]) -> Quantification a
withGenQ (Int -> Gen CardanoSigningKey -> Gen [CardanoSigningKey]
forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n Gen CardanoSigningKey
forall a. Arbitrary a => Gen a
arbitrary Gen [CardanoSigningKey]
-> ([CardanoSigningKey] -> Bool) -> Gen [CardanoSigningKey]
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n) (Int -> Bool)
-> ([CardanoSigningKey] -> Int) -> [CardanoSigningKey] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [CardanoSigningKey] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([CardanoSigningKey] -> Int)
-> ([CardanoSigningKey] -> [CardanoSigningKey])
-> [CardanoSigningKey]
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [CardanoSigningKey] -> [CardanoSigningKey]
forall a. Eq a => [a] -> [a]
nub)) (Bool -> [CardanoSigningKey] -> Bool
forall a b. a -> b -> a
const Bool
True) ([[CardanoSigningKey]]
-> [CardanoSigningKey] -> [[CardanoSigningKey]]
forall a b. a -> b -> a
const [])
  CardanoSigningKey
aliceCardanoSk <- case [CardanoSigningKey]
ownerKeys of
    CardanoSigningKey
k : [CardanoSigningKey]
_ -> CardanoSigningKey -> DL WorldState CardanoSigningKey
forall a. a -> DL WorldState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CardanoSigningKey
k
    [] -> Text -> DL WorldState CardanoSigningKey
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"closedHeadWithManyOutputs: n must be > 0"
  let utxo :: [(CardanoSigningKey, Value)]
utxo = (,Lovelace -> Value
lovelaceToValue Lovelace
1_000_000) (CardanoSigningKey -> (CardanoSigningKey, Value))
-> [CardanoSigningKey] -> [(CardanoSigningKey, Value)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CardanoSigningKey]
ownerKeys
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$
    Seed
      { $sel:seedKeys:Seed :: [(Secret (SigningKey HydraKey), CardanoSigningKey)]
seedKeys = [(Secret (SigningKey HydraKey)
aliceSk, CardanoSigningKey
aliceCardanoSk)]
      , $sel:contestationPeriod:Seed :: ContestationPeriod
contestationPeriod = Natural -> ContestationPeriod
UnsafeContestationPeriod Natural
10
      , $sel:additionalUTxO:Seed :: UTxOType Payment
additionalUTxO = [(CardanoSigningKey, Value)]
UTxOType Payment
utxo
      , $sel:concurrentSettlements:Seed :: Bool
concurrentSettlements = Bool
False
      }
  Var HeadId
headId <- Action WorldState HeadId -> DL WorldState (Var HeadId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState HeadId -> DL WorldState (Var HeadId))
-> Action WorldState HeadId -> DL WorldState (Var HeadId)
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState HeadId
Init Party
alice
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Deposit{$sel:headIdVar:Seed :: Var HeadId
headIdVar = Var HeadId
headId, $sel:utxoToDeposit:Seed :: UTxOType Payment
utxoToDeposit = [(CardanoSigningKey, Value)]
UTxOType Payment
utxo}
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Close{$sel:party:Seed :: Party
party = Party
alice}
  [(CardanoSigningKey, Value)]
-> DL WorldState [(CardanoSigningKey, Value)]
forall a. a -> DL WorldState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(CardanoSigningKey, Value)]
utxo

-- NOTE: The fork scenarios use @numberOfBlocks = 1@: it erases exactly the tip
-- block, which holds the step observed just before.

-- | The automatic fanout is in progress and a fork erases its latest step.
-- The node must re-post it (the step is expected to be reported a second
-- time) and the head must still be fully fanned out.
autoFanoutStepErased :: DL WorldState ()
autoFanoutStepErased :: DL WorldState ()
autoFanoutStepErased = do
  -- The node sizes each step by the script budget, about 23 outputs here, so
  -- this takes one partial step before the final one.
  DL WorldState (UTxOType Payment) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (UTxOType Payment) -> DL WorldState ())
-> DL WorldState (UTxOType Payment) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Int -> DL WorldState (UTxOType Payment)
closedHeadWithManyOutputs (Int
3 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
fanoutOutputThreshold)
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState ()
Model.StartFanout Party
alice
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Int -> Action WorldState ()
Model.ObservePartialFanoutSteps Int
1
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Model.RollbackAndFork{$sel:numberOfBlocks:Seed :: Natural
numberOfBlocks = Natural
1, $sel:requeueErased:Seed :: RequeueMode
requeueErased = RequeueMode
RequeueNone}
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Int -> Action WorldState ()
Model.ObservePartialFanoutSteps Int
2
  DL WorldState (Var (UTxO Era)) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var (UTxO Era)) -> DL WorldState ())
-> DL WorldState (Var (UTxO Era)) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era)))
-> Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState (UTxO Era)
Model.ObserveFanoutFinalized Party
alice
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Action WorldState ()
Model.StopTheWorld

-- | Like 'autoFanoutStepErased' but with two partial steps landed, of which
-- the fork erases the second: the node has to post that step again while its
-- bookkeeping is already at the final one.
autoFanoutTwoStepsErased :: DL WorldState ()
autoFanoutTwoStepsErased :: DL WorldState ()
autoFanoutTwoStepsErased = do
  DL WorldState (UTxOType Payment) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (UTxOType Payment) -> DL WorldState ())
-> DL WorldState (UTxOType Payment) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Int -> DL WorldState (UTxOType Payment)
closedHeadWithManyOutputs (Int
6 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
fanoutOutputThreshold)
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState ()
Model.StartFanout Party
alice
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Int -> Action WorldState ()
Model.ObservePartialFanoutSteps Int
2
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Model.RollbackAndFork{$sel:numberOfBlocks:Seed :: Natural
numberOfBlocks = Natural
1, $sel:requeueErased:Seed :: RequeueMode
requeueErased = RequeueMode
RequeueNone}
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Int -> Action WorldState ()
Model.ObservePartialFanoutSteps Int
3
  DL WorldState (Var (UTxO Era)) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var (UTxO Era)) -> DL WorldState ())
-> DL WorldState (Var (UTxO Era)) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era)))
-> Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState (UTxO Era)
Model.ObserveFanoutFinalized Party
alice
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Action WorldState ()
Model.StopTheWorld

-- | Manual mode: the client hands the node two selections in turn. The
-- second one drains the head, so it ends in the final fanout.
manualPartialFanout :: DL WorldState ()
manualPartialFanout :: DL WorldState ()
manualPartialFanout = do
  [(CardanoSigningKey, Value)]
utxo <- Int -> DL WorldState (UTxOType Payment)
closedHeadWithManyOutputs (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
fanoutOutputThreshold Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
5)
  let ([(CardanoSigningKey, Value)]
firstSelection, [(CardanoSigningKey, Value)]
rest) = Int
-> [(CardanoSigningKey, Value)]
-> ([(CardanoSigningKey, Value)], [(CardanoSigningKey, Value)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
fanoutOutputThreshold [(CardanoSigningKey, Value)]
utxo
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Party -> UTxOType Payment -> Action WorldState ()
Model.PartialFanoutStep Party
alice [(CardanoSigningKey, Value)]
UTxOType Payment
firstSelection
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Party -> UTxOType Payment -> Action WorldState ()
Model.PartialFanoutStep Party
alice [(CardanoSigningKey, Value)]
UTxOType Payment
rest
  DL WorldState (Var (UTxO Era)) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var (UTxO Era)) -> DL WorldState ())
-> DL WorldState (Var (UTxO Era)) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era)))
-> Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState (UTxO Era)
Model.ObserveFanoutFinalized Party
alice
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Action WorldState ()
Model.StopTheWorld

-- | Manual mode with a fork erasing the first selection's step before the
-- client hands over the next selection. The node must post the erased step
-- again (the step is expected to be reported a second time) before the head
-- can be drained.
manualFanoutStepErased :: DL WorldState ()
manualFanoutStepErased :: DL WorldState ()
manualFanoutStepErased = do
  [(CardanoSigningKey, Value)]
utxo <- Int -> DL WorldState (UTxOType Payment)
closedHeadWithManyOutputs (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
fanoutOutputThreshold Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
5)
  let ([(CardanoSigningKey, Value)]
firstSelection, [(CardanoSigningKey, Value)]
rest) = Int
-> [(CardanoSigningKey, Value)]
-> ([(CardanoSigningKey, Value)], [(CardanoSigningKey, Value)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
fanoutOutputThreshold [(CardanoSigningKey, Value)]
utxo
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Party -> UTxOType Payment -> Action WorldState ()
Model.PartialFanoutStep Party
alice [(CardanoSigningKey, Value)]
UTxOType Payment
firstSelection
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Model.RollbackAndFork{$sel:numberOfBlocks:Seed :: Natural
numberOfBlocks = Natural
1, $sel:requeueErased:Seed :: RequeueMode
requeueErased = RequeueMode
RequeueNone}
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Int -> Action WorldState ()
Model.ObservePartialFanoutSteps Int
2
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Party -> UTxOType Payment -> Action WorldState ()
Model.PartialFanoutStep Party
alice [(CardanoSigningKey, Value)]
UTxOType Payment
rest
  DL WorldState (Var (UTxO Era)) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var (UTxO Era)) -> DL WorldState ())
-> DL WorldState (Var (UTxO Era)) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era)))
-> Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState (UTxO Era)
Model.ObserveFanoutFinalized Party
alice
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Action WorldState ()
Model.StopTheWorld

-- | Scenario 6: a fork erases a finalized increment, the re-post lands, and
-- a second fork erases the re-posted increment as well.
rePostedIncrementErasedAgain :: DL WorldState ()
rePostedIncrementErasedAgain :: DL WorldState ()
rePostedIncrementErasedAgain = do
  (Var HeadId
headId, [(Party, [(CardanoSigningKey, Value)])]
fuel) <- Int -> DL WorldState (Var HeadId, [(Party, UTxOType Payment)])
openHeadWithDepositFuel Int
2
  let ((Party
_, UTxOType Payment
fuelA), (Party, UTxOType Payment)
_) = [(Party, UTxOType Payment)]
-> ((Party, UTxOType Payment), (Party, UTxOType Payment))
twoParties [(Party, [(CardanoSigningKey, Value)])]
[(Party, UTxOType Payment)]
fuel
  Var TxId
a <- Action WorldState TxId -> DL WorldState (Var TxId)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState TxId -> DL WorldState (Var TxId))
-> Action WorldState TxId -> DL WorldState (Var TxId)
forall a b. (a -> b) -> a -> b
$ Var HeadId -> UTxOType Payment -> Action WorldState TxId
Model.SubmitDeposit Var HeadId
headId UTxOType Payment
fuelA
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
a
  -- The fork helper lets the chain run on for three blocks afterwards, so the
  -- re-posted increment is already a few blocks deep when the second fork
  -- hits: 3 reaches it while staying clear of the deposit (5+ blocks back).
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Model.RollbackAndFork{$sel:numberOfBlocks:Seed :: Natural
numberOfBlocks = Natural
3, $sel:requeueErased:Seed :: RequeueMode
requeueErased = RequeueMode
RequeueNone}
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
a
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Model.RollbackAndFork{$sel:numberOfBlocks:Seed :: Natural
numberOfBlocks = Natural
3, $sel:requeueErased:Seed :: RequeueMode
requeueErased = RequeueMode
RequeueNone}
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized Var TxId
a
  DL WorldState ()
headStillSettles

propHydraModel :: Actions WorldState -> Property
propHydraModel :: Actions WorldState -> Property
propHydraModel Actions WorldState
actions =
  (forall s. PropertyM (RunMonad (IOSim s)) ()) -> Property
forall a.
Testable a =>
(forall s. PropertyM (RunMonad (IOSim s)) a) -> Property
runIOSimProp ((forall s. PropertyM (RunMonad (IOSim s)) ()) -> Property)
-> (forall s. PropertyM (RunMonad (IOSim s)) ()) -> Property
forall a b. (a -> b) -> a -> b
$ do
    (Annotated WorldState, Env (RunMonad (IOSim s)))
_ <- Actions WorldState
-> PropertyM
     (RunMonad (IOSim s))
     (Annotated WorldState, Env (RunMonad (IOSim s)))
forall state (m :: * -> *) e.
(StateModel state, RunModel state m, e ~ Error state,
 forall a. IsPerformResult e a) =>
Actions state -> PropertyM m (Annotated state, Env m)
runActions Actions WorldState
actions
    Bool -> PropertyM (RunMonad (IOSim s)) ()
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assert Bool
True

-- XXX: This is very similar to propHydraModel, where the assertion is
-- basically a post condition!?
propCheckModelBalances :: Property
propCheckModelBalances :: Property
propCheckModelBalances =
  Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
within Int
30000000 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    Gen (Actions WorldState)
-> (Actions WorldState -> [Actions WorldState])
-> (Actions WorldState -> Property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrink Gen (Actions WorldState)
forall a. Arbitrary a => Gen a
arbitrary Actions WorldState -> [Actions WorldState]
forall a. Arbitrary a => a -> [a]
shrink Actions WorldState -> Property
checkModelBalances

-- | Same balance consistency assertion as 'propCheckModelBalances', but over
-- longer random action sequences: heavier L2 traffic with deposits, decommits,
-- benign rollbacks and divergent-fork rollbacks interleaved. This is the
-- property meant to shake out races between settlement, re-posting and
-- rollbacks: a wedged head surfaces as a 'waitUntilMatch' timeout inside the
-- failing action, together with the shrunk action sequence and an io-sim
-- trace to diagnose from.
propStressModelBalances :: Property
propStressModelBalances :: Property
propStressModelBalances =
  Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
within Int
600000000 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
20 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
      (Int -> Int) -> Property -> Property
forall prop. Testable prop => (Int -> Int) -> prop -> Property
mapSize (Int -> Int -> Int
forall a b. a -> b -> a
const Int
100) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        DL WorldState () -> (Actions WorldState -> Property) -> Property
forall s a.
(DynLogicModel s, Testable a) =>
DL s () -> (Actions s -> a) -> Property
forAllDL DL WorldState ()
concurrentWalk Actions WorldState -> Property
checkModelBalances

-- | A random walk with 'concurrentSettlements': deposits and decommits may
-- overlap each other, L2 traffic and forks of every 'RequeueMode'.
concurrentWalk :: DL WorldState ()
concurrentWalk :: DL WorldState ()
concurrentWalk = do
  Action WorldState ()
seed <- Quantification (Action WorldState ())
-> DL WorldState (Action WorldState ())
forall a s.
QuantifyConstraints (HasNoVariables a) =>
Quantification a -> DL s a
forAllNonVariableQ (Quantification (Action WorldState ())
 -> DL WorldState (Action WorldState ()))
-> Quantification (Action WorldState ())
-> DL WorldState (Action WorldState ())
forall a b. (a -> b) -> a -> b
$ Gen (Action WorldState ())
-> (Action WorldState () -> Bool)
-> (Action WorldState () -> [Action WorldState ()])
-> Quantification (Action WorldState ())
forall a. Gen a -> (a -> Bool) -> (a -> [a]) -> Quantification a
withGenQ (Bool -> Gen (Action WorldState ())
genSeedWith Bool
True) (Bool -> Action WorldState () -> Bool
forall a b. a -> b -> a
const Bool
True) ([Action WorldState ()]
-> Action WorldState () -> [Action WorldState ()]
forall a b. a -> b -> a
const [])
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Action WorldState ()
seed
  DL WorldState ()
forall s. DL s ()
anyActions_

checkModelBalances :: Actions WorldState -> Property
checkModelBalances :: Actions WorldState -> Property
checkModelBalances Actions WorldState
actions =
  (forall s. PropertyM (RunMonad (IOSim s)) ()) -> Property
forall a.
Testable a =>
(forall s. PropertyM (RunMonad (IOSim s)) a) -> Property
runIOSimProp ((forall s. PropertyM (RunMonad (IOSim s)) ()) -> Property)
-> (forall s. PropertyM (RunMonad (IOSim s)) ()) -> Property
forall a b. (a -> b) -> a -> b
$ do
    (Annotated WorldState
metadata, Env (RunMonad (IOSim s))
_symEnv) <- Actions WorldState
-> PropertyM
     (RunMonad (IOSim s))
     (Annotated WorldState, Env (RunMonad (IOSim s)))
forall state (m :: * -> *) e.
(StateModel state, RunModel state m, e ~ Error state,
 forall a. IsPerformResult e a) =>
Actions state -> PropertyM m (Annotated state, Env m)
runActions Actions WorldState
actions
    let WorldState{[(Secret (SigningKey HydraKey), CardanoSigningKey)]
hydraParties :: [(Secret (SigningKey HydraKey), CardanoSigningKey)]
$sel:hydraParties:WorldState :: WorldState -> [(Secret (SigningKey HydraKey), CardanoSigningKey)]
hydraParties, GlobalState
$sel:hydraState:WorldState :: WorldState -> GlobalState
hydraState :: GlobalState
hydraState, [(Var TxId, UTxOType Payment)]
pendingCommits :: [(Var TxId, UTxOType Payment)]
$sel:pendingCommits:WorldState :: WorldState -> [(Var TxId, UTxOType Payment)]
pendingCommits} = Annotated WorldState -> WorldState
forall state. Annotated state -> state
underlyingState Annotated WorldState
metadata
    -- XXX: This wait time is arbitrary and corresponds to 3 "blocks" from
    -- the underlying simulated chain which produces a block every 20s. It
    -- should be enough to ensure all nodes' threads terminate their actions
    -- and those gets picked up by the chain
    RunMonad (IOSim s) () -> PropertyM (RunMonad (IOSim s)) ()
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (RunMonad (IOSim s) () -> PropertyM (RunMonad (IOSim s)) ())
-> RunMonad (IOSim s) () -> PropertyM (RunMonad (IOSim s)) ()
forall a b. (a -> b) -> a -> b
$ IOSim s () -> RunMonad (IOSim s) ()
forall (m :: * -> *) a. Monad m => m a -> RunMonad m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift IOSim s ()
forall (m :: * -> *). MonadDelay m => m ()
waitForAMinute
    let parties :: Set Party
parties = [Party] -> Set Party
forall a. Ord a => [a] -> Set a
Set.fromList ([Party] -> Set Party) -> [Party] -> Set Party
forall a b. (a -> b) -> a -> b
$ Secret (SigningKey HydraKey) -> Party
deriveParty (Secret (SigningKey HydraKey) -> Party)
-> ((Secret (SigningKey HydraKey), CardanoSigningKey)
    -> Secret (SigningKey HydraKey))
-> (Secret (SigningKey HydraKey), CardanoSigningKey)
-> Party
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Secret (SigningKey HydraKey), CardanoSigningKey)
-> Secret (SigningKey HydraKey)
forall a b. (a, b) -> a
fst ((Secret (SigningKey HydraKey), CardanoSigningKey) -> Party)
-> [(Secret (SigningKey HydraKey), CardanoSigningKey)] -> [Party]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Secret (SigningKey HydraKey), CardanoSigningKey)]
hydraParties
    Map Party (TestHydraClient Tx (IOSim s))
nodes <- RunMonad (IOSim s) (Map Party (TestHydraClient Tx (IOSim s)))
-> PropertyM
     (RunMonad (IOSim s)) (Map Party (TestHydraClient Tx (IOSim s)))
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (RunMonad (IOSim s) (Map Party (TestHydraClient Tx (IOSim s)))
 -> PropertyM
      (RunMonad (IOSim s)) (Map Party (TestHydraClient Tx (IOSim s))))
-> RunMonad (IOSim s) (Map Party (TestHydraClient Tx (IOSim s)))
-> PropertyM
     (RunMonad (IOSim s)) (Map Party (TestHydraClient Tx (IOSim s)))
forall a b. (a -> b) -> a -> b
$ (Nodes (IOSim s) -> Map Party (TestHydraClient Tx (IOSim s)))
-> RunMonad (IOSim s) (Map Party (TestHydraClient Tx (IOSim s)))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Nodes (IOSim s) -> Map Party (TestHydraClient Tx (IOSim s))
forall (m :: * -> *). Nodes m -> Map Party (TestHydraClient Tx m)
nodes
    Bool -> PropertyM (RunMonad (IOSim s)) ()
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assert (Set Party
parties Set Party -> Set Party -> Bool
forall a. Eq a => a -> a -> Bool
== Map Party (TestHydraClient Tx (IOSim s)) -> Set Party
forall k a. Map k a -> Set k
Map.keysSet Map Party (TestHydraClient Tx (IOSim s))
nodes)
    Set Party
-> (Party -> PropertyM (RunMonad (IOSim s)) ())
-> PropertyM (RunMonad (IOSim s)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Set Party
parties ((Party -> PropertyM (RunMonad (IOSim s)) ())
 -> PropertyM (RunMonad (IOSim s)) ())
-> (Party -> PropertyM (RunMonad (IOSim s)) ())
-> PropertyM (RunMonad (IOSim s)) ()
forall a b. (a -> b) -> a -> b
$ \Party
p -> do
      RunMonad (IOSim s) () -> PropertyM (RunMonad (IOSim s)) ()
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (RunMonad (IOSim s) () -> PropertyM (RunMonad (IOSim s)) ())
-> RunMonad (IOSim s) () -> PropertyM (RunMonad (IOSim s)) ()
forall a b. (a -> b) -> a -> b
$ IOSim s () -> RunMonad (IOSim s) ()
forall (m :: * -> *) a. Monad m => m a -> RunMonad m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IOSim s () -> RunMonad (IOSim s) ())
-> IOSim s () -> RunMonad (IOSim s) ()
forall a b. (a -> b) -> a -> b
$ DiffTime -> IOSim s ()
forall (m :: * -> *). MonadDelay m => DiffTime -> m ()
threadDelay DiffTime
1
      GlobalState
-> UTxOType Payment
-> Map Party (TestHydraClient Tx (IOSim s))
-> Party
-> PropertyM (RunMonad (IOSim s)) ()
forall s.
GlobalState
-> UTxOType Payment
-> Map Party (TestHydraClient Tx (IOSim s))
-> Party
-> PropertyM (RunMonad (IOSim s)) ()
assertBalancesInOpenHeadAreConsistent GlobalState
hydraState (((Var TxId, [(CardanoSigningKey, Value)])
 -> [(CardanoSigningKey, Value)])
-> [(Var TxId, [(CardanoSigningKey, Value)])]
-> [(CardanoSigningKey, Value)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Var TxId, [(CardanoSigningKey, Value)])
-> [(CardanoSigningKey, Value)]
forall a b. (a, b) -> b
snd [(Var TxId, [(CardanoSigningKey, Value)])]
[(Var TxId, UTxOType Payment)]
pendingCommits) Map Party (TestHydraClient Tx (IOSim s))
nodes Party
p
 where
  waitForAMinute :: MonadDelay m => m ()
  waitForAMinute :: forall (m :: * -> *). MonadDelay m => m ()
waitForAMinute = DiffTime -> m ()
forall (m :: * -> *). MonadDelay m => DiffTime -> m ()
threadDelay DiffTime
60

-- | The node's head UTxO must contain everything the model has as confirmed,
-- and nothing else except commits still pending in the model: those were
-- submitted but not observed as finalized ('SubmitDeposit'), so the node may
-- or may not have absorbed them yet.
assertBalancesInOpenHeadAreConsistent ::
  GlobalState ->
  -- | Pending (unobserved) commits, see 'pendingCommits'.
  UTxOType Payment ->
  Map Party (TestHydraClient Tx (IOSim s)) ->
  Party ->
  PropertyM (RunMonad (IOSim s)) ()
assertBalancesInOpenHeadAreConsistent :: forall s.
GlobalState
-> UTxOType Payment
-> Map Party (TestHydraClient Tx (IOSim s))
-> Party
-> PropertyM (RunMonad (IOSim s)) ()
assertBalancesInOpenHeadAreConsistent GlobalState
world UTxOType Payment
pendingCommitted Map Party (TestHydraClient Tx (IOSim s))
nodes Party
p = do
  Bool -> PropertyM (RunMonad (IOSim s)) ()
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assert (Key (Map Party (TestHydraClient Tx (IOSim s)))
Party
p Key (Map Party (TestHydraClient Tx (IOSim s)))
-> Map Party (TestHydraClient Tx (IOSim s)) -> Bool
forall t. StaticMap t => Key t -> t -> Bool
`member` Map Party (TestHydraClient Tx (IOSim s))
nodes)
  let node :: TestHydraClient Tx (IOSim s)
node = Map Party (TestHydraClient Tx (IOSim s))
nodes Map Party (TestHydraClient Tx (IOSim s))
-> Party -> TestHydraClient Tx (IOSim s)
forall k a. Ord k => Map k a -> k -> a
! Party
p
  case GlobalState
world of
    Open{$sel:offChainState:Start :: GlobalState -> OffChainState
offChainState = OffChainState{UTxOType Payment
confirmedUTxO :: UTxOType Payment
$sel:confirmedUTxO:OffChainState :: OffChainState -> UTxOType Payment
confirmedUTxO}} -> do
      UTxO Era
utxo <- RunMonad (IOSim s) (UTxO Era)
-> PropertyM (RunMonad (IOSim s)) (UTxO Era)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (RunMonad (IOSim s) (UTxO Era)
 -> PropertyM (RunMonad (IOSim s)) (UTxO Era))
-> RunMonad (IOSim s) (UTxO Era)
-> PropertyM (RunMonad (IOSim s)) (UTxO Era)
forall a b. (a -> b) -> a -> b
$ IOSim s (UTxO Era) -> RunMonad (IOSim s) (UTxO Era)
forall (m :: * -> *) a. Monad m => m a -> RunMonad m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IOSim s (UTxO Era) -> RunMonad (IOSim s) (UTxO Era))
-> IOSim s (UTxO Era) -> RunMonad (IOSim s) (UTxO Era)
forall a b. (a -> b) -> a -> b
$ TestHydraClient Tx (IOSim s) -> IOSim s (UTxOType Tx)
forall tx (m :: * -> *).
(IsTx tx, MonadDelay m) =>
TestHydraClient tx m -> m (UTxOType tx)
headUTxO TestHydraClient Tx (IOSim s)
node
      let sorted :: [TxOut x] -> [TxOut x]
          sorted :: forall x. [TxOut x] -> [TxOut x]
sorted = (TxOut x -> (AddressInEra, Lovelace)) -> [TxOut x] -> [TxOut x]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (\TxOut x
o -> (TxOut x -> AddressInEra
forall ctx. TxOut ctx -> AddressInEra
txOutAddress TxOut x
o, Value -> Lovelace
selectLovelace (TxOut x -> Value
forall ctx. TxOut ctx -> Value
txOutValue TxOut x
o)))
      let expected :: [TxOut CtxUTxO]
expected = [TxOut CtxUTxO] -> [TxOut CtxUTxO]
forall x. [TxOut x] -> [TxOut x]
sorted ([(CardanoSigningKey, Value)] -> [TxOut CtxUTxO]
toTxOuts [(CardanoSigningKey, Value)]
UTxOType Payment
confirmedUTxO)
      let pendingOuts :: [TxOut CtxUTxO]
pendingOuts = [TxOut CtxUTxO] -> [TxOut CtxUTxO]
forall x. [TxOut x] -> [TxOut x]
sorted ([(CardanoSigningKey, Value)] -> [TxOut CtxUTxO]
toTxOuts [(CardanoSigningKey, Value)]
UTxOType Payment
pendingCommitted)
      let actual :: [TxOut CtxUTxO]
actual = [TxOut CtxUTxO] -> [TxOut CtxUTxO]
forall x. [TxOut x] -> [TxOut x]
sorted (UTxO Era -> [TxOut CtxUTxO]
forall era. UTxO era -> [TxOut CtxUTxO era]
UTxO.txOutputs UTxO Era
utxo)
      let missing :: [TxOut CtxUTxO]
missing = [TxOut CtxUTxO]
expected [TxOut CtxUTxO] -> [TxOut CtxUTxO] -> [TxOut CtxUTxO]
forall a. Eq a => [a] -> [a] -> [a]
\\ [TxOut CtxUTxO]
actual
          unexpected :: [TxOut CtxUTxO]
unexpected = ([TxOut CtxUTxO]
actual [TxOut CtxUTxO] -> [TxOut CtxUTxO] -> [TxOut CtxUTxO]
forall a. Eq a => [a] -> [a] -> [a]
\\ [TxOut CtxUTxO]
expected) [TxOut CtxUTxO] -> [TxOut CtxUTxO] -> [TxOut CtxUTxO]
forall a. Eq a => [a] -> [a] -> [a]
\\ [TxOut CtxUTxO]
pendingOuts
      Property -> PropertyM (RunMonad (IOSim s)) ()
forall prop (m :: * -> *) a.
(Testable prop, Monad m) =>
prop -> PropertyM m a
stop (Property -> PropertyM (RunMonad (IOSim s)) ())
-> Property -> PropertyM (RunMonad (IOSim s)) ()
forall a b. (a -> b) -> a -> b
$
        ([TxOut CtxUTxO] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TxOut CtxUTxO]
missing Bool -> Bool -> Bool
&& [TxOut CtxUTxO] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TxOut CtxUTxO]
unexpected)
          Bool -> (Bool -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"actual: \n  " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n  " ((TxOut CtxUTxO -> String) -> [TxOut CtxUTxO] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TxOut CtxUTxO -> String
forall x. TxOut x -> String
renderTxOut [TxOut CtxUTxO]
actual))
          Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"expected: \n  " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n  " ((TxOut CtxUTxO -> String) -> [TxOut CtxUTxO] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TxOut CtxUTxO -> String
forall x. TxOut x -> String
renderTxOut [TxOut CtxUTxO]
expected))
          Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"pending commits: \n  " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n  " ((TxOut CtxUTxO -> String) -> [TxOut CtxUTxO] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TxOut CtxUTxO -> String
forall x. TxOut x -> String
renderTxOut [TxOut CtxUTxO]
pendingOuts))
          Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"missing: \n  " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n  " ((TxOut CtxUTxO -> String) -> [TxOut CtxUTxO] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TxOut CtxUTxO -> String
forall x. TxOut x -> String
renderTxOut [TxOut CtxUTxO]
missing))
          Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"unexpected: \n  " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n  " ((TxOut CtxUTxO -> String) -> [TxOut CtxUTxO] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TxOut CtxUTxO -> String
forall x. TxOut x -> String
renderTxOut [TxOut CtxUTxO]
unexpected))
          Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Incorrect balance for party " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Party -> String
forall b a. (Show a, IsString b) => a -> b
show Party
p)
    GlobalState
_ -> do
      () -> PropertyM (RunMonad (IOSim s)) ()
forall a. a -> PropertyM (RunMonad (IOSim s)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
 where
  renderTxOut :: TxOut x -> String
  renderTxOut :: forall x. TxOut x -> String
renderTxOut TxOut x
o =
    Text -> String
forall a. ToString a => a -> String
toString (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$
      AddressInEra -> Text
forall addr. SerialiseAddress addr => addr -> Text
serialiseAddress (TxOut x -> AddressInEra
forall ctx. TxOut ctx -> AddressInEra
txOutAddress TxOut x
o) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Value -> Text
renderValue (TxOut x -> Value
forall ctx. TxOut ctx -> Value
txOutValue TxOut x
o)

propIsDistributive :: (Show b, Eq b, Semigroup a, Semigroup b) => (a -> b) -> a -> a -> Property
propIsDistributive :: forall b a.
(Show b, Eq b, Semigroup a, Semigroup b) =>
(a -> b) -> a -> a -> Property
propIsDistributive a -> b
f a
x a
y =
  a -> b
f a
x b -> b -> b
forall a. Semigroup a => a -> a -> a
<> a -> b
f a
y b -> b -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== a -> b
f (a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
y)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"f (x <> y)   " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> b -> String
forall b a. (Show a, IsString b) => a -> b
show (a -> b
f (a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
y)))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"f x <> f y: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> b -> String
forall b a. (Show a, IsString b) => a -> b
show (a -> b
f a
x b -> b -> b
forall a. Semigroup a => a -> a -> a
<> a -> b
f a
y))

-- | Expect to see contestations when trying to close with
-- an old snapshot
--
-- XXX: Since heads open empty (funds only enter via version-bumping
-- increments), a head with funds always has 'onChainVersion' > 0 and closing
-- with the initial snapshot (open version 0) is invalid on-chain — so this
-- scenario is effectively vacuous under random actions. To stay meaningful it
-- needs the mock to close with an old /confirmed/ snapshot at the current
-- version instead of 'CloseWithInitialSnapshot'.
partyContestsToWrongClosedSnapshot :: DL WorldState ()
partyContestsToWrongClosedSnapshot :: DL WorldState ()
partyContestsToWrongClosedSnapshot = do
  DL WorldState ()
forall s. DL s ()
anyActions_
  DL WorldState ()
settlePending
  DL WorldState WorldState
forall s. DL s s
getModelStateDL DL WorldState WorldState
-> (WorldState -> DL WorldState ()) -> DL WorldState ()
forall a b.
DL WorldState a -> (a -> DL WorldState b) -> DL WorldState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    st :: WorldState
st@WorldState{$sel:hydraState:WorldState :: WorldState -> GlobalState
hydraState = Open{$sel:offChainState:Start :: GlobalState -> OffChainState
offChainState = OffChainState{UTxOType Payment
$sel:confirmedUTxO:OffChainState :: OffChainState -> UTxOType Payment
confirmedUTxO :: UTxOType Payment
confirmedUTxO}, onChainVersion :: GlobalState -> Natural
onChainVersion = Natural
0}} | Bool -> Bool
not ([(CardanoSigningKey, Value)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(CardanoSigningKey, Value)]
UTxOType Payment
confirmedUTxO) -> do
      (Party
party, Payment
payment) <- Quantification (Party, Payment) -> DL WorldState (Party, Payment)
forall a s.
QuantifyConstraints (HasNoVariables a) =>
Quantification a -> DL s a
forAllNonVariableQ (WorldState -> Quantification (Party, Payment)
nonConflictingTx WorldState
st)
      Var Payment
tx <- Action WorldState Payment -> DL WorldState (Var Payment)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState Payment -> DL WorldState (Var Payment))
-> Action WorldState Payment -> DL WorldState (Var Payment)
forall a b. (a -> b) -> a -> b
$ Party -> Payment -> Action WorldState Payment
Model.NewTx Party
party Payment
payment
      Action WorldState () -> DL WorldState ()
eventually (Var Payment -> Action WorldState ()
ObserveConfirmedTx Var Payment
tx)
      Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState ()
Model.CloseWithInitialSnapshot Party
party
      DL WorldState (Var (UTxO Era)) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var (UTxO Era)) -> DL WorldState ())
-> DL WorldState (Var (UTxO Era)) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era)))
-> Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState (UTxO Era)
Model.Fanout Party
party
    WorldState
_ -> () -> DL WorldState ()
forall a. a -> DL WorldState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Action WorldState ()
Model.StopTheWorld

-- | Given any random walk of the model, if the Head is open a NewTx getting
-- confirmed must be part of the UTxO after finalization.
fanoutContainsWholeConfirmedUTxO :: DL WorldState ()
fanoutContainsWholeConfirmedUTxO :: DL WorldState ()
fanoutContainsWholeConfirmedUTxO = do
  DL WorldState ()
forall s. DL s ()
anyActions_
  DL WorldState ()
settlePending
  DL WorldState WorldState
forall s. DL s s
getModelStateDL DL WorldState WorldState
-> (WorldState -> DL WorldState ()) -> DL WorldState ()
forall a b.
DL WorldState a -> (a -> DL WorldState b) -> DL WorldState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    st :: WorldState
st@WorldState{$sel:hydraState:WorldState :: WorldState -> GlobalState
hydraState = Open{$sel:offChainState:Start :: GlobalState -> OffChainState
offChainState = OffChainState{UTxOType Payment
$sel:confirmedUTxO:OffChainState :: OffChainState -> UTxOType Payment
confirmedUTxO :: UTxOType Payment
confirmedUTxO}}} | Bool -> Bool
not ([(CardanoSigningKey, Value)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(CardanoSigningKey, Value)]
UTxOType Payment
confirmedUTxO) -> do
      (Party
party, Payment
payment) <- Quantification (Party, Payment) -> DL WorldState (Party, Payment)
forall a s.
QuantifyConstraints (HasNoVariables a) =>
Quantification a -> DL s a
forAllNonVariableQ (WorldState -> Quantification (Party, Payment)
nonConflictingTx WorldState
st)
      Var Payment
tx <- Action WorldState Payment -> DL WorldState (Var Payment)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState Payment -> DL WorldState (Var Payment))
-> Action WorldState Payment -> DL WorldState (Var Payment)
forall a b. (a -> b) -> a -> b
$ Party -> Payment -> Action WorldState Payment
Model.NewTx Party
party Payment
payment
      Action WorldState () -> DL WorldState ()
eventually (Var Payment -> Action WorldState ()
ObserveConfirmedTx Var Payment
tx)
      Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState ()
Model.Close Party
party
      -- NOTE: The check is actually in the Model postcondition for 'Fanout'
      DL WorldState (Var (UTxO Era)) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var (UTxO Era)) -> DL WorldState ())
-> DL WorldState (Var (UTxO Era)) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era)))
-> Action WorldState (UTxO Era) -> DL WorldState (Var (UTxO Era))
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState (UTxO Era)
Model.Fanout Party
party
    WorldState
_ -> () -> DL WorldState ()
forall a. a -> DL WorldState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Action WorldState ()
Model.StopTheWorld

-- | Observe every settlement the random walk left pending, so that the steps
-- after it ('NewTx', 'Close', ...) are not blocked by their preconditions.
settlePending :: DL WorldState ()
settlePending :: DL WorldState ()
settlePending = do
  WorldState{GlobalState
$sel:hydraState:WorldState :: WorldState -> GlobalState
hydraState :: GlobalState
hydraState, [(Var TxId, UTxOType Payment)]
$sel:pendingCommits:WorldState :: WorldState -> [(Var TxId, UTxOType Payment)]
pendingCommits :: [(Var TxId, UTxOType Payment)]
pendingCommits, [(Var (UTxO Era), Payment)]
pendingDecommits :: [(Var (UTxO Era), Payment)]
$sel:pendingDecommits:WorldState :: WorldState -> [(Var (UTxO Era), Payment)]
pendingDecommits} <- DL WorldState WorldState
forall s. DL s s
getModelStateDL
  case GlobalState
hydraState of
    Open{} -> do
      [Var TxId] -> (Var TxId -> DL WorldState ()) -> DL WorldState ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ((Var TxId, [(CardanoSigningKey, Value)]) -> Var TxId
forall a b. (a, b) -> a
fst ((Var TxId, [(CardanoSigningKey, Value)]) -> Var TxId)
-> [(Var TxId, [(CardanoSigningKey, Value)])] -> [Var TxId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var TxId, [(CardanoSigningKey, Value)])]
[(Var TxId, UTxOType Payment)]
pendingCommits) ((Var TxId -> DL WorldState ()) -> DL WorldState ())
-> (Var TxId -> DL WorldState ()) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> (Var TxId -> Action WorldState ())
-> Var TxId
-> DL WorldState ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var TxId -> Action WorldState ()
Model.ObserveCommitFinalized
      [Var (UTxO Era)]
-> (Var (UTxO Era) -> DL WorldState ()) -> DL WorldState ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ((Var (UTxO Era), Payment) -> Var (UTxO Era)
forall a b. (a, b) -> a
fst ((Var (UTxO Era), Payment) -> Var (UTxO Era))
-> [(Var (UTxO Era), Payment)] -> [Var (UTxO Era)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var (UTxO Era), Payment)]
pendingDecommits) ((Var (UTxO Era) -> DL WorldState ()) -> DL WorldState ())
-> (Var (UTxO Era) -> DL WorldState ()) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> (Var (UTxO Era) -> Action WorldState ())
-> Var (UTxO Era)
-> DL WorldState ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var (UTxO Era) -> Action WorldState ()
Model.ObserveDecommitFinalized
    GlobalState
_ -> () -> DL WorldState ()
forall a. a -> DL WorldState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

nonConflictingTx :: WorldState -> Quantification (Party, Payment.Payment)
nonConflictingTx :: WorldState -> Quantification (Party, Payment)
nonConflictingTx WorldState
st =
  Gen (Party, Payment)
-> ((Party, Payment) -> Bool)
-> ((Party, Payment) -> [(Party, Payment)])
-> Quantification (Party, Payment)
forall a. Gen a -> (a -> Bool) -> (a -> [a]) -> Quantification a
withGenQ (WorldState -> Gen (Party, Payment)
genPayment WorldState
st) (Bool -> (Party, Payment) -> Bool
forall a b. a -> b -> a
const Bool
True) ([(Party, Payment)] -> (Party, Payment) -> [(Party, Payment)]
forall a b. a -> b -> a
const [])
    Quantification (Party, Payment)
-> ((Party, Payment) -> Bool) -> Quantification (Party, Payment)
forall a. Quantification a -> (a -> Bool) -> Quantification a
`whereQ` \(Party
party, Payment
tx) -> WorldState -> Action WorldState Payment -> Bool
forall state a. StateModel state => state -> Action state a -> Bool
forall a. WorldState -> Action WorldState a -> Bool
precondition WorldState
st (Party -> Payment -> Action WorldState Payment
Model.NewTx Party
party Payment
tx)

-- • Conflict-Free Liveness (Head):
--
-- In presence of a network adversary, a conflict-free execution satisfies the following condition:
-- For any transaction tx input via (new,tx), tx ∈ T i∈[n] Ci eventually holds.
--
-- NOTE: The model network is adversarial in delivery timing: each node
-- receives messages with a random per-node delay (see 'maxNetworkLatency' in
-- 'Hydra.Model.MockChain'), so nodes fall behind each other and behind their
-- own chain observations. Delivery order per node is preserved, matching the
-- production etcd network's total order — per-node reordering is deliberately
-- not modelled as it cannot happen there.
conflictFreeLiveness :: DL WorldState ()
conflictFreeLiveness :: DL WorldState ()
conflictFreeLiveness = do
  DL WorldState ()
forall s. DL s ()
anyActions_
  DL WorldState ()
settlePending
  DL WorldState WorldState
forall s. DL s s
getModelStateDL DL WorldState WorldState
-> (WorldState -> DL WorldState ()) -> DL WorldState ()
forall a b.
DL WorldState a -> (a -> DL WorldState b) -> DL WorldState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    st :: WorldState
st@WorldState{$sel:hydraState:WorldState :: WorldState -> GlobalState
hydraState = Open{$sel:offChainState:Start :: GlobalState -> OffChainState
offChainState = OffChainState{UTxOType Payment
$sel:confirmedUTxO:OffChainState :: OffChainState -> UTxOType Payment
confirmedUTxO :: UTxOType Payment
confirmedUTxO}}} | Bool -> Bool
not ([(CardanoSigningKey, Value)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(CardanoSigningKey, Value)]
UTxOType Payment
confirmedUTxO) -> do
      (Party
party, Payment
payment) <- Quantification (Party, Payment) -> DL WorldState (Party, Payment)
forall a s.
QuantifyConstraints (HasNoVariables a) =>
Quantification a -> DL s a
forAllNonVariableQ (WorldState -> Quantification (Party, Payment)
nonConflictingTx WorldState
st)
      Var Payment
tx <- Action WorldState Payment -> DL WorldState (Var Payment)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState Payment -> DL WorldState (Var Payment))
-> Action WorldState Payment -> DL WorldState (Var Payment)
forall a b. (a -> b) -> a -> b
$ Party -> Payment -> Action WorldState Payment
Model.NewTx Party
party Payment
payment
      Action WorldState () -> DL WorldState ()
eventually (Var Payment -> Action WorldState ()
ObserveConfirmedTx Var Payment
tx)
    WorldState
_ -> () -> DL WorldState ()
forall a. a -> DL WorldState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Action WorldState ()
Model.StopTheWorld

-- There cannot be a UTxO with no ADAs
-- See https://github.com/input-output-hk/cardano-ledger/blob/master/doc/explanations/min-utxo-mary.rst
propDoesNotGenerate0AdaUTxO :: Actions WorldState -> Property
propDoesNotGenerate0AdaUTxO :: Actions WorldState -> Property
propDoesNotGenerate0AdaUTxO (Actions [Step WorldState]
actions) =
  Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not ((Step WorldState -> Bool) -> [Step WorldState] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Step WorldState -> Bool
contains0AdaUTxO [Step WorldState]
actions)
 where
  contains0AdaUTxO :: Step WorldState -> Bool
  contains0AdaUTxO :: Step WorldState -> Bool
contains0AdaUTxO = \case
    Var a
_anyVar := (ActionWithPolarity (Model.Deposit Var HeadId
_ UTxOType Payment
utxo) Polarity
_) -> ((CardanoSigningKey, Value) -> Bool)
-> [(CardanoSigningKey, Value)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (CardanoSigningKey, Value) -> Bool
forall a. (a, Value) -> Bool
contains0Ada [(CardanoSigningKey, Value)]
UTxOType Payment
utxo
    Var a
_anyVar := (ActionWithPolarity (Model.SubmitDeposit Var HeadId
_ UTxOType Payment
utxo) Polarity
_) -> ((CardanoSigningKey, Value) -> Bool)
-> [(CardanoSigningKey, Value)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (CardanoSigningKey, Value) -> Bool
forall a. (a, Value) -> Bool
contains0Ada [(CardanoSigningKey, Value)]
UTxOType Payment
utxo
    Var a
_anyVar := (ActionWithPolarity (Model.NewTx Party
_anyParty Payment.Payment{Value
$sel:value:Payment :: Payment -> Value
value :: Value
value}) Polarity
_) -> Value
value Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
== Lovelace -> Value
lovelaceToValue Lovelace
0
    Step WorldState
_anyOtherStep -> Bool
False

  contains0Ada :: (a, Value) -> Bool
  contains0Ada :: forall a. (a, Value) -> Bool
contains0Ada = (Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
== Lovelace -> Value
lovelaceToValue Lovelace
0) (Value -> Bool) -> ((a, Value) -> Value) -> (a, Value) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Value) -> Value
forall a b. (a, b) -> b
snd

-- * Utilities

-- | Specialised runner similar to <monadicST https://hackage.haskell.org/package/QuickCheck-2.14.3/docs/Test-QuickCheck-Monadic.html#v:monadicST>.
runIOSimProp :: Testable a => (forall s. PropertyM (RunMonad (IOSim s)) a) -> Property
runIOSimProp :: forall a.
Testable a =>
(forall s. PropertyM (RunMonad (IOSim s)) a) -> Property
runIOSimProp forall s. PropertyM (RunMonad (IOSim s)) a
p = Gen Property -> Property
forall prop. Testable prop => prop -> Property
property ((forall s. Gen (RunMonad (IOSim s) Property)) -> Gen Property
forall a.
Testable a =>
(forall s. Gen (RunMonad (IOSim s) a)) -> Gen Property
runRunMonadIOSimGen (PropertyM (RunMonad (IOSim s)) a
-> Gen (RunMonad (IOSim s) Property)
forall a (m :: * -> *).
(Testable a, Monad m) =>
PropertyM m a -> Gen (m Property)
monadic' PropertyM (RunMonad (IOSim s)) a
forall s. PropertyM (RunMonad (IOSim s)) a
p))

-- | Similar to <runSTGen https://hackage.haskell.org/package/QuickCheck-2.14.3/docs/Test-QuickCheck-Monadic.html#v:runSTGen>
--
-- It returns `Property` rather than `Gen a`, what allows to enhance the logging
-- in case of failures.
runRunMonadIOSimGen ::
  forall a.
  Testable a =>
  (forall s. Gen (RunMonad (IOSim s) a)) ->
  Gen Property
runRunMonadIOSimGen :: forall a.
Testable a =>
(forall s. Gen (RunMonad (IOSim s) a)) -> Gen Property
runRunMonadIOSimGen forall s. Gen (RunMonad (IOSim s) a)
f = do
  Capture forall a. Gen a -> a
eval <- Gen Capture
capture
  let tr :: SimTrace a
tr = (forall s. IOSim s a) -> SimTrace a
forall a. (forall s. IOSim s a) -> SimTrace a
runSimTrace ((Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a) -> IOSim s a
forall s.
(Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a) -> IOSim s a
sim Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a
forall a. Gen a -> a
eval)
  Property -> Gen Property
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$
    SimTrace a -> Property -> Property
forall prop. Testable prop => SimTrace a -> prop -> Property
logsOnError SimTrace a
tr (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
      case Bool -> SimTrace a -> Either Failure a
forall a. Bool -> SimTrace a -> Either Failure a
traceResult Bool
False SimTrace a
tr of
        Right a
a -> a -> Property
forall prop. Testable prop => prop -> Property
property a
a
        Left (FailureException (SomeException e
ex)) ->
          case e -> Maybe HUnitFailure
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast e
ex of
            Just (HUnitFailure Maybe SrcLoc
loc FailureReason
reason) ->
              Bool
False
                Bool -> (Bool -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (FailureReason -> String
formatFailureReason FailureReason
reason)
                Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Location: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> (SrcLoc -> String) -> Maybe SrcLoc -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"unknown" SrcLoc -> String
prettySrcLoc Maybe SrcLoc
loc)
            Maybe HUnitFailure
Nothing -> String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (e -> String
forall b a. (Show a, IsString b) => a -> b
show e
ex) Bool
False
        Left Failure
ex ->
          String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Failure -> String
forall b a. (Show a, IsString b) => a -> b
show Failure
ex) Bool
False
 where
  logsOnError :: Testable prop => SimTrace a -> prop -> Property
  logsOnError :: forall prop. Testable prop => SimTrace a -> prop -> Property
logsOnError SimTrace a
tr =
    -- NOTE: Store trace dump in file when showing the counterexample. Behavior of
    -- this during shrinking is not 100% confirmed, show the trace directly if you
    -- want to be sure:
    --
    -- counterexample $ toString traceDump
    String -> prop -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String -> prop -> Property)
-> (IO String -> String) -> IO String -> prop -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO String -> String
forall a. IO a -> a
unsafePerformIO (IO String -> prop -> Property) -> IO String -> prop -> Property
forall a b. (a -> b) -> a -> b
$ do
      String
fn <- String -> String -> IO String
writeSystemTempFile String
"io-sim-trace" (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ Text -> String
forall a. ToString a => a -> String
toString Text
traceDump
      String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ String
"IOSim trace stored in: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> String
forall a. ToString a => a -> String
toString String
fn
   where
    traceDump :: Text
traceDump = Proxy (HydraLog Tx) -> SimTrace a -> Text
forall log a.
(Typeable log, ToJSON log) =>
Proxy log -> SimTrace a -> Text
printTrace (Proxy (HydraLog Tx)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (HydraLog Tx)) SimTrace a
tr

  sim ::
    forall s.
    (Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a) ->
    IOSim s a
  sim :: forall s.
(Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a) -> IOSim s a
sim Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a
eval = do
    TVar s (Nodes (IOSim s))
v <-
      String
-> Nodes (IOSim s) -> IOSim s (TVar (IOSim s) (Nodes (IOSim s)))
forall (m :: * -> *) a.
MonadLabelledSTM m =>
String -> a -> m (TVar m a)
newLabelledTVarIO
        String
"sim-nodes"
        Nodes
          { $sel:nodes:Nodes :: Map Party (TestHydraClient Tx (IOSim s))
nodes = Map Party (TestHydraClient Tx (IOSim s))
forall a. Monoid a => a
mempty
          , $sel:logger:Nodes :: Tracer (IOSim s) (HydraLog Tx)
logger = Tracer (IOSim s) (HydraLog Tx)
forall a s. Typeable a => Tracer (IOSim s) a
traceInIOSim
          , $sel:threads:Nodes :: [Async (IOSim s) ()]
threads = [Async (IOSim s) ()]
[Async s ()]
forall a. Monoid a => a
mempty
          , $sel:chain:Nodes :: SimulatedChainNetwork Tx (IOSim s)
chain = SimulatedChainNetwork Tx (IOSim s)
forall tx (m :: * -> *). SimulatedChainNetwork tx m
dummySimulatedChainNetwork
          , $sel:eventStores:Nodes :: Map
  Party
  (EventStore (StateEvent Tx) (IOSim s), IOSim s [StateEvent Tx])
eventStores = Map
  Party
  (EventStore (StateEvent Tx) (IOSim s), IOSim s [StateEvent Tx])
forall a. Monoid a => a
mempty
          , $sel:nodeThreads:Nodes :: Map Party (Async (IOSim s) ())
nodeThreads = Map Party (Async (IOSim s) ())
Map Party (Async s ())
forall a. Monoid a => a
mempty
          }
    ReaderT (RunState (IOSim s)) (IOSim s) a
-> RunState (IOSim s) -> IOSim s a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (RunMonad (IOSim s) a -> ReaderT (RunState (IOSim s)) (IOSim s) a
forall (m :: * -> *) a. RunMonad m a -> ReaderT (RunState m) m a
runMonad (Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a
eval Gen (RunMonad (IOSim s) a)
forall s. Gen (RunMonad (IOSim s) a)
f)) (TVar (IOSim s) (Nodes (IOSim s)) -> RunState (IOSim s)
forall (m :: * -> *). TVar m (Nodes m) -> RunState m
RunState TVar (IOSim s) (Nodes (IOSim s))
TVar s (Nodes (IOSim s))
v)

eventually :: Action WorldState () -> DL WorldState ()
eventually :: Action WorldState () -> DL WorldState ()
eventually Action WorldState ()
a = Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (DiffTime -> Action WorldState ()
Wait DiffTime
10) DL WorldState () -> DL WorldState () -> DL WorldState ()
forall a b. DL WorldState a -> DL WorldState b -> DL WorldState b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Action WorldState ()
a

action_ :: Typeable a => Action WorldState a -> DL WorldState ()
action_ :: forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ = DL WorldState (Var a) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var a) -> DL WorldState ())
-> (Action WorldState a -> DL WorldState (Var a))
-> Action WorldState a
-> DL WorldState ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action WorldState a -> DL WorldState (Var a)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action