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. When the base secret width is also computable in polynomial time in unary, exists_uniform_decrypt_circuits compiles the native decryption algorithm via CircuitValue.exists_uniformCircuitFamily to provide a native polynomial-time 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_uniform_decrypt_circuits: uniformly generated polynomial-size circuits for the complete tagged decryption algorithm when secretWidth is computable in polynomial time in unary.
• 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.ComputableInPolyTime (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.ComputableInTimeAndSpace (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.ComputableInPolyTime (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; see exists_uniform_decrypt_circuits when secretWidth is computable in polynomial time in unary.

theorem Cslib.Crypto.Homomorphic.Leveled.exists_uniform_decrypt_circuits {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hD : Turing.MultiTapeTM.ComputableInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) (hsecret : Turing.MultiTapeTM.ComputableInPolyTime secretWidth Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : ∃ (circuits : (n : ℕ) → Circuits.Circuit Circuits.Boolean.signature (3 * secretWidth n + 1 + (ciphertextWidth n + 1)) 1), Turing.MultiTapeTM.ComputableInPolyTime (fun (n : ℕ) => ⟨3 * secretWidth n + 1 + (ciphertextWidth n + 1), circuits n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 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

When the base secret width is computable in polynomial time in unary, the actual decoder, tag selection and base-circuit evaluation have a uniformly generated family of polynomial-size circuits on the derived key and ciphertext widths. One circuit family and one native polynomial-time generator work for every depth budget, and the specification covers all words of the prescribed widths, without a support or validity premise. Since hD determines only the sum secretWidth n + ciphertextWidth n, computing the wrapper arity (3 * secretWidth n + 1) + (ciphertextWidth n + 1) and the split point between the secret key and ciphertext uses hsecret.