The Hadamard assignment tester

An assignment tester Dinur, Definition 3.1 for a constraint C on the labels of the two ends of an edge checks, with a constant number of queries and a constant rejection rate, that two tables encode labels satisfying C. It is handed the tables and a proof; it accepts the encodings of satisfying labels together with an honest proof, and rejects every proof with probability at least a constant times the distance of the tables from the encodings of the closest satisfying labels. Running it on every edge of a constraint graph over a large alphabet reduces the alphabet to a constant one (PCP.ConstraintGraph.compose): for this, the number of queries and the rejection rate must not depend on the alphabet, however large the proof is.

The tester here, for constraints on labels in a finite type α, follows Arora and Barak Arora and Barak, Chapter 22 and is built on the Hadamard tester for quadratic equations (BitString.exists_forall_hadamardCode_tensor_eq_of_le_blrAcceptance).

• A label a is encoded by its long code BitString.longCode a, the dictator r ↦ r a on α → Bool, which is the Hadamard encoding of the unit vector of a. The long codes of distinct labels differ on half of the inputs, so a table within relative distance 1/4 of a long code determines its label (BitString.eq_of_hammingDist_longCode_lt).
• The labels σ : Fin 2 → α of the two ends are described by Boolean variables indexed by Fin 2 × α, their one-hot encoding HadamardTester.oneHot σ. The constraint becomes a system of quadratic equations in the variables (HadamardTester.equationCoeff): no two variables incompatible with C are both set, and an odd number of the variables of each end are set. Its solutions are the one-hot encodings of the labels satisfying C (HadamardTester.forall_hadamardCode_tensor_equationCoeff_iff). Reading the Hadamard encoding of the one-hot encoding at the vector that is r on the variables of an end and zero elsewhere (HadamardTester.endEmbed) reads the long code of the label of that end at r.
• The proof consists of a linear table, supposedly the Hadamard encoding of the variables, and a quadratic table, supposedly that of their tensor square. On independent random strings, the tester hadamardTester C runs five checks, each a local test (PCP.LocalTest): the linearity test on both tables, the tensor test, the equation test for the quadratic equations of C, and the input test, which compares the bit of the table of a random end at a random point with the self-corrected read of the linear table at the corresponding vector. It accepts when all five do, and makes 17 queries.

If the tester accepts with probability at least 1 - ρ for some ρ < 1/28, the linear table is within ρ of the Hadamard encoding of a solution of the equations, which is the one-hot encoding of labels satisfying C, and the input test puts the tables within distance 3ρ of the long codes of these labels (HadamardTester.exists_inputDist_le_of_le_acceptProb). So the tester rejects with probability at least 1/28 times the distance of the tables from the long codes of satisfying labels (HadamardTester.exists_inputDist_div_le_one_sub_acceptProb). As a constraint graph, over the alphabet Bool × (HadamardTester.Query → Bool) of 2 ^ 18 symbols, it is an assignment tester in the sense of Dinur: a labelling violates a proportion of the edges at least 1/476 times that distance (HadamardTester.exists_inputDist_div_le_unsatFrac).

Main definitions

• Cslib.PCP.HadamardTester.oneHot: the one-hot encoding of the labels of the two ends.
• Cslib.PCP.HadamardTester.equationCoeff, Cslib.PCP.HadamardTester.equationRhs: the quadratic equations of a constraint.
• Cslib.PCP.HadamardTester.blrTest, Cslib.PCP.HadamardTester.tensorTest, Cslib.PCP.HadamardTester.equationTest, Cslib.PCP.HadamardTester.inputTest: the checks of the tester, as local tests.
• Cslib.PCP.hadamardTester: the assignment tester of a constraint.
• Cslib.PCP.HadamardTester.inputDist: the distance of the tables of a proof from the long codes of labels.
• Cslib.PCP.HadamardTester.honestProof: the proof of satisfying labels.

Main results

