The canonical decider, as a program

Paper II, II:1757–1787: the canonical decider of a tailored normal form verifier, on the questions x, y and the answers a, b of index n, runs the answer-length calculator L on (n, x, κ) and (n, y, κ) for both kinds κ of variables, checks that |a| = ℓ^R(x) + ℓ^L(x) and |b| = ℓ^R(y) + ℓ^L(y), runs the linear-constraints processor LP on the readable parts (n, x, y, a^R, b^R), and accepts when every constraint c it outputs satisfies ⟨c, (a, b, 1)⟩ = 0. This file writes it as a program of the ambient model.

• Prog.pushProg F P: from a state s, running P on an input F s built from it and pushing the output onto the state — with its runs and its inversion, and that of Cost.seqProg.
• The polynomial-time pieces: the readings of Cost.Data.spineList and Cost.Data.bitsListD as programs, the length check, satF (one linear constraint, through the parity dot product LowDegree.BinaryLinear.dotBitsProg) and allSatF (all of them).
• canonProg L LP: the four runs of L, the run of LP, and the final check, in sequence; canonProg_accepts: it accepts exactly when the five runs halt and the check passes.

Running programs in sequence

theorem MIPRE.Cost.seqProg_inv {p q : Prog} (hq : Prog.WellScoped 1 q) {x z : Data} {t : ℕ} (h : (seqProg p q).Runs x z t) : ∃ (y : Data) (s : ℕ) (u : ℕ), p.Runs x y s ∧ q.Runs y z u

Inverting seqProg: a run of p then q is a run of p, and one of q on its output.

def MIPRE.Cost.Prog.pushProg (F P : Prog) : Prog

From a state s: build the input F s, run the closed program P on it, and push its output onto the state, cons (P (F s)) s.

Equations

• F.pushProg P = F.let_ (((MIPRE.Cost.Prog.var 0).let_ P).let_ ((MIPRE.Cost.Prog.var 0).cons (MIPRE.Cost.Prog.var 2)))

theorem MIPRE.Cost.Prog.pushProg_wellScoped {F P : Prog} (hF : WellScoped 1 F) (hP : WellScoped 1 P) : WellScoped 1 (F.pushProg P)

theorem MIPRE.Cost.Prog.pushProg_runs {F P : Prog} (hP : WellScoped 1 P) {s v r : Data} {t₁ t₂ : ℕ} (h₁ : F.Runs s v t₁) (h₂ : P.Runs v r t₂) : ∃ (t : ℕ), (F.pushProg P).Runs s (r.cons s) t

theorem MIPRE.Cost.Prog.pushProg_inv {F P : Prog} (hP : WellScoped 1 P) {s out : Data} {t : ℕ} (h : (F.pushProg P).Runs s out t) : ∃ (v : Data) (r : Data) (t₁ : ℕ) (t₂ : ℕ), F.Runs s v t₁ ∧ P.Runs v r t₂ ∧ out = r.cons s

Steps, as polynomial-time functions

theorem MIPRE.Cost.PolyTimeFun.pushSeq_iff {σ : Type u_1} {τ : Type u_2} [SizedEncoding σ] [SizedEncoding τ] (F : PolyTimeFun σ τ) {P Q : Prog} (hP : Prog.WellScoped 1 P) (hQ : Prog.WellScoped 1 Q) (s : σ) (out : Data) : (∃ (t : ℕ), (seqProg (F.code.pushProg P) Q).Runs (encode s) out t) ↔ ∃ (r : Data), (∃ (t : ℕ), P.Runs (encode (F.toFun s)) r t) ∧ ∃ (t : ℕ), Q.Runs (encode (r, s)) out t

A step followed by the rest: running pushProg F P and then Q from the state s is running P on F s, to some output r, and Q on the new state (r, s).

theorem MIPRE.Cost.PolyTimeFun.runs_true_iff {σ : Type u_1} [SizedEncoding σ] (C : PolyTimeFun σ Bool) (s : σ) : (∃ (t : ℕ), C.code.Runs (encode s) (encode true) t) ↔ C.toFun s = true

