diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 32b25a57..13323c5d 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -1,4 +1,4 @@ -name: Test Compilation for OCaml +name: Compilation for Griotte # Prevent parallel CI: Stop every workflow of a branch concurrency: @@ -74,3 +74,14 @@ jobs: eval "$(opam env)" opam exec -- dune build --display short -j ${{ env.JOBS_LIMIT }} --trace-file griotte.trc ./pretty-print-trace.sh griotte.trc + + - name: Build docs + run: opam exec -- make html + + - name: Deploy docs (if main branch) + uses: peaceiris/actions-gh-pages@v4 + if: ${{ steps.get_branch.outputs.branch == 'main' }} + with: + github_token: ${{ secrets.GITHUB_TOKEN }} + publish_dir: ./html + destination_dir: dev diff --git a/.gitignore b/.gitignore index dc326721..c12ca8d4 100644 --- a/.gitignore +++ b/.gitignore @@ -297,4 +297,5 @@ Makefile.coq Makefile.coq.conf _build/ +html/ *.trc diff --git a/Makefile b/Makefile index f5c37be9..7ddc811e 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,10 @@ -.PHONY: all theories doc +EXTRA_DIR = rocqdoc_extra +BUILD_DOC_DIR = _build/default/theories/cap_machine.html +PUBLISH_DIR = html -all: theories doc +.PHONY: all theories rocqdoc html + +all: theories rocqdoc theories: dune build --display short --trace-file griotte.trc @@ -8,11 +12,19 @@ theories: pretty-timed: theories ./pretty-print-trace.sh griotte.trc -doc: +rocqdoc: theories dune build @doc --display short +html: rocqdoc + rm -rf $(PUBLISH_DIR) + mkdir $(PUBLISH_DIR) + cp $(BUILD_DOC_DIR)/* $(PUBLISH_DIR) + chmod -R +w $(PUBLISH_DIR) + cp $(EXTRA_DIR)/resources/* $(PUBLISH_DIR) + clean: dune clean + rm -rf $(PUBLISH_DIR) rm -f griotte.trc # Adapted from https://github.com/AbsInt/CompCert/blob/master/Makefile diff --git a/README.md b/README.md index 79a46064..81a760ee 100644 --- a/README.md +++ b/README.md @@ -163,9 +163,6 @@ The organisation of the `theories/` folder is as follows. - `region_invariants_allocation.v`: Lemmas for allocating a range of standard resources. -- `world_interp_allocation_compartments.v`: - Lemmas for allocating standard resources for adversary compartments. - - `model_interp_stack.v`: Definitions and lemmas specific to reasoning about the stack region. @@ -174,6 +171,13 @@ The organisation of the `theories/` folder is as follows. - `world_ghost_theory.v`: Ghost theory of world interpretation. Clean interface with the model to ease the proofs for the user. + +- `world_interp_allocation_compartments.v`: + Lemmas for allocating standard resources for adversary compartments. + +- `world_interp_stack.v`: + Extension of the ghost theory of world interpretation, + specific to stack region. ## Logical relation and FTLR `logrel/` @@ -186,7 +190,7 @@ The organisation of the `theories/` folder is as follows. - `world_interp_stack.v`: A collections of lemmas related to world manipulation in presence of safe-to-share. -- `monotone.v`: Proof of the monotonicity of the value relation with regards to +- `ftlr/monotone.v`: Proof of the monotonicity of the value relation with regards to public future worlds, and private future worlds for non local words. - `fundamental.v`: Contains *Fundamental Theorem of Logical @@ -198,10 +202,6 @@ The organisation of the `theories/` folder is as follows. Definition of resources to have a clean interface with manipulation of the world, for stack region. -- `world_interp_stack.v`: - Extension of the ghost theory of world interpretation, - specific to stack region. - ## Switcher `switcher/` - `switcher.v`: Code of the Griotte switcher. diff --git a/dune-project b/dune-project index e67e85a2..d12e5252 100644 --- a/dune-project +++ b/dune-project @@ -18,7 +18,7 @@ (name griotte) (synopsis "Griotte") (description "Griotte") - (depends ocaml dune rocq-iris equations) + (depends ocaml dune odoc rocq-iris equations) (tags (Rocq CHERIoT "capability machine" Iris))) diff --git a/opam b/opam index afad613b..7daf48ca 100644 --- a/opam +++ b/opam @@ -5,6 +5,7 @@ maintainer: "" authors: [ "anonymous" ] depends: [ "dune" {= "3.21.0"} + "odoc" "rocq-core" {= "9.1.1"} "rocq-stdlib" {= "9.0.0"} "rocq-stdpp" {= "1.13.0"} diff --git a/rocqdoc_extra/LICENSE b/rocqdoc_extra/LICENSE new file mode 100644 index 00000000..9cc94e57 --- /dev/null +++ b/rocqdoc_extra/LICENSE @@ -0,0 +1,21 @@ +Copyright (c) 2016, Tobias Tebbi +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + * Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND +ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE LIABLE FOR ANY +DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES +(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND +ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/rocqdoc_extra/footer.html b/rocqdoc_extra/footer.html new file mode 100644 index 00000000..d0f79a88 --- /dev/null +++ b/rocqdoc_extra/footer.html @@ -0,0 +1,8 @@ + + + + + + diff --git a/rocqdoc_extra/header.html b/rocqdoc_extra/header.html new file mode 100644 index 00000000..0e698bfc --- /dev/null +++ b/rocqdoc_extra/header.html @@ -0,0 +1,27 @@ + + + + + + + + + + + + + +
+
diff --git a/rocqdoc_extra/resources/config.js b/rocqdoc_extra/resources/config.js new file mode 100644 index 00000000..72be6131 --- /dev/null +++ b/rocqdoc_extra/resources/config.js @@ -0,0 +1,72 @@ +var coqdocjs = coqdocjs || {}; + +coqdocjs.repl = { + "forall": "∀", + "exists": "∃", + "~": "¬", + "/\\": "∧", + "\\/": "∨", + "->": "→", + "<-": "←", + "<->": "↔", + "=>": "⇒", + "<>": "≠", + "<=": "≤", + ">=": "≥", + "el": "∈", + "nel": "∉", + "<<=": "⊆", + "|-": "⊢", + ">>": "»", + "<<": "⊆", + "++": "⧺", + "===": "≡", + "=/=": "≢", + "=~=": "≅", + "==>": "⟹", + "lhd": "⊲", + "rhd": "⊳", + "nat": "ℕ", + "alpha": "α", + "beta": "β", + "gamma": "γ", + "delta": "δ", + "epsilon": "ε", + "eta": "η", + "iota": "ι", + "kappa": "κ", + "lambda": "λ", + "mu": "μ", + "nu": "ν", + "omega": "ω", + "phi": "ϕ", + "pi": "π", + "psi": "ψ", + "rho": "ρ", + "sigma": "σ", + "tau": "τ", + "theta": "θ", + "xi": "ξ", + "zeta": "ζ", + "Delta": "Δ", + "Gamma": "Γ", + "Pi": "Π", + "Sigma": "Σ", + "Omega": "Ω", + "Xi": "Ξ" +}; + +coqdocjs.subscr = { + "0" : "₀", + "1" : "₁", + "2" : "₂", + "3" : "₃", + "4" : "₄", + "5" : "₅", + "6" : "₆", + "7" : "₇", + "8" : "₈", + "9" : "₉", +}; + +coqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="]; diff --git a/rocqdoc_extra/resources/coqdoc.css b/rocqdoc_extra/resources/coqdoc.css new file mode 100644 index 00000000..18dad894 --- /dev/null +++ b/rocqdoc_extra/resources/coqdoc.css @@ -0,0 +1,197 @@ +@import url(https://fonts.googleapis.com/css?family=Open+Sans:400,700); + +body{ + font-family: 'Open Sans', sans-serif; + font-size: 14px; + color: #2D2D2D +} + +a { + text-decoration: none; + border-radius: 3px; + padding-left: 3px; + padding-right: 3px; + margin-left: -3px; + margin-right: -3px; + color: inherit; + font-weight: bold; +} + +#main .code a, #main .inlinecode a, #toc a { + font-weight: inherit; +} + +a[href]:hover, [clickable]:hover{ + background-color: rgba(0,0,0,0.1); + cursor: pointer; +} + +h, h1, h2, h3, h4, h5 { + line-height: 1; + color: black; + text-rendering: optimizeLegibility; + font-weight: normal; + letter-spacing: 0.1em; + text-align: left; +} + +div + br { + display: none; +} + +div:empty{ display: none;} + +#main h1 { + font-size: 2em; +} + +#main h2 { + font-size: 1.667rem; +} + +#main h3 { + font-size: 1.333em; +} + +#main h4, #main h5, #main h6 { + font-size: 1em; +} + +#toc h2 { + padding-bottom: 0; +} + +#main .doc { + margin: 0; + text-align: justify; +} + +.inlinecode, .code, #main pre { + font-family: monospace; +} + +.code > br:first-child { + display: none; +} + +.doc + .code{ + margin-top:0.5em; +} + +.block{ + display: block; + margin-top: 5px; + margin-bottom: 5px; + padding: 10px; + text-align: center; +} + +.block img{ + margin: 15px; +} + +table.infrule { + border: 0px; + margin-left: 50px; + margin-top: 10px; + margin-bottom: 10px; +} + +td.infrule { + font-family: "Droid Sans Mono", "DejaVu Sans Mono", monospace; + text-align: center; + padding: 0; + line-height: 1; +} + +tr.infrulemiddle hr { + margin: 1px 0 1px 0; +} + +.infrulenamecol { + color: rgb(60%,60%,60%); + padding-left: 1em; + padding-bottom: 0.1em +} + +.id[type="constructor"], .id[type="projection"], .id[type="method"], +.id[title="constructor"], .id[title="projection"], .id[title="method"] { + color: #A30E16; +} + +.id[type="var"], .id[type="variable"], +.id[title="var"], .id[title="variable"] { + color: inherit; +} + +.id[type="definition"], .id[type="record"], .id[type="class"], .id[type="instance"], .id[type="inductive"], .id[type="library"], +.id[title="definition"], .id[title="record"], .id[title="class"], .id[title="instance"], .id[title="inductive"], .id[title="library"] { + color: #A6650F; +} + +.id[type="lemma"], +.id[title="lemma"]{ + color: #188B0C; +} + +.id[type="keyword"], .id[type="notation"], .id[type="abbreviation"], +.id[title="keyword"], .id[title="notation"], .id[title="abbreviation"]{ + color : #2874AE; +} + +.comment { + color: #808080; +} + +/* TOC */ + +#toc h2{ + letter-spacing: 0; + font-size: 1.333em; +} + +/* Index */ + +#index { + margin: 0; + padding: 0; + width: 100%; +} + +#index #frontispiece { + margin: 1em auto; + padding: 1em; + width: 60%; +} + +.booktitle { font-size : 140% } +.authors { font-size : 90%; + line-height: 115%; } +.moreauthors { font-size : 60% } + +#index #entrance { + text-align: center; +} + +#index #entrance .spacer { + margin: 0 30px 0 30px; +} + +ul.doclist { + margin-top: 0em; + margin-bottom: 0em; +} + +#toc > * { + clear: both; +} + +#toc > a { + display: block; + float: left; + margin-top: 1em; +} + +#toc a h2{ + display: inline; +} diff --git a/rocqdoc_extra/resources/coqdocjs.css b/rocqdoc_extra/resources/coqdocjs.css new file mode 100644 index 00000000..d94bb581 --- /dev/null +++ b/rocqdoc_extra/resources/coqdocjs.css @@ -0,0 +1,249 @@ +/* replace unicode */ + +.id[repl] .hidden { + font-size: 0; +} + +.id[repl]:before{ + content: attr(repl); +} + +/* folding proofs */ + +@keyframes show-proof { + 0% { + max-height: 1.2em; + opacity: 1; + } + 99% { + max-height: 1000em; + } + 100%{ + } +} + +@keyframes hide-proof { + from { + visibility: visible; + max-height: 10em; + opacity: 1; + } + to { + max-height: 1.2em; + } +} + +.proof { + cursor: pointer; +} +.proof * { + cursor: pointer; +} + +.proof { + overflow: hidden; + position: relative; + transition: opacity 1s; + display: inline-block; +} + +.proof[show="false"] { + max-height: 1.2em; + visibility: visible; + opacity: 0.3; +} + +.proof[show="false"][animate] { + animation-name: hide-proof; + animation-duration: 0.25s; +} + +.proof[show=true] { + animation-name: show-proof; + animation-duration: 10s; +} + +.proof[show="false"]:before { + position: absolute; + visibility: visible; + width: 100%; + height: 100%; + display: block; + opacity: 0; + content: "M"; +} +.proof[show="false"]:hover:before { + content: ""; +} + +.proof[show="false"] + br + br { + display: none; +} + +.proof[show="false"]:hover { + visibility: visible; + opacity: 0.5; +} + +#toggle-proofs[proof-status="no-proofs"] { + display: none; +} + +#toggle-proofs[proof-status="some-hidden"]:before { + content: "Show Proofs"; +} + +#toggle-proofs[proof-status="all-shown"]:before { + content: "Hide Proofs"; +} + + +/* page layout */ + +html, body { + height: 100%; + margin:0; + padding:0; +} + +@media only screen { /* no div with internal scrolling to allow printing of whole content */ + body { + display: flex; + flex-direction: column + } + + #content { + flex: 1; + overflow: auto; + display: flex; + flex-direction: column; + } +} + +#content:focus { + outline: none; /* prevent glow in OS X */ +} + +#main { + display: block; + padding: 16px; + padding-top: 1em; + padding-bottom: 2em; + margin-left: auto; + margin-right: auto; + max-width: 60em; + flex: 1 0 auto; +} + +.libtitle { + display: none; +} + +/* header */ +#header { + width:100%; + padding: 0; + margin: 0; + display: flex; + align-items: center; + background-color: rgb(21,57,105); + color: white; + font-weight: bold; + overflow: hidden; +} + + +.button { + cursor: pointer; +} + +#header * { + text-decoration: none; + vertical-align: middle; + margin-left: 15px; + margin-right: 15px; +} + +#header > .right, #header > .left { + display: flex; + flex: 1; + align-items: center; +} +#header > .left { + text-align: left; +} +#header > .right { + flex-direction: row-reverse; +} + +#header a, #header .button { + color: white; + box-sizing: border-box; +} + +#header a { + border-radius: 0; + padding: 0.2em; +} + +#header .button { + background-color: rgb(63, 103, 156); + border-radius: 1em; + padding-left: 0.5em; + padding-right: 0.5em; + margin: 0.2em; +} + +#header a:hover, #header .button:hover { + background-color: rgb(181, 213, 255); + color: black; +} + +#header h1 { padding: 0; + margin: 0;} + +/* footer */ +#footer { + text-align: center; + opacity: 0.5; + font-size: 75%; +} + +/* hyperlinks */ + +@keyframes highlight { + 50%{ + background-color: black; + } +} + +:target * { + animation-name: highlight; + animation-duration: 1s; +} + +a[name]:empty { + float: right; +} + +/* Proviola */ + +div.code { + width: auto; + float: none; +} + +div.goal { + position: fixed; + left: 75%; + width: 25%; + top: 3em; +} + +div.doc { + clear: both; +} + +span.command:hover { + background-color: inherit; +} diff --git a/rocqdoc_extra/resources/coqdocjs.js b/rocqdoc_extra/resources/coqdocjs.js new file mode 100644 index 00000000..7ff56988 --- /dev/null +++ b/rocqdoc_extra/resources/coqdocjs.js @@ -0,0 +1,189 @@ +var coqdocjs = coqdocjs || {}; +(function(){ + +function replace(s){ + var m; + if (m = s.match(/^(.+)'/)) { + return replace(m[1])+"'"; + } else if (m = s.match(/^([A-Za-z]+)_?(\d+)$/)) { + return replace(m[1])+m[2].replace(/\d/g, function(d){ + if (coqdocjs.subscr.hasOwnProperty(d)) { + return coqdocjs.subscr[d]; + } else { + return d; + } + }); + } else if (coqdocjs.repl.hasOwnProperty(s)){ + return coqdocjs.repl[s] + } else { + return s; + } +} + +function toArray(nl){ + return Array.prototype.slice.call(nl); +} + +function replInTextNodes() { + coqdocjs.replInText.forEach(function(toReplace){ + toArray(document.getElementsByClassName("code")).concat(toArray(document.getElementsByClassName("inlinecode"))).forEach(function(elem){ + toArray(elem.childNodes).forEach(function(node){ + if (node.nodeType != Node.TEXT_NODE) return; + var fragments = node.textContent.split(toReplace); + node.textContent = fragments[fragments.length-1]; + for (var k = 0; k < fragments.length - 1; ++k) { + node.parentNode.insertBefore(document.createTextNode(fragments[k]),node); + var replacement = document.createElement("span"); + replacement.appendChild(document.createTextNode(toReplace)); + replacement.setAttribute("class", "id"); + replacement.setAttribute("type", "keyword"); + node.parentNode.insertBefore(replacement, node); + } + }); + }); + }); +} + +function replNodes() { + toArray(document.getElementsByClassName("id")).forEach(function(node){ + if (["var", "variable", "keyword", "notation", "definition", "inductive"].indexOf(node.getAttribute("type"))>=0){ + var text = node.textContent; + var replText = replace(text); + if(text != replText) { + node.setAttribute("repl", replText); + node.setAttribute("title", text); + var hidden = document.createElement("span"); + hidden.setAttribute("class", "hidden"); + while (node.firstChild) { + hidden.appendChild(node.firstChild); + } + node.appendChild(hidden); + } + } + }); +} + +function isVernacStart(l, t){ + t = t.trim(); + for(var s of l){ + if (t == s || t.startsWith(s+" ") || t.startsWith(s+".")){ + return true; + } + } + return false; +} + +function isProofStart(n){ + return isVernacStart(["Proof"], n.textContent) && !isVernacStart(["Default", "Suggest"], n.previousSibling.previousSibling.textContent) || + (isVernacStart(["Next"], n.textContent) && isVernacStart(["Obligation"], n.nextSibling.nextSibling.textContent)); +} + +function isProofEnd(s){ + return isVernacStart(["Qed", "Admitted", "Defined", "Abort"], s); +} + +function proofStatus(){ + var proofs = toArray(document.getElementsByClassName("proof")); + if(proofs.length) { + for(var proof of proofs) { + if (proof.getAttribute("show") === "false") { + return "some-hidden"; + } + } + return "all-shown"; + } + else { + return "no-proofs"; + } +} + +function updateView(){ + document.getElementById("toggle-proofs").setAttribute("proof-status", proofStatus()); +} + +function foldProofs() { + var hasCommands = true; + var nodes = document.getElementsByClassName("command"); + if(nodes.length == 0) { + hasCommands = false; + console.log("no command tags found") + nodes = document.getElementsByClassName("id"); + } + toArray(nodes).forEach(function(node){ + if(isProofStart(node)) { + var proof = document.createElement("span"); + proof.setAttribute("class", "proof"); + + node.parentNode.insertBefore(proof, node); + if(proof.previousSibling.nodeType === Node.TEXT_NODE) + proof.appendChild(proof.previousSibling); + while(node && !isProofEnd(node.textContent)) { + proof.appendChild(node); + node = proof.nextSibling; + } + if (proof.nextSibling) proof.appendChild(proof.nextSibling); // the Qed + if (!hasCommands && proof.nextSibling) proof.appendChild(proof.nextSibling); // the dot after the Qed + + proof.addEventListener("click", function(proof){return function(e){ + if (e.target.parentNode.tagName.toLowerCase() === "a") + return; + proof.setAttribute("show", proof.getAttribute("show") === "true" ? "false" : "true"); + proof.setAttribute("animate", ""); + updateView(); + };}(proof)); + proof.setAttribute("show", "false"); + } + }); +} + +function toggleProofs(){ + var someProofsHidden = proofStatus() === "some-hidden"; + toArray(document.getElementsByClassName("proof")).forEach(function(proof){ + proof.setAttribute("show", someProofsHidden); + proof.setAttribute("animate", ""); + }); + updateView(); +} + +function repairDom(){ + // pull whitespace out of command + toArray(document.getElementsByClassName("command")).forEach(function(node){ + while(node.firstChild && node.firstChild.textContent.trim() == ""){ + console.log("try move"); + node.parentNode.insertBefore(node.firstChild, node); + } + }); + toArray(document.getElementsByClassName("id")).forEach(function(node){ + node.setAttribute("type", node.getAttribute("title")); + }); + toArray(document.getElementsByClassName("idref")).forEach(function(ref){ + toArray(ref.childNodes).forEach(function(child){ + if (["var", "variable"].indexOf(child.getAttribute("type")) > -1) + ref.removeAttribute("href"); + }); + }); + +} + +function fixTitle(){ + var url = "/" + window.location.pathname; + var basename = url.substring(url.lastIndexOf('/')+1, url.lastIndexOf('.')); + if (basename === "toc") {document.title = "Table of Contents";} + else if (basename === "indexpage") {document.title = "Index";} + else {document.title = basename;} +} + +function postprocess(){ + repairDom(); + replInTextNodes() + replNodes(); + foldProofs(); + document.getElementById("toggle-proofs").addEventListener("click", toggleProofs); + updateView(); +} + +fixTitle(); +document.addEventListener('DOMContentLoaded', postprocess); + +coqdocjs.toggleProofs = toggleProofs; +})(); diff --git a/rocqdoc_extra/resources/index.html b/rocqdoc_extra/resources/index.html new file mode 100644 index 00000000..2f94de25 --- /dev/null +++ b/rocqdoc_extra/resources/index.html @@ -0,0 +1,320 @@ + + + + + + + + + + + + + +
+
+

