HTTP/1.1 Reader

This module defines the reader state machine for parsing incoming HTTP/1.1 messages. It tracks the parsing state including start line, headers, and body handling for both fixed-length and chunked transfer encodings.

inductive Std.Http.Protocol.H1.Reader.BodyState : Type

The body-framing sub-state of the Reader state machine.

• fixed (remaining : Nat) : BodyState

  Parse fixed-length body bytes, tracking the number of bytes remaining.

• chunkedSize : BodyState

  Parse the next chunk-size line in chunked transfer encoding.

• chunkedBody (ext : Array (Chunk.ExtensionName × Option Chunk.ExtensionValue)) (remaining : Nat) : BodyState

  Parse chunk data for the current chunk.

• closeDelimited : BodyState

  Parse body bytes until EOF (connection close).

@[implicit_reducible]

instance Std.Http.Protocol.H1.Reader.instInhabitedBodyState : Inhabited BodyState

@[implicit_reducible]

instance Std.Http.Protocol.H1.Reader.instReprBodyState : Repr BodyState

def Std.Http.Protocol.H1.Reader.instReprBodyState.repr : BodyState → Nat → Format

@[implicit_reducible]

instance Std.Http.Protocol.H1.Reader.instBEqBodyState : BEq BodyState

def Std.Http.Protocol.H1.Reader.instBEqBodyState.beq : BodyState → BodyState → Bool

inductive Std.Http.Protocol.H1.Reader.State (dir : Direction) : Type

The state of the Reader state machine.

• needStartLine {dir : Direction} : State dir

  Initial state waiting for HTTP start line.

• needHeader {dir : Direction} : Nat → State dir

  State waiting for HTTP headers, tracking number of headers parsed.

• readBody {dir : Direction} : BodyState → State dir

  Unified body-reading state.

• continue {dir : Direction} : State dir → State dir

  Paused waiting for a canContinue decision, carrying the next state.

• pending {dir : Direction} : State dir

  State waiting to be able to read new data.

• complete {dir : Direction} : State dir

  State that it completed a single request or response and can go to the next one

• closed {dir : Direction} : State dir

  State that it has completed and cannot process more data.

• failed {dir : Direction} (error : Error) : State dir

  The input is malformed.

@[implicit_reducible]

instance Std.Http.Protocol.H1.Reader.instInhabitedState {a✝ : Direction} : Inhabited (State a✝)

def Std.Http.Protocol.H1.Reader.instReprState.repr {dir✝ : Direction} : State dir✝ → Nat → Format

@[implicit_reducible]

instance Std.Http.Protocol.H1.Reader.instReprState {dir✝ : Direction} : Repr (State dir✝)

def Std.Http.Protocol.H1.Reader.instBEqState.beq {dir✝ : Direction} : State dir✝ → State dir✝ → Bool

@[implicit_reducible]

instance Std.Http.Protocol.H1.Reader.instBEqState {dir✝ : Direction} : BEq (State dir✝)

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

Manages the reading state of the HTTP parsing and processing machine.

• state : State dir

  The current state of the machine.

• input : ByteArray.Iterator

  The input byte array.

• messageHead : Message.Head dir

  The incoming message head.

• messageCount : Nat

  Count of messages that this connection has already parsed.

• bodyBytesRead : Nat

  Number of body bytes read for the current message.

• headerBytesRead : Nat

  Number of header bytes accumulated for the current message. Counts name + value bytes plus 4 bytes per line for : and \r\n.

• noMoreInput : Bool

  Set when no further input bytes will arrive (the remote end has closed the connection).

@[inline]

def Std.Http.Protocol.H1.Reader.isClosed {dir : Direction} (reader : Reader dir) : Bool

Checks if the reader is in a closed state and cannot process more messages.

@[inline]

def Std.Http.Protocol.H1.Reader.isComplete {dir : Direction} (reader : Reader dir) : Bool

Checks if the reader has completed parsing the current message.

@[inline]

def Std.Http.Protocol.H1.Reader.hasFailed {dir : Direction} (reader : Reader dir) : Bool

Checks if the reader has encountered an error.

@[inline]

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

Feeds new data into the reader's input buffer. If the current input is exhausted, replaces it; otherwise compacts the buffer by discarding already-parsed bytes before appending.

@[inline]

def Std.Http.Protocol.H1.Reader.setInput {dir : Direction} (input : ByteArray.Iterator) (reader : Reader dir) : Reader dir

Replaces the reader's input iterator with a new one.

@[inline]

def Std.Http.Protocol.H1.Reader.setMessageHead {dir : Direction} (messageHead : Message.Head dir) (reader : Reader dir) : Reader dir

Updates the message head being constructed.

@[inline]

def Std.Http.Protocol.H1.Reader.addHeader {dir : Direction} (name : Header.Name) (value : Header.Value) (reader : Reader dir) : Reader dir

Adds a header to the current message head.

@[inline]

def Std.Http.Protocol.H1.Reader.close {dir : Direction} (reader : Reader dir) : Reader dir

Closes the reader, transitioning to the closed state.

@[inline]

def Std.Http.Protocol.H1.Reader.markComplete {dir : Direction} (reader : Reader dir) : Reader dir

Marks the current message as complete and prepares for the next message.

@[inline]

def Std.Http.Protocol.H1.Reader.fail {dir : Direction} (error : Error) (reader : Reader dir) : Reader dir

Transitions the reader to a failed state with the given error.

@[inline]

def Std.Http.Protocol.H1.Reader.reset {dir : Direction} (reader : Reader dir) : Reader dir

Resets the reader to parse a new message on the same connection.

@[inline]

def Std.Http.Protocol.H1.Reader.needsMoreInput {dir : Direction} (reader : Reader dir) : Bool

Checks if more input is needed to continue parsing.

@[inline]

def Std.Http.Protocol.H1.Reader.getError {dir : Direction} (reader : Reader dir) : Option Error

Returns the current parse error if the reader has failed.

@[inline]

def Std.Http.Protocol.H1.Reader.remainingBytes {dir : Direction} (reader : Reader dir) : Nat

Gets the number of bytes remaining in the input buffer.

@[inline]

def Std.Http.Protocol.H1.Reader.advance {dir : Direction} (n : Nat) (reader : Reader dir) : Reader dir

Advances the input iterator by n bytes.

@[inline]

def Std.Http.Protocol.H1.Reader.startHeaders {dir : Direction} (reader : Reader dir) : Reader dir

Transitions to the state for reading headers.

@[inline]

def Std.Http.Protocol.H1.Reader.addBodyBytes {dir : Direction} (n : Nat) (reader : Reader dir) : Reader dir

Adds body bytes parsed for the current message.

@[inline]

def Std.Http.Protocol.H1.Reader.addHeaderBytes {dir : Direction} (n : Nat) (reader : Reader dir) : Reader dir

Adds header bytes accumulated for the current message.

@[inline]

def Std.Http.Protocol.H1.Reader.startFixedBody {dir : Direction} (size : Nat) (reader : Reader dir) : Reader dir

Transitions to the state for reading a fixed-length body.

@[inline]

def Std.Http.Protocol.H1.Reader.startChunkedBody {dir : Direction} (reader : Reader dir) : Reader dir

Transitions to the state for reading chunked transfer encoding.

@[inline]

def Std.Http.Protocol.H1.Reader.markNoMoreInput {dir : Direction} (reader : Reader dir) : Reader dir

Marks that no more input will be provided (connection closed).

def Std.Http.Protocol.H1.Reader.shouldKeepAlive {dir : Direction} (reader : Reader dir) : Bool

Checks if the connection should be kept alive for the next message.