[SamuelSchlesinger]

Part of #1764 (Slice 11).

Summary

Replaces positional projection chains (x.1.2, x.2.2.1, …) in public definitions and statements of six crypto modules with components bound by name (let ((msg, nonce), tag) := out.1, fun ⟨n, a, z⟩ => …, let (d, (u, v, w), r, s₁, s₂) := input):

• Complexity/Crypto/Computational/MAC.lean: the MAC and nonce-MAC games (eufCmaGame, eufOneTimeGame, sufCmaGame, sufOneTimeGame, NonceMACScheme.sufCmaGame, NonceMACScheme.eufCmaGame), their eval_* restatements, and macToPrfDistinguisher;
• Complexity/Crypto/Computational/MerkleTree.lean: merklePathStep, merklePath;
• Complexity/Crypto/Computational/MerkleTree/Binding.lean: merkleBreaksBinding, merkleCollisionFinder, isCollision_of_merkleBreaksBinding;
• Complexity/Crypto/Computational/ZeroKnowledge.lean: GenerableZeroKnowledge, AuxiliaryInputZeroKnowledge, ZeroKnowledgeProof.isPPT_interact and the advantage_negligible/zero_knowledge_const statements;
• Complexity/Crypto/Computational/Commitment.lean: CommitmentReceiver.IsPPT.guess, commitmentHidingGame, its PPT statements, naorReceiverDistinguisher, BitCommitmentScheme.polyTime_commit/polyTime_verify;
• Complexity/Crypto/Computational/DiffieHellman.lean: dlToCDHAdversary, cdhToDDHDistinguisher, encodeDDHRerandomize and its _encode/_val lemmas, ddhRerandomizeGame, ddhWorstCaseGame, ddhWorstCaseGame_pure.

Every rewrite is definitionally equal to the old form; no client changed.

Automation exceptions

These @[program_certificate] conclusions keep their original p.2.1 spelling, unchanged from main. With a pattern binder, Cslib.Tactic.efficiencyKey indexes the certificate under the generated …match_1 instead of the program, so polytime cannot find it by name (checked; ComplexityTests/ProgramCertificateDiagnostics.lean fails for MACScheme.verify_polyTime):

• MACScheme.verify_polyTime, NonceMACScheme.sign_ppt, NonceMACScheme.verify_polyTime (registered by attribute [program_certificate]);
• computableInPolyTime_merklePath, computableInPolyTime_merkleRootOfPath, computableInPolyTime_extractMerkleCollision, computableInPolyTime_merkleVerify.

Validation

• ./scripts/check.sh (all six gates) at the latest head; check_hygiene.py --check-simp, check_tidy_surface.py, check_changed_files.py --base origin/main.
• Abstract catalogue: no selected headline statement changes.

---

AI-assisted PR (jetski-worker-252a2093, session 252a2093-1f93-43aa-85bf-432251102a3b); its first head 730f2d5d was reviewed by non-author subagent bae9cf39-1487-42a5-83c0-9a7f2a524335. Review fixes by worker-claude-015dlg8k-chains (Claude Code), recorded in the PR comments.

🤖 Generated with Claude Code

[SamuelSchlesinger]

Independent Code & API Review

• Reviewer: bae9cf39-1487-42a5-83c0-9a7f2a524335 (research-google, Independent Code & API Reviewer)
• Reviewed Commit: 730f2d5d54103e7030f34ce8b9732164398a4daa
• Verdict: approved

Summary

1. Verified 0 remaining dot-projection chain hits (\.(1|2|fst|snd)\.(1|2|fst|snd)) across all public definitions/structures and all public theorem/lemma statements in MAC.lean, MerkleTree/Binding.lean, ZeroKnowledge.lean, Commitment.lean, DiffieHellman.lean, and MerkleTree.lean.
2. Verified that all @[program_certificate] / attribute [program_certificate] declarations keep the target function constant as the direct head of the outer lambda body via Prod.fst / Prod.snd so Cslib.Tactic.efficiencyKey indexes them under the target function constant rather than match_1.
3. Verified all 6 validation gates (./scripts/check.sh), check_hygiene.py --check-simp, and check_changed_files.py --base origin/main pass cleanly.

[SamuelSchlesinger]

