proof(SafePassword): annotate 25 bodyless decls as OWED (Refs standards#158) (#59)

## Summary

Annotates all 25 bodyless declarations in
`src/Proven/SafePassword/Proofs.idr` as **OWED-with-justification**, per
the convention established 2026-05-20 by SafeChecksum (reference:
`src/Proven/SafeChecksum/Proofs.idr` L24-L137) and replicated across
SafeBuffer / SafeCryptoAccel / SafeHKDF / SafeBloom / SafeFPGA /
SafeAPIKey / SafeHtml / SafeMath and 10 other Safe* siblings.

Refs hyperpolymath/standards#158.

## Form (matches SafeChecksum)

- Triple-pipe `|||` doc block stating claim + Idris2 0.8.0 blocker +
discharge condition
- `public export` followed by leading `0 ` (erased multiplicity,
runtime-stripped)
- Bare type signature, otherwise unchanged
- No `postulate` keyword (estate-wide choice)
- Zero `believe_me`, zero `idris_crash`
- Discoverable as named declarations (vs silent / commented-out)

The single non-OWED proof in the file, `policyCheckDeterministic`,
discharges by `Refl` and is left untouched.

## Blocker families

The 25 OWED items cluster into four families documented in the module
header:

1. **String FFI opacity** — `unpack` / `length` / `toLower` /
`isInfixOf` / `elem` on abstract `String` are FFI-bound and do not
type-level reduce in Idris2 0.8.0. Same blocker family as SafeChecksum's
`luhnValidatesKnownGood`.
2. **`Char`-class FFI opacity** — `isUpper` / `isLower` / `isDigit` /
`isSpace` / `isAlphaNum` are FFI-bound `Char` primitives.
3. **`covering` (non-`total`) reducer barrier** — `analyzeStrength`,
`quickStrengthCheck`, `meetsRequirement`, and `detectPatterns` are
declared `covering` because the `windows`/`drop`-based helper in
`detectDatePattern` defeats the totality checker. Same shape as
SafeMath's `gcd` family (`src/Proven/SafeMath/Proofs.idr` L167-L197).
4. **External KDF opacity** — Argon2id / bcrypt / scrypt / PBKDF2 are
external (FFI to native crypto libraries); the per-field `if`-chains in
`validateArgon2Params` / `validateBcryptParams` / `validateScryptParams`
do not reduce by `Refl` for an abstract `params : XParams` until
case-analysed.

## Per-decl claim + reason

### Policy Compliance (4)

| Decl | Claim | Blocker family |
|---|---|---|
| `validPasswordLength` | `null (checkPolicy …) = True` implies both
`length pwd >= minLength` and `length pwd <= maxLength` | 1 (String FFI)
|
| `emptyPasswordFails` | `minLength > 0` implies `null (checkPolicy
policy "") = False` | 1 (`unpack ""` not definitionally `[]`) |
| `longerPasswordBetter` | violation-list length is monotone-down in
password length | 1 + per-checker monotonicity lemmas |

### Hash Security (5)

| Decl | Claim | Blocker family |
|---|---|---|
| `argon2ParamsValid` | `validateArgon2Params = Right` implies OWASP
minima on t/m/p | 4 (KDF opacity in `if`-chain) |
| `bcryptCostBounded` | `validateBcryptParams = Right` implies `cost ∈
[10, 31]` | 4 |
| `defaultArgon2Valid` | default Argon2 params clear validation | 4
(Nat-literal `<` doesn't reduce) |
| `defaultBcryptValid` | default Bcrypt params clear validation | 4 |
| `defaultScryptValid` | default Scrypt params clear validation | 4 |

### Constant-Time Comparison (3)

| Decl | Claim | Blocker family |
|---|---|---|
| `constantTimeRefl` | `constantTimeHashCompare h h = True` |
`Data.Bits` `xor x x = 0` not exposed as Refl |
| `constantTimeSym` | `cthCompare` is symmetric | `xor`-commutativity
over `Bits8` not exposed |
| `differentLengthNoMatch` | different lengths never match | Bool-Prop
reflection gap on `/=` (same as SafeAPIKey `formatMismatchRejected`) |

### Strength Analysis (5)

| Decl | Claim | Blocker family |
|---|---|---|
| `strengthScoreBounded` | `score <= 100` | 3 (`covering`
`analyzeStrength`) |
| `entropyNonNegative` | `entropy >= 0.0` | 3 + `Double` non-negativity
lemma needed |
| `longerHigherEntropy` | longer pwd implies higher-or-equal entropy | 1
+ 2 + 3 stacked |
| `veryStrongMax` | `level <= VeryStrong = True` | custom `Ord
StrengthLevel` not via `Cast → Fin 5` |
| `strengthTransitive` | `<=` is transitive on `StrengthLevel` | same
`Ord`-derivation gap as `veryStrongMax` |

### Pattern Detection (2)

| Decl | Claim | Blocker family |
|---|---|---|
| `commonPasswordDetected` | common-password match implies
`CommonPassword` in `detectPatterns` | 1 + 3 |
| `patternPenaltyNonNeg` | `patternPenalty p >= 0` (trivially: `Nat >=
0`) | per-constructor `Refl` not auto-derived |

### Rehash Decision (2)

| Decl | Claim | Blocker family |
|---|---|---|
| `paramsAtLeastRefl` | `paramsAtLeast p p = True` | 4 (nested
case-analysis) |
| `strongerRequiresRehash` | asymmetric component of the partial order |
4 + `PartialOrder`-class refactor needed |

### Policy Builder (3)

| Decl | Claim | Blocker family |
|---|---|---|
| `builderProducesPolicy` | `build policyBuilder = defaultPolicy` |
`MkPolicyBuilder` newtype not unwrapped |
| `withMinLengthCorrect` | `minLength (build (withMinLength n b)) = n` |
same as `builderProducesPolicy` |
| `chainedBuildersCompose` | chained builder calls compose on disjoint
fields | reduces to `withMinLengthCorrect` |

### Requirement Satisfaction (2)

| Decl | Claim | Blocker family |
|---|---|---|
| `higherImpliesLower` | meeting higher requirement implies meeting
lower | 3 + `veryStrongMax`-style derivation gap |
| `veryStrongSatisfiesAll` | `quickStrengthCheck = VeryStrong` satisfies
all requirements | composes `veryStrongMax` + `strengthScoreBounded` |

## Scope

- Touches only `src/Proven/SafePassword/Proofs.idr`
- 25 declarations annotated; the lone non-OWED proof
`policyCheckDeterministic` (discharges by `Refl`) is unchanged
- No other files touched (Hash.idr / Policy.idr / Strength.idr / FFI /
bindings all untouched)

## 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)

## Test plan

- [ ] Idris2 0.8.0 `--check` on `src/Proven/SafePassword/Proofs.idr`
once estate base-package binary incompatibility is unjammed (local
`idris2 --build proven.ipkg` currently errors on `base >= 0.6.0`
resolution — same baseline-rot mentioned in PR #41)
- [ ] Verify no downstream module shadows the names (grep was clean at
edit time)
- [ ] Owner review of OWED reasons against SafeChecksum precedent

## Why draft

Filed DRAFT pending CI / base-package unjam, matching sibling PRs #37 /
#41 / #46 / #52 in this campaign.

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

Author: hyperpolymath