Introduction

The Cook-Levin theorem states that CNF SAT is NP-complete. This mission formalizes the theorem over a multi-tape Turing machine model in Lean 4.

Main Goal

Prove CookLevin.cook_levin_theorem:

$$NPComplete SAT$$

under the decider and reduction hypotheses.

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

Processors in a distributed system may hold separate readings of a sensor, clock, or diagnostic result while some processors give misleading reports. The aim of interactive consistency is for every functioning processor to compute the same vector of reported values and to put each functioning processor's actual private value in its corresponding position. A shared vector can then be used for a common decision. Pease, Shostak, and Lamport formulated this problem for isolated processors communicating by two-party messages; their paper discusses clock synchronization, input stabilization, and diagnostic tests as concrete applications Pease–Shostak–Lamport 1980.

In the paper's oral-message model, faulty processors can invent reports about values they received from others. The other two missions in this series formalize the recursive majority procedure for $n\ge 3m+1$ and the matching impossibility result below that bound. Section 5 changes the communication assumption: a faulty processor may refuse to pass on a received value but cannot pass on an altered value as if it came from its original sender. Under that assumption, the authors give a procedure for every $n\ge m$, including configurations outside the oral-message threshold Pease–Shostak–Lamport 1980, §§3–5.

Setting

Let $P$ be a finite set of $n$ processors and $V$ a type of private values. Each processor $q\in P$ has a value $\sigma(q)\in V$. A scenario $\sigma$ records the values reported along chains of processors. A string $p_1p_2\cdots p_r$ is read from receiver to originator: $p_1$ receives a report ultimately attributed to $p_r$. A recorded value may be NIL, meaning that no authenticated value is available. The view available to receiver $p$ is its $p$-scenario, the restriction $w\mapsto\sigma(pw)$; it contains no report that begins with a different receiver.

Choose a set $N\subseteq P$ of nonfaulty processors. At most $m$ processors may be faulty, expressed as $|P|\le |N|+m$. An authenticated scenario consistent with $N$ obeys two conditions whenever the displayed strings are in the $(m+1)$-level scenario. If $p\in N$ and $q\in P$, the report made by nonfaulty relay $p$ is truthful: $\sigma(qpw)=\sigma(pw)$. For any prefix $w'$, a chain passing through nonfaulty $p$ carries either the value at $p$ or NIL: $\sigma(w'pw)\in\{\sigma(pw),\mathrm{NIL}\}$. The second condition allows omission by later relays while excluding a changed value falsely attributed to $p$ Pease–Shostak–Lamport 1980, p. 233.

For each receiver $p$ and originator $q$, the procedure forms $S_{pq}$, the set of all non-NIL values in $p$'s view on strings $pwq$. The intermediate string $w$ has at most $m$ distinct letters, all in $P\setminus\{p,q\}$. Receiver $p$ records the sole value in $S_{pq}$ when this set is a singleton; otherwise it records NIL. The resulting entries, one for each $q\in P$, form $p$'s proposed consistency vector Pease–Shostak–Lamport 1980, p. 233.

Formalization targets

The first milestone covers a nonfaulty originator $q$: every nonfaulty receiver $p$ sees exactly its true value. The second covers a faulty originator: the set of non-NIL values seen by one nonfaulty receiver is contained in the set seen by another. The same statement with the receivers exchanged gives equality of their sets.

The goal is the procedure's full interactive-consistency guarantee, for every choice of $N$ and every authenticated scenario satisfying the conditions above:

$$\begin{aligned} R_p(q)&=\sigma(q) &&(p,q\in N),\\ R_p(r)&=R_{p'}(r) &&(p,p'\in N,\ r\in P). \end{aligned}$$

Here $R_p(r)$ is the optional value recorded by processor $p$ for processor $r$. Both clauses matter: agreement alone could be achieved by always recording NIL, while correct nonfaulty entries alone would leave faulty entries inconsistent.

Significance

The result identifies an exact communication assumption under which the paper's $3m+1$ oral-message bound no longer governs the procedure. Even if a faulty originator gives conflicting values, nonfaulty receivers finish with identical entries for that originator; if an originator is nonfaulty, they retain its actual value. The paper describes authenticators as a practical approximation to the assumption, but the guarantee here is a mathematical statement about scenarios satisfying its two conditions, not a probability claim about a cryptographic implementation Pease–Shostak–Lamport 1980, §5.

Formalizing this result supplies precise interfaces for authenticated scenario consistency, local views, the set $S_{pq}$, and the recording rule. The paper proves the result on pp. 233–234; this mission asks for a machine-checked proof of those statements in Lean. The scenario and local-view definitions can support later formalizations of message-passing protocols with truthful or omissible relays. Contributions that establish the two source milestones and the final guarantee, or develop reusable list and finite-set facts needed by them, are within scope.

Difficulty

The case of a faulty originator is the central difficulty. Its private value has no required relationship to what different nonfaulty receivers hear, so simply asserting that every receiver obtains the same direct report is unjustified. A faulty relay may also omit a report, which makes equality of raw scenario entries too strong. The target must compare sets of non-NIL values obtained along admissible relay chains. At the longest allowed chain, the length bound prevents adding another relay, and the number of faulty processors is needed to establish that an admissible nonfaulty relay occurs in the chain Pease–Shostak–Lamport 1980, p. 234.

Formalization scope

Lean represents processors by a finite set P : Finset α, values by a type V, strings by List α, and NIL by none : Option V. A scenario is a total function from strings to optional values. Only strings over $P$ of length at most $m+2$ are constrained by authenticated consistency, matching the $(m+1)$-level scenario that the procedure reads. A single-letter string has a non-NIL private value for every processor in $P$. Conditions (i) and (ii) constrain nonfaulty relays only; condition (ii) allows either the original value or NIL for every prefix over $P$, including an empty prefix.

The procedure is applied only to $p$'s view $w\mapsto\sigma(pw)$, so it has no access to the full scenario or to $N$. Its intermediate strings are repetition-free, exclude both $p$ and $q$, and have length at most $m$. The set $S_{pq}$ contains values in $V$, not NIL; an empty set and a set with multiple values both cause a NIL record. The formal theorem retains the printed $n\ge m$ condition, although it is not needed in the proof of the stated set relationships. It also covers $p=q$, $m=0$, and empty or singleton processor sets when their quantified conditions apply. These conventions rule out an always-NIL decision rule and the trivial rule that reads $\sigma(q)$ from outside the receiver's view.

The cryptographic maps $A_p$, their message encodings, and the paper's assertion that practical authenticators can meet the assumption with arbitrarily high probability are outside scope. The formal result assumes the two exact authenticated-scenario conditions. A complete development needs finite-set cardinality and list facts, especially about distinct relay strings and bounded concatenation; these facts can be reused for other authenticated relay models.

Selected references

