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