feat: add replay phase measurement adapter

Main.lean

@@ -21,6 +21,7 @@ structure Context where
   whichLandrun : String
   whichLean4Export : String
   externalKernels : (Std.TreeMap String (Array String))
+  measurementCommand : Option (Array String)
 
 abbrev M := ReaderT Context IO
 
@@ -85,10 +86,31 @@ def buildLandrunArgs (spawnArgs : LandrunArgs) : Array String :=
   let args := spawnArgs.executablePaths.foldl (init := args) (fun acc path => acc ++ #["--rox", path.toString])
   args ++ #["--", spawnArgs.cmd] ++ spawnArgs.args
 
-def runSandBoxedWithStdout (spawnArgs : LandrunArgs) : M String := do
+/-- Optionally place a trusted measurement adapter outside landrun.
+
+The adapter receives `--phase <phase> -- <landrun> <args...>` and must preserve
+the wrapped process's stdout, stderr, and exit code. This lets replay
+infrastructure measure the sandboxed solution build/export separately from an
+external checker without moving either untrusted operation outside landrun.
+Ordinary comparator callers configure no adapter and retain the exact previous
+execution path. -/
+def measuredCommand (landrun : String) (args : Array String)
+    (phase : Option String) (adapter : Option (Array String)) : String × Array String :=
+  match phase, adapter with
+  | some phase, some command =>
+    if command.isEmpty then
+      (landrun, args)
+    else
+      (command[0]!, command[1...*].toArray ++ #["--phase", phase, "--", landrun] ++ args)
+  | _, _ => (landrun, args)
+
+def runSandBoxedWithStdout (spawnArgs : LandrunArgs)
+    (measurementPhase : Option String := none) : M String := do
   let args := buildLandrunArgs spawnArgs
+  let (cmd, args) := measuredCommand
+    (← read).whichLandrun args measurementPhase (← read).measurementCommand
   let { stdout, stderr, exitCode } ← IO.Process.output {
-    cmd := (← read).whichLandrun,
+    cmd
     args,
     env := spawnArgs.envOverride
     cwd := (← getProjectDir)
@@ -99,10 +121,13 @@ def runSandBoxedWithStdout (spawnArgs : LandrunArgs) : M String := do
   return stdout
 
 
-def runSandBoxed (spawnArgs : LandrunArgs) : M Unit := do
+def runSandBoxed (spawnArgs : LandrunArgs)
+    (measurementPhase : Option String := none) : M Unit := do
   let args := buildLandrunArgs spawnArgs
+  let (cmd, args) := measuredCommand
+    (← read).whichLandrun args measurementPhase (← read).measurementCommand
   let proc ← IO.Process.spawn {
-    cmd := (← read).whichLandrun,
+    cmd
     args,
     env := spawnArgs.envOverride
     cwd := (← getProjectDir)
@@ -111,7 +136,7 @@ def runSandBoxed (spawnArgs : LandrunArgs) : M Unit := do
   if ret != 0 then
     throw <| .userError s!"Child exited with {ret}"
 
-def safeLakeBuild (target : Lean.Name) : M Unit := do
+def safeLakeBuild (target : Lean.Name) (measurementPhase : Option String := none) : M Unit := do
   IO.println s!"Building {target}"
   let leanPrefix ← getLeanPrefix
   let projectDir ← getProjectDir
@@ -129,9 +154,10 @@ def safeLakeBuild (target : Lean.Name) : M Unit := do
     readablePaths := #[projectDir]
     writablePaths := #[dotLakeDir]
     executablePaths := #[leanPrefix, gitLocation]
-  }
+  } measurementPhase
 
-def safeExport (module : Lean.Name) (decls : Array Lean.Name) : M String := do
+def safeExport (module : Lean.Name) (decls : Array Lean.Name)
+    (measurementPhase : Option String := none) : M String := do
   IO.println s!"Exporting {decls} from {module}"
   let baseArgs := #[module.toString, "--"]
   let args := decls.foldl (·.push <| ·.toString) baseArgs
@@ -147,7 +173,7 @@ def safeExport (module : Lean.Name) (decls : Array Lean.Name) : M String := do
     readablePaths := #[projectDir, dotLakeDir]
     writablePaths := #[]
     executablePaths := #[leanPrefix]
-  }
+  } measurementPhase
 
 def runExternalKernel (kernelName : String) (kernelCommand : Array String)
     (solutionExport : String) : M (Option String) := do
