Iris 4.2 and std++ 1.10

Announcements
1

Hi everyone,

We are happy to announce the release of Iris 4.2 and std++ 1.10. 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 highlights of this new Iris version are:

  • We have new laws to “undiscard” discarded fractions, allowing one to update from DfracDiscarded to DfracOwn(q) for some fresh q. This gives rise to new laws for all constructions that use dfrac, such as ghost_map_elem_unpersist : ∀ k γ v, k ↪[γ]□ v ==∗ ∃ q, k ↪[γ]{#q} v.
  • The gmap_view K V camera now supports value types V that are arbitrary cameras, and lifts their composition to the whole map. The previous gmap_view type can be recovered as gmap_view K (agree V).
  • The iFrame tactic has become stronger for goals that contain existential quantifiers: iFrame will now attempt to instantiate these. For example, framing P x in goal Q ∗ ∃ y, P y ∗ R will now succeed with remaining goal Q ∗ R.

For std++, the biggest new feature in this release is the bitvector library with support for fixed-size integers. It is distributed as a separate package, coq-stdpp-bitvector. The library is developed and maintained by Michael
Sammler.

The supported Coq versions are 8.18 and 8.19.

For further details, see the full changelog of Iris at CHANGELOG.md · master · Iris / Iris · GitLab and std++ at CHANGELOG.md · master · Iris / stdpp · GitLab.

This release was managed by Ralf Jung and Robbert Krebbers.

std++ received further contributions from Mathias Adam Møller, Michael Sammler, Pierre Rousselin, Pierre Roux, and Thibaut Pérami.

Iris received further contributions from Ike Mulder, Jan-Oliver Kaiser, Johannes Hostert, Pierre Roux, Thomas Somers, and Yixuan Chen.

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: Iris Chat Room.

Best,
The Iris and std++ teams