Summary (Overview)

  • Iris-Lean is a comprehensive reimplementation of the Iris framework for concurrent separation logic, originally developed in Rocq (Coq), now rebuilt in the Lean proof assistant.
  • The project covers all non-experimental features of Iris, including the base logic, the Iris Proof Mode (IPM), the algebraic hierarchy, and the HeapLang program logic.
  • Key innovations include: a novel IPM implementation leveraging Lean's metaprogramming, use of quotient types to simplify OFE equivalence handling, integration with Mathlib for heavy mathematical reasoning, and a Diaframe-like automation tactic called Wander.
  • The authors demonstrate the framework's utility through a Continuous Probabilistic Program Logic (CTE) for reasoning about programs manipulating random real numbers.
  • Performance benchmarks suggest significant speedups in proof automation compared to Iris-Rocq, and the project is open-source on GitHub and Zenodo.

Introduction and Theoretical Foundation

Iris is a well-established framework for higher-order concurrent separation logic, used to verify safety, security, and probabilistic properties of programs. Its mechanization in Rocq has been crucial for adoption, providing both a sound foundation and the Iris Proof Mode (IPM)—a tactic language for interactive reasoning inside the embedded logic.

The motivation for reimplementing Iris in Lean is threefold:

  1. Metaprogramming: Lean's flexible metaprogramming enables a more powerful and ergonomic IPM.
  2. Automation: Lean's simp and typeclass synthesis infrastructure can replace custom-built automation in Rocq.
  3. Mathlib integration: Access to Lean's extensive mathematical library supports program logics with heavy mathematical dependencies (e.g., measure theory for probabilistic verification).

The theoretical foundation rests on:

  • Step-indexed semantics for reasoning about recursive and coinductive features.
  • Bunched implications (BI) as the logical core.
  • OFEs (Ordered Families of Equivalences) for modeling resources.
  • Ghost resources and monotone predicates for separation logic resources.

Methodology

Algebraic Hierarchy and Bundling

Iris-Lean reimplements the algebraic hierarchy using a mixed bundling strategy:

  • Unbundled typeclasses for type-level operations (e.g., Dist, Equiv).
  • Bundled structures for properties like OFE and BI to enable typeclass inference.

Lean's lack of cumulative universes required a novel approach: Iris-Lean uses universe-polymorphic structures with explicit universe parameters, avoiding the limitations of Rocq's design. This also enabled a merge request to Iris-Rocq adopting the same approach.

Quotient Types for Equivalences

Iris-Rocq uses setoids for OFE equivalences (≡). Iris-Lean instead:

  • Requires ≡ to coincide with = (Leibniz equality) for most structures.
  • Uses quotient types when equivalence does not hold definitionally.
  • This simplifies rewriting and reduces boilerplate, leveraging Lean's built-in quotient support.

Proof Mode (IPM) in Lean

The IPM is reimplemented using:

  • A single inductive tree type Hyps for the spatial and persistent context.
  • Typed expressions (Lean.Expr) for metaprogrammatic manipulation.
  • A custom typeclass synthesizer built on Lean's own, reusing infrastructure for TC and Hint Mode-like annotations.
  • Direct parser integration for tactic syntax (no string literals), improving usability and type information.

Automation: Wander

Wander is a tactic mimicking Diaframe's automation for Iris proofs. It:

  • Reuses Lean's simp for simplification.
  • Implements proof search for separation logic goals.
  • Supports automatic introduction, framing, and solving of goals.

Fixed Point Elaborators

Iris-Lean provides custom elaborators for defining Iris fixed points (least/greatest fixed points of monotone functions, and contractive fixed points) in a style similar to Lean's def and inductive, reducing boilerplate.

Empirical Validation / Results

  • HeapLang port: Over 80% of the HeapLang separation logic and examples are ported, including a concurrent counter and quicksort specification.
  • Performance: Benchmarks show Iris-Lean's IPM and automation outperform Iris-Rocq in several cases, with significant speedups in proof search.
  • Probabilistic Program Logic: The CTE logic was successfully implemented, requiring:
    • Equipping program expressions with a MeasurableSpace.
    • Generalizing countable sums to Lebesgue integrals.
    • Proving adequacy and soundness results.

The authors also used temporary linters and attributes to track generalization of definitions during the CTE development, preserving build integrity.

Theoretical and Practical Implications

  • Design insights: The paper shows how Lean's features (quotients, metaprogramming, typeclass synthesis) can simplify and improve upon Rocq-based designs.
  • Interoperability: The rocq_alias tool helps maintain correspondence with Iris-Rocq, easing future synchronization.
  • Broader impact: Iris-Lean could become canonical infrastructure for program verification in Lean, with potential integration with CSLib and Std.Do.
  • Mathematical integration: The ability to use Mathlib enables program logics with heavy mathematical content (e.g., measure theory), opening new application areas.

Conclusion

Iris-Lean is a complete reimplementation of Iris in Lean, demonstrating that Lean's modern features can enhance both the ergonomics and performance of separation logic frameworks. The project achieves full coverage of Iris's non-experimental features, introduces novel automation and metaprogramming techniques, and validates its approach through a probabilistic program logic.

Future directions:

  • Continued synchronization with Iris-Rocq.
  • Integration with Lean's evolving standard library and CSLib.
  • Exploration of further automation and user-facing tooling.

The authors envision Iris-Lean as a foundation for future program verification research in Lean, with the full codebase available at GitHub and Zenodo.

Related papers