proof(idris2): tighten Ephapax.IR.Decode to %default total (#96)

## Summary

Sixth file in the `%default partial` → `%default total` chain.
Companions: SExpr (#89), Stream (#90), Util (#91), Lexer (#93), AST
(#94).

Flip `%default partial → %default total`. Roughly 22 atomic
encode/decode helpers (the `baseToAtom`/`atomToBase` style maps,
`encodeLit`/`decodeLit`, `encodeTy`/`decodeTy`, `escape`/`unescape`,
`encodeParam`/`decodeParam`, etc.) are now provably total under the file
default.

## 7 `covering` markers retained

Two distinct Idris2 0.8.0 limits force this:

1. **`encodeExpr` / `decodeExpr`** — structural recursion runs through
`map encodeExpr es` and `traverse decodeExpr rest` for the `Block` case.
The recursion *is* structural via list head/tail induction on a `List
Expr`, but Idris2 SCT cannot trace the size decrease across the
`Functor` / `Traversable` dictionary call. Same root cause as the
existing `Show Expr` / `Eq Expr` `covering` markers in AST.idr (#94).

2. **`encodeDecl` / `decodeDecl` / `fromSExpr` / `toSExpr`** —
transitively call the two above; inherit `covering`.

3. **`encode`** — `encode = show . toSExpr` depends on
`Ephapax.IR.SExpr.show` totality, which lands in PR #89. After #89
merges, `encode` would still be `covering` from `toSExpr`.

`covering` is strictly stronger than the previous file default of
`partial` — no new escape. No `assert_total` / `believe_me`.

## Verification

```
$ IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --check Ephapax/IR/Decode.idr
3/3: Building Ephapax.IR.Decode (Ephapax/IR/Decode.idr)
$ idris2 --check Ephapax/Parse/Parser.idr   # downstream
6/6: Building Ephapax.Parse.Parser
$ idris2 --check Ephapax/Affine/Emit.idr     # downstream
4/4: Building Ephapax.Affine.Emit
```

## Refs

- `#124` (proof-debt audit epic)
- `#134` (ephapax totality sub-issue)
- Companions: PR `#89` (SExpr), `#90` (Stream), `#91` (Util), `#93`
(Lexer), `#94` (AST)

## Test plan

- [x] `idris2 --check Ephapax/IR/Decode.idr` builds green under
`%default total`
- [x] Downstream Parse/Parser + Affine/Emit still build
- [ ] CI green
- [x] No `assert_*` / `believe_me`; only 7 deliberate `covering` markers
(justified above)

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

@@ -5,7 +5,7 @@ import Data.String
 import Ephapax.IR.SExpr
 import Ephapax.IR.AST
 
-%default partial
+%default total
 
 baseToAtom : BaseTy -> String
 baseToAtom Unit = "unit"
@@ -154,6 +154,7 @@ decodeTy (List [Atom "borrow", inner]) = pure (Borrow !(decodeTy inner))
 decodeTy (List [Atom "var", Atom v]) = pure (Var v)
 decodeTy _ = Left (Invalid "unknown type")
 
+covering
 encodeExpr : Expr -> SExpr
 encodeExpr (Lit lit) = List [Atom "lit", encodeLit lit]
 encodeExpr (VarE name) = List [Atom "var", Atom name]
@@ -181,6 +182,7 @@ encodeExpr (Block es) = List (Atom "block" :: map encodeExpr es)
 encodeExpr (BinOpE op a b) = List [Atom "binop", Atom (binopToAtom op), encodeExpr a, encodeExpr b]
 encodeExpr (UnOpE op e) = List [Atom "unop", Atom (unaryToAtom op), encodeExpr e]
 
+covering
 decodeExpr : SExpr -> Either ParseError Expr
 decodeExpr (List (Atom tag :: rest)) =
   case tag of
@@ -273,12 +275,14 @@ decodeParam (List [Atom name, ty]) = do
   pure (name, t)
 decodeParam _ = Left (Invalid "param must be (name ty)")
 
+covering
 encodeDecl : Decl -> SExpr
 encodeDecl (Fn name params ret body) =
   List [Atom "fn", Atom name, List (map encodeParam params), encodeTy ret, encodeExpr body]
 encodeDecl (TypeDecl name ty) =
   List [Atom "type", Atom name, encodeTy ty]
 
+covering
 decodeDecl : SExpr -> Either ParseError Decl
 decodeDecl (List (Atom "fn" :: Atom name :: List params :: ret :: body :: [])) = do
   ps <- traverse decodeParam params
@@ -291,17 +295,20 @@ decodeDecl (List (Atom "type" :: Atom name :: ty :: [])) = do
 decodeDecl _ = Left (Invalid "unknown decl")
 
 public export
+covering
 fromSExpr : SExpr -> Either ParseError Module
 fromSExpr (List (Atom "module" :: Atom name :: List decls :: [])) = do
   ds <- traverse decodeDecl decls
   pure (MkModule name ds)
 fromSExpr _ = Left (Invalid "expected (module name (decls...))")
 
 public export
+covering
 toSExpr : Module -> SExpr
 toSExpr (MkModule name decls) =
   List [Atom "module", Atom name, List (map encodeDecl decls)]
 
 public export
+covering
 encode : Module -> String
 encode = show . toSExpr