Exact re-encoding of arbitrary valid Pauli payloads

The parser's width and count checks make every retained row canonical. For the implemented Shoup field, decoding and re-encoding therefore recovers every accepted raw payload, not only payloads constructed from a semantic answer.

theorem MIPRE.QLD.PauliAnswerProgram.rows_getD {n : ℕ} (rows : List Cost.BitStr) (hn : rows.length = n) : (List.ofFn fun (i : Fin n) => rows.getD ↑i []) = rows

theorem MIPRE.QLD.PauliAnswerProgram.row_getD_mem {n : ℕ} (rows : List Cost.BitStr) (hn : rows.length = n) (i : Fin n) : rows.getD ↑i [] ∈ rows

theorem MIPRE.QLD.PauliAnswerProgram.fieldRows_roundtrip {k n : ℕ} (E : SAT.BinField k) (hE : ∀ (bs : Cost.BitStr), List.length bs = k → E.toBits (E.ofBits bs) = bs) (rows : List Cost.BitStr) (hn : rows.length = n) (hw : ∀ row ∈ rows, List.length row = k) : (E.vecBits fun (i : Fin n) => E.ofBits (rows.getD ↑i [])) = rows

theorem MIPRE.QLD.PauliAnswerProgram.bitRows_roundtrip {n : ℕ} (rows : List Cost.BitStr) (hn : rows.length = n) (hw : ∀ row ∈ rows, List.length row = 1) : (List.ofFn fun (i : Fin n) => [List.getD (rows.getD ↑i []) 0 false]) = rows

theorem MIPRE.QLD.PauliAnswerProgram.answerRows_decodeRows {k m d : ℕ} (E : SAT.BinField k) (hE : ∀ (bs : Cost.BitStr), List.length bs = k → E.toBits (E.ofBits bs) = bs) (T : Ty) (rows : List Cost.BitStr) (hn : rows.length = count T m d) (hw : ∀ row ∈ rows, List.length row = width T k) : answerRows E (decodeRows E m d T rows) = rows

Exact-width rows are recovered after semantic answer decoding.

theorem MIPRE.QLD.PauliAnswerProgram.parser_rows_spec (T : Ty) (m k d : ℕ) (bs : Cost.BitStr) (h : (parser.toFun (T, Cost.unary m, Cost.unary k, Cost.unary d, bs)).1 = true) : have rows := (parser.toFun (T, Cost.unary m, Cost.unary k, Cost.unary d, bs)).2; rows.length = count T m d ∧ (∀ row ∈ rows, List.length row = width T k) ∧ rows.flatten = bs

A successful parser returns the exact count, exact row widths and the original bits.

theorem MIPRE.QLD.PauliAnswerProgram.decodeBits_format {k m d : ℕ} (E : SAT.BinField k) (q : Question E.carrier m) (bs : Cost.BitStr) : q.fmtOk (decodeBits E m d q.ty bs) = true

Decoding an answer always has the constructor prescribed by its actual question.

theorem MIPRE.QLD.PauliAnswerProgram.answerBits_decodeBits (k : ℕ) (hk : 1 ≤ k) (m d : ℕ) (T : Ty) (bs : Cost.BitStr) (h : (parser.toFun (T, Cost.unary m, Cost.unary k, Cost.unary d, bs)).1 = true) : answerBits (SAT.shoupBinField k hk) (decodeBits (SAT.shoupBinField k hk) m d T bs) = bs

Every accepted raw payload for the implemented field re-encodes exactly.