The low-degree checks, as programs #

Slice P4h of planning/aldous-lyons-track.md: the constraints of the low-degree checks of the answer-reduced game (Typed.ldCons) computed by a program from the parameters, the two questions' low-degree bits and the layout of the answers.

ldEqF: the equations that two answers agree codeword by codeword (ldEq), each the difference of two windows (ldEqF_eq).
ldLineF: the equations that the line polynomials, evaluated at a parameter, are the point values (ldLine), by Horner's rule (ldLineF_eq).
ldConsF: the low-degree checks at two questions of one role, by the pair of types (ldConsF_eq). A question's low-degree vector is read from the last bits of its vector part in runs of blocks (blocks1_ldPart): the point, the direction, the seed. The selected direction of an axis-parallel line is the seed's block (selectorProg), the point-on-line guard is memberProg, the line parameter parameterProg, the introspection stage's programs.

Field elements of the answer bits #

source

theorem MIPRE.Tailored.AnsRed.Typed.window_eq_fldAt {t : ℕ} {ht : 1 ≤ t} {N : ℕ} (z : Cost.BitStr) (hz : List.length z ≤ N) (o : ℕ) :

window z o t = (SAT.shoupBinField t ht).toBits ((Intro.fldAt t ht N o) (Intro.bitVec N z))

source

theorem MIPRE.Tailored.AnsRed.Typed.zeros_eq (t : ℕ) (ht : 1 ≤ t) :

List.replicate t false = (SAT.shoupBinField t ht).toBits 0

source

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.mulU :

Cost.PolyTimeFun (Cost.Unary × Cost.Unary) Cost.Unary

(u, v) ↦ u v in unary.

Equations

MIPRE.Tailored.AnsRed.Typed.mulU = MIPRE.LowDegree.DegreeArithmetic.mulUnaryProg

Instances For

source

@[simp]

theorem MIPRE.Tailored.AnsRed.Typed.mulU_apply (a b : ℕ) :

mulU.toFun (Cost.unary a, Cost.unary b) = Cost.unary (a * b)

source

@[simp]

theorem MIPRE.Tailored.AnsRed.Typed.append_unary (a b : ℕ) :

Cost.PolyTimeFun.append.toFun (Cost.unary a, Cost.unary b) = Cost.unary (a + b)

source

theorem MIPRE.Tailored.AnsRed.Typed.unary_append_unary (a b : ℕ) :

Cost.unary a ++ Cost.unary b = Cost.unary (a + b)

Equal codewords #

source

noncomputable def MIPRE.Tailored.AnsRed.Typed.pairsF :

Cost.PolyTimeFun (Cost.Unary × Cost.Unary) (List (Cost.Unary × Cost.Unary))

The pairs (c, e) with c < k and e < n, in unary, c major.

Equations

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

Instances For

source

theorem MIPRE.Tailored.AnsRed.Typed.pairsF_apply (k n : ℕ) :

pairsF.toFun (Cost.unary k, Cost.unary n) = List.flatMap (fun (c : ℕ) => List.map (fun (e : ℕ) => (Cost.unary c, Cost.unary e)) (List.range n)) (List.range k)

source

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.EqIn :

Type

The input of the equality equations: t, k, the number n of coefficients, Na, N.

Equations

MIPRE.Tailored.AnsRed.Typed.EqIn = (MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary)

Instances For

source

noncomputable def MIPRE.Tailored.AnsRed.Typed.ldEqF :

Cost.PolyTimeFun EqIn (List Cost.BitStr)

The equality equations ldEq, as a program: at (c, e), the window of the first answer at (c n + e) t plus that of the second at Na + (c n + e) t.

Equations

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

Instances For

source

theorem MIPRE.Tailored.AnsRed.Typed.mem_pairs {k n : ℕ} {p : Cost.Unary × Cost.Unary} (h : p ∈ List.flatMap (fun (c : ℕ) => List.map (fun (e : ℕ) => (Cost.unary c, Cost.unary e)) (List.range n)) (List.range k)) :

∃ (c : ℕ) (e : ℕ), p = (Cost.unary c, Cost.unary e)

source

