The output indicator, as a program

The triangulated output indicator L* (Definition defn:decider-read, II:8381) of MIPRE.Tailored.AnsRed.Indicator, written as a program of the ambient model: the four runs of the answer-length calculator and the run of the processor of the canonical decider (MIPRE.Tailored.canonProg, whose input builders it reuses), followed by a polynomial-time check that decides LstarOK at the parameters prm n of the index.

• The check's pieces: unary ranges (rangeU), the positions of the ones of a window (onesU), the purified equation with its variables in unary (pureEqnU), the triangulation in unary (triangleU), and the table loop by loop (tableU), each with the program computing it and its reading (toEqn_pureEqnU, map_toTri_triangleU, tableU_eq).
• lstarCore: the check, parameter-free, reading (ℓ, ◇) in unary beside its input (lstarCore_apply); lstarRaw prm runs it on the parameters prm n of the index, the one place where the parameter program enters.
• lstarFinal prm: the check, deciding LstarOK (2^ℓ) (2^◇) with (ℓ, ◇) = prm n in unary (lstarFinal_apply, through lstarCheck_eq): the powers of two are capped by the input, so the check is polynomial-time.
• lstarProg prm L LP: the output indicator of a tailored verifier with answer-length calculator L and processor LP; lstarProg_accepts: it accepts exactly when the five runs halt and LstarOK holds of their outputs.

Helpers

noncomputable def MIPRE.Tailored.AnsRed.mapR {ι : Type u_1} {α : Type u_2} {γ : Type u_3} [Cost.SizedEncoding ι] [Cost.SizedEncoding α] [Cost.SizedEncoding γ] (F : Cost.PolyTimeFun (α × ι) γ) (l : Cost.PolyTimeFun ι (List α)) : Cost.PolyTimeFun ι (List γ)

Map over a list computed from the input, the input as the context.

Equations

• MIPRE.Tailored.AnsRed.mapR F l = F.mapWith.comp (l.pair (MIPRE.Cost.PolyTimeFun.id ι))

@[simp]

theorem MIPRE.Tailored.AnsRed.mapR_apply {ι : Type u_1} {α : Type u_2} {γ : Type u_3} [Cost.SizedEncoding ι] [Cost.SizedEncoding α] [Cost.SizedEncoding γ] (F : Cost.PolyTimeFun (α × ι) γ) (l : Cost.PolyTimeFun ι (List α)) (i : ι) : (mapR F l).toFun i = List.map (fun (a : α) => F.toFun (a, i)) (l.toFun i)

noncomputable def MIPRE.Tailored.AnsRed.flatMapR {ι : Type u_1} {α : Type u_2} {γ : Type u_3} [Cost.SizedEncoding ι] [Cost.SizedEncoding α] [Cost.SizedEncoding γ] (F : Cost.PolyTimeFun (α × ι) (List γ)) (l : Cost.PolyTimeFun ι (List α)) : Cost.PolyTimeFun ι (List γ)

flatMap over a list computed from the input, the input as the context.

Equations

• MIPRE.Tailored.AnsRed.flatMapR F l = MIPRE.Tailored.RepProg.flattenF.comp (MIPRE.Tailored.AnsRed.mapR F l)

@[simp]

theorem MIPRE.Tailored.AnsRed.flatMapR_apply {ι : Type u_1} {α : Type u_2} {γ : Type u_3} [Cost.SizedEncoding ι] [Cost.SizedEncoding α] [Cost.SizedEncoding γ] (F : Cost.PolyTimeFun (α × ι) (List γ)) (l : Cost.PolyTimeFun ι (List α)) (i : ι) : (flatMapR F l).toFun i = List.flatMap (fun (a : α) => F.toFun (a, i)) (l.toFun i)

noncomputable def MIPRE.Tailored.AnsRed.andF : Cost.PolyTimeFun (Bool × Bool) Bool

&&.

Equations

• MIPRE.Tailored.AnsRed.andF = MIPRE.SAT.andProg

@[simp]

theorem MIPRE.Tailored.AnsRed.andF_apply (p : Bool × Bool) : andF.toFun p = (p.1 && p.2)

noncomputable def MIPRE.Tailored.AnsRed.orF : Cost.PolyTimeFun (Bool × Bool) Bool

||.

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.orF_apply (p : Bool × Bool) : orF.toFun p = (p.1 || p.2)

noncomputable def MIPRE.Tailored.AnsRed.xorF : Cost.PolyTimeFun (Bool × Bool) Bool

