proof(xml-7-44): discharge Xml744.Attribute proof debts (#80)

## Summary

Discharges the two `PROOF_TODO`-marked sites in `Xml744.Attribute` that
blocked the toolkit's build on Idris2 0.8.0.

1. **`attrName`** used `decEq (isValidName s) True` — `decEq` for `Bool`
is not in scope with the current imports. Replaced with `with
(isValidName s) proof prf`, which binds `prf : isValidName s = True`
directly in the matched branch and discharges `MkAttrName`'s
auto-implicit.

2. **`unsafeAttrName`** was `cast (MkAttrName s)` — never compiled (no
matching `Cast` instance; `MkAttrName` requires the validity proof to
construct). Now takes the proof as an auto-implicit: `(s : String) ->
{auto prf : isValidName s = True} -> AttrName`, so it can only be called
on strings whose validity Idris2 can verify at elaboration time. `Refl`
discharges for any literal — matching the existing doc "use only for
known-good literals".

## Knock-on changes (still in `Xml744.Attribute`)

- `wAttr` routed through `unsafeAttrName ("w:" ++ n)`. Signature bumped
to `(n : String) -> {auto prf : isValidName ("w:" ++ n) = True} ->
String -> XmlAttr` so callers' literal `n` lets the elaborator reduce
both the concatenation and `isValidName` to `True`. All four existing
call sites (`wAttr "id"`, `"author"`, `"date"`, `"initials"`) discharge
automatically.
- `isNameStartChar`, `isNameChar`, `isValidName` promoted from `export`
to `public export` so cross-module callers see the definitions for
elaboration-time reduction.

## Verification

```
$ idris2 -p contrib Xml744/Attribute.idr
1/3: Building Xml744.Escape (Xml744/Escape.idr)
2/3: Building Xml744.Text (Xml744/Text.idr)
3/3: Building Xml744.Attribute (Xml744/Attribute.idr)
Xml744.Attribute> :total Xml744.Attribute.attrName       --> is total
Xml744.Attribute> :total Xml744.Attribute.unsafeAttrName --> is total
Xml744.Attribute> :total Xml744.Attribute.wAttr          --> is total
[+ attr / renderAttr / getAttrValue / id / name / value — all total]
```

`grep -E
'assert_total|assert_smaller|believe_me|%unsafe|PROOF_TODO|idris_crash|partial
' src/Xml744/Attribute.idr` → no matches.

Toolkit build now advances `3/6 → 4/6`. Element still red on its own
parallel debts (see below).

## Out of scope — known follow-ups in `Xml744.Element`

- `tagName` uses the same `decEq` form (fix: `with proof`).
- `unsafeTagName` uses the same `cast (MkTagName s)` placeholder (fix:
auto-implicit proof).
- `render` / `renderPretty.go` fail totality due to mutual recursion
through `[XmlNode]` — needs explicit termination, e.g. Nat fuel.

Stacks on top of #79 (`proof-debt/xml744-escape-totality`); base is
`main` per [[feedback_stacked_pr_orphan_trap_github]], so the diff is
cumulative until #79 lands, then this rebases to a single-file change.

## Test plan

- [ ] CI green
- [ ] `idris2 --build idris2-ecosystem/xml-toolkit/xml-7-44.ipkg` builds
modules 1–3 cleanly (verified locally)

🤖 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/Attribute.idr

@@ -9,15 +9,22 @@ import Data.List
 
 %default total
 
-||| Valid XML name characters (simplified - ASCII subset)
+||| Valid XML name characters (simplified - ASCII subset).
+|||
+||| `public export` so cross-module callers of `unsafeAttrName` / `wAttr` on
+||| string literals can have the auto-implicit `isValidName s = True` proof
+||| discharged by elaboration-time reduction. With plain `export` only the
+||| name is visible and reduction is blocked.
+public export
 isNameStartChar : Char -> Bool
 isNameStartChar c = isAlpha c || c == '_' || c == ':'
 
+public export
 isNameChar : Char -> Bool
 isNameChar c = isNameStartChar c || isDigit c || c == '-' || c == '.'
 
-||| Check if a string is a valid XML name
-export
+||| Check if a string is a valid XML name.
+public export
 isValidName : String -> Bool
 isValidName s = case unpack s of
   [] => False
@@ -28,19 +35,26 @@ public export
 data AttrName : Type where
   MkAttrName : (n : String) -> {auto prf : isValidName n = True} -> AttrName
 
-||| Try to create an attribute name (returns Nothing if invalid)
+||| Try to create an attribute name (returns Nothing if invalid).
+|||
+||| The `with proof` form binds `prf : isValidName s = True` in the matched
+||| branch, which discharges `MkAttrName`'s auto-implicit. Replaces the
+||| previous `decEq (isValidName s) True` form — `decEq` for `Bool` is not in
+||| scope on Idris2 0.8.0 with the current imports.
 export
 attrName : (s : String) -> Maybe AttrName
-attrName s = case decEq (isValidName s) True of
-  Yes prf => Just (MkAttrName s)
-  No _ => Nothing
-
-||| Unsafe attribute name creation (use only for known-good literals)
+attrName s with (isValidName s) proof prf
+  attrName s | True  = Just (MkAttrName s)
+  attrName s | False = Nothing
+
+||| Attribute-name constructor for string literals whose validity Idris2
+||| can verify at elaboration time. The auto-implicit `isValidName s = True`
+||| is discharged by `Refl` for any literal (or compile-time-known) string.
+||| Replaces the previous `cast (MkAttrName s)` placeholder, which never
+||| compiled (no matching `Cast` instance, and `MkAttrName` needs the proof).
 export
-unsafeAttrName : String -> AttrName
--- PROOF_TODO: Replace cast with actual proof
--- PROOF_TODO: Replace cast with actual proof
-unsafeAttrName s = cast (MkAttrName s)
+unsafeAttrName : (s : String) -> {auto prf : isValidName s = True} -> AttrName
+unsafeAttrName s = MkAttrName s
 
 ||| Common attribute names as constants
 export
@@ -77,9 +91,13 @@ export
 getAttrValue : XmlAttr -> String
 getAttrValue (MkAttr _ v) = exfiltrate v
 
-||| Convenience for common w: namespace attributes (OOXML)
+||| Convenience for common w: namespace attributes (OOXML).
+|||
+||| The auto-implicit proof obligation `isValidName ("w:" ++ n) = True` is
+||| discharged at the call site by `Refl` for any literal `n` (the elaborator
+||| reduces both the string concatenation and `isValidName` on closed terms).
 export
-wAttr : String -> String -> XmlAttr
+wAttr : (n : String) -> {auto prf : isValidName ("w:" ++ n) = True} -> String -> XmlAttr
 wAttr n v = attr (unsafeAttrName ("w:" ++ n)) v
 
 ||| Example: attribute that would break with raw quotes