Documentation

MIPRE.Tailored.AnsRed.Slots

The polynomials of a PCP, slot by slot #

The answer-reduced game (defn:combi_ans_red, II:10285) asks the oracle for a PCP evaluated at a point or restricted to a line, and the isolated players for two of its polynomials: Alice for the two assignments g_A, g_{La} of the first answer, Bob for those of the second (Table tab:Answer_Lengths_combinatorial_ans_red). This file names the polynomials of a PCP (Pcp), so that the game can list them as codewords and compare them across players.

Slot L: one slot for each polynomial of a PCP of layout L, with its readability (Slot.readable), the number of its variables (Slot.size) and their place among the PCP's (Slot.emb, the blocks of Definition defn:blocks_of_vars_circuit).
The codewords of a role (slotsOf), readable first: the oracle's are all the slots (oSlots, heartsuit = ♥^R + ♥^L of eq:def_heartsuit), an isolated player's the two of its answer.
A PCP's polynomial in a slot (Pcp.slot), its value at a point (Pcp.slotEval), and the thirteen checks on slot values (PassesV), which are the checks of Pcp.Passes (passes_iff_passesV), split into the part on readable values (PassesR) and the part the linear values enter (PassesL).
From polynomials on more variables that each depend only on their slot's block — what the game's indifference check guarantees — the PCP they are (Pcp.ofPolys): its slots, renamed back, are the given polynomials (rename_ofPolys_slot), so its values are theirs.

inductive MIPRE.Tailored.AnsRed.Slot (L : PcpDims) :

The slots of a PCP (Definition defn:PCP_of_V_n_satisfied): one for each polynomial, the readable ones first.

gA {L : PcpDims} : Slot L
gB {L : PcpDims} : Slot L
gO {L : PcpDims} : Slot L
gW {L : PcpDims} (k : Fin 3) : Slot L
αR {L : PcpDims} (X : Fin L.m) : Slot L
βA {L : PcpDims} (i : Fin L.ℓ) : Slot L
βB {L : PcpDims} (i : Fin L.ℓ) : Slot L
βO {L : PcpDims} (i : Fin L.oW) : Slot L
βW {L : PcpDims} (k : Fin 3) (i : Fin L.r) : Slot L
gLa {L : PcpDims} : Slot L
gLb {L : PcpDims} : Slot L
gL {L : PcpDims} (k : Fin 3) : Slot L
αL {L : PcpDims} (X : Fin L.oW) : Slot L
βLa {L : PcpDims} (i : Fin L.ℓ) : Slot L
βLb {L : PcpDims} (i : Fin L.ℓ) : Slot L
βL {L : PcpDims} (k : Fin 3) (i : Fin L.dm) : Slot L

Instances For

@[instance_reducible]

instance MIPRE.Tailored.AnsRed.instDecidableEqSlot {L✝ : PcpDims} :

DecidableEq (Slot L✝)

Equations

MIPRE.Tailored.AnsRed.instDecidableEqSlot = MIPRE.Tailored.AnsRed.instDecidableEqSlot.decEq

def MIPRE.Tailored.AnsRed.instDecidableEqSlot.decEq {L✝ : PcpDims} (x✝ x✝¹ : Slot L✝) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

def MIPRE.Tailored.AnsRed.Slot.readable {L : PcpDims} :

Slot L → Bool

Whether a slot is readable: the paper's Π^R.

Equations

Instances For

def MIPRE.Tailored.AnsRed.Slot.size {L : PcpDims} :

Slot L → ℕ

The number of variables of a slot's polynomial.

Equations

Instances For

def MIPRE.Tailored.AnsRed.Slot.emb {L : PcpDims} (s : Slot L) :

Fin s.size → Fin L.m

The block of a slot: where its variables sit among the PCP's.

Equations

