{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE EmptyCase           #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# 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.Word
import           GHC.Generics (Generic)

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)
      ]

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

-- | 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
$cto :: forall x. Rep MempoolSizeAndCapacity x -> MempoolSizeAndCapacity
$cfrom :: forall x. MempoolSizeAndCapacity -> Rep MempoolSizeAndCapacity x
Generic, MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool
(MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool)
-> (MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool)
-> Eq MempoolSizeAndCapacity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool
$c/= :: MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool
== :: MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool
$c== :: 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
showList :: [MempoolSizeAndCapacity] -> ShowS
$cshowList :: [MempoolSizeAndCapacity] -> ShowS
show :: MempoolSizeAndCapacity -> String
$cshow :: MempoolSizeAndCapacity -> String
showsPrec :: Int -> MempoolSizeAndCapacity -> ShowS
$cshowsPrec :: Int -> MempoolSizeAndCapacity -> ShowS
Show)

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

  data ClientHasAgency st where
    TokIdle     :: ClientHasAgency StIdle
    TokAcquired :: ClientHasAgency StAcquired

  data ServerHasAgency st where
    TokAcquiring :: ServerHasAgency StAcquiring
    TokBusy      :: TokBusyKind k -> ServerHasAgency (StBusy k)

  data NobodyHasAgency st where
    TokDone  :: NobodyHasAgency StDone

  exclusionLemma_ClientAndServerHaveAgency :: ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st
TokIdle ServerHasAgency st
tok = case ServerHasAgency st
tok of {}

  exclusionLemma_NobodyAndClientHaveAgency :: NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st
TokDone ClientHasAgency st
tok = case ClientHasAgency st
tok of {}

  exclusionLemma_NobodyAndServerHaveAgency :: NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st
TokDone ServerHasAgency st
tok = case ServerHasAgency st
tok of {}

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

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

instance Show (ClientHasAgency (st :: LocalTxMonitor txid tx slot)) where
  show :: ClientHasAgency st -> String
show = \case
    ClientHasAgency st
TokIdle     -> String
"TokIdle"
    ClientHasAgency st
TokAcquired -> String
"TokAcquired"

instance Show (ServerHasAgency (st :: LocalTxMonitor txid tx slot)) where
  show :: ServerHasAgency st -> String
show = \case
    ServerHasAgency st
TokAcquiring        -> String
"TokAcquiring"
    TokBusy TokNextTx   -> String
"TokBusy TokNextTx"
    TokBusy TokHasTx    -> String
"TokBusy TokHasTx"
    TokBusy TokGetSizes -> String
"TokBusy TokGetSizes"