rebase transfinite iris

0c58544d · Lennard Gäher · 75a18932 · 0c58544d · 75a18932 · 0c58544d
Commit 0c58544d authored Nov 24, 2020 by Lennard Gäher
--- a/.gitignore
+++ b/.gitignore
 *.vo
+*.vok
+*.vos
 *.vio
 *.v.d
 .coqdeps.d
@@ -13,6 +15,16 @@
 .coq-native/
 build-dep/
 Makefile.coq
+.Makefile.coq.d
 Makefile.coq.conf
 *.crashcoqide
 .env
+_opam
+
+
+*.fdb_latexmk
+*.fls
+**/auto/*
+
+*.pygtex
+*.pygstyle
\ No newline at end of file
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
-image: ralfjung/opam-ci:opam2
-
-stages:
-  - build
-
-variables:
-  CPU_CORES: "10"
-
-.template: &template
-  stage: build
-  tags:
-  - fp
-  script:
-  - git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
-  - ci/buildjob
-  cache:
-    key: "$CI_JOB_NAME"
-    paths:
-    - opamroot/
-  only:
-  - master
-  - /^ci/
-  except:
-  - triggers
-  - schedules
-  - api
-
-## Build jobs
-
-build-coq.dev:
-  <<: *template
-  variables:
-    OCAML: "ocaml-base-compiler.4.07.0"
-    OPAM_PINS: "coq version dev"
-    CI_COQCHK: "1"
-
-build-coq.8.10.dev:
-  <<: *template
-  variables:
-    OCAML: "ocaml-base-compiler.4.07.0"
-    OPAM_PINS: "coq version 8.10.dev"
-
-build-coq.8.9.1:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.9.1"
-
-build-coq.8.9.0:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.9.0"
-    OPAM_PKG: "coq-iris"
-    DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
-    DOC_OPTS: "--external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp"
-    TIMING_CONF: "coq-8.9.0"
-  tags:
-  - fp-timing
-
-build-coq.8.8.2:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.8.2"
-
-build-coq.8.7.2:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.7.2"
--- a/Makefile
+++ b/Makefile
@@ -9,7 +9,7 @@ all: Makefile.coq
 clean: Makefile.coq
 	+@make -f Makefile.coq clean
 	find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
-	rm -f Makefile.coq
+	rm -f Makefile.coq .lia.cache
 .PHONY: clean

 # Create Coq Makefile.
@@ -29,14 +29,8 @@ build-dep: build-dep/opam phony
 	@# 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 "# Pinning build-dep package." && \
-	  if opam --version | grep "^1\." -q; then \
-	    BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
-	    opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
-	    opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
-	  else \
-	    opam install $(OPAMFLAGS) build-dep/; \
-	  fi
+	@echo "# Installing build-dep package."
+	@opam install $(OPAMFLAGS) build-dep/

 # Some files that do *not* need to be forwarded to Makefile.coq
 Makefile: ;

--- a/Makefile.coq.local
+++ b/Makefile.coq.local
-# Run tests interleaved with main build.  They have to be in the same target for this.
-real-all: $(if $(NO_TEST),,test)
-
-# the test suite
-TESTFILES=$(wildcard tests/*.v)
-NORMALIZER=test-normalizer.sed
-
-test: $(TESTFILES:.v=.vo)
-.PHONY: test
-
-COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.7\b" -q && echo 1)
-COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
-
-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.
-# - 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)TEST="$$(basename -s .v $<)" && \
-	  if test -f "tests/$$TEST.$(COQ_MINOR_VERSION).ref"; then \
-	    REF="tests/$$TEST.$(COQ_MINOR_VERSION).ref"; \
-	  else \
-	    REF="tests/$$TEST.ref"; \
-	  fi && \
-	  echo "COQTEST$(if $(COQ_OLD), [no ref],$(if $(MAKE_REF), [make ref],)) $<$(if $(COQ_OLD),, (ref: $$REF))" && \
-	  TMPFILE="$$(mktemp)" && \
-	  $(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
-	  sed -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
-	  mv "$$TMPFILE".new "$$TMPFILE" && \
-	  $(if $(COQ_OLD),true, \
-	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff -u "$$REF" "$$TMPFILE") \
-	  ) && \
-	  rm -f "$$TMPFILE" && \
-	  touch $@
--- a/README.md
+++ b/README.md
-# IRIS COQ DEVELOPMENT [[coqdoc]](https://plv.mpi-sws.org/coqdoc/iris/)
+# TRANSFINITE IRIS COQ DEVELOPMENT

-This is the Coq development of the [Iris Project](http://iris-project.org),
+This is the Coq development of the Transfinite Iris project. 
+It is based on 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 Transfinite Iris, a supplementary appendix PDF has been submitted alongside this artifact.

-For understanding the theory of Iris, 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
-[available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
+For using Transfinite Iris and inspecting the development interactively, it needs to be compiled.

-## Building Iris
+## Building Transfinite Iris

 ### Prerequisites

 This version is known to compile with:

- - Coq 8.7.2 / 8.8.2 / 8.9.0 / 8.9.1
- - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
+ - Coq 8.10.2
+ - Iris-stdpp 1.3.0 ([std++](https://gitlab.mpi-sws.org/iris/stdpp))

-For a version compatible with Coq 8.6, have a look at the
-[iris-3.1 branch](https://gitlab.mpi-sws.org/iris/iris/tree/iris-3.1).
-If you need to work with Coq 8.5, please check out the
-[iris-3.0 branch](https://gitlab.mpi-sws.org/iris/iris/tree/iris-3.0).
+We assume that you have opam (2.0 or newer; tested with 2.0.7) available for the following instructions.

-### Working *with* Iris
+### Installation

-To use Iris in your own proofs, we recommend you install Iris via opam (1.2.2 or
-newer).  To obtain the latest stable release, you have to add the Coq opam
-repository:
+1. Setup a new opam switch and switch to it:
+  ```
+  opam update
+  opam switch create iris-transfinite 4.07.1+flambda
+  eval $(opam env)
+  ```

-    opam repo add coq-released https://coq.inria.fr/opam/released
+2. Add the Coq opam repository: 
+```
+  opam repo add coq-released https://coq.inria.fr/opam/released
+```
+3. Run `make build-dep` to install the right versions of the dependencies, 
+   in particular Coq 8.10.2 and coq-stdpp 1.3.0.

-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 do `opam install coq-iris`.  To fetch updates later, run
-`opam update && opam upgrade`.  However, notice that we do not guarnatee
-backwards-compatibility, so upgrading Iris may break your Iris-using
-developments.
-
-### Working *on* Iris
-
-To work on Iris itself, you need to install its build-dependencies.  Again we
-recommend you do that with opam (1.2.2 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 build-dep` 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 build-dep`.
+4. Run `make -jN` to build the full development, where `N` is the number of threads
+   to use for the build process.

 ## Directory Structure

-* The folder [algebra](theories/algebra) contains the COFE and CMRA
-  constructions as well as the solver for recursive domain equations.
+* The folder [ordinals](theories/algebra/ordinals) contains a formalisation of 
+  von Neumann ordinals and basic ordinal arithmetic. 
+* The folder [algebra](theories/algebra) contains step-index types, 
+  the COFE and CMRA constructions as well as the solver for recursive domain equations.
 * The folder [base_logic](theories/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.
@@ -74,9 +53,11 @@ followed by `make build-dep`.
    dynamic resources and ownership of them; the other constructions depend
    on this setup.
 * The folder [program_logic](theories/program_logic) specializes the base logic
-  to build Iris, the program logic.   This includes weakest preconditions that
+  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 [refinement](theories/program_logic/refinement) contains the definition
+  of a program logic for termination-preserving refinement and termination.
 * The folder [bi](theories/bi) contains the BI++ laws, as well as derived
  connectives, laws and constructions that are applicable for general BIS.
 * The folder [proofmode](theories/proofmode) contains
@@ -85,59 +66,64 @@ followed by `make build-dep`.
  interactive proofs. Documentation can be found in
  [ProofMode.md](ProofMode.md).
 * The folder [heap_lang](theories/heap_lang) defines the ML-like concurrent heap
-  language
-  * The subfolder [lib](theories/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 folder [tests](theories/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.
-
-## 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).
-
-## Further Resources
-
-Getting along with Iris in Coq:
-
-* Iris proof patterns are documented in the [proof guide](ProofGuide.md).
-* Syntactic conventions are described in the [style guide](StyleGuide.md).
-* The Iris tactics are described in the
-  [the Iris Proof Mode (IPM) / MoSeL documentation](ProofMode.md) as well as the
-  [HeapLang documentation](HeapLang.md).
-* The generated coqdoc is [available online](https://plv.mpi-sws.org/coqdoc/iris/).
-
-Contacting the developers:
-
-* Discussion about the Iris Coq development happens on the mailing list
-  [iris-club@lists.mpi-sws.org](https://lists.mpi-sws.org/listinfo/iris-club)
-  and in the [Iris Chat](https://mattermost.mpi-sws.org/iris).  This is also the
-  right place to ask questions.  The chat requires an account at the
-  [MPI-SWS GitLab](https://gitlab.mpi-sws.org/users/sign_in) (use the "Register"
-  tab). If you have trouble joining the chat, please contact
-  [Ralf](https://gitlab.mpi-sws.org/jung).
-* If you want to report a bug, please use the
-  [issue tracker](https://gitlab.mpi-sws.org/iris/iris/issues), which also
-  requires an MPI-SWS GitLab 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](Editor.md).
-* If you are writing a paper that uses Iris in one way or another, you could use
-  the [Iris LaTeX macros](docs/iris.sty) for typesetting the various Iris
-  connectives.
+  language.
+* The folder [examples](theories/examples) contains examples executed in 
+  Transfinite Iris. See below for a detailed summary.
+
+## Examples
+
+The following is a list of examples we have done in Transfinite Iris.
+* The key notions of simulations and generalized simulations used for the 
+  key ideas section of the paper are formalized in [keyideas](theories/examples/keyideas).
+* Counterexamples for some negative statements in the paper are formalized in 
+  [counterexamples.v](theories/examples/counterexamples.v)
+* [safety](theories/examples/safety) contains examples for safety reasoning taken 
+  from existing work that we have ported to Transfinite Iris.
+* [termination](theories/examples/termination) contains proofs of termination:
+  * [eventloop](theories/examples/termination/eventloop.v) contains the verification
+    of the eventloop example from the paper.
+  * [thunk](theories/examples/termination/thunk.v) contains the verification of a thunk example.
+  * [logrel](theories/examples/termination/logrel.v) formalizes and extends the 
+    logical relation for termination by Spies et al, "Transfinite Step-Indexing for Termination" 
+* [refinements](theories/examples/refinements) contains the termination-preserving refinement
+  examples from the paper.
+  * [derived] (theories/examples/refinements/derived.v) contains the derived Hoare triples shown in the paper.
+  * [refinement](theories/examples/refinements/refinement.v) contains the HeapLang source language.
+  * [memoization](theories/examples/refinement/memoization.v) provides memoization functions and 
+    the following examples:
+    * Fibonacci function
+    * Levenshtein distance
+
+
+## Theorems referenced in the paper
+
+We have fully mechanized the soundness of Iris and the examples in §3.4 and §4.2.
+The following table references the corresponding theorems as well as some additional mechanized lemmas.
+
+| Paper | Coq |
+| ------ | ------ |
+| Lemma 2.1 | [simulations/sim_is_rpr](theories/examples/keyideas/simulations.v) |
+| Lemma 2.2 | [simulations/sim_is_tpr](theories/examples/keyideas/simulations.v) |
+| Hoare Proof Rules of Figure 1 | [derived](theories/examples/refinements/derived.v) |
+| Theorem 3.3 (Refinement Adequacy) | [heap_lang_ref_adequacy](theories/examples/refinements/refinement.v) | 
+| Definition of memo_rec | [mem_rec](theories/examples/refinements/memoization.v) | 
+| PureMemoRec (simpl) | [natfun_mem_rec_spec](theories/examples/refinements/memoization.v) | 
+| Levenshtein and Fibonacci | [memoization](theories/examples/refinements/memoization.v) | 
+| Theorem 4.1 (Time Credits Adequacy) | [heap_lang_ref_adequacy](theories/examples/termination/adequacy.v) | 
+| Reentrant Event Loop | [event_loop](theories/examples/termination/eventloop.v) | 
+| Logical Relation for Termination | [logrel_adequacy](theories/examples/termination/logrel.v) | 
+| Ordinals validate the existential property | [set_model_large_index](theories/algebra/ordinals/ord_stepindex.v) |
+| Theorem 5.3 | [fixpoint](theories/algebra/ofe.v) | 
+| Model Construction (Theorem 5.4) | [iprop](theories/base_logic/lib/iprop.v) | 
+| Theorem 5.5 | [no_later_existential_commuting](theories/examples/counterexamples.v) | 
+
+## Acknowledgements
+
+The mechanization of set-theoretic ordinals and the underlying ZF model construction 
+has been based on Coq code by Dominik Kirst and Gert Smolka, available at: 
+
+* "Large Model Constructions for Second-Order ZF in Dependent Type Theory"
+  by Dominik Kirst and Gert Smolka, CPP 2018
+  See https://www.ps.uni-saarland.de/Publications/details/KirstSmolka:2017:Large-Model.html.
+* "Formalised Set Theory: Well-Orderings and the Axiom of Choice", Dominik Kirst. 
+  See https://www.ps.uni-saarland.de/~kirst/bachelor.php 
--- a/_CoqProject
+++ b/_CoqProject
@@ -11,17 +11,34 @@
 # We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
 -arg -w -arg -ambiguous-paths

+theories/algebra/ordinals/set_model.v
+theories/algebra/ordinals/set_sets.v
+theories/algebra/ordinals/set_functions.v
+theories/algebra/ordinals/set_ordinals.v
+theories/algebra/ordinals/ord_stepindex.v
+theories/algebra/ordinals/arithmetic.v
+
+theories/algebra/base.v
+theories/algebra/stepindex.v
 theories/algebra/monoid.v
+theories/algebra/ofe.v
 theories/algebra/cmra.v
+theories/algebra/updates.v
+theories/base_logic/base_logic.v
+theories/program_logic/language.v
+theories/bi/notation.v
+theories/bi/interface.v
+theories/bi/derived_connectives.v
+theories/bi/derived_laws_bi.v
+theories/bi/derived_laws_sbi.v
+theories/bi/satisfiable.v
+
+
 theories/algebra/big_op.v
-theories/algebra/cmra_big_op.v
-theories/algebra/sts.v
 theories/algebra/auth.v
 theories/algebra/frac_auth.v
 theories/algebra/gmap.v
-theories/algebra/ofe.v
-theories/algebra/base.v
-theories/algebra/dra.v
+theories/algebra/wf_IR.v
 theories/algebra/cofe_solver.v
 theories/algebra/agree.v
 theories/algebra/excl.v
@@ -30,71 +47,59 @@ theories/algebra/frac.v
 theories/algebra/csum.v
 theories/algebra/list.v
 theories/algebra/vector.v
-theories/algebra/updates.v
 theories/algebra/local_updates.v
 theories/algebra/gset.v
 theories/algebra/gmultiset.v
 theories/algebra/coPset.v
-theories/algebra/deprecated.v
 theories/algebra/proofmode_classes.v
 theories/algebra/ufrac.v
 theories/algebra/namespace_map.v
 theories/algebra/ufrac_auth.v
-theories/bi/notation.v
-theories/bi/interface.v
-theories/bi/derived_connectives.v
-theories/bi/derived_laws_bi.v
-theories/bi/derived_laws_sbi.v
+theories/algebra/dfrac.v
+theories/algebra/auth_map.v
+theories/algebra/auth_frac.v
+theories/algebra/mlist.v
 theories/bi/plainly.v
 theories/bi/big_op.v
 theories/bi/updates.v
 theories/bi/bi.v
 theories/bi/tactics.v
-theories/bi/monpred.v
 theories/bi/embedding.v
 theories/bi/weakestpre.v
 theories/bi/telescopes.v
-theories/bi/lib/counterexamples.v
 theories/bi/lib/fixpoint.v
 theories/bi/lib/fractional.v
-theories/bi/lib/laterable.v
-theories/bi/lib/atomic.v
-theories/bi/lib/core.v
 theories/base_logic/upred.v
 theories/base_logic/bi.v
 theories/base_logic/derived.v
 theories/base_logic/proofmode.v
-theories/base_logic/base_logic.v
-theories/base_logic/bupd_alt.v
+theories/base_logic/satisfiable.v
 theories/base_logic/lib/iprop.v
 theories/base_logic/lib/own.v
 theories/base_logic/lib/saved_prop.v
 theories/base_logic/lib/wsat.v
 theories/base_logic/lib/invariants.v
 theories/base_logic/lib/fancy_updates.v
+theories/base_logic/lib/logical_step.v
 theories/base_logic/lib/viewshifts.v
-theories/base_logic/lib/auth.v
-theories/base_logic/lib/sts.v
-theories/base_logic/lib/boxes.v
 theories/base_logic/lib/na_invariants.v
 theories/base_logic/lib/cancelable_invariants.v
 theories/base_logic/lib/gen_heap.v
-theories/base_logic/lib/fancy_updates_from_vs.v
 theories/base_logic/lib/proph_map.v
-theories/program_logic/adequacy.v
-theories/program_logic/lifting.v
 theories/program_logic/weakestpre.v
-theories/program_logic/total_weakestpre.v
-theories/program_logic/total_adequacy.v
+theories/program_logic/lifting.v
+theories/program_logic/adequacy.v
 theories/program_logic/hoare.v
-theories/program_logic/language.v
 theories/program_logic/ectx_language.v
 theories/program_logic/ectxi_language.v
 theories/program_logic/ectx_lifting.v
-theories/program_logic/ownp.v
-theories/program_logic/total_lifting.v
-theories/program_logic/total_ectx_lifting.v
-theories/program_logic/atomic.v
+theories/program_logic/refinement/ref_source.v
+theories/program_logic/refinement/ref_weakestpre.v
+theories/program_logic/refinement/ref_adequacy.v
+theories/program_logic/refinement/tc_weakestpre.v
+theories/program_logic/refinement/seq_weakestpre.v
+theories/program_logic/refinement/ref_lifting.v
+theories/program_logic/refinement/ref_ectx_lifting.v
 theories/heap_lang/locations.v
 theories/heap_lang/lang.v
 theories/heap_lang/metatheory.v
@@ -103,19 +108,6 @@ theories/heap_lang/lifting.v
 theories/heap_lang/notation.v
 theories/heap_lang/proofmode.v
 theories/heap_lang/adequacy.v
-theories/heap_lang/total_adequacy.v
-theories/heap_lang/lib/spawn.v
-theories/heap_lang/lib/par.v
-theories/heap_lang/lib/assert.v
-theories/heap_lang/lib/lock.v
-theories/heap_lang/lib/spin_lock.v
-theories/heap_lang/lib/ticket_lock.v
-theories/heap_lang/lib/nondet_bool.v
-theories/heap_lang/lib/lazy_coin.v
-theories/heap_lang/lib/clairvoyant_coin.v
-theories/heap_lang/lib/counter.v
-theories/heap_lang/lib/atomic_heap.v
-theories/heap_lang/lib/increment.v
 theories/proofmode/base.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v
@@ -131,6 +123,49 @@ theories/proofmode/classes.v
 theories/proofmode/class_instances_bi.v
 theories/proofmode/class_instances_sbi.v
 theories/proofmode/frame_instances.v
-theories/proofmode/monpred.v
 theories/proofmode/modalities.v
 theories/proofmode/modality_instances.v
+
+#################
+### Examples
+#################
+
+# General Transfinite Iris
+theories/examples/transfinite.v
+
+# derived Hoare triples
+theories/examples/refinements/derived.v
+
+# key ideas
+theories/examples/keyideas/simulations.v
+theories/examples/keyideas/generalized_simulations.v
+
+# Existing Safety Examples
+theories/examples/safety/spawn.v
+theories/examples/safety/par.v
+theories/examples/safety/assert.v
+theories/examples/safety/lock.v
+theories/examples/safety/spin_lock.v
+theories/examples/safety/ticket_lock.v
+theories/examples/safety/nondet_bool.v
+theories/examples/safety/counter.v
+theories/examples/safety/lazy_coin.v
+theories/examples/safety/clairvoyant_coin.v 
+
+theories/examples/safety/barrier/barrier.v
+theories/examples/safety/barrier/proof.v
+theories/examples/safety/barrier/specification.v
+theories/examples/safety/barrier/example_client.v
+
+# Termination Proofs
+theories/examples/termination/adequacy.v
+theories/examples/termination/thunk.v
+theories/examples/termination/eventloop.v
+theories/examples/termination/logrel.v
+
+# Termination Preserving Refinement
+theories/examples/refinements/refinement.v
+theories/examples/refinements/memoization.v
+
+# Some formalised counterexamples
+theories/examples/counterexamples.v
--- a/opam
+++ b/opam
-opam-version: "1.2"
+opam-version: "2.0"
 name: "coq-iris"
-synopsis: "This is the Coq development of the Iris Project"
 maintainer: "Ralf Jung <jung@mpi-sws.org>"
 authors: "The Iris Team"
-homepage: "http://iris-project.org/"
-bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
 license: "BSD"
-dev-repo: "https://gitlab.mpi-sws.org/iris/iris.git"
-build: [make "-j%{jobs}%"]
-install: [make "install"]
-remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+
+synopsis: "This is the Coq development of the Iris Project"
+
 depends: [
-  "coq" { (= "8.7.2") | (= "8.8.2") | (>= "8.9" & < "8.11~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2019-07-08.0.2e0bf441") | (= "dev") }
+  "coq" { (= "8.10.2") }
+  "coq-stdpp" { (= "1.3.0") }
 ]
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -51,17 +51,17 @@ Qed.

 Section agree.
 Local Set Default Proof Using "Type".
-Context {A : ofeT}.
+Context {SI} {A : ofeT SI}.
 Implicit Types a b : A.
 Implicit Types x y : agree A.

 (* OFE *)
-Instance agree_dist : Dist (agree A) := λ n x y,
+Instance agree_dist : Dist SI (agree A) := λ n x y,
  (∀ a, a ∈ agree_car x → ∃ b, b ∈ agree_car y ∧ a ≡{n}≡ b) ∧
  (∀ b, b ∈ agree_car y → ∃ a, a ∈ agree_car x ∧ a ≡{n}≡ b).
 Instance agree_equiv : Equiv (agree A) := λ x y, ∀ n, x ≡{n}≡ y.

-Definition agree_ofe_mixin : OfeMixin (agree A).
+Definition agree_ofe_mixin : OfeMixin SI (agree A).
 Proof.
  split.
  - done.
@@ -73,14 +73,14 @@ Proof.
        destruct (H2 b) as (c&?&?); eauto. by exists c; split; last etrans.
      * intros a ?. destruct (H2' a) as (b&?&?); auto.