1 files changed, 468 insertions, 0 deletions
diff --git a/site/posts/CoqffiEcho.org b/site/posts/CoqffiEcho.org
new file mode 100644
index 0000000..0c984dc
--- /dev/null
+++ b/site/posts/CoqffiEcho.org
@@ -0,0 +1,468 @@
+#+BEGIN_EXPORT html
+<h1>Implementing an Echo Server in Coq with <code>coqffi</code></h1>
+#+END_EXPORT
+
+#+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 programm, 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.
+
+#+TOC: headlines 2
+
+* 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 an manipulating 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 [@@impure]
+val listen : socket_descr -> unit [@@impure]
+val recv : socket_descr -> string [@@impure]
+val send : socket_descr -> string -> int [@@impure]
+val accept_connection : socket_descr -> socket_descr [@@impure]
+val close_socket : socket_descr -> unit [@@impure]
+#+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 discuss.
+
+#+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 clients.
+
+#+BEGIN_SRC ocaml :tangle coqffi-tutorial/ffi/proc.mli
+type identity = Parent of int | Child
+
+val fork : unit -> identity [@@impure]
+#+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 monad 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 guessing 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 part 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 consists in
+
+#+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 in (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