feat(scripts): kernel-level axiom sweep with committed regression baseline

.github/workflows/ci.yml

@@ -49,7 +49,7 @@ jobs:
         run: lake exe cache get
 
       - name: Run validation wrapper
-        run: ./scripts/validate.sh
+        run: ./scripts/validate.sh --axioms
 
       - name: Save Lean cache
         if: success() && steps.lake-cache.outputs.cache-hit != 'true'

AGENTS.md

@@ -186,6 +186,10 @@ lake exe cache get && lake build
 
 After adding new `.lean` files: `./scripts/update-lib.sh`.
 For routine local validation: `./scripts/validate.sh`.
+For anything that must stay axiom-clean, run `./scripts/validate.sh --axioms`.
+PolyFun has a zero-debt baseline: do not add `sorry` or non-standard axioms to it.
+`lake exe axiomsweep --update-baseline` only rewrites the empty baseline after all
+taint has been removed; it refuses to record tainted declarations.
 
 Environment linters and the test library have Lake drivers:
 

docs/wiki/quickstart.md

@@ -56,8 +56,14 @@ untracked `PolyFun/**/*.lean` files are present.
 
 `--lint` adds `lake lint` (Batteries' environment linters: `docBlame`,
 `simpNF`, `checkUnivs`, …) to the convenience wrapper. `--test` adds
-`lake test` (builds the `PolyFunTest` library). The main CI `build` job runs
-`validate.sh` without these flags, but separate `lint` and `test` CI jobs run
+`lake test` (builds the `PolyFunTest` library). `--axioms` adds
+the executable fixture matrix and `lake exe axiomsweep --check`. The check scans
+every imported `PolyFun.*` declaration and fails on any `sorryAx` or non-standard
+axiom dependency. The committed `scripts/axiom_baseline.json` is a zero-debt
+policy, not an allowlist: both arrays must remain empty. Update mode refuses to
+record taint and is only useful for resetting a stale baseline after all debt is
+removed. The main CI `build` job runs `validate.sh --axioms`, so a taint finding
+fails CI. Separate `lint` and `test` CI jobs run
 `lake lint` / `lake test`, and the `linting.yml` workflow runs the text style
 lint, so treat all three as required for merge. Text style (copyright headers,
 line length, module docstrings) is additionally enforced at build time by the

lakefile.toml

@@ -49,3 +49,18 @@ name = "PolyFun"
 name = "PolyFunTest"
 globs = ["PolyFunTest.+"]
 leanOptions = { weak.linter.style.header = false }
+
+# Kernel-level axiom / sorry accounting; see scripts/AxiomSweep.lean.
+# Runtime-imports the built PolyFun oleans, so run it after `lake build`.
+[[lean_exe]]
+name = "axiomsweep"
+srcDir = "scripts"
+root = "AxiomSweep"
+supportInterpreter = true
+
+# Isolated executable fixtures for the axiom-sweep mutation matrix. This library is not
+# a default target and deliberately contains synthetic kernel taint.
+[[lean_lib]]
+name = "AxiomSweepTestFixtures"
+srcDir = "scripts"
+globs = ["AxiomSweepTestFixtures.+"]

scripts/AxiomSweepTestFixtures/Clean.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+module
+
+/-! # Clean executable fixture for axiomsweep -/
+
+public section
+
+namespace AxiomSweepTestFixtures.Clean
+
+def base : Nat := 7
+
+def transitive : Nat := base + 1
+
+end AxiomSweepTestFixtures.Clean

scripts/AxiomSweepTestFixtures/Tainted.lean

@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+module
+
+import AxiomSweepTestFixtures.Tainted.AxiomInType
+import AxiomSweepTestFixtures.Tainted.DirectSorry
+import AxiomSweepTestFixtures.Tainted.Mutual
+import AxiomSweepTestFixtures.Tainted.NativeNames
+
+/-! # Imported taint fixture root for axiomsweep -/

scripts/AxiomSweepTestFixtures/Tainted/AxiomInType.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+module
+
+/-! # Axiom-in-type fixture for axiomsweep -/
+
+public section
+
+namespace AxiomSweepTestFixtures.Tainted
+
+axiom typeIndex : Nat
+
+axiom axiomInType : Fin (typeIndex + 1)
+
+end AxiomSweepTestFixtures.Tainted

scripts/AxiomSweepTestFixtures/Tainted/DirectSorry.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+module
+
+/-! # Direct and transitive `sorryAx` fixtures for axiomsweep -/
+
+public section
+
+namespace AxiomSweepTestFixtures.Tainted
+
+opaque directSorry : Nat := sorryAx Nat true
+
+def transitiveSorry : Nat := directSorry
+
+end AxiomSweepTestFixtures.Tainted

