{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wno-orphans #-}

#if __GLASGOW_HASKELL__ >= 910
{-# OPTIONS_GHC -Wno-x-partial #-}
#endif

-- | See 'MakeAtomic'.
module Test.Consensus.Mempool.StateMachine (tests) where

import           Cardano.Slotting.Slot
import           Control.Arrow (second)
import           Control.Concurrent.Class.MonadSTM.Strict.TChan
import           Control.Monad (void)
import           Control.Monad.Except (runExcept)
import qualified Control.Tracer as CT (Tracer (..), traceWith)
import qualified Data.Foldable as Foldable
import           Data.Function (on)
import qualified Data.Map.Strict as Map
import           Data.Maybe (fromMaybe)
import qualified Data.Measure as Measure
import           Data.Proxy
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.TreeDiff
import qualified Data.TreeDiff.OMap as TD
import           GHC.Generics
import           Ouroboros.Consensus.Block
import           Ouroboros.Consensus.HeaderValidation
import           Ouroboros.Consensus.Ledger.Basics hiding (TxIn, TxOut)
import           Ouroboros.Consensus.Ledger.SupportsMempool
import           Ouroboros.Consensus.Ledger.SupportsProtocol
                     (LedgerSupportsProtocol)
import           Ouroboros.Consensus.Ledger.Tables.Utils
import           Ouroboros.Consensus.Mempool
import           Ouroboros.Consensus.Mempool.Impl.Common (tickLedgerState)
import           Ouroboros.Consensus.Mempool.TxSeq
import           Ouroboros.Consensus.Mock.Ledger.Address
import           Ouroboros.Consensus.Mock.Ledger.Block
import           Ouroboros.Consensus.Mock.Ledger.State
import           Ouroboros.Consensus.Mock.Ledger.UTxO (Expiry, Tx, TxIn, TxOut)
import qualified Ouroboros.Consensus.Mock.Ledger.UTxO as Mock
import           Ouroboros.Consensus.Util
import           Ouroboros.Consensus.Util.Condense (condense)
import           Ouroboros.Consensus.Util.IOLike hiding (bracket)
import           Test.Cardano.Ledger.TreeDiff ()
import           Test.Consensus.Mempool.Util (TestBlock, applyTxToLedger,
                     genTxs, genValidTxs, testInitLedger,
                     testLedgerConfigNoSizeLimits)
import           Test.QuickCheck
import           Test.QuickCheck.Monadic
import           Test.StateMachine hiding ((:>))
import           Test.StateMachine.DotDrawing
import qualified Test.StateMachine.Types as QC
import           Test.StateMachine.Types (History (..), HistoryEvent (..))
import qualified Test.StateMachine.Types.Rank2 as Rank2
import           Test.Tasty
import           Test.Tasty.QuickCheck
import           Test.Util.Orphans.ToExpr ()
import           Test.Util.ToExpr ()

{-------------------------------------------------------------------------------
  Datatypes
-------------------------------------------------------------------------------}

-- | Whether the LedgerDB should be wiped out
data ModifyDB = KeepDB | ClearDB deriving ((forall x. ModifyDB -> Rep ModifyDB x)
-> (forall x. Rep ModifyDB x -> ModifyDB) -> Generic ModifyDB
forall x. Rep ModifyDB x -> ModifyDB
forall x. ModifyDB -> Rep ModifyDB x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ModifyDB -> Rep ModifyDB x
from :: forall x. ModifyDB -> Rep ModifyDB x
$cto :: forall x. Rep ModifyDB x -> ModifyDB
to :: forall x. Rep ModifyDB x -> ModifyDB
Generic, [ModifyDB] -> Expr
ModifyDB -> Expr
(ModifyDB -> Expr) -> ([ModifyDB] -> Expr) -> ToExpr ModifyDB
forall a. (a -> Expr) -> ([a] -> Expr) -> ToExpr a
$ctoExpr :: ModifyDB -> Expr
toExpr :: ModifyDB -> Expr
$clistToExpr :: [ModifyDB] -> Expr
listToExpr :: [ModifyDB] -> Expr
ToExpr, Context -> ModifyDB -> IO (Maybe ThunkInfo)
Proxy ModifyDB -> String
(Context -> ModifyDB -> IO (Maybe ThunkInfo))
-> (Context -> ModifyDB -> IO (Maybe ThunkInfo))
-> (Proxy ModifyDB -> String)
-> NoThunks ModifyDB
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> ModifyDB -> IO (Maybe ThunkInfo)
noThunks :: Context -> ModifyDB -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> ModifyDB -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> ModifyDB -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy ModifyDB -> String
showTypeOf :: Proxy ModifyDB -> String
NoThunks)

instance Arbitrary ModifyDB where
  arbitrary :: Gen ModifyDB
arbitrary = [ModifyDB] -> Gen ModifyDB
forall a. HasCallStack => [a] -> Gen a
elements [ModifyDB
KeepDB, ModifyDB
ClearDB]

keepsDB :: ModifyDB -> Bool
keepsDB :: ModifyDB -> Bool
keepsDB ModifyDB
KeepDB  = Bool
True
keepsDB ModifyDB
ClearDB = Bool
False

-- | The model
data Model blk r = Model {
    -- | The current tip on the mempool
    forall {k} blk (r :: k).
Model blk r -> TickedLedgerState blk ValuesMK
modelMempoolIntermediateState :: !(TickedLedgerState blk ValuesMK)

    -- | The current list of transactions
  , forall {k} blk (r :: k). Model blk r -> [(GenTx blk, TicketNo)]
modelTxs                      :: ![(GenTx blk, TicketNo)]

    -- | The current size of the mempool
  , forall {k} blk (r :: k). Model blk r -> TxMeasure blk
modelCurrentSize              :: !(TxMeasure blk)

  , forall {k} blk (r :: k). Model blk r -> TxMeasure blk
modelCapacity                 :: !(TxMeasure blk)

    -- | Last seen ticket number
    --
    -- This indicates how many transactions have ever been added to the mempool.
  , forall {k} blk (r :: k). Model blk r -> TicketNo
modelLastSeenTicketNo         :: !TicketNo

  , forall {k} blk (r :: k). Model blk r -> LedgerCfg (LedgerState blk)
modelConfig                   :: !(LedgerCfg (LedgerState blk))

    --  * LedgerDB

    -- | The current tip on the ledgerdb
  , forall {k} blk (r :: k). Model blk r -> LedgerState blk ValuesMK
modelLedgerDBTip              :: !(LedgerState blk ValuesMK)

    -- | The old states which are still on the LedgerDB. These should
    -- technically be ancestors of the tip, but for the mempool we don't care.
  , forall {k} blk (r :: k).
Model blk r -> Set (LedgerState blk ValuesMK)
modelReachableStates          :: !(Set (LedgerState blk ValuesMK))

    -- | States which were previously on the LedgerDB. We keep these so that
    -- 'ChangeLedger' does not generate a different state with the same hash.
  , forall {k} blk (r :: k).
Model blk r -> Set (LedgerState blk ValuesMK)
modelOtherStates              :: !(Set (LedgerState blk ValuesMK))

  }

-- | The commands used by QSM
--
-- We divide them in 'Action' which are the ones that we on purpose perform on
-- the mempool, and 'Event's which happen by external triggers. This is a mere
-- convenience, in the eyes of QSM they are the same thing.
data Command blk r =
    Action !(Action blk r)
  | Event  !(Event blk r)
  deriving ((forall (a :: k). Command blk a -> Rep1 (Command blk) a)
-> (forall (a :: k). Rep1 (Command blk) a -> Command blk a)
-> Generic1 (Command blk)
forall (a :: k). Rep1 (Command blk) a -> Command blk a
forall (a :: k). Command blk a -> Rep1 (Command blk) a
forall k blk (a :: k). Rep1 (Command blk) a -> Command blk a
forall k blk (a :: k). Command blk a -> Rep1 (Command blk) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cfrom1 :: forall k blk (a :: k). Command blk a -> Rep1 (Command blk) a
from1 :: forall (a :: k). Command blk a -> Rep1 (Command blk) a
$cto1 :: forall k blk (a :: k). Rep1 (Command blk) a -> Command blk a
to1 :: forall (a :: k). Rep1 (Command blk) a -> Command blk a
Generic1)
  deriving ((forall (p :: k -> *) (q :: k -> *).
 (forall (x :: k). p x -> q x) -> Command blk p -> Command blk q)
-> Functor (Command blk)
forall k blk (p :: k -> *) (q :: k -> *).
(forall (x :: k). p x -> q x) -> Command blk p -> Command blk q
forall k (f :: (k -> *) -> *).
(forall (p :: k -> *) (q :: k -> *).
 (forall (x :: k). p x -> q x) -> f p -> f q)
-> Functor f
forall (p :: k -> *) (q :: k -> *).
(forall (x :: k). p x -> q x) -> Command blk p -> Command blk q
$cfmap :: forall k blk (p :: k -> *) (q :: k -> *).
(forall (x :: k). p x -> q x) -> Command blk p -> Command blk q
fmap :: forall (p :: k -> *) (q :: k -> *).
(forall (x :: k). p x -> q x) -> Command blk p -> Command blk q
Rank2.Functor, (forall m (p :: k -> *).
 Monoid m =>
 (forall (x :: k). p x -> m) -> Command blk p -> m)
-> Foldable (Command blk)
forall k blk m (p :: k -> *).
Monoid m =>
(forall (x :: k). p x -> m) -> Command blk p -> m
forall m (p :: k -> *).
Monoid m =>
(forall (x :: k). p x -> m) -> Command blk p -> m
forall k (f :: (k -> *) -> *).
(forall m (p :: k -> *).
 Monoid m =>
 (forall (x :: k). p x -> m) -> f p -> m)
-> Foldable f
$cfoldMap :: forall k blk m (p :: k -> *).
Monoid m =>
(forall (x :: k). p x -> m) -> Command blk p -> m
foldMap :: forall m (p :: k -> *).
Monoid m =>
(forall (x :: k). p x -> m) -> Command blk p -> m
Rank2.Foldable, Foldable (Command blk)
Functor (Command blk)
(Functor (Command blk), Foldable (Command blk)) =>
(forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
 Applicative f =>
 (forall (a :: k). p a -> f (q a))
 -> Command blk p -> f (Command blk q))
-> Traversable (Command blk)
forall k blk. Foldable (Command blk)
forall k blk. Functor (Command blk)
forall k blk (f :: * -> *) (p :: k -> *) (q :: k -> *).
Applicative f =>
(forall (a :: k). p a -> f (q a))
-> Command blk p -> f (Command blk q)
forall k (t :: (k -> *) -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
 Applicative f =>
 (forall (a :: k). p a -> f (q a)) -> t p -> f (t q))
-> Traversable t
forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
Applicative f =>
(forall (a :: k). p a -> f (q a))
-> Command blk p -> f (Command blk q)
$ctraverse :: forall k blk (f :: * -> *) (p :: k -> *) (q :: k -> *).
Applicative f =>
(forall (a :: k). p a -> f (q a))
-> Command blk p -> f (Command blk q)
traverse :: forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
Applicative f =>
(forall (a :: k). p a -> f (q a))
-> Command blk p -> f (Command blk q)
Rank2.Traversable)

-- | Actions on the mempool
data Action blk r =
    -- | Add some transactions to the mempool
    TryAddTxs ![GenTx blk]
  | -- | Unconditionally sync with the ledger db
    SyncLedger
  | -- | Ask for the current snapshot
    GetSnapshot
  -- TODO: maybe add 'GetSnapshotFor (Point blk)', but this requires to keep
  -- track of some more states to make it meaningful.
  deriving ((forall (a :: k). Action blk a -> Rep1 (Action blk) a)
-> (forall (a :: k). Rep1 (Action blk) a -> Action blk a)
-> Generic1 (Action blk)
forall (a :: k). Rep1 (Action blk) a -> Action blk a
forall (a :: k). Action blk a -> Rep1 (Action blk) a
forall k blk (a :: k). Rep1 (Action blk) a -> Action blk a
forall k blk (a :: k). Action blk a -> Rep1 (Action blk) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cfrom1 :: forall k blk (a :: k). Action blk a -> Rep1 (Action blk) a
from1 :: forall (a :: k). Action blk a -> Rep1 (Action blk) a
$cto1 :: forall k blk (a :: k). Rep1 (Action blk) a -> Action blk a
to1 :: forall (a :: k). Rep1 (Action blk) a -> Action blk a
Generic1)
  deriving ((forall (p :: k -> *) (q :: k -> *).
 (forall (x :: k). p x -> q x) -> Action blk p -> Action blk q)
-> Functor (Action blk)
forall k blk (p :: k -> *) (q :: k -> *).
(forall (x :: k). p x -> q x) -> Action blk p -> Action blk q
forall k (f :: (k -> *) -> *).
(forall (p :: k -> *) (q :: k -> *).
 (forall (x :: k). p x -> q x) -> f p -> f q)
-> Functor f
forall (p :: k -> *) (q :: k -> *).
(forall (x :: k). p x -> q x) -> Action blk p -> Action blk q
$cfmap :: forall k blk (p :: k -> *) (q :: k -> *).
(forall (x :: k). p x -> q x) -> Action blk p -> Action blk q
fmap :: forall (p :: k -> *) (q :: k -> *).
(forall (x :: k). p x -> q x) -> Action blk p -> Action blk q
Rank2.Functor, (forall m (p :: k -> *).
 Monoid m =>
 (forall (x :: k). p x -> m) -> Action blk p -> m)
-> Foldable (Action blk)
forall k blk m (p :: k -> *).
Monoid m =>
(forall (x :: k). p x -> m) -> Action blk p -> m
forall m (p :: k -> *).
Monoid m =>
(forall (x :: k). p x -> m) -> Action blk p -> m
forall k (f :: (k -> *) -> *).
(forall m (p :: k -> *).
 Monoid m =>
 (forall (x :: k). p x -> m) -> f p -> m)
-> Foldable f
$cfoldMap :: forall k blk m (p :: k -> *).
Monoid m =>
(forall (x :: k). p x -> m) -> Action blk p -> m
foldMap :: forall m (p :: k -> *).
Monoid m =>
(forall (x :: k). p x -> m) -> Action blk p -> m
Rank2.Foldable, Foldable (Action blk)
Functor (Action blk)
(Functor (Action blk), Foldable (Action blk)) =>
(forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
 Applicative f =>
 (forall (a :: k). p a -> f (q a))
 -> Action blk p -> f (Action blk q))
-> Traversable (Action blk)
forall k blk. Foldable (Action blk)
forall k blk. Functor (Action blk)
forall k blk (f :: * -> *) (p :: k -> *) (q :: k -> *).
Applicative f =>
(forall (a :: k). p a -> f (q a))
-> Action blk p -> f (Action blk q)
forall k (t :: (k -> *) -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
 Applicative f =>
 (forall (a :: k). p a -> f (q a)) -> t p -> f (t q))
-> Traversable t
forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
Applicative f =>
(forall (a :: k). p a -> f (q a))
-> Action blk p -> f (Action blk q)
$ctraverse :: forall k blk (f :: * -> *) (p :: k -> *) (q :: k -> *).
Applicative f =>
(forall (a :: k). p a -> f (q a))
-> Action blk p -> f (Action blk q)
traverse :: forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
Applicative f =>
(forall (a :: k). p a -> f (q a))
-> Action blk p -> f (Action blk q)
Rank2.Traversable, (forall (r :: k). Action blk r -> String)
-> (forall (r :: k). Proxy (Action blk r) -> Context)
-> CommandNames (Action blk)
forall (r :: k). Proxy (Action blk r) -> Context
forall (r :: k). Action blk r -> String
forall k blk (r :: k). Proxy (Action blk r) -> Context
forall k blk (r :: k). Action blk r -> String
forall k (cmd :: k -> *).
(forall (r :: k). cmd r -> String)
-> (forall (r :: k). Proxy (cmd r) -> Context) -> CommandNames cmd
$ccmdName :: forall k blk (r :: k). Action blk r -> String
cmdName :: forall (r :: k). Action blk r -> String
$ccmdNames :: forall k blk (r :: k). Proxy (Action blk r) -> Context
cmdNames :: forall (r :: k). Proxy (Action blk r) -> Context
CommandNames)

-- | Events external to the mempool
data Event blk r = ChangeLedger
    !(LedgerState blk ValuesMK)
    !ModifyDB
  deriving ((forall (a :: k). Event blk a -> Rep1 (Event blk) a)
-> (forall (a :: k). Rep1 (Event blk) a -> Event blk a)
-> Generic1 (Event blk)
forall (a :: k). Rep1 (Event blk) a -> Event blk a
forall (a :: k). Event blk a -> Rep1 (Event blk) a
forall k blk (a :: k). Rep1 (Event blk) a -> Event blk a
forall k blk (a :: k). Event blk a -> Rep1 (Event blk) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cfrom1 :: forall k blk (a :: k). Event blk a -> Rep1 (Event blk) a
from1 :: forall (a :: k). Event blk a -> Rep1 (Event blk) a
$cto1 :: forall k blk (a :: k). Rep1 (Event blk) a -> Event blk a
to1 :: forall (a :: k). Rep1 (Event blk) a -> Event blk a
Generic1)
  deriving ((forall (p :: k -> *) (q :: k -> *).
 (forall (x :: k). p x -> q x) -> Event blk p -> Event blk q)
-> Functor (Event blk)
forall k blk (p :: k -> *) (q :: k -> *).
(forall (x :: k). p x -> q x) -> Event blk p -> Event blk q
forall k (f :: (k -> *) -> *).
(forall (p :: k -> *) (q :: k -> *).
 (forall (x :: k). p x -> q x) -> f p -> f q)
-> Functor f
forall (p :: k -> *) (q :: k -> *).
(forall (x :: k). p x -> q x) -> Event blk p -> Event blk q
$cfmap :: forall k blk (p :: k -> *) (q :: k -> *).
(forall (x :: k). p x -> q x) -> Event blk p -> Event blk q
fmap :: forall (p :: k -> *) (q :: k -> *).
(forall (x :: k). p x -> q x) -> Event blk p -> Event blk q
Rank2.Functor, (forall m (p :: k -> *).
 Monoid m =>
 (forall (x :: k). p x -> m) -> Event blk p -> m)
-> Foldable (Event blk)
forall k blk m (p :: k -> *).
Monoid m =>
(forall (x :: k). p x -> m) -> Event blk p -> m
forall m (p :: k -> *).
Monoid m =>
(forall (x :: k). p x -> m) -> Event blk p -> m
forall k (f :: (k -> *) -> *).
(forall m (p :: k -> *).
 Monoid m =>
 (forall (x :: k). p x -> m) -> f p -> m)
-> Foldable f
$cfoldMap :: forall k blk m (p :: k -> *).
Monoid m =>
(forall (x :: k). p x -> m) -> Event blk p -> m
foldMap :: forall m (p :: k -> *).
Monoid m =>
(forall (x :: k). p x -> m) -> Event blk p -> m
Rank2.Foldable, Foldable (Event blk)
Functor (Event blk)
(Functor (Event blk), Foldable (Event blk)) =>
(forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
 Applicative f =>
 (forall (a :: k). p a -> f (q a))
 -> Event blk p -> f (Event blk q))
-> Traversable (Event blk)
forall k blk. Foldable (Event blk)
forall k blk. Functor (Event blk)
forall k blk (f :: * -> *) (p :: k -> *) (q :: k -> *).
Applicative f =>
(forall (a :: k). p a -> f (q a)) -> Event blk p -> f (Event blk q)
forall k (t :: (k -> *) -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
 Applicative f =>
 (forall (a :: k). p a -> f (q a)) -> t p -> f (t q))
-> Traversable t
forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
Applicative f =>
(forall (a :: k). p a -> f (q a)) -> Event blk p -> f (Event blk q)
$ctraverse :: forall k blk (f :: * -> *) (p :: k -> *) (q :: k -> *).
Applicative f =>
(forall (a :: k). p a -> f (q a)) -> Event blk p -> f (Event blk q)
traverse :: forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
Applicative f =>
(forall (a :: k). p a -> f (q a)) -> Event blk p -> f (Event blk q)
Rank2.Traversable, (forall (r :: k). Event blk r -> String)
-> (forall (r :: k). Proxy (Event blk r) -> Context)
-> CommandNames (Event blk)
forall (r :: k). Proxy (Event blk r) -> Context
forall (r :: k). Event blk r -> String
forall k blk (r :: k). Proxy (Event blk r) -> Context
forall k blk (r :: k). Event blk r -> String
forall k (cmd :: k -> *).
(forall (r :: k). cmd r -> String)
-> (forall (r :: k). Proxy (cmd r) -> Context) -> CommandNames cmd
$ccmdName :: forall k blk (r :: k). Event blk r -> String
cmdName :: forall (r :: k). Event blk r -> String
$ccmdNames :: forall k blk (r :: k). Proxy (Event blk r) -> Context
cmdNames :: forall (r :: k). Proxy (Event blk r) -> Context
CommandNames)

instance CommandNames (Command blk) where
  cmdName :: forall (r :: k). Command blk r -> String
cmdName (Action Action blk r
action) = Action blk r -> String
forall (r :: k). Action blk r -> String
forall k (cmd :: k -> *) (r :: k).
CommandNames cmd =>
cmd r -> String
cmdName Action blk r
action
  cmdName (Event Event blk r
event)   = Event blk r -> String
forall (r :: k). Event blk r -> String
forall k (cmd :: k -> *) (r :: k).
CommandNames cmd =>
cmd r -> String
cmdName Event blk r
event

  cmdNames :: forall r. Proxy (Command blk r) -> [String]
  cmdNames :: forall {k} (r :: k). Proxy (Command blk r) -> Context
cmdNames Proxy (Command blk r)
_ = Proxy (Action blk r) -> Context
forall (r :: k). Proxy (Action blk r) -> Context
forall k (cmd :: k -> *) (r :: k).
CommandNames cmd =>
Proxy (cmd r) -> Context
cmdNames (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Action blk r))
            Context -> Context -> Context
forall a. [a] -> [a] -> [a]
++ Proxy (Event blk r) -> Context
forall (r :: k). Proxy (Event blk r) -> Context
forall k (cmd :: k -> *) (r :: k).
CommandNames cmd =>
Proxy (cmd r) -> Context
cmdNames (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Event blk r))

