sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

feat: client

Browse Source
This commit is contained in:
Sofia Rodrigues
2026-03-16 00:01:33 -03:00
parent d4884cde14
commit 65da1ee047
14 changed files with 1595 additions and 246 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
src/Std/Internal/Http/Client.lean
View File

@@ -63,19 +63,23 @@ def proxy (b : Client.Builder) (host : String) (port : UInt16) : Client.Builder
/--
Routes all connections through a proxy specified as a URL string.
Returns `none` if the URL is invalid or has no authority component.
Only HTTP proxies are supported. The scheme determines the default port
when no explicit port is specified (`http` → 80, `https` → 443). TLS
(HTTPS proxy CONNECT tunnels) is not supported.
-/
def proxy? (b : Client.Builder) (url : String) : Option Client.Builder := do
let uri ← URI.parse? url
let auth ← uri.authority
let host := toString auth.host
let defaultPort : UInt16 := if uri.scheme.val == "https" then 443 else 80
let port : UInt16 := match auth.port with
| .value p => p
| _ => defaultPort
| _ => URI.Scheme.defaultPort uri.scheme
pure { b with config := { b.config with proxy := some (host, port) } }
/--
Sets the total request timeout (connect + send + receive).
Sets the request timeout (send + receive).
DNS resolution and TCP connect are not covered by this timeout;
use the OS-level socket timeout for those.
-/
def timeout (b : Client.Builder) (ms : Time.Millisecond.Offset) : Client.Builder :=
if h : 0 < ms then

279
src/Std/Internal/Http/Client/Agent.lean
View File

