feat: add well-founded Repeat type for verified repeat/while loops

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`.

Key changes:
- `src/Init/Repeat.lean`: `Repeat` type, `Repeat.Rel` step relation,
  `Repeat.forIn` using `extrinsicFix`, and override macro expanding
  `repeat` to `Repeat.mk` (replacing the `Loop.mk` fallback)
- `backward.do.while` option (default `false`): when `true`, reverts to
  legacy `Loop.mk` behavior
- Builtin do-element elaborator dispatching based on `backward.do.while`
- `Spec.forIn_repeat`: `@[spec]` theorem enabling `mvcgen` verification
  of `repeat`/`while` loops with user-supplied variant and invariant
- `WPAdequacy` class linking `MonadAttach.CanReturn` with WP proofs
- `MonadAttach` instances for `BaseAsync`/`EAsync`
- Test with verified `sqrt` function proving correctness via `mvcgen`

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

src/Init.lean

@@ -40,6 +40,7 @@ public import Init.Grind
 public import Init.GrindInstances
 public import Init.Sym
 public import Init.While
+public import Init.Repeat
 public import Init.Syntax
 public import Init.Internal
 public import Init.Try

src/Init/Repeat.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Init.Core
+public import Init.Control.MonadAttach
+public import Init.WFExtrinsicFix
+import Init.While
+
+set_option linter.missingDocs true
+
+@[expose] public section
+
+namespace Lean
+
+/-!
+# Well-founded `Repeat` type for verified `repeat`/`while` loops
+
+This module provides a `Repeat` type that serves as an alternative to `Loop` for `repeat`/`while`
+loops. Unlike `Loop`, which uses `partial` recursion, `Repeat` is implemented using
+`WellFounded.extrinsicFix` and `MonadAttach`, enabling verified reasoning about loop programs.
+-/
+
+/-- A type for `repeat`/`while` loops that supports well-founded reasoning via `extrinsicFix`. -/
+inductive Repeat where
+  /-- Creates a `Repeat` value. -/
+  | mk
+
+/--
+The step relation for well-founded recursion in `Repeat.forIn`.
+Relates `b'` to `b` when `f () b` can plausibly return `ForInStep.yield b'`,
+as witnessed by `MonadAttach.CanReturn`.
+-/
+def Repeat.IsPlausibleStep {β : Type u} {m : Type u → Type v} [Monad m] [MonadAttach m]
+    (f : Unit → β → m (ForInStep β)) : β → β → Prop :=
+  fun b' b => MonadAttach.CanReturn (f () b) (ForInStep.yield b')
+
+/-- Iterates the body `f` using well-founded recursion via `extrinsicFix`. -/
+@[inline]
+def Repeat.forIn {β : Type u} {m : Type u → Type v} [Monad m] [MonadAttach m]
+    (_ : Repeat) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
+  haveI : Nonempty β := ⟨init⟩
+  WellFounded.extrinsicFix (Repeat.IsPlausibleStep f) (a := init) fun b recur => do
+    match ← MonadAttach.attach (f () b) with
+      | ⟨ForInStep.done b, _⟩ => pure b
+      | ⟨ForInStep.yield b, h⟩ => recur b h
+
+instance [Monad m] [MonadAttach m] : ForIn m Repeat Unit where
+  forIn := Repeat.forIn
+
+/-- Override the bootstrapping `repeat` macro from `Init.While` to use `Repeat.mk` instead of
+`Loop.mk`. When the builtin do-element elaborator for `repeat` is available (`backward.do.while`
+option dispatch), this macro defers to it by throwing `unsupportedSyntax`. -/
+macro_rules
+  | `(doElem| repeat $seq) => do
+    if ← Macro.hasDecl `Lean.Elab.Do.elabDoRepeat then
+      Lean.Macro.throwUnsupported
+    `(doElem| for _ in Repeat.mk do $seq)
+
+end Lean

src/Init/While.lean

@@ -32,8 +32,11 @@ partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop
 instance [Monad m] : ForIn m Loop Unit where
   forIn := Loop.forIn
 
