The input's question and answer split at an auxiliary answer

The introspection verifier's source decider is run on the input verifier W at index 2^n, on the questions toBits (pull (firstEmbedding hs) y) read off the y-registers of the two Introspect answers (AuxiliaryDecision.sourcePredicate); the honest strategy measures the input's strategy at the same question (SourcePadding.strategy, and the numbering of CanonicalGame cancels on the way back). A Read answer carries the input answer of the Introspect answer it is compared with, at the same register, and a Sample answer at the seed z that of the question L_w(z) (AuxiliaryChecks.sampling).

So at an auxiliary answer the input question is srcQuestion t y, and the tailored layout (MIPRE.Tailored.Intro.enc) splits the input's answer there by the lengths the input's answer-length calculator gives (srcSplitR, srcSplitL): computable from the readable register alone, as the linear-constraints processor needs.

noncomputable def MIPRE.Tailored.Intro.srcQuestion (W : Verifier 7) {n Q : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Q) : Introspection.AuxType 7 × Bool → Cost.BitStr → Cost.BitStr

The input question of an auxiliary answer, read off its register: the register's first dim bits at Introspect, Read and Hide, and those of L_w(z) at Sample.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Tailored.Intro.srcQuestion W hs x✝¹ x✝ = MIPRE.CL.toBits (MIPRE.CL.pull (MIPRE.Introspection.AuxiliaryProgram.firstEmbedding hs) (MIPRE.CL.ofBits Q x✝))

noncomputable def MIPRE.Tailored.Intro.srcSplitR (V : TailoredVerifier 7) (W : Verifier 7) {n Q : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Q) (t : Introspection.AuxType 7 × Bool) (y : Cost.BitStr) : ℕ

The number of readable bits of the input's answer at an auxiliary answer.

Equations

• MIPRE.Tailored.Intro.srcSplitR V W hs t y = V.lenOf (2 ^ n) (MIPRE.Tailored.Intro.srcQuestion W hs t y) false

noncomputable def MIPRE.Tailored.Intro.srcSplitL (V : TailoredVerifier 7) (W : Verifier 7) {n Q : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Q) (t : Introspection.AuxType 7 × Bool) (y : Cost.BitStr) : ℕ

The number of linear bits of the input's answer at an auxiliary answer.

Equations

• MIPRE.Tailored.Intro.srcSplitL V W hs t y = V.lenOf (2 ^ n) (MIPRE.Tailored.Intro.srcQuestion W hs t y) true