The PCP sampler as a directly answered sampler

Piece AR-3d of planning/answer-reduction.md: the downsized PCP half of the answer-reduced sampler as a CL.DirectSampler (MIPRE/Foundations/CL/ProductSamplerProg), for a family of PCP parameters whose m and m' are powers of two (PcpFamily), with the effective seed selectors: the high bits of the seed (PcpFamily.sel), the selectors the introspection sampler uses.

• The queries of the downsized presentation, in bits, are the queries of the presentation over F_q in Shoup bits (toBits_eval_truncate_pcpCl, toBits_mapOfPrefix_pcpCl, indicatorBits_factorOfPrefix_pcpCl).
• The parameters at an index (PcpFamily.pd) are k, m' and the six copies' descriptions, in unary; a routine computes them. The answer function (answerProg) reads the copy and the test type off the type and runs the copy's program (MIPRE/Background/AnswerReduction/StageProg).

The type encoding

def MIPRE.AnswerReduction.tyOfNat : ℕ → Option LIDT.CL.Ty

A test type from its number.

Equations

• MIPRE.AnswerReduction.tyOfNat 0 = some MIPRE.LIDT.CL.Ty.point
• MIPRE.AnswerReduction.tyOfNat 1 = some MIPRE.LIDT.CL.Ty.aline
• MIPRE.AnswerReduction.tyOfNat 2 = some MIPRE.LIDT.CL.Ty.dline
• MIPRE.AnswerReduction.tyOfNat x✝ = none

@[instance_reducible]

instance MIPRE.AnswerReduction.instSizedEncodingTy : Cost.SizedEncoding LIDT.CL.Ty

Equations

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

The downsized presentation in bits

theorem MIPRE.AnswerReduction.ofBits_flatBits (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] (v : Pcp.Coord P → Fq P hk) : CL.ofBits (Pcp.pcpDim P * P.k) (Pcp.flatBits P hk v) = (CL.reindexEquiv (Pcp.bitIndex P P.k)) ((CL.downsizeEquiv (basis P hk)) v)

