HTTP/1.1 Protocol State Machine

This module implements the core HTTP/1.1 protocol state machine that handles parsing requests/responses and generating output. The machine is direction-aware, supporting both server mode (receiving requests) and client mode (receiving responses).

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

Results from a single step of the state machine.

• events : Array (Event dir)

  Events that occurred during this step (e.g., headers received, control flow, errors).

• output : Internal.ChunkedBuffer

  Output data ready to be sent to the socket.

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

A single body chunk produced by a pull-driven read.

• final : Bool

  Whether this chunk finishes the current body stream.

• incomplete : Bool

  Whether the chunk data is partial for the current frame/body slice (more bytes are still required to complete it).

• chunk : Chunk

  The pulled body chunk.

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

The HTTP/1.1 protocol state machine.

• reader : Reader dir

  The state of the reader.

• writer : Writer dir

  The state of the writer.

• config : Config

  The configuration.

• events : Array (Event dir)

  Events that happened during reading and writing.

• error : Option Error

  Error thrown by the machine.

• instant : Option (Time.DateTime Time.TimeZone.UTC)

  The timestamp for the Date header.

• keepAlive : Bool

  If the connection will be kept alive after the message.

• forcedFlush : Bool

  Whether a forced flush has been requested by the user.

• pullBodyStalled : Bool

  Set when a previous pullBody call could not make progress in .readBody. Cleared on new input or state reset.

@[inline]

def Std.Http.Protocol.H1.Machine.failed {dir : Direction} (machine : Machine dir) : Bool

Returns true if the reader is in a failed state.

Equations

• machine.failed = match machine.reader.state with | Std.Http.Protocol.H1.Reader.State.failed error => true | x => false

@[inline]

def Std.Http.Protocol.H1.Machine.isReaderComplete {dir : Direction} (machine : Machine dir) : Bool

Returns true if the reader has completed successfully.

Equations

• machine.isReaderComplete = match machine.reader.state with | Std.Http.Protocol.H1.Reader.State.complete => true | x => false

@[inline]

def Std.Http.Protocol.H1.Machine.isReaderClosed {dir : Direction} (machine : Machine dir) : Bool

Returns true if the reader is closed.

Equations

• machine.isReaderClosed = match machine.reader.state with | Std.Http.Protocol.H1.Reader.State.closed => true | x => false

@[inline]

def Std.Http.Protocol.H1.Machine.isReaderAwaitingContinue {dir : Direction} (machine : Machine dir) : Bool

Returns true when the reader is paused waiting for a canContinue decision (server-side only; always false on the client side).

Equations

• machine_2.isReaderAwaitingContinue = true
• machine.isReaderAwaitingContinue = false

@[inline]

def Std.Http.Protocol.H1.Machine.shouldFlush {dir : Direction} (machine : Machine dir) : Bool

Returns true if the machine should flush buffered output.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Machine.isWaitingMessage {dir : Direction} (machine : Machine dir) : Bool

Returns true if the writer is waiting for headers of a new message.

Equations

• machine.isWaitingMessage = decide ((machine.writer.state == Std.Http.Protocol.H1.Writer.State.waitingHeaders) = true ∧ ¬machine.writer.sentMessage = true)

@[inline]

def Std.Http.Protocol.H1.Machine.halted {dir : Direction} (machine : Machine dir) : Bool

Returns true if both reader and writer are closed and no output remains.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Machine.canPullBody {dir : Direction} (machine : Machine dir) : Bool

Returns true when pullBody can attempt to produce body data immediately.

Equations

• machine.canPullBody = (!Std.Http.Protocol.H1.Machine.drainBodyInternally✝ machine && match machine.reader.state with | Std.Http.Protocol.H1.Reader.State.readBody a => true | x => false)

@[inline]

def Std.Http.Protocol.H1.Machine.canPullBodyNow {dir : Direction} (machine : Machine dir) : Bool

Returns true when pullBody is currently expected to make progress.

Equations

• machine.canPullBodyNow = (machine.canPullBody && !machine.pullBodyStalled)

@[inline]

