HTTP/1.1 Writer

This module defines the writer state machine for generating outgoing HTTP/1.1 messages. It handles encoding headers and body content for both fixed-length and chunked transfer encodings.

inductive Std.Http.Protocol.H1.Writer.State : Type

The state of the Writer state machine.

• pending : State

  Initial state before any outgoing message has been prepared.

• waitingHeaders : State

  Waiting for the application to provide the outgoing message head via send.

• waitingForFlush : State

  The message head has been provided; waiting for shouldFlush to become true before serializing headers to output.

• writingBodyFixed (n : Nat) : State

  Writing a fixed-length body; n is the number of bytes still to be sent.

• writingBodyChunked : State

  Writing a chunked transfer-encoding body (HTTP/1.1).

• writingBodyClosingFrame : State

  Writing a connection-close body (HTTP/1.0 server, unknown length). Raw bytes are written without chunk framing; the peer reads until the connection closes.

• complete : State

  Completed writing a single message and ready to begin the next one.

• closed : State

  Closed; no further data can be written.

@[implicit_reducible]

instance Std.Http.Protocol.H1.Writer.instInhabitedState : Inhabited State

Equations

• Std.Http.Protocol.H1.Writer.instInhabitedState = { default := Std.Http.Protocol.H1.Writer.instInhabitedState.default }

def Std.Http.Protocol.H1.Writer.instReprState.repr : State → Nat → Format

Equations

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

@[implicit_reducible]

instance Std.Http.Protocol.H1.Writer.instReprState : Repr State

Equations

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

@[implicit_reducible]

instance Std.Http.Protocol.H1.Writer.instBEqState : BEq State

Equations

• Std.Http.Protocol.H1.Writer.instBEqState = { beq := Std.Http.Protocol.H1.Writer.instBEqState.beq }

def Std.Http.Protocol.H1.Writer.instBEqState.beq : State → State → Bool

Equations

• Std.Http.Protocol.H1.Writer.instBEqState.beq Std.Http.Protocol.H1.Writer.State.pending Std.Http.Protocol.H1.Writer.State.pending = true
• Std.Http.Protocol.H1.Writer.instBEqState.beq Std.Http.Protocol.H1.Writer.State.waitingHeaders Std.Http.Protocol.H1.Writer.State.waitingHeaders = true
• Std.Http.Protocol.H1.Writer.instBEqState.beq Std.Http.Protocol.H1.Writer.State.waitingForFlush Std.Http.Protocol.H1.Writer.State.waitingForFlush = true
• Std.Http.Protocol.H1.Writer.instBEqState.beq (Std.Http.Protocol.H1.Writer.State.writingBodyFixed a) (Std.Http.Protocol.H1.Writer.State.writingBodyFixed b) = (a == b)
• Std.Http.Protocol.H1.Writer.instBEqState.beq Std.Http.Protocol.H1.Writer.State.writingBodyChunked Std.Http.Protocol.H1.Writer.State.writingBodyChunked = true
• Std.Http.Protocol.H1.Writer.instBEqState.beq Std.Http.Protocol.H1.Writer.State.writingBodyClosingFrame Std.Http.Protocol.H1.Writer.State.writingBodyClosingFrame = true
• Std.Http.Protocol.H1.Writer.instBEqState.beq Std.Http.Protocol.H1.Writer.State.complete Std.Http.Protocol.H1.Writer.State.complete = true
• Std.Http.Protocol.H1.Writer.instBEqState.beq Std.Http.Protocol.H1.Writer.State.closed Std.Http.Protocol.H1.Writer.State.closed = true
• Std.Http.Protocol.H1.Writer.instBEqState.beq x✝¹ x✝ = false

structure Std.Http.Protocol.H1.Writer (dir : Direction) : Type

Manages the writing state of the HTTP generating and writing machine.

• userData : Array Chunk

  Body chunks supplied by the user, accumulated before being flushed to output.

• outputData : Internal.ChunkedBuffer

  All the data produced by the writer, ready to be sent to the socket.

• state : State

  The state of the writer machine.

• knownSize : Option Body.Length

  When the user specifies the exact body size upfront, Content-Length framing is used instead of chunked transfer encoding.

• messageHead : Message.Head dir.swap

  The outgoing message that will be written to the output.

• sentMessage : Bool

  Whether the user has called send to provide the outgoing message head.

