Binary subset sums of modular matrix rows

Uniform modular matrices give two-universal hashing of one binary row, for every positive modulus. Many independent binary rows may use the same public matrix, with a statistical-distance loss linear in their count. No whole-matrix universality or pointwise assertion about a fixed matrix is needed.

Main results

• Cslib.BitString.SubsetSum.uniform_vecMul_sub: distinct rows give a uniform difference.
• Cslib.BitString.SubsetSum.vecMul_collision_probability: exact modular collision probability.
• Cslib.BitString.SubsetSum.dist_mul_le: the joint bound with the entire public matrix retained.

References

• [C. Gentry, A. Sahai and B. Waters, Homomorphic Encryption from Learning with Errors: Conceptually-Simpler, Asymptotically-Faster, Attribute-Based, Section 3.2] [GSW13]

theorem Cslib.BitString.SubsetSum.hash_eq_vecMul {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [Fintype ι] [Ring R] (A : ι → κ → R) (r : ι → Bool) : hash A r = Matrix.vecMul (fun (i : ι) => ↑(r i).toNat) (Matrix.of A)

Modular multiplication by a binary row is a subset sum of the matrix rows.

theorem Cslib.BitString.SubsetSum.hashRows_eq_mul {ι : Type u_1} {κ : Type u_2} {ρ : Type u_3} {R : Type u_4} [Fintype ι] [Ring R] (A : ι → κ → R) (r : ρ → ι → Bool) : hashRows A r = ((Matrix.of r).map fun (bit : Bool) => ↑bit.toNat) * Matrix.of A

Multiplication by a binary matrix applies the same subset-sum hash to every row.

theorem Cslib.BitString.SubsetSum.uniform_vecMul_sub {q m d : ℕ} [NeZero q] (x y : Fin m → Bool) (hxy : x ≠ y) : PMF.map (fun (A : Matrix (Fin m) (Fin d) (ZMod q)) => Matrix.vecMul (fun (i : Fin m) => ↑(x i).toNat) A - Matrix.vecMul (fun (i : Fin m) => ↑(y i).toNat) A) (Probability.PMF.uniformOfFintype (Matrix (Fin m) (Fin d) (ZMod q))) = Probability.PMF.uniformOfFintype (Fin d → ZMod q)

For distinct binary rows, their modular-product difference is uniform for any positive q.

theorem Cslib.BitString.SubsetSum.vecMul_collision_probability {q m d : ℕ} [NeZero q] (x y : Fin m → Bool) (hxy : x ≠ y) : (∑ A : Matrix (Fin m) (Fin d) (ZMod q), if Matrix.vecMul (fun (i : Fin m) => ↑(x i).toNat) A = Matrix.vecMul (fun (i : Fin m) => ↑(y i).toNat) A then ((Probability.PMF.uniformOfFintype (Matrix (Fin m) (Fin d) (ZMod q))) A).toReal else 0) = (↑q ^ d)⁻¹

Binary rows collide modulo q with probability exactly 1 / q^d, without primality.

theorem Cslib.BitString.SubsetSum.dist_mul_le {q m d : ℕ} [NeZero q] {Rows : Type u_5} [Fintype Rows] [DecidableEq Rows] : dist ((Probability.PMF.uniformOfFintype (Matrix (Fin m) (Fin d) (ZMod q))).bind fun (A : Matrix (Fin m) (Fin d) (ZMod q)) => PMF.map (fun (r : Matrix Rows (Fin m) Bool) => (A, (r.map fun (bit : Bool) => ↑bit.toNat) * A)) (Probability.PMF.uniformOfFintype (Matrix Rows (Fin m) Bool))) ((Probability.PMF.uniformOfFintype (Matrix (Fin m) (Fin d) (ZMod q))).bind fun (A : Matrix (Fin m) (Fin d) (ZMod q)) => PMF.map (fun (x : Matrix Rows (Fin d) (ZMod q)) => (A, x)) (Probability.PMF.uniformOfFintype (Matrix Rows (Fin d) (ZMod q)))) ≤ ↑(Fintype.card Rows) * √(↑q ^ d / 2 ^ m) / 2

Independent binary rows share one uniform public matrix. The comparison retains that matrix; the replacement modular matrix is independent of it.