-- | Wether or not this test must be atomic.
--
-- The reason behind this data type is that 'TryAddTxs' is on its nature prone
-- to race-conditions. And that is OK with us. For example take the following
-- sequence of commands:
--
-- @@@
--  TryAddTxs [Tx1, Tx2] || GetSnapshot
-- @@@
--
-- If we happen to hit the following interleaving:
--
-- @@@
--  AddTx Tx1; GetSnapshot; AddTx Tx2
-- @@@
--
-- the model will never be able to reproduce the result of the snapshot.
--
-- So in order to do a meaningful testing, what we do is:
--
-- 1. Run a sequential test of actions ensuring that the responses of the model
--    and SUT match on 'GetSnaphsot'. This provides us with assurance that the
--    model works as expected on single-threaded/sequential scenarios.
--
-- 2. Run a parallel test where 'TryAddTxs' is unitary (i.e. use the 'Atomic'
--    modifier) ensuring that the responses of the model and SUT match on
--    'GetSnaphsot'. This ensures that there are no race conditions on this
--    case, or rephrased, that the operations on the mempool remain atomic even
--    if executed on separate threads.
--
-- 3. Run a parallel test where 'TryAddTxs' is not unitary (using the
--    'NonAtomic' modifier) and **NOT** checking the responses of the model
--    versus the SUT. This ensures that there are no deadlocks and no
--    errors/exceptions thrown when running in parallel.
--
-- We believe that these test cover all the interesting cases and provide enough
-- assurance on the implementation of the Mempool.
data MakeAtomic = Atomic | NonAtomic | DontCare

generator ::
  ( Arbitrary (LedgerState blk ValuesMK)
  , UnTick blk
  , StandardHash blk
  , GetTip (LedgerState blk)
  )
  => MakeAtomic
  -> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
     -- ^ Transaction generator based on an state
  -> Model blk Symbolic
  -> Maybe (Gen (Command blk Symbolic))
generator :: forall blk.
(Arbitrary (LedgerState blk ValuesMK), UnTick blk,
 StandardHash blk, GetTip (LedgerState blk)) =>
MakeAtomic
-> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
-> Model blk Symbolic
-> Maybe (Gen (Command blk Symbolic))
generator MakeAtomic
ma Int -> LedgerState blk ValuesMK -> Gen [GenTx blk]
gTxs Model blk Symbolic
model =
   Gen (Command blk Symbolic) -> Maybe (Gen (Command blk Symbolic))
