Nola: Later-Free Ghost State for Verifying Termination

Nola is a framework for later-free higher-order ghost state, enabling termination verification in the presence of advanced features.

It is fully mechanized in Coq as a library for 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
• Architecture

Publications

• 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 where this README.md is located, run:

opam switch link for_nola NOLA_DIR

To set up opam repos for Coq and Iris for the active opam switch, run:

opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

Building Nola

First, go to the directory NOLA_DIR where this README.md is located:

cd NOLA_DIR

To fix development dependencies and install them, run:

make devdep

To build Nola's 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 Coq code, run:

make viewdoc

Architecture

All the Coq code is in nola/ and structured as follows:

• prelude : Prelude
• util/ : General-purpose utilities, extending stdpp
  • eq (Equality)
  • uip (UIP)
  • fn (Functions)
  • gmap (On gmap), gmultiset (On gmultiset)
  • prod (Modified product), plist (Product list), tagged (Tagged type)
  • proph (Prophecy)
  • order (Order theory), psg (Pseudo-gfp)
  • 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 (Modality with a custom world satisfaction), 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 (Coinductive-inductive formula)
  • paradox (Paradox)
• heap_lang/ : Variant of Iris HeapLang, supporting Ndnat (infinite non-determinism) and 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)
• rust_lang/ : Variant of RustBelt's language, supporting Ndnat (infinite non-determinism) and program logic with termination sensitivity and 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), ilist (Infinite list), borrow (Borrow), mutex (Mutex), deriv (Derivability)
  • rust_halt/ : RustHalt, a formal foundation of functional and termination-sensitive Rust program verification
    • 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)
    • sum_more (More on the sum type)
    • adequacy (Adequacy)
    • verify/ (Verification examples)
      • list (Singly linked list type), list_more (More on the list type)