CHANGELOG.md 68.2 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 `````` `````` Simon Friis Vindum committed Feb 23, 2021 6 7 ``````## Iris master `````` Ralf Jung committed Mar 27, 2021 8 9 ``````Coq 8.11 is no longer supported in this version of Iris. `````` Simon Friis Vindum committed Feb 23, 2021 10 11 ``````**Changes in `algebra`:** `````` Simon Friis Vindum committed Feb 24, 2021 12 13 14 15 ``````* Generalize the authorative elements of the `view`, `auth` and `gset_bij` cameras to be parameterized by a [discardable fraction](iris/algebra/dfrac.v) (`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 `````` Ralf Jung committed May 19, 2021 16 `````` the "frac" in their name has been changed into "dfrac". (by Simon Friis Vindum) `````` Ralf Jung committed Mar 09, 2021 17 18 19 20 21 22 23 24 25 26 ``````* 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](iris/algebra/reservation_map.v) 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](iris/algebra/dyn_reservation_map.v) for further information. `````` Ralf Jung committed Mar 17, 2021 27 28 ``````* Demote the Camera structure on `list` to `iris_staging` since its composition is not very well-behaved. `````` Ralf Jung committed May 12, 2021 29 ``````* Extend `gmap_view` with lemmas for "big" operations on maps. `````` 30 31 32 33 ``````* 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. `````` Paolo G. Giarrusso committed Jun 17, 2021 34 ``````* Set `Hint Mode` for the classes `OfeDiscrete`, `Dist`, `Unit`, `CmraMorphism`, `````` Paolo G. Giarrusso committed Jun 08, 2021 35 `````` `rFunctorContractive`, `urFunctorContractive`. `````` Ralf Jung committed Jun 20, 2021 36 37 38 ``````* Set `Hint Mode` for the stdpp class `Equiv`. This might require few spurious type annotations until [Coq bug #14441](https://github.com/coq/coq/issues/14441) is fixed. `````` Ralf Jung committed Jun 17, 2021 39 40 ``````* 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. `````` Robbert Krebbers committed Jul 22, 2021 41 ``````* Add `NonExpansive` instances for `curry` and friends. `````` Simon Friis Vindum committed Feb 23, 2021 42 `````` `````` Robbert Krebbers committed May 25, 2021 43 44 45 46 47 ``````**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`. `````` Ralf Jung committed May 26, 2021 48 ``````* Add lemmas for swapping nested big-ops: `big_sep{L,M,S,MS}_sep{L,M,S,MS}`. `````` 49 50 ``````* 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`. `````` Paolo G. Giarrusso committed May 31, 2021 51 52 ``````* Rename `bupd_forall` to `bupd_plain_forall`, and add `{bupd,fupd}_{and,or,forall,exist}`. `````` Ralf Jung committed Jun 18, 2021 53 54 55 56 57 ``````* 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) {{ Φ }}`. `````` Ralf Jung committed Jun 18, 2021 58 ``````* Improve `make_laterable`: `````` Ralf Jung committed Jun 18, 2021 59 `````` - Adjust definition such that `Laterable P` iff `P ⊢ make_laterable P`. `````` Ralf Jung committed Jun 18, 2021 60 61 62 `````` 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`. `````` Ralf Jung committed Jul 23, 2021 63 ``````* Improvements to `BiMonoPred`: `````` Robbert Krebbers committed Jul 22, 2021 64 65 `````` - Use `□`/`-∗` instead of ``/`→`. - Strengthen to ensure that functions for recursive calls are non-expansive. `````` Ralf Jung committed Jul 26, 2021 66 ``````* Add `big_andM` (big conjunction on finite maps) with lemmas similar to `big_andL`. `````` Hai Dang committed Jul 26, 2021 67 68 69 ``````* 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 70 `````` (by Hai Dang, BedRock Systems) `````` Ralf Jung committed Jul 28, 2021 71 72 73 ``````* Improve notation printing around `WP`, Texan triples, and logically atomic triples. * 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 74 ``````* Add the lemmas `big_sepM_impl_strong` and `big_sepM_impl_dom_subseteq` that `````` Simon Friis Vindum committed Jul 30, 2021 75 `````` generalize the existing `big_sepM_impl` lemma. (by Simon Friis Vindum) `````` Robbert Krebbers committed May 25, 2021 76 `````` `````` Ralf Jung committed Mar 24, 2021 77 ``````**Changes in `proofmode`:** `````` Ralf Jung committed Mar 24, 2021 78 79 80 `````` * 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 81 `````` https://gitlab.mpi-sws.org/iris/string-ident. (by Tej Chajed) `````` Ralf Jung committed Mar 24, 2021 82 ``````* Add support for destructing existentials with the intro pattern `[%x ...]`. `````` Ralf Jung committed May 19, 2021 83 `````` (by Tej Chajed) `````` Ralf Jung committed May 26, 2021 84 ``````* `iMod`/`iModIntro` show proper error messages when they fail due to mask `````` Ralf Jung committed Jun 06, 2021 85 86 `````` mismatches. To support this, the proofmode typeclass `FromModal` now takes an additional pure precondition. `````` Paolo G. Giarrusso committed Jul 25, 2021 87 88 89 90 ``````* 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 91 92 `````` 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 93 94 `````` https://coq.inria.fr/refman/addendum/type-classes.html#coq:cmd.Instance. (by Paolo G. Giarrusso, BedRock Systems) `````` Ralf Jung committed Jul 26, 2021 95 96 97 ``````* 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 98 99 100 ``````* Improve performance of the `iIntoEmpValid` tactic used by `iPoseProof`, especially in the case of large goals and lemmas with many forall quantifiers (by Armaël Guéneau) `````` Ralf Jung committed Mar 24, 2021 101 `````` `````` Ralf Jung committed May 26, 2021 102 103 104 ``````**Changes in `bi`:** * Add lemmas characterizing big-ops over pure predicates (`big_sep*_pure*`). `````` Ralf Jung committed Jun 07, 2021 105 106 ``````* Move `BiAffine`, `BiPositive`, `BiLöb`, and `BiPureForall` from `bi.derived_connectives` to `bi.extensions`. `````` Paolo G. Giarrusso committed Jul 18, 2021 107 ``````* Strengthen `persistent_fractional` to support propositions that are persistent `````` Ralf Jung committed Jul 18, 2021 108 `````` and either affine or absorbing. (by Paolo G. Giarrusso, BedRock Systems) `````` Ralf Jung committed May 26, 2021 109 `````` `````` Ralf Jung committed Mar 05, 2021 110 111 112 113 ``````**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 114 115 ``````* 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 116 `````` (by Jacques-Henri Jourdan) `````` Ralf Jung committed Jun 02, 2021 117 118 119 ``````* 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`. `````` 120 121 122 `````` **Changes in `program_logic`:** `````` Jacques-Henri Jourdan committed Mar 06, 2021 123 124 125 126 127 128 ``````* 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: `````` 129 130 131 132 133 134 135 `````` - 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 136 `````` (by Jacques-Henri Jourdan) `````` Ralf Jung committed May 11, 2021 137 ``````* Remove `wp_frame_wand_l`; add `wp_frame_wand` as more symmetric replacement. `````` Ralf Jung committed Jul 19, 2021 138 139 ``````* Swap the polarity of the mask in logically atomic triples, so that it matches regular `WP` masks. `````` Ralf Jung committed Sep 01, 2021 140 ``````* Rename `iris_invG` to `iris_invGS`. `````` 141 `````` `````` Ralf Jung committed Mar 18, 2021 142 143 144 ``````**Changes in `heap_lang`:** * Rename `Build_loc` constructor for `loc` type to `Loc`. `````` Ralf Jung committed May 19, 2021 145 ``````* Add atomic `Xchg` ("exchange"/"swap") operation. (by Simon Hudon, Google LLC) `````` Ralf Jung committed Mar 18, 2021 146 `````` `````` Ralf Jung committed Mar 06, 2021 147 148 149 150 151 152 153 154 155 156 ``````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 315 316 317 318 319 320 321 322 323 324 325 326 ``````* 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 327 `````` `````` Tej Chajed committed Jul 21, 2020 328 329 330 331 332 333 334 335 336 ``````**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 337 338 339 340 341 ``````* 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 342 343 344 345 346 ``````* 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 347 348 349 ``````* 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 350 351 ``````* Add Coq side-condition `φ` to class `ElimAcc` (similar to what we already had for `ElimInv` and `ElimModal`). `````` Rodolphe Lepigre committed Jan 27, 2021 352 353 ``````* 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 354 `````` or spatial context matching `pat`. The tactic `iSelect` is used to implement: `````` Rodolphe Lepigre committed Jan 27, 2021 355 356 357 358 359 `````` + `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 360 `````` `````` Ralf Jung committed Sep 15, 2020 361 362 363 364 ``````**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 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 ``````* 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 389 390 391 392 393 394 395 396 ``````* 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 397 ``````* Change `uPred_mono` to only require inclusion at the smaller step-index. `````` Robbert Krebbers committed Oct 05, 2020 398 399 400 401 402 403 ``````* 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 404 405 406 407 ``````* 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 408 409 410 411 ``````* 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 412 413 414 415 ``````* 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 416 417 ``````* Strengthen `mapsto_valid_2` conclusion from `✓ (q1 + q2)%Qp` to `⌜✓ (q1 + q2)%Qp ∧ v1 = v2⌝`. `````` Ralf Jung committed Nov 10, 2020 418 419 ``````* Change `gen_heap_init` to also return ownership of the points-to facts for the initial heap. `````` Ralf Jung committed Nov 10, 2020 420 421 ``````* 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 422 423 424 425 426 427 428 ``````* 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 429 `````` `````` Michael Sammler committed Oct 01, 2020 430 431 432 433 434 ``````**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 435 436 ``````* `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 437 ``````* Merge `wp_value_inv`/`wp_value_inv'` into `wp_value_fupd`/`wp_value_fupd'` by `````` Ralf Jung committed Feb 16, 2021 438 `````` making the lemmas bidirectional. `````` Robbert Krebbers committed Dec 18, 2020 439 440 441 ``````* 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 442 ``````* Opening an invariant or eliminating a mask-changing update modality around a `````` Robbert Krebbers committed Jan 07, 2021 443 444 `````` 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 445 `````` modality (|={E1,E2}=> ...) in (WP ...)". `````` Ralf Jung committed Feb 05, 2021 446 447 ``````* In `Ectx_step` and `step_atomic`, mark the parameters that are determined by the goal as implicit. `````` Ralf Jung committed Feb 16, 2021 448 449 ``````* 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 450 `````` `````` Ralf Jung committed Nov 10, 2020 451 452 453 ``````**Changes in `heap_lang`:** * `wp_pures` now turns goals of the form `WP v {{ Φ }}` into `Φ v`. `````` Ralf Jung committed Nov 10, 2020 454 455 ``````* 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 456 457 ``````* 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 458 459 460 461 ``````* 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 462 463 464 ``````* 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 465 `````` `````` Ralf Jung committed Sep 14, 2020 466 467 468 469 470 471 ``````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 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 ``````* 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 668 `````` - `|={E1}[E2]|>=> Q` for `|={E1}[E2]▷=> Q` `````` Ralf Jung committed Jul 14, 2020 669 670 671 672 673 `````` 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 674 675 676 677 ``````* 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 678 679 680 681 682 683 ``````* 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 684 ``````* Fix `big_sepM2_fmap*` only working for `nat` keys. `````` Ralf Jung committed Jul 14, 2020 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 `````` **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 707 708 709 710 711 712 ``````* 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 713 714 715 716 717 718 719 720 721 722 ``````* 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 723 `````` `````` Ralf Jung committed Jul 14, 2020 724 725 726 727 728 729 ``````**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 730 731 `````` `{o,r,ur}Functor_apply` to better match their intent. This fixes "ambiguous coercion path" warnings. `````` Ralf Jung committed Jul 14, 2020 732 733 ``````* 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 734 735 ``````* Move derived camera constructions (`frac_auth` and `ufrac_auth`) to the folder `algebra/lib`. `````` Ralf Jung committed Jul 14, 2020 736 737 738 739 740 741 742 743 744 745 746 747 748 749 ``````* 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 750 751 752 753 754 755 756 757 758 759 760 `````` `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 761 ``````* Remove `auth_both_op` and rename `auth_both_frac_op` into `auth_both_op`. `````` Ralf Jung committed Jul 14, 2020 762 763 ``````* 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 764 765 766 `````` `singleton_includedN` → `singleton_includedN_l`, `singleton_included` → `singleton_included_l`, `singleton_included_exclusive` → `singleton_included_exclusive_l`. `````` Ralf Jung committed Jul 15, 2020 767 768 769 770 771 772 773 774 775 `````` * 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 776 ``````* Add `min_nat`, an RA for natural numbers with `min` as the operation. `````` Ralf Jung committed Jul 14, 2020 777 ``````* Add many missing `Proper`/non-expansiveness lemmas for maps and lists. `````` Ralf Jung committed Jul 15, 2020 778 779 780 781 ``````* 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 782 `````` `````` Ralf Jung committed Jul 14, 2020 783 784 785 ``````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 786 787 ````````` sed -i -E ' `````` Ralf Jung committed Jul 14, 2020 788 789 790 791 792 793 ``````# 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 794 795 796 797 ``````# 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 798 ``````s/\blist_(op|core)_singletonM\b/list_singletonM_\1/g `````` Ralf Jung committed Apr 07, 2020 799 ``````s/\blist_op_length\b/list_length_op/g `````` Ralf Jung committed Jul 14, 2020 800 801 802 803 804 805 806 ``````# 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 807 808 809 810 811 812 813 ``````# 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 814 ``````s/\bauth_both_frac_op\b/auth_both_op/g `````` Simon Friis Vindum committed Jun 17, 2020 815 ``````s/\bmnat\b/max_nat/g `````` Ralf Jung committed Jul 14, 2020 816 ``````s/\bcoreP_wand\b/coreP_entails/g `````` Ralf Jung committed Apr 07, 2020 817 818 819 ``````' \$(find theories -name "*.v") ``` `````` Ralf Jung committed Aug 29, 2019 820 ``````## Iris 3.2.0 (released 2019-08-29) `````` Ralf Jung committed Aug 28, 2019 821 `````` `````` Ralf Jung committed Aug 28, 2019 822 823 824 ``````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 825 826 827 828 829 830 ``````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 831 832 833 834 835 836 837 838 839 840 841 842 843 844 `````` 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 (Compare-and-set got replaced by compare-exchange and limited to only compare values that can actually be compared atomically) and more powerful, with added support for arrays and prophecy variables. Further details are given in the changelog below. `````` Ralf Jung committed Aug 29, 2019 845 846 847 848 849 850 851 852 ``````This release of Iris received contributions by Aleš Bizjak, Amin Timany, Dan Frumin, Glen Mével, Hai Dang, Hugo Herbelin, Jacques-Henri Jourdan, Jan Menz, Jan-Oliver Kaiser, Jonas Kastberg Hinrichsen, Joseph Tassarotti, Mackie Loeffel, Marianna Rapoport, Maxime Dénès, Michael Sammler, Paolo G. Giarrusso, Pierre-Marie Pédrot, Ralf Jung, Robbert Krebbers, Rodolphe Lepigre, and Tej Chajed. Thanks a lot to everyone involved! **Changes in the theory of Iris itself:** `````` Ralf Jung committed Jan 24, 2018 853 `````` `````` Ralf Jung committed Jun 05, 2019 854 ``````* Change in the definition of WP, so that there is a fancy update between `````` Jacques-Henri Jourdan committed Jun 14, 2018 855 856 `````` the quantification over the next states and the later modality. This makes it possible to prove more powerful lifting lemmas: The new versions feature an `````` Ralf Jung committed Jun 14, 2018 857 `````` "update that takes a step". `````` Ralf Jung committed Jun 05, 2019 858 859 860 ``````* Add weakest preconditions for total program correctness. * "(Potentially) stuck" weakest preconditions and the "plainly modality" are no longer considered experimental. `````` Ralf Jung committed Jun 06, 2019 861 ``````* Add the notion of an "observation" to the language interface, so that `````` Ralf Jung committed Oct 05, 2018 862 863 `````` every reduction step can optionally be marked with an event, and an execution trace has a matching list of events. Change WP so that it is told the entire `````` Ralf Jung committed Jun 06, 2019 864 `````` future trace of observations from the beginning. `````` Ralf Jung committed Jun 05, 2019 865 ``````* The Löb rule is now a derived rule; it follows from later-intro, later `````` Ralf Jung committed Jul 06, 2018 866 867 `````` being contractive and the fact that we can take fixpoints of contractive functions. `````` Ralf Jung committed Jun 05, 2019 868 ``````* Add atomic updates and logically atomic triples, including tactic support. `````` Ralf Jung committed Jul 13, 2018 869 `````` See `heap_lang/lib/increment.v` for an example. `````` Ralf Jung committed Jun 06, 2019 870 871 872 ``````* Extend the state interpretation with a natural number that keeps track of the number of forked-off threads, and have a global fixed proposition that describes the postcondition of each forked-off thread (instead of it being `````` Robbert Krebbers committed Jun 12, 2019 873 `````` `True`). `````` Ralf Jung committed Jun 12, 2019 874 875 876 ``````* A stronger adequacy statement for weakest preconditions that involves the final state, the post-condition of forked-off threads, and also applies if the main-thread has not terminated. `````` Ralf Jung committed Jun 06, 2019 877 878 879 ``````* The user-chosen functor used to instantiate the Iris logic now goes from COFEs to Cameras (it was OFEs to Cameras). `````` Ralf Jung committed Aug 29, 2019 880 ``````**Changes in heap_lang:** `````` Ralf Jung committed Jun 06, 2019 881 `````` `````` Ralf Jung committed Jun 24, 2019 882 883 884 885 886 887 888 889 ``````* CAS (compare-and-set) got replaced by CmpXchg (compare-exchange). The difference is that CmpXchg returns a pair consisting of the old value and a boolean indicating whether the comparison was successful and hence the exchange happened. CAS can be obtained by simply projecting to the second component, but also providing the old value more closely models the primitive typically provided in systems languages (C, C++, Rust). The comparison by this operation also got weakened to be efficiently implementable: CmpXchg may only be used to compare "unboxed" values that can `````` Ralf Jung committed Jul 12, 2019 890 891 892 893 894 `````` be represented in a single machine word. It is sufficient if one of the two compared values is unboxed. * For consistency, the restrictions CmpXchg imposes on comparison also apply to the `=` binary operator. This also fixes the long-standing problem that that operator allowed compared closures with each other. `````` Ralf Jung committed Jul 13, 2019 895 896 ``````* Implement prophecy variables using the new support for "observations". The erasure theorem (showing that prophecy variables do not alter program `````` Ralf Jung committed Aug 28, 2019 897 `````` behavior) can be found [in the iris/examples repository][prophecy-erasure]. `````` Ralf Jung committed Jun 06, 2019 898 ``````* heap_lang now uses right-to-left evaluation order. This makes it `````` Ralf Jung committed Oct 05, 2018 899 `````` significantly easier to write specifications of curried functions. `````` Ralf Jung committed Jun 06, 2019 900 ``````* heap_lang values are now injected in heap_lang expressions via a specific `````` Jacques-Henri Jourdan committed Oct 31, 2018 901 902 `````` constructor of the expr inductive type. This simplifies much the tactical infrastructure around the language. In particular, this allow us to get rid `````` Robbert Krebbers committed Oct 31, 2018 903 `````` the reflection mechanism that was needed for proving closedness, atomicity and `````` Jacques-Henri Jourdan committed Oct 31, 2018 904 905 `````` "valueness" of a term. The price to pay is the addition of new "administrative" reductions in the operational semantics of the language. `````` Ralf Jung committed Jun 06, 2019 906 907 ``````* heap_lang now has support for allocating, accessing and reasoning about arrays (continuously allocated regions of memory). `````` Robbert Krebbers committed Jun 10, 2019 908 ``````* One can now assign "meta" data to heap_lang locations. `````` Ralf Jung committed Jan 24, 2018 909 `````` `````` Ralf Jung committed Aug 28, 2019 910 911 ``````[prophecy-erasure]: https://gitlab.mpi-sws.org/iris/examples/blob/3f33781fe6e19cfdb25259c8194d34403f1134d5/theories/logatom/proph_erasure.v `````` Ralf Jung committed Aug 29, 2019 912 ``````**Changes in Coq:** `````` Robbert Krebbers committed Jan 03, 2018 913 `````` `````` Ralf Jung committed Aug 28, 2019 914 ``````* An all-new generalized proof mode that abstracts away from Iris! Major new `````` Ralf Jung committed Jul 09, 2018 915 916 917 918 919 920 `````` features: - The proof mode can now be used with logics derived from Iris (like iGPS), with non-step-indexed logics and even with non-affine (i.e., linear) logics. - `iModIntro` is more flexible and more powerful, it now also subsumes `iNext` and `iAlways`. - General infrastructure for deriving a logic for monotone predicates over `````` Ralf Jung committed Aug 28, 2019 921 `````` an existing logic (see the paper for more details). `````` Ralf Jung committed Jul 09, 2018 922 `````` Developments instantiating the proof mode typeclasses may need significant `````` Robbert Krebbers committed May 02, 2019 923 924 `````` changes. For developments just using the proof mode tactics, porting should not be too much effort. Notable things to port are: `````` Ralf Jung committed Jul 02, 2018 925 926 927 928 929 `````` - All the BI laws moved from the `uPred` module to the `bi` module. For example, `uPred.later_equivI` became `bi.later_equivI`. - Big-ops are automatically imported, imports of `iris.base_logic.big_op` have to be removed. - The ⊢ notation can sometimes infer different (but convertible) terms when `````` Robbert Krebbers committed Dec 14, 2018 930 `````` searching for the BI to use, which (due to Coq limitations) can lead to `````` Ralf Jung committed Jul 02, 2018 931 932 933 934 `````` failing rewrites, in particular when rewriting at function types. * The `iInv` tactic can now be used without the second argument (the name for the closing update). It will then instead add the obligation to close the invariant to the goal. `````` Ralf Jung committed May 21, 2019 935 936 ``````* The new `iEval` tactic can be used to execute a simplification or rewriting tactic on some specific part(s) of the proofmode goal. `````` Ralf Jung committed Jul 04, 2018 937 938 ``````* Added support for defining derived connectives involving n-ary binders using telescopes. `````` Ralf Jung committed Jul 06, 2018 939 940 941 ``````* The proof mode now more consistently "prettifies" the goal after each tactic. Prettification also simplifies some BI connectives, like conditional modalities and telescope quantifiers. `````` Ralf Jung committed Jul 02, 2018 942 ``````* Improved pretty-printing of Iris connectives (in particular WP and fancy `````` Ralf Jung committed Jul 06, 2018 943 944 945 `````` updates) when Coq has to line-wrap the output. This goes hand-in-hand with an improved test suite that also tests pretty-printing. * Added a `gmultiset` RA. `````` Ralf Jung committed Jul 14, 2020 946 ``````* Rename `timelessP` → `timeless` (projection of the `Timeless` class) `````` Ralf Jung committed Feb 20, 2018 947 948 ``````* The CMRA axiom `cmra_extend` is now stated in `Type`, using `sigT` instead of in `Prop` using `exists`. This makes it possible to define the function space `````` Jacques-Henri Jourdan committed Feb 20, 2018 949 `````` CMRA even for an infinite domain. `````` Robbert Krebbers committed Feb 20, 2018 950 951 952 953 954 ``````* Rename proof mode type classes for laters: - `IntoLaterN` → `MaybeIntoLaterN` (this one _may_ strip a later) - `IntoLaterN'` → `IntoLaterN` (this one _should_ strip a later) - `IntoLaterNEnv` → `MaybeIntoLaterNEnv` - `IntoLaterNEnvs` → `MaybeIntoLaterNEnvs` `````` 955 956 ``````* Rename: - `frag_auth_op` → `frac_auth_frag_op` `````` 957 958 959 `````` - `cmra_opM_assoc` → `cmra_op_opM_assoc` - `cmra_opM_assoc_L` → `cmra_op_opM_assoc_L` - `cmra_opM_assoc'` → `cmra_opM_opM_assoc` `````` Robbert Krebbers committed Feb 21, 2018 960 ``````* `namespaces` has been moved to std++. `````` Ralf Jung committed Jun 18, 2018 961 962 ``````* Changed `IntoVal` to be directly usable for rewriting `e` into `of_val v`, and changed `AsVal` to be usable for rewriting via the `[v <-]` destruct pattern. `````` Ralf Jung committed Oct 05, 2018 963 ``````* `wp_fork` is now written in curried form. `````` Robbert Krebbers committed Oct 05, 2018 964 ``````* `PureExec`/`wp_pure` now supports taking multiple steps at once. `````` Jacques-Henri Jourdan committed Oct 31, 2018 965 966 967 ``````* A new tactic, `wp_pures`, executes as many pure steps as possible, excluding steps that would require unlocking subterms. Every impure wp_ tactic executes this tactic before doing anything else. `````` Dan Frumin committed Feb 03, 2019 968 ``````* Add `big_sepM_insert_acc`. `````` Dan Frumin committed Apr 07, 2019 969 970 971 972 ``````* Add big separating conjunctions that operate on pairs of lists (`big_sepL2`) and on pairs of maps (`big_sepM2`). In the former case the lists are required to have the same length, and in the latter case the maps are required to have the same domains. `````` Dan Frumin committed Mar 06, 2019 973 974 975 ``````* The `_strong` lemmas (e.g. `own_alloc_strong`) work for all infinite sets, instead of just for cofinite sets. The versions with cofinite sets have been renamed to use the `_cofinite` suffix. `````` Robbert Krebbers committed Mar 14, 2019 976 977 978 ``````* Remove locked value lambdas. The value scope notations `rec: f x := e` and `(λ: x, e)` no longer add a `locked`. Instead, we made the `wp_` tactics smarter to no longer unfold lambdas/recs that occur behind definitions. `````` Ralf Jung committed May 21, 2019 979 ``````* Export the fact that `iPreProp` is a COFE. `````` Hai Dang committed May 23, 2019 980 981 982 983 984 985 986 ``````* The CMRA `auth` now can have fractional authoritative parts. So now `auth` has 3 types of elements: the fractional authoritative `●{q} a`, the full authoritative `● a ≡ ●{1} a`, and the non-authoritative `◯ a`. Updates are only possible with the full authoritative element `● a`, while fractional authoritative elements have agreement: `✓ (●{p} a ⋅ ●{q} b) ⇒ a ≡ b`. As a consequence, `auth` is no longer a COFE and does not preserve Leibniz equality. `````` Ralf Jung committed Jun 24, 2019 987 988 ``````* Add a COFE construction (and functor) on dependent pairs `sigTO`, dual to `discrete_funO`. `````` Hai Dang committed May 24, 2019 989 990 991 992 993 994 ``````* Rename in `auth`: - Use `auth_auth_proj`/`auth_frag_proj` for the projections of `auth`: `authoritative` → `auth_auth_proj` and `auth_own` → `auth_frag_proj`. - Use `auth_auth` and `auth_frag` for the injections into authoritative elements and non-authoritative elements respectively. - Lemmas for the projections and injections are renamed accordingly. `````` Hai Dang committed May 24, 2019 995 996 997 998 999 `````` For examples: + `authoritative_validN` → `auth_auth_proj_validN` + `auth_own_validN` → `auth_frag_proj_validN` + `auth_auth_valid` was not renamed because it was already used for the authoritative injection. `````` Hai Dang committed May 24, 2019 1000 `````` - `auth_both_valid` → `auth_both_valid_2` ``````