Homomorphic evaluation of Boolean circuits under GSW

A circuit is compiled into consecutive NAND layers by Layered.compile, and every layer is evaluated on serialized GSW ciphertexts. Constants are the noiseless public ciphertexts Flatten(μ · I_N), copies forward a wire, and NAND is the serialized Flatten(I_N - C₁ C₂). The evaluator is deterministic and uses only the dimensions, not the public key.

BoundedError is GSW's "B-bounded error" on complete serialized words. A NAND layer multiplies the bound by at most N + 1, where N = (n + 1) * w, so a circuit of depth d, compiled into 2 * d layers, returns a (N + 1) ^ (2 * d) * B-bounded ciphertext of its output on B-bounded inputs [GentrySahaiWaters2013, Section 3.3]. Under the strict margin 4 * m * η * (N + 1) ^ (2 * d) < 2 ^ w this decrypts correctly for every supported key and fresh encryption. The margin constant 4 comes from this library's middle-half decoder; it is not the paper's q / B > 8 (N + 1) ^ L [GentrySahaiWaters2013, Section 3.4].

Main definitions

• Cslib.Crypto.Homomorphic.GSW.constCiphertext, .constSerialized: noiseless constants.
• Cslib.Crypto.Homomorphic.GSW.BoundedError: a complete word with a bounded integer error.
• Cslib.Crypto.Homomorphic.GSW.evaluateNode, .evaluateLayer, .evaluateLayers: layered evaluation on serialized ciphertexts, total on malformed inputs.
• Cslib.Crypto.Homomorphic.GSW.evaluateCircuit: compile, evaluate and select output 0.

Main results

• Cslib.Crypto.Homomorphic.GSW.boundedError_encryptSerialized: supported fresh encryptions have error bounded by m * η.
• Cslib.Crypto.Homomorphic.GSW.BoundedError.nandSerialized: NAND turns bounds B₁, B₂ into B₁ + N * B₂.
• Cslib.Crypto.Homomorphic.GSW.boundedError_evaluateCircuit: the error after a circuit of depth d is bounded by (N + 1) ^ (2 * d) times the input bound.
• Cslib.Crypto.Homomorphic.GSW.evaluateCircuit_correct: correctness and exact width on supported fresh encryptions under the strict margin.

References

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

def Cslib.Crypto.Homomorphic.GSW.constCiphertext (n w : ℕ) (μ : Bool) : Ciphertext n w

The noiseless ciphertext Flatten(μ · I_N) of a public bit.

theorem Cslib.Crypto.Homomorphic.GSW.constCiphertext_hasError {n w : ℕ} (t : Fin n → ZMod (2 ^ w)) (μ : Bool) : HasError t (constCiphertext n w μ) μ 0

A noiseless constant satisfies the GSW equation with zero error, under every secret.

theorem Cslib.Crypto.Homomorphic.GSW.constCiphertext_eq_decomposeMatrix (n w : ℕ) (μ : Bool) : constCiphertext n w μ = decomposeMatrix w (↑μ.toNat • gadgetMatrix n w)

The constant is the bit decomposition of μ • G.

def Cslib.Crypto.Homomorphic.GSW.constSerialized (n w : ℕ) (μ : Bool) : List Bool

Write all bits of Flatten(μ · I_N) in the ciphertext order of serializeCiphertext.

theorem Cslib.Crypto.Homomorphic.GSW.constSerialized_eq (n w : ℕ) (μ : Bool) : constSerialized n w μ = serializeCiphertext (constCiphertext n w μ)

The computed word is the canonical serialization of the typed constant.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.length_constSerialized (n w : ℕ) (μ : Bool) : (constSerialized n w μ).length = ((n + 1) * w) ^ 2

A constant word has the complete square ciphertext width.

def Cslib.Crypto.Homomorphic.GSW.BoundedError (n w : ℕ) (secret : List Bool) (bound : ℕ) (μ : Bool) (ciphertext : List Bool) : Prop

ciphertext is a complete square ciphertext word encrypting μ under secret whose integer error has every coordinate bounded by bound. This is GSW's "B-bounded error" [GentrySahaiWaters2013, Section 3.4] for serialized words. It makes no freshness claim.

