Motivation

Automatic verification of programs that manipulate pointers needs procedure specifications: preconditions saying which part of the heap a procedure touches and postconditions saying what it leaves behind. Writing them by hand does not scale to millions of lines of code. Calcagno, Distefano, O'Hearn and Yang (J. ACM 58(6), 2011) infer them compositionally with bi-abduction: when symbolic execution reaches a call whose precondition is not implied by the current state, it asks for the missing memory $M$ that would make it hold. This abduction question in separation logic,

$$\Delta * M \models H,$$

is the engine behind the Abductor tool and, later, Facebook Infer.

The question has many solutions ($M = \mathsf{false}$ is always one), so its quality matters. The paper defines an order $\precsim$ on solutions that prefers less memory and then logical strength, shows that a best solution always exists as a semantic object, and then asks whether it can be written down and computed in the language that the analysis actually manipulates: symbolic heaps. For the fragment whose only spatial predicate is points-to, it answers yes. That answer, Theorem 3.25, is the goal of this mission.

Setting

Values are natural numbers; $0$ is nil and the nonzero naturals are the locations. A heap $h$ is a finite partial map from locations to values; a stack $s$ assigns a value to every variable; a state is a pair $(s,h)$. Write $h = h_0 \uplus h_1$ when $h_0,h_1$ have disjoint domains and $h$ is their union. A predicate is an arbitrary set of states. On predicates:

• $s,h \models F * G$ iff $h = h_0 \uplus h_1$ with $s,h_0 \models F$ and $s,h_1 \models G$;
• $s,h \models F \mathbin{-\!\!*} G$ iff for every $h'$ disjoint from $h$ with $s,h' \models F$, we have $s,h \uplus h' \models G$;
• $\mathsf{emp}$ holds in the empty heap, $\mathsf{true}$ everywhere, and $\neg$, $\vee$, $\wedge$, $\exists X$, $\forall X$ are the Boolean and quantifier operations; $F \models G$ is inclusion.

