The constraints of the introspection processor at a pair of detyped questions

Issue #281. The processor's core (mainP) on the environment, the two readable answers and the two detyped questions: it decodes the edge of the two graph views (edgeSel, the router's selectedEdge as a finite table), branches on it over the finite label alphabet (Cost.PolyTimeFun.choose), checks the readable lengths, and computes the constraints of Typed.consRaw at the edge's labels (rawP): the Pauli basis test (pauliConsProg), the Pauli to auxiliary clauses (pauliAuxP, in either order), and the auxiliary pairs (auxPairP).

mainP_spec: on the environment of a bounded input and the bits of two detyped questions, the output is the detyped game's constraints, TypedData.detype's cons on Sound.tdata.

@[reducible, inline]

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

The labels.

Equations

• MIPRE.Tailored.Intro.LpIntro.Label = MIPRE.Introspection.DecisionKernel.Label

The lengths of a label

noncomputable def MIPRE.Tailored.Intro.LpIntro.lenU (t : Label) (κ : Bool) : Cost.PolyTimeFun Env Cost.Unary

The length of kind κ of a label, in unary (LenIntro.lin on the parameters).

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.totLenU (t : Label) : Cost.PolyTimeFun Env Cost.Unary

The total length of a label, in unary.

Equations

• MIPRE.Tailored.Intro.LpIntro.totLenU t = MIPRE.Tailored.Intro.catF (MIPRE.Tailored.Intro.LpIntro.lenU t false) (MIPRE.Tailored.Intro.LpIntro.lenU t true)

theorem MIPRE.Tailored.Intro.LpIntro.envT_par (c lam n : ℕ) (T : TailoredVerifier 7) : (envT c lam n T).2.2.2.1 = (Cost.unary (kk c lam n), Cost.unary (jj c lam n), Cost.unary (2 ^ jj c lam n))

theorem MIPRE.Tailored.Intro.LpIntro.length_lenU (c lam n : ℕ) (T : TailoredVerifier 7) (t : Label) (κ : Bool) : List.length ((lenU t κ).toFun (envT c lam n T)) = if κ = true then Typed.len (kk c lam n) (jj c lam n) ((2 ^ n) ^ lam) t - Typed.lenR (kk c lam n) (jj c lam n) ((2 ^ n) ^ lam) t else Typed.lenR (kk c lam n) (jj c lam n) ((2 ^ n) ^ lam) t

theorem MIPRE.Tailored.Intro.LpIntro.length_lenU_false (c lam n : ℕ) (T : TailoredVerifier 7) (t : Label) : List.length ((lenU t false).toFun (envT c lam n T)) = Typed.lenR (kk c lam n) (jj c lam n) ((2 ^ n) ^ lam) t

theorem MIPRE.Tailored.Intro.LpIntro.length_totLenU (c lam n : ℕ) (T : TailoredVerifier 7) (t : Label) : List.length ((totLenU t).toFun (envT c lam n T)) = Typed.len (kk c lam n) (jj c lam n) ((2 ^ n) ^ lam) t

The Pauli to auxiliary clauses

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.LpIntro.zD : Cost.PolyTimeFun DIn Cost.BitStr

Q zeros.

Equations

• MIPRE.Tailored.Intro.LpIntro.zD = MIPRE.Tailored.Intro.zerosOf (MIPRE.Tailored.Intro.LpIntro.eQ.comp MIPRE.Tailored.Intro.LpIntro.dE)

noncomputable def MIPRE.Tailored.Intro.LpIntro.pauliHideP (U : Cost.ClockedUniversalMachine) (w : Bool) : Cost.PolyTimeFun DIn (List Cost.BitStr)

The first hiding edge's constraints (pauliHideCons at the first factor and its kernel generators), role w.

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.pauliDirP (U : Cost.ClockedUniversalMachine) (p : QLD.Ty) (t : Introspection.AuxType 7 × Bool) : Cost.PolyTimeFun DIn (List Cost.BitStr)

The directed clauses from a Pauli label to an auxiliary one (Typed.pauliDir).

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.pauliAuxP (U : Cost.ClockedUniversalMachine) (p : QLD.Ty) (t : Introspection.AuxType 7 × Bool) : Cost.PolyTimeFun DIn (List Cost.BitStr)

The constraints from a Pauli label to an auxiliary one (Typed.pauliAux).

Equations

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

The pair of questions

@[reducible, inline]

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

The environment, the two readable answers and the two questions' bits.

Equations

