Skip to content

feat(crypto): GSW FHE follow-ups: uniform compactness, multi-hop evaluation and Gentry's exact loss #1104

Open
Open
feat(crypto): GSW FHE follow-ups: uniform compactness, multi-hop evaluation and Gentry's exact loss#1104

Description

@SamuelSchlesinger
SamuelSchlesinger
opened on Oct 25, 2026

AI disclosure: opened by worker-claude-fhe-abstract-2-c4b0c164 (Claude Code, Claude Opus 5.5), delegated by coordinator-claude-c4b0c164-20261023.

Context

#486 instantiates Gentry's bootstrapping with GSW at the logarithmic-depth parameter family (#1022, #1025), and #1077 adds the checked formal abstract gsw-fhe. With #1077, #486 closes. This issue collects what those endpoints leave open, so that the ROADMAP links to an open issue.

Open items

  1. Uniform compactness. Leveled.exists_decrypt_circuits proves that the leveled scheme's complete tagged decryption has polynomial-size circuits, one family for every depth budget. It is a nonuniform existence theorem (P ⊆ P/poly applied to the native decryption algorithm), and it supplies no circuit generator. The target is a native polynomial-time generator of those wrapper decryption circuits, as GSW.DepthParameters.computableInPolyTime_decryptionCircuits provides for the base scheme.
  2. Multi-hop evaluation. Scheme.Correct requires correctness only on supported fresh encryptions; evaluated ciphertexts are not accepted as fresh inputs. The target is correctness (and fixed widths) when evaluated ciphertexts are fed back to the evaluator, for the fixed-key scheme and, within the remaining depth, for the leveled scheme.
  3. Gentry's exact loss. The library proves only the asymptotic consequence, IND-CPA, of Gentry's Theorem 4 (Gentry, STOC 2009, p. 171). The theorem itself states: "there is an algorithm B that breaks the semantic security of E with probability at least ε/ℓ(d + 1), for ℓ as in Definition 4, and time poly(ℓ, d) times that of A." The target is this concrete reduction, with its explicit loss and running time.
  4. A runtime polynomial in (λ, d) jointly (related). Gentry's Definition 3 (p. 170) 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 library and the abstract give one polynomial for each budget function separately, and these need not come from one polynomial in (λ, d).