• M. Pease, R. Shostak, and L. Lamport, Reaching Agreement in the Presence of Faults, Journal of the ACM 27(2), 1980, 228–234. DOI: 10.1145/322186.322188.

Motivation

A fault-tolerant system built from several processors must let its working processors act on the same data, even though some processors may have failed in ways nobody can predict: a failed processor may stop relaying information, relay something it invented, or tell different processors different things. Pease, Shostak and Lamport (J. ACM 27 (1980) 228–234) isolated the core question in the setting of the SIFT aircraft-control computer: each of $n$ processors holds a private value, at most $m$ processors are faulty, and processors communicate only by two-party messages. Can the nonfaulty processors each compute a vector of values, one entry per processor, such that all nonfaulty processors compute the same vector and the entry of each nonfaulty processor is its true private value? This requirement is called interactive consistency.

The paper answers with a sharp threshold. Interactive consistency can be achieved when $n\ge 3m+1$ (Section 3), and it cannot be achieved when $n\le 3m$, however many rounds of message exchange are allowed (Section 4). With unforgeable signatures it can be achieved for every $n\ge m$ (Section 5). The impossibility half is the origin of the "$3m+1$" bound that appears throughout Byzantine fault tolerance, popularised two years later as the Byzantine Generals Problem (Lamport, Shostak, Pease, ACM TOPLAS 4 (1982)). This mission is the impossibility theorem.

Timeline:

• 1980: Pease, Shostak and Lamport prove the threshold $n\ge 3m+1$ for interactive consistency with oral messages, including the impossibility for $n\le 3m$ stated in terms of scenarios.
• 1982: Lamport, Shostak and Pease restate the problem as the Byzantine Generals Problem, with the same bound.
• 1985–1986: Fischer, Lynch and Merritt give a short "hexagon" proof of the same bound for several agreement problems (Distributed Computing 1 (1986)).

Setting

Let $P$ be a finite set of $n$ processors and $V$ a set of values. Write $P^*$ for the set of strings over $P$ (the empty string included) and $P^+$ for the nonempty strings. A string $p_1p_2\cdots p_r$ is read as a chain of reports: $p_1$ was told by $p_2$ that $\dots$ $p_{r-1}$ was told by $p_r$ that $p_r$'s private value is the recorded value.

A scenario is a map $\sigma: P^+\to V$. The value $\sigma(p)$ is processor $p$'s private value, and $\sigma(p_1\cdots p_r)$ is the value $p_1$ received for the chain $p_2\cdots p_r$. For $p\in P$, the $p$-scenario $\sigma_p$ is the restriction of $\sigma$ to the strings beginning with $p$: everything $p$ ever learns.

For a set $N\subseteq P$ of nonfaulty processors, $\sigma$ is consistent with $N$ if

$$\sigma(pqw)=\sigma(qw)\qquad\text{for all }q\in N,\ p\in P,\ w\in P^*,$$

that is, every nonfaulty processor reports truthfully what it knows or hears. Faulty processors are unconstrained.

A decision family assigns to each $p\in P$ a map $F_p$ that takes a $p$-scenario and a processor $q$ and returns a value $F_p(\sigma_p,q)\in V$: the entry $p$ computes for $q$. The family assures interactive consistency for $m$ faults if for every $N\subseteq P$ with $|N|\ge n-m$ and every scenario $\sigma$ consistent with $N$,

1. $F_p(\sigma_p,q)=\sigma(q)$ for all $p,q\in N$;
2. $F_p(\sigma_p,r)=F_q(\sigma_q,r)$ for all $p,q\in N$, $r\in P$.

In the Lean development these are InteractiveConsistency.Impossibility.ConsistentWith P N σ and AssuresIC P m F, with restrict σ p the $p$-scenario.

Formalization targets

Goal: the THEOREM of Section 4

If $|V|\ge 2$ and

$$3\le n\le 3m,$$

then no family $\{F_p\mid p\in P\}$ assures interactive consistency for $m$ faults. Since scenarios are defined on strings of every length, no bound on the number of rounds is assumed.

Milestones, in the order the proof of the paper uses them

1. If $3\le n\le 3m$, then $P$ is the disjoint union of three nonempty sets $A$, $B$, $C$, each with at most $m$ members (p. 232).
2. For such a partition and values $v,v'$, the scenarios $\alpha,\beta,\sigma$ that the page defines by recursion on the length of strings are consistent with $A\cup C$, $B\cup C$ and $A\cup B$ respectively (p. 233).
3. For the same scenarios, $\alpha(aw)=\sigma(aw)$ and $\beta(bw)=\sigma(bw)$ for all $a\in A$, $b\in B$, $w\in P^*$ (p. 233).

Significance

The theorem shows that the algorithm of Section 3 is optimal in its fault tolerance: with oral messages, $n\ge 3m+1$ processors are not only sufficient but necessary. Every later lower bound for Byzantine agreement, Byzantine broadcast and approximate agreement with unauthenticated messages rests on this bound or a variant of its argument, and it is the reason replicated state machines tolerating $m$ Byzantine faults use $3m+1$ replicas. It also explains why Section 5 needs authentication: the argument depends on faulty processors being able to relay fabricated values.

The result has been proved since 1980; what is open here is its formalization. Nothing on Prove2Me models message-passing agreement, and this mission states the theorem in the paper's own model: scenarios on unbounded strings and decision functions of a single $p$-scenario. The mission produces a reusable vocabulary (scenarios, consistency, interactive consistency) and the explicit three-scenario construction.

Difficulty

The obvious attempt is to argue round by round about what a processor can know after $k$ rounds; with unboundedly many rounds this never terminates in a contradiction. The paper's argument instead needs three entire scenarios, each a legitimate behaviour for a different set of faulty processors, that two processors cannot tell apart from their own views. Writing these scenarios down so that consistency holds on every string while the indistinguishability survives on every string is the delicate part: the faulty set of each scenario must relay exactly the values that keep the other scenario's view intact, and one of the defining equations ($\beta(paw)=\alpha(aw)$) looks like a misprint but is what the argument requires. The counting step is elementary but carries the hypothesis $n\ge 3$ that the printed theorem leaves implicit.

Formalization scope

Processors are a Finset P in a type with decidable equality; strings are lists read left to right ($p_1$ is the head of the list); a scenario is a total function List α → V whose values on the empty list and on lists with a letter outside $P$ carry no meaning: every condition quantifies only over strings whose letters lie in $P$. Decision functions have type α → (List α → V) → α → V and are applied only to the $p$-scenario fun w => σ (p :: w), never to $\sigma$; giving $F_p$ the whole scenario would make the problem trivial (output $\sigma(q)$). Consistency with $N$ constrains only relays by members of $N$, and includes the empty $w$. The quorum $|N|\ge n-m$ is written $|P|\le |N|+m$, which avoids truncated subtraction on $\mathbb N$. $|V|\ge 2$ is the existence of two distinct values.

