The auxiliary answers, read off the padded layout

In the padded layout of the tailored introspection verifier (MIPRE.Tailored.Intro.enc) an auxiliary answer is a list of windows: the register y at 0; at Introspect and Sample the input's readable answer bits at Q and its linear ones at Q + R; at Read the same readable bits at Q, the dual y' at Q + R and the linear bits at 2Q + R; at Hide the dual y' at Q and the tail x at 2Q. This file reads the parsed answer of the introspection verifier's kernel off those windows (parsed), and writes the comparisons of its auxiliary checks between two such answers as linear constraints:

• srcEqCons, srcEqCons_iff: two input answers are equal: their splits and readable bits agree (a readable condition) and their linear bits agree (bit by bit);
• regEqCons_iff: two registers in windows are equal;
• sampleCons, readCons, hideReadCons, hideNextCons, sourceCons: the clauses of the directed checks (AuxiliaryQuotient.directed), each with its _iff;
• sameCons: consistency of two answers at one label;
• swapCon: a constraint on (b, a) as one on (a, b), for the other orientation;
• auxPair, auxPair_iff: all of it at an ordered pair of auxiliary labels, with a readable condition G on each register: the constraints hold exactly when G holds at both registers, the parsed answers agree when the labels do, and the directed checks accept both ways.

The input's split of its answer at a register, sR and sL, and the source game's constraints are parameters, as are lists of generators of the kernels of the hiding stages' linear maps (KerGens); the instance supplies them.

Windows

def MIPRE.Tailored.Intro.win (a : Cost.BitStr) (o m : ℕ) : Cost.BitStr

The window of length m at offset o.

Equations

• MIPRE.Tailored.Intro.win a o m = List.take m (List.drop o a)

theorem MIPRE.Tailored.Intro.length_win {a : Cost.BitStr} {o m : ℕ} (h : o + m ≤ List.length a) : List.length (win a o m) = m

theorem MIPRE.Tailored.Intro.win_take {a : Cost.BitStr} {o m n : ℕ} (h : o + m ≤ n) : win (List.take n a) o m = win a o m

A window inside a prefix is the window of the whole.

def MIPRE.Tailored.Intro.reg (Q : ℕ) (a : Cost.BitStr) (o : ℕ) : Fin Q → CL.𝔽₂

The register in the window of length Q at offset o.

Equations

• MIPRE.Tailored.Intro.reg Q a o = MIPRE.CL.ofBits Q (MIPRE.Tailored.Intro.win a o Q)

theorem MIPRE.Tailored.Intro.toBits_reg {Q : ℕ} {a : Cost.BitStr} {o : ℕ} (h : o + Q ≤ List.length a) : CL.toBits (reg Q a o) = win a o Q

theorem MIPRE.Tailored.Intro.reg_eq_iff {Q : ℕ} {a b : Cost.BitStr} {oa ob : ℕ} (ha : oa + Q ≤ List.length a) (hb : ob + Q ≤ List.length b) : reg Q a oa = reg Q b ob ↔ win a oa Q = win b ob Q

Equality of two windows of the two answers

theorem MIPRE.Tailored.Intro.regEqCons_iff {Q la lb oa ob : ℕ} {a b : Cost.BitStr} (ha : List.length a = la) (hb : List.length b = lb) (hoa : oa + Q ≤ la) (hob : ob + Q ≤ lb) : (∀ c ∈ eqCons la lb oa ob Q, Satisfies c (a ++ b ++ [true])) ↔ reg Q a oa = reg Q b ob

Two registers in windows are equal exactly when the window constraints hold.

def MIPRE.Tailored.Intro.srcEqCons (la lb oRa oLa oRb oLb sRa sLa sRb sLb : ℕ) (aR bR : Cost.BitStr) : List Cost.BitStr

The constraints that two input answers are equal: the splits and the readable bits agree, a readable condition, and the linear bits agree bit by bit. The readable bits are windows of the readable parts aR, bR; the linear bits windows of the answers.

Equations

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

theorem MIPRE.Tailored.Intro.forall_mem_append {l₁ l₂ : List Cost.BitStr} {p : Cost.BitStr → Prop} : (∀ c ∈ l₁ ++ l₂, p c) ↔ (∀ c ∈ l₁, p c) ∧ ∀ c ∈ l₂, p c

theorem MIPRE.Tailored.Intro.srcEqCons_iff {la lb lRa lRb oRa oLa oRb oLb sRa sLa sRb sLb : ℕ} {a b : Cost.BitStr} (ha : List.length a = la) (hb : List.length b = lb) (hRa : oRa + sRa ≤ lRa) (hRb : oRb + sRb ≤ lRb) (hla : lRa ≤ la) (hlb : lRb ≤ lb) (hLa : oLa + sLa ≤ la) (hLb : oLb + sLa ≤ lb) : (∀ c ∈ srcEqCons la lb oRa oLa oRb oLb sRa sLa sRb sLb (List.take lRa a) (List.take lRb b), Satisfies c (a ++ b ++ [true])) ↔ sRa = sRb ∧ sLa = sLb ∧ win a oRa sRa ++ win a oLa sLa = win b oRb sRb ++ win b oLb sLb

The input-answer equality constraints, read: with the readable windows inside the readable parts, they hold exactly when the splits agree and the two input answers, the readable window followed by the linear window, are equal.

The parsed auxiliary answer

def MIPRE.Tailored.Intro.auxLenR (Q R : ℕ) : Introspection.AuxType 7 → ℕ

The number of readable bits of an auxiliary label.

Equations

• MIPRE.Tailored.Intro.auxLenR Q R (MIPRE.Introspection.AuxType.hide k) = Q
• MIPRE.Tailored.Intro.auxLenR Q R x✝ = Q + R

def MIPRE.Tailored.Intro.auxLen (Q R : ℕ) : Introspection.AuxType 7 → ℕ

The number of bits of an auxiliary label.

Equations

• MIPRE.Tailored.Intro.auxLen Q R MIPRE.Introspection.AuxType.introspect = Q + 2 * R
• MIPRE.Tailored.Intro.auxLen Q R MIPRE.Introspection.AuxType.sample = Q + 2 * R
• MIPRE.Tailored.Intro.auxLen Q R MIPRE.Introspection.AuxType.read = 2 * Q + 2 * R
• MIPRE.Tailored.Intro.auxLen Q R (MIPRE.Introspection.AuxType.hide k) = 3 * Q

def MIPRE.Tailored.Intro.srcOffL (Q R : ℕ) : Introspection.AuxType 7 → ℕ

The offset of the input's linear answer bits.

Equations

• MIPRE.Tailored.Intro.srcOffL Q R MIPRE.Introspection.AuxType.read = 2 * Q + R
• MIPRE.Tailored.Intro.srcOffL Q R x✝ = Q + R

