From 3c16b4ebaeca585ae176aa0ed0b0131dcfd94228 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 3 Aug 2022 13:59:53 -0400
Subject: [PATCH] changelog
---
CHANGELOG.md | 53 +++++++++++++++++++++++++++-------------------------
1 file changed, 28 insertions(+), 25 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 89bc4ab23..a5783e424 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -71,14 +71,19 @@ lemma.
* Prepare for supporting later credits, by adding a resource `£ n` describing
ownership of `n` credits that can be eliminated at fancy updates.
Note that HeapLang has not yet been equipped with support for later credits.
- To retain backwards compatibility with the interaction laws of fancy updates
- with the plainly modality (`BiFUpdPlainly`), which are incompatible with
- later credits, the logic is parameterized by two typeclasses, `HasLc`
- and `HasNoLc`, that allow opting for either later credits or `BiFUpdPlainly`.
- The soundness lemmas for the fancy update modality are available in two versions,
- with later credits (suffix `_lc`) and without later credits (suffix `_no_lc`).
- The lemmas without later credits still generate credits, but they cannot be used
- in any meaningful way. The lemma `step_fupdN_soundness_gen` is generic over this choice.
+ + To retain backwards compatibility with the interaction laws of fancy updates
+ with the plainly modality (`BiFUpdPlainly`), which are incompatible with
+ later credits, the logic has a new parameter of type `has_lc`, which is
+ either `HasLc` or `HasNoLc`. The parameter is an index of the `invGS_gen`
+ typeclass; the old `invGS` is an alias for `invGS_gen HasLc` so that
+ developments default to having later credits available. Libraries that want
+ to be generic over whether credits are available or not, and proofs that
+ need `BiFUpdPlainly`, need to be changed to use `invGS_gen` rather than
+ `invGS`.
+ + The core soundness lemma `step_fupdN_soundness_gen` similarly takes a `has_lc`
+ parameter to control how the logic is supposed to be instantiated. The lemma
+ always generates credits, but they cannot be used in any meaningful way unless
+ `HasLc` is picked.
* Add discardable fractions `dfrac` to `saved_anything_own`, `saved_prop_own`,
and `saved_pred_own`, so they can be updated. The previous persistent versions
can be recovered with the fraction `DfracDiscarded`. Allocation lemmas now take
@@ -96,17 +101,16 @@ lemma.
+ All lifting lemmas have been altered to provide credits.
`wp_lift_step_fupdN` provides `S (num_laters_per_step ns)` credits, while all other
lemmas always provide one credit.
-* In line with the support for later credits (see `base_logic`), the adequacy statements
- have been changed to account for `HasLc` and `HasNoLc`:
- + The lemma `twp_total` (total adequacy) provides an additional assumption `HasNoLc`.
- Clients of the adequacy proof will need to introduce this additional assumption and
- keep it around in case `BiFUpdPlainly` is used.
+* In line with the support for later credits (see `base_logic`), `irisGS_gen`
+ now also has a `has_lc` parameter and the adequacy statements have been
+ changed to account for that:
+ + The lemma `twp_total` (total adequacy) provides `irisGS_gen HasNoLc`. Clients
+ of the adequacy proof will need to make sure to be either generic over the
+ choice of `has_lc` or explicitly opt-out of later credits.
+ The adequacy lemmas for the partial WP, in particular `wp_adequacy`,
- `wp_strong_adequacy` and `wp_invariance`, are now available in two flavors,
- one providing `HasLc` to enable the use of later credits in the future (suffix `_lc`),
- and one without support for later credits, providing `HasNoLc` (suffix `_no_lc`).
- Clients of the adequacy proof will need to opt for either of these and introduce
- the additional assumptions.
+ `wp_strong_adequacy` and `wp_invariance`, are now available in two flavors:
+ the old names generate `irisGS` (a short-hand for `irisGS_gen HasLc`); new
+ lemmas with a `_gen` suffix leave the choice of `has_lc` to the user.
+ The parameter for the stuckness bit `s` in `wp_strong_adequacy{_lc, _no_lc}` has
moved up and is now universally quantified in the lemma instead of being existentially
quantified at the Iris-level. For clients that already previously quantified over `s`
@@ -120,14 +124,13 @@ lemma.
number of steps taken so far. This number is tied to ghost state in the state
interpretation, which is exposed, updated, and used with new lemmas
`wp_lb_init`, `wp_lb_update`, and `wp_step_fupdN_lb`. (by Jonas Kastberg Hinrichsen)
-* In line with the support for later credits (see `base_logic`), the adequacy statements
- for HeapLang have been changed:
- + `heap_adequacy` provides the additional assumption `HasLc`, which needs to be
- introduced by clients and will enable using new proof rules for later credits
- in the future.
+* In line with the support for later credits (see `base_logic`), `heapGS_gen`
+ now takes an additional `has_lc` parameter, and `heapGS` is a short-hand for
+ `heapGS_gen HasLc`. The adequacy statements for HeapLang have been changed
+ accordingly:
+ + `heap_adequacy` provides `heapGS`, thus enabling the use of later credits.
This precludes usage of the laws in `BiFUpdPlainly` in the HeapLang instance of Iris.
- + `heap_total` provides the additional assumption `HasNoLc`, which needs to be
- introduced by clients and needs to be kept around to use the laws in `BiFUpdPlainly`.
+ + `heap_total` provides `heapGS_gen HasNoLc`.
Currently, the primitive laws for HeapLang do not yet provide later credits.
The following `sed` script helps adjust your code to the renaming (on macOS,
--
GitLab