The product of a typed sampler and a directly answered one: the program

The program half of MIPRE/Foundations/CL/ProductSampler. A DirectSampler is a family of typed presentations whose queries a total polynomial-time function answers outright, for every level, from parameters a routine computes at the index: the downsized PCP sampler of answer reduction is one. The product TypedSampler.prodDirect A B L of a typed sampler A and a direct sampler B has the types Ta × Tb, the presentations prodCL L (A.cl n w ta) (B.cl n tb) and a program making at most one call, through the universal machine, to A's, after a call to B's parameter routine:

• the dimension query is forwarded to A, and B's dimension added;
• a typed query is split: the last B.dim n bits of its vectors go to B's answer function, the others make up A's query, whose answer the post-processor prepends;
• beyond A's level ℓa (it is padded to L), the marginal is asked at level ℓa, and a linear map or factor query is answered directly, A's half zero.

The program is hardcode core (encode (A.prog, ℓa, B.parProg)) for a core depending only on B's two functions: that is what makes a sampler built this way depend only on its input sampler's program and its parameters.

@[reducible, inline]

abbrev MIPRE.CL.DirectInput : Type

The input of a direct answer: (p, type, kind, j, u, y), with p the parameters at the index and the query's kind, level and vectors as in Sampler.Query.toTuple.

Equations

• MIPRE.CL.DirectInput = (MIPRE.Cost.Data × MIPRE.Cost.Data × ℕ × ℕ × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

structure MIPRE.CL.DirectSampler (ℓ : ℕ) (T : Type u_1) [Cost.SizedEncoding T] : Type u_1

A directly answered typed sampler, the same for both players: a routine computes its parameters pd n at the index n, and a polynomial-time function of the parameters answers its queries, at every level.

• parProg : Cost.Prog

  The parameter routine.

• parProg_closed : Cost.Prog.WellScoped 1 self.parProg
• pd : ℕ → Cost.Data

  The parameters at each index.

• parProg_runs (n : ℕ) : ∃ (t : ℕ), self.parProg.Runs (Cost.encode n) (self.pd n) t
• dim : ℕ → ℕ

  The dimension.

• cl (n : ℕ) : T → CLFun 𝔽₂ (Fin (self.dim n)) ℓ

  The typed CL functions.

• cl_exactlyOn (n : ℕ) (t : T) : (self.cl n t).ExactlyOn Finset.univ
• dimProg : Cost.PolyTimeFun Cost.Data Cost.Unary

  The dimension, in unary, from the parameters.

• dimProg_eq (n : ℕ) : List.length (self.dimProg.toFun (self.pd n)) = self.dim n
• answer : Cost.PolyTimeFun DirectInput Cost.BitStr

  The answers.

• answer_marginal (n : ℕ) (t : T) (j : ℕ) (z : Cost.BitStr) : 1 ≤ j → List.length z = self.dim n → self.answer.toFun (self.pd n, Cost.encode t, 1, j, z, []) = toBits ((CLFun.truncate j (self.cl n t)).eval (ofBits (self.dim n) z))
• answer_linear (n : ℕ) (t : T) (j : ℕ) (u y : Cost.BitStr) : 1 ≤ j → (∃ (x : Fin (self.dim n) → 𝔽₂), u = toBits ((CLFun.truncate (j - 1) (self.cl n t)).eval x)) → List.length y = self.dim n → self.answer.toFun (self.pd n, Cost.encode t, 2, j, u, y) = toBits (((self.cl n t).mapOfPrefix (j - 1) (ofBits (self.dim n) u)) (ofBits (self.dim n) y))
• answer_factor (n : ℕ) (t : T) (j : ℕ) (u : Cost.BitStr) : 1 ≤ j → (∃ (x : Fin (self.dim n) → 𝔽₂), u = toBits ((CLFun.truncate (j - 1) (self.cl n t)).eval x)) → self.answer.toFun (self.pd n, Cost.encode t, 3, j, u, []) = indicatorBits ((self.cl n t).factorOfPrefix (j - 1) (ofBits (self.dim n) u))

The parameter stage

The input is (H, n, q) with H = (A.prog, ℓa, B.parProg) hardcoded. The first stage calls the parameter routine on n and prepends its answer.

noncomputable def MIPRE.CL.ProductSampler.route0 : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Call the parameter routine on the index, keeping the input.

Equations

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

noncomputable def MIPRE.CL.ProductSampler.post0 : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

Prepend the parameters.

Equations

• MIPRE.CL.ProductSampler.post0 = MIPRE.Cost.PolyTimeFun.treePair.ap₂ MIPRE.Cost.PolyTimeFun.snd MIPRE.Cost.PolyTimeFun.fst

The core

Its input is (p, H, n, q), p the parameters.

noncomputable def MIPRE.CL.ProductSampler.pdD : Cost.PolyTimeFun Cost.Data Cost.Data

The parameters.

Equations

• MIPRE.CL.ProductSampler.pdD = MIPRE.Cost.PolyTimeFun.treeHead

noncomputable def MIPRE.CL.ProductSampler.progD : Cost.PolyTimeFun Cost.Data Cost.Data

A's program.

Equations

• MIPRE.CL.ProductSampler.progD = MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Cost.PolyTimeFun.treeTail)

