The bits of the padded answer layout #
The ZPC strategy of the tailored introspection verifier has one observable per bit of the padded
re-encoding MIPRE.Tailored.Intro.enc of an answer. This file says what each bit is, as a
function of the parts of the answer (getD_enc_pair, getD_enc_read, getD_enc_hide): a bit
of the register y, of the dual register y' or of the X tail; a bit of the input's answer
α in its readable block (α_j when j is below the input's readable length, 0 above); or a
bit of its linear block (α_{s + j}, s the input's readable length). Padding is invisible to
List.getD _ _ false, so no hypothesis on α is needed.
theorem
MIPRE.Tailored.Intro.getD_enc_pair
{P : Type u_1}
{ℓ Q R : ℕ}
{splitR : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ}
{t : Introspection.AuxType ℓ × Bool}
(ht : t.1 = Introspection.AuxType.introspect ∨ t.1 = Introspection.AuxType.sample)
{y α : Cost.BitStr}
(hy : List.length y = Q)
(hs : splitR t y ≤ R)
(i : ℕ)
:
The bits of an Introspect or Sample answer.
theorem
MIPRE.Tailored.Intro.getD_enc_read
{P : Type u_1}
{ℓ Q R : ℕ}
{splitR : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ}
{w : Bool}
{y yp α : Cost.BitStr}
(hy : List.length y = Q)
(hyp : List.length yp = Q)
(hs : splitR (Introspection.AuxType.read, w) y ≤ R)
(i : ℕ)
:
List.getD (enc Q R splitR (Sum.inr (Introspection.AuxType.read, w)) (Introspection.AnswerParser.tripleBits y yp α)) i
false = if i < Q then List.getD y i false
else if i - Q < R then if i - Q < splitR (Introspection.AuxType.read, w) y then List.getD α (i - Q) false else false
else if i - Q - R < Q then List.getD yp (i - Q - R) false
else List.getD α (splitR (Introspection.AuxType.read, w) y + (i - Q - R - Q)) false
The bits of a Read answer.
theorem
MIPRE.Tailored.Intro.getD_enc_hide
{P : Type u_1}
{ℓ Q R : ℕ}
{splitR : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ}
{k : Fin ℓ}
{w : Bool}
{y yp x : Cost.BitStr}
(hy : List.length y = Q)
(hyp : List.length yp = Q)
(i : ℕ)
:
The bits of a Hide answer.