Std.Http server: answer a syntactically valid but unrecognized method with 501, not 400? #16335

Description

RFC 9110 §9.1: "An origin server that receives a request method that is unrecognized or not
implemented SHOULD respond with the 501 (Not Implemented) status code." RFC 9112 §3: "A server
that receives a method longer than any that it implements SHOULD respond with a 501". The H1
machine fails parseMethod with "unrecognized method", which becomes badMessage → 400:

PATCH / HTTP/1.1  →  reaches the handler
FOO / HTTP/1.1    →  "HTTP/1.1 400 Bad Request⏎Connection: close⏎Content-Length: 0⏎⏎"

tests/async/elab/async_http_h1_rfc_compliance.lean currently asserts §3: unrecognized method → badMessage, so this may be deliberate — if so, could the reason be documented? Otherwise: 501
for a well-formed token method that is not recognized, 400 only for a non-token.

Versions

v4.35.0, nightly-2026-11-06, master 2026-11-07.

Found while auditing RFC 9110/9112 conformance of Std.Http (Lean v4.35.0, re-checked against master 2026-11-07). Standalone repro available on request.

This report was prepared and written with AI assistance (Claude).