noncomputable def MIPRE.CL.ProductSampler.levelA : Cost.PolyTimeFun Cost.Data ℕ

A's level.

Equations

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

noncomputable def MIPRE.CL.ProductSampler.nD : Cost.PolyTimeFun Cost.Data Cost.Data

The index.

Equations

• MIPRE.CL.ProductSampler.nD = MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeTail)

noncomputable def MIPRE.CL.ProductSampler.qD : Cost.PolyTimeFun Cost.Data Cost.Data

The typed query, nil for the dimension query.

Equations

• MIPRE.CL.ProductSampler.qD = MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeTail)

noncomputable def MIPRE.CL.ProductSampler.tagD : Cost.PolyTimeFun Cost.Data Cost.Data

The type pair.

Equations

• MIPRE.CL.ProductSampler.tagD = MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.CL.ProductSampler.qD

noncomputable def MIPRE.CL.ProductSampler.queryD : Cost.PolyTimeFun Cost.Data Cost.Data

The untyped query.

Equations

• MIPRE.CL.ProductSampler.queryD = MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.CL.ProductSampler.qD

noncomputable def MIPRE.CL.ProductSampler.parsedQ : Cost.PolyTimeFun Cost.Data Detyping.Program.Parsed

The untyped query, parsed: (n, kind, w, j, u, y).

Equations

• MIPRE.CL.ProductSampler.parsedQ = MIPRE.CL.Detyping.Program.parse.comp (MIPRE.Cost.PolyTimeFun.treePair.ap₂ MIPRE.CL.ProductSampler.nD MIPRE.CL.ProductSampler.queryD)

noncomputable def MIPRE.CL.ProductSampler.dimB (D : Cost.PolyTimeFun Cost.Data Cost.Unary) : Cost.PolyTimeFun Cost.Data Cost.Unary

B's dimension.

Equations

• MIPRE.CL.ProductSampler.dimB D = D.comp MIPRE.CL.ProductSampler.pdD

noncomputable def MIPRE.CL.ProductSampler.kind : Cost.PolyTimeFun Cost.Data ℕ

The kind of the query.

Equations

• MIPRE.CL.ProductSampler.kind = MIPRE.CL.Detyping.Program.pKind.comp MIPRE.CL.ProductSampler.parsedQ

noncomputable def MIPRE.CL.ProductSampler.lev : Cost.PolyTimeFun Cost.Data ℕ

Its level.

Equations

• MIPRE.CL.ProductSampler.lev = MIPRE.CL.Detyping.Program.pLevel.comp MIPRE.CL.ProductSampler.parsedQ