Griotte: Verified Compartmentalisation via Capabilities

+

+ June Rousseau, + Aïna Linn Georges, + Jean Pichon-Pharabod, + Lars Birkedal

+ +

The complete list of modules in the development can be found in + the Table of Contents. We give below an overview of + the contents of the formalization. +

+ +

Operational semantics

+
    +
  • addr_reg: + Defines registers and the set of (finite) memory addresses. +
    • + +
  • machine_base: Contains + the syntax (permissions, capability, instructions, ...) of the + capability machine. +
    • + +
  • machine_parameters: + Defines a number of "settings" for the machine, that parameterize + the whole development (e.g. the specific encoding scheme for + instructions, etc.). +
    • + +
  • cap_lang: Defines the + operational semantics of the machine, and the embedding of the capability + machine language into Iris. +
    • +
+ +

Program logic

+
    +
  • rules.rules_base: + Contains some of the core resource algebras for the program logic, + namely the definition for points to predicates with permissions. +
    • + +
  • rules: Imports all the Hoare + triple rules for each instruction. These rules are separated into separate + files (located in the rules/ folder). +
    • +
+ +

Model of Kripke World

+
    +
  • sts: + The definition of stsCollection (named sts_full_world in the implementation), + and associated lemmas. In particular: + private and public future world relations (all these definitions are + parameterised by the standard states and two relations over them transitions. + These are instantiated in world_std_sts). +
    • + +
  • world_std_std: + Definitions of the standard world and the standard invariant states. + Also contains lemmas about standard transitions. +
    • + +
  • sts_multiple_updates: + Auxiliary definitions to reason about multiple updates to a world. +
    • + +
  • world_ghost_resources: + Defines the ghost resources needed to interpret the world. +
    • + +
  • region_invariants: + Definitions for standard resources, and the shared + resources map sharedResources (named region in the implementation). + Contains some lemmas for "opening" and "closing" the map, + akin to opening and closing invariants. +
    • + +
  • region_invariants_revocation: + Lemmas for revoking standard resources in the world interpretation. +
    • + +
  • region_invariants_allocation: + Lemmas for allocating a range of standard resources. +
    • + +
  • model_interp_stack: + Definitions and lemmas specific to reasoning about the stack region. +
    • +
