CHANGELOG.md

In this changelog, we document "large-ish" changes to Iris that affect even the way the logic is used on paper. We also document changes in the Coq development; every API-breaking change should be listed, but not every new lemma.

Iris master

Changes in bi:

• Rename least_fixpoint_ind into least_fixpoint_iter, rename greatest_fixpoint_coind into greatest_fixpoint_coiter, rename least_fixpoint_strong_ind into least_fixpoint_ind, add lemmas least_fixpoint_{ind_wf, ne', strong_mono}, and add lemmas greatest_fixpoint_{coind, paco, ne', strong_mono}.

The following sed script helps adjust your code to the renaming (on macOS, replace sed by gsed, installed via e.g. brew install gnu-sed). Note that the script is not idempotent, do not run it twice.

sed -i -E -f- $(find theories -name "*.v") <<EOF
# least/greatest fixpoint renames
s/\bleast_fixpoint_ind\b/least_fixpoint_iter/g
s/\bgreatest_fixpoint_coind\b/greatest_fixpoint_coiter/g
s/\bleast_fixpoint_strong_ind\b/least_fixpoint_ind/g
EOF

Iris 3.5.0 (2021-11-05)

The highlights and most notable changes of this release are:

• Coq 8.14 is now supported, while Coq 8.12 and Coq 8.13 remain supported.
• The proof mode now has native support for pure names %H in intro patterns, without installing iris/string-ident. If you had the plugin installed, to migrate simply uninstall the plugin and stop importing it.
• The proof mode now supports destructing existentials with the "[%x ...]" pattern.
• iMod and iModIntro now report an error message for mask mismatches.
• Performance improvements for the proof mode in iFrame in non-affine logics, iPoseProof, and iDestruct (by Paolo G. Giarrusso, Bedrock Systems, and Armaël Guéneau).
• The new ghost_map logic-level library supports a ghost gmap K V with an authoritative view and per-element points-to facts written k ↪[γ] w.
• Weakest preconditions now support a flexible number of laters per physical step of the operational semantics. See merge request !585 (by Jacques-Henri Jourdan and Yusuke Matsushita).
• HeapLang now has an atomic Xchg (exchange) operation (by Simon Hudon, Google).

This release was managed by Ralf Jung, Robbert Krebbers, and Tej Chajed, with contributions from Amin Timany, Armaël Guéneau, Dan Frumin, Dmitry Khalanskiy, Hoang-Hai Dang, Jacques-Henri Jourdan, Lennard Gäher, Michael Sammler, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Friis Vindum, Simon Hudon, Tej Chajed, and Yusuke Matsushita. Thanks a lot to everyone involved!

Changes in algebra:

