proof(SafeAPIKey): emptyKeyRejected + fullMaskFormat fail to reduce (Idris2 0.8.0) #95

Background

Surfaced during sibling audit for #92 (qualified-projection fix).
Two Refl proofs in `src/Proven/SafeAPIKey/Proofs.idr` fail to
type-check under Idris2 0.8.0, but the root cause is not the
same as #92's shadowing bug — it's FFI primitive reduction.

Failing proofs

1. `emptyKeyRejected : mkAPIKey "" = Nothing` (line 21)

Idris2 0.8.0 error:
```
Can't solve constraint between: Nothing and
with block in mkAPIKey "" (choose (length "" >= MinKeyLength))
```

`mkAPIKey` is defined as:
```idris
mkAPIKey : String -> Maybe APIKey
mkAPIKey s with (choose (length s >= MinKeyLength))
mkAPIKey s | Left _ = Nothing
mkAPIKey s | Right _ = Just (MkAPIKey s ...)
```

The `with` block doesn't fully reduce on a concrete `""` because
`length`/`>=` go through String FFI primitives that Idris2 0.8.0
doesn't type-level reduce. Same blocker family as the
`SafeChecksum` Luhn/ISBN OWED items.

2. `fullMaskFormat : (key : APIKey) -> isPrefixOf "[REDACTED:" (fullMask key) = True` (line 76)

Idris2 0.8.0 error:
```
Can't solve constraint between: True and
isPrefixOfBy (==) (unpack (fromString "[REDACTED:"))
(unpack (fullMask key))
```

`fullMask` is `"[REDACTED:" ++ show (length key.raw) ++ " chars]"`.
`isPrefixOf` ought to match on the leading literal, but `++`/`unpack`
chains through FFI String primitives that don't reduce universally
quantified `key.raw`.

Why these are NOT a #92 dup

#92 is about `isOriginAllowed defaultPolicy origin = False` where the
problem was the type-signature binding `defaultPolicy` as a fresh
implicit (shadowing warning emitted). Qualifying the name fixed it.

Here:

• `emptyKeyRejected` has `""` (literal, not an identifier) — no shadowing.
• `fullMaskFormat` quantifies over `(key : APIKey)` — the variable
  binder is correct and intentional.

Both failures are FFI-primitive reduction issues, not name resolution.

Proposed fix paths

For `emptyKeyRejected`

Either:

• Refactor `mkAPIKey` to a `case` split that exposes the empty-string
  decision propositionally (e.g. dispatch on `Dec (length s = 0)` first).
• Or rewrite the proof via a `smallStringRejected` bridge lemma that
  case-splits on `choose` directly.

For `fullMaskFormat`

Either:

• Strengthen `isPrefixOf` for the `literal ++ rest` shape via a small
  helper lemma (`isPrefixOfConcatLeft : isPrefixOf s (s ++ t) = True`).
• Or weaken the property — e.g. `startsWith` over `Char` lists instead
  of FFI String.

Acceptance

• `emptyKeyRejected` type-checks
• `fullMaskFormat` type-checks
• Add `Proven.SafeAPIKey.Proofs` to `proven.ipkg` modules list
  (was excluded by proof(SafeCORS): qualify defaultPolicy to fix 4 broken Refl proofs (#92) #94 because of these two failures)
• CI `Idris 2 CI` green

Refs #92 (sibling audit surfaced this)
Refs #94 (which adds `SafeCORS.Proofs` to ipkg but excludes this file)