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

Equations

• Std.Http.Protocol.H1.Reader.instInhabitedBodyState = { default := Std.Http.Protocol.H1.Reader.instInhabitedBodyState.default }

@[implicit_reducible]

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

Equations

• Std.Http.Protocol.H1.Reader.instReprBodyState = { reprPrec := Std.Http.Protocol.H1.Reader.instReprBodyState.repr }

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

Equations

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

@[implicit_reducible]

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

Equations

• Std.Http.Protocol.H1.Reader.instBEqBodyState = { beq := Std.Http.Protocol.H1.Reader.instBEqBodyState.beq }

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

Equations

• Std.Http.Protocol.H1.Reader.instBEqBodyState.beq (Std.Http.Protocol.H1.Reader.BodyState.fixed a) (Std.Http.Protocol.H1.Reader.BodyState.fixed b) = (a == b)
• Std.Http.Protocol.H1.Reader.instBEqBodyState.beq Std.Http.Protocol.H1.Reader.BodyState.chunkedSize Std.Http.Protocol.H1.Reader.BodyState.chunkedSize = true
• Std.Http.Protocol.H1.Reader.instBEqBodyState.beq (Std.Http.Protocol.H1.Reader.BodyState.chunkedBody a a_1) (Std.Http.Protocol.H1.Reader.BodyState.chunkedBody b b_1) = (a == b && a_1 == b_1)
• Std.Http.Protocol.H1.Reader.instBEqBodyState.beq Std.Http.Protocol.H1.Reader.BodyState.closeDelimited Std.Http.Protocol.H1.Reader.BodyState.closeDelimited = true
• Std.Http.Protocol.H1.Reader.instBEqBodyState.beq x✝¹ x✝ = false

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✝)

Equations

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

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Equations

• Std.Http.Protocol.H1.Reader.instBEqState.beq Std.Http.Protocol.H1.Reader.State.needStartLine Std.Http.Protocol.H1.Reader.State.needStartLine = true
• Std.Http.Protocol.H1.Reader.instBEqState.beq (Std.Http.Protocol.H1.Reader.State.needHeader a) (Std.Http.Protocol.H1.Reader.State.needHeader b) = (a == b)
• Std.Http.Protocol.H1.Reader.instBEqState.beq (Std.Http.Protocol.H1.Reader.State.readBody a) (Std.Http.Protocol.H1.Reader.State.readBody b) = (a == b)
• Std.Http.Protocol.H1.Reader.instBEqState.beq a.continue b.continue = Std.Http.Protocol.H1.Reader.instBEqState.beq a b
• Std.Http.Protocol.H1.Reader.instBEqState.beq Std.Http.Protocol.H1.Reader.State.pending Std.Http.Protocol.H1.Reader.State.pending = true
• Std.Http.Protocol.H1.Reader.instBEqState.beq Std.Http.Protocol.H1.Reader.State.complete Std.Http.Protocol.H1.Reader.State.complete = true
• Std.Http.Protocol.H1.Reader.instBEqState.beq Std.Http.Protocol.H1.Reader.State.closed Std.Http.Protocol.H1.Reader.State.closed = true
• Std.Http.Protocol.H1.Reader.instBEqState.beq (Std.Http.Protocol.H1.Reader.State.failed a) (Std.Http.Protocol.H1.Reader.State.failed b) = (a == b)
• Std.Http.Protocol.H1.Reader.instBEqState.beq x✝¹ x✝ = false

@[implicit_reducible]

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

Equations

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

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.

Equations

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

@[inline]

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

Checks if the reader has completed parsing the current message.

Equations

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

@[inline]

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

Checks if the reader has encountered an error.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

Closes the reader, transitioning to the closed state.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• reader.reset = { state := Std.Http.Protocol.H1.Reader.State.needStartLine, input := reader.input, messageCount := reader.messageCount, noMoreInput := reader.noMoreInput }

@[inline]

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

Checks if more input is needed to continue parsing.

Equations

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

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

Equations

• reader.getError = match reader.state with | Std.Http.Protocol.H1.Reader.State.failed err => some err | x => none

@[inline]

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

Gets the number of bytes remaining in the input buffer.

Equations

• reader.remainingBytes = reader.input.array.size - reader.input.pos

@[inline]

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

Advances the input iterator by n bytes.

Equations

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

@[inline]

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

Transitions to the state for reading headers.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

Transitions to the state for reading chunked transfer encoding.

Equations

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

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

Equations

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

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.

Equations

• reader.shouldKeepAlive = reader.messageHead.shouldKeepAlive