p. A:41 — if the simulator halts, it returns the same answer as $T(M)$

Proved

ObfImpossibility.RiceSimulator.stage_answer_sound

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

computabilityp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1rice-theorem

Let $T$ and $M$ be machines, $n\in\mathbb N$ and $\sigma\in\mathbb N$ . Suppose stage $n$ of the simulator stops with answer $\sigma$ , that is, $T$ run for $n$ steps halts on every machine of $S_n$ (the machines of size $|M|$ that are $n$ -compatible with $M$ ) with output $\sigma$ . Then

T(\ulcorner M\urcorner)=\sigma .

Since $M$ is $n$ -compatible with itself, $M$ always belongs to $S_n$ ; so whatever stage the simulator stops at, its answer is the one $T$ gives on $M$ . This is the correctness half of the proof of Theorem A.2.

Formalization Note "Run $T$ for $n$ steps" is Code.evaln n T; the conclusion is σ ∈ Code.eval T (encode M), i.e. $T$ halts on $\ulcorner M\urcorner$ with output $\sigma$ . No promise hypothesis is needed.

Preamble

import Mathlib
import Definitions.Def_ObfImpossibility_RiceSimulator_Setting

Formal statement

namespace ObfImpossibility.RiceSimulator

/-- p. A:41: if the simulator halts (at some stage `n` with answer `σ`) then it returns the
same answer as `T(M)`. -/
theorem stage_answer_sound (T M : Machine) (n σ : ℕ) (h : StageAnswer T M n σ) :
    σ ∈ T.eval (Encodable.encode M) := 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, 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

p. A:41 — if the simulator halts, it returns the same answer as T(M)T(M)T(M)

p. A:41 — if the simulator halts, it returns the same answer as $T(M)$