+ +

Interface with Kripke World

+ Interface of Krikpe World for the user +
    + +
  • world_ghost_theory: + Ghost theory of world interpretation. + Clean interface with the model to ease the proofs for the user. +
    • + +
  • world_interp_allocation_compartment: + Lemmas for allocating standard resources for adversary compartments. +
    • + +
  • world_interp_stack: + Extension of the ghost theory of world interpretation, + specific to stack region. +
    • +
+ + +

Logical relation

+
    +
  • call_stack: + Definitions of the logical call-stack resources. +
    • + +
  • logrel: + The definition of the unary logical relation. +
    • + +
  • fundamental: + Establishes + the fundamental theorem of our logical relation. Each case (one + for each instruction) is proved in a separate file (located in + the ftlr/ folder), which are all imported and applied + in this file. +
    • +
+ +

Switcher

+
    +
  • switcher: + Code of the switcher. +
    • + +
  • switcher_preamble: + Definition of the switcher's invariant and + sealing predicate for the export table's otype. +
    • + +
  • interp_switcher_call: + Proof that the switcher's cross-compartment call sentry is safe to execute +
    • + +
  • interp_switcher_return: + Proof that the switcher's cross-compartment return sentry is safe to execute +
    • + +
  • switcher_spec_call: + Specification and proofs of the switcher's cross-compartment call sentry for known code, invoking unknown code. +
    • + +
  • switcher_spec_return: + Specification and proofs of the switcher's cross-compartment return sentry for known code, invoking unknown code. +
    • +
