Implementing an Echo Server in Coq with coqffi
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.
opam install coq-coqffi coq-simple-io
Besides, this article is a literate program, and you can download the resulting source tree if you want to try to read the source directly, or modify it to your taste.
Revisions
This revisions table has been automatically generated
from the
git
history of this website repository, and the
change descriptions may not always be as useful as they should.
You can consult the source of this file in its current version here.
2021-08-20 | Fix a Coq warning | 3f65732 |
2021-08-20 | Improve the graph of dependencies of the Echo server | f29303e |
2021-03-28 | 2021 Spring redesign | 495f9db |
2021-02-24 | Release of coqffi 1.0.0~beta4 | 1a197fb |
2021-01-24 | Prepare coqffi.1.0.0~beta3 release | c15ed87 |
2020-12-10 | Spellchecking and revisions table for the coqffi articles | 9098a01 |
2020-12-10 | Add a Series on coqffi, and the first literate program of this blog | 2706544 |
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.
. ├── bin │ ├── dune │ ├── echo.v │ └── uint63.ml ├── dune-project ├── ffi │ ├── dune │ ├── proc.ml │ ├── proc.mli │ ├── socket.ml │ └── socket.mli └── src ├── dune └── Server.v
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 bycoqffi
. src/
contains the Coq implementation of our echo server- It provides a Coq theory (
Echo
) which depends on theFFI
theory theSimpleIO
theory ofcoq-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).
We enable Coq-related stanza with (using coq 0.2)
in the
dune-project
.
file.
(lang dune 2.7)
(using coq 0.2)
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.
(library
(name ffi)
(libraries unix))
dune
will look for any .ml
and .mli
files within the directory
and will consider they belong to the ffi
library. We use the
unix
library to implement the features we are looking for.
Then, we add the following stanza to the dune
file of the ffi/
directory.
(coq.theory
(name FFI))
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.
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
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.
Implementation for socket.mli
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.
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
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
.
(rule
(target Socket.v)
(action (run coqffi %{cmi:socket} -o %{target})))
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.
Socket.v
as generated by coqffi
(* This file has been generated by coqffi. *)
Set Implicit Arguments.
Unset Strict Implicit.
Set Contextual Implicit.
Generalizable All Variables.
Close Scope nat_scope.
From CoqFFI Require Export Extraction.
From SimpleIO Require Import IO_Monad.
Axiom socket_descr : Type.
Extract Constant socket_descr => "Ffi.Socket.socket_descr".
(** * Impure Primitives *)
(** ** Monad Definition *)
Class MonadSocket (m : Type -> Type) : Type :=
{ open_socket : string -> i63 -> m socket_descr
; listen : socket_descr -> m unit
; recv : socket_descr -> m string
; send : socket_descr -> string -> m i63
; accept_connection : socket_descr -> m socket_descr
; close_socket : socket_descr -> m unit
}.
(** ** [IO] Instance *)
Axiom io_open_socket : string -> i63 -> IO socket_descr.
Axiom io_listen : socket_descr -> IO unit.
Axiom io_recv : socket_descr -> IO string.
Axiom io_send : socket_descr -> string -> IO i63.
Axiom io_accept_connection : socket_descr -> IO socket_descr.
Axiom io_close_socket : socket_descr -> IO unit.
Extract Constant io_open_socket
=> "(fun x1 x2 k__ -> k__ ((Ffi.Socket.open_socket x1 x2)))".
Extract Constant io_listen => "(fun x1 k__ -> k__ ((Ffi.Socket.listen x1)))".
Extract Constant io_recv => "(fun x1 k__ -> k__ ((Ffi.Socket.recv x1)))".
Extract Constant io_send
=> "(fun x1 x2 k__ -> k__ ((Ffi.Socket.send x1 x2)))".
Extract Constant io_accept_connection
=> "(fun x1 k__ -> k__ ((Ffi.Socket.accept_connection x1)))".
Extract Constant io_close_socket
=> "(fun x1 k__ -> k__ ((Ffi.Socket.close_socket x1)))".
Instance IO_MonadSocket : MonadSocket IO :=
{ open_socket := io_open_socket
; listen := io_listen
; recv := io_recv
; send := io_send
; accept_connection := io_accept_connection
; close_socket := io_close_socket
}.
(* The generated file ends here. *)
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.
type identity = Parent of int | Child
val fork : unit -> identity
Implementation for proc.mli
Again, thanks to the Unix
module, the implementation is pretty
straightforward.
type identity = Parent of int | Child
let fork x =
match Unix.fork x with
| 0 -> Child
| x -> Parent x
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.
(rule
(target Proc.v)
(action (run coqffi -ftransparent-types %{cmi:proc} -o %{target})))
Proc.v
as generated by coqffi
(* This file has been generated by coqffi. *)
Set Implicit Arguments.
Unset Strict Implicit.
Set Contextual Implicit.
Generalizable All Variables.
Close Scope nat_scope.
From CoqFFI Require Export Extraction.
From SimpleIO Require Import IO_Monad.
Inductive identity : Type :=
| Parent (x0 : i63) : identity
| Child : identity.
Extract Inductive identity => "Ffi.Proc.identity"
[ "Ffi.Proc.Parent" "Ffi.Proc.Child" ].
(** * Impure Primitives *)
(** ** Monad Definition *)
Class MonadProc (m : Type -> Type) : Type := { fork : unit -> m identity
}.
(** ** [IO] Instance *)
Axiom io_fork : unit -> IO identity.
Extract Constant io_fork => "(fun x1 k__ -> k__ ((Ffi.Proc.fork x1)))".
Instance IO_MonadProc : MonadProc IO := { fork := io_fork
}.
(* The generated file ends here. *)
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.
(coq.theory
(name Echo)
(theories FFI))
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.
From ExtLib Require Import Monad MonadFix.
From FFI Require Import Proc Socket.
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.
Generalizable All Variables.
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.
Import MonadLetNotation.
Open Scope monad_scope.
Then, we define a notation to be able to define local, monadic
recursive functions using the mfix
combinator of the MonadFix
typeclass.
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).
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.
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.
The handler for the echo server is straightforward: it just reads incoming bytes from the socket, sends it back, and closes the socket.
Definition echo_handler `{Monad m, MonadSocket m} (sock : socket_descr)
: m unit :=
let* msg := recv sock in
send sock msg;;
close_socket sock.
Composing our generic TCP server with our echo handler gives us an echo server.
Definition echo_server `{Monad m, MonadFix m, MonadProc m, MonadSocket m}
: m unit :=
tcp_srv echo_handler.
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.
(coq.extraction
(prelude echo)
(theories Echo)
(extracted_modules echo))
(executable
(name echo)
(libraries ffi))
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 Extraction
command to
wrap it up.
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.
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.
let of_int x = x
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
dune exec bin/echo.exe
And connecting to it can be achieved with a program like telnet
.
$ 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.