Simplify the theme

9 files changed, 184 insertions, 1403 deletions

diff --git a/.gitignore b/.gitignore
index 2d03d68..3425c78 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,29 +1,29 @@
 
 # begin generated files
 .cleopatra
-coq.mk
 site/style/coq.sass
+coq.mk
 .emacs
+site/style/org.sass
+org.mk
 scripts/export-org.el
 scripts/packages.el
-org.mk
-site/style/org.sass
 package-lock.json
 node_modules/
-soupault.conf
+scripts/katex.js
+soupault.mk
+katex.mk
+package.json
+scripts/history.sh
+templates/history.html
+site/style/plugins.sass
 plugins/external-urls.lua
 plugins/urls-rewriting.lua
 plugins/fix-org-urls.lua
-site/style/plugins.sass
-templates/history.html
-scripts/history.sh
-package.json
-soupault.mk
-katex.mk
-scripts/katex.js
-theme.mk
-templates/main.html
+soupault.conf
 site/style/main.sass
+templates/main.html
+theme.mk
 build.log
 *.vo
 *.vok
@@ -31,26 +31,25 @@ build.log
 .*.aux
 *.glob
 .lia.cache
-site/posts/AlgebraicDatatypes.html
-site/posts/StronglySpecifiedFunctionsProgram.html
-site/posts/MiniHTTPServer.html
-site/posts/ClightIntroduction.html
-site/posts/StronglySpecifiedFunctions.html
 site/posts/RewritingInCoq.html
-site/posts/Ltac101.html
+site/posts/StronglySpecifiedFunctions.html
+site/posts/AlgebraicDatatypes.html
 site/posts/MixingLtacAndGallina.html
-site/index.html
+site/posts/Ltac101.html
+site/posts/ClightIntroduction.html
+site/posts/StronglySpecifiedFunctionsProgram.html
 site/news/ColorlessThemes-0.2.html
 site/cleopatra/soupault.html
-site/cleopatra/theme.html
 site/cleopatra/org.html
 site/cleopatra/coq.html
-site/cleopatra.html
-site/posts/Thanks.html
-site/posts/DiscoveringCommonLisp.html
+site/cleopatra/theme.html
 site/posts/ExtensibleTypeSafeErrorHandling.html
+site/posts/DiscoveringCommonLisp.html
 site/posts/MonadTransformers.html
 site/posts/CleopatraV1.html
+site/posts/Thanks.html
+site/cleopatra.html
+site/index.html
 build/
 site/style/main.css
 # end generated files
diff --git a/Makefile b/Makefile
deleted file mode 100644
index 2682086..0000000
--- a/Makefile
+++ /dev/null
@@ -1,49 +0,0 @@
-ROOT := $(shell pwd)
-CLEODIR := site/cleopatra
-
-ARTIFACTS := build.log
-CONFIGURE :=
-
-EMACSBIN := emacs
-EMACS := ROOT="${ROOT}" ${EMACSBIN}
-TANGLE := --batch \
-          --load="${ROOT}/scripts/tangle-org.el" \
-          2>> build.log
-
-define emacs-tangle =
-echo "  tangle  $<"
-${EMACS} $< ${TANGLE}
-endef
-
-default : postbuild ignore
-
-init :
-	@rm -f build.log
-
-prebuild : init
-
-build : prebuild
-
-postbuild : build
-
-.PHONY : init prebuild build postbuild ignore
-
-include bootstrap.mk
-
-prebuild : bootstrap-prebuild
-build : bootstrap-build
-postbuild : bootstrap-postbuild
-
-bootstrap-prebuild : bootstrap.mk scripts/update-gitignore.sh
-bootstrap-build : bootstrap-prebuild
-bootstrap-postbuild : bootstrap-build
-
-bootstrap.mk scripts/update-gitignore.sh &:\
-   ${CLEODIR}/Bootstrap.org
-	@$(emacs-tangle)
-
-CONFIGURE += bootstrap.mk scripts/update-gitignore.sh
-
-.PHONY : bootstrap-prebuild \
-         bootstrap-build \
-         bootstrap-postbuild
diff --git a/site/cleopatra/coq.org b/site/cleopatra/coq.org
index 51b0ecb..7f617e8 100644
--- a/site/cleopatra/coq.org
+++ b/site/cleopatra/coq.org
@@ -28,80 +28,52 @@ COQDOCARG := --no-index --charset utf8 --short \
 #+END_SRC
 
 #+BEGIN_SRC sass :tangle site/style/coq.sass