Symbolic heaps of the Points-to Instantiation. Expressions $E$ are variables or natural-number constants. A pure formula $\Pi$ is a conjunction of $E = E'$ and $E \neq E'$. A spatial formula $\Sigma$ is a $*$-conjunction of points-to facts $E \mapsto E'$, possibly with $*\,\mathsf{true}$; here $s,h \models E \mapsto E'$ iff $[\![E]\!]s \neq 0$ and $h$ is the one-cell heap $[\,[\![E]\!]s \mapsto [\![E']\!]s\,]$. A symbolic heap is $H = \exists \vec X.\, \Pi \wedge \Sigma$, and a disjunction $D = H_1 \vee \dots \vee H_n$. In the abduction question (5), $\Delta * D \models H$, the left-hand side $\Delta = \Pi \wedge L_1 \mapsto R_1 * \dots * L_n \mapsto R_n$ is quantifier-free.

Orders. $M \le M'$ iff $M' \models M * \mathsf{true}$ (spatially smaller), and

$$M \precsim M' \iff (M \le M' \wedge M' \not\le M) \vee (M \le M' \wedge M' \le M \wedge M \models M').$$

$\min(F)$ keeps the states of $F$ no proper subheap of which (with the same stack) is in $F$. $\mathrm{Elsewhere}(F) = \neg(F \mathbin{-\!\!*} \mathsf{false})$ says that some separate heap satisfies $F$, and the compatible preorder is $D \le_c D' \iff (D \wedge \mathrm{Elsewhere}(\Delta)) \le (D' \wedge \mathrm{Elsewhere}(\Delta))$. Subtraction is $F - G = F \wedge \neg((\neg\mathsf{emp}) * G)$.

Formalization targets

Goal: Theorem 3.25

There is a single algorithm $f$ such that for every quantifier-free $\Delta$ and symbolic heap $H$ of the Points-to Instantiation, the disjunction $D = f(\Delta, H)$ satisfies

$$\Delta * D \models H \quad\text{and}\quad D \precsim M \ \text{ for every predicate } M \text{ with } \Delta * M \models H.$$

Both halves are part of the goal: the best solution is expressible as a disjunction of symbolic heaps, and it is computable.

Milestones, in the order the paper's argument uses them

1. Lemma 3.16. If $D$ is a minimal solution w.r.t. $\le_c$, then $\min(D \vee \neg\mathrm{Elsewhere}(\Delta))$ is the minimal solution w.r.t. $\precsim$.
2. Figure 2 derives solutions (§3.4.2). If $\Delta * [D] \triangleright H$ is derivable, then $\Delta * D \models H$.
3. Lemma 3.18. For all $\Delta, H$ some $D$ with $\Delta * [D] \triangleright H$ is derivable, and the proof search terminates.
4. Lemma 3.19. If $\Delta * [D] \triangleright H$ is derivable and $\Delta * F \models H$, then $D \le_c F$.
5. Lemma 3.20. $\mathrm{Incompat}(\Delta)$ and $\neg\mathrm{Elsewhere}(\Delta)$ are semantically equivalent.
6. Lemma 3.23. Six algebraic properties of subtraction, including $\min(F_1 \vee \dots \vee F_n) = G_1 \vee \dots \vee G_n$ with $G_i = ((F_i - F_1)\cdots - F_n)$.
7. Quantifier removal for pure formulae (§3.4.4). $\exists X.\Pi$ is equivalent to a computable pure formula without $X$.
8. Subtraction with quantifiers (§3.4.4). $(\exists\vec X.\Delta) - (\exists\vec Y.\Delta')$ is a computable disjunction of symbolic heaps.

Significance

The result. Semantically the best solution is $\min(\Delta \mathbin{-\!\!*} H)$ (Theorem 3.13 of the paper), a formula that nests $-\!\!*$ and negation around $*$, which no automatic separation-logic prover handles and which says nothing directly about the shape of the missing memory. Theorem 3.25 shows that in the points-to fragment this object collapses to a finite disjunction of symbolic heaps, the format in which an analysis draws "pictures of memory", and that it can be computed. It gives an optimal abduction procedure against which the paper's heuristic procedure can be measured.

Formalizing it. The theorem is proved in the paper, but several steps are given as sketches ("the proof of each of these properties is straightforward", "a straightforward exercise"), Lemma 3.18 has only a proof sketch, and the quantifier-free subtraction display on p. 33 is incomplete as printed (it inspects only the points-to facts and not the pure part of the subtracted heap). A machine-checked development would supply the missing arguments, fix the subtraction step, and give a verified reference implementation of optimal abduction for points-to symbolic heaps. No part of it is known to have been formalized.

Difficulty

The obvious route is to compute $\min(\Delta \mathbin{-\!\!*} H)$ directly, but $-\!\!*$ quantifies over all heaps, and symbolic heaps have no syntax for it. The paper splits the problem into three phases (a $\le_c$-minimal solution from a proof system, the incompatible solutions, and $\min$), and each phase carries its own difficulty. The proof system's minimality (Lemma 3.19) must hold against arbitrary semantic predicates, not only symbolic heaps, and it fails as soon as $\Delta$ may denote more than one heap for a given stack (the paper notes that adding list segments breaks it). Computing $\min$ needs subtraction of symbolic heaps with quantifiers, which in turn needs quantifier elimination for Boolean combinations of equalities over an infinite domain, and the paper's quantifier-free subtraction step has to be repaired. Showing that the final disjunction is $\precsim$-least, not merely a solution, needs all three phases.

Formalization scope

All statements live in the namespace BiAbduction.Systematic. Values are ℕ with nil 0, locations are the nonzero naturals, variables are ℕ (program and logical variables form one sort), and heaps are maps ℕ → Option ℕ with 0 unallocated and finite domain. Finiteness of heaps is essential, since $\min$ relies on well-foundedness of the subheap order. Predicates are arbitrary Set (Stack × Heap). The syntax is built from ℕ, Bool, Sum, Prod and List by abbreviations, so "computed by an algorithm" is Mathlib's Computable₂ with the standard Primcodable encodings. The left-hand side $\Delta$ has no true conjunct, as in the paper's proofs; the right-hand side may have one. Figure 2 is an inductive relation in which psto may match any right-hand points-to fact. The soundness and $\le_c$-minimality statements assume the paper's bound-variable convention (no variable bound in $H$ occurs in $\Delta$); the goal does not need it.

The goal cannot be met by a degenerate reading. The competitors $M$ range over all predicates, not only over disjunctions, and computability refers to fixed standard encodings. The points-to semantics excludes nil addresses, and heaps are finite.

A complete development needs the separation-logic algebra of predicates (associativity and commutativity of $*$, the adjunction between $*$ and $-\!\!*$), properties of $\min$ under finite heaps, the soundness and minimality of the proof system, quantifier elimination for equality logic, and a computability argument for list-manipulating procedures. The semantic layer and the quantifier-elimination result are reusable beyond this mission. Contributions to any milestone, and to the supporting lemmas of §3.3 (Lemmas 3.10–3.11, Theorem 3.13), are welcome.

Theorem numbers and page references are those of the accepted manuscript of the J. ACM article (72 pages), not of the typeset journal version.

Selected references

• C. Calcagno, D. Distefano, P. W. O'Hearn, H. Yang, Compositional Shape Analysis by means of Bi-Abduction, Journal of the ACM 58(6), Article 26, 2011. https://doi.org/10.1145/2049697.2049700
• C. Calcagno, D. Distefano, P. W. O'Hearn, H. Yang, Compositional Shape Analysis by means of Bi-Abduction, POPL 2009. https://doi.org/10.1145/1480881.1480917
• J. Berdine, C. Calcagno, P. W. O'Hearn, Symbolic Execution with Separation Logic, APLAS 2005. https://doi.org/10.1007/11575467_5
• J. C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, LICS 2002. https://doi.org/10.1109/LICS.2002.1029817
• D. Pym, P. W. O'Hearn, H. Yang, Possible Worlds and Resources: The Semantics of BI, Theoretical Computer Science 315(1), 2004. https://doi.org/10.1016/j.tcs.2003.11.020

Motivation

Automatic program analyses for heap-manipulating code have to infer, for each procedure, a precondition describing the memory the procedure needs. Calcagno, Distefano, O'Hearn and Yang (J. ACM 2011) do this with bi-abduction: at a call site the analysis asks for an anti-frame $M$, the missing memory, and a frame, the memory left untouched, so that the current state together with $M$ meets the callee's precondition. Their tool, Abductor, and its successor Infer, derive specifications compositionally, procedure by procedure, without a whole program.

A natural question is what the inferred preconditions mean. The paper's informal answer is that the analysis aims at footprints: descriptions of the cells a program actually uses. §4.2.4 makes this precise for straight-line sequences of actions: if each precondition is precise and the prover always returns the best anti-frame, the inferred precondition is exactly the footprint. That result rests on the semantic theory of best abductive solutions developed in §3.3: with respect to a natural order, the abduction question $F * M \models G$ has a unique best solution, $\min(F \mathbin{-\!\!*} G)$.

Setting

A heap is a finite partial map from locations to values; a stack maps variables to values; a state is a stack–heap pair $(s,h)$. A predicate is an arbitrary set of states. Write $h = h_0 \uplus h_1$ when $h_0, h_1$ have disjoint domains and $h$ is their union, and $h' \subseteq h$ for a subheap. The separating conjunction $F * G$ holds of $(s,h)$ when $h = h_0 \uplus h_1$ with $(s,h_0) \in F$ and $(s,h_1) \in G$; $\mathsf{true}$ is the set of all states; the separating implication $F \mathbin{-\!\!*} G$ holds of $(s,h)$ when every disjoint $h'$ with $(s,h') \in F$ gives $(s, h \uplus h') \in G$. Entailment $F \models G$ is inclusion.

A solution of the abduction question $F * M \models G$ is any predicate $M$ with $F * M \models G$. Solutions are compared by the spatial preorder and the betterness order

$$M \le M' \iff M' \models M * \mathsf{true}, \qquad M \precsim M' \iff (M \le M' \wedge M' \not\le M) \vee (M \le M' \wedge M' \le M \wedge M \models M').$$

The minimal states of $F$ are $\min(F)$: the states $(s,h) \in F$ such that no proper subheap $h' \subsetneq h$ has $(s,h') \in F$.

