diff --git a/.gitmodules b/.gitmodules index 849a6b3..e69de29 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +0,0 @@ -[submodule "coqdocjs"] - path = coqdocjs - url = https://github.com/coq-community/coqdocjs.git diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..d14bf9e --- /dev/null +++ b/LICENSE @@ -0,0 +1,9 @@ +MIT License + +Copyright (c) Iris Tutorial developers and contributors + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/README.md b/README.md index db5aa8a..f7dfef8 100644 --- a/README.md +++ b/README.md @@ -1,30 +1,30 @@ # Iris Tutorial -The Iris Tutorial is an introduction to the [Iris separation logic framework](https://iris-project.org/) and how to work with its [Coq formalization](https://gitlab.mpi-sws.org/iris/iris/). +The Iris Tutorial is an introduction to the [Iris separation logic framework](https://iris-project.org/) and how to work with its [Rocq formalization](https://gitlab.mpi-sws.org/iris/iris/). -The exposition is intended for a broad range of readers from advanced undergraduates to PhD students and researchers. We assume that readers are already motivated to learn Iris and thus present the material in a bottom-up fashion, rather than starting out with cool motivating examples. The tutorial material is intended to be self-contained. No specific background in logic or programming languages is assumed but some familiarity with basic programming languages theory and discrete mathematics will be beneficial, see e.g. [TAPL](https://www.cis.upenn.edu/~bcpierce/tapl/). Additionally, basic knowledge of the Coq proof assistant is assumed. Advanced Coq tactics have been purposefully kept to a minimum, and some proofs are longer than necessary to facilitate learning. +The exposition is intended for a broad range of readers from advanced undergraduates to PhD students and researchers. We assume that readers are already motivated to learn Iris and thus present the material in a bottom-up fashion, rather than starting out with cool motivating examples. The tutorial material is intended to be self-contained. No specific background in logic or programming languages is assumed but some familiarity with basic programming languages theory and discrete mathematics will be beneficial, see e.g. [TAPL](https://www.cis.upenn.edu/~bcpierce/tapl/). Additionally, basic knowledge of the Rocq prover is assumed. Advanced Rocq tactics have been purposefully kept to a minimum, and some proofs are longer than necessary to facilitate learning. We demonstrate more advanced tactics in chapter [ticket_lock_advanced](/theories/ticket_lock_advanced.v). The tutorial comes in two versions: - The folder `exercises`: a skeleton development with exercises left admitted. - The folder `theories`: the full development with solutions. -The tutorial consists of several chapters, each corresponding to a Coq file. The graph in [Chapter Dependencies](README.md#chapter-dependencies) illustrates possible ways to go through the tutorial. However, the recommended order is specified in the [Recommended Learning Path](README.md#recommended-learning-path). +The tutorial consists of several chapters, each corresponding to a Rocq file. The graph in [Chapter Dependencies](README.md#chapter-dependencies) illustrates possible ways to go through the tutorial. However, the recommended order is specified in the [Recommended Learning Path](README.md#recommended-learning-path). ## Setup This version is known to compile with -- Coq 8.19.2 -- Iris 4.2.0 +- Rocq 8.20.1 +- Iris 4.3.0 The recommended way to install the dependencies is through [opam](https://opam.ocaml.org/doc/Install.html). 1. Install [opam](https://opam.ocaml.org/doc/Install.html) if not already installed (a version greater than 2.0 is required). -2. Install a new switch and link it to the project. +2. Install a new switch and link it to the project. From the root of the repository, execute ``` opam switch create iris_tutorial 5.2.0 opam switch link iris_tutorial . ``` -3. Add the Coq opam repository. +3. Add the Rocq opam repository. ``` opam repo add coq-released https://coq.inria.fr/opam/released opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git @@ -41,7 +41,7 @@ Iris makes extensive use of Unicode characters. [This guide](https://gitlab.mpi- ## Chapter Overview - [basics](/exercises/basics.v) - Introduction to the separation logic and the Iris Proof Mode -- [pure](/exercises/pure.v) - Distinction between the Coq context and the Iris context +- [pure](/exercises/pure.v) - Distinction between the Rocq context and the Iris context - [lang](/exercises/lang.v) - Introduction to HeapLang - [specifications](/exercises/specifications.v) - Weakest precondition, basic resources, Hoare triples, and basic concurrency @@ -57,6 +57,7 @@ Iris makes extensive use of Unicode characters. [This guide](https://gitlab.mpi- - [counter](/exercises/counter.v) - The authoritative camera - [spin_lock](/exercises/spin_lock.v) - Specification of a spin lock - [ticket_lock](/exercises/ticket_lock.v) - Specification of a ticket lock +- [ticket_lock_advanced](/theories/ticket_lock_advanced.v) - Advanced Rocq tactics - [adequacy](/exercises/adequacy.v) - Adequacy - [merge_sort](/exercises/merge_sort.v) - Merge sort - [custom_ra](/exercises/custom_ra.v) - Defining resource algebras from scratch @@ -144,7 +145,10 @@ The hope is that the maintenance and extension of this tutorial becomes a collab If you have suggestions for future topics or improvements for existing ones, please add them to [TODO.md](TODO.md). +**Note**: by contributing to the Iris Tutorial you agree that your contributions will be released under the terms of Iris Tutorial's license — see [the LICENSE file](LICENSE). + ### How to Contribute + To contribute, we recommend following these steps: 1. Fork the repository. @@ -196,4 +200,27 @@ If you have specific requests or questions about the tutorial, please contact: **Amin Timany**\ Aarhus University\ - \ No newline at end of file + + +### Contributors +Below is a list of people who have contributed to the tutorial, sorted by last name. If you have contributed to the project, please add yourself to the list. + +**Lars Birkedal**\ +Aarhus University\ + + +**Simon Gregersen**\ +Aarhus University\ + + +**Mathias Adam Møller**\ +Aarhus University\ + + +**Mathias Pedersen**\ +Aarhus University\ + + +**Amin Timany**\ +Aarhus University\ + diff --git a/TODO.md b/TODO.md index 95bb143..498e444 100644 --- a/TODO.md +++ b/TODO.md @@ -1,5 +1,12 @@ +# Fixes +- The chapter [gr_predicates.v] does actually not talk about guarded fixpoints, only least fixpoints +- Clean up proofs in some chapters + - Reduce use of SSreflect + - Simplify proofs + # Possible future topics -- Have a file showcasing advanced Coq tactics. +- Chapter on prophecies +- Chapter on HOCAP-style specifications - Chapters "Linked List", "Arrays", and "Merge Sort" all use list functionality from std++ (e.g. fmap and lookup). These should be introduced beforehand, for example in an appendix, with the chapters referring to the appendix. - Consider introducing commands "About", "Locate", "Print", etc. in an introductory chapter. - Add example with "Landin's knot" (recursion through the store) to showcase use of dicardable fractions or invariants for sequential programs diff --git a/_CoqProject b/_CoqProject index 966746e..09f3f52 100644 --- a/_CoqProject +++ b/_CoqProject @@ -19,11 +19,13 @@ theories/structured_conc.v theories/counter.v theories/spin_lock.v theories/ticket_lock.v +theories/array_lock.v theories/adequacy.v theories/merge_sort.v theories/custom_ra.v theories/ofe.v + exercises/basics.v exercises/pure.v exercises/lang.v @@ -40,7 +42,8 @@ exercises/structured_conc.v exercises/counter.v exercises/spin_lock.v exercises/ticket_lock.v +exercises/array_lock.v exercises/adequacy.v exercises/merge_sort.v exercises/custom_ra.v -exercises/ofe.v +exercises/ofe.v \ No newline at end of file diff --git a/coqdocjs b/coqdocjs deleted file mode 160000 index 5740184..0000000 --- a/coqdocjs +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 57401849fffb24500c078973a8382dd3086fd2bf diff --git a/coqdocjs/.gitignore b/coqdocjs/.gitignore new file mode 100644 index 0000000..8efb29d --- /dev/null +++ b/coqdocjs/.gitignore @@ -0,0 +1,34 @@ +.*.aux +.*.d +*.a +*.cma +*.cmi +*.cmo +*.cmx +*.cmxa +*.cmxs +*.glob +*.ml.d +*.ml4.d +*.mli.d +*.mllib.d +*.mlpack.d +*.native +*.o +*.v.d +*.vio +*.vo +*.vok +*.vos +.DS_Store +.coq-native/ +.csdp.cache +.lia.cache +.nia.cache +.nlia.cache +.nra.cache +csdp.cache +lia.cache +nia.cache +nlia.cache +nra.cache diff --git a/coqdocjs/LICENSE b/coqdocjs/LICENSE new file mode 100644 index 0000000..9cc94e5 --- /dev/null +++ b/coqdocjs/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/coqdocjs/Makefile.doc b/coqdocjs/Makefile.doc new file mode 100644 index 0000000..a93fe5a --- /dev/null +++ b/coqdocjs/Makefile.doc @@ -0,0 +1,19 @@ +COQDOCJS_DIR ?= coqdocjs +EXTRA_DIR = $(COQDOCJS_DIR)/extra +COQDOCFLAGS ?= \ + --toc --toc-depth 2 --html --interpolate \ + --index indexpage --no-lib-name --parse-comments \ + --with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html +export COQDOCFLAGS +COQMAKEFILE ?= Makefile.coq +COQDOCJS_LN ?= false + +coqdoc: $(COQMAKEFILE) + $(MAKE) -f $^ html +ifeq ($(COQDOCJS_LN),true) + ln -sf ../$(EXTRA_DIR)/resources html +else + cp -R $(EXTRA_DIR)/resources html +endif + +.PHONY: coqdoc diff --git a/coqdocjs/README.md b/coqdocjs/README.md new file mode 100644 index 0000000..685d4a3 --- /dev/null +++ b/coqdocjs/README.md @@ -0,0 +1,44 @@ +# CoqdocJS + +CoqdocJS is a little script to dynamically improve the coqdoc output. +The result can be seen here: + +https://www.ps.uni-saarland.de/autosubst/doc/Ssr.POPLmark.html + +It offers the following features: +- Customizable Unicode display: + It only changes the display, copy-paste from the website produces pure ASCII. + It only replaces complete identifiers or notation tokens, possibly terminated by numbers or apostrophes. + It does not replace randomly, like in "omega." or "tauto." + To add new symbols, edit [config.js](extra/resources/config.js). +- Proof hiding: + All proofs longer than one line are hidden by default. They can be uncovered by clicking on "Proof...". + +All of this works with the ordinary coqdoc, by asking coqdoc to use a header file including the javascript files and some custom CSS. + +## Usage + +1. Clone this repository as a subdirectory or submodule; +2. Include [Makefile.doc] in your `Makefile`, or copy it as, e.g., `Makefile.coq.local`; +3. Run `make coqdoc` to build documentations. + +A minimal example is shown [here](example). + +### Environment Variables +Name | Usage | Default +---|---|--- +`COQDOCFLAGS` | Override the flags passed to `coqdoc` | see [Makefile.doc] +`COQDOCEXTRAFLAGS` | Extend the flags passed to `coqdoc` | empty +`COQDOCJS_LN` | If set to `true` then symlink resource files; otherwise copy | `false` +`COQDOCJS_DIR` | Folder containing CoqdocJS | `coqdocjs` +`COQMAKEFILE` | Makefile generated by `coq_makefile` | `Makefile.coq` + +## Files + +- [Makefile.doc]: a generic Makefile setup that calls coqc and coqdoc with the right parameters +- [config.js](extra/resources/config.js): contains the unicode replacement table +- [coqdoc.css](extra/resources/coqdoc.css): a replacement for the default Coqdoc CSS style. Can be removed to use the default style +- [coqdocjs.js](extra/resources/coqdocjs.js) and [coqdocjs.css](extra/resources/coqdocjs.css): the script rewriting the DOM and adding the dynamic features with a corresponding CSS style +- [header.html](extra/header.html) and [footer.html](extra/footer.html): custom header and footer files used in every generated html file + +[Makefile.doc]: Makefile.doc diff --git a/coqdocjs/example/.gitignore b/coqdocjs/example/.gitignore new file mode 100644 index 0000000..a3200a7 --- /dev/null +++ b/coqdocjs/example/.gitignore @@ -0,0 +1,3 @@ +Makefile.coq +Makefile.coq.conf +html/ diff --git a/coqdocjs/example/Makefile b/coqdocjs/example/Makefile new file mode 100644 index 0000000..4829da8 --- /dev/null +++ b/coqdocjs/example/Makefile @@ -0,0 +1,21 @@ +COQMAKEFILE ?= Makefile.coq +COQDOCEXTRAFLAGS = -s +COQDOCJS_LN = true +COQ_PROJ ?= _CoqProject + +all: $(COQMAKEFILE) + $(MAKE) -f $^ $@ + +clean: $(COQMAKEFILE) + $(MAKE) -f $^ cleanall + $(RM) $^ $^.conf + +$(COQMAKEFILE): $(COQ_PROJ) + $(COQBIN)coq_makefile -f $^ -o $@ + +force $(COQ_PROJ) Makefile: ; + +%: $(COQMAKEFILE) force + @+$(MAKE) -f $< $@ + +.PHONY: clean all force diff --git a/coqdocjs/example/Makefile.coq.local b/coqdocjs/example/Makefile.coq.local new file mode 120000 index 0000000..944d6ca --- /dev/null +++ b/coqdocjs/example/Makefile.coq.local @@ -0,0 +1 @@ +coqdocjs/Makefile.doc \ No newline at end of file diff --git a/coqdocjs/example/README.md b/coqdocjs/example/README.md new file mode 100644 index 0000000..8172989 --- /dev/null +++ b/coqdocjs/example/README.md @@ -0,0 +1,4 @@ +# CoqdocJS Usage Example +This folder contains a minimal example to use CoqdocJS in your project. + +You can build the docs with `make coqdoc`. diff --git a/coqdocjs/example/_CoqProject b/coqdocjs/example/_CoqProject new file mode 100644 index 0000000..0471ff8 --- /dev/null +++ b/coqdocjs/example/_CoqProject @@ -0,0 +1,2 @@ +-Q ./ MyProjectName +a.v diff --git a/coqdocjs/example/a.v b/coqdocjs/example/a.v new file mode 100644 index 0000000..a22e167 --- /dev/null +++ b/coqdocjs/example/a.v @@ -0,0 +1,10 @@ +(** * Section *) +Variant foo := bar. (* comments *) + +(** ** Subsection *) +(** Documentations. *) +Example baz : forall f : foo, f = bar. +Proof. + intros []. + reflexivity. +Qed. diff --git a/coqdocjs/example/coqdocjs/Makefile.doc b/coqdocjs/example/coqdocjs/Makefile.doc new file mode 120000 index 0000000..806fdb8 --- /dev/null +++ b/coqdocjs/example/coqdocjs/Makefile.doc @@ -0,0 +1 @@ +../../Makefile.doc \ No newline at end of file diff --git a/coqdocjs/example/coqdocjs/extra b/coqdocjs/example/coqdocjs/extra new file mode 120000 index 0000000..31b3d97 --- /dev/null +++ b/coqdocjs/example/coqdocjs/extra @@ -0,0 +1 @@ +../../extra \ No newline at end of file diff --git a/coqdocjs/extra/footer.html b/coqdocjs/extra/footer.html new file mode 100644 index 0000000..2ff40b3 --- /dev/null +++ b/coqdocjs/extra/footer.html @@ -0,0 +1,8 @@ + + + + + + diff --git a/coqdocjs/extra/header.html b/coqdocjs/extra/header.html new file mode 100644 index 0000000..c064d5a --- /dev/null +++ b/coqdocjs/extra/header.html @@ -0,0 +1,26 @@ + + + + + + + + + + + + + +
+
diff --git a/coqdocjs/extra/resources/config.js b/coqdocjs/extra/resources/config.js new file mode 100644 index 0000000..72be613 --- /dev/null +++ b/coqdocjs/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/coqdocjs/extra/resources/coqdoc.css b/coqdocjs/extra/resources/coqdoc.css new file mode 100644 index 0000000..18dad89 --- /dev/null +++ b/coqdocjs/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/coqdocjs/extra/resources/coqdocjs.css b/coqdocjs/extra/resources/coqdocjs.css new file mode 100644 index 0000000..d94bb58 --- /dev/null +++ b/coqdocjs/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/coqdocjs/extra/resources/coqdocjs.js b/coqdocjs/extra/resources/coqdocjs.js new file mode 100644 index 0000000..7ff5698 --- /dev/null +++ b/coqdocjs/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/docker_image/Dockerfile b/docker_image/Dockerfile index 2f656e1..1134074 100644 --- a/docker_image/Dockerfile +++ b/docker_image/Dockerfile @@ -19,13 +19,13 @@ RUN opam repo add --set-default iris-dev https://gitlab.mpi-sws.org/iris/opam.gi RUN opam switch create stable ocaml.5.2.0 RUN eval $(opam env) RUN opam update -RUN opam install coq.8.19.2 vscoq-language-server -RUN opam install coq-iris.4.2.0 coq-iris-heap-lang +RUN opam install coq.8.20.1 vscoq-language-server +RUN opam install coq-iris.4.3.0 coq-iris-heap-lang RUN opam switch create unstable ocaml.5.2.0 RUN eval $(opam env) RUN opam update -RUN opam install coq.8.19.2 vscoq-language-server +RUN opam install coq.8.20.1 vscoq-language-server RUN opam install coq-iris coq-iris-heap-lang coq-iris-unstable RUN opam switch stable diff --git a/exercises/adequacy.v b/exercises/adequacy.v index 0df1f38..bd9b259 100644 --- a/exercises/adequacy.v +++ b/exercises/adequacy.v @@ -25,7 +25,7 @@ From exercises Require Import spin_lock. Here, [e1] is the expression we want to reduce, and [σ1] is the current state of the machine. [e2] and [σ2] are then the new expression and new state. [efs] is a list of expressions representing - new threads spawned. Finally [κs] represents a list of something + new threads spawned. Finally, [κs] represents a list of something called observations. We won't use these, so [κs] will remain empty. This relation isn't very nice to work with by itself. To fix this, we diff --git a/exercises/array_lock.v b/exercises/array_lock.v index e335362..59ce617 100644 --- a/exercises/array_lock.v +++ b/exercises/array_lock.v @@ -123,7 +123,7 @@ Proof. - intros [[d ->]|[d ->]]. all: rewrite (comm Nat.add) Nat.mul_comm. 2: symmetry. - all: by apply Nat.mod_add. + all: by apply Nat.Div0.mod_add. Qed. Lemma invitation_add (γ : name) (n m : nat) : invitation γ (n + m) ⊣⊢ invitation γ n ∗ invitation γ m. @@ -171,9 +171,8 @@ Proof. iFrame "Ha Hn Hγ Hι". iLeft. iFrame. - rewrite Nat2Z.id Nat.mod_0_l. - - done. - - by apply Nat.lt_neq in Hcap. + rewrite Nat2Z.id Nat.Div0.mod_0_l. + by apply Nat.lt_neq in Hcap. Qed. Lemma wait_spec (γ : name) (l : val) (t cap : nat) (R : iProp Σ) : @@ -196,7 +195,7 @@ Proof. + iPoseProof (lookup_array _ _ _ (t `mod` cap) #true with "Ha") as "[Ht Ha]". { apply list_lookup_insert. - rewrite replicate_length. + rewrite length_replicate. apply Nat.mod_upper_bound. by apply Nat.lt_neq in Hcap. } @@ -425,7 +424,7 @@ Proof. iPoseProof (update_array _ _ _ (o `mod` cap) #true with "Ha") as "[Ht Ha]". { apply list_lookup_insert. - rewrite replicate_length. + rewrite length_replicate. apply Nat.mod_upper_bound. by apply Nat.lt_neq in Hcap. } diff --git a/exercises/arrays.v b/exercises/arrays.v index 63a3627..ccb2a8d 100644 --- a/exercises/arrays.v +++ b/exercises/arrays.v @@ -21,7 +21,7 @@ Context `{heapGS Σ}. (** To see arrays in action, let's implement a function, [copy], that - copies an array, while keeping the original intact. We define it in + copies an array while keeping the original intact. We define it in terms of a more general function, [copy_to]. *) @@ -87,8 +87,8 @@ Proof. Qed. (** - When allocating arrays, heaplang requires the size to be greater - than zero. So we add this to our precondition. + When allocating arrays, HeapLang requires the size to be greater than + zero. So we add this to our precondition. *) Lemma copy_spec a l : {{{a ↦∗ l ∗ ⌜0 < length l⌝}}} @@ -105,7 +105,7 @@ Proof. { iPureIntro. symmetry. - apply replicate_length. + apply length_replicate. } iIntros "[Ha Ha']". wp_pures. @@ -155,10 +155,10 @@ Definition reverse : val := "reverse" ("arr" +ₗ #1) ("len" - #2). (** - Notice we are not following structural induction on the list of - values as we remove elements from both the front and the back. As - such you need to use either löb induction or strong induction on the - size of the list. + Notice we are not following structural induction on the list of values + as we remove elements from both the front and the back. As such, you + need to use either löb induction or strong induction on the size of + the list. *) Lemma reverse_spec a l : {{{a ↦∗ l}}} diff --git a/exercises/basics.v b/exercises/basics.v index 0fef3b4..e9c564e 100644 --- a/exercises/basics.v +++ b/exercises/basics.v @@ -8,7 +8,7 @@ From iris.proofmode Require Import proofmode. (** ** Introduction *) (** - In short, Iris is `higher-order concurrent separation logic + In short, Iris is a `higher-order concurrent separation logic framework'. That is quite a mouthful, so let us break it down. Firstly, the `framework' part means that Iris is not tied to any @@ -38,7 +38,7 @@ From iris.proofmode Require Import proofmode. Finally, `higher-order' refers to the fact that predicates may depend on other predicates. Being a program logic means that programs are proved correct with respect to some specification – a description of - the programs behavior and interaction with resources. As programs are + the program's behavior and interaction with resources. As programs are usually composed of other programs, we would want our specifications to be generic so that they may be used in a myriad of contexts. Having support for higher-order predicates means that program specifications @@ -72,7 +72,7 @@ Context {Σ: gFunctors}. - [P ⊢ Q] asks whether [Q] holds assuming [P] Iris is built on top of Coq, so to smoothen the experience, we will be - working with the Iris Proof Mode (IPM). The practical implications of + working with the Iris Proof Mode (IPM). The practical implication of this is that we get a new context, called the spatial context, in addition to the usual context, now called the non-spatial context. Hypotheses from both contexts can be used to prove the goal. @@ -102,7 +102,7 @@ Proof. (** This adds [P] to the spatial context with the identifier ["H"]. To finish the proof, one would normally use either [exact] or [apply]. - So in Iris we use either [iExact] or [iApply]. + So in Iris, we use either [iExact] or [iApply]. *) iApply "H". Qed. @@ -129,7 +129,7 @@ Qed. entailment [Φ₁ ∗ ... ∗ Φₙ ⊢ Ψ]. Technically, since Iris is built on top of Coq, proving an Iris - entailment in Coq corresponds to proving ⊢ₓ (P ⊢ Q). In other + entailment in Coq corresponds to proving [⊢ₓ (P ⊢ Q)]. In other words, the spatial context is part of the Coq goal. This is the reason why the regular Coq tactics no longer suffice. The new tactics work with both the non-spatial and the spatial contexts. @@ -165,7 +165,7 @@ Definition and_success (P Q : iProp Σ) := (P ∧ Q)%I. (** The core connective in separation logic is the `separating conjunction', written [P ∗ Q], for propositions [P] and [Q]. - Separating conjunction differs from regular conjunction particularly + Separating conjunction differs from regular conjunction, particularly in its introduction rule: [[ @@ -191,16 +191,16 @@ Proof. Unlike [∧], [∗] is not idempotent. Specifically, there are Iris propositions for which [¬(P ⊢ P ∗ P)]. Because of this, it is generally not possible to use [iSplit] to introduce [∗]. The - [iSplit] tactic would duplicate the spatial context, and is - therefore not available when the context is non-empty. + [iSplit] tactic would duplicate the spatial context and is therefore + not available when the context is non-empty. *) Fail iSplit. (** Instead, Iris introduces the tactics [iSplitL] and [iSplitR]. These allow you to specify how you want to separate your resources to - prove each of the subgoals. The hypotheses mentioned by [iSplitL] - are given to the left subgoal, and the remaining to the right. - Conversely for [iSplitR]. + prove each subgoal. The hypotheses mentioned by [iSplitL] are given + to the left subgoal, and the remaining to the right. Conversely for + [iSplitR]. *) iSplitL "HQ". - iApply "HQ". @@ -213,7 +213,7 @@ Qed. introduces it with separating conjunction. This connective is written as [P -∗ Q] and pronounced `magic wand' or simply `wand'. Separation is so widely used that [P -∗ Q] is treated specially; instead of - writing [P ⊢ Q] we can write [P -∗ Q], with the [⊢] being implicit. + writing [P ⊢ Q], we can write [P -∗ Q], with the [⊢] being implicit. That is, [⊢ P -∗ Q] is notationally equivalent to [P -∗ Q]. Writing a wand instead of entailment makes currying more natural. Here @@ -255,7 +255,7 @@ Qed. (** Bi-entailment of Iris propositions is denoted [P ⊣⊢ Q]. It is an - equivalence relation and most connectives preserve this relation. It + equivalence relation, and most connectives preserve this relation. It is encoded using the setoid library with the typeclass [Proper]. It is therefore possible to use the [rewrite] tactic inside the Iris Proof Mode. Bi-entailment is defined as [(P -∗ Q) ∧ (Q -∗ P)], so it can be @@ -284,7 +284,7 @@ Qed. (** Hypotheses that fit arguments exactly can be supplied directly without a square bracket to avoid trivial subgoals, as in the above. Try this - in following exercise. + in the following exercise. *) Lemma wand_adj (P Q R : iProp Σ) : (P -∗ Q -∗ R) ⊣⊢ (P ∗ Q -∗ R). Proof. @@ -327,8 +327,8 @@ Admitted. Iris has existential and universal quantifiers over any Coq type. Existential quantifiers are proved using the [iExists] tactic, using the same syntax as for [exists]. Elimination of existentials is done - through the pattern ["[%_ _]"] or as part of a ["(_&..&_)"] with a [%] in - front of the existential variable. + through the pattern ["[%_ _]"] or as part of a ["(_&..&_)"] with a [%] + in front of the existential variable. *) Lemma sep_ex_distr {A} (P : iProp Σ) (Φ : A → iProp Σ) : (P ∗ ∃ x, Φ x) ⊣⊢ ∃ x, P ∗ Φ x. diff --git a/exercises/counter.v b/exercises/counter.v index 38e61f5..e75df63 100644 --- a/exercises/counter.v +++ b/exercises/counter.v @@ -13,7 +13,7 @@ From iris.heap_lang Require Import lang proofmode notation par. functions: - a constructor, [mk_counter], which creates a new counter starting at [0]. - - an increment function, [incr], which increments the counter, and + - an increment function, [incr], which increments the counter and returns the old value of the counter. - a read function, [read], which reads the current value of the counter. @@ -56,8 +56,8 @@ Definition is_counter1 (v : val) (n : nat) : iProp Σ := (** This predicate is, however, not persistent, so our value would not be - shareable across threads. To fix this we can put the knowledge into an - invariant. + shareable across threads. To fix this, we can put the knowledge into + an invariant. *) Let N := nroot .@ "counter". @@ -67,7 +67,7 @@ Definition is_counter2 (v : val) (n : nat) : iProp Σ := (** However, with this definition, we have locked the value of the pointer - to always be [n]. To fix this we could abstract the value and instead + to always be [n]. To fix this, we could abstract the value and instead only specify its lower bound. *) @@ -75,14 +75,14 @@ Definition is_counter3 (v : val) (n : nat) : iProp Σ := ∃ l : loc, ⌜v = #l⌝ ∗ inv N (∃ m : nat, l ↦ #m ∗ ⌜n ≤ m⌝). (** - Now we can change the what the pointer maps to, but we still cannot - refine the lower bound. + We can now change what the pointer maps to, but we still cannot refine + the lower bound. The final step is to use ghost state. The idea is to link [n] and [m] to pieces of ghost state in such a way that the validity of their composite is [n ≤ m]. - To achieve this we will use the _authoritative_ resource algebra, + To achieve this, we will use the _authoritative_ resource algebra, [auth]. This resource algebra is parametrised by a CMRA, [A]. There are two types of elements in the carrier of the authoritative RA: - [● x] called an authoritative element @@ -268,15 +268,15 @@ Section spec2. total value. To this end, we will use fractions. The [frac] resource algebra is - similar to [dfrac], but without the capability of discarding - fractions. As such, [frac] consists of non-negative rationals with - addition as composition, and a fraction is only valid if it is less - than or equal to [1]. This means that all the fractions can add up to - at most [1]. Combining [frac] with other resource algebras allows us - to keep track of how much of the resource we own, meaning we can do - the exact kind of aggregation we need. So this time we will use the - resource algebra [authR (optionUR (prodR fracR natR))]. Here, [natR] - is the natural numbers with addition. + similar to [dfrac] but without the capability of discarding fractions. + As such, [frac] consists of non-negative rationals with addition as + composition, and a fraction is only valid if it is less than or equal + to [1]. This means that all the fractions can add up to at most [1]. + Combining [frac] with other resource algebras allows us to keep track + of how much of the resource we own, meaning we can do the exact kind + of aggregation we need. So this time, we will use the resource algebra + [authR (optionUR (prodR fracR natR))]. Here, [natR] is the natural + numbers with addition. *) Context `{!heapGS Σ, !inG Σ (authR (optionUR (prodR fracR natR)))}. @@ -315,7 +315,7 @@ Qed. (** When allocating a new state, there will be _one_ fragment, which contains the entire fraction. Using the above lemma, we can then split - up the fragment, and supply these fragments to participating threads. + up the fragment and supply these fragments to participating threads. *) Lemma alloc_initial_state : ⊢ |==> ∃ γ, own γ (● Some (1%Qp, 0)) ∗ own γ (◯ Some (1%Qp, 0)). @@ -357,8 +357,8 @@ Proof. Qed. (** - However, when a fragment has the entire fraction, then there can't be - any other fragments – intuitively, we have collected all contributions + However, when a fragment has the entire fraction, there can't be any + other fragments – intuitively, we have collected all contributions from all threads. So the count stored in the fragment must be equal to the one in the authoritative element. *) @@ -401,7 +401,7 @@ Qed. (** Let us prove the specifications for the counter functions again. This time, however, we will have two specifications for [read] – one with - an arbitrary fraction, and one with the whole fraction. + an arbitrary fraction and one with the whole fraction. *) Lemma mk_counter_spec : diff --git a/exercises/custom_ra.v b/exercises/custom_ra.v index 98a1d00..442aa68 100644 --- a/exercises/custom_ra.v +++ b/exercises/custom_ra.v @@ -20,12 +20,11 @@ Definition prog : expr := (** We wish to show that the program terminates with a number that is at - least [5]. To do this we will use an invariant separated into the + least [5]. To do this, we will use an invariant separated into the different abstract states of our program. At the outset, the location will map to [4]. During the execution of the threads, the location - will be changed to either [5] or [6]. However, we just care about that - it must become greater than [4]. As such we will have the following - states. + will be changed to either [5] or [6]. However, we just care about it + becoming greater than [4]. As such, we will have the following states. *) Inductive state := @@ -41,7 +40,7 @@ Inductive state := (** The [state] data structure will be our carrier for the RA. To use - [state] as a resource algebra we need to turn it into a resource + [state] as a resource algebra, we need to turn it into a resource algebra, meaning we need it to adhere to [RAMixin]. As such, we must define an equivalence relation, composition, the core, and valid elements, and prove that these definitions satisfy the fields in @@ -60,13 +59,13 @@ Section state. Global Instance state_equiv_instance : Equiv state := eq. Global Instance state_equiv_equivalence : Equivalence (≡@{state}) := _. (** - To help convert between equivalence and equality we can tell Iris + To help convert between equivalence and equality, we can tell Iris that they coincide, which in this case is trivial. *) Global Instance state_leibniz_equiv : LeibnizEquiv state := _. (** - Recall that resource algebras are discrete cameras, and that cameras + Recall that resource algebras are discrete cameras and that cameras build on OFEs (Ordered family of equivalences). As such, to define a resources algebra, we must first define its OFE. An OFE encodes a kind of time dependence, but when the camera is _discrete_ and hence a @@ -167,7 +166,7 @@ Proof. red. done. Qed. Lemma state_update s : s ~~> Final. Proof. (** - As we are working with a discrete CMRA we can simplify this + As we are working with a discrete CMRA, we can simplify this statement as follows. *) rewrite cmra_discrete_update. @@ -186,7 +185,7 @@ Context `{!inG Σ stateR}. Our first lemma shows how a new State resource is created. We can create new resources via the basic update modality [|==> P]. This operation states that P holds after an update of resources. To work - with the update modality we can use two facts: + with the update modality, we can use two facts: - [P ⊢ |==> P] - [(P ⊢ |==> Q) ⊢ (|==> P ⊢ |==> Q)] Rather than working with these facts directly, we can use @@ -194,7 +193,7 @@ Context `{!inG Σ stateR}. *) Lemma alloc_Start : ⊢ |==> ∃ γ, own γ Start. Proof. - (** To allocate a new resource we use [own_alloc]. *) + (** To allocate a new resource, we use [own_alloc]. *) iApply own_alloc. (** We are naturally only allowed to allocate valid resources, but since @@ -205,8 +204,8 @@ Qed. (** Likewise, owning a resource means that it is valid. - A quick note: [✓ _] and [⌜✓ _⌝] are different, they only coincide when - the CMRA is discrete. + A quick note: [✓ _] and [⌜✓ _⌝] are different – they only coincide + when the CMRA is discrete. *) Lemma state_valid γ (s : state) : own γ s ⊢ ⌜✓ s⌝. Proof. @@ -243,15 +242,14 @@ Context `{!heapGS Σ, !spawnG Σ, !inG Σ stateR}. Let N := nroot .@ "state". (** - We can now define the invariant we hinted to in the beginning as - follows. + We can now define the invariant we hinted at in the beginning. *) Definition state_inv γ (l : loc) (x : Z) : iProp Σ := ∃ y : Z, l ↦ #y ∗ (own γ Start ∗ ⌜x = y⌝ ∨ own γ Final ∗ ⌜x < y⌝%Z). (** Rather than proving the entire program at once, we will split it into - 3 pieces, starting with the 2 threads. + three pieces, starting with the two threads. Note that WP contains an update modality, meaning we can update resources in between steps. diff --git a/exercises/invariants.v b/exercises/invariants.v index 6e79e74..8a07af6 100644 --- a/exercises/invariants.v +++ b/exercises/invariants.v @@ -36,8 +36,8 @@ Proof. *) wp_apply (wp_fork with "[Hl]"). (** - As such we have to pick a thread to own [l]. But as both threads - need to access [l], we are stuck. + As such, we must pick a thread to own [l]. But as both threads need + to access [l], we are stuck. *) Abort. @@ -49,11 +49,11 @@ Section inv_intro. (** As the above program illustrates, some resources are required by multiple threads simultaneously. If those resources are not shareable - (i.e. persistent), then we will get stuck, as in the example above. - To get around this problem, we can devise an invariant for said + (i.e. persistent), then we will get stuck, as in the example above. To + get around this problem, we can devise an invariant for said resources. That is, we come up with a proposition [P] which describes the resources in a way that is always true, no matter where in the - program we are, or how threads have interleaved. We can then use Iris' + program we are or how threads have interleaved. We can then use Iris' invariant functionality to assert that [P] is an invariant: [inv N P]. Here, [N] is a `namespace', which we may think of as the name of the invariant. @@ -119,13 +119,13 @@ Abort. Another example of a goal permitting invariant openings is the _fancy update modality_, which essentially just adds a mask to the update modality. A fancy update modality is written [|={E}=>] for a mask [E]. - The fancy update modality is like the update modality, but with - support for invariants: if the goal contains [|={E}=>], then we are - allowed to open all invariants in [E]. + The fancy update modality is like the update modality but with support + for invariants: if the goal contains [|={E}=>], then we are allowed to + open all invariants in [E]. *) (** - Another restriction on invariant openings is that, when the goal is a + Another restriction on invariant openings is that when the goal is a weakest precondition [WP e {{Φ}}], an invariant can be open for at most one program step. This is enforced by requiring [e] to be an atomic expression, meaning it reduces to a value in one step. After @@ -168,7 +168,7 @@ Proof. *) iInv "Hinv" as "Hl". (** - This tactic did quit a bit, so let us break it down. + This tactic did quite a bit, so let us break it down. Firstly, notice that we got the points-to predicate from the invariant. A small caveat is that we only get the predicate later. @@ -176,7 +176,7 @@ Proof. cases, which we discuss in a later chapter. Secondly, the postcondition of the weakest precondition in the goal - got augmented with [|={⊤ ∖ ↑N}=> ▷ l ↦ #1]. After stepping through + was augmented with [|={⊤ ∖ ↑N}=> ▷ l ↦ #1]. After stepping through the current WP, we will have to prove this proposition to show that the invariant [l ↦ #1] still holds. The fancy update modality is there to stop us from opening the invariant to prove that the @@ -224,7 +224,7 @@ Proof. (** We have now used the invariant to reduce the right-hand [!#l]. Reducing the left-hand dereference is done analogously. - First we bind the dereference. + First, we bind the dereference. *) wp_bind (!#l)%E. (** Then we open the invariant. *) @@ -299,7 +299,7 @@ Qed. Side note: The above proof demonstrates why, when we have to prove the postcondition of a WP, we have to prove it _behind_ a fancy update modality. Having the fancy update modality in the goal allows us to - allocate/open invariants, and allocate/update resources. + allocate/open invariants and allocate/update resources. *) End inv_intro. @@ -329,7 +329,7 @@ Proof. rewrite /prog. wp_alloc l as "Hl". wp_pures. - (** We now allocate our [prog_inv] invariant, using [inv_alloc]. *) + (** We now allocate our [prog_inv] invariant using [inv_alloc]. *) iMod (inv_alloc N _ (prog_inv l) with "[Hl]") as "#Hinv". (** We prove that the invariant is currently true. *) { @@ -369,7 +369,7 @@ End proofs. (** Let us look at another program. This program will create a thread to - continuously increment a counter, while the main thread will read the + continuously increment a counter while the main thread will read the counter at some point. As such, this program should produce some non-negative number. However, we will only prove that it returns a number. Later, we will see other tools that will allow us to refine diff --git a/exercises/lang.v b/exercises/lang.v index 455595f..44a7968 100644 --- a/exercises/lang.v +++ b/exercises/lang.v @@ -7,7 +7,7 @@ From iris.heap_lang Require Import lang notation spawn par. (** ** Introduction *) (** - HeapLang is a untyped concurrent programming language with a heap. It + HeapLang is an untyped concurrent programming language with a heap. It is an ML-like language, sporting many of the usual constructs such as let expressions, lambda abstractions, and recursive functions. It also supports higher-order functions. The evaluation order is right to left @@ -15,7 +15,7 @@ From iris.heap_lang Require Import lang notation spawn par. The syntax for HeapLang is fairly standard, but there are some quirks as we are working inside Coq. As the features of HeapLang are fairly - standard, the focus in this chapter is manly on showcasing the syntax + standard, the focus in this chapter is mainly on showcasing the syntax of the language through simple examples. *) @@ -28,7 +28,7 @@ From iris.heap_lang Require Import lang notation spawn par. [iris.unstable.heap_lang]. The interpreter provides the function [exec], which takes as input some fuel and an expression. The expression is then executed until it terminates at a value [v], the - execution runs out fuel, or the program gets stuck. In case of + execution runs out of fuel, or the program gets stuck. In case of termination, [inl v] is returned. Otherwise [inr err] is returned, with [err] describing the error. *) @@ -268,7 +268,7 @@ Example cas : expr := instruction [Fork e] creates a new thread which executes [e]. The invoking thread continues execution after creation. If the computation of [e] terminates, then the resulting value is simply thrown away. - Hence, [e] is only run for its side-effects. + Hence, [e] is only run for its side effects. *) Example fork : expr := diff --git a/exercises/later.v b/exercises/later.v index a7be626..a10e703 100644 --- a/exercises/later.v +++ b/exercises/later.v @@ -18,7 +18,7 @@ Context `{!heapGS Σ}. The later modality is used quite extensively in Iris. We have already seen that it is used to define Hoare triples, but it has many more - uses. For instance, it is a prime tool to reason about recursive + uses. For instance, it is a prime tool for reasoning about recursive programs. It can be used to write specifications that capture the minimum number of steps taken by a program. It is also an integral part of working with invariants, which we introduce in a later @@ -26,11 +26,11 @@ Context `{!heapGS Σ}. *) (** - The later modality is monotone meaning that if we know [P ⊢ Q], then + The later modality is monotone, meaning that if we know [P ⊢ Q], then we can also conclude [▷ P ⊢ ▷ Q]. In words, if we know that [P] - entails [Q], then we also know that, if we get [P] after one step, we + entails [Q], then we also know that if we get [P] after one step, we will also get [Q] after one step. This is captured by the [iNext] - tactic, which introduces a later, while stripping laters from our + tactic, which introduces a later while stripping laters from our hypotheses. *) @@ -72,7 +72,7 @@ Qed. (** The later modality distributes over [∧], [∨], [∗], and is preserved - by [∃] and [∀]. This means that we can destruct these constructs + by [∃] and [∀]. This means we can destruct these constructs regardless of being prefaced by any laters. *) @@ -111,8 +111,8 @@ Admitted. To see this in action, let us look at a simple program: [1 + 2 + 3]. This program takes two steps to evaluate, so we can prove that if a - proposition holds after two steps, then it will hold after the program - has terminated. + proposition holds after two steps, it will hold after the program has + terminated. *) Lemma take_2_steps (P : iProp Σ) : ▷ ▷ P -∗ WP #1 + #2 + #3 {{_, P}}. @@ -154,15 +154,15 @@ Qed. (** ** Löb Induction *) (** - The later modality allows for a strong induction principle, called Löb - induction. Essentially, Löb induction states that, to prove a + The later modality allows for a strong induction principle called Löb + induction. Essentially, Löb induction states that to prove a proposition [P], we are allowed to assume that [P] holds later, i.e. [▷ P]. Formally, we have [□ (▷ P -∗ P) -∗ P]. Recall that [▷] represents a single step in the logic. Löb induction essentially performs induction in the number of steps. Intuitively, Löb induction - states that, if we can show that whenever [P] holds for strictly - smaller than [n] steps we can prove that [P] holds for [n] steps, then - [P] holds for all steps. + states that if we can show that whenever [P] holds for strictly + smaller than [n] steps, we can prove that [P] holds for [n] steps, + then [P] holds for all steps. We can use this principle to prove many properties of recursive programs. To see this in action, we will define a simple recursive @@ -174,7 +174,7 @@ Example count : val := (** This function never terminates for any input as it will keep calling - itself with larger and larger inputs. To show this we pick the + itself with larger and larger inputs. To show this, we pick the postcondition [False]. We can now use Löb induction, along with [wp_rec], to prove this specification. *) @@ -184,13 +184,13 @@ Proof. (** The tactic for Löb induction, [iLöb], requires us to specify the name of the induction hypothesis, which we here call ["IH"]. - Optionally, it can also forall quantify any of our variables before - performing induction. We here forall quantify [x] as it changes for - every recursive call. + Optionally, it can also universally quantify over any of our variables + before performing induction. We here universally quantify over [x] as it + changes for every recursive call. *) iLöb as "IH" forall (x). (** - [iLöb] automatically introduces the forall quantified variables in + [iLöb] automatically introduces the universally quantified variables in the goal, so we can proceed to execute the function. *) wp_rec. diff --git a/exercises/linked_lists.v b/exercises/linked_lists.v index e92daf9..98951c5 100644 --- a/exercises/linked_lists.v +++ b/exercises/linked_lists.v @@ -25,7 +25,7 @@ Fixpoint isList (l : val) (xs : list val) : iProp Σ := *) (** - Now we can define HeapLang functions that act on lists, such as [inc]. + We can now define HeapLang functions that act on lists, such as [inc]. The [inc] function recursively increments all the values of a list. *) Definition inc : val := @@ -41,7 +41,7 @@ Definition inc : val := (** Intuitively, the specification we give for this function should state - that the linked list should only contain integers, and that, after + that the linked list should only contain integers and that, after executing the function, each integer has been incremented. As such, we parametrise the specification not by a list of values, but by a list of integers. We then map each integer to a HeapLang value using [# _], @@ -53,9 +53,9 @@ Lemma inc_spec (l : val) (xs : list Z) : {{{ RET #(); isList l ((λ x, #(x + 1)) <$> xs)}}}. Proof. (** - The proof proceeds by structural induction in [xs]. As [l] changes - in each iteration, we must forall quantify it to strengthen the - induction hypothesis. + The proof proceeds by structural induction in [xs]. As [l] changes in each + iteration, we must universally quantify over it to strengthen the induction + hypothesis. *) revert l. induction xs as [|x xs' IH]; simpl. @@ -101,7 +101,7 @@ Proof. Admitted. (** - We will implement reverse using a helper function, called + We will implement reverse using a helper function called [reverse_append], which takes two arguments, [l] and [acc], and returns the list [rev l ++ acc]. *) @@ -117,7 +117,7 @@ Definition reverse_append : val := end. (** - When acc is the empty list, it should thus simply return the reverse + When [acc] is the empty list, it should thus simply return the reverse of [l]. *) Definition reverse : val := @@ -134,7 +134,7 @@ Proof. Admitted. (** - Now we use the specification of [reverse_append] to prove the + Now, we use the specification of [reverse_append] to prove the specification of [reverse]. *) Lemma reverse_spec (l : val) (xs : list val) : @@ -184,7 +184,7 @@ Definition fold_right : val := - Importantly, we do not change the original list. So we put [isList l xs] in the postcondition. - Note that Hoare triples are persistent and persistent predicates are + Note that Hoare triples are persistent, and persistent predicates are closed under universal quantification. Hence, in the proof, the assumption for [f] will move into the persistent context. *) diff --git a/exercises/merge_sort.v b/exercises/merge_sort.v index 499e790..0f33ae9 100644 --- a/exercises/merge_sort.v +++ b/exercises/merge_sort.v @@ -10,7 +10,7 @@ From iris.heap_lang Require Import array lang proofmode notation par. (** Let us implement a simple multithreaded merge sort on arrays. Merge sort consists of splitting the array in half until we are left with - pieces of size [0] or [1]. Then each pair of pieces is merged into a + pieces of size [0] or [1]. Then, each pair of pieces is merged into a new sorted array. *) diff --git a/exercises/ofe.v b/exercises/ofe.v index 06d18f0..58cb39c 100644 --- a/exercises/ofe.v +++ b/exercises/ofe.v @@ -10,7 +10,7 @@ From iris.algebra Require Export ofe. Iris. However, they form good intuition about the usefulness of OFEs. We will look at streams over natural numbers. These are infinite - sequences with [head] being the first value, and [tail] being the rest + sequences with [head] being the first value and [tail] being the rest of the stream. We define streams as a coinductive type. You should be able to follow this file without extensive knowledge of coinduction. *) @@ -29,7 +29,7 @@ Add Printing Constructor stream. CoFixpoint zeros := SCons 0 zeros. (** - [CoFixpoints] allows us to build coinductive values, in the same way + [CoFixpoints] allows us to build coinductive values in the same way that [Fixpoint] allows us to use inductive types recursively. We can get the [n]'th element of the stream by iterating through the @@ -42,7 +42,7 @@ Fixpoint nth (s : stream) (n : nat) : nat := end. (** - We can likewise define a stream from its [n]'th elements + We can likewise define a stream from its [n]'th elements. *) CoFixpoint fun2stream (f : nat → nat) : stream := SCons (f 0) (fun2stream (f ∘ S)). @@ -62,11 +62,11 @@ Local Instance stream_equiv_instance : Equiv stream := λ s1 s2, ∀ n, nth s1 n = nth s2 n. (** - Now for the OFE structure, we introduce the concept of approximate + Now, for the OFE structure, we introduce the concept of approximate equivalence using the typeclass [Dist]. This typeclass defines a family of equivalence relations written - [[x ≡{n}≡ y]] where [n] is the precision. In our case this will + [[x ≡{n}≡ y]] where [n] is the precision. In our case, this will decide how many of the elements of the stream we look at. *) Local Instance stream_dist_instance : Dist stream := λ n s1 s2, @@ -99,8 +99,8 @@ End ofe. (** We can now ask the question of whether we can build values from a - sequence of better and better approximations. To this end we use the - concept of a chain. Here chains are sequences such that all elements + sequence of better and better approximations. To this end, we use the + concept of a chain. Here, chains are sequences such that all elements after the [n]'th element are [n]-equivalent. An OFE is complete if all chains approach a value. This is also called a COFE for complete OFE. @@ -207,7 +207,7 @@ Fixpoint sapp (l : list nat) (s : stream) : stream := (** This operation is [NonExpansive] when we fix the list we wish to prepend. Furthermore, we can prove this without unfolding the - definition of [dist], by using what we have proved so far. + definition of [dist] by using what we have proved thus far. *) Global Instance sapp_ne (l : list nat) : NonExpansive (sapp l). Proof. @@ -218,8 +218,8 @@ Global Instance sapp_proper (l : list nat) : Proper ((≡) ==> (≡)) (sapp l). Proof. apply ne_proper, _. Qed. (** - Now let's define a stream that simply repeats a list over and over - again. Intuitively we should be able to define it as follows: + Now, let's define a stream that simply repeats a list over and over + again. Intuitively, we should be able to define it as follows: *) Fail CoFixpoint repeat (l : list nat) : stream := sapp l (repeat l). @@ -230,7 +230,7 @@ Fail CoFixpoint repeat (l : list nat) : stream := result remains empty. So we will never end up with an infinite stream. - To fix this we can insert a separator in between the repetitions of + To fix this, we can insert a separator in between the repetitions of the list: *) Fail CoFixpoint repeat_with_sep (l : list nat) (x : nat) : stream := @@ -240,7 +240,7 @@ Fail CoFixpoint repeat_with_sep (l : list nat) (x : nat) : stream := But this still fails with the same error. This is because Coq uses a simple syntactic check to validate co-fixpoint definitions. - To satisfy this check we are forced to syntactically produce at least + To satisfy this check, we are forced to syntactically produce at least one element of the stream per recursive call, which is violated by the call to [sapp]. In practice, this means that we cannot reuse most of our existing operations when writing new recursively defined streams. @@ -256,8 +256,8 @@ Definition repeat_with_sep (l : list nat) (x : nat) := repeat_with_sep_helper l x l. (** - To be sure that this definition is correct, we can show that it still - solves the fixpoint equation. To do this we first need to show that + To ensure that this definition is correct, we can show that it still + solves the fixpoint equation. To do this, we first need to show that the helper function does what it is supposed to. *) Lemma repeat_with_sep_helper_unfold (l : list nat) (x : nat) (helper : list nat) : @@ -294,7 +294,7 @@ Global Instance repeat_with_sep_contractive (l : list nat) (x : nat) : Contracti Proof. solve_contractive. Qed. (** - To get a fixpoint for such a function we need three things: + To get a fixpoint for such a function, we need three things: - The type we wish to produce an element of (stream) must have a COFE structure, which we defined earlier. - The function we wish to find a fixpoint for must be contractive, @@ -342,7 +342,7 @@ CoFixpoint stream_map (f : nat → nat) (s : stream) : stream := just build this as a fixpoint on streams. Instead, we need to build a fixpoint on [stream → stream]. However, this is not equipped with a canonical OFE structure. Instead, we need to write - [stream -d> streamO]. Here [d] stands for discrete, meaning we don't + [stream -d> streamO]. Here, [d] stands for discrete, meaning we don't consider any OFE structure on the domain. As such, we are allowed to change the parameter arbitrarily on recursive calls. *) @@ -398,7 +398,7 @@ Fail CoFixpoint power2 : stream := However, this again fails the syntactic check, as we are modifying the tail of the stream. - To fix this we could instead define a stream starting with a number + To fix this, we could instead define a stream starting with a number [n] doubling [n] at every step. *) CoFixpoint power2_helper (n : nat) : stream := @@ -430,7 +430,7 @@ Definition power2_pre (s : stream) : stream := SCons 1 (stream_map (λ n, n * 2) s). (** - This is again contractive in [s], because [SCons] is [Contractive] and + This is again contractive in [s] because [SCons] is [Contractive] and [stream_map] is [NonExpansive]. *) Global Instance power2_pre_contractive : Contractive power2_pre. @@ -458,7 +458,7 @@ Qed. propositions recursively, we can use [fixpoint]. Importantly, all the connectives of the logic are [NonExpansive]. To then use guarded fixpoints, we need a [Contractive] function like [SCons]. And for - [iProp] this is later [▷ P]. We have already run into two connectives + [iProp], this is later [▷ P]. We have already run into two connectives defined using the guarded-fixpoint, namely the weakest precondition [WP], and invariants [inv]. This is why we can remove laters from premises when taking a step in the program, as this corresponds to diff --git a/exercises/persistently.v b/exercises/persistently.v index 05df8be..1d4b2bd 100644 --- a/exercises/persistently.v +++ b/exercises/persistently.v @@ -14,7 +14,7 @@ Context `{!heapGS Σ}. (** In separation logic, propositions are generally not duplicable. This is because resources are generally exclusive. However, resources do - not _have_ to be exclusive. A great example of this is `read only + not _have_ to be exclusive. A great example of this is `read-only memory'. There is no danger in letting many threads access the same location simultaneously if they can only read from it. Hence, it would not make sense to require that ownership of those locations be @@ -26,7 +26,7 @@ Context `{!heapGS Σ}. intuitionistic logic, which is why they are also sometimes referred to as intuitionistic. - A propositions is persistent when [P ⊢ □ P]. That is, assuming [P], we + A proposition is persistent when [P ⊢ □ P]. That is, assuming [P], we need to show that [P] does not rely on any exclusive resources. Persistency is preserved by most connectives, so proving that a proposition is persistent is usually a matter of showing that the @@ -92,10 +92,10 @@ Proof. Admitted. (** - Persistent propositions satisfy a lot of nice properties, simply by + Persistent propositions satisfy a lot of nice properties simply by being duplicable [P ⊢ P ∗ P]. For example, [P ∧ Q] and [P ∗ Q] - coincide, when either [P] or [Q] is persistent. Likewise, [P → Q] and - [P -∗ Q] coincide, when [P] is persistent. + coincide when either [P] or [Q] is persistent. Likewise, [P → Q] and + [P -∗ Q] coincide when [P] is persistent. *) Check bi.persistent_and_sep. @@ -111,9 +111,9 @@ Check bi.impl_wand. (** ** Proving Persistency *) (** - To prove a proposition [□ P], we have to prove [P] without assuming - any exclusive resources. In other words, we have to throw away the - spatial context when proving [P]. + To prove a proposition [□ P], we must prove [P] without assuming any + exclusive resources. In other words, we have to throw away the spatial + context when proving [P]. *) Lemma pers_intro (P Q : iProp Σ) `{!Persistent P} : P ∗ Q ⊢ □ P. @@ -169,8 +169,8 @@ Proof. iModIntro. (** By default, [iFrame] will not frame propositions from the - persistent context. To make it do so, we have to give it the - argument ["#"]. + persistent context. To make it do so, we must give it the argument + ["#"]. *) iFrame "#". - (* exercise *) @@ -220,7 +220,7 @@ Proof. apply _. Qed. (** For more complicated predicates, such as ones defined as a fixpoint, [Persistent] cannot automatically infer its persistence. The following - predicate asserts that all values in a given list is equal to [5]. + predicate asserts that all values in a given list are equal to [5]. *) Fixpoint myPredFix (xs : list val) : iProp Σ := @@ -259,7 +259,7 @@ Proof. apply _. Qed. -(** Now, Iris recognises [myPredFix] as persistent. *) +(** Iris now recognises [myPredFix] as persistent. *) Lemma first_is_5 (x : val) (xs : list val) : myPredFix (x :: xs) -∗ ⌜x = #5⌝ ∗ myPredFix (x :: xs). @@ -278,7 +278,7 @@ Qed. (** Thus far, the only basic persistent propositions we have seen are pure - propositions, such as equalities. In this section we introduce two + propositions, such as equalities. In this section, we introduce two additional examples of persistent propositions: Hoare triples and persistent points-to predicates. *) @@ -288,7 +288,7 @@ Qed. (** All Hoare triples are persistent. This probably does not come as a - surprise, if the reader recalls how we defined Hoare triples in the + surprise if the reader recalls how we defined Hoare triples in the [specifications] chapter. As a reminder, here is the definition again. [□( ∀ Φ, P -∗ ▷ (∀ r0 .. rn, Q -∗ Φ v) -∗ WP e {{v, Φ v }})] @@ -343,7 +343,7 @@ Context `{spawnG Σ}. [l ↦ dq v], where [dq] is a `discarded fraction'. We return to the `discarded' part momentarily, but for now, we assume that [dq] is a fraction in the interval (0; 1]. The predicate [l ↦ v] is a special - case, where the fraction [dq] is [1]. The basic idea is that points-to + case where the fraction [dq] is [1]. The basic idea is that points-to predicates can be split up and recombined, allowing ownership of points-to predicates to be shared. *) @@ -381,7 +381,7 @@ Abort. (** Fractional points-to predicates are especially useful in scenarios - where a location is read by multiple threads in parallel, but later + where a location is read by multiple threads in parallel but later only used by a single thread. *) @@ -397,7 +397,7 @@ Proof. iIntros (Φ) "[Hl1 Hl2] HΦ". rewrite /par_read_write. (** - The idea is to give each thread half of the points-to predicate, and + The idea is to give each thread half of the points-to predicate and assert that both will return their halves afterwards. *) set t_post := (λ w : val, (⌜w = v⌝ ∗ l ↦{#1 / 2} v)%I). diff --git a/exercises/pure.v b/exercises/pure.v index 8c75410..b141c7c 100644 --- a/exercises/pure.v +++ b/exercises/pure.v @@ -62,9 +62,9 @@ Qed. It is quite easy to show that the propositions [⌜5 = 5⌝] and [⌜x = y⌝] from above are pure. However, it can become quite burdensome for more complicated Iris propositions. Fortunately, Iris has two typeclasses - [IntoPure] and [FromPure] which can identify pure propositions for us. - These are used by the [iPureIntro] tactic to automatically identify - pure propositions. + [IntoPure] and [FromPure] that can identify pure propositions for us. + These are used by the [iPureIntro] tactic to identify pure + propositions automatically. *) (** [True] is pure. *) diff --git a/exercises/resource_algebra.v b/exercises/resource_algebra.v index b2d9a12..e272205 100644 --- a/exercises/resource_algebra.v +++ b/exercises/resource_algebra.v @@ -17,9 +17,9 @@ From iris.heap_lang Require Import lang proofmode notation. resources uniformly – we define a fixed set of criteria that a notion of resource must satisfy in order to be used in the logic. If the notion satisfies those criteria, then it is a `resource algebra' - (often shorted to `RA'). We can then have a small handful of rules for - resource algebras in general, and we hence do not need to change the - logic every time we wish to use a new notion of a resource. + (often shortened to `RA'). We can then have a small handful of rules + for resource algebras in general, and we hence do not need to change + the logic every time we wish to use a new notion of a resource. In this way, resource algebras are oblivious to the existence of Iris – they exist as a separate thing. Iris then has a mechanism to embed @@ -30,7 +30,7 @@ From iris.heap_lang Require Import lang proofmode notation. A small side note: in Iris, resource algebras are specialisations of the more general structure `CMRA' (in particular, resource algebras are `discrete' CMRAs). In turn, CMRAs are built on top of `Ordered - Families of Equations' (shortened to `OFE'). The exact details of + Families of Equivalences' (shortened to `OFE'). The exact details of these concepts are not important for this chapter, but we mention them as they appear a few times throughout the chapter. CMRAs and OFEs are covered in more detail in later chapters. @@ -110,7 +110,7 @@ Print RAMixin. expresses that, if [y ≡ z], then [x ⋅ y ≡ x ⋅ z], for all [x]. The fields [ra_assoc] and [ra_comm] assert that the operation [⋅] - should be associative and commutative. This in effect makes [A] a + should be associative and commutative. This, in effect, makes [A] a commutative semigroup, which means that we can make all resource algebras a preorder through the extension order, written [x ≼ y]. The extension order is defined as: @@ -121,7 +121,7 @@ Print RAMixin. [y] in terms of [x] and some [z]. The fields [ra_pcore_l] and [ra_pcore_idemp] capture the idea that the - core extracts the shareable part of a resource, and how shareable + core extracts the shareable part of a resource and how shareable resources behave. [ra_pcore_l] expresses that including the same shareable resource multiple times does not change a resource, and [ra_pcore_idemp] states that invoking the core on a resource twice @@ -324,10 +324,9 @@ Proof. Qed. Lemma dfrac_valid_discarded : ✓ (DfracDiscarded). -(* Solution *) Proof. - rewrite dfrac_valid. - done. -Qed. +Proof. + (* exercise *) +Admitted. Lemma dfrac_invalid_own : ¬ (✓ (DfracOwn (2/3) ⋅ DfracOwn (2/3))). Proof. @@ -392,16 +391,14 @@ Proof. Qed. Lemma dfrac_pre_disc_both : DfracDiscarded ≼ DfracBoth (3/4). -(* Solution *) Proof. - exists (DfracOwn (3/4)). - compute_done. -Qed. +Proof. + (* exercise *) +Admitted. Lemma dfrac_pre_own_both : DfracOwn (2/4) ≼ DfracBoth (3/4). -(* Solution *) Proof. - exists (DfracBoth (1/4)). - compute_done. -Qed. +Proof. + (* exercise *) +Admitted. (* ----------------------------------------------------------------- *) (** *** Frame Preserving Update *) @@ -411,14 +408,14 @@ Qed. update resources – resources are used to reason about programs, and programs update resources. One has to be careful with how resources are allowed to be updated; in Iris, only _valid_ resources can be - owned. It should always be the case that, if we combine the resources + owned. It should always be the case that if we combine the resources owned by all threads in the system, the resulting resource should be valid. Otherwise, we could easily derive falsehood. Hence, when a thread updates its resources, it must ensure that it does not introduce the possibility of obtaining an invalid element. We call - such an update a `frame preserving Update', and write [x ~~> y] to - mean that we can perform a frame preserving update from resource [x] - to resource [y]. The formal definition for this notion turns out to be + such an update a `frame preserving update' and write [x ~~> y] to mean + that we can perform a frame preserving update from resource [x] to + resource [y]. The formal definition for this notion turns out to be quite succinct: [x ~~> y = ∀z, ✓(x ⋅ z) → ✓(y ⋅ z)] @@ -427,7 +424,7 @@ Qed. also valid with [y]. If this is the case, then it is okay to update [x] to [y]. Since [z] is forall quantified, [z] also represents the resource we get by combining the resources from all other threads. - That is to say, [x ~~> y] ensures that, if the combination of all + That is to say, [x ~~> y] ensures that if the combination of all resources was valid before the update, it still is after. As [z] represents all the other resources, it is called the `frame', and the proposition [x ~~> y] expresses that the validity of [z] – the frame – @@ -555,7 +552,7 @@ Admitted. concepts of resource algebra. While dfrac has some use cases on its own, it is especially useful when composed with other resource algebra (e.g. it is used to define the points-to predicate). Hence, in this - section, we will introduce some often used resource algebras. + section, we will introduce some often-used resource algebras. Unlike dfrac, the resource algebras we study in this section are parametrised by other resource algebras (or OFEs, or CMRAs). This @@ -636,7 +633,7 @@ End exclusive. (** So how is this resource algebra useful? While it is a key component in - many fairly complex resource algebras, it has a super simple, yet + many fairly complex resource algebras, it has a super simple yet extremely practical use case. Together with the OFE [unitO], we can create the resource algebra of `tokens'. *) @@ -684,7 +681,7 @@ Context {A : ofe}. carrier of resource algebra), and all it cares about is whether two resources are equivalent. That is, whether they _agree_. As such, the carrier of agree is the same as the carrier of the underlying resource - algebra, and all resources in [agree A] are valid – irregardless of + algebra, and all resources in [agree A] are valid – regardless of their validity in the original resource algebra. *) @@ -748,12 +745,9 @@ Qed. Lemma agree_valid_opL (a b : A) : ✓ (to_agree a ⋅ to_agree b) → to_agree a ⋅ to_agree b ≡ to_agree a. -(* Solution *) Proof. - intros Hvalid. - apply to_agree_op_valid in Hvalid. - rewrite Hvalid. - apply agree_idemp. -Qed. +Proof. + (* exercise *) +Admitted. (** Due to idempotency and the fact that the combination of equivalent @@ -771,7 +765,7 @@ Admitted. (** The usefulness of the agree construction is demonstrated by the fact that it is used to define the resource of heaps. The inclusion of the - agree RA allows us to conclude that, if we have two points-to + agree RA allows us to conclude that if we have two points-to predicates for the same location, [l ↦{dq1} v1] and [l ↦{dq2} v2], then they _agree_ on the value stored at the location: [v1 = v2]. *) @@ -817,7 +811,7 @@ About pair_op. About pair_valid. (** - A pair is included in another pair, if the components of the first are + A pair is included in another pair if the components of the first are included in the components of the second. *) @@ -854,7 +848,7 @@ Qed. (** The product RA is often used in conjunction with dfrac and agree, with - the first component being a dfrac, and the second being an element of + the first component being a dfrac and the second being an element of some resource algebra wrapped in agree. This pattern is common enough that it has been added to Iris' library of resource algebras. *) @@ -889,7 +883,7 @@ Section ghost. in Iris have type [iProp Σ]. The [Σ] can be thought of as a global list of resource algebras that are available in the logic. The [Σ] is always universally quantified to enable composition of proofs. - However, we may put _restrictions_ on [Σ], to specify that the list + However, we may put _restrictions_ on [Σ] to specify that the list must contain some specific resource algebra of our choosing. The typeclass [inG Σ R] expresses that the resource algebra [R] is in the [G]lobal list of resource algebras [Σ]. If we add this to the Coq @@ -944,8 +938,8 @@ Context `{!heapGS Σ}. exactly one way of embedding a resource [r] from some resource algebra [R] into the logic: the proposition [own γ r] asserts _ownership_ of the resource [r] in an instance of the resource algebra [R] named [γ]. - That is to say, in Iris, once we have added a [R] to [Σ], we may - create multiple instances of [R], so that the same resource in [R] may + That is to say, in Iris, once we have added an [R] to [Σ], we may + create multiple instances of [R] so that the same resource in [R] may be owned multiple times. To distinguish between instances, we use `ghost names' (sometimes also called `ghost variables' or `ghost locations'), which is usually written with a lower-case gamma: [γ]. @@ -968,7 +962,7 @@ Definition token (γ : gname) := own γ (Excl ()). defined in terms of [own]. That is, [l ↦ v] is just notation denoting ownership of a resource in the resource of heaps! But where is the ghost name [γ]? When adding the resource of heaps to [Σ], we do it - with the [heapGS Σ] typeclass. Here, the [S] stands for `singleton', + with the [heapGS Σ] typeclass. Here, the [S] stands for `singleton' and signifies that only _one_ instance of the resource of heaps exists. As such, we do not need ghost names to distinguish between instances. @@ -1054,7 +1048,7 @@ Qed. (** Recall that the core extracts the shareable part of a resource. If the core of some resource is itself, then that resource is freely - shareable – in particular ownership of the resource is duplicable. + shareable – in particular, ownership of the resource is duplicable. That is, if [pcore r = Some r], then [own γ r] is persistent. *) @@ -1166,7 +1160,7 @@ Admitted. About own_alloc. (** - That is, if we have some resource algebra [A], and wish to create and + That is, if we have some resource algebra [A] and wish to create and get ownership of resource [a] in [A], then, as long as [a] is valid, we may update our resources to get ownership of [a] in a _fresh_ instance of [A], identified by a fresh ghost name [γ]. @@ -1216,7 +1210,7 @@ Proof. Qed. (** - Exercise: Use [own_dfrac_update] to prove the following hoare triple. + Exercise: Use [own_dfrac_update] to prove the following Hoare triple. *) Lemma hoare_triple_dfrac (γ : gname): diff --git a/exercises/specifications.v b/exercises/specifications.v index 54db743..3c64bd6 100644 --- a/exercises/specifications.v +++ b/exercises/specifications.v @@ -44,7 +44,7 @@ Example arith : expr := (** This program should evaluate to [16]. We can express this in the logic with a weakest precondition. In general, a weakest precondition has - the form [WP e {{v, Φ v}}]. This asserts that, if the HeapLang program + the form [WP e {{v, Φ v}}]. This asserts that if the HeapLang program [e] terminates at some value [v], then [v] satisfies the predicate [Φ]. The double curly brackets [{{v, Φ v}}] is called the `postcondition'. For the case of [arith], we would express its @@ -149,7 +149,7 @@ Example lambda : expr := <> These tactics similarly apply the underlying rules of the logic, - however we shall from now on refrain from explicitly mentioning the + however, we shall from now on refrain from explicitly mentioning the rules applied. Through experience, the reader should get an intuition for how each tactic manipulates the goal. @@ -169,7 +169,7 @@ Admitted. resource of heaps. As mentioned in basics.v, propositions in Iris describe/assert ownership of resources. To describe resources in the resource of heaps, we use the `points-to' predicate, written [l ↦ v]. - Intuitively, this describes all heap fragments that has value [v] + Intuitively, this describes all heap fragments that have value [v] stored at location [l]. The proposition [l1 ↦ #1 ∗ l2 ↦ #2] then describes all heap fragments that map [l1] to [#1] and [l2] to [#2]. @@ -235,7 +235,7 @@ Qed. subgoals. The first corresponds to the case where the [CmpXchg] instruction succeeded. Thus, we get to assume [H1 : v = v1], and our points-to predicate for [l] is updated to [l ↦ v2]. The second - corresponds to case where [CmpXchg] failed. We instead get + corresponds to the case where [CmpXchg] failed. We instead get [H2 : v ≠ v1], and our points-to predicate for [l] is unchanged. Let us demonstrate this with a simple example program which simply @@ -282,7 +282,7 @@ Example cas : expr := #(). (** - The result of both [CAS] instructions are predetermined. Hence, we can + The result of both [CAS] instructions is predetermined. Hence, we can use the [wp_cmpxchg_suc] and [wp_cmpxchg_fail] tactics to symbolically execute them (remember that [CAS l v1 v2] is syntactic sugar for [Snd (CmpXchg l v1 v2)]). @@ -346,10 +346,10 @@ Proof. [WP e {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e {{ Ψ }}]. - With this it suffices to prove that the postcondition of [prog_spec] - implies the postcondition in our current goal. This is achieved with - the [wp_wand] lemma, which generates two subgoals, one corresponding - to [WP e {{ Φ }}] and one to [(∀ v, Φ v -∗ Ψ v)]. + With this, it suffices to prove that the postcondition of + [prog_spec] implies the postcondition in our current goal. This is + achieved with the [wp_wand] lemma, which generates two subgoals, one + corresponding to [WP e {{ Φ }}] and one to [(∀ v, Φ v -∗ Ψ v)]. *) iApply wp_wand; simpl. { iApply prog_spec. } @@ -384,9 +384,9 @@ Qed. Lemma prog_add_2_spec' : ⊢ WP prog + #2 {{ v, ⌜v = #5⌝ }}. Proof. wp_bind prog. - (** The goal is now on the exact form required by [prog_spec_2] *) + (** The goal is now on the exact form required by [prog_spec_2]. *) iApply prog_spec_2. - (** And the proof proceeds as before *) + (** And the proof proceeds as before. *) iIntros "%w ->". wp_pure. done. @@ -394,7 +394,7 @@ Qed. (** We can even simplify this proof further by using the [wp_apply] - tactic which automatically applies [wp_bind] for us. + tactic, which automatically applies [wp_bind] for us. *) Lemma prog_add_2_spec'' : ⊢ WP prog + #2 {{ v, ⌜v = #5⌝ }}. wp_apply prog_spec_2. @@ -412,7 +412,7 @@ Qed. precondition does not explicitly specify which conditions must be met before executing the program. It only talks about which conditions are met after – the postcondition. Hoare triples build on weakest - preconditions by requiring us to explicitly mention the the conditions + preconditions by requiring us to explicitly mention the conditions that must hold before running the program – the precondition. The syntax for Hoare triples is as follows: @@ -433,7 +433,7 @@ Qed. Firstly, inspired by the [prog_spec_2] example from the previous section, this definition makes the postcondition generic. Next, the precondition [P] implies the generic weakest precondition, - signifying that we must first prove [P] before we can apply + signifying that we must first prove [P] before we can apply the specification for [e]. Finally, the definition uses two modalities that we have yet to cover. The persistently modality [□] signifies that the specification can be @@ -493,12 +493,12 @@ Proof. Qed. (** - A convention in Iris is to write specifications using Hoare triples, + A convention in Iris is to write specifications using Hoare triples but prove them by converting them to weakest preconditions as in the examples above. There are several reasons for this. Firstly, it ensures that all specifications are generic in the postcondition. Secondly, specifications written in terms of Hoare triples are usually - easier to read, as they name explicitly what must be obtained before + easier to read, as they explicitly name what must be obtained before the program can be executed. Finally, proving Hoare triples directly can be quite awkward and burdensome, especially in Coq. *) @@ -569,7 +569,7 @@ Proof. iIntros (Φ _) "HΦ". rewrite /par_client. (** - The program starts by creating two fresh location, [l1] and [l2]. + The program starts by creating two fresh locations, [l1] and [l2]. *) wp_alloc l1 as "Hl1". wp_let. @@ -587,7 +587,7 @@ Proof. (** We can now apply the [wp_par] specification. Note how we transfer ownership of [l1 ↦ #0] to the first thread, and [l2 ↦ #0] to the - second. This allows each thread to perform their store operations. + second. This allows each thread to perform its store operation. *) wp_apply (wp_par t1_post t2_post with "[Hl1] [Hl2]"). (** diff --git a/exercises/spin_lock.v b/exercises/spin_lock.v index 1fd4264..8803071 100644 --- a/exercises/spin_lock.v +++ b/exercises/spin_lock.v @@ -20,10 +20,10 @@ Definition mk_lock : val := (** To acquire the lock, we use [CAS l false true] (compare and set). This - instruction atomically writes [true] to location [l], if [l] contains + instruction atomically writes [true] to location [l] if [l] contains [false]. The [CAS] instruction then returns a boolean, signifying whether [l] was updated. If the [CAS] fails, it means that the lock is - currently acquired somewhere else. So we simply try again, until the lock + currently acquired somewhere else. So we simply try again until the lock is free. *) Definition acquire : val := @@ -68,7 +68,7 @@ Context `{heapGS Σ}. algebra is generic. However, we just need one exclusive element, so we will instantiate the exclusive RA with the unit OFE: [exclR unitO]. Note that this is exactly the resource algebra we used to define - tokens. As such, we will reuse tokens here, but rename them to clarify + tokens. As such, we will reuse tokens here but rename them to clarify their intent. *) Context `{!tokenG Σ}. @@ -139,7 +139,7 @@ Proof. Qed. (** - Acquiring the lock should grant access to the protected resources, as + Acquiring the lock should grant access to the protected resources as well as knowledge that the lock has been locked. *) Lemma acquire_spec γ v P : @@ -201,7 +201,7 @@ Definition prog : expr := (** [x] can take on the values of [0], [1], and [7]. However, we should - not observe [7], as it is overridden before the lock is released. + not observe [7], as it is overwritten before the lock is released. *) Lemma prog_spec : ⊢ WP prog {{ v, ⌜v = #0 ∨ v = #1⌝}}. Proof. diff --git a/exercises/structured_conc.v b/exercises/structured_conc.v index e6cd1d3..64b4e91 100644 --- a/exercises/structured_conc.v +++ b/exercises/structured_conc.v @@ -25,7 +25,7 @@ From iris.heap_lang Require Import lang proofmode notation. The library definitions additionally give and prove specifications for the constructs, which we have used in previous chapters. In this - chapter, we will define the constructs from scratch, and write our own + chapter, we will define the constructs from scratch and write our own specifications for them. *) @@ -46,11 +46,11 @@ From iris.heap_lang Require Import lang proofmode notation. About wp_fork. (** - For convenience, we included it here as well in `simplified' form. + For convenience, we include it here as well in `simplified' form. [WP e {{_, True}} -∗ ▷ Φ #() -∗ WP Fork e {{v, Φ v}}] - That is, to show a weakest precondition of [Fork e] we have to show + That is, to show a weakest precondition of [Fork e], we have to show the weakest precondition of [e] for a trivial postcondition. The key point is that we only require the forked-off thread to be safe – we do not care about its return value, hence the trivial postcondition. @@ -101,12 +101,12 @@ Definition join: val := {{{ P }}} spawn f {{{ h, RET h; join_handle h Ψ }}} ]] - This states that, to get a specification for [spawn f], we first must + This states that to get a specification for [spawn f], we first must prove a specification for [f] which captures which resources [f] needs, [P], and what the value [f] terminates at satisfies, [Ψ]. If we can prove such a specification for [f], then, given [P], we can also run [spawn f], which will return a value [h] which satisfies a - `join-handle' predicate. This predicate is a promise that, if we + `join-handle' predicate. This predicate is a promise that if we invoke [join] with [h], then the value we get back satisfies [Ψ]. This is reflected in the specification for [join]: @@ -123,7 +123,7 @@ Context `{!heapGS Σ}. Let N := nroot .@ "handle". (** - Since we are using a shared channel we will use an invariant to allow + Since we are using a shared channel, we will use an invariant to allow the two (concurrently running) threads to access it. An initial attempt at stating this invariant looks as follows. *) @@ -132,7 +132,7 @@ Definition handle_inv1 (l : loc) (Ψ : val → iProp Σ) : iProp Σ := (** The stated invariant governs the shared channel (some location [l]) - and states that either no value has been sent yet, or some value has + and states that either no value has been sent yet or some value has been sent that satisfies the predicate [Ψ]. We can then use the invariant to define the [join_handle] predicate. @@ -162,8 +162,10 @@ Proof. by iApply "IH". - wp_load. iModIntro. - (** Now we need [HΨ] to reestablish the invariant but we also need it for - the postcondition. We are stuck... *) + (** + Now we need [HΨ] to reestablish the invariant, but we also need it + for the postcondition. We are stuck... + *) Abort. (** @@ -189,7 +191,7 @@ Definition handle_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ (** This enables the owner of the token to open the invariant, extract [Ψ w], and close the invariant in the case that mentions the token. As - such, we include the token in the join handle, so that [join] gets + such, we include the token in the join handle so that [join] gets access to the token. *) @@ -334,7 +336,7 @@ Context `{!heapGS Σ, !tokenG Σ}. (** It is actually quite straightforward to prove the [par] specification - as most of the heavy lifting is done by [spawn_spec] and [par_spec]. + as most of the heavy lifting is done by [spawn_spec] and [join_spec]. *) Lemma par_spec (P1 P2 : iProp Σ) (e1 e2 : expr) (Q1 Q2 : val → iProp Σ) : {{{ P1 }}} e1 {{{ v, RET v; Q1 v }}} -∗ @@ -364,7 +366,7 @@ Proof. wp_pures. (** Next, we execute [e2] in the current thread using its specification, - ["H2"], which gives us that, if [e2] terminates at some value [v2], + ["H2"], which gives us that if [e2] terminates at some value [v2], then [Q2 v2]. *) wp_apply ("H2" with "HP2"). diff --git a/exercises/ticket_lock.v b/exercises/ticket_lock.v index 55eb9da..db34fc6 100644 --- a/exercises/ticket_lock.v +++ b/exercises/ticket_lock.v @@ -14,12 +14,12 @@ From iris.heap_lang Require Import lang proofmode notation. lock makes them wait in line. It functions similarly to a ticketing system that one often finds in bakeries and pharmacies. Upon entering the shop, you pick a ticket with some number and wait until the number - on the screen has reached your number. Once this happen, it becomes + on the screen has reached your number. Once this happens, it becomes your turn to speak to the shop assistant. In our scenario, talking to the shop assistant corresponds to accessing the protected resources. To implement this, we will maintain two counters: [o] and [n]. The - first counter, [o], represent the number on the screen – the customer + first counter, [o], represents the number on the screen – the customer currently being served. The second counter, [n], represents the next number to be dispensed by the ticketing machine. @@ -27,7 +27,7 @@ From iris.heap_lang Require Import lang proofmode notation. and keep its previous value as a ticket for a position in the queue. Once the ticket has been obtained, the thread must wait until the first counter, [o], reaches its ticket value. Once this happens, the - thread gets access the protected resources. The thread can then + thread gets access to the protected resources. The thread can then release the lock by incrementing the first counter. *) @@ -55,9 +55,9 @@ Definition release : val := (** As a ticket lock is a lock, we expect it to satisfy the same - specification as the spin-lock. This time you have to come up with the - necessary resource algebra and lock invariant by yourself. It might be - instructive to first look through all required predicates and + specification as the spin-lock. This time, you have to come up with + the necessary resource algebra and lock invariant by yourself. It + might be instructive to first look through all required predicates and specifications to figure out exactly what needs to be proven. *) diff --git a/exercises/ticket_lock_advanced.v b/exercises/ticket_lock_advanced.v new file mode 100644 index 0000000..fa01560 --- /dev/null +++ b/exercises/ticket_lock_advanced.v @@ -0,0 +1,187 @@ +From iris.algebra Require Import auth excl gset numbers. +From iris.base_logic.lib Require Export invariants. +From iris.heap_lang Require Import lang proofmode notation. + +(* ################################################################# *) +(** * Case Study: Ticket Lock Advanced *) + +(** + The implementation, resource algebra, and representation predicates + are identical to the original Ticket Lock chapter. Only the proofs + differ. +*) + +(* ================================================================= *) +(** ** Implementation *) + +Definition mk_lock : val := + λ: <>, (ref #0, ref #0). + +Definition wait : val := + rec: "wait" "n" "l" := + let: "o" := !(Fst "l") in + if: "o" = "n" then #() else "wait" "n" "l". + +Definition acquire : val := + rec: "acquire" "l" := + let: "n" := !(Snd "l") in + if: CAS (Snd "l") "n" ("n" + #1) then + wait "n" "l" + else + "acquire" "l". + +Definition release : val := + λ: "l", Fst "l" <- ! (Fst "l") + #1. + +(* ================================================================= *) +(** ** Representation Predicates *) + +Definition RA : cmra := + authR (prodUR (optionUR (exclR natO)) (gset_disjR nat)). + +Section proofs. +Context `{!heapGS Σ, !inG Σ RA}. +Let N := nroot .@ "ticket_lock". + +Definition locked_by (γ : gname) (o : nat) : iProp Σ := + own γ (◯ (Excl' o, GSet ∅)). + +Definition locked (γ : gname) : iProp Σ := + ∃ o, locked_by γ o. + +Lemma locked_excl γ : locked γ -∗ locked γ -∗ False. +Proof. + iIntros "[%o1 H1] [%o2 H2]". + iDestruct (own_valid_2 with "H1 H2") as %[]%auth_frag_valid_1; done. +Qed. + +Definition issued (γ : gname) (x : nat) : iProp Σ := + own γ (◯ (ε : option (excl nat), GSet {[x]})). + +Definition lock_inv (γ : gname) (lo ln : loc) (P : iProp Σ) : iProp Σ := + ∃ o n : nat, lo ↦ #o ∗ ln ↦ #n ∗ + own γ (● (Excl' o, GSet (set_seq 0 n))) ∗ + ( + (locked_by γ o ∗ P) ∨ + issued γ o + ). + +Definition is_lock (γ : gname) (l : val) (P : iProp Σ) : iProp Σ := + ∃ lo ln : loc, ⌜l = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln P). + +(* ================================================================= *) +(** ** Specifications *) + +Lemma mk_lock_spec P : + {{{ P }}} mk_lock #() {{{ γ l, RET l; is_lock γ l P }}}. +Proof. + iIntros "%Φ HP HΦ". + wp_lam. + wp_alloc lo; wp_alloc ln. + wp_pures. + iMod (own_alloc (● (Excl' 0, GSet ∅) ⋅ ◯ (Excl' 0, GSet ∅))) as "(%γ & Hγ & Ho)". + { by apply auth_both_valid_discrete. } + iApply ("HΦ" $! γ). + iExists _, _; iSplitR; first done. + iApply inv_alloc; iExists 0, 0; eauto with iFrame. +Qed. + +Lemma wait_spec γ l P x : + {{{ is_lock γ l P ∗ issued γ x }}} + wait #x l + {{{ RET #(); locked γ ∗ P }}}. +Proof. + iIntros "%Φ [(%lo & %ln & -> & #I) Hx] HΦ". + iLöb as "IH". + wp_rec. + wp_pures. + wp_bind (! _)%E. + iInv "I" as "(%o & %n & Hlo & Hln & Hγ)". + wp_load. + destruct (decide (o = x)) as [->|]. + - iDestruct "Hγ" as "[Hγ [[Hexcl HP]|Ho]]". + + iSplitL "Hlo Hln Hγ Hx"; first by iExists _, _; iFrame. + iModIntro. + wp_pures. + rewrite bool_decide_eq_true_2 //. + wp_pures. + by iApply "HΦ"; iFrame. + + iDestruct (own_valid_2 with "Hx Ho") as + %[_ Hvl%gset_disj_valid_op]%auth_frag_valid_1; + set_solver. + - iSplitL "Hlo Hln Hγ"; first by iExists _, _; iFrame. + iModIntro. + wp_pures. + rewrite bool_decide_eq_false_2; last naive_solver. + wp_pures. + iApply ("IH" with "Hx HΦ"). +Qed. + +Lemma acquire_spec γ l P : + {{{ is_lock γ l P }}} acquire l {{{ RET #(); locked γ ∗ P }}}. +Proof. + iIntros "%Φ (%lo & %ln & -> & #I) HΦ". + iLöb as "IH". + wp_rec. + wp_pures. + wp_bind (! _)%E. + iInv "I" as "(%o & %n & Hlo & Hln & Hγ)". + wp_load. + iSplitL "Hlo Hln Hγ"; first by iExists _, _; iFrame. + clear o. + iModIntro. + wp_pures. + wp_bind (CmpXchg _ _ _). + iInv "I" as "(%o & %n' & Hlo & Hln & Hγ)". + destruct (decide (n' = n)) as [->|]. + - wp_cmpxchg_suc. + rewrite Z.add_comm -(Nat2Z.inj_add 1) /=. + iDestruct "Hγ" as "[Hγ Hγ']". + iMod (own_update _ _ (● (Excl' o, GSet (set_seq 0 (S n))) ⋅ ◯ (ε, GSet {[n]})) with "Hγ") as "[Hγ Hn]". + { + apply auth_update_alloc, prod_local_update_2. + rewrite set_seq_S_end_union_L /=. + apply gset_disj_alloc_empty_local_update; apply (set_seq_S_end_disjoint 0). + } + iSplitL "Hlo Hln Hγ Hγ'"; first by iExists _, _; iFrame. + iModIntro. + wp_pures. + wp_apply (wait_spec with "[I $Hn]"); first iExists _, _; eauto. + - wp_cmpxchg_fail; first naive_solver. + iModIntro. + iSplitL "Hlo Hln Hγ"; first by iExists _, _; iFrame. + wp_pures. + by iApply "IH". +Qed. + +Lemma release_spec γ l P : + {{{ is_lock γ l P ∗ locked γ ∗ P }}} release l {{{ RET #(); True }}}. +Proof. + iIntros "%Φ ((%lo & %ln & -> & #I) & [%o Hexcl] & HP) HΦ". + wp_lam. + wp_pures. + wp_bind (! _)%E. + iInv "I" as "(%o' & %n & Hlo & Hln & [Hγ [[>Hexcl' _]|Ho]])". + { by iDestruct (own_valid_2 with "Hexcl Hexcl'") as %[]%auth_frag_valid_1. } + wp_load. + iDestruct (own_valid_2 with "Hγ Hexcl") as + %[[<-%Excl_included%leibniz_equiv _]%pair_included _]%auth_both_valid_discrete. + iModIntro. + iSplitL "Hlo Hln Hγ Ho"; first by iFrame. + clear n. + wp_pures. + rewrite Z.add_comm -(Nat2Z.inj_add 1) /=. + iInv "I" as "(%o' & %n & Hlo & Hln & [Hγ [[>Hexcl' _]|Ho]])". + { by iDestruct (own_valid_2 with "Hexcl Hexcl'") as %[]%auth_frag_valid. } + wp_store. + iDestruct (own_valid_2 with "Hγ Hexcl") as + %[[<-%Excl_included%leibniz_equiv _]%pair_included _]%auth_both_valid_discrete. + iCombine "Hγ Hexcl" as "Hγ". + iMod (own_update _ _ (● (Excl' (S o), GSet (set_seq 0 n)) ⋅ ◯ (Excl' (S o), ε)) with "Hγ") as "[Hγ Hexcl]". + { by apply auth_update, prod_local_update_1, option_local_update, exclusive_local_update. } + iModIntro. + iSplitR "HΦ"; last by iApply "HΦ". + iExists _, _; eauto with iFrame. +Qed. + +End proofs. diff --git a/exercises/timeless.v b/exercises/timeless.v index 31721ba..342b217 100644 --- a/exercises/timeless.v +++ b/exercises/timeless.v @@ -14,7 +14,7 @@ Context `{!heapGS Σ}. A large class of propositions do not depend on time; they are either always true or always false. An example is equalities; [2 + 2 = 4] is always true. We call such propositions _timeless_. All pure - propositions are timeless and ownership of a resource is timeless if + propositions are timeless, and ownership of a resource is timeless if the resource comes from a resource algebra (this includes points-to predicates). Further, timelessness is preserved by most connectives. As a rule of thumb, a predicate is timeless if @@ -89,7 +89,7 @@ Qed. (** The last scenario we mention is when the goal contains a later. In - this case, we may remove laters from timeless hypotheses, without + this case, we may remove laters from timeless hypotheses without removing the later from the goal. *) @@ -105,7 +105,7 @@ Qed. (** Timeless propositions are especially useful in connection with - invariants. Recall from the invariants chapter that, when we open an + invariants. Recall from the invariants chapter that when we open an invariant, [inv N P], we only get the resources _later_, [▷P]. Often, however, we require the resources now. Consider the following example. *) diff --git a/iris-tutorial.opam b/iris-tutorial.opam index 1d4cedf..4b892aa 100644 --- a/iris-tutorial.opam +++ b/iris-tutorial.opam @@ -10,7 +10,7 @@ bug-reports: "https://github.com/logsem/iris-tutorial/issues" build: [make "-j%{jobs}%"] install: [] depends: [ - "coq" { (= "8.19.2") } - "coq-iris" { (= "4.2.0") } - "coq-iris-heap-lang" { (= "4.2.0") } + "coq" { (= "8.20.1") } + "coq-iris" { (= "4.3.0") } + "coq-iris-heap-lang" { (= "4.3.0") } ] diff --git a/theories/adequacy.v b/theories/adequacy.v index cc63544..f7ae28b 100644 --- a/theories/adequacy.v +++ b/theories/adequacy.v @@ -25,7 +25,7 @@ From solutions Require Import spin_lock. Here, [e1] is the expression we want to reduce, and [σ1] is the current state of the machine. [e2] and [σ2] are then the new expression and new state. [efs] is a list of expressions representing - new threads spawned. Finally [κs] represents a list of something + new threads spawned. Finally, [κs] represents a list of something called observations. We won't use these, so [κs] will remain empty. This relation isn't very nice to work with by itself. To fix this, we diff --git a/theories/array_lock.v b/theories/array_lock.v index e335362..59ce617 100644 --- a/theories/array_lock.v +++ b/theories/array_lock.v @@ -123,7 +123,7 @@ Proof. - intros [[d ->]|[d ->]]. all: rewrite (comm Nat.add) Nat.mul_comm. 2: symmetry. - all: by apply Nat.mod_add. + all: by apply Nat.Div0.mod_add. Qed. Lemma invitation_add (γ : name) (n m : nat) : invitation γ (n + m) ⊣⊢ invitation γ n ∗ invitation γ m. @@ -171,9 +171,8 @@ Proof. iFrame "Ha Hn Hγ Hι". iLeft. iFrame. - rewrite Nat2Z.id Nat.mod_0_l. - - done. - - by apply Nat.lt_neq in Hcap. + rewrite Nat2Z.id Nat.Div0.mod_0_l. + by apply Nat.lt_neq in Hcap. Qed. Lemma wait_spec (γ : name) (l : val) (t cap : nat) (R : iProp Σ) : @@ -196,7 +195,7 @@ Proof. + iPoseProof (lookup_array _ _ _ (t `mod` cap) #true with "Ha") as "[Ht Ha]". { apply list_lookup_insert. - rewrite replicate_length. + rewrite length_replicate. apply Nat.mod_upper_bound. by apply Nat.lt_neq in Hcap. } @@ -425,7 +424,7 @@ Proof. iPoseProof (update_array _ _ _ (o `mod` cap) #true with "Ha") as "[Ht Ha]". { apply list_lookup_insert. - rewrite replicate_length. + rewrite length_replicate. apply Nat.mod_upper_bound. by apply Nat.lt_neq in Hcap. } diff --git a/theories/arrays.v b/theories/arrays.v index 9d51c33..21da373 100644 --- a/theories/arrays.v +++ b/theories/arrays.v @@ -21,7 +21,7 @@ Context `{heapGS Σ}. (** To see arrays in action, let's implement a function, [copy], that - copies an array, while keeping the original intact. We define it in + copies an array while keeping the original intact. We define it in terms of a more general function, [copy_to]. *) @@ -87,8 +87,8 @@ Proof. Qed. (** - When allocating arrays, heaplang requires the size to be greater - than zero. So we add this to our precondition. + When allocating arrays, HeapLang requires the size to be greater than + zero. So we add this to our precondition. *) Lemma copy_spec a l : {{{a ↦∗ l ∗ ⌜0 < length l⌝}}} @@ -105,7 +105,7 @@ Proof. { iPureIntro. symmetry. - apply replicate_length. + apply length_replicate. } iIntros "[Ha Ha']". wp_pures. @@ -173,10 +173,10 @@ Definition reverse : val := "reverse" ("arr" +ₗ #1) ("len" - #2). (** - Notice we are not following structural induction on the list of - values as we remove elements from both the front and the back. As - such you need to use either löb induction or strong induction on the - size of the list. + Notice we are not following structural induction on the list of values + as we remove elements from both the front and the back. As such, you + need to use either löb induction or strong induction on the size of + the list. *) Lemma reverse_spec a l : {{{a ↦∗ l}}} @@ -201,9 +201,9 @@ Lemma reverse_spec a l : destruct l as [|v1 l]; first done. clear H. change (v1 :: ?l) with ([v1] ++ l) at 2. - rewrite !rev_app_distr app_length Nat2Z.inj_add /=. + rewrite !rev_app_distr length_app Nat2Z.inj_add /=. rewrite !array_cons !array_app !array_singleton. - rewrite rev_length Loc.add_assoc. + rewrite length_rev Loc.add_assoc. iDestruct "Ha" as "(Hv1 & Hl & Hv2)". wp_pures. wp_load. diff --git a/theories/basics.v b/theories/basics.v index c607df0..d04bb2b 100644 --- a/theories/basics.v +++ b/theories/basics.v @@ -8,7 +8,7 @@ From iris.proofmode Require Import proofmode. (** ** Introduction *) (** - In short, Iris is `higher-order concurrent separation logic + In short, Iris is a `higher-order concurrent separation logic framework'. That is quite a mouthful, so let us break it down. Firstly, the `framework' part means that Iris is not tied to any @@ -38,7 +38,7 @@ From iris.proofmode Require Import proofmode. Finally, `higher-order' refers to the fact that predicates may depend on other predicates. Being a program logic means that programs are proved correct with respect to some specification – a description of - the programs behavior and interaction with resources. As programs are + the program's behavior and interaction with resources. As programs are usually composed of other programs, we would want our specifications to be generic so that they may be used in a myriad of contexts. Having support for higher-order predicates means that program specifications @@ -72,7 +72,7 @@ Context {Σ: gFunctors}. - [P ⊢ Q] asks whether [Q] holds assuming [P] Iris is built on top of Coq, so to smoothen the experience, we will be - working with the Iris Proof Mode (IPM). The practical implications of + working with the Iris Proof Mode (IPM). The practical implication of this is that we get a new context, called the spatial context, in addition to the usual context, now called the non-spatial context. Hypotheses from both contexts can be used to prove the goal. @@ -102,7 +102,7 @@ Proof. (** This adds [P] to the spatial context with the identifier ["H"]. To finish the proof, one would normally use either [exact] or [apply]. - So in Iris we use either [iExact] or [iApply]. + So in Iris, we use either [iExact] or [iApply]. *) iApply "H". Qed. @@ -129,7 +129,7 @@ Qed. entailment [Φ₁ ∗ ... ∗ Φₙ ⊢ Ψ]. Technically, since Iris is built on top of Coq, proving an Iris - entailment in Coq corresponds to proving ⊢ₓ (P ⊢ Q). In other + entailment in Coq corresponds to proving [⊢ₓ (P ⊢ Q)]. In other words, the spatial context is part of the Coq goal. This is the reason why the regular Coq tactics no longer suffice. The new tactics work with both the non-spatial and the spatial contexts. @@ -165,7 +165,7 @@ Definition and_success (P Q : iProp Σ) := (P ∧ Q)%I. (** The core connective in separation logic is the `separating conjunction', written [P ∗ Q], for propositions [P] and [Q]. - Separating conjunction differs from regular conjunction particularly + Separating conjunction differs from regular conjunction, particularly in its introduction rule: [[ @@ -191,16 +191,16 @@ Proof. Unlike [∧], [∗] is not idempotent. Specifically, there are Iris propositions for which [¬(P ⊢ P ∗ P)]. Because of this, it is generally not possible to use [iSplit] to introduce [∗]. The - [iSplit] tactic would duplicate the spatial context, and is - therefore not available when the context is non-empty. + [iSplit] tactic would duplicate the spatial context and is therefore + not available when the context is non-empty. *) Fail iSplit. (** Instead, Iris introduces the tactics [iSplitL] and [iSplitR]. These allow you to specify how you want to separate your resources to - prove each of the subgoals. The hypotheses mentioned by [iSplitL] - are given to the left subgoal, and the remaining to the right. - Conversely for [iSplitR]. + prove each subgoal. The hypotheses mentioned by [iSplitL] are given + to the left subgoal, and the remaining to the right. Conversely for + [iSplitR]. *) iSplitL "HQ". - iApply "HQ". @@ -213,7 +213,7 @@ Qed. introduces it with separating conjunction. This connective is written as [P -∗ Q] and pronounced `magic wand' or simply `wand'. Separation is so widely used that [P -∗ Q] is treated specially; instead of - writing [P ⊢ Q] we can write [P -∗ Q], with the [⊢] being implicit. + writing [P ⊢ Q], we can write [P -∗ Q], with the [⊢] being implicit. That is, [⊢ P -∗ Q] is notationally equivalent to [P -∗ Q]. Writing a wand instead of entailment makes currying more natural. Here @@ -261,7 +261,7 @@ Qed. (** Bi-entailment of Iris propositions is denoted [P ⊣⊢ Q]. It is an - equivalence relation and most connectives preserve this relation. It + equivalence relation, and most connectives preserve this relation. It is encoded using the setoid library with the typeclass [Proper]. It is therefore possible to use the [rewrite] tactic inside the Iris Proof Mode. Bi-entailment is defined as [(P -∗ Q) ∧ (Q -∗ P)], so it can be @@ -290,7 +290,7 @@ Qed. (** Hypotheses that fit arguments exactly can be supplied directly without a square bracket to avoid trivial subgoals, as in the above. Try this - in following exercise. + in the following exercise. *) Lemma wand_adj (P Q R : iProp Σ) : (P -∗ Q -∗ R) ⊣⊢ (P ∗ Q -∗ R). (* BEGIN SOLUTION *) @@ -362,8 +362,8 @@ END TEMPLATE *) Iris has existential and universal quantifiers over any Coq type. Existential quantifiers are proved using the [iExists] tactic, using the same syntax as for [exists]. Elimination of existentials is done - through the pattern ["[%_ _]"] or as part of a ["(_&..&_)"] with a [%] in - front of the existential variable. + through the pattern ["[%_ _]"] or as part of a ["(_&..&_)"] with a [%] + in front of the existential variable. *) Lemma sep_ex_distr {A} (P : iProp Σ) (Φ : A → iProp Σ) : (P ∗ ∃ x, Φ x) ⊣⊢ ∃ x, P ∗ Φ x. diff --git a/theories/counter.v b/theories/counter.v index a5dbfef..5e4eaf5 100644 --- a/theories/counter.v +++ b/theories/counter.v @@ -13,7 +13,7 @@ From iris.heap_lang Require Import lang proofmode notation par. functions: - a constructor, [mk_counter], which creates a new counter starting at [0]. - - an increment function, [incr], which increments the counter, and + - an increment function, [incr], which increments the counter and returns the old value of the counter. - a read function, [read], which reads the current value of the counter. @@ -56,8 +56,8 @@ Definition is_counter1 (v : val) (n : nat) : iProp Σ := (** This predicate is, however, not persistent, so our value would not be - shareable across threads. To fix this we can put the knowledge into an - invariant. + shareable across threads. To fix this, we can put the knowledge into + an invariant. *) Let N := nroot .@ "counter". @@ -67,7 +67,7 @@ Definition is_counter2 (v : val) (n : nat) : iProp Σ := (** However, with this definition, we have locked the value of the pointer - to always be [n]. To fix this we could abstract the value and instead + to always be [n]. To fix this, we could abstract the value and instead only specify its lower bound. *) @@ -75,14 +75,14 @@ Definition is_counter3 (v : val) (n : nat) : iProp Σ := ∃ l : loc, ⌜v = #l⌝ ∗ inv N (∃ m : nat, l ↦ #m ∗ ⌜n ≤ m⌝). (** - Now we can change the what the pointer maps to, but we still cannot - refine the lower bound. + We can now change what the pointer maps to, but we still cannot refine + the lower bound. The final step is to use ghost state. The idea is to link [n] and [m] to pieces of ghost state in such a way that the validity of their composite is [n ≤ m]. - To achieve this we will use the _authoritative_ resource algebra, + To achieve this, we will use the _authoritative_ resource algebra, [auth]. This resource algebra is parametrised by a CMRA, [A]. There are two types of elements in the carrier of the authoritative RA: - [● x] called an authoritative element @@ -327,15 +327,15 @@ Section spec2. total value. To this end, we will use fractions. The [frac] resource algebra is - similar to [dfrac], but without the capability of discarding - fractions. As such, [frac] consists of non-negative rationals with - addition as composition, and a fraction is only valid if it is less - than or equal to [1]. This means that all the fractions can add up to - at most [1]. Combining [frac] with other resource algebras allows us - to keep track of how much of the resource we own, meaning we can do - the exact kind of aggregation we need. So this time we will use the - resource algebra [authR (optionUR (prodR fracR natR))]. Here, [natR] - is the natural numbers with addition. + similar to [dfrac] but without the capability of discarding fractions. + As such, [frac] consists of non-negative rationals with addition as + composition, and a fraction is only valid if it is less than or equal + to [1]. This means that all the fractions can add up to at most [1]. + Combining [frac] with other resource algebras allows us to keep track + of how much of the resource we own, meaning we can do the exact kind + of aggregation we need. So this time, we will use the resource algebra + [authR (optionUR (prodR fracR natR))]. Here, [natR] is the natural + numbers with addition. *) Context `{!heapGS Σ, !inG Σ (authR (optionUR (prodR fracR natR)))}. @@ -374,7 +374,7 @@ Qed. (** When allocating a new state, there will be _one_ fragment, which contains the entire fraction. Using the above lemma, we can then split - up the fragment, and supply these fragments to participating threads. + up the fragment and supply these fragments to participating threads. *) Lemma alloc_initial_state : ⊢ |==> ∃ γ, own γ (● Some (1%Qp, 0)) ∗ own γ (◯ Some (1%Qp, 0)). @@ -416,8 +416,8 @@ Proof. Qed. (** - However, when a fragment has the entire fraction, then there can't be - any other fragments – intuitively, we have collected all contributions + However, when a fragment has the entire fraction, there can't be any + other fragments – intuitively, we have collected all contributions from all threads. So the count stored in the fragment must be equal to the one in the authoritative element. *) @@ -460,7 +460,7 @@ Qed. (** Let us prove the specifications for the counter functions again. This time, however, we will have two specifications for [read] – one with - an arbitrary fraction, and one with the whole fraction. + an arbitrary fraction and one with the whole fraction. *) Lemma mk_counter_spec : diff --git a/theories/custom_ra.v b/theories/custom_ra.v index c4d5f85..9862cea 100644 --- a/theories/custom_ra.v +++ b/theories/custom_ra.v @@ -20,12 +20,11 @@ Definition prog : expr := (** We wish to show that the program terminates with a number that is at - least [5]. To do this we will use an invariant separated into the + least [5]. To do this, we will use an invariant separated into the different abstract states of our program. At the outset, the location will map to [4]. During the execution of the threads, the location - will be changed to either [5] or [6]. However, we just care about that - it must become greater than [4]. As such we will have the following - states. + will be changed to either [5] or [6]. However, we just care about it + becoming greater than [4]. As such, we will have the following states. *) Inductive state := @@ -41,7 +40,7 @@ Inductive state := (** The [state] data structure will be our carrier for the RA. To use - [state] as a resource algebra we need to turn it into a resource + [state] as a resource algebra, we need to turn it into a resource algebra, meaning we need it to adhere to [RAMixin]. As such, we must define an equivalence relation, composition, the core, and valid elements, and prove that these definitions satisfy the fields in @@ -60,13 +59,13 @@ Section state. Global Instance state_equiv_instance : Equiv state := eq. Global Instance state_equiv_equivalence : Equivalence (≡@{state}) := _. (** - To help convert between equivalence and equality we can tell Iris + To help convert between equivalence and equality, we can tell Iris that they coincide, which in this case is trivial. *) Global Instance state_leibniz_equiv : LeibnizEquiv state := _. (** - Recall that resource algebras are discrete cameras, and that cameras + Recall that resource algebras are discrete cameras and that cameras build on OFEs (Ordered family of equivalences). As such, to define a resources algebra, we must first define its OFE. An OFE encodes a kind of time dependence, but when the camera is _discrete_ and hence a @@ -167,7 +166,7 @@ Proof. red. done. Qed. Lemma state_update s : s ~~> Final. Proof. (** - As we are working with a discrete CMRA we can simplify this + As we are working with a discrete CMRA, we can simplify this statement as follows. *) rewrite cmra_discrete_update. @@ -186,7 +185,7 @@ Context `{!inG Σ stateR}. Our first lemma shows how a new State resource is created. We can create new resources via the basic update modality [|==> P]. This operation states that P holds after an update of resources. To work - with the update modality we can use two facts: + with the update modality, we can use two facts: - [P ⊢ |==> P] - [(P ⊢ |==> Q) ⊢ (|==> P ⊢ |==> Q)] Rather than working with these facts directly, we can use @@ -194,7 +193,7 @@ Context `{!inG Σ stateR}. *) Lemma alloc_Start : ⊢ |==> ∃ γ, own γ Start. Proof. - (** To allocate a new resource we use [own_alloc]. *) + (** To allocate a new resource, we use [own_alloc]. *) iApply own_alloc. (** We are naturally only allowed to allocate valid resources, but since @@ -205,8 +204,8 @@ Qed. (** Likewise, owning a resource means that it is valid. - A quick note: [✓ _] and [⌜✓ _⌝] are different, they only coincide when - the CMRA is discrete. + A quick note: [✓ _] and [⌜✓ _⌝] are different – they only coincide + when the CMRA is discrete. *) Lemma state_valid γ (s : state) : own γ s ⊢ ⌜✓ s⌝. Proof. @@ -243,15 +242,14 @@ Context `{!heapGS Σ, !spawnG Σ, !inG Σ stateR}. Let N := nroot .@ "state". (** - We can now define the invariant we hinted to in the beginning as - follows. + We can now define the invariant we hinted at in the beginning. *) Definition state_inv γ (l : loc) (x : Z) : iProp Σ := ∃ y : Z, l ↦ #y ∗ (own γ Start ∗ ⌜x = y⌝ ∨ own γ Final ∗ ⌜x < y⌝%Z). (** Rather than proving the entire program at once, we will split it into - 3 pieces, starting with the 2 threads. + three pieces, starting with the two threads. Note that WP contains an update modality, meaning we can update resources in between steps. diff --git a/theories/invariants.v b/theories/invariants.v index 4bb3af3..4544640 100644 --- a/theories/invariants.v +++ b/theories/invariants.v @@ -36,8 +36,8 @@ Proof. *) wp_apply (wp_fork with "[Hl]"). (** - As such we have to pick a thread to own [l]. But as both threads - need to access [l], we are stuck. + As such, we must pick a thread to own [l]. But as both threads need + to access [l], we are stuck. *) Abort. @@ -49,11 +49,11 @@ Section inv_intro. (** As the above program illustrates, some resources are required by multiple threads simultaneously. If those resources are not shareable - (i.e. persistent), then we will get stuck, as in the example above. - To get around this problem, we can devise an invariant for said + (i.e. persistent), then we will get stuck, as in the example above. To + get around this problem, we can devise an invariant for said resources. That is, we come up with a proposition [P] which describes the resources in a way that is always true, no matter where in the - program we are, or how threads have interleaved. We can then use Iris' + program we are or how threads have interleaved. We can then use Iris' invariant functionality to assert that [P] is an invariant: [inv N P]. Here, [N] is a `namespace', which we may think of as the name of the invariant. @@ -119,13 +119,13 @@ Abort. Another example of a goal permitting invariant openings is the _fancy update modality_, which essentially just adds a mask to the update modality. A fancy update modality is written [|={E}=>] for a mask [E]. - The fancy update modality is like the update modality, but with - support for invariants: if the goal contains [|={E}=>], then we are - allowed to open all invariants in [E]. + The fancy update modality is like the update modality but with support + for invariants: if the goal contains [|={E}=>], then we are allowed to + open all invariants in [E]. *) (** - Another restriction on invariant openings is that, when the goal is a + Another restriction on invariant openings is that when the goal is a weakest precondition [WP e {{Φ}}], an invariant can be open for at most one program step. This is enforced by requiring [e] to be an atomic expression, meaning it reduces to a value in one step. After @@ -168,7 +168,7 @@ Proof. *) iInv "Hinv" as "Hl". (** - This tactic did quit a bit, so let us break it down. + This tactic did quite a bit, so let us break it down. Firstly, notice that we got the points-to predicate from the invariant. A small caveat is that we only get the predicate later. @@ -176,7 +176,7 @@ Proof. cases, which we discuss in a later chapter. Secondly, the postcondition of the weakest precondition in the goal - got augmented with [|={⊤ ∖ ↑N}=> ▷ l ↦ #1]. After stepping through + was augmented with [|={⊤ ∖ ↑N}=> ▷ l ↦ #1]. After stepping through the current WP, we will have to prove this proposition to show that the invariant [l ↦ #1] still holds. The fancy update modality is there to stop us from opening the invariant to prove that the @@ -224,7 +224,7 @@ Proof. (** We have now used the invariant to reduce the right-hand [!#l]. Reducing the left-hand dereference is done analogously. - First we bind the dereference. + First, we bind the dereference. *) wp_bind (!#l)%E. (** Then we open the invariant. *) @@ -299,7 +299,7 @@ Qed. Side note: The above proof demonstrates why, when we have to prove the postcondition of a WP, we have to prove it _behind_ a fancy update modality. Having the fancy update modality in the goal allows us to - allocate/open invariants, and allocate/update resources. + allocate/open invariants and allocate/update resources. *) End inv_intro. @@ -329,7 +329,7 @@ Proof. rewrite /prog. wp_alloc l as "Hl". wp_pures. - (** We now allocate our [prog_inv] invariant, using [inv_alloc]. *) + (** We now allocate our [prog_inv] invariant using [inv_alloc]. *) iMod (inv_alloc N _ (prog_inv l) with "[Hl]") as "#Hinv". (** We prove that the invariant is currently true. *) { @@ -380,7 +380,7 @@ End proofs. (** Let us look at another program. This program will create a thread to - continuously increment a counter, while the main thread will read the + continuously increment a counter while the main thread will read the counter at some point. As such, this program should produce some non-negative number. However, we will only prove that it returns a number. Later, we will see other tools that will allow us to refine diff --git a/theories/lang.v b/theories/lang.v index 455595f..44a7968 100644 --- a/theories/lang.v +++ b/theories/lang.v @@ -7,7 +7,7 @@ From iris.heap_lang Require Import lang notation spawn par. (** ** Introduction *) (** - HeapLang is a untyped concurrent programming language with a heap. It + HeapLang is an untyped concurrent programming language with a heap. It is an ML-like language, sporting many of the usual constructs such as let expressions, lambda abstractions, and recursive functions. It also supports higher-order functions. The evaluation order is right to left @@ -15,7 +15,7 @@ From iris.heap_lang Require Import lang notation spawn par. The syntax for HeapLang is fairly standard, but there are some quirks as we are working inside Coq. As the features of HeapLang are fairly - standard, the focus in this chapter is manly on showcasing the syntax + standard, the focus in this chapter is mainly on showcasing the syntax of the language through simple examples. *) @@ -28,7 +28,7 @@ From iris.heap_lang Require Import lang notation spawn par. [iris.unstable.heap_lang]. The interpreter provides the function [exec], which takes as input some fuel and an expression. The expression is then executed until it terminates at a value [v], the - execution runs out fuel, or the program gets stuck. In case of + execution runs out of fuel, or the program gets stuck. In case of termination, [inl v] is returned. Otherwise [inr err] is returned, with [err] describing the error. *) @@ -268,7 +268,7 @@ Example cas : expr := instruction [Fork e] creates a new thread which executes [e]. The invoking thread continues execution after creation. If the computation of [e] terminates, then the resulting value is simply thrown away. - Hence, [e] is only run for its side-effects. + Hence, [e] is only run for its side effects. *) Example fork : expr := diff --git a/theories/later.v b/theories/later.v index 0bdca4b..6586496 100644 --- a/theories/later.v +++ b/theories/later.v @@ -18,7 +18,7 @@ Context `{!heapGS Σ}. The later modality is used quite extensively in Iris. We have already seen that it is used to define Hoare triples, but it has many more - uses. For instance, it is a prime tool to reason about recursive + uses. For instance, it is a prime tool for reasoning about recursive programs. It can be used to write specifications that capture the minimum number of steps taken by a program. It is also an integral part of working with invariants, which we introduce in a later @@ -26,11 +26,11 @@ Context `{!heapGS Σ}. *) (** - The later modality is monotone meaning that if we know [P ⊢ Q], then + The later modality is monotone, meaning that if we know [P ⊢ Q], then we can also conclude [▷ P ⊢ ▷ Q]. In words, if we know that [P] - entails [Q], then we also know that, if we get [P] after one step, we + entails [Q], then we also know that if we get [P] after one step, we will also get [Q] after one step. This is captured by the [iNext] - tactic, which introduces a later, while stripping laters from our + tactic, which introduces a later while stripping laters from our hypotheses. *) @@ -72,7 +72,7 @@ Qed. (** The later modality distributes over [∧], [∨], [∗], and is preserved - by [∃] and [∀]. This means that we can destruct these constructs + by [∃] and [∀]. This means we can destruct these constructs regardless of being prefaced by any laters. *) @@ -114,8 +114,8 @@ Qed. To see this in action, let us look at a simple program: [1 + 2 + 3]. This program takes two steps to evaluate, so we can prove that if a - proposition holds after two steps, then it will hold after the program - has terminated. + proposition holds after two steps, it will hold after the program has + terminated. *) Lemma take_2_steps (P : iProp Σ) : ▷ ▷ P -∗ WP #1 + #2 + #3 {{_, P}}. @@ -157,15 +157,15 @@ Qed. (** ** Löb Induction *) (** - The later modality allows for a strong induction principle, called Löb - induction. Essentially, Löb induction states that, to prove a + The later modality allows for a strong induction principle called Löb + induction. Essentially, Löb induction states that to prove a proposition [P], we are allowed to assume that [P] holds later, i.e. [▷ P]. Formally, we have [□ (▷ P -∗ P) -∗ P]. Recall that [▷] represents a single step in the logic. Löb induction essentially performs induction in the number of steps. Intuitively, Löb induction - states that, if we can show that whenever [P] holds for strictly - smaller than [n] steps we can prove that [P] holds for [n] steps, then - [P] holds for all steps. + states that if we can show that whenever [P] holds for strictly + smaller than [n] steps, we can prove that [P] holds for [n] steps, + then [P] holds for all steps. We can use this principle to prove many properties of recursive programs. To see this in action, we will define a simple recursive @@ -177,7 +177,7 @@ Example count : val := (** This function never terminates for any input as it will keep calling - itself with larger and larger inputs. To show this we pick the + itself with larger and larger inputs. To show this, we pick the postcondition [False]. We can now use Löb induction, along with [wp_rec], to prove this specification. *) @@ -187,13 +187,13 @@ Proof. (** The tactic for Löb induction, [iLöb], requires us to specify the name of the induction hypothesis, which we here call ["IH"]. - Optionally, it can also forall quantify any of our variables before - performing induction. We here forall quantify [x] as it changes for - every recursive call. + Optionally, it can also universally quantify over any of our variables + before performing induction. We here universally quantify over [x] as it + changes for every recursive call. *) iLöb as "IH" forall (x). (** - [iLöb] automatically introduces the forall quantified variables in + [iLöb] automatically introduces the universally quantified variables in the goal, so we can proceed to execute the function. *) wp_rec. diff --git a/theories/linked_lists.v b/theories/linked_lists.v index 5f1ee76..56c5744 100644 --- a/theories/linked_lists.v +++ b/theories/linked_lists.v @@ -25,7 +25,7 @@ Fixpoint isList (l : val) (xs : list val) : iProp Σ := *) (** - Now we can define HeapLang functions that act on lists, such as [inc]. + We can now define HeapLang functions that act on lists, such as [inc]. The [inc] function recursively increments all the values of a list. *) Definition inc : val := @@ -41,7 +41,7 @@ Definition inc : val := (** Intuitively, the specification we give for this function should state - that the linked list should only contain integers, and that, after + that the linked list should only contain integers and that, after executing the function, each integer has been incremented. As such, we parametrise the specification not by a list of values, but by a list of integers. We then map each integer to a HeapLang value using [# _], @@ -53,9 +53,9 @@ Lemma inc_spec (l : val) (xs : list Z) : {{{ RET #(); isList l ((λ x, #(x + 1)) <$> xs)}}}. Proof. (** - The proof proceeds by structural induction in [xs]. As [l] changes - in each iteration, we must forall quantify it to strengthen the - induction hypothesis. + The proof proceeds by structural induction in [xs]. As [l] changes in each + iteration, we must universally quantify over it to strengthen the induction + hypothesis. *) revert l. induction xs as [|x xs' IH]; simpl. @@ -139,7 +139,7 @@ Admitted. END TEMPLATE *) (** - We will implement reverse using a helper function, called + We will implement reverse using a helper function called [reverse_append], which takes two arguments, [l] and [acc], and returns the list [rev l ++ acc]. *) @@ -155,7 +155,7 @@ Definition reverse_append : val := end. (** - When acc is the empty list, it should thus simply return the reverse + When [acc] is the empty list, it should thus simply return the reverse of [l]. *) Definition reverse : val := @@ -194,7 +194,7 @@ Admitted. END TEMPLATE *) (** - Now we use the specification of [reverse_append] to prove the + Now, we use the specification of [reverse_append] to prove the specification of [reverse]. *) Lemma reverse_spec (l : val) (xs : list val) : @@ -249,7 +249,7 @@ Definition fold_right : val := - Importantly, we do not change the original list. So we put [isList l xs] in the postcondition. - Note that Hoare triples are persistent and persistent predicates are + Note that Hoare triples are persistent, and persistent predicates are closed under universal quantification. Hence, in the proof, the assumption for [f] will move into the persistent context. *) diff --git a/theories/merge_sort.v b/theories/merge_sort.v index 52298a0..0f51fcf 100644 --- a/theories/merge_sort.v +++ b/theories/merge_sort.v @@ -10,7 +10,7 @@ From iris.heap_lang Require Import array lang proofmode notation par. (** Let us implement a simple multithreaded merge sort on arrays. Merge sort consists of splitting the array in half until we are left with - pieces of size [0] or [1]. Then each pair of pieces is merged into a + pieces of size [0] or [1]. Then, each pair of pieces is merged into a new sorted array. *) @@ -106,22 +106,22 @@ Lemma merge_spec (a1 a2 b : loc) (l1 l2 : list Z) (l : list val) : wp_pures. destruct l1 as [|x1 l1]. { - rewrite nil_length Nat.add_0_l in H. + rewrite length_nil Nat.add_0_l in H. wp_pures. iApply (wp_array_copy_to with "[$Hb $Ha2]"). - by rewrite H. - - by rewrite fmap_length. + - by rewrite length_fmap. - iIntros "!> [Hb Ha2]". iApply "HΦ". by iFrame. } destruct l2 as [|x2 l2]. { - rewrite nil_length Nat.add_0_r in H. + rewrite length_nil Nat.add_0_r in H. wp_pures. iApply (wp_array_copy_to with "[$Hb $Ha1]"). - by rewrite H. - - by rewrite fmap_length. + - by rewrite length_fmap. - iIntros "!> [Hb Ha1]". iApply "HΦ". iFrame. @@ -130,7 +130,7 @@ Lemma merge_spec (a1 a2 b : loc) (l1 l2 : list Z) (l : list val) : apply StronglySorted_inv in Hl1 as [H1 Hl1]. apply StronglySorted_inv in Hl2 as [H2 Hl2]. wp_pures. - rewrite !cons_length Nat.add_succ_l Nat.add_succ_r in H. + rewrite !length_cons Nat.add_succ_l Nat.add_succ_r in H. destruct l as [|y l]; first done. cbn in H. injection H as H. @@ -225,7 +225,7 @@ Lemma merge_sort_inner_spec (a b : loc) (l : list Z) : iApply "HΦ". iFrame. iPureIntro. - rewrite fmap_length. + rewrite length_fmap. split; last done. apply (Nat2Z.inj_le _ 1) in Hlen. destruct l as [|i1 [|i2 l]]. @@ -255,10 +255,10 @@ Lemma merge_sort_inner_spec (a b : loc) (l : list Z) : - by apply firstn_length_le. } clear H. - rewrite app_length in Hlen. - rewrite app_length. + rewrite length_app in Hlen. + rewrite length_app. replace (length l1 + length l2 - length l1) with (length l2) by lia. - rewrite fmap_app !array_app fmap_length. + rewrite fmap_app !array_app length_fmap. iDestruct "Ha" as "[Ha1 Ha2]". iDestruct "Hb" as "[Hb1 Hb2]". wp_apply (par_spec @@ -288,18 +288,18 @@ Lemma merge_sort_inner_spec (a b : loc) (l : list Z) : { iPureIntro. split_and!; [done..|]. - rewrite app_length. + rewrite length_app. by f_equal. } iIntros "%l (Hb1 & Hb2 & Ha & Hl & %Hl)". iCombine "Hb1 Hb2" as "Hb". - erewrite <-fmap_length, <-array_app, <-fmap_app. + erewrite <-length_fmap, <-array_app, <-fmap_app. iApply "HΦ". iFrame. iPureIntro. split. + by rewrite Hl1 Hl2. - + rewrite fmap_length. + + rewrite length_fmap. by apply Permutation_length. Qed. @@ -340,8 +340,8 @@ Lemma merge_sort_spec (a : loc) (l : list Z) : rewrite Nat2Z.id. wp_pures. wp_apply (wp_array_copy_to with "[$Hb $Ha]"). - { by rewrite replicate_length. } - { by rewrite fmap_length. } + { by rewrite length_replicate. } + { by rewrite length_fmap. } iIntros "[Hb Ha]". wp_pures. wp_apply (merge_sort_inner_spec with "[$Ha $Hb]"). diff --git a/theories/ofe.v b/theories/ofe.v index 3b26d5a..1abbb96 100644 --- a/theories/ofe.v +++ b/theories/ofe.v @@ -10,7 +10,7 @@ From iris.algebra Require Export ofe. Iris. However, they form good intuition about the usefulness of OFEs. We will look at streams over natural numbers. These are infinite - sequences with [head] being the first value, and [tail] being the rest + sequences with [head] being the first value and [tail] being the rest of the stream. We define streams as a coinductive type. You should be able to follow this file without extensive knowledge of coinduction. *) @@ -29,7 +29,7 @@ Add Printing Constructor stream. CoFixpoint zeros := SCons 0 zeros. (** - [CoFixpoints] allows us to build coinductive values, in the same way + [CoFixpoints] allows us to build coinductive values in the same way that [Fixpoint] allows us to use inductive types recursively. We can get the [n]'th element of the stream by iterating through the @@ -42,7 +42,7 @@ Fixpoint nth (s : stream) (n : nat) : nat := end. (** - We can likewise define a stream from its [n]'th elements + We can likewise define a stream from its [n]'th elements. *) CoFixpoint fun2stream (f : nat → nat) : stream := SCons (f 0) (fun2stream (f ∘ S)). @@ -64,11 +64,11 @@ Local Instance stream_equiv_instance : Equiv stream := λ s1 s2, ∀ n, nth s1 n = nth s2 n. (** - Now for the OFE structure, we introduce the concept of approximate + Now, for the OFE structure, we introduce the concept of approximate equivalence using the typeclass [Dist]. This typeclass defines a family of equivalence relations written - [[x ≡{n}≡ y]] where [n] is the precision. In our case this will + [[x ≡{n}≡ y]] where [n] is the precision. In our case, this will decide how many of the elements of the stream we look at. *) Local Instance stream_dist_instance : Dist stream := λ n s1 s2, @@ -125,8 +125,8 @@ End ofe. (** We can now ask the question of whether we can build values from a - sequence of better and better approximations. To this end we use the - concept of a chain. Here chains are sequences such that all elements + sequence of better and better approximations. To this end, we use the + concept of a chain. Here, chains are sequences such that all elements after the [n]'th element are [n]-equivalent. An OFE is complete if all chains approach a value. This is also called a COFE for complete OFE. @@ -233,7 +233,7 @@ Fixpoint sapp (l : list nat) (s : stream) : stream := (** This operation is [NonExpansive] when we fix the list we wish to prepend. Furthermore, we can prove this without unfolding the - definition of [dist], by using what we have proved so far. + definition of [dist] by using what we have proved thus far. *) Global Instance sapp_ne (l : list nat) : NonExpansive (sapp l). (* SOLUTION *) Proof. @@ -247,8 +247,8 @@ Global Instance sapp_proper (l : list nat) : Proper ((≡) ==> (≡)) (sapp l). Proof. apply ne_proper, _. Qed. (** - Now let's define a stream that simply repeats a list over and over - again. Intuitively we should be able to define it as follows: + Now, let's define a stream that simply repeats a list over and over + again. Intuitively, we should be able to define it as follows: *) Fail CoFixpoint repeat (l : list nat) : stream := sapp l (repeat l). @@ -259,7 +259,7 @@ Fail CoFixpoint repeat (l : list nat) : stream := result remains empty. So we will never end up with an infinite stream. - To fix this we can insert a separator in between the repetitions of + To fix this, we can insert a separator in between the repetitions of the list: *) Fail CoFixpoint repeat_with_sep (l : list nat) (x : nat) : stream := @@ -269,7 +269,7 @@ Fail CoFixpoint repeat_with_sep (l : list nat) (x : nat) : stream := But this still fails with the same error. This is because Coq uses a simple syntactic check to validate co-fixpoint definitions. - To satisfy this check we are forced to syntactically produce at least + To satisfy this check, we are forced to syntactically produce at least one element of the stream per recursive call, which is violated by the call to [sapp]. In practice, this means that we cannot reuse most of our existing operations when writing new recursively defined streams. @@ -285,8 +285,8 @@ Definition repeat_with_sep (l : list nat) (x : nat) := repeat_with_sep_helper l x l. (** - To be sure that this definition is correct, we can show that it still - solves the fixpoint equation. To do this we first need to show that + To ensure that this definition is correct, we can show that it still + solves the fixpoint equation. To do this, we first need to show that the helper function does what it is supposed to. *) Lemma repeat_with_sep_helper_unfold (l : list nat) (x : nat) (helper : list nat) : @@ -323,7 +323,7 @@ Global Instance repeat_with_sep_contractive (l : list nat) (x : nat) : Contracti Proof. solve_contractive. Qed. (** - To get a fixpoint for such a function we need three things: + To get a fixpoint for such a function, we need three things: - The type we wish to produce an element of (stream) must have a COFE structure, which we defined earlier. - The function we wish to find a fixpoint for must be contractive, @@ -371,7 +371,7 @@ CoFixpoint stream_map (f : nat → nat) (s : stream) : stream := just build this as a fixpoint on streams. Instead, we need to build a fixpoint on [stream → stream]. However, this is not equipped with a canonical OFE structure. Instead, we need to write - [stream -d> streamO]. Here [d] stands for discrete, meaning we don't + [stream -d> streamO]. Here, [d] stands for discrete, meaning we don't consider any OFE structure on the domain. As such, we are allowed to change the parameter arbitrarily on recursive calls. *) @@ -432,7 +432,7 @@ Fail CoFixpoint power2 : stream := However, this again fails the syntactic check, as we are modifying the tail of the stream. - To fix this we could instead define a stream starting with a number + To fix this, we could instead define a stream starting with a number [n] doubling [n] at every step. *) CoFixpoint power2_helper (n : nat) : stream := @@ -469,7 +469,7 @@ Definition power2_pre (s : stream) : stream := SCons 1 (stream_map (λ n, n * 2) s). (** - This is again contractive in [s], because [SCons] is [Contractive] and + This is again contractive in [s] because [SCons] is [Contractive] and [stream_map] is [NonExpansive]. *) Global Instance power2_pre_contractive : Contractive power2_pre. @@ -497,7 +497,7 @@ Qed. propositions recursively, we can use [fixpoint]. Importantly, all the connectives of the logic are [NonExpansive]. To then use guarded fixpoints, we need a [Contractive] function like [SCons]. And for - [iProp] this is later [▷ P]. We have already run into two connectives + [iProp], this is later [▷ P]. We have already run into two connectives defined using the guarded-fixpoint, namely the weakest precondition [WP], and invariants [inv]. This is why we can remove laters from premises when taking a step in the program, as this corresponds to diff --git a/theories/persistently.v b/theories/persistently.v index c3ed990..285f76c 100644 --- a/theories/persistently.v +++ b/theories/persistently.v @@ -14,7 +14,7 @@ Context `{!heapGS Σ}. (** In separation logic, propositions are generally not duplicable. This is because resources are generally exclusive. However, resources do - not _have_ to be exclusive. A great example of this is `read only + not _have_ to be exclusive. A great example of this is `read-only memory'. There is no danger in letting many threads access the same location simultaneously if they can only read from it. Hence, it would not make sense to require that ownership of those locations be @@ -26,7 +26,7 @@ Context `{!heapGS Σ}. intuitionistic logic, which is why they are also sometimes referred to as intuitionistic. - A propositions is persistent when [P ⊢ □ P]. That is, assuming [P], we + A proposition is persistent when [P ⊢ □ P]. That is, assuming [P], we need to show that [P] does not rely on any exclusive resources. Persistency is preserved by most connectives, so proving that a proposition is persistent is usually a matter of showing that the @@ -95,10 +95,10 @@ Lemma pers_dup (P : iProp Σ) `{!Persistent P} : P ⊢ P ∗ P. Qed. (** - Persistent propositions satisfy a lot of nice properties, simply by + Persistent propositions satisfy a lot of nice properties simply by being duplicable [P ⊢ P ∗ P]. For example, [P ∧ Q] and [P ∗ Q] - coincide, when either [P] or [Q] is persistent. Likewise, [P → Q] and - [P -∗ Q] coincide, when [P] is persistent. + coincide when either [P] or [Q] is persistent. Likewise, [P → Q] and + [P -∗ Q] coincide when [P] is persistent. *) Check bi.persistent_and_sep. @@ -114,9 +114,9 @@ Check bi.impl_wand. (** ** Proving Persistency *) (** - To prove a proposition [□ P], we have to prove [P] without assuming - any exclusive resources. In other words, we have to throw away the - spatial context when proving [P]. + To prove a proposition [□ P], we must prove [P] without assuming any + exclusive resources. In other words, we have to throw away the spatial + context when proving [P]. *) Lemma pers_intro (P Q : iProp Σ) `{!Persistent P} : P ∗ Q ⊢ □ P. @@ -172,8 +172,8 @@ Proof. iModIntro. (** By default, [iFrame] will not frame propositions from the - persistent context. To make it do so, we have to give it the - argument ["#"]. + persistent context. To make it do so, we must give it the argument + ["#"]. *) iFrame "#". (* BEGIN SOLUTION *) @@ -229,7 +229,7 @@ Proof. apply _. Qed. (** For more complicated predicates, such as ones defined as a fixpoint, [Persistent] cannot automatically infer its persistence. The following - predicate asserts that all values in a given list is equal to [5]. + predicate asserts that all values in a given list are equal to [5]. *) Fixpoint myPredFix (xs : list val) : iProp Σ := @@ -268,7 +268,7 @@ Proof. apply _. Qed. -(** Now, Iris recognises [myPredFix] as persistent. *) +(** Iris now recognises [myPredFix] as persistent. *) Lemma first_is_5 (x : val) (xs : list val) : myPredFix (x :: xs) -∗ ⌜x = #5⌝ ∗ myPredFix (x :: xs). @@ -287,7 +287,7 @@ Qed. (** Thus far, the only basic persistent propositions we have seen are pure - propositions, such as equalities. In this section we introduce two + propositions, such as equalities. In this section, we introduce two additional examples of persistent propositions: Hoare triples and persistent points-to predicates. *) @@ -297,7 +297,7 @@ Qed. (** All Hoare triples are persistent. This probably does not come as a - surprise, if the reader recalls how we defined Hoare triples in the + surprise if the reader recalls how we defined Hoare triples in the [specifications] chapter. As a reminder, here is the definition again. [□( ∀ Φ, P -∗ ▷ (∀ r0 .. rn, Q -∗ Φ v) -∗ WP e {{v, Φ v }})] @@ -363,7 +363,7 @@ Context `{spawnG Σ}. [l ↦ dq v], where [dq] is a `discarded fraction'. We return to the `discarded' part momentarily, but for now, we assume that [dq] is a fraction in the interval (0; 1]. The predicate [l ↦ v] is a special - case, where the fraction [dq] is [1]. The basic idea is that points-to + case where the fraction [dq] is [1]. The basic idea is that points-to predicates can be split up and recombined, allowing ownership of points-to predicates to be shared. *) @@ -401,7 +401,7 @@ Abort. (** Fractional points-to predicates are especially useful in scenarios - where a location is read by multiple threads in parallel, but later + where a location is read by multiple threads in parallel but later only used by a single thread. *) @@ -417,7 +417,7 @@ Proof. iIntros (Φ) "[Hl1 Hl2] HΦ". rewrite /par_read_write. (** - The idea is to give each thread half of the points-to predicate, and + The idea is to give each thread half of the points-to predicate and assert that both will return their halves afterwards. *) set t_post := (λ w : val, (⌜w = v⌝ ∗ l ↦{#1 / 2} v)%I). diff --git a/theories/pure.v b/theories/pure.v index b63ea42..9f102da 100644 --- a/theories/pure.v +++ b/theories/pure.v @@ -62,9 +62,9 @@ Qed. It is quite easy to show that the propositions [⌜5 = 5⌝] and [⌜x = y⌝] from above are pure. However, it can become quite burdensome for more complicated Iris propositions. Fortunately, Iris has two typeclasses - [IntoPure] and [FromPure] which can identify pure propositions for us. - These are used by the [iPureIntro] tactic to automatically identify - pure propositions. + [IntoPure] and [FromPure] that can identify pure propositions for us. + These are used by the [iPureIntro] tactic to identify pure + propositions automatically. *) (** [True] is pure. *) diff --git a/theories/resource_algebra.v b/theories/resource_algebra.v index 145341f..c250030 100644 --- a/theories/resource_algebra.v +++ b/theories/resource_algebra.v @@ -17,9 +17,9 @@ From iris.heap_lang Require Import lang proofmode notation. resources uniformly – we define a fixed set of criteria that a notion of resource must satisfy in order to be used in the logic. If the notion satisfies those criteria, then it is a `resource algebra' - (often shorted to `RA'). We can then have a small handful of rules for - resource algebras in general, and we hence do not need to change the - logic every time we wish to use a new notion of a resource. + (often shortened to `RA'). We can then have a small handful of rules + for resource algebras in general, and we hence do not need to change + the logic every time we wish to use a new notion of a resource. In this way, resource algebras are oblivious to the existence of Iris – they exist as a separate thing. Iris then has a mechanism to embed @@ -30,7 +30,7 @@ From iris.heap_lang Require Import lang proofmode notation. A small side note: in Iris, resource algebras are specialisations of the more general structure `CMRA' (in particular, resource algebras are `discrete' CMRAs). In turn, CMRAs are built on top of `Ordered - Families of Equations' (shortened to `OFE'). The exact details of + Families of Equivalences' (shortened to `OFE'). The exact details of these concepts are not important for this chapter, but we mention them as they appear a few times throughout the chapter. CMRAs and OFEs are covered in more detail in later chapters. @@ -110,7 +110,7 @@ Print RAMixin. expresses that, if [y ≡ z], then [x ⋅ y ≡ x ⋅ z], for all [x]. The fields [ra_assoc] and [ra_comm] assert that the operation [⋅] - should be associative and commutative. This in effect makes [A] a + should be associative and commutative. This, in effect, makes [A] a commutative semigroup, which means that we can make all resource algebras a preorder through the extension order, written [x ≼ y]. The extension order is defined as: @@ -121,7 +121,7 @@ Print RAMixin. [y] in terms of [x] and some [z]. The fields [ra_pcore_l] and [ra_pcore_idemp] capture the idea that the - core extracts the shareable part of a resource, and how shareable + core extracts the shareable part of a resource and how shareable resources behave. [ra_pcore_l] expresses that including the same shareable resource multiple times does not change a resource, and [ra_pcore_idemp] states that invoking the core on a resource twice @@ -327,7 +327,7 @@ Proof. Qed. Lemma dfrac_valid_discarded : ✓ (DfracDiscarded). -(* Solution *) Proof. +(* SOLUTION *) Proof. rewrite dfrac_valid. done. Qed. @@ -395,13 +395,13 @@ Proof. Qed. Lemma dfrac_pre_disc_both : DfracDiscarded ≼ DfracBoth (3/4). -(* Solution *) Proof. +(* SOLUTION *) Proof. exists (DfracOwn (3/4)). compute_done. Qed. Lemma dfrac_pre_own_both : DfracOwn (2/4) ≼ DfracBoth (3/4). -(* Solution *) Proof. +(* SOLUTION *) Proof. exists (DfracBoth (1/4)). compute_done. Qed. @@ -414,14 +414,14 @@ Qed. update resources – resources are used to reason about programs, and programs update resources. One has to be careful with how resources are allowed to be updated; in Iris, only _valid_ resources can be - owned. It should always be the case that, if we combine the resources + owned. It should always be the case that if we combine the resources owned by all threads in the system, the resulting resource should be valid. Otherwise, we could easily derive falsehood. Hence, when a thread updates its resources, it must ensure that it does not introduce the possibility of obtaining an invalid element. We call - such an update a `frame preserving Update', and write [x ~~> y] to - mean that we can perform a frame preserving update from resource [x] - to resource [y]. The formal definition for this notion turns out to be + such an update a `frame preserving update' and write [x ~~> y] to mean + that we can perform a frame preserving update from resource [x] to + resource [y]. The formal definition for this notion turns out to be quite succinct: [x ~~> y = ∀z, ✓(x ⋅ z) → ✓(y ⋅ z)] @@ -430,7 +430,7 @@ Qed. also valid with [y]. If this is the case, then it is okay to update [x] to [y]. Since [z] is forall quantified, [z] also represents the resource we get by combining the resources from all other threads. - That is to say, [x ~~> y] ensures that, if the combination of all + That is to say, [x ~~> y] ensures that if the combination of all resources was valid before the update, it still is after. As [z] represents all the other resources, it is called the `frame', and the proposition [x ~~> y] expresses that the validity of [z] – the frame – @@ -569,7 +569,7 @@ END TEMPLATE *) concepts of resource algebra. While dfrac has some use cases on its own, it is especially useful when composed with other resource algebra (e.g. it is used to define the points-to predicate). Hence, in this - section, we will introduce some often used resource algebras. + section, we will introduce some often-used resource algebras. Unlike dfrac, the resource algebras we study in this section are parametrised by other resource algebras (or OFEs, or CMRAs). This @@ -650,7 +650,7 @@ End exclusive. (** So how is this resource algebra useful? While it is a key component in - many fairly complex resource algebras, it has a super simple, yet + many fairly complex resource algebras, it has a super simple yet extremely practical use case. Together with the OFE [unitO], we can create the resource algebra of `tokens'. *) @@ -698,7 +698,7 @@ Context {A : ofe}. carrier of resource algebra), and all it cares about is whether two resources are equivalent. That is, whether they _agree_. As such, the carrier of agree is the same as the carrier of the underlying resource - algebra, and all resources in [agree A] are valid – irregardless of + algebra, and all resources in [agree A] are valid – regardless of their validity in the original resource algebra. *) @@ -762,7 +762,7 @@ Qed. Lemma agree_valid_opL (a b : A) : ✓ (to_agree a ⋅ to_agree b) → to_agree a ⋅ to_agree b ≡ to_agree a. -(* Solution *) Proof. +(* SOLUTION *) Proof. intros Hvalid. apply to_agree_op_valid in Hvalid. rewrite Hvalid. @@ -798,7 +798,7 @@ END TEMPLATE *) (** The usefulness of the agree construction is demonstrated by the fact that it is used to define the resource of heaps. The inclusion of the - agree RA allows us to conclude that, if we have two points-to + agree RA allows us to conclude that if we have two points-to predicates for the same location, [l ↦{dq1} v1] and [l ↦{dq2} v2], then they _agree_ on the value stored at the location: [v1 = v2]. *) @@ -844,7 +844,7 @@ About pair_op. About pair_valid. (** - A pair is included in another pair, if the components of the first are + A pair is included in another pair if the components of the first are included in the components of the second. *) @@ -881,7 +881,7 @@ Qed. (** The product RA is often used in conjunction with dfrac and agree, with - the first component being a dfrac, and the second being an element of + the first component being a dfrac and the second being an element of some resource algebra wrapped in agree. This pattern is common enough that it has been added to Iris' library of resource algebras. *) @@ -916,7 +916,7 @@ Section ghost. in Iris have type [iProp Σ]. The [Σ] can be thought of as a global list of resource algebras that are available in the logic. The [Σ] is always universally quantified to enable composition of proofs. - However, we may put _restrictions_ on [Σ], to specify that the list + However, we may put _restrictions_ on [Σ] to specify that the list must contain some specific resource algebra of our choosing. The typeclass [inG Σ R] expresses that the resource algebra [R] is in the [G]lobal list of resource algebras [Σ]. If we add this to the Coq @@ -971,8 +971,8 @@ Context `{!heapGS Σ}. exactly one way of embedding a resource [r] from some resource algebra [R] into the logic: the proposition [own γ r] asserts _ownership_ of the resource [r] in an instance of the resource algebra [R] named [γ]. - That is to say, in Iris, once we have added a [R] to [Σ], we may - create multiple instances of [R], so that the same resource in [R] may + That is to say, in Iris, once we have added an [R] to [Σ], we may + create multiple instances of [R] so that the same resource in [R] may be owned multiple times. To distinguish between instances, we use `ghost names' (sometimes also called `ghost variables' or `ghost locations'), which is usually written with a lower-case gamma: [γ]. @@ -995,7 +995,7 @@ Definition token (γ : gname) := own γ (Excl ()). defined in terms of [own]. That is, [l ↦ v] is just notation denoting ownership of a resource in the resource of heaps! But where is the ghost name [γ]? When adding the resource of heaps to [Σ], we do it - with the [heapGS Σ] typeclass. Here, the [S] stands for `singleton', + with the [heapGS Σ] typeclass. Here, the [S] stands for `singleton' and signifies that only _one_ instance of the resource of heaps exists. As such, we do not need ghost names to distinguish between instances. @@ -1081,7 +1081,7 @@ Qed. (** Recall that the core extracts the shareable part of a resource. If the core of some resource is itself, then that resource is freely - shareable – in particular ownership of the resource is duplicable. + shareable – in particular, ownership of the resource is duplicable. That is, if [pcore r = Some r], then [own γ r] is persistent. *) @@ -1199,7 +1199,7 @@ Qed. About own_alloc. (** - That is, if we have some resource algebra [A], and wish to create and + That is, if we have some resource algebra [A] and wish to create and get ownership of resource [a] in [A], then, as long as [a] is valid, we may update our resources to get ownership of [a] in a _fresh_ instance of [A], identified by a fresh ghost name [γ]. @@ -1251,7 +1251,7 @@ Proof. Qed. (** - Exercise: Use [own_dfrac_update] to prove the following hoare triple. + Exercise: Use [own_dfrac_update] to prove the following Hoare triple. *) Lemma hoare_triple_dfrac (γ : gname): diff --git a/theories/specifications.v b/theories/specifications.v index dabe9d1..9298106 100644 --- a/theories/specifications.v +++ b/theories/specifications.v @@ -44,7 +44,7 @@ Example arith : expr := (** This program should evaluate to [16]. We can express this in the logic with a weakest precondition. In general, a weakest precondition has - the form [WP e {{v, Φ v}}]. This asserts that, if the HeapLang program + the form [WP e {{v, Φ v}}]. This asserts that if the HeapLang program [e] terminates at some value [v], then [v] satisfies the predicate [Φ]. The double curly brackets [{{v, Φ v}}] is called the `postcondition'. For the case of [arith], we would express its @@ -149,7 +149,7 @@ Example lambda : expr := <> These tactics similarly apply the underlying rules of the logic, - however we shall from now on refrain from explicitly mentioning the + however, we shall from now on refrain from explicitly mentioning the rules applied. Through experience, the reader should get an intuition for how each tactic manipulates the goal. @@ -177,7 +177,7 @@ END TEMPLATE *) resource of heaps. As mentioned in basics.v, propositions in Iris describe/assert ownership of resources. To describe resources in the resource of heaps, we use the `points-to' predicate, written [l ↦ v]. - Intuitively, this describes all heap fragments that has value [v] + Intuitively, this describes all heap fragments that have value [v] stored at location [l]. The proposition [l1 ↦ #1 ∗ l2 ↦ #2] then describes all heap fragments that map [l1] to [#1] and [l2] to [#2]. @@ -243,7 +243,7 @@ Qed. subgoals. The first corresponds to the case where the [CmpXchg] instruction succeeded. Thus, we get to assume [H1 : v = v1], and our points-to predicate for [l] is updated to [l ↦ v2]. The second - corresponds to case where [CmpXchg] failed. We instead get + corresponds to the case where [CmpXchg] failed. We instead get [H2 : v ≠ v1], and our points-to predicate for [l] is unchanged. Let us demonstrate this with a simple example program which simply @@ -290,7 +290,7 @@ Example cas : expr := #(). (** - The result of both [CAS] instructions are predetermined. Hence, we can + The result of both [CAS] instructions is predetermined. Hence, we can use the [wp_cmpxchg_suc] and [wp_cmpxchg_fail] tactics to symbolically execute them (remember that [CAS l v1 v2] is syntactic sugar for [Snd (CmpXchg l v1 v2)]). @@ -374,10 +374,10 @@ Proof. [WP e {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e {{ Ψ }}]. - With this it suffices to prove that the postcondition of [prog_spec] - implies the postcondition in our current goal. This is achieved with - the [wp_wand] lemma, which generates two subgoals, one corresponding - to [WP e {{ Φ }}] and one to [(∀ v, Φ v -∗ Ψ v)]. + With this, it suffices to prove that the postcondition of + [prog_spec] implies the postcondition in our current goal. This is + achieved with the [wp_wand] lemma, which generates two subgoals, one + corresponding to [WP e {{ Φ }}] and one to [(∀ v, Φ v -∗ Ψ v)]. *) iApply wp_wand; simpl. { iApply prog_spec. } @@ -412,9 +412,9 @@ Qed. Lemma prog_add_2_spec' : ⊢ WP prog + #2 {{ v, ⌜v = #5⌝ }}. Proof. wp_bind prog. - (** The goal is now on the exact form required by [prog_spec_2] *) + (** The goal is now on the exact form required by [prog_spec_2]. *) iApply prog_spec_2. - (** And the proof proceeds as before *) + (** And the proof proceeds as before. *) iIntros "%w ->". wp_pure. done. @@ -422,7 +422,7 @@ Qed. (** We can even simplify this proof further by using the [wp_apply] - tactic which automatically applies [wp_bind] for us. + tactic, which automatically applies [wp_bind] for us. *) Lemma prog_add_2_spec'' : ⊢ WP prog + #2 {{ v, ⌜v = #5⌝ }}. wp_apply prog_spec_2. @@ -440,7 +440,7 @@ Qed. precondition does not explicitly specify which conditions must be met before executing the program. It only talks about which conditions are met after – the postcondition. Hoare triples build on weakest - preconditions by requiring us to explicitly mention the the conditions + preconditions by requiring us to explicitly mention the conditions that must hold before running the program – the precondition. The syntax for Hoare triples is as follows: @@ -461,7 +461,7 @@ Qed. Firstly, inspired by the [prog_spec_2] example from the previous section, this definition makes the postcondition generic. Next, the precondition [P] implies the generic weakest precondition, - signifying that we must first prove [P] before we can apply + signifying that we must first prove [P] before we can apply the specification for [e]. Finally, the definition uses two modalities that we have yet to cover. The persistently modality [□] signifies that the specification can be @@ -521,12 +521,12 @@ Proof. Qed. (** - A convention in Iris is to write specifications using Hoare triples, + A convention in Iris is to write specifications using Hoare triples but prove them by converting them to weakest preconditions as in the examples above. There are several reasons for this. Firstly, it ensures that all specifications are generic in the postcondition. Secondly, specifications written in terms of Hoare triples are usually - easier to read, as they name explicitly what must be obtained before + easier to read, as they explicitly name what must be obtained before the program can be executed. Finally, proving Hoare triples directly can be quite awkward and burdensome, especially in Coq. *) @@ -597,7 +597,7 @@ Proof. iIntros (Φ _) "HΦ". rewrite /par_client. (** - The program starts by creating two fresh location, [l1] and [l2]. + The program starts by creating two fresh locations, [l1] and [l2]. *) wp_alloc l1 as "Hl1". wp_let. @@ -615,7 +615,7 @@ Proof. (** We can now apply the [wp_par] specification. Note how we transfer ownership of [l1 ↦ #0] to the first thread, and [l2 ↦ #0] to the - second. This allows each thread to perform their store operations. + second. This allows each thread to perform its store operation. *) wp_apply (wp_par t1_post t2_post with "[Hl1] [Hl2]"). (** diff --git a/theories/spin_lock.v b/theories/spin_lock.v index 09c58fb..b37b668 100644 --- a/theories/spin_lock.v +++ b/theories/spin_lock.v @@ -20,10 +20,10 @@ Definition mk_lock : val := (** To acquire the lock, we use [CAS l false true] (compare and set). This - instruction atomically writes [true] to location [l], if [l] contains + instruction atomically writes [true] to location [l] if [l] contains [false]. The [CAS] instruction then returns a boolean, signifying whether [l] was updated. If the [CAS] fails, it means that the lock is - currently acquired somewhere else. So we simply try again, until the lock + currently acquired somewhere else. So we simply try again until the lock is free. *) Definition acquire : val := @@ -68,7 +68,7 @@ Context `{heapGS Σ}. algebra is generic. However, we just need one exclusive element, so we will instantiate the exclusive RA with the unit OFE: [exclR unitO]. Note that this is exactly the resource algebra we used to define - tokens. As such, we will reuse tokens here, but rename them to clarify + tokens. As such, we will reuse tokens here but rename them to clarify their intent. *) Context `{!tokenG Σ}. @@ -139,7 +139,7 @@ Proof. Qed. (** - Acquiring the lock should grant access to the protected resources, as + Acquiring the lock should grant access to the protected resources as well as knowledge that the lock has been locked. *) Lemma acquire_spec γ v P : @@ -210,7 +210,7 @@ Definition prog : expr := (** [x] can take on the values of [0], [1], and [7]. However, we should - not observe [7], as it is overridden before the lock is released. + not observe [7], as it is overwritten before the lock is released. *) Lemma prog_spec : ⊢ WP prog {{ v, ⌜v = #0 ∨ v = #1⌝}}. Proof. diff --git a/theories/structured_conc.v b/theories/structured_conc.v index cd2ec67..2950d83 100644 --- a/theories/structured_conc.v +++ b/theories/structured_conc.v @@ -25,7 +25,7 @@ From iris.heap_lang Require Import lang proofmode notation. The library definitions additionally give and prove specifications for the constructs, which we have used in previous chapters. In this - chapter, we will define the constructs from scratch, and write our own + chapter, we will define the constructs from scratch and write our own specifications for them. *) @@ -46,11 +46,11 @@ From iris.heap_lang Require Import lang proofmode notation. About wp_fork. (** - For convenience, we included it here as well in `simplified' form. + For convenience, we include it here as well in `simplified' form. [WP e {{_, True}} -∗ ▷ Φ #() -∗ WP Fork e {{v, Φ v}}] - That is, to show a weakest precondition of [Fork e] we have to show + That is, to show a weakest precondition of [Fork e], we have to show the weakest precondition of [e] for a trivial postcondition. The key point is that we only require the forked-off thread to be safe – we do not care about its return value, hence the trivial postcondition. @@ -101,12 +101,12 @@ Definition join: val := {{{ P }}} spawn f {{{ h, RET h; join_handle h Ψ }}} ]] - This states that, to get a specification for [spawn f], we first must + This states that to get a specification for [spawn f], we first must prove a specification for [f] which captures which resources [f] needs, [P], and what the value [f] terminates at satisfies, [Ψ]. If we can prove such a specification for [f], then, given [P], we can also run [spawn f], which will return a value [h] which satisfies a - `join-handle' predicate. This predicate is a promise that, if we + `join-handle' predicate. This predicate is a promise that if we invoke [join] with [h], then the value we get back satisfies [Ψ]. This is reflected in the specification for [join]: @@ -123,7 +123,7 @@ Context `{!heapGS Σ}. Let N := nroot .@ "handle". (** - Since we are using a shared channel we will use an invariant to allow + Since we are using a shared channel, we will use an invariant to allow the two (concurrently running) threads to access it. An initial attempt at stating this invariant looks as follows. *) @@ -132,7 +132,7 @@ Definition handle_inv1 (l : loc) (Ψ : val → iProp Σ) : iProp Σ := (** The stated invariant governs the shared channel (some location [l]) - and states that either no value has been sent yet, or some value has + and states that either no value has been sent yet or some value has been sent that satisfies the predicate [Ψ]. We can then use the invariant to define the [join_handle] predicate. @@ -162,8 +162,10 @@ Proof. by iApply "IH". - wp_load. iModIntro. - (** Now we need [HΨ] to reestablish the invariant but we also need it for - the postcondition. We are stuck... *) + (** + Now we need [HΨ] to reestablish the invariant, but we also need it + for the postcondition. We are stuck... + *) Abort. (** @@ -189,7 +191,7 @@ Definition handle_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ (** This enables the owner of the token to open the invariant, extract [Ψ w], and close the invariant in the case that mentions the token. As - such, we include the token in the join handle, so that [join] gets + such, we include the token in the join handle so that [join] gets access to the token. *) @@ -334,7 +336,7 @@ Context `{!heapGS Σ, !tokenG Σ}. (** It is actually quite straightforward to prove the [par] specification - as most of the heavy lifting is done by [spawn_spec] and [par_spec]. + as most of the heavy lifting is done by [spawn_spec] and [join_spec]. *) Lemma par_spec (P1 P2 : iProp Σ) (e1 e2 : expr) (Q1 Q2 : val → iProp Σ) : {{{ P1 }}} e1 {{{ v, RET v; Q1 v }}} -∗ @@ -364,7 +366,7 @@ Proof. wp_pures. (** Next, we execute [e2] in the current thread using its specification, - ["H2"], which gives us that, if [e2] terminates at some value [v2], + ["H2"], which gives us that if [e2] terminates at some value [v2], then [Q2 v2]. *) wp_apply ("H2" with "HP2"). diff --git a/theories/ticket_lock.v b/theories/ticket_lock.v index 253fca8..bbe2757 100644 --- a/theories/ticket_lock.v +++ b/theories/ticket_lock.v @@ -14,12 +14,12 @@ From iris.heap_lang Require Import lang proofmode notation. lock makes them wait in line. It functions similarly to a ticketing system that one often finds in bakeries and pharmacies. Upon entering the shop, you pick a ticket with some number and wait until the number - on the screen has reached your number. Once this happen, it becomes + on the screen has reached your number. Once this happens, it becomes your turn to speak to the shop assistant. In our scenario, talking to the shop assistant corresponds to accessing the protected resources. To implement this, we will maintain two counters: [o] and [n]. The - first counter, [o], represent the number on the screen – the customer + first counter, [o], represents the number on the screen – the customer currently being served. The second counter, [n], represents the next number to be dispensed by the ticketing machine. @@ -27,7 +27,7 @@ From iris.heap_lang Require Import lang proofmode notation. and keep its previous value as a ticket for a position in the queue. Once the ticket has been obtained, the thread must wait until the first counter, [o], reaches its ticket value. Once this happens, the - thread gets access the protected resources. The thread can then + thread gets access to the protected resources. The thread can then release the lock by incrementing the first counter. *) @@ -55,9 +55,9 @@ Definition release : val := (** As a ticket lock is a lock, we expect it to satisfy the same - specification as the spin-lock. This time you have to come up with the - necessary resource algebra and lock invariant by yourself. It might be - instructive to first look through all required predicates and + specification as the spin-lock. This time, you have to come up with + the necessary resource algebra and lock invariant by yourself. It + might be instructive to first look through all required predicates and specifications to figure out exactly what needs to be proven. *) diff --git a/theories/ticket_lock_advanced.v b/theories/ticket_lock_advanced.v index 6151408..fa01560 100644 --- a/theories/ticket_lock_advanced.v +++ b/theories/ticket_lock_advanced.v @@ -3,34 +3,17 @@ From iris.base_logic.lib Require Export invariants. From iris.heap_lang Require Import lang proofmode notation. (* ################################################################# *) -(** * Case Study: Ticket Lock *) - -(* ================================================================= *) -(** ** Implementation *) +(** * Case Study: Ticket Lock Advanced *) (** - Let us look at another implementation of a lock, namely a ticket lock. - Instead of having every thread fight to acquire the lock, the ticket - lock makes them wait in line. It functions similarly to a ticketing - system that one often finds in bakeries and pharmacies. Upon entering - the shop, you pick a ticket with some number and wait until the number - on the screen has reached your number. Once this happen, it becomes - your turn to speak to the shop assistant. In our scenario, talking to - the shop assistant corresponds to accessing the protected resources. - - To implement this, we will maintain two counters: [o] and [n]. The - first counter, [o], represent the number on the screen – the customer - currently being served. The second counter, [n], represents the next - number to be dispensed by the ticketing machine. - - To acquire the lock, a thread must increment the second counter, [n], - and keep its previous value as a ticket for a position in the queue. - Once the ticket has been obtained, the thread must wait until the - first counter, [o], reaches its ticket value. Once this happens, the - thread gets access the protected resources. The thread can then - release the lock by incrementing the first counter. + The implementation, resource algebra, and representation predicates + are identical to the original Ticket Lock chapter. Only the proofs + differ. *) +(* ================================================================= *) +(** ** Implementation *) + Definition mk_lock : val := λ: <>, (ref #0, ref #0). @@ -53,98 +36,35 @@ Definition release : val := (* ================================================================= *) (** ** Representation Predicates *) -(** - As a ticket lock is a lock, we expect it to satisfy the same - specification as the spin-lock. This time you have to come up with the - necessary resource algebra and lock invariant by yourself. It might be - instructive to first look through all required predicates and - specifications to figure out exactly what needs to be proven. -*) - -Definition RA : cmra -(* BEGIN SOLUTION *) - (** - We will use a finite set of numbers to represent the tickets that - have been issued – the second counter. This becomes a camera by - using the disjoint union as an operation. - - For the first counter, we will use the exclusive camera over the - natural numbers – this means that there can be only one - access-granting ticket owned at a time. - - By wrapping them both in an authoritative camera, we can use the - authoritative fragment to bind the values of our counters to the - ghost state. - *) - := authR (prodUR (optionUR (exclR natO)) (gset_disjR nat)). -(* END SOLUTION BEGIN TEMPLATE - (* := insert your definition here *). Admitted. -END TEMPLATE *) +Definition RA : cmra := + authR (prodUR (optionUR (exclR natO)) (gset_disjR nat)). Section proofs. Context `{!heapGS Σ, !inG Σ RA}. Let N := nroot .@ "ticket_lock". -(** - This time around, we know that the thread is locked by a thread with a - specific ticket. As such, we first define a predicate [locked_by] - which states that the lock is locked by ticket [o]. -*) -Definition locked_by (γ : gname) (o : nat) : iProp Σ -(* BEGIN SOLUTION *) - (** - We know that the lock is locked by ticket [o] when we have ownership - of the exclusive counter being [o]. - *) - := own γ (◯ (Excl' o, GSet ∅)). -(* END SOLUTION BEGIN TEMPLATE - (* := insert your definition here *). Admitted. -END TEMPLATE *) +Definition locked_by (γ : gname) (o : nat) : iProp Σ := + own γ (◯ (Excl' o, GSet ∅)). -(** The lock is locked when it has been locked by some ticket. *) Definition locked (γ : gname) : iProp Σ := ∃ o, locked_by γ o. Lemma locked_excl γ : locked γ -∗ locked γ -∗ False. -(* SOLUTION *) Proof. +Proof. iIntros "[%o1 H1] [%o2 H2]". iDestruct (own_valid_2 with "H1 H2") as %[]%auth_frag_valid_1; done. Qed. -(** - We will also have a predicate signifying that ticket [x] has been - _issued_. A thread will need to have been issued ticket [x] in order - to wait for the first counter to become [x]. -*) -Definition issued (γ : gname) (x : nat) : iProp Σ -(* BEGIN SOLUTION *) - (** A ticket is simply the singleton set over its index. *) - := own γ (◯ (ε : option (excl nat), GSet {[x]})). -(* END SOLUTION BEGIN TEMPLATE - (* := insert your definition here *). Admitted. -END TEMPLATE *) - -Definition lock_inv (γ : gname) (lo ln : loc) (P : iProp Σ) : iProp Σ -(* BEGIN SOLUTION *) - (** - Our invariant will first link the authoritative fragment to the - counters. For the second counter, this means that all tickets prior - to the counter's current value must have been issued. +Definition issued (γ : gname) (x : nat) : iProp Σ := + own γ (◯ (ε : option (excl nat), GSet {[x]})). - Secondly, the lock contains either ownership of the value of the - first counter as well as the protected resources (the queue is - unlocked), or the current access-granting ticket (the queue is - locked). - *) - := ∃ o n : nat, lo ↦ #o ∗ ln ↦ #n ∗ +Definition lock_inv (γ : gname) (lo ln : loc) (P : iProp Σ) : iProp Σ := + ∃ o n : nat, lo ↦ #o ∗ ln ↦ #n ∗ own γ (● (Excl' o, GSet (set_seq 0 n))) ∗ ( (locked_by γ o ∗ P) ∨ issued γ o ). -(* END SOLUTION BEGIN TEMPLATE - (* := insert your definition here *). Admitted. -END TEMPLATE *) Definition is_lock (γ : gname) (l : val) (P : iProp Σ) : iProp Σ := ∃ lo ln : loc, ⌜l = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln P). @@ -154,7 +74,7 @@ Definition is_lock (γ : gname) (l : val) (P : iProp Σ) : iProp Σ := Lemma mk_lock_spec P : {{{ P }}} mk_lock #() {{{ γ l, RET l; is_lock γ l P }}}. -(* SOLUTION *) Proof. +Proof. iIntros "%Φ HP HΦ". wp_lam. wp_alloc lo; wp_alloc ln. @@ -170,7 +90,7 @@ Lemma wait_spec γ l P x : {{{ is_lock γ l P ∗ issued γ x }}} wait #x l {{{ RET #(); locked γ ∗ P }}}. -(* SOLUTION *) Proof. +Proof. iIntros "%Φ [(%lo & %ln & -> & #I) Hx] HΦ". iLöb as "IH". wp_rec. @@ -199,7 +119,7 @@ Qed. Lemma acquire_spec γ l P : {{{ is_lock γ l P }}} acquire l {{{ RET #(); locked γ ∗ P }}}. -(* SOLUTION *) Proof. +Proof. iIntros "%Φ (%lo & %ln & -> & #I) HΦ". iLöb as "IH". wp_rec. @@ -236,7 +156,7 @@ Qed. Lemma release_spec γ l P : {{{ is_lock γ l P ∗ locked γ ∗ P }}} release l {{{ RET #(); True }}}. -(* SOLUTION *) Proof. +Proof. iIntros "%Φ ((%lo & %ln & -> & #I) & [%o Hexcl] & HP) HΦ". wp_lam. wp_pures. diff --git a/theories/timeless.v b/theories/timeless.v index 31721ba..342b217 100644 --- a/theories/timeless.v +++ b/theories/timeless.v @@ -14,7 +14,7 @@ Context `{!heapGS Σ}. A large class of propositions do not depend on time; they are either always true or always false. An example is equalities; [2 + 2 = 4] is always true. We call such propositions _timeless_. All pure - propositions are timeless and ownership of a resource is timeless if + propositions are timeless, and ownership of a resource is timeless if the resource comes from a resource algebra (this includes points-to predicates). Further, timelessness is preserved by most connectives. As a rule of thumb, a predicate is timeless if @@ -89,7 +89,7 @@ Qed. (** The last scenario we mention is when the goal contains a later. In - this case, we may remove laters from timeless hypotheses, without + this case, we may remove laters from timeless hypotheses without removing the later from the goal. *) @@ -105,7 +105,7 @@ Qed. (** Timeless propositions are especially useful in connection with - invariants. Recall from the invariants chapter that, when we open an + invariants. Recall from the invariants chapter that when we open an invariant, [inv N P], we only get the resources _later_, [▷P]. Often, however, we require the resources now. Consider the following example. *)