Exclusive or.

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.xorF_apply (p : Bool × Bool) : xorF.toFun p = (p.1 ^^ p.2)

noncomputable def MIPRE.Tailored.AnsRed.anyF : Cost.PolyTimeFun (List Bool) Bool

Some element of the list is true.

Equations

• MIPRE.Tailored.AnsRed.anyF = (MIPRE.SAT.notBoolP.comp (MIPRE.SAT.allBoolProg.comp MIPRE.SAT.notBoolP.map)).congr (fun (l : List Bool) => l.any id) MIPRE.Tailored.AnsRed.anyF._proof_1

@[simp]

theorem MIPRE.Tailored.AnsRed.anyF_apply (l : List Bool) : anyF.toFun l = l.any id

noncomputable def MIPRE.Tailored.AnsRed.getDU : Cost.PolyTimeFun (Cost.BitStr × Cost.Unary) Bool

The bit of a string at a unary position, false past the end.

Equations

• MIPRE.Tailored.AnsRed.getDU = (MIPRE.Cost.PolyTimeFun.headD false).comp MIPRE.Cost.PolyTimeFun.drop

theorem MIPRE.Tailored.AnsRed.headD_drop {α : Type u_1} (l : List α) (n : ℕ) (d : α) : (List.drop n l).headD d = l.getD n d

@[simp]

theorem MIPRE.Tailored.AnsRed.getDU_apply (p : Cost.BitStr × Cost.Unary) : getDU.toFun p = List.getD p.1 (List.length p.2) false

theorem MIPRE.Tailored.AnsRed.unary_eq_of_length {u : Cost.Unary} {k : ℕ} (h : List.length u = k) : u = Cost.unary k

A unary list is the unary numeral of its length.

noncomputable def MIPRE.Tailored.AnsRed.rangeU : Cost.PolyTimeFun Cost.Unary (List Cost.Unary)

The unary numerals below the length of u.

Equations

• MIPRE.Tailored.AnsRed.rangeU = MIPRE.Cost.PolyTimeFun.reverse.comp (MIPRE.Cost.PolyTimeFun.tail.comp MIPRE.LowDegree.DegreeArithmetic.descendingUnaryProg)

@[simp]

theorem MIPRE.Tailored.AnsRed.rangeU_apply (u : Cost.Unary) : rangeU.toFun u = List.map Cost.unary (List.range (List.length u))

The purified equation, in unary

def MIPRE.Tailored.AnsRed.onesU (c : Cost.BitStr) (o k : ℕ) : List Cost.Unary

The positions j < k, in unary, at which c has a one at o + j: onesFrom in unary.

Equations

• MIPRE.Tailored.AnsRed.onesU c o k = List.flatMap (fun (j : MIPRE.Cost.Unary) => if List.getD c (o + List.length j) false = true then [j] else []) (List.map MIPRE.Cost.unary (List.range k))

theorem MIPRE.Tailored.AnsRed.flatMap_filter_eq {β : Type u_1} (l : List ℕ) (p : ℕ → Bool) (f : ℕ → β) : List.flatMap (fun (j : ℕ) => if p j = true then [f j] else []) l = List.map f (List.filter p l)

theorem MIPRE.Tailored.AnsRed.map_length_onesU (c : Cost.BitStr) (o k : ℕ) : List.map List.length (onesU c o k) = onesFrom c o k

def MIPRE.Tailored.AnsRed.pureEqnU (lRx lLx lRy lLy N : ℕ) (aR bR c : Cost.BitStr) : List Cost.Unary × Bool

The purified equation (pureEqn) with its variables in unary and its right-hand side a bit: the positions of the ones of the two linear windows, those of y shifted by N, and the parity of the affine coordinate and the two readable inner products.

Equations

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

def MIPRE.Tailored.AnsRed.toEqn (e : List Cost.Unary × Bool) : Eqn

An equation with its variables in unary, read.

Equations

• MIPRE.Tailored.AnsRed.toEqn e = { vars := List.map List.length e.1, rhs := MIPRE.LowDegree.ofBool e.2 }

theorem MIPRE.Tailored.AnsRed.ofBool_dotBits_window {c v : Cost.BitStr} {o k : ℕ} (hk : o + k ≤ List.length c) : LowDegree.ofBool (LowDegree.BinaryLinear.dotBits (List.take k (List.drop o c)) v) = ∑ j ∈ Finset.range k, bitAt c (o + j) * bitAt v j

The inner product of a window of c with v, as a sum, when the window lies in c.

