Nola: Later-Free Ghost State for Verifying Termination in Iris

Nola is a framework for later-free higher-order ghost state, enabling termination verification in the presence of advanced features such as Rust's ownership types.

It is fully mechanized in Rocq (formerly known as Coq) as a library of the Iris separation logic framework.

The name Nola comes from 'No later' and the nickname for New Orleans, Louisiana, USA, in memory of POPL 2020 held in that city.

• Publications
• Getting Started
• Connection with the PLDI 2025 Paper
• Guide to the Rocq Code
• Overview of the Rocq Code

Publications

• Yusuke Matsushita and Takeshi Tsukada. Nola: Later-Free Ghost State for Verifying Termination in Iris.
  ACM PLDI 2025. June 13, 2025. Paper.
  • Yusuke Matsushita and Takeshi Tsukada. Artifact for "Nola: Later-Free Ghost State for Verifying Termination in Iris". Zenodo. 2025. Zenodo record.
• Yusuke Matsushita. Non-Step-Indexed Separation Logic with Invariants and Rust-Style Borrows.
  Ph.D. Dissertation, University of Tokyo. Dec 6, 2023. Paper, Talk slides.
  • Yusuke Matsushita. Non-Step-Indexed Separation Logic with Invariants and Rust-Style Borrows.
    Bulletin of Ph.D. Dissertations in AY 2023 Recommended by SIGs, Information Processing Society of Japan. Aug 15, 2024. HTML (Japanese).

Getting Started

Now we explain how to get started.

• Setting Up Opam
• Building Nola

Setting Up Opam

We use opam ver 2.* for package management. To install opam, you can refer to the official installation guide.

To create a new opam switch named for_nola (you can choose any name), run:

opam switch create for_nola 4.14.2 # Choose any OCaml version you like

To activate the opam switch for_nola just globally, run:

opam switch set for_nola

Or, to activate the opam switch for_nola locally in the directory NOLA_DIR (typically named nola) where this README.md is located, run:

opam switch link for_nola NOLA_DIR

To enable installing a development version of Iris for the active opam switch, run:

opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

Building Nola

First, go to the directory NOLA_DIR (typically named nola) where this README.md is located:

cd NOLA_DIR

To fix the development dependencies and install them, run:

make devdep

To build Nola's Rocq code locally, run:

make -j16 # Choose a job number

Or, to install Nola as an opam library, run:

opam install .

To generate and browse a document for Nola's Rocq code, run:

make viewdoc

Connection with the PLDI 2025 Paper

To check statements of the PLDI 2025 paper, you can refer to the following parts of our Rocq mechanization.

• Paradoxes
• Later-Free Ghost State
• View Shifts and Hoare Triples
• Extensible Construction of Formula Syntax
• Magic Derivability
• Examples and RustHalt

Paradoxes

• Paradoxes: nola.bi.paradox.
  • Paradoxes of the naive later-free invariant.
    • For the program logic based on Landin's knot: inv_landin.
    • Purely logically for view shifts: inv_vs.
  • Paradox of the step-indexed total Hoare triple: twp.
  • Paradoxes of unbounded later weakening.
    • Under finite step-indexing: exist_laterN.
    • Under transfinite step-indexing: exist_laterOrd.

Later-Free Ghost State

All the proof rules are proved to be sound with respect to the semantic model.

• Nola's later-free invariant: nola.iris.inv.
  • INV-PERSIST: inv_tok_persistent, INV-ALLOC: inv_tok_alloc, INV-ACC: inv_tok_acc_vs, THOARE-INV: inv_tok_acc_twp, WINV-CREATE: inv_wsat_alloc.
• Nola's later-free borrow.
  • Lifetime: nola.iris.lft,
    • LFT-ALLOC: lft_alloc, LFT-END: lft_end.
  • Borrow: nola.iris.borrow.
    • BOR-LEND-NEW: bor_lend_tok_new, LEND-BACK: lend_tok_retrieve, BOR-OPEN: bor_tok_open, OBOR-CLOSE: obor_tok_close, WBOR-CREATE: borrow_wsat_alloc.
  • Prophetic borrow: nola.iris.pborrow.

View Shifts and Hoare Triples

• Parameterized view shifts: nola.iris.modw.
  • VS-EXPAND: vsw-expand.
• Parameterized Hoare triples: nola.iris.wpw.
  • VS-THOARE: vsw-thoarew, THOARE-VS: thoarew-vsw, THOARE-EXPAND: thoarew-expand.
• Extended HeapLang: nola.heap_lang.
  • Adequacy of the total Hoare triple: total_adequacy.heap_total.
• Extended λRust, RustBelt's core language: nola.lrust.
  • Adequacy of the total Hoare triple: adequacy.lrust_total.

