Harden the CI check scripts

.github/workflows/ci.yml

@@ -127,3 +127,23 @@ jobs:
           persist-credentials: false
       - name: Check no ambient evaluation-based checks in the lane import cone
         run: python3 scripts/check_native_optin.py
+
+  build-coverage:
+    name: every module is reachable from the build surface
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1
+        with:
+          persist-credentials: false
+      - name: Check the lakefile targets cover the module tree
+        run: scripts/check_build_coverage.sh
+
+  umbrella-imports:
+    name: no Mathlib umbrella imports
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1
+        with:
+          persist-credentials: false
+      - name: Check no file imports Mathlib or Mathlib.Tactic wholesale
+        run: scripts/check_no_umbrella_imports.sh

scripts/check_build_coverage.sh

@@ -0,0 +1,162 @@
+#!/usr/bin/env bash
+# Check that every Lean module in the package is reachable from the build surface.
+#
+# `lake build` compiles exactly the modules reachable from the default targets: each
+# `lean_lib`'s glob roots plus everything they transitively import. A module outside that
+# set is not elaborated at all — its `sorry`s, its axiom drift, even a failure to compile
+# are invisible to CI while the build stays green. CI runs a plain `lake build`
+# (leanprover/lean-action), so `defaultTargets` in `lakefile.toml` is the single spelling
+# of the build surface and there is no CI-side target list to drift from it. This script
+# asserts the end-to-end property: EVERY module file in the package is covered by some
+# counted target, however the import graph shifts under future trims.
+#
+# The check mirrors Lake's own semantics (Lake.Glob, v4.30.0):
+#   * `"A.B"`   selects exactly the module A.B;
+#   * `"A.B.+"` selects all submodules of A.B (the files under A/B/), not A.B itself;
+#   * `"A.B.*"` selects A.B and all submodules;
+#   * a `lean_lib` with no `globs` field defaults to its root module (`Glob.one name`).
+# The counted targets are `defaultTargets` plus the `FastFieldNative` lane: the lane is
+# deliberately outside `defaultTargets` (precompilation over its import closure is
+# expensive, so building it is opt-in), and its own invariants are enforced by
+# `scripts/check_native_lane.sh` and `scripts/check_native_optin.py`.
+#
+# `find` rather than `git ls-files`: a not-yet-staged module is still checked. Run from
+# the repository root; exits non-zero on violation.
+set -euo pipefail
+cd "$(dirname "$0")/.."
+
+# Top-level module files (the package roots, and any stray module someone adds
+# beside them) are part of the universe too — hardcoding the known roots would
+# leave a stray top-level module invisible to the check.
+{ find CompElliptic MetaCheck -name '*.lean' -print
+  find . -maxdepth 1 -name '*.lean' -print | sed 's|^\./||'; } | sort | awk '
+  # The found files arrive on stdin as a LIST; they become awk input files via ARGV,
+  # so FILENAME-based dispatch below sees each one. Lean module paths contain no
+  # whitespace, so line-based reading is exact.
+  BEGIN {
+    nuniv = 0
+    ARGV[ARGC++] = "lakefile.toml"
+    while ((getline f < "/dev/stdin") > 0) ARGV[ARGC++] = f
+    # The opt-in precompiled lane counts as a covered target; see the header.
+    targets["FastFieldNative"] = 1
+  }
+
+  # ── lakefile.toml: defaultTargets and each [[lean_lib]] name/globs ──────────
+  FILENAME == "lakefile.toml" {
+    if ($0 ~ /^defaultTargets[ \t]*=/) {
+      line = $0
+      while (match(line, /"[^"]+"/)) {
+        targets[substr(line, RSTART + 1, RLENGTH - 2)] = 1
+        line = substr(line, RSTART + RLENGTH)
+      }
+    }
+    if ($0 ~ /^\[\[lean_lib\]\]/) { inlib = 1; libname = ""; next }
+    if ($0 ~ /^\[/) { inlib = 0; inglobs = 0; next }
+    if (inlib && match($0, /^name[ \t]*=[ \t]*"[^"]+"/)) {
+      line = $0; match(line, /"[^"]+"/)
+      libname = substr(line, RSTART + 1, RLENGTH - 2)
+      next
+    }
+    if (inlib && $0 ~ /^globs[ \t]*=/) inglobs = 1
+    if (inlib && inglobs) {
+      line = $0
+      while (match(line, /"[^"]+"/)) {
+        libglobs[libname] = libglobs[libname] " " substr(line, RSTART + 1, RLENGTH - 2)
+        line = substr(line, RSTART + RLENGTH)
+      }
+      if ($0 ~ /\]/) inglobs = 0
+    }
+    next
+  }
+
+  # ── *.lean files: the module universe and its internal import edges ─────────
+  # Imports are recorded only from the file HEADER (Lean permits them nowhere
+  # else): edge scanning stops at the first line that is not blank, a comment,
+  # `module`/`prelude`, or an import. Without this, an import-shaped line inside
+  # a block comment or docstring would create a phantom edge — and a phantom
+  # edge lets the guard pass for a module `lake build` never elaborates.
+  {
+    if (!(FILENAME in seen)) {
+      seen[FILENAME] = 1
+      mod = FILENAME
+      sub(/\.lean$/, "", mod)
+      gsub(/\//, ".", mod)
+      univ[mod] = 1
+      order[nuniv++] = mod
+      filemod[mod] = FILENAME
+      curmod = mod
+      hdrdone = 0
+      cdepth = 0
+    }
+    if (hdrdone) next
+    line = $0
+    if (cdepth > 0) {                     # inside a (possibly nested) block comment
+      cdepth += gsub(/\/-/, "/-", line) - gsub(/-\//, "-/", line)
+      next
+    }
+    if (line ~ /^[ \t]*$/) next           # blank
+    if (line ~ /^[ \t]*--/) next          # line comment
+    if (line ~ /^[ \t]*\/-/) {            # block comment or docstring opens
+      cdepth += gsub(/\/-/, "/-", line) - gsub(/-\//, "-/", line)
+      next
+    }
+    sub(/^public[ \t]+/, "", line)
+    sub(/^meta[ \t]+/, "", line)
+    if (line ~ /^import[ \t]+/) {
+      split(line, parts, /[ \t]+/)
+      adj[curmod] = adj[curmod] " " parts[2]
+      next
+    }
+    if (line ~ /^(module|prelude)[ \t]*$/) next
+    hdrdone = 1                           # first real command: the header is over
+  }
+
+  END {
+    status = 0
+    # Expand the counted targets globs into the BFS root set.
+    for (lib in targets) {
+      globs = (lib in libglobs) ? libglobs[lib] : lib
+      n = split(globs, g, / +/)
+      for (i = 1; i <= n; i++) {
+        if (g[i] == "") continue
+        hit = 0
+        if (g[i] ~ /\.\+$/ || g[i] ~ /\.\*$/) {
+          pre = substr(g[i], 1, length(g[i]) - 2)      # strip ".+" / ".*"
+          withroot = (g[i] ~ /\.\*$/)
+          for (j = 0; j < nuniv; j++) {
+            m = order[j]
+            if (index(m, pre ".") == 1 || (withroot && m == pre)) {
+              queue[nq++] = m; hit = 1
+            }
+          }
+        } else if (g[i] in univ) {
+          queue[nq++] = g[i]; hit = 1
+        }
+        if (!hit) {
+          printf "VIOLATION: target %s glob %s matches no module file\n", lib, g[i] > "/dev/stderr"
+          status = 1
+        }
+      }
+    }
+    # BFS over the in-package import edges.
+    for (q = 0; q < nq; q++) {
+      m = queue[q]
+      if (m in covered) continue
+      covered[m] = 1
+      n = split(adj[m], deps, / +/)
+      for (i = 1; i <= n; i++)
+        if (deps[i] in univ && !(deps[i] in covered))
+          queue[nq++] = deps[i]
+    }
+    ncov = 0
+    for (j = 0; j < nuniv; j++) {
+      m = order[j]
+      if (m in covered) { ncov++; continue }
+      printf "VIOLATION: %s (%s) is not built by any counted target — add it to a lakefile glob or import it from a covered module\n", m, filemod[m] > "/dev/stderr"
+      status = 1
+    }
+    if (status == 0)
+      printf "build coverage: %d module(s), all covered by the counted targets.\n", ncov
+    exit status
+  }
+'

scripts/check_csimp_census.sh

@@ -1,16 +1,19 @@
 #!/usr/bin/env bash
 # Check that every `@[csimp]` declaration in the library is covered by an
-# `assert_axioms` entry in CompElliptic/TrustBoundary.lean. The compiler applies a
+# `assert_axioms` entry in some census file. The compiler applies a
 # csimp substitution in all downstream compiled code, but the axioms of the lemma's
-# own proof are not propagated into downstream `native_decide` axiom tracking (open
+# own proof are not propagated into downstream `native_decide` axiom tracking (
 # lean4#7463), so a csimp lemma whose axioms go unchecked would be an
 # axiom-smuggling channel.
 #
 # Robustness: every line containing "csimp" is scanned. Documentation must quote
 # mentions as exactly `@[csimp]` (backtick-quoted); that exact string is removed
 # before testing, so any remaining attribute syntax (`@[..., csimp, ...]` or
 # `attribute [csimp] name`) is treated as real and must name its declaration on
-# the same line. Matching against the census is by the declaration's final name
+# the same line. An `attribute` command may list several targets; every one is
+# checked, and an unparsable target fails rather than being skipped. The same-line
+# rule is load-bearing: a target continued onto the next line is invisible to a
+# line scanner. Matching against the census is by the declaration's final name
 # component.
 #
 # Scope: this guards against accidental omissions, NOT adversarial code. Run from
@@ -20,8 +23,26 @@ cd "$(dirname "$0")/.."
 
 # Every "csimp" line in the library (the census file itself included: a csimp
 # declared there is enforced like any other, and its comments follow the same
-# quoting rule).
-matches=$(grep -rn "csimp" CompElliptic/ --include="*.lean" || true)
+# quoting rule). `MetaCheck/` is excluded: it holds forged declarations that
+# exercise the rejection paths of the census macros themselves; censusing those
+# would assert the very axiom set a fixture exists to be rejected for.
+matches=$(find CompElliptic CompElliptic.lean FastFieldNative.lean -name '*.lean' -print0 \
+  | xargs -0 grep -n "csimp" /dev/null || true)
+
+# Census entries that actually run, by final name component. Any census file
+# counts, not just CompElliptic/TrustBoundary.lean: a lemma is pinned wherever
+# its entry sits.
+#
+# Widening the search to those files means excluding `#guard_msgs`-wrapped
+# entries, which assert that a census entry *fails* and so are the opposite of
+# coverage. They sit at column 0 like real entries -- the wrapper is the
+# preceding line -- and the rejection fixtures are full of them, so an
+# expected-to-fail entry would otherwise satisfy this check.
+censused=$(find CompElliptic MetaCheck -name "*.lean" -print0 | xargs -0 awk '
+  FNR == 1 { prev = "" }
+  /^assert_axioms / && prev !~ /^#guard_msgs/ { sub(/.*\./, "", $2); print $2 }
+  { prev = $0 }
+')
 
 status=0
 count=0
@@ -31,20 +52,38 @@ while IFS=: read -r file lineno line; do
   if ! printf '%s' "$stripped" | grep -qE '@\[[^]]*\bcsimp\b|attribute[[:space:]]*\[[^]]*\bcsimp\b'; then
     continue  # only quoted documentation mentions on this line
   fi
-  name=$(printf '%s' "$stripped" | sed -nE "s/.*(theorem|def)[[:space:]]+([A-Za-z0-9_'.]+).*/\2/p")
-  if [[ -z "$name" ]]; then
-    name=$(printf '%s' "$stripped" | sed -nE "s/.*attribute[[:space:]]*\[[^]]*csimp[^]]*\][[:space:]]+([A-Za-z0-9_'.]+).*/\1/p")
+  names=$(printf '%s' "$stripped" | sed -nE "s/.*(theorem|def)[[:space:]]+([A-Za-z0-9_'.]+).*/\2/p")
+  if [[ -z "$names" ]]; then
+    # `attribute [csimp] a b …` applies the attribute to every listed target: collect the whole
+    # target list, and fail on any token the identifier grammar does not cover rather than
+    # silently checking a prefix of the command.
+    targets=$(printf '%s' "$stripped" \
+      | sed -nE "s/.*attribute[[:space:]]*\[[^]]*csimp[^]]*\][[:space:]]+(.*)$/\1/p" \
+      | sed -E 's/--.*$//')
+    ident_re="^[A-Za-z0-9_'.]+$"
+    for target in $targets; do
+      if [[ "$target" =~ $ident_re ]]; then
+        names="$names $target"
+      else
+        echo "VIOLATION: $file:$lineno: unparsable csimp attribute target '$target'" >&2
+        status=1
+      fi
+    done
   fi
-  if [[ -z "$name" ]]; then
+  if [[ -z "${names// /}" ]]; then
     echo "VIOLATION: $file:$lineno: csimp attribute syntax must name its declaration on the same line (write \`@[csimp] theorem <name>\`), and documentation mentions must be quoted as exactly \`@[csimp]\`" >&2
     status=1
     continue
   fi
-  count=$((count + 1))
-  if ! grep -qE "^assert_axioms .*\.${name}( |\$)|^assert_axioms ${name}( |\$)" CompElliptic/TrustBoundary.lean; then
-    echo "VIOLATION: csimp declaration ${name} ($file:$lineno) has no assert_axioms entry in CompElliptic/TrustBoundary.lean" >&2
-    status=1
-  fi
+  for name in $names; do
+    count=$((count + 1))
+    # Herestring rather than a pipe: `grep -q` exits at the first match, which under `pipefail`
+    # would make a *successful* lookup fail the pipeline on the writer's SIGPIPE.
+    if ! grep -qxF "${name##*.}" <<< "$censused"; then
+      echo "VIOLATION: csimp declaration ${name} ($file:$lineno) has no assert_axioms entry in any census file" >&2
+      status=1
+    fi
+  done
 done <<< "$matches"
 
 if [[ $status -eq 0 ]]; then

scripts/check_native_lane.sh

@@ -8,8 +8,15 @@ cd "$(dirname "$0")/.."
 
 # The lane, parsed from lakefile.toml's precompileModules libraries (the single
 # source of truth) via check_native_optin.py; module names become file paths.
+# Command substitution (unlike process substitution) propagates the
+# script's failure through `set -e`, even if it dies after partial output.
+LANE_OUTPUT="$(python3 scripts/check_native_optin.py --print-lane)"
+if [[ -z "$LANE_OUTPUT" ]]; then
+  echo "ERROR: check_native_optin.py --print-lane printed no lane modules" >&2
+  exit 1
+fi
 LANE_MODULES=()
-mapfile -t LANE_MODULES < <(python3 scripts/check_native_optin.py --print-lane)
+mapfile -t LANE_MODULES <<< "$LANE_OUTPUT"
 LANE=()
 for mod in "${LANE_MODULES[@]}"; do LANE+=("${mod//.//}.lean"); done
 

scripts/check_no_umbrella_imports.sh

@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+# Check that no Lean file imports the Mathlib umbrella modules.
+#
+# `import Mathlib` pulls in all of Mathlib, and `import Mathlib.Tactic` is the same
+# failure mode at smaller scale: each transitively loads a large slice of Mathlib's
+# theory into every Lean process that elaborates the file (measured in zcash/ironwood
+# at roughly 6.5 GB RSS for the full umbrella and +1.3 GB RSS / +1.6 s import-load
+# time for `Mathlib.Tactic`, against the narrow modules a file actually needs).
+# During a parallel Lake build several such processes create severe memory and GC
+# pressure. Nothing fails when an umbrella import creeps in — builds just quietly
+# get slow — so the absence has to be enforced mechanically.
+#
+# The rule: no tracked `.lean` file may contain a bare `import Mathlib` or a bare
+# `import Mathlib.Tactic` (with or without a trailing comment). Specific submodule
+# imports such as `import Mathlib.Tactic.Ring` are fine. If an umbrella import is
+# ever legitimately needed, extend this script with an explicit allowlist rather
+# than deleting the check.
+#
+# Run from the repository root; exits non-zero on violation.
+set -euo pipefail
+cd "$(dirname "$0")/.."
+
+# One-or-more whitespace after `import` (not exactly one space), and optional
+# `public`/`meta` modifiers, so spacing variants and module-system prefixes
+# cannot slip a banned umbrella past the anchor.
+violations=$(git ls-files '*.lean' | xargs grep -nE '^(public[[:space:]]+)?(meta[[:space:]]+)?import[[:space:]]+Mathlib(\.Tactic)?([[:space:]]|$)' || true)
+
+if [ -n "$violations" ]; then
+  echo "::error::bare 'import Mathlib' / 'import Mathlib.Tactic' umbrella imports are not allowed; import the specific Mathlib modules instead (see scripts/check_no_umbrella_imports.sh):"
+  echo "$violations"
+  exit 1
+fi
+echo "umbrella imports: none."