@@ -67,11 +67,6 @@ public structure Agent (α : Type) where
-/
port : UInt16
/--
URIs visited in the current redirect chain, used to detect cycles.
-/
redirectHistory : Array URI
/--
Cookie jar shared across all requests and redirects through this agent.
-/
@@ -94,8 +89,27 @@ public structure Agent (α : Type) where
-/
connectTo : Option (URI.Host → UInt16 → Async (Session α)) := none
/--
Called when a connection error is confirmed (i.e., `session.send` threw and all retries
are committed to using a fresh session). Receives the broken session together with the
host and port so the caller can:
* For pool agents: evict every session to that host so the next retry gets a fresh one.
* For standalone agents: close the session's request channel so the background loop exits.
The default closes the session channel; pool agents set this to an eviction function.
-/
onBrokenSession : Session α → URI.Host → UInt16 → Async Unit :=
fun s _ _ => discard <| s.close
namespace Agent
/--
Returns `true` for HTTP methods that are safe to retry on connection failure.
Non-idempotent methods (POST, PATCH) must not be retried automatically because
the server may have already processed the request before the connection dropped.
-/
private def isIdempotentMethod (m : Method) : Bool :=
m == .get || m == .head || m == .put || m == .delete || m == .options || m == .trace
/--
Rewrites an origin-form request target to absolute-form for proxy forwarding.
`GET /path?q=1 HTTP/1.1` becomes `GET http://host:port/path?q=1 HTTP/1.1`.
@@ -106,13 +120,15 @@ def toAbsoluteFormRequest
(scheme : URI.Scheme) (host : URI.Host) (port : UInt16) : Request Body.AnyBody :=
match request.line.uri with
| .originForm o =>
let pathStr := toString o.path
let queryStr := match o.query with | none => "" | some q => toString q
let portStr := if port == URI.Scheme.defaultPort scheme then "" else s!":{port}"
let urlStr := s!"{scheme}://{host}{portStr}{pathStr}{queryStr}"
match RequestTarget.parse? urlStr with
| some target => { request with line := { request.line with uri := target } }
| none => request
{ request with
line := { request.line with uri := .absoluteForm {
scheme,
path := o.path,
query := o.query.getD .empty,
authority := some { host, port := .value port }
}
}
}
| _ => request
/--
@@ -124,26 +140,30 @@ def ofTransport [Transport α] (socket : α) (scheme : URI.Scheme)
(host : URI.Host) (port : UInt16)
(connectTo : Option (URI.Host → UInt16 → Async (Session α)) := none)
(config : Config := {}) : Async (Agent α) := do
let session ← Session.new socket config
let cookieJar ← Cookie.Jar.new
pure { session, scheme, host, port, redirectHistory := #[], cookieJar, connectTo }
pure { session, scheme, host, port, cookieJar, connectTo }
/--
Injects matching cookies from `cookieJar` into the request headers for `host`.
Does nothing if the jar contains no matching cookies.
-/
def injectCookies (cookieJar : Cookie.Jar) (host : URI.Host)
def injectCookies (cookieJar : Cookie.Jar) (host : URI.Host) (scheme : URI.Scheme)
(request : Request Body.AnyBody) : Async (Request Body.AnyBody) := do
-- Respect an explicit Cookie header set by the caller.
if request.line.headers.contains .cookie then return request
let path := match request.line.uri with
| .originForm o => toString o.path
| .absoluteForm af => toString af.path
| _ => "/"
let cookies ← cookieJar.cookiesFor host path
match Cookie.Jar.toCookieHeader cookies with
| .originForm o => o.path
| .absoluteForm af => af.path
| _ => URI.Path.parseOrRoot "/"
match ← cookieJar.cookiesFor host path (secure := scheme.val == "https") with
| none => return request
| some cookieValue =>
let newHeaders :=
request.line.headers.insert Header.Name.cookie (Header.Value.ofString! cookieValue)
let newHeaders := request.line.headers.insert .cookie cookieValue
return { request with line := { request.line with headers := newHeaders } }
/--
@@ -171,87 +191,105 @@ inductive RedirectDecision where
Response is final, should validate status and return it.
-/
| done
/-- Follow a redirect to `(host, port, scheme)` with `request`, updating `history`. -/
| follow (host : URI.Host) (port : UInt16) (scheme : URI.Scheme)
(request : Request Body.AnyBody) (history : Array URI)
/--
Follow a redirect to `(host, port, scheme)` with `request`, updating `history`.
-/
| follow (host : URI.Host) (port : UInt16) (scheme : URI.Scheme) (request : Request Body.AnyBody)
/--
Inspects `response` and decides whether to follow a redirect.
Returns `.done` when:
- `remaining` is 0 or the response is not a redirection,
- the `Location` header is absent,
- a redirect cycle is detected, or
- the `Location` header is absent, or
- the `Location` value cannot be parsed.
Returns `.follow` with the rewritten request (method, body, and headers adjusted per
RFC 9110 §15.4, including `Authorization` stripped on cross-origin hops) when a valid
redirect target is found. The response body is drained before returning `.follow`.
redirect target is found. The response body is drained (up to `drainLimit` bytes) before
returning `.follow`; if the body exceeds `drainLimit` the incoming channel is closed and
the connection is left to recover or time out.
-/
def decideRedirect
(remaining : Nat) (history : Array URI)
(remaining : Nat)
(currentHost : URI.Host) (currentPort : UInt16) (currentScheme : URI.Scheme)
(request : Request Body.AnyBody) (response : Response Body.Incoming)
(drainLimit : Nat)
: Async RedirectDecision := do
if remaining == 0 || !response.line.status.isRedirection then
if remaining == 0 ∨ !response.line.status.isRedirection then
return .done
let some locationValue := response.line.headers.get? Header.Name.location
let some locationValue := response.line.headers.get? .location
| return .done
let locationStr := locationValue.value
let locationURI := URI.parse? locationStr
discard <| ContextAsync.run (response.body.readAll (α := ByteArray))
if let some uri := locationURI then
if history.contains uri then return .done
let some target := RequestTarget.parse? locationStr
| return .done
-- Drain
discard <| ContextAsync.run do
try
discard <| response.body.readAll (α := ByteArray) (maximumSize := some drainLimit.toUInt64)
catch _ =>
response.body.close
let newMethod := match response.line.status with
| .seeOther => .get
| .movedPermanently | .found =>
if request.line.method == .post then .get else request.line.method
| _ => request.line.method
let bodyIsStreaming := match request.body with | .outgoing _ => true | _ => false
let newBody : Body.AnyBody :=
if newMethod == .get || newMethod == .head || newMethod != request.line.method then
.empty {}
else
request.body
if newMethod == .get || newMethod == .head || newMethod != request.line.method then .empty {}
else if bodyIsStreaming then .empty {}
else request.body
let newHistory := match locationURI with
| some uri => history.push uri
| none => history
let (newHost, newPort, newScheme) := match target with
| .absoluteForm af =>
let h := af.authority.map URI.Authority.host |>.getD currentHost
let p : UInt16 :=
match af.authority with
| some auth => match auth.port with
| URI.Port.value v => v
| _ => URI.Scheme.defaultPort af.scheme
| none => URI.Scheme.defaultPort af.scheme
(h, p, af.scheme)
| _ => (currentHost, currentPort, currentScheme)
let (newHost, newPort, newScheme) := match locationURI with
| some uri =>
if let some auth := uri.authority then
let h := auth.host
let p : UInt16 := match auth.port with
| .value p => p
| _ => URI.Scheme.defaultPort uri.scheme
(h, p, uri.scheme)
else (currentHost, currentPort, currentScheme)
| none => (currentHost, currentPort, currentScheme)
-- Avoid SSRF.
if newScheme.val != "http" && newScheme.val != "https" then
return .done
-- Strip Authorization
let isCrossOrigin := newHost != currentHost || newPort != currentPort || newScheme != currentScheme
-- Strip Authorization on cross-origin redirects to prevent credential leakage (RFC 9110 §15.4).
let crossOrigin := newHost != currentHost || newPort != currentPort
let newHeaders :=
if crossOrigin then request.line.headers.erase Header.Name.authorization
if isCrossOrigin then
request.line.headers
|>.erase Header.Name.authorization
|>.erase Header.Name.proxyAuthorization
|>.erase Header.Name.cookie
else request.line.headers
return .follow newHost newPort newScheme
{ line := { request.line with uri := target, method := newMethod, headers := newHeaders }
body := newBody
extensions := request.extensions }
newHistory
private partial def sendWithRedirects [Transport α]
(agent : Agent α) (request : Request Body.AnyBody)
(remaining : Nat) (retriesLeft : Nat) : Async (Response Body.Incoming) := do
(remaining : Nat) (retriesLeft : Nat)
(history : Array (URI.Host × UInt16 × String) := #[]) : Async (Response Body.Incoming) := do
-- Record the current URL in the history and detect redirect cycles.
let currentKey := (agent.host, agent.port, toString request.line.uri)
let history := history.push currentKey
-- Rewrite to absolute-form when a proxy is configured.
let request :=
if agent.session.config.proxy.isSome then
@@ -259,51 +297,62 @@ private partial def sendWithRedirects [Transport α]
else
request
let request ← injectCookies agent.cookieJar agent.host request
let request ← injectCookies agent.cookieJar agent.host agent.scheme request
let response ← try agent.session.send request
catch err => do
-- Connection error: retry with a fresh session if budget and factory allow.
if retriesLeft > 0 then
agent.onBrokenSession agent.session agent.host agent.port
let bodyIsReplayable := match request.body with | .outgoing _ => false | _ => true
if retriesLeft > 0 && isIdempotentMethod request.line.method && bodyIsReplayable then
if let some factory := agent.connectTo then
sleep agent.session.config.retryDelay
let newSession ← factory agent.host agent.port
return ← sendWithRedirects { agent with session := newSession } request remaining (retriesLeft - 1)
return ← sendWithRedirects { agent with session := newSession } request remaining (retriesLeft - 1) history
throw err
let response ← applyInterceptors agent.interceptors response
processCookies agent.cookieJar agent.host response.line.headers
match ← decideRedirect remaining agent.redirectHistory agent.host agent.port agent.scheme request response with
match ← decideRedirect remaining agent.host agent.port agent.scheme request response
agent.session.config.redirectBodyDrainLimit with
| .done =>
if let some validate := agent.session.config.validateStatus then
if !validate response.line.status then
throw (.userError s!"unexpected HTTP status: {response.line.status.toCode}")
return response
| .follow newHost newPort newScheme newRequest newHistory =>
| .follow newHost newPort newScheme newRequest =>
if let some policy := agent.session.config.redirectPolicy then
if !policy newHost newPort then
return response
let nextKey := (newHost, newPort, toString newRequest.line.uri)
if history.contains nextKey then
return response
if newHost != agent.host || newPort != agent.port then
-- For custom transports without a connectTo factory we cannot open a new
-- connection to a different host; return the redirect response as-is.
let some factory := agent.connectTo | return response
let _ ← agent.session.close
let some factory := agent.connectTo
| return response
let newSession ← factory newHost newPort
let response ← sendWithRedirects
{ session := newSession
scheme := newScheme
host := newHost
port := newPort
redirectHistory := newHistory
cookieJar := agent.cookieJar
interceptors := agent.interceptors
connectTo := some factory }
newRequest (remaining - 1) retriesLeft
-- Close the cross-host session: signals the background loop to shut down after
-- the response body is consumed (safe because the channel is only polled once
-- the current response is fully delivered and waitingForRequest becomes true).
let _ ← newSession.close
return response
sendWithRedirects
{ session := newSession
scheme := newScheme
host := newHost
port := newPort
cookieJar := agent.cookieJar
interceptors := agent.interceptors
connectTo := some factory
onBrokenSession := agent.onBrokenSession }
newRequest (remaining - 1) retriesLeft history
else
sendWithRedirects { agent with redirectHistory := newHistory } newRequest (remaining - 1) retriesLeft
sendWithRedirects agent newRequest (remaining - 1) retriesLeft history
/--
Send a request, automatically following redirects up to `config.maxRedirects` hops and
@@ -312,9 +361,9 @@ For cross-host redirects the agent reconnects using its `connectTo` factory (if
Cookies are automatically injected from the jar and `Set-Cookie` responses are stored.
Response interceptors are applied after every response.
-/
def send {β : Type} [Coe β Body.AnyBody] [Transport α]
(agent : Agent α) (request : Request β) : Async (Response Body.Incoming) :=
sendWithRedirects agent
def send {β : Type} [Coe β Body.AnyBody] [Transport α] (agent : Agent α) (request : Request β) : Async (Response Body.Incoming) :=
sendWithRedirects
agent
{ line := request.line, body := (request.body : Body.AnyBody), extensions := request.extensions }
agent.session.config.maxRedirects
agent.session.config.maxRetries
@@ -369,30 +418,12 @@ private def withHostHeader [Transport α] (rb : Agent.RequestBuilder α) : Agent
{ rb with builder := rb.builder.header! "Host" hostValue }
/--
Injects matching cookies from the agent's jar if no `Cookie` header is already present.
-/
private def withCookies [Transport α] (rb : Agent.RequestBuilder α) : Async (Agent.RequestBuilder α) := do
if rb.builder.line.headers.contains Header.Name.cookie then
return rb
let path := match rb.builder.line.uri with
| .originForm o => toString o.path
| .absoluteForm af => toString af.path
| _ => "/"
let cookies ← rb.agent.cookieJar.cookiesFor rb.agent.host path
match Cookie.Jar.toCookieHeader cookies with
| none => return rb
| some cookieValue =>
return { rb with builder := rb.builder.header! "Cookie" cookieValue }
/--
Prepares the builder by injecting Host and Cookie headers, then calls `f` to build
and send the request.
Prepares the builder by injecting the `Host` header, then calls `f` to build and send the
request. Cookie injection is handled by `Agent.injectCookies` inside `sendWithRedirects`.
-/
private def prepare [Transport α] (rb : Agent.RequestBuilder α)
(f : Agent.RequestBuilder α → Async (Response Body.Incoming)) : Async (Response Body.Incoming) := do
let rb := rb.withHostHeader
let rb ← rb.withCookies
f rb
(f : Agent.RequestBuilder α → Async (Response Body.Incoming)) : Async (Response Body.Incoming) :=
f rb.withHostHeader
/--
Adds a typed header to the request.
@@ -471,36 +502,46 @@ end Agent.RequestBuilder
namespace Agent
/-- Creates a GET request builder for the given path or URL. -/
/--
Creates a GET request builder for the given path or URL
-/
def get [Transport α] (agent : Agent α) (path : String) : Agent.RequestBuilder α :=
{ agent, builder := Request.get (RequestTarget.parse! path) }
/-- Creates a POST request builder for the given path or URL. -/
/--
Creates a POST request builder for the given path or URL
-/
def post [Transport α] (agent : Agent α) (path : String) : Agent.RequestBuilder α :=
{ agent, builder := Request.post (RequestTarget.parse! path) }
/-- Creates a PUT request builder for the given path or URL. -/
/--
Creates a PUT request builder for the given path or URL
-/
def put [Transport α] (agent : Agent α) (path : String) : Agent.RequestBuilder α :=
{ agent, builder := Request.put (RequestTarget.parse! path) }
/-- Creates a DELETE request builder for the given path or URL. -/
/--
Creates a DELETE request builder for the given path or URL
-/
def delete [Transport α] (agent : Agent α) (path : String) : Agent.RequestBuilder α :=
{ agent, builder := Request.delete (RequestTarget.parse! path) }
/-- Creates a PATCH request builder for the given path or URL. -/
/--
Creates a PATCH request builder for the given path or URL
-/
def patch [Transport α] (agent : Agent α) (path : String) : Agent.RequestBuilder α :=
{ agent, builder := Request.patch (RequestTarget.parse! path) }
/-- Creates a HEAD request builder for the given path or URL. -/
/--
Creates a HEAD request builder for the given path or URL
-/
def headReq [Transport α] (agent : Agent α) (path : String) : Agent.RequestBuilder α :=
{ agent, builder := Request.head (RequestTarget.parse! path) }
/-- Creates an OPTIONS request builder for the given path or URL. -/
/--
Creates an OPTIONS request builder for the given path or URL.
-/
def options [Transport α] (agent : Agent α) (path : String) : Agent.RequestBuilder α :=
{ agent, builder := Request.options (RequestTarget.parse! path) }
end Agent
end Client
end Http
end Std
end Std.Http.Client.Agent

21
src/Std/Internal/Http/Client/Config.lean
View File

@@ -57,7 +57,8 @@ structure Config where
keepAliveTimeout : { x : Time.Millisecond.Offset // 0 < x } := ⟨60000, by decide⟩
/--
Timeout for the entire request lifecycle (connect + read + write).
Timeout for the request lifecycle (send + receive) per connection.
DNS resolution and TCP connect are not covered by this timeout.
-/
requestTimeout : { x : Time.Millisecond.Offset // 0 < x } := ⟨120000, by decide⟩
@@ -105,6 +106,14 @@ structure Config where
-/
proxy : Option (String × UInt16) := none
/--
Maximum number of bytes allowed in a single response body.
When `some n`, reading more than `n` bytes from the body resolves the current
request with an error and closes the connection.
`none` (default) imposes no limit.
-/
maxResponseBodySize : Option Nat := none
/--
Optional predicate that decides whether a response status is acceptable.
When `none`, all status codes are accepted (no error is thrown).
@@ -119,6 +128,16 @@ structure Config where
-/
validateStatus : Option (Status → Bool) := none
/--
Maximum number of bytes drained from an intermediate redirect response body before
-/
redirectBodyDrainLimit : Nat := 1024 * 1024
/--
Optional predicate called before following each redirect.
-/
redirectPolicy : Option (URI.Host → UInt16 → Bool) := none
namespace Config
/--

27
src/Std/Internal/Http/Client/Connection.lean
View File

@@ -161,6 +161,7 @@ private structure ConnectionState where
uploadBytes : UInt64 := 0
downloadProgress : Option (Watch UInt64) := none
downloadBytes : UInt64 := 0
downloadBodyBytes : UInt64 := 0
@[inline]
private def requestHasExpectContinue (request : Request Body.Operations) : Bool :=
@@ -230,6 +231,10 @@ private def processH1Events
| .needMoreData expect =>
st := { st with requiresData := true, expectData := expect }
-- `.needAnswer` is emitted by processWrite when the writer is in `waitingHeaders`
-- state in `.sending` mode, signalling that the client machine needs the next request.
-- The client loop tracks this through `waitingForRequest` instead, so this event
-- is intentionally a no-op here.
| .needAnswer => pure ()
| .endHeaders head =>
@@ -305,6 +310,7 @@ private def processH1Events
uploadBytes := 0
downloadProgress := none
downloadBytes := 0
downloadBodyBytes := 0
}
| .failed err =>
@@ -395,7 +401,28 @@ private def handleRecvEvent
let mut st := { state with machine := newMachine }
if let some pulled := pulledChunk then
let newBodyBytes := st.downloadBodyBytes + pulled.chunk.data.size.toUInt64
st := { st with downloadBodyBytes := newBodyBytes }
-- Enforce the response body size limit before writing data to the caller.
if let some maxSize := config.maxResponseBodySize then
if newBodyBytes > maxSize.toUInt64 then
if let some packet := st.currentRequest then
packet.onError (.userError "response body exceeds maximum allowed size")
if let some body := st.responseOutgoing then
if ¬(← Body.Writer.isClosed body) then Body.Writer.close body
if let some w := st.downloadProgress then Watch.close w
return ({ st with
machine := st.machine.closeWriter.closeReader.noMoreInput
currentRequest := none
responseOutgoing := none
downloadProgress := none
}, false)
if let some body := st.responseOutgoing then
-- If the caller has dropped/closed the incoming side, the write fails.
-- Silently swallowing the error is correct: the loop must continue pulling
-- wire bytes to keep the connection in a valid state for reuse.
try Body.Writer.send body pulled.chunk pulled.incomplete
catch _ => pure ()

89
src/Std/Internal/Http/Client/Pool.lean
View File

@@ -54,6 +54,7 @@ private def createTcpSession (host : URI.Host) (port : UInt16) (config : Config)
-- Try each resolved address in order; return on first successful connect.
-- This handles hosts that resolve to both IPv6 (::1) and IPv4 (127.0.0.1).
let mut lastErr : IO.Error := IO.userError s!"could not connect to {connectHost.quote}:{connectPort}"
for ipAddr in addrs do
let socketAddr : Std.Net.SocketAddress := match ipAddr with
| .v4 ip => .v4 ⟨ip, connectPort⟩
@@ -92,6 +93,11 @@ public structure Agent.Pool where
-/
cookieJar : Cookie.Jar
/--
Monotonically increasing counter used to assign unique IDs to pooled sessions.
-/
nextId : Mutex UInt64
/--
Response interceptors applied (in order) after every response from any session in the pool.
-/
@@ -105,7 +111,8 @@ Creates a new, empty connection pool.
def new (config : Config := {}) (maxPerHost : Nat := 4) : Async Agent.Pool := do
let state ← Mutex.new (∅ : Std.HashMap (String × UInt16) (Array (Session Socket.Client) × Nat))
let cookieJar ← Cookie.Jar.new
pure { state, maxPerHost, config, cookieJar }
let nextId ← Mutex.new (1 : UInt64)
pure { state, maxPerHost, config, cookieJar, nextId }
/--
Returns a session for `(host, port)`, reusing an existing one when available or
@@ -127,6 +134,11 @@ def getOrCreateSession (pool : Agent.Pool) (host : URI.Host) (port : UInt16) : A
-- Slow path: create a new session and register it.
let session ← createTcpSession host port pool.config
let newId ← pool.nextId.atomically do
let id ← MonadState.get
MonadState.set (id + 1)
return id
let session := { session with id := newId }
pool.state.atomically do
let st ← MonadState.get
let (sessions, idx) := (st.get? (toString host, port)).getD (#[], 0)
@@ -138,48 +150,17 @@ def getOrCreateSession (pool : Agent.Pool) (host : URI.Host) (port : UInt16) : A
return session
/--
Removes all sessions for `(host, port)` from the pool.
Called when a connection error is detected so the next request gets a fresh connection.
Removes a single broken session from the pool by its unique ID.
Healthy sibling sessions to the same host are preserved.
-/
private def evictSessions (pool : Agent.Pool) (host : URI.Host) (port : UInt16) : Async Unit := do
private def evictSession (pool : Agent.Pool) (host : URI.Host) (port : UInt16) (sessionId : UInt64) : Async Unit := do
pool.state.atomically do
let st ← MonadState.get
MonadState.set (st.erase (toString host, port))
private partial def sendPoolWithRedirects
(pool : Agent.Pool) (host : URI.Host) (port : UInt16)
(request : Request Body.AnyBody)
(remaining : Nat)
(retriesLeft : Nat)
(redirectHistory : Array URI) : Async (Response Body.Incoming) := do
let request :=
if pool.config.proxy.isSome then
Agent.toAbsoluteFormRequest request (URI.Scheme.ofPort port) host port
else
request
let request ← Agent.injectCookies pool.cookieJar host request
let session ← pool.getOrCreateSession host port
let response ← try session.send request
catch err => do
evictSessions pool host port
if retriesLeft > 0 then
sleep pool.config.retryDelay
return ← sendPoolWithRedirects pool host port request remaining (retriesLeft - 1) redirectHistory
throw err
let response ← Agent.applyInterceptors pool.interceptors response
Agent.processCookies pool.cookieJar host response.line.headers
match ← Agent.decideRedirect remaining redirectHistory host port (URI.Scheme.ofPort port) request response with
| .done =>
if let some validate := pool.config.validateStatus then
if !validate response.line.status then
throw (.userError s!"unexpected HTTP status: {response.line.status.toCode}")
return response
| .follow newHost newPort _ newRequest newHistory =>
sendPoolWithRedirects pool newHost newPort newRequest (remaining - 1) retriesLeft newHistory
match st.get? (toString host, port) with
| none => pure ()
| some (sessions, idx) =>
let sessions' := sessions.filter (fun s => s.id != sessionId)
MonadState.set (st.insert (toString host, port) (sessions', idx))
/--
Sends a request through a pooled session for `(host, port)`, injecting cookies from the
@@ -189,12 +170,19 @@ failure (retrying up to `config.maxRetries` times).
-/
def send {β : Type} [Coe β Body.AnyBody]
(pool : Agent.Pool) (host : URI.Host) (port : UInt16)
(request : Request β) : Async (Response Body.Incoming) :=
sendPoolWithRedirects pool host port
{ line := request.line, body := (request.body : Body.AnyBody), extensions := request.extensions }
pool.config.maxRedirects
pool.config.maxRetries
#[]
(request : Request β) : Async (Response Body.Incoming) := do
let session ← pool.getOrCreateSession host port
Agent.send {
session
scheme := URI.Scheme.ofPort port
host := host
port := port
cookieJar := pool.cookieJar
interceptors := pool.interceptors
connectTo := some pool.getOrCreateSession
onBrokenSession := fun brokenSession h p => pool.evictSession h p brokenSession.id
} request
end Agent.Pool
@@ -211,11 +199,6 @@ def connect (host : URI.Host) (port : UInt16) (config : Config := {}) : Async (A
let session ← createTcpSession host port config
let cookieJar ← Cookie.Jar.new
let scheme := URI.Scheme.ofPort port
pure { session, scheme, host, port, redirectHistory := #[], cookieJar,
connectTo := some (fun h p => createTcpSession h p config) }
pure { session, scheme, host, port, cookieJar, connectTo := some (createTcpSession · · config) }
end Agent
end Client
end Http
end Std
end Std.Http.Client.Agent

6
src/Std/Internal/Http/Client/Session.lean
View File

@@ -44,6 +44,12 @@ public structure Session (α : Type) where
-/
config : Config
/--
Unique identifier assigned by the pool when this session is registered.
Zero for sessions created outside a pool.
-/
id : UInt64 := 0
namespace Session
/--

147
src/Std/Internal/Http/Data/Cookie.lean
View File

@@ -8,6 +8,8 @@ module
prelude
public import Std.Sync.Mutex
public import Std.Internal.Http.Data.URI
public import Std.Internal.Http.Data.Cookie.Parser
public import Std.Internal.Http.Data.Headers
public import Init.Data.String
public import Init.Data.Array.Basic
public import Init.Data.List.Basic
@@ -206,8 +208,14 @@ structure Cookie where
-/
secure : Bool
/--
When `true` the cookie must not be exposed to non-HTTP APIs.
Stored for completeness; no client-side script enforcement applies here.
-/
httpOnly : Bool
/--
A thread-safe HTTP cookie jar.
A HTTP cookie jar.
Reference: https://www.rfc-editor.org/rfc/rfc6265#section-5
-/
@@ -236,34 +244,24 @@ private def domainMatches (cookieDomain : URI.Host) (hostOnly : Bool) (host : UR
/--
Path matching per RFC 6265 §5.1.4.
-/
private def pathMatches (cookiePath : URI.Path) (requestPath : String) : Bool :=
let s := toString cookiePath
requestPath == s ||
(requestPath.startsWith s &&
(s.endsWith "/" || requestPath.startsWith (s ++ "/")))
/--
Splits `s` at the first occurrence of `sep`, returning `(before, after)`.
Returns `(s, "")` when `sep` does not appear in `s`.
-/
private def splitFirst (s : String) (sep : String) : String × String :=
match s.splitOn sep with
| [] | [_] => (s, "")
| first :: rest => (first, String.intercalate sep rest)
A request path matches a cookie path when they are identical, or when the cookie path is a
strict segment-wise prefix of the request path. Segment boundaries correspond to `/`, so
`/foo` never prefix-matches `/foobar` (different segments).
/--
Attempts to parse a host string into a `URI.Host`, trying IPv4, bracketed IPv6, and
domain name forms in order.
A trailing `/` in the cookie path is normalised away before the prefix test; this covers
both RFC conditions:
- cookie-path ends with `/` → its meaningful segments are a strict prefix of request-path.
- first char after prefix is `/` → satisfied automatically at segment boundaries.
-/
private def parseHostStr (s : String) : Option URI.Host :=
if let some ip := Net.IPv4Addr.ofString s then
some (.ipv4 ip)
else if s.startsWith "[" && s.endsWith "]" && s.length > 2 then
let inner := s.dropEnd 1 |>.drop 1 |>.toString
(Net.IPv6Addr.ofString inner).map .ipv6
else
(URI.DomainName.ofString? s).map .name
private def pathMatches (cookiePath : URI.Path) (requestPath : URI.Path) : Bool :=
requestPath == cookiePath ||
let cp :=
if cookiePath.hasTrailingSlash && !cookiePath.isEmpty
then cookiePath.segments.pop
else cookiePath.segments
requestPath.segments.size > cp.size &&
requestPath.startsWith { cookiePath with segments := cp }
/--
Parses a single `Set-Cookie` header value and stores the resulting cookie.
@@ -273,70 +271,79 @@ Parses a single `Set-Cookie` header value and stores the resulting cookie.
Reference: https://www.rfc-editor.org/rfc/rfc6265#section-5.2
-/
def processSetCookie (jar : Jar) (host : URI.Host) (headerValue : String) : BaseIO Unit := do
let rawParts := (headerValue.splitOn ";").map String.trimAscii
let some rawNameValue := rawParts[0]?
let .ok parsed := Cookie.Parser.parseSetCookie.run headerValue.toUTF8
| return ()
let (rawName, rawValue) := splitFirst rawNameValue.toString "="
let some cookieName := Cookie.Name.ofString? parsed.name
| return ()
let some cookieName := Cookie.Name.ofString? rawName | return ()
let some cookieValue := Cookie.Value.ofString? rawValue | return ()
let some cookieValue := Cookie.Value.ofString? parsed.value
| return ()
let mut cookieDomain : Option URI.Host := none
let mut cookiePath : URI.Path := URI.Path.parseOrRoot "/"
let mut secure := false
let cookiePath : URI.Path :=
if let some p := parsed.path then URI.Path.parseOrRoot p
else URI.Path.parseOrRoot "/"
for attr in rawParts.drop 1 do
let (attrName, attrVal) := splitFirst attr.toString "="
match attrName.trimAscii.toString.toLower with
| "domain" =>
let d := if attrVal.startsWith "." then attrVal.drop 1 else attrVal
let d := d.trimAscii.toString
if !d.isEmpty then
cookieDomain := (URI.DomainName.ofString? d).map URI.Host.name
| "path" =>
let p := attrVal.trimAscii.toString
if !p.isEmpty then cookiePath := URI.Path.parseOrRoot p
| "secure" => secure := true
| _ => pure ()
-- RFC 6265 §5.2.3: resolve domain; missing or invalid Domain → host-only
let (domain, hostOnly) :=
match parsed.domain with
| some d =>
match URI.DomainName.ofString? d with
| some name => (URI.Host.name name, false)
| none => (host, true)
| none => (host, true)
let (domain, hostOnly) ← match cookieDomain with
| some d => pure (d, false)
| none => pure (host, true)
-- RFC 6265 §5.3 step 6: if domain attribute is set, the origin host must domain-match it.
-- This prevents a server at api.example.com from setting Domain=evil.com or Domain=com.
if !hostOnly && !domainMatches domain false host then
return ()
let cookie : Cookie := { name := cookieName, value := cookieValue, domain, hostOnly, path := cookiePath, secure }
-- RFC 6265 §5.2.2: Max-Age ≤ 0 signals deletion — remove any matching cookie and stop.
if let some maxAgeVal := parsed.maxAge then
if maxAgeVal ≤ 0 then
jar.cookies.atomically do
let cs ← get
set (cs.filter fun c => !(c.name == cookieName && c.domain == domain && c.path == cookiePath))
return ()
let cookie : Cookie := {
name := cookieName
value := cookieValue
domain
hostOnly
path := cookiePath
secure := parsed.secure
httpOnly := parsed.httpOnly
}
-- Limit the total cookie count to prevent unbounded memory growth.
-- RFC 6265 §6.1 recommends supporting at least 3000 cookies total.
let maxCookies := 3000
jar.cookies.atomically do
let cs ← get
let cs := cs.filter fun c =>
!(c.name == cookie.name && c.domain == cookie.domain && c.path == cookie.path)
set (cs.push cookie)
let cs := cs.filter fun c => !(c.name == cookie.name && c.domain == cookie.domain && c.path == cookie.path)
if cs.size < maxCookies then
set (cs.push cookie)
/--
Returns all cookies that should be sent for a request to `host` at `path`.
Pass `secure := true` when the request channel is HTTPS.
Returns the `Cookie` header value for all cookies that should be sent for a request to `host`
at `path`. Pass `secure := true` when the request channel is HTTPS. Returns `none` when no
cookies match.
Reference: https://www.rfc-editor.org/rfc/rfc6265#section-5.4
-/
def cookiesFor
(jar : Jar) (host : URI.Host) (path : String)
(secure : Bool := false) : BaseIO (Array Cookie) :=
(jar : Jar) (host : URI.Host) (path : URI.Path)
(secure : Bool := false) : BaseIO (Option Header.Value) :=
jar.cookies.atomically do
let cs ← get
return cs.filter fun c =>
let matching := cs.filter fun c =>
domainMatches c.domain c.hostOnly host &&
pathMatches c.path path &&
(!c.secure || secure)
/--
Formats an array of cookies into a `Cookie` header value string.
Returns `none` when the array is empty.
-/
def toCookieHeader (cookies : Array Cookie) : Option String :=
if cookies.isEmpty then
none
else
some (String.intercalate "; " (cookies.map (fun c => c.name.value ++ "=" ++ c.value.value)).toList)
if matching.isEmpty then
return none
else
return Header.Value.ofString? (String.intercalate "; " (matching.map (fun c => c.name.value ++ "=" ++ c.value.value)).toList)
end Std.Http.Cookie.Jar

225
src/Std/Internal/Http/Data/Cookie/Parser.lean Normal file
View File

@@ -0,0 +1,225 @@
/-
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sofia Rodrigues
-/
module
prelude
import Init.Data.String
public import Std.Internal.Parsec
public import Std.Internal.Parsec.ByteArray
public import Std.Internal.Http.Internal.Char
public section
/-!
# Cookie Parser
This module provides a `Set-Cookie` response-header parser following RFC 6265 §4.1. The
`parseSetCookie` combinator returns a `Parsed` structure with raw `String` fields; callers are
responsible for validating cookie-name and cookie-value semantics (e.g. via `Cookie.Name.ofString?`
and `Cookie.Value.ofString?`).
On parse failure the cookie is silently discarded per RFC 6265 §5.2.
Reference: https://www.rfc-editor.org/rfc/rfc6265#section-4.1
-/
namespace Std.Http.Cookie.Parser
set_option linter.all true
open Std Internal Parsec ByteArray Internal.Char
/-
cookie-octet = %x21 / %x23-2B / %x2D-3A / %x3C-5B / %x5D-7E
; US-ASCII visible characters excluding SP, DQUOTE,
; comma, semicolon, and backslash.
; Reference: https://www.rfc-editor.org/rfc/rfc6265#section-4.1.1
-/
@[inline]
private def isCookieOctetByte (c : UInt8) : Bool :=
c == 0x21 ||
(0x23 ≤ c && c ≤ 0x2B) ||
(0x2D ≤ c && c ≤ 0x3A) ||
(0x3C ≤ c && c ≤ 0x5B) ||
(0x5D ≤ c && c ≤ 0x7E)
/-
av-octet = %x20-3A / %x3C-7E
; any CHAR except CTLs or ";"
; Reference: https://www.rfc-editor.org/rfc/rfc6265#section-4.1.1
-/
@[inline]
private def isAvOctetByte (c : UInt8) : Bool :=
(0x20 ≤ c && c ≤ 0x3A) || (0x3C ≤ c && c ≤ 0x7E)
/-
token = 1*tchar
tchar = "!" / "#" / "$" / "%" / "&" / "'" / "*" / "+" / "-" / "." /
"^" / "_" / "`" / "|" / "~" / DIGIT / ALPHA
; Reference: https://www.rfc-editor.org/rfc/rfc9110#section-5.6.2
-/
@[inline]
private def parseToken (limit : Nat) : Parser ByteSlice :=
takeWhile1AtMost (fun c => tchar (Char.ofUInt8 c)) limit
/--
Parsed result of a `Set-Cookie` header value, prior to semantic validation.
Cookie-name and cookie-value are raw strings that callers must validate
(e.g. via `Cookie.Name.ofString?` and `Cookie.Value.ofString?`).
- `domain`: the `Domain` attribute value with any leading `.` already stripped;
`none` if the attribute is absent.
- `path`: the `Path` attribute value (guaranteed to start with `/`);
`none` if the attribute is absent or does not start with `/`.
- `secure`: `true` when the `Secure` attribute is present.
- `httpOnly`: `true` when the `HttpOnly` attribute is present.
-/
structure Parsed where
/--
Raw cookie name (an HTTP token).
-/
name : String
/--
Raw cookie value (`*cookie-octet` or double-quoted).
-/
value : String
/--
`Domain` attribute value with any leading `.` stripped, or `none` if absent.
-/
domain : Option String
/--
`Path` attribute value starting with `/`, or `none` if absent or invalid.
-/
path : Option String
/--
`true` when the `Secure` attribute is present.
-/
secure : Bool
/-- `true` when the `HttpOnly` attribute is present. -/
httpOnly : Bool
/-- `Max-Age` attribute value in seconds, or `none` if absent or unparseable.
Values ≤ 0 signal cookie deletion per RFC 6265 §5.2.2. -/
maxAge : Option Int := none
-- cookie-name = token
private def parseCookieName : Parser String := do
let bytes ← parseToken 4096
let some str := String.fromUTF8? bytes.toByteArray
| fail "invalid cookie name encoding"
return str
/-
cookie-value = *cookie-octet / ( DQUOTE *cookie-octet DQUOTE )
-/
private def parseCookieValue : Parser String := do
let bytes ←
if (← peekWhen? (· == '"'.toUInt8)).isSome then
skipByte '"'.toUInt8
let inner ← takeWhileAtMost isCookieOctetByte 4096
skipByte '"'.toUInt8
pure inner
else
takeWhileAtMost isCookieOctetByte 4096
let some str := String.fromUTF8? bytes.toByteArray
| fail "invalid cookie value encoding"
return str
-- av-name = token (parsed case-insensitively)
private def parseAttrName : Parser String := do
let bytes ← takeWhileAtMost (fun c => tchar (Char.ofUInt8 c)) 256
return (String.fromUTF8! bytes.toByteArray).toLower
-- av-value = *av-octet
private def parseAttrValue : Parser String := do
let bytes ← takeWhileAtMost isAvOctetByte 4096
let some str := String.fromUTF8? bytes.toByteArray
| fail "invalid attribute value encoding"
return str
/-
cookie-av = expires-av / max-age-av / domain-av / path-av / secure-av /
httponly-av / extension-av
domain-av = "Domain=" domain-value
domain-value = <subdomain> ; as per RFC 1034, Section 3.5
path-av = "Path=" path-value
path-value = *av-octet
secure-av = "Secure"
httponly-av = "HttpOnly"
extension-av = *av-octet
-/
private def parseCookieAv : Parser (String × Option String) := do
let name ← parseAttrName
let value ← optional (attempt (skipByte '='.toUInt8 *> parseAttrValue))
return (name, value)
/-
set-cookie-string = cookie-pair *( ";" SP cookie-av )
cookie-pair = cookie-name "=" cookie-value
-/
/--
Parses a `Set-Cookie` header value and returns a `Parsed` result.
Attribute processing follows RFC 6265 §5.2:
- `Domain`: leading `.` is stripped; invalid domain strings set `domain` to `none`.
- `Path`: values not starting with `/` set `path` to `none` (caller uses the default `/`).
- `Secure`: sets `secure` to `true` regardless of whether a value follows the attribute name.
- `HttpOnly`: sets `httpOnly` to `true`.
- All other attributes (including `Expires`, `Max-Age`, `SameSite`) are ignored.
-/
public def parseSetCookie : Parser Parsed := do
let name ← parseCookieName
skipByte '='.toUInt8
let value ← parseCookieValue
-- *( ";" SP cookie-av )
let attrs ← many (attempt do
skipByte ';'.toUInt8
let _ ← optional (skipByte ' '.toUInt8)
parseCookieAv)
let mut domain : Option String := none
let mut path : Option String := none
let mut secure := false
let mut httpOnly := false
let mut maxAge : Option Int := none
for (attrName, attrVal) in attrs do
match attrName with
| "domain" =>
let v := (attrVal.getD "").trimAscii.toString
-- RFC 6265 §5.2.3: ignore a leading U+002E FULL STOP character
let v := if v.startsWith "." then (v.drop 1).toString else v
if !v.isEmpty then domain := some v
| "path" =>
let v := (attrVal.getD "").trimAscii.toString
-- RFC 6265 §5.2.4: if av-value is empty or does not start with "/", use default
if !v.isEmpty && v.startsWith "/" then path := some v
| "secure" => secure := true
| "httponly" => httpOnly := true
| "max-age" =>
-- RFC 6265 §5.2.2: parse an optional leading '-' followed by one or more digits.
if let some v := attrVal then
let s := v.trimAscii.toString
let (neg, digits) := if s.startsWith "-" then (true, s.drop 1) else (false, s)
if !digits.isEmpty && digits.all Char.isDigit then
let absVal : Nat := digits.foldl (fun acc c => acc * 10 + (c.toNat - '0'.toNat)) 0
maxAge := some (if neg then -(absVal : Int) else (absVal : Int))
| _ => pure ()
return { name, value, domain, path, secure, httpOnly, maxAge }
end Std.Http.Cookie.Parser

5
src/Std/Internal/Http/Data/Headers/Name.lean
View File

@@ -192,4 +192,9 @@ Standard Location header name
-/
def location : Header.Name := .mk "location"
/--
Standard Proxy-Authorization header name
-/
def proxyAuthorization : Header.Name := .mk "proxy-authorization"
end Std.Http.Header.Name

26
src/Std/Internal/Http/Data/URI/Basic.lean
View File

@@ -381,6 +381,32 @@ def toDecodedSegments (p : Path) : Array String :=
p.segments.map fun seg =>
seg.decode.getD (toString seg)
/--
Returns `true` if `pre` is a segment-wise prefix of `p`. Each segment in `pre` must equal
the corresponding segment in `p` by encoded value. An absolute `pre` additionally requires
`p` to be absolute.
-/
def startsWith (p pre : Path) : Bool :=
(!pre.absolute || p.absolute) &&
pre.segments.size ≤ p.segments.size &&
(Array.range pre.segments.size).all fun i => p.segments[i]! == pre.segments[i]!
/--
Returns `true` if the path ends with a trailing slash. The root path (`/`) is considered to
have a trailing slash.
-/
def hasTrailingSlash (p : Path) : Bool :=
(p.absolute && p.segments.isEmpty) ||
(p.segments.back?.map (toString · == "") |>.getD false)
/--
Ensures the path ends with a trailing slash by appending an empty segment if needed. Idempotent:
the root path (`/`) and any path already ending with `/` are returned unchanged.
-/
def ensureTrailingSlash (p : Path) : Path :=
if p.hasTrailingSlash then p
else { p with segments := p.segments.push (EncodedSegment.encode "") }
end Path
/--

1
src/Std/Sync.lean
View File

@@ -18,5 +18,6 @@ public import Std.Sync.Broadcast
public import Std.Sync.StreamMap
public import Std.Sync.CancellationToken
public import Std.Sync.CancellationContext
public import Std.Sync.Watch
@[expose] public section

319
src/Std/Sync/Watch.lean Normal file
View File

@@ -0,0 +1,319 @@
/-
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sofia Rodrigues
-/
module
prelude
public import Init.Data.Queue
public import Std.Sync.Mutex
public import Std.Internal.Async.Select
public section
open Std.Internal.IO.Async
/-!
This module contains the implementation of `Std.Watch`. `Std.Watch` is a single-value watch
channel, inspired by [tokio's watch implementation](https://github.com/tokio-rs/tokio/blob/master/tokio/src/sync/watch.rs).
A watch channel holds a single value that can be updated by the sender. Multiple receivers
can independently observe the current value and wait for it to change.
Unlike `Std.Channel`, a watch channel:
- Retains only the latest value, not a queue of messages.
- Allows receivers to read the current value without consuming it.
- Notifies all receivers when the value changes (broadcast semantics on change).
- Returns an error on `changed` if the sender has been dropped.
-/
namespace Std
/--
Errors that may be thrown while interacting with the watch channel API.
-/
inductive Watch.Error where
/--
The sender was dropped, so no new values will ever be sent.
-/
| closed
deriving Repr, DecidableEq, Hashable
instance : ToString Watch.Error where
toString
| .closed => "watch channel sender was dropped"
instance : MonadLift (EIO Watch.Error) IO where
monadLift x := EIO.toIO (.userError <| toString ·) x
private inductive Watch.Waiter (α : Type) where
| normal (promise : IO.Promise α)
| select (waiter : Internal.IO.Async.Waiter α)
private def Watch.Waiter.resolve (c : Watch.Waiter α) (x : α) : BaseIO Bool := do
match c with
| .normal promise =>
promise.resolve x
return true
| .select waiter =>
waiter.race (return false) fun promise => do
promise.resolve (.ok x)
return true
/--
The shared state of a watch channel.
-/
private structure Watch.State (α : Type) where
/--
The current value held by the watch channel.
-/
value : α
/--
Monotonically increasing version. Incremented on every `send`.
-/
version : Nat
/--
Whether the sender has been dropped (closed).
-/
closed : Bool
/--
Receivers waiting for the value to change.
-/
waiters : Std.Queue (Watch.Waiter (Except Watch.Error Unit))
deriving Nonempty
/--
A watch channel sender. Holds a reference to the shared state and can update the value.
-/
structure Watch (α : Type) where
private mk ::
private state : Mutex (Watch.State α)
deriving Nonempty
/--
A watch channel receiver. Each receiver independently tracks the version it last observed.
-/
structure Watch.Receiver (α : Type) where
private mk ::
private state : Mutex (Watch.State α)
private lastSeen : IO.Ref Nat
deriving Nonempty
namespace Watch
/--
Creates a new watch channel with an initial value. Returns the sender and a receiver.
-/
def new (initial : α) : BaseIO (Watch α × Watch.Receiver α) := do
let state ← Mutex.new {
value := initial
version := 0
closed := false
waiters := ∅
}
let lastSeen ← IO.mkRef 0
return (⟨state⟩, ⟨state, lastSeen⟩)
/--
Sends a new value, updating the watched value and notifying all waiting receivers.
-/
def send (w : Watch α) (v : α) : BaseIO Unit := do
w.state.atomically do
let st ← get
let newVersion := st.version + 1
set { st with value := v, version := newVersion, waiters := ∅ }
for waiter in st.waiters.toArray do
discard <| waiter.resolve (.ok ())
/--
Closes the watch channel, signaling to receivers that no more values will be sent.
Waiting receivers will be woken up and their `changed` call will return `Watch.Error.closed`.
-/
def close (w : Watch α) : BaseIO Unit := do
w.state.atomically do
let st ← get
set { st with closed := true, waiters := ∅ }
for waiter in st.waiters.toArray do
discard <| waiter.resolve (.error .closed)
/--
Returns `true` if the sender has been closed.
-/
def isClosed (w : Watch α) : BaseIO Bool :=
w.state.atomically do
return (← get).closed
/--
Returns the current value held by the watch channel, as seen from the sender side.
-/
def current (w : Watch α) : BaseIO α :=
w.state.atomically do
return (← MonadState.get).value
namespace Receiver
/--
Borrow the current value without marking it as seen.
-/
def borrow (r : Watch.Receiver α) : BaseIO α :=
r.state.atomically do
return (← get).value
/--
Borrow the current value and mark the current version as seen, so that
the next `changed` call will only wake on a strictly newer value.
-/
def borrowAndUpdate (r : Watch.Receiver α) : BaseIO α := do
r.state.atomically do
let st ← get
r.lastSeen.set st.version
return st.value
/--
Returns `true` if the watched value has changed since this receiver last called
`borrowAndUpdate` or `changed`.
-/
def hasChanged (r : Watch.Receiver α) : BaseIO Bool := do
r.state.atomically do
let st ← get
let seen ← r.lastSeen.get
return st.version > seen
/--
Wait until the watched value changes relative to the version last seen by this receiver.
Returns `ok ()` on success or `error Watch.Error.closed` if the sender was dropped.
After a successful return the new value can be retrieved with `borrow` or `borrowAndUpdate`.
-/
partial def changed (r : Watch.Receiver α) : BaseIO (Task (Except Watch.Error Unit)) := do
r.state.atomically do
let st ← get
let seen ← r.lastSeen.get
if st.version > seen then
r.lastSeen.set st.version
return .pure <| .ok ()
else if st.closed then
return .pure <| .error .closed
else
let promise ← IO.Promise.new
modify fun s => { s with waiters := s.waiters.enqueue (.normal promise) }
BaseIO.bindTask promise.result? fun
| none => return .pure <| .error .closed
| some (Except.error e) => return .pure <| .error e
| some (Except.ok ()) =>
/- A notification arrived; recurse so `lastSeen` is updated atomically. -/
r.changed
/--
Creates a `Selector` that resolves when the watched value changes.
-/
def changedSelector (r : Watch.Receiver α) : Selector (Except Watch.Error Unit) where
tryFn := do
r.state.atomically do
let st ← get
let seen ← r.lastSeen.get
if st.version > seen then
r.lastSeen.set st.version
return some (.ok ())
else if st.closed then
return some (.error .closed)
else
return none
registerFn waiter := do
r.state.atomically do
let st ← get
let seen ← r.lastSeen.get
if st.version > seen || st.closed then
let result : Except Watch.Error Unit :=
if st.version > seen then .ok () else .error .closed
if st.version > seen then r.lastSeen.set st.version
waiter.race (return ()) fun promise =>
promise.resolve (.ok result)
else
modify fun s => { s with waiters := s.waiters.enqueue (.select waiter) }
unregisterFn := do
r.state.atomically do
let st ← get
let waiters ← st.waiters.filterM fun
| .normal _ => return true
| .select w => return !(← w.checkFinished)
set { st with waiters }
end Receiver
/--
A sync wrapper around `Watch.Receiver` for blocking use.
-/
@[expose] def Sync (α : Type) : Type := Watch α
/--
A sync wrapper around `Watch.Receiver` for blocking use.
-/
@[expose] def Sync.Receiver (α : Type) : Type := Watch.Receiver α
namespace Sync
/--
Creates a new watch channel with an initial value. Returns the sender and a sync receiver.
-/
@[inline]
def new (initial : α) : BaseIO (Sync α × Sync.Receiver α) :=
Watch.new initial
/--
Sends a new value, updating the watched value and notifying all waiting receivers.
-/
@[inline]
def send (w : Sync α) (v : α) : BaseIO Unit :=
Watch.send w v
/--
Closes the watch channel.
-/
@[inline]
def close (w : Sync α) : BaseIO Unit :=
Watch.close w
/--
Returns `true` if the sender has been closed.
-/
@[inline]
def isClosed (w : Sync α) : BaseIO Bool :=
Watch.isClosed w
namespace Receiver
/--
Borrow the current value without marking it as seen.
-/
@[inline]
def borrow (r : Sync.Receiver α) : BaseIO α :=
Watch.Receiver.borrow r
/--
Borrow the current value and mark it as seen.
-/
@[inline]
def borrowAndUpdate (r : Sync.Receiver α) : BaseIO α :=
Watch.Receiver.borrowAndUpdate r
/--
Returns `true` if the watched value has changed since last seen.
-/
@[inline]
def hasChanged (r : Sync.Receiver α) : BaseIO Bool :=
Watch.Receiver.hasChanged r
/--
Block until the watched value changes. Returns `ok ()` or `error Watch.Error.closed`.
-/
def changed (r : Sync.Receiver α) : BaseIO (Except Watch.Error Unit) := do
IO.wait (← Watch.Receiver.changed r)
end Receiver
end Sync
end Watch
end Std

431
tests/elab/async_http_client_security.lean Normal file
View File

@@ -0,0 +1,431 @@
import Std.Internal.Http
import Std.Internal.Async
import Std.Internal.Async.Timer
open Std.Internal.IO Async
open Std Http
/-!
# HTTP Client Security Tests
Tests for security properties of the HTTP client:
- `Authorization` is stripped on cross-scheme redirects (same host+port, different scheme).
Before the fix `crossOrigin` checked host+port only; a http→https redirect to the same
host+port would silently keep the credential header.
- Streaming (`.outgoing`) request bodies must not be retried on connection failure.
A channel-backed body is consumed on first use; retrying would send an empty body.
-/
private def runWithTimeout (name : String) (timeoutMs : Nat := 3000) (action : IO Unit) : IO Unit := do
let task ← IO.asTask action
let ticks := (timeoutMs + 9) / 10
let rec loop (remaining : Nat) : IO Unit := do
if (← IO.getTaskState task) == .finished then
match (← IO.wait task) with
| .ok x => pure x
| .error err => throw err
else
match remaining with
| 0 =>
IO.cancel task
throw <| IO.userError s!"Test '{name}' timed out after {timeoutMs}ms"
| n + 1 =>
IO.sleep 10
loop n
loop ticks
-- Build a raw HTTP/1.1 response byte string.
private def rawResp
(status : String) (hdrs : Array (String × String)) (body : String) : ByteArray :=
let hdrLines := hdrs.foldl (fun s (k, v) => s ++ s!"{k}: {v}\r\n") ""
s!"HTTP/1.1 {status}\r\n{hdrLines}\r\n{body}".toUTF8
-- ============================================================
-- Redirect: Authorization stripped on scheme-change redirect
-- ============================================================
-- A 302 redirect from http://example.com:443/ to https://example.com:443/r has the
-- same host and port but a different scheme. crossOrigin must be true so that the
-- Authorization header is stripped before the redirect request is sent.
-- ============================================================
#eval show IO _ from runWithTimeout "scheme-change strips Authorization" 3000 <| Async.block do
let (mockClient, mockServer) ← Mock.new
let session ← Client.Session.new mockServer (config := {})
let cookieJar ← Cookie.Jar.new
let some domain := URI.DomainName.ofString? "example.com"
| throw (IO.userError "DomainName parse failed")
-- Agent with scheme=http on port 443. Redirect target https://example.com:443/r
-- has same host+port but different scheme → crossOrigin must be true after the fix.
let agent : Client.Agent Mock.Server := {
session
scheme := URI.Scheme.ofString! "http"
host := .name domain
port := 443
cookieJar
}
let request ← Request.new
|>.method .get
|>.uri! "/"
|>.header! "Host" "example.com:443"
|>.header! "Authorization" "Bearer secret-token"
|>.blank
let resultPromise : IO.Promise (Except String (Response Body.Incoming)) ← IO.Promise.new
background do
let result : Except String (Response Body.Incoming) ← try
let resp ← Client.Agent.send agent request
pure (Except.ok resp)
catch e => pure (Except.error (toString e))
discard <| resultPromise.resolve result
-- First exchange: drain the request, reply with 302 redirecting to HTTPS same host+port.
let _ ← mockClient.recv?
mockClient.send (rawResp "302 Found"
#[("Location", "https://example.com:443/redirected"),
("Content-Length", "0"),
("Connection", "keep-alive")] "")
-- Second exchange: receive the redirected request and capture its bytes.
let some redirectBytes ← mockClient.recv?
| throw (IO.userError "Test failed: no redirect request received")
mockClient.send (rawResp "200 OK"
#[("Content-Length", "2"), ("Connection", "close")] "ok")
-- Wait for the agent to finish.
match ← await resultPromise.result! with
| Except.error e => throw (IO.userError s!"agent error: {e}")
| Except.ok _ => pure ()
let redirectText := String.fromUTF8! redirectBytes
if redirectText.contains "Authorization:" then
throw <| IO.userError
s!"Test 'scheme-change strips Authorization' FAILED: \
Authorization header present in redirect request\n{redirectText.quote}"
-- ============================================================
-- Redirect: Authorization preserved on same-origin redirect
-- ============================================================
-- A 302 redirect to the same scheme, host, and port is a same-origin redirect.
-- The Authorization header must NOT be stripped in this case.
-- ============================================================
#eval show IO _ from runWithTimeout "same-origin preserves Authorization" 3000 <| Async.block do
let (mockClient, mockServer) ← Mock.new
let session ← Client.Session.new mockServer (config := {})
let cookieJar ← Cookie.Jar.new
let some domain := URI.DomainName.ofString? "example.com"
| throw (IO.userError "DomainName parse failed")
let agent : Client.Agent Mock.Server := {
session
scheme := URI.Scheme.ofString! "http"
host := .name domain
port := 80
cookieJar
}
let request ← Request.new
|>.method .get
|>.uri! "/"
|>.header! "Host" "example.com"
|>.header! "Authorization" "Bearer secret-token"
|>.blank
let resultPromise : IO.Promise (Except String (Response Body.Incoming)) ← IO.Promise.new
background do
let result : Except String (Response Body.Incoming) ← try
let resp ← Client.Agent.send agent request
pure (Except.ok resp)
catch e => pure (Except.error (toString e))
discard <| resultPromise.resolve result
-- First exchange: reply with 302 to same scheme+host+port.
let _ ← mockClient.recv?
mockClient.send (rawResp "302 Found"
#[("Location", "http://example.com/same-origin"),
("Content-Length", "0"),
("Connection", "keep-alive")] "")
-- Second exchange: receive the redirected request.
let some redirectBytes ← mockClient.recv?
| throw (IO.userError "Test failed: no redirect request received")
mockClient.send (rawResp "200 OK"
#[("Content-Length", "2"), ("Connection", "close")] "ok")
match ← await resultPromise.result! with
| Except.error e => throw (IO.userError s!"agent error: {e}")
| Except.ok _ => pure ()
let redirectText := String.fromUTF8! redirectBytes
unless redirectText.contains "Authorization:" do
throw <| IO.userError
s!"Test 'same-origin preserves Authorization' FAILED: \
Authorization header was stripped on same-origin redirect\n{redirectText.quote}"
-- ============================================================
-- Body replay classification
-- ============================================================
-- Verifies that only `.outgoing` (channel-backed streaming) bodies are classified as
-- non-replayable, while `.full` (fixed bytes) and `.empty` bodies are safe to retry.
-- This mirrors the `bodyIsReplayable` check added to the retry guard in Agent.lean.
-- ============================================================
#eval show IO _ from Async.block do
-- .outgoing: channel is consumed on first send, must not be retried.
let (out, _) ← Body.mkChannel
let streamBody : Body.AnyBody := .outgoing out
let replayable := match streamBody with | .outgoing _ => false | _ => true
if replayable then
throw <| IO.userError "Test 'outgoing body is not replayable' FAILED"
-- .full: fixed ByteArray, safe to send again.
let fullBody : Body.AnyBody := .full (← Body.Full.ofByteArray "hello".toUTF8)
let replayable2 := match fullBody with | .outgoing _ => false | _ => true
unless replayable2 do
throw <| IO.userError "Test 'full body is replayable' FAILED"
-- .empty: trivially safe.
let emptyBody : Body.AnyBody := .empty {}
let replayable3 := match emptyBody with | .outgoing _ => false | _ => true
unless replayable3 do
throw <| IO.userError "Test 'empty body is replayable' FAILED"
-- ============================================================
-- Redirect: non-HTTP/HTTPS scheme in Location is not followed
-- ============================================================
-- A 302 response with Location: ftp://internal-host/secret must not be followed.
-- Before the fix, decideRedirect accepted any scheme that RequestTarget.parse? could
-- parse and would try to connect to the ftp host on port 80 (SSRF).
-- After the fix, only http:// and https:// redirect targets are followed; everything
-- else returns the 3xx response as-is.
-- ============================================================
#eval show IO _ from runWithTimeout "ftp:// redirect not followed" 3000 <| Async.block do
let (mockClient, mockServer) ← Mock.new
let session ← Client.Session.new mockServer (config := {})
let cookieJar ← Cookie.Jar.new
let some domain := URI.DomainName.ofString? "example.com"
| throw (IO.userError "DomainName parse failed")
let agent : Client.Agent Mock.Server := {
session
scheme := URI.Scheme.ofString! "http"
host := .name domain
port := 80
cookieJar
}
let request ← Request.new
|>.method .get
|>.uri! "/"
|>.header! "Host" "example.com"
|>.blank
let resultPromise : IO.Promise (Except String (Response Body.Incoming)) ← IO.Promise.new
background do
let result ← try
let resp ← Client.Agent.send agent request
pure (Except.ok resp)
catch e => pure (Except.error (toString e))
discard <| resultPromise.resolve result
-- Server replies with a redirect to ftp:// (non-HTTP scheme).
let _ ← mockClient.recv?
mockClient.send (rawResp "302 Found"
#[("Location", "ftp://internal-host/secret"),
("Content-Length", "0")] "")
match ← await resultPromise.result! with
| Except.error e => throw (IO.userError s!"agent error: {e}")
| Except.ok resp =>
-- The agent must return the 302 as-is, not follow it.
unless resp.line.status == .found do
throw <| IO.userError
s!"Test 'ftp:// redirect not followed' FAILED: expected 302, got {resp.line.status.toCode}"
#eval show IO _ from runWithTimeout "file:// redirect not followed" 3000 <| Async.block do
let (mockClient, mockServer) ← Mock.new
let session ← Client.Session.new mockServer (config := {})
let cookieJar ← Cookie.Jar.new
let some domain := URI.DomainName.ofString? "example.com"
| throw (IO.userError "DomainName parse failed")
let agent : Client.Agent Mock.Server := {
session
scheme := URI.Scheme.ofString! "http"
host := .name domain
port := 80
cookieJar
}
let request ← Request.new
|>.method .get
|>.uri! "/"
|>.header! "Host" "example.com"
|>.blank
let resultPromise : IO.Promise (Except String (Response Body.Incoming)) ← IO.Promise.new
background do
let result ← try
let resp ← Client.Agent.send agent request
pure (Except.ok resp)
catch e => pure (Except.error (toString e))
discard <| resultPromise.resolve result
let _ ← mockClient.recv?
mockClient.send (rawResp "301 Moved Permanently"
#[("Location", "file:///etc/passwd"),
("Content-Length", "0")] "")
match ← await resultPromise.result! with
| Except.error e => throw (IO.userError s!"agent error: {e}")
| Except.ok resp =>
unless resp.line.status == .movedPermanently do
throw <| IO.userError
s!"Test 'file:// redirect not followed' FAILED: expected 301, got {resp.line.status.toCode}"
-- ============================================================
-- Redirect: https:// redirect IS followed (sanity check)
-- ============================================================
-- Verify that the scheme restriction doesn't accidentally block legitimate
-- https:// redirects (same host, different scheme from http to https).
-- ============================================================
#eval show IO _ from runWithTimeout "https:// redirect is followed" 3000 <| Async.block do
let (mockClient, mockServer) ← Mock.new
let session ← Client.Session.new mockServer (config := {})
let cookieJar ← Cookie.Jar.new
let some domain := URI.DomainName.ofString? "example.com"
| throw (IO.userError "DomainName parse failed")
-- Agent with connectTo = none; cross-host redirects return the 3xx as-is.
-- We use the same-host case: http://example.com:80/target (same host+port, scheme changes).
let agent : Client.Agent Mock.Server := {
session
scheme := URI.Scheme.ofString! "http"
host := .name domain
port := 80
cookieJar
}
let request ← Request.new
|>.method .get
|>.uri! "/"
|>.header! "Host" "example.com"
|>.blank
let resultPromise : IO.Promise (Except String (Response Body.Incoming)) ← IO.Promise.new
background do
let result ← try
let resp ← Client.Agent.send agent request
pure (Except.ok resp)
catch e => pure (Except.error (toString e))
discard <| resultPromise.resolve result
-- 302 to https://example.com/page — same host+port, scheme differs from http.
-- No connectTo factory means cross-origin redirect returns 302 as-is, but at least
-- the scheme check must not block it before that point; the 302 must be attempted.
let _ ← mockClient.recv?
mockClient.send (rawResp "302 Found"
#[("Location", "https://example.com/page"),
("Content-Length", "0")] "")
-- For same-host https: the redirect IS attempted on the same session; serve 200.
let redirectReqOpt ← mockClient.recv?
if redirectReqOpt.isSome then
mockClient.send (rawResp "200 OK"
#[("Content-Length", "2"), ("Connection", "close")] "ok")
match ← await resultPromise.result! with
| Except.error e => throw (IO.userError s!"agent error: {e}")
| Except.ok resp =>
-- We accept either 302 (no connectTo for cross-host) or 200 (same-session follow).
let code := resp.line.status.toCode
unless code == 200 || code == 302 do
throw <| IO.userError
s!"Test 'https:// redirect is followed' FAILED: unexpected status {code}"
-- ============================================================
-- Redirect: streaming body dropped on method-preserving redirect
-- ============================================================
-- A 307 redirect preserves the original method and body. When the body is a
-- streaming channel (.outgoing) that has already been consumed by the first
-- request, it cannot be replayed. The redirect request must send no body
-- (Content-Length: 0) rather than silently retransmitting whatever bytes remain
-- in the channel (none, so it would be empty anyway — but the fix must explicitly
-- classify .outgoing as non-replayable so future semantics stay correct).
-- ============================================================
#eval show IO _ from runWithTimeout "streaming body dropped on 307 redirect" 3000 <| Async.block do
let (mockClient, mockServer) ← Mock.new
let session ← Client.Session.new mockServer (config := {})
let cookieJar ← Cookie.Jar.new
let some domain := URI.DomainName.ofString? "example.com"
| throw (IO.userError "DomainName parse failed")
let agent : Client.Agent Mock.Server := {
session
scheme := URI.Scheme.ofString! "http"
host := .name domain
port := 80
cookieJar
}
-- Build a PUT request with a streaming body.
let (bodyOut, bodyIn) ← Body.mkChannel
-- Write some payload and close the channel.
Body.Writer.send bodyOut { data := "payload".toUTF8 } false
Body.Writer.close bodyOut
let request ← Request.new
|>.method .put
|>.uri! "/upload"
|>.header! "Host" "example.com"
|>.stream (fun out => do
Body.Writer.send out { data := "payload".toUTF8 } false
Body.Writer.close out)
let resultPromise : IO.Promise (Except String (Response Body.Incoming)) ← IO.Promise.new
background do
let result ← try
let resp ← Client.Agent.send agent request
pure (Except.ok resp)
catch e => pure (Except.error (toString e))
discard <| resultPromise.resolve result
-- First request: drain it and reply with 307 (method-preserving redirect).
let some _firstBytes ← mockClient.recv?
| throw (IO.userError "Test failed: no first request received")
mockClient.send (rawResp "307 Temporary Redirect"
#[("Location", "/new-upload"),
("Content-Length", "0")] "")
-- Second request: the redirect. The streaming body is already consumed so
-- the client must send no body (Content-Length: 0 or absent, no body bytes).
let some redirectBytes ← mockClient.recv?
| throw (IO.userError "Test failed: no redirect request received")
mockClient.send (rawResp "200 OK"
#[("Content-Length", "2"), ("Connection", "close")] "ok")
match ← await resultPromise.result! with
| Except.error e => throw (IO.userError s!"agent error: {e}")
| Except.ok _ => pure ()
let redirectText := String.fromUTF8! redirectBytes
-- The redirect request must target /new-upload.
unless redirectText.contains "PUT /new-upload" do
throw <| IO.userError
s!"Test 'streaming body dropped on 307 redirect' FAILED: expected PUT /new-upload\n{redirectText.quote}"
-- The body must be empty: Content-Length 0 (or no body bytes after blank line).
-- We check that "payload" does not appear in the redirect request.
if redirectText.contains "payload" then
throw <| IO.userError
s!"Test 'streaming body dropped on 307 redirect' FAILED: \
streaming body payload present in redirect request\n{redirectText.quote}"
-- Discard the incoming body channel created during test setup.
Body.Reader.close bodyIn

255
tests/elab/async_http_cookie_parser.lean Normal file
View File

@@ -0,0 +1,255 @@
import Std.Internal.Http.Data.Cookie
open Std.Http
/-!
# Cookie Parser Tests
Tests for `Set-Cookie` header parsing following RFC 6265 §4.1.
-/
-- Helper: parse a Set-Cookie header value, throw on failure.
def parseCookie (s : String) : IO Cookie.Parser.Parsed :=
IO.ofExcept (Cookie.Parser.parseSetCookie.run s.toUTF8)
-- Helper: assert parsing fails.
def parseShouldFail (label : String) (s : String) : IO Unit := do
match Cookie.Parser.parseSetCookie.run s.toUTF8 with
| .ok _ => throw <| IO.userError s!"Test '{label}' failed: expected parse failure but succeeded"
| .error _ => pure ()
-- ============================================================================
-- Basic cookie-pair
-- ============================================================================
#eval show IO _ from do
-- Minimal name=value
let p ← parseCookie "foo=bar"
unless p.name == "foo" do
throw <| IO.userError s!"Test 'basic name' failed: expected 'foo', got {p.name.quote}"
unless p.value == "bar" do
throw <| IO.userError s!"Test 'basic value' failed: expected 'bar', got {p.value.quote}"
unless p.domain == none do
throw <| IO.userError s!"Test 'basic domain absent' failed: expected none, got {repr p.domain}"
unless p.path == none do
throw <| IO.userError s!"Test 'basic path absent' failed: expected none, got {repr p.path}"
unless p.secure == false do
throw <| IO.userError "Test 'basic secure absent' failed: expected false"
-- Empty value is allowed (cookie-value = *cookie-octet)
let pEmpty ← parseCookie "session="
unless pEmpty.value == "" do
throw <| IO.userError s!"Test 'empty value' failed: expected '', got {pEmpty.value.quote}"
-- Numeric name is not a valid token (digits alone are not all tchar? Actually digits ARE tchar)
-- tchar includes DIGIT, so "123" is a valid token
let pNum ← parseCookie "123=abc"
unless pNum.name == "123" do
throw <| IO.userError s!"Test 'numeric name' failed: expected '123', got {pNum.name.quote}"
-- ============================================================================
-- Quoted cookie values
-- ============================================================================
#eval show IO _ from do
-- Double-quoted value: quotes are stripped, inner value is returned
let p ← parseCookie "id=\"abc123\""
unless p.value == "abc123" do
throw <| IO.userError s!"Test 'quoted value' failed: expected 'abc123', got {p.value.quote}"
-- Empty quoted value
let pEq ← parseCookie "id=\"\""
unless pEq.value == "" do
throw <| IO.userError s!"Test 'empty quoted value' failed: expected '', got {pEq.value.quote}"
-- Quoted value with all valid cookie-octets (excluding DQUOTE, SP, comma, semicolon, backslash)
let pOctets ← parseCookie "t=\"!#$%&'*+-.^_`|~\""
unless pOctets.value == "!#$%&'*+-.^_`|~" do
throw <| IO.userError s!"Test 'quoted cookie-octets' failed: got {pOctets.value.quote}"
-- ============================================================================
-- Domain attribute
-- ============================================================================
#eval show IO _ from do
-- Domain present
let p ← parseCookie "x=y; Domain=example.com"
unless p.domain == some "example.com" do
throw <| IO.userError s!"Test 'domain' failed: expected some \"example.com\", got {repr p.domain}"
-- Leading dot is stripped per RFC 6265 §5.2.3
let pDot ← parseCookie "x=y; Domain=.example.com"
unless pDot.domain == some "example.com" do
throw <| IO.userError s!"Test 'domain leading dot stripped' failed: expected some \"example.com\", got {repr pDot.domain}"
-- Empty domain attribute → domain is none
let pEmpty ← parseCookie "x=y; Domain="
unless pEmpty.domain == none do
throw <| IO.userError s!"Test 'empty domain' failed: expected none, got {repr pEmpty.domain}"
-- Dot-only domain → stripped to empty → domain is none
let pDotOnly ← parseCookie "x=y; Domain=."
unless pDotOnly.domain == none do
throw <| IO.userError s!"Test 'dot-only domain' failed: expected none, got {repr pDotOnly.domain}"
-- ============================================================================
-- Path attribute
-- ============================================================================
#eval show IO _ from do
-- Valid path starting with /
let p ← parseCookie "x=y; Path=/foo/bar"
unless p.path == some "/foo/bar" do
throw <| IO.userError s!"Test 'path' failed: expected some \"/foo/bar\", got {repr p.path}"
-- Root path
let pRoot ← parseCookie "x=y; Path=/"
unless pRoot.path == some "/" do
throw <| IO.userError s!"Test 'root path' failed: expected some \"/\", got {repr pRoot.path}"
-- Path not starting with / → none per RFC 6265 §5.2.4
let pNoSlash ← parseCookie "x=y; Path=noslash"
unless pNoSlash.path == none do
throw <| IO.userError s!"Test 'path without leading slash' failed: expected none, got {repr pNoSlash.path}"
-- Empty path → none
let pEmpty ← parseCookie "x=y; Path="
unless pEmpty.path == none do
throw <| IO.userError s!"Test 'empty path' failed: expected none, got {repr pEmpty.path}"
-- ============================================================================
-- Secure attribute
-- ============================================================================
#eval show IO _ from do
-- Secure present
let p ← parseCookie "x=y; Secure"
unless p.secure == true do
throw <| IO.userError "Test 'secure' failed: expected true"
-- Secure absent
let pNo ← parseCookie "x=y"
unless pNo.secure == false do
throw <| IO.userError "Test 'secure absent' failed: expected false"
-- Secure= (with a value — treated as Secure since we match the attr name)
let pVal ← parseCookie "x=y; Secure=true"
unless pVal.secure == true do
throw <| IO.userError "Test 'secure with value' failed: expected true"
-- ============================================================================
-- Combined attributes
-- ============================================================================
#eval show IO _ from do
let p ← parseCookie "sessionId=abc123; Domain=example.com; Path=/app; Secure"
unless p.name == "sessionId" do
throw <| IO.userError s!"Test 'combined name' failed: got {p.name.quote}"
unless p.value == "abc123" do
throw <| IO.userError s!"Test 'combined value' failed: got {p.value.quote}"
unless p.domain == some "example.com" do
throw <| IO.userError s!"Test 'combined domain' failed: got {repr p.domain}"
unless p.path == some "/app" do
throw <| IO.userError s!"Test 'combined path' failed: got {repr p.path}"
unless p.secure == true do
throw <| IO.userError "Test 'combined secure' failed: expected true"
-- ============================================================================
-- Case-insensitive attribute names (RFC 6265 §5.2)
-- ============================================================================
#eval show IO _ from do
-- Uppercase attribute names must be recognized
let p ← parseCookie "x=y; DOMAIN=example.com; PATH=/; SECURE"
unless p.domain == some "example.com" do
throw <| IO.userError s!"Test 'uppercase domain' failed: got {repr p.domain}"
unless p.path == some "/" do
throw <| IO.userError s!"Test 'uppercase path' failed: got {repr p.path}"
unless p.secure == true do
throw <| IO.userError "Test 'uppercase secure' failed: expected true"
-- Mixed-case attribute names
let pMixed ← parseCookie "x=y; Domain=a.com; Secure; Path=/x"
unless pMixed.domain == some "a.com" do
throw <| IO.userError s!"Test 'mixed-case domain' failed: got {repr pMixed.domain}"
unless pMixed.secure == true do
throw <| IO.userError "Test 'mixed-case secure' failed: expected true"
unless pMixed.path == some "/x" do
throw <| IO.userError s!"Test 'mixed-case path' failed: got {repr pMixed.path}"
-- ============================================================================
-- Unknown attributes are silently ignored
-- ============================================================================
#eval show IO _ from do
-- HttpOnly is silently ignored
let p ← parseCookie "x=y; HttpOnly"
unless p.name == "x" && p.value == "y" do
throw <| IO.userError s!"Test 'HttpOnly ignored' failed: name={p.name.quote} value={p.value.quote}"
-- Expires is silently ignored
let pExp ← parseCookie "x=y; Expires=Thu, 01 Jan 2026 00:00:00 GMT"
unless pExp.name == "x" && pExp.value == "y" do
throw <| IO.userError s!"Test 'Expires ignored' failed"
-- SameSite is silently ignored
let pSS ← parseCookie "x=y; SameSite=Strict"
unless pSS.name == "x" && pSS.value == "y" do
throw <| IO.userError s!"Test 'SameSite ignored' failed"
-- Max-Age is silently ignored
let pMaxAge ← parseCookie "x=y; Max-Age=3600"
unless pMaxAge.name == "x" && pMaxAge.value == "y" do
throw <| IO.userError s!"Test 'Max-Age ignored' failed"
-- Multiple unknown attributes
let pMulti ← parseCookie "x=y; Foo=bar; HttpOnly; Baz; Path=/p"
unless pMulti.path == some "/p" do
throw <| IO.userError s!"Test 'unknown attrs + path' failed: got {repr pMulti.path}"
-- ============================================================================
-- Duplicate attribute handling (last-write-wins is fine, RFC 6265 §5.3)
-- ============================================================================
#eval show IO _ from do
-- Last Domain wins
let p ← parseCookie "x=y; Domain=first.com; Domain=second.com"
unless p.domain == some "second.com" do
throw <| IO.userError s!"Test 'duplicate domain last wins' failed: got {repr p.domain}"
-- Last Path wins
let pPath ← parseCookie "x=y; Path=/first; Path=/second"
unless pPath.path == some "/second" do
throw <| IO.userError s!"Test 'duplicate path last wins' failed: got {repr pPath.path}"
-- ============================================================================
-- Semicolon spacing: RFC 6265 §4.1 allows optional SP after ";"
-- ============================================================================
#eval show IO _ from do
-- No space after semicolon
let pNoSp ← parseCookie "x=y;Secure"
unless pNoSp.secure == true do
throw <| IO.userError "Test 'no space after semicolon' failed: expected Secure=true"
-- Space after semicolon (standard)
let pSp ← parseCookie "x=y; Secure"
unless pSp.secure == true do
throw <| IO.userError "Test 'space after semicolon' failed: expected Secure=true"
-- ============================================================================
-- Invalid cookie names → parse failure
-- ============================================================================
#eval show IO _ from do
-- Empty name is not a valid token (token = 1*tchar, requires at least one char)
parseShouldFail "empty name" "=value"
-- Space in name (space is not a tchar)
parseShouldFail "space in name" "foo bar=value"
-- Semicolon in name (not a tchar)
parseShouldFail "semicolon in name" "foo;bar=value"
-- Missing '=' separator
parseShouldFail "missing equals" "nameonly"