Totality refactor: SafePassword.Strength.{detectPatterns, analyzeStrength, ...} (covering → total)

[hyperpolymath]

Summary

src/Proven/SafePassword/Strength.idr declares 7 functions as covering (not total):

• detectPatterns (line 154)
• analyzeStrength (line 239)
• 5 others at lines 346, 351, 356, 380

The root cause is a single helper, inside detectPatterns.detectDatePattern.windows:

```idris
windows : Nat -> List a -> List (List a)
windows _ [] = []
windows n xs = if length xs < n then [] else take n xs :: windows n (drop 1 xs)
```

drop 1 xs does not give the Idris2 0.8.0 totality checker a structurally-decreasing argument it can verify, so windows is marked covering. That covering propagates up through detectDatePattern → detectPatterns → analyzeStrength → all downstream callers.

Refactor needed

Rewrite windows so totality is structurally evident. Options (any of):

• Length-indexed Vect: change the signature to windows : (n : Nat) -> Vect k a -> Vect (k - n) (Vect n a) (or similar) so structural recursion on the outer Vect is visible.
• assert_smaller on the recursive call: windows n (drop 1 xs) becomes windows n (assert_smaller xs (drop 1 xs)) — escape hatch, not a true refactor, but unblocks the chain. Acceptable per the existing src/Proven/SafeInput.idr:282 precedent.
• Fuel-bounded variant: windowsFuel : Nat -> Nat -> List a -> List (List a) with a per-call fuel parameter; expose windows = windowsFuel maxBound.
• Replace with Data.List.Quantifiers or contrib's window helper if a total equivalent exists.

Recommendation: assert_smaller for the minimum-churn fix; or full Vect refactor if downstream call sites can tolerate the type change.

OWED sites that discharge once this lands

Per the per-site classification in docs/proof-debt-triage-tier-a.md (Phase 2 Days 3-10, ~209 sites):

• src/Proven/SafePassword/Proofs.idr:257 — strengthScoreBounded (~60 min after totality)
• src/Proven/SafePassword/Proofs.idr:454 — higherImpliesLower (~50 min after totality)
• src/Proven/SafePassword/Proofs.idr:471 — veryStrongSatisfiesAll (~40 min after totality)

Total downstream proof work: ~2.5h once totality lands. The refactor itself is estimated 2-4h.

Acceptance criteria

• src/Proven/SafePassword/Strength.idr builds with %default total (no covering declarations).
• Existing tests pass (proven.ipkg + tests.ipkg).
• The 3 OWED sites above land as discharged theorems in a follow-up PR.

Related

• Phase 2 triage plan: docs/proof-debt-triage.md §8 Days 11-14.
• Per-site disposition: docs/proof-debt-triage-tier-a.md § SafePassword.
• Family 3 (covering/totality) is one of 7 blocker families in PROOF-NEEDS.md.

🤖 Filed by Claude during Phase 2 Days 11-14 of the proof-debt triage.