theorem MIPRE.AnswerReduction.toBits_eval_truncate_pcpCl (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (t : Pcp.PcpTy) (j : ℕ) (v : Pcp.Coord P → Fq P hk) : CL.toBits ((CL.CLFun.truncate j (pcpCl P hk S S' t)).eval (CL.ofBits (Pcp.pcpDim P * P.k) (Pcp.flatBits P hk v))) = Pcp.flatBits P hk ((CL.CLFun.truncate j (Pcp.pres P S S' t)).eval v)

theorem MIPRE.AnswerReduction.toBits_mapOfPrefix_pcpCl (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (t : Pcp.PcpTy) (j : ℕ) (u y : Pcp.Coord P → Fq P hk) : CL.toBits (((pcpCl P hk S S' t).mapOfPrefix j (CL.ofBits (Pcp.pcpDim P * P.k) (Pcp.flatBits P hk u))) (CL.ofBits (Pcp.pcpDim P * P.k) (Pcp.flatBits P hk y))) = Pcp.flatBits P hk (((Pcp.pres P S S' t).mapOfPrefix j u) y)

theorem MIPRE.AnswerReduction.indicatorBits_factorOfPrefix_pcpCl (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (t : Pcp.PcpTy) (j : ℕ) (u : Pcp.Coord P → Fq P hk) : CL.indicatorBits ((pcpCl P hk S S' t).factorOfPrefix j (CL.ofBits (Pcp.pcpDim P * P.k) (Pcp.flatBits P hk u))) = StageProg.flatInd P P.k ((Pcp.pres P S S' t).factorOfPrefix j u)

Selectors of power-of-two blocks

theorem MIPRE.AnswerReduction.pow_dvd_card (k : ℕ) (hk : 1 ≤ k) (sz jw : ℕ) (hsz : sz = 2 ^ jw) (hjw : jw ≤ k) : sz ∣ Fintype.card (SAT.shoupBinField k hk).carrier

noncomputable def MIPRE.AnswerReduction.powSel (k : ℕ) (hk : 1 ≤ k) (sz jw : ℕ) (hsz : sz = 2 ^ jw) (hjw : jw ≤ k) [NeZero sz] : LIDT.CL.Sel (SAT.shoupBinField k hk).carrier sz ⋯

The effective seed selector: the high jw bits of the seed, for blocks of size sz = 2^jw.

Equations

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

theorem MIPRE.AnswerReduction.powSel_χ (k : ℕ) (hk : 1 ≤ k) (sz jw : ℕ) (hsz : sz = 2 ^ jw) (hjw : jw ≤ k) [NeZero sz] (a : (SAT.shoupBinField k hk).carrier) : ↑((powSel k hk sz jw hsz hjw).χ a) = ↑(Introspection.SeedProgram.selector (SAT.shoupBinField k hk) jw hjw a)

Families of PCP parameters

structure MIPRE.AnswerReduction.PcpFamily : Type

A family of PCP parameters whose m and m' are powers of two, 2^{jm} and 2^{jm'}, with jm, jm' ≤ k: what the effective seed selectors need.

• par : ℕ → SAT.PcpParams

  The parameters at each index.

• hk (n : ℕ) : 1 ≤ (self.par n).k
• jm : ℕ → ℕ

  log₂ m.

• jm' : ℕ → ℕ

  log₂ m'.

• m_eq (n : ℕ) : (self.par n).m = 2 ^ self.jm n
• m'_eq (n : ℕ) : (self.par n).m' = 2 ^ self.jm' n
• jm_le (n : ℕ) : self.jm n ≤ (self.par n).k
• jm'_le (n : ℕ) : self.jm' n ≤ (self.par n).k

instance MIPRE.AnswerReduction.PcpFamily.neZero_m (F : PcpFamily) (n : ℕ) : NeZero (F.par n).m

noncomputable def MIPRE.AnswerReduction.PcpFamily.sel (F : PcpFamily) (n : ℕ) : LIDT.CL.Sel (Fq (F.par n) ⋯) (F.par n).m ⋯

The selector of the first five copies.

Equations

• F.sel n = MIPRE.AnswerReduction.powSel (F.par n).k ⋯ (F.par n).m (F.jm n) ⋯ ⋯

noncomputable def MIPRE.AnswerReduction.PcpFamily.sel' (F : PcpFamily) (n : ℕ) : LIDT.CL.Sel (Fq (F.par n) ⋯) (F.par n).m' ⋯

The selector of the sixth copy.

Equations

• F.sel' n = MIPRE.AnswerReduction.powSel (F.par n).k ⋯ (F.par n).m' (F.jm' n) ⋯ ⋯

noncomputable def MIPRE.AnswerReduction.PcpFamily.cl (F : PcpFamily) (n : ℕ) (t : Pcp.PcpTy) : CL.CLFun CL.𝔽₂ (Fin (Pcp.pcpDim (F.par n) * (F.par n).k)) 3

The downsized PCP presentation at index n.

Equations

• F.cl n t = MIPRE.AnswerReduction.pcpCl (F.par n) ⋯ (F.sel n) (F.sel' n) t

def MIPRE.AnswerReduction.PcpFamily.desc (F : PcpFamily) (n : ℕ) (c : Fin 6) : StageProg.Desc

The description of a copy: offset, length, selector width, seed.

Equations

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

def MIPRE.AnswerReduction.PcpFamily.pd (F : PcpFamily) (n : ℕ) : Cost.Data

The parameters at index n: k, m' and the six copies' descriptions, in unary.

Equations

• F.pd n = MIPRE.Cost.encode (MIPRE.Cost.unary (F.par n).k, MIPRE.Cost.unary (F.par n).m', List.ofFn (F.desc n))

Reading the parameters

noncomputable def MIPRE.AnswerReduction.rawListP : Cost.PolyTimeFun Cost.Data (List Cost.Data)

A list's elements' encodings.

Equations

• MIPRE.AnswerReduction.rawListP = MIPRE.Cost.PolyTimeFun.ofEncodeEq MIPRE.CL.Detyping.Program.rawList MIPRE.CL.Detyping.Program.encode_rawList

theorem MIPRE.AnswerReduction.rawList_encode {α : Type u_1} [Cost.SizedEncoding α] (l : List α) : CL.Detyping.Program.rawList (Cost.encode l) = List.map Cost.encode l

noncomputable def MIPRE.AnswerReduction.readU : Cost.PolyTimeFun Cost.Data Cost.Unary

A unary numeral.

Equations

• MIPRE.AnswerReduction.readU = (MIPRE.Cost.PolyTimeFun.const ()).map.comp MIPRE.AnswerReduction.rawListP

theorem MIPRE.AnswerReduction.readU_encode (u : Cost.Unary) : readU.toFun (Cost.encode u) = u

noncomputable def MIPRE.AnswerReduction.readDesc : Cost.PolyTimeFun Cost.Data StageProg.Desc

A copy's description.

Equations

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

theorem MIPRE.AnswerReduction.readDesc_encode (d : StageProg.Desc) : readDesc.toFun (Cost.encode d) = d

The answer program

noncomputable def MIPRE.AnswerReduction.pdI : Cost.PolyTimeFun CL.DirectInput Cost.Data

Equations

• MIPRE.AnswerReduction.pdI = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.AnswerReduction.tagI : Cost.PolyTimeFun CL.DirectInput Cost.Data

Equations

• MIPRE.AnswerReduction.tagI = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.AnswerReduction.kP : Cost.PolyTimeFun CL.DirectInput Cost.Unary

Equations

• MIPRE.AnswerReduction.kP = MIPRE.AnswerReduction.readU.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.AnswerReduction.pdI)

noncomputable def MIPRE.AnswerReduction.mP : Cost.PolyTimeFun CL.DirectInput Cost.Unary

Equations

• MIPRE.AnswerReduction.mP = MIPRE.AnswerReduction.readU.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.AnswerReduction.pdI))

noncomputable def MIPRE.AnswerReduction.descsP : Cost.PolyTimeFun CL.DirectInput (List Cost.Data)

Equations

• MIPRE.AnswerReduction.descsP = MIPRE.AnswerReduction.rawListP.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.AnswerReduction.pdI))

