Linear checks on answer bits, and their constraint vectors

A tailored game's constraint is a bit vector c of length N + 1, satisfied by the answer bits z of length N when ⟨c, (z, 1)⟩ = 0 (MIPRE.Tailored.Satisfies). This file produces such vectors from linear checks: an F₂-linear functional φ on F₂^N and a target c, read as the equation φ(z) = c. The constraint of a check (LinCheck.toCon) lists the values of φ on the unit vectors, then c; satisfies_toCon_iff is the statement that it is satisfied exactly when φ(z) = c. So a decision procedure that is a conjunction of affine equations in the answer bits becomes a constraint list by writing down the functionals, with no coefficient bookkeeping: the coefficients are whatever the functional gives on the unit vectors, which a program computes by evaluating the check at those vectors.

The functionals are built from two readers: getv l, the bit at position l, and, for the effective binary field shoupBinField k hk, fldAt o, the field element whose canonical k bits start at position o (MIPRE.SAT.shoupCoordinateEquiv, under which toBits is F₂-linear). An equation E(z) = κ between field elements, E an F₂-linear map to the field, is the k checks of its coordinates (fieldChecks, forall_fieldChecks_iff).

reject is the check 0 = 1, whose constraint is rejectConstraint N.

structure MIPRE.Tailored.Intro.LinCheck (N : ℕ) : Type

A linear check on N answer bits: the equation φ(z) = c over F₂.

• φ : (Fin N → ZMod 2) →ₗ[ZMod 2] ZMod 2

  The linear part.

• c : ZMod 2

  The target.

def MIPRE.Tailored.Intro.bitVec (N : ℕ) (z : Cost.BitStr) : Fin N → ZMod 2

The answer bits as a vector of F₂^N (bits beyond the string read 0).

Equations

• MIPRE.Tailored.Intro.bitVec N z l = MIPRE.LowDegree.ofBool (List.getD z (↑l) false)

def MIPRE.Tailored.Intro.LinCheck.Holds {N : ℕ} (χ : LinCheck N) (v : Fin N → ZMod 2) : Prop

The check holds at a vector.

Equations

• χ.Holds v = (χ.φ v = χ.c)

def MIPRE.Tailored.Intro.LinCheck.toCon {N : ℕ} (χ : LinCheck N) : Cost.BitStr

The constraint vector of a check: the functional on the unit vectors, then the target.

Equations

• χ.toCon = (List.ofFn fun (l : Fin N) => MIPRE.LowDegree.BinaryLinear.bit (χ.φ fun (j : Fin N) => if l = j then 1 else 0)) ++ [MIPRE.LowDegree.BinaryLinear.bit χ.c]

@[simp]

theorem MIPRE.Tailored.Intro.LinCheck.length_toCon {N : ℕ} (χ : LinCheck N) : List.length χ.toCon = N + 1

def MIPRE.Tailored.Intro.LinCheck.reject (N : ℕ) : LinCheck N

The check 0 = 1, which no vector satisfies.

Equations

• MIPRE.Tailored.Intro.LinCheck.reject N = { φ := 0, c := 1 }

theorem MIPRE.Tailored.Intro.LinCheck.not_holds_reject {N : ℕ} (v : Fin N → ZMod 2) : ¬(reject N).Holds v

@[simp]

theorem MIPRE.Tailored.Intro.LinCheck.holds_reject {N : ℕ} (v : Fin N → ZMod 2) : (reject N).Holds v ↔ False

theorem MIPRE.Tailored.Intro.LinCheck.toCon_reject {N : ℕ} : (reject N).toCon = rejectConstraint N

theorem MIPRE.Tailored.Intro.ofBool_dotBit {n : ℕ} (α a : Fin n → Bool) : LowDegree.ofBool (dotBit α a) = ∑ i : Fin n, LowDegree.ofBool (a i) * LowDegree.ofBool (α i)

theorem MIPRE.Tailored.Intro.satisfies_toCon_iff {N : ℕ} (χ : LinCheck N) (z : Cost.BitStr) (hz : List.length z = N) : Satisfies χ.toCon (z ++ [true]) ↔ χ.Holds (bitVec N z)

The constraint of a check is satisfied exactly when the check holds.

Readers

def MIPRE.Tailored.Intro.getv (N l : ℕ) : (Fin N → ZMod 2) →ₗ[ZMod 2] ZMod 2

The bit at position l, 0 beyond N.

Equations

• MIPRE.Tailored.Intro.getv N l = if h : l < N then LinearMap.proj ⟨l, h⟩ else 0

theorem MIPRE.Tailored.Intro.getv_bitVec {N : ℕ} (z : Cost.BitStr) (hz : List.length z ≤ N) (l : ℕ) : (getv N l) (bitVec N z) = LowDegree.ofBool (List.getD z l false)

noncomputable def MIPRE.Tailored.Intro.fldAt (k : ℕ) (hk : 1 ≤ k) (N o : ℕ) : (Fin N → ZMod 2) →ₗ[ZMod 2] (SAT.shoupBinField k hk).carrier

The field element whose canonical bits start at position o.

Equations

• MIPRE.Tailored.Intro.fldAt k hk N o = ↑(MIPRE.SAT.shoupCoordinateEquiv k hk).symm ∘ₗ LinearMap.pi fun (i : Fin k) => MIPRE.Tailored.Intro.getv N (o + ↑i)

theorem MIPRE.Tailored.Intro.fldAt_eq {k : ℕ} {hk : 1 ≤ k} {N o : ℕ} (v : Fin N → ZMod 2) (x : (SAT.shoupBinField k hk).carrier) (h : ∀ i < k, (getv N (o + i)) v = LowDegree.ofBool (List.getD ((SAT.shoupBinField k hk).toBits x) i false)) : (fldAt k hk N o) v = x

fldAt o reads the field element x when the bits from o on are those of x.

noncomputable def MIPRE.Tailored.Intro.fieldChecks (k : ℕ) (hk : 1 ≤ k) {N : ℕ} (E : (Fin N → ZMod 2) →ₗ[ZMod 2] (SAT.shoupBinField k hk).carrier) (κ : (SAT.shoupBinField k hk).carrier) : List (LinCheck N)

The k coordinate checks of the field equation E(z) = κ.

Equations

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

theorem MIPRE.Tailored.Intro.forall_fieldChecks_iff {k : ℕ} {hk : 1 ≤ k} {N : ℕ} (E : (Fin N → ZMod 2) →ₗ[ZMod 2] (SAT.shoupBinField k hk).carrier) (κ : (SAT.shoupBinField k hk).carrier) (v : Fin N → ZMod 2) : (∀ χ ∈ fieldChecks k hk E κ, χ.Holds v) ↔ E v = κ

The coordinate checks hold exactly when the field equation does.