Prove2Me

Proof of Thm A.4, p. A:42 — a halting run S⟨M0⟩()S^{\langle M_0\rangle}() only sees queries with t,∣x∣≤nt,|x|\le n

Proved
ObfImpossibility.RiceNoSize.finite_queries

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

computabilityoracle-machinesp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let SS be an oracle machine and M0M_0 a machine such that S⟨M0⟩()S^{\langle M_0\rangle}() halts with output σ\sigma. Then there is an nn bounding tt and ∣x∣|x| over the queries (1t,x)(1^t,x) that matter, in the following sense: for every machine MM,

(∀t,x≤n: ⟨M⟩(1t,x)=⟨M0⟩(1t,x))  ⟹  S⟨M⟩()=σ.\Big(\forall t,x\le n:\ \langle M\rangle(1^t,x)=\langle M_0\rangle(1^t,x)\Big)\;\Longrightarrow\; S^{\langle M\rangle}()=\sigma .

In the proof of Theorem A.4 this is applied with M0=ZM_0=Z and σ=0\sigma=0: the halting run of SS on ZZ asks only finitely many queries, so any machine with the same bounded behaviour on those queries receives the same answer from SS.

Formalization Note The statement holds for every oracle program and every machine; it is the "use principle" of oracle computation specialised to the oracle ⟨⋅⟩\langle\cdot\rangle. Queries are coded as Nat.pair t x.

Preamble
import Mathlib
import Definitions.Def_ObfImpossibility_RiceNoSize_ProofObjects
Formal statement
namespace ObfImpossibility.RiceNoSize

/-- p. A:42: a halting run `S^{⟨M₀⟩}() = σ` makes oracle queries `(1^t, x)` with `t` and `|x|`
bounded by some `n`; hence every machine `M` with `⟨M⟩(1^t, x) = ⟨M₀⟩(1^t, x)` for all
`t, |x| ≤ n` also has `S^{⟨M⟩}() = σ`. -/
theorem finite_queries (S : FriedbergMuchnik.Program) (M₀ : Machine) (σ : ℕ)
    (h : simRun S M₀ = Part.some σ) :
    ∃ n : ℕ, ∀ M : Machine,
      (∀ t x : ℕ, t ≤ n → x ≤ n → bounded M t x = bounded M₀ t x) →
      simRun S M = Part.some σ := by sorry

end ObfImpossibility.RiceNoSize
Source
Barak et al., On the (Im)possibility of Obfuscating Programs, J. ACM 59(2) (2012), author's copy, p. A:42, proof of Theorem A.4 ("Let n be an upper bound on |x| and t over all oracle queries (1^t, x) of S^⟨Z⟩().")
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