From 16d4a741465c65a6daefa5233355cb973f3c2088 Mon Sep 17 00:00:00 2001 From: Jiayi Fan <110795593+fushanbobfan@users.noreply.github.com> Date: Sun, 4 Oct 2026 19:34:39 -0700 Subject: [PATCH] fix: replay kernel primitives before the rest of the solution The kernel unfolds a string literal to String.ofList [Char.ofNat ..] without any declaration mentioning those constants, so replay could add a declaration that reduces a literal before Char.ofNat or String.ofList were in the environment. Replay the dependency closure of the primitive targets first, then the remaining constants. Fixes #93 --- Comparator/Util.lean | 15 +++++++++++++++ Main.lean | 14 +++++++++++--- .../projects/string_literal_decide/Challenge.lean | 2 ++ .../projects/string_literal_decide/Solution.lean | 2 ++ tests/projects/string_literal_decide/config.json | 7 +++++++ tests/projects/string_literal_decide/test.json | 3 +++ .../projects/string_literal_match/Challenge.lean | 7 +++++++ tests/projects/string_literal_match/Solution.lean | 6 ++++++ tests/projects/string_literal_match/config.json | 7 +++++++ tests/projects/string_literal_match/test.json | 3 +++ 10 files changed, 63 insertions(+), 3 deletions(-) create mode 100644 tests/projects/string_literal_decide/Challenge.lean create mode 100644 tests/projects/string_literal_decide/Solution.lean create mode 100644 tests/projects/string_literal_decide/config.json create mode 100644 tests/projects/string_literal_decide/test.json create mode 100644 tests/projects/string_literal_match/Challenge.lean create mode 100644 tests/projects/string_literal_match/Solution.lean create mode 100644 tests/projects/string_literal_match/config.json create mode 100644 tests/projects/string_literal_match/test.json diff --git a/Comparator/Util.lean b/Comparator/Util.lean index 131a070..be5f7f8 100644 --- a/Comparator/Util.lean +++ b/Comparator/Util.lean @@ -25,4 +25,19 @@ def runForUsedConsts [Monad m] (info : Lean.ConstantInfo) (f : Lean.Name → m U f rule.ctor rule.rhs.getUsedConstants.forM f +/-- +The names in `constMap` that `roots` depend on, transitively and including `roots` themselves. +-/ +partial def dependencyClosure (constMap : Std.HashMap Lean.Name Lean.ConstantInfo) + (roots : Array Lean.Name) : Lean.NameSet := + (roots.forM visit).run {} |>.snd +where + visit (n : Lean.Name) : StateM Lean.NameSet Unit := do + if (← get).contains n then return + let some info := constMap[n]? | return + modify (·.insert n) + runForUsedConsts info visit + -- The kernel needs `Eq` to add `Quot`, without `Quot` mentioning it. + if info matches .quotInfo .. then visit ``Eq + end Comparator diff --git a/Main.lean b/Main.lean index 8560511..e3f1cb3 100644 --- a/Main.lean +++ b/Main.lean @@ -209,7 +209,8 @@ where -- TODO: get rid of this heuristic kernelName.contains "noda" -def runBuiltinKernel (solution : Export.ExportedEnv) : M (Option String) := do +def runBuiltinKernel (solution : Export.ExportedEnv) (primitives : Array Lean.Name) : + M (Option String) := do IO.println "Running Lean default kernel on solution." let env ← Lean.mkEmptyEnvironment let mut kernelEnv := env.toKernelEnv @@ -218,8 +219,15 @@ def runBuiltinKernel (solution : Export.ExportedEnv) : M (Option String) := do -- multiple times leads to errors. let quotTargets := [`Quot.mk, `Quot.lift, `Quot.ind] let kernelConstMap := quotTargets.foldl (init := origConstMap) (·.erase ·) + -- The kernel can use primitives that no declaration mentions, e.g. it unfolds a string literal + -- to `String.ofList [Char.ofNat ..]`. `replay` only orders by mentioned constants, so add the + -- primitives and their dependencies first. + let primitiveClosure := dependencyClosure kernelConstMap primitives + let primitiveConstMap := kernelConstMap.filter fun n _ => primitiveClosure.contains n + let restConstMap := kernelConstMap.filter fun n _ => !primitiveClosure.contains n try - kernelEnv ← kernelEnv.replay kernelConstMap + kernelEnv ← kernelEnv.replay primitiveConstMap + kernelEnv ← kernelEnv.replay restConstMap IO.println "Lean default kernel accepts the solution" catch e => IO.println "Lean default kernel rejects the solution" @@ -297,7 +305,7 @@ def verifyMatch (challengeExport : String) (solutionExport : String) : let mut result := none for (kernelName, kernelCommand) in ← getExternalKernels do result := result <|> (← runExternalKernel kernelName kernelCommand solutionExport) - result := result <|> (← runBuiltinKernel solution) + result := result <|> (← runBuiltinKernel solution (← primitiveTargets)) if let some error := result then throw <| IO.userError error diff --git a/tests/projects/string_literal_decide/Challenge.lean b/tests/projects/string_literal_decide/Challenge.lean new file mode 100644 index 0000000..c7e45b8 --- /dev/null +++ b/tests/projects/string_literal_decide/Challenge.lean @@ -0,0 +1,2 @@ +theorem str_ne : ("live" = "dead") = False := by + sorry diff --git a/tests/projects/string_literal_decide/Solution.lean b/tests/projects/string_literal_decide/Solution.lean new file mode 100644 index 0000000..923172d --- /dev/null +++ b/tests/projects/string_literal_decide/Solution.lean @@ -0,0 +1,2 @@ +theorem str_ne : ("live" = "dead") = False := by + decide diff --git a/tests/projects/string_literal_decide/config.json b/tests/projects/string_literal_decide/config.json new file mode 100644 index 0000000..2d49b23 --- /dev/null +++ b/tests/projects/string_literal_decide/config.json @@ -0,0 +1,7 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["str_ne"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false +} diff --git a/tests/projects/string_literal_decide/test.json b/tests/projects/string_literal_decide/test.json new file mode 100644 index 0000000..5d4bf27 --- /dev/null +++ b/tests/projects/string_literal_decide/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 0 +} diff --git a/tests/projects/string_literal_match/Challenge.lean b/tests/projects/string_literal_match/Challenge.lean new file mode 100644 index 0000000..211eb6a --- /dev/null +++ b/tests/projects/string_literal_match/Challenge.lean @@ -0,0 +1,7 @@ +def strTag (s : String) : Nat := + match s with + | "live" => 1 + | _ => 0 + +theorem strTag_live : strTag "live" = 1 := by + sorry diff --git a/tests/projects/string_literal_match/Solution.lean b/tests/projects/string_literal_match/Solution.lean new file mode 100644 index 0000000..3137882 --- /dev/null +++ b/tests/projects/string_literal_match/Solution.lean @@ -0,0 +1,6 @@ +def strTag (s : String) : Nat := + match s with + | "live" => 1 + | _ => 0 + +theorem strTag_live : strTag "live" = 1 := rfl diff --git a/tests/projects/string_literal_match/config.json b/tests/projects/string_literal_match/config.json new file mode 100644 index 0000000..daa06c4 --- /dev/null +++ b/tests/projects/string_literal_match/config.json @@ -0,0 +1,7 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["strTag_live"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false +} diff --git a/tests/projects/string_literal_match/test.json b/tests/projects/string_literal_match/test.json new file mode 100644 index 0000000..5d4bf27 --- /dev/null +++ b/tests/projects/string_literal_match/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 0 +}