CI: audit every declaration, broader source checks, pinned elan

.github/workflows/ci.yml

@@ -8,9 +8,10 @@ on:
 
 permissions: {}
 
+# A new push to a pull request cancels its running check; runs on main always finish.
 concurrency:
   group: ci-${{ github.ref }}
-  cancel-in-progress: true
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
 
 jobs:
   build:
@@ -28,13 +29,42 @@ jobs:
       - name: Check the sources
         run: scripts/check-sources.sh
 
+      # A pinned release, checked against its published SHA-256.
+      - name: Install elan
+        env:
+          ELAN_VERSION: v4.2.4
+          ELAN_SHA256: 42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63
+        run: |
+          curl -sSfL -o elan.tar.gz \
+            "https://github.com/leanprover/elan/releases/download/${ELAN_VERSION}/elan-x86_64-unknown-linux-gnu.tar.gz"
+          echo "${ELAN_SHA256}  elan.tar.gz" | sha256sum --check
+          tar -xzf elan.tar.gz
+          ./elan-init -y --default-toolchain none
+          rm elan.tar.gz elan-init
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      # Runs restore the newest build of main; only pushes to main save one, so pull requests do
+      # not evict it.
+      - name: Restore the build
+        id: restore
+        uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
+        with:
+          path: .lake
+          key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-${{ github.sha }}
+          restore-keys: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-
+
+      - name: Get the Mathlib cache
+        run: lake exe cache get
+
       - name: Build, failing on any warning
-        uses: leanprover/lean-action@f061402b660e0c34644504b324e830f2991d4865 # v1.6.1
+        run: lake build --wfail
+
+      - name: Save the build
+        if: github.event_name == 'push'
+        uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
         with:
-          auto-config: "false"
-          build: "true"
-          build-args: "--wfail"
-          use-mathlib-cache: "true"
+          path: .lake
+          key: ${{ steps.restore.outputs.cache-primary-key }}
 
-      - name: Audit the axioms of the endpoints
+      - name: Audit the axioms of every declaration
         run: scripts/check-axioms.sh

AGENTS.md

@@ -292,13 +292,18 @@ scripts/check-axioms.sh
 git diff --check
 ```
 
-`scripts/check-sources.sh` rejects axiom declarations, native evaluation (`native_decide`,
-`bv_decide`), `implemented_by`/`extern` bindings and heartbeat or recursion-depth overrides.
-`lake build --wfail` fails on any warning, including `declaration uses 'sorry'`.
-`scripts/check-axioms.sh` runs every file under `src/Tests` that prints axioms
-(`#print axioms`) and checks the envelope: `propext`, `Classical.choice` and `Quot.sound`;
-any other axiom, including `sorryAx`, is a failure. CI (`.github/workflows/ci.yml`) runs these
+`scripts/check-sources.sh` is a quick first check: it rejects axiom declarations, native
+evaluation (`native_decide`, `bv_decide`, `native := true`), `implemented_by`, `extern` and
+`csimp`, options that switch off kernel or `sorry` checks, and heartbeat or recursion-depth
+overrides, in code, comments and docstrings alike. `lake build --wfail` fails on any warning,
+including `declaration uses 'sorry'`. `scripts/check-axioms.sh` is the complete audit: it imports
+every module under `src` and checks that every declaration stays within `propext`,
+`Classical.choice` and `Quot.sound`, however a `sorry`, native evaluation or axiom is written.
+The only exemptions, listed in `scripts/AxiomAudit.lean`, are DSL diagnostics that check an
+elaboration error and so contain `sorryAx`. The `#print axioms` lines under `src/Tests` document
+the main results; the audit does not depend on them. CI (`.github/workflows/ci.yml`) runs these
 three on every pull request and on `main`, and `.github/workflows/zizmor.yml` audits the
-workflows with zizmor. Actions are pinned to commit hashes, which Dependabot updates.
+workflows with zizmor. Actions are pinned to commit hashes, which Dependabot updates; elan is
+pinned to a release and its SHA-256 in `ci.yml`, which is updated by hand.
 
 For changes to public declarations used downstream, also build `chachapoly-cc`.

