summaryrefslogtreecommitdiffstats
path: root/site/posts/MiniHTTPServer.v
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-02-04 23:07:30 +0100
committerThomas Letan <lthms@soap.coffee>2020-02-04 23:07:30 +0100
commit25c29703094557c095f6c998ac50e115ce7a1d72 (patch)
tree55a22f749a49d0bd234644264278910b0ceedf26 /site/posts/MiniHTTPServer.v
parent1f851ca9f2b400b5f7ca4d6a10c15fa734b86a17 (diff)
Publish a new article
Diffstat (limited to 'site/posts/MiniHTTPServer.v')
-rw-r--r--site/posts/MiniHTTPServer.v1003
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.