-syntax "repeat " doSeq : doElem
+syntax (name := doRepeat) "repeat " doSeq : doElem
 
+/-- Bootstrapping fallback macro for `repeat`.
+Expands to `for _ in Loop.mk do ...`. Overridden by the macro in `Init.Repeat` after
+bootstrapping. -/
 macro_rules
   | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)
 

src/Lean/Elab/BuiltinDo.lean

@@ -15,3 +15,4 @@ public import Lean.Elab.BuiltinDo.Jump
 public import Lean.Elab.BuiltinDo.Misc
 public import Lean.Elab.BuiltinDo.For
 public import Lean.Elab.BuiltinDo.TryCatch
+public import Lean.Elab.BuiltinDo.Repeat

src/Lean/Elab/BuiltinDo/Repeat.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Lean.Elab.BuiltinDo.Basic
+meta import Lean.Parser.Do
+import Lean.Elab.BuiltinDo.For
+import Lean.Elab.Do.Switch
+
+public section
+
+namespace Lean.Elab.Do
+
+open Lean.Parser.Term
+
+/--
+Builtin do-element elaborator for `repeat` (syntax kind `Lean.doRepeat`).
+
+When `backward.do.while` is `true`, expands to `for _ in Loop.mk do ...` (legacy behavior).
+When `backward.do.while` is `false` (default), expands to `for _ in Repeat.mk do ...`
+(well-founded behavior).
+-/
+@[builtin_doElem_elab Lean.doRepeat] def elabDoRepeat : DoElab := fun stx dec => do
+  let `(doElem| repeat $seq) := stx | throwUnsupportedSyntax
+  let expanded ←
+    if Term.backward.do.while.get (← getOptions) then
+      `(doElem| for _ in Loop.mk do $seq)
+    else
+      `(doElem| for _ in Repeat.mk do $seq)
+  Term.withMacroExpansion stx expanded <|
+    withRef expanded <| elabDoElem ⟨expanded⟩ dec
+
+end Lean.Elab.Do

src/Lean/Elab/Do/Legacy.lean

@@ -1780,6 +1780,10 @@ mutual
             doIfToCode doElem doElems
           else if k == ``Parser.Term.doUnless then
             doUnlessToCode doElem doElems
+          else if k == `Lean.doRepeat then
+            let seq := doElem[1]
+            let expanded ← `(doElem| for _ in Loop.mk do $seq)
+            doSeqToCode (expanded :: doElems)
           else if k == ``Parser.Term.doFor then withFreshMacroScope do
             doForToCode doElem doElems
           else if k == ``Parser.Term.doMatch then

src/Lean/Elab/Do/Switch.lean

@@ -19,6 +19,11 @@ register_builtin_option backward.do.legacy : Bool := {
   descr    := "Use the legacy `do` elaborator instead of the new, extensible implementation."
 }
 
+register_builtin_option backward.do.while : Bool := {
+  defValue := false
+  descr    := "Use the legacy partial `Loop` type for `repeat`/`while` loops instead of the well-founded `Repeat` type. Useful as a workaround when the monad lacks a `MonadAttach` instance."
+}
+
 private def toDoElem (newKind : SyntaxNodeKind) : Macro := fun stx => do
   let stx := stx.setKind newKind
   withRef stx `(do $(⟨stx⟩):doElem)

src/Std/Do/SPred/Laws.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Std.Do.SPred.Notation
+import Init.PropLemmas
 
 @[expose] public section
 