noncomputable def MIPRE.CL.ProductSampler.uD : Cost.PolyTimeFun Cost.Data Cost.BitStr

Its first vector.

Equations

• MIPRE.CL.ProductSampler.uD = MIPRE.CL.Detyping.Program.pU.comp MIPRE.CL.ProductSampler.parsedQ

noncomputable def MIPRE.CL.ProductSampler.yD : Cost.PolyTimeFun Cost.Data Cost.BitStr

Its second vector.

Equations

• MIPRE.CL.ProductSampler.yD = MIPRE.CL.Detyping.Program.pY.comp MIPRE.CL.ProductSampler.parsedQ

noncomputable def MIPRE.CL.ProductSampler.leftBits (D : Cost.PolyTimeFun Cost.Data Cost.Unary) (l : Cost.PolyTimeFun Cost.Data Cost.BitStr) : Cost.PolyTimeFun Cost.Data Cost.BitStr

All but the last B.dim n bits: A's half.

Equations

• MIPRE.CL.ProductSampler.leftBits D l = MIPRE.Cost.PolyTimeFun.reverse.comp (MIPRE.Cost.PolyTimeFun.drop.comp ((MIPRE.Cost.PolyTimeFun.reverse.comp l).pair (MIPRE.CL.ProductSampler.dimB D)))

noncomputable def MIPRE.CL.ProductSampler.rightBits (D : Cost.PolyTimeFun Cost.Data Cost.Unary) (l : Cost.PolyTimeFun Cost.Data Cost.BitStr) : Cost.PolyTimeFun Cost.Data Cost.BitStr

The last B.dim n bits: B's half.

Equations

• MIPRE.CL.ProductSampler.rightBits D l = MIPRE.Cost.PolyTimeFun.reverse.comp (MIPRE.Cost.PolyTimeFun.take.comp ((MIPRE.Cost.PolyTimeFun.reverse.comp l).pair (MIPRE.CL.ProductSampler.dimB D)))

noncomputable def MIPRE.CL.ProductSampler.answerB (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) : Cost.PolyTimeFun Cost.Data Cost.BitStr

B's half of the answer.

Equations

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

