Documentation

MIPRE.Background.QLD.PauliBinaryInterface

Raw Pauli programs for the final introspection compiler #

source
noncomputable def MIPRE.QLD.PauliBinaryProgram.endpointValid :
Cost.PolyTimeFun (Introspection.PauliStageProgram.Parameters × Payload) Bool

Exact answer format at one raw typed endpoint.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.QLD.PauliBinaryProgram.endpointValid_apply (k j m : Cost.Unary) (T : Ty) (q a : Cost.BitStr) :
    endpointValid.toFun ((k, j, m), T, q, a) = (PauliAnswerProgram.parser.toFun (T, m, k, Cost.unary 1, a)).1
    source
    noncomputable def MIPRE.QLD.PauliBinaryProgram.fullAnswer :
    Cost.PolyTimeFun (Introspection.PauliStageProgram.Parameters × Cost.BitStr) (Bool × Cost.BitStr)

    Full X/Z outcomes use exactly the same parameters as the query compiler.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.QLD.PauliBinaryProgram.fullAnswer_apply (k j m : Cost.Unary) (a : Cost.BitStr) :
      fullAnswer.toFun ((k, j, m), a) = PauliFullAnswerProgram.program.toFun (m, k, a)
      source
      noncomputable def MIPRE.QLD.PauliBinaryProgram.questionOfBits (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (T : Ty) (q : Cost.BitStr) :
      Question (SAT.shoupBinField k hk).carrier (2 ^ j)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.QLD.PauliBinaryProgram.program_ofBits_iff (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (hj : j ≤ k) (hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier) (T U : Ty) (q r a b : Cost.BitStr) (hq : List.length q = (3 * 2 ^ j + 3) * k) (hr : List.length r = (3 * 2 ^ j + 3) * k) :
        program.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), (T, q, a), U, r, b) = true ↔ endpointValid.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), T, q, a) = true ∧ endpointValid.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), U, r, b) = true ∧ accepts hm (questionOfBits k hk hodd j T q) (questionOfBits k hk hodd j U r) (PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) (2 ^ j) 1 T a) (PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) (2 ^ j) 1 U b) = true

        On every full-length question payload, the actual raw program is exactly the QLD acceptance relation after the proved basis and answer decoders.

        source
        theorem MIPRE.QLD.PauliBinaryProgram.program_canonical (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (hj : j ≤ k) (hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier) (T U : Ty) (x y : PauliCL.Coord (2 ^ j) → (SAT.shoupBinField k hk).carrier) (a b : Answer (SAT.shoupBinField k hk).carrier (2 ^ j) 1) (ha : (PauliCL.ExplicitSeed.decode (PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) T x).fmtOk a = true) (hb : (PauliCL.ExplicitSeed.decode (PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) U y).fmtOk b = true) :
        program.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), (T, CL.toBits ((PauliCL.binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)) x), PauliAnswerProgram.answerBits (SAT.shoupBinField k hk) a), U, CL.toBits ((PauliCL.binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)) y), PauliAnswerProgram.answerBits (SAT.shoupBinField k hk) b) = accepts hm (PauliCL.ExplicitSeed.decode (PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) T x) (PauliCL.ExplicitSeed.decode (PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) U y) a b