Skip to content
Permalink
Browse files

Merge #513

513: PeerRole symmetry in typed-protocols r=coot a=coot



Co-authored-by: Marcin Szamotulski <profunctor@pm.me>
  • Loading branch information...
iohk-bors and coot committed May 15, 2019
2 parents fabb7e2 + 4814148 commit ec12f2d9a688a69cd730544fa45bc138fd3a1677
@@ -23,6 +23,7 @@ module Network.TypedProtocol.Core (
-- * Engaging in protocols
-- $using
PeerRole(..),
FlipAgency,
PeerHasAgency(..),
WeHaveAgency,
TheyHaveAgency,
@@ -298,8 +298,8 @@ runConnectedPeers :: (MonadSTM m, MonadAsync m, MonadCatch m,
=> m (Channel m bytes, Channel m bytes)
-> Tracer m (TraceSendRecv ps)
-> Codec ps failure m bytes
-> Peer ps AsClient st m a
-> Peer ps AsServer st m b
-> Peer ps pr st m a
-> Peer ps (FlipAgency pr) st m b
-> m (a, b)
runConnectedPeers createChannels tr codec client server =
createChannels >>= \(clientChannel, serverChannel) ->
@@ -315,8 +315,8 @@ runConnectedPeersPipelined :: (MonadSTM m, MonadAsync m, MonadCatch m,
-> Tracer m (TraceSendRecv ps)
-> Codec ps failure m bytes
-> Natural
-> PeerPipelined ps AsClient st m a
-> Peer ps AsServer st m b
-> PeerPipelined ps pr st m a
-> Peer ps (FlipAgency pr) st m b
-> m (a, b)
runConnectedPeersPipelined createChannels tr codec maxOutstanding client server =
createChannels >>= \(clientChannel, serverChannel) ->
@@ -79,16 +79,16 @@ import Data.Void (absurd)
-- * It is useful for testing peer implementations against each other in a
-- minimalistic setting.
--
connect :: forall ps (st :: ps) m a b.
connect :: forall ps (pr :: PeerRole) (st :: ps) m a b.
(Monad m, Protocol ps)
=> Peer ps AsClient st m a
-> Peer ps AsServer st m b
=> Peer ps pr st m a
-> Peer ps (FlipAgency pr) st m b
-> m (a, b, TerminalStates ps)
connect = go
where
go :: forall (st' :: ps).
Peer ps AsClient st' m a
-> Peer ps AsServer st' m b
Peer ps pr st' m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
go (Done stA a) (Done stB b) = return (a, b, TerminalStates stA stB)
go (Effect a ) b = a >>= \a' -> go a' b
@@ -101,21 +101,39 @@ connect = go
go (Yield (ClientAgency stA) _ _) (Yield (ServerAgency stB) _ _) =
absurd (exclusionLemma_ClientAndServerHaveAgency stA stB)

go (Yield (ServerAgency stA) _ _) (Yield (ClientAgency stB) _ _) =
absurd (exclusionLemma_ClientAndServerHaveAgency stB stA)

go (Await (ServerAgency stA) _) (Await (ClientAgency stB) _) =
absurd (exclusionLemma_ClientAndServerHaveAgency stB stA)

go (Await (ClientAgency stA) _) (Await (ServerAgency stB) _) =
absurd (exclusionLemma_ClientAndServerHaveAgency stA stB)

go (Done stA _) (Yield (ServerAgency stB) _ _) =
absurd (exclusionLemma_NobodyAndServerHaveAgency stA stB)

go (Done stA _) (Yield (ClientAgency stB) _ _) =
absurd (exclusionLemma_NobodyAndClientHaveAgency stA stB)

go (Done stA _) (Await (ClientAgency stB) _) =
absurd (exclusionLemma_NobodyAndClientHaveAgency stA stB)

go (Done stA _) (Await (ServerAgency stB) _) =
absurd (exclusionLemma_NobodyAndServerHaveAgency stA stB)

go (Yield (ClientAgency stA) _ _) (Done stB _) =
absurd (exclusionLemma_NobodyAndClientHaveAgency stB stA)

go (Yield (ServerAgency stA) _ _) (Done stB _) =
absurd (exclusionLemma_NobodyAndServerHaveAgency stB stA)

go (Await (ServerAgency stA) _) (Done stB _) =
absurd (exclusionLemma_NobodyAndServerHaveAgency stB stA)

go (Await (ClientAgency stA) _) (Done stB _) =
absurd (exclusionLemma_NobodyAndClientHaveAgency stB stA)


-- | The terminal states for the protocol. Used in 'connect' and
-- 'connectPipelined' to return the states in which the peers terminated.
@@ -137,11 +155,11 @@ data TerminalStates ps where
--
-- This can be exercised using a QuickCheck style generator.
--
connectPipelined :: forall ps (st :: ps) m a b.
connectPipelined :: forall ps (pr :: PeerRole) (st :: ps) m a b.
(Monad m, Protocol ps)
=> [Bool] -- ^ Interleaving choices. [] gives no pipelining.
-> PeerPipelined ps AsClient st m a
-> Peer ps AsServer st m b
-> PeerPipelined ps pr st m a
-> Peer ps (FlipAgency pr) st m b
-> m (a, b, TerminalStates ps)

connectPipelined cs0 (PeerPipelined peerA) peerB =
@@ -150,8 +168,8 @@ connectPipelined cs0 (PeerPipelined peerA) peerB =
goSender :: forall (st' :: ps) n c.
[Bool]
-> Queue n c
-> PeerSender ps AsClient st' n c m a
-> Peer ps AsServer st' m b
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)

goSender _ EmptyQ (SenderDone stA a) (Done stB b) = return (a, b, terminals)
@@ -181,26 +199,44 @@ connectPipelined cs0 (PeerPipelined peerA) peerB =
goSender _ _ (SenderDone stA _) (Yield (ServerAgency stB) _ _) =
absurd (exclusionLemma_NobodyAndServerHaveAgency stA stB)

goSender _ _ (SenderDone stA _) (Yield (ClientAgency stB) _ _) =
absurd (exclusionLemma_NobodyAndClientHaveAgency stA stB)

goSender _ _ (SenderDone stA _) (Await (ClientAgency stB) _) =
absurd (exclusionLemma_NobodyAndClientHaveAgency stA stB)

goSender _ _ (SenderDone stA _) (Await (ServerAgency stB) _) =
absurd (exclusionLemma_NobodyAndServerHaveAgency stA stB)

goSender _ _ (SenderYield (ClientAgency stA) _ _) (Done stB _) =
absurd (exclusionLemma_NobodyAndClientHaveAgency stB stA)

goSender _ _ (SenderYield (ServerAgency stA) _ _) (Done stB _) =
absurd (exclusionLemma_NobodyAndServerHaveAgency stB stA)

goSender _ _ (SenderYield (ClientAgency stA) _ _) (Yield (ServerAgency stB) _ _) =
absurd (exclusionLemma_ClientAndServerHaveAgency stA stB)

goSender _ _ (SenderYield (ServerAgency stA) _ _) (Yield (ClientAgency stB) _ _) =
absurd (exclusionLemma_ClientAndServerHaveAgency stB stA)

goSender _ _ (SenderPipeline (ClientAgency stA) _ _ _) (Done stB _) =
absurd (exclusionLemma_NobodyAndClientHaveAgency stB stA)

goSender _ _ (SenderPipeline (ServerAgency stA) _ _ _) (Done stB _) =
absurd (exclusionLemma_NobodyAndServerHaveAgency stB stA)

goSender _ _ (SenderPipeline (ClientAgency stA) _ _ _) (Yield (ServerAgency stB) _ _) =
absurd (exclusionLemma_ClientAndServerHaveAgency stA stB)

goSender _ _ (SenderPipeline (ServerAgency stA) _ _ _) (Yield (ClientAgency stB) _ _) =
absurd (exclusionLemma_ClientAndServerHaveAgency stB stA)


goReceiver :: forall (st' :: ps) (stdone :: ps) c.
PeerReceiver ps AsClient st' stdone m c
-> Peer ps AsServer st' m b
-> m (Peer ps AsServer stdone m b, c)
PeerReceiver ps pr st' stdone m c
-> Peer ps (FlipAgency pr) st' m b
-> m (Peer ps (FlipAgency pr) stdone m b, c)

goReceiver (ReceiverDone x) b = return (b, x)
goReceiver (ReceiverEffect a) b = a >>= \a' -> goReceiver a' b
@@ -213,9 +249,15 @@ connectPipelined cs0 (PeerPipelined peerA) peerB =
goReceiver (ReceiverAwait (ServerAgency stA) _) (Done stB _) =
absurd (exclusionLemma_NobodyAndServerHaveAgency stB stA)

goReceiver (ReceiverAwait (ClientAgency stA) _) (Done stB _) =
absurd (exclusionLemma_NobodyAndClientHaveAgency stB stA)

goReceiver (ReceiverAwait (ServerAgency stA) _) (Await (ClientAgency stB) _) =
absurd (exclusionLemma_ClientAndServerHaveAgency stB stA)

goReceiver (ReceiverAwait (ClientAgency stA) _) (Await (ServerAgency stB) _) =
absurd (exclusionLemma_ClientAndServerHaveAgency stA stB)


-- | Prove that we have a total conversion from pipelined peers to regular
-- peers. This is a sanity property that shows that pipelining did not give

0 comments on commit ec12f2d

Please sign in to comment.
You can’t perform that action at this time.