feat: add lake check to check a project against the kernel

This PR adds `lake check`, which builds a project's default targets, exports them, replays the result through the kernel, and reports the axioms that code rests on, failing on any beyond `propext`, `Classical.choice` and `Quot.sound`. There is no challenge to compare against.

Nothing about the project is evaluated outside the sandbox. `lake env` resolves its dependencies and `lake query :modules` names the modules to check, both inside it, so the project's configuration is never elaborated in Lake's own address space; the build and the export follow in the same sandbox. As for `lake challenge`, this requires the project to carry a `lake-manifest.json`, since the sandbox cannot write one into the project directory.

The exporter is given no declaration list, so the export covers everything in scope rather than only what the project declares, and a check costs roughly the same whatever the project's size: about a minute for a project holding a single theorem. The axiom report copes with that without a list of roots: an axiom that is merely importable is referred to by nothing, so the axioms that some other constant refers to are exactly the ones the code rests on. Note that the kernel accepts `sorryAx`, so a `sorry` is caught by this report and by nothing else.

All the default targets' modules go through the pipeline together, in one sandboxed `lake build`, one export and one kernel replay. Since each module's export already covers its whole import closure, a pass per module would re-check what they share: on a two-root project the roots' exports agree on 6,437,744 of 6,437,817 lines, so the second pass would double the run for two extra constants.

The sandbox invocations in `Lake.Check` get one definition each. `landrunSpawnArgs` builds the `IO.Process.SpawnArgs` that both `runSandBoxedWithStdout` and `runSandBoxedExitCode` use, and `runSandBoxed` is the latter plus the exit-code check. `runExternalKernel` goes through `runSandBoxedExitCode` rather than spawning `landrun` itself, keeping its own messages. `runExporter` holds the exporter's grants, which `safeExport` and `exportModules` had spelled out identically.

The two commands share the tool resolution and the sandbox context through `mkContext`; the vendored comparison path is untouched.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Author: Kha

src/lake/Lake/CLI/Check.lean