Extensible Construction of Formula Syntax

• Extensible construction of formula syntax: nola.iris.cif.

Magic Derivability

• Magic derivability: nola.bi.deriv.
  • DER-SOUND: der_sound, DER-DERIV: der_Deriv, DERIV-MAP: Deriv_mapl.

Examples and RustHalt

• Demonstration of how our program logic can emulate CFML: nola.examples.cfml.
• Basic examples: nola.examples.basic.
  • Loop decrementing the value of a location: twp_decr_loop, With non-deterministic initialization: twp_decr_loop_nd.
• Examples of shared mutable infinite lists: nola.examples.ilist.
  • Verifying tail access: twp_tail_list.
  • Verifying iterc: twp_iter_ilist, Verifying two threads running iterc: twp_fork2_iter_ilist, Verifying iterc for the multiple-of-three invariant: twp_iter_ilist_add3_mul3.
  • Verifying iterc2, with two counters under the lexicographic order: twp_iter2_ilist.
  • Verifying iteration using any step function under any well-founded relation: twp_iterst_ilist, with an instantiation example twp_iterst_ilist_step2.
• Basic examples for borrows: nola.examples.borrow.
  • Dereference of nested mutable borrows: bor_bor_deref.
  • Load from an immutable shared borrow over an integer: imbor_load.
• Mutex examples for borrows: nola.examples.mutex.
  • Acquiring a lock via a shared borrow of a mutex: mutex_bor_try_acquire, Create a shared borrow of a mutex: mutex_bor_lend_new.
• Examples for magic derivability: nola.examples.deriv.
  • Examples of semantic alteration: inv'_sep_comm, inv'_inv'_sep_comm and inv'_bor_lft.
  • Access via a view shift invd_acc_vs, Access via a total Hoare triple invd_acc_thoare, Allocation inv'_alloc, General rule for semantic alteration: inv'_iff'.
• A prototype of RustHalt: nola.examples.rust_halt.
  • INT-ADD: num.type_add_int, BOX-MUT-BORROW: ptrs_more.sub_borrow_box, MUT-REF-WRITE: mutref.write_mutref, MUT-REF-SHARE: ptrs_more.type_share, FN-REC-CALL: core.type_call, REAL: core.type_real.
  • Borrow subdivision: prod_more.sub_mutref_prod_split, sum_more.type_case_sum_mutref etc., Reborrowing: ptrs_more.sub_reborrow, ptrs_more.type_deref_mutref_mutref etc.
  • Verification examples: verify.
    • Verifying mutation of a list: list_more.type_iter_list_mut_fun.
    • Verifying mutation of a rich list over a mutable reference: mutlist_more.type_iter_mutlist_mut_fun.
  • Adequacy: adequacy.

Guide to the Rocq Code

When tackling the Rocq code of Nola, you can refer to the guide here.

• Notations
• Typical contexts

Notations

Nola introduces the following notations, guarded under modules:

• Modalities with a custom world satisfaction W: Add [W] in the middle, as defined in nola.bi.modw.
  • E.g., |=[W]=> P, P =[W]=∗ Q, |=[W]{E}=> P, P -∗[W] Q.
• Weakest preconditions and Hoare triples with a custom world satisfaction W: Add [W] before the expression, as defined in nola.bi.wpw.
  • E.g., WP[W] e [{ Ψ }], [[{ P }]][W] e [[{ v, RET v; Ψ v }]].
• Modalities with the except-0 modality ◇ : Add ◇, as defined in nola.bi.mod and nola.bi.modw.
  • E.g., |==>◇ P, P ==∗◇ Q, P -∗[W]◇ Q.
• Iterative separating conjunction over plist (nola.util.plist): Use [∗ plist], as defined in nola.bi.plist.
  • E.g., [∗ plist] x ∈ xl, Φ x.
• Custom product type prod (nola.util.prod): Add ', as defined in nola.util.prod.
  • E.g., (a, b, c)', p.1'.
• General semantics under magic derivability: Use ⟦ ⟧, as defined in nola.bi.deriv.
  • E.g., ⟦ Px ⟧, ⟦ Px ⟧(δ).
• Semantics for cif (nola.iris.cif): Use ⟦ ⟧ᶜ, as defined in nola.iris.cif.
  • E.g., ⟦ Px ⟧ᶜ, ⟦ Px ⟧ᶜ(δ).
• Equivalence for productivity: Use ≡[ ]≡, as defined in nola.util.productive.
  • E.g., a ≡[k]≡ b, a ≡[<k]≡ b.

Typical contexts

For extensibility, proofs using Nola are typically parameterized with various contexts, such as the following (xxx is a placeholder for a name):

