From 2706544cf000a6f9875e81f86d885d4dc68dfb23 Mon Sep 17 00:00:00 2001 From: Thomas Letan Date: Thu, 10 Dec 2020 14:15:24 +0100 Subject: Add a Series on coqffi, and the first literate program of this blog --- site/posts/CoqffiEcho.org | 468 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 468 insertions(+) create mode 100644 site/posts/CoqffiEcho.org (limited to 'site/posts/CoqffiEcho.org') 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 +

Implementing an Echo Server in Coq with coqffi

+#+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: 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. + +#+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: Socket.v as generated by coqffi + +#+BEGIN_SRC coq :noweb yes +<> +#+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: Implementation for proc.mli + +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: Proc.v as generated by coqffi +#+BEGIN_SRC coq :noweb yes +<> +#+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 -- cgit v1.2.3