The consistency and indifference checks, as programs

Slice P4h of planning/aldous-lyons-track.md: the constraints of the consistency checks (Typed.consCons) and of the indifference checks (Typed.indCons) of the answer-reduced game, computed by programs from the parameters and the layout of the answers.

• copyF: the equations that listed codewords of one answer are listed codewords of the other (copyF_eq); consConsF lists the isolated player's two codewords against the oracle's in the same slots, at the positions idxO (consConsF_eq).
• indF: the equations that the coefficients 1, …, d of the codewords whose blocks miss a direction vanish (indF_eq), the blocks read off a table of intervals of wires (ivF, the blocks of MIPRE.Tailored.AnsRed.Slot.lo); indConsF at an axis-parallel line, in the direction its seed selects (indConsF_eq).

Copies of codewords

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.CopyIn : Type

The input of the copy equations: t, the number n of coefficients, the offsets oI and oO of the two answers, N, and the copied codewords (c, o_c): the c-th codeword of the first answer is the o_c-th of the second.

Equations

• MIPRE.Tailored.AnsRed.Typed.CopyIn = (MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × List (MIPRE.Cost.Unary × MIPRE.Cost.Unary))

noncomputable def MIPRE.Tailored.AnsRed.Typed.copyF : Cost.PolyTimeFun CopyIn (List Cost.BitStr)

The copy equations, as a program: at ((c, o_c), e), the window of coefficient e of the c-th codeword at oI plus that of the o_c-th at oO.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.copyF_eq {t : ℕ} {ht : 1 ≤ t} (n oI oO N : ℕ) (cws : List (ℕ × ℕ)) : copyF.toFun (Cost.unary t, Cost.unary n, Cost.unary oI, Cost.unary oO, Cost.unary N, List.map (fun (p : ℕ × ℕ) => (Cost.unary p.1, Cost.unary p.2)) cws) = eqsCons t ht (List.flatMap (fun (p : ℕ × ℕ) => List.map (fun (e : ℕ) => (Intro.fldAt t ht N (oI + (p.1 * n + e) * t) - Intro.fldAt t ht N (oO + (p.2 * n + e) * t), 0)) (List.range n)) cws)

The copy program computes the copy equations.

The consistency checks

theorem MIPRE.Tailored.AnsRed.Typed.consEqs_alice {t : ℕ} {ht : 1 ≤ t} {L : PcpDims} (N oI oO n : ℕ) : consEqs L N oI oO n Role.alice = List.flatMap (fun (p : ℕ × ℕ) => List.map (fun (e : ℕ) => (Intro.fldAt t ht N (oI + (p.1 * n + e) * t) - Intro.fldAt t ht N (oO + (p.2 * n + e) * t), 0)) (List.range n)) [(0, 0), (1, (rSlots L).length)]

An isolated player's copy equations: its two codewords against the oracle's in the same slots, g_A, g_{La} at the oracle's positions 0 and R for Alice, g_B, g_{Lb} at 1 and R + 1 for Bob, R the oracle's readable count.

theorem MIPRE.Tailored.AnsRed.Typed.consEqs_bob {t : ℕ} {ht : 1 ≤ t} {L : PcpDims} (N oI oO n : ℕ) : consEqs L N oI oO n Role.bob = List.flatMap (fun (p : ℕ × ℕ) => List.map (fun (e : ℕ) => (Intro.fldAt t ht N (oI + (p.1 * n + e) * t) - Intro.fldAt t ht N (oO + (p.2 * n + e) * t), 0)) (List.range n)) [(0, 1), (1, (rSlots L).length + 1)]

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.ConsIn : Type

The input of the consistency checks: t, the number n of coefficients, Na, N, the oracle's readable count R, and the two roles.

Equations

• MIPRE.Tailored.AnsRed.Typed.ConsIn = (MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Role × MIPRE.Role)

noncomputable def MIPRE.Tailored.AnsRed.Typed.kT : Cost.PolyTimeFun ConsIn Cost.Unary

Equations

• MIPRE.Tailored.AnsRed.Typed.kT = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Tailored.AnsRed.Typed.kN : Cost.PolyTimeFun ConsIn Cost.Unary

Equations

• MIPRE.Tailored.AnsRed.Typed.kN = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Tailored.AnsRed.Typed.kNa : Cost.PolyTimeFun ConsIn Cost.Unary

Equations

• MIPRE.Tailored.AnsRed.Typed.kNa = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.Tailored.AnsRed.Typed.kNN : Cost.PolyTimeFun ConsIn Cost.Unary

Equations