theorem MIPRE.Tailored.AnsRed.toEqn_pureEqnU (lRx lLx lRy lLy N : ℕ) (aR bR c : Cost.BitStr) : toEqn (pureEqnU lRx lLx lRy lLy N aR bR c) = pureEqn lRx lLx lRy lLy N aR bR c

def MIPRE.Tailored.AnsRed.rowsU (N lRx lLx lRy lLy : ℕ) (aR bR : Cost.BitStr) (cs : List Cost.BitStr) : List (List Cost.Unary × Bool)

The rows the indicator decouples, in unary.

Equations

• MIPRE.Tailored.AnsRed.rowsU N lRx lLx lRy lLy aR bR cs = List.map (MIPRE.Tailored.AnsRed.pureEqnU lRx lLx lRy lLy N aR bR) cs

theorem MIPRE.Tailored.AnsRed.map_toEqn_rowsU (N lRx lLx lRy lLy : ℕ) (aR bR : Cost.BitStr) (cs : List Cost.BitStr) : List.map toEqn (rowsU N lRx lLx lRy lLy aR bR cs) = lsRows N lRx lLx lRy lLy aR bR cs

The triangulation, in unary

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.TriU : Type

A triangulated equation with its variables in unary, and its coefficients as the signature word [0, 0, a₁, a₂, a₃, b] with which the table compares its signs.

Equations

• MIPRE.Tailored.AnsRed.TriU = ((MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary) × MIPRE.Cost.BitStr)

def MIPRE.Tailored.AnsRed.toTri (t : TriU) : Tri

A triangulated equation in unary, read.

Equations

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

def MIPRE.Tailored.AnsRed.TriU.WF (t : TriU) : Prop

The signature word is [0, 0, a₁, a₂, a₃, b].

Equations

• t.WF = (t.2 = [false, false, List.getD t.2 2 false, List.getD t.2 3 false, List.getD t.2 4 false, List.getD t.2 5 false])

def MIPRE.Tailored.AnsRed.yvU (N r i : Cost.Unary) : Cost.Unary

yv N r i = N + r N + i, in unary.

Equations

• MIPRE.Tailored.AnsRed.yvU N r i = N ++ (MIPRE.Cost.unary (List.length r * List.length N) ++ i)

@[simp]

theorem MIPRE.Tailored.AnsRed.length_yvU (N r i : Cost.Unary) : List.length (yvU N r i) = yv (List.length N) (List.length r) (List.length i)

def MIPRE.Tailored.AnsRed.triRowU (N r : Cost.Unary) (e : List Cost.Unary × Bool) : List TriU

The triangulation of one row in unary (triRow), the row's index r in unary.

Equations

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

def MIPRE.Tailored.AnsRed.triangleU (N : Cost.Unary) (rows : List (List Cost.Unary × Bool)) : List TriU

The triangulation in unary (triangle).

Equations

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

theorem MIPRE.Tailored.AnsRed.mapIdx_eq_zip_range {α : Type u_1} {β : Type u_2} (l : List α) (f : ℕ → α → β) : List.mapIdx f l = List.map (fun (p : α × ℕ) => f p.2 p.1) (l.zip (List.range l.length))

theorem MIPRE.Tailored.AnsRed.map_toTri_triRowU (N r : Cost.Unary) (e : List Cost.Unary × Bool) : List.map toTri (triRowU N r e) = triRow (List.length N) (List.length r) (toEqn e)

theorem MIPRE.Tailored.AnsRed.map_toTri_triangleU (N : Cost.Unary) (rows : List (List Cost.Unary × Bool)) : List.map toTri (triangleU N rows) = triangle (List.length N) (List.map toEqn rows)

theorem MIPRE.Tailored.AnsRed.triRowU_wf (N r : Cost.Unary) (e : List Cost.Unary × Bool) (t : TriU) : t ∈ triRowU N r e → t.WF

theorem MIPRE.Tailored.AnsRed.triangleU_wf (N : Cost.Unary) (rows : List (List Cost.Unary × Bool)) (t : TriU) : t ∈ triangleU N rows → t.WF

The table, in unary

def MIPRE.Tailored.AnsRed.signWord (s : ℕ) : Cost.BitStr

The six signs held by the last coordinate s, as a word [ε_A, ε_B, ε₁, ε₂, ε₃, ε₀].

Equations

• MIPRE.Tailored.AnsRed.signWord s = List.map s.testBit (List.range 6)

