Canonical raw input parsing for the introspection decision kernel

Only the fixed finite question labels are decoded by a lookup table. The source programs arrive as typed compiler metadata, never through a claimed polynomial-time decoder for arbitrary program syntax.

@[reducible, inline]

abbrev MIPRE.Introspection.DecisionKernel.Label : Type

Equations

• MIPRE.Introspection.DecisionKernel.Label = MIPRE.Introspection.QuestionType MIPRE.QLD.Ty 7

@[reducible, inline]

abbrev MIPRE.Introspection.DecisionKernel.Fields : Type

Equations

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

@[reducible, inline]

abbrev MIPRE.Introspection.DecisionKernel.Input : Type

Equations

• MIPRE.Introspection.DecisionKernel.Input = MIPRE.Introspection.DecisionPreparation.KernelInput

noncomputable def MIPRE.Introspection.DecisionKernel.labelKeys : List Cost.Data

Equations

• MIPRE.Introspection.DecisionKernel.labelKeys = (Finset.image MIPRE.Cost.encode Finset.univ).toList

noncomputable def MIPRE.Introspection.DecisionKernel.labelOption (d : Cost.Data) : Option Label

Equations

• MIPRE.Introspection.DecisionKernel.labelOption d = if d ∈ MIPRE.Introspection.DecisionKernel.labelKeys then MIPRE.Cost.decode d else none

theorem MIPRE.Introspection.DecisionKernel.table_not_mem (f : Cost.Data → Cost.Data) (xs : List Cost.Data) (d : Cost.Data) (h : d ∉ xs) : (Cost.PolyTimeFun.finiteTable f xs).toFun d = Cost.Data.nil

noncomputable def MIPRE.Introspection.DecisionKernel.labelDecoder : Cost.PolyTimeFun Cost.Data (Option Label)

Equations

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

noncomputable def MIPRE.Introspection.DecisionKernel.labelReader : Cost.PolyTimeFun Cost.Data Label

Equations

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

@[simp]

theorem MIPRE.Introspection.DecisionKernel.labelReader_encode (t : Label) : labelReader.toFun (Cost.encode t) = t

def MIPRE.Introspection.DecisionKernel.tailN : ℕ → Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.Introspection.DecisionKernel.tailN 0 = MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Data
• MIPRE.Introspection.DecisionKernel.tailN n.succ = MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Introspection.DecisionKernel.tailN n)

noncomputable def MIPRE.Introspection.DecisionKernel.indexField : Cost.PolyTimeFun Cost.Data ℕ

Equations

• MIPRE.Introspection.DecisionKernel.indexField = MIPRE.CL.Detyping.Program.readNat.comp MIPRE.Cost.PolyTimeFun.treeHead

noncomputable def MIPRE.Introspection.DecisionKernel.leftLabelField : Cost.PolyTimeFun Cost.Data Label

Equations

• MIPRE.Introspection.DecisionKernel.leftLabelField = MIPRE.Introspection.DecisionKernel.labelReader.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Introspection.DecisionKernel.tailN 1))

noncomputable def MIPRE.Introspection.DecisionKernel.leftQuestionField : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

• MIPRE.Introspection.DecisionKernel.leftQuestionField = MIPRE.CL.Detyping.Program.readBits.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Introspection.DecisionKernel.tailN 2))

noncomputable def MIPRE.Introspection.DecisionKernel.rightLabelField : Cost.PolyTimeFun Cost.Data Label

Equations

• MIPRE.Introspection.DecisionKernel.rightLabelField = MIPRE.Introspection.DecisionKernel.labelReader.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Introspection.DecisionKernel.tailN 3))

noncomputable def MIPRE.Introspection.DecisionKernel.rightQuestionField : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

• MIPRE.Introspection.DecisionKernel.rightQuestionField = MIPRE.CL.Detyping.Program.readBits.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Introspection.DecisionKernel.tailN 4))

noncomputable def MIPRE.Introspection.DecisionKernel.leftAnswerField : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

• MIPRE.Introspection.DecisionKernel.leftAnswerField = MIPRE.CL.Detyping.Program.readBits.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Introspection.DecisionKernel.tailN 5))

noncomputable def MIPRE.Introspection.DecisionKernel.rightAnswerField : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

• MIPRE.Introspection.DecisionKernel.rightAnswerField = MIPRE.CL.Detyping.Program.readBits.comp (MIPRE.Introspection.DecisionKernel.tailN 6)

noncomputable def MIPRE.Introspection.DecisionKernel.readFields : Cost.PolyTimeFun Cost.Data Fields

Equations

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

@[simp]

theorem MIPRE.Introspection.DecisionKernel.readFields_encode (n : ℕ) (T U : Label) (x y a b : Cost.BitStr) : readFields.toFun (Cost.encode (n, T, x, U, y, a, b)) = (n, T, x, U, y, a, b)

@[simp]

theorem MIPRE.Introspection.DecisionKernel.leftLabelField_encode (n : ℕ) (T U : Label) (x y a b : Cost.BitStr) : leftLabelField.toFun (Cost.encode (n, T, x, U, y, a, b)) = T

@[simp]

theorem MIPRE.Introspection.DecisionKernel.leftQuestionField_encode (n : ℕ) (T U : Label) (x y a b : Cost.BitStr) : leftQuestionField.toFun (Cost.encode (n, T, x, U, y, a, b)) = x

@[simp]

theorem MIPRE.Introspection.DecisionKernel.rightLabelField_encode (n : ℕ) (T U : Label) (x y a b : Cost.BitStr) : rightLabelField.toFun (Cost.encode (n, T, x, U, y, a, b)) = U

