Reject malformed introspection answers before a source call

The input is encode (n, answerA, answerB). On two valid Introspect answers the source receives encode (n, yA, yB, aA, aB). The supplied index is retained, so this wrapper can precede the exponential-index clock adapter. This module does not implement the register projection from Q coordinates to a source question space, or the other auxiliary edge tests.

noncomputable def MIPRE.Introspection.AnswerParser.guardIndex : Cost.PolyTimeFun Cost.Data ℕ

Equations

• MIPRE.Introspection.AnswerParser.guardIndex = MIPRE.CL.Detyping.Program.readNat.comp MIPRE.Cost.PolyTimeFun.treeHead

noncomputable def MIPRE.Introspection.AnswerParser.guardLeft : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

• MIPRE.Introspection.AnswerParser.guardLeft = MIPRE.CL.Detyping.Program.readBits.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Cost.PolyTimeFun.treeTail)

noncomputable def MIPRE.Introspection.AnswerParser.guardRight : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

• MIPRE.Introspection.AnswerParser.guardRight = MIPRE.CL.Detyping.Program.readBits.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeTail)

noncomputable def MIPRE.Introspection.AnswerParser.callArgument (Q : ℕ) (x : Cost.Data) : Cost.Data

Equations

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

noncomputable def MIPRE.Introspection.AnswerParser.callArgumentProg (Q : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

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

@[simp]

theorem MIPRE.Introspection.AnswerParser.callArgumentProg_apply (Q : ℕ) (x : Cost.Data) : (callArgumentProg Q).toFun x = callArgument Q x

def MIPRE.Introspection.AnswerParser.callReady (Q R : ℕ) (x : Cost.Data) : Prop

Equations

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

@[instance_reducible]

noncomputable instance MIPRE.Introspection.AnswerParser.instDecidableCallReady (Q R : ℕ) (x : Cost.Data) : Decidable (callReady Q R x)

Equations

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

noncomputable def MIPRE.Introspection.AnswerParser.guardedRoute (Q R : ℕ) : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Equations

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

theorem MIPRE.Introspection.AnswerParser.nestedIf {α : Type u_1} (p q : Prop) [Decidable p] [Decidable q] (a b : α) : (if p then if q then a else b else b) = if p ∧ q then a else b

theorem MIPRE.Introspection.AnswerParser.guardedRoute_apply (Q R : ℕ) (x : Cost.Data) : (guardedRoute Q R).toFun x = if callReady Q R x then (true, (callArgument Q x).cons Cost.Data.nil) else (false, Cost.encode false)

@[simp]

theorem MIPRE.Introspection.AnswerParser.guardIndex_cons (n : ℕ) (d : Cost.Data) : guardIndex.toFun ((Cost.encode n).cons d) = n

theorem MIPRE.Introspection.AnswerParser.guardedRoute_preserves (Q R n : ℕ) (d a : Cost.Data) (h : (guardedRoute Q R).toFun ((Cost.encode n).cons d) = (true, a)) : ∃ (q : Cost.Data) (ctx : Cost.Data), a = ((Cost.encode n).cons q).cons ctx

noncomputable def MIPRE.Introspection.AnswerParser.guardedProg (Q R : ℕ) (source : Cost.Prog) : Cost.Prog

Actual program: invalid tuples return false before the source program is evaluated.

Equations

• MIPRE.Introspection.AnswerParser.guardedProg Q R source = MIPRE.Cost.Prog.routeOneCall (MIPRE.Introspection.AnswerParser.guardedRoute Q R) source MIPRE.Cost.PolyTimeFun.snd

theorem MIPRE.Introspection.AnswerParser.guardedProg_closed (Q R : ℕ) {source : Cost.Prog} (hs : Cost.Prog.WellScoped 1 source) : Cost.Prog.WellScoped 1 (guardedProg Q R source)

theorem MIPRE.Introspection.AnswerParser.guardedProg_reject (Q R : ℕ) (source : Cost.Prog) (x : Cost.Data) (h : ¬callReady Q R x) : ∃ (t : ℕ), (guardedProg Q R source).Runs x (Cost.encode false) t

Rejection needs no halting assumption about the source.

theorem MIPRE.Introspection.AnswerParser.guardedProg_call (Q R : ℕ) {source : Cost.Prog} (hs : Cost.Prog.WellScoped 1 source) (x r : Cost.Data) (t : ℕ) (h : callReady Q R x) (hr : source.Runs (callArgument Q x) r t) : ∃ (time : ℕ), (guardedProg Q R source).Runs x r time

theorem MIPRE.Introspection.AnswerParser.guardedProg_halts (Q R n : ℕ) {source : Cost.Prog} (hs : Cost.Prog.WellScoped 1 source) (halts : ∀ (d : Cost.Data), Cost.Halts source ((Cost.encode n).cons d)) (d : Cost.Data) : Cost.Halts (guardedProg Q R source) ((Cost.encode n).cons d)

theorem MIPRE.Introspection.AnswerParser.guardedProg_haltsWithin (Q R n B k : ℕ) {source : Cost.Prog} (hs : Cost.Prog.WellScoped 1 source) (bound : ∀ (d : Cost.Data), Cost.HaltsWithin source ((Cost.encode n).cons d) (B * (d.size + 1) ^ k)) (d : Cost.Data) : Cost.HaltsWithin (guardedProg Q R source) ((Cost.encode n).cons d) (Polynomial.eval ((Cost.encode n).cons d).size (Cost.Prog.routeCost (guardedRoute Q R) Cost.PolyTimeFun.snd B k))

Full ambient input-size polynomial transfer for the guarded source call.

theorem MIPRE.Introspection.AnswerParser.callReady_input (Q R n : ℕ) (a b : Cost.BitStr) : callReady Q R (Cost.encode (n, a, b)) ↔ pairValid Q R a ∧ pairValid Q R b

theorem MIPRE.Introspection.AnswerParser.callArgument_input (Q n : ℕ) (a b : Cost.BitStr) : callArgument Q (Cost.encode (n, a, b)) = Cost.encode (n, (pairParts Q a).1, (pairParts Q b).1, (pairParts Q a).2, (pairParts Q b).2)

theorem MIPRE.Introspection.AnswerParser.callReady_fields (Q R n : ℕ) (a b : Cost.BitStr) (h : callReady Q R (Cost.encode (n, a, b))) : List.length (pairParts Q a).1 = Q ∧ List.length (pairParts Q b).1 = Q ∧ List.length (pairParts Q a).2 ≤ R ∧ List.length (pairParts Q b).2 ≤ R

Every call has both full register lengths and the separate original-answer cutoffs.

theorem MIPRE.Introspection.AnswerParser.guardedProg_accepts_iff (Q R n : ℕ) (source : Decider) (halts : ∀ (d : Cost.Data), Cost.Halts source.prog ((Cost.encode n).cons d)) (a b : Cost.BitStr) : (∃ (t : ℕ), (guardedProg Q R source.prog).Runs (Cost.encode (n, a, b)) (Cost.encode true) t) ↔ pairValid Q R a ∧ pairValid Q R b ∧ source.Accepts n (pairParts Q a).1 (pairParts Q b).1 (pairParts Q a).2 (pairParts Q b).2

On total sources, guarded acceptance is exactly valid parsing followed by source acceptance.