proof(SafeBase64): annotate 22 bodyless decls as OWED (Refs standards#158) (#64)

## Summary

22 bodyless declarations in `src/Proven/SafeBase64/Proofs.idr` are
converted from `export <sig>` (no body) into the canonical estate OWED
form: `0 <sig>` (erased multiplicity) with a `||| OWED:` docstring that
names the Idris2 0.8.0 blocker and the unblocking condition. Matches the
convention established in `Proven.SafeChecksum.Proofs` and the
recently-merged sibling PRs (#37 SafeAPIKey, #41 SafeHtml, #46 SafeMath,
#49 SafeNetwork, #51 SafeEnv, #52 SafeTOML, #53 SafeCSRF, #54
SafeString).

Refs hyperpolymath/standards#158.

## Blocker partitioning

The 22 OWED decls cluster into four well-known Idris2 0.8.0 blocker
families:

### 1. String FFI opacity (`pack` / `unpack` / `elem` / `length` /
`index'` non-Refl)

Same blocker family as `SafeChecksum.luhnValidatesKnownGood` and
`SafeHtml.escapePreservesNoLT`.

- `standardAlphabetValid` — `elem c (unpack standardAlphabet)` is opaque
- `urlSafeAlphabetValid` — same shape for URL-safe alphabet
- `encodeOutputValid` — `all (isValidOutputChar variant) (unpack ...)`
over `pack`-wrapped encoder output
- `variantsEqualLength` — `length (unpack s)` non-Refl
- `noPadShorter` — `length . unpack` + Bool `<=` reflection
- `invalidCharDetected` — `elem` + `unpack` + `decode` chained opacity
- `invalidPaddingDetected` — `index' . unpack` + `length . unpack`
non-Refl
- `mimeLineBreaksCorrect` — `split . encodeBytesToString MIME` + `length
. unpack` chain
- `mimeIgnoresWhitespace` — `pack . filter . unpack` (the
`stripWhitespace` definition) non-Refl
- `urlSafeContainsNoUnsafe` — `all . unpack . encodeBytesToString
URLSafe` chain
- `standardMayContainUnsafe` — `elem . unpack . encodeBytesToString
Standard` disjunctive witness

### 2. `Data.Bits` non-Refl on `Bits8` shift/and operations (compound
blocker)

The encoder/decoder pair compose `pack`/`unpack` with `Bits8`
bit-manipulation (`shiftL` / `shiftR` / `.&.` from `Data.Bits`) whose
`Refl`-normalisation is not exposed through the `Bits` type-class
projection.

- `roundtripCorrect` — fundamental round-trip
- `roundtripEmpty` — empty-input round-trip
- `roundtripSingleByte` — 1-byte padding-arm round-trip
- `roundtripString` — string-level round-trip (transitively on
`roundtripCorrect`)
- `segmentedRoundtrip` — transitively on `roundtripCorrect`

### 3. `Integral Nat` type-class projection non-unfolding (`div` /
`mod`)

Same blocker as `SafeChecksum.sumChecksumEmpty` (`0 \`mod\` 256 = 0`
non-Refl).

- `paddedLengthMultipleOf4` — `(encodedLength variant n) \`mod\` 4 = 0`
non-Refl
- `decodedLengthBound` — Bool `<=` + `div` chain
- `encodingIncreasesLength` — chained `Nat` `div` / `>=` inequalities
- `threeToFourRatio` — `(n + 2) \`div\` 3 = n \`div\` 3` under `n
\`mod\` 3 = 0`
- `paddingMatchesRemainder` — `countPadding . encodeBytesToString` +
`Integral Nat` `mod`

### 4. `case` / `with` not retaining equational witness through opaque
function application

Same shape as boj-server's class-J Bool-vs-Prop reflection gap
(`Boj.SafetyLemmas.charEqSym`).

- `decodeNeverCrashes` — case-split on `decode variant input` does not
produce a Refl chain back to the scrutinee

## Phase 1 attempt (try to discharge as real proofs)

Per the runbook, I considered Phase 1 before applying OWED. All 22
signatures are in the four blocker families above, each of which has
already been established in merged sibling PRs as genuinely irreducible
in Idris2 0.8.0 (the same `pack`/`unpack` opacity that blocks
`SafeHtml.escapePreservesNoLT` blocks every String-passing decl here;
the same `Data.Bits` non-Refl that blocks the boj-server class-J posture
blocks every `Bits8`-chunking round-trip here). No new Phase 1 territory
is available — these are honest claims, parked behind well-understood
Idris2 0.8.0 limitations.

## Phase 2 outcome (OWED applied)

All 22 decls now use the SafeChecksum-style OWED form:

```idris
||| OWED: <claim restated, with witness sketch>
||| Held back by <Idris2 0.8.0 blocker, with cross-reference to
||| sibling OWED decl in the same family>. Discharge once <unblocking
||| condition>.
0 declarationName : <signature>
```

The companion alias `encodingPreservesOrder = roundtripCorrect` is also
converted to `0 ` multiplicity so that the file remains coherent — a
default-multiplicity decl cannot reference a `0 ` decl. The alias's
semantics are unchanged (equality proofs are erased at runtime anyway).

## Verification

- Local `idris2 --build proven.ipkg` is gated behind a long-running
estate `--install` (other session), so the in-worktree build is queued.
The conversion is mechanical and matches the merged sibling-PR
convention exactly; CI on this PR will be the authoritative oracle.
- No external callers anywhere in `src/` or `tests/` (`grep -rn` clean
for all 22 names plus `encodingPreservesOrder` — only the def-sites and
intra-docstring cross-references remain).
- Visibility shift `export -> 0` matches the merged PR #54 (SafeString)
pattern: `+0 concatLength`, `+0 trimNoWhitespace`, etc.

## Why draft

Filed DRAFT per the convention (estate CI jam) so the owner can
land/merge once the estate-wide proven CI queue settles and after the
parallel `--install` completes.

## Test plan

- [ ] `idris2 --check --total` green on the touched module (gated on
estate CI queue).
- [x] No regressions: callers grep clean for all 22 names +
`encodingPreservesOrder`.
- [x] Convention match: visible only via erased `0 ` multiplicity (no
`believe_me`, no `postulate`, no `assert_total`).
- [ ] Owner-side: ratify against any other in-flight SafeBase64 edits
before merging.

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

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

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

Author: hyperpolymath