• MIPRE.Tailored.Intro.LpIntro.IIn = (MIPRE.Tailored.Intro.LpIntro.DIn × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

noncomputable def MIPRE.Tailored.Intro.LpIntro.iD : Cost.PolyTimeFun IIn DIn

Equations

• MIPRE.Tailored.Intro.LpIntro.iD = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Tailored.Intro.LpIntro.iX : Cost.PolyTimeFun IIn Cost.BitStr

Equations

• MIPRE.Tailored.Intro.LpIntro.iX = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Tailored.Intro.LpIntro.iY : Cost.PolyTimeFun IIn Cost.BitStr

Equations

• MIPRE.Tailored.Intro.LpIntro.iY = MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.iD_apply (i : IIn) : iD.toFun i = i.1

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.iX_apply (i : IIn) : iX.toFun i = i.2.1

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.iY_apply (i : IIn) : iY.toFun i = i.2.2

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.LpIntro.gd : ℕ

The number of bits of a graph view.

Equations

• MIPRE.Tailored.Intro.LpIntro.gd = MIPRE.CL.Detyping.graphDim MIPRE.Tailored.Intro.LpIntro.Label

noncomputable def MIPRE.Tailored.Intro.LpIntro.contentOf (x : Cost.PolyTimeFun IIn Cost.BitStr) : Cost.PolyTimeFun IIn Cost.BitStr

The content of a question: its bits after the graph view.

Equations

• MIPRE.Tailored.Intro.LpIntro.contentOf x = MIPRE.Tailored.Intro.dropOf x (MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary MIPRE.Tailored.Intro.LpIntro.gd))

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.contentOf_apply (x : Cost.PolyTimeFun IIn Cost.BitStr) (i : IIn) : (contentOf x).toFun i = List.drop gd (x.toFun i)

noncomputable def MIPRE.Tailored.Intro.LpIntro.edgeSel : Cost.PolyTimeFun IIn (Option (Label × Label))