An action $\alpha$ is given by its specification $\{P_\alpha\}\,\alpha\,\{Q_\alpha\}$, a pair of predicates. A predicate $P$ is precise if every $(s,h)$ has at most one subheap $h_f \subseteq h$ with $(s,h_f) \in P$. For a nonempty sequence of actions, the safe states and the footprint are

$$\mathrm{safe}(\alpha) = P_\alpha * \mathsf{true},\quad \mathrm{safe}(\alpha;C) = P_\alpha * \big(Q_\alpha \mathbin{-\!\!*} \mathrm{safe}(C)\big),\quad \mathrm{foot}(C) = \min(\mathrm{safe}(C)).$$

The canonical precondition $P_C$ of a sequence, as computed by an ideal bi-abductive prover, is $P_\alpha$ for a single action and $P_\alpha * M$ for $\alpha; C$, where $M$ is the best solution of $Q_\alpha * M \models P_C * \mathsf{true}$.

Formalization targets

Goal: Theorem 4.11 (Deriving Footprint)

If every precondition $P_\beta$ of the sequence is precise and every anti-frame is a $\precsim$-best solution, then

$$\mathrm{foot}(C) = P_C .$$

Milestones

1. Lemma 3.10. $\le$ is a preorder; $M \le \min(M)$ and $\min(M) \le M$; and $M, M'$ are $\le$-equivalent iff $\min(M) = \min(M')$.
2. Lemma 3.11. $\precsim$ is a partial order, and $M' \le M$ implies $\min(M') \precsim M$.
3. Lemma 3.12. $F \mathbin{-\!\!*} G$ is a $\le$-least solution of $F * M \models G$; equivalently $F * M \models G \iff M \models F \mathbin{-\!\!*} G$.
4. Theorem 3.13. The $\precsim$-least solution exists, is unique, and equals $\min(F \mathbin{-\!\!*} G)$.
5. Proof of Theorem 4.11, safe states. $\mathrm{safe}(C) = \mathrm{foot}(C) * \mathsf{true}$ for every sequence.
6. Proof of Theorem 4.11, precision. If $P$ is precise, $\min(P * X) = \min(P) * \min(X)$ for every $X$, and $\min(P) = P$.

Significance

Theorem 3.13 gives the abduction question a canonical semantic answer, and it is the yardstick for every algorithm in the paper: the heuristic procedure of §3.2 is shown not to reach it, and the systematic procedure of §3.4 is proved to compute it on a restricted fragment. Theorem 4.11 connects this semantic optimum to program analysis: on straight-line paths, bi-abduction with an ideal prover infers neither more nor less memory than the program touches. It is the paper's theoretical justification for aiming the analysis at footprints.

Neither result has a machine-checked proof that this mission knows of; the platform has no separation-logic layer at all. The mission produces a self-contained semantic layer for separation logic over a concrete heap model (finite heaps, $*$, $\mathbin{-\!\!*}$, $\min$, the orders $\le$ and $\precsim$, precise predicates) that the companion mission on the systematic abduction algorithm, and later work on frame inference or footprint analysis, can share. The paper proves both results; the work here is to formalize those proofs.

Difficulty

Most steps are short once the definitions are fixed, and the paper states several of them as "immediate". Two points are not. First, $\min(M) \le M$ and the "if" direction of Lemma 3.10(3) need every state of $M$ to lie above a minimal one; this holds because heaps are finite, so the subheap order is well founded, and fails for infinite heaps. Second, the inductive step of Theorem 4.11 passes through $\mathrm{safe}(C) = P_C * \mathsf{true}$ and through distributing $\min$ over a precise $*$-factor. Precision of $P_\alpha$ is what forces the split of a minimal heap of $P_\alpha * X$ to be unique; without it, the two sides of the displayed chain on p. 50 differ. The induction must carry precision for every action of the tail.

