Finite original-answer payloads for the compiled introspection game

def MIPRE.Introspection.AuxiliaryAnswer.bounded (R : ℕ) (bs : Cost.BitStr) : Verifier.Answers R

A total decoder into the finite verifier alphabet. The format check makes the default branch irrelevant on every accepted pair or Read endpoint.

Equations

• MIPRE.Introspection.AuxiliaryAnswer.bounded R bs = if h : List.length bs ≤ R then ⟨bs, h⟩ else ⟨[], ⋯⟩

@[simp]

theorem MIPRE.Introspection.AuxiliaryAnswer.bounded_val {R : ℕ} (bs : Cost.BitStr) (h : List.length bs ≤ R) : ↑(bounded R bs) = bs

@[simp]

theorem MIPRE.Introspection.AuxiliaryAnswer.bounded_subtype (R : ℕ) (a : Verifier.Answers R) : bounded R ↑a = a

def MIPRE.Introspection.AuxiliaryAnswer.payloadBound {PA : Type u_2} {V : Type u_3} (R : ℕ) : ParsedAnswer V Cost.BitStr PA → Prop

The internal bound applies exactly to payloads carrying an original answer.

Equations

• MIPRE.Introspection.AuxiliaryAnswer.payloadBound R (MIPRE.Introspection.ParsedAnswer.pair y a) = (List.length a ≤ R)
• MIPRE.Introspection.AuxiliaryAnswer.payloadBound R (MIPRE.Introspection.ParsedAnswer.read y yp a) = (List.length a ≤ R)
• MIPRE.Introspection.AuxiliaryAnswer.payloadBound R x✝ = True

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

theorem MIPRE.Introspection.AuxiliaryAnswer.valid_aux_length {P : Type u_1} {Q ℓ : ℕ} (R : ℕ) (t : AuxType ℓ) (w : Bool) (bs : Cost.BitStr) (h : Valid Q R (Sum.inr (t, w)) bs) : Q ≤ List.length bs

Every accepted auxiliary payload already contains one full register.