From eeb1a96e34024f3501158a78595ba36d37c01ae4 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 14:11:03 +0100 Subject: [PATCH] proof(SafeCORS): discharge misconfiguredNoHeaders OWED to real proof MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the bodyless `0 misconfiguredNoHeaders` OWED declaration with a genuine proof, using a small bridge lemma `validatePolicyNonNil`. The earlier OWED comment claimed Idris2 0.8.0 could not reduce the `validatePolicy` / `generateHeaders` chain past the leading `++` conjunct; in fact it can — `rewrite`ing by the `isUnsafeConfiguration policy = True` hypothesis collapses the inner `if` to its `True` arm, after which `[WildcardWithCredentials] ++ tail` unfolds to `WildcardWithCredentials :: tail` and `isNil (_ :: _)` reduces by `Refl`. The opaque `emptyMethods` right operand never needs inspection because `isNil` matches the spine constructor of the *whole* list, not its content. Zero `believe_me`, zero `postulate`, zero `assert_total`. The two new top-level functions are both `public export` so downstream proof modules can reuse `validatePolicyNonNil` directly. Scope discipline: this PR does NOT touch the four pre-existing broken `Refl` proofs in the same file (`defaultPolicyDeniesAll`, `defaultPolicyIsSafe`, `defaultPolicyNoErrors`, `defaultPolicyNoHeaders`). Those fail for a separate reason — Idris2 0.8.0 does not reduce record-field projection on a literal `MkCORSPolicy ...` constructor unless the value name is *qualified* (`Proven.SafeCORS.defaultPolicy.allowOrigins` reduces by Refl; `defaultPolicy.allowOrigins` does not). That is independent tech debt and is filed as a separate follow-up. Local oracle: - `idris2 --build cors-check.ipkg` reports exactly the 4 pre-existing Refl errors and zero new errors at `misconfiguredNoHeaders` or `validatePolicyNonNil`. - `Proven.SafeCORS.Proofs` is not in `proven.ipkg`, so this change does not move CI status; the discharge stands on its own type signature. Refs hyperpolymath/standards#124 Refs hyperpolymath/standards#158 Co-Authored-By: Claude Opus 4.7 (1M context) --- src/Proven/SafeCORS/Proofs.idr | 61 +++++++++++++++++++++------------- 1 file changed, 37 insertions(+), 24 deletions(-) diff --git a/src/Proven/SafeCORS/Proofs.idr b/src/Proven/SafeCORS/Proofs.idr index a9c92eb3..30d2fb1a 100644 --- a/src/Proven/SafeCORS/Proofs.idr +++ b/src/Proven/SafeCORS/Proofs.idr @@ -78,30 +78,43 @@ noneAlwaysSafe policy prf = rewrite prf in Refl -- Header Generation Safety -------------------------------------------------------------------------------- -||| OWED: When `isUnsafeConfiguration policy = True`, `generateHeaders -||| policy origin` returns `Nothing`. Held back by Idris2 0.8.0 not -||| reducing the chained `validatePolicy` / `generateHeaders` guard -||| under a single `Refl`: `generateHeaders` branches on `not (isNil -||| (validatePolicy policy))`, and `validatePolicy` itself is `if -||| isUnsafeConfiguration policy then [WildcardWithCredentials] else -||| [] ++ (if isNil allowMethods && not (isNil allowHeaders) then -||| [EmptyMethodList] else [])`. Rewriting by the hypothesis pushes -||| the inner `if` to the `True` arm, but the surrounding `++` / -||| `isNil` / `not` chain does not normalise to `True` definitionally -||| because the right operand of `++` is an opaque conditional over -||| `policy.allowMethods` / `policy.allowHeaders`. Discharge once -||| `validatePolicy` is refactored to expose a top-level disjunctive -||| case on `isUnsafeConfiguration` (or once a `cong`-style proof is -||| written by-hand routing through `appendNilLeftNeutral` / `isNil -||| (x :: xs) = False`). Same blocker family as the FFI-bound -||| `validateLuhn` / `validateISBN*` OWED items in -||| `Proven.SafeChecksum.Proofs` — opaque-spine list reduction under -||| Idris2 0.8.0. -export -0 misconfiguredNoHeaders : (policy : CORSPolicy) -> - (origin : Origin) -> - isUnsafeConfiguration policy = True -> - generateHeaders policy origin = Nothing +||| Bridge lemma (discharged 2026-05-30): if a policy is unsafely +||| configured, its `validatePolicy` list is non-empty. +||| +||| The earlier OWED comment claimed Idris2 0.8.0 could not reduce +||| `++` past the leading `if isUnsafeConfiguration policy then +||| [WildcardWithCredentials] else []`. In fact it CAN — `rewrite`ing +||| by the hypothesis collapses the `if` to its `True` arm, after +||| which `[WildcardWithCredentials] ++ tail` reduces to +||| `WildcardWithCredentials :: tail` and `isNil (_ :: _)` reduces to +||| `False` by `Refl`. The right operand of `++` (the opaque +||| `emptyMethods` conditional) never needs to be inspected because +||| `isNil` matches on the spine constructor of the *whole* list, not +||| on its content. +public export +validatePolicyNonNil : (policy : CORSPolicy) -> + isUnsafeConfiguration policy = True -> + isNil (validatePolicy policy) = False +validatePolicyNonNil policy prf = rewrite prf in Refl + +||| DISCHARGED (Refs hyperpolymath/standards#158): when +||| `isUnsafeConfiguration policy = True`, `generateHeaders policy +||| origin` returns `Nothing`. +||| +||| Proof: `generateHeaders` short-circuits on +||| `not (isNil (validatePolicy policy))`. Rewriting by +||| `validatePolicyNonNil` reduces that guard to `not False = True`, +||| which fires the `Nothing` arm of the outer `if`. No `believe_me`, +||| no `postulate`, no `assert_total`. +public export +misconfiguredNoHeaders : (policy : CORSPolicy) -> + (origin : Origin) -> + isUnsafeConfiguration policy = True -> + generateHeaders policy origin = Nothing +misconfiguredNoHeaders policy origin prf = + let nonNil : (isNil (validatePolicy policy) = False) + nonNil = validatePolicyNonNil policy prf + in rewrite nonNil in Refl -------------------------------------------------------------------------------- -- Origin Matching Properties