Lean features simplify and speed up Iris concurrency proofs
Iris in Lean
Logic in Computer ScienceProgramming Languages
Summary
Verifying that programs with multiple parts running at the same time behave correctly is very challenging. Iris is a framework that helps by using a special kind of logic with powerful tools built in the Coq system. The authors show how moving Iris to the Lean proof assistant, which has flexible programming features and other advantages, makes the logic easier to use and faster. They also combine Iris with a large math library in Lean to check programs that involve probability. This work helps programmers and tool builders verify complex software more efficiently.
What this means in practice
- •For software verification engineers: Use the Lean-based Iris framework to verify concurrent programs with improved proof automation and handling of logic resources.
- •For formal methods tool developers: Build verification tools by integrating Iris logic with Lean’s metaprogramming and math libraries to handle complex program properties including probabilistic reasoning.
Authors
Markus de Medeiros, Sergei Stepanenko, Zongyuan Liu, Oliver Soeser, Fernando Leal, Alvin Tang, Max Vistrup, Ralf Jung, Mario Carneiro, Joseph Tassarotti, Michael Sammler, Lars Birkedal
Abstract
The Iris framework for concurrent separation logic has been widely used for program verification research. An important factor contributing to the framework's adoption is its high-quality mechanization in Rocq. This mechanization uses a number of Rocq features in sophisticated ways, including a carefully constructed algebraic hierarchy for modeling separation logic resources, and a proof mode for embedded separation logic proofs, which combines custom Ltac with extensible typeclasses. The library has been developed for over a decade with dozens of contributors, with an emphasis on modularity and maintainability. We explore how Lean features like flexible metaprogramming and quotient types can simplify the design and usage of Iris. Using these features, we provide a novel implementation of the Iris proof mode with improved performance, simplify the handling of equivalences through quotient types, build a variant of Diaframe proof automation, and provide convenience features like automatic construction of Iris fixed points. Building on Lean lets us integrate with the extensive Mathlib library, allowing us to re-use results from this library for program verification tasks that have heavy mathematical dependencies, as we demonstrate with an application to probabilistic program verification.