• MIPRE.Tailored.AnsRed.Typed.kNN = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Tailored.AnsRed.Typed.kR : Cost.PolyTimeFun ConsIn Cost.Unary

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.kRoles : Cost.PolyTimeFun ConsIn (Role × Role)

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.cwsF (i₀ : ℕ) : Cost.PolyTimeFun ConsIn (List (Cost.Unary × Cost.Unary))

The copied codewords (0, i₀), (1, R + i₀).

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.copyB (oI oO : Cost.PolyTimeFun ConsIn Cost.Unary) (i₀ : ℕ) : Cost.PolyTimeFun ConsIn (List Cost.BitStr)

The copy equations at offsets oI, oO.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.consBranch : Role × Role → Cost.PolyTimeFun ConsIn (List Cost.BitStr)

The branch at a pair of roles.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Tailored.AnsRed.Typed.consBranch x✝ = MIPRE.Cost.PolyTimeFun.const []

noncomputable def MIPRE.Tailored.AnsRed.Typed.consConsF : Cost.PolyTimeFun ConsIn (List Cost.BitStr)

The consistency checks, as a program, by the pair of roles.

Equations

• MIPRE.Tailored.AnsRed.Typed.consConsF = MIPRE.Tailored.AnsRed.Typed.kRoles.choose MIPRE.Tailored.AnsRed.Typed.consBranch (MIPRE.Cost.PolyTimeFun.const [])

theorem MIPRE.Tailored.AnsRed.Typed.consConsF_eq {t : ℕ} {ht : 1 ≤ t} (j d : ℕ) (L : PcpDims) (Na N : ℕ) (S : LIDT.CL.Ty) (r₁ r₂ : Role) : consConsF.toFun (Cost.unary t, Cost.unary (ncoef j d S), Cost.unary Na, Cost.unary N, Cost.unary (rSlots L).length, r₁, r₂) = consCons t ht j d L Na N S r₁ r₂

The consistency program computes the consistency checks.

The indifference checks

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.IndIn : Type

The input of the indifference equations: t, d, the offset o of the answer, N, the direction i, and the blocks of the answer's codewords, as intervals (lo, len) of wires.

Equations

• MIPRE.Tailored.AnsRed.Typed.IndIn = (MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × ℕ × List (MIPRE.Cost.Unary × MIPRE.Cost.Unary))

noncomputable def MIPRE.Tailored.AnsRed.Typed.indF : Cost.PolyTimeFun IndIn (List Cost.BitStr)

The indifference equations, as a program: for each codeword whose block misses the direction, the windows of its coefficients 1, …, d.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.indF_eq {t : ℕ} {ht : 1 ≤ t} (d o N i : ℕ) (ivs : List (ℕ × ℕ)) : indF.toFun (Cost.unary t, Cost.unary d, Cost.unary o, Cost.unary N, i, List.map (fun (p : ℕ × ℕ) => (Cost.unary p.1, Cost.unary p.2)) ivs) = eqsCons t ht (List.flatMap (fun (p : ℕ × ℕ × ℕ) => if p.2.1 ≤ i ∧ i < p.2.1 + p.2.2 then [] else List.map (fun (e : ℕ) => (Intro.fldAt t ht N (o + (p.1 * (d + 1) + (e + 1)) * t), 0)) (List.range d)) ((List.range ivs.length).zip ivs))

The indifference program computes the indifference equations of codewords with the given blocks.

The blocks of the codewords

theorem MIPRE.Tailored.AnsRed.Typed.mem_blockM_iff {j : ℕ} {L : PcpDims} (hLM : L.m ≤ 2 ^ j) (s : Slot L) (i : Fin (2 ^ j)) : i ∈ blockM j hLM s ↔ s.lo ≤ ↑i ∧ ↑i < s.lo + s.size

A direction lies in a slot's block exactly when it lies in its interval of wires.

theorem MIPRE.Tailored.AnsRed.Typed.flatMap_finRange_get {α : Type u_1} {β : Type u_2} (l : List α) (f : ℕ → α → List β) : List.flatMap (fun (c : Fin l.length) => f (↑c) (l.get c)) (List.finRange l.length) = List.flatMap (fun (p : ℕ × α) => f p.1 p.2) ((List.range l.length).zip l)

def MIPRE.Tailored.AnsRed.Typed.ivsOf (L : PcpDims) (r : Role) : List (ℕ × ℕ)

The blocks of a role's codewords, as intervals of wires.

Equations

• MIPRE.Tailored.AnsRed.Typed.ivsOf L r = List.map (fun (s : MIPRE.Tailored.AnsRed.Slot L) => (s.lo, s.size)) (MIPRE.Tailored.AnsRed.slotsOf L r)

