{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE DeriveAnyClass           #-}
{-# LANGUAGE DeriveGeneric            #-}
{-# LANGUAGE EmptyCase                #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE LambdaCase               #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE StandaloneDeriving       #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies             #-}

-- | The type of the local transaction monitoring protocol.
--
-- This is used by local clients (like wallets, explorers and CLI tools) to
-- monitor the transactions passing through the mempool of a local node.
--
-- The protocol is stateful such that the server keeps track of the transactions
-- already sent to the client.
--
-- @
--                    START
--                      ⇓
--                    ┌───────────────┐
--            ┌──────▶│     Idle      │⇒ DONE
--            │       └───┬───────────┘
--            │           │
--            │   Acquire │
--            │           ▼
--            │       ┌───────────────┐
--    Release │       │   Acquiring   │
--            │       └───┬───────────┘
--            │           │       ▲
--            │  Acquired │       │ AwaitAcquire
--            │           ▼       │
--            │       ┌───────────┴───┐
--            └───────┤   Acquired    │
--                    └───┬───────────┘
--                        │       ▲
--  HasTx|NextTx|GetSizes │       │ Reply (HasTx|NextTx|GetSizes)
--                        ▼       │
--                    ┌───────────┴───┐
--                    │      Busy     │
--                    └───────────────┘
-- @
module Ouroboros.Network.Protocol.LocalTxMonitor.Type where


import Data.Kind
import Data.Singletons
import Data.Word
import GHC.Generics (Generic)

import Control.DeepSeq
import Network.TypedProtocol.Core
import Ouroboros.Network.Util.ShowProxy


-- | The kind of the local transaction monitoring protocol, and the types of
-- the states in the protocol state machine.
--
-- It is parametrised over the type of transactions.
--
data LocalTxMonitor txid tx slot where

  -- | The client has agency; it can request a transaction or terminate.
  --
  -- There is no timeout in this state.
  --
  StIdle   :: LocalTxMonitor txid tx slot

  -- | The server has agency; it is capturing the latest mempool snapshot.
  --
  StAcquiring :: LocalTxMonitor txid tx slot

  -- | The client has agency; The server is locked on a particular mempool
  -- snapshot. The client can now perform various requests on that snapshot,
  -- or acquire a new one, more recent.
  --
  StAcquired  :: LocalTxMonitor txid tx slot

  -- | The server has agency; It must respond, there's no timeout.
  --
  StBusy :: StBusyKind -> LocalTxMonitor txid tx slot

  -- | Nobody has agency. The terminal state.
  --
  StDone   :: LocalTxMonitor txid tx slot


instance
    ( ShowProxy txid
    , ShowProxy tx
    , ShowProxy slot
    ) =>
    ShowProxy (LocalTxMonitor txid tx slot)
  where
    showProxy :: Proxy (LocalTxMonitor txid tx slot) -> String
showProxy Proxy (LocalTxMonitor txid tx slot)
_ = [String] -> String
unwords
      [ String
"LocalTxMonitor"
      , Proxy txid -> String
forall {k} (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy txid
forall {k} (t :: k). Proxy t
Proxy :: Proxy txid)
      , Proxy tx -> String
forall {k} (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy tx
forall {k} (t :: k). Proxy t
Proxy :: Proxy tx)
      , Proxy slot -> String
forall {k} (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy slot
forall {k} (t :: k). Proxy t
Proxy :: Proxy slot)
      ]

type SingLocalTxMonitor :: LocalTxMonitor txid tx slot -> Type
data SingLocalTxMonitor st where
    SingIdle      :: SingLocalTxMonitor StIdle
    SingAcquiring :: SingLocalTxMonitor StAcquiring
    SingAcquired  :: SingLocalTxMonitor StAcquired
    SingBusy      :: SingBusyKind k
                  -> SingLocalTxMonitor (StBusy k)
    SingDone      :: SingLocalTxMonitor StDone

instance StateTokenI StIdle      where stateToken :: StateToken 'StIdle
stateToken = StateToken 'StIdle
SingLocalTxMonitor 'StIdle
forall {k} {k} {k} {txid :: k} {tx :: k} {slot :: k}.
SingLocalTxMonitor 'StIdle
SingIdle
instance StateTokenI StAcquiring where stateToken :: StateToken 'StAcquiring
stateToken = StateToken 'StAcquiring
SingLocalTxMonitor 'StAcquiring
forall {k} {k} {k} {txid :: k} {tx :: k} {slot :: k}.
SingLocalTxMonitor 'StAcquiring
SingAcquiring
instance StateTokenI StAcquired  where stateToken :: StateToken 'StAcquired
stateToken = StateToken 'StAcquired
SingLocalTxMonitor 'StAcquired
forall {k} {k} {k} {txid :: k} {tx :: k} {slot :: k}.
SingLocalTxMonitor 'StAcquired
SingAcquired
instance SingI k =>
         StateTokenI (StBusy k)  where stateToken :: StateToken ('StBusy k)
stateToken = SingBusyKind k -> SingLocalTxMonitor ('StBusy k)
forall {k} {k} {k} {txid :: k} {tx :: k} {slot :: k}
       (k :: StBusyKind).
SingBusyKind k -> SingLocalTxMonitor ('StBusy k)
SingBusy (Sing k
forall {k} (a :: k). SingI a => Sing a
sing :: Sing k)
instance StateTokenI StDone      where stateToken :: StateToken 'StDone
stateToken = StateToken 'StDone
SingLocalTxMonitor 'StDone
forall {k} {k} {k} {txid :: k} {tx :: k} {slot :: k}.
SingLocalTxMonitor 'StDone
SingDone

deriving instance Show (SingLocalTxMonitor st)


data StBusyKind where
  -- | The server is busy fetching the next transaction from the mempool
  NextTx :: StBusyKind
  -- | The server is busy looking for the presence of a specific transaction in
  -- the mempool
  HasTx :: StBusyKind
  -- | The server is busy looking for the current size and max capacity of the
  -- mempool
  GetSizes :: StBusyKind

type SingBusyKind :: StBusyKind -> Type
data SingBusyKind st where
    SingNextTx   :: SingBusyKind NextTx
    SingHasTx    :: SingBusyKind HasTx
    SingGetSizes :: SingBusyKind GetSizes

type instance Sing = SingBusyKind
instance SingI NextTx   where sing :: Sing 'NextTx
sing = Sing 'NextTx
SingBusyKind 'NextTx
SingNextTx
instance SingI HasTx    where sing :: Sing 'HasTx
sing = Sing 'HasTx
SingBusyKind 'HasTx
SingHasTx
instance SingI GetSizes where sing :: Sing 'GetSizes
sing = Sing 'GetSizes
SingBusyKind 'GetSizes
SingGetSizes

deriving instance Show (SingBusyKind st)

-- | Describes the MemPool sizes and capacity for a given snapshot.
data MempoolSizeAndCapacity = MempoolSizeAndCapacity
  { MempoolSizeAndCapacity -> Word32
capacityInBytes :: !Word32
    -- ^ The maximum capacity of the mempool. Note that this may dynamically
    -- change when the ledger state is updated.
  , MempoolSizeAndCapacity -> Word32
sizeInBytes     :: !Word32
    -- ^ The summed byte size of all the transactions in the mempool.
  , MempoolSizeAndCapacity -> Word32
numberOfTxs     :: !Word32
    -- ^ The number of transactions in the mempool
  } deriving ((forall x. MempoolSizeAndCapacity -> Rep MempoolSizeAndCapacity x)
-> (forall x.
    Rep MempoolSizeAndCapacity x -> MempoolSizeAndCapacity)
-> Generic MempoolSizeAndCapacity
forall x. Rep MempoolSizeAndCapacity x -> MempoolSizeAndCapacity
forall x. MempoolSizeAndCapacity -> Rep MempoolSizeAndCapacity x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MempoolSizeAndCapacity -> Rep MempoolSizeAndCapacity x
from :: forall x. MempoolSizeAndCapacity -> Rep MempoolSizeAndCapacity x
$cto :: forall x. Rep MempoolSizeAndCapacity x -> MempoolSizeAndCapacity
to :: forall x. Rep MempoolSizeAndCapacity x -> MempoolSizeAndCapacity
Generic, MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool
(MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool)
-> (MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool)
-> Eq MempoolSizeAndCapacity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool
== :: MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool
$c/= :: MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool
/= :: MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool
Eq, Int -> MempoolSizeAndCapacity -> ShowS
[MempoolSizeAndCapacity] -> ShowS
MempoolSizeAndCapacity -> String
(Int -> MempoolSizeAndCapacity -> ShowS)
-> (MempoolSizeAndCapacity -> String)
-> ([MempoolSizeAndCapacity] -> ShowS)
-> Show MempoolSizeAndCapacity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MempoolSizeAndCapacity -> ShowS
showsPrec :: Int -> MempoolSizeAndCapacity -> ShowS
$cshow :: MempoolSizeAndCapacity -> String
show :: MempoolSizeAndCapacity -> String
$cshowList :: [MempoolSizeAndCapacity] -> ShowS
showList :: [MempoolSizeAndCapacity] -> ShowS
Show, MempoolSizeAndCapacity -> ()
(MempoolSizeAndCapacity -> ()) -> NFData MempoolSizeAndCapacity
forall a. (a -> ()) -> NFData a
$crnf :: MempoolSizeAndCapacity -> ()
rnf :: MempoolSizeAndCapacity -> ()
NFData)

instance Protocol (LocalTxMonitor txid tx slot) where

  -- | The messages in the transaction monitoring protocol.
  --
  -- There is no guarantee or requirement that every transaction that enters
  -- the mempool be sent, it need only be in the mempool at the time. So this
  -- protocol can be used to monitor what is in the mempool but it cannot
  -- guarantee to return everything that ever passed though the mempool. In
  -- particular if the client is too slow then txs can be removed from the
  -- mempool before the client requests them. This is reasonable semantics
  -- since it is observationally equivalent to what can happen anyway: we can
  -- \"miss\" a transaction even before the transaction makes it into the
  -- node's mempool (since it can be removed from the mempool of a peer and
  -- then not forwarded).
  --
  data Message (LocalTxMonitor txid tx slot) from to where

    -- | Acquire the latest snapshot. This enables subsequent queries to be
    -- made against a consistent view of the mempool.
    --
    -- There is no timeout.
    --
    MsgAcquire
      :: Message (LocalTxMonitor txid tx slot) StIdle StAcquiring

    -- | The server is now locked to a particular snapshot. It returns the
    -- slot number of the 'virtual block' under construction.
    --
    MsgAcquired
      :: slot
      -> Message (LocalTxMonitor txid tx slot) StAcquiring StAcquired

    -- | Like 'MsgAcquire' but await for a new snapshot different from the one
    -- currently acquired.
    --
    -- There is no timeout; the caller will block until a new snapshot is
    -- available.
    --
    MsgAwaitAcquire
      :: Message (LocalTxMonitor txid tx slot) StAcquired StAcquiring

    -- | The client requests a single transaction and waits a reply.
    --
    MsgNextTx
      :: Message (LocalTxMonitor txid tx slot) StAcquired (StBusy NextTx)

    -- | The server responds with a single transaction. This must be a
    -- transaction that was not previously sent to the client for this
    -- particular snapshot.
    --
    MsgReplyNextTx
      :: Maybe tx
      -> Message (LocalTxMonitor txid tx slot) (StBusy NextTx) StAcquired

    -- | The client checks whether the server knows of a particular transaction
    -- identified by its id.
    --
    MsgHasTx
      :: txid
      -> Message (LocalTxMonitor txid tx slot) StAcquired (StBusy HasTx)

    -- | The server responds 'True' when the given tx is present in the snapshot,
    -- False otherwise.
    --
    MsgReplyHasTx
      :: Bool
      -> Message (LocalTxMonitor txid tx slot) (StBusy HasTx) StAcquired

    -- | The client asks the server about the mempool current size and max
    -- capacity.
    --
    MsgGetSizes
      :: Message (LocalTxMonitor txid tx slot) StAcquired (StBusy GetSizes)

    -- | The server responds with the mempool size and max capacity.
    --
    MsgReplyGetSizes
      :: MempoolSizeAndCapacity
      -> Message (LocalTxMonitor txid tx slot) (StBusy GetSizes) StAcquired

    -- | Release the acquired snapshot, in order to loop back to the idle state.
    --
    MsgRelease
      :: Message (LocalTxMonitor txid tx slot) StAcquired StIdle

    -- | The client can terminate the protocol.
    --
    MsgDone
      :: Message (LocalTxMonitor txid tx slot) StIdle StDone

  type StateAgency StIdle      = ClientAgency
  type StateAgency StAcquiring = ServerAgency
  type StateAgency StAcquired  = ClientAgency
  type StateAgency (StBusy _)  = ServerAgency
  type StateAgency StDone      = NobodyAgency

  type StateToken = SingLocalTxMonitor


instance ( NFData txid
         , NFData tx
         , NFData slot
         ) => NFData (Message (LocalTxMonitor txid tx slot) from to) where
  rnf :: Message (LocalTxMonitor txid tx slot) from to -> ()
rnf Message (LocalTxMonitor txid tx slot) from to
R:MessageLocalTxMonitorfromto (*) (*) (*) txid tx slot from to
MsgAcquire             = ()
  rnf (MsgAcquired slot
slot)     = slot -> ()
forall a. NFData a => a -> ()
rnf slot
slot
  rnf Message (LocalTxMonitor txid tx slot) from to
R:MessageLocalTxMonitorfromto (*) (*) (*) txid tx slot from to
MsgAwaitAcquire        = ()
  rnf Message (LocalTxMonitor txid tx slot) from to
R:MessageLocalTxMonitorfromto (*) (*) (*) txid tx slot from to
MsgNextTx              = ()
  rnf (MsgReplyNextTx Maybe tx
mbTx)  = Maybe tx -> ()
forall a. NFData a => a -> ()
rnf Maybe tx
mbTx
  rnf (MsgHasTx txid
txid)        = txid -> ()
forall a. NFData a => a -> ()
rnf txid
txid
  rnf (MsgReplyHasTx Bool
b)      = Bool -> ()
forall a. NFData a => a -> ()
rnf Bool
b
  rnf Message (LocalTxMonitor txid tx slot) from to
R:MessageLocalTxMonitorfromto (*) (*) (*) txid tx slot from to
MsgGetSizes            = ()
  rnf (MsgReplyGetSizes MempoolSizeAndCapacity
msc) = MempoolSizeAndCapacity -> ()
forall a. NFData a => a -> ()
rnf MempoolSizeAndCapacity
msc
  rnf Message (LocalTxMonitor txid tx slot) from to
R:MessageLocalTxMonitorfromto (*) (*) (*) txid tx slot from to
MsgRelease             = ()
  rnf Message (LocalTxMonitor txid tx slot) from to
R:MessageLocalTxMonitorfromto (*) (*) (*) txid tx slot from to
MsgDone                = ()

data TokBusyKind (k :: StBusyKind) where
  TokNextTx   :: TokBusyKind NextTx
  TokHasTx    :: TokBusyKind HasTx
  TokGetSizes :: TokBusyKind GetSizes

instance NFData (TokBusyKind k) where
  rnf :: TokBusyKind k -> ()
rnf TokBusyKind k
TokNextTx   = ()
  rnf TokBusyKind k
TokHasTx    = ()
  rnf TokBusyKind k
TokGetSizes = ()

deriving instance (Show txid, Show tx, Show slot)
  => Show (Message (LocalTxMonitor txid tx slot) from to)