theorem MIPRE.Tailored.AnsRed.Typed.ldEqF_eq {t : ℕ} {ht : 1 ≤ t} (k n Na N : ℕ) :

ldEqF.toFun (Cost.unary t, Cost.unary k, Cost.unary n, Cost.unary Na, Cost.unary N) = eqsCons t ht (ldEq N Na k n)

The equality program computes ldEq.

Line polynomials against point values #

source

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.LineIn :

Type

The input of the line equations: t, k, the number n of coefficients, the offsets oL of the line answer and oP of the point answer, N, and the parameter's bits.

Equations

MIPRE.Tailored.AnsRed.Typed.LineIn = (MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.BitStr)

Instances For

source

noncomputable def MIPRE.Tailored.AnsRed.Typed.ldLineF :

Cost.PolyTimeFun LineIn (List Cost.BitStr)

The line equations ldLine, as a program: at c, Horner's evaluation at the parameter of the n windows of the c-th line polynomial, plus the window of the c-th point value.

Equations

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

Instances For

source

theorem MIPRE.Tailored.AnsRed.Typed.ldLineF_eq {t : ℕ} {ht : 1 ≤ t} (k n oL oP N : ℕ) (α : Fq t ht) :

ldLineF.toFun (Cost.unary t, Cost.unary k, Cost.unary n, Cost.unary oL, Cost.unary oP, Cost.unary N, (SAT.shoupBinField t ht).toBits α) = eqsCons t ht (ldLine N k n oL oP α)

The line program computes ldLine.

The low-degree vector of a question #

source

theorem MIPRE.Tailored.AnsRed.Typed.ldBitsV_ldPart {t : ℕ} {ht : 1 ≤ t} {j rV : ℕ} (y : Fin (rV + D j * t) → CL.𝔽₂) :

ldBitsV j t ht (ldPart t ht j rV y) = List.drop rV (CL.toBits y)

The low-degree bits of a typed question's vector are its last D j * t bits.

source

theorem MIPRE.Tailored.AnsRed.Typed.blocks1_ldPart {t : ℕ} {ht : 1 ≤ t} {j rV : ℕ} (y : Fin (rV + D j * t) → CL.𝔽₂) :

blocks1 (Cost.unary t) (Cost.unary (2 ^ j)) (List.drop rV (CL.toBits y)) = ((SAT.shoupBinField t ht).vecBits ((regs j).ptOf (ldPart t ht j rV y)), (SAT.shoupBinField t ht).vecBits ((regs j).dirOf (ldPart t ht j rV y)), [(SAT.shoupBinField t ht).toBits (ldPart t ht j rV y (regs j).coord)])

The runs of the low-degree bits of a typed question: the point, the direction, the seed.

source

noncomputable def MIPRE.Tailored.AnsRed.Typed.blkF :

Cost.PolyTimeFun (Cost.Unary × Cost.Unary × Cost.BitStr) AnswerReduction.StageProg.Blocks

The runs of M + M + 1 blocks of t bits, on (t, M, z).

Equations

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

Instances For

source

theorem MIPRE.Tailored.AnsRed.Typed.blkF_apply (k m : Cost.Unary) (z : Cost.BitStr) :

blkF.toFun (k, m, z) = blocks1 k m z

source

noncomputable def MIPRE.Tailored.AnsRed.Typed.dirAF :

Cost.PolyTimeFun (Cost.Unary × Cost.Unary × ℕ) (List Cost.BitStr)

The direction e_i of an axis-parallel line, on (t, M, i): M field elements, one at i, zero elsewhere.

Equations

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

Instances For

source

theorem MIPRE.Tailored.AnsRed.Typed.dirAF_apply {t : ℕ} {ht : 1 ≤ t} {M : ℕ} (i : Fin M) :

dirAF.toFun (Cost.unary t, Cost.unary M, ↑i) = (SAT.shoupBinField t ht).vecBits (Pi.single i 1)

The checks at two questions of one role #

source

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.LdCIn :

Type

The input of the low-degree checks: t, j, M, d; the number k of codewords, the length Na of the first answer, N; the two questions' types and low-degree bits.

Equations