Correctness of depth-budgeted homomorphic encryption

The actual acyclic sampler and padded evaluator satisfy the existing encryption interface for every Boolean circuit within the chosen depth budget. Fresh ciphertexts decrypt at the initial endpoint; evaluated ciphertexts decrypt at the final endpoint, independent of actual depth.

The private key has length 3 * secretWidth n + 1 and ciphertexts have length ciphertextWidth n + 1. These exact lengths are independent of the depth budget. Uniform polynomial bounds and security remain separate obligations. Correctness takes fresh input ciphertexts, as in Scheme.Correct; it does not identify evaluated ciphertexts with fresh ones.

Main results

• Cslib.Crypto.Homomorphic.Leveled.encryptedWires_evaluateCircuit: a common final key for every permitted circuit, including depth-zero wiring and input-free constants.
• Cslib.Crypto.Homomorphic.Leveled.correct: perfect correctness of the constructed scheme.
• Cslib.Crypto.Homomorphic.Leveled.fixedWidth: budget-independent secret and ciphertext widths.

References

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

theorem Cslib.Crypto.Homomorphic.Leveled.mem_support_keyGen_iff {E : Scheme} (n budget : ℕ) (output : List Bool × List Bool) : output ∈ (keyGen E n budget).eval.support ↔ ∃ (keys : List (List Bool × List Bool)) (links : List (List (List Bool))), (keys, links) ∈ (E.generateKeyChain n (2 * budget)).eval.support ∧ keyPair (2 * budget) keys links = output

The serialized keys come from an actual supported acyclic chain.

theorem Cslib.Crypto.Homomorphic.Leveled.decrypt_false {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (n : ℕ) (first last payload : List Bool) (hfirst : first.length = secretWidth n) (hpayload : payload.length = ciphertextWidth n) : decrypt D n (encSecretKey (first, last)) (false :: payload) = E.decrypt n first payload

A false tag selects the initial endpoint on valid payloads.

theorem Cslib.Crypto.Homomorphic.Leveled.decrypt_true {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (n : ℕ) (first last payload : List Bool) (hlast : last.length = secretWidth n) (hpayload : payload.length = ciphertextWidth n) : decrypt D n (encSecretKey (first, last)) (true :: payload) = E.decrypt n last payload

A true tag selects the final endpoint on valid payloads.

theorem Cslib.Crypto.Homomorphic.Leveled.encryptedWires_evaluateCircuit {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Scheme.Bootstrappable D) (n budget : ℕ) (keys : List (List Bool × List Bool)) (links : List (List (List Bool))) {inputCount outputCount : ℕ} (c : Circuits.Circuit Circuits.Boolean.signature inputCount outputCount) (hbudget : c.depth ≤ budget) (hchain : (keys, links) ∈ (E.generateKeyChain n (2 * budget)).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 budget (List.map Prod.fst keys.tail) links inputs inputCount c.code).eval.support) : E.EncryptedWires ciphertextWidth n (keys.getD (2 * budget) ([], [])).2 (List.ofFn (c.eval Circuits.Boolean.interpretation x)) outputs

Padding reaches the budget's final key and preserves the original ordered output vector.

theorem Cslib.Crypto.Homomorphic.Leveled.freshInputs_tail {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) {budget : ℕ → ℕ} {n : ℕ} {pk bits : List Bool} {inputs : List (List Bool)} (h : (scheme D budget).FreshInputs n pk bits inputs) : E.FreshInputs n ((publicKeyDecoder.decode pk).1.getD 0 []) bits (List.map List.tail inputs)

Removing fresh tags gives fresh base ciphertexts under the initial public key.

theorem Cslib.Crypto.Homomorphic.Leveled.encrypt_spec {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (budget : ℕ → ℕ) (n : ℕ) (keys : List Bool × List Bool) (hkeys : keys ∈ ((scheme D budget).keyGen n).eval.support) (bit : Bool) (ciphertext : List Bool) (hc : ciphertext ∈ ((scheme D budget).encrypt n keys.1 bit).eval.support) : ciphertext.length = ciphertextWidth n + 1 ∧ (scheme D budget).decrypt n keys.2 ciphertext = bit

Fresh ciphertexts have the tagged base width and decrypt under the initial endpoint.

theorem Cslib.Crypto.Homomorphic.Leveled.evaluate_spec {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Scheme.Bootstrappable D) (budget : ℕ → ℕ) (n : ℕ) (keys : List Bool × List Bool) (hkeys : keys ∈ ((scheme D budget).keyGen n).eval.support) (c : (m : ℕ) × Circuits.Circuit Circuits.Boolean.signature m 1) (hbudget : (scheme D budget).permitted n c) (bits : List Bool) (inputs : List (List Bool)) (hbits : bits.length = c.fst) (hinputs : (scheme D budget).FreshInputs n keys.1 bits inputs) (ciphertext : List Bool) (hc : ciphertext ∈ ((scheme D budget).evaluate n keys.1 c inputs).eval.support) : ciphertext.length = ciphertextWidth n + 1 ∧ (scheme D budget).decrypt n keys.2 ciphertext = c.snd.eval Circuits.Boolean.interpretation (BitString.ofList c.fst bits) 0

Every supported permitted evaluation has the tagged base width and decrypts at the common final endpoint. This includes circuits whose actual depth is smaller than the chosen budget.

theorem Cslib.Crypto.Homomorphic.Leveled.correct {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Scheme.Bootstrappable D) (budget : ℕ → ℕ) : (scheme D budget).Correct

Bootstrappability constructs a correct scheme for every circuit within the depth budget. No assumption of leveled correctness is used; the keys, padding, and evaluation are explicit.

theorem Cslib.Crypto.Homomorphic.Leveled.fixedWidth {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Scheme.Bootstrappable D) (budget : ℕ → ℕ) : (scheme D budget).FixedWidth (fun (n : ℕ) => 3 * secretWidth n + 1) fun (n : ℕ) => ciphertextWidth n + 1

Private key and ciphertext lengths are independent of both circuit size and depth budget. Public key size and key-generation work may grow with the budget.