CHANGELOG.md 30 KB
Newer Older
 Ralf Jung committed Jul 25, 2016 1 2 3 ``````In this changelog, we document "large-ish" changes to Iris that affect even the way the logic is used on paper. We also mention some significant changes in the Coq development, but not every API-breaking change is listed. Changes marked `````` Ralf Jung committed Oct 21, 2016 4 ```````[#]` still need to be ported to the Iris Documentation LaTeX file(s). `````` Ralf Jung committed Aug 08, 2016 5 `````` `````` Robbert Krebbers committed Sep 11, 2019 6 7 ``````## Iris master `````` Ralf Jung committed Nov 01, 2019 8 9 10 11 ``````**Changes in the theory of Iris itself:** * [#] Redefine invariants as "semantic invariants" so that they support splitting and other forms of weakening. `````` Jonas Kastberg committed Nov 05, 2019 12 13 ``````* Updated the strong variant of the opening lemma for cancellable invariants to match that of regular invariants, where you can pick the mask at a later time. `````` Amin Timany committed Nov 06, 2019 14 15 16 17 18 19 `````` **Changes in program logic:** * In the axiomatization of ectx languages we replace the axiom of positivity of context composition with an axiom that says if `fill K e` takes a head step, then either `K` is the empty evaluation context or `e` is a value. `````` Ralf Jung committed Nov 01, 2019 20 `````` `````` Robbert Krebbers committed Sep 11, 2019 21 22 ``````**Changes in Coq:** `````` Ralf Jung committed Feb 25, 2020 23 ``````* Added support for Coq 8.10 and Coq 8.11; dropped support for Coq 8.7 and Coq 8.8. `````` Ralf Jung committed Mar 16, 2020 24 25 26 27 ``````* Removed coercion from `iProp` (and other MoSeL propositions) to `Prop`. Instead, use the new unary notation `⊢ P`, or `⊢@{PROP} P` if the proposition type cannot be inferred. This also means that `%I` should not be necessary any more when stating lemmas, as `P` above is automatically parsed in scope `%I`. `````` Robbert Krebbers committed Sep 11, 2019 28 29 ``````* A new tactic `iStopProof` to turn the proof mode entailment into an ordinary Coq goal `big star of context ⊢ proof mode goal`. `````` Robbert Krebbers committed Sep 19, 2019 30 31 ``````* Rename `iProp`/`iPreProp` to `iPropO`/`iPrePropO` since they are `ofeT`s. Introduce `iProp` for the `Type` carrier of `iPropO`. `````` Robbert Krebbers committed Nov 21, 2019 32 33 34 ``````* Move derived camera constructions (`frac_auth` and `ufrac_auth`) to the folder `algebra/lib`. * Add derived camera construction `excl_auth A` for `auth (option (excl A))`. `````` Robbert Krebbers committed Nov 21, 2019 35 36 37 ``````* Make use of `notypeclasses refine` in the implementation of `iPoseProof` and `iAssumption`, see https://gitlab.mpi-sws.org/iris/iris/merge_requests/329 This has two consequences: `````` Ralf Jung committed Nov 22, 2019 38 39 `````` 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. `````` Robbert Krebbers committed Nov 22, 2019 40 41 `````` 2. Due to the use of `notypeclasses refine`, TC constraints are solved less eagerly, see https://github.com/coq/coq/issues/6583. `````` Robbert Krebbers committed Nov 21, 2019 42 43 44 45 `````` 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). `````` Ralf Jung committed Dec 02, 2019 46 47 48 ``````* Removed `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. `````` Robbert Krebbers committed Jan 13, 2020 49 50 ``````* Added the type `siProp` of "plain" step-indexed propositions, together with basic proofmode support. `````` Michael Sammler committed Jan 16, 2020 51 52 ``````* Sealed the definitions of `big_opS`, `big_opMS`, `big_opM` and `big_sepM2` to prevent undesired simplification. `````` Robbert Krebbers committed Feb 02, 2020 53 54 55 56 57 58 59 60 ``````* The tactics `iDestruct`, `iPoseProof`, and `iAssert` have become stronger: - 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 https://gitlab.mpi-sws.org/iris/iris/merge_requests/341. `````` Ralf Jung committed Feb 14, 2020 61 62 63 64 65 66 67 68 69 ``````* Renamed some accessor-style lemmas to consistently use the suffix `_acc` instead of `_open`: `inv_open` -> `inv_acc`, `inv_open_strong` -> `inv_acc_strong`, `inv_open_timeless` -> `inv_acc_timeless`, `na_inv_open` -> `na_inv_acc`, `cinv_open` -> `cinv_acc`, `cinv_open_strong` -> `cinv_acc_strong`, `auth_open` -> `auth_acc`, `sts_open` -> `sts_acc`. To make this work we also had to rename `inv_acc` -> `inv_alter`. (Most developments should be unaffected as the typical way to invoke these lemmas is through `iInv`, and that does not change.) `````` Jonas Kastberg committed Feb 14, 2020 70 71 ``````* Added a construction `bi_rtc` to create reflexive transitive closures of PROP-level binary relations. `````` Robbert Krebbers committed Feb 18, 2020 72 73 ``````* Add new introduction pattern `-# pat` that moves a hypothesis from the intuitionistic context to the spatial context. `````` Robbert Krebbers committed Mar 10, 2020 74 75 76 77 78 79 80 ``````* Made lemma names for `fill` more consistent - Use the `_inv` suffix for the the backwards directions: `reducible_fill` → `reducible_fill_inv`, `reducible_no_obs_fill` → `reducible_no_obs_fill_inv`, `not_stuck_fill` → `not_stuck_fill_inv`. - Use the non-`_inv` names (that freed up) for the forwards directions: `reducible_fill`, `reducible_no_obs_fill`, `irreducible_fill_inv`. `````` Robbert Krebbers committed Mar 20, 2020 81 ``````* The tactic `iAssumption` also recognizes assumptions `⊢ P` in the Coq context. `````` Robbert Krebbers committed Apr 01, 2020 82 83 ``````* Add notion `ofe_iso A B` that states that OFEs `A` and `B` are isomorphic. * Make use of `ofe_iso` in the COFE solver. `````` Robbert Krebbers committed Apr 01, 2020 84 85 ``````* The functions `{o,r,ur}Functor_diag` are no longer coercions, and renamed into `{o,r,ur}Functor_apply` to better match their intent. `````` Robbert Krebbers committed Apr 02, 2020 86 87 88 89 90 ``````* Change `inv_iff`, `cinv_iff` and `na_inv_iff` to make order of arguments consistent and more convenient for `iApply`. They are now of the form `inv N P -∗ ▷ □ (P ↔ Q) -∗ inv N Q` and (similar for `na_inv_iff` and `cinv_iff`), following e.g., `inv_alter` and `wp_wand`. * Add lemma `is_lock_iff` and show that `is_lock` is contractive. `````` Robbert Krebbers committed Apr 02, 2020 91 92 93 ``````* Rename `{o,r,ur}Functor_{ne,id,compose,contractive}` into `{o,r,ur}Functor_map_{ne,id,compose,contractive}`. * Add `{o,r,ur}Functor_oFunctor_compose` for composition of functors. `````` Robbert Krebbers committed Apr 03, 2020 94 95 96 ``````* Affine, absorbing, persistent and timeless instances for telescopes. * Better support for telescopes in the proof mode, i.e., all tactics should recognize and distribute telescopes now. `````` Robbert Krebbers committed Apr 03, 2020 97 ``````* Remove namespace `N` from `is_lock`. `````` Robbert Krebbers committed Apr 03, 2020 98 99 100 101 102 ``````* Make lemma `Excl_included` a bi-implication. * Add lemma `singleton_included : {[ i := x ]} ≼ ({[ i := y ]} ↔ x ≡ y ∨ x ≼ y`, and rename existing asymmetric lemmas (with a singleton on just the LHS): + `singleton_includedN` → `singleton_includedN_l`. + `singleton_included` → `singleton_included_l`. `````` Robbert Krebbers committed Apr 04, 2020 103 `````` + `singleton_included_exclusive` → `singleton_included_exclusive_l` `````` Tej Chajed committed Apr 06, 2020 104 ``````* The proof mode now supports names for pure facts in intro patterns. Support `````` Tej Chajed committed Apr 06, 2020 105 `````` requires implementing `string_to_ident`. Without this tactic such patterns `````` Tej Chajed committed Apr 06, 2020 106 107 108 `````` 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 109 110 111 112 113 114 115 116 ``````* Make names of `f_op`/`f_core` rewrite lemmas more consistent: `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_singletonM_core`, `list_op_singletonM` -> `list_singletonM_op`, `sts_op_auth_frag` -> `sts_auth_frag_op`, `sts_op_auth_frag_up` -> `sts_auth_frag_up_op`, `````` Ralf Jung committed Apr 07, 2020 117 118 119 120 121 122 123 124 125 126 127 128 129 130 `````` `sts_op_frag` -> `sts_frag_op`, `list_op_length` -> `list_length_op`. * Make list singleton lemmas consistent with gmap: `elem_of_list_singletonM` -> `elem_of_list_singleton`, `list_lookup_singletonM` -> `list_lookup_singleton`, `list_lookup_singletonM_lt` -> `list_lookup_singleton_lt`, `list_lookup_singletonM_gt` -> `list_lookup_singleton_gt`, `list_lookup_singletonM_ne` -> `list_lookup_singleton_ne`, `list_singletonM_validN` -> `list_singleton_validN`, `list_singletonM_length` -> `list_singleton_length`, `list_singletonM_core` -> `list_singleton_core`, `list_singletonM_op` -> `list_singleton_op`, `list_alter_singletonM` -> `list_alter_singleton`, `list_singletonM_included` -> `list_singleton_included`. `````` Robbert Krebbers committed Sep 11, 2019 131 `````` `````` Tej Chajed committed Feb 23, 2020 132 133 134 ``````**Changes in heap_lang:** * Added a fraction to the heap_lang `array` assertion. `````` Tej Chajed committed Feb 25, 2020 135 ``````* Added array_copy library for copying and cloning arrays. `````` Tej Chajed committed Feb 23, 2020 136 `````` `````` Ralf Jung committed Aug 29, 2019 137 ``````## Iris 3.2.0 (released 2019-08-29) `````` Ralf Jung committed Aug 28, 2019 138 `````` `````` Ralf Jung committed Aug 28, 2019 139 140 141 ``````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 142 143 144 145 146 147 ``````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 148 149 150 151 152 153 154 155 156 157 158 159 160 161 `````` 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 162 163 164 165 166 167 168 169 ``````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 170 `````` `````` Ralf Jung committed Jun 05, 2019 171 ``````* Change in the definition of WP, so that there is a fancy update between `````` Jacques-Henri Jourdan committed Jun 14, 2018 172 173 `````` 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 174 `````` "update that takes a step". `````` Ralf Jung committed Jun 05, 2019 175 176 177 ``````* 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 178 ``````* Add the notion of an "observation" to the language interface, so that `````` Ralf Jung committed Oct 05, 2018 179 180 `````` 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 181 `````` future trace of observations from the beginning. `````` Ralf Jung committed Jun 05, 2019 182 ``````* The Löb rule is now a derived rule; it follows from later-intro, later `````` Ralf Jung committed Jul 06, 2018 183 184 `````` being contractive and the fact that we can take fixpoints of contractive functions. `````` Ralf Jung committed Jun 05, 2019 185 ``````* Add atomic updates and logically atomic triples, including tactic support. `````` Ralf Jung committed Jul 13, 2018 186 `````` See `heap_lang/lib/increment.v` for an example. `````` Ralf Jung committed Jun 06, 2019 187 188 189 ``````* 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 190 `````` `True`). `````` Ralf Jung committed Jun 12, 2019 191 192 193 ``````* 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 194 195 196 ``````* 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 197 ``````**Changes in heap_lang:** `````` Ralf Jung committed Jun 06, 2019 198 `````` `````` Ralf Jung committed Jun 24, 2019 199 200 201 202 203 204 205 206 ``````* 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 207 208 209 210 211 `````` 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 212 213 ``````* 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 214 `````` behavior) can be found [in the iris/examples repository][prophecy-erasure]. `````` Ralf Jung committed Jun 06, 2019 215 ``````* heap_lang now uses right-to-left evaluation order. This makes it `````` Ralf Jung committed Oct 05, 2018 216 `````` significantly easier to write specifications of curried functions. `````` Ralf Jung committed Jun 06, 2019 217 ``````* heap_lang values are now injected in heap_lang expressions via a specific `````` Jacques-Henri Jourdan committed Oct 31, 2018 218 219 `````` 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 220 `````` the reflection mechanism that was needed for proving closedness, atomicity and `````` Jacques-Henri Jourdan committed Oct 31, 2018 221 222 `````` "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 223 224 ``````* heap_lang now has support for allocating, accessing and reasoning about arrays (continuously allocated regions of memory). `````` Robbert Krebbers committed Jun 10, 2019 225 ``````* One can now assign "meta" data to heap_lang locations. `````` Ralf Jung committed Jan 24, 2018 226 `````` `````` Ralf Jung committed Aug 28, 2019 227 228 ``````[prophecy-erasure]: https://gitlab.mpi-sws.org/iris/examples/blob/3f33781fe6e19cfdb25259c8194d34403f1134d5/theories/logatom/proph_erasure.v `````` Ralf Jung committed Aug 29, 2019 229 ``````**Changes in Coq:** `````` Robbert Krebbers committed Jan 03, 2018 230 `````` `````` Ralf Jung committed Aug 28, 2019 231 ``````* An all-new generalized proof mode that abstracts away from Iris! Major new `````` Ralf Jung committed Jul 09, 2018 232 233 234 235 236 237 `````` 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 238 `````` an existing logic (see the paper for more details). `````` Ralf Jung committed Jul 09, 2018 239 `````` Developments instantiating the proof mode typeclasses may need significant `````` Robbert Krebbers committed May 02, 2019 240 241 `````` 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 242 243 244 245 246 `````` - 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 247 `````` searching for the BI to use, which (due to Coq limitations) can lead to `````` Ralf Jung committed Jul 02, 2018 248 249 250 251 `````` 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 252 253 ``````* 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 254 255 ``````* Added support for defining derived connectives involving n-ary binders using telescopes. `````` Ralf Jung committed Jul 06, 2018 256 257 258 ``````* 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 259 ``````* Improved pretty-printing of Iris connectives (in particular WP and fancy `````` Ralf Jung committed Jul 06, 2018 260 261 262 `````` 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. `````` Robbert Krebbers committed Jan 03, 2018 263 ``````* Rename `timelessP` -> `timeless` (projection of the `Timeless` class) `````` Ralf Jung committed Feb 20, 2018 264 265 ``````* 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 266 `````` CMRA even for an infinite domain. `````` Robbert Krebbers committed Feb 20, 2018 267 268 269 270 271 ``````* 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` `````` 272 273 ``````* Rename: - `frag_auth_op` → `frac_auth_frag_op` `````` 274 275 276 `````` - `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 277 ``````* `namespaces` has been moved to std++. `````` Ralf Jung committed Jun 18, 2018 278 279 ``````* 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 280 ``````* `wp_fork` is now written in curried form. `````` Robbert Krebbers committed Oct 05, 2018 281 ``````* `PureExec`/`wp_pure` now supports taking multiple steps at once. `````` Jacques-Henri Jourdan committed Oct 31, 2018 282 283 284 ``````* 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 285 ``````* Add `big_sepM_insert_acc`. `````` Dan Frumin committed Apr 07, 2019 286 287 288 289 ``````* 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 290 291 292 ``````* 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 293 294 295 ``````* 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 296 ``````* Export the fact that `iPreProp` is a COFE. `````` Hai Dang committed May 23, 2019 297 298 299 300 301 302 303 ``````* 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 304 305 ``````* Add a COFE construction (and functor) on dependent pairs `sigTO`, dual to `discrete_funO`. `````` Hai Dang committed May 24, 2019 306 307 308 309 310 311 ``````* 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 312 313 314 315 316 `````` 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 317 318 `````` - `auth_both_valid` → `auth_both_valid_2` - `auth_valid_discrete_2` → `auth_both_valid` `````` Robbert Krebbers committed Jun 11, 2019 319 320 321 ``````* Add the camera `ufrac` for unbounded fractions (i.e. without fractions that can be `> 1`) and the camera `ufrac_auth` for a variant of the authoritative fractional camera (`frac_auth`) with unbounded fractions. `````` Ralf Jung committed Jun 11, 2019 322 323 ``````* Changed `frac_auth` notation from `●!`/`◯!` to `●F`/`◯F`. sed script: `s/◯!/◯F/g; s/●!/●F/g;`. `````` Paolo G. Giarrusso committed Aug 08, 2019 324 325 ``````* Lemma `prop_ext` works in both directions; its default direction is the opposite of what it used to be. `````` Paolo G. Giarrusso committed Aug 13, 2019 326 ``````* Make direction of `f_op` rewrite lemmas more consistent: Flip `pair_op`, `````` Paolo G. Giarrusso committed Aug 13, 2019 327 328 `````` `Cinl_op`, `Cinr_op`, `cmra_morphism_op`, `cmra_morphism_pcore`, `cmra_morphism_core`. `````` Robbert Krebbers committed Aug 24, 2019 329 330 ``````* Rename lemmas `fupd_big_sep{L,M,S,MS}` into `big_sep{L,M,S,MS}_fupd` to be consistent with other such big op lemmas. Also add such lemmas for `bupd`. `````` Robbert Krebbers committed Jun 18, 2019 331 ``````* Rename `C` suffixes into `O` since we no longer use COFEs but OFEs. Also `````` Ralf Jung committed Jun 18, 2019 332 `````` rename `ofe_fun` into `discrete_fun` and the corresponding notation `-c>` into `````` Ralf Jung committed Apr 02, 2020 333 334 `````` `-d>`. The renaming can be automatically done using the following script (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`): `````` Robbert Krebbers committed Jun 18, 2019 335 ````````` `````` Paolo G. Giarrusso committed Jun 21, 2019 336 ``````sed -i ' `````` Robbert Krebbers committed Jun 18, 2019 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 ``````s/\bCofeMor/OfeMor/g; s/\-c>/\-d>/g; s/\bcFunctor/oFunctor/g; s/\bCFunctor/OFunctor/g; s/\b\%CF/\%OF/g; s/\bconstCF/constOF/g; s/\bidCF/idOF/g s/\bdiscreteC/discreteO/g; s/\bleibnizC/leibnizO/g; s/\bunitC/unitO/g; s/\bprodC/prodO/g; s/\bsumC/sumO/g; s/\bboolC/boolO/g; s/\bnatC/natO/g; s/\bpositiveC/positiveO/g; s/\bNC/NO/g; s/\bZC/ZO/g; s/\boptionC/optionO/g; s/\blaterC/laterO/g; s/\bofe\_fun/discrete\_fun/g; s/\bdiscrete\_funC/discrete\_funO/g; s/\bofe\_morC/ofe\_morO/g; s/\bsigC/sigO/g; s/\buPredC/uPredO/g; s/\bcsumC/csumO/g; s/\bagreeC/agreeO/g; s/\bauthC/authO/g; s/\bnamespace_mapC/namespace\_mapO/g; s/\bcmra\_ofeC/cmra\_ofeO/g; s/\bucmra\_ofeC/ucmra\_ofeO/g; s/\bexclC/exclO/g; s/\bgmapC/gmapO/g; s/\blistC/listO/g; s/\bvecC/vecO/g; s/\bgsetC/gsetO/g; s/\bgset\_disjC/gset\_disjO/g; s/\bcoPsetC/coPsetO/g; s/\bgmultisetC/gmultisetO/g; s/\bufracC/ufracO/g s/\bfracC/fracO/g; s/\bvalidityC/validityO/g; s/\bbi\_ofeC/bi\_ofeO/g; s/\bsbi\_ofeC/sbi\_ofeO/g; s/\bmonPredC/monPredO/g; s/\bstateC/stateO/g; s/\bvalC/valO/g; s/\bexprC/exprO/g; s/\blocC/locO/g; s/\bdec\_agreeC/dec\_agreeO/g; s/\bgnameC/gnameO/g; s/\bcoPset\_disjC/coPset\_disjO/g; `````` Paolo G. Giarrusso committed Jun 21, 2019 388 ``````' \$(find theories -name "*.v") `````` Robbert Krebbers committed Jun 18, 2019 389 ````````` `````` Hai Dang committed May 24, 2019 390 `````` `````` Ralf Jung committed Dec 19, 2017 391 ``````## Iris 3.1.0 (released 2017-12-19) `````` Ralf Jung committed Apr 12, 2017 392 `````` `````` Ralf Jung committed Aug 29, 2019 393 ``````**Changes in and extensions of the theory:** `````` Ralf Jung committed Oct 26, 2017 394 `````` `````` Ralf Jung committed Dec 11, 2017 395 ``````* Define `uPred` as a quotient on monotone predicates `M -> SProp`. `````` Ralf Jung committed Dec 13, 2017 396 397 ``````* Get rid of some primitive laws; they can be derived: `True ⊢ □ True` and `□ (P ∧ Q) ⊢ □ (P ∗ Q)` `````` Ralf Jung committed Nov 23, 2017 398 ``````* Camera morphisms have to be homomorphisms, not just monotone functions. `````` Ralf Jung committed Oct 28, 2017 399 ``````* Add a proof that `f` has a fixed point if `f^k` is contractive. `````` Robbert Krebbers committed Oct 26, 2017 400 401 ``````* Constructions for least and greatest fixed points over monotone predicates (defined in the logic of Iris using impredicative quantification). `````` Ralf Jung committed Oct 28, 2017 402 ``````* Add a proof of the inverse of `wp_bind`. `````` Ralf Jung committed Dec 13, 2017 403 ``````* [Experimental feature] Add new modality: ■ ("plainly"). `````` Ralf Jung committed Dec 11, 2017 404 405 406 407 408 409 410 411 ``````* [Experimental feature] Support verifying code that might get stuck by distinguishing "non-stuck" vs. "(potentially) stuck" weakest preconditions. (See [Swasey et al., OOPSLA '17] for examples.) The non-stuck `WP e @ E {{ Φ }}` ensures that, as `e` runs, it does not get stuck. The stuck `WP e @ E ?{{ Φ }}` ensures that, as usual, all invariants are preserved while `e` runs, but it permits execution to get stuck. The former implies the latter. The full judgment is `WP e @ s; E {{ Φ }}`, where non-stuck WP uses *stuckness bit* `s = NotStuck` while stuck WP uses `s = MaybeStuck`. `````` Ralf Jung committed Oct 26, 2017 412 `````` `````` Ralf Jung committed Aug 29, 2019 413 ``````**Changes in Coq:** `````` Ralf Jung committed Oct 26, 2017 414 `````` `````` Robbert Krebbers committed Dec 14, 2017 415 416 ``````* Move the `prelude` folder to its own project: [coq-std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp) `````` Ralf Jung committed Dec 13, 2017 417 418 419 420 421 422 423 424 425 426 427 ``````* Some extensions/improvements of heap_lang: - Improve handling of pure (non-state-dependent) reductions. - Add fetch-and-add (`FAA`) operation. - Add syntax for all Coq's binary operations on `Z`. * Generalize `saved_prop` to let the user choose the location of the type-level later. Rename the general form to `saved_anything`. Provide `saved_prop` and `saved_pred` as special cases. * Improved big operators: + They are no longer tied to cameras, but work on any monoid + The version of big operations over lists was redefined so that it enjoys more definitional equalities. `````` Ralf Jung committed Oct 28, 2017 428 ``````* Rename some things and change notation: `````` Robbert Krebbers committed Oct 26, 2017 429 `````` - The unit of a camera: `empty` -> `unit`, `∅` -> `ε` `````` Ralf Jung committed Oct 29, 2017 430 `````` - Disjointness: `⊥` -> `##` `````` Ralf Jung committed Oct 28, 2017 431 `````` - A proof mode type class `IntoOp` -> `IsOp` `````` Robbert Krebbers committed Oct 26, 2017 432 433 434 435 436 437 `````` - OFEs with all elements being discrete: `Discrete` -> `OfeDiscrete` - OFE elements whose equality is discrete: `Timeless` -> `Discrete` - Timeless propositions: `TimelessP` -> `Timeless` - Camera elements such that `core x = x`: `Persistent` -> `CoreId` - Persistent propositions: `PersistentP` -> `Persistent` - The persistent modality: `always` -> `persistently` `````` Ralf Jung committed Dec 07, 2017 438 `````` - Adequacy for non-stuck weakestpre: `adequate_safe` -> `adequate_not_stuck` `````` Ralf Jung committed Oct 26, 2017 439 `````` - Consistently SnakeCase identifiers: `````` Robbert Krebbers committed Oct 26, 2017 440 441 442 443 444 445 446 447 448 449 `````` + `CMRAMixin` -> `CmraMixin` + `CMRAT` -> `CmraT` + `CMRATotal` -> `CmraTotal` + `CMRAMorphism` -> `CmraMorphism` + `CMRADiscrete` -> `CmraDiscrete` + `UCMRAMixin` -> `UcmraMixin` + `UCMRAT` -> `UcmraT` + `DRAMixin` -> `DraMixin` + `DRAT` -> `DraT` + `STS` -> `Sts` `````` Ralf Jung committed Oct 28, 2017 450 451 `````` - Many lemmas also changed their name. `always_*` became `persistently_*`, and furthermore: (the following list is not complete) `````` Robbert Krebbers committed Oct 26, 2017 452 453 454 455 456 457 458 459 460 461 `````` + `impl_wand` -> `impl_wand_1` (it only involves one direction of the equivalent) + `always_impl_wand` -> `impl_wand` + `always_and_sep_l` -> `and_sep_l` + `always_and_sep_r` -> `and_sep_r` + `always_sep_dup` -> `sep_dup` + `wand_impl_always` -> `impl_wand_persistently` (additionally, the direction of this equivalence got swapped for consistency's sake) + `always_wand_impl` -> `persistently_impl_wand` (additionally, the direction of this equivalence got swapped for consistency's sake) `````` Ralf Jung committed Jun 12, 2019 462 `````` The following `sed` snippet should get you most of the way (on macOS you will `````` Paolo G. Giarrusso committed Jun 21, 2019 463 `````` have to replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`): `````` Ralf Jung committed Oct 26, 2017 464 ````````` `````` Paolo G. Giarrusso committed Jun 21, 2019 465 ``````sed -i 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscrete\b/CmraDiscrete/g; s/\bCMRAT\b/CmraT/g; s/\bCMRAMixin\b/CmraMixin/g; s/\bUCMRAT\b/UcmraT/g; s/\bUCMRAMixin\b/UcmraMixin/g; s/\bSTS\b/Sts/g' \$(find -name "*.v") `````` Ralf Jung committed Oct 26, 2017 466 ````````` `````` Ralf Jung committed Dec 13, 2017 467 468 ``````* `PersistentL` and `TimelessL` (persistence and timelessness of lists of propositions) are replaces by `TCForall` from std++. `````` Ralf Jung committed Oct 26, 2017 469 470 ``````* Fix a bunch of consistency issues in the proof mode, and make it overall more usable. In particular: `````` Robbert Krebbers committed Oct 26, 2017 471 472 473 474 475 476 477 478 479 480 `````` - All proof mode tactics start the proof mode if necessary; `iStartProof` is no longer needed and should only be used for building custom proof mode tactics. - Change in the grammar of specialization patterns: `>[...]` -> `[> ...]` - Various new specification patterns for `done` and framing. - There is common machinery for symbolic execution of pure reductions. This is provided by the type classes `PureExec` and `IntoVal`. - There is a new connective `tc_opaque`, which can be used to make definitions opaque for type classes, and thus opaque for most tactics of the proof mode. `````` Ralf Jung committed Oct 28, 2017 481 482 483 484 485 486 487 488 `````` - Define Many missing type class instances for distributing connectives. - Implement the tactics `iIntros (?)` and `iIntros "!#"` (i.e. `iAlways`) using type classes. This makes them more generic, e.g., `iIntros (?)` also works when the universal quantifier is below a modality, and `iAlways` also works for the plainness modality. A breaking change, however, is that these tactics now no longer work when the universal quantifier or modality is behind a type class opaque definition. Furthermore, this can change the name of anonymous identifiers introduced with the "%" pattern. `````` Ralf Jung committed Nov 24, 2017 489 ``````* Make `ofe_fun` dependently typed, subsuming `iprod`. The latter got removed. `````` Ralf Jung committed Oct 28, 2017 490 491 492 ``````* Define the generic `fill` operation of the `ectxi_language` construct in terms of a left fold instead of a right fold. This gives rise to more definitional equalities. `````` Robbert Krebbers committed Nov 23, 2017 493 494 495 496 497 ``````* The language hierarchy (`language`, `ectx_language`, `ectxi_language`) is now fully formalized using canonical structures instead of using a mixture of type classes and canonical structures. Also, it now uses explicit mixins. The file `program_logic/ectxi_language` contains some documentation on how to setup Iris for your language. `````` Ralf Jung committed Dec 13, 2017 498 499 ``````* Restore the original, stronger notion of atomicity alongside the weaker notion. These are `Atomic a e` where the stuckness bit `s` indicates whether `````` Robbert Krebbers committed Dec 14, 2017 500 501 `````` expression `e` is weakly (`a = WeaklyAtomic`) or strongly (`a = StronglyAtomic`) atomic. `````` Robbert Krebbers committed Oct 26, 2017 502 503 504 505 ``````* Various improvements to `solve_ndisj`. * Use `Hint Mode` to prevent Coq from making arbitrary guesses in the presence of evars, which often led to divergence. There are a few places where type annotations are now needed. `````` Robbert Krebbers committed Oct 29, 2017 506 ``````* The rules `internal_eq_rewrite` and `internal_eq_rewrite_contractive` are now `````` Ralf Jung committed Dec 13, 2017 507 `````` stated in the logic, i.e., they are `iApply`-friendly. `````` Ralf Jung committed Apr 12, 2017 508 `````` `````` Ralf Jung committed Jan 11, 2017 509 ``````## Iris 3.0.0 (released 2017-01-11) `````` Ralf Jung committed Aug 08, 2016 510 `````` `````` Ralf Jung committed Dec 12, 2016 511 512 513 ``````* There now is a deprecation process. The modules `*.deprecated` contain deprecated notations and definitions that are provided for backwards compatibility and will be removed in a future version of Iris. `````` Ralf Jung committed Oct 10, 2016 514 ``````* View shifts are radically simplified to just internalize frame-preserving `````` Ralf Jung committed Aug 08, 2016 515 `````` updates. Weakestpre is defined inside the logic, and invariants and view `````` Ralf Jung committed Dec 09, 2016 516 `````` shifts with masks are also coded up inside Iris. Adequacy of weakestpre is `````` Ralf Jung committed Dec 12, 2016 517 `````` proven in the logic. The old ownership of the entire physical state is `````` Ralf Jung committed Dec 09, 2016 518 519 `````` replaced by a user-selected predicate over physical state that is maintained by weakestpre. `````` Ralf Jung committed Dec 05, 2016 520 ``````* Use OFEs instead of COFEs everywhere. COFEs are only used for solving the `````` Ralf Jung committed Dec 12, 2016 521 522 `````` recursive domain equation. As a consequence, CMRAs no longer need a proof of completeness. (The old `cofeT` is provided by `algebra.deprecated`.) `````` Ralf Jung committed Dec 05, 2016 523 ``````* Implement a new agreement construction. Unlike the old one, this one `````` Ralf Jung committed Dec 13, 2016 524 525 `````` preserves discreteness. dec_agree is thus no longer needed and has been moved to algebra.deprecated. `````` Ralf Jung committed Dec 12, 2016 526 527 528 ``````* Renaming and moving things around: uPred and the rest of the base logic are in `base_logic`, while `program_logic` is for everything involving the general Iris notion of a language. `````` Ralf Jung committed Jan 11, 2017 529 530 531 532 ``````* Renaming in prelude.list: Rename `prefix_of` -> `prefix` and `suffix_of` -> `suffix` in lemma names, but keep notation ``l1 `prefix_of` l2`` and ``l1 `suffix_of` l2``. `` l1 `sublist` l2`` becomes ``l1 `sublist_of` l2``. Rename `contains` -> `submseteq` and change `` l1 `contains` l2`` to ``l1 ⊆+ l2``. `````` Ralf Jung committed Dec 12, 2016 533 534 535 ``````* Slightly weaker notion of atomicity: an expression is atomic if it reduces in one step to something that does not reduce further. * Changed notation for embedding Coq assertions into Iris. The new notation is `````` Ralf Jung committed Oct 29, 2017 536 `````` ⌜φ⌝. Also removed `=` and `⊥` from the Iris scope. (The old notations are `````` Ralf Jung committed Dec 12, 2016 537 `````` provided in `base_logic.deprecated`.) `````` Ralf Jung committed Nov 22, 2016 538 ``````* Up-closure of namespaces is now a notation (↑) instead of a coercion. `````` Ralf Jung committed Dec 12, 2016 539 540 ``````* With invariants and the physical state being handled in the logic, there is no longer any reason to demand the CMRA unit to be discrete. `````` Ralf Jung committed Oct 10, 2016 541 ``````* The language can now fork off multiple threads at once. `````` Ralf Jung committed Dec 12, 2016 542 543 ``````* Local Updates (for the authoritative monoid) are now a 4-way relation with syntax-directed lemmas proving them. `````` Ralf Jung committed Jul 25, 2016 544 545 546 `````` ## Iris 2.0 `````` Ralf Jung committed Jul 25, 2016 547 548 549 550 ``````* [heap_lang] No longer use dependent types for expressions. Instead, values carry a proof of closedness. Substitution, closedness and value-ness proofs are performed by computation after reflecting into a term langauge that knows about values and closed expressions. `````` Ralf Jung committed Jul 25, 2016 551 552 ``````* [program_logic/language] The language does not define its own "atomic" predicate. Instead, atomicity is defined as reducing in one step to a value. `````` Ralf Jung committed Aug 09, 2016 553 554 555 556 557 ``````* [program_logic] Due to a lack of maintenance and usefulness, lifting lemmas for Hoare triples are removed. ## Iris 2.0-rc2 `````` Ralf Jung committed Dec 12, 2016 558 ``````This version matches the final ICFP 2016 paper. `````` Ralf Jung committed Aug 09, 2016 559 560 `````` * [algebra] Make the core of an RA or CMRA a partial function. `````` Ralf Jung committed Jul 27, 2016 561 ``````* [program_logic/lifting] Lifting lemmas no longer round-trip through a `````` Ralf Jung committed Jul 27, 2016 562 563 564 `````` user-chosen predicate to define the configurations we can reduce to; they directly relate to the operational semantics. This is equivalent and much simpler to read. `````` Ralf Jung committed Jul 25, 2016 565 566 567 `````` ## Iris 2.0-rc1 `````` Ralf Jung committed Dec 12, 2016 568 ``This is the Coq development and Iris Documentation as submitted to ICFP 2016.``