• CON : cifcon: The family of constructors for cif (nola.iris.cif).
• JUDG : ofe: The judgment data type for magic derivability (nola.bi.deriv).
• Csem CON JUDG Σ: Semantics for the family of constructors CON for cif.
• Jsem JUDG (iProp Σ): Semantics for the judgment JUDG.
• xxxC ... CON: Requires some constructors to be included in CON.
• xxxJ ... JUDG: Requires some judgments to be included in JUDG.
• xxxCS ... CON JUDG Σ: Designates the semantics of the required constructors of CON.
• xxxJS ... JUDG Σ: Designates the semantics of the required judgments of JUDG.
• Deriv ih δ: δ is a valid derivability candidate under the induction hypothesis ih for magic derivability (nola.bi.deriv).

Overview of the Rocq Code

The Rocq code is all in nola/ and is structured as follows:

• prelude : Prelude
• util/ : General-purpose utilities, extending std++
  • eq (Equality), uip (UIP)
  • fn (Functions), gmap (On gmap), gmultiset (On gmultiset)
  • prod (Modified product), bin (Binary tree), plist (Product list), tagged (Tagged type)
  • proph (Prophecy)
  • order (Order theory), psg (Pseudo-gfp)
  • wf (Well-foundedness)
  • productive (Productivity)
  • nary (N-ary maps), cit (Coinductive-inductive tree)
• bi/ : Libraries for bunched implication logic
  • util (Utilities)
  • internal (Internal equality)
  • gmap (On gmap), plist (On plist)
  • order (Order theory), deriv (Magic derivability)
  • mod (Modality classes), modw (Modalities with custom world satisfactions), wpw (Weakest precondition with a custom world satisfaction)
  • judg (Judgments)
  • paradox (Paradoxes)
• iris/ : Libraries for Iris base logic
  • iprop (Utility for iProp), own (Utility for own)
  • list (On lists), option (On option), agree (On agree), csum (On csum)
  • sinv (Simple invariants)
  • inv (Invariants), inv_deriv (Invariants relaxed with derivability), na_inv (Non-atomic invariants), na_inv_deriv (Non-atomic invariants relaxed with derivability)
  • dinv (Direct invariants), dinv_deriv (Direct invariants relaxed with derivability), store (Stored propositions), store_deriv (Stored propositions relaxed with derivability)
  • lft (Lifetime), borrow (Borrows), borrow_deriv (Borrows relaxed with derivability), fborrow (Fractured borrows)
  • proph (Prophecy), proph_ag (Prophetic agreement), pborrow (Prophetic borrows), pborrow_deriv (Prophetic borrows relaxed with derivability)
  • cif (Extensible construction of coinductive-inductive formulas)
  • paradox (Paradox)
• heap_lang/ : Variant of Iris HeapLang, supporting program logic with custom world satisfactions for Nola
  • locations (On locations)
  • lang (Language), pretty (Pretty printing for the language), notation (Notation for the language), tactics (Tactics for the language)
  • metatheory (Metatheory on the language), proph_erasure (Prophecy erasure theorem for the language)
  • class_instances (Class instances for the program logic), definitions (Definitions for the program logic), primitive_laws (Primitive laws of the program logic), derived_laws (Derived laws of the program logic), proofmode (Proof mode utility for the program logic)
  • adequacy (Safety adequacy of the program logic), total_adequacy (Termination adequacy of the program logic)
• lrust/ : Variant of λRust, RustBelt's core language, supporting program logic with custom world satisfactions for Nola
  • lang (Language), notation (Notation for the language), tactics (Tactics for the language)
  • races (Race freedom guarantee of the language)
  • heap (Ghost state for the heap), lifting (Program logic), proofmode (Proof mode utility for the program logic)
  • adequacy (Adequacy of the program logic)
• examples/ : Examples
  • xty (Syntactic type), con (Constructors)
  • cfml (Demonstration of how our program logic can emulate CFML), basic (Basic examples), ilist (Infinite list), borrow (Borrow), mutex (Mutex), deriv (Derivability)
  • rust_halt/ : A prototype of RustHalt, a semantic foundation for total correctness verification of Rust programs
    • base (Basics), type (Type model)
    • core (Core features)
    • num (Numeric types), uninit (Uninitialized data type)
    • prod (Product type), sum (Sum type)
    • rec (Recursive type), mod (Modification type)
    • ptr (Utility for pointer types), box (Box pointer type), shrref (Shared reference type), mutref (Mutable reference type)
    • ptrs_more (More on basic pointer types), prod_more (More on the product type), sum_more (More on the sum type)
    • adequacy (Adequacy)
    • verify/ : Verification examples
      • util (Utility)
      • ack (Ackermann function)
      • list (Singly linked list type), list_more (More on the list type)
      • mutlist (Singly linked list over a mutable reference), mutlist_more (More on the mutlist type)