Nola: Nested Invariants and Borrows without Step-Indexing

Nola is a library for achieving expressive later-free nested invariants and borrows by the power of deep embedding. 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
  • funext (Function extensionality)
  • func (Functions), pred (Predicates), rel (Relations), list (Lists), nat (Natural numbers)
  • prod (Modified product), schoice (Variant over a list), plist (Product list)
  • hgt (General height of a tree), ctx (Context with unguarded/guarded variables)
  • proph (Prophecy)
• iris/ : Iris libraries
  • ofe (OFEs)
  • list (On list), gmap (On gmap), plist (On plist)
  • deriv (Derivability)
  • upd (Update), wp (Weakest precondition)
  • later (Later)
  • sinv (Simple invariant), inv (Invariant), na_inv (Non-atomic invariant)
  • lft (Lifetime), borrow (Borrowing)
  • proph (Prophecy), proph_ag (Prophetic agreement), pborrow (Prophetic borrowing)
  • paradox (Paradoxes)
• examples/ : Examples
  • heap_lang/ : Variant of Iris HeapLang, with Ndnat (terminating infinite non-determinism) added
  • minilogic : Minimal showcase logic
  • later : Instantiating Nola with later
  • logic/ : Showcase Logic
    • synty (Syntactic type),
    • prop (Proposition), subst (Substitution), iris (Iris preliminaries), intp (Interpretation), deriv (Derivability)
    • facts (Facts), adequacy (Adequacy)
    • sinv (Simple invariant), inv (Invariant), na_inv (Non-atomic invariant), borrow (Borrowing)
    • verify/ (Verification examples)
      • vlist (Shared mutable list with values)
      • ilist_base, ilist, na_ilist (Shared mutable infinite list)
      • borrow (Borrowing)
  • type/ : Stratified type system
    • type (Type), subst (Substitution), iris (Iris preliminaries), intp (Interpretation), deriv (Derivability)
    • facts (Facts), adequacy (Adequacy)
    • rules/ (Typing rules)
      • conv (Type conversion), expr (Expression typing), ref (Expression typing for references)
    • verify/ (Verification examples)
      • ilist (Shared mutable infinite stream)

Story

Nested Invariants

By nested invariants, we mean various forms of invariants or protocols expressed by separation-logic propositions that may contain invariants themselves. They can flexibly model or reason about shared mutable state. Impredicative invariants have been essential in the modern usage of separation logic, especially Iris.

The standard invariant in Iris is inv N P : iProp, which uses the namespace N for access. Iris also uses cancellable invariants and non-atomic invariants.

Also, RustBelt built an Iris library called the lifetime logic to semantically model borrows of the Rust programming language as rich invariants. For example, Rust's mutable borrow &'a mut T is modeled by an invariant called a full borrow &{α} P : iProp. It borrows during the lifetime α mutable state expressed by an Iris proposition P : iProp. This is an advanced form of cancellable invariant.

Obstacle: Laters

Step-Indexing

All the existing separation logics with nested invariants, such as Iris, resort to step-indexing. It is the technique of layering the logic world with step-indices 0, 1, 2, …: ℕ, having notions more defined as the step-index grows. Why?

Their separation-logic proposition iProp is a predicate over an abstract resource Res. To model invariants, they want Res to model agreement on iProp. So naively, they have a domain equation like the following, which is a circular definition:

iProp  ≜  Res → Prop     Res  ≜  F iProp

So they used step-indexing to make this solvable, like:

iProp  ≜  Res → sProp     Res  ≜  F (▶ iProp)

Here, sProp is a step-indexed proposition ℕ →anti Prop and ▶ delays the definition of a data type by one step-index.

Laters in the Way

Sounds fine? But this comes with the cost of the later modality ▷.

Due to ▶ added to iProp, we can use invariants only for propositions under ▷, which delays the definition of a proposition by one step-index.

inv N P ={↑N,∅}=> ▷ P ∗ (▷ P ={∅,↑N}=∗ True)

This causes significant practical issues, especially for dealing with nested invariants.

The later modality ▷ is ill-behaved: it is non-idempotent and doesn't commute with the update modality |==>. Various efforts have been made to get over ▷, such as later credits, but difficulties remain.

More fundamentally, the power to strip off ▷ makes program predicates weaker, ensuring only safety properties (such as partial correctness) but not liveness properties (especially, termination and total correctness) of programs. Indeed, recent studies Simuliris and Fair Operational Semantics, for example, just gave up nested invariants in Iris for reasoning about rich liveness properties regarding fair scheduling.

Solution: Nola

Nola proposes a new construction of nested invariants, which is free from the later modality ▷!

We can enjoy various forms of nested invariants, free from cumbersome later handling and achieving advanced liveness verification.

Core Idea: Deep Embedding

To achieve nested invariants, Nola uses deeply embedded separation-logic proposition, that is, the data type for the syntax A equipped with the semantic interpretation ⟦ ⟧ : A → iProp. Now we have broken the circular definition because the resource Res for a semantic proposition iProp depends just on the syntax A, like:

iProp  ≜  Res → Prop     Res  ≜  F A     ⟦ ⟧ : A → iProp

Easy!