Homomorphic evaluation of consecutive layers

Constants are encrypted under the target public key, copies are refreshed, and NANDs use the augmented decryption circuit. Every output is truncated to the base decryption circuit's arity. On valid executions truncation changes nothing; on malformed inputs it still bounds the next layer's wire volume. This unconditional bound is needed for strict polynomial-time evaluation.

Only public keys and encrypted key links are runtime inputs. Secret keys appear in correctness predicates, never in the evaluator. EncryptedWires pairs every plaintext with a ciphertext of the required width and decryption, without asserting that intermediate ciphertexts are fresh.

Main definitions

• Cslib.Crypto.Homomorphic.Scheme.EncryptedWires: the invariant between adjacent layers.
• Cslib.Crypto.Homomorphic.Scheme.evaluateNode: evaluate and bound a single node.
• Cslib.Crypto.Homomorphic.Scheme.evaluateLayer: traverse a layer with independent calls.
• Cslib.Crypto.Homomorphic.Scheme.evaluateLayers: the public bounded loop over all layers.

Main results

• Cslib.Crypto.Homomorphic.Scheme.encryptedWires_evaluateLayer: correct evaluation from the preceding key to the target key, including constants, copies and repeated inputs.

References

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

def Cslib.Crypto.Homomorphic.Scheme.EncryptedWires (E : Scheme) (ciphertextWidth : ℕ → ℕ) (n : ℕ) (sk bits : List Bool) (inputs : List (List Bool)) : Prop

Pair the plaintext wires with ciphertexts of the right width and decryption. This includes equality of wire counts, and makes no fresh-encryption assumption.

theorem Cslib.Crypto.Homomorphic.Scheme.EncryptedWires.getD {E : Scheme} {ciphertextWidth : ℕ → ℕ} {n : ℕ} {sk bits : List Bool} {inputs : List (List Bool)} (h : E.EncryptedWires ciphertextWidth n sk bits inputs) {i : ℕ} (hi : i < bits.length) : (inputs.getD i []).length = ciphertextWidth n ∧ E.decrypt n sk (inputs.getD i []) = bits.getD i false

A valid wire lookup preserves both width and decryption.

theorem Cslib.Crypto.Homomorphic.Scheme.EncryptedWires.select {E : Scheme} {ciphertextWidth : ℕ → ℕ} {n : ℕ} {sk bits : List Bool} {inputs : List (List Bool)} (h : E.EncryptedWires ciphertextWidth n sk bits inputs) {outputs : List ℕ} (houtputs : ∀ i ∈ outputs, i < bits.length) : E.EncryptedWires ciphertextWidth n sk (Circuits.Boolean.Layered.select bits outputs) (List.map (fun (x : ℕ) => inputs.getD x []) outputs)

Selecting valid ciphertext wires preserves their width and plaintexts, with no key change. Output order and repetitions are exactly those of the index list.

theorem Cslib.Crypto.Homomorphic.Scheme.FreshInputs.encryptedWires {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) {n : ℕ} {keys : List Bool × List Bool} (hkeys : keys ∈ (E.keyGen n).eval.support) {bits : List Bool} {inputs : List (List Bool)} (h : E.FreshInputs n keys.1 bits inputs) : E.EncryptedWires ciphertextWidth n keys.2 bits inputs

Fresh encryptions initialize the stronger invariant used after evaluation.

theorem Cslib.Crypto.Homomorphic.Scheme.take_decryptionArity_eq {secretWidth ciphertextWidth : ℕ → ℕ} {n : ℕ} {ciphertext : List Bool} (h : ciphertext.length = ciphertextWidth n) : List.take (secretWidth n + ciphertextWidth n) ciphertext = ciphertext

Truncation at the decryption circuit's input arity leaves every valid ciphertext unchanged. The arity can be read from the generated circuit without computing the width functions.

