feat: JSON verification reports

Comparator/Compare.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 import Comparator.Axioms
+import Comparator.Json
 import Export.Parse
 
 namespace Comparator
@@ -19,7 +20,7 @@ structure State where
   worklist : Array Lean.Name
   checked : Std.HashSet Lean.Name
 
-abbrev CompareM := ReaderT Context <| StateT State <| Except String
+abbrev CompareM := ReaderT Context <| StateT State <| Except (CheckFailure × String)
 
 deriving instance BEq for Lean.QuotKind
 deriving instance BEq for Lean.QuotVal
@@ -42,15 +43,15 @@ partial def loop : CompareM Unit := do
     loop
   else
     let some challengeConst := (← read).challenge.constMap[target]?
-      | throw s!"Const not found in challenge '{target}'"
+      | throw (.notFound, s!"Const not found in challenge '{target}'")
     let some solutionConst := (← read).solution.constMap[target]?
-      | throw s!"Const not found in solution '{target}'"
+      | throw (.notFound, s!"Const not found in solution '{target}'")
 
     if (← read).definitionTargets.contains solutionConst.name then
       solutionConst.type.getUsedConstants.forM addWorklist
     else
       if challengeConst != solutionConst then
-        throw s!"Const does not match between challenge and target '{target}'"
+        throw (.dependency, s!"Const does not match between challenge and target '{target}'")
       addRelevantConsts solutionConst
 
     modify fun s => { s with checked := s.checked.insert target }
@@ -63,45 +64,47 @@ def definitionHoleMatches (challengeHole solutionHole : Lean.DefinitionVal) : Bo
     && challengeHole.safety == solutionHole.safety
 
 def compareAt (challenge solution : Export.ExportedEnv) (theoremTargets : Array Lean.Name)
-    (definitionTargets : Array Lean.Name) (primitive : Array Lean.Name) : Except String Unit := do
+    (definitionTargets : Array Lean.Name) (primitive : Array Lean.Name)
+    (checked : Std.HashSet Lean.Name := {}) : Except (CheckFailure × String) (Std.HashSet Lean.Name) := do
   let mut worklist := primitive
 
   for target in theoremTargets do
     let some challengeConst := challenge.constMap[target]?
-      | throw s!"Const not found in challenge: '{target}'"
+      | throw (.notFound, s!"Const not found in challenge: '{target}'")
 
     let some solutionConst := solution.constMap[target]?
-      | throw s!"Const not found in solution: '{target}'"
+      | throw (.notFound, s!"Const not found in solution: '{target}'")
 
-    let (challengeConst, solutionConst) ←
+    let (challengeConstVal, solutionConstVal) ←
       match challengeConst, solutionConst with
       | .thmInfo cc, .thmInfo sc
       | .axiomInfo cc, .axiomInfo sc => pure (cc.toConstantVal, sc.toConstantVal)
-      | _, _ => throw s!"Challenge and solution constant kind don't match: '{target}'"
+      | _, _ => throw (.kind (constKind challengeConst) (constKind solutionConst), s!"Challenge and solution constant kind don't match: '{target}'")
 
-    if challengeConst != solutionConst then
-      throw s!"Challenge and solution theorem statement do not match: '{target}'"
+    if challengeConstVal != solutionConstVal then
+      throw (.signature, s!"Challenge and solution theorem statement do not match: '{target}'")
 
-    worklist := worklist ++ challengeConst.type.getUsedConstants
+    worklist := worklist ++ challengeConstVal.type.getUsedConstants
 
   for target in definitionTargets do
-    let some challengeConst := challenge.constMap[target]?
-      | throw s!"Const not found in challenge: '{target}'"
+    let some challengeConstInfo := challenge.constMap[target]?
+      | throw (.notFound, s!"Const not found in challenge: '{target}'")
 
-    let some solutionConst := solution.constMap[target]?
-      | throw s!"Const not found in solution: '{target}'"
+    let some solutionConstInfo := solution.constMap[target]?
+      | throw (.notFound, s!"Const not found in solution: '{target}'")
 