@@ -157,3 +158,17 @@ theorem imp_curry {P Q : SVal.StateTuple σs → Prop} : (SVal.curry (fun t =>
   induction σs
   case nil => rfl
   case cons σ σs ih => intro s; simp only [imp_cons, SVal.curry_cons]; exact ih
+
+/-! # Prop-indexed quantifiers -/
+
+/-- Simplifies an existential over a true proposition. -/
+theorem exists_prop_of_true {p : Prop} (h : p) {P : p → SPred σs} : spred(∃ (h : p), P h) = P h := by
+  induction σs with
+  | nil => ext; exact _root_.exists_prop_of_true h
+  | cons σ σs ih => ext; exact ih
+
+/-- Simplifies a universal over a true proposition. -/
+theorem forall_prop_of_true {p : Prop} (h : p) {P : p → SPred σs} : spred(∀ (h : p), P h) = P h := by
+  induction σs with
+  | nil => ext; exact _root_.forall_prop_of_true h
+  | cons σ σs ih => ext; exact ih

src/Std/Do/Triple/RepeatSpec.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Std.Do.Triple.SpecLemmas
+import Std.Tactic.Do.Syntax
+
+set_option linter.missingDocs true
+
+@[expose] public section
+
+namespace Std.Do
+
+/-!
+# Specification theorem for `Repeat` loops
+
+This file contains the `@[spec]` theorem for `forIn` over `Lean.Repeat`, which enables
+verified reasoning about `repeat`/`while` loops using `mvcgen`.
+-/
+
+set_option mvcgen.warning false
+
+section
+
+variable {β : Type u} {m : Type u → Type v} {ps : PostShape.{u}}
+variable [Monad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] [WPMonad m ps]
+
+/--
+Specification for `forIn` over a `Lean.Repeat` value.
+Takes a variant (termination measure), an invariant, a proof that the variant decreases,
+and a proof that each step preserves the invariant.
+-/
+@[spec]
+theorem Spec.forIn_repeat
+    {l : _root_.Lean.Repeat} {init : β} {f : Unit → β → m (ForInStep β)}
+    (_variant : RepeatVariant β)
+    (inv : RepeatInvariant β ps)
+    (hwf : WellFounded (_root_.Lean.Repeat.IsPlausibleStep f))
+    (step : ∀ b,
+      Triple
+        (f () b)
+        (inv.1 (.repeat b))
+        (fun r => match r with
+          | .yield b' => inv.1 (.repeat b')
+          | .done b' => inv.1 (.done b'), inv.2)) :
+    Triple (forIn l init f) (inv.1 (.repeat init)) (fun b => inv.1 (.done b), inv.2) := by
+  change Triple (_root_.Lean.Repeat.forIn l init f) _ _
+  simp only [_root_.Lean.Repeat.forIn, WellFounded.extrinsicFix_eq_fix hwf]
+  induction hwf.apply init with
+  | intro b hacc ih =>
+  rw [WellFounded.fix_eq]
+  mvcgen [step, ih]
+  rename_i stp
+  apply SPred.forall_intro
+  intro _
+  cases stp <;> mvcgen [ih]
+
+end
+
+end Std.Do

src/Std/Do/Triple/SpecLemmas.lean

@@ -10,6 +10,8 @@ public import Std.Do.Triple.Basic
 public import Init.Data.Range.Polymorphic.Iterators
 import Init.Data.Range.Polymorphic
 public import Init.Data.Slice.Array
+public import Std.Do.WP.Adequacy
+public import Init.Repeat
 
 -- This public import is a workaround for #10652.
 -- Without it, adding the `spec` attribute for `instMonadLiftTOfMonadLift` will fail.
@@ -2188,3 +2190,90 @@ theorem Spec.forIn_stringSlice
       next => apply Triple.pure; simp
       next b => simp [ih _ _ hsp.next]
   | endPos => simpa using Triple.pure _ (by simp)
