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 +}