theorem MIPRE.Tailored.AnsRed.signWord_eq (s : ℕ) : signWord s = [s.testBit 0, s.testBit 1, s.testBit 2, s.testBit 3, s.testBit 4, s.testBit 5]

def MIPRE.Tailored.AnsRed.signWords : List Cost.BitStr

The 64 sign words, in the order of the last coordinate.

Equations

• MIPRE.Tailored.AnsRed.signWords = List.map MIPRE.Tailored.AnsRed.signWord (List.range 64)

def MIPRE.Tailored.AnsRed.triMatch (u₁ u₂ u₃ : Cost.Unary) (w : Cost.BitStr) (t : TriU) : Bool

A triangulated equation matches the signs w and the three copy coordinates.

Equations

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

def MIPRE.Tailored.AnsRed.decIndU (uA uB u₁ u₂ u₃ : Cost.Unary) (w : Cost.BitStr) (N : Cost.Unary) (tris : List TriU) : Bool

The indicator at given coordinates and signs, in unary: decInd inside the loops, whose ranges make its range conditions true.

Equations

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

def MIPRE.Tailored.AnsRed.tableU (N D : Cost.Unary) (tris : List TriU) : Cost.BitStr

The table, loop by loop, in unary.

Equations

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

theorem MIPRE.Tailored.AnsRed.sgn_eq_ofBool {s i : ℕ} {b : Bool} : sgn s i = LowDegree.ofBool b ↔ s.testBit i = b

theorem MIPRE.Tailored.AnsRed.sgn_eq_one {s i : ℕ} : sgn s i = 1 ↔ s.testBit i = true

theorem MIPRE.Tailored.AnsRed.sgn_eq_zero {s i : ℕ} : sgn s i = 0 ↔ s.testBit i = false

theorem MIPRE.Tailored.AnsRed.ofBool_ne_zero {b : Bool} : LowDegree.ofBool b ≠ 0 ↔ b = true

theorem MIPRE.Tailored.AnsRed.decIndU_eq {N D uA uB u₁ u₂ u₃ s : ℕ} {tris : List TriU} (hwf : ∀ t ∈ tris, t.WF) (hA : uA < N) (hB : uB < N) (h₁ : u₁ < D) (h₂ : u₂ < D) : decIndU (Cost.unary uA) (Cost.unary uB) (Cost.unary u₁) (Cost.unary u₂) (Cost.unary u₃) (signWord s) (Cost.unary N) tris = decide (decInd N N D (List.map toTri tris) uA uB u₁ u₂ u₃ (sgn s 0) (sgn s 1) (sgn s 2) (sgn s 3) (sgn s 4) (sgn s 5))

The indicator in unary is decInd inside the loops.

theorem MIPRE.Tailored.AnsRed.flatMap_congr_mem {α : Type u_1} {β : Type u_2} {l : List α} {f g : α → List β} (h : ∀ a ∈ l, f a = g a) : List.flatMap f l = List.flatMap g l

theorem MIPRE.Tailored.AnsRed.tableU_eq (N D : ℕ) {tris : List TriU} (hwf : ∀ t ∈ tris, t.WF) : tableU (Cost.unary N) (Cost.unary D) tris = indTable N D (List.map toTri tris)

The table in unary is the table, on well-formed equations.

The programs of the pieces

noncomputable def MIPRE.Tailored.AnsRed.onesUF : Cost.PolyTimeFun (Cost.BitStr × Cost.Unary × Cost.Unary) (List Cost.Unary)

onesU, as a program on (c, o, k).

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.onesUF_apply (p : Cost.BitStr × Cost.Unary × Cost.Unary) : onesUF.toFun p = onesU p.1 (List.length p.2.1) (List.length p.2.2)

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.PCtx : Type

The context of a purified equation: the four lengths, the table size, the readable answers.

Equations

