Pin that selected verification calls back through a plain function

tests/test_lean_sources.py

@@ -8,6 +8,7 @@
 import stat
 import subprocess
 import sys
+import types
 from collections.abc import Callable
 from pathlib import Path
 
@@ -1505,6 +1506,31 @@ def counting_lookup(descriptor: int, name: str, relative: str) -> os.stat_result
     assert [frames_at_level[level + 1] - frames_at_level[level] for level in range(4)] == [3, 3, 3, 3]
 
 
+def test_selected_verification_calls_back_through_a_plain_function(
+    tmp_path: Path,
+    monkeypatch: pytest.MonkeyPatch,
+) -> None:
+    # A C-implemented callback such as functools.partial adds no Python frame,
+    # so the frame count above misses it, but it spends CPython's separate C
+    # recursion budget at every folder level of verification.
+    _require_descriptor_capture()
+    (tmp_path / "d").mkdir()
+    (tmp_path / "d" / "Deep.lean").write_text("def deep : Nat := 0\n")
+    callbacks: list[type] = []
+    recheck = tree_snapshot_module._recheck_scanned_directory
+
+    def recording_recheck(*args: object, **kwargs: object) -> object:
+        if kwargs.get("verify_kept") is not None:
+            callbacks.append(type(kwargs["verify_kept"]))
+        return recheck(*args, **kwargs)
+
+    monkeypatch.setattr(tree_snapshot_module, "_recheck_scanned_directory", recording_recheck)
+
+    snapshot_project_sources(tmp_path)
+
+    assert callbacks and set(callbacks) == {types.FunctionType}
+
+
 @pytest.mark.parametrize(
     ("relative", "directory"),
     [("Project/Secret.lean", False), ("Project/Private", True)],