feat: verifiable repeat/while loops

[sgraf812]

This PR introduces Lean.Repeat, a well-founded alternative to Lean.Loop for repeat/while loops. Unlike Loop, which uses partial recursion (making loop bodies opaque to the proof system), Repeat is implemented using WellFounded.extrinsicFix and MonadAttach, enabling compositional verification of loop programs via mvcgen.

When the new behavior is active (default), repeat/while loops expand to for _ in Repeat.mk do ... instead of for _ in Loop.mk do .... The backward.do.while option (default false) reverts to the legacy Loop.mk behavior.

New files:

• src/Init/Repeat.lean: Repeat type, Repeat.Rel step relation, Repeat.forIn using extrinsicFix, and override macro
• src/Lean/Elab/BuiltinDo/Repeat.lean: builtin do-element elaborator dispatching on backward.do.while
• src/Std/Do/WP/Adequacy.lean: WPAdequacy class linking MonadAttach.CanReturn with WP proofs
• src/Std/Do/Triple/RepeatSpec.lean: @[spec] theorem Spec.forIn_repeat for mvcgen
• tests/elab/repeat_extrinsic.lean: verified sqrt example and option tests

Modified files add supporting infrastructure: backward.do.while option registration, legacy elaborator support, SPred lemmas (exists_prop_of_true, forall_prop_of_true), spec lemmas (Spec.attach, Repeat.Rel.of_wp, RepeatCursor/RepeatInvariant/RepeatVariant types), and MonadAttach instances for BaseAsync/EAsync.

🤖 Generated with Claude Code

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a88f81bc28bc93561a48cb47a8d00dfd6d2599d0 --onto 4786e082dca22873d14d2a5b9b7c8843380c6e78. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-31 13:28:31)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a88f81bc28bc93561a48cb47a8d00dfd6d2599d0 --onto fc0cf68539ad3b481a1802414c22c44506519c9d. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-02 11:32:12)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a88f81bc28bc93561a48cb47a8d00dfd6d2599d0 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-31 13:28:33)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a88f81bc28bc93561a48cb47a8d00dfd6d2599d0 --onto 861bc19e0c1c45b5766cc5c9ef0488568368b236. You can force reference manual CI using the force-manual-ci label. (2026-04-02 11:32:13)

[Rob23oba]

Some food for thought; There are some variants of repeat verification that we might want to see:

-- 1. loop only terminates when the initial value satisfies some invariant (here `i ≤ x`)
-- We basically get this one for free by swapping out `extrinsicFix` for `partialExtrinsicFix`
def loopWithTerminationPrecond (x : Nat) : Id Nat := do
  let mut i := 0
  while i ≠ x do
    i := i + 1
  return i

example : (loopWithTerminationPrecond x).run = x := by sorry

-- 2. loop only terminates when the initial *state* satisfies some invariant (here `(← get) ≤ x`)
-- I'm not quite sure how to tackle this one...
def loopWithStatefulTerminationPrecond (x : Nat) : StateM Nat Nat := do
  set 0
  while (← get) ≠ x do
    modify fun i => i + 1
  get

example : (loopWithStatefulTerminationPrecond x).run' state = x := by sorry

-- 3. loop may not terminate; but we are in `Option`
-- similar to 1. but this time we want non-termination to provide meaningful output (i.e. `none`)
-- in this case it's enough to take the unique fixpoint of `fun cont : Nat → Option Nat => if x ≠ 20 then cont (x + 1) else pure x`
def possiblyDivergentLoop (x : Nat) : Option Nat := do
  let mut x := x
  while x ≠ 20 do
    x := x + 1
  return x

example : possiblyDivergentLoop x = some n → n = 20 ∧ x ≤ n := by sorry

inductive SpecialM (α : Type) where
  | ok (val : α)
  | error (err : String)
  | diverge

instance : Monad SpecialM where
  pure := .ok
  bind
    | .ok val, f => f val
    | .error err, _ => .error err
    | .diverge, _ => .diverge

