Executable local prefix guards

The question type selects one of the seven fixed scan depths. The full register width, source program, clock and raw answer remain runtime data. The caller's format check validates the tuple; here its first field is scanned.

@[reducible, inline]

abbrev MIPRE.Introspection.AuxiliaryPrefixGuard.Input (P : Type u_2) : Type u_2

Equations

• MIPRE.Introspection.AuxiliaryPrefixGuard.Input P = (MIPRE.Introspection.AuxiliarySource.Context × ℕ × MIPRE.Introspection.QuestionType P 7 × MIPRE.Cost.BitStr)

noncomputable def MIPRE.Introspection.AuxiliaryPrefixGuard.context {P : Type u_1} [Cost.SizedEncoding P] : Cost.PolyTimeFun (Input P) AuxiliarySource.Context

Equations

• MIPRE.Introspection.AuxiliaryPrefixGuard.context = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Introspection.AuxiliaryPrefixGuard.width {P : Type u_1} [Cost.SizedEncoding P] : Cost.PolyTimeFun (Input P) ℕ

Equations

• MIPRE.Introspection.AuxiliaryPrefixGuard.width = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Introspection.AuxiliaryPrefixGuard.label {P : Type u_1} [Cost.SizedEncoding P] : Cost.PolyTimeFun (Input P) (QuestionType P 7)

Equations

• MIPRE.Introspection.AuxiliaryPrefixGuard.label = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.Introspection.AuxiliaryPrefixGuard.answer {P : Type u_1} [Cost.SizedEncoding P] : Cost.PolyTimeFun (Input P) Cost.BitStr

Equations

• MIPRE.Introspection.AuxiliaryPrefixGuard.answer = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.Introspection.AuxiliaryPrefixGuard.claim {P : Type u_1} [Cost.SizedEncoding P] : Cost.PolyTimeFun (Input P) Cost.BitStr

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryPrefixGuard.contextFor {P : Type u_1} [Cost.SizedEncoding P] (w : Bool) : Cost.PolyTimeFun (Input P) AuxiliarySource.Context

The endpoint's role selects the source CL function.

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryPrefixGuard.scan {P : Type u_1} [Cost.SizedEncoding P] (U : Cost.ClockedUniversalMachine) (w : Bool) (k : ℕ) : Cost.PolyTimeFun (Input P) Bool

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryPrefixGuard.branch {P : Type u_1} [Cost.SizedEncoding P] (U : Cost.ClockedUniversalMachine) : QuestionType P 7 → Cost.PolyTimeFun (Input P) Bool

Equations

• MIPRE.Introspection.AuxiliaryPrefixGuard.branch U (Sum.inr (MIPRE.Introspection.AuxType.hide k, w)) = MIPRE.Introspection.AuxiliaryPrefixGuard.scan U w ↑k
• MIPRE.Introspection.AuxiliaryPrefixGuard.branch U (Sum.inr (MIPRE.Introspection.AuxType.read, w)) = MIPRE.Introspection.AuxiliaryPrefixGuard.scan U w 6
• MIPRE.Introspection.AuxiliaryPrefixGuard.branch U x✝ = MIPRE.Cost.PolyTimeFun.const true

