Hi everyone,
We are happy to announce the release of Iris 4.0 and std++ 1.8. 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.
The highlight of Iris 4.0 is the later credits mechanism, which provides a new way to eliminate later modalities.
This new mechanism complements the existing techniques of taking program steps, exploiting timelessness, and various modality commuting rules. At each program step, one obtains a credit £ 1, which is an ownable Iris resource. These credits don’t have to be used at the present step, but can be saved up, and used to eliminate laters at any point in the verification using the fancy update modality. Later credits are particularly useful in proofs where there is not a one-to-one correspondence between program steps and later eliminations, for example, logical atomicity proofs. As a consequence, we have been able to simplify the definition of logical atomicity by removing the ‘laterable’ mechanism.
The later credit mechanism is described in detail in the ICFP’22 paper and there is a small tutorial in the Iris repository. The examples repository contains some logically atomic case studies that make use of later credits: the counter with a backup (Section 4 of the later credits paper), as well as the elimination stack, conditional increment, and RDCSS.
Iris 4.0 supports Coq 8.13 - 8.16. For all the details, and a sed script that helps with porting code using Iris, see the changelog.
This release was managed by Ralf Jung, Robbert Krebbers, and Lennard Gäher, with contributions from Glen Mével, Gregory Malecha, Ike Mulder, Irene Yoon, Jan-Oliver Kaiser, Jonas Kastberg Hinrichsen, Lennard Gäher, Michael Sammler, Niklas Mück, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Spies, and Tej Chajed. Thanks a lot to everyone involved!
For std++, Coq 8.16 is newly supported by this release, and Coq 8.12 to 8.15 remain supported. Coq 8.11 is no longer supported. For more details, see the changelog.
This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Lennard Gäher, with contributions from Andrej Dudenhefner, Dan Frumin, Gregory Malecha, Jan-Oliver Kaiser, Lennard Gäher, Léo tefanesco, Michael Sammler, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, and Vincent Siles. 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