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

Coq 8.11 is no longer supported in this version of Iris.

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".
• 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.

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.
• Add support for destructing existentials with the intro pattern [%x ...].

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.

Changes in program_logic:

• Change definition of weakest precondition to use a variable number of laters (i.e., logical steps) for each physical step of the operational semantics, depending on the number of physical steps executed since the begining of the execution of the program. See merge request !595. This implies several API-breaking changes, which can be easily fixed in client formalizations in a backward compatible manner as follows:
  • Ignore the new parameter ns in the state interpretation, which corresponds to a step counter.
  • Use the constant function "0" for the new field num_laters_per_step of irisG.
  • Use fupd_intro _ _ for the new field state_interp_mono of irisG.
  • Some proofs using lifting lemmas and adequacy theorems need to be adapted to ignore the new step counter.
• Remove wp_frame_wand_l; add wp_frame_wand as more symmetric replacement.

Changes in heap_lang:

• Rename Build_loc constructor for loc type to Loc.

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
# auth and view renames from frac to dfrac
s/\b(auth|view)_(auth|both|update)_frac_(is_op|op_invN|op_inv|inv_L|validN|op_validN|valid|op_valid|valid_2|valid_discrete|includedN|included|alloc|validI|validI_2|validI_1|validI|)\b/\1_\2_dfrac_\3/g
s/\bgset_bij_auth_frac_(\w*)\b/gset_bij_auth_dfrac_\1/g
s/\bgset_bij_auth_empty_frac_valid\b/gset_bij_auth_empty_dfrac_valid/g
s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
EOF

Iris 3.4.0

The highlights and most notable changes of this release are as follows:

• Coq 8.13 is now supported; the old Coq 8.9 and Coq 8.10 are not supported any more.
• The new view RA construction generalizes auth to user-defined abstraction relations. (thanks to Gregory Malecha for the inspiration)
• The new dfrac RA extends frac (fractions 0 < q ≤ 1) with support for "discarding" some part of the fraction in exchange for a persistent witness that discarding has happened. This can be used to easily generalize fractional permissions with support for persistently owning "any part" of the resource. (by Simon Friis Vindum)
• The new gmap_view RA provides convenient lemmas for ghost ownership of heap-like structures with an "authoritative" view. Thanks to dfrac, it supports both exclusive (mutable) and persistent (immutable) ownership of individual map elements.
• With this release we are beginning to provide logic-level abstractions for ghost state, which have the advantage that the user does not have to directly interact with RAs to use them.
  • ghost_var provides a logic-level abstraction of ghost variables: a mutable "variable" with fractional ownership.
  • mono_nat provides a "monotone counter" with a persistent witnesses representing a lower bound of the current counter value. (by Tej Chajed)
  • gset_bij provides a monotonically growing partial bijection; this is useful in particular when building binary logical relations for languages with a heap.
• HeapLang provides a persistent read-only points-to assertion l ↦□ v. (by Simon Friis Vindum)
• We split Iris into multiple opam packages: coq-iris no longer contains HeapLang, which is now in a separate package coq-iris-heap-lang. The two packages coq-iris-deprecated (for old modules that we eventually plan to remove entirely) and coq-iris-staging (for new modules that are not yet ready for prime time) exist only as development versions, so they are not part of this release.
• The proofmode now does a better job at picking reasonable names when moving variables into the Coq context without a name being explicitly given by the user. However, the exact variable names remain unspecified. (by Tej Chajed)

Further details are given in the changelog below.

This release of Iris was managed by Ralf Jung and Robbert Krebbers, with contributions by Arthur Azevedo de Amorim, Dan Frumin, Enrico Tassi, Hai Dang, Michael Sammler, Paolo G. Giarrusso, Rodolphe Lepigre, Simon Friis Vindum, Tej Chajed, and Yusuke Matsushita. Thanks a lot to everyone involved!