Iris 4.1 and std++ 1.9 released

Announcements
1

Hello everyone,

We are happy to announce the release of Iris 4.1 and std++ 1.9. Iris is a concurrent separation logic framework for Coq; for an overview of the numerous research projects employing Iris, see https://iris-project.org/. std++ is an extended “standard” library for Coq.

This Iris release mostly features quality-of-life improvements, such as smarter handling of ->/<- patterns by iDestruct, support for an arbitrary number of Coq intro patterns in the Iris proofmode tactics (iIntros, iDestruct, etc.), and support for immediately introducing the postcondition of a WP specification via wp_apply lemma as "Hpost".

The biggest changes and new features are:

  • Logically atomic triples now support private (non-atomic) postconditions, and the notation was changed to not clash with Autosubst any more. Existing users of logically atomic specifications have to update their notation, see the full CHANGELOG for more details.

  • The meaning of P -∗ Q as a Coq proposition has changed from P ⊢ Q to ⊢ P -∗ Q. If you are only using the Iris proofmode, this will not make a difference, but when writing proof scripts or tactics that rewrite or apply Iris lemmas, the exact position of the ⊢ P -∗ Q matters and this will now always be visible in lemma statements.

  • iCombine is starting to gain support for a gives clause, which yields persistent facts gained from combining the resources. So far, this remains mostly experimental. We support ↦ and the connectives of ghost theories in base_logic/lib, but support for own and custom cameras is minimal and will be improved in future releases.

  • Some initial refactoring prepares Iris for eventually supporting transfinite step-indexing.

  • New resources algebras have been added: Z, max_Z, mono_Z, and mra (the monotone resource algebra of https://iris-project.org/pdfs/2021-CPP-monotone-final.pdf)

For std++, the highlights of this release are:

  • gmap and related types are re-implemented based on Appel and Leroy’s Efficient Extensional Binary Tries, making them usable in nested inductive definitions and improving extensionality. More information can be found in Robbert Krebbers’ Coq Workshop talk, see The Coq Workshop 2023

  • New tactics ospecialize, odestruct, oinversion etc are added. These tactics improve upon efeed / edestruct by allowing one to leave more terms open when specializing arguments. For instance, odestruct (H _ x) will turn the _ into an evar rather than trying to infer it immediately, making it usable in many situations where edestruct fails. This can significantly shorten the overhead involved in forward reasoning proofs. For more information, see the test cases provided here.

For further details, see the full changelog of Iris here and std++ here

Iris 4.1 and std++ 1.9 support Coq 8.16-8.18.

This release of Iris and std++ was managed by Ralf Jung, Robbert Krebbers, and Johannes Hostert.

This Iris release received contributions from Amin Timany, Arthur Azevedo de Amorim, Armaël Guéneau, Benjamin Peters, Dan Frumin, Dorian Lesbre, Ike Mulder, Isaac van Bakel, Jaemin Choi, Janine Lohse, Jan-Oliver Kaiser, Jonas Kastberg Hinrichsen, Lennard Gäher, Mathias Adam Møller, Michael Sammler, Paolo Giarrusso, Pierre Roux, Rodolphe Lepigre, Simcha van Collem, Simon Friis Vindum, Simon Spies, Tej Chajed, Yixuan Chen, and Yusuke Matsushita.

This std++ release received contributions from Dorian Lesbre, Herman Bergwerf, Ike Mulder, Isaac van Bakel, Jan-Oliver Kaiser, Jonas Kastberg, Marijn van Wezel, Michael Sammler, Paolo Giarrusso, Tej Chajed, and Thibaut Pérami.

Thanks a lot to everyone involved!

Both packages are available in the Coq opam registry. For further information and installation instructions for Iris and std++, see the respective project websites:

If you have any questions, feel free to reply to this email, or join our Iris community chat room.

Best,

The Iris and std++ teams