theorem MIPRE.Tailored.AnsRed.Typed.length_ivsOf {L : PcpDims} (r : Role) : (ivsOf L r).length = (slotsOf L r).length

theorem MIPRE.Tailored.AnsRed.Typed.indEqs_eq {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {L : PcpDims} (d : ℕ) (hLM : L.m ≤ 2 ^ j) (N o : ℕ) (r : Role) (i : Fin (2 ^ j)) : indEqs d L hLM N o r i = List.flatMap (fun (p : ℕ × ℕ × ℕ) => if p.2.1 ≤ ↑i ∧ ↑i < p.2.1 + p.2.2 then [] else List.map (fun (e : ℕ) => (Intro.fldAt t ht N (o + (p.1 * (d + 1) + (e + 1)) * t), 0)) (List.range d)) ((List.range (ivsOf L r).length).zip (ivsOf L r))

The indifference equations are those of the codewords' blocks.

theorem MIPRE.Tailored.AnsRed.Typed.ivsOf_alice {L : PcpDims} : ivsOf L Role.alice = [(1, L.ℓ), (L.ℓ + L.ℓ + 3, L.ℓ)]

theorem MIPRE.Tailored.AnsRed.Typed.ivsOf_bob {L : PcpDims} : ivsOf L Role.bob = [(L.ℓ + 2, L.ℓ), (L.ℓ + L.ℓ + 3 + L.ℓ, L.ℓ)]

def MIPRE.Tailored.AnsRed.Typed.oracleRuns (L : PcpDims) : List (ℕ × ℕ × ℕ)

The oracle's blocks, in runs: (count, lo, len), in the order of its codewords.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ivsOf_oracle {L : PcpDims} : ivsOf L Role.oracle = List.flatMap (fun (r : ℕ × ℕ × ℕ) => List.replicate r.1 (r.2.1, r.2.2)) (oracleRuns L)

The oracle's blocks are its runs, expanded.

The tables, as programs

def MIPRE.Tailored.AnsRed.Typed.listF {α β : Type} [Cost.SizedEncoding α] [Cost.SizedEncoding β] : List (Cost.PolyTimeFun α β) → Cost.PolyTimeFun α (List β)

A list of programs, as a program of lists.

Equations

• MIPRE.Tailored.AnsRed.Typed.listF [] = MIPRE.Cost.PolyTimeFun.const []
• MIPRE.Tailored.AnsRed.Typed.listF (f :: fs) = f.cons (MIPRE.Tailored.AnsRed.Typed.listF fs)

@[simp]

theorem MIPRE.Tailored.AnsRed.Typed.listF_apply {α β : Type} [Cost.SizedEncoding α] [Cost.SizedEncoding β] (fs : List (Cost.PolyTimeFun α β)) (a : α) : (listF fs).toFun a = List.map (fun (f : Cost.PolyTimeFun α β) => f.toFun a) fs

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.uC (c : ℕ) : Cost.PolyTimeFun ArParams Cost.Unary

A constant in unary.

Equations

• MIPRE.Tailored.AnsRed.Typed.uC c = MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary c)

noncomputable def MIPRE.Tailored.AnsRed.Typed.oWF : Cost.PolyTimeFun ArParams Cost.Unary

◇' = 2ℓ + 3◇ + 6, the width of an index of O.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.mF : Cost.PolyTimeFun ArParams Cost.Unary

m, the number of wires.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.vOF : Cost.PolyTimeFun ArParams Cost.Unary

The first wire of an index of O, 2ℓ + 3.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.vWF (k : ℕ) : Cost.PolyTimeFun ArParams Cost.Unary

The first wire of the k-th witness index.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.oLF (k : ℕ) : Cost.PolyTimeFun ArParams Cost.Unary

The first wire of the k-th copy's cell.

Equations

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

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.trF (c lo len : Cost.PolyTimeFun ArParams Cost.Unary) : Cost.PolyTimeFun ArParams (Cost.Unary × Cost.Unary × Cost.Unary)

A run (count, lo, len).

Equations

• MIPRE.Tailored.AnsRed.Typed.trF c lo len = c.pair (lo.pair len)

noncomputable def MIPRE.Tailored.AnsRed.Typed.runsF : Cost.PolyTimeFun ArParams (List (Cost.Unary × Cost.Unary × Cost.Unary))

The oracle's runs of blocks, as a program of the parameters.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.runsF_arParams (t j d : ℕ) (L : PcpDims) (e : Cost.Data) : runsF.toFun (arParams t j d L e) = List.map (fun (r : ℕ × ℕ × ℕ) => (Cost.unary r.1, Cost.unary r.2.1, Cost.unary r.2.2)) (oracleRuns L)