• Cslib.PCP.HadamardTester.forall_hadamardCode_tensor_equationCoeff_iff: the solutions of the quadratic equations of a constraint are the one-hot encodings of its satisfying labels.
• Cslib.PCP.HadamardTester.passes_honestProof: completeness of the tester.
• Cslib.PCP.HadamardTester.exists_inputDist_le_of_le_acceptProb, Cslib.PCP.HadamardTester.exists_inputDist_div_le_one_sub_acceptProb, Cslib.PCP.HadamardTester.one_div_le_one_sub_acceptProb_of_forall_not: soundness of the tester.
• Cslib.PCP.HadamardTester.satisfies_toConstraintGraph_honestProof, Cslib.PCP.HadamardTester.exists_inputDist_div_le_unsatFrac, Cslib.PCP.HadamardTester.one_div_le_unsatFrac_of_forall_not: completeness and soundness of the tester as a constraint graph.

References

• I. Dinur, The PCP theorem by gap amplification
• I. Dinur, The PCP theorem by gap amplification, ECCC TR05-046, revision 1
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

The one-hot encoding and the quadratic equations of a constraint

def Cslib.PCP.HadamardTester.oneHot {α : Type u_1} [DecidableEq α] (σ : Fin 2 → α) : Fin 2 × α → Bool

The one-hot encoding of the labels σ : Fin 2 → α of the two ends of an edge, as Boolean variables indexed by Fin 2 × α: the variable (b, a) is set exactly when the end b has the label a.

@[simp]

theorem Cslib.PCP.HadamardTester.oneHot_apply {α : Type u_1} [DecidableEq α] (σ : Fin 2 → α) (p : Fin 2 × α) : oneHot σ p = decide (σ p.1 = p.2)

