Nola: Modular Liveness Verification by Later-Free Ghost State

Nola is a framework that enables modular liveness verification by higher-order ghost state with the later modality cleared. It is fully mechanized in Coq with the Iris separation logic framework.

The name Nola comes from 'No later' and the nickname for New Orleans, Louisiana, US.

• Publication
• Getting Started
• Architecture

Publication

• Non-Step-Indexed Separation Logic with Invariants and Rust-Style Borrows. Yusuke Matsushita. Ph.D. Thesis, University of Tokyo. Dec 2023. Paper Talk slides

Getting Started

We use opam ver 2.* for package management.

To set up an opam switch named nola and link it to the folder:

opam switch create nola 5.0.0 # Choose an OCaml version
opam switch link nola .

To set up opam repos for Coq and Iris for the current opam switch:

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

To fix development dependencies and compile Coq code:

make devdep
make -j16 # Choose a job number

Or to install as a library locally:

opam install .

To generate and browse a document:

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 (iprop)
  • own (On 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
• rust_lang/ : Variant of RustBelt's language, supporting Ndnat and program logic with termination sensitivity and custom world satisfactions
• 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)