noncomputable def MIPRE.Tailored.AnsRed.Typed.ivBranch : Role → Cost.PolyTimeFun (ArParams × Role) (List (Cost.Unary × Cost.Unary))

The blocks of a role's codewords, at a role.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.ivF : Cost.PolyTimeFun (ArParams × Role) (List (Cost.Unary × Cost.Unary))

The blocks of a role's codewords, as a program.

Equations

• MIPRE.Tailored.AnsRed.Typed.ivF = MIPRE.Cost.PolyTimeFun.snd.choose MIPRE.Tailored.AnsRed.Typed.ivBranch (MIPRE.Cost.PolyTimeFun.const [])

theorem MIPRE.Tailored.AnsRed.Typed.ivF_eq (t j d : ℕ) (L : PcpDims) (e : Cost.Data) (r : Role) : ivF.toFun (arParams t j d L e, r) = List.map (fun (p : ℕ × ℕ) => (Cost.unary p.1, Cost.unary p.2)) (ivsOf L r)

The indifference checks at a question

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.IndCIn : Type

The input of the indifference checks of one answer: the parameters, the answer's offset o, N, its type, and its question's low-degree bits.

Equations

• MIPRE.Tailored.AnsRed.Typed.IndCIn = (MIPRE.Tailored.AnsRed.Typed.ArParams × MIPRE.Cost.Unary × MIPRE.Cost.Unary × (MIPRE.Role × MIPRE.LIDT.CL.Ty) × MIPRE.Cost.BitStr)

noncomputable def MIPRE.Tailored.AnsRed.Typed.iP : Cost.PolyTimeFun IndCIn ArParams

Equations

• MIPRE.Tailored.AnsRed.Typed.iP = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Tailored.AnsRed.Typed.iO : Cost.PolyTimeFun IndCIn Cost.Unary

Equations

• MIPRE.Tailored.AnsRed.Typed.iO = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Tailored.AnsRed.Typed.iN : Cost.PolyTimeFun IndCIn Cost.Unary

Equations

• MIPRE.Tailored.AnsRed.Typed.iN = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.Tailored.AnsRed.Typed.iTy : Cost.PolyTimeFun IndCIn (Role × LIDT.CL.Ty)

Equations

• MIPRE.Tailored.AnsRed.Typed.iTy = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Tailored.AnsRed.Typed.iB : Cost.PolyTimeFun IndCIn Cost.BitStr

Equations

• MIPRE.Tailored.AnsRed.Typed.iB = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Tailored.AnsRed.Typed.iChi : Cost.PolyTimeFun IndCIn ℕ

The direction the question's seed selects.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.indAline : Cost.PolyTimeFun IndCIn (List Cost.BitStr)

The indifference equations of an axis-parallel line answer.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.indBranch : LIDT.CL.Ty → Cost.PolyTimeFun IndCIn (List Cost.BitStr)

The branch at a type of the low-degree test.

Equations

• MIPRE.Tailored.AnsRed.Typed.indBranch MIPRE.LIDT.CL.Ty.aline = MIPRE.Tailored.AnsRed.Typed.indAline
• MIPRE.Tailored.AnsRed.Typed.indBranch x✝ = MIPRE.Cost.PolyTimeFun.const []

noncomputable def MIPRE.Tailored.AnsRed.Typed.indConsF : Cost.PolyTimeFun IndCIn (List Cost.BitStr)

The indifference checks of an answer, as a program, by its type.

Equations

• MIPRE.Tailored.AnsRed.Typed.indConsF = (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Tailored.AnsRed.Typed.iTy).choose MIPRE.Tailored.AnsRed.Typed.indBranch (MIPRE.Cost.PolyTimeFun.const [])

theorem MIPRE.Tailored.AnsRed.Typed.indConsF_eq {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (hsel : ∀ (a : Fq t ht), ↑(sel.χ a) = Introspection.SeedProgram.selectorProg.toFun (Cost.unary t, Cost.unary j, (SAT.shoupBinField t ht).toBits a)) {rV : ℕ} {L : PcpDims} (hLM : L.m ≤ 2 ^ j) (d o N : ℕ) (e : Cost.Data) (r : Role) (S : LIDT.CL.Ty) (y : Fin (rV + D j * t) → CL.𝔽₂) : indConsF.toFun (arParams t j d L e, Cost.unary o, Cost.unary N, (r, S), List.drop rV (CL.toBits y)) = indCons j d L hM hLM N o r (ldQ t ht j rV sel S y)

The indifference program computes the indifference checks of an answer.