How Iris works

Iris is a framework for proving programs correct, built as a library for the Rocq prover. Its logic is a higher-order concurrent separation logic: an assertion describes the resources a piece of code owns (a heap cell, a share of one, a role in a protocol), it may quantify over other assertions, and threads share assertions through invariants. A language joins Iris by giving its step relation, and one theorem, adequacy, turns a proof in the logic into a plain Rocq fact about every run. Iris comes from Derek Dreyer's group at MPI-SWS and Lars Birkedal's at Aarhus, with Ralf Jung and Robbert Krebbers as its main builders, and has been developed in the open since 2015 (iris-project.org).

This page tells where Iris comes from, what its logic can say, how it differs from other ways of verifying C, and how it is built in Rocq. Then it shows how nanofil uses it: the machinemachine nanofilThe machine of a runtime R, Machine R, is what one thread's program sees run under R: Semantics.v's steps, plus R's allocations and R's actions at safepoints. mstep is its step relation and mreachable its runs. as an Iris language, resources keyed by object identityidentity nanofilAn object's identity is its base, the number its capabilities name; it outlives the object's bounds, so a freed object keeps its identity. One memory persists from another when every object of the first is in the second as it was, or freed: no identity is lost, moved or given to a new object., and a spike that proves a linked-list program never panics (logic.md records the decision). Each idea links to its page in the concept index. The shaded notes go deeper, or say where nanofil meets the idea. Rocq is quoted as written, from Iris 4.5 and from nanofil's spikes in rocq/spikes.

Hoare logic

In 1967 Robert Floyd attached assertions to the edges of flowcharts, and in 1969 Tony Hoare made that a logic of program text (An Axiomatic Basis for Computer Programming). Its judgment is the Hoare tripleHoare triple IrisA Hoare triple {P} c {Q} says that if P holds when c starts and c finishes, Q holds when it does. Hoare logic gives one rule per construct: assignment substitutes into the postcondition, sequencing chains triples, a loop needs an invariant each iteration keeps. It is partial correctness: a run that never finishes satisfies every triple. {P} c {Q}: if P holds when c starts and c finishes, Q holds when it does. Each construct has a rule. Assignment substitutes into the postcondition, sequencing chains two triples, and a loop needs an invariant that each iteration keeps. The triple says nothing about a run that never finishes, and neither do Iris's: it is partial correctness.

Hoare logic handles variables and breaks on pointers. Its assignment rule substitutes for the variable assigned, but *p ← 1 may change *q when p and q alias, so every assertion about any cell must say whether it might be the one written. Proofs of pointer programs drowned in such side conditions, as Rod Burstall had already noticed in 1972.

Separation logic

Between 1999 and 2002 John Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang fixed this by making an assertion describe only the part of the heap a command owns (Reynolds, LICS 2002). The assertion language came from O'Hearn and Pym's logic of bunched implications. Three connectives carry the idea of separation logicseparation logic IrisSeparation logic is Hoare logic whose assertions describe the part of memory a piece of code owns. ℓ ↦ v owns one cell, P ∗ Q holds of memory that splits into a part where P holds and a disjoint part where Q holds, and the frame rule lets code proved on what it owns run inside any larger memory, which it leaves alone. Aliasing is ruled out by the assertions, not by side conditions.:

• ℓ ↦ v, points-to: cell ℓ holds v, and whoever holds the assertion owns the cell. It is not a fact about the whole heap; it is the permission to read and write one cell.

• P ∗ Q, separating conjunction: the heap splits into two disjoint parts, one where P holds and one where Q does. So ℓ ↦ v ∗ ℓ' ↦ w implies ℓ ≠ ℓ': the assertion itself rules out aliasing.

• P −∗ Q, the magic wandmagic wand IrisThe magic wand P -∗ Q holds of resources that, joined with any disjoint resources where P holds, give resources where Q holds. It is a structure with a hole that P fills: a function's precondition is a wand to its weakest precondition, and a structure that lends out a part owns part ∗ (part -∗ whole).: owning it and P yields Q. It is a structure with a hole that P fills, as when part of a structure is lent out.

The payoff is the frame rule. Code proved correct on the cells it uses stays correct in any larger heap, and leaves the rest alone. In Iris it is a lemma about weakest preconditions, proved once (weakestpre.v):

