pp. A:41–A:42 — the simulator halts on every instance of the promise

Proved

ObfImpossibility.RiceSimulator.stage_answer_exists

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

computabilityp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1promise-problemsrice-theorem

Let $\Pi=(\Pi_Y,\Pi_N)$ be a promise problem closed under $[\cdot]$ and let $T$ be a machine that decides $\Pi$ . Then:

for every $M\in\Pi_Y$ there is a stage $n$ at which $T$ , run for $n$ steps, halts on every machine of $S_n$ with output $1$ ;
for every $M\in\Pi_N$ there is a stage $n$ at which $T$ , run for $n$ steps, halts on every machine of $S_n$ with output $0$ .

Here $S_n$ is the set of machines of size $|M|$ that are $n$ -compatible with $M$ . In other words, the simulator of Theorem A.2 halts on every promise instance, with the answer $T(\ulcorner M\urcorner)$ . This is the termination half of the proof of Theorem A.2.

Formalization Note The paper says "S always halts"; its argument (and the statement here) covers only $M\in\Pi_Y\cup\Pi_N$ , where $T$ is guaranteed to halt. Outside the promise $T$ , and hence the simulator, may diverge.

Preamble

import Mathlib
import Definitions.Def_ObfImpossibility_RiceSimulator_Setting

Formal statement

namespace ObfImpossibility.RiceSimulator

/-- pp. A:41–A:42: the simulator halts on every instance of the promise: for `M ∈ Π_Y`
(resp. `Π_N`) some stage `n` stops with answer `1` (resp. `0`), the answer of `T(M)`. -/
theorem stage_answer_exists (P : PromiseProblem) (hclosed : P.ClosedUnderFn)
    (T : Machine) (hT : Decides T P) :
    (∀ M ∈ P.yes, ∃ n : ℕ, StageAnswer T M n 1) ∧
    (∀ M ∈ P.no, ∃ n : ℕ, StageAnswer T M n 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, pp. A:41–A:42, proof of 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