\ignore{ \begin{code} 
{-|
Module      :  Parry.Protocol
Copyright   :  (c) Pierre-Étienne Meunier 2014
License     :  GPL-3
Maintainer  :  pierre-etienne.meunier@lif.univ-mrs.fr
Stability   :  experimental
Portability :  All

This module contains all data types exchanged between the client
and the server, except for the initial \"@Hello@\" message, and is
mostly exposed for full disclosure of the protocol's proof.
-}
{-# LANGUAGE DeriveGeneric #-}
\end{code} } The first module we need is {\tt Parry.Protocol}, that defines the type of messages exchanged between the client and server. We assume, in the rest of the proof, that the {\tt encode} and {\tt decode} functions generated by the {\tt Binary} instances of these datatypes verify {\tt decode.encode} is the identity. \hfill \begin{code} 
module Parry.Protocol where
import Data.Binary
import GHC.Generics (Generic)
import Codec.Crypto.RSA.Pure

-- | The type of messages sent by the client, exposed here for full
-- disclosure of the protocol's proof.
data ClientMessage j=
  GetJob Integer PublicKey
  | JobDone { clientId::Integer, jobResults::[j], currentJob::j }
  | NewJobs { clientId::Integer, jobResults::[j], currentJob::j,
              nextJob::j, newJobs::[j] }
  | Alive Integer
  deriving (Generic, Show)

-- | The type of messages sent by the server, exposed here for full
-- disclosure of the protocol's proof.
data ServerMessage j=
  Job Bool j
  | Finished
  | Ack
  | Die
  deriving (Generic,Show)

instance (Binary j)=>Binary (ClientMessage j)
instance (Binary j)=>Binary (ServerMessage j)
\end{code} \vspace{1em}