Separation 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.

• In Iris the frame rule is a lemma about weakest preconditions, wp_frame_l, and ∗ is defined on 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. resources rather than heaps.

• nanofil needs it because the facts that keep 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). from failing (this field points to a live 16-byte object) are about objects, and travel with whoever owns them. The planned logic's assertions own pieces keyed by 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.: an object's livelive 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. token, its bytes and its 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. slots. never_panics_by_invariant is the logic without separation, one invariant naming everything.

• The hand-rolled spike, Sep.v, defines ∗ as a split of a footprint of pieces; the Iris spike uses Iris's.

See How Iris works, Separation logic.