The repeated linear-constraints processor

The linear-constraints processor of the repeated tailored verifier (issue #280, P2b), on (n, x, y, a^R, b^R), with the input sampler S̄, calculator L̄ and processor P̄ and the parameters (λ, τ) stored:

1. the dimension s and k = k(n) in unary, as the calculator does;
2. cut x and y into their k blocks, and run L̄ on both kinds of every block of both;
3. from the lengths, cut a^R and b^R into the coordinates' readable answers, and run P̄ on (n, xᵢ, yᵢ, a^R_i, b^R_i) for every coordinate;
4. output every coordinate's constraints, padded to all the variables (padWithL, which is TailoredGame.padCons).

The stages

@[reducible, inline]

abbrev MIPRE.Tailored.RepProg.LpPar : Type

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

Equations

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

@[reducible, inline]

abbrev MIPRE.Tailored.RepProg.LpIn : Type

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

Equations

• MIPRE.Tailored.RepProg.LpIn = (MIPRE.Tailored.RepProg.LpPar × ℕ × MIPRE.Cost.Data)

noncomputable def MIPRE.Tailored.RepProg.lpA : Cost.PolyTimeFun LpIn (LpIn × 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.lpA_apply (a : LpIn) : lpA.toFun a = (a, a.1.1, [Cost.encode (a.2.1, CL.Sampler.Query.dimension)])

noncomputable def MIPRE.Tailored.RepProg.lpB : Cost.PolyTimeFun (LpIn × List Cost.Data) (LpIn × ℕ)

Stage 2: read the dimension.

Equations

• MIPRE.Tailored.RepProg.lpB = 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.lpB_apply (p : LpIn × List Cost.Data) : lpB.toFun p = (p.1, CL.Detyping.Program.readNat.toFun (p.2.headD Cost.Data.nil))

noncomputable def MIPRE.Tailored.RepProg.lpC : Cost.PolyTimeFun (LpIn × Cost.Unary) ((LpIn × Cost.Unary) × ℕ × ℕ × ℕ × ℕ)

Stage 3: the input of dimProg computing k.

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.lpC_apply (a : LpIn) (us : Cost.Unary) : lpC.toFun (a, us) = ((a, us), 1, a.1.2.2.2.1, a.2.1, a.1.2.2.2.2)

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

The four components of the datum d = (x, y, a^R, b^R).

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

theorem MIPRE.Tailored.RepProg.read_encode (x y aR bR : Cost.BitStr) : readX (Cost.encode (x, y, aR, bR)) = x ∧ readY (Cost.encode (x, y, aR, bR)) = y ∧ readAR (Cost.encode (x, y, aR, bR)) = aR ∧ readBR (Cost.encode (x, y, aR, bR)) = bR

noncomputable def MIPRE.Tailored.RepProg.readXF : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

• MIPRE.Tailored.RepProg.readXF = MIPRE.CL.Detyping.Program.readBits.comp MIPRE.Cost.PolyTimeFun.treeHead

noncomputable def MIPRE.Tailored.RepProg.readYF : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

• MIPRE.Tailored.RepProg.readYF = MIPRE.CL.Detyping.Program.readBits.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Cost.PolyTimeFun.treeTail)

noncomputable def MIPRE.Tailored.RepProg.readARF : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

• MIPRE.Tailored.RepProg.readARF = MIPRE.CL.Detyping.Program.readBits.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeTail))

noncomputable def MIPRE.Tailored.RepProg.readBRF : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

• MIPRE.Tailored.RepProg.readBRF = MIPRE.CL.Detyping.Program.readBits.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeTail))

@[reducible, inline]

abbrev MIPRE.Tailored.RepProg.LpSt : Type

The state after k in unary: ((a, s), k).

Equations

• MIPRE.Tailored.RepProg.LpSt = ((MIPRE.Tailored.RepProg.LpIn × MIPRE.Cost.Unary) × MIPRE.Cost.Unary)

noncomputable def MIPRE.Tailored.RepProg.blocksX (st : LpSt) : List Cost.BitStr

The blocks of x and of y at a state.

Equations

• MIPRE.Tailored.RepProg.blocksX st = MIPRE.Tailored.RepProg.blocks (MIPRE.Tailored.RepProg.readX st.1.1.2.2) (List.length st.1.2) (List.length st.2)

noncomputable def MIPRE.Tailored.RepProg.blocksY (st : LpSt) : List Cost.BitStr

