Skip to content

proof(SafeAPIKey): fix emptyKeyRejected + reshape fullMaskFormat (closes #95) #96

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
May 30, 2026
Merged

proof(SafeAPIKey): fix emptyKeyRejected + reshape fullMaskFormat (closes #95) #96

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions proven.ipkg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 9 additions & 1 deletion src/Proven/SafeAPIKey.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
17 changes: 14 additions & 3 deletions src/Proven/SafeAPIKey/Proofs.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading