Canonical auxiliary answer coding

Pauli payloads are left as bytes for the separate field-aware parser. The other three answer shapes use full-register binary vectors and the existing canonical tuple syntax. Valid raw tuples re-encode exactly, so same-type byte consistency is exactly consistency of parsed answers.

def MIPRE.Introspection.AuxiliaryAnswer.bits {Q : ℕ} : ParsedAnswer (Fin Q → CL.𝔽₂) Cost.BitStr Cost.BitStr → Cost.BitStr

Encode full register coordinates and preserve the original answer bytes.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.AuxiliaryAnswer.bits (MIPRE.Introspection.ParsedAnswer.pauli a) = a
• MIPRE.Introspection.AuxiliaryAnswer.bits (MIPRE.Introspection.ParsedAnswer.pair y a) = MIPRE.Introspection.AnswerParser.pairBits (MIPRE.CL.toBits y) a
• MIPRE.Introspection.AuxiliaryAnswer.bits (MIPRE.Introspection.ParsedAnswer.read y yp a) = MIPRE.Introspection.AnswerParser.tripleBits (MIPRE.CL.toBits y) (MIPRE.CL.toBits yp) a

def MIPRE.Introspection.AuxiliaryAnswer.decode {P : Type u_1} {ℓ : ℕ} (Q : ℕ) : QuestionType P ℓ → Cost.BitStr → ParsedAnswer (Fin Q → CL.𝔽₂) Cost.BitStr Cost.BitStr

Total type-directed decoding; the caller checks canonical format first.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.AuxiliaryAnswer.decode Q (Sum.inl val) x✝ = MIPRE.Introspection.ParsedAnswer.pauli x✝

theorem MIPRE.Introspection.AuxiliaryAnswer.decode_fits {P : Type u_1} {Q ℓ : ℕ} (t : QuestionType P ℓ) (bs : Cost.BitStr) : TypedPredicate.fits t (decode Q t bs) = true

Decoding chooses exactly the constructor required by the question.

theorem MIPRE.Introspection.AuxiliaryAnswer.decode_bits {P : Type u_1} {Q ℓ : ℕ} (t : QuestionType P ℓ) (a : ParsedAnswer (Fin Q → CL.𝔽₂) Cost.BitStr Cost.BitStr) (h : TypedPredicate.fits t a = true) : decode Q t (bits a) = a

Every correctly tagged parsed answer survives the byte round trip.

def MIPRE.Introspection.AuxiliaryAnswer.Valid {P : Type u_1} {ℓ : ℕ} (Q R : ℕ) : QuestionType P ℓ → Cost.BitStr → Prop

Canonical syntax and register lengths, with the separate original-answer cutoff.

Equations

• MIPRE.Introspection.AuxiliaryAnswer.Valid Q R (Sum.inl val) x✝ = True
• MIPRE.Introspection.AuxiliaryAnswer.Valid Q R (Sum.inr (MIPRE.Introspection.AuxType.introspect, snd)) x✝ = MIPRE.Introspection.AnswerParser.pairValid Q R x✝
• MIPRE.Introspection.AuxiliaryAnswer.Valid Q R (Sum.inr (MIPRE.Introspection.AuxType.sample, snd)) x✝ = MIPRE.Introspection.AnswerParser.pairValid Q R x✝
• MIPRE.Introspection.AuxiliaryAnswer.Valid Q R (Sum.inr (MIPRE.Introspection.AuxType.read, snd)) x✝ = MIPRE.Introspection.AnswerParser.tripleValid Q R false x✝
• MIPRE.Introspection.AuxiliaryAnswer.Valid Q R (Sum.inr (MIPRE.Introspection.AuxType.hide k, snd)) x✝ = MIPRE.Introspection.AnswerParser.tripleValid Q Q true x✝

theorem MIPRE.Introspection.AuxiliaryAnswer.bits_decode {P : Type u_1} {Q ℓ : ℕ} (R : ℕ) (t : QuestionType P ℓ) (bs : Cost.BitStr) (h : Valid Q R t bs) : bits (decode Q t bs) = bs

A parser-accepted auxiliary payload is the exact canonical encoding of its decoded answer, including the full third register of a Hide answer.

theorem MIPRE.Introspection.AuxiliaryAnswer.bits_eq_iff {P : Type u_1} {Q ℓ : ℕ} (t : QuestionType P ℓ) (a b : ParsedAnswer (Fin Q → CL.𝔽₂) Cost.BitStr Cost.BitStr) (ha : TypedPredicate.fits t a = true) (hb : TypedPredicate.fits t b = true) : bits a = bits b ↔ a = b

For a fixed type, byte equality and parsed equality coincide.