#+TITLE: Implementing an Echo Server in Coq with ~coqffi~

#+SERIES: ./Coqffi.html
#+SERIES_PREV: ./CoqffiIntro.html

#+NAME: coqffi_output
#+BEGIN_SRC sh :results output :exports none :var mod=""
cat ${ROOT}/lp/coqffi-tutorial/_build/default/ffi/${mod}
#+END_SRC

In this article, we will demonstrate how ~coqffi~ can be used to
implement an echo server, /i.e./, a TCP server which sends back any
input it receives from its clients.  In addition to ~coqffi~, you will
need to install ~coq-simple-io~.  The latter is available in the
~released~ repository of the Opam Coq Archive.

#+BEGIN_SRC sh
opam install coq-coqffi coq-simple-io
#+END_SRC

Besides, this article is a literate program, and you can download
[[/files/coqffi-tutorial.tar.gz][the resulting source tree]] if you
want to try to read the source directly, or modify it to your taste.

#+BEGIN_EXPORT html
<nav id="generate-toc"></nav>
<div id="history">site/posts/CoqffiEcho.org</div>
#+END_EXPORT

* Project Layout

Before diving too much into the implementation of our echo server, we
first give an overview of the resulting project’s layout. Since we aim
at implementing a program, we draw our inspiration from the idiomatic
way of organizing a OCaml project.

#+BEGIN_SRC sh :results output :exports results
cd ${ROOT}/lp/coqffi-tutorial/
tree --noreport -I "_build"
#+END_SRC

We have three directories at the root of the project.

- ~ffi/~ contains the low-level OCaml code ::
  It provides an OCaml library (~ffi~), and a Coq theory (~FFI~) which
  gathers the FFI modules generated by ~coqffi~.
- ~src/~ contains the Coq implementation of our echo server ::
  It provides a Coq theory (~Echo~) which depends on the ~FFI~ theory
  the ~SimpleIO~ theory of ~coq-simple~io~. This theory provides the
  implementation of our echo server in Coq.
- ~bin/~ contains the pieces of code to get an executable program ::
  It contains a Coq module (~echo.v~) which configures and uses the
  extraction mechanism to generate an OCaml module (~echo.ml~). This
  OCaml module can be compiled to get an executable program.

Note that we could have decided to only have one Coq theory. We could
also have added a fourth directory (~theories/~) for formal
verification specific code, but this is out of the scope of this
tutorial.

Overall, we use ~dune~ to compile and compose the different parts of
the echo server. ~dune~ has a native —yet unstable at the time of
writing— support for building Coq projects, with very convenient
stanzas like =coq.theory= and =coq.extraction=.

The following graph summarizes the dependencies between each component
(plain arrows symbolize software dependencies).

#+BEGIN_SRC dot :file deps.svg :exports results
digraph dependencies {
  graph [nodesep="0.4"];
  rankdir="LR";
  node [shape=box];
  subgraph {
    rank=same;
    FFI [label="(coq.theory FFI)"];
    ffi [label="(library ffi)"];
  }
  subgraph {
    Echo [label="(coq.theory Echo)"];
  }

  subgraph {
    rank=same;
    echo_v [label="(coq.extraction echo)"];
    echo_ml [label="(executable echo)"];
  }

  ffi -> FFI [style="dotted" label="generated by coqffi"];
  echo_ml -> echo_v [dir=back style="dotted" label="generated by Coq"];
  echo_v -> Echo -> FFI;
  echo_ml -> ffi;
}
#+END_SRC

We enable Coq-related stanza with ~(using coq 0.2)~ in the
~dune-project~.
file.

#+BEGIN_SRC lisp :tangle coqffi-tutorial/dune-project
(lang dune 2.7)
(using coq 0.2)
#+END_SRC

The rest of this tutorial proceeds by diving into each directory.

* FFI Bindings

Our objective is to implement an echo server, /i.e./, a server which
(1) accepts incoming connections, and (2) sends back any incoming
messages. We will consider two classes of effects. One is related to
creating and manipulating TCP sockets. The other is dedicated to
process management, more precisely to be able to fork when receiving
incoming connections.

