The register data of the introspection processor

Issue #281 (Phase 3 of planning/aldous-lyons-track.md). The linear-constraints processor of the tailored introspection verifier (LpIntro.lean) works on an environment Env prepared once per input: the clock 2^{(λn + 1)^5} in unary, the clamped description of the input M, the index 2^n, the Pauli parameters (k, j, 2^j) in unary and the register width Q and the cutoff R in unary (envOf). This file computes from it, at an auxiliary label t and a register y of Q bits, the data the readable condition Typed.G reads:

• ctxP w: the kernel's context (CLData.context) of role w;
• srcQP t: the input question srcQuestion t y;
• splitU κ t: the input's split srcSplitR/srcSplitL at the register, in unary, by a clocked run of the input's answer-length calculator (InputRuns);
• GP t: the readable condition Typed.G itself, as a Boolean.

Each has its correctness theorem at envOf c λ n (clamp (T.progs, λ)), for a λ-bounded tailored input T, a λ-bounded normal form verifier V with T's sampler program, and 1 ≤ n.

The environment

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.LpIntro.kk (c lam n : ℕ) : ℕ

The field width k and the selector width j at (c, λ, n).

Equations

• MIPRE.Tailored.Intro.LpIntro.kk c lam n = MIPRE.Introspection.SourceCompiler.fieldBits c lam n

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.LpIntro.jj (c lam n : ℕ) : ℕ

Equations

• MIPRE.Tailored.Intro.LpIntro.jj c lam n = MIPRE.Introspection.PauliSamplerParameters.selectorBits c lam n

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.LpIntro.QQ (c lam n : ℕ) : ℕ

The register width Q = 2^{2^j} k (SourceCompiler.registerBits), in the form of Typed.Q.

Equations

• MIPRE.Tailored.Intro.LpIntro.QQ c lam n = 2 ^ 2 ^ MIPRE.Tailored.Intro.LpIntro.jj c lam n * MIPRE.Tailored.Intro.LpIntro.kk c lam n

theorem MIPRE.Tailored.Intro.LpIntro.QQ_eq (c lam n : ℕ) : QQ c lam n = Introspection.SourceCompiler.registerBits c lam n

@[reducible, inline]

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

The environment: the clock, the clamped description, the index 2^n, the Pauli parameters, Q and R in unary.

Equations

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

def MIPRE.Tailored.Intro.LpIntro.envOf (c lam n : ℕ) (M : InputRuns.Metadata) : Env

The environment at (c, λ, n) and the description M.

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.eClock : Cost.PolyTimeFun Env Cost.Unary

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.eM : Cost.PolyTimeFun Env InputRuns.Metadata

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.eIdx : Cost.PolyTimeFun Env ℕ

Equations

• MIPRE.Tailored.Intro.LpIntro.eIdx = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.Tailored.Intro.LpIntro.ePar : Cost.PolyTimeFun Env Introspection.PauliSamplerParameters.Parameters

Equations

• MIPRE.Tailored.Intro.LpIntro.ePar = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Tailored.Intro.LpIntro.eQ : Cost.PolyTimeFun Env Cost.Unary

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.eR : Cost.PolyTimeFun Env Cost.Unary

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.eClock_apply (e : Env) : eClock.toFun e = e.1

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.eM_apply (e : Env) : eM.toFun e = e.2.1

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.eIdx_apply (e : Env) : eIdx.toFun e = e.2.2.1

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.ePar_apply (e : Env) : ePar.toFun e = e.2.2.2.1

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.eQ_apply (e : Env) : eQ.toFun e = e.2.2.2.2.1

@[simp]

theorem MIPRE.Tailored.Intro.LpIntro.eR_apply (e : Env) : eR.toFun e = e.2.2.2.2.2

noncomputable def MIPRE.Tailored.Intro.LpIntro.ctxP (w : Bool) : Cost.PolyTimeFun Env Introspection.AuxiliarySource.Context

The kernel's context of role w, from the environment.

Equations

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

theorem MIPRE.Tailored.Intro.LpIntro.toBits_zero (Q : ℕ) : CL.toBits 0 = List.replicate Q false

theorem MIPRE.Tailored.Intro.LpIntro.ctxP_envOf (c lam n : ℕ) (M : InputRuns.Metadata) (V : Verifier 7) (hM : M.1.1 = V.sampler.prog) (w : Bool) : (ctxP w).toFun (envOf c lam n M) = CLData.context V lam n (Introspection.SourceCompiler.registerBits c lam n) w

The register level

@[reducible, inline]

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

A register with the environment.

Equations

• MIPRE.Tailored.Intro.LpIntro.RIn = (MIPRE.Tailored.Intro.LpIntro.Env × MIPRE.Cost.BitStr)

noncomputable def MIPRE.Tailored.Intro.LpIntro.cIn (w : Bool) : Cost.PolyTimeFun RIn CLData.Input

The kernel's input of role w: its context and the register.

Equations

• MIPRE.Tailored.Intro.LpIntro.cIn w = ((MIPRE.Tailored.Intro.LpIntro.ctxP w).comp MIPRE.Cost.PolyTimeFun.fst).pair MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Tailored.Intro.LpIntro.srcQP (U : Cost.ClockedUniversalMachine) (t : Introspection.AuxType 7 × Bool) : Cost.PolyTimeFun RIn Cost.BitStr

The input question at an auxiliary label: L_w of the register at Sample, the register's first dim bits otherwise.

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.lenReadU : Cost.PolyTimeFun Cost.Data Cost.Unary

A clocked result read as a length, in unary.

Equations

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

theorem MIPRE.Tailored.Intro.LpIntro.length_lenReadU (d : Cost.Data) : List.length (lenReadU.toFun d) = InputRuns.lenRead.toFun d

theorem MIPRE.Tailored.Intro.LpIntro.isEmpty_drop (u v : Cost.Unary) : (List.drop (List.length v) u).isEmpty = decide (List.length u ≤ List.length v)

noncomputable def MIPRE.Tailored.Intro.LpIntro.splitU (U : Cost.ClockedUniversalMachine) (κ : Bool) (t : Introspection.AuxType 7 × Bool) : Cost.PolyTimeFun RIn Cost.Unary

The input's split at an auxiliary label, in unary: readable (κ = false) or linear.

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.fitsCore (U : Cost.ClockedUniversalMachine) (t : Introspection.AuxType 7 × Bool) : Cost.PolyTimeFun RIn Bool

Whether the input's answer fits the cutoff, off Hide (srcFits).

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.fitsP (U : Cost.ClockedUniversalMachine) (t : Introspection.AuxType 7 × Bool) : Cost.PolyTimeFun RIn Bool

Whether the input's answer fits the cutoff (srcFits).

Equations

• MIPRE.Tailored.Intro.LpIntro.fitsP U t = if MIPRE.Tailored.Intro.isHideT t.1 = true then MIPRE.Cost.PolyTimeFun.const true else MIPRE.Tailored.Intro.LpIntro.fitsCore U t

def MIPRE.Tailored.Intro.LpIntro.prefLevel : Introspection.AuxType 7 → Option ℕ

The level of the prefix guard of a label: i at Hide i, 6 at Read.

Equations

• MIPRE.Tailored.Intro.LpIntro.prefLevel (MIPRE.Introspection.AuxType.hide i) = some ↑i
• MIPRE.Tailored.Intro.LpIntro.prefLevel MIPRE.Introspection.AuxType.read = some 6
• MIPRE.Tailored.Intro.LpIntro.prefLevel x✝ = none

noncomputable def MIPRE.Tailored.Intro.LpIntro.prefP (U : Cost.ClockedUniversalMachine) (t : Introspection.AuxType 7 × Bool) : Cost.PolyTimeFun RIn Bool

The prefix condition (Typed.prefixOK).

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.srcP (U : Cost.ClockedUniversalMachine) (t : Introspection.AuxType 7 × Bool) : Cost.PolyTimeFun RIn Bool

Source membership at an Introspect register.

Equations

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

noncomputable def MIPRE.Tailored.Intro.LpIntro.GP (U : Cost.ClockedUniversalMachine) (t : Introspection.AuxType 7 × Bool) : Cost.PolyTimeFun RIn Bool

The readable condition Typed.G, as a Boolean.

Equations

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