Formalization scope

Lean represents values and variables as natural numbers, with $0$ as nil and the nonzero naturals as locations; a heap is a cell map ℕ → Option ℕ with cell 0 = none and finite domain; disjoint union is a relation. Predicates are Set (Stack × Heap), entailment is ⊆, and $\mathsf{true}$ is Set.univ. Program and logical variables are not distinguished, and actions carry no parameters, as in §4.2.4; the stack is the same on both sides of every connective. "The minimal solution w.r.t. $\precsim$" is the $\precsim$-least solution, competing against every predicate, not only symbolic heaps. A sequence of actions is a head action plus a tail list, so the empty sequence never occurs. Theorem numbers and pages are those of the accepted manuscript of the J. ACM article (pp. 1–72, footer "Journal of the ACM, Vol. V, No. N, May 2011"), not of the typeset Article 26.

The paper does not define "the canonical spec" in §4.2.4. The formalization reads it from the proof of Theorem 4.11, as an inductive relation whose anti-frames are arbitrary $\precsim$-least solutions. Defining the anti-frame as $\min(Q_\alpha \mathbin{-\!\!*} (P_C * \mathsf{true}))$ would build Theorem 3.13 into the definition, and dropping precision, allowing infinite heaps or restricting the competitors in the definition of a best solution would change the theorem; all of these are ruled out.

Needed infrastructure: the heap model with union and subheap lemmas, well-foundedness of strict subheap inclusion on finite heaps, the adjunction between $*$ and $\mathbin{-\!\!*}$, and upward closure of $\mathrm{safe}(C)$. Reusable pieces, such as the heap model, the adjunction and the properties of $\min$, are welcome as separate lemmas.

Selected references

• C. Calcagno, D. Distefano, P. W. O'Hearn, H. Yang, Compositional Shape Analysis by means of Bi-Abduction, Journal of the ACM 58(6), 2011. https://doi.org/10.1145/2049697.2049700
• C. Calcagno, D. Distefano, P. W. O'Hearn, H. Yang, Compositional Shape Analysis by means of Bi-Abduction, POPL 2009. https://doi.org/10.1145/1480881.1480917
• C. Calcagno, P. W. O'Hearn, H. Yang, Local Action and Abstract Separation Logic, LICS 2007. https://doi.org/10.1109/LICS.2007.30
• D. Pym, P. W. O'Hearn, H. Yang, Possible Worlds and Resources: The Semantics of BI, Theoretical Computer Science 315(1), 2004. https://doi.org/10.1016/j.tcs.2003.11.020
• J. C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, LICS 2002. https://doi.org/10.1109/LICS.2002.1029817

Motivation

Distributed programs often establish a conversation among several participants, then exchange messages without waiting for each send to be received. A specification of each participant in isolation does not by itself say whether their actions will fit together. Multiparty asynchronous session types address this by describing the intended conversation once as a global type and checking each participant against a projected local type. Honda, Yoshida and Carbone develop this calculus and state a progress result for a restricted class of well-typed programs: if execution has not finished, another reduction is available. The restriction matters because independently initiated sessions can interfere and deadlock even when their communications are individually typed. Honda, Yoshida and Carbone (2016)

Setting

A program is a process before execution: it contains no message queues or restricted session channels, even after structural rearrangement, and it has no free session channels or process variables. A requester on a shared name $a$ starts a session with participants numbered $2$ through $n$. Each participant receives the same vector $\widetilde s$ of fresh session channels. An asynchronous send appends a message to the appropriate FIFO queue; a receive reads the queue head. Requests, sends, delegations and selections are emitting prefixes. Accepts, receives and branches are receiving prefixes. The reduction relation $P\longrightarrow Q$ includes these communications, conditionals, guarded declaration unfolding, and closure under parallel composition, restriction and structural congruence $\equiv$. Honda, Yoshida and Carbone (2016), Figs. 1–3 and Def. 2.1

A global type $G$ specifies which numbered role sends a value or choice to another role on channel index $k$, followed by the remainder of the conversation. It may also contain parallel components and guarded recursion. A partial projection $G\upharpoonright p$ gives role $p$ its endpoint type. Global types must be linear: causally ordered actions on a common channel have both input and output dependency chains. A global type is coherent when it is linear and projects to all its participants; the runtime typing $\Delta$ is coherent when each session family comes from such a global type. Honda, Yoshida and Carbone (2016), Defs. 3.12, 4.1–4.2 and 5.9

The runtime judgement $\Gamma\vdash P\triangleright_{\widetilde s}\Delta$ records the types of the process and the queue channels it mentions. Type contexts remember messages already in transit and compose with endpoint types. A process is queue-full when the channels in $\widetilde s$ equal the channels occurring in $\Delta$. A prefix is active when it is outside another prefix and outside either branch of a conditional, after permitted declaration unfolding. A process is well-linked when every reachable process has each active shared-name prefix in a redex. A process is simple when it has a typing derivation whose session environments obey the singleton and emptiness restrictions of Definition 5.25, with no delegation input or output rule. Honda, Yoshida and Carbone (2016), pp. 28–37

