summaryrefslogtreecommitdiffstats
path: root/site/posts/MiniHTTPServer.v
blob: 259d1631f6c5a0af7cd34bf9082630b5efcccdd6 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
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.