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

Tool to build clients for Parry.
-}
\end{code}
}

We now prove the client functions. More precisely, we prove that the clients
that can be built using the functions in this module are valid and fluent,
provided that their ``worker'' function explores the space correctly. We include
the whole source code of this module for the sake of completeness.

\hfill

\begin{code}
module Parry.Client(
  -- * Jobs on the client side
  Client(..),
  -- * Writing clients
  client,Config(..),defaultConfig
  ) where
import Network
import System.IO
import System.Exit
#ifdef UNIX
import System.Posix.Signals
#endif
import Control.Concurrent
import Control.Exception as E
import Data.List
import Codec.Crypto.RSA.Pure
import qualified Data.ByteString.Lazy.Char8 as B8
import qualified Data.ByteString.Char8 as S
import Data.Binary
import Parry.Util
import Parry.Protocol


-- | For a job to be usable by Parry's clients, it must be a member of this class.
class Client j where
  -- | This function is used by the client to distinguish results from regular jobs.
  isResult::j->Bool
\end{code}
\ignore{
\begin{code}
-- | Client configuration
data Config=Config {
  -- | The server's host name (either a DNS name or an IP address).
  server::String,
  -- | The port number (for instance @'Network.PortNumber' 5129@).
  port::PortID,
  -- | The private key to sign messages.
  privateKey::PrivateKey,
  -- | The public key, that the server must know of before the clients connect.
  publicKey::PublicKey
  }

-- | A default configuration, matching the server's
-- 'Parry.Server.defaultConfig'.  Note that, like in the server, you
-- must provide your own private key for signing the protocol
-- messages. See 'Parry.Server.defaultConfig' for an example method to
-- generate these keys.
defaultConfig::PrivateKey->PublicKey->Config
defaultConfig pr pu=Config {
  server="127.0.0.1",
  port=PortNumber 5129,
  privateKey=pr,
  publicKey=pu
  }
\end{code}
}
\begin{lemma}
\label{lem:signAndSend}
The {\tt signAndSend\_} and {\tt signAndSend} functions send only one kind of
messages on the network, with two lines: the first line is an encoding
via {\tt encode16l} of $m$, the encoding via {\tt encode} of a constructor
of the {\tt ClientMessage} type.
The second line is the RSA signature of $m$ using the private key in the
{\tt conf} argument.
\begin{proof}

The results follows from the fact that this function uses only two lines to send
messages on the network, and these two lines have the claimed form.

\hfill

\begin{code}
-- | A wrapper around signAndSend, to force the type of @j@, which is
-- needed for the protocol's @Alive@ messages.
signAndSend_::(Binary j)=>Config->j->ClientMessage j->IO (ServerMessage j)
signAndSend_ conf _ a=signAndSend conf a

-- | Sign a message and send it.
signAndSend::(Binary j)=>Config->ClientMessage j->IO (ServerMessage j)
signAndSend conf m=do {
  let { msg=encode m };
  case sign (privateKey conf) msg of {
    Right b->E.catch (do {
                         l<-bracket (connectTo (server conf) (port conf)) (hClose)
                            (\h->do {
                                B8.hPutStrLn h $ encode16l msg;
                                B8.hPutStrLn h $ encode16l b;
                                hFlush h;
                                S.hGetLine h;
                                });
                         case decodeOrFail $ decode16l $ B8.fromStrict l of {
                           Right (_,_,a)->return a;
                           Left _->do {
                             threadDelay 1000000;
                             signAndSend conf m
                             }
                           }})
             (\e->do {
                 let { _=e::IOError };
                 print e;
                 threadDelay 1000000;signAndSend conf m
                 });
    er->do {
      print er;hFlush stdout;threadDelay 100000;signAndSend conf m
      }
    }}
\end{code}

\end{proof}
\end{lemma}

To prove the remaining functions, we need to introduce the following invariant
on their arguments:
\begin{invariant}
\label{h}
When the {\tt cur} variable is not {\tt Nothing},
the {\tt jobs} and {\tt results} variables contain,
respectively, the list of all jobs of the contents of {\tt cur} that have not
been completely explored, and the list of results found during the exploration
of all other subjobs of the job in {\tt cur}.
\end{invariant}


