From a31209cace29956c11084ec829670d8c8fb34e64 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Mon, 10 Aug 2026 04:49:20 +0100 Subject: [PATCH] ci: re-check the build with the nanoda kernel checker MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add a CI job that exports the built library with lean4export and re-checks every declaration with nanoda, an independent Rust reimplementation of the Lean kernel. A kernel soundness bug would then have to appear in two distinct implementations to go unnoticed. The job depends on the build job, so the fast build check can gate PR acceptance on its own, and restores that job's build cache rather than rebuilding. The committed nanoda config is a machine-checked axiom census: strict mode rejects any axiom declared outside the permitted list, and the pp_declars list fails the run if an expected native_decide axiom disappears from the export. scripts/check_export_axioms.py closes the remaining gap: axioms that Lean core declares unconditionally (sorryAx and the legacy compiler-trust axioms) must be permitted, so it checks that nothing cites them. sorryAx, Lean.ofReduceBool, and Lean.ofReduceNat are cited by nothing — in particular a sorry anywhere in the library fails the check — and Lean.trustCompiler only by core's deprecated reduceBool and reduceNat gates. The script verifies the export's structural conventions rather than assuming them, and distinguishes census violations from structural errors. scripts/check_nanoda.sh drives the pipeline and asserts that every project module is reachable from the export roots, so a module cannot silently drop out of the re-check. Co-authored-by: Claude Fable 5 --- .github/workflows/ci.yml | 31 ++++ scripts/check_export_axioms.py | 269 +++++++++++++++++++++++++++++++++ scripts/check_nanoda.sh | 59 ++++++++ scripts/nanoda-config.json | 34 +++++ 4 files changed, 393 insertions(+) create mode 100755 scripts/check_export_axioms.py create mode 100755 scripts/check_nanoda.sh create mode 100644 scripts/nanoda-config.json diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d241722..c59a4fb 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -24,6 +24,37 @@ jobs: # and runs `lake build` — which also runs the in-file `native_decide` sanity checks. - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0 + # Re-checks the library with nanoda, an independent reimplementation of the Lean + # kernel (see scripts/check_nanoda.sh). A separate job so `build` reports quickly and + # can gate PR acceptance on its own; this one starts only after a green build, and its + # `lake build` restores the build cache that job just saved, so it verifies rather + # than rebuilds. + nanoda: + name: an independent kernel accepts the build + needs: build + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 + with: + persist-credentials: false + - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0 + - name: Build lean4export at the pinned toolchain's tag + run: | + TOOLCHAIN=$(cat lean-toolchain) + git clone --depth 1 --branch "${TOOLCHAIN##*:}" \ + https://github.com/leanprover/lean4export work/lean4export + cd work/lean4export && lake build + - name: Build nanoda at the pinned revision + run: | + git clone --depth 1 \ + --revision=418320295890faed83a96fd97907b12a3b6728c2 \ + https://github.com/ammkrn/nanoda_lib work/nanoda_lib + cargo build --release --manifest-path work/nanoda_lib/Cargo.toml + - name: Export the library and re-check it + run: | + scripts/check_nanoda.sh work/lean4export/.lake/build/bin/lean4export \ + work/nanoda_lib/target/release/nanoda_bin + generators: name: Field-file generators reproduce runs-on: ubuntu-latest diff --git a/scripts/check_export_axioms.py b/scripts/check_export_axioms.py new file mode 100755 index 0000000..b3231f3 --- /dev/null +++ b/scripts/check_export_axioms.py @@ -0,0 +1,269 @@ +#!/usr/bin/env python3 +"""Check the axiom census of a lean4export ndjson export against the nanoda config. + +nanoda's strict mode (`unpermitted_axiom_hard_error: true`) rejects any axiom *declared* +outside the permitted list, but must permit axioms Lean core declares whether or not +anything uses them (`sorryAx` and the legacy compiler-trust axioms). Permitting a +declaration says nothing about use, so this script closes that gap from the export +itself: + + * the axioms declared in the export are exactly the config's `permitted_axioms`; + * `sorryAx`, `Lean.ofReduceBool`, and `Lean.ofReduceNat` are cited by no expression + at all — in particular, a `sorry` anywhere in the library fails here; + * `Lean.trustCompiler` is cited only by `Lean.reduceBool` and `Lean.reduceNat` — + the opaque evaluation functions of the deprecated compiler-trust route, distinct + from their propositional bridge axioms `Lean.ofReduceBool`/`Lean.ofReduceNat` + above — and nothing in this repository consumes them. + +Failures come in two kinds, mirroring `check_native_optin.py`: + + * VIOLATION (exit 1) — an undesired outcome in structurally well-formed data: a + declared axiom outside the permitted list, a stale permitted entry, or a citation + of an axiom that must be unreferenced. Violations are collected, the full axiom + census is printed regardless, and the process exits non-zero at the end. + * ERROR (exit 2) — the export's structure is not as this script assumes: an + unrecognized line shape or kind, a non-monotonic or undefined id, a cyclic name + chain, or an unpinned format version. Conclusions drawn from such data would be + unreliable, so the scan stops immediately without printing a census. + +The scan does not silently rely on the export's structural conventions; it verifies +them: + + * the format version is pinned (bump deliberately after re-checking the assumptions); + * every line's shape is from the closed known set, so a citation cannot hide inside + an unhandled construct; + * name, expression, and level ids are dense — each new id increments the previous + by exactly 1 (names and levels from 1, id 0 being the reserved anonymous name and + zero level; expressions from 0) — and every referenced sub-id is strictly smaller + than the id being defined, so a referenced id is always already defined and the + single-pass citation propagation over the expression DAG cannot miss a forward or + dangling reference. + +Usage: scripts/check_export_axioms.py [nanoda-config.json] +The export path is read from the config (single source of truth). Runs from the +repository root. +""" +import json +import sys +from pathlib import Path +from typing import NoReturn + +FORMAT_VERSION = "3.1.0" +MAX_REPORTED_VIOLATIONS = 100 + +# Axioms that must be cited by no expression in the export. +UNREFERENCED = {"sorryAx", "Lean.ofReduceBool", "Lean.ofReduceNat"} +# Axioms that only the named declarations may cite. +RESTRICTED = {"Lean.trustCompiler": {"Lean.reduceBool", "Lean.reduceNat"}} +TARGETS = UNREFERENCED | set(RESTRICTED) +TARGET_COMPONENTS = {t.rsplit(".", 1)[-1] for t in TARGETS} + +EXPR_KINDS = {"app", "bvar", "const", "forallE", "lam", "letE", "natVal", "proj", + "sort", "strVal"} +LEVEL_KINDS = {"imax", "max", "param", "succ"} +DECL_KINDS = {"axiom", "def", "inductive", "opaque", "quot", "thm"} +# Expression sub-ids per expression kind (everything else in the payload is a name id, +# a level id, or plain data). +EXPR_SUBFIELDS = {"app": ("fn", "arg"), "forallE": ("type", "body"), + "lam": ("type", "body"), "letE": ("type", "value", "body"), + "proj": ("struct",)} +# Keys holding expression ids inside declaration payloads (at any nesting depth). +DECL_EXPR_KEYS = {"type", "value", "rhs"} + +violations = [] + + +def violation(msg): + violations.append(msg) + + +def error(msg) -> NoReturn: + print(f"ERROR: {msg} — the export's structure is not as this script assumes, so " + f"its conclusions would be unreliable; re-verify the assumptions and update " + f"this script", file=sys.stderr) + sys.exit(2) + + +def main(): + config_path = Path(sys.argv[1] if len(sys.argv) > 1 else "scripts/nanoda-config.json") + config = json.loads(config_path.read_text()) + permitted = set(config["permitted_axioms"]) + export_path = Path(config["export_file_path"]) + + names = {} # name id -> (prefix id, component) + + def resolve(i): + parts, seen = [], set() + while i != 0: + if i in seen: + error(f"name id {i} has a cyclic prefix chain") + seen.add(i) + entry = names.get(i) + if entry is None: + error(f"name id {i} is undefined") + pre, comp = entry + parts.append(comp) + i = pre + return ".".join(reversed(parts)) + + def decl_expr_ids(payload): + todo, out = [payload], [] + while todo: + x = todo.pop() + if isinstance(x, dict): + for k, v in x.items(): + if k in DECL_EXPR_KEYS and isinstance(v, int): + out.append(v) + else: + todo.append(v) + elif isinstance(x, list): + todo.extend(x) + return out + + target_name_ids = {} # name id -> target full name + taint = {} # expr id -> frozenset of target full names + citers = {} # target full name -> set of citing declaration names + const_cited = {t: False for t in TARGETS} + declared_axioms = set() + max_in = max_il = 0 # id 0: the reserved anonymous name / zero level + max_ie = -1 + meta_seen = False + + with open(export_path, "rb") as f: + for raw in f: + o = json.loads(raw) + if "in" in o: + i = o["in"] + if i != max_in + 1: + error(f"name id {i} does not follow {max_in} densely") + max_in = i + if "str" in o: + pre, comp = o["str"]["pre"], o["str"]["str"] + elif "num" in o: + pre, comp = o["num"]["pre"], str(o["num"]["i"]) + else: + error(f"unknown name entry shape: {sorted(o.keys())}") + if len(o) != 2: + error(f"unknown name line shape: {sorted(o.keys())}") + if not (pre == 0 or pre < i): + error(f"name id {i} references non-earlier prefix {pre}") + names[i] = (pre, comp) + if comp in TARGET_COMPONENTS: + full = resolve(i) + if full in TARGETS: + target_name_ids[i] = full + elif "ie" in o: + i = o["ie"] + if i != max_ie + 1: + error(f"expression id {i} does not follow {max_ie} densely") + max_ie = i + rest = set(o.keys()) - {"ie"} + if len(rest) != 1 or len(o) != 2: + error(f"unknown expression line shape: {sorted(o.keys())}") + (kind,) = rest + if kind not in EXPR_KINDS: + error(f"unknown expression kind '{kind}' at expression id {i}") + t = set() + if kind == "const": + nid = o["const"]["name"] + if nid in target_name_ids: + full = target_name_ids[nid] + t.add(full) + const_cited[full] = True + for f2 in EXPR_SUBFIELDS.get(kind, ()): + v = o[kind][f2] + if not 0 <= v < i: + error(f"expression id {i} references non-earlier sub-id {v}") + if v in taint: + t |= taint[v] + if t: + taint[i] = frozenset(t) + elif "il" in o: + i = o["il"] + if i != max_il + 1: + error(f"level id {i} does not follow {max_il} densely") + max_il = i + rest = set(o.keys()) - {"il"} + if len(rest) != 1 or len(o) != 2: + error(f"unknown level line shape: {sorted(o.keys())}") + (kind,) = rest + if kind not in LEVEL_KINDS: + error(f"unknown level kind '{kind}' at level id {i}") + if kind == "succ": + subs = [o[kind]] + elif kind in ("max", "imax"): + subs = o[kind] + else: # param references a name id, not a level id + subs = [] + for v in subs: + if v >= i: + error(f"level id {i} references non-earlier sub-id {v}") + elif "meta" in o: + meta_seen = True + version = o["meta"]["format"]["version"] + if version != FORMAT_VERSION: + error(f"export format version {version} != pinned {FORMAT_VERSION}") + else: + kinds = set(o.keys()) & DECL_KINDS + if len(kinds) != 1 or len(o) != 1: + error(f"unknown line shape: {sorted(o.keys())}") + (kind,) = kinds + d = o[kind] + if kind == "axiom": + declared_axioms.add(resolve(d["name"])) + hit = set() + for v in decl_expr_ids(d): + if not 0 <= v <= max_ie: + error(f"declaration references undefined expression id {v}") + if v in taint: + hit |= taint[v] + if hit: + if kind == "inductive": + nm = ", ".join(resolve(ty["name"]) for ty in d["types"]) + else: + nm = resolve(d["name"]) + for t2 in hit: + citers.setdefault(t2, set()).add(nm) + + if not meta_seen: + error("export has no meta line; format version unverified") + + if declared_axioms != permitted: + unpermitted = sorted(declared_axioms - permitted) + undeclared = sorted(permitted - declared_axioms) + if unpermitted: + violation(f"axiom(s) declared but not permitted: {unpermitted}") + if undeclared: + violation(f"permitted axiom(s) not declared in the export (stale census " + f"entry): {undeclared}") + + for t in sorted(UNREFERENCED): + if const_cited[t] or citers.get(t): + violation(f"'{t}' is cited by: {sorted(citers.get(t, {''}))}") + for t, allowed in RESTRICTED.items(): + extra = citers.get(t, set()) - allowed + if extra: + violation(f"'{t}' is cited outside its allowance {sorted(allowed)}: " + f"{sorted(extra)}") + + # Print the full census whether or not anything was flagged: this is the actionable + # state when a check above has flagged a stale or widened axiom list. + print(f"export axiom census: {len(declared_axioms)} axiom(s) declared:") + for a in sorted(declared_axioms): + cited = ([] if a not in TARGETS else + sorted(citers.get(a, set())) or ["nothing"]) + note = f" (cited by: {', '.join(cited)})" if cited else "" + print(f" {a}{note}") + + if violations: + for msg in violations[:MAX_REPORTED_VIOLATIONS]: + print(f"VIOLATION: {msg}", file=sys.stderr) + if len(violations) > MAX_REPORTED_VIOLATIONS: + print(f"... and {len(violations) - MAX_REPORTED_VIOLATIONS} further " + f"violation(s)", file=sys.stderr) + sys.exit(1) + print("export axiom census: all checks passed") + + +if __name__ == "__main__": + main() diff --git a/scripts/check_nanoda.sh b/scripts/check_nanoda.sh new file mode 100755 index 0000000..9263b85 --- /dev/null +++ b/scripts/check_nanoda.sh @@ -0,0 +1,59 @@ +#!/usr/bin/env bash +# Re-check the built library with nanoda, an independent reimplementation of the Lean +# kernel in Rust (https://github.com/ammkrn/nanoda_lib). The point is kernel-level +# defence in depth: a proof of False exploiting a kernel soundness bug would also have +# to get past a second, independently implemented checker (cf. the postmortem of +# lean4#14576, which recommends exactly this). +# +# Usage: scripts/check_nanoda.sh +# The library must already be built (`lake build`). Set LAKE to choose the lake that +# provides the export environment (default: `lake` from PATH). +# +# scripts/nanoda-config.json is the machine-checked axiom census: nanoda's strict mode +# fails on any axiom declared outside its `permitted_axioms`, and `pp_declars` fails if +# an expected native_decide axiom disappears from the export. In between, +# scripts/check_export_axioms.py closes the remaining gap: axioms that must be +# permitted because Lean core declares them unconditionally, but must remain unused +# (`sorryAx` in particular) are checked to be cited by nothing. +set -euo pipefail + +LEAN4EXPORT=${1:?usage: check_nanoda.sh } +NANODA=${2:?usage: check_nanoda.sh } +LAKE=${LAKE:-lake} + +# The export roots. Every module of the package must be reachable from these (checked +# below), so a module cannot silently drop out of the re-check. MetaCheck is +# deliberately absent: it is not part of the production library, and its forged axioms +# exist to be rejected. +ROOTS=(CompElliptic CompElliptic.Fields.Jubjub FastFieldNative) + +python3 - "${ROOTS[@]}" <<'EOF' +import re, sys +from pathlib import Path +roots = sys.argv[1:] +files = [Path("CompElliptic.lean"), Path("FastFieldNative.lean")] +files += sorted(Path("CompElliptic").rglob("*.lean")) +mod = lambda p: ".".join(p.with_suffix("").parts) +imports = {mod(f): set(re.findall(r"^import\s+([A-Za-z0-9_.]+)", f.read_text(), re.M)) + for f in files} +reachable, todo = set(), list(roots) +while todo: + m = todo.pop() + if m in reachable or m not in imports: + continue + reachable.add(m) + todo.extend(imports[m]) +missing = sorted(set(imports) - reachable) +if missing: + print("VIOLATION: module(s) outside the export roots' import closure:", + file=sys.stderr) + for m in missing: + print(f" {m}", file=sys.stderr) + sys.exit(1) +print(f"export coverage: all {len(imports)} project modules reachable from the roots") +EOF + +mkdir -p work +"$LAKE" env "$LEAN4EXPORT" "${ROOTS[@]}" > work/compelliptic-export.ndjson +python3 scripts/check_export_axioms.py scripts/nanoda-config.json +"$NANODA" scripts/nanoda-config.json diff --git a/scripts/nanoda-config.json b/scripts/nanoda-config.json new file mode 100644 index 0000000..53b1015 --- /dev/null +++ b/scripts/nanoda-config.json @@ -0,0 +1,34 @@ +{ + "export_file_path": "work/compelliptic-export.ndjson", + "use_stdin": false, + "permitted_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "sorryAx", + "Lean.trustCompiler", + "Lean.ofReduceBool", + "Lean.ofReduceNat", + "CompElliptic.Fields.Pasta.pallasBase._native.native_decide.ax_1", + "CompElliptic.Fields.Pasta.pallasBase._native.native_decide.ax_2", + "CompElliptic.Fields.Pasta.vestaBase._native.native_decide.ax_1", + "CompElliptic.Fields.Pasta.vestaBase._native.native_decide.ax_2", + "CompElliptic.Curves.Pasta.Pallas.q_nsmul_Gpt._native.native_decide.ax_1_1", + "CompElliptic.Curves.Pasta.Vesta.p_nsmul_Gpt._native.native_decide.ax_1_1" + ], + "unpermitted_axiom_hard_error": true, + "num_threads": 4, + "nat_extension": true, + "string_extension": true, + "pp_declars": [ + "CompElliptic.Fields.Pasta.pallasBase._native.native_decide.ax_1", + "CompElliptic.Fields.Pasta.pallasBase._native.native_decide.ax_2", + "CompElliptic.Fields.Pasta.vestaBase._native.native_decide.ax_1", + "CompElliptic.Fields.Pasta.vestaBase._native.native_decide.ax_2", + "CompElliptic.Curves.Pasta.Pallas.q_nsmul_Gpt._native.native_decide.ax_1_1", + "CompElliptic.Curves.Pasta.Vesta.p_nsmul_Gpt._native.native_decide.ax_1_1" + ], + "unknown_pp_declar_hard_error": true, + "pp_to_stdout": true, + "print_success_message": true +}