Exact, bounded parsing of field-valued answer tables

The number of field elements is supplied in binary and the field width in unary. Before allocating any list of blocks, the count is capped by the actual answer length. The parser checks every width and exact re-encoding, including the absence of trailing bits. Its polynomial bound therefore holds even when a malformed short answer claims an exponentially large number of elements.

This supplies the payload parser for point, polynomial and full Pauli answers. Question-type dispatch and the interpretation of field rows are separate.

theorem MIPRE.Introspection.FieldAnswerParser.length_flatten_of_width (rows : List Cost.BitStr) (k : ℕ) (hw : ∀ row ∈ rows, List.length row = k) : rows.flatten.length = rows.length * k

theorem MIPRE.Introspection.FieldAnswerParser.splitBlocks_exact (n k : ℕ) (bs : Cost.BitStr) (hlen : List.length bs = n * k) : (BinaryBlock.splitBlocks n k bs).flatten = bs ∧ ∀ row ∈ BinaryBlock.splitBlocks n k bs, List.length row = k

noncomputable def MIPRE.Introspection.FieldAnswerParser.rowsProg : Cost.PolyTimeFun (ℕ × Cost.Unary × Cost.BitStr) (List Cost.BitStr)

Candidate rows, with the binary count capped before the unary scan.

Equations

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

@[simp]

theorem MIPRE.Introspection.FieldAnswerParser.rowsProg_apply (n : ℕ) (k : Cost.Unary) (bs : Cost.BitStr) : rowsProg.toFun (n, k, bs) = BinaryBlock.splitBlocks (min n (List.length bs)) (List.length k) bs

noncomputable def MIPRE.Introspection.FieldAnswerParser.readyProg : Cost.PolyTimeFun (ℕ × Cost.Unary × Cost.BitStr) Bool

Validate the count, every block width, and the exact original bit string.

Equations

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

theorem MIPRE.Introspection.FieldAnswerParser.readyProg_spec (n : ℕ) (k : Cost.Unary) (bs : Cost.BitStr) : readyProg.toFun (n, k, bs) = true ↔ 0 < List.length k ∧ (rowsProg.toFun (n, k, bs)).length = n ∧ (∀ row ∈ rowsProg.toFun (n, k, bs), List.length row = List.length k) ∧ (rowsProg.toFun (n, k, bs)).flatten = bs

theorem MIPRE.Introspection.FieldAnswerParser.readyProg_iff_length (n : ℕ) (k : Cost.Unary) (bs : Cost.BitStr) : readyProg.toFun (n, k, bs) = true ↔ 0 < List.length k ∧ List.length bs = n * List.length k

noncomputable def MIPRE.Introspection.FieldAnswerParser.parserProg : Cost.PolyTimeFun (ℕ × Cost.Unary × Cost.BitStr) (Bool × List Cost.BitStr)

The flag must be checked before interpreting the candidate rows.

Equations

• MIPRE.Introspection.FieldAnswerParser.parserProg = MIPRE.Introspection.FieldAnswerParser.readyProg.pair MIPRE.Introspection.FieldAnswerParser.rowsProg

theorem MIPRE.Introspection.FieldAnswerParser.parserProg_flatten (rows : List Cost.BitStr) (k : ℕ) (hk : 0 < k) (hw : ∀ row ∈ rows, List.length row = k) : parserProg.toFun (rows.length, Cost.unary k, rows.flatten) = (true, rows)

theorem MIPRE.Introspection.FieldAnswerParser.parserProg_vecBits {n k : ℕ} (E : SAT.BinField k) (hk : 0 < k) (v : Fin n → E.carrier) : parserProg.toFun (n, Cost.unary k, (E.vecBits v).flatten) = (true, E.vecBits v)

Canonically encoded field vectors are returned exactly, without padding or loss.

theorem MIPRE.Introspection.FieldAnswerParser.fold_double (u : Cost.Unary) (a : ℕ) : List.foldl (fun (n : ℕ) (x : Unit) => Nat.bit false n) a u = a * 2 ^ List.length u

noncomputable def MIPRE.Introspection.FieldAnswerParser.scalePowerOfTwoProg : Cost.PolyTimeFun (ℕ × Cost.Unary) ℕ

Binary shifting computes an exponentially large count without unary allocation.

Equations

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

@[simp]

theorem MIPRE.Introspection.FieldAnswerParser.scalePowerOfTwoProg_apply (a : ℕ) (u : Cost.Unary) : scalePowerOfTwoProg.toFun (a, u) = a * 2 ^ List.length u

noncomputable def MIPRE.Introspection.FieldAnswerParser.fullPauliParserProg : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × Cost.BitStr) (Bool × List Cost.BitStr)

Full Pauli payloads: dimension, field width, and raw answer bits.

Equations

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

theorem MIPRE.Introspection.FieldAnswerParser.fullPauliParserProg_vecBits {m k : ℕ} (E : SAT.BinField k) (hk : 0 < k) (v : Fin (2 ^ m) → E.carrier) : fullPauliParserProg.toFun (Cost.unary m, Cost.unary k, (E.vecBits v).flatten) = (true, E.vecBits v)