Resource Algebra

A resource algebra is an algebraic structure that specifies how resources — whether physical memory, logical permissions, or ghost state — can be composed, decomposed, and recombined in separation-logic proofs. Formally, it is a partial commutative monoid equipped with a validity predicate that prevents contradictory ownership claims from being combined.

The composition operation captures the intuition that two disjoint resources can be merged into a single resource describing their union. The partiality captures the constraint that not all resources are compatible: two threads cannot both hold exclusive write access to the same memory location. The validity predicate ensures that combined resources remain meaningful — preventing, for example, the construction of a resource that claims both ownership and non-ownership of the same object.

Resource algebras were developed as the foundation of Iris's treatment of ghost state, but the concept has proven general enough to unify disparate verification techniques. Any system that reasons about ownership, permissions, or access control can be viewed through the resource-algebra lens — suggesting that the algebraic structure of resource composition is a universal feature of sound local reasoning, not merely a technical device for concurrent program verification.

The resource algebra is not a convenience for proof engineers. It is the discovery that the logic of ownership has a mathematical structure — and that discovering this structure is what makes compositional verification possible.