\begin{lemma}
\label{lem:dowork}
If there is a function {\tt doWork} such that, at the same time:
\begin{enumerate}
\item For all values of {\tt b}, {\tt save} and {\tt j}, {\tt doWork b save j}
only calls {\tt save} with arguments {\tt l} and {\tt r}, where {\tt r} is the
list of all results that have been found when the subjobs of {\tt j} that have
not been completely explored are all in list {\tt l}.

\item For all values of {\tt b}, {\tt save} and {\tt j}, {\tt doWork b save
j} returns the list of all subjobs of {\tt j} that have not been explored, and
all results that have been found in {\tt j}, in the remaining subjobs of {\tt j}.

\end{enumerate}
Then {\tt client conf doWork} is a valid and fluent client.
\begin{proof}

We first prove fluency: in the two functions below ({\tt work} and {\tt
client}), the only messages sent to the network are either sent using {\tt
signAndSend}, or else consist of a single line containing exactly {\tt Hello},
which is the definition of fluency (by Lemma \ref{lem:signAndSend}).

We now prove that {\tt client conf doWork} is valid. Indeed, condition
\ref{valid:newjobs} of validity ({\tt NewJobs} messages contain all subjobs of
the current job) is clearly respected by the {\tt work} function: indeed, by the
definition of a result, the {\tt todo} variable in {\tt work} is the list of all
subjobs that have not been explored. Condition \ref{valid:jobdone} is also
respected, because it is not applicable to the {\tt work} function.

Moreover, the {\tt work} function returns either {\tt Nothing}, or {\tt Just
(j,r)} where {\tt j} is a job, and {\tt r} is the list of all results found
during the exploration of {\tt j}. We prove this recursively on its code:

\hfill
\begin{code}
work::(Client j,Binary j)=>Config->MVar [j]->MVar[j]->MVar (Maybe j)->
      (Bool->([j]->[j]->IO ())->j->IO [j])->Bool->Integer->j->IO (Maybe (j,[j]))
work conf jobs results cur doWork shared num j=do
  let save jobs_ results_ jobs results=do
        modifyMVar_ jobs_ $ \_->return jobs
        modifyMVar_ results_ $ \_->return results
  someWork<-doWork shared (save jobs results) j
  let (result,todo)=partition isResult someWork
  case todo of
\end{code}
\hfill

Either {\tt doWork} has returned no new jobs, in which case the induction
hypothesis clearly holds, because the exploration of the current job is over.

\hfill
\begin{code}
    []->return (Just (j,result))
\end{code}
\hfill

Or {\tt doWork} returns some new jobs. In this case, {\tt work} is called on
{\tt u} only after reply {\tt Ack} has been received from the server,
acknowledging that the current job registered for this client has been updated.
Therefore, {\tt work} is called recursively on the current job of this client,
and hence, the claim also holds, by recursion.

\hfill
\begin{code}
    u:v->do
      x<-signAndSend conf (NewJobs {clientId=num,jobResults=result,
                                    currentJob=j,nextJob=u,newJobs=v })
      modifyMVar_ cur (\_->do {
                          modifyMVar_ results (\_->return []);
                          modifyMVar_ jobs (\_->return [u]);
                          return (Just u)
                          })
      case x of
        Ack->work conf jobs results cur doWork (shared && (null v)) num u;
        _->return Nothing
\end{code}
\hfill

We will now prove validity for the code of the {\tt client} function.
We have assumed that the {\tt save} function above is only called on
a list {\tt l} of subjobs, and a list {\tt r} of results, such that
{\tt l} contains all subjobs of the initial job {\tt j} that have
not been completely explored when results {\tt r} are found.

Therefore, in the {\tt work} function above, Invariant \ref{h} on
the {\tt jobs\_} and {\tt results\_} variables is clearly maintained:

\hfill
\ignore{
\begin{code}
-- | @'client' config work@ calls its argument function @work@ on a
-- boolean @s@ (if the server asked to share jobs) and the actual job
-- @j@ that must be done. @work@ must return a list of resulting jobs,
-- that may include results (see 'Parry.Protocol.Client').
--
-- Workers asked to share their input job should share it as early as
-- possible: this usually means that the job already got killed in a
-- previous attempt, probably because of its length.
\end{code}
}
\begin{code}
client::(Binary j,Client j)=>
        Config->(Bool->([j]->[j]->IO())->j->IO [j])->IO ()