MIPRE.Tailored.AnsRed.Slot.gA.emb = L.vA
(MIPRE.Tailored.AnsRed.Slot.βA i).emb = L.vA
MIPRE.Tailored.AnsRed.Slot.gB.emb = L.vB
(MIPRE.Tailored.AnsRed.Slot.βB i).emb = L.vB
MIPRE.Tailored.AnsRed.Slot.gO.emb = L.vO
(MIPRE.Tailored.AnsRed.Slot.βO i).emb = L.vO
(MIPRE.Tailored.AnsRed.Slot.αL X).emb = L.vO
(MIPRE.Tailored.AnsRed.Slot.gW k).emb = L.vW k
(MIPRE.Tailored.AnsRed.Slot.βW k i).emb = L.vW k
(MIPRE.Tailored.AnsRed.Slot.αR X).emb = id
MIPRE.Tailored.AnsRed.Slot.gLa.emb = L.vO ∘ L.oA
(MIPRE.Tailored.AnsRed.Slot.βLa i).emb = L.vO ∘ L.oA
MIPRE.Tailored.AnsRed.Slot.gLb.emb = L.vO ∘ L.oB
(MIPRE.Tailored.AnsRed.Slot.βLb i).emb = L.vO ∘ L.oB
(MIPRE.Tailored.AnsRed.Slot.gL k).emb = L.vO ∘ L.oL k
(MIPRE.Tailored.AnsRed.Slot.βL k i).emb = L.vO ∘ L.oL k

Instances For

theorem MIPRE.Tailored.AnsRed.Slot.emb_injective {L : PcpDims} (s : Slot L) :

Function.Injective s.emb

The codewords of the roles #

def MIPRE.Tailored.AnsRed.rSlots (L : PcpDims) :

The readable slots, in the order of the oracle's codewords.

Equations

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

Instances For

def MIPRE.Tailored.AnsRed.lSlots (L : PcpDims) :

The linear slots, in the order of the oracle's codewords.

Equations

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

Instances For

def MIPRE.Tailored.AnsRed.rOf (L : PcpDims) :

Role → List (Slot L)

The readable codewords of a role: all the readable slots for the oracle, g_A for Alice and g_B for Bob.

Equations

Instances For

def MIPRE.Tailored.AnsRed.lOf (L : PcpDims) :

Role → List (Slot L)

The linear codewords of a role: all the linear slots for the oracle, g_{La} for Alice and g_{Lb} for Bob.

Equations

Instances For

def MIPRE.Tailored.AnsRed.slotsOf (L : PcpDims) (r : Role) :

The codewords of a role, readable first.

Equations

MIPRE.Tailored.AnsRed.slotsOf L r = MIPRE.Tailored.AnsRed.rOf L r ++ MIPRE.Tailored.AnsRed.lOf L r

Instances For

theorem MIPRE.Tailored.AnsRed.readable_of_mem_rSlots {L : PcpDims} {s : Slot L} (h : s ∈ rSlots L) :

s.readable = true

theorem MIPRE.Tailored.AnsRed.not_readable_of_mem_lSlots {L : PcpDims} {s : Slot L} (h : s ∈ lSlots L) :

s.readable = false

theorem MIPRE.Tailored.AnsRed.readable_of_mem_rOf {L : PcpDims} {r : Role} {s : Slot L} (h : s ∈ rOf L r) :

s.readable = true

theorem MIPRE.Tailored.AnsRed.not_readable_of_mem_lOf {L : PcpDims} {r : Role} {s : Slot L} (h : s ∈ lOf L r) :

s.readable = false

theorem MIPRE.Tailored.AnsRed.mem_slotsOf_oracle {L : PcpDims} (s : Slot L) :

s ∈ slotsOf L Role.oracle

Every slot is a codeword of the oracle.

theorem MIPRE.Tailored.AnsRed.mem_rSlots_of_readable {L : PcpDims} {s : Slot L} (h : s.readable = true) :

Positions among the oracle's codewords #

def MIPRE.Tailored.AnsRed.idxO {L : PcpDims} (s : Slot L) :

The position of a slot among the oracle's codewords.

Equations