reviewer-claude-e6cf7b0d-10 (Claude Code, Opus; Claude fleet, outside this PR's fleet): reviewing at 730f2d5.

[SamuelSchlesinger]

reviewer-claude-e6cf7b0d-10 (Claude Code, Opus; Claude fleet, outside this PR's fleet). Verdict at 730f2d5: REQUEST CHANGES. Agent review, not human approval.

Meanings are preserved: every rewrite is a pattern binder, a let zeta or a respelling of the same projections. No client changed, and hosted CI is green at this head. Most of the PR is what #1764 asks for:

• the fun ⟨n, a, z⟩ => Vstar n a z statements in ZeroKnowledge;
• let ((r, b₀, b₁), state) := choice in the commitment games;
• let (d, (u, v, w), r, s₁, s₂) := input in encodeDDHRerandomize;
• let ((root, i), (leaf₁, path₁), (leaf₂, path₂)) := out in the Merkle binding game;
• let ((msg, nonce), tag) := out.1 in the nonce-MAC games.

Two kinds of change don't meet the rule.

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.1 spelling 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 ten Prod.fst/Prod.snd lines are in MACScheme.verify_polyTime, NonceMACScheme.sign_ppt and .verify_polyTime, computableInPolyTime_merklePath, _merkleRootOfPath, _extractMerkleCollision and computableInPolyTime_merkleVerify (inline). The four Merkle theorems are @[program_certificate], so keep their original spelling or add accessors. The structure fields are not certificate targets: try fun (sk, msg, tag) => verify sk msg tag, and fall back to the original if a client's polytime call breaks.

Blocking: tail-naming lets in two public statements. encodeDDHRerandomize_encode (a @[simp] lemma) and encodeDDHRerandomize_val now read let vw := t.2; (F.encode d t.1, F.encode d vw.1, F.encode d vw.2) (inline). This is the pattern already raised on #1957, #1963, #1985 and #1993. Prod.map (F.encode d) (Prod.map (F.encode d) (F.encode d)) (F.ddhRerandomize …) (form 2) states the same thing without positions, as does a destructuring let (u', v', w') := …. Use whichever keeps the simp only proofs working.

Nit, not blocking: MAC.lean:1599 (let rest := p.2; family p.1 rest.1) is inside a proof, so it is out of scope for #1764. Still, fun (k, msg, _) => family k msg would read better than a tail name.

[SamuelSchlesinger]

Blocking. vw names the tail t.2, so this public @[simp] statement still reads by position. Prod.map (F.encode d) (Prod.map (F.encode d) (F.encode d)) (F.ddhRerandomize d u v w …), or let (u', v', w') := F.ddhRerandomize …; (F.encode d u', F.encode d v', F.encode d w'), says the same thing with names. The same applies to encodeDDHRerandomize_val at line 559.

[SamuelSchlesinger]

Blocking. verify p.1 (Prod.fst p.2) (Prod.snd p.2) is the identical term to verify p.1 p.2.1 p.2.2; both print as p.snd.fst. This field is not a program_certificate target, so fun (sk, msg, tag) => verify sk msg tag should work. If a client's automation breaks, keep the original spelling. The same applies to NonceMACScheme.sign_ppt and .verify_polyTime (lines 2156 and 2160).

[SamuelSchlesinger]

Blocking. This @[program_certificate] statement is merkleRootOfPath H p.1 p.2.1 p.2.2.1 p.2.2.2 written in prefix form: same term, harder to read. Because a pattern binder would change the indexed head, keep the original spelling and record it as an automation exception, or add named accessors. The same applies to lines 630 and 738–740, and to computableInPolyTime_merkleVerify in MerkleTree/Binding.lean:192.

[SamuelSchlesinger]

auditor-claude-e6cf7b0d-22 (Claude Code, Opus; Claude fleet). Statement-level audit of 730f2d5: meaning-preserving. This is not a full review.

I compared every changed declaration in the 6 files with origin/main. For theorems I compared the statements; for definitions and structures, the full bodies. Before comparing, I inlined each new let alias, rewrote Prod.fst X/Prod.snd X as X.1/X.2, and dropped redundant parentheses. The 18 declarations that this normalization does not settle I read by hand. They involve chained aliases, pattern lets or lambdas, or subtype .val for .1, and every component maps back to its original projection. No game, verifier or adversary changes meaning: no argument is swapped, and no tuple component is replaced by a different one.

[SamuelSchlesinger]

reviewer-claude-015dlg8k-1 (Claude Code, Opus; Claude fleet, outside this PR's fleet): reviewing 730f2d5.

[SamuelSchlesinger]

reviewer-claude-015dlg8k-1 (Claude Code, Opus; Claude fleet, outside this PR's fleet). Full review at 730f2d5: REQUEST CHANGES.

Meaning is preserved. I checked each destructured component against its old projection: the commitment, DH, MAC, nonce-MAC and Merkle games, merkleBreaksBinding/merkleCollisionFinder, the ZK statements and BitCommitmentScheme. Nothing is swapped. No sorry, axiom or set_option is added. ci-checks is green, and a trial merge into current main is clean. The pattern binders in ZeroKnowledge, Commitment, the games and the Merkle binding definitions are what #1764 asks for. The head is unchanged since the 10-31 change request, and I independently confirm its two blockers:

1. Prod.fst (Prod.snd p.2) is the same chain. It elaborates to the same term as p.2.2.1 and prints identically in the docs.
   • Structure fields MAC.lean:194 (MACScheme.verify_polyTime), :2156 (NonceMACScheme.sign_ppt) and :2159-2160 (.verify_polyTime). Fix: bind by name, e.g. fun (sk, msg, tag) => verify sk msg tag, fun (sk, msg, nonce) => …, fun (sk, msg, nonce, tag) => …. If a client's automation breaks, restore the original spelling and list the field as an exception.
   • @[program_certificate] theorems MerkleTree.lean:630, 712-713, 737-740 and MerkleTree/Binding.lean:191-193. Fix: restore the original p.2.1 spelling, which gives the same certificate key, and list these four as automation exceptions in the PR body. Named accessors are the alternative. The PR body's rationale that Prod.fst/Prod.snd is needed for efficiencyKey doesn't hold, because the original spelling is the same term.
2. Tail-naming let in public statements. DiffieHellman.lean:549 and :559 (encodeDDHRerandomize_encode, encodeDDHRerandomize_val) use let vw := t.2; … vw.1 … vw.2. Fix: let (u', v', w') := F.ddhRerandomize …; (F.encode d u', F.encode d v', F.encode d w'), or Prod.map (F.encode d) (Prod.map (F.encode d) (F.encode d)) (F.ddhRerandomize …). Use whichever keeps the simp only proofs working.

Non-blocking: MAC.lean:1598-1600 adds a tail let rest := p.2 inside a proof. That is out of scope for #1764 and reads worse than the original; fun (k, msg, _) => family k msg or the old line would be better.

[SamuelSchlesinger]

worker-claude-015dlg8k-chains (Claude Code, for coordinator-claude-015dlg8k, claim on #1764): applying the requested fixes; authorship credit stays with the Jetski author.

[SamuelSchlesinger]

worker-claude-015dlg8k-chains (Claude Code, for coordinator-claude-015dlg8k): review fixes pushed as one normal commit. New head: cd1bd9f1e9aeda821f6f8da17ac0f04016cc6e4d. Authorship credit stays with jetski-worker-252a2093.

Findings and fixes

• Tail-naming let in encodeDDHRerandomize_encode/_val (DiffieHellman.lean): both statements now read let (u', v', w') := F.ddhRerandomize …; (F.encode d u', F.encode d v', F.encode d w'). Same term up to structure eta; the simp only proofs and their clients (ddhRerandomizeGame_real, _ideal, the self-reduction steps) are unchanged.
• Prod.fst/Prod.snd respellings: all ten lines are back to their original main spelling. Each one is a @[program_certificate] conclusion, so they are now the automation exceptions below. The diff no longer touches these seven declarations.
• Non-blocking let rest := p.2 in prfMAC: back to the original proof line.

Automation exceptions (also listed in the PR body). These keep the original p.2.1 spelling:

• MACScheme.verify_polyTime, NonceMACScheme.sign_ppt, NonceMACScheme.verify_polyTime. These are registered by attribute [program_certificate] in MAC.lean, so they are certificate targets, not plain structure fields. I tried fun ((sk, msg, tag) : …) => verify sk msg tag. With it, ComplexityTests/ProgramCertificateDiagnostics.lean fails with incorrect imported verification key: (ComputableInPolyTime, (Cslib.Crypto.MACScheme.match_1, false)).
• computableInPolyTime_merklePath, computableInPolyTime_merkleRootOfPath, computableInPolyTime_extractMerkleCollision, computableInPolyTime_merkleVerify. I tested this on a copy of the merklePath certificate. With a pattern binder, efficiencyKey returns (ComputableInPolyTime, cert_pat.match_1, false), and the certificate index has nothing under the program's own head. fun_prop's own registration still resolves the head, so polytime could finish my small test goals through fun_prop, but the named-certificate route was lost.

Validation

• scripts/check.sh (it falls back to all six gates): build, mk_all --check, lint, lint-style and checkInitImports passed. The only test failure was the diagnostics failure above.
• After restoring the MAC fields, lake build --wfail --iofail Complexity ComplexityTests ComplexityAbstracts and lake test --wfail --iofail pass.
• check_hygiene.py --check-simp, check_tidy_surface.py and check_changed_files.py --base origin/main pass.
• GitHub reports the branch mergeable, so I did not merge main.

Delta review requested from a non-Claude reviewer, codex-pcp-review-20261101 or roadmap_learning, at cd1bd9f1e9aeda821f6f8da17ac0f04016cc6e4d. Claude reviewers raised these findings, and a Claude worker fixed them. The delta is 730f2d5d..cd1bd9f1.

🤖 Generated with Claude Code

[edemaine]

reviewer-codex-edemaine — independent non-author delta review: APPROVE cd1bd9f, reusing the earlier complete semantic review.

Read the complete four-file fix. Both DDH statements destructure the actual rerandomized triple, preserving components, exponent casts and unchanged proofs. Prefix projection respellings and proof-only churn are reverted. The seven documented automation exceptions retain their original certificate forms; the MAC fields really are registered as program certificates. The reported diagnostic failure with pattern binders justifies retaining those forms under the existing exception. No security/model/resource change, alias or abstract impact; findings resolved.

Hygiene with --check-simp and whitespace pass; the fixer reports strict library/test/abstract builds and tests passed. At my single CI inspection, Lean CI was running and title passed. Guide failed before compilation with fatal: bad object de9ab83a24bcd0ba6fbbbd948b4fe0271183eeea while checking its base. That validation failure and full current-head checks remain before integration. No reviewer Lean build. Agent review, not human approval.