@[simp]

theorem MIPRE.Introspection.DecisionKernel.rightQuestionField_encode (n : ℕ) (T U : Label) (x y a b : Cost.BitStr) : rightQuestionField.toFun (Cost.encode (n, T, x, U, y, a, b)) = y

@[simp]

theorem MIPRE.Introspection.DecisionKernel.leftAnswerField_encode (n : ℕ) (T U : Label) (x y a b : Cost.BitStr) : leftAnswerField.toFun (Cost.encode (n, T, x, U, y, a, b)) = a

@[simp]

theorem MIPRE.Introspection.DecisionKernel.rightAnswerField_encode (n : ℕ) (T U : Label) (x y a b : Cost.BitStr) : rightAnswerField.toFun (Cost.encode (n, T, x, U, y, a, b)) = b

noncomputable def MIPRE.Introspection.DecisionKernel.raw : Cost.PolyTimeFun Input Cost.Data

Equations

• MIPRE.Introspection.DecisionKernel.raw = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Introspection.DecisionKernel.metadata : Cost.PolyTimeFun Input DecisionPreparation.Metadata

Equations

• MIPRE.Introspection.DecisionKernel.metadata = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Introspection.DecisionKernel.resourceTail : Cost.PolyTimeFun Input (Cost.Unary × ℕ × PauliSamplerParameters.Parameters × ℕ × ℕ)

Equations

• MIPRE.Introspection.DecisionKernel.resourceTail = MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Introspection.DecisionKernel.budget : Cost.PolyTimeFun Input Cost.Unary

Equations

• MIPRE.Introspection.DecisionKernel.budget = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Introspection.DecisionKernel.resourceTail

noncomputable def MIPRE.Introspection.DecisionKernel.sourceIndex : Cost.PolyTimeFun Input ℕ

Equations

• MIPRE.Introspection.DecisionKernel.sourceIndex = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Introspection.DecisionKernel.resourceTail)

noncomputable def MIPRE.Introspection.DecisionKernel.parameters : Cost.PolyTimeFun Input PauliSamplerParameters.Parameters

Equations

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

noncomputable def MIPRE.Introspection.DecisionKernel.registerWidth : Cost.PolyTimeFun Input ℕ

Equations

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

noncomputable def MIPRE.Introspection.DecisionKernel.originalCutoff : Cost.PolyTimeFun Input ℕ

Equations

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

noncomputable def MIPRE.Introspection.DecisionKernel.sourceSampler : Cost.PolyTimeFun Input Cost.Prog

Equations

• MIPRE.Introspection.DecisionKernel.sourceSampler = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Introspection.DecisionKernel.metadata)

noncomputable def MIPRE.Introspection.DecisionKernel.sourceDecider : Cost.PolyTimeFun Input Cost.Prog

Equations

• MIPRE.Introspection.DecisionKernel.sourceDecider = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Introspection.DecisionKernel.metadata)

noncomputable def MIPRE.Introspection.DecisionKernel.leftType : Cost.PolyTimeFun Input Label

Equations

• MIPRE.Introspection.DecisionKernel.leftType = MIPRE.Introspection.DecisionKernel.leftLabelField.comp MIPRE.Introspection.DecisionKernel.raw

noncomputable def MIPRE.Introspection.DecisionKernel.rightType : Cost.PolyTimeFun Input Label

Equations

• MIPRE.Introspection.DecisionKernel.rightType = MIPRE.Introspection.DecisionKernel.rightLabelField.comp MIPRE.Introspection.DecisionKernel.raw

noncomputable def MIPRE.Introspection.DecisionKernel.leftQuestion : Cost.PolyTimeFun Input Cost.BitStr

Equations

• MIPRE.Introspection.DecisionKernel.leftQuestion = MIPRE.Introspection.DecisionKernel.leftQuestionField.comp MIPRE.Introspection.DecisionKernel.raw

noncomputable def MIPRE.Introspection.DecisionKernel.rightQuestion : Cost.PolyTimeFun Input Cost.BitStr

Equations

• MIPRE.Introspection.DecisionKernel.rightQuestion = MIPRE.Introspection.DecisionKernel.rightQuestionField.comp MIPRE.Introspection.DecisionKernel.raw

noncomputable def MIPRE.Introspection.DecisionKernel.leftBits : Cost.PolyTimeFun Input Cost.BitStr

Equations

• MIPRE.Introspection.DecisionKernel.leftBits = MIPRE.Introspection.DecisionKernel.leftAnswerField.comp MIPRE.Introspection.DecisionKernel.raw

noncomputable def MIPRE.Introspection.DecisionKernel.rightBits : Cost.PolyTimeFun Input Cost.BitStr

Equations

• MIPRE.Introspection.DecisionKernel.rightBits = MIPRE.Introspection.DecisionKernel.rightAnswerField.comp MIPRE.Introspection.DecisionKernel.raw

noncomputable def MIPRE.Introspection.DecisionKernel.canonical : Cost.PolyTimeFun Input Bool

Equations

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

theorem MIPRE.Introspection.DecisionKernel.canonical_encode (M : DecisionPreparation.Metadata) (clock : Cost.Unary) (N Q R : ℕ) (p : PauliSamplerParameters.Parameters) (n : ℕ) (T U : Label) (x y a b : Cost.BitStr) : canonical.toFun (Cost.encode (n, T, x, U, y, a, b), M, clock, N, p, Q, R) = true