Lean 4 port of Iris, a higher-order concurrent separation logic framework.

About Iris

"Iris is a framework that can be used for reasoning about safety of concurrent programs, as the logic in logical relations, to reason about type-systems, data-abstraction etc."
– https://iris-project.org/

Rocq formalization of Iris: https://gitlab.mpi-sws.org/iris/iris/

Project

Currently, Iris-Lean has support for

• MoSeL, the proof interface of Iris
• IProp, the standard model of Iris
• HeapLang, the Iris example language and logic
• A selection of the Iris resources, including invariants, later credits, and many more.

Users of Iris-Lean should be aware of the documentation:

• tactics.md: Instructions for using Iris tactics.
• tracking site: Iris-Lean correspondence for definitions in Iris-Rocq.
• compatibility.md: Important differences between Iris-Rocq and Iris-Lean.
• proofmode.md: Details of MoSeL; support for separation logics other than Iris.

Using Iris-Lean as a Dependency

• Iris-Lean is updated in sync with Lean. The releases page includes tags for recent versions.
• The master branch may contain features added since the last release:

[[require]]
name = "iris"
git.url = "https://github.com/leanprover-community/iris-lean.git" 
git.subDir = "Iris" 
rev = "master"

• To use Iris constructions based on mathlib, you can also import the math library

[[require]]
name = "iris"
git.url = "https://github.com/leanprover-community/iris-lean.git" 
git.subDir = "IrisMath" 
rev = "master"

Development

Development for Iris-Lean coordinates in:

• The iris-lean channel on the Lean Zulip.
• The Iris Mattermost channel

We always welcome new contributors! For questions, contribution guidance, and development information, feel free to introduce yourself on the Zulip.

Miscellaneous

Unicode Input

Most of the unicode characters used in Iris can be written with the Lean extension replacement, e.g. \ast will automatically be replaced with ∗. To add additional replacements, edit the Lean extension setting lean4.input.customTranslations. Suggested additional replacements are listed below.

"sep": "∗",
"wand": "-∗",
"pure": "⌜⌝",
"bientails": "⊣⊢",
"emb": "⎡⎤",
"auth": "●", 
"frag": "◯",
"incl": "≼", 
"valid": "✓",
"later": "▷",
"except0": "◇",
"plainly": "■",
"intuit": "□",
"credit": "£",

References

• koenig22, Master Thesis, An Improved Interface for Interactive Proofs in Separation Logic, 2022-10, Lars König, KIT.
• demedeiros26, Draft paper. Iris in Lean, Markus de Medeiros, Sergei Stepanenko, Zongyuan Liu, Oliver Soeser, Fernando Leal, Alvin Tang, Max Vistrup, Ralf Jung, Mario Carneiro, Joseph Tassarotti, Michael Sammler, and Lars Birkedal.