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 (
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 -∗ Qas a Coq proposition has changed from
P ⊢ Qto
⊢ P -∗ Q. If you are only using the Iris proofmode, this will not make a difference, but when writing proof scripts or tactics that
applyIris lemmas, the exact position of the
⊢ P -∗ Qmatters and this will now always be visible in lemma statements.
iCombineis starting to gain support for a
givesclause, 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
ownand 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:
mra(the monotone resource algebra of https://iris-project.org/pdfs/2021-CPP-monotone-final.pdf)
For std++, the highlights of this release are:
gmapand 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
oinversionetc are added. These tactics improve upon
edestructby 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
edestructfails. This can significantly shorten the overhead involved in forward reasoning proofs. For more information, see the test cases provided 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.
The Iris and std++ teams