Source-game checks using the shared explicit clock

The final decision kernel receives the exponential index and unary clock once. These polynomial-time checks reuse that resource for Sample and cross-Introspect, with precisely the guards of the earlier source compiler.

@[reducible, inline]

abbrev MIPRE.Introspection.ClockedSourceChecks.SampleInput : Type

Equations

• MIPRE.Introspection.ClockedSourceChecks.SampleInput = (MIPRE.Cost.Unary × MIPRE.Cost.Prog × MIPRE.Introspection.AuxiliaryProgram.SamplingInput)

@[reducible, inline]

abbrev MIPRE.Introspection.ClockedSourceChecks.CrossInput : Type

Equations

• MIPRE.Introspection.ClockedSourceChecks.CrossInput = (MIPRE.Cost.Unary × MIPRE.Cost.Prog × MIPRE.Introspection.SourceCompiler.GuardInput)

noncomputable def MIPRE.Introspection.ClockedSourceChecks.sampling (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun SampleInput Bool

The sampling query uses the already reindexed source input.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Introspection.ClockedSourceChecks.sampling_iff (U : Cost.ClockedUniversalMachine) (b : Cost.Unary) (S : Cost.Prog) (x : AuxiliaryProgram.SamplingInput) : (sampling U).toFun (b, S, x) = true ↔ AuxiliaryProgram.SamplingReady x ∧ Cost.clockedResult S (AuxiliaryProgram.samplingCall.toFun x) (List.length b) = AuxiliaryProgram.samplingExpected.toFun x

noncomputable def MIPRE.Introspection.ClockedSourceChecks.cross (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun CrossInput Bool

A source decision call checks both canonical padded questions and all original answer cutoffs before evaluating the bounded source program.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Introspection.ClockedSourceChecks.cross_iff (U : Cost.ClockedUniversalMachine) (b : Cost.Unary) (D : Cost.Prog) (x : SourceCompiler.GuardInput) : (cross U).toFun (b, D, x) = true ↔ SourceCompiler.GuardReady x ∧ Cost.clockedResult D (SourceCompiler.projectedCall.toFun x) (List.length b) = (Cost.encode true).cons (Cost.encode true)

theorem MIPRE.Introspection.ClockedSourceChecks.sampling_eq_program (U : Cost.ClockedUniversalMachine) (k lam n j Q R s : ℕ) (S : Cost.Prog) (w : Bool) (a b : Cost.BitStr) : (sampling U).toFun (Cost.unary (ansBound k lam n), S, j, w, 2 ^ n, Q, R, s, a, b) = true ↔ ∃ (t : ℕ), (AuxiliaryProgram.samplingProg k lam U S).Runs (Cost.encode (j, w, n, Q, R, s, a, b)) (Cost.encode true) t

The shared-clock sampling check is exactly the previously verified clock-computing program, after moving index preparation outside the kernel.

theorem MIPRE.Introspection.ClockedSourceChecks.sampling_depthFamily {ℓ lam n Q R : ℕ} (U : Cost.ClockedUniversalMachine) (V : Verifier ℓ) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hℓ : 1 ≤ ℓ) (hℓR : ℓ.size ≤ (2 ^ n) ^ lam) (hs : V.sampler.dim (2 ^ n) ≤ Q) (hQ : 4 ≤ Q) (hR : 3 * R ≤ Q) (w : Bool) (y z : Fin Q → CL.𝔽₂) (a b : Cost.BitStr) : (sampling U).toFun (Cost.unary (ansBound 5 lam n), V.sampler.prog, ℓ, w, 2 ^ n, Q, R, V.sampler.dim (2 ^ n), AnswerParser.pairBits (CL.toBits y) a, AnswerParser.pairBits (CL.toBits z) b) = true ↔ List.length a ≤ R ∧ List.length b ≤ R ∧ CLChecks.sampling (SourcePadding.depthFamily (AuxiliaryProgram.firstEmbedding hs) (fun (w : Bool) => V.sampler.cl (2 ^ n) (Player.ofBool w)) w) (y, a) (z, b)

Exact full-register Sample semantics for the actual padded source.

theorem MIPRE.Introspection.ClockedSourceChecks.cross_original {ℓ lam n Q : ℕ} (U : Cost.ClockedUniversalMachine) (V : Verifier ℓ) (hV : V.IsBounded lam) (hn : 1 ≤ n) (s : ℕ) (a b : Cost.BitStr) : have x := (2 ^ n, Q, (2 ^ n) ^ lam, s, a, b); (cross U).toFun (Cost.unary (ansBound 5 lam n), V.decider.prog, x) = true ↔ SourceCompiler.GuardReady x ∧ V.decider.Accepts (2 ^ n) (List.take s (SourceCompiler.leftParts.toFun x).1) (List.take s (SourceCompiler.rightParts.toFun x).1) (SourceCompiler.leftParts.toFun x).2 (SourceCompiler.rightParts.toFun x).2

Exact source-game acceptance on the original legal alphabet.