From 128a6cb2551089334b9c853c422ff2c7de137b4e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 22:43:52 +0530 Subject: [PATCH 01/10] verify: Replay a Lean project into one kernel environment, importing the toolchain once. --- clang/lib/Verify/Driver/LeanCertifier.h | 161 +++++++++++++----------- 1 file changed, 86 insertions(+), 75 deletions(-) diff --git a/clang/lib/Verify/Driver/LeanCertifier.h b/clang/lib/Verify/Driver/LeanCertifier.h index dc62393db9..2a1cf1f5b0 100644 --- a/clang/lib/Verify/Driver/LeanCertifier.h +++ b/clang/lib/Verify/Driver/LeanCertifier.h @@ -16,7 +16,7 @@ open Lean /-- The axioms a constant depends on, through the statements and values of the constants it uses, read from the kernel's constants. -/ -def axiomsOf (env : Environment) (root : Name) : Except String NameSet := Id.run do +def axiomsOf (env : Kernel.Environment) (root : Name) : Except String NameSet := Id.run do let mut seen : NameSet := {} let mut axioms : NameSet := {} let mut work := #[root] @@ -56,35 +56,92 @@ unsafe def moduleConstants (module : Name) : constants := constants.insert name info return (parts[0].1.imports, constants) -/-- Replays constants with the kernel into the environment of imports, as -leanchecker does: nothing in them escaped the kernel. -/ -unsafe def replayInto (imports : Array Import) - (constants : Std.HashMap Name ConstantInfo) : IO Unit := do - let (_, s) ← importModulesCore imports |>.run - let env ← finalizeImport s imports {} 0 false false (isModule := true) - discard <| env.toKernelEnv.replay constants +/-- A module of the project, read from its compiled files. -/ +structure ProjectModule where + name : Name + imports : Array Import + constants : Std.HashMap Name ConstantInfo -/-- Replays a module's own constants into the environment of its imports. -/ -unsafe def replayModule (module : Name) : IO Unit := do +/-- The modules of the project some modules import, each after the modules it +imports, and the toolchain's modules they import. -/ +structure Closure where + modules : Array ProjectModule := #[] + toolchain : Array Import := #[] + seen : NameSet := {} + +unsafe def Closure.visit (toolchain : String) (module : Name) : StateT Closure IO Unit := do + if (← get).seen.contains module then return + modify fun c => { c with seen := c.seen.insert module } + if (← findOLean module).toString.startsWith toolchain then + modify fun c => { c with toolchain := c.toolchain.push { module } } + return let (imports, constants) ← moduleConstants module - replayInto imports constants + for i in imports do + Closure.visit toolchain i.module + modify fun c => { c with modules := c.modules.push { name := module, imports, constants } } + +/-- The kernel's environment of the project: the toolchain's modules the +project imports, imported once, then every module of the project replayed +with the kernel, each after the modules it imports, as leanchecker does. A +module the kernel rejects, one that imports it, and one that declares a +constant an earlier module or the toolchain declares otherwise are left out, +each with why; the constant each other module declares is recorded with it. -/ +structure Replayed where + env : Kernel.Environment + rejected : Std.HashMap Name String + owner : Std.HashMap Name Name + +unsafe def replayProject (closure : Closure) : IO Replayed := do + let (_, s) ← importModulesCore closure.toolchain |>.run + let imported ← finalizeImport s closure.toolchain {} 0 false false (isModule := true) + let mut env := imported.toKernelEnv + let mut rejected : Std.HashMap Name String := {} + let mut owner : Std.HashMap Name Name := {} + for m in closure.modules do + if let some i := m.imports.find? (rejected.contains ·.module) then + rejected := rejected.insert m.name rejected[i.module]! + continue + let mut fresh : Std.HashMap Name ConstantInfo := {} + let mut clash : Option String := none + for (name, info) in m.constants do + match env.find? name with + | none => fresh := fresh.insert name info + | some known => + -- Lean derives an equation lemma in each module that unfolds a + -- definition, the same constant every time, and the kernel takes a + -- theorem twice when it states the same. + let same := known.type == info.type && known.levelParams == info.levelParams && + (known.isTheorem || known.value? == info.value?) + unless same do + let other := (owner[name]?).map toString |>.getD "the toolchain" + clash := some s!"{m.name} declares {name}, which {other} declares" + break + if let some why := clash then + rejected := rejected.insert m.name why + continue + try env ← env.replay fresh + catch e => + rejected := rejected.insert m.name s!"the kernel rejects {m.name}: {e}" + continue + for (name, _) in fresh do + owner := owner.insert name m.name + return { env, rejected, owner } /-- Whether the proof of a goal states exactly the goal the generated module defines and depends on no axiom outside the allowed ones. -/ -def checkStatement (env : Environment) (goal module : Name) (allowed : NameSet) : +def checkStatement (project : Replayed) (goal module : Name) (allowed : NameSet) : Option String := Id.run do let generated := `CppVerify.Generated - let moduleOf (c : Name) : Option Name := - (env.getModuleIdxFor? c).bind fun i => env.header.moduleNames[i.toNat]? + let env := project.env let proof := goal.appendAfter "_proof" match env.find? goal with | some (.defnInfo _) => - if moduleOf goal != some generated then + if project.owner[goal]? != some generated then return some s!"{goal} is not the goal {generated} defines" | _ => return some s!"{generated} defines no goal {goal}" match env.find? proof with | some (.thmInfo v) => - if moduleOf proof != some module then + if project.owner[proof]? != some module then return some s!"{proof} is not declared in {module}" if v.type != .const goal [] then return some s!"{proof} proves {v.type}, not {goal}" @@ -100,60 +157,14 @@ def checkStatement (env : Environment) (goal module : Name) (allowed : NameSet) | some _ => return some s!"{proof} is not a theorem" | none => return some s!"{module} declares no {proof}" -/-- A goal is proved when every module of the project its proof imports passes -the kernel (each replayed once in a run), and its proof states exactly the -goal and uses only the allowed axioms. Imported data is never freed: a later -import in the process reads it. -/ -unsafe def checkGoal (goal module : Name) (allowed : NameSet) (toolchain : String) - (replayed : IO.Ref NameSet) : IO (Option String) := do - let env ← importModules #[{ module }] {} - let project ← env.header.moduleNames.filterM fun m => - return !(← findOLean m).toString.startsWith toolchain - let why := checkStatement env goal module allowed - for m in project do - if (← replayed.get).contains m then continue - try replayModule m - catch e => return some s!"the kernel rejects {m}: {e}" - replayed.modify (·.insert m) - return why - -/-- Every goal checked in one environment: each proof module imported once, -and every module of the project replayed together into the environment of the -toolchain's modules they import. A check reads only kernel constants, each -in the module that declares it, so proofs imported together cannot change -each other's checks; but one bad module would stop the replay of all, and a -proof file that declares a goal's name stops the import, so then none is -reported (`none`) and each goal is checked by itself. A proof file of -cppverify_auto imports `Lean`, whose import each goal would repeat. -/ -unsafe def checkTogether (entries : Array (Name × Name)) (allowed : NameSet) - (toolchain : String) : IO (Option (Array (Option String))) := do - let modules := entries.foldl (fun ms (_, m) => if ms.contains m then ms else ms.push m) #[] - let some env ← (try some <$> importModules (modules.map ({ module := · })) {} - catch _ => pure none) | return none - let project ← env.header.moduleNames.filterM fun m => - return !(← findOLean m).toString.startsWith toolchain - let mut imports : Array Import := #[] - let mut constants : Std.HashMap Name ConstantInfo := {} - for m in project do - let (own, declared) ← moduleConstants m - for i in own do - unless project.contains i.module || imports.any (·.module == i.module) do - imports := imports.push i - -- Lean derives an equation lemma in each module that unfolds the - -- definition, the same constant every time. - for (name, info) in declared do - if let some known := constants[name]? then - unless known.type == info.type && known.value? == info.value? do - return none - continue - constants := constants.insert name info - try replayInto imports constants catch _ => return none - return some (entries.map fun (goal, module) => checkStatement env goal module allowed) - /-- Usage: Certify GOALS ALLOWED, where each line of GOALS is a goal and its proof module, separated by a tab, and ALLOWED lists the axioms a proof may use, separated by commas. Prints one line per goal: `ok` or `fail`, the goal, -and why it failed. -/ +and why it failed. A goal is proved when its proof module and the generated +module pass the kernel, with every module of the project they import, and +its proof states exactly the goal and uses only the allowed axioms. The +generated module is replayed first, so that a proof file that declares a +name it declares is the one left out. -/ unsafe def main (args : List String) : IO UInt32 := do let [goals, allowed] := args | throw <| IO.userError "usage: Certify GOALS ALLOWED" let sysroot ← findSysroot @@ -164,16 +175,16 @@ unsafe def main (args : List String) : IO UInt32 := do for line in ← IO.FS.lines goals do let [goal, module] := line.splitOn "\t" | continue entries := entries.push (goal.toName, module.toName) - let report (goal : Name) : Option String → IO Unit + let roots := #[`CppVerify.Generated] ++ entries.map (·.2) + let (_, closure) ← (roots.forM (Closure.visit toolchain)).run {} + let project ← replayProject closure + for (goal, module) in entries do + let why := (project.rejected[module]?).orElse fun _ => + (project.rejected[`CppVerify.Generated]?).orElse fun _ => + checkStatement project goal module allowed + match why with | none => IO.println s!"ok\t{goal}" | some why => IO.println s!"fail\t{goal}\t{why.replace "\n" " "}" - if let some results ← checkTogether entries allowed toolchain then - for (goal, _) in entries, why in results do - report goal why - return 0 - let replayed ← IO.mkRef ({} : NameSet) - for (goal, module) in entries do - report goal (← checkGoal goal module allowed toolchain replayed) return 0 )lean"; From 62cac8d2ffbddfcf2373563d8533ad6174633152 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 22:43:52 +0530 Subject: [PATCH 02/10] test: Add a program whose first goal sorts before the other function's goals. --- .../test/Verify/suite/Inputs/lean_certifier_first.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_certifier_first.cpp diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_first.cpp b/clang/test/Verify/suite/Inputs/lean_certifier_first.cpp new file mode 100644 index 0000000000..29404fc469 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier_first.cpp @@ -0,0 +1,11 @@ +int early() + cppverify::post(cppverify::result == 2) +{ + return 1; +} + +int fine() + cppverify::post(cppverify::result == 1) +{ + return 1; +} From 9d85f6e1c4d8959955ea7081e60b70e24f7d7f85 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 22:43:52 +0530 Subject: [PATCH 03/10] test: Add a proof of the first goal that defines a goal of its own under its name. --- .../first/cppverify_early_103f65_postcondition_646d2761.lean | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_certifier_proofs/first/cppverify_early_103f65_postcondition_646d2761.lean diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/first/cppverify_early_103f65_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/first/cppverify_early_103f65_postcondition_646d2761.lean new file mode 100644 index 0000000000..cc38fc4238 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/first/cppverify_early_103f65_postcondition_646d2761.lean @@ -0,0 +1,5 @@ +/- A goal of the same name of its own, true, in the proof of the goal that + comes first, which imports nothing of the project. -/ +def cppverify_early_103f65_postcondition_646d2761 : Prop := True + +theorem cppverify_early_103f65_postcondition_646d2761_proof : cppverify_early_103f65_postcondition_646d2761 := trivial From fe6fc92ee3e6c24d340be9c29633cc29d05dd1ca Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 22:43:53 +0530 Subject: [PATCH 04/10] test: Expect a proof file that redeclares its goal to be the module left out, also when it comes first. --- clang/test/Verify/suite/lean_certifier.test | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/clang/test/Verify/suite/lean_certifier.test b/clang/test/Verify/suite/lean_certifier.test index b738cacb2d..353324ad67 100644 --- a/clang/test/Verify/suite/lean_certifier.test +++ b/clang/test/Verify/suite/lean_certifier.test @@ -38,6 +38,14 @@ # RUN: cp %S/Inputs/lean_certifier_proofs/shadowed/cppverify_one_* %t/shadowed/CppVerify/Proofs/cppverify_one_99bcee/ # RUN: not %cpp-verify --backend=lean --lean-project=%t/shadowed --lean-certify %S/Inputs/lean_certifier.cpp -- 2>&1 | FileCheck %s --check-prefix=SHADOWED # +# The same in the proof of the goal that comes first, which imports nothing +# of the project: the generated module is replayed first all the same, so the +# proof file is the module left out, and the next function is certified. +# RUN: %cpp-verify --backend=lean --no-lean-auto --lean-project=%t/first %S/Inputs/lean_certifier_first.cpp -- > /dev/null +# RUN: cp %S/Inputs/lean_certifier_proofs/cppverify_fine_* %t/first/CppVerify/Proofs/cppverify_fine_52006a/ +# RUN: cp %S/Inputs/lean_certifier_proofs/first/* %t/first/CppVerify/Proofs/cppverify_early_103f65/ +# RUN: not %cpp-verify --backend=lean --no-lean-auto --lean-project=%t/first --lean-certify %S/Inputs/lean_certifier_first.cpp -- 2>&1 | FileCheck %s --check-prefix=FIRST +# # An axiom behind a lemma. # RUN: cp -r %t/base %t/hidden # RUN: cp %S/Inputs/lean_certifier_proofs/hidden/cppverify_one_* %t/hidden/CppVerify/Proofs/cppverify_one_99bcee/ @@ -59,7 +67,10 @@ # IMPORTED-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: the kernel rejects CppVerify.Lemmas: while replaying declaration 'cheat': (kernel) declaration type mismatch, 'cheat' has type True but it is expected to have type cppverify_one_99bcee_postcondition_646d2761) # SHADOWED: Certified: fine [backend=Lean] -# SHADOWED-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: cppverify_one_99bcee_postcondition_646d2761 is not the goal CppVerify.Generated defines) +# SHADOWED-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: CppVerify.Proofs.cppverify_one_99bcee.cppverify_one_99bcee_postcondition_646d2761 declares cppverify_one_99bcee_postcondition_646d2761, which CppVerify.Generated declares) + +# FIRST: Unresolved: lean obligation: early (Lean certification failed: {{.*}}; the proof of fn_5f5a356561726c7976::postcondition@2:37: CppVerify.Proofs.cppverify_early_103f65.cppverify_early_103f65_postcondition_646d2761 declares cppverify_early_103f65_postcondition_646d2761, which CppVerify.Generated declares) +# FIRST-NEXT: Certified: fine [backend=Lean] # HIDDEN: Certified: fine [backend=Lean] # HIDDEN-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: cppverify_one_99bcee_postcondition_646d2761_proof depends on the axiom escape, which is not one of Lean's foundations) From f716cd7a9aa91317b7039f09765c415d9814c2d5 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 22:43:53 +0530 Subject: [PATCH 05/10] test: Add a wrapper that bounds the peak memory of the processes a command runs. --- clang/test/Verify/suite/Inputs/peak_memory.py | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/peak_memory.py diff --git a/clang/test/Verify/suite/Inputs/peak_memory.py b/clang/test/Verify/suite/Inputs/peak_memory.py new file mode 100644 index 0000000000..9584b83d06 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/peak_memory.py @@ -0,0 +1,19 @@ +#!/usr/bin/env python3 +"""Runs a command, then prints whether the largest process it ran stayed +below a resident memory bound, in MB, and exits with the command's status. + +usage: peak_memory.py MB COMMAND... + +Linux reports ru_maxrss in kilobytes, for every descendant waited for.""" +import resource +import subprocess +import sys + +limit = int(sys.argv[1]) +done = subprocess.run(sys.argv[2:]) +peak = resource.getrusage(resource.RUSAGE_CHILDREN).ru_maxrss // 1024 +if peak < limit: + print("peak memory below {} MB".format(limit)) +else: + print("peak memory {} MB, not below {} MB".format(peak, limit)) +sys.exit(done.returncode) From a9098e0e874dd3d33de6c7fe920ec2d61cfe75c2 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 22:43:54 +0530 Subject: [PATCH 06/10] test: Bound the Lean checker's memory where a proof imports Lean through a rejected module. --- .../Verify/suite/lean_certifier_memory.test | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 clang/test/Verify/suite/lean_certifier_memory.test diff --git a/clang/test/Verify/suite/lean_certifier_memory.test b/clang/test/Verify/suite/lean_certifier_memory.test new file mode 100644 index 0000000000..c892c86670 --- /dev/null +++ b/clang/test/Verify/suite/lean_certifier_memory.test @@ -0,0 +1,20 @@ +# REQUIRES: lean, system-linux +# +# The checker imports the toolchain's modules once and replays the project's +# into one kernel environment, so its memory does not grow with the goals or +# with the imports of their proofs. A proof that imports Lean through a module +# the kernel rejects made it import Lean's environment again for every goal +# and every module it replayed, never freeing one: 13 GB here, now under 4. +# +# RUN: rm -rf %t && mkdir -p %t +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %S/Inputs/lean_certifier.cpp -- > /dev/null +# RUN: cp %S/Inputs/lean_certifier_proofs/cppverify_fine_* %t/p/CppVerify/Proofs/cppverify_fine_52006a/ +# RUN: cp %S/Inputs/lean_certifier_proofs/cppverify_one_* %t/p/CppVerify/Proofs/cppverify_one_99bcee/ +# RUN: cp %S/Inputs/lean_certifier_proofs/imported/Lemmas.lean %t/p/CppVerify/ +# RUN: cp %S/Inputs/lean_certifier_proofs/imported/cppverify_one_* %t/p/CppVerify/Proofs/cppverify_one_99bcee/ +# RUN: cd %t/p && lake build CppVerify.Lemmas +# RUN: not %python %S/Inputs/peak_memory.py 6144 %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %S/Inputs/lean_certifier.cpp -- 2>&1 | FileCheck %s + +# CHECK: Certified: fine [backend=Lean] +# CHECK-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: the kernel rejects CppVerify.Lemmas: while replaying declaration 'cheat' +# CHECK-NEXT: peak memory below 6144 MB From f814f9fa0cc266c53462145cab1f37a9b18b1a2e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 22:43:54 +0530 Subject: [PATCH 07/10] docs: Say that certification imports the toolchain once and rejects a module that redeclares a name. --- .../book/part-ii/ch17-backends-modular-calls.rst | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/website/source/book/part-ii/ch17-backends-modular-calls.rst b/website/source/book/part-ii/ch17-backends-modular-calls.rst index 032f7b26aa..c403e1a17a 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -582,7 +582,11 @@ user's source. For each goal: - the kernel replays every declaration of every module of the project the proof imports, as ``leanchecker`` does, so nothing escaped the kernel; only - the pinned toolchain's own modules are trusted; + the pinned toolchain's own modules are trusted, and they are imported once + for all the goals, however many of their proofs import ``Lean``; +- no module may declare a name that an earlier one declares otherwise, and + ``CppVerify.Generated`` comes first, so a proof file that defines a goal + of its own under the goal's name is rejected; - the proof ``G_proof`` must be a theorem whose type is exactly the goal ``G`` that ``CppVerify.Generated`` defines; - the axioms it depends on, collected from the constants it uses, must be @@ -629,8 +633,11 @@ for the rest, gives: A theorem of the goal added by a command with ``debug.skipKernelTC``, which skips the kernel, is rejected at its replay (``the kernel rejects CppVerify.Lemmas: while replaying declaration 'cheat': (kernel) declaration -type mismatch``), and a user axiom behind a lemma by its name (``depends on -the axiom escape, which is not one of Lean's foundations``). +type mismatch``), a proof file that defines a goal of its own under the +goal's name at its replay too (``...cppverify_one_99bcee_postcondition_646d2761 declares +cppverify_one_99bcee_postcondition_646d2761, which CppVerify.Generated +declares``), and a user axiom behind a lemma by its name (``depends on the +axiom escape, which is not one of Lean's foundations``). Portable obligation archives ---------------------------- From ed50d74e7b47d05139b483242ff9ef08ea8742c8 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 22:43:54 +0530 Subject: [PATCH 08/10] docs: Say in the release notes that the checker replays into one environment. --- website/source/release-notes.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 42ebaaa422..a9443338d7 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -106,8 +106,8 @@ a false postcondition, and so did a theorem of the goal added by a command with ``debug.skipKernelTC`` and checked by no kernel, in the proof file or in a module it imports. Certification now checks the compiled modules with a program that elaborates none of the user's source: the kernel replays every -module of the project a proof imports, the proof's type must be exactly its -goal, and its axioms are collected from the constants it uses. A failing +module of the project a proof imports, into one environment with the +toolchain's modules imported once, the proof's type must be exactly its goal, and its axioms are collected from the constants it uses. A failing proof also no longer fails every function of the project: each function is certified on its own goals (:doc:`book/part-ii/ch17-backends-modular-calls`). From e918963b812bc33eed5a039c75a4f15d314a48e3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 22:43:55 +0530 Subject: [PATCH 09/10] docs: Describe the checker's single kernel environment in the design. --- docs/DESIGN.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 2e47c14254..bb4518e207 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1956,10 +1956,12 @@ holds against a proof author in bad faith. It compiles the user module and each proof file on its own with `sorry` as an error, then runs a checker (`LeanCertifier.h`) on the compiled modules, which elaborates none of the user's source, so no macro, notation, or command of theirs changes what it -checks: the kernel replays every module of the project a proof imports (only -the pinned toolchain's own modules are trusted), as `leanchecker` does, so no -declaration escaped the kernel; the proof's type is exactly the constant of its -goal, which `CppVerify.Generated` defines; and the axioms it depends on, +checks: the kernel replays every module of the project a proof imports into +one environment, after the toolchain's modules, imported once (only those are +trusted), as `leanchecker` does, so no declaration escaped the kernel, and a +module that declares a name an earlier one declares otherwise is rejected, +the generated module being replayed first; the proof's type is exactly the +constant of its goal, which `CppVerify.Generated` defines; and the axioms it depends on, collected from the constants it uses, are among `propext`, `Quot.sound`, and `Classical.choice`. A function is `Certified` when every one of its goals passes, and a failing goal leaves only its own function `Unresolved`, with the From c55de5b2af87925a85824c3bcd328954ed90729d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 22:43:55 +0530 Subject: [PATCH 10/10] docs: Describe the checker's single kernel environment and its memory in the architecture. --- docs/ARCHITECTURE.md | 45 ++++++++++++++++++++++++++------------------ 1 file changed, 27 insertions(+), 18 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index e2ed48978b..3dda2cbd89 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1717,23 +1717,30 @@ uses when the source around it changes. `LeanCertifier.h`, written into the project as `.cppverify/Certify.lean`, with `lake env lean --run` over the goals that built. The checker elaborates none of the user's source, so their macros and commands cannot - change what it checks. It first checks every goal in one environment: all - proof modules imported at once, and the constants of every module of the - project replayed together through the kernel into the environment of the - toolchain modules they import (a constant two modules declare, as an - equation lemma derived in each, must be the same). A check reads only - kernel constants, so proofs imported together cannot change each other's - checks; an automatic proof imports `Lean`, whose import each goal would - repeat (33 goals took 161 s, now 8 s). If that import or replay fails, as a - proof file that declares a goal's name or a module the kernel rejects - makes it, each goal is checked on its own: it imports the proof module - (never freeing imported data, which a later import in the process reads), - and every module of the import closure whose `.olean` lies outside the - toolchain is replayed (as `leanchecker`'s `replayFromImports`), each once - in a run. Either way it checks that `G_proof` is a theorem of type exactly - `.const G []` with `G` a definition of `CppVerify.Generated`, collects its - axioms by walking the kernel constants it uses, and prints `ok` or `fail` - with the reason per goal. Each Lean result + change what it checks. It reads, from their compiled files, the generated + module, every proof module, and every module of the project they import + (its `.olean` lies outside the toolchain), imports the toolchain modules + among their imports once, and replays the project's modules through the + kernel into that one environment, each after the modules it imports and + the generated module first, as `leanchecker` does. A module the kernel + rejects, a module that imports one, and a module that declares a constant + an earlier module or the toolchain declares otherwise are left out, each + with why; a constant two modules declare alike (an equation lemma Lean + derives in each, a theorem stated the same, which the kernel's replay + takes twice) is the same. So a proof file that declares a goal's name is + the one left out (`... declares G, which CppVerify.Generated declares`), + and a bad module fails only the goals whose proofs import it. Every check + reads the kernel's constants and the module that declared each, so proofs + cannot change each other's checks: a goal passes when its proof module and + the generated module were replayed, `G_proof` is a theorem of type exactly + `.const G []` with `G` a definition of `CppVerify.Generated`, and the + axioms its kernel constants reach are allowed; it prints `ok` or `fail` + with the reason per goal. One import matters because an automatic proof + imports `Lean`: a check per goal took 161 s for 33 goals (now 8 s), and the + first 0.2 checker, which fell back to it when one module failed, imported + each proof module and the imports of each module it replayed again, never + freeing imported data, which took 13 GB for one proof through a rejected + module (now 3.6 GB, `lean_certifier_memory.test`) and stopped CI runners. Each Lean result records its goals (`VerifyResult::LeanGoals`), and a function is `Certified` only when all of them pass; a failure names the obligation. Before 0.2 certification parsed what `Check.lean` printed, which imports @@ -1743,7 +1750,9 @@ uses when the source around it changes. `lean_certifier.test` checks each of those attacks, a proof file that defines a goal of the same name of its own (the type check alone would take it), a proof that does not build, and an axiom behind a lemma, with a function whose -proofs are sound certified beside each. `lean_readable.cpp` checks the readable form of each kind of assumption, +proofs are sound certified beside each; `lean_certifier_memory.test` bounds +the checker's memory where a proof imports `Lean` through a module the kernel +rejects. `lean_readable.cpp` checks the readable form of each kind of assumption, the bridge, the stubs (every one builds), a proof by hypothesis names that certifies, and a readable form that says less than its goal, which fails at its bridge. `lean_automation.test` checks what an export writes (an automatic