A polynomial-time decision accepts exactly when it is true.

Reading data, as programs

noncomputable def MIPRE.Cost.PolyTimeFun.spineF : PolyTimeFun Data (List Data)

Every datum encodes its spineList.

Equations

• MIPRE.Cost.PolyTimeFun.spineF = MIPRE.Cost.PolyTimeFun.ofEncodeEq MIPRE.Cost.Data.spineList ⋯

noncomputable def MIPRE.Cost.PolyTimeFun.bitDF : PolyTimeFun Data Bool

A datum read as a bit.

Equations

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

noncomputable def MIPRE.Cost.PolyTimeFun.bitsListF : PolyTimeFun Data (List BitStr)

A datum read as a list of bit strings.

Equations

• MIPRE.Cost.PolyTimeFun.bitsListF = (MIPRE.Cost.PolyTimeFun.bitDF.map.comp MIPRE.Cost.PolyTimeFun.spineF).map.comp MIPRE.Cost.PolyTimeFun.spineF

@[simp]

theorem MIPRE.Cost.PolyTimeFun.bitsListF_apply (d : Data) : bitsListF.toFun d = d.bitsListD

noncomputable def MIPRE.Cost.PolyTimeFun.lenUnaryF : PolyTimeFun Data Unary

A datum read as a length in unary.

Equations

• MIPRE.Cost.PolyTimeFun.lenUnaryF = MIPRE.Cost.PolyTimeFun.length.comp MIPRE.Cost.PolyTimeFun.spineF

@[simp]

theorem MIPRE.Cost.PolyTimeFun.lenUnaryF_apply (d : Data) : lenUnaryF.toFun d = unary d.spineList.length

noncomputable def MIPRE.Cost.PolyTimeFun.lenBitsF : PolyTimeFun Data BitStr

A datum read as a length, written as that many falses.

Equations

• MIPRE.Cost.PolyTimeFun.lenBitsF = (MIPRE.Cost.PolyTimeFun.const false).map.comp MIPRE.Cost.PolyTimeFun.spineF

@[simp]

theorem MIPRE.Cost.PolyTimeFun.lenBitsF_apply (d : Data) : lenBitsF.toFun d = List.map (fun (x : Data) => false) d.spineList

noncomputable def MIPRE.Cost.PolyTimeFun.falsesF : PolyTimeFun BitStr BitStr

A bit string's length, written as that many falses.

Equations

• MIPRE.Cost.PolyTimeFun.falsesF = (MIPRE.Cost.PolyTimeFun.const false).map

@[simp]

theorem MIPRE.Cost.PolyTimeFun.falsesF_apply (a : BitStr) : falsesF.toFun a = List.map (fun (x : Bool) => false) a

One linear constraint, and all of them

theorem MIPRE.Tailored.map_false_eq_iff {α : Type u_1} {β : Type u_2} (a : List α) (b : List β) : List.map (fun (x : α) => false) a = List.map (fun (x : β) => false) b ↔ a.length = b.length

theorem MIPRE.Tailored.even_count_zipWith_iff (c v : Cost.BitStr) : Even (List.count true (List.zipWith (fun (x1 x2 : Bool) => x1 && x2) c v)) ↔ LowDegree.BinaryLinear.dotBits c v = false

The parity of the number of common ones is the parity dot product of LowDegree.BinaryLinear.

noncomputable def MIPRE.Tailored.satF : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) Bool

One constraint: c and v have the same length and ⟨c, v⟩ = 0.

Equations

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

@[simp]

theorem MIPRE.Tailored.satF_apply (p : Cost.BitStr × Cost.BitStr) : satF.toFun p = decide (Satisfies p.1 p.2)

noncomputable def MIPRE.Tailored.allSatStep : Cost.PolyTimeFun ((Bool × Cost.BitStr) × Cost.BitStr) (Bool × Cost.BitStr)

The step of allSatF: conjoin one more constraint, keeping the vector.

Equations

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

@[simp]

