Theory of Computation

Motivation

Barak, Goldreich, Impagliazzo, Rudich, Sahai, Vadhan and Yang (J. ACM 59(2), 2012) proved that virtual-black-box obfuscation is impossible in general: there are programs from which any obfuscated copy leaks something that oracle access to the program does not. The definition being refuted asks that whatever can be computed from the obfuscated code can also be computed by a simulator that only has oracle access to the program and is told an upper bound on its size.

Appendix A of the paper studies the computability analogue of this definition, where running time is unbounded. Rice's theorem says that no non-trivial property of the function computed by a Turing machine is decidable. The appendix asks a relative version: if a property of programs depends only on the computed function and is decidable from the code on a promise, can it also be decided from black-box access alone? Theorem A.2 answers yes when the simulator is given the size $1^{|M|}$. Theorem A.4, the goal of this mission, shows that the size cannot be dropped. The result says which part of the simulator's interface is essential: an upper bound on program length is needed already in the computability setting, not only to pay for running time.

Setting

A machine $M$ is a one-tape Turing machine over the tape alphabet $\{0,1\}$, with $0$ the blank, and with states $0,1,\dots,q$; state $0$ is initial. In state $s$ reading symbol $a$ the machine either halts or moves to a new state and performs one action (move left, move right, or write a symbol). One such transition is one step. The size $|M|=q+1$ is the number of states.

Inputs are natural numbers in unary: input $x$ is the tape $1^x$, so $|x|=x$. When $M$ halts, its output is the number of consecutive $1$s starting at the head. The computed function $[M]:\mathbb N\rightharpoonup\mathbb N$ is defined where $M$ halts. The step-bounded function is

$$\langle M\rangle(1^t,x)=\begin{cases}y&\text{if } M(x)\text{ halts with output } y \text{ after at most } t \text{ steps},\\ \bot&\text{otherwise.}\end{cases}$$

