Safe Haskell | None |
---|---|

Language | Haskell2010 |

Proofs about the typed protocol framework.

It also provides helpful testing utilities.

## Synopsis

- 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)
- data TerminalStates ps where
- TerminalStates ∷ ∀ ps (st ∷ ps). NobodyHasAgency st → NobodyHasAgency st → TerminalStates ps

- connectPipelined ∷ ∀ ps (pr ∷ PeerRole) (st ∷ ps) m a b. (Monad m, Protocol ps) ⇒ [Bool] → PeerPipelined ps pr st m a → Peer ps (FlipAgency pr) st m b → m (a, b, TerminalStates ps)
- forgetPipelined ∷ ∀ ps (pr ∷ PeerRole) (st ∷ ps) m a. Functor m ⇒ PeerPipelined ps pr st m a → Peer ps pr st m a
- data Queue (n ∷ N) a where
- enqueue ∷ a → Queue n a → Queue (S n) a
- pipelineInterleaving ∷ Int → [Bool] → [req] → [resp] → [Either req resp]

# 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.

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

# Pipelining proofs

Additional proofs specific to the pipelining features

∷ ∀ 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.

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

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.