Repository navigation
feat(crypto): construct shallow GSW decryption circuits #528
Description
Part of #486. Depends on logarithmic-depth binary addition (#526); coordinate the serialized interface with native decryption/NAND (#527). The goal is the actual decryption circuit required by DecryptionCircuits.correct, not an assumed circuit-performance field.
For N=(n+1)w, construct a Boolean circuit taking n*w + N^2 raw bits, ordered as the serialized secret followed by the serialized ciphertext. Acceptance:
- Prove that evaluation equals the existing total
GSW.decrypton every well-sized raw secret/ciphertext pair. Correctness must not assume honestly generated keys, encryption support or a small-noise invariant: the generic refresh contract quantifies over all well-sized inputs. - Reuse the selected ciphertext row
(0,w-1)and gadget recomposition. Forw≥2, prove the half-open decoder agrees with XOR of the top two bits of(a₀ - Σ aⱼ₊₁*tⱼ) mod 2^w. Handlew=0,1by proving their actual current semantics separately. - Build modular products and sums from shifted partial products, balanced carry-save reduction and the logarithmic-depth finisher. Prove a concrete bound of the form
depth ≤ C*(clog₂(n+1)+clog₂(w+1)+1)and polynomial size, with explicit constants sufficient for later parameter arithmetic. The illustrative constant 64 from the feasibility sketch is not an accepted bound until proved. - Give one native polynomial-time generator of the serialized circuit, including all indexing and wiring. Connect the Boolean circuit to the existing layered NAND compiler with its actual depth/size overhead.
- Add raw-input semantic clients, boundary-width cases, generator certificates and axiom guards; run all six checks and obtain independent source/API/correctness review.
The current #501 family has only bounded-depth slack under our proved noise-growth inequality. A later milestone must choose and prove a wider-modulus family satisfying 4*Bfresh*(N+1)^L < 2^w for augmented decryption. Any changed family requires its own exact decision-LWE premise; the present assumption does not transfer automatically. Neither this circuit milestone nor a feasibility calculation proves bootstrappability.
Sources: Gentry, STOC 2009, Definitions 4–5; Gentry–Sahai–Waters, CRYPTO 2013, §§3.3–3.4. Reuse recomposeMatrix_mulVec, Circuit.balanced, existing carry-save circuits and Layered.compile where applicable. AI-assisted task decomposition from a read-only feasibility review, not a completed proof. State: available; no implementation claim.
Activity
SamuelSchlesinger commentedon Oct 23, 2026
active — worker-codex-gsw-shallow-decryption-20261023 (
/root)Claiming the full shallow-decryption circuit milestone on branch
feat/gsw-decryption-circuit-20261023, based on the validated #524 source in the existing private clone. I will first prove the exact selected-row/decoder-bit characterization for arbitrary raw inputs, then construct the circuit and native generator using #526. #527 owns serialized native decryption/NAND separately; shared changes will be coordinated. No bootstrappability or parameter-family completion is implied. Independent review will be performed by an agent who did not author this work.SamuelSchlesinger commentedon Oct 23, 2026
The exact scalar/typed decryption prerequisite is now MCP-clean: width-zero/one behavior, the top-two-bit XOR characterization including quarter ties, and selected-row recomposition for arbitrary secrets/ciphertexts. Direct raw-input boundary/wraparound regressions and axiom guards also pass MCP.
This small shared prerequisite will be included with source credit in #527, where the native decoder consumes it; it will not wait for the full shallow circuit. Root remains responsible for #528. Independent reviewer
/root/refactor_plan_reviewhas checked the library statements; final test/revision review is pending. The shallow circuit and native generator remain unfinished.SamuelSchlesinger commentedon Oct 23, 2026
active — worker-codex-gsw-shallow-decryption-20261023. The shared exact decoder/phase lemmas are included and independently approved in PR #537. Varying-size native code bundling is ready in #534. I have now checked native generators for the actual existing three-to-two and four-to-two carry-save circuits, using #526's fixed-formula template helper; semantic/code equality and carry/overflow clients pass MCP. I will package that bounded prerequisite separately, then construct the full modular-product/sum decryption circuit. The complete #528 statement remains open.
SamuelSchlesinger commentedon Oct 23, 2026
State: active. Worker
worker-codex-gsw-shallow-decryption-20261023continues the actual shallow-decryption construction in/private/tmp/complexitylib-gsw-lwe-security-20261023, branchfeat/gsw-decryption-circuit-20261023. Supporting #540 generators are now in #544 after all six checks and independent review; #526 addition/generation is in #542. Delegated exact balanced-tree native construction as separate #543 to/root/library_map, sessionworker-codex-balanced-code-20261023, isolated branchfeat/balanced-code-20261023; existing half-split semantics and whole encoded-state bounds are explicit criteria. Root next builds modular multiplication and the selected-row inner product, then connects actual decoder semantics/depth/native generation. #538 separately proves a larger exact-family noise margin; no circuit-fit or full bootstrappability claim yet.SamuelSchlesinger commentedon Oct 23, 2026
State: available — human-requested pause. Worker
worker-codex-gsw-shallow-decryption-20261023is releasing active ownership after saving a fully checked arithmetic checkpoint; no unattended work or updates are promised.Local branch
feat/gsw-arithmetic-checkpoint-20261023in/private/tmp/complexitylib-circuit-bundling-20261023is clean atffe3b05a89e937155c8f2f1279892bfba9316837(source commitaaf7b957b678d7b326e56038cbb4688ab20e2a81, final treeb66e7e739ed10c6de56255da5568b8c582324551). It is based on localba319b88, tree-identical to published #544 head11c1e537. Nine-file manifest/private/tmp/gsw-arithmetic-checkpoint-manifest.json, SHA256491b198af895ef80beffe3ddfe8345f64dc8f37883593670955ff1111fa524ed; all six checks passed, log/private/tmp/gsw-arithmetic-checkpoint-six-gates.log. Independent/root/refactor_plan_reviewapproved source/API/correctness/tests/docs without findings; formal abstract catalogue has no changed entry. Checkpoint bundle, patch and metadata are/private/tmp/gsw-arithmetic-checkpoint.{bundle,patch,json}. No PR/source upload attempted for this checkpoint during the pause.Completed here: exact modular multiplication with depth ≤9+14clog₂(w+1), carry-save inner products with depth ≤1+12clog₂w+12clog₂n, exact modular subtraction with depth ≤8+2clog₂(w+1), polynomial gate bounds, raw-code/boundary/block-order/underflow regressions and axiom guards. The original scratch checkout
/private/tmp/complexitylib-gsw-lwe-security-20261023is clean after saving its nine source/test files in stash commitf87cdc7c8c0f273384e69ef0da04b8a27da04880; its shared decoder files are byte-identical to #537. Ten verified idle root-owned Lean/Lake processes were stopped, with no survivors.Resume order: integrate or otherwise compose reviewed #524/#534/#542/#544 and #537/#552; publish/review-bind the saved #543 balanced-code checkpoint when authorized; finish native code generators for these arithmetic circuits; construct the full selected-row decryption circuit and prove equality with the existing total decoder on every well-sized raw input, including w=0,1; prove its actual augmented NAND compilation fits #538's depth budget; then instantiate bootstrapping with the exact new-family LWE premise and explicit additional evaluation-key/circular-security premise where required. No complete shallow-decryption circuit, parameter-fit theorem or full FHE endpoint is claimed.
feat(crypto): prove GSW logarithmic-depth parameter margins
feat(crypto): prove GSW logarithmic-depth parameter margins
SamuelSchlesinger commentedon Oct 23, 2026
active —
worker-codex-01a16ab8-528, delegated bycoordinator-codex-01a16ab8, taking the explicitly released #528 scope at Samuel's request. Branchfeat/gsw-shallow-decryption-528, new isolated worktree/home/samuel/Code/complexitylib-codex/528, based on landed main0a3b3f66.The checkpoint paths in the prior handoff belong to another machine:
/private/tmpdoes not exist here, and the recorded arithmetic commitsffe3b05a/aaf7b957and balanced-code commitsee5a5504/9c3d220bare absent from this repository's object database. No matching published arithmetic/balanced branch or local bundle was found in the inspected project/temp directories. I have not recovered or reused that unpublished code; its prior author/reviewer credit and recorded results remain preserved in this issue. I am checking other authoritative reachable sources before deciding which prerequisites must be reimplemented.The task remains the actual all-well-sized-input selected-row shallow circuit, exact width-zero/one semantics, uniform native generation, concrete size/depth and layered-NAND overhead with parameter fit. Arithmetic checkpoints alone do not finish it. #543 requires separate coordinated ownership and publication/review binding; #486's exact-family security and full FHE obligations remain open. No approval or merge of authored work will be performed by this worker.
SamuelSchlesinger commentedon Oct 23, 2026
Active —
worker-codex-01a16ab8-528: checkpoint 189543ce constructs the actual selected-row decryptor and proves agreement withdecryptSerializedon every well-sized raw secret/ciphertext pair, including widths zero and one. Its circuit depth is at most28 + 18 clog₂(w+1) + 12 clog₂(n)and its gate count at most131(n+1)(w+1)². The six new modules pass focused strict Lean builds.This is not completion of #528: native full-code generation (coordinating #543), the concrete parameter-budget fit, checked clients and full gates remain. The earlier private-machine checkpoint was unavailable here; this published branch contains the new implementation, while retaining the earlier workers' contribution record above.
SamuelSchlesinger commentedon Oct 23, 2026
Awaiting review —
worker-codex-01a16ab8-528: full circuit/native-generation/quantitative-fit deliverable is ready in #607. Validation, exact revisions, checked clients, private-helper API design and remaining #486 limits are recorded in the PR. Depends on #594; request independent Claude source/API/correctness review. No author approval or merge.