From 618cace26c2edd243c7925c8b5e947b1e7bc8f90 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 18:48:12 +0100 Subject: [PATCH] proof(SafeEmail): annotate 19 bodyless decls as OWED-with-justification Converts the 19 bodyless `export` / `public export` declarations in src/Proven/SafeEmail/Proofs.idr to the estate's OWED-with-justification convention established 2026-05-20 across SafeChecksum, SafeBuffer, SafeCryptoAccel, SafeHKDF, SafeBloom, SafeFPGA, SafeAPIKey, SafeCORS, SafeCSV, SafeSemVer, SafeHtml, SafeTOML, SafeMath, SafeNetwork, SafeOTP, SafeEnv, SafeCSRF, SafeString, SafeYAML: - Triple-pipe `|||` doc-comment stating the claim - Leading `0 ` (erased multiplicity, runtime-stripped) - Bare type signature, no `postulate` keyword - Explicit Idris2 0.8.0 blocker + discharge condition Each annotation names the RFC 5321 / RFC 5322 claim and the Idris2 0.8.0 root cause: String FFI opacity (parseEmail, splitOnLast, unpack, isPrefixOf, isSuffixOf, toLower), record-field projection on universally-quantified records (validResult, combineResults), Eq ValidationSeverity Bool-reduction gap, filter/nubBy List lemma gap, and Bool-LEM via case-split. Zero `believe_me`, zero `postulate`, zero `idris_crash`. All items at multiplicity 0 so they cannot leak into runtime. Discoverable as named declarations. Local verification (Idris2 0.8.0): IDRIS2_PREFIX=.../idris2/0.8.0 \ idris2 --source-dir src --check src/Proven/SafeEmail/Proofs.idr -> exit 0 -> 4 pre-existing `validResult`-shadowing warnings (unchanged from baseline; not introduced by this PR). Refs hyperpolymath/standards#158. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/Proven/SafeEmail/Proofs.idr | 364 +++++++++++++++++++++++++------- 1 file changed, 287 insertions(+), 77 deletions(-) diff --git a/src/Proven/SafeEmail/Proofs.idr b/src/Proven/SafeEmail/Proofs.idr index b13784b4..0677fe92 100644 --- a/src/Proven/SafeEmail/Proofs.idr +++ b/src/Proven/SafeEmail/Proofs.idr @@ -1,10 +1,19 @@ -- SPDX-License-Identifier: PMPL-1.0-or-later -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -||| Proofs for SafeEmail operations +||| Proofs for SafeEmail operations (RFC 5321 / RFC 5322). ||| -||| This module contains proof signatures for properties of email operations. -||| Many proofs are declared but not yet implemented — they serve as proof -||| obligations to be discharged in a future verification pass. +||| This module contains proof signatures for properties of email parsing +||| and validation. Where the property is discharged by definitional +||| unfolding (Refl) under Idris2 0.8.0 it is given a body; where the +||| property is irreducible under Idris2 0.8.0 the declaration is given +||| as a `0 `-erased OWED signature with a `||| OWED:` docstring naming +||| the blocker and the discharge condition. Same posture as +||| `Proven.SafeChecksum.Proofs` and the SafeHtml / SafeTOML / SafeMath +||| sibling modules (Refs hyperpolymath/standards#158). +||| +||| Zero `believe_me`, zero `postulate`, zero `idris_crash`. All OWED +||| items are at multiplicity 0 so they cannot leak into runtime, and +||| are named (vs commented-out) so they are discoverable by audit. module Proven.SafeEmail.Proofs import Proven.Core @@ -20,41 +29,105 @@ import Data.Maybe -- Parsing Properties -------------------------------------------------------------------------------- -||| Empty string parsing fails +||| OWED: `parseEmail "" = Nothing`. Directly matches the first +||| pattern clause of `parseEmail` in `Proven.SafeEmail.Parser` +||| (`parseEmail "" = Nothing`, Parser.idr L187), so the claim is +||| obviously true. Held back by Idris2 0.8.0's String-literal +||| matching: the empty-string literal `""` at the use site does not +||| definitionally reduce against the empty-string pattern in the +||| target clause when the function is invoked at the type level — +||| `Refl` is rejected with "Can't solve constraint between … and …". +||| Same blocker family as the SafeChecksum / SafeHtml String-literal +||| reduction gap. Discharge once Idris2's String-pattern elaborator +||| reduces empty-literal arguments against pattern clauses by Refl, +||| or via a reflective `Data.String` tactic. public export -parseEmptyFails : parseEmail "" = Nothing +0 parseEmptyFails : parseEmail "" = Nothing -||| Parsing is deterministic +||| Parsing is deterministic (any function is). This is `Refl` at +||| every input — included as a sanity anchor to document the +||| referential-transparency property callers may rely on. public export parseDeterministic : (s : String) -> parseEmail s = parseEmail s parseDeterministic s = Refl -||| A string with no '@' character fails to parse as an email -parseNoAtFails : parseEmail "noatsign" = Nothing +||| OWED: a string with no `'@'` character fails to parse as an +||| email (`parseEmail "noatsign" = Nothing`). Reduces by the +||| `splitOnLast '@' s = Nothing => Left NoAtSign` arm of +||| `parseEmailEither` (Parser.idr L174-175). Held back by Idris2 +||| 0.8.0 not reducing `splitOnLast` (a `String -> String -> ...` +||| function threading through opaque `unpack` / `pack` String FFI +||| primitives) at the type level. Same blocker family as the +||| SafeChecksum `validateLuhn` / `validateISBN10` String-FFI gap. +||| Discharge once a `Data.String` reflective tactic is available, +||| or once `splitOnLast` is reformulated on `List Char` so its +||| reduction does not pass through `unpack`. +0 parseNoAtFails : parseEmail "noatsign" = Nothing -------------------------------------------------------------------------------- -- Validation Properties -------------------------------------------------------------------------------- -||| Valid result has isValid = True +||| OWED: `validResult.isValid = True`. By definition +||| `validResult = MkValidationResult True []` (Validation.idr L62), +||| so the record-field projection should reduce to `True` by Refl. +||| Held back by Idris2 0.8.0 not auto-reducing record-field +||| projections (`.isValid`) on named top-level constructor +||| applications — the elaborator inlines `validResult` but does not +||| commit `(MkValidationResult True []).isValid` to `True` without +||| an explicit case-split or pattern match. Same family as the +||| SafeBuffer / SafeCSV record-projection gap. Discharge by +||| inlining `validResult` at the call site or by a reflective +||| record-projection tactic. public export -validResultIsValid : validResult.isValid = True - -||| Adding an Error-severity issue makes the result invalid -errorMakesInvalid : (issue : ValidationIssue) -> - issue.severity = Error -> - (addIssue issue validResult).isValid = False - -||| Adding a Warning-severity issue keeps the result valid -warningKeepsValid : (issue : ValidationIssue) -> - issue.severity = Warning -> - (addIssue issue validResult).isValid = True - -||| Combining valid results is valid +0 validResultIsValid : validResult.isValid = True + +||| OWED: adding an Error-severity issue makes the result invalid. +||| `addIssue` (Validation.idr L71-74) computes the new validity as +||| `result.isValid && issue.severity /= Error`; given +||| `issue.severity = Error` we have `Error /= Error = False`, so the +||| conjunction collapses to `False` for any starting `result`. Held +||| back by Idris2 0.8.0's user-defined `Eq ValidationSeverity` +||| instance (Validation.idr L28-32): equality on the three-arm +||| `data ValidationSeverity = Error | Warning | Info` does not +||| reduce under `(/=)` by Refl alone because `(/=)` is implemented +||| as `not . (==)` and `not (Error == Error)` requires unfolding +||| both the user-written `Eq` instance and `not`. Same family as +||| boj-server SafetyLemmas' enum-equality reflection gap. Discharge +||| with a `Bool`-vs-`Prop` reflective lemma `(==) Error Error = True` +||| plus `Not (True = False)` reasoning. +0 errorMakesInvalid : (issue : ValidationIssue) -> + issue.severity = Error -> + (addIssue issue validResult).isValid = False + +||| OWED: adding a Warning-severity issue keeps the result valid. +||| By the same `addIssue` definition (Validation.idr L71-74), with +||| `issue.severity = Warning` we get `Warning /= Error = True` and +||| starting `validResult.isValid = True`, so `True && True = True`. +||| Held back by the same `Eq ValidationSeverity` reduction gap as +||| `errorMakesInvalid` above, compounded by the +||| `validResultIsValid` record-projection gap. Discharge alongside +||| `errorMakesInvalid`. +0 warningKeepsValid : (issue : ValidationIssue) -> + issue.severity = Warning -> + (addIssue issue validResult).isValid = True + +||| OWED: combining two valid results yields a valid result. By the +||| definition `combineResults r1 r2 = MkValidationResult +||| (r1.isValid && r2.isValid) (r1.issues ++ r2.issues)` +||| (Validation.idr L78-80), with `r1.isValid = True` and +||| `r2.isValid = True` we get `True && True = True`. Held back by +||| Idris2 0.8.0 not reducing the record-field projection +||| `(MkValidationResult (r1.isValid && r2.isValid) _).isValid` to +||| `r1.isValid && r2.isValid` by Refl when `r1`, `r2` are +||| universally quantified (no constructor in normal form to fire +||| the projector). Discharge by case-split on `r1`, `r2` to expose +||| the `MkValidationResult` constructor, then `Refl` after the +||| `True && True = True` rewrite. public export -combineValidValid : (r1, r2 : ValidationResult) -> - r1.isValid = True -> r2.isValid = True -> - (combineResults r1 r2).isValid = True +0 combineValidValid : (r1, r2 : ValidationResult) -> + r1.isValid = True -> r2.isValid = True -> + (combineResults r1 r2).isValid = True -------------------------------------------------------------------------------- -- Email Structure Properties @@ -65,8 +138,19 @@ public export data ContainsAt : String -> Type where MkContainsAt : (s : String) -> (prf : '@' `elem` unpack s = True) -> ContainsAt s -||| If parseEmail succeeds, the input string contained '@' -parsedContainsAt : (s : String) -> isJust (parseEmail s) = True -> ContainsAt s +||| OWED: if `parseEmail s` succeeds (`isJust (parseEmail s) = True`), +||| the input string contains `'@'` (`'@' `elem` unpack s = True`). +||| Reduces by following `parseEmail s = Just _` back through +||| `parseEmailEither` (Parser.idr L171-182): the only success arm +||| requires `splitOnLast '@' s = Just (local, domain)`, which in +||| turn requires `'@'` to appear in `s`. Held back by Idris2 0.8.0's +||| String FFI opacity — `splitOnLast`, `unpack`, and `elem` all +||| pass through opaque primitives that do not type-level reduce. +||| Same blocker family as `parseNoAtFails`. Discharge once the +||| String FFI is reflectively modelled, or once `splitOnLast` is +||| factored through `List Char` with a structural lemma +||| `splitOnLastJust : splitOnLast c s = Just _ -> c `elem` unpack s = True`. +0 parsedContainsAt : (s : String) -> isJust (parseEmail s) = True -> ContainsAt s ||| Local part length bound public export @@ -87,11 +171,24 @@ data ValidTotalLength : String -> Type where -- Normalization Properties -------------------------------------------------------------------------------- -||| toLower on a domain is idempotent -normalizeIdempotent : (email : ParsedEmail) -> - toLower email.domain = toLower (toLower email.domain) - -||| Normalized emails with same local and domain are equal +||| OWED: `toLower` on a domain string is idempotent +||| (`toLower (toLower d) = toLower d`). True because case-folding to +||| lower case fixes the lowercase alphabet (and leaves non-letters +||| alone), so the second application is the identity on the image +||| of the first. Held back by Idris2 0.8.0's String-level `toLower` +||| being a wrapper over the opaque `prim__strToLower` FFI primitive +||| — it is not reducible at the type level. Same family as the +||| SafeHtml `escapePreservesNoLT` String-FFI gap. Discharge once a +||| `Data.String` reflective tactic is available, or via a +||| character-level lemma `Data.Char.toLowerIdempotent` lifted +||| through `pack . map toLower . unpack` (which still requires +||| reducing through `unpack` / `pack`). +0 normalizeIdempotent : (email : ParsedEmail) -> + toLower email.domain = toLower (toLower email.domain) + +||| Normalized emails with same local and domain are equal (trivial +||| restatement of the third hypothesis). Discharged by Refl on the +||| supplied equality witness. public export normalizedEquality : (e1, e2 : ParsedEmail) -> e1.localPart = e2.localPart -> @@ -116,44 +213,109 @@ isHeaderSafe c = c /= '\n' && c /= '\r' && c /= '\0' sanitizeForHeader : String -> String sanitizeForHeader str = pack (filter isHeaderSafe (unpack str)) -||| Filtering out header-unsafe chars leaves no newlines -sanitizeRemovesNewlinesLemma : (s : String) -> - all (\c => c /= '\n' && c /= '\r') - (filter (\c => c /= '\n' && c /= '\r' && c /= '\0') (unpack s)) - = True - -||| Sanitization removes newlines +||| OWED: filtering out the union predicate +||| `(c /= '\n' && c /= '\r' && c /= '\0')` from a `List Char` +||| leaves a list where every element satisfies the weaker predicate +||| `(c /= '\n' && c /= '\r')`. Standard `filter` post-condition +||| (`all p (filter q xs) = True` when `q x = True -> p x = True`, +||| with the implication discharged by `&&` projection). Held back +||| by Idris2 0.8.0 not auto-deriving the `filter`-postcondition +||| lemma — `Data.List` exposes no `filterAll : (forall x. q x = +||| True -> p x = True) -> all p (filter q xs) = True`, and the +||| direct proof requires structural induction on `xs` plus a +||| `&&`-projection lemma which is itself opaque under Idris2's +||| `Bool` reduction. Same family as SafeHtml's filter-correctness +||| OWED. Discharge with a hand-written `filterAll` lemma or with a +||| reflective `Bool` tactic. +0 sanitizeRemovesNewlinesLemma : (s : String) -> + all (\c => c /= '\n' && c /= '\r') + (filter (\c => c /= '\n' && c /= '\r' && c /= '\0') (unpack s)) + = True + +||| OWED: `sanitizeForHeader s` always produces a string with no +||| newlines (CR/LF) — the safety property the function exists for. +||| Decomposes as `unpack (pack (filter isHeaderSafe (unpack s))) = +||| filter isHeaderSafe (unpack s)` (the `unpack . pack = id` round +||| trip, opaque under String FFI) composed with the +||| `sanitizeRemovesNewlinesLemma` above. Held back by the +||| combination of two Idris2 0.8.0 blockers: (1) the `unpack . pack` +||| round-trip is not a Refl (the String FFI's `prim__strCons` / +||| `prim__strSubstr` cycle is not reducible at the type level); +||| (2) the upstream `sanitizeRemovesNewlinesLemma` is itself OWED. +||| Discharge once both are discharged. public export -sanitizeRemovesNewlines : (s : String) -> - NoNewlines (sanitizeForHeader s) +0 sanitizeRemovesNewlines : (s : String) -> + NoNewlines (sanitizeForHeader s) -------------------------------------------------------------------------------- -- List Operations Properties -------------------------------------------------------------------------------- -||| filterValid retains only emails that pass full validation -filterValidCorrect : (emails : List String) -> - all (\e => (validateEmailFull e).isValid) (filterValid emails) = True +||| OWED: `filterValid` retains only emails that pass full +||| validation (`all (.isValid . validateEmailFull) (filterValid +||| emails) = True`). By definition `filterValid = filter (\s => +||| (validateEmailFull s).isValid)` (Validation.idr L286), so this +||| is the `filter` post-condition `all p (filter p xs) = True` — +||| the standard `filterAllP` lemma. Held back by Idris2 0.8.0's +||| `Data.List` not exposing `filterAllP` as a Refl-discharable +||| identity (`filter p` decomposes by induction on the list, and +||| the cons-case requires both `p x = True` and the IH composed +||| with `(::)`). Discharge with a hand-written +||| `filterAllSelf : (xs : List a) -> all p (filter p xs) = True` +||| lemma in `Data.List`, or via the reflective `Bool` tactic. +0 filterValidCorrect : (emails : List String) -> + all (\e => (validateEmailFull e).isValid) (filterValid emails) = True uniqueEmails : List ParsedEmail -> List ParsedEmail uniqueEmails = nubBy (\e1, e2 => toLower (e1.localPart ++ "@" ++ e1.domain) == toLower (e2.localPart ++ "@" ++ e2.domain)) -||| nubBy-based deduplication never increases list length -uniqueNoDuplicates : (emails : List ParsedEmail) -> - LTE (length (uniqueEmails emails)) (length emails) +||| OWED: `nubBy`-based deduplication never increases list length +||| (`length (nubBy p xs) <= length xs`). Standard `Data.List` +||| post-condition — `nubBy` only removes elements, never adds them. +||| Held back by Idris2 0.8.0's `Data.List` not exposing the lemma +||| `nubByLengthLTE : (xs : List a) -> LTE (length (nubBy p xs)) +||| (length xs)` as a Refl-discharable identity. The direct proof +||| requires structural induction on `xs` plus the `LTE`-transport +||| lemma `LTE n (S n)` for the skip-arm. Same family as the +||| boj-server `Data.List` length-monotonicity OWED set. Discharge +||| by adding the missing lemma to `Data.List`, or by extending +||| `Data.List.Lemmas` (contrib) with it. +0 uniqueNoDuplicates : (emails : List ParsedEmail) -> + LTE (length (uniqueEmails emails)) (length emails) -------------------------------------------------------------------------------- -- Domain Validation Properties -------------------------------------------------------------------------------- -||| Free email domain check is exhaustive +||| OWED: `isFreeEmail` is total and exhaustive (it returns either +||| `True` or `False` for every domain — i.e., it is a decidable +||| predicate). By definition `isFreeEmail domain = toLower domain +||| `elem` freeEmailDomains` (Validation.idr L259), whose return +||| type is `Bool`, so the claim is the `Bool`-LEM +||| `(b : Bool) -> Either (b = True) (b = False)`. Held back by +||| Idris2 0.8.0 not auto-deriving `Bool`-LEM as a Refl (the +||| standard discharge is `case b of True => Left Refl; False => +||| Right Refl`, but this is a case-split not a Refl). Same family +||| as SafeTOML's `isScalarCorrect` Bool-LEM gap. Discharge with a +||| one-line case-split on `isFreeEmail domain`. public export -freeEmailExhaustive : (domain : String) -> - Either (isFreeEmail domain = True) (isFreeEmail domain = False) - -||| checkCommonTypos detects "gmial.com" as a typo of "gmail.com" -typoCheckFindsKnown : checkCommonTypos "gmial.com" = addIssue +0 freeEmailExhaustive : (domain : String) -> + Either (isFreeEmail domain = True) (isFreeEmail domain = False) + +||| OWED: `checkCommonTypos "gmial.com"` returns the +||| canonical W010 warning suggesting `"gmail.com"`. By the +||| `checkCommonTypos` definition (Validation.idr L150-166) the +||| first entry of the `checks` list is `("gmial.com", "gmail.com")` +||| and `find` returns it because `toLower "gmial.com" == "gmial.com"`, +||| so the result is `addIssue (W010 "...gmail.com?") validResult`. +||| Held back by Idris2 0.8.0's String FFI opacity on `toLower` and +||| String-equality `(==)` — neither reduces a literal-vs-literal +||| comparison to `True` by Refl at the type level. Same family as +||| `normalizeIdempotent` and `parseNoAtFails`. Discharge once the +||| String FFI is reflectively modelled, or by refactoring +||| `checkCommonTypos` to operate on `List Char`. +0 typoCheckFindsKnown : checkCommonTypos "gmial.com" = addIssue (MkValidationIssue Warning "W010" "Possible typo - did you mean gmail.com?") validResult @@ -162,31 +324,79 @@ typoCheckFindsKnown : checkCommonTypos "gmial.com" = addIssue -- RFC Compliance Properties -------------------------------------------------------------------------------- -||| A valid local part does not start with a dot -validLocalNoStartDot : (local : String) -> - (validateLocalPart local).isValid = True -> - isPrefixOf "." local = False - -||| A valid local part does not end with a dot -validLocalNoEndDot : (local : String) -> - (validateLocalPart local).isValid = True -> - isSuffixOf "." local = False - -||| A valid domain has at least one label when split on '.' -validDomainHasLabel : (domain : String) -> - (validateDomain domain).isValid = True -> - LTE 1 (length (forget (split (== '.') domain))) +||| OWED: a local part that passes `validateLocalPart` does not +||| start with a dot (`isPrefixOf "." local = False`). Reduces by +||| inspecting `validateLocalPart` (Validation.idr L88-105): the +||| `result''` arm adds an Error issue E003 when +||| `isPrefixOf "." local = True`, which sets `.isValid = False`; +||| so `.isValid = True` requires `isPrefixOf "." local = False`. +||| Held back by Idris2 0.8.0's String FFI opacity on `isPrefixOf` +||| (it threads through `prim__strHead` / `prim__strSubstr`), and +||| by the `addIssue` Bool-reduction gap shared with +||| `errorMakesInvalid`. Same family as `parseNoAtFails`. Discharge +||| once the String FFI is reflectively modelled. +0 validLocalNoStartDot : (local : String) -> + (validateLocalPart local).isValid = True -> + isPrefixOf "." local = False + +||| OWED: a local part that passes `validateLocalPart` does not end +||| with a dot (`isSuffixOf "." local = False`). Identical shape to +||| `validLocalNoStartDot` — `validateLocalPart` adds Error E004 +||| when `isSuffixOf "." local = True`. Held back by the same +||| String-FFI / Bool-reduction blockers; discharged in the same +||| stroke. +0 validLocalNoEndDot : (local : String) -> + (validateLocalPart local).isValid = True -> + isSuffixOf "." local = False + +||| OWED: a domain that passes `validateDomain` has at least one +||| label when split on `'.'` (`LTE 1 (length (forget (split (== '.') +||| domain)))`). `split (== '.')` returns a `List1`, which by +||| definition has length `>= 1` (`forget : List1 a -> List a` +||| preserves the non-emptiness). Held back by Idris2 0.8.0's +||| `Data.List1` not exposing the length-lower-bound lemma +||| `LTE 1 (length (forget xs))` as a Refl. Discharge with a +||| one-line case-split on the `List1` constructor (`x ::: xs` +||| gives length `S (length xs) >= S Z`). +0 validDomainHasLabel : (domain : String) -> + (validateDomain domain).isValid = True -> + LTE 1 (length (forget (split (== '.') domain))) -------------------------------------------------------------------------------- -- Comprehensive Validation Properties -------------------------------------------------------------------------------- -||| If basic validation fails, comprehensive validation also fails -comprehensiveCatchesRFC : (s : String) -> - (validateEmailFull s).isValid = False -> - (validateComprehensive s).isValid = False - -||| If basic validation passes, comprehensive validation has no errors -validPassesComprehensive : (s : String) -> - (validateEmailFull s).isValid = True -> - hasErrors (validateComprehensive s) = False +||| OWED: if `validateEmailFull s` fails, `validateComprehensive s` +||| also fails. Both functions parse via `parseEmail s` first +||| (Validation.idr L132, L210); the `Nothing` arm returns the same +||| E000 invalid result in both, and the `Just email` arm in +||| `validateComprehensive` combines a superset of the issues +||| `validateEmailFull` combines (`validateLocalPart`, +||| `validateDomain` plus the typo / role / plus / numeric checks), +||| and `combineResults` is monotone in invalidity. Held back by the +||| `combineResults` record-projection gap shared with +||| `combineValidValid` plus the `foldl combineResults` invariant +||| (which `Data.List` does not expose as a Refl in Idris2 0.8.0). +||| Discharge alongside `combineValidValid`. +0 comprehensiveCatchesRFC : (s : String) -> + (validateEmailFull s).isValid = False -> + (validateComprehensive s).isValid = False + +||| OWED: if `validateEmailFull s` passes, `validateComprehensive s` +||| has no errors (`hasErrors (validateComprehensive s) = False`). +||| Reduces by inspecting which `ValidationIssue`s the four extra +||| checks (`checkCommonTypos`, `checkRoleAddress`, +||| `checkPlusAddressing`, `checkNumericLocal`) can add: by code +||| inspection of Validation.idr L150-201, every issue these add +||| has severity `Warning` (W010) or `Info` (I001/I002/I003), never +||| `Error`. So if the `validateEmailFull` path is error-free, +||| `validateComprehensive` is also error-free. Held back by Idris2 +||| 0.8.0 not reducing the `foldl combineResults` accumulator +||| across the seven-step result list, plus the `hasErrors` +||| `any . (.severity = Error)` Bool-reduction gap shared with +||| `errorMakesInvalid`. Discharge alongside `errorMakesInvalid` + +||| `combineValidValid`, with one extra step-lemma per extra check +||| (each: "this check only emits non-Error issues"). +0 validPassesComprehensive : (s : String) -> + (validateEmailFull s).isValid = True -> + hasErrors (validateComprehensive s) = False