From 33baed815c14c24776cd1a19d1e753ce2ac2b698 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 15:14:16 +0100 Subject: [PATCH] proof(SafeAPIKey): fix emptyKeyRejected + reshape fullMaskFormat (closes #95) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two distinct FFI-reduction issues in `src/Proven/SafeAPIKey/Proofs.idr` that fail under Idris2 0.8.0 (and were never caught by CI because the `Proofs` module was not in `proven.ipkg`): **emptyKeyRejected** — `mkAPIKey "" = Nothing`. The pre-fix definition funneled the empty string through `with (choose (length s >= 16))`, which can't reduce at type-check time because `prim__strLength` / `>=` are FFI primitives. Fix: add an explicit `mkAPIKey "" = Nothing` fast-path equation BEFORE the `with`-block. Identical runtime behaviour (empty rejected either way), and the proof now discharges by `Refl` directly via the first equation. **fullMaskFormat / Structure** — was `(key : APIKey) -> isPrefixOf "[REDACTED:" (fullMask key) = True`. The pre-fix `Refl` failed because `isPrefixOf` walks `unpack`/`++` through the String FFI on a universally-quantified `key`. Replaced with `fullMaskStructure : ... fullMask key = "[REDACTED:" ++ show (length key.raw) ++ " chars]"` — structural equality, definitionally true (`Refl`), and delivers the same safety guarantee: the output is a fixed-prefix template containing only the redacted length count, no key material. Any consumer that needs the original `isPrefixOf` form can derive it locally from `fullMaskStructure` + a small list-prefix lemma without running into the FFI-reduction wall. CI coverage closed: `Proven.SafeAPIKey.Proofs` added to `proven.ipkg` modules list. This was the gating condition from #92's sibling-audit acceptance criteria (was excluded by #94 pending the present fix). Verified: `idris2 --check src/Proven/SafeAPIKey/Proofs.idr` clean under Idris2 0.8.0 (zero `believe_me`, zero `assert_total`, zero `postulate`). Closes #95 Refs hyperpolymath/proven#92 (sibling-audit surfaced this) Refs hyperpolymath/proven#94 (which excluded SafeAPIKey.Proofs from ipkg pending this fix) Co-Authored-By: Claude Opus 4.7 (1M context) --- proven.ipkg | 1 + src/Proven/SafeAPIKey.idr | 10 +++++++++- src/Proven/SafeAPIKey/Proofs.idr | 17 ++++++++++++++--- 3 files changed, 24 insertions(+), 4 deletions(-) diff --git a/proven.ipkg b/proven.ipkg index 40402c1a..212c1feb 100644 --- a/proven.ipkg +++ b/proven.ipkg @@ -238,6 +238,7 @@ modules = Proven , Proven.SafeCORS , Proven.SafeCORS.Proofs , Proven.SafeAPIKey + , Proven.SafeAPIKey.Proofs , Proven.SafeWebSocket -- Security hardening modules (v1.2.0) , Proven.SafeCSRF diff --git a/src/Proven/SafeAPIKey.idr b/src/Proven/SafeAPIKey.idr index a171cd8d..b3ca8f1f 100644 --- a/src/Proven/SafeAPIKey.idr +++ b/src/Proven/SafeAPIKey.idr @@ -84,9 +84,17 @@ record APIKey where ||| Postulate: length check for key construction keyLengthOk : (s : String) -> {auto 0 _ : So (length s >= MinKeyLength)} -> So (length s >= MinKeyLength) -||| Attempt to create an APIKey from a raw string +||| Attempt to create an APIKey from a raw string. +||| +||| The empty-string fast-path is explicit so the proof +||| `emptyKeyRejected` (in `Proofs.idr`) discharges by `Refl` without +||| relying on the `prim__strLength`/`>=` FFI primitives to reduce at +||| type-check time. Behaviour is identical to a single `with`-clause +||| definition — empty strings fail the length check either way. +||| See hyperpolymath/proven#95. public export mkAPIKey : String -> Maybe APIKey +mkAPIKey "" = Nothing mkAPIKey s with (choose (length s >= MinKeyLength)) mkAPIKey s | Left prf = Just (MkAPIKey s (detectFormat s) prf) mkAPIKey s | Right _ = Nothing diff --git a/src/Proven/SafeAPIKey/Proofs.idr b/src/Proven/SafeAPIKey/Proofs.idr index 90779049..ed471a45 100644 --- a/src/Proven/SafeAPIKey/Proofs.idr +++ b/src/Proven/SafeAPIKey/Proofs.idr @@ -71,10 +71,21 @@ emptyFormatUnknown = Refl -------------------------------------------------------------------------------- ||| fullMask never exposes any key characters. -||| The output is "[REDACTED:N chars]" which contains no key material. +||| +||| The original formulation asked for `isPrefixOf "[REDACTED:"` +||| (fullMask key) = True`, but Idris2 0.8.0 cannot reduce the +||| `isPrefixOf` call through the `unpack`/`++` String-FFI chain when +||| the right operand is universally quantified. Splitting the +||| guarantee in two delivers the same safety property by structural +||| equality (which `Refl` discharges) plus a derived prefix-lemma +||| that any consumer can apply locally — see #95 for the bridge +||| approach. +||| +||| The output is "[REDACTED:N chars]" — opaque length, no key bytes. public export -fullMaskFormat : (key : APIKey) -> isPrefixOf "[REDACTED:" (fullMask key) = True -fullMaskFormat key = Refl +fullMaskStructure : (key : APIKey) -> + fullMask key = "[REDACTED:" ++ show (length key.raw) ++ " chars]" +fullMaskStructure _ = Refl -------------------------------------------------------------------------------- -- Format Matching Properties