noncomputable def MIPRE.AnswerReduction.descP : Cost.PolyTimeFun CL.DirectInput StageProg.Desc

Equations

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

noncomputable def MIPRE.AnswerReduction.τP : Cost.PolyTimeFun CL.DirectInput ℕ

Equations

• MIPRE.AnswerReduction.τP = MIPRE.CL.Detyping.Program.readNat.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.AnswerReduction.tagI)

noncomputable def MIPRE.AnswerReduction.kindA : Cost.PolyTimeFun CL.DirectInput ℕ

Equations

• MIPRE.AnswerReduction.kindA = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.AnswerReduction.jA : Cost.PolyTimeFun CL.DirectInput ℕ

Equations

• MIPRE.AnswerReduction.jA = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.AnswerReduction.uA : Cost.PolyTimeFun CL.DirectInput Cost.BitStr

Equations

• MIPRE.AnswerReduction.uA = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)))

noncomputable def MIPRE.AnswerReduction.yA : Cost.PolyTimeFun CL.DirectInput Cost.BitStr

Equations

• MIPRE.AnswerReduction.yA = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)))

noncomputable def MIPRE.AnswerReduction.assemble : Cost.PolyTimeFun CL.DirectInput StageProg.Input

The copy program's input, read off a direct query.

Equations

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

noncomputable def MIPRE.AnswerReduction.answerProg : Cost.PolyTimeFun CL.DirectInput Cost.BitStr

The answer program of the PCP sampler: the copy program on the copy the type names.

Equations

• MIPRE.AnswerReduction.answerProg = MIPRE.AnswerReduction.StageProg.copyProg.comp MIPRE.AnswerReduction.assemble

noncomputable def MIPRE.AnswerReduction.dimProg : Cost.PolyTimeFun Cost.Data Cost.Unary

