typed-protocols-0.1.0.0: A framework for strongly typed protocols

Network.TypedProtocol.Proofs

Description

Proofs about the typed protocol framework.

It also provides helpful testing utilities.

Synopsis

# About these proofs

Typed languages such as Haskell can embed proofs. In total languages this is straightforward: a value inhabiting a type is a proof of the property corresponding to the type.

In languages like Haskell that have ⊥ as a value of every type, things are slightly more complicated. We have to demonstrate that the value that inhabits the type of interest is not ⊥ which we can do by evaluation.

This idea crops up frequently in advanced type level programming in Haskell. For example Refl proofs that two types are equal have to have a runtime representation that is evaluated to demonstrate it is not ⊥ before it can be relied upon.

The proofs here are about the nature of typed protocols in this framework. The connect and connectPipelined proofs rely on a few lemmas about the individual protocol. See AgencyProofs.

# Connect proof

connect ∷ ∀ ps (pr ∷ PeerRole) (st ∷ ps) m a b. (Monad m, Protocol ps) ⇒ Peer ps pr st m a → Peer ps (FlipAgency pr) st m b → m (a, b, TerminalStates ps) Source #

The connect function takes two peers that agree on a protocol and runs them in lock step, until (and if) they complete.

The connect function serves a few purposes.

• The fact we can define this function at at all proves some minimal sanity property of the typed protocol framework.
• It demonstrates that all protocols defined in the framework can be run with synchronous communication rather than requiring buffered communication.
• It is useful for testing peer implementations against each other in a minimalistic setting.

data TerminalStates ps where Source #

The terminal states for the protocol. Used in connect and connectPipelined to return the states in which the peers terminated.

Constructors

 TerminalStates ∷ ∀ ps (st ∷ ps). NobodyHasAgency st → NobodyHasAgency st → TerminalStates ps

# Pipelining proofs

Additional proofs specific to the pipelining features

Arguments

 ∷ ∀ ps (pr ∷ PeerRole) (st ∷ ps) m a b. (Monad m, Protocol ps) ⇒ [Bool] Interleaving choices. [] gives no pipelining. → PeerPipelined ps pr st m a → Peer ps (FlipAgency pr) st m b → m (a, b, TerminalStates ps)

Analogous to connect but for pipelined peers.

Since pipelining allows multiple possible interleavings, we provide a [Bool] parameter to control the choices. Each True will trigger picking the first choice in the SenderCollect construct (if possible), leading to more results outstanding. This can also be interpreted as a greater pipeline depth, or more messages in-flight.

This can be exercised using a QuickCheck style generator.

forgetPipelined ∷ ∀ ps (pr ∷ PeerRole) (st ∷ ps) m a. Functor m ⇒ PeerPipelined ps pr st m a → Peer ps pr st m a Source #

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 us extra expressiveness or to break the protocol state machine.

## Pipeline proof helpers

data Queue (n ∷ N) a where Source #

A size indexed queue. This is useful for proofs, including connectPipelined but also as so-called direct functions for running a client and server wrapper directly against each other.

Constructors

 EmptyQ ∷ Queue Z a ConsQ ∷ a → Queue n a → Queue (S n) a

enqueue ∷ a → Queue n a → Queue (S n) a Source #

At an element to the end of a Queue. This is not intended to be efficient. It is only for proofs and tests.

## Auxilary functions

Arguments

 ∷ Int Bound on outstanding responses → [Bool] Pipelining choices → [req] → [resp] → [Either req resp]

A reference specification for interleaving of requests and responses with pipelining, where the environment can choose whether a response is available yet.

This also supports bounded choice where the maximum number of outstanding in-flight responses is limted.