The repeated answer-length calculator

The answer-length calculator of the repeated tailored verifier (issue #280, P2b), on (n, x, κ), with the input sampler S̄ and calculator L̄ and the parameters (λ, τ) stored:

1. ask S̄ for the dimension s = s(n), and put it in unary;
2. compute k = k(n) = Repetition.reps λ τ n in unary (dimProg on 1, then to unary);
3. cut x into its k blocks of s bits, and run L̄ on (n, xᵢ, κ') for every block and both kinds κ';
4. output the concatenation of the outputs at the kind κ, whose length is the sum of the coordinates' lengths.

It runs L̄ on both kinds so that it halts only where every coordinate has both its lengths (RepSpec.good_of_len). Every stage between the calls is a PolyTimeFun; the calls go through Calls.mapCall.

theorem MIPRE.Tailored.RepProg.rawList_eq_spineList (d : Cost.Data) : CL.Detyping.Program.rawList d = d.spineList

The stages

@[reducible, inline]

abbrev MIPRE.Tailored.RepProg.LenPar : Type

The stored data of the calculator: (S̄, L̄, λ, τ).

Equations

• MIPRE.Tailored.RepProg.LenPar = (MIPRE.Cost.Prog × MIPRE.Cost.Prog × ℕ × ℕ)

@[reducible, inline]

abbrev MIPRE.Tailored.RepProg.LenIn : Type

The input of the core: the stored data and (n, d).

Equations

• MIPRE.Tailored.RepProg.LenIn = (MIPRE.Tailored.RepProg.LenPar × ℕ × MIPRE.Cost.Data)

noncomputable def MIPRE.Tailored.RepProg.dimQueryF {ι : Type} [Cost.SizedEncoding ι] (nF : Cost.PolyTimeFun ι ℕ) : Cost.PolyTimeFun ι Cost.Data

The dimension query (n, dimension).

Equations

• MIPRE.Tailored.RepProg.dimQueryF nF = MIPRE.CL.Detyping.Program.encoded.comp (nF.pair (MIPRE.Cost.PolyTimeFun.const MIPRE.CL.Sampler.Query.dimension))

noncomputable def MIPRE.Tailored.RepProg.lenA : Cost.PolyTimeFun LenIn (LenIn × Cost.Prog × List Cost.Data)

Stage 1: the call to S̄ on the dimension query.

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.lenA_apply (a : LenIn) : lenA.toFun a = (a, a.1.1, [Cost.encode (a.2.1, CL.Sampler.Query.dimension)])

noncomputable def MIPRE.Tailored.RepProg.lenB : Cost.PolyTimeFun (LenIn × List Cost.Data) (LenIn × ℕ)

Stage 2: read the dimension.

Equations

• MIPRE.Tailored.RepProg.lenB = MIPRE.Cost.PolyTimeFun.fst.pair (MIPRE.CL.Detyping.Program.readNat.comp ((MIPRE.Cost.PolyTimeFun.headD MIPRE.Cost.Data.nil).comp MIPRE.Cost.PolyTimeFun.snd))

@[simp]

theorem MIPRE.Tailored.RepProg.lenB_apply (p : LenIn × List Cost.Data) : lenB.toFun p = (p.1, CL.Detyping.Program.readNat.toFun (p.2.headD Cost.Data.nil))

noncomputable def MIPRE.Tailored.RepProg.lenC : Cost.PolyTimeFun (LenIn × Cost.Unary) ((LenIn × Cost.Unary) × ℕ × ℕ × ℕ × ℕ)

Stage 3: the input of dimProg computing k = 2^{τ(|λ| + |n|)} · 1.

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.lenC_apply (a : LenIn) (us : Cost.Unary) : lenC.toFun (a, us) = ((a, us), 1, a.1.2.2.1, a.2.1, a.1.2.2.2)

noncomputable def MIPRE.Tailored.RepProg.lenQueryF (κ : Bool) : Cost.PolyTimeFun (Cost.BitStr × ℕ) Cost.Data

The query to L̄ at a block and a kind: (n, xᵢ, κ).

Equations

• MIPRE.Tailored.RepProg.lenQueryF κ = MIPRE.CL.Detyping.Program.encoded.comp (MIPRE.Cost.PolyTimeFun.snd.pair (MIPRE.Cost.PolyTimeFun.fst.pair (MIPRE.Cost.PolyTimeFun.const κ)))

@[simp]

theorem MIPRE.Tailored.RepProg.lenQueryF_apply (κ : Bool) (p : Cost.BitStr × ℕ) : (lenQueryF κ).toFun p = Cost.encode (p.2, p.1, κ)

def MIPRE.Tailored.RepProg.lenQueries (n : ℕ) (bl : List Cost.BitStr) : List Cost.Data

The queries to L̄: every block at false, then every block at true.

Equations

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

noncomputable def MIPRE.Tailored.RepProg.readQ (d : Cost.Data) : Cost.BitStr

The question and the kind read off the datum d = (x, κ).

Equations

• MIPRE.Tailored.RepProg.readQ d = MIPRE.CL.Detyping.Program.readBits.toFun (MIPRE.Cost.PolyTimeFun.treeHead.toFun d)

noncomputable def MIPRE.Tailored.RepProg.readK (d : Cost.Data) : Bool

Equations

• MIPRE.Tailored.RepProg.readK d = MIPRE.CL.Detyping.Program.rawTruthProg.toFun (MIPRE.Cost.PolyTimeFun.treeTail.toFun d)

noncomputable def MIPRE.Tailored.RepProg.lenD : Cost.PolyTimeFun ((LenIn × Cost.Unary) × Cost.Unary) ((Bool × Cost.Unary) × Cost.Prog × List Cost.Data)

Stage 4: the blocks of x and the queries to L̄; the context is (κ, k).

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.lenD_apply (p : (LenIn × Cost.Unary) × Cost.Unary) : lenD.toFun p = ((readK p.1.1.2.2, p.2), p.1.1.1.2.1, lenQueries p.1.1.2.1 (blocks (readQ p.1.1.2.2) (List.length p.1.2) (List.length p.2)))

def MIPRE.Tailored.RepProg.lenOut (κ : Bool) (k : ℕ) (rs : List Cost.Data) : List Cost.Data

The output: the concatenation of the outputs at the kind κ.

Equations

• MIPRE.Tailored.RepProg.lenOut κ k rs = (List.map MIPRE.CL.Detyping.Program.rawList (if κ = true then List.drop k rs else List.take k rs)).flatten

noncomputable def MIPRE.Tailored.RepProg.lenE : Cost.PolyTimeFun ((Bool × Cost.Unary) × List Cost.Data) (List Cost.Data)

Stage 5: the output.

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.lenE_apply (p : (Bool × Cost.Unary) × List Cost.Data) : lenE.toFun p = lenOut p.1.1 (List.length p.1.2) p.2

The program

noncomputable def MIPRE.Tailored.RepProg.lenCore (univ : Cost.Prog) : Cost.Prog

The core of the repeated answer-length calculator, on ((S̄, L̄, λ, τ), (n, d)).

Equations

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

theorem MIPRE.Tailored.RepProg.lenCore_wellScoped {univ : Cost.Prog} (hU : Cost.Prog.WellScoped 1 univ) : Cost.Prog.WellScoped 1 (lenCore univ)

The run

@[simp]

theorem MIPRE.Tailored.RepProg.encode_list_data (l : List Cost.Data) : Cost.encode l = Cost.Data.list l

noncomputable def MIPRE.Tailored.RepProg.lenQs (n : ℕ) (d : Cost.Data) (s k : ℕ) : List Cost.Data

The queries of the calculator to L̄ at (n, d), with dimension s and k coordinates.

Equations

• MIPRE.Tailored.RepProg.lenQs n d s k = MIPRE.Tailored.RepProg.lenQueries n (MIPRE.Tailored.RepProg.blocks (MIPRE.Tailored.RepProg.readQ d) s k)

noncomputable def MIPRE.Tailored.RepProg.lenCoreCost (sp lp : Cost.Prog) (lam tau n : ℕ) (d : Cost.Data) (s k Td T Z : ℕ) (rs : List Cost.Data) : ℕ

The cost of the core, stage by stage, with the dimension query of cost at most Td, the calls to L̄ of cost at most T, and Z bounding the queries and results of the last loop.

Equations

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

theorem MIPRE.Tailored.RepProg.lenCore_runsLe {univ : Cost.Prog} (hU : Cost.Prog.WellScoped 1 univ) (sp lp : Cost.Prog) (lam tau n : ℕ) (d : Cost.Data) (s : ℕ) {Td : ℕ} (hdim : Calls.RunsLe univ ((Cost.encode sp).cons (Cost.encode (n, CL.Sampler.Query.dimension))) (Cost.encode s) Td) (f : Cost.Data → Cost.Data) (T Z : ℕ) (hf : ∀ q ∈ lenQs n d s (Repetition.reps lam tau n), Calls.RunsLe univ ((Cost.encode lp).cons q) (f q) T) (hZ : (Cost.Data.list (lenQs n d s (Repetition.reps lam tau n))).size + (Cost.Data.list (List.map f (lenQs n d s (Repetition.reps lam tau n)))).size + 1 ≤ Z) : Calls.RunsLe (lenCore univ) (Cost.encode ((sp, lp, lam, tau), n, d)) (Cost.encode (lenOut (readK d) (Repetition.reps lam tau n) (List.map f (lenQs n d s (Repetition.reps lam tau n))))) (lenCoreCost sp lp lam tau n d s (Repetition.reps lam tau n) Td T Z (List.map f (lenQs n d s (Repetition.reps lam tau n))))

The run of the core, from runs of the calls: the dimension query answered by s, and the calls to L̄ answered by f.

theorem MIPRE.Tailored.RepProg.lenCore_inv {univ : Cost.Prog} (hU : Cost.Prog.WellScoped 1 univ) (sp lp : Cost.Prog) (lam tau n : ℕ) (d : Cost.Data) (s : ℕ) {td : ℕ} (hdim : univ.Runs ((Cost.encode sp).cons (Cost.encode (n, CL.Sampler.Query.dimension))) (Cost.encode s) td) {r : Cost.Data} {t : ℕ} (h : (lenCore univ).Runs (Cost.encode ((sp, lp, lam, tau), n, d)) r t) : ∃ (rs : List Cost.Data), List.Forall₂ (fun (q r : Cost.Data) => ∃ (t' : ℕ), univ.Runs ((Cost.encode lp).cons q) r t') (lenQs n d s (Repetition.reps lam tau n)) rs ∧ r = Cost.encode (lenOut (readK d) (Repetition.reps lam tau n) rs)

Inversion of the core: when the dimension query is answered by s, a halting run ran L̄ on every query, and output the concatenation of the results at the kind κ.

The calculator

noncomputable def MIPRE.Tailored.RepProg.repLenProg (sp lp : Cost.Prog) (lam tau : ℕ) : Cost.Prog

The program of the repeated answer-length calculator: the core with (S̄, L̄, λ, τ) stored.

Equations

• MIPRE.Tailored.RepProg.repLenProg sp lp lam tau = MIPRE.Cost.hardcode (MIPRE.Tailored.RepProg.lenCore MIPRE.Cost.selfUniversal.univ) (MIPRE.Cost.encode (sp, lp, lam, tau))

noncomputable def MIPRE.Tailored.RepProg.repLen {ℓ : ℕ} (S : CL.Sampler ℓ) (L : Decider) (lam tau : ℕ) : Decider

The repeated answer-length calculator.

Equations

• MIPRE.Tailored.RepProg.repLen S L lam tau = { prog := MIPRE.Tailored.RepProg.repLenProg S.prog L.prog lam tau, closed := ⋯ }

theorem MIPRE.Tailored.RepProg.readQ_encode (x : Cost.BitStr) (κ : Bool) : readQ (Cost.encode (x, κ)) = x

theorem MIPRE.Tailored.RepProg.readK_encode (x : Cost.BitStr) (κ : Bool) : readK (Cost.encode (x, κ)) = κ

theorem MIPRE.Tailored.RepProg.toBits_blockEquiv {k s : ℕ} (x : Fin (k * s) → CL.𝔽₂) (i : Fin k) : CL.toBits ((CL.blockEquiv finProdFinEquiv) x i) = Cost.Data.chunk s (↑i) (CL.toBits x)

The i-th block of a question of 𝔽₂^{k s} is the i-th chunk of its bit string.

theorem MIPRE.Tailored.RepProg.blocks_toBits {k s : ℕ} (x : Fin (k * s) → CL.𝔽₂) : blocks (CL.toBits x) s k = List.ofFn fun (i : Fin k) => CL.toBits ((CL.blockEquiv finProdFinEquiv) x i)

theorem MIPRE.Tailored.RepProg.exists_of_forall₂ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : List α} {l₂ : List β} : List.Forall₂ R l₁ l₂ → ∀ a ∈ l₁, ∃ (b : β), R a b

theorem MIPRE.Tailored.RepProg.lenOut_lenQueries (n : ℕ) (bl : List Cost.BitStr) (κ : Bool) (f : Cost.Data → Cost.Data) {k : ℕ} (hk : bl.length = k) : lenOut κ k (List.map f (lenQueries n bl)) = (List.map (fun (xi : Cost.BitStr) => CL.Detyping.Program.rawList (f (Cost.encode (n, xi, κ)))) bl).flatten

The output at the queries of a list of blocks: the concatenation of the results at the kind κ.

theorem MIPRE.Tailored.RepProg.length_flatten_map_ofFn {α : Type u_1} {k : ℕ} (g : Fin k → Cost.BitStr) (F : Cost.BitStr → List α) : (List.map F (List.ofFn g)).flatten.length = ∑ i : Fin k, (F (g i)).length

The length of a list concatenated over the coordinates.

theorem MIPRE.Tailored.RepProg.lenQs_toBits {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau n : ℕ) (x : Fin (TailoredVerifier.K lam tau n * V.sampler.dim n) → CL.𝔽₂) (κ : Bool) : lenQs n (Cost.encode (CL.toBits x, κ)) (V.sampler.dim n) (TailoredVerifier.K lam tau n) = lenQueries n (List.ofFn fun (i : Fin (TailoredVerifier.K lam tau n)) => CL.toBits (V.qc lam tau n x i))

The queries at a question of the repeated verifier are those of its coordinates.

theorem MIPRE.Tailored.RepProg.dim_univ {ℓ : ℕ} (V : TailoredVerifier ℓ) (n : ℕ) : ∃ (td : ℕ), Cost.selfUniversal.univ.Runs ((Cost.encode V.sampler.prog).cons (Cost.encode (n, CL.Sampler.Query.dimension))) (Cost.encode (V.sampler.dim n)) td

The dimension query, through the universal machine.

theorem MIPRE.Tailored.RepProg.repLen_runs_of {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau : ℕ) {n : ℕ} {d r : Cost.Data} {t : ℕ} (h : (lenCore Cost.selfUniversal.univ).Runs (Cost.encode ((V.sampler.prog, V.len.prog, lam, tau), n, d)) r t) : ∃ (t' : ℕ), (repLen V.sampler V.len lam tau).prog.Runs ((Cost.encode n).cons d) r t'

The run of the calculator from a run of its core.

theorem MIPRE.Tailored.RepProg.repLen_lenIs {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau n : ℕ) (x : Fin (TailoredVerifier.K lam tau n * V.sampler.dim n) → CL.𝔽₂) (hx : ∀ (i : Fin (TailoredVerifier.K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n x i))) (κ : Bool) : LenIs (repLen V.sampler V.len lam tau) n (CL.toBits x) κ (∑ i : Fin (TailoredVerifier.K lam tau n), V.lenOf n (CL.toBits (V.qc lam tau n x i)) κ)

RepSpec.len_eq: at a question all of whose coordinates have their lengths, the calculator outputs the sum of the coordinates' lengths.

theorem MIPRE.Tailored.RepProg.good_of_repLen {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau n : ℕ) (x : Fin (TailoredVerifier.K lam tau n * V.sampler.dim n) → CL.𝔽₂) (κ : Bool) (m : ℕ) (h : LenIs (repLen V.sampler V.len lam tau) n (CL.toBits x) κ m) (i : Fin (TailoredVerifier.K lam tau n)) : V.LenDefined n (CL.toBits (V.qc lam tau n x i))

RepSpec.good_of_len: the calculator halts only at questions all of whose coordinates have their lengths.

theorem MIPRE.Tailored.RepProg.repLen_lenBound {ℓ : ℕ} (S : CL.Sampler ℓ) (L : Decider) (lam tau n B : ℕ) (hB : LenBound L n B) : LenBound (repLen S L lam tau) n (Repetition.reps lam tau n * B)

The lengths of the repeated calculator are at most k(n) times the input's.