def Cslib.Crypto.Homomorphic.Scheme.evaluateNode {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (n : ℕ) (pk : List Bool) (encryptedKey inputs : List (List Bool)) (node : Circuits.Boolean.Layered.Node) : ProbComp (List Bool)

Evaluate one node under the target public key, then bound its result on every input.

def Cslib.Crypto.Homomorphic.Scheme.evaluateLayer {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (n : ℕ) (pk : List Bool) (encryptedKey inputs : List (List Bool)) (layer : List Circuits.Boolean.Layered.Node) : ProbComp (List (List Bool))

Execute each node using the same preceding layer and encrypted secret key.

def Cslib.Crypto.Homomorphic.Scheme.evaluateLayerStep {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (n : ℕ) (publicKeys : List (List Bool)) (encryptedKeys : List (List (List Bool))) (layers : List (List Circuits.Boolean.Layered.Node)) (state : ℕ × List (List Bool)) : ProbComp (ℕ × List (List Bool))

One level of the public loop. The state stores the next level and its current wires. The public-key list starts at the first target key, after the input-encryption key.

def Cslib.Crypto.Homomorphic.Scheme.evaluateLayers {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (n : ℕ) (publicKeys : List (List Bool)) (encryptedKeys : List (List (List Bool))) (inputs : List (List Bool)) (layers : List (List Circuits.Boolean.Layered.Node)) : ProbComp (List (List Bool))

Evaluate all scheduled layers. Missing public data uses empty defaults; correctness requires a valid chain, while the efficiency certificate covers these malformed inputs as well.

theorem Cslib.Crypto.Homomorphic.Scheme.length_evaluateNode_le {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (n : ℕ) (pk : List Bool) (encryptedKey inputs : List (List Bool)) (node : Circuits.Boolean.Layered.Node) (result : List Bool) (h : result ∈ (evaluateNode D n pk encryptedKey inputs node).eval.support) : result.length ≤ secretWidth n + ciphertextWidth n

A node's output is bounded even with invalid wires, keys, or encrypted key links.

theorem Cslib.Crypto.Homomorphic.Scheme.evaluateLayer_bounds {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (n : ℕ) (pk : List Bool) (encryptedKey inputs : List (List Bool)) (layer : List Circuits.Boolean.Layered.Node) (outputs : List (List Bool)) (h : outputs ∈ (evaluateLayer D n pk encryptedKey inputs layer).eval.support) : outputs.length = layer.length ∧ ∀ ciphertext ∈ outputs, ciphertext.length ≤ secretWidth n + ciphertextWidth n

Every execution has the scheduled number of output wires, each bounded by the decryption circuit's arity. No correctness, validity, or key-generation premise is used.

theorem Cslib.Crypto.Homomorphic.Scheme.evaluateNode_correct {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Bootstrappable D) (n : ℕ) (keys : List Bool × List Bool) (hkeys : keys ∈ (E.keyGen n).eval.support) (sk : List Bool) (hsk : sk.length = secretWidth n) (encryptedKey : List (List Bool)) (hek : E.FreshInputs n keys.1 sk encryptedKey) (bits : List Bool) (inputs : List (List Bool)) (hinputs : E.EncryptedWires ciphertextWidth n sk bits inputs) (node : Circuits.Boolean.Layered.Node) (hnode : Circuits.Boolean.Layered.Node.Valid bits.length node) (result : List Bool) (hresult : result ∈ (evaluateNode D n keys.1 encryptedKey inputs node).eval.support) : result.length = ciphertextWidth n ∧ E.decrypt n keys.2 result = Circuits.Boolean.Layered.Node.eval bits node

Valid nodes move the invariant to the target key. No intermediate freshness is needed.

theorem Cslib.Crypto.Homomorphic.Scheme.encryptedWires_evaluateLayer {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Bootstrappable D) (n : ℕ) (keys : List Bool × List Bool) (hkeys : keys ∈ (E.keyGen n).eval.support) (sk : List Bool) (hsk : sk.length = secretWidth n) (encryptedKey : List (List Bool)) (hek : E.FreshInputs n keys.1 sk encryptedKey) (bits : List Bool) (inputs : List (List Bool)) (hinputs : E.EncryptedWires ciphertextWidth n sk bits inputs) (layer : List Circuits.Boolean.Layered.Node) (hlayer : ∀ node ∈ layer, Circuits.Boolean.Layered.Node.Valid bits.length node) (outputs : List (List Bool)) (houtputs : outputs ∈ (evaluateLayer D n keys.1 encryptedKey inputs layer).eval.support) : E.EncryptedWires ciphertextWidth n keys.2 (Circuits.Boolean.Layered.evalLayer bits layer) outputs

Evaluating a valid layer preserves the exact wire count, ciphertext width and plaintext values under the next key.