The input's CL data, computed from the kernel's context

The linear-constraints processor of the tailored introspection verifier needs, at a register y (a length-Q bit string), data about the padded CL functions L w = AuxiliaryDecision.padded V hs w of the input normal form verifier V at index 2^n. The decision kernel of MIPRE.Introspection.seven already computes all of it from one AuxiliarySource.Context, with a clocked universal machine U; this file exposes each datum as a Cost.PolyTimeFun on Input = AuxiliarySource.Context × BitStr, at the context the kernel builds (context V lam n Q w, the kernel's queryContext with role w), with a correctness theorem for a λ-bounded V, 1 ≤ n and hs : V.sampler.dim (2^n) ≤ Q:

• eval: (L w).eval z (one marginal query at full depth, padded with zeros), and sourceEval, its first dim bits;
• outputPrefix k: the reported prefix (L w).outputPrefix k y, k ≤ 7, read off the kernel's attained-prefix scan (scan), under the guard at k - 1 (Guard);
• factor k and register k: the stage register (L w).factorOfPrefix k y (k < 7, the kernel's factor query at the scanned prefix, under the guard at k) and the prefix register CLChecks.prefixRegister (L w) k y (k ≤ 7, the union of the first k of them, under the guard at k - 1), as length-Q masks (CL.indicatorBits);
• matrix k: the matrix of CLChecks.stageLinear (L w) k y (k < 7, under the guard at k) as matrixBits (LinearMap.toMatrix' _), rows vectorBits (M i), the input format of kernelGeneratorsProg (kernelGenerators);
• guard k and inSource: the prefix guard decide (∃ x, ((L w).truncate k).eval x = (L w).outputPrefix k y) (k ≤ 7) and decide (SourceCompiler.InSource dim y), exactly.

The sampler program is specified only at attained prefixes (CL.Sampler.runs_factor, runs_linear), so the data of stage k are correct only under the prefix guard at k, which is itself computed exactly; at a register that fails it the processor emits rejectConstraint without reading them.

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.CLData.Input : Type

A context of the decision kernel and a register, as a bit string.

Equations

• MIPRE.Tailored.Intro.CLData.Input = (MIPRE.Introspection.AuxiliarySource.Context × MIPRE.Cost.BitStr)

def MIPRE.Tailored.Intro.CLData.context (V : Verifier 7) (lam n Q : ℕ) (w : Bool) : Introspection.AuxiliarySource.Context

The context the kernel builds for V, λ, n, the register width Q and the role w: the shared clock, the sampler program, the index 2^n, the role, and a level and prefix (of length Q) that every query below replaces.

Equations

• MIPRE.Tailored.Intro.CLData.context V lam n Q w = MIPRE.Introspection.SourcePadding.Program.queryContext V lam n w 0 0

The evaluation L_w(z)

noncomputable def MIPRE.Tailored.Intro.CLData.widths (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun Input Introspection.SourcePadding.Program.QContext

The kernel's width data: the source dimension, capped by the register width.

Equations

• MIPRE.Tailored.Intro.CLData.widths U = (MIPRE.Introspection.SourcePadding.Program.adapt U).comp MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Tailored.Intro.CLData.marginalContext (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun Input Introspection.AuxiliarySource.Context

The marginal query at full depth 7 on the first dim bits of the register.

Equations

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

noncomputable def MIPRE.Tailored.Intro.CLData.sourceEval (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun Input Cost.BitStr

The source's evaluation on the first dim bits of the register: L_w of the input verifier, unpadded.

Equations

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

noncomputable def MIPRE.Tailored.Intro.CLData.eval (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun Input Cost.BitStr

The padded evaluation: the source's, followed by zeros up to the register width.

Equations

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

theorem MIPRE.Tailored.Intro.CLData.context_dimension (U : Cost.ClockedUniversalMachine) {lam n : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (Q : ℕ) (w : Bool) : (Introspection.SourcePadding.Program.dimension U).toFun (context V lam n Q w) = V.sampler.dim (2 ^ n)

theorem MIPRE.Tailored.Intro.CLData.widths_context (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) (y : Cost.BitStr) : (widths U).toFun (context V lam n Q w, y) = (Cost.unary (V.sampler.dim (2 ^ n)), context V lam n Q w)

theorem MIPRE.Tailored.Intro.CLData.sourceEval_correct (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) (z : Fin Q → CL.𝔽₂) : (sourceEval U).toFun (context V lam n Q w, CL.toBits z) = CL.toBits (CL.pull (Introspection.AuxiliaryProgram.firstEmbedding hs) ((Introspection.AuxiliaryDecision.padded V hs w).eval z))

The source evaluation: the first dim bits of L_w(z), i.e. L_w of the input verifier at the first dim bits of z.

theorem MIPRE.Tailored.Intro.CLData.eval_correct (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) (z : Fin Q → CL.𝔽₂) : (eval U).toFun (context V lam n Q w, CL.toBits z) = CL.toBits ((Introspection.AuxiliaryDecision.padded V hs w).eval z)

The evaluation L_w(z) of the padded input CL function, as a length-Q bit string.

The prefix scan and the reported prefixes

noncomputable def MIPRE.Tailored.Intro.CLData.scan (U : Cost.ClockedUniversalMachine) (k : ℕ) : Cost.PolyTimeFun Input Introspection.AuxiliaryScan.State

The kernel's attained-prefix scan to depth k on the register (AuxiliaryScan.program over the kernel's padded factor and matrix queries).

Equations

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

noncomputable def MIPRE.Tailored.Intro.CLData.outputPrefix (U : Cost.ClockedUniversalMachine) (k : ℕ) : Cost.PolyTimeFun Input Cost.BitStr

The reported prefix outputPrefix k y, the second field of the scan state.

Equations

• MIPRE.Tailored.Intro.CLData.outputPrefix U k = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Tailored.Intro.CLData.scan U k))

def MIPRE.Tailored.Intro.CLData.Guard {Q : ℕ} (V : Verifier 7) {n : ℕ} (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) (k : ℕ) (y : Fin Q → CL.𝔽₂) : Prop

The prefix guard at level k in its semantic form: the reported k-prefix of y is attained by the first k stages.

Equations

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

theorem MIPRE.Tailored.Intro.CLData.guard_mono {Q n : ℕ} (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) {j k : ℕ} (hj : j ≤ k) (y : Fin Q → CL.𝔽₂) (hg : Guard V hs w k y) : Guard V hs w j y

theorem MIPRE.Tailored.Intro.CLData.guard_zero {Q n : ℕ} (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) (y : Fin Q → CL.𝔽₂) : Guard V hs w 0 y

theorem MIPRE.Tailored.Intro.CLData.scan_of_guard (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) {k : ℕ} (hk : k ≤ 7) (y : Fin Q → CL.𝔽₂) (hg : Guard V hs w k y) : ∃ (x : Fin Q → CL.𝔽₂), (scan U k).toFun (context V lam n Q w, CL.toBits y) = (true, CL.toBits ((Introspection.AuxiliaryDecision.padded V hs w).outputPrefix k y), CL.toBits x) ∧ (CL.CLFun.truncate k (Introspection.AuxiliaryDecision.padded V hs w)).eval x = (Introspection.AuxiliaryDecision.padded V hs w).outputPrefix k y

Under the guard at k, the scan succeeds with the reported prefix and a seed attaining it.

theorem MIPRE.Tailored.Intro.CLData.outputPrefix_correct (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) {k : ℕ} (hk : k ≤ 7) (y : Fin Q → CL.𝔽₂) (hg : Guard V hs w (k - 1) y) : (outputPrefix U k).toFun (context V lam n Q w, CL.toBits y) = CL.toBits ((Introspection.AuxiliaryDecision.padded V hs w).outputPrefix k y)

The reported prefix outputPrefix k y, for k ≤ 7, under the guard one level below (no hypothesis at k = 0).

theorem MIPRE.Tailored.Intro.CLData.outputPrefix_correct_of_guard (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) {k : ℕ} (hk : k ≤ 7) (y : Fin Q → CL.𝔽₂) (hg : Guard V hs w k y) : (outputPrefix U k).toFun (context V lam n Q w, CL.toBits y) = CL.toBits ((Introspection.AuxiliaryDecision.padded V hs w).outputPrefix k y)

The reported prefix under the guard at its own level.

The stage register and the prefix register, as masks

noncomputable def MIPRE.Tailored.Intro.CLData.stageContext (U : Cost.ClockedUniversalMachine) (k : ℕ) : Cost.PolyTimeFun Input Introspection.AuxiliarySource.Context

The context of the stage-k source queries: level k + 1 at the scanned prefix.

Equations

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

noncomputable def MIPRE.Tailored.Intro.CLData.factor (U : Cost.ClockedUniversalMachine) (k : ℕ) : Cost.PolyTimeFun Input Cost.BitStr

The register read at stage k, (L w).factorOfPrefix k y, as a length-Q mask.

Equations

• MIPRE.Tailored.Intro.CLData.factor U k = (MIPRE.Introspection.SourcePadding.Program.factorFromContext U).comp (MIPRE.Tailored.Intro.CLData.stageContext U k)

theorem MIPRE.Tailored.Intro.CLData.stageContext_of_guard (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) {k : ℕ} (hk : k ≤ 7) (y : Fin Q → CL.𝔽₂) (hg : Guard V hs w k y) : (stageContext U k).toFun (context V lam n Q w, CL.toBits y) = Introspection.AuxiliaryScan.contextAt (context V lam n Q w) (k + 1) (CL.toBits ((Introspection.AuxiliaryDecision.padded V hs w).outputPrefix k y))

Under the guard at k, the stage-k queries are made at the attained reported prefix.

theorem MIPRE.Tailored.Intro.CLData.factor_correct (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) {k : ℕ} (hk : k < 7) (y : Fin Q → CL.𝔽₂) (hg : Guard V hs w k y) : (factor U k).toFun (context V lam n Q w, CL.toBits y) = CL.indicatorBits ((Introspection.AuxiliaryDecision.padded V hs w).factorOfPrefix k y)

The stage register (L w).factorOfPrefix k y, k < 7, under the guard at k.

noncomputable def MIPRE.Tailored.Intro.CLData.orBitsProg : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) Cost.BitStr

Pointwise disjunction of two bit strings.

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.CLData.orBitsProg_apply (p : Cost.BitStr × Cost.BitStr) : orBitsProg.toFun p = List.zipWith (fun (x1 x2 : Bool) => x1 || x2) p.1 p.2

theorem MIPRE.Tailored.Intro.CLData.indicatorBits_union {Q : ℕ} (A B : Finset (Fin Q)) : CL.indicatorBits (A ∪ B) = List.zipWith (fun (x1 x2 : Bool) => x1 || x2) (CL.indicatorBits A) (CL.indicatorBits B)

def MIPRE.Tailored.Intro.CLData.register (U : Cost.ClockedUniversalMachine) : ℕ → Cost.PolyTimeFun Input Cost.BitStr

The prefix register CLChecks.prefixRegister (L w) k y, the union of the first k stage registers, as a length-Q mask.

Equations

• MIPRE.Tailored.Intro.CLData.register U 0 = MIPRE.Introspection.AuxiliaryScan.zeros.comp MIPRE.Cost.PolyTimeFun.snd
• MIPRE.Tailored.Intro.CLData.register U k.succ = MIPRE.Tailored.Intro.CLData.orBitsProg.comp ((MIPRE.Tailored.Intro.CLData.register U k).pair (MIPRE.Tailored.Intro.CLData.factor U k))

theorem MIPRE.Tailored.Intro.CLData.register_correct (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) {k : ℕ} (hk : k ≤ 7) (y : Fin Q → CL.𝔽₂) (hg : Guard V hs w (k - 1) y) : (register U k).toFun (context V lam n Q w, CL.toBits y) = CL.indicatorBits (Introspection.CLChecks.prefixRegister (Introspection.AuxiliaryDecision.padded V hs w) k y)

The prefix register CLChecks.prefixRegister (L w) k y, k ≤ 7, under the guard one level below (no hypothesis at k = 0).

theorem MIPRE.Tailored.Intro.CLData.register_correct_of_guard (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) {k : ℕ} (hk : k ≤ 7) (y : Fin Q → CL.𝔽₂) (hg : Guard V hs w k y) : (register U k).toFun (context V lam n Q w, CL.toBits y) = CL.indicatorBits (Introspection.CLChecks.prefixRegister (Introspection.AuxiliaryDecision.padded V hs w) k y)

The prefix register under the guard at its own level.

The stage linear map, as a matrix

noncomputable def MIPRE.Tailored.Intro.CLData.matrix (U : Cost.ClockedUniversalMachine) (k : ℕ) : Cost.PolyTimeFun Input (List Cost.BitStr)

The matrix of the stage-k linear map, as the rows vectorBits (M i) of M = LinearMap.toMatrix' (CLChecks.stageLinear (L w) k y).toLinearMap (matrixBits): the kernel's matrix query at the scanned prefix.

Equations

• MIPRE.Tailored.Intro.CLData.matrix U k = (MIPRE.Introspection.SourcePadding.Program.matrixFromContext U).comp (MIPRE.Tailored.Intro.CLData.stageContext U k)

theorem MIPRE.Tailored.Intro.CLData.matrix_correct (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) {k : ℕ} (hk : k < 7) (y : Fin Q → CL.𝔽₂) (hg : Guard V hs w k y) : (matrix U k).toFun (context V lam n Q w, CL.toBits y) = LowDegree.BinaryLinear.matrixBits (LinearMap.toMatrix' (Introspection.CLChecks.stageLinear (Introspection.AuxiliaryDecision.padded V hs w) k y).toLinearMap)

The stage matrix, k < 7, under the guard at k.

noncomputable def MIPRE.Tailored.Intro.CLData.kernelGenerators (U : Cost.ClockedUniversalMachine) (k : ℕ) : Cost.PolyTimeFun Input (List Cost.BitStr)

Generators of the kernel of the stage-k linear map (kernelGeneratorsProg on the register width and the stage matrix).

Equations

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

theorem MIPRE.Tailored.Intro.CLData.kernelGenerators_correct (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) {k : ℕ} (hk : k < 7) (y : Fin Q → CL.𝔽₂) (hg : Guard V hs w k y) : (kernelGenerators U k).toFun (context V lam n Q w, CL.toBits y) = LowDegree.BinaryLinear.kernelGeneratorsProg.toFun (Cost.unary Q, LowDegree.BinaryLinear.matrixBits (LinearMap.toMatrix' (Introspection.CLChecks.stageLinear (Introspection.AuxiliaryDecision.padded V hs w) k y).toLinearMap))

The prefix guard and source membership

noncomputable def MIPRE.Tailored.Intro.CLData.guard (U : Cost.ClockedUniversalMachine) (k : ℕ) : Cost.PolyTimeFun Input Bool

The prefix guard at level k: the success flag of the kernel's scan.

Equations

• MIPRE.Tailored.Intro.CLData.guard U k = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Tailored.Intro.CLData.scan U k)

theorem MIPRE.Tailored.Intro.CLData.guard_iff (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) {k : ℕ} (hk : k ≤ 7) (y : Fin Q → CL.𝔽₂) : (guard U k).toFun (context V lam n Q w, CL.toBits y) = true ↔ Guard V hs w k y

theorem MIPRE.Tailored.Intro.CLData.guard_correct (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) {k : ℕ} (hk : k ≤ 7) (y : Fin Q → CL.𝔽₂) : (guard U k).toFun (context V lam n Q w, CL.toBits y) = decide (∃ (x : Fin Q → CL.𝔽₂), (CL.CLFun.truncate k (Introspection.AuxiliaryDecision.padded V hs w)).eval x = (Introspection.AuxiliaryDecision.padded V hs w).outputPrefix k y)

The prefix guard at level k ≤ 7, exactly (PrefixGuard.holds at Hide k).

noncomputable def MIPRE.Tailored.Intro.CLData.inSource (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun Input Bool

Source membership of the register: its bits beyond the source dimension are zero.

Equations

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

theorem MIPRE.Tailored.Intro.CLData.inSource_correct (U : Cost.ClockedUniversalMachine) {lam n : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (Q : ℕ) (w : Bool) (y : Cost.BitStr) : (inSource U).toFun (context V lam n Q w, y) = decide (Introspection.SourceCompiler.InSource (V.sampler.dim (2 ^ n)) y)

Source membership SourceCompiler.InSource (V.sampler.dim (2^n)) y, exactly.