The linear-constraints processor of the introspection verifier

Issue #281 (Phase 3 of planning/aldous-lyons-track.md): the linear-constraints processor P^intro of the tailored presentation of Introspection.seven, at the input's three programs (S, L, P) and the parameter λ. On (n, x, y, a^R, b^R), for λ ≥ 1 and n ≥ 1, its program

1. prepares the shared resources as the decision kernel of seven does (DecisionPreparation.prog): the clock 2^{(λn + 1)^5} in unary, the index 2^n, the Pauli parameters (k, j, 2^j) in unary, Q and R;
2. puts Q and R in unary (ClockArithmetic.bothUnary);
3. runs the core mainP (LpIntroCons.lean) on the environment, with the input's description clamped to λ (InputRuns.clamp) stored in the program (hardcode).

At λ = 0 it is the empty program, and at n = 0 it inspects the index in place (LenIntro.lenWrap) and outputs nil: both output the empty list of constraints.

• lpIntroC c U V λ, lpIntroProgC c U: the processor and its program from (V, λ), in polynomial time (lpIntroProgC_eq);
• lpIntroC_lpIs: what it outputs, on every input, at positive λ and n; lpIntroC_lpIs_zero: the empty list at λ = 0 or n = 0;
• lpIntro, lpIntroProg: the same at sevenConstant and selfClockedUniversal;
• lpIntro_cons_eq: the cons_eq clause of Output.IntroSpec for a λ-bounded input whose normal form verifier T.ofTNFVT U0 is λ-bounded, at n ≥ 1; introSpec_lenIntro_lpIntro: the whole specification, with LenIntro.lenIntro.

The kernel input

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.LpIntro.KIn : Type

The prepared resources, the description typed.

Equations

• MIPRE.Tailored.Intro.LpIntro.KIn = (MIPRE.Cost.Data × MIPRE.Tailored.Intro.InputRuns.Metadata × MIPRE.Cost.Unary × ℕ × MIPRE.Introspection.PauliSamplerParameters.Parameters × ℕ × ℕ)

noncomputable def MIPRE.Tailored.Intro.LpIntro.kernelInput (c : ℕ) (M : InputRuns.Metadata) (x : Cost.Data) : KIn

The resources DecisionPreparation.prog prepares from cons (encode M) x.

Equations

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

theorem MIPRE.Tailored.Intro.LpIntro.encode_kernelInput (c : ℕ) (M : InputRuns.Metadata) (x : Cost.Data) : Cost.encode (kernelInput c M x) = Cost.encode (Introspection.DecisionPreparation.resources c ((Cost.encode M).cons x))

noncomputable def MIPRE.Tailored.Intro.LpIntro.argQR : Cost.PolyTimeFun Cost.Data Cost.Data

The pair (Q, R) in the encoded resources.

Equations

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

theorem MIPRE.Tailored.Intro.LpIntro.argQR_kernelInput (c : ℕ) (M : InputRuns.Metadata) (x : Cost.Data) : argQR.toFun (Cost.encode (kernelInput c M x)) = Cost.encode (Introspection.SourceCompiler.registerBits c M.2 (Introspection.ClockSimulation.indexReader.toFun x), Introspection.SourceCompiler.originalBound M.2 (Introspection.ClockSimulation.indexReader.toFun x))

noncomputable def MIPRE.Tailored.Intro.LpIntro.rX : Cost.PolyTimeFun Cost.Data Cost.BitStr

The readers of the raw input (n, x, y, a, b).

Equations

• MIPRE.Tailored.Intro.LpIntro.rX = MIPRE.CL.Detyping.Program.readBits.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Cost.PolyTimeFun.treeTail)

noncomputable def MIPRE.Tailored.Intro.LpIntro.rY : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

• MIPRE.Tailored.Intro.LpIntro.rY = MIPRE.CL.Detyping.Program.readBits.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeTail))

noncomputable def MIPRE.Tailored.Intro.LpIntro.rA : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.rB : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.toIIn : Cost.PolyTimeFun (KIn × Cost.Unary × Cost.Unary) IIn

The core's input, from the resources and (Q, R) in unary.

Equations

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

theorem MIPRE.Tailored.Intro.LpIntro.toIIn_kernelInput (c lam n : ℕ) (M : InputRuns.Metadata) (hM : M.2 = lam) (xs ys aR bR : Cost.BitStr) : toIIn.toFun (kernelInput c M (Cost.encode (n, xs, ys, aR, bR)), Cost.unary (Introspection.SourceCompiler.registerBits c lam n), Cost.unary (Introspection.SourceCompiler.originalBound lam n)) = ((envOf c lam n M, aR, bR), xs, ys)

