Exact raw-answer semantics of the executable Pauli predicate

theorem MIPRE.QLD.PauliBooleanProgram.program_formats (input : Input) (h : program.toFun input = true) : (PauliAnswerProgram.parser.toFun (input.2.1.1, input.1.2.2, input.1.1, Cost.unary 1, input.2.1.2.2)).1 = true ∧ (PauliAnswerProgram.parser.toFun (input.2.2.1, input.1.2.2, input.1.1, Cost.unary 1, input.2.2.2.2)).1 = true

Acceptance forces the exact answer format at both original endpoints, regardless of which orientation the arithmetic router uses.

theorem MIPRE.QLD.PauliBooleanProgram.program_raw_correct_valid (k : ℕ) (hk : 1 ≤ 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 : Cost.BitStr) (ha : (PauliAnswerProgram.parser.toFun (T, Cost.unary (2 ^ j), Cost.unary k, Cost.unary 1, a)).1 = true) (hb : (PauliAnswerProgram.parser.toFun (U, Cost.unary (2 ^ j), Cost.unary k, Cost.unary 1, b)).1 = true) : program.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), (T, PauliCL.fieldEncoding (SAT.shoupBinField k hk) x, a), U, PauliCL.fieldEncoding (SAT.shoupBinField k hk) y, 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) (PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) (2 ^ j) 1 T a) (PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) (2 ^ j) 1 U b)

theorem MIPRE.QLD.PauliBooleanProgram.program_raw_iff (k : ℕ) (hk : 1 ≤ 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 : Cost.BitStr) : program.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), (T, PauliCL.fieldEncoding (SAT.shoupBinField k hk) x, a), U, PauliCL.fieldEncoding (SAT.shoupBinField k hk) y, b) = true ↔ (PauliAnswerProgram.parser.toFun (T, Cost.unary (2 ^ j), Cost.unary k, Cost.unary 1, a)).1 = true ∧ (PauliAnswerProgram.parser.toFun (U, Cost.unary (2 ^ j), Cost.unary k, Cost.unary 1, b)).1 = true ∧ 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) (PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) (2 ^ j) 1 T a) (PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) (2 ^ j) 1 U b) = true

The whole raw predicate: exact parsing followed by the QLD predicate on the uniquely decoded semantic answers. Malformed payloads are rejected.