Merida in the movie Ralph 2.0

Implementing and Certifying a Web Server in Coq

This article has originally been published on February 02, 2020.
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.
  1. Implementation
    1. Defining Interfaces
      1. The TCP Interface
      2. The FILESYSTEM Interface
      3. The CONSOLE Interface
    2. Implementing a HTTP Server
      1. A Word on Non-Termination
      2. A Generic TCP Server
      3. A HTTP Handler
  2. Certifying
    1. Defining a Contract
      1. The Witness State Type and Helpers
      2. The Update Function
      3. The Caller Obligations
      4. The Callee Obligations
      5. The Contract Definition
    2. Problem Definition
    3. MiniHTTPServer Proofs of Correctness
      1. Certifying read_content
      2. Certifying file_exists
      3. Certifying http_handler
      4. Certifying repeatM
      5. Certifying http_server
Revisions

This revisions table has been automatically generated from the git history of this website repository, and the change descriptions may not always be as useful as they should.

You can consult the source of this file in its current version here.

2020-07-12 Various fixes here and there b85b9bc
2020-02-19 Use the correct font for interfaces in the titles 7171020
2020-02-19 Do not use raw HTML for the titles of Coq posts 9d8fc20
2020-02-16 Automatically generate a revision table from git history b47ee36
2020-02-05 Small changes in MiniHTTPServer.v bec5bbf
2020-02-04 Publish a new article 25c2970
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:

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:
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 (addr : bytestring)
  : TCP socket_descriptor


| ListenIncomingConnection (socket : socket_descriptor)
  : TCP unit


| AcceptConnection (socket : socket_descriptor)
  : TCP socket_descriptor


| ReadSocket (socket : socket_descriptor)
  : TCP bytestring
| WriteSocket (socket : socket_descriptor) (msg : bytestring)
  : TCP unit


| 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:

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:
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.