.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
@@ -8,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:
-  - coqc -v
-  - 'time make -j8 TIMED=y 2>&1 | tee build-log.txt'
-  - 'fgrep Axiom build-log.txt && exit 1'
-  - 'cat build-log.txt  | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
-  - make validate
-  only:
-  - master
-  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

-The source code (i.e., everything except for files in the docs/ folder) in this
-development is licensed under the terms of the BSD license, while the
-documentation (i.e., everything inside the docs/ folder) is licensed under the
-terms of the CC-BY 4.0 license.  Fur further details, see LICENSE-CODE and
-LICENSE-DOCS, respectively.
+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/, are distributed
-under the terms of the BSD license, included below.
+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
 
-                            BSD LICENCE
+------------------------------------------------------------------------------
 
 Redistribution and use in source and binary forms, with or without
 modification, are permitted provided that the following conditions are met:
@@ -12,17 +13,17 @@ modification, are permitted provided that the following conditions are met:
     * 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.
+    * 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 <COPYRIGHT HOLDER> BE LIABLE FOR ANY
-DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+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
+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/ folder of this development are distributed
+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.

Makefile

-# Makefile originally taken from coq-club
-
-%: Makefile.coq phony
-	+make -f Makefile.coq $@
-
+# Default target
 all: Makefile.coq
-	+make -f Makefile.coq all
+	+@$(MAKE) -f Makefile.coq all
+.PHONY: all
 
-clean: Makefile.coq
-	+make -f Makefile.coq clean
-	rm -f Makefile.coq
-
-Makefile.coq: _CoqProject Makefile
-	coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq
+# Build with dune.
+# This exists only for CI; you should just call `dune build` directly instead.
+dune:
+	@dune build --display=short
+.PHONY: dune
 
-_CoqProject: ;
-
-Makefile: ;
+# 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
 
-.PHONY: all clean 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 $@

ProofMode.md