Correctness

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.LpIntro.envT (c lam n : ℕ) (T : TailoredVerifier 7) : Env

The environment of the input T at (c, λ, n).

Equations

• MIPRE.Tailored.Intro.LpIntro.envT c lam n T = MIPRE.Tailored.Intro.LpIntro.envOf c lam n (MIPRE.Tailored.Intro.InputRuns.clamp.toFun (T.progs, lam))

theorem MIPRE.Tailored.Intro.LpIntro.ctxP_envT {c lam n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hsamp : V.sampler.prog = T.sampler.prog) (w : Bool) : (ctxP w).toFun (envT c lam n T) = CLData.context V lam n (QQ c lam n) w

theorem MIPRE.Tailored.Intro.LpIntro.cIn_envT {c lam n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hsamp : V.sampler.prog = T.sampler.prog) (w : Bool) (y : Cost.BitStr) : (cIn w).toFun (envT c lam n T, y) = (CLData.context V lam n (QQ c lam n) w, y)

theorem MIPRE.Tailored.Intro.LpIntro.srcQP_envT (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (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) (t : Introspection.AuxType 7 × Bool) (y : Cost.BitStr) (hy : List.length y = QQ c lam n) : (srcQP U t).toFun (envT c lam n T, y) = srcQuestion V hs t y

The input question at a register.

theorem MIPRE.Tailored.Intro.LpIntro.length_srcQuestion_le {c lam n : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ QQ c lam n) (t : Introspection.AuxType 7 × Bool) (y : Cost.BitStr) : List.length (srcQuestion V hs t y) ≤ (2 ^ n) ^ lam

The input question has at most (2^n)^λ bits.

theorem MIPRE.Tailored.Intro.LpIntro.length_splitU (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (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) (κ : Bool) (t : Introspection.AuxType 7 × Bool) (y : Cost.BitStr) (hy : List.length y = QQ c lam n) : List.length ((splitU U κ t).toFun (envT c lam n T, y)) = T.lenOf (2 ^ n) (srcQuestion V hs t y) κ

The input's split at a register, in unary.

theorem MIPRE.Tailored.Intro.LpIntro.splitU_envT (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (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) (κ : Bool) (t : Introspection.AuxType 7 × Bool) (y : Cost.BitStr) (hy : List.length y = QQ c lam n) : (splitU U κ t).toFun (envT c lam n T, y) = Cost.unary (T.lenOf (2 ^ n) (srcQuestion V hs t y) κ)

theorem MIPRE.Tailored.Intro.LpIntro.fitsP_envT (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (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) (t : Introspection.AuxType 7 × Bool) (y : Cost.BitStr) (hy : List.length y = QQ c lam n) : (fitsP U t).toFun (envT c lam n T, y) = true ↔ srcFits ((2 ^ n) ^ lam) (srcSplitR T V hs) (srcSplitL T V hs) t y

theorem MIPRE.Tailored.Intro.LpIntro.prefP_envT (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (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) (t : Introspection.AuxType 7 × Bool) (y : Cost.BitStr) (hy : List.length y = QQ c lam n) : (prefP U t).toFun (envT c lam n T, y) = true ↔ Typed.prefixOK (kk c lam n) (jj c lam n) V hs t y

theorem MIPRE.Tailored.Intro.LpIntro.srcP_envT (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (hT : T.IsBounded lam) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hsamp : V.sampler.prog = T.sampler.prog) (t : Introspection.AuxType 7 × Bool) (y : Cost.BitStr) : (srcP U t).toFun (envT c lam n T, y) = true ↔ t.1 = Introspection.AuxType.introspect → Introspection.SourceCompiler.InSource (V.sampler.dim (2 ^ n)) y

theorem MIPRE.Tailored.Intro.LpIntro.GP_envT (U : Cost.ClockedUniversalMachine) {c lam n : ℕ} (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) (t : Introspection.AuxType 7 × Bool) (y : Cost.BitStr) (hy : List.length y = QQ c lam n) : (GP U t).toFun (envT c lam n T, y) = true ↔ Typed.G (kk c lam n) (jj c lam n) ((2 ^ n) ^ lam) T V hs t y

The readable condition Typed.G at a register of Q bits.