proof(idris2): tighten Ephapax.Parse.Stream to %default total (#90)

## Summary

Second file in the `%default partial` → `%default total` chain for
`ephapax/idris2/src/Ephapax/`. SExpr.idr (#89) was first; Stream.idr is
this one.

Only one definition in `Stream.idr` actually recurses: the `where`-bound
`build` inside `remaining`. It walks an `Int` index up to `s.len` —
Idris2 can't detect this as terminating because Int is not a structural
recursor.

Fix: replace `build` with a Nat-fueled helper `buildFuel`, with fuel `=
integerToNat (s.len - s.index)`. Each recursive call decrements fuel by
1 and increments the index by 1 in lockstep, so the fuel can never run
out before the `i >= s.len` guard fires. When `s.index >= s.len` the
cast/truncation produces fuel 0 — matching the partial original's
empty-return.

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

## Verification

```
$ IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --check Ephapax/Parse/Stream.idr
1/3: Building Ephapax.Parse.Lexer
2/3: Building Ephapax.Parse.ZigBuffer
3/3: Building Ephapax.Parse.Stream
```

Downstream `Ephapax.Parse.Parser` (which `import Ephapax.Parse.Stream`)
also still builds clean — checked locally.

## Refs

- `#124` (proof-debt audit epic)
- `#134` (ephapax totality sub-issue)
- Companion: PR `#89` (Ephapax.IR.SExpr — same campaign, file 1 of 9)

## Test plan

- [x] `idris2 --check Ephapax/Parse/Stream.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/Stream.idr

@@ -3,7 +3,7 @@ module Ephapax.Parse.Stream
 import Ephapax.Parse.Lexer
 import Ephapax.Parse.ZigBuffer
 
-%default partial
+%default total
 
 public export
 record Stream where
@@ -45,12 +45,13 @@ atEnd s = s.index >= s.len
 
 public export
 remaining : Stream -> List Token
-remaining s = build s.index
+remaining s = buildFuel (integerToNat (cast (s.len - s.index))) s.index
   where
-    build : Int -> List Token
-    build i =
+    buildFuel : Nat -> Int -> List Token
+    buildFuel Z _ = []
+    buildFuel (S k) i =
       if i >= s.len then []
-      else MkToken (getTokKind s.buf i) (getTokPos s.buf i) :: build (i + 1)
+      else MkToken (getTokKind s.buf i) (getTokPos s.buf i) :: buildFuel k (i + 1)
 
 public export
 at : Int -> Stream -> Maybe Token