From e2abf3a13edb3a1421390c4602aab837953c386b Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 30 May 2026 23:56:41 +0100
Subject: [PATCH] proof(SafePassword): DISCHARGE withMinLengthCorrect via
 nested constructor case-split (proven#90 #107)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The OWED comment for `withMinLengthCorrect` correctly diagnosed the
blocker (record-update through `MkPolicyBuilder` wrapper doesn't
reduce for abstract builder) and suggested case-split. Empirically
verified that a DOUBLE case-split is needed — both the outer
`MkPolicyBuilder` and the inner `MkPolicy` constructor must be
exposed for the projection `({ minLength := n } p).minLength` to
reduce to `n`.

DISCHARGE (one line):

```idris
withMinLengthCorrect n (MkPolicyBuilder (MkPolicy _ _ _ _ _ _ _ _ _ _)) = Refl
```

The 10 underscores correspond to PasswordPolicy's 10 fields
(`minLength`, `maxLength`, `requireUppercase`, `requireLowercase`,
`requireDigit`, `requireSymbol`, `minUniqueChars`,
`maxRepeatedChars`, `forbiddenPatterns`, `forbiddenWords`).

Test harness verified at `/tmp/charrefl/src/TestPolicyBuilder.idr` —
single case-split on `MkPolicyBuilder _` alone is NOT sufficient
because `{minLength := n} p` doesn't reduce through abstract `p`.
Both layers needed.

The sister OWED `chainedBuildersCompose` (line 430) is NOT
discharged in this PR — it requires reducing `Policy.policyBuilder`
(a top-level constant) which still trips the record-projection-
through-top-level-constant blocker we hit in SafeCSV PR #137.
Discharge of that one waits for either an Idris2 0.8.0 fix or a
named-constant-bridge lemma technique.

Zero `believe_me`/`postulate`/`idris_crash`.

Refs proven#90 (Phase 3 OWED triage), proven#107 (overly-cautious
OWED meta).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 src/Proven/SafePassword/Proofs.idr | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

diff --git a/src/Proven/SafePassword/Proofs.idr b/src/Proven/SafePassword/Proofs.idr
index 83771b94..2e526b10 100644
--- a/src/Proven/SafePassword/Proofs.idr
+++ b/src/Proven/SafePassword/Proofs.idr
@@ -402,18 +402,19 @@ public export
 public export
 0 builderProducesPolicy : build Policy.policyBuilder = Policy.defaultPolicy
 
-||| OWED: `withMinLength n` followed by `build` yields a policy whose
-||| `minLength` field equals `n`. The implementation is
-||| `withMinLength n (MkPolicyBuilder p) = MkPolicyBuilder ({minLength
-||| := n} p)`, so the equation is true by record-update normalisation
-||| — but Idris2 0.8.0 does not reduce the record-update through the
-||| `MkPolicyBuilder` wrapper for an abstract starting builder
-||| `b : PolicyBuilder`. Discharge by case-splitting on
-||| `b = MkPolicyBuilder _` plus `Refl`, or by marking `build` and
-||| `withMinLength` `%inline`.
+||| DISCHARGED: `withMinLength n` followed by `build` yields a policy
+||| whose `minLength` field equals `n`. The OWED comment suggested the
+||| pattern: case-split on `b = MkPolicyBuilder _` to expose the
+||| constructor. Verified empirically that a DOUBLE case-split
+||| (`MkPolicyBuilder (MkPolicy _ _ _ _ _ _ _ _ _ _)`) is needed —
+||| the inner `PasswordPolicy` constructor also has to be exposed for
+||| the record-update projection `({ minLength := n } p).minLength`
+||| to reduce. Once both are exposed, the chain collapses to `Refl`.
+||| Test at `/tmp/charrefl/src/TestPolicyBuilder.idr`.
 public export
-0 withMinLengthCorrect : (n : Nat) -> (b : PolicyBuilder) ->
-                         minLength (build (withMinLength n b)) = n
+withMinLengthCorrect : (n : Nat) -> (b : PolicyBuilder) ->
+                       minLength (build (withMinLength n b)) = n
+withMinLengthCorrect n (MkPolicyBuilder (MkPolicy _ _ _ _ _ _ _ _ _ _)) = Refl
 
 ||| OWED: chained builder calls compose correctly — `withMinLength n
 ||| (withUppercase policyBuilder)` then `build`'s `minLength` is `n`.