The repeated sampler

The sampler of ComputeParrepVerifier (thm:parallel-repetition) as a CL.Sampler: on an ℓ-level sampler S with dimension s(n) and parameters (λ, τ), the sampler of dimension k(n) s(n), k(n) = 2^{τ(|λ| + |n|)} (MIPRE.Repetition.reps), whose CL functions are the k(n)-fold direct sums CLFun.famSum of those of S, and whose program is the fixed core Prog.repSampCore of MIPRE.Foundations.Repeat.Sampler, run through the self-interpreter selfUniversal and the s-m-n construction hardcode on (S.prog, λ, τ) (planning/repetition-verifier.md, R3(b)).

The correctness clauses reduce to those of S on the blocks of the query (Bits.lean), the halting clause to the case analysis repSampCore_runs_any on the shape of the query, which also carries the explicit cost used by the time bound (MIPRE.Foundations.Repeat.SamplerCost).

theorem MIPRE.Repeat.exists_uniform_bound {α : Type u_1} (L : List α) (Q : α → ℕ → Prop) (h : ∀ a ∈ L, ∃ (t : ℕ), Q a t) : ∃ (T : ℕ), ∀ a ∈ L, ∃ t ≤ T, Q a t

A finite list of halting runs halts within a common bound.

Halting on every query

def MIPRE.Repeat.blockQueries (s : ℕ) : Cost.Data → List Cost.Data

The block queries the core asks S̄ on the query datum d, at dimension s: for a query (kind, w, j, u, y) of nonzero kind and s > 0, the queries (kind, w, j, blockU, blockY) on the pairs of blocks; none otherwise.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Repeat.blockQueries s x✝ = []

theorem MIPRE.Repeat.lockProg_runs_malformed (univ : Cost.Prog) (sD nD sz kD qr : Cost.Data) (h : qr = Cost.Data.nil ∨ (∃ (wD : Cost.Data), qr = wD.cons Cost.Data.nil) ∨ ∃ (wD : Cost.Data) (jD : Cost.Data), qr = wD.cons (jD.cons Cost.Data.nil)) : ∃ t ≤ 8, Cost.Eval [sD.cons (nD.cons (sz.cons (kD.cons qr)))] univ.lockProg Cost.Data.nil t

theorem MIPRE.Repeat.lockCost_mono {s C C' U U' Y Y' Z : ℕ} (hC : C ≤ C') (hU : U ≤ U') (hY : Y ≤ Y') : Cost.Prog.lockCost s C U Y Z ≤ Cost.Prog.lockCost s C' U' Y' Z

theorem MIPRE.Repeat.encode_nat_zero : Cost.encode 0 = Cost.Data.nil

theorem MIPRE.Repeat.dimProg_runs_encode (lam tau n s : ℕ) : ∃ t ≤ Cost.Prog.dimCost tau (lam.size + n.size) (Cost.esize lam) (Cost.esize n) (Cost.esize s) + 3, Cost.Eval [(Cost.encode s).cons ((Cost.encode lam).cons ((Cost.encode n).cons (Cost.encode tau)))] Cost.Prog.dimProg (Cost.encode (2 ^ (tau * (lam.size + n.size)) * s)) t

The dimension branch on (s, λ, n, τ), s in binary: the numeral 2^{τ(|λ| + |n|)} s.

def MIPRE.Repeat.zBound (sD : Cost.Data) (n s D Tu : ℕ) : ℕ

A bound on the sizes in the block loop of the core on a query of size D.

Equations

• MIPRE.Repeat.zBound sD n s D Tu = s + 3 * D + (sD.size + MIPRE.Cost.esize n + D + 4) + 1 + D * (Tu + 1) + Tu

def MIPRE.Repeat.anyCost (lam tau n : ℕ) (sD : Cost.Data) (s D td Tu : ℕ) : ℕ

The cost of the core on a query of size D at index n, with the dimension query answered in time td and each block query in time Tu: the sum of the branches' bounds.

Equations

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

