Repository navigation
feat(crypto): instantiate bootstrapping with a concrete LWE-based scheme #486
Description
Scope
Recover the concrete LWE-based homomorphic encryption goal as a separate development from the generic conditional Gentry bootstrapping theorem in #322. The generic endpoint was completed in #481; it does not exhibit a secure and correct concrete cryptosystem.
The deterministic GSW algebra with exact noise and correctness proofs is merged (#488 / PR #496). Finite sampling and supported correctness are tracked in #495; statistical hiding with a shared public matrix is in #494 / PR #498. The next independently reviewable milestones are #500 (complete native key generation and encryption) and #501 (the exact decision-LWE reduction and actual scheme IND-CPA theorem). Ownership and active status are recorded in the comments. Decryption/evaluation runtime, shallow augmented decryption, admissible bootstrapping parameters and the concrete FHE instantiation remain part of this parent objective.
Required result
- Define the actual key generation, encryption, decryption, evaluation, and finite sampling algorithms for a concrete LWE-based construction, with explicit parameter and noise families.
- State the decision-LWE assumption as a precise computational distinguishing experiment matching those algorithms and the library's uniform probabilistic polynomial-time adversaries. Prove the encryption security reduction to that assumption.
- Prove correctness, noise growth, output widths, and native polynomial-time certificates for the actual algorithms. Construct the decryption circuits and establish the augmented-decryption bootstrappability hypotheses rather than assuming the desired output properties in a structure.
- Give an explicit nonvacuous admissible parameter family and connect the construction to the leveled endpoint for every polynomially bounded requested depth family. Separate requested depth, executable budget, ciphertext size, and decryption cost.
- Address the library's perfect-support correctness contract explicitly. Unbounded noise tails cannot be silently discarded: any bounded or truncated sampler needs an appropriate correctness argument and a security comparison supporting the exact stated assumption.
- If a fixed-key, arbitrary-depth endpoint is provided, expose its separate one-key circular-security assumption unless it is proved from a clearly stated stronger assumption. Do not infer circular security from ordinary IND-CPA or ordinary decision-LWE without a proof.
Completion and review
The final theorem must identify all cryptographic and parameter assumptions and the actual constructed scheme. A Regev-style public-key encryption result, a functional toy scheme, or a security-only fixture is a milestone, not completion of this issue. Require meaningful client examples, headline axiom guards, all repository checks, and independent API/correctness review of the final statements against the primary sources. Keep ROADMAP.md accurate throughout. Once the full endpoint is proved, provide a checked Lean formal abstract and generated PDF stating the actual construction, correctness and parameter conditions, computational security assumptions, native resource guarantees and compactness. State any circular-security assumption separately. Independently review the abstract against the final Lean definitions and statements; supporting algebra alone does not complete this headline.
The withdrawn worst-case quantum lattice-to-LWE reduction (#330, roadmap target 10) is a separate theorem goal; using a precise decision-LWE assumption does not claim that reduction has been recovered.
Primary sources and dependencies
- Gentry, Fully Homomorphic Encryption Using Ideal Lattices (STOC 2009): https://www.cs.cmu.edu/~odonnell/hits09/gentry-homomorphic-encryption.pdf
- Gentry, Sahai, and Waters, Homomorphic Encryption from Learning with Errors: Conceptually-Simpler, Asymptotically-Faster, Attribute-Based (CRYPTO 2013), a candidate construction to assess during the design milestone: https://eprint.iacr.org/2013/340
- Generic conditional bootstrapping: feat(crypto): formalize Gentry's bootstrapping theorem for leveled and fixed-key fully homomorphic encryption #322 and feat(crypto): complete leveled bootstrapping for polynomial depth families #481.
AI-assisted task decomposition by worker-codex-gentry-endpoint-20261023. This issue records an open target, not a completed construction or security proof.
Activity
SamuelSchlesinger commentedon Oct 23, 2026
Active design claim — worker-codex-lwe-design-20261023. I am checking the actual GSW-style construction, bounded noise, computational LWE experiment, and native implementation obligations before splitting the first code milestone. /root/maintenance_audit is checking the construction/security path against primary sources; /root/refactor_plan_review is mapping reusable algebra, sampling, encoding and runtime APIs. These are read-only delegated subtasks; root owns the design and subsequent issue/branch scope. #487 remains in coordinator review. No concrete LWE or security result is claimed yet.
SamuelSchlesinger commentedon Oct 23, 2026
Active — worker-codex-lwe-design-20261023. The actual GSW key/encryption/NAND equations and noise-threshold correctness are implemented under #488; targeted source and nonzero-noise regression builds pass. Final independent review and all six repository checks are underway. Sampling/native implementation, the decision-LWE security reduction, and shallow decryption with admissible parameters remain open. The completion criteria now include the user's requested checked formal abstract and PDF for the full endpoint.
While #488 validates, /root/refactor_plan_review is scoping the shared-matrix statistical hiding argument and /root/maintenance_audit is scoping finite sampling and uniform binary implementations. Both follow-ups are read-only; root will split implementation issues after checking their proposed contracts.
SamuelSchlesinger commentedon Oct 23, 2026
Milestone handoff — worker-codex-lwe-design-20261023. The deterministic GSW core is awaiting coordinator integration in #496, with all six local gates passing and independent approval of its published head. The next scoped tasks are finite sampling/support correctness (#495) and shared-matrix statistical hiding (#494). The read-only reconnaissance subtasks are complete; their task-owned Lean servers are stopped. This parent remains open: native complete algorithms, the decision-LWE reduction, admissible parameters and shallow-decryption bootstrappability still require proofs.
SamuelSchlesinger commentedon Oct 23, 2026
Coordinator integration: the deterministic construction/correctness milestone #488 landed in #496 after review and validation. This supplies the actual GSW gadgets, keys/encryption/NAND, integer-noise bounds and decoder correctness. The full secure native bootstrappable instantiation remains open; sampling #495 and shared-public-matrix hiding #494 are tracked separately. Validation/review evidence stays on the PR.
SamuelSchlesinger commentedon Oct 23, 2026
Active — worker-codex-lwe-design-20261023 / worker-codex-lwe-sampling-20261023: the GSW algebra/correctness core is merged in #496; statistical hiding is awaiting coordinator integration in #498. The #495 sampler implementation, exact joint fair-bit law, typed/serialized bridges and native random-input certificates have independent approval; all six local gates are running before publication. Delegated read-only next-step scopes:
/root/maintenance_auditis mapping the complete native matrix algorithms, and/root/refactor_plan_reviewis mapping the exact generated-key decision-LWE reduction. Full algorithm efficiency, that computational reduction, admissible parameter families and shallow augmented decryption remain open.doc(roadmap): record the conditional Gentry endpoint and LWE follow-up
doc(crypto): document GSW correctness scope and source
SamuelSchlesinger commentedon Oct 23, 2026
paused at the user's request— worker-codex-lwe-design-20261023. The user explicitly paused the recovery goal; root and all delegated workers have stopped theorem development and are preserving handoffs. #502 contains the reviewed, fully validated sampler integration at14f944215584f80090b89e45fc23b888675bc9b0. #500 has partial matrix encoding/pure-bit helper work in its private clone, with the unfinished roundtrip explicitly recorded. #501 has its isolated branch and design/ownership record but no LWE assumption or security reduction implemented yet; delegated parameter work is also paused. No FHE endpoint is claimed, and no unattended progress or hourly updates are promised. On resumption, recheck live ownership and revisions before editing.SamuelSchlesinger commentedon Oct 23, 2026
active— worker-codex-lwe-design-20261023. The user re-enabled the goal after the brief pause. #502 is handed off for coordinator review at exact reviewed/validated head14f944215584f80090b89e45fc23b888675bc9b0; #500 native algorithms and #501 exact LWE security work have resumed in their preserved isolated clones with unchanged ownership. Delegated parameter and signed-modular subtasks are explicitly scoped in those issues. The concrete FHE endpoint and later recovery goals remain open.feat(crypto): prove GSW hiding with a shared public matrix
SamuelSchlesinger commentedon Oct 23, 2026
Coordinator integration: #502 landed, completing #495's supported GSW sampling and serialized random-input certificates. Generated-key security (#501), full native algorithms (#500 and the remaining decryption/evaluation work), admissible parameters and bootstrappability remain open here. #515 separately adds the requested modern-FHE roadmap; those schemes remain planned.
SamuelSchlesinger commentedon Oct 23, 2026
active — worker-codex-lwe-design-20261023; update covers delegated GSW tasks and root security work.
#502 sampling is merged. #500 native key generation/encryption is published as #519, with six local gates and independent review passed; a small reviewed duplicate-lemma cleanup is being validated before final integration. #501 now has a checked concrete
Parameters.indCPAtheorem for the actual serialized programs, conditional only on the exact centered-binomial decision-LWE assumption. Its nine-file core/test slice passed a 6,582-job strict checkpoint and independent review; the formal abstract, final parent integration and full repository gates remain in progress.The modern-FHE roadmap requested by Samuel has merged as #515. It records ring/RLWE arithmetic, FHEW/TFHE programmable bootstrapping, BFV/BGV, CKKS, scheme switching and threshold protocols as later work, preserving this recovery as the first target.
The next substantive #486 gaps remain native decryption/NAND/evaluation, an actual shallow augmented-decryption circuit with compatible parameters, and a concrete instantiation of the generic bootstrapping/compactness endpoint. The current positive-noise family proves fresh and one-NAND correctness, not bootstrappability. Fixed-key FHE still needs its separately stated joint circular-security assumption.
SamuelSchlesinger commentedon Oct 23, 2026
Delegated preparation — worker-codex-lwe-design-20261023
While #501's final integrated checks run,
/root/library_mapis doing a read-only planning subtask: compare the existing native/circuit APIs and generic bootstrapping contract with the primary GSW construction, and identify a feasible shallow augmented-decryption milestone and its exact parameter/security requirements. No implementation ownership or theorem-completion claim is assigned by this subtask. In particular, it must not treat the current fresh/one-NAND parameter family or an arbitrary polynomial-time decryptor as a proof of bootstrappability.SamuelSchlesinger commentedon Oct 23, 2026
Coordinator integration: #519 landed and #500 is completed. Actual serialized GSW key generation and encryption now have uniform native polynomial-time certificates and exact typed/distribution bridges. This closes that runtime milestone; native decryption/NAND, generated-key security (#501), admissible parameters and bootstrappability remain open here.
SamuelSchlesinger commentedon Oct 23, 2026
active — worker-codex-gsw-lwe-security-20261023
The generated-key security milestone is submitted in #524, with all six local gates and independent source/abstract/PDF review complete; CI and coordinator integration remain. Native key generation/encryption (#519) and the modern-methods roadmap (#515) have merged.
The read-only bootstrappability review identified a concrete next sequence: uniform logarithmic-depth addition (#526), native serialized decryption/NAND (#527), then shallow decryption circuits (#528). These issues are available, with separate acceptance criteria and no implementation claims yet. The current parameters have only bounded-depth slack under the proved noise bound. After the shallow circuit is proved, we still need a wider-modulus parameter theorem, accumulated evaluation correctness, native evaluation, and the actual generic bootstrapping instantiation. The new parameter family must state its own exact LWE assumption.
Full #486 remains open. Ordinary generated-key IND-CPA is now proved conditionally in the submitted milestone; circular security and the withdrawn worst-case lattice reduction are still separate obligations.
SamuelSchlesinger commentedon Oct 23, 2026
active — worker-codex-gsw-shallow-decryption-20261023 (
/root)Next implementation wave is delegated with separate ownership:
/root/library_mapworks on #526 (logarithmic-depth addition),/root/maintenance_auditon #527 (native serialized decryption/NAND), and root on #528 (shallow decryption)./root/refactor_plan_reviewis independent reviewer and does not author these changes. Each worker uses a private repository/build output and maintains the corresponding issue. Root begins the exact raw-input decryption identities while the two prerequisites proceed.SamuelSchlesinger commentedon Oct 23, 2026
The current work now connects actual key generation, encryption, NAND and decryption: #537 has passed all six checks and independent review, and is awaiting integration. #524's base security code CI passed; its separate PDF installer timed out (#536). Circuit work continues through reviewed #534 and the logarithmic-depth adder #526. I delegated the explicit wider-modulus noise-margin family to
/root/maintenance_auditin #538, while retaining the actual shallow-decryption construction in #528. The new family will have its own exact LWE premise; it will not count as bootstrappable until the constructed circuit fits its proved budget.feat(crypto): certify native GSW key generation and encryption
SamuelSchlesinger commentedon Oct 23, 2026
Human-requested pause; session
worker-codex-gsw-shallow-decryption-20261023and delegated workers have stopped at checked handoffs. Published ready/reviewed steps include #524 (exact LWE-to-IND-CPA), #537 (native evaluation/decryption), #534/#542/#544 (circuit constructors and carry lookahead), and #552 (wider exact-family noise/depth parameters); integration remains coordinator work. The new balanced generator (#543) and arithmetic (#528) are preserved as clean local commits with all six checks and independent review. Detailed resume record: #528 (comment) . #543 publication was rejected by automatic approval review and was not retried through another route. Task-owned Lean processes were stopped; no unattended work/updates are promised.The remaining mathematical endpoint is unchanged: construct and uniformly generate actual shallow GSW decryption, prove the augmented compiled circuit fits the new depth/noise budget, instantiate bootstrapping, and state every security assumption at the actual chosen family. Full FHE remains open. The separate PDF dependency-install timeout remains #536; code validation does not substitute for its artifact check.
feat(crypto): prove GSW logarithmic-depth parameter margins
feat(crypto): prove GSW logarithmic-depth parameter margins
doc(roadmap): record the open lattice, proof-system and symmetric cry…