proof(xml-7-44): make Xml744.Escape.exfiltrate provably total (#79)

## Summary

- Resolves the three `assert_total` proof escapes in
`Xml744.Escape.exfiltrate`'s inner `replaceAll` worker (originally
wrapping partial calls to `strHead`, `head`, and `tail` on Idris2 0.7).
- The earlier refactor that pattern-matched the partial calls away
**left the function failing Idris2's termination check** on 0.8.0 —
recursion through `pack $ drop ...` is not structurally smaller, so the
file did not actually build (`exfiltrate is not total, possibly not
terminating`).
- This PR rewrites the worker as `replaceAllChars : Nat -> List Char ->
List Char -> List Char -> List Char` with a fuel parameter sized to
`length (unpack str)`. Each recursive step consumes ≥ 1 char of the
third argument so the fuel bound is never the binding constraint — it
just makes termination structurally obvious. Matches the Nat-fueled
pattern from the ephapax totality campaign (standards#134).

## Verification

```
$ idris2 -p contrib Xml744/Escape.idr
1/1: Building Xml744.Escape (Xml744/Escape.idr)
Xml744.Escape> :total Xml744.Escape.exfiltrate
Xml744.Escape.exfiltrate is total
Xml744.Escape> :total Xml744.Escape.infiltrate
Xml744.Escape.infiltrate is total
Xml744.Escape> :total Xml744.Escape.infiltrateAttr
Xml744.Escape.infiltrateAttr is total
Xml744.Escape> :total Xml744.Escape.makeSafe
Xml744.Escape.makeSafe is total
```

`grep -E 'assert_total|assert_smaller|believe_me|%unsafe|partial '
src/Xml744/Escape.idr` matches only the new doc-comment line referencing
what is *not* used.

## Out of scope (separate proof debts in this toolkit)

- `Xml744.Attribute` has a pre-existing baseline issue (`decEq` not in
scope for `Bool` on Idris2 0.8.0) and a `PROOF_TODO`-marked `cast
(MkAttrName s)` in `unsafeAttrName` — both predate this branch and are
distinct from the three escapes called out in the proof-debt request.

## Test plan

- [ ] CI green
- [ ] `idris2 --build idris2-ecosystem/xml-toolkit/xml-7-44.ipkg` builds
`Xml744.Escape` cleanly (verified locally; downstream module errors are
unrelated and tracked separately)

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

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

Author: hyperpolymath

idris2-ecosystem/xml-toolkit/src/Xml744/Escape.idr

@@ -48,6 +48,11 @@ infiltrateAttr : String -> String
 infiltrateAttr = concatMap escapeAttrChar . unpack
 
 ||| Exfiltrate: safely extract content from XML (unescape entities)
+|||
+||| The worker `replaceAllChars` recurses on a `Nat` fuel sized to the input.
+||| Each step consumes at least one character of the third argument, so the
+||| fuel bound is never reached in practice — it exists to make termination
+||| structurally obvious to Idris2 without `assert_total` / `assert_smaller`.
 export
 exfiltrate : String -> String
 exfiltrate s =
@@ -58,18 +63,19 @@ exfiltrate s =
       s5 = replaceAll "'" "'" s4
   in s5
   where
+    replaceAllChars : Nat -> List Char -> List Char -> List Char -> List Char
+    replaceAllChars _     _         _  []        = []
+    replaceAllChars _     []        _  xs        = xs
+    replaceAllChars Z     _         _  xs        = xs
+    replaceAllChars (S k) (f :: fs) to (x :: xs) =
+      if isPrefixOf (f :: fs) (x :: xs)
+        then to ++ replaceAllChars k (f :: fs) to (drop (length fs) xs)
+        else x :: replaceAllChars k (f :: fs) to xs
+
     replaceAll : String -> String -> String -> String
     replaceAll from to str =
-      case unpack from of
-        [] => str  -- empty search string, return unchanged
-        (fc :: _) =>
-          case break (== fc) (unpack str) of
-            (before, []) => str
-            (before, (r :: rs)) =>
-              if isPrefixOf (unpack from) (r :: rs)
-                then pack before ++ to ++ replaceAll from to (pack $ drop (length from) (r :: rs))
-                else pack before ++ singleton r ++
-                     replaceAll from to (pack rs)
+      let chars = unpack str
+      in pack (replaceAllChars (length chars) (unpack from) (unpack to) chars)
 
 ||| Check if a string contains any unescaped dangerous characters
 export