• MIPRE.Tailored.AnsRed.PCtx = (MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

noncomputable def MIPRE.Tailored.AnsRed.pureEqnRaw : Cost.PolyTimeFun (Cost.BitStr × PCtx) (List Cost.Unary × Bool)

The program computing pureEqnU on a constraint and its context.

Equations

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

theorem MIPRE.Tailored.AnsRed.pureEqnRaw_apply (p : Cost.BitStr × PCtx) : pureEqnRaw.toFun p = pureEqnU (List.length p.2.1) (List.length p.2.2.1) (List.length p.2.2.2.1) (List.length p.2.2.2.2.1) (List.length p.2.2.2.2.2.1) p.2.2.2.2.2.2.1 p.2.2.2.2.2.2.2 p.1

noncomputable def MIPRE.Tailored.AnsRed.pureEqnUF : Cost.PolyTimeFun (Cost.BitStr × PCtx) (List Cost.Unary × Bool)

pureEqnU, as a program on a constraint and its context.

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.pureEqnUF_apply (c : Cost.BitStr) (lRx lLx lRy lLy N : Cost.Unary) (aR bR : Cost.BitStr) : pureEqnUF.toFun (c, lRx, lLx, lRy, lLy, N, aR, bR) = pureEqnU (List.length lRx) (List.length lLx) (List.length lRy) (List.length lLy) (List.length N) aR bR c

noncomputable def MIPRE.Tailored.AnsRed.rowsUF : Cost.PolyTimeFun (List Cost.BitStr × PCtx) (List (List Cost.Unary × Bool))

The rows, as a program on the constraints and the context.

Equations

• MIPRE.Tailored.AnsRed.rowsUF = MIPRE.Tailored.AnsRed.pureEqnUF.mapWith

@[simp]

theorem MIPRE.Tailored.AnsRed.rowsUF_apply (cs : List Cost.BitStr) (lRx lLx lRy lLy N : Cost.Unary) (aR bR : Cost.BitStr) : rowsUF.toFun (cs, lRx, lLx, lRy, lLy, N, aR, bR) = rowsU (List.length N) (List.length lRx) (List.length lLx) (List.length lRy) (List.length lLy) aR bR cs

noncomputable def MIPRE.Tailored.AnsRed.yvUF : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × Cost.Unary) Cost.Unary

yvU, as a program on (N, r, i).

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.yvUF_apply (N r i : Cost.Unary) : yvUF.toFun (N, r, i) = yvU N r i

noncomputable def MIPRE.Tailored.AnsRed.triRowRaw : Cost.PolyTimeFun ((List Cost.Unary × Bool) × Cost.Unary × Cost.Unary) (List TriU)

The program computing triRowU on (e, r, N).

Equations

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

theorem MIPRE.Tailored.AnsRed.triRowRaw_apply (p : (List Cost.Unary × Bool) × Cost.Unary × Cost.Unary) : triRowRaw.toFun p = triRowU p.2.2 p.2.1 p.1

noncomputable def MIPRE.Tailored.AnsRed.triRowUF : Cost.PolyTimeFun ((List Cost.Unary × Bool) × Cost.Unary × Cost.Unary) (List TriU)

triRowU, as a program on (e, r, N).

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.triRowUF_apply (e : List Cost.Unary × Bool) (r N : Cost.Unary) : triRowUF.toFun (e, r, N) = triRowU N r e

noncomputable def MIPRE.Tailored.AnsRed.triangleUF : Cost.PolyTimeFun (List (List Cost.Unary × Bool) × Cost.Unary) (List TriU)

triangleU, as a program on (rows, N).

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.triangleUF_apply (rows : List (List Cost.Unary × Bool)) (N : Cost.Unary) : triangleUF.toFun (rows, N) = triangleU N rows

noncomputable def MIPRE.Tailored.AnsRed.triMatchRaw : Cost.PolyTimeFun (TriU × Cost.Unary × Cost.Unary × Cost.Unary × Cost.BitStr) Bool

triMatch, as a program on (t, u₁, u₂, u₃, w).

Equations

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

theorem MIPRE.Tailored.AnsRed.triMatchRaw_apply (p : TriU × Cost.Unary × Cost.Unary × Cost.Unary × Cost.BitStr) : triMatchRaw.toFun p = triMatch p.2.1 p.2.2.1 p.2.2.2.1 p.2.2.2.2 p.1

noncomputable def MIPRE.Tailored.AnsRed.triMatchF : Cost.PolyTimeFun (TriU × Cost.Unary × Cost.Unary × Cost.Unary × Cost.BitStr) Bool

triMatch, as a program.

Equations

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

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.IIn : Type

The input of the indicator in the loops: the five coordinates, the signs, N, D and the triangulated equations.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.decIndRaw : Cost.PolyTimeFun IIn Bool

decIndU, as a program.

Equations

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

theorem MIPRE.Tailored.AnsRed.decIndRaw_apply (p : IIn) : decIndRaw.toFun p = decIndU p.1 p.2.1 p.2.2.1 p.2.2.2.1 p.2.2.2.2.1 p.2.2.2.2.2.1 p.2.2.2.2.2.2.1 p.2.2.2.2.2.2.2.2

