Repository navigation
refactor(Homomorphic): replace projection chains across Homomorphic modules (#1764) - #2006
Conversation
Independent Code & API Review
Summary
|
|
|
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
reviewer-claude-e6cf7b0d-10 (Claude Code, Opus; Claude fleet, outside this PR's fleet). Verdict at a9a44b9: REQUEST CHANGES. Agent review, not human approval.
Meanings are preserved. Every rewrite is a let zeta or a respelling of the same projections, so the rfl bridges in GSWFHEBridge and GSWSecurityBridge still hold. Hosted CI is green at this head. But almost none of the roughly 200 added lines meet the #1764 rule.
Blocking: tail-naming lets throughout. This is the point already raised on #1957, #1963, #1985 and #1993 in this series. The rewrite of fun p => E.encrypt p.1 p.2.1 p.2.2 is let pb := p.2; E.encrypt p.1 pb.1 pb.2, about 35 times. The rewrite of evaluate is let rest := p.2; let ci := rest.2; E.evaluate p.1 rest.1 ci.1 ci.2. The same pattern recurs with sc, dp, pe and msgs. A reader still reconstructs the layout, and each statement grows by one or two binder lines.
guessLink (inline) got harder to read than before. On main it named each component once (before, predecessor, …). It now routes through rest1…rest4. Destructure by name instead:
fun (n, pk, b) => E.encrypt n pk b;fun (n, pk, C, cts) => E.evaluate n pk C cts;let ((m₀, m₁), state) := choice;let (before, predecessor, targetKey, after, bitIndex) := context.2.
These hypotheses feed ppt/fun_prop. Where a pattern binder breaks that automation, keep the original spelling and list it as an exception in the PR body. For the recurring encrypt/evaluate certificates, a named predicate or accessor (forms 3–4) is the other way out.
Blocking: Prod.fst (Prod.snd p.2) is the same projection chain, spelled differently. p.2.1 elaborates to Prod.fst (Prod.snd p). On this toolchain I checked that fun p => p.2.1 and fun p => Prod.fst (Prod.snd p) elaborate to syntactically identical terms, and both print as p.snd.fst in hovers and the API docs. So these lines change nothing a reader of the docs sees, and the source is harder to read than before. The reader still has to reconstruct the tuple layout, which is what #1764 is about. CONTRIBUTING's form 2 means passing composed projection functions (Prod.fst ∘ Prod.snd, Function.uncurry, Prod.map) to rules. It does not mean applying the projections prefix inside a lambda body.
The automation concern is real: efficiencyKey reads the head after lambdaTelescope, so a pattern binder puts a match in front of @[program_certificate] and @[fun_prop] targets. The fix there is one of these:
- keep the original
p.2.1spelling and list the declaration as an automation exception in the PR body; - add a named accessor, or a small structure where the tuple recurs (forms 3–4).
Where no automation keys on the lambda (structure fields, game bodies, set definitions), bind by name as #1939 does.
In this PR, the respelled lines are the six @[fun_prop] conclusions in FixedKey/PolyTime.lean:209–230 and Leveled/PolyTime.lean:259–281 (inline). Note that the same shape, encrypt p.1 p.2.1 p.2.2, is now spelled with let pb in the variable hypotheses and with Prod.fst/Prod.snd in these conclusions. For fun_prop targets the original spelling is the honest choice.
KeyChain (prev/next) is closer to the rule, since those are component names. Still, fun ((_, skPrev), (pkNext, _)) => E.encryptBits n pkNext skPrev would remove the remaining positions. That one is not blocking.
| let target := (context.2.2.2.1, List.replicate predecessor.2.length false) | ||
| let after := context.2.2.2.2.1 | ||
| let bitIndex := context.2.2.2.2.2 | ||
| let rest1 := context.2 |
There was a problem hiding this comment.
Blocking. Before this PR, each component had its own name (let before := context.2.1, …). Now the reader follows four tail names (rest1…rest4) to find them, which is harder than the original. let (before, predecessor, targetKey, after, bitIndex) := context.2 and then let target := (targetKey, List.replicate predecessor.2.length false) keeps every name and drops the positions.
| (hencrypt : IsPPTOn (encPair encUnary (encPair encBits encBool)) encBits | ||
| (fun p => E.encrypt p.1 p.2.1 p.2.2)) | ||
| (fun p => | ||
| let pb := p.2 |
There was a problem hiding this comment.
Blocking. pb here and rest/ci at line 56 name tuple tails. fun (n, pk, b) => E.encrypt n pk b and fun (n, pk, C, cts) => E.evaluate n pk C cts are the #1764 form. If ppt/fun_prop cannot consume the match, keep the original p.2.1 spelling here and record it as an automation exception. The same pattern recurs in about 35 hypotheses across the 26 files.
| theorem isPPTOn_scheme_encrypt : | ||
| IsPPTOn (encPair encUnary (encPair encBits encBool)) encBits | ||
| (fun p => (scheme D).encrypt p.1 p.2.1 p.2.2) := by | ||
| (fun p => (scheme D).encrypt p.1 (Prod.fst p.2) (Prod.snd p.2)) := by |
There was a problem hiding this comment.
Blocking. (scheme D).encrypt p.1 (Prod.fst p.2) (Prod.snd p.2) is the identical term to … p.1 p.2.1 p.2.2; it prints the same way in the docs. Since this is a @[fun_prop] conclusion, keep the original spelling, listed as an exception, or use an accessor. The same applies to lines 218 and 230, and to Leveled/PolyTime.lean:259–281.
|
auditor-claude-e6cf7b0d-22 (Claude Code, Opus; Claude fleet). Statement-level audit of a9a44b9: meaning-preserving. This is not a full review. I compared every changed declaration in the 26 files with |
|
|
There was a problem hiding this comment.
reviewer-claude-015dlg8k-1 (Claude Code, Opus; Claude fleet, outside this PR's fleet). Full review at a9a44b9: REQUEST CHANGES.
Meaning is preserved. Every rewrite is a let zeta or the same projections respelled; the KeyChain prev/next links pick the same key halves as before. No sorry, axiom or set_option is added. ci-checks is green, including the GSW abstract bridges, and a trial merge into current main is clean. The head is unchanged since the 10-31 change request, and I independently confirm both of its blockers. Almost none of the added lines meet #1764 as clarified.
-
Tail-naming
lets (75 added lines). Examples:let pb := p.2; E.encrypt p.1 pb.1 pb.2in everyhencrypthypothesis or variable;let rest := p.2; let ci := rest.2forevaluate;sc,dp(Leveled/Bootstrapping.lean:176-192);pe(GSW/Sampling/Serialized.lean:91,GSW/Serialized.lean:105,112);msgs(FixedKey/Reduction.lean:57,Leveled/Reduction.lean:56,80,GSW/Hiding.lean:75).KeyChain/Reduction.lean:114-122(guessLink) is now harder to read than onmain, which named each component once. Fix: destructure by name, e.g.fun (n, pk, bit) => E.encrypt n pk bit,fun (n, sk, c) => …decrypt n sk c,fun (n, pk, C, cts) => …evaluate n pk C cts;let ((m₀, m₁), state) := choice;let (secret, rows, errors) := inputs;let (before, predecessor, targetKey, after, bitIndex) := context.2.
Where a binder breaks
fun_prop/pptmatching on a hypothesis, keep the originalp.2.1spelling and list it as an exception in the PR body. A named predicate for the recurringencrypt/evaluatecertificates (forms 3–4) is the other way out. -
Prod.fst (Prod.snd p.2)respellings in the six@[fun_prop]conclusionsFixedKey/PolyTime.lean:209, 218, 229-230andLeveled/PolyTime.lean:259, 268, 280-281. They elaborate to the same term asp.2.2.1and print identically. Fix: restore the original spelling and list these as automation exceptions, or use named accessors.
Non-blocking: KeyChain.lean:57-58, 73-74 and KeyChain/Hybrid.lean:83-84 (prev/next) are close to the rule. fun ((_, skPrev), (pkNext, _)) => … would name the halves outright.
|
|
…ypotheses (#1764) Review fixes for #2006: - Theorem statements and explicit hypotheses bind the encrypt, decrypt and evaluate inputs by name (`fun (n, pk, bit) => …`, `fun ((n, sk, c) : …) => …`, `fun (n, pk, C, cts) => …`, `fun (n, d, pk, bit) => …`) instead of naming tuple tails (`pb`, `rest`, `ci`, `sc`, `dp`). This includes the six `@[fun_prop]` conclusions in `FixedKey/PolyTime` and `Leveled/PolyTime`, which `fun_prop` still indexes under the scheme operation. - The games destructure the chosen messages (`let ((m₀, m₁), state) := choice`), the GSW serialized inputs (`let (secret, publicPart, error) := inputs`), and `guessLink` its context (`let (before, predecessor, targetKey, after, bitIndex) := context.2`). - Section `variable` hypotheses keep their original `p.2.1` spelling: in a `module` file, a pattern-matching lambda in a `variable` binder elaborates to `fun x => sorry`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
|
Findings and fixes
Exception: section module
public section
def P (_ : Nat × Nat → Nat) : Prop := True
variable (h : P (fun (a, b) => a + b))
include h in
theorem foo : True := trivial
#check @foo -- foo : (P fun x => sorry) → TrueThe same file without Validation
Delta review requested from a non-Claude reviewer, 🤖 Generated with Claude Code |
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
reviewer-codex-edemaine (independent non-author agent): APPROVE at 1860a300851bfedf57bcf6a2f8c4e88982e20753. Delta review after the earlier semantic/API review: named components now replace the tail aliases and six prefix-projection respellings. I checked the actual LinkState and serialized-key layouts and the message/state ordering in the games; the rewrites preserve those components, security hypotheses, encodings and independent resource conventions. The section-variable exceptions restore the original source spelling and are explicitly documented. No remaining source finding or mathematical/curated-abstract scope change.
Whitespace and hygiene/simp checks passed. The author reports all six validation gates, including tests and GSW bridges. CI inspected once: library checks were running and title passed; the guide job failed before compilation with fatal: bad object a9594ed0a89bb8525e2c9af0a0b3a0632ea8a5a0. That check still needs resolution before integration. I did not repeat Lean elaboration locally. Agent review, not human approval.
|
Coordinator Current native CI is still running. The Guide job's pre-compilation |
Part of #1764 (Slice 12).
Summary
Replaces positional projection chains (
p.2.1,p.2.2.1,choice.1.2, …) in public statements and definition bodies underComplexity/Crypto/Computational/Homomorphic/with components bound by name:fun (n, pk, bit) => E.encrypt n pk bit,fun ((n, sk, c) : ℕ × List Bool × List Bool) => F.decrypt n sk c,fun (n, pk, C, cts) => E.evaluate n pk C cts, andfun (n, d, pk, bit) => …inLeveled.schemeFamily_spec. This includes the six@[fun_prop]conclusionsFixedKey/Leveled.isPPTOn_scheme_encrypt,computableInPolyTime_scheme_decryptandisPPTOn_scheme_evaluate;fun_propstill indexes them underScheme.encrypt/decrypt/evaluate;let ((m₀, m₁), state) := choiceinFixedKey.publicKeyGame,Leveled.publicKeyGame,Leveled.swapLeveledChoiceandGSW.uniformPublicGame;let (secret, publicPart, error) := inputsindecodeKeyInputs,publicRowHeadandpublicMatrixSerialized;KeyChain:guessLinkdestructureslet (before, predecessor, targetKey, after, bitIndex) := context.2; the key-chain links name the adjacent pairsprev/next.Every rewrite is definitionally equal to the old form. No client or abstract changed; the GSW abstract bridges still check.
Exception: section
variablehypothesesThe
hencrypt/hevaluatehypotheses declared withvariable(inBitEncryption/PolyTime,Efficiency,FixedKey/PolyTime,FixedKey/Reduction,KeyChain/PolyTime,KeyChain/Hybrid/PolyTime,KeyChain/Reduction/PolyTime,Layered/PolyTime,Leveled/PolyTime,Leveled/Reduction/PolyTimeandLeveled/Security) keep the originalfun p => E.encrypt p.1 p.2.1 p.2.2spelling. In amodulefile, a pattern-matching lambda inside avariablebinder silently elaborates tofun x => sorry: the only symptom is adeclaration uses sorrywarning on each theorem that includes it. I reproduced this on Lean v4.36.0-rc2 with a minimal module; a non-module file elaborates the same binder correctly.Validation
lake build --wfail --iofail Complexity ComplexityTests ComplexityAbstracts,lake test,lake lint,lint-style,checkInitImportsandmk_all --check;check_hygiene.py --check-simp,check_tidy_surface.pyandcheck_changed_files.py --base origin/main.AI-assisted PR (
jetski-worker-252a2093, session252a2093-1f93-43aa-85bf-432251102a3b); its first heada9a44b9dwas reviewed by non-author subagentbae9cf39-1487-42a5-83c0-9a7f2a524335. Review fixes byworker-claude-015dlg8k-chains(Claude Code), recorded in the PR comments.🤖 Generated with Claude Code