{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

#if __GLASGOW_HASKELL__ >= 908
{-# 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 (when)
import Control.Monad.Class.MonadTimer.SI (MonadTimer)
import Control.Monad.Except (Except, runExcept)
import Control.Tracer (nullTracer)
import qualified Control.Tracer as CT (Tracer, mkTracer, traceWith)
import qualified Data.Foldable as Foldable
import Data.Function (on)
import qualified Data.List.NonEmpty as NE
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.Abstract hiding (TxIn, TxOut)
import Ouroboros.Consensus.Ledger.SupportsMempool
import Ouroboros.Consensus.Ledger.SupportsProtocol
  ( LedgerSupportsProtocol
  )
import qualified Ouroboros.Consensus.Ledger.Tables.Basics as Ledger
import Ouroboros.Consensus.Ledger.Tables.Utils
import Ouroboros.Consensus.Mempool
import Ouroboros.Consensus.Mempool.Impl.Common (MempoolLedgerDBView (..), 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.Storage.LedgerDB.Forker
import Ouroboros.Consensus.Util
import Ouroboros.Consensus.Util.Condense (condense)
import Ouroboros.Consensus.Util.IOLike hiding (bracket)
import Ouroboros.Network.Block (genesisPoint)
import Test.Cardano.Ledger.TreeDiff ()
import Test.Consensus.Mempool.Util
  ( TestBlock
  , applyTxToLedger
  , bumpTip
  , genTxs
  , genValidTxs
  , testInitLedger
  , testLedgerConfigNoSizeLimits
  )
import Test.QuickCheck
import Test.QuickCheck.Monadic
import Test.StateMachine hiding ((:>))
import Test.StateMachine.DotDrawing
import Test.StateMachine.Types (History (..), HistoryEvent (..))
import qualified Test.StateMachine.Types as QC
import qualified Test.StateMachine.Types.Rank2 as Rank2
import Test.Tasty
import Test.Tasty.HUnit (assertBool, testCase)
import Test.Tasty.QuickCheck
import Test.Util.Orphans.ToExpr ()
import qualified Test.Util.QuickCheck as QC
import Test.Util.ToExpr ()

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

-- | The model
data Model blk r = Model
  { forall {k} blk (r :: k).
Model blk r -> TickedLedgerState blk ValuesMK
modelMempoolIntermediateState :: !(TickedLedgerState blk ValuesMK)
  -- ^ The current tip on the mempool
  , forall {k} blk (r :: k). Model blk r -> LedgerState blk ValuesMK
modelMempoolBase :: !(LedgerState blk ValuesMK)
  -- ^ The (unticked) ledger state the mempool is currently applied on top of,
  -- i.e. the tip it last synced to. Needed to re-derive the mempool after a
  -- 'RemoveTxs', which re-applies the kept txs on this same base rather than
  -- syncing to a new one.
  , forall {k} blk (r :: k). Model blk r -> [(GenTx blk, TicketNo)]
modelTxs :: ![(GenTx blk, TicketNo)]
  , forall {k} blk (r :: k). Model blk r -> [(GenTx blk, TicketNo)]
modelAllValidTxs :: ![(GenTx blk, TicketNo)]
  -- ^ The current list of transactions
  , forall {k} blk (r :: k). Model blk r -> TxMeasure blk
modelCurrentSize :: !(TxMeasure blk)
  -- ^ The current size of the mempool
  , forall {k} blk (r :: k). Model blk r -> TxMeasure blk
modelCapacity :: !(TxMeasure blk)
  , forall {k} blk (r :: k). Model blk r -> TicketNo
modelLastSeenTicketNo :: !TicketNo
  -- ^ Last seen ticket number
  --
  -- This indicates how many transactions have ever been added to the mempool.
  , forall {k} blk (r :: k). Model blk r -> LedgerCfg LedgerState blk
modelConfig :: !(LedgerCfg LedgerState blk)
  , --  * LedgerDB

    forall {k} blk (r :: k). Model blk r -> LedgerState blk ValuesMK
modelLedgerDBTip :: !(LedgerState blk ValuesMK)
  -- ^ The current tip on the ledgerdb
  , forall {k} blk (r :: k).
Model blk r -> Set (LedgerState blk ValuesMK)
modelLedgerDBOtherStates :: !(Set (LedgerState blk ValuesMK))
  -- ^ The old states which are still on the LedgerDB.
  , forall {k} blk (r :: k). Model blk r -> Bool
modelIsSyncing :: !Bool
  }

-- | 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
  | -- | Force-remove transactions (as the forge loop does on a rejected block).
    RemoveTxs ![GenTxId blk]
  | -- | 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 -> [Char])
-> (forall (r :: k). Proxy (Action blk r) -> [[Char]])
-> CommandNames (Action blk)
forall (r :: k). Proxy (Action blk r) -> [[Char]]
forall (r :: k). Action blk r -> [Char]
forall k blk (r :: k). Proxy (Action blk r) -> [[Char]]
forall k blk (r :: k). Action blk r -> [Char]
forall k (cmd :: k -> *).
(forall (r :: k). cmd r -> [Char])
-> (forall (r :: k). Proxy (cmd r) -> [[Char]]) -> CommandNames cmd
$ccmdName :: forall k blk (r :: k). Action blk r -> [Char]
cmdName :: forall (r :: k). Action blk r -> [Char]
$ccmdNames :: forall k blk (r :: k). Proxy (Action blk r) -> [[Char]]
cmdNames :: forall (r :: k). Proxy (Action blk r) -> [[Char]]
CommandNames)

-- | Events external to the mempool
data Event blk r
  = ChangeLedger
      !(LedgerState blk ValuesMK)
  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 -> [Char])
-> (forall (r :: k). Proxy (Event blk r) -> [[Char]])
-> CommandNames (Event blk)
forall (r :: k). Proxy (Event blk r) -> [[Char]]
forall (r :: k). Event blk r -> [Char]
forall k blk (r :: k). Proxy (Event blk r) -> [[Char]]
forall k blk (r :: k). Event blk r -> [Char]
forall k (cmd :: k -> *).
(forall (r :: k). cmd r -> [Char])
-> (forall (r :: k). Proxy (cmd r) -> [[Char]]) -> CommandNames cmd
$ccmdName :: forall k blk (r :: k). Event blk r -> [Char]
cmdName :: forall (r :: k). Event blk r -> [Char]
$ccmdNames :: forall k blk (r :: k). Proxy (Event blk r) -> [[Char]]
cmdNames :: forall (r :: k). Proxy (Event blk r) -> [[Char]]
CommandNames)

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

  cmdNames :: forall r. Proxy (Command blk r) -> [String]
  cmdNames :: forall {k} (r :: k). Proxy (Command blk r) -> [[Char]]
cmdNames Proxy (Command blk r)
_ =
    Proxy (Action blk r) -> [[Char]]
forall (r :: k). Proxy (Action blk r) -> [[Char]]
forall k (cmd :: k -> *) (r :: k).
CommandNames cmd =>
Proxy (cmd r) -> [[Char]]
cmdNames (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Action blk r))
      [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ Proxy (Event blk r) -> [[Char]]
forall (r :: k). Proxy (Event blk r) -> [[Char]]
forall k (cmd :: k -> *) (r :: k).
CommandNames cmd =>
Proxy (cmd r) -> [[Char]]
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)
  , HasTxId (GenTx blk)
  ) =>
  MakeAtomic ->
  -- | Transaction generator based on an state
  (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk]) ->
  Model blk Symbolic ->
  Maybe (Gen (Command blk Symbolic))
generator :: forall blk.
(Arbitrary (LedgerState blk ValuesMK), UnTick blk,
 StandardHash blk, GetTip (LedgerState blk), HasTxId (GenTx 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, Gen (Command blk Symbolic))] -> Gen (Command blk Symbolic))
-> [(Int, Gen (Command blk Symbolic))]
-> Gen (Command blk Symbolic)
forall a b. (a -> b) -> a -> b
$
      [
        ( 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 :: * -> * -> *).
UnTick blk =>
TickedLedgerState blk mk -> LedgerState blk mk
forall (mk :: * -> * -> *).
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 :: * -> * -> *).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: * -> * -> *).
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 :: * -> * -> *).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: * -> * -> *).
GetTip l =>
l mk -> Point l
getTip
                                             Set (LedgerState blk ValuesMK)
modelLedgerDBOtherStates
                                       )
                                     (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 :: * -> * -> *).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: * -> * -> *).
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)
modelLedgerDBOtherStates 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)
modelLedgerDBOtherStates)])
                )
                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 :: * -> * -> *).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: * -> * -> *).
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 :: * -> * -> *).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: * -> * -> *).
GetTip l =>
l mk -> Point l
getTip)
            pure $ Event $ ChangeLedger ls
        )
      , (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)
      ]
        -- Only remove when there is something to remove; races with SyncLedger.
        [(Int, Gen (Command blk Symbolic))]
