Iris 4.4

Stream: iris-lean

[Mario Carneiro]

News from Rocq Iris:

Hi everyone,

We are happy to announce the release of Iris 4.4 and std++ 1.12. 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.

The main new Iris features are support for transfinite step-indexing for
resource algebras, and new proof rules for reasoning about propositions of the
form ∀ .. own and own .. ∧ own ... Otherwise, these releases mostly include
quality of life improvements.

For Iris, the supported Rocq versions are 8.19 - 9.0, while std++ also supports
version 8.18.

For further details, see the full changelog of Iris at
https://gitlab.mpi-sws.org/iris/iris/-/blob/master/CHANGELOG.md#iris-440-2025-06-04
and std++ at
https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/CHANGELOG.md#1120-2025-06-04.

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

std++ received contributions from Andres Erbsen, Kimaya Bedarkar, Marijn van
Wezel, Michael Sammler, Ralf Jung, Robbert Krebbers, Rodolphe Lepigre, Rudy
Peterson, and Marijn van Wezel.

Iris received contributions from Benjamin Peters, Daniel Nezamabadi, Ike Mulder,
Isaac van Bakel, Jan-Oliver Kaiser, Janggun Lee, Johannes Hostert, Lennard
Gäher, Michael Sammler, Paolo G. Giarrusso, Pierre Roux, Ralf Jung, Robbert
Krebbers, Rodolphe Lepigre, Sanjit Bhat, Tej Chajed, Travis Hance, William
Mansky, Yixuan Chen, Yiyun Liu, Yusuke Matsushita, Rudy Peterson, and Thomas Somers.
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.

We are also happy to announce iris-contrib
(https://gitlab.mpi-sws.org/iris/iris-contrib) on behalf of the iris-contrib
maintainers:
Iris-contrib is meant to collect community additions to Iris and std++,
especially in the form of utility lemmas. As such, it is the ideal destination
for the collected lemmas in everyone's util.v files. :) And if you need a lemma
that you cannot find in Iris or std++, maybe someone has already proved it in
iris-contrib!
Iris-contrib has low requirements for MRs (see the README) -- as long as it
compiles and you put your lemmas in sensible places, you should be good. The
plan for popular additions is to eventually upstream them to Iris or std++. We
hope that iris-contrib will also be a useful staging ground for trying out and
discussing additions.
Iris-contrib is maintained by Vincent Lafeychine and Lennard Gäher. We aim to
ensure compatibility with Iris master and that iris-contrib always builds, but
provide no further stability guarantees.

Best,
The Iris and std++ teams

[Mario Carneiro]

transfinite step indexing is probably the most relevant update for us

[Markus de Medeiros]

Nice! I didn't know that effort was so far along.