Homomorphic evaluation of ordinary Boolean circuits

Compile the shared De Morgan circuit, execute its layers, and select the designated outputs without another key transition. There are twice the circuit's designated-output depth many transitions. Unused gates do not increase this count, and depth-zero wiring uses the input key.

The final key here depends on actual circuit depth. Homomorphic.Leveled.Basic constructs a depth-budgeted scheme, and Homomorphic.Leveled.Correctness proves normalization to a common final key. Security reductions remain separate obligations.

Main definitions

• Cslib.Crypto.Homomorphic.Scheme.evaluateCircuit: the actual compiler and encrypted evaluator.

Main results

• Cslib.Crypto.Homomorphic.Scheme.encryptedWires_evaluateCircuit: evaluation along any valid supported key list, including repeated keys and inputs from previous evaluations.
• Cslib.Crypto.Homomorphic.Scheme.encryptedWires_evaluateCircuit_of_generatedChain: every supported execution evaluates the original circuit and retains the base ciphertext width.

References

• C. Gentry, Fully homomorphic encryption using ideal lattices, Section 2

def Cslib.Crypto.Homomorphic.Scheme.evaluateCircuit {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (n : ℕ) (publicKeys : List (List Bool)) (encryptedKeys : List (List (List Bool))) (inputs : List (List Bool)) (inputCount : ℕ) (code : List (Circuits.Boolean.Op × List ℕ) × List ℕ) : ProbComp (List (List Bool))

Compile and evaluate raw circuit code, then select its outputs with no further key change. The algorithm is total on raw codes; semantic correctness is for typed circuit codes.

theorem Cslib.Crypto.Homomorphic.Scheme.encryptedWires_evaluateCircuit {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Bootstrappable D) (n : ℕ) (keys : List (List Bool × List Bool)) (links : List (List (List Bool))) {inputCount outputCount : ℕ} (c : Circuits.Circuit Circuits.Boolean.signature inputCount outputCount) (hcount : keys.length = 2 * c.depth + 1) (hkeys : ∀ key ∈ keys, key ∈ (E.keyGen n).eval.support) (hlinks : E.ValidLinks n keys links) (x : Fin inputCount → Bool) (inputs : List (List Bool)) (hinputs : E.EncryptedWires ciphertextWidth n (keys.getD 0 ([], [])).2 (List.ofFn x) inputs) (outputs : List (List Bool)) (houtputs : outputs ∈ (evaluateCircuit D n (List.map Prod.fst keys.tail) links inputs inputCount c.code).eval.support) : E.EncryptedWires ciphertextWidth n (keys.getD (2 * c.depth) ([], [])).2 (List.ofFn (c.eval Circuits.Boolean.interpretation x)) outputs

Every supported evaluation preserves the ordered plaintext vector and exact ciphertext width. Keys and encrypted links may repeat; inputs need only have the right width and decryption, so outputs of previous evaluations are permitted.

theorem Cslib.Crypto.Homomorphic.Scheme.encryptedWires_evaluateCircuit_of_generatedChain {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Bootstrappable D) (n : ℕ) (keys : List (List Bool × List Bool)) (links : List (List (List Bool))) {inputCount outputCount : ℕ} (c : Circuits.Circuit Circuits.Boolean.signature inputCount outputCount) (hchain : (keys, links) ∈ (E.generateKeyChain n (2 * c.depth)).eval.support) (x : Fin inputCount → Bool) (inputs : List (List Bool)) (hinputs : E.FreshInputs n (keys.getD 0 ([], [])).1 (List.ofFn x) inputs) (outputs : List (List Bool)) (houtputs : outputs ∈ (evaluateCircuit D n (List.map Prod.fst keys.tail) links inputs inputCount c.code).eval.support) : E.EncryptedWires ciphertextWidth n (keys.getD (2 * c.depth) ([], [])).2 (List.ofFn (c.eval Circuits.Boolean.interpretation x)) outputs

Every supported evaluation of an ordinary circuit decrypts to its ordered output vector. The generated chain uses two key transitions per original depth, and no transition for output selection. Input ciphertexts are fresh under the first key; the final widths are unchanged.