noncomputable def MIPRE.Tailored.AnsRed.decIndF : Cost.PolyTimeFun IIn Bool

decIndU, as a program.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.tableRaw : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × List TriU) Cost.BitStr

The table program, loop by loop, on (N, D, tris).

Equations

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

theorem MIPRE.Tailored.AnsRed.tableRaw_apply (p : Cost.Unary × Cost.Unary × List TriU) : tableRaw.toFun p = tableU p.1 p.2.1 p.2.2

noncomputable def MIPRE.Tailored.AnsRed.tableF : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × List TriU) Cost.BitStr

tableU, as a program.

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.tableF_apply (N D : Cost.Unary) (tris : List TriU) : tableF.toFun (N, D, tris) = tableU N D tris

Powers of two, capped

noncomputable def MIPRE.Tailored.AnsRed.capStep : Cost.PolyTimeFun ((Cost.Unary × Cost.Unary) × Unit) (Cost.Unary × Cost.Unary)

The step of pow2CapF: double the accumulator, capped at the length of the cap.

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.capStep_apply (acc m : Cost.Unary) (x : Unit) : capStep.toFun ((acc, m), x) = (List.take (List.length m) (acc ++ acc), m)

theorem MIPRE.Tailored.AnsRed.foldl_capStep (l : Cost.Unary) {acc m : Cost.Unary} (h : List.length acc ≤ List.length m) : List.foldl (fun (s : Cost.Unary × Cost.Unary) (a : Unit) => capStep.toFun (s, a)) (acc, m) l = (Cost.unary (min (2 ^ List.length l * List.length acc) (List.length m)), m)

theorem MIPRE.Tailored.AnsRed.capStep_bounded : capStep.FoldBounded (2 * Polynomial.X + 1)

noncomputable def MIPRE.Tailored.AnsRed.pow2CapF : Cost.PolyTimeFun (Cost.Unary × Cost.Unary) Cost.Unary

min(2^k, m) in unary, on (k, m): never more than m, so polynomial in the input.

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.pow2CapF_apply (k m : Cost.Unary) : pow2CapF.toFun (k, m) = Cost.unary (min (2 ^ List.length k) (List.length m))

noncomputable def MIPRE.Tailored.AnsRed.tableSizeF : Cost.PolyTimeFun (Cost.Unary × Cost.Unary) Cost.Unary

The number of indices of the table, tableSize, in unary.

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.tableSizeF_apply (N D : Cost.Unary) : tableSizeF.toFun (N, D) = Cost.unary (tableSize (List.length N) (List.length D))

The check

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.FIn : Type

The input of the check: the output of the processor, the four lengths ((n, y, true) first) and the decider's input (n, x, y, a, b), as the canonical decider stacks them.

Equations

• MIPRE.Tailored.AnsRed.FIn = (MIPRE.Cost.Data × MIPRE.Cost.Data × MIPRE.Cost.Data × MIPRE.Cost.Data × MIPRE.Cost.Data × MIPRE.Tailored.DIn)

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.CIn : Type

The input of the parameter-free check: the input of the check and the parameters (ℓ, ◇) in unary.

Equations

• MIPRE.Tailored.AnsRed.CIn = (MIPRE.Tailored.AnsRed.FIn × MIPRE.Cost.Unary × MIPRE.Cost.Unary)

noncomputable def MIPRE.Tailored.AnsRed.lstarCore : Cost.PolyTimeFun CIn Bool

The check, parameter-free: on the input of the check and parameters (ℓ, ◇) in unary, it decides LstarOK (2^ℓ) (2^◇) (lstarCore_apply). The parameter program enters the check only through lstarRaw.

Equations

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

theorem MIPRE.Tailored.AnsRed.lstarCore_apply (r₀ r₁ r₂ r₃ r₄ : Cost.Data) (i : DIn) (ℓ dm : Cost.Unary) : lstarCore.toFun ((r₀, r₁, r₂, r₃, r₄, i), ℓ, dm) = lstarCheck (List.length ℓ) (List.length dm) r₄.spineList.length r₃.spineList.length r₂.spineList.length r₁.spineList.length r₀.bitsListD i.2.2.2.1 i.2.2.2.2

noncomputable def MIPRE.Tailored.AnsRed.lstarIdx : Cost.PolyTimeFun FIn ℕ

The index n of the input of the check.

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.lstarIdx_apply (z : FIn) : lstarIdx.toFun z = z.2.2.2.2.2.1