Formalization targets

The goal is Corollary 5.30. For every simple, well-linked program $P$ whose free names have shared sorts, and every reachable process $P'$,

$$P\longrightarrow^*P'\quad\Longrightarrow\quad P'\equiv 0\ \lor\ \exists P''\;P'\longrightarrow P''.$$

Here $0$ is inaction, and $P'\equiv 0$ includes completed sessions whose empty queues disappear by structural congruence. The milestones are the closed-typing preservation clause of Theorem 5.19(3), the linearity and message agreement clauses of Theorem 5.22, and the immediate-step claim of Proposition 5.29(1). Those are statements of the paper and give separate targets before the progress corollary. Honda, Yoshida and Carbone (2016), pp. 34–37

Significance

For the specified class of programs, progress excludes a reachable state that is neither finished nor reducible. It combines static endpoint information with the operational facts about queues and shared-name synchronisation. The communication-safety milestone also states that a value receive is paired with a value message of matching arity, channel reception with a channel vector of matching length, and branching with an offered label. These claims describe behavior of the paper's asynchronous multiparty calculus, rather than a property of a particular implementation. Honda, Yoshida and Carbone (2016), Theorem 5.22 and Corollary 5.30

The paper supplies mathematical proofs, but this mission's statements have no completed machine-checked proofs. Formalizing the result requires a precise account of the calculus, including queue messages, scope, recursive calls, type contexts, projection and the limited form of simplicity. The definitions can support later work on subject reduction and session fidelity in the same model. A contribution may prove any milestone or the goal, or improve the shared definitions while preserving the source's hypotheses and conclusions.

Difficulty

Typing each participant does not immediately give a reduction of their parallel composition. A send can be present while a receive is blocked by an earlier queue message, and a session initiation can be blocked by a shared-name prefix in a different session. Communication safety must relate active prefixes to a unique queue and its actual head message. Progress additionally needs the restrictions on derivations and shared-name links to rule out interference among sessions. The rules for structural congruence and declaration unfolding make the location of a redex depend on more than the outer syntactic constructor. Honda, Yoshida and Carbone (2016), §§5.4–5.5

Formalization scope

Lean uses natural numbers for role identifiers, shared names, channels, labels and process variables. Channel indices are one based, following $s[1..m]$. A global type, value sort and endpoint type are separate syntax classes; finite branch families are lists with nonempty, distinct labels where a well-formed type is required. Recursion is read equi-recursively by an endpoint bisimulation, and global-type linearity is checked on every finite unfolding. Projection returns an optional endpoint type so undefined projections cannot acquire a default value. The session typings are finite maps represented by association lists, with distinct roles and disjoint channel domains. The judgement's subscript $\widetilde s$ lists queue channels, while the domain of $\Delta$ lists all sessions under typing.

The formalization uses named process binders and a structural-congruence relation containing alpha conversion. Received-value and call substitution is capture avoiding under explicit freshness conditions. Expression evaluation is fixed to the ordinary Boolean connectives used in the paper's typing rules. Runtime typing includes the queue rules and the partial composition of type contexts. The restricted typing system for simplicity retains runtime queue rules and excludes both delegation directions. The paper prints “[RCV]” in Definition 5.25(2), but its appendix explicitly excludes “[SREC]”; this draft follows the appendix and records that reading in its audit notes. The result quantifies over actual programs and makes simplicity imply typability, so a free, blocked input or an untyped syntax check cannot satisfy the goal. Honda, Yoshida and Carbone (2016), Def. 5.25 and Appendix B.8

Every prefix rule acts on a singleton entry $\widetilde s:T@p$ (Notation 4.5); process-variable signatures carry one singleton entry per session vector, as in [VAR]; [SREC] receives the channel names it binds, without substitution (Remark 2.2). Proposition 5.29(1) and Corollary 5.30 are false as printed for open terms: a free name of sort bool used as a conditional guard, or a free process variable, is a stuck simple process. The formal statements therefore add that the free names of the process have shared sorts and, for Proposition 5.29(1), that it has no free process variables (a program has none by definition).

The development needs Mathlib's finite sets, lists and reflexive-transitive closure, plus its own definitions of the process calculus and typing judgements. The Lean declarations in this proposal are draft statements and definitions for review; they are not proofs of the paper's results.

Selected references

• Kohei Honda, Nobuko Yoshida and Marco Carbone, Multiparty Asynchronous Session Types, Journal of the ACM 63(1), Article 9, 2016. DOI 10.1145/2827695

Motivation

Multiparty communication protocols involve several participants who send messages over shared session channels. An implementation may send a later message before an earlier one has been received, so a written sequence of interactions does not by itself prevent a receiver from taking the wrong message. Honda, Yoshida, and Carbone use global types to specify the whole conversation and a linearity condition to rule out conflicting uses of a channel. Their condition is part of the type system that supports subject reduction and session fidelity in the same paper. Honda, Yoshida, and Carbone, 2016

Global types can contain recursion. Reading their full behaviour as a regular tree may therefore involve infinitely many copies of the same interaction. Proposition 3.13(1) says that checking just one finite unfolding suffices to determine whether every later finite unfolding satisfies the paper's linearity condition. This mission formalizes that proposition and the definitions on which its statement depends. Honda, Yoshida, and Carbone, 2016, §3.5 and Appendix A

