Add optional structured verification results

.github/workflows/lean_action_ci.yml

@@ -54,3 +54,4 @@ jobs:
         run: |
           export PATH="$GITHUB_WORKSPACE/nanoda/target/release:$GITHUB_WORKSPACE/lean4export/.lake/build/bin:$GITHUB_WORKSPACE/landrun:$PATH"
           lean --run runtests.lean
+          python3 scripts/test-results.py

Main.lean

@@ -9,7 +9,19 @@ import Export.Parse
 
 namespace Comparator
 
+/-- Optional machine result. An absent result never establishes acceptance. -/
+structure VerificationResult where
+  schemaVersion : Nat := 1
+  outcome : String := "error"
+  stage : String := "configuration"
+  reason : String := "execution_error"
+  detail : String := ""
+  config : Lean.Json := .null
+  leanVersion : String := Lean.versionString
+  deriving Lean.ToJson
+
 structure Context where
+  result : Option (IO.Ref VerificationResult) := none
   projectDir : System.FilePath
   challengeModule : Lean.Name
   solutionModule : Lean.Name
@@ -24,6 +36,15 @@ structure Context where
 
 abbrev M := ReaderT Context IO
 
+def setStage (stage : String) : M Unit := do
+  if let some result := (← read).result then
+    result.modify fun r => { r with stage }
+
+def reject (reason detail : String) : M Unit := do
+  if let some result := (← read).result then
+    result.modify fun r => { r with outcome := "rejected", reason, detail }
+  throw <| IO.userError detail
+
 structure LandrunArgs where
   cmd : String
   args : Array String
@@ -287,30 +308,45 @@ def stringStream (s : String) : BaseIO IO.FS.Stream := do
 
 def verifyMatch (challengeExport : String) (solutionExport : String) :
     M Unit := do
+  setStage "parse_exports"
   let challenge ← Export.parseStream (← stringStream challengeExport)
   let solution ← Export.parseStream (← stringStream solutionExport)
   let theoremNames ← getTheoremNames
   let definitionNames ← getDefinitionNames
   let targets := (← getTheoremNames) ++ (← getLegalAxioms)
-  IO.ofExcept <| Comparator.compareAt challenge solution targets definitionNames (← primitiveTargets)
-  IO.ofExcept <| Comparator.checkAxioms solution theoremNames definitionNames (← getLegalAxioms)
-  let mut result := none
+  setStage "target_comparison"
+  if let .error error := Comparator.compareAt challenge solution targets definitionNames (← primitiveTargets) then
+    reject "target_mismatch" error
+  setStage "axiom_policy"
+  if let .error error := Comparator.checkAxioms solution theoremNames definitionNames (← getLegalAxioms) then
+    reject "disallowed_axiom" error
+  -- External kernels have no shared rejection protocol. A nonzero exit is an error.
+  let mut externalError := none
+  setStage "external_kernels"
   for (kernelName, kernelCommand) in ← getExternalKernels do
-    result := result <|> (← runExternalKernel kernelName kernelCommand solutionExport)
-  result := result <|> (← runBuiltinKernel solution)
-  if let some error := result then
+    externalError := externalError <|> (← runExternalKernel kernelName kernelCommand solutionExport)
+  setStage "lean_kernel"
+  let builtinError ← runBuiltinKernel solution
+  if let some error := externalError then
+    setStage "external_kernels"
     throw <| IO.userError error
+  if let some error := builtinError then
+    reject "kernel_rejected" error
 
 def compareIt : M Unit := do
   let exportTargets := (← builtinTargets) ++ (← getTheoremNames) ++ (← getLegalAxioms)
     ++ (← primitiveTargets) ++ (← getDefinitionNames)
 
   let challengeModule ← getChallengeModule
+  setStage "challenge_build"
   safeLakeBuild challengeModule
+  setStage "challenge_export"
   let challengeExport ← safeExport challengeModule exportTargets
 
   let solutionModule ← getSolutionModule