noncomputable def MIPRE.Tailored.Intro.LpIntro.kernel (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun (KIn × Cost.Unary × Cost.Unary) (List Cost.BitStr)

The kernel: the core on the prepared input.

Equations

• MIPRE.Tailored.Intro.LpIntro.kernel U = (MIPRE.Tailored.Intro.LpIntro.mainP U).comp MIPRE.Tailored.Intro.LpIntro.toIIn

noncomputable def MIPRE.Tailored.Intro.LpIntro.core (c : ℕ) (U : Cost.ClockedUniversalMachine) : Cost.Prog

The core program on cons (encode M) (n, x, y, a, b).

Equations

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

theorem MIPRE.Tailored.Intro.LpIntro.core_wellScoped (c : ℕ) (U : Cost.ClockedUniversalMachine) : Cost.Prog.WellScoped 1 (core c U)

theorem MIPRE.Tailored.Intro.LpIntro.core_runs (c : ℕ) (U : Cost.ClockedUniversalMachine) (M : InputRuns.Metadata) (x : Cost.Data) : ∃ (t : ℕ), (core c U).Runs ((Cost.encode M).cons x) (Cost.encode ((kernel U).toFun (kernelInput c M x, Cost.unary (Introspection.SourceCompiler.registerBits c M.2 (Introspection.ClockSimulation.indexReader.toFun x)), Cost.unary (Introspection.SourceCompiler.originalBound M.2 (Introspection.ClockSimulation.indexReader.toFun x))))) t

The processor

noncomputable def MIPRE.Tailored.Intro.LpIntro.lpProg (c : ℕ) (U : Cost.ClockedUniversalMachine) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : Cost.Prog

The program of the processor at the input's programs V and λ: empty at λ = 0, otherwise the core with the clamped description stored, behind the index test.

Equations

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

theorem MIPRE.Tailored.Intro.LpIntro.lpProg_wellScoped (c : ℕ) (U : Cost.ClockedUniversalMachine) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : Cost.Prog.WellScoped 1 (lpProg c U V lam)

noncomputable def MIPRE.Tailored.Intro.LpIntro.lpIntroC (c : ℕ) (U : Cost.ClockedUniversalMachine) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : Decider

The linear-constraints processor of the introspection verifier at the constant c, the clocked universal machine U, the input's programs V and the level λ.

Equations

• MIPRE.Tailored.Intro.LpIntro.lpIntroC c U V lam = { prog := MIPRE.Tailored.Intro.LpIntro.lpProg c U V lam, closed := ⋯ }

noncomputable def MIPRE.Tailored.Intro.LpIntro.lpIntroProgC (c : ℕ) (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun InputRuns.Metadata Cost.Prog

The processor's program from (V, λ), in polynomial time.

Equations

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

theorem MIPRE.Tailored.Intro.LpIntro.lpIntroProgC_eq (c : ℕ) (U : Cost.ClockedUniversalMachine) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : (lpIntroProgC c U).toFun (V, lam) = (lpIntroC c U V lam).prog

theorem MIPRE.Tailored.Intro.LpIntro.lpIntroC_lpIs (c : ℕ) (U : Cost.ClockedUniversalMachine) (V : Cost.Prog × Cost.Prog × Cost.Prog) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) (xs ys aR bR : Cost.BitStr) : LpIs (lpIntroC c U V lam) n xs ys aR bR ((mainP U).toFun ((envOf c lam n (InputRuns.clamp.toFun (V, lam)), aR, bR), xs, ys))

What the processor outputs at positive λ and n: the core on the environment of the clamped description.

theorem MIPRE.Tailored.Intro.LpIntro.lpIntroC_lpIs_zero (c : ℕ) (U : Cost.ClockedUniversalMachine) (V : Cost.Prog × Cost.Prog × Cost.Prog) {lam n : ℕ} (h : lam = 0 ∨ n = 0) (xs ys aR bR : Cost.BitStr) : LpIs (lpIntroC c U V lam) n xs ys aR bR []

At λ = 0 or n = 0 the processor outputs no constraint.

At the constant of Introspection.seven

noncomputable def MIPRE.Tailored.Intro.LpIntro.lpIntro (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : Decider

The linear-constraints processor P^intro_λ of the tailored presentation of Introspection.seven, at the input's programs V.

Equations

• MIPRE.Tailored.Intro.LpIntro.lpIntro V lam = MIPRE.Tailored.Intro.LpIntro.lpIntroC MIPRE.Introspection.sevenConstant MIPRE.Cost.selfClockedUniversal V lam

noncomputable def MIPRE.Tailored.Intro.LpIntro.lpIntroProg : Cost.PolyTimeFun ((Cost.Prog × Cost.Prog × Cost.Prog) × ℕ) Cost.Prog

Its program from (V, λ), in polynomial time.

Equations

• MIPRE.Tailored.Intro.LpIntro.lpIntroProg = MIPRE.Tailored.Intro.LpIntro.lpIntroProgC MIPRE.Introspection.sevenConstant MIPRE.Cost.selfClockedUniversal

theorem MIPRE.Tailored.Intro.LpIntro.lpIntroProg_eq (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : lpIntroProg.toFun (V, lam) = (lpIntro V lam).prog

theorem MIPRE.Tailored.Intro.LpIntro.lpIntro_lpIs_zero {V : Cost.Prog × Cost.Prog × Cost.Prog} {lam n : ℕ} (h : lam = 0 ∨ n = 0) (xs ys aR bR : Cost.BitStr) : LpIs (lpIntro V lam) n xs ys aR bR []

At λ = 0 or n = 0, the processor outputs no constraint.

The specification

theorem MIPRE.Tailored.Intro.LpIntro.toBits_qe {c : ℕ} {hc : 1 ≤ c} {he : Even c} {lam n : ℕ} {U : Cost.ClockedUniversalMachine} {V : Verifier 7} (hl : 1 ≤ lam) (hn : 1 ≤ n) (x : CL.Detyping.Coord Label (Fin (Introspection.PauliSampler.dimension c lam n)) → ZMod 2) : CL.toBits ((Output.qe c hc he U V hl hn) x) = CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv (Introspection.PauliSampler.dimension c lam n)) x)

theorem MIPRE.Tailored.Intro.LpIntro.lpIntroC_cons_eq {c : ℕ} (hc : 1 ≤ c) (he : Even c) {lam n : ℕ} (U : Cost.ClockedUniversalMachine) (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hV : V.IsBounded lam) (hl : 1 ≤ lam) (hn : 1 ≤ n) (hsamp : V.sampler.prog = T.sampler.prog) (hs : V.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (x y : CL.Detyping.Coord Label (Fin (Introspection.PauliSampler.dimension c lam n)) → ZMod 2) (aR bR : Cost.BitStr) : LpIs (lpIntroC c U T.progs lam) n (CL.toBits ((Output.qe c hc he U V hl hn) x)) (CL.toBits ((Output.qe c hc he U V hl hn) y)) aR bR ((presented Introspection.DecisionCompiler.graph (Sound.H c hc he lam n U V) (Sound.tdata c hc he lam n T V hs (regKerGens (Introspection.SourceCompiler.registerBits c lam n)))).cons x y aR bR)

The cons_eq clause of the specification, at a constant c: for a λ-bounded input T and a λ-bounded normal form verifier V with T's sampler program, at n ≥ 1, the processor outputs at every pair of detyped questions the presented game's constraints.

theorem MIPRE.Tailored.Intro.LpIntro.lpIntro_cons_eq {lam n : ℕ} (T : TailoredVerifier 7) (U0 : Cost.UniversalMachine) (hT : T.IsBounded lam) (hV : (T.ofTNFVT U0).IsBounded lam) (hl : 1 ≤ lam) (hn : 1 ≤ n) (hs : (T.ofTNFVT U0).sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits Introspection.sevenConstant lam n) (x y : CL.Detyping.Coord Label (Fin (Introspection.PauliSampler.dimension Introspection.sevenConstant lam n)) → ZMod 2) (aR bR : Cost.BitStr) : LpIs (lpIntro T.progs lam) n (CL.toBits ((Output.qe Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ Cost.selfClockedUniversal (T.ofTNFVT U0) hl hn) x)) (CL.toBits ((Output.qe Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ Cost.selfClockedUniversal (T.ofTNFVT U0) hl hn) y)) aR bR ((presented Introspection.DecisionCompiler.graph (Sound.H Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ lam n Cost.selfClockedUniversal (T.ofTNFVT U0)) (Sound.tdata Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ lam n T (T.ofTNFVT U0) hs (regKerGens (Introspection.SourceCompiler.registerBits Introspection.sevenConstant lam n)))).cons x y aR bR)

The cons_eq clause of Output.IntroSpec for lpIntro: for a λ-bounded tailored input T whose normal form verifier T.ofTNFVT U0 is λ-bounded, at n ≥ 1, with the kernel generators regKerGens.

theorem MIPRE.Tailored.Intro.LpIntro.introSpec_lenIntro_lpIntro {lam n : ℕ} (T : TailoredVerifier 7) (U0 : Cost.UniversalMachine) (hT : T.IsBounded lam) (hV : (T.ofTNFVT U0).IsBounded lam) (hl : 1 ≤ lam) (hn : 1 ≤ n) (hs : (T.ofTNFVT U0).sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits Introspection.sevenConstant lam n) : Output.IntroSpec Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ Cost.selfClockedUniversal (T.ofTNFVT U0) hl hn (presented Introspection.DecisionCompiler.graph (Sound.H Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ lam n Cost.selfClockedUniversal (T.ofTNFVT U0)) (Sound.tdata Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ lam n T (T.ofTNFVT U0) hs (regKerGens (Introspection.SourceCompiler.registerBits Introspection.sevenConstant lam n)))) (LenIntro.lenIntro lam) (lpIntro T.progs lam)

The specification Output.IntroSpec of the output's two programs, with LenIntro.lenIntro and lpIntro: for a λ-bounded tailored input T whose normal form verifier T.ofTNFVT U0 is λ-bounded, at n ≥ 1, with the kernel generators regKerGens.