theorem Cslib.Crypto.Homomorphic.GSW.BoundedError.mono {n w : ℕ} {secret : List Bool} {bound : ℕ} {μ : Bool} {ciphertext : List Bool} (h : BoundedError n w secret bound μ ciphertext) {bound' : ℕ} (hle : bound ≤ bound') : BoundedError n w secret bound' μ ciphertext

A bound may be weakened.

theorem Cslib.Crypto.Homomorphic.GSW.BoundedError.decryptSerialized_eq {n w : ℕ} {secret : List Bool} {bound : ℕ} {μ : Bool} {ciphertext : List Bool} (h : BoundedError n w secret bound μ ciphertext) (hw : 0 < w) (hmargin : 4 * bound < 2 ^ w) : decryptSerialized n w secret ciphertext = μ

A word with error strictly below a quarter of the modulus decrypts to its plaintext.

theorem Cslib.Crypto.Homomorphic.GSW.BoundedError.nandSerialized {n w : ℕ} {secret : List Bool} {bound₁ bound₂ : ℕ} {μ₁ μ₂ : Bool} {left right : List Bool} (hleft : BoundedError n w secret bound₁ μ₁ left) (hright : BoundedError n w secret bound₂ μ₂ right) : BoundedError n w secret (bound₁ + (n + 1) * w * bound₂) (!(μ₁ && μ₂)) (GSW.nandSerialized n w left right)

NAND of B₁- and B₂-bounded words is B₁ + N * B₂-bounded, with N = (n + 1) * w [GentrySahaiWaters2013, Section 3.3].

theorem Cslib.Crypto.Homomorphic.GSW.boundedError_constSerialized (n w : ℕ) (secret : List Bool) (μ : Bool) : BoundedError n w secret 0 μ (constSerialized n w μ)

A noiseless constant is 0-bounded under every secret word.

theorem Cslib.Crypto.Homomorphic.GSW.boundedError_encryptSerialized {n m w η : ℕ} {keys : List Bool × List Bool} (hkeys : keys ∈ (keyGenSerialized n m w η).eval.support) (μ : Bool) {ciphertext : List Bool} (hciphertext : ciphertext ∈ (encryptSerialized n m w keys.1 μ).eval.support) : BoundedError n w keys.2 (m * η) μ ciphertext

Every supported fresh encryption under a supported key has error bounded by m * η.

def Cslib.Crypto.Homomorphic.GSW.evaluateNode (n w : ℕ) (wires : List (List Bool)) : Circuits.Boolean.Layered.Node → List Bool

Evaluate one layered node on serialized ciphertexts. Copies are cut to the ciphertext width, which leaves every complete ciphertext unchanged and bounds malformed wires.

def Cslib.Crypto.Homomorphic.GSW.evaluateLayer (n w : ℕ) (wires : List (List Bool)) (layer : List Circuits.Boolean.Layered.Node) : List (List Bool)

Evaluate every node of a layer on the preceding wires.

def Cslib.Crypto.Homomorphic.GSW.evaluateLayers (n w : ℕ) (wires : List (List Bool)) (layers : List (List Circuits.Boolean.Layered.Node)) : List (List Bool)

Evaluate the layers in order, starting from the input ciphertexts.

def Cslib.Crypto.Homomorphic.GSW.evaluateCircuit (n w : ℕ) (C : (k : ℕ) × Circuits.Circuit Circuits.Boolean.signature k 1) (inputs : List (List Bool)) : List Bool

Compile the circuit into NAND layers, evaluate them, and return designated output 0. Evaluation needs only the dimensions; no public key or evaluation key is read.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.evaluateLayers_nil (n w : ℕ) (wires : List (List Bool)) : evaluateLayers n w wires [] = wires

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.evaluateLayers_cons (n w : ℕ) (wires : List (List Bool)) (layer : List Circuits.Boolean.Layered.Node) (layers : List (List Circuits.Boolean.Layered.Node)) : evaluateLayers n w wires (layer :: layers) = evaluateLayers n w (evaluateLayer n w wires layer) layers

