Compact decryption for the leveled construction

The actual leveled decryption algorithm decodes two secret endpoints, chooses one using the ciphertext tag, and evaluates the base decryption circuit. Its circuit bound must include this wrapper, not just the base circuit. We apply P ⊆ P/poly to the complete native algorithm and fix the unary security parameter by a substitution. Framing the secret-key input and fixing the parameter together cost four gates.

The resulting family depends only on the security parameter, not on the depth budget. It agrees with decryption on all words of the prescribed lengths, including malformed secret-key encodings. This establishes the common-decryption-circuit condition in Gentry's Definition 3. The conclusion is a nonuniform existence theorem; it does not supply a circuit generator.

Main results

• Cslib.Crypto.Homomorphic.Leveled.exists_decrypt_circuits: polynomial-size circuits for the complete tagged decryption algorithm, with one family shared by every depth budget.
• Cslib.Crypto.Homomorphic.Leveled.exists_decrypt_parameter_bound: a native time and space bound depending only on the security parameter at the prescribed widths, shared by every budget.

References

• C. Gentry, Fully Homomorphic Encryption Using Ideal Lattices, Sections 1.1 and 2
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1

theorem Cslib.Crypto.Homomorphic.Leveled.exists_decrypt_parameter_bound {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) : ∃ (time : ℕ × List Bool × List Bool → ℕ) (space : ℕ × List Bool × List Bool → ℕ) (bound : ℕ → ℕ), PolynomiallyBounded bound ∧ (∀ (budget : ℕ → ℕ), Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace (fun (p : ℕ × List Bool × List Bool) => (scheme D budget).decrypt p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBool time space) ∧ ∀ (n : ℕ) (sk ciphertext : List Bool), sk.length = 3 * secretWidth n + 1 → ciphertext.length = ciphertextWidth n + 1 → time (n, sk, ciphertext) ≤ bound n ∧ space (n, sk, ciphertext) ≤ bound n

The native decryption computation has one time and space certificate for every depth budget. On all words of the derived widths, both resources are bounded by a polynomial in the security parameter alone. The native certificate itself covers arbitrary input words.

theorem Cslib.Crypto.Homomorphic.Leveled.exists_decrypt_circuits {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) : ∃ (circuits : (n : ℕ) → Circuits.Circuit Circuits.Boolean.signature (3 * secretWidth n + 1 + (ciphertextWidth n + 1)) 1), (PolynomiallyBounded fun (n : ℕ) => (circuits n).size) ∧ ∀ (budget : ℕ → ℕ) (n : ℕ) (sk ciphertext : List Bool), sk.length = 3 * secretWidth n + 1 → ciphertext.length = ciphertextWidth n + 1 → (circuits n).eval Circuits.Boolean.interpretation (BitString.ofList (3 * secretWidth n + 1 + (ciphertextWidth n + 1)) (sk ++ ciphertext)) 0 = (scheme D budget).decrypt n sk ciphertext

The actual decoder, tag selection and base-circuit evaluation have polynomial-size circuits on the derived key and ciphertext widths. One circuit family works for every depth budget, and its specification includes every word of those widths, without a support or validity premise. This is nonuniform circuit existence, not a circuit-generation certificate.