-@mixin patchy-centered($inc: 0rem)
-    width : 100vw
-    position: relative
-    @media screen and (min-width : $document-width)
-        padding-left : calc(50vw - #{$document-width} / 2)
-        right : calc(50vw - #{$document-width} / 2)
-    @media screen and (max-width : $document-width)
-        padding-left : 1rem
-        right : 1rem
-
 div.code
     white-space: nowrap
+    line-height : 140%
 
-.coq-text-block
-    @include patchy-centered
-    padding-top: 1rem
-    padding-bottom: 1rem
-
-.doc
-    @include padding-centered
-    margin-top : 1em
-    margin-bottom : 1em
-
-    pre
-        @include patchy-centered
-        padding-top : 1rem
-        padding-bottom : 1rem
-        background : $bg-verbatim
-        overflow-x : auto
+div.code,
+span.inlinecode
+    font-family : 'Fira Code', monospace
+    font-size : 80%
 
-.code
-    @include padding-centered
-    @include code-block
-
-.inlinecode
-    @include code-font
+div.doc
+    max-width : 35rem
+    line-height : 140%
 
-h1, h2, h3, h4, h5, h6
-    .inlinecode
-        font-size: 100%
+.paragraph
+    margin-bottom : .8em
+#+END_SRC
 
+#+BEGIN_SRC sass :tangle site/style/coq.sass
 .code
     .id[title="keyword"]
-        color : #ff6188
+        color : #d73a49
 
     .id[title="definition"],
     .id[title="projection"],
     .id[title="theorem"],
     .id[title="lemma"]
-        color : #a9dc76
+        color : #6f42c1
 
     .id[title="inductive"],
     .id[title="record"],
     .id[title="axiom"],
     .id[title="class"]
-        color : #78dce8
+        color : #005cc5
 
     .id[title="constructor"]
-        color : #ab9df2
+        color : #e36209
 
     a[href]
         color : inherit
         text-decoration : none
-        background : #403e41
-        padding : .05rem .15rem .05rem .15rem
+        background : #f7f7f7
+        padding : .1rem .15rem .1rem .15rem
         border-radius : 15%
 
         .url-mark
             display: none
-
-.paragraph
-    margin-top: 1em
-    margin-bottom: 1em
-
 #+END_SRC
 
 # Local Variables:
diff --git a/site/cleopatra/org.org b/site/cleopatra/org.org
index b846ee8..df6c513 100644
--- a/site/cleopatra/org.org
+++ b/site/cleopatra/org.org
@@ -9,9 +9,9 @@
 (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 monokai-pro-theme :ensure t :defer t
+(use-package github-modern-theme :ensure t :defer t
   :init
-  (load-theme 'monokai-pro t))
+  (load-theme 'github-modern t))
 #+END_SRC
 
 #+BEGIN_SRC emacs-lisp :tangle scripts/export-org.el
@@ -97,21 +97,8 @@ INIT := --batch --load="${ROOT}/scripts/packages.el" \
 #+END_SRC
 
 #+BEGIN_SRC sass :tangle site/style/org.sass
-.org-src-container
-    @include code-block
-    padding-top : .1rem
-    padding-bottom : .1rem
-
-.org-src-tangled-to, .org-src-name
-    @include padding-centered(4rem)
-
-.example
-    @include verbatim-block
-    // this is hacky, but it works: no need for a padding-bottom
-    padding-top : 1rem
-
-.footdef
-    @include padding-centered
+#text-footnotes
+    max-width : 35rem
 
 .footpara
     display: inline
@@ -127,27 +114,23 @@ INIT := --batch --load="${ROOT}/scripts/packages.el" \
     display: none
 
 dl
-  dt
-    font-weight: bold
-  dd p
-    margin-top: 0
+    dt
+        font-weight: bold
+    dd p
+        margin-top: 0
 
 .footnotes
-  font-size : 1rem
+    font-size : 1rem
 
 .org-literate-programming
-  padding-top : 1rem
-  padding-bottom : 1rem
-  .org-src-name
-    @include code-font
-    font-weight: bold
-
-  .org-src-tangled-to:before
-    content: "\f054"
-    font : normal normal normal 14px/1 ForkAwesome
-
-  .org-src-tangled-to
-    @include code-font
-    font-weight: bold
-    text-align: right
+    .org-src-tangled-to:before
+        content: "\f054"
+        font : normal normal normal 11px/1 ForkAwesome
+
+    .org-src-tangled-to,
+    .org-src-name
+        font-family : 'Fira Code', monospace
+        font-size : 70%
+        font-weight: bold
+        color : #444
 #+END_SRC
diff --git a/site/cleopatra/soupault.org b/site/cleopatra/soupault.org
index fb2c57c..0675ae7 100644
--- a/site/cleopatra/soupault.org
+++ b/site/cleopatra/soupault.org
@@ -361,7 +361,14 @@ https://code.soap.coffee/writing/lthms.git
   <table>
   {{#history}}
   <tr>
-    <td class="date"{{#created}} id="created-at"{{/created}}{{#modified}} id="modified-at"{{/modified}}>
+    <td class="date"
+{{#created}}
+        id="created-at"
+{{/created}}
+{{#modified}}
+        id="modified-at"
+{{/modified}}
+        >
       {{date}}
     </td>
     <td class="subject">{{subject}}</td>
@@ -377,26 +384,21 @@ https://code.soap.coffee/writing/lthms.git
 #+END_SRC
 
 #+BEGIN_SRC sass :tangle site/style/plugins.sass
-#history
-  table
-    @include margin-centered(2rem)
-    border-top: 2px solid $primary-color
-    border-bottom: 2px solid $primary-color
-    border-collapse: collapse;
-
-  td
-    border-bottom: 1px solid $primary-color
-    padding: .5em
-    vertical-align: top
-
-  td.commit
-    font-size: smaller
-
-  td.commit
-    font-family: 'Fira Code', monospace
-    color: $code-fg-color
-    font-size: 80%
-    white-space: nowrap;
+table
+    border-top : 2px solid black
+    border-bottom : 2px solid black
+    border-collapse : collapse
+    max-width : 35rem
+
+td
+    border-bottom : 1px solid black
+    padding : .5em
+
+#history .commit
+    font-size : smaller
+    font-family : 'Fira Code', monospace
+    width : 7em
+    text-align : center
 #+END_SRC
 
 *** Implementation
diff --git a/site/cleopatra/theme.org b/site/cleopatra/theme.org
index 35f13b4..4c2ea26 100644
--- a/site/cleopatra/theme.org
+++ b/site/cleopatra/theme.org
@@ -29,35 +29,24 @@ ARTIFACTS += ${CSS}
 #+NAME: head
 #+BEGIN_SRC html :noweb no-export
 <head>
-  <<encoding>>
-  <<viewport>>
+  <meta charset="utf-8">
+  <meta name="viewport"
+        content="width=device-width, initial-scale=1.0">
   <title></title>
   <<syncloading_html>>
   <<asyncloading_html>>
 </head>
 #+END_SRC
 
-*** Encoding
-
-#+NAME: encoding
-#+BEGIN_SRC html
-<meta charset="utf-8">
-#+END_SRC
-
-*** Viewport
-
-#+NAME: viewport
-#+BEGIN_SRC html
-<meta name="viewport"
-      content="width=device-width, initial-scale=1.0">
-#+END_SRC
-
 *** Assets Loading
 
 #+NAME: syncloading_html
 #+BEGIN_SRC html
+<link
+   href="https://soap.coffee/+vendors/normalize.css.8.0.1/normalize.css"
+   rel="stylesheet">
 <link rel="stylesheet" href="/style/main.css">
-<link rel="icon" type="image/ico"  href="/img/merida.webp">
+<link rel="icon" type="image/ico" href="/img/merida.webp">
 #+END_SRC
 
 #+NAME: asyncloading_js
@@ -71,13 +60,13 @@ noscript.parentNode.removeChild(noscript);
 #+BEGIN_SRC html
 <noscript id="asyncloading">
   <link href="https://soap.coffee/+vendors/fira-code.2+swap/font.css"
-     rel="stylesheet">
+        rel="stylesheet">
   <link href="https://soap.coffee/+vendors/et-book+swap/font.css"
-     rel="stylesheet">
+        rel="stylesheet">
   <link href="https://soap.coffee/+vendors/katex.0.11.1+swap/katex.css"
-     rel="stylesheet">
+        rel="stylesheet">
   <link href="https://soap.coffee/+vendors/fork-awesome.1.1.7+swap/css/fork-awesome.min.css"
-     rel="stylesheet">
+        rel="stylesheet">
 </nolink>
 #+END_SRC
 
@@ -86,20 +75,38 @@ noscript.parentNode.removeChild(noscript);
 #+NAME: body
 #+BEGIN_SRC html :noweb no-export
 <body id="default">
-  <nav>
+  <header>
     <ul>
       <li> <a href="/news">News</a></li>
-      <li> <a href="/">Write-ups</a></li>
+      <li> <a href="/">Technical Articles</a></li>
+      <li> <a href="/projects">Projects</a></li>
     </ul>
-  </nav>
-  <header>
-    <img src="/img/merida.webp"
-         alt="Merida in the movie Ralph 2.0" />
   </header>
   <main>
   <!-- your page content will be inserted here,
        see the content_selector option in soupault.conf -->
   </main>
+  <footer>
+    <img src="https://soap.coffee/~lthms/img/merida.webp"
+         alt="Merida from the movie Ralph 2.0 from Disney is the
+              avatar I use most of the time on the Internet"
+         title="lthms’ avatar" />
+
+    <p>
+      Hi, I’m <strong>lthms</strong>, and this is my humble corner of the
+      Internet. You are very welcome here! If you are interested in
+      <em>functional programming</em>, <em>formal verification</em>, or <em>free
+      software projects in the making</em>, you may even enjoy your stay!
+    </p>
+
+    <p>
+      This website has been generated using a collection of
+      <a href="/posts/Thanks.html">awesome free software projects</a>. You can
+      have a look at <a href="https://code.soap.coffee/writing/lthms">the source
+      of this webpage</a>, and if you have find an error, feel free to <a
+      href="mailto:">shoot me an email</a>.
+    </p>
+  </footer>
   <script>
     <<asyncloading_js>>
   </script>
@@ -109,184 +116,61 @@ noscript.parentNode.removeChild(noscript);
 * Main SASS File
 
 #+BEGIN_SRC sass :tangle site/style/main.sass
-$bg-color: #2d2a2e
-$bg-verbatim : #f4f4f4
-$code-fg-color: #fcfcfa
-$text-fg-color: #505050
-$primary-color: black
-$todo-bg: #e4d3b3
-$todo-fg: #2f2b24
-$remark-bg: #c5dbe2
-$remark-fg: #4d575e
-
-$sans-serif : sans-serif
-
-$document-width : 38rem
-
-a
-    color : #557de8
-a:visited
-    color : #40599a
-
-@mixin padding-centered($inc: 0rem)
-    @media screen and (min-width : $document-width)
-        padding-left : calc(50% - #{$document-width} / 2 - #{$inc})
-        padding-right : calc(50% - #{$document-width} / 2 - #{$inc})
-    @media screen and (max-width : $document-width)
-        padding-left : 1rem
-        padding-right : 1rem
-
-@mixin margin-centered($inc: 0rem)
-    @media screen and (min-width : $document-width)
-        margin-left : calc(50% - #{$document-width} / 2 - #{$inc})
-        margin-right : calc(50% - #{$document-width} / 2 - #{$inc})
-    @media screen and (max-width : $document-width)
-        margin-left : 1rem
-        margin-right : 1rem
-
-@mixin text-font
-    font-family : serif
-
-@mixin code-font($size : .8em)
-    font-family: 'Fira Code', monospace
-    font-size: $size
-
-@mixin code-block
-    @include padding-centered
-    @include code-font
-    background : $bg-color
-    color : $code-fg-color
-    overflow-x : auto
-    scrollbar-width : thin
-
-@mixin verbatim-block
-    @include padding-centered
-    @include code-font
-    background : $bg-verbatim
-    overflow-x : auto
-    scrollbar-width : thin
-
 *
-  box-sizing: border-box
+    box-sizing : border-box
 
-html, body
-    margin : 0
-    padding : 0
+html
     width : 100%
-    height : 100%
-    font-size : 115%
-    @include text-font
+    font-size : 100%
 
 body
-    overflow-x : hidden
-
-code, tt
-    @include code-font
-
+    padding : 2rem
+
+main p,
+main h1,
+main h2,
+main h3,
+main h4,
+main h5,
+main h6,
+main ul,
+main dl,
+main ol,
+header,
+footer
+    max-width : 35rem
+    line-height : 140%
+
+header ul,
+footer p
+    font-size : 90%
+
+header ul
+    padding : 0
+    margin : 0
+    list-style-type : none
+    display : flex
+    gap : 1rem
+
+main
+    padding-top : 1rem
+    padding-bottom : 1rem
+
+footer img
+    border-radius : 100%
+    max-width : 7rem
+    float : right
+    margin-left : 1rem
+    margin-bottom : 1rem
+
+code,
+tt,
 pre
-    @include code-font
-
-body#default
-    nav
-        @include margin-centered
-        padding-top : 1rem
-        padding-bottom : 1rem
-
-        ul
-            padding : 0
-            margin : 0
-            width : 100%
-            display : flex
-            flex-direction : row
-            justify-content : center
-            list-style-type : none
-
-            li
-                padding-left: .5em
-                padding-right: .5em
-                text-transform: uppercase
-                font-family: sans-serif
-                font-weight: bold
-
-                a
-                    text-decoration: none
-
-    header
-        text-align: center
-
-        img
-            text-align: center
-            border-radius: 50%
-            width: 150px
-
-    main
-        h1
-            text-align: center
-
-        h2, h3, h4, h5, h6
-            font-style: italic
-
-
-            code, tt
-                font-size: 100%
-
-        h1, h2, h3, h4, h5, h6, p, summary
-            @include padding-centered
-
-        dl, ul, ol
-            @include margin-centered
-
-        .TODO
-            background : $todo-bg
-            color : $todo-fg
-            padding-top : .1rem
-            padding-bottom : .1rem
-            margin-top : 1rem
-            margin-bottom : 1rem
-
-        @import coq, org
-
-.index
-    dt
-        font-weight : bold
-        color : $primary-color
-
-    dd
-        margin-left : 0
-        margin-bottom : 1em
-
-        ol
-            margin-top: 0.3em
+    font-family : 'Fira Code', monospace
+    font-size : 80%
+    line-height : 140%
 
 @import plugins
-
-/* VCARD (index.html) */
-body#vcard
-    display: flex
-    align-items: center
-    flex-direction: column
-    font-size: 125%
-
-    article
-        max-width: 400px
-        width: 80%
-        margin: auto
-
-        img
-            display: block
-            border-radius: 50%
-            width: 175px
-            margin: auto
-            margin-bottom: 3em
-
-    h1
-        color: $primary-color
-        font-size: 300%
-        text-align: center
-
-    nav dt
-        font-weight: bold
-
-        a
-            color: $primary-color
+@import org
+@import coq
 #+END_SRC
diff --git a/site/index.org b/site/index.org
index 6c7e36d..ff77c3d 100644
--- a/site/index.org
+++ b/site/index.org
@@ -1,7 +1,7 @@
 #+OPTIONS: toc:nil num:nil
 
 #+BEGIN_EXPORT html
-<h1>Write-ups</h1>
+<h1>Technical Articles</h1>
 
 <article class="index">
 #+END_EXPORT
@@ -20,39 +20,35 @@ Coq is a formal proof management system which provides a pure functional
 language with nice dependent types together with an environment for writing
 machine-checked proofs.
 
-- [[./posts/AlgebraicDatatypes.html][Proving Algebraic Datatypes are “Algebraic”]] ::
-  The set of types which can be defined in a language together with ~+~ and ~*~
-  form an “algebraic structure” in the mathematical sense, hence the name. It
-  means the definitions of ~+~ and ~*~ have to satisfy properties such as
-  commutativity or the existence of neutral elements.
-
-- [[./posts/ClightIntroduction.html][A Study of Clight and its Semantics]] ::
-  Clight is a “simplified” C AST used by CompCert, the certified C compiler. In
-  this write-up, we prove a straighforward functional property of a small C
-  function, as an exercise to discover the Clight semantics.
+- A Series on Strongly-Specified Funcions in Coq ::
+  Coq ~Prop~ sort allows for defining properties function arguments have to
+  satisfy, such that using such a function requires providing a proof the
+  property is satisfied.
 
-- [[./posts/MiniHTTPServer.html][Implementing and Certifying a Web Server in Coq]] ::
-  An explanation on how to write an almost pure Coq, and working (albeit
-  minimal) HTTP server.
+  1. [[./posts/StronglySpecifiedFunctions.html][Using the ~refine~ Tactics]]
+  2. [[./posts/StronglySpecifiedFunctionsProgram.html][Using the ~Program~ Framework]]
 
 - A Series on Ltac ::
   Ltac is the “tactic language” of Coq. It allows for writing proof scripts
   which construct proof terms later checked by Coq.
 
   1. [[./posts/Ltac101.html][Ltac 101]]
-  1. [[./posts/MixingLtacAndGallina.html][Mixing Ltac and Gallina for Fun and Profit]]
+  2. [[./posts/MixingLtacAndGallina.html][Mixing Ltac and Gallina for Fun and Profit]]
 
 - [[./posts/RewritingInCoq.html][Rewriting in Coq]] ::
   The ~rewrite~ tactics are really useful, since they are not limited to the Coq
   built-in equality relation.
 
-- A Series on Strongly-Specified Funcions in Coq ::
-  Coq ~Prop~ sort allows for defining properties function arguments have to
-  satisfy, such that using such a function requires providing a proof the
-  property is satisfied.
+- [[./posts/ClightIntroduction.html][A Study of Clight and its Semantics]] ::
+  Clight is a “simplified” C AST used by CompCert, the certified C compiler. In
+  this write-up, we prove a straighforward functional property of a small C
+  function, as an exercise to discover the Clight semantics.
 
-  1. [[./posts/StronglySpecifiedFunctions.html][Using the ~refine~ Tactics]]
-  2. [[./posts/StronglySpecifiedFunctionsProgram.html][Using the ~Program~ Framework]]
+- [[./posts/AlgebraicDatatypes.html][Proving Algebraic Datatypes are “Algebraic”]] ::
+  The set of types which can be defined in a language together with ~+~ and ~*~
+  form an “algebraic structure” in the mathematical sense, hence the name. It
+  means the definitions of ~+~ and ~*~ have to satisfy properties such as
+  commutativity or the existence of neutral elements.
 
 * About Haskell
 
@@ -94,11 +90,6 @@ process.
   3. [[./cleopatra/org.org][Authoring Contents As Org Documents ~(TODO)~]]
   4. [[./cleopatra/soupault.org][Processing HTML with ~soupault~]]
 
-- [[./posts/Thanks.html][Thanks!]] ::
-  If it were not for many awesome FOSS projects, this corner of the Internet
-  would not exist. This is my attempt to give well-deserved credit to them and
-  their creators.
-
 - [[./posts/CleopatraV1.html][*~cleopatra~* the First]] ::
   This write-up is the literate program of the first version of *~cleopatra~*,
   before it became a command-line program implemented in Rust.
diff --git a/site/news/index.html b/site/news/index.html
index 1bbb731..1664aed 100644
--- a/site/news/index.html
+++ b/site/news/index.html
@@ -1,7 +1,5 @@
 <h1>News</h1>
 
-<h2>Hobbyist Projects</h2>
-
 <ul>
   <li>
     On <strong>April 17, 2020</strong>, my first contribution to
diff --git a/site/posts/MiniHTTPServer.v b/site/posts/MiniHTTPServer.v
deleted file mode 100644
index dda5841..0000000
--- a/site/posts/MiniHTTPServer.v
+++ /dev/null
@@ -1,999 +0,0 @@
-(** * Implementing and Certifying a Web Server in Coq *)
-
-(** This article has originally been published on #<span class="time">February
-02, 2020</span>#. *)
-
-(** FreeSpec is a general-purpose framework for implementing (with a Free monad)
-    and certifying (with contracts) impure computations. In this tutorial, we
-    will use FreeSpec to implement and certify a webserver we call
-    <<MiniHTTPServer>>. Our goal is to prove our HTTP server correctly uses the
-    filesystem, that is it reads from and closes valid file descriptors, and
-    closes all its file descriptors.
-
-    #<div id="generate-toc"></div>#
-
-    #<div id="history">site/posts/MiniHTTPServer.v</div>#
-
-    The [FreeSpec.Core] module reexports the key component provided by
-    FreeSpec. *)
-
-From FreeSpec.Core Require Import All.
-
-(** ** Implementation *)
-
-(** FreeSpec provides the [impure] monad to implement impure computations. This
-    monad is equipped with the necessary notations to write idiomatic momadic
-    code, thanks to the same notations as the ones introduced in recent versions
-    of OCaml.
-
-    The [impure] type takes two parameters respectively of type [interface] and
-    [Type]:
-
-      - An interface is a parameterized inductive type, whose constructors
-        identify impure primitives. For an interface [i], a term of type [i a]
-        identifies a primitive which produces a term of type [a]. An impure
-        computation of type [impure i a] can leverage primitives of the
-        interface [i].
-      - The second parameter of [impure] is the type of result returned by the
-        impure computation. Therefore, an impure computation of type [impure i a]
-        is expected to produce a result of type [a]. *)
-
-(** *** Defining Interfaces *)
-
-(** An [interface] is a parameterized inductive type whose constructors identify
-    impure primitives.
-
-    For our server, we anticipate the use of three “kinds” of primitives to:
-
-      - Create and manipulate TCP sockets
-      - Interact with the filesystem
-      - Interact with the console
-
-    Since an impure computation can use _several_ interfaces, FreeSpec favors
-    defining indendent primitives as part of different interfaces. In our case,
-    this means we will have three different interfaces. *)
-
-(** **** The [TCP] Interface *)
-
-(** We first consider the interface which will allows us to interact with TCP
-    sockets. The related primitives will rely on socket _descriptors_, whose
-    concrete implementaiton is opaque in most languages. We will introduce it as
-    an axiom. *)
-
-Axiom socket_descriptor : Type.
-
-(** Using [socket_descriptor], we can define the [TCP] type. *)
-
-Inductive TCP : interface :=
-
-(**   - [NewTCPSocket] is a primitive to create a socket. It takes as an argument
-        the address of the socket (of the form <<[url]:[port]>>) of type [bytestring]
-        (a type provided by the <<coq-prelude>> project with a convenient string
-        notation). It returns a [socket_descriptor] to interact with the newly
-        created socket. *)
-
-| NewTCPSocket (addr : bytestring)
-  : TCP socket_descriptor
-
-(**   - [ListenIncomingConnection] changes the mode of a given socket identified
-        by a [socket_descriptor], effectively creating a server. It returns
-        nothing, thus its type is [TCP unit]. *)
-
-| ListenIncomingConnection (socket : socket_descriptor)
-  : TCP unit
-
-(**   - [AcceptConnection] takes a [socket_descriptor] (in “listen incomming
-        connection” mode). The impure computation then waits until a client
-        initiate a connection, and when it happens, [AcceptConnection] returns a
-        new socket to interact with this client. Thus, the type of
-        [AcceptConnection] is [TCP socket_descriptor]. *)
-
-| AcceptConnection (socket : socket_descriptor)
-  : TCP socket_descriptor
-
-(**   - [ReadSocket] and [WriteSocket] allows to receive data from and send data
-        to the socket, that is interacting with the client. They also use the
-        [bytestring] type *)
-
-| ReadSocket (socket : socket_descriptor)
-  : TCP bytestring
-| WriteSocket (socket : socket_descriptor) (msg : bytestring)
-  : TCP unit
-
-(**   - Finally, [CloseTCPSocket] interrupts an existing connection by closing the
-        link between the server and the client.  *)
-
-| CloseTCPSocket (socket : socket_descriptor)
-  : TCP unit.
-
-(** Terms of type [TCP] are empty shell. They _identify_ a primitive, and
-    nothing more.  FreeSpec provides a helper named [request] to turn a
-    primitive identifier (that is, a term of type [i a]) into an impure
-    computation consisting in using the primitive and returning its result. The
-    type of [request] is really informing:
-
-<<
-request : forall `{Provide ix i} {a},
-            i a -> impure ix a
->>
-
-    The interface type of the impure computation created by [request] ([ix]) is
-    universally quantified, with only the restriction that [ix] provides at
-    least the primitives of [i]. The use of this bounded universal
-    quantification is to seemlessly compose impure computations using different
-    interfaces.
-
-    To reduce the verbosity of the impure computation verbosity, we use the
-    [Generalizable All Variables] feature of Coq. *)
-
-Generalizable All Variables.
-
-(** Then, for each constructor of [TCP], we create an impure computation with
-    the exact same arguments. This is cumbersome, but in future version of
-    FreeSpec we hope we will be able to provide helpers to generate them
-    automatically, thanks to the [MetaCoq] project. *)
-
-Definition new_tcp_socket `{Provide ix TCP}
-    (addr : bytestring)
-  : impure ix socket_descriptor :=
-  request (NewTCPSocket addr).
-
-Definition listen_incoming_connection `{Provide ix TCP}
-    (socket : socket_descriptor)
-  : impure ix unit :=
-  request (ListenIncomingConnection socket).
-
-Definition accept_connection `{Provide ix TCP}
-    (socket : socket_descriptor)
-  : impure ix socket_descriptor :=
-  request (AcceptConnection socket).
-
-Definition read_socket `{Provide ix TCP}
-    (socket : socket_descriptor)
-  : impure ix bytestring :=
-  request (ReadSocket socket).
-
-Definition write_socket `{Provide ix TCP}
-      (socket : socket_descriptor) (msg : bytestring)
-    : impure ix unit :=
-  request (WriteSocket socket msg).
-
-Definition close_socket `{Provide ix TCP}
-    (socket : socket_descriptor)
-  : impure ix unit :=
-  request (CloseTCPSocket socket).
-
-(** **** The [FILESYSTEM] Interface *)
-
-(** We provide a similar description of the [FILESYSEM] interface, and define
-    the basic impure computations that we will then leverage to use it (thanks
-    to the [request] helper of FreeSpec). *)
-
-Axiom file_descriptor : Type.
-
-Inductive FILESYSTEM : interface :=
-| Open (path : bytestring) : FILESYSTEM file_descriptor
-| FileExists (file : bytestring) : FILESYSTEM bool
-| Read (file : file_descriptor) : FILESYSTEM bytestring
-| Close (file : file_descriptor) : FILESYSTEM unit.
-
-Definition open `{Provide ix FILESYSTEM}
-    (path : bytestring)
-  : impure ix file_descriptor :=
-  request (Open path).
-
-Definition close `{Provide ix FILESYSTEM}
-    (fd : file_descriptor)
-  : impure ix unit :=
-  request (Close fd).
-
-Definition file_exists `{Provide ix FILESYSTEM}
-    (path : bytestring)
-  : impure ix bool :=
-  request (FileExists path).
-
-Definition read `{Provide ix FILESYSTEM}
-    (fd : file_descriptor)
-  : impure ix bytestring :=
-  request (Read fd).
-
-(** **** The [CONSOLE] Interface *)
-
-Inductive CONSOLE : interface :=
-| Scan : CONSOLE bytestring
-| Echo : bytestring -> CONSOLE unit.
-
-Definition scan `{Provide ix CONSOLE} : impure ix bytestring :=
-  request Scan.
-
-Definition echo `{Provide ix CONSOLE} (msg : bytestring) : impure ix unit :=
-  request (Echo msg).
-
-(** *** Implementing a HTTP Server *)
-
-(** With the three interfaces we have defined in the previous section, we can
-    now implement <<MiniHTTPServer>>, that is a minimal HTTP server. Our
-    objective is to write a code as idiomatic as possible.
-
-    To that end, we rely on the <<coq-prelude>> package, and therefore import
-    it. *)
-
-From Base Require Import Prelude.
-
-(** **** A Word on Non-Termination *)
-
-(** As Coq users know, Gallina only allows to implement strictly recursive
-    functions, which means a function in Coq will always terminate. A webserver,
-    on the other hand, is expected to run as long as incoming connections
-    arrive.  FreeSpec will eventually deal with non-termination, but this has
-    not been our priority just yet. In the context of this tutorial, we
-    compromise and <<MiniHTTPServer>> will therefore only accept a finite number
-    of connections. However, we show that it is correct for any number of finite
-    steps.
-
-    To implement this behavior, we introduce [repeatM], which repeats an impure
-    computation [n] times. *)
-
-Fixpoint repeatM `{Monad m} {a}
-    (n : nat) (p : m a)
-  : m unit :=
-  match n with
-  | O => pure tt
-  | S n => p >>= fun _ => repeatM n p
-  end.
-
-(** **** A Generic TCP Server *)
-
-(** We first define a generic TCP Server as an impure computation parameterized
-    by a so-called handler, that is an impure computation which computes a
-    response message for each request message received from a client. *)
-
-Definition tcp_server `{Provide ix TCP}
-    (n : nat) (handler : bytestring -> impure ix bytestring)
-  : impure ix unit :=
-  let* server := new_tcp_socket "127.0.0.1:8088" in
-  listen_incoming_connection server;;
-
-  repeatM n (
-    let* client := accept_connection server in
-
-    let* req := read_socket client in
-    let* res := handler req in
-    write_socket client res;;
-
-    close_socket client);;
-
-  close_socket server.
-
-(** **** A HTTP Handler *)
-
-(** <<MiniHTTPServer>> is a minimal server which serves static files over HTTP.
-    The main task of its handler will perform is therefore to fetch the content
-    of a file identified by a given path. To implement this behavior, we define
-    an impure computation [read_content], which performs some logging in
-    addition to interacting with the file system.
-
-    As such, [read_content] uses two interfaces. We can specify that thanks to
-    [Provide], for instance with [`{Provide ix CONSOLE, Provide ix FILESYSTEM}].
-    FreeSpec provides [Provide2], [Provide3], [Provide4], and [Provide5] to make
-    the type more readable. *)
-
-Timeout 2 Definition read_content `{Provide2 ix FILESYSTEM CONSOLE}
-    (path : bytestring)
-  : impure ix bytestring :=
-  echo ("  reading <" ++ path ++ ">... ");;
-  let* fd := open path in
-  let* c := read fd in
-  close fd;;
-  echo "done.\n";;
-  pure c.
-
-(** Using this utility function, we can define the handler itself.
-
-    The parsing of the incoming HTTP requests, and the serialization of HTTP
-    response have been implemented in Coq, but are not relevant in this
-    tutorial. They are provided inside the <<coq-MiniHTTPServer>> and we reuse
-    them. *)
-
-From MiniHTTPServer Require Import URI HTTP.
-
-(** This provides the following types and functions:
-
-      - [http_req] encodes the supported HTTP requests (currently, only GET
-        requests are supported).
-      - [http_request] a parsing function of the form [bytestring -> error_stack +
-        http_req]
-      - [http_res] encodes the HTTP responses used by MiniHTTPServer (in our
-        case, 200, 401, and 404)
-      - [response_to_string] to serialize a response as a valid HTTP string. *)
-
-Definition request_handler `{Provide2 ix FILESYSTEM CONSOLE}
-    (base : list directory_id) (req : request)
-  : impure ix response :=
-  match req with
-  | Get uri =>
-    let path := uri_to_path (sandbox base uri) in
-    let* isf := file_exists path in
-    if (isf : bool)
-    then make_response success_OK <$> read_content path
-    else (
-      echo ("  resource <" ++ path ++"> not found\n");;
-      pure (make_response client_error_NotFound
-                          "Resource not found."))
-  end.
-
-Definition http_handler `{Provide2 ix FILESYSTEM CONSOLE}
-    (base : list directory_id) (req : bytestring)
-  : impure ix bytestring :=
-  echo "new request received\n";;
-  echo ("  request size is "
-           ++ bytestring_of_int (Bytestring.length req)
-           ++ "\n");;
-
-  let* res :=
-     match http_request req with
-     | inr req => request_handler base (fst req)
-     | _ => pure (make_response client_error_BadRequest
-                                "Bad request")
-     end in
-
-  pure (response_to_string res).
-
-(** Since [read_content] uses the [CONSOLE] interface in addition to
-    [FILESYSTEM], our [http_handler] type exposes this explicitely. However,
-    [http_handler] does not use the [TCP] interface itself, and therefore the
-    [TCP] interface does not appear inside its type even if in practice it will
-    be used in a context where [TCP] is available.
-
-    [http_server] is the final function, the [tcp_server] is specialized with
-    our [http_handler]. As a consequence, the type of [http_server] exposes the
-    three interfaces we use. *)
-
-Definition http_server
-   `{Provide3 ix FILESYSTEM TCP CONSOLE}
-    (n : nat)
-  : impure ix unit :=
- echo "hello, MiniHTTPServer!\n";;
- tcp_server n (http_handler [Dirname "tmp"]).
-
-(** ** Certifying *)
-
-(** As a reminder, our goal is to prove our HTTP server correctly use the
-    filesystem, that is it reads from and closes valid file descriptors, and
-    closes all its file descriptors. To that end, we need to define a contract
-    for the [FILESYSTEM] interface, then reason about [http_server] executions
-    w.r.t. this contract. *)
-
-(** *** Defining a Contract *)
-
-(** Defining a contract for an interface in FreeSpec means specifying how an
-    interface shall be used, but also what to expect from the results of its
-    primitives. *)
-
-(** **** The Witness State Type and Helpers *)
-
-(** A contract in FreeSpec has a so-called witness state attached to it. It
-    allows to take into account the stateful nature of impure computations and
-    primitives implementers. More precisely, a primitive of an interface which
-    could be used at a given time may become forbidden in the future.
-
-    This is precisely the case with our use case: a valid file descriptor
-    becomes invalid once it has been used as an arguent of the [Close]
-    primitive. Witness states shall be as simple as possible, and only holds the
-    minimum amount of information about past executed primitives. In our case,
-    the witness state can be as simple as a set of open file descriptors. *)
-
-Definition fd_set : Type :=
-  file_descriptor -> bool.
-
-(** In addition, we provide the usuals helpers to manipulate (addition,
-    deletion) and reason about sets. *)
-
-Axiom fd_eq_dec : forall (fd1 fd2 : file_descriptor),
-    { fd1 = fd2 } + { ~ (fd1 = fd2) }.
-
-Definition add_fd (ω : fd_set)
-    (fd : file_descriptor)
-  : fd_set :=
-  fun (fd' : file_descriptor) =>
-    if fd_eq_dec fd fd' then true else ω fd'.
-
-Definition del_fd (ω : fd_set)
-    (fd : file_descriptor)
-  : fd_set :=
-  fun (fd' : file_descriptor) =>
-    if fd_eq_dec fd fd' then false else ω fd'.
-
-Definition member (ω : fd_set)
-    (fd : file_descriptor)
-  : Prop :=
-  ω fd = true.
-
-Definition absent (ω : fd_set)
-    (fd : file_descriptor)
-  : Prop :=
-  ω fd = false.
-
-Lemma member_not_absent (ω : fd_set)
-    (fd : file_descriptor)
-  : member ω fd -> ~ absent ω fd.
-
-Proof.
-  unfold member, absent.
-  intros m a.
-  now rewrite m in a.
-Qed.
-
-Hint Resolve member_not_absent : minihttp.
-
-Lemma absent_not_member (ω : fd_set)
-    (fd : file_descriptor)
-  : absent ω fd -> ~ member ω fd.
-
-Proof.
-  unfold member, absent.
-  intros a m.
-  now rewrite m in a.
-Qed.
-
-Hint Resolve absent_not_member : minihttp.
-
-Lemma member_add_fd (ω : fd_set)
-    (fd : file_descriptor)
-  : member (add_fd ω fd) fd.
-
-Proof.
-  unfold member, add_fd.
-  destruct fd_eq_dec; auto.
-Qed.
-
-Hint Resolve member_add_fd : minihttp.
-
-(** **** The Update Function *)
-
-(** In FreeSpec, a contract provides a so-called “update function” to be used to
-    reason about an interface usage over time. At any computation step requiring
-    the use of a primitive, the “current” witness state is used to determine
-    both the caller and the callee obligations. Then, the update function is
-    used to update the witness state to take into account what happened for
-    future primitives execution.
-
-    In our case, since the witness state is just a set of open file descriptors
-    and does not hold any information about e.g. file actual content, the update
-    function remains simple: we add newly open file descriptor after [Open], and
-    remove them after [Close]. *)
-
-Definition fd_set_update (ω : fd_set)
-    (a : Type) (e : FILESYSTEM a) (x : a)
-  : fd_set :=
-  match e, x with
-  | Open _, fd =>
-    add_fd ω fd
-  | Close fd, _ =>
-    del_fd ω fd
-  | Read _, _ =>
-    ω
-  | FileExists _, _ =>
-    ω
-  end.
-
-(** **** The Caller Obligations *)
-
-(** Our experiment with FreeSpec has tended to show that using inductive types
-    for obligations is the more convenient approach in practice, but this comes
-    with a tradeoff in terms of readability. *)
-
-Inductive fd_set_caller_obligation (ω : fd_set)
-  : forall (a : Type), FILESYSTEM a -> Prop :=
-
-(** We do not restrict the use of [Open] or [FileExists] *)
-
-| fd_set_open_caller (p : bytestring)
-  : fd_set_caller_obligation ω file_descriptor (Open p)
-| fd_set_is_file_caller (p : bytestring)
-  : fd_set_caller_obligation ω bool (FileExists p)
-
-(** In order for [Read] and [Close] to be used correctly, their
-    [file_descriptor] argument has to be a member of the witness state. *)
-
-| fd_set_read_caller (fd : file_descriptor)
-    (is_member : member ω fd)
-  : fd_set_caller_obligation ω bytestring (Read fd)
-| fd_set_close_caller (fd : file_descriptor)
-    (is_member : member ω fd)
-  : fd_set_caller_obligation ω unit (Close fd).
-
-Hint Constructors fd_set_caller_obligation : minihttp.
-
-(** **** The Callee Obligations *)
-
-(** The callee obligations of our contract are not as straightforward as the
-    caller obligations. It appears that we could potentially require nothing
-    special from a [FILESYSTEM] implementer for our particular use case. There
-    is, however, one scenario that we want to avoid in practice:
-
-      - The caller opens two different files
-      - The callee returns the same file descriptor for both files
-      - the caller closes one file descriptor, and uses the second one
-
-    In such a scenario, the caller misuses the interface in good faith. To avoid
-    this, we require the [Open] primitives to return _fresh_ file
-    descriptors. *)
-
-Inductive fd_set_callee_obligation (ω : fd_set)
-  : forall (a : Type), FILESYSTEM a -> a -> Prop :=
-
-(** The [file_descriptor] returned by the [Open] primitive shall not be a member
-    of the witness state. *)
-
-| fd_set_open_callee (p : bytestring) (fd : file_descriptor)
-    (is_absent : absent ω fd)
-  : fd_set_callee_obligation ω file_descriptor (Open p) fd
-
-(** We do not specify any particular requirements for the results of the other
-    primitives. Therefore, we cannot use this contract to reason about the
-    result of reading twice the same file, for instance. This would require
-    another contract, which is totally fine with FreeSpec since we can compose
-    them together. *)
-
-| fd_set_read_callee (fd : file_descriptor) (s : bytestring)
-  : fd_set_callee_obligation ω bytestring (Read fd) s
-| fd_set_close_callee (fd : file_descriptor) (t : unit)
-  : fd_set_callee_obligation ω unit (Close fd) t
-| fd_set_is_file_callee (p : bytestring) (b : bool)
-  : fd_set_callee_obligation ω bool (FileExists p) b.
-
-Hint Constructors fd_set_callee_obligation : minihttp.
-
-(** **** The Contract Definition *)
-
-(** We put everything together by defining a term of type [contract FILESYSTEM
-    fd set]. *)
-
-Definition fd_set_contract : contract FILESYSTEM fd_set :=
-  {| witness_update := fd_set_update
-   ; caller_obligation := fd_set_caller_obligation
-   ; callee_obligation := fd_set_callee_obligation
-  |}.
-
-(** *** Problem Definition *)
-
-(** From the caller perspective, there is two concerns that we want to express.
-    First, we _always_ use correct file descriptors. Secondly, we _eventually_
-    close any file descriptor previously opened.
-
-    The first objective is a _safety_ property that we can express
-    using the [respectful_impure] predicate. The exact lemma is:
-
-<<
-Lemma fd_set_respectful_http_server
-   `{StrictProvide3 ix FILESYSTEM TCP CONSOLE}
-    (ω : fd_set) (n : nat)
-  : respectful_impure fd_set_contract ω (http_server n).
->>
-
-    The [StrictProvide3] typeclass is very analogous to the [Provide3] one, but
-    it requires more contrains about its arguments. The exact details about
-    the difference is out of the scope of this tutorial, especially since the
-    two typeclasses with eventually be merged together.
-
-    The second objective is a _liveness_ property that we can express agains the
-    final witness state. This can be acheived using the [respectful_run]
-    predicate provided by FreeSpec.
-
-<<
-Lemma fd_set_preserving_http_server
-   `{StrictProvide3 ix FILESYSTEM TCP CONSOLE}
-    (n : nat)
-  : forall (ω ω' : fd_set) (x : unit),
-    respectful_run fd_set_contract (http_server n) ω ω' x
-    -> forall fd, ω fd = ω' fd.
->>
-
-    This property can be read as: any [file_descriptor] which is opened during
-    the execution of [http_server] is closed before the execution ends. This
-    is a property that we generalize for any impure computations:  *)
-
-Definition fd_set_preserving {a}
-   `{MayProvide ix FILESYSTEM}
-    (p : impure ix a) :=
-  forall (ω ω' : fd_set) (x : a),
-    respectful_run fd_set_contract p ω ω' x
-    -> forall fd, ω fd = ω' fd.
-
-(** And, as a consequence, the second lemma we want to prove becomes:
-
-<<
-Lemma fd_set_preserving_http_server
-   `{StrictProvide3 ix FILESYSTEM TCP CONSOLE}
-    (n : nat)
-  : fd_set_preserving (http_server n).
->> *)
-
-(** *** <<MiniHTTPServer>> Proofs of Correctness *)
-
-(** We now have defined everything we need to prove the correctness of
-    <<MiniHTTPServer>>. The rest of this tutorial consists in actually write the
-    proofs. Our approach is bottom-up: we start from the leaves of our
-    computations, show they have some important properties, then reuse our
-    result to eventually conclude about the correctness of the whole program. *)
-
-(** **** Certifying [read_content] *)
-
-(** From the perspective of this tutorial, the [read_content] impure computation
-    is an interesting starting point: it uses two primitives that can be misused
-    according to the [fd_set_contract] ([Read], and [Close]), and it also uses
-    an interface which is not relevant from the perspective of [fd_set_contract]
-    ([CONSOLE]). *)
-
-Lemma fd_set_respectful_read_content
-   `{StrictProvide2 ix FILESYSTEM CONSOLE}
-    (ω : fd_set) (path : bytestring)
-  : respectful_impure fd_set_contract ω (read_content path).
-
-(** FreeSpec provides the [prove_impure] tactics to automate as much as possible
-    the construction of a proof for [respectful_impure] goals. It performs many
-    uninteresting tasks that FreeSpec users would have to do manually if they
-    decided not to use it. For the sake of demonstration, we attempt to do just that,
-    and use [repeat constructor].
-
-    This generates 5 hardly readable subgoals, for instance the 5th subgoal is:
-
-<<
-  ω : fd_set
-  path : bytestring
-  x : unit
-  H4 : gen_callee_obligation fd_set_contract ω
-         (inj_p (Echo ("  reading <" ++ path ++ ">... "))) x
-  x0 : file_descriptor
-  H5 : gen_callee_obligation fd_set_contract
-         (gen_witness_update fd_set_contract ω
-            (inj_p (Echo ("  reading <" ++ path ++ ">... "))) x)
-         (inj_p (Open path)) x0
-  x1 : bytestring
-  H6 : gen_callee_obligation fd_set_contract
-         (gen_witness_update fd_set_contract
-            (gen_witness_update fd_set_contract ω
-               (inj_p (Echo ("  reading <" ++ path ++ ">... "))) x)
-            (inj_p (Open path)) x0) (inj_p (Read x0)) x1
-  x2 : unit
-  H7 : gen_callee_obligation fd_set_contract
-         (gen_witness_update fd_set_contract
-            (gen_witness_update fd_set_contract
-               (gen_witness_update fd_set_contract ω
-                  (inj_p (Echo ("  reading <" ++ path ++ ">... "))) x)
-               (inj_p (Open path)) x0) (inj_p (Read x0)) x1)
-         (inj_p (Close x0)) x2
-  ============================
- gen_caller_obligation fd_set_contract
-   (gen_witness_update fd_set_contract
-      (gen_witness_update fd_set_contract
-         (gen_witness_update fd_set_contract
-            (gen_witness_update fd_set_contract ω
-               (inj_p (Echo ("  reading <" ++ path ++ ">... "))) x)
-            (inj_p (Open path)) x0) (inj_p (Read x0)) x1)
-      (inj_p (Close x0)) x2) (inj_p (Echo "done.
-"))
->>
-
-    [prove_impure] provides a much cleaner output:
-
-<<
-subgoal 1 is:
-  fd_set_caller_obligation ω file_descriptor (Open path)
-
-subgoal 2 is:
- fd_set_caller_obligation (add_fd ω x0) bytestring (Read x0)
-
-subgoal 3 is:
- fd_set_caller_obligation (add_fd ω x0) unit (Close x0)
->>
-
-    In this case, we can use the [minihttp] database that we have enriched with various [Hint]
-    to conclude automatically about this. *)
-
-Proof.
-  prove_impure.
-  all: eauto with minihttp.
-Qed.
-
-Hint Resolve fd_set_respectful_read_content : minihttp.
-
-(** The second property we want to prove about [read_content] is that
-    it does not forget to close any [file_descriptor]. *)
-
-Lemma fd_set_preserving_read_content
-   `{StrictProvide2 ix FILESYSTEM CONSOLE}
-    (path : bytestring)
-  : fd_set_preserving (read_content path).
-
-(** Similarly to [prove_impure], FreeSpec provides a tactic to exploit
-    hypotheses about [respectful_run]. More precisely, it explore the different
-    execution path that could lead to the production of the run in hypothesis,
-    and clean-up as much as possible the resulting alternative goals.. We can
-    explicit the tasks performed by [respectful_run] with the following
-    command.
-
-<<
-  repeat match goal with
-         | H : respectful_run _ _ _ _ _ |- _ =>
-           inversion H; clear H; ssubst
-         end.
->>
-
-    This produces the following goal:
-
-<<
-  path : bytestring
-  ω : fd_set
-  x : bytestring
-  x0 : unit
-  o_callee : gen_callee_obligation fd_set_contract ω
-               (inj_p (Echo ("  reading <" ++ path ++ ">... "))) x0
-  o_caller : gen_caller_obligation fd_set_contract ω
-               (inj_p (Echo ("  reading <" ++ path ++ ">... ")))
-  x1 : file_descriptor
-  o_callee0 : gen_callee_obligation fd_set_contract
-                (gen_witness_update fd_set_contract ω
-                   (inj_p (Echo ("  reading <" ++ path ++ ">... "))) x0)
-                (inj_p (Open path)) x1
-  o_caller0 : gen_caller_obligation fd_set_contract
-                (gen_witness_update fd_set_contract ω
-                   (inj_p (Echo ("  reading <" ++ path ++ ">... "))) x0)
-                (inj_p (Open path))
-
-                               [...]
-
-  o_caller3 : gen_caller_obligation fd_set_contract
-                (gen_witness_update fd_set_contract
-                   (gen_witness_update fd_set_contract
-                      (gen_witness_update fd_set_contract
-                         (gen_witness_update fd_set_contract ω
-                            (inj_p (Echo ("  reading <" ++ path ++ ">... "))) x0)
-                         (inj_p (Open path)) x1) (inj_p (Read x1)) x)
-                   (inj_p (Close x1)) x3) (inj_p (Echo "done.
-"))
-  o_callee3 : gen_callee_obligation fd_set_contract
-                (gen_witness_update fd_set_contract
-                   (gen_witness_update fd_set_contract
-                      (gen_witness_update fd_set_contract
-                         (gen_witness_update fd_set_contract ω
-                            (inj_p (Echo ("  reading <" ++ path ++ ">... "))) x0)
-                         (inj_p (Open path)) x1) (inj_p (Read x1)) x)
-                   (inj_p (Close x1)) x3) (inj_p (Echo "done.
-")) x4
-  ============================
-  forall fd : file_descriptor,
-  ω fd =
-  gen_witness_update fd_set_contract
-    (gen_witness_update fd_set_contract
-       (gen_witness_update fd_set_contract
-          (gen_witness_update fd_set_contract
-             (gen_witness_update fd_set_contract ω
-                (inj_p (Echo ("  reading <" ++ path ++ ">... "))) x0)
-             (inj_p (Open path)) x1) (inj_p (Read x1)) x)
-       (inj_p (Close x1)) x3) (inj_p (Echo "done.
-")) x4 fd
->>
-
-    On the contrary, [unroll_respectful_run] keeps the goal manageable, and once called, the FreeSpec
-    internals are gone and we can write a “classical” Coq proof. *)
-
-Proof.
-  intros ω ω' x run.
-  unroll_respectful_run run.
-  intros fd'.
-  unfold add_fd, del_fd.
-  destruct fd_eq_dec; subst.
-  + now inversion o_callee0; ssubst.
-  + reflexivity.
-Qed.
-
-(** The implementation details of [read_content] will not be relevant with our
-    two freshly proven lemmas. Therefore, we make the impure computation to
-    prevent [improve_impure] and [unroll_respectful_run] to unfold them. *)
-
-#[local] Opaque read_content.
-
-(** **** Certifying [file_exists] *)
-
-(** We use the exact same approach for [file_exists]. Since this computation
-    does not use any problematic primitives, the proofs are straightforward. *)
-
-Lemma fd_set_respectful_file_exists
-   `{Provide ix FILESYSTEM}
-    (ω : fd_set) (path : bytestring)
-  : respectful_impure fd_set_contract ω (file_exists path).
-
-Proof.
-  prove impure with minihttp.
-Qed.
-
-Hint Resolve fd_set_respectful_file_exists : minihttp.
-
-Lemma fd_set_preserving_file_exists
-   `{Provide ix FILESYSTEM} (path : bytestring)
-  : fd_set_preserving (file_exists path).
-
-Proof.
-  intros ω ω' x run.
-  now unroll_respectful_run run.
-Qed.
-
-(** Again, we make [file_exists] opaque because its concrete implementation is
-    not relevant anymore. *)
-
-#[local] Opaque file_exists.
-
-(** **** Certifying [http_handler] *)
-
-(** The [http_handler] is interesting, because to a large extent, it does not
-    use primitives itself: it relies on other impure computations [read_content]
-    and [file_exists] to do so. Interesting readers can try to remove the
-    vernacular commands which make these two computations opaques and see the
-    outputs of [prove_impure] and [unroll_respectful_run]: in a nutshell, they
-    would find themselves having to prove one more time the exact same goals, in
-    more crowded contexts. *)
-
-#[local] Opaque http_request.
-
-Lemma fd_set_respectful_http_handler
-   `{StrictProvide2 ix FILESYSTEM CONSOLE}
-    (base : list directory_id) (req : bytestring)
-    (ω : fd_set)
-  : respectful_impure fd_set_contract ω (http_handler base req).
-
-Proof.
-  prove_impure.
-  destruct (http_request req).
-  + prove_impure.
-  + destruct (fst p).
-    prove_impure.
-
-(** Here, [prove_impure] did not unfold [file_exists] and [read_content], but
-    has leveraged FreeSpec formalism to generate two clean subgoals.
-<<
-subgoal 1 is:
-  respectful_impure fd_set_contract ω
-    (file_exists (uri_to_path (sandbox base resource)))
-
-subgoal 2 is:
- respectful_impure fd_set_contract w
-   (read_content (uri_to_path (sandbox base resource)))
->>
-
-    Both are straightforward to prove using the [minihttp] hint database. *)
-
-    all: eauto with minihttp.
-Qed.
-
-Hint Resolve fd_set_respectful_http_handler : minihttp.
-
-Lemma fd_set_preserving_http_handler
-   `{StrictProvide2 ix FILESYSTEM CONSOLE}
-    (base : list directory_id) (req : bytestring)
-  : fd_set_preserving (http_handler base req).
-
-Proof.
-  intros ω ω' x run fd.
-  unroll_respectful_run run.
-  destruct (http_request req).
-  + now unroll_respectful_run run.
-  + destruct p as [[res_id] req'].
-    unroll_respectful_run run.
-
-(** [unroll_respectful_run] uses a simiral approach when in presence of opaque
-    terms. *)
-
-    ++ apply fd_set_preserving_file_exists in run0.
-       apply fd_set_preserving_read_content in run.
-       now transitivity (ω'' fd).
-    ++ now apply fd_set_preserving_file_exists in run0.
-Qed.
-
-Hint Resolve fd_set_preserving_http_handler : minihttp.
-
-#[local] Opaque http_handler.
-#[local] Opaque response_to_string.
-
-(** **** Certifying [repeatM] *)
-
-From Coq Require Import FunctionalExtensionality.
-
-Lemma fd_set_preserving_repeatM {a}
-   `{Provide ix FILESYSTEM}
-    (p : impure ix a)
-    (fd_preserving : fd_set_preserving p)
-    (n : nat)
-  : fd_set_preserving (repeatM n p).
-
-Proof.
-  intros ω ω' fd run.
-  induction n.
-  + now unroll_respectful_run run.
-  + unroll_respectful_run run.
-    apply IHn.
-    replace ω with ω''; auto.
-    symmetry.
-    apply functional_extensionality.
-    eauto.
-Qed.
-
-Hint Resolve fd_set_preserving_repeatM : minihttp.
-
-Lemma repeatM_preserving_respectful {a}
-   `{Provide ix FILESYSTEM}
-    (p : impure ix a) (ω : fd_set)
-    (fd_trust : respectful_impure fd_set_contract ω p)
-    (fd_preserving : fd_set_preserving p)
-    (n : nat)
-  : respectful_impure fd_set_contract ω (repeatM n p).
-
-Proof.
-  induction n.
-  + prove_impure.
-  + prove_impure.
-    ++ exact fd_trust.
-    ++ replace w with ω; auto.
-       apply functional_extensionality.
-       intros fd.
-       eapply fd_preserving.
-       exact Hrun.
-Qed.
-
-#[local] Opaque repeatM.
-
-Lemma fd_set_preserving_tcp_server_repeat_routine
-   `{Provide ix TCP, MayProvide ix FILESYSTEM, Distinguish ix TCP FILESYSTEM}
-    (server : socket_descriptor)
-    (handler : bytestring -> impure ix bytestring)
-    (preserve : forall (req : bytestring), fd_set_preserving (handler req))
-  : fd_set_preserving (
-         let* client := accept_connection server in
-
-         let* req := read_socket client in
-         let* res := handler req in
-         write_socket client res;;
-
-         close_socket client).
-
-Proof.
-  intros ω ω' b run fd.
-  unroll_respectful_run run.
-  now apply preserve in run.
-Qed.
-
-Hint Resolve fd_set_preserving_tcp_server_repeat_routine : minihttp.
-
-(** **** Certifying [http_server] *)
-
-Lemma fd_set_respectful_http_server
-   `{StrictProvide3 ix FILESYSTEM TCP CONSOLE}
-    (ω : fd_set) (n : nat)
-  : respectful_impure fd_set_contract ω (http_server n).
-
-Proof.
-  prove_impure.
-  apply repeatM_preserving_respectful.
-  + prove_impure.
-    apply fd_set_respectful_http_handler.
-  + intros ω' ω'' [] run fd.
-    apply fd_set_preserving_tcp_server_repeat_routine
-      in run;
-      auto with minihttp.
-    apply fd_set_preserving_http_handler.
-Qed.
-
-Lemma fd_set_preserving_http_server
-   `{StrictProvide3 ix FILESYSTEM TCP CONSOLE}
-    (n : nat)
-  : fd_set_preserving (http_server n).
-
-Proof.
-  intros ω ω' x run fd.
-  unroll_respectful_run run.
-  apply fd_set_preserving_repeatM in run;
-    auto with minihttp.
-  apply fd_set_preserving_tcp_server_repeat_routine.
-  apply fd_set_preserving_http_handler.
-Qed.