From 128a6cb2551089334b9c853c422ff2c7de137b4e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 22:43:52 +0530 Subject: [PATCH 01/80] 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/80] 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/80] 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/80] 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/80] 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/80] 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/80] 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/80] 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/80] 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/80] 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 From 51a9a6a503ffa0eeac5c1115ae59ad7833331d40 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:02 +0530 Subject: [PATCH 11/80] verify: Declare a Lean project's generated modules and the prelude's emitter. --- clang/lib/Verify/Backend/LeanBackend.h | 28 +++++++++++++++++++++++--- 1 file changed, 25 insertions(+), 3 deletions(-) diff --git a/clang/lib/Verify/Backend/LeanBackend.h b/clang/lib/Verify/Backend/LeanBackend.h index 7145e8596c..92adb95a55 100644 --- a/clang/lib/Verify/Backend/LeanBackend.h +++ b/clang/lib/Verify/Backend/LeanBackend.h @@ -4,8 +4,10 @@ #include "VerifyBackend.h" #include "llvm/Support/raw_ostream.h" +#include #include #include +#include #include namespace clang { @@ -38,21 +40,37 @@ struct LeanProjectGoal { /// The group of a module's goals in a project: its function's directory. std::string leanProjectGroup(const ObligationModule &Module); +/// The generated modules of a Lean project: the declarations of the specs +/// its goals apply, which every goal module imports, and each group's spec +/// definitions and goals. +struct LeanProjectModules { + std::string Specs; + std::map Goals; + /// The groups in the order their functions were exported: the source's. + std::vector Order; +}; + +/// The definitions every exported goal is stated with. +void emitLeanPrelude(llvm::raw_ostream &OS, bool Project); + /// Selection names the internal IDs to export; a project goal is named by /// its function and semantic hash, so it keeps its name whatever else is /// exported, and a scratch-pad goal keeps the positional name it has when /// every obligation is exported. A project records every goal of the module, -/// the ones left out as not exported. +/// the ones left out as not exported. Declarations, when given, receives +/// the declarations of the specs, each once. VerifyResult exportLeanScratchPad(const ObligationModule &Module, llvm::raw_ostream &OS, bool EmitPreamble, std::set &EmittedFunctions, std::set &EmittedTheorems, unsigned ModuleIndex, std::vector *ProjectGoals, - const std::set *Selection = nullptr); + const std::set *Selection = nullptr, + llvm::raw_ostream *Declarations = nullptr); class LeanVerifyBackend : public VerifyBackend { - llvm::raw_ostream *Out; + llvm::raw_ostream *Out = nullptr; + LeanProjectModules *Modules = nullptr; bool PreambleEmitted = false; std::set EmittedFunctions; std::set EmittedTheorems; @@ -64,6 +82,10 @@ class LeanVerifyBackend : public VerifyBackend { LeanVerifyBackend(llvm::raw_ostream *OS, std::vector *ProjectGoals) : Out(OS), ProjectGoals(ProjectGoals) {} + /// A project's export, into its modules. + LeanVerifyBackend(LeanProjectModules *Modules, + std::vector *ProjectGoals) + : Modules(Modules), ProjectGoals(ProjectGoals) {} llvm::StringRef getName() const override { return "lean"; } BackendCapabilities getCapabilities() const override { // Collections have no Lean semantics yet. From 34ef6d00c0649df59e9562095afc5597058824ab Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:02 +0530 Subject: [PATCH 12/80] verify: Emit a project's spec declarations apart from its goals, and the prelude on its own. --- clang/lib/Verify/Backend/LeanBackend.cpp | 102 ++++++++++++----------- 1 file changed, 55 insertions(+), 47 deletions(-) diff --git a/clang/lib/Verify/Backend/LeanBackend.cpp b/clang/lib/Verify/Backend/LeanBackend.cpp index 98eda10f5b..d1b7d0b6e6 100644 --- a/clang/lib/Verify/Backend/LeanBackend.cpp +++ b/clang/lib/Verify/Backend/LeanBackend.cpp @@ -1087,12 +1087,63 @@ static void emitLeanFunctionBodies(const ObligationModule &Module, } } +// The definitions every exported goal is stated with: the heap model, the +// machine comparisons, and C++ division; a project's goals also have the +// lemmas their readable forms' bridges use. +void verify::emitLeanPrelude(llvm::raw_ostream &OS, bool Project) { + OS << "noncomputable section\n\n"; + OS << "set_option maxRecDepth 100000\n"; + OS << "set_option maxHeartbeats 0\n\n"; + OS << "local instance cppVerifyPropDecidable (p : Prop) : Decidable p :=\n"; + OS << " Classical.propDecidable p\n\n"; + OS << "abbrev CppHeap := Int -> Int\n\n"; + OS << "def heapSelectInt (h : CppHeap) (p : Int) : Int := h p\n"; + OS << "abbrev heapSelectBool (h : CppHeap) (p : Int) : Prop := h p ≠ 0\n"; + OS << "def heapSelectBv (w : Nat) (h : CppHeap) (p : Int) : BitVec w :=\n"; + OS << " BitVec.ofInt w (h p)\n\n"; + OS << "def heapStoreInt (h : CppHeap) (p v : Int) (h' : CppHeap) : " + "Prop :=\n"; + OS << " h' = fun q => if q = p then v else h q\n"; + OS << "def heapStoreBool (h : CppHeap) (p : Int) (v : Prop)\n"; + OS << " (h' : CppHeap) : Prop :=\n"; + OS << " h' = fun q => if q = p then\n"; + OS << " @ite Int v (Classical.propDecidable v) 1 0 else h q\n"; + OS << "def heapStoreBv {w : Nat} (h : CppHeap) (p : Int) (v : BitVec w)\n"; + OS << " (h' : CppHeap) : Prop :=\n"; + OS << " h' = fun q => if q = p then Int.ofNat v.toNat else h q\n\n"; + OS << "opaque validPtr : Int -> Prop\n\n"; + // Reducible, so instance search sees the Bool comparison and decides it. + OS << "abbrev cppBvUlt {w : Nat} (x y : BitVec w) : Prop := x.ult y = " + "true\n"; + OS << "abbrev cppBvUle {w : Nat} (x y : BitVec w) : Prop := x.ule y = " + "true\n"; + OS << "abbrev cppBvSlt {w : Nat} (x y : BitVec w) : Prop := x.slt y = " + "true\n"; + OS << "abbrev cppBvSle {w : Nat} (x y : BitVec w) : Prop := x.sle y = " + "true\n\n"; + OS << "def cppIntDiv (x y : Int) : Int :=\n"; + OS << " if y = 0 then 0 else\n"; + OS << " let q := (if x < 0 then -x else x) / " + "(if y < 0 then -y else y)\n"; + OS << " if (x < 0) ≠ (y < 0) then -q else q\n"; + OS << "def cppIntRem (x y : Int) : Int :=\n"; + OS << " if y = 0 then x else x - cppIntDiv x y * y\n\n"; + if (Project) { + // What the bridges from readable goals use. + OS << "theorem cppverify_imp_or {a b : Prop} (h : a → b) : ¬a ∨ b :=\n"; + OS << " (Classical.em a).elim (fun ha => Or.inr (h ha)) Or.inl\n"; + OS << "theorem cppverify_not_imp_or {a b : Prop} (h : ¬a → b) : a ∨ b " + ":=\n"; + OS << " (Classical.em a).elim Or.inl (fun ha => Or.inr (h ha))\n\n"; + } +} + VerifyResult verify::exportLeanScratchPad( const ObligationModule &Module, llvm::raw_ostream &OS, bool EmitPreamble, std::set &EmittedFunctions, std::set &EmittedTheorems, unsigned ModuleIndex, std::vector *ProjectGoals, - const std::set *Selection) { + const std::set *Selection, llvm::raw_ostream *Declarations) { VerifyResult Result; if (!Module.CorrectnessGoal || !Module.CounterexampleQuery) { Result.Status = VerifyStatus::Unresolved; @@ -1130,54 +1181,11 @@ VerifyResult verify::exportLeanScratchPad( OS << " This file exports canonical obligations but does not certify " "them. -/\n\n"; } - OS << "noncomputable section\n\n"; - OS << "set_option maxRecDepth 100000\n"; - OS << "set_option maxHeartbeats 0\n\n"; - OS << "local instance cppVerifyPropDecidable (p : Prop) : Decidable p :=\n"; - OS << " Classical.propDecidable p\n\n"; - OS << "abbrev CppHeap := Int -> Int\n\n"; - OS << "def heapSelectInt (h : CppHeap) (p : Int) : Int := h p\n"; - OS << "abbrev heapSelectBool (h : CppHeap) (p : Int) : Prop := h p ≠ 0\n"; - OS << "def heapSelectBv (w : Nat) (h : CppHeap) (p : Int) : BitVec w :=\n"; - OS << " BitVec.ofInt w (h p)\n\n"; - OS << "def heapStoreInt (h : CppHeap) (p v : Int) (h' : CppHeap) : " - "Prop :=\n"; - OS << " h' = fun q => if q = p then v else h q\n"; - OS << "def heapStoreBool (h : CppHeap) (p : Int) (v : Prop)\n"; - OS << " (h' : CppHeap) : Prop :=\n"; - OS << " h' = fun q => if q = p then\n"; - OS << " @ite Int v (Classical.propDecidable v) 1 0 else h q\n"; - OS << "def heapStoreBv {w : Nat} (h : CppHeap) (p : Int) (v : BitVec w)\n"; - OS << " (h' : CppHeap) : Prop :=\n"; - OS << " h' = fun q => if q = p then Int.ofNat v.toNat else h q\n\n"; - OS << "opaque validPtr : Int -> Prop\n\n"; - // Reducible, so instance search sees the Bool comparison and decides it. - OS << "abbrev cppBvUlt {w : Nat} (x y : BitVec w) : Prop := x.ult y = " - "true\n"; - OS << "abbrev cppBvUle {w : Nat} (x y : BitVec w) : Prop := x.ule y = " - "true\n"; - OS << "abbrev cppBvSlt {w : Nat} (x y : BitVec w) : Prop := x.slt y = " - "true\n"; - OS << "abbrev cppBvSle {w : Nat} (x y : BitVec w) : Prop := x.sle y = " - "true\n\n"; - OS << "def cppIntDiv (x y : Int) : Int :=\n"; - OS << " if y = 0 then 0 else\n"; - OS << " let q := (if x < 0 then -x else x) / " - "(if y < 0 then -y else y)\n"; - OS << " if (x < 0) ≠ (y < 0) then -q else q\n"; - OS << "def cppIntRem (x y : Int) : Int :=\n"; - OS << " if y = 0 then x else x - cppIntDiv x y * y\n\n"; - if (ProjectGoals) { - // What the bridges from readable goals use. - OS << "theorem cppverify_imp_or {a b : Prop} (h : a → b) : ¬a ∨ b :=\n"; - OS << " (Classical.em a).elim (fun ha => Or.inr (h ha)) Or.inl\n"; - OS << "theorem cppverify_not_imp_or {a b : Prop} (h : ¬a → b) : a ∨ b " - ":=\n"; - OS << " (Classical.em a).elim Or.inl (fun ha => Or.inr (h ha))\n\n"; - } + emitLeanPrelude(OS, ProjectGoals != nullptr); } - emitLeanFunctionDeclarations(Module, OS, EmittedFunctions); + emitLeanFunctionDeclarations(Module, Declarations ? *Declarations : OS, + EmittedFunctions); emitLeanFunctionBodies(Module, OS); OS << "/- function: "; printLeanCommentText(Module.FunctionName, OS); From cdcaec52d11e528e430beed76129c7f750dfd5e9 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:03 +0530 Subject: [PATCH 13/80] verify: Let the Lean backend write the modules of a project. --- clang/lib/Verify/Backend/VerifyBackend.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/clang/lib/Verify/Backend/VerifyBackend.h b/clang/lib/Verify/Backend/VerifyBackend.h index 6159936740..6e3a71e715 100644 --- a/clang/lib/Verify/Backend/VerifyBackend.h +++ b/clang/lib/Verify/Backend/VerifyBackend.h @@ -307,12 +307,14 @@ inline unsigned moduleTimeoutMs(const ObligationModule &Module, } struct LeanProjectGoal; +struct LeanProjectModules; std::unique_ptr createVerifyBackend(BackendKind K, llvm::raw_ostream *LeanOut = nullptr, unsigned BMCUnroll = 10, const BackendExecutionOptions &Execution = {}, - std::vector *LeanProjectGoals = nullptr); + std::vector *LeanProjectGoals = nullptr, + LeanProjectModules *LeanModules = nullptr); VerifyResult lowerObligationModule(const ObligationModule &Module, From 505cf155582c2f9cdb46ab84c4b819888f4f1ed9 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:03 +0530 Subject: [PATCH 14/80] verify: Write each function's Lean goals to its module and the specs they apply to Specs. --- clang/lib/Verify/Backend/VerifyBackend.cpp | 30 +++++++++++++++++----- 1 file changed, 24 insertions(+), 6 deletions(-) diff --git a/clang/lib/Verify/Backend/VerifyBackend.cpp b/clang/lib/Verify/Backend/VerifyBackend.cpp index 134495fe9a..1c69d41bbc 100644 --- a/clang/lib/Verify/Backend/VerifyBackend.cpp +++ b/clang/lib/Verify/Backend/VerifyBackend.cpp @@ -15,17 +15,32 @@ using namespace verify; VerifyResult LeanVerifyBackend::verifyModule(const ObligationModule &Module) { VerifyResult R; - if (!Out) { + if (!Out && !Modules) { R.Status = VerifyStatus::Unresolved; R.Reason = VerifyReason::LeanExportFailure; R.Message = "no lean output stream"; return R; } const size_t Before = ProjectGoals ? ProjectGoals->size() : 0; - VerifyResult Result = exportLeanScratchPad( - Module, *Out, !PreambleEmitted, EmittedFunctions, EmittedTheorems, - ++ModuleIndex, ProjectGoals, Selection ? &*Selection : nullptr); - PreambleEmitted = true; + VerifyResult Result; + if (Modules) { + // A project's goals go to their function's module, and the specs they + // apply are declared once, in the module every goal module imports. + const std::string Group = leanProjectGroup(Module); + if (!Modules->Goals.count(Group)) + Modules->Order.push_back(Group); + llvm::raw_string_ostream Goals(Modules->Goals[Group]); + llvm::raw_string_ostream Specs(Modules->Specs); + Result = exportLeanScratchPad(Module, Goals, /*EmitPreamble=*/false, + EmittedFunctions, EmittedTheorems, + ++ModuleIndex, ProjectGoals, + Selection ? &*Selection : nullptr, &Specs); + } else { + Result = exportLeanScratchPad( + Module, *Out, !PreambleEmitted, EmittedFunctions, EmittedTheorems, + ++ModuleIndex, ProjectGoals, Selection ? &*Selection : nullptr); + PreambleEmitted = true; + } if (ProjectGoals) for (size_t I = Before; I < ProjectGoals->size(); ++I) if ((*ProjectGoals)[I].Exported) @@ -754,11 +769,14 @@ std::unique_ptr verify::createVerifyBackend(BackendKind K, llvm::raw_ostream *LeanOut, unsigned BMCUnroll, const BackendExecutionOptions &Execution, - std::vector *LeanProjectGoals) { + std::vector *LeanProjectGoals, + LeanProjectModules *LeanModules) { switch (K) { case BackendKind::Z3: return std::make_unique(Execution, "z3"); case BackendKind::Lean: + if (LeanModules) + return std::make_unique(LeanModules, LeanProjectGoals); return std::make_unique(LeanOut, LeanProjectGoals); case BackendKind::BMC: return std::make_unique(BMCUnroll, Execution); From 86e4a9d83f6bc225e2c9da770f1ca9b9ef5bd095 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:03 +0530 Subject: [PATCH 15/80] verify: Import only the prelude in the module of cppverify_auto. --- clang/lib/Verify/Driver/LeanAutomation.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang/lib/Verify/Driver/LeanAutomation.h b/clang/lib/Verify/Driver/LeanAutomation.h index 0db32bac01..ee97ecc42a 100644 --- a/clang/lib/Verify/Driver/LeanAutomation.h +++ b/clang/lib/Verify/Driver/LeanAutomation.h @@ -25,7 +25,7 @@ inline constexpr llvm::StringLiteral LeanAutomationSource = R"lean(/- Generated by CppVerify: the tactics of its automatic proofs, which proof files may use too. Regeneration replaces this file. -/ import Lean -import CppVerify.Generated +import CppVerify.Prelude register_option cppverify.autoBudget : Nat := { defValue := 50000 From c23e58c36a1f188fc669926726d70f5ee57de591 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:04 +0530 Subject: [PATCH 16/80] verify: Check each goal against its own module, and fail every goal when a User lemma uses sorry. --- clang/lib/Verify/Driver/LeanCertifier.h | 61 +++++++++++++++---------- 1 file changed, 37 insertions(+), 24 deletions(-) diff --git a/clang/lib/Verify/Driver/LeanCertifier.h b/clang/lib/Verify/Driver/LeanCertifier.h index 2a1cf1f5b0..4286533013 100644 --- a/clang/lib/Verify/Driver/LeanCertifier.h +++ b/clang/lib/Verify/Driver/LeanCertifier.h @@ -38,9 +38,10 @@ def axiomsOf (env : Kernel.Environment) (root : Name) : Except String NameSet := | none => return .error s!"{c} is not in the environment" return .ok axioms -/-- A module's imports and its own constants, read from its compiled files. -/ +/-- A module's imports and its own constants, in the order it declares them, +read from its compiled files. -/ unsafe def moduleConstants (module : Name) : - IO (Array Import × Std.HashMap Name ConstantInfo) := do + IO (Array Import × Array Name × Std.HashMap Name ConstantInfo) := do let file ← findOLean module let mut files := #[file] let server := OLeanLevel.server.adjustFileName file @@ -54,12 +55,13 @@ unsafe def moduleConstants (module : Name) : let mut constants := {} for name in parts[parts.size - 1].1.constNames, info in parts[parts.size - 1].1.constants do constants := constants.insert name info - return (parts[0].1.imports, constants) + return (parts[0].1.imports, parts[parts.size - 1].1.constNames, constants) /-- A module of the project, read from its compiled files. -/ structure ProjectModule where name : Name imports : Array Import + declared : Array Name constants : Std.HashMap Name ConstantInfo /-- The modules of the project some modules import, each after the modules it @@ -75,10 +77,10 @@ unsafe def Closure.visit (toolchain : String) (module : Name) : StateT Closure I if (← findOLean module).toString.startsWith toolchain then modify fun c => { c with toolchain := c.toolchain.push { module } } return - let (imports, constants) ← moduleConstants module + let (imports, declared, constants) ← moduleConstants module for i in imports do Closure.visit toolchain i.module - modify fun c => { c with modules := c.modules.push { name := module, imports, constants } } + modify fun c => { c with modules := c.modules.push { name := module, imports, declared, constants } } /-- The kernel's environment of the project: the toolchain's modules the project imports, imported once, then every module of the project replayed @@ -127,11 +129,10 @@ unsafe def replayProject (closure : Closure) : IO Replayed := do owner := owner.insert name m.name return { env, rejected, owner } -/-- Whether the proof of a goal states exactly the goal the generated module +/-- Whether the proof of a goal states exactly the goal its generated module defines and depends on no axiom outside the allowed ones. -/ -def checkStatement (project : Replayed) (goal module : Name) (allowed : NameSet) : - Option String := Id.run do - let generated := `CppVerify.Generated +def checkStatement (project : Replayed) (goal module generated : Name) + (allowed : NameSet) : Option String := Id.run do let env := project.env let proof := goal.appendAfter "_proof" match env.find? goal with @@ -157,31 +158,43 @@ def checkStatement (project : Replayed) (goal module : Name) (allowed : NameSet) | some _ => return some s!"{proof} is not a theorem" | none => return some s!"{module} declares no {proof}" -/-- 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. 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. -/ +/-- The declaration of the user's lemmas that uses `sorry`, if one does: an +admitted lemma fails every goal, as when the module was compiled with `sorry` +an error. -/ +def userSorry (closure : Closure) (project : Replayed) : Option String := Id.run do + let some user := closure.modules.find? (·.name == `CppVerify.User) | return none + for name in user.declared do + if let .ok axioms := axiomsOf project.env name then + if axioms.contains ``sorryAx then + return some s!"{name} of CppVerify.User uses sorry" + return none + +/-- Usage: Certify GOALS ALLOWED, where each line of GOALS is a goal, its +proof module, and the module that defines it, separated by tabs, 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. A goal is proved when its +proof module and its 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 modules are replayed first, so that a +proof file that declares a name one 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 initSearchPath sysroot let toolchain := (sysroot / "lib" / "lean").toString let allowed := (allowed.splitOn ",").foldl (fun s a => s.insert a.toName) ({} : NameSet) - let mut entries : Array (Name × Name) := #[] + let mut entries : Array (Name × Name × Name) := #[] for line in ← IO.FS.lines goals do - let [goal, module] := line.splitOn "\t" | continue - entries := entries.push (goal.toName, module.toName) - let roots := #[`CppVerify.Generated] ++ entries.map (·.2) + let [goal, module, generated] := line.splitOn "\t" | continue + entries := entries.push (goal.toName, module.toName, generated.toName) + let roots := entries.map (·.2.2) ++ entries.map (·.2.1) let (_, closure) ← (roots.forM (Closure.visit toolchain)).run {} let project ← replayProject closure - for (goal, module) in entries do + let user := userSorry closure project + for (goal, module, generated) in entries do let why := (project.rejected[module]?).orElse fun _ => - (project.rejected[`CppVerify.Generated]?).orElse fun _ => - checkStatement project goal module allowed + (project.rejected[generated]?).orElse fun _ => user.orElse fun _ => + checkStatement project goal module generated allowed match why with | none => IO.println s!"ok\t{goal}" | some why => IO.println s!"fail\t{goal}\t{why.replace "\n" " "}" From 2ef7e14bd9b794deda04c182d280bc52747e5fa9 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:04 +0530 Subject: [PATCH 17/80] verify: Give each function's Lean goals a module, and compile a proof again only when what it imports changed. --- clang/lib/Verify/Driver/Verifier.cpp | 281 +++++++++++++++++++++------ 1 file changed, 218 insertions(+), 63 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index f317e60815..8800d39092 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -32,6 +32,7 @@ #include "llvm/ADT/ScopeExit.h" #include "llvm/ADT/SmallString.h" #include "llvm/ADT/SmallVector.h" +#include "llvm/ADT/StringExtras.h" #include "llvm/Support/Error.h" #include "llvm/Support/FileSystem.h" #include "llvm/Support/FormatVariadic.h" @@ -41,6 +42,7 @@ #include "llvm/Support/MemoryBuffer.h" #include "llvm/Support/Path.h" #include "llvm/Support/Program.h" +#include "llvm/Support/SHA256.h" #include "llvm/Support/ThreadPool.h" #include "llvm/Support/Threading.h" #include "llvm/Support/raw_ostream.h" @@ -1255,6 +1257,28 @@ static llvm::Error writeTextFile(llvm::StringRef Path, return llvm::Error::success(); } +// A generated file is rewritten only when it changes, so that a rerun of the +// same source leaves every file as it was. +static llvm::Error writeTextFileIfChanged(llvm::StringRef Path, + llvm::StringRef Contents) { + if (auto Buffer = llvm::MemoryBuffer::getFile(Path, /*IsText=*/true)) + if ((*Buffer)->getBuffer() == Contents) + return llvm::Error::success(); + return writeTextFile(Path, Contents); +} + +static constexpr llvm::StringLiteral LeanGeneratedNote = + "/- Generated by CppVerify. Regeneration replaces this file, never a " + "proof. -/"; + +// What each module of goals starts with: options and the instance attribute +// of the prelude's classical decidability are local to a file. +static constexpr llvm::StringLiteral LeanGoalModulePreamble = + "noncomputable section\n\n" + "set_option maxRecDepth 100000\n" + "set_option maxHeartbeats 0\n\n" + "attribute [local instance] cppVerifyPropDecidable\n\n"; + static llvm::Error writeTextFileIfMissing(llvm::StringRef Path, llvm::StringRef Contents) { if (llvm::sys::fs::exists(Path)) @@ -1314,18 +1338,28 @@ struct LeanProofRecord { std::string Automation; }; -// A proof starts from the goal's readable form, its names introduced. Stubs -// before cppverify_auto did not import it. -static std::string leanProofHead(llvm::StringRef Goal, bool Automation = true) { - return "import CppVerify.User\n" + - std::string(Automation ? "import CppVerify.Auto\n" : "") + - "\ntheorem " + Goal.str() + "_proof : " + Goal.str() + +// The imports a proof file starts with: its function's goals, the user's +// lemmas, and the automation. Before 0.2's modules a proof imported only +// User (which imported every goal), and before cppverify_auto, not Auto. +enum class LeanProofImports { Modules, Automation, User }; + +// A proof starts from the goal's readable form, its names introduced. +static std::string +leanProofHead(llvm::StringRef Goal, llvm::StringRef Group, + LeanProofImports Imports = LeanProofImports::Modules) { + std::string Head; + if (Imports == LeanProofImports::Modules) + Head += "import CppVerify.Goals." + Group.str() + "\n"; + Head += "import CppVerify.User\n"; + if (Imports != LeanProofImports::User) + Head += "import CppVerify.Auto\n"; + return Head + "\ntheorem " + Goal.str() + "_proof : " + Goal.str() + " := by\n apply " + Goal.str() + ".of_readable\n"; } -static std::string leanProof(llvm::StringRef Goal, llvm::StringRef Intros, - llvm::StringRef Last) { - std::string Proof = leanProofHead(Goal); +static std::string leanProof(llvm::StringRef Goal, llvm::StringRef Group, + llvm::StringRef Intros, llvm::StringRef Last) { + std::string Proof = leanProofHead(Goal, Group); if (!Intros.empty()) Proof += " intro " + Intros.str() + "\n"; return Proof + " " + Last.str() + "\n"; @@ -1335,9 +1369,15 @@ static std::string leanProof(llvm::StringRef Goal, llvm::StringRef Intros, // whether cppverify_auto proves it: its last line is a stub's `sorry` or a // step of cppverify_auto. static std::optional leanGeneratedProof(llvm::StringRef Body, - llvm::StringRef Goal) { - if (!Body.consume_front(leanProofHead(Goal)) && - !Body.consume_front(leanProofHead(Goal, /*Automation=*/false))) + llvm::StringRef Goal, + llvm::StringRef Group) { + if (!llvm::any_of( + std::initializer_list{LeanProofImports::Modules, + LeanProofImports::Automation, + LeanProofImports::User}, + [&](LeanProofImports Imports) { + return Body.consume_front(leanProofHead(Goal, Group, Imports)); + })) return std::nullopt; if (Body.consume_front(" intro ")) { const size_t End = Body.find('\n'); @@ -1407,8 +1447,9 @@ static std::optional readLeanProof(llvm::StringRef Path) { return std::nullopt; const size_t End = Text.find("-/\n"); if (End != llvm::StringRef::npos) - if (std::optional Automatic = - leanGeneratedProof(Text.substr(End + 3), Record.Goal)) { + if (std::optional Automatic = leanGeneratedProof( + Text.substr(End + 3), Record.Goal, + llvm::sys::path::filename(llvm::sys::path::parent_path(Path)))) { Record.Pristine = true; Record.Automatic = *Automatic; } @@ -1428,7 +1469,8 @@ static void replaceAllIn(std::string &Text, llvm::StringRef From, static llvm::Error moveLeanProof(llvm::StringRef From, llvm::StringRef To, const LeanProjectGoal &Goal, llvm::StringRef OldGoal, - llvm::StringRef OldBodies) { + llvm::StringRef OldBodies, + llvm::StringRef OldGroup = "") { auto Buffer = llvm::MemoryBuffer::getFile(From); if (!Buffer) return llvm::createStringError( @@ -1449,6 +1491,9 @@ static llvm::Error moveLeanProof(llvm::StringRef From, llvm::StringRef To, } replaceAllIn(Body, OldGoal, Goal.Name); replaceAllIn(Body, OldBodies, Goal.BodyPrefix); + if (!OldGroup.empty()) + replaceAllIn(Body, ("import CppVerify.Goals." + OldGroup + "\n").str(), + "import CppVerify.Goals." + Goal.Group + "\n"); if (std::error_code EC = llvm::sys::fs::create_directories(llvm::sys::path::parent_path(To))) return llvm::createStringError(EC, "cannot create %s", To.str().c_str()); @@ -1623,7 +1668,7 @@ class Verifier { } } - llvm::Expected initializeLeanProject() { + llvm::Error initializeLeanProject() { const std::string &Root = leanProjectRoot(); std::error_code EC = llvm::sys::fs::create_directories( leanProjectPath(Root, {"CppVerify", "Proofs"})); @@ -1672,18 +1717,67 @@ class Verifier { leanProjectPath(Root, {"lakefile.toml"}), Lakefile)) return std::move(Error); + // A project of an earlier release imports CppVerify.Generated here, + // which still imports every goal. constexpr llvm::StringLiteral UserFile = - "import CppVerify.Generated\n\n" + "import CppVerify.Specs\n\n" "/- Add reusable lemmas here. This file is never regenerated. -/\n"; if (llvm::Error Error = writeTextFileIfMissing( leanProjectPath(Root, {"CppVerify", "User.lean"}), UserFile)) - return std::move(Error); - if (llvm::Error Error = - writeTextFile(leanProjectPath(Root, {"CppVerify", "Auto.lean"}), - LeanAutomationSource)) - return std::move(Error); + return Error; + + std::string Prelude = std::string(LeanGeneratedNote) + "\n\n"; + llvm::raw_string_ostream PreludeOS(Prelude); + emitLeanPrelude(PreludeOS, /*Project=*/true); + for (const auto &[File, Contents] : + {std::pair{"Prelude.lean", Prelude}, + {"Auto.lean", LeanAutomationSource}}) + if (llvm::Error Error = writeTextFileIfChanged( + leanProjectPath(Root, {"CppVerify", File}), Contents)) + return Error; + // The root of the library, so that `lake build` builds every proof. + return writeTextFileIfChanged(leanProjectPath(Root, {"CppVerify.lean"}), + "import CppVerify.Check\n"); + } - return leanProjectPath(Root, {"CppVerify", "Generated.lean"}); + // The generated modules of a run: Specs, a goal module for each function + // the run exported, and Generated, which imports them all. Any other goal + // module is removed, so that every module of the project builds: one an + // earlier run wrote may apply a spec Specs no longer declares, as after a + // fallback run whose solver settled the functions that applied it. The + // proofs of a function the run did not export stay as they are. + llvm::Error writeLeanProjectModules(const LeanProjectModules &Modules) { + const std::string &Root = leanProjectRoot(); + const std::string Header = std::string(LeanGeneratedNote) + "\n"; + if (llvm::Error Error = writeTextFileIfChanged( + leanProjectPath(Root, {"CppVerify", "Specs.lean"}), + Header + "import CppVerify.Prelude\n\nnoncomputable section\n\n" + + Modules.Specs)) + return Error; + const std::string GoalsDir = leanProjectPath(Root, {"CppVerify", "Goals"}); + if (std::error_code EC = llvm::sys::fs::create_directories(GoalsDir)) + return llvm::createStringError(EC, "cannot create %s", GoalsDir.c_str()); + std::string Generated = Header + "import CppVerify.Prelude\n" + "import CppVerify.Specs\n"; + for (const std::string &Group : Modules.Order) { + if (llvm::Error Error = writeTextFileIfChanged( + leanProjectPath(GoalsDir, {Group + ".lean"}), + Header + "import CppVerify.Specs\n\n" + + LeanGoalModulePreamble.str() + Modules.Goals.at(Group))) + return Error; + Generated += "import CppVerify.Goals." + Group + "\n"; + } + if (llvm::Error Error = writeTextFileIfChanged( + leanProjectPath(Root, {"CppVerify", "Generated.lean"}), Generated)) + return Error; + + std::error_code EC; + for (llvm::sys::fs::directory_iterator It(GoalsDir, EC), End; + It != End && !EC; It.increment(EC)) + if (llvm::sys::path::extension(It->path()) == ".lean" && + !Modules.Goals.count(llvm::sys::path::stem(It->path()).str())) + llvm::sys::fs::remove(It->path()); + return llvm::Error::success(); } static std::vector @@ -1802,8 +1896,9 @@ class Verifier { (Moving->Path != ProofPath || !Taken.count(ProofPath))) { const bool WasKept = llvm::StringRef(Moving->Path).starts_with(StaleDir); - if (llvm::Error Error = moveLeanProof(Moving->Path, ProofPath, *Goal, - Moving->Goal, Moving->BodyPrefix)) + if (llvm::Error Error = + moveLeanProof(Moving->Path, ProofPath, *Goal, Moving->Goal, + Moving->BodyPrefix, groupOf(*Moving))) return Error; Diags.push_back({VerifyDiagnostic::Warning, "the Lean proof of " + Goal->StableId + @@ -1841,9 +1936,10 @@ class Verifier { llvm::sys::path::parent_path(ProofPath))) return llvm::createStringError(EC, "cannot create %s", ProofPath.c_str()); - if (llvm::Error Error = writeTextFile( - ProofPath, leanProofHeader(*Goal) + - leanProof(Goal->Name, Goal->Intros, "sorry"))) + if (llvm::Error Error = + writeTextFile(ProofPath, leanProofHeader(*Goal) + + leanProof(Goal->Name, Goal->Group, + Goal->Intros, "sorry"))) return Error; Taken.insert(ProofPath); } @@ -1931,8 +2027,8 @@ class Verifier { CheckFile += "example : " + Name + " := " + Name + "_proof\n"; CheckFile += "#print axioms " + Name + "_proof\n"; } - return writeTextFile(leanProjectPath(Root, {"CppVerify", "Check.lean"}), - CheckFile); + return writeTextFileIfChanged( + leanProjectPath(Root, {"CppVerify", "Check.lean"}), CheckFile); } // Certifies each goal's proof: an error fails every goal; otherwise the @@ -2008,6 +2104,58 @@ class Verifier { return Launcher; } + // What a proof is built from: the pinned toolchain, its source, and the + // compiled modules of the project in its import closure, read from the + // import lines of their sources. None when a module of the closure has no + // compiled module. + std::optional leanProofKey(llvm::StringRef ProofSource) { + const std::string &Root = leanProjectRoot(); + auto importsOf = [](llvm::StringRef Source) { + std::vector Imports; + if (auto Buffer = llvm::MemoryBuffer::getFile(Source)) + for (llvm::StringRef Rest = (*Buffer)->getBuffer(); !Rest.empty();) { + auto [Line, Next] = Rest.split('\n'); + Rest = Next; + if (Line.consume_front("import ")) + Imports.push_back(Line.trim().str()); + } + return Imports; + }; + llvm::SHA256 Hasher; + Hasher.update(LeanToolchain); + auto Source = llvm::MemoryBuffer::getFile(ProofSource); + if (!Source) + return std::nullopt; + Hasher.update((*Source)->getBuffer()); + std::map Compiled; + std::vector Work = importsOf(ProofSource); + while (!Work.empty()) { + const std::string Module = Work.back(); + Work.pop_back(); + if (Compiled.count(Module)) + continue; + std::string Relative = Module; + std::replace(Relative.begin(), Relative.end(), '.', '/'); + const std::string ModuleSource = + leanProjectPath(Root, {Relative + ".lean"}); + if (!llvm::sys::fs::exists(ModuleSource)) + continue; + auto Object = llvm::MemoryBuffer::getFile(leanProjectPath( + Root, {".lake", "build", "lib", "lean", Relative + ".olean"})); + if (!Object) + return std::nullopt; + Compiled[Module] = llvm::toHex(llvm::SHA256::hash( + llvm::arrayRefFromStringRef((*Object)->getBuffer()))); + for (std::string &Import : importsOf(ModuleSource)) + Work.push_back(std::move(Import)); + } + for (const auto &[Module, Hash] : Compiled) { + Hasher.update(Module); + Hasher.update(Hash); + } + return llvm::toHex(Hasher.final()); + } + llvm::Expected> certifyLeanProject(const std::vector &ProjectGoals) { if (ProjectGoals.empty()) @@ -2028,15 +2176,6 @@ class Verifier { !Build) return Build.takeError(); - const std::string UserObject = leanProjectPath( - Root, {".lake", "build", "lib", "lean", "CppVerify", "User.olean"}); - if (auto User = - runLake({"env", "lean", "-EhasSorry", "-R", Root, "-o", UserObject, - leanProjectPath(Root, {"CppVerify", "User.lean"})}, - "user"); - !User) - return User.takeError(); - const std::string ProofBuildDir = leanProjectPath( Root, {".lake", "build", "lib", "lean", "CppVerify", "Proofs"}); if (std::error_code EC = llvm::sys::fs::create_directories(ProofBuildDir)) @@ -2053,7 +2192,14 @@ class Verifier { leanProjectPath(ProofBuildDir, {Goal->Group}))) return llvm::createStringError( EC, "cannot create Lean proof build directory"); - // Each proof builds by itself, several at once. + // Each proof builds by itself, several at once, unless nothing it is + // built from changed since it last built: its source and the compiled + // modules of the project it imports (which Lake has just built). Lake + // cannot say this itself: a module whose import failed is not built and + // not named, and its .olean of an earlier build would stay. + const std::string KeyDir = leanProjectPath(Root, {".cppverify", "built"}); + if (std::error_code EC = llvm::sys::fs::create_directories(KeyDir)) + return llvm::createStringError(EC, "cannot create %s", KeyDir.c_str()); std::vector> BuildErrors(Proofs.size()); std::atomic NextProof{0}; auto buildProofs = [&] { @@ -2064,13 +2210,22 @@ class Verifier { leanProjectPath(Root, leanProofComponents(*Goal, File)); const std::string ProofObject = leanProjectPath( leanProjectPath(ProofBuildDir, {Goal->Group}), {Name + ".olean"}); + const std::string KeyFile = leanProjectPath(KeyDir, {Name}); + const std::optional Key = leanProofKey(ProofSource); + if (Key && llvm::sys::fs::exists(ProofObject)) + if (auto Kept = llvm::MemoryBuffer::getFile(KeyFile)) + if ((*Kept)->getBuffer() == *Key) + continue; llvm::sys::fs::remove(ProofObject); + llvm::sys::fs::remove(KeyFile); if (auto Proof = runLake({"env", "lean", "-EhasSorry", "-R", Root, "-o", ProofObject, ProofSource}, Name); !Proof) BuildErrors[I] = llvm::StringRef(llvm::toString(Proof.takeError())).rtrim().str(); + else if (Key) + llvm::consumeError(writeTextFile(KeyFile, *Key)); } }; { @@ -2088,7 +2243,8 @@ class Verifier { Failures[Name] = *BuildErrors[I]; continue; } - Built += Name + "\tCppVerify.Proofs." + Goal->Group + "." + Name + "\n"; + Built += Name + "\tCppVerify.Proofs." + Goal->Group + "." + Name + + "\tCppVerify.Goals." + Goal->Group + "\n"; } if (Built.empty()) return Failures; @@ -2179,7 +2335,8 @@ class Verifier { : ""; for (size_t Next = 0; Next < Goals.size() && !interruptRequested();) { - std::string Text = "import CppVerify.User\nimport CppVerify.Auto\n\n" + std::string Text = "import CppVerify.Generated\nimport CppVerify.User\n" + "import CppVerify.Auto\n\n" "set_option cppverify.autoReport " + ReportName + "\n#eval CppVerify.Auto.report " + ReportName + " \"ready\"\n"; @@ -2373,8 +2530,9 @@ class Verifier { {VerifyDiagnostic::Warning, "cppverify_auto was not tried on the new Lean goals: " + Why}); }; - if (auto Build = Launcher->run( - {"build", "CppVerify.User", "CppVerify.Auto"}, "build", Root); + if (auto Build = Launcher->run({"build", "CppVerify.Generated", + "CppVerify.User", "CppVerify.Auto"}, + "build", Root); !Build) return skipped( "the project does not build (" + @@ -2425,10 +2583,10 @@ class Verifier { const std::string Text = Trial.Step.empty() ? leanProofHeader(Goal, Tag + Trial.Why) + - leanProof(Goal.Name, Goal.Intros, "sorry") + leanProof(Goal.Name, Goal.Group, Goal.Intros, "sorry") : leanProofHeader(Goal, Tag + "proves it with " + Trial.Step, /*Automatic=*/true) + - leanProof(Goal.Name, Goal.Intros, Trial.Step); + leanProof(Goal.Name, Goal.Group, Goal.Intros, Trial.Step); if (llvm::Error Error = writeTextFile(pathOf(Goal), Text)) Failures.push_back(llvm::toString(std::move(Error))); } @@ -2664,19 +2822,16 @@ class Verifier { std::string LeanOutputPath = Opts.LeanOutPath; const bool HasLeanProject = !Opts.LeanProjectPath.empty() || !Opts.LeanFallbackProjectPath.empty(); + // A project's goals go to modules, one per function. + LeanProjectModules LeanModules; if (HasLeanProject) { - auto GeneratedPath = initializeLeanProject(); - if (!GeneratedPath) { + if (llvm::Error Error = initializeLeanProject()) { Diags.push_back({VerifyDiagnostic::Error, "cannot initialize Lean project (" + - llvm::toString(GeneratedPath.takeError()) + ")"}); + llvm::toString(std::move(Error)) + ")"}); return false; } - LeanOutputPath = std::move(*GeneratedPath); - } - if ((Opts.Backend == BackendKind::Lean || - !Opts.LeanFallbackProjectPath.empty()) && - !LeanOutputPath.empty()) { + } else if (Opts.Backend == BackendKind::Lean && !LeanOutputPath.empty()) { std::error_code EC; LeanFile = std::make_unique(LeanOutputPath, EC, llvm::sys::fs::OF_Text); @@ -2720,11 +2875,12 @@ class Verifier { if (!Parallel) SharedBackend = createVerifyBackend( Opts.Backend, LeanOut, Opts.BMCUnroll, Execution, - Opts.LeanProjectPath.empty() ? nullptr : &LeanProjectGoals); + Opts.LeanProjectPath.empty() ? nullptr : &LeanProjectGoals, + Opts.LeanProjectPath.empty() ? nullptr : &LeanModules); std::unique_ptr LeanFallbackBackend; if (!Opts.LeanFallbackProjectPath.empty()) - LeanFallbackBackend = std::make_unique( - LeanFile.get(), &LeanProjectGoals); + LeanFallbackBackend = + std::make_unique(&LeanModules, &LeanProjectGoals); // Vacuity checks: whether a verified function's end is reachable at all. // A vacuous path is refuted quickly; a satisfiable one is not worth // searching long, since an unsettled check only omits a warning. @@ -4160,15 +4316,14 @@ class Verifier { // certified one is a proof like a solver's, and one that fails, or that // certification does not check, establishes nothing. if (HasLeanProject) { - if (LeanFile) { - LeanFile->flush(); - LeanFile.reset(); - } std::vector ExportedGoals; llvm::copy_if(LeanProjectGoals, std::back_inserter(ExportedGoals), [](const LeanProjectGoal &Goal) { return Goal.Exported; }); - llvm::Error Finalized = finalizeLeanProject( - LeanProjectGoals, LeanFallbackBackend ? &LeanRunGroups : nullptr); + const std::set *RunGroups = + LeanFallbackBackend ? &LeanRunGroups : nullptr; + llvm::Error Finalized = writeLeanProjectModules(LeanModules); + if (!Finalized) + Finalized = finalizeLeanProject(LeanProjectGoals, RunGroups); if (!Finalized && Opts.LeanAuto) automateLeanProject(LeanProjectGoals); if (!Finalized) From da1845ac80628be4824f9bc6a8db765d98f3f965 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:05 +0530 Subject: [PATCH 18/80] test: Add a helper that prints a Lean project's generated text in import order. --- clang/test/Verify/suite/Inputs/lean_project_text.py | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_project_text.py diff --git a/clang/test/Verify/suite/Inputs/lean_project_text.py b/clang/test/Verify/suite/Inputs/lean_project_text.py new file mode 100644 index 0000000000..a090df2bd5 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_project_text.py @@ -0,0 +1,11 @@ +"""Prints the generated text of a Lean project: its prelude, its specs, and +each goal module in the order its Generated module imports them, the +functions' source order.""" +import pathlib, sys + +root = pathlib.Path(sys.argv[1]) / "CppVerify" +parts = [root / "Prelude.lean", root / "Specs.lean"] +for line in (root / "Generated.lean").read_text().splitlines(): + if line.startswith("import CppVerify.Goals."): + parts.append(root / "Goals" / (line[len("import CppVerify.Goals."):] + ".lean")) +sys.stdout.write("".join(part.read_text() for part in parts)) From 548094c26c56f038f8e851c03f52a1851e333cd4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:05 +0530 Subject: [PATCH 19/80] test: Read a Lean project's goals from its modules in the fidelity gate. --- clang/test/Verify/suite/Inputs/run_backend_fidelity.py | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/clang/test/Verify/suite/Inputs/run_backend_fidelity.py b/clang/test/Verify/suite/Inputs/run_backend_fidelity.py index 18d97cddca..d8734e15cc 100644 --- a/clang/test/Verify/suite/Inputs/run_backend_fidelity.py +++ b/clang/test/Verify/suite/Inputs/run_backend_fidelity.py @@ -476,8 +476,14 @@ def check_lean_identity(cpp_verify, source, canonical, work): ], {0}, ) - generated = project / "CppVerify" / "Generated.lean" - text = generated.read_text() + # The project's generated text: its prelude, specs, and each goal module. + root = project / "CppVerify" + modules = [root / "Prelude.lean", root / "Specs.lean"] + [ + root / "Goals" / (line[len("import CppVerify.Goals."):] + ".lean") + for line in (root / "Generated.lean").read_text().splitlines() + if line.startswith("import CppVerify.Goals.") + ] + text = "".join(module.read_text() for module in modules) if "sorry" in text: fail("generated Lean semantics contains an admitted proof") From 2c9de793f21997699dfcd61394e3a85b54104334 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:05 +0530 Subject: [PATCH 20/80] test: Add the five functions of the Lean modules test. --- .../test/Verify/suite/Inputs/lean_modules.cpp | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_modules.cpp diff --git a/clang/test/Verify/suite/Inputs/lean_modules.cpp b/clang/test/Verify/suite/Inputs/lean_modules.cpp new file mode 100644 index 0000000000..eb8b11b768 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_modules.cpp @@ -0,0 +1,36 @@ +// Five functions for lean_modules.test: inc and dbl, which cppverify_auto +// proves, and two that apply the recursive spec tri, whose postconditions +// Inputs/lean_modules_*.lean prove. + +cppverify::spec int tri(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : tri(n - 1) + n; +} + +int inc(int x) + cppverify::pre(0 <= x && x < 1000) + cppverify::post(cppverify::result == x + 1) +{ + return x + 1; +} + +int dbl(int x) + cppverify::pre(0 <= x && x < 1000) + cppverify::post(cppverify::result == 2 * x) +{ + return x + x; +} + +int tri_zero() + cppverify::post(cppverify::result == tri(0)) +{ + return 0; +} + +int plus_tri_zero(int x) + cppverify::pre(0 <= x && x < 1000) + cppverify::post(cppverify::result == x + tri(0)) +{ + return x; +} From 28af37d0fd176cd96bd9e2656010edb459e3873e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:06 +0530 Subject: [PATCH 21/80] test: Add the proof of tri_zero's postcondition for the Lean modules test. --- .../Verify/suite/Inputs/lean_modules_tri_zero.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_modules_tri_zero.lean diff --git a/clang/test/Verify/suite/Inputs/lean_modules_tri_zero.lean b/clang/test/Verify/suite/Inputs/lean_modules_tri_zero.lean new file mode 100644 index 0000000000..03445c1a79 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_modules_tri_zero.lean @@ -0,0 +1,11 @@ +import CppVerify.Goals.cppverify_tri_zero_e086e9 +import CppVerify.User +import CppVerify.Auto + +theorem cppverify_tri_zero_e086e9_postcondition_44e49d34_proof : + cppverify_tri_zero_e086e9_postcondition_44e49d34 := by + apply cppverify_tri_zero_e086e9_postcondition_44e49d34.of_readable + intro __heap_alloc_0 __heap_live_0 __result_1 tri_0 _ _ h_null_1 h_null_2 h_result_1 + rw [tri_0] at * + simp only [cppSpecBody_e086e9ab_fn_5f5a3374726969_1] at * + cppverify_auto From 901c3ca0e94edafadb4f06dd70a4d336589e2ba9 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:06 +0530 Subject: [PATCH 22/80] test: Add the proof of plus_tri_zero's postcondition for the Lean modules test. --- .../suite/Inputs/lean_modules_plus_tri_zero.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_modules_plus_tri_zero.lean diff --git a/clang/test/Verify/suite/Inputs/lean_modules_plus_tri_zero.lean b/clang/test/Verify/suite/Inputs/lean_modules_plus_tri_zero.lean new file mode 100644 index 0000000000..2af3414bc0 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_modules_plus_tri_zero.lean @@ -0,0 +1,11 @@ +import CppVerify.Goals.cppverify_plus_tri_zero_10bb8a +import CppVerify.User +import CppVerify.Auto + +theorem cppverify_plus_tri_zero_10bb8a_postcondition_8b45419c_proof : + cppverify_plus_tri_zero_10bb8a_postcondition_8b45419c := by + apply cppverify_plus_tri_zero_10bb8a_postcondition_8b45419c.of_readable + intro __heap_alloc_0 __heap_live_0 __result_1 x_0 tri_0 _ _ h_pre_1 h_null_1 h_null_2 h_result_1 + rw [tri_0] at * + simp only [cppSpecBody_10bb8a86_fn_5f5a3374726969_1] at * + cppverify_auto From adf19a3b5f4b7f57e432c45502c8610dc5ef1fde Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:06 +0530 Subject: [PATCH 23/80] test: Check the module of each function's Lean goals and incremental certification. --- clang/test/Verify/suite/lean_modules.test | 118 ++++++++++++++++++++++ 1 file changed, 118 insertions(+) create mode 100644 clang/test/Verify/suite/lean_modules.test diff --git a/clang/test/Verify/suite/lean_modules.test b/clang/test/Verify/suite/lean_modules.test new file mode 100644 index 0000000000..50ef7e179f --- /dev/null +++ b/clang/test/Verify/suite/lean_modules.test @@ -0,0 +1,118 @@ +# REQUIRES: lean +# +# A Lean project has a module of goals for each function, +# CppVerify/Goals/.lean, which imports CppVerify.Specs, where each spec +# the goals apply is declared once. A proof imports its function's goals, +# User, and Auto, so certification builds again only the proofs of a function +# whose goals changed. +# +# RUN: rm -rf %t && mkdir -p %t && cp %S/Inputs/lean_modules.cpp %t/m.cpp +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %t/m.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Generated.lean --check-prefix=GENERATED +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Specs.lean --check-prefix=SPECS --implicit-check-not=opaque +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Goals/cppverify_tri_zero_e086e9.lean --check-prefix=GOALS +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Goals/cppverify_plus_tri_zero_10bb8a.lean --check-prefix=GOALS-PLUS +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_inc_c0810e/cppverify_inc_c0810e_postcondition_e4ef4574.lean --check-prefix=IMPORTS +# RUN: FileCheck %s --input-file=%t/p/CppVerify/User.lean --check-prefix=USER +# RUN: FileCheck %s --input-file=%t/p/CppVerify.lean --check-prefix=ROOT +# +# The two goal modules that apply tri are certified together. +# RUN: cp %S/Inputs/lean_modules_tri_zero.lean %t/p/CppVerify/Proofs/cppverify_tri_zero_e086e9/cppverify_tri_zero_e086e9_postcondition_44e49d34.lean +# RUN: cp %S/Inputs/lean_modules_plus_tri_zero.lean %t/p/CppVerify/Proofs/cppverify_plus_tri_zero_10bb8a/cppverify_plus_tri_zero_10bb8a_postcondition_8b45419c.lean +# RUN: %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %t/m.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFY +# +# A run of the same source writes no file. +# RUN: touch %t/same +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %t/m.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT +# RUN: find %t/p -newer %t/same -type f -not -path '*/.lake/*' | count 0 +# +# A change to dbl builds dbl's goal module and proofs again, and the module +# that imports every goal module; nothing else. +# RUN: touch %t/before +# RUN: sed 's/cppverify::result == 2 \* x/cppverify::result == x + x/' %S/Inputs/lean_modules.cpp > %t/m.cpp +# RUN: %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %t/m.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFY +# RUN: cd %t/p/.lake/build/lib/lean && find CppVerify -name '*.olean' -newer %t/before | env LC_ALL=C sort | FileCheck %s --check-prefix=REBUILT --implicit-check-not=olean +# +# `lake build` builds every proof. Run in the project, elan selects its +# toolchain. +# RUN: cd %t/p && lake build 2>&1 | FileCheck %s --check-prefix=LAKE +# +# A function that is gone takes its goal module with it. +# RUN: sed -e 's/cppverify::result == 2 \* x/cppverify::result == x + x/' -e '/^int inc(/,/^}/d' %S/Inputs/lean_modules.cpp > %t/m.cpp +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %t/m.cpp -- 2>&1 | FileCheck %s --check-prefix=WITHOUT-INC +# RUN: not test -e %t/p/CppVerify/Goals/cppverify_inc_c0810e.lean +# +# A project of an earlier release, whose User imports Generated, still +# certifies: each proof then depends on every goal module. +# RUN: printf 'import CppVerify.Generated\n' > %t/p/CppVerify/User.lean +# RUN: %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %t/m.cpp -- 2>&1 | FileCheck %s --check-prefix=OLD-USER +# +# A fallback run writes the goal modules of the functions it exports and no +# other, since Specs then declares only the specs those apply. Here the +# solver verifies every function: no goal module stays, and every proof does. +# RUN: %cpp-verify --lean-fallback=%t/p %t/m.cpp -- 2>&1 | FileCheck %s --check-prefix=FALLBACK +# RUN: not test -e %t/p/CppVerify/Goals/cppverify_tri_zero_e086e9.lean +# RUN: test -f %t/p/CppVerify/Proofs/cppverify_tri_zero_e086e9/cppverify_tri_zero_e086e9_postcondition_44e49d34.lean +# RUN: cd %t/p && lake build 2>&1 | FileCheck %s --check-prefix=LAKE + +# EXPORT: Exported: decreases: tri (cppverify_auto proved 1 of 1 goals) +# EXPORT-NEXT: Exported: lean obligation: inc (cppverify_auto proved 3 of 3 goals) +# EXPORT-NEXT: Exported: lean obligation: dbl (cppverify_auto proved 3 of 3 goals) +# EXPORT-NEXT: Exported: lean obligation: tri_zero (cppverify_auto proved 1 of 2 goals) +# EXPORT-NEXT: Exported: lean obligation: plus_tri_zero (cppverify_auto proved 1 of 2 goals) + +# GENERATED: {{^}}import CppVerify.Prelude{{$}} +# GENERATED-NEXT: {{^}}import CppVerify.Specs{{$}} +# GENERATED-NEXT: {{^}}import CppVerify.Goals.cppverify_tri_decreases_f55d4c{{$}} +# GENERATED-NEXT: {{^}}import CppVerify.Goals.cppverify_inc_c0810e{{$}} +# GENERATED-NEXT: {{^}}import CppVerify.Goals.cppverify_dbl_47613e{{$}} +# GENERATED-NEXT: {{^}}import CppVerify.Goals.cppverify_tri_zero_e086e9{{$}} +# GENERATED-NEXT: {{^}}import CppVerify.Goals.cppverify_plus_tri_zero_10bb8a{{$}} +# GENERATED-EMPTY: + +# SPECS: {{^}}import CppVerify.Prelude{{$}} +# SPECS: /- spec function: tri -/ +# SPECS-NEXT: {{^}}opaque cppSpec_fn_5f5a3374726969 : Int -> Int{{$}} + +# Each goal module defines the spec bodies it uses under its own prefix. +# GOALS: {{^}}import CppVerify.Specs{{$}} +# GOALS-NOT: {{^}}import +# GOALS: {{^}}attribute [local instance] cppVerifyPropDecidable{{$}} +# GOALS: {{^}}def cppSpecBody_e086e9ab_fn_5f5a3374726969_1 +# GOALS-PLUS: {{^}}import CppVerify.Specs{{$}} +# GOALS-PLUS: {{^}}def cppSpecBody_10bb8a86_fn_5f5a3374726969_1 + +# IMPORTS: {{^}}import CppVerify.Goals.cppverify_inc_c0810e{{$}} +# IMPORTS-NEXT: {{^}}import CppVerify.User{{$}} +# IMPORTS-NEXT: {{^}}import CppVerify.Auto{{$}} +# IMPORTS-NOT: import + +# USER: {{^}}import CppVerify.Specs{{$}} +# ROOT: {{^}}import CppVerify.Check{{$}} + +# CERTIFY: Certified: decreases: tri [backend=Lean] +# CERTIFY-NEXT: Certified: inc [backend=Lean] +# CERTIFY-NEXT: Certified: dbl [backend=Lean] +# CERTIFY-NEXT: Certified: tri_zero [backend=Lean] +# CERTIFY-NEXT: Certified: plus_tri_zero [backend=Lean] + +# REBUILT: CppVerify/Generated.olean +# REBUILT-NEXT: CppVerify/Goals/cppverify_dbl_47613e.olean +# REBUILT-NEXT: CppVerify/Proofs/cppverify_dbl_47613e/cppverify_dbl_47613e_missing_return_54ae7c80.olean +# REBUILT-NEXT: CppVerify/Proofs/cppverify_dbl_47613e/cppverify_dbl_47613e_overflow_fce34d13.olean +# REBUILT-NEXT: CppVerify/Proofs/cppverify_dbl_47613e/cppverify_dbl_47613e_postcondition_ce469baa.olean + +# LAKE: Build completed successfully + +# WITHOUT-INC: Exported: decreases: tri +# WITHOUT-INC-NEXT: Exported: lean obligation: dbl +# WITHOUT-INC-NEXT: Exported: lean obligation: tri_zero + +# OLD-USER: Certified: decreases: tri [backend=Lean] +# OLD-USER-NEXT: Certified: dbl [backend=Lean] +# OLD-USER-NEXT: Certified: tri_zero [backend=Lean] +# OLD-USER-NEXT: Certified: plus_tri_zero [backend=Lean] + +# FALLBACK: Verified: dbl [backend=z3] +# FALLBACK-NEXT: Verified: tri_zero [backend=z3] +# FALLBACK-NEXT: Verified: plus_tri_zero [backend=z3] From 0350c69fade7a7703c36f24bbe03f6e979cafc9a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:07 +0530 Subject: [PATCH 24/80] test: Expect the goal module among the imports of an automatic proof. --- clang/test/Verify/suite/lean_automation.test | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/clang/test/Verify/suite/lean_automation.test b/clang/test/Verify/suite/lean_automation.test index 0862d09576..5c5ace654f 100644 --- a/clang/test/Verify/suite/lean_automation.test +++ b/clang/test/Verify/suite/lean_automation.test @@ -28,7 +28,7 @@ # # A stub that no revision of cppverify_auto tried, as before automation, and # one an earlier revision tried, are tried. -# RUN: sed -i -e '/^ automation:/d' -e '/^import CppVerify.Auto$/d' -e 's/^ cppverify_auto_grind$/ sorry/' %t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_missing_return_54ae7c80.lean +# RUN: sed -i -e '/^ automation:/d' -e '/^import CppVerify.Goals\./d' -e '/^import CppVerify.Auto$/d' -e 's/^ cppverify_auto_grind$/ sorry/' %t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_missing_return_54ae7c80.lean # RUN: sed -i 's/cppverify_auto 1 did not prove it/cppverify_auto 0 did not prove it/' %t/p/CppVerify/Proofs/cppverify_square_934e38/cppverify_square_934e38_overflow_f86973f7.lean # RUN: %cpp-verify --backend=lean --lean-project=%t/p %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=EDITED # RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_missing_return_54ae7c80.lean --check-prefix=TRIED @@ -57,6 +57,7 @@ # PROVED: automation: cppverify_auto 1 proves it with cppverify_auto_grind # PROVED-NEXT: cppverify_auto proves this goal. cpp-verify rewrites this file only while it # PROVED-NEXT: is unedited; a proof you write here is yours, kept as any other. -/ +# PROVED-NEXT: import CppVerify.Goals.cppverify_next_e1e917 # PROVED-NEXT: import CppVerify.User # PROVED-NEXT: import CppVerify.Auto # PROVED-EMPTY: From 56a9fb07d2180a6807a2361a8d51bc0ffc94a13e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:07 +0530 Subject: [PATCH 25/80] test: Expect the goal module in the message for a shadowed goal. --- clang/test/Verify/suite/lean_certifier.test | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/clang/test/Verify/suite/lean_certifier.test b/clang/test/Verify/suite/lean_certifier.test index 353324ad67..7edbabeb7f 100644 --- a/clang/test/Verify/suite/lean_certifier.test +++ b/clang/test/Verify/suite/lean_certifier.test @@ -67,9 +67,9 @@ # 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.Proofs.cppverify_one_99bcee.cppverify_one_99bcee_postcondition_646d2761 declares cppverify_one_99bcee_postcondition_646d2761, which CppVerify.Generated declares) +# 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.Goals.cppverify_one_99bcee 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: 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.Goals.cppverify_early_103f65 declares) # FIRST-NEXT: Certified: fine [backend=Lean] # HIDDEN: Certified: fine [backend=Lean] From 9f9fbb290836ab9535d99c296c6ea8c7ffee7a73 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:07 +0530 Subject: [PATCH 26/80] test: Expect an admitted User lemma to fail every goal through the checker. --- clang/test/Verify/suite/lean_certify.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/clang/test/Verify/suite/lean_certify.cpp b/clang/test/Verify/suite/lean_certify.cpp index 2cd5205c70..831f3d40c4 100644 --- a/clang/test/Verify/suite/lean_certify.cpp +++ b/clang/test/Verify/suite/lean_certify.cpp @@ -28,7 +28,6 @@ void trivial() // ADMITTED-SAME: declaration uses `sorry` // CERTIFIED: Certified: trivial [backend=Lean] // USER-ADMITTED: Unresolved: lean obligation: trivial (Lean certification failed: -// USER-ADMITTED-SAME: User.lean -// USER-ADMITTED-SAME: declaration uses `sorry` +// USER-ADMITTED-SAME: unfinished of CppVerify.User uses sorry // AXIOM: Unresolved: lean obligation: trivial (Lean certification failed: the proof of {{.*}}::missing-return@synthetic: cppverify_trivial_3e4f5a_missing_return_ba8abb90_proof depends on the axiom escape, which is not one of Lean's foundations; the proof of {{.*}}::postcondition@{{[0-9]+}}:{{[0-9]+}}: cppverify_trivial_3e4f5a_postcondition_ba8abb90_proof depends on the axiom escape, which is not one of Lean's foundations) // STALE: Unresolved: lean obligation: trivial (Lean certification failed: From e261a4d7eed9464496536ca8a52bbff2f599804a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:08 +0530 Subject: [PATCH 27/80] test: Read the fallback project's generated text from its modules. --- clang/test/Verify/suite/lean_fallback.test | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/clang/test/Verify/suite/lean_fallback.test b/clang/test/Verify/suite/lean_fallback.test index 1aed3ce551..72fe98493b 100644 --- a/clang/test/Verify/suite/lean_fallback.test +++ b/clang/test/Verify/suite/lean_fallback.test @@ -5,7 +5,7 @@ // RUN: test -f %t.project/CppVerify/Generated.lean // RUN: test -f %t.project/CppVerify/Check.lean // RUN: grep -q '^import CppVerify.Proofs.cppverify_' %t.project/CppVerify/Check.lean -// RUN: FileCheck %s --input-file=%t.project/CppVerify/Generated.lean --check-prefix=GENERATED +// RUN: %python %S/Inputs/lean_project_text.py %t.project | FileCheck %s --check-prefix=GENERATED // RUN: not %cpp-verify --solver-rlimit=400 --lean-fallback-scope=all --lean-fallback=%t.project --lean-certify %S/spec_fuel_recursive_pass.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFY // RUN: cp %S/Inputs/lean_fallback_goal_1.lean %t.project/CppVerify/Proofs/cppverify_fibo_step_624f01/cppverify_fibo_step_624f01_missing_return_ba8abb90.lean // RUN: cp %S/Inputs/lean_fallback_goal_2.lean %t.project/CppVerify/Proofs/cppverify_fibo_step_624f01/cppverify_fibo_step_624f01_postcondition_559cb60a.lean @@ -37,6 +37,6 @@ // FAILED-JSON-SAME: "reason":"lean.export-failed" // FAILED-JSON-SAME: "status":"unresolved" -// GENERATED: Generated by CppVerify for an editable Lean project. +// GENERATED: Generated by CppVerify. Regeneration replaces this file, never a proof. // GENERATED: function: fibo_step // GENERATED: function: fibo_six From 4cbeefd8613993f09361318f296422ead5f7ea20 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:08 +0530 Subject: [PATCH 28/80] test: Find spec bodies in their goal module and the goal module in a moved proof's imports. --- clang/test/Verify/suite/lean_identity.test | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/clang/test/Verify/suite/lean_identity.test b/clang/test/Verify/suite/lean_identity.test index d66b654f83..47ca665edc 100644 --- a/clang/test/Verify/suite/lean_identity.test +++ b/clang/test/Verify/suite/lean_identity.test @@ -26,7 +26,7 @@ # statement: every proof stays, and so do the spec bodies the proofs unfold. # RUN: %cpp-verify --backend=lean --lean-project=%t/p %t/-src/inserted.cpp -- 2>&1 | FileCheck %s --check-prefix=INSERTED --implicit-check-not=warning # RUN: grep -q 'cppSpecBody_6a2cf351_fn_5f5a3374726969_4,' %t/p/CppVerify/Proofs/cppverify_six_6a2cf3/cppverify_six_6a2cf3_postcondition_198bc076.lean -# RUN: grep -q '^def cppSpecBody_6a2cf351_fn_5f5a3374726969_4$' %t/p/CppVerify/Generated.lean +# RUN: grep -q '^def cppSpecBody_6a2cf351_fn_5f5a3374726969_4$' %t/p/CppVerify/Goals/cppverify_six_6a2cf3.lean # RUN: test -f %t/p/CppVerify/Proofs/cppverify_zero_5ece85/cppverify_zero_5ece85_postcondition_36923ed0.lean # # Renamed functions take their proofs along, each its own, with the names @@ -117,6 +117,7 @@ # HEADER-NEXT: bodies: cppSpecBody_6a2cf351_ # HEADER-NEXT: source: {{.*}}/ -src/base.cpp:8:37 # HEADER: -/ +# HEADER-NEXT: import CppVerify.Goals.cppverify_six_6a2cf3 # HEADER-NEXT: import CppVerify.User # HEADER-EMPTY: # HEADER-NEXT: theorem cppverify_six_6a2cf3_postcondition_198bc076_proof : From accb2c9468c06946796c7749c7f5339139ede508 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:09 +0530 Subject: [PATCH 29/80] test: Read the Lean projects' generated text from their modules. --- clang/test/Verify/suite/lean_kernel.test | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/clang/test/Verify/suite/lean_kernel.test b/clang/test/Verify/suite/lean_kernel.test index 15440d41e0..df0e028ac2 100644 --- a/clang/test/Verify/suite/lean_kernel.test +++ b/clang/test/Verify/suite/lean_kernel.test @@ -7,12 +7,13 @@ // RUN: lake --dir=%t.quant build CppVerify.Generated // RUN: %cpp-verify --backend=lean --lean-project=%t.recursive %S/spec_fuel_recursive_pass.cpp -- // RUN: lake --dir=%t.recursive build CppVerify.Generated -// RUN: %python -c "import os, sys; sys.exit(os.path.getsize(r'%t.recursive/CppVerify/Generated.lean') >= 100000)" +// RUN: %python %S/Inputs/lean_project_text.py %t.recursive > %t.recursive.lean +// RUN: %python -c "import os, sys; sys.exit(os.path.getsize(r'%t.recursive.lean') >= 100000)" // RUN: %cpp-verify --backend=lean --lean-project=%t.names %S/Inputs/lean_name_encoding.cpp -- -// RUN: grep -Eq 'cppEncoded_[0-9a-f]+' %t.names/CppVerify/Generated.lean +// RUN: %python %S/Inputs/lean_project_text.py %t.names | grep -Eq 'cppEncoded_[0-9a-f]+' // RUN: lake --dir=%t.names build CppVerify.Generated // RUN: lake --dir=%t.names build CppVerify.Check // Heap-reading specs take the heap state as a CppHeap argument. // RUN: %cpp-verify --check-ub --backend=lean --lean-project=%t.heapspec %S/heap_reading_spec.cpp -- -// RUN: grep -q '(__spec_heap : CppHeap)' %t.heapspec/CppVerify/Generated.lean +// RUN: %python %S/Inputs/lean_project_text.py %t.heapspec | grep -q '(__spec_heap : CppHeap)' // RUN: lake --dir=%t.heapspec build CppVerify.Generated From 66be53e3b1e2adb7339e9506c555eaf6ec35a22d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:09 +0530 Subject: [PATCH 30/80] test: Read the Lean project's generated text from its modules. --- clang/test/Verify/suite/lean_project.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/clang/test/Verify/suite/lean_project.cpp b/clang/test/Verify/suite/lean_project.cpp index 51f4a7c9c6..5561998437 100644 --- a/clang/test/Verify/suite/lean_project.cpp +++ b/clang/test/Verify/suite/lean_project.cpp @@ -7,7 +7,7 @@ // RUN: test -f %t.project/CppVerify/Check.lean // RUN: test -f %t.project/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_missing_return_ba8abb90.lean // RUN: grep -Fxq 'leanprover/lean4:v4.35.0' %t.project/lean-toolchain -// RUN: FileCheck %s --input-file=%t.project/CppVerify/Generated.lean --check-prefix=GENERATED +// RUN: %python %S/Inputs/lean_project_text.py %t.project | FileCheck %s --check-prefix=GENERATED // RUN: grep -Fq 'import CppVerify.Proofs.cppverify_trivial_3e4f5a.cppverify_trivial_3e4f5a_missing_return_ba8abb90' %t.project/CppVerify/Check.lean // RUN: echo '/- USER_KEEP -/' >> %t.project/CppVerify/User.lean // RUN: echo '/- PROOF_KEEP -/' >> %t.project/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_missing_return_ba8abb90.lean @@ -30,7 +30,7 @@ void trivial() {} // EXPORT: Exported: lean obligation: trivial -// GENERATED: Generated by CppVerify for an editable Lean project. +// GENERATED: Generated by CppVerify. Regeneration replaces this file, never a proof. // GENERATED-NOT: unchecked Lean scratch-pad // GENERATED: function: trivial // GENERATED: source: {{.*}}lean_project.cpp:{{[0-9]+:[0-9]+}} From 97f37766eed6a90d57ab9835c04c1b766a70b230 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:09 +0530 Subject: [PATCH 31/80] test: Read and edit the readable goals in their function's module. --- clang/test/Verify/suite/lean_readable.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/clang/test/Verify/suite/lean_readable.cpp b/clang/test/Verify/suite/lean_readable.cpp index 8227146516..16bd3f0f2b 100644 --- a/clang/test/Verify/suite/lean_readable.cpp +++ b/clang/test/Verify/suite/lean_readable.cpp @@ -7,7 +7,7 @@ // // RUN: rm -rf %t && mkdir -p %t // RUN: %cpp-verify --backend=lean --no-lean-auto --lean-project=%t/p %s -- 2>&1 | FileCheck %s --check-prefix=EXPORT -// RUN: FileCheck %s --input-file=%t/p/CppVerify/Generated.lean +// RUN: %python %S/Inputs/lean_project_text.py %t/p | FileCheck %s // RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_twice_edf933/cppverify_twice_edf933_postcondition_28de726e.lean --check-prefix=STUB // RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_poly_c94108/cppverify_poly_c94108_postcondition_fde367c1.lean --check-prefix=LETS // Every stub's names match its readable form: the project builds, with @@ -21,7 +21,7 @@ // // A readable form that says less than its goal does not build: here the // definition of b is replaced by the conclusion it should lead to. -// RUN: sed -i 's/(h_b_1 : b_1 = __local_call_2_1)/(h_b_1 : b_1 = x_0 + (BitVec.ofInt 32 (2)))/' %t/p/CppVerify/Generated.lean +// RUN: sed -i 's/(h_b_1 : b_1 = __local_call_2_1)/(h_b_1 : b_1 = x_0 + (BitVec.ofInt 32 (2)))/' %t/p/CppVerify/Goals/cppverify_twice_edf933.lean // RUN: cd %t/p && not lake build CppVerify.Generated 2>&1 | FileCheck %s --check-prefix=BRIDGE int next(int x) @@ -222,4 +222,4 @@ int poly(int x) // TRUSTED: Exported: lean obligation: twice // CERTIFIED: Certified: twice [backend=Lean] [trusts=next] -// BRIDGE: Generated.lean:{{[0-9]+}}:{{[0-9]+}}: Application type mismatch: The argument +// BRIDGE: cppverify_twice_edf933.lean:{{[0-9]+}}:{{[0-9]+}}: Application type mismatch: The argument From 6ae6209ce5783d5281ae93d9048380ce697ff449 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:10 +0530 Subject: [PATCH 32/80] test: Read the exported Lean semantics from the project's modules. --- clang/test/Verify/suite/lean_semantics.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/clang/test/Verify/suite/lean_semantics.cpp b/clang/test/Verify/suite/lean_semantics.cpp index dcafd92436..5ec309a04d 100644 --- a/clang/test/Verify/suite/lean_semantics.cpp +++ b/clang/test/Verify/suite/lean_semantics.cpp @@ -9,8 +9,8 @@ // // RUN: rm -rf %t.export %t.mix %t.numerals %t.call // RUN: %cpp-verify --backend=lean --lean-project=%t.export %s -- 2>&1 | FileCheck %s --check-prefix=EXPORT -// RUN: FileCheck %s --input-file=%t.export/CppVerify/Generated.lean --check-prefix=LEAN -// RUN: not grep -E 'BitVec\.(udiv|sdiv) ' %t.export/CppVerify/Generated.lean +// RUN: %python %S/Inputs/lean_project_text.py %t.export | FileCheck %s --check-prefix=LEAN +// RUN: %python %S/Inputs/lean_project_text.py %t.export | not grep -E 'BitVec\.(udiv|sdiv) ' // RUN: lake --dir=%t.export build CppVerify.Generated // // The prelude's values where C++, SMT-LIB, and Lean's own operators differ. From 7e119a19fbae3658ee70c9db4c4d7dcfeb00840e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:10 +0530 Subject: [PATCH 33/80] test: Expect the trial of cppverify_auto to build the goal modules too. --- clang/test/Verify/suite/lean_toolchain.test | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang/test/Verify/suite/lean_toolchain.test b/clang/test/Verify/suite/lean_toolchain.test index 306038ccee..03b229fd70 100644 --- a/clang/test/Verify/suite/lean_toolchain.test +++ b/clang/test/Verify/suite/lean_toolchain.test @@ -22,7 +22,7 @@ # The trial of cppverify_auto, then certification, each with the pin. # ELAN-LOG: {{^}}+leanprover/lean4:v4.35.0 --version{{$}} -# ELAN-LOG-NEXT: {{^}}+leanprover/lean4:v4.35.0 --dir={{.*}}.project build CppVerify.User CppVerify.Auto{{$}} +# ELAN-LOG-NEXT: {{^}}+leanprover/lean4:v4.35.0 --dir={{.*}}.project build CppVerify.Generated CppVerify.User CppVerify.Auto{{$}} # ELAN-LOG-NEXT: {{^}}+leanprover/lean4:v4.35.0 --version{{$}} # ELAN-LOG-NEXT: {{^}}+leanprover/lean4:v4.35.0 --dir={{.*}}.project build CppVerify.Generated CppVerify.User CppVerify.Auto{{$}} From 71ce0e1dddfd5afab70a5cdb7f1f270fccac7ba5 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:10 +0530 Subject: [PATCH 34/80] docs: Explain the module of each function's Lean goals and incremental certification in chapter 17. --- .../part-ii/ch17-backends-modular-calls.rst | 132 ++++++++++++++++-- 1 file changed, 117 insertions(+), 15 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 c403e1a17a..ce0f0911a4 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -156,21 +156,22 @@ For an explicit interactive proof: # complete proof/CppVerify/Proofs/*/*.lean; put shared lemmas in User.lean cpp-verify --backend=lean --lean-project=proof --lean-certify file.cpp -``Generated.lean``, ``Auto.lean``, and ``Check.lean`` are machine-owned; -``Check.lean`` imports every proof, so ``lake build CppVerify.Check`` builds -them all at once. ``User.lean`` is never overwritten, and each goal has a proof +The generated modules (``Prelude.lean``, ``Specs.lean``, ``Goals/``, +``Generated.lean``, ``Auto.lean``, and ``Check.lean``) are machine-owned; +``Check.lean`` imports every proof, so ``lake build``, run in the project, +builds them all (see `One module of goals per function`_ below). +``User.lean`` is never overwritten, and each goal has a proof file of its own: the proof ``cppverify_auto`` finds for it, or a stub (see `Proofs cppverify_auto finds`_ below). cpp-verify rewrites that file only while nobody has edited it; an edited one it never rewrites, but moves with its goal (see `Proofs that follow their goals`_ below). The project pins ``leanprover/lean4:v4.35.0``, which certification runs whatever elan's default toolchain is; a project 0.1 generated, pinned to ``v4.32.2``, moves to -it with a warning. Certification compiles the user -module and each proof file with admissions promoted to errors, then checks the -compiled modules as described in `What certification checks`_ below. +it with a warning. Certification builds the project +and compiles each proof file with admissions promoted to errors, then checks +the compiled modules as described in `What certification checks`_ below. -Each goal in ``Generated.lean`` is a Lean proposition that means what the -obligation means, so a proof of it is a proof of the obligation: +Each goal is a Lean proposition that means what the obligation means, so a proof of it is a proof of the obligation: - every operator keeps its grouping under Lean's own precedence: ``(a ^ b) + 1`` is ``(a_0 ^^^ b_0) + 1``, since Lean reads @@ -324,7 +325,7 @@ is ``Certified: f [backend=Lean] [vacuous]``, with a warning. Goals as hypotheses ~~~~~~~~~~~~~~~~~~~ -Next to each goal, ``Generated.lean`` states it as hypotheses and a +Next to each goal, its module states it as hypotheses and a conclusion. Each hypothesis is an assumption the goal makes, named by where it comes from, and a bridge from that form to the goal is proved in the same file. For this file: @@ -474,6 +475,7 @@ A goal it proves gets that proof, with a header that says so: automation: cppverify_auto 1 proves it with cppverify_auto_grind cppverify_auto proves this goal. cpp-verify rewrites this file only while it is unedited; a proof you write here is yours, kept as any other. -/ + import CppVerify.Goals.cppverify_next_e1e917 import CppVerify.User import CppVerify.Auto @@ -572,6 +574,104 @@ that cpp-verify 0.1 wrote for fn_5f5a3373697876::postcondition@8:37 is now CppVerify/Proofs/cppverify_six_6a2cf3/cppverify_six_6a2cf3_postcondition_198bc076.lean``. A 0.1 proof of a goal the source no longer has is kept in ``Stale/``. +One module of goals per function +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Each function's goals have a Lean module of their own, so that a change to +one function builds again only what depends on it. For this file: + +.. cppverify-example: flags --backend=lean --lean-project={dir}/proof + +.. code-block:: cpp + + cppverify::spec int tri(int n) + cppverify::decreases(n) + { + return n <= 0 ? 0 : tri(n - 1) + n; + } + + int inc(int x) + cppverify::pre(0 <= x && x < 1000) + cppverify::post(cppverify::result == x + 1) + { + return x + 1; + } + + int tri_zero() + cppverify::post(cppverify::result == tri(0)) + { + return 0; + } + +``cpp-verify --backend=lean --lean-project=proof file.cpp`` prints: + +.. code-block:: text + + Exported: decreases: tri (cppverify_auto proved 1 of 1 goals) + Exported: lean obligation: inc (cppverify_auto proved 3 of 3 goals) + Exported: lean obligation: tri_zero (cppverify_auto proved 1 of 2 goals) + +and writes: + +.. code-block:: text + + proof/ + lakefile.toml + lean-toolchain + CppVerify.lean the library's root, which imports Check + CppVerify/ + Prelude.lean the heap model, the comparisons, the bridge lemmas + Specs.lean each spec the goals apply, declared once + Goals/ + cppverify_tri_decreases_f55d4c.lean + cppverify_inc_c0810e.lean + cppverify_tri_zero_e086e9.lean + Generated.lean imports every goal module + Auto.lean cppverify_auto + User.lean your lemmas, never rewritten + Proofs/ + cppverify_inc_c0810e/ + cppverify_inc_c0810e_postcondition_e4ef4574.lean + ... + Check.lean imports every proof + +``Specs.lean`` declares each spec function the goals apply once, ``tri`` +here, as a function of which nothing is known +(``opaque cppSpec_fn_5f5a3374726969 : Int -> Int``). Each goal module imports +it and defines the bodies its goals unfold under its own prefix, as in +``cppSpecBody_e086e9ab_fn_5f5a3374726969_1``, so any goal modules can be +imported together. A proof imports its function's goals, your lemmas, and +the automation: + +.. code-block:: lean4 + + import CppVerify.Goals.cppverify_inc_c0810e + import CppVerify.User + import CppVerify.Auto + +A new ``User.lean`` imports ``CppVerify.Specs``, so a lemma there may speak +of the specs and of the prelude; a lemma about one function's goals belongs +in a module of yours that imports that function's goals. A ``User.lean`` of +an earlier release imports ``CppVerify.Generated``, which still imports every +goal module: its proofs keep working, but each then depends on every goal. + +A generated file is written only when its text changes, so exporting an +unchanged source writes nothing, and ``lake build`` or your editor builds +again only what a change reaches. Certification builds the generated +modules, ``User.lean``, and ``Auto.lean`` with Lake, then compiles each proof +file with admissions promoted to errors, unless nothing it is built from +changed since it last passed: its text and the compiled modules of the +project it imports. After a change to the postcondition of ``inc``, it +compiles again the goal module of ``inc``, ``Generated.lean``, and the three +proofs of ``inc``, and none of the others. + +A run writes the goal module of each function it exports, and removes any +other: a function you delete takes its module with it, and so does a +function that a ``--lean-fallback`` run leaves to its solver, since +``Specs.lean`` then declares only what the exported functions apply. The +proofs of such a function stay where they are, and build again once its +goals are exported again. + What certification checks ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -585,12 +685,14 @@ user's source. For each goal: 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 goal modules come 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; + ``G`` that its function's goal module defines; - the axioms it depends on, collected from the constants it uses, must be - among ``propext``, ``Quot.sound``, and ``Classical.choice``. + among ``propext``, ``Quot.sound``, and ``Classical.choice``; +- no declaration of ``User.lean`` may use ``sorry``: an admitted lemma there + fails every goal. Each function is certified on its own goals. For this file, where ``one`` claims a false postcondition: @@ -635,8 +737,8 @@ skips the kernel, is rejected at its replay (``the kernel rejects CppVerify.Lemmas: while replaying declaration 'cheat': (kernel) declaration 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 +cppverify_one_99bcee_postcondition_646d2761, which +CppVerify.Goals.cppverify_one_99bcee 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 e406b754bdee559b68b004f99990d31a23df2d06 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:11 +0530 Subject: [PATCH 35/80] docs: Describe the modules of a Lean project in the tooling reference. --- website/source/language/tooling.rst | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index a7082dc386..d2b8429c7b 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -286,7 +286,11 @@ Backends output uses one shared preamble and identity-qualified theorem names. * - ``--lean-project=DIR`` - With ``--backend=lean``, which it selects, generate a pinned editable project. Generated - semantics live in ``CppVerify/Generated.lean``; reusable lemmas and + semantics live in a module per function, ``CppVerify/Goals/.lean``, + with each spec they apply declared once in ``CppVerify/Specs.lean``; a + proof imports its function's module, so certification compiles again + only the proofs of a function whose goals changed, and a generated + file is written only when its text changes. Reusable lemmas and per-obligation proof files are preserved across regeneration. A goal is named by its function and the hash of its statement (``cppverify_one_99bcee_postcondition_cd6bdfcd``), and its proof file, From 0c43c5c4115afdba35f54292c5fcabe50ca2028c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:11 +0530 Subject: [PATCH 36/80] docs: Note the Lean module per function in the release notes. --- website/source/release-notes.rst | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index a9443338d7..60b91f1188 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -385,6 +385,20 @@ proofs side by side and checks them in one Lean environment: the 33 goals of one test took 204 s and now take 12 s (:doc:`book/part-ii/ch17-backends-modular-calls`). +**A Lean module per function.** A Lean project kept every goal of every +function in ``CppVerify/Generated.lean``, which every proof imported, so a +change to one function built every proof again, and certification compiled +every proof on every run. Each function's goals now have a module of their +own, ``CppVerify/Goals/.lean``, the specs they apply are declared +once, in ``CppVerify/Specs.lean``, and a proof imports its function's goals, +``User``, and ``Auto``. A generated file is written only when its text +changes, and certification compiles a proof again only when it or a module +it imports changed: after a change to one of five functions, it compiles +that function's three proofs. ``lake build``, which failed for want of the +library's root module, builds every proof. A ``User.lean`` that 0.1 wrote, +which imports ``CppVerify.Generated``, keeps working +(:doc:`book/part-ii/ch17-backends-modular-calls`). + **Lean 4.35.0.** Lean projects pin ``leanprover/lean4:v4.35.0``. A project 0.1 generated, pinned to ``v4.32.2``, moves to the new pin the next time cpp-verify writes it, with a warning; a proof that no longer builds needs updating for that From f2558ecf8d6dfef4f433ecc997541501d11a3c2f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:11 +0530 Subject: [PATCH 37/80] docs: Describe a Lean project's modules in the design. --- docs/DESIGN.md | 25 +++++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index bb4518e207..219ba08aad 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1913,7 +1913,16 @@ Lean's evaluation agrees with the certifier on random ground terms and on every operator at its extreme operands. Standalone output is an unchecked scratch-pad. Editable project mode pins Lean 4.35.0 (`LeanToolchain`), overwrites only generated semantics and the active check module, and preserves reusable user lemmas and one proof file -per goal. A goal is named by its function and its statement, never by a +per goal. The generated semantics are a module per function, +`CppVerify/Goals/.lean`, over one `CppVerify/Specs.lean` that +declares each spec the goals apply once, as Vermilion emits a unit per +function over one `Specs` file; each goal module defines the spec bodies its +goals unfold under the function's prefix. A proof imports its function's +goal module, the user's lemmas (`User.lean`, which a new project starts by +importing `Specs`), and `Auto`, so a change to one function builds again +only what imports its module. A file is written only when its text changes, +and a run writes the goal modules of the functions it exports and removes +every other, so that every module of the project builds. A goal is named by its function and its statement, never by a position: `cppverify__
__`, where `h6` hashes the function's identity (overloads) and `h8` begins the SHA-256 hash of the obligation's statement, its goal with the logical declarations it uses and @@ -1952,18 +1961,22 @@ any other; any other gets a stub that records the attempt and the revision of `cppverify_auto` that made it. A file is tried again only when no attempt by the current revision is recorded, and only while nobody has edited it. Initial generation is `Exported`. Certification -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 +holds against a proof author in bad faith. It builds the generated modules, +`User`, and `Auto` with Lake and compiles each proof file on its own with +`sorry` as an error, unless nothing it is built from changed since it last +built: its text and the compiled project modules it imports, by hash, since +Lake does not say which modules of a failed build are current. It 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 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, +the goal modules being replayed first; the proof's type is exactly the +constant of its goal, which its function's goal module 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 +`Classical.choice`. A declaration of `User.lean` that uses `sorry` fails +every goal. A function is `Certified` when every one of its goals passes, and a failing goal leaves only its own function `Unresolved`, with the obligation and the reason. Certification runs the pinned toolchain whatever elan's default is, and a project pinned by an earlier release moves to From a9899605f7ca6af32e310ded86bce27c884dd17b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:12 +0530 Subject: [PATCH 38/80] docs: Describe a Lean project's modules and proof keys in the architecture. --- docs/ARCHITECTURE.md | 95 ++++++++++++++++++++++++++++++-------------- 1 file changed, 65 insertions(+), 30 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 3dda2cbd89..98795dfc1c 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1627,6 +1627,25 @@ uses when the source around it changes. `Proofs/Goal_.lean`: reordering two postconditions gave each proof the other's goal, and inserting a function renamed the bodies every later proof used. +- **Modules.** The adapter writes a project's goals by group + (`LeanProjectModules`): the goals, readable forms, bridges, and spec + bodies of each function go to `CppVerify/Goals/.lean`, which + imports `CppVerify/Specs.lean`, where `emitLeanFunctionDeclarations` + declares each spec the run's modules apply once (`opaque + cppSpec_`). Two goal modules that declared one spec would clash + when imported together, and Lean 4.35's import keeps one of two differing + declarations without a word. The prelude is `CppVerify/Prelude.lean`, and + `CppVerify/Generated.lean` imports every goal module, so a `User.lean` of + 0.1, which imports it, still sees every goal. A proof imports its goal + module, `User` (which a new project starts with `import CppVerify.Specs`), + and `Auto` (which imports `Prelude`); `CppVerify.lean`, the library's + root, imports `Check`, so `lake build` builds every proof (before, the + library had no root and `lake build` failed). Every file is written only + when its text changes (`writeTextFileIfChanged`), and + `writeLeanProjectModules` removes every goal module the run did not + write: a fallback run rewrites `Specs` with the specs of the modules it + exports, and a module it kept from an earlier run failed (`Unknown + identifier cppSpec_...`). - **Records.** The exporter returns a `LeanProjectGoal` for every obligation of each module it exports, those a fallback selection leaves to the solver marked `Exported = false`, with the 0.1 names of the goal and @@ -1675,7 +1694,7 @@ uses when the source around it changes. `G.of_readable : G.readable → G` is a term, one prelude lemma per hypothesis (`cppverify_imp_or : (a → b) → ¬a ∨ b`, or `cppverify_not_imp_or : (¬a → b) → a ∨ b`), so the kernel checks with - `Generated.lean` that the readable form implies the goal: a printer bug in + the goal module that the readable form implies the goal: a printer bug in it fails the build, never certifies. `LeanProjectGoal::Intros` gives the stub its `intro` list. On the 375 suite exports, the 351 that built before still build, with every bridge. @@ -1699,8 +1718,8 @@ uses when the source around it changes. neither is a step. Heartbeats alone did not bound the time, since a kernel check is not counted. The trial takes every exported goal whose proof file is pristine and whose header (`automation:`) names no attempt by the - current `LeanAutomationRevision`, builds `User` and `Auto` with the pinned - toolchain, and runs `lean` itself (with the `LEAN_PATH` of `lake env`, so a + current `LeanAutomationRevision`, builds `Generated`, `User`, and `Auto` + with the pinned toolchain, and runs `lean` itself (with the `LEAN_PATH` of `lake env`, so a stopped process leaves no child) on a file of one theorem per goal, in `--jobs` chunks. Lean reports to a file, line by line: the step that proved each goal, then the axioms of its theorem or that the kernel @@ -1712,35 +1731,46 @@ uses when the source around it changes. the attempt. An export's `LeanAutomatic` counts its goals with automatic proofs. Without the toolchain nothing is tried. - **Certification** (`certifyLeanProject`) builds `Generated`, `User`, and - `Auto`, then each proof file with `lean -EhasSorry`, `--jobs` at once, - recording the goals whose proofs do not build, and runs the checker of + `Auto` with Lake, then each proof file with `lean -EhasSorry`, `--jobs` at + once, unless its key is unchanged (`leanProofKey`: SHA-256 of the + toolchain, the proof's text, and the bytes of the `.olean` of every project + module in its import closure, read from the `import` lines of their + sources; written to `.cppverify/built/` after a build, and removed + with the `.olean` before one). Lake cannot tell this itself: when a + dependency fails it names only the dependency, and a dependent's `.olean` + of an earlier build stays, so a proof the user broke would certify from + its old `.olean`. It records the goals whose proofs do not build and runs + the checker of `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 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 + change what it checks. It reads, from their compiled files, the goal + modules the goal list names, 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 goal modules 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.Goals. 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 its goal module were + replayed, `G_proof` is a theorem of type exactly `.const G []` with `G` a + definition of its goal module, and the axioms its kernel constants reach + are allowed; every goal fails when a declaration of `CppVerify.User` + depends on `sorryAx` (`userSorry`; before, `User` was compiled with `sorry` + an error); 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 @@ -1764,7 +1794,12 @@ unfinished lemma does not count, and `--no-lean-auto`. `lean_identity.test` walk reordering, renames of two functions at once, a changed statement, a removed function and its return, fallback runs, pruning, and a 0.1 project with proofs, stubs, and a proof of a goal that is gone) and certifies it after -the renames and the migration. +the renames and the migration. `lean_modules.test` checks the layout (a +spec declared once for two goal modules certified together, a proof's +imports, a new `User`), that a rerun writes no file, that a change to one +function compiles only its goal module, `Generated`, and its proofs again, +`lake build`, that a deleted function takes its module, a 0.1 `User.lean`, +and a fallback run that keeps no goal module. ## Counterexample Extraction From f178db1f30a334b614a39b78a7b98714ee0124e6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:12 +0530 Subject: [PATCH 39/80] test: Import its function's goal module in the proof cppverify_fine_52006a_missing_return_54ae7c80.lean. --- .../cppverify_fine_52006a_missing_return_54ae7c80.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_missing_return_54ae7c80.lean index 24d917ca90..53b4aee615 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fine_52006a import CppVerify.User theorem cppverify_fine_52006a_missing_return_54ae7c80_proof : cppverify_fine_52006a_missing_return_54ae7c80 := by From b138c4bb9bf5bdd9ac21af8d4eb9a2a64346aa64 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:12 +0530 Subject: [PATCH 40/80] test: Import its function's goal module in the proof cppverify_fine_52006a_postcondition_cd6bdfcd.lean. --- .../cppverify_fine_52006a_postcondition_cd6bdfcd.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_postcondition_cd6bdfcd.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_postcondition_cd6bdfcd.lean index 2d440f8a0e..415249b275 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_postcondition_cd6bdfcd.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_postcondition_cd6bdfcd.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fine_52006a import CppVerify.User theorem cppverify_fine_52006a_postcondition_cd6bdfcd_proof : cppverify_fine_52006a_postcondition_cd6bdfcd := by From 1bf5460d8e51968f7f477702c62f2c300565613c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:13 +0530 Subject: [PATCH 41/80] test: Import its function's goal module in the proof cppverify_one_99bcee_missing_return_54ae7c80.lean. --- .../cppverify_one_99bcee_missing_return_54ae7c80.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean index f7d3d1a1a7..c6061d122c 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_missing_return_54ae7c80_proof : cppverify_one_99bcee_missing_return_54ae7c80 := by From 77bdebb76f9dac56ba5dd98f113879dcf877c713 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:13 +0530 Subject: [PATCH 42/80] test: Import its function's goal module in the proof cppverify_one_99bcee_postcondition_646d2761.lean. --- .../hidden/cppverify_one_99bcee_postcondition_646d2761.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/hidden/cppverify_one_99bcee_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/hidden/cppverify_one_99bcee_postcondition_646d2761.lean index 823511abad..3ed1c6e593 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/hidden/cppverify_one_99bcee_postcondition_646d2761.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/hidden/cppverify_one_99bcee_postcondition_646d2761.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User /- An axiom behind a lemma. -/ From e0d4296270879b789dfd9b234d118680d370295c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:14 +0530 Subject: [PATCH 43/80] test: Import its function's goal module in the proof Lemmas.lean. --- .../suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean index 0897c5c20f..71e1a1f4ad 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User import Lean From 98d82b0059cdc9d6a60a8ba050a5f2c671a2f9bd Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:14 +0530 Subject: [PATCH 44/80] test: Import its function's goal module in the proof cppverify_one_99bcee_postcondition_646d2761.lean. --- .../rewritten/cppverify_one_99bcee_postcondition_646d2761.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/cppverify_one_99bcee_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/cppverify_one_99bcee_postcondition_646d2761.lean index f5ce026671..ed060924ed 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/cppverify_one_99bcee_postcondition_646d2761.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/cppverify_one_99bcee_postcondition_646d2761.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_postcondition_646d2761_proof : True := trivial From 71886e0fdaacc94fd4cea45c22422eb92671eaee Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:14 +0530 Subject: [PATCH 45/80] test: Import its function's goal module in the proof cppverify_one_99bcee_postcondition_646d2761.lean. --- .../unchecked/cppverify_one_99bcee_postcondition_646d2761.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/unchecked/cppverify_one_99bcee_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/unchecked/cppverify_one_99bcee_postcondition_646d2761.lean index 296d7e4797..0c477a9fa8 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/unchecked/cppverify_one_99bcee_postcondition_646d2761.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/unchecked/cppverify_one_99bcee_postcondition_646d2761.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User import Lean From aaf0ec7ffc36b15bfa7274b301a55cd0270c1733 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:15 +0530 Subject: [PATCH 46/80] test: Import its function's goal module in the proof lean_dependencies_impossible.lean. --- clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean index 391927a090..c2cb31fbe6 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_impossible_9d6c7c import CppVerify.User theorem cppverify_impossible_9d6c7c_postcondition_1cd35301_proof : cppverify_impossible_9d6c7c_postcondition_1cd35301 := by From 910acbeb6d209b683ddd6babc68949401a1836b4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:15 +0530 Subject: [PATCH 47/80] test: Import its function's goal module in the proof lean_dependencies_looping.lean. --- clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean index b07ce3c20e..4a74afae54 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_looping_3f4bd4 import CppVerify.User theorem cppverify_looping_3f4bd4_postcondition_d06fccd0_proof : cppverify_looping_3f4bd4_postcondition_d06fccd0 := by From 69d11773b5cbd1e6e38d15da70f328b86a431dcb Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:15 +0530 Subject: [PATCH 48/80] test: Import its function's goal module in the proof lean_dependencies_mixed.lean. --- clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean index 9df085a719..b6bbaa9d98 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_product_4751c3 import CppVerify.User theorem cppverify_product_4751c3_postcondition_c4d4674b_proof : From 6ce143542319211b101a66baba5f9d177aa3a8f0 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:16 +0530 Subject: [PATCH 49/80] test: Import its function's goal module in the proof lean_dependencies_positive.lean. --- clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean index 4a3c213156..5fd5c25e71 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_positive_fb6abf import CppVerify.User theorem cppverify_positive_fb6abf_postcondition_78bdd643_proof : cppverify_positive_fb6abf_postcondition_78bdd643 := by From d69832dc383c904ea28a032f29bd195d5fc78c28 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:16 +0530 Subject: [PATCH 50/80] test: Import its function's goal module in the proof lean_dependencies_same.lean. --- clang/test/Verify/suite/Inputs/lean_dependencies_same.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_same.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_same.lean index 5a8320c770..a663e3e6a1 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_same.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_same.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_same_9601c2 import CppVerify.User theorem cppverify_same_9601c2_postcondition_ce92acf8_proof : cppverify_same_9601c2_postcondition_ce92acf8 := by From 1d6af47cdb2b2847432b8a67ef458c5eb67cfe17 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:16 +0530 Subject: [PATCH 51/80] test: Import its function's goal module in the proof lean_dependencies_seven.lean. --- clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean index ae71525385..741439d952 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_seven_634ea3 import CppVerify.User theorem cppverify_seven_634ea3_postcondition_f0d135e6_proof : cppverify_seven_634ea3_postcondition_f0d135e6 := by From fad7045e6499a98707b90dbd55e7f4c8bbbf4a41 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:17 +0530 Subject: [PATCH 52/80] test: Import its function's goal module in the proof lean_dependencies_termination.lean. --- .../test/Verify/suite/Inputs/lean_dependencies_termination.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_termination.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_termination.lean index 86ffa0028e..ef58ba38cf 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_termination.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_termination.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_scaled_decreases_52d363 import CppVerify.User theorem cppverify_scaled_decreases_52d363_termination_3164b050_proof : cppverify_scaled_decreases_52d363_termination_3164b050 := by From 49a0e1f059213da58601b933baa2e78648255327 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:17 +0530 Subject: [PATCH 53/80] test: Import its function's goal module in the proof lean_dependencies_trusting.lean. --- clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean index 3fd338653d..d075683fb3 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_trusting_b6301a import CppVerify.User theorem cppverify_trusting_b6301a_postcondition_bafafdfb_proof : cppverify_trusting_b6301a_postcondition_bafafdfb := by From 23e010b75f6abc42577c2e5c59aab5e3e0f9bfb9 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:18 +0530 Subject: [PATCH 54/80] test: Import its function's goal module in the proof lean_fallback_goal_1.lean. --- clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean b/clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean index 8ba810ff34..1db8715a34 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fibo_step_624f01 import CppVerify.User theorem cppverify_fibo_step_624f01_missing_return_ba8abb90_proof : From 64c657077b34b58509a2e38feda2ad851351c9df Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:18 +0530 Subject: [PATCH 55/80] test: Import its function's goal module in the proof lean_fallback_goal_2.lean. --- clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean b/clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean index df65b45915..86bfafa577 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fibo_step_624f01 import CppVerify.User theorem cppverify_fibo_step_624f01_postcondition_559cb60a_proof : From cc18009b8d544da835e6890da39c6a6c5b01376e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:18 +0530 Subject: [PATCH 56/80] test: Import its function's goal module in the proof lean_fallback_goal_3.lean. --- clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean b/clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean index 55b9772bad..6ec932841d 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fibo_six_ec829a import CppVerify.User theorem cppverify_fibo_six_ec829a_missing_return_ba8abb90_proof : From ce46518fa66a885005f9b9e9f855b6fe95e170d8 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:19 +0530 Subject: [PATCH 57/80] test: Import its function's goal module in the proof lean_fallback_goal_4.lean. --- clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean b/clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean index 8ebf102ec4..df78e0c7ec 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fibo_six_ec829a import CppVerify.User theorem cppverify_fibo_six_ec829a_postcondition_30cd1b97_proof : From 8d1523beec00f36f20e6e3678d7b4ab0efc0d551 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:19 +0530 Subject: [PATCH 58/80] test: Import its function's goal module in the proof lean_fallback_partial_goal_1.lean. --- clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean b/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean index aa658e5ebc..9e7048ae1a 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_bump_ce87d1 import CppVerify.User theorem cppverify_bump_ce87d1_overflow_f5ee4d20_proof : From df334198eebbf9d6216ff899ca1fec9f20dd0265 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:19 +0530 Subject: [PATCH 59/80] test: Import its function's goal module in the proof lean_fallback_partial_goal_2.lean. --- clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean b/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean index 8d12720c5a..0218241f17 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_bump_ce87d1 import CppVerify.User theorem cppverify_bump_ce87d1_assertion_06404a7a_proof : From 2f1a00609dab0203a4bc914fbdca25e6e711b23a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:20 +0530 Subject: [PATCH 60/80] test: Import its function's goal module in the proof cppverify_bump_ce87d1_missing_return_ba8abb90.lean. --- .../cppverify_bump_ce87d1_missing_return_ba8abb90.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_bump_ce87d1_missing_return_ba8abb90.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_bump_ce87d1_missing_return_ba8abb90.lean index 145a149822..acb538820c 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_bump_ce87d1_missing_return_ba8abb90.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_bump_ce87d1_missing_return_ba8abb90.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_bump_ce87d1 import CppVerify.User theorem cppverify_bump_ce87d1_missing_return_ba8abb90_proof : From 5daf12111e51a806ae56113f9f29740cb36287e1 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:20 +0530 Subject: [PATCH 61/80] test: Import its function's goal module in the proof cppverify_one_99bcee_missing_return_54ae7c80.lean. --- .../cppverify_one_99bcee_missing_return_54ae7c80.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean index f9024c9662..9bece241a3 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_missing_return_54ae7c80_proof : From 16a8c939940dc985caa367840f256995e998b1e0 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:20 +0530 Subject: [PATCH 62/80] test: Import its function's goal module in the proof cppverify_one_99bcee_postcondition_cd6bdfcd.lean. --- .../cppverify_one_99bcee_postcondition_cd6bdfcd.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd.lean index eee644659e..58448ce153 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_postcondition_cd6bdfcd_proof : From 6be02b0978495205d898a97a1a542558b20a7dbb Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:21 +0530 Subject: [PATCH 63/80] test: Import its function's goal module in the proof cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean. --- .../cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean index 7f4b99e6d4..1f724407fa 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_postcondition_cd6bdfcd_2_proof : From ca6c465ecaf104d43a0db048bdb5cd8dff2fe100 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:21 +0530 Subject: [PATCH 64/80] test: Import its function's goal module in the proof cppverify_one_99bcee_postcondition_ebbe6a6a.lean. --- .../cppverify_one_99bcee_postcondition_ebbe6a6a.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_ebbe6a6a.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_ebbe6a6a.lean index 5b4dde2b95..b09560a383 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_ebbe6a6a.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_ebbe6a6a.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_postcondition_ebbe6a6a_proof : From 7b861cb2f2f376f3b5f9d94962b716b15fa9ed14 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:22 +0530 Subject: [PATCH 65/80] test: Import its function's goal module in the proof cppverify_six_6a2cf3_missing_return_54ae7c80.lean. --- .../cppverify_six_6a2cf3_missing_return_54ae7c80.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_missing_return_54ae7c80.lean index f3ca2db1f1..8fdce88ad3 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_six_6a2cf3 import CppVerify.User theorem cppverify_six_6a2cf3_missing_return_54ae7c80_proof : From 5eedfdf9c605a7dc273d83a7086208d0c9827bd4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:22 +0530 Subject: [PATCH 66/80] test: Import its function's goal module in the proof cppverify_six_6a2cf3_postcondition_198bc076.lean. --- .../cppverify_six_6a2cf3_postcondition_198bc076.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_postcondition_198bc076.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_postcondition_198bc076.lean index 3dae61ac78..0d1c2b271c 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_postcondition_198bc076.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_postcondition_198bc076.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_six_6a2cf3 import CppVerify.User theorem cppverify_six_6a2cf3_postcondition_198bc076_proof : From c318e4c86c6eed8af4c610ca86bcdb199ed8c853 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:22 +0530 Subject: [PATCH 67/80] test: Import its function's goal module in the proof cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean. --- .../cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean index 9f5bed9a7f..05952c73c6 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_tri_decreases_f55d4c import CppVerify.User theorem cppverify_tri_decreases_f55d4c_termination_3c6bb93f_proof : From 201ea08d254d10ee216cf72e595d218c564f4b70 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:23 +0530 Subject: [PATCH 68/80] test: Import its function's goal module in the proof cppverify_twice_edf933_missing_return_54ae7c80.lean. --- .../cppverify_twice_edf933_missing_return_54ae7c80.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean index d450f13548..18f468999d 100644 --- a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_twice_edf933 import CppVerify.User theorem cppverify_twice_edf933_missing_return_54ae7c80_proof : cppverify_twice_edf933_missing_return_54ae7c80 := by From 9bacf87068a15d7b66ddd16d6e53889774d3aca9 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:23 +0530 Subject: [PATCH 69/80] test: Import its function's goal module in the proof cppverify_twice_edf933_postcondition_28de726e.lean. --- .../cppverify_twice_edf933_postcondition_28de726e.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean index e1080ebc94..11440c7bf0 100644 --- a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_twice_edf933 import CppVerify.User theorem cppverify_twice_edf933_postcondition_28de726e_proof : cppverify_twice_edf933_postcondition_28de726e := by From 451f38fe9868fee7b346ddc8aadd7f363f1ede99 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:23 +0530 Subject: [PATCH 70/80] test: Import its function's goal module in the proof cppverify_twice_edf933_precondition_51b3c1f0.lean. --- .../cppverify_twice_edf933_precondition_51b3c1f0.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean index 5c6b0e43e4..30d1e5cc82 100644 --- a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_twice_edf933 import CppVerify.User theorem cppverify_twice_edf933_precondition_51b3c1f0_proof : cppverify_twice_edf933_precondition_51b3c1f0 := by From 05003b5300d550eeabf7e6da1caf390f76f860d8 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:24 +0530 Subject: [PATCH 71/80] test: Import its function's goal module in the proof cppverify_twice_edf933_precondition_f0a3d715.lean. --- .../cppverify_twice_edf933_precondition_f0a3d715.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean index 2607fff7eb..9b2059d45a 100644 --- a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_twice_edf933 import CppVerify.User theorem cppverify_twice_edf933_precondition_f0a3d715_proof : cppverify_twice_edf933_precondition_f0a3d715 := by From 93b75ad137b25646627b3c56c5f0ddad0d8a30cc Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:24 +0530 Subject: [PATCH 72/80] test: Import its function's goal module in the proof lean_semantics_call.lean. --- clang/test/Verify/suite/Inputs/lean_semantics_call.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_semantics_call.lean b/clang/test/Verify/suite/Inputs/lean_semantics_call.lean index 8dc0f46fa3..5df905de2c 100644 --- a/clang/test/Verify/suite/Inputs/lean_semantics_call.lean +++ b/clang/test/Verify/suite/Inputs/lean_semantics_call.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_small_74ff94 import CppVerify.User theorem cppverify_small_74ff94_precondition_4e324fa2_proof : From d49e8f9625aa4f6ff51bfc7a031d6b5020a9a254 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:24 +0530 Subject: [PATCH 73/80] test: Import its function's goal module in the proof lean_semantics_mix.lean. --- clang/test/Verify/suite/Inputs/lean_semantics_mix.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_semantics_mix.lean b/clang/test/Verify/suite/Inputs/lean_semantics_mix.lean index 4c46c601c2..623902f5cf 100644 --- a/clang/test/Verify/suite/Inputs/lean_semantics_mix.lean +++ b/clang/test/Verify/suite/Inputs/lean_semantics_mix.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_mix_b839ab import CppVerify.User theorem cppverify_mix_b839ab_assertion_255467f3_proof : From 1136d88661c58f48d674b8d02dcf63aa38d1c951 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 06:50:25 +0530 Subject: [PATCH 74/80] test: Import its function's goal module in the proof lean_semantics_numerals.lean. --- clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean b/clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean index 5142c33706..96e97fd298 100644 --- a/clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean +++ b/clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_difference_465d5b import CppVerify.User theorem cppverify_difference_465d5b_assertion_d7e0e821_proof : From 9359c25e7403528271106f9fbac530623a9d5662 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 18:35:40 +0530 Subject: [PATCH 75/80] test: Import its function's goal module in the proof cppverify_reading_8d7035_division_by_zero_df06c970.lean. --- .../cppverify_reading_8d7035_division_by_zero_df06c970.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_division_by_zero_df06c970.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_division_by_zero_df06c970.lean index daf2ade742..6002daa66b 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_division_by_zero_df06c970.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_division_by_zero_df06c970.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_reading_8d7035 import CppVerify.User theorem cppverify_reading_8d7035_division_by_zero_df06c970_proof : cppverify_reading_8d7035_division_by_zero_df06c970 := by From cf3fc2c9752e4bfb6da719321559845e066ad7e9 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 18:35:40 +0530 Subject: [PATCH 76/80] test: Import its function's goal module in the proof cppverify_reading_8d7035_missing_return_54ae7c80.lean. --- .../cppverify_reading_8d7035_missing_return_54ae7c80.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_missing_return_54ae7c80.lean index 7bb7dd4b6b..8a10f2476c 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_reading_8d7035 import CppVerify.User theorem cppverify_reading_8d7035_missing_return_54ae7c80_proof : cppverify_reading_8d7035_missing_return_54ae7c80 := by From 1e8a0a14f1aae7eec49e1246e1ba6315c45c9ae7 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 18:35:41 +0530 Subject: [PATCH 77/80] test: Import its function's goal module in the proof cppverify_reading_8d7035_postcondition_54ae7c80.lean. --- .../cppverify_reading_8d7035_postcondition_54ae7c80.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_postcondition_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_postcondition_54ae7c80.lean index 97d154cc3c..b99f29c9e1 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_postcondition_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_postcondition_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_reading_8d7035 import CppVerify.User theorem cppverify_reading_8d7035_postcondition_54ae7c80_proof : cppverify_reading_8d7035_postcondition_54ae7c80 := by From 4eb310f89959d312267b05181ca167fcb08ee50c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 18:35:41 +0530 Subject: [PATCH 78/80] test: Import its function's goal module in the proof cppverify_reading_8d7035_precondition_155ffe95.lean. --- .../cppverify_reading_8d7035_precondition_155ffe95.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_155ffe95.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_155ffe95.lean index d8692c5599..df12dae878 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_155ffe95.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_155ffe95.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_reading_8d7035 import CppVerify.User theorem cppverify_reading_8d7035_precondition_155ffe95_proof : cppverify_reading_8d7035_precondition_155ffe95 := by From 9b346cc5723c659a9c0c70fe74ce943e9e3fc24d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 18:35:41 +0530 Subject: [PATCH 79/80] test: Import its function's goal module in the proof cppverify_reading_8d7035_precondition_814bc5b2.lean. --- .../cppverify_reading_8d7035_precondition_814bc5b2.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_814bc5b2.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_814bc5b2.lean index 5779536cb6..589c770d90 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_814bc5b2.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_814bc5b2.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_reading_8d7035 import CppVerify.User theorem cppverify_reading_8d7035_precondition_814bc5b2_proof : cppverify_reading_8d7035_precondition_814bc5b2 := by From 04706a910e770bf4eaa1aa0cfda25d69e07979e8 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 18:35:41 +0530 Subject: [PATCH 80/80] test: Import its function's goal module in the proof cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean. --- ...pverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean index 8e3effb2e7..8d4ca35013 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_sensor_contract_eb6f5c import CppVerify.User theorem cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d_proof : cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d := by