scripts/AxiomSweepTestFixtures/Tainted/Mutual.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+module
+
+/-! # Mutual-inductive fixpoint fixture for axiomsweep -/
+
+public section
+
+namespace AxiomSweepTestFixtures.Tainted
+
+axiom mutualAxiom : True
+
+mutual
+  inductive MutualLeft : Type where
+    | fromRight : MutualRight → MutualLeft
+    | tainted : True.intro = mutualAxiom → MutualLeft
+
+  inductive MutualRight : Type where
+    | fromLeft : MutualLeft → MutualRight
+end
+
+end AxiomSweepTestFixtures.Tainted

scripts/AxiomSweepTestFixtures/Tainted/NativeNames.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+module
+
+/-! # Native-axiom name-normalization fixtures for axiomsweep -/
+
+public section
+
+namespace AxiomSweepTestFixtures.Tainted.Generated._native.native_decide
+
+axiom ax_12_34 : True
+
+end AxiomSweepTestFixtures.Tainted.Generated._native.native_decide
+
+namespace AxiomSweepTestFixtures.Tainted.Collision._native.native_decide
+
+axiom ax_12_extra : True
+axiom ax_x_34 : True
+
+namespace ax_12_34
+
+axiom extra : True
+
+end ax_12_34
+
+end AxiomSweepTestFixtures.Tainted.Collision._native.native_decide
+
+namespace AxiomSweepTestFixtures.Tainted
+
+theorem generatedNativeUser : True := Generated._native.native_decide.ax_12_34
+
+theorem collisionUser : True := Collision._native.native_decide.ax_12_extra
+
+theorem collisionNondecimalUser : True := Collision._native.native_decide.ax_x_34
+
+theorem collisionExtraSegmentUser : True :=
+  Collision._native.native_decide.ax_12_34.extra
+
+end AxiomSweepTestFixtures.Tainted

scripts/AxiomSweepTestFixtures/Unimported.lean

@@ -0,0 +1,16 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+module
+
+/-! # Deliberately unimported `sorryAx` fixture for axiomsweep -/
+
+public section
+
+namespace AxiomSweepTestFixtures.Unimported
+
+opaque hiddenSorry : Nat := sorryAx Nat true
+
+end AxiomSweepTestFixtures.Unimported

scripts/axiom_baseline.json

@@ -0,0 +1 @@
+{"sorry": [], "nonstandard": []}

scripts/test-axiomsweep.sh

@@ -0,0 +1,134 @@
+#!/usr/bin/env bash
+
+# Execute falsifiable fixtures for the kernel-level axiom sweep.
+
+set -euo pipefail
+
+REPO_ROOT="$(git rev-parse --show-toplevel)"
+cd "$REPO_ROOT"
+
+FIXTURE_TMP="$(mktemp -d "${TMPDIR:-/tmp}/polyfun-axiomsweep.XXXXXX")"
+trap 'rm -rf -- "$FIXTURE_TMP"' EXIT
+
+expect_status() {
+  local expected="$1"
+  local label="$2"
+  shift 2
+  local log="$FIXTURE_TMP/${label}.log"
+  local actual=0
+  "$@" >"$log" 2>&1 || actual=$?
+  if [[ "$actual" -ne "$expected" ]]; then
+    echo "ERROR: $label returned $actual; expected $expected" >&2
+    sed -n '1,160p' "$log" >&2
+    return 1
+  fi
+}
+
+EMPTY_BASELINE="$FIXTURE_TMP/empty.json"
+NONEMPTY_BASELINE="$FIXTURE_TMP/nonempty.json"
+INVALID_BASELINE="$FIXTURE_TMP/invalid.json"
+MISSING_BASELINE="$FIXTURE_TMP/missing.json"
+CLEAN_REPORT="$FIXTURE_TMP/clean.json"
+TAINTED_REPORT="$FIXTURE_TMP/tainted.json"
+TAINTED_REPORT_2="$FIXTURE_TMP/tainted-2.json"
+UNIMPORTED_REPORT="$FIXTURE_TMP/unimported.json"
+
+printf '{"sorry": [], "nonstandard": []}\n' >"$EMPTY_BASELINE"
+printf '{"sorry": ["preauthorized.future"], "nonstandard": []}\n' >"$NONEMPTY_BASELINE"
+printf '{not-json}\n' >"$INVALID_BASELINE"
+
+lake build AxiomSweepTestFixtures
+lake exe axiomsweep --root AxiomSweepTestFixtures.Clean --out "$CLEAN_REPORT"
+lake exe axiomsweep --root AxiomSweepTestFixtures.Tainted --out "$TAINTED_REPORT"
+lake exe axiomsweep --root AxiomSweepTestFixtures.Tainted --out "$TAINTED_REPORT_2"
+lake exe axiomsweep --root AxiomSweepTestFixtures.Unimported --out "$UNIMPORTED_REPORT"
+
+cmp "$TAINTED_REPORT" "$TAINTED_REPORT_2"
+
+python3 - "$CLEAN_REPORT" "$TAINTED_REPORT" "$UNIMPORTED_REPORT" <<'PY'
+import json
+import sys
+
+clean_path, tainted_path, unimported_path = sys.argv[1:]
+
+with open(clean_path, encoding="utf-8") as stream:
+    clean = json.load(stream)
+with open(tainted_path, encoding="utf-8") as stream:
+    tainted = json.load(stream)
+with open(unimported_path, encoding="utf-8") as stream:
+    unimported = json.load(stream)
+
+clean_entries = {entry["name"]: entry for entry in clean["declarations"]}
+tainted_entries = {entry["name"]: entry for entry in tainted["declarations"]}
+unimported_entries = {entry["name"]: entry for entry in unimported["declarations"]}
+
+assert clean_entries
+assert all(not entry["axioms"] for entry in clean_entries.values())
+
+prefix = "AxiomSweepTestFixtures.Tainted."
+direct = tainted_entries[prefix + "directSorry"]["axioms"]
+transitive = tainted_entries[prefix + "transitiveSorry"]["axioms"]
+assert "sorryAx" in direct
+assert "sorryAx" in transitive
+
+axiom_in_type = tainted_entries[prefix + "axiomInType"]["axioms"]
+assert prefix + "typeIndex" in axiom_in_type
+
+mutual_right = tainted_entries[prefix + "MutualRight"]["axioms"]
+assert prefix + "mutualAxiom" in mutual_right
+
+all_axioms = {
+    axiom
+    for entry in tainted_entries.values()
+    for axiom in entry["axioms"]
+}
+generated = prefix + "Generated._native.native_decide"
+generated_raw = generated + ".ax_12_34"
+assert generated in all_axioms
+assert generated_raw not in all_axioms
+assert prefix + "Collision._native.native_decide.ax_12_extra" in all_axioms
+assert prefix + "Collision._native.native_decide.ax_x_34" in all_axioms
+assert prefix + "Collision._native.native_decide.ax_12_34.extra" in all_axioms
+
+hidden = "AxiomSweepTestFixtures.Unimported.hiddenSorry"
+assert hidden not in tainted_entries
+assert hidden in unimported_entries
+assert "sorryAx" in unimported_entries[hidden]["axioms"]
+PY
+
+expect_status 0 clean-check \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Clean \
+    --check --baseline "$EMPTY_BASELINE"
+expect_status 1 tainted-check \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Tainted \
+    --check --baseline "$EMPTY_BASELINE"
+expect_status 2 preauthorized-taint \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Tainted \
+    --check --baseline "$NONEMPTY_BASELINE"
+expect_status 2 stale-debt \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Clean \
+    --check --baseline "$NONEMPTY_BASELINE"
+expect_status 2 missing-baseline \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Clean \
+    --check --baseline "$MISSING_BASELINE"
+expect_status 2 invalid-baseline \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Clean \
+    --check --baseline "$INVALID_BASELINE"
+expect_status 2 conflicting-flags \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Clean \
+    --check --update-baseline --baseline "$EMPTY_BASELINE"
+
+cp "$NONEMPTY_BASELINE" "$FIXTURE_TMP/shrink.json"
+expect_status 0 shrink-baseline \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Clean \
+    --update-baseline --baseline "$FIXTURE_TMP/shrink.json"
+cmp "$EMPTY_BASELINE" "$FIXTURE_TMP/shrink.json"
+
+cp "$EMPTY_BASELINE" "$FIXTURE_TMP/growth.json"
+cp "$FIXTURE_TMP/growth.json" "$FIXTURE_TMP/growth-before.json"
+expect_status 1 reject-baseline-growth \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Tainted \
+    --update-baseline --baseline "$FIXTURE_TMP/growth.json"
+cmp "$FIXTURE_TMP/growth-before.json" "$FIXTURE_TMP/growth.json"
+
+echo "✓ Axiom sweep executable fixture matrix passed."