From 6934370da04283a272a292b726b2e5746a809467 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Wed, 19 Aug 2026 01:15:48 +0100 Subject: [PATCH 1/4] ci: fail the native-lane check when the lane list cannot be obtained MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The lane modules were read via `mapfile` from a process substitution, whose failure escapes `set -e`: if check_native_optin.py died (or died after partial output), the loop ran over an empty or truncated lane and the check passed vacuously as "core-only (0 modules)". Use command substitution — an assignment's exit status is the command's, so any failure aborts the script — and reject empty output explicitly. Co-authored-by: Claude Fable 5 --- scripts/check_native_lane.sh | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/scripts/check_native_lane.sh b/scripts/check_native_lane.sh index df004e4..0b7351e 100755 --- a/scripts/check_native_lane.sh +++ b/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 From 3379d5ffe80e5de5881c9fa98b17c83d16cfc77a Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Wed, 19 Aug 2026 01:30:43 +0100 Subject: [PATCH 2/4] ci: adopt ironwood's hardened csimp census MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Port the zcash/ironwood improvements to the shared csimp-census check: - an `attribute [csimp] a b …` command is censused per target, and an unparsable target fails rather than being silently skipped; - census entries count from any file, matched by final name component, with `#guard_msgs`-wrapped entries excluded (they assert that an entry *fails*, so they are the opposite of coverage); - the census lookup uses a herestring rather than piping into `grep -q`, which exits at the first match and would fail a *successful* lookup under `pipefail` via the writer's SIGPIPE; - `MetaCheck/` is excluded from the scan (it holds forged declarations exercising the census macros' rejection paths), and the top-level root modules are included. Co-authored-by: Claude Fable 5 --- scripts/check_csimp_census.sh | 67 +++++++++++++++++++++++++++-------- 1 file changed, 53 insertions(+), 14 deletions(-) diff --git a/scripts/check_csimp_census.sh b/scripts/check_csimp_census.sh index ed13fab..128536a 100755 --- a/scripts/check_csimp_census.sh +++ b/scripts/check_csimp_census.sh @@ -1,8 +1,8 @@ #!/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. # @@ -10,7 +10,10 @@ # 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 \`), 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 From f5c9015f9813b9a2ee31e2ad27838f71ed0aa17c Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Wed, 19 Aug 2026 01:31:05 +0100 Subject: [PATCH 3/4] ci: check that every module is reachable from the build surface Adapted from zcash/ironwood's check_build_coverage.sh. `lake build` compiles exactly the modules reachable from the default targets, so a module outside that set is never elaborated: its sorries, axiom drift, or failure to compile stay invisible while CI is green. The script mirrors Lake's glob semantics over lakefile.toml and BFS-closes the in-package import graph, flagging any module file no counted target reaches. Differences from the ironwood original: CI here runs a plain `lake build`, so there is no CI-side target list to compare against defaultTargets; the opt-in `FastFieldNative` lane counts as a covered target (its own invariants are enforced by check_native_lane.sh and check_native_optin.py); and the module universe includes all top-level `*.lean` files, so a stray module beside the package roots is caught rather than being invisible to the scan. Co-authored-by: Claude Fable 5 --- .github/workflows/ci.yml | 10 ++ scripts/check_build_coverage.sh | 162 ++++++++++++++++++++++++++++++++ 2 files changed, 172 insertions(+) create mode 100755 scripts/check_build_coverage.sh diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 024daa5..4c5b460 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -127,3 +127,13 @@ 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 diff --git a/scripts/check_build_coverage.sh b/scripts/check_build_coverage.sh new file mode 100755 index 0000000..896a283 --- /dev/null +++ b/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 + } +' From 141f6f97970d61ad8c741403801850df3afedb29 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Wed, 19 Aug 2026 01:31:05 +0100 Subject: [PATCH 4/4] ci: forbid Mathlib umbrella imports MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Port zcash/ironwood's guard: no tracked Lean file may contain a bare `import Mathlib` or `import Mathlib.Tactic`. Each umbrella loads a large slice of Mathlib into every elaborating process (measured in ironwood at ~6.5 GB RSS for the full umbrella, +1.3 GB RSS per process for `Mathlib.Tactic`), and nothing fails when one creeps in — builds just quietly get slow. The library is currently clean; this keeps it that way. Co-authored-by: Claude Fable 5 --- .github/workflows/ci.yml | 10 +++++++++ scripts/check_no_umbrella_imports.sh | 33 ++++++++++++++++++++++++++++ 2 files changed, 43 insertions(+) create mode 100755 scripts/check_no_umbrella_imports.sh diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4c5b460..6153a11 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -137,3 +137,13 @@ jobs: 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 diff --git a/scripts/check_no_umbrella_imports.sh b/scripts/check_no_umbrella_imports.sh new file mode 100755 index 0000000..b58b078 --- /dev/null +++ b/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."