noncomputable def MIPRE.CL.ProductSampler.queryA (D : Cost.PolyTimeFun Cost.Data Cost.Unary) (j : Cost.PolyTimeFun Cost.Data ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

A's query at the level j: (n, (ta, (kind, w, j, u_A, y_A))).

Equations

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

noncomputable def MIPRE.CL.ProductSampler.request (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) (j : Cost.PolyTimeFun Cost.Data ℕ) : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

A call to A on its typed query at the level j; the context is B's half.

Equations

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

noncomputable def MIPRE.CL.ProductSampler.requestDim (D : Cost.PolyTimeFun Cost.Data Cost.Unary) : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

The call for the dimension; the context is B's dimension.

Equations

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

noncomputable def MIPRE.CL.ProductSampler.levA : Cost.PolyTimeFun Cost.Data ℕ

The marginal's level for A, at most ℓa.

Equations

• MIPRE.CL.ProductSampler.levA = (MIPRE.Cost.PolyTimeFun.leNat.ap₂ MIPRE.CL.ProductSampler.lev MIPRE.CL.ProductSampler.levelA).ite MIPRE.CL.ProductSampler.lev MIPRE.CL.ProductSampler.levelA

noncomputable def MIPRE.CL.ProductSampler.direct (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

The direct answer beyond A's level: zero on A's half.

Equations

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

noncomputable def MIPRE.CL.ProductSampler.route (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

The router.

Equations

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

noncomputable def MIPRE.CL.ProductSampler.post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

The post-processor: A's bits then B's, or the sum of the dimensions.

Equations

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

noncomputable def MIPRE.CL.ProductSampler.stage (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) : Cost.Prog

The routed stage of the core.

Equations

• MIPRE.CL.ProductSampler.stage B D = MIPRE.Cost.Prog.routeOneCall (MIPRE.CL.ProductSampler.route B D) MIPRE.Cost.selfUniversal.univ MIPRE.CL.ProductSampler.post

noncomputable def MIPRE.CL.ProductSampler.stage0 : Cost.Prog

The parameter stage of the core.

Equations

• MIPRE.CL.ProductSampler.stage0 = MIPRE.Cost.Prog.routeOneCall MIPRE.CL.ProductSampler.route0 MIPRE.Cost.selfUniversal.univ MIPRE.CL.ProductSampler.post0

noncomputable def MIPRE.CL.ProductSampler.core (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) : Cost.Prog

The core of the product sampler: the parameters, then the routed call.

Equations

• MIPRE.CL.ProductSampler.core B D = MIPRE.CL.ProductSampler.stage0.let_ (MIPRE.CL.ProductSampler.stage B D)

theorem MIPRE.CL.ProductSampler.stage_closed (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) : Cost.Prog.WellScoped 1 (stage B D)

theorem MIPRE.CL.ProductSampler.stage0_closed : Cost.Prog.WellScoped 1 stage0

theorem MIPRE.CL.ProductSampler.core_closed (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) : Cost.Prog.WellScoped 1 (core B D)

noncomputable def MIPRE.CL.ProductSampler.prog (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) : Cost.Prog

The product sampler's program: the core with (A.prog, ℓa, parProg) hardcoded.

Equations

• MIPRE.CL.ProductSampler.prog B D ap ℓa pp = MIPRE.Cost.hardcode (MIPRE.CL.ProductSampler.core B D) (MIPRE.Cost.encode (ap, ℓa, pp))

theorem MIPRE.CL.ProductSampler.prog_closed (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) : Cost.Prog.WellScoped 1 (prog B D ap ℓa pp)

The router on well-formed queries

theorem MIPRE.CL.ProductSampler.take_reverse_reverse {α : Type u_1} (l : List α) {a b : ℕ} (h : l.length = a + b) : (List.drop b l.reverse).reverse = List.take a l

theorem MIPRE.CL.ProductSampler.drop_reverse_reverse {α : Type u_1} (l : List α) {a b : ℕ} (h : l.length = a + b) : (List.take b l.reverse).reverse = List.drop a l

@[reducible, inline]

abbrev MIPRE.CL.ProductSampler.input {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (q : TypedSampler.Query (Ta × Tb)) : Cost.Data

The input of the routed stage on a typed query.

Equations

• MIPRE.CL.ProductSampler.input ap ℓa pp pdn n q = pdn.cons ((MIPRE.Cost.encode (ap, ℓa, pp)).cons (MIPRE.Cost.encode (n, q)))

theorem MIPRE.CL.ProductSampler.parsedQ_input {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) : parsedQ.toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = (Cost.encode n, q.toTuple.1, q.toTuple.2.1.toBool, q.toTuple.2.2.1, q.toTuple.2.2.2.1, q.toTuple.2.2.2.2)

@[simp]

theorem MIPRE.CL.ProductSampler.kind_input {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) : kind.toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = q.toTuple.1

@[simp]

theorem MIPRE.CL.ProductSampler.lev_input {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) : lev.toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = q.toTuple.2.2.1

@[simp]

theorem MIPRE.CL.ProductSampler.uD_input {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) : uD.toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = q.toTuple.2.2.2.1

@[simp]

theorem MIPRE.CL.ProductSampler.yD_input {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) : yD.toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = q.toTuple.2.2.2.2

@[simp]

theorem MIPRE.CL.ProductSampler.levelA_input {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) : levelA.toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = ℓa

@[simp]

theorem MIPRE.CL.ProductSampler.dimB_input (D : Cost.PolyTimeFun Cost.Data Cost.Unary) {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) : (dimB D).toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = D.toFun pdn

@[simp]

theorem MIPRE.CL.ProductSampler.qD_input {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) : qD.toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = (Cost.encode (ta, tb)).cons (Cost.encode q)

@[simp]

theorem MIPRE.CL.ProductSampler.tagD_input {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) : tagD.toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = (Cost.encode ta).cons (Cost.encode tb)

@[simp]

theorem MIPRE.CL.ProductSampler.pdD_input {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) : pdD.toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = pdn

@[simp]

theorem MIPRE.CL.ProductSampler.progD_input {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) : progD.toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = Cost.encode ap

@[simp]

theorem MIPRE.CL.ProductSampler.nD_input {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) : nD.toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = Cost.encode n

theorem MIPRE.CL.ProductSampler.answerB_input (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) : (answerB B D).toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = B.toFun (pdn, Cost.encode tb, q.toTuple.1, q.toTuple.2.2.1, (List.take (List.length (D.toFun pdn)) (List.reverse q.toTuple.2.2.2.1)).reverse, (List.take (List.length (D.toFun pdn)) (List.reverse q.toTuple.2.2.2.2)).reverse)

theorem MIPRE.CL.ProductSampler.queryA_input (D : Cost.PolyTimeFun Cost.Data Cost.Unary) {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) (j : Cost.PolyTimeFun Cost.Data ℕ) : (queryA D j).toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = (Cost.encode n).cons ((Cost.encode ta).cons (Cost.encode (q.toTuple.1, q.toTuple.2.1, j.toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)), (List.drop (List.length (D.toFun pdn)) (List.reverse q.toTuple.2.2.2.1)).reverse, (List.drop (List.length (D.toFun pdn)) (List.reverse q.toTuple.2.2.2.2)).reverse)))

theorem MIPRE.CL.ProductSampler.route_dimension (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) : (route B D).toFun (input ap ℓa pp pdn n TypedSampler.Query.dimension) = (true, ((Cost.encode ap).cons ((Cost.encode n).cons Cost.Data.nil)).cons (Cost.Data.nil.cons (Cost.encode (List.map (fun (x : Unit) => true) (D.toFun pdn)))))

theorem MIPRE.CL.ProductSampler.route_atType (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) : (route B D).toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = if q.toTuple.1 = 1 then (request B D levA).toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) else if q.toTuple.2.2.1 ≤ ℓa then (request B D lev).toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) else (direct B D).toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q))