The dimension program: (2m' + 6) k in unary.

Equations

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

theorem MIPRE.AnswerReduction.PcpFamily.answerProg_apply (F : PcpFamily) (n : ℕ) (t : Pcp.PcpTy) (kind j : ℕ) (u y : Cost.BitStr) : answerProg.toFun (F.pd n, Cost.encode t, kind, j, u, y) = StageProg.copyAnswer (Cost.unary (F.par n).k) (F.desc n t.1) (StageProg.tyNat t.2) (Cost.unary (F.par n).m') kind j u y

theorem MIPRE.AnswerReduction.PcpFamily.dimProg_pd (F : PcpFamily) (n : ℕ) : List.length (dimProg.toFun (F.pd n)) = Pcp.pcpDim (F.par n) * (F.par n).k

theorem MIPRE.AnswerReduction.PcpFamily.le_lt (F : PcpFamily) (n : ℕ) (t : Pcp.PcpTy) (h : ↑t.1 < 5) : ↑t.1 * (F.par n).m + (F.par n).m ≤ (F.par n).m'

theorem MIPRE.AnswerReduction.PcpFamily.pres_lt (F : PcpFamily) (n : ℕ) (t : Pcp.PcpTy) (h : ↑t.1 < 5) : Pcp.pres (F.par n) (F.sel n) (F.sel' n) t = (Pcp.regsAt (F.par n) (↑t.1 * (F.par n).m) (F.par n).m t.1 ⋯).pres (F.sel n) t.2

theorem MIPRE.AnswerReduction.PcpFamily.pres_ge (F : PcpFamily) (n : ℕ) (t : Pcp.PcpTy) (h : ¬↑t.1 < 5) : Pcp.pres (F.par n) (F.sel n) (F.sel' n) t = (Pcp.regsAt (F.par n) 0 (F.par n).m' t.1 ⋯).pres (F.sel' n) t.2

theorem MIPRE.AnswerReduction.PcpFamily.desc_lt (F : PcpFamily) (n : ℕ) (c : Fin 6) (h : ↑c < 5) : F.desc n c = (Cost.unary (↑c * (F.par n).m), Cost.unary (F.par n).m, Cost.unary (F.jm n), Cost.unary ↑c)

theorem MIPRE.AnswerReduction.PcpFamily.desc_ge (F : PcpFamily) (n : ℕ) (c : Fin 6) (h : ¬↑c < 5) : F.desc n c = (Cost.unary 0, Cost.unary (F.par n).m', Cost.unary (F.jm' n), Cost.unary ↑c)

theorem MIPRE.AnswerReduction.PcpFamily.answer_marginal (F : PcpFamily) (n : ℕ) (t : Pcp.PcpTy) {j : ℕ} (hj : 1 ≤ j) (v : Pcp.Coord (F.par n) → Fq (F.par n) ⋯) : answerProg.toFun (F.pd n, Cost.encode t, 1, j, Pcp.flatBits (F.par n) ⋯ v, []) = Pcp.flatBits (F.par n) ⋯ ((CL.CLFun.truncate j (Pcp.pres (F.par n) (F.sel n) (F.sel' n) t)).eval v)

The marginals, by the copy the type names.

theorem MIPRE.AnswerReduction.PcpFamily.answer_linear (F : PcpFamily) (n : ℕ) (t : Pcp.PcpTy) {j : ℕ} (hj : 1 ≤ j) (u y : Pcp.Coord (F.par n) → Fq (F.par n) ⋯) : answerProg.toFun (F.pd n, Cost.encode t, 2, j, Pcp.flatBits (F.par n) ⋯ u, Pcp.flatBits (F.par n) ⋯ y) = Pcp.flatBits (F.par n) ⋯ (((Pcp.pres (F.par n) (F.sel n) (F.sel' n) t).mapOfPrefix (j - 1) u) y)

The stage maps, by the copy the type names.

theorem MIPRE.AnswerReduction.PcpFamily.answer_factor (F : PcpFamily) (n : ℕ) (t : Pcp.PcpTy) {j : ℕ} (hj : 1 ≤ j) (u : Pcp.Coord (F.par n) → Fq (F.par n) ⋯) : answerProg.toFun (F.pd n, Cost.encode t, 3, j, Pcp.flatBits (F.par n) ⋯ u, []) = StageProg.flatInd (F.par n) (F.par n).k ((Pcp.pres (F.par n) (F.sel n) (F.sel' n) t).factorOfPrefix (j - 1) u)

The factor spaces, by the copy the type names.

theorem MIPRE.AnswerReduction.PcpFamily.exists_flatBits_of_toBits (F : PcpFamily) (n : ℕ) {j : ℕ} (t : Pcp.PcpTy) (x : Fin (Pcp.pcpDim (F.par n) * (F.par n).k) → CL.𝔽₂) : ∃ (u : Pcp.Coord (F.par n) → (SAT.shoupBinField (F.par n).k ⋯).carrier), CL.toBits ((CL.CLFun.truncate j (F.cl n t)).eval x) = Pcp.flatBits (F.par n) ⋯ u

noncomputable def MIPRE.AnswerReduction.PcpFamily.directSampler (F : PcpFamily) (pp : Cost.Prog) (hpp : Cost.Prog.WellScoped 1 pp) (hruns : ∀ (n : ℕ), ∃ (t : ℕ), pp.Runs (Cost.encode n) (F.pd n) t) : CL.DirectSampler 3 Pcp.PcpTy

The PCP sampler, directly answered, given a routine computing its parameters.

Equations

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