Repository navigation
feat(circuit): construct uniform logarithmic-depth binary addition #526
Description
Part of the concrete bootstrapping recovery in #486. The existing Boolean.finishCircuit w w has a proved depth bound 7*w; the ordinary word adder also propagates carries sequentially. Shallow GSW decryption needs a logarithmic-depth finisher. Increasing the modulus does not repair a decryption-depth bound linear in the modulus bit width.
Construct an actual Boolean carry-lookahead/prefix adder, reusing the current circuit composition and balanced-tree APIs after checking upstream for overlap. Acceptance:
- Prove exact addition of two unsigned
w-bit words and a carry-in, including the output carry, for every input and width. Derive the modular2^wresult needed by carry-save clients; cover zero width and overflow explicitly. - Prove an explicit bound
depth ≤ C*(Nat.clog 2 (w+1)+1)for an absolute constant and a polynomial size bound. Polynomial size is sufficient for this milestone; linear-size optimization is not required. - Construct and certify one native polynomial-time generator of the serialized circuit from unary width. An existential circuit family or a polynomial size bound alone does not establish uniform construction.
- Provide a checked client replacing the sequential carry-save finishing stage while preserving its value modulo
2^w. Keep the existing public adder interfaces compatible. - Credit the actual prefix/carry-lookahead construction used; add meaningful carry-chain/overflow clients and axiom guards, run all six repository checks, and obtain independent API/correctness review.
Existing consumers: Complexity/Computability/Circuit/Boolean/CarrySave.lean (finishCircuit, val_fstBits_eval_finishCircuit_mod), Boolean/Word.lean, and the planned GSW shallow-decryption circuit. Place the reusable result in the Boolean circuit library, without crypto dependencies.
This issue proves an arithmetic circuit primitive, not GSW bootstrappability. AI-assisted task decomposition from the read-only #486 feasibility review. State: available; no implementation claim.
Activity
SamuelSchlesinger commentedon Oct 23, 2026
Active — worker-codex-carry-lookahead-20261023 (worker). I claim the full #526 scope: exact carry-in/out addition, explicit logarithmic depth and polynomial size, a native serialized circuit generator, and a carry-save finishing client. I will work on branch
feat/carry-lookahead-20261023in an isolated repository based on PR #524's validated source tree d79a101d3483da59b6edbf0740152d288e4a828a. Independent API/correctness review will be requested before publication. No implementation has started; I am checking upstream APIs and the ordered carry-composition design first.SamuelSchlesinger commentedon Oct 23, 2026
Active — worker-codex-carry-lookahead-20261023. The actual doubling circuit and exact carry-in/out addition proof are complete through MCP, including width zero. Its proved depth is at most
7 + 2*Nat.clog 2 (w+1), with exact gate count15*w + 2*(w+1) + 3*(w+1)*Nat.clog 2 (w+1). The modular adder and carry-save replacement are also proved. Native generation is in progress: fixed-template instantiation, complete code-size bounds, and the uniform single-round code generator are checked; the bounded composition loop and final assembly remain. Targeted strict dependency/semantic builds passed; no full-suite result yet. Work remains on the claimed isolated branch, with independent review planned before publication.SamuelSchlesinger commentedon Oct 23, 2026
Active — worker-codex-carry-lookahead-20261023. The exact adder, modular interface, logarithmic-depth carry-save finisher, and all three actual native code generators are complete. Strict focused source and regression builds passed. The work now stacks on #534 and reuses its varying-size bundler; independent review is checking the final source/tests/docs while the six required gates run. The remaining work is validation, review fixes if needed, and publication.
SamuelSchlesinger commentedon Oct 23, 2026
Awaiting review — worker-codex-carry-lookahead-20261023. The full agreed arithmetic/generator scope is implemented in PR #542, stacked on #534. All six repository checks passed on the published source tree; independent API/correctness/tests/docs review approved that snapshot, with its exact-revision record being attached to the PR. This supplies #528’s arithmetic primitive and makes no bootstrappability claim. The issue remains open pending coordinator integration.