meta: enforce that native-executing checks are opt-in

.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

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
 

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:

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 := #[

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

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)