Documentation

MIPRE.Background.Introspection.DecisionCompilerRoute

Detyping the prepared decision kernel #

The graph router consumes the original untyped input and the already prepared dimension and answer cutoff. A genuine edge is checked by the typed kernel using those same resources. No second clock or parameter preparation occurs.

source
@[reducible, inline]
abbrev MIPRE.Introspection.DecisionCompiler.graph (t u : QuestionType QLD.Ty 7) :
Prop
Equations
Instances For
    source
    noncomputable def MIPRE.Introspection.DecisionCompiler.cutoffField :
    Cost.PolyTimeFun DecisionKernel.Input ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def MIPRE.Introspection.DecisionCompiler.routeContext :
      Cost.PolyTimeFun DecisionKernel.Input Cost.Data
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.Introspection.DecisionCompiler.routeContext_apply (z : DecisionKernel.Input) :
        routeContext.toFun z = CL.Detyping.DeciderProgram.context (DecisionKernel.raw.toFun z) (DecisionKernel.questionDimension.toFun z) (answerBound (DecisionKernel.registerWidth.toFun z) (DecisionKernel.originalCutoff.toFun z)) (answerBound (DecisionKernel.registerWidth.toFun z) (DecisionKernel.originalCutoff.toFun z))
        source
        noncomputable def MIPRE.Introspection.DecisionCompiler.router :
        Cost.PolyTimeFun DecisionKernel.Input (Bool × Cost.Data)
        Equations
        Instances For
          source
          def MIPRE.Introspection.DecisionCompiler.withRaw (z : DecisionKernel.Input) (x : Cost.Data) :
          DecisionKernel.Input
          Equations
          Instances For
            source
            noncomputable def MIPRE.Introspection.DecisionCompiler.routedInput :
            Cost.PolyTimeFun DecisionKernel.Input DecisionKernel.Input
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def MIPRE.Introspection.DecisionCompiler.untypedKernel (U : Cost.ClockedUniversalMachine) :
              Cost.PolyTimeFun DecisionKernel.Input Bool
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem MIPRE.Introspection.DecisionCompiler.untypedKernel_apply (U : Cost.ClockedUniversalMachine) (z : DecisionKernel.Input) :
                (untypedKernel U).toFun z = if (router.toFun z).1 = true then (DecisionKernel.program U).toFun (withRaw z (Cost.PolyTimeFun.treeHead.toFun (router.toFun z).2)) else decide ((router.toFun z).2 = Cost.encode true)
                source
                theorem MIPRE.Introspection.DecisionCompiler.router_context (n : ℕ) (x y a b : Cost.BitStr) (M : DecisionPreparation.Metadata) (clock : Cost.Unary) (N Q R : ℕ) (p : PauliSamplerParameters.Parameters) :
                router.toFun (Cost.encode (n, x, y, a, b), M, clock, N, p, Q, R) = if List.length x = CL.Detyping.graphDim DecisionKernel.Label + (3 * List.length p.2.2 + 3) * List.length p.1 ∧ List.length y = CL.Detyping.graphDim DecisionKernel.Label + (3 * List.length p.2.2 + 3) * List.length p.1 ∧ List.length a ≤ answerBound Q R ∧ List.length b ≤ answerBound Q R then match CL.Detyping.DeciderProgram.selectedEdge graph (CL.Detyping.graphOfBits x) (CL.Detyping.graphOfBits y) with | none => (false, Cost.encode true) | some uv => (true, (Cost.encode (n, uv.1, List.drop (CL.Detyping.graphDim DecisionKernel.Label) x, uv.2, List.drop (CL.Detyping.graphDim DecisionKernel.Label) y, a, b)).cons Cost.Data.nil) else (false, Cost.encode false)
                source
                theorem MIPRE.Introspection.DecisionCompiler.untypedKernel_iff (U : Cost.ClockedUniversalMachine) (n : ℕ) (x y a b : Cost.BitStr) (M : DecisionPreparation.Metadata) (clock : Cost.Unary) (N Q R : ℕ) (p : PauliSamplerParameters.Parameters) :
                (untypedKernel U).toFun (Cost.encode (n, x, y, a, b), M, clock, N, p, Q, R) = true ↔ List.length x = CL.Detyping.graphDim DecisionKernel.Label + (3 * List.length p.2.2 + 3) * List.length p.1 ∧ List.length y = CL.Detyping.graphDim DecisionKernel.Label + (3 * List.length p.2.2 + 3) * List.length p.1 ∧ List.length a ≤ answerBound Q R ∧ List.length b ≤ answerBound Q R ∧ match CL.Detyping.DeciderProgram.selectedEdge graph (CL.Detyping.graphOfBits x) (CL.Detyping.graphOfBits y) with | none => True | some uv => (DecisionKernel.program U).toFun (Cost.encode (n, uv.1, List.drop (CL.Detyping.graphDim DecisionKernel.Label) x, uv.2, List.drop (CL.Detyping.graphDim DecisionKernel.Label) y, a, b), M, clock, N, p, Q, R) = true

                Canonical untyped inputs use exactly the graph router's edge convention, with the global answer cutoff enforced also on nonedge views.