Nola: Parameterization for Later-Free Invariants and Borrows

Nola is a library to achieve later-free invariants and borrows by the power of parameterization. It is fully mechanized in Coq with the Iris separation logic framework.

The name Nola comes from No laters and a nickname for New Orleans, Louisiana, US.

• Publication
• Getting Started
• Story
  • Nested invariants
  • Obstacle: Laters
  • Solution: Nola

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
  • fn (Functions), rel (Relations)
  • prod (Modified product), plist (Product list)
  • proph (Prophecy)
  • intp (Interpretation)
  • order (Order theory), psg (Pseudo-gfp)
  • citree (Coinductive-inductive tree)
• bi/ : Libraries for bunched implication logic
  • ofe (On OFE), list (On list), gmap (On gmap), plist (On plist)
  • order (Order theory), deriv (Derivability)
  • genupd (General update), updw (Update with a custom world satisfaction), wpw (Weakest precondition with a custom world satisfaction), util (Utilities)
  • paradox (Paradoxes)
• iris/ : Libraries for Iris base logic
  • ofe (On OFE), list (On list)
  • sinv (Simple invariant), sinv_deriv (Simple invariant relaxed with derivability)
  • inv (Invariant), inv_deriv (Invariant relaxed with derivability), na_inv (Non-atomic invariant), na_inv_deriv (Non-atomic invariant relaxed with derivability)
  • lft (Lifetime), borrow (Borrowing), borrow_deriv (Borrowing relaxed with derivability)
  • proph (Prophecy), proph_ag (Prophetic agreement), pborrow (Prophetic borrowing)
  • ciprop (Coinductive-inductive proposition)
• heap_lang/ : Variant of Iris HeapLang, supporting Ndnat (infinite non-determinism) and program logic with custom world satisfactions
  • lib/ : Libraries
    • mutex (Mutex machinery)
• examples/ : Examples
  • minilogic : Minimal showcase logic
  • later : Instantiating Nola with later
  • logic/ : Showcase logic