Equations

• MIPRE.Tailored.RepProg.blocksY st = MIPRE.Tailored.RepProg.blocks (MIPRE.Tailored.RepProg.readY st.1.1.2.2) (List.length st.1.2) (List.length st.2)

noncomputable def MIPRE.Tailored.RepProg.blocksXF : Cost.PolyTimeFun LpSt (List Cost.BitStr)

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.blocksXF_apply (st : LpSt) : blocksXF.toFun st = blocksX st

noncomputable def MIPRE.Tailored.RepProg.blocksYF : Cost.PolyTimeFun LpSt (List Cost.BitStr)

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.blocksYF_apply (st : LpSt) : blocksYF.toFun st = blocksY st

noncomputable def MIPRE.Tailored.RepProg.lpLenQs (st : LpSt) : List Cost.Data

The length queries: every block of x at both kinds, then every block of y.

Equations

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

noncomputable def MIPRE.Tailored.RepProg.lenQueriesF : Cost.PolyTimeFun (List Cost.BitStr × ℕ) (List Cost.Data)

The length queries at a list of blocks, in polynomial time.

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.lenQueriesF_apply (p : List Cost.BitStr × ℕ) : lenQueriesF.toFun p = lenQueries p.2 p.1

noncomputable def MIPRE.Tailored.RepProg.lpD : Cost.PolyTimeFun LpSt (LpSt × Cost.Prog × List Cost.Data)

Stage 4: the queries to L̄.

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.lpD_apply (st : LpSt) : lpD.toFun st = (st, st.1.1.1.2.1, lpLenQs st)

From the lengths to the queries to the processor

def MIPRE.Tailored.RepProg.lensOf (rs : List Cost.Data) : List Cost.Unary

The lengths, in unary, of a list of outputs of the calculator.

Equations

• MIPRE.Tailored.RepProg.lensOf rs = List.map (fun (r : MIPRE.Cost.Data) => MIPRE.Cost.unary (MIPRE.CL.Detyping.Program.rawList r).length) rs

noncomputable def MIPRE.Tailored.RepProg.lensOfF : Cost.PolyTimeFun (List Cost.Data) (List Cost.Unary)

Equations

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

def MIPRE.Tailored.RepProg.quarter (rs : List Cost.Data) (k j : ℕ) : List Cost.Data

The j-th quarter of the results, k each.

Equations

• MIPRE.Tailored.RepProg.quarter rs k j = List.take k (List.drop (j * k) rs)

def MIPRE.Tailored.RepProg.lpPads (rs : List Cost.Data) (k : ℕ) : List (List Cost.Unary)

The twelve lengths of every coordinate, from the results of the calls to L̄.

Equations

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

def MIPRE.Tailored.RepProg.lpQuery (n : ℕ) (aR bR : Cost.BitStr) (q : (Cost.BitStr × Cost.BitStr) × List Cost.Unary) : Cost.Data

The query to P̄ at a coordinate: its blocks and its readable answers.

Equations

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

def MIPRE.Tailored.RepProg.lpQueries (n : ℕ) (bx by' : List Cost.BitStr) (aR bR : Cost.BitStr) (pads : List (List Cost.Unary)) : List Cost.Data

The queries to P̄.

Equations

• MIPRE.Tailored.RepProg.lpQueries n bx by' aR bR pads = List.map (MIPRE.Tailored.RepProg.lpQuery n aR bR) ((bx.zip by').zip pads)

noncomputable def MIPRE.Tailored.RepProg.dropTimesF : ℕ → Cost.PolyTimeFun (List Cost.Data × Cost.Unary) (List Cost.Data)

j blocks of k dropped.

Equations

• MIPRE.Tailored.RepProg.dropTimesF 0 = MIPRE.Cost.PolyTimeFun.fst
• MIPRE.Tailored.RepProg.dropTimesF j.succ = MIPRE.Cost.PolyTimeFun.drop.comp ((MIPRE.Tailored.RepProg.dropTimesF j).pair MIPRE.Cost.PolyTimeFun.snd)

theorem MIPRE.Tailored.RepProg.dropTimesF_apply (rs : List Cost.Data) (uk : Cost.Unary) (j : ℕ) : (dropTimesF j).toFun (rs, uk) = List.drop (j * List.length uk) rs

