.gitattributes

+*.v gitlab-language=coq
+
+# Convert to native line endings on checkout.
+*.ref text
+# Shell scripts need Linux line endings.
+*.sh eol=lf

.gitignore

 *.vo
+*.vos
+*.vok
+*.vio
 *.v.d
+.coqdeps.d
 *.glob
 *.cache
 *.aux
@@ -7,5 +11,17 @@
 .\#*
 *~
 *.bak
+.coqdeps.d
 .coq-native/
+*.crashcoqide
+.env
+builddep/
+_CoqProject.*
 Makefile.coq
+Makefile.coq.conf
+.Makefile.coq.d
+Makefile.package.*
+.Makefile.package.*
+_opam
+_build
+*.install

.gitlab-ci.yml

-image: coq:8.5
+image: ralfjung/opam-ci:opam2
 
-buildjob:
+stages:
+  - build
+
+variables:
+  CPU_CORES: "10"
+  OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
+  # Avoid needlessly increasing our TCB with native_compute
+  COQEXTRAFLAGS: "-native-compiler no"
+
+.only_branches: &only_branches
+  only:
+  - /^master/@iris/iris
+  - /^ci/@iris/iris
+
+.only_mr: &only_mr
+  only:
+  - merge_requests
+
+.branches_and_mr: &branches_and_mr
+  only:
+  - /^master/@iris/iris
+  - /^ci/@iris/iris
+  - merge_requests
+
+.template: &template
+  <<: *only_branches
+  stage: build
+  interruptible: true
   tags:
-  - coq
+  - fp
   script:
-  - 'make -j8 TIMED=y 2>&1 | tee build-log.txt'
-  - 'cat build-log.txt  | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" > build-time.txt'
-  artifacts:
+  - git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
+  - ci/buildjob
+  cache:
+    key: "$CI_JOB_NAME"
     paths:
-    - build-time.txt
+    - _opam/
+  except:
+  - triggers
+  - schedules
+  - api
+
+## Build jobs
+
+# The newest version runs with timing.
+build-coq.8.20.1:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.20.1"
+    DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
+    OPAM_PKG: "1"
+    DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
+    DOC_OPTS: "--external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp"
+  tags:
+  - fp-timing
+  interruptible: false
+
+# The newest version also runs in MRs, without timing.
+build-coq.8.20.1-mr:
+  <<: *template
+  <<: *only_mr
+  variables:
+    OPAM_PINS: "coq version 8.20.1"
+    DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
+
+# Also ensure Dune works.
+build-coq.8.20.1-dune:
+  <<: *template
+  <<: *branches_and_mr
+  variables:
+    OPAM_PINS: "coq version 8.20.1   dune version 3.15.2"
+    MAKE_TARGET: "dune"
+
+# The oldest version runs in MRs, without name mangling.
+build-coq.8.19.2:
+  <<: *template
+  <<: *branches_and_mr
+  variables:
+    OPAM_PINS: "coq version 8.19.2"
+
+trigger-stdpp.dev:
+  <<: *template
+  variables:
+    STDPP_REPO: "iris/stdpp"
+    OPAM_PINS: "coq version $NIGHTLY_COQ   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV"
+    CI_COQCHK: "1"
+  except:
+  only:
+  - triggers
+  - schedules
+  - api

.gitlab/issue_templates/Bug.md

+<!--
+
+When reporting a bug, please always include the version of Iris you are using.
+If you are using opam, you can determine your Iris version by running
+
+  opam show coq-iris -f version
+
+-->

CONTRIBUTING.md

