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:

• Generalize big_op lemmas that were previously assuming Absorbingness of some assertion: they now take any of (TCOr) an Affine instance or an Absorbing instance. This breaks uses where an Absorbing instance was provided without relying on TC search (e.g. in by apply ...; a possible fix is by apply: ...). (by Glen Mével, Bedrock Systems)

Changes in proofmode:

• iAssumption no longer instantiates evar premises with False. This used to occur when the conclusion contains variables that are not in scope of the evar, thus blocking the default behavior of instantiating the premise with the conclusion. The old behavior can be emulated withiExFalso. iExact "H".
• iInduction now supports induction schemes that involve Forall and Forall2 (for example, for trees with finite branching).

Changes in base_logic:

• Make the inG instances for libG fields local, so they are only used inside the library that defines the libG.

Iris 3.6.0 (2022-01-22)

The highlights and most notable changes of this release are:

• Coq 8.15 is now supported, while Coq 8.13 and Coq 8.14 remain supported. Coq 8.12 is no longer supported.
• Support for discardable fractions (dfrac) has been added to gmap_view authoritative elements, and to the mono_nat library. See below for other dfrac-related changes.
• A new mono_list algebra provides monotonically growing lists with an exclusive authoritative element and persistent prefix witnesses. See iris/algebra/lib/mono_list.v for details. An experimental logic-level library wrapping the algebra is available at iris_staging/base_logic/mono_list.v; if you use it, please give feedback on the tracking issue iris/iris#439.

This release was managed by Ralf Jung, Robbert Krebbers, and Tej Chajed, with contributions from Dan Frumin, Jonas Kastberg Hinrichsen, Lennard Gäher, Matthieu Sozeau, Michael Sammler, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Friis Vindum, Tej Chajed, and Vincent Siles. Thanks a lot to everyone involved!

Changes in algebra

• Define non-expansive instance for dom. This, in particular, makes it possible to iRewrite below dom (even if the dom appears in ⌜ _ ⌝).
• Generalize the authorative elements of gmap_view to be parameterized by a discardable fraction (dfrac) instead of a fraction (frac). Lemmas affected by this have been renamed such that the "frac" in their name has been changed into "dfrac". (by Simon Friis Vindum)
• Change ufrac_auth notation to not use curly braces, since these fractions do not behave like regular fractions (and cannot be made dfrac). Old: ●U{q} a, ◯U{q} b; new: ●U_q a, ◯U_q b.
• Equip frac_agree with support for dfrac and rename it to dfrac_agree. The old to_frac_agree and its lemmas still exist, except that the frac_agree_op_valid lemmas are made bi-directional.
• Rename typeclass instance Later_inj -> Next_inj.
• Remove view_auth_frac_op, auth_auth_frac_op, gmap_view_auth_frac_op; the corresponding dfrac lemmas can be used instead (together with dfrac_op_own if needed).
• Equip mono_nat algebra with support for dfrac, make API more consistent, and add notation for algebra elements. See iris/algebra/lib/mono_nat.v for details. This affects some existing terms and lemmas:
  • mono_nat_auth now takes a dfrac, but the recommendation is to port to the notation.
  • mono_nat_lb_op: direction of equality is swapped.
  • mono_nat_auth_frac_op, mono_nat_auth_frac_op_valid, mono_nat_auth_frac_valid, mono_nat_both_frac_valid: use dfrac variant instead.
• Add mono_list algebra for monotonically growing lists with an exclusive authoritative element and persistent prefix witnesses. See iris/algebra/lib/mono_list.v for details.

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}.
• Move persistently_forall_2 (∀ <pers> ⊢ <pers> ∀) out of the BI interface into a new typeclass, BiPersistentlyForall. The BI interface instead just demands the equivalent property for conjunction ((<pers> P) ∧ (<pers> Q) ⊢ <pers> (P ∧ Q)). This enables the IPM to support logics where the persistently modality is defined with an existential quantifier. This also necessitates removing persistently_impl_plainly from BiPlainly into a new typeclass BiPersistentlyImplPlainly. Proofs that are generic in PROP might have to add those new classes as assumptions to remain compatible, and code that instantiates the BI interface needs to provide instances for the new classes.
• Make frame_fractional not an instance any more; instead fractional propositions that want to support framing are expected to register an appropriate instance themselves. HeapLang and gen_heap ↦ still support framing, but the other fractional propositions in Iris do not.

Changes in heap_lang:

• The is_closed_expr predicate is formulated in terms of a set of binders (as opposed to a list of binders).

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
# gmap_view renames from frac to dfrac
s/\bgmap_view_(auth|both)_frac_(op_invN|op_inv|op_inv_L|valid|op_validN|op_valid|op_valid_L)\b/gmap_view_\1_dfrac_\2/g
s/\bgmap_view_persist\b/gmap_view_frag_persist/g
# frac_agree with dfrac
s/\bfrac_agreeR\b/dfrac_agreeR/g
EOF