Correct, compact and secure acyclic leveled encryption

The independently proved correctness, exact width, native runtime and IND-CPA results apply to the same constructed scheme. This module assembles correctness, budget-independent polynomial widths and security without assuming those conclusions for the output scheme. Native certificates for its algorithms remain available in Leveled.PolyTime.

Leveled.exists_decrypt_circuits and Leveled.exists_decrypt_parameter_bound give one decryption circuit family and one parameter-only resource bound shared by all budgets. These include the complete tagged decoder and are chosen independently of the requested depth family.

The contract evaluates fresh ciphertexts under an efficiently computed unary depth budget. It does not promise arbitrary reuse of evaluated wrapper ciphertexts, circuit privacy, a concrete base scheme, or fixed-key evaluation without a predetermined budget.

Main results

• Cslib.Crypto.Homomorphic.Leveled.correct_fixedWidth_indCPA: a correct, secure constructed scheme with exact polynomial secret and ciphertext widths independent of the depth budget.
• Cslib.Crypto.Homomorphic.Leveled.exists_scheme_of_polynomiallyBounded: every polynomially bounded depth family is covered by an actual efficient and secure scheme, without requiring the requested family to be computable.

References

• C. Gentry, Fully homomorphic encryption using ideal lattices, Section 2, Theorems 3 and 4

theorem Cslib.Crypto.Homomorphic.Leveled.correct_fixedWidth_indCPA {E : Scheme} {secretWidth ciphertextWidth budget : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hboot : Scheme.Bootstrappable D) (hsecure : Encryption.INDCPA E.keyGen E.encrypt) (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) E.keyGen) (hencrypt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Bool) => E.encrypt p.1 p.2.1 p.2.2) (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) (hbudget : Turing.MultiTapeTM.ComputableTidilyInPolyTime budget Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : (scheme D budget).Correct ∧ ((scheme D budget).FixedWidth (fun (n : ℕ) => 3 * secretWidth n + 1) fun (n : ℕ) => ciphertextWidth n + 1) ∧ (PolynomiallyBounded fun (n : ℕ) => 3 * secretWidth n + 1) ∧ (PolynomiallyBounded fun (n : ℕ) => ciphertextWidth n + 1) ∧ Encryption.INDCPA (scheme D budget).keyGen (scheme D budget).encrypt

Assemble the actual construction's correctness, exact compact widths and IND-CPA security. The native decryption-circuit generator bounds both widths; no output property is an input hypothesis. Evaluation runtime additionally uses the base evaluator certificate, as stated by isPPTOn_scheme_evaluate.

theorem Cslib.Crypto.Homomorphic.Leveled.exists_scheme_of_polynomiallyBounded {E : Scheme} {secretWidth ciphertextWidth depth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hboot : Scheme.Bootstrappable D) (hsecure : Encryption.INDCPA E.keyGen E.encrypt) (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) E.keyGen) (hencrypt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Bool) => E.encrypt p.1 p.2.1 p.2.2) (hevaluate : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair (Circuits.Boolean.encCircuit 1) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × ((n : ℕ) × Circuits.Circuit Circuits.Boolean.signature n 1) × List (List Bool)) => E.evaluate p.1 p.2.1 p.2.2.1 p.2.2.2) (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) (hdepth : PolynomiallyBounded depth) : ∃ (budget : ℕ → ℕ), Turing.MultiTapeTM.ComputableTidilyInPolyTime budget Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary ∧ (∀ (n : ℕ), depth n ≤ budget n) ∧ (scheme D budget).Correct ∧ (∀ (n : ℕ) (c : (m : ℕ) × Circuits.Circuit Circuits.Boolean.signature m 1), c.snd.depth ≤ depth n → (scheme D budget).permitted n c) ∧ ((scheme D budget).FixedWidth (fun (n : ℕ) => 3 * secretWidth n + 1) fun (n : ℕ) => ciphertextWidth n + 1) ∧ (PolynomiallyBounded fun (n : ℕ) => 3 * secretWidth n + 1) ∧ (PolynomiallyBounded fun (n : ℕ) => ciphertextWidth n + 1) ∧ Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (scheme D budget).keyGen ∧ (Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Bool) => (scheme D budget).encrypt p.1 p.2.1 p.2.2) ∧ Turing.MultiTapeTM.ComputableTidilyInPolyTime (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 ∧ (Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair (Circuits.Boolean.encCircuit 1) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × ((n : ℕ) × Circuits.Circuit Circuits.Boolean.signature n 1) × List (List Bool)) => (scheme D budget).evaluate p.1 p.2.1 p.2.2.1 p.2.2.2) ∧ Encryption.INDCPA (scheme D budget).keyGen (scheme D budget).encrypt

Every polynomially bounded depth family is covered by one actual leveled scheme with polynomial widths, native algorithms and IND-CPA security. The selected unary budget dominates the requested depth at every parameter, including its finite prefix. The requested depth family itself need not be computable: only the selected polynomial majorant is executed.