+
+/-!
+# Repeat loop specification infrastructure
+-/
+
+/--
+Cursor type for `Repeat` loop invariants.
+Represents either a loop iteration in progress or a completed loop.
+-/
+inductive RepeatCursor (β : Type u) where
+  /-- The loop is in progress with the current accumulator state `s`. -/
+  | «repeat» (s : β) : RepeatCursor β
+  /-- The loop has finished with the final accumulator state `s`. -/
+  | done (s : β) : RepeatCursor β
+
+/--
+An invariant for a `Repeat` loop. A postcondition over `RepeatCursor β` capturing both
+the in-progress and completed states.
+-/
+@[spec_invariant_type]
+abbrev RepeatInvariant (β : Type u) (ps : PostShape.{u}) := PostCond (RepeatCursor β) ps
+
+/--
+A variant (termination measure) for a `Repeat` loop.
+Maps the accumulator state to a natural number that decreases with each iteration.
+-/
+@[spec_invariant_type]
+abbrev RepeatVariant (β : Type u) := β → Nat
+
+section
+
+variable {α : Type u₁} {m : Type u₁ → Type v} {ps : PostShape.{u₁}}
+variable [Monad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] [WPMonad m ps]
+
+/--
+Specification for `MonadAttach.attach`: the precondition is the weakest precondition of `x` with
+a postcondition that universally quantifies over the `CanReturn` proof.
+-/
+@[spec]
+theorem Spec.attach
+    {x : m α} {Q : PostCond (Subtype (MonadAttach.CanReturn x)) ps} :
+    ⦃ wp⟦x⟧ ⟨fun a => spred(∀ (h : MonadAttach.CanReturn x a), Q.1 ⟨a, h⟩), Q.2⟩ ⦄ MonadAttach.attach x ⦃Q⦄ := by
+  apply Triple.iff.mpr
+  conv in wp x => rw [← WeaklyLawfulMonadAttach.map_attach (x := x)]
+  simp only [WPMonad.wp_map]
+  -- Goal: (Subtype.val <$> wp (attach x)).apply ⟨..., Q.2⟩ ⊢ₛ (wp (attach x)).apply Q
+  -- Rewrite LHS using apply_Functor_map
+  rw [PredTrans.apply_Functor_map]
+  -- Now both sides have (wp (attach x)).apply, use mono
+  apply (wp (MonadAttach.attach x)).mono
+  constructor
+  · intro ⟨a, h⟩
+    dsimp only []
+    rw [SPred.forall_prop_of_true h]
+  · dsimp only []
+    exact ExceptConds.entails.refl _
+
+end
+
+section
+
+variable {β : Type u₁} {m : Type u₁ → Type v} {ps : PostShape.{u₁}}
+variable [Monad m] [MonadAttach m] [WPAdequacy m ps]
+
+/--
+Derives well-foundedness of `_root_.Lean.Repeat.IsPlausibleStep f` from a WP proof that every
+step decreases a measure.
+-/
+theorem _root_.Lean.Repeat.IsPlausibleStep.wf_of_wp_measure {f : Unit → β → m (ForInStep β)}
+    (measure : β → Nat)
+    (h : ∀ b, ⦃⌜True⌝⦄ f () b ⦃⇓ step => ⌜∀ b', step = .yield b' → measure b' < measure b⌝⦄)
+    : WellFounded (_root_.Lean.Repeat.IsPlausibleStep f) := by
+  apply Subrelation.wf ?_ (_root_.measure measure).wf
+  intro b' b hstep
+  simp_wf
+  simp [_root_.Lean.Repeat.IsPlausibleStep] at hstep
+  have h' : ⊢ₛ wp⟦f () b⟧ (⇓? step => ⌜∀ b', step = .yield b' → measure b' < measure b⌝) := by
+    apply SPred.entails.trans (Triple.iff.mp (h b))
+    apply (wp (f () b)).mono
+    simp [PostCond.entails]
+  exact WPAdequacy.adequate
+    (m := m) (ps := ps) (x := f () b)
+    (P := fun step => ∀ b', step = .yield b' → measure b' < measure b)
+    h' (.yield b') hstep b' rfl
+
+end
+

src/Std/Do/WP.lean

@@ -9,5 +9,6 @@ prelude
 public import Std.Do.WP.Basic
 public import Std.Do.WP.Monad
 public import Std.Do.WP.SimpLemmas
+public import Std.Do.WP.Adequacy
 
 set_option linter.missingDocs true

src/Std/Do/WP/Adequacy.lean