MIPRE.Tailored.AnsRed.idxO s = List.idxOf s (MIPRE.Tailored.AnsRed.slotsOf L MIPRE.Role.oracle)

Instances For

theorem MIPRE.Tailored.AnsRed.idxO_lt {L : PcpDims} (s : Slot L) :

idxO s < (slotsOf L Role.oracle).length

theorem MIPRE.Tailored.AnsRed.getElem_idxO {L : PcpDims} (s : Slot L) :

(slotsOf L Role.oracle)[idxO s] = s

theorem MIPRE.Tailored.AnsRed.idxO_lt_of_readable {L : PcpDims} {s : Slot L} (h : s.readable = true) :

idxO s < (rSlots L).length

A readable slot sits among the oracle's readable codewords.

theorem MIPRE.Tailored.AnsRed.readable_getElem_slotsOf {L : PcpDims} (r : Role) {c : ℕ} (hc : c < (slotsOf L r).length) :

(slotsOf L r)[c].readable = true ↔ c < (rOf L r).length

A codeword of a role is readable exactly when it is among the role's readable ones.

theorem MIPRE.Tailored.AnsRed.length_rSlots {L : PcpDims} :

(rSlots L).length = 6 + L.m + L.ℓ + L.ℓ + L.oW + 3 * L.r

theorem MIPRE.Tailored.AnsRed.length_lSlots {L : PcpDims} :

(lSlots L).length = 5 + L.oW + L.ℓ + L.ℓ + 3 * L.dm

A PCP's slots #

def MIPRE.Tailored.AnsRed.Pcp.slot {L : PcpDims} {F : Type u_1} [CommRing F] (P : Pcp L F) (s : Slot L) :

MvPolynomial (Fin s.size) F

A PCP's polynomial in a slot, on the slot's variables.

Equations

P.slot MIPRE.Tailored.AnsRed.Slot.gA = P.gA
P.slot MIPRE.Tailored.AnsRed.Slot.gB = P.gB
P.slot MIPRE.Tailored.AnsRed.Slot.gO = P.gO
P.slot (MIPRE.Tailored.AnsRed.Slot.gW k) = P.gW k
P.slot (MIPRE.Tailored.AnsRed.Slot.αR X) = P.αR X
P.slot (MIPRE.Tailored.AnsRed.Slot.βA i) = P.βA i
P.slot (MIPRE.Tailored.AnsRed.Slot.βB i) = P.βB i
P.slot (MIPRE.Tailored.AnsRed.Slot.βO i) = P.βO i
P.slot (MIPRE.Tailored.AnsRed.Slot.βW k i) = P.βW k i
P.slot MIPRE.Tailored.AnsRed.Slot.gLa = P.gLa
P.slot MIPRE.Tailored.AnsRed.Slot.gLb = P.gLb
P.slot (MIPRE.Tailored.AnsRed.Slot.gL k) = P.gL k
P.slot (MIPRE.Tailored.AnsRed.Slot.αL X) = P.αL X
P.slot (MIPRE.Tailored.AnsRed.Slot.βLa i) = P.βLa i
P.slot (MIPRE.Tailored.AnsRed.Slot.βLb i) = P.βLb i
P.slot (MIPRE.Tailored.AnsRed.Slot.βL k i) = P.βL k i

Instances For

def MIPRE.Tailored.AnsRed.Pcp.slotEval {L : PcpDims} {F : Type u_1} [CommRing F] (P : Pcp L F) (p : Fin L.m → F) (s : Slot L) :

F

A PCP's value in a slot at a point of the PCP's variables.

Equations

P.slotEval p s = (MvPolynomial.eval (p ∘ s.emb)) (P.slot s)

Instances For

noncomputable def MIPRE.Tailored.AnsRed.Pcp.slotPoly {L : PcpDims} {F : Type u_1} [CommRing F] (P : Pcp L F) (s : Slot L) :

MvPolynomial (Fin L.m) F

