getHeaderNames should return header name once also when request has it in different case

[findepi]

Jetty version(s)
12.0.9

Jetty Environment
ee10

Java version/vendor (use: java -version)
Java 22

OS type/version
MacOS

Description
request.getHeaderNames is typically used to iterate over header names in the request and then request.getHeaders is used to retrieve values:

// example code supposed tor resemble typical use of getHeaderNames()
Enumeration<String> names = servletRequest.getHeaderNames();
while (names.hasMoreElements()) {
    String name = names.nextElement();
    doSomething(name, servletRequest.getHeaders(name))
}

When request contains both Foo-Bar and foo-bar headers, getHeaderNames returns both String values, so foo-bar header values are processed twice.

How to reproduce?

curl -H 'Foo-Bar: one' -H 'foo-bar: two'  http://localhost:8080/endpoint

[findepi]

This code is potentially wrong because of this: https://github.com/jakartaee/servlet/blob/26a58cb1a6f148b56e274bf0f8030176d20cfeb6/api/src/main/java/jakarta/servlet/http/HttpServlet.java#L565
(it's look like it doesn't handle duplicated headers well, even if they are in same case)

[gregw]

I can confirm a reproduction... investigating....

[gregw]

Reopened to add some comments to HttpFields regarding how it is implemented as a list and the reasons behind that (see #3682)