Redirect planning

Pure HTTP redirect-decision logic.

decideRedirect inspects a response-line Status and Location header and produces a RedirectOutcome describing whether to stop or follow, plus the full rewrite required by RFC 9110 §15.4 (Redirect 3xx) and RFC 9112 §3.2 (Request Target).

This module never touches IO or Async.

References:

• https://httpwg.org/specs/rfc9110.html#status.3xx
• https://httpwg.org/specs/rfc9112.html#section-3.2

inductive Std.Http.Protocol.H1.RedirectBodyAction : Type

What the caller must do with the body of the original request when following a redirect.

• empty : RedirectBodyAction

  Send an empty body on the redirected request. Chosen when the method changes (303 See Other, or 301/302 on POST) or when the original body cannot be replayed.

• replay : RedirectBodyAction

  Reset the original body and resend it on the redirected request. Chosen for method-preserving redirects (307/308) when the body is marked replayable.

@[instance_reducible]

instance Std.Http.Protocol.H1.instDecidableEqRedirectBodyAction : DecidableEq RedirectBodyAction

Equations

• Std.Http.Protocol.H1.instDecidableEqRedirectBodyAction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Std.Http.Protocol.H1.instReprRedirectBodyAction : Repr RedirectBodyAction

Equations

• Std.Http.Protocol.H1.instReprRedirectBodyAction = { reprPrec := Std.Http.Protocol.H1.instReprRedirectBodyAction.repr }

def Std.Http.Protocol.H1.instReprRedirectBodyAction.repr : RedirectBodyAction → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Std.Http.Protocol.H1.instInhabitedRedirectBodyAction : Inhabited RedirectBodyAction

Equations

• Std.Http.Protocol.H1.instInhabitedRedirectBodyAction = { default := Std.Http.Protocol.H1.instInhabitedRedirectBodyAction.default }

structure Std.Http.Protocol.H1.RedirectPlan : Type

The concrete work the caller must perform to follow a redirect.

• origin : URI.Origin

  Target origin (scheme, host, port) for the redirected request.

• target : RequestTarget

  Rewritten request target put on the wire: origin-form for same-origin redirects, absolute-form for cross-origin redirects, with any userinfo stripped per RFC 9110 §4.2.4.

• method : Method

  Method to use for the redirected request (possibly downgraded to GET for 301/302 on POST or for 303).

• headers : Headers

  Headers for the redirected request after cross-origin and method-change scrubbing.

• bodyAction : RedirectBodyAction

  What to do with the original request body.

• isCrossOrigin : Bool

  Whether the redirect crosses origin boundaries (different host, port, or scheme). Useful for credential-handling decisions at the call site.

def Std.Http.Protocol.H1.instReprRedirectPlan.repr : RedirectPlan → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Std.Http.Protocol.H1.instReprRedirectPlan : Repr RedirectPlan

Equations

• Std.Http.Protocol.H1.instReprRedirectPlan = { reprPrec := Std.Http.Protocol.H1.instReprRedirectPlan.repr }

inductive Std.Http.Protocol.H1.RedirectOutcome : Type

Result of evaluating whether to follow a redirect.

• done : RedirectOutcome

  Response is final. Stop redirecting and return it.

• follow (plan : RedirectPlan) : RedirectOutcome

  Follow the redirect described by plan.

@[instance_reducible]

instance Std.Http.Protocol.H1.instInhabitedRedirectOutcome : Inhabited RedirectOutcome

Equations

• Std.Http.Protocol.H1.instInhabitedRedirectOutcome = { default := Std.Http.Protocol.H1.instInhabitedRedirectOutcome.default }

def Std.Http.Protocol.H1.decideRedirect (current : URI.Origin) (request : Request.Head) (bodyReplayable onlySafeRedirects : Bool) (responseVersion : Version) (status : Status) (responseHeaders : Headers) : RedirectOutcome

Decides whether to follow a redirect given the server's response-line status, version, and headers, the pending request, and whether the request body is replayable.

Returns .done when:

• the status is not a 3xx redirection,
• the response is HTTP/1.0 and the status code is not 301 or 302 (the only redirect codes defined by RFC 2616),
• no Location header is present,
• the Location value does not parse as a URI-reference (RFC 9110 §10.2.2),
• the target resolves to a non-http(s) scheme (SSRF guard), or
• onlySafeRedirects is true and the original method is not safe (RFC 9110 §9.2.1: GET, HEAD, OPTIONS, TRACE).

Returns .follow plan otherwise. The caller is expected to drain the redirect response body and, when plan.bodyAction == .replay, reset the original body before dispatching the rewritten request. On a cross-origin hop the original Host header is rewritten to the new origin, but only when one was present; if the original request carried no Host, supplying one for the new origin is the caller's responsibility.

Notes on specific status codes that always return .done:

• 300 Multiple Choices — may carry a Location naming the server's preferred choice, but RFC 9110 §15.4.1 leaves the selection to the user agent, so we deliberately do not auto-select.
• 304 Not Modified — cache revalidation result, not a navigation redirect.
• 305 Use Proxy — deprecated (RFC 9110 §15.4.6); blocked for security.
• 306 — reserved/unused.

Equations

• One or more equations did not get rendered due to their size.