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

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.

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