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.

The scheme evaluator (scheme D budget).evaluate remains single-hop. Multi-hop evaluation goes through evaluateHop, with the caller tracking the depth offsets along the chain. Because the private artifact retains only the two endpoint secrets (0 and 2 * budget n), only a hop that ends at budget n (offset + step = budget n) yields a ciphertext that (scheme D budget).decrypt can decrypt; a hop ending before budget n (including a depth-zero wiring hop at an intermediate offset) produces a true-tagged ciphertext under key 2 * (offset + step) that (scheme D budget).decrypt cannot decrypt.

This level-indexed hop API is an original adaptation, closest to Gentry's sub-scheme E^(δ) ([Gen09], Section 2, p. 171). GHV is cited for the multi-hop notion (paraphrase: evaluation can be applied to its own outputs) [GHV10]; that notion is not claimed for the fixed-start scheme evaluator (scheme D budget).evaluate itself.

Main results

• Cslib.Crypto.Homomorphic.Leveled.encryptedWires_evaluateCircuit_drop: evaluating a padded circuit at an arbitrary offset along a generated key chain.
• 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.evaluateHop_spec: correctness of a single depth-bounded evaluation hop from level offset to offset + step.
• Cslib.Crypto.Homomorphic.Leveled.evaluateHop_twoHop_spec: two-hop leveled evaluation across step₁ + step₂ = budget n decrypts under the endpoint secret key to the composed circuit value.
• 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, pp. 171--172
• C. Gentry, S. Halevi, and V. Vaikuntanathan, $i$-Hop Homomorphic Encryption and Rerandomizable Yao Circuits

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_drop {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Scheme.Bootstrappable D) (n total offset step : ℕ) (keys : List (List Bool × List Bool)) (links : List (List (List Bool))) {inputCount outputCount : ℕ} (c : Circuits.Circuit Circuits.Boolean.signature inputCount outputCount) (hstep : c.depth ≤ step) (htotal : offset + step ≤ total) (hchain : (keys, links) ∈ (E.generateKeyChain n (2 * total)).eval.support) (x : Fin inputCount → Bool) (inputs : List (List Bool)) (hinputs : E.EncryptedWires ciphertextWidth n (keys.getD (2 * offset) ([], [])).2 (List.ofFn x) inputs) (outputs : List (List Bool)) (houtputs : outputs ∈ (evaluateCircuit D n step (List.drop (2 * offset) (List.map Prod.fst keys).tail) (List.drop (2 * offset) links) inputs inputCount c.code).eval.support) : E.EncryptedWires ciphertextWidth n (keys.getD (2 * (offset + step)) ([], [])).2 (List.ofFn (c.eval Circuits.Boolean.interpretation x)) outputs

Evaluating a circuit of depth at most step starting at depth offset offset (2 * offset into a generated chain of depth 2 * total) advances the wire invariant to key 2 * (offset + step) and preserves the ordered output vector.

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.evaluateHop_spec {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Scheme.Bootstrappable D) (n total offset step : ℕ) (chain : List (List Bool × List Bool)) (links : List (List (List Bool))) (hchain : (chain, links) ∈ (E.generateKeyChain n (2 * total)).eval.support) (c : (m : ℕ) × Circuits.Circuit Circuits.Boolean.signature m 1) (hstep : c.snd.depth ≤ step) (htotal : offset + step ≤ total) (bits : List Bool) (inputs : List (List Bool)) (hbits : bits.length = c.fst) (hinputs : E.EncryptedWires ciphertextWidth n (chain.getD (2 * offset) ([], [])).2 bits (List.map List.tail inputs)) (ciphertext : List Bool) (hc : ciphertext ∈ (evaluateHop D n offset step (keyPair (2 * total) chain links).1 c inputs).eval.support) : ciphertext.length = ciphertextWidth n + 1 ∧ ciphertext.headD false = true ∧ E.decrypt n (chain.getD (2 * (offset + step)) ([], [])).2 ciphertext.tail = c.snd.eval Circuits.Boolean.interpretation (BitString.ofList c.fst bits) 0

Evaluating one hop of depth at most step starting at offset offset produces a true-tagged ciphertext of width ciphertextWidth n + 1 whose payload decrypts under key 2 * (offset + step) to the evaluated circuit output.

