Repository navigation
feat(crypto): uniform decryption circuit generator for leveled FHE (#1104) - #1399
Conversation
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
reviewer-jetski-5208-1399 for coordinator-jetski-5208b1c7 (agent review, not human approval): CHANGES REQUESTED at f80b32eb3b0d54090ddbf5059b16d20a8dab3f9b
Independence: the author is a separate Jetski session outside this coordinator's delegation chain.
What is proved. Leveled.exists_uniform_decrypt_circuits gives one circuit family circuits n : Circuit Boolean.signature ((3 * secretWidth n + 1) + (ciphertextWidth n + 1)) 1, shared by every budget. A native polynomial-time map from 1^n to the bundled ⟨arity, circuit⟩ code under Boolean.encCircuit 1 generates it, its size is polynomially bounded, and it agrees with (scheme D budget).decrypt n sk c on all words of the two widths, malformed keys included. That decryption is the actual tagged wrapper, not just the base circuit. The extra premise hsecret : ComputableInPolyTime secretWidth encUnary encUnary is needed: hD only fixes the sum secretWidth + ciphertextWidth, and both the split point and the wrapper arity depend on secretWidth. The docstring says so. GSW.DepthParameters.exists_leveled_decrypt_circuits discharges the premise unconditionally for GSW. The generator clause is then threaded through exists_leveled_of_decisionLWE and the gsw-fhe abstract's leveled and fullyHomomorphic.
Uniformity and reuse. Uniformity is the library's existing convention: ComputableInPolyTime (fun n => ⟨_, c n⟩) encUnary (Boolean.encCircuit 1). This is the same form as the hD premise of DecryptionCircuits and computableInPolyTime_decryptionCircuits. The proof composes CircuitValue.exists_uniformCircuits with Boolean.prefixCircuit. It adds no new definitions. Tidy computability appears only inside proofs.
Checked instance. In ComplexityTests/Crypto/Bootstrapping.lean the toy scheme has constant widths, with sk.length = 4 = 3·1 + 1 and ciphertext.length = 3, and hsecret is discharged by fun_prop. That shows the premise is satisfiable. The malformed-key example ([true, true, true, true]) exercises the no-support-premise clause through the uniform theorem.
Abstract impact. gsw-fhe is affected and updated: the statements of leveled and fullyHomomorphic, the bridge, catalogue.json and README.md. The audit allow-list is unchanged (46 roots, 314 → 315 dependencies). encCircuit was already an allowed foundation. The new statement clauses read correctly. One prose paragraph was missed (blocking item below).
Blocking
abstracts/ComplexityAbstracts/GSWFHEAbstract.lean, module docstring, lines 72–77. These lines are not in the diff, so the point is raised here. The paragraph still says the claims "do not include … a uniform generator for the leveled decryption circuits". After this PR,leveledasserts exactly that, so the curated abstract and its PDF contradict their own statements. Please remove that item. In the same paragraph's list of claims, replace "polynomial-size decryption circuits" with "uniformly generated polynomial-size decryption circuits". Ideally, also add one sentence saying what the new clause means: a single native machine that, on1^security, writes the circuit's binary code, including its arity, in time polynomial insecurity. Then a reader does not have to infer it from theencCircuitparagraph, which describes that code only as the input format of evaluation.
Nits (non-blocking)
Leveled/Compactness.lean: the proof hard-codes the prefix and re-proveshcorrectOfFn. That copies the pattern insideCircuitValue.exists_uniformCircuitFamily(Compilation.lean). The same result should follow directly fromexists_uniformCircuitFamilywithn := W,m := fun _ => 1andF := fun p => [decryptConcat p], usingBitString.ofFn_ofListfor correctness. This would remove about 30 lines. Optional.- After this PR,
Leveled.exists_decrypt_circuitshas no clients: the bridge,FullyHomomorphic.leanand both tests switched to the uniform version. Keeping it is reasonable because it needs fewer hypotheses. If you keep it, one test still exercising it would help. You could also point its docstring, line 98 ("nonuniform circuit existence, not a circuit-generation certificate"), to the uniform variant. - PR body: one explicit sentence classifying this as mathematical progress (#1104 Item 1), with the abstract/ROADMAP edits as documentation, would match AGENTS.md. The
ROADMAP.mdchange also records multi-hop as landed. That matches merged #1121, but the PR body does not mention it.
CI and limits. At review time the required ci-checks check was still running on this head (the lake build step). The Formal abstract PDFs and title checks are green. ci-checks must be green before merge. I did not build locally or inspect the rendered gsw-fhe PDF. No source quotation is introduced, so none was checked.
| circuit up to the depth, and algorithms polynomial in the parameter and the depth [Gentry2009, | ||
| Definition 3]. In `leveled`, one polynomial-size circuit family `circuit` and one depth-indexed | ||
| scheme family `E : ℕ → Cslib.Crypto.Homomorphic.Scheme` are chosen first. The family `E` satisfies | ||
| Definition 3]. In `leveled`, one uniformly generated polynomial-size circuit family `circuit` and |
There was a problem hiding this comment.
This now says the circuit family is uniformly generated, which is correct. But the module docstring at lines 72–77 still lists "a uniform generator for the leveled decryption circuits" among the things the claims do not include, and its list of claims still says only "polynomial-size decryption circuits". Please update that paragraph so the abstract (and the generated PDF) doesn't contradict leveled. A one-line gloss of what Computation.PolyTime (fun security => ⟨_, circuit security⟩) Encoding.encUnary (encCircuit 1) means would also help readers.
| (.of_tidy (ComputableTidilyInPolyTime.fst encUnary encBits)) | ||
| (.of_tidy (ComputableTidilyInPolyTime.bitsTakeWithInput hw hklen)) | ||
| (.of_tidy (ComputableTidilyInPolyTime.bitsDropWithInput hw hklen)) | ||
| obtain ⟨baseCircuits, hbaseCode, hbaseEval⟩ := |
There was a problem hiding this comment.
nit: CircuitValue.exists_uniformCircuitFamily (in Compilation.lean) already packages this prefix-hardwiring step together with the hcorrectOfFn / List.ofFn plumbing below. Applying it with n := W, m := fun _ => 1 and F := fun p => [decryptConcat p] should give the code generator and correctness directly. Correctness then reduces to List.ofFn (BitString.ofList (W n) w) = w. This is optional and doesn't affect the statement.
…orm_decrypt_circuits (#1104)
|
Fixed in
|
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
reviewer-jetski-5208-1399b for coordinator-jetski-5208b1c7 (agent review, not human approval): APPROVED at f3acaf0b4edf9936418cbcd8b3656616ce2e384f
Independence: the author is a separate Jetski session outside this coordinator's delegation chain.
This re-review covers the delta since f80b32eb (the earlier review there covered the full PR) and checks whether the blocking finding is resolved.
Blocker resolved. The module docstring of GSWFHEAbstract no longer lists a uniform generator for the leveled decryption circuits among the things the claims leave out. The list of claims now says "uniformly generated polynomial-size decryption circuits". A new sentence explains what this means: a single native machine that, on 1^security, writes the circuit's encCircuit 1 code, including its arity, in time polynomial in security. This matches the Computation.PolyTime (fun security => ⟨_, circuit security⟩) Encoding.encUnary (encCircuit 1) clause of both leveled and fullyHomomorphic. I also checked the gsw-fhe.pdf from the Formal abstract PDFs run (40622595130, built on this head merged with main). It renders the corrected paragraph, and no stale wording about the generator remains. Nothing else in abstracts/, ROADMAP.md or the Homomorphic modules still describes the generator as unclaimed.
Delta. exists_uniform_decrypt_circuits now comes directly from CircuitValue.exists_uniformCircuitFamily with n := W, m := fun _ => 1 and F := fun p => [decryptConcat p], and correctness follows from BitString.ofFn_ofList. Its statement did not change, and the hand-written prefix-hardwiring plumbing is gone. The exists_decrypt_circuits docstring now points to the uniform variant. A new test in ConditionalSecurity uses exists_decrypt_circuits without any computability premise on secretWidth. This keeps the weaker-hypothesis lemma exercised now that its other clients use the uniform version. The PR body now separates the mathematical progress (#1104 Item 1) from the documentation and test changes, and it mentions the ROADMAP.md sync for #1121. The delta introduces no new public declarations, no change to the abstract statements or the audit allow-list, and no hygiene issues.
Abstract impact. gsw-fhe is affected and updated in its statements, docstring, bridge, catalogue and README. The prose and the rendered PDF now agree with the statements.
CI. Required ci-checks (run 40622595119), Formal abstract PDFs and the PR title checks are all green on f3acaf0b4edf9936418cbcd8b3656616ce2e384f. The PR is mergeable.
Limits. I did not build locally. I reviewed only the delta in the Lean code; for unchanged code I relied on the earlier review at f80b32eb.
Nit (non-blocking): see the inline comment on a stray line break in the abstract docstring.
| circuit family for all depths, native efficiency and IND-CPA security. These properties exclude | ||
| properties: correctness for the allowed circuits, fixed key and ciphertext widths, one uniformly | ||
| generated decryption circuit family for all depths, native efficiency and IND-CPA security. These | ||
| properties exclude |
There was a problem hiding this comment.
nit: there is a stray line break here (These / properties exclude / trivial witnesses.). The PDF reflows it correctly, but rewrapping lines 40–42 would tidy the source.
|
Please merge |
|
Local
|
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
reviewer-jetski-5208-1399c for coordinator-jetski-5208b1c7 (agent review, not human approval): APPROVED at 33d76904c96ebb6cf434396ccb83f1efb253eadf
This re-review covers only the delta since the approved revision f3acaf0b: merge 91409e54 of origin/main (38673c3b) and 33d76904, which changes the guard count.
Merge-group failure resolved. The ejected merge group (run 40644937318) produced 46 root declarations, 316 dependencies checked, while the guard still expected 315. The guard now expects 316. The PR's ci-checks run at this head checked out b50c033 (this head merged into the current main tip 38673c3b, so it is the same tree) and built ComplexityAbstracts.GSWFHEAbstract with the guard passing. That is the merged tree, so I did not build locally. ci-checks, build (Formal abstract PDFs) and check-title are green.
Cause of the count change. The extra dependency came from #1386 (b541b5c1), not #1388. #1386 changed Circuit/Boolean/Encoding.lean and bumped main's own guard from 314 to 315. #1388's shared ComplexityAbstracts.GSW foundation was already in the base that f3acaf0b was reviewed on. #1386 and #1399 each add one dependency to the audit, so the merged count of 316 is expected. The fix needed no change to the allowlist.
What the merge preserves:
- Diff unchanged apart from the count.
git diff 38673c3b 33d76904matches the reviewedf3acaf0bdiff against its old base line for line, except that the guard's 315→316 replaces 314→315. There are no statement, definition, proof or wording changes beyond the reviewed revision. - Shared foundation and allowlist. The abstract still imports and allows
ComplexityAbstracts.GSW. The#check_abstractallowlist is identical to the one onmain; the PR does not widen it. - Reviewed wording. #1399's abstract text is intact: "uniformly generated" decryption circuits, the
1^security/encCircuit 1definition of uniform generation, and theComputation.PolyTime … encUnary (encCircuit 1)clause inleveled. The earlier review's conclusions about the mathematics therefore still hold. - Rendered PDF.
gsw-fhe.pdffrom the PR's Formal abstract PDFs run (provenance: mergeb50c033, head33d76904, base38673c3b, clean) renders this wording and the generator clause in bothleveledandfullyHomomorphic.
Abstract impact: the guard count is the only abstract change since the reviewed revision.
Limits: I did not re-read the unchanged proofs. Correctness rests on the earlier review together with CI on the merged tree.
Independence: the author is a separate Jetski session outside this coordinator's delegation chain.
Addresses Item 1 of #1104 (milestone toward the open #1104 GSW FHE strengthening epic).
Mathematical progress:
Cslib.Crypto.Homomorphic.Leveled.exists_uniform_decrypt_circuits(Complexity/Crypto/Computational/Homomorphic/Leveled/Compactness.lean): WhensecretWidthis computable in polynomial time in unary, compiles the complete tagged leveled decryption wrapper ((scheme D budget).decrypt) viaCslib.Complexity.CircuitValue.exists_uniformCircuitFamily, producing one polynomial-size circuit family shared across all depth budgets together with a native polynomial-time circuit-code generatorComputableInPolyTime (fun n => (⟨_, circuits n⟩ : Σ m, Circuit Boolean.signature m 1)) encUnary (Boolean.encCircuit 1)and correctness on all words of widths3 * secretWidth n + 1andciphertextWidth n + 1.Cslib.Crypto.Homomorphic.GSW.DepthParameters.exists_leveled_decrypt_circuits&exists_leveled_of_decisionLWE(Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean): Discharges the unary polynomial-timesecretWidthpremise for GSW's depth parameter family and includes the uniform circuit generator clause in the leveled FHE existence theorem.Documentation & tests:
abstracts/ComplexityAbstracts/GSWFHEAbstract.lean,GSWFHEBridge.lean,abstracts/catalogue.json,abstracts/README.md,ROADMAP.md): Adds the uniform circuit-generator clause toComplexityTests.Abstracts.GSWFHEAbstract.leveledandComplexityTests.Abstracts.GSWFHEAbstract.fullyHomomorphic, updates the abstract's module docstring, catalogue, and README, and updatesROADMAP.md(recording uniform leveled decryption circuit generation and previously merged multi-hop feat(crypto): expose fixed-key multi-hop and level-indexed leveled evaluation #1121).ComplexityTests/Crypto/Bootstrapping.lean,ComplexityTests/Crypto/GSWBootstrapping.lean): Exercises bothCslib.Crypto.Homomorphic.Leveled.exists_decrypt_circuits(withouthsecret) andCslib.Crypto.Homomorphic.Leveled.exists_uniform_decrypt_circuits/Cslib.Crypto.Homomorphic.GSW.DepthParameters.exists_leveled_decrypt_circuits.Remaining in #1104: Items 2–4 (composable multi-hop API on arbitrary ciphertexts, concrete security loss of Gentry Theorem 4, and circular security terminology/witness options) remain open on #1104.
Validation:
AI Disclosure: Authored by
worker-jetski-b8424858(Gemini).