Setting

A global type $G$ describes actions among roles $p,q$ on channels identified by positive indices $k$. Its constructors are a value communication $p\to q:k\langle U\rangle.G'$, a labelled branch $p\to q:k\{\ell_j:G_j\}_{j\in J}$, parallel composition $G_1\mid G_2$, recursion $\mu t.G'$, a recursion variable $t$, and termination $\mathrm{end}$. The carried value type $U$ may contain shared names whose sorts include another global type, or it may be a located end-point type. The formal syntax represents end-point sends, receives, selections, branches, recursion, variables, and termination because shared global types can occur within the sorts carried by those types. Honda, Yoshida, and Carbone, 2016, Figs. 4 and 6

An action node is an occurrence of a communication or branching action in the tree of a finite unfolding. Each node has a sender, receiver, and channel index. The action order $n_1\prec n_2$ holds when one action lies before another in the same continuation or branch, according to Definition 3.7. Actions in different branches or parallel components have no order solely because they appear next to each other in the syntax. Honda, Yoshida, and Carbone, 2016, pp. 15–16

The paper refines that order into three dependency relations. An II step matches receivers; an IO step connects a receiver to a later sender; and an OO step matches both sender and channel. An input dependency is a chain of IO steps ending in II. An output dependency is a nonempty chain of OO or IO steps. A finite type is linear when every ordered pair of actions on the same channel has both dependencies, including the corresponding condition on the global types carried within its values. The last II step matters because a chain ending at an output has not checked the ordering of the final input. Honda, Yoshida, and Carbone, 2016, Defs. 3.11–3.12

Write $G^{(n)}$ for the finite result of unfolding every recursion in $G$ $n$ times and replacing remaining recursion variables by $\mathrm{end}$. For a single recursion $G=\mu t.H$, the paper gives $G^{(0)}=H[\mathrm{end}/t]$ and $G^{(n+1)}=H[G^{(n)}/t]$. Unfolding does not enter carried types. The one-time unfolding is $G^{(1)}$. Honda, Yoshida, and Carbone, 2016, p. 20 and Notation A.1

Formalization targets

The milestone is the direction the paper calls the “if-direction”: for a well-formed global type and a positive unfolding index, linearity at that index implies linearity at the first one.

$$\operatorname{WellFormed}(G)\ \land\ n\ge 1\ \land\ \operatorname{Linear}(G^{(n)}) \quad\Longrightarrow\quad \operatorname{Linear}(G^{(1)}).$$

The mission goal is Proposition 3.13(1), the equivalence between the first unfolding and any positive unfolding.

$$\forall G\text{ well formed}\,\forall n\ge 1,\qquad \operatorname{Linear}(G^{(1)}) \quad\Longleftrightarrow\quad \operatorname{Linear}(G^{(n)}).$$

The lower bound $n\ge1$ is essential. The paper explicitly begins its Appendix A induction at $n=1$ and gives examples that satisfy linearity at the zeroth unfolding but fail after one unfolding. Proposition 3.13(2), the paper's decidability claim, is outside this mission: formalizing computational decidability would require an effective representation and decision procedure rather than a classical Decidable instance. Honda, Yoshida, and Carbone, 2016, p. 20 and Appendix A

Significance

The proposition turns a property stated over arbitrarily deep recursive behaviour into a fixed finite test. It supports the paper's decidability result and supplies the channel-ordering premise used later in coherent global types and runtime typing. Without the stabilization claim, checking a recursive global type by inspecting one finite copy would leave later channel conflicts unresolved. Honda, Yoshida, and Carbone, 2016, Props. 3.13–3.14 and Def. 4.2

The result is already proved in the paper. The formalization work is to give the paper's finite unfolding, action order, dependency chains, and recursive carried-type condition exact Lean meanings, then verify the equivalence against those meanings. The local mission currently contains open theorem statements and compiled definitions; it does not claim a machine-checked proof of Proposition 3.13(1). Those definitions can also be reused when formalizing the paper's coherence and subject-reduction results.

Difficulty

The main obstacle is the interaction between recursion and causality. Unfolding creates further occurrences of actions, while an input dependency requires a chain with a specific final II edge and an output dependency allows only OO or IO edges. The action order also depends on a node's place in a branch, continuation, or parallel component. Merely comparing channel labels across two unfoldings does not establish the required dependencies. The carried-type condition adds another level: unfolding the outer type leaves its carried types intact, but their own linearity must still be checked. Honda, Yoshida, and Carbone, 2016, Defs. 3.7, 3.11–3.12 and Appendix A

Formalization scope

Lean represents roles, labels, type variables, and channel indices by natural numbers, with channel indices interpreted as one-based. Branches are lists; WellFormed G records nonempty branches with distinct labels, closed guarded recursion, positive channel indices, and distinct sender and receiver, also checking carried global types. Both theorem statements assume it to make the paper's standing syntax conventions explicit. The sort grammar includes Boolean and natural-number sorts, shared-name sorts, and coded additional base sorts for the paper's ellipsis. The recursion constructor is named mu and the sort type SType because rec and Sort have special meanings in Lean.

