Publish a new article

1 files changed, 1003 insertions, 0 deletions

diff --git a/site/posts/MiniHTTPServer.v b/site/posts/MiniHTTPServer.v
new file mode 100644
index 0000000..259d163
--- /dev/null
+++ b/site/posts/MiniHTTPServer.v
@@ -0,0 +1,1003 @@
+(** #<h1>Implementing and Certifying a Web Server in Coq</h1># *)
+
+(** #<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>#
+
+    The [FreeSpec.Core] module reexports the key component provided by
+    FreeSpec. *)
+
+From FreeSpec Require Import Core.
+
+(** ** 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 [bytes]
+        (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 : bytes)
+  : 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
+        [bytes] type *)
+
+| ReadSocket (socket : socket_descriptor)
+  : TCP bytes
+| WriteSocket (socket : socket_descriptor) (msg : bytes)
+  : 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 : bytes)
+  : 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 bytes :=
+  request (ReadSocket socket).
+
+Definition write_socket `{Provide ix TCP}
+      (socket : socket_descriptor) (msg : bytes)
+    : 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 : bytes) : FILESYSTEM file_descriptor
+| FileExists (file : bytes) : FILESYSTEM bool
+| Read (file : file_descriptor) : FILESYSTEM bytes
+| Close (file : file_descriptor) : FILESYSTEM unit.
+
+Definition open `{Provide ix FILESYSTEM}
+    (path : bytes)
+  : 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 : bytes)
+  : impure ix bool :=
+  request (FileExists path).
+
+Definition read `{Provide ix FILESYSTEM}
+    (fd : file_descriptor)
+  : impure ix bytes :=
+  request (Read fd).
+
+(** **** The CONSOLE Interface *)
+
+(** Finally, FreeSpec already provides a few generic interfaces for FreeSpec
+    users, including a [CONSOLE] interface:
+
+<<
+Inductive CONSOLE : interface :=
+| Scan : CONSOLE bytes
+| Echo : bytes -> CONSOLE unit.
+>>
+
+    It is defined in the [FreeSpec.Stdlib.Console] module. *)
+
+From FreeSpec.Stdlib Require Import Console.
+
+(** *** 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 Prelude Require Import All Bytes.
+
+(** **** 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 => do p >>= fun _ => repeatM n p end
+  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 : bytes -> impure ix bytes)
+  : impure ix unit :=
+  do let* server := new_tcp_socket "127.0.0.1:8088" in
+     listen_incoming_connection server;
+
+     repeatM n do
+       let* client := accept_connection server in
+
+       let* req := read_socket client in
+       let* res := handler req in
+       write_socket client res;
+
+       close_socket client
+     end;
+
+     close_socket server
+  end.
+
+(** **** 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. *)
+
+Definition read_content `{Provide2 ix FILESYSTEM CONSOLE}
+    (path : bytes)
+  : impure ix bytes :=
+  do echo ("  reading <" ++ path ++ ">... ");
+     let* fd := open path in
+     let* c := read fd in
+     close fd;
+     echo ("done.\n");
+     pure c
+  end.
+
+(** 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 [bytes -> 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 =>
+    do 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 do
+         echo ("  resource <" ++ path ++"> not found\n");
+         pure (make_response client_error_NotFound
+                             "Resource not found.")
+       end
+    end
+  end.
+
+Definition http_handler `{Provide2 ix FILESYSTEM CONSOLE}
+    (base : list directory_id) (req : bytes)
+  : impure ix bytes :=
+  do echo "new request received\n";
+     echo ("  request size is " ++ Int.bytes_of_int (Bytes.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)
+  end.
+
+(** 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 :=
+  do echo "hello, MiniHTTPServer!\n";
+     tcp_server n (http_handler [Dirname "tmp"])
+  end.
+
+(** ** 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 : bytes)
+  : fd_set_caller_obligation ω file_descriptor (Open p)
+| fd_set_is_file_caller (p : bytes)
+  : 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 ω bytes (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 : bytes) (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 : bytes)
+  : fd_set_callee_obligation ω bytes (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 : bytes) (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 : bytes)
+  : 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 : bytes
+  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 : bytes
+  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) bytes (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 : bytes)
+  : 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 : bytes
+  ω : fd_set
+  x : bytes
+  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 : bytes)
+  : 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 : bytes)
+  : 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 : bytes)
+    (ω : 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 : bytes)
+  : 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 : bytes -> impure ix bytes)
+    (preserve : forall (req : bytes), fd_set_preserving (handler req))
+  : fd_set_preserving (do
+         let* client := accept_connection server in
+
+         let* req := read_socket client in
+         let* res := handler req in
+         write_socket client res;
+
+         close_socket client
+       end).
+
+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.