proof(idris2): tighten Ephapax.Parse.Util to %default total (#91)

## Summary

Third file in the `%default partial` → `%default total` chain for
`ephapax/idris2/src/Ephapax/`. SExpr.idr (#89) was first; Stream.idr
(#90) second.

Two combinators in `Util.idr` recurse unboundedly on a `Stream` rather
than on a structural recursor:
- `many : Parser a -> Parser (List a)` — repeated application until
first failure
- `sepBy.sepTail` — alternating separator + element

Replace both with Nat-fueled siblings (`manyFuel` / `sepTailFuel`) where
fuel `= integerToNat (cast (s.len - s.index))` — the count of remaining
tokens in the input stream at entry. Each recursive call decrements fuel
by 1, and the inner parser is assumed to consume ≥1 token per success
(the only well-formed usage).

`sepBy1` already delegates to `sepBy` and inherits totality for free.

## Soundness

On a *consuming* inner parser (every real combinator client), the fueled
form is observationally identical to the partial original: the stream is
monotonically advancing, so the parser exhausts the stream before the
fuel exhausts (in the common case it's tight equality — fuel =
tokens-remaining).

On a degenerate non-consuming inner parser, the partial original loops
forever; the fueled form returns a truncated list. Strictly safer.

No `assert_total` / `assert_smaller` / `believe_me` escapes.

## Verification

```
$ IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --check Ephapax/Parse/Util.idr
4/4: Building Ephapax.Parse.Util (Ephapax/Parse/Util.idr)
$ idris2 --check Ephapax/Parse/Parser.idr   # downstream
6/6: Building Ephapax.Parse.Parser (Ephapax/Parse/Parser.idr)
```

## Refs

- `#124` (proof-debt audit epic)
- `#134` (ephapax totality sub-issue)
- Companion: PR `#89` (SExpr — file 1), PR `#90` (Stream — file 2)

## Test plan

- [x] `idris2 --check Ephapax/Parse/Util.idr` builds green under
`%default total`
- [x] Downstream `Ephapax.Parse.Parser` still builds
- [ ] CI green
- [ ] No `assert_*` / `believe_me` introduced (verified by inspection —
see diff)

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

idris2/src/Ephapax/Parse/Util.idr

@@ -4,7 +4,7 @@ import Data.List
 import Ephapax.Parse.Lexer
 import Ephapax.Parse.Stream
 
-%default partial
+%default total
 
 public export
 data ParseError = PE String (Maybe Pos)
@@ -56,12 +56,17 @@ expectIdent stream =
 public export
 many : Parser a -> Parser (List a)
 many p stream =
-  case p stream of
-    Left _ => Right ([], stream)
-    Right (v, rest) =>
-      case many p rest of
-        Left err => Left err
-        Right (vs, rest2) => Right (v :: vs, rest2)
+  manyFuel (integerToNat (cast (stream.len - stream.index))) p stream
+  where
+    manyFuel : Nat -> Parser a -> Parser (List a)
+    manyFuel Z _ s = Right ([], s)
+    manyFuel (S k) p s =
+      case p s of
+        Left _ => Right ([], s)
+        Right (v, rest) =>
+          case manyFuel k p rest of
+            Left err => Left err
+            Right (vs, rest2) => Right (v :: vs, rest2)
 
 public export
 optional : Parser a -> Parser (Maybe a)
@@ -156,16 +161,18 @@ sepBy : Parser a -> Parser sep -> Parser (List a)
 sepBy p sep stream =
   case p stream of
     Left _ => Right ([], stream)
-    Right (v, rest) => sepTail [v] rest
+    Right (v, rest) =>
+      sepTailFuel (integerToNat (cast (rest.len - rest.index))) [v] rest
   where
-    sepTail : List a -> Parser (List a)
-    sepTail acc stream2 =
+    sepTailFuel : Nat -> List a -> Parser (List a)
+    sepTailFuel Z acc stream2 = Right (reverse acc, stream2)
+    sepTailFuel (S k) acc stream2 =
       case sep stream2 of
         Left _ => Right (reverse acc, stream2)
         Right (_, rest) =>
           case p rest of
             Left err => Left err
-            Right (v, rest2) => sepTail (v :: acc) rest2
+            Right (v, rest2) => sepTailFuel k (v :: acc) rest2
 
 public export
 sepBy1 : Parser a -> Parser sep -> Parser (List a)