@@ -117,29 +117,29 @@ def buildLandrunArgs (spawnArgs : LandrunArgs) : Array String :=
   let args := spawnArgs.connectPorts.foldl (init := args) (fun acc port => acc ++ #["--connect-tcp", port])
   args ++ #["--", spawnArgs.cmd] ++ spawnArgs.args
 
-def runSandBoxedWithStdout (spawnArgs : LandrunArgs) : M String := do
-  let args := buildLandrunArgs spawnArgs
-  let { stdout, stderr, exitCode } ← IO.Process.output {
-    cmd := (← read).whichLandrun,
-    args,
+/-- The `landrun` invocation that puts `spawnArgs` under the sandbox. -/
+def landrunSpawnArgs (spawnArgs : LandrunArgs) : M IO.Process.SpawnArgs := do
+  return {
+    cmd := (← read).whichLandrun
+    args := buildLandrunArgs spawnArgs
     env := spawnArgs.envOverride
-    cwd := (← getProjectDir)
+    cwd := ← getProjectDir
   }
+
+def runSandBoxedWithStdout (spawnArgs : LandrunArgs) : M String := do
+  let { stdout, stderr, exitCode } ← IO.Process.output (← landrunSpawnArgs spawnArgs)
   IO.eprint stderr
   if exitCode != 0 then
     throw <| .userError s!"Child exited with {exitCode}"
   return stdout
 
+/-- Runs `spawnArgs` sandboxed, letting its output through, and returns its exit code. -/
+def runSandBoxedExitCode (spawnArgs : LandrunArgs) : M UInt32 := do
+  let proc ← IO.Process.spawn (← landrunSpawnArgs spawnArgs)
+  proc.wait
 
 def runSandBoxed (spawnArgs : LandrunArgs) : M Unit := do
-  let args := buildLandrunArgs spawnArgs
-  let proc ← IO.Process.spawn {
-    cmd := (← read).whichLandrun,
-    args,
-    env := spawnArgs.envOverride
-    cwd := (← getProjectDir)
-  }
-  let ret ← proc.wait
+  let ret ← runSandBoxedExitCode spawnArgs
   if ret != 0 then
     throw <| .userError s!"Child exited with {ret}"
 
@@ -183,8 +183,34 @@ def safeResolveWorkspace : M (String × String) := do
     throw <| .userError "`lake env` did not report the project's search path"
   return (leanPath, binPath)
 
-def safeLakeBuild (target : Lean.Name) : M Unit := do
-  IO.println s!"Building {target}"
+/--
+Asks the project which modules its default targets contain, inside the sandbox.
+
+Resolving targets means evaluating the project's configuration, which is code, so it happens where
+every other evaluation of it happens. `lake query :modules` reports the modules of the package's
+default targets, one per line.
+-/
+def safeQueryModules : M (Array Lean.Name) := do
+  IO.println "Resolving targets"
+  let projectDir ← getProjectDir
+  let whichLake := (← read).whichLake
+  let out ← runSandBoxedWithStdout {
+    cmd := whichLake.toString,
+    args := #["query", ":modules"],
+    envPass := #["PATH", "HOME", "LEAN_ABORT_ON_PANIC"]
+    envOverride := #[("LEAN_ABORT_ON_PANIC", some "1")]
+    readablePaths := #[projectDir]
+    writablePaths := #[projectDir / ".lake"]
+  }
+  let mods := out.split '\n' |>.toStringList |>.filterMap fun line =>
+    let line := line.trimAscii.toString
+    if line.isEmpty then none else some line.toName
+  return mods.toArray
+
+def safeLakeBuild (targets : Array Lean.Name) : M Unit := do
+  let targetArgs := targets.map (·.toString)
+  let targetList := " ".intercalate targetArgs.toList
+  IO.println s!"Building {targetList}"
   let projectDir ← getProjectDir
   let dotLakeDir := projectDir / ".lake"
 
@@ -194,31 +220,31 @@ def safeLakeBuild (target : Lean.Name) : M Unit := do
   let whichLake := (← read).whichLake
   runSandBoxed {
     cmd := whichLake.toString,
-    args := #["build", target.toString],
+    args := #["build"] ++ targetArgs,
     envPass := #["PATH", "HOME", "LEAN_ABORT_ON_PANIC"]
     envOverride := #[("LEAN_ABORT_ON_PANIC", some "1")]
     readablePaths := #[projectDir]
     writablePaths := #[dotLakeDir]
   }
 
-def safeExport (module : Lean.Name) (decls : Array Lean.Name) : M String := do
-  IO.println s!"Exporting {decls} from {module}"
-  let baseArgs := #[module.toString, "--"]
-  let args := decls.foldl (·.push <| ·.toString) baseArgs
-
+/-- Runs the bundled exporter in the sandbox, with the grants every export needs. -/
+def runExporter (args : Array String) : M String := do
   let projectDir ← getProjectDir
-  let dotLakeDir := projectDir / ".lake"
   let whichLean4Export := (← read).whichLean4Export
   runSandBoxedWithStdout {
     cmd := whichLean4Export.toString
-    args := args,
+    args
     envPass := #["PATH", "HOME", "LEAN_PATH", "LEAN_ABORT_ON_PANIC"]
     envOverride := #[("LEAN_ABORT_ON_PANIC", some "1"), ("LEAN_PATH", some (← read).leanPath),
       ("PATH", some (← read).binPath)]
-    readablePaths := #[projectDir, dotLakeDir]
+    readablePaths := #[projectDir, projectDir / ".lake"]
     writablePaths := #[]
   }
 
+def safeExport (module : Lean.Name) (decls : Array Lean.Name) : M String := do
+  IO.println s!"Exporting {decls} from {module}"
+  runExporter <| #[module.toString, "--"] ++ decls.map (·.toString)
+
 def runExternalKernel (kernelName : String) (kernelCommand : Array String)
     (solutionExport : String) : M (Option String) := do
   IO.println s!"Running {kernelName} kernel on solution"
@@ -253,17 +279,8 @@ def runExternalKernel (kernelName : String) (kernelCommand : Array String)
       readablePaths := #[configPath.toString, solutionPath.toString]
       writablePaths := #[]
     }