noncomputable def MIPRE.Introspection.AuxiliaryPrefixGuard.program {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun (Input P) Bool

A uniform polynomial-time program; finite enumeration chooses control only.

Equations

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

@[simp]

theorem MIPRE.Introspection.AuxiliaryPrefixGuard.program_apply {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] (U : Cost.ClockedUniversalMachine) (x : Input P) : (program U).toFun x = (branch U (label.toFun x)).toFun x

@[simp]

theorem MIPRE.Introspection.AuxiliaryPrefixGuard.program_pauli {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] (U : Cost.ClockedUniversalMachine) (ctx : AuxiliarySource.Context) (Q : ℕ) (p : P) (bs : Cost.BitStr) : (program U).toFun (ctx, Q, Sum.inl p, bs) = true

@[simp]

theorem MIPRE.Introspection.AuxiliaryPrefixGuard.program_introspect {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] (U : Cost.ClockedUniversalMachine) (ctx : AuxiliarySource.Context) (Q : ℕ) (w : Bool) (bs : Cost.BitStr) : (program U).toFun (ctx, Q, Sum.inr (AuxType.introspect, w), bs) = true

@[simp]

theorem MIPRE.Introspection.AuxiliaryPrefixGuard.program_sample {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] (U : Cost.ClockedUniversalMachine) (ctx : AuxiliarySource.Context) (Q : ℕ) (w : Bool) (bs : Cost.BitStr) : (program U).toFun (ctx, Q, Sum.inr (AuxType.sample, w), bs) = true

theorem MIPRE.Introspection.AuxiliaryPrefixGuard.contextFor_queryContext {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] (V : Verifier 7) (lam n : ℕ) (v w : Bool) (initialLevel : ℕ) {Q : ℕ} (initial : Fin Q → CL.𝔽₂) (t : QuestionType P 7) (bs : Cost.BitStr) : (contextFor w).toFun (SourcePadding.Program.queryContext V lam n v initialLevel initial, Q, t, bs) = SourcePadding.Program.queryContext V lam n w initialLevel initial

theorem MIPRE.Introspection.AuxiliaryPrefixGuard.scan_correct {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hQ : V.sampler.dim (2 ^ n) ≤ Q) (v w : Bool) (initialLevel : ℕ) (initial y yp : Fin Q → CL.𝔽₂) (last : Cost.BitStr) (t : QuestionType P 7) (k : ℕ) (hk : k ≤ 7) : (scan U w k).toFun (SourcePadding.Program.queryContext V lam n v initialLevel initial, Q, t, AnswerParser.tripleBits (CL.toBits y) (CL.toBits yp) last) = true ↔ ∃ (x : Fin Q → CL.𝔽₂), (CL.CLFun.truncate k (SourcePadding.depthFamily (AuxiliaryProgram.firstEmbedding hQ) (SourcePadding.Program.sourceFamily V n) w)).eval x = (SourcePadding.depthFamily (AuxiliaryProgram.firstEmbedding hQ) (SourcePadding.Program.sourceFamily V n) w).outputPrefix k y

The scan flag is exactly prefix attainability for the actual bounded, same-depth padded source. No query correctness assumption remains.

theorem MIPRE.Introspection.AuxiliaryPrefixGuard.program_hide {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {PA : Type u_2} (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hQ : V.sampler.dim (2 ^ n) ≤ Q) (v w : Bool) (initialLevel : ℕ) (initial y yp z : Fin Q → CL.𝔽₂) (k : Fin 7) : (program U).toFun (SourcePadding.Program.queryContext V lam n v initialLevel initial, Q, Sum.inr (AuxType.hide k, w), AnswerParser.tripleBits (CL.toBits y) (CL.toBits yp) (CL.toBits z)) = true ↔ PrefixGuard.holds (SourcePadding.depthFamily (AuxiliaryProgram.firstEmbedding hQ) (SourcePadding.Program.sourceFamily V n)) (Sum.inr (AuxType.hide k, w)) (ParsedAnswer.hide y yp z)

Exact Hide guard on the canonical full-register answer encoding.

theorem MIPRE.Introspection.AuxiliaryPrefixGuard.program_read {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {PA : Type u_2} (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hQ : V.sampler.dim (2 ^ n) ≤ Q) (v w : Bool) (initialLevel : ℕ) (initial y yp : Fin Q → CL.𝔽₂) (a : Cost.BitStr) : (program U).toFun (SourcePadding.Program.queryContext V lam n v initialLevel initial, Q, Sum.inr (AuxType.read, w), AnswerParser.tripleBits (CL.toBits y) (CL.toBits yp) a) = true ↔ PrefixGuard.holds (SourcePadding.depthFamily (AuxiliaryProgram.firstEmbedding hQ) (SourcePadding.Program.sourceFamily V n)) (Sum.inr (AuxType.read, w)) (ParsedAnswer.read y yp a)

Exact Read guard; only its first six source stages are required.