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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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.

@[inline]

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

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

@[inline]

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

Checks if the writer has completed processing a request.

@[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.

@[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.

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.

@[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.

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.

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.

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.

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.

@[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.

@[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.

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.

@[inline]

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

Closes the writer, transitioning to the closed state.