@@ -184,10 +210,12 @@ def runExternalKernel (kernelName : String) (kernelCommand : Array String)
       executablePaths := #[]
     }
     let args := buildLandrunArgs spawnArgs
+    let (cmd, args) := measuredCommand
+      (← read).whichLandrun args (some "checker") (← read).measurementCommand
 
     try
       let proc ← IO.Process.spawn {
-        cmd := (← read).whichLandrun,
+        cmd
         args,
         env := spawnArgs.envOverride
         cwd := (← getProjectDir)
@@ -301,8 +329,8 @@ def compareIt : M Unit := do
   let challengeExport ← safeExport challengeModule exportTargets
 
   let solutionModule ← getSolutionModule
-  safeLakeBuild solutionModule
-  let solutionExport ← safeExport solutionModule exportTargets
+  safeLakeBuild solutionModule (some "build")
+  let solutionExport ← safeExport solutionModule exportTargets (some "build")
 
   verifyMatch challengeExport solutionExport
 
@@ -316,6 +344,7 @@ structure Config where
   permitted_axioms : Array String
   enable_nanoda? : Option Bool
   external_kernels? : Option (Std.TreeMap String (Array String))
+  measurement_command? : Option (Array String)
   deriving Lean.FromJson, Lean.ToJson, Repr
 
 def M.run (x : M α) (cfg : Config) : IO α := do
@@ -325,6 +354,7 @@ def M.run (x : M α) (cfg : Config) : IO α := do
   let whichLean4Export := (← IO.getEnv "COMPARATOR_LEAN4EXPORT").getD "lean4export"
   let whichLandrun := (← IO.getEnv "COMPARATOR_LANDRUN").getD "landrun"
   let mut externalKernels := cfg.external_kernels?.getD {}
+  let measurementCommand := cfg.measurement_command?
   let defaultNanoda := "nanoda_bin"
   let nanodaOverride? ← IO.getEnv "COMPARATOR_NANODA"
 
@@ -335,6 +365,10 @@ def M.run (x : M α) (cfg : Config) : IO α := do
     if kernelCommand.isEmpty then
       throw <| .userError s!"{kernelName} has an empty command"
 
+  if let some command := measurementCommand then
+    if command.isEmpty then
+      throw <| .userError "measurement_command must not be empty"
+
   if cfg.enable_nanoda?.getD false then
     let whichNanoda := nanodaOverride?.getD defaultNanoda
     externalKernels := externalKernels.insert "nanoda" #[whichNanoda]
@@ -352,7 +386,8 @@ def M.run (x : M α) (cfg : Config) : IO α := do
     gitLocation := gitLocation,
     whichLean4Export := whichLean4Export,
     whichLandrun := whichLandrun,
-    externalKernels := externalKernels
+    externalKernels := externalKernels,
+    measurementCommand
   }
 
 end Comparator

README.md