theorem MIPRE.CL.ProductSampler.levA_input {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) : levA.toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = if q.toTuple.2.2.1 ≤ ℓa then q.toTuple.2.2.1 else ℓa

theorem MIPRE.CL.ProductSampler.request_input (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) (j : Cost.PolyTimeFun Cost.Data ℕ) : (request B D j).toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = (true, ((Cost.encode ap).cons ((queryA D j).toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)))).cons ((Cost.Data.nil.cons Cost.Data.nil).cons (Cost.encode ((answerB B D).toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q))))))

theorem MIPRE.CL.ProductSampler.direct_input (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (ta : Ta) (tb : Tb) (q : Sampler.Query) : (direct B D).toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q)) = (false, Cost.encode (List.map (fun (x : Bool) => false) (if q.toTuple.1 = 2 then (List.drop (List.length (D.toFun pdn)) (List.reverse q.toTuple.2.2.2.2)).reverse else (List.drop (List.length (D.toFun pdn)) (List.reverse q.toTuple.2.2.2.1)).reverse) ++ (answerB B D).toFun (input ap ℓa pp pdn n (TypedSampler.Query.atType (ta, tb) q))))

theorem MIPRE.CL.ProductSampler.post_bits (bA bB : Cost.BitStr) : post.toFun ((Cost.Data.nil.cons Cost.Data.nil).cons (Cost.encode bB), Cost.encode bA) = Cost.encode (bA ++ bB)