def Std.Http.Protocol.H1.Machine.feed {dir : Direction} (machine : Machine dir) (data : ByteArray) : Machine dir

Feeds input bytes into the reader side of the machine.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Machine.closeReader {dir : Direction} (machine : Machine dir) : Machine dir

Signals EOF on the reader's input without changing the reader state. Used internally for flow control (e.g., after rejecting Expect: 100-continue). To also transition the reader to .closed, follow this with setReaderState .closed.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Machine.closeWriter {dir : Direction} (machine : Machine dir) : Machine dir

Closes the writer side, preventing any further message output.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Machine.userClosedBody {dir : Direction} (machine : Machine dir) : Machine dir

Signals that the user is not sending data anymore.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Machine.noMoreInput {dir : Direction} (machine : Machine dir) : Machine dir

Signals that the socket is not sending data anymore.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Machine.setKnownSize {dir : Direction} (machine : Machine dir) (size : Body.Length) : Machine dir

Set a known size for the message body, replacing any previous value.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Machine.suppressOutgoingBody {dir : Direction} (machine : Machine dir) (forceZero : Bool := false) : Machine dir

Suppresses writing body bytes for the current outgoing message while keeping header generation active. Used for responses that must not carry payload bytes.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Machine.send {dir : Direction} (machine : Machine dir) (message : Message.Head dir.swap) : Machine dir

Send the head of a message to the machine.

Must only be called when machine.isWaitingMessage is true. If called in any other state (e.g. called twice), the machine panics.

Informational (1xx) responses are written directly to the output buffer; the writer stays in waitingHeaders so the application can send additional interim responses or the final response. The reader state is not affected — use canContinue to resolve an Expect: 100-continue decision separately.

Equations

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

def Std.Http.Protocol.H1.Machine.canContinue {dir : Direction} (machine : Machine dir) (status : Status) : Machine dir

Resolves an Expect: 100-continue decision.

When status is 100 Continue, sends the interim response and advances to body reading. For any other status, sends the rejection response (typically 417), disables keep-alive, and closes the reader — the body will not be received.

Equations

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

def Std.Http.Protocol.H1.Machine.closeWithError (machine : Machine Direction.receiving) (status : Status) : Machine Direction.receiving

Sends an error response with Connection: close and shuts down input.

If the machine is waiting to send a message, sends status with a Connection: close header and signals that the body is done (letting the step function encode and flush the response), then stops accepting further input. Otherwise, closes the writer directly and stops accepting further input.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Machine.sendData {dir : Direction} (machine : Machine dir) (data : Array Chunk) : Machine dir

Enqueues body chunks into the writer buffer for encoding and sending.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Machine.takeEvents {dir : Direction} (machine : Machine dir) : Machine dir × Array (Event dir)

Takes and clears all accumulated events, returning the drained array.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Machine.takeOutput {dir : Direction} (machine : Machine dir) : Machine dir × Internal.ChunkedBuffer

Takes and clears accumulated output bytes, returning them as a buffer.

Equations

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

partial def Std.Http.Protocol.H1.Machine.processWrite {dir : Direction} (machine : Machine dir) : Machine dir

Advances writer-side state machine by one logical transition.

Depending on writer state, this may:

• request an application answer,
• serialize headers,
• flush fixed/chunked body bytes,
• finalize/close after completion.

partial def Std.Http.Protocol.H1.Machine.processRead {dir : Direction} (machine : Machine dir) : Machine dir

Advances reader-side state machine by one logical transition.

Dispatches parsing work according to current reader state (start-line, headers, body, completion, or failure handling).

def Std.Http.Protocol.H1.Machine.step {dir : Direction} (machine : Machine dir) : Machine dir × StepResult dir

Execute one step of the state machine.

Equations

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

@[inline]

def Std.Http.Protocol.H1.Machine.pullBody {dir : Direction} (machine : Machine dir) : Machine dir × Option PulledChunk

Pulls at most one body chunk from the reader.

It advances body parsing until it either:

• produces a chunk (some PulledChunk), or
• cannot continue for now (none).

Equations

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