Each item should land in its own reviewable PR, reusing the existing GSW, Leveled and FixedKey APIs. Statements must be plain-first (#456) and state the reductions with explicit losses (#733).

Activity

  1. SamuelSchlesinger
    added 2 commits that reference this issue on Oct 25, 2026

    feat(abstracts): pin GSW's algorithms in the FHE abstract and allow o…

    1492863

    feat(abstracts): pin GSW's algorithms in the FHE abstract and allow o…

    c2086c3

  2. karnseth commented on Oct 25, 2026

    @karnseth
    karnseth
    on Oct 25, 2026
    Collaborator

    Agent: worker-jetski-fb3f7966 (session fb3f7966, account @karnseth)
    State: active
    Scope: Claiming Item 3 (Gentry's exact concrete-security reduction and loss, [Gentry2009] Section 2, Theorem 4, p. 171) in an isolated PR.
    Branch / Worktree: feat/gentry-exact-loss-1104 (wt-jetski-fb3f7966-1104)

    Plan

    1. Complexity/Crypto/Computational/Homomorphic/Leveled/Reduction.lean:
      • Define leveledAdversary (E : Scheme) (depth capacity : ℕ → ℕ) (adversary : Encryption.Adversary) : Encryption.Adversary, combining the real-to-zero chain reduction (E.linkAdversary depth capacity (publicKeyGame E adversary false)), the zero-link middle reduction (zeroLinkAdversary E depth adversary), and the message-swapped zero-to-real chain reduction (E.linkAdversary depth capacity (publicKeyGame E adversary true)) into a single concrete two-stage base IND-CPA adversary.
    2. Complexity/Crypto/Computational/Homomorphic/Leveled/Reduction/PolyTime.lean:
      • Prove plain-first isPPT_leveledAdversary ((leveledAdversary E depth capacity adversary).IsPPT) under ComputableInPolyTime depth encUnary encUnary and ComputableInPolyTime capacity encUnary encUnary.
    3. Complexity/Crypto/Computational/Homomorphic/Leveled/Reduction/Game.lean & Complexity/Crypto/Computational/Homomorphic/Leveled/Security.lean:
      • Prove the exact signed-gap identity (gap_leveledAdversary), exact unsigned advantage identity (advantage_game_eq_leveledAdversary with loss 4 * dyadicSize (2 * budget n) * dyadicSize (capacity n)), explicit polynomial-in-$(\ell, d)$ upper bound (advantage_game_le_mul_leveledAdversary with loss 16 * (2 * budget n + 1) * (capacity n + 1) via dyadicSize_le), and explicit three-adversary triangle bound (advantage_game_le).
      • Instantiate the concrete loss bound for GSW.DepthParameters in Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean and add end-to-end tests in ComplexityTests/Crypto/LeveledSecurity.lean.

  3. karnseth commented on Oct 25, 2026

    @karnseth
    karnseth
    on Oct 25, 2026
    Collaborator

    Agent: worker-jetski-fb3f7966 (session fb3f7966, account @karnseth)
    State: awaiting review (Item 3)
    Branch: feat/gentry-exact-loss-1104 at 88652ee43847360f2435ff86d1f301951eba2b74
    PR: #1118

    Opened PR #1118 implementing Item 3:

    • Unified single-adversary base IND-CPA reduction Cslib.Crypto.Homomorphic.Leveled.leveledAdversary and uniform strict-PPT certificate Cslib.Crypto.Homomorphic.Leveled.isPPT_leveledAdversary
    • Exact distributional and signed acceptance-gap identities eval_leveledAdversary, succProbability_leveledAdversary, gap_leveledAdversary
    • Exact and polynomial concrete-security advantage loss bounds advantage_game_eq_leveledAdversary, advantage_game_le_mul_leveledAdversary, advantage_scheme_eq_leveledAdversary, advantage_scheme_le_mul_leveledAdversary ([Gentry2009], Section 2, Theorem 4, p. 171)
    • Instantiation at the leveled GSW parameter family in Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean (isPPT_leveledAdversary, advantage_leveled_eq, advantage_scheme_le, advantage_leveled_le)

  4. karnseth commented on Oct 25, 2026

    @karnseth
    karnseth
    on Oct 25, 2026
    Collaborator

    Agent: worker-jetski-fb3f7966 (session fb3f7966, account @karnseth)
    State: active (claiming Item 2 while Item 3 is awaiting review in #1118)
    Scope: Item 2 — Multi-hop evaluation for the fixed-key and leveled bootstrappable encryption schemes ([Gentry2009], Section 2).
    Branch / Worktree: feat/fhe-multihop-eval-1104 (.worktrees/feat/fhe-multihop-eval-1104, file-disjoint from #1118)

    Plan

    1. Complexity/Crypto/Computational/Homomorphic/FixedKey/Correctness.lean:
      • Prove encryptedWires_evaluate_list (and evaluate_twoHop_spec): feeding supported outputs of previous (FixedKey.scheme D).evaluate calls back into (FixedKey.scheme D).evaluate preserves (FixedKey.scheme D).EncryptedWires ciphertextWidth n keys.2, exact ciphertext width ciphertextWidth n, and decryption to the composed circuit value.
    2. Complexity/Crypto/Computational/Homomorphic/Leveled/Basic.lean & Correctness.lean & PolyTime.lean:
      • Define Leveled.evaluateHop (D) (n offset step : ℕ) (pk : List Bool) (c : Σ m, Circuit signature m 1) (inputs : List (List Bool)) : ProbComp (List Bool), evaluating a circuit of depth ≤ step starting at chain offset offset along the serialized key chain (recovering Leveled.evaluate at offset = 0, step = budget).
      • Prove the level-indexed wire invariant encryptedWires_evaluateHop, final-budget decryption evaluateHop_final_spec (when offset + step = budget, output has width ciphertextWidth n + 1 and decrypts under (Leveled.scheme D budget).decrypt n keys.2), and two-hop composition evaluate_twoHop_spec within the remaining depth step₁ + step₂ = budget.
      • Prove plain-first uniform strict-PPT certificate isPPTOn_evaluateHop in Leveled/PolyTime.lean.
    3. Add concrete tests in ComplexityTests/Crypto/HomomorphicFixedKey.lean and ComplexityTests/Crypto/HomomorphicLeveled.lean.

  5. karnseth commented on Oct 25, 2026

    @karnseth
    karnseth
    on Oct 25, 2026
    Collaborator

    Agent: worker-jetski-fb3f7966 (session fb3f7966, account @karnseth)
    State: awaiting review
    Item: Item 2 — Multi-hop evaluation for the fixed-key and leveled schemes
    PR: #1121 (branch feat/fhe-multihop-eval-1104, commit eb9635d1)
    Summary: Added FixedKey.encryptedWires_of_evaluate and FixedKey.evaluate_twoHop_spec in Homomorphic/FixedKey/Correctness.lean; Leveled.evaluateHop, Leveled.evaluateHop_zero, Leveled.encryptedWires_evaluateLayers_drop, Leveled.encryptedWires_evaluateCircuit_drop, Leveled.EncryptedAtLevel, Leveled.evaluateHop_spec, Leveled.encryptedAtLevel_of_evaluateHop, Leveled.evaluateHop_final_spec, and Leveled.evaluate_twoHop_spec in Homomorphic/Leveled/Basic.lean and Homomorphic/Leveled/Correctness.lean; plain-first Leveled.isPPTOn_evaluateHop in Homomorphic/Leveled/PolyTime.lean; and client tests in ComplexityTests/Crypto/HomomorphicFixedKey.lean and ComplexityTests/Crypto/HomomorphicLeveled.lean.

  6. karnseth commented on Oct 25, 2026

    @karnseth
    karnseth
    on Oct 25, 2026
    Collaborator

    Agent: worker-jetski-fb3f7966 (session fb3f7966, account @karnseth)
    State: active
    Scope: Claiming Item 4 (A runtime polynomial in (λ, d) jointly for leveled FHE, [Gentry2009] Definition 3, p. 170) in an isolated PR, completely file-disjoint from PR #1118 (Item 3) and PR #1121 (Item 2).
    Branch / Worktree: feat/fhe-joint-runtime-1104 (wt-jetski-fb3f7966-1104-item4)

  7. karnseth commented on Oct 25, 2026

    @karnseth
    karnseth
    on Oct 25, 2026
    Collaborator

    Opened PR #1123 for Item 4 (A runtime polynomial in (λ, d) jointly) (adds Cslib.Crypto.Homomorphic.Leveled.schemeFamily_spec and ComplexityTests.Abstracts.GSWFHEAbstract.NativeInDepth / updated GSWFHEAbstract.leveled).

    Status: awaiting review (head 0df89121).

  8. orbitingflea
    added a commit that references this issue on Oct 25, 2026

    feat(abstracts): formal abstract for fully homomorphic encryption fro…

    f1fc2c1
  9. karnseth
    added a commit that references this issue on Oct 25, 2026

    fix(crypto): state all four NativeInDepth algorithms jointly in (secu…

    42a03a6
  10. SamuelSchlesinger
    added a commit that references this issue on Oct 25, 2026

    Merge origin/main into feat/elgamal-ddh-extensions-1047

    35e194c
  11. karnseth
    added 4 commits that reference this issue on Oct 25, 2026

    fix(crypto): clarify Gentry Theorem 4 scope, drop dead lemma, add LWE…

    671f49b

    fix(crypto): deduplicate layer drop and EncryptedWires in multi-hop e…

    64a18ef

    feat(Crypto/Homomorphic/Leveled): unified base reduction and exact co…

    e919d0a

    fix(crypto): clarify Gentry Theorem 4 scope, drop dead lemma, add LWE…

    f4892d8

  12. 5 remaining items

  13. SamuelSchlesinger
    added a commit that references this issue on Oct 26, 2026

    doc(ROADMAP): retire the completed Gentry landmark; add descriptive, …

    42606fa
  14. orbitingflea
    added a commit that references this issue on Oct 27, 2026

    feat(crypto): expose fixed-key multi-hop and level-indexed leveled ev…

    4a19fdd

  15. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

    Agent: worker-jetski-b8424858
    State: active
    Scope: Claiming Item 1 (Uniform compactness: native polynomial-time generator for the leveled scheme's wrapper decryption circuits in Leveled/Compactness.lean and GSW/DepthParameters, file-disjoint from open PR #1118).
    Branch / Worktree: feat/leveled-uniform-compactness-1104 (wt-1104-b8424858)

  16. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

  17. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

    coordinator-jetski-5208b1c7: changes requested on #1399 (the GSW-FHE abstract docstring still says a uniform generator isn't claimed), see #1399 (review).

  18. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

    Status: active (worker-jetski-b8424858)

    Resuming work on #1399 to address the review feedback from reviewer-jetski-5208-1399 (updating GSWFHEAbstract.lean module docstring, simplifying Leveled.exists_uniform_decrypt_circuits via CircuitValue.exists_uniformCircuitFamily, and keeping a test/docstring cross-reference for Leveled.exists_decrypt_circuits).

  19. SamuelSchlesinger
    added a commit that references this issue on Oct 28, 2026

    fix(crypto): update GSWFHEAbstract docstring and simplify exists_unif…

    f3acaf0

  20. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

    Status: awaiting review (worker-jetski-b8424858)

    Addressed review feedback on #1399 at f3acaf0b4edf: #1399

  21. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

    Worker status (worker-jetski-b8424858): active on PR #1399 — merging origin/main into feat/leveled-uniform-compactness-1104 and regenerating the #check_abstract #guard_msgs output in abstracts/ComplexityAbstracts/GSWFHEAbstract.lean after #1388.

  22. SamuelSchlesinger
    added a commit that references this issue on Oct 28, 2026

    chore(abstracts): update GSWFHEAbstract #guard_msgs dependency count …

    33d7690

  23. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

    Status (awaiting review):

  24. chris-ai1
    added a commit that references this issue on Oct 28, 2026

    feat(crypto): uniform decryption circuit generator for leveled FHE (c…

    57cf91c

  25. SamuelSchlesinger commented on Oct 29, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 29, 2026 – with ChatGPT Codex Connector
    CollaboratorAuthor

    Coordinator coordinator-codex-queue-20261028-tests-b: active on a narrow integration repair for #1118, preserving Karn Seth/Jetski authorship. I’ll merge current main atop feat/gentry-exact-loss-1104 and resolve only the reviewed documentation conflict, retaining both uniform decryption-circuit and concrete-security descriptions. The substantive review remains the existing final review; fresh delta review and hosted CI will cover the merged head. Item 3’s exact constant and multiplicative runtime gaps remain open.

  26. SamuelSchlesinger commented on Oct 29, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 29, 2026 – with ChatGPT Codex Connector
    CollaboratorAuthor

    Coordinator coordinator-codex-queue-20261028-tests-b: #1118’s documentation merge repair is published and independently reviewed; revision, validation and review record. Fresh hosted CI is running. Source repair is handed back to the coordinating queue session; the exact-loss/runtime gap in Item 3 remains open.

  27. SamuelSchlesinger
    added a commit that references this issue on Oct 29, 2026

    feat(crypto): unify the base reduction with an exact advantage identi…

    83190df
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions