The first hiding edge as controlled linear constraints

The first hiding edge of the introspection verifier compares an X-basis Pauli answer a with a Hide answer (y, y', x) of level 0, three registers of Q = 2^(2^j) k bits. The kernel reads the Pauli answer as the register Π a = pauliProject (pauliDecode a): its field elements expanded in the self-dual normal basis (QLD.PauliFullAnswerProgram.registerVector). The check is the quotient relaxation AuxiliaryQuotient.hidingPauli: the duals of y' and of Π a under the first stage of the conditionally linear function P agree, and Π a and x agree off the first factor S = P.factorOfPrefix 0 0.

Π is F₂-linear in the answer bits (pauliXProj, pauliXProj_eq), so both halves are linear checks on the two answers, with coefficients computed from P:

• for z in a list gens spanning the kernel of stageLinear P 0 0: ∑ zᵢ (proj S (Π a))ᵢ + ∑ zᵢ (proj S y')ᵢ = 0, which over the whole list is the equality of duals (AuxiliaryDual.registerDual_eq_iff_dot, as in MIPRE.Tailored.Intro.dualCons_iff);
• for i ∉ S, enumerated along List.finRange: (Π a)ᵢ = xᵢ.

hideChecks writes them for the two answers at arbitrary offsets of one bit vector, and hideChecks_iff is their meaning; pauliHideCons (Pauli answer first) and pauliHideConsRev (Hide answer first) are the constraint lists of the two orientations of the edge, and pauliHideCons_iff, pauliHideConsRev_iff the main theorems.

The file also records the byte round trip of the Pauli answers at their label lengths (answerBits_decodeBits_of_length), for every label.

The byte round trip

theorem MIPRE.Tailored.Intro.PauliHide.answerBits_decodeBits_of_length (k : ℕ) (hk : 1 ≤ k) (m : ℕ) (T : QLD.Ty) (a : Cost.BitStr) (ha : List.length a = pauliLen m k T) : QLD.PauliAnswerProgram.answerBits (SAT.shoupBinField k hk) (QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) m 1 T a) = a

The byte round trip of Pauli answers: an answer of its label's length is the encoding of its decoding, at every label.

theorem MIPRE.Tailored.Intro.PauliHide.decodeBits_fmtOk (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (T : QLD.Ty) (q a : Cost.BitStr) : (QLD.PauliBinaryProgram.questionOfBits k hk hodd j T q).fmtOk (QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) (2 ^ j) 1 T a) = true

The decoded answer has the format of the decoded question (any payloads).

Registers of the answer bits

def MIPRE.Tailored.Intro.PauliHide.regAt (N o s : ℕ) : (Fin N → ZMod 2) →ₗ[ZMod 2] Fin s → ZMod 2

The register of s bits starting at position o.

Equations

• MIPRE.Tailored.Intro.PauliHide.regAt N o s = LinearMap.pi fun (i : Fin s) => MIPRE.Tailored.Intro.getv N (o + ↑i)

theorem MIPRE.Tailored.Intro.PauliHide.regAt_eq {N : ℕ} {v : Fin N → ZMod 2} {o o' s : ℕ} {w : Cost.BitStr} (h : PauliCons.Reads v o w) (hw : o' + s ≤ List.length w) : (regAt N (o + o') s) v = CL.ofBits s (List.drop o' w)

theorem MIPRE.Tailored.Intro.PauliHide.ofBits_append_left (s : ℕ) (u w : Cost.BitStr) (hu : List.length u = s) : CL.ofBits s (u ++ w) = CL.ofBits s u

def MIPRE.Tailored.Intro.PauliHide.dotForm {s : ℕ} (w : Fin s → ZMod 2) : (Fin s → ZMod 2) →ₗ[ZMod 2] ZMod 2

The inner product with w, as a linear form.

Equations

• MIPRE.Tailored.Intro.PauliHide.dotForm w = { toFun := fun (x : Fin s → ZMod 2) => ∑ i : Fin s, w i * x i, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MIPRE.Tailored.Intro.PauliHide.dotForm_apply {s : ℕ} (w x : Fin s → ZMod 2) : (dotForm w) x = ∑ i : Fin s, w i * x i

noncomputable def MIPRE.Tailored.Intro.PauliHide.pauliXProj (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j N o : ℕ) : (Fin N → ZMod 2) →ₗ[ZMod 2] Fin (2 ^ 2 ^ j * k) → ZMod 2

The full Pauli register of the answer at position o: the field element of entry z is read at o + z k (z numbered by cubeEnumeration) and expanded in the self-dual normal basis, in the numbering registerNumbering.

Equations

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

theorem MIPRE.Tailored.Intro.PauliHide.pauliXProj_eq {N : ℕ} (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (W : QLD.Bas) {v : Fin N → ZMod 2} {o : ℕ} {a : Cost.BitStr} (h : PauliCons.Reads v o a) (ha : List.length a = pauliLen (2 ^ j) k (QLD.Ty.pauli W)) : (pauliXProj k hk hodd j N o) v = Introspection.DecisionKernel.Answer.pauliProject (SAT.shoupSelfDualNormalBasis k hk hodd) (Introspection.DecisionKernel.Answer.pauliDecode (SAT.shoupBinField k hk) (2 ^ j) (Sum.inl (QLD.Ty.pauli W)) a)

pauliXProj reads the kernel's register of a Pauli answer of its label's length, in either basis.

The checks

noncomputable def MIPRE.Tailored.Intro.PauliHide.hideChecks (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j N oP oH : ℕ) {ℓ : ℕ} (P : CL.CLFun CL.𝔽₂ (Fin (2 ^ 2 ^ j * k)) ℓ) (gens : List (Fin (2 ^ 2 ^ j * k) → CL.𝔽₂)) : List (LinCheck N)

The checks of the first hiding edge, for a Pauli answer at oP and a Hide answer (y, y', x) at oH, its registers at oH, oH + Q, oH + 2Q.

Equations

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

theorem MIPRE.Tailored.Intro.PauliHide.hideChecks_iff (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) {N oP oH ℓ : ℕ} (P : CL.CLFun CL.𝔽₂ (Fin (2 ^ 2 ^ j * k)) ℓ) (gens : List (Fin (2 ^ 2 ^ j * k) → CL.𝔽₂)) (hgens : ∀ g ∈ gens, (Introspection.CLChecks.stageLinear P 0 0) g = 0) (hspan : ∀ (z : Fin (2 ^ 2 ^ j * k) → CL.𝔽₂), (Introspection.CLChecks.stageLinear P 0 0) z = 0 → z ∈ Submodule.span CL.𝔽₂ {g : Fin (2 ^ 2 ^ j * k) → CL.𝔽₂ | g ∈ gens}) (v : Fin N → ZMod 2) (X Y Y' X' : Fin (2 ^ 2 ^ j * k) → CL.𝔽₂) (hX : (pauliXProj k hk hodd j N oP) v = X) (hY' : (regAt N (oH + 2 ^ 2 ^ j * k) (2 ^ 2 ^ j * k)) v = Y') (hX' : (regAt N (oH + 2 * (2 ^ 2 ^ j * k)) (2 ^ 2 ^ j * k)) v = X') : (∀ χ ∈ hideChecks k hk hodd j N oP oH P gens, χ.Holds v) ↔ Introspection.AuxiliaryQuotient.hidingPauli P X (Y, Y', X')

The checks of the first hiding edge hold exactly when hidingPauli does, for registers read off the bit vector.

The constraints of the two orientations

noncomputable def MIPRE.Tailored.Intro.PauliHide.pauliHideCons (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) {ℓ : ℕ} (P : CL.CLFun CL.𝔽₂ (Fin (2 ^ 2 ^ j * k)) ℓ) (gens : List (Fin (2 ^ 2 ^ j * k) → CL.𝔽₂)) : List Cost.BitStr

The constraints of the first hiding edge, Pauli answer first: the Pauli answer has Q = 2^(2^j) k bits and the Hide answer 3Q.

Equations

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

noncomputable def MIPRE.Tailored.Intro.PauliHide.pauliHideConsRev (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) {ℓ : ℕ} (P : CL.CLFun CL.𝔽₂ (Fin (2 ^ 2 ^ j * k)) ℓ) (gens : List (Fin (2 ^ 2 ^ j * k) → CL.𝔽₂)) : List Cost.BitStr

The constraints of the first hiding edge, Hide answer first.

Equations

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

theorem MIPRE.Tailored.Intro.PauliHide.length_of_mem_pauliHideCons (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) {ℓ : ℕ} (P : CL.CLFun CL.𝔽₂ (Fin (2 ^ 2 ^ j * k)) ℓ) (gens : List (Fin (2 ^ 2 ^ j * k) → CL.𝔽₂)) {c : Cost.BitStr} (hc : c ∈ pauliHideCons k hk hodd j P gens) : List.length c = pauliLen (2 ^ j) k (QLD.Ty.pauli QLD.Bas.X) + 3 * (2 ^ 2 ^ j * k) + 1

theorem MIPRE.Tailored.Intro.PauliHide.length_of_mem_pauliHideConsRev (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) {ℓ : ℕ} (P : CL.CLFun CL.𝔽₂ (Fin (2 ^ 2 ^ j * k)) ℓ) (gens : List (Fin (2 ^ 2 ^ j * k) → CL.𝔽₂)) {c : Cost.BitStr} (hc : c ∈ pauliHideConsRev k hk hodd j P gens) : List.length c = 3 * (2 ^ 2 ^ j * k) + pauliLen (2 ^ j) k (QLD.Ty.pauli QLD.Bas.X) + 1

theorem MIPRE.Tailored.Intro.PauliHide.hide_regs {N : ℕ} {v : Fin N → ZMod 2} {oH Q : ℕ} {y y' x : Cost.BitStr} (h : PauliCons.Reads v oH (y ++ y' ++ x)) (hy : List.length y = Q) (hy' : List.length y' = Q) (hx : List.length x = Q) : (regAt N (oH + Q) Q) v = CL.ofBits Q y' ∧ (regAt N (oH + 2 * Q) Q) v = CL.ofBits Q x

The Hide registers read off a Hide answer at oH.

theorem MIPRE.Tailored.Intro.PauliHide.pauliHideCons_iff (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) {ℓ : ℕ} (P : CL.CLFun CL.𝔽₂ (Fin (2 ^ 2 ^ j * k)) ℓ) (gens : List (Fin (2 ^ 2 ^ j * k) → CL.𝔽₂)) (hgens : ∀ g ∈ gens, (Introspection.CLChecks.stageLinear P 0 0) g = 0) (hspan : ∀ (z : Fin (2 ^ 2 ^ j * k) → CL.𝔽₂), (Introspection.CLChecks.stageLinear P 0 0) z = 0 → z ∈ Submodule.span CL.𝔽₂ {g : Fin (2 ^ 2 ^ j * k) → CL.𝔽₂ | g ∈ gens}) (a y y' x : Cost.BitStr) (ha : List.length a = pauliLen (2 ^ j) k (QLD.Ty.pauli QLD.Bas.X)) (hy : List.length y = 2 ^ 2 ^ j * k) (hy' : List.length y' = 2 ^ 2 ^ j * k) (hx : List.length x = 2 ^ 2 ^ j * k) : (∀ c ∈ pauliHideCons k hk hodd j P gens, Satisfies c (a ++ (y ++ y' ++ x) ++ [true])) ↔ Introspection.AuxiliaryQuotient.hidingPauli P (Introspection.DecisionKernel.Answer.pauliProject (SAT.shoupSelfDualNormalBasis k hk hodd) (Introspection.DecisionKernel.Answer.pauliDecode (SAT.shoupBinField k hk) (2 ^ j) (Sum.inl (QLD.Ty.pauli QLD.Bas.X)) a)) (CL.ofBits (2 ^ 2 ^ j * k) y, CL.ofBits (2 ^ 2 ^ j * k) y', CL.ofBits (2 ^ 2 ^ j * k) x)

The first hiding edge as linear constraints, Pauli answer first.

theorem MIPRE.Tailored.Intro.PauliHide.pauliHideConsRev_iff (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) {ℓ : ℕ} (P : CL.CLFun CL.𝔽₂ (Fin (2 ^ 2 ^ j * k)) ℓ) (gens : List (Fin (2 ^ 2 ^ j * k) → CL.𝔽₂)) (hgens : ∀ g ∈ gens, (Introspection.CLChecks.stageLinear P 0 0) g = 0) (hspan : ∀ (z : Fin (2 ^ 2 ^ j * k) → CL.𝔽₂), (Introspection.CLChecks.stageLinear P 0 0) z = 0 → z ∈ Submodule.span CL.𝔽₂ {g : Fin (2 ^ 2 ^ j * k) → CL.𝔽₂ | g ∈ gens}) (a y y' x : Cost.BitStr) (ha : List.length a = pauliLen (2 ^ j) k (QLD.Ty.pauli QLD.Bas.X)) (hy : List.length y = 2 ^ 2 ^ j * k) (hy' : List.length y' = 2 ^ 2 ^ j * k) (hx : List.length x = 2 ^ 2 ^ j * k) : (∀ c ∈ pauliHideConsRev k hk hodd j P gens, Satisfies c (y ++ y' ++ x ++ a ++ [true])) ↔ Introspection.AuxiliaryQuotient.hidingPauli P (Introspection.DecisionKernel.Answer.pauliProject (SAT.shoupSelfDualNormalBasis k hk hodd) (Introspection.DecisionKernel.Answer.pauliDecode (SAT.shoupBinField k hk) (2 ^ j) (Sum.inl (QLD.Ty.pauli QLD.Bas.X)) a)) (CL.ofBits (2 ^ 2 ^ j * k) y, CL.ofBits (2 ^ 2 ^ j * k) y', CL.ofBits (2 ^ 2 ^ j * k) x)

The first hiding edge as linear constraints, Hide answer first.