+ +

Case studies

+ +

Compartmentalisation (CMDC) Example

+ Example showcasing IMUD. + +
    +
  • cmdc: + Code of the compartmentalisation example. +
    • + +
  • cmdc_spec: + Specification of the compartmentalisation example. +
    • + +
  • cmdc_adequacy: + End-to-end theorem of the compartmentalisation example. + On particular, the final theorem is + cmdc_adequacy. +
    • +
+ + +

Deep Locality (DLE) Example

+ Example showcasing the novel deep locality permission. + + + +

Deep Immutability (DROE) Example

+ Example showcasing the novel deep immutability permission. + + + +

Very Awkward Example (VAE)

+ Example showcasing that the switcher implements Well-Bracketed Control Flow. + +
    +
  • vae: + Code of the VAE example. +
    • + +
  • vae_spec: + Specification of the VAE example. +
    • + +
  • vae_spec_closure: + Specification of closure involved in the VAE example. +
    • + +
  • vae_adequacy: + End-to-end theorem of the VAE example. + On particular, the final theorem is + vae_adequacy. +
    • +
+ + +

Protection Against Dangling Pointers (LSE Downward) Example

+ Example showcasing that the switcher implements protection against dangling pointers. + +
    +
  • lse: + Code of the LSE downward example. +
    • + +
  • lse_spec: + Specification of the LSE downward example. +
    • + +
  • lse_spec_closure: + Specification of closure involved in the LSE downward example. +
    • + +
  • lse_adequacy: + End-to-end theorem of the LSE downward example. + On particular, the final theorem is + lse_adequacy. +
    • +