-Tactic overview
-===============
-
-Many of the tactics below apply to more goals than described in this document
-since the behavior of these tactics can be tuned via instances of the type
-classes in the file [proofmode/classes](proofmode/classes.v). Most notable, many
-of the tactics can be applied when the to be introduced or to be eliminated
-connective appears under a later, an update modality, or in the conclusion of a
-weakest precondition.
-
-Applying hypotheses and lemmas
-------------------------------
-
-- `iExact "H"`  : finish the goal if the conclusion matches the hypothesis `H`
-- `iAssumption` : finish the goal if the conclusion matches any hypothesis
-- `iApply pm_trm` : match the conclusion of the current goal against the
-  conclusion of `pm_trm` and generates goals for the premises of `pm_trm`. See
-  proof mode terms below.
-
-Context management
-------------------
-
-- `iIntros (x1 ... xn) "ipat1 ... ipatn"` : introduce universal quantifiers
-  using Coq introduction patterns `x1 ... xn` and implications/wands using proof
-  mode introduction patterns `ipat1 ... ipatn`.
-- `iClear (x1 ... xn) "selpat"` : clear the hypotheses given by the selection
-  pattern `selpat` and the Coq level hypotheses/variables `x1 ... xn`.
-- `iRevert (x1 ... xn) "selpat"` : revert the hypotheses given by the selection
-  pattern `selpat` into wands, and the Coq level hypotheses/variables
-  `x1 ... xn` into universal quantifiers. Persistent hypotheses are wrapped into
-  the always modality.
-- `iRename "H1" into "H2"` : rename the hypothesis `H1` into `H2`.
-- `iSpecialize pm_trm` : instantiate universal quantifiers and eliminate
-  implications/wands of a hypothesis `pm_trm`. See proof mode terms below.
-- `iSpecialize pm_trm as #` : instantiate universal quantifiers and eliminate
-  implications/wands of a hypothesis whose conclusion is persistent. In this
-  case, all hypotheses can be used for proving the premises, as well as for
-  the resulting goal.
-- `iPoseProof pm_trm as "H"` : put `pm_trm` into the context as a new hypothesis
-  `H`.
-- `iAssert P with "spat" as "ipat"` : create a new goal with conclusion `P` and
-  put `P` in the context of the original goal. The specialization pattern
-  `spat` specifies which hypotheses will be consumed by proving `P`. The
-  introduction pattern `ipat` specifies how to eliminate `P`.
-- `iAssert P with "spat" as %cpat` : assert `P` and eliminate it using the Coq
-  introduction pattern `cpat`.
-
-Introduction of logical connectives
------------------------------------
-
-- `iPureIntro` : turn a pure goal into a Coq goal. This tactic works for goals
-  of the shape `■ φ`, `a ≡ b` on discrete COFEs, and `✓ a` on discrete CMRAs.
-
-- `iLeft` : left introduction of disjunction.
-- `iRight` : right introduction of disjunction.
-
-- `iSplit` : introduction of a conjunction, or separating conjunction provided
-  one of the operands is persistent.
-- `iSplitL "H1 ... Hn"` : introduction of a separating conjunction. The
-  hypotheses `H1 ... Hn` are used for the left conjunct, and the remaining ones
-  for the right conjunct. Persistent hypotheses are ignored, since these do not
-  need to be split.
-- `iSplitR "H0 ... Hn"` : symmetric version of the above.
-- `iExist t1, .., tn` : introduction of an existential quantifier.
-
-Elimination of logical connectives
-----------------------------------
-
-- `iExFalso` : Ex falso sequitur quod libet.
-- `iDestruct pm_trm as (x1 ... xn) "ipat"` : elimination of existential
-  quantifiers using Coq introduction patterns `x1 ... xn` and elimination of
-  object level connectives using the proof mode introduction pattern `ipat`.
-  In case all branches of `ipat` start with an `#` (moving the hypothesis to the
-  persistent context) or `%` (moving the hypothesis to the pure Coq context),
-  one can use all hypotheses for proving the premises of `pm_trm`, as well as
-  for proving the resulting goal.
-- `iDestruct pm_trm as %cpat` : elimination of a pure hypothesis using the Coq
-  introduction pattern `cpat`. When using this tactic, all hypotheses can be
-  used for proving the premises of `pm_trm`, as well as for proving the
-  resulting goal.
-
-Separating logic specific tactics
----------------------------------
-
-- `iFrame (t1 .. tn) "selpat"` : cancel the Coq terms (or Coq hypotheses)
-  `t1 ... tn` and Iris hypotheses given by `selpat` in the goal. The constructs
-  of the selection pattern have the following meaning:
-
-  + `%` : repeatedly frame hypotheses from the Coq context.
-  + `#` : repeatedly frame hypotheses from the persistent context.
-  + `★` : frame as much of the spatial context as possible.
-
-  Notice that framing spatial hypotheses makes them disappear, but framing Coq
-  or persistent hypotheses does not make them disappear.
-
-  This tactic finishes the goal in case everything in the conclusion has been
-  framed.
-- `iCombine "H1" "H2" as "H"` : turns `H1 : P1` and `H2 : P2` into
-  `H : P1 ★ P2`.
-
-Modalities
-----------
-
-- `iModIntro` : introduction of a modality that is an instance of the
-  `IntoModal` type class. Instances include: later, except 0, basic update and
-  fancy update.
-- `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality `pm_trm` that is
-  an instance of the `ElimModal` type class. Instances include: later, except 0,
-  basic update and fancy update.
-
-The later modality
-------------------
-
-- `iNext` : introduce a later by stripping laters from all hypotheses.
-- `iLöb as "IH" forall (x1 ... xn)` : perform Löb induction by generating a
-  hypothesis `IH : ▷ goal`. The tactic generalizes over the Coq level variables
-  `x1 ... xn`, the hypotheses given by the selection pattern `selpat`, and the
-  spatial context.
-
-Induction
----------
-
-- `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction on
-  the Coq term `x`. The Coq introduction pattern is used to name the introduced
-  variables. The induction hypotheses are inserted into the persistent context
-  and given fresh names prefixed `IH`. The tactic generalizes over the Coq level
-  variables `x1 ... xn`, the hypotheses given by the selection pattern `selpat`,
-  and the spatial context.
-
-Rewriting
----------
-
-- `iRewrite pm_trm` : rewrite an equality in the conclusion.
-- `iRewrite pm_trm in "H"` : rewrite an equality in the hypothesis `H`.
-
-Iris
-----
-
-- `iInv N as (x1 ... xn) "ipat" "Hclose"` : open the invariant `N`, the update
-  for closing the invariant is put in a hypothesis named `Hclose`.
-
-Miscellaneous
--------------
-
-- The tactic `done` is extended so that it also performs `iAssumption` and
-  introduces pure connectives.
-- The proof mode adds hints to the core `eauto` database so that `eauto`
-  automatically introduces: conjunctions and disjunctions, universal and
-  existential quantifiers, implications and wand, always, later and update
-  modalities, and pure connectives.
-
-Selection patterns
-==================
-
-Selection patterns are used to select hypotheses in the tactics `iRevert`,
-`iClear`, `iFrame`, `iLöb` and `iInduction`. The proof mode supports the
-following _selection patterns_:
-
-- `H` : select the hypothesis named `H`.
-- `%` : select the entire pure/Coq context.
-- `#` : select the entire persistent context.
-- `★` : select the entire spatial context.
-
-Introduction patterns
-=====================
-
-Introduction patterns are used to perform introductions and eliminations of
-multiple connectives on the fly. The proof mode supports the following
-_introduction patterns_:
-
-- `H` : create a hypothesis named `H`.
-- `?` : create an anonymous hypothesis.
-- `_` : remove the hypothesis.
-- `$` : frame the hypothesis in the goal.
-- `[ipat ipat]` : (separating) conjunction elimination.
-- `[ipat|ipat]` : disjunction elimination.
-- `[]` : false elimination.
-- `%` : move the hypothesis to the pure Coq context (anonymously).
-- `# ipat` : move the hypothesis to the persistent context.
-- `> ipat` : eliminate a modality (if the goal permits).
-
-Apart from this, there are the following introduction patterns that can only
-appear at the top level:
-
-- `{H1 ... Hn}` : clear `H1 ... Hn`.
-- `{$H1 ... $Hn}` : frame `H1 ... Hn` (this pattern can be mixed with the
-  previous pattern, e.g., `{$H1 H2 $H3}`).
-- `!%` : introduce a pure goal (and leave the proof mode).
-- `!#` : introduce an always modality (given that the spatial context is empty).
-- `!>` : introduce a modality.
-- `/=` : perform `simpl`.
-- `*` : introduce all universal quantifiers.
-- `**` : introduce all universal quantifiers, as well as all arrows and wands.
-
-For example, given:
-
-        ∀ x, x = 0 ⊢ □ (P → False ∨ □ (Q ∧ ▷ R) -★ P ★ ▷ (R ★ Q ∧ x = pred 2)).
-
-You can write
-
-        iIntros (x) "% !# $ [[] | #[HQ HR]] /= !>".
-
-which results in:
-
-        x : nat
-        H : x = 0
-        ______________________________________(1/1)
-        "HQ" : Q
-        "HR" : R
-        --------------------------------------□
-        R ★ Q ∧ x = 1
-
-
-Specialization patterns
-=======================
-
-Since we are reasoning in a spatial logic, when eliminating a lemma or
-hypothesis of type ``P_0 -★ ... -★ P_n -★ R``, one has to specify how the
-hypotheses are split between the premises. The proof mode supports the following
-_specification patterns_ to express splitting of hypotheses:
-
-- `H` : use the hypothesis `H` (it should match the premise exactly). If `H` is
-  spatial, it will be consumed.
-- `[H1 ... Hn]` : generate a goal with the (spatial) hypotheses `H1 ... Hn` and
-  all persistent hypotheses. The spatial hypotheses among `H1 ... Hn` will be
-  consumed. Hypotheses may be prefixed with a `$`, which results in them being
-  framed in the generated goal.
-- `[-H1 ... Hn]`  : negated form of the above pattern. This pattern does not
-  accept hypotheses prefixed with a `$`.
-- `>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
-  is a modality, in which case the modality will be kept in the generated goal
-  for the premise will be wrapped into the modality.
-- `[#]` : This pattern can be used when eliminating `P -★ Q` with `P`
-  persistent. Using this pattern, all hypotheses are available in the goal for
-  `P`, as well the remaining goal.
-- `[%]` : This pattern can be used when eliminating `P -★ Q` when `P` is pure.
-  It will generate a Coq goal for `P` and does not consume any hypotheses.
-- `*` : instantiate all top-level universal quantifiers with meta variables.
-
-For example, given:
-
-        H : □ P -★ P 2 -★ x = 0 -★ Q1 ∗ Q2
-
-You can write:
-
-        iDestruct ("H" with "[#] [H1 H2] [%]") as "[H4 H5]".
-
-Proof mode terms
-================
-
-Many of the proof mode tactics (such as `iDestruct`, `iApply`, `iRewrite`) can
-take both hypotheses and lemmas, and allow one to instantiate universal
-quantifiers and implications/wands of these hypotheses/lemmas on the fly.
-
-The syntax for the arguments of these tactics, called _proof mode terms_, is:
-
-        (H $! t1 ... tn with "spat1 .. spatn")
-
-Here, `H` can be both a hypothesis, as well as a Coq lemma whose conclusion is
-of the shape `P ⊢ Q`. In the above, `t1 ... tn` are arbitrary Coq terms used
-for instantiation of universal quantifiers, and `spat1 .. spatn` are
-specialization patterns to eliminate implications and wands.
-
-Proof mode terms can be written down using the following short hands too:
-
-        (H with "spat1 .. spatn")
-        (H $! t1 ... tn)
-        H
-

README.md

-# IRIS COQ DEVELOPMENT
+# Iris Coq Development [[coqdoc]](https://plv.mpi-sws.org/coqdoc/iris/)
 
-This is the Coq development of the [Iris Project](http://plv.mpi-sws.org/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.
 
-## Prerequisites
+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.5pl2
- - 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
-
-The development can then be installed as the Coq user contribution `iris` by
-running:
-
-    make install
-
-## Structure
-
-* The folder [prelude](prelude) contains an extended "Standard Library" by
-  Robbert Krebbers <http://robbertkrebbers.nl/thesis.html>.
-* The folder [algebra](algebra) contains the COFE and CMRA constructions as well
-  as the solver for recursive domain equations.
-* The folder [base_logic](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 folder [program_logic](program_logic) specializes the base logic to build
-  Iris, the program logic.  Most crucially, this includes world satisfaction
-  and weakest preconditions.  Furthermore, some language-independent derived
-  constructions (e.g., STSs) are defined in this folder.
-* The folder [heap_lang](heap_lang) defines the ML-like concurrent heap language
-  * The subfolder [lib](heap_lang/lib) contains a few derived constructions
-    within this language, e.g., parallel composition.
-    Most notable here s [lib/barrier](heap_lang/lib/barrier), the implementation
-    and proof of a barrier as described in <http://doi.acm.org/10.1145/2818638>.
-* The folder [proofmode](proofmode) contains the Iris proof mode, which extends
-  Coq with contexts for persistent and spatial Iris assertions. It also contains
-  tactics for interactive proofs in Iris. Documentation can be found in
-  [ProofMode.md](ProofMode.md).
-* The folder [tests](tests) contains modules we use to test our infrastructure.
-  Users of the Iris Coq library should *not* depend on these modules; they may
-  change or disappear without any notice.
-
-## Documentation
-
-A LaTeX version of the core logic definitions and some derived forms is
-available in [docs/iris.tex](docs/iris.tex).  A compiled PDF version of this
-document is [http://plv.mpi-sws.org/iris/appendix-3.0.pdf](available online).
+ - 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 . iris
-prelude/option.v
-prelude/fin_map_dom.v
-prelude/bset.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/coPset.v
-prelude/lexico.v
-prelude/set.v
-prelude/decidable.v
-prelude/list.v
-prelude/error.v
-prelude/functions.v
-prelude/hlist.v
-prelude/sorting.v
-algebra/cmra.v
-algebra/cmra_big_op.v
-algebra/cmra_tactics.v
-algebra/sts.v
-algebra/auth.v
-algebra/gmap.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/frac.v
-algebra/csum.v
-algebra/list.v
-algebra/updates.v
-algebra/local_updates.v
-algebra/gset.v
-algebra/coPset.v
-base_logic/upred.v
-base_logic/primitive.v
-base_logic/derived.v
-base_logic/base_logic.v
-base_logic/tactics.v
-base_logic/big_op.v
-base_logic/hlist.v
-base_logic/soundness.v
-base_logic/double_negation.v
-program_logic/iprop.v
-program_logic/adequacy.v
-program_logic/lifting.v
-program_logic/invariants.v
-program_logic/wsat.v
-program_logic/weakestpre.v
-program_logic/fancy_updates.v
-program_logic/hoare.v
-program_logic/viewshifts.v
-program_logic/language.v
-program_logic/ectx_language.v
-program_logic/ectxi_language.v
-program_logic/ectx_lifting.v
-program_logic/own.v
-program_logic/saved_prop.v
-program_logic/auth.v
-program_logic/sts.v
-program_logic/namespaces.v
-program_logic/boxes.v
-program_logic/counter_examples.v
-program_logic/iris.v
-program_logic/thread_local.v
-program_logic/cancelable_invariants.v
-heap_lang/lang.v
-heap_lang/tactics.v
-heap_lang/wp_tactics.v
-heap_lang/lifting.v
-heap_lang/derived.v
-heap_lang/notation.v
-heap_lang/heap.v
-heap_lang/lib/spawn.v
-heap_lang/lib/par.v
-heap_lang/lib/assert.v
-heap_lang/lib/lock.v
-heap_lang/lib/spin_lock.v
-heap_lang/lib/ticket_lock.v
-heap_lang/lib/counter.v
-heap_lang/lib/barrier/barrier.v
-heap_lang/lib/barrier/specification.v
-heap_lang/lib/barrier/protocol.v
-heap_lang/lib/barrier/proof.v
-heap_lang/proofmode.v
-heap_lang/adequacy.v
-tests/atomic.v
-tests/heap_lang.v
-tests/one_shot.v
-tests/joining_existentials.v
-tests/proofmode.v
-tests/barrier_client.v
-tests/list_reverse.v
-tests/tree_sum.v
-tests/counter.v
-proofmode/coq_tactics.v
-proofmode/environments.v
-proofmode/intro_patterns.v
-proofmode/spec_patterns.v
-proofmode/sel_patterns.v
-proofmode/tactics.v
-proofmode/notation.v
-proofmode/classes.v
-proofmode/class_instances.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 iris.algebra Require Export cmra.
-From iris.base_logic Require Import base_logic.
-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 → agree_car x n ≡{n'}≡ agree_car 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 → agree_car x n ≡{n}≡ agree_car 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' → agree_car x n' ≡{n'}≡ agree_car y n').
-Program Instance agree_compl : Compl (agree A) := λ c,
-  {| agree_car n := agree_car (c n) n;
-     agree_is_valid n := agree_is_valid (c n) n |}.
-Next Obligation.
-  intros c n ?. apply (chain_cauchy c n (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 (agree_car 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 A) agree_cofe_mixin.
-
-Program Instance agree_op : Op (agree A) := λ x y,
-  {| agree_car := 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_pcore : PCore (agree A) := Some.
-
-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.
-  symmetry. 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.
-  apply cmra_total_mixin; try apply _ || by eauto.
-  - 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 [(?&?&?) ?].
-  - 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 agreeR : cmraT :=
-  CMRAT (agree A) agree_cofe_mixin agree_cmra_mixin.
-
-Global Instance agree_total : CMRATotal agreeR.
-Proof. rewrite /CMRATotal; eauto. Qed.
-Global Instance agree_persistent (x : agree A) : Persistent x.
-Proof. by constructor. Qed.
-
-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_uninj n (x : agree A) : ✓{n} x → ∃ y : A, to_agree y ≡{n}≡ x.
-Proof.
-  intros [??]. exists (agree_car x n).
-  split; naive_solver eauto using agree_valid_le.
-Qed.
-
-(** Internalized properties *)
-Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b : uPred M).
-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 agreeR : clear implicits.
-
-Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
-  {| agree_car n := f (agree_car x n); agree_is_valid := agree_is_valid x;
-     agree_valid_S := agree_valid_S _ x |}.
-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 agreeRF (F : cFunctor) : rFunctor := {|
-  rFunctor_car A B := agreeR (cFunctor_car F A B);
-  rFunctor_map A1 A2 B1 B2 fg := agreeC_map (cFunctor_map F fg)
-|}.
-Next Obligation.
-  intros ? A1 A2 B1 B2 n ???; simpl. by apply agreeC_map_ne, cFunctor_ne.
-Qed.
-Next Obligation.
-  intros F A B x; simpl. rewrite -{2}(agree_map_id x).
-  apply agree_map_ext=>y. by rewrite cFunctor_id.
-Qed.
-Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -agree_map_compose.
-  apply agree_map_ext=>y; apply cFunctor_compose.
-Qed.
-
-Instance agreeRF_contractive F :
-  cFunctorContractive F → rFunctorContractive (agreeRF F).
-Proof.
-  intros ? A1 A2 B1 B2 n ???; simpl.
-  by apply agreeC_map_ne, cFunctor_contractive.
-Qed.

algebra/auth.v

-From iris.algebra Require Export excl local_updates.
-From iris.base_logic Require Import base_logic.
-From iris.proofmode Require Import class_instances.
-Local Arguments valid _ _ !_ /.
-Local Arguments validN _ _ _ !_ /.
-
-Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }.
-Add Printing Constructor auth.
-Arguments Auth {_} _ _.
-Arguments authoritative {_} _.
-Arguments auth_own {_} _.
-Notation "◯ a" := (Auth None 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 ∧ auth_own x ≡ auth_own y.
-Instance auth_dist : Dist (auth A) := λ n x y,
-  authoritative x ≡{n}≡ authoritative y ∧ auth_own x ≡{n}≡ auth_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) (@auth_own A).
-Proof. by destruct 1. Qed.
-Global Instance own_proper : Proper ((≡) ==> (≡)) (@auth_own A).
-Proof. by destruct 1. Qed.
-
-Instance auth_compl : Compl (auth A) := λ c,
-  Auth (compl (chain_map authoritative c)) (compl (chain_map auth_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 auth_own c)).
-Qed.
-Canonical Structure authC := CofeT (auth A) 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 : ucmraT}.
-Implicit Types a b : A.
-Implicit Types x y : auth A.
-
-Instance auth_valid : Valid (auth A) := λ x,
-  match authoritative x with
-  | Excl' a => (∀ n, auth_own x ≼{n} a) ∧ ✓ a
-  | None => ✓ auth_own x
-  | ExclBot' => False
-  end.
-Global Arguments auth_valid !_ /.
-Instance auth_validN : ValidN (auth A) := λ n x,
-  match authoritative x with
-  | Excl' a => auth_own x ≼{n} a ∧ ✓{n} a
-  | None => ✓{n} auth_own x
-  | ExclBot' => False
-  end.
-Global Arguments auth_validN _ !_ /.
-Instance auth_pcore : PCore (auth A) := λ x,
-  Some (Auth (core (authoritative x)) (core (auth_own x))).
-Instance auth_op : Op (auth A) := λ x y,
-  Auth (authoritative x ⋅ authoritative y) (auth_own x ⋅ auth_own y).
-
-Lemma auth_included (x y : auth A) :
-  x ≼ y ↔ authoritative x ≼ authoritative y ∧ auth_own x ≼ auth_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 : ✓{n} x → ✓{n} authoritative x.
-Proof. by destruct x as [[[]|]]. Qed.
-Lemma auth_own_validN n x : ✓{n} x → ✓{n} auth_own x.
-Proof. destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN. Qed.
-
-Lemma auth_valid_discrete `{CMRADiscrete A} x :
-  ✓ x ↔ match authoritative x with
-        | Excl' a => auth_own x ≼ a ∧ ✓ a
-        | None => ✓ auth_own x
-        | ExclBot' => False
-        end.
-Proof.
-  destruct x as [[[?|]|] ?]; simpl; try done.
-  setoid_rewrite <-cmra_discrete_included_iff; naive_solver eauto using 0.
-Qed.
-Lemma auth_valid_discrete_2 `{CMRADiscrete A} a b : ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
-Proof. by rewrite auth_valid_discrete /= left_id. Qed.
-
-Lemma authoritative_valid  x : ✓ x → ✓ authoritative x.
-Proof. by destruct x as [[[]|]]. Qed.
-Lemma auth_own_valid `{CMRADiscrete A} x : ✓ x → ✓ auth_own x.
-Proof.
-  rewrite auth_valid_discrete.
-  destruct x as [[[]|]]; naive_solver eauto using cmra_valid_included.
-Qed.
-
-Lemma auth_cmra_mixin : CMRAMixin (auth A).
-Proof.
-  apply cmra_total_mixin.
-  - eauto.
-  - 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 as [?? Hx|]; first destruct Hx; intros ?; cofe_subst; auto.
-  - 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_core_l.
-  - by split; simpl; rewrite ?cmra_core_idemp.
-  - intros ??; rewrite! auth_included; intros [??].
-    by split; simpl; apply cmra_core_mono.
-  - 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.
-  - intros n x y1 y2 ? [??]; simpl in *.
-    destruct (cmra_extend n (authoritative x) (authoritative y1)
-      (authoritative y2)) as (ea1&ea2&?&?&?); auto using authoritative_validN.
-    destruct (cmra_extend n (auth_own x) (auth_own y1) (auth_own y2))
-      as (b1&b2&?&?&?); auto using auth_own_validN.
-    by exists (Auth ea1 b1), (Auth ea2 b2).
-Qed.
-Canonical Structure authR := CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.
-
-Global Instance auth_cmra_discrete : CMRADiscrete A → CMRADiscrete authR.
-Proof.
-  split; first apply _.
-  intros [[[?|]|] ?]; rewrite /= /cmra_valid /cmra_validN /=; auto.
-  - setoid_rewrite <-cmra_discrete_included_iff.
-    rewrite -cmra_discrete_valid_iff. tauto.
-  - by rewrite -cmra_discrete_valid_iff.
-Qed.
-
-Instance auth_empty : Empty (auth A) := Auth ∅ ∅.
-Lemma auth_ucmra_mixin : UCMRAMixin (auth A).
-Proof.
-  split; simpl.
-  - apply (@ucmra_unit_valid A).
-  - by intros x; constructor; rewrite /= left_id.
-  - do 2 constructor; simpl; apply (persistent_core _).
-Qed.
-Canonical Structure authUR :=
-  UCMRAT (auth A) auth_cofe_mixin auth_cmra_mixin auth_ucmra_mixin.
-
-Global Instance auth_frag_persistent a : Persistent a → Persistent (◯ a).
-Proof. do 2 constructor; simpl; auto. by apply persistent_core. Qed.
-
-(** Internalized properties *)
-Lemma auth_equivI {M} (x y : auth A) :
-  x ≡ y ⊣⊢ (authoritative x ≡ authoritative y ∧ auth_own x ≡ auth_own y : uPred M).
-Proof. by uPred.unseal. Qed.
-Lemma auth_validI {M} (x : auth A) :
-  ✓ x ⊣⊢ (match authoritative x with
-          | Excl' a => (∃ b, a ≡ auth_own x ⋅ b) ∧ ✓ a
-          | None => ✓ auth_own x
-          | ExclBot' => False
-          end : uPred M).
-Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
-
-Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
-Proof. done. Qed.
-Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
-Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
-Global Instance auth_frag_cmra_homomorphism : UCMRAHomomorphism (Auth None).
-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_auth_valid a : ✓ a → ✓ (● a).
-Proof. intros; split; simpl; auto using ucmra_unit_leastN. Qed.
-
-Lemma auth_update a b a' b' :
-  (a,b) ~l~> (a',b') → ● a ⋅ ◯ b ~~> ● a' ⋅ ◯ b'.
-Proof.
-  intros Hup; apply cmra_total_update.
-  move=> n [[[?|]|] bf1] // [[bf2 Ha] ?]; do 2 red; simpl in *.
-  move: Ha; rewrite !left_id -assoc=> Ha.
-  destruct (Hup n (Some (bf1 ⋅ bf2))); auto.
-  split; last done. exists bf2. by rewrite -assoc.
-Qed.
-
-Lemma auth_update_alloc a a' b' : (a,∅) ~l~> (a',b') → ● a ~~> ● a' ⋅ ◯ b'.
-Proof. intros. rewrite -(right_id _ _ (● a)). by apply auth_update. Qed.
-Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',∅) → ● a ⋅ ◯ b ~~> ● a'.
-Proof. intros. rewrite -(right_id _ _ (● a')). by apply auth_update. Qed.
-End cmra.
-
-Arguments authR : clear implicits.
-Arguments authUR : clear implicits.
-
-(* Proof mode class instances *)
-Instance from_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
-  FromOp a b1 b2 → FromOp (◯ a) (◯ b1) (◯ b2).
-Proof. done. Qed.
-Instance into_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
-  IntoOp a b1 b2 → IntoOp (◯ a) (◯ b1) (◯ b2).
-Proof. done. Qed.
-
-(* Functor *)
-Definition auth_map {A B} (f : A → B) (x : auth A) : auth B :=
-  Auth (excl_map f <$> authoritative x) (f (auth_own x)).
-Lemma auth_map_id {A} (x : auth A) : auth_map id x = x.
-Proof. by destruct x as [[[]|]]. 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 as [[[]|]]. 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.
-  apply option_fmap_setoid_ext=> a; by apply excl_map_ext.
-Qed.
-Instance auth_map_ne {A B : cofeT} n :
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
-Proof.
-  intros f g Hf [??] [??] [??]; split; simpl in *; [|by apply Hf].
-  apply option_fmap_ne; [|done]=> x y ?; by apply excl_map_ne.
-Qed.
-Instance auth_map_cmra_monotone {A B : ucmraT} (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 cmra_monotoneN, cmra_monotone_validN.
-  - by intros [x a] [y b]; rewrite !auth_included /=;
-      intros [??]; split; simpl; apply: cmra_monotone.
-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 authRF (F : urFunctor) : rFunctor := {|
-  rFunctor_car A B := authR (urFunctor_car F A B);
-  rFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
-|}.
-Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
-Qed.
-Next Obligation.
-  intros F A B x. rewrite /= -{2}(auth_map_id x).
-  apply auth_map_ext=>y; apply urFunctor_id.
-Qed.
-Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
-  apply auth_map_ext=>y; apply urFunctor_compose.
-Qed.
-
-Instance authRF_contractive F :
-  urFunctorContractive F → rFunctorContractive (authRF F).
-Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
-Qed.
-
-Program Definition authURF (F : urFunctor) : urFunctor := {|
-  urFunctor_car A B := authUR (urFunctor_car F A B);
-  urFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
-|}.
-Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
-Qed.
-Next Obligation.
-  intros F A B x. rewrite /= -{2}(auth_map_id x).
-  apply auth_map_ext=>y; apply urFunctor_id.
-Qed.
-Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
-  apply auth_map_ext=>y; apply urFunctor_compose.
-Qed.
-
-Instance authURF_contractive F :
-  urFunctorContractive F → urFunctorContractive (authURF F).
-Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
-Qed.

algebra/base.v

-From mathcomp Require Export ssreflect.
-From iris.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_tactics.v

-From iris.algebra Require Export cmra.
-From iris.algebra Require Import cmra_big_op.
-
-(** * Simple solver for validity and inclusion by reflection *)
-Module ra_reflection. Section ra_reflection.
-  Context  {A : ucmraT}.
-
-  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 id ∅ (Σ !! 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 id ∅ (Σ !! n)) <$> flatten e).
-  Proof.
-    induction e as [| |e1 IH1 e2 IH2]; rewrite /= ?right_id //.
-    by rewrite fmap_app IH1 IH2 big_op_app.
-  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.