NAND-augmented decryption circuits

Gentry's bootstrappability condition concerns actual circuits obtained by connecting a gate to copies of the decryption circuit [Gen09], Definition 4. Here augmentNand D runs two copies of D on disjoint input blocks and applies NAND to their outputs. NAND uses one AND gate and one NOT gate in the De Morgan basis.

Main definitions

• Cslib.Crypto.Homomorphic.augmentNand: NAND applied to two copies of a circuit.

Main results

• Cslib.Crypto.Homomorphic.eval_augmentNand: the augmentation computes NAND of the two results.
• Cslib.Crypto.Homomorphic.size_augmentNand: the augmentation has exactly 2 * D.size + 2 gates.

References

• C. Gentry, Fully Homomorphic Encryption Using Ideal Lattices, Section 2

def Cslib.Crypto.Homomorphic.augmentNand {n : ℕ} (D : Circuits.Circuit Circuits.Boolean.signature n 1) : Circuits.Circuit Circuits.Boolean.signature (n + n) 1

Connect the outputs of two copies of D, on disjoint input blocks, to a NAND circuit.

@[simp]

theorem Cslib.Crypto.Homomorphic.eval_augmentNand {n : ℕ} (D : Circuits.Circuit Circuits.Boolean.signature n 1) (x y : Fin n → Bool) (j : Fin 1) : (augmentNand D).eval Circuits.Boolean.interpretation (Fin.append x y) j = !(D.eval Circuits.Boolean.interpretation x 0 && D.eval Circuits.Boolean.interpretation y 0)

The NAND augmentation evaluates D on each input block and takes NAND of the results.

@[simp]

theorem Cslib.Crypto.Homomorphic.size_augmentNand {n : ℕ} (D : Circuits.Circuit Circuits.Boolean.signature n 1) : (augmentNand D).size = 2 * D.size + 2

The two copies of D and the two NAND gates account for every gate of the augmentation.