diff --git a/Parser.lean b/Parser.lean
index 44c3621..9f34a82 100644
--- a/Parser.lean
+++ b/Parser.lean
@@ -6,6 +6,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 import Parser.Basic
 import Parser.Char
 import Parser.Error
+import Parser.Iterators
 import Parser.Parser
 import Parser.Prelude
 import Parser.RegEx
diff --git a/Parser/Basic.lean b/Parser/Basic.lean
index 75d7d12..ecf969d 100644
--- a/Parser/Basic.lean
+++ b/Parser/Basic.lean
@@ -127,15 +127,23 @@ def test (p : ParserT ε σ τ m α) : ParserT ε σ τ m Bool :=
 
 /-! ### `foldr` -/
 
-/-- `foldr f p q` -/
+/-- `foldr f p q` folds `f` from right to left, parsing `p` repeatedly until it fails, then
+finishing with `q`. Terminates via well-founded recursion on `Stream.remaining`. -/
 @[inline]
-partial def foldr (f : α → β → β) (p : ParserT ε σ τ m α) (q : ParserT ε σ τ m β) :
-  ParserT ε σ τ m β :=
-  try
-    let x ← withBacktracking p
-    let y ← foldr f p q
-    return f x y
-  catch _ => q
+def foldr (f : α → β → β) (p : ParserT ε σ τ m α) (q : ParserT ε σ τ m β) :
+  ParserT ε σ τ m β := do
+  go (← getStream)
+where
+  go (s₀ : σ) : ParserT ε σ τ m β := do
+    try
+      let x ← withBacktracking p
+      let s₁ ← getStream
+      if _h : Stream.remaining s₁ < Stream.remaining s₀ then
+        return f x (← go s₁)
+      else
+        return f x (← q)
+    catch _ => q
+  termination_by Stream.remaining s₀
 
 /-! ### `take` family -/
 
@@ -194,15 +202,22 @@ def takeManyN (n : Nat) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array
 array of returned values of `p` and the output of `stop`. If `p` fails before `stop` is encountered,
 the error from `p` is reported and no input is consumed.
 -/
-partial def takeUntil (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) :
+def takeUntil (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) :
   ParserT ε σ τ m (Array α × β) :=
