Constraints on registers read off windows

The introspection verifier's hiding checks compare registers x : Fin s → 𝔽₂ — the duals and tails of Read and Hide answers — through projections onto coordinate sets and through the dual maps registerDual L, with the sets and the maps computed from the readable register. In the padded layout a register is a window of an answer (toBits x at a known offset). This file writes such comparisons as linear constraints:

• dotL_toBits: the inner product of two windows is the 𝔽₂ sum ∑ wᵢ xᵢ;
• projEqCons, projEqCons_iff: the constraints xᵢ = yᵢ for i ∈ S, holding exactly when proj S x = proj S y;
• dualCons, dualCons_iff: for a list of vectors spanning the kernel of L, the constraints ∑ᵢ zᵢ (proj S (x - y))ᵢ = 0, holding exactly when registerDual L x = registerDual L y (AuxiliaryDual.registerDual_eq_iff_dot).

Inner products of registers

theorem MIPRE.Tailored.Intro.decide_add_eq_one (u v : CL.𝔽₂) : decide (u + v = 1) = (decide (u = 1) ^^ decide (v = 1))

theorem MIPRE.Tailored.Intro.decide_mul_eq_one (u v : CL.𝔽₂) : decide (u * v = 1) = (decide (u = 1) && decide (v = 1))

theorem MIPRE.Tailored.Intro.dotL_toBits {s : ℕ} (w x : Fin s → CL.𝔽₂) : dotL (CL.toBits w) (CL.toBits x) = decide (∑ i : Fin s, w i * x i = 1)

The inner product of two windows is the 𝔽₂ sum.

def MIPRE.Tailored.Intro.regForm {s : ℕ} (n o : ℕ) (w : Fin s → CL.𝔽₂) : Cost.BitStr

A register-level linear form, placed at an offset.

Equations

• MIPRE.Tailored.Intro.regForm n o w = MIPRE.Tailored.Intro.place n o (MIPRE.CL.toBits w)

theorem MIPRE.Tailored.Intro.length_regForm {s n o : ℕ} (w : Fin s → CL.𝔽₂) (h : o + s ≤ n) : List.length (regForm n o w) = n

theorem MIPRE.Tailored.Intro.dotL_regForm {s n o : ℕ} {w x : Fin s → CL.𝔽₂} {a : Cost.BitStr} (h : o + s ≤ n) (ha : List.length a = n) (hx : List.take s (List.drop o a) = CL.toBits x) : dotL (regForm n o w) a = decide (∑ i : Fin s, w i * x i = 1)

theorem MIPRE.Tailored.Intro.satisfies_regForms_iff {s la lb oa ob : ℕ} {a b : Cost.BitStr} (ha : List.length a = la) (hb : List.length b = lb) (hoa : oa + s ≤ la) (hob : ob + s ≤ lb) {x y wa wb : Fin s → CL.𝔽₂} (hx : List.take s (List.drop oa a) = CL.toBits x) (hy : List.take s (List.drop ob b) = CL.toBits y) (γ : Bool) : Satisfies (regForm la oa wa ++ regForm lb ob wb ++ [γ]) (a ++ b ++ [true]) ↔ decide (∑ i : Fin s, wa i * x i + ∑ i : Fin s, wb i * y i = 1) = γ

A constraint between two registers, read: ∑ wa·x + ∑ wb·y = γ.

Equality on a coordinate set

def MIPRE.Tailored.Intro.projEqCons {s : ℕ} (la lb oa ob : ℕ) (S : Finset (Fin s)) : List Cost.BitStr

The constraints xᵢ = yᵢ for i ∈ S, the registers at offsets oa of a, ob of b, in increasing order of i.

Equations

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

theorem MIPRE.Tailored.Intro.sum_single_mul {s : ℕ} (i : Fin s) (x : Fin s → CL.𝔽₂) : ∑ j : Fin s, Pi.single i 1 j * x j = x i

theorem MIPRE.Tailored.Intro.projEqCons_iff {s la lb oa ob : ℕ} {a b : Cost.BitStr} (ha : List.length a = la) (hb : List.length b = lb) (hoa : oa + s ≤ la) (hob : ob + s ≤ lb) {x y : Fin s → CL.𝔽₂} (hx : List.take s (List.drop oa a) = CL.toBits x) (hy : List.take s (List.drop ob b) = CL.toBits y) (S : Finset (Fin s)) : (∀ c ∈ projEqCons la lb oa ob S, Satisfies c (a ++ b ++ [true])) ↔ (CL.proj S) x = (CL.proj S) y

The coordinate-set equality constraints hold exactly when the projections agree.

Equality of duals

def MIPRE.Tailored.Intro.dualCons {s : ℕ} (la lb oa ob : ℕ) (S : Finset (Fin s)) (gens : List (Fin s → CL.𝔽₂)) : List Cost.BitStr

The constraints ∑ᵢ zᵢ (proj S (x - y))ᵢ = 0 for z in a list.

Equations

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

theorem MIPRE.Tailored.Intro.sum_proj_mul {s : ℕ} (S : Finset (Fin s)) (z x : Fin s → CL.𝔽₂) : ∑ i : Fin s, (CL.proj S) z i * x i = ∑ i : Fin s, z i * (CL.proj S) x i

theorem MIPRE.Tailored.Intro.dualCons_iff {s la lb oa ob : ℕ} {a b : Cost.BitStr} (ha : List.length a = la) (hb : List.length b = lb) (hoa : oa + s ≤ la) (hob : ob + s ≤ lb) {x y : Fin s → CL.𝔽₂} (hx : List.take s (List.drop oa a) = CL.toBits x) (hy : List.take s (List.drop ob b) = CL.toBits y) {S : Finset (Fin s)} (L : CL.RegLinear CL.𝔽₂ S) (gens : List (Fin s → CL.𝔽₂)) (hgens : ∀ g ∈ gens, L g = 0) (hspan : ∀ (z : Fin s → CL.𝔽₂), L z = 0 → z ∈ Submodule.span CL.𝔽₂ {g : Fin s → CL.𝔽₂ | g ∈ gens}) : (∀ c ∈ dualCons la lb oa ob S gens, Satisfies c (a ++ b ++ [true])) ↔ (Introspection.AuxiliaryDual.registerDual L) x = (Introspection.AuxiliaryDual.registerDual L) y

The dual equality constraints, for a list of vectors of the kernel of L spanning it, hold exactly when the duals agree.