Documentation

MIPRE.Tailored.Intro.Layout

The padded answer layout of the tailored introspection verifier #

The introspection verifier's answers are byte strings of variable length: an auxiliary answer is a tuple of self-delimiting fields (AnswerParser.pairBits, tripleBits), the last of which may be the input's answer, of any length up to the original cutoff R. A tailored game has, at each question, a fixed number of readable and of linear answer bits. This file fixes the re-encoding, by the question's label (QuestionType P ℓ):

a Pauli label p keeps its bytes, plen p of them, all readable when pread p (the Z-basis answers) and all linear otherwise;
Introspect and Sample, (y, α): readable y and the input's readable answer bits padded to R, linear the input's linear answer bits padded to R;
Read, (y, y', α): readable y and the padded readable bits of α, linear y' and the padded linear bits of α;
Hide, (y, y', x): readable y, linear y' and x.

The input's answer at the question read off y has splitR t y readable and splitL t y linear bits, the two functions being parameters here; the instance runs the input's answer-length calculator. enc re-encodes, dec decodes, and dec_enc is the round trip on well-formed answers whose input answer has the input's lengths; length_enc says that enc has the label's lengths.

def MIPRE.Tailored.Intro.pad (R : ℕ) (l : Cost.BitStr) :

Pad with zeros to length R.

Equations

MIPRE.Tailored.Intro.pad R l = l ++ List.replicate (R - List.length l) false

Instances For

@[simp]

theorem MIPRE.Tailored.Intro.length_pad {R : ℕ} {l : Cost.BitStr} (h : List.length l ≤ R) :

List.length (pad R l) = R

theorem MIPRE.Tailored.Intro.take_pad {R : ℕ} (l : Cost.BitStr) :

List.take (List.length l) (pad R l) = l

def MIPRE.Tailored.Intro.lenR {P : Type u_1} {ℓ : ℕ} (Q R : ℕ) (plen : P → ℕ) (pread : P → Bool) :

Introspection.QuestionType P ℓ → ℕ

The number of readable answer bits of a label.

Equations

MIPRE.Tailored.Intro.lenR Q R plen pread (Sum.inl p) = if pread p = true then plen p else 0
MIPRE.Tailored.Intro.lenR Q R plen pread (Sum.inr (MIPRE.Introspection.AuxType.introspect , snd)) = Q + R
MIPRE.Tailored.Intro.lenR Q R plen pread (Sum.inr (MIPRE.Introspection.AuxType.sample , snd)) = Q + R
MIPRE.Tailored.Intro.lenR Q R plen pread (Sum.inr (MIPRE.Introspection.AuxType.read , snd)) = Q + R
MIPRE.Tailored.Intro.lenR Q R plen pread (Sum.inr (MIPRE.Introspection.AuxType.hide k, snd)) = Q

Instances For

def MIPRE.Tailored.Intro.lenL {P : Type u_1} {ℓ : ℕ} (Q R : ℕ) (plen : P → ℕ) (pread : P → Bool) :

Introspection.QuestionType P ℓ → ℕ

The number of linear answer bits of a label.

Equations

MIPRE.Tailored.Intro.lenL Q R plen pread (Sum.inl p) = if pread p = true then 0 else plen p
MIPRE.Tailored.Intro.lenL Q R plen pread (Sum.inr (MIPRE.Introspection.AuxType.introspect , snd)) = R
MIPRE.Tailored.Intro.lenL Q R plen pread (Sum.inr (MIPRE.Introspection.AuxType.sample , snd)) = R
MIPRE.Tailored.Intro.lenL Q R plen pread (Sum.inr (MIPRE.Introspection.AuxType.read , snd)) = Q + R
MIPRE.Tailored.Intro.lenL Q R plen pread (Sum.inr (MIPRE.Introspection.AuxType.hide k, snd)) = 2 * Q

Instances For

def MIPRE.Tailored.Intro.enc {P : Type u_1} {ℓ : ℕ} (Q R : ℕ) (splitR : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ) :

Introspection.QuestionType P ℓ → Cost.BitStr → Cost.BitStr

The re-encoding of a byte answer, readable bits first.

Equations

One or more equations did not get rendered due to their size.
MIPRE.Tailored.Intro.enc Q R splitR (Sum.inl val) x✝ = x✝

Instances For

def MIPRE.Tailored.Intro.unpad {ℓ : ℕ} (R : ℕ) (splitR splitL : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ) (t : Introspection.AuxType ℓ × Bool) (y rb lb : Cost.BitStr) :

The input's answer, from its two padded blocks.

Equations

MIPRE.Tailored.Intro.unpad R splitR splitL t y rb lb = List.take (splitR t y) (List.take R rb) ++ List.take (splitL t y) (List.take R lb)

Instances For

def MIPRE.Tailored.Intro.dec {P : Type u_1} {ℓ : ℕ} (Q R : ℕ) (splitR splitL : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ) :

Introspection.QuestionType P ℓ → Cost.BitStr → Cost.BitStr

The decoding of a re-encoded answer.

Equations

One or more equations did not get rendered due to their size.
MIPRE.Tailored.Intro.dec Q R splitR splitL (Sum.inl val) x✝ = x✝

Instances For

The round trip #

def MIPRE.Tailored.Intro.Fits {ℓ : ℕ} (R : ℕ) (splitR splitL : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ) (t : Introspection.AuxType ℓ × Bool) (y α : Cost.BitStr) :

The input's answer fits its two blocks.

Equations

MIPRE.Tailored.Intro.Fits R splitR splitL t y α = (List.length α = splitR t y + splitL t y ∧ splitR t y ≤ R ∧ splitL t y ≤ R)

Instances For

theorem MIPRE.Tailored.Intro.take_take_pad {R : ℕ} {l : Cost.BitStr} (h : List.length l ≤ R) (rest : Cost.BitStr) :

List.take (List.length l) (List.take R (pad R l ++ rest)) = l

theorem MIPRE.Tailored.Intro.unpad_pad {ℓ R : ℕ} {splitR splitL : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ} {t : Introspection.AuxType ℓ × Bool} {y α : Cost.BitStr} (h : Fits R splitR splitL t y α) (rest : Cost.BitStr) :

unpad R splitR splitL t y (pad R (List.take (splitR t y) α) ++ rest) (pad R (List.drop (splitR t y) α)) = α

theorem MIPRE.Tailored.Intro.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) :

enc Q R splitR (Sum.inr t) (Introspection.AnswerParser.pairBits y α) = y ++ pad R (List.take (splitR t y) α) ++ pad R (List.drop (splitR t y) α)

theorem MIPRE.Tailored.Intro.dec_enc_pair {P : Type u_1} {ℓ Q R : ℕ} {splitR splitL : 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) (h : Fits R splitR splitL t y α) :

dec Q R splitR splitL (Sum.inr t) (enc Q R splitR (Sum.inr t) (Introspection.AnswerParser.pairBits y α)) = Introspection.AnswerParser.pairBits y α

theorem MIPRE.Tailored.Intro.dec_enc_read {P : Type u_1} {ℓ Q R : ℕ} {splitR splitL : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ} {w : Bool} {y yp α : Cost.BitStr} (hy : List.length y = Q) (hyp : List.length yp = Q) (h : Fits R splitR splitL (Introspection.AuxType.read , w) y α) :

dec Q R splitR splitL (Sum.inr (Introspection.AuxType.read , w)) (enc Q R splitR (Sum.inr (Introspection.AuxType.read , w)) (Introspection.AnswerParser.tripleBits y yp α)) = Introspection.AnswerParser.tripleBits y yp α

theorem MIPRE.Tailored.Intro.dec_enc_hide {P : Type u_1} {ℓ Q R : ℕ} {splitR splitL : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ} {k : Fin ℓ} {w : Bool} {y yp x : Cost.BitStr} (hy : List.length y = Q) (hyp : List.length yp = Q) (hx : List.length x = Q) :

dec Q R splitR splitL (Sum.inr (Introspection.AuxType.hide k, w)) (enc Q R splitR (Sum.inr (Introspection.AuxType.hide k, w)) (Introspection.AnswerParser.tripleBits y yp x)) = Introspection.AnswerParser.tripleBits y yp x

The lengths #

theorem MIPRE.Tailored.Intro.length_enc_pair {P : Type u_1} {ℓ Q R : ℕ} (plen : P → ℕ) (pread : P → Bool) {splitR splitL : 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) (h : Fits R splitR splitL t y α) :

List.length (enc Q R splitR (Sum.inr t) (Introspection.AnswerParser.pairBits y α)) = lenR Q R plen pread (Sum.inr t) + lenL Q R plen pread (Sum.inr t)

theorem MIPRE.Tailored.Intro.length_enc_read {P : Type u_1} {ℓ Q R : ℕ} (plen : P → ℕ) (pread : P → Bool) {splitR splitL : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ} {w : Bool} {y yp α : Cost.BitStr} (hy : List.length y = Q) (hyp : List.length yp = Q) (h : Fits R splitR splitL (Introspection.AuxType.read , w) y α) :

List.length (enc Q R splitR (Sum.inr (Introspection.AuxType.read , w)) (Introspection.AnswerParser.tripleBits y yp α)) = lenR Q R plen pread (Sum.inr (Introspection.AuxType.read , w)) + lenL Q R plen pread (Sum.inr (Introspection.AuxType.read , w))

theorem MIPRE.Tailored.Intro.length_enc_hide {P : Type u_1} {ℓ Q R : ℕ} (plen : P → ℕ) (pread : P → Bool) {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) (hx : List.length x = Q) :

List.length (enc Q R splitR (Sum.inr (Introspection.AuxType.hide k, w)) (Introspection.AnswerParser.tripleBits y yp x)) = lenR Q R plen pread (Sum.inr (Introspection.AuxType.hide k, w)) + lenL Q R plen pread (Sum.inr (Introspection.AuxType.hide k, w))

theorem MIPRE.Tailored.Intro.length_enc_pauli {P : Type u_1} {ℓ : ℕ} (Q R : ℕ) (plen : P → ℕ) (pread : P → Bool) (splitR : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ) (p : P) (bs : Cost.BitStr) (h : List.length bs = plen p) :

List.length (enc Q R splitR (Sum.inl p) bs) = lenR Q R plen pread (Sum.inl p) + lenL Q R plen pread (Sum.inl p)

theorem MIPRE.Tailored.Intro.dec_enc_pauli {P : Type u_1} {ℓ : ℕ} (Q R : ℕ) (splitR splitL : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ) (p : P) (bs : Cost.BitStr) :

dec Q R splitR splitL (Sum.inl p) (enc Q R splitR (Sum.inl p) bs) = bs

Well-formed answers, uniformly #

def MIPRE.Tailored.Intro.OkLayout {P : Type u_1} {ℓ : ℕ} (Q R : ℕ) (plen : P → ℕ) (splitR splitL : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ) :

Introspection.QuestionType P ℓ → Cost.BitStr → Prop

A byte answer is well formed for the layout at a label: a Pauli answer of the label's length, or a tuple whose registers have length Q and whose input answer fits its two blocks.

Equations

One or more equations did not get rendered due to their size.
MIPRE.Tailored.Intro.OkLayout Q R plen splitR splitL (Sum.inl val) x✝ = (List.length x✝ = plen val)

Instances For

theorem MIPRE.Tailored.Intro.dec_enc_of_ok {P : Type u_1} {ℓ Q R : ℕ} {plen : P → ℕ} {splitR splitL : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ} {u : Introspection.QuestionType P ℓ} {bs : Cost.BitStr} (h : OkLayout Q R plen splitR splitL u bs) :

dec Q R splitR splitL u (enc Q R splitR u bs) = bs

The round trip on well-formed answers.

theorem MIPRE.Tailored.Intro.length_enc_of_ok {P : Type u_1} {ℓ Q R : ℕ} {plen : P → ℕ} (pread : P → Bool) {splitR splitL : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ} {u : Introspection.QuestionType P ℓ} {bs : Cost.BitStr} (h : OkLayout Q R plen splitR splitL u bs) :

List.length (enc Q R splitR u bs) = lenR Q R plen pread u + lenL Q R plen pread u

Well-formed answers re-encode to the label's lengths.

On bounded answers #

def MIPRE.Tailored.Intro.decB {P : Type u_1} {ℓ : ℕ} (Q R : ℕ) (splitR splitL : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ) (B : ℕ) (u : Introspection.QuestionType P ℓ) (tb : Cost.BitStr) :

Verifier.Answers B

Decoding into the answers of length at most B, [] when the decoding is longer.

Equations

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

Instances For

theorem MIPRE.Tailored.Intro.decB_enc_of_ok {P : Type u_1} {ℓ Q R : ℕ} {plen : P → ℕ} {splitR splitL : Introspection.AuxType ℓ × Bool → Cost.BitStr → ℕ} {B : ℕ} {u : Introspection.QuestionType P ℓ} (a : Verifier.Answers B) (h : OkLayout Q R plen splitR splitL u ↑a) :

decB Q R splitR splitL B u (enc Q R splitR u ↑a) = a