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

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

Volume-preserving box transport supplies geometric operations for a finite computation. The selected goal assembles these into a force and a fixed particle observer. The pinned manuscript supplies the research context.

Setting

A finite machine and input determine effective velocity and force coefficients. The force depends affinely on positive viscosity, and after time one the velocity is periodic and depends only on the machine.

Formalization target

The selected goal is OAI.BalancedTransport.balanced_three_stack_realization. Its central assertion is

$$\exists t\geq0:\ X(t,(4,0,0))\in(-1,2)^3\quad\Longleftrightarrow\quad M\text{ halts on }w.$$

The theorem states that there exist velocity fields U(M,w), force coefficients f₀(M,w) and f₁(M,w), material flows X(M,w), and a globally 1-periodic velocity field R(M) for each finite deterministic tape machine M, with the following properties for every finite input word w. On nonnegative time and ℝ³, U, f₀ and f₁ are smooth and vanish outside a common spatial compact set independent of time; every mixed space-time derivative of U is uniformly bounded. Moreover, f₀ = ∂ₜU + (U·∇)U and f₁ = −ΔU. All three families are uniformly effective from the encoded machine and input: algorithms approximate every mixed derivative component at rational space-time points within 2⁻ⁿ, provide global integer bounds on these derivatives, and provide integer support radii. The velocity is 1-periodic after time 1 and satisfies U(M,w)(t,x) = R(M)(t,x) for every t ≥ 1, so its later field depends only on M. The flow satisfies X(0,a) = a and ∂ₜX(t,a) = U(t,X(t,a)); its trajectory starting at (4,0,0) enters (−1,2)³ at some nonnegative time exactly when M halts on w, meaning that a configuration with no next transition is reached after finitely many machine steps. For every viscosity ν > 0, the force f = f₀ + νf₁ is smooth, has uniformly bounded mixed derivatives, and is 1-periodic after time 1; U with pressure zero solves the incompressible Navier–Stokes equation ∂ₜU + (U·∇)U = νΔU + f with U(0,·) = 0. This velocity is unique among smooth zero-data solutions in the comparison class, and every such solution has spatially constant pressure. The comparison class requires the velocity and all spatial derivatives through order two to be continuous in time as L² functions, the velocity to be continuously differentiable in time in L², velocity and first spatial derivatives to be bounded on each finite time slab, and pressure, after subtracting a time-dependent scalar, together with its first spatial derivatives to be continuous in time in L²; (U,0) belongs to this class. Finally, derivative approximations and global derivative bounds for f are computable when ν is computable, and computable relative to any rational name of ν whose nth approximation has error at most 2⁻ⁿ.

Significance and status

The balanced three-stack realization is the main goal; balanced box routing is a separate supporting reference. The exact conclusion permits spatially constant pressure in competing solutions and explicitly states its comparison class. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

Uniform effectiveness, compact support, periodic behavior and uniqueness must all coexist with exact halting detection.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

• OAI.BoxTransport.Routing.balanced_box_routing (Open).

Selected references

• OpenAI, Incompressible Box Transport and Finite Computation, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

A force whose derivatives decay rapidly can still encode a computation in a particle trajectory. The selected construction makes the observer condition and effectiveness requirements precise. The pinned manuscript supplies the research context.

Setting

For each finite deterministic machine and valid input, compilers produce smooth force and velocity fields on nonnegative time and real three-space, with common compact spatial support.

Formalization target

The selected goal is OAI.AlternatingNS.alternating. Its central assertion is

$$\exists t\geq0:\ X_1(t)>0\quad\Longleftrightarrow\quad M\text{ halts on }w.$$

