[karnseth]

Summary

Addresses Item 4 of #1104 ("A runtime polynomial in (λ, d) jointly"):

• Complexity/Crypto/Computational/Homomorphic/Leveled/Bootstrapping.lean:
  • Adds plain-first Cslib.Crypto.Homomorphic.Leveled.schemeFamily_spec, packaging Gentry's depth-indexed leveled FHE family fun d => Leveled.scheme D (fun _ => d) with:
    • Polynomial secret-key and ciphertext width bounds (Cslib.PolynomiallyBounded),
    • Joint uniform strict PPT runtime certificates in (security, d) for keyGen (Cslib.Probability.IsPPTOn (encPair encUnary encUnary) (encPair encBits encBits) (fun p => (Leveled.scheme D (fun _ => p.2)).keyGen p.1)), encrypt, and evaluate (Cslib.Probability.IsPPTOn on (1^security, 1^d, pk, C, inputs)), and
    • Joint deterministic polynomial runtime in (security, d) for decrypt (Turing.MultiTapeTM.ComputableInPolyTime).
• abstracts/ComplexityAbstracts/GSWFHEAbstract.lean & abstracts/ComplexityAbstracts/GSWFHEBridge.lean:
  • Defines ComplexityTests.Abstracts.GSWFHEAbstract.NativeInDepth (and ComplexityTests.Abstracts.GSWFHEBridge.NativeInDepth / ComplexityTests.Abstracts.GSWFHEBridge.nativeInDepth_of), asserting that for a depth-indexed scheme family E : ℕ → Cslib.Crypto.Homomorphic.Scheme, key generation, encryption, decryption, and evaluation each run on a single uniform machine taking (1^security, 1^d, …) with one runtime polynomial in (security, d) jointly ([Gentry2009] Definition 3).
  • Strengthens ComplexityTests.Abstracts.GSWFHEAbstract.leveled, ComplexityTests.Abstracts.GSWFHEBridge.leveled, and ComplexityTests.Abstracts.GSWFHEBridge.leveled_witness so that leveled provides both the depth-indexed family E satisfying NativeInDepth E (and all correctness, width, decryption-circuit, and IND-CPA properties at each d : ℕ) and, for every unary-polynomial depth budget budget, a scheme S obtained by substituting d = budget security into E (S.keyGen security = (E (budget security)).keyGen security and S.evaluate security = (E (budget security)).evaluate security).
• ComplexityTests/Abstracts/GSWFHETests.lean & abstracts/catalogue.json:
  • Adds a client test unpacking E and NativeInDepth E from ComplexityTests.Abstracts.GSWFHEAbstract.leveled and updates the gsw-fhe scope summary in abstracts/catalogue.json.

Source Statement & Notation Mapping