A PCP's polynomial in a slot, on all the PCP's variables.

Equations

P.slotPoly s = (MvPolynomial.rename s.emb) (P.slot s)

Instances For

theorem MIPRE.Tailored.AnsRed.Pcp.eval_slotPoly {L : PcpDims} {F : Type u_1} [CommRing F] (P : Pcp L F) (p : Fin L.m → F) (s : Slot L) :

(MvPolynomial.eval p) (P.slotPoly s) = P.slotEval p s

def MIPRE.Tailored.AnsRed.FormulaCheckV {L : PcpDims} {F : Type u_1} [CommRing F] (T : MvPolynomial (Fin L.m) F) (w : Slot L → F) (p : Fin L.m → F) :

The formula check on the values of the slots at a point.

Equations

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

Instances For

def MIPRE.Tailored.AnsRed.SystemCheckV {L : PcpDims} {F : Type u_1} [CommRing F] (w : Slot L → F) (x : Fin L.oW → F) :

The system check on the values of the slots at a point of the index space of O.

Equations

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

Instances For

def MIPRE.Tailored.AnsRed.AssignCheckV {F : Type u_1} [CommRing F] {k : ℕ} (g : F) (β x : Fin k → F) :

An assignment check on values: g (1 - g) is the certificate sum at x.

Equations

MIPRE.Tailored.AnsRed.AssignCheckV g β x = (g * (1 - g) = ∑ i : Fin k, x i * (1 - x i) * β i)

Instances For

def MIPRE.Tailored.AnsRed.PassesV {L : PcpDims} {F : Type u_1} [CommRing F] (T : MvPolynomial (Fin L.m) F) (w : Slot L → F) (p : Fin L.m → F) :

The thirteen checks on the values of the slots at a point, in the order of Pcp.Passes.

Equations

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

Instances For

theorem MIPRE.Tailored.AnsRed.passes_iff_passesV {L : PcpDims} {F : Type u_1} [CommRing F] (T : MvPolynomial (Fin L.m) F) (P : Pcp L F) (p : Fin L.m → F) :

Pcp.Passes T P p ↔ PassesV T (P.slotEval p) p

The checks of a PCP at a point are the checks on its values there.

def MIPRE.Tailored.AnsRed.PassesR {L : PcpDims} {F : Type u_1} [CommRing F] (T : MvPolynomial (Fin L.m) F) (w : Slot L → F) (p : Fin L.m → F) :

The checks on the readable values: the formula check and the readable assignment checks.

Equations

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

Instances For

def MIPRE.Tailored.AnsRed.PassesL {L : PcpDims} {F : Type u_1} [CommRing F] (w : Slot L → F) (p : Fin L.m → F) :

The checks the linear values enter: the system check and the linear assignment checks.

Equations

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

Instances For

@[instance_reducible]

instance MIPRE.Tailored.AnsRed.instDecidablePassesROfDecidableEq {L : PcpDims} {F : Type u_1} [CommRing F] [DecidableEq F] (T : MvPolynomial (Fin L.m) F) (w : Slot L → F) (p : Fin L.m → F) :

Decidable (PassesR T w p)

Equations

MIPRE.Tailored.AnsRed.instDecidablePassesROfDecidableEq T w p = id (id (id inferInstance))

theorem MIPRE.Tailored.AnsRed.passesV_iff {L : PcpDims} {F : Type u_1} [CommRing F] (T : MvPolynomial (Fin L.m) F) (w : Slot L → F) (p : Fin L.m → F) :

PassesV T w p ↔ PassesR T w p ∧ PassesL w p

theorem MIPRE.Tailored.AnsRed.passesR_congr {L : PcpDims} {F : Type u_1} [CommRing F] (T : MvPolynomial (Fin L.m) F) {w w' : Slot L → F} (p : Fin L.m → F) (h : ∀ (s : Slot L), s.readable = true → w s = w' s) :

PassesR T w p ↔ PassesR T w' p

The readable checks read only readable values.