theorem MIPRE.Tailored.allSatStep_apply (s : Bool × Cost.BitStr) (c : Cost.BitStr) : allSatStep.toFun (s, c) = (s.1 && decide (Satisfies c s.2), s.2)

theorem MIPRE.Tailored.esize_allSatStep (s : Bool × Cost.BitStr) (c : Cost.BitStr) : Cost.esize (allSatStep.toFun (s, c)) ≤ Cost.esize s + Polynomial.eval (Cost.esize c) 2

theorem MIPRE.Tailored.foldl_allSatStep (cs : List Cost.BitStr) (b : Bool) (v : Cost.BitStr) : List.foldl (fun (s : Bool × Cost.BitStr) (c : Cost.BitStr) => allSatStep.toFun (s, c)) (b, v) cs = (b && cs.all fun (c : Cost.BitStr) => decide (Satisfies c v), v)

noncomputable def MIPRE.Tailored.allSatF : Cost.PolyTimeFun (List Cost.BitStr × Cost.BitStr) Bool

All constraints of a list are satisfied by v.

Equations

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

@[simp]

theorem MIPRE.Tailored.allSatF_apply (p : List Cost.BitStr × Cost.BitStr) : allSatF.toFun p = decide (∀ c ∈ p.1, Satisfies c p.2)

The canonical decider

@[reducible, inline]

abbrev MIPRE.Tailored.DIn : Type

The input of a decider, (n, x, y, a, b).

Equations

