Documentation

MIPRE.Tailored.AnsRed.SlotIndex

The positions of the slots among the oracle's codewords #

The oracle's answer in the answer-reduced game lists a codeword for every slot of the PCP, the readable ones first (slotsOf), and a slot's codeword sits at its position idxO. The linear-constraints processor reads the codewords at these positions, so they are computed here in closed form: the readable slots in the order of rSlots, then the linear ones in the order of lSlots, after the 6 + m + 2ℓ + ◇' + 3r readable ones (idxO_gA, …, idxO_βL). The isolated players' codewords are g_A, g_{La} and g_B, g_{Lb} (slotsOf_alice, slotsOf_bob).

source
theorem MIPRE.Tailored.AnsRed.idxOf_ofFn {α : Type u_1} [DecidableEq α] {n : ℕ} {f : Fin n → α} (hf : Function.Injective f) (i : Fin n) :
List.idxOf (f i) (List.ofFn f) = ↑i
source
theorem MIPRE.Tailored.AnsRed.finRange3_flatMap {α : Type u_1} (g : Fin 3 → List α) :
List.flatMap g (List.finRange 3) = g 0 ++ (g 1 ++ g 2)
source
theorem MIPRE.Tailored.AnsRed.idxOf_gW (L : PcpDims) (k : Fin 3) :
List.idxOf (Slot.gW k) (List.ofFn Slot.gW) = ↑k
source
theorem MIPRE.Tailored.AnsRed.idxOf_αR (L : PcpDims) (X : Fin L.m) :
List.idxOf (Slot.αR X) (List.ofFn Slot.αR) = ↑X
source
theorem MIPRE.Tailored.AnsRed.idxOf_βA (L : PcpDims) (i : Fin L.ℓ) :
List.idxOf (Slot.βA i) (List.ofFn Slot.βA) = ↑i
source
theorem MIPRE.Tailored.AnsRed.idxOf_βB (L : PcpDims) (i : Fin L.ℓ) :
List.idxOf (Slot.βB i) (List.ofFn Slot.βB) = ↑i
source
theorem MIPRE.Tailored.AnsRed.idxOf_βO (L : PcpDims) (i : Fin L.oW) :
List.idxOf (Slot.βO i) (List.ofFn Slot.βO) = ↑i
source
theorem MIPRE.Tailored.AnsRed.idxOf_βW (L : PcpDims) (k : Fin 3) (i : Fin L.r) :
List.idxOf (Slot.βW k i) (List.ofFn (Slot.βW k)) = ↑i
source
theorem MIPRE.Tailored.AnsRed.idxOf_gL (L : PcpDims) (k : Fin 3) :
List.idxOf (Slot.gL k) (List.ofFn Slot.gL) = ↑k
source
theorem MIPRE.Tailored.AnsRed.idxOf_αL (L : PcpDims) (X : Fin L.oW) :
List.idxOf (Slot.αL X) (List.ofFn Slot.αL) = ↑X
source
theorem MIPRE.Tailored.AnsRed.idxOf_βLa (L : PcpDims) (i : Fin L.ℓ) :
List.idxOf (Slot.βLa i) (List.ofFn Slot.βLa) = ↑i
source
theorem MIPRE.Tailored.AnsRed.idxOf_βLb (L : PcpDims) (i : Fin L.ℓ) :
List.idxOf (Slot.βLb i) (List.ofFn Slot.βLb) = ↑i
source
theorem MIPRE.Tailored.AnsRed.idxOf_βL (L : PcpDims) (k : Fin 3) (i : Fin L.dm) :
List.idxOf (Slot.βL k i) (List.ofFn (Slot.βL k)) = ↑i
source
def MIPRE.Tailored.AnsRed.tacticSlot_idx :
Lean.ParserDescr

The simp set that computes positions of slots in the oracle's codewords.

