From bb8d8da1afa0f67db2eb10a34f323d72abdb0a8e Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Tue, 24 Feb 2026 14:19:15 +0100
Subject: [PATCH] test: add benchmark vcgen_reader_state (#12671)

This PR adds the benchmark vcgen_reader_state that is a variant of
vcgen_add_sub_cancel that takes the value to subtract from a `ReaderT`
layer. Measurements:
```
goal_100: 201 ms, 1 VCs by sorry: 0 ms, kernel: 52 ms
goal_500: 382 ms, 1 VCs by sorry: 0 ms, kernel: 327 ms
goal_1000: 674 ms, 1 VCs by sorry: 1 ms, kernel: 741 ms
```
Which suggests it scales linearly. The generated VC triggers superlinear
behavior in `grind`, though, hence it is discharged by `sorry`.
---
 tests/bench/mvcgen/sym/lakefile.lean          |  3 +-
 .../bench/mvcgen/sym/vcgen_reader_state.lean  | 56 +++++++++++++++++++
 2 files changed, 58 insertions(+), 1 deletion(-)
 create mode 100644 tests/bench/mvcgen/sym/vcgen_reader_state.lean

diff --git a/tests/bench/mvcgen/sym/lakefile.lean b/tests/bench/mvcgen/sym/lakefile.lean
index c81badd4f2..4c3a2ea47c 100644
--- a/tests/bench/mvcgen/sym/lakefile.lean
+++ b/tests/bench/mvcgen/sym/lakefile.lean
@@ -15,7 +15,8 @@ lean_lib Driver where
 
 @[default_target]
 lean_lib VCGenBench where
-  roots := #[`vcgen_add_sub_cancel, `vcgen_deep_add_sub_cancel, `vcgen_get_throw_set]
+  roots := #[`vcgen_add_sub_cancel, `vcgen_deep_add_sub_cancel, `vcgen_get_throw_set,
+             `vcgen_reader_state]
   moreLeanArgs := #["--tstack=100000000"]
 
 @[default_target]
diff --git a/tests/bench/mvcgen/sym/vcgen_reader_state.lean b/tests/bench/mvcgen/sym/vcgen_reader_state.lean
new file mode 100644
index 0000000000..575ed487cd
--- /dev/null
+++ b/tests/bench/mvcgen/sym/vcgen_reader_state.lean
@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+import Lean
+import VCGen
+import Driver
+
+open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
+
+set_option mvcgen.warning false
+
+/-!
+A variant of the `vcgen_add_sub_cancel` benchmark, but reading the value to subtract from `ReaderT`.
+-/
+
+abbrev M := ReaderT Nat <| StateM Nat
+
+-- Partially evaluated specs for best performance.
+
+@[spec high]
+theorem Spec.M_read :
+    ⦃fun r s => Q.fst r r s⦄ read (m := M) ⦃Q⦄ := by
+  mvcgen
+
+@[spec high]
+theorem Spec.M_get :
+    ⦃fun r s => Q.fst s r s⦄ get (m := M) ⦃Q⦄ := by
+  mvcgen
+
+@[spec high]
+theorem Spec.M_set (n : Nat) :
+    ⦃fun r _ => Q.fst () r n⦄ set (m := M) n ⦃Q⦄ := by
+  mvcgen
+
+def step : M Unit := do
+  let r ← read
+  let s ← get
+  set (s + r)
+  let s ← get
+  set (s - r)
+
+def loop (n : Nat) : M Unit := do
+  match n with
+  | 0 => pure ()
+  | n+1 => step; loop n
+
+def Goal (n : Nat) : Prop := ∀ post, ⦃post⦄ loop n ⦃⇓_ => post⦄
+
+set_option maxRecDepth 10000
+set_option maxHeartbeats 10000000
+
+#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry) -- grind scales superlinearly here
+  [100, 500, 1000]
+  -- [1000]