The great rewrite of 2023

1 files changed, 0 insertions, 471 deletions

diff --git a/site/posts/CoqffiEcho.org b/site/posts/CoqffiEcho.org
deleted file mode 100644
index f2b03b1..0000000
--- a/site/posts/CoqffiEcho.org
+++ /dev/null
@@ -1,471 +0,0 @@
-#+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
-[[rel:/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="Socket.v" style="dashed"];
-    ffi [label="socket.mli"];
-  }
-  subgraph {
-    Echo [label="Echo.v"];
-  }
-
-  subgraph {
-    rank=same;
-    echo_v [label="main.v"];
-    echo_ml [label="main.ml" style="dashed"];
-  }
-
-  ffi -> FFI [style="dashed" label="coqffi      "];
-  echo_ml -> echo_v [dir=back style="dashed" label="coqc     "];
-  FFI -> Echo -> echo_v;
-  ffi -> echo_ml;
-}
-#+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 name, 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