Node names are finite child-index paths. Prec is the transitive closure of the five clauses of Definition 3.7. Every II, IO, or OO step includes this order. Input dependency requires at least one step, resolving the printed $n\ge0$ against the same sentence's mandatory final II step. Carried types are reached through value and end-point type syntax, and nested carriers are included transitively. Linear checks each such carried type at every finite unfolding. The definitions also encode the paper's positive-index and non-reflexive interaction conventions in WellFormed. A linearity predicate that ignores carried types or treats separate parallel components as ordered would change the target theorem. Honda, Yoshida, and Carbone, 2016, pp. 12–13, 16, 19–20

Useful contributions include results about finite unfolding and the action order, preservation of labels at recurring positions, and dependency-chain properties under unfolding. The two folding claims in Appendix A are not listed as milestones here because a faithful folding operation for nested recursion and multiple occurrences has not yet been specified. Their absence is a scope limit on the attack path, not an assumption in the goal.

Selected references

• Kohei Honda, Nobuko Yoshida, and Marco Carbone, Multiparty Asynchronous Session Types, Journal of the ACM 63(1), Article 9, 2016. DOI: 10.1145/2827695.

Motivation

Runtime monitoring checks a running system against a specification by inspecting its trace of events as it is produced. Policies on data, such as "every published report was approved within the last 10 days" or "each value stored in in reaches out within 5 time units", quantify over data values and constrain the time between events. Metric first-order temporal logic (MFOTL) expresses such policies: it extends first-order logic with past and future temporal operators that carry intervals of allowed time differences.

Basin, Klaedtke, Müller and Zălinescu (J. ACM 62(2), Article 15, 2015) give a monitor for MFOTL properties $\square\Phi$ with $\Phi$ bounded. It allows negation and quantification over the infinite domain $\mathbb N$ without restriction, because every relation it manipulates is represented by a finite automaton: the input structures are automatic structures. The paper implements it in the prototype tool MonPoly-Reg (§6). Its correctness rests on Theorem 3.9: the monitor reports exactly the violations of $\Phi$, at every time point.

Setting

A signature $S=(C,R,\iota)$ has finitely many constants and predicates with arities. Formulas are built from $t\approx t'$ and $r(t_1,\dots,t_{\iota(r)})$ by $\neg$, $\vee$, $\exists x$ and the temporal operators $\bullet_I$ (previous), $\circ_I$ (next), $\mathsf S_I$ (since) and $\mathsf U_I$ (until), where $I=[b,b')$ is a nonempty interval of $\mathbb N$ with $b'\in\mathbb N\cup\{\infty\}$. A formula is bounded if every $\mathsf U_I$ in it has $b'<\infty$.

A temporal structure $(\bar{\mathcal D},\bar\tau)$ assigns to each time point $i\in\mathbb N$ relations $r^{\mathcal D_i}\subseteq\mathbb N^{\iota(r)}$ and a time stamp $\tau_i\in\mathbb N$; constants are rigid, $\tau_0\le\tau_1\le\cdots$, and $\bar\tau$ exceeds every bound. Satisfaction $(\bar{\mathcal D},\bar\tau,v,i)\models\varphi$ is Definition 2.2; for example $\psi\,\mathsf U_I\,\psi'$ holds at $i$ if $\psi'$ holds at some $j\ge i$ with $\tau_j-\tau_i\in I$ and $\psi$ holds at all $k\in[i,j)$. For $\varphi$ with free variables $x_1<\dots<x_n$, the satisfying set is

$$\varphi^{(\bar{\mathcal D},\bar\tau,i)}=\{\bar d\in\mathbb N^n\mid(\bar{\mathcal D},\bar\tau,v[\bar x\mapsto\bar d],i)\models\varphi\ \text{for some }v\}.$$