Equations
Instances For

    The readable slots #

    source
    @[simp]
    theorem MIPRE.Tailored.AnsRed.idxO_gA {L : PcpDims} :
    idxO Slot.gA = 0
    source
    @[simp]
    theorem MIPRE.Tailored.AnsRed.idxO_gB {L : PcpDims} :
    idxO Slot.gB = 1
    source
    @[simp]
    theorem MIPRE.Tailored.AnsRed.idxO_gO {L : PcpDims} :
    idxO Slot.gO = 2
    source
    theorem MIPRE.Tailored.AnsRed.idxO_gW {L : PcpDims} (k : Fin 3) :
    idxO (Slot.gW k) = 3 + ↑k
    source
    theorem MIPRE.Tailored.AnsRed.idxO_αR {L : PcpDims} (X : Fin L.m) :
    idxO (Slot.αR X) = 6 + ↑X
    source
    theorem MIPRE.Tailored.AnsRed.idxO_βA {L : PcpDims} (i : Fin L.ℓ) :
    idxO (Slot.βA i) = 6 + L.m + ↑i
    source
    theorem MIPRE.Tailored.AnsRed.idxO_βB {L : PcpDims} (i : Fin L.ℓ) :
    idxO (Slot.βB i) = 6 + L.m + L.ℓ + ↑i
    source
    theorem MIPRE.Tailored.AnsRed.idxO_βO {L : PcpDims} (i : Fin L.oW) :
    idxO (Slot.βO i) = 6 + L.m + L.ℓ + L.ℓ + ↑i
    source
    theorem MIPRE.Tailored.AnsRed.idxO_βW {L : PcpDims} (k : Fin 3) (i : Fin L.r) :
    idxO (Slot.βW k i) = 6 + L.m + L.ℓ + L.ℓ + L.oW + ↑k * L.r + ↑i

    The linear slots #

    source
    theorem MIPRE.Tailored.AnsRed.idxO_gLa {L : PcpDims} :
    idxO Slot.gLa = (rSlots L).length
    source
    theorem MIPRE.Tailored.AnsRed.idxO_gLb {L : PcpDims} :
    idxO Slot.gLb = (rSlots L).length + 1
    source
    theorem MIPRE.Tailored.AnsRed.idxO_gL {L : PcpDims} (k : Fin 3) :
    idxO (Slot.gL k) = (rSlots L).length + 2 + ↑k
    source
    theorem MIPRE.Tailored.AnsRed.idxO_αL {L : PcpDims} (X : Fin L.oW) :
    idxO (Slot.αL X) = (rSlots L).length + 5 + ↑X
    source
    theorem MIPRE.Tailored.AnsRed.idxO_βLa {L : PcpDims} (i : Fin L.ℓ) :
    idxO (Slot.βLa i) = (rSlots L).length + 5 + L.oW + ↑i
    source
    theorem MIPRE.Tailored.AnsRed.idxO_βLb {L : PcpDims} (i : Fin L.ℓ) :
    idxO (Slot.βLb i) = (rSlots L).length + 5 + L.oW + L.ℓ + ↑i
    source
    theorem MIPRE.Tailored.AnsRed.idxO_βL {L : PcpDims} (k : Fin 3) (i : Fin L.dm) :
    idxO (Slot.βL k i) = (rSlots L).length + 5 + L.oW + L.ℓ + L.ℓ + ↑k * L.dm + ↑i

    The isolated players' codewords #

    source
    theorem MIPRE.Tailored.AnsRed.slotsOf_alice {L : PcpDims} :
    slotsOf L Role.alice = [Slot.gA, Slot.gLa]
    source
    theorem MIPRE.Tailored.AnsRed.slotsOf_bob {L : PcpDims} :
    slotsOf L Role.bob = [Slot.gB, Slot.gLb]

    The blocks of the slots #

    source
    def MIPRE.Tailored.AnsRed.Slot.lo {L : PcpDims} :
    Slot L → ℕ

    The first wire of a slot's block: each block is the interval of size wires from it.

    Equations
    Instances For
      source
      theorem MIPRE.Tailored.AnsRed.Slot.val_emb {L : PcpDims} (s : Slot L) (x : Fin s.size) :
      ↑(s.emb x) = s.lo + ↑x

      A slot's block is the interval of size wires from lo.

      source
      theorem MIPRE.Tailored.AnsRed.Slot.exists_emb_iff {L : PcpDims} (s : Slot L) (w : ℕ) :
      (∃ (x : Fin s.size), ↑(s.emb x) = w) ↔ s.lo ≤ w ∧ w < s.lo + s.size

      A wire lies in a slot's block exactly when it lies in its interval.