theorem MIPRE.Repeat.repSampCore_runs_any {univ : Cost.Prog} (hU : Cost.Prog.WellScoped 1 univ) (sD : Cost.Data) (lam tau n s : ℕ) (d : Cost.Data) {td : ℕ} (hdim : Cost.Eval [sD.cons ((Cost.encode n).cons (Cost.encode CL.Sampler.Query.dimension))] univ (Cost.encode s) td) (fq : Cost.Data → Cost.Data) (Tu : ℕ) (hq : ∀ q ∈ blockQueries s d, ∃ t ≤ Tu, Cost.Eval [sD.cons ((Cost.encode n).cons q)] univ (fq q) t) : ∃ (r : Cost.Data), ∃ t ≤ anyCost lam tau n sD s d.size td Tu, Cost.Eval [(Cost.Prog.sampParams sD (Cost.encode lam) (Cost.encode tau)).cons ((Cost.encode n).cons d)] univ.repSampCore r t

The core halts on every query, within anyCost, given the dimension of S̄ at n and the answers of S̄ on the block queries.

The sampler

noncomputable def MIPRE.Repeat.repSamplerProg (sp : Cost.Prog) (lam tau : ℕ) : Cost.Prog

The program of the repeated sampler on (S̄, λ, τ): the core, hardcoded.

Equations

• MIPRE.Repeat.repSamplerProg sp lam tau = MIPRE.Cost.hardcode MIPRE.Cost.selfUniversal.univ.repSampCore (MIPRE.Cost.encode (sp, lam, tau))

theorem MIPRE.Repeat.repSamplerProg_wellScoped (sp : Cost.Prog) (lam tau : ℕ) : Cost.Prog.WellScoped 1 (repSamplerProg sp lam tau)

theorem MIPRE.Repeat.repSamplerProg_runs (sp : Cost.Prog) (lam tau n : ℕ) (d : Cost.Data) {r : Cost.Data} {t : ℕ} (h : Cost.Eval [(Cost.Prog.sampParams (Cost.encode sp) (Cost.encode lam) (Cost.encode tau)).cons ((Cost.encode n).cons d)] Cost.selfUniversal.univ.repSampCore r t) : (repSamplerProg sp lam tau).Runs ((Cost.encode n).cons d) r (t + (Cost.encode (sp, lam, tau)).size + ((Cost.encode n).cons d).size + 3)

theorem MIPRE.Repeat.dim_call {ℓ : ℕ} (S : CL.Sampler ℓ) (n : ℕ) : ∃ (td : ℕ), Cost.Eval [(Cost.encode S.prog).cons ((Cost.encode n).cons (Cost.encode CL.Sampler.Query.dimension))] Cost.selfUniversal.univ (Cost.encode (S.dim n)) td

The dimension query to S, through the universal machine.

theorem MIPRE.Repeat.block_call {ℓ : ℕ} (S : CL.Sampler ℓ) (n : ℕ) (q : Cost.Data) : ∃ (r : Cost.Data) (t : ℕ), Cost.Eval [(Cost.encode S.prog).cons ((Cost.encode n).cons q)] Cost.selfUniversal.univ r t

Any block query to S, through the universal machine, halts with S's own result.

theorem MIPRE.Repeat.repSampler_halts {ℓ : ℕ} (S : CL.Sampler ℓ) (lam tau n : ℕ) (d : Cost.Data) : Cost.Halts (repSamplerProg S.prog lam tau) ((Cost.encode n).cons d)

The repeated sampler halts on every input.