def MIPRE.Tailored.Intro.srcAns (Q R : ℕ) (sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (t : Introspection.AuxType 7 × Bool) (a : Cost.BitStr) : Cost.BitStr

The input's answer carried by an auxiliary answer: the readable window at Q and the linear window at srcOffL, of the lengths the input gives at the register y.

Equations

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

def MIPRE.Tailored.Intro.parsed (Q R : ℕ) (sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) {PA : Type u_1} : Introspection.AuxType 7 × Bool → Cost.BitStr → Introspection.ParsedAnswer (Fin Q → CL.𝔽₂) (Verifier.Answers R) PA

The kernel's parsed answer read off the windows of an auxiliary answer.

Equations

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

def MIPRE.Tailored.Intro.srcFits (R : ℕ) (sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (t : Introspection.AuxType 7 × Bool) (y : Cost.BitStr) : Prop

The readable condition on one auxiliary answer: the input's answer fits the original cutoff.

Equations

• MIPRE.Tailored.Intro.srcFits R sR sL t y = match t.1 with | MIPRE.Introspection.AuxType.hide k => True | x => sR t y + sL t y ≤ R

theorem MIPRE.Tailored.Intro.length_srcAns {Q R : ℕ} {sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ} {t : Introspection.AuxType 7 × Bool} {a : Cost.BitStr} (ha : List.length a = auxLen Q R t.1) (hf : srcFits R sR sL t (win a 0 Q)) (ht : ∀ (k : Fin 7), t.1 ≠ Introspection.AuxType.hide k) : List.length (srcAns Q R sR sL t a) = sR t (win a 0 Q) + sL t (win a 0 Q)

theorem MIPRE.Tailored.Intro.bounded_srcAns_val {Q R : ℕ} {sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ} {t : Introspection.AuxType 7 × Bool} {a : Cost.BitStr} (ha : List.length a = auxLen Q R t.1) (hf : srcFits R sR sL t (win a 0 Q)) (ht : ∀ (k : Fin 7), t.1 ≠ Introspection.AuxType.hide k) : ↑(Introspection.AuxiliaryAnswer.bounded R (srcAns Q R sR sL t a)) = srcAns Q R sR sL t a

The comparisons of the auxiliary checks

noncomputable def MIPRE.Tailored.Intro.sampleCons (Q R : ℕ) (sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (L : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7) (w : Bool) (aR bR : Cost.BitStr) : List Cost.BitStr

The sampling comparison between Introspect w (a) and Sample w (b): y = L_w(z), a readable condition, and equal input answers.

Equations

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

def MIPRE.Tailored.Intro.readCons (Q R : ℕ) (sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (w : Bool) (aR bR : Cost.BitStr) : List Cost.BitStr

The reading comparison between Introspect w (a) and Read w (b): equal registers, a readable condition, and equal input answers.

Equations

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

noncomputable def MIPRE.Tailored.Intro.hideReadCons (Q R : ℕ) (L : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7) (w : Bool) (aR bR : Cost.BitStr) : List Cost.BitStr

The comparison between the last Hide w (a) and Read w (b): equal prefixes of the registers, a readable condition, and equal duals.

Equations

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

def MIPRE.Tailored.Intro.KerGens (Q : ℕ) (kg : (S : Finset (Fin Q)) → CL.RegLinear CL.𝔽₂ S → List (Fin Q → CL.𝔽₂)) : Prop

Lists of vectors spanning the kernel of every register-local linear map.

Equations

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

noncomputable def MIPRE.Tailored.Intro.hideNextCons (Q : ℕ) (L : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7) (kg : (S : Finset (Fin Q)) → CL.RegLinear CL.𝔽₂ S → List (Fin Q → CL.𝔽₂)) (w : Bool) (k : ℕ) (aR bR : Cost.BitStr) : List Cost.BitStr

The comparison between Hide level k + 1 (a) and the next level (b), both w: equal prefixes, a readable condition; the duals equal on the prefix register of b, the tails equal off the next one; and the dual readout of b at its stage equal at b's dual and a's tail.

Equations

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

theorem MIPRE.Tailored.Intro.bounded_srcAns_eq_iff {Q R : ℕ} {sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ} {t u : Introspection.AuxType 7 × Bool} {a b : Cost.BitStr} (ha : List.length a = auxLen Q R t.1) (hb : List.length b = auxLen Q R u.1) (hfa : srcFits R sR sL t (win a 0 Q)) (hfb : srcFits R sR sL u (win b 0 Q)) (hta : ∀ (k : Fin 7), t.1 ≠ Introspection.AuxType.hide k) (htb : ∀ (k : Fin 7), u.1 ≠ Introspection.AuxType.hide k) : Introspection.AuxiliaryAnswer.bounded R (srcAns Q R sR sL t a) = Introspection.AuxiliaryAnswer.bounded R (srcAns Q R sR sL u b) ↔ srcAns Q R sR sL t a = srcAns Q R sR sL u b

theorem MIPRE.Tailored.Intro.sampleCons_iff {Q R : ℕ} {sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ} {L : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7} {w : Bool} {a b : Cost.BitStr} (ha : List.length a = auxLen Q R Introspection.AuxType.introspect) (hb : List.length b = auxLen Q R Introspection.AuxType.sample) (hfa : srcFits R sR sL (Introspection.AuxType.introspect, w) (win a 0 Q)) (hfb : srcFits R sR sL (Introspection.AuxType.sample, w) (win b 0 Q)) (hsplit : ∀ (y z : Cost.BitStr), CL.ofBits Q y = (L w).eval (CL.ofBits Q z) → sR (Introspection.AuxType.introspect, w) y = sR (Introspection.AuxType.sample, w) z ∧ sL (Introspection.AuxType.introspect, w) y = sL (Introspection.AuxType.sample, w) z) : (∀ c ∈ sampleCons Q R sR sL L w (List.take (Q + R) a) (List.take (Q + R) b), Satisfies c (a ++ b ++ [true])) ↔ Introspection.CLChecks.sampling (L w) (reg Q a 0, Introspection.AuxiliaryAnswer.bounded R (srcAns Q R sR sL (Introspection.AuxType.introspect, w) a)) (reg Q b 0, Introspection.AuxiliaryAnswer.bounded R (srcAns Q R sR sL (Introspection.AuxType.sample, w) b))

The sampling comparison as constraints. The input's split at a Sample answer is that at the Introspect answer of the register it samples (hsplit).

theorem MIPRE.Tailored.Intro.readCons_iff {Q R : ℕ} {sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ} {w : Bool} {a b : Cost.BitStr} (ha : List.length a = auxLen Q R Introspection.AuxType.introspect) (hb : List.length b = auxLen Q R Introspection.AuxType.read) (hfa : srcFits R sR sL (Introspection.AuxType.introspect, w) (win a 0 Q)) (hfb : srcFits R sR sL (Introspection.AuxType.read, w) (win b 0 Q)) (hsplit : ∀ (y : Cost.BitStr), sR (Introspection.AuxType.introspect, w) y = sR (Introspection.AuxType.read, w) y ∧ sL (Introspection.AuxType.introspect, w) y = sL (Introspection.AuxType.read, w) y) : (∀ c ∈ readCons Q R sR sL w (List.take (Q + R) a) (List.take (Q + R) b), Satisfies c (a ++ b ++ [true])) ↔ Introspection.CLChecks.reading (reg Q a 0, Introspection.AuxiliaryAnswer.bounded R (srcAns Q R sR sL (Introspection.AuxType.introspect, w) a)) (reg Q b 0, reg Q b (Q + R), Introspection.AuxiliaryAnswer.bounded R (srcAns Q R sR sL (Introspection.AuxType.read, w) b))

The reading comparison as constraints. The input's split at a Read answer is that at an Introspect answer of the same register (hsplit).

theorem MIPRE.Tailored.Intro.hideReadCons_iff {Q R : ℕ} {L : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7} {w : Bool} {k : Fin 7} {a b : Cost.BitStr} (ha : List.length a = auxLen Q R (Introspection.AuxType.hide k)) (hb : List.length b = auxLen Q R Introspection.AuxType.read) (α : Verifier.Answers R) : (∀ c ∈ hideReadCons Q R L w (List.take Q a) (List.take (Q + R) b), Satisfies c (a ++ b ++ [true])) ↔ Introspection.CLChecks.hidingRead (L w) (reg Q a 0, reg Q a Q, reg Q a (2 * Q)) (reg Q b 0, reg Q b (Q + R), α)

The comparison of the last Hide with Read as constraints.

theorem MIPRE.Tailored.Intro.hideNextCons_iff {Q : ℕ} {L : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7} {kg : (S : Finset (Fin Q)) → CL.RegLinear CL.𝔽₂ S → List (Fin Q → CL.𝔽₂)} (hkg : KerGens Q kg) {w : Bool} {k : ℕ} {a b : Cost.BitStr} (ha : List.length a = 3 * Q) (hb : List.length b = 3 * Q) : (∀ c ∈ hideNextCons Q L kg w k (List.take Q a) (List.take Q b), Satisfies c (a ++ b ++ [true])) ↔ Introspection.AuxiliaryQuotient.hidingNext (L w) k (reg Q a 0, reg Q a Q, reg Q a (2 * Q)) (reg Q b 0, reg Q b Q, reg Q b (2 * Q))

The comparison of consecutive Hide levels as constraints.

Consistency at one label

def MIPRE.Tailored.Intro.sameCons (Q R : ℕ) (sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (t : Introspection.AuxType 7 × Bool) (aR bR : Cost.BitStr) : List Cost.BitStr

The comparison of two answers at the same auxiliary label: equal registers, a readable condition, and equal duals, tails and input answers.

Equations

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

theorem MIPRE.Tailored.Intro.sameCons_iff {Q R : ℕ} {sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ} {PA : Type u_1} {t : Introspection.AuxType 7 × Bool} {a b : Cost.BitStr} (ha : List.length a = auxLen Q R t.1) (hb : List.length b = auxLen Q R t.1) (hfa : srcFits R sR sL t (win a 0 Q)) (hfb : srcFits R sR sL t (win b 0 Q)) : (∀ c ∈ sameCons Q R sR sL t (List.take (auxLenR Q R t.1) a) (List.take (auxLenR Q R t.1) b), Satisfies c (a ++ b ++ [true])) ↔ parsed Q R sR sL t a = parsed Q R sR sL t b

Consistency at one label as constraints: they hold exactly when the parsed answers are equal.

The source game

def MIPRE.Tailored.Intro.sourceCons (Q R : ℕ) (sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (srcCons : Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → List Cost.BitStr) (aR bR : Cost.BitStr) : List Cost.BitStr

The source game's constraints at the edge (Introspect false, Introspect true): the input's constraints srcCons at the two registers and the two readable input answers, re-indexed onto the windows of the two Introspect answers.

Equations

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

theorem MIPRE.Tailored.Intro.sourceCons_iff {Q R : ℕ} {sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ} {srcCons : Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → List Cost.BitStr} {D : (Fin Q → CL.𝔽₂) → (Fin Q → CL.𝔽₂) → Verifier.Answers R → Verifier.Answers R → Bool} (hD : ∀ (ya yb : Cost.BitStr), List.length ya = Q → List.length yb = Q → ∀ (α β : Verifier.Answers R), D (CL.ofBits Q ya) (CL.ofBits Q yb) α β = true ↔ List.length ↑α = sR (Introspection.AuxType.introspect, false) ya + sL (Introspection.AuxType.introspect, false) ya ∧ List.length ↑β = sR (Introspection.AuxType.introspect, true) yb + sL (Introspection.AuxType.introspect, true) yb ∧ ∀ c ∈ srcCons ya yb (List.take (sR (Introspection.AuxType.introspect, false) ya) ↑α) (List.take (sR (Introspection.AuxType.introspect, true) yb) ↑β), Satisfies c (↑α ++ ↑β ++ [true])) {a b : Cost.BitStr} (ha : List.length a = auxLen Q R Introspection.AuxType.introspect) (hb : List.length b = auxLen Q R Introspection.AuxType.introspect) (hfa : srcFits R sR sL (Introspection.AuxType.introspect, false) (win a 0 Q)) (hfb : srcFits R sR sL (Introspection.AuxType.introspect, true) (win b 0 Q)) : (∀ c ∈ sourceCons Q R sR sL srcCons (List.take (Q + R) a) (List.take (Q + R) b), Satisfies c (a ++ b ++ [true])) ↔ D (reg Q a 0) (reg Q b 0) (Introspection.AuxiliaryAnswer.bounded R (srcAns Q R sR sL (Introspection.AuxType.introspect, false) a)) (Introspection.AuxiliaryAnswer.bounded R (srcAns Q R sR sL (Introspection.AuxType.introspect, true) b)) = true

The source game's constraints: when the source predicate D accepts exactly the input answers of the input's lengths satisfying the input's constraints (hD), the re-indexed constraints hold exactly when D accepts the two parsed Introspect answers.

The other orientation

def MIPRE.Tailored.Intro.swapCon (la lb : ℕ) (c : Cost.BitStr) : Cost.BitStr

A constraint on (b, a), with b of length lb and a of length la, as one on (a, b).

Equations

• MIPRE.Tailored.Intro.swapCon la lb c = List.take la (List.drop lb c) ++ List.take lb c ++ List.drop (lb + la) c

theorem MIPRE.Tailored.Intro.satisfies_swapCon {la lb : ℕ} {a b : Cost.BitStr} (ha : List.length a = la) (hb : List.length b = lb) (c : Cost.BitStr) : Satisfies (swapCon la lb c) (a ++ b ++ [true]) ↔ Satisfies c (b ++ a ++ [true])

A swapped constraint holds of (a, b) exactly when the constraint holds of (b, a).

theorem MIPRE.Tailored.Intro.forall_swapCon_iff {la lb : ℕ} {a b : Cost.BitStr} (ha : List.length a = la) (hb : List.length b = lb) (cs : List Cost.BitStr) : (∀ c ∈ List.map (swapCon la lb) cs, Satisfies c (a ++ b ++ [true])) ↔ ∀ c ∈ cs, Satisfies c (b ++ a ++ [true])

One orientation of the directed checks between auxiliary answers

noncomputable def MIPRE.Tailored.Intro.dirAux (Q R : ℕ) (sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (L : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7) (kg : (S : Finset (Fin Q)) → CL.RegLinear CL.𝔽₂ S → List (Fin Q → CL.𝔽₂)) (srcCons : Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → List Cost.BitStr) : Introspection.AuxType 7 × Bool → Introspection.AuxType 7 × Bool → Cost.BitStr → Cost.BitStr → List Cost.BitStr

The constraints of one orientation of the directed auxiliary checks, on an ordered pair of auxiliary labels: those of AuxiliaryQuotient.directed's clause for the pair, none when it has none.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Tailored.Intro.dirAux Q R sR sL L kg srcCons x✝³ x✝² x✝¹ x✝ = []

theorem MIPRE.Tailored.Intro.dirAux_iff {Q R : ℕ} {sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ} {L : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7} {P : Type u_1} {PA : Type u_2} (X Z : P) (project : PA → Fin Q → CL.𝔽₂) {kg : (S : Finset (Fin Q)) → CL.RegLinear CL.𝔽₂ S → List (Fin Q → CL.𝔽₂)} (hkg : KerGens Q kg) {srcCons : Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → List Cost.BitStr} {D : (Fin Q → CL.𝔽₂) → (Fin Q → CL.𝔽₂) → Verifier.Answers R → Verifier.Answers R → Bool} (hD : ∀ (ya yb : Cost.BitStr), List.length ya = Q → List.length yb = Q → ∀ (α β : Verifier.Answers R), D (CL.ofBits Q ya) (CL.ofBits Q yb) α β = true ↔ List.length ↑α = sR (Introspection.AuxType.introspect, false) ya + sL (Introspection.AuxType.introspect, false) ya ∧ List.length ↑β = sR (Introspection.AuxType.introspect, true) yb + sL (Introspection.AuxType.introspect, true) yb ∧ ∀ c ∈ srcCons ya yb (List.take (sR (Introspection.AuxType.introspect, false) ya) ↑α) (List.take (sR (Introspection.AuxType.introspect, true) yb) ↑β), Satisfies c (↑α ++ ↑β ++ [true])) (hS : ∀ (w : Bool) (y z : Cost.BitStr), CL.ofBits Q y = (L w).eval (CL.ofBits Q z) → sR (Introspection.AuxType.introspect, w) y = sR (Introspection.AuxType.sample, w) z ∧ sL (Introspection.AuxType.introspect, w) y = sL (Introspection.AuxType.sample, w) z) (hRd : ∀ (w : Bool) (y : Cost.BitStr), sR (Introspection.AuxType.introspect, w) y = sR (Introspection.AuxType.read, w) y ∧ sL (Introspection.AuxType.introspect, w) y = sL (Introspection.AuxType.read, w) y) {t u : Introspection.AuxType 7 × Bool} {a b : Cost.BitStr} (ha : List.length a = auxLen Q R t.1) (hb : List.length b = auxLen Q R u.1) (hfa : srcFits R sR sL t (win a 0 Q)) (hfb : srcFits R sR sL u (win b 0 Q)) : (∀ c ∈ dirAux Q R sR sL L kg srcCons t u (List.take (auxLenR Q R t.1) a) (List.take (auxLenR Q R u.1) b), Satisfies c (a ++ b ++ [true])) ↔ Introspection.AuxiliaryQuotient.directed L X Z project D (Sum.inr t) (Sum.inr u) (parsed Q R sR sL t a) (parsed Q R sR sL u b) = true

One orientation of the directed auxiliary checks as constraints.

A pair of auxiliary answers

noncomputable def MIPRE.Tailored.Intro.auxPair (Q R : ℕ) (sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (L : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7) (G : Introspection.AuxType 7 × Bool → Cost.BitStr → Prop) (kg : (S : Finset (Fin Q)) → CL.RegLinear CL.𝔽₂ S → List (Fin Q → CL.𝔽₂)) (srcCons : Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → List Cost.BitStr) (t u : Introspection.AuxType 7 × Bool) (aR bR : Cost.BitStr) : List Cost.BitStr

The constraints at an ordered pair of auxiliary labels: when a readable condition G holds at both registers, consistency when the labels agree and the directed checks in both orientations; otherwise the rejecting constraint alone (the checks' data need not be computable off G).

Equations

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

theorem MIPRE.Tailored.Intro.auxLenR_add_le {Q R : ℕ} (t : Introspection.AuxType 7) : Q ≤ auxLenR Q R t

theorem MIPRE.Tailored.Intro.auxPair_iff {Q R : ℕ} {sR sL : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ} {L : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7} {P : Type u_1} {PA : Type u_2} (X Z : P) (project : PA → Fin Q → CL.𝔽₂) {G : Introspection.AuxType 7 × Bool → Cost.BitStr → Prop} (hG : ∀ (t : Introspection.AuxType 7 × Bool) (y : Cost.BitStr), G t y → srcFits R sR sL t y) {kg : (S : Finset (Fin Q)) → CL.RegLinear CL.𝔽₂ S → List (Fin Q → CL.𝔽₂)} (hkg : KerGens Q kg) {srcCons : Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → List Cost.BitStr} {D : (Fin Q → CL.𝔽₂) → (Fin Q → CL.𝔽₂) → Verifier.Answers R → Verifier.Answers R → Bool} (hD : ∀ (ya yb : Cost.BitStr), List.length ya = Q → List.length yb = Q → ∀ (α β : Verifier.Answers R), D (CL.ofBits Q ya) (CL.ofBits Q yb) α β = true ↔ List.length ↑α = sR (Introspection.AuxType.introspect, false) ya + sL (Introspection.AuxType.introspect, false) ya ∧ List.length ↑β = sR (Introspection.AuxType.introspect, true) yb + sL (Introspection.AuxType.introspect, true) yb ∧ ∀ c ∈ srcCons ya yb (List.take (sR (Introspection.AuxType.introspect, false) ya) ↑α) (List.take (sR (Introspection.AuxType.introspect, true) yb) ↑β), Satisfies c (↑α ++ ↑β ++ [true])) (hS : ∀ (w : Bool) (y z : Cost.BitStr), CL.ofBits Q y = (L w).eval (CL.ofBits Q z) → sR (Introspection.AuxType.introspect, w) y = sR (Introspection.AuxType.sample, w) z ∧ sL (Introspection.AuxType.introspect, w) y = sL (Introspection.AuxType.sample, w) z) (hRd : ∀ (w : Bool) (y : Cost.BitStr), sR (Introspection.AuxType.introspect, w) y = sR (Introspection.AuxType.read, w) y ∧ sL (Introspection.AuxType.introspect, w) y = sL (Introspection.AuxType.read, w) y) {t u : Introspection.AuxType 7 × Bool} {a b : Cost.BitStr} (ha : List.length a = auxLen Q R t.1) (hb : List.length b = auxLen Q R u.1) : (∀ c ∈ auxPair Q R sR sL L G kg srcCons t u (List.take (auxLenR Q R t.1) a) (List.take (auxLenR Q R u.1) b), Satisfies c (a ++ b ++ [true])) ↔ G t (win a 0 Q) ∧ G u (win b 0 Q) ∧ (t = u → parsed Q R sR sL t a = parsed Q R sR sL u b) ∧ Introspection.AuxiliaryQuotient.directed L X Z project D (Sum.inr t) (Sum.inr u) (parsed Q R sR sL t a) (parsed Q R sR sL u b) = true ∧ Introspection.AuxiliaryQuotient.directed L X Z project D (Sum.inr u) (Sum.inr t) (parsed Q R sR sL u b) (parsed Q R sR sL t a) = true

The constraints at a pair of auxiliary labels: they hold exactly when the readable condition holds at both registers, the parsed answers agree when the labels do, and the directed checks accept in both orientations.