The repeated linear-constraints processor meets its specification

RepSpec.lp_iff for repLp (issue #280, P2b): at good questions and readable answers of the right lengths, the processor halts exactly when every coordinate's processor does, and then outputs the product's constraints. The lengths the program reads off the calculator's outputs are the coordinates' (lensOf_quarter), so its twelve lengths at a coordinate are those of TailoredGame.padCons (lens_lpPads), its queries to the input processor are the coordinates' (lpPQs_eq), and its output is the product's constraints (lpOut_eq).

Lengths of the scans

theorem MIPRE.Tailored.RepProg.length_flatten_unary (L : List Cost.Unary) : L.flatten.length = (List.map List.length L).sum

theorem MIPRE.Tailored.RepProg.lens_triples (L : List Cost.Unary) (i : ℕ) (hi : i < L.length) : List.map List.length (triples L)[i] = [(List.take i (List.map List.length L)).sum, (List.map List.length L)[i], (List.drop (i + 1) (List.map List.length L)).sum]

The lengths of the triple at a position: the sum before, the length at, the sum after.

@[simp]

theorem MIPRE.Tailored.RepProg.length_triples (L : List Cost.Unary) : (triples L).length = L.length

@[simp]

theorem MIPRE.Tailored.RepProg.length_padData (A B C D : List Cost.Unary) : (padData A B C D).length = min (min A.length B.length) (min C.length D.length)

theorem MIPRE.Tailored.RepProg.getElem_padData (A B C D : List Cost.Unary) (i : ℕ) (h : i < (padData A B C D).length) : (padData A B C D)[i] = (triples A)[i] ++ (triples B)[i] ++ ((triples C)[i] ++ (triples D)[i])

Sums over the coordinates

theorem MIPRE.Tailored.RepProg.sum_take_ofFn_eq {k : ℕ} (f : Fin k → ℕ) (i : Fin k) : (List.take (↑i) (List.ofFn f)).sum = ∑ j : Fin k with j < i, f j

theorem MIPRE.Tailored.RepProg.sum_drop_ofFn_eq {k : ℕ} (f : Fin k → ℕ) (i : Fin k) : (List.drop (↑i + 1) (List.ofFn f)).sum = ∑ j : Fin k, f j - (∑ j : Fin k with j < i, f j + f i)

Quarters

theorem MIPRE.Tailored.RepProg.quarter_append (A B C D : List Cost.Data) {k : ℕ} (hA : A.length = k) (hB : B.length = k) (hC : C.length = k) (hD : D.length = k) : quarter (A ++ B ++ (C ++ D)) k 0 = A ∧ quarter (A ++ B ++ (C ++ D)) k 1 = B ∧ quarter (A ++ B ++ (C ++ D)) k 2 = C ∧ quarter (A ++ B ++ (C ++ D)) k 3 = D

theorem MIPRE.Tailored.RepProg.forall₂_quarter {R : Cost.Data → Cost.Data → Prop} {l₁ l₂ : List Cost.Data} (h : List.Forall₂ R l₁ l₂) (k j : ℕ) : List.Forall₂ R (quarter l₁ k j) (quarter l₂ k j)

theorem MIPRE.Tailored.RepProg.lens_lensOf {ℓ : ℕ} (V : TailoredVerifier ℓ) (n : ℕ) (b : Bool) (bl : List Cost.BitStr) (rs : List Cost.Data) : (∀ xi ∈ bl, ∃ (k : ℕ), LenIs V.len n xi b k) → List.Forall₂ (fun (q r : Cost.Data) => ∃ (t : ℕ), Cost.selfUniversal.univ.Runs ((Cost.encode V.len.prog).cons q) r t) (List.map (fun (xi : Cost.BitStr) => Cost.encode (n, xi, b)) bl) rs → List.map List.length (lensOf rs) = List.map (fun (xi : Cost.BitStr) => V.lenOf n xi b) bl

The calls to the input calculator answered, the lengths read off the results are the coordinates'.

theorem MIPRE.Tailored.RepProg.padWithL_eq {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x y : Fin k → X) (i : Fin k) (p : List Cost.Unary) (hp : List.map List.length p = [G.preR x i, G.lenR (x i), G.sufR x i, G.preL x i, G.lenL (x i), G.sufL x i, G.preR y i, G.lenR (y i), G.sufR y i, G.preL y i, G.lenL (y i), G.sufL y i]) (c : Cost.BitStr) : padWithL p c = G.padCons x y i c

The padding by twelve lengths is the padding of the product.

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.RepProg.specSt {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau n : ℕ) (x y : Fin (TailoredVerifier.K lam tau n * V.sampler.dim n) → CL.𝔽₂) (aR bR : Cost.BitStr) : LpSt

The state of the processor at (n, x, y, a^R, b^R).

Equations

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

theorem MIPRE.Tailored.RepProg.blocksX_specSt {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau n : ℕ) (x y : Fin (TailoredVerifier.K lam tau n * V.sampler.dim n) → CL.𝔽₂) (aR bR : Cost.BitStr) : blocksX (specSt V lam tau n x y aR bR) = List.ofFn fun (i : Fin (TailoredVerifier.K lam tau n)) => CL.toBits (V.qc lam tau n x i)

theorem MIPRE.Tailored.RepProg.blocksY_specSt {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau n : ℕ) (x y : Fin (TailoredVerifier.K lam tau n * V.sampler.dim n) → CL.𝔽₂) (aR bR : Cost.BitStr) : blocksY (specSt V lam tau n x y aR bR) = List.ofFn fun (i : Fin (TailoredVerifier.K lam tau n)) => CL.toBits (V.qc lam tau n y i)

theorem MIPRE.Tailored.RepProg.lens_quarters {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau n : ℕ) (x y : Fin (TailoredVerifier.K lam tau n * V.sampler.dim n) → CL.𝔽₂) (aR bR : Cost.BitStr) (hx : ∀ (i : Fin (TailoredVerifier.K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n x i))) (hy : ∀ (i : Fin (TailoredVerifier.K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n y i))) (rs₁ : List Cost.Data) (hrs : List.Forall₂ (fun (q r : Cost.Data) => ∃ (t : ℕ), Cost.selfUniversal.univ.Runs ((Cost.encode V.len.prog).cons q) r t) (lpLenQs (specSt V lam tau n x y aR bR)) rs₁) : (List.map List.length (lensOf (quarter rs₁ (TailoredVerifier.K lam tau n) 0)) = List.ofFn fun (i : Fin (TailoredVerifier.K lam tau n)) => (V.tgame n).lenR ((V.qEquiv lam tau n) x i)) ∧ (List.map List.length (lensOf (quarter rs₁ (TailoredVerifier.K lam tau n) 1)) = List.ofFn fun (i : Fin (TailoredVerifier.K lam tau n)) => (V.tgame n).lenL ((V.qEquiv lam tau n) x i)) ∧ (List.map List.length (lensOf (quarter rs₁ (TailoredVerifier.K lam tau n) 2)) = List.ofFn fun (i : Fin (TailoredVerifier.K lam tau n)) => (V.tgame n).lenR ((V.qEquiv lam tau n) y i)) ∧ List.map List.length (lensOf (quarter rs₁ (TailoredVerifier.K lam tau n) 3)) = List.ofFn fun (i : Fin (TailoredVerifier.K lam tau n)) => (V.tgame n).lenL ((V.qEquiv lam tau n) y i)

The calls to L̄ answered by rs₁, the four quarters of lengths.

theorem MIPRE.Tailored.RepProg.lens_lpPads {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau n : ℕ) (x y : Fin (TailoredVerifier.K lam tau n * V.sampler.dim n) → CL.𝔽₂) (aR bR : Cost.BitStr) (hx : ∀ (i : Fin (TailoredVerifier.K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n x i))) (hy : ∀ (i : Fin (TailoredVerifier.K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n y i))) (rs₁ : List Cost.Data) (hrs : List.Forall₂ (fun (q r : Cost.Data) => ∃ (t : ℕ), Cost.selfUniversal.univ.Runs ((Cost.encode V.len.prog).cons q) r t) (lpLenQs (specSt V lam tau n x y aR bR)) rs₁) : (lpPads rs₁ (TailoredVerifier.K lam tau n)).length = TailoredVerifier.K lam tau n ∧ ∀ (i : Fin (TailoredVerifier.K lam tau n)), List.map List.length ((lpPads rs₁ (TailoredVerifier.K lam tau n)).getD ↑i []) = [(V.tgame n).preR ((V.qEquiv lam tau n) x) i, (V.tgame n).lenR ((V.qEquiv lam tau n) x i), (V.tgame n).sufR ((V.qEquiv lam tau n) x) i, (V.tgame n).preL ((V.qEquiv lam tau n) x) i, (V.tgame n).lenL ((V.qEquiv lam tau n) x i), (V.tgame n).sufL ((V.qEquiv lam tau n) x) i, (V.tgame n).preR ((V.qEquiv lam tau n) y) i, (V.tgame n).lenR ((V.qEquiv lam tau n) y i), (V.tgame n).sufR ((V.qEquiv lam tau n) y) i, (V.tgame n).preL ((V.qEquiv lam tau n) y) i, (V.tgame n).lenL ((V.qEquiv lam tau n) y i), (V.tgame n).sufL ((V.qEquiv lam tau n) y) i]

The twelve lengths of every coordinate are those of the product's padding.

theorem MIPRE.Tailored.RepProg.length_getD_of_lens {p : List Cost.Unary} {l : List ℕ} (hp : List.map List.length p = l) (j : ℕ) : List.length (p.getD j []) = l.getD j 0

theorem MIPRE.Tailored.RepProg.lpPQs_eq {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau n : ℕ) (x y : Fin (TailoredVerifier.K lam tau n * V.sampler.dim n) → CL.𝔽₂) (aR bR : Cost.BitStr) (hx : ∀ (i : Fin (TailoredVerifier.K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n x i))) (hy : ∀ (i : Fin (TailoredVerifier.K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n y i))) (rs₁ : List Cost.Data) (hrs : List.Forall₂ (fun (q r : Cost.Data) => ∃ (t : ℕ), Cost.selfUniversal.univ.Runs ((Cost.encode V.len.prog).cons q) r t) (lpLenQs (specSt V lam tau n x y aR bR)) rs₁) : lpPQs (specSt V lam tau n x y aR bR) rs₁ = List.ofFn fun (i : Fin (TailoredVerifier.K lam tau n)) => Cost.encode (n, CL.toBits (V.qc lam tau n x i), CL.toBits (V.qc lam tau n y i), (V.tgame n).coordR ((V.qEquiv lam tau n) x) aR i, (V.tgame n).coordR ((V.qEquiv lam tau n) y) bR i)

The queries to the input processor are the coordinates'.

theorem MIPRE.Tailored.RepProg.lpOut_eq {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau n : ℕ) (x y : Fin (TailoredVerifier.K lam tau n * V.sampler.dim n) → CL.𝔽₂) (aR bR : Cost.BitStr) (hx : ∀ (i : Fin (TailoredVerifier.K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n x i))) (hy : ∀ (i : Fin (TailoredVerifier.K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n y i))) (rs₁ : List Cost.Data) (hrs : List.Forall₂ (fun (q r : Cost.Data) => ∃ (t : ℕ), Cost.selfUniversal.univ.Runs ((Cost.encode V.len.prog).cons q) r t) (lpLenQs (specSt V lam tau n x y aR bR)) rs₁) (rs₂ : List Cost.Data) (h₂ : rs₂.length = TailoredVerifier.K lam tau n) : lpOut (lpPads rs₁ (TailoredVerifier.K lam tau n)) rs₂ = List.flatMap (fun (i : Fin (TailoredVerifier.K lam tau n)) => List.map ((V.tgame n).padCons ((V.qEquiv lam tau n) x) ((V.qEquiv lam tau n) y) i) (rs₂.getD (↑i) Cost.Data.nil).bitsListD) (List.finRange (TailoredVerifier.K lam tau n))

The output is the padded constraints of the coordinates.

The processor

noncomputable def MIPRE.Tailored.RepProg.repLpProg (sp lp pp : Cost.Prog) (lam tau : ℕ) : Cost.Prog

The program of the repeated processor: the core with (S̄, L̄, P̄, λ, τ) stored.

Equations

• MIPRE.Tailored.RepProg.repLpProg sp lp pp lam tau = MIPRE.Cost.hardcode (MIPRE.Tailored.RepProg.lpCore MIPRE.Cost.selfUniversal.univ) (MIPRE.Cost.encode (sp, lp, pp, lam, tau))

noncomputable def MIPRE.Tailored.RepProg.repLp {ℓ : ℕ} (S : CL.Sampler ℓ) (L P : Decider) (lam tau : ℕ) : Decider

The repeated linear-constraints processor.

Equations

• MIPRE.Tailored.RepProg.repLp S L P lam tau = { prog := MIPRE.Tailored.RepProg.repLpProg S.prog L.prog P.prog lam tau, closed := ⋯ }

The specification

noncomputable def MIPRE.Tailored.RepProg.chooseRun (c q : Cost.Data) : Cost.Data

A result of univ on (c, q), when there is one.

Equations

• MIPRE.Tailored.RepProg.chooseRun c q = if h : ∃ (r : MIPRE.Cost.Data) (t : ℕ), MIPRE.Cost.selfUniversal.univ.Runs (c.cons q) r t then h.choose else MIPRE.Cost.Data.nil

theorem MIPRE.Tailored.RepProg.chooseRun_spec {c q : Cost.Data} (h : ∃ (r : Cost.Data) (t : ℕ), Cost.selfUniversal.univ.Runs (c.cons q) r t) : ∃ (t : ℕ), Cost.selfUniversal.univ.Runs (c.cons q) (chooseRun c q) t

theorem MIPRE.Tailored.RepProg.forall₂_map_self {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (f : α → β) {l : List α} : (∀ a ∈ l, R a (f a)) → List.Forall₂ R l (List.map f l)

theorem MIPRE.Tailored.RepProg.mem_lenQueries {n : ℕ} {bl : List Cost.BitStr} {q : Cost.Data} (h : q ∈ lenQueries n bl) : ∃ xi ∈ bl, ∃ (b : Bool), q = Cost.encode (n, xi, b)

theorem MIPRE.Tailored.RepProg.repLp_lpIs_iff {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau n : ℕ) (x y : Fin (TailoredVerifier.K lam tau n * V.sampler.dim n) → CL.𝔽₂) (aR bR : Cost.BitStr) (hx : ∀ (i : Fin (TailoredVerifier.K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n x i))) (hy : ∀ (i : Fin (TailoredVerifier.K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n y i))) (cs : List Cost.BitStr) : LpIs (repLp V.sampler V.len V.lp lam tau) n (CL.toBits x) (CL.toBits y) aR bR cs ↔ (∀ (i : Fin (TailoredVerifier.K lam tau n)), ∃ (c : List Cost.BitStr), LpIs V.lp n (CL.toBits (V.qc lam tau n x i)) (CL.toBits (V.qc lam tau n y i)) ((V.tgame n).coordR ((V.qEquiv lam tau n) x) aR i) ((V.tgame n).coordR ((V.qEquiv lam tau n) y) bR i) c) ∧ cs = ((V.tgame n).repeat (TailoredVerifier.K lam tau n)).cons ((V.qEquiv lam tau n) x) ((V.qEquiv lam tau n) y) aR bR

RepSpec.lp_iff for the repeated processor.

theorem MIPRE.Tailored.RepProg.repSpec {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau n : ℕ) : V.RepSpec lam tau (repLen V.sampler V.len lam tau) (repLp V.sampler V.len V.lp lam tau) n

The repeated programs meet their specification at every index.