client conf doWork=
  let startConnection=do
        hPutStrLn stderr "Connecting..."
        hFlush stderr
        l<-E.catch (bracket (connectTo (server conf) (port conf)) hClose
                    (\h->do {
                        B8.hPutStrLn h (B8.pack "Hello");
                        hFlush h;
                        l<-S.hGetLine h;
                        case decodeOrFail (decode16l (B8.fromStrict l)) of {
                          Right x->return (Right x);
                          Left _->return (Left ())
                          }}))
           (\e->let _=e::IOError in do { hPutStrLn stderr $ show e; return (Left ()) })
        case l of
          Right (_,_,num)->do
            jobs<-newMVar []
            results<-newMVar []
            cur<-newMVar Nothing
\end{code}
\hfill

At this point, {\tt cur} contains {\tt Nothing}: Invariant \ref{h} is clearly
maintained.

Now remark that, when the {\tt saveAll} function below is called, and the {\tt
cur} variable contains {\tt Nothing}, no message is sent. Therefore, if
Invariant \ref{h} holds when {\tt saveAll} is called, the corresponding {\tt NewJobs}
message respects the validity condition.

\hfill
\begin{code}
            let saveAll=withMVar jobs $ \j->
                  withMVar cur $ \curj->
                  case (j,curj) of {
                    (h:s,Just cu)->
                       withMVar results $ \res->do {
                         _<-signAndSend conf (
                            NewJobs { clientId=num,
                                      jobResults=res,
                                      currentJob=cu,
                                      nextJob=h,
                                      newJobs=s
                                    });
                         return ()};
                       _->return ()
                    }
            myth<-myThreadId
            threads<-newMVar myth
#ifdef UNIX
            installHandler sigTERM
              (Catch (modifyMVar_ threads (\a->do {if a==myth then return () else
                                                     killThread a;return myth}))) Nothing
#endif
            let getAJob=do
                  job_<-signAndSend conf (GetJob num (publicKey conf));
                  case job_ of
                    Job share j->do
                      modifyMVar_ cur (\_->do {
                                          modifyMVar_ jobs (\_->return [j]);
                                          modifyMVar_ results (\_->return []);
                                          return (Just j)
                                          });
                      workerMVar<-newEmptyMVar;
\end{code}
\hfill

At this point, Invariant \ref{h} still holds: the only subjob of the current job
is itself, and no results have been found.

\hfill
\begin{code}
                      workerThread<-
                        forkFinally
                        (do {
                            x<-work conf jobs results cur doWork share num j;
                            case x of {
                              Just (j',r)->do {
                                 _<-signAndSend conf
                                    (JobDone {clientId=num,
                                              currentJob=j',
                                              jobResults=r });
                                 return () };
                              Nothing->return ()
                              }})
                        (\_->putMVar workerMVar ())
\end{code}
\hfill

Here, the validity condition holds for the {\tt JobDone} message: indeed, the
current job has been completely explored, and found exactly the results in {\tt
r}.

\hfill
\begin{code}
                      let heartbeat=do
                            answer<-signAndSend_ conf j (Alive num)
                            case answer of
                              Ack->do { threadDelay 300000000; heartbeat }
                              _->do { saveAll; killThread workerThread }
                      heartbeatMVar<-newEmptyMVar
                      hbThread<-forkIO
                                (heartbeat`finally`(putMVar heartbeatMVar ()))
                      modifyMVar_ threads (\_->return workerThread)
                      takeMVar workerMVar
                      killThread hbThread
                      takeMVar heartbeatMVar
                      stop<-withMVar threads (\t->return (t==myth))
                      if stop then do { saveAll; exitSuccess } else getAJob
                    Finished->return ();
                    _->do
                      threadDelay 10000000
                      getAJob
            getAJob
          Left _->do
            threadDelay 5000000
            startConnection
  in
   startConnection
\end{code}
\end{proof}
\end{lemma}