theorem Cslib.Crypto.Homomorphic.GSW.boundedError_evaluateNode {n w : ℕ} {secret : List Bool} {bound : ℕ} {bits : List Bool} {wires : List (List Bool)} (h : List.Forall₂ (BoundedError n w secret bound) bits wires) (node : Circuits.Boolean.Layered.Node) (hnode : Circuits.Boolean.Layered.Node.Valid bits.length node) : BoundedError n w secret (((n + 1) * w + 1) * bound) (Circuits.Boolean.Layered.Node.eval bits node) (evaluateNode n w wires node)

One valid node multiplies the error bound by at most N + 1.

theorem Cslib.Crypto.Homomorphic.GSW.forall₂_evaluateLayer {n w : ℕ} {secret : List Bool} {bound : ℕ} {bits : List Bool} {wires : List (List Bool)} (h : List.Forall₂ (BoundedError n w secret bound) bits wires) {layer : List Circuits.Boolean.Layered.Node} (hlayer : ∀ node ∈ layer, Circuits.Boolean.Layered.Node.Valid bits.length node) : List.Forall₂ (BoundedError n w secret (((n + 1) * w + 1) * bound)) (Circuits.Boolean.Layered.evalLayer bits layer) (evaluateLayer n w wires layer)

A valid layer multiplies the error bound by at most N + 1.

theorem Cslib.Crypto.Homomorphic.GSW.forall₂_evaluateLayers {n w : ℕ} {secret : List Bool} {bound : ℕ} {bits : List Bool} {wires : List (List Bool)} (h : List.Forall₂ (BoundedError n w secret bound) bits wires) {layers : List (List Circuits.Boolean.Layered.Node)} (hlayers : Circuits.Boolean.Layered.WellFormed bits.length layers) : List.Forall₂ (BoundedError n w secret (((n + 1) * w + 1) ^ layers.length * bound)) (Circuits.Boolean.Layered.eval bits layers) (evaluateLayers n w wires layers)

A well-formed schedule of L layers multiplies the error bound by at most (N + 1) ^ L [GentrySahaiWaters2013, Section 3.3]. Copy layers are counted although they add no error.

theorem Cslib.Crypto.Homomorphic.GSW.boundedError_evaluateCircuit {n w : ℕ} {secret : List Bool} {bound : ℕ} (C : (k : ℕ) × Circuits.Circuit Circuits.Boolean.signature k 1) {bits : List Bool} {wires : List (List Bool)} (hbits : bits.length = C.fst) (h : List.Forall₂ (BoundedError n w secret bound) bits wires) : BoundedError n w secret (((n + 1) * w + 1) ^ (2 * C.snd.depth) * bound) (C.snd.eval Circuits.Boolean.interpretation (BitString.ofList C.fst bits) 0) (evaluateCircuit n w C wires)

A circuit of depth d evaluated on B-bounded inputs returns a (N + 1) ^ (2 * d) * B-bounded ciphertext of its output, with N = (n + 1) * w. The inputs may themselves be outputs of earlier evaluations.

theorem Cslib.Crypto.Homomorphic.GSW.evaluateCircuit_correct {n w m η : ℕ} (hw : 0 < w) {keys : List Bool × List Bool} (hkeys : keys ∈ (keyGenSerialized n m w η).eval.support) (C : (k : ℕ) × Circuits.Circuit Circuits.Boolean.signature k 1) (hmargin : 4 * m * η * ((n + 1) * w + 1) ^ (2 * C.snd.depth) < 2 ^ w) {bits : List Bool} {inputs : List (List Bool)} (hbits : bits.length = C.fst) (hinputs : List.Forall₂ (fun (μ : Bool) (c : List Bool) => c ∈ (encryptSerialized n m w keys.1 μ).eval.support) bits inputs) : (evaluateCircuit n w C inputs).length = ((n + 1) * w) ^ 2 ∧ decryptSerialized n w keys.2 (evaluateCircuit n w C inputs) = C.snd.eval Circuits.Boolean.interpretation (BitString.ofList C.fst bits) 0

GSW circuit evaluation is correct on supported fresh encryptions under a supported key, when 4 * m * η * (N + 1) ^ (2 * d) < 2 ^ w for the circuit's depth d. The output also has the exact square ciphertext width. This is the bounded-depth correctness of [GentrySahaiWaters2013, Sections 3.3 and 3.4] for the library's decoder.