fix: rank a vcgen call's unfoldings below a named or starred spec

src/Lean/Elab/Tactic/Do/Attr.lean

@@ -352,11 +352,13 @@ instance : BEq SpecTheorem where
 
 abbrev SpecEntry := SpecTheorem
 
-/-- Priority for a spec named explicitly in a `vcgen [...]` argument list. -/
-def explicitSpecPrio : Nat := eval_prio high + 20
-
+-- Call-site priority bands, all above `@[spec high]`, ordered named > `*` > unfold.
+/-- Priority for a spec named in a `vcgen [...]` argument list. -/
+def explicitSpecPrio : Nat := eval_prio high + 3000
 /-- Priority for a local hypothesis pulled into `vcgen`'s spec set by `*`. -/
-def starSpecPrio : Nat := eval_prio high + 10
+def starSpecPrio : Nat := eval_prio high + 2000
+/-- Priority for the equational and unfold specs a bracketed definition in a `vcgen [...]` list contributes. -/
+def unfoldSpecPrio : Nat := eval_prio high + 1000
 
 structure SpecTheorems where
   specs : DiscrTree SpecTheorem := DiscrTree.empty

src/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.lean

@@ -102,7 +102,7 @@ public def addSimpSpecs (database : SpecTheorems) (simpThms : SimpTheorems) :
   -- entry; feed both back to `simpSpecTheorems` as the `SimpEntry`s the definition would produce.
   let entries := simpThms.post.values.map (SimpEntry.thm ·)
     ++ simpThms.toUnfold.toList.toArray.map (SimpEntry.toUnfold ·)
-  for newSpec in ← simpSpecTheorems entries explicitSpecPrio do
+  for newSpec in ← simpSpecTheorems entries unfoldSpecPrio do
     specs := Sym.insertPattern specs newSpec.pattern newSpec
   return { specs, erased }
 

tests/elab/vcgenAmbientLocalSpec.lean

@@ -2,15 +2,18 @@ import Std.Internal.Do
 import Std.Tactic.Do
 
 /-! `vcgen` ranks the specs available at a call site into priority bands: a spec named in the
-`vcgen [...]` list outranks a local hypothesis pulled in by `*`, which outranks a spec collected
-from an ambient hypothesis. The call-site bands sit just above `high`, so an `@[spec high]` used to
-outrank default specs does not shadow a call-site spec, while a priority above the band still does.
+`vcgen [...]` list outranks a local hypothesis pulled in by `*`, which outranks a bracketed
+definition's unfolding, which outranks a spec collected from an ambient hypothesis. The call-site
+bands sit just above `high`, so an `@[spec high]` used to outrank default specs does not shadow a
+call-site spec, while a priority above the band still does.
 
 `viaBinder`, `viaHave`, and `viaStar` prove one goal three ways, checking that a named spec wins over
 the ambient spec collected from the same hypothesis. `namedBeatsSpec`, `specHighLoses`, and
 `specHighestWins` isolate the banding against `@[spec]`, `@[spec high]`, and a priority above the band.
 `unfoldBeatsSpec` checks that a bracketed definition is unfolded ahead of a lossy `@[spec]` keyed on
-the same program, including when the program's state type is a variable.
+the same program, including when the program's state type is a variable. `namedStopBeatsUnfold` and
+`starStopBeatsUnfold` check that a spec for the definition, named or pulled by `*`, outranks its
+unfolding at a recursive call.
 -/
 
 open Std.Internal.Do Lean.Order
@@ -94,7 +97,7 @@ theorem termBeatsSpecHigh (hNamed : ⦃ fun _ => True ⦄ leaf ⦃ fun r _ => r
     ⦃ fun _ => True ⦄ leaf ⦃ fun r _ => r = 7 ⦄ := by
   vcgen [show ⦃ fun _ => True ⦄ leaf ⦃ fun r _ => r = 7 ⦄ from hNamed] <;> grind
 
-@[spec high + 30] axiom leaf_above : ⦃ fun _ => True ⦄ leaf ⦃ fun r _ => r = 7 ⦄
+@[spec high + 3001] axiom leaf_above : ⦃ fun _ => True ⦄ leaf ⦃ fun r _ => r = 7 ⦄
 
 -- A priority above the call-site band still overrides a named local.
 theorem specHighestWins (hNamed : ⦃ fun _ => True ⦄ leaf ⦃ fun _ _ => True ⦄) :
@@ -116,3 +119,21 @@ theorem unfoldBeatsSpec {σ : Type} (a : σ) :
     ⦃ fun s => s.1 = a ⦄ (bumpSnd : StateM (σ × Nat) Nat) ⦃ fun _ s => s.1 = a ⦄ := by
   fail_if_success (vcgen <;> grind)
   vcgen [bumpSnd] <;> grind
+
+-- `tail` is bracketed to unfold, and the named `hstop` outranks its unfolding at the recursive call.
+theorem namedStopBeatsUnfold (b : Nat) (rest : List Char) (f : Nat)
+    (hItem : ⦃ fun s => s = enc b ++ rest ⦄ item f ⦃ fun r s => r = b ∧ s = rest ⦄)
+    (hstop : ∀ acc, ⦃ fun s => s = rest ⦄ tail f acc ⦃ fun r s => r = acc ∧ s = rest ⦄) :
+    ∀ acc, ⦃ fun s => s = '+' :: (enc b ++ rest) ⦄ tail (f + 1) acc
+      ⦃ fun r s => r = acc + b ∧ s = rest ⦄ := by
+  intro acc
+  vcgen [tail, hItem, hstop] <;> grind
+
+-- As `namedStopBeatsUnfold`, but the spec is pulled by `*`; its band still outranks the unfolding.
+theorem starStopBeatsUnfold (b : Nat) (rest : List Char) (f : Nat)
+    (hItem : ⦃ fun s => s = enc b ++ rest ⦄ item f ⦃ fun r s => r = b ∧ s = rest ⦄)
+    (hstop : ∀ acc, ⦃ fun s => s = rest ⦄ tail f acc ⦃ fun r s => r = acc ∧ s = rest ⦄) :
+    ∀ acc, ⦃ fun s => s = '+' :: (enc b ++ rest) ⦄ tail (f + 1) acc
+      ⦃ fun r s => r = acc + b ∧ s = rest ⦄ := by
+  intro acc
+  vcgen [tail, *] <;> grind