theorem Cslib.Crypto.Homomorphic.Leveled.encryptedWires_of_evaluateHop {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Scheme.Bootstrappable D) {n total offset step : ℕ} {chain : List (List Bool × List Bool)} {links : List (List (List Bool))} (hchain : (chain, links) ∈ (E.generateKeyChain n (2 * total)).eval.support) (htotal : offset + step ≤ total) {midBits : List Bool} {mids : List (List Bool)} (hmids : List.Forall₂ (fun (bit : Bool) (mid : List Bool) => ∃ (c : (m : ℕ) × Circuits.Circuit Circuits.Boolean.signature m 1) (bits : List Bool) (inputs : List (List Bool)), c.snd.depth ≤ step ∧ bits.length = c.fst ∧ E.EncryptedWires ciphertextWidth n (chain.getD (2 * offset) ([], [])).2 bits (List.map List.tail inputs) ∧ mid ∈ (evaluateHop D n offset step (keyPair (2 * total) chain links).1 c inputs).eval.support ∧ c.snd.eval Circuits.Boolean.interpretation (BitString.ofList c.fst bits) 0 = bit) midBits mids) : E.EncryptedWires ciphertextWidth n (chain.getD (2 * (offset + step)) ([], [])).2 midBits (List.map List.tail mids)

Pointwise hop evaluations at offset offset with step budget step advance EncryptedWires on the stripped ciphertext payloads to 2 * (offset + step).

theorem Cslib.Crypto.Homomorphic.Leveled.evaluateHop_final_spec {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Scheme.Bootstrappable D) (budget : ℕ → ℕ) (n offset step : ℕ) (chain : List (List Bool × List Bool)) (links : List (List (List Bool))) (hchain : (chain, links) ∈ (E.generateKeyChain n (2 * budget n)).eval.support) (hfinal : offset + step = budget n) (c : (m : ℕ) × Circuits.Circuit Circuits.Boolean.signature m 1) (hstep : c.snd.depth ≤ step) (bits : List Bool) (inputs : List (List Bool)) (hbits : bits.length = c.fst) (hinputs : E.EncryptedWires ciphertextWidth n (chain.getD (2 * offset) ([], [])).2 bits (List.map List.tail inputs)) (ciphertext : List Bool) (hc : ciphertext ∈ (evaluateHop D n offset step (keyPair (2 * budget n) chain links).1 c inputs).eval.support) : ciphertext.length = ciphertextWidth n + 1 ∧ (scheme D budget).decrypt n (keyPair (2 * budget n) chain links).2 ciphertext = c.snd.eval Circuits.Boolean.interpretation (BitString.ofList c.fst bits) 0

Final hop reaching the total budget offset + step = budget n: the output ciphertext has width ciphertextWidth n + 1 and decrypts under (scheme D budget).decrypt to the circuit value.

theorem Cslib.Crypto.Homomorphic.Leveled.evaluateHop_twoHop_spec {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Scheme.Bootstrappable D) (budget : ℕ → ℕ) (n step₁ step₂ : ℕ) (keys : List Bool × List Bool) (hkeys : keys ∈ ((scheme D budget).keyGen n).eval.support) (hbudget : step₁ + step₂ = budget n) (outer : (m : ℕ) × Circuits.Circuit Circuits.Boolean.signature m 1) (houter : outer.snd.depth ≤ step₂) (midBits : List Bool) (mids : List (List Bool)) (hmidBits : midBits.length = outer.fst) (hmids : List.Forall₂ (fun (bit : Bool) (mid : List Bool) => ∃ (c : (m : ℕ) × Circuits.Circuit Circuits.Boolean.signature m 1) (bits : List Bool) (inputs : List (List Bool)), c.snd.depth ≤ step₁ ∧ bits.length = c.fst ∧ (scheme D budget).FreshInputs n keys.1 bits inputs ∧ mid ∈ (evaluateHop D n 0 step₁ keys.1 c inputs).eval.support ∧ c.snd.eval Circuits.Boolean.interpretation (BitString.ofList c.fst bits) 0 = bit) midBits mids) (ciphertext : List Bool) (hc : ciphertext ∈ (evaluateHop D n step₁ step₂ keys.1 outer mids).eval.support) : ciphertext.length = ciphertextWidth n + 1 ∧ (scheme D budget).decrypt n keys.2 ciphertext = outer.snd.eval Circuits.Boolean.interpretation (BitString.ofList outer.fst midBits) 0

Two-hop leveled evaluation: first-hop circuits of depth at most step₁ evaluated on fresh inputs via evaluateHop D n 0 step₁ keys.1, followed by a second-hop circuit outer of depth at most step₂ evaluated on the intermediate ciphertexts via evaluateHop D n step₁ step₂ keys.1 with step₁ + step₂ = budget n, produces a ciphertext of width ciphertextWidth n + 1 that decrypts under (scheme D budget).decrypt n keys.2 to the composed circuit value.

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.