noncomputable def MIPRE.Tailored.RepProg.quarterF (j : ℕ) : Cost.PolyTimeFun (List Cost.Data × Cost.Unary) (List Cost.Data)

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.quarterF_apply (j : ℕ) (p : List Cost.Data × Cost.Unary) : (quarterF j).toFun p = quarter p.1 (List.length p.2) j

noncomputable def MIPRE.Tailored.RepProg.concat4F : Cost.PolyTimeFun ((List Cost.Unary × List Cost.Unary) × List Cost.Unary × List Cost.Unary) (List Cost.Unary)

The concatenation of the four triples of a coordinate.

Equations

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

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

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.lpPadsF_apply (p : List Cost.Data × Cost.Unary) : lpPadsF.toFun p = lpPads p.1 (List.length p.2)

noncomputable def MIPRE.Tailored.RepProg.lpQueryF : Cost.PolyTimeFun (((Cost.BitStr × Cost.BitStr) × List Cost.Unary) × ℕ × Cost.BitStr × Cost.BitStr) Cost.Data

The query to P̄ at a coordinate, in polynomial time.

Equations

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

noncomputable def MIPRE.Tailored.RepProg.lpQueriesF : Cost.PolyTimeFun (((List Cost.BitStr × List Cost.BitStr) × List (List Cost.Unary)) × ℕ × Cost.BitStr × Cost.BitStr) (List Cost.Data)

The queries to P̄, in polynomial time.

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.lpQueriesF_apply (p : ((List Cost.BitStr × List Cost.BitStr) × List (List Cost.Unary)) × ℕ × Cost.BitStr × Cost.BitStr) : lpQueriesF.toFun p = lpQueries p.2.1 p.1.1.1 p.1.1.2 p.2.2.1 p.2.2.2 p.1.2

noncomputable def MIPRE.Tailored.RepProg.lpPQs (st : LpSt) (rs : List Cost.Data) : List Cost.Data

The queries to P̄ at a state and the results of the calls to L̄.

Equations

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

noncomputable def MIPRE.Tailored.RepProg.ppF : Cost.PolyTimeFun (LpSt × List Cost.Data) Cost.Prog

Projections of (st, rs).

Equations

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

noncomputable def MIPRE.Tailored.RepProg.nF : Cost.PolyTimeFun (LpSt × List Cost.Data) ℕ

Equations

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

noncomputable def MIPRE.Tailored.RepProg.dF : Cost.PolyTimeFun (LpSt × List Cost.Data) Cost.Data

Equations

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

noncomputable def MIPRE.Tailored.RepProg.padsF : Cost.PolyTimeFun (LpSt × List Cost.Data) (List (List Cost.Unary))

Equations

• MIPRE.Tailored.RepProg.padsF = MIPRE.Tailored.RepProg.lpPadsF.comp (MIPRE.Cost.PolyTimeFun.snd.pair (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.fst))

noncomputable def MIPRE.Tailored.RepProg.lpE : Cost.PolyTimeFun (LpSt × List Cost.Data) (List (List Cost.Unary) × Cost.Prog × List Cost.Data)

Stage 5: the queries to P̄; the context is the twelve lengths of every coordinate.

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.lpE_apply (p : LpSt × List Cost.Data) : lpE.toFun p = (lpPads p.2 (List.length p.1.2), p.1.1.1.1.2.2.1, lpPQs p.1 p.2)

theorem MIPRE.Tailored.RepProg.readBits_eq_bitsD (d : Cost.Data) : CL.Detyping.Program.readBits.toFun d = d.bitsD

def MIPRE.Tailored.RepProg.lpOut (pads : List (List Cost.Unary)) (rs : List Cost.Data) : List Cost.BitStr

The output: every coordinate's constraints, padded.

Equations

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

noncomputable def MIPRE.Tailored.RepProg.bitsListDF : Cost.PolyTimeFun Cost.Data (List Cost.BitStr)

bitsListD, in polynomial time.

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.bitsListDF_apply (d : Cost.Data) : bitsListDF.toFun d = d.bitsListD

noncomputable def MIPRE.Tailored.RepProg.lpF : Cost.PolyTimeFun (List (List Cost.Unary) × List Cost.Data) (List Cost.BitStr)

Stage 6: the output.

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.lpF_apply (p : List (List Cost.Unary) × List Cost.Data) : lpF.toFun p = lpOut p.1 p.2

The program

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