@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Std.Do.WP.Monad
+import Init.Control.MonadAttach
+
+@[expose] public section
+
+set_option linter.missingDocs true
+
+/-!
+# WP Adequacy
+
+This module provides a small adequacy principle: a `mayThrow` postcondition is enough to recover
+facts about values that `MonadAttach` says can actually be returned.
+-/
+
+namespace Std.Do
+
+/-- A small adequacy principle: a `mayThrow` postcondition is enough to recover facts about
+values that `MonadAttach` says can actually be returned. -/
+class WPAdequacy (m : Type u → Type v) (ps : outParam PostShape.{u}) [Monad m] [MonadAttach m]
+    extends WP m ps where
+  /-- If the weakest precondition says that `P` holds for all return values, then `P` holds for
+  any value that `MonadAttach.CanReturn` says can be returned. -/
+  adequate {α : Type u} {x : m α} {P : α → Prop} :
+    (⊢ₛ wp⟦x⟧ (⇓? a => ⌜P a⌝)) → ∀ a, MonadAttach.CanReturn x a → P a
+
+instance : WPAdequacy Id .pure where
+  adequate := by
+    intro α x P hwp a hret
+    have hx : P x.run := by
+      simpa [WP.wp] using hwp
+    simpa [MonadAttach.CanReturn] using (hret ▸ hx)
+
+instance [Monad m] [MonadAttach m] [WPAdequacy m ps] :
+    WPAdequacy (StateT σ m) (.arg σ ps) where
+  adequate := by
+    intro α x P hwp a hret
+    rcases hret with ⟨s, s', hret⟩
+    have hwp' : ⊢ₛ wp⟦x.run s⟧ (⇓? r => ⌜P r.1⌝) := hwp s
+    exact WPAdequacy.adequate (m := m) (ps := ps) (x := x.run s) (P := fun r => P r.1) hwp' (a, s') hret
+
+instance [Monad m] [MonadAttach m] [WPAdequacy m ps] :
+    WPAdequacy (ReaderT ρ m) (.arg ρ ps) where
+  adequate := by
+    intro α x P hwp a hret
+    rcases hret with ⟨r, hret⟩
+    have hwp' : ⊢ₛ wp⟦x.run r⟧ (⇓? a => ⌜P a⌝) := hwp r
+    exact WPAdequacy.adequate (m := m) (ps := ps) (x := x.run r) (P := P) hwp' a hret
+
+instance [Monad m] [MonadAttach m] [WPAdequacy m .pure] :
+    WPAdequacy (ExceptT ε m) (.except ε .pure) where
+  adequate := by
+    intro α x P hwp a hret
+    have hwp0 := hwp
+    simp only [WP.wp, PredTrans.apply_pushExcept, ExceptConds.fst_true, ExceptConds.snd_true] at hwp0
+    have hwp' : ⊢ₛ wp⟦x.run⟧ (⇓? r => ⌜match r with | .ok a => P a | .error _ => True⌝) := by
+      apply SPred.entails.trans hwp0
+      apply (wp x.run).mono
+      simp [PostCond.entails]
+      intro r <;> cases r <;> simp
+    exact WPAdequacy.adequate (m := m) (ps := .pure) (x := x.run)
+      (P := fun r => match r with | .ok a => P a | .error _ => True) hwp' (.ok a) hret
+
+instance [Monad m] [MonadAttach m] [WPAdequacy m .pure] :
+    WPAdequacy (OptionT m) (.except PUnit .pure) where
+  adequate := by
+    intro α x P hwp a hret
+    have hwp0 := hwp
+    simp only [WP.wp, PredTrans.apply_pushOption, ExceptConds.fst_true, ExceptConds.snd_true] at hwp0
+    have hwp' : ⊢ₛ wp⟦x.run⟧ (⇓? r => ⌜match r with | some a => P a | none => True⌝) := by
+      apply SPred.entails.trans hwp0
+      apply (wp x.run).mono
+      simp [PostCond.entails]
+      intro r <;> cases r <;> simp
+    exact WPAdequacy.adequate (m := m) (ps := .pure) (x := x.run)
+      (P := fun r => match r with | some a => P a | none => True) hwp' (some a) hret
+
+end Std.Do

src/Std/Internal/Async/Basic.lean

