.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
 \#*\#
+.\#*
 *~
 *.bak
+.coqdeps.d
 .coq-native/
-Makefile
+*.crashcoqide
+.env
+builddep/
+_CoqProject.*
+Makefile.coq
+Makefile.coq.conf
+.Makefile.coq.d
+Makefile.package.*
+.Makefile.package.*
+_opam
+_build
+*.install

.gitlab-ci.yml

+image: ralfjung/opam-ci:opam2
+
+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:
+  - fp
+  script:
+  - git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
+  - ci/buildjob
+  cache:
+    key: "$CI_JOB_NAME"
+    paths:
+    - _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

+# Default target
+all: Makefile.coq
+	+@$(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
+	@# 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
+
+# Backwards compatibility target
+build-dep: builddep
+.PHONY: build-dep
+
+# 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
- - Autosubst 1.4
-
-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 commands to build the full development:
-
-  ./configure
-  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
-modures/option.v
-modures/cmra.v
-modures/cmra_big_op.v
-modures/cmra_tactics.v
-modures/sts.v
-modures/auth.v
-modures/fin_maps.v
-modures/logic.v
-modures/cofe.v
-modures/base.v
-modures/dra.v
-modures/cofe_solver.v
-modures/agree.v
-modures/excl.v
-iris/model.v
-iris/adequacy.v
-iris/hoare_lifting.v
-iris/lifting.v
-iris/namespace.v
-iris/viewshifts.v
-iris/wsat.v
-iris/ownership.v
-iris/weakestpre.v
-iris/pviewshifts.v
-iris/resources.v
-iris/hoare.v
-iris/language.v
-iris/functor.v
-iris/tests.v
-barrier/heap_lang.v
-barrier/heap_lang_tactics.v
-barrier/lifting.v
-barrier/sugar.v
-barrier/tests.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/stepindex.v
+iris/algebra/stepindex_finite.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

barrier/heap_lang.v

-Require Export Autosubst.Autosubst.
-Require Export iris.language.
-Require Import prelude.gmap.
-
-Module heap_lang.
-(** Expressions and vals. *)
-Definition loc := positive. (* Really, any countable type. *)
-
-Inductive expr :=
-  (* Base lambda calculus *)
-  | Var (x : var)
-  | Rec (e : {bind 2 of expr}) (* These are recursive lambdas.
-                                  The *inner* binder is the recursive call! *)
-  | App (e1 e2 : expr)
-  (* Natural numbers *)
-  | LitNat (n : nat)
-  | Plus (e1 e2 : expr)
-  | Le (e1 e2 : expr)
-  (* Unit *)
-  | LitUnit
-  (* Products *)
-  | Pair (e1 e2 : expr)
-  | Fst (e : expr)
-  | Snd (e : expr)
-  (* Sums *)
-  | InjL (e : expr)
-  | InjR (e : expr)
-  | Case (e0 : expr) (e1 : {bind expr}) (e2 : {bind expr})
-  (* Concurrency *)
-  | Fork (e : expr)
-  (* Heap *)
-  | Loc (l : loc)
-  | Alloc (e : expr)
-  | Load (e : expr)
-  | Store (e1 : expr) (e2 : expr)
-  | Cas (e0 : expr) (e1 : expr) (e2 : expr).
-
-Instance Ids_expr : Ids expr. derive. Defined.
-Instance Rename_expr : Rename expr. derive. Defined.
-Instance Subst_expr : Subst expr. derive. Defined.
-Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed.
-
-(* This sugar is used by primitive reduction riles (<=, CAS) and hence
-defined here. *)
-Notation LitTrue := (InjL LitUnit).
-Notation LitFalse := (InjR LitUnit).
-
-Inductive val :=
-  | RecV (e : {bind 2 of expr}) (* These are recursive lambdas.
-                                   The *inner* binder is the recursive call! *)
-  | LitNatV (n : nat)
-  | LitUnitV
-  | PairV (v1 v2 : val)
-  | InjLV (v : val)
-  | InjRV (v : val)
-  | LocV (l : loc).
-
-Definition LitTrueV := InjLV LitUnitV.
-Definition LitFalseV := InjRV LitUnitV.
-
-Fixpoint of_val (v : val) : expr :=
-  match v with
-  | RecV e => Rec e
-  | LitNatV n => LitNat n
-  | LitUnitV => LitUnit
-  | PairV v1 v2 => Pair (of_val v1) (of_val v2)
-  | InjLV v => InjL (of_val v)
-  | InjRV v => InjR (of_val v)
-  | LocV l => Loc l
-  end.
-Fixpoint to_val (e : expr) : option val :=
-  match e with
-  | Rec e => Some (RecV e)
-  | LitNat n => Some (LitNatV n)
-  | LitUnit => Some LitUnitV
-  | Pair e1 e2 => v1 ← to_val e1; v2 ← to_val e2; Some (PairV v1 v2)
-  | InjL e => InjLV <$> to_val e
-  | InjR e => InjRV <$> to_val e
-  | Loc l => Some (LocV l)
-  | _ => None
-  end.
-
-(** The state: heaps of vals. *)
-Definition state := gmap loc val.
-
-(** Evaluation contexts *)
-Inductive ectx_item :=
-  | AppLCtx (e2 : expr)
-  | AppRCtx (v1 : val)
-  | PlusLCtx (e2 : expr)
-  | PlusRCtx (v1 : val)
-  | LeLCtx (e2 : expr)
-  | LeRCtx (v1 : val)
-  | PairLCtx (e2 : expr)
-  | PairRCtx (v1 : val)
-  | FstCtx
-  | SndCtx
-  | InjLCtx
-  | InjRCtx
-  | CaseCtx (e1 : {bind expr}) (e2 : {bind expr})
-  | AllocCtx
-  | LoadCtx
-  | StoreLCtx (e2 : expr)
-  | StoreRCtx (v1 : val)
-  | CasLCtx (e1 : expr)  (e2 : expr)
-  | CasMCtx (v0 : val) (e2 : expr)
-  | CasRCtx (v0 : val) (v1 : val).
-
-Notation ectx := (list ectx_item).
-
-Implicit Types Ki : ectx_item.
-Implicit Types K : ectx.
-
-Definition ectx_item_fill (Ki : ectx_item) (e : expr) : expr :=
-  match Ki with
-  | AppLCtx e2 => App e e2
-  | AppRCtx v1 => App (of_val v1) e
-  | PlusLCtx e2 => Plus e e2
-  | PlusRCtx v1 => Plus (of_val v1) e
-  | LeLCtx e2 => Le e e2
-  | LeRCtx v1 => Le (of_val v1) e
-  | PairLCtx e2 => Pair e e2
-  | PairRCtx v1 => Pair (of_val v1) e
-  | FstCtx => Fst e
-  | SndCtx => Snd e
-  | InjLCtx => InjL e
-  | InjRCtx => InjR e
-  | CaseCtx e1 e2 => Case e e1 e2
-  | AllocCtx => Alloc e
-  | LoadCtx => Load e
-  | StoreLCtx e2 => Store e e2
-  | StoreRCtx v1 => Store (of_val v1) e
-  | CasLCtx e1 e2 => Cas e e1 e2
-  | CasMCtx v0 e2 => Cas (of_val v0) e e2
-  | CasRCtx v0 v1 => Cas (of_val v0) (of_val v1) e
-  end.
-
-Fixpoint fill K e :=
-  (* FIXME RJ: This really is fold_left, but if I use that all automation breaks:
-       fold_left (fun e Ki => ectx_item_fill Ki e).
-     Or maybe we even have a combinator somewhere to swap the arguments? *)
-  match K with [] => e | Ki :: K => ectx_item_fill Ki (fill K e) end.
-
-(** The stepping relation *)
-Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
-  | BetaS e1 e2 v2 σ :
-     to_val e2 = Some v2 →
-     head_step (App (Rec e1) e2) σ e1.[(Rec e1),e2/] σ None
-  | PlusS n1 n2 σ:
-     head_step (Plus (LitNat n1) (LitNat n2)) σ (LitNat (n1 + n2)) σ None
-  | LeTrueS n1 n2 σ :
-     n1 ≤ n2 →
-     head_step (Le (LitNat n1) (LitNat n2)) σ LitTrue σ None
-  | LeFalseS n1 n2 σ :
-     n1 > n2 →
-     head_step (Le (LitNat n1) (LitNat n2)) σ LitFalse σ None
-  | FstS e1 v1 e2 v2 σ :
-     to_val e1 = Some v1 → to_val e2 = Some v2 →
-     head_step (Fst (Pair e1 e2)) σ e1 σ None
-  | SndS e1 v1 e2 v2 σ :
-     to_val e1 = Some v1 → to_val e2 = Some v2 →
-     head_step (Snd (Pair e1 e2)) σ e2 σ None
-  | CaseLS e0 v0 e1 e2 σ :
-     to_val e0 = Some v0 →
-     head_step (Case (InjL e0) e1 e2) σ e1.[e0/] σ None
-  | CaseRS e0 v0 e1 e2 σ :
-     to_val e0 = Some v0 →
-     head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ None
-  | ForkS e σ:
-     head_step (Fork e) σ LitUnit σ (Some e)
-  | AllocS e v σ l :
-     to_val e = Some v → σ !! l = None →
-     head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None
-  | LoadS l v σ :
-     σ !! l = Some v →
-     head_step (Load (Loc l)) σ (of_val v) σ None
-  | StoreS l e v σ :
-     to_val e = Some v → is_Some (σ !! l) →
-     head_step (Store (Loc l) e) σ LitUnit (<[l:=v]>σ) None
-  | CasFailS l e1 v1 e2 v2 vl σ :
-     to_val e1 = Some v1 → to_val e2 = Some v2 →
-     σ !! l = Some vl → vl ≠ v1 →
-     head_step (Cas (Loc l) e1 e2) σ LitFalse σ None
-  | CasSucS l e1 v1 e2 v2 σ :
-     to_val e1 = Some v1 → to_val e2 = Some v2 →
-     σ !! l = Some v1 →
-     head_step (Cas (Loc l) e1 e2) σ LitTrue (<[l:=v2]>σ) None.
-
-(** Atomic expressions *)
-Definition atomic (e: expr) :=
-  match e with
-  | Alloc e => is_Some (to_val e)
-  | Load e => is_Some (to_val e)
-  | Store e1 e2 => is_Some (to_val e1) ∧ is_Some (to_val e2)
-  | Cas e0 e1 e2 => is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2)
-  | _ => False
-  end.
-
-(** Close reduction under evaluation contexts.
-We could potentially make this a generic construction. *)
-Inductive prim_step
-    (e1 : expr) (σ1 : state) (e2 : expr) (σ2: state) (ef: option expr) : Prop :=
-  Ectx_step (K : ectx) e1' e2' :
-    e1 = fill K e1' → e2 = fill K e2' →
-    head_step e1' σ1 e2' σ2 ef → prim_step e1 σ1 e2 σ2 ef.
-
-(** Basic properties about the language *)
-Lemma to_of_val v : to_val (of_val v) = Some v.
-Proof. by induction v; simplify_option_equality. Qed.
-
-Lemma of_to_val e v : to_val e = Some v → of_val v = e.
-Proof.
-  revert v; induction e; intros; simplify_option_equality; auto with f_equal.
-Qed.
-
-Instance: Injective (=) (=) of_val.
-Proof. by intros ?? Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.
-
-Instance ectx_item_fill_inj Ki : Injective (=) (=) (ectx_item_fill Ki).
-Proof. destruct Ki; intros ???; simplify_equality'; auto with f_equal. Qed.
-
-Instance ectx_fill_inj K : Injective (=) (=) (fill K).
-Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
-
-Lemma fill_app K1 K2 e : fill (K1 ++ K2) e = fill K1 (fill K2 e).
-Proof. revert e; induction K1; simpl; auto with f_equal. Qed.
-
-Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e).
-Proof.
-  intros [v' Hv']; revert v' Hv'.
-  induction K as [|[]]; intros; simplify_option_equality; eauto.
-Qed.
-
-Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
-Proof. rewrite !eq_None_not_Some; eauto using fill_val. Qed.
-
-Lemma values_head_stuck e1 σ1 e2 σ2 ef :
-  head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
-Proof. destruct 1; naive_solver. Qed.
-
-Lemma values_stuck e1 σ1 e2 σ2 ef : prim_step e1 σ1 e2 σ2 ef → to_val e1 = None.
-Proof. intros [??? -> -> ?]; eauto using fill_not_val, values_head_stuck. Qed.
-
-Lemma atomic_not_val e : atomic e → to_val e = None.
-Proof. destruct e; naive_solver. Qed.
-
-Lemma atomic_fill K e : atomic (fill K e) → to_val e = None → K = [].
-Proof.
-  rewrite eq_None_not_Some.
-  destruct K as [|[]]; naive_solver eauto using fill_val.
-Qed.
-
-Lemma atomic_head_step e1 σ1 e2 σ2 ef :
-  atomic e1 → head_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
-Proof. destruct 2; simpl; rewrite ?to_of_val; naive_solver. Qed.
-
-Lemma atomic_step e1 σ1 e2 σ2 ef :
-  atomic e1 → prim_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
-Proof.
-  intros Hatomic [K e1' e2' -> -> Hstep].
-  assert (K = []) as -> by eauto 10 using atomic_fill, values_head_stuck.
-  naive_solver eauto using atomic_head_step.
-Qed.
-
-Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
-  head_step (ectx_item_fill Ki e) σ1 e2 σ2 ef → is_Some (to_val e).
-Proof. destruct Ki; inversion_clear 1; simplify_option_equality; eauto. Qed.
-
-Lemma fill_item_inj Ki1 Ki2 e1 e2 :
-  to_val e1 = None → to_val e2 = None →
-  ectx_item_fill Ki1 e1 = ectx_item_fill Ki2 e2 → Ki1 = Ki2.
-Proof.
-  destruct Ki1, Ki2; intros; try discriminate; simplify_equality';
-    repeat match goal with
-    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
-    end; auto.
-Qed.
-
-(* When something does a step, and another decomposition of the same expression
-has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
-other words, [e] also contains the reducible expression *)
-Lemma step_by_val K K' e1 e1' σ1 e2 σ2 ef :
-  fill K e1 = fill K' e1' → to_val e1 = None → head_step e1' σ1 e2 σ2 ef →
-  K `prefix_of` K'.
-Proof.
-  intros Hfill Hred Hnval; revert K' Hfill.
-  induction K as [|Ki K IH]; simpl; intros K' Hfill; auto using prefix_of_nil.
-  destruct K' as [|Ki' K']; simplify_equality'.
-  { destruct (proj1 (eq_None_not_Some (to_val (fill K e1))));
-      eauto using fill_not_val, head_ctx_step_val. }
-  cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
-  eauto using fill_item_inj, values_head_stuck, fill_not_val.
-Qed.
-
-Lemma alloc_fresh e v σ :
-  let l := fresh (dom _ σ) in
-  to_val e = Some v → head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None.
-Proof.
-  by intros; apply AllocS, (not_elem_of_dom (D:=gset positive)), is_fresh.
-Qed.
-
-End heap_lang.
-
-(** Language *)
-Program Canonical Structure heap_lang : language := {|
-  expr := heap_lang.expr; val := heap_lang.val; state := heap_lang.state;
-  of_val := heap_lang.of_val; to_val := heap_lang.to_val;
-  atomic := heap_lang.atomic; prim_step := heap_lang.prim_step;
-|}.
-Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
-  heap_lang.values_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step.
-Import heap_lang.
-
-Global Instance heap_lang_ctx K :
-  LanguageCtx heap_lang (heap_lang.fill K).
-Proof.
-  split.
-  * eauto using heap_lang.fill_not_val.
-  * intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
-    by exists (K ++ K') e1' e2'; rewrite ?heap_lang.fill_app ?Heq1 ?Heq2.
-  * intros e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
-    destruct (heap_lang.step_by_val
-      K K'' e1 e1'' σ1 e2'' σ2 ef) as [K' ->]; eauto.
-    rewrite heap_lang.fill_app in Heq1; apply (injective _) in Heq1.
-    exists (fill K' e2''); rewrite heap_lang.fill_app; split; auto.
-    econstructor; eauto.
-Qed.

barrier/heap_lang_tactics.v

-Require Export barrier.heap_lang.
-Require Import prelude.fin_maps.
-Import heap_lang.
-
-Ltac inv_step :=
-  repeat match goal with
-  | _ => progress simplify_map_equality' (* simplify memory stuff *)
-  | H : to_val _ = Some _ |- _ => apply of_to_val in H
-  | H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
-  | H : prim_step _ _ _ _ _ |- _ => destruct H; subst
-  | H : _ = fill ?K ?e |- _ =>
-     destruct K as [|[]];
-     simpl in H; first [subst e|discriminate H|injection' H]
-     (* ensure that we make progress for each subgoal *)
-  | H : head_step ?e _ _ _ _, Hv : of_val ?v = fill ?K ?e |- _ =>
-    apply values_head_stuck, (fill_not_val K) in H;
-    by rewrite -Hv to_of_val in H (* maybe use a helper lemma here? *)
-  | H : head_step ?e _ _ _ _ |- _ =>
-     try (is_var e; fail 1); (* inversion yields many goals if e is a variable
-     and can thus better be avoided. *)
-     inversion H; subst; clear H
-  end.
-
-Ltac reshape_expr e tac :=
-  let rec go K e :=
-  match e with
-  | _ => tac (reverse K) e
-  | App ?e1 ?e2 =>
-     lazymatch e1 with
-     | of_val ?v1 => go (AppRCtx v1 :: K) e2 | _ => go (AppLCtx e2 :: K) e1
-     end
-  | Plus ?e1 ?e2 =>
-     lazymatch e1 with
-     | of_val ?v1 => go (PlusRCtx v1 :: K) e2 | _ => go (PlusLCtx e2 :: K) e1
-     end
-  | Le ?e1 ?e2 =>
-     lazymatch e1 with
-     | of_val ?v1 => go (LeRCtx v1 :: K) e2 | _ => go (LeLCtx e2 :: K) e1
-     end
-  | Pair ?e1 ?e2 =>
-     lazymatch e1 with
-     | of_val ?v1 => go (PairRCtx v1 :: K) e2 | _ => go (PairLCtx e2 :: K) e1
-     end
-  | Fst ?e => go (FstCtx :: K) e
-  | Snd ?e => go (SndCtx :: K) e
-  | InjL ?e => go (InjLCtx :: K) e
-  | InjR ?e => go (InjRCtx :: K) e
-  | Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
-  | Alloc ?e => go (AllocCtx :: K) e
-  | Load ?e => go (LoadCtx :: K) e
-  | Store ?e1 ?e2 => go (StoreLCtx e2 :: K) e1 || go (StoreRCtx e1 :: K) e2
-  | Cas ?e0 ?e1 ?e2 =>
-     lazymatch e0 with
-     | of_val ?v0 =>
-        lazymatch e1 with
-        | of_val ?v1 => go (CasRCtx v0 v1 :: K) e2
-        | _ => go (CasMCtx v0 e2 :: K) e1
-        end
-     | _ => go (CasLCtx e1 e2 :: K) e0
-     end
-  end in go (@nil ectx_item) e.
-
-Ltac do_step tac :=
-  try match goal with |- language.reducible _ _ => eexists _, _, _ end;
-  simpl;
-  match goal with
-  | |- prim_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
-     reshape_expr e1 ltac:(fun K e1' =>
-       eapply Ectx_step with K e1' _); [reflexivity|reflexivity|];
-       first [apply alloc_fresh|econstructor];
-       rewrite ?to_of_val; tac; fail
-  end.

barrier/lifting.v

-Require Import prelude.gmap iris.lifting.
-Require Export iris.weakestpre barrier.heap_lang_tactics.
-Import uPred.
-Import heap_lang.
-Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
-
-Section lifting.
-Context {Σ : iFunctor}.
-Implicit Types P : iProp heap_lang Σ.
-Implicit Types Q : val → iProp heap_lang Σ.
-Implicit Types K : ectx.
-
-(** Bind. *)
-Lemma wp_bind {E e} K Q :
-  wp E e (λ v, wp E (fill K (of_val v)) Q) ⊑ wp E (fill K e) Q.
-Proof. apply wp_bind. Qed.
-
-(** Base axioms for core primitives of the language: Stateful reductions. *)
-Lemma wp_alloc_pst E σ e v Q :
-  to_val e = Some v →
-  (ownP σ ★ ▷ (∀ l, ■(σ !! l = None) ∧ ownP (<[l:=v]>σ) -★ Q (LocV l)))
-       ⊑ wp E (Alloc e) Q.
-Proof.
-  intros.
-  (* FIXME RJ: ssreflect rewrite does not work. *)
-  rewrite <-(wp_lift_atomic_step (Alloc e)
-    (λ v' σ', ∃ l, v' = LocV l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None) σ)=> //;
-    last first.
-  { (* TODO RJ: Somehow automation used to kill all this...?? *)
-    intros. inv_step. eexists; split_ands; try done; [].
-    eexists; done. }
-  apply sep_mono, later_mono; first done.
-  apply forall_intro=>e2; apply forall_intro=>σ2.
-  apply wand_intro_l.
-  rewrite always_and_sep_l' -associative -always_and_sep_l'.
-  apply const_elim_l=>-[l [-> [-> ?]]].
-  rewrite (forall_elim l) const_equiv //.
-  by rewrite left_id wand_elim_r.
-Qed.
-
-Lemma wp_load_pst E σ l v Q :
-  σ !! l = Some v →
-  (ownP σ ★ ▷ (ownP σ -★ Q v)) ⊑ wp E (Load (Loc l)) Q.
-Proof.
-  intros; rewrite -(wp_lift_atomic_det_step σ v σ) //;
-    last (by intros; inv_step; eauto).
-Qed.
-
-Lemma wp_store_pst E σ l e v v' Q :
-  to_val e = Some v → σ !! l = Some v' →
-  (ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Q LitUnitV)) ⊑ wp E (Store (Loc l) e) Q.
-Proof.
-  intros.
-  rewrite -(wp_lift_atomic_det_step σ LitUnitV (<[l:=v]>σ)) //;
-    last by intros; inv_step; eauto.
-Qed.
-
-Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
-  to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 →
-  (ownP σ ★ ▷ (ownP σ -★ Q LitFalseV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
-Proof.
-  intros; rewrite -(wp_lift_atomic_det_step σ LitFalseV σ) //;
-    last by intros; inv_step; eauto.
-Qed.
-
-Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
-  to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
-  (ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Q LitTrueV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
-Proof.
-  intros.
-  rewrite -(wp_lift_atomic_det_step σ LitTrueV (<[l:=v2]>σ)) //;
-    last by intros; inv_step; eauto.
-Qed.
-
-(** Base axioms for core primitives of the language: Stateless reductions *)
-Lemma wp_fork E e :
-  ▷ wp (Σ:=Σ) coPset_all e (λ _, True) ⊑ wp E (Fork e) (λ v, ■(v = LitUnitV)).
-Proof.
-  rewrite -(wp_lift_pure_step E (λ e' ef, e' = LitUnit ∧ ef = Some e)) //=;
-    last by intros; inv_step; eauto.
-  apply later_mono, forall_intro=>e2; apply forall_intro=>ef.
-  apply impl_intro_l, const_elim_l=>-[-> ->] /=.
-  apply sep_intro_True_l; last done.
-  by rewrite -wp_value' //; apply const_intro.
-Qed.
-
-Lemma wp_rec E ef e v Q :
-  to_val e = Some v →
-  ▷ wp E ef.[Rec ef, e /] Q ⊑ wp E (App (Rec ef) e) Q.
-Proof.
-  intros; rewrite -(wp_lift_pure_det_step (App _ _) ef.[Rec ef, e /]) //=;
-    last by intros; inv_step; eauto.
-Qed.
-
-Lemma wp_plus E n1 n2 Q :
-  ▷ Q (LitNatV (n1 + n2)) ⊑ wp E (Plus (LitNat n1) (LitNat n2)) Q.
-Proof.
-  rewrite -(wp_lift_pure_det_step (Plus _ _) (LitNat (n1 + n2))) //=;
-    last by intros; inv_step; eauto.
-  by rewrite -wp_value'.
-Qed.
-
-Lemma wp_le_true E n1 n2 Q :
-  n1 ≤ n2 →
-  ▷ Q LitTrueV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
-Proof.
-  intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitTrue) //=;
-    last by intros; inv_step; eauto with lia.
-  by rewrite -wp_value'.
-Qed.
-
-Lemma wp_le_false E n1 n2 Q :
-  n1 > n2 →
-  ▷ Q LitFalseV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
-Proof.
-  intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitFalse) //=;
-    last by intros; inv_step; eauto with lia.
-  by rewrite -wp_value'.
-Qed.
-
-Lemma wp_fst E e1 v1 e2 v2 Q :
-  to_val e1 = Some v1 → to_val e2 = Some v2 →
-  ▷Q v1 ⊑ wp E (Fst (Pair e1 e2)) Q.
-Proof.
-  intros; rewrite -(wp_lift_pure_det_step (Fst _) e1) //=;
-    last by intros; inv_step; eauto.
-  by rewrite -wp_value'.
-Qed.
-
-Lemma wp_snd E e1 v1 e2 v2 Q :
-  to_val e1 = Some v1 → to_val e2 = Some v2 →
-  ▷ Q v2 ⊑ wp E (Snd (Pair e1 e2)) Q.
-Proof.
-  intros; rewrite -(wp_lift_pure_det_step (Snd _) e2) //=;
-    last by intros; inv_step; eauto.
-  by rewrite -wp_value'.
-Qed.
-
-Lemma wp_case_inl E e0 v0 e1 e2 Q :
-  to_val e0 = Some v0 →
-  ▷ wp E e1.[e0/] Q ⊑ wp E (Case (InjL e0) e1 e2) Q.
-Proof.
-  intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e1.[e0/]) //=;
-    last by intros; inv_step; eauto.
-Qed.
-
-Lemma wp_case_inr E e0 v0 e1 e2 Q :
-  to_val e0 = Some v0 →
-  ▷ wp E e2.[e0/] Q ⊑ wp E (Case (InjR e0) e1 e2) Q.
-Proof.
-  intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e2.[e0/]) //=;
-    last by intros; inv_step; eauto.
-Qed.
-
-(** Some derived stateless axioms *)
-Lemma wp_le E n1 n2 P Q :
-  (n1 ≤ n2 → P ⊑ ▷ Q LitTrueV) →
-  (n1 > n2 → P ⊑ ▷ Q LitFalseV) →
-  P ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
-Proof.
-  intros; destruct (decide (n1 ≤ n2)).
-  * rewrite -wp_le_true; auto.
-  * rewrite -wp_le_false; auto with lia.
-Qed.
-
-End lifting.

barrier/sugar.v

-Require Export barrier.heap_lang barrier.lifting.
-Import uPred.
-Import heap_lang.
-
-(** Define some syntactic sugar. LitTrue and LitFalse are defined in heap_lang.v. *)
-Definition Lam (e : {bind expr}) := Rec e.[ren(+1)].
-Definition Let (e1 : expr) (e2: {bind expr}) := App (Lam e2) e1.
-Definition Seq (e1 e2 : expr) := Let e1 e2.[ren(+1)].
-Definition If (e0 e1 e2 : expr) := Case e0 e1.[ren(+1)] e2.[ren(+1)].
-Definition Lt e1 e2 := Le (Plus e1 $ LitNat 1) e2.
-Definition Eq e1 e2 :=
-  Let e1 (Let e2.[ren(+1)]
-         (If (Le (Var 0) (Var 1)) (Le (Var 1) (Var 0)) LitFalse)).
-
-Definition LamV (e : {bind expr}) := RecV e.[ren(+1)].
-
-Definition LetCtx (e2 : {bind expr}) := AppRCtx (LamV e2).
-Definition SeqCtx (e2 : expr) := LetCtx (e2.[ren(+1)]).
-
-Section suger.
-Context {Σ : iFunctor}.
-Implicit Types P : iProp heap_lang Σ.
-Implicit Types Q : val → iProp heap_lang Σ.
-
-(** Proof rules for the sugar *)
-Lemma wp_lam E ef e v Q :
-  to_val e = Some v → ▷ wp E ef.[e/] Q ⊑ wp E (App (Lam ef) e) Q.
-Proof.
-  intros Hv. rewrite -wp_rec; last eassumption.
-  (* RJ: This pulls in functional extensionality. If that bothers us, we have
-     to talk to the Autosubst guys. *)
-  by asimpl.
-Qed.
-Lemma wp_let E e1 e2 Q :
-  wp E e1 (λ v, ▷wp E (e2.[of_val v/]) Q) ⊑ wp E (Let e1 e2) Q.
-Proof.
-  rewrite -(wp_bind [LetCtx e2]). apply wp_mono=>v.
-  by rewrite -wp_lam //= to_of_val.
-Qed.
-Lemma wp_if_true E e1 e2 Q : ▷ wp E e1 Q ⊑ wp E (If LitTrue e1 e2) Q.
-Proof. rewrite -wp_case_inl //. by asimpl. Qed.
-Lemma wp_if_false E e1 e2 Q : ▷ wp E e2 Q ⊑ wp E (If LitFalse e1 e2) Q.
-Proof. rewrite -wp_case_inr //. by asimpl. Qed.
-Lemma wp_lt E n1 n2 P Q :
-  (n1 < n2 → P ⊑ ▷ Q LitTrueV) →
-  (n1 ≥ n2 → P ⊑ ▷ Q LitFalseV) →
-  P ⊑ wp E (Lt (LitNat n1) (LitNat n2)) Q.
-Proof.
-  intros; rewrite -(wp_bind [LeLCtx _]) -wp_plus -later_intro /=.
-  auto using wp_le with lia.
-Qed.
-Lemma wp_eq E n1 n2 P Q :
-  (n1 = n2 → P ⊑ ▷ Q LitTrueV) →
-  (n1 ≠ n2 → P ⊑ ▷ Q LitFalseV) →
-  P ⊑ wp E (Eq (LitNat n1) (LitNat n2)) Q.
-Proof.
-  intros HPeq HPne.
-  rewrite -wp_let -wp_value' // -later_intro; asimpl.
-  rewrite -wp_rec //; asimpl.
-  rewrite -(wp_bind [CaseCtx _ _]) -later_intro; asimpl.
-  apply wp_le; intros; asimpl.
-  * rewrite -wp_case_inl // -!later_intro. apply wp_le; auto with lia.
-  * rewrite -wp_case_inr // -later_intro -wp_value' //; auto with lia.
-Qed.
-End suger.

barrier/tests.v

-(** This file is essentially a bunch of testcases. *)
-Require Import modures.logic.
-Require Import barrier.lifting barrier.sugar.
-Import heap_lang.
-Import uPred.
-
-Module LangTests.
-  Definition add := Plus (LitNat 21) (LitNat 21).
-  Goal ∀ σ, prim_step add σ (LitNat 42) σ None.
-  Proof. intros; do_step done. Qed.
-  Definition rec := Rec (App (Var 0) (Var 1)). (* fix f x => f x *)
-  Definition rec_app := App rec (LitNat 0).
-  Goal ∀ σ, prim_step rec_app σ rec_app σ None.
-  Proof. intros; do_step done. Qed.
-  Definition lam := Lam (Plus (Var 0) (LitNat 21)).
-  Goal ∀ σ, prim_step (App lam (LitNat 21)) σ add σ None.
-  Proof. intros; do_step done. Qed.
-End LangTests.
-
-Module LiftingTests.
-  Context {Σ : iFunctor}.
-  Implicit Types P : iProp heap_lang Σ.
-  Implicit Types Q : val → iProp heap_lang Σ.
-
-  (* TODO RJ: Some syntactic sugar for language expressions would be nice. *)
-  Definition e3 := Load (Var 0).
-  Definition e2 := Seq (Store (Var 0) (Plus (Load $ Var 0) (LitNat 1))) e3.
-  Definition e := Let (Alloc (LitNat 1)) e2.
-  Goal ∀ σ E, (ownP σ : iProp heap_lang Σ) ⊑ (wp E e (λ v, ■(v = LitNatV 2))).
-  Proof.
-    move=> σ E. rewrite /e.
-    rewrite -wp_let. rewrite -wp_alloc_pst; last done.
-    apply sep_intro_True_r; first done.
-    rewrite -later_intro. apply forall_intro=>l.
-    apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_.
-    rewrite -later_intro. asimpl.
-    rewrite -(wp_bind [SeqCtx (Load (Loc _))]).
-    rewrite -(wp_bind [StoreRCtx (LocV _)]).
-    rewrite -(wp_bind [PlusLCtx _]).
-    rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
-    { by rewrite lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
-    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
-    rewrite -wp_plus -later_intro.
-    rewrite -wp_store_pst; first (apply sep_intro_True_r; first done); last first.
-    { by rewrite lookup_insert. }
-    { done. }
-    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
-    rewrite -wp_lam // -later_intro. asimpl.
-    rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
-    { by rewrite lookup_insert. }
-    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
-    by apply const_intro.
-  Qed.
-
-  Definition FindPred' n1 Sn1 n2 f := If (Lt Sn1 n2)
-                                      (App f Sn1)
-                                      n1.
-  Definition FindPred n2 := Rec (Let (Plus (Var 1) (LitNat 1))
-                                     (FindPred' (Var 2) (Var 0) n2.[ren(+3)] (Var 1))).
-  Definition Pred := Lam (If (Le (Var 0) (LitNat 0))
-                             (LitNat 0)
-                             (App (FindPred (Var 0)) (LitNat 0))
-                         ).
-
-  Lemma FindPred_spec n1 n2 E Q :
-    (■(n1 < n2) ∧ Q (LitNatV $ pred n2)) ⊑
-       wp E (App (FindPred (LitNat n2)) (LitNat n1)) Q.
-  Proof.
-    revert n1. apply löb_all_1=>n1.
-    rewrite -wp_rec //. asimpl.
-    (* Get rid of the ▷ in the premise. *)
-    etransitivity; first (etransitivity; last eapply equiv_spec, later_and).
-    { apply and_mono; first done. by rewrite -later_intro. }
-    apply later_mono.
-    (* Go on. *)
-    rewrite -(wp_let _ _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred $ LitNat n2))).
-    rewrite -wp_plus. asimpl.
-    rewrite -(wp_bind [CaseCtx _ _]).
-    rewrite -!later_intro /=.
-    apply wp_lt; intros Hn12.
-    * (* TODO RJ: It would be better if we could use wp_if_true here
-         (and below). But we cannot, because the substitutions in there
-         got already unfolded. *)
-      rewrite -wp_case_inl //.
-      rewrite -!later_intro. asimpl.
-      rewrite (forall_elim (S n1)).
-      eapply impl_elim; first by eapply and_elim_l. apply and_intro.
-      + apply const_intro; omega.
-      + by rewrite !and_elim_r.
-    * rewrite -wp_case_inr //.
-      rewrite -!later_intro -wp_value' //.
-      rewrite and_elim_r. apply const_elim_l=>Hle.
-      by replace n1 with (pred n2) by lia.
-  Qed.
-
-  Lemma Pred_spec n E Q :
-    ▷Q (LitNatV $ pred n) ⊑ wp E (App Pred (LitNat n)) Q.
-  Proof.
-    rewrite -wp_lam //. asimpl.
-    rewrite -(wp_bind [CaseCtx _ _]).
-    apply later_mono, wp_le=> Hn.
-    - rewrite -wp_case_inl //.
-      rewrite -!later_intro -wp_value' //.
-      by replace n with 0 by lia.
-    - rewrite -wp_case_inr //.
-      rewrite -!later_intro -FindPred_spec.
-      auto using and_intro, const_intro with lia.
-  Qed.
-
-  Goal ∀ E,
-    True ⊑ wp (Σ:=Σ) E
-      (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, ■(v = LitNatV 40)).
-  Proof.
-    intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro.
-    asimpl. (* TODO RJ: Can we somehow make it so that Pred gets folded again? *)
-    rewrite -Pred_spec -later_intro. by apply const_intro.
-  Qed.
-End LiftingTests.

configure

-#!/bin/sh
-coq_makefile -f _CoqProject -o Makefile