-    let .defnInfo challengeConst := challengeConst
-      | throw s!"Challenge constant is not a definition: '{target}'"
-    let .defnInfo solutionConst := solutionConst
-      | throw s!"Solution constant is not a definition: '{target}'"
+    let .defnInfo challengeConstDef := challengeConstInfo
+      | throw (.kind (constKind challengeConstInfo) (constKind solutionConstInfo), s!"Challenge constant is not a definition: '{target}'")
+    let .defnInfo solutionConstDef := solutionConstInfo
+      | throw (.kind (constKind challengeConstInfo) (constKind solutionConstInfo), s!"Solution constant is not a definition: '{target}'")
 
-    if !definitionHoleMatches challengeConst solutionConst then
-      throw s!"Const does not match between challenge and target '{target}'"
+    if !definitionHoleMatches challengeConstDef solutionConstDef then
+      throw (.signature, s!"Const does not match between challenge and target '{target}'")
 
-    worklist := worklist.push solutionConst.name
+    worklist := worklist.push solutionConstDef.name
 
   let definitionTargets := Std.HashSet.ofArray definitionTargets
-  Compare.loop.run { challenge, solution, definitionTargets } |>.run' { worklist, checked := {} }
+  let (_, s) ← Compare.loop.run { challenge, solution, definitionTargets } |>.run { worklist, checked }
+  return s.checked
 
 end Comparator

Comparator/Json.lean

@@ -0,0 +1,41 @@
+import Lean
+
+namespace Comparator
+
+def constKind : Lean.ConstantInfo → String
+  | .defnInfo _ => "definition"
+  | .thmInfo _ => "theorem"
+  | .axiomInfo _ => "axiom"
+  | .opaqueInfo _ => "opaque"
+  | .quotInfo _ => "quotient"
+  | .inductInfo _ => "inductive"
+  | .ctorInfo _ => "constructor"
+  | .recInfo _ => "recursor"
+
+structure KernelReport where
+  accepted : Option Bool := none
+  failureMessage : Option String := none
+  deriving Lean.ToJson, Inhabited, Repr
+
+inductive CheckFailure where
+  | kind (kind1 kind2 : String) -- Declaration kind mismatch
+  | signature                   -- Target statement/signature mismatch
+  | dependency                  -- Transitive dependency DAG mismatch
+  | axioms                      -- Illegal leaf axioms detected
+  | notFound                    -- Target decl not found
+  deriving Lean.ToJson, Inhabited, Repr
+
+structure TargetReport where
+  targetName : Lean.Name
+  targetKind : String
+  failureCategory : Option CheckFailure
+  failureMessage : Option String
+  deriving Lean.ToJson, Inhabited, Repr
+
+structure VerificationReport where
+  reports : Array TargetReport := #[]
+  kernel : KernelReport := {}
+  nanoda : KernelReport := {}
+  deriving Lean.ToJson, Inhabited, Repr
+
+end Comparator

Main.lean

@@ -5,6 +5,7 @@ Authors: Henrik Böving
 -/
 import Lean
 import Comparator
+import Comparator.Json
 import Lean4Checker.Replay
 import Export.Parse
 
@@ -23,6 +24,7 @@ structure Context where
   whichLandrun : String
   whichLean4Export : String
   whichNanoda : String
+  jsonOutputPath : Option String
 
 abbrev M := ReaderT Context IO
 
@@ -241,18 +243,63 @@ def stringStream (s : String) : BaseIO IO.FS.Stream := do
   }
   return IO.FS.Stream.ofBuffer ref
 
