verify: Replay a Lean project into one kernel environment, importing the toolchain once

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";
 

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;
+}

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

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)

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)

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

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