`Std.Http`: `URI.Query` lookups compare percent-encoded bytes, which are not canonical

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Std.Http.URI.Query's String-keyed operations (get, getD, find?, findAll, contains, erase, set) percent-encode the caller's key and compare the resulting bytes against the stored name's bytes. Percent-encoding is not canonical, so this is not a well-defined equality on names: a byte that may appear literally may equally appear as a triplet, and both spellings are valid encodings of the same parameter.

Context

Found in a middleware library built on Std.Http.Server, on an OAuth consent form whose checkboxes were named after the scopes they approve:

<input type="checkbox" name="approve-todos:read" value="on" checked>

The browser posts approve-todos%3Aread=on&decision=allow, Params.get "approve-todos:read" is none.

Two things make it expensive to find. The failure is a silent false negative, so nothing surfaces. And it does not reproduce with curl: curl -d 'a:b=on' sends the bytes it is given, colon intact, and the lookup matches. Only a real browser encodes the name, so handler tests and manual curl checks pass and the failure appears only in a browser.

No prior Zulip discussion, and a search of the issue tracker turns up nothing mentioning URI.Query at all.

Steps to Reproduce

1. Build a Query holding the parameter as a browser puts it on the wire: the name a:b percent-encoded to a%3Ab.
2. Confirm the stored name decodes to the name you expect.
3. Look that name up with Query.get.

import Std.Http
open Std.Http

/-- The query a browser produces for a field named `a:b`. -/
def q : URI.Query :=
  match URI.EncodedQueryParam.fromString? "a%3Ab", URI.EncodedQueryParam.fromString? "on" with
  | some k, some v => URI.Query.empty.insertEncoded k (some v)
  | _, _ => URI.Query.empty

#eval toString q                             -- "?a%3Ab=on"
#eval q.toArray.map (fun p => p.fst.decode)  -- #[some "a:b"]  the stored name IS "a:b"
#eval q.get "a:b"                            -- some "on" expected; actual: none

The same happens through Std.Http's own URI parser, on a URL a browser would produce. URI.query changed type between the two versions:

-- v4.33.0, where `URI.query : URI.Query`
#eval (URI.parse? "https://example.com/consent?a%3Ab=on").bind (fun u => u.query.get "a:b")

-- nightly, where `URI.query : Option URI.Query`
#eval (URI.parse? "https://example.com/consent?a%3Ab=on").bind (fun u => u.query.bind (·.get "a:b"))

-- both print: none

Expected behavior: q.get "a:b" is some "on". A parameter whose name decodes to a:b is found by the key "a:b", whichever legal spelling of that name arrived on the wire.

Actual behavior: q.get "a:b" is none. The parameter is unreachable by its own name: "a:b" misses because the stored bytes are a%3Ab, and "a%3Ab" misses because the key is itself encoded to a%253Ab.

Versions

4.33.0
4.35.0-nightly-2026-08-26

Ubuntu 26.04 LTS, aarch64. The repro above gives identical results on both: none, false, 0, nothing erased, and the duplicate name emitted by set.

Additional Information

The root cause is in Std/Http/Data/URI/Basic.lean:

def findEncoded? (query : Query) (key : EncodedQueryParam) : Option (Option EncodedQueryParam) :=
  let matchingKey := Array.find? (fun x => x.fst.toByteArray = key.toByteArray) query
  matchingKey.map (fun x => x.snd)

def find? (query : Query) (key : String) : Option (Option EncodedQueryParam) :=
  query.findEncoded? (EncodedQueryParam.encode key)

find?'s doc comment says: "The key is percent-encoded before matching. This avoids aliasing between raw and pre-encoded spellings." The intent is right, but the effect is the opposite of the intent; Encoding the key does not stop two different names colliding, it stops one name matching itself.

contains and findAll behave the same way, since both route through the same byte comparison. Continuing with the q above:

#eval q.contains "a:b"        -- true expected; actual: false
#eval (q.findAll "a:b").size  -- 1 expected; actual: 0

set and erase can corrupt the query. erase uses the same comparison and set is erase then insert, so setting a parameter already present under a different spelling does not replace it, but appends instead:

#eval toString (q.erase "a:b")        -- "?a%3Ab=on"          -- nothing erased
#eval toString (q.set "a:b" "off")    -- "?a%3Ab=on&a:b=off"  -- duplicate name on the wire

Suggested fix. Have the String-keyed operations compare decoded names. A parameter's name is what it decodes to, which is what the wire format means and what a caller passing a plain String is asking for:

def find? (query : Query) (key : String) : Option (Option EncodedQueryParam) :=
  (Array.find? (fun x => x.fst.decode == some key) query).map (fun x => x.snd)

with findAll, contains and erase following the same shape.

Caveats:

• Decoding on every comparison costs more than a byte compare. We could alternatively, compare bytes first and decode only on a miss; the fast path is unchanged for the common case where both sides are spelled alike.
• EncodedQueryString.decode maps + to space unconditionally, so a decoded comparison makes a b, a+b and a%20b one name. That is correct for application/x-www-form-urlencoded and wrong for an RFC 3986 query string, where + is an ordinary sub-delim. This is a pre-existing property of EncodedQueryParam rather than something the fix introduces, but the fix does make it observable through get.

Impact

There is no call-site workaround, because the defect is in what String-keyed lookup means. A client that wants a form field found by the name its own markup gave it has to stop using the String-keyed API and reimplement the lookup over Query.toArray:

https://github.com/paulbutcher/lean-middleware/commit/212c6598cf7bc4dcae1e6308aa3cb34e74a71aba

Any other Std.Http consumer that accepts browser-posted forms will face the same issue.

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start in Std/Http/Data/URI/Basic.lean at Query.findEncoded? and the String-keyed find?, then trace findAll, contains, erase, and set. Run the supplied Lean reproduction for an encoded name such as a%3Ab; done means String-keyed operations find, replace, erase, and report the decoded parameter consistently.