Dynamic source-question projection and internal answer cutoff

The input carries (n,Q,R,s,answerA,answerB) with all four numbers in binary. The guard validates the paper's tuple encoding, the separate original-answer cutoff, and membership of both register strings in the zero-padded source question space. Only then does it invoke the source on the first s bits.

@[reducible, inline]

abbrev MIPRE.Introspection.SourceCompiler.GuardInput : Type

Equations

• MIPRE.Introspection.SourceCompiler.GuardInput = (ℕ × ℕ × ℕ × ℕ × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

noncomputable def MIPRE.Introspection.SourceCompiler.inputIndex : Cost.PolyTimeFun GuardInput ℕ

Equations

• MIPRE.Introspection.SourceCompiler.inputIndex = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Introspection.SourceCompiler.inputQ : Cost.PolyTimeFun GuardInput ℕ

Equations

• MIPRE.Introspection.SourceCompiler.inputQ = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Introspection.SourceCompiler.inputR : Cost.PolyTimeFun GuardInput ℕ

Equations

• MIPRE.Introspection.SourceCompiler.inputR = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.Introspection.SourceCompiler.inputDim : Cost.PolyTimeFun GuardInput ℕ

Equations

• MIPRE.Introspection.SourceCompiler.inputDim = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Introspection.SourceCompiler.inputLeft : Cost.PolyTimeFun GuardInput Cost.BitStr

Equations

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

noncomputable def MIPRE.Introspection.SourceCompiler.inputRight : Cost.PolyTimeFun GuardInput Cost.BitStr

Equations

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

noncomputable def MIPRE.Introspection.SourceCompiler.leftParts : Cost.PolyTimeFun GuardInput (Cost.BitStr × Cost.BitStr)

Equations

• MIPRE.Introspection.SourceCompiler.leftParts = MIPRE.Introspection.DynamicParser.pairParts.comp (MIPRE.Introspection.SourceCompiler.inputLeft.pair MIPRE.Introspection.SourceCompiler.inputQ)

noncomputable def MIPRE.Introspection.SourceCompiler.rightParts : Cost.PolyTimeFun GuardInput (Cost.BitStr × Cost.BitStr)

Equations

• MIPRE.Introspection.SourceCompiler.rightParts = MIPRE.Introspection.DynamicParser.pairParts.comp (MIPRE.Introspection.SourceCompiler.inputRight.pair MIPRE.Introspection.SourceCompiler.inputQ)

def MIPRE.Introspection.SourceCompiler.InSource (s : ℕ) (y : Cost.BitStr) : Prop

Equations

• MIPRE.Introspection.SourceCompiler.InSource s y = (List.drop s y = List.replicate (List.length y - s) false)

@[instance_reducible]

instance MIPRE.Introspection.SourceCompiler.instDecidableInSource (s : ℕ) (y : Cost.BitStr) : Decidable (InSource s y)

Equations

• MIPRE.Introspection.SourceCompiler.instDecidableInSource s y = MIPRE.Introspection.SourceCompiler.instDecidableInSource._aux_1 s y

noncomputable def MIPRE.Introspection.SourceCompiler.sourceCheck : Cost.PolyTimeFun (Cost.BitStr × ℕ) Bool

Equations

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

theorem MIPRE.Introspection.SourceCompiler.sourceCheck_iff (y : Cost.BitStr) (s : ℕ) : sourceCheck.toFun (y, s) = true ↔ InSource s y

theorem MIPRE.Introspection.SourceCompiler.InSource_padding {s Q : ℕ} {y : Cost.BitStr} (hy : List.length y = Q) (h : InSource s y) : y = List.take s y ++ List.replicate (Q - s) false

noncomputable def MIPRE.Introspection.SourceCompiler.eight : Cost.PolyTimeFun ℕ ℕ

Equations

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

@[simp]

theorem MIPRE.Introspection.SourceCompiler.eight_apply (n : ℕ) : eight.toFun n = 8 * n

noncomputable def MIPRE.Introspection.SourceCompiler.guardAndCheck {α : Type u_1} [Cost.SizedEncoding α] (f g : Cost.PolyTimeFun α Bool) : Cost.PolyTimeFun α Bool

Equations

• MIPRE.Introspection.SourceCompiler.guardAndCheck f g = f.ite g (MIPRE.Cost.PolyTimeFun.const false)

theorem MIPRE.Introspection.SourceCompiler.guardAndCheck_iff {α : Type u_1} [Cost.SizedEncoding α] (f g : Cost.PolyTimeFun α Bool) (x : α) : (guardAndCheck f g).toFun x = true ↔ f.toFun x = true ∧ g.toFun x = true

def MIPRE.Introspection.SourceCompiler.GuardReady (x : GuardInput) : Prop

Equations

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

@[instance_reducible]

noncomputable instance MIPRE.Introspection.SourceCompiler.instDecidableGuardReady (x : GuardInput) : Decidable (GuardReady x)

Equations

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

noncomputable def MIPRE.Introspection.SourceCompiler.guardCheck : Cost.PolyTimeFun GuardInput Bool

Equations

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

theorem MIPRE.Introspection.SourceCompiler.guardCheck_iff (x : GuardInput) : guardCheck.toFun x = true ↔ GuardReady x

noncomputable def MIPRE.Introspection.SourceCompiler.projectedCall : Cost.PolyTimeFun GuardInput Cost.Data

Equations

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

theorem MIPRE.Introspection.SourceCompiler.projectedCall_apply (x : GuardInput) : projectedCall.toFun x = Cost.encode (inputIndex.toFun x, List.take (inputDim.toFun x) (leftParts.toFun x).1, List.take (inputDim.toFun x) (rightParts.toFun x).1, (leftParts.toFun x).2, (rightParts.toFun x).2)

theorem MIPRE.Introspection.SourceCompiler.GuardReady_cutoffs {x : GuardInput} (h : GuardReady x) : (List.take (inputDim.toFun x) (leftParts.toFun x).1).length ≤ inputR.toFun x ∧ (List.take (inputDim.toFun x) (rightParts.toFun x).1).length ≤ inputR.toFun x ∧ List.length (leftParts.toFun x).2 ≤ inputR.toFun x ∧ List.length (rightParts.toFun x).2 ≤ inputR.toFun x

All four original strings satisfy the internal original-game bound.

theorem MIPRE.Introspection.SourceCompiler.GuardReady_question_lengths {x : GuardInput} (h : GuardReady x) : (List.take (inputDim.toFun x) (leftParts.toFun x).1).length = inputDim.toFun x ∧ (List.take (inputDim.toFun x) (rightParts.toFun x).1).length = inputDim.toFun x

Projection produces questions of exactly the original sampler dimension.

theorem MIPRE.Introspection.SourceCompiler.GuardReady_padding {x : GuardInput} (h : GuardReady x) : (leftParts.toFun x).1 = List.take (inputDim.toFun x) (leftParts.toFun x).1 ++ List.replicate (inputQ.toFun x - inputDim.toFun x) false ∧ (rightParts.toFun x).1 = List.take (inputDim.toFun x) (rightParts.toFun x).1 ++ List.replicate (inputQ.toFun x - inputDim.toFun x) false

Both accepted register strings are the canonical zero-padded source questions.

noncomputable def MIPRE.Introspection.SourceCompiler.readInput : Cost.PolyTimeFun Cost.Data GuardInput

Equations

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

@[simp]

theorem MIPRE.Introspection.SourceCompiler.readInput_encode (x : GuardInput) : readInput.toFun (Cost.encode x) = x

def MIPRE.Introspection.SourceCompiler.RawReady (x : Cost.Data) : Prop

Equations

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

@[instance_reducible]

noncomputable instance MIPRE.Introspection.SourceCompiler.instDecidableRawReady (x : Cost.Data) : Decidable (RawReady x)

Equations

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

noncomputable def MIPRE.Introspection.SourceCompiler.projectedRoute : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Equations

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

theorem MIPRE.Introspection.SourceCompiler.projectedRoute_apply (x : Cost.Data) : projectedRoute.toFun x = if RawReady x then (true, (projectedCall.toFun (readInput.toFun x)).cons Cost.Data.nil) else (false, Cost.encode false)

noncomputable def MIPRE.Introspection.SourceCompiler.projectedProg (source : Cost.Prog) : Cost.Prog

Equations

• MIPRE.Introspection.SourceCompiler.projectedProg source = MIPRE.Cost.Prog.routeOneCall MIPRE.Introspection.SourceCompiler.projectedRoute source MIPRE.Cost.PolyTimeFun.snd

theorem MIPRE.Introspection.SourceCompiler.projectedProg_closed {source : Cost.Prog} (hs : Cost.Prog.WellScoped 1 source) : Cost.Prog.WellScoped 1 (projectedProg source)

theorem MIPRE.Introspection.SourceCompiler.projectedProg_reject (source : Cost.Prog) (x : Cost.Data) (h : ¬RawReady x) : ∃ (t : ℕ), (projectedProg source).Runs x (Cost.encode false) t

Rejection evaluates no source code, even if that code diverges.

theorem MIPRE.Introspection.SourceCompiler.projectedProg_call {source : Cost.Prog} (hs : Cost.Prog.WellScoped 1 source) (x r : Cost.Data) (t : ℕ) (h : RawReady x) (hr : source.Runs (projectedCall.toFun (readInput.toFun x)) r t) : ∃ (time : ℕ), (projectedProg source).Runs x r time

theorem MIPRE.Introspection.SourceCompiler.projectedProg_halts {source : Cost.Prog} (hs : Cost.Prog.WellScoped 1 source) (halts : ∀ (x : Cost.Data), Cost.Halts source x) (x : Cost.Data) : Cost.Halts (projectedProg source) x

theorem MIPRE.Introspection.SourceCompiler.projectedProg_accepts_iff {source : Cost.Prog} (hs : Cost.Prog.WellScoped 1 source) (halts : ∀ (x : Cost.Data), Cost.Halts source x) (x : Cost.Data) : (∃ (t : ℕ), (projectedProg source).Runs x (Cost.encode true) t) ↔ RawReady x ∧ ∃ (t : ℕ), source.Runs (projectedCall.toFun (readInput.toFun x)) (Cost.encode true) t