noncomputable def MIPRE.Tailored.AnsRed.lstarRaw (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) : Cost.PolyTimeFun FIn Bool

The program of the check, at the parameter program prm of the index: the parameter-free check lstarCore, on the input and the parameters prm n of its index.

Equations

• MIPRE.Tailored.AnsRed.lstarRaw prm = MIPRE.Tailored.AnsRed.lstarCore.comp ((MIPRE.Cost.PolyTimeFun.id MIPRE.Tailored.AnsRed.FIn).pair (prm.comp MIPRE.Tailored.AnsRed.lstarIdx))

theorem MIPRE.Tailored.AnsRed.lstarRaw_apply (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) (r₀ r₁ r₂ r₃ r₄ : Cost.Data) (i : DIn) : (lstarRaw prm).toFun (r₀, r₁, r₂, r₃, r₄, i) = lstarCheck (List.length (prm.toFun i.1).1) (List.length (prm.toFun i.1).2) r₄.spineList.length r₃.spineList.length r₂.spineList.length r₁.spineList.length r₀.bitsListD i.2.2.2.1 i.2.2.2.2

noncomputable def MIPRE.Tailored.AnsRed.lstarFinal (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) : Cost.PolyTimeFun FIn Bool

The check of the output indicator, as a program: it decides LstarOK at the table size 2^ℓ and the copy size 2^◇ that prm gives the index (lstarFinal_apply).

Equations

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

theorem MIPRE.Tailored.AnsRed.lstarFinal_apply (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) (r₀ r₁ r₂ r₃ r₄ : Cost.Data) (i : DIn) : (lstarFinal prm).toFun (r₀, r₁, r₂, r₃, r₄, i) = decide (LstarOK (2 ^ List.length (prm.toFun i.1).1) (2 ^ List.length (prm.toFun i.1).2) r₄.spineList.length r₃.spineList.length r₂.spineList.length r₁.spineList.length r₀.bitsListD i.2.2.2.1 i.2.2.2.2)

The output indicator

noncomputable def MIPRE.Tailored.AnsRed.lstarTail₄ (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) (P : Cost.Prog) : Cost.Prog

After the fourth run of the answer-length calculator: run the processor, then check.

Equations

• MIPRE.Tailored.AnsRed.lstarTail₄ prm P = MIPRE.Cost.seqProg (MIPRE.Tailored.canonIn₅.code.pushProg P) (MIPRE.Tailored.AnsRed.lstarFinal prm).code

noncomputable def MIPRE.Tailored.AnsRed.lstarTail₃ (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) (L P : Cost.Prog) : Cost.Prog

After the third run.

Equations

• MIPRE.Tailored.AnsRed.lstarTail₃ prm L P = MIPRE.Cost.seqProg (MIPRE.Tailored.canonIn₄.code.pushProg L) (MIPRE.Tailored.AnsRed.lstarTail₄ prm P)

noncomputable def MIPRE.Tailored.AnsRed.lstarTail₂ (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) (L P : Cost.Prog) : Cost.Prog

After the second run.

Equations

• MIPRE.Tailored.AnsRed.lstarTail₂ prm L P = MIPRE.Cost.seqProg (MIPRE.Tailored.canonIn₃.code.pushProg L) (MIPRE.Tailored.AnsRed.lstarTail₃ prm L P)

noncomputable def MIPRE.Tailored.AnsRed.lstarTail₁ (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) (L P : Cost.Prog) : Cost.Prog

After the first run.

Equations

• MIPRE.Tailored.AnsRed.lstarTail₁ prm L P = MIPRE.Cost.seqProg (MIPRE.Tailored.canonIn₂.code.pushProg L) (MIPRE.Tailored.AnsRed.lstarTail₂ prm L P)

noncomputable def MIPRE.Tailored.AnsRed.lstarProg (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) (L P : Cost.Prog) : Cost.Prog

The output indicator L* of a tailored verifier with answer-length calculator L and processor P (Definition defn:decider-read), at the parameter program prm: on encode (n, x, y, a, b), the four runs of L and the run of P of the canonical decider, then the check.

Equations

• MIPRE.Tailored.AnsRed.lstarProg prm L P = MIPRE.Cost.seqProg (MIPRE.Tailored.canonIn₁.code.pushProg L) (MIPRE.Tailored.AnsRed.lstarTail₁ prm L P)

theorem MIPRE.Tailored.AnsRed.lstarTail₄_wellScoped (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) {P : Cost.Prog} (hP : Cost.Prog.WellScoped 1 P) : Cost.Prog.WellScoped 1 (lstarTail₄ prm P)