def Cslib.PCP.HadamardTester.Compatible {α : Type u_1} (C : α → α → Prop) (p p' : Fin 2 × α) : Prop

Two variables, given by an end and a label, are compatible with the constraint C when some labels satisfying C set both of them.

noncomputable def Cslib.PCP.HadamardTester.equationCoeff {α : Type u_1} [Fintype α] [DecidableEq α] (C : α → α → Prop) : (Fin 2 × α) × Fin 2 × α ⊕ Fin 2 → (Fin 2 × α) × Fin 2 × α → Bool

The coefficients of the quadratic equations of the constraint C in the variables x, as linear equations hadamardCode (tensor x x) (equationCoeff C e) = equationRhs e in the tensor square of the variables: for every pair of variables incompatible with C (inl), the equation saying that they are not both set, and for every end (inr), the equation saying that an odd number of its variables are set. Their solutions are the one-hot encodings of the labels satisfying C (forall_hadamardCode_tensor_equationCoeff_iff).

def Cslib.PCP.HadamardTester.equationRhs {α : Type u_1} : (Fin 2 × α) × Fin 2 × α ⊕ Fin 2 → Bool

The right-hand sides of the quadratic equations of a constraint: 0 for the pairs of variables, 1 for the ends.

theorem Cslib.PCP.HadamardTester.forall_hadamardCode_tensor_equationCoeff_iff {α : Type u_1} [Fintype α] [DecidableEq α] {C : α → α → Prop} {x : Fin 2 × α → Bool} : (∀ (e : (Fin 2 × α) × Fin 2 × α ⊕ Fin 2), BitString.hadamardCode (BitString.tensor x x) (equationCoeff C e) = equationRhs e) ↔ ∃ (σ : Fin 2 → α), C (σ 0) (σ 1) ∧ x = oneHot σ

The quadratic equations of a constraint: their solutions are exactly the one-hot encodings of the labels satisfying the constraint.

def Cslib.PCP.HadamardTester.endEmbed {α : Type u_1} (b : Fin 2) (r : α → Bool) : Fin 2 × α → Bool

The assignment of the variables that is r on the variables of the end b and zero on those of the other end.

The checks, as local tests

def Cslib.PCP.HadamardTester.blrTest (ι : Type u_2) : LocalTest (ι → Bool) ((ι → Bool) × (ι → Bool)) (Fin 3) Bool

The linearity test of Blum, Luby and Rubinfeld, as a local test on a table f : (ι → Bool) → Bool: on the random string (x, y), it reads f at x, y and x + y, and accepts when (f x ^^ f y) = f (x + y).

def Cslib.PCP.HadamardTester.tensorTest (ι : Type u_2) : LocalTest ((ι → Bool) ⊕ (ι × ι → Bool)) ((ι → Bool) × (ι → Bool) × (ι → Bool) × (ι → Bool) × (ι × ι → Bool)) (Fin 6) Bool

The tensor test, as a local test on the pair of tables Sum.elim f g: on the random string (y, z, r, s, t), it compares the self-corrected read of g at tensor y z with randomness t with the product of the self-corrected reads of f at y and z with randomnesses r and s.

def Cslib.PCP.HadamardTester.equationTest {ι : Type u_2} {κ : Type u_3} [Fintype κ] (A : κ → ι → Bool) (b : κ → Bool) : LocalTest (ι → Bool) ((κ → Bool) × (ι → Bool)) (Fin 2) Bool

The equation test for the linear equations hadamardCode w (A e) = b e, as a local test on a table g : (ι → Bool) → Bool: on the random string (k, t), it compares the self-corrected read of g at the sum of the A e with k e set, with randomness t, with the sum of the b e with k e set.

def Cslib.PCP.HadamardTester.inputTest (α : Type u_1) : LocalTest (Fin 2 × (α → Bool) ⊕ (Fin 2 × α → Bool)) (Fin 2 × (α → Bool) × (Fin 2 × α → Bool)) (Fin 3) Bool

The input test, as a local test on the tables of the two ends and the linear table, Sum.elim (fun p ↦ T p.1 p.2) f: on the random string (b, r, y), it compares the bit of the table T b at r with the self-corrected read of f at endEmbed b r with randomness y.

The tester

@[reducible, inline]

abbrev Cslib.PCP.HadamardTester.LinPos (α : Type u_1) : Type u_1

The assignments of the variables Fin 2 × α: the positions of the linear table, and the random strings of its checks.

@[reducible, inline]

abbrev Cslib.PCP.HadamardTester.QuadPos (α : Type u_1) : Type u_1

The assignments of the pairs of variables: the positions of the quadratic table, and the random strings of its checks.

@[reducible, inline]

abbrev Cslib.PCP.HadamardTester.EqnRand (α : Type u_1) : Type u_1

The random strings of the equation test: the sets of quadratic equations of a constraint.

@[instance_reducible]

instance Cslib.PCP.HadamardTester.LinPos.instFintype {α : Type u_1} [Fintype α] [DecidableEq α] : Fintype (LinPos α)

@[instance_reducible]

instance Cslib.PCP.HadamardTester.QuadPos.instFintype {α : Type u_1} [Fintype α] [DecidableEq α] : Fintype (QuadPos α)

@[instance_reducible]

instance Cslib.PCP.HadamardTester.EqnRand.instFintype {α : Type u_1} [Fintype α] [DecidableEq α] : Fintype (EqnRand α)

@[reducible, inline]

abbrev Cslib.PCP.HadamardTester.Pos (α : Type u_1) : Type u_1

The positions of the proofs read by the tester for constraints on labels in α: the bit inl (b, r) of the table of the end b at r, the bit inr (inl y) of the linear table at y, and the bit inr (inr z) of the quadratic table at z.

@[reducible, inline]

abbrev Cslib.PCP.HadamardTester.Rand (α : Type u_1) : Type u_1

The random strings of the tester: those of its five checks.

@[instance_reducible]

instance Cslib.PCP.HadamardTester.instFintypeRand {α : Type u_1} [Fintype α] [DecidableEq α] : Fintype (Rand α)

The random strings of the tester are finitely many.

@[reducible, inline]

abbrev Cslib.PCP.HadamardTester.Query : Type

The queries of the tester: three for each linearity test, six for the tensor test, two for the equation test and three for the input test.

theorem Cslib.PCP.HadamardTester.card_query : Fintype.card Query = 17

The tester makes 17 queries.

theorem Cslib.PCP.HadamardTester.card_rand {α : Type u_1} [Fintype α] [DecidableEq α] : Fintype.card (Rand α) = 2 ^ (20 * Fintype.card α ^ 2 + 15 * Fintype.card α + 3)

The tester uses 20 k² + 15 k + 3 random bits, for k labels.

def Cslib.PCP.HadamardTester.inputTable {α : Type u_1} (π : Pos α → Bool) (b : Fin 2) : (α → Bool) → Bool

The table of the end b carried by the proof π.

noncomputable def Cslib.PCP.hadamardTester {α : Type u_1} [Fintype α] [DecidableEq α] (C : α → α → Prop) : LocalTest (HadamardTester.Pos α) (HadamardTester.Rand α) HadamardTester.Query Bool

The Hadamard assignment tester of the constraint C on labels in α Arora and Barak, Chapter 22: on independent random strings, the linearity test on the linear and on the quadratic table, the tensor test, the equation test for the quadratic equations of C, and the input test; it accepts when all five accept.

Soundness

noncomputable def Cslib.PCP.HadamardTester.inputDist {α : Type u_1} [Fintype α] [DecidableEq α] (π : Pos α → Bool) (σ : Fin 2 → α) : ℝ

The distance of the tables of the proof π from the long codes of the labels σ: the relative Hamming distance of the table of an end from the long code of its label, averaged over the two ends. It is the proportion of the positions of the two tables at which π differs from the long codes.

theorem Cslib.PCP.HadamardTester.inputDist_nonneg {α : Type u_1} [Fintype α] [DecidableEq α] (π : Pos α → Bool) (σ : Fin 2 → α) : 0 ≤ inputDist π σ

theorem Cslib.PCP.HadamardTester.inputDist_le_one {α : Type u_1} [Fintype α] [DecidableEq α] (π : Pos α → Bool) (σ : Fin 2 → α) : inputDist π σ ≤ 1

theorem Cslib.PCP.HadamardTester.hammingDist_inputTable_div_le {α : Type u_1} [Fintype α] [DecidableEq α] (π : Pos α → Bool) (σ : Fin 2 → α) (b : Fin 2) : ↑(hammingDist (inputTable π b) (BitString.longCode (σ b))) / 2 ^ Fintype.card α ≤ 2 * inputDist π σ

The distance of each table from the long code of its label is at most twice the distance of the tables.

theorem Cslib.PCP.HadamardTester.exists_inputDist_le_of_le_acceptProb {α : Type u_1} [Fintype α] [DecidableEq α] {C : α → α → Prop} {π : Pos α → Bool} {ρ : ℝ} (hρ : ρ < 1 / 28) (h : 1 - ρ ≤ (hadamardTester C).acceptProb π) : ∃ (σ : Fin 2 → α), C (σ 0) (σ 1) ∧ inputDist π σ ≤ 3 * ρ

Soundness of the Hadamard assignment tester: if the tester of C accepts the proof π with probability at least 1 - ρ for some ρ < 1/28, then the tables of π are within distance 3ρ of the long codes of labels satisfying C. The linearity tests decode the linear and the quadratic table to x and w; the tensor test forces w to be the tensor square of x, and the equation test makes x a solution of the equations of C, hence the one-hot encoding of satisfying labels; the input test then compares the tables with their long codes.

theorem Cslib.PCP.HadamardTester.exists_inputDist_div_le_one_sub_acceptProb {α : Type u_1} [Fintype α] [DecidableEq α] {C : α → α → Prop} (hC : ∃ (a : α) (b : α), C a b) (π : Pos α → Bool) : ∃ (σ : Fin 2 → α), C (σ 0) (σ 1) ∧ inputDist π σ / 28 ≤ 1 - (hadamardTester C).acceptProb π

Soundness of the Hadamard assignment tester Dinur, Definition 3.1: if the constraint C is satisfiable, the tester of C rejects every proof with probability at least 1/28 times the distance of its tables from the long codes of some labels satisfying C.

theorem Cslib.PCP.HadamardTester.one_div_le_one_sub_acceptProb_of_forall_not {α : Type u_1} [Fintype α] [DecidableEq α] {C : α → α → Prop} (hC : ∀ (a b : α), ¬C a b) (π : Pos α → Bool) : 1 / 28 ≤ 1 - (hadamardTester C).acceptProb π

Soundness of the Hadamard assignment tester for an unsatisfiable constraint: the tester rejects every proof with probability at least 1/28.

Completeness

def Cslib.PCP.HadamardTester.honestProof {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Fin 2 → α) : Pos α → Bool

The honest proof for the labels σ: the long codes of the labels as the tables of the ends, and the Hadamard encodings of their one-hot encoding and of its tensor square as the linear and the quadratic table.

@[simp]

theorem Cslib.PCP.HadamardTester.inputDist_honestProof {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Fin 2 → α) : inputDist (honestProof σ) σ = 0

The tables of the honest proof for σ are the long codes of σ.

theorem Cslib.PCP.HadamardTester.passes_honestProof {α : Type u_1} [Fintype α] [DecidableEq α] {C : α → α → Prop} {σ : Fin 2 → α} (hσ : C (σ 0) (σ 1)) (ω : Rand α) : (hadamardTester C).Passes (honestProof σ) ω

Completeness of the Hadamard assignment tester: the honest proof for labels satisfying the constraint passes on every random string.

theorem Cslib.PCP.HadamardTester.acceptProb_honestProof {α : Type u_1} [Fintype α] [DecidableEq α] {C : α → α → Prop} {σ : Fin 2 → α} (hσ : C (σ 0) (σ 1)) : (hadamardTester C).acceptProb (honestProof σ) = 1

Completeness of the Hadamard assignment tester: the honest proof for labels satisfying the constraint is accepted with probability one.

The tester as a constraint graph

theorem Cslib.PCP.HadamardTester.satisfies_toConstraintGraph_honestProof {α : Type u_1} [Fintype α] [DecidableEq α] {C : α → α → Prop} {σ : Fin 2 → α} (hσ : C (σ 0) (σ 1)) (γ : Bool) (x : Rand α × Query) : (hadamardTester C).toConstraintGraph.Satisfies ((hadamardTester C).labellingOf (honestProof σ) γ) x

Completeness of the tester as a constraint graph Dinur, Definition 3.1: for labels satisfying the constraint, the labelling of the constraint graph of the tester by the honest proof, whose positions of the tables carry the long codes of the labels, satisfies every edge.

theorem Cslib.PCP.HadamardTester.exists_inputDist_div_le_unsatFrac {α : Type u_1} [Fintype α] [DecidableEq α] {C : α → α → Prop} (hC : ∃ (a : α) (b : α), C a b) (A : Pos α ⊕ Rand α → Bool × (Query → Bool)) : ∃ (σ : Fin 2 → α), C (σ 0) (σ 1) ∧ inputDist (LocalTest.proofOf A) σ / 476 ≤ (hadamardTester C).toConstraintGraph.unsatFrac A

Soundness of the tester as a constraint graph Dinur, Definition 3.1: if the constraint C is satisfiable, every labelling of the constraint graph of the tester violates a proportion of the edges at least 1/476 times the distance of the tables it carries from the long codes of some labels satisfying C.

theorem Cslib.PCP.HadamardTester.one_div_le_unsatFrac_of_forall_not {α : Type u_1} [Fintype α] [DecidableEq α] {C : α → α → Prop} (hC : ∀ (a b : α), ¬C a b) (A : Pos α ⊕ Rand α → Bool × (Query → Bool)) : 1 / 476 ≤ (hadamardTester C).toConstraintGraph.unsatFrac A

Soundness of the tester as a constraint graph for an unsatisfiable constraint: every labelling violates a proportion at least 1/476 of the edges.