@@ -25,6 +25,27 @@ Where `Challenge.lean` contains at least a theorem named `todo1` that has a `sor
 and `Solution.lean` is provided by a party trying to convince you that they have proven `todo1` by
 writing out the same theorem but with a proper proof attached.
 
+### Optional phase measurement adapter
+
+A trusted caller may set `measurement_command` to a non-empty argv array. For
+the untrusted solution only, Comparator then invokes the adapter outside
+Landrun as:
+
+```
+<measurement_command...> --phase build -- <landrun> <args...>
+<measurement_command...> --phase checker -- <landrun> <args...>
+```
+
+The `build` phase is emitted separately for the solution build and export. The
+`checker` phase is emitted for each configured external kernel. The adapter
+must transparently preserve the wrapped command's standard streams and exit
+status; it may aggregate wall time or performance counters in a location that
+untrusted code cannot write. Challenge build/export and the built-in kernel
+are deliberately not labeled as solution build or external-checker cost.
+
+With no `measurement_command`, Comparator executes Landrun directly as before.
+An empty adapter argv is rejected rather than silently disabling measurement.
+
 Given the following assumptions:
 1. The transitive closure of imports of `Challenge.lean` as well as `lakefile.toml`/`lakefile.lean`
    are controlled by you or trustworthy.

runtests.lean

@@ -25,6 +25,7 @@ open Lean System.FilePath IO.FS IO.Process System
 
 structure TestConfig where
   exit_code : Nat
+  expected_measurement_phases : Option (Array String) := none
   deriving FromJson, ToJson
 
 inductive TestResult
@@ -86,7 +87,7 @@ def readTestConfig (configPath : FilePath) : IO TestConfig := do
 def getTempDir : IO FilePath := do
   return "/tmp" / s!"lean_test_{← IO.rand 0 999999}"
 
-def runTestProject (projectPath : FilePath) (projectName : String) (testsDir : FilePath)
+def runTestProject (projectPath : FilePath) (projectName : String) (_testsDir : FilePath)
     (comparatorPath : FilePath) : IO TestResult := do
   try
     let configPath := projectPath / "test.json"
@@ -103,6 +104,13 @@ def runTestProject (projectPath : FilePath) (projectName : String) (testsDir : F
 
     let exitCode ← runCommandInDir tempDir "lake" #["env", comparatorPath.toString, "config.json"]
 
+    if let some expected := config.expected_measurement_phases then
+      let raw ← IO.FS.readFile (tempDir / "measurement.log")
+      let actual := raw.splitOn "\n" |>.filter (!·.isEmpty) |>.toArray
+      if actual != expected then
+        IO.FS.removeDirAll tempDir
+        return .error projectName s!"Measurement phases mismatch: expected {expected}, got {actual}"
+
     IO.FS.removeDirAll tempDir
 
     if exitCode == config.exit_code then

tests/projects/empty_measurement_command/Challenge.lean

@@ -0,0 +1 @@
+theorem fixture : True := by sorry

tests/projects/empty_measurement_command/Solution.lean

@@ -0,0 +1 @@
+theorem fixture : True := by trivial

tests/projects/empty_measurement_command/config.json

@@ -0,0 +1,7 @@
+{
+    "challenge_module": "Challenge",
+    "solution_module": "Solution",
+    "theorem_names": ["fixture"],
+    "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
+    "measurement_command": []
+}

tests/projects/empty_measurement_command/test.json

@@ -0,0 +1,3 @@
+{
+    "exit_code": 1
+}

tests/projects/simple_match/config.json

@@ -3,5 +3,7 @@
     "solution_module": "Solution",
     "theorem_names": ["comm"],
     "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
-    "enable_nanoda": false
+    "enable_nanoda": false,
+    "external_kernels": {"fixture": ["true"]},
+    "measurement_command": ["/bin/sh", "measurement-adapter.sh", "measurement.log"]
 }

tests/projects/simple_match/measurement-adapter.sh

@@ -0,0 +1,12 @@
+#!/bin/sh
+set -eu
+
+log=$1
+shift
+test "$1" = "--phase"
+phase=$2
+shift 2
+test "$1" = "--"
+shift
+printf '%s\n' "$phase" >> "$log"
+exec "$@"

tests/projects/simple_match/test.json

@@ -1,3 +1,4 @@
 {
-        "exit_code": 0
+    "exit_code": 0,
+    "expected_measurement_phases": ["build", "build", "checker"]
 }