Iris 4.5 and std++ 1.13 release

Announcements
1

Hi everyone,

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

For Iris, the main features this release are

  • A new class for a “step-indexed BI logic” (Sbi), which gives a generic treatment of step-indexed operations such as “internal validity” ≡, “internal CMRA validity” ✓, the “plainly modality” ■, plain propositions Plain, and the soundness lemmas. Each BI logic (e.g., iProp, monPred, ironProp, siProp) gets these features for free by inhabiting Sbi.

  • The proofmode tactics have been ported to use Rocq’s better behaved unification algorithm (“evarconv”) instead of legacy unification.

  • The tactics iNext and wp_pure have been extended with support for for later credits.

For stdpp the main feature this release is that the lemmas for lookup and commuting operations on lists and maps have been made more ergonomic (particularly, new lemmas combine the cases for = and ≠) and made more consistent.

Matching the rename of Rocq itself, the opam packages have been renamed to rocq-iris and rocq-stdpp respectively.

The supported Rocq versions for both Iris and std++ are 9.0, 9.1, and 9.2.

For further details, see the full changelog of Iris at https://gitlab.mpi-sws.org/iris/iris/-/blob/master/CHANGELOG.md?ref_type=heads
and std++ at https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/CHANGELOG.md?ref_type=heads.

This release was managed by Jesper Bengtson, Ralf Jung, and Robbert Krebbers.

Iris received contributions from Alessio Duè, Arnaud Daby-Seesaram, Arthur Azevedo de Amorim, Benjamin Peters, Enrico Tassi, Hai Dang, Isaac van Bakel, Jan-Oliver Kaiser, Johannes Hostert, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, Rodolphe Lepigre, Rudy Peterson, Sanjit Bhat, Simcha van Collem, Tej Chajed, Yiqun Liu, and Zichen Zhang.

std++ received contributions from Andres Erbsen, Benjamin Peters, Brian Campbell, Egor Namakonov, François Pottier, Isaac van Bakel, Jan-Oliver Kaiser, Johannes Hostert, Jonas Kastberg Hinrichsen, Kimaya Bedarkar, Marijn van Wezel, Michael Sammler, Nikhil Chatterjee, Niklas Mück, Pierre Roux, Ralf Jung, Robbert Krebbers, Rodolphe Lepigre, Rudy Peterson, Sanjit Bhat, Simcha van Collem, Tej Chajed, and Zichen Zhang.

Thanks a lot to everyone involved!

Both packages are available in the Rocq opam registry. For further information and installation instructions for Iris and std++, see the respective project websites:
https://gitlab.mpi-sws.org/iris/iris
https://gitlab.mpi-sws.org/iris/stdpp

If you have any questions, feel free to reply to this email, or join our Iris community chat room: Iris Chat Room: https://iris-project.org/chat.html.

Best,

The Iris and std++ teams