forall a. a -> Maybe a
Just (Gen (Command blk Symbolic) -> Maybe (Gen (Command blk Symbolic)))
-> Gen (Command blk Symbolic) -> Maybe (Gen (Command blk Symbolic))
forall a b. (a -> b) -> a -> b
$
    [(Int, Gen (Command blk Symbolic))] -> Gen (Command blk Symbolic)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
      [(Int
100,
          Action blk Symbolic -> Command blk Symbolic
forall {k} blk (r :: k). Action blk r -> Command blk r
Action (Action blk Symbolic -> Command blk Symbolic)
-> ([GenTx blk] -> Action blk Symbolic)
-> [GenTx blk]
-> Command blk Symbolic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenTx blk] -> Action blk Symbolic
forall {k} blk (r :: k). [GenTx blk] -> Action blk r
TryAddTxs ([GenTx blk] -> Command blk Symbolic)
-> Gen [GenTx blk] -> Gen (Command blk Symbolic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case MakeAtomic
ma of
            MakeAtomic
Atomic -> do
              Int -> LedgerState blk ValuesMK -> Gen [GenTx blk]
gTxs Int
1 (LedgerState blk ValuesMK -> Gen [GenTx blk])
-> (TickedLedgerState blk ValuesMK -> LedgerState blk ValuesMK)
-> TickedLedgerState blk ValuesMK
-> Gen [GenTx blk]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TickedLedgerState blk ValuesMK -> LedgerState blk ValuesMK
forall blk (mk :: MapKind).
UnTick blk =>
TickedLedgerState blk mk -> LedgerState blk mk
forall (mk :: MapKind).
TickedLedgerState blk mk -> LedgerState blk mk
unTick (TickedLedgerState blk ValuesMK -> Gen [GenTx blk])
-> TickedLedgerState blk ValuesMK -> Gen [GenTx blk]
forall a b. (a -> b) -> a -> b
$ TickedLedgerState blk ValuesMK
modelMempoolIntermediateState
            MakeAtomic
_ -> do
              n <- Positive Int -> Int
forall a. Positive a -> a
getPositive (Positive Int -> Int) -> Gen (Positive Int) -> Gen Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Positive Int)
forall a. Arbitrary a => Gen a
arbitrary
              gTxs n . unTick $ modelMempoolIntermediateState
       )
      , (Int
10, Command blk Symbolic -> Gen (Command blk Symbolic)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Command blk Symbolic -> Gen (Command blk Symbolic))
-> Command blk Symbolic -> Gen (Command blk Symbolic)
forall a b. (a -> b) -> a -> b
$ Action blk Symbolic -> Command blk Symbolic
forall {k} blk (r :: k). Action blk r -> Command blk r
Action Action blk Symbolic
forall {k} blk (r :: k). Action blk r
SyncLedger)
      , (Int
10, do
            ls <- [Gen (LedgerState blk ValuesMK)] -> Gen (LedgerState blk ValuesMK)
forall a. HasCallStack => [Gen a] -> Gen a
oneof ([ Gen (LedgerState blk ValuesMK)
forall a. Arbitrary a => Gen a
arbitrary Gen (LedgerState blk ValuesMK)
-> (LedgerState blk ValuesMK -> Bool)
-> Gen (LedgerState blk ValuesMK)
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` ( Bool -> Bool
not
                                               (Bool -> Bool)
-> (LedgerState blk ValuesMK -> Bool)
-> LedgerState blk ValuesMK
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Point (LedgerState blk) -> Set (Point (LedgerState blk)) -> Bool)
-> Set (Point (LedgerState blk)) -> Point (LedgerState blk) -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Point (LedgerState blk) -> Set (Point (LedgerState blk)) -> Bool
forall a. Eq a => a -> Set a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (LedgerState blk ValuesMK -> Point (LedgerState blk)
forall (mk :: MapKind).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: MapKind).
GetTip l =>
l mk -> Point l
getTip LedgerState blk ValuesMK
modelLedgerDBTip
                                                            Point (LedgerState blk)
-> Set (Point (LedgerState blk)) -> Set (Point (LedgerState blk))
forall a. Ord a => a -> Set a -> Set a
`Set.insert` (LedgerState blk ValuesMK -> Point (LedgerState blk))
-> Set (LedgerState blk ValuesMK) -> Set (Point (LedgerState blk))
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map LedgerState blk ValuesMK -> Point (LedgerState blk)
forall (mk :: MapKind).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: MapKind).
GetTip l =>
l mk -> Point l
getTip (Set (LedgerState blk ValuesMK)
modelOtherStates
                                                                                         Set (LedgerState blk ValuesMK)
-> Set (LedgerState blk ValuesMK) -> Set (LedgerState blk ValuesMK)
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set (LedgerState blk ValuesMK)
modelReachableStates))
                                               (Point (LedgerState blk) -> Bool)
-> (LedgerState blk ValuesMK -> Point (LedgerState blk))
-> LedgerState blk ValuesMK
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerState blk ValuesMK -> Point (LedgerState blk)
forall (mk :: MapKind).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: MapKind).
GetTip l =>
l mk -> Point l
getTip)
                        ] [Gen (LedgerState blk ValuesMK)]
-> [Gen (LedgerState blk ValuesMK)]
-> [Gen (LedgerState blk ValuesMK)]
forall a. [a] -> [a] -> [a]
++ (if Set (LedgerState blk ValuesMK) -> Bool
forall a. Set a -> Bool
Set.null Set (LedgerState blk ValuesMK)
modelReachableStates then [] else [[LedgerState blk ValuesMK] -> Gen (LedgerState blk ValuesMK)
forall a. HasCallStack => [a] -> Gen a
elements (Set (LedgerState blk ValuesMK) -> [LedgerState blk ValuesMK]
forall a. Set a -> [a]
Set.toList Set (LedgerState blk ValuesMK)
modelReachableStates)])
                          [Gen (LedgerState blk ValuesMK)]
-> [Gen (LedgerState blk ValuesMK)]
-> [Gen (LedgerState blk ValuesMK)]
forall a. [a] -> [a] -> [a]
++ (if Set (LedgerState blk ValuesMK) -> Bool
forall a. Set a -> Bool
Set.null Set (LedgerState blk ValuesMK)
modelOtherStates then [] else [[LedgerState blk ValuesMK] -> Gen (LedgerState blk ValuesMK)
forall a. HasCallStack => [a] -> Gen a
elements (Set (LedgerState blk ValuesMK) -> [LedgerState blk ValuesMK]
forall a. Set a -> [a]
Set.toList Set (LedgerState blk ValuesMK)
modelOtherStates)])
                        )
                         Gen (LedgerState blk ValuesMK)
-> (LedgerState blk ValuesMK -> Bool)
-> Gen (LedgerState blk ValuesMK)
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Bool -> Bool
not (Bool -> Bool)
-> (LedgerState blk ValuesMK -> Bool)
-> LedgerState blk ValuesMK
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Point (LedgerState blk) -> Point (LedgerState blk) -> Bool
forall a. Eq a => a -> a -> Bool
== (LedgerState blk ValuesMK -> Point (LedgerState blk)
forall (mk :: MapKind).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: MapKind).
GetTip l =>
l mk -> Point l
getTip LedgerState blk ValuesMK
modelLedgerDBTip)) (Point (LedgerState blk) -> Bool)
-> (LedgerState blk ValuesMK -> Point (LedgerState blk))
-> LedgerState blk ValuesMK
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerState blk ValuesMK -> Point (LedgerState blk)
forall (mk :: MapKind).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: MapKind).
GetTip l =>
l mk -> Point l
getTip)
            Event . ChangeLedger ls <$> arbitrary)
      , (Int
10, Command blk Symbolic -> Gen (Command blk Symbolic)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Command blk Symbolic -> Gen (Command blk Symbolic))
-> Command blk Symbolic -> Gen (Command blk Symbolic)
forall a b. (a -> b) -> a -> b
$ Action blk Symbolic -> Command blk Symbolic
forall {k} blk (r :: k). Action blk r -> Command blk r
Action Action blk Symbolic
forall {k} blk (r :: k). Action blk r
GetSnapshot)
      ]
  where
    Model{
        TickedLedgerState blk ValuesMK
modelMempoolIntermediateState :: forall {k} blk (r :: k).
Model blk r -> TickedLedgerState blk ValuesMK
modelMempoolIntermediateState :: TickedLedgerState blk ValuesMK
modelMempoolIntermediateState
      , LedgerState blk ValuesMK
modelLedgerDBTip :: forall {k} blk (r :: k). Model blk r -> LedgerState blk ValuesMK
modelLedgerDBTip :: LedgerState blk ValuesMK
modelLedgerDBTip
      , Set (LedgerState blk ValuesMK)
modelReachableStates :: forall {k} blk (r :: k).
Model blk r -> Set (LedgerState blk ValuesMK)
modelReachableStates :: Set (LedgerState blk ValuesMK)
modelReachableStates
      , Set (LedgerState blk ValuesMK)
modelOtherStates :: forall {k} blk (r :: k).
Model blk r -> Set (LedgerState blk ValuesMK)
modelOtherStates :: Set (LedgerState blk ValuesMK)
modelOtherStates
    } = Model blk Symbolic
model

data Response blk r =
    -- | Nothing to tell
    Void
  | -- | Return the contents of a snapshot
    GotSnapshot ![(GenTx blk, TicketNo)]
  deriving ((forall (a :: k). Response blk a -> Rep1 (Response blk) a)
-> (forall (a :: k). Rep1 (Response blk) a -> Response blk a)
-> Generic1 (Response blk)
forall (a :: k). Rep1 (Response blk) a -> Response blk a
forall (a :: k). Response blk a -> Rep1 (Response blk) a
forall k blk (a :: k). Rep1 (Response blk) a -> Response blk a
forall k blk (a :: k). Response blk a -> Rep1 (Response blk) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cfrom1 :: forall k blk (a :: k). Response blk a -> Rep1 (Response blk) a
from1 :: forall (a :: k). Response blk a -> Rep1 (Response blk) a
$cto1 :: forall k blk (a :: k). Rep1 (Response blk) a -> Response blk a
to1 :: forall (a :: k). Rep1 (Response blk) a -> Response blk a
Generic1)
  deriving ((forall (p :: k -> *) (q :: k -> *).
 (forall (x :: k). p x -> q x) -> Response blk p -> Response blk q)
-> Functor (Response blk)
forall k blk (p :: k -> *) (q :: k -> *).
(forall (x :: k). p x -> q x) -> Response blk p -> Response blk q
forall k (f :: (k -> *) -> *).
(forall (p :: k -> *) (q :: k -> *).
 (forall (x :: k). p x -> q x) -> f p -> f q)
-> Functor f
forall (p :: k -> *) (q :: k -> *).
(forall (x :: k). p x -> q x) -> Response blk p -> Response blk q
$cfmap :: forall k blk (p :: k -> *) (q :: k -> *).
(forall (x :: k). p x -> q x) -> Response blk p -> Response blk q
fmap :: forall (p :: k -> *) (q :: k -> *).
(forall (x :: k). p x -> q x) -> Response blk p -> Response blk q
Rank2.Functor, (forall m (p :: k -> *).
 Monoid m =>
 (forall (x :: k). p x -> m) -> Response blk p -> m)
-> Foldable (Response blk)
forall k blk m (p :: k -> *).
Monoid m =>
(forall (x :: k). p x -> m) -> Response blk p -> m
forall m (p :: k -> *).
Monoid m =>
(forall (x :: k). p x -> m) -> Response blk p -> m
forall k (f :: (k -> *) -> *).
(forall m (p :: k -> *).
 Monoid m =>
 (forall (x :: k). p x -> m) -> f p -> m)
-> Foldable f
$cfoldMap :: forall k blk m (p :: k -> *).
Monoid m =>
(forall (x :: k). p x -> m) -> Response blk p -> m
foldMap :: forall m (p :: k -> *).
Monoid m =>
(forall (x :: k). p x -> m) -> Response blk p -> m
Rank2.Foldable, Foldable (Response blk)
Functor (Response blk)
(Functor (Response blk), Foldable (Response blk)) =>
(forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
 Applicative f =>
 (forall (a :: k). p a -> f (q a))
 -> Response blk p -> f (Response blk q))
-> Traversable (Response blk)
forall k blk. Foldable (Response blk)
forall k blk. Functor (Response blk)
forall k blk (f :: * -> *) (p :: k -> *) (q :: k -> *).
Applicative f =>
(forall (a :: k). p a -> f (q a))
-> Response blk p -> f (Response blk q)
forall k (t :: (k -> *) -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
 Applicative f =>
 (forall (a :: k). p a -> f (q a)) -> t p -> f (t q))
-> Traversable t
forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
Applicative f =>
(forall (a :: k). p a -> f (q a))
-> Response blk p -> f (Response blk q)
$ctraverse :: forall k blk (f :: * -> *) (p :: k -> *) (q :: k -> *).
Applicative f =>
(forall (a :: k). p a -> f (q a))
-> Response blk p -> f (Response blk q)
traverse :: forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
Applicative f =>
(forall (a :: k). p a -> f (q a))
-> Response blk p -> f (Response blk q)
Rank2.Traversable)

{-------------------------------------------------------------------------------
  Model side
-------------------------------------------------------------------------------}

initModel ::
  ( LedgerSupportsMempool blk
  , ValidateEnvelope blk
  )
  => LedgerConfig blk
  -> TxMeasure blk
  -> LedgerState blk ValuesMK
  -> Model blk r
initModel :: forall {k} blk (r :: k).
(LedgerSupportsMempool blk, ValidateEnvelope blk) =>
LedgerConfig blk
-> TxMeasure blk -> LedgerState blk ValuesMK -> Model blk r
initModel LedgerConfig blk
cfg TxMeasure blk
capacity LedgerState blk ValuesMK
initialState =
  Model {
    modelMempoolIntermediateState :: TickedLedgerState blk ValuesMK
modelMempoolIntermediateState = TickedLedgerState blk ValuesMK
ticked
  , modelReachableStates :: Set (LedgerState blk ValuesMK)
modelReachableStates          = Set (LedgerState blk ValuesMK)
forall a. Set a
Set.empty
  , modelLedgerDBTip :: LedgerState blk ValuesMK
modelLedgerDBTip              = LedgerState blk ValuesMK
initialState
  , modelTxs :: [(GenTx blk, TicketNo)]
modelTxs                      = []
  , modelCurrentSize :: TxMeasure blk
modelCurrentSize              = TxMeasure blk
forall a. Measure a => a
Measure.zero
  , modelLastSeenTicketNo :: TicketNo
modelLastSeenTicketNo         = TicketNo
zeroTicketNo
  , modelCapacity :: TxMeasure blk
modelCapacity                 = TxMeasure blk
capacity
  , modelConfig :: LedgerConfig blk
modelConfig                   = LedgerConfig blk
cfg
  , modelOtherStates :: Set (LedgerState blk ValuesMK)
modelOtherStates              = Set (LedgerState blk ValuesMK)
forall a. Set a
Set.empty
  }
  where ticked :: TickedLedgerState blk ValuesMK
ticked = LedgerConfig blk
-> LedgerState blk ValuesMK -> TickedLedgerState blk ValuesMK
forall blk.
(ValidateEnvelope blk, LedgerSupportsMempool blk) =>
LedgerConfig blk
-> LedgerState blk ValuesMK -> TickedLedgerState blk ValuesMK
tick LedgerConfig blk
cfg LedgerState blk ValuesMK
initialState

mock ::
     Model blk Symbolic
  -> Command blk Symbolic
  -> GenSym (Response blk Symbolic)
mock :: forall blk.
Model blk Symbolic
-> Command blk Symbolic -> GenSym (Response blk Symbolic)
mock Model blk Symbolic
model = \case
  Action (TryAddTxs [GenTx blk]
_)     -> Response blk Symbolic -> GenSym (Response blk Symbolic)
forall a. a -> GenSym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Response blk Symbolic
forall {k} blk (r :: k). Response blk r
Void
  Action Action blk Symbolic
SyncLedger        -> Response blk Symbolic -> GenSym (Response blk Symbolic)
forall a. a -> GenSym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Response blk Symbolic
forall {k} blk (r :: k). Response blk r
Void
  Action Action blk Symbolic
GetSnapshot       -> Response blk Symbolic -> GenSym (Response blk Symbolic)
forall a. a -> GenSym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Response blk Symbolic -> GenSym (Response blk Symbolic))
-> Response blk Symbolic -> GenSym (Response blk Symbolic)
forall a b. (a -> b) -> a -> b
$ [(GenTx blk, TicketNo)] -> Response blk Symbolic
forall {k} blk (r :: k). [(GenTx blk, TicketNo)] -> Response blk r
GotSnapshot ([(GenTx blk, TicketNo)] -> Response blk Symbolic)
-> [(GenTx blk, TicketNo)] -> Response blk Symbolic
forall a b. (a -> b) -> a -> b
$ Model blk Symbolic -> [(GenTx blk, TicketNo)]
forall {k} blk (r :: k). Model blk r -> [(GenTx blk, TicketNo)]
modelTxs Model blk Symbolic
model
  Event (ChangeLedger LedgerState blk ValuesMK
_ ModifyDB
_) -> Response blk Symbolic -> GenSym (Response blk Symbolic)
forall a. a -> GenSym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Response blk Symbolic
forall {k} blk (r :: k). Response blk r
Void

{-------------------------------------------------------------------------------
  Transitions
-------------------------------------------------------------------------------}

doSync ::
  ( ValidateEnvelope blk
  , LedgerSupportsMempool blk
  , Eq (TickedLedgerState blk ValuesMK)
  )
  => Model blk r
  -> Model blk r
doSync :: forall {k} blk (r :: k).
(ValidateEnvelope blk, LedgerSupportsMempool blk,
 Eq (TickedLedgerState blk ValuesMK)) =>
Model blk r -> Model blk r
doSync Model blk r
model =
    if TickedLedgerState blk ValuesMK
st TickedLedgerState blk ValuesMK
-> TickedLedgerState blk ValuesMK -> Bool
forall a. Eq a => a -> a -> Bool
== TickedLedgerState blk ValuesMK
st'
    then Model blk r
model
    else
      let
          ([(GenTx blk, TicketNo)]
validTxs, TicketNo
_tk, TxMeasure blk
newSize, TickedLedgerState blk ValuesMK
st'') =
            LedgerConfig blk
-> TicketNo
-> TxMeasure blk
-> TxMeasure blk
-> TickedLedgerState blk ValuesMK
-> [(GenTx blk, Maybe TicketNo)]
-> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
    TickedLedgerState blk ValuesMK)
forall blk.
(LedgerSupportsMempool blk, BasicEnvelopeValidation blk) =>
LedgerConfig blk
-> TicketNo
-> TxMeasure blk
-> TxMeasure blk
-> TickedLedgerState blk ValuesMK
-> [(GenTx blk, Maybe TicketNo)]
-> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
    TickedLedgerState blk ValuesMK)
foldTxs LedgerConfig blk
modelConfig TicketNo
zeroTicketNo TxMeasure blk
modelCapacity TxMeasure blk
forall a. Measure a => a
Measure.zero TickedLedgerState blk ValuesMK
st' ([(GenTx blk, Maybe TicketNo)]
 -> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
     TickedLedgerState blk ValuesMK))
-> [(GenTx blk, Maybe TicketNo)]
-> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
    TickedLedgerState blk ValuesMK)
forall a b. (a -> b) -> a -> b
$ ((GenTx blk, TicketNo) -> (GenTx blk, Maybe TicketNo))
-> [(GenTx blk, TicketNo)] -> [(GenTx blk, Maybe TicketNo)]
forall a b. (a -> b) -> [a] -> [b]
map ((TicketNo -> Maybe TicketNo)
-> (GenTx blk, TicketNo) -> (GenTx blk, Maybe TicketNo)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: MapKind) b c d. Arrow a => a b c -> a (d, b) (d, c)
second TicketNo -> Maybe TicketNo
forall a. a -> Maybe a
Just) [(GenTx blk, TicketNo)]
modelTxs

      in
        Model blk r
model {
          modelMempoolIntermediateState = st''
        , modelTxs                      = validTxs
        , modelCurrentSize              = newSize
        }
  where

      st' :: TickedLedgerState blk ValuesMK
st' = LedgerConfig blk
-> LedgerState blk ValuesMK -> TickedLedgerState blk ValuesMK
forall blk.
(ValidateEnvelope blk, LedgerSupportsMempool blk) =>
LedgerConfig blk
-> LedgerState blk ValuesMK -> TickedLedgerState blk ValuesMK
tick LedgerConfig blk
modelConfig LedgerState blk ValuesMK
modelLedgerDBTip

      Model {
        modelMempoolIntermediateState :: forall {k} blk (r :: k).
Model blk r -> TickedLedgerState blk ValuesMK
modelMempoolIntermediateState = TickedLedgerState blk ValuesMK
st
      , LedgerState blk ValuesMK
modelLedgerDBTip :: forall {k} blk (r :: k). Model blk r -> LedgerState blk ValuesMK
modelLedgerDBTip :: LedgerState blk ValuesMK
modelLedgerDBTip
      , [(GenTx blk, TicketNo)]
modelTxs :: forall {k} blk (r :: k). Model blk r -> [(GenTx blk, TicketNo)]
modelTxs :: [(GenTx blk, TicketNo)]
modelTxs
      , TxMeasure blk
modelCapacity :: forall {k} blk (r :: k). Model blk r -> TxMeasure blk
modelCapacity :: TxMeasure blk
modelCapacity
      , LedgerConfig blk
modelConfig :: forall {k} blk (r :: k). Model blk r -> LedgerCfg (LedgerState blk)
modelConfig :: LedgerConfig blk
modelConfig
      } = Model blk r
model

doChangeLedger ::
  (StandardHash blk, GetTip (LedgerState blk))
  => Model blk r
  -> LedgerState blk ValuesMK
  -> ModifyDB
  -> Model blk r
doChangeLedger :: forall {k} blk (r :: k).
(StandardHash blk, GetTip (LedgerState blk)) =>
Model blk r -> LedgerState blk ValuesMK -> ModifyDB -> Model blk r
doChangeLedger Model blk r
model LedgerState blk ValuesMK
l' ModifyDB
b' =
   Model blk r
model { modelLedgerDBTip = l'
         , modelReachableStates =
            if keepsDB b'
            then l' `Set.delete` Set.insert modelLedgerDBTip modelReachableStates
            else Set.empty
         , modelOtherStates =
            if keepsDB b'
            then modelOtherStates
            else modelLedgerDBTip `Set.insert` (modelOtherStates `Set.union` modelReachableStates)
         }
 where
    Model {
        LedgerState blk ValuesMK
modelLedgerDBTip :: forall {k} blk (r :: k). Model blk r -> LedgerState blk ValuesMK
modelLedgerDBTip :: LedgerState blk ValuesMK
modelLedgerDBTip
      , Set (LedgerState blk ValuesMK)
modelReachableStates :: forall {k} blk (r :: k).
Model blk r -> Set (LedgerState blk ValuesMK)
modelReachableStates :: Set (LedgerState blk ValuesMK)
modelReachableStates
      , Set (LedgerState blk ValuesMK)
modelOtherStates :: forall {k} blk (r :: k).
Model blk r -> Set (LedgerState blk ValuesMK)
modelOtherStates :: Set (LedgerState blk ValuesMK)
modelOtherStates
      } = Model blk r
model

doTryAddTxs ::
  ( LedgerSupportsMempool blk
  , ValidateEnvelope blk
  , Eq (TickedLedgerState blk ValuesMK)
  , Eq (GenTx blk)
  )
  => Model blk r
  -> [GenTx blk]
  -> Model blk r
doTryAddTxs :: forall {k} blk (r :: k).
(LedgerSupportsMempool blk, ValidateEnvelope blk,
 Eq (TickedLedgerState blk ValuesMK), Eq (GenTx blk)) =>
Model blk r -> [GenTx blk] -> Model blk r
doTryAddTxs Model blk r
model [] = Model blk r
model
doTryAddTxs Model blk r
model [GenTx blk]
txs =
    case (LedgerState blk ValuesMK -> Bool)
-> Set (LedgerState blk ValuesMK)
-> Maybe (LedgerState blk ValuesMK)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
Foldable.find
           ((Point (Ticked (LedgerState blk)) -> Point (LedgerState blk)
forall {k1} {k2} (b :: k1) (b' :: k2).
Coercible (HeaderHash b) (HeaderHash b') =>
Point b -> Point b'
castPoint (TickedLedgerState blk ValuesMK -> Point (Ticked (LedgerState blk))
forall (mk :: MapKind).
Ticked (LedgerState blk) mk -> Point (Ticked (LedgerState blk))
forall (l :: LedgerStateKind) (mk :: MapKind).
GetTip l =>
l mk -> Point l
getTip TickedLedgerState blk ValuesMK
st) Point (LedgerState blk) -> Point (LedgerState blk) -> Bool
forall a. Eq a => a -> a -> Bool
==) (Point (LedgerState blk) -> Bool)
-> (LedgerState blk ValuesMK -> Point (LedgerState blk))
-> LedgerState blk ValuesMK
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerState blk ValuesMK -> Point (LedgerState blk)
forall (mk :: MapKind).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: MapKind).
GetTip l =>
l mk -> Point l
getTip)
           (LedgerState blk ValuesMK
-> Set (LedgerState blk ValuesMK) -> Set (LedgerState blk ValuesMK)
forall a. Ord a => a -> Set a -> Set a
Set.insert LedgerState blk ValuesMK
modelLedgerDBTip Set (LedgerState blk ValuesMK)
modelReachableStates) of
      Maybe (LedgerState blk ValuesMK)
Nothing -> Model blk r -> [GenTx blk] -> Model blk r
forall {k} blk (r :: k).
(LedgerSupportsMempool blk, ValidateEnvelope blk,
 Eq (TickedLedgerState blk ValuesMK), Eq (GenTx blk)) =>
Model blk r -> [GenTx blk] -> Model blk r
doTryAddTxs (Model blk r -> Model blk r
forall {k} blk (r :: k).
(ValidateEnvelope blk, LedgerSupportsMempool blk,
 Eq (TickedLedgerState blk ValuesMK)) =>
Model blk r -> Model blk r
doSync Model blk r
model) [GenTx blk]
txs
      Just LedgerState blk ValuesMK
_ ->
        let nextTicket :: TicketNo
nextTicket = TicketNo -> TicketNo
forall a. Enum a => a -> a
succ (TicketNo -> TicketNo) -> TicketNo -> TicketNo
forall a b. (a -> b) -> a -> b
$ Model blk r -> TicketNo
forall {k} blk (r :: k). Model blk r -> TicketNo
modelLastSeenTicketNo Model blk r
model
            ([(GenTx blk, TicketNo)]
validTxs, TicketNo
tk, TxMeasure blk
newSize, TickedLedgerState blk ValuesMK
st'') =
              LedgerConfig blk
-> TicketNo
-> TxMeasure blk
-> TxMeasure blk
-> TickedLedgerState blk ValuesMK
-> [(GenTx blk, Maybe TicketNo)]
-> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
    TickedLedgerState blk ValuesMK)
forall blk.
(LedgerSupportsMempool blk, BasicEnvelopeValidation blk) =>
LedgerConfig blk
-> TicketNo
-> TxMeasure blk
-> TxMeasure blk
-> TickedLedgerState blk ValuesMK
-> [(GenTx blk, Maybe TicketNo)]
-> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
    TickedLedgerState blk ValuesMK)
foldTxs LedgerConfig blk
cfg TicketNo
nextTicket TxMeasure blk
modelCapacity TxMeasure blk
modelCurrentSize TickedLedgerState blk ValuesMK
st ([(GenTx blk, Maybe TicketNo)]
 -> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
     TickedLedgerState blk ValuesMK))
-> [(GenTx blk, Maybe TicketNo)]
-> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
    TickedLedgerState blk ValuesMK)
forall a b. (a -> b) -> a -> b
$ (GenTx blk -> (GenTx blk, Maybe TicketNo))
-> [GenTx blk] -> [(GenTx blk, Maybe TicketNo)]
forall a b. (a -> b) -> [a] -> [b]
map (,Maybe TicketNo
forall a. Maybe a
Nothing) [GenTx blk]
txs
            modelTxs' :: [(GenTx blk, TicketNo)]
modelTxs'           = [(GenTx blk, TicketNo)]
modelTxs [(GenTx blk, TicketNo)]
-> [(GenTx blk, TicketNo)] -> [(GenTx blk, TicketNo)]
forall a. [a] -> [a] -> [a]
++ [(GenTx blk, TicketNo)]
validTxs
        in
          Model blk r
model {
            modelMempoolIntermediateState = st''
          , modelTxs                      = modelTxs'
          , modelLastSeenTicketNo         = pred tk
          , modelCurrentSize              = newSize
          }
  where
    Model {
        modelMempoolIntermediateState :: forall {k} blk (r :: k).
Model blk r -> TickedLedgerState blk ValuesMK
modelMempoolIntermediateState = TickedLedgerState blk ValuesMK
st
      , [(GenTx blk, TicketNo)]
modelTxs :: forall {k} blk (r :: k). Model blk r -> [(GenTx blk, TicketNo)]
modelTxs :: [(GenTx blk, TicketNo)]
modelTxs
      , TxMeasure blk
modelCurrentSize :: forall {k} blk (r :: k). Model blk r -> TxMeasure blk
modelCurrentSize :: TxMeasure blk
modelCurrentSize
      , Set (LedgerState blk ValuesMK)
modelReachableStates :: forall {k} blk (r :: k).
Model blk r -> Set (LedgerState blk ValuesMK)
modelReachableStates :: Set (LedgerState blk ValuesMK)
modelReachableStates
      , LedgerState blk ValuesMK
modelLedgerDBTip :: forall {k} blk (r :: k). Model blk r -> LedgerState blk ValuesMK
modelLedgerDBTip :: LedgerState blk ValuesMK
modelLedgerDBTip
      , modelConfig :: forall {k} blk (r :: k). Model blk r -> LedgerCfg (LedgerState blk)
modelConfig = LedgerConfig blk
cfg
      , TxMeasure blk
modelCapacity :: forall {k} blk (r :: k). Model blk r -> TxMeasure blk
modelCapacity :: TxMeasure blk
modelCapacity
      } = Model blk r
model

transition ::
     ( Eq (GenTx blk)
     , Eq (TickedLedgerState blk ValuesMK)
     , LedgerSupportsMempool blk
     , ToExpr (GenTx blk)
     , ValidateEnvelope blk
     , ToExpr (Command blk r)
     )
  => Model blk r
  -> Command blk r
  -> Response blk r
  -> Model blk r
transition :: forall {k} blk (r :: k).
(Eq (GenTx blk), Eq (TickedLedgerState blk ValuesMK),
 LedgerSupportsMempool blk, ToExpr (GenTx blk),
 ValidateEnvelope blk, ToExpr (Command blk r)) =>
Model blk r -> Command blk r -> Response blk r -> Model blk r
transition Model blk r
model Command blk r
cmd Response blk r
resp = case (Command blk r
cmd, Response blk r
resp) of
  (Action (TryAddTxs [GenTx blk]
txs), Response blk r
Void)      -> Model blk r -> [GenTx blk] -> Model blk r
forall {k} blk (r :: k).
(LedgerSupportsMempool blk, ValidateEnvelope blk,
 Eq (TickedLedgerState blk ValuesMK), Eq (GenTx blk)) =>
Model blk r -> [GenTx blk] -> Model blk r
doTryAddTxs Model blk r
model [GenTx blk]
txs
  (Event (ChangeLedger LedgerState blk ValuesMK
l ModifyDB
b), Response blk r
Void)    -> Model blk r -> LedgerState blk ValuesMK -> ModifyDB -> Model blk r
forall {k} blk (r :: k).
(StandardHash blk, GetTip (LedgerState blk)) =>
Model blk r -> LedgerState blk ValuesMK -> ModifyDB -> Model blk r
doChangeLedger Model blk r
model LedgerState blk ValuesMK
l ModifyDB
b
  (Action Action blk r
GetSnapshot, GotSnapshot{}) -> Model blk r
model
  (Action Action blk r
SyncLedger, Response blk r
Void)           -> Model blk r -> Model blk r
forall {k} blk (r :: k).
(ValidateEnvelope blk, LedgerSupportsMempool blk,
 Eq (TickedLedgerState blk ValuesMK)) =>
Model blk r -> Model blk r
doSync Model blk r
model
  (Command blk r, Response blk r)
_ -> String -> Model blk r
forall a. HasCallStack => String -> a
error (String -> Model blk r) -> String -> Model blk r
forall a b. (a -> b) -> a -> b
$ String
"mismatched command "
             String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Command blk r -> String
forall a. Show a => a -> String
show Command blk r
cmd
             String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" and response "
             String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Response blk r -> String
forall a. Show a => a -> String
show Response blk r
resp

{-------------------------------------------------------------------------------
  Ledger helper functions
-------------------------------------------------------------------------------}

-- | Apply a list of transactions short-circuiting if the mempool gets full.
-- Emulates almost exactly the behaviour of 'implTryTryAddTxs'.
foldTxs ::
  forall blk.
  ( LedgerSupportsMempool blk
  , BasicEnvelopeValidation blk
  )
  => LedgerConfig blk
  -> TicketNo
  -> TxMeasure blk
  -> TxMeasure blk
  -> TickedLedgerState blk ValuesMK
  -> [(GenTx blk, Maybe TicketNo)]
  -> ( [(GenTx blk, TicketNo)]
     , TicketNo
     , TxMeasure blk
     , TickedLedgerState blk ValuesMK
     )
foldTxs :: forall blk.
(LedgerSupportsMempool blk, BasicEnvelopeValidation blk) =>
LedgerConfig blk
-> TicketNo
-> TxMeasure blk
-> TxMeasure blk
-> TickedLedgerState blk ValuesMK
-> [(GenTx blk, Maybe TicketNo)]
-> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
    TickedLedgerState blk ValuesMK)
foldTxs LedgerConfig blk
cfg TicketNo
nextTk TxMeasure blk
capacity TxMeasure blk
initialFilled TickedLedgerState blk ValuesMK
initialState  =
    ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
 TickedLedgerState blk ValuesMK)
-> [(GenTx blk, Maybe TicketNo)]
-> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
    TickedLedgerState blk ValuesMK)
go ([], TicketNo
nextTk, TxMeasure blk
initialFilled, TickedLedgerState blk ValuesMK
initialState)
  where
    go :: ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
 TickedLedgerState blk ValuesMK)
-> [(GenTx blk, Maybe TicketNo)]
-> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
    TickedLedgerState blk ValuesMK)
go ([(GenTx blk, TicketNo)]
acc, TicketNo
tk, TxMeasure blk
curSize, TickedLedgerState blk ValuesMK
st) [] = ( [(GenTx blk, TicketNo)] -> [(GenTx blk, TicketNo)]
forall a. [a] -> [a]
reverse [(GenTx blk, TicketNo)]
acc
                                   , TicketNo
tk
                                   , TxMeasure blk
curSize
                                   , TickedLedgerState blk ValuesMK
st
                                   )
    go ([(GenTx blk, TicketNo)]
acc, TicketNo
tk, TxMeasure blk
curSize, TickedLedgerState blk ValuesMK
st) ((GenTx blk
tx, Maybe TicketNo
txtk):[(GenTx blk, Maybe TicketNo)]
next) =
      let slot :: SlotNo
slot = case TickedLedgerState blk ValuesMK -> WithOrigin SlotNo
forall (l :: LedgerStateKind) (mk :: MapKind).
GetTip l =>
l mk -> WithOrigin SlotNo
getTipSlot TickedLedgerState blk ValuesMK
st of
            WithOrigin SlotNo
Origin -> Proxy blk -> SlotNo
forall blk. BasicEnvelopeValidation blk => Proxy blk -> SlotNo
minimumPossibleSlotNo (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @blk)
            At SlotNo
v   -> SlotNo
v SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ SlotNo
1
      in
        case Except
  (ApplyTxErr blk)
  (TxMeasure blk,
   (TickedLedgerState blk DiffMK, Validated (GenTx blk)))
-> Either
     (ApplyTxErr blk)
     (TxMeasure blk,
      (TickedLedgerState blk DiffMK, Validated (GenTx blk)))
forall e a. Except e a -> Either e a
runExcept (Except
   (ApplyTxErr blk)
   (TxMeasure blk,
    (TickedLedgerState blk DiffMK, Validated (GenTx blk)))
 -> Either
      (ApplyTxErr blk)
      (TxMeasure blk,
       (TickedLedgerState blk DiffMK, Validated (GenTx blk))))
-> Except
     (ApplyTxErr blk)
     (TxMeasure blk,
      (TickedLedgerState blk DiffMK, Validated (GenTx blk)))
-> Either
     (ApplyTxErr blk)
     (TxMeasure blk,
      (TickedLedgerState blk DiffMK, Validated (GenTx blk)))
forall a b. (a -> b) -> a -> b
$ (,) (TxMeasure blk
 -> (TickedLedgerState blk DiffMK, Validated (GenTx blk))
 -> (TxMeasure blk,
     (TickedLedgerState blk DiffMK, Validated (GenTx blk))))
-> ExceptT (ApplyTxErr blk) Identity (TxMeasure blk)
-> ExceptT
     (ApplyTxErr blk)
     Identity
     ((TickedLedgerState blk DiffMK, Validated (GenTx blk))
      -> (TxMeasure blk,
          (TickedLedgerState blk DiffMK, Validated (GenTx blk))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LedgerConfig blk
-> TickedLedgerState blk ValuesMK
-> GenTx blk
-> ExceptT (ApplyTxErr blk) Identity (TxMeasure blk)
forall blk.
TxLimits blk =>
LedgerConfig blk
-> TickedLedgerState blk ValuesMK
-> GenTx blk
-> Except (ApplyTxErr blk) (TxMeasure blk)
txMeasure LedgerConfig blk
cfg TickedLedgerState blk ValuesMK
st GenTx blk
tx ExceptT
  (ApplyTxErr blk)
  Identity
  ((TickedLedgerState blk DiffMK, Validated (GenTx blk))
   -> (TxMeasure blk,
       (TickedLedgerState blk DiffMK, Validated (GenTx blk))))
-> ExceptT
     (ApplyTxErr blk)
     Identity
     (TickedLedgerState blk DiffMK, Validated (GenTx blk))
-> Except
     (ApplyTxErr blk)
     (TxMeasure blk,
      (TickedLedgerState blk DiffMK, Validated (GenTx blk)))
forall a b.
ExceptT (ApplyTxErr blk) Identity (a -> b)
-> ExceptT (ApplyTxErr blk) Identity a
-> ExceptT (ApplyTxErr blk) Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> LedgerConfig blk
-> WhetherToIntervene
-> SlotNo
-> GenTx blk
-> TickedLedgerState blk ValuesMK
-> ExceptT
     (ApplyTxErr blk)
     Identity
     (TickedLedgerState blk DiffMK, Validated (GenTx blk))
forall blk.
LedgerSupportsMempool blk =>
LedgerConfig blk
-> WhetherToIntervene
-> SlotNo
-> GenTx blk
-> TickedLedgerState blk ValuesMK
-> Except
     (ApplyTxErr blk)
     (TickedLedgerState blk DiffMK, Validated (GenTx blk))
applyTx LedgerConfig blk
cfg WhetherToIntervene
DoNotIntervene SlotNo
slot GenTx blk
tx TickedLedgerState blk ValuesMK
st  of
          Left{} ->
            ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
 TickedLedgerState blk ValuesMK)
-> [(GenTx blk, Maybe TicketNo)]
-> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
    TickedLedgerState blk ValuesMK)
go ( [(GenTx blk, TicketNo)]
acc
               , TicketNo
tk
               , TxMeasure blk
curSize
               , TickedLedgerState blk ValuesMK
st
               )
            [(GenTx blk, Maybe TicketNo)]
next
          Right (TxMeasure blk
txsz, (TickedLedgerState blk DiffMK
st', Validated (GenTx blk)
vtx))
            | (TxMeasure blk
curSize TxMeasure blk -> TxMeasure blk -> Bool
forall a. Measure a => a -> a -> Bool
Measure.<= TxMeasure blk
curSize TxMeasure blk -> TxMeasure blk -> TxMeasure blk
forall a. Measure a => a -> a -> a
`Measure.plus` TxMeasure blk
txsz
              -- Overflow
               Bool -> Bool -> Bool
&& TxMeasure blk
curSize TxMeasure blk -> TxMeasure blk -> TxMeasure blk
forall a. Measure a => a -> a -> a
`Measure.plus` TxMeasure blk
txsz TxMeasure blk -> TxMeasure blk -> Bool
forall a. Measure a => a -> a -> Bool
Measure.<= TxMeasure blk
capacity
              )

             -- fits
              ->
                ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
 TickedLedgerState blk ValuesMK)
-> [(GenTx blk, Maybe TicketNo)]
-> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
    TickedLedgerState blk ValuesMK)
go ( (Validated (GenTx blk) -> GenTx blk
forall blk.
LedgerSupportsMempool blk =>
Validated (GenTx blk) -> GenTx blk
txForgetValidated Validated (GenTx blk)
vtx, TicketNo -> Maybe TicketNo -> TicketNo
forall a. a -> Maybe a -> a
fromMaybe TicketNo
tk Maybe TicketNo
txtk)(GenTx blk, TicketNo)
-> [(GenTx blk, TicketNo)] -> [(GenTx blk, TicketNo)]
forall a. a -> [a] -> [a]
:[(GenTx blk, TicketNo)]
acc
                   , TicketNo -> TicketNo
forall a. Enum a => a -> a
succ TicketNo
tk
                   , TxMeasure blk
curSize TxMeasure blk -> TxMeasure blk -> TxMeasure blk
forall a. Measure a => a -> a -> a
`Measure.plus` TxMeasure blk
txsz
                   , TickedLedgerState blk ValuesMK
-> TickedLedgerState blk DiffMK -> TickedLedgerState blk ValuesMK
forall (l :: LedgerStateKind) (l' :: LedgerStateKind).
(SameUtxoTypes l l', HasLedgerTables l, HasLedgerTables l') =>
l ValuesMK -> l' DiffMK -> l' ValuesMK
applyDiffs TickedLedgerState blk ValuesMK
st TickedLedgerState blk DiffMK
st'
                   )
                  [(GenTx blk, Maybe TicketNo)]
next
            | Bool
otherwise ->
                ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
 TickedLedgerState blk ValuesMK)
-> [(GenTx blk, Maybe TicketNo)]
-> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
    TickedLedgerState blk ValuesMK)
go ( [(GenTx blk, TicketNo)]
acc
                   , TicketNo
tk
                   , TxMeasure blk
curSize
                   , TickedLedgerState blk ValuesMK
st
                   )
                [(GenTx blk, Maybe TicketNo)]
next

tick ::
  ( ValidateEnvelope blk
  , LedgerSupportsMempool blk
  )
  => LedgerConfig blk
  -> LedgerState blk ValuesMK
  -> TickedLedgerState blk ValuesMK
tick :: forall blk.
(ValidateEnvelope blk, LedgerSupportsMempool blk) =>
LedgerConfig blk
-> LedgerState blk ValuesMK -> TickedLedgerState blk ValuesMK
tick LedgerConfig blk
cfg LedgerState blk ValuesMK
st = LedgerState blk ValuesMK
-> Ticked (LedgerState blk) DiffMK
-> Ticked (LedgerState blk) ValuesMK
forall (l :: LedgerStateKind) (l' :: LedgerStateKind).
(SameUtxoTypes l l', HasLedgerTables l, HasLedgerTables l') =>
l ValuesMK -> l' DiffMK -> l' ValuesMK
applyDiffs LedgerState blk ValuesMK
st Ticked (LedgerState blk) DiffMK
ticked
  where
    ticked :: Ticked (LedgerState blk) DiffMK
ticked = (SlotNo, Ticked (LedgerState blk) DiffMK)
-> Ticked (LedgerState blk) DiffMK
forall a b. (a, b) -> b
snd
           ((SlotNo, Ticked (LedgerState blk) DiffMK)
 -> Ticked (LedgerState blk) DiffMK)
-> (LedgerState blk ValuesMK
    -> (SlotNo, Ticked (LedgerState blk) DiffMK))
-> LedgerState blk ValuesMK
-> Ticked (LedgerState blk) DiffMK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerConfig blk
-> ForgeLedgerState blk
-> (SlotNo, Ticked (LedgerState blk) DiffMK)
forall blk.
(UpdateLedger blk, ValidateEnvelope blk) =>
LedgerConfig blk
-> ForgeLedgerState blk -> (SlotNo, TickedLedgerState blk DiffMK)
tickLedgerState LedgerConfig blk
cfg
           (ForgeLedgerState blk -> (SlotNo, Ticked (LedgerState blk) DiffMK))
-> (LedgerState blk ValuesMK -> ForgeLedgerState blk)
-> LedgerState blk ValuesMK
-> (SlotNo, Ticked (LedgerState blk) DiffMK)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerState blk EmptyMK -> ForgeLedgerState blk
forall blk. LedgerState blk EmptyMK -> ForgeLedgerState blk
ForgeInUnknownSlot
           (LedgerState blk EmptyMK -> ForgeLedgerState blk)
-> (LedgerState blk ValuesMK -> LedgerState blk EmptyMK)
-> LedgerState blk ValuesMK
-> ForgeLedgerState blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerState blk ValuesMK -> LedgerState blk EmptyMK
forall (l :: LedgerStateKind) (mk :: MapKind).
HasLedgerTables l =>
l mk -> l EmptyMK
forgetLedgerTables
           (LedgerState blk ValuesMK -> Ticked (LedgerState blk) DiffMK)
-> LedgerState blk ValuesMK -> Ticked (LedgerState blk) DiffMK
forall a b. (a -> b) -> a -> b
$ LedgerState blk ValuesMK
st

{-------------------------------------------------------------------------------
  SUT side
-------------------------------------------------------------------------------}

-- | The System Under Test
data SUT m blk =
  SUT
  !(Mempool m blk)
    -- ^ A Mempool
  !(StrictTVar m (MockedLedgerDB blk))
    -- ^ Emulates a ledger db to the extent needed by the ledger interface.
  deriving (forall x. SUT m blk -> Rep (SUT m blk) x)
-> (forall x. Rep (SUT m blk) x -> SUT m blk)
-> Generic (SUT m blk)
forall x. Rep (SUT m blk) x -> SUT m blk
forall x. SUT m blk -> Rep (SUT m blk) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (m :: * -> *) blk x. Rep (SUT m blk) x -> SUT m blk
forall (m :: * -> *) blk x. SUT m blk -> Rep (SUT m blk) x
$cfrom :: forall (m :: * -> *) blk x. SUT m blk -> Rep (SUT m blk) x
from :: forall x. SUT m blk -> Rep (SUT m blk) x
$cto :: forall (m :: * -> *) blk x. Rep (SUT m blk) x -> SUT m blk
to :: forall x. Rep (SUT m blk) x -> SUT m blk
Generic

deriving instance ( NoThunks (Mempool m blk)
                  , NoThunks (StrictTVar m (MockedLedgerDB blk))
                  ) =>  NoThunks (SUT m blk)

-- | A very minimal mock of the ledger db.
--
-- The ledger interface will serve the values from this datatype.
data MockedLedgerDB blk = MockedLedgerDB {
    -- | The current LedgerDB tip
    forall blk. MockedLedgerDB blk -> LedgerState blk ValuesMK
ldbTip        :: !(LedgerState blk ValuesMK)
    -- | States which are still reachable in the LedgerDB
  , forall blk. MockedLedgerDB blk -> Set (LedgerState blk ValuesMK)
reachableTips :: !(Set (LedgerState blk ValuesMK))
    -- | States which are no longer reachable in the LedgerDB
  , forall blk. MockedLedgerDB blk -> Set (LedgerState blk ValuesMK)
otherStates   :: !(Set (LedgerState blk ValuesMK))
  } deriving ((forall x. MockedLedgerDB blk -> Rep (MockedLedgerDB blk) x)
-> (forall x. Rep (MockedLedgerDB blk) x -> MockedLedgerDB blk)
-> Generic (MockedLedgerDB blk)
forall x. Rep (MockedLedgerDB blk) x -> MockedLedgerDB blk
forall x. MockedLedgerDB blk -> Rep (MockedLedgerDB blk) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall blk x. Rep (MockedLedgerDB blk) x -> MockedLedgerDB blk
forall blk x. MockedLedgerDB blk -> Rep (MockedLedgerDB blk) x
$cfrom :: forall blk x. MockedLedgerDB blk -> Rep (MockedLedgerDB blk) x
from :: forall x. MockedLedgerDB blk -> Rep (MockedLedgerDB blk) x
$cto :: forall blk x. Rep (MockedLedgerDB blk) x -> MockedLedgerDB blk
to :: forall x. Rep (MockedLedgerDB blk) x -> MockedLedgerDB blk
Generic)

-- | Create a ledger interface and provide the tvar to modify it when switching
-- ledgers.
newLedgerInterface ::
  ( MonadSTM m
  , NoThunks (MockedLedgerDB blk)
  , LedgerSupportsMempool blk
  )
  => LedgerState blk ValuesMK
  -> m (LedgerInterface m blk, StrictTVar m (MockedLedgerDB blk))
newLedgerInterface :: forall (m :: * -> *) blk.
(MonadSTM m, NoThunks (MockedLedgerDB blk),
 LedgerSupportsMempool blk) =>
LedgerState blk ValuesMK
-> m (LedgerInterface m blk, StrictTVar m (MockedLedgerDB blk))
newLedgerInterface LedgerState blk ValuesMK
initialLedger = do
  t <- MockedLedgerDB blk -> m (StrictTVar m (MockedLedgerDB blk))
forall (m :: * -> *) a.
(HasCallStack, MonadSTM m, NoThunks a) =>
a -> m (StrictTVar m a)
newTVarIO (MockedLedgerDB blk -> m (StrictTVar m (MockedLedgerDB blk)))
-> MockedLedgerDB blk -> m (StrictTVar m (MockedLedgerDB blk))
forall a b. (a -> b) -> a -> b
$ LedgerState blk ValuesMK
-> Set (LedgerState blk ValuesMK)
-> Set (LedgerState blk ValuesMK)
-> MockedLedgerDB blk
forall blk.
LedgerState blk ValuesMK
-> Set (LedgerState blk ValuesMK)
-> Set (LedgerState blk ValuesMK)
-> MockedLedgerDB blk
MockedLedgerDB LedgerState blk ValuesMK
initialLedger Set (LedgerState blk ValuesMK)
forall a. Set a
Set.empty Set (LedgerState blk ValuesMK)
forall a. Set a
Set.empty
  pure (LedgerInterface {
      getCurrentLedgerState = forgetLedgerTables . ldbTip <$> readTVar t
    , getLedgerTablesAtFor  = \Point blk
pt LedgerTables (LedgerState blk) KeysMK
keys -> do
        MockedLedgerDB ti oldReachableTips _ <- STM m (MockedLedgerDB blk) -> m (MockedLedgerDB blk)
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m (MockedLedgerDB blk) -> m (MockedLedgerDB blk))
-> STM m (MockedLedgerDB blk) -> m (MockedLedgerDB blk)
forall a b. (a -> b) -> a -> b
$ StrictTVar m (MockedLedgerDB blk) -> STM m (MockedLedgerDB blk)
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m (MockedLedgerDB blk)
t
        if pt == castPoint (getTip ti) -- if asking for tables at the tip of the
                                       -- ledger db
        then
          let tbs = (forall k v.
 LedgerTableConstraints' (LedgerState blk) k v =>
 KeysMK k v -> ValuesMK k v -> ValuesMK k v)
-> LedgerTables (LedgerState blk) KeysMK
-> LedgerTables (LedgerState blk) ValuesMK
-> LedgerTables (LedgerState blk) ValuesMK
forall (l :: LedgerStateKind) (mk1 :: MapKind) (mk2 :: MapKind)
       (mk3 :: MapKind).
LedgerTableConstraints l =>
(forall k v.
 LedgerTableConstraints' l k v =>
 mk1 k v -> mk2 k v -> mk3 k v)
-> LedgerTables l mk1 -> LedgerTables l mk2 -> LedgerTables l mk3
ltliftA2 KeysMK k v -> ValuesMK k v -> ValuesMK k v
forall k v. Ord k => KeysMK k v -> ValuesMK k v -> ValuesMK k v
forall k v.
LedgerTableConstraints' (LedgerState blk) k v =>
KeysMK k v -> ValuesMK k v -> ValuesMK k v
f LedgerTables (LedgerState blk) KeysMK
keys (LedgerTables (LedgerState blk) ValuesMK
 -> LedgerTables (LedgerState blk) ValuesMK)
-> LedgerTables (LedgerState blk) ValuesMK
-> LedgerTables (LedgerState blk) ValuesMK
forall a b. (a -> b) -> a -> b
$ LedgerState blk ValuesMK -> LedgerTables (LedgerState blk) ValuesMK
forall (mk :: MapKind).
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
LedgerState blk mk -> LedgerTables (LedgerState blk) mk
forall (l :: LedgerStateKind) (mk :: MapKind).
(HasLedgerTables l, CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
l mk -> LedgerTables l mk
projectLedgerTables LedgerState blk ValuesMK
ti
          in  pure $ Just tbs
        else case Foldable.find ((castPoint pt ==). getTip) oldReachableTips of
           Maybe (LedgerState blk ValuesMK)
Nothing -> Maybe (LedgerTables (LedgerState blk) ValuesMK)
-> m (Maybe (LedgerTables (LedgerState blk) ValuesMK))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (LedgerTables (LedgerState blk) ValuesMK)
forall a. Maybe a
Nothing
           Just LedgerState blk ValuesMK
mtip ->
             if Point blk
pt Point blk -> Point blk -> Bool
forall a. Eq a => a -> a -> Bool
== Point (LedgerState blk) -> Point blk
forall {k1} {k2} (b :: k1) (b' :: k2).
Coercible (HeaderHash b) (HeaderHash b') =>
Point b -> Point b'
castPoint (LedgerState blk ValuesMK -> Point (LedgerState blk)
forall (mk :: MapKind).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: MapKind).
GetTip l =>
l mk -> Point l
getTip LedgerState blk ValuesMK
mtip)
             -- if asking for tables at some still reachable state
             then
               let tbs :: LedgerTables (LedgerState blk) ValuesMK
tbs = (forall k v.
 LedgerTableConstraints' (LedgerState blk) k v =>
 KeysMK k v -> ValuesMK k v -> ValuesMK k v)
-> LedgerTables (LedgerState blk) KeysMK
-> LedgerTables (LedgerState blk) ValuesMK
-> LedgerTables (LedgerState blk) ValuesMK
forall (l :: LedgerStateKind) (mk1 :: MapKind) (mk2 :: MapKind)
       (mk3 :: MapKind).
LedgerTableConstraints l =>
(forall k v.
 LedgerTableConstraints' l k v =>
 mk1 k v -> mk2 k v -> mk3 k v)
-> LedgerTables l mk1 -> LedgerTables l mk2 -> LedgerTables l mk3
ltliftA2 KeysMK k v -> ValuesMK k v -> ValuesMK k v
forall k v. Ord k => KeysMK k v -> ValuesMK k v -> ValuesMK k v
forall k v.
LedgerTableConstraints' (LedgerState blk) k v =>
KeysMK k v -> ValuesMK k v -> ValuesMK k v
f LedgerTables (LedgerState blk) KeysMK
keys (LedgerTables (LedgerState blk) ValuesMK
 -> LedgerTables (LedgerState blk) ValuesMK)
-> LedgerTables (LedgerState blk) ValuesMK
-> LedgerTables (LedgerState blk) ValuesMK
forall a b. (a -> b) -> a -> b
$ LedgerState blk ValuesMK -> LedgerTables (LedgerState blk) ValuesMK
forall (mk :: MapKind).
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
LedgerState blk mk -> LedgerTables (LedgerState blk) mk
forall (l :: LedgerStateKind) (mk :: MapKind).
(HasLedgerTables l, CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
l mk -> LedgerTables l mk
projectLedgerTables LedgerState blk ValuesMK
mtip
               in  Maybe (LedgerTables (LedgerState blk) ValuesMK)
-> m (Maybe (LedgerTables (LedgerState blk) ValuesMK))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (LedgerTables (LedgerState blk) ValuesMK)
 -> m (Maybe (LedgerTables (LedgerState blk) ValuesMK)))
-> Maybe (LedgerTables (LedgerState blk) ValuesMK)
-> m (Maybe (LedgerTables (LedgerState blk) ValuesMK))
forall a b. (a -> b) -> a -> b
$ LedgerTables (LedgerState blk) ValuesMK
-> Maybe (LedgerTables (LedgerState blk) ValuesMK)
forall a. a -> Maybe a
Just LedgerTables (LedgerState blk) ValuesMK
tbs
             else
               -- if asking for tables at other point or at the mempool tip but
               -- it is not reachable
               Maybe (LedgerTables (LedgerState blk) ValuesMK)
-> m (Maybe (LedgerTables (LedgerState blk) ValuesMK))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (LedgerTables (LedgerState blk) ValuesMK)
forall a. Maybe a
Nothing
    }, t)
 where
   f :: Ord k => KeysMK k v -> ValuesMK k v -> ValuesMK k v
   f :: forall k v. Ord k => KeysMK k v -> ValuesMK k v -> ValuesMK k v
f (KeysMK Set k
s) (ValuesMK Map k v
v) =
      Map k v -> ValuesMK k v
forall k v. Map k v -> ValuesMK k v
ValuesMK (Map k v -> Set k -> Map k v
forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map k v
v Set k
s)

-- | Make a SUT
mkSUT ::
  forall m blk. ( NoThunks (MockedLedgerDB blk)
  , IOLike m
  , LedgerSupportsProtocol blk
  , LedgerSupportsMempool blk
  , HasTxId (GenTx blk)
  )
  => LedgerConfig blk
  -> LedgerState blk ValuesMK
  -> m (SUT m blk, CT.Tracer m String)
mkSUT :: forall (m :: * -> *) blk.
(NoThunks (MockedLedgerDB blk), IOLike m,
 LedgerSupportsProtocol blk, LedgerSupportsMempool blk,
 HasTxId (GenTx blk)) =>
LedgerConfig blk
-> LedgerState blk ValuesMK -> m (SUT m blk, Tracer m String)
mkSUT LedgerConfig blk
cfg LedgerState blk ValuesMK
initialLedger = do
  (lif, t) <- LedgerState blk ValuesMK
-> m (LedgerInterface m blk, StrictTVar m (MockedLedgerDB blk))
forall (m :: * -> *) blk.
(MonadSTM m, NoThunks (MockedLedgerDB blk),
 LedgerSupportsMempool blk) =>
LedgerState blk ValuesMK
-> m (LedgerInterface m blk, StrictTVar m (MockedLedgerDB blk))
newLedgerInterface LedgerState blk ValuesMK
initialLedger
  trcrChan <- atomically newTChan :: m (StrictTChan m (Either String (TraceEventMempool blk)))
  let trcr = (Either String (TraceEventMempool blk) -> m ())
-> Tracer m (Either String (TraceEventMempool blk))
forall (m :: * -> *) a. (a -> m ()) -> Tracer m a
CT.Tracer ((Either String (TraceEventMempool blk) -> m ())
 -> Tracer m (Either String (TraceEventMempool blk)))
-> (Either String (TraceEventMempool blk) -> m ())
-> Tracer m (Either String (TraceEventMempool blk))
forall a b. (a -> b) -> a -> b
$ -- Dbg.traceShowM @(Either String (TraceEventMempool blk))
                         STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m () -> m ())
-> (Either String (TraceEventMempool blk) -> STM m ())
-> Either String (TraceEventMempool blk)
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictTChan m (Either String (TraceEventMempool blk))
-> Either String (TraceEventMempool blk) -> STM m ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTChan m a -> a -> STM m ()
writeTChan StrictTChan m (Either String (TraceEventMempool blk))
trcrChan
  mempool <- openMempoolWithoutSyncThread
               lif
               cfg
               (MempoolCapacityBytesOverride $ unIgnoringOverflow txMaxBytes')
               (CT.Tracer $ CT.traceWith trcr . Right)
  pure (SUT mempool t, CT.Tracer $ atomically . writeTChan trcrChan . Left)

semantics ::
     ( MonadSTM m
     , LedgerSupportsMempool blk
     , ValidateEnvelope blk
     ) =>
     CT.Tracer m String
  -> Command blk Concrete
  -> StrictTVar m (SUT m blk)
  -> m (Response blk Concrete)
semantics :: forall (m :: * -> *) blk.
(MonadSTM m, LedgerSupportsMempool blk, ValidateEnvelope blk) =>
Tracer m String
-> Command blk Concrete
-> StrictTVar m (SUT m blk)
-> m (Response blk Concrete)
semantics Tracer m String
trcr Command blk Concrete
cmd StrictTVar m (SUT m blk)
r = do
  SUT m t <- STM m (SUT m blk) -> m (SUT m blk)
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m (SUT m blk) -> m (SUT m blk))
-> STM m (SUT m blk) -> m (SUT m blk)
forall a b. (a -> b) -> a -> b
$ StrictTVar m (SUT m blk) -> STM m (SUT m blk)
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m (SUT m blk)
r
  case cmd of
    Action (TryAddTxs [GenTx blk]
txs) -> do

      (GenTx blk -> m (MempoolAddTxResult blk)) -> [GenTx blk] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Mempool m blk
-> AddTxOnBehalfOf -> GenTx blk -> m (MempoolAddTxResult blk)
forall (m :: * -> *) blk.
Mempool m blk
-> AddTxOnBehalfOf -> GenTx blk -> m (MempoolAddTxResult blk)
addTx Mempool m blk
m AddTxOnBehalfOf
AddTxForRemotePeer) [GenTx blk]
txs
      Response blk Concrete -> m (Response blk Concrete)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Response blk Concrete
forall {k} blk (r :: k). Response blk r
Void

    Action Action blk Concrete
SyncLedger   -> do
      m (MempoolSnapshot blk) -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m (MempoolSnapshot blk) -> m ())
-> m (MempoolSnapshot blk) -> m ()
forall a b. (a -> b) -> a -> b
$ Mempool m blk -> m (MempoolSnapshot blk)
forall (m :: * -> *) blk. Mempool m blk -> m (MempoolSnapshot blk)
syncWithLedger Mempool m blk
m
      Response blk Concrete -> m (Response blk Concrete)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Response blk Concrete
forall {k} blk (r :: k). Response blk r
Void

    Action Action blk Concrete
GetSnapshot -> do
      txs <- MempoolSnapshot blk
-> [(Validated (GenTx blk), TicketNo, TxMeasure blk)]
forall blk.
MempoolSnapshot blk
-> [(Validated (GenTx blk), TicketNo, TxMeasure blk)]
snapshotTxs (MempoolSnapshot blk
 -> [(Validated (GenTx blk), TicketNo, TxMeasure blk)])
-> m (MempoolSnapshot blk)
-> m [(Validated (GenTx blk), TicketNo, TxMeasure blk)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STM m (MempoolSnapshot blk) -> m (MempoolSnapshot blk)
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (Mempool m blk -> STM m (MempoolSnapshot blk)
forall (m :: * -> *) blk.
Mempool m blk -> STM m (MempoolSnapshot blk)
getSnapshot Mempool m blk
m)
      pure $ GotSnapshot [ (txForgetValidated vtx, tk) | (vtx, tk, _) <- txs ]

    Event (ChangeLedger LedgerState blk ValuesMK
l' ModifyDB
newReachable) -> do
      Tracer m String -> String -> m ()
forall (m :: * -> *) a. Tracer m a -> a -> m ()
CT.traceWith Tracer m String
trcr (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"ChangingLedger to " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Point (LedgerState blk) -> String
forall a. Show a => a -> String
show (LedgerState blk ValuesMK -> Point (LedgerState blk)
forall (mk :: MapKind).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: MapKind).
GetTip l =>
l mk -> Point l
getTip LedgerState blk ValuesMK
l')
      STM m (Response blk Concrete) -> m (Response blk Concrete)
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m (Response blk Concrete) -> m (Response blk Concrete))
-> STM m (Response blk Concrete) -> m (Response blk Concrete)
forall a b. (a -> b) -> a -> b
$ do
       MockedLedgerDB ledgerTip oldReachableTips oldUnreachableTips <- StrictTVar m (MockedLedgerDB blk) -> STM m (MockedLedgerDB blk)
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m (MockedLedgerDB blk)
t
       if getTip l' == getTip ledgerTip
       then if keepsDB newReachable
            then pure ()
            else
              let (newReachableTips, newUnreachableTips) = (Set.empty,
                      Set.insert ledgerTip
                    $ Set.union oldUnreachableTips oldReachableTips
                   )
              in writeTVar t (MockedLedgerDB l' newReachableTips newUnreachableTips)
       else
         let
           (newReachableTips, newUnreachableTips) =
             if keepsDB newReachable
              then (Set.insert ledgerTip oldReachableTips, oldUnreachableTips)
              else (Set.empty,
                      Set.insert ledgerTip
                    $ Set.union oldUnreachableTips oldReachableTips
                   )
         in
           writeTVar t (MockedLedgerDB l' newReachableTips newUnreachableTips)
       pure Void

{-------------------------------------------------------------------------------
  Conditions
-------------------------------------------------------------------------------}

precondition :: Model blk Symbolic -> Command blk Symbolic -> Logic
-- precondition cfg Model {modelCurrentSize} (Action (TryAddTxs txs)) =
--   Boolean $ not (null txs) && modelCurrentSize > 0 && sum (map tSize rights $ init txs) < modelCurrentSize
precondition :: forall blk. Model blk Symbolic -> Command blk Symbolic -> Logic
precondition Model blk Symbolic
_ Command blk Symbolic
_ = Logic
Top

postcondition ::
  ( LedgerSupportsMempool blk
  , Eq (GenTx blk)
--  , Show (TickedLedgerState blk ValuesMK)
  )
  => Model    blk Concrete
  -> Command  blk Concrete
  -> Response blk Concrete
  -> Logic
postcondition :: forall blk.
(LedgerSupportsMempool blk, Eq (GenTx blk)) =>
Model blk Concrete
-> Command blk Concrete -> Response blk Concrete -> Logic
postcondition Model blk Concrete
model (Action Action blk Concrete
GetSnapshot) (GotSnapshot [(GenTx blk, TicketNo)]
txs) =
  -- Annotate (show $ modelMempoolIntermediateState model) $
  Model blk Concrete -> [(GenTx blk, TicketNo)]
forall {k} blk (r :: k). Model blk r -> [(GenTx blk, TicketNo)]
modelTxs Model blk Concrete
model [(GenTx blk, TicketNo)] -> [(GenTx blk, TicketNo)] -> Logic
forall a. (Eq a, Show a) => a -> a -> Logic
.== [(GenTx blk, TicketNo)]
txs
postcondition Model blk Concrete
_ Command blk Concrete
_ Response blk Concrete
_ = Logic
Top

noPostcondition ::
     Model    blk Concrete
  -> Command  blk Concrete
  -> Response blk Concrete
  -> Logic
noPostcondition :: forall blk.
Model blk Concrete
-> Command blk Concrete -> Response blk Concrete -> Logic
noPostcondition Model blk Concrete
_ Command blk Concrete
_ Response blk Concrete
_ = Logic
Top

shrinker :: Model blk Symbolic
         -> Command blk Symbolic
         -> [Command blk Symbolic]
shrinker :: forall blk.
Model blk Symbolic
-> Command blk Symbolic -> [Command blk Symbolic]
shrinker Model blk Symbolic
_ (Action (TryAddTxs [GenTx blk]
txs)) =
  Action blk Symbolic -> Command blk Symbolic
forall {k} blk (r :: k). Action blk r -> Command blk r
Action (Action blk Symbolic -> Command blk Symbolic)
-> ([GenTx blk] -> Action blk Symbolic)
-> [GenTx blk]
-> Command blk Symbolic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenTx blk] -> Action blk Symbolic
forall {k} blk (r :: k). [GenTx blk] -> Action blk r
TryAddTxs ([GenTx blk] -> Command blk Symbolic)
-> [[GenTx blk]] -> [Command blk Symbolic]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GenTx blk -> [GenTx blk]) -> [GenTx blk] -> [[GenTx blk]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList GenTx blk -> [GenTx blk]
forall a. a -> [a]
shrinkNothing [GenTx blk]
txs
shrinker Model blk Symbolic
_ Command blk Symbolic
_ = []

{-------------------------------------------------------------------------------
  State Machine
-------------------------------------------------------------------------------}

sm ::
  ( LedgerSupportsMempool blk
  , IOLike m
  , ValidateEnvelope blk
  )
  => StateMachine (Model blk) (Command blk) m (Response blk)
  -> CT.Tracer m String
  -> StrictTVar m (SUT m blk)
  -> StateMachine (Model blk) (Command blk) m (Response blk)
sm :: forall blk (m :: * -> *).
(LedgerSupportsMempool blk, IOLike m, ValidateEnvelope blk) =>
StateMachine (Model blk) (Command blk) m (Response blk)
-> Tracer m String
-> StrictTVar m (SUT m blk)
-> StateMachine (Model blk) (Command blk) m (Response blk)
sm StateMachine (Model blk) (Command blk) m (Response blk)
sm0 Tracer m String
trcr StrictTVar m (SUT m blk)
ior = StateMachine (Model blk) (Command blk) m (Response blk)
sm0 {
    QC.semantics = \Command blk Concrete
c -> Tracer m String
-> Command blk Concrete
-> StrictTVar m (SUT m blk)
-> m (Response blk Concrete)
forall (m :: * -> *) blk.
(MonadSTM m, LedgerSupportsMempool blk, ValidateEnvelope blk) =>
Tracer m String
-> Command blk Concrete
-> StrictTVar m (SUT m blk)
-> m (Response blk Concrete)
semantics Tracer m String
trcr Command blk Concrete
c StrictTVar m (SUT m blk)
ior
    }

smUnused ::
  ( blk ~ TestBlock
  , LedgerSupportsMempool blk
  , LedgerSupportsProtocol blk
  , Monad m
  )
  => LedgerConfig blk
  -> LedgerState blk ValuesMK
  -> TxMeasure blk
  -> MakeAtomic
  -> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
  -> StateMachine (Model blk) (Command blk) m (Response blk)
smUnused :: forall blk (m :: * -> *).
(blk ~ TestBlock, LedgerSupportsMempool blk,
 LedgerSupportsProtocol blk, Monad m) =>
LedgerConfig blk
-> LedgerState blk ValuesMK
-> TxMeasure blk
-> MakeAtomic
-> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
-> StateMachine (Model blk) (Command blk) m (Response blk)
smUnused LedgerConfig blk
cfg LedgerState blk ValuesMK
initialState TxMeasure blk
capacity MakeAtomic
ma Int -> LedgerState blk ValuesMK -> Gen [GenTx blk]
gTxs =
  StateMachine {
      initModel :: forall (r :: * -> *). Model blk r
QC.initModel     = LedgerConfig blk
-> TxMeasure blk -> LedgerState blk ValuesMK -> Model blk r
forall {k} blk (r :: k).
(LedgerSupportsMempool blk, ValidateEnvelope blk) =>
LedgerConfig blk
-> TxMeasure blk -> LedgerState blk ValuesMK -> Model blk r
initModel LedgerConfig blk
cfg TxMeasure blk
capacity LedgerState blk ValuesMK
initialState
    , transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
Model blk r -> Command blk r -> Response blk r -> Model blk r
QC.transition    = Model blk r -> Command blk r -> Response blk r -> Model blk r
forall {k} blk (r :: k).
(Eq (GenTx blk), Eq (TickedLedgerState blk ValuesMK),
 LedgerSupportsMempool blk, ToExpr (GenTx blk),
 ValidateEnvelope blk, ToExpr (Command blk r)) =>
Model blk r -> Command blk r -> Response blk r -> Model blk r
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
Model blk r -> Command blk r -> Response blk r -> Model blk r
transition
    , precondition :: Model blk Symbolic -> Command blk Symbolic -> Logic
QC.precondition  = Model blk Symbolic -> Command blk Symbolic -> Logic
forall blk. Model blk Symbolic -> Command blk Symbolic -> Logic
precondition
    , postcondition :: Model blk Concrete
-> Command blk Concrete -> Response blk Concrete -> Logic
QC.postcondition =
        case MakeAtomic
ma of
          MakeAtomic
NonAtomic -> Model blk Concrete
-> Command blk Concrete -> Response blk Concrete -> Logic
forall blk.
Model blk Concrete
-> Command blk Concrete -> Response blk Concrete -> Logic
noPostcondition
          MakeAtomic
Atomic    -> Model blk Concrete
-> Command blk Concrete -> Response blk Concrete -> Logic
forall blk.
(LedgerSupportsMempool blk, Eq (GenTx blk)) =>
Model blk Concrete
-> Command blk Concrete -> Response blk Concrete -> Logic
postcondition
          MakeAtomic
DontCare  -> Model blk Concrete
-> Command blk Concrete -> Response blk Concrete -> Logic
forall blk.
(LedgerSupportsMempool blk, Eq (GenTx blk)) =>
Model blk Concrete
-> Command blk Concrete -> Response blk Concrete -> Logic
postcondition
    , invariant :: Maybe (Model blk Concrete -> Logic)
QC.invariant     = Maybe (Model blk Concrete -> Logic)
forall a. Maybe a
Nothing
    , generator :: Model blk Symbolic -> Maybe (Gen (Command blk Symbolic))
QC.generator     = MakeAtomic
-> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
-> Model blk Symbolic
-> Maybe (Gen (Command blk Symbolic))
forall blk.
(Arbitrary (LedgerState blk ValuesMK), UnTick blk,
 StandardHash blk, GetTip (LedgerState blk)) =>
MakeAtomic
-> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
-> Model blk Symbolic
-> Maybe (Gen (Command blk Symbolic))
generator MakeAtomic
ma Int -> LedgerState blk ValuesMK -> Gen [GenTx blk]
gTxs
    , shrinker :: Model blk Symbolic
-> Command blk Symbolic -> [Command blk Symbolic]
QC.shrinker      = Model blk Symbolic
-> Command blk Symbolic -> [Command blk Symbolic]
forall blk.
Model blk Symbolic
-> Command blk Symbolic -> [Command blk Symbolic]
shrinker
    , semantics :: Command blk Concrete -> m (Response blk Concrete)
QC.semantics     = Command blk Concrete -> m (Response blk Concrete)
forall a. HasCallStack => a
undefined
    , mock :: Model blk Symbolic
-> Command blk Symbolic -> GenSym (Response blk Symbolic)
QC.mock          = Model blk Symbolic
-> Command blk Symbolic -> GenSym (Response blk Symbolic)
forall blk.
Model blk Symbolic
-> Command blk Symbolic -> GenSym (Response blk Symbolic)
mock
    , cleanup :: Model blk Concrete -> m ()
QC.cleanup       = Model blk Concrete -> m ()
forall (m :: * -> *) (model :: (* -> *) -> *).
Monad m =>
model Concrete -> m ()
noCleanup
    }

{-------------------------------------------------------------------------------
  Properties
-------------------------------------------------------------------------------}

prop_mempoolSequential ::
  forall blk .
  ( HasTxId (GenTx blk)
  , blk ~ TestBlock
  , LedgerSupportsMempool blk
  , LedgerSupportsProtocol blk
  )
  => LedgerConfig blk
  -> TxMeasure blk
  -> LedgerState blk ValuesMK
     -- ^ Initial state
  -> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
     -- ^ Transaction generator
  -> Property
prop_mempoolSequential :: forall blk.
(HasTxId (GenTx blk), blk ~ TestBlock, LedgerSupportsMempool blk,
 LedgerSupportsProtocol blk) =>
LedgerConfig blk
-> TxMeasure blk
-> LedgerState blk ValuesMK
-> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
-> Property
prop_mempoolSequential LedgerConfig blk
cfg TxMeasure blk
capacity LedgerState blk ValuesMK
initialState Int -> LedgerState blk ValuesMK -> Gen [GenTx blk]
gTxs = StateMachine (Model blk) (Command blk) IO (Response blk)
-> Maybe Int
-> (Commands (Command blk) (Response blk) -> Property)
-> Property
forall prop (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       (model :: (* -> *) -> *) (m :: * -> *).
(Testable prop, Show (cmd Symbolic), Show (resp Symbolic),
 Show (model Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Maybe Int -> (Commands cmd resp -> prop) -> Property
forAllCommands StateMachine (Model blk) (Command blk) IO (Response blk)
sm0 Maybe Int
forall a. Maybe a
Nothing ((Commands (Command blk) (Response blk) -> Property) -> Property)
-> (Commands (Command blk) (Response blk) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$
  \Commands (Command blk) (Response blk)
cmds -> PropertyM IO () -> Property
forall a. Testable a => PropertyM IO a -> Property
monadicIO
    (do
        (sut, trcr) <- IO (SUT IO blk, Tracer IO String)
-> PropertyM IO (SUT IO blk, Tracer IO String)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (IO (SUT IO blk, Tracer IO String)
 -> PropertyM IO (SUT IO blk, Tracer IO String))
-> IO (SUT IO blk, Tracer IO String)
-> PropertyM IO (SUT IO blk, Tracer IO String)
forall a b. (a -> b) -> a -> b
$ LedgerConfig blk
-> LedgerState blk ValuesMK -> IO (SUT IO blk, Tracer IO String)
forall (m :: * -> *) blk.
(NoThunks (MockedLedgerDB blk), IOLike m,
 LedgerSupportsProtocol blk, LedgerSupportsMempool blk,
 HasTxId (GenTx blk)) =>
LedgerConfig blk
-> LedgerState blk ValuesMK -> m (SUT m blk, Tracer m String)
mkSUT LedgerConfig blk
cfg LedgerState blk ValuesMK
initialState
        ior <- run $ newTVarIO sut
        let sm' = StateMachine (Model blk) (Command blk) IO (Response blk)
-> Tracer IO String
-> StrictTVar IO (SUT IO blk)
-> StateMachine (Model blk) (Command blk) IO (Response blk)
forall blk (m :: * -> *).
(LedgerSupportsMempool blk, IOLike m, ValidateEnvelope blk) =>
StateMachine (Model blk) (Command blk) m (Response blk)
-> Tracer m String
-> StrictTVar m (SUT m blk)
-> StateMachine (Model blk) (Command blk) m (Response blk)
sm StateMachine (Model blk) (Command blk) IO (Response blk)
sm0 Tracer IO String
trcr StrictTVar IO (SUT IO blk)
ior
        (hist, model, res) <- runCommands sm' cmds
        prettyCommands sm0 hist
          $ checkCommandNames cmds
          $ tabulate "Command sequence length"
              [QC.lengthCommands cmds `bucketiseBy` 10]
          $ tabulate "Maximum ticket number"
              [(\(TicketNo Word64
t) -> Word64
t) (modelLastSeenTicketNo model) `bucketiseBy` 5]
          $ tabulate "Number of txs to add"
              [ length txs `bucketiseBy` 10
              | (_, Invocation (Action (TryAddTxs txs)) _) <- unHistory hist
              ]
          $ res === Ok
    )
  where
    sm0 :: StateMachine (Model blk) (Command blk) IO (Response blk)
sm0 = LedgerConfig blk
-> LedgerState blk ValuesMK
-> TxMeasure blk
-> MakeAtomic
-> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
-> StateMachine (Model blk) (Command blk) IO (Response blk)
forall blk (m :: * -> *).
(blk ~ TestBlock, LedgerSupportsMempool blk,
 LedgerSupportsProtocol blk, Monad m) =>
LedgerConfig blk
-> LedgerState blk ValuesMK
-> TxMeasure blk
-> MakeAtomic
-> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
-> StateMachine (Model blk) (Command blk) m (Response blk)
smUnused LedgerConfig blk
cfg LedgerState blk ValuesMK
initialState TxMeasure blk
capacity MakeAtomic
DontCare Int -> LedgerState blk ValuesMK -> Gen [GenTx blk]
gTxs

    bucketiseBy :: a -> a -> String
bucketiseBy a
v a
n =
      let
        l :: a
l = (a
v a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
n) a -> a -> a
forall a. Num a => a -> a -> a
* a
n
      in
        String
"[" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> a -> String
forall a. Show a => a -> String
show a
l String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"-" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> a -> String
forall a. Show a => a -> String
show (a
l a -> a -> a
forall a. Num a => a -> a -> a
+ a
n) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
")"

prop_mempoolParallel ::
  ( HasTxId (GenTx blk)
  , blk ~ TestBlock
  , LedgerSupportsMempool blk
  , LedgerSupportsProtocol blk
  )
  => LedgerConfig blk
  -> TxMeasure blk
  -> LedgerState blk ValuesMK
  -> MakeAtomic
  -> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
  -> Property
prop_mempoolParallel :: forall blk.
(HasTxId (GenTx blk), blk ~ TestBlock, LedgerSupportsMempool blk,
 LedgerSupportsProtocol blk) =>
LedgerConfig blk
-> TxMeasure blk
-> LedgerState blk ValuesMK
-> MakeAtomic
-> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
-> Property
prop_mempoolParallel LedgerConfig blk
cfg TxMeasure blk
capacity LedgerState blk ValuesMK
initialState MakeAtomic
ma Int -> LedgerState blk ValuesMK -> Gen [GenTx blk]
gTxs = StateMachine (Model blk) (Command blk) IO (Response blk)
-> Maybe Int
-> Int
-> (ParallelCommands (Command blk) (Response blk) -> Property)
-> Property
forall prop (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       (model :: (* -> *) -> *) (m :: * -> *).
(Testable prop, Show (cmd Symbolic), Show (resp Symbolic),
 Show (model Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Maybe Int
-> Int
-> (ParallelCommands cmd resp -> prop)
-> Property
forAllParallelCommandsNTimes StateMachine (Model blk) (Command blk) IO (Response blk)
sm0 Maybe Int
forall a. Maybe a
Nothing Int
100 ((ParallelCommands (Command blk) (Response blk) -> Property)
 -> Property)
-> (ParallelCommands (Command blk) (Response blk) -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$
  \ParallelCommands (Command blk) (Response blk)
cmds -> PropertyM IO () -> Property
forall a. Testable a => PropertyM IO a -> Property
monadicIO (PropertyM IO () -> Property) -> PropertyM IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
        (sut, trcr) <- IO (SUT IO blk, Tracer IO String)
-> PropertyM IO (SUT IO blk, Tracer IO String)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (IO (SUT IO blk, Tracer IO String)
 -> PropertyM IO (SUT IO blk, Tracer IO String))
-> IO (SUT IO blk, Tracer IO String)
-> PropertyM IO (SUT IO blk, Tracer IO String)
forall a b. (a -> b) -> a -> b
$ LedgerConfig blk
-> LedgerState blk ValuesMK -> IO (SUT IO blk, Tracer IO String)
forall (m :: * -> *) blk.
(NoThunks (MockedLedgerDB blk), IOLike m,
 LedgerSupportsProtocol blk, LedgerSupportsMempool blk,
 HasTxId (GenTx blk)) =>
LedgerConfig blk
-> LedgerState blk ValuesMK -> m (SUT m blk, Tracer m String)
mkSUT LedgerConfig blk
cfg LedgerState blk ValuesMK
initialState
        ior <- run $ newTVarIO sut
        let sm' = StateMachine (Model blk) (Command blk) IO (Response blk)
-> Tracer IO String
-> StrictTVar IO (SUT IO blk)
-> StateMachine (Model blk) (Command blk) IO (Response blk)
forall blk (m :: * -> *).
(LedgerSupportsMempool blk, IOLike m, ValidateEnvelope blk) =>
StateMachine (Model blk) (Command blk) m (Response blk)
-> Tracer m String
-> StrictTVar m (SUT m blk)
-> StateMachine (Model blk) (Command blk) m (Response blk)
sm StateMachine (Model blk) (Command blk) IO (Response blk)
sm0 Tracer IO String
trcr StrictTVar IO (SUT IO blk)
ior
        res <- runParallelCommands sm' cmds
        prettyParallelCommandsWithOpts
          cmds
          (Just (GraphOptions "./mempoolParallel.png" Png))
          res
 where
   sm0 :: StateMachine (Model blk) (Command blk) IO (Response blk)
sm0 = LedgerConfig blk
-> LedgerState blk ValuesMK
-> TxMeasure blk
-> MakeAtomic
-> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
-> StateMachine (Model blk) (Command blk) IO (Response blk)
forall blk (m :: * -> *).
(blk ~ TestBlock, LedgerSupportsMempool blk,
 LedgerSupportsProtocol blk, Monad m) =>
LedgerConfig blk
-> LedgerState blk ValuesMK
-> TxMeasure blk
-> MakeAtomic
-> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
-> StateMachine (Model blk) (Command blk) m (Response blk)
smUnused LedgerConfig blk
cfg LedgerState blk ValuesMK
initialState TxMeasure blk
capacity MakeAtomic
ma Int -> LedgerState blk ValuesMK -> Gen [GenTx blk]
gTxs

-- | See 'MakeAtomic' on the reasoning behind having these tests.
tests :: TestTree
tests :: TestTree
tests = String -> [TestTree] -> TestTree
testGroup String
"QSM"
        [ String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty String
"sequential"
          (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
1000 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ LedgerConfig TestBlock
-> TxMeasure TestBlock
-> LedgerState TestBlock ValuesMK
-> (Int -> LedgerState TestBlock ValuesMK -> Gen [GenTx TestBlock])
-> Property
forall blk.
(HasTxId (GenTx blk), blk ~ TestBlock, LedgerSupportsMempool blk,
 LedgerSupportsProtocol blk) =>
LedgerConfig blk
-> TxMeasure blk
-> LedgerState blk ValuesMK
-> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
-> Property
prop_mempoolSequential LedgerConfig TestBlock
testLedgerConfigNoSizeLimits IgnoringOverflow ByteSize32
TxMeasure TestBlock
txMaxBytes' LedgerState TestBlock ValuesMK
testInitLedger
          ((Int -> LedgerState TestBlock ValuesMK -> Gen [GenTx TestBlock])
 -> Property)
-> (Int -> LedgerState TestBlock ValuesMK -> Gen [GenTx TestBlock])
-> Property
forall a b. (a -> b) -> a -> b
$ \Int
i -> (([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
 -> [GenTx TestBlock])
-> Gen ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
-> Gen [GenTx TestBlock]
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((GenTx TestBlock, Bool) -> GenTx TestBlock)
-> [(GenTx TestBlock, Bool)] -> [GenTx TestBlock]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (GenTx TestBlock, Bool) -> GenTx TestBlock
forall a b. (a, b) -> a
fst ([(GenTx TestBlock, Bool)] -> [GenTx TestBlock])
-> (([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
    -> [(GenTx TestBlock, Bool)])
-> ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
-> [GenTx TestBlock]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
-> [(GenTx TestBlock, Bool)]
forall a b. (a, b) -> a
fst) (Gen ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
 -> Gen [GenTx TestBlock])
-> (LedgerState TestBlock ValuesMK
    -> Gen ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK))
-> LedgerState TestBlock ValuesMK
-> Gen [GenTx TestBlock]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int
-> LedgerState TestBlock ValuesMK
-> Gen ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
genTxs Int
i
        , String -> [TestTree] -> TestTree
testGroup String
"parallel"
          [ String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty String
"atomic"
            (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
1000 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ LedgerConfig TestBlock
-> TxMeasure TestBlock
-> LedgerState TestBlock ValuesMK
-> MakeAtomic
-> (Int -> LedgerState TestBlock ValuesMK -> Gen [GenTx TestBlock])
-> Property
forall blk.
(HasTxId (GenTx blk), blk ~ TestBlock, LedgerSupportsMempool blk,
 LedgerSupportsProtocol blk) =>
LedgerConfig blk
-> TxMeasure blk
-> LedgerState blk ValuesMK
-> MakeAtomic
-> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
-> Property
prop_mempoolParallel LedgerConfig TestBlock
testLedgerConfigNoSizeLimits IgnoringOverflow ByteSize32
TxMeasure TestBlock
txMaxBytes' LedgerState TestBlock ValuesMK
testInitLedger MakeAtomic
Atomic
            ((Int -> LedgerState TestBlock ValuesMK -> Gen [GenTx TestBlock])
 -> Property)
-> (Int -> LedgerState TestBlock ValuesMK -> Gen [GenTx TestBlock])
-> Property
forall a b. (a -> b) -> a -> b
$ \Int
i -> (([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
 -> [GenTx TestBlock])
-> Gen ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
-> Gen [GenTx TestBlock]
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((GenTx TestBlock, Bool) -> GenTx TestBlock)
-> [(GenTx TestBlock, Bool)] -> [GenTx TestBlock]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (GenTx TestBlock, Bool) -> GenTx TestBlock
forall a b. (a, b) -> a
fst ([(GenTx TestBlock, Bool)] -> [GenTx TestBlock])
-> (([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
    -> [(GenTx TestBlock, Bool)])
-> ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
-> [GenTx TestBlock]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
-> [(GenTx TestBlock, Bool)]
forall a b. (a, b) -> a
fst) (Gen ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
 -> Gen [GenTx TestBlock])
-> (LedgerState TestBlock ValuesMK
    -> Gen ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK))
-> LedgerState TestBlock ValuesMK
-> Gen [GenTx TestBlock]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int
-> LedgerState TestBlock ValuesMK
-> Gen ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
genTxs Int
i
          , String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty String
"non atomic"
            (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
10 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ LedgerConfig TestBlock
-> TxMeasure TestBlock
-> LedgerState TestBlock ValuesMK
-> MakeAtomic
-> (Int -> LedgerState TestBlock ValuesMK -> Gen [GenTx TestBlock])
-> Property
forall blk.
(HasTxId (GenTx blk), blk ~ TestBlock, LedgerSupportsMempool blk,
 LedgerSupportsProtocol blk) =>
LedgerConfig blk
-> TxMeasure blk
-> LedgerState blk ValuesMK
-> MakeAtomic
-> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
-> Property
prop_mempoolParallel LedgerConfig TestBlock
testLedgerConfigNoSizeLimits IgnoringOverflow ByteSize32
TxMeasure TestBlock
txMaxBytes' LedgerState TestBlock ValuesMK
testInitLedger MakeAtomic
NonAtomic
            ((Int -> LedgerState TestBlock ValuesMK -> Gen [GenTx TestBlock])
 -> Property)
-> (Int -> LedgerState TestBlock ValuesMK -> Gen [GenTx TestBlock])
-> Property
forall a b. (a -> b) -> a -> b
$ \Int
i -> (([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
 -> [GenTx TestBlock])
-> Gen ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
-> Gen [GenTx TestBlock]
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((GenTx TestBlock, Bool) -> GenTx TestBlock)
-> [(GenTx TestBlock, Bool)] -> [GenTx TestBlock]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (GenTx TestBlock, Bool) -> GenTx TestBlock
forall a b. (a, b) -> a
fst ([(GenTx TestBlock, Bool)] -> [GenTx TestBlock])
-> (([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
    -> [(GenTx TestBlock, Bool)])
-> ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
-> [GenTx TestBlock]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
-> [(GenTx TestBlock, Bool)]
forall a b. (a, b) -> a
fst) (Gen ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
 -> Gen [GenTx TestBlock])
-> (LedgerState TestBlock ValuesMK
    -> Gen ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK))
-> LedgerState TestBlock ValuesMK
-> Gen [GenTx TestBlock]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int
-> LedgerState TestBlock ValuesMK
-> Gen ([(GenTx TestBlock, Bool)], LedgerState TestBlock ValuesMK)
genTxs Int
i
          ]
        ]

{-------------------------------------------------------------------------------
  Instances
-------------------------------------------------------------------------------}

-- | The 'TestBlock' txMaxBytes is fixed to a very high number. We use this
-- local declaration to have a mempool that sometimes fill but still don't make
-- it configurable.
txMaxBytes' :: IgnoringOverflow ByteSize32
txMaxBytes' :: IgnoringOverflow ByteSize32
txMaxBytes' = ByteSize32 -> IgnoringOverflow ByteSize32
forall a. a -> IgnoringOverflow a
IgnoringOverflow (ByteSize32 -> IgnoringOverflow ByteSize32)
-> ByteSize32 -> IgnoringOverflow ByteSize32
forall a b. (a -> b) -> a -> b
$ Word32 -> ByteSize32
ByteSize32 Word32
forall a. Bounded a => a
maxBound

instance (StandardHash blk, GetTip (LedgerState blk)) =>
         Eq (LedgerState blk ValuesMK) where
  == :: LedgerState blk ValuesMK -> LedgerState blk ValuesMK -> Bool
(==) = Point (LedgerState blk) -> Point (LedgerState blk) -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Point (LedgerState blk) -> Point (LedgerState blk) -> Bool)
-> (LedgerState blk ValuesMK -> Point (LedgerState blk))
-> LedgerState blk ValuesMK
-> LedgerState blk ValuesMK
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` LedgerState blk ValuesMK -> Point (LedgerState blk)
forall (mk :: MapKind).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: MapKind).
GetTip l =>
l mk -> Point l
getTip

instance (UnTick blk, StandardHash blk, GetTip (LedgerState blk)) =>
         Eq (TickedLedgerState blk ValuesMK) where
  == :: TickedLedgerState blk ValuesMK
-> TickedLedgerState blk ValuesMK -> Bool
(==) = Point (LedgerState blk) -> Point (LedgerState blk) -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Point (LedgerState blk) -> Point (LedgerState blk) -> Bool)
-> (TickedLedgerState blk ValuesMK -> Point (LedgerState blk))
-> TickedLedgerState blk ValuesMK
-> TickedLedgerState blk ValuesMK
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (LedgerState blk ValuesMK -> Point (LedgerState blk)
forall (mk :: MapKind).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: MapKind).
GetTip l =>
l mk -> Point l
getTip (LedgerState blk ValuesMK -> Point (LedgerState blk))
-> (TickedLedgerState blk ValuesMK -> LedgerState blk ValuesMK)
-> TickedLedgerState blk ValuesMK
-> Point (LedgerState blk)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TickedLedgerState blk ValuesMK -> LedgerState blk ValuesMK
forall blk (mk :: MapKind).
UnTick blk =>
TickedLedgerState blk mk -> LedgerState blk mk
forall (mk :: MapKind).
TickedLedgerState blk mk -> LedgerState blk mk
unTick)

