From ce7b87e8b410d60c8d629f28dddffae41f4aa8ce Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 17:31:30 +0100 Subject: [PATCH] proof(SafeColor): DISCHARGE WCAG threshold anchors via Refl MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Both SafeColor OWEDs are definitional unfolds — `meetsWCAG_AA` and `meetsWCAG_AAA` are `public export` with bodies `contrastRatio c1 c2 >= 4.5` and `contrastRatio c1 c2 >= 7.0` respectively (SafeColor.idr L188-194). The LHS of each proof unfolds directly to the RHS for `Refl`. The OWED comments cited "Double-comparison opacity" — that blocker only applies if you tried to REDUCE `contrastRatio c1 c2 >= 4.5` to a concrete `True`/`False`. Here we don't reduce; the goal just states the definitional equality between the wrapper and its body. Eighth PR in today's overly-cautious-OWED hunt. Refs hyperpolymath/proven#90 Co-Authored-By: Claude Opus 4.7 (1M context) --- src/Proven/SafeColor/Proofs.idr | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/src/Proven/SafeColor/Proofs.idr b/src/Proven/SafeColor/Proofs.idr index b7ae5b4c..81c097a9 100644 --- a/src/Proven/SafeColor/Proofs.idr +++ b/src/Proven/SafeColor/Proofs.idr @@ -85,12 +85,20 @@ parseHexEmptyRejected = Refl -- OWED markers -------------------------------------------------------------------------------- -||| OWED: WCAG-AA threshold = 4.5. Blocked on Double-comparison opacity. +||| DISCHARGED: WCAG-AA threshold = 4.5. `meetsWCAG_AA` is `public +||| export` with body `contrastRatio c1 c2 >= 4.5` (SafeColor.idr +||| L188-189), so the LHS unfolds directly to the RHS for `Refl`. No +||| Double-comparison reduction is needed — both sides are literally +||| the same expression. public export -0 wcagAAThreshold : +wcagAAThreshold : (c1, c2 : RGB) -> meetsWCAG_AA c1 c2 = (contrastRatio c1 c2 >= 4.5) +wcagAAThreshold _ _ = Refl -||| OWED: WCAG-AAA threshold = 7.0. Same blocker. +||| DISCHARGED: WCAG-AAA threshold = 7.0. `meetsWCAG_AAA` is `public +||| export` with body `contrastRatio c1 c2 >= 7.0` (SafeColor.idr +||| L193-194) — same unfolding pattern as `wcagAAThreshold`. public export -0 wcagAAAThreshold : +wcagAAAThreshold : (c1, c2 : RGB) -> meetsWCAG_AAA c1 c2 = (contrastRatio c1 c2 >= 7.0) +wcagAAAThreshold _ _ = Refl