The padding of the repeated linear-constraints processor, in polynomial time

The processor of the repeated tailored verifier (issue #280) pads each coordinate's constraints to all the variables (TailoredGame.padCons). The padding of a constraint is determined by twelve lengths — before, at and after the coordinate, for the readable and the linear variables of each question — which the program holds in unary:

• padWithL p c, the padding of c by the twelve lengths p, and padWithF;
• triples L, for every position i of a list of lengths, the sum of the lengths before it, its own and the sum of those after it, and triplesF;
• padData, the twelve lengths of every coordinate from the four lists of lengths.

The padding

def MIPRE.Tailored.RepProg.padWithL (p : List Cost.Unary) (c : Cost.BitStr) : Cost.BitStr

The padding of c by twelve lengths p: readable before/at/after for the first question, linear before/at/after, then the same for the second question.

Equations

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

noncomputable def MIPRE.Tailored.RepProg.appF {ι : Type} [Cost.SizedEncoding ι] {α : Type} [Cost.SizedEncoding α] (F G : Cost.PolyTimeFun ι (List α)) : Cost.PolyTimeFun ι (List α)

Concatenation of two computed lists.

Equations

• MIPRE.Tailored.RepProg.appF F G = MIPRE.Cost.PolyTimeFun.append.comp (F.pair G)

@[simp]

theorem MIPRE.Tailored.RepProg.appF_apply {ι : Type} [Cost.SizedEncoding ι] {α : Type} [Cost.SizedEncoding α] (F G : Cost.PolyTimeFun ι (List α)) (a : ι) : (appF F G).toFun a = F.toFun a ++ G.toFun a

noncomputable def MIPRE.Tailored.RepProg.lenAt (j : ℕ) : Cost.PolyTimeFun (Cost.BitStr × List Cost.Unary) Cost.Unary

The j-th length.

Equations

• MIPRE.Tailored.RepProg.lenAt j = (MIPRE.Cost.PolyTimeFun.nthD [] j).comp MIPRE.Cost.PolyTimeFun.snd

@[simp]

theorem MIPRE.Tailored.RepProg.lenAt_apply (j : ℕ) (q : Cost.BitStr × List Cost.Unary) : (lenAt j).toFun q = q.2.getD j []

noncomputable def MIPRE.Tailored.RepProg.zerosAt (j : ℕ) : Cost.PolyTimeFun (Cost.BitStr × List Cost.Unary) Cost.BitStr

j zeros, the j-th length.

Equations

• MIPRE.Tailored.RepProg.zerosAt j = MIPRE.Cost.PolyTimeFun.replicate.comp ((MIPRE.Tailored.RepProg.lenAt j).pair (MIPRE.Cost.PolyTimeFun.const false))

@[simp]

theorem MIPRE.Tailored.RepProg.zerosAt_apply (j : ℕ) (q : Cost.BitStr × List Cost.Unary) : (zerosAt j).toFun q = List.replicate (List.length (q.2.getD j [])) false

noncomputable def MIPRE.Tailored.RepProg.sliceF (u v : Cost.PolyTimeFun (Cost.BitStr × List Cost.Unary) Cost.Unary) : Cost.PolyTimeFun (Cost.BitStr × List Cost.Unary) Cost.BitStr

The constraint without its first u coefficients, kept to its next v.

Equations

• MIPRE.Tailored.RepProg.sliceF u v = MIPRE.Cost.PolyTimeFun.take.comp ((MIPRE.Cost.PolyTimeFun.drop.comp (MIPRE.Cost.PolyTimeFun.fst.pair u)).pair v)

@[simp]

theorem MIPRE.Tailored.RepProg.sliceF_apply (u v : Cost.PolyTimeFun (Cost.BitStr × List Cost.Unary) Cost.Unary) (q : Cost.BitStr × List Cost.Unary) : (sliceF u v).toFun q = List.take (List.length (v.toFun q)) (List.drop (List.length (u.toFun q)) q.1)

noncomputable def MIPRE.Tailored.RepProg.padWithF : Cost.PolyTimeFun (Cost.BitStr × List Cost.Unary) Cost.BitStr

The padding, in polynomial time, on (c, p).

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.padWithF_apply (c : Cost.BitStr) (p : List Cost.Unary) : padWithF.toFun (c, p) = padWithL p c

Before, at and after

noncomputable def MIPRE.Tailored.RepProg.scanStepF : Cost.PolyTimeFun (Cost.Unary × List Cost.Unary) (Cost.Unary × List Cost.Unary)

The step of the scan: move the head of the remaining lengths onto the accumulated sum.

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.scanStepF_apply (q : Cost.Unary × List Cost.Unary) : scanStepF.toFun q = (q.1 ++ q.2.headD [], q.2.tail)

theorem MIPRE.Tailored.RepProg.iterate_scanStepF (L : List Cost.Unary) (acc : Cost.Unary) (i : ℕ) : scanStepF.toFun^[i] (acc, L) = (acc ++ (List.take i L).flatten, List.drop i L)

theorem MIPRE.Tailored.RepProg.esize_flatten_unary_le (L : List Cost.Unary) : Cost.esize L.flatten ≤ Cost.esize L

theorem MIPRE.Tailored.RepProg.esize_scan_le (L : List Cost.Unary) (acc : Cost.Unary) (i : ℕ) : Cost.esize (acc ++ (List.take i L).flatten, List.drop i L) ≤ 2 * Cost.esize (acc, L)

def MIPRE.Tailored.RepProg.tripleOut (q : Cost.Unary × List Cost.Unary) : List Cost.Unary

The sum before, the length at and the sum after the position of a scan state.

Equations

• MIPRE.Tailored.RepProg.tripleOut q = [q.1, q.2.headD [], q.2.tail.flatten]

noncomputable def MIPRE.Tailored.RepProg.tripleOutF : Cost.PolyTimeFun (Cost.Unary × List Cost.Unary) (List Cost.Unary)

Equations

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

def MIPRE.Tailored.RepProg.triples (L : List Cost.Unary) : List (List Cost.Unary)

Before, at and after every position of a list of lengths.

Equations

• MIPRE.Tailored.RepProg.triples L = List.ofFn fun (i : Fin L.length) => [(List.take (↑i) L).flatten, L.getD ↑i [], (List.drop (↑i + 1) L).flatten]

noncomputable def MIPRE.Tailored.RepProg.triplesF : Cost.PolyTimeFun (List Cost.Unary) (List (List Cost.Unary))

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.triplesF_apply (L : List Cost.Unary) : triplesF.toFun L = triples L

def MIPRE.Tailored.RepProg.padData (LRx LLx LRy LLy : List Cost.Unary) : List (List Cost.Unary)

The twelve lengths of every coordinate, from the readable and linear lengths of the two questions' coordinates.

Equations

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