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". (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.
• State bi_mono_pred using □/-∗ instead of <pers>/→.

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.

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.

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. (by Jacques-Henri Jourdan)
• Remove wp_frame_wand_l; add wp_frame_wand as more symmetric replacement.
• Swap the polarity of the mask in logically atomic triples, so that it matches regular WP masks.

Changes in heap_lang:

• Rename Build_loc constructor for loc type to Loc.
• Add atomic Xchg ("exchange"/"swap") operation. (by Simon Hudon, Google LLC)

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
# big_sepM renames
s/\bbig_sepM2_lookup_1\b/big_sepM2_lookup_l/g
s/\bbig_sepM2_lookup_2\b/big_sepM2_lookup_r/g
# big_*_intro
s/\bbig_sep(L|L2|M|M2|S)_intuitionistically_forall\b/big_sep\1_intro/g
s/\bbig_orL_lookup\b/big_orL_intro/g
s/\bbupd_forall\b/bupd_plain_forall/g
# "global singleton" rename
s/\b(inv|iris|(gen|inv)_heap|(Gen|Inv)Heap|proph_map|ProphMap|[oO]wnP|[hH]eap)G\b/\1GS/g
s/\b([iI]nv|iris|(gen|inv)_heap|(Gen|Inv)Heap|proph_map|ProphMap|[oO]wnP|[hH]eap)PreG\b/\1GpreS/g
EOF

Iris 3.4.0 (released 2021-02-16)