test: speed up vcgen_get_throw_set.lean by partially evaluating specs (#12670)

This PR speeds up the vcgen_get_throw_set benchmark by a factor of 4 by
partially evaluating specs.

tests/bench/mvcgen/sym/vcgen_get_throw_set.lean

@@ -9,18 +9,35 @@ import Driver
 
 open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
 
-@[spec]
-theorem Spec.monadLift_ExceptT [Monad m] [WPMonad m ps] {x : m α} :
-    ⦃wp⟦x⟧ (Q.1, Q.2.2)⦄ monadLift (n := ExceptT ε m) x ⦃Q⦄ := by
-  simp [Triple.iff, monadLift, MonadLift.monadLift, MonadLiftT.monadLift, ExceptT.lift, wp]
+set_option mvcgen.warning false
 
-def step (lim : Nat) : ExceptT String (StateM Nat) Unit := do
+abbrev M := ExceptT String <| StateM Nat
+
+-- We partially evaluate a couple of specs for best performance.
+-- If you comment those out, you will see a 4x slowdown.
+
+@[spec high]
+theorem Spec.throw_M {e : String} :
+    ⦃Q.2.1 e⦄ throw (m := M) e ⦃Q⦄ := by
+  mvcgen
+
+@[spec high]
+theorem Spec.set_M {s : Nat} :
+    ⦃fun _ => Q.1 ⟨⟩ s⦄ set (m := M) s ⦃Q⦄ := by
+  mvcgen
+
+@[spec high]
+theorem Spec.get_M :
+    ⦃fun s => Q.1 s s⦄ get (m := M) ⦃Q⦄ := by
+  mvcgen
+
+def step (lim : Nat) : M Unit := do
   let s ← get
   if s > lim then
     throw "s is too large"
   set (s + 1)
 
-def loop (n : Nat) : ExceptT String (StateM Nat) Unit := do
+def loop (n : Nat) : M Unit := do
   match n with
   | 0 => pure ()
   | n+1 => loop n; step n
@@ -30,13 +47,6 @@ def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = 0⌝⦄ loop n ⦃⇓_ s => ⌜s
 set_option maxRecDepth 10000
 set_option maxHeartbeats 10000000
 
-/-
-example : Goal 20 := by
-  simp only [Goal, loop, step]
-  mvcgen'
-  all_goals sorry
--/
-
 #eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry)
   [100, 500, 1000]
   -- [1000]