Correct evaluation along a generated key chain

The bounded evaluator implements every well-formed program in the consecutive-layer model. Its invariant tracks the current level, the exact plaintext wire list and ciphertext widths. There is one key transition per scheduled layer, regardless of its number of nodes.

The runtime receives the public projection of the target keys and encrypted links. The full key-pair list is only a witness in these theorems. The final plaintexts decrypt with the last secret key; fresh inputs use the first key. Homomorphic.Evaluation composes this theorem with the ordinary-circuit compiler and output selection. Homomorphic.Leveled.Correctness packages the endpoint distinction in a depth-budgeted scheme; security remains a separate obligation.

Main results

• Cslib.Crypto.Homomorphic.Scheme.encryptedWires_evaluateLayers: the complete loop preserves the layer invariant along a valid chain.
• Cslib.Crypto.Homomorphic.Scheme.encryptedWires_evaluateLayers_of_generatedChain: correctness for every supported key-chain sample and pointwise fresh input encryptions.

References

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

theorem Cslib.Crypto.Homomorphic.Scheme.encryptedWires_evaluateLayers {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))) (layers : List (List Circuits.Boolean.Layered.Node)) (hcount : keys.length = layers.length + 1) (hkeys : ∀ key ∈ keys, key ∈ (E.keyGen n).eval.support) (hlinks : E.ValidLinks n keys links) (bits : List Bool) (inputs : List (List Bool)) (hinputs : E.EncryptedWires ciphertextWidth n (keys.getD 0 ([], [])).2 bits inputs) (hvalid : Circuits.Boolean.Layered.WellFormed bits.length layers) (outputs : List (List Bool)) (houtputs : outputs ∈ (evaluateLayers D n (List.map Prod.fst keys.tail) links inputs layers).eval.support) : E.EncryptedWires ciphertextWidth n (keys.getD layers.length ([], [])).2 (Circuits.Boolean.Layered.eval bits layers) outputs

Evaluate all layers along an acyclic key chain. Correctness requires valid references; the public algorithm itself is defined on every input. The initial wires may already be evaluated ciphertexts, provided that their width and decryption are correct.

theorem Cslib.Crypto.Homomorphic.Scheme.encryptedWires_evaluateLayers_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))) (layers : List (List Circuits.Boolean.Layered.Node)) (hchain : (keys, links) ∈ (E.generateKeyChain n layers.length).eval.support) (bits : List Bool) (inputs : List (List Bool)) (hinputs : E.FreshInputs n (keys.getD 0 ([], [])).1 bits inputs) (hvalid : Circuits.Boolean.Layered.WellFormed bits.length layers) (outputs : List (List Bool)) (houtputs : outputs ∈ (evaluateLayers D n (List.map Prod.fst keys.tail) links inputs layers).eval.support) : E.EncryptedWires ciphertextWidth n (keys.getD layers.length ([], [])).2 (Circuits.Boolean.Layered.eval bits layers) outputs

The actual sampler supplies all key and link premises. Each fresh input is under the initial key, and each final output decrypts under the key after the last scheduled layer.