• MIPRE.Tailored.DIn = (ℕ × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

noncomputable def MIPRE.Tailored.canonIn₁ : Cost.PolyTimeFun DIn (ℕ × Cost.BitStr × Bool)

The input of the first run of L, (n, x, false).

Equations

• MIPRE.Tailored.canonIn₁ = MIPRE.Cost.PolyTimeFun.fst.pair ((MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd).pair (MIPRE.Cost.PolyTimeFun.const false))

noncomputable def MIPRE.Tailored.canonIn₂ : Cost.PolyTimeFun (Cost.Data × DIn) (ℕ × Cost.BitStr × Bool)

The input of the second run of L, (n, x, true).

Equations

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

noncomputable def MIPRE.Tailored.canonIn₃ : Cost.PolyTimeFun (Cost.Data × Cost.Data × DIn) (ℕ × Cost.BitStr × Bool)

The input of the third run of L, (n, y, false).

Equations

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

noncomputable def MIPRE.Tailored.canonIn₄ : Cost.PolyTimeFun (Cost.Data × Cost.Data × Cost.Data × DIn) (ℕ × Cost.BitStr × Bool)

The input of the fourth run of L, (n, y, true).

Equations

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

noncomputable def MIPRE.Tailored.canonIn₅ : Cost.PolyTimeFun (Cost.Data × Cost.Data × Cost.Data × Cost.Data × DIn) DIn

The input of the run of LP: (n, x, y, a^R, b^R), the readable parts cut at the lengths the first and the third run of L wrote.

Equations

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

noncomputable def MIPRE.Tailored.canonFinal : Cost.PolyTimeFun (Cost.Data × Cost.Data × Cost.Data × Cost.Data × Cost.Data × DIn) Bool

The final check, on the five outputs and the input.

Equations

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

noncomputable def MIPRE.Tailored.canonTail₄ (P : Cost.Prog) : Cost.Prog

The canonical decider after the fourth run of L: run LP, then check.

Equations

• MIPRE.Tailored.canonTail₄ P = MIPRE.Cost.seqProg (MIPRE.Tailored.canonIn₅.code.pushProg P) MIPRE.Tailored.canonFinal.code

noncomputable def MIPRE.Tailored.canonTail₃ (L P : Cost.Prog) : Cost.Prog

After the third run of L.

Equations

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

noncomputable def MIPRE.Tailored.canonTail₂ (L P : Cost.Prog) : Cost.Prog

After the second run of L.

Equations

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

noncomputable def MIPRE.Tailored.canonTail₁ (L P : Cost.Prog) : Cost.Prog

After the first run of L.

Equations

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

noncomputable def MIPRE.Tailored.canonProg (L P : Cost.Prog) : Cost.Prog

The canonical decider of a tailored verifier with answer-length calculator L and linear-constraints processor P (II:1757–1787), on encode (n, x, y, a, b): four runs of L, one of P, and the final check, in sequence.

Equations

• MIPRE.Tailored.canonProg L P = MIPRE.Cost.seqProg (MIPRE.Tailored.canonIn₁.code.pushProg L) (MIPRE.Tailored.canonTail₁ L P)

theorem MIPRE.Tailored.canonTail₄_wellScoped {P : Cost.Prog} (hP : Cost.Prog.WellScoped 1 P) : Cost.Prog.WellScoped 1 (canonTail₄ P)

theorem MIPRE.Tailored.canonTail₃_wellScoped {L P : Cost.Prog} (hL : Cost.Prog.WellScoped 1 L) (hP : Cost.Prog.WellScoped 1 P) : Cost.Prog.WellScoped 1 (canonTail₃ L P)

theorem MIPRE.Tailored.canonTail₂_wellScoped {L P : Cost.Prog} (hL : Cost.Prog.WellScoped 1 L) (hP : Cost.Prog.WellScoped 1 P) : Cost.Prog.WellScoped 1 (canonTail₂ L P)

theorem MIPRE.Tailored.canonTail₁_wellScoped {L P : Cost.Prog} (hL : Cost.Prog.WellScoped 1 L) (hP : Cost.Prog.WellScoped 1 P) : Cost.Prog.WellScoped 1 (canonTail₁ L P)

theorem MIPRE.Tailored.canonProg_wellScoped {L P : Cost.Prog} (hL : Cost.Prog.WellScoped 1 L) (hP : Cost.Prog.WellScoped 1 P) : Cost.Prog.WellScoped 1 (canonProg L P)

@[simp]

theorem MIPRE.Tailored.canonIn₁_apply (i : DIn) : canonIn₁.toFun i = (i.1, i.2.1, false)

@[simp]

theorem MIPRE.Tailored.canonIn₂_apply (r : Cost.Data) (i : DIn) : canonIn₂.toFun (r, i) = (i.1, i.2.1, true)

@[simp]

theorem MIPRE.Tailored.canonIn₃_apply (r r' : Cost.Data) (i : DIn) : canonIn₃.toFun (r, r', i) = (i.1, i.2.2.1, false)

@[simp]

theorem MIPRE.Tailored.canonIn₄_apply (r r' r'' : Cost.Data) (i : DIn) : canonIn₄.toFun (r, r', r'', i) = (i.1, i.2.2.1, true)

@[simp]

theorem MIPRE.Tailored.canonIn₅_apply (r₄ r₃ r₂ r₁ : Cost.Data) (i : DIn) : canonIn₅.toFun (r₄, r₃, r₂, r₁, i) = (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)

theorem MIPRE.Tailored.canonFinal_apply (r₀ r₁ r₂ r₃ r₄ : Cost.Data) (i : DIn) : canonFinal.toFun (r₀, r₁, r₂, r₃, r₄, i) = (decide (List.length i.2.2.2.1 = r₄.spineList.length + r₃.spineList.length) && (decide (List.length i.2.2.2.2 = r₂.spineList.length + r₁.spineList.length) && decide (∀ c ∈ r₀.bitsListD, Satisfies c (i.2.2.2.1 ++ i.2.2.2.2 ++ [true]))))

The final check, read: the two lengths, and every constraint.

theorem MIPRE.Tailored.canonProg_accepts {L P : Cost.Prog} (hL : Cost.Prog.WellScoped 1 L) (hP : Cost.Prog.WellScoped 1 P) (i : DIn) : (∃ (t : ℕ), (canonProg 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) ∧ List.length i.2.2.2.1 = r₁.spineList.length + r₂.spineList.length ∧ List.length i.2.2.2.2 = r₃.spineList.length + r₄.spineList.length ∧ ∀ c ∈ r₀.bitsListD, Satisfies c (i.2.2.2.1 ++ i.2.2.2.2 ++ [true])

The canonical decider accepts exactly when the five runs halt and the check passes.