Fact (1), p. A:41 — $n$ -compatibility with $M$ is decidable with oracle access to $\langle M\rangle$

Proved

ObfImpossibility.RiceSimulator.fact_1_compatibility_decidable

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

computabilityoracle-machinesp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1rice-theorem

Let $M$ and $N$ be machines and $n\in\mathbb N$ , and recall that $N$ is $n$ -compatible with $M$ when $\langle N\rangle(1^t,x)=\langle M\rangle(1^t,x)$ for all $t\le n$ and all inputs $x$ with $|x|\le n$ .

There is a single oracle machine $C$ that decides $n$ -compatibility with $M$ using only oracle access to $\langle M\rangle$ : for all machines $M$ , $N$ and all $n$ ,

C^{\langle M\rangle}(n,\ulcorner N\urcorner)=\begin{cases}1 & \text{if } N \text{ is } n\text{-compatible with } M,\\ 0 & \text{otherwise.}\end{cases}

In particular $C$ halts on every input.

This is fact (1) in the proof of Theorem A.2: the simulator built there recomputes the set $S_n$ of machines of size $|M|$ that are $n$ -compatible with $M$ at every stage, and this is the uniform procedure that does it.

Formalization Note The pair $(n,\ulcorner N\urcorner)$ is passed as Nat.pair n (encode N). The same program $C$ must work for every $M$ , $N$ , $n$ (the existential quantifier precedes them), so the statement asserts uniform computability relative to the oracle, not a per-instance property.

Preamble

import Mathlib
import Definitions.Def_ObfImpossibility_RiceSimulator_Setting

Formal statement

namespace ObfImpossibility.RiceSimulator

/-- Fact (1), p. A:41: `n`-compatibility with `M` can be decided using oracle access to `⟨M⟩`,
by one oracle machine `C` that works for every `M`, on input the pair `(n, N)`. -/
theorem fact_1_compatibility_decidable :
    ∃ C : FriedbergMuchnik.Program, ∀ (M N : Machine) (n : ℕ),
      (Compatible n N M → simRun C M (Nat.pair n (Encodable.encode N)) = Part.some 1) ∧
      (¬ Compatible n N M → simRun C M (Nat.pair n (Encodable.encode N)) = 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, proof of Theorem A.2, fact (1)

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

Fact (1), p. A:41 — nnn-compatibility with MMM is decidable with oracle access to ⟨M⟩\langle M\rangle⟨M⟩

Fact (1), p. A:41 — $n$ -compatibility with $M$ is decidable with oracle access to $\langle M\rangle$