The theorem states that for every positive real viscosity ν computable by rational approximations with error at most 2⁻ⁿ, there exist computable compilers for a force f and velocity U, and one compact set K⊂ℝ³, with the following property for every well-formed finite deterministic Turing machine M and valid finite input w. The compiled programs describe smooth fields f,U on [0,∞)×ℝ³, both spatially supported in K for all nonnegative times, such that every mixed space-time derivative D satisfies sup_{t≥0,x}(1+t+‖x‖)ᴶ‖Df(t,x)‖<∞ and the analogous bound for U, for every nonnegative integer J. Each program supplies rational approximations to all mixed derivatives at rational space-time points with requested error 2⁻ᵏ, effective moduli of continuity on bounded regions, and integer bounds for all these weighted derivative norms. The velocity starts from zero, is divergence-free, and solves the classical forced Navier–Stokes equation ∂ₜU+(U·∇)U=νΔU+f with identically zero pressure; specifically f=∂ₜU+(U·∇)U−νΔU. On every interval [0,T], U is continuous in H² and continuously differentiable in L², and U and its spatial derivative are uniformly bounded in space and time. Moreover, any classical solution (v,p) with the same force and zero initial velocity equals (U,0) pointwise for all nonnegative times, provided on every [0,T] it has v continuous in H², continuously differentiable in L², and uniformly bounded, and p continuous in H¹. Here these Sobolev continuity conditions mean continuous L² representatives of every spatial derivative through the indicated order; time derivatives at zero are taken within [0,∞). Every initial point a has a unique trajectory X(a,t) for t≥0 satisfying X(a,0)=a and ∂ₜX(a,t)=U(t,X(a,t)). Finally, the trajectory starting at (−1,0,0) has strictly positive first coordinate at some nonnegative time if and only if M halts on w, where encountering a missing instruction also counts as halting.

Significance and status

The goal is the alternating-coordinate construction at every positive computable viscosity. It includes Sobolev time regularity, effective bounds, zero initial velocity and the exact observer condition, rather than all three manuscript constructions. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The encoding must preserve all weighted derivative bounds and uniqueness in the stated comparison class while recording arbitrarily long computations.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, Computation under Rapidly Vanishing Navier–Stokes Forcing, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Incompressible transport can implement prescribed geometric operations on coding sheets. The selected statement concerns one such finite transport construction with effective smooth forcing. The pinned manuscript supplies the research context.

Setting

Source and target rectangles have rational data and specified positive diagonal ratios. In the formula, D_i(y)=q_i+diag(r_i)(y−p_i), with source and target centers p_i and q_i. Space is represented periodically with period ten, and the viscosity is a positive computable real.

Formalization target

The selected goal is OAI.Solenoidal.sheet_theorem. Its central assertion is

$$X(1,\mathrm{sheet}(y))=\mathrm{sheet}(D_i y)\pmod{(10\mathbb Z)^3}.$$

The theorem states that, for any natural number N, any sheet datum D of size N, and any computable real viscosity ν>0, there exist a forcing field f and a velocity field u (each a time-dependent vector field on ℝ³) and a flow map X such that the following hold. Here D consists of N source rectangles and N target rectangles with rational corners, all inside the square [2,3]², with the sources pairwise separated by a positive distance and likewise the targets, together with positive rational ratios in each of two coordinates such that the diagonal affine map from source i to target i, which sends the source center to the target center and scales offsets by the ratios, maps the source rectangle exactly onto the target rectangle. Both f and u are periodic in space with period 10 in every coordinate and are C^∞ in space and time jointly. The forcing f is effective, meaning that all its mixed space-time partial derivatives can be approximated to any rational accuracy by a single fixed partial recursive procedure from computable names of the evaluation point. Moreover f has zero mean over the fundamental cell [0,10)³ at every time, is divergence free, and is 1-periodic in time. The field u is a classical solution on t≥0 of the forced Navier–Stokes equations ∂ₜu + (u·∇)u = −∇p + ν Δu + f with zero pressure, zero initial data, incompressibility and spatial periodicity, so u is a solution driven by f without pressure. Any classical solution v with pressure p for the same f and ν and with zero initial velocity coincides with u, and has p identically zero, for all t≥0. The flow map X satisfies X(0,a)=a and solves the particle-path equation dX/dt=u(t,X) for t≥0, and for each i and each point y of the i-th source rectangle, the time-1 flow image of the sheet point (y₀,y₁,2) agrees modulo the torus ℝ³/(10ℤ)³ with the sheet point at the diagonal-map image of y. Further, u vanishes in a neighborhood of every integer time, the advection term (u·∇)u vanishes everywhere, and both f and u have all their mixed space-time derivatives uniformly bounded by rational bounds computable from the derivative multi-index by a fixed partial recursive procedure. Finally, if N=0 then f and u are identically zero.

Significance and status

The target is the sheet theorem, including its encoded uniqueness statement and zero-advection conditions. Machine-halting detection is not a conclusion of this published goal. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The construction must simultaneously enforce smoothness, incompressibility, temporal periodicity, effective bounds and exact transport on every point of each sheet rectangle.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, Geometric Programs for Solenoidal Forcing, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

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