Binary gadgets for GSW encryption

Residues modulo 2 ^ w decompose into exactly w bits, ordered from least to most significant. The expanded coordinate type is ι × Fin w: the original coordinate comes first. Recomposition accepts arbitrary modular entries, while decomposition and flattening return Boolean matrices. The same bitMatrix lift interprets these bits in the modular computation and in integer noise witnesses.

These are the row operations from Gentry, Sahai and Waters, Sections 2.3 and 3.1. The paper uses ⌊log₂ q⌋ + 1 digits for a general modulus q. For q = 2 ^ w, its last digit is redundant; this module uses the minimal w digits. Width zero is allowed: its residue ring is ZMod 1, and its expanded coordinate type is empty.

Main definitions

• bitDecomp, bitCompose, powersOfTwo: the binary row operations.
• bitMatrix: interpret a Boolean matrix in a type with natural-number casts.
• decomposeMatrix, recomposeMatrix, flattenMatrix: apply the row operations to matrices.

Main results

• recomposeMatrix_decomposeMatrix: recomposition recovers every modular matrix.
• decomposeMatrix_mulVec: decomposition preserves multiplication by the expanded secret.
• flattenMatrix_mulVec: flattening preserves that multiplication on arbitrary modular inputs.
• recomposeMatrix_flattenMatrix: flattening preserves recomposition.
• recomposeMatrix_sub, recomposeMatrix_mul: row recomposition commutes with subtraction and left matrix multiplication, as used by serialized NAND.

References

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

def Cslib.Crypto.Homomorphic.GSW.bitDecomp {ι : Type u_1} (w : ℕ) (v : ι → ZMod (2 ^ w)) : ι × Fin w → Bool

The least-significant-first digits of each residue.

def Cslib.Crypto.Homomorphic.GSW.bitCompose {ι : Type u_1} (w : ℕ) (v : ι × Fin w → ZMod (2 ^ w)) : ι → ZMod (2 ^ w)

Recompose a row of arbitrary modular coefficients with binary place values.

def Cslib.Crypto.Homomorphic.GSW.powersOfTwo {ι : Type u_1} (w : ℕ) (s : ι → ZMod (2 ^ w)) : ι × Fin w → ZMod (2 ^ w)

Expand each secret coordinate by its binary place values.

def Cslib.Crypto.Homomorphic.GSW.bitMatrix {ρ : Type u_2} {κ : Type u_3} (R : Type u_4) [NatCast R] (C : Matrix ρ κ Bool) : Matrix ρ κ R

Interpret the same Boolean entries as zero or one in the chosen coefficient type.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.bitMatrix_apply {ρ : Type u_2} {κ : Type u_3} (R : Type u_4) [NatCast R] (C : Matrix ρ κ Bool) (i : ρ) (j : κ) : bitMatrix R C i j = ↑(C i j).toNat

def Cslib.Crypto.Homomorphic.GSW.decomposeMatrix {ι : Type u_1} {ρ : Type u_2} (w : ℕ) (A : Matrix ρ ι (ZMod (2 ^ w))) : Matrix ρ (ι × Fin w) Bool

Decompose each row, retaining the original row index and expanding its column index.

def Cslib.Crypto.Homomorphic.GSW.recomposeMatrix {ι : Type u_1} {ρ : Type u_2} (w : ℕ) (C : Matrix ρ (ι × Fin w) (ZMod (2 ^ w))) : Matrix ρ ι (ZMod (2 ^ w))

Recompose each row of an arbitrary modular matrix.

def Cslib.Crypto.Homomorphic.GSW.flattenMatrix {ι : Type u_1} {ρ : Type u_2} (w : ℕ) (C : Matrix ρ (ι × Fin w) (ZMod (2 ^ w))) : Matrix ρ (ι × Fin w) Bool

Normalize arbitrary modular rows to Boolean rows by recomposing and decomposing.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.bitCompose_bitDecomp {ι : Type u_1} (w : ℕ) (v : ι → ZMod (2 ^ w)) : (bitCompose w fun (j : ι × Fin w) => ↑(bitDecomp w v j).toNat) = v

Recomposition recovers a row from its actual binary digits.

theorem Cslib.Crypto.Homomorphic.GSW.bitCompose_add {ι : Type u_1} (w : ℕ) (a b : ι × Fin w → ZMod (2 ^ w)) : bitCompose w (a + b) = bitCompose w a + bitCompose w b

The weighted row sum commutes with addition.

theorem Cslib.Crypto.Homomorphic.GSW.bitCompose_smul {ι : Type u_1} (w : ℕ) (a : ZMod (2 ^ w)) (v : ι × Fin w → ZMod (2 ^ w)) : bitCompose w (a • v) = a • bitCompose w v