Explicit readings of the page:

• The printed hypothesis "$n\ge 3m$" is a misprint for $n\le 3m$ (the proof opens "Since $n\le 3m$", and the section title is "Proof of Impossibility for $n<3m+1$"); with $n\ge 3m$ the statement is false.
• The hypothesis $n\ge 3$ is implicit in the proof's "three nonempty sets". It is necessary: for $n\le 2$ the family $F_p(\sigma_p,q)=\sigma(pq)$ assures interactive consistency.
• In the construction, each letter $a$, $b$, $c$ ranges independently over $A$, $B$, $C$ (so "$\alpha(cc)$" covers $\alpha(c'c)$); the value $\sigma(c'cw)$, which the page leaves unspecified, is fixed to $\sigma(cw)$.
• The construction is stated as a definition, and the two "easy" claims about it (consistency, indistinguishability) are separate milestones.

A complete development needs only finite sets and lists from Mathlib. The vocabulary of p. 232 is shared with the other two missions of this series, Reaching Agreement in the Presence of Faults 1 (the algorithm for $n\ge 3m+1$) and 3 (authenticated messages, $n\ge m$), each of which defines it in its own namespace. Proofs of the milestones and of the goal are welcome, as is a proof of the goal by a different route.

Selected references

• M. Pease, R. Shostak, L. Lamport, Reaching agreement in the presence of faults, Journal of the ACM 27(2) (1980) 228–234. https://doi.org/10.1145/322186.322188
• L. Lamport, R. Shostak, M. Pease, The Byzantine Generals Problem, ACM Transactions on Programming Languages and Systems 4(3) (1982) 382–401. https://doi.org/10.1145/357172.357176
• M. J. Fischer, N. A. Lynch, M. Merritt, Easy impossibility proofs for distributed consensus problems, Distributed Computing 1 (1986) 26–39. https://doi.org/10.1007/BF01843568

Motivation

A fault-tolerant system often replicates a computation on several processors and needs the nonfaulty ones to act on the same data, even though some processors may fail in arbitrary ways: send wrong values, send different values to different recipients, or lie about what they were told. Pease, Shostak and Lamport posed the question in 1980, motivated by the SIFT fault-tolerant aircraft-control computer under development at SRI (Wensley et al. 1978), where it arises in clock synchronization among other places: $n$ processors, at most $m$ of them faulty, communicate by two-party messages whose sender is always identifiable, and each holds a private value. Can the nonfaulty processors all compute the same vector of values, one entry per processor, whose entry for every nonfaulty processor is that processor's true value? The paper (J. ACM 27 (1980) 228–234) calls this interactive consistency and settles it: possible if and only if $n \ge 3m+1$ when messages can be forged in relay, and possible for every $n \ge m$ when they cannot. The same problem, under the name Byzantine generals, became the standard model of arbitrary ("Byzantine") failures in distributed computing (Lamport, Shostak & Pease 1982); the $3m+1$ bound underlies the quorum sizes of later replication protocols.

This mission covers the positive half of the paper's characterization: Section 3's recursive procedure, which achieves interactive consistency with $n\ge 3m+1$ processors in $m+1$ rounds of message exchange.

Setting

Let $P$ be a finite set of $n = |P|$ processors and $V$ a set of values. A string over a set $S$ is a finite sequence $p_1p_2\cdots p_r$ of elements of $S$, repetitions allowed. For $k\ge 1$ a $k$-level scenario is a map $\sigma$ from the nonempty strings over $P$ of length at most $k+1$ to $V$. The value $\sigma(p)$ is $p$'s private value $V_p$; for $r\ge 2$, $\sigma(p_1p_2\cdots p_r)$ is the value $p_2$ tells $p_1$ that $p_3$ told $p_2$ … that $p_r$ told $p_{r-1}$ is $p_r$'s private value. A $k$-level scenario records the outcome of $k$ rounds of message exchange.

Faults are modeled by a set $N\subseteq P$ of nonfaulty processors, unknown to the processors. Nonfaulty processors relay truthfully, so $\sigma$ is consistent with $N$ when

$$\sigma(pqw) = \sigma(qw)\qquad (q\in N,\ p\in P,\ w \text{ a string over } P,\ |pqw|\le k+1).$$

Faulty processors are otherwise unconstrained. A processor $p$ sees only its view $\sigma_p$, the restriction of $\sigma$ to strings beginning with $p$.

The procedure (p. 230). Processor $p$ computes the entry for processor $q$ as follows, with $n$ and $m$ the current processor count and fault bound:

1. If some $Q\subseteq P$ with $|Q|>(n+m)/2$ and some $v$ satisfy $\sigma_p(pwq)=v$ for every string $w$ over $Q$ of length $\le m$, record $v$.
2. Otherwise apply the procedure for $m-1$, $n-1$ to the processor set $P-\{q\}$ and the view $\hat\sigma_p(pw)=\sigma_p(pwq)$, obtaining a vector of $n-1$ entries. If at least $\lfloor (n+m)/2\rfloor$ of them agree, record the common value; otherwise record NIL.

In Lean this is InteractiveConsistency.OralAlgorithm.record m P τ q with τ = fun w => σ (p :: w), values in Option V with none for NIL.

Formalization targets

Goal: the procedure assures interactive consistency

For $n\ge 3m+1$, for every $N\subseteq P$ with $|N|\ge n-m$ and every $(m+1)$-level scenario $\sigma$ consistent with $N$,

$$\mathrm{record}(m,P,\sigma_p,q)=\sigma(q)\quad(p,q\in N),\qquad \mathrm{record}(m,P,\sigma_p,r)=\mathrm{record}(m,P,\sigma_{p'},r)\quad(p,p'\in N,\ r\in P).$$

This is procedure_assures_ic. It is the paper's claim about this procedure, not an existence statement.

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

1. Nonfaulty $q$ (p. 231): for $p,q\in N$, step (1) succeeds and $p$ records $V_q$.
2. Two step-(1) quorums agree (p. 231): if $p,p'\in N$ find quorums $Q_1,Q_2$ with values $v,v'$, then $v=v'$.
3. The subscenario (p. 230): for faulty $q$, $\hat\sigma(w)=\sigma(wq)$ is an $m$-level scenario on $P-\{q\}$ consistent with $N$, and $|N|\ge (n-1)-(m-1)$.
4. The $\hat Q$ claim (p. 231): if $Q,v$ satisfy step (1) for $p'$ and $q$, then $\hat Q=Q-\{q\}$ has at least $\lfloor(n+m)/2\rfloor$ members and $\hat Q, v$ satisfy step (1) of the recursive call for every $q'\in\hat Q$.

Significance

The theorem is the upper bound in the tight characterization $n\ge 3m+1$ of when interactive consistency is achievable with unauthenticated messages; the matching impossibility (the paper's Section 4 THEOREM) shows that no procedure, with any number of rounds, does better. The procedure is the ancestor of the "oral messages" algorithm $\mathrm{OM}(m)$ of the Byzantine generals paper, and its quorum arithmetic ($|Q|>(n+m)/2$, intersections of two quorums containing a nonfaulty member) recurs throughout Byzantine fault-tolerant replication.

The result is proved in the paper, in a half-page induction. What this mission adds is a machine-checked proof against an explicit model of scenarios, views and consistency with a bounded number of rounds. Machine-checked proofs exist for the related $\mathrm{OM}(m)$ algorithm of the later Byzantine generals paper in other proof systems; this procedure, with its quorum-based step (1), has to our knowledge not been formalized in Lean, and nothing on message-passing agreement exists on this platform.

Difficulty

Each step of the paper's proof is short, but the bookkeeping is where an argument breaks. The recursion changes three things at once: the processor set loses $q$, the fault bound drops by one, and the scenario becomes $\hat\sigma(w)=\sigma(wq)$ of one level less. The induction hypothesis must therefore be stated for every finite processor set and every scenario, and applied to a subscenario whose consistency is inherited only for strings of the right length. The mixed case, where one nonfaulty processor exits at step (1) and another recurses, is the delicate one: the two processors' computations take different branches, and since $q$ is faulty nothing forces either value to be $q$'s private value. The thresholds are exact: $|Q|>(n+m)/2$ in step (1) and $\lfloor(n+m)/2\rfloor$ agreeing entries in step (2), both in the current $n$ and $m$; off-by-one changes in either break the case analysis. Finally, step (2)'s majority value must be shown unique, so that two processors with the same vector record the same value.

Formalization scope

Processors form a Finset α with decidable equality; strings are List α, read left to right (the receiver first, the originator last), so $\sigma_p(pwq)$ is σ (p :: (w ++ [q])). A scenario is a total function List α → V; consistency with $N$ (ConsistentUpTo P N (m + 1) σ) constrains it only on strings over $P$ of length at most $m+2$, the domain of an $(m+1)$-level scenario and all the procedure reads. The procedure receives only the view fun w => σ (p :: w), never $\sigma$ or $N$. The fault hypothesis $|N|\ge n-m$ is P.card ≤ N.card + m; $m=0$ is included.

Explicit readings of the paper's prose: "size $>(n+m)/2$" is P.card + m < 2 * Q.card; $\lfloor(n+m)/2\rfloor$ is natural-number division; "strings over $Q$ of length $\le m$" includes the empty string and allows repetitions; the step-(2) vector is indexed by P.erase q and includes $p$'s own entry; the recorded value in step (1) is $\sigma_p(pq)$ (the empty string forces it); when several values reach the step-(2) threshold one is chosen deterministically from the vector (under the goal's hypotheses at most one does); for $m=0$ a failing step (1) records NIL (never reached under the hypotheses). Two printed slips are corrected in the Lean: "records $V_q$ and $q$" (for "for $q$") and "$\sigma_{p'}(p'wq')$" (for $\hat\sigma_{p'}$).

Trivializing formalizations are ruled out: the procedure never sees $\sigma$ itself (with it, recording $\sigma(q)$ would be trivial), consistency constrains only relays by nonfaulty processors, and $N$ ranges over every subset of size at least $n-m$.

The development needs only finite sets and lists; no library beyond Mathlib is required. The quorum-intersection lemmas and the subscenario construction are reusable for other oral-message protocols. Contributions welcome: proofs of the four milestones, the goal by induction on $m$, and a computable version of the procedure for concrete instances. This is mission 1 of a series of three on this paper; mission 2 formalizes the impossibility THEOREM for $n\le 3m$ (Section 4), and mission 3 the authenticated-message procedure for every $n\ge m$ (Section 5).

Selected references

• M. Pease, R. Shostak, L. Lamport, Reaching agreement in the presence of faults, Journal of the ACM 27(2), 1980, 228–234. https://doi.org/10.1145/322186.322188
• L. Lamport, R. Shostak, M. Pease, The Byzantine generals problem, ACM Transactions on Programming Languages and Systems 4(3), 1982, 382–401. https://doi.org/10.1145/357172.357176
• J. H. Wensley et al., SIFT: Design and analysis of a fault-tolerant computer for aircraft control, Proceedings of the IEEE 66(10), 1978, 1240–1255. https://doi.org/10.1109/PROC.1978.11114

Motivation

Consensus asks $N$ processors, each holding an initial value, to agree on one value despite some of them failing. It underlies replicated databases, atomic commit and state-machine replication. Its solvability depends on the timing assumptions. With fully synchronous processors and communication, $t$ fail-stop faults can be tolerated for any $t < N$. With fully asynchronous communication, Fischer, Lynch and Paterson showed that no deterministic protocol tolerates even one fail-stop fault (JACM 1985).

Dwork, Lynch and Stockmeyer (JACM 1988) introduced partial synchrony, a model between these two extremes. Message delays have an upper bound $\Delta$, but either the bound is unknown to the protocol, or it holds only from an unknown time on. For each fault type they found the exact number of faults that can be tolerated. This mission formalizes the lower bound for fail-stop faults: when the processors are synchronous and communication is partially synchronous, no consensus protocol tolerates $t$ faults once $N \le 2t$.

Timeline. 1985: Fischer, Lynch, Paterson, impossibility of consensus with one fail-stop fault under asynchrony. 1987: Dolev, Dwork, Stockmeyer, which combinations of synchrony assumptions admit consensus (JACM 1987). 1988: Dwork, Lynch, Stockmeyer, partial synchrony, with matching upper and lower bounds on resiliency for fail-stop, omission, authenticated Byzantine and Byzantine faults. The global stabilization time of the 1988 paper became a common liveness assumption for later fault-tolerant agreement protocols.

Setting

There are $N$ processors $p_1, \dots, p_N$. Each processor holds an initial value $v_i \in \{0, 1\}$. Each runs a deterministic protocol: a transition diagram over a possibly infinite set of states. In each state the next instruction is either $\mathrm{Send}(m, p_j)$, which puts message $m$ in $p_j$'s buffer, or $\mathrm{Receive}(p_i)$, which removes a set $S$ of messages from $p_i$'s buffer and delivers it. The next state depends on the current state and, for a Receive, on $S$. A step never both sends and receives. Each state may record a decision, and the first decision a processor records is final.

Real time is the ticks $1, 2, 3, \dots$. A run fixes the initial values and, at each tick, which processors take a step and which messages each Receive delivers. A message is delivered only after the tick at which it was sent, only to its addressee, and at most once.

• Synchronous processors ($\Phi = 1$): every correct processor takes a step at every tick.
• Fail-stop faults: a faulty processor follows the protocol until it stops, and it never restarts. A processor that stops at time $0$ is initially dead.
• $\Delta$ holds in $[T, \infty)$: a message sent at a tick $s_1 \ge T$ is delivered no later than any Receive of its addressee at a tick $s_2 \ge s_1 + \Delta$.
• Delta holds eventually: $\Delta$ is a fixed positive integer known to the protocol. In every run, $\Delta$ holds in $[T, \infty)$ for some unknown global stabilization time $T$. Messages sent before $T$ may be delayed arbitrarily or lost.
• Delta is unknown: the protocol is fixed first. In every run, some positive $\Delta$ holds in $[1, \infty)$.

A protocol is a $t$-resilient consensus protocol achieving weak unanimity if the following holds for every set $C$ of at least $N - t$ processors and every allowed run in which the processors of $C$ are correct and the others fail-stop. No two processors of $C$ decide differently (consistency). Every processor of $C$ decides (termination). If all initial values are $v$ and no processor is faulty, every decision is $v$ (weak unanimity).

Formalization targets

Goal: Theorem 4.3

For integers $t \le N$ with

$$2 \le N \le 2t,$$

there is no $t$-resilient consensus protocol achieving weak unanimity for binary values with fail-stop faults and synchronous processors. This holds for every positive $\Delta$ when $\Delta$ holds eventually, and when delta is unknown.

Milestones: the three scenarios of the proof

Split the processors into groups $P$ and $Q$ with $1 \le |P|, |Q| \le t$.

• Scenario A: all inputs $0$ and $Q$ initially dead. The processors of $P$ decide by some time $T_A$, and they decide $0$.
• Scenario B: all inputs $1$ and $P$ initially dead. The processors of $Q$ decide $1$ by some time $T_B$.
• Scenario C: all processors alive, $P$ starting with $0$ and $Q$ with $1$, and messages between the groups held back past a time $T$. Up to time $T$, every processor of $P$ is in the same state as in Scenario A, and every processor of $Q$ in the same state as in Scenario B.

Significance

The result. Theorem 4.3 shows that the resiliency $N \ge 2t + 1$ of the paper's fail-stop and omission protocols (Theorems 4.1 and 4.2) is optimal. It holds even under three restrictions: binary values, weak unanimity, and processors in perfect lock-step. Partial synchrony costs a majority of correct processors, whereas full synchrony costs nothing. The same scenarios give the authenticated Byzantine bound $N \ge 3t + 1$ (Theorem 4.4). The halting remark of Section 4.2 rests on an argument of the same kind.

The formalization. The theorem is proved in the paper, and its proof is short. It is not machine-checked anywhere known to the mission. No message-passing model is on the platform. This mission supplies one: a step-level model with buffers, per-message timing, fail-stop faults and both partially synchronous communication models. It also gives a machine-checked impossibility on top of that model. FLP, Theorem 4.4 and the lower bounds of Section 6 are natural follow-ups on the same definitions.

Difficulty

The informal proof is an indistinguishability argument. Making it formal means comparing different runs of the same deterministic protocol. Two points need care.

First, the scenarios must be allowed runs. Scenario C holds messages between the groups back past $\max(T_A, T_B)$. With delta unknown, this needs a $\Delta$ larger than that delay. When $\Delta$ holds eventually, $\Delta$ is fixed before the protocol, and the protocol fixes $T_A$ and $T_B$. So the delay is legal only for messages sent before the global stabilization time, which must therefore be placed after $\max(T_A, T_B)$. Read literally, "every message between the groups takes more than $\max(T_A, T_B)$ steps" is not an allowed run in this model.

Second, "the processors of $P$ act exactly as they do in Scenario A" is a claim about whole runs. Two runs must agree on states, on which messages are in which buffer, and on when each message is delivered, tick by tick up to $T$. With one-to-one sends and atomic steps, "delivered in exactly time 1" also needs a reading: a processor that sends at the next tick cannot receive at that tick.

Formalization scope

All declarations live in the namespace DLSConsensus.LowerBound. Processor $p_i$ is the index $i - 1$ of Fin N. Values are Bool. The protocol's state type and message type are arbitrary types in Type, finite or infinite. R.state i n is the state after tick $n$. A message instance is identified in the run by its sender and send tick. A Receive hands the protocol each delivered message as (sender, content); the absolute send tick is not exposed.

Explicit readings and conventions:

• "Fail-stop or omission faults": the goal is the fail-stop impossibility. It implies the omission case, because a fail-stop processor looks to the others like one whose sends are all omitted. The omission case is not a separate item.
• A fail-stop processor may skip ticks before its final stop. The processor timing bound $\Phi = 1$ applies to correct processors.
• "Decides": the first state that records a decision. Irreversibility therefore holds by definition.
• "Delivered in exactly time 1": the message is delivered no later than the addressee's first Receive at least one tick after the send.
• "Within time $T_A$" and "for some finite $T_B$": an explicit $\exists$ before the decision bound.
• "Messages between the groups take more than $\max(T_A, T_B)$ steps": no message between the groups is delivered at a tick $\le T$, for any given $T$.
• "Act exactly as they do": equal local states at every tick $n \le T$.
• Quantifier order: when $\Delta$ holds eventually, $\Delta$ is chosen first, then the protocol, then the run with its stabilization time. When delta is unknown, the protocol is chosen first and each run carries its own $\Delta$. In both models $\Delta > 0$.

Trivializing formalizations are ruled out. The model has allowed runs for every protocol, so Resilient is never vacuously true. Correct processors step at every tick, so termination does not fail for the wrong reason. Unanimity is the weak form, applied only when no processor is faulty.

Contributions welcome: a general simulation lemma (equal inputs up to a tick give equal states up to that tick), the construction of runs from a delivery schedule, and proofs of the scenarios. These parts are reusable for the other lower bounds of the paper.

Selected references

• C. Dwork, N. Lynch, L. Stockmeyer, Consensus in the presence of partial synchrony, Journal of the ACM 35(2), 1988, 288–323. https://doi.org/10.1145/42282.42283
• M. J. Fischer, N. A. Lynch, M. S. Paterson, Impossibility of distributed consensus with one faulty process, Journal of the ACM 32(2), 1985, 374–382. https://doi.org/10.1145/3149.214121
• D. Dolev, C. Dwork, L. Stockmeyer, On the minimal synchronism needed for distributed consensus, Journal of the ACM 34(1), 1987, 77–97. https://doi.org/10.1145/7531.7533

Motivation

Consensus asks $N$ processors, each starting with a value, to agree on one value although some of them may be faulty. It underlies replicated databases, atomic commitment and state-machine replication. Two classical models bracket the problem. In a fully synchronous system, with known bounds on message delay and processor speed, consensus is solvable for many fault types. In a fully asynchronous system, Fischer, Lynch and Paterson showed in 1985 that no deterministic protocol tolerates even one fail-stop fault (FLP, J. ACM 1985).

Dwork, Lynch and Stockmeyer (J. ACM 35(2), 1988, 288–323) introduced partial synchrony between these extremes: message delays are bounded, but either the bound is unknown, or it holds only from an unknown global stabilization time (GST) on. This model, and the GST abstraction in particular, became the standard assumption under which practical consensus protocols (Paxos-style and Byzantine fault-tolerant replication) are proved live. The paper determines, for each fault type, the largest number $t$ of faults that consensus can tolerate under partial synchrony. This mission formalizes its first positive result: for fail-stop and omission faults, $N \ge 2t+1$ processors suffice.

Setting

There are $N$ processors $p_1,\dots,p_N$, an integer $t \le N$, and an arbitrary set $V$ of values; processor $p_i$ starts with $\mathrm{init}(p_i)\in V$.

In the basic round model (Section 3.1 of the paper), computation proceeds in rounds $r = 1, 2, 3, \dots$. In each round every processor sends messages, each message is either delivered in that round or lost, and every processor then performs a state transition on the messages it received. Losses are described by a predicate $\mathrm{deliv}(r,q,p)$. A set $C$ of processors (the correct ones) and a round $\mathrm{GST}$ constrain it: every message sent at a round $r \ge \mathrm{GST}$ from a processor of $C$ to a processor of $C$ is delivered. Before GST any message may be lost, and messages from or to processors outside $C$ may be lost at any time. Processors outside $C$ follow the protocol but lose sends and receptions (omission faults, which include fail-stop faults).

Algorithm 1 (Section 3.2.1) works as follows. Every processor keeps a set $\mathrm{PROPER}$, initially $\{\mathrm{init}(p)\}$, attaches it to every message, and merges in every PROPER set it receives. A processor may hold locks, each a value with an associated phase number; $v$ is acceptable to $p$ if $p$ has no lock on a value other than $v$. Phase $k \ge 1$ belongs to $p_i$ when $k \equiv i \pmod N$. Trying phase $k$ occupies rounds $4k-3$, $4k-2$, $4k-1$:

1. every processor sends the owner the list of its acceptable values that are in its PROPER set; the owner proposes, by an arbitrary choice, a value appearing in at least $N-t$ of the lists received, if there is one;
2. the owner broadcasts $(\mathrm{lock}\ v, k)$; each receiver locks $v$ with phase $k$;
3. each receiver acknowledges; with at least $t+1$ acknowledgements the owner decides $v$.

Lock-release phase $k$ is round $4k$: every processor broadcasts its locks $(v,h)$, and a lock on $v$ with phase $h$ is released on receipt of some $(w,h')$ with $w \ne v$ and $h' \ge h$.

The correctness conditions (Section 2.4) for the set $C$ are consistency (no two decisions of processors in $C$ differ), termination (every processor in $C$ decides), and strong unanimity (if all $N$ initial values equal $v$, every decision in $C$ is $v$).

Formalization targets

Goal: Theorem 3.1

For all $N, t$ with $N \ge 2t+1$, every value type $V$, all initial values, every $C$ with $|C| \ge N-t$, every $\mathrm{GST}$, every delivery pattern allowed for $C$ and $\mathrm{GST}$, and every admissible choice of proposals,

$$\text{Algorithm 1 achieves}\quad \text{Consistency}(C)\ \wedge\ \text{StrongUnanimity}(C)\ \wedge\ \text{Termination}(C).$$

This is the theorem as printed; it fixes no constants.

Milestones

• Lemma 3.1: no two distinct values acquire locks with the same associated phase.
• Lemma 3.2: if $v$ is decided at the first phase $k$ at which any decision is made, then at least $t+1$ processors lock $v$ at phase $k$, and each keeps, from then on, a lock on $v$ with phase at least $k$.
• Lemma 3.3: immediately after a lock-release round $4k \ge \mathrm{GST}$, the processors of $C$ together hold locks on at most one value.
• Round bound (Section 3.2.1, p. 298): every processor of $C$ decides at some phase $k$ with

$$4k-1 \le \mathrm{GST} + 4(N+1).$$

Significance

Theorem 3.1 shows that, against omission and fail-stop faults, partially synchronous communication costs nothing in resilience compared with a majority bound: $N \ge 2t+1$ suffices, and Section 4 of the paper shows that $N \le 2t$ does not. The lock-and-release structure of Algorithm 1 (a value is decided only after a quorum locks it, and locks are released only on evidence of a later competing lock) recurs in later partially synchronous protocols, where safety must hold regardless of timing and liveness is obtained only after stabilization. The result separates the two concerns cleanly: consistency and strong unanimity hold in every run, while termination uses GST.

The result is proved in the paper; to the best of the available information it has not been formalized in Lean, and no distributed-computing model exists on Prove2Me. The mission produces a machine-checked model of the basic round model with a GST delivery guarantee, a full executable specification of Algorithm 1, and proofs of its safety and liveness. The paper's own proof of Lemma 3.3 is one line and the termination argument relies on "sufficient communication"; a formal proof must make these steps explicit.

Difficulty

The safety argument is an invariant over an unbounded number of phases with an arbitrary loss pattern: a lock on the decided value must be shown never to be released without being replaced by a higher lock on the same value, while competing locks on other values may exist at faulty or slow processors. The obvious argument ("after a decision, every later proposal must equal the decided value") is circular without a persistence statement for locks such as Lemma 3.2. Liveness requires reasoning about what every correct processor knows after GST (its PROPER set and the locks of the others), and it depends on processors sending lock-release and list messages even when these carry no locks or no acceptable values. Quorum counting with $N-t$ and $t+1$ must be carried out over distinct senders.

Formalization scope

• Processors are Fin N; the paper's $p_i$ is the processor of index $i-1$. Rounds start at $1$; exec … 0 is the initial state and exec … r the state after round $r$. Phases start at $1$.
• The paper's "chooses one arbitrarily" is a parameter pick : ℕ → Set V → V, required only to pick an element of every nonempty candidate set, and universally quantified in every theorem.
• The paper's "the behavior of the processors not in $C$ is allowed by the fault type $F$" is read as: processors outside $C$ run Algorithm 1, and any message from or to them may be lost (omission faults, containing fail-stop).
• The GST guarantee covers a processor's messages to itself when it is in $C$; before GST self-messages may be lost like any other.
• Every processor sends its list in round $4k-3$ and its lock-release message in round $4k$ even when they are empty, since both carry the PROPER set (Section 3.2: PROPER sets are piggybacked on all messages).
• A decision is the event DecidesAt p k v (owner of phase $k$, proposed $v$, at least $t+1$ acknowledgements in round $4k-1$); consistency requires all such events of processors in $C$ to agree.
• "Decide by round $\mathrm{GST}+4(N+1)$" is read as: the deciding phase $k$ satisfies $4k-1 \le \mathrm{GST}+4(N+1)$.
• Not formalized: Remark 1's asymptotic claims, the PROPER simplifications for weak unanimity, Algorithms 2 and 3.

A formalization in which a run cannot exist, the delivery constraint is unsatisfiable, the choice of proposals is fixed, or faulty processors are absent ($C$ = all processors) would trivialize the theorem; the model here admits runs in which processors decide, and $C$ ranges over all sets of at least $N-t$ processors.

Reusable beyond this mission: the round-based message-passing model with a GST delivery guarantee and omission faults. Contributions of general lemmas about runs (monotonicity of PROPER sets, persistence of locks, quorum intersection over Finset) are welcome.

Selected references

• C. Dwork, N. Lynch, L. Stockmeyer, Consensus in the presence of partial synchrony, Journal of the ACM 35(2), 1988, 288–323. https://doi.org/10.1145/42282.42283
• M. J. Fischer, N. A. Lynch, M. S. Paterson, Impossibility of distributed consensus with one faulty process, Journal of the ACM 32(2), 1985, 374–382. https://doi.org/10.1145/3149.214121

Motivation

When are two scientific theories "the same theory in different words"? Philosophers of science have used two formal criteria. Definitional equivalence (Glymour) is strict: it requires a common definitional extension and therefore cannot relate theories with different numbers of sorts. Categorical equivalence (Halvorson, Weatherall) is liberal: it asks only that the categories of models be equivalent. It has been applied to classical mechanics, electromagnetism and Newtonian gravitation (Weatherall 2016; survey in Weatherall 2019).

Barrett and Halvorson (2016) proposed Morita equivalence as a syntactic criterion between these two. It allows definitions of new sorts (products, coproducts, subsorts, quotients) in addition to the usual definitions of new predicates and function symbols. Their main results place the new criterion strictly between the other two:

• Morita equivalence implies categorical equivalence (their Theorem 5.1).
• The converse fails (their Theorem 5.2).

This mission formalizes that comparison: the semantic core of Morita extensions, the implication, the separating example, and the paper's motivating "two kinds of things" example.

Setting

A signature $\Sigma$ (Sig) consists of a type of sorts, function symbols $f : \sigma_1\times\dots\times\sigma_m\to\sigma$ and predicate symbols $p\subseteq\sigma_1\times\dots\times\sigma_m$. Formulas (Formula L Γ) are built in a typed context $\Gamma$ from $\bot$, $=$, predicates, $\to$ and $\forall$. A structure (Str) assigns a nonempty set to each sort and interprets the symbols. A theory $T$ is a set of formulas in context, each read as its universal closure; a model of $T$ is a structure satisfying them all.

The category $\mathrm{Mod}(T)$ (Model T) has the models of $T$ as objects and elementary embeddings as arrows: maps on every sort that preserve and reflect every formula. Theories $T_1,T_2$ are categorically equivalent (CategoricallyEquivalent) if $\mathrm{Mod}(T_1)\simeq\mathrm{Mod}(T_2)$.

A Morita extension of a $\Sigma$-theory $T$ (MoritaData L T) adds to $\Sigma$:

• new sorts, each with its defining symbols:
  • a product $\sigma$ of $\sigma_1,\sigma_2$, with projections $\pi_1,\pi_2$;
  • a coproduct, with injections $\rho_1,\rho_2$;
  • a subsort cut out by a $\Sigma$-formula $\varphi(x)$, with an injection $i$;
  • a quotient by a $\Sigma$-formula $\varphi(x_1,x_2)$, with a projection $\varepsilon$;
• new predicates and function symbols, each explicitly defined by a $\Sigma$-formula.

Each new symbol gets one defining axiom, and the symbols of one new sort share a single axiom. The extension $T^+$ (D.ext) is $T$ together with these axioms. Each definition must satisfy its admissibility condition in every model of $T$:

Definition	Condition
subsort	$\exists x\,\varphi(x)$
quotient	$\varphi$ is an equivalence relation
function symbol	$\forall x\,\exists!y\,\varphi(x,y)$

The reduct gives a functor $\Pi:\mathrm{Mod}(T^+)\to\mathrm{Mod}(T)$ (D.proj).

$T_1$ and $T_2$ are Morita equivalent (MoritaEquivalent) if two finite chains of Morita extensions $T_1\rightsquigarrow T_1'$ and $T_2\rightsquigarrow T_2'$ (MoritaReach) end in logically equivalent theories, that is, theories with the same models, over a common signature.

Formalization targets

Goal: Morita equivalence implies categorical equivalence

$$T_1 \text{ Morita equivalent to } T_2 \;\Longrightarrow\; \mathrm{Mod}(T_1)\simeq\mathrm{Mod}(T_2).$$

Milestones

1. Unique expansion. Every model $M$ of $T$ has an expansion $N\models T^+$ with $\Pi N\cong M$, and any two such expansions are isomorphic.
2. $\Pi$ is faithful.
3. $\Pi$ is full.
4. Conservativity. For every $\Sigma$-formula $\alpha$: $T\models\alpha$ iff $T^+\models\alpha$.
5. Translation. Every $\Sigma^+$-formula whose free variables all have old sorts is $T^+$-equivalent to a $\Sigma$-formula.
6. Two kinds of things. $T_1=\{\exists x\,p(x),\ \exists x\,q(x),\ \forall x\,(p(x)\vee q(x)),\ \forall x\,\neg(p(x)\wedge q(x))\}$ over one sort is Morita equivalent to the empty theory over two sorts.
7. Separating example, first half. $T_1=\{\exists^{=1}x\,(x=x)\}$ and $T_2=T_1\cup\{\forall y\,(p_0(y)\to p_i(y)) : i\in\mathbb N\}$, over one sort and countably many unary predicates, are categorically equivalent.
8. Separating example, second half. These two theories are not Morita equivalent.

Milestones 1–3 together say that $\Pi$ is an equivalence of categories. Milestones 6–8 are not needed for the goal; they record the paper's examples, which show that Morita equivalence relates theories with different numbers of sorts and is strictly stronger than categorical equivalence.

Significance

The result itself. The goal makes Morita equivalence a syntactic sufficient condition for categorical equivalence: an explicit dictionary of definitions yields an equivalence of model categories. Milestone 8 shows the converse fails, so categorical equivalence is strictly weaker. Milestone 6 shows that Morita equivalence, unlike definitional equivalence, can relate theories with different numbers of sorts. Together these locate the criterion that later philosophy-of-physics work uses to compare formulations with different ontologies, such as different numbers of kinds of objects.

Formalizing it. The results are proved on paper and, as far as is known, have no machine-checked proofs. Mathlib's ModelTheory library is single-sorted, so none of this is available there. The mission produces a reusable many-sorted first-order logic with:

• syntax, semantics and signature maps;
• elementary embeddings and the category of models;
• Morita extensions with their reduct functors.

The paper's arguments for conservativity and translation are informal in places; for example, the translation in the appendix uses coding of new-sorted variables. A formal proof fixes these details.

Difficulty

The obvious route to the goal composes the reduct functors along the chains. The work lies in showing that each reduct is an equivalence when the arrows are elementary embeddings.

• Fullness. An elementary embedding of reducts extends uniquely to the new sorts. Showing that the extension is again elementary requires the translation of Milestone 5: every $\Sigma^+$-formula has to be pulled back to a $\Sigma$-formula, including formulas that quantify over the new sorts.
• Coproduct and quotient sorts. Quantifiers over these sorts must be eliminated in favour of quantifiers over the old sorts.

For Milestone 8 the difficulty is reversed. One must rule out every pair of chains, including chains that introduce arbitrary new sorts. The paper's proof argues with a single common Morita extension. The definition, however, allows chains, and the paper notes that a chain need not collapse to a single extension. The argument must therefore be run through conservativity and translation along each chain.

Formalization scope

• Self-contained logic. Signatures have dependent arities (Fin m → Srt). Terms and formulas use de Bruijn variables in typed contexts Γ : Fin n → Srt; Formula.all binds variable 0.
• Theories. A theory is a Set (Axiom L), each axiom being a formula in context read as its universal closure. Because sorts are nonempty, this agrees with the sentence version.
• Nonempty sorts. Every structure has nonempty carriers. This is the paper's convention, and without it Milestone 6 is false: the empty theory over two sorts would have models with an empty sort.
• Morita extensions are built, not recognized. MoritaData L T lists the new sorts and symbols and their defining $\Sigma$-formulas. The signature $\Sigma^+$ (D.sig) and the axioms are generated from it, and admissibility is stated semantically, over all models of $T$. Any Morita extension in the paper's sense is of this form up to renaming of the new symbols.
• A common signature up to renaming. MoritaEquivalent asks for a bijective signature map F between the two chain ends such that a structure is a model of $T_2'$ iff its F-reduct is a model of $T_1'$.
• Universes. Models live in Type.
• Separating example. The paper writes $T_2$ with fresh symbols $q_i$; here $T_1$ and $T_2$ share the signature with predicates $p_i$, which only renames symbols.
• No trivialization. None of the targets holds vacuously: Morita extensions require genuine admissibility proofs, and the arrows are elementary embeddings, not arbitrary maps. Milestone 6 needs explicit chains and an explicit renaming, with arity casts.

A complete development will need:

• the substitution and weakening lemmas for de Bruijn formulas;
• the realization of signature maps;
• the construction of expansions;
• a translation function from $\Sigma^+$-formulas to $\Sigma$-formulas.

These pieces are reusable for any later work on interpretations or theoretical equivalence. Alternative proofs of Milestone 8, for example by counting finitely axiomatized subtheories, are welcome.

Selected references

• T. W. Barrett, H. Halvorson, Morita Equivalence, Rev. Symb. Logic 9 (2016) 556–582. arXiv:1506.04675. Source of all targets: §3–§5 and the appendix; Example 4 and Theorems 4.1–4.3, 5.1, 5.2.
• J. O. Weatherall, Are Newtonian Gravitation and Geometrized Newtonian Gravitation Theoretically Equivalent?, Erkenntnis 81 (2016) 1073–1091. arXiv:1411.5757.
• J. O. Weatherall, Theoretical Equivalence in Physics, Philos. Compass 14 (2019). arXiv:1810.08192.
• H. Halvorson, The Logic in Philosophy of Science, Cambridge University Press, 2019. doi:10.1017/9781316275603.

Reversible Binary 2D Cellular Automata: Disproof of $R = 18$ and Lower Bound $R \ge 33,076,358$

Problem Statement & Context

A two-dimensional binary cellular automaton (CA) on the infinite grid $\mathbb{Z}^2$ with the standard $3 \times 3$ Moore neighborhood $M = \{-1,0,1\}^2$ updates configurations $c : \mathbb{Z}^2 \to \{0,1\}$ via a local rule $f : \{0,1\}^M \to \{0,1\}$ according to:

$$F_f(c)(z) = f\Big(\big(c(z + u)\big)_{u \in M}\Big)$$

A local rule $f$ is reversible (or bijective) if its global map $F_f$ is a bijection of the configuration space $\{0,1\}^{\mathbb{Z}^2}$.

Let $R$ denote the exact number of reversible binary local rules on the $3 \times 3$ Moore neighborhood. A longstanding open conjecture asserted that $R = 18$, corresponding solely to the 18 trivial single-cell shifts and complemented shifts:

$$f(c) = c(z + u) \quad \text{or} \quad f(c) = 1 - c(z + u) \quad (u \in M)$$

In this mission, we formally disprove $R = 18$ by constructing an explicit non-trivial conserved-landscape rule $f_\star$ whose global map $F_{f_\star}$ is an involution on $\mathbb{Z}^2$, proving $19 \le R$. We further extend this result to establish $R \ge 33,076,358$.

---

Ladder of Proven Bounds

Bound Level	Proven Bound	Description / Mathematical Mechanism
$\mathbf{L_0}$	$R \ge 18$	Trivial single-cell shifts and complemented shifts ($2 \times 9 = 18$).
$\mathbf{L_1}$	$R \ge 19$	Disproof of $R = 18$ via explicit non-trivial conserved-landscape rule $f_\star$.
$\mathbf{L_2}$	$R \ge 33,070,982$	Conserved-landscape marker rule family ($24,576$ centered rules).
$\mathbf{L_3}$	$R \ge 33,076,358$	Incorporation of $5,376$ off-centre marker rules reading center cell $x_0$.
Symmetry	$R_{\text{rot90}} = 74$	Exactly 74 rules invariant under $90^\circ$ spatial rotations.
Torus	$	\mathcal{R}_{2,3}
Upper Limit	$R \le 2^{511}$	Derived from constant divergence condition $f(\mathbf{0}) \ne f(\mathbf{1})$.

---

Key Milestone Theorems

1. Theorem 1 (Trivial Rule Reversibility): All 18 single-cell shift and negated-shift rules are bijective global maps.
2. Theorem 2 (Conserved-Landscape Involution $f_\star$): The rule $f_\star$ complements a cell iff its W and SE neighbors are $1$ and the other six are $0$. $F_{f_\star} \circ F_{f_\star} = \text{id}$.
3. Theorem 3 (Non-Triviality & $19 \le R$): $f_\star$ differs from every trivial rule, establishing $19 \le R$ and disproving $R = 18$.
4. Theorem 4 (Constant Divergence Condition): Every reversible rule satisfies $f(\mathbf{0}) \ne f(\mathbf{1})$.