Theorem A.2 (Rice's Theorem, second generalization) — a decidable promise problem closed under $[\cdot]$ is decided by a simulator with $\langle M\rangle$ and $1^{|M|}$

Proved

ObfImpossibility.RiceSimulator.theorem_A_2

by mikedeng1 · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

computabilityoracle-machinesp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1promise-problemsrice-theorem

Let $\Pi=(\Pi_Y,\Pi_N)$ be a promise problem on machines that is closed under $[\cdot]$ (functionally equivalent machines lie in the same parts of $\Pi$ ) and decidable (some machine $T$ outputs $1$ on the description of every $M\in\Pi_Y$ and $0$ on the description of every $M\in\Pi_N$ ). Then there exists a single 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 .

Here $S$ receives only the size $|M|$ of $M$ as input and oracle access to the bounded-run function $\langle M\rangle(1^t,x)$ ; it does not see the description of $M$ . Both equalities include that $S$ halts.

This is the paper's computability-theoretic form of the slogan "the only useful thing you can do with a machine is run it": any semantic property of machines that can be decided from their code, even only on a promise, can already be decided by running the machine on inputs of one's choice for budgets of one's choice, given a bound on its size.

Formalization Note $S$ is a uniform oracle program (FriedbergMuchnik.Program) chosen before $M$ ; $S^{\langle M\rangle}(z)$ is oracleEval with the total oracle oracle M. The input $1^{|M|}$ is passed as the number $|M|$ = Nat.size (encode M) (unary versus binary is immaterial for computability); it is not the description of $M$ , and many machines share each size. $\langle M\rangle(1^t,x)$ is Mathlib's fuel-bounded evaluation Code.evaln t M x.

Preamble

import Mathlib
import Definitions.Def_ObfImpossibility_RiceSimulator_Setting

Formal statement

namespace ObfImpossibility.RiceSimulator

/-- Theorem A.2 (Rice's Theorem — second generalization), p. A:41: if a promise problem
`Π` closed under `[·]` is decidable, then one oracle machine `S` decides it from oracle
access to `⟨M⟩` and the input `|M|`. -/
theorem theorem_A_2 (P : PromiseProblem) (hclosed : P.ClosedUnderFn) (hdec : P.IsDecidable) :
    ∃ S : FriedbergMuchnik.Program,
      (∀ M ∈ P.yes, simRun S M (size M) = Part.some 1) ∧
      (∀ M ∈ P.no, simRun S M (size M) = Part.some 0) := by sorry

end ObfImpossibility.RiceSimulator

Source

Barak et al., On the (Im)possibility of Obfuscating Programs, J. ACM 59(2) (2012), author's copy, p. A:41, Theorem A.2

Human review

Endorsed by Shuze Chen · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem A.2 (Rice's Theorem, second generalization) — a decidable promise problem closed under [⋅][\cdot][⋅] is decided by a simulator with ⟨M⟩\langle M\rangle⟨M⟩ and 1∣M∣1^{|M|}1∣M∣

Theorem A.2 (Rice's Theorem, second generalization) — a decidable promise problem closed under $[\cdot]$ is decided by a simulator with $\langle M\rangle$ and $1^{|M|}$