instance (StandardHash blk, GetTip (LedgerState blk)) =>
         Ord (LedgerState blk ValuesMK) where
  compare :: LedgerState blk ValuesMK -> LedgerState blk ValuesMK -> Ordering
compare = Point (LedgerState blk) -> Point (LedgerState blk) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Point (LedgerState blk) -> Point (LedgerState blk) -> Ordering)
-> (LedgerState blk ValuesMK -> Point (LedgerState blk))
-> LedgerState blk ValuesMK
-> LedgerState blk ValuesMK
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` LedgerState blk ValuesMK -> Point (LedgerState blk)
forall (mk :: MapKind).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: MapKind).
GetTip l =>
l mk -> Point l
getTip

instance (Eq (Validated (GenTx blk)), m ~ TxMeasure blk, Eq m) => Eq (TxSeq m (Validated (GenTx blk))) where
  TxSeq m (Validated (GenTx blk))
s1 == :: TxSeq m (Validated (GenTx blk))
-> TxSeq m (Validated (GenTx blk)) -> Bool
== TxSeq m (Validated (GenTx blk))
s2 = TxSeq m (Validated (GenTx blk))
-> [TxTicket m (Validated (GenTx blk))]
forall sz tx. TxSeq sz tx -> [TxTicket sz tx]
toList TxSeq m (Validated (GenTx blk))
s1 [TxTicket m (Validated (GenTx blk))]
-> [TxTicket m (Validated (GenTx blk))] -> Bool
forall a. Eq a => a -> a -> Bool
== TxSeq m (Validated (GenTx blk))
-> [TxTicket m (Validated (GenTx blk))]
forall sz tx. TxSeq sz tx -> [TxTicket sz tx]
toList TxSeq m (Validated (GenTx blk))
s2

instance NoThunks (Mempool IO TestBlock) where
  showTypeOf :: Proxy (Mempool IO TestBlock) -> String
showTypeOf Proxy (Mempool IO TestBlock)
_  = Proxy (Mempool IO TestBlock) -> String
forall a. NoThunks a => Proxy a -> String
showTypeOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Mempool IO TestBlock))
  wNoThunks :: Context -> Mempool IO TestBlock -> IO (Maybe ThunkInfo)
wNoThunks Context
_ Mempool IO TestBlock
_ = Maybe ThunkInfo -> IO (Maybe ThunkInfo)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ThunkInfo
forall a. Maybe a
Nothing

instance ( ToExpr (TxId (GenTx blk))
         , ToExpr (GenTx blk)
         , ToExpr (LedgerState blk ValuesMK)
         , ToExpr (TickedLedgerState blk ValuesMK)
         , LedgerSupportsMempool blk
         ) => ToExpr (Model blk r) where

  toExpr :: Model blk r -> Expr
toExpr Model blk r
model = String -> OMap String Expr -> Expr
Rec String
"Model" (OMap String Expr -> Expr) -> OMap String Expr -> Expr
forall a b. (a -> b) -> a -> b
$ [(String, Expr)] -> OMap String Expr
forall k v. Ord k => [(k, v)] -> OMap k v
TD.fromList
    [ (String
"mempoolTip", TickedLedgerState blk ValuesMK -> Expr
forall a. ToExpr a => a -> Expr
toExpr (TickedLedgerState blk ValuesMK -> Expr)
-> TickedLedgerState blk ValuesMK -> Expr
forall a b. (a -> b) -> a -> b
$ Model blk r -> TickedLedgerState blk ValuesMK
forall {k} blk (r :: k).
Model blk r -> TickedLedgerState blk ValuesMK
modelMempoolIntermediateState Model blk r
model)
    , (String
"ledgerTip", LedgerState blk ValuesMK -> Expr
forall a. ToExpr a => a -> Expr
toExpr (LedgerState blk ValuesMK -> Expr)
-> LedgerState blk ValuesMK -> Expr
forall a b. (a -> b) -> a -> b
$ Model blk r -> LedgerState blk ValuesMK
forall {k} blk (r :: k). Model blk r -> LedgerState blk ValuesMK
modelLedgerDBTip Model blk r
model)
    , (String
"txs", [(GenTx blk, TicketNo)] -> Expr
forall a. ToExpr a => a -> Expr
toExpr ([(GenTx blk, TicketNo)] -> Expr)
-> [(GenTx blk, TicketNo)] -> Expr
forall a b. (a -> b) -> a -> b
$ Model blk r -> [(GenTx blk, TicketNo)]
forall {k} blk (r :: k). Model blk r -> [(GenTx blk, TicketNo)]
modelTxs Model blk r
model)
    , (String
"size", Word32 -> Expr
forall a. ToExpr a => a -> Expr
toExpr (Word32 -> Expr) -> Word32 -> Expr
forall a b. (a -> b) -> a -> b
$ ByteSize32 -> Word32
unByteSize32 (ByteSize32 -> Word32) -> ByteSize32 -> Word32
forall a b. (a -> b) -> a -> b
$ TxMeasure blk -> ByteSize32
forall a. HasByteSize a => a -> ByteSize32
txMeasureByteSize (TxMeasure blk -> ByteSize32) -> TxMeasure blk -> ByteSize32
forall a b. (a -> b) -> a -> b
$ Model blk r -> TxMeasure blk
forall {k} blk (r :: k). Model blk r -> TxMeasure blk
modelCurrentSize Model blk r
model)
    , (String
"capacity", Word32 -> Expr
forall a. ToExpr a => a -> Expr
toExpr (Word32 -> Expr) -> Word32 -> Expr
forall a b. (a -> b) -> a -> b
$ ByteSize32 -> Word32
unByteSize32 (ByteSize32 -> Word32) -> ByteSize32 -> Word32
forall a b. (a -> b) -> a -> b
$ TxMeasure blk -> ByteSize32
forall a. HasByteSize a => a -> ByteSize32
txMeasureByteSize (TxMeasure blk -> ByteSize32) -> TxMeasure blk -> ByteSize32
forall a b. (a -> b) -> a -> b
$ Model blk r -> TxMeasure blk
forall {k} blk (r :: k). Model blk r -> TxMeasure blk
modelCapacity Model blk r
model)
    , (String
"lastTicket", TicketNo -> Expr
forall a. ToExpr a => a -> Expr
toExpr (TicketNo -> Expr) -> TicketNo -> Expr
forall a b. (a -> b) -> a -> b
$ Model blk r -> TicketNo
forall {k} blk (r :: k). Model blk r -> TicketNo
modelLastSeenTicketNo Model blk r
model)]

instance ( ToExpr (TxId (GenTx blk))
         , ToExpr (GenTx blk)
         , ToExpr (TickedLedgerState blk ValuesMK)
         , ToExpr (LedgerState blk ValuesMK)
         , LedgerSupportsMempool blk) => Show (Model blk r) where
  show :: Model blk r -> String
show = Expr -> String
forall a. Show a => a -> String
show (Expr -> String) -> (Model blk r -> Expr) -> Model blk r -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model blk r -> Expr
forall a. ToExpr a => a -> Expr
toExpr

instance ToExpr (Action TestBlock r) where
  toExpr :: Action TestBlock r -> Expr
toExpr (TryAddTxs [GenTx TestBlock]
txs) = String -> [Expr] -> Expr
App String
"TryAddTxs" ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$
    [ String -> [Expr] -> Expr
App (Int -> String -> String
forall a. Int -> [a] -> [a]
take Int
8 (String -> String
forall a. HasCallStack => [a] -> [a]
tail (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. HasCallStack => [a] -> [a]
init (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ TxId -> String
forall a. Show a => a -> String
show TxId
txid)
           String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" "
           String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [(String, Ix)] -> String
forall a. Show a => a -> String
show [ (Int -> String -> String
forall a. Int -> [a] -> [a]
take Int
8 (String -> String
forall a. HasCallStack => [a] -> [a]
tail (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. HasCallStack => [a] -> [a]
init (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ TxId -> String
forall a. Show a => a -> String
show TxId
a), Ix
b) | (TxId
a,Ix
b) <- Set (TxId, Ix) -> [(TxId, Ix)]
forall a. Set a -> [a]
Set.toList Set (TxId, Ix)
txins ]
           String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" ->> "
           String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [(String, Ix)] -> String
forall a. Show a => a -> String
show [ ( Addr -> String
forall a. Condense a => a -> String
condense Addr
a, Ix
b) | ((TxId, Ix)
_,(Addr
a, Ix
b)) <- Map (TxId, Ix) TxOut -> [((TxId, Ix), TxOut)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (TxId, Ix) TxOut
txouts ]
           String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"") [] | SimpleGenTx Tx
tx TxId
txid <- [GenTx TestBlock]
txs
       , let txins :: Set (TxId, Ix)
txins = Tx -> Set (TxId, Ix)
forall a. HasMockTxs a => a -> Set (TxId, Ix)
Mock.txIns Tx
tx
       , let txouts :: Map (TxId, Ix) TxOut
txouts = Tx -> Map (TxId, Ix) TxOut
forall a. HasMockTxs a => a -> Map (TxId, Ix) TxOut
Mock.txOuts Tx
tx]
  toExpr Action TestBlock r
SyncLedger      = String -> [Expr] -> Expr
App String
"SyncLedger" []
  toExpr Action TestBlock r
GetSnapshot     = String -> [Expr] -> Expr
App String
"GetSnapshot" []

instance ToExpr (LedgerState blk ValuesMK) => ToExpr (Event blk r) where
  toExpr :: Event blk r -> Expr
toExpr (ChangeLedger LedgerState blk ValuesMK
ls ModifyDB
b) =
      String -> OMap String Expr -> Expr
Rec String
"ChangeLedger" (OMap String Expr -> Expr) -> OMap String Expr -> Expr
forall a b. (a -> b) -> a -> b
$ [(String, Expr)] -> OMap String Expr
forall k v. Ord k => [(k, v)] -> OMap k v
TD.fromList [ (String
"tip",  LedgerState blk ValuesMK -> Expr
forall a. ToExpr a => a -> Expr
toExpr LedgerState blk ValuesMK
ls)
                                       , (String
"newFork", ModifyDB -> Expr
forall a. ToExpr a => a -> Expr
toExpr ModifyDB
b) ]

instance ToExpr (Command TestBlock r) where
  toExpr :: Command TestBlock r -> Expr
toExpr (Action Action TestBlock r
act) = Action TestBlock r -> Expr
forall a. ToExpr a => a -> Expr
toExpr Action TestBlock r
act
  toExpr (Event Event TestBlock r
ev)   = Event TestBlock r -> Expr
forall a. ToExpr a => a -> Expr
toExpr Event TestBlock r
ev

instance ToExpr (Command blk r) => Show (Command blk r) where
  show :: Command blk r -> String
show = -- unwords . take 2 . words .
    Expr -> String
forall a. Show a => a -> String
show (Expr -> String)
-> (Command blk r -> Expr) -> Command blk r -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Command blk r -> Expr
forall a. ToExpr a => a -> Expr
toExpr

instance ( ToExpr (GenTx blk)
         , LedgerSupportsMempool blk) => ToExpr (Response blk r) where

  toExpr :: Response blk r -> Expr
toExpr Response blk r
Void = String -> [Expr] -> Expr
App String
"Void" []
  toExpr (GotSnapshot [(GenTx blk, TicketNo)]
s) =
    String -> OMap String Expr -> Expr
Rec String
"GotSnapshot" (OMap String Expr -> Expr) -> OMap String Expr -> Expr
forall a b. (a -> b) -> a -> b
$
      [(String, Expr)] -> OMap String Expr
forall k v. Ord k => [(k, v)] -> OMap k v
TD.fromList [ (String
"txs", [(GenTx blk, TicketNo)] -> Expr
forall a. ToExpr a => a -> Expr
toExpr [(GenTx blk, TicketNo)]
s) ]

instance ( ToExpr (GenTx blk)
         , LedgerSupportsMempool blk) => Show (Response blk r) where
  show :: Response blk r -> String
show = -- unwords . take 2 . words .
    Expr -> String
forall a. Show a => a -> String
show (Expr -> String)
-> (Response blk r -> Expr) -> Response blk r -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Response blk r -> Expr
forall a. ToExpr a => a -> Expr
toExpr

deriving instance NoThunks (LedgerState blk ValuesMK) => NoThunks (MockedLedgerDB blk)

instance Arbitrary (LedgerState TestBlock ValuesMK) where
  arbitrary :: Gen (LedgerState TestBlock ValuesMK)
arbitrary = do
    n <- Positive Int -> Int
forall a. Positive a -> a
getPositive (Positive Int -> Int) -> Gen (Positive Int) -> Gen Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Positive Int)
forall a. Arbitrary a => Gen a
arbitrary
    (txs, _) <- genValidTxs n testInitLedger
    case runExcept $ repeatedlyM (flip (applyTxToLedger testLedgerConfigNoSizeLimits)) txs testInitLedger of
      Left MockError TestBlock
_   -> String -> Gen (LedgerState TestBlock ValuesMK)
forall a. HasCallStack => String -> a
error String
"Must not happen"
      Right LedgerState TestBlock ValuesMK
st -> LedgerState TestBlock ValuesMK
-> Gen (LedgerState TestBlock ValuesMK)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure LedgerState TestBlock ValuesMK
st

instance ToExpr (TickedLedgerState TestBlock ValuesMK) where
   toExpr :: TickedLedgerState TestBlock ValuesMK -> Expr
toExpr (TickedSimpleLedgerState LedgerState TestBlock ValuesMK
st) = String -> [Expr] -> Expr
App String
"Ticked" [ LedgerState TestBlock ValuesMK -> Expr
forall a. ToExpr a => a -> Expr
toExpr LedgerState TestBlock ValuesMK
st ]

instance ToExpr (LedgerState TestBlock ValuesMK) where
   toExpr :: LedgerState TestBlock ValuesMK -> Expr
toExpr (SimpleLedgerState MockState TestBlock
st LedgerTables (LedgerState TestBlock) ValuesMK
tbs) = String -> OMap String Expr -> Expr
Rec String
"LedgerState" (OMap String Expr -> Expr) -> OMap String Expr -> Expr
forall a b. (a -> b) -> a -> b
$ [(String, Expr)] -> OMap String Expr
forall k v. Ord k => [(k, v)] -> OMap k v
TD.fromList
      [ (String
"state", Point TestBlock -> Expr
forall a. ToExpr a => a -> Expr
toExpr (Point TestBlock -> Expr) -> Point TestBlock -> Expr
forall a b. (a -> b) -> a -> b
$ MockState TestBlock -> Point TestBlock
forall blk. MockState blk -> Point blk
mockTip MockState TestBlock
st)
      , (String
"tables", LedgerTables (LedgerState TestBlock) ValuesMK -> Expr
forall a. ToExpr a => a -> Expr
toExpr LedgerTables (LedgerState TestBlock) ValuesMK
tbs)]

instance ToExpr Addr where
  toExpr :: Addr -> Expr
toExpr Addr
a = String -> [Expr] -> Expr
App (Addr -> String
forall a. Show a => a -> String
show Addr
a) []

deriving instance ToExpr (GenTx TestBlock)
deriving instance ToExpr Tx
deriving instance ToExpr Expiry

instance ToExpr (LedgerTables (LedgerState TestBlock) ValuesMK) where
  toExpr :: LedgerTables (LedgerState TestBlock) ValuesMK -> Expr
toExpr = LedgerTables (LedgerState TestBlock) ValuesMK -> Expr
forall a. (Generic a, GToExpr (Rep a)) => a -> Expr
genericToExpr

instance ToExpr (ValuesMK TxIn TxOut) where
  toExpr :: ValuesMK (TxId, Ix) TxOut -> Expr
toExpr (ValuesMK Map (TxId, Ix) TxOut
m) = String -> [Expr] -> Expr
App String
"Values" [ Map (TxId, Ix) TxOut -> Expr
forall a. ToExpr a => a -> Expr
toExpr Map (TxId, Ix) TxOut
m ]

class UnTick blk where
  unTick :: forall mk. TickedLedgerState blk mk ->  LedgerState blk mk

instance UnTick TestBlock where
  unTick :: forall (mk :: MapKind).
TickedLedgerState TestBlock mk -> LedgerState TestBlock mk
unTick = Ticked (LedgerState TestBlock) mk -> LedgerState TestBlock mk
forall c ext (mk :: MapKind).
Ticked (LedgerState (SimpleBlock c ext)) mk
-> LedgerState (SimpleBlock c ext) mk
getTickedSimpleLedgerState