So a specification names only its footprint. Reading a cell needs that cell and nothing else. In the triple notation for heap_lang, Iris's example language, where ! #ℓ loads from location ℓ:

Recursive data becomes a recursive predicate. The list from p holding xs is null when xs is empty, and otherwise a node owning its cells, separately from the list after it. Since ∗ keeps each node's cells apart from the rest, the predicate excludes cycles and sharing without saying so.

Concurrent separation logic

O'Hearn's concurrent separation logicconcurrent separation logic IrisConcurrent separation logic carries ownership across threads: threads that own disjoint resources run in parallel without interfering, and a lock guards a resource invariant that the thread taking the lock receives and must restore before releasing it. The decade after it produced a logic per sharing pattern (RGSep, CAP, iCAP, TaDA and more), each with its own soundness proof; Iris reduced them to ghost state and invariants. (CONCUR 2004, with a soundness proof by Stephen Brookes; the two shared the 2016 Gödel Prize) carried ownership across threads. Threads that own disjoint parts of the heap run in parallel without interfering. A lock protects a resource invariant, an assertion that the thread taking the lock receives and must restore before releasing it, so ownership moves with the lock.

Fine-grained concurrent code, which synchronizes through atomic instructions instead of locks, did not fit, and the next decade produced a logic per pattern. Fractional permissions shared cells for reading (Boyland 2003; Bornat, Calcagno, O'Hearn and Parkinson 2005). RGSep mixed in rely-guarantee (Vafeiadis and Parkinson 2007). Concurrent abstract predicates hid shared state behind protocols (Dinsdale-Young et al. 2010), and HOCAP, iCAP, CaReSL, TaDA, FCSL and GPS followed. Each had its own model and its own soundness proof; Matthew Parkinson named the situation "The next 700 separation logics" (2010).

Iris

Iris was the answer to that zoo. Its first paper claimed that the zoo's mechanisms reduce to two: ghost state the user defines with a partial commutative monoid, and invariants. A new pattern is then a choice of monoid and an invariant, proved inside the logic, instead of a new logic. Later versions shrank the core further and filled its gaps:

• 1.0, 2015: ghost state from monoids, invariants and a step-indexed model, with the rest derived. Jung, Swasey, Sieczkowski, Svendsen, Turon, Birkedal and Dreyer, Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning, POPL.

• 2.0, 2016: camerascamera IrisA camera is the kind of resource Iris's propositions are about: a set with a composition ⋅ of two pieces, a validity ✓ saying which compositions are possible, and a step-indexed equality. Owning two pieces is owning their composition. A frame-preserving update a ~~> a' changes a piece to another that stays valid with anything another party could own. Choosing a camera is choosing what can be owned and how it may change., so that ghost state may hold propositions. Jung, Krebbers, Birkedal and Dreyer, Higher-Order Ghost State, ICFP.

• 3.0, 2017: a small base logic, with invariants, fancy updatesupdate modality IrisAn update modality says a proposition holds after a change the proof makes on its own, with no program step. The basic update |==> P changes ghost state by frame-preserving updates and allocates new ghost locations. The fancy update |={E1,E2}=> P may also open and close invariants, from the mask E1 of closed invariants to E2; P ={E}=∗ Q is P -∗ |={E}=> Q. and weakest preconditions defined in it. Krebbers, Jung, Bizjak, Jourdan, Dreyer and Birkedal, The Essence of Higher-Order Concurrent Separation Logic, ESOP.

• 3.1, 2018: the whole construction in one account, the reference to read. Jung, Krebbers, Jourdan, Bizjak, Birkedal and Dreyer, Iris from the Ground Up, JFP.

• 4.0, 2022: later credits, an ownable right to remove a laterlater modality IrisIris's propositions hold or fail at each step index, a budget of program steps still to run, and ▷ P ("later P") holds at n + 1 when P holds at n. Stored propositions, in invariants or ghost state, come back only under a ▷, and each program step lets a proof remove one. Löb induction, (▷ P → P) ⊢ P, proves P while assuming it one step later; loops, recursion and the weakest precondition itself are proved or defined that way.. Spies, Gäher, Tassarotti, Jung, Krebbers, Birkedal and Dreyer, Later Credits, ICFP.

Releases continued, 4.5 in March 2026 for Rocq 9.0 to 9.2, the one nanofil's pinned nixpkgs ships (changelog). Beside the logic came the Iris Proof ModeIris Proof Mode IrisThe Iris Proof Mode is a set of Rocq tactics that give separation-logic goals their own context: hypotheses named by strings, a persistent zone that can be used again and a spatial zone whose hypotheses tactics consume. iIntros, iDestruct "H" as "[H1 H2]", iFrame, iSplitL, iMod, iNext and iLöb do the splitting, framing and modal reasoning that would otherwise be lemma chains; typeclasses make them extensible. (Krebbers, Timany, Birkedal, POPL 2017; generalized as MoSeL, ICFP 2018), which made proofs in it practical. Uses followed: RustBelt proved that Rust standard libraries built on unsafe code are safe to use (Jung, Jourdan, Krebbers, Dreyer, POPL 2018), and RefinedC, Cerise, Perennial's crash-safe storage and Aneris's distributed systems are all Iris instances. VST, the older C logic, was itself rebuilt on Iris (POPL 2024).

What kind of logic it is

Propositions are resources

An Iris proposition has type iPropΣ and describes resources: it holds of some and not of others, and ∗ splits them. Most propositions cannot be duplicated: from ℓ ↦ v there is no way to get two. The logic is affine, so a resource may be thrown away but never copied. Some propositions are knowledge rather than ownership, and those are persistentpersistent proposition IrisA persistent proposition is knowledge rather than ownership: it owns nothing exclusive, so it can be copied, □ P giving □ P ∗ □ P, and kept after it is used. Pure facts ⌜φ⌝, invariants, a cell that never changes again (ℓ ↦□ v) and specifications of functions are persistent; ℓ ↦ v is not.: □P holds when P does without owning anything exclusive, and □P gives □P ∗ □P. A Rocq fact φ embeds as ⌜φ⌝, which is persistent.

Higher-order means a proposition may quantify over propositions and predicates, as in ∀ Φ : val → iProp Σ. That is how a specification abstracts over whatever its caller keeps, how a function that takes a callback states the callback's specification, and how a container is generic in what its elements own.

Ghost state

Ghost stateghost state IrisGhost state exists only in the proof. own γ a owns the piece a of the ghost location γ, where a belongs to a camera; it is allocated and changed by updates, never by the program. It records what the program's memory does not: shares, histories, a protocol's phase, or a whole map that the state interpretation ties to the real heap. exists only in the proof. It records what the program's memory does not: who holds which share of a cell, a counter's history, the phase of a protocol each thread is in. ownγ a says the proof owns the piece a of the ghost location γ, where a belongs to a resource algebra the user picks, a cameracamera IrisA camera is the kind of resource Iris's propositions are about: a set with a composition ⋅ of two pieces, a validity ✓ saying which compositions are possible, and a step-indexed equality. Owning two pieces is owning their composition. A frame-preserving update a ~~> a' changes a piece to another that stays valid with anything another party could own. Choosing a camera is choosing what can be owned and how it may change.: a set with a partial composition ⋅ and a validity ✓. Owning two pieces is owning their composition, everything owned together is valid, and allocating and changing ghost state are updates (own.v):

An update a ⇝ a' must preserve frames: for any piece c another party may own, if a ⋅ c was valid, a' ⋅ c is. So changing your own ghost state never invalidates anyone else's. Choosing a camera is choosing a protocol. Excl gives exclusive ownership, fractions in (0, 1] give shares, Agree gives agreement on a value that never changes, and the authoritative camera gives one party ● a, the whole, and others ◯ b, fragments that must be included in it. Iris's heap is the last: the state interpretation owns ● of a map that equals the real heap, and ℓ ↦ v is ◯ of the one-entry map (gen_heap, on ghost_map).

Invariants

An Iris invariantIris invariant IrisAn Iris invariant inv N P says that P holds, of resources no one owns, between every two steps of the program. It is persistent, so every thread may know it; a thread opens it for one atomic step, takes P out under a later, and puts P back before the step ends. Masks record which invariants are open, so none opens twice at once. Since Iris 3 it is defined in the logic from ghost state and fancy updates. invN P says that P holds, of resources no one owns, between every two steps. It is persistent, so every thread may know it. A thread opens it for one atomic step, takes P out, and puts P back before the step ends (invariants.v):

The mask E is the set of invariants that may be opened. Opening N removes it from the mask, so it cannot be opened twice at once, which would duplicate P. CSL's lock invariants, RGSep's shared regions and CAP's protocols are each an invariant over some ghost state. Since Iris 3, inv is not a primitive but a persistent proposition defined in the logic, the ability to open:

The later modality

Invariants, and ghost state that holds propositions, make the model circular: a proposition is a predicate over resources, and a resource may contain a proposition. Iris breaks the circle with step-indexing (later modalitylater modality IrisIris's propositions hold or fail at each step index, a budget of program steps still to run, and ▷ P ("later P") holds at n + 1 when P holds at n. Stored propositions, in invariants or ghost state, come back only under a ▷, and each program step lets a proof remove one. Löb induction, (▷ P → P) ⊢ P, proves P while assuming it one step later; loops, recursion and the weakest precondition itself are proved or defined that way.). Each proposition holds or fails at each step index n, a budget of steps still to run, and ▷P, "later P", holds at n + 1 when P holds at n. A proposition that was stored, in an invariant or in ghost state, comes back only under a ▷, which is why inv_acc gives ▷P. The program takes a step while an invariant is open, and each step lets the proof remove one ▷.

The same indices give recursion for nothing. Löb induction proves P while assuming P one step later (derived_laws_later.v):

A loop is proved by assuming the loop safe one step later and showing that its body takes a step before it uses the assumption. The weakest precondition is itself defined that way.

Update modalities

Changing ghost state is not a program step, so it has its own connective, an update modalityupdate modality IrisAn update modality says a proposition holds after a change the proof makes on its own, with no program step. The basic update |==> P changes ghost state by frame-preserving updates and allocates new ghost locations. The fancy update |={E1,E2}=> P may also open and close invariants, from the mask E1 of closed invariants to E2; P ={E}=∗ Q is P -∗ |={E}=> Q.. The basic update |⇛ P says P holds once ghost state is changed by frame-preserving updates; own_alloc and own_update above produce one. The fancy update E1|⇛E2 P may also open and close invariants: it starts with the invariants in E1 closed and ends with those in E2 closed, and inv_acc is one. P ⇛E Q abbreviates P −∗ |⇛E Q.

Weakest preconditions

The weakest preconditionweakest precondition IrisWP e {{ v, Φ v }} says that running e is safe and that, if it ends in a value v, Φ v holds. Iris defines it once for every language by guarded recursion: unless e is a value, given the state interpretation of any state, e can step (when stuckness is NotStuck), and after every step it can take, one later on, the new state's interpretation and the WP of what e became hold. Hoare triples and specifications are wands into it. WPe {v. Φv} says that running e is safe and that, if it ends in a value v, Φ v holds. Iris defines it once for every language, by guarded recursion, as the fixpoint of this function (weakestpre.v):

Read it as a game against the machine. If e1 is a value, update to Φ v. Otherwise the machine names a state σ1 and hands over its state interpretationstate interpretation IrisThe state interpretation is the proposition a language instance ties to the machine's real state. The WP receives it before every step and must give it back for the new state, so it is an invariant of every run; a proof never sees the state itself, only what owning fragments and the interpretation together imply. For heap_lang it is the authoritative ghost heap, which equals the real heap. (for heap_lang, the authoritative heap). The proof must show that e1 can step, when the stuckness s is NotStuck, and, for every step e1 can take, after a later, return the new state's interpretation, the weakest precondition of what e1 became, and one for each thread it forked. The proof never sees the state itself. It owns fragments such as ℓ ↦ v and learns facts about σ1 by combining them with state_interp.

A Hoare triple ⦃P⦄ e ⦃RET v; Q⦄ is notation for □∀Φ, P −∗ ▷Q −∗ Φv −∗ WPe {Φ}. For any continuation Φ, owning P and the promise that Q gives Φ, e is safe and ends in Φ. Specifications in this continuation style compose: the caller's Φ carries everything the caller keeps.

Adequacy

A proof in the logic is worth something only if it says something about runs. Adequacyadequacy nanofilAdequacy is the one theorem that ties a program logic to the machine: if a program's proof in the logic can be derived, then no state any of its runs reaches fails. It is proved once; after it, proving a program never panics is deriving its proof, with no reasoning about runs. says it, once per language, in Rocq's own logic (adequacy.v):

wp_adequacy proves adequate from a proof, after allocating any invariants and ghost state, of the initial state's interpretation and a WP for e1. Every thread of every reachable configuration is then a value or can step, and a main thread that ends satisfies the postcondition. The proof unfolds the WP along the run, one step and one ▷ at a time, and ends with the base logic's soundness, which turns ⊢ ▷n⌜φ⌝ into φ.

What you can say with it

• Ownership and framing. A specification mentions only what the code touches; the frame rule carries the rest. A function that borrows a list and gives it back says so with the same lst p xs before and after.

• Sharing. A fraction splits ℓ ↦ v into read-only shares ℓ ↦q v, and a cell that never changes again becomes the persistent ℓ ↦□ v, which anyone may copy.

• Protocols. A camera states the possible states and transitions; an invariant ties them to real memory. A monotone counter, a one-shot flag, a lock and a reference count are a few lines each.

• Higher-order specifications. A function that takes a closure quantifies over the closure's specification, and a structure that lends out a part owns P ∗ P −∗ whole.

• Logical atomicity. An operation that takes many steps may be specified as if it took effect at one point, its linearization point (atomic updates, after TaDA). Prophecy variables (POPL 2020) let a proof use what the program will do later.

• Logical relations and refinement. iProp is a good language for semantic types: RustBelt interprets each Rust type as an Iris predicate, and ReLoC and Simuliris prove that one program refines another.

• Other kinds of program. Crash recovery (Perennial), distributed systems (Aneris), probabilistic programs (Clutch) and capability machines (Cerise) instantiate the same framework.

What it does not give for free: a plain WP is partial correctness, so termination needs the total weakest precondition or an argument outside the logic; liveness is hard; and Iris is a framework, not a push-button verifier. Automation comes from libraries on top, such as RefinedC's Lithium and Diaframe, and each new language costs an instantiation and its rules.

How it differs

Each approach makes a different choice of what is trusted and what is proved about which program.

• A hand-rolled logic: assertions as predicates on heaps, with a star and its frame lemmas written for one language, everything proved by hand in Rocq. Sep.v is one; its adequacy is never_panics_by_invariant, but its framing is manual.

• VST: Andrew Appel's Verifiable C, a higher-order impredicative separation logic for CompCert's Clight with its own step-indexed model, proved sound in Rocq against CompCert's semantics, so its proofs reach the assembly; rebuilt on Iris in 2024. It is a logic for C with C's memory model; nanofil proves programs in its own IR, whose memory is Fil-C's.

• CompCert: Xavier Leroy's verified C compiler, which proves in Rocq that the assembly simulates the source. It proves a translation, not programs; nanofil proves its validatorvalidator nanofilThe validator decides whether a module is well formed and, in checked IR, whether every access is covered by evidence that still holds. Every producer of checked IR must get its output past it, and Soundness.v proves that a module it accepts never runs to unchecked. sound instead (valid_no_unchecked) and checks its passes by translation validationtranslation validation nanofilTranslation validation checks each transformation's result rather than proving the transformation once: nanofil's register checker, the check passes' *_refines/2, and the interpreter refinement of difftest -O (amd64_regs_check:check_regs/5, opt:refines/2, refines). A wrong pass then makes a compile fail rather than produce a wrong output, as far as the checker is right..

• RefinedC: refinement types for C built on Iris, with Lithium searching for the typing proof. It is the ownership-types rung of logic.md's ladder: its typing derivations are Iris proofs, so they need no soundness proof of their own.

• Cerise: Iris on a CHERI-like capability machine that runs untrusted code. It is the nearest prior art: capabilities and their bounds as Iris resources.

• VeriFast, Viper, Verus: separation logic, or implicit dynamic frames, decided by symbolic execution and an SMT solver. Fast and practical, but the verifier is trusted, not proved.

How it is built in Rocq

Iris is a stack of libraries, each built only on the interface of the one below:

The model

A proposition is a predicate on a step index and a resource, closed under taking fewer steps and owning more (upred.v):

The connectives are definitions on it. ∗ splits the resource, up to equality at the current index, and ▷ looks one index down:

iPropΣ is uPrediResURΣ. Σ lists the camera functors a proof uses, and its resources map each to a finite map from ghost names γ to camera elements. A camera in Σ may mention iPropΣ itself, as an invariant's ghost state mentions P, so iProp is the solution of a recursive domain equation, which Iris constructs once, in the style of America and Rutten, over ordered families of equivalences (OFEs). Step-indexing is what makes the solution exist: each recursive occurrence sits under a ▷.

The laws are proved in the model once and packaged as the bi interface, for bunched implications. Everything above it, the proof mode included, uses only the interface, so the same proof mode serves other separation logics; that is MoSeL.

The proof mode

Proving P ∗ Q ⊢ Q ∗ P with Rocq's own tactics means rewriting with associativity and commutativity lemmas, and real goals have a dozen conjuncts. The Iris Proof ModeIris Proof Mode IrisThe Iris Proof Mode is a set of Rocq tactics that give separation-logic goals their own context: hypotheses named by strings, a persistent zone that can be used again and a spatial zone whose hypotheses tactics consume. iIntros, iDestruct "H" as "[H1 H2]", iFrame, iSplitL, iMod, iNext and iLöb do the splitting, framing and modal reasoning that would otherwise be lemma chains; typeclasses make them extensible. gives Iris goals their own context. Hypotheses have string names and live in two zones: persistent ones, which can be used any number of times, and spatial ones, which a tactic consumes. Above the double line is Rocq's own context; below it, persistent hypotheses (none here) would come first, then the spatial ones, then the goal under ∗. A goal of nanofil's spike, in the middle of the proof below, as Rocq prints it, without the section's variables and with shorter rules (the spike's page draws every state of the proof):

m : mem
s : R.state
ps : list (piece * pval)
h : gmap piece pval
Ha : agrees (m, s).1 h
Hd : live_disjoint (m, s).1
Hr : R.ready (m, s).2 (m, s).1
=============================
"Hh" : gen_heap_interp h
"Hps" : pts ps
-----------------------------∗
⌜owned_facts ps m⌝

iIntros Hσ Hps introduces wands, iDestruct Hσ as h [Hh %Hσ] opens an existential and a ∗ and moves a pure fact into Rocq's context, iFrame cancels hypotheses against the goal, iSplitL H gives H to the left conjunct, iMod runs an update, iNext removes a later, and iLöb as IH starts Löb induction. The tactics are driven by typeclasses (IntoSep, Frame, ElimModal), so a new connective joins them with instances. The whole proof of that goal, pts_facts:

A language

A language is a structure: expressions, values, states, observations, and a step relation that may fork threads (language.v):

The mixin asks three laws: a value round-trips through of_val and to_val, and a value takes no step. With that, WP and adequacy exist for the language. The user then picks a state interpretation (an irisGS_gen instance) and proves a rule per primitive operation from Iris's lifting lemmas, such as wp_lift_step; heap_lang's wp_load, wp_store and wp_alloc are proved that way. A language whose expressions have evaluation contexts (ectx_language) also gets wp_bind, which proves a subexpression first and the rest under its result.

nanofil's machine in Iris

nanofil's campaign is now a property of whole programs (formal.md): never_panics says that no run of a module, from any admissible input, with any fuelfuel nanofilThe interpreter's bound on executed blocks: each block entered costs one unit, and running out ends the run out_of_fuel, which proves nothing (interp:run/5). and anything the runtime does, reaches a state that fails. Campaign 3 already proves that a validated module never makes an uncheckedunchecked nanofilunchecked(Why) is the outcome of a raw access its capability does not allow, or of a reuse form whose trust was false: a check was missing or too weak, which only a broken pass produces. It is neither undefined behaviour nor a trap, so it refines nothing (interp:raw_res/2). access; never_panics asks that no check fails either. A check's success depends on facts about the heap (this field points to a live 16-byte object), which belong to whoever owns the object, so the logic is a separation logic. The two spikes prove the same theorem twice, once in a hand-rolled logic and once in Iris; logic.md compares them and recommends Iris. This section reads the Iris one.

The machine as a language

IrisLang.v wraps the machine. An expression is a configuration without its memory, or the outcomeoutcome nanofilAn outcome is how a run ends: a return, unreachable, undefined behaviour, a trap, unchecked, or running out of fuel. interp.pl and the model give the same outcomes term for term, which is what the outcome gate compares. a run ended with; the Iris state is the memory with the runtime's state:

A primitive step is a machine step from a configuration that does not fail, a refused allocation, or an ending that is not a failure:

This is the whole trick. A panic, a stuck step and a negative allocation are each a configuration with no primitive step, so in Iris's terms it is stuck (fails_not_reducible). Running out of fuel, a refusal and a normal return end the run in a value. A safepointpoll Fil-CA safepoint is a point where the thread may run signal handlers and answer the collector. The collector frees nothing the program can name there, but a handler the program installed may free an object under the rest of the program. A pollcheck is a safepoint on an edge: a jump target poll(L), a poll edge, runs one before going to L. Calls, allocations and some helpers are safepoints too (ir:evidence_preserving/1, ir:polls_every_cycle/1). is an mstep that leaves the expression as it was and changes only the state. Nothing forks, and observations are unused.

Adequacy is never_panics

A WP with stuckness NotStuck demands that every reachable expression be a value or reducible. In this language that is exactly that no reachable configuration fails. So Iris's adequacy, with a bridge from the machine's reachability to Iris's (adequate_no_fails), proves Panics.v's statement itself, wp_never_panics:

The postcondition is True: never_panics is a safety property, so what a run returns does not matter, only that every step it takes is safe. The fuel is universally quantified and OutOfFuel is a value, so the WP needs no termination argument. The theorem took 174 lines and an hour. The hard part of an adequacy proof is the logic's model, and Iris has proved that once for every language.

Resources keyed by identity

What can a proof own in Fil-C's memory? Pieces.v, shared by both spikes, answers: an object's life, one byte, or one auxaux Fil-CAn object's aux allocation, as large as its payload: where Fil-C keeps the lowers of the pointers stored in the object, slot for slot, while their intvals sit in the object's bytes. The aux word in the object header points at it; it is null for an object no pointer was ever stored into, which the collector then scans as a leaf. A pointer store must *ensure* it exists, which may call the runtime; a pointer load reads it. slot, each named by the object's identityidentity nanofilAn object's identity is its base, the number its capabilities name; it outlives the object's bounds, so a freed object keeps its identity. One memory persists from another when every object of the first is in the second as it was, or freed: no identity is lost, moved or given to a new object. and an offset:

Keying by identity is forced, not chosen. In the model a new object may cover addresses a freed object once had (fresh), so an address may belong to two objects in turn, but an identity never does (free_keeps_ids). An assertion about address a would be about whichever object is there; an assertion about identity b stays about one object for its whole life, and after it.

IrisHeap.v gives each piece a value, puts the pieces in Iris's gen_heap, and defines the state interpretation: the authoritative ghost heap agrees with the memory, live objects do not overlap, and the runtime is readyready nanofilA runtime is ready in a memory when its own state and that memory agree well enough that its next allocation is fresh. Readiness is the runtime's invariant: the axioms about allocation and the address space are stated only for ready states.. pts owns a list of pieces with their values:

A checkcheck Fil-CAn access check: check(Lo, Hi, Rights, Align) of a pointer P traps unless P's capability permits Rights on [P+Lo, P+Hi) with P+Lo Align-aligned, and otherwise yields P as a proof of class a. check_local does the same for a named local, and check_function yields a function proof of class f (ir:op_kind/2, pizlonate:checked_access/4). splits along these pieces. Its bounds test is arithmetic on the object's extent and the pointer's offset, and its free-flag test needs the object still live. logic.md's plan makes those two halves two resources. The meta factmeta nanofilA meta fact, meta b n k, says that the object of identity b was allocated with extent n bytes and kind k (heap, global data, stack). It is the persistent half of owning an object in the planned program logic: once true it stays true, so it can be copied and shared freely, because nothing after an allocation changes what was allocated. With the pointer's offset from b it decides a check's bounds by arithmetic alone; whether the object is still there is the live token's part. meta b n k (b was allocated with n bytes, of kind k) is persistent, because nothing after an allocation changes what was allocated; it would be a ghost_map element b ↪□ n, k, which anyone may copy. The live tokenlive nanofilA live token, live b, is permission to rely on the object of identity b not being freed. It is the temporal half of a check: the bounds come from b's meta fact, and the free flag passes as long as the token is held. Free consumes it, so whoever frees an object must own it, and an object no one else owns cannot be freed behind the owner's back. For a heap object it is exclusive, or split into fractions for readers; for global data, which is never freed, it is persistent. live b is exclusive, or split into fractions for readers, and free consumes it, so only the owner can free. Cells are points-to pieces, as above. The spike needed only live: its PLive piece carries the region, and the bounds come from there.

Safepoints, by Löb

A safepoint is where the runtime acts, and Runtime.v's axiom for it is the collector's alone, collector_live: no region changes at a safepoint, so no safepoint frees a live object. The spikes once took that as a premise, keeps_live, as Buffer.v did; with collector_live it is a lemma of Pieces.v for every runtime, and no rule or theorem takes it. A safepoint keeps every region and byte, and rewrites only aux slots that hold a dead object's capability (safepoint_shape, from collector_live, non_moving and aux_round_trip), so it keeps heap_interp with the same ghost heap.

Every rule of the spike comes from one lifting lemma, wpc_lift, and that lemma deals with safepoints once:

Given Q, the configuration is safe if Q and the state interpretation show it does not fail, and if after every step that is not a safepoint (nosp_step) they give back the state interpretation and safety of what follows. The safepoint case is missing from the premises because the proof closes it with iLöb: a safepoint steps from EConffr callers fuel to itself, so what is to be proved after it is the lemma's own conclusion, one step later, which Löb induction assumes. No program proof mentions safepoints again. The hand-rolled spike, without ▷, needs each function's assertions to survive a safepoint and a lemma per function to say so. Fuel cannot replace Löb here, because a safepoint spends no fuel.

A list, summed

The program is listsum.c, compiled by nanofil:

In checked IR, sum checks each node's value field, half-checks and loads the next pointer with its capability from the aux, and polls on the loop's back edge; listsum allocates each node on the collected heap and stores through checked pointers. A node owns its life as a 16-byte heap object, the aux slot of its next pointer, and the bytes of both fields; the list is a recursive predicate, with the pointer's own capability and alignment as pure facts (IrisListSum.v):

sum's specification, sum_spec, is in continuation style. The machine keeps the callers stack inside the expression, so there is no evaluation context to bind; instead the caller's resumption, with any result and any fuel, is a resource the callee carries to its return:

The frame is free: whatever the caller owns besides the list rides inside cont. Each loop is a Löb induction at the point after its head's phis, and each step is one rule application with the step computed, as in Symbolic.v. The theorem is then adequacy (heap_never_panics) applied to listsum's specification (listsum_spec):

Planting a bug shows what the specification carries: a node without its PLive piece makes lst_head unable to show the next node is live, only that it was allocated, and sum's checks of it cannot be proved to pass.

Against the hand-rolled logic

The hand-rolled spike states assertions as predicates on a footprint of pieces and the memory, with ∗ written out:

It needs no new adequacy, since an invariant of configurations built from its assertions goes straight into never_panics_by_invariant. Everything Iris's proof mode does, it does by lemma: emp ∗ P is P only up to "the same pieces", four-way stars are reassociated by explicit chains, and walked nodes are dropped by lst_cons_drop. The two spikes are the same size and prove the same theorem:

In both, most of the program proof's time goes to computing the machine's step on abstract states, which no logic removes. What separates them is where the next proofs spend effort, which is why logic.md recommends Iris: framing, safepoints and the wand that Hello's quotearg needs (stringret ∗ stringret −∗ slots) all come with it.

What comes next

From logic.md: step lemmas, one per instruction form of the core subsetcore subset nanofilThe core subset is the part of checked filc-mode IR that the Rocq model runs and validates: the integer, pointer and proof classes, floats, check and every reuse form, the raw accesses, flight, poll edges, direct calls, check_function with raw_call, free, named locals, touch, variadics and setjmp, which is validated as ir.pl does while its step is stuck, as the interpreter refuses it. A function that uses anything else decodes to IOutside., proved once as the WP's rules, so that no program proof computes a step; an ectx_language whose context is the callers stack, so that a function's specification returns its resources as an ordinary triple; meta as persistent ghost_map elements beside live and the cells; then Iris in the main build, hi.c and gc.ir's sum through the logic with libc's contracts as triples, and Hello. Campaign 5's certificates and RefinedC-style ownership types would then be fragments of the logic, sound because adequacy is.