A promise problem $\Pi=(\Pi_Y,\Pi_N)$ is a pair of disjoint sets of machines. It is closed under $[\cdot]$ if $[M]=[M']$ implies $M\in\Pi_Y\iff M'\in\Pi_Y$ and $M\in\Pi_N\iff M'\in\Pi_N$. It is decidable if a program $T$ reading the description $\ulcorner M\urcorner$ outputs $1$ on $\Pi_Y$ and $0$ on $\Pi_N$; outside $\Pi_Y\cup\Pi_N$, $T$ may diverge.

An oracle machine $S$ may query $\langle M\rangle$: it asks $(t,x)$ and receives $\langle M\rangle(1^t,x)$. $S^{\langle M\rangle}()$ is its output with this oracle and no input. In particular $S$ does not know $|M|$.

Conjecture A.3 (Rice's theorem, third generalization) asserts: for every promise problem $\Pi$ closed under $[\cdot]$ and decidable, there is an oracle machine $S$ with

$$M\in\Pi_Y\Rightarrow S^{\langle M\rangle}()=1,\qquad M\in\Pi_N\Rightarrow S^{\langle M\rangle}()=0.$$

The proof uses the description complexity of a partial function, $\mathrm{KC}(f)=\min\{|M|:[M]=f\}$.

Formalization targets

Goal: Theorem A.4

$$\neg\,\text{Conjecture A.3}.$$

There is a decidable promise problem closed under $[\cdot]$ that no oracle machine without the size can decide. The witness is

$$\Pi_Y=\{M: M\text{ always halts and } \exists x<\mathrm{KC}([M]),\ [M](x)=1\},\qquad \Pi_N=\{M: M\text{ always halts and } [M]\equiv 0\}.$$

Milestones, in the order of the paper's proof

1. $\Pi$ is closed under $[\cdot]$.
2. $\mathrm{KC}([M])\le|M|$.
3. $\Pi$ is decidable.
4. The machine $Z$ that reads its input and returns $0$ satisfies $\langle Z\rangle(1^t,x)=\bot$ for $t<|x|$ and $0$ otherwise, and $Z\in\Pi_N$.
5. If $S^{\langle M_0\rangle}()=\sigma$, there is $n$ such that every $M$ agreeing with $M_0$ on all $\langle\cdot\rangle(1^t,x)$ with $t,|x|\le n$ also has $S^{\langle M\rangle}()=\sigma$.
6. For all $n,r$ some machine computes $N_{n,r}(x)=0,1,r$ (for $|x|\le n$, $|x|=n+1$, $|x|\ge n+2$) and has the same step profile as $Z$ on all $|x|\le n$.
7. For every $n$ some $r$ has $\mathrm{KC}(N_{n,r})>n+1$, so machines computing $N_{n,r}$ lie in $\Pi_Y$.

Significance

The result. Theorem A.4 separates two interfaces for a simulator. With $1^{|M|}$, every decidable promise problem closed under $[\cdot]$ is decided from black-box access (Theorem A.2). Without it, some are not. The size bound in the virtual-black-box definition is therefore doing real work even when complexity is ignored, and any computability-theoretic notion of obfuscation must hand the simulator a bound on the program's length.

Formalizing it. The theorem is proved in the paper in a few lines, and the proof rests on facts the paper does not argue: that a halting oracle computation reads only finitely many oracle values, that a machine with a prescribed function and a prescribed running time on short inputs exists, and that some $N_{n,r}$ has description complexity above $n+1$. The paper says only "Let r be a string of Kolmogorov complexity 2n"; the counting argument behind it is left implicit. No machine-checked proof of Theorem A.4 or of Theorem A.2 is known to exist. This mission produces one in a model with literal step counts, together with reusable statements about step-bounded Turing machines and the use principle for oracle programs.

Difficulty

The obvious attempt at Conjecture A.3 is to search for a machine consistent with the observed values of $\langle M\rangle$ and run $T$ on it. Without a size bound the search space is infinite, and a finite prefix of $\langle M\rangle$ never pins down $[M]$. The difficulty of the formal proof is elsewhere. It has to build $N_{n,r}$ as an actual Turing machine with an exact step count on short inputs, and to prove that its description complexity exceeds $n+1$. Both need the step semantics to be exact. A fuel-based semantics in which larger programs need more fuel on the same input does not support the construction of $N_{n,r}$.

Formalization scope

Machines are Mathlib's Post–Turing machines Turing.TM0.Machine Bool (Fin (q+1)), with the blank false and initial state 0. $[M]$ is TM0.eval followed by the head read-out; $\langle M\rangle(1^t,x)$ iterates TM0.step at most $t$ times. $|M|$ is the number of states, so there are finitely many machines of each size. Inputs are unary, $|x|=x$. This is forced, because the proof compares inputs both with numbers ($x<\mathrm{KC}([M])$, $N_{n,r}(n+1)=1$) and with lengths ($|x|\le n$, $t<|x|$). The paper's string $r$ is a natural number. The description $\ulcorner M\urcorner$ is the encoding of $q$ and the transition table, and the decider $T$ is a Mathlib Nat.Partrec.Code acting on it. $\mathrm{KC}$ is sInf over $\mathbb N$, which would be $0$ for a function no machine computes; that case does not arise for $f=[M]$, and milestone 7 asserts $\mathrm{KC}>n+1$ outright.

Oracle machines are the published uniform oracle programs FriedbergMuchnik.Program with semantics oracleEval. A query $(t,x)$ is coded Nat.pair t x, and the answers $\bot$ and $y$ are coded $0$ and $y+1$. $S^{\langle M\rangle}()$ runs $S$ on the fixed input $0$.

The simulator is a single program chosen before $M$, and it only sees the values of $\langle M\rangle$ it queries. A formalization in which $S$ is an arbitrary function of the whole oracle, or receives $|M|$, would make the goal false, and one in which the oracle is $[M]$ changes the statement. Both are excluded here.

Needed infrastructure: computability of simulating a TM0 machine from its description (for milestone 3), the use principle for oracleEval with a total oracle (milestone 5), explicit construction and step analysis of $Z$ and $N_{n,r}$ (milestones 4 and 6), and a counting bound on machines of bounded size (milestone 7). The first two are reusable beyond this mission. Proofs of individual milestones are welcome independently.

Selected references

• B. Barak, O. Goldreich, R. Impagliazzo, S. Rudich, A. Sahai, S. Vadhan, K. Yang, On the (Im)possibility of Obfuscating Programs, Journal of the ACM 59(2), 2012. https://doi.org/10.1145/2160158.2160159 (Appendix A, Conjecture A.3 and Theorem A.4, p. A:42 of the author's copy).
• H. G. Rice, Classes of recursively enumerable sets and their decision problems, Transactions of the AMS 74(2), 1953. https://doi.org/10.1090/S0002-9947-1953-0053041-6

Motivation

Program obfuscation asks for a compiler that turns a program into one computing the same function while revealing nothing beyond what black-box access to the function reveals. Barak, Goldreich, Impagliazzo, Rudich, Sahai, Vadhan and Yang (J. ACM 59(2), 2012; conference version CRYPTO 2001) showed that this "virtual black box" notion cannot be achieved in general. Part of their motivation is an informal reading of Rice's Theorem: since every non-trivial semantic property of programs is undecidable from the code, "the only useful thing you can do with a machine is run it". Section 5 of the paper asks whether a complexity-theoretic analogue holds, and Appendix A asks what the right computability-theoretic statement is once one passes from languages to promise problems.

Classical Rice's Theorem (Rice, 1953) concerns languages: a decidable set of machines closed under functional equivalence is empty or everything. For promise problems the naive analogue (Conjecture A.1 of the paper) is false: the problem "halts everywhere and outputs 1 on 0" versus "halts everywhere and outputs 0 on 0" is decidable, non-trivial, and closed under functional equivalence. Appendix A replaces "trivial" by "decidable by a simulator that only runs the machine", proves that version (Theorem A.2), and shows that the size bound given to the simulator cannot be dropped (Theorem A.4, a separate mission in this series). This mission formalizes Theorem A.2.

Setting

A machine $M$ is a program for a partial recursive function, identified with its description, a natural number $\ulcorner M\urcorner$. Its computed function $[M]:\mathbb N\rightharpoonup\mathbb N$ is possibly partial, and $[M]\equiv[M']$ means equality of partial functions. The size $|M|$ is the length of the binary description of $M$; there are at most $2^s$ machines of size $s$.

The bounded run of $M$ is

$$\langle M\rangle(1^t,x)=\begin{cases} y & \text{if } M(x)\text{ halts with output } y \text{ within budget } t,\\ \bot&\text{otherwise.}\end{cases}$$

An oracle machine $S$ may query $\langle M\rangle$ at any pair $(t,x)$ of its choice; $S^{\langle M\rangle}(z)$ is its output on input $z$. Oracle access to $\langle M\rangle$ is what running $M$ provides: one may choose inputs and budgets, but one never sees the code.

A promise problem $\Pi=(\Pi_Y,\Pi_N)$ is a pair of disjoint sets of machines. A machine $T$ decides $\Pi$ if $T(\ulcorner M\urcorner)=1$ for $M\in\Pi_Y$ and $T(\ulcorner M\urcorner)=0$ for $M\in\Pi_N$; nothing is asked of $T$ outside $\Pi_Y\cup\Pi_N$. $\Pi$ is closed under $[\cdot]$ if $[M]\equiv[M']$ implies $M\in\Pi_Y\Leftrightarrow M'\in\Pi_Y$ and $M\in\Pi_N\Leftrightarrow M'\in\Pi_N$.

A machine $N$ is $n$-compatible with $M$ if $\langle N\rangle(1^t,x)=\langle M\rangle(1^t,x)$ for all $t\le n$ and all $x$ with $|x|\le n$, and $S_n$ denotes the set of machines of size $|M|$ that are $n$-compatible with $M$.

Formalization targets

Goal: Theorem A.2 (p. A:41)

If $\Pi$ is closed under $[\cdot]$ and decidable, then there is one oracle machine $S$ such that for every machine $M$

$$M\in\Pi_Y\Rightarrow S^{\langle M\rangle}(1^{|M|})=1,\qquad M\in\Pi_N\Rightarrow S^{\langle M\rangle}(1^{|M|})=0 .$$

Milestones (proof of Theorem A.2, pp. A:41–A:42)

1. Fact (1): $n$-compatibility with $M$ is decidable by one oracle machine with oracle $\langle M\rangle$, uniformly in $M$, $N$, $n$.
2. Fact (3): if $[M]\not\equiv[N]$, there is $n'$ with $N$ not $n$-compatible with $M$ for every $n>n'$.
3. There is $n''$ such that every $N\in S_n$ with $n>n''$ satisfies $[N]\equiv[M]$.
4. If some stage $n$ finds $T$, run for $n$ steps, halting on all of $S_n$ with a common answer $\sigma$, then $\sigma=T(\ulcorner M\urcorner)$.
5. For $M\in\Pi_Y$ (resp. $\Pi_N$) such a stage exists, with answer $1$ (resp. $0$).

Significance

The result. Theorem A.2 is the precise sense in which a semantic property of programs, decidable from the code on a promise, is decidable without the code: running the program on chosen inputs for chosen budgets, plus a bound on its length, suffices. It is the computability-theoretic counterpart of Conjecture 5.2, the complexity-theoretic statement whose failure (Theorem 5.3, under cryptographic assumptions) is one face of the impossibility of obfuscation. Together with Theorem A.4 it isolates the size bound as the ingredient that makes the generalization true.

Formalizing it. The theorem has a complete proof in the paper, about one page long. No machine-checked version is known: the Prove2Me catalogue has classical Rice's Theorem for index sets of Nat.Partrec.Code (FamousTheorems.rice_theorem, which this proof does not use) but nothing on promise problems, bounded-run oracles, or simulators. A formal proof produces reusable infrastructure: the oracle $\langle M\rangle$ as a total function on query codes, decidability of compatibility relative to it, and a dovetailing simulator assembled as a uniform oracle program.

Difficulty

Each mathematical step is elementary; the work lies in the effective content. The obvious idea, "query $\langle M\rangle$ until $[M]$ is known and then decide", fails: $[M]$ is an infinite object, and no finite set of queries pins it down. The paper's simulator instead uses the size bound to restrict attention to finitely many candidate codes, and needs $T$ to agree on every surviving candidate at a common budget. Turning this into one oracle program requires enumerating all codes of a given size, deciding compatibility from finitely many oracle answers, comparing bounded runs of $T$, and searching over $n$, all uniformly in $M$ and with no access to $\ulcorner M\urcorner$. Termination holds only on promise instances, since $T$ may diverge elsewhere, so the argument cannot assume a total decider.

Formalization scope

Machines are Mathlib's Nat.Partrec.Code; descriptions are Encodable.encode; $[M]$ is Code.eval; $\langle M\rangle(1^t,x)$ is Code.evaln t M x : Option ℕ, with none for $\bot$. The budget of evaln is fuel rather than a literal Turing-machine step count. It is monotone in $t$, converges to $[M]$, and is primitive recursive in $(t,M,x)$, and these are the only properties of step counts that the proof uses. Inputs are natural numbers, $|x|$ is Nat.size x, and $|M|$ is Nat.size (encode M). Oracle machines are the published uniform oracle programs FriedbergMuchnik.Program with semantics oracleEval (a single syntax tree with an oracle-query instruction, equivalent to relative partial recursiveness). The oracle $\langle M\rangle$ is the total function sending Nat.pair t x to 0 for $\bot$ and to y + 1 for an output $y$. The simulator's input $1^{|M|}$ is the number $|M|$, since unary versus binary is immaterial here. "$S^{\langle M\rangle}(1^{|M|})=1$" means that the run halts with output $1$. Promise problems carry their disjointness, as in the paper, although no statement uses it. The decider $T$ is a Code applied to descriptions and may diverge off the promise.

The trivializing readings are excluded. $S$ is chosen before $M$ (one program, not one per machine). It receives the size of $M$, never its description, and many machines share each size. It sees only the finitely many oracle answers a halting run queries. The oracle is the bounded-run function $\langle M\rangle$, not $[M]$ or the code.

Contributions welcome: proofs of the milestones; a primitive-recursive enumeration of the codes of a given size; a proof that oracle M is uniformly computable from M, which is useful beyond this mission.

Selected references

• B. Barak, O. Goldreich, R. Impagliazzo, S. Rudich, A. Sahai, S. Vadhan, K. Yang, On the (Im)possibility of Obfuscating Programs, Journal of the ACM 59(2), 2012. https://doi.org/10.1145/2160158.2160159
• H. G. Rice, Classes of recursively enumerable sets and their decision problems, Transactions of the AMS 74(2), 1953. https://doi.org/10.1090/S0002-9947-1953-0053041-6
• S. Even, A. L. Selman, Y. Yacobi, The complexity of promise problems with applications to public-key cryptography, Information and Control 61(2), 1984. https://doi.org/10.1016/S0019-9958(84)80056-X

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

Motivation

Turing reducibility compares sets of natural numbers by their information content: $A\le_TB$ if an oracle Turing machine with oracle $B$ computes the characteristic function of $A$. Identifying mutually reducible sets gives the Turing degrees $\mathcal D_T$, partially ordered by $\le_T$. A central question of computability theory since the 1970s is how much of the underlying computational structure the abstract order remembers. The strongest possible answer is rigidity: the order has no nontrivial automorphisms, so every degree is determined by its position in the order.

Timeline

• 1939. Turing introduces oracle machines and relative computability (doi:10.1112/plms/s2-45.1.161).
• 1977. Jockusch and Solovay prove that every jump-preserving automorphism fixes all degrees above $\mathbf0^{(4)}$ (doi:10.1007/BF03007659).
• 1980. Nerode and Shore prove that every automorphism fixes some cone of degrees, whose base may depend on the automorphism (doi:10.1016/0003-4843(80)90004-2).
• 1999. Shore and Slaman prove that the Turing jump is definable from the order, so every automorphism preserves it (Math. Res. Lett., 1999).
• 2005. Slaman and Woodin's manuscript Definability in Degree Structures shows that every automorphism fixes all degrees above $\mathbf0''$, that the automorphism group is countable, that every automorphism has an arithmetic representation on sets of integers, and that rigidity is equivalent to their biinterpretability conjecture; see also Slaman's survey (doi:10.1142/9789812794055_0002).
• 2007. Shore gives direct degree-theoretic definitions of the jump (J. Math. Log., 2007).
• 2018. Kjos-Hanssen shows that automorphisms induced by permutations of the integers are trivial (doi:10.1017/bsl.2018.15).

After these results the remaining problem was rigidity at degrees outside the known fixed cone. The source of this mission, an OpenAI preprint dated September 24, 2026, proves full rigidity.

Setting

An oracle is a function $A:\mathbb N\to\{0,1\}$ (a set of natural numbers). $A\le_TB$ means that the characteristic function of $A$ is partial recursive relative to $B$. This is a preorder; its quotient by $A\equiv_TB\iff(A\le_TB\wedge B\le_TA)$ is the set $\mathcal D_T$ of Turing degrees, partially ordered by $\le_T$. An automorphism of $(\mathcal D_T,\le_T)$ is a bijection $\pi:\mathcal D_T\to\mathcal D_T$ with

$$\mathbf a\le_T\mathbf b\iff\pi(\mathbf a)\le_T\pi(\mathbf b).$$

No definability, Borel or continuity hypothesis is imposed on $\pi$.

Formalization targets

Goal: Theorem 1.1

$$\forall\pi\in\operatorname{Aut}(\mathcal D_T,\le_T)\ \ \forall\mathbf a\in\mathcal D_T:\qquad \pi(\mathbf a)=\mathbf a.$$

The Lean statement OAI.TuringRigidity.ManuscriptMain.rigidity is open on the platform.

Significance

Rigidity says that the order $\le_T$ alone determines every Turing degree. By the theorem of Slaman and Woodin, it is equivalent to their biinterpretability conjecture: the degrees are biinterpretable without parameters with full second-order arithmetic (Corollary 5.1). Consequently every relation on degrees that is definable in second-order arithmetic and invariant under Turing equivalence is definable in the degree order, which settles a family of definability questions at once.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Its proof relies on the Slaman–Woodin representation theorem, whose cited source is an unpublished 2005 manuscript; a formalization would either need to formalize that input as well or isolate it as an explicit hypothesis, and would make the dependence fully transparent.

Difficulty

Earlier methods fix cones of degrees: coding arguments work above a sufficiently high base such as $\mathbf0''$, where enough information can be coded and decoded. Below that base the coding machinery is not available, and an arbitrary automorphism carries no a priori regularity. The proof must turn the arithmetic (hence Borel) representation of an automorphism into recovery of every individual real, using a category argument that works for every irrational parameter, not only generic ones.

Formalization scope

• Oracles are ℕ → Bool; reducibility is Mathlib's TuringReducible between the characteristic functions viewed as partial functions ℕ →. ℕ (values $0$ and $1$).
• Degree is Antisymmetrization Oracle Reduces with the induced partial order; automorphisms are order isomorphisms Degree ≃o Degree, i.e. bijections preserving and reflecting $\le_T$.
• The statement quantifies over all order isomorphisms, with no measurability or definability assumption, as in the paper.

A complete development needs relativized computability (oracle machines, joins, the jump), Borel and Baire-category arguments on $2^{\mathbb N}$ and $\mathbb R$, and the Slaman–Woodin representation theorem (Theorem 3.1). Formalizing that theorem would itself be a substantial and reusable contribution. Contributions formalizing Proposition 4.1 (recovery of an irrational from four values of a Borel subadditive map with countable fibers) are welcome.

Selected references

• OpenAI, Rigidity of the Turing degrees, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Rigidity-of-the-Turing-degrees-September-24-2026/paper.pdf
• T. A. Slaman, W. H. Woodin, Definability in Degree Structures, unpublished manuscript, 2005. https://math.berkeley.edu/~slaman/talks/sw.pdf
• T. A. Slaman, Global properties of the Turing degrees and the Turing jump, in Computational Prospects of Infinity, Part I, 2008. https://doi.org/10.1142/9789812794055_0002
• C. G. Jockusch, Jr., R. M. Solovay, Fixed points of jump preserving automorphisms of degrees, Israel J. Math., 1977. https://doi.org/10.1007/BF03007659
• A. Nerode, R. A. Shore, Reducibility orderings: theories, definability and automorphisms, Ann. Math. Logic, 1980. https://doi.org/10.1016/0003-4843(80)90004-2
• R. A. Shore, T. A. Slaman, Defining the Turing jump, Math. Res. Lett., 1999.
• R. A. Shore, Direct and local definitions of the Turing jump, J. Math. Log., 2007.
• B. Kjos-Hanssen, Permutations of the integers induce only the trivial automorphism of the Turing degrees, Bull. Symb. Log., 2018. https://doi.org/10.1017/bsl.2018.15
• A. M. Turing, Systems of logic based on ordinals, Proc. London Math. Soc., 1939. https://doi.org/10.1112/plms/s2-45.1.161