def Network.Wai.Handler.Warp.maxHeaders : Nat

Maximum number of headers per request. Requests with more headers are rejected to prevent denial-of-service.

Equations

• Network.Wai.Handler.Warp.maxHeaders = 100

def Network.Wai.Handler.Warp.parseHttpVersion (s : String) : Option HTTP.Types.HttpVersion

Parse an HTTP version string like "HTTP/1.1". $$\text{parseHttpVersion} : \text{String} \to \text{Option}(\text{HttpVersion})$$

Equations

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

theorem Network.Wai.Handler.Warp.parseHttpVersion_http11 : parseHttpVersion "HTTP/1.1" = some HTTP.Types.http11

theorem Network.Wai.Handler.Warp.parseHttpVersion_http10 : parseHttpVersion "HTTP/1.0" = some HTTP.Types.http10

theorem Network.Wai.Handler.Warp.parseHttpVersion_http09 : parseHttpVersion "HTTP/0.9" = some HTTP.Types.http09

theorem Network.Wai.Handler.Warp.parseHttpVersion_http20 : parseHttpVersion "HTTP/2.0" = some HTTP.Types.http20

def Network.Wai.Handler.Warp.parseRequestLine (line : String) : Option (HTTP.Types.Method × String × String × HTTP.Types.HttpVersion)

Parse a request line like "GET /path?query HTTP/1.1". Returns (method, rawPath, rawQuery, version) or none if malformed. $$\text{parseRequestLine} : \text{String} \to \text{Option}(\text{Method} \times \text{String} \times \text{String} \times \text{HttpVersion})$$

Equations

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

theorem Network.Wai.Handler.Warp.parseRequestLine_empty : parseRequestLine "" = none

def Network.Wai.Handler.Warp.parseHeaderLine (line : String) : Option HTTP.Types.Header

Parse a single header line like "Content-Type: text/html". Returns none if the line doesn't contain a colon. $$\text{parseHeaderLine} : \text{String} \to \text{Option}(\text{Header})$$

Equations

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

def Network.Wai.Handler.Warp.parseHeaders (lines : List String) : HTTP.Types.RequestHeaders

Parse header lines into a list of headers. $$\text{parseHeaders} : \text{List}(\text{String}) \to \text{RequestHeaders}$$

Equations

• Network.Wai.Handler.Warp.parseHeaders lines = List.filterMap Network.Wai.Handler.Warp.parseHeaderLine lines

def Network.Wai.Handler.Warp.recvHeaders (buf : Socket.FFI.RecvBuffer) : IO (String × List String)

Read all header lines from a buffered reader until an empty line. Returns the request line and header lines. Uses O(1) cons + single reverse instead of O(n) append. Bounded by maxHeaders to prevent DoS. $$\text{recvHeaders} : \text{RecvBuffer} \to \text{IO}(\text{String} \times \text{List}(\text{String}))$$

Equations

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

axiom Network.Wai.Handler.Warp.recvHeaders_bounded (buf : Socket.FFI.RecvBuffer) (rl : String) (hdrs : List String) : recvHeaders buf = pure (rl, hdrs) → hdrs.length ≤ maxHeaders

Header count bound: The header count returned by recvHeaders is bounded by maxHeaders. The while loop checks count >= maxHeaders before each cons, ensuring at most maxHeaders elements are added. Axiom-dependent on IO monad execution semantics — the loop guard is checked before each FFI.recvBufReadLine call, but the proof cannot be discharged because recvHeaders uses do-notation over IO with mutable state (let mut), which is opaque to the kernel. $$\forall\, \text{rl}\; \text{hdrs},\; \text{recvHeaders}(\text{buf}) = \text{pure}(\text{rl}, \text{hdrs}) \implies \text{hdrs.length} \leq \text{maxHeaders}$$

def Network.Wai.Handler.Warp.parseRequest (buf : Socket.FFI.RecvBuffer) (remoteAddr : Socket.SockAddr) : IO (Option Request)

Parse a full HTTP request from a buffered reader. Returns none if the request line is malformed or the connection is closed. $$\text{parseRequest} : \text{RecvBuffer} \to \text{SockAddr} \to \text{IO}(\text{Option}(\text{Request}))$$

Equations

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