+def writeReport (report : VerificationReport) : M Unit := do
+  if let some p := (← read).jsonOutputPath then
+    IO.FS.writeFile p (Lean.Json.compress <| Lean.toJson report)
+
+def verifyOneTarget (challenge solution : Export.ExportedEnv) (target : Lean.Name)
+    (targetKind : String) : M TargetReport := do
+  let legalAxioms ← getLegalAxioms
+  let defNames ← getDefinitionNames
+  let primitives ← primitiveTargets
+  let (thmTargets, defTargets) :=
+    if targetKind == "theorem" then (#[target], defNames) else (#[], #[target])
+
+  let (failureCategory, failureMessage) :=
+    match Comparator.compareAt challenge solution thmTargets defTargets primitives with
+    | .error (failCat, errorMsg) => (some failCat, some errorMsg)
+    | .ok _ =>
+      match Comparator.checkAxioms solution thmTargets defTargets legalAxioms with
+      | .error errorMsg => (some CheckFailure.axioms, some errorMsg)
+      | .ok () => (none, none)
+
+  return { targetName := target, targetKind, failureCategory, failureMessage }
+
 def verifyMatch (challengeExport : String) (solutionExport : String) :
     M Unit := do
   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 allTargets := (← getTheoremNames).map (·, "theorem") ++ (← getDefinitionNames).map (·, "definition")
+  let reports ← allTargets.mapM fun (n, k) => verifyOneTarget challenge solution n k
+  let mut result : VerificationReport := { reports }
+  writeReport result
+
+  let fails := reports.filter (·.failureCategory.isSome)
+  if !fails.isEmpty then
+    let msg := fails.foldl (init := "Some targets failed:\n") fun acc o =>
+      acc ++ s!"- {o.targetName}: {o.failureMessage.get!}\n"
+    throw <| IO.userError msg
+
+  let mut errs := #[]
   if ← getNanodaEnabled then
-    runNanoda solutionExport
-  runKernel solution
+    try
+      runNanoda solutionExport
+      result := { result with nanoda := { accepted := some true } }
+    catch e =>
+      result := { result with nanoda := { accepted := some false, failureMessage := some (toString e) } }
+      errs := errs.push e
+
+  try
+    runKernel (← Export.parseStream (← stringStream solutionExport))
+    result := { result with kernel := { accepted := some true } }
+  catch e =>
+    result := { result with kernel := { accepted := some false, failureMessage := some (toString e) } }
+    errs := errs.push e
+
+  writeReport result
+  if !errs.isEmpty then
+    throw errs[0]!
 
 def compareIt : M Unit := do
   let exportTargets := (← builtinTargets) ++ (← getTheoremNames) ++ (← getLegalAxioms)
@@ -277,6 +324,7 @@ structure Config where
   definition_names : Option (Array String) := none
   permitted_axioms : Array String
   enable_nanoda : Bool
+  json_output_path : Option String := none
   deriving Lean.FromJson, Lean.ToJson, Repr
 
 def M.run (x : M α) (cfg : Config) : IO α := do
@@ -298,7 +346,8 @@ def M.run (x : M α) (cfg : Config) : IO α := do
     enableNanoda := cfg.enable_nanoda,
     whichLean4Export,
     whichLandrun,
-    whichNanoda
+    whichNanoda,
+    jsonOutputPath := cfg.json_output_path
   }
 
 end Comparator

README.md

@@ -18,6 +18,7 @@ Comparator is configured through a JSON file:
     "challenge_module": "Challenge",
     "solution_module": "Solution",
     "theorem_names": ["todo1"],
+    "json_output_path": "verification-report.json",
     "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
     "enable_nanoda": false
 }
@@ -26,6 +27,10 @@ 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.
 
+The optional `json_output_path` setting writes a machine-readable outcome for each configured theorem
+or definition before comparator returns a verification failure. Each outcome records the target kind,
+accepted declaration name, failure category, and transitive axioms.
+
 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_json_output : Option Lean.Json := none
   deriving FromJson, ToJson
 
 inductive TestResult
