Bounded-source correctness of the full-register sampling program #
theorem
MIPRE.Introspection.AuxiliaryProgram.marginal_query_size_le
(R : ℕ)
(hR : 1 ≤ R)
(w : Player)
(j : ℕ)
(z : Cost.BitStr)
(hj : j.size ≤ R)
(hz : List.length z ≤ R)
:
theorem
MIPRE.Introspection.AuxiliaryProgram.bounded_marginal_result
{ℓ lam n : ℕ}
(V : Verifier ℓ)
(hV : V.IsBounded lam)
(hn : 1 ≤ n)
(w : Player)
(j : ℕ)
(z : Cost.BitStr)
(hj : 1 ≤ j)
(hjℓ : j ≤ ℓ)
(hjR : j.size ≤ (2 ^ n) ^ lam)
(hz : List.length z = V.sampler.dim (2 ^ n))
:
Cost.clockedResult V.sampler.prog (Cost.encode (2 ^ n, CL.Sampler.Query.marginal w j z)) (ansBound 5 lam n) = (Cost.encode true).cons
(Cost.encode
(CL.toBits ((CL.CLFun.truncate j (V.sampler.cl (2 ^ n) w)).eval (CL.ofBits (V.sampler.dim (2 ^ n)) z))))
A legal marginal query fits the same exponent-five clock as the source decider. Its level enters through the length of its binary encoding.
theorem
MIPRE.Introspection.AuxiliaryProgram.samplingResult_marginal
{ℓ lam n Q R : ℕ}
(V : Verifier ℓ)
(hV : V.IsBounded lam)
(hn : 1 ≤ n)
(hℓ : 1 ≤ ℓ)
(hℓR : ℓ.size ≤ (2 ^ n) ^ lam)
(hQ : V.sampler.dim (2 ^ n) ≤ Q)
(w : Bool)
(y z : Fin Q → CL.𝔽₂)
(a b : Cost.BitStr)
:
samplingResult 5 lam V.sampler.prog
(ℓ, w, n, Q, R, V.sampler.dim (2 ^ n), AnswerParser.pairBits (CL.toBits y) a, AnswerParser.pairBits (CL.toBits z) b) = (Cost.encode true).cons
(Cost.encode (CL.toBits ((V.sampler.cl (2 ^ n) (Player.ofBool w)).eval (CL.pull (firstEmbedding hQ) z))))
theorem
MIPRE.Introspection.AuxiliaryProgram.samplingReady_vectors
{s Q R ℓ : ℕ}
(hℓ : 1 ≤ ℓ)
(hs : s ≤ Q)
(hQ : 4 ≤ Q)
(hR : 3 * R ≤ Q)
(n : ℕ)
(w : Bool)
(y z : Fin Q → CL.𝔽₂)
(a b : Cost.BitStr)
:
SamplingReady (ℓ, w, n, Q, R, s, AnswerParser.pairBits (CL.toBits y) a, AnswerParser.pairBits (CL.toBits z) b) ↔ List.length a ≤ R ∧ List.length b ≤ R ∧ SourceCompiler.InSource s (CL.toBits y) ∧ a = b
theorem
MIPRE.Introspection.AuxiliaryProgram.samplingProg_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)
:
(∃ (t : ℕ),
(samplingProg 5 lam U V.sampler.prog).Runs
(Cost.encode
(ℓ, w, n, Q, R, V.sampler.dim (2 ^ n), AnswerParser.pairBits (CL.toBits y) a, AnswerParser.pairBits (CL.toBits z) b))
(Cost.encode true) t) ↔ List.length a ≤ R ∧ List.length b ≤ R ∧ CLChecks.sampling
(SourcePadding.depthFamily (firstEmbedding hs) (fun (w : Bool) => V.sampler.cl (2 ^ n) (Player.ofBool w)) w)
(y, a) (z, b)
The actual program accepts precisely the full-Q sampling relation for the same-depth padded source CL, on the original answer cutoff. No restriction is placed on the Sample seed's spectator coordinates.