theorem MIPRE.CL.ProductSampler.post_dim (d : ℕ) (bB : Cost.BitStr) : post.toFun (Cost.Data.nil.cons (Cost.encode bB), Cost.encode d) = Cost.encode (d + List.length bB)

theorem MIPRE.CL.ProductSampler.route_call_shape (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) (p H nD' q payload : Cost.Data) (h : (route B D).toFun (p.cons (H.cons (nD'.cons q))) = (true, payload)) : ∃ (d : Cost.Data) (ctx : Cost.Data), payload = ((Cost.PolyTimeFun.treeHead.toFun H).cons (nD'.cons d)).cons ctx

Every call the router makes keeps the index.

theorem MIPRE.CL.ProductSampler.stage0_runs (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (q : Cost.Data) (t : ℕ) (hpp : pp.Runs (Cost.encode n) pdn t) : ∃ (t' : ℕ), stage0.Runs ((Cost.encode (ap, ℓa, pp)).cons ((Cost.encode n).cons q)) (pdn.cons ((Cost.encode (ap, ℓa, pp)).cons ((Cost.encode n).cons q))) t'

The parameter stage prepends the routine's answer.

theorem MIPRE.CL.ProductSampler.prog_runs_of_stage (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (q r : Cost.Data) (t t₁ : ℕ) (hpp : pp.Runs (Cost.encode n) pdn t) (h : (stage B D).Runs (pdn.cons ((Cost.encode (ap, ℓa, pp)).cons ((Cost.encode n).cons q))) r t₁) : ∃ (t' : ℕ), (prog B D ap ℓa pp).Runs ((Cost.encode n).cons q) r t'

theorem MIPRE.CL.ProductSampler.prog_runs_call (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (q a ctx r : Cost.Data) (t₀ t : ℕ) (hpp : pp.Runs (Cost.encode n) pdn t₀) (hroute : (route B D).toFun (pdn.cons ((Cost.encode (ap, ℓa, pp)).cons ((Cost.encode n).cons q))) = (true, ((Cost.encode ap).cons a).cons ctx)) (hr : ap.Runs a r t) : ∃ (t' : ℕ), (prog B D ap ℓa pp).Runs ((Cost.encode n).cons q) (post.toFun (ctx, r)) t'

theorem MIPRE.CL.ProductSampler.prog_runs_direct (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) (ap : Cost.Prog) (ℓa : ℕ) (pp : Cost.Prog) (pdn : Cost.Data) (n : ℕ) (q r : Cost.Data) (t₀ : ℕ) (hpp : pp.Runs (Cost.encode n) pdn t₀) (hroute : (route B D).toFun (pdn.cons ((Cost.encode (ap, ℓa, pp)).cons ((Cost.encode n).cons q))) = (false, r)) : ∃ (t : ℕ), (prog B D ap ℓa pp).Runs ((Cost.encode n).cons q) r t

The product sampler

theorem MIPRE.CL.TypedSampler.toBits_zero_vec (s : ℕ) : toBits 0 = List.replicate s false

theorem MIPRE.CL.TypedSampler.indicatorBits_empty' (s : ℕ) : indicatorBits ∅ = List.replicate s false

theorem MIPRE.CL.TypedSampler.map_false_eq {l : Cost.BitStr} {s : ℕ} (h : List.length l = s) : List.map (fun (x : Bool) => false) l = List.replicate s false

noncomputable def MIPRE.CL.TypedSampler.prodDirect {ℓa ℓb : ℕ} {Ta : Type u_1} {Tb : Type u_2} [Cost.SizedEncoding Ta] [Cost.SizedEncoding Tb] (A : TypedSampler ℓa Ta) (B : DirectSampler ℓb Tb) (L : ℕ) (hA : 1 ≤ ℓa) (ha : ℓa ≤ L) (hb : ℓb ≤ L) : TypedSampler L (Ta × Tb)

The product of a typed sampler and a direct sampler: the types are pairs, the presentations prodCL, and the program calls A's at most once.

Equations

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