theorem MIPRE.Tailored.AnsRed.lstarTail₃_wellScoped (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) {L P : Cost.Prog} (hL : Cost.Prog.WellScoped 1 L) (hP : Cost.Prog.WellScoped 1 P) : Cost.Prog.WellScoped 1 (lstarTail₃ prm L P)

theorem MIPRE.Tailored.AnsRed.lstarTail₂_wellScoped (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) {L P : Cost.Prog} (hL : Cost.Prog.WellScoped 1 L) (hP : Cost.Prog.WellScoped 1 P) : Cost.Prog.WellScoped 1 (lstarTail₂ prm L P)

theorem MIPRE.Tailored.AnsRed.lstarTail₁_wellScoped (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) {L P : Cost.Prog} (hL : Cost.Prog.WellScoped 1 L) (hP : Cost.Prog.WellScoped 1 P) : Cost.Prog.WellScoped 1 (lstarTail₁ prm L P)

theorem MIPRE.Tailored.AnsRed.lstarProg_wellScoped (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) {L P : Cost.Prog} (hL : Cost.Prog.WellScoped 1 L) (hP : Cost.Prog.WellScoped 1 P) : Cost.Prog.WellScoped 1 (lstarProg prm L P)

theorem MIPRE.Tailored.AnsRed.lstarProg_accepts (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) {L P : Cost.Prog} (hL : Cost.Prog.WellScoped 1 L) (hP : Cost.Prog.WellScoped 1 P) (i : DIn) : (∃ (t : ℕ), (lstarProg prm L P).Runs (Cost.encode i) (Cost.encode true) t) ↔ ∃ (r₁ : Cost.Data) (r₂ : Cost.Data) (r₃ : Cost.Data) (r₄ : Cost.Data) (r₀ : Cost.Data), (∃ (t : ℕ), L.Runs (Cost.encode (i.1, i.2.1, false)) r₁ t) ∧ (∃ (t : ℕ), L.Runs (Cost.encode (i.1, i.2.1, true)) r₂ t) ∧ (∃ (t : ℕ), L.Runs (Cost.encode (i.1, i.2.2.1, false)) r₃ t) ∧ (∃ (t : ℕ), L.Runs (Cost.encode (i.1, i.2.2.1, true)) r₄ t) ∧ (∃ (t : ℕ), P.Runs (Cost.encode (i.1, i.2.1, i.2.2.1, List.take r₁.spineList.length i.2.2.2.1, List.take r₃.spineList.length i.2.2.2.2)) r₀ t) ∧ LstarOK (2 ^ List.length (prm.toFun i.1).1) (2 ^ List.length (prm.toFun i.1).2) r₁.spineList.length r₂.spineList.length r₃.spineList.length r₄.spineList.length r₀.bitsListD i.2.2.2.1 i.2.2.2.2

The output indicator accepts exactly when the five runs halt and the check passes.

noncomputable def MIPRE.Tailored.AnsRed.lstar (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) {ℓ : ℕ} (V : TailoredVerifier ℓ) : Decider

The output indicator of a tailored verifier, at the parameter program prm, as a decider on (n, x, y, a, b).

Equations

• MIPRE.Tailored.AnsRed.lstar prm V = { prog := MIPRE.Tailored.AnsRed.lstarProg prm V.len.prog V.lp.prog, closed := ⋯ }

theorem MIPRE.Tailored.AnsRed.lstar_accepts_iff (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) {ℓ : ℕ} (V : TailoredVerifier ℓ) (n : ℕ) (x y a b : Cost.BitStr) : (lstar prm V).Accepts n x y a b ↔ ∃ (lRx : ℕ) (lLx : ℕ) (lRy : ℕ) (lLy : ℕ) (cs : List Cost.BitStr), LenIs V.len n x false lRx ∧ LenIs V.len n x true lLx ∧ LenIs V.len n y false lRy ∧ LenIs V.len n y true lLy ∧ LpIs V.lp n x y (List.take lRx a) (List.take lRy b) cs ∧ LstarOK (2 ^ List.length (prm.toFun n).1) (2 ^ List.length (prm.toFun n).2) lRx lLx lRy lLy cs a b

What the output indicator accepts (claim:properties_of_L*): (n, x, y, a, b) such that the answer-length calculator gives the four lengths, the processor gives the constraints cs on the readable answers cut at the readable lengths, and the check passes at the parameters of the index.