+# Contributing to the Iris Coq Development
+
+Here you can find some how-tos for various thing sthat might come up when doing
+Iris development.  This is for contributing to Iris itself; see
+[the README](README.md#further-resources) for resources helpful for all Iris
+users.
+
+To work on Iris itself, you need to install its build-dependencies.  Again we
+recommend you do that with opam (2.0.0 or newer).  This requires the following
+two repositories:
+
+    opam repo add coq-released https://coq.inria.fr/opam/released
+    opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+
+Once you got opam set up, run `make builddep` to install the right versions
+of the dependencies.
+
+Run `make -jN` to build the full development, where `N` is the number of your
+CPU cores.
+
+To update Iris, do `git pull`.  After an update, the development may fail to
+compile because of outdated dependencies.  To fix that, please run `opam update`
+followed by `make builddep`.
+
+## How to submit a merge request
+
+To contribute code, you need an MPI-SWS GitLab account as described on the
+[chat page](https://iris-project.org/chat.html).  Then you can fork the
+[Iris git repository][iris], make your changes in your fork, and create a merge
+request.  If forking fails with an error, please send your MPI-SWS GitLab
+username to [Ralf Jung][jung] to unlock forks for your account.
+
+Please do *not* use the master branch of your fork, that might confuse CI.  Use
+a feature branch instead.
+
+[jung]: https://gitlab.mpi-sws.org/jung
+[iris]: https://gitlab.mpi-sws.org/iris/iris
+
+We prefer small and self-contained merge requests that add a single feature
+over merge requests that add arbitrary collections of lemmas. Small merge
+requests are easier to review, and will typically be merged more quickly
+(because it avoids blocking the whole merge request on a single
+discussion).
+
+Please follow the coding style laid out in our [style
+guide](docs/style_guide.md).
+
+## How to update the std++ dependency
+
+* Do the change in std++, push it.
+* Wait for CI to publish a new std++ version on the opam archive, then run
+  `opam update iris-dev`.
+* In Iris, change the `opam` file to depend on the new version.
+  (In case you do not use opam yourself, you can see recently published versions
+  [in this repository](https://gitlab.mpi-sws.org/iris/opam/commits/master).)
+* Run `make builddep` (in Iris) to install the new version of std++.
+  You may have to do `make clean` as Coq will likely complain about .vo file
+  mismatches.
+
+## How to write/update test cases
+
+The files in `tests/` are test cases.  Each of the `.v` files comes with a
+matching `.ref` file containing the expected output of `coqc`.  Adding `Show.`
+in selected places in the proofs makes `coqc` print the current goal state.
+This is used to make sure the proof mode prints goals and reduces terms the way
+we expect it to.  You can run `make MAKE_REF=1` to re-generate all the `.ref` files;
+this is useful after adding or removing `Show.` from a test.  If you do this,
+make sure to check the diff for any unexpected changes in the output!
+
+Some test cases have per-Coq-version `.ref` files (e.g., `atomic.8.8.ref` is a
+Coq-8.8-specific `.ref` file).  If you change one of these, remember to update
+*all* the `.ref` files.
+
+If you want to compile without tests run `make NO_TEST=1`.
+
+## How to build/install only one package
+
+Iris is split into multiple packages that can be installed separately via opam.
+You can invoke the Makefile of a particular package by doing `./make-package
+$PACKAGE $MAKE_ARGS`, where `$MAKE_ARGS` are passed to `make` (so you can use
+the usual `-jN`, `install`, ...).  This should only rarely be necessary. For
+example, if you are not using opam and you want to install only the `iris`
+package (without HeapLang, to avoid waiting on that part of the build), you can
+do `./make-package iris install`.  (If you are using opam, you can achieve the
+same by pinning `coq-iris` to your Iris checkout.)
+
+Note that `./make-package` will never run the test suite, so please always do a
+regular `make -jN` before submitting an MR.
+
+## How to test effects on reverse dependencies
+
+The `iris-bot` script makes it easy to test the effect of a branch on reverse
+dependencies. It can start tests ensuring they all still build, and it can do
+comparative timing runs.
+
+If you have suitable permissions, you can trigger these builds yourself.
+But first, you need to do some setup: you need to create a GitLab access token
+and set the `GITLAB_TOKEN` environment variable to it. Go to
+<https://gitlab.mpi-sws.org/-/profile/personal_access_tokens>, pick a suitable
+name (such as "iris-bot"), select the "api" scope, and then click "Create
+personal access token". Copy the value it shows and store it in some suitable
+place; you will not be able to retrieve this value from GitLab in the future!
+For example, you could create a `.env` file in your Iris clone containing:
+```
+export GITLAB_TOKEN=<your token here>
+```
+Then you can easily get the token back into the environment via `. .env`.
+
+Once that setup is done, you can now use `iris-bot`. Set at least one of
+`IRIS_REV` or `STDPP_REV` to control which branches of these projects to build
+against (they default to the default git branch). `IRIS_REPO` and `STDPP_REPO`
+can be used to control the repository in which the branch is situated. Setting
+`IRIS` to "user:branch" will use the given branch on that user's fork of Iris,
+and similar for `STDPP`.
+
+Supported commands:
+- `./iris-bot build [$filter]`: Builds all reverse dependencies against the
+  given branches. The optional `filter` argument only builds projects whose
+  names contains that string.
+- `./iris-bot time $project`: Measure the impact of this branch on the build
+  time of the given reverse dependency. Only Iris branches are supported for
+  now.
+
+Examples:
+- `IRIS_REV=myname/mybranch ./iris-bot build` builds *all* reverse dependencies
+  against `myname/mybranch` from the main Iris repository.
+- `IRIS=user:branch ./iris-bot build examples` builds the [examples] against
+  the `branch` in `user`'s fork of Iris.
+- `IRIS_REV=myname/mybranch ./iris-bot time examples` measures the timing impact
+  of `myname/mybranch` from the main Iris repository on the [examples].
+
+[examples]: https://gitlab.mpi-sws.org/iris/examples

LICENSE

-All files in this development, excluding those in docs/, are distributed
-under the terms of the BSD license, included below.
-
-------------------------------------------------------------------------------
-
-                            BSD LICENCE
-
-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.
-    * Neither the name of the <organization> nor the
-      names of its contributors may be used to endorse or promote products
-      derived from this software without specific prior written permission.
-
-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 <COPYRIGHT HOLDER> 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.
+The source code (i.e., everything except for files in the docs/ and tex/
+folders) in this development is licensed under the terms of the BSD license,
+while the documentation (i.e., everything inside the docs/ and tex/ folders) is
+licensed under the terms of the CC-BY 4.0 license.  Fur further details, see
+LICENSE-CODE and LICENSE-DOCS, respectively.

LICENSE-CODE

+All files in this development, excluding those in docs/ and tex/, are
+distributed under the terms of the 3-clause BSD license
+(https://opensource.org/licenses/BSD-3-Clause), included below.
+
+Copyright: Iris developers and contributors
+
+------------------------------------------------------------------------------
+
+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.
+    * Neither the name of the copyright holder nor the names of its contributors
+      may be used to endorse or promote products derived from this software
+      without specific prior written permission.
+
+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 HOLDER OR CONTRIBUTORS 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.

LICENSE-DOCS

+All files in the docs/ and tex/ folders of this development are distributed
+under the terms of the CC-BY 4.0 license <https://creativecommons.org/licenses/by/4.0/>.
+
+For your convenience, a plain-text version of the license is included below.
+
+------------------------------------------------------------------------------
+Attribution 4.0 International
+
+=======================================================================
+
+Creative Commons Corporation ("Creative Commons") is not a law firm and
+does not provide legal services or legal advice. Distribution of
+Creative Commons public licenses does not create a lawyer-client or
+other relationship. Creative Commons makes its licenses and related
+information available on an "as-is" basis. Creative Commons gives no
+warranties regarding its licenses, any material licensed under their
+terms and conditions, or any related information. Creative Commons
+disclaims all liability for damages resulting from their use to the
+fullest extent possible.
+
+Using Creative Commons Public Licenses
+
+Creative Commons public licenses provide a standard set of terms and
+conditions that creators and other rights holders may use to share
+original works of authorship and other material subject to copyright
+and certain other rights specified in the public license below. The
+following considerations are for informational purposes only, are not
+exhaustive, and do not form part of our licenses.
+
+     Considerations for licensors: Our public licenses are
+     intended for use by those authorized to give the public
+     permission to use material in ways otherwise restricted by
+     copyright and certain other rights. Our licenses are
+     irrevocable. Licensors should read and understand the terms
+     and conditions of the license they choose before applying it.
+     Licensors should also secure all rights necessary before
+     applying our licenses so that the public can reuse the
+     material as expected. Licensors should clearly mark any
+     material not subject to the license. This includes other CC-
+     licensed material, or material used under an exception or
+     limitation to copyright. More considerations for licensors:
+	wiki.creativecommons.org/Considerations_for_licensors
+
+     Considerations for the public: By using one of our public
+     licenses, a licensor grants the public permission to use the
+     licensed material under specified terms and conditions. If
+     the licensor's permission is not necessary for any reason--for
+     example, because of any applicable exception or limitation to
+     copyright--then that use is not regulated by the license. Our
+     licenses grant only permissions under copyright and certain
+     other rights that a licensor has authority to grant. Use of
+     the licensed material may still be restricted for other
+     reasons, including because others have copyright or other
+     rights in the material. A licensor may make special requests,
+     such as asking that all changes be marked or described.
+     Although not required by our licenses, you are encouraged to
+     respect those requests where reasonable. More_considerations
+     for the public: 
+	wiki.creativecommons.org/Considerations_for_licensees
+
+=======================================================================
+
+Creative Commons Attribution 4.0 International Public License
+
+By exercising the Licensed Rights (defined below), You accept and agree
+to be bound by the terms and conditions of this Creative Commons
+Attribution 4.0 International Public License ("Public License"). To the
+extent this Public License may be interpreted as a contract, You are
+granted the Licensed Rights in consideration of Your acceptance of
+these terms and conditions, and the Licensor grants You such rights in
+consideration of benefits the Licensor receives from making the
+Licensed Material available under these terms and conditions.
+
+
+Section 1 -- Definitions.
+
+  a. Adapted Material means material subject to Copyright and Similar
+     Rights that is derived from or based upon the Licensed Material
+     and in which the Licensed Material is translated, altered,
+     arranged, transformed, or otherwise modified in a manner requiring
+     permission under the Copyright and Similar Rights held by the
+     Licensor. For purposes of this Public License, where the Licensed
+     Material is a musical work, performance, or sound recording,
+     Adapted Material is always produced where the Licensed Material is
+     synched in timed relation with a moving image.
+
+  b. Adapter's License means the license You apply to Your Copyright
+     and Similar Rights in Your contributions to Adapted Material in
+     accordance with the terms and conditions of this Public License.
+
+  c. Copyright and Similar Rights means copyright and/or similar rights
+     closely related to copyright including, without limitation,
+     performance, broadcast, sound recording, and Sui Generis Database
+     Rights, without regard to how the rights are labeled or
+     categorized. For purposes of this Public License, the rights
+     specified in Section 2(b)(1)-(2) are not Copyright and Similar
+     Rights.
+
+  d. Effective Technological Measures means those measures that, in the
+     absence of proper authority, may not be circumvented under laws
+     fulfilling obligations under Article 11 of the WIPO Copyright
+     Treaty adopted on December 20, 1996, and/or similar international
+     agreements.
+
+  e. Exceptions and Limitations means fair use, fair dealing, and/or
+     any other exception or limitation to Copyright and Similar Rights
+     that applies to Your use of the Licensed Material.
+
+  f. Licensed Material means the artistic or literary work, database,
+     or other material to which the Licensor applied this Public
+     License.
+
+  g. Licensed Rights means the rights granted to You subject to the
+     terms and conditions of this Public License, which are limited to
+     all Copyright and Similar Rights that apply to Your use of the
+     Licensed Material and that the Licensor has authority to license.
+
+  h. Licensor means the individual(s) or entity(ies) granting rights
+     under this Public License.
+
+  i. Share means to provide material to the public by any means or
+     process that requires permission under the Licensed Rights, such
+     as reproduction, public display, public performance, distribution,
+     dissemination, communication, or importation, and to make material
+     available to the public including in ways that members of the
+     public may access the material from a place and at a time
+     individually chosen by them.
+
+  j. Sui Generis Database Rights means rights other than copyright
+     resulting from Directive 96/9/EC of the European Parliament and of
+     the Council of 11 March 1996 on the legal protection of databases,
+     as amended and/or succeeded, as well as other essentially
+     equivalent rights anywhere in the world.
+
+  k. You means the individual or entity exercising the Licensed Rights
+     under this Public License. Your has a corresponding meaning.
+
+
+Section 2 -- Scope.
+
+  a. License grant.
+
+       1. Subject to the terms and conditions of this Public License,
+          the Licensor hereby grants You a worldwide, royalty-free,
+          non-sublicensable, non-exclusive, irrevocable license to
+          exercise the Licensed Rights in the Licensed Material to:
+
+            a. reproduce and Share the Licensed Material, in whole or
+               in part; and
+
+            b. produce, reproduce, and Share Adapted Material.
+
+       2. Exceptions and Limitations. For the avoidance of doubt, where
+          Exceptions and Limitations apply to Your use, this Public
+          License does not apply, and You do not need to comply with
+          its terms and conditions.
+
+       3. Term. The term of this Public License is specified in Section
+          6(a).
+
+       4. Media and formats; technical modifications allowed. The
+          Licensor authorizes You to exercise the Licensed Rights in
+          all media and formats whether now known or hereafter created,
+          and to make technical modifications necessary to do so. The
+          Licensor waives and/or agrees not to assert any right or
+          authority to forbid You from making technical modifications
+          necessary to exercise the Licensed Rights, including
+          technical modifications necessary to circumvent Effective
+          Technological Measures. For purposes of this Public License,
+          simply making modifications authorized by this Section 2(a)
+          (4) never produces Adapted Material.
+
+       5. Downstream recipients.
+
+            a. Offer from the Licensor -- Licensed Material. Every
+               recipient of the Licensed Material automatically
+               receives an offer from the Licensor to exercise the
+               Licensed Rights under the terms and conditions of this
+               Public License.
+
+            b. No downstream restrictions. You may not offer or impose
+               any additional or different terms or conditions on, or
+               apply any Effective Technological Measures to, the
+               Licensed Material if doing so restricts exercise of the
+               Licensed Rights by any recipient of the Licensed
+               Material.
+
+       6. No endorsement. Nothing in this Public License constitutes or
+          may be construed as permission to assert or imply that You
+          are, or that Your use of the Licensed Material is, connected
+          with, or sponsored, endorsed, or granted official status by,
+          the Licensor or others designated to receive attribution as
+          provided in Section 3(a)(1)(A)(i).
+
+  b. Other rights.
+
+       1. Moral rights, such as the right of integrity, are not
+          licensed under this Public License, nor are publicity,
+          privacy, and/or other similar personality rights; however, to
+          the extent possible, the Licensor waives and/or agrees not to
+          assert any such rights held by the Licensor to the limited
+          extent necessary to allow You to exercise the Licensed
+          Rights, but not otherwise.
+
+       2. Patent and trademark rights are not licensed under this
+          Public License.
+
+       3. To the extent possible, the Licensor waives any right to
+          collect royalties from You for the exercise of the Licensed
+          Rights, whether directly or through a collecting society
+          under any voluntary or waivable statutory or compulsory
+          licensing scheme. In all other cases the Licensor expressly
+          reserves any right to collect such royalties.
+
+
+Section 3 -- License Conditions.
+
+Your exercise of the Licensed Rights is expressly made subject to the
+following conditions.
+
+  a. Attribution.
+
+       1. If You Share the Licensed Material (including in modified
+          form), You must:
+
+            a. retain the following if it is supplied by the Licensor
+               with the Licensed Material:
+
+                 i. identification of the creator(s) of the Licensed
+                    Material and any others designated to receive
+                    attribution, in any reasonable manner requested by
+                    the Licensor (including by pseudonym if
+                    designated);
+
+                ii. a copyright notice;
+
+               iii. a notice that refers to this Public License;
+
+                iv. a notice that refers to the disclaimer of
+                    warranties;
+
+                 v. a URI or hyperlink to the Licensed Material to the
+                    extent reasonably practicable;
+
+            b. indicate if You modified the Licensed Material and
+               retain an indication of any previous modifications; and
+
+            c. indicate the Licensed Material is licensed under this
+               Public License, and include the text of, or the URI or
+               hyperlink to, this Public License.
+
+       2. You may satisfy the conditions in Section 3(a)(1) in any
+          reasonable manner based on the medium, means, and context in
+          which You Share the Licensed Material. For example, it may be
+          reasonable to satisfy the conditions by providing a URI or
+          hyperlink to a resource that includes the required
+          information.
+
+       3. If requested by the Licensor, You must remove any of the
+          information required by Section 3(a)(1)(A) to the extent
+          reasonably practicable.
+
+       4. If You Share Adapted Material You produce, the Adapter's
+          License You apply must not prevent recipients of the Adapted
+          Material from complying with this Public License.
+
+
+Section 4 -- Sui Generis Database Rights.
+
+Where the Licensed Rights include Sui Generis Database Rights that
+apply to Your use of the Licensed Material:
+
+  a. for the avoidance of doubt, Section 2(a)(1) grants You the right
+     to extract, reuse, reproduce, and Share all or a substantial
+     portion of the contents of the database;
+
+  b. if You include all or a substantial portion of the database
+     contents in a database in which You have Sui Generis Database
+     Rights, then the database in which You have Sui Generis Database
+     Rights (but not its individual contents) is Adapted Material; and
+
+  c. You must comply with the conditions in Section 3(a) if You Share
+     all or a substantial portion of the contents of the database.
+
+For the avoidance of doubt, this Section 4 supplements and does not
+replace Your obligations under this Public License where the Licensed
+Rights include other Copyright and Similar Rights.
+
+
+Section 5 -- Disclaimer of Warranties and Limitation of Liability.
+
+  a. UNLESS OTHERWISE SEPARATELY UNDERTAKEN BY THE LICENSOR, TO THE
+     EXTENT POSSIBLE, THE LICENSOR OFFERS THE LICENSED MATERIAL AS-IS
+     AND AS-AVAILABLE, AND MAKES NO REPRESENTATIONS OR WARRANTIES OF
+     ANY KIND CONCERNING THE LICENSED MATERIAL, WHETHER EXPRESS,
+     IMPLIED, STATUTORY, OR OTHER. THIS INCLUDES, WITHOUT LIMITATION,
+     WARRANTIES OF TITLE, MERCHANTABILITY, FITNESS FOR A PARTICULAR
+     PURPOSE, NON-INFRINGEMENT, ABSENCE OF LATENT OR OTHER DEFECTS,
+     ACCURACY, OR THE PRESENCE OR ABSENCE OF ERRORS, WHETHER OR NOT
+     KNOWN OR DISCOVERABLE. WHERE DISCLAIMERS OF WARRANTIES ARE NOT
+     ALLOWED IN FULL OR IN PART, THIS DISCLAIMER MAY NOT APPLY TO YOU.
+
+  b. TO THE EXTENT POSSIBLE, IN NO EVENT WILL THE LICENSOR BE LIABLE
+     TO YOU ON ANY LEGAL THEORY (INCLUDING, WITHOUT LIMITATION,
+     NEGLIGENCE) OR OTHERWISE FOR ANY DIRECT, SPECIAL, INDIRECT,
+     INCIDENTAL, CONSEQUENTIAL, PUNITIVE, EXEMPLARY, OR OTHER LOSSES,
+     COSTS, EXPENSES, OR DAMAGES ARISING OUT OF THIS PUBLIC LICENSE OR
+     USE OF THE LICENSED MATERIAL, EVEN IF THE LICENSOR HAS BEEN
+     ADVISED OF THE POSSIBILITY OF SUCH LOSSES, COSTS, EXPENSES, OR
+     DAMAGES. WHERE A LIMITATION OF LIABILITY IS NOT ALLOWED IN FULL OR
+     IN PART, THIS LIMITATION MAY NOT APPLY TO YOU.
+
+  c. The disclaimer of warranties and limitation of liability provided
+     above shall be interpreted in a manner that, to the extent
+     possible, most closely approximates an absolute disclaimer and
+     waiver of all liability.
+
+
+Section 6 -- Term and Termination.
+
+  a. This Public License applies for the term of the Copyright and
+     Similar Rights licensed here. However, if You fail to comply with
+     this Public License, then Your rights under this Public License
+     terminate automatically.
+
+  b. Where Your right to use the Licensed Material has terminated under
+     Section 6(a), it reinstates:
+
+       1. automatically as of the date the violation is cured, provided
+          it is cured within 30 days of Your discovery of the
+          violation; or
+
+       2. upon express reinstatement by the Licensor.
+
+     For the avoidance of doubt, this Section 6(b) does not affect any
+     right the Licensor may have to seek remedies for Your violations
+     of this Public License.
+
+  c. For the avoidance of doubt, the Licensor may also offer the
+     Licensed Material under separate terms or conditions or stop
+     distributing the Licensed Material at any time; however, doing so
+     will not terminate this Public License.
+
+  d. Sections 1, 5, 6, 7, and 8 survive termination of this Public
+     License.
+
+
+Section 7 -- Other Terms and Conditions.
+
+  a. The Licensor shall not be bound by any additional or different
+     terms or conditions communicated by You unless expressly agreed.
+
+  b. Any arrangements, understandings, or agreements regarding the
+     Licensed Material not stated herein are separate from and
+     independent of the terms and conditions of this Public License.
+
+
+Section 8 -- Interpretation.
+
+  a. For the avoidance of doubt, this Public License does not, and
+     shall not be interpreted to, reduce, limit, restrict, or impose
+     conditions on any use of the Licensed Material that could lawfully
+     be made without permission under this Public License.
+
+  b. To the extent possible, if any provision of this Public License is
+     deemed unenforceable, it shall be automatically reformed to the
+     minimum extent necessary to make it enforceable. If the provision
+     cannot be reformed, it shall be severed from this Public License
+     without affecting the enforceability of the remaining terms and
+     conditions.
+
+  c. No term or condition of this Public License will be waived and no
+     failure to comply consented to unless expressly agreed to by the
+     Licensor.
+
+  d. Nothing in this Public License constitutes or may be interpreted
+     as a limitation upon, or waiver of, any privileges and immunities
+     that apply to the Licensor or You, including from the legal
+     processes of any jurisdiction or authority.
+
+
+=======================================================================
+
+Creative Commons is not a party to its public
+licenses. Notwithstanding, Creative Commons may elect to apply one of
+its public licenses to material it publishes and in those instances
+will be considered the “Licensor.” The text of the Creative Commons
+public licenses is dedicated to the public domain under the CC0 Public
+Domain Dedication. Except for the limited purpose of indicating that
+material is shared under a Creative Commons public license or as
+otherwise permitted by the Creative Commons policies published at
+creativecommons.org/policies, Creative Commons does not authorize the
+use of the trademark "Creative Commons" or any other trademark or logo
+of Creative Commons without its prior written consent including,
+without limitation, in connection with any unauthorized modifications
+to any of its public licenses or any other arrangements,
+understandings, or agreements concerning use of licensed material. For
+the avoidance of doubt, this paragraph does not form part of the
+public licenses.
+
+Creative Commons may be contacted at creativecommons.org.
+

Makefile

-# Makefile taken from coq-club, Christian Doczkal <doczkal@ps.uni-saarland.de>,
-# who adapted it from "somewhere".
+# Default target
 all: Makefile.coq
-	+make -f Makefile.coq all
+	+@$(MAKE) -f Makefile.coq all
+.PHONY: all
+
+# Build with dune.
+# This exists only for CI; you should just call `dune build` directly instead.
+dune:
+	@dune build --display=short
+.PHONY: dune
+
+# Permit local customization
+-include Makefile.local
+
+# Forward most targets to Coq makefile (with some trick to make this phony)
+%: Makefile.coq phony
+	@#echo "Forwarding $@"
+	+@$(MAKE) -f Makefile.coq $@
+phony: ;
+.PHONY: phony
 
 clean: Makefile.coq
-	+make -f Makefile.coq clean
-	rm -f Makefile.coq
+	+@$(MAKE) -f Makefile.coq clean
+	@# Make sure not to enter the `_opam` folder.
+	find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
+	rm -f Makefile.coq .lia.cache builddep/*
+.PHONY: clean
+
+# Create Coq Makefile.
+Makefile.coq: _CoqProject Makefile
+	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
+
+# Install build-dependencies
+OPAMFILES=$(wildcard *.opam)
+BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
+
+builddep/%-builddep.opam: %.opam Makefile
+	@echo "# Creating builddep package for $<."
+	@mkdir -p builddep
+	@sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
+
+builddep-opamfiles: $(BUILDDEPFILES)
+.PHONY: builddep-opamfiles
+
+builddep: builddep-opamfiles
+	@# We want opam to not just install the build-deps now, but to also keep satisfying these
+	@# constraints.  Otherwise, `opam upgrade` may well update some packages to versions
+	@# that are incompatible with our build requirements.
+	@# To achieve this, we create a fake opam package that has our build-dependencies as
+	@# dependencies, but does not actually install anything itself.
+	@echo "# Installing builddep packages."
+	@opam install $(OPAMFLAGS) $(BUILDDEPFILES)
+.PHONY: builddep
 
-Makefile.coq: _CoqProject
-	coq_makefile -f _CoqProject -o Makefile.coq
+# Backwards compatibility target
+build-dep: builddep
+.PHONY: build-dep
 
-.PHONY: all clean
+# Some files that do *not* need to be forwarded to Makefile.coq.
+# ("::" lets Makefile.local overwrite this.)
+Makefile Makefile.local _CoqProject $(OPAMFILES):: ;

Makefile.coq.local

+# use NO_TEST=1 to skip the tests
+NO_TEST:=
+
+# use MAKE_REF=1 to generate new reference files
+MAKE_REF:=
+
+# Only test reference output on known versions of Coq, to avoid blocking
+# Coq CI when they change the printing a little.
+# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
+COQ_REF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(20)\." -q && echo 1)
+
+# Run tests interleaved with main build.  They have to be in the same target for this.
+real-all: style $(if $(NO_TEST),,test)
+
+style: $(VFILES) coq-lint.sh
+# Make sure everything imports the options, and some general linting.
+	$(SHOW)"COQLINT"
+	$(HIDE)for FILE in $(VFILES); do \
+	  if ! grep -F -q 'From iris.prelude Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
+	  ./coq-lint.sh "$$FILE" || exit 1; \
+	done
+# Make sure main Iris does not import other Iris packages.
+	$(HIDE)if grep -E 'iris\.(heap_lang|deprecated|unstable)' --include "*.v" -R iris; then echo "ERROR: Iris may not import modules from other Iris packages (see above for violations)."; echo; exit 1; fi
+.PHONY: style
+
+# the test suite
+TESTFILES:=$(shell find tests -name "*.v")
+NORMALIZER:=test-normalizer.sed
+
+test: $(TESTFILES:.v=.vo)
+.PHONY: test
+
+COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
+
+tests/.coqdeps.d: $(TESTFILES)
+	$(SHOW)'COQDEP TESTFILES'
+	$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
+-include tests/.coqdeps.d
+
+# Main test script (comments out-of-line because macOS otherwise barfs?!?)
+# - Determine reference file (`REF`).
+# - Print user-visible status line.
+# - unset env vars that change Coq's output
+# - Dump Coq output into a temporary file.
+# - Run `sed -i` on that file in a way that works on macOS.
+# - Either compare the result with the reference file, or move it over the reference file.
+# - Cleanup, and mark as done for make.
+$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(NORMALIZER)
+	$(HIDE)REF=$*".ref" && \
+	  echo "COQTEST$(if $(COQ_REF),$(if $(MAKE_REF), [make ref],), [ref ignored]) $< (ref: $$REF)" && \
+	  TMPFILE="$$(mktemp)" && \
+	  unset OCAMLRUNPARAM && \
+	  $(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
+	  sed -E -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
+	  mv "$$TMPFILE".new "$$TMPFILE" && \
+	  $(if $(COQ_REF),\
+	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE"), \
+	    true \
+	  ) && \
+	  rm -f "$$TMPFILE" && \
+	  touch $@

README

-PREREQUISITES
--------------
-
-This version is known to compile with:
-
- - Coq 8.5
- - Ssreflect 1.6
-
-For development, better make sure you have a version of Ssreflect that includes
-commit be724937 (no such version has been released so far, you will have to
-fetch the development branch yourself). Iris compiles fine even without this
-patch, but proof bullets will only be in 'strict' (enforcing) mode with the
-fixed version of Ssreflect.
- 
-BUILDING INSTRUCTIONS
----------------------
-
-Run the following command to build the full development:
-
-  make

README.md

+# Iris Coq Development [[coqdoc]](https://plv.mpi-sws.org/coqdoc/iris/)
+
+This is the Coq development of the [Iris Project](http://iris-project.org),
+which includes [MoSeL](http://iris-project.org/mosel/), a general proof mode
+for carrying out separation logic proofs in Coq.
+
+For using the Coq library, check out the
+[API documentation](https://plv.mpi-sws.org/coqdoc/iris/).
+
+For understanding the theory of Iris, a LaTeX version of the core logic
+definitions and some derived forms is available in
+[tex/iris.tex](tex/iris.tex).  A compiled PDF version of this document is
+[available online](http://plv.mpi-sws.org/iris/appendix-3.4.pdf).
+
+## Side-effects
+
+Importing Iris has some side effects as the library sets some global options.
+
+* First of all, Iris imports std++, so the
+  [std++ side-effects](https://gitlab.mpi-sws.org/iris/stdpp/#side-effects)
+  apply.
+* On top of that, Iris imports ssreflect, which replaces the default `rewrite`
+  tactic with the ssreflect version. However, `done` is overwritten to keep
+  using the std++ version of the tactic.  We also set `SsrOldRewriteGoalsOrder`
+  and re-open `general_if_scope` to un-do some effects of ssreflect.
+
+## Building Iris
+
+### Prerequisites
+
+This version is known to compile with:
+
+ - Coq 8.19.2 / 8.20.1
+ - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
+
+Generally we always aim to support the last two stable Coq releases. Support for
+older versions will be dropped when it is convenient.
+
+If you need to work with older versions of Coq, you can check out the
+[tags](https://gitlab.mpi-sws.org/iris/iris/-/tags) for old Iris releases that
+still support them.
+
+### Working *with* Iris
+
+To use Iris in your own proofs, we recommend you install Iris via opam (2.0.0 or
+newer).  To obtain the latest stable release, you have to add the Coq opam
+repository:
+
+    opam repo add coq-released https://coq.inria.fr/opam/released
+
+To obtain a development version, also add the Iris opam repository:
+
+    opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+
+Either way, you can now install Iris:
+- `opam install coq-iris` will install the libraries making up the Iris logic,
+  but leave it up to you to instantiate the `program_logic.language` interface
+  to define a programming language for Iris to reason about.
+- `opam install coq-iris-heap-lang` will additionally install HeapLang, the
+  default language used by various Iris projects.
+
+To fetch updates later, run `opam update && opam upgrade`.
+
+#### Be notified of breaking changes
+
+We do not guarantee backwards-compatibility, so upgrading Iris may break your
+Iris-using developments.  If you want to be notified of breaking changes, please
+let us know your account name on the
+[MPI-SWS GitLab](https://gitlab.mpi-sws.org/) so we can add you to the
+notification group.  Note that this excludes the "unstable" and "deprecated"
+packages (see below).
+
+#### Use of Iris in submitted artifacts
+
+If you are using Iris as part of an artifact submitted for publication with a
+paper, we recommend you make the artifact self-contained so that it can be built
+in the future without relying in any other server to still exist. However, if
+that is for some reason not possible, and if you are using opam to obtain the
+right version of Iris and you used a `dev.*` version, please let us know which
+exact Iris version you artifact relies on so that we can
+[add it to this wiki page](https://gitlab.mpi-sws.org/iris/iris/-/wikis/Pinned-Iris-package-versions)
+and avoid removing it from our opam repository in the future.
+
+### Working *on* Iris
+
+See the [contribution guide](CONTRIBUTING.md) for information on how to work on
+the Iris development itself.
+
+## Directory Structure
+
+Iris is structured into multiple *packages*, some of which contain multiple
+modules in separate folders.
+
+* The [iris](iris) package contains the language-independent parts of Iris.
+  + The folder [prelude](iris/prelude) contains modules imported everywhere in
+    Iris.
+  + The folder [algebra](iris/algebra) contains the COFE and CMRA
+    constructions as well as the solver for recursive domain equations.
+    - The subfolder [lib](iris/algebra/lib) contains some general derived RA
+      constructions.
+  + The folder [bi](iris/bi) contains the BI++ laws, as well as derived
+    connectives, laws and constructions that are applicable for general BIs.
+    - The subfolder [lib](iris/bi/lib) contains some general derived logical
+      constructions.
+  + The folder [proofmode](iris/proofmode) contains
+    [MoSeL](http://iris-project.org/mosel/), which extends Coq with contexts for
+    intuitionistic and spatial BI++ assertions. It also contains tactics for
+    interactive proofs. Documentation can be found in
+    [proof_mode.md](docs/proof_mode.md).
+  + The folder [base_logic](iris/base_logic) defines the Iris base logic and
+    the primitive connectives.  It also contains derived constructions that are
+    entirely independent of the choice of resources.
+    - The subfolder [lib](iris/base_logic/lib) contains some generally useful
+      derived constructions.  Most importantly, it defines composable
+      dynamic resources and ownership of them; the other constructions depend
+      on this setup.
+  + The folder [program_logic](iris/program_logic) specializes the base logic
+    to build Iris, the program logic.   This includes weakest preconditions that
+    are defined for any language satisfying some generic axioms, and some derived
+    constructions that work for any such language.
+  + The folder [si_logic](iris/si_logic) defines a "plain" step-indexed logic
+    and shows that it is an instance of the BI interface.
+* The [iris_heap_lang](iris_heap_lang) package defines the ML-like concurrent
+  language HeapLang and provides tactic support and proof mode integration.
+  + The subfolder [lib](iris_heap_lang/lib) contains a few derived
+    constructions within this language, e.g., parallel composition.
+    For more examples of using Iris and heap_lang, have a look at the
+    [Iris Examples](https://gitlab.mpi-sws.org/iris/examples).
+* The [iris_unstable](iris_unstable) package contains libraries that are not yet
+  ready for inclusion in Iris proper. For each library, there is a corresponding
+  "tracking issue" in the Iris issue tracker (also linked from the library
+  itself) which tracks the work that still needs to be done before moving the
+  library to Iris. No stability guarantees whatsoever are made for this package.
+* The [iris_deprecated](iris_deprecated) package contains libraries that have been
+  removed from Iris proper, but are kept around to give users some more time to
+  switch to their intended replacements. The individual libraries come with comments
+  explaining the deprecation and making recommendations for what to use
+  instead. No stability guarantees whatsoever are made for this package.
+* The folder [tests](tests) contains modules we use to test our
+  infrastructure. These modules are not installed by `make install`, and should
+  not be imported.
+
+Note that the unstable and deprecated packages are not released, so they only
+exist in the development version of Iris.
+
+## Case Studies
+
+The following is a (probably incomplete) list of case studies that use Iris, and
+that should be compatible with this version:
+
+* [Iris Examples](https://gitlab.mpi-sws.org/iris/examples) is where we
+  collect miscellaneous case studies that do not have their own repository.
+* [LambdaRust](https://gitlab.mpi-sws.org/iris/lambda-rust) is a Coq
+  formalization of the core Rust type system.
+* [GPFSL](https://gitlab.mpi-sws.org/iris/gpfsl) is a logic for release-acquire
+  and relaxed memory.
+* [Iron](https://gitlab.mpi-sws.org/iris/iron) is a linear separation logic
+  built on top of Iris for precise reasoning about resources (such as making
+  sure there are no memory leaks).
+* [Actris](https://gitlab.mpi-sws.org/iris/actris) is a separation logic
+  built on top of Iris for session-type based reasoning of message-passing
+  programs.
+
+## Further Resources
+
+Getting along with Iris in Coq:
+
+* The coding style is documented in the [style guide](docs/style_guide.md).
+* Iris proof patterns and conventions are documented in the
+  [proof guide](docs/proof_guide.md).
+* Various notions of equality and logical entailment in Iris and their Coq
+  interface are described in the
+  [equality docs](docs/equalities_and_entailments.md).
+* The Iris tactics are described in the
+  [the Iris Proof Mode (IPM) / MoSeL documentation](docs/proof_mode.md) as well as the
+  [HeapLang documentation](docs/heap_lang.md).
+* The generated coqdoc is [available online](https://plv.mpi-sws.org/coqdoc/iris/).
+
+Contacting the developers:
+
+* Discussion about the Iris Coq development happens in the [Iris
+  Chat](https://iris-project.org/chat.html). This is also the right place to ask
+  questions.
+* If you want to report a bug, please use the
+  [issue tracker](https://gitlab.mpi-sws.org/iris/iris/issues), which requires
+  an MPI-SWS GitLab account. The [chat page](https://iris-project.org/chat.html)
+  describes how to create such an account.
+* To contribute to Iris itself, see the [contribution guide](CONTRIBUTING.md).
+
+Miscellaneous:
+
+* Information on how to set up your editor for unicode input and output is
+  collected in [editor.md](docs/editor.md).
+* If you are writing a paper that uses Iris in one way or another, you could use
+  the [Iris LaTeX macros](tex/iris.sty) for typesetting the various Iris
+  connectives.

_CoqProject

--Q . ""
-prelude/option.v
-prelude/fin_map_dom.v
-prelude/bsets.v
-prelude/fin_maps.v
-prelude/vector.v
-prelude/pmap.v
-prelude/stringmap.v
-prelude/fin_collections.v
-prelude/mapset.v
-prelude/proof_irrel.v
-prelude/hashset.v
-prelude/pretty.v
-prelude/countable.v
-prelude/orders.v
-prelude/natmap.v
-prelude/strings.v
-prelude/relations.v
-prelude/collections.v
-prelude/listset.v
-prelude/streams.v
-prelude/gmap.v
-prelude/base.v
-prelude/tactics.v
-prelude/prelude.v
-prelude/listset_nodup.v
-prelude/finite.v
-prelude/numbers.v
-prelude/nmap.v
-prelude/zmap.v
-prelude/co_pset.v
-prelude/lexico.v
-prelude/sets.v
-prelude/decidable.v
-prelude/list.v
-prelude/error.v
-prelude/functions.v
-algebra/option.v
-algebra/cmra.v
-algebra/cmra_big_op.v
-algebra/cmra_tactics.v
-algebra/sts.v
-algebra/auth.v
-algebra/fin_maps.v
-algebra/cofe.v
-algebra/base.v
-algebra/dra.v
-algebra/cofe_solver.v
-algebra/agree.v
-algebra/dec_agree.v
-algebra/excl.v
-algebra/iprod.v
-algebra/functor.v
-algebra/upred.v
-algebra/upred_tactics.v
-algebra/upred_big_op.v
-algebra/frac.v
-program_logic/model.v
-program_logic/adequacy.v
-program_logic/hoare_lifting.v
-program_logic/lifting.v
-program_logic/invariants.v
-program_logic/viewshifts.v
-program_logic/wsat.v
-program_logic/ownership.v
-program_logic/weakestpre.v
-program_logic/pviewshifts.v
-program_logic/resources.v
-program_logic/hoare.v
-program_logic/language.v
-program_logic/tests.v
-program_logic/ghost_ownership.v
-program_logic/global_functor.v
-program_logic/saved_prop.v
-program_logic/auth.v
-program_logic/sts.v
-program_logic/namespaces.v
-heap_lang/lang.v
-heap_lang/tactics.v
-heap_lang/wp_tactics.v
-heap_lang/lifting.v
-heap_lang/derived.v
-heap_lang/heap.v
-heap_lang/notation.v
-heap_lang/tests.v
-heap_lang/substitution.v
-barrier/barrier.v
-barrier/specification.v
-barrier/protocol.v
-barrier/proof.v
-barrier/client.v
+# Search paths for all packages. They must all match the regex
+# `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
+-Q iris/prelude iris.prelude
+-Q iris/algebra iris.algebra
+-Q iris/si_logic iris.si_logic
+-Q iris/bi iris.bi
+-Q iris/proofmode iris.proofmode
+-Q iris/base_logic iris.base_logic
+-Q iris/program_logic iris.program_logic
+-Q iris_heap_lang iris.heap_lang
+-Q iris_unstable iris.unstable
+-Q iris_deprecated iris.deprecated
+
+# Custom flags (to be kept in sync with the dune file at the root of the repo).
+# We sometimes want to locally override notation, and there is no good way to do that with scopes.
+-arg -w -arg -notation-overridden
+# Cannot use non-canonical projections as it causes massive unification failures
+# (https://github.com/coq/coq/issues/6294).
+-arg -w -arg -redundant-canonical-projection
+# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
+-arg -w -arg -notation-incompatible-prefix
+# We can't do this migration yet until we require Coq 9.0
+-arg -w -arg -deprecated-from-Coq
+-arg -w -arg -deprecated-dirpath-Coq
+
+iris/prelude/options.v
+iris/prelude/prelude.v
+iris/algebra/monoid.v
+iris/algebra/cmra.v
+iris/algebra/big_op.v
+iris/algebra/cmra_big_op.v
+iris/algebra/sts.v
+iris/algebra/numbers.v
+iris/algebra/view.v
+iris/algebra/auth.v
+iris/algebra/gmap.v
+iris/algebra/ofe.v
+iris/algebra/cofe_solver.v
+iris/algebra/agree.v
+iris/algebra/excl.v
+iris/algebra/functions.v
+iris/algebra/frac.v
+iris/algebra/dfrac.v
+iris/algebra/csum.v
+iris/algebra/list.v
+iris/algebra/vector.v
+iris/algebra/updates.v
+iris/algebra/local_updates.v
+iris/algebra/gset.v
+iris/algebra/gmultiset.v
+iris/algebra/coPset.v
+iris/algebra/proofmode_classes.v
+iris/algebra/ufrac.v
+iris/algebra/reservation_map.v
+iris/algebra/dyn_reservation_map.v
+iris/algebra/max_prefix_list.v
+iris/algebra/mra.v
+iris/algebra/lib/excl_auth.v
+iris/algebra/lib/frac_auth.v
+iris/algebra/lib/ufrac_auth.v
+iris/algebra/lib/dfrac_agree.v
+iris/algebra/lib/gmap_view.v
+iris/algebra/lib/mono_nat.v
+iris/algebra/lib/mono_Z.v
+iris/algebra/lib/mono_list.v
+iris/algebra/lib/gset_bij.v
+iris/si_logic/siprop.v
+iris/si_logic/bi.v
+iris/bi/notation.v
+iris/bi/interface.v
+iris/bi/derived_connectives.v
+iris/bi/extensions.v
+iris/bi/derived_laws.v
+iris/bi/derived_laws_later.v
+iris/bi/plainly.v
+iris/bi/internal_eq.v
+iris/bi/big_op.v
+iris/bi/updates.v
+iris/bi/ascii.v
+iris/bi/bi.v
+iris/bi/monpred.v
+iris/bi/embedding.v
+iris/bi/weakestpre.v
+iris/bi/telescopes.v
+iris/bi/lib/cmra.v
+iris/bi/lib/counterexamples.v
+iris/bi/lib/fixpoint_mono.v
+iris/bi/lib/fixpoint_banach.v
+iris/bi/lib/fractional.v
+iris/bi/lib/laterable.v
+iris/bi/lib/atomic.v
+iris/bi/lib/core.v
+iris/bi/lib/relations.v
+iris/base_logic/upred.v
+iris/base_logic/bi.v
+iris/base_logic/derived.v
+iris/base_logic/proofmode.v
+iris/base_logic/base_logic.v
+iris/base_logic/algebra.v
+iris/base_logic/bupd_alt.v
+iris/base_logic/lib/iprop.v
+iris/base_logic/lib/own.v
+iris/base_logic/lib/saved_prop.v
+iris/base_logic/lib/wsat.v
+iris/base_logic/lib/invariants.v
+iris/base_logic/lib/fancy_updates.v
+iris/base_logic/lib/boxes.v
+iris/base_logic/lib/na_invariants.v
+iris/base_logic/lib/cancelable_invariants.v
+iris/base_logic/lib/gen_heap.v
+iris/base_logic/lib/gen_inv_heap.v
+iris/base_logic/lib/fancy_updates_from_vs.v
+iris/base_logic/lib/proph_map.v
+iris/base_logic/lib/ghost_var.v
+iris/base_logic/lib/mono_nat.v
+iris/base_logic/lib/gset_bij.v
+iris/base_logic/lib/ghost_map.v
+iris/base_logic/lib/later_credits.v
+iris/base_logic/lib/token.v
+iris/program_logic/adequacy.v
+iris/program_logic/lifting.v
+iris/program_logic/weakestpre.v
+iris/program_logic/total_weakestpre.v
+iris/program_logic/total_adequacy.v
+iris/program_logic/language.v
+iris/program_logic/ectx_language.v
+iris/program_logic/ectxi_language.v
+iris/program_logic/ectx_lifting.v
+iris/program_logic/ownp.v
+iris/program_logic/total_lifting.v
+iris/program_logic/total_ectx_lifting.v
+iris/program_logic/atomic.v
+iris/proofmode/base.v
+iris/proofmode/ident_name.v
+iris/proofmode/string_ident.v
+iris/proofmode/tokens.v
+iris/proofmode/coq_tactics.v
+iris/proofmode/ltac_tactics.v
+iris/proofmode/environments.v
+iris/proofmode/reduction.v
+iris/proofmode/intro_patterns.v
+iris/proofmode/spec_patterns.v
+iris/proofmode/sel_patterns.v
+iris/proofmode/tactics.v
+iris/proofmode/notation.v
+iris/proofmode/classes.v
+iris/proofmode/classes_make.v
+iris/proofmode/class_instances.v
+iris/proofmode/class_instances_later.v
+iris/proofmode/class_instances_updates.v
+iris/proofmode/class_instances_embedding.v
+iris/proofmode/class_instances_plainly.v
+iris/proofmode/class_instances_internal_eq.v
+iris/proofmode/class_instances_frame.v
+iris/proofmode/class_instances_make.v
+iris/proofmode/monpred.v
+iris/proofmode/modalities.v
+iris/proofmode/modality_instances.v
+iris/proofmode/proofmode.v
+
+iris_heap_lang/locations.v
+iris_heap_lang/lang.v
+iris_heap_lang/class_instances.v
+iris_heap_lang/pretty.v
+iris_heap_lang/metatheory.v
+iris_heap_lang/tactics.v
+iris_heap_lang/primitive_laws.v
+iris_heap_lang/derived_laws.v
+iris_heap_lang/notation.v
+iris_heap_lang/proofmode.v
+iris_heap_lang/adequacy.v
+iris_heap_lang/total_adequacy.v
+iris_heap_lang/proph_erasure.v
+iris_heap_lang/lib/spawn.v
+iris_heap_lang/lib/par.v
+iris_heap_lang/lib/assert.v
+iris_heap_lang/lib/lock.v
+iris_heap_lang/lib/rw_lock.v
+iris_heap_lang/lib/spin_lock.v
+iris_heap_lang/lib/ticket_lock.v
+iris_heap_lang/lib/rw_spin_lock.v
+iris_heap_lang/lib/nondet_bool.v
+iris_heap_lang/lib/lazy_coin.v
+iris_heap_lang/lib/clairvoyant_coin.v
+iris_heap_lang/lib/counter.v
+iris_heap_lang/lib/atomic_heap.v
+iris_heap_lang/lib/increment.v
+iris_heap_lang/lib/diverge.v
+iris_heap_lang/lib/arith.v
+iris_heap_lang/lib/array.v
+iris_heap_lang/lib/logatom_lock.v
+
+iris_unstable/algebra/list.v
+iris_unstable/base_logic/algebra.v
+iris_unstable/base_logic/mono_list.v
+iris_unstable/heap_lang/interpreter.v
+
+iris_deprecated/base_logic/auth.v
+iris_deprecated/base_logic/sts.v
+iris_deprecated/base_logic/viewshifts.v
+iris_deprecated/program_logic/hoare.v

algebra/agree.v

-From algebra Require Export cmra.
-From algebra Require Import functor upred.
-Local Hint Extern 10 (_ ≤ _) => omega.
-
-Record agree (A : Type) : Type := Agree {
-  agree_car :> nat → A;
-  agree_is_valid : nat → Prop;
-  agree_valid_S n : agree_is_valid (S n) → agree_is_valid n
-}.
-Arguments Agree {_} _ _ _.
-Arguments agree_car {_} _ _.
-Arguments agree_is_valid {_} _ _.
-
-Section agree.
-Context {A : cofeT}.
-
-Instance agree_validN : ValidN (agree A) := λ n x,
-  agree_is_valid x n ∧ ∀ n', n' ≤ n → x n' ≡{n'}≡ x n.
-Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x.
-
-Lemma agree_valid_le n n' (x : agree A) :
-  agree_is_valid x n → n' ≤ n → agree_is_valid x n'.
-Proof. induction 2; eauto using agree_valid_S. Qed.
-
-Instance agree_equiv : Equiv (agree A) := λ x y,
-  (∀ n, agree_is_valid x n ↔ agree_is_valid y n) ∧
-  (∀ n, agree_is_valid x n → x n ≡{n}≡ y n).
-Instance agree_dist : Dist (agree A) := λ n x y,
-  (∀ n', n' ≤ n → agree_is_valid x n' ↔ agree_is_valid y n') ∧
-  (∀ n', n' ≤ n → agree_is_valid x n' → x n' ≡{n'}≡ y n').
-Program Instance agree_compl : Compl (agree A) := λ c,
-  {| agree_car n := c (S n) n; agree_is_valid n := agree_is_valid (c (S n)) n |}.
-Next Obligation.
-  intros c n ?. apply (chain_cauchy c n (S (S n))), agree_valid_S; auto.
-Qed.
-Definition agree_cofe_mixin : CofeMixin (agree A).
-Proof.
-  split.
-  - intros x y; split.
-    + by intros Hxy n; split; intros; apply Hxy.
-    + by intros Hxy; split; intros; apply Hxy with n.
-  - split.
-    + by split.
-    + by intros x y Hxy; split; intros; symmetry; apply Hxy; auto; apply Hxy.
-    + intros x y z Hxy Hyz; split; intros n'; intros.
-      * trans (agree_is_valid y n'). by apply Hxy. by apply Hyz.
-      * trans (y n'). by apply Hxy. by apply Hyz, Hxy.
-  - intros n x y Hxy; split; intros; apply Hxy; auto.
-  - intros n c; apply and_wlog_r; intros;
-      symmetry; apply (chain_cauchy c); naive_solver.
-Qed.
-Canonical Structure agreeC := CofeT agree_cofe_mixin.
-
-Lemma agree_car_ne n (x y : agree A) : ✓{n} x → x ≡{n}≡ y → x n ≡{n}≡ y n.
-Proof. by intros [??] Hxy; apply Hxy. Qed.
-Lemma agree_cauchy n (x : agree A) i : ✓{n} x → i ≤ n → x i ≡{i}≡ x n.
-Proof. by intros [? Hx]; apply Hx. Qed.
-
-Program Instance agree_op : Op (agree A) := λ x y,
-  {| agree_car := x;
-     agree_is_valid n := agree_is_valid x n ∧ agree_is_valid y n ∧ x ≡{n}≡ y |}.
-Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
-Instance agree_unit : Unit (agree A) := id.
-Instance agree_minus : Minus (agree A) := λ x y, x.
-
-Instance: Comm (≡) (@op (agree A) _).
-Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
-Lemma agree_idemp (x : agree A) : x ⋅ x ≡ x.
-Proof. split; naive_solver. Qed.
-Instance: ∀ n : nat, Proper (dist n ==> impl) (@validN (agree A) _ n).
-Proof.
-  intros n x y Hxy [? Hx]; split; [by apply Hxy|intros n' ?].
-  rewrite -(proj2 Hxy n') 1?(Hx n'); eauto using agree_valid_le.
-  by apply dist_le with n; try apply Hxy.
-Qed.
-Instance: ∀ x : agree A, Proper (dist n ==> dist n) (op x).
-Proof.
-  intros n x y1 y2 [Hy' Hy]; split; [|done].
-  split; intros (?&?&Hxy); repeat (intro || split);
-    try apply Hy'; eauto using agree_valid_le.
-  - etrans; [apply Hxy|apply Hy]; eauto using agree_valid_le.
-  - etrans; [apply Hxy|symmetry; apply Hy, Hy'];
-      eauto using agree_valid_le.
-Qed.
-Instance: Proper (dist n ==> dist n ==> dist n) (@op (agree A) _).
-Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
-Instance: Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _.
-Instance: Assoc (≡) (@op (agree A) _).
-Proof.
-  intros x y z; split; simpl; intuition;
-    repeat match goal with H : agree_is_valid _ _ |- _ => clear H end;
-    by cofe_subst; rewrite !agree_idemp.
-Qed.
-
-Lemma agree_included (x y : agree A) : x ≼ y ↔ y ≡ x ⋅ y.
-Proof.
-  split; [|by intros ?; exists y].
-  by intros [z Hz]; rewrite Hz assoc agree_idemp.
-Qed.
-Lemma agree_op_inv n (x1 x2 : agree A) : ✓{n} (x1 ⋅ x2) → x1 ≡{n}≡ x2.
-Proof. intros Hxy; apply Hxy. Qed.
-Lemma agree_valid_includedN n (x y : agree A) : ✓{n} y → x ≼{n} y → x ≡{n}≡ y.
-Proof.
-  move=> Hval [z Hy]; move: Hval; rewrite Hy.
-  by move=> /agree_op_inv->; rewrite agree_idemp.
-Qed.
-
-Definition agree_cmra_mixin : CMRAMixin (agree A).
-Proof.
-  split; try (apply _ || done).
-  - by intros n x1 x2 Hx y1 y2 Hy.
-  - intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
-    rewrite (Hx n'); last auto.
-    symmetry; apply dist_le with n; try apply Hx; auto.
-  - intros x; apply agree_idemp.
-  - by intros n x y [(?&?&?) ?].
-  - by intros x y; rewrite agree_included.
-  - intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
-    + by rewrite agree_idemp.
-    + by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
-Qed.
-Canonical Structure agreeRA : cmraT := CMRAT agree_cofe_mixin agree_cmra_mixin.
-
-Program Definition to_agree (x : A) : agree A :=
-  {| agree_car n := x; agree_is_valid n := True |}.
-Solve Obligations with done.
-Global Instance to_agree_ne n : Proper (dist n ==> dist n) to_agree.
-Proof. intros x1 x2 Hx; split; naive_solver eauto using @dist_le. Qed.
-Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _.
-Global Instance to_agree_inj n : Inj (dist n) (dist n) (to_agree).
-Proof. by intros x y [_ Hxy]; apply Hxy. Qed.
-Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ≡{n}≡ x.
-Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
-
-(** Internalized properties *)
-Lemma agree_equivI {M} a b : (to_agree a ≡ to_agree b)%I ≡ (a ≡ b : uPred M)%I.
-Proof.
-  uPred.unseal. do 2 split. by intros [? Hv]; apply (Hv n). apply: to_agree_ne.
-Qed.
-Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊑ (x ≡ y : uPred M).
-Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_inv. Qed.
-End agree.
-
-Arguments agreeC : clear implicits.
-Arguments agreeRA : clear implicits.
-
-Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
-  {| agree_car n := f (x n); agree_is_valid := agree_is_valid x |}.
-Solve Obligations with auto using agree_valid_S.
-Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
-Proof. by destruct x. Qed.
-Lemma agree_map_compose {A B C} (f : A → B) (g : B → C) (x : agree A) :
-  agree_map (g ∘ f) x = agree_map g (agree_map f x).
-Proof. done. Qed.
-
-Section agree_map.
-  Context {A B : cofeT} (f : A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}.
-  Instance agree_map_ne n : Proper (dist n ==> dist n) (agree_map f).
-  Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed.
-  Instance agree_map_proper : Proper ((≡) ==> (≡)) (agree_map f) := ne_proper _.
-  Lemma agree_map_ext (g : A → B) x :
-    (∀ x, f x ≡ g x) → agree_map f x ≡ agree_map g x.
-  Proof. by intros Hfg; split; simpl; intros; rewrite ?Hfg. Qed.
-  Global Instance agree_map_monotone : CMRAMonotone (agree_map f).
-  Proof.
-    split; first apply _.
-    - by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx].
-    - intros x y; rewrite !agree_included=> ->.
-      split; last done; split; simpl; last tauto.
-      by intros (?&?&Hxy); repeat split; intros;
-        try apply Hxy; try apply Hf; eauto using @agree_valid_le.
-  Qed.
-End agree_map.
-
-Definition agreeC_map {A B} (f : A -n> B) : agreeC A -n> agreeC B :=
-  CofeMor (agree_map f : agreeC A → agreeC B).
-Instance agreeC_map_ne A B n : Proper (dist n ==> dist n) (@agreeC_map A B).
-Proof.
-  intros f g Hfg x; split; simpl; intros; first done.
-  by apply dist_le with n; try apply Hfg.
-Qed.
-
-Program Definition agreeF : iFunctor :=
-  {| ifunctor_car := agreeRA; ifunctor_map := @agreeC_map |}.
-Solve Obligations with done.

algebra/auth.v

-From algebra Require Export excl.
-From algebra Require Import functor upred.
-Local Arguments valid _ _ !_ /.
-Local Arguments validN _ _ _ !_ /.
-
-Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
-Add Printing Constructor auth.
-Arguments Auth {_} _ _.
-Arguments authoritative {_} _.
-Arguments own {_} _.
-Notation "◯ a" := (Auth ExclUnit a) (at level 20).
-Notation "● a" := (Auth (Excl a) ∅) (at level 20).
-
-(* COFE *)
-Section cofe.
-Context {A : cofeT}.
-Implicit Types a : excl A.
-Implicit Types b : A.
-Implicit Types x y : auth A.
-
-Instance auth_equiv : Equiv (auth A) := λ x y,
-  authoritative x ≡ authoritative y ∧ own x ≡ own y.
-Instance auth_dist : Dist (auth A) := λ n x y,
-  authoritative x ≡{n}≡ authoritative y ∧ own x ≡{n}≡ own y.
-
-Global Instance Auth_ne : Proper (dist n ==> dist n ==> dist n) (@Auth A).
-Proof. by split. Qed.
-Global Instance Auth_proper : Proper ((≡) ==> (≡) ==> (≡)) (@Auth A).
-Proof. by split. Qed.
-Global Instance authoritative_ne: Proper (dist n ==> dist n) (@authoritative A).
-Proof. by destruct 1. Qed.
-Global Instance authoritative_proper : Proper ((≡) ==> (≡)) (@authoritative A).
-Proof. by destruct 1. Qed.
-Global Instance own_ne : Proper (dist n ==> dist n) (@own A).
-Proof. by destruct 1. Qed.
-Global Instance own_proper : Proper ((≡) ==> (≡)) (@own A).
-Proof. by destruct 1. Qed.
-
-Instance auth_compl : Compl (auth A) := λ c,
-  Auth (compl (chain_map authoritative c)) (compl (chain_map own c)).
-Definition auth_cofe_mixin : CofeMixin (auth A).
-Proof.
-  split.
-  - intros x y; unfold dist, auth_dist, equiv, auth_equiv.
-    rewrite !equiv_dist; naive_solver.
-  - intros n; split.
-    + by intros ?; split.
-    + by intros ?? [??]; split; symmetry.
-    + intros ??? [??] [??]; split; etrans; eauto.
-  - by intros ? [??] [??] [??]; split; apply dist_S.
-  - intros n c; split. apply (conv_compl n (chain_map authoritative c)).
-    apply (conv_compl n (chain_map own c)).
-Qed.
-Canonical Structure authC := CofeT auth_cofe_mixin.
-
-Global Instance Auth_timeless a b :
-  Timeless a → Timeless b → Timeless (Auth a b).
-Proof. by intros ?? [??] [??]; split; apply: timeless. Qed.
-Global Instance auth_discrete : Discrete A → Discrete authC.
-Proof. intros ? [??]; apply _. Qed.
-Global Instance auth_leibniz : LeibnizEquiv A → LeibnizEquiv (auth A).
-Proof. by intros ? [??] [??] [??]; f_equal/=; apply leibniz_equiv. Qed.
-End cofe.
-
-Arguments authC : clear implicits.
-
-(* CMRA *)
-Section cmra.
-Context {A : cmraT}.
-Implicit Types a b : A.
-Implicit Types x y : auth A.
-
-Global Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
-Instance auth_valid : Valid (auth A) := λ x,
-  match authoritative x with
-  | Excl a => own x ≼ a ∧ ✓ a
-  | ExclUnit => ✓ own x
-  | ExclBot => False
-  end.
-Global Arguments auth_valid !_ /.
-Instance auth_validN : ValidN (auth A) := λ n x,
-  match authoritative x with
-  | Excl a => own x ≼{n} a ∧ ✓{n} a
-  | ExclUnit => ✓{n} own x
-  | ExclBot => False
-  end.
-Global Arguments auth_validN _ !_ /.
-Instance auth_unit : Unit (auth A) := λ x,
-  Auth (unit (authoritative x)) (unit (own x)).
-Instance auth_op : Op (auth A) := λ x y,
-  Auth (authoritative x ⋅ authoritative y) (own x ⋅ own y).
-Instance auth_minus : Minus (auth A) := λ x y,
-  Auth (authoritative x ⩪ authoritative y) (own x ⩪ own y).
-
-Lemma auth_included (x y : auth A) :
-  x ≼ y ↔ authoritative x ≼ authoritative y ∧ own x ≼ own y.
-Proof.
-  split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
-  intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
-Qed.
-Lemma authoritative_validN n (x : auth A) : ✓{n} x → ✓{n} authoritative x.
-Proof. by destruct x as [[]]. Qed.
-Lemma own_validN n (x : auth A) : ✓{n} x → ✓{n} own x.
-Proof. destruct x as [[]]; naive_solver eauto using cmra_validN_includedN. Qed.
-
-Definition auth_cmra_mixin : CMRAMixin (auth A).
-Proof.
-  split.
-  - by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
-  - by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
-  - intros n [x a] [y b] [Hx Ha]; simpl in *;
-      destruct Hx; intros ?; cofe_subst; auto.
-  - by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
-      split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'.
-  - intros [[] ?]; rewrite /= ?cmra_included_includedN ?cmra_valid_validN;
-      naive_solver eauto using O.
-  - intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
-  - by split; simpl; rewrite assoc.
-  - by split; simpl; rewrite comm.
-  - by split; simpl; rewrite ?cmra_unit_l.
-  - by split; simpl; rewrite ?cmra_unit_idemp.
-  - intros ??; rewrite! auth_included; intros [??].
-    by split; simpl; apply cmra_unit_preserving.
-  - assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
-    { intros n a b1 b2 <-; apply cmra_includedN_l. }
-   intros n [[a1| |] b1] [[a2| |] b2];
-     naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
-  - by intros ??; rewrite auth_included;
-      intros [??]; split; simpl; apply cmra_op_minus.
-  - intros n x y1 y2 ? [??]; simpl in *.
-    destruct (cmra_extend n (authoritative x) (authoritative y1)
-      (authoritative y2)) as (ea&?&?&?); auto using authoritative_validN.
-    destruct (cmra_extend n (own x) (own y1) (own y2))
-      as (b&?&?&?); auto using own_validN.
-    by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
-Qed.
-Canonical Structure authRA : cmraT := CMRAT auth_cofe_mixin auth_cmra_mixin.
-Global Instance auth_cmra_discrete : CMRADiscrete A → CMRADiscrete authRA.
-Proof.
-  split; first apply _.
-  intros [[] ?]; by rewrite /= /cmra_valid /cmra_validN /=
-    -?cmra_discrete_included_iff -?cmra_discrete_valid_iff.
-Qed.
-
-(** Internalized properties *)
-Lemma auth_equivI {M} (x y : auth A) :
-  (x ≡ y)%I ≡ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M)%I.
-Proof. by uPred.unseal. Qed.
-Lemma auth_validI {M} (x : auth A) :
-  (✓ x)%I ≡ (match authoritative x with
-             | Excl a => (∃ b, a ≡ own x ⋅ b) ∧ ✓ a
-             | ExclUnit => ✓ own x
-             | ExclBot => False
-             end : uPred M)%I.
-Proof. uPred.unseal. by destruct x as [[]]. Qed.
-
-(** The notations ◯ and ● only work for CMRAs with an empty element. So, in
-what follows, we assume we have an empty element. *)
-Context `{Empty A, !CMRAIdentity A}.
-
-Global Instance auth_cmra_identity : CMRAIdentity authRA.
-Proof.
-  split; simpl.
-  - by apply (@cmra_empty_valid A _).
-  - by intros x; constructor; rewrite /= left_id.
-  - apply _.
-Qed.
-Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
-Proof. done. Qed.
-Lemma auth_both_op a b : Auth (Excl a) b ≡ ● a ⋅ ◯ b.
-Proof. by rewrite /op /auth_op /= left_id. Qed.
-
-Lemma auth_update a a' b b' :
-  (∀ n af, ✓{n} a → a ≡{n}≡ a' ⋅ af → b ≡{n}≡ b' ⋅ af ∧ ✓{n} b) →
-  ● a ⋅ ◯ a' ~~> ● b ⋅ ◯ b'.
-Proof.
-  move=> Hab n [[?| |] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
-  destruct (Hab n (bf1 ⋅ bf2)) as [Ha' ?]; auto.
-  { by rewrite Ha left_id assoc. }
-  split; [by rewrite Ha' left_id assoc; apply cmra_includedN_l|done].
-Qed.
-
-Lemma auth_local_update L `{!LocalUpdate Lv L} a a' :
-  Lv a → ✓ L a' →
-  ● a' ⋅ ◯ a ~~> ● L a' ⋅ ◯ L a.
-Proof.
-  intros. apply auth_update=>n af ? EQ; split; last by apply cmra_valid_validN.
-  by rewrite EQ (local_updateN L) // -EQ.
-Qed.
-
-Lemma auth_update_op_l a a' b :
-  ✓ (b ⋅ a) → ● a ⋅ ◯ a' ~~> ● (b ⋅ a) ⋅ ◯ (b ⋅ a').
-Proof. by intros; apply (auth_local_update _). Qed.
-Lemma auth_update_op_r a a' b :
-  ✓ (a ⋅ b) → ● a ⋅ ◯ a' ~~> ● (a ⋅ b) ⋅ ◯ (a' ⋅ b).
-Proof. rewrite -!(comm _ b); apply auth_update_op_l. Qed.
-
-(* This does not seem to follow from auth_local_update.
-   The trouble is that given ✓ (L a ⋅ a'), Lv a
-   we need ✓ (a ⋅ a'). I think this should hold for every local update,
-   but adding an extra axiom to local updates just for this is silly. *)
-Lemma auth_local_update_l L `{!LocalUpdate Lv L} a a' :
-  Lv a → ✓ (L a ⋅ a') →
-  ● (a ⋅ a') ⋅ ◯ a ~~> ● (L a ⋅ a') ⋅ ◯ L a.
-Proof.
-  intros. apply auth_update=>n af ? EQ; split; last by apply cmra_valid_validN.
-  by rewrite -(local_updateN L) // EQ -(local_updateN L) // -EQ.
-Qed.
-End cmra.
-
-Arguments authRA : clear implicits.
-
-(* Functor *)
-Definition auth_map {A B} (f : A → B) (x : auth A) : auth B :=
-  Auth (excl_map f (authoritative x)) (f (own x)).
-Lemma auth_map_id {A} (x : auth A) : auth_map id x = x.
-Proof. by destruct x; rewrite /auth_map excl_map_id. Qed.
-Lemma auth_map_compose {A B C} (f : A → B) (g : B → C) (x : auth A) :
-  auth_map (g ∘ f) x = auth_map g (auth_map f x).
-Proof. by destruct x; rewrite /auth_map excl_map_compose. Qed.
-Lemma auth_map_ext {A B : cofeT} (f g : A → B) x :
-  (∀ x, f x ≡ g x) → auth_map f x ≡ auth_map g x.
-Proof. constructor; simpl; auto using excl_map_ext. Qed.
-Instance auth_map_cmra_ne {A B : cofeT} n :
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
-Proof.
-  intros f g Hf [??] [??] [??]; split; [by apply excl_map_cmra_ne|by apply Hf].
-Qed.
-Instance auth_map_cmra_monotone {A B : cmraT} (f : A → B) :
-  CMRAMonotone f → CMRAMonotone (auth_map f).
-Proof.
-  split; try apply _.
-  - intros n [[a| |] b]; rewrite /= /cmra_validN /=; try
-      naive_solver eauto using includedN_preserving, validN_preserving.
-  - by intros [x a] [y b]; rewrite !auth_included /=;
-      intros [??]; split; simpl; apply: included_preserving.
-Qed.
-Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
-  CofeMor (auth_map f).
-Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
-Proof. intros f f' Hf [[a| |] b]; repeat constructor; apply Hf. Qed.
-
-Program Definition authF (Σ : iFunctor) : iFunctor := {|
-  ifunctor_car := authRA ∘ Σ; ifunctor_map A B := authC_map ∘ ifunctor_map Σ
-|}.
-Next Obligation.
-  by intros Σ A B n f g Hfg; apply authC_map_ne, ifunctor_map_ne.
-Qed.
-Next Obligation.
-  intros Σ A x. rewrite /= -{2}(auth_map_id x).
-  apply auth_map_ext=>y; apply ifunctor_map_id.
-Qed.
-Next Obligation.
-  intros Σ A B C f g x. rewrite /= -auth_map_compose.
-  apply auth_map_ext=>y; apply ifunctor_map_compose.
-Qed.

algebra/base.v

-From mathcomp Require Export ssreflect.
-From prelude Require Export prelude.
-Global Set Bullet Behavior "Strict Subproofs".
-Global Open Scope general_if_scope.
-Ltac done := prelude.tactics.done.
\ No newline at end of file

algebra/cmra_big_op.v

-From algebra Require Export cmra.
-From prelude Require Import gmap.
-
-Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
-  match xs with [] => ∅ | x :: xs => x ⋅ big_op xs end.
-Arguments big_op _ _ !_ /.
-Instance: Params (@big_op) 2.
-Definition big_opM `{Countable K} {A : cmraT} `{Empty A} (m : gmap K A) : A :=
-  big_op (snd <$> map_to_list m).
-Instance: Params (@big_opM) 5.
-
-(** * Properties about big ops *)
-Section big_op.
-Context `{CMRAIdentity A}.
-
-(** * Big ops *)
-Lemma big_op_nil : big_op (@nil A) = ∅.
-Proof. done. Qed.
-Lemma big_op_cons x xs : big_op (x :: xs) = x ⋅ big_op xs.
-Proof. done. Qed.
-Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) big_op.
-Proof.
-  induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
-  - by rewrite IH.
-  - by rewrite !assoc (comm _ x).
-  - by trans (big_op xs2).
-Qed.
-Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op.
-Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
-Lemma big_op_app xs ys : big_op (xs ++ ys) ≡ big_op xs ⋅ big_op ys.
-Proof.
-  induction xs as [|x xs IH]; simpl; first by rewrite ?left_id.
-  by rewrite IH assoc.
-Qed.
-Lemma big_op_contains xs ys : xs `contains` ys → big_op xs ≼ big_op ys.
-Proof.
-  intros [xs' ->]%contains_Permutation.
-  rewrite big_op_app; apply cmra_included_l.
-Qed.
-Lemma big_op_delete xs i x :
-  xs !! i = Some x → x ⋅ big_op (delete i xs) ≡ big_op xs.
-Proof. by intros; rewrite {2}(delete_Permutation xs i x). Qed.
-
-Context `{Countable K}.
-Implicit Types m : gmap K A.
-Lemma big_opM_empty : big_opM (∅ : gmap K A) ≡ ∅.
-Proof. unfold big_opM. by rewrite map_to_list_empty. Qed.
-Lemma big_opM_insert m i x :
-  m !! i = None → big_opM (<[i:=x]> m) ≡ x ⋅ big_opM m.
-Proof. intros ?; by rewrite /big_opM map_to_list_insert. Qed.
-Lemma big_opM_delete m i x :
-  m !! i = Some x → x ⋅ big_opM (delete i m) ≡ big_opM m.
-Proof.
-  intros. by rewrite -{2}(insert_delete m i x) // big_opM_insert ?lookup_delete.
-Qed.
-Lemma big_opM_singleton i x : big_opM ({[i := x]} : gmap K A) ≡ x.
-Proof.
-  rewrite -insert_empty big_opM_insert /=; last auto using lookup_empty.
-  by rewrite big_opM_empty right_id.
-Qed.
-Global Instance big_opM_proper : Proper ((≡) ==> (≡)) (big_opM : gmap K A → _).
-Proof.
-  intros m1; induction m1 as [|i x m1 ? IH] using map_ind.
-  { by intros m2; rewrite (symmetry_iff (≡)) map_equiv_empty; intros ->. }
-  intros m2 Hm2; rewrite big_opM_insert //.
-  rewrite (IH (delete i m2)); last by rewrite -Hm2 delete_insert.
-  destruct (map_equiv_lookup (<[i:=x]> m1) m2 i x)
-    as (y&?&Hxy); auto using lookup_insert.
-  rewrite Hxy -big_opM_insert; last auto using lookup_delete.
-  by rewrite insert_delete.
-Qed.
-Lemma big_opM_lookup_valid n m i x : ✓{n} big_opM m → m !! i = Some x → ✓{n} x.
-Proof.
-  intros Hm ?; revert Hm; rewrite -(big_opM_delete _ i x) //.
-  apply cmra_validN_op_l.
-Qed.
-End big_op.

algebra/cmra_tactics.v

-From algebra Require Export cmra.
-From algebra Require Import cmra_big_op.
-
-(** * Simple solver for validity and inclusion by reflection *)
-Module ra_reflection. Section ra_reflection.
-  Context `{CMRAIdentity A}.
-
-  Inductive expr :=
-    | EVar : nat → expr
-    | EEmpty : expr
-    | EOp : expr → expr → expr.
-  Fixpoint eval (Σ : list A) (e : expr) : A :=
-    match e with
-    | EVar n => from_option ∅ (Σ !! n)
-    | EEmpty => ∅
-    | EOp e1 e2 => eval Σ e1 ⋅ eval Σ e2
-    end.
-  Fixpoint flatten (e : expr) : list nat :=
-    match e with
-    | EVar n => [n]
-    | EEmpty => []
-    | EOp e1 e2 => flatten e1 ++ flatten e2
-    end.
-  Lemma eval_flatten Σ e :
-    eval Σ e ≡ big_op ((λ n, from_option ∅ (Σ !! n)) <$> flatten e).
-  Proof.
-    by induction e as [| |e1 IH1 e2 IH2];
-      rewrite /= ?right_id ?fmap_app ?big_op_app ?IH1 ?IH2.
-  Qed.
-  Lemma flatten_correct Σ e1 e2 :
-    flatten e1 `contains` flatten e2 → eval Σ e1 ≼ eval Σ e2.
-  Proof.
-    by intros He; rewrite !eval_flatten; apply big_op_contains; rewrite ->He.
-  Qed.
-
-  Class Quote (Σ1 Σ2 : list A) (l : A) (e : expr) := {}.
-  Global Instance quote_empty: Quote E1 E1 ∅ EEmpty.
-  Global Instance quote_var Σ1 Σ2 e i:
-    rlist.QuoteLookup Σ1 Σ2 e i → Quote Σ1 Σ2 e (EVar i) | 1000.
-  Global Instance quote_app Σ1 Σ2 Σ3 x1 x2 e1 e2 :
-    Quote Σ1 Σ2 x1 e1 → Quote Σ2 Σ3 x2 e2 → Quote Σ1 Σ3 (x1 ⋅ x2) (EOp e1 e2).
-  End ra_reflection.
-
-  Ltac quote :=
-    match goal with
-    | |- @included _ _ _ ?x ?y =>
-      lazymatch type of (_ : Quote [] _ x _) with Quote _ ?Σ2 _ ?e1 =>
-      lazymatch type of (_ : Quote Σ2 _ y _) with Quote _ ?Σ3 _ ?e2 =>
-        change (eval Σ3 e1 ≼ eval Σ3 e2)
-      end end
-    end.
-End ra_reflection.
-
-Ltac solve_included :=
-  ra_reflection.quote;
-  apply ra_reflection.flatten_correct, (bool_decide_unpack _);
-  vm_compute; apply I.
-
-Ltac solve_validN :=
-  match goal with
-  | H : ✓{?n} ?y |- ✓{?n'} ?x =>
-     let Hn := fresh in let Hx := fresh in
-     assert (n' ≤ n) as Hn by omega;
-     assert (x ≼ y) as Hx by solve_included;
-     eapply cmra_validN_le, Hn; eapply cmra_validN_included, Hx; apply H
-  end.