-    let args := buildLandrunArgs spawnArgs
-
     try
-      let proc ← IO.Process.spawn {
-        cmd := (← read).whichLandrun,
-        args,
-        env := spawnArgs.envOverride
-        cwd := (← getProjectDir)
-      }
-
-      let ret ← proc.wait
+      let ret ← runSandBoxedExitCode spawnArgs
       if ret != 0 then
         IO.println s!"{kernelName} kernel rejected the solution"
         return some s!"{kernelName} exited with {ret}"
@@ -375,11 +392,11 @@ public def compareIt : M Unit := do
     ++ (← primitiveTargets) ++ (← getDefinitionNames)
 
   let challengeModule ← getChallengeModule
-  safeLakeBuild challengeModule
+  safeLakeBuild #[challengeModule]
   let challengeExport ← safeExport challengeModule exportTargets
 
   let solutionModule ← getSolutionModule
-  safeLakeBuild solutionModule
+  safeLakeBuild #[solutionModule]
   let solutionExport ← safeExport solutionModule exportTargets
 
   verifyMatch challengeExport solutionExport
@@ -465,6 +482,35 @@ def resolveExternalKernels (cfg : Config) : IO (Except ExitCode (Std.TreeMap Str
       return .error (← cannotRun s!"`{kernelName}` kernel `{kernelCommand[0]!}` was not found")
   return .ok externalKernels
 
+/-- Exports everything in scope in `modules`. -/
+def exportModules (modules : Array Lean.Name) : M String := do
+  let moduleArgs := modules.map (·.toString)
+  IO.println s!"Exporting the declarations of {" ".intercalate moduleArgs.toList}"
+  runExporter moduleArgs
+
+def standardAxioms : Array Lean.Name :=
+  #[``propext, ``Classical.choice, ``Quot.sound]
+
+/-- Reports the axioms the checked modules rest on, and rejects any beyond `standardAxioms`. -/
+def checkUsedAxioms (exported : LeanExport.ExportedEnv) : M Unit := do
+  let used := usedAxioms exported
+  if used.isEmpty then
+    IO.println "Uses no axioms"
+  else
+    IO.println s!"Uses axioms: {", ".intercalate (used.toList.map (·.1.toString))}"
+  let illegal := used.filter fun (ax, _) => !standardAxioms.contains ax
+  unless illegal.isEmpty do
+    throw <| .userError <| "\n".intercalate <| illegal.toList.map fun (ax, ref) =>
+      s!"Axiom '{ax}' is not permitted; it is used by '{ref}'"
+
+/-- Checks a set of module roots at once against the kernel with no challenge to compare it to. -/
+def checkModules (modules : Array Lean.Name) : M Unit := do
+  safeLakeBuild modules
+  let exported ← LeanExport.parseStream (← stringStream (← exportModules modules))
+  if let some error ← runBuiltinKernel exported then
+    throw <| .userError error
+  checkUsedAxioms exported
+
 /--
 Runs `lake challenge`: builds and exports the challenge and the solution in a sandbox, then judges
 the solution against the challenge.
@@ -514,4 +560,28 @@ public def runChallenge (configFile? : Option System.FilePath) (lean : LeanInsta
     IO.eprintln s!"error: {e}"
     return 1
 
+/--
+Runs `lake check`: builds and exports the project's default targets in the sandbox and checks them
+with the kernel, with no challenge to compare them against.
+-/
+public def runCheck (lean : LeanInstall) (lake : LakeInstall)
+    (projectDir : System.FilePath) : IO ExitCode := do
+  let base ←
+    match ← mkContext "check" lean lake projectDir with
+    | .error rc => return rc
+    | .ok ctx => pure ctx
+  if let some rc ← checkManifest "check" base.projectDir then
+    return rc
+  try
+    let (leanPath, binPath) ← ReaderT.run safeResolveWorkspace base
+    let ctx := { base with leanPath, binPath }
+    let targets ← ReaderT.run safeQueryModules ctx
+    if targets.isEmpty then
+      return ← cannotRun "nothing to check: this project has no default build targets"
+    ReaderT.run (checkModules targets) ctx
+    return 0
+  catch e =>
+    IO.eprintln s!"error: {e}"
+    return 1
+
 end Lake.Check

src/lake/Lake/CLI/Help.lean

@@ -31,6 +31,7 @@ COMMANDS:
   clean                 remove build outputs
   shake                 minimize imports in source files
   challenge             judge a solution against a challenge
+  check                 check this project against external checker(s)
   env <cmd> <args>...   execute a command in Lake's environment
   lean <file>           elaborate a Lean file in Lake's context
   update                update dependencies and save them to the manifest
@@ -479,6 +480,48 @@ HARDENING:
     systemd-run --user --pty --property=RestrictAddressFamilies=~AF_UNIX \\
       lake challenge --config challenge.json"
 
+def helpCheck :=
+"Check this project against external checker(s)
+
+USAGE:
+  lake check
+
+Builds the default build targets, exports them, and replays the result through
+the kernel, erroring on any use of non-standard axioms.
+
+The project is untrusted input: its configuration is evaluated, and its code
+built and exported, inside a `landrun` sandbox, and none of its `.olean` files
+is ever loaded into Lake's own address space. Both the dependencies and the
+targets to check are resolved there, since resolving either evaluates the
+configuration and that is code. `landrun` is required; there is no unsandboxed
+mode, so this command is available on Linux only.
+
+The project has to carry a `lake-manifest.json`, because dependencies are
+resolved inside the sandbox and it cannot write to the project directory.
+Building the project once is enough to write one.
+
+EXIT CODES:
+  0                     the kernel accepts the project and it rests only on the
+                        permitted axioms
+  1                     the kernel rejects it, an axiom is not permitted, or a
+                        build did not succeed
+  2                     could not start: `landrun` is missing, the project has
+                        no `lake-manifest.json`, or it has no default targets
+
+ENVIRONMENT:
+  COMPARATOR_LANDRUN    sandbox executable (default: `landrun` on PATH)
+
+  The exporter is always the `leanexport` of this toolchain, and deliberately
+  not configurable: the export format has to match the compiler that produced
+  the `.olean` files being exported.
+
+HARDENING:
+  The sandbox bounds writes and TCP connections exactly as `lake challenge`'s
+  does, and its limits and the `AF_UNIX` caveat apply here too. See the
+  HARDENING section of `lake help challenge`.
+
+See `lake help challenge` to judge a solution against a challenge instead."
+
 def helpCacheCli :=
 "Manage the Lake cache
 
@@ -864,6 +907,7 @@ public def help : (cmd : String) → String
 | "clean"               => helpClean
 | "shake"               => helpShake
 | "challenge"           => helpChallenge
+| "check"               => helpCheck
 | "script"              => helpScriptCli
 | "scripts"             => helpScriptList
 | "run"                 => helpScriptRun

src/lake/Lake/CLI/Main.lean

@@ -1176,6 +1176,17 @@ protected def challenge : CliM PUnit := do
   let cfg ← mkLoadConfig opts
   exit <| ← Check.runChallenge opts.challengeConfig? leanInstall lakeInstall cfg.wsDir
 
+/-- The `lake check` command: check this project against the kernel. -/
+protected def check : CliM PUnit := do
+  processOptions lakeOption
+  let opts ← getThe LakeOptions
+  noArgsRem do
+  let (leanInstall, lakeInstall) ← opts.getInstall
+  -- The workspace is deliberately not loaded here: evaluating the project's configuration is code
+  -- execution, and containing it is what the sandbox is for.
+  let cfg ← mkLoadConfig opts
+  exit <| ← Check.runCheck leanInstall lakeInstall cfg.wsDir
+
 protected def script : CliM PUnit := do
   if let some cmd ← takeArg? then
     processLeadingOptions lakeOption -- between `lake script <cmd>` and args
@@ -1332,6 +1343,7 @@ def lakeCli : (cmd : String) → CliM PUnit
 | "clean"               => lake.clean
 | "shake"               => lake.shake
 | "challenge"           => lake.challenge
+| "check"               => lake.check
 | "script"              => lake.script
 | "scripts"             => lake.script.list
 | "run"                 => lake.script.run

src/lake/Lake/Check/Axioms.lean

@@ -54,6 +54,22 @@ where
 
 end Axioms
 
+/--
+The axioms some other constant in `env` refers to, each paired with one constant that refers to it.
+-/
+public def usedAxioms (env : LeanExport.ExportedEnv) : Array (Lean.Name × Lean.Name) :=
+  -- `constOrder` is the export order, so the result is deterministic without needing an `Ord`.
+  let collect : StateM (Std.HashSet Lean.Name × Array (Lean.Name × Lean.Name)) Unit := do
+    for name in env.constOrder do
+      let some info := env.constMap[name]? | continue
+      runForUsedConsts info fun ref => do
+        -- `runForUsedConsts` reports the constant itself, which is not an incoming reference
+        unless ref == name do
+          if let some (.axiomInfo ..) := env.constMap[ref]? then
+            modify fun (seen, used) =>
+              if seen.contains ref then (seen, used) else (seen.insert ref, used.push (ref, name))
+  (collect.run ({}, #[])).2.2
+
 public def checkAxioms (solution : LeanExport.ExportedEnv) (theoremTargets : Array Lean.Name)
     (definitionTargets : Array Lean.Name) (legalAxioms : Array Lean.Name) : Except String Unit := do
   let mut worklist := #[]

tests/lake/tests/check-audit-reject/Solution.lean

@@ -0,0 +1,22 @@
+import Lean
+
+open Lean
+
+unsafe def badNatUnsafe : Nat := unsafeCast (-4294967296 : Int)
+
+@[implemented_by badNatUnsafe] opaque badNatVal : Nat
+
+run_elab
+  addDecl <| .defnDecl {
+    name        := .str .anonymous "badNat"
+    levelParams := []
+    type        := .const ``Nat []
+    value       := .lit <| .natVal badNatVal
+    hints       := .opaque
+    safety      := .safe
+  }
+
+theorem boom : False := by
+  have truly_marvelous_0 : ¬badNat ≤ 9223372036854775807 := by decide
+  have truly_marvelous_1 : ¬9223372036854775807 < badNat := by decide
+  omega

tests/lake/tests/check-audit-reject/clean.sh

@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json produced.out

tests/lake/tests/check-audit-reject/lakefile.toml

@@ -0,0 +1,6 @@
+name = "checktest"
+version = "0.1.0"
+defaultTargets = ["Solution"]
+
+[[lean_lib]]
+name = "Solution"

tests/lake/tests/check-audit-reject/test.sh

@@ -0,0 +1,21 @@
+#!/usr/bin/env bash
+source ../common.sh
+
+./clean.sh
+
+if [ "`uname`" != Linux ]; then
+  echo "Skipping test: lake check needs Linux Landlock"
+  exit 0
+fi
+
+# Landlock cannot be assumed available in CI containers; see `../fake-landrun.sh`.
+export COMPARATOR_LANDRUN="$PWD/../fake-landrun.sh"
+
+# `lake check` resolves dependencies inside the sandbox, which cannot write to the project
+# directory, so the manifest has to be in place first. Building the project once does the same;
+# this just skips the build.
+"$LAKE" resolve-deps
+
+test_status_out 1 'error:' check
+
+rm -f produced.out

tests/lake/tests/check-audit/Solution.lean

@@ -0,0 +1,2 @@
+theorem comm (n m : Nat) : n + m = m + n := by
+  grind

tests/lake/tests/check-audit/clean.sh

@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json produced.out