-- ... setting up more instances for `SpecialM`

-- 4. loop may not terminate; but we have a special monad
-- similar to 3. but just requiring a fixpoint is not enough
-- since `error` and `diverge` are not distinguishable just from the `Monad` instance
def specialDivergence (x : Nat) : SpecialM Nat := do
  let mut x := x
  while x ≠ 20 do
    x := x + 1
  return x

example : specialDivergence 21 = .diverge := by sorry

Possibly an idea would be a special MonadRepeat class (mostly interesting for case 4.) or a stronger form of MonadAttach (mostly interesting for case 2.).

[sgraf812]

@Rob23oba although the PR body doesn't reflect it yet, I followed through on an idea by @datokrat and rebased the entire approach on partial_fixpoint. The upside is that this approach is less restrictive to monads (more monads possible, fewer hardcoded assumptions about what are postconditions) and allows for the more expressive stateful measures you requested, see the test case 🎉 The downside is that partial_fixpoint is a bit magical to me and certainly a bit remote from the actual runtime semantics. Still, I think a reasonable definition of Totality for deterministic monads is possible as

def Total {β : Type u} {m : Type u → Type v} {ps} [Nonempty β] [Monad m] [WP m ps] (body : Unit → β → m (ForInStep β)) :=
  ∃ (f : β → β), ∀ [MonoBindRight m] b,
  ⦃⌜True⌝⦄ Repeat.forIn b body ⦃⇓ r => ⌜f b = r⌝⦄

[datokrat]

Very optional suggestion: We could call it MonadTail or something, emphasizing that the continuation is a tail call and making it sound less similar to the propositional MonoBind?

[sgraf812]

Yes, I thought about that a bit as well. Maybe we can even generalize the theorem a bit because I don't think the property is much related to PartialOrder at all... Very roughly, something like

  preserves {a : m α} {f₁ f₂ : α → m β} {R : m β → m β → Prop} (h : ∀ x, R (f₁ x) (f₂ x)) : R (a >>= f₁) (a >>= f₂)

should hold (for certain R); it reeks of parametricity/logical relations. But perhaps the exact details are too complicated to work out and the ad-hoc thing is OK for now.

Anyway, all on board with MonadTail. Waiting for Claude quota...

[Rob23oba]

Hmm what about extrinsic partial_fixpoint?

@[specialize]
partial def Lean.Order.opaqueFix {α : Sort u} [Lean.Order.CCPO α] (f : α → α) : α :=
  f (opaqueFix f)

open scoped Classical in
@[implemented_by opaqueFix]
def Lean.Order.extrinsicFix {α : Sort u} [Lean.Order.CCPO α] (f : α → α) : α :=
  if h : monotone f then
    fix f h
  else
    opaqueFix f

@[inline, always_inline]
def Repeat.forIn {β : Type u} {m : Type u → Type v}
    [Monad m] [Lean.Order.CCPO (m β)] (b : β) (f : Unit → β → m (ForInStep β)) : m β :=
  Lean.Order.extrinsicFix (α := (b : β) → m β) (b := b) fun cont b => do
    match ← f () b with
    | .done val => pure val
    | .yield val => cont val

One advantage of that is that we can also apply it where we don't have a proof of monotonicity (i.e. bind_mono_right). Also, we can trivially expand it to the new forIn:

@[inline, always_inline]
def repeatNew {m : Type u → Type v} [Lean.Order.CCPO (m α)] (f : (cont : σ → m α) → σ → m α)
    (init : σ) : m α :=
  Lean.Order.extrinsicFix f init

Edit: Also, just to mention, I think partial_fixpoint alone addresses all four examples I've provided; with this extrinsic variant we should also be able to fix the problem with BaseAsync and others. Maybe a raw Lean.Order.CCPO is not the best idea though; what about splitting into MonadTail (which just supplies the CCPO) and LawfulMonadTail (which supplies the monotonicity proof)?