scripts/AxiomAudit.lean

@@ -0,0 +1,54 @@
+import Lean
+
+/-!
+# Axiom audit of every declaration
+
+Imports the modules named on the command line and checks that every declaration they define
+depends on no axiom other than `propext`, `Classical.choice` and `Quot.sound`. `sorry`
+(`sorryAx`), native evaluation (`Lean.ofReduceBool`, `Lean.trustCompiler` and the auxiliary
+axioms of `native_decide`) and declared axioms all show up here, however they are written.
+Run by `scripts/check-axioms.sh`.
+-/
+
+open Lean
+
+/-- The accepted axioms. -/
+def allowed : List Name := [``propext, ``Classical.choice, ``Quot.sound]
+
+/-- Components whose declarations may use `sorryAx`. Each is a DSL diagnostic that checks an
+elaboration error with `#guard_msgs`; after the error Lean still adds the generated
+declarations, with `sorryAx` in place of the part that failed. -/
+def mayUseSorry : List Name :=
+  [`DSLTests.Diagnostics.Infinite, `DSLTests.Diagnostics.Growing,
+    `DSLTests.Diagnostics.Uninitialized, `DSLTests.Diagnostics.WrongReply]
+
+/-- Whether declaration `c` may depend on axiom `a`. -/
+def accepted (c a : Name) : Bool :=
+  allowed.contains a || (a == ``sorryAx && mayUseSorry.any (·.isPrefixOf c))
+
+unsafe def main (args : List String) : IO UInt32 := do
+  let modules := args.toArray.map String.toName
+  if modules.isEmpty then
+    IO.eprintln "error: no modules to audit"
+    return 1
+  enableInitializersExecution
+  initSearchPath (← findSysroot)
+  let env ← importModules (modules.map ({ module := · })) {} (loadExts := true)
+  let audited : NameSet := modules.foldl (·.insert ·) {}
+  -- The declarations defined in the audited modules, not in their imports.
+  let ours (c : Name) : Bool :=
+    match env.getModuleIdxFor? c with
+    | some idx => audited.contains env.header.moduleNames[idx.toNat]!
+    | none => false
+  let names := env.constants.fold (init := #[]) fun acc c _ => if ours c then acc.push c else acc
+  let ctx : Core.Context := { fileName := "<axiom audit>", fileMap := default }
+  let (bad, _) ← (names.filterMapM fun c => do
+      let axs ← collectAxioms c
+      let outside := axs.filter fun a => !accepted c a
+      return if outside.isEmpty then none else some (c, outside)
+    : CoreM _).toIO ctx { env }
+  for (c, axs) in bad do
+    IO.println s!"error: {c} depends on {axs.toList}"
+  IO.println s!"axioms: {names.size} declarations in {modules.size} modules, \
+    {bad.size} outside the envelope"
+  return if bad.isEmpty then 0 else 1

scripts/check-axioms.sh

@@ -1,44 +1,16 @@
 #!/usr/bin/env bash
-# Runs every file under `src/Tests` that prints axioms and fails if an audited endpoint depends
-# on an axiom other than `propext`, `Classical.choice` and `Quot.sound` (`sorryAx` included).
-# Expects the library to be built (`lake build`).
+# Audits every declaration of every module under `src` and fails if one depends on an axiom other
+# than `propext`, `Classical.choice` and `Quot.sound` (`sorryAx` included). The exemptions are
+# listed in `scripts/AxiomAudit.lean`. Expects the library to be built (`lake build`).
 set -euo pipefail
 
 cd "$(dirname "$0")/.."
 
-allowed='^(propext|Classical\.choice|Quot\.sound)$'
-status=0
-total=0
-
-files=()
+modules=()
 while IFS= read -r file; do
-  files+=("$file")
-done < <(grep -rl '#print axioms' src/Tests | sort)
-if [[ ${#files[@]} -eq 0 ]]; then
-  echo "error: no axiom audits found under src/Tests"
-  exit 1
-fi
-
-for file in "${files[@]}"; do
-  if ! output=$(lake env lean "$file" 2>&1); then
-    echo "$output"
-    echo "error: $file does not compile"
-    status=1
-    continue
-  fi
-  # A message may wrap over several lines; join them before matching.
-  joined=$(tr '\n' ' ' <<<"$output")
-  audited=$(grep -oE "depends on axioms|does not depend on any axioms" <<<"$joined" \
-    | wc -l | tr -d ' ' || true)
-  total=$((total + audited))
-  outside=$(grep -oE "depends on axioms: \[[^]]*\]" <<<"$joined" \
-    | sed -E 's/.*\[//; s/\]$//' | tr ',' '\n' | tr -d ' ' | grep -vE "$allowed" | sort -u || true)
-  if [[ -n $outside ]]; then
-    echo "error: $file: axioms outside the envelope: $(tr '\n' ' ' <<<"$outside")"
-    status=1
-  fi
-  echo "$file: $audited endpoints"
-done
+  module=${file#src/}
+  module=${module%.lean}
+  modules+=("${module//\//.}")
+done < <(find src -name '*.lean' | sort)
 
-echo "axioms: $total endpoints in ${#files[@]} files"
-exit $status
+lake env lean --run scripts/AxiomAudit.lean "${modules[@]}"

scripts/check-sources.sh

@@ -1,6 +1,7 @@
 #!/usr/bin/env bash
-# Fails if the sources declare an axiom, evaluate natively, bind compiled code, or raise a
-# resource limit. `sorry` and `admit` are caught by `lake build --wfail`.
+# A quick first check, before anything is built: fails if the sources declare an axiom, evaluate
+# natively, bind compiled code, switch off a kernel or `sorry` check, or raise a resource limit.
+# Comments and docstrings are matched too. `scripts/check-axioms.sh` is the complete audit.
 set -euo pipefail
 
 cd "$(dirname "$0")/.."
@@ -9,21 +10,31 @@ status=0
 
 check() {
   local what=$1 pattern=$2
-  local hits
-  hits=$(grep -rnE "$pattern" src || true)
+  local hits code=0
+  hits=$(grep -rnE "$pattern" src) || code=$?
+  if [[ $code -gt 1 ]]; then
+    echo "error: grep failed while checking for $what"
+    exit 2
+  fi
   if [[ -n $hits ]]; then
     echo "$hits"
     echo "error: $what"
     status=1
   fi
 }
 
-check "axiom declarations" '^[[:space:]]*((private|protected)[[:space:]]+)?axiom[[:space:]]'
-check "native evaluation" 'native_decide|bv_decide|decide \+native|Lean\.ofReduceBool'
-check "compiled code bindings" '@\[(implemented_by|extern)'
-check "resource limits" 'maxHeartbeats|maxRecDepth|synthInstance\.maxSize'
+modifiers='((private|protected|public|noncomputable|unsafe|partial|nonrec|meta)[[:space:]]+)*'
+attributes='(@\[[^]]*[]][[:space:]]*)*'
+check "axiom declarations" "(^|-/|[]])[[:space:]]*${attributes}${modifiers}axiom[[:space:]]"
+check "native evaluation" \
+  'native_decide|bv_decide|[+]native|native[[:space:]]*:=|reduceBool|reduceNat|trustCompiler'
+check "compiled code bindings" \
+  'implemented_by|csimp|(@\[|attribute[[:space:]]*\[|,)[[:space:]]*extern'
+check "kernel or sorry checks switched off" \
+  'debug\.skipKernelTC|warn\.sorry|addDeclCore|addDeclWithoutChecking|doCheck'
+check "resource limits" 'maxHeartbeats|maxRecDepth|synthInstance\.max'
 
 if [[ $status -eq 0 ]]; then
-  echo "sources: no axiom declarations, native evaluation, code bindings or limit overrides"
+  echo "sources: no axioms, native evaluation, code bindings, disabled checks or limit overrides"
 fi
 exit $status