• Generalize the authorative elements of the view, auth and gset_bij cameras to be parameterized by a discardable fraction (dfrac) instead of a fraction (frac). Normal fractions are now denoted ●{#q} a and ●V{#q} a. Lemmas affected by this have been renamed such that the "frac" in their name has been changed into "dfrac". (by Simon Friis Vindum)
• Generalize namespace_map to reservation_map which enhances gmap positive A with a notion of 'tokens' that enable allocating a particular name in the map. See algebra.reservation_map for further information.
• Add dyn_reservation_map which further extends reservation_map with the ability to dynamically allocate an infinite set of tokens. This is useful to perform synchronized allocation of the same name in two maps/APIs without dedicated support from one of the involved maps/APIs. See algebra.dyn_reservation_map for further information.
• Demote the Camera structure on list to iris_staging since its composition is not very well-behaved.
• Extend gmap_view with lemmas for "big" operations on maps.
• Typeclasses instances triggering a canonical structure search such as Equiv, Dist, Op, Valid, ValidN, Unit, PCore now use an Hint Extern based on refine instead of apply, in order to use Coq's newer unification algorithm.
• Set Hint Mode for the classes OfeDiscrete, Dist, Unit, CmraMorphism, rFunctorContractive, urFunctorContractive.
• Set Hint Mode for the stdpp class Equiv. This might require few spurious type annotations until Coq bug #14441 is fixed.
• Add max_prefix_list RA on lists whose composition is only defined when one operand is a prefix of the other. The result is the longer list.
• Add NonExpansive instances for curry and friends.

Changes in bi:

• Add new lemmas big_sepM2_delete_l and big_sepM2_delete_r.
• Rename big_sepM2_lookup_1 → big_sepM2_lookup_l and big_sepM2_lookup_2 → big_sepM2_lookup_r.
• Add lemmas for swapping nested big-ops: big_sep{L,M,S,MS}_sep{L,M,S,MS}.
• Rename big_sep{L,L2,M,M2,S}_intuitionistically_forall → big_sep{L,L2,M,M2,S}_intro, and big_orL_lookup → big_orL_intro.
• Rename bupd_forall to bupd_plain_forall, and add {bupd,fupd}_{and,or,forall,exist}.
• Decouple Wp and Twp typeclasses from the program_logic.language interface. The typeclasses are now parameterized over an expression and a value type, instead of a language. This requires extra type annotations or explicit coercions in a few cases, in particular WP v {{ Φ }} must now be written WP (of_val v) {{ Φ }}.
• Improve make_laterable:
  • Adjust definition such that Laterable P iff P ⊢ make_laterable P. As a consequence, make_laterable_elim got weaker: elimination now requires an except-0 modality (make_laterable P -∗ ◇ P).
  • Add iModIntro support for make_laterable.
• Improvements to BiMonoPred:
  • Use □/-∗ instead of <pers>/→.
  • Strengthen to ensure that functions for recursive calls are non-expansive.
• Add big_andM (big conjunction on finite maps) with lemmas similar to big_andL.
• Add transitive embedding that constructs an embedding of PROP1 into PROP3 by combining the embeddings of PROP1 into PROP2 and PROP2 into PROP3. This construct is not declared as an instance to avoid TC search divergence. (by Hai Dang, BedRock Systems)
• Improve notation printing around magic wands, view shifts, WP, Texan triples, and logically atomic triples.
• Slight change to the AACC notation for atomic accessors (which is usually only printed, not parsed): added a , before ABORT, for consistency with COMM.
• Add the lemmas big_sepM_impl_strong and big_sepM_impl_dom_subseteq that generalize the existing big_sepM_impl lemma. (by Simon Friis Vindum)
• Add new instance fractional_big_sepL2. (by Paolo G. Giarrusso, BedRock Systems)

Changes in proofmode:

• Add support for pure names %H in intro patterns. This is now natively supported whereas the previous experimental support required installing https://gitlab.mpi-sws.org/iris/string-ident. (by Tej Chajed)
• Add support for destructing existentials with the intro pattern [%x ...]. (by Tej Chajed)
• iMod/iModIntro show proper error messages when they fail due to mask mismatches. To support this, the proofmode typeclass FromModal now takes an additional pure precondition.
• Fix performance of iFrame in logics without BiAffine. To adjust your code if you use such logics and define Frame instances, ensure these instances to have priority at least 2: they should have either at least 2 (non-dependent) premises, or an explicit priority. References: docs for frame_here_absorbing in iris/proofmode/frame_instances.v and https://coq.inria.fr/refman/addendum/type-classes.html#coq:cmd.Instance. (by Paolo G. Giarrusso, BedRock Systems)
• Rename the main entry point module for the proofmode from iris.proofmode.tactics to iris.proofmode.proofmode. Under normal circumstances, this should be the only proofmode file you need to import.
• Improve performance of the iIntoEmpValid tactic used by iPoseProof, especially in the case of large goals and lemmas with many forall quantifiers. (by Armaël Guéneau)
• Improve performance of the iDestruct tactic, by using user-provided names more eagerly in order to avoid later calls to iRename. (by Armaël Guéneau)

Changes in bi:

• Add lemmas characterizing big-ops over pure predicates (big_sep*_pure*).
• Move BiAffine, BiPositive, BiLöb, and BiPureForall from bi.derived_connectives to bi.extensions.
• Strengthen persistent_fractional to support propositions that are persistent and either affine or absorbing. (by Paolo G. Giarrusso, BedRock Systems)

Changes in base_logic:

• Add ghost_map, a logic-level library for a gmap K V with an authoritative view and per-element points-to facts written k ↪[γ] w.
• Generalize the soundness lemma of the base logic step_fupdN_soundness. It applies even if invariants stay open accross an arbitrary number of laters. (by Jacques-Henri Jourdan)
• Rename those *G typeclasses that must be global singletons to *GS, and their corresponding preG class to GpreS. Affects invG, irisG, gen_heapG, inv_heapG, proph_mapG, ownPG, heapG.