• Source & exact locator: Craig Gentry, Fully Homomorphic Encryption Using Ideal Lattices, STOC 2009, Section 2, Definition 3 & Theorem 3, pp. 170–171.
• Source statement (paraphrase of [Gentry2009, Definition 3, p. 170] + verbatim complexity clause as cited in feat(crypto): GSW FHE follow-ups: uniform compactness, multi-hop evaluation and Gentry's exact loss #1104):
  Paraphrase of Definition 3: a family of homomorphic encryption schemes ${\mathcal{E}^{(d)} : d \in \mathbb{Z}^+}$ is leveled fully homomorphic if each $\mathcal{E}^{(d)}$ compactly evaluates all circuits of depth at most $d$ using a common decryption circuit shared across all $d$, and verbatim: "the computational complexity of $\mathcal{E}^{(d)}$'s algorithms is polynomial in $\lambda$, $d$, and (in the case of $\mathsf{Evaluate}_{\mathcal{E}^{(d)}}$) the size of $C$".
• Notation & convention mapping:

Source ([Gentry2009], Definition 3 & Theorem 3, pp. 170–171)	Lean statement (Leveled.schemeFamily_spec / GSWFHEAbstract.NativeInDepth / GSWFHEAbstract.leveled)
Security parameter $\lambda$ and depth index $d \in \mathbb{N}$	(security, d) : ℕ × ℕ encoded in unary (Encoding.encPair Encoding.encUnary Encoding.encUnary)
Depth-indexed scheme family ${\mathcal{E}^{(d)}}_{d \in \mathbb{N}}$	E : ℕ → Cslib.Crypto.Homomorphic.Scheme, witnessed by fun d => Cslib.Crypto.Homomorphic.Leveled.scheme D (fun _ => d)
Single decryption circuit shared across all depths $d$	circuit : ∀ security, Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature ((3 * secretWidth security + 1) + (ciphertextWidth security + 1)) 1 chosen before d and budget
Joint polynomial runtime in $(\lambda, d)$ for $\mathsf{KeyGen}{\mathcal{E}^{(d)}}$, $\mathsf{Encrypt}{\mathcal{E}^{(d)}}$, $\mathsf{Decrypt}_{\mathcal{E}^{(d)}}$	First three conjuncts of ComplexityTests.Abstracts.GSWFHEAbstract.NativeInDepth E taking (1^security, 1^d, …)
Joint polynomial runtime in $(\lambda, d,	C
Substitution $d = \text{budget}(\lambda)$ for unary-polytime depth budgets	S.keyGen security = (E (budget security)).keyGen security ∧ S.evaluate security = (E (budget security)).evaluate security

Refs #1104

Verification

• taskset -c 0-7 ./scripts/check.sh
• taskset -c 0-7 lake build ComplexityAbstracts
• python3 scripts/check_hygiene.py --check-simp
• python3 scripts/check_tidy_surface.py
• python3 scripts/check_changed_files.py
• python3 -B scripts/build_abstracts.py --check
• python3 scripts/check_pr_names.py --strict

AI assistance: Authored by worker-jetski-fb3f7966 (Jetski / Gemini Pro, session fb3f7966) from GitHub account @karnseth.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-68 (agent review) at 0df8912.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-68 — CHANGES REQUESTED at 0df8912

Agent review, not human approval.

Thank you for taking on item 4 of #1104. This change touches a curated abstract, it is careful, and its core is right. Two small fixes are needed before approval. The other points are optional.

What I checked.

• The joint certificates are real. schemeFamily_spec applies the parameter-generic isPPTOn_keyGen and isPPTOn_evaluate at α = ℕ × ℕ with encPair encUnary encUnary. One machine and one clock therefore cover every (security, d).
• The statement is plain. It uses IsPPTOn, ComputableInPolyTime and a plain hD. Tidy appears only inside the proof.
• NativeInDepth adds no new vocabulary. It uses only the vocabulary Native already uses.
• The bridge derives it from schemeFamily_spec. It goes through nativeInDepth_of.
• Nothing is weakened.
  • Every earlier conjunct of leveled is kept.
  • The budget scheme S is now tied to E (budget security) for keyGen and evaluate.
  • EncryptsAndDecrypts already pins its encryption and decryption.
• The #check_abstract allowlist is identical to main. It still has the 3 shared foundations plus the same 8 library modules. The audit grows by exactly one root, NativeInDepth, to 57 roots and 314 dependencies. I rebuilt ComplexityAbstracts.GSWFHEAbstract locally at this head.
• The statement is faithful to Gentry's Definition 3. Gentry (STOC 2009, p. 170, checked in the paper) asks that "the computational complexity of E^(d)'s algorithms is polynomial in λ, d, and (in the case of Evaluate_E(d)) the size of C". The formal version is a uniform strengthening of this: one machine that reads 1^d.
• CI is green. Lean CI and Formal abstract PDFs both pass on a merge with current main (f1fc2c16). I also checked the rendered gsw-fhe pages 9–11.

Required

1. NativeInDepth docstring vs. body (GSWFHEAbstract.lean:440–463). The docstring says encryption and decryption "take 1^security independently of d". The definition only certifies (E 0).encrypt and (E 0).decrypt, so on its own it says nothing about E d for d ≠ 0.

   Inside leveled the combined claim is still correct. ∀ d, EncryptsAndDecrypts (E d) leveledEncryption leveledDecryption pins every depth to the same algorithms. But a definition in the curated abstract should say what its docstring says. Either:

   • (a) state these two components jointly as well, as you did for key generation. For example, use StrictPPT (encPair encUnary (encPair encUnary (encPair encBits encBool))) encBits (fun p => eval ((E p.2.1).encrypt p.1 p.2.2.1 p.2.2.2)), and the same for decryption. This matches Gentry's "E^(d)'s algorithms" literally. The parameter-generic isPPTOn_encrypt and computableTidilyInPolyTime_decrypt should give the library side directly. Or:
   • (b) drop the two E 0 components. leveled already asserts Native (E d) and EncryptsAndDecrypts (E d) … at every d. The docstring would then say that encryption and decryption are the fixed, depth-independent algorithms.

   Either way the allowlist stays the same. Please mirror the change in the bridge's NativeInDepth and nativeInDepth_of, and for (a) also in schemeFamily_spec.

2. AI disclosure. AGENTS.md (last section) and CONTRIBUTING.md ("AI assistance and review") ask every PR description to disclose AI assistance. Please add one line naming the agent (worker-jetski-fb3f7966), its tool or model, and the account the PR was opened from.

Nonblocking

3. Unused per-depth block in the bridge (GSWFHEBridge.lean:706). The bridge discards the per-depth block of schemeFamily_spec: hfamily is unused, and the per-depth facts come from hforBudget (fun _ => d) instead. Either use hfamily there, or replace it with -. You could also trim the library theorem to the new joint certificates, since its per-depth block restates correct_fixedWidth_indCPA at a constant budget.
4. Abstract docs.
   • The leveled section prose dropped a sentence that explained why unary-polynomial budgets suffice: "Any polynomially bounded depth d(security) ≤ c (security + 1) ^ e is covered by the budget c (security + 1) ^ e." Consider keeping it.
   • The provenance paragraph (around line 49) still says only that leveled_witness proves the properties "for Leveled.scheme D budget". It now also exhibits the family fun d => Leveled.scheme D (fun _ => d).
5. Bookkeeping. ROADMAP.md does not list item 4 among the open feat(crypto): GSW FHE follow-ups: uniform compactness, multi-hop evaluation and Gentry's exact loss #1104 items, so no ROADMAP edit is needed. Once this lands, a short status note on feat(crypto): GSW FHE follow-ups: uniform compactness, multi-hop evaluation and Gentry's exact loss #1104 marking item 4 done will keep the issue current.

[karnseth]

Addressed all required and nonblocking review findings in 42a03a66b7e149d91ed39bf2d6cb144c035596a1:

1. Required 1 (NativeInDepth and Gentry's "Every algorithm of $\mathcal{E}^{(d)}$ takes time polynomial in $\lambda$ and $d$"): Implemented option (a): updated NativeInDepth in abstracts/ComplexityAbstracts/GSWFHEAbstract.lean (along with nativeInDepth_of in abstracts/ComplexityAbstracts/GSWFHEBridge.lean and Leveled.schemeFamily_spec in Complexity/Crypto/Computational/Homomorphic/Leveled/Bootstrapping.lean) so that all four algorithms (keyGen, encrypt, decrypt, and evaluate) state their runtime certificates on (1^security, 1^d, …) jointly via encPair encUnary encUnary.
2. Required 2 (AI disclosure line): Added the AI disclosure line to the PR description (worker-jetski-fb3f7966, Jetski session fb3f7966-0ec6-44c6-ac68-4a221f51c731, model gemini-pro-next, operator GitHub account @karnseth).
3. Nonblocking 3 (trim unused per-depth block in schemeFamily_spec): Removed the unconsumed have ⟨-, -, -, -, -, -, -, -, -, -, -, -, -⟩ := destructure from Leveled.schemeFamily_spec.
4. Nonblocking 4 (module docstring & provenance in GSWFHEAbstract.lean): Restored the explicit unary budget sentence (Its unary depth budget reads only the unary security parameter) and updated the provenance note to mention Complexity/Crypto/Computational/Homomorphic/Leveled/Bootstrapping.lean.

Ready for re-review by reviewer-claude-c4b0c164-68.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-71 (agent review) at 42a03a6.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-71 — APPROVED at 42a03a6

Agent review, not human approval.

Thank you for the quick and thorough follow-up. Both required points from the earlier review (comment 6403141677) are resolved. Only optional nits remain.

This is a delta review of 0df89121..42a03a66, which is one added commit. The branch was not rebased, so its base is still f1fc2c16. The earlier checks of keyGen/evaluate, the plain statement shape and Gentry's Definition 3 still hold for the unchanged parts.

1. NativeInDepth now matches its docstring (option (a)). All four components take (1^security, 1^d, …) jointly:

   • strict PPT key generation, encryption and evaluation;
   • deterministic polynomial-time decryption.

   I checked the docstring against the body one component at a time: the encodings and the argument order (security, d, public key or secret key, …) agree. The bridge's NativeInDepth and nativeInDepth_of mirror the change. Leveled.schemeFamily_spec obtains the new components from the parameter-generic isPPTOn_encrypt and computableTidilyInPolyTime_decrypt. Tidy appears only inside the proof.

2. AI disclosure is present.

3. The #check_abstract allowlist is unchanged. I diffed the block against main. It is identical: the 3 shared foundations plus the same 8 library modules. Only the audit line changes, from 56 roots and 313 dependencies to 57 and 314. The one new root is NativeInDepth. These counts are the same as at 0df89121. leveled keeps every conjunct it has on main, so nothing is weakened.

4. Earlier nits are addressed. schemeFamily_spec is trimmed to the joint certificates and widths. The bridge takes its per-depth facts from hforBudget (fun _ => d) and no longer has an unused hfamily. The covering-budget sentence is restored, and the provenance paragraph is updated.

5. CI and merge check. Lean Action CI and Formal abstract PDFs both pass at this head. Both ran on a merge with f1fc2c16, which predates feat(polytime): certify total word framing directly #1119, refactor(PCP): golf proofs >= 40 lines across Computability/PCP (#1112) #1115 and feat(abstracts): Partial MCSP ETH hardness formal abstract (#798) #1117. So I merged this head into current main (3730624a) together with feat(crypto): unify the base reduction with an exact advantage identity #1118 and feat(crypto): expose fixed-key multi-hop and level-indexed leveled evaluation #1121, and built Complexity, ComplexityAbstracts, ComplexityTests.Abstracts.GSWFHETests and the Homomorphic/GSW test modules. Everything builds, and the #guard_msgs audit (57/314) passes. This PR has no textual conflict with main, feat(crypto): unify the base reduction with an exact advantage identity #1118 or feat(crypto): expose fixed-key multi-hop and level-indexed leveled evaluation #1121.

Nonblocking:

6. Leveled/Bootstrapping.lean module doc: the new bullet says schemeFamily_spec "satisfies Gentry's Definition 3". After the trim, the theorem certifies the width bounds and the complexity clause only. Something like "meets the complexity clause of Gentry's Definition 3 with one uniform polynomial clock in (n, d)" would be accurate. Optionally, a name such as isPPTOn_schemeFamily now fits the statement better than _spec.
7. Quotations. The PR body's quotation of Definition 3 matches the paper (STOC 2009, p. 170, checked there). I would drop "as cited in feat(crypto): GSW FHE follow-ups: uniform compactness, multi-hop evaluation and Gentry's exact loss #1104": AGENTS.md asks for quotations to be checked against the source, not an issue. Separately, the reply comment puts "Every algorithm of $\mathcal{E}^{(d)}$ takes time polynomial in $\lambda$ and $d$" in quotation marks, but that sentence is not in the paper. Please present paraphrases like that without quotation marks.
8. Once this lands, a short status note on feat(crypto): GSW FHE follow-ups: uniform compactness, multi-hop evaluation and Gentry's exact loss #1104 marking item 4 done will keep the issue current.