From d2176cb5fb729fbef487ac61cb962af2afe57064 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= <wojciech@lean-fro.org>
Date: Fri, 6 Feb 2026 11:41:03 +0000
Subject: [PATCH] test: add tests and benchmarks for `cbv` tactic (#12345)

This PR adds two benchmarks (sieve of Eratosthenes, removing duplicates
from the list) and one test (a function with sublinear complexity
defined via well-founded recursion evaluated on large naturals with up
to `60` digits).

The tests have been suggested by @b-mehta.
---
 tests/bench/cbv/dedup.lean               | 16 ++++++++++
 tests/bench/cbv/divisors.lean            | 30 +++++++++++++++++++
 tests/bench/speedcenter.exec.velcom.yaml | 12 ++++++++
 tests/lean/run/cbv2.lean                 | 38 ++++++++++++++++++++++++
 4 files changed, 96 insertions(+)
 create mode 100644 tests/bench/cbv/dedup.lean
 create mode 100644 tests/bench/cbv/divisors.lean
 create mode 100644 tests/lean/run/cbv2.lean

diff --git a/tests/bench/cbv/dedup.lean b/tests/bench/cbv/dedup.lean
new file mode 100644
index 0000000000..4c188f5488
--- /dev/null
+++ b/tests/bench/cbv/dedup.lean
@@ -0,0 +1,16 @@
+import Std
+set_option cbv.warning false
+
+def dedup (l : List Nat) : List Nat := Id.run do
+  let mut S : Std.TreeSet Nat := ∅
+  for i in l do
+    S := S.insert i
+  return S.toList
+
+example : dedup [1] = [1] := by conv => lhs; cbv
+
+example : dedup [1,2] = [1,2] := by conv => lhs; cbv
+
+example : dedup [1,1] = [1] := by conv => lhs; cbv
+
+example : dedup [1,2,2] = [1,2] := by conv => lhs; cbv
diff --git a/tests/bench/cbv/divisors.lean b/tests/bench/cbv/divisors.lean
new file mode 100644
index 0000000000..c67476e209
--- /dev/null
+++ b/tests/bench/cbv/divisors.lean
@@ -0,0 +1,30 @@
+import Lean
+open Lean
+
+def divisorsList (n : Nat) : List Nat :=
+  (List.range' 1 n).filter fun d => n % d = 0
+
+def mkProblem (n : Nat) : Expr := mkApp (mkConst ``divisorsList) (mkNatLit n)
+
+def runProblem (n : Nat) : MetaM Unit := do
+  let problem := mkProblem n
+  let startTime ← IO.monoNanosNow
+  let executed ← Lean.Meta.Tactic.Cbv.cbvEntry problem
+  let endTime ← IO.monoNanosNow
+  let ms := (endTime - startTime).toFloat / 1000000.0
+  match executed with
+  | .rfl _ => IO.println s!"goal_{n}: {ms} ms"
+  | .step _ proof _ =>
+    let startTime ← IO.monoNanosNow
+    Meta.checkWithKernel proof
+    let endTime ← IO.monoNanosNow
+    let kernelMs := (endTime - startTime).toFloat / 1000000.0
+    IO.println s!"cbv: goal_{n}: {ms} ms, kernel: {kernelMs} ms"
+
+def runCbvTests : MetaM Unit := do
+  IO.println "=== Call-By-Value Tactic Tests ==="
+  IO.println ""
+  for n in List.range 200 do
+    runProblem n
+
+#eval runCbvTests
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
index 7799b63b8c..197b1eadcc 100644
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -671,3 +671,15 @@
   run_config:
     <<: *time
     cmd: lean ./cbv/leroy.lean
+- attributes:
+    description: cbv tactic (Eratosthenes' sieve)
+    tags: [other]
+  run_config:
+    <<: *time
+    cmd: lean ./cbv/divisors.lean
+- attributes:
+    description: cbv tactic (removing duplicates from the list)
+    tags: [other]
+  run_config:
+    <<: *time
+    cmd: lean ./cbv/dedup.lean
diff --git a/tests/lean/run/cbv2.lean b/tests/lean/run/cbv2.lean
new file mode 100644
index 0000000000..3a8102c9ae
--- /dev/null
+++ b/tests/lean/run/cbv2.lean
@@ -0,0 +1,38 @@
+set_option cbv.warning false
+
+def popcount : Nat → Nat
+| 0 => 0
+| 1 => 1
+| n@(_+2) => if n % 2 = 0 then popcount (n / 2) else popcount (n / 2) + 1
+termination_by n => n
+
+/--
+error: Tactic `decide` failed for proposition
+  popcount 123498203491224398 = 32
+because its `Decidable` instance
+  instDecidableEqNat (popcount 123498203491224398) 32
+did not reduce to `isTrue` or `isFalse`.
+
+After unfolding the instances `instDecidableEqNat` and `Nat.decEq`, reduction got stuck at the `Decidable` instance
+  match h : (popcount 123498203491224398).beq 32 with
+  | true => isTrue ⋯
+  | false => isFalse ⋯
+-/
+#guard_msgs in
+example : popcount 123498203491224398 = 32 := by decide
+
+example : popcount 123498203491224398 = 32 := by conv => lhs; cbv
+
+example : popcount 1234982034912243981 = 30 := by conv => lhs; cbv
+
+example : popcount 1234982034912243981523 = 35 := by conv => lhs; cbv
+
+example : popcount 12349820349122439815231238 = 42 := by conv => lhs; cbv
+
+example : popcount 12349820349122439815231238098123 = 49 := by conv => lhs; cbv
+
+example : popcount 1234982034912243981523123809812323 = 65 := by conv => lhs; cbv
+
+example : popcount 1234982034912243981523123809812323982928213984812309234 = 101 := by conv => lhs; cbv
+
+example : popcount 1234982034912243981523123809812323982928213984812309234213989 = 84 := by conv => lhs; cbv