Exact row arithmetic for GSW decryption

The expanded-secret product used by GSW.decrypt equals one recomposed ciphertext row paired with the unexpanded secret. Its first coordinate is subtracted by the sum of the remaining coordinates times the secret entries. For width at least two, decryption is exclusive-or of the two highest bits of this residue.

These identities hold on every typed secret and Boolean ciphertext. They require no key generation, encryption support or noise hypothesis, as needed for a decryption circuit correct on all well-sized raw inputs. They do not yet construct that circuit or bound its depth.

Main definitions

• decryptionPhase: the recomposed row's modular inner product with the secret vector.

Main results

• decryptionPhase_eq_mulVec: the row expression equals the original expanded-secret product.
• decrypt_eq_decode_decryptionPhase: decryption uses the highest row of the leading coordinate.
• decrypt_eq_xor_highBits: the two highest bits determine decryption at width at least two.

References

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

def Cslib.Crypto.Homomorphic.GSW.decryptionPhase {n w : ℕ} (t : Fin n → ZMod (2 ^ w)) (C : Ciphertext n w) (row : Fin (n + 1) × Fin w) : ZMod (2 ^ w)

Recompose one ciphertext row, then take its inner product with (1,-t).

theorem Cslib.Crypto.Homomorphic.GSW.decryptionPhase_eq_mulVec {n w : ℕ} (t : Fin n → ZMod (2 ^ w)) (C : Ciphertext n w) (row : Fin (n + 1) × Fin w) : decryptionPhase t C row = (bitMatrix (ZMod (2 ^ w)) C).mulVec (powersOfTwo w (secretVector t)) row

Row recomposition preserves the original multiplication by the expanded secret.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.decrypt_zero {n : ℕ} (t : Fin n → ZMod (2 ^ 0)) (C : Ciphertext n 0) : decrypt t C = false

The total width-zero decryption routine returns false.

theorem Cslib.Crypto.Homomorphic.GSW.decrypt_eq_decode_decryptionPhase {n w : ℕ} (hw : 0 < w) (t : Fin n → ZMod (2 ^ w)) (C : Ciphertext n w) : decrypt t C = decode w (decryptionPhase t C (0, ⟨w - 1, ⋯⟩))

At positive width, decryption reads the highest digit of the leading coordinate.

theorem Cslib.Crypto.Homomorphic.GSW.decrypt_one {n : ℕ} (t : Fin n → ZMod (2 ^ 1)) (C : Ciphertext n 1) : decrypt t C = (decryptionPhase t C (0, 0)).val.testBit 0

At width one, decryption is the sole bit of the selected row's phase.

theorem Cslib.Crypto.Homomorphic.GSW.decrypt_eq_xor_highBits {n w : ℕ} (hw : 2 ≤ w) (t : Fin n → ZMod (2 ^ w)) (C : Ciphertext n w) : decrypt t C = ((decryptionPhase t C (0, ⟨w - 1, ⋯⟩)).val.testBit (w - 1) ^^ (decryptionPhase t C (0, ⟨w - 1, ⋯⟩)).val.testBit (w - 2))

At width at least two, all raw ciphertexts decrypt by exclusive-or of two phase bits.