-> [(Int, Gen (Command blk Symbolic))]
-> [(Int, Gen (Command blk Symbolic))]
forall a. [a] -> [a] -> [a]
++ [ (Int
10, Action blk Symbolic -> Command blk Symbolic
forall {k} blk (r :: k). Action blk r -> Command blk r
Action (Action blk Symbolic -> Command blk Symbolic)
-> ([GenTxId blk] -> Action blk Symbolic)
-> [GenTxId blk]
-> Command blk Symbolic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenTxId blk] -> Action blk Symbolic
forall {k} blk (r :: k). [GenTxId blk] -> Action blk r
RemoveTxs ([GenTxId blk] -> Command blk Symbolic)
-> Gen [GenTxId blk] -> Gen (Command blk Symbolic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([GenTxId blk] -> Gen [GenTxId blk]
forall a. [a] -> Gen [a]
sublistOf (((GenTx blk, TicketNo) -> GenTxId blk)
-> [(GenTx blk, TicketNo)] -> [GenTxId blk]
forall a b. (a -> b) -> [a] -> [b]
map (GenTx blk -> GenTxId blk
forall tx. HasTxId tx => tx -> TxId tx
txId (GenTx blk -> GenTxId blk)
-> ((GenTx blk, TicketNo) -> GenTx blk)
-> (GenTx blk, TicketNo)
-> GenTxId blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenTx blk, TicketNo) -> GenTx blk
forall a b. (a, b) -> a
fst) [(GenTx blk, TicketNo)]
modelTxs) Gen [GenTxId blk] -> ([GenTxId blk] -> Bool) -> Gen [GenTxId blk]
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Bool -> Bool
not (Bool -> Bool) -> ([GenTxId blk] -> Bool) -> [GenTxId blk] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenTxId blk] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null)))
           | Bool -> Bool
not ([(GenTx blk, TicketNo)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(GenTx blk, TicketNo)]
modelTxs)
           ]
 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)
modelLedgerDBOtherStates :: forall {k} blk (r :: k).
Model blk r -> Set (LedgerState blk ValuesMK)
modelLedgerDBOtherStates :: Set (LedgerState blk ValuesMK)
modelLedgerDBOtherStates
    , [(GenTx blk, TicketNo)]
modelTxs :: forall {k} blk (r :: k). Model blk r -> [(GenTx blk, TicketNo)]
modelTxs :: [(GenTx blk, TicketNo)]
modelTxs
    } = Model blk Symbolic
model

data Response blk r
  = -- | Nothing to tell
    Void
  | -- | Return the contents of a snapshot
    GotSnapshot ![(GenTx blk, TicketNo)]
  | AddResult ![MempoolAddTxResult blk]
  | Synced !(Point blk, [(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
    , modelMempoolBase :: LedgerState blk ValuesMK
modelMempoolBase = LedgerState blk ValuesMK
initialState
    , modelLedgerDBOtherStates :: Set (LedgerState blk ValuesMK)
modelLedgerDBOtherStates = 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
    , modelAllValidTxs :: [(GenTx blk, TicketNo)]
modelAllValidTxs = []
    , modelLastSeenTicketNo :: TicketNo
modelLastSeenTicketNo = TicketNo
zeroTicketNo
    , modelCapacity :: TxMeasure blk
modelCapacity = TxMeasure blk
capacity
    , modelConfig :: LedgerConfig blk
modelConfig = LedgerConfig blk
cfg
    , modelIsSyncing :: Bool
modelIsSyncing = Bool
False
    }
 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 -> GenSym (Response blk Symbolic))
-> Response blk Symbolic -> GenSym (Response blk Symbolic)
forall a b. (a -> b) -> a -> b
$ [MempoolAddTxResult blk] -> Response blk Symbolic
forall {k} blk (r :: k). [MempoolAddTxResult blk] -> Response blk r
AddResult []
  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 -> GenSym (Response blk Symbolic))
-> Response blk Symbolic -> GenSym (Response blk Symbolic)
forall a b. (a -> b) -> a -> b
$ (Point blk, [(GenTx blk, TicketNo)]) -> Response blk Symbolic
forall {k} blk (r :: k).
(Point blk, [(GenTx blk, TicketNo)]) -> Response blk r
Synced (Point blk
forall {k} (block :: k). Point block
genesisPoint, [])
  Action (RemoveTxs [GenTxId 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
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
_) -> 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 :: * -> * -> *) 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''
          , modelMempoolBase = modelLedgerDBTip
          , 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 ->
  Model blk r
doChangeLedger :: forall {k} blk (r :: k).
(StandardHash blk, GetTip (LedgerState blk)) =>
Model blk r -> LedgerState blk ValuesMK -> Model blk r
doChangeLedger Model blk r
model LedgerState blk ValuesMK
l' =
  Model blk r
model
    { modelLedgerDBTip = l'
    , modelLedgerDBOtherStates =
        Set.insert modelLedgerDBTip modelLedgerDBOtherStates
    }
 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)
modelLedgerDBOtherStates :: forall {k} blk (r :: k).
Model blk r -> Set (LedgerState blk ValuesMK)
modelLedgerDBOtherStates :: Set (LedgerState blk ValuesMK)
modelLedgerDBOtherStates
    } = Model blk r
model

doTryAddTxs ::
  ( LedgerSupportsMempool blk
  , ValidateEnvelope blk
  ) =>
  Model blk r ->
  [GenTx blk] ->
  Model blk r
doTryAddTxs :: forall {k} blk (r :: k).
(LedgerSupportsMempool blk, ValidateEnvelope 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 (Ticked LedgerState blk ValuesMK -> Point (Ticked LedgerState blk)
forall (mk :: * -> * -> *).
Ticked LedgerState blk mk -> Point (Ticked LedgerState blk)
forall (l :: LedgerStateKind) (mk :: * -> * -> *).
GetTip l =>
l mk -> Point l
getTip Ticked LedgerState 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 :: * -> * -> *).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: * -> * -> *).
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)
modelLedgerDBOtherStates) of
    Maybe (LedgerState blk ValuesMK)
Nothing -> [Char] -> Model blk r
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible!"
    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, Ticked LedgerState blk ValuesMK
st'') =
            LedgerConfig blk
-> TicketNo
-> TxMeasure blk
-> TxMeasure blk
-> Ticked LedgerState blk ValuesMK
-> [(GenTx blk, Maybe TicketNo)]
-> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
    Ticked LedgerState 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 Ticked LedgerState blk ValuesMK
st ([(GenTx blk, Maybe TicketNo)]
 -> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
     Ticked LedgerState blk ValuesMK))
