From 7046164ce83ed9568e5830b8fe8ffaeeb0533718 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 30 May 2026 14:46:52 +0100
Subject: [PATCH] proof(SafeCORS): qualify defaultPolicy in 4 Refl signatures
 (closes #92 partial)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Idris2 0.8.0 implicitly binds bare lowercase `defaultPolicy` in type
signatures as a fresh variable, shadowing `Proven.SafeCORS.defaultPolicy`
(elaborator emits the shadowing warning). The `Refl` on the RHS then
cannot reduce because the type-level `defaultPolicy` is the opaque
implicit, not the concrete `MkCORSPolicy AllowNone [] [] [] Nothing False`.

Qualifying the name as `Proven.SafeCORS.defaultPolicy` resolves the
shadowing — all 4 default-policy proofs (`defaultPolicyDeniesAll`,
`defaultPolicyIsSafe`, `defaultPolicyNoErrors`, `defaultPolicyNoHeaders`)
now type-check, no `believe_me` / `assert_total` / `postulate`.

CI-coverage gap fixed: adds `Proven.SafeCORS.Proofs` to `proven.ipkg`
modules list so this file is type-checked by the `Idris 2 CI`
workflow on every push.

Acceptance criteria from #92:
- [x] 4 defaultPolicy* Refl proofs type-check
- [x] Proven.SafeCORS.Proofs added to proven.ipkg
- [x] Sibling audit: SafeArgs.Proofs ✓ clean; SafeAPIKey.Proofs has
      2 errors of a **different class** (with-block + String FFI
      reduction, not the shadowing pattern) — captured in follow-up
- [ ] CI green — pending push

The SafeAPIKey.Proofs failures (`emptyKeyRejected`, `fullMaskFormat`)
are not the qualified-projection bug; they need a separate fix and a
separate issue. Adding only SafeCORS.Proofs to the ipkg until those
are repaired, per "don't regress CI" discipline.

Refs hyperpolymath/proven#92
Refs hyperpolymath/standards#124

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 proven.ipkg                    |  1 +
 src/Proven/SafeCORS/Proofs.idr | 19 ++++++++++++++-----
 2 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/proven.ipkg b/proven.ipkg
index 00a3ffcb..40402c1a 100644
--- a/proven.ipkg
+++ b/proven.ipkg
@@ -236,6 +236,7 @@ modules = Proven
         , Proven.SafeHTTP
         , Proven.SafePromptInjection
         , Proven.SafeCORS
+        , Proven.SafeCORS.Proofs
         , Proven.SafeAPIKey
         , Proven.SafeWebSocket
         -- Security hardening modules (v1.2.0)
diff --git a/src/Proven/SafeCORS/Proofs.idr b/src/Proven/SafeCORS/Proofs.idr
index 30d2fb1a..1cd96997 100644
--- a/src/Proven/SafeCORS/Proofs.idr
+++ b/src/Proven/SafeCORS/Proofs.idr
@@ -17,25 +17,34 @@ import Data.List
 -- Default Policy Properties
 --------------------------------------------------------------------------------
 
+-- NOTE: bare `defaultPolicy` in these type signatures is implicitly
+-- bound as a fresh lowercase variable by Idris2 0.8.0, shadowing
+-- `Proven.SafeCORS.defaultPolicy`. The `Refl` then cannot reduce
+-- because the type-level `defaultPolicy` is opaque. Qualifying with
+-- `Proven.SafeCORS.defaultPolicy` resolves the shadowing. See
+-- hyperpolymath/proven#92.
+
 ||| The default policy denies all origins.
 public export
-defaultPolicyDeniesAll : (origin : Origin) -> isOriginAllowed defaultPolicy origin = False
+defaultPolicyDeniesAll : (origin : Origin) ->
+                         isOriginAllowed Proven.SafeCORS.defaultPolicy origin = False
 defaultPolicyDeniesAll _ = Refl
 
 ||| The default policy is not an unsafe configuration.
 public export
-defaultPolicyIsSafe : isUnsafeConfiguration defaultPolicy = False
+defaultPolicyIsSafe : isUnsafeConfiguration Proven.SafeCORS.defaultPolicy = False
 defaultPolicyIsSafe = Refl
 
 ||| The default policy has no validation errors.
 public export
-defaultPolicyNoErrors : validatePolicy defaultPolicy = []
+defaultPolicyNoErrors : validatePolicy Proven.SafeCORS.defaultPolicy = []
 defaultPolicyNoErrors = Refl
 
 ||| The default policy does not generate headers (denies all).
 public export
-defaultPolicyNoHeaders : (origin : Origin) -> generateHeaders defaultPolicy origin = Nothing
-defaultPolicyNoHeaders origin = Refl
+defaultPolicyNoHeaders : (origin : Origin) ->
+                         generateHeaders Proven.SafeCORS.defaultPolicy origin = Nothing
+defaultPolicyNoHeaders _ = Refl
 
 --------------------------------------------------------------------------------
 -- Wildcard+Credentials Safety