The core of the repeated linear-constraints processor, on ((S̄, L̄, P̄, λ, τ), (n, d)).

Equations

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

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

The run

@[reducible, inline]

abbrev MIPRE.Tailored.RepProg.lpSt (sp lp pp : Cost.Prog) (lam tau n : ℕ) (d : Cost.Data) (s : ℕ) : LpSt

The state after the first stages: ((a, s), k).

Equations

• MIPRE.Tailored.RepProg.lpSt sp lp pp lam tau n d s = ((((sp, lp, pp, lam, tau), n, d), MIPRE.Cost.unary s), MIPRE.Cost.unary (MIPRE.Repetition.reps lam tau n))

noncomputable def MIPRE.Tailored.RepProg.lpCoreCost (sp lp pp : Cost.Prog) (lam tau n : ℕ) (d : Cost.Data) (s Td T₁ Z₁ T₂ Z₂ : ℕ) (rs₁ 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₁ with bound Z₁ on the second loop, and the calls to P̄ of cost at most T₂ with bound Z₂ on the third.

Equations

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

theorem MIPRE.Tailored.RepProg.lpCore_runsLe {univ : Cost.Prog} (hU : Cost.Prog.WellScoped 1 univ) (sp lp pp : 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₁ f₂ : Cost.Data → Cost.Data) (T₁ Z₁ T₂ Z₂ : ℕ) (hf₁ : ∀ q ∈ lpLenQs (lpSt sp lp pp lam tau n d s), Calls.RunsLe univ ((Cost.encode lp).cons q) (f₁ q) T₁) (hZ₁ : (Cost.Data.list (lpLenQs (lpSt sp lp pp lam tau n d s))).size + (Cost.Data.list (List.map f₁ (lpLenQs (lpSt sp lp pp lam tau n d s)))).size + 1 ≤ Z₁) (hf₂ : ∀ q ∈ lpPQs (lpSt sp lp pp lam tau n d s) (List.map f₁ (lpLenQs (lpSt sp lp pp lam tau n d s))), Calls.RunsLe univ ((Cost.encode pp).cons q) (f₂ q) T₂) (hZ₂ : (Cost.Data.list (lpPQs (lpSt sp lp pp lam tau n d s) (List.map f₁ (lpLenQs (lpSt sp lp pp lam tau n d s))))).size + (Cost.Data.list (List.map f₂ (lpPQs (lpSt sp lp pp lam tau n d s) (List.map f₁ (lpLenQs (lpSt sp lp pp lam tau n d s)))))).size + 1 ≤ Z₂) : Calls.RunsLe (lpCore univ) (Cost.encode ((sp, lp, pp, lam, tau), n, d)) (Cost.encode (lpOut (lpPads (List.map f₁ (lpLenQs (lpSt sp lp pp lam tau n d s))) (Repetition.reps lam tau n)) (List.map f₂ (lpPQs (lpSt sp lp pp lam tau n d s) (List.map f₁ (lpLenQs (lpSt sp lp pp lam tau n d s))))))) (lpCoreCost sp lp pp lam tau n d s Td T₁ Z₁ T₂ Z₂ (List.map f₁ (lpLenQs (lpSt sp lp pp lam tau n d s))) (List.map f₂ (lpPQs (lpSt sp lp pp lam tau n d s) (List.map f₁ (lpLenQs (lpSt sp lp pp lam tau n d s))))))

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

theorem MIPRE.Tailored.RepProg.lpCore_inv {univ : Cost.Prog} (hU : Cost.Prog.WellScoped 1 univ) (sp lp pp : 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 : (lpCore univ).Runs (Cost.encode ((sp, lp, pp, lam, tau), n, d)) r t) : ∃ (rs₁ : List Cost.Data) (rs₂ : List Cost.Data), List.Forall₂ (fun (q r : Cost.Data) => ∃ (t' : ℕ), univ.Runs ((Cost.encode lp).cons q) r t') (lpLenQs (lpSt sp lp pp lam tau n d s)) rs₁ ∧ List.Forall₂ (fun (q r : Cost.Data) => ∃ (t' : ℕ), univ.Runs ((Cost.encode pp).cons q) r t') (lpPQs (lpSt sp lp pp lam tau n d s) rs₁) rs₂ ∧ r = Cost.encode (lpOut (lpPads rs₁ (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 length query and P̄ on every query its results determine, and output the padded constraints.