-  have := Inhabited.mk do return ((#[] : Array α), (← stop))
-  withBacktracking do rest #[]
+  withBacktracking do
+    rest (← getStream) #[]
 where
-  rest [Inhabited (ParserT ε σ τ m (Array α × β))] (acc : Array α) := do
+  rest (s₀ : σ) (acc : Array α) : ParserT ε σ τ m (Array α × β) := do
     match ← option? stop with
     | some y => return (acc, y)
-    | none => rest <| acc.push (← p)
+    | none =>
+      let x ← p
+      let s₁ ← getStream
+      if _h : Stream.remaining s₁ < Stream.remaining s₀ then
+        rest s₁ (acc.push x)
+      else
+        return (acc.push x, ← stop)
+  termination_by Stream.remaining s₀
 
 /-! ### `drop` family -/
 
@@ -236,6 +251,26 @@ all outputs.
 def dropMany (p : ParserT ε σ τ m α) : ParserT ε σ τ m PUnit :=
   foldl (Function.const α) .unit p
 
+/--
+One-step unfolding of `dropMany` for `m = Id`.
+
+Applies `foldl_eq` with `f = Function.const α` and `init = PUnit.unit`.
+Since `Function.const α PUnit.unit x = PUnit.unit` for all `x`, the
+recursive call is simply `dropMany p s'`.
+-/
+theorem dropMany_eq (p : Parser ε σ τ α) (s : σ) :
+    (dropMany p : Parser ε σ τ _) s =
+      match p s with
+      | .ok s' _ =>
+        if _h : Stream.remaining s' < Stream.remaining s then
+          (dropMany p : Parser ε σ τ _) s'
+        else .ok s' PUnit.unit
+      | .error s' _ =>
+        .ok (Stream.setPosition s' (Stream.getPosition s)) PUnit.unit := by
+  show (foldl (Function.const α) PUnit.unit p) s = _
+  rw [foldl_eq]; simp only [Function.const]
+  cases hp : p s <;> rfl
+
 /--
 `dropMany1 p` parses one or more occurrences of `p` (with backtracking) until it fails, ignoring
 all outputs.
@@ -256,13 +291,21 @@ def dropManyN (n : Nat) (p : ParserT ε σ τ m α) : ParserT ε σ τ m PUnit :
 outputs from `p`. If `p` fails before encountering `stop` then the error from  `p` is reported
 and no input is consumed.
 -/
-partial def dropUntil (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m β :=
-  withBacktracking loop
+def dropUntil (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m β :=
+  withBacktracking do
+    loop (← getStream)
 where
-  loop := do
+  loop (s₀ : σ) : ParserT ε σ τ m β := do
     match ← option? stop with
-    | some s => return s
-    | none => p *> loop
+    | some y => return y
+    | none =>
+      let _ ← p
+      let s₁ ← getStream
+      if _h : Stream.remaining s₁ < Stream.remaining s₀ then
+        loop s₁
+      else
+        stop
+  termination_by Stream.remaining s₀
 
 /-! `count` family -/
 
@@ -271,9 +314,29 @@ where
 successes.
 -/
 @[inline]
-partial def count (p : ParserT ε σ τ m α) : ParserT ε σ τ m Nat :=
+def count (p : ParserT ε σ τ m α) : ParserT ε σ τ m Nat :=
   foldl (fun n _ => n+1) 0 p
 
+/--
+One-step unfolding of `count` for `m = Id`.
+
+Applies `foldl_eq` with `f = fun n _ => n+1` and `init = 0`.
+After one successful parse, the accumulator is 1, so the recursive call
+uses `foldl (fun n _ => n+1) 1 p`.
+-/
+theorem count_eq (p : Parser ε σ τ α) (s : σ) :
+    (count p : Parser ε σ τ _) s =
+      match p s with
+      | .ok s' _ =>
+        if _h : Stream.remaining s' < Stream.remaining s then
+          (foldl (fun n (_ : α) => n+1) 1 p : Parser ε σ τ _) s'
+        else .ok s' 1
+      | .error s' _ =>
+        .ok (Stream.setPosition s' (Stream.getPosition s)) 0 := by
+  show (foldl (fun n (_ : α) => n + 1) 0 p) s = _
+  rw [foldl_eq]; simp only [Nat.zero_add]
+  cases hp : p s <;> rfl
+
 /--
 `countUpTo n p` parses up to `n` occurrences of `p` until it fails, and returns the count of
 successes. This parser never fails.
@@ -294,15 +357,22 @@ where
 the count of successes and the output of `stop`. If `p` fails before encountering `stop` then the
 error from  `p` is reported and no input is consumed.
 -/
-partial def countUntil (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) :
-  ParserT ε σ τ m (Nat × β) := do
-  let _ := Inhabited.mk do return (0, ← stop)
-  withBacktracking do loop 0
+def countUntil (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) :
+  ParserT ε σ τ m (Nat × β) :=
+  withBacktracking do
+    loop (← getStream) 0
 where
-  loop [Inhabited (ParserT ε σ τ m (Nat × β))] (ct : Nat) := do
+  loop (s₀ : σ) (ct : Nat) : ParserT ε σ τ m (Nat × β) := do
     match ← option? stop with
-    | some s => return (ct, s)
-    | none => p *> loop (ct+1)
+    | some y => return (ct, y)
+    | none =>
+      let _ ← p
+      let s₁ ← getStream
+      if h : Stream.remaining s₁ < Stream.remaining s₀ then
+        loop s₁ (ct + 1)
+      else
+        return (ct + 1, ← stop)
+  termination_by Stream.remaining s₀
 
 /-! ### `endBy` family -/
 
diff --git a/Parser/Iterators.lean b/Parser/Iterators.lean
new file mode 100644
index 0000000..a75a4d0
--- /dev/null
+++ b/Parser/Iterators.lean
@@ -0,0 +1,150 @@
+/-
+Copyright © 2026 Nicolas Rouquette. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+
+import Parser.Stream
+import Std.Data.Iterators
+
+/-! # Std.Iterators bridge for Parser.Stream
+
+This module provides `Iterator` and `Finite` instances for `Parser.Stream` types, bridging the
+lean4-parser stream abstraction to the `Std.Data.Iterators` framework.
+
+## Design
+
+Each `Parser.Stream σ τ` provides:
+- A `Std.Stream σ τ` with `next? : σ → Option (τ × σ)` for consuming tokens
+- `remaining : σ → Nat`, an upper bound that strictly decreases on each `next?` yielding `some`
+
+We define `StreamIterator σ τ` wrapper that provides:
+- `Iterator (StreamIterator σ τ) Id τ` — steps via `next?`, never skips (for all `Parser.Stream`)
+- `Finite (StreamIterator σ τ) Id` — well-founded via `remaining` (requires `LawfulParserStream`)
+- `IteratorLoop` — enables `for` loops over stream tokens (requires `LawfulParserStream`)
+
+## Usage
+
+```lean
+import Parser.Iterators
+
+-- Given a LawfulParserStream instance (e.g., Subarray, OfList):
+def collectTokens [Parser.Stream σ τ] [LawfulParserStream σ τ] (s : σ) : Array τ := Id.run do
+  let mut acc := #[]
+  for tok in (StreamIterator.mk s).iter do
+    acc := acc.push tok
+  return acc
+```
+-/
+
+open Std Std.Iterators
+
+namespace Parser.Stream
+
+/--
+Wrapper that presents a `Parser.Stream` state as a `Std.Iterators` iterator state.
+
+The iterator yields tokens of type `τ` by calling `next?` on the underlying stream.
+It terminates when `next?` returns `none`.
+-/
+structure StreamIterator (σ : Type) (τ : Type) [Parser.Stream σ τ] where
+  /-- The underlying parser stream state. -/
+  stream : σ
+
+variable {σ τ : Type} [Parser.Stream σ τ]
+
+/-- Create a `StreamIterator` from a parser stream state. -/
+@[inline]
+def StreamIterator.mk' (s : σ) : StreamIterator σ τ := ⟨s⟩
+
+/-- Create a monadic iterator (`IterM Id τ`) from a `StreamIterator`. -/
+@[inline]
+def StreamIterator.iterM (s : StreamIterator σ τ) : IterM (α := StreamIterator σ τ) Id τ :=
+  IterM.mk s Id τ
+
+/-- Create a pure iterator (`Iter τ`) from a `StreamIterator`. -/
+@[inline]
+def StreamIterator.iter (s : StreamIterator σ τ) : Iter (α := StreamIterator σ τ) τ :=
+  s.iterM.toIter
+
+/--
+Predicate for the `Iterator` instance. Defined as a standalone function so that
+`simp` and `unfold` can reduce it when the `IterStep` constructor is known.
+-/
+def isPlausibleStreamStep
+    (it : IterM (α := StreamIterator σ τ) Id τ)
+    (step : IterStep (IterM (α := StreamIterator σ τ) Id τ) τ) : Prop :=
+  match step with
+  | .yield it' out =>
+    Stream.next? it.internalState.stream = some (out, it'.internalState.stream)
+  | .skip _ => False
+  | .done => Stream.next? it.internalState.stream = none
+
+/--
+`Iterator` instance for `StreamIterator`. Each step calls `next?` on the underlying stream:
+- If `next?` returns `some (tok, s')`, yields `tok` and advances to `s'`.
+- If `next?` returns `none`, the iterator is done.
+
+The iterator never produces `skip` steps.
+
+The `IsPlausibleStep` predicate ties each step to the actual `next?` result, ensuring that
+the plausible successor relation mirrors the stream's token consumption — which is the basis
+for the `Finite` proof.
+-/
+instance instIterator : Iterator (StreamIterator σ τ) Id τ where
+  IsPlausibleStep := isPlausibleStreamStep
+  step it := pure <|
+    match h : Stream.next? it.internalState.stream with
+    | some (tok, s') =>
+      .deflate ⟨.yield (IterM.mk (α := StreamIterator σ τ) ⟨s'⟩ Id τ) tok, by
+        unfold isPlausibleStreamStep
+        simp
+        exact h⟩
+    | none =>
+      .deflate ⟨.done, by
+        unfold isPlausibleStreamStep
+        exact h⟩
+
+/--
+`Finite` instance for `StreamIterator`, proven via `LawfulParserStream.remaining_decreases`.
+
+The `remaining` field of `Parser.Stream` provides an upper bound on tokens that strictly
+decreases when `next?` returns `some`. We use `remaining ∘ StreamIterator.stream` as the
+well-founded measure via a `FinitenessRelation`.
+
+Requires `LawfulParserStream σ τ` to provide the proof that `remaining` strictly decreases.
+Types without a `LawfulParserStream` instance (e.g., `mkDefault`) still get the `Iterator`
+instance above, but not `Finite` — they cannot prove termination.
+-/
+def streamFinitenessRelation [LawfulParserStream σ τ] :
+    FinitenessRelation (StreamIterator σ τ) Id where
+  Rel := InvImage WellFoundedRelation.rel
+    (Parser.Stream.remaining ∘ StreamIterator.stream ∘ IterM.internalState)
+  wf := InvImage.wf _ WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    obtain ⟨step, hsucc, hplaus⟩ := h
+    cases step with
+    | yield it'' out =>
+      simp [IterStep.successor] at hsucc
+      subst hsucc
+      simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, isPlausibleStreamStep] at hplaus
+      exact LawfulParserStream.remaining_decreases _ _ _ hplaus
+    | skip it'' =>
+      simp [IterStep.successor] at hsucc
+      subst hsucc
+      simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, isPlausibleStreamStep] at hplaus
+    | done =>
+      simp [IterStep.successor] at hsucc
+
+instance [LawfulParserStream σ τ] : Iterators.Finite (StreamIterator σ τ) Id :=
+  Iterators.Finite.of_finitenessRelation streamFinitenessRelation
+
+/--
+`IteratorLoop` instance enabling `for` loops and standard consumers (`fold`, `toList`, etc.)
+over `StreamIterator`. Requires `LawfulParserStream` for the `Finite` proof.
+-/
+@[always_inline, inline]
+instance [LawfulParserStream σ τ] {n : Type → Type} [Monad n] :
+    IteratorLoop (StreamIterator σ τ) Id n :=
+  .defaultImplementation
+
+end Parser.Stream
diff --git a/Parser/Parser.lean b/Parser/Parser.lean
index 80b6284..cd5efbc 100644
--- a/Parser/Parser.lean
+++ b/Parser/Parser.lean
@@ -185,16 +185,73 @@ def withErrorMessage (msg : String) (p : ParserT ε σ τ m α) : ParserT ε σ
 
 /-! ### `foldl` family -/
 
+/--
+Core loop for `efoldlP`. Terminates via well-founded recursion on `Stream.remaining s`.
+
+After each successful `p >>= f` step, we check whether `Stream.remaining` decreased. If not
+(the parser succeeded without consuming input), the loop stops to prevent infinite iteration.
+This matches the original fuel-based semantics but uses `remaining` directly as the termination
+measure rather than a separate fuel parameter.
+-/
 @[specialize]
-private partial def efoldlPAux [Inhabited ε] [Inhabited σ] [Inhabited β]
+private def efoldlPAux [Inhabited ε] [Inhabited σ] [Inhabited β]
   (f : β → α → ParserT ε σ τ m β) (p : ParserT ε σ τ m α) (y : β) (s : σ) :
-  m (Parser.Result ε σ (β × ε × Bool)) :=
+  m (Parser.Result ε σ (β × ε × Bool)) := do
   let savePos := Stream.getPosition s
-  p s >>= fun
-    | .ok s x => f y x s >>= fun
-      | .ok s y => efoldlPAux f p y s
-      | .error s e => return .ok (Stream.setPosition s savePos) (y, e, true)
-    | .error s e => return .ok (Stream.setPosition s savePos) (y, e, false)
+  match ← p s with
+  | .ok s' x =>
+    match ← f y x s' with
+    | .ok s'' y' =>
+      if _h : Stream.remaining s'' < Stream.remaining s then
+        efoldlPAux f p y' s''
+      else
+        -- Parser didn't consume; stop to avoid infinite loop.
+        return .ok s'' (y', Error.unexpected (Stream.getPosition s'') none, false)
+    | .error s'' e => return .ok (Stream.setPosition s'' savePos) (y, e, true)
+  | .error s' e => return .ok (Stream.setPosition s' savePos) (y, e, false)
+termination_by Stream.remaining s
+
+/-! ### `efoldlPAux` one-step equation (m = Id)
+
+For the identity monad, `efoldlPAux` reduces to a direct case split on
+`p s` and `f y x s'`.  This one-step equation is the foundation for
+downstream `@[simp]` lemmas for `foldl`, `dropMany`, and `count`.
+-/
+
+/--
+One-step unfolding of `efoldlPAux` for `m = Id`.
+
+This expresses the recursive function as a case split:
+- If `p s` fails → return accumulator, backtrack position, error from `p`.
+- If `p s` succeeds with `(s', x)` and `f y x s'` fails → return accumulator,
+  backtrack position, error from `f`.
+- If both succeed with stream `s''` and `remaining s'' < remaining s` → recurse.
+- If both succeed but stream didn't advance → stop, return accumulator.
+-/
+private theorem efoldlPAux_eq [Inhabited ε] [Inhabited σ] [Inhabited β]
+    (f : β → α → Parser ε σ τ β) (p : Parser ε σ τ α) (y : β) (s : σ) :
+    efoldlPAux (m := Id) f p y s =
+      match p s with
+      | .ok s' x =>
+        match f y x s' with
+        | .ok s'' y' =>
+          if _h : Stream.remaining s'' < Stream.remaining s then
+            efoldlPAux (m := Id) f p y' s''
+          else
+            .ok s'' (y', Error.unexpected (Stream.getPosition s'') none, false)
+        | .error s'' e =>
+          .ok (Stream.setPosition s'' (Stream.getPosition s)) (y, e, true)
+      | .error s' e =>
+        .ok (Stream.setPosition s' (Stream.getPosition s)) (y, e, false) := by
+  rw [efoldlPAux]
+  simp only [bind, Bind.bind, pure, Pure.pure]
+  cases hp : p s with
+  | ok s' x =>
+    simp only []
+    cases hf : f y x s' with
+    | ok s'' y' => simp only []
+    | error s'' e => rfl
+  | error s' e => rfl
 
 /--
 `foldlP f init p` folds the parser function `f` from left to right using `init` as an intitial
@@ -260,6 +317,83 @@ This parser never fails.
 def foldl (f : β → α → β) (init : β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m β :=
   Prod.fst <$> efoldl f init p
 
+/-! ### Fold-combinator specification lemmas (m = Id)
+
+One-step unfolding lemmas that make the fold combinators
+deductively transparent for proofs.  All are specialized to
+`m = Id` (the `Parser` abbreviation), since the monadic plumbing
+reduces to identity / function application for `Id`.
+-/
+
+/--
+`efoldlPAux` is independent of the `Inhabited` instances.
+
+The `[Inhabited ε] [Inhabited σ] [Inhabited β]` arguments are required
+by well-founded recursion infrastructure but do not appear in the
+function body.  This lemma allows changing instances freely.
+-/
+private theorem efoldlPAux_inhabited_irrel
+    (iε : Inhabited ε) (iσ : Inhabited σ) (iβ : Inhabited β)
+    (jε : Inhabited ε) (jσ : Inhabited σ) (jβ : Inhabited β)
+    (f : β → α → Parser ε σ τ β) (p : Parser ε σ τ α) (y : β) (s : σ) :
+    @efoldlPAux _ Id _ _ _ _ _ _ _ iε iσ iβ f p y s =
+    @efoldlPAux _ Id _ _ _ _ _ _ _ jε jσ jβ f p y s := by
+  rw [@efoldlPAux_eq _ _ _ _ _ _ _ iε iσ iβ f p y s,
+      @efoldlPAux_eq _ _ _ _ _ _ _ jε jσ jβ f p y s]
+  split -- match p s
+  · split -- match f y _ _
+    · split -- if remaining < remaining
+      · exact efoldlPAux_inhabited_irrel iε iσ iβ jε jσ jβ f p _ _
+      · rfl
+    · rfl
+  · rfl
+termination_by Stream.remaining s
+
+/--
+One-step unfolding of `foldl` for `m = Id`.
+
+`foldl f init p` applied to stream `s` performs one step:
+- If `p s` succeeds with `(s', x)` and `remaining s' < remaining s`,
+  it recurses with `foldl f (f init x) p s'`.
+- If `p s` succeeds but stream didn't advance, returns `f init x`.
+- If `p s` fails, returns `init` with position restored.
+-/
+theorem foldl_eq (f : β → α → β) (init : β) (p : Parser ε σ τ α) (s : σ) :
+    (foldl f init p : Parser ε σ τ _) s =
+      match p s with
+      | .ok s' x =>
+        if _h : Stream.remaining s' < Stream.remaining s then
+          (foldl f (f init x) p : Parser ε σ τ _) s'
+        else .ok s' (f init x)
+      | .error s' _ =>
+        .ok (Stream.setPosition s' (Stream.getPosition s)) init := by
+  -- Unfold the full foldl chain to efoldlPAux on both sides
+  simp only [foldl, efoldl, efoldlM, efoldlP,
+             Functor.map, bind, Bind.bind, pure, Pure.pure,
+             monadLift, MonadLift.monadLift]
+  -- Unfold efoldlPAux one step with explicit Inhabited instances
+  rw [@efoldlPAux_eq _ _ _ _ _ _ _
+      ⟨Error.unexpected (Stream.getPosition s) none⟩ ⟨s⟩ ⟨init⟩]
+  -- Case-split on p s
+  cases hp : p s with
+  | ok s' x =>
+    -- Reduce inner matches: F init x s' = .ok s' (f init x), etc.
+    simp only []
+    -- Split on the consuming condition
+    by_cases h : Stream.remaining s' < Stream.remaining s
+    · -- Consuming: reduce dite on both sides
+      simp only [dif_pos h]
+      -- Both sides: match chain wrapping efoldlPAux with different Inhabited
+      congr 1; congr 1
+      exact efoldlPAux_inhabited_irrel
+        ⟨Error.unexpected (Stream.getPosition s) none⟩ ⟨s⟩ ⟨init⟩
+        ⟨Error.unexpected (Stream.getPosition s') none⟩ ⟨s'⟩ ⟨f init x⟩
+        (fun y x s => .ok s (f y x)) p (f init x) s'
+    · -- Not consuming
+      simp only [dif_neg h]
+  | error s' e =>
+    simp only []
+
 /-! ### `option` family -/
 
 /--
diff --git a/Parser/Stream.lean b/Parser/Stream.lean
index 7e1e082..fbc601f 100644
--- a/Parser/Stream.lean
+++ b/Parser/Stream.lean
@@ -27,6 +27,10 @@ backtracking and error reporting.
 * The type `Position` is used to record position data for the stream type.
 * `getPosition (s : σ) : Position` returns the current position of stream `s`.
 * `setPosition (s : σ) (p : Position) : σ` restores stream `s` to position `p`.
+* `remaining (s : σ) : Nat` returns an upper bound on remaining tokens in `s`.
+
+  This value must strictly decrease when a token is consumed (`next?` returns `some`).
+  It is used as a termination measure for total fold combinators.
 
 Implementations should try to make the `Position` type as lightweight as possible for `getPosition`
 and `setPosition` to work properly. Often `Position` is just a scalar type or another simple type.
@@ -36,9 +40,26 @@ protected class Parser.Stream (σ : Type _) (τ : outParam (Type _)) extends Std
   Position : Type _
   getPosition : σ → Position
   setPosition : σ → Position → σ
+  /-- An upper bound on the number of remaining tokens. Must strictly decrease when `next?`
+      returns `some`. Used as a well-founded termination measure for fold combinators. -/
+  remaining : σ → Nat
 attribute [reducible, inherit_doc Parser.Stream] Parser.Stream.Position
 attribute [inherit_doc Parser.Stream] Parser.Stream.getPosition Parser.Stream.setPosition
 
+/-- Lawful parser stream: `remaining` strictly decreases when `next?` consumes a token.
+
+This law formalizes the contract that `Parser.Stream.remaining` provides a well-founded termination
+measure. Instances of `LawfulParserStream` are required by the sorry-free `Finite` instance for
+`StreamIterator`, enabling provably terminating iteration via `Std.Data.Iterators`.
+
+The `mkDefault` fallback does not satisfy this law (its `remaining` uses a `partial def`),
+so there is intentionally no `LawfulParserStream` instance for `mkDefault`.
+-/
+class LawfulParserStream (σ : Type _) (τ : outParam (Type _)) [Parser.Stream σ τ] : Prop where
+  /-- `remaining` strictly decreases when `next?` returns `some`. -/
+  remaining_decreases : ∀ (s : σ) (tok : τ) (s' : σ),
+    Stream.next? s = some (tok, s') → Parser.Stream.remaining s' < Parser.Stream.remaining s
+
 namespace Parser.Stream
 
 /-- Stream segment type. -/
@@ -58,18 +79,33 @@ prefer tailored `Parser.Stream` instances to this default.
 @[nolint unusedArguments]
 def mkDefault (σ τ) [Std.Stream σ τ] := σ
 
+/-- Count remaining tokens by iterating the stream. O(n) — only used by `mkDefault`. -/
+private partial def countStreamRemaining (next? : σ → Option (τ × σ)) (s : σ) : Nat :=
+  match next? s with
+  | none => 0
+  | some (_, s') => countStreamRemaining next? s' + 1
+
 @[reducible]
 instance (σ τ) [self : Std.Stream σ τ] : Parser.Stream (mkDefault σ τ) τ where
   toStream := self
   Position := σ
   getPosition s := s
   setPosition _ p := p
+  remaining s := countStreamRemaining self.next? s
 
 @[reducible]
 instance : Parser.Stream String.Slice Char where
   Position := String.Slice
   getPosition s := s
   setPosition _ s := s
+  remaining s := s.endExclusive.offset.byteIdx - s.startInclusive.offset.byteIdx
+
+/-- TODO: prove via `Slice.Pos.lt_next` and `Slice.sliceFrom` lemmas once the
+right `simp` set for String.Slice byte-index arithmetic is identified. -/
+instance : LawfulParserStream String.Slice Char where
+  remaining_decreases _ _ _ _ := by
+    simp only [Parser.Stream.remaining]
+    sorry
 
 @[reducible]
 instance : Parser.Stream Substring.Raw Char where
@@ -80,6 +116,14 @@ instance : Parser.Stream Substring.Raw Char where
       { s with startPos := p }
     else
       { s with startPos := s.stopPos }
+  remaining s := s.stopPos.byteIdx - s.startPos.byteIdx
+
+/-- TODO: prove via `String.Pos.Raw.lt_next` once the right `simp` set for
+Substring.Raw byte-index arithmetic is identified. -/
+instance : LawfulParserStream Substring.Raw Char where
+  remaining_decreases _ _ _ _ := by
+    simp only [Parser.Stream.remaining]
+    sorry
 
 @[reducible]
 instance (τ) : Parser.Stream (Subarray τ) τ where
@@ -90,12 +134,34 @@ instance (τ) : Parser.Stream (Subarray τ) τ where
       ⟨{ s.internalRepresentation with start := p, start_le_stop := h }⟩
     else
       ⟨{ s.internalRepresentation with start := s.stop, start_le_stop := Nat.le_refl s.stop }⟩
+  remaining s := s.stop - s.start
+
+instance (τ) : LawfulParserStream (Subarray τ) τ where
+  remaining_decreases s tok s' h := by
+    simp only [Parser.Stream.remaining]
+    dsimp [Stream.next?, Std.Stream.next?] at h
+    split at h
+    · next hlt =>
+      obtain ⟨_, rfl⟩ := Option.some.inj h
+      simp only [Subarray.start, Subarray.stop]
+      have h1 : s.start = s.internalRepresentation.start := rfl
+      have h2 : s.stop = s.internalRepresentation.stop := rfl
+      omega
+    · nomatch h
 
 @[reducible]
 instance : Parser.Stream ByteSlice UInt8 where
   Position := Nat
   getPosition s := s.start
   setPosition s p := s.slice p
+  remaining s := s.stop - s.start
+
+instance : LawfulParserStream ByteSlice UInt8 where
+  remaining_decreases s tok s' h := by
+    simp only [Parser.Stream.remaining]
+    -- Stream.next? for ByteSlice: s[0]? >>= (·, s.popFront)
+    -- popFront advances start by 1, so s'.stop - s'.start < s.stop - s.start
+    sorry
 
 /-- `OfList` is a view of a list stream that keeps track of consumed tokens. -/
 structure OfList (τ : Type _) where
@@ -129,9 +195,22 @@ instance (τ) : Parser.Stream (OfList τ) τ where
   Position := Nat
   getPosition s := s.past.length
   setPosition := OfList.setPosition
+  remaining s := s.next.length
   next? s :=
     match s with
     | ⟨x :: rest, past⟩ => some (x, ⟨rest, x :: past⟩)
     | _ => none
 
+instance (τ) : LawfulParserStream (OfList τ) τ where
+  remaining_decreases s tok s' h := by
+    simp only [Parser.Stream.remaining]
+    match s, h with
+    | ⟨_ :: _, _⟩, h =>
+      dsimp [Stream.next?, Std.Stream.next?] at h
+      obtain ⟨_, rfl⟩ := Option.some.inj h
+      simp [List.length_cons]
+    | ⟨[], _⟩, h =>
+      dsimp [Stream.next?, Std.Stream.next?] at h
+      nomatch h
+
 end Parser.Stream