CHANGELOG.md 76.5 KB
 Ralf Jung committed Jul 25, 2016 1 ``````In this changelog, we document "large-ish" changes to Iris that affect even the `````` Ralf Jung committed Jul 14, 2020 2 3 4 ``````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. `````` Ralf Jung committed Aug 08, 2016 5 `````` `````` Janno committed Jan 24, 2022 6 7 ``````## Iris master `````` Glen Mével committed Jan 27, 2022 8 9 10 11 12 13 ``````**Changes in `bi`:** * Generalize `big_op` lemmas that were previously assuming `Absorbing`ness 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 `````` Glen Mével committed Feb 01, 2022 14 `````` is `by apply: ...`). (by Glen Mével, Bedrock Systems) `````` Glen Mével committed Jan 27, 2022 15 `````` `````` Janno committed Jan 24, 2022 16 17 18 19 20 21 ``````**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 with`iExFalso. iExact "H".` `````` Robbert Krebbers committed Feb 02, 2022 22 23 ``````* `iInduction` now supports induction schemes that involve `Forall` and `Forall2` (for example, for trees with finite branching). `````` Robbert Krebbers committed Apr 23, 2022 24 ``````* `iRevert` of a pure hypothesis generates a wand instead of an implication. `````` Janno committed Jan 24, 2022 25 `````` `````` Ralf Jung committed Mar 21, 2022 26 27 28 29 30 ``````**Changes in `base_logic`:** * Make the `inG` instances for `libG` fields local, so they are only used inside the library that defines the `libG`. `````` Jonas Kastberg committed Apr 10, 2022 31 32 33 34 35 36 37 38 ``````**Changes in `iris_heap_lang`:** * Changed the `num_laters_per_step` of `heap_lang` to `λ n, n`, signifying that each step of the weakest precondition strips `n` laters, where `n` is the 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) `````` Tej Chajed committed Jan 23, 2022 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 ``````## 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](https://gitlab.mpi-sws.org/iris/iris/-/issues/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! `````` Simon Friis Vindum committed Feb 23, 2021 61 `````` `````` Robbert Krebbers committed Nov 16, 2021 62 63 64 65 ``````**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 `⌜ _ ⌝`). `````` Ralf Jung committed Nov 22, 2021 66 67 68 69 ``````* Generalize the authorative elements of `gmap_view` to be parameterized by a [discardable fraction](iris/algebra/dfrac.v) (`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) `````` Ralf Jung committed Dec 16, 2021 70 71 72 ``````* 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`. `````` Ralf Jung committed Dec 16, 2021 73 74 75 ``````* 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. `````` Dan Frumin committed Dec 30, 2021 76 ``````* Rename typeclass instance `Later_inj` -> `Next_inj`. `````` Ralf Jung committed Jan 14, 2022 77 78 79 ``````* 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). `````` Ralf Jung committed Jan 16, 2022 80 81 82 83 84 85 86 87 ``````* 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. `````` Ralf Jung committed Jan 17, 2022 88 89 90 ``````* 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. `````` Robbert Krebbers committed Nov 16, 2021 91 `````` `````` Lennard Gäher committed Nov 06, 2021 92 ``````**Changes in `bi`:** `````` Ralf Jung committed Nov 08, 2021 93 `````` `````` Lennard Gäher committed Nov 06, 2021 94 95 96 97 98 ``````* 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}`. `````` Ralf Jung committed Nov 08, 2021 99 100 101 102 103 104 105 106 107 ``````* Move `persistently_forall_2` (`∀ ∀`) out of the BI interface into a new typeclass, `BiPersistentlyForall`. The BI interface instead just demands the equivalent property for conjunction (`( P) ∧ ( Q) ⊢ (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 `````` Robbert Krebbers committed Nov 08, 2021 108 `````` needs to provide instances for the new classes. `````` Ralf Jung committed Jan 16, 2022 109 110 111 112 ``````* 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. `````` Lennard Gäher committed Nov 06, 2021 113 `````` `````` Dan Frumin committed Jan 11, 2022 114 115 116 117 118 ``````**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). `````` Lennard Gäher committed Nov 06, 2021 119 120 121 122 123 124 125 126 127 ``````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") <`/`→`. - Strengthen to ensure that functions for recursive calls are non-expansive. `````` Ralf Jung committed Jul 26, 2021 223 ``````* Add `big_andM` (big conjunction on finite maps) with lemmas similar to `big_andL`. `````` Hai Dang committed Jul 26, 2021 224 225 226 ``````* Add transitive embedding that constructs an embedding of `PROP1` into `PROP3` by combining the embeddings of `PROP1` into `PROP2` and `PROP2` into `PROP3`. This construct is *not* declared as an instance to avoid TC search divergence. `````` Ralf Jung committed Jul 26, 2021 227 `````` (by Hai Dang, BedRock Systems) `````` Ralf Jung committed Sep 04, 2021 228 229 ``````* Improve notation printing around magic wands, view shifts, `WP`, Texan triples, and logically atomic triples. `````` Ralf Jung committed Jul 28, 2021 230 231 ``````* Slight change to the `AACC` notation for atomic accessors (which is usually only printed, not parsed): added a `,` before `ABORT`, for consistency with `COMM`. `````` Simon Friis Vindum committed Jul 30, 2021 232 ``````* Add the lemmas `big_sepM_impl_strong` and `big_sepM_impl_dom_subseteq` that `````` Simon Friis Vindum committed Jul 30, 2021 233 `````` generalize the existing `big_sepM_impl` lemma. (by Simon Friis Vindum) `````` Paolo G. Giarrusso committed Oct 26, 2021 234 ``````* Add new instance `fractional_big_sepL2`. (by Paolo G. Giarrusso, BedRock Systems) `````` Robbert Krebbers committed May 25, 2021 235 `````` `````` Ralf Jung committed Mar 24, 2021 236 ``````**Changes in `proofmode`:** `````` Ralf Jung committed Mar 24, 2021 237 238 239 `````` * Add support for pure names `%H` in intro patterns. This is now natively supported whereas the previous experimental support required installing `````` Ralf Jung committed May 19, 2021 240 `````` https://gitlab.mpi-sws.org/iris/string-ident. (by Tej Chajed) `````` Ralf Jung committed Mar 24, 2021 241 ``````* Add support for destructing existentials with the intro pattern `[%x ...]`. `````` Ralf Jung committed May 19, 2021 242 `````` (by Tej Chajed) `````` Ralf Jung committed May 26, 2021 243 ``````* `iMod`/`iModIntro` show proper error messages when they fail due to mask `````` Ralf Jung committed Jun 06, 2021 244 245 `````` mismatches. To support this, the proofmode typeclass `FromModal` now takes an additional pure precondition. `````` Paolo G. Giarrusso committed Jul 25, 2021 246 247 248 249 ``````* Fix performance of `iFrame` in logics without `BiAffine`. To adjust your code if you use such logics and define `Frame` instances, ensure these instances to have priority at least 2: they should have either at least 2 (non-dependent) premises, or an explicit priority. `````` Robbert Krebbers committed Jul 25, 2021 250 251 `````` References: docs for `frame_here_absorbing` in [iris/proofmode/frame_instances.v](iris/proofmode/frame_instances.v) and `````` Paolo G. Giarrusso committed Jul 25, 2021 252 253 `````` https://coq.inria.fr/refman/addendum/type-classes.html#coq:cmd.Instance. (by Paolo G. Giarrusso, BedRock Systems) `````` Ralf Jung committed Jul 26, 2021 254 255 256 ``````* Rename the main entry point module for the proofmode from `iris.proofmode.tactics` to `iris.proofmode.proofmode`. Under normal circumstances, this should be the only proofmode file you need to import. `````` Armaël Guéneau committed Sep 06, 2021 257 ``````* Improve performance of the `iIntoEmpValid` tactic used by `iPoseProof`, `````` Ralf Jung committed Sep 06, 2021 258 `````` especially in the case of large goals and lemmas with many forall quantifiers. `````` Armaël Guéneau committed Sep 06, 2021 259 `````` (by Armaël Guéneau) `````` Armaël Guéneau committed Oct 01, 2021 260 261 262 ``````* Improve performance of the `iDestruct` tactic, by using user-provided names more eagerly in order to avoid later calls to `iRename`. (by Armaël Guéneau) `````` Ralf Jung committed Mar 24, 2021 263 `````` `````` Ralf Jung committed May 26, 2021 264 265 266 ``````**Changes in `bi`:** * Add lemmas characterizing big-ops over pure predicates (`big_sep*_pure*`). `````` Ralf Jung committed Jun 07, 2021 267 268 ``````* Move `BiAffine`, `BiPositive`, `BiLöb`, and `BiPureForall` from `bi.derived_connectives` to `bi.extensions`. `````` Paolo G. Giarrusso committed Jul 18, 2021 269 ``````* Strengthen `persistent_fractional` to support propositions that are persistent `````` Ralf Jung committed Jul 18, 2021 270 `````` and either affine or absorbing. (by Paolo G. Giarrusso, BedRock Systems) `````` Ralf Jung committed May 26, 2021 271 `````` `````` Ralf Jung committed Mar 05, 2021 272 273 274 275 ``````**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`. `````` Jacques-Henri Jourdan committed Mar 06, 2021 276 277 ``````* Generalize the soundness lemma of the base logic `step_fupdN_soundness`. It applies even if invariants stay open accross an arbitrary number of laters. `````` Ralf Jung committed May 19, 2021 278 `````` (by Jacques-Henri Jourdan) `````` Ralf Jung committed Jun 02, 2021 279 280 281 ``````* 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`. `````` 282 283 284 `````` **Changes in `program_logic`:** `````` Jacques-Henri Jourdan committed Mar 06, 2021 285 286 287 288 289 290 ``````* 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](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595). This implies several API-breaking changes, which can be easily fixed in client formalizations in a backward compatible manner as follows: `````` 291 292 293 294 295 296 297 `````` - 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. `````` Ralf Jung committed May 19, 2021 298 `````` (by Jacques-Henri Jourdan) `````` Ralf Jung committed May 11, 2021 299 ``````* Remove `wp_frame_wand_l`; add `wp_frame_wand` as more symmetric replacement. `````` Ralf Jung committed Jul 19, 2021 300 301 ``````* Swap the polarity of the mask in logically atomic triples, so that it matches regular `WP` masks. `````` Ralf Jung committed Sep 01, 2021 302 ``````* Rename `iris_invG` to `iris_invGS`. `````` 303 `````` `````` Ralf Jung committed Mar 18, 2021 304 305 306 ``````**Changes in `heap_lang`:** * Rename `Build_loc` constructor for `loc` type to `Loc`. `````` Ralf Jung committed May 19, 2021 307 ``````* Add atomic `Xchg` ("exchange"/"swap") operation. (by Simon Hudon, Google LLC) `````` Ralf Jung committed Mar 18, 2021 308 `````` `````` Ralf Jung committed Mar 06, 2021 309 310 311 312 313 ``````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") <` to get rid of the `fupd` in the goal if `E2 ⊆ E1`. The lemma `fupd_mask_weaken Enew` can be `iApply`ed to shrink the first mask to `Enew` without getting rid of the modality; the same effect can also be obtained slightly more conveniently by using `iMod` with `fupd_mask_subseteq Enew`. To make the new names work, rename some existing lemmas: `fupd_intro_mask` → `fupd_mask_intro_subseteq`, `fupd_intro_mask'` → `fupd_mask_subseteq` (implicit arguments also changed here), `fupd_mask_weaken` → `fupd_mask_intro_discard`. Remove `fupd_mask_same` since it was unused and obscure. In the `BiFUpd` axiomatization, rename `bi_fupd_mixin_fupd_intro_mask` to `bi_fupd_mixin_fupd_mask_subseteq` and weaken the lemma to be specifically about `emp` (the stronger version can be derived). `````` Ralf Jung committed Feb 16, 2021 477 478 479 480 481 482 483 484 485 486 487 488 ``````* Remove `bi.tactics` with tactics that predate the proofmode (and that have not been working properly for quite some time). * Strengthen `persistent_sep_dup` to support propositions that are persistent and either affine or absorbing. * Fix the statement of the lemma `fupd_plainly_laterN`; the old lemma was a duplicate of `fupd_plain_laterN`. * Strengthen `big_sepL2_app_inv` by weakening a premise (it is sufficient for one of the two pairs of lists to have equal length). * Rename `equiv_entails` → `equiv_entails_1_1`, `equiv_entails_sym` → `equiv_entails_1_2`, and `equiv_spec` → `equiv_entails`. * Remove the laws `pure_forall_2 : (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝` from the BI interface and factor it into a type class `BiPureForall`. `````` Ralf Jung committed Feb 16, 2021 489 `````` `````` Tej Chajed committed Jul 21, 2020 490 491 492 493 494 495 496 497 498 ``````**Changes in `proofmode`:** * The proofmode now preserves user-supplied names for existentials when using `iDestruct ... as (?) "..."`. This is backwards-incompatible if you were relying on the previous automatic names (which were always "H", possibly freshened). It also requires some changes if you were implementing `IntoExist` yourself, since the typeclass now forwards names. If your instance transforms one `IntoExist` into another, you can generally just forward the name from the premise. `````` Tej Chajed committed Jul 21, 2020 499 500 501 502 503 ``````* The proofmode also preserves user-supplied names in `iIntros`, for example with `iIntros (?)` and `iIntros "%"`, as described for destructing existentials above. As part of this change, it now uses a base name of `H` for pure facts rather than the previous default of `a`. This also requires some changes if you were implementing `FromForall`, in order to forward names. `````` Robbert Krebbers committed Sep 29, 2020 504 505 506 507 508 ``````* Make `iFrame` "less" smart w.r.t. clean up of modalities. It now consistently removes the modalities ``, ``, `` and `□` only if the result after framing is `True` or `emp`. In particular, it no longer removes `` if the result after framing is affine, and it no longer removes `□` if the result after framing is intuitionistic. `````` Robbert Krebbers committed Sep 29, 2020 509 510 511 ``````* Allow framing below an `` modality if the hypothesis that is framed is affine. (Previously, framing below `` was only possible if the hypothesis that is framed resides in the intuitionistic context.) `````` Robbert Krebbers committed Jan 07, 2021 512 513 ``````* Add Coq side-condition `φ` to class `ElimAcc` (similar to what we already had for `ElimInv` and `ElimModal`). `````` Rodolphe Lepigre committed Jan 27, 2021 514 515 ``````* Add a tactic `iSelect pat tac` (similar to `select` in std++) which runs the tactic `tac H` with the name `H` of the last hypothesis of the intuitionistic `````` Robbert Krebbers committed Feb 15, 2021 516 `````` or spatial context matching `pat`. The tactic `iSelect` is used to implement: `````` Rodolphe Lepigre committed Jan 27, 2021 517 518 519 520 521 `````` + `iRename select (pat)%I into name` which renames the matching hypothesis, + `iDestruct select (pat)%I as ...` which destructs the matching hypothesis, + `iClear select (pat)%I` which clears the matching hypothesis, + `iRevert select (pat)%I` which reverts the matching hypothesis, + `iFrame select (pat)%I` which cancels the matching hypothesis. `````` Tej Chajed committed Jul 21, 2020 522 `````` `````` Ralf Jung committed Sep 15, 2020 523 524 525 526 ``````**Changes in `base_logic`:** * Add a `ghost_var` library that provides (fractional) ownership of a ghost variable of arbitrary `Type`. `````` Ralf Jung committed Feb 16, 2021 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 ``````* Define a ghost state library on top of the `mono_nat` resource algebra. See [base_logic.lib.mono_nat](iris/base_logic/lib/mono_nat.v) for further information. * Define a ghost state library on top of the `gset_bij` resource algebra. See [base_logic.lib.gset_bij](iris/base_logic/lib/gset_bij.v) for further information. * Extend the `gen_heap` library with read-only points-to assertions using [discardable fractions](iris/algebra/dfrac.v). + The `mapsto` connective now takes a `dfrac` rather than a `frac` (i.e., positive rational number `Qp`). + The notation `l ↦{ dq } v` is generalized to discardable fractions `dq : dfrac`. + The new notation `l ↦{# q} v` is used for a concrete fraction `q : frac` (e.g., to enable writing `l ↦{# 1/2} v`). + The new notation `l ↦□ v` is used for the discarded fraction. This persistent proposition provides read-only access to `l`. + The lemma `mapsto_persist : l ↦{dq} v ==∗ l ↦□ v` is used for making the location `l` read-only. + See the [changes to HeapLang](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/554) for an indication on how to adapt your language. + See the [changes to iris-examples](https://gitlab.mpi-sws.org/iris/examples/-/commit/a8425b708ec51d918d5cf6eb3ab6fde88f4e2c2a) for an indication on how to adapt your development. In particular, instead of `∃ q, l ↦{q} v` you likely want to use `l ↦□ v`, which has the advantage of being persistent (rather than just duplicable). `````` Ralf Jung committed Sep 16, 2020 551 552 553 554 555 556 557 558 ``````* Change type of some ghost state lemmas (mostly about allocation) to use `∗` instead of `∧` (consistent with our usual style). This affects the following lemmas: `own_alloc_strong_dep`, `own_alloc_cofinite_dep`, `own_alloc_strong`, `own_alloc_cofinite`, `own_updateP`, `saved_anything_alloc_strong`, `saved_anything_alloc_cofinite`, `saved_prop_alloc_strong`, `saved_prop_alloc_cofinite`, `saved_pred_alloc_strong`, `saved_pred_alloc_cofinite`, `auth_alloc_strong`, `auth_alloc_cofinite`, `auth_alloc`. `````` Ralf Jung committed Sep 29, 2020 559 ``````* Change `uPred_mono` to only require inclusion at the smaller step-index. `````` Robbert Krebbers committed Oct 05, 2020 560 561 562 563 564 565 ``````* Put `iProp`/`iPreProp`-isomorphism into the `own` construction. This affects clients that define higher-order ghost state constructions. Concretely, when defining an `inG`, the functor no longer needs to be applied to `iPreProp`, but should be applied to `iProp`. This avoids clients from having to push through the `iProp`/`iPreProp`-isomorphism themselves, which is now handled once and for all by the `own` construction. `````` Ralf Jung committed Oct 13, 2020 566 567 568 569 ``````* Rename `gen_heap_ctx` to `gen_heap_interp`, since it is meant to be used in the state interpretation of WP and since `_ctx` is elsewhere used as a suffix indicating "this is a persistent assumption that clients should always have in their context". Likewise, rename `proph_map_ctx` to `proph_map_interp`. `````` Ralf Jung committed Oct 20, 2020 570 571 572 573 ``````* Move `uPred.prod_validI`, `uPred.option_validI`, and `uPred.discrete_fun_validI` to the new `base_logic.algebra` module. That module is exported by `base_logic.base_logic` so these names are now usually available everywhere, and no longer inside the `uPred` module. `````` Ralf Jung committed Nov 03, 2020 574 575 576 577 ``````* Remove the `gen_heap` notations `l ↦ -` and `l ↦{q} -`. They were barely used and looked very confusing in context: `l ↦ - ∗ P` looks like a magic wand. * Change `gen_inv_heap` notation `l ↦□ I` to `l ↦_I □`, so that `↦□` can be used by `gen_heap`. `````` Ralf Jung committed Nov 03, 2020 578 579 ``````* Strengthen `mapsto_valid_2` conclusion from `✓ (q1 + q2)%Qp` to `⌜✓ (q1 + q2)%Qp ∧ v1 = v2⌝`. `````` Ralf Jung committed Nov 10, 2020 580 581 ``````* Change `gen_heap_init` to also return ownership of the points-to facts for the initial heap. `````` Ralf Jung committed Nov 10, 2020 582 583 ``````* Rename `mapsto_mapsto_ne` to `mapsto_frac_ne`, and add a simpler `mapsto_ne` that does not require reasoning about fractions. `````` Ralf Jung committed Feb 16, 2021 584 585 586 587 588 589 590 ``````* Deprecate the `auth` and `sts` modules. These were logic-level wrappers around the underlying RAs; as far as we know, they are unused since they were not flexible enough for practical use. * Deprecate the `viewshift` module, which defined a binary view-shift connective with an implicit persistence modality. It was unused and too easily confused with `={_}=∗`, the binary view-shift (fancy update) *without* a persistence modality. `````` Ralf Jung committed Sep 15, 2020 591 `````` `````` Michael Sammler committed Oct 01, 2020 592 593 594 595 596 ``````**Changes in `program_logic`:** * `wp_strong_adequacy` now applies to an initial state with multiple threads instead of only a single thread. The derived adequacy lemmas are unchanged. `````` Ralf Jung committed Nov 27, 2020 597 598 ``````* `pure_exec_fill` is no longer registered as an instance for `PureExec`, to avoid TC search attempting to apply this instance all the time. `````` Ralf Jung committed Dec 04, 2020 599 ``````* Merge `wp_value_inv`/`wp_value_inv'` into `wp_value_fupd`/`wp_value_fupd'` by `````` Ralf Jung committed Feb 16, 2021 600 `````` making the lemmas bidirectional. `````` Robbert Krebbers committed Dec 18, 2020 601 602 603 ``````* Generalize HeapLang's `mapsto` (`↦`), `array` (`↦∗`), and atomic heap connectives to discardable fractions. See the CHANGELOG entry in the category `base_logic` for more information. `````` Robbert Krebbers committed Jan 07, 2021 604 ``````* Opening an invariant or eliminating a mask-changing update modality around a `````` Robbert Krebbers committed Jan 07, 2021 605 606 `````` non-atomic weakest precondition creates a side-condition `Atomic ...`. Before, this would fail with the unspecific error "iMod: cannot eliminate `````` Robbert Krebbers committed Jan 07, 2021 607 `````` modality (|={E1,E2}=> ...) in (WP ...)". `````` Ralf Jung committed Feb 05, 2021 608 609 ``````* In `Ectx_step` and `step_atomic`, mark the parameters that are determined by the goal as implicit. `````` Ralf Jung committed Feb 16, 2021 610 611 ``````* Deprecate the `hoare` module to prevent accidental usage; the recommended way to write Hoare-style specifications is to use Texan triples. `````` Michael Sammler committed Oct 01, 2020 612 `````` `````` Ralf Jung committed Nov 10, 2020 613 614 615 ``````**Changes in `heap_lang`:** * `wp_pures` now turns goals of the form `WP v {{ Φ }}` into `Φ v`. `````` Ralf Jung committed Nov 10, 2020 616 617 ``````* Fix `wp_bind` in case of a NOP (i.e., when the given expression pattern is already at the top level). `````` Ralf Jung committed Dec 04, 2020 618 619 ``````* The `wp_` tactics now preserve the possibility of doing a fancy update when the expression reduces to a value. `````` Robbert Krebbers committed Jan 04, 2021 620 621 622 623 ``````* Move `IntoVal`, `AsVal`, `Atomic`, `AsRecV`, and `PureExec` instances to their own file [heap_lang.class_instances](iris_heap_lang/class_instances.v). * Move `inv_head_step` tactic and `head_step` auto hints (now part of new hint database `head_step`) to [heap_lang.tactics](iris_heap_lang/tactics.v). `````` Robbert Krebbers committed Jan 17, 2021 624 625 626 ``````* The tactic `wp_apply` no longer performs `wp_pures` before applying the given lemma. The new tactic `wp_smart_apply` repeatedly performs single `wp_pure` steps until the lemma matches the goal. `````` Ralf Jung committed Nov 10, 2020 627 `````` `````` Ralf Jung committed Sep 14, 2020 628 629 630 631 632 633 ``````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") < ■ (P -∗ Q) -∗ coreP P -∗ coreP Q`. * Remove notation for 3-mask step-taking updates, and made 2-mask notation less confusing by distinguishing it better from mask-changing updates. Old: `|={Eo,Ei}▷=> P`. New: `|={Eo}[Ei]▷=> P`. Here, `Eo` is the "outer mask" (used at the beginning and end) and `Ei` the "inner mask" (used around the ▷ in the middle). As part of this, the lemmas about the 3-mask variant were changed to be about the 2-mask variant instead, and `step_fupd_mask_mono` now also has a more consistent argument order for its masks. * Add a counterexample showing that sufficiently powerful cancellable invariants with a linear token subvert the linearity guarantee (see `bi.lib.counterexmples` for details). * Redefine invariants as "semantic invariants" so that they support splitting and other forms of weakening. * Add lemmas `inv_combine` and `inv_combine_dup_l` for combining invariants. * Add the type `siProp` of "plain" step-indexed propositions, together with basic proofmode support. `````` Ralf Jung committed Jul 14, 2020 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 ``````* New ASCII versions of Iris notations. These are marked parsing only and can be made available using `Require Import iris.bi.ascii`. The new notations are (notations marked [†] are disambiguated using notation scopes): - entailment: `|-` for `⊢` and `-|-` for `⊣⊢` - logic[†]: `->` for `→`, `/\\` for `∧`, `\\/` for `∨`, and `<->` for `↔` - quantifiers[†]: `forall` for `∀` and `exists` for `∃` - separation logic: `**` for `∗`, `-*` for `-∗`, and `*-*` for `∗-∗` - step indexing: `|>` for `▷` - modalities: `<#>` for `□` and `` for `◇` - most derived notations can be computed from previous notations using the substitutions above, e.g. replace `∗` with `*` and `▷` with `|>`. Examples include the following: - `|={E1,E2}=* P` for `|={E1,E2}=∗` - `P ={E}=* Q` for `P ={E}=∗ Q` - `P ={E1,E2}=* Q` for `P ={E1,E2}=∗ Q` `````` Ralf Jung committed Jul 15, 2020 830 `````` - `|={E1}[E2]|>=> Q` for `|={E1}[E2]▷=> Q` `````` Ralf Jung committed Jul 14, 2020 831 832 833 834 835 `````` The full list can be found in [theories/bi/ascii.v](theories/bi/ascii.v), where the ASCII notations are defined in terms of the unicode notations. * Add affine, absorbing, persistent and timeless instances for telescopes. * Add a construction `bi_rtc` to create reflexive transitive closures of PROP-level binary relations. `````` Simon Friis Vindum committed Jul 02, 2020 836 837 838 839 ``````* Slightly strengthen the lemmas `big_sepL_nil'`, `big_sepL2_nil'`, `big_sepM_nil'` `big_sepM2_empty'`, `big_sepS_empty'`, and `big_sepMS_empty'`. They now only require that the argument `P` is affine instead of the whole BI being affine. `````` Ralf Jung committed Jul 14, 2020 840 841 842 843 844 845 ``````* Add `big_sepL_insert_acc`, a variant of `big_sepL_lookup_acc` which allows updating the value. * Add many missing `Proper`/non-expansiveness lemmas for big-ops. * Add `big_*_insert_delete` lemmas to split a `<[i:=x]> m` map into `i` and the rest. * Seal the definitions of `big_opS`, `big_opMS`, `big_opM` and `big_sepM2` to prevent undesired simplification. `````` Ralf Jung committed Jul 14, 2020 846 ``````* Fix `big_sepM2_fmap*` only working for `nat` keys. `````` Ralf Jung committed Jul 14, 2020 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 `````` **Changes in `proofmode`:** * Make use of `notypeclasses refine` in the implementation of `iPoseProof` and `iAssumption`, see . This has two consequences: 1. Coq's "new" unification algorithm (the one in `refine`, not the "old" one in `apply`) is used more often by the proof mode tactics. 2. Due to the use of `notypeclasses refine`, TC constraints are solved less eagerly, see . In order to port your development, it is often needed to instantiate evars explicitly (since TC search is performed less eagerly), and in few cases it is needed to unfold definitions explicitly (due to new unification algorithm behaving differently). * Strengthen the tactics `iDestruct`, `iPoseProof`, and `iAssert`: - They succeed in certain cases where they used to fail. - They keep certain hypotheses in the intuitionistic context, where they were moved to the spatial context before. The latter can lead to stronger proof mode contexts, and therefore to backwards incompatibility. This can usually be fixed by manually clearing some hypotheses. A more detailed description of the changes can be found in . `````` Ralf Jung committed Jul 15, 2020 869 870 871 872 873 874 ``````* Remove the long-deprecated `cofeT` alias (for `ofeT`) and `dec_agree` RA (use `agree` instead). * Add `auto` hint for `∗-∗`. * Add new tactic `iStopProof` to turn the proof mode entailment into an ordinary Coq goal `big star of context ⊢ proof mode goal`. `````` Ralf Jung committed Jul 14, 2020 875 876 877 878 879 880 881 882 883 884 ``````* Add new introduction pattern `-# pat` that moves a hypothesis from the intuitionistic context to the spatial context. * The tactic `iAssumption` also recognizes assumptions `⊢ P` in the Coq context. * Better support for telescopes in the proof mode, i.e., all tactics should recognize and distribute telescopes now. * The proof mode now supports names for pure facts in intro patterns. Support requires implementing `string_to_ident`. Without this tactic such patterns will fail. We provide one implementation using Ltac2 which works with Coq 8.11 and can be installed with opam; see [iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident) for details. `````` Ralf Jung committed Apr 07, 2020 885 `````` `````` Ralf Jung committed Jul 14, 2020 886 887 888 889 890 891 ``````**Changes in `algebra`:** * Remove `Core` type class for defining the total core; it is now always defined in terms of the partial core. The only user of this type class was the STS RA. * The functions `{o,r,ur}Functor_diag` are no longer coercions, and renamed into `````` Ralf Jung committed Jul 14, 2020 892 893 `````` `{o,r,ur}Functor_apply` to better match their intent. This fixes "ambiguous coercion path" warnings. `````` Ralf Jung committed Jul 14, 2020 894 895 ``````* Rename `{o,r,ur}Functor_{ne,id,compose,contractive}` into `{o,r,ur}Functor_map_{ne,id,compose,contractive}`. `````` Ralf Jung committed Jul 14, 2020 896 897 ``````* Move derived camera constructions (`frac_auth` and `ufrac_auth`) to the folder `algebra/lib`. `````` Ralf Jung committed Jul 14, 2020 898 899 900 901 902 903 904 905 906 907 908 909 910 911 ``````* Rename `mnat` to `max_nat` and "box" it by creating a separate type for it. * Move the RAs for `nat` and `positive` and the `mnat` RA into a separate module. They must now be imported from `From iris.algebra Require Import numbers`. * Make names of `f_op`/`f_core` rewrite lemmas more consistent by always making `_core`/`_op` the suffix: `op_singleton` → `singleton_op`, `core_singleton` → `singleton_core`, `discrete_fun_op_singleton` → `discrete_fun_singleton_op`, `discrete_fun_core_singleton` → `discrete_fun_singleton_core`, `list_core_singletonM` → `list_singleton_core`, `list_op_singletonM` → `list_singleton_op`, `sts_op_auth_frag` → `sts_auth_frag_op`, `sts_op_auth_frag_up` → `sts_auth_frag_up_op`, `sts_op_frag` → `sts_frag_op`, `````` Ralf Jung committed Jul 14, 2020 912 913 914 915 916 917 918 919 920 921 922 `````` `list_op_length` → `list_length_op`, `list_core_singletonM` → `list_singletonM_core`, `list_op_singletonM` → `list_singletonM_op`. * All list "map singleton" lemmas consistently use `singletonM` in their name: `list_singleton_valid` → `list_singletonM_valid`, `list_singleton_core_id` → `list_singletonM_core_id`, `list_singleton_snoc` → `list_singletonM_snoc`, `list_singleton_updateP` → `list_singletonM_updateP`, `list_singleton_updateP'` → `list_singletonM_updateP'`, `list_singleton_update` → `list_singletonM_update`, `list_alloc_singleton_local_update` → `list_alloc_singletonM_local_update`. `````` Ralf Jung committed Jul 14, 2020 923 ``````* Remove `auth_both_op` and rename `auth_both_frac_op` into `auth_both_op`. `````` Ralf Jung committed Jul 14, 2020 924 925 ``````* Add lemma `singleton_included : {[ i := x ]} ≼ ({[ i := y ]} ↔ x ≡ y ∨ x ≼ y`, and rename existing asymmetric lemmas (with a singleton on just the LHS): `````` Ralf Jung committed Jul 14, 2020 926 927 928 `````` `singleton_includedN` → `singleton_includedN_l`, `singleton_included` → `singleton_included_l`, `singleton_included_exclusive` → `singleton_included_exclusive_l`. `````` Ralf Jung committed Jul 15, 2020 929 930 931 932 933 934 935 936 937 `````` * Add notion `ofe_iso A B` that states that OFEs `A` and `B` are isomorphic. This is used in the COFE solver. * Add `{o,r,ur}Functor_oFunctor_compose` for composition of functors. * Add `pair_op_1` and `pair_op_2` to split a pair where one component is the unit. * Add derived camera construction `excl_auth A` for `auth (option (excl A))`. * Make lemma `Excl_included` a bi-implication. * Make `auth_update_core_id` work with any fraction of the authoritative element. `````` Yusuke Matsushita committed Oct 31, 2020 938 ``````* Add `min_nat`, an RA for natural numbers with `min` as the operation. `````` Ralf Jung committed Jul 14, 2020 939 ``````* Add many missing `Proper`/non-expansiveness lemmas for maps and lists. `````` Ralf Jung committed Jul 15, 2020 940 941 942 943 ``````* Add `list_singletonM_included` and `list_lookup_singletonM_{lt,gt}` lemmas about singletons in the list RA. * Add `list_core_id'`, a stronger version of `list_core_id` which only talks about elements that are actually in the list. `````` Ralf Jung committed Jul 14, 2020 944 `````` `````` Ralf Jung committed Jul 14, 2020 945 946 947 ``````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. `````` Ralf Jung committed Apr 07, 2020 948 949 ````````` sed -i -E ' `````` Ralf Jung committed Jul 14, 2020 950 951 952 953 954 955 ``````# functor renames s/\b(o|r|ur)Functor_(ne|id|compose|contractive)\b/\1Functor_map_\2/g # singleton_included renames s/\bsingleton_includedN\b/singleton_includedN_l/g s/\bsingleton_included\b/singleton_included_l/g s/\bsingleton_included_exclusive\b/singleton_included_exclusive_l/g `````` Ralf Jung committed Apr 07, 2020 956 957 958 959 ``````# f_op/f_core renames s/\b(op|core)_singleton\b/singleton_\1/g s/\bdiscrete_fun_(op|core)_singleton\b/discrete_fun_singleton_\1/g s/\bsts_op_(auth_frag|auth_frag_up|frag)\b/sts_\1_op/g `````` Ralf Jung committed Jul 14, 2020 960 ``````s/\blist_(op|core)_singletonM\b/list_singletonM_\1/g `````` Ralf Jung committed Apr 07, 2020 961 ``````s/\blist_op_length\b/list_length_op/g `````` Ralf Jung committed Jul 14, 2020 962 963 964 965 966 967 968 ``````# list "singleton map" renames s/\blist_singleton_valid\b/list_singletonM_valid/g s/\blist_singleton_core_id\b/list_singletonM_core_id/g s/\blist_singleton_snoc\b/list_singletonM_snoc/g s/\blist_singleton_updateP\b/list_singletonM_updateP/g s/\blist_singleton_update\b/list_singletonM_update/g s/\blist_alloc_singleton_local_update\b/list_alloc_singletonM_local_update/g `````` Ralf Jung committed Jul 14, 2020 969 970 971 972 973 974 975 ``````# inv renames s/\binv_sep(|_1|_2)\b/inv_split\1/g s/\binv_acc\b/inv_alter/g s/\binv_open(|_strong|_timeless)\b/inv_acc\1/g s/\bcinv_open(|_strong)\b/cinv_acc\1/g s/\b(na_inv|auth|sts)_open\b/\1_acc/g # miscellaneous `````` Simon Friis Vindum committed Apr 23, 2020 976 ``````s/\bauth_both_frac_op\b/auth_both_op/g `````` Simon Friis Vindum committed Jun 17, 2020 977 ``````s/\bmnat\b/max_nat/g `````` Ralf Jung committed Jul 14, 2020 978 ``````s/\bcoreP_wand\b/coreP_entails/g `````` Ralf Jung committed Apr 07, 2020 979 980 981 ``````' \$(find theories -name "*.v") ``` `````` Ralf Jung committed Aug 29, 2019 982 ``````## Iris 3.2.0 (released 2019-08-29) `````` Ralf Jung committed Aug 28, 2019 983 `````` `````` Ralf Jung committed Aug 28, 2019 984 985 986 ``````The highlight of this release is the completely re-engineered interactive proof mode. Not only did many tactics become more powerful; the entire proof mode can now be used not just for Iris but also for other separation logics satisfying `````` Ralf Jung committed Aug 28, 2019 987 988 989 990 991 992 ``````the proof mode interface (e.g., [Iron] and [GPFSL]). Also see the [accompanying paper][MoSeL]. [Iron]: https://iris-project.org/iron/ [GPFSL]: https://gitlab.mpi-sws.org/iris/gpfsl/ [MoSeL]: https://iris-project.org/mosel/ `````` Ralf Jung committed Aug 28, 2019 993 994 995 996 997 998 999 1000 `````` Beyond that, the Iris program logic gained the ability to reason about potentially stuck programs, and a significantly strengthened adequacy theorem that unifies the three previously separately presented theorems. There are now also Hoare triples for total program correctness (but with very limited support for invariants) and logical atomicity. And finally, our example language HeapLang was made more realistic ``````