The binary CL family of the answer-reduced sampler

Piece AR-3c of planning/answer-reduction.md: the typed CL functions of the answer-reduced sampler Ŝ^ar (sec:ar-verifier, ld_compiler.tex), over 𝔽₂, one for each type (r, t) ∈ Role × PcpTy.

• The PCP half is downsized along the Shoup polynomial basis (pcpBin), whose coordinates are the field elements' bits fld.toBits, the representation the PCP verifier reads (shoupCoordinateEquiv_encoding). This is finding 1 of the plan: questions need no change of basis before the PCP verifier sees them. Its bits are numbered by Pcp.bitIndex (pcpCl).
• The oracle half is the oracularized sampler's roleFamily of the input sampler.
• Both are padded to L = max (ℓ + 1) 3 levels and put side by side, the oracle half first (cl, the product CLFun.prodCL of MIPRE/Foundations/CL/ProductSampler).

cl_exactlyOn is the exactness a CL.TypedSampler asks for, and oraclePart_eval, pcpPart_eval say what the question of a type carries: the oracle's question in the oracle coordinates, the downsized PCP question in the others.

The family

@[reducible, inline]

abbrev MIPRE.AnswerReduction.Fq (P : SAT.PcpParams) (hk : 1 ≤ P.k) : Type

The field of the PCP, F_q with q = 2^k, in its Shoup representation.

Equations

• MIPRE.AnswerReduction.Fq P hk = (MIPRE.SAT.shoupBinField P.k hk).carrier

@[reducible, inline]

noncomputable abbrev MIPRE.AnswerReduction.basis (P : SAT.PcpParams) (hk : 1 ≤ P.k) : Module.Basis (Fin P.k) (ZMod 2) (Fq P hk)

The Shoup polynomial basis of F_q over 𝔽₂: its coordinates are the bits of an element.

Equations

• MIPRE.AnswerReduction.basis P hk = MIPRE.SAT.shoupPowerBasis P.k hk

@[reducible, inline]

abbrev MIPRE.AnswerReduction.level (ℓ : ℕ) : ℕ

The common level max (ℓ + 1) 3.

Equations

• MIPRE.AnswerReduction.level ℓ = max (ℓ + 1) 3

@[reducible, inline]

abbrev MIPRE.AnswerReduction.dim {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) : ℕ

The dimension of the answer-reduced sampler at index n.

Equations

• MIPRE.AnswerReduction.dim V n P = V.sampler.dim n + MIPRE.AnswerReduction.Pcp.pcpDim P * P.k

noncomputable def MIPRE.AnswerReduction.pcpBin (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) : CL.CLFun CL.𝔽₂ (Pcp.Coord P × Fin P.k) 3

The downsized PCP presentation of a PCP type.

Equations

• MIPRE.AnswerReduction.pcpBin P hk S S' t = MIPRE.CL.CLFun.downsize (MIPRE.AnswerReduction.basis P hk) (MIPRE.AnswerReduction.Pcp.pres P S S' t)

noncomputable def MIPRE.AnswerReduction.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) : CL.CLFun CL.𝔽₂ (Fin (Pcp.pcpDim P * P.k)) 3

The downsized PCP presentation, on the numbered bits.

Equations

• MIPRE.AnswerReduction.pcpCl P hk S S' t = MIPRE.CL.CLFun.reindex (MIPRE.AnswerReduction.Pcp.bitIndex P P.k) (MIPRE.AnswerReduction.pcpBin P hk S S' t)

noncomputable def MIPRE.AnswerReduction.cl {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (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') (rt : Role × Pcp.PcpTy) : CL.CLFun CL.𝔽₂ (Fin (dim V n P)) (level ℓ)

The typed CL function of the answer-reduced sampler at the type rt: the oracle half on the first coordinates, the PCP half on the rest, at the common level.

Equations

• MIPRE.AnswerReduction.cl V n P hk S S' rt = MIPRE.CL.CLFun.prodCL (MIPRE.AnswerReduction.level ℓ) (MIPRE.roleFamily (V.sampler.cl n) rt.1) (MIPRE.AnswerReduction.pcpCl P hk S S' rt.2) ⋯ ⋯

theorem MIPRE.AnswerReduction.pcpBin_exactlyOn (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) : (pcpBin P hk S S' t).ExactlyOn Finset.univ

theorem MIPRE.AnswerReduction.pcpCl_exactlyOn (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) : (pcpCl P hk S S' t).ExactlyOn Finset.univ

theorem MIPRE.AnswerReduction.cl_exactlyOn {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (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') (rt : Role × Pcp.PcpTy) : (cl V n P hk S S' rt).ExactlyOn Finset.univ

theorem MIPRE.AnswerReduction.pcpCl_eval (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) (v : Pcp.Coord P → Fq P hk) : (pcpCl P hk S S' t).eval ((CL.reindexEquiv (Pcp.bitIndex P P.k)) ((CL.downsizeEquiv (basis P hk)) v)) = (CL.reindexEquiv (Pcp.bitIndex P P.k)) ((CL.downsizeEquiv (basis P hk)) ((Pcp.pres P S S' t).eval v))

What a question carries

def MIPRE.AnswerReduction.oraclePart {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (y : Fin (dim V n P) → CL.𝔽₂) : Fin (V.sampler.dim n) → CL.𝔽₂

The oracle coordinates of a vector.

Equations

• MIPRE.AnswerReduction.oraclePart V n P y = MIPRE.CL.leftPart y

noncomputable def MIPRE.AnswerReduction.pcpPart {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) (y : Fin (dim V n P) → CL.𝔽₂) : Pcp.Coord P → Fq P hk

The PCP coordinates of a vector, read back as a vector of V^pcp.

Equations

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

theorem MIPRE.AnswerReduction.eval_cl {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (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') (rt : Role × Pcp.PcpTy) (y : Fin (dim V n P) → CL.𝔽₂) : (cl V n P hk S S' rt).eval y = Fin.append ((roleFamily (V.sampler.cl n) rt.1).eval (CL.leftPart y)) ((pcpCl P hk S S' rt.2).eval (CL.rightPart y))

theorem MIPRE.AnswerReduction.oraclePart_eval {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (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') (rt : Role × Pcp.PcpTy) (y : Fin (dim V n P) → CL.𝔽₂) : oraclePart V n P ((cl V n P hk S S' rt).eval y) = (roleFamily (V.sampler.cl n) rt.1).eval (oraclePart V n P y)

The oracle half of a question is the oracularized sampler's question.

theorem MIPRE.AnswerReduction.pcpPart_eval {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (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') (rt : Role × Pcp.PcpTy) (y : Fin (dim V n P) → CL.𝔽₂) : pcpPart V n P hk ((cl V n P hk S S' rt).eval y) = (Pcp.pres P S S' rt.2).eval (pcpPart V n P hk y)

The PCP half of a question is the PCP presentation's question.