A domain representation is a regular language $\mathcal L$ over a finite alphabet with a surjection $\nu:\mathcal L\to\mathbb N$ whose equality relation is regular. A relation $A\subseteq\mathbb N^k$ is regular if the words $u_1\otimes\cdots\otimes u_k$ (the letter-by-letter convolution, padded with $\#$) with $(\nu(u_1),\dots,\nu(u_k))\in A$ form a regular language.

The monitor $\mathsf M_\Phi$ (Fig. 2) reads $(\mathcal D_0,\tau_0),(\mathcal D_1,\tau_1),\dots$ one element per loop iteration. It extends each $\mathcal D_j$ to $\hat{\mathcal D}_j$ with auxiliary relations $p_\alpha$ (and $r_\alpha$, $s_\alpha$ for since and until) for every temporal subformula $\alpha$, built incrementally by the constructions of §3.4 once a list $Q$ of pending triples $(\alpha,j,S)$ says that enough of the future has been read. When $\hat{\mathcal D}_i$ is complete it outputs the set $(\neg\hat\Phi)^{\hat{\mathcal D}_i}$ with $\tau_i$, where $\hat\Phi$ is $\Phi$ with each top-level temporal subformula $\alpha$ replaced by the atom $p_\alpha(\bar x)$.

Formalization targets

Goal: Theorem 3.9

For every input satisfying the restrictions of §3.1 and every bounded $\Phi$:

$$\text{(i)}\quad (n,O,t)\ \text{output by line 9}\ \Longrightarrow\ O=(\neg\Phi)^{(\bar{\mathcal D},\bar\tau,n)},\ O\ \text{regular},\ t=\tau_n;$$ $$\text{(ii)}\quad \forall n\in\mathbb N,\quad n=0\ \text{or some output at index }n-1\text{ occurs},$$

where each output is followed by line 11 setting $i$ to the next index. This records counter values reached inside the while loop, including values that may never appear at a loop entry. Part (ii) excludes the vacuous reading of (i).

Milestones

1. Lemma 3.4: $\hat\varphi^{\hat{\mathcal D}_i}=\varphi^{(\bar{\mathcal D},\bar\tau,i)}$ once the auxiliary relations of $\mathit{tsub}(\varphi)$ are correct, and regularity is preserved.
2. Lemmas 3.5–3.8: the constructions for $\bullet_I$, $\circ_I$, $\mathsf S_I$ and bounded $\mathsf U_I$ produce regular relations equal to the satisfying sets, with the stated characterizations of $r_\alpha$ and $s_\alpha$.
3. Observations (1)–(3) of the proof of Theorem 3.9 on the list $Q$ and the counter $i$.
4. The claim that line 7 can always be executed, in the form: if $(\alpha,j,\emptyset)\in Q_k$ then the build stores $p_\alpha^{\hat{\mathcal D}_j}=\alpha^{(\bar{\mathcal D},\bar\tau,j)}$, which is regular.

Significance

Theorem 3.9 makes $\mathsf M_\Phi$ a sound and complete monitor for the safety fragment $\square\Phi$, $\Phi$ bounded: every violation at every time point is reported, nothing else is, and every output is a finitely represented (regular) set even though it may be infinite. It covers unrestricted negation and quantification, which finite-relation monitors (§4 of the paper) cannot handle. The incremental constructions of §3.4 are the template reused by later MFOTL monitors.

The paper gives a mathematical proof of its monitor's correctness. This mission asks for a Lean proof that checks the MFOTL semantics, automatic relations over $\mathbb N$, and the correctness of this particular monitor, including the until construction whose printed version is defective (see Formalization scope).

Difficulty

Two parts are hard. The regularity claims need the fundamental property of automatic structures: first-order definable relations are regular, which requires closure of padded convolution languages under Boolean operations, cylindrification, permutation of tracks and projection, the last with removal of trailing padding. The arithmetic constraints of the since and until constructions additionally need successor and offset relations definable from $\prec$.

The scheduling argument is the other part. Correctness of a build at $(\alpha,j)$ requires that every input relation, at time points up to $j+\ell_j$ for until, was built before and not discarded since. Following only the syntax of $\alpha$ does not settle this: a needed relation for a subformula at a later time point may be built in the same iteration as $\alpha$'s.

Formalization scope

The domain is $\mathbb N$, as §3.1 assumes. Relations are sets of lists of natural numbers, ordered by the sorted free variables. Interval upper bounds are in $\mathbb N_\infty$; intervals carry the proof that they are nonempty. The representation $(\mathcal L,\nu)$ is a single parameter shared by the hypothesis "every $r^{\mathcal D_i}$ is regular" and the regularity claims of the conclusions; it is never chosen existentially. The binary predicate $\prec$ interpreted as $<$ is a hypothesis.

Two hypotheses on $\Phi$ besides boundedness are the paper's own "without loss of generality" assumptions: each temporal subformula occurs once in $\Phi$ (§3.6), and the direct subformulas of each $\mathsf S_I$, $\mathsf U_I$ subformula have the same free variables (§3.4; achieved by padding with $x\approx x$, as in §3.5). No other restriction is placed on $\Phi$.

The printed until construction (§3.4.4) is repaired: the guard of $U_r$ is "$\bar a\in\hat\beta^{\hat{\mathcal D}_{i+k}}$ for all $\ell_{i-1}\le k\le\ell_i$", since the printed guard empties $r_\alpha$ in the paper's own example of §3.5; $U_s$ keeps only tuples with $j'\ge1$, since otherwise a $\gamma$-witness at time point $i-1$ survives to time point $i$ when $\tau_i=\tau_{i-1}$; and time-stamp equations are encoded additively. Lemma 3.8(i) reads $\bar a\in\mathbb N^n$ and adds $j\le\ell_i$. "Effectively computable" in Theorem 3.9(i) is not formalized. Part (ii) uses the output at index $n-1$ as the record of the line-11 increment to $n$; for $n=0$, the counter is initialized by line 2. Loop-entry states alone can skip counter values reached within one iteration.

The monitor is a state machine whose builds and outputs are computed only from its store of relations; it never consults the satisfaction relation or satisfying sets. A formalization in which line 7 reads the semantics would turn Theorem 3.9(i) into a restatement of Lemma 3.4, and is ruled out. A build whose input is missing stores nothing, so a monitor that silently fails would violate (ii).

Contributions welcome: the theory of automatic relations (reusable beyond this mission), the semantic halves of Lemmas 3.4–3.8, and the scheduling invariants.

Selected references

• D. Basin, F. Klaedtke, S. Müller, E. Zălinescu, Monitoring metric first-order temporal properties, J. ACM 62(2), Article 15, 2015. https://doi.org/10.1145/2699444

Bound $L_4$: $33,070,982 \le R$

This mission formalizes the lower bound $33,070,982 \le R$ on the number of reversible binary cellular automata on the $3 \times 3$ Moore neighborhood. Extending the conserved-landscape marker families to both centered and off-centered rules.