The input's constraints, re-indexed into the padded layout

At the edge (introspect false, introspect true) the introspection verifier runs the input's decider on the two input answers carried by the two Introspect answers. For a tailored input, that decider accepts exactly when the input's constraints hold of the two input answers (MIPRE.Tailored.TailoredVerifier.tgame_accepts_iff). In the padded layout (MIPRE.Tailored.Intro.enc) an Introspect answer carries the input's readable bits at offset Q and its linear bits at offset Q + R, so an input constraint becomes a constraint on the two tailored answers placed in two windows of each (reindex), and it holds exactly when the original holds of the input answers read off those windows (satisfies_reindex_iff).

def MIPRE.Tailored.Intro.place2 (n o₁ : ℕ) (w₁ : Cost.BitStr) (o₂ : ℕ) (w₂ : Cost.BitStr) : Cost.BitStr

Two vectors placed at two offsets of a vector of length n, the first before the second.

Equations

• MIPRE.Tailored.Intro.place2 n o₁ w₁ o₂ w₂ = List.replicate o₁ false ++ w₁ ++ MIPRE.Tailored.Intro.place (n - o₁ - List.length w₁) (o₂ - o₁ - List.length w₁) w₂

theorem MIPRE.Tailored.Intro.length_place2 {n o₁ o₂ : ℕ} {w₁ w₂ : Cost.BitStr} (h₁ : o₁ + List.length w₁ ≤ o₂) (h₂ : o₂ + List.length w₂ ≤ n) : List.length (place2 n o₁ w₁ o₂ w₂) = n

theorem MIPRE.Tailored.Intro.dotL_place2 {n o₁ o₂ : ℕ} {w₁ w₂ a : Cost.BitStr} (h₁ : o₁ + List.length w₁ ≤ o₂) (h₂ : o₂ + List.length w₂ ≤ n) (ha : List.length a = n) : dotL (place2 n o₁ w₁ o₂ w₂) a = (dotL w₁ (List.take (List.length w₁) (List.drop o₁ a)) ^^ dotL w₂ (List.take (List.length w₂) (List.drop o₂ a)))

def MIPRE.Tailored.Intro.inputOf (Q R : ℕ) (a : Cost.BitStr) (lR lL : ℕ) : Cost.BitStr

The two answer windows of an input answer in the layout: the readable bits at Q, the linear ones at Q + R.

Equations

• MIPRE.Tailored.Intro.inputOf Q R a lR lL = List.take lR (List.drop Q a) ++ List.take lL (List.drop (Q + R) a)

def MIPRE.Tailored.Intro.reindex (Q R lRa lLa lRb lLb la lb : ℕ) (c : Cost.BitStr) : Cost.BitStr

An input constraint, re-indexed onto tailored answers of lengths la, lb; a constraint of the wrong length (never satisfied) becomes the rejecting one.

Equations

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

theorem MIPRE.Tailored.Intro.dotL_split_right {c u v : Cost.BitStr} (h : List.length u ≤ List.length c) : dotL c (u ++ v) = (dotL (List.take (List.length u) c) u ^^ dotL (List.drop (List.length u) c) v)

theorem MIPRE.Tailored.Intro.satisfies_reindex_iff (Q R lRa lLa lRb lLb : ℕ) {la lb : ℕ} {a b : Cost.BitStr} (ha : List.length a = la) (hb : List.length b = lb) (hRa : lRa ≤ R) (hLa : Q + R + lLa ≤ la) (hRb : lRb ≤ R) (hLb : Q + R + lLb ≤ lb) (c : Cost.BitStr) : Satisfies (reindex Q R lRa lLa lRb lLb la lb c) (a ++ b ++ [true]) ↔ Satisfies c (inputOf Q R a lRa lLa ++ inputOf Q R b lRb lLb ++ [true])

The re-indexed constraint holds exactly when the original holds of the input answers.