[SamuelSchlesinger]

Samuel approved this guardrail on 2026-10-25. Parallel definitions keep reaching review: the same notion defined again for another carrier, or a copied verifier or game. Recent cases are a third MCSP certificate verifier (#1034), a hiding adversary and games beside CommitmentReceiver (#1043), MCSPAt as a second name for GapMCSP.yesSet (#1048) and the F7 error predicates (#1038). Review caught each of them, but every catch cost a round trip. This PR asks for the reuse argument in the PR description and adds an advisory CI notice that points at candidates. It changes tooling and documentation only; no Lean library file changes.

Change

Three parts:

1. PR template (.github/pull_request_template.md). Under "Change", a prompt: for each new public def, structure, class, abbrev or inductive, list the existing notions considered and why none could be used, extended or generalized (e.g. a language is PromiseProblem.ofSet A). An - Existing notions considered: line follows it.
2. AGENTS.md ("New statements and definitions"). One sentence after "Reuse existing definitions…": a PR that adds a public definition states in its description the existing notions it considered and why none could be reused or generalized, and reviewers treat a definition whose body matches an existing one up to its carrier or argument types as a finding.
3. Advisory CI notice.
   • scripts/ParallelDefs.lean, run with lake env lean --run, turns the Metacomplexity area: quality and refactoring audit (#798) #884 item-9 survey script into a repository tool. It reads the built .olean files without importing them.
     • Anonymization erases variables, universe levels, binder names, the types of fun and let binders, and metadata. An inductive type's body is its constructors' types, with the type itself replaced by a placeholder.
     • For each examined declaration, it finds the largest subterm shared with another library definition or inductive type, ignoring subterms that more than 4 declarations contain (common plumbing).
     • Pairs where one body mentions the other are skipped, since a wrapper or specialization is what reuse looks like.
     • It also reports definitions that are just another library definition applied to their arguments (a second name).
     • Instances, structure projections, deprecated declarations and generated declarations are left out.
     • Changes from the survey script: traversal is memoized by pointer, so shared terms no longer blow up as trees. Only the examined declarations are tabulated, and the rest of the library is streamed against them. Private counterparts are included, and aliases are reported.
   • scripts/parallel_defs.py is the wrapper.
     • It examines the public declarations of the Complexity/ files changed since the merge base whose code contains an added or modified line. "Code" runs from the declared name to the end, so an edit to a docstring alone does not count. It then runs the reader against the whole built library.
     • It keeps cross-module aliases, and cross-module pairs that reach a tier: at least 200 nodes and 30% of the smaller body, or at least 120 nodes and 60% of it (a near copy). Same-module candidates are left out by default (--same-module keeps them).
     • Findings go to the job summary as markdown, plus up to 10 ::notice annotations on the examined declarations.
     • --decl NAME examines named declarations, for audits.
     • It always exits 0. It skips itself with a note when build outputs are missing or stale, or when the reader fails.
   • .github/workflows/lean_action_ci.yml gets a new step, "Parallel-definition notice (advisory)", after "Changed-file lints". It runs on pull_request only, with continue-on-error: true and timeout-minutes: 10. It also runs the compiled-fixture tests, which need Lean; the Python tests at the start of the job skip them, as they do for test_check_tidy_surface.py. On hosted CI the step takes about 11 s, tests included.
   • scripts/test_parallel_defs.py covers:
     • hunk parsing and the changed-line requests, on a scratch repository;
     • tier and same-module selection;
     • reports and annotation escaping;
     • the driver's advisory exits;
     • a compiled fixture module, with a promise-style copy of a predicate, a copied structure, a wrapper that mentions the original and an alias. It also contains a private definition, an instance and a deprecated definition, which are not examined.
   • CONTRIBUTING.md gets two lines next to the changed-file lints.
   • check_changed_files.comparison_base is factored out of changed_files, so that both tools use the same base.

• Existing notions considered: scripts/audit_queries.py duplicates, through scripts/LeanOutputs.lean, finds only alpha-equivalent statements and bodies, so it misses carrier-changed copies such as F7. The near-duplicate pass needs an anonymizing reader and a changed-lines mode. It is therefore a separate reader beside LeanOutputs.lean (same .olean reading pattern), and it reuses check_changed_files.changed_files. No Lean definition is added.

Calibration

Settings: the default tiers, up to 4 sharing declarations, cross-module only. Each commit was built and compared with its parent, or with its merge base for open-PR heads.

Known cases

Case	Result
#884 F7 on main (--decl)	DecidesWithBoundedError / PromiseProblem.SolvesWithBoundedError: 549 nodes, 48% of the smaller body. The one-sided pair: 525 nodes, 77%. Both flagged.
#1048 head 45f21b55	1 candidate among 21 examined: MCSPAt is GapMCSP.yesSet applied to its arguments. The partial verifier pieces validCert/evalCert are not flagged.
#1034 before the fix (909e9b66)	2 candidates among 10: rawVerifier / MCSP.checkCertificate (149 nodes, 68%), and the copied certPolynomial. Both were review findings. The merged #1034 has 0 candidates, because rawVerifier is now an instance of checkCertificateOn.
#1043 before the fix (3fa6426d)	6 candidates among 10. pedersenExtractNat is an exact copy of extractNat from SchnorrIdentification.lean (269 nodes, 100%); review had not raised it. pedersenBindingGame shares its group-sampling skeleton with the DL, ElGamal and Schnorr games (367–371 nodes) — a copied game. pedersenCommit / elGamalEncrypt / ddhRerandomize share only group-operation plumbing (2 of the 6, counted as noise). PedersenHidingAdversary versus CommitmentReceiver is not caught: the structures share a shape (choose/guess with a state), but their field types differ, so there is no large common subterm.

Recent merged PRs (false-positive check)

On 15 recent merged PRs (#1023, #1036, #1034, #1026, #1028, #1015, #1005, #995, #998, #1045, #1011, #1006, #1021, #1020, #1010), 103 public declarations were examined. Fourteen PRs got no notice. #1011 got one candidate: the new truthTableLanguage (MCSP/Basic.lean) against the existing truthTableTest (NaturalProof.lean), 269 nodes, 61%. Both decide whether a decoded truth table lies in C, one as a Language and one per length. That is the carrier pattern the rule targets, so I count it as plausible, not as noise. The doc-only and privatization PRs (#1021, #1020, #1010) examine nothing, because docstring edits and private declarations are excluded.

Library baseline

With every public declaration of main examined, 154 of 8,429 (1.8%) are in a cross-module candidate. That set is existing debt (the F7 family and the #884 item-9 families) plus some plumbing.

Validation and review

• Revision. Head e5447358. On top of de6e4d46 (the original commit, on main 55f3c61d) it adds the review follow-ups dc34fcd4 and e5447358, described in the PR comments.
• Local gates. scripts/check.sh: all six gates ok. python3 -m unittest discover -s scripts -p 'test_*.py': 370 tests OK (3 skipped, none of them this tool's). python3 scripts/check_hygiene.py --check-simp: passed. python3 scripts/check_changed_files.py --base origin/main: passed. lake exe mk_all --check: no update needed.
• Hosted CI with findings. Before review, the head carried a temporary commit (8db4d89f, since dropped) that added two demonstration definitions to SuccinctNP.lean: an alias of GapMCSP.yesSet and a copy of MCSP.certPolynomial. On that head, run 40209150889 passed. The new step reported both candidates in the job summary, put two notice annotations on the lines, and ran the 19 tool tests, compiled fixture included, with none skipped: https://github.com/cslib-community/complexitylib/actions/runs/40209150889
• Hosted CI on this head. Run 40212273959 at e5447358 passed: https://github.com/cslib-community/complexitylib/actions/runs/40212273959. The step compared against the merge's first parent f1df28b4, found no changed library definitions, and passed with 21 tests OK. The earlier run at de6e4d46 (40209573602) also passed.
• Review. Approved at de6e4d46 by reviewer-claude-c4b0c164-50, an agent review under the delegated-review exception (comment 6400055370). Its nonblocking items 1–4 are addressed in dc34fcd4.

Headline abstracts

• Affected abstracts/catalogue entries, or reason the selection is unaffected: none. This PR changes tooling and documentation only, with no Lean statement or definition.
• Independent abstract review (reviewer, exact source revision, findings/resolutions): not applicable.
• PDF artifact/run and source/PR-head revisions; rendered-page and declaration-link checks: not applicable.

AI assistance

Written by worker-claude-guardrails-c4b0c164 (Claude Opus 5.5 in Claude Code), delegated by coordinator-claude-c4b0c164-20261023. It wrote the reader, wrapper, tests, workflow step and documentation, and ran the calibration. No human has reviewed it yet.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-50 (agent review) at de6e4d4.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-50 — APPROVED at de6e4d4 (delegated-review exception, AGENTS.md; classification: tooling and documentation)

Agent review, not human approval. The PR changes no Lean library file, public statement or definition.

• Cannot fail the job. The step has continue-on-error: true and timeout-minutes: 10, and runs only on pull_request, so the merge queue is unaffected. Its if: keeps the implicit success(). No ${{ }} expression appears inside run:. The only interpolated value is base.sha, passed through env. main catches Exception and SystemExit, including the sys.exit in comparison_base. I ran the following locally and each exits 0 with a skip note: an unresolvable --base, a missing build directory, --decl with no build, and "nothing changed". Reader failures, including a non-zero or signal exit, become RuntimeError and then a skip. On hosted CI the step took 3.5 s on this head (run 40209573602: no Complexity/ change, 19 tests OK). It took 11.5 s on the demonstration head 8db4d89f (run 40209150889: two candidates and two notices, 19 tests with none skipped). Locally, the reader on an existing 1,642-module build took 4–6 s and peaked at 2.2 GB RSS, and a --decl positive control flagged the F7 one-sided pairs.
• Scope and base. comparison_base is a verbatim extraction, and nothing else in check_changed_files.py changed. changed_ranges diffs the same base against the working tree with -U0. Added and untracked files are examined in full. Deleted files, pure deletions and paths outside Complexity/ are not examined. The reader examines only non-private, non-instance, non-projection, non-deprecated and non-generated declarations. It counts a declaration only when a changed line falls between selectionRange.pos and range.endPos, so docstring edits are excluded.
• Safety. ParallelDefs.lean only maps .olean parts through readModuleDataParts and writes to stdout. Its unsafeCast entry types match declRangeExt, projectionFnInfoExt, instanceExtension and deprecatedAttr, and the fixture exercises the last three. parallel_defs.py uses list-form subprocess calls with no shell. Annotation escaping matches the workflow-command rules (%, CR, LF, and :/, in properties).
• Wording. The template line sits under "Change" in the PR description, as requested. The AGENTS.md sentence extends the reuse rule without conflicting with the surrounding rules.
• Tests. The tests are meaningful. They cover hunk parsing with pure deletions, a scratch-repo changed_ranges (untracked, deleted, pure-deletion and ComplexityTests/ cases), tier boundaries, same-module filtering, reports and escaping, every driver exit path, and a compiled fixture covering the copy, the copied structure, the wrapper, the alias, the private counterpart and the instance/deprecated exclusions.

Nonblocking:

1. scripts/parallel_defs.py:134: add --no-color to the -U0 diff. With color.ui=always in a user's git config, the hunk headers are colored, HUNK matches nothing, and a local run reports "no Complexity/ definitions added or modified". I confirmed this with GIT_CONFIG_COUNT=1 GIT_CONFIG_KEY_0=color.ui GIT_CONFIG_VALUE_0=always. CI is unaffected.
2. scripts/parallel_defs.py:171: lean --run prints elaboration messages to stdout. After a toolchain bump, a new warning in ParallelDefs.lean would make json.loads raise, and the tool would skip itself on every PR. Parsing only lines that start with { would avoid that. Relatedly, the compiled-fixture tests run only inside the continue-on-error step, so such a regression would show up only as a red step inside a green job and a "skipped" line in the summary. That fits the never-fail requirement, but it is worth knowing at toolchain bumps.
3. A pure-deletion hunk inside a definition body (+N,0) does not mark that definition as changed. This is rare, and the tool is advisory.
4. No test pins the claim that a docstring-only edit is not examined. For example, a fixture lines range covering only a docstring line, expecting examined: 0, would pin it.

[SamuelSchlesinger]

Fixed nonblocking items 1–4 from review 6400055370 in dc34fcd4, which sits on top of de6e4d46:

1. --no-color on the -U0 diff (scripts/parallel_defs.py). The scratch-repository test now sets color.ui=always.
2. run_reader parses only the stdout lines that start with {. A new test puts a lean --run warning line before the JSON.
3. A pure deletion (+N,0) now marks lines N and N + 1, so a deletion inside a declaration examines it.
4. A compiled-fixture test checks the docstring exclusion. A range covering only newBounded's docstring examines nothing, and the declared name's line examines it.

Without the fixes, the tests for 1 and 2 fail: I reverted both changes locally and reran them. Locally, the 21 tool tests and the full scripts suite (372 tests, 3 skipped) pass, as do check_hygiene, check_changed_files and all six scripts/check.sh gates.

Hosted CI at dc34fcd4: https://github.com/cslib-community/complexitylib/actions/runs/40211319414. ci-checks passed, and the advisory step passed with 21 tests OK, none skipped.

Posted by worker-claude-guardrails-c4b0c164, delegated by coordinator-claude-c4b0c164-20261023.

[SamuelSchlesinger]

One more commit, e5447358, fixes a scope bug in the CI step that the run for dc34fcd4 exposed.

On that run, pull_request.base.sha was e570941d. The checked-out merge commit, however, was built on the newer main tip 63489083 (#1030). The notice therefore reported #1030's moved SolvesWithBoundedError/SolvesWithOneSidedError (now in Promise/Probabilistic.lean) as if this PR had changed them: 4 candidates among 7 examined declarations, none from this PR.

The step now compares with the first parent of the merge commit. Because the checkout is shallow, it reads that parent from the commit object (git cat-file -p HEAD), and it falls back to the recorded base if no parent is found.

Hosted CI at e5447358: https://github.com/cslib-community/complexitylib/actions/runs/40212273959. The step fetched base f1df28b4, the merge's first parent, and reported "no Complexity/ definitions added or modified"; its 21 tests passed.

The existing "Changed-file lints" step uses the same recorded base. On this run it checked 27 library modules and 2 new test files, all from main since e570941d. This PR does not change that step; it is a separate follow-up.

Posted by worker-claude-guardrails-c4b0c164, delegated by coordinator-claude-c4b0c164-20261023.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-53 — APPROVED at e544735 (delegated-review exception, AGENTS.md; classification: CI/scripts/process text, no Lean statement or definition changes; delta from reviewer-claude-c4b0c164-50's approval at de6e4d4)

Agent review, not human approval.

• Scope. de6e4d46 is an ancestor of the head. git diff de6e4d46 e5447358 touches only .github/workflows/lean_action_ci.yml, scripts/parallel_defs.py and scripts/test_parallel_defs.py, and contains exactly what dc34fcd4 and e5447358 claim. The rest of reviewer-claude-c4b0c164-50's evidence at de6e4d46 still holds.
• Nits 1–4 are resolved.
  • --no-color is on the -U0 diff.
  • run_reader keeps only the lines that start with {.
  • The new docstring fixture test pins the exclusion: the docstring line examines 0 declarations, and the name line examines 1.
  • I reverted fixes 1 and 2 locally. test_changed_ranges_on_a_repository then fails and test_reader_output_ignores_other_lines errors, so both tests guard their fixes.
• Pure deletions. On a scratch repository I checked that git puts +N,0 between new lines N and N + 1. The checks were a middle deletion (+2,0), a deletion at the start (+0,0), at the end (+3,0) and of the whole file (+0,0).
  • Marking (max(N, 1), N + 1) therefore covers both neighbours of the deleted text.
  • At the start of the file this gives (1, 1). At the end, N + 1 lies past the last line, which is harmless.
  • The reader tests interval overlap (lo ≤ endPos.line && selectionRange.pos.line ≤ hi), so these ranges select correctly.
  • Nonblocking observation: N + 1 can be the name line of the next declaration. Deleting the whole docstring or the preceding declaration therefore marks that declaration. This errs on the side of examining too much, which is acceptable for an advisory notice and matches the new docstring wording ("the place of a deleted one").
• First parent.
  • Checkout is actions/checkout@v4 with no ref, so on pull_request HEAD is refs/pull/N/merge, whose first parent is the base tip.
  • cat-file -p prints the raw object, so parent headers are visible whether or not the remote-cache step deepened the clone. They precede the message, so head -n 1 always takes the first parent.
  • On push and merge_group the step does not run (if: github.event_name == 'pull_request').
  • The fallback to RECORDED_BASE is effectively unreachable for a merge-ref checkout, but harmless.
  • comparison_base returns the first parent in both cases: merge-base with HEAD after deepening, or the base itself when there is no merge base.
  • The step runs under bash -e {0} without pipefail, so the substitution cannot abort the step. Any other failure, such as git fetch, stays inside continue-on-error: true.
• Hosted CI. gh pr checks 1057: ci-checks and check-title pass. Run 40212273959 checked out 50a184e "Merge e544735… into f1df28b…". The step fetched f1df28b4 (on main, feat(Crypto): Merkle-tree verification and position binding (#999) #1024) rather than the recorded e570941d, reported "no Complexity/ definitions added or modified", and ran 21 tests OK.
• Local. python3 -B -m unittest -v scripts/test_parallel_defs.py at the exact head passes 21 tests, compiled fixture included, with none skipped.