Therefore, the ~ffi~ library will provide two modules. Likewise, the
~FFI~ theory will provide two analogous modules generated by ~coqffi~.

In the ~ffi/~ directory, we add the following stanza to the ~dune~
file.

#+BEGIN_SRC lisp :tangle coqffi-tutorial/ffi/dune
(library
  (name ffi)
  (libraries unix))
#+END_SRC

~dune~ will look for any ~.ml~ and ~.mli~ files within the directory
and will consider they belong to the ~ffi~ library. We use the
[[https://caml.inria.fr/pub/docs/manual-ocaml/libref/Unix.html][~unix~]]
library to implement the features we are looking for.

Then, we add the following stanza to the ~dune~ file of the ~ffi/~
directory.

#+BEGIN_SRC lisp :tangle coqffi-tutorial/ffi/dune
(coq.theory
  (name FFI))
#+END_SRC

This tells ~dune~ to look for ~.v~ file within the ~ffi/~ directory,
in order to build them with Coq.  A nice feature of ~dune~ is that if
we automatically generate Coq files, they will be automatically
“attached” to this theory.

** Sockets

Sockets are boring. The following OCaml module interface provides the
necessary type and functions to manipulate them.

#+BEGIN_SRC ocaml :tangle coqffi-tutorial/ffi/socket.mli
type socket_descr

val open_socket : string -> int -> socket_descr
val listen : socket_descr -> unit
val recv : socket_descr -> string
val send : socket_descr -> string -> int
val accept_connection : socket_descr -> socket_descr
val close_socket : socket_descr -> unit
#+END_SRC

Our focus is how to write the interface modules for ~coqffi~. Since
the object of this tutorial is not the implementation of an echo
server in itself, the implementation details of the ~ffi~ library will
not be discussed.

#+BEGIN_details
#+HTML: <summary>Implementation for <code>socket.mli</code></summary>

There is not much to say, except that (as already stated) we use the
~Unix~ module to manipulate sockets, and we attach to each socket a
buffer to store incoming bytes.

#+BEGIN_SRC ocaml :tangle coqffi-tutorial/ffi/socket.ml
let buffer_size = 1024

type socket_descr = {
  fd : Unix.file_descr;
  recv_buffer : bytes;
}

let from_fd fd =
  let rbuff = Bytes.create buffer_size in
  { fd = fd; recv_buffer = rbuff }

let open_socket hostname port =
  let open Unix in
  let addr = inet_addr_of_string hostname in
  let fd = socket PF_INET SOCK_STREAM 0 in
  setsockopt fd SO_REUSEADDR true;
  bind fd (ADDR_INET (addr, port));
  from_fd fd

let listen sock = Unix.listen sock.fd 1

let recv sock =
  let s = Unix.read sock.fd sock.recv_buffer 0 buffer_size in
  Bytes.sub_string sock.recv_buffer 0 s

let send sock msg =
  Unix.write_substring sock.fd msg 0 (String.length msg)

let accept_connection sock =
  Unix.accept sock.fd |> fst |> from_fd

let close_socket sock = Unix.close sock.fd
#+END_SRC
#+END_details

~dune~ generates ~.cmi~ files for the ~.mli~ files of our library, and
provides the necessary bits to easily locate them. Besides, the
=action= stanza can be used here to tell to ~dune~ how to generate the
module ~Socket.v~ from ~file.cmi~. We add the following entry to
~ffi/dune~.

#+BEGIN_SRC lisp :tangle coqffi-tutorial/ffi/dune
(rule
  (target Socket.v)
  (action (run coqffi %{cmi:socket} -o %{target})))
#+END_SRC

We call ~coqffi~ without any feature-related command-line argument,
which means only the ~simple-io~ feature is enabled. As a consequence,
the ~socket_descr~ type is axiomatized in Coq, and in addition to a
=MonadSocket= monad, ~coqffi~ will generate an instance for this monad
for the =IO= monad of ~coq-simple-io~.

Interested readers can have a look at the generated Coq module below.

#+BEGIN_details
#+HTML: <summary><code>Socket.v</code> as generated by <code>coqffi</code></summary>

#+BEGIN_SRC coq :noweb yes
<<coqffi_output(mod="Socket.v")>>
#+END_SRC
#+END_details

** Process Management

In order to avoid a client to block the server by connecting to it
without sending anything, we can fork a new process for each client.

#+BEGIN_SRC ocaml :tangle coqffi-tutorial/ffi/proc.mli
type identity = Parent of int | Child

val fork : unit -> identity
#+END_SRC

#+BEGIN_details
#+HTML: <summary>Implementation for <code>proc.mli</code></summary>

Again, thanks to the ~Unix~ module, the implementation is pretty
straightforward.

#+BEGIN_SRC ocaml :tangle coqffi-tutorial/ffi/proc.ml
type identity = Parent of int | Child

let fork x =
  match Unix.fork x with
  | 0 -> Child
  | x -> Parent x
#+END_SRC
#+END_details

This time, the ~proc.mli~ module interface introduces a transparent
type, /i.e./, it also provides its definition. This is a good use case
for the ~transparent-types~ feature of ~coqffi~. In the stanza for
generating ~Proc.v~, we enable it with the ~-ftransparent-types~
command-line argument, like this.

#+BEGIN_SRC lisp :tangle coqffi-tutorial/ffi/dune
(rule
  (target Proc.v)
  (action (run coqffi -ftransparent-types %{cmi:proc} -o %{target})))
#+END_SRC

#+BEGIN_details
#+HTML: <summary><code>Proc.v</code> as generated by <code>coqffi</code></summary>
#+BEGIN_SRC coq :noweb yes
<<coqffi_output(mod="Proc.v")>>
#+END_SRC
#+END_details

We now have everything we need to implement an echo server in Coq.

* Implementing an Echo Server

Our implementation will be part of a dedicated Coq theory, called
~Echo~. This is done easily a ~dune~ file in the ~src/~ directory,
with the following content.

#+BEGIN_SRC lisp :tangle coqffi-tutorial/src/dune
(coq.theory
  (name Echo)
  (theories FFI))
#+END_SRC

In the rest of this section, we will discuss the content of the unique
module of this theory. Hopefully, readers familiar with programming
impurity by means of monads will not find anything particularly
surprising here.

Let us start with the inevitable sequence of import commands. We use
the =Monad= and =MonadFix= typeclasses of =ExtLib=, and our FFI
modules from the =FFI= theory we have previously defined.

#+BEGIN_SRC coq :tangle coqffi-tutorial/src/Server.v
From ExtLib Require Import Monad MonadFix.
From FFI Require Import Proc Socket.
#+END_SRC

Letting Coq guess the type of unintroduced variables using the ~`~
annotation (/e.g./, in presence of ~`{Monad m}~, Coq understands ~m~
is of type ~Type -> Type~) is always nice, so we enable it.

#+BEGIN_SRC coq :tangle coqffi-tutorial/src/Server.v
Generalizable All Variables.
#+END_SRC

We enable the monad notation provided by =ExtLib=. In this article, we
prefer the ~let*~ notation (as recently introduced by OCaml) over the
~<-~ notation of Haskell, but both are available.

#+BEGIN_SRC coq :tangle coqffi-tutorial/src/Server.v
Import MonadLetNotation.
Open Scope monad_scope.
#+END_SRC

Then, we define a notation to be able to define local, monadic
recursive functions using the =mfix= combinator of the =MonadFix=
typeclass.

#+BEGIN_SRC coq :tangle coqffi-tutorial/src/Server.v
Notation "'let_rec*' f x ':=' p 'in' q" :=
  (let f := mfix (fun f x => p) in q)
    (at level 61, x pattern, f ident, q at next level, right associativity).
#+END_SRC

Note that ~mfix~ does /not/ check whether or not the defined function
will terminate (contrary to the ~fix~ keyword of Coq). This is
fortunate because in our case, we do not want our echo server to
converge, but rather to accept an infinite number of connections.

We can demonstrate how this notation can be leveraged by defining a
generic TCP server, parameterized by a handler to deal with incoming
connections.

#+BEGIN_SRC coq :tangle coqffi-tutorial/src/Server.v
Definition tcp_srv `{Monad m, MonadFix m, MonadProc m, MonadSocket m}
    (handler : socket_descr -> m unit)
  : m unit :=
  let* srv := open_socket "127.0.0.1" 8888 in
  listen srv;;

  let_rec* tcp_aux _ :=
    let* client := accept_connection srv in
    let* res := fork tt in
    match res with
    | Parent _ => close_socket client >>= tcp_aux
    | Child =>  handler client
    end
  in

  tcp_aux tt.
#+END_SRC

The handler for the echo server is straightforward: it just reads
incoming bytes from the socket, sends it back, and closes the socket.

#+BEGIN_SRC coq :tangle coqffi-tutorial/src/Server.v
Definition echo_handler `{Monad m, MonadSocket m} (sock : socket_descr)
  : m unit :=
  let* msg := recv sock in
  send sock msg;;
  close_socket sock.
#+END_SRC

Composing our generic TCP server with our echo handler gives us an
echo server.

#+BEGIN_SRC coq :tangle coqffi-tutorial/src/Server.v
Definition echo_server `{Monad m, MonadFix m, MonadProc m, MonadSocket m}
  : m unit :=
  tcp_srv echo_handler.
#+END_SRC

Because ~coqffi~ has generated typeclasses for the impure primitives
of ~proc.mli~ and ~socket.mli~, =echo_server= is polymorphic, and can
be instantiated for different monads. When it comes to extracting our
program, we will generally prefer the =IO= monad of ~coq-simple-io~.
But we could also imagine verifying the client handler with FreeSpec,
or the generic TCP server with Interaction Trees (which support
diverging computations). Overall, we can have different verification
strategies for different parts of our program, by leveraging the most
relevant framework for each part, yet being able to extract it in an
efficient form.

The next section shows how this last part is achieved using, once
again, a convenient stanza of dune.

* Extracting and Building an Executable

The ~0.2~ version of the Coq-related stanzas of ~dune~ provides the
~coq.extraction~ stanza, which can be used to build a Coq module
expected to generate ~ml~ files.

In our case, we will write ~bin/echo.v~ to extract the ~echo_server~
in a ~echo.ml~ module, and uses the =executable= stanza of ~dune~ to
get an executable from this file. To achieve this, the ~bin/dune~
file simply requires these two stanzas.

#+BEGIN_SRC lisp :tangle coqffi-tutorial/bin/dune
(coq.extraction
  (prelude echo)
  (theories Echo)
  (extracted_modules echo))

(executable
  (name echo)
  (libraries ffi))
#+END_SRC

We are almost done. We now need to write the ~echo.v~ module, which
mostly consists of (1) providing a =MonadFix= instance for the =IO=
monad, (2) using the =IO.unsafe_run= function to escape the =IO=
monad, (3) calling the src_coq[:exports code]{Extraction} command to
wrap it up.

#+BEGIN_SRC coq :tangle coqffi-tutorial/bin/echo.v
From Coq Require Extraction.
From ExtLib Require Import MonadFix.
From SimpleIO Require Import SimpleIO.
From Echo Require Import Server.

Instance MonadFix_IO : MonadFix IO :=
  { mfix := @IO.fix_io }.

Definition main : io_unit :=
  IO.unsafe_run echo_server.

Extraction "echo.ml" main.
#+END_SRC

Since we are using the =i63= type (signed 63bits integers) of the
~CoqFFI~ theory, and since =i63= is implemented under the hood with
Coq primitive integers, we /also/ need to provide a =Uint63= module
with a =of_int= function. Fortunately, this module is straightforward
to write.

#+BEGIN_SRC ocaml :tangle coqffi-tutorial/bin/uint63.ml
let of_int x = x
#+END_SRC

And /voilà/. A call to ~dune~ at the root of the repository will
build everything (Coq and OCaml alike). Starting the echo server
is as simple as

#+BEGIN_SRC sh
dune exec bin/echo.exe
#+END_SRC

And connecting to it can be achieved with a program like =telnet=.

#+BEGIN_SRC console
$ telnet 127.0.0.1 8888
Trying 127.0.0.1...
Connected to 127.0.0.1.
Escape character is '^]'.
hello, echo server!
hello, echo server!
Connection closed by foreign host.
#+END_SRC