• userClosedBody : Bool

  Set when the user has finished sending body data, allowing fixed-size framing to be determined upfront.

• omitBody : Bool

  When true, body bytes are intentionally omitted from the wire for this message (e.g. HEAD responses), while headers/framing metadata may still describe the hypothetical representation.

• userDataBytes : Nat

  Running total of bytes across all userData chunks, maintained incrementally to avoid an O(n) fold on every fixed-length write step.

@[inline]

def Std.Http.Protocol.H1.Writer.noMoreUserData {dir : Direction} (writer : Writer dir) : Bool

Returns true when no more user body data will arrive: either the user called closeBody, or the writer has already transitioned to complete or closed.

Note: this does not mean the wire is ready to accept new bytes — a closed writer cannot send anything. Use this to decide whether to flush pending body data rather than to check writability.

Equations

• writer.noMoreUserData = match writer.state with | Std.Http.Protocol.H1.Writer.State.closed => true | Std.Http.Protocol.H1.Writer.State.complete => true | x => writer.userClosedBody

@[inline]

def Std.Http.Protocol.H1.Writer.isClosed {dir : Direction} (writer : Writer dir) : Bool

Checks if the writer is closed (cannot process more data).

Equations

• writer.isClosed = match writer.state with | Std.Http.Protocol.H1.Writer.State.closed => true | x => false

@[inline]

def Std.Http.Protocol.H1.Writer.isComplete {dir : Direction} (writer : Writer dir) : Bool

Checks if the writer has completed processing a request.

Equations

• writer.isComplete = match writer.state with | Std.Http.Protocol.H1.Writer.State.complete => true | x => false

@[inline]

def Std.Http.Protocol.H1.Writer.canAcceptData {dir : Direction} (writer : Writer dir) : Bool

Checks if the writer can accept more data from the user.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Writer.closeBody {dir : Direction} (writer : Writer dir) : Writer dir

Marks the body as closed, indicating no more user data will be added.

Equations

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

def Std.Http.Protocol.H1.Writer.determineTransferMode {dir : Direction} (writer : Writer dir) : Body.Length

Determines the transfer encoding mode based on explicit setting, body closure state, or defaults to chunked.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Writer.addUserData {dir : Direction} (data : Array Chunk) (writer : Writer dir) : Writer dir

Adds user data chunks to the writer's buffer if the writer can accept data.

Empty chunks (zero bytes of data) are accepted here but will be silently dropped during the chunked-encoding write step — see writeChunkedBody.

Equations

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

def Std.Http.Protocol.H1.Writer.writeFixedBody {dir : Direction} (writer : Writer dir) (limitSize : Nat) : Writer dir × Nat

Writes accumulated user data to output using fixed-size encoding.

Equations

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

def Std.Http.Protocol.H1.Writer.writeChunkedBody {dir : Direction} (writer : Writer dir) : Writer dir

Writes accumulated user data to output using chunked transfer encoding.

Empty chunks are silently discarded. See Chunk.empty for the protocol-level rationale.

Equations

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

def Std.Http.Protocol.H1.Writer.writeFinalChunk {dir : Direction} (writer : Writer dir) : Writer dir

Writes the final chunk terminator (0\r\n\r\n) and transitions to complete state.

Equations

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

def Std.Http.Protocol.H1.Writer.writeRawBody {dir : Direction} (writer : Writer dir) : Writer dir

Writes accumulated user data to output as raw bytes (HTTP/1.0 connection-close framing). No chunk framing is added; the peer reads until the connection closes.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Writer.takeOutput {dir : Direction} (writer : Writer dir) : Option (Writer dir × ByteArray)

Extracts all accumulated output data and returns it with a cleared output buffer.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Writer.setState {dir : Direction} (state : State) (writer : Writer dir) : Writer dir

Updates the writer's state machine to a new state.

Equations

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

def Std.Http.Protocol.H1.Writer.shouldKeepAlive {dir : Direction} (writer : Writer dir) : Bool

Checks if the connection should be kept alive based on the Connection header.

Equations

• writer.shouldKeepAlive = (Option.map (fun (v : Std.Http.Header.Value) => v.value.toLower != "close") (writer.messageHead.headers.get? Std.Http.Header.Name.connection)).getD true

@[inline]

def Std.Http.Protocol.H1.Writer.close {dir : Direction} (writer : Writer dir) : Writer dir

Closes the writer, transitioning to the closed state.

Equations

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