diff options
| -rw-r--r-- | .gitignore | 81 | ||||
| -rw-r--r-- | site/cleopatra.org | 2 | ||||
| -rw-r--r-- | site/cleopatra/coq.org | 7 | ||||
| -rw-r--r-- | site/cleopatra/literate-programming.org | 42 | ||||
| -rw-r--r-- | site/cleopatra/org.org | 40 | ||||
| -rw-r--r-- | site/cleopatra/soupault.org | 2 | ||||
| -rw-r--r-- | site/index.org | 6 | ||||
| -rw-r--r-- | site/posts/CleopatraV1.org | 18 | ||||
| -rw-r--r-- | site/posts/Coqffi.org | 17 | ||||
| -rw-r--r-- | site/posts/CoqffiEcho.org | 468 | ||||
| -rw-r--r-- | site/posts/CoqffiIntro.org | 310 |
11 files changed, 932 insertions, 61 deletions
@@ -1,8 +1,11 @@ +*~ # begin generated files .cleopatra site/style/coq.sass coq.mk +export-lp.el +literate-programming.mk .emacs site/style/org.sass org.mk @@ -25,36 +28,78 @@ theme.mk site/style/main.sass templates/main.html build.log -*.vo -*.vok -*.vos -.*.aux -*.glob +site/posts/RewritingInCoq.vo +site/posts/StronglySpecifiedFunctionsRefine.vo +site/posts/AlgebraicDatatypes.vo +site/posts/MixingLtacAndGallina.vo +site/posts/LtacPatternMatching.vo +site/posts/ClightIntroduction.vo +site/posts/StronglySpecifiedFunctionsProgram.vo +site/posts/LtacMetaprogramming.vo +site/posts/RewritingInCoq.vok +site/posts/StronglySpecifiedFunctionsRefine.vok +site/posts/AlgebraicDatatypes.vok +site/posts/MixingLtacAndGallina.vok +site/posts/LtacPatternMatching.vok +site/posts/ClightIntroduction.vok +site/posts/StronglySpecifiedFunctionsProgram.vok +site/posts/LtacMetaprogramming.vok +site/posts/RewritingInCoq.vos +site/posts/StronglySpecifiedFunctionsRefine.vos +site/posts/AlgebraicDatatypes.vos +site/posts/MixingLtacAndGallina.vos +site/posts/LtacPatternMatching.vos +site/posts/ClightIntroduction.vos +site/posts/StronglySpecifiedFunctionsProgram.vos +site/posts/LtacMetaprogramming.vos +site/posts/RewritingInCoq.glob +site/posts/StronglySpecifiedFunctionsRefine.glob +site/posts/AlgebraicDatatypes.glob +site/posts/MixingLtacAndGallina.glob +site/posts/LtacPatternMatching.glob +site/posts/ClightIntroduction.glob +site/posts/StronglySpecifiedFunctionsProgram.glob +site/posts/LtacMetaprogramming.glob +site/posts/.RewritingInCoq.aux +site/posts/.StronglySpecifiedFunctionsRefine.aux +site/posts/.AlgebraicDatatypes.aux +site/posts/.MixingLtacAndGallina.aux +site/posts/.LtacPatternMatching.aux +site/posts/.ClightIntroduction.aux +site/posts/.StronglySpecifiedFunctionsProgram.aux +site/posts/.LtacMetaprogramming.aux .lia.cache -site/posts/AlgebraicDatatypes.html site/posts/RewritingInCoq.html -site/posts/LtacPatternMatching.html +site/posts/StronglySpecifiedFunctionsRefine.html +site/posts/AlgebraicDatatypes.html site/posts/MixingLtacAndGallina.html -site/posts/LtacMetaprogramming.html -site/posts/StronglySpecifiedFunctionsProgram.html +site/posts/LtacPatternMatching.html site/posts/ClightIntroduction.html -site/posts/StronglySpecifiedFunctionsRefine.html -site/cleopatra.html +site/posts/StronglySpecifiedFunctionsProgram.html +site/posts/LtacMetaprogramming.html +lp/ +site/files/coqffi-tutorial.tar.gz +site/posts/deps.svg site/opinions/MonadTransformers.html site/opinions/index.html +site/news/ColorlessThemes-0.2.html +site/projects/index.html site/cleopatra/soupault.html -site/cleopatra/coq.html site/cleopatra/org.html +site/cleopatra/literate-programming.html +site/cleopatra/coq.html site/cleopatra/theme.html -site/index.html -site/news/ColorlessThemes-0.2.html -site/projects/index.html -site/posts/Thanks.html +site/posts/ExtensibleTypeSafeErrorHandling.html +site/posts/CoqffiEcho.html site/posts/DiscoveringCommonLisp.html -site/posts/StronglySpecifiedFunctions.html +site/posts/CoqffiIntro.html site/posts/CleopatraV1.html -site/posts/ExtensibleTypeSafeErrorHandling.html +site/posts/StronglySpecifiedFunctions.html +site/posts/Thanks.html site/posts/Ltac.html +site/posts/Coqffi.html +site/cleopatra.html +site/index.html build/ site/style/main.css # end generated files diff --git a/site/cleopatra.org b/site/cleopatra.org index 67fd917..313007f 100644 --- a/site/cleopatra.org +++ b/site/cleopatra.org @@ -40,6 +40,8 @@ written as literate programs. - [[file:cleopatra/coq.org][Authoring Contents As Coq Documents ~(TODO)~]] :: +- [[./cleopatra/literate-programming.org][Authoring Literate Programs ~(TODO)~]] :: + - [[./cleopatra/org.org][Authoring Contents As Org Documents ~(TODO)~]] :: - [[./cleopatra/soupault.org][Processing HTML with ~soupault~]] :: diff --git a/site/cleopatra/coq.org b/site/cleopatra/coq.org index 7bd5d48..fcbee03 100644 --- a/site/cleopatra/coq.org +++ b/site/cleopatra/coq.org @@ -5,13 +5,18 @@ #+BEGIN_SRC makefile :tangle coq.mk COQ_POSTS := $(shell find site/ -name "*.v") COQ_HTML := $(COQ_POSTS:.v=.html) +COQ_ARTIFACTS := $(COQ_POSTS:.v=.vo) \ + $(COQ_POSTS:.v=.vok) \ + $(COQ_POSTS:.v=.vos) \ + $(COQ_POSTS:.v=.glob) \ + $(join $(dir ${COQ_POSTS}),$(addprefix ".",$(notdir $(COQ_POSTS:.v=.aux)))) coq-build : ${COQ_HTML} theme-build : site/style/coq.sass soupault-build : coq-build -ARTIFACTS += *.vo *.vok *.vos .*.aux *.glob .lia.cache +ARTIFACTS += ${COQ_ARTIFACTS} .lia.cache ARTIFACTS += ${COQ_HTML} COQLIB := "https://coq.inria.fr/distrib/current/stdlib/" diff --git a/site/cleopatra/literate-programming.org b/site/cleopatra/literate-programming.org new file mode 100644 index 0000000..7310864 --- /dev/null +++ b/site/cleopatra/literate-programming.org @@ -0,0 +1,42 @@ +#+BEGIN_EXPORT html +<h1>Literate Programming Projects</h1> +#+END_EXPORT + +#+BEGIN_SRC makefile :tangle literate-programming.mk +literate-programming-prebuild : + @cleopatra echo "Tangling" "literate programming project" + @cleopatra exec -- cleopatra-run-elisp export-lp.el >> build.log + +org-build : literate-programming-build + +COQFFI_ARCHIVE := site/files/coqffi-tutorial.tar.gz + +coqffi-tutorial-build : literate-programming-prebuild + @cleopatra echo "Building" "coqffi tutorial" + @cd lp/coqffi-tutorial; dune build --display quiet + @cleopatra echo "Archiving" "coqffi tutorial" + @rm -f ${COQFFI_ARCHIVE} + @tar --exclude="_build" -czvf ${COQFFI_ARCHIVE} lp/coqffi-tutorial >> build.log + +literate-programming-build : coqffi-tutorial-build + +ARTIFACTS += lp/ ${COQFFI_ARCHIVE} site/posts/deps.svg + +#+END_SRC + +#+BEGIN_SRC emacs-lisp :tangle export-lp.el +(cleopatra:configure) + +(org-babel-do-load-languages + 'org-babel-load-languages + '((shell . t))) + +(setq org-publish-project-alist + '(("lp" + :base-directory "site/posts" + :publishing-directory "lp" + :recursive t + :publishing-function cleopatra:tangle-publish))) + +(org-publish-all) +#+END_SRC diff --git a/site/cleopatra/org.org b/site/cleopatra/org.org index e6f7a9a..9c2728b 100644 --- a/site/cleopatra/org.org +++ b/site/cleopatra/org.org @@ -9,6 +9,8 @@ (use-package haskell-mode :ensure t :defer t) (use-package toml-mode :ensure t :defer t) (use-package json-mode :ensure t :defer t) +(use-package proof-general :ensure t :defer t) +(use-package tuareg :ensure t :defer t) (use-package github-modern-theme :ensure t :defer t :init (load-theme 'github-modern t)) @@ -17,9 +19,13 @@ #+BEGIN_SRC emacs-lisp :tangle scripts/export-org.el (cleopatra:configure) +(setq org-html-doctype "html5") +(setq org-html-html5-fancy t) + (org-babel-do-load-languages 'org-babel-load-languages - '((shell . t))) + '((shell . t) + (dot . t))) (setq org-export-with-toc nil) @@ -28,37 +34,6 @@ (add-to-list 'org-entities-user '("mi" "\\)" nil "</span>" "" "" "")) -(setq org-babel-exp-code-template - (concat "#+BEGIN_SRC %lang%switches%flags " - ":tangle %tangle :name %name\n" - "%body\n" - "#+END_SRC")) - -(defun cleopatra-html-src-block (oldfun src-block contents info) - (let* - ((old-ret (funcall oldfun src-block contents info)) - (pars (org-babel-parse-header-arguments - (org-element-property :parameters src-block))) - (tangle (cdr (assoc :tangle pars))) - (name (cdr (assoc :name pars)))) - (cond - (name - (concat - "<div class=\"org-literate-programming\">" - (format "<div class=\"org-src-name\"><<%s>> :=</div>" name) - old-ret - "</div>")) - ((not (string= tangle "no")) - (concat - "<div class=\"org-literate-programming\">" - old-ret - (format "<div class=\"org-src-tangled-to\">%s</div>" tangle) - "</div>")) - (t old-ret)))) - -(advice-add 'org-html-src-block - :around #'cleopatra-html-src-block) - (org-html-export-to-html nil nil nil t) #+END_SRC @@ -73,6 +48,7 @@ org-build : ${ORG_HTML} theme-build : site/style/org.sass soupault-build : org-build +org-build : literate-programming-build ARTIFACTS += ${ORG_HTML} CONFIGURE += .emacs diff --git a/site/cleopatra/soupault.org b/site/cleopatra/soupault.org index 02fe7f4..e7de9bf 100644 --- a/site/cleopatra/soupault.org +++ b/site/cleopatra/soupault.org @@ -648,7 +648,7 @@ consequence, we systematically ~touch~ ~packase-lock.json~ to satisfy ~make~. #+BEGIN_SRC makefile :tangle katex.mk package-lock.json : package.json - @echo " init npm packages" + @cleopatra echo "Fetching" "npm packages" @npm install &>> build.log @touch $@ diff --git a/site/index.org b/site/index.org index 263395e..ea0d27b 100644 --- a/site/index.org +++ b/site/index.org @@ -52,6 +52,12 @@ machine-checked proofs. means the definitions of ~+~ and ~*~ have to satisfy properties such as commutativity or the existence of neutral elements. +- [[./posts/Coqffi.org][A Series on ~coqffi~]] :: + ~coqffi~ generates Coq FFI modules from compiled OCaml interface + modules (~.cmi~). In practice, it greatly reduces the hassle to mix + together OCaml and Coq modules within the same codebase, especially + when used together with the ~build~ build system. + * About Haskell Haskell is a pure, lazy, functional programming language with a very expressive diff --git a/site/posts/CleopatraV1.org b/site/posts/CleopatraV1.org index 11d796b..ee5789d 100644 --- a/site/posts/CleopatraV1.org +++ b/site/posts/CleopatraV1.org @@ -78,7 +78,7 @@ In a nutshell, For this website, these constants are defined as follows. -#+BEGIN_SRC makefile :tangle Makefile :noweb no-export +#+BEGIN_SRC makefile :noweb no-export ROOT := $(shell pwd) CLEODIR := site/cleopatra #+END_SRC @@ -94,7 +94,7 @@ and providing rules to remove them. Long-term artifacts whose generation can be time consuming. They will only be removed by ~make cleanall~. -#+BEGIN_SRC makefile :tangle Makefile +#+BEGIN_SRC makefile ARTIFACTS := build.log CONFIGURE := #+END_SRC @@ -114,7 +114,7 @@ deleted with ~make clean~ for instance). However, it is overwritten. If you try to modify it and find that *~cleopatra~* does not work properly, you should restore it using ~git~. -#+BEGIN_SRC emacs-lisp :tangle scripts/tangle-org.el +#+BEGIN_SRC emacs-lisp (require 'org) (cd (getenv "ROOT")) (setq org-confirm-babel-evaluate nil) @@ -130,7 +130,7 @@ restore it using ~git~. We define variables that ensure that the ~ROOT~ environment variable is set and ~tangle-org.el~ is loaded when using Emacs. -#+BEGIN_SRC makefile :tangle Makefile +#+BEGIN_SRC makefile EMACSBIN := emacs EMACS := ROOT="${ROOT}" ${EMACSBIN} TANGLE := --batch \ @@ -142,7 +142,7 @@ Finally, we introduce a [[https://www.gnu.org/software/make/manual/html_node/Canned-Recipes.html#Canned-Recipes][canned recipe]] to seamlessly tangle a given file. -#+BEGIN_SRC makefile :tangle Makefile +#+BEGIN_SRC makefile define emacs-tangle = echo " tangle $<" ${EMACS} $< ${TANGLE} @@ -157,7 +157,7 @@ processes. This chain is divided into three stages: ~prebuild~, ~build~, and This translates as follows in ~Makefile~. -#+BEGIN_SRC makefile :tangle Makefile +#+BEGIN_SRC makefile default : postbuild ignore init : @@ -261,7 +261,7 @@ source block when the latter is tangled. We derive the rule to tangle ~bootstrap.mk~ using =extends=, which gives us the following Makefile snippet. -#+BEGIN_SRC makefile :tangle Makefile :noweb yes +#+BEGIN_SRC makefile :noweb yes <<extends(IN="Bootstrap.org", PROC="bootstrap", AUX="scripts/update-gitignore.sh")>> #+END_SRC @@ -287,7 +287,7 @@ Each generation process shall * Wrapping-up -#+BEGIN_SRC bash :tangle scripts/update-gitignore.sh :shebang "#+/bin/bash" +#+BEGIN_SRC bash :shebang "#+/bin/bash" BEGIN_MARKER="# begin generated files" END_MARKER="# begin generated files" @@ -305,7 +305,7 @@ done echo ${END_MARKER} >> .gitignore #+END_SRC -#+BEGIN_SRC makefile :tangle bootstrap.mk +#+BEGIN_SRC makefile ignore : @echo " update gitignore" @scripts/update-gitignore.sh \ diff --git a/site/posts/Coqffi.org b/site/posts/Coqffi.org new file mode 100644 index 0000000..7937901 --- /dev/null +++ b/site/posts/Coqffi.org @@ -0,0 +1,17 @@ +#+BEGIN_EXPORT html +<h1>A Series on <code>coqffi</code></h1> +#+END_EXPORT + +~coqffi~ generates Coq FFI modules from compiled OCaml interface +modules (~.cmi~). In practice, it greatly reduces the hassle to mix +together OCaml and Coq modules within the same codebase, especially +when used together with the ~build~ build system. + +- [[./CoqffiIntro.org][~coqffi~ in a Nutshell]] :: + For each entry of a ~cmi~ file, ~coqffi~ tries to generate an + equivalent (from the extraction mechanism perspective) Coq + definition. In this article, we walk through how ~coqffi~ works. +- [[./CoqffiEcho.org][Implementing an Echo Server in Coq with ~coqffi~]] :: + In this tutorial, 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. 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 diff --git a/site/posts/CoqffiIntro.org b/site/posts/CoqffiIntro.org new file mode 100644 index 0000000..dc76940 --- /dev/null +++ b/site/posts/CoqffiIntro.org @@ -0,0 +1,310 @@ +#+BEGIN_EXPORT html +<h1><code>coqffi</code> in a Nutshell</h1> +#+END_EXPORT + +For each entry of a ~cmi~ file, ~coqffi~ tries to generate an +equivalent (from the extraction mechanism perspective) Coq +definition. In this article, we walk through how ~coqffi~ works. + +Note that we do not dive into the vernacular commands ~coqffi~ +generates. They are of no concern for ~coqffi~’s users. + +#+TOC: headlines 2 + +* Getting Started + +** Requirements + +The latest versiof of ~coqffi~ (~coqffi.1.0.0~beta2~ at the time of +writing) is compatible with OCaml ~4.08~ up to ~4.11~, and Coq ~8.12~. +If you want to use ~coqffi~, but have incompatible requirements of +your own, feel free to +[[https://github.com/coq-community/coqffi/issues][submit an issue]]. + +** Installing ~coqffi~ + +The recommended way to install ~coqffi~ is through the +[[https://coq.inria.fr/opam/www][Opam Coq Archive]], in the ~released~ +repository. If you haven’t activated this repository yet, you can use +the following bash command. + +#+BEGIN_SRC sh +opam repo add coq-released https://coq.inria.fr/opam/released +#+END_SRC + +Then, installing ~coqffi~ is as simple as + +#+BEGIN_SRC sh +opam install coq-coqffi +#+END_SRC + +You can also get the source from +[[https://github.com/coq-community/coqffi][the upstream ~git~ +repository]]. The ~README~ provides the necessary pieces of +information to build it from source. + +** Additional Dependencies + +One major difference between Coq and OCaml is that the former is pure, +while the latter is not. Impurity can be modelled in pure languages, +and Coq does not lack of frameworks in this respect. ~coqffi~ +currently supports two of them: +[[https://github.com/Lysxia/coq-simple-io][~coq-simple-io~]] and +[[https://github.com/ANSSI-FR/FreeSpec][FreeSpec]]. It is also +possible to use it with +[[https://github.com/DeepSpec/InteractionTrees][Interaction Trees]], +albeit in a less direct manner. + + +* Primitives Types + +~coqffi~ supports a set of primitives types, /i.e./, a set of OCaml +types for which it knows an equivalent type in Coq. The list is the +following (the Coq types are fully qualified in the table, but not in +the generated Coq module as the necessry ~Import~ statement are +generated too). + +| Ocaml type | Coq type | +|-------------+-------------------------------| +| =bool= | =Coq.Init.Datatypes.bool= | +| =char= | =Coq.Strings.Ascii.ascii= | +| =int= | =CoqFFI.Data.Int.i63= | +| ='a list= | =Coq.Init.Datatypes.list a= | +| ='a option= | =Coq.Init.Datatypes.option a= | +| =string= | =Coq.Strings.String.string= | +| =unit= | =Coq.Init.Datatypes.unit= | + +The =i63= type is introduced by the =CoqFFI= theory to provide signed +primitive integers to Coq users. They are implemented on top of the +(sadly unsigned) Coq native integers introduced in Coq +~8.10~. Hopefully, the =i63= type will be deprecated once [[https://github.com/coq/coq/pull/13559][signed +primitive integers find their way to Coq upstream]]. + +When processing the entries of a given interface model, ~coqffi~ will +checks that they only use these types, or types introduced by the +interface module itself. + +* Code Generation + +~coqffi~ distinguishes three types of entries: +types, pure functions, and impure primitives. We now discuss how each +one of them are handled. + +** Types + +By default, ~coqffi~ generates axiomatized definitions for each type +defined in a ~cmi~ files. This means that src_ocaml[:exports +code]{type t} becomes src_coq[:exports code]{Axiom t : Type}. +Polymorphism is supported, /i.e./, src_ocaml[:exports code]{type 'a t} +becomes src_coq[:exports code]{Axiom t : forall (a : Type), Type}. + +It is possible to provide a “model” for a type using the =coq_model= +annotation, for instance for reasoning purposes. For instance, +we can specify that a type is equivalent to a =list=. + +#+BEGIN_SRC ocaml +type 'a t [@@coq_model "list"] +#+END_SRC + +This generates the following Coq definition. + +#+BEGIN_SRC coq +Definition t : forall (a : Type), Type := list. +#+END_SRC + +It is important to be careful when using the =coq_model= annotation. +More precisely, the fact that =t= is a =list= in the “Coq universe” +shall not be used while the implementation phase, only the +verification phase. + +Finally, ~coqffi~ has got an experimental feature called +~transparent-types~ (enable by using the ~-ftransparent-types~ +command-line argument). If the type definition is given in the module +interface, then ~coqffi~ tries to generates an equivalent definition +in Coq. For instance, + +#+BEGIN_SRC ocaml +type 'a llist = + | LCons of 'a * (unit -> 'a llist) + | LNil +#+END_SRC + +becomes + +#+BEGIN_SRC coq +Inductive llist (a : Type) : Type := +| LCons (x0 : a) (x1 : unit -> llist a) : llist a +| LNil : llist a. +#+END_SRC + +Mutually recursive types are supported, so + +#+BEGIN_SRC ocaml +type even = Zero | ESucc of odd +and odd = OSucc of even +#+END_SRC + +becomes + +#+BEGIN_SRC coq +Inductive odd : Type := +| OSucc (x0 : even) : odd +with even : Type := +| Zero : even +| ESucc (x0 : odd) : even. +#+END_SRC + +The ~transparent-types~ feature is *experimental*, and is currently +limited to variant types. It notably does not support +records. Besides, it may generate incorrect Coq types, because it does +not check whether or not the +[[https://coq.inria.fr/refman/language/core/inductive.html#positivity-condition][positivity +condition]] is satisfied. + +** Pure Functions + +~coqffi~ assumes OCaml values are pure by default, and will generate +regular axiomatized Coq definitions for them. Similarly to type +entries, it is possible to provide a Coq model using the =coq_module= +annotation. + +#+BEGIN_SRC ocaml +val unpack : string -> (char * string) option +#+END_SRC + +becomes + +#+BEGIN_SRC coq +Axiom unpack : string -> option (ascii * string). +#+END_SRC + +Polymorphic functions are supported. + +#+BEGIN_SRC ocaml +val map : ('a -> 'b) -> 'a list -> 'b list +#+END_SRC + +becomes + +#+BEGIN_SRC coq +Axiom map : forall (a : Type) (b : Type), (a -> b) -> list a -> list b. +#+END_SRC + +** Impure Primitives + +Finally, ~coqffi~ reserves a special treatment for OCaml value +explicitely marked as impure, using the =impure= annotation. Impurity +is usually handled in pure programming languages by means of monads, +and ~coqffi~ is no exception to the rule. + +Given the set of impure primitives declared in an interface module, +~coqffi~ will (1) generates a typeclass which gathers these +primitives, and (2) generates instances of this typeclass for +supported backends. + +We illustrate the rest of this section with the following impure +primitives. + +#+BEGIN_SRC ocaml +val echo : string -> unit [@@impure] +val scan : unit -> string [@@impure] +#+END_SRC + +where =echo= allows to write something the standard output, and =scan= +to read the standard input. + +Assuming the processed module interface is named ~console.mli~, the +following Coq typeclass is generated. + +#+BEGIN_SRC coq +Class MonadConsole (m : Type -> Type) := { echo : string -> m unit + ; scan : unit -> m string + }. +#+END_SRC + +Using this typeclass and with the additional support of an additional +=Monad= typeclass, we can specify impure computations which interacts +with the console. For instance, with the support of ~ExtLib~, one can +write. + +#+BEGIN_SRC coq +Definition pipe `{Monad m, MonadConsole m} : m unit := + let* msg := scan () in + echo msg. +#+END_SRC + +There is no canonical way to model impurity in Coq, but over the years +several frameworks have been released to tackle this challenge. + +~coqffi~ provides three features related to impure primitives. + +*** ~simple-io~ + +This feature allows to generate an instance of the typeclass for the +=IO= monad introduced in the ~coq-simple-io~ package + +#+BEGIN_SRC coq +Axiom io_echo : string -> IO unit. +Axiom io_scan : unit -> IO string. + +Instance IO_MonadConsole : MonadConsole IO := { echo := io_echo + ; scan := io_scan + }. +#+END_SRC + +It is enabled by default, but can be disabled using the +~-fno-simple-io~ command-line argument. + +*** ~interface~ + +This feature allows to generate an inductive type which describes the +set of primitives available, to be used with frameworks like +[[https://github.com/ANSSI-FR/FreeSpec][FreeSpec]] or +[[https://github.com/DeepSpec/InteractionTrees][Interactions Trees]] + +#+BEGIN_SRC coq +Inductive CONSOLE : Type -> Type := +| Echo : string -> CONSOLE unit +| Scan : unit -> CONSOLE string. + +Definition inj_echo `{Inject CONSOLE m} (x0 : string) : m unit := + inject (Echo x0). + +Definition inj_scan `{Inject CONSOLE m} (x0 : unit) : m string := + inject (Scan x0). + +Instance Inject_MonadConsole `{Inject CONSOLE m} : MonadConsole m := + { echo := inj_echo + ; scan := inj_scan + }. +#+END_SRC + +Providing an instance of the form src_coq[:exports code]{forall i, +Inject i M} is enough for your monad =M= to be compatible with this +feature (see for instance +[[https://github.com/ANSSI-FR/FreeSpec/blob/master/theories/FFI/FFI.v][how +FreeSpec implements it]]). + +*** ~freespec~ + +It allows to generate a semantics for the inductive type generated by +the ~interface~ feature. + +#+BEGIN_SRC coq +Axiom unsafe_echo : string -> unit. +Axiom unsafe_scan : uint -> string. + +Definition console_unsafe_semantics : semantics CONSOLE := + bootstrap (fun a e => + local match e in CONSOLE a return a with + | Echo x0 => unsafe_echo x0 + | Scan x0 => unsafe_scan x0 + end). +#+END_SRC + +* Moving Forward + +~coqffi~ comes with a comprehensive man page. In addition, the +interested reader can proceed to the next article of this series, +which explains how [[./CoqffiEcho.org][~coqffi~ can be used to easily +implement an echo server in Coq]]. |