Das Kapitel untersucht die Entwicklung der Trennlogik und verfolgt ihre Entwicklung von den späten 1990er Jahren bis hin zu modernen, gleichzeitigen Trennlogiken höherer Ordnung wie Iris. Es betont die grundlegende Rolle von Vor- und Nachbedingungen in den Programmspezifikationen und den Einsatz eines zersplitterten Gewerkschaftsfunktionärs, um trennende Konjunktionen zu bilden. Das Herzstück von Iris ist seine abstrakte Definition von Ressourcen, die flexibel genug sein müssen, um den Programmzustand und verschiedene Funktionen, die bei der Programmüberprüfung verwendet werden, zu handhaben. Das Kapitel stellt eine neuartige Eigenschaft dieser Ressourcen, die so genannten Kameras, vor und verwendet sie, um den Begriff der Ressourcenalgebren (RAs) zu vereinfachen. Sie konstruiert eine Kategorie von Ressourcenalgebren und zeigt, dass wichtige Kameras in der Iris einfache universelle Eigenschaften als RAs zulassen. Der Text vertieft sich auch in den historischen Kontext der Trennungslogik, das Aufkommen des Geisterstaates und die Komplexität, die durch Staat höherer Ordnung und Parallelität eingeführt wird. Er diskutiert die Definition von Kameras und ihre Beschränkungen, insbesondere das Fehlen einer geeigneten Kategorie von Kameras und die Herausforderungen bei der Artikulation der Vollständigkeit von Kameraxiomen. Das Kapitel stellt dann das maximale idempotente Axiom vor, um die Definition von Kameras zu vereinfachen und den Kernbetrieb durch eine einzige Eigenschaft zu ersetzen, die die Existenz eines maximalen idempotenten Elements sicherstellt. Diese Vereinfachung führt zu einer gut erzogenen Kategorie von Ressourcenalgebren, in der viele wichtige Ressourcenalgebren einfache universelle Eigenschaften aufweisen. Das Kapitel untersucht auch die Beziehung zwischen Ressourcenalgebren und anderen Kategorien und liefert universelle Charakterisierungen verschiedener Ressourcenalgebren. Es schließt mit einer Diskussion über die Implikationen dieser Ergebnisse für die Iris-Formalisierung im Coq und schlägt zukünftige Richtungen für die Ausweitung der Coq-Implementierung vor, um die gesamte Kategorie von Presheaves zu verwenden und den Begriff der Ressourcenalgebren zu übernehmen.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
We revisit the foundational notion of “resources” used by separation logics from a categorical and algebraic viewpoint. In particular, we show that the cameras used by concurrent, higher-order, impredicative separation logics like Iris as a generalization of partial commutative monoids can be simplified and clarified and we introduce a category of cameras in which many vital cameras exhibit simple universal properties. We do this by observing that an important structure on cameras (the core operator) can be uniquely constrained and replaced by the property governing the idempotent elements of the camera. We verify that all cameras used in practice in Iris satisfy this property and use this insight to simplify the existing Iris formalization.
1 Introduction
Since its introduction in the late 1990s and early 2000s separation logics [22, 24], have gone through numerous conceptual revisions and alterations. Modern higher-order concurrent separation logics such as Iris [18] are now vastly more complex and built on top of several layers of abstraction in order to account for concurrency and higher-order reasoning, but the premise is still fundamentally unchanged: specifications for a program are given by pre- and post-conditions which are some form of predicate on program state and a “disjoint union” operator on program state gives rise to a separating conjunction in these specifications.
To manage this complexity, Iris attempts to realize the vast majority of the program logic purely within a flexible base logic. The result is that base Iris is a standard higher-order logic supplemented with the connectives of bunched implication logic, a handful of modalities, and a family of propositions denoting ownership. The heart of Iris is therefore in its highly abstracted definition of resource used by ownership propositions. These must be flexible enough to handle not only program state but also to encode the various features (invariants, state transition systems, etc.) that program logics utilize to verify programs.
Our goal is to revisit these abstract resources, termed cameras1 in Iris, and isolate a new property of these structures. We capitalize on this new property to remove some of the complexity of cameras and obtain a simpler notion of resource algebras (RAs). We then construct a category of resource algebras and show that important cameras in Iris admit simple universal properties as RAs.
Anzeige
1.1 From heaps to cameras
The impetus for the more general notion of resource in Iris traces back to the advent of separation logic [24]. In particular, separation logic’s eponymous separating conjunction is derived from an important piece of additional structure carried by program heaps (the most basic realization of program state): a disjoint union operation. Recall that one may represent heaps as partial maps from locations (e.g., natural numbers) to values. Given two such heaps \(h_1,h_2\) with disjoint domains of definition, one may unambiguously form their union \(h_1 \uplus h_2\). With this to hand, one defines the separating conjunction as follows:
While predicates in the original separation logic were taken over exactly the data needed to execute a program—i.e., the state of the heap—it was quickly realized that this was inadequate for realistic programs. Their correctness often depended upon invariants or conditions that might not be reflected directly in the memory. While a variety of solutions were proposed, the most elegant was to simply enlarge the definition of “program state” to include ghost state: objects which were not strictly necessary to describe the program execution. A simple example of ghost state is heaps with fractional permissions, which can be used to account for whether a thread has read or write ownership of a heap location [5].
The unifying feature of this more general ghost state is a partial ‘union’ operation. Whatever ghost state is used, it forms a set M equipped with a partial commutative and associative operation \(\cdot \) (see, e.g., [6, 9, 10, 16]). Our definition of \(*\) generalizes to such an M without change2 whereby we can define the primitives of separation logic over an arbitrary partial commutative monoidM. This extra generality allows for a more conceptual definition of ghost state.
This story is complicated by higher-order state, concurrency, and other features. To cope with them, separation logics leverage step-indexing [1]. Rather than pre- and post-conditions being drawn from (monotone) predicates \(M \rightarrow \textrm{Prop}\), they are further indexed by a natural number \(\mathbb {N}\times M \rightarrow \textrm{Prop}\). The extra indexing soundly simulates arbitrary recursion in predicates.
In fact, embracing a small amount of revisionism, one can see all of this as ordinary separation logic done internally to a particular presheaf topos \(\textbf{PSh}({\omega })\) [3, 11, 21]. Working internally like this, it becomes natural to regard the partial commutative monoid as a “step-indexed” set with partial operations i.e., a partial commutative monoid internally to \(\textbf{PSh}({\omega })\). With this extra layer of generality, Jung et al. [18] showed that all the features of a modern concurrent separation logic could be built on top of ghost state within a higher-order logic.
Anzeige
With this motivation, we give a slightly imprecise definition of an Iris camera:
Definition 1
A camera consists of a (step-indexed) set M, a (step-indexed) partial multiplication operation (\(\cdot \)), and a partial operation \(|{-}|\) which (when defined) maps m to an idempotent element \(|{m}|\) such that \(|{m}|\cdot m = m\).
1.2 Core and duplicable propositions
Unfortunately, the definition of camera is far more complex than the above might indicate. As a result, it is difficult to give a high-level definition of cameras without eliding important details and it is challenging to articulate why the camera axioms are in any way complete.3 One manifestation of this poor behavior is the lack of a suitable category of cameras: there is no well-behaved notion of morphism of cameras and even simple constructions like the product of two cameras \(M_1 \times M_2\) lack any universal property which could give a more conceptual description.
Some of the complexity is not, strictly speaking, mathematical. For instance, representing partial operations and step-indexing in a proof assistant is known to be arduous and the definition of camera is tuned to make it as easy as possible to realize in Coq at the cost of more uniform behavior. However, a central aspect of the generalization of cameras over partial commutative monoids is to replace the unit element \(\epsilon \) with a core operation\(|{-}|\) which is both complex and slightly ad-hoc. As it stands, requiring the existence of this operator is a major obstacle towards a good category of cameras.
To properly situate the definition of core and motivate our proposed replacement for it, we once more turn to traditional separation logic. In this setting, there is a comonadic modality\(\Box \) defined by:
$$ ({\Box P})\,h \triangleq P({\emptyset }) $$
The \(\Box \) modality occurs frequently when working within separation logic: it isolates those specifications for which separating conjunction coincides with ordinary conjunction such that, e.g., \(\Box P\) can be duplicated to \(\Box P *\Box P\). In Iris, for instance, \(\Box \) is crucial for specifying features like invariants as well as for embedding ordinary propositions into the program logic. In the simple setting of traditional separation logic, \(\Box \) can actually be characterized in a number of distinct ways, any of which could be used to generalize \(\Box \) to arbitrary cameras:
\(\Box \) is defined by evaluating at the unit of \(\uplus \).
\(\Box \) is the “always” comonad from Kripke models of modal logic.
\(\Box \) is the unique operation preserving \(\top \), \(\wedge \), and \(\exists \) such that \(\Box ({\ell \mathrel {\hookrightarrow }v}) = \bot \).
\(\Box \) is defined by evaluating at the unique idempotent with respect to \(\uplus \).
In order to lift \(\Box \) to an arbitrary camera M, the definition of a camera more-or-less hard-codes the necessary structure for the fourth definition; the axioms of \(|{-}|\) are exactly those needed to ensure that \(P \mapsto P \circ |{-}|\) (modulo partiality) gives rise to a \(\Box \) modality.
Even this description hides some complexity. Bizjak and Birkedal [4] observed that absent step-indexing, there is a bijection between core structures and well-behaved \(\Box \) modalities. However, this (1) does not extend to the step-indexed case and (2) offers no insight as to which of the many \(\Box \) modalities should be chosen. In particular, when working with \(\textsf{Heap}\) there was a single clear choice of \(\Box \) modality with a variety of different characterizations. In contrast, for a general camera there are many distinct choices of core inducing distinct \(\Box \) modalities.
1.3 The maximal idempotent axiom
In this work, we simplify the definition of cameras by removing the core operation from their specification entirely. In its place, we instead impose a single additional property on our cameras insisting that for each \(a \in M\), there exists a maximal idempotent below a or no idempotents at all. To disambiguate, we term the resulting structure a resource algebra. In other words, rather than requiring each resource algebra to come equipped with a partial assignment of elements to idempotents below them, we require that there is always a ‘best’ such assignment which picks out the largest possible idempotent. This choice in turn yields a \(\Box \) modality uniquely defined as the largest modality satisfying the expected axioms.
This substantially simplifies the definition of a resource algebra: we exchange one operation and four axioms for this single new axiom. More than this, however, the removal of core makes it possible to give a satisfactory category of resource algebras\(\textbf{RA}\). Given that cameras are nearly partial commutative monoids, it was long suspected that they should organize into a well-behaved category. In particular, it was conjectured that various examples of cameras used in Iris (sums, products, etc.) ought to enjoy universal properties within this category. We confirm this conjecture and observe that all of the cameras by Iris can be realized as resource algebras and that many common cameras induce resource algebras arising from adjoints or universal constructions within \(\textbf{RA}\).
Our development of the theory of resource algebras takes place entirely within the internal language of \(\textbf{PSh}({\omega })\) and, consequently, does not mention step-indexing at all. In fact, our proofs are designed to apply also to transfinite versions of Iris (based on presheaves over larger ordinals) or separation logics without any step-indexing at all. The only cost for this generality is the need to work within a constructive setting.
Remark 1
The importance of maximum idempotent elements to isolate a universal core was noted independently by Dardinier et al. [7] in the context of automatic verification. We defer a more detailed comparison of till Section 7.
1.4 Contributions
We contribute a simpler and more abstract definition of “resources” for concurrent separation logics like Iris. We do this by removing a structure from Iris’s definition of camera and replacing it with a new axiom (the maximal idempotent axiom), thereby obtaining the new notion of a resource algebra. We show the following:
Every camera used in Iris satisfies the maximal idempotent axiom and therefore induces a resource algebra.
Every resource algebra induces a universal \(\Box \) modality.
Resource algebras assemble into a well-behaved category \(\textbf{RA}\) in which many important resource algebras enjoy simple universal properties.
All of our results are carried out within a version of extensional type theory and apply not just to step-indexing over \(\omega \) but to transfinite separation logics as well.
Finally, we show how to adapt the Iris formalization in Coq as it stands today to partially benefit from these results. In so doing, we also note various places where expediency of formalization has complicated the definition of cameras and give a precise account of the trade-offs these induce.
2 A brief reprise of \(\textbf{PSh}({\omega })\)
For much of this paper (Sections 3 to 5) we work internally to the topos of trees \(\textbf{PSh}({\omega })\). In this section, we review the basic properties of this internal language.
2.1 Type theory within \(\textbf{PSh}({\omega })\)
To begin with, we recall that \(\textbf{PSh}({\omega })\) is a presheaf topos and therefore supports a rich internal language: a model of extensional dependent type theory with all the standard connectives, including a hierarchy of universes (\(\mathcal {U}_{i}\)) [13, 14]. Among others, included in these are various inductive types such as the type of natural numbers, lists, and so on. We note that as we are dealing with extensional equality, both function extensionality (funext) and unicity of identity proofs (UIP) hold. As is standard, we largely ignore size issues and simply write \(\mathcal {U}\). Also included is a type of propositions \(\textrm{Prop}\) closed under all the standard logical connectives, including impredicative quantification. There is a function \(\textrm{Prf}: \textrm{Prop}\rightarrow \mathcal {U}\) which sends a proposition to the type of its proofs such that \(\textrm{Prf}({\phi })\) contains at most one element. Finally, \(\textrm{Prop}\) satisfies propositional extensionality: \(\textrm{Prf}({\phi }) \cong \textrm{Prf}({\psi }) \iff \phi = \psi \) where \(\cong \) refers to the standard notion of isomorphism of types.
Rather than explicitly adding all the necessary logical connectives to \(\textrm{Prop}\), we realize them all at once through the addition of an “inverse” of sorts to \(\textrm{Prf}\) sending a type \(A : \mathcal {U}_{i}\) to the propositional truncation \([A] : \textrm{Prop}\). The defining characteristic of propositional truncation is that if B is a type with at most one element, then \(A \rightarrow B \cong \textrm{Prf}({[A]}) \rightarrow B\). Consequently, \(\textrm{Prf}({[A]}) \cong A\) if A is a type containing at most one element e.g., if \(A = \textrm{Prf}({\phi })\). One can then show, for instance, that logical entailment \(\phi \rightarrow \psi \) can be defined as \([\textrm{Prf}({\phi }) \rightarrow \textrm{Prf}({\psi })]\).
Finally, the internal language supports the axioms of guarded recursion (a later modality \(\rhd \), Löb induction, etc.). Surprisingly, this structure is not relevant to our discussion of resource algebras and so we refer the reader to Birkedal et al. [3] for details and an explanation of the semantics of the internal language.
2.2 Partial maps within \(\textbf{PSh}({\omega })\)
For a first example of working within the internal language of \(\textbf{PSh}({\omega })\) and in preparation for Sections 3, we define the notion of a partial map. A naïve first guess might be to say that a partial map from \(A \rightharpoonup B\) consists of an ordinary function \(A \rightarrow \textbf{1} + B\). While this definition suffices in ‘ordinary’ external mathematics, it is too strict when working internally as we are. Indeed, this definition only captures functions whose domain of definition is decidable and we will frequently be interested in partial functions f where \(f(a)\downarrow \) is an arbitrary proposition and therefore—since \(\textbf{PSh}({\omega })\) does not satisfy excluded middle—typically undecidable.
We instead use the partial map classifier following Rosolini [25]:
Definition 2
If \(A : \mathcal {U}\) then the partial map classifier \({A}^{?}\) is \(\sum _{\phi : \textrm{Prop}} \textrm{Prf}({\phi }) \rightarrow A\).
A map \(f : A \rightarrow {B}^{?}\) encodes a partial map from A to B. Note that f consists of (1) a map \(f_0 : A \rightarrow \textrm{Prop}\) indicating where f is defined and (2) a map \(f_1 : ({a : A}) \rightarrow \textrm{Prf}({f_0\,a}) \rightarrow B\) giving the value of f when it is defined.
Definition 3
We define the type of partial maps \(A \rightharpoonup B\) to be \(A \rightarrow {B}^{?}\)
Lemma 1
\({-}^{?}\) is a monad whose unit and join operations are defined as follows:
We use standard monadic notation (\(x \leftarrow a; b({x})\)) to manipulate \({A}^{?}\) and write \({f}^{?} : {A}^{?} \rightarrow {B}^{?}\) for the functorial action.
Definition 4
We define the approximation partial order \(({\phi ,a}) \sqsubseteq ({\psi ,b}) : \textrm{Prop}\) on \({A}^{?}\) as \(\exists f : \textrm{Prf}(\phi ) \rightarrow \textrm{Prf}(\psi ).\, (z : \textrm{Prf}(\phi )) \rightarrow a\,z = b(f\,z)\).
3 Resource Algebras and the Maximal Idempotent Axiom
We now analyze the abstract definition of resources using the internal language. While this definition is closely related to Iris’s cameras, we avoid several maneuvers used by Iris to optimize for formalization in order to take full advantage of the internal language. A full comparison is provided in Section 6. We show how various portions of the definition may be replaced and folded into a single new axiom we term the maximal idempotent axiom.
3.1 Partial commutative semigroups and predicates
We begin with the basic notion of a type equipped with a partial multiplication:
Definition 5
A partial commutative semigroup (PCS) consists of a type A and a partial map \((\cdot ) : A \times A \rightharpoonup A\) satisfying the following conditions:
1.
If a, b : A then \(a \cdot b = b \cdot a : {A}^{?}\)
2.
If a, b, c : A then \(x \leftarrow (a \cdot b); x \cdot c = x \leftarrow (b \cdot c); a \cdot x : {A}^{?}\)
In light of (1) and (2), we may unambiguously write \(a \cdot b \cdot c\).
Lemma 2
If A is a PCS then \(a \le b \triangleq a = b \vee \exists c : A.\, a \cdot c = \textsf{ret}\,b\) is a preorder.
As mentioned in the introduction, the semantics of separation logics like Iris can be constructed within monotone predicates on a PCS \((A,\cdot )\):
$$ A \xrightarrow {\textsf{mon}} \textrm{Prop}\triangleq {\lbrace }{P : A \rightarrow \textrm{Prop}}{\vert }\forall a \le b.\, P(a) \rightarrow P(b){\rbrace } $$
We will not spell out how all the connectives of higher-order logic are interpreted into \(A \xrightarrow {\textsf{mon}} \textrm{Prop}\), but we record the definition of \(*\) for intuition:
The classical definition of a camera is a PCS with a core operation:
Definition 6
If \((A,\cdot )\) is a PCS, a core structure on A is a map \(|{-}|: A \rightarrow \textbf{1} + A\) satisfying the following conditions:
1.
If \(|{a}|= \textsf{in}_{2}(a')\) then \(a' \cdot a = \textsf{ret}\,a\).
2.
If \(|{a}|= \textsf{in}_{2}(a')\) then \(|{a'}|= \textsf{in}_{2}(a')\).
3.
If \(a \le b\) then \(|{a}|\le |{b}|\)
For the last point, we order \(\textbf{1} + A\) such that \(\textsf{in}_{1}(\star )\) is the minimum element.
Definition 7
A camera is a PCS equipped with a core structure.4
As mentioned in the introduction, any core structure induces a comonadic modality \(\Box \) on monotone predicates \(A \xrightarrow {\textsf{mon}} \textrm{Prop}\):
If \(|{-}|\) is a core structure then the induced \(\Box \) modality is monotone, comonadic (\(\Box P \rightarrow P\) and \(\Box \Box P \iff \Box P\)), and commutes with \(\exists \), \(\rhd \), and satisfies the following: \((\Box P) \wedge Q \iff (\Box P) *Q\)
For the purposes of separation logic, it is the last property that is most vital. It allows a user of separation logic to freely exchange separating and ordinary conjunction when manipulating \(\Box P\) and thereby allows one to e.g., duplicate \(\Box P\) into \(\Box P *\Box P\) and similar. Intuitively, \(\Box P\) is the closest replacement of P which satisfies this property. Unfortunately, this idea is complicated by the fact that there are often great many distinct core structures which one may choose to equip \((A,\cdot )\) with, and they induce distinct modalities. It is thus far from clear which core structure (if any) actually forces \(\Box P\) to realize the above description.
This situation is in contrast to the motivating example with monotone predicates on heaps where the \(\Box \) modality could be characterized by several universal properties. Our goal is to isolate a property of core which fully constrains its definition to give the largest possible \(\Box \) modality. That is, we wish to find a core structure \(|{-}|\) so that if \(|{-}|'\) is another core structure then \(\forall P.\,\Box _{|{-}|'} P \rightarrow \Box _{|{-}|} P\).
We begin by massaging Definition 6 into a form which is easier to work with. If \(|{-}|\) is a core structure and \(|{a}|= \textsf{in}_{2}(a')\) then \(a'\) is an idempotent element (by 1 and 2). In light of 3, we may therefore view \(|{-}|\) as a monotone assignment \(A \rightarrow \textbf{1} + \textsf{Idem}(A)\) and, more specifically, an assignment \((a : A) \rightarrow {\lbrace }{x : \textbf{1} + \textsf{Idem}(A)}{\vert }{x \le \textsf{in}_{2}(a)}{\rbrace }\).
Lemma 4
A core structure on \((A,\cdot )\) is equivalent to a monotone map \((a : A) \rightarrow {\lbrace }{x : \textbf{1} + \textsf{Idem}(A)}{\vert }{x \le \textsf{in}_{2}(a)} {\rbrace }\).
A great many such monotone maps are possible for most PCSs. For instance, the constant map \(\lambda a \rightarrow \textsf{in}_{1}(\star )\) is always available and if A has a global unit \(\epsilon \), then \(\lambda a \rightarrow \textsf{in}_{2}(\epsilon )\) is also a valid choice. As core structures are particular monotone maps between preorders, they themselves inherit a preorder defined pointwise.
Lemma 5
The assignment of core structures to \(\Box \) modalities is monotone: if \(|{-}|\) and \(|{-}|'\) are two core structures such that \(|{-}|\le |{-}|'\) then \(\Box _{|{-}|} P \rightarrow \Box _{|{-}|'} P\).
We note that we have have already encountered the unique minimal core structure for any PCS: the assignment \(\lambda a \rightarrow \textsf{in}_{1}(\star )\) which discards all information of a. Unfolding, this core structure induces the \(\Box \) modality which sends every proposition to \(\bot \), which is clearly the smallest possible modality. Much more useful is the maximal\(\Box \) modality.
In order to obtain the largest possible \(\Box \) modality, it suffices to construct a core structure which is maximal. In particular, it would suffice to ensure \(|{-}|\) sends a to the largest possible idempotent element contained within a and which is undefined only if no idempotent element exists. Notice that a priori there may be distinct maximal core structures as A is merely pre-ordered, but every PCS is partially-ordered on idempotent elements, in particular:
Lemma 6
If i, j are idempotents such that \(i \le j\) and \(j \le i\) then \(i = j\).
Proof
By assumption so there exists \(i'\) and \(j'\) such that \(i \cdot i' = \textsf{ret}\,j\) and \(j \cdot j' = \textsf{ret}\,i\). Since both i and j are idempotent, this tells us that \(j \cdot i = \textsf{ret}\,i\) and \(i \cdot j = \textsf{ret}\,j\). Commutativity then tells us that \(i = j\).
In particular, core structures are partially-ordered and (using pointwise multiplication) form a join semi-lattice. We therefore conclude the following:
Corollary 1
Maximal core structures are unique.
Unfortunately, there is no guarantee that a maximal core structure need exist:
Lemma 7
There exists a PCS for which there is no maximal core structure.
Proof
Consider the PCS on \(A = \mathbb {N}+ \textbf{1} = \{0 \dots \infty \}\) where (1) \(n \cdot m = \max (n,m)\) (2) \(n \cdot \infty = \infty \cdot n = \infty \) and (3) \(\infty \cdot \infty \) is undefined. Note that \(\textsf{Idem}(A)\) consists of all elements of A except \(\infty \).
To define a core structure on A, note that if \(|{\infty }|= \textsf{in}_{2}(n)\), then \(|{m}|\le \textsf{in}_{2}(n)\) for all m by (3) and if \(|{\infty }|= \textsf{in}_{1}(\star )\) then \(|{m}|= \textsf{in}_{1}(\star )\). It follows that any core structure \(|{-}|\) where \(|{\infty }|= \textsf{in}_{2}(n)\) must be smaller than the core structure \(|{-}|^{n+1}\) defined by \(|{\infty }|^{n+1} = \textsf{in}_{2}(n + 1)\) and \(|{m}|^{n+1} = \textsf{in}_{2}(\min (n + 1, m))\). This yields an ascending chain of core structures \(|{-}|^{1} < |{-}|^{2} \dots \) for which there is no upper bound.
Fortunately, maximal core structures do exist in a wide variety of circumstances. For instance, it was necessary that our above counterexample involved an infinite number of idempotent elements.
Lemma 8
If for each a : A, \({\lbrace }{x : \textbf{1} + \textsf{Idem}(A)}{\vert }{x \le \textsf{in}_{2}(a)}{\rbrace }\) is equivalent to a finite type \(\mathbb {N}_{\le n}\) for some n, then A has a maximal core structure.
Many common PCSs have only a single idempotent element each element e.g.:
Corollary 2
\(\textsf{Heap}\) has a maximal core structure: \(\lambda h \rightarrow \epsilon \).
3.3 The maximal idempotent axiom
We can reformulate the requirement that PCS possess a maximal core structure into the following property:
Definition 8
(The Maximal Idempotent Axiom). A PCS \((A,\cdot )\) satisfies the maximal idempotent (MI) axiom if the following holds for all a : A:
$$\begin{aligned} &\textsf{MI}(a) \triangleq \lnot (\exists i \le a.\, i\,\textsf{idem}) \vee ( \exists i \le a.\,i\,\textsf{idem} \wedge \forall j \le a. j\,\textsf{idem} \rightarrow j \le i ) \end{aligned}$$
In other words, below each a : A there either exists a maximal idempotent or there are no idempotents at all.
A priori, one may worry that the mere existence of a maximal idempotent below a : A does not suffice to construct a function \(|{-}|\) picking it out. After all, in general constructing such a function amounts to the axiom of choice and the lack of excluded middle implies the failure of the axiom of choice internal to \(\textbf{PSh}({\omega })\). However, as a topos \(\textbf{PSh}({\omega })\) does satisfy the axiom of unique choice: if \(\forall a : A.\,\exists ! b : B.\,\varPhi (a,b)\) then \(\exists ! f : A \rightarrow B.\,\forall a : A.\,\varPhi (a,f(a))\). Since maximal idempotents are unique, we obtain the following:
Theorem 1
If \((A,\cdot )\) satisfies the MI axiom then A has a maximal core structure.
Lemma 9
If \(\phi ,\psi : \textrm{Prop}\) such that \(\phi \wedge \psi = \bot \) then \(\textrm{Prf}(\phi \vee \psi ) \cong \textrm{Prf}(\phi ) + \textrm{Prf}(\psi )\).
Lemma 10
If \(A : \mathcal {U}\) and \(\phi : A \rightarrow \textrm{Prop}\) such that \(\exists a : A.\,\phi \,a = \exists ! a : A.\,\phi \,a\) then \(\textrm{Prf}(\exists a : A.\,\phi \,a) \cong \sum _{a : A} \textrm{Prf}(\phi \,a)\).
Proof
(Theorem1). Since the total absence of idempotents and the presence of maximal idempotent are disjoint, \(\textrm{Prf}(\textsf{MI}(a))\) is equal to the following:
$$ (\textrm{Prf}(\exists i \le a.\, i\,\textsf{idem}) \rightarrow \bot ) + \textrm{Prf}( \exists i \le a.\,i\,\textsf{idem} \wedge \forall j \le a. j\,\textsf{idem} \rightarrow j \le i ) $$
Next, since maximal idempotents are unique, the second summand is equivalent to unique existence, whereby we may replace it with the following:
$$ ((i : A) \rightarrow i \le a \rightarrow i\,\textsf{idem} \rightarrow \bot ) + \sum \nolimits _{i \le a} i\,\textsf{idem} \times ((j \le a) \rightarrow j\,\textsf{idem} \rightarrow j \le i) $$
In other words, \(\textrm{Prf}(\forall a : A.\,\textsf{MI}(a))\) is equivalent to a choice function sending each element of A to the maximal idempotent below A or a proof that there are no idempotents below A at all. This function is the required maximal core structure.
This addresses a rather mysterious fact about cameras: why are core structures partial in a different way than \(\cdot \)? In light of the above, we see that a core structure \(|{-}|\) has decidable support because \(|{a}|\) is undefined just when a contains no idempotents at all and the MI axiom guarantees that this is decidable.
We now redefine and simplify cameras from their formulation in Iris. Rather than insisting that a camera be a PCS equipped with a core structure, we instead ask that it satisfy the MI axiom. This has the simultaneous advantages of (1) ensuring that the induced core structure is as large as possible while also (2) merely being a property to check, not an additional structure.
Definition 9
A resource algebra is a PCS satisfying the maximal idempotent axiom. Write \(\textsf{RA}\) for the type of all resource algebras.
To justify this definition, we show that it is not overly restrictive (Section 4) and that it opens up more conceptual descriptions of existing cameras (Section 5).
4 Examples of cameras
If Definition 9 is to be an adequate replacement for the current definition of cameras in Iris, it must not rule out examples which are currently used in practice. Fortunately, every camera currently used in the Iris formalization in Coq satisfies the MI axiom. For reasons of space, we present only a handful of the most important resource algebras used in separation logic and illustrate the proofs that they satisfy the MI axiom. We divide these examples into two categories: basic stock cameras which are used in a wide variety of constructions and a few operations on cameras used to build up more complex examples.
4.1 Basic resource algebras
For the basic ‘building block’ resource algebras, Lemma 8 suffices to show that the relevant PCSs satisfy the MI axiom; in practice, they all have no idempotent elements, one idempotent element, or every element is idempotent. We illustrate this with two representative examples.
First, the exclusive resource algebra which is used to encode ownership of non-duplicable abstract resources:
Lemma 11
If \(A : \mathcal {U}\), regard A as a PCS \(\textsf{Excl}(A)\) where \(\cdot _{\textsf{Excl}(A)}\) is undefined everywhere. \(\textsf{Excl}(A)\) satisfies the MI axiom.
Proof
Such a camera has no idempotents, so Lemma 8 trivially applies.
For another extreme example, we consider the agreement resource algebra which is used to enforce global agreement about a particular value. For this, take a type \(A : \mathcal {U}\) and regard A as a PCS \(\textsf{Ag}(A)\) using the following partial multiplication operation: \(a \cdot _{\textsf{Ag}(A)} a' \triangleq (a = a', \lambda \_ \rightarrow a)\).
Lemma 12
For any \(A : \mathcal {U}\), \(\textsf{Ag}(A)\) satisfies the MI axiom.
Proof
Lemma 8 applies as the only element contained in \(\textsf{Idem}(A)_{\le a}\) is a itself.
4.2 Constructions on resource algebras
The power of resource algebras is their composability: given simple resource algebras like those outlined above, we may stitch them together into more powerful constructions like \(\textsf{Heap}\). We outline the most important constructions for combining resource algebras and show that they preserve the MI axiom.
Given two resource algebras A and B we consider pointwise multiplication:
$$ (a, b) \cdot _{A \times B} (a', b') \triangleq \bar{a} \leftarrow a \cdot a'; \bar{b} \leftarrow b \cdot b'; \textsf{ret}(\bar{a}, \bar{b}) $$
Lemma 13
If A and B are resource algebras, \(A \times B\) satisfies the MI axiom.
Proof
Fix a pair (a, b). An idempotent below \((a,b)\) consists of a pair \((i,j)\) of idempotents i below a and j below b. By the MI axiom of both A and B, it is decidable whether or not there exists any idempotents below either a or b whence whether any such pair \((i,j)\) exists. By a further application of the MI axiom, if such a pair exists, there is a pair of maximal idempotents as required.
Given a resource algebra A, we can construct the resource algebra \(\textsf{Opt}(A) = \textbf{1} + A\) adjoining a new element to A. This element will act as the unit of multiplication, meaning the partial multiplication operation will be defined as:
$$ x \cdot _{\textsf{Opt}(A)}~\hbox {y} \triangleq {\left\{ \begin{array}{ll} \textsf{ret}(y) & x = \textsf{in}_{1}(\star ) \\ \textsf{ret}(x) & y = \textsf{in}_{1}(\star ) \\ {\textsf{in}_{2}}^{?}(a \cdot _{A} a') & x = \textsf{in}_{2}(a), y = \textsf{in}_{2}(a') \end{array}\right. } $$
Lemma 14
\(\textsf{Opt}(A)\) satisfies the MI axiom.
Proof
Fix \(x : \textsf{Opt}(A)\). If \(x = \textsf{in}_{1}(\star )\), then x itself is idempotent and thus the necessary maximal idempotent. If instead \(x = \textsf{in}_{2}(a)\), then the idempotents below x are either of the form \(\textsf{in}_{1}(\star )\) or \(\textsf{in}_{2}(i)\) where i is an idempotent below a. Accordingly, the maximal idempotent below \(\textsf{in}_{2}(a)\) is either the maximal idempotent below a or \(\textsf{in}_{1}(\star )\) if no such idempotent exists.
For our final example, we describe a more complex construction assembling a collection of resource algebras together. This ‘direct sum’ operation is used pervasively in Iris: any real use of Iris is based on this resource algebra to stitch together all of the resources required the verification of a given program. We describe it in more generality than it is presented in Iris by allowing for direct sums to be indexed by a type I with decidable equality.
Fix a family of resource algebras \(A : (i : I) \rightarrow \textsf{RA}\), let \(\bigoplus _{i : I} A\,i\) denote the type of partial maps \((i : I) \rightarrow A(i)\) with decidable and non-empty, finite support. Representing these in type theory can be somewhat difficult, but our internal language is strong enough to define quotient types (using \(\textrm{Prop}\)). Accordingly, we realize \(\bigoplus _{i : I} A\,i\) as a quotient of the following type:
The quotienting relation identifies two triples \((n, f, a)\) and \((n', f', a')\) just when \(n = n'\) and there is a bijection \(\sigma : \mathbb {N}_{\le n} \rightarrow \mathbb {N}_{\le n}\) such that \(f = f' \circ \sigma \) and \(a = a' \circ \sigma \).
For convenience, we will write elements of \(\bigoplus _{i : I} A\,i\) as \(\{(i_0, a_0), \dots , (i_n, a_n)\}\) where \(i_0, \dots , i_n\) are disjoint elements of I and \(a_k : A\,i_k\).
Lemma 15
\(\bigoplus _{i : I} A\,i\) is a partial semigroup under pointwise multiplication.
Proof (Sketch)
The definition of pointwise multiplication is somewhat involved and so we only sketch it here. Fix two elements \(\rho = \{(i_0, a_0), \dots , (i_n, a_n)\}\) and \(\rho ' = \{(j_0, b_0), \dots , (j_m, b_{m})\}\). Rearranging the elements of \(\rho '\) if necessary, we assume that there exists \(\ell \) such that \(i_k = j_k\) if \(k < \ell \) and outside of these pairs, the sequences Is are disjoint. Note that this requires I to have decidable equality.
We define the \(\rho \cdot \rho '\) by multiplying together the \(\ell \) elements overlapping between \(\rho \) and \(\rho '\) and, when these are all defined, returning the partial map with these the results and along with the elements of \(\rho \) and \(\rho '\) outside the overlap:
Since \({-}^{?}\) is a commutative monad, the order of these multiplications are irrelevant and so this process respects the equivalence relation quotienting \(\bigoplus _{i : I} A\,i\).
Theorem 2
\(\bigoplus _{i : I} A\,i\) satisfies the MI axiom.
Proof
Fix \(\rho = \{(i_0, a_0), \dots , (i_n, a_n)\}\). Since \(\textsf{MI}(\rho )\) is a proposition the quotienting is irrelevant and we ignore it. Next, note that if \(\sigma \cdot \sigma ' = \textsf{ret}(\rho )\), then the support of \(\sigma \) and \(\sigma '\) must be subsets of the support of \(\rho \). Accordingly, if \(\sigma \) is an idempotent within \(\rho \), then it consists of a collection of idempotents drawn from \(A\,i_k\) below the corresponding element \(a_k\).
Since each \(A\,i_k\) is a resource algebra, the MI axiom tells us that there is either (1) no idempotent below \(a_k\) or (2) a maximal idempotent \(a_k'\) below \(a_k\). Without loss of generality, let us assume that \(a_k\) has a maximal idempotent if and only if \(k \le m\) for some m and no idempotent below it \(k > m\).
The maximal idempotent below \(\rho \) is then given by \(\sigma = \{(i_0, a'_0), \dots , (i_{m}, a'_m)\}\). Indeed, any other idempotent \(\sigma '\) below \(\rho \) must have a smaller support than \(\sigma \) and, where both are defined, the value of \(\sigma '\) is smaller than that of \(\sigma \) by construction.
Note that the above depends critically on the fact that the existence of a maximal idempotent is decidable. We must be able to analyze whether the \(i_k\) entry is to be included based on whether or not \(a_k\) contains a maximal idempotent.
To conclude this section, we describe how one can combine these simpler resource algebras into more complex constructions needed for realistic program logics. For instance, the foundational resource algebra representing heaps can be constructed as follows. Writing \(\textsf{Loc}\) and \(\textsf{Val}\) to be the types of locations and (syntactic) values in a hypothetical imperative language, we define the resource algebra of heaps in this language as follows:
In this definition \(\textsf{in}_{1}(\star )\) represents the empty heap, and the exclusive resouce algebra ensures that multiplication of heaps is only defined when the locations of the relevant heaps are disjoint. In particular, there is no need to check the MI axiom here: it is automatic since all constructions involved preserve its validity.
5 The Category of Resource Algebras
We now turn to the properties of resource algebras collectively by structuring them into a category. In particular, we show that many resource algebras that are important in practice satisfy simple and recognizable universal properties. The proofs of these facts are not terribly difficult, but this is the point; by isolating a well-behaved definition of resource algebra these calculations are of the sort familiar to any category of algebraic structures.
To define the category of resource algebras, we must, of course, decide on what a morphism of resource algebras should be. Since a resource algebra is a PCS satisfying an additional property, a first idea is to define the category of resource algebras to be a full subcategory of partial commutative semigroups. This is analogous to how, e.g., a morphism of abelian groups is an ordinary group homomorphism whose domain and codomain happen to be abelian. When formulating morphisms of PCSs, the real wrinkle is partiality; from a categorical point of view, PCSs are commutative semigroups in the Kleisli category of \({-}^{?}\). But Kleisli categories for a monad are usually poorly behaved and \({-}^{?}\) is no exception. The solution is to integrate the partial ordering \(\sqsubseteq \) introduced in Section 2:
Definition 10
A morphism of resource algebras\(f : (A,\cdot ) \rightarrow (B,\cdot )\) is a function \(f : A \rightarrow B\) such that \({f}^{?}(a_0 \cdot a_1) \sqsubseteq f(a_0) \cdot f(a_1)\) when \(a_0,a_1 : A\).
Informally: a morphism of resource algebras is a morphism between carriers which commutes with multiplication provided the multiplication is defined in the domain. Such morphisms are commonly referred to as lax morphisms since we do not, e.g., require \(f(a_0) \cdot f(a_1)\) to be undefined if \(a_0 \cdot a_1\) is undefined. As we shall see, lax morphisms enjoy better categorical properties.
Lemma 16
Resource algebras and morphisms of such form a category \(\textbf{RA}\).
5.1 First steps with \(\textbf{RA}\)
We now record a few basic properties of \(\textbf{RA}\):
Lemma 17
\(\textbf{RA}\) has finite products and finite coproducts.
Proof
Initial and terminal objects are given by \(\textbf{0}\) and \(\textbf{1}\) with the obvious multiplication maps. We have already encountered Lemma 13 and, since the construction of coproducts is unsurprising, we content ourselves with showing that \(A \times B\) has the expected universal property.
To this end, observe that the projection maps \(\pi _{1} : A \times B \rightarrow A\) and \(\pi _{2} : A \times B \rightarrow B\) are both morphisms of resource algebras. Surprisingly, this is the most subtle part of the proof and it depends upon the fact that we require only that \({\pi _{1}}^{?}(p \cdot q) \sqsubseteq \pi _{1}\,p \cdot \pi _{p}\,q\) rather than equality. To see that the universal property is satisfied, we need only show that if C is a resource algebra such that \(f : C \rightarrow A\) and \(g : C \rightarrow B\) are morphisms, then \(\lambda c.\, (f\,c,g\,c)\) is a morphism to \(A \times B\). This is a routine calculation.
The universal property of the direct sum algebra is slightly longer to describe as it is not a simple limit or colimit. However, in light of the complexity of the definition of multiplication in \(\bigoplus _{i : I} A\,i\), we note that even though the universal property is complex, it is significantly more conceptual than the actual definition.
Definition 11
A compatible cocone over A is a family of morphisms \((f_i : A\,i \rightarrow C)_{i : I}\) such that for every finite family of elements \(a_0 : A\,i_0, \dots , a_n : A\,i_n\) the product \(f_{i_0}\,a_0 \cdot \ldots \cdot f_{i_n}\,a_n\) is defined.
Lemma 18
The resource algebra \(\bigoplus _{i : I} A\,i\) along with the canonical inclusions \(A\,i \rightarrow \bigoplus _{i : I} A\,i\) is the universal compatible cocone over A.
In other words, modulo partiality \(\bigoplus _{i : I} A\,i\) is the coproduct of A; it is the universal way to include each \(A\,i\) inside a single resource algebra in such a way that multiplications between disjoint elements are permitted.
5.2 The relation between \(\textbf{RA}\) and other categories
A number of the resource algebras encountered in Section 4 can be characterized as adjoints of natural functors between \(\textbf{RA}\) and other categories. For instance, \(\textsf{Excl}\) and \(\textsf{Ag}\) are both left adjoints to certain functors from \(\textbf{RA}\) to the category of small types and functions between them (denoted \(\textbf{TY}\)).
Lemma 19
\(\textsf{Excl}\) is left adjoint to the forgetful functor \(\textbf{RA}\rightarrow \textbf{TY}\).
Proof
Examining definitions, since multiplication in \(\textsf{Excl}\) is always undefined, a morphism \(\textsf{Excl}(A) \rightarrow B\) is precisely a map from A to the carrier of B, as required.
A similar argument gives a universal characterization of \(\textsf{Ag}\):
Lemma 20
\(\textsf{Ag}\) is left adjoint to the functor \(\textsf{Idem} : \textbf{RA}\rightarrow \textbf{TY}\) that maps a resource algebra to its set of idempotents.
The final result concerns \(\textsf{Opt}\). As this resource algebra extends an existing resource algebra with a unit element (i.e., an element \(\epsilon \) where \(\epsilon \cdot - = \textsf{ret}\)), it is reasonable to guess that \(\textsf{Opt}(A)\) is the resource algebra “freely generated” by A along with a unit. To state this precisely, we introduce unital resource algebras:
Definition 12
A unital resource algebra is a resource algebra \((A,\cdot )\) with a unit and a unital morphism a morphism of resource algebras preserving the unit.
Definition 13
The category of unital resource algebras is denoted \(\textbf{uRA}\).
Lemma 21
There is a forgetful functor \(U : \textbf{uRA} \rightarrow \textbf{RA}\) and the left adjoint to this functor is given by \(\textsf{Opt}\).
We note that while the proof of this lemma is straightforward, it is simply false if the definition of resource algebra included a core structure as data.
For a small example of how all of these universal properties combine, let us turn to the ‘map of resource algebras’ used to instantiate Iris: \(\textsf{Opt}(\bigoplus _i A\,i)\). We can give a concise description of this rather large resource algebra as the universal method of collecting together the family of resource algebras A and freely adjoining a unit.
6 From the topos of trees to the Iris formalization
Thus far, we have taken our motivation from Iris and its formalization in Coq but focused our attention on the better-behaved \(\textbf{PSh}({\omega })\) and its internal type theory. While this is ideal for working on paper, Iris and its realization in Coq must also optimize for the practicalities of formalization with Coq and therefore use only a subcategory of \(\textbf{PSh}({\omega })\) and a more ad-hoc replacement for \({-}^{?}\) in its definition of cameras. In this section, we discuss the impact of our results in Sections 3 to 5 for Iris and its formalization in Coq. Within this section we disregard the internal language of \(\textbf{PSh}({\omega })\) and work externally. For clarity, we refer to cameras as they appear in the Iris formalization as Iris cameras and reserve the terms camera and resource algebra for the notions discussed in Section 3.
6.1 Cameras in Iris
We begin with a brief summary of Iris. Rather than using all of \(\textbf{PSh}({\omega })\), Iris’s basic types are drawn from the full subcategory of total presheaves:
Definition 14
A total presheaf \(X : \textbf{PSh}({\omega })\) is one whose restriction maps \(X(n + 1) \rightarrow X(n)\) are surjective.
Equivalently, a total presheaf is a set X together with a family of equivalence relations \((\equiv _0) \subseteq (\equiv _1) \dots \) such that \(X = \mathop {\textsf{lim}}\nolimits _{n} X/(\equiv _n)\) i.e., a COFE in Iris parlance [18]. Under this encoding, a natural transformation between total presheaves is a map of sets which respects all the equivalence relations. Total presheaves are closed under products, sums, exponentials, the partial map classifier, and various other operations in \(\textbf{PSh}({\omega })\). However, they are not closed under finite limits, do not form a locally cartesian closed category, and lack a strong internal language.
To ease formalization, Iris avoids using \({-}^{?}\) and encodes of partiality indirectly:
Definition 15
A (total) lifted PCS (LPCS) \((X,\cdot ,\mathcal {V})\) is a (total) presheaf X with an associative and commutative natural transformation \(\cdot : X \times X \rightarrow X\) and a validity predicate\(\mathcal {V} : X \rightarrow \textrm{Prop}\) such that \(\forall x,y \in X(n).\, \mathcal {V}_n(x \cdot _n y) \subseteq \mathcal {V}_n(x)\).5
Intuitively, we have arranged for \(\cdot \) to be total by having X also contain sentinel values. The role of \(\mathcal {V}\) is then to carve out those elements of X which are genuine from those merely representing undefined multiplications.
One PCS \((M, \cdot )\) induces an LPCS by taking \(({M}^{?}, \bar{\cdot }, \pi _{1})\) where \(\bar{\cdot } : {M}^{?} \times {M}^{?} \rightarrow {M}^{?}\) is the Kleisli extension of \(\cdot \). The reverse is also possible: given \((X,\cdot ,\mathcal {V})\) one can take the subpresheaf of valid elements along with the partial map induced by \(\cdot \) defined only when \(x \cdot y\) is valid. The loop PCS \(\rightarrow \) LPCS \(\rightarrow \) PCS is the identity.
Definition 16
A core structure on a total LPCS \((X,\cdot ,\mathcal {V})\) is a natural transformation \(|{-}|: X \rightarrow \textbf{1} + X\) satisfying the following properties:
If \(x \in X(n)\) and \(|{x}|= \textsf{in}_{2}(x')\) then \(x' \cdot x = x\) and \(|{x'}|= \textsf{in}_{2}(x')\).
\(|{-}|\) is monotone with respect to the extension order on X.
In general, a core structure on an LPCS is distinct from a core structure on the induced PCS due to the presence of invalid elements. However, one can always extend a core structure on a PCS to a core structure on the induced LPCS.
Definition 17
An Iris camera is a total LPCS equipped with a core structure.
In fact, the definition is more relaxed: a total presheaf can be represented as a family of equivalence relations on a set \((X,(\equiv )_n)\) satisfying \(X = \mathop {\textsf{lim}}\nolimits _{n} X/(\equiv )_n\). Iris currently requires only the strictly weaker condition that \((\bigcap _{n} (\equiv _n)) = {\lbrace }{(x,x)}{\vert }{x \in X}{\rbrace } \) of its cameras to e.g., give a particular definition of the agreement camera. We will return to this point in Section 6.3.
6.2 Maximal idempotent axiom for Iris cameras
Despite the difference between a core structure on an Iris camera and a core structure on the induced partial commutative semigroup, one can translate the definition of the MI axiom into the language Iris cameras:
Definition 18
An Iris camera X satisfies the maximal idempotent axiom if the following holds for every n and \(x : X(n)\) such that \(n \in \mathcal {V}_n(x)\):6
$$\begin{aligned} &(\forall y : X(0).\, y \le {x}\vert _{0} \wedge y \cdot _0 y = y \rightarrow \bot ) \\ &\quad \vee ( \exists y : X(n).\, y \le x \wedge y \cdot _n y = y \wedge \forall m \le n, z : X(m).\,z \le {x}\vert _{m} \wedge z \cdot _m z = z \rightarrow z \le {y}\vert _{m} ) \end{aligned}$$
We have written e.g., \({x}\vert _{m}\) for the functorial action \(X(m \le n)(x)\).
This definition is mechanically produced by unfolding the internal definition in \(\textbf{PSh}({\omega })\) of the maximal idempotent axiom [3]. For instance, PCS satisfies the MI axiom if and only if the induced LPCS satisfies the above proposition.
Theorem 3
Every Iris camera in the Iris formalization satisfies the MI axiom.
We have proven this by extending the Iris formalization with proofs of the MI axiom for every Iris camera [12]. More precisely, the accompanying Coq formalization of this paper modifies the existing Iris formalization in Coq by (1) removing the core operation from the structure defining cameras and (2) replacing it with the above translation of the MI axiom. We have then carried this change through the rest of the formalization by updating every camera used in the codebase with a proof of the MI axiom. Notably, we did not need to make significant modifications to other parts of the Iris codebase and no case studies were affected.
In total then, the theoretical work done in Section 3 has allowed us to remove explicit constructions in the Iris formalization and replace them with more conceptual arguments all without requiring any change to the complicated proofs in separation logic currently carried out within Iris.
Remark 2
As discussed in Section 3, one may as well replace \(\vee \) with \(+\) and \(\exists \) with \(\textstyle \sum \). When extending the Iris formalization, we have made these substitutions as Coq’s metatheory is too weak to justify either replacement without axioms.
6.3 Categories of Iris cameras
While the MI axiom can be used to save effort and complexity in the formalization, the results of Section 5 do not translate so easily. There are several incompatible possible definitions of morphisms for Iris cameras and none are fully satisfactory. For instance, morphisms may be themselves total or only defined on valid elements, they may preserve validity laxly or strictly, etc. Each of these definitions gives rise to a category satisfying some, but not all, of the properties of \(\textbf{RA}\). Fundamentally, the issue is that totalizing a PCS forces us to consider invalid elements.
There exists a well-behaved subclass of LPCSs which organize into a category: the image of the map \((M,\cdot ) \mapsto ({M}^{?}, \bar{\cdot }, \pi _{1})\). However, important Iris cameras do not land in this class of LPCSs because e.g., their underlying types are discrete.
For a concrete example of how this state of affairs complicates research in Iris, consider the resource algebra \(\textsf{Ag}(A)\) from Section 4. It induces an Iris camera by passing to the induced LPCS \(\hat{\textsf{Ag}}(A) = {\textsf{Ag}(A)^{?}}\) which satisfies the desiderata of the agreement Iris camera [18, Section 4.3]. A closely related construction appeared in Jung et al. [17], but was criticized for being exceptionally difficult to define [18]; this suggests an advantage of our categorical approach which yields \(\hat{\textsf{Ag}}(A)\) as the composition of a number of simple and canonical results.
Rather than \(\hat{\textsf{Ag}}(A)\), Jung et al. [18] use a more ad-hoc construction \(\textsf{Ag}'(A)\) as it is easier to formalize. However, \(\textsf{Ag}'(A)\) is not a total presheaf: we do not have \(\textsf{Ag}'(A) = \mathop {\textsf{lim}}\nolimits _{n} \textsf{Ag}'(A)/(\equiv )_n\) because of the presence of ‘junk’ elements which are never valid. This motivated practitioners to stop requiring that Iris cameras satisfy the completeness condition. However, these junk elements ensure that \(\textsf{Ag}'(A)\) is not the totalization of a PCS and it is therefore not among those LPCSs which organize into a well-behaved category. Consequently, we have no good universal property describing \(\textsf{Ag}'(A)\).
From our point of view, however, the issue is not with \(\hat{\textsf{Ag}}(A)\)—it has the expected universal property—but with the insistence on lifted PCSs. For instance, while \(\textsf{Ag}'(A)\) is easier to deal with than \({\textsf{Ag}(A)^{?}}\), it is still more complex than the underlying type of \(\textsf{Ag}(A)\): A! Strikingly, \(\textsf{Ag}(A)\) is simpler to define than \(\textsf{Ag}'(A)\) and the motivating advantage besides simplicity recommending \(\textsf{Ag}'(A)\) over \(\hat{\textsf{Ag}}(A)\)—a technical property involving the interaction between \(\textsf{Ag}'(A)\) and the later modality—follows without any additional effort for the resource algebra \(\textsf{Ag}(A)\). More generally, if one works with resource algebras instead of Iris cameras, the underlying types are simplified, the multiplication operation is more transparent, and the results enjoy universal properties.
Fortunately, most of the payoff of our investigation of resource algebras is contained in Theorem 3; for formalization purposes, it is not necessary to have a well-behaved category of Iris cameras, even if one is useful for discovering and explaining particular examples. We therefore view Section 5 as evidence that future iterations of Iris and similar separation logics would benefit from using a (1) broader class of presheaves and (2) using PCSs over LPCSs.
7 Related Work
A great deal of effort has focused on the logical underpinnings of (concurrent) separation logics and our work fits into this tradition. The logical core of separation logic was developed under the name bunched implication logic [15, 23] and subsequently generalized by Biering et al. [2] to account for higher-order separation logics. The importance of partial commutative monoids in separation logic was apparent in these models and PCMs were subsequently featured prominently in concurrent separation logics [6, 9, 10, 16]. Early versions of Iris [19] also included partial commutative monoids, but later replaced them with cameras [17, 18, 20].
Directly related is the work by Bizjak and Birkedal [4] which analyzes the behavior of \(\Box \) modalities in terms of the core structures which induce them. They show that there is a bijection between \(\Box \) modalities and core structures in the non-step-indexed setting and a weaker correspondence in a constructive setting. We have used this as inspiration for our approach to uniquely define core as the operation inducing the largest possible \(\Box \) modality. They also elucidate the connection between \(\textbf{PSh}({\omega })\) and the model of Iris [18].
Also closely related is the work of Dardinier et al. [7]. In Appendix A of this work, the authors define a subclass of partial commutative monoids wherein each element a : M satisfies the additional property that \({\lbrace }b{\vert }b \le a \wedge b \cdot b = b{\rbrace }\) is finite and non-empty. They then observe that in such cases, there is a unique largest core operation on M which they then use in their separation logic. Interestingly, their motivation for introducing this property was not to obtain a better behaved category of PCMs, but rather to facilitate automation by ensuring resources could be decomposed into duplicable and non-duplicable components. their condition is less general than the MI axiom: it applies only to discrete resources and requires the conditions of Lemma 8. However, in the future we hope to explore further how the MI axiom and the work of Dardinier et al. [7] interact, in particular, whether the latter can be extended to a step-indexed setting in this manner.
Finally, we note that our observation that total presheaves can be limiting when extending the model of Iris was also noted by Spies et al. [26] who found several technical issues generalizing total presheaves to a transfinite setting.
8 Conclusion and Future Work
A key aspect of modern separation logics is how resources are modeled. In this paper we have introduced a novel notion of resource algebra, which differs in a subtle but crucial way from the camera definition used in Iris, by omitting the core operation and replacing it by a property, the maximal idempotent axiom. We have demonstrated that the new definition improves upon the earlier one in the sense that it induces a universal \(\Box \) modality and a well-behaved category RA of resource algebras. Moreover, we have shown that many of the known resource algebra constructions from Iris can be adapted to our new definition of resource algebra and that they satisfy universal properties. Finally, we have also shown that all the Iris cameras satisfy the maximal idempotent axiom.
Future work includes extending the Coq implementation of Iris to use the full category of presheaves rather than just a subcategory thereof, and thence to adopt our notion of resource algebra to such an implementation.
Acknowledgments
This work was supported in part by a Villum Investigator grant (no. 25804), Center for Basic Research in Program Verification (CPV), from the VILLUM Foundation. This work was co-funded by the European Union (ERC, CHORDS, 101096090). Views and opinions expressed are however those of the authors only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Jung et al. [18], required an additional axiom to force \(\rhd \) to commute with \(*\). We have followed e.g. Spies et al. [26] and removed this requirement to allow for more models.
The reader may be surprised to see \(y : X(0)\) rather than \(X(n)\). To make this predicate monotone in n, we must require that it holds whenever \(y : X(m)\) for \(m \le n\) and it is therefore both necessary and sufficient to check when \(m = 0\).
