proof(SafePassword): TENTATIVE DISCHARGE 3 default-params validators via Refl (proven#90, #107) (#118)

MEDIUM-confidence experiment per
[proven#107](#107) —
concrete-literal if-chain reduction.

\`\`\`idris
public export
defaultArgon2Valid : isRight (validateArgon2Params
Hash.defaultArgon2Params) = True
defaultArgon2Valid = Refl

public export
defaultBcryptValid : isRight (validateBcryptParams
Hash.defaultBcryptParams) = True
defaultBcryptValid = Refl

public export
defaultScryptValid : isRight (validateScryptParams
Hash.defaultScryptParams) = True
defaultScryptValid = Refl
\`\`\`

All three OWEDs cite "Nat-literal normalisation gap". If Idris2 0.8.0
reduces literal-vs-literal comparisons (`3 < 1 = False`, `65536 < 8192 =
False`, etc.) structurally, Refl closes.

This is one of the higher-uncertainty experiments — Nat `<` on literals
MAY or MAY NOT reduce without an explicit case-split. If CI rejects,
close and revert.

Refs #90 #107

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

Author: hyperpolymath

src/Proven/SafePassword/Proofs.idr

@@ -172,25 +172,21 @@ public export
 ||| available, or refactor `defaultArgon2Params` to `Bits32`-typed
 ||| fields that reduce eagerly.
 public export
-0 defaultArgon2Valid : isRight (validateArgon2Params Hash.defaultArgon2Params) = True
-
-||| OWED: `defaultBcryptParams` (`cost = 12`) clears
-||| `validateBcryptParams`. Same Nat-literal-normalisation blocker as
-||| `defaultArgon2Valid` (Family 4) — the `if 12 < 10 then … else if
-||| 12 > 31 then … else Right p` chain does not reduce by `Refl`
-||| despite both leaves being constant-folded. Discharge once a
-||| `Data.Nat` reflective tactic for `<` / `>` on literal `Nat`s is
-||| available.
+defaultArgon2Valid : isRight (validateArgon2Params Hash.defaultArgon2Params) = True
+defaultArgon2Valid = Refl
+
+||| TENTATIVE DISCHARGE: `defaultBcryptParams` (`cost = 12`) clears
+||| `validateBcryptParams`. Concrete-literal if-chain.
 public export
-0 defaultBcryptValid : isRight (validateBcryptParams Hash.defaultBcryptParams) = True
+defaultBcryptValid : isRight (validateBcryptParams Hash.defaultBcryptParams) = True
+defaultBcryptValid = Refl
 
-||| OWED: `defaultScryptParams` (`n=16384, r=8, p=1, keyLength=32`)
-||| clears `validateScryptParams`. Same Nat-literal-normalisation
-||| blocker as `defaultArgon2Valid` / `defaultBcryptValid` (Family 4).
-||| Discharge once a `Data.Nat` reflective tactic for `<` on literal
-||| `Nat`s is available.
+||| TENTATIVE DISCHARGE: `defaultScryptParams` (`n=16384, r=8, p=1,
+||| keyLength=32`) clears `validateScryptParams`. Concrete-literal
+||| if-chain over 4 fields.
 public export
-0 defaultScryptValid : isRight (validateScryptParams Hash.defaultScryptParams) = True
+defaultScryptValid : isRight (validateScryptParams Hash.defaultScryptParams) = True
+defaultScryptValid = Refl
 
 --------------------------------------------------------------------------------
 -- Constant-Time Comparison Proofs