The edge of the two graph views (the router's selectedEdge), by a finite table.

Equations

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

theorem MIPRE.Tailored.Intro.LpIntro.edgeSel_apply (i : IIn) : edgeSel.toFun i = CL.Detyping.DeciderProgram.selectedEdge Introspection.DecisionCompiler.graph (CL.Detyping.graphOfBits i.2.1) (CL.Detyping.graphOfBits i.2.2)

noncomputable def MIPRE.Tailored.Intro.LpIntro.rawP (U : Cost.ClockedUniversalMachine) : Label → Label → Cost.PolyTimeFun IIn (List Cost.BitStr)

The constraints at a pair of labels before the length check (Typed.consRaw).

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Tailored.Intro.LpIntro.rawP U (Sum.inl p) (Sum.inr t) = (MIPRE.Tailored.Intro.LpIntro.pauliAuxP U p t).comp MIPRE.Tailored.Intro.LpIntro.iD
• MIPRE.Tailored.Intro.LpIntro.rawP U (Sum.inr t) (Sum.inr u) = (MIPRE.Tailored.Intro.LpIntro.auxPairP U t u).comp MIPRE.Tailored.Intro.LpIntro.iD

noncomputable def MIPRE.Tailored.Intro.LpIntro.consP (U : Cost.ClockedUniversalMachine) : Option (Label × Label) → Cost.PolyTimeFun IIn (List Cost.BitStr)

The constraints at an edge (Typed.consL), none off the edges.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Tailored.Intro.LpIntro.consP U none = MIPRE.Cost.PolyTimeFun.const []

noncomputable def MIPRE.Tailored.Intro.LpIntro.mainP (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun IIn (List Cost.BitStr)

The core of the processor: branch on the edge.

Equations

• MIPRE.Tailored.Intro.LpIntro.mainP U = MIPRE.Tailored.Intro.LpIntro.edgeSel.choose (MIPRE.Tailored.Intro.LpIntro.consP U) (MIPRE.Cost.PolyTimeFun.const [])

Correctness

theorem MIPRE.Tailored.Intro.LpIntro.edgeOf_eq_selectedEdge {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x y : CL.Detyping.Coord Label ι → ZMod 2) : edgeOf Introspection.DecisionCompiler.graph x y = Option.map (fun (uv : Introspection.QuestionType QLD.Ty 7 × Introspection.QuestionType QLD.Ty 7) => ((uv.1, CL.pull Function.Embedding.inr x), uv.2, CL.pull Function.Embedding.inr y)) (CL.Detyping.DeciderProgram.selectedEdge Introspection.DecisionCompiler.graph (CL.pull Function.Embedding.inl x) (CL.pull Function.Embedding.inl y))

The edge of a pair of detyped questions is the router's selected edge, with the contents.

theorem MIPRE.Tailored.Intro.LpIntro.pauliHideP_spec (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (he : Even c) (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hsamp : V.sampler.prog = T.sampler.prog) (hs : V.sampler.dim (2 ^ n) ≤ QQ c lam n) (w : Bool) (aR bR : Cost.BitStr) : (pauliHideP U w).toFun (envT c lam n T, aR, bR) = PauliHide.pauliHideCons (kk c lam n) ⋯ ⋯ (jj c lam n) (LL V hs w) (regKerGens (QQ c lam n) ((LL V hs w).factorOfPrefix 0 0) (Introspection.CLChecks.stageLinear (LL V hs w) 0 0))

The first hiding edge's constraints.

theorem MIPRE.Tailored.Intro.LpIntro.pauliLenR_Z (k m : ℕ) : PauliCons.pauliLenR k m (QLD.Ty.pauli QLD.Bas.Z) = pauliLen m k (QLD.Ty.pauli QLD.Bas.Z)

theorem MIPRE.Tailored.Intro.LpIntro.pauliDirP_spec (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (he : Even c) (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hsamp : V.sampler.prog = T.sampler.prog) (hs : V.sampler.dim (2 ^ n) ≤ QQ c lam n) (p : QLD.Ty) (t : Introspection.AuxType 7 × Bool) (aR bR : Cost.BitStr) (ha : List.length aR = PauliCons.pauliLenR (kk c lam n) (2 ^ jj c lam n) p) : (pauliDirP U p t).toFun (envT c lam n T, aR, bR) = Typed.pauliDir (kk c lam n) ⋯ ⋯ (jj c lam n) ((2 ^ n) ^ lam) V hs (regKerGens (QQ c lam n)) p t aR bR

The directed clauses from a Pauli label to an auxiliary one.

theorem MIPRE.Tailored.Intro.LpIntro.pauliAuxP_spec (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (he : Even c) (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hsamp : V.sampler.prog = T.sampler.prog) (hs : V.sampler.dim (2 ^ n) ≤ QQ c lam n) (p : QLD.Ty) (t : Introspection.AuxType 7 × Bool) (aR bR : Cost.BitStr) (ha : List.length aR = PauliCons.pauliLenR (kk c lam n) (2 ^ jj c lam n) p) (hb : List.length bR = auxLenR (QQ c lam n) ((2 ^ n) ^ lam) t.1) : (pauliAuxP U p t).toFun (envT c lam n T, aR, bR) = Typed.pauliAux (kk c lam n) ⋯ ⋯ (jj c lam n) ((2 ^ n) ^ lam) T V hs (regKerGens (QQ c lam n)) p t aR bR

The constraints from a Pauli label to an auxiliary one.

theorem MIPRE.Tailored.Intro.LpIntro.rawP_spec (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (hc : 1 ≤ c) (he : Even c) (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hsamp : V.sampler.prog = T.sampler.prog) (hs : V.sampler.dim (2 ^ n) ≤ QQ c lam n) (u v : Label) (aR bR xs ys : Cost.BitStr) (hx : (List.drop gd xs).length = Introspection.PauliSampler.dimension c lam n) (hy : (List.drop gd ys).length = Introspection.PauliSampler.dimension c lam n) (ha : List.length aR = Typed.lenR (kk c lam n) (jj c lam n) ((2 ^ n) ^ lam) u) (hb : List.length bR = Typed.lenR (kk c lam n) (jj c lam n) ((2 ^ n) ^ lam) v) : (rawP U u v).toFun ((envT c lam n T, aR, bR), xs, ys) = Typed.consRaw (kk c lam n) ⋯ ⋯ (jj c lam n) ⋯ ((2 ^ n) ^ lam) T V hs (regKerGens (QQ c lam n)) u v (List.drop gd xs) (List.drop gd ys) aR bR

The constraints at a pair of labels, before the length check, for readable answers of the labels' readable lengths and contents of the sampler's dimension.

theorem MIPRE.Tailored.Intro.LpIntro.mainP_spec (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (hc : 1 ≤ c) (he : Even c) (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hsamp : V.sampler.prog = T.sampler.prog) (hs : V.sampler.dim (2 ^ n) ≤ QQ c lam n) (x y : CL.Detyping.Coord Label (Fin (Introspection.PauliSampler.dimension c lam n)) → CL.𝔽₂) (aR bR : Cost.BitStr) : (mainP U).toFun ((envT c lam n T, aR, bR), CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv (Introspection.PauliSampler.dimension c lam n)) x), CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv (Introspection.PauliSampler.dimension c lam n)) y)) = match edgeOf Introspection.DecisionCompiler.graph x y with | some (u, v) => (Sound.tdata c hc he lam n T V hs (regKerGens (QQ c lam n))).cons u v aR bR | none => []

The core of the processor at two detyped questions: the detyped game's constraints.