From 75236795238503b29b4a0edd5158f4be0a329961 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Mon, 27 Jul 2026 14:26:36 +0100 Subject: [PATCH] meta: enforce that native-executing checks are opt-in Plain lake build already builds and loads the FastFieldNative dylib: the lane's proof modules import its definition modules, and neither declaration order nor glob overlap prevents the shared facet from being built for their elaboration (tested and refuted on Lean/Lake v4.30.0). Since loading is inseparable from the lane's kernel-verified proofs, the enforceable opt-in boundary is one level up: scripts/check_native_optin.py fails the build if any module whose import closure reaches a lane module contains an evaluation-based check (#eval, #guard, native_decide) without an explicit opt-in entry. Documents the observed Lake behaviour in the research doc (Appendix C), the lakefile, and the README. Co-authored-by: Claude Fable 5 --- .github/workflows/ci.yml | 10 ++ README.md | 12 ++- design/lean-native-trust-research.md | 29 ++++++ lakefile.lean | 6 ++ scripts/check_native_lane.sh | 12 +-- scripts/check_native_optin.py | 133 +++++++++++++++++++++++++++ 6 files changed, 195 insertions(+), 7 deletions(-) create mode 100755 scripts/check_native_optin.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 92a2b03..d241722 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -61,3 +61,13 @@ jobs: persist-credentials: false - name: Check every @[csimp] declaration has an assert_axioms entry run: scripts/check_csimp_census.sh + + native-optin: + name: native-executing checks are opt-in + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 + with: + persist-credentials: false + - name: Check no ambient evaluation-based checks in the lane import cone + run: python3 scripts/check_native_optin.py diff --git a/README.md b/README.md index 4be69ba..e450750 100644 --- a/README.md +++ b/README.md @@ -101,7 +101,17 @@ uses of `@[csimp]` — but we anyway check that if such were added, each replace its own `assert_axioms` entry in `CompElliptic/TrustBoundary.lean`, preventing "axiom smuggling" via this route. This is enforced by `scripts/check_csimp_census.sh` in CI. -For the `@[csimp]` check and in general, we do not attempt to guard against adversarial code. +Executing a check through locally compiled native code (a `precompileModules` dylib) trusts +the C emitter, the local C toolchain, and the loader, coarse-grained and with no axiom trace — +a larger surface than `native_decide`'s per-computation axioms. Loading the lane's dylib is +inseparable from elaborating its proof modules, so the enforced invariant sits at the level of +checks: no module reaching a lane module by imports may contain an evaluation-based check +(`#eval`, `#guard`, `native_decide`) unless explicitly opted in, enforced by +`scripts/check_native_optin.py` in CI. See `design/lean-native-trust-research.md` (Appendix C) +for the observed Lake behaviour behind this rule. + +For the `@[csimp]` check, the native opt-in check, and in general, we do not attempt to guard +against adversarial code. ## Status diff --git a/design/lean-native-trust-research.md b/design/lean-native-trust-research.md index a0a0a1f..5102243 100644 --- a/design/lean-native-trust-research.md +++ b/design/lean-native-trust-research.md @@ -390,6 +390,35 @@ generator; at v4.30.0 the lowering is `ToIR.lean`, written in Lean. --- +## Appendix C: Lake and the precompiled lane in practice (observed, this repository) + +Empirical findings on Lean/Lake v4.30.0, from experiments in this repository: + +- **The default build emits and loads the lane dylib.** Plain `lake build` (default + targets only) builds `FastFieldNative:shared`. The cause is not target membership + but imports: the lane's own proof modules (`ProjectiveMontEquiv`, the vendored + Montgomery theorem files, `TrustBoundary`) legitimately import the lane's + definition modules, and Lake builds and loads the owning library's shared facet + for their elaboration. +- **Declaration order and glob overlap are not an opt-in boundary.** The hypothesis + that listing the `CompElliptic` library (whose `andSubmodules` glob covers the + lane modules) before `FastFieldNative` would make the default build interpret + them was tested and refuted: the shared facet is built regardless. Module-to- + library ownership under overlapping globs is not a mechanism one should rely on + for trust boundaries. +- **Consequence: the enforceable opt-in boundary is at checks, not loading.** + Since dylib loading is inseparable from elaborating the lane's kernel-verified + proofs, the invariant this repository enforces (`scripts/check_native_optin.py`) + is: no module whose import closure reaches a lane module may contain an + evaluation-based check (`#eval`, `#guard`, `native_decide`) unless explicitly + opted in with a rationale. Loading is capability; executing a check through the + loaded code is the trust event. +- **Related hazard: silent dylib-name collision.** Lean module names are global + across a build, and a downstream repository declaring its own precompiled + library with the same root module name as a dependency's collides silently — + the build stays green, one shared object is never emitted, and the affected + modules quietly run interpreted. Dotted library names avoid this. + ## Sources Documentation: diff --git a/lakefile.lean b/lakefile.lean index 789703c..af2f0b6 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -21,6 +21,12 @@ lean_lib CompElliptic where -- the whole import closure, so one mathlib-side import silently makes the build enormous -- hence -- the definitions/proofs split, and `scripts/check_native_lane.sh`. `FastFieldNative.lean` exists -- only because Lean derives a dynlib's `initialize_...` symbol from the library name. +-- NOTE (observed on Lean/Lake v4.30.0): declaring the `CompElliptic` library first does NOT +-- stop the default build from building and loading this lane's dylib — the lane's proof +-- modules import the definition modules, so the shared facet is built for their elaboration. +-- Ownership under overlapping globs and declaration order is not an opt-in boundary; the +-- opt-in invariant for native-executing checks is enforced by `scripts/check_native_optin.py` +-- (see `design/lean-native-trust-research.md`, Appendix C). lean_lib FastFieldNative where precompileModules := true globs := #[ diff --git a/scripts/check_native_lane.sh b/scripts/check_native_lane.sh index 9e6d2dd..6b3d21f 100755 --- a/scripts/check_native_lane.sh +++ b/scripts/check_native_lane.sh @@ -6,12 +6,12 @@ set -euo pipefail cd "$(dirname "$0")/.." -# The lane, mirroring the `FastFieldNative` globs in lakefile.lean. -LANE=( - "FastFieldNative.lean" - "CompElliptic/Vendor/CompPoly/Montgomery/Native64x8Defs.lean" - "CompElliptic/Curves/Pasta/Fast/ProjectiveMontDefs.lean" -) +# The lane, parsed from lakefile.lean's precompileModules libraries (the single +# source of truth) via check_native_optin.py; module names become file paths. +LANE_MODULES=() +mapfile -t LANE_MODULES < <(python3 scripts/check_native_optin.py --print-lane) +LANE=() +for mod in "${LANE_MODULES[@]}"; do LANE+=("${mod//.//}.lean"); done # `FastFieldNative.lean` is the root module; it may import the rest of the lane and nothing else. status=0 diff --git a/scripts/check_native_optin.py b/scripts/check_native_optin.py new file mode 100755 index 0000000..8d5220c --- /dev/null +++ b/scripts/check_native_optin.py @@ -0,0 +1,133 @@ +#!/usr/bin/env python3 +"""Check that native-executing checks are opt-in. + +Elaborating a module that (transitively) imports a `precompileModules` lane module +loads the lane's locally compiled dylib, and the interpreter then dispatches calls +into it for any evaluation run during that module's elaboration. Loading is +unavoidable for the lane's own proof modules, so the enforced invariant is one +level up: no module whose import closure reaches a lane module may contain an +evaluation-based check (`#eval`, `#guard`, `native_decide`) unless it is on the +explicit opt-in list below. A check that executes locally compiled native code +trusts the C emitter, the local C toolchain, and the loader, coarse-grained and +with no axiom trace — so it must be a documented decision, never ambient. + +The lane is parsed from lakefile.lean (the single source of truth): every +`lean_lib` with `precompileModules := true` contributes its glob entries. +`--print-lane` prints the lane module names, one per line, for consumption by +`scripts/check_native_lane.sh` — so the lakefile is the only place the lane is +stated. Parse failures are violations, not skips. + +Scope: textual, non-adversarial (comments and strings are stripped heuristically; +crafted code could evade this). Run from the repository root; exits non-zero on +violation. +""" +import re, sys +from pathlib import Path + +def parse_lane(): + text = Path("lakefile.lean").read_text() + lane = [] # (kind, module-name) with kind in {"one", "andSubmodules"} + for block in re.split(r"(?m)^lean_lib\s+", text)[1:]: + name_m = re.match(r"([A-Za-z0-9_.]+)\s+where", block) + if not name_m or not re.search(r"precompileModules\s*:=\s*true", block): + continue + globs = re.search(r"globs\s*:=\s*#\[(.*?)\]", block, re.S) + entries = re.findall(r"\.(one|andSubmodules)\s+`([A-Za-z0-9_.]+)", + globs.group(1)) if globs else [] + if not entries: + print(f"ERROR: cannot parse the globs of precompileModules library " + f"{name_m.group(1)}; extend parse_lane", file=sys.stderr) + sys.exit(2) + lane.extend(entries) + if not lane: + print("ERROR: no precompileModules library found in lakefile.lean; " + "if the lane was removed, retire this script", file=sys.stderr) + sys.exit(2) + return lane + +LANE_ENTRIES = parse_lane() + +def is_lane(mod: str) -> bool: + return any(mod == name or (kind == "andSubmodules" and mod.startswith(name + ".")) + for kind, name in LANE_ENTRIES) +# Modules allowed to contain evaluation-based checks despite reaching a lane +# module. Add a module here only with a comment saying which checks it runs and +# why native execution is intended. +OPT_IN = set() + +EVAL_TOKENS = re.compile(r"#eval\b|#guard\b|\bnative_decide\b|\bdecide\s*\+\s*native\b") + +def module_name(path: Path) -> str: + return ".".join(path.with_suffix("").parts) + +def strip_code(text: str) -> str: + # Remove block comments (with nesting), line comments, and string literals. + out, i, depth, n = [], 0, 0, len(text) + while i < n: + two = text[i:i+2] + if two == "/-": + depth += 1; i += 2; continue + if depth > 0: + if two == "-/": + depth -= 1; i += 2 + else: + i += 1 + continue + if two == "--": + j = text.find("\n", i) + i = n if j == -1 else j + continue + if text[i] == '"': + j = i + 1 + while j < n and text[j] != '"': + j += 2 if text[j] == "\\" else 1 + i = j + 1 + continue + out.append(text[i]); i += 1 + return "".join(out) + +if "--print-lane" in sys.argv[1:]: + for kind, name in LANE_ENTRIES: + if kind != "one": + print(f"ERROR: --print-lane only supports .one entries (got .{kind} " + f"{name}); teach check_native_lane.sh about prefixes first", + file=sys.stderr) + sys.exit(2) + print(name) + sys.exit(0) + +files = sorted(p for p in Path(".").glob("*.lean") if p.name != "lakefile.lean") \ + + sorted(Path("CompElliptic").rglob("*.lean")) +imports = {} +for f in files: + mods = re.findall(r"^import\s+([A-Za-z0-9_.]+)", f.read_text(), re.M) + imports[module_name(f)] = set(mods) + +# Modules whose import closure reaches the lane. +reaches = set() +changed = True +while changed: + changed = False + for m, deps in imports.items(): + if m not in reaches and any(is_lane(d) or d in reaches for d in deps): + reaches.add(m); changed = True + +status = 0 +for f in files: + m = module_name(f) + if m not in reaches or is_lane(m) or m in OPT_IN: + continue + code = strip_code(f.read_text()) + hits = sorted(set(EVAL_TOKENS.findall(code))) + if hits: + print(f"VIOLATION: {f} reaches a precompiled lane module and contains " + f"evaluation-based check(s) {hits}; native-executing checks must be " + f"opt-in — add the module to OPT_IN in this script with a rationale, " + f"or move the check out of the lane's import cone", file=sys.stderr) + status = 1 + +in_cone = sorted(m for m in reaches if not is_lane(m) and m in imports) +print(f"native opt-in: {len(in_cone)} module(s) in the lane import cone, " + f"{len(OPT_IN)} opted in, no ambient native-executing checks" + if status == 0 else "native opt-in: violations found", file=sys.stdout) +sys.exit(status)