+  setStage "solution_build"
   safeLakeBuild solutionModule
+  setStage "solution_export"
   let solutionExport ← safeExport solutionModule exportTargets
 
   verifyMatch challengeExport solutionExport
@@ -327,7 +363,7 @@ structure Config where
   external_kernels? : Option (Std.TreeMap String (Array String))
   deriving Lean.FromJson, Lean.ToJson, Repr
 
-def M.run (x : M α) (cfg : Config) : IO α := do
+def M.run (x : M α) (cfg : Config) (result : Option (IO.Ref VerificationResult) := none) : IO α := do
   let cwd ← IO.Process.getCurrentDir
   let leanPrefix ← queryLeanPrefix cwd
   let gitLocation ← queryGitLocation
@@ -351,6 +387,7 @@ def M.run (x : M α) (cfg : Config) : IO α := do
     externalKernels := externalKernels.modify "nanoda" fun cmd => cmd.set! 0 nanodaOverride
 
   ReaderT.run x {
+    result := result
     projectDir := cwd
     challengeModule := cfg.challenge_module.toName,
     solutionModule := cfg.solution_module.toName,
@@ -367,8 +404,25 @@ def M.run (x : M α) (cfg : Config) : IO α := do
 end Comparator
 
 def main (args : List String) : IO Unit := do
-  let some (configPath : String) := args[0]?
-    | throw <| .userError "Expected config file path as first argument."
-  let content ← IO.FS.readFile configPath
-  let config ← IO.ofExcept <| Lean.FromJson.fromJson? <| ← IO.ofExcept <| Lean.Json.parse content
-  Comparator.M.run Comparator.compareIt config
+  let (configPath, resultPath) ← match args with
+    | [config] => pure (config, none)
+    | [config, "--result-json", path] => pure (config, some path)
+    | _ => throw <| IO.userError "usage: comparator config.json [--result-json result.json]"
+  -- Reserve a new file before running project code. Keep it outside project-writable paths.
+  let output ← resultPath.mapM fun path => IO.FS.Handle.mk path .writeNew
+  let result ← IO.mkRef ({} : Comparator.VerificationResult)
+  let failure ← try
+    let content ← IO.FS.readFile configPath
+    let config : Comparator.Config ← IO.ofExcept <| Lean.FromJson.fromJson? <| ← IO.ofExcept <| Lean.Json.parse content
+    result.modify fun r => { r with config := Lean.toJson config }
+    Comparator.M.run Comparator.compareIt config (some result)
+    result.modify fun r => { r with outcome := "pass", stage := "complete", reason := "verified" }
+    pure none
+  catch error =>
+    result.modify fun r => { r with detail := error.toString }
+    pure (some error)
+  if let some handle := output then
+    handle.putStr ((Lean.toJson (← result.get)).compress ++ "\n")
+    handle.flush
+  if let some error := failure then
+    throw error

README.md

@@ -137,6 +137,30 @@ def large : Nat := 38
 theorem large_lt : 37 < large := by decide
 ```
 
+## Structured results
+
+`comparator config.json --result-json /trusted-output/result.json` writes a version 1
+JSON result and preserves success/failure exit behavior. The output path must be new
+and outside all paths writable by project code. Existing files are never overwritten.
+Normal log output remains on stdout/stderr.
+
+The result contains `schemaVersion`, `outcome`, `stage`, `reason`, `detail`, the parsed
+`config` and `leanVersion`. `outcome` is:
+
+- `pass`: target comparison, axiom policy and all configured kernels succeeded.
+- `rejected`: target mismatch, disallowed axiom or an explicit builtin-kernel rejection.
+- `error`: configuration, build, export, parse, process or external-kernel failure.
+
+Stages identify where execution stopped. External kernels lack a common rejection
+protocol, so their nonzero exits remain errors; callers must not classify their logs.
+A timeout, killed process, empty/missing/malformed result, or disagreement with the
+exit status is an execution error. Only a complete `pass` with exit zero is acceptance.
+
+This record is not an authenticated receipt. The trusted caller must bind it to the
+exact challenge, submission, dependencies, executable digests, effective environment
+(including kernel overrides), containment policy and run identity. JSON output does
+not change Comparator's trust or sandbox requirements above.
+
 ## Development
 
 The `scripts/fake-landrun.sh` can be used to replace Landrun in development if you are not on a Linux system that supports landrun.

scripts/test-results.py

@@ -0,0 +1,71 @@
+#!/usr/bin/env python3
+"""Exercise result JSON on real trusted fixtures; sandbox qualification is separate."""
+import json
+from pathlib import Path
+import shutil
+import subprocess
+import tempfile
+
+ROOT = Path(__file__).resolve().parents[1]
+BIN = ROOT / '.lake/build/bin/comparator'
+
+
+def invoke(project, *args):
+    return subprocess.run(['lake', 'env', str(BIN), *args], cwd=project,
+                          capture_output=True, text=True, timeout=120)
+
+
+def fixture(root, name, folder=None):
+    project = root / (folder or name)
+    shutil.copytree(ROOT / 'tests/projects' / name, project)
+    shutil.copyfile(ROOT / 'lean-toolchain', project / 'lean-toolchain')
+    if not (project / 'lakefile.toml').exists():
+        (project / 'lakefile.toml').write_text(
+            'name = "resulttest"\n[[lean_lib]]\nname = "Challenge"\n[[lean_lib]]\nname = "Solution"\n')
+    return project
+
+
+def check(project, result, outcome, stage, reason):
+    proc = invoke(project, 'config.json', '--result-json', str(result))
+    data = json.loads(result.read_text())
+    assert data['schemaVersion'] == 1, data
+    assert (data['outcome'], data['stage'], data['reason']) == (outcome, stage, reason), data
+    assert (proc.returncode == 0) == (outcome == 'pass'), proc.stdout + proc.stderr
+    assert data['leanVersion'], data
+    return data
+
+
+def main():
+    with tempfile.TemporaryDirectory() as directory:
+        root = Path(directory)
+        for name, outcome, stage, reason in (
+            ('simple_match', 'pass', 'complete', 'verified'),
+            ('simple_mismatch', 'rejected', 'target_comparison', 'target_mismatch'),
+            ('simple_axiom_issue', 'rejected', 'axiom_policy', 'disallowed_axiom'),
+            ('def_hole_axiom_issue', 'rejected', 'axiom_policy', 'disallowed_axiom'),
+        ):
+            project = fixture(root, name)
+            result = root / (name + '.json')
+            data = check(project, result, outcome, stage, reason)
+            assert data['config']['theorem_names'] == json.loads((project / 'config.json').read_text())['theorem_names']
+            assert (invoke(project, 'config.json').returncode == 0) == (outcome == 'pass')
+            before = result.read_bytes()
+            assert invoke(project, 'config.json', '--result-json', str(result)).returncode != 0
+            assert result.read_bytes() == before
+            print('PASS', name, flush=True)
+        project = fixture(root, 'simple_match', 'bad_config')
+        (project / 'config.json').write_text('{')
+        check(project, root / 'bad_config.json', 'error', 'configuration', 'execution_error')
+        project = fixture(root, 'simple_match', 'bad_build')
+        (project / 'Solution.lean').write_text('this cannot elaborate\n')
+        check(project, root / 'bad_build.json', 'error', 'solution_build', 'execution_error')
+        project = fixture(root, 'simple_match', 'external_error')
+        config = json.loads((project / 'config.json').read_text())
+        config['external_kernels'] = {'crashing_kernel': ['/bin/false']}
+        (project / 'config.json').write_text(json.dumps(config))
+        check(project, root / 'external_error.json', 'error', 'external_kernels', 'execution_error')
+        print('PASS configuration, build and external-process errors; no log classification')
+
+
+if __name__ == '__main__':
+    main()