-> [(GenTx blk, Maybe TicketNo)]
-> ([(GenTx blk, TicketNo)], TicketNo, TxMeasure blk,
    Ticked LedgerState 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'
            , modelAllValidTxs = modelAllValidTxs ++ validTxs
            , modelLastSeenTicketNo = pred tk
            , modelCurrentSize = newSize
            }
 where
  Model
    { modelMempoolIntermediateState :: forall {k} blk (r :: k).
Model blk r -> TickedLedgerState blk ValuesMK
modelMempoolIntermediateState = Ticked LedgerState blk ValuesMK
st
    , [(GenTx blk, TicketNo)]
modelTxs :: forall {k} blk (r :: k). Model blk r -> [(GenTx blk, TicketNo)]
modelTxs :: [(GenTx blk, TicketNo)]
modelTxs
    , [(GenTx blk, TicketNo)]
modelAllValidTxs :: forall {k} blk (r :: k). Model blk r -> [(GenTx blk, TicketNo)]
modelAllValidTxs :: [(GenTx blk, TicketNo)]
modelAllValidTxs
    , TxMeasure blk
modelCurrentSize :: forall {k} blk (r :: k). Model blk r -> TxMeasure blk
modelCurrentSize :: TxMeasure blk
modelCurrentSize
    , Set (LedgerState blk ValuesMK)
modelLedgerDBOtherStates :: forall {k} blk (r :: k).
Model blk r -> Set (LedgerState blk ValuesMK)
modelLedgerDBOtherStates :: Set (LedgerState blk ValuesMK)
modelLedgerDBOtherStates
    , 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

-- | Force-remove the given transactions, then re-derive the mempool by
-- re-applying the /kept/ txs against the current base (mirrors
-- 'removeTxsEvenIfValid'/'pureRemoveTxs': the base is unchanged, only the txs
-- shrink).
doRemoveTxs ::
  ( LedgerSupportsMempool blk
  , ValidateEnvelope blk
  , HasTxId (GenTx blk)
  ) =>
  Model blk r ->
  [GenTxId blk] ->
  Model blk r
doRemoveTxs :: forall {k} blk (r :: k).
(LedgerSupportsMempool blk, ValidateEnvelope blk,
 HasTxId (GenTx blk)) =>
Model blk r -> [GenTxId blk] -> Model blk r
doRemoveTxs Model blk r
model [GenTxId blk]
ids =
  let toRemove :: Set (GenTxId blk)
toRemove = [GenTxId blk] -> Set (GenTxId blk)
forall a. Ord a => [a] -> Set a
Set.fromList [GenTxId blk]
ids
      kept :: [(GenTx blk, TicketNo)]
kept = ((GenTx blk, TicketNo) -> Bool)
-> [(GenTx blk, TicketNo)] -> [(GenTx blk, TicketNo)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((GenTxId blk -> Set (GenTxId blk) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set (GenTxId blk)
toRemove) (GenTxId blk -> Bool)
-> ((GenTx blk, TicketNo) -> GenTxId blk)
-> (GenTx blk, TicketNo)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenTx blk -> GenTxId blk
forall tx. HasTxId tx => tx -> TxId tx
txId (GenTx blk -> GenTxId blk)
-> ((GenTx blk, TicketNo) -> GenTx blk)
-> (GenTx blk, TicketNo)
-> GenTxId blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenTx blk, TicketNo) -> GenTx blk
forall a b. (a, b) -> a
fst) [(GenTx blk, TicketNo)]
modelTxs
      ([(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 (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
modelMempoolBase) ([(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 :: * -> * -> *) 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)]
kept
   in Model blk r
model
        { modelMempoolIntermediateState = st''
        , modelTxs = validTxs
        , modelCurrentSize = newSize
        }
 where
  Model
    { LedgerState blk ValuesMK
modelMempoolBase :: forall {k} blk (r :: k). Model blk r -> LedgerState blk ValuesMK
modelMempoolBase :: LedgerState blk ValuesMK
modelMempoolBase
    , [(GenTx blk, TicketNo)]
modelTxs :: forall {k} blk (r :: k). Model blk r -> [(GenTx blk, TicketNo)]
modelTxs :: [(GenTx blk, TicketNo)]
modelTxs
    , LedgerConfig blk
modelConfig :: forall {k} blk (r :: k). Model blk r -> LedgerCfg LedgerState blk
modelConfig :: LedgerConfig blk
modelConfig
    , TxMeasure blk
modelCapacity :: forall {k} blk (r :: k). Model blk r -> TxMeasure blk
modelCapacity :: TxMeasure blk
modelCapacity
    } = Model blk r
model

transition ::
  ( Eq (TickedLedgerState blk ValuesMK)
  , LedgerSupportsMempool blk
  , HasTxId (GenTx 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 (TickedLedgerState blk ValuesMK), LedgerSupportsMempool blk,
 HasTxId (GenTx 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), AddResult [MempoolAddTxResult blk]
_res) -> (Model blk r -> [GenTx blk] -> Model blk r
forall {k} blk (r :: k).
(LedgerSupportsMempool blk, ValidateEnvelope blk) =>
Model blk r -> [GenTx blk] -> Model blk r
doTryAddTxs Model blk r
model [GenTx blk]
txs){modelIsSyncing = False}
  (Event (ChangeLedger LedgerState blk ValuesMK
l), Response blk r
Void) -> (Model blk r -> LedgerState blk ValuesMK -> Model blk r
forall {k} blk (r :: k).
(StandardHash blk, GetTip (LedgerState blk)) =>
Model blk r -> LedgerState blk ValuesMK -> Model blk r
doChangeLedger Model blk r
model LedgerState blk ValuesMK
l){modelIsSyncing = False}
  (Action Action blk r
GetSnapshot, GotSnapshot{}) -> Model blk r
model{modelIsSyncing = False}
  (Action Action blk r
SyncLedger, Synced{}) -> (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){modelIsSyncing = True}
  (Action (RemoveTxs [GenTxId blk]
ids), Response blk r
Void) -> (Model blk r -> [GenTxId blk] -> Model blk r
forall {k} blk (r :: k).
(LedgerSupportsMempool blk, ValidateEnvelope blk,
 HasTxId (GenTx blk)) =>
Model blk r -> [GenTxId blk] -> Model blk r
doRemoveTxs Model blk r
model [GenTxId blk]
ids){modelIsSyncing = False}
  (Command blk r, Response blk r)
_ ->
    [Char] -> Model blk r
forall a. HasCallStack => [Char] -> a
error ([Char] -> Model blk r) -> [Char] -> Model blk r
forall a b. (a -> b) -> a -> b
$
      [Char]
"mismatched command "
        [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Command blk r -> [Char]
forall a. Show a => a -> [Char]
show Command blk r
cmd
        [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" and response "
        [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Response blk r -> [Char]
forall a. Show a => a -> [Char]
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 :: * -> * -> *).
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.
LedgerSupportsMempool blk =>
LedgerConfig blk
-> TickedLedgerState blk ValuesMK
-> GenTx blk
-> Except (ApplyTxErr blk) (TxMeasure blk)
txMeasureFull 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) blk
       (l' :: * -> LedgerStateKind).
(HasLedgerTables l blk, HasLedgerTables l' blk) =>
l blk ValuesMK -> l' blk DiffMK -> l' blk 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

txMeasureFull ::
  LedgerSupportsMempool blk =>
  LedgerConfig blk ->
  TickedLedgerState blk ValuesMK ->
  GenTx blk ->
  Except (ApplyTxErr blk) (TxMeasure blk)
txMeasureFull :: forall blk.
LedgerSupportsMempool blk =>
LedgerConfig blk
-> TickedLedgerState blk ValuesMK
-> GenTx blk
-> Except (ApplyTxErr blk) (TxMeasure blk)
txMeasureFull LedgerConfig blk
cfg TickedLedgerState blk ValuesMK
st GenTx blk
tx =
  TxMeasurePhase1 blk -> TxMeasurePhase2 blk -> TxMeasure blk
forall blk.
TxMeasurePhase1 blk -> TxMeasurePhase2 blk -> TxMeasure blk
TxMeasure
    (TxMeasurePhase1 blk -> TxMeasurePhase2 blk -> TxMeasure blk)
-> ExceptT (ApplyTxErr blk) Identity (TxMeasurePhase1 blk)
-> ExceptT
     (ApplyTxErr blk) Identity (TxMeasurePhase2 blk -> TxMeasure blk)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LedgerConfig blk
-> TickedLedgerState blk EmptyMK
-> GenTx blk
-> ExceptT (ApplyTxErr blk) Identity (TxMeasurePhase1 blk)
forall blk.
TxLimits blk =>
LedgerConfig blk
-> TickedLedgerState blk EmptyMK
-> GenTx blk
-> Except (ApplyTxErr blk) (TxMeasurePhase1 blk)
txMeasurePhase1 LedgerConfig blk
cfg (TickedLedgerState blk ValuesMK -> TickedLedgerState blk EmptyMK
forall (l :: * -> LedgerStateKind) blk (mk :: * -> * -> *).
HasLedgerTables l blk =>
l blk mk -> l blk EmptyMK
forgetLedgerTables TickedLedgerState blk ValuesMK
st) GenTx blk
tx
    ExceptT
  (ApplyTxErr blk) Identity (TxMeasurePhase2 blk -> TxMeasure blk)
-> ExceptT (ApplyTxErr blk) Identity (TxMeasurePhase2 blk)
-> ExceptT (ApplyTxErr blk) Identity (TxMeasure 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
-> TickedLedgerState blk ValuesMK
-> GenTx blk
-> ExceptT (ApplyTxErr blk) Identity (TxMeasurePhase2 blk)
forall blk.
TxLimits blk =>
LedgerConfig blk
-> TickedLedgerState blk ValuesMK
-> GenTx blk
-> Except (ApplyTxErr blk) (TxMeasurePhase2 blk)
txMeasurePhase2 LedgerConfig blk
cfg TickedLedgerState blk ValuesMK
st GenTx blk
tx

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) blk
       (l' :: * -> LedgerStateKind).
(HasLedgerTables l blk, HasLedgerTables l' blk) =>
l blk ValuesMK -> l' blk DiffMK -> l' blk 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) blk (mk :: * -> * -> *).
HasLedgerTables l blk =>
l blk mk -> l blk 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
      -- | A Mempool
      !(Mempool m blk)
      -- | Emulates a ledger db to the extent needed by the ledger interface.
      !(StrictTVar m (MockedLedgerDB blk))
  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))
  , IOLike m
  ) =>
  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
  { forall blk. MockedLedgerDB blk -> LedgerState blk ValuesMK
ldbTip :: !(LedgerState blk ValuesMK)
  -- ^ The current LedgerDB tip
  , forall blk. MockedLedgerDB blk -> Set (LedgerState blk ValuesMK)
reachableTips :: !(Set (LedgerState blk ValuesMK))
  -- ^ States which are still reachable in the LedgerDB
  }
  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 ::
  ( NoThunks (MockedLedgerDB blk)
  , LedgerSupportsMempool blk
  , IOLike m
  ) =>
  LedgerState blk ValuesMK ->
  m (LedgerInterface m blk, StrictTVar m (MockedLedgerDB blk))
newLedgerInterface :: forall blk (m :: * -> *).
(NoThunks (MockedLedgerDB blk), LedgerSupportsMempool blk,
 IOLike m) =>
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) -> MockedLedgerDB blk
forall blk.
LedgerState blk ValuesMK
-> Set (LedgerState blk ValuesMK) -> MockedLedgerDB blk
MockedLedgerDB LedgerState blk ValuesMK
initialLedger Set (LedgerState blk ValuesMK)
forall a. Set a
Set.empty
  pure
    ( LedgerInterface
        { getCurrentLedgerState = do
            st <- ldbTip <$> readTVar t
            pure $
              MempoolLedgerDBView
                (forgetLedgerTables st)
                ( pure $
                    Right $
                      ReadOnlyForker
                        { roforkerClose = pure ()
                        , roforkerReadStatistics = pure $ Statistics 0
                        , roforkerReadTables = pure . ltliftA2 restrictValuesMK (projectLedgerTables st)
                        , roforkerRangeReadTables = const $ pure (emptyLedgerTables, Nothing)
                        , roforkerGetLedgerState = pure $ forgetLedgerTables st
                        }
                )
        }
    , t
    )

-- | Make a SUT
mkSUT ::
  forall m blk.
  ( NoThunks (MockedLedgerDB blk)
  , IOLike m
  , MonadTimer 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, MonadTimer m,
 LedgerSupportsProtocol blk, LedgerSupportsMempool blk,
 HasTxId (GenTx blk)) =>
LedgerConfig blk
-> LedgerState blk ValuesMK -> m (SUT m blk, Tracer m [Char])
mkSUT LedgerConfig blk
cfg LedgerState blk ValuesMK
initialLedger = do
  (lif, t) <- LedgerState blk ValuesMK
-> m (LedgerInterface m blk, StrictTVar m (MockedLedgerDB blk))
forall blk (m :: * -> *).
(NoThunks (MockedLedgerDB blk), LedgerSupportsMempool blk,
 IOLike m) =>
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 [Char] (TraceEventMempool blk) -> m ())
-> Tracer m (Either [Char] (TraceEventMempool blk))
forall (m :: * -> *) a. Applicative m => (a -> m ()) -> Tracer m a
CT.mkTracer ((Either [Char] (TraceEventMempool blk) -> m ())
 -> Tracer m (Either [Char] (TraceEventMempool blk)))
-> (Either [Char] (TraceEventMempool blk) -> m ())
-> Tracer m (Either [Char] (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 [Char] (TraceEventMempool blk) -> STM m ())
-> Either [Char] (TraceEventMempool blk)
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictTChan m (Either [Char] (TraceEventMempool blk))
-> Either [Char] (TraceEventMempool blk) -> STM m ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTChan m a -> a -> STM m ()
writeTChan StrictTChan m (Either [Char] (TraceEventMempool blk))
trcrChan
  mempool <-
    openMempoolWithoutSyncThread
      lif
      cfg
      (MempoolCapacityBytesOverride $ unIgnoringOverflow $ tmPhase1 txMaxBytes')
      (Nothing :: Maybe MempoolTimeoutConfig)
      (CT.mkTracer $ CT.traceWith trcr . Right)
  pure (SUT mempool t, CT.mkTracer $ atomically . writeTChan trcrChan . Left)

semantics ::
  ( LedgerSupportsMempool blk
  , ValidateEnvelope blk
  , IOLike m
  ) =>
  CT.Tracer m String ->
  Command blk Concrete ->
  StrictTVar m (SUT m blk) ->
  m (Response blk Concrete)
semantics :: forall blk (m :: * -> *).
(LedgerSupportsMempool blk, ValidateEnvelope blk, IOLike m) =>
Tracer m [Char]
-> Command blk Concrete
-> StrictTVar m (SUT m blk)
-> m (Response blk Concrete)
semantics Tracer m [Char]
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
      [MempoolAddTxResult blk] -> Response blk Concrete
forall {k} blk (r :: k). [MempoolAddTxResult blk] -> Response blk r
AddResult ([MempoolAddTxResult blk] -> Response blk Concrete)
-> m [MempoolAddTxResult blk] -> m (Response blk Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GenTx blk -> m (MempoolAddTxResult blk))
-> [GenTx blk] -> m [MempoolAddTxResult blk]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
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
    Action Action blk Concrete
SyncLedger -> do
      snap <- Mempool m blk -> m (MempoolSnapshot blk)
forall (m :: * -> *) blk. Mempool m blk -> m (MempoolSnapshot blk)
testSyncWithLedger Mempool m blk
m
      pure (Synced (snapshotPoint snap, [(txForgetValidated tt, tk) | (tt, tk, _) <- snapshotTxs snap]))
    Action (RemoveTxs [GenTxId blk]
ids) -> do
      case [GenTxId blk] -> Maybe (NonEmpty (GenTxId blk))
forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty [GenTxId blk]
ids of
        Maybe (NonEmpty (GenTxId blk))
Nothing -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        Just NonEmpty (GenTxId blk)
neids -> Mempool m blk -> NonEmpty (GenTxId blk) -> m ()
forall (m :: * -> *) blk.
Mempool m blk -> NonEmpty (GenTxId blk) -> m ()
removeTxsEvenIfValid Mempool m blk
m NonEmpty (GenTxId blk)
neids
      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') -> do
      Tracer m [Char] -> [Char] -> m ()
forall (m :: * -> *) a. Monad m => Tracer m a -> a -> m ()
CT.traceWith Tracer m [Char]
trcr ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"ChangingLedger to " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Point (LedgerState blk) -> [Char]
forall a. Show a => a -> [Char]
show (LedgerState blk ValuesMK -> Point (LedgerState blk)
forall (mk :: * -> * -> *).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: * -> * -> *).
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 <- 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
            pure ()
          else
            writeTVar t (MockedLedgerDB l' (Set.insert ledgerTip oldReachableTips))
        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
m (Action Action blk Symbolic
SyncLedger) = Bool -> Logic
Boolean (Bool -> Logic) -> Bool -> Logic
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Model blk Symbolic -> Bool
forall {k} blk (r :: k). Model blk r -> Bool
modelIsSyncing Model blk Symbolic
m)
precondition Model blk Symbolic
_ (Action (RemoveTxs [GenTxId blk]
ids)) = Bool -> Logic
Boolean (Bool -> Logic) -> Bool -> Logic
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not ([GenTxId blk] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [GenTxId blk]
ids)
precondition Model blk Symbolic
_ Command blk Symbolic
_ = Logic
Top

postcondition ::
  ( LedgerSupportsMempool blk
  , Eq (GenTx blk)
  , HasTxId (GenTx blk)
  , --  , Show (TickedLedgerState blk ValuesMK)
    UnTick blk
  , ValidateEnvelope blk
  , ToExpr (Command blk Concrete)
  , ToExpr (GenTx blk)
  , Show (Ledger.TxIn blk)
  , Show (Ledger.TxOut blk)
  ) =>
  Model blk Concrete ->
  Command blk Concrete ->
  Response blk Concrete ->
  Logic
postcondition :: forall blk.
(LedgerSupportsMempool blk, Eq (GenTx blk), HasTxId (GenTx blk),
 UnTick blk, ValidateEnvelope blk, ToExpr (Command blk Concrete),
 ToExpr (GenTx blk), Show (TxIn blk), Show (TxOut 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) =
  [Char] -> Logic -> Logic
Annotate [Char]
"Mismatch getting snapshot" (Logic -> Logic) -> Logic -> Logic
forall a b. (a -> b) -> a -> b
$
    [Char] -> Logic -> Logic
Annotate ([(GenTx blk, TicketNo)] -> [Char]
forall a. Show a => a -> [Char]
show ([(GenTx blk, TicketNo)] -> [Char])
-> [(GenTx blk, TicketNo)] -> [Char]
forall a b. (a -> b) -> a -> b
$ Model blk Concrete -> [(GenTx blk, TicketNo)]
forall {k} blk (r :: k). Model blk r -> [(GenTx blk, TicketNo)]
modelAllValidTxs Model blk Concrete
model) (Logic -> Logic) -> Logic -> Logic
forall a b. (a -> b) -> a -> b
$
      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
model c :: Command blk Concrete
c@(Action (TryAddTxs [GenTx blk]
txs)) r :: Response blk Concrete
r@(AddResult [MempoolAddTxResult blk]
res) =
  let model' :: Model blk Concrete
model' = Model blk Concrete
-> Command blk Concrete
-> Response blk Concrete
-> Model blk Concrete
forall {k} blk (r :: k).
(Eq (TickedLedgerState blk ValuesMK), LedgerSupportsMempool blk,
 HasTxId (GenTx 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 Concrete
model Command blk Concrete
c Response blk Concrete
r
   in [Char] -> Logic -> Logic
Annotate [Char]
"Mismatch result adding transaction" (Logic -> Logic) -> Logic -> Logic
forall a b. (a -> b) -> a -> b
$
        [Char] -> Logic -> Logic
Annotate (([(GenTx blk, TicketNo)], [(GenTx blk, MempoolAddTxResult blk)])
-> [Char]
forall a. Show a => a -> [Char]
show (Model blk Concrete -> [(GenTx blk, TicketNo)]
forall {k} blk (r :: k). Model blk r -> [(GenTx blk, TicketNo)]
modelTxs Model blk Concrete
model', [GenTx blk]
-> [MempoolAddTxResult blk]
-> [(GenTx blk, MempoolAddTxResult blk)]
forall a b. [a] -> [b] -> [(a, b)]
zip [GenTx blk]
txs [MempoolAddTxResult blk]
res)) (Logic -> Logic) -> Logic -> Logic
forall a b. (a -> b) -> a -> b
$
          Bool -> Logic
Boolean (Bool -> Logic) -> Bool -> Logic
forall a b. (a -> b) -> a -> b
$
            [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
              [ GenTx blk
tx GenTx blk -> [GenTx blk] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((GenTx blk, TicketNo) -> GenTx blk)
-> [(GenTx blk, TicketNo)] -> [GenTx blk]
forall a b. (a -> b) -> [a] -> [b]
map (GenTx blk, TicketNo) -> GenTx blk
forall a b. (a, b) -> a
fst (Model blk Concrete -> [(GenTx blk, TicketNo)]
forall {k} blk (r :: k). Model blk r -> [(GenTx blk, TicketNo)]
modelTxs Model blk Concrete
model')
              | (GenTx blk
tx, MempoolAddTxResult blk
res') <- [GenTx blk]
-> [MempoolAddTxResult blk]
-> [(GenTx blk, MempoolAddTxResult blk)]
forall a b. [a] -> [b] -> [(a, b)]
zip [GenTx blk]
txs [MempoolAddTxResult blk]
res
              , case MempoolAddTxResult blk
res' of MempoolTxAdded{} -> Bool
True; MempoolAddTxResult blk
_ -> Bool
False
              ]
postcondition Model blk Concrete
model c :: Command blk Concrete
c@(Action Action blk Concrete
SyncLedger) r :: Response blk Concrete
r@(Synced (Point blk
_, [(GenTx blk, TicketNo)]
txs)) =
  let model' :: Model blk Concrete
model' = Model blk Concrete
-> Command blk Concrete
-> Response blk Concrete
-> Model blk Concrete
forall {k} blk (r :: k).
(Eq (TickedLedgerState blk ValuesMK), LedgerSupportsMempool blk,
 HasTxId (GenTx 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 Concrete
model Command blk Concrete
c Response blk Concrete
r
   in [Char] -> Logic -> Logic
Annotate [Char]
"Mismatch revalidating transactions in Sync" (Logic -> Logic) -> Logic -> Logic
forall a b. (a -> b) -> a -> b
$
        [Char] -> Logic -> Logic
Annotate (([(GenTx blk, TicketNo)], [(GenTx blk, TicketNo)]) -> [Char]
forall a. Show a => a -> [Char]
show (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)]
txs)) (Logic -> Logic) -> Logic -> Logic
forall a b. (a -> b) -> a -> b
$
          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
_ (Action (RemoveTxs [GenTxId blk]
ids)) =
  Action blk Symbolic -> Command blk Symbolic
forall {k} blk (r :: k). Action blk r -> Command blk r
Action (Action blk Symbolic -> Command blk Symbolic)
-> ([GenTxId blk] -> Action blk Symbolic)
-> [GenTxId blk]
-> Command blk Symbolic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenTxId blk] -> Action blk Symbolic
forall {k} blk (r :: k). [GenTxId blk] -> Action blk r
RemoveTxs ([GenTxId blk] -> Command blk Symbolic)
-> [[GenTxId blk]] -> [Command blk Symbolic]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([GenTxId blk] -> Bool) -> [[GenTxId blk]] -> [[GenTxId blk]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ([GenTxId blk] -> Bool) -> [GenTxId blk] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenTxId blk] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) ((GenTxId blk -> [GenTxId blk]) -> [GenTxId blk] -> [[GenTxId blk]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList GenTxId blk -> [GenTxId blk]
forall a. a -> [a]
shrinkNothing [GenTxId blk]
ids)
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 [Char]
-> 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 [Char]
trcr StrictTVar m (SUT m blk)
ior = StateMachine (Model blk) (Command blk) m (Response blk)
sm0{QC.semantics = \Command blk Concrete
c -> Tracer m [Char]
-> Command blk Concrete
-> StrictTVar m (SUT m blk)
-> m (Response blk Concrete)
forall blk (m :: * -> *).
(LedgerSupportsMempool blk, ValidateEnvelope blk, IOLike m) =>
Tracer m [Char]
-> Command blk Concrete
-> StrictTVar m (SUT m blk)
-> m (Response blk Concrete)
semantics Tracer m [Char]
trcr Command blk Concrete
c StrictTVar m (SUT m blk)
ior}

smUnused ::
  ( blk ~ TestBlock
  , 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, 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 (TickedLedgerState blk ValuesMK), LedgerSupportsMempool blk,
 HasTxId (GenTx 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), HasTxId (GenTx blk),
 UnTick blk, ValidateEnvelope blk, ToExpr (Command blk Concrete),
 ToExpr (GenTx blk), Show (TxIn blk), Show (TxOut 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), HasTxId (GenTx blk),
 UnTick blk, ValidateEnvelope blk, ToExpr (Command blk Concrete),
 ToExpr (GenTx blk), Show (TxIn blk), Show (TxOut 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), HasTxId (GenTx 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
  ) =>
  LedgerConfig blk ->
  TxMeasure blk ->
  -- | Initial state
  LedgerState blk ValuesMK ->
  -- | Transaction generator
  (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk]) ->
  Property
prop_mempoolSequential :: forall blk.
(HasTxId (GenTx blk), blk ~ TestBlock) =>
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 [Char])
-> PropertyM IO (SUT IO blk, Tracer IO [Char])
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (IO (SUT IO blk, Tracer IO [Char])
 -> PropertyM IO (SUT IO blk, Tracer IO [Char]))
-> IO (SUT IO blk, Tracer IO [Char])
-> PropertyM IO (SUT IO blk, Tracer IO [Char])
forall a b. (a -> b) -> a -> b
$ LedgerConfig blk
-> LedgerState blk ValuesMK -> IO (SUT IO blk, Tracer IO [Char])
forall (m :: * -> *) blk.
(NoThunks (MockedLedgerDB blk), IOLike m, MonadTimer m,
 LedgerSupportsProtocol blk, LedgerSupportsMempool blk,
 HasTxId (GenTx blk)) =>
LedgerConfig blk
-> LedgerState blk ValuesMK -> m (SUT m blk, Tracer m [Char])
mkSUT LedgerConfig blk
cfg LedgerState blk ValuesMK
initialState
          ior <- run $ newTVarIO sut
          let sm' = StateMachine (Model blk) (Command blk) IO (Response blk)
-> Tracer IO [Char]
-> 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 [Char]
-> 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 [Char]
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, 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 -> [Char]
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
      [Char]
"[" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> a -> [Char]
forall a. Show a => a -> [Char]
show a
l [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"-" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> a -> [Char]
forall a. Show a => a -> [Char]
show (a
l a -> a -> a
forall a. Num a => a -> a -> a
+ a
n) [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
")"

prop_mempoolParallel ::
  ( HasTxId (GenTx blk)
  , blk ~ TestBlock
  ) =>
  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) =>
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
10 ((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 [Char])
-> PropertyM IO (SUT IO blk, Tracer IO [Char])
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (IO (SUT IO blk, Tracer IO [Char])
 -> PropertyM IO (SUT IO blk, Tracer IO [Char]))
-> IO (SUT IO blk, Tracer IO [Char])
-> PropertyM IO (SUT IO blk, Tracer IO [Char])
forall a b. (a -> b) -> a -> b
$ LedgerConfig blk
-> LedgerState blk ValuesMK -> IO (SUT IO blk, Tracer IO [Char])
forall (m :: * -> *) blk.
(NoThunks (MockedLedgerDB blk), IOLike m, MonadTimer m,
 LedgerSupportsProtocol blk, LedgerSupportsMempool blk,
 HasTxId (GenTx blk)) =>
LedgerConfig blk
-> LedgerState blk ValuesMK -> m (SUT m blk, Tracer m [Char])
mkSUT LedgerConfig blk
cfg LedgerState blk ValuesMK
initialState
    ior <- run $ newTVarIO sut
    let sm' = StateMachine (Model blk) (Command blk) IO (Response blk)
-> Tracer IO [Char]
-> 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 [Char]
-> 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 [Char]
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, 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

-- | A regression test for one specific interleaving that random parallel
-- testing is very unlikely to hit, so we reproduce it deterministically: while a
-- mempool sync is in flight, the forge loop 'removeTxsEvenIfValid' drops a tx. A
-- sync snapshots the mempool, revalidates /off the lock/, then commits; if a
-- removal lands in that window a naive sync commits its now-stale snapshot and
-- /resurrects/ the removed tx.
--
-- This function interleaves 'semantics' and 'transition' in a very atypical way.
-- Normally one calls a QSM search function and it handles all of this, but the
-- point here is to reach the rare interleaving deterministically, so there is no
-- random search:
--
-- >        [X1]        -- TryAddTxs [x]
-- >         |
-- >        [X2]        -- ChangeLedger base1
-- >       /    \
-- >    [L1]    [R1]    -- L1: SyncLedger      R1: RemoveTxs [x]
-- >     |       |
-- >     |      [R2]    -- R2: SyncLedger
-- >       \    /
-- >        [X3]        -- GetSnapshot
--
-- Each node is an action this function performs:
--
--   * Each @X*@ is a 'step' (defined below): both a 'semantics' and a
--     'transition' call, so it mutates the SUT (the real mempool) /and/ advances
--     the model's pure state.
--   * @L1@ is only a 'semantics' call — it does not touch the model.
--   * @R1@ and @R2@ are only 'transition' calls — they do not touch the SUT.
--   * @X3@ is a final 'step', the 'GetSnapshot' query, so we can check the model
--     and the SUT still agree.
--
-- Crucially, @L1@ does /two/ things: its 'SyncLedger' /implicitly/ invokes
-- 'interposeRemoval'. So @L1@ does to the SUT exactly what @R1@+@R2@ do to the
-- model — but @L1@'s implicit 'RemoveTxs' is carefully arranged to happen
-- \"during\" @L1@'s explicit 'SyncLedger', i.e. inside the sync's off-lock read,
-- after its snapshot and before its commit. The tip change to @base1@ ('bumpTip')
-- keeps @x@ valid, so the only thing that can drop it is that removal — and a
-- correct sync must not bring it back.
prop_removeDuringSyncSM :: IO ()
prop_removeDuringSyncSM :: IO ()
prop_removeDuringSyncSM = do
  let cfg :: LedgerConfig TestBlock
cfg = LedgerConfig TestBlock
testLedgerConfigNoSizeLimits
      capacity :: TxMeasure TestBlock
capacity = TxMeasure TestBlock
txMaxBytes'
      base0 :: LedgerState TestBlock ValuesMK
base0 = LedgerState TestBlock ValuesMK
testInitLedger
      base1 :: LedgerState TestBlock ValuesMK
base1 = LedgerState TestBlock ValuesMK -> LedgerState TestBlock ValuesMK
bumpTip LedgerState TestBlock ValuesMK
base0

  (txs, _) <- Gen ([GenTx TestBlock], LedgerState TestBlock ValuesMK)
-> IO ([GenTx TestBlock], LedgerState TestBlock ValuesMK)
forall a. Gen a -> IO a
generate (Gen ([GenTx TestBlock], LedgerState TestBlock ValuesMK)
 -> IO ([GenTx TestBlock], LedgerState TestBlock ValuesMK))
-> Gen ([GenTx TestBlock], LedgerState TestBlock ValuesMK)
-> IO ([GenTx TestBlock], LedgerState TestBlock ValuesMK)
forall a b. (a -> b) -> a -> b
$ Int
-> LedgerState TestBlock ValuesMK
-> Gen ([GenTx TestBlock], LedgerState TestBlock ValuesMK)
genValidTxs Int
1 LedgerState TestBlock ValuesMK
base0
  assertBool "expected a valid tx" (not (null txs))
  let x = [GenTx TestBlock] -> GenTx TestBlock
forall a. HasCallStack => [a] -> a
head [GenTx TestBlock]
txs
      xid = GenTx TestBlock -> TxId (GenTx TestBlock)
forall tx. HasTxId tx => tx -> TxId tx
txId GenTx TestBlock
x

  -- Reference to the mempool, filled once it exists so the ledger interface can
  -- reach back into it to interpose the removal.
  mempoolRef <- newEmptyMVar
  removed <- newTVarIO False
  ldb <- newTVarIO $ MockedLedgerDB base0 Set.empty
  let interposeRemoval LedgerState TestBlock ValuesMK
st =
        -- Fire exactly once, and only in the sync's snapshot read: only the sync
        -- serves 'base1' (setup reads serve 'base0', and the removal's own read
        -- uses the stored 'base0' forker).
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (LedgerState TestBlock ValuesMK -> Point (LedgerState TestBlock)
forall (mk :: * -> * -> *).
LedgerState TestBlock mk -> Point (LedgerState TestBlock)
forall (l :: LedgerStateKind) (mk :: * -> * -> *).
GetTip l =>
l mk -> Point l
getTip LedgerState TestBlock ValuesMK
st Point (LedgerState TestBlock)
-> Point (LedgerState TestBlock) -> Bool
forall a. Eq a => a -> a -> Bool
== LedgerState TestBlock ValuesMK -> Point (LedgerState TestBlock)
forall (mk :: * -> * -> *).
LedgerState TestBlock mk -> Point (LedgerState TestBlock)
forall (l :: LedgerStateKind) (mk :: * -> * -> *).
GetTip l =>
l mk -> Point l
getTip LedgerState TestBlock ValuesMK
base1) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
          firstTime <- STM IO Bool -> IO Bool
forall a. HasCallStack => STM IO a -> IO a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM IO Bool -> IO Bool) -> STM IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ do
            done <- StrictTVar IO Bool -> STM IO Bool
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar IO Bool
removed
            writeTVar removed True
            pure (not done)
          when firstTime $ do
            mempool <- readMVar mempoolRef
            removeTxsEvenIfValid mempool (NE.fromList [xid])
      readTables LedgerState TestBlock ValuesMK
st LedgerTables TestBlock KeysMK
keys = do
        LedgerState TestBlock ValuesMK -> IO ()
interposeRemoval LedgerState TestBlock ValuesMK
st
        LedgerTables TestBlock ValuesMK
-> IO (LedgerTables TestBlock ValuesMK)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((forall k v.
 LedgerTableConstraints' blk k v =>
 ValuesMK k v -> KeysMK k v -> ValuesMK k v)
-> LedgerTables TestBlock ValuesMK
-> LedgerTables TestBlock KeysMK
-> LedgerTables TestBlock ValuesMK
forall l (mk1 :: * -> * -> *) (mk2 :: * -> * -> *)
       (mk3 :: * -> * -> *).
LedgerTableConstraints l =>
(forall k v.
 LedgerTableConstraints' blk k v =>
 mk1 k v -> mk2 k v -> mk3 k v)
-> LedgerTables l mk1 -> LedgerTables l mk2 -> LedgerTables l mk3
ltliftA2 ValuesMK k v -> KeysMK k v -> ValuesMK k v
forall k v. Ord k => ValuesMK k v -> KeysMK k v -> ValuesMK k v
forall k v.
LedgerTableConstraints' blk k v =>
ValuesMK k v -> KeysMK k v -> ValuesMK k v
restrictValuesMK (LedgerState TestBlock ValuesMK -> LedgerTables TestBlock ValuesMK
forall (mk :: * -> * -> *).
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
LedgerState TestBlock mk -> LedgerTables TestBlock mk
forall (l :: * -> LedgerStateKind) blk (mk :: * -> * -> *).
(HasLedgerTables l blk, CanMapMK mk, CanMapKeysMK mk,
 ZeroableMK mk) =>
l blk mk -> LedgerTables blk mk
projectLedgerTables LedgerState TestBlock ValuesMK
st) LedgerTables TestBlock KeysMK
keys)
      ledgerInterface =
        LedgerInterface
          { getCurrentLedgerState :: STM IO (MempoolLedgerDBView IO TestBlock)
getCurrentLedgerState = do
              st <- MockedLedgerDB TestBlock -> LedgerState TestBlock ValuesMK
forall blk. MockedLedgerDB blk -> LedgerState blk ValuesMK
ldbTip (MockedLedgerDB TestBlock -> LedgerState TestBlock ValuesMK)
-> STM (MockedLedgerDB TestBlock)
-> STM (LedgerState TestBlock ValuesMK)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictTVar IO (MockedLedgerDB TestBlock)
-> STM IO (MockedLedgerDB TestBlock)
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar IO (MockedLedgerDB TestBlock)
ldb
              pure $
                MempoolLedgerDBView
                  (forgetLedgerTables st)
                  ( pure $
                      Right $
                        ReadOnlyForker
                          { roforkerClose = pure ()
                          , roforkerReadStatistics = pure $ Statistics 0
                          , roforkerReadTables = readTables st
                          , roforkerRangeReadTables = const $ pure (emptyLedgerTables, Nothing)
                          , roforkerGetLedgerState = pure $ forgetLedgerTables st
                          }
                  )
          }
  mempool <-
    openMempoolWithoutSyncThread
      ledgerInterface
      cfg
      (MempoolCapacityBytesOverride $ unIgnoringOverflow $ tmPhase1 capacity)
      (Nothing :: Maybe MempoolTimeoutConfig)
      nullTracer
  putMVar mempoolRef mempool
  sutVar <- newTVarIO (SUT mempool ldb)

  let model0 = LedgerConfig TestBlock
-> TxMeasure TestBlock
-> LedgerState TestBlock ValuesMK
-> Model TestBlock r
forall {k} blk (r :: k).
(LedgerSupportsMempool blk, ValidateEnvelope blk) =>
LedgerConfig blk
-> TxMeasure blk -> LedgerState blk ValuesMK -> Model blk r
initModel LedgerConfig TestBlock
SimpleLedgerConfig
  SimpleMockCrypto (SimpleBftExt SimpleMockCrypto BftMockCrypto)
cfg TxMeasure TestBlock
capacity LedgerState TestBlock ValuesMK
base0
      -- Run one command through the state machine: execute it via 'semantics',
      -- check its 'postcondition' against the model, and return the model
      -- advanced by 'transition'.
      step Model TestBlock Concrete
model Command TestBlock Concrete
cmd = do
        resp <- Tracer IO [Char]
-> Command TestBlock Concrete
-> StrictTVar IO (SUT IO TestBlock)
-> IO (Response TestBlock Concrete)
forall blk (m :: * -> *).
(LedgerSupportsMempool blk, ValidateEnvelope blk, IOLike m) =>
Tracer m [Char]
-> Command blk Concrete
-> StrictTVar m (SUT m blk)
-> m (Response blk Concrete)
semantics Tracer IO [Char]
forall (m :: * -> *) a. Monad m => Tracer m a
nullTracer Command TestBlock Concrete
cmd StrictTVar IO (SUT IO TestBlock)
sutVar
        assertBool ("postcondition violated by " <> show cmd) $
          boolean (postcondition model cmd resp)
        pure (transition model cmd resp)

  -- X1, X2: add x, then move the ledger tip so the sync does real work without
  -- invalidating x ('ChangeLedger' goes through 'semantics', which writes the
  -- same mocked ledger db the interface reads).
  model1 <- step model0 (Action (TryAddTxs [x]))
  model2 <- step model1 (Event (ChangeLedger base1))

  -- L1: the sync runs to completion, and 'interposeRemoval' drops x during its
  -- off-lock read.
  syncResp <- semantics nullTracer (Action SyncLedger) sutVar

  -- R1, R2: mirror L1 on the model — remove, then sync, the only sensible
  -- linearization.
  let model3 = Model TestBlock Concrete
-> Command TestBlock Concrete
-> Response TestBlock Concrete
-> Model TestBlock Concrete
forall {k} blk (r :: k).
(Eq (TickedLedgerState blk ValuesMK), LedgerSupportsMempool blk,
 HasTxId (GenTx blk), ToExpr (GenTx blk), ValidateEnvelope blk,
 ToExpr (Command blk r)) =>
Model blk r -> Command blk r -> Response blk r -> Model blk r
transition Model TestBlock Concrete
model2 (Action TestBlock Concrete -> Command TestBlock Concrete
forall {k} blk (r :: k). Action blk r -> Command blk r
Action ([TxId (GenTx TestBlock)] -> Action TestBlock Concrete
forall {k} blk (r :: k). [GenTxId blk] -> Action blk r
RemoveTxs [TxId (GenTx TestBlock)
xid])) Response TestBlock Concrete
forall {k} blk (r :: k). Response blk r
Void
      model4 = Model TestBlock Concrete
-> Command TestBlock Concrete
-> Response TestBlock Concrete
-> Model TestBlock Concrete
forall {k} blk (r :: k).
(Eq (TickedLedgerState blk ValuesMK), LedgerSupportsMempool blk,
 HasTxId (GenTx blk), ToExpr (GenTx blk), ValidateEnvelope blk,
 ToExpr (Command blk r)) =>
Model blk r -> Command blk r -> Response blk r -> Model blk r
transition Model TestBlock Concrete
model3 (Action TestBlock Concrete -> Command TestBlock Concrete
forall {k} blk (r :: k). Action blk r -> Command blk r
Action Action TestBlock Concrete
forall {k} blk (r :: k). Action blk r
SyncLedger) Response TestBlock Concrete
syncResp

  -- X3: the snapshot must match the model, i.e. x is gone. Pre-fix the sync
  -- resurrects x and this 'postcondition' fails.
  _ <- step model4 (Action GetSnapshot)
  pure ()

-- | See 'MakeAtomic' on the reasoning behind having these tests.
tests :: TestTree
tests :: TestTree
tests =
  [Char] -> [TestTree] -> TestTree
testGroup
    [Char]
"QSM"
    [ [Char] -> IO () -> TestTree
testCase [Char]
"removal is not undone by a concurrent sync" IO ()
prop_removeDuringSyncSM
    , [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"sequential" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
QC.withNumTests 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) =>
LedgerConfig blk
-> TxMeasure blk
-> LedgerState blk ValuesMK
-> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
-> Property
prop_mempoolSequential LedgerConfig TestBlock
testLedgerConfigNoSizeLimits 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
    , [Char] -> [TestTree] -> TestTree
testGroup
        [Char]
"parallel"
        [ -- Restrict the length of the command list for QSM parallel testing.
          -- More commands require exponentially more memory to explore.
          QuickCheckMaxSize -> TestTree -> TestTree
forall v. IsOption v => v -> TestTree -> TestTree
localOption (Int -> QuickCheckMaxSize
QuickCheckMaxSize Int
40) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
            [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"atomic" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
              Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
QC.withNumTests 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) =>
LedgerConfig blk
-> TxMeasure blk
-> LedgerState blk ValuesMK
-> MakeAtomic
-> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
-> Property
prop_mempoolParallel LedgerConfig TestBlock
testLedgerConfigNoSizeLimits 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
        , [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"non atomic" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
            Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
QC.withNumTests 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) =>
LedgerConfig blk
-> TxMeasure blk
-> LedgerState blk ValuesMK
-> MakeAtomic
-> (Int -> LedgerState blk ValuesMK -> Gen [GenTx blk])
-> Property
prop_mempoolParallel LedgerConfig TestBlock
testLedgerConfigNoSizeLimits 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' :: TxMeasure TestBlock
txMaxBytes' :: TxMeasure TestBlock
txMaxBytes' = TxMeasurePhase1 TestBlock
-> TxMeasurePhase2 TestBlock -> TxMeasure TestBlock
forall blk.
TxMeasurePhase1 blk -> TxMeasurePhase2 blk -> TxMeasure blk
TxMeasure (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) TrivialTxMeasurePhase2
TxMeasurePhase2 TestBlock
TrivialTxMeasurePhase2

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 :: * -> * -> *).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: * -> * -> *).
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 :: * -> * -> *).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: * -> * -> *).
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 :: * -> * -> *).
UnTick blk =>
TickedLedgerState blk mk -> LedgerState blk mk
forall (mk :: * -> * -> *).
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 :: * -> * -> *).
LedgerState blk mk -> Point (LedgerState blk)
forall (l :: LedgerStateKind) (mk :: * -> * -> *).
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) -> [Char]
showTypeOf Proxy (Mempool IO TestBlock)
_ = Proxy (Mempool IO TestBlock) -> [Char]
forall a. NoThunks a => Proxy a -> [Char]
showTypeOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Mempool IO TestBlock))
  wNoThunks :: [[Char]] -> Mempool IO TestBlock -> IO (Maybe ThunkInfo)
wNoThunks [[Char]]
_ 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 =
    [Char] -> OMap [Char] Expr -> Expr
Rec [Char]
"Model" (OMap [Char] Expr -> Expr) -> OMap [Char] Expr -> Expr
forall a b. (a -> b) -> a -> b
$
      [([Char], Expr)] -> OMap [Char] Expr
forall k v. Ord k => [(k, v)] -> OMap k v
TD.fromList
        [ ([Char]
"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)
        , ([Char]
"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)
        , ([Char]
"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)
        , ([Char]
"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)
        , ([Char]
"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)
        , ([Char]
"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 -> [Char]
show = Expr -> [Char]
forall a. Show a => a -> [Char]
show (Expr -> [Char]) -> (Model blk r -> Expr) -> Model blk r -> [Char]
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) =
    [Char] -> [Expr] -> Expr
App [Char]
"TryAddTxs" ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$
      [ [Char] -> [Expr] -> Expr
App
          ( Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
take Int
8 ([Char] -> [Char]
forall a. HasCallStack => [a] -> [a]
tail ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
forall a. HasCallStack => [a] -> [a]
init ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ Hash SHA256 Tx -> [Char]
forall a. Show a => a -> [Char]
show Hash SHA256 Tx
txid)
              [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" "
              [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'"') ([([Char], Word)] -> [Char]
forall a. Show a => a -> [Char]
show [(Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
take Int
8 ([Char] -> [Char]
forall a. HasCallStack => [a] -> [a]
tail ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
forall a. HasCallStack => [a] -> [a]
init ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ Hash SHA256 Tx -> [Char]
forall a. Show a => a -> [Char]
show Hash SHA256 Tx
a), Word
b) | (Hash SHA256 Tx
a, Word
b) <- Set TxIn -> [TxIn]
forall a. Set a -> [a]
Set.toList Set TxIn
txins])
              [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" ->> "
              [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'"') ([([Char], Word)] -> [Char]
forall a. Show a => a -> [Char]
show [(Addr -> [Char]
forall a. Condense a => a -> [Char]
condense Addr
a, Word
b) | (TxIn
_, (Addr
a, Word
b)) <- Map TxIn TxOut -> [(TxIn, TxOut)]
forall k a. Map k a -> [(k, a)]
Map.toList Map TxIn TxOut
txouts])
              [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
""
          )
          []
      | SimpleGenTx Tx
tx Hash SHA256 Tx
txid <- [GenTx TestBlock]
txs
      , let txins :: Set TxIn
txins = Tx -> Set TxIn
forall a. HasMockTxs a => a -> Set TxIn
Mock.txIns Tx
tx
      , let txouts :: Map TxIn TxOut
txouts = Tx -> Map TxIn TxOut
forall a. HasMockTxs a => a -> Map TxIn TxOut
Mock.txOuts Tx
tx
      ]
  toExpr Action TestBlock r
SyncLedger = [Char] -> [Expr] -> Expr
App [Char]
"SyncLedger" []
  toExpr Action TestBlock r
GetSnapshot = [Char] -> [Expr] -> Expr
App [Char]
"GetSnapshot" []
  toExpr (RemoveTxs [TxId (GenTx TestBlock)]
ids) =
    [Char] -> [Expr] -> Expr
App [Char]
"RemoveTxs" [[Char] -> [Expr] -> Expr
App (Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
take Int
8 ([Char] -> [Char]
forall a. HasCallStack => [a] -> [a]
tail ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
forall a. HasCallStack => [a] -> [a]
init ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ TxId (GenTx TestBlock) -> [Char]
forall a. Show a => a -> [Char]
show TxId (GenTx TestBlock)
i)) [] | TxId (GenTx TestBlock)
i <- [TxId (GenTx TestBlock)]
ids]

instance ToExpr (LedgerState blk ValuesMK) => ToExpr (Event blk r) where
  toExpr :: Event blk r -> Expr
toExpr (ChangeLedger LedgerState blk ValuesMK
ls) =
    [Char] -> [Expr] -> Expr
App [Char]
"ChangeLedger" [LedgerState blk ValuesMK -> Expr
forall a. ToExpr a => a -> Expr
toExpr LedgerState blk ValuesMK
ls]

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 -> [Char]
show =
    -- unwords . take 2 . words .
    Expr -> [Char]
forall a. Show a => a -> [Char]
show (Expr -> [Char])
-> (Command blk r -> Expr) -> Command blk r -> [Char]
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 = [Char] -> [Expr] -> Expr
App [Char]
"Void" []
  toExpr (GotSnapshot [(GenTx blk, TicketNo)]
s) =
    [Char] -> [Expr] -> Expr
App
      [Char]
"GotSnapshot"
      [[Expr] -> Expr
Lst [[(GenTx blk, TicketNo)] -> Expr
forall a. ToExpr a => a -> Expr
toExpr [(GenTx blk, TicketNo)]
s]]
  toExpr (AddResult [MempoolAddTxResult blk]
res) =
    [Char] -> [Expr] -> Expr
App [Char]
"AddResult" ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$
      [ [Expr] -> Expr
Lst ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$
          (MempoolAddTxResult blk -> Expr)
-> [MempoolAddTxResult blk] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map
            ( (([Char] -> [Expr] -> Expr) -> [Expr] -> [Char] -> Expr
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Char] -> [Expr] -> Expr
App []) ([Char] -> Expr)
-> (MempoolAddTxResult blk -> [Char])
-> MempoolAddTxResult blk
-> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
                MempoolTxAdded{} -> [Char]
"OK"
                MempoolTxRejected{} -> [Char]
"NO"
            )
            [MempoolAddTxResult blk]
res
      ]
  toExpr (Synced (Point blk, [(GenTx blk, TicketNo)])
res) =
    [Char] -> [Expr] -> Expr
App [Char]
"Synced" [[Char] -> [Expr] -> Expr
App ((Point blk, [(GenTx blk, TicketNo)]) -> [Char]
forall a. Show a => a -> [Char]
show (Point blk, [(GenTx blk, TicketNo)])
res) []]

instance
  ( ToExpr (GenTx blk)
  , LedgerSupportsMempool blk
  ) =>
  Show (Response blk r)
  where
  show :: Response blk r -> [Char]
show =
    -- unwords . take 2 . words .
    Expr -> [Char]
forall a. Show a => a -> [Char]
show (Expr -> [Char])
-> (Response blk r -> Expr) -> Response blk r -> [Char]
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
_ -> [Char] -> Gen (LedgerState TestBlock ValuesMK)
forall a. HasCallStack => [Char] -> a
error [Char]
"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) = [Char] -> [Expr] -> Expr
App [Char]
"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 TestBlock ValuesMK
tbs) =
    [Char] -> [Expr] -> Expr
App [Char]
"LedgerState" ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$
      [ [Expr] -> Expr
Lst
          [ (WithOrigin SlotNo, ChainHash TestBlock) -> Expr
forall a. ToExpr a => a -> Expr
toExpr (Point TestBlock -> WithOrigin SlotNo
forall {k} (block :: k). Point block -> WithOrigin SlotNo
pointSlot (Point TestBlock -> WithOrigin SlotNo)
-> Point TestBlock -> WithOrigin SlotNo
forall a b. (a -> b) -> a -> b
$ MockState TestBlock -> Point TestBlock
forall blk. MockState blk -> Point blk
mockTip MockState TestBlock
st, Point TestBlock -> ChainHash TestBlock
forall {k} (block :: k). Point block -> ChainHash block
pointHash (Point TestBlock -> ChainHash TestBlock)
-> Point TestBlock -> ChainHash TestBlock
forall a b. (a -> b) -> a -> b
$ MockState TestBlock -> Point TestBlock
forall blk. MockState blk -> Point blk
mockTip MockState TestBlock
st)
          , LedgerTables TestBlock ValuesMK -> Expr
forall a. ToExpr a => a -> Expr
toExpr LedgerTables TestBlock ValuesMK
tbs
          ]
      ]

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

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

instance ToExpr (LedgerTables TestBlock ValuesMK) where
  toExpr :: LedgerTables TestBlock ValuesMK -> Expr
toExpr (LedgerTables (ValuesMK Map (TxIn TestBlock) (TxOut TestBlock)
v)) = [Expr] -> Expr
Lst [([Char], [Char]) -> Expr
forall a. ToExpr a => a -> Expr
toExpr (TxIn -> [Char]
forall a. Condense a => a -> [Char]
condense TxIn
txin, TxOut -> [Char]
forall a. Condense a => a -> [Char]
condense TxOut
txout) | (TxIn
txin, TxOut
txout) <- Map TxIn TxOut -> [(TxIn, TxOut)]
forall k a. Map k a -> [(k, a)]
Map.toList Map TxIn TxOut
Map (TxIn TestBlock) (TxOut TestBlock)
v]

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

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

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