The weighted row sum commutes with scalar multiplication.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.recomposeMatrix_decomposeMatrix {ι : Type u_1} {ρ : Type u_2} (w : ℕ) (A : Matrix ρ ι (ZMod (2 ^ w))) : recomposeMatrix w (bitMatrix (ZMod (2 ^ w)) (decomposeMatrix w A)) = A

Recomposition recovers every modular matrix from its Boolean decomposition.

theorem Cslib.Crypto.Homomorphic.GSW.recomposeMatrix_add {ι : Type u_1} {ρ : Type u_2} (w : ℕ) (A B : Matrix ρ (ι × Fin w) (ZMod (2 ^ w))) : recomposeMatrix w (A + B) = recomposeMatrix w A + recomposeMatrix w B

Recomposition is additive, including on matrices that are not Boolean.

theorem Cslib.Crypto.Homomorphic.GSW.recomposeMatrix_sub {ι : Type u_1} {ρ : Type u_2} (w : ℕ) (A B : Matrix ρ (ι × Fin w) (ZMod (2 ^ w))) : recomposeMatrix w (A - B) = recomposeMatrix w A - recomposeMatrix w B

Row recomposition preserves subtraction before the resulting residues are decomposed.

theorem Cslib.Crypto.Homomorphic.GSW.recomposeMatrix_mul {ι : Type u_1} {ρ : Type u_2} {κ : Type u_3} [Fintype κ] (w : ℕ) (A : Matrix ρ κ (ZMod (2 ^ w))) (B : Matrix κ (ι × Fin w) (ZMod (2 ^ w))) : recomposeMatrix w (A * B) = A * recomposeMatrix w B

Recompose a matrix product by recomposing the right operand, retaining all modular counts.

theorem Cslib.Crypto.Homomorphic.GSW.recomposeMatrix_smul {ι : Type u_1} {ρ : Type u_2} (w : ℕ) (a : ZMod (2 ^ w)) (C : Matrix ρ (ι × Fin w) (ZMod (2 ^ w))) : recomposeMatrix w (a • C) = a • recomposeMatrix w C

Recomposition commutes with modular scalar multiplication.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.recomposeMatrix_flattenMatrix {ι : Type u_1} {ρ : Type u_2} (w : ℕ) (C : Matrix ρ (ι × Fin w) (ZMod (2 ^ w))) : recomposeMatrix w (bitMatrix (ZMod (2 ^ w)) (flattenMatrix w C)) = recomposeMatrix w C

Flattening preserves the recomposed matrix.

theorem Cslib.Crypto.Homomorphic.GSW.bitCompose_dotProduct {ι : Type u_1} [Fintype ι] (w : ℕ) (v : ι × Fin w → ZMod (2 ^ w)) (s : ι → ZMod (2 ^ w)) : bitCompose w v ⬝ᵥ s = v ⬝ᵥ powersOfTwo w s

Recomposition transfers the powers-of-two expansion from the secret to the other row.

theorem Cslib.Crypto.Homomorphic.GSW.recomposeMatrix_mulVec {ι : Type u_1} {ρ : Type u_2} [Fintype ι] (w : ℕ) (C : Matrix ρ (ι × Fin w) (ZMod (2 ^ w))) (s : ι → ZMod (2 ^ w)) : (recomposeMatrix w C).mulVec s = C.mulVec (powersOfTwo w s)

Matrix recomposition transfers multiplication by an expanded secret to the original secret.

theorem Cslib.Crypto.Homomorphic.GSW.decomposeMatrix_mulVec {ι : Type u_1} {ρ : Type u_2} [Fintype ι] (w : ℕ) (A : Matrix ρ ι (ZMod (2 ^ w))) (s : ι → ZMod (2 ^ w)) : (bitMatrix (ZMod (2 ^ w)) (decomposeMatrix w A)).mulVec (powersOfTwo w s) = A.mulVec s

The Boolean decomposition has the same product with the powers-of-two secret.

theorem Cslib.Crypto.Homomorphic.GSW.flattenMatrix_mulVec {ι : Type u_1} {ρ : Type u_2} [Fintype ι] (w : ℕ) (C : Matrix ρ (ι × Fin w) (ZMod (2 ^ w))) (s : ι → ZMod (2 ^ w)) : (bitMatrix (ZMod (2 ^ w)) (flattenMatrix w C)).mulVec (powersOfTwo w s) = C.mulVec (powersOfTwo w s)

Flattening preserves multiplication by the expanded secret on every modular input.