@@ -487,6 +487,8 @@ instance : Monad BaseAsync where
   pure := BaseAsync.pure
   bind := BaseAsync.bind
 
+instance : MonadAttach BaseAsync := .trivial
+
 instance : MonadLift BaseIO BaseAsync where
   monadLift := BaseAsync.lift
 
@@ -707,6 +709,8 @@ instance : Monad (EAsync ε) where
   pure := EAsync.pure
   bind := EAsync.bind
 
+instance : MonadAttach (EAsync ε) := .trivial
+
 instance : MonadLift (EIO ε) (EAsync ε) where
   monadLift := EAsync.lift
 

src/Std/Tactic/Do.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Std.Tactic.Do.ProofMode
 public import Std.Tactic.Do.Syntax
+public import Std.Do.Triple.RepeatSpec
 
 @[expose] public section
 

tests/elab/repeat_extrinsic.lean

@@ -0,0 +1,89 @@
+module
+
+import Std
+
+set_option mvcgen.warning false
+
+open Std.Do
+
+/-!
+# Tests for extrinsic `repeat`/`while` loops
+
+These tests verify that the new `Repeat` type and its verification infrastructure work correctly.
+-/
+
+/-- `sqrt n` computes the integer square root of `n` using a `while` loop. -/
+def sqrt (n : Nat) : Id Nat := do
+  if n = 0 then
+    return 0
+  let mut i := 0
+  while i * i ≤ n
+  do
+    i := i + 1
+  return i - 1
+
+/-- The `sqrt` function returns the correct integer square root. -/
+theorem sqrt_correct :
+    ⦃⌜True⌝⦄ sqrt n ⦃⇓ res => ⌜res * res ≤ n ∧ n < (res + 1) * (res+1)⌝⦄ := by
+  mvcgen [sqrt]
+  invariants
+  | inv1 => fun i => (n + 2) - i
+  | inv2 => ⇓ cursor => match cursor with
+    | .repeat i => ⌜∀ j, j < i → j * j ≤ n⌝
+    | .done i => ⌜(∀ j, j < i → j * j ≤ n) ∧ n < i * i⌝
+  with (try grind)
+  | vc2 =>
+    apply Lean.Repeat.IsPlausibleStep.wf_of_wp_measure (fun i => (n + 2) - i)
+    intro r
+    mvcgen with try grind
+    | vc1 hsqr =>
+      have : r ≤ n := Nat.le_trans (Nat.le_mul_self r) hsqr
+      grind
+  | vc3 =>
+    rename_i b hsqr _ hinv
+    intro j hj
+    rcases Nat.lt_or_eq_of_le (Nat.lt_succ_iff.mp hj) with hlt | rfl
+    · exact hinv j hlt
+    · exact hsqr
+  | vc6 res h =>
+    have : res - 1 < res := by grind
+    grind
+
+set_option backward.do.while true in
+/-- Test: `backward.do.while true` should expand to `Loop.mk`. -/
+def loopBackwardCompat (n : Nat) : Nat := Id.run do
+  let mut i := 0
+  repeat
+    if i < n then
+      i := i + 1
+    else
+      break
+  return i
+
+-- Verify the backward-compat loop computes correctly
+#guard loopBackwardCompat 5 == 5
+#guard loopBackwardCompat 0 == 0
+
+/-- Test: default setting should expand to `Repeat.mk`. -/
+def loopDefault (n : Nat) : Nat := Id.run do
+  let mut i := 0
+  repeat
+    if i < n then
+      i := i + 1
+    else
+      break
+  return i
+
+-- Verify the default loop computes correctly
+#guard loopDefault 5 == 5
+#guard loopDefault 0 == 0
+
+-- Verify sqrt computes correctly
+#guard Id.run (sqrt 0) == 0
+#guard Id.run (sqrt 1) == 1
+#guard Id.run (sqrt 4) == 2
+#guard Id.run (sqrt 8) == 2
+#guard Id.run (sqrt 9) == 3
+#guard Id.run (sqrt 15) == 3
+#guard Id.run (sqrt 16) == 4
+#guard Id.run (sqrt 100) == 10