proof(SafeJWT): annotate 16 bodyless decls as OWED (Refs standards#158) (#62)

## Summary

Converts the 16 bodyless declarations in `src/Proven/SafeJWT/Proofs.idr`
from terse `Depends on Idris2 SafeJWT … implementation correctness.`
comments to the estate's **OWED-with-justification** convention
established 2026-05-20 across SafeChecksum / Buffer / CryptoAccel / HKDF
/ Bloom / FPGA / SafeAPIKey / SafeHtml / SafeMath / SafeTOML / SafeEnv /
SafeNetwork / SafeOTP / SafeCSRF / SafeString:

- Triple-pipe `|||` doc-comment stating the claim
- `0 ` (erased multiplicity) so the postulate is not runtime-callable
- Bare signature, no `postulate` keyword
- Explicit Idris2 0.8.0 blocker + discharge condition
- `[Category X]` tag classifying the OWED into one of 5 families

Refs hyperpolymath/standards#158.

## Category taxonomy (5 families for these 16 OWED items)

### Category A — Result-monad soundness through String/Integer FFI (6
items)

The validators (`validateExp`, `validateNbf`, `validateIssuer`,
`validateAudience`, `validateRequiredClaims`, `validateMaxAge`) all
return `Result JWTError ()`. The proofs read `isOk validateX = True` and
want to recover the underlying Bool/Prop precondition. Closing each
requires either (a) a `Bool`-vs-`Prop` reflection lemma on the relevant
FFI primitive (`prim__strEq`, `Integer` `<`/`>`/`>=`, `Data.List.elem`),
or (b) an `ifFalseElim`/`ifTrueElim` lemma to walk back through the
`if/then/else` decision head.

- `expValidationSound` — `Integer` `>` opacity + `if/then/else` over
Bool head
- `nbfValidationSound` — same family as `expValidationSound`
- `issuerValidationSound` — `prim__strEq` opacity (class-J: same shape
as boj-server `charEqSound`, gossamer `stringNotEqCommut`)
- `audienceValidationSound` — `Data.List.elem` over `String` (composes
with String-FFI)
- `requiredClaimsPresent` — `List` recursion +
`getClaim`/`hasRequiredClaim` lookup over `String`-keyed list
- `maxAgeValidationSound` — `tokenAge` case-split + `Integer` `>`
opacity + `cast : Nat -> Integer` partial reduction

### Category B — Cryptographic FFI primitives (3 items)

`verifySignature` (Validate.idr L231-L270) routes through
`prim__verifyHMAC` / `prim__verifyRSA` / `prim__verifyECDSA` /
`prim__verifyEdDSA` — all FFI-bound cryptographic primitives that encode
the underlying hardness assumption and are completely opaque to the type
checker. Same trust posture as boj-server's I7 FFI-correctness
assumptions.

- `keyMustMatchAlgorithm` — top guard `if not (isKeyValidForAlgorithm
key alg) then Err _ else …`
- `noKeyOnlyForNone` — `NoKey` arm + `alg == None` Bool decision (enum
`Eq` reflection gap)
- `secretKeyRequiresHMAC` — `SecretKey` arm + 14-arm `JWTAlgorithm` enum
case-split to align `isKeyValidForAlgorithm` with `isSymmetric`

### Category C — Composition / reverse-construction (2 items)

- `fullValidationImpliesAll` — closing requires `Result`'s `>>=`
bind-projection (`(m >>= k) = Ok x -> exists y. m = Ok y`), plus `when`
Bool-head opacity, plus record-projection opacity on `opts.validateExp`
etc.
- `validatedJWTFromValidation` — **structurally OWED**, not a reduction
gap. `ValidatedJWT` is a plain record with no proof field carrying its
`validate` provenance, so the implication "every `ValidatedJWT` came
from `validate`" is a **module-discipline invariant**, not a type-level
one. Direct analogue of `SafeTOML.dateComponentsValid` (PR #52) —
discharge by refactoring `ValidatedJWT` to a smart-constructor /
dependent record carrying a `validate`-provenance proof field, or by
hiding `MkValidatedJWT` from the public API and re-exporting only
`validate`.

### Category D — Negative soundness through `validateAlgorithm` guard (2
items)

- `rejectNonePreventsNone` — composes record-projection,
`algEqSound`-style reflection, and `Result`-bind `Err`-propagation
- `allowedAlgorithmsRestrictive` — same composition + `Data.List.elem`
reflection

Both close in 3 `rewrite` + `Refl` steps once the three lemmas they
depend on (record-projection reduction, `algEqSound`, `Result`-bind
projection) land.

### Category E — Attack-prevention compositions (3 items)

- `algorithmConfusionPrevented` — 8-arm `SigningKey` case-split + the
same `noneNotSecure`-shaped `absurd Refl` cascade. Mechanically
derivable (~10 lines, structurally identical to `noneNotSecure`), but no
derived "disjointness over a pair of Bool indicator functions" tactic in
Idris2 0.8.0.
- `tokenSubstitutionPrevented` — `prim__strEq` on `"malicious-issuer" /=
"expected-issuer"`. **Same class-J precedent** as gossamer
`stringNotEqCommut` (`%unsafe` + `believe_me ()` over
`prim__eq_String`).
- `replayMitigatedWithMaxAge` — combined blocker family of
`maxAgeValidationSound` + `fullValidationImpliesAll`

## Safety posture

- Zero `believe_me`
- Zero `postulate`
- Zero `idris_crash`
- All `0 `-erased — postulates cannot leak into runtime
- Discoverable as named declarations (vs silent / commented-out)
- Every OWED entry names a category, a blocker, AND a discharge
condition

## Scope

- Touches only `src/Proven/SafeJWT/Proofs.idr` (+386 / -110 lines)
- The 6 proven proofs in this file (`noneNotSecure`, `hmacIsSymmetric`,
`defaultRejectsNone`, `strictAllowsOnlySecure`, `validatedMeansChecked`,
plus the `Predicate` data declarations and `securityGuarantees` doc) are
untouched

## Why draft

CI / Idris2 0.8.0 base-package dependency resolution is jammed
estate-wide on this worktree:
```
Error: Failed to resolve the dependencies for proven:
  Required base >= 0.6.0 but no matching version is installed.
```
Same blocker that gated PRs #37 / #41 / #46 / #52 as DRAFT. Owner to
promote from DRAFT once the base-package install is unjammed. Per-decl
bodies remain bodyless (only the doc and modifiers changed), so the
type-check delta is purely on parse + erased-decl admissibility, which
is conservative.

## Reference pattern

See PR #46 (`SafeMath`) and PR #52 (`SafeTOML`) for the closest
stylistic precedents (`public export` + `0 ` + multi-line doc with
discharge condition).

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

Author: hyperpolymath