The PCP of block-local polynomials #

noncomputable def MIPRE.Tailored.AnsRed.slotOf {L : PcpDims} {F : Type u_1} [CommRing F] {N : ℕ} (ι : Fin L.m → Fin N) (hι : Function.Injective ι) (s : Slot L) (g : MvPolynomial (Fin N) F) :

MvPolynomial (Fin s.size) F

The polynomial on a slot's variables that a polynomial on N variables is, when it depends only on the slot's block (placed among the N variables by ι).

Equations

MIPRE.Tailored.AnsRed.slotOf ι hι s g = (MvPolynomial.killCompl ⋯) g

Instances For

noncomputable def MIPRE.Tailored.AnsRed.Pcp.ofPolys {L : PcpDims} {F : Type u_1} [CommRing F] {N : ℕ} (ι : Fin L.m → Fin N) (hι : Function.Injective ι) (f : Slot L → MvPolynomial (Fin N) F) :

Pcp L F

The PCP of a family of polynomials on N variables, one per slot, each read on its slot's block.

Equations

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

Instances For

theorem MIPRE.Tailored.AnsRed.Pcp.slot_ofPolys {L : PcpDims} {F : Type u_1} [CommRing F] {N : ℕ} (ι : Fin L.m → Fin N) (hι : Function.Injective ι) (f : Slot L → MvPolynomial (Fin N) F) (s : Slot L) :

(ofPolys ι hι f).slot s = slotOf ι hι s (f s)

theorem MIPRE.Tailored.AnsRed.rename_slotOf {L : PcpDims} {F : Type u_1} [CommRing F] {N : ℕ} (ι : Fin L.m → Fin N) (hι : Function.Injective ι) {s : Slot L} {g : MvPolynomial (Fin N) F} (hg : ↑g.vars ⊆ Set.range (ι ∘ s.emb)) :

(MvPolynomial.rename (ι ∘ s.emb)) (slotOf ι hι s g) = g

A polynomial that depends only on a slot's block is the renaming of its reading there.

theorem MIPRE.Tailored.AnsRed.rename_ofPolys_slot {L : PcpDims} {F : Type u_1} [CommRing F] {N : ℕ} (ι : Fin L.m → Fin N) (hι : Function.Injective ι) {f : Slot L → MvPolynomial (Fin N) F} (hf : ∀ (s : Slot L), ↑(f s).vars ⊆ Set.range (ι ∘ s.emb)) (s : Slot L) :

(MvPolynomial.rename (ι ∘ s.emb)) ((Pcp.ofPolys ι hι f).slot s) = f s

The slots of the PCP of block-local polynomials, renamed back, are the polynomials.

theorem MIPRE.Tailored.AnsRed.slotEval_ofPolys {L : PcpDims} {F : Type u_1} [CommRing F] {N : ℕ} (ι : Fin L.m → Fin N) (hι : Function.Injective ι) {f : Slot L → MvPolynomial (Fin N) F} (hf : ∀ (s : Slot L), ↑(f s).vars ⊆ Set.range (ι ∘ s.emb)) (u : Fin N → F) (s : Slot L) :

(Pcp.ofPolys ι hι f).slotEval (u ∘ ι) s = (MvPolynomial.eval u) (f s)

The values of the PCP of block-local polynomials are theirs.

theorem MIPRE.Tailored.AnsRed.indDeg_ofPolys {L : PcpDims} {F : Type u_1} [CommRing F] {N : ℕ} (ι : Fin L.m → Fin N) (hι : Function.Injective ι) {f : Slot L → MvPolynomial (Fin N) F} (hf : ∀ (s : Slot L), ↑(f s).vars ⊆ Set.range (ι ∘ s.emb)) {d : ℕ} (hd : ∀ (s : Slot L) (i : Fin N), MvPolynomial.degreeOf i (f s) ≤ d) :

(Pcp.ofPolys ι hι f).IndDeg d

The PCP of block-local polynomials of individual degree at most d has degree at most d.