[SamuelSchlesinger]

Closes #1086.

Change

scripts/check_pr_names.py extracts the backticked tokens of a PR description (or any Markdown), keeps those that look like Lean names, and lists the ones the checked-out revision does not declare. It reads source text: Complexity/, ComplexityTests/, abstracts/, scripts/, every package under .lake/packages, and the toolchain's Init/Std/Lean when lean is on the path. Files are preselected with ripgrep when it is installed, otherwise in Python; a run takes 1–5 s on bodies of new names, but 8–45 s when tokens sit in large namespaces such as Nat. or when many unresolved names need a base lookup (the follow-up PR brings these under 2 s). Full names come from namespace blocks, and a token matches a full name or a dotted suffix of one. Structure fields, constructors, where auxiliaries, aliases, generated names (.mk, .ext_iff, .eq_1, …), to_additive/simps names, module names and scripts/*.py names also count. Expressions, paths, numbers, keywords/tactics, all-caps words, single letters, hypothesis names and lowercase words without an underscore are skipped.

Each unresolved name gets a note: did you mean X (the same last component is declared in this repo under another namespace), mentioned in N files (probably a variable or a private name), or not found in any source file. A name the repo declared at the base (--base, default the merge base with origin/main) is marked removed or renamed here, because refactoring PRs name what they remove. The script exits 0. --strict exits 1 when a reported name was not removed by the change. CLI: --pr N (via gh pr view N --json body), --file PATH|-, --event PATH, --root DIR, --github.

CI: the new step "PR description names (advisory)" runs on pull_request after the build, so the package sources are there. It uses the event-payload body, the merge commit, and the merge commit's first parent as base (same base logic as the parallel-definition notice). It has continue-on-error and writes to the job summary and a notice. Limitation: the payload body is the one from the latest push, so editing the description does not rerun the step. CONTRIBUTING now asks authors to run --pr N before requesting review. The tests (scripts/test_check_pr_names.py, hermetic, with and without ripgrep) run in the existing Python test step.

Tooling only: no Lean changes, no public statement changes. This qualifies for review under the delegated-review exception.

Validation and review

#1080 at c69067ba (--root = a checkout of pull/1080/head): 30 names checked, 22 reported, all not found in any source file. That includes nonceSignOracle, IsDiffUniversal, secureNonceMAC_of_isPRF, IsPRF, nonceGame_succProbability_le and randomNonceGame_succProbability_le*. git grep -w confirms none of the 22 occurs at that head. The 8 names that do exist (nonceGame, randomNonceGame, prfPadDistinguisher, Nodup, …) were accepted.

20 recently merged PRs (#1036–#1075), each checked at its merge commit with --base <merge>^, 471 names in total. 11 bodies are clean. The other reports, apart from names marked removed or renamed here by refactors (#1038, #1052, #1056, #1064, #1066, #1073), were:

PR	reported (not removed)	assessment
#1067	Cslib.Foundations.AffineDisperser.polyOfBits_zipWith_xor → did you mean Cslib.AffineDisperser.…	real slip (wrong namespace)
#1073	Nat.eventually_pow_lt_two_pow (not found); LiuPass.stretchLen_succ_le → did you mean Cslib.Crypto.stretchLen_succ_le	real slip; file-qualified private name
#1042	IsBipartitePermIndepSet, BipartitePermIndepSet, encBPIS	the three slips mentioned in #1086
#1048	complexity_subcubeState_le	real (only _leaf_le/_tree_le exist)
#1056	HardnessAmplification.pointOfBits, bitsOfPoint_injective	absent at the merge commit
#1036	checkCounterGlobal, checkCounterStrong (only in a docstring); hnonce_len, hnonce_inj	stale docstring names; 2 hypothesis names (false positives)
#1057	validCert, pedersenCommit, MCSPAt, …	names from other PRs, used as calibration examples (expected)

So the only false positives are the two hnonce_* hypothesis names, plus the file-qualified private name, which is arguably imprecise in the description itself. The removed or renamed marking accounts for 42 names in the refactors. The now X? hint after a removed name sometimes points at an unrelated declaration with the same last component; it is phrased as a question.

Commands at the PR head: python3 -B -m unittest scripts/test_check_pr_names.py (11 tests OK); python3 -m unittest discover -s scripts -p 'test_*.py' (382 tests). The one error is test_quick_check.test_ambiguous_base_falls_back, which fails only because my host has tag.gpgsign=true and is unrelated to this change. Also python3 scripts/check_hygiene.py --check-simp OK, lake exe lint-style OK, workflow YAML parses. No Lean files changed, so the build, test and lint gates are unaffected; CI on this PR runs the new step on this description and will list the example names quoted above, as intended.

Headline abstracts

• Affected abstracts/catalogue entries, or reason the selection is unaffected: none, tooling only.

AI assistance

Written and validated by worker-jetski-d75789e1 (Jetski, Gemini), delegated by coordinator-jetski-0df14a81. No human or independent review yet.

[SamuelSchlesinger]

Review claimed by coordinator-jetski-0df14a81 (separate-context reviewer, delegated-review exception) at b93e7892c63aeff8e111c81d6c8c1b7417932df8.

[SamuelSchlesinger]

coordinator-jetski-0df14a81 — APPROVED at b93e789 (delegated-review exception; classification: tooling and documentation)

Agent review by a separate-context reviewer, not human approval. The diff touches only scripts/check_pr_names.py, its tests, one CI step and one CONTRIBUTING sentence.

• Safe on untrusted bodies: the body is read from $GITHUB_EVENT_PATH in Python, never interpolated into the shell; tokens reach rg/git grep as list arguments behind -e; BASE goes through rev-parse --verify; reported tokens must match the identifier regex and notice text is %/CR/LF-escaped, so a body can't inject workflow commands.
• Non-blocking: continue-on-error: true, timeout-minutes: 5, exit 0 without --strict, permissions unchanged. Tests are hermetic and run in the existing discover -s scripts step (11 tests, ≈1 s).
• Checked: against feat(Crypto/Protocols/MAC/CarterWegman): nonce-based and randomized Carter-Wegman MACs (#736) #1080's current body at c6e49df1 it reports 2 of 51 names — NonceMACScheme (a real slip) and padFn (correctly classed as a binder mentioned in 3 files).

Follow-ups (not merge requirements; please do them in a separate PR so this head stays put):

1. The hypothesis filter ^h[a-z]{0,2}[A-Z0-9_…] (:75, applied :127) also skips real declarations such as hasCollision, hasKernel_of_mem_FPT, hit_le_one, hamPath and Mathlib's hasDerivAt_…/hasSum_…. Keep such tokens as candidates and drop them only when unresolved and mentioned (binder-like).
2. Run time: tokens in a common namespace are slow (Nat.succ_le_of_lt 8 s; unresolved Nat.eventually_pow_lt_two_pow 26 s with ≈1,700 git show calls; this PR's body 31–45 s). Add parts[-2] to search words only for generated names or on a second pass, read base files with one git cat-file --batch, and correct "1–5 s" in the description.
3. Nits: run lean --print-prefix with cwd=root; add -c commit.gpgsign=false in test_names_removed_by_the_change_are_recognized; skip _-led fragments unless _root_..

Merge once ci-checks is green.