@@ -103,6 +104,17 @@ def runTestProject (projectPath : FilePath) (projectName : String) (testsDir : F
 
     let exitCode ← runCommandInDir tempDir "lake" #["env", comparatorPath.toString, "config.json"]
 
+    let projectConfig := Lean.Json.parse (← IO.FS.readFile (tempDir / "config.json")) |>.toOption.getD .null
+    if let .ok jsonOut := projectConfig.getObjValAs? String "json_output_path" then
+      let outputJson ← IO.ofExcept <| Lean.Json.parse (← IO.FS.readFile (tempDir / jsonOut))
+      if let some expectedJson := config.expected_json_output then
+        if outputJson != expectedJson then
+          IO.FS.removeDirAll tempDir
+          return .error projectName s!"JSON mismatch.\nExpected: {expectedJson}\nGot: {outputJson}"
+      else
+        IO.FS.removeDirAll tempDir
+        return .error projectName s!"Configuration specifies 'json_output_path' but test.json is missing 'expected_json_output'."
+
     IO.FS.removeDirAll tempDir
 
     if exitCode == config.exit_code then

tests/projects/def_hole_type_mismatch/config.json

@@ -3,6 +3,7 @@
     "solution_module": "Solution",
     "theorem_names": ["foo"],
     "definition_names": ["n"],
+    "json_output_path": "verification-report.json",
     "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
     "enable_nanoda": false
 }

tests/projects/def_hole_type_mismatch/test.json

@@ -1,3 +1,11 @@
 {
-        "exit_code": 1
+    "exit_code": 1,
+    "expected_json_output": {
+        "reports": [
+            { "targetName": "foo", "targetKind": "theorem", "failureCategory": "signature", "failureMessage": "Const does not match between challenge and target 'n'" },
+            { "targetName": "n", "targetKind": "definition", "failureCategory": "signature", "failureMessage": "Const does not match between challenge and target 'n'" }
+        ],
+        "nanoda": { "failureMessage": null, "accepted": null },
+        "kernel": { "failureMessage": null, "accepted": null }
+    }
 }

tests/projects/olean_issue/config.json

@@ -2,6 +2,7 @@
     "challenge_module": "Challenge",
     "solution_module": "Solution",
     "theorem_names": ["boom"],
+    "json_output_path": "verification-report.json",
     "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
     "enable_nanoda": false
 }

tests/projects/olean_issue/test.json

@@ -1,3 +1,11 @@
 {
-        "exit_code": 1
+    "exit_code": 1,
+    "expected_json_output": {
+        "reports": [{ "targetName": "boom", "targetKind": "theorem", "failureCategory": null, "failureMessage": null }],
+        "nanoda": { "failureMessage": null, "accepted": null },
+        "kernel": {
+            "failureMessage": "(kernel) application type mismatch\n  @id\n    (@Eq Bool\n      (Decidable.decide (Not (@LE.le Nat instLENat badNat 9223372036854775807))\n        (instDecidableNot (@LE.le Nat instLENat badNat 9223372036854775807) (Nat.decLe badNat 9223372036854775807)))\n      Bool.true)\n    (@Eq.refl Bool Bool.true)\nargument has type\n  @Eq Bool Bool.true Bool.true\nbut function has type\n  @Eq Bool\n      (Decidable.decide (Not (@LE.le Nat instLENat badNat 9223372036854775807))\n        (instDecidableNot (@LE.le Nat instLENat badNat 9223372036854775807) (Nat.decLe badNat 9223372036854775807)))\n      Bool.true →\n    @Eq Bool\n      (Decidable.decide (Not (@LE.le Nat instLENat badNat 9223372036854775807))\n        (instDecidableNot (@LE.le Nat instLENat badNat 9223372036854775807) (Nat.decLe badNat 9223372036854775807)))\n      Bool.true",
+            "accepted": false
+        }
+    }
 }

tests/projects/simple_match/config.json

@@ -2,6 +2,7 @@
     "challenge_module": "Challenge",
     "solution_module": "Solution",
     "theorem_names": ["comm"],
+    "json_output_path": "verification-report.json",
     "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
     "enable_nanoda": false
 }

tests/projects/simple_match/test.json

@@ -1,3 +1,8 @@
 {
-        "exit_code": 0
+    "exit_code": 0,
+    "expected_json_output": {
+        "reports": [{ "targetName": "comm", "targetKind": "theorem", "failureCategory": null, "failureMessage": null }],
+        "nanoda": { "failureMessage": null, "accepted": null },
+        "kernel": { "failureMessage": null, "accepted": true }
+    }
 }