Selected-row GSW decryption circuits

The input order is the complete serialized secret followed by the complete serialized ciphertext. The row selected by the existing total decoder is used on every input, without a key-generation or noise hypothesis. Arithmetic circuits preserve residues modulo the word modulus.

Main definitions

• Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.inputWidth: the complete raw input length.
• Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.circuit: the actual total raw-input decryptor.

Main results

• Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.correct: agreement with serialized decryption on every well-sized raw input, including widths zero and one and both half-open decoder ties.
• Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.depth_circuit_le: explicit logarithmic depth.
• Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.size_circuit_le: explicit polynomial gate count.

References

• C. Gentry, A. Sahai, B. Waters, Sections 3.1 and 3.4.
• C. Gentry, Definition 4: augmented decryption takes all key and ciphertext bits.

@[reducible, inline]

abbrev Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.inputWidth (n w : ℕ) : ℕ

Secret bits precede all square-matrix ciphertext bits.

def Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.circuit (n w : ℕ) : Circuits.Circuit Circuits.Boolean.signature (inputWidth n w) 1

The actual total GSW decryptor, with all raw secret and ciphertext bits as inputs.

theorem Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.depth_circuit_le (n w : ℕ) : (circuit n w).depth ≤ 28 + 18 * Nat.clog 2 (w + 1) + 12 * Nat.clog 2 n

The selected-row construction has logarithmic depth in both parameter dimensions.

theorem Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.size_circuit_le (n w : ℕ) : (circuit n w).size ≤ 131 * (n + 1) * (w + 1) ^ 2

Polynomial gate count includes all unused fallback gates in the balanced construction.

theorem Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.correct (n w : ℕ) (secret ciphertext : List Bool) (hs : secret.length = n * w) (hc : ciphertext.length = (n + 1) * w * ((n + 1) * w)) : (circuit n w).eval Circuits.Boolean.interpretation (BitString.ofList (inputWidth n w) (secret ++ ciphertext)) 0 = decryptSerialized n w secret ciphertext

The serialized contract required by generic refresh: every well-sized raw pair is covered.