theorem MIPRE.Repeat.univ_call {ℓ : ℕ} (S : CL.Sampler ℓ) (n : ℕ) (q r : Cost.Data) {t : ℕ} (h : S.prog.Runs ((Cost.encode n).cons q) r t) : ∃ (t' : ℕ), Cost.Eval [(Cost.encode S.prog).cons ((Cost.encode n).cons q)] Cost.selfUniversal.univ r t'

The universal machine on a block query, from S's answer.

theorem MIPRE.Repeat.repSampler_runs_dimension {ℓ : ℕ} (S : CL.Sampler ℓ) (lam tau n : ℕ) : ∃ (t : ℕ), (repSamplerProg S.prog lam tau).Runs (Cost.encode (n, CL.Sampler.Query.dimension)) (Cost.encode (Repetition.reps lam tau n * S.dim n)) t

The dimension query.

theorem MIPRE.Repeat.lockProg_runs_blocks {univ : Cost.Prog} (hU : Cost.Prog.WellScoped 1 univ) {s : ℕ} (hs : 0 < s) (sD nD kD wD jD : Cost.Data) (k : ℕ) (z y' : Cost.BitStr) (hz : List.length z = k * s) (g : Cost.BitStr → Cost.BitStr → Cost.BitStr) (hg : ∀ (i : Fin k), ∃ (t : ℕ), Cost.Eval [Cost.Prog.mapQuery sD nD kD wD jD (Cost.encode (Cost.Data.chunk s (↑i) z)) (Cost.encode (Cost.Data.chunk s (↑i) y'))] univ (Cost.encode (g (Cost.Data.chunk s (↑i) z) (Cost.Data.chunk s (↑i) y'))) t) : ∃ (t : ℕ), Cost.Eval [Cost.Prog.lockInput sD nD (Cost.encode s) kD wD jD (Cost.encode z) (Cost.encode y')] univ.lockProg (Cost.encode (List.ofFn fun (i : Fin k) => g (Cost.Data.chunk s (↑i) z) (Cost.Data.chunk s (↑i) y')).flatten) t

lockProg on well-formed blocks: with g the answer of S̄ on a pair of blocks, the concatenation of the answers on the k pairs.

theorem MIPRE.Repeat.repSampler_runs_of_lock {ℓ : ℕ} (S : CL.Sampler ℓ) (lam tau n : ℕ) (k₀ k₁ qr : Cost.Data) {r : Cost.Data} {t td : ℕ} (hdim : Cost.Eval [(Cost.encode S.prog).cons ((Cost.encode n).cons (Cost.encode CL.Sampler.Query.dimension))] Cost.selfUniversal.univ (Cost.encode (S.dim n)) td) (run : Cost.Eval [(Cost.encode S.prog).cons ((Cost.encode n).cons ((Cost.encode (S.dim n)).cons ((k₀.cons k₁).cons qr)))] Cost.selfUniversal.univ.lockProg r t) : ∃ (t' : ℕ), (repSamplerProg S.prog lam tau).Runs ((Cost.encode n).cons ((k₀.cons k₁).cons qr)) r t'

The run of the repeated sampler on a query of nonzero kind, from a run of lockProg.

theorem MIPRE.Repeat.encode_nat_one : Cost.encode 1 = (Cost.Data.nil.cons Cost.Data.nil).cons Cost.Data.nil

theorem MIPRE.Repeat.encode_nat_two : Cost.encode 2 = Cost.Data.nil.cons ((Cost.Data.nil.cons Cost.Data.nil).cons Cost.Data.nil)

theorem MIPRE.Repeat.encode_nat_three : Cost.encode 3 = (Cost.Data.nil.cons Cost.Data.nil).cons ((Cost.Data.nil.cons Cost.Data.nil).cons Cost.Data.nil)

theorem MIPRE.Repeat.encode_marginal (n : ℕ) (w : Player) (j : ℕ) (z : Cost.BitStr) : Cost.encode (n, CL.Sampler.Query.marginal w j z) = (Cost.encode n).cons (((Cost.Data.nil.cons Cost.Data.nil).cons Cost.Data.nil).cons ((Cost.encode w).cons ((Cost.encode j).cons ((Cost.encode z).cons Cost.Data.nil))))

theorem MIPRE.Repeat.encode_linear (n : ℕ) (w : Player) (j : ℕ) (u y : Cost.BitStr) : Cost.encode (n, CL.Sampler.Query.linear w j u y) = (Cost.encode n).cons ((Cost.Data.nil.cons ((Cost.Data.nil.cons Cost.Data.nil).cons Cost.Data.nil)).cons ((Cost.encode w).cons ((Cost.encode j).cons ((Cost.encode u).cons (Cost.encode y)))))

theorem MIPRE.Repeat.encode_factor (n : ℕ) (w : Player) (j : ℕ) (u : Cost.BitStr) : Cost.encode (n, CL.Sampler.Query.factor w j u) = (Cost.encode n).cons (((Cost.Data.nil.cons Cost.Data.nil).cons ((Cost.Data.nil.cons Cost.Data.nil).cons Cost.Data.nil)).cons ((Cost.encode w).cons ((Cost.encode j).cons ((Cost.encode u).cons Cost.Data.nil))))

theorem MIPRE.Repeat.repSampler_runs_marginal {ℓ : ℕ} (S : CL.Sampler ℓ) (lam tau n : ℕ) (w : Player) (j : ℕ) (z : Cost.BitStr) (hj : 1 ≤ j) (hj' : j ≤ ℓ) (hz : List.length z = Repetition.reps lam tau n * S.dim n) : ∃ (t : ℕ), (repSamplerProg S.prog lam tau).Runs (Cost.encode (n, CL.Sampler.Query.marginal w j z)) (Cost.encode (CL.toBits ((CL.CLFun.truncate j (CL.CLFun.famSum finProdFinEquiv ℓ fun (x : Fin (Repetition.reps lam tau n)) => S.cl n w)).eval (CL.ofBits (Repetition.reps lam tau n * S.dim n) z)))) t

The marginal query.

theorem MIPRE.Repeat.chunk_toBits_truncate {ℓ : ℕ} (S : CL.Sampler ℓ) (lam tau n : ℕ) (w : Player) (j : ℕ) (u : Cost.BitStr) (hu : ∃ (x : Fin (Repetition.reps lam tau n * S.dim n) → CL.𝔽₂), u = CL.toBits ((CL.CLFun.truncate j (CL.CLFun.famSum finProdFinEquiv ℓ fun (x : Fin (Repetition.reps lam tau n)) => S.cl n w)).eval x)) : List.length u = Repetition.reps lam tau n * S.dim n ∧ ∀ (i : Fin (Repetition.reps lam tau n)), ∃ (x : Fin (S.dim n) → CL.𝔽₂), Cost.Data.chunk (S.dim n) (↑i) u = CL.toBits ((CL.CLFun.truncate j (S.cl n w)).eval x)

The blocks of a string in the image of a truncation of the direct sum are in the images of the truncations of the summands.

theorem MIPRE.Repeat.repSampler_runs_linear {ℓ : ℕ} (S : CL.Sampler ℓ) (lam tau n : ℕ) (w : Player) (j : ℕ) (u y : Cost.BitStr) (hj : 1 ≤ j) (hj' : j ≤ ℓ) (hu : ∃ (x : Fin (Repetition.reps lam tau n * S.dim n) → CL.𝔽₂), u = CL.toBits ((CL.CLFun.truncate (j - 1) (CL.CLFun.famSum finProdFinEquiv ℓ fun (x : Fin (Repetition.reps lam tau n)) => S.cl n w)).eval x)) (hy : List.length y = Repetition.reps lam tau n * S.dim n) : ∃ (t : ℕ), (repSamplerProg S.prog lam tau).Runs (Cost.encode (n, CL.Sampler.Query.linear w j u y)) (Cost.encode (CL.toBits (((CL.CLFun.famSum finProdFinEquiv ℓ fun (x : Fin (Repetition.reps lam tau n)) => S.cl n w).mapOfPrefix (j - 1) (CL.ofBits (Repetition.reps lam tau n * S.dim n) u)) (CL.ofBits (Repetition.reps lam tau n * S.dim n) y)))) t

The linear query.

theorem MIPRE.Repeat.repSampler_runs_factor {ℓ : ℕ} (S : CL.Sampler ℓ) (lam tau n : ℕ) (w : Player) (j : ℕ) (u : Cost.BitStr) (hj : 1 ≤ j) (hj' : j ≤ ℓ) (hu : ∃ (x : Fin (Repetition.reps lam tau n * S.dim n) → CL.𝔽₂), u = CL.toBits ((CL.CLFun.truncate (j - 1) (CL.CLFun.famSum finProdFinEquiv ℓ fun (x : Fin (Repetition.reps lam tau n)) => S.cl n w)).eval x)) : ∃ (t : ℕ), (repSamplerProg S.prog lam tau).Runs (Cost.encode (n, CL.Sampler.Query.factor w j u)) (Cost.encode (CL.indicatorBits ((CL.CLFun.famSum finProdFinEquiv ℓ fun (x : Fin (Repetition.reps lam tau n)) => S.cl n w).factorOfPrefix (j - 1) (CL.ofBits (Repetition.reps lam tau n * S.dim n) u)))) t

The factor query.

noncomputable def MIPRE.Repeat.repSampler {ℓ : ℕ} (S : CL.Sampler ℓ) (lam tau : ℕ) : CL.Sampler ℓ

The repeated sampler (ComputeParrepVerifier, sampler half): k(n) independent copies of S, k(n) = 2^{τ(|λ| + |n|)}.

Equations

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

@[simp]

theorem MIPRE.Repeat.repSampler_prog {ℓ : ℕ} (S : CL.Sampler ℓ) (lam tau : ℕ) : (repSampler S lam tau).prog = repSamplerProg S.prog lam tau

@[simp]

theorem MIPRE.Repeat.repSampler_dim {ℓ : ℕ} (S : CL.Sampler ℓ) (lam tau n : ℕ) : (repSampler S lam tau).dim n = Repetition.reps lam tau n * S.dim n