Skip to content

Commit 4057f22

Browse files
proof(SafeColor): DISCHARGE WCAG-AA + WCAG-AAA threshold anchors via Refl (proven#90) (#105)
Ninth "overly cautious OWED" discharge of today's [proven#90 Phase 3](#90) campaign. ## What it does \`\`\`idris public export wcagAAThreshold : (c1, c2 : RGB) -> meetsWCAG_AA c1 c2 = (contrastRatio c1 c2 >= 4.5) wcagAAThreshold _ _ = Refl public export wcagAAAThreshold : (c1, c2 : RGB) -> meetsWCAG_AAA c1 c2 = (contrastRatio c1 c2 >= 7.0) wcagAAAThreshold _ _ = Refl \`\`\` ## Why it works \`meetsWCAG_AA\` and \`meetsWCAG_AAA\` are \`public export\` with these exact expressions as their bodies (SafeColor.idr L188-194). The LHS unfolds directly to the RHS for \`Refl\` — no Double-comparison reduction needed. 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; we just state the definitional equality between the wrapper and its body. Refs #90 Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent a6700dc commit 4057f22

1 file changed

Lines changed: 12 additions & 4 deletions

File tree

src/Proven/SafeColor/Proofs.idr

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -85,12 +85,20 @@ parseHexEmptyRejected = Refl
8585
-- OWED markers
8686
--------------------------------------------------------------------------------
8787

88-
||| OWED: WCAG-AA threshold = 4.5. Blocked on Double-comparison opacity.
88+
||| DISCHARGED: WCAG-AA threshold = 4.5. `meetsWCAG_AA` is `public
89+
||| export` with body `contrastRatio c1 c2 >= 4.5` (SafeColor.idr
90+
||| L188-189), so the LHS unfolds directly to the RHS for `Refl`. No
91+
||| Double-comparison reduction is needed — both sides are literally
92+
||| the same expression.
8993
public export
90-
0 wcagAAThreshold :
94+
wcagAAThreshold :
9195
(c1, c2 : RGB) -> meetsWCAG_AA c1 c2 = (contrastRatio c1 c2 >= 4.5)
96+
wcagAAThreshold _ _ = Refl
9297

93-
||| OWED: WCAG-AAA threshold = 7.0. Same blocker.
98+
||| DISCHARGED: WCAG-AAA threshold = 7.0. `meetsWCAG_AAA` is `public
99+
||| export` with body `contrastRatio c1 c2 >= 7.0` (SafeColor.idr
100+
||| L193-194) — same unfolding pattern as `wcagAAThreshold`.
94101
public export
95-
0 wcagAAAThreshold :
102+
wcagAAAThreshold :
96103
(c1, c2 : RGB) -> meetsWCAG_AAA c1 c2 = (contrastRatio c1 c2 >= 7.0)
104+
wcagAAAThreshold _ _ = Refl

0 commit comments

Comments
 (0)