+ +

Stack Object (SO) Example

+ Example showcasing that we can use stack objects. + + + +
+
+ + + diff --git a/theories/assumptions.v b/theories/assumptions.v index 9b2c9798..bb7f9480 100644 --- a/theories/assumptions.v +++ b/theories/assumptions.v @@ -7,7 +7,9 @@ From cap_machine Require stack_object_adequacy vae_adequacy . +(** Uncomment the following to print assumptions. *) +(* Goal True. idtac " Assumptions of fundamental theorem:". Abort. Print Assumptions fundamental.fundamental. @@ -35,3 +37,4 @@ Print Assumptions stack_object_adequacy.so_adequacy. Goal True. idtac " Assumptions of Very Awkward Example (VAE) end-to-end theorem:". Abort. Print Assumptions vae_adequacy.vae_adequacy. +*) diff --git a/theories/dune b/theories/dune index 7a43ff5f..dc5344f6 100644 --- a/theories/dune +++ b/theories/dune @@ -3,10 +3,15 @@ (rocq.theory (name cap_machine) (package griotte) + (rocqdoc_header ../rocqdoc_extra/header.html) + (rocqdoc_footer ../rocqdoc_extra/footer.html) (rocqdoc_flags - --utf8 --parse-comments --toc --lib-subtitles - --external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp - --external https://plv.mpi-sws.org/coqdoc/iris/ iris) + --external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp + --external https://plv.mpi-sws.org/coqdoc/iris/ iris + --toc --toc-depth 2 --html --interpolate + --index indexpage --no-lib-name --parse-comments + --utf8 --lib-subtitles + ) (flags :standard -w -convert_concl_no_check -w -several-object-files