ci: re-check the build with the nanoda kernel checker

[daira]

Re-checks the entire built library with nanoda, an independent reimplementation of the Lean kernel in Rust. As noted in the postmortem of leanprover/lean4#14576, doing this implies that a kernel soundness bug has to appear in two independently implemented kernels to go unnoticed. Builds on #20, whose +native(...) owner census pins the per-use native_decide axiom names that the checker's permitted list needs.

• scripts/nanoda-config.json — the machine-checked axiom census. Strict mode (unpermitted_axiom_hard_error) fails on any axiom declared outside permitted_axioms; pp_declars fails the run if an expected native_decide axiom disappears from the export; the admitted axioms are pretty-printed into the CI log with their types (the primitivity certificates show their literal roots of unity).
• scripts/check_export_axioms.py — lean4export dumps the whole environment, so axioms Lean core declares unconditionally (sorryAx, Lean.trustCompiler, Lean.ofReduceBool, Lean.ofReduceNat) must be permitted for strict mode to run at all, and permitting a declaration says nothing about use. This script closes the gap by scanning the export: the declared axioms are exactly the permitted list; sorryAx/ofReduceBool/ofReduceNat are cited by nothing (in particular, a sorry anywhere in the library fails CI here); and trustCompiler is cited only by core's deprecated reduceBool/reduceNat gates. The export's structural conventions (pinned format version, closed shape set, dense ids, no forward or dangling references) are verified rather than assumed; census violations (exit 1, census still printed) are distinguished from structural errors (exit 2).
• scripts/check_nanoda.sh — drives export → census check → nanoda, and asserts that every project module is reachable from the export roots, so a module cannot silently drop out of the re-check. MetaCheck is deliberately outside the roots: its forged axioms exist to be rejected.
• CI — a nanoda job with needs: build, so the fast build check reports on its own and can gate PR acceptance; the job restores the build job's cache instead of rebuilding, then builds lean4export at the toolchain's tag and nanoda at a pinned revision.

The full pipeline (coverage check, export of 314,801 declarations at 1.8 GB, census check, 4-thread nanoda) runs in 5m 13s on an M-series laptop, on top of an up-to-date lake build.

🤖